Metamath Proof Explorer

Theorem sylow2

Description: Sylow's second theorem. See also sylow2b for the "hard" part of the proof. Any two Sylow P -subgroups are conjugate to one another, and hence the same size, namely P ^ ( P pCnt | X | ) (see fislw ). This is part of Metamath 100 proof #72. (Contributed by Mario Carneiro, 18-Jan-2015)

Ref Expression
Hypotheses sylow2.x 
|- X = ( Base ` G )
sylow2.f 
|- ( ph -> X e. Fin )
sylow2.h 
|- ( ph -> H e. ( P pSyl G ) )
sylow2.k 
|- ( ph -> K e. ( P pSyl G ) )
sylow2.a 
|- .+ = ( +g ` G )
sylow2.d 
|- .- = ( -g ` G )
Assertion sylow2 
|- ( ph -> E. g e. X H = ran ( x e. K |-> ( ( g .+ x ) .- g ) ) )

Proof

Step Hyp Ref Expression
1 sylow2.x 
 |-  X = ( Base ` G )
2 sylow2.f 
 |-  ( ph -> X e. Fin )
3 sylow2.h 
 |-  ( ph -> H e. ( P pSyl G ) )
4 sylow2.k 
 |-  ( ph -> K e. ( P pSyl G ) )
5 sylow2.a 
 |-  .+ = ( +g ` G )
6 sylow2.d 
 |-  .- = ( -g ` G )
7 2 adantr 
 |-  ( ( ph /\ ( g e. X /\ H C_ ran ( x e. K |-> ( ( g .+ x ) .- g ) ) ) ) -> X e. Fin )
8 slwsubg 
 |-  ( K e. ( P pSyl G ) -> K e. ( SubGrp ` G ) )
9 4 8 syl 
 |-  ( ph -> K e. ( SubGrp ` G ) )
10 simprl 
 |-  ( ( ph /\ ( g e. X /\ H C_ ran ( x e. K |-> ( ( g .+ x ) .- g ) ) ) ) -> g e. X )
11 eqid 
 |-  ( x e. K |-> ( ( g .+ x ) .- g ) ) = ( x e. K |-> ( ( g .+ x ) .- g ) )
12 1 5 6 11 conjsubg 
 |-  ( ( K e. ( SubGrp ` G ) /\ g e. X ) -> ran ( x e. K |-> ( ( g .+ x ) .- g ) ) e. ( SubGrp ` G ) )
13 9 10 12 syl2an2r 
 |-  ( ( ph /\ ( g e. X /\ H C_ ran ( x e. K |-> ( ( g .+ x ) .- g ) ) ) ) -> ran ( x e. K |-> ( ( g .+ x ) .- g ) ) e. ( SubGrp ` G ) )
14 1 subgss 
 |-  ( ran ( x e. K |-> ( ( g .+ x ) .- g ) ) e. ( SubGrp ` G ) -> ran ( x e. K |-> ( ( g .+ x ) .- g ) ) C_ X )
15 13 14 syl 
 |-  ( ( ph /\ ( g e. X /\ H C_ ran ( x e. K |-> ( ( g .+ x ) .- g ) ) ) ) -> ran ( x e. K |-> ( ( g .+ x ) .- g ) ) C_ X )
16 7 15 ssfid 
 |-  ( ( ph /\ ( g e. X /\ H C_ ran ( x e. K |-> ( ( g .+ x ) .- g ) ) ) ) -> ran ( x e. K |-> ( ( g .+ x ) .- g ) ) e. Fin )
17 simprr 
 |-  ( ( ph /\ ( g e. X /\ H C_ ran ( x e. K |-> ( ( g .+ x ) .- g ) ) ) ) -> H C_ ran ( x e. K |-> ( ( g .+ x ) .- g ) ) )
18 1 2 3 slwhash 
 |-  ( ph -> ( # ` H ) = ( P ^ ( P pCnt ( # ` X ) ) ) )
19 1 2 4 slwhash 
 |-  ( ph -> ( # ` K ) = ( P ^ ( P pCnt ( # ` X ) ) ) )
20 18 19 eqtr4d 
 |-  ( ph -> ( # ` H ) = ( # ` K ) )
21 slwsubg 
 |-  ( H e. ( P pSyl G ) -> H e. ( SubGrp ` G ) )
22 3 21 syl 
 |-  ( ph -> H e. ( SubGrp ` G ) )
23 1 subgss 
 |-  ( H e. ( SubGrp ` G ) -> H C_ X )
24 22 23 syl 
 |-  ( ph -> H C_ X )
25 2 24 ssfid 
 |-  ( ph -> H e. Fin )
26 1 subgss 
 |-  ( K e. ( SubGrp ` G ) -> K C_ X )
27 9 26 syl 
 |-  ( ph -> K C_ X )
28 2 27 ssfid 
 |-  ( ph -> K e. Fin )
29 hashen 
 |-  ( ( H e. Fin /\ K e. Fin ) -> ( ( # ` H ) = ( # ` K ) <-> H ~~ K ) )
30 25 28 29 syl2anc 
 |-  ( ph -> ( ( # ` H ) = ( # ` K ) <-> H ~~ K ) )
31 20 30 mpbid 
 |-  ( ph -> H ~~ K )
32 1 5 6 11 conjsubgen 
 |-  ( ( K e. ( SubGrp ` G ) /\ g e. X ) -> K ~~ ran ( x e. K |-> ( ( g .+ x ) .- g ) ) )
33 9 10 32 syl2an2r 
 |-  ( ( ph /\ ( g e. X /\ H C_ ran ( x e. K |-> ( ( g .+ x ) .- g ) ) ) ) -> K ~~ ran ( x e. K |-> ( ( g .+ x ) .- g ) ) )
34 entr 
 |-  ( ( H ~~ K /\ K ~~ ran ( x e. K |-> ( ( g .+ x ) .- g ) ) ) -> H ~~ ran ( x e. K |-> ( ( g .+ x ) .- g ) ) )
35 31 33 34 syl2an2r 
 |-  ( ( ph /\ ( g e. X /\ H C_ ran ( x e. K |-> ( ( g .+ x ) .- g ) ) ) ) -> H ~~ ran ( x e. K |-> ( ( g .+ x ) .- g ) ) )
36 fisseneq 
 |-  ( ( ran ( x e. K |-> ( ( g .+ x ) .- g ) ) e. Fin /\ H C_ ran ( x e. K |-> ( ( g .+ x ) .- g ) ) /\ H ~~ ran ( x e. K |-> ( ( g .+ x ) .- g ) ) ) -> H = ran ( x e. K |-> ( ( g .+ x ) .- g ) ) )
37 16 17 35 36 syl3anc 
 |-  ( ( ph /\ ( g e. X /\ H C_ ran ( x e. K |-> ( ( g .+ x ) .- g ) ) ) ) -> H = ran ( x e. K |-> ( ( g .+ x ) .- g ) ) )
38 eqid 
 |-  ( G |`s H ) = ( G |`s H )
39 38 slwpgp 
 |-  ( H e. ( P pSyl G ) -> P pGrp ( G |`s H ) )
40 3 39 syl 
 |-  ( ph -> P pGrp ( G |`s H ) )
41 1 2 22 9 5 40 19 6 sylow2b 
 |-  ( ph -> E. g e. X H C_ ran ( x e. K |-> ( ( g .+ x ) .- g ) ) )
42 37 41 reximddv 
 |-  ( ph -> E. g e. X H = ran ( x e. K |-> ( ( g .+ x ) .- g ) ) )