proposition: Lemma row_gen_sum_mxval W (i : 'I_m) : row i (val_gen W) = \sum_j row (gen_base 0 j) (mxval (W i j)).
proof: Proof. rewrite -val_gen_row [row i W]row_sum_delta val_gen_sum. apply: eq_bigr => /= j _ /[1!mxE]; move: {W i}(W i j) => x. have ->: x = \sum_k gen (val x 0 k) * inFA (delta_mx 0 k). case: x => u; apply: mxval_inj; rewrite {1}[u]row_sum_delta. rewrite mxval_sum [mxval _]horner_rVpoly mulmx_suml linear_sum /=. apply: eq_bigr => k _; rewrite mxvalM genK [mxval _]horner_rVpoly /=. by rewrite mul_scalar_mx -scalemxAl linearZ. rewrite scaler_suml val_gen_sum mxval_sum linear_sum; apply: eq_bigr => k _. rewrite mxvalM genK mul_scalar_mx linearZ [mxval _]horner_rVpoly /=. rewrite -scalerA; apply: (canLR in_genK); rewrite in_genZ; congr (_ *: _). apply: (canRL val_genK); transitivity (row (mxvec_index j k) base); last first. by rewrite -rowE rowK mxvecE mxE rowK mxvecK. rewrite rowE -mxvec_delta -[val_gen _](row_id 0) rowK /=; congr (mxvec _ *m _). apply/row_matrixP=> j'; rewrite rowK !mxE mulr_natr rowE mul_delta_mx_cond. by rewrite !mulrb (fun_if rVval). Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path) mathcomp(div choice fintype tuple finfun bigop prime) mathcomp(ssralg poly polydiv finset fingroup morphism) mathcomp(perm automorphism quotient finalg action zmodp) mathcomp(commutator cyclic center pgroup matrix mxalgebra) mathcomp(mxpoly)