Metamath Proof Explorer

Theorem sylow1

Description: Sylow's first theorem. If P ^ N is a prime power that divides the cardinality of G , then G has a supgroup with size P ^ N . This is part of Metamath 100 proof #72. (Contributed by Mario Carneiro, 16-Jan-2015)

Ref Expression
Hypotheses sylow1.x 
|- X = ( Base ` G )
sylow1.g 
|- ( ph -> G e. Grp )
sylow1.f 
|- ( ph -> X e. Fin )
sylow1.p 
|- ( ph -> P e. Prime )
sylow1.n 
|- ( ph -> N e. NN0 )
sylow1.d 
|- ( ph -> ( P ^ N ) || ( # ` X ) )
Assertion sylow1 
|- ( ph -> E. g e. ( SubGrp ` G ) ( # ` g ) = ( P ^ N ) )

Proof

Step Hyp Ref Expression
1 sylow1.x 
 |-  X = ( Base ` G )
2 sylow1.g 
 |-  ( ph -> G e. Grp )
3 sylow1.f 
 |-  ( ph -> X e. Fin )
4 sylow1.p 
 |-  ( ph -> P e. Prime )
5 sylow1.n 
 |-  ( ph -> N e. NN0 )
6 sylow1.d 
 |-  ( ph -> ( P ^ N ) || ( # ` X ) )
7 eqid 
 |-  ( +g ` G ) = ( +g ` G )
8 eqid 
 |-  { s e. ~P X | ( # ` s ) = ( P ^ N ) } = { s e. ~P X | ( # ` s ) = ( P ^ N ) }
9 oveq2 
 |-  ( s = z -> ( u ( +g ` G ) s ) = ( u ( +g ` G ) z ) )
10 9 cbvmptv 
 |-  ( s e. v |-> ( u ( +g ` G ) s ) ) = ( z e. v |-> ( u ( +g ` G ) z ) )
11 oveq1 
 |-  ( u = x -> ( u ( +g ` G ) z ) = ( x ( +g ` G ) z ) )
12 11 mpteq2dv 
 |-  ( u = x -> ( z e. v |-> ( u ( +g ` G ) z ) ) = ( z e. v |-> ( x ( +g ` G ) z ) ) )
13 10 12 eqtrid 
 |-  ( u = x -> ( s e. v |-> ( u ( +g ` G ) s ) ) = ( z e. v |-> ( x ( +g ` G ) z ) ) )
14 13 rneqd 
 |-  ( u = x -> ran ( s e. v |-> ( u ( +g ` G ) s ) ) = ran ( z e. v |-> ( x ( +g ` G ) z ) ) )
15 mpteq1 
 |-  ( v = y -> ( z e. v |-> ( x ( +g ` G ) z ) ) = ( z e. y |-> ( x ( +g ` G ) z ) ) )
16 15 rneqd 
 |-  ( v = y -> ran ( z e. v |-> ( x ( +g ` G ) z ) ) = ran ( z e. y |-> ( x ( +g ` G ) z ) ) )
17 14 16 cbvmpov 
 |-  ( u e. X , v e. { s e. ~P X | ( # ` s ) = ( P ^ N ) } |-> ran ( s e. v |-> ( u ( +g ` G ) s ) ) ) = ( x e. X , y e. { s e. ~P X | ( # ` s ) = ( P ^ N ) } |-> ran ( z e. y |-> ( x ( +g ` G ) z ) ) )
18 preq12 
 |-  ( ( a = x /\ b = y ) -> { a , b } = { x , y } )
19 18 sseq1d 
 |-  ( ( a = x /\ b = y ) -> ( { a , b } C_ { s e. ~P X | ( # ` s ) = ( P ^ N ) } <-> { x , y } C_ { s e. ~P X | ( # ` s ) = ( P ^ N ) } ) )
20 oveq2 
 |-  ( a = x -> ( k ( u e. X , v e. { s e. ~P X | ( # ` s ) = ( P ^ N ) } |-> ran ( s e. v |-> ( u ( +g ` G ) s ) ) ) a ) = ( k ( u e. X , v e. { s e. ~P X | ( # ` s ) = ( P ^ N ) } |-> ran ( s e. v |-> ( u ( +g ` G ) s ) ) ) x ) )
21 id 
 |-  ( b = y -> b = y )
22 20 21 eqeqan12d 
 |-  ( ( a = x /\ b = y ) -> ( ( k ( u e. X , v e. { s e. ~P X | ( # ` s ) = ( P ^ N ) } |-> ran ( s e. v |-> ( u ( +g ` G ) s ) ) ) a ) = b <-> ( k ( u e. X , v e. { s e. ~P X | ( # ` s ) = ( P ^ N ) } |-> ran ( s e. v |-> ( u ( +g ` G ) s ) ) ) x ) = y ) )
23 22 rexbidv 
 |-  ( ( a = x /\ b = y ) -> ( E. k e. X ( k ( u e. X , v e. { s e. ~P X | ( # ` s ) = ( P ^ N ) } |-> ran ( s e. v |-> ( u ( +g ` G ) s ) ) ) a ) = b <-> E. k e. X ( k ( u e. X , v e. { s e. ~P X | ( # ` s ) = ( P ^ N ) } |-> ran ( s e. v |-> ( u ( +g ` G ) s ) ) ) x ) = y ) )
24 19 23 anbi12d 
 |-  ( ( a = x /\ b = y ) -> ( ( { a , b } C_ { s e. ~P X | ( # ` s ) = ( P ^ N ) } /\ E. k e. X ( k ( u e. X , v e. { s e. ~P X | ( # ` s ) = ( P ^ N ) } |-> ran ( s e. v |-> ( u ( +g ` G ) s ) ) ) a ) = b ) <-> ( { x , y } C_ { s e. ~P X | ( # ` s ) = ( P ^ N ) } /\ E. k e. X ( k ( u e. X , v e. { s e. ~P X | ( # ` s ) = ( P ^ N ) } |-> ran ( s e. v |-> ( u ( +g ` G ) s ) ) ) x ) = y ) ) )
25 24 cbvopabv 
 |-  { <. a , b >. | ( { a , b } C_ { s e. ~P X | ( # ` s ) = ( P ^ N ) } /\ E. k e. X ( k ( u e. X , v e. { s e. ~P X | ( # ` s ) = ( P ^ N ) } |-> ran ( s e. v |-> ( u ( +g ` G ) s ) ) ) a ) = b ) } = { <. x , y >. | ( { x , y } C_ { s e. ~P X | ( # ` s ) = ( P ^ N ) } /\ E. k e. X ( k ( u e. X , v e. { s e. ~P X | ( # ` s ) = ( P ^ N ) } |-> ran ( s e. v |-> ( u ( +g ` G ) s ) ) ) x ) = y ) }
26 1 2 3 4 5 6 7 8 17 25 sylow1lem3 
 |-  ( ph -> E. h e. { s e. ~P X | ( # ` s ) = ( P ^ N ) } ( P pCnt ( # ` [ h ] { <. a , b >. | ( { a , b } C_ { s e. ~P X | ( # ` s ) = ( P ^ N ) } /\ E. k e. X ( k ( u e. X , v e. { s e. ~P X | ( # ` s ) = ( P ^ N ) } |-> ran ( s e. v |-> ( u ( +g ` G ) s ) ) ) a ) = b ) } ) ) <_ ( ( P pCnt ( # ` X ) ) - N ) )
27 2 adantr 
 |-  ( ( ph /\ ( h e. { s e. ~P X | ( # ` s ) = ( P ^ N ) } /\ ( P pCnt ( # ` [ h ] { <. a , b >. | ( { a , b } C_ { s e. ~P X | ( # ` s ) = ( P ^ N ) } /\ E. k e. X ( k ( u e. X , v e. { s e. ~P X | ( # ` s ) = ( P ^ N ) } |-> ran ( s e. v |-> ( u ( +g ` G ) s ) ) ) a ) = b ) } ) ) <_ ( ( P pCnt ( # ` X ) ) - N ) ) ) -> G e. Grp )
28 3 adantr 
 |-  ( ( ph /\ ( h e. { s e. ~P X | ( # ` s ) = ( P ^ N ) } /\ ( P pCnt ( # ` [ h ] { <. a , b >. | ( { a , b } C_ { s e. ~P X | ( # ` s ) = ( P ^ N ) } /\ E. k e. X ( k ( u e. X , v e. { s e. ~P X | ( # ` s ) = ( P ^ N ) } |-> ran ( s e. v |-> ( u ( +g ` G ) s ) ) ) a ) = b ) } ) ) <_ ( ( P pCnt ( # ` X ) ) - N ) ) ) -> X e. Fin )
29 4 adantr 
 |-  ( ( ph /\ ( h e. { s e. ~P X | ( # ` s ) = ( P ^ N ) } /\ ( P pCnt ( # ` [ h ] { <. a , b >. | ( { a , b } C_ { s e. ~P X | ( # ` s ) = ( P ^ N ) } /\ E. k e. X ( k ( u e. X , v e. { s e. ~P X | ( # ` s ) = ( P ^ N ) } |-> ran ( s e. v |-> ( u ( +g ` G ) s ) ) ) a ) = b ) } ) ) <_ ( ( P pCnt ( # ` X ) ) - N ) ) ) -> P e. Prime )
30 5 adantr 
 |-  ( ( ph /\ ( h e. { s e. ~P X | ( # ` s ) = ( P ^ N ) } /\ ( P pCnt ( # ` [ h ] { <. a , b >. | ( { a , b } C_ { s e. ~P X | ( # ` s ) = ( P ^ N ) } /\ E. k e. X ( k ( u e. X , v e. { s e. ~P X | ( # ` s ) = ( P ^ N ) } |-> ran ( s e. v |-> ( u ( +g ` G ) s ) ) ) a ) = b ) } ) ) <_ ( ( P pCnt ( # ` X ) ) - N ) ) ) -> N e. NN0 )
31 6 adantr 
 |-  ( ( ph /\ ( h e. { s e. ~P X | ( # ` s ) = ( P ^ N ) } /\ ( P pCnt ( # ` [ h ] { <. a , b >. | ( { a , b } C_ { s e. ~P X | ( # ` s ) = ( P ^ N ) } /\ E. k e. X ( k ( u e. X , v e. { s e. ~P X | ( # ` s ) = ( P ^ N ) } |-> ran ( s e. v |-> ( u ( +g ` G ) s ) ) ) a ) = b ) } ) ) <_ ( ( P pCnt ( # ` X ) ) - N ) ) ) -> ( P ^ N ) || ( # ` X ) )
32 simprl 
 |-  ( ( ph /\ ( h e. { s e. ~P X | ( # ` s ) = ( P ^ N ) } /\ ( P pCnt ( # ` [ h ] { <. a , b >. | ( { a , b } C_ { s e. ~P X | ( # ` s ) = ( P ^ N ) } /\ E. k e. X ( k ( u e. X , v e. { s e. ~P X | ( # ` s ) = ( P ^ N ) } |-> ran ( s e. v |-> ( u ( +g ` G ) s ) ) ) a ) = b ) } ) ) <_ ( ( P pCnt ( # ` X ) ) - N ) ) ) -> h e. { s e. ~P X | ( # ` s ) = ( P ^ N ) } )
33 eqid 
 |-  { t e. X | ( t ( u e. X , v e. { s e. ~P X | ( # ` s ) = ( P ^ N ) } |-> ran ( s e. v |-> ( u ( +g ` G ) s ) ) ) h ) = h } = { t e. X | ( t ( u e. X , v e. { s e. ~P X | ( # ` s ) = ( P ^ N ) } |-> ran ( s e. v |-> ( u ( +g ` G ) s ) ) ) h ) = h }
34 simprr 
 |-  ( ( ph /\ ( h e. { s e. ~P X | ( # ` s ) = ( P ^ N ) } /\ ( P pCnt ( # ` [ h ] { <. a , b >. | ( { a , b } C_ { s e. ~P X | ( # ` s ) = ( P ^ N ) } /\ E. k e. X ( k ( u e. X , v e. { s e. ~P X | ( # ` s ) = ( P ^ N ) } |-> ran ( s e. v |-> ( u ( +g ` G ) s ) ) ) a ) = b ) } ) ) <_ ( ( P pCnt ( # ` X ) ) - N ) ) ) -> ( P pCnt ( # ` [ h ] { <. a , b >. | ( { a , b } C_ { s e. ~P X | ( # ` s ) = ( P ^ N ) } /\ E. k e. X ( k ( u e. X , v e. { s e. ~P X | ( # ` s ) = ( P ^ N ) } |-> ran ( s e. v |-> ( u ( +g ` G ) s ) ) ) a ) = b ) } ) ) <_ ( ( P pCnt ( # ` X ) ) - N ) )
35 1 27 28 29 30 31 7 8 17 25 32 33 34 sylow1lem5 
 |-  ( ( ph /\ ( h e. { s e. ~P X | ( # ` s ) = ( P ^ N ) } /\ ( P pCnt ( # ` [ h ] { <. a , b >. | ( { a , b } C_ { s e. ~P X | ( # ` s ) = ( P ^ N ) } /\ E. k e. X ( k ( u e. X , v e. { s e. ~P X | ( # ` s ) = ( P ^ N ) } |-> ran ( s e. v |-> ( u ( +g ` G ) s ) ) ) a ) = b ) } ) ) <_ ( ( P pCnt ( # ` X ) ) - N ) ) ) -> E. g e. ( SubGrp ` G ) ( # ` g ) = ( P ^ N ) )
36 26 35 rexlimddv 
 |-  ( ph -> E. g e. ( SubGrp ` G ) ( # ` g ) = ( P ^ N ) )