proposition: Theorem Puig_factorization : 'O_p^'(G) * 'N_G('Z('L(S))) = G.
proof: Proof. set D := 'O_p^'(G); set Z := 'Z(_); have [sSG pS _] := and3P sylS. have sSN: S \subset 'N(D) by rewrite (subset_trans sSG) ?gFnorm. have p'D: p^'.-group D := pcore_pgroup _ _. have tiSD: S :&: D = 1 := coprime_TIg (pnat_coprime pS p'D). have def_Zq: Z / D = 'Z('L(S / D)). rewrite !quotientE -(setIid S) -(morphim_restrm sSN); set f := restrm _ _. have injf: 'injm f by rewrite ker_restrm ker_coset tiSD. rewrite -!(injmF _ injf) ?Puig_sub //= morphim_restrm. by rewrite (setIidPr _) // subIset ?Puig_sub. have{def_Zq} nZq: Z / D <| G / D. have sylSq: p.-Sylow(G / D) (S / D) by apply: morphim_pHall. rewrite def_Zq (Puig_center_normal _ _ sylSq) ?quotient_odd ?quotient_sol //. exact: trivg_pcore_quotient. have sZS: Z \subset S by rewrite subIset ?Puig_sub. have sZN: Z \subset 'N_G(Z) by rewrite subsetI normG (subset_trans sZS). have nDZ: Z \subset 'N(D) by rewrite (subset_trans sZS). rewrite -(mulSGid sZN) mulgA -(norm_joinEr nDZ) (@Frattini_arg p) //= -/D -/Z. rewrite -cosetpre_normal quotientK ?quotientGK ?pcore_normal // in nZq. by rewrite norm_joinEr. rewrite /pHall -divgS joing_subr ?(pgroupS sZS) /= ?norm_joinEr //= -/Z. by rewrite TI_cardMg ?mulnK //; apply/trivgP; rewrite /= setIC -tiSD setSI. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun eqtype ssrnat seq div) mathcomp(fintype bigop prime finset ssralg fingroup morphism) mathcomp(automorphism quotient gfunctor commutator zmodp center pgroup) mathcomp(sylow gseries nilpotent abelian maximal) mathcomp(matrix mxalgebra mxrepresentation mxabelem) odd_order(BGsection1 BGsection2)