proposition: Corollary any_cent_rank3_Uniquness p A B : abelian A -> p.-group A -> 'r(A) >= 3 -> A \in 'U -> p.-group B -> ~~ cyclic B -> 'r_p('C(B)) >= 3 -> B \in 'U.
proof: Proof. move=> cAA pA rA3 uA pB ncycB /p_rank_geP[C /= Ep3C]. have [cBC abelC dimC3] := pnElemP Ep3C; have [pC cCC _] := and3P abelC. have [P /= sylP sCP] := Sylow_superset (subsetT _) pC. wlog sAP: A pA cAA rA3 uA / A \subset P. move=> IHA; have [x _] := Sylow_Jsub sylP (subsetT _) pA. by apply: IHA; rewrite ?pgroupJ ?abelianJ ?rankJ ?uniq_mmaxJ. have ncycC: ~~ cyclic C by rewrite (abelem_cyclic abelC) dimC3. have ncycP: ~~ cyclic P := contra (cyclicS sCP) ncycC. have [D] := ex_odd_normal_p2Elem (pHall_pgroup sylP) (mFT_odd _) ncycP. case/andP=> sDP nDP /pnElemP[_ abelD dimD2]. have CADge2: 'r('C_A(D)) >= 2. move: rA3; rewrite (rank_pgroup pA) => /p_rank_geP[E]. case/pnElemP=> sEA abelE dimE3; apply: leq_trans (rankS (setSI _ sEA)). rewrite (rank_abelem (abelemS (subsetIl _ _) abelE)) -(leq_add2r 1) addn1. rewrite -dimE3 -leq_subLR -logn_div ?cardSg ?divgS ?subsetIl //. rewrite logn_quotient_cent_abelem ?dimD2 //. exact: subset_trans (subset_trans sAP nDP). have CCDge2: 'r('C_C(D)) >= 2. rewrite (rank_abelem (abelemS (subsetIl _ _) abelC)) -(leq_add2r 1) addn1. rewrite -dimC3 -leq_subLR -logn_div ?cardSg ?divgS ?subsetIl //. by rewrite logn_quotient_cent_abelem ?dimD2 //; apply: subset_trans nDP. rewrite centsC in cBC; apply: cent_uniq_Uniqueness cBC _; last first. by rewrite ltnNge (rank_pgroup pB) -odd_pgroup_rank1_cyclic ?mFT_odd. have cCDC: C \subset 'C('C_C(D)) by rewrite (sub_abelian_cent (abelem_abelian abelC)) ?subsetIl. apply: cent_uniq_Uniqueness cCDC _; last by rewrite (rank_abelem abelC) dimC3. apply: cent_uniq_Uniqueness (subsetIr _ _) CCDge2. have cDCA: D \subset 'C('C_A(D)) by rewrite centsC subsetIr. apply: cent_uniq_Uniqueness cDCA _; last by rewrite (rank_abelem abelD) dimD2. by apply: cent_uniq_Uniqueness uA _ CADge2; rewrite subIset // -abelianE cAA. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun eqtype ssrnat seq div fintype path) mathcomp(finset prime fingroup action automorphism quotient cyclic) mathcomp(gproduct gfunctor pgroup center commutator gseries nilpotent) mathcomp(sylow abelian maximal hall) odd_order(BGsection1 BGsection4 BGsection5 BGsection6) odd_order(BGsection7 BGsection8)