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 ) )