proposition: Fact BGappendixC3_Ediv : E = [set x^-1 | x in E]%R.
proof: Proof. suffices sEV_E: [set x^-1 | x in E]%R \subset E. by apply/esym/eqP; rewrite eqEcard sEV_E card_imset //=; apply: invr_inj. have /mulG_sub[/(subset_trans sP0P)/subsetP-sP0H /subsetP-sUH] := sdprodW defH. have Hs := sP0H s P0s; have P1t: t \in P1 by rewrite memJ_conjg. have nUP1 t1: t1 \in P1 -> U :^ t1 = U by move/(subsetP nUP0y)/normP. have nUtn n u: u \in U -> u ^ (t ^+ n) \in U. by rewrite -mem_conjgV nUP1 ?groupV ?groupX. have nUtVn n u: u \in U -> u ^ (t ^- n) \in U. by rewrite -mem_conjg nUP1 ?groupX. have Qsti i: s ^- i * t ^+ i \in Q. by rewrite -conjXg -commgEl (subsetP sQP0Q) // commGC mem_commg ?groupX. pose is_sUs m a j n u s1 v := [/\ a \in U, u \in U, v \in U, s1 \in P0 & s ^+ m * a ^ t ^+ j * s ^- n = u * s1 * v]. have split_sUs m a j n: a \in U -> exists u, exists s1, exists v, is_sUs m a j n u s1 v. - move=> Ua; suffices: s ^+ m * a ^ t ^+ j * s ^- n \in H. by case/splitH=> u Uu [v Uv [s1 P0s1 Dusv1]]; exists u, s1, v. by rewrite 2?groupM ?groupV ?groupX // sUH ?nUtn. have nt_sUs m j n a u s1 v: (m == n.+1) || (n == m.+1) -> is_sUs m a j n u s1 v -> s1 != 1. - move/pred2P=> Dmn [Ua Uu Uv _ Dusv]; have{Dmn}: s ^+ m != s ^+ n. by case: Dmn => ->; last rewrite eq_sym; rewrite expgS eq_mulgV1 ?mulgK. apply: contraNneq => s1_1; rewrite {s1}s1_1 mulg1 in Dusv. have:= groupM Uu Uv; rewrite -Dusv => /(not_splitU _ _ (nUtn j a Ua))/orP. by rewrite !in_group // eq_invg1 -eq_mulgV1 => -[]// /andP[? /eqP->]. have sUs_modP m a j n u s1 v: is_sUs m a j n u s1 v -> a ^ t ^+ j = u * v. have [nUP /isom_inj/injmP/=quoUP_inj] := sdprod_isom defH. case=> Ua Uu Uv P0s1 /(congr1 (coset P)); rewrite (conjgCV u) -(mulgA _ u). rewrite coset_kerr ?groupV 2?coset_kerl ?groupX //; last first. by rewrite -mem_conjg (normsP nUP) // (subsetP sP0P). by move/quoUP_inj->; rewrite ?nUtn ?groupM. have expUMp u v Uu Uv := expgMn p (centsP cUU u v Uu Uv). have sUsXp m a j n u s1 v: is_sUs m a j n u s1 v -> is_sUs m (a ^+ p) j n (u ^+ p) s1 (v ^+ p). - move=> Dusv; have{Dusv} [/sUs_modP Duv [Ua Uu Vv P0s1 Dusv]] := (Dusv, Dusv). split; rewrite ?groupX //; move: P0s1 Dusv; rewrite -defP0 => /cycleP[k ->]. rewrite conjXg -!(mulgA _ (s ^+ k)) ![s ^+ k * _]conjgC 2!mulgA -expUMp //. rewrite {}Duv ![s ^+ m * _]conjgC !conjXg -![_ * _ * s ^- n]mulgA. move/mulgI/(congr1 (Frobenius_aut charFp \o sigma))=> /= Duv_p. congr (_ * _); apply/(injmP inj_sigma); rewrite ?in_PU //. by rewrite !{1}sigmaE ?in_PU // rmorphB !rmorphMn rmorph1 in Duv_p *. have odd_P: odd #|P| by rewrite oP oddX odd_p orbT. suffices EpsiV a: a \in U -> psi a \in E -> psi (a^-1 ^ t ^+ 3) \in E. apply/subsetP => _ /imsetP[x Ex ->]. have /imsetP[a Ua Dx]: x \in psi @: U by rewrite im_psi; case/setIdP: Ex. suffices: psi (a^-1 ^ t ^+ (3 * #|P|)) \in E. rewrite Dx -psiV // -{2}(conjg1 a^-1); congr (psi (_ ^ _) \in E). by apply/eqP; rewrite -order_dvdn orderJ dvdn_mull ?order_dvdG. rewrite -(odd_double_half #|P|) odd_P addnC. elim: _./2 => [|n /EpsiV/EpsiV/=]; first by rewrite EpsiV -?Dx. by rewrite conjVg invgK -!conjgM -!expgD -!mulnSr !(groupV, nUtn) //; apply. move=> Ua Ea; have{Ea} [b Ub Dab]: exists2 b, b \in U & psi a + psi b = 2%:R. case/setIdP: Ea => _; rewrite -im_psi => /imsetP[b Ub Db]; exists b => //. by rewrite -Db addrC subrK. have [u2 [s2 [v2 usv2P]]] := split_sUs 3%N (a * _) 2%N 1%N (groupM Ua (groupVr Ub)). have{Ua} [u1 [s1 [v1 usv1P]]] := split_sUs 1%N a^-1 3%N 2%N (groupVr Ua). have{Ub} [u3 [s3 [v3 usv3P]]] := split_sUs 2%N b 1%N 3%N Ub. pose s2def w1 w2 w3 := t * s2^-1 * t = w1 * s3 * w2 * t ^+ 2 * s1 * w3. pose w1 := v2 ^ t^-1 * u3; pose w2 := v3 * u1 ^ t ^- 2; pose w3 := v1 * u2 ^ t. have stXC m n: (m <= n)%N -> s ^- n ^ t ^+ m = s ^- m ^ t ^+ n * s ^- (n - m). move/subnK=> Dn; apply/(mulgI (s ^- (n - m) * t ^+ n))/(mulIg (t ^+ (n - m))). rewrite -{1}[in t ^+ n]Dn expgD !mulgA !mulgK -invMg -2!mulgA -!expgD. by rewrite addnC Dn (centsP (abelem_abelian abelQ)) ?mulgA. wlog suffices Ds2: a b u1 v1 u2 v2 u3 v3 @w1 @w2 @w3 Dab usv1P usv2P usv3P / s2def w1 w2 w3; last first. - apply/esym; rewrite -[_ * t]mulgA [_ * t]conjgC mulgA -(expgS _ 1) conjVg. rewrite /w2 mulgA; apply: (canRL (mulKVg _)); rewrite 2!mulgA -conjgE. rewrite conjMg conjgKV /w3 mulgA; apply: (canLR (mulgKV _)). rewrite /w1 -4!mulgA (mulgA u1) (mulgA u3) conjMg -conjgM mulKg -mulgA. have [[[Ua _ _ _ <-] [_ _ _ _ Ds2]] [Ub _ _ _ <-]] := (usv1P, usv2P, usv3P). apply: (canLR (mulKVg _)); rewrite -!invMg -!conjMg -{}Ds2 groupV in Ua *. rewrite -[t]expg1 2!conjMg -conjgM -expgS 2!conjMg -conjgM -expgSr mulgA. apply: (canLR (mulgK _)); rewrite 2!invMg -!conjVg invgK invMg invgK -4!mulgA. rewrite (mulgA _ s) stXC // mulgKV -!conjMg stXC // mulgKV -conjMg conjgM. apply: (canLR (mulKVg _)); rewrite -2!conjVg 2!mulgA -conjMg (stXC 1%N) //. rewrite mulgKV -conjgM -expgSr -mulgA -!conjMg; congr (_ ^ t ^+ 3). apply/(canLR (mulKVg _))/(canLR (mulgK _))/(canLR invgK). rewrite -!mulgA (mulgA _ b) mulgA invMg -!conjVg !invgK. by apply/(injmP inj_sigma); rewrite 1?groupM ?sigmaE ?memJ_P. have [[Ua Uu1 Uv1 P0s1 Dusv1] /sUs_modP-Duv1] := (usv1P, usv1P). have [[_ Uu2 Uv2 P0s2 _] [Ub Uu3 Uv3 P0s3 _]] := (usv2P, usv3P). suffices /(congr1 sigma): s ^+ 2 = s ^ v1 * s ^ a^-1 ^ t ^+ 3. rewrite inE sigmaX // sigma_s sigmaM ?memJ_P -?psiE ?nUtn // => ->. by rewrite addrK -!im_psi !imset_f ?nUtn. rewrite groupV in Ua; have [Hs1 Hs3]: s1 \in H /\ s3 \in H by rewrite !sP0H. have nt_s1: s1 != 1 by apply: nt_sUs usv1P. have nt_s3: s3 != 1 by apply: nt_sUs usv3P. have{sUsXp} Ds2p: s2def (w1 ^+ p) (w2 ^+ p) (w3 ^+ p). have [/sUsXp-usv1pP /sUsXp-usv2pP /sUsXp-usv3pP] := And3 usv1P usv2P usv3P. rewrite expUMp ?groupV // !expgVn in usv1pP usv2pP. rewrite !(=^~ conjXg _ _ p, expUMp) ?groupV -1?[t]expg1 ?nUtn ?nUtVn //. apply: Ds2 usv1pP usv2pP usv3pP => //. by rewrite !psiX // -!Frobenius_autE -rmorphD Dab rmorph_nat. have{} Ds2: s2def w1 w2 w3 by apply: Ds2 usv1P usv2P usv3P. wlog [Uw1 Uw2 Uw3]: w1 w2 w3 Ds2p Ds2 / [/\ w1 \in U, w2 \in U & w3 \in U]. by move/(_ w1 w2 w3)->; rewrite ?(nUtVn, nUtVn 1%N, nUtn 1%N, in_group). have{Ds2p} Dw3p: (w2 ^- p * w1 ^- p.-1 ^ s3 * w2) ^ t ^+ 2 = w3 ^+ p.-1 ^ s1^-1. rewrite -[w1 ^+ _](mulKg w1) -[w3 ^+ _](mulgK w3) -expgS -expgSr !prednK //. rewrite -(canLR (mulKg _) Ds2p) -(canLR (mulKg _) Ds2) 6!invMg !invgK. by rewrite mulgA mulgK [2%N]lock /conjg !mulgA mulVg mul1g mulgK. have w_id w: w \in U -> w ^+ p.-1 == 1 -> w = 1. by move=> Uw /eqP/(canRL_in (expgK _) Uw)->; rewrite ?expg1n ?oU. have{Uw3} Dw3: w3 = 1. apply: w_id => //; have:= @not_splitU s1^-1^-1 s1^-1 (w3 ^+ p.-1). rewrite !groupV mulVg eqxx andbT {2}invgK (negPf nt_s1) groupX //= => -> //. have /tiH_P1 <-: t ^+ 2 \in P1^#. rewrite 2!inE groupX // andbT -order_dvdn gtnNdvd // orderJ. by rewrite odd_gt2 ?order_gt1 // orderE defP0 (oddSg sP0P). by rewrite -mulgA -conjgE inE -{2}Dw3p memJ_conjg !in_group ?Hs1 // sUH. have{Dw3p} Dw2p: w2 ^+ p.-1 = w1 ^- p.-1 ^ s3. apply/(mulIg w2)/eqP; rewrite -expgSr prednK // eq_mulVg1 mulgA. by rewrite (canRL (conjgK _) Dw3p) Dw3 expg1n !conj1g. have{Uw1} Dw1: w1 = 1. apply: w_id => //; have:= @not_splitU s3^-1 s3 (w1 ^- p.-1). rewrite mulVg (negPf nt_s3) andbF -mulgA -conjgE -Dw2p !in_group //=. by rewrite eqxx andbT eq_invg1 /= => ->. have{w1 w2 w3 Dw1 Dw3 w_id Uw2 Dw2p} Ds2: t * s2^-1 * t = s3 * t ^+ 2 * s1. by rewrite Ds2 Dw3 [w2]w_id ?mulg1 ?Dw2p ?Dw1 ?mul1g // expg1n invg1 conj1g. have /centsP abP0: abelian P0 by rewrite -defP0 cycle_abelian. have QP0ys := memJ_norm y (subsetP (commg_normr P0 Q) _ _). have{QP0ys} memQP0 := (QP0ys, groupV, groupM); have nQ_P0 := subsetP nQP0. have sQP0_Q: [~: Q, P0] \subset Q by rewrite commg_subl. have /centsP abQP0 := abelianS sQP0_Q (abelem_abelian abelQ). have{s2def} Ds312: s3 * s1 * s2 = 1. apply/set1P; rewrite -set1gE -(coprime_TIg coQP) inE. rewrite coset_idr ?(subsetP sP0P) ?nQ_P0 ?groupM //. rewrite -mulgA -[s2](mulgK s) [_ * s]abP0 // -[s2](mulKVg s). rewrite -!mulgA [s * _]mulgA [s1 * _]mulgA [s1 * _]abP0 ?groupM //. rewrite 2!(mulgA s3) [s^-1 * _]mulgA !(morphM, morphV) ?nQ_P0 ?in_group //=. have ->: coset Q s = coset Q t by rewrite coset_kerl ?groupV ?coset_kerr. have nQt: t \in 'N(Q) by rewrite -(conjGid Qy) normJ memJ_conjg nQ_P0. rewrite -morphV // -!morphM ?(nQt, groupM) ?groupV // ?nQ_P0 //= -Ds2. by rewrite 2!mulgA mulgK mulgKV mulgV morph1. pose x := (y ^ s3)^-1 * y ^ s^-1 * (y ^ (s * s1)^-1)^-1 * y. have{abP0} Dx: x ^ s^-1 = x. rewrite 3!conjMg !conjVg -!conjgM -!invMg (mulgA s) -(expgS _ 1). rewrite [x]abQP0 ?memQP0 // [rhs in y * rhs]abQP0 ?memQP0 //. apply/(canRL (mulKVg _)); rewrite 4!mulgA; congr (_ * _). rewrite [RHS]abQP0 ?memQP0 //; apply/(canRL (mulgK _))/eqP. rewrite -3!mulgA [rhs in y^-1 * rhs]abQP0 ?memQP0 // -eq_invg_sym eq_invg_mul. apply/eqP; transitivity (t ^+ 2 * s1 * (t^-1 * s2 * t^-1) * s3); last first. by rewrite -[s2]invgK -!invMg mulgA Ds2 -(mulgA s3) invMg mulKVg mulVg. rewrite (canRL (mulKg _) Ds312) -2![_ * t^-1]mulgA. have Dt1 si: si \in P0 -> t^-1 = (s^-1 ^ si) ^ y. by move=> P0si; rewrite {2}/conjg -conjVg -(abP0 si) ?groupV ?mulKg. by rewrite {1}(Dt1 s1) // (Dt1 s3^-1) ?groupV // -conjXg /conjg !{1}gnorm. have{Dx memQP0} Dx1: x = 1. apply/set1P; rewrite -set1gE; have [_ _ _ <-] := dprodP defQ. rewrite setIAC (setIidPr sQP0_Q) inE -{2}defP0 -cycleV cent_cycle. by rewrite (sameP cent1P commgP) commgEl Dx mulVg eqxx !memQP0. pose t1 := s1 ^ y; pose t3 := s3 ^ y. have{x Dx1} Ds13: s1 * (t * t1)^-1 = (t3 * t)^-1 * s3. by apply/eqP; rewrite eq_sym eq_mulVg1 invMg invgK -Dx1 /x /conjg !gnorm. suffices Ds1: s1 = s^-1. rewrite -(canLR (mulKg _) (canRL (mulgKV _) Dusv1)) Ds1 Duv1. by rewrite !invMg invgK /conjg !gnorm. have [_ _ /trivgPn[u Uu nt_u] _ _] := Frobenius_context frobH. apply: (conjg_inj y); apply: contraNeq nt_u. rewrite -/t1 conjVg -/t eq_mulVg1 -invMg => nt_tt1. have Hu := sUH u Uu; have P1tt1: t * t1 \in P1 by rewrite groupM ?memJ_conjg. have /tiH_P1 defU: (t * t1)^-1 \in P1^# by rewrite 2!inE nt_tt1 groupV. suffices: (u ^ s1) ^ (t * t1)^-1 \in U. rewrite -mem_conjg nUP1 // conjgE mulgA => /(not_splitU _ _ Uu). by rewrite groupV (negPf nt_s1) andbF mulVg eqxx andbT /= => /(_ _ _)/eqP->. rewrite -defU inE memJ_conjg -conjgM Ds13 conjgM groupJ ?(groupJ _ Hs1) //. by rewrite sUH // -mem_conjg nUP1 // groupM ?memJ_conjg. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun eqtype choice ssrnat seq div fintype tuple finfun) mathcomp(bigop order ssralg finset prime binomial poly polydiv) mathcomp(fingroup morphism quotient automorphism action finalg zmodp) mathcomp(gfunctor gproduct cyclic commutator pgroup abelian frobenius) odd_order(BGsection1) mathcomp(matrix mxalgebra mxabelem vector falgebra fieldext galois) mathcomp(finfield ssrnum algC classfun character integral_char inertia)