proposition: Lemma normed_constrained_meet_trans Q1 Q2 H : A \subset H -> H \proper G -> Q1 \in |/|*(A; q) -> Q2 \in |/|*(A; q) -> Q1 :&: H != 1 -> Q2 :&: H != 1 -> exists2 k, k \in K & Q2 :=: Q1 :^ k.
proof: Proof. move: {2}_.+1 (ltnSn (#|G| - #|Q1 :&: Q2|)) => m. elim: m => // m IHm in H Q1 Q2 * => geQ12m sAH prHG maxQ1 maxQ2 ntHQ1 ntHQ2. have:= maxQ1; rewrite inE => /maxgroupP[/andP[qQ1 nQ1A] maxQ1P]. have:= maxQ2; rewrite inE => /maxgroupP[/andP[qQ2 nQ2A] maxQ2P]. have prQ12: Q1 :&: Q2 \proper G. rewrite properT; apply: contraNneq (@mFT_nonSolvable gT) => <-. by apply: pgroup_sol (pgroupS _ qQ1); rewrite subsetIl. wlog defH: H prHG sAH ntHQ1 ntHQ2 / Q1 :&: Q2 != 1 -> H :=: 'N(Q1 :&: Q2). case: (eqVneq (Q1 :&: Q2) 1) => [-> | ntQ12] IH. by apply: (IH H) => //; case/eqP. apply: (IH 'N(Q1 :&: Q2)%G); rewrite ?normsI ?mFT_norm_proper //; apply: contra ntQ12; rewrite -!subG1; apply: subset_trans; by rewrite subsetI normG (subsetIl, subsetIr). pose L := 'O_pi^'(H); have sLH: L \subset H := pcore_sub _ _. have [nLA coLA solL]: [/\ A \subset 'N(L), coprime #|L| #|A| & solvable L]. rewrite gFnorm_trans ?normsG // coprime_sym coprime_pi' ?cardG_gt0 //. by rewrite -pgroupE pcore_pgroup (solvableS sLH) ?mFT_sol. have Qsyl Q: Q \in |/|*(A; q) -> Q :&: H != 1 -> exists R : {group _}, [/\ q.-Sylow(L) R, A \subset 'N(R) & Q :&: H \subset R]. - case/mem_max_normed=> qQ nQA ntQH. have qQH: q.-group (Q :&: H) by rewrite (pgroupS _ qQ) ?subsetIl. have nQHA: A \subset 'N(Q :&: H) by rewrite normsI // normsG. apply: coprime_Hall_subset => //; apply: (hyp71) => //. rewrite inE nQHA /psubgroup subsetIr andbT. by apply: sub_in_pnat qQH => p _; move/eqnP->. have [R1 [sylR1 nR1A sQR1]] := Qsyl _ maxQ1 ntHQ1. have [R2 [sylR2 nR2A sQR2]] := Qsyl _ maxQ2 ntHQ2. have [h Ch defR2] := coprime_Hall_trans nLA coLA solL sylR2 nR2A sylR1 nR1A. have{Ch} [Hh Kh]: h \in H /\ h \in K. case/setIP: Ch => Lh Ch; rewrite (subsetP sLH) //. rewrite (mem_normal_Hall hallK (pcore_normal _ _)) //. by rewrite (mem_p_elt _ Lh) ?pcore_pgroup. have [Q3 maxQ3 sR2Q3] := max_normed_exists (pHall_pgroup sylR2) nR2A. have maxQ1h: (Q1 :^ h)%G \in |/|*(A; q) by rewrite actsKmax. case: (eqsVneq Q1 Q2) => [| neQ12]; first by exists 1; rewrite ?group1 ?conjsg1. have ntHQ3: Q3 :&: H != 1. by apply: subG1_contra ntHQ2; rewrite subsetI subsetIr (subset_trans sQR2). have ntHQ1h: (Q1 :^ h) :&: H != 1. by move: ntHQ1; rewrite !trivg_card1 -(cardJg _ h) conjIg (conjGid Hh). suff [prI1 prI2]: Q1 :&: Q2 \proper Q1 :&: R1 /\ Q1 :&: Q2 \proper Q2 :&: R2. have: #|G| - #|(Q1 :^ h) :&: Q3| < m. rewrite ltnS in geQ12m; apply: leq_trans geQ12m. rewrite ltn_sub2l ?(proper_card prQ12) // -(cardJg _ h) proper_card //. by rewrite (proper_sub_trans _ (setIS _ sR2Q3)) // defR2 -conjIg properJ. have: #|G| - #|Q3 :&: Q2| < m. rewrite ltnS in geQ12m; apply: leq_trans geQ12m. rewrite ltn_sub2l ?proper_card // (proper_sub_trans prI2) //. by rewrite setIC setISS. case/(IHm H) => // k2 Kk2 defQ2; case/(IHm H) => // k3 Kk3 defQ3. by exists (h * k3 * k2); rewrite ?groupM ?conjsgM // -defQ3. case: (eqVneq (Q1 :&: Q2) 1) => [-> | ntQ12]. by rewrite !proper1G; split; [move: ntHQ1 | move: ntHQ2]; apply: subG1_contra; rewrite subsetI subsetIl. rewrite -(setIidPr (subset_trans (pHall_sub sylR1) sLH)) setIA. rewrite -(setIidPr (subset_trans (pHall_sub sylR2) sLH)) setIA. rewrite (setIidPl sQR1) (setIidPl sQR2) {}defH //. have nilQ1 := pgroup_nil qQ1; have nilQ2 := pgroup_nil qQ2. rewrite !nilpotent_proper_norm /proper ?subsetIl ?subsetIr ?subsetI ?subxx //=. by rewrite andbT; apply: contra neQ12 => sQ21; rewrite (maxQ2P Q1) ?qQ1. by apply: contra neQ12 => sQ12; rewrite (maxQ1P Q2) ?qQ2. Qed.
imports: HB(structures) mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun eqtype ssrnat seq div choice fintype bigop) mathcomp(finset prime fingroup morphism automorphism action quotient) mathcomp(gfunctor cyclic pgroup center commutator gseries nilpotent) mathcomp(sylow abelian maximal hall) odd_order(BGsection1 BGsection6)