Metamath Proof Explorer

Theorem sylow3

Description: Sylow's third theorem. The number of Sylow subgroups is a divisor of | G | / d , where d is the common order of a Sylow subgroup, and is equivalent to 1 mod P . This is part of Metamath 100 proof #72. (Contributed by Mario Carneiro, 19-Jan-2015)

Ref Expression
Hypotheses sylow3.x 
|- X = ( Base ` G )
sylow3.g 
|- ( ph -> G e. Grp )
sylow3.xf 
|- ( ph -> X e. Fin )
sylow3.p 
|- ( ph -> P e. Prime )
sylow3.n 
|- N = ( # ` ( P pSyl G ) )
Assertion sylow3 
|- ( ph -> ( N || ( ( # ` X ) / ( P ^ ( P pCnt ( # ` X ) ) ) ) /\ ( N mod P ) = 1 ) )

Proof

Step Hyp Ref Expression
1 sylow3.x 
 |-  X = ( Base ` G )
2 sylow3.g 
 |-  ( ph -> G e. Grp )
3 sylow3.xf 
 |-  ( ph -> X e. Fin )
4 sylow3.p 
 |-  ( ph -> P e. Prime )
5 sylow3.n 
 |-  N = ( # ` ( P pSyl G ) )
6 1 slwn0 
 |-  ( ( G e. Grp /\ X e. Fin /\ P e. Prime ) -> ( P pSyl G ) =/= (/) )
7 2 3 4 6 syl3anc 
 |-  ( ph -> ( P pSyl G ) =/= (/) )
8 n0 
 |-  ( ( P pSyl G ) =/= (/) <-> E. k k e. ( P pSyl G ) )
9 7 8 sylib 
 |-  ( ph -> E. k k e. ( P pSyl G ) )
10 2 adantr 
 |-  ( ( ph /\ k e. ( P pSyl G ) ) -> G e. Grp )
11 3 adantr 
 |-  ( ( ph /\ k e. ( P pSyl G ) ) -> X e. Fin )
12 4 adantr 
 |-  ( ( ph /\ k e. ( P pSyl G ) ) -> P e. Prime )
13 eqid 
 |-  ( +g ` G ) = ( +g ` G )
14 eqid 
 |-  ( -g ` G ) = ( -g ` G )
15 oveq2 
 |-  ( c = z -> ( a ( +g ` G ) c ) = ( a ( +g ` G ) z ) )
16 15 oveq1d 
 |-  ( c = z -> ( ( a ( +g ` G ) c ) ( -g ` G ) a ) = ( ( a ( +g ` G ) z ) ( -g ` G ) a ) )
17 16 cbvmptv 
 |-  ( c e. b |-> ( ( a ( +g ` G ) c ) ( -g ` G ) a ) ) = ( z e. b |-> ( ( a ( +g ` G ) z ) ( -g ` G ) a ) )
18 oveq1 
 |-  ( a = x -> ( a ( +g ` G ) z ) = ( x ( +g ` G ) z ) )
19 id 
 |-  ( a = x -> a = x )
20 18 19 oveq12d 
 |-  ( a = x -> ( ( a ( +g ` G ) z ) ( -g ` G ) a ) = ( ( x ( +g ` G ) z ) ( -g ` G ) x ) )
21 20 mpteq2dv 
 |-  ( a = x -> ( z e. b |-> ( ( a ( +g ` G ) z ) ( -g ` G ) a ) ) = ( z e. b |-> ( ( x ( +g ` G ) z ) ( -g ` G ) x ) ) )
22 17 21 syl5eq 
 |-  ( a = x -> ( c e. b |-> ( ( a ( +g ` G ) c ) ( -g ` G ) a ) ) = ( z e. b |-> ( ( x ( +g ` G ) z ) ( -g ` G ) x ) ) )
23 22 rneqd 
 |-  ( a = x -> ran ( c e. b |-> ( ( a ( +g ` G ) c ) ( -g ` G ) a ) ) = ran ( z e. b |-> ( ( x ( +g ` G ) z ) ( -g ` G ) x ) ) )
24 mpteq1 
 |-  ( b = y -> ( z e. b |-> ( ( x ( +g ` G ) z ) ( -g ` G ) x ) ) = ( z e. y |-> ( ( x ( +g ` G ) z ) ( -g ` G ) x ) ) )
25 24 rneqd 
 |-  ( b = y -> ran ( z e. b |-> ( ( x ( +g ` G ) z ) ( -g ` G ) x ) ) = ran ( z e. y |-> ( ( x ( +g ` G ) z ) ( -g ` G ) x ) ) )
26 23 25 cbvmpov 
 |-  ( a e. X , b e. ( P pSyl G ) |-> ran ( c e. b |-> ( ( a ( +g ` G ) c ) ( -g ` G ) a ) ) ) = ( x e. X , y e. ( P pSyl G ) |-> ran ( z e. y |-> ( ( x ( +g ` G ) z ) ( -g ` G ) x ) ) )
27 simpr 
 |-  ( ( ph /\ k e. ( P pSyl G ) ) -> k e. ( P pSyl G ) )
28 eqid 
 |-  { u e. X | ( u ( a e. X , b e. ( P pSyl G ) |-> ran ( c e. b |-> ( ( a ( +g ` G ) c ) ( -g ` G ) a ) ) ) k ) = k } = { u e. X | ( u ( a e. X , b e. ( P pSyl G ) |-> ran ( c e. b |-> ( ( a ( +g ` G ) c ) ( -g ` G ) a ) ) ) k ) = k }
29 eqid 
 |-  { x e. X | A. y e. X ( ( x ( +g ` G ) y ) e. k <-> ( y ( +g ` G ) x ) e. k ) } = { x e. X | A. y e. X ( ( x ( +g ` G ) y ) e. k <-> ( y ( +g ` G ) x ) e. k ) }
30 1 10 11 12 13 14 26 27 28 29 sylow3lem4 
 |-  ( ( ph /\ k e. ( P pSyl G ) ) -> ( # ` ( P pSyl G ) ) || ( ( # ` X ) / ( P ^ ( P pCnt ( # ` X ) ) ) ) )
31 5 30 eqbrtrid 
 |-  ( ( ph /\ k e. ( P pSyl G ) ) -> N || ( ( # ` X ) / ( P ^ ( P pCnt ( # ` X ) ) ) ) )
32 5 oveq1i 
 |-  ( N mod P ) = ( ( # ` ( P pSyl G ) ) mod P )
33 23 25 cbvmpov 
 |-  ( a e. k , b e. ( P pSyl G ) |-> ran ( c e. b |-> ( ( a ( +g ` G ) c ) ( -g ` G ) a ) ) ) = ( x e. k , y e. ( P pSyl G ) |-> ran ( z e. y |-> ( ( x ( +g ` G ) z ) ( -g ` G ) x ) ) )
34 eqid 
 |-  { x e. X | A. y e. X ( ( x ( +g ` G ) y ) e. s <-> ( y ( +g ` G ) x ) e. s ) } = { x e. X | A. y e. X ( ( x ( +g ` G ) y ) e. s <-> ( y ( +g ` G ) x ) e. s ) }
35 1 10 11 12 13 14 27 33 34 sylow3lem6 
 |-  ( ( ph /\ k e. ( P pSyl G ) ) -> ( ( # ` ( P pSyl G ) ) mod P ) = 1 )
36 32 35 syl5eq 
 |-  ( ( ph /\ k e. ( P pSyl G ) ) -> ( N mod P ) = 1 )
37 31 36 jca 
 |-  ( ( ph /\ k e. ( P pSyl G ) ) -> ( N || ( ( # ` X ) / ( P ^ ( P pCnt ( # ` X ) ) ) ) /\ ( N mod P ) = 1 ) )
38 9 37 exlimddv 
 |-  ( ph -> ( N || ( ( # ` X ) / ( P ^ ( P pCnt ( # ` X ) ) ) ) /\ ( N mod P ) = 1 ) )