proposition: Lemma gal_matrix : {w : #|A|.-tuple L | {subset w <= E} /\ 0 \notin w & [/\ \matrix_(i, j < #|A|) enum_val i (tnth w j) \in unitmx, directv (\sum_i K * <[tnth w i]>) & group_set A -> (\sum_i K * <[tnth w i]>)%VS = E] }.
proof: Proof. pose nzE (w : #|A|.-tuple L) := {subset w <= E} /\ 0 \notin w. pose M w := \matrix_(i, j < #|A|) nth 1%g (enum A) i (tnth w j). have [w [Ew nzw] uM]: {w : #|A|.-tuple L | nzE w & M w \in unitmx}. rewrite {}/nzE {}/M cardE; have: uniq (enum A) := enum_uniq _. elim: (enum A) => [|x s IHs] Uxs. by exists [tuple]; rewrite // flatmx0 -(flatmx0 1%:M) unitmx1. have [s'x Us]: x \notin s /\ uniq s by apply/andP. have{IHs} [w [Ew nzw] uM] := IHs Us; set M := \matrix_(i, j) _ in uM. pose a := \row_i x (tnth w i) *m invmx M. pose c_ y := oapp (a 0) (-1) (insub (index y s)). have cx_n1 : c_ x = -1 by rewrite /c_ insubN ?index_mem. have nz_cx : c_ x != 0 by rewrite cx_n1 oppr_eq0 oner_neq0. have Px: [pred y in x :: s] x := mem_head x s. have{Px nz_cx} /sig2W[w0 Ew0 nzS] := gal_independent_contra Px nz_cx. exists [tuple of cons w0 w]. split; first by apply/allP; rewrite /= Ew0; apply/allP. rewrite inE negb_or (contraNneq _ nzS) // => <-. by rewrite big1 // => y _; rewrite rmorph0 mulr0. rewrite unitmxE -[\det _]mul1r; set M1 := \matrix_(i, j < 1 + size s) _. have <-: \det (block_mx 1 (- a) 0 1%:M) = 1 by rewrite det_ublock !det1 mulr1. rewrite -det_mulmx -[M1]submxK mulmx_block !mul0mx !mul1mx !add0r !mulNmx. have ->: drsubmx M1 = M by apply/matrixP => i j; rewrite !mxE !(tnth_nth 0). have ->: ursubmx M1 - a *m M = 0. by apply/rowP=> i; rewrite mulmxKV // !mxE !(tnth_nth 0) subrr. rewrite det_lblock unitrM andbC -unitmxE uM unitfE -oppr_eq0. congr (_ != 0): nzS; rewrite [_ - _]mx11_scalar det_scalar !mxE opprB /=. rewrite -big_uniq // big_cons /= cx_n1 mulN1r addrC; congr (_ + _). rewrite (big_nth 1%g) big_mkord; apply: eq_bigr => j _. by rewrite /c_ index_uniq // valK; congr (_ * _); rewrite !mxE. exists w => [//|]; split=> [||gA]. - by congr (_ \in unitmx): uM; apply/matrixP=> i j; rewrite !mxE -enum_val_nth. - apply/directv_sum_independent=> kw_ Kw_kw sum_kw_0 j _. have /fin_all_exists2[k_ Kk_ Dk_] i := memv_cosetP (Kw_kw i isT). pose kv := \col_i k_ i. transitivity (kv j 0 * tnth w j); first by rewrite !mxE. suffices{j}/(canRL (mulKmx uM))->: M w *m kv = 0 by rewrite mulmx0 mxE mul0r. apply/colP=> i /[!mxE]; pose Ai := nth 1%g (enum A) i. transitivity (Ai (\sum_j kw_ j)); last by rewrite sum_kw_0 rmorph0. rewrite rmorph_sum; apply: eq_bigr => j _; rewrite !mxE /= -/Ai. rewrite Dk_ mulrC rmorphM /=; congr (_ * _). by have /mem_fixedFieldP[_ -> //] := Kk_ j; rewrite -mem_enum mem_nth -?cardE. pose G := group gA; have G_1 := group1 G; pose iG := enum_rank_in G_1. apply/eqP; rewrite eqEsubv; apply/andP; split. apply/subv_sumP=> i _; apply: subv_trans (asubv _). by rewrite prodvS ?capvSl // -memvE Ew ?mem_tnth. apply/subvP=> w0 Ew0; apply/memv_sumP. pose wv := \col_(i < #|A|) enum_val i w0; pose v := invmx (M w) *m wv. exists (fun i => tnth w i * v i 0) => [i _|]; last first. transitivity (wv (iG 1%g) 0); first by rewrite mxE enum_rankK_in ?gal_id. rewrite -[wv](mulKVmx uM) -/v mxE; apply: eq_bigr => i _. by congr (_ * _); rewrite !mxE -enum_val_nth enum_rankK_in ?gal_id. rewrite mulrC memv_mul ?memv_line //; apply/fixedFieldP=> [|x Gx]. rewrite mxE rpred_sum // => j _; rewrite !mxE rpredM //; last exact: memv_gal. have E_M k l: M w k l \in E by rewrite mxE memv_gal // Ew ?mem_tnth. have Edet n (N : 'M_n) (E_N : forall i j, N i j \in E): \det N \in E. by apply: rpred_sum => sigma _; rewrite rpredMsign rpred_prod. rewrite /invmx uM 2!mxE mulrC rpred_div ?Edet //. by rewrite rpredMsign Edet // => k l; rewrite 2!mxE. suffices{i} {2}<-: map_mx x v = v by rewrite [map_mx x v i 0]mxE. have uMx: map_mx x (M w) \in unitmx by rewrite map_unitmx. rewrite map_mxM map_invmx /=; apply: canLR {uMx}(mulKmx uMx) _. apply/colP=> i /[!mxE]; pose ix := iG (enum_val i * x)%g. have Dix b: b \in E -> enum_val ix b = x (enum_val i b). by move=> Eb; rewrite enum_rankK_in ?groupM ?enum_valP // galM ?lfunE. transitivity ((M w *m v) ix 0); first by rewrite mulKVmx // mxE Dix. rewrite mxE; apply: eq_bigr => j _; congr (_ * _). by rewrite !mxE -!enum_val_nth Dix // ?Ew ?mem_tnth. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq div) mathcomp(choice fintype tuple finfun bigop ssralg poly) mathcomp(polydiv finset fingroup morphism quotient perm) mathcomp(action zmodp cyclic matrix mxalgebra vector) mathcomp(falgebra fieldext separable)