Metamath Proof Explorer

Theorem fislw

Description: The sylow subgroups of a finite group are exactly the groups which have cardinality equal to the maximum power of P dividing the group. (Contributed by Mario Carneiro, 16-Jan-2015)

Ref Expression
Hypothesis fislw.1 
|- X = ( Base ` G )
Assertion fislw 
|- ( ( G e. Grp /\ X e. Fin /\ P e. Prime ) -> ( H e. ( P pSyl G ) <-> ( H e. ( SubGrp ` G ) /\ ( # ` H ) = ( P ^ ( P pCnt ( # ` X ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 fislw.1 
 |-  X = ( Base ` G )
2 simpr 
 |-  ( ( ( G e. Grp /\ X e. Fin /\ P e. Prime ) /\ H e. ( P pSyl G ) ) -> H e. ( P pSyl G ) )
3 slwsubg 
 |-  ( H e. ( P pSyl G ) -> H e. ( SubGrp ` G ) )
4 2 3 syl 
 |-  ( ( ( G e. Grp /\ X e. Fin /\ P e. Prime ) /\ H e. ( P pSyl G ) ) -> H e. ( SubGrp ` G ) )
5 simpl2 
 |-  ( ( ( G e. Grp /\ X e. Fin /\ P e. Prime ) /\ H e. ( P pSyl G ) ) -> X e. Fin )
6 1 5 2 slwhash 
 |-  ( ( ( G e. Grp /\ X e. Fin /\ P e. Prime ) /\ H e. ( P pSyl G ) ) -> ( # ` H ) = ( P ^ ( P pCnt ( # ` X ) ) ) )
7 4 6 jca 
 |-  ( ( ( G e. Grp /\ X e. Fin /\ P e. Prime ) /\ H e. ( P pSyl G ) ) -> ( H e. ( SubGrp ` G ) /\ ( # ` H ) = ( P ^ ( P pCnt ( # ` X ) ) ) ) )
8 simpl3 
 |-  ( ( ( G e. Grp /\ X e. Fin /\ P e. Prime ) /\ ( H e. ( SubGrp ` G ) /\ ( # ` H ) = ( P ^ ( P pCnt ( # ` X ) ) ) ) ) -> P e. Prime )
9 simprl 
 |-  ( ( ( G e. Grp /\ X e. Fin /\ P e. Prime ) /\ ( H e. ( SubGrp ` G ) /\ ( # ` H ) = ( P ^ ( P pCnt ( # ` X ) ) ) ) ) -> H e. ( SubGrp ` G ) )
10 simpl2 
 |-  ( ( ( G e. Grp /\ X e. Fin /\ P e. Prime ) /\ ( H e. ( SubGrp ` G ) /\ ( # ` H ) = ( P ^ ( P pCnt ( # ` X ) ) ) ) ) -> X e. Fin )
11 10 adantr 
 |-  ( ( ( ( G e. Grp /\ X e. Fin /\ P e. Prime ) /\ ( H e. ( SubGrp ` G ) /\ ( # ` H ) = ( P ^ ( P pCnt ( # ` X ) ) ) ) ) /\ ( k e. ( SubGrp ` G ) /\ ( H C_ k /\ P pGrp ( G |`s k ) ) ) ) -> X e. Fin )
12 simprl 
 |-  ( ( ( ( G e. Grp /\ X e. Fin /\ P e. Prime ) /\ ( H e. ( SubGrp ` G ) /\ ( # ` H ) = ( P ^ ( P pCnt ( # ` X ) ) ) ) ) /\ ( k e. ( SubGrp ` G ) /\ ( H C_ k /\ P pGrp ( G |`s k ) ) ) ) -> k e. ( SubGrp ` G ) )
13 1 subgss 
 |-  ( k e. ( SubGrp ` G ) -> k C_ X )
14 12 13 syl 
 |-  ( ( ( ( G e. Grp /\ X e. Fin /\ P e. Prime ) /\ ( H e. ( SubGrp ` G ) /\ ( # ` H ) = ( P ^ ( P pCnt ( # ` X ) ) ) ) ) /\ ( k e. ( SubGrp ` G ) /\ ( H C_ k /\ P pGrp ( G |`s k ) ) ) ) -> k C_ X )
15 11 14 ssfid 
 |-  ( ( ( ( G e. Grp /\ X e. Fin /\ P e. Prime ) /\ ( H e. ( SubGrp ` G ) /\ ( # ` H ) = ( P ^ ( P pCnt ( # ` X ) ) ) ) ) /\ ( k e. ( SubGrp ` G ) /\ ( H C_ k /\ P pGrp ( G |`s k ) ) ) ) -> k e. Fin )
16 simprrl 
 |-  ( ( ( ( G e. Grp /\ X e. Fin /\ P e. Prime ) /\ ( H e. ( SubGrp ` G ) /\ ( # ` H ) = ( P ^ ( P pCnt ( # ` X ) ) ) ) ) /\ ( k e. ( SubGrp ` G ) /\ ( H C_ k /\ P pGrp ( G |`s k ) ) ) ) -> H C_ k )
17 ssdomg 
 |-  ( k e. Fin -> ( H C_ k -> H ~<_ k ) )
18 15 16 17 sylc 
 |-  ( ( ( ( G e. Grp /\ X e. Fin /\ P e. Prime ) /\ ( H e. ( SubGrp ` G ) /\ ( # ` H ) = ( P ^ ( P pCnt ( # ` X ) ) ) ) ) /\ ( k e. ( SubGrp ` G ) /\ ( H C_ k /\ P pGrp ( G |`s k ) ) ) ) -> H ~<_ k )
19 simprrr 
 |-  ( ( ( ( G e. Grp /\ X e. Fin /\ P e. Prime ) /\ ( H e. ( SubGrp ` G ) /\ ( # ` H ) = ( P ^ ( P pCnt ( # ` X ) ) ) ) ) /\ ( k e. ( SubGrp ` G ) /\ ( H C_ k /\ P pGrp ( G |`s k ) ) ) ) -> P pGrp ( G |`s k ) )
20 eqid 
 |-  ( G |`s k ) = ( G |`s k )
21 20 subggrp 
 |-  ( k e. ( SubGrp ` G ) -> ( G |`s k ) e. Grp )
22 12 21 syl 
 |-  ( ( ( ( G e. Grp /\ X e. Fin /\ P e. Prime ) /\ ( H e. ( SubGrp ` G ) /\ ( # ` H ) = ( P ^ ( P pCnt ( # ` X ) ) ) ) ) /\ ( k e. ( SubGrp ` G ) /\ ( H C_ k /\ P pGrp ( G |`s k ) ) ) ) -> ( G |`s k ) e. Grp )
23 20 subgbas 
 |-  ( k e. ( SubGrp ` G ) -> k = ( Base ` ( G |`s k ) ) )
24 12 23 syl 
 |-  ( ( ( ( G e. Grp /\ X e. Fin /\ P e. Prime ) /\ ( H e. ( SubGrp ` G ) /\ ( # ` H ) = ( P ^ ( P pCnt ( # ` X ) ) ) ) ) /\ ( k e. ( SubGrp ` G ) /\ ( H C_ k /\ P pGrp ( G |`s k ) ) ) ) -> k = ( Base ` ( G |`s k ) ) )
25 24 15 eqeltrrd 
 |-  ( ( ( ( G e. Grp /\ X e. Fin /\ P e. Prime ) /\ ( H e. ( SubGrp ` G ) /\ ( # ` H ) = ( P ^ ( P pCnt ( # ` X ) ) ) ) ) /\ ( k e. ( SubGrp ` G ) /\ ( H C_ k /\ P pGrp ( G |`s k ) ) ) ) -> ( Base ` ( G |`s k ) ) e. Fin )
26 eqid 
 |-  ( Base ` ( G |`s k ) ) = ( Base ` ( G |`s k ) )
27 26 pgpfi 
 |-  ( ( ( G |`s k ) e. Grp /\ ( Base ` ( G |`s k ) ) e. Fin ) -> ( P pGrp ( G |`s k ) <-> ( P e. Prime /\ E. n e. NN0 ( # ` ( Base ` ( G |`s k ) ) ) = ( P ^ n ) ) ) )
28 22 25 27 syl2anc 
 |-  ( ( ( ( G e. Grp /\ X e. Fin /\ P e. Prime ) /\ ( H e. ( SubGrp ` G ) /\ ( # ` H ) = ( P ^ ( P pCnt ( # ` X ) ) ) ) ) /\ ( k e. ( SubGrp ` G ) /\ ( H C_ k /\ P pGrp ( G |`s k ) ) ) ) -> ( P pGrp ( G |`s k ) <-> ( P e. Prime /\ E. n e. NN0 ( # ` ( Base ` ( G |`s k ) ) ) = ( P ^ n ) ) ) )
29 19 28 mpbid 
 |-  ( ( ( ( G e. Grp /\ X e. Fin /\ P e. Prime ) /\ ( H e. ( SubGrp ` G ) /\ ( # ` H ) = ( P ^ ( P pCnt ( # ` X ) ) ) ) ) /\ ( k e. ( SubGrp ` G ) /\ ( H C_ k /\ P pGrp ( G |`s k ) ) ) ) -> ( P e. Prime /\ E. n e. NN0 ( # ` ( Base ` ( G |`s k ) ) ) = ( P ^ n ) ) )
30 29 simpld 
 |-  ( ( ( ( G e. Grp /\ X e. Fin /\ P e. Prime ) /\ ( H e. ( SubGrp ` G ) /\ ( # ` H ) = ( P ^ ( P pCnt ( # ` X ) ) ) ) ) /\ ( k e. ( SubGrp ` G ) /\ ( H C_ k /\ P pGrp ( G |`s k ) ) ) ) -> P e. Prime )
31 prmnn 
 |-  ( P e. Prime -> P e. NN )
32 30 31 syl 
 |-  ( ( ( ( G e. Grp /\ X e. Fin /\ P e. Prime ) /\ ( H e. ( SubGrp ` G ) /\ ( # ` H ) = ( P ^ ( P pCnt ( # ` X ) ) ) ) ) /\ ( k e. ( SubGrp ` G ) /\ ( H C_ k /\ P pGrp ( G |`s k ) ) ) ) -> P e. NN )
33 32 nnred 
 |-  ( ( ( ( G e. Grp /\ X e. Fin /\ P e. Prime ) /\ ( H e. ( SubGrp ` G ) /\ ( # ` H ) = ( P ^ ( P pCnt ( # ` X ) ) ) ) ) /\ ( k e. ( SubGrp ` G ) /\ ( H C_ k /\ P pGrp ( G |`s k ) ) ) ) -> P e. RR )
34 32 nnge1d 
 |-  ( ( ( ( G e. Grp /\ X e. Fin /\ P e. Prime ) /\ ( H e. ( SubGrp ` G ) /\ ( # ` H ) = ( P ^ ( P pCnt ( # ` X ) ) ) ) ) /\ ( k e. ( SubGrp ` G ) /\ ( H C_ k /\ P pGrp ( G |`s k ) ) ) ) -> 1 <_ P )
35 eqid 
 |-  ( 0g ` G ) = ( 0g ` G )
36 35 subg0cl 
 |-  ( k e. ( SubGrp ` G ) -> ( 0g ` G ) e. k )
37 12 36 syl 
 |-  ( ( ( ( G e. Grp /\ X e. Fin /\ P e. Prime ) /\ ( H e. ( SubGrp ` G ) /\ ( # ` H ) = ( P ^ ( P pCnt ( # ` X ) ) ) ) ) /\ ( k e. ( SubGrp ` G ) /\ ( H C_ k /\ P pGrp ( G |`s k ) ) ) ) -> ( 0g ` G ) e. k )
38 37 ne0d 
 |-  ( ( ( ( G e. Grp /\ X e. Fin /\ P e. Prime ) /\ ( H e. ( SubGrp ` G ) /\ ( # ` H ) = ( P ^ ( P pCnt ( # ` X ) ) ) ) ) /\ ( k e. ( SubGrp ` G ) /\ ( H C_ k /\ P pGrp ( G |`s k ) ) ) ) -> k =/= (/) )
39 hashnncl 
 |-  ( k e. Fin -> ( ( # ` k ) e. NN <-> k =/= (/) ) )
40 15 39 syl 
 |-  ( ( ( ( G e. Grp /\ X e. Fin /\ P e. Prime ) /\ ( H e. ( SubGrp ` G ) /\ ( # ` H ) = ( P ^ ( P pCnt ( # ` X ) ) ) ) ) /\ ( k e. ( SubGrp ` G ) /\ ( H C_ k /\ P pGrp ( G |`s k ) ) ) ) -> ( ( # ` k ) e. NN <-> k =/= (/) ) )
41 38 40 mpbird 
 |-  ( ( ( ( G e. Grp /\ X e. Fin /\ P e. Prime ) /\ ( H e. ( SubGrp ` G ) /\ ( # ` H ) = ( P ^ ( P pCnt ( # ` X ) ) ) ) ) /\ ( k e. ( SubGrp ` G ) /\ ( H C_ k /\ P pGrp ( G |`s k ) ) ) ) -> ( # ` k ) e. NN )
42 30 41 pccld 
 |-  ( ( ( ( G e. Grp /\ X e. Fin /\ P e. Prime ) /\ ( H e. ( SubGrp ` G ) /\ ( # ` H ) = ( P ^ ( P pCnt ( # ` X ) ) ) ) ) /\ ( k e. ( SubGrp ` G ) /\ ( H C_ k /\ P pGrp ( G |`s k ) ) ) ) -> ( P pCnt ( # ` k ) ) e. NN0 )
43 42 nn0zd 
 |-  ( ( ( ( G e. Grp /\ X e. Fin /\ P e. Prime ) /\ ( H e. ( SubGrp ` G ) /\ ( # ` H ) = ( P ^ ( P pCnt ( # ` X ) ) ) ) ) /\ ( k e. ( SubGrp ` G ) /\ ( H C_ k /\ P pGrp ( G |`s k ) ) ) ) -> ( P pCnt ( # ` k ) ) e. ZZ )
44 simpl1 
 |-  ( ( ( G e. Grp /\ X e. Fin /\ P e. Prime ) /\ ( H e. ( SubGrp ` G ) /\ ( # ` H ) = ( P ^ ( P pCnt ( # ` X ) ) ) ) ) -> G e. Grp )
45 1 grpbn0 
 |-  ( G e. Grp -> X =/= (/) )
46 44 45 syl 
 |-  ( ( ( G e. Grp /\ X e. Fin /\ P e. Prime ) /\ ( H e. ( SubGrp ` G ) /\ ( # ` H ) = ( P ^ ( P pCnt ( # ` X ) ) ) ) ) -> X =/= (/) )
47 hashnncl 
 |-  ( X e. Fin -> ( ( # ` X ) e. NN <-> X =/= (/) ) )
48 10 47 syl 
 |-  ( ( ( G e. Grp /\ X e. Fin /\ P e. Prime ) /\ ( H e. ( SubGrp ` G ) /\ ( # ` H ) = ( P ^ ( P pCnt ( # ` X ) ) ) ) ) -> ( ( # ` X ) e. NN <-> X =/= (/) ) )
49 46 48 mpbird 
 |-  ( ( ( G e. Grp /\ X e. Fin /\ P e. Prime ) /\ ( H e. ( SubGrp ` G ) /\ ( # ` H ) = ( P ^ ( P pCnt ( # ` X ) ) ) ) ) -> ( # ` X ) e. NN )
50 8 49 pccld 
 |-  ( ( ( G e. Grp /\ X e. Fin /\ P e. Prime ) /\ ( H e. ( SubGrp ` G ) /\ ( # ` H ) = ( P ^ ( P pCnt ( # ` X ) ) ) ) ) -> ( P pCnt ( # ` X ) ) e. NN0 )
51 50 adantr 
 |-  ( ( ( ( G e. Grp /\ X e. Fin /\ P e. Prime ) /\ ( H e. ( SubGrp ` G ) /\ ( # ` H ) = ( P ^ ( P pCnt ( # ` X ) ) ) ) ) /\ ( k e. ( SubGrp ` G ) /\ ( H C_ k /\ P pGrp ( G |`s k ) ) ) ) -> ( P pCnt ( # ` X ) ) e. NN0 )
52 51 nn0zd 
 |-  ( ( ( ( G e. Grp /\ X e. Fin /\ P e. Prime ) /\ ( H e. ( SubGrp ` G ) /\ ( # ` H ) = ( P ^ ( P pCnt ( # ` X ) ) ) ) ) /\ ( k e. ( SubGrp ` G ) /\ ( H C_ k /\ P pGrp ( G |`s k ) ) ) ) -> ( P pCnt ( # ` X ) ) e. ZZ )
53 oveq1 
 |-  ( p = P -> ( p pCnt ( # ` k ) ) = ( P pCnt ( # ` k ) ) )
54 oveq1 
 |-  ( p = P -> ( p pCnt ( # ` X ) ) = ( P pCnt ( # ` X ) ) )
55 53 54 breq12d 
 |-  ( p = P -> ( ( p pCnt ( # ` k ) ) <_ ( p pCnt ( # ` X ) ) <-> ( P pCnt ( # ` k ) ) <_ ( P pCnt ( # ` X ) ) ) )
56 1 lagsubg 
 |-  ( ( k e. ( SubGrp ` G ) /\ X e. Fin ) -> ( # ` k ) || ( # ` X ) )
57 12 11 56 syl2anc 
 |-  ( ( ( ( G e. Grp /\ X e. Fin /\ P e. Prime ) /\ ( H e. ( SubGrp ` G ) /\ ( # ` H ) = ( P ^ ( P pCnt ( # ` X ) ) ) ) ) /\ ( k e. ( SubGrp ` G ) /\ ( H C_ k /\ P pGrp ( G |`s k ) ) ) ) -> ( # ` k ) || ( # ` X ) )
58 41 nnzd 
 |-  ( ( ( ( G e. Grp /\ X e. Fin /\ P e. Prime ) /\ ( H e. ( SubGrp ` G ) /\ ( # ` H ) = ( P ^ ( P pCnt ( # ` X ) ) ) ) ) /\ ( k e. ( SubGrp ` G ) /\ ( H C_ k /\ P pGrp ( G |`s k ) ) ) ) -> ( # ` k ) e. ZZ )
59 49 adantr 
 |-  ( ( ( ( G e. Grp /\ X e. Fin /\ P e. Prime ) /\ ( H e. ( SubGrp ` G ) /\ ( # ` H ) = ( P ^ ( P pCnt ( # ` X ) ) ) ) ) /\ ( k e. ( SubGrp ` G ) /\ ( H C_ k /\ P pGrp ( G |`s k ) ) ) ) -> ( # ` X ) e. NN )
60 59 nnzd 
 |-  ( ( ( ( G e. Grp /\ X e. Fin /\ P e. Prime ) /\ ( H e. ( SubGrp ` G ) /\ ( # ` H ) = ( P ^ ( P pCnt ( # ` X ) ) ) ) ) /\ ( k e. ( SubGrp ` G ) /\ ( H C_ k /\ P pGrp ( G |`s k ) ) ) ) -> ( # ` X ) e. ZZ )
61 pc2dvds 
 |-  ( ( ( # ` k ) e. ZZ /\ ( # ` X ) e. ZZ ) -> ( ( # ` k ) || ( # ` X ) <-> A. p e. Prime ( p pCnt ( # ` k ) ) <_ ( p pCnt ( # ` X ) ) ) )
62 58 60 61 syl2anc 
 |-  ( ( ( ( G e. Grp /\ X e. Fin /\ P e. Prime ) /\ ( H e. ( SubGrp ` G ) /\ ( # ` H ) = ( P ^ ( P pCnt ( # ` X ) ) ) ) ) /\ ( k e. ( SubGrp ` G ) /\ ( H C_ k /\ P pGrp ( G |`s k ) ) ) ) -> ( ( # ` k ) || ( # ` X ) <-> A. p e. Prime ( p pCnt ( # ` k ) ) <_ ( p pCnt ( # ` X ) ) ) )
63 57 62 mpbid 
 |-  ( ( ( ( G e. Grp /\ X e. Fin /\ P e. Prime ) /\ ( H e. ( SubGrp ` G ) /\ ( # ` H ) = ( P ^ ( P pCnt ( # ` X ) ) ) ) ) /\ ( k e. ( SubGrp ` G ) /\ ( H C_ k /\ P pGrp ( G |`s k ) ) ) ) -> A. p e. Prime ( p pCnt ( # ` k ) ) <_ ( p pCnt ( # ` X ) ) )
64 55 63 30 rspcdva 
 |-  ( ( ( ( G e. Grp /\ X e. Fin /\ P e. Prime ) /\ ( H e. ( SubGrp ` G ) /\ ( # ` H ) = ( P ^ ( P pCnt ( # ` X ) ) ) ) ) /\ ( k e. ( SubGrp ` G ) /\ ( H C_ k /\ P pGrp ( G |`s k ) ) ) ) -> ( P pCnt ( # ` k ) ) <_ ( P pCnt ( # ` X ) ) )
65 eluz2 
 |-  ( ( P pCnt ( # ` X ) ) e. ( ZZ>= ` ( P pCnt ( # ` k ) ) ) <-> ( ( P pCnt ( # ` k ) ) e. ZZ /\ ( P pCnt ( # ` X ) ) e. ZZ /\ ( P pCnt ( # ` k ) ) <_ ( P pCnt ( # ` X ) ) ) )
66 43 52 64 65 syl3anbrc 
 |-  ( ( ( ( G e. Grp /\ X e. Fin /\ P e. Prime ) /\ ( H e. ( SubGrp ` G ) /\ ( # ` H ) = ( P ^ ( P pCnt ( # ` X ) ) ) ) ) /\ ( k e. ( SubGrp ` G ) /\ ( H C_ k /\ P pGrp ( G |`s k ) ) ) ) -> ( P pCnt ( # ` X ) ) e. ( ZZ>= ` ( P pCnt ( # ` k ) ) ) )
67 33 34 66 leexp2ad 
 |-  ( ( ( ( G e. Grp /\ X e. Fin /\ P e. Prime ) /\ ( H e. ( SubGrp ` G ) /\ ( # ` H ) = ( P ^ ( P pCnt ( # ` X ) ) ) ) ) /\ ( k e. ( SubGrp ` G ) /\ ( H C_ k /\ P pGrp ( G |`s k ) ) ) ) -> ( P ^ ( P pCnt ( # ` k ) ) ) <_ ( P ^ ( P pCnt ( # ` X ) ) ) )
68 29 simprd 
 |-  ( ( ( ( G e. Grp /\ X e. Fin /\ P e. Prime ) /\ ( H e. ( SubGrp ` G ) /\ ( # ` H ) = ( P ^ ( P pCnt ( # ` X ) ) ) ) ) /\ ( k e. ( SubGrp ` G ) /\ ( H C_ k /\ P pGrp ( G |`s k ) ) ) ) -> E. n e. NN0 ( # ` ( Base ` ( G |`s k ) ) ) = ( P ^ n ) )
69 24 fveqeq2d 
 |-  ( ( ( ( G e. Grp /\ X e. Fin /\ P e. Prime ) /\ ( H e. ( SubGrp ` G ) /\ ( # ` H ) = ( P ^ ( P pCnt ( # ` X ) ) ) ) ) /\ ( k e. ( SubGrp ` G ) /\ ( H C_ k /\ P pGrp ( G |`s k ) ) ) ) -> ( ( # ` k ) = ( P ^ n ) <-> ( # ` ( Base ` ( G |`s k ) ) ) = ( P ^ n ) ) )
70 69 rexbidv 
 |-  ( ( ( ( G e. Grp /\ X e. Fin /\ P e. Prime ) /\ ( H e. ( SubGrp ` G ) /\ ( # ` H ) = ( P ^ ( P pCnt ( # ` X ) ) ) ) ) /\ ( k e. ( SubGrp ` G ) /\ ( H C_ k /\ P pGrp ( G |`s k ) ) ) ) -> ( E. n e. NN0 ( # ` k ) = ( P ^ n ) <-> E. n e. NN0 ( # ` ( Base ` ( G |`s k ) ) ) = ( P ^ n ) ) )
71 68 70 mpbird 
 |-  ( ( ( ( G e. Grp /\ X e. Fin /\ P e. Prime ) /\ ( H e. ( SubGrp ` G ) /\ ( # ` H ) = ( P ^ ( P pCnt ( # ` X ) ) ) ) ) /\ ( k e. ( SubGrp ` G ) /\ ( H C_ k /\ P pGrp ( G |`s k ) ) ) ) -> E. n e. NN0 ( # ` k ) = ( P ^ n ) )
72 pcprmpw 
 |-  ( ( P e. Prime /\ ( # ` k ) e. NN ) -> ( E. n e. NN0 ( # ` k ) = ( P ^ n ) <-> ( # ` k ) = ( P ^ ( P pCnt ( # ` k ) ) ) ) )
73 30 41 72 syl2anc 
 |-  ( ( ( ( G e. Grp /\ X e. Fin /\ P e. Prime ) /\ ( H e. ( SubGrp ` G ) /\ ( # ` H ) = ( P ^ ( P pCnt ( # ` X ) ) ) ) ) /\ ( k e. ( SubGrp ` G ) /\ ( H C_ k /\ P pGrp ( G |`s k ) ) ) ) -> ( E. n e. NN0 ( # ` k ) = ( P ^ n ) <-> ( # ` k ) = ( P ^ ( P pCnt ( # ` k ) ) ) ) )
74 71 73 mpbid 
 |-  ( ( ( ( G e. Grp /\ X e. Fin /\ P e. Prime ) /\ ( H e. ( SubGrp ` G ) /\ ( # ` H ) = ( P ^ ( P pCnt ( # ` X ) ) ) ) ) /\ ( k e. ( SubGrp ` G ) /\ ( H C_ k /\ P pGrp ( G |`s k ) ) ) ) -> ( # ` k ) = ( P ^ ( P pCnt ( # ` k ) ) ) )
75 simplrr 
 |-  ( ( ( ( G e. Grp /\ X e. Fin /\ P e. Prime ) /\ ( H e. ( SubGrp ` G ) /\ ( # ` H ) = ( P ^ ( P pCnt ( # ` X ) ) ) ) ) /\ ( k e. ( SubGrp ` G ) /\ ( H C_ k /\ P pGrp ( G |`s k ) ) ) ) -> ( # ` H ) = ( P ^ ( P pCnt ( # ` X ) ) ) )
76 67 74 75 3brtr4d 
 |-  ( ( ( ( G e. Grp /\ X e. Fin /\ P e. Prime ) /\ ( H e. ( SubGrp ` G ) /\ ( # ` H ) = ( P ^ ( P pCnt ( # ` X ) ) ) ) ) /\ ( k e. ( SubGrp ` G ) /\ ( H C_ k /\ P pGrp ( G |`s k ) ) ) ) -> ( # ` k ) <_ ( # ` H ) )
77 1 subgss 
 |-  ( H e. ( SubGrp ` G ) -> H C_ X )
78 77 ad2antrl 
 |-  ( ( ( G e. Grp /\ X e. Fin /\ P e. Prime ) /\ ( H e. ( SubGrp ` G ) /\ ( # ` H ) = ( P ^ ( P pCnt ( # ` X ) ) ) ) ) -> H C_ X )
79 10 78 ssfid 
 |-  ( ( ( G e. Grp /\ X e. Fin /\ P e. Prime ) /\ ( H e. ( SubGrp ` G ) /\ ( # ` H ) = ( P ^ ( P pCnt ( # ` X ) ) ) ) ) -> H e. Fin )
80 79 adantr 
 |-  ( ( ( ( G e. Grp /\ X e. Fin /\ P e. Prime ) /\ ( H e. ( SubGrp ` G ) /\ ( # ` H ) = ( P ^ ( P pCnt ( # ` X ) ) ) ) ) /\ ( k e. ( SubGrp ` G ) /\ ( H C_ k /\ P pGrp ( G |`s k ) ) ) ) -> H e. Fin )
81 hashdom 
 |-  ( ( k e. Fin /\ H e. Fin ) -> ( ( # ` k ) <_ ( # ` H ) <-> k ~<_ H ) )
82 15 80 81 syl2anc 
 |-  ( ( ( ( G e. Grp /\ X e. Fin /\ P e. Prime ) /\ ( H e. ( SubGrp ` G ) /\ ( # ` H ) = ( P ^ ( P pCnt ( # ` X ) ) ) ) ) /\ ( k e. ( SubGrp ` G ) /\ ( H C_ k /\ P pGrp ( G |`s k ) ) ) ) -> ( ( # ` k ) <_ ( # ` H ) <-> k ~<_ H ) )
83 76 82 mpbid 
 |-  ( ( ( ( G e. Grp /\ X e. Fin /\ P e. Prime ) /\ ( H e. ( SubGrp ` G ) /\ ( # ` H ) = ( P ^ ( P pCnt ( # ` X ) ) ) ) ) /\ ( k e. ( SubGrp ` G ) /\ ( H C_ k /\ P pGrp ( G |`s k ) ) ) ) -> k ~<_ H )
84 sbth 
 |-  ( ( H ~<_ k /\ k ~<_ H ) -> H ~~ k )
85 18 83 84 syl2anc 
 |-  ( ( ( ( G e. Grp /\ X e. Fin /\ P e. Prime ) /\ ( H e. ( SubGrp ` G ) /\ ( # ` H ) = ( P ^ ( P pCnt ( # ` X ) ) ) ) ) /\ ( k e. ( SubGrp ` G ) /\ ( H C_ k /\ P pGrp ( G |`s k ) ) ) ) -> H ~~ k )
86 fisseneq 
 |-  ( ( k e. Fin /\ H C_ k /\ H ~~ k ) -> H = k )
87 15 16 85 86 syl3anc 
 |-  ( ( ( ( G e. Grp /\ X e. Fin /\ P e. Prime ) /\ ( H e. ( SubGrp ` G ) /\ ( # ` H ) = ( P ^ ( P pCnt ( # ` X ) ) ) ) ) /\ ( k e. ( SubGrp ` G ) /\ ( H C_ k /\ P pGrp ( G |`s k ) ) ) ) -> H = k )
88 87 expr 
 |-  ( ( ( ( G e. Grp /\ X e. Fin /\ P e. Prime ) /\ ( H e. ( SubGrp ` G ) /\ ( # ` H ) = ( P ^ ( P pCnt ( # ` X ) ) ) ) ) /\ k e. ( SubGrp ` G ) ) -> ( ( H C_ k /\ P pGrp ( G |`s k ) ) -> H = k ) )
89 eqid 
 |-  ( G |`s H ) = ( G |`s H )
90 89 subgbas 
 |-  ( H e. ( SubGrp ` G ) -> H = ( Base ` ( G |`s H ) ) )
91 90 ad2antrl 
 |-  ( ( ( G e. Grp /\ X e. Fin /\ P e. Prime ) /\ ( H e. ( SubGrp ` G ) /\ ( # ` H ) = ( P ^ ( P pCnt ( # ` X ) ) ) ) ) -> H = ( Base ` ( G |`s H ) ) )
92 91 fveq2d 
 |-  ( ( ( G e. Grp /\ X e. Fin /\ P e. Prime ) /\ ( H e. ( SubGrp ` G ) /\ ( # ` H ) = ( P ^ ( P pCnt ( # ` X ) ) ) ) ) -> ( # ` H ) = ( # ` ( Base ` ( G |`s H ) ) ) )
93 simprr 
 |-  ( ( ( G e. Grp /\ X e. Fin /\ P e. Prime ) /\ ( H e. ( SubGrp ` G ) /\ ( # ` H ) = ( P ^ ( P pCnt ( # ` X ) ) ) ) ) -> ( # ` H ) = ( P ^ ( P pCnt ( # ` X ) ) ) )
94 92 93 eqtr3d 
 |-  ( ( ( G e. Grp /\ X e. Fin /\ P e. Prime ) /\ ( H e. ( SubGrp ` G ) /\ ( # ` H ) = ( P ^ ( P pCnt ( # ` X ) ) ) ) ) -> ( # ` ( Base ` ( G |`s H ) ) ) = ( P ^ ( P pCnt ( # ` X ) ) ) )
95 oveq2 
 |-  ( n = ( P pCnt ( # ` X ) ) -> ( P ^ n ) = ( P ^ ( P pCnt ( # ` X ) ) ) )
96 95 rspceeqv 
 |-  ( ( ( P pCnt ( # ` X ) ) e. NN0 /\ ( # ` ( Base ` ( G |`s H ) ) ) = ( P ^ ( P pCnt ( # ` X ) ) ) ) -> E. n e. NN0 ( # ` ( Base ` ( G |`s H ) ) ) = ( P ^ n ) )
97 50 94 96 syl2anc 
 |-  ( ( ( G e. Grp /\ X e. Fin /\ P e. Prime ) /\ ( H e. ( SubGrp ` G ) /\ ( # ` H ) = ( P ^ ( P pCnt ( # ` X ) ) ) ) ) -> E. n e. NN0 ( # ` ( Base ` ( G |`s H ) ) ) = ( P ^ n ) )
98 89 subggrp 
 |-  ( H e. ( SubGrp ` G ) -> ( G |`s H ) e. Grp )
99 98 ad2antrl 
 |-  ( ( ( G e. Grp /\ X e. Fin /\ P e. Prime ) /\ ( H e. ( SubGrp ` G ) /\ ( # ` H ) = ( P ^ ( P pCnt ( # ` X ) ) ) ) ) -> ( G |`s H ) e. Grp )
100 91 79 eqeltrrd 
 |-  ( ( ( G e. Grp /\ X e. Fin /\ P e. Prime ) /\ ( H e. ( SubGrp ` G ) /\ ( # ` H ) = ( P ^ ( P pCnt ( # ` X ) ) ) ) ) -> ( Base ` ( G |`s H ) ) e. Fin )
101 eqid 
 |-  ( Base ` ( G |`s H ) ) = ( Base ` ( G |`s H ) )
102 101 pgpfi 
 |-  ( ( ( G |`s H ) e. Grp /\ ( Base ` ( G |`s H ) ) e. Fin ) -> ( P pGrp ( G |`s H ) <-> ( P e. Prime /\ E. n e. NN0 ( # ` ( Base ` ( G |`s H ) ) ) = ( P ^ n ) ) ) )
103 99 100 102 syl2anc 
 |-  ( ( ( G e. Grp /\ X e. Fin /\ P e. Prime ) /\ ( H e. ( SubGrp ` G ) /\ ( # ` H ) = ( P ^ ( P pCnt ( # ` X ) ) ) ) ) -> ( P pGrp ( G |`s H ) <-> ( P e. Prime /\ E. n e. NN0 ( # ` ( Base ` ( G |`s H ) ) ) = ( P ^ n ) ) ) )
104 8 97 103 mpbir2and 
 |-  ( ( ( G e. Grp /\ X e. Fin /\ P e. Prime ) /\ ( H e. ( SubGrp ` G ) /\ ( # ` H ) = ( P ^ ( P pCnt ( # ` X ) ) ) ) ) -> P pGrp ( G |`s H ) )
105 104 adantr 
 |-  ( ( ( ( G e. Grp /\ X e. Fin /\ P e. Prime ) /\ ( H e. ( SubGrp ` G ) /\ ( # ` H ) = ( P ^ ( P pCnt ( # ` X ) ) ) ) ) /\ k e. ( SubGrp ` G ) ) -> P pGrp ( G |`s H ) )
106 oveq2 
 |-  ( H = k -> ( G |`s H ) = ( G |`s k ) )
107 106 breq2d 
 |-  ( H = k -> ( P pGrp ( G |`s H ) <-> P pGrp ( G |`s k ) ) )
108 eqimss 
 |-  ( H = k -> H C_ k )
109 108 biantrurd 
 |-  ( H = k -> ( P pGrp ( G |`s k ) <-> ( H C_ k /\ P pGrp ( G |`s k ) ) ) )
110 107 109 bitrd 
 |-  ( H = k -> ( P pGrp ( G |`s H ) <-> ( H C_ k /\ P pGrp ( G |`s k ) ) ) )
111 105 110 syl5ibcom 
 |-  ( ( ( ( G e. Grp /\ X e. Fin /\ P e. Prime ) /\ ( H e. ( SubGrp ` G ) /\ ( # ` H ) = ( P ^ ( P pCnt ( # ` X ) ) ) ) ) /\ k e. ( SubGrp ` G ) ) -> ( H = k -> ( H C_ k /\ P pGrp ( G |`s k ) ) ) )
112 88 111 impbid 
 |-  ( ( ( ( G e. Grp /\ X e. Fin /\ P e. Prime ) /\ ( H e. ( SubGrp ` G ) /\ ( # ` H ) = ( P ^ ( P pCnt ( # ` X ) ) ) ) ) /\ k e. ( SubGrp ` G ) ) -> ( ( H C_ k /\ P pGrp ( G |`s k ) ) <-> H = k ) )
113 112 ralrimiva 
 |-  ( ( ( G e. Grp /\ X e. Fin /\ P e. Prime ) /\ ( H e. ( SubGrp ` G ) /\ ( # ` H ) = ( P ^ ( P pCnt ( # ` X ) ) ) ) ) -> A. k e. ( SubGrp ` G ) ( ( H C_ k /\ P pGrp ( G |`s k ) ) <-> H = k ) )
114 isslw 
 |-  ( H e. ( P pSyl G ) <-> ( P e. Prime /\ H e. ( SubGrp ` G ) /\ A. k e. ( SubGrp ` G ) ( ( H C_ k /\ P pGrp ( G |`s k ) ) <-> H = k ) ) )
115 8 9 113 114 syl3anbrc 
 |-  ( ( ( G e. Grp /\ X e. Fin /\ P e. Prime ) /\ ( H e. ( SubGrp ` G ) /\ ( # ` H ) = ( P ^ ( P pCnt ( # ` X ) ) ) ) ) -> H e. ( P pSyl G ) )
116 7 115 impbida 
 |-  ( ( G e. Grp /\ X e. Fin /\ P e. Prime ) -> ( H e. ( P pSyl G ) <-> ( H e. ( SubGrp ` G ) /\ ( # ` H ) = ( P ^ ( P pCnt ( # ` X ) ) ) ) ) )