proposition: Corollary exceptional_structure (Ms := M`_\sigma) : [/\ A :=: 'Ohm_1(P), 'C_Ms(A) = 1 & exists2 A1, A1 \in 'E_p^1(A) & exists2 A2, A2 \in 'E_p^1(A) & [/\ A1 :!=: A2, 'C_Ms(A1) = 1 & 'C_Ms(A2) = 1]].
proof: Proof. pose iMNA := #|'N(A) : M|. have defA: A :=: 'Ohm_1(P). apply/eqP; rewrite eqEcard -{1}(Ohm1_id abelA) OhmS //= oA -rM. rewrite -(p_rank_Sylow sylP) p_rank_abelian ?exceptional_Sylow_abelian //. by rewrite -card_pgroup // (pgroupS _ (pHall_pgroup sylP)) ?Ohm_sub. have iMNAgt1: iMNA > 1. rewrite indexg_gt1 defA; apply: contra (subset_trans _) not_sNP_M. by rewrite char_norms ?Ohm_char. have iMNAgt2: iMNA > 2. pose q := pdiv iMNA; have q_iMNA: q %| iMNA := pdiv_dvd iMNA. rewrite (leq_trans _ (dvdn_leq (ltnW _) q_iMNA)) // ltn_neqAle eq_sym. rewrite (sameP eqP (prime_oddPn _)) ?prime_gt1 ?pdiv_prime //. by rewrite (dvdn_odd q_iMNA) // (dvdn_odd (dvdn_indexg _ _)) ?mFT_odd. rewrite [iMNA](cardD1 (gval M)) orbit_refl !ltnS lt0n in iMNAgt1 iMNAgt2. have{iMNAgt1} [Mg1 /= NM_Mg1] := pred0Pn iMNAgt1. rewrite (cardD1 Mg1) inE /= NM_Mg1 ltnS lt0n in iMNAgt2. have{iMNAgt2} [Mg2 /= NM_Mg2] := pred0Pn iMNAgt2. case/andP: NM_Mg1 => neM_Mg1 /rcosetsP[g1 nAg1 defMg1]. have{neM_Mg1} notMg1: g1 \notin M. by apply: contra neM_Mg1 => M_g1; rewrite defMg1 rcoset_id. case/and3P: NM_Mg2 => neMg12 neM_Mg2 /rcosetsP[g2 nAg2 defMg2]. have{neM_Mg2} notMg2: g2 \notin M. by apply: contra neM_Mg2 => M_g2; rewrite defMg2 rcoset_id. pose A1 := (A0 :^ g1)%G; pose A2 := (A0 :^ g2)%G. have EpA1: A1 \in 'E_p^1(A) by rewrite -(normP nAg1) pnElemJ. have EpA2: A2 \in 'E_p^1(A) by rewrite -(normP nAg2) pnElemJ. have{neMg12} neqA12: A1 :!=: A2. rewrite -(canF_eq (conjsgKV g2)) -conjsgM (sameP eqP normP). rewrite (contra (subsetP sNA0_M _)) // -mem_rcoset. by apply: contra neMg12 => g1Mg2; rewrite defMg1 defMg2 (rcoset_eqP g1Mg2). have{notMg1 nAg1} regA1: 'C_Ms(A1) = 1. by case/exceptional_TI_MsigmaJ: notMg1; rewrite // -(normP nAg1) conjSg. have{notMg2 nAg2} regA2: 'C_Ms(A2) = 1. by case/exceptional_TI_MsigmaJ: notMg2; rewrite // -(normP nAg2) conjSg. split=> //; last by exists A1 => //; exists A2 => //. by apply/trivgP; rewrite -regA1 setIS ?centS //; case/pnElemP: EpA1. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun eqtype ssrnat seq div path fintype) mathcomp(bigop finset prime fingroup morphism perm automorphism quotient) mathcomp(action gproduct gfunctor pgroup cyclic center commutator) mathcomp(gseries nilpotent sylow abelian maximal hall) odd_order(BGsection1 BGsection3 BGsection4 BGsection5 BGsection6) odd_order(BGsection7 BGsection10)