# Metamath Proof Explorer

## Theorem sylow2b

Description: Sylow's second theorem. Any P -group H is a subgroup of a conjugated P -group K of order P ^ n || ( #X ) with n maximal. This is usually stated under the assumption that K is a Sylow subgroup, but we use a slightly different definition, whose equivalence to this one requires this theorem. This is part of Metamath 100 proof #72. (Contributed by Mario Carneiro, 18-Jan-2015)

Ref Expression
Hypotheses sylow2b.x ${⊢}{X}={\mathrm{Base}}_{{G}}$
sylow2b.xf ${⊢}{\phi }\to {X}\in \mathrm{Fin}$
sylow2b.h ${⊢}{\phi }\to {H}\in \mathrm{SubGrp}\left({G}\right)$
sylow2b.k ${⊢}{\phi }\to {K}\in \mathrm{SubGrp}\left({G}\right)$
sylow2b.a
sylow2b.hp ${⊢}{\phi }\to {P}\mathrm{pGrp}\left({G}{↾}_{𝑠}{H}\right)$
sylow2b.kn ${⊢}{\phi }\to \left|{K}\right|={{P}}^{{P}\mathrm{pCnt}\left|{X}\right|}$
sylow2b.d
Assertion sylow2b

### Proof

Step Hyp Ref Expression
1 sylow2b.x ${⊢}{X}={\mathrm{Base}}_{{G}}$
2 sylow2b.xf ${⊢}{\phi }\to {X}\in \mathrm{Fin}$
3 sylow2b.h ${⊢}{\phi }\to {H}\in \mathrm{SubGrp}\left({G}\right)$
4 sylow2b.k ${⊢}{\phi }\to {K}\in \mathrm{SubGrp}\left({G}\right)$
5 sylow2b.a
6 sylow2b.hp ${⊢}{\phi }\to {P}\mathrm{pGrp}\left({G}{↾}_{𝑠}{H}\right)$
7 sylow2b.kn ${⊢}{\phi }\to \left|{K}\right|={{P}}^{{P}\mathrm{pCnt}\left|{X}\right|}$
8 sylow2b.d
9 eqid ${⊢}{G}{~}_{\mathit{QG}}{K}={G}{~}_{\mathit{QG}}{K}$
10 oveq2
11 10 cbvmptv
12 oveq1
13 12 mpteq2dv
14 11 13 syl5eq
15 14 rneqd
16 mpteq1
17 16 rneqd
18 15 17 cbvmpov
19 1 2 3 4 5 9 18 6 7 8 sylow2blem3