Metamath Proof Explorer


Theorem sylow3lem3

Description: Lemma for sylow3 , first part. The number of Sylow subgroups is the same as the index (number of cosets) of the normalizer of the Sylow subgroup K . (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 )
sylow3lem1.a
|- .+ = ( +g ` G )
sylow3lem1.d
|- .- = ( -g ` G )
sylow3lem1.m
|- .(+) = ( x e. X , y e. ( P pSyl G ) |-> ran ( z e. y |-> ( ( x .+ z ) .- x ) ) )
sylow3lem2.k
|- ( ph -> K e. ( P pSyl G ) )
sylow3lem2.h
|- H = { u e. X | ( u .(+) K ) = K }
sylow3lem2.n
|- N = { x e. X | A. y e. X ( ( x .+ y ) e. K <-> ( y .+ x ) e. K ) }
Assertion sylow3lem3
|- ( ph -> ( # ` ( P pSyl G ) ) = ( # ` ( X /. ( G ~QG N ) ) ) )

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 sylow3lem1.a
 |-  .+ = ( +g ` G )
6 sylow3lem1.d
 |-  .- = ( -g ` G )
7 sylow3lem1.m
 |-  .(+) = ( x e. X , y e. ( P pSyl G ) |-> ran ( z e. y |-> ( ( x .+ z ) .- x ) ) )
8 sylow3lem2.k
 |-  ( ph -> K e. ( P pSyl G ) )
9 sylow3lem2.h
 |-  H = { u e. X | ( u .(+) K ) = K }
10 sylow3lem2.n
 |-  N = { x e. X | A. y e. X ( ( x .+ y ) e. K <-> ( y .+ x ) e. K ) }
11 pwfi
 |-  ( X e. Fin <-> ~P X e. Fin )
12 3 11 sylib
 |-  ( ph -> ~P X e. Fin )
13 slwsubg
 |-  ( x e. ( P pSyl G ) -> x e. ( SubGrp ` G ) )
14 1 subgss
 |-  ( x e. ( SubGrp ` G ) -> x C_ X )
15 13 14 syl
 |-  ( x e. ( P pSyl G ) -> x C_ X )
16 13 15 elpwd
 |-  ( x e. ( P pSyl G ) -> x e. ~P X )
17 16 ssriv
 |-  ( P pSyl G ) C_ ~P X
18 ssfi
 |-  ( ( ~P X e. Fin /\ ( P pSyl G ) C_ ~P X ) -> ( P pSyl G ) e. Fin )
19 12 17 18 sylancl
 |-  ( ph -> ( P pSyl G ) e. Fin )
20 hashcl
 |-  ( ( P pSyl G ) e. Fin -> ( # ` ( P pSyl G ) ) e. NN0 )
21 19 20 syl
 |-  ( ph -> ( # ` ( P pSyl G ) ) e. NN0 )
22 21 nn0cnd
 |-  ( ph -> ( # ` ( P pSyl G ) ) e. CC )
23 10 1 5 nmzsubg
 |-  ( G e. Grp -> N e. ( SubGrp ` G ) )
24 eqid
 |-  ( G ~QG N ) = ( G ~QG N )
25 1 24 eqger
 |-  ( N e. ( SubGrp ` G ) -> ( G ~QG N ) Er X )
26 2 23 25 3syl
 |-  ( ph -> ( G ~QG N ) Er X )
27 26 qsss
 |-  ( ph -> ( X /. ( G ~QG N ) ) C_ ~P X )
28 12 27 ssfid
 |-  ( ph -> ( X /. ( G ~QG N ) ) e. Fin )
29 hashcl
 |-  ( ( X /. ( G ~QG N ) ) e. Fin -> ( # ` ( X /. ( G ~QG N ) ) ) e. NN0 )
30 28 29 syl
 |-  ( ph -> ( # ` ( X /. ( G ~QG N ) ) ) e. NN0 )
31 30 nn0cnd
 |-  ( ph -> ( # ` ( X /. ( G ~QG N ) ) ) e. CC )
32 2 23 syl
 |-  ( ph -> N e. ( SubGrp ` G ) )
33 eqid
 |-  ( 0g ` G ) = ( 0g ` G )
34 33 subg0cl
 |-  ( N e. ( SubGrp ` G ) -> ( 0g ` G ) e. N )
35 ne0i
 |-  ( ( 0g ` G ) e. N -> N =/= (/) )
36 32 34 35 3syl
 |-  ( ph -> N =/= (/) )
37 1 subgss
 |-  ( N e. ( SubGrp ` G ) -> N C_ X )
38 2 23 37 3syl
 |-  ( ph -> N C_ X )
39 3 38 ssfid
 |-  ( ph -> N e. Fin )
40 hashnncl
 |-  ( N e. Fin -> ( ( # ` N ) e. NN <-> N =/= (/) ) )
41 39 40 syl
 |-  ( ph -> ( ( # ` N ) e. NN <-> N =/= (/) ) )
42 36 41 mpbird
 |-  ( ph -> ( # ` N ) e. NN )
43 42 nncnd
 |-  ( ph -> ( # ` N ) e. CC )
44 42 nnne0d
 |-  ( ph -> ( # ` N ) =/= 0 )
45 1 2 3 4 5 6 7 sylow3lem1
 |-  ( ph -> .(+) e. ( G GrpAct ( P pSyl G ) ) )
46 eqid
 |-  ( G ~QG H ) = ( G ~QG H )
47 eqid
 |-  { <. x , y >. | ( { x , y } C_ ( P pSyl G ) /\ E. g e. X ( g .(+) x ) = y ) } = { <. x , y >. | ( { x , y } C_ ( P pSyl G ) /\ E. g e. X ( g .(+) x ) = y ) }
48 1 9 46 47 orbsta2
 |-  ( ( ( .(+) e. ( G GrpAct ( P pSyl G ) ) /\ K e. ( P pSyl G ) ) /\ X e. Fin ) -> ( # ` X ) = ( ( # ` [ K ] { <. x , y >. | ( { x , y } C_ ( P pSyl G ) /\ E. g e. X ( g .(+) x ) = y ) } ) x. ( # ` H ) ) )
49 45 8 3 48 syl21anc
 |-  ( ph -> ( # ` X ) = ( ( # ` [ K ] { <. x , y >. | ( { x , y } C_ ( P pSyl G ) /\ E. g e. X ( g .(+) x ) = y ) } ) x. ( # ` H ) ) )
50 1 24 32 3 lagsubg2
 |-  ( ph -> ( # ` X ) = ( ( # ` ( X /. ( G ~QG N ) ) ) x. ( # ` N ) ) )
51 47 1 gaorber
 |-  ( .(+) e. ( G GrpAct ( P pSyl G ) ) -> { <. x , y >. | ( { x , y } C_ ( P pSyl G ) /\ E. g e. X ( g .(+) x ) = y ) } Er ( P pSyl G ) )
52 45 51 syl
 |-  ( ph -> { <. x , y >. | ( { x , y } C_ ( P pSyl G ) /\ E. g e. X ( g .(+) x ) = y ) } Er ( P pSyl G ) )
53 52 ecss
 |-  ( ph -> [ K ] { <. x , y >. | ( { x , y } C_ ( P pSyl G ) /\ E. g e. X ( g .(+) x ) = y ) } C_ ( P pSyl G ) )
54 8 adantr
 |-  ( ( ph /\ h e. ( P pSyl G ) ) -> K e. ( P pSyl G ) )
55 simpr
 |-  ( ( ph /\ h e. ( P pSyl G ) ) -> h e. ( P pSyl G ) )
56 3 adantr
 |-  ( ( ph /\ h e. ( P pSyl G ) ) -> X e. Fin )
57 1 56 55 54 5 6 sylow2
 |-  ( ( ph /\ h e. ( P pSyl G ) ) -> E. u e. X h = ran ( z e. K |-> ( ( u .+ z ) .- u ) ) )
58 eqcom
 |-  ( ( u .(+) K ) = h <-> h = ( u .(+) K ) )
59 simpr
 |-  ( ( ( ph /\ h e. ( P pSyl G ) ) /\ u e. X ) -> u e. X )
60 54 adantr
 |-  ( ( ( ph /\ h e. ( P pSyl G ) ) /\ u e. X ) -> K e. ( P pSyl G ) )
61 mptexg
 |-  ( K e. ( P pSyl G ) -> ( z e. K |-> ( ( u .+ z ) .- u ) ) e. _V )
62 rnexg
 |-  ( ( z e. K |-> ( ( u .+ z ) .- u ) ) e. _V -> ran ( z e. K |-> ( ( u .+ z ) .- u ) ) e. _V )
63 60 61 62 3syl
 |-  ( ( ( ph /\ h e. ( P pSyl G ) ) /\ u e. X ) -> ran ( z e. K |-> ( ( u .+ z ) .- u ) ) e. _V )
64 simpr
 |-  ( ( x = u /\ y = K ) -> y = K )
65 simpl
 |-  ( ( x = u /\ y = K ) -> x = u )
66 65 oveq1d
 |-  ( ( x = u /\ y = K ) -> ( x .+ z ) = ( u .+ z ) )
67 66 65 oveq12d
 |-  ( ( x = u /\ y = K ) -> ( ( x .+ z ) .- x ) = ( ( u .+ z ) .- u ) )
68 64 67 mpteq12dv
 |-  ( ( x = u /\ y = K ) -> ( z e. y |-> ( ( x .+ z ) .- x ) ) = ( z e. K |-> ( ( u .+ z ) .- u ) ) )
69 68 rneqd
 |-  ( ( x = u /\ y = K ) -> ran ( z e. y |-> ( ( x .+ z ) .- x ) ) = ran ( z e. K |-> ( ( u .+ z ) .- u ) ) )
70 69 7 ovmpoga
 |-  ( ( u e. X /\ K e. ( P pSyl G ) /\ ran ( z e. K |-> ( ( u .+ z ) .- u ) ) e. _V ) -> ( u .(+) K ) = ran ( z e. K |-> ( ( u .+ z ) .- u ) ) )
71 59 60 63 70 syl3anc
 |-  ( ( ( ph /\ h e. ( P pSyl G ) ) /\ u e. X ) -> ( u .(+) K ) = ran ( z e. K |-> ( ( u .+ z ) .- u ) ) )
72 71 eqeq2d
 |-  ( ( ( ph /\ h e. ( P pSyl G ) ) /\ u e. X ) -> ( h = ( u .(+) K ) <-> h = ran ( z e. K |-> ( ( u .+ z ) .- u ) ) ) )
73 58 72 syl5bb
 |-  ( ( ( ph /\ h e. ( P pSyl G ) ) /\ u e. X ) -> ( ( u .(+) K ) = h <-> h = ran ( z e. K |-> ( ( u .+ z ) .- u ) ) ) )
74 73 rexbidva
 |-  ( ( ph /\ h e. ( P pSyl G ) ) -> ( E. u e. X ( u .(+) K ) = h <-> E. u e. X h = ran ( z e. K |-> ( ( u .+ z ) .- u ) ) ) )
75 57 74 mpbird
 |-  ( ( ph /\ h e. ( P pSyl G ) ) -> E. u e. X ( u .(+) K ) = h )
76 47 gaorb
 |-  ( K { <. x , y >. | ( { x , y } C_ ( P pSyl G ) /\ E. g e. X ( g .(+) x ) = y ) } h <-> ( K e. ( P pSyl G ) /\ h e. ( P pSyl G ) /\ E. u e. X ( u .(+) K ) = h ) )
77 54 55 75 76 syl3anbrc
 |-  ( ( ph /\ h e. ( P pSyl G ) ) -> K { <. x , y >. | ( { x , y } C_ ( P pSyl G ) /\ E. g e. X ( g .(+) x ) = y ) } h )
78 elecg
 |-  ( ( h e. ( P pSyl G ) /\ K e. ( P pSyl G ) ) -> ( h e. [ K ] { <. x , y >. | ( { x , y } C_ ( P pSyl G ) /\ E. g e. X ( g .(+) x ) = y ) } <-> K { <. x , y >. | ( { x , y } C_ ( P pSyl G ) /\ E. g e. X ( g .(+) x ) = y ) } h ) )
79 55 54 78 syl2anc
 |-  ( ( ph /\ h e. ( P pSyl G ) ) -> ( h e. [ K ] { <. x , y >. | ( { x , y } C_ ( P pSyl G ) /\ E. g e. X ( g .(+) x ) = y ) } <-> K { <. x , y >. | ( { x , y } C_ ( P pSyl G ) /\ E. g e. X ( g .(+) x ) = y ) } h ) )
80 77 79 mpbird
 |-  ( ( ph /\ h e. ( P pSyl G ) ) -> h e. [ K ] { <. x , y >. | ( { x , y } C_ ( P pSyl G ) /\ E. g e. X ( g .(+) x ) = y ) } )
81 53 80 eqelssd
 |-  ( ph -> [ K ] { <. x , y >. | ( { x , y } C_ ( P pSyl G ) /\ E. g e. X ( g .(+) x ) = y ) } = ( P pSyl G ) )
82 81 fveq2d
 |-  ( ph -> ( # ` [ K ] { <. x , y >. | ( { x , y } C_ ( P pSyl G ) /\ E. g e. X ( g .(+) x ) = y ) } ) = ( # ` ( P pSyl G ) ) )
83 1 2 3 4 5 6 7 8 9 10 sylow3lem2
 |-  ( ph -> H = N )
84 83 fveq2d
 |-  ( ph -> ( # ` H ) = ( # ` N ) )
85 82 84 oveq12d
 |-  ( ph -> ( ( # ` [ K ] { <. x , y >. | ( { x , y } C_ ( P pSyl G ) /\ E. g e. X ( g .(+) x ) = y ) } ) x. ( # ` H ) ) = ( ( # ` ( P pSyl G ) ) x. ( # ` N ) ) )
86 49 50 85 3eqtr3rd
 |-  ( ph -> ( ( # ` ( P pSyl G ) ) x. ( # ` N ) ) = ( ( # ` ( X /. ( G ~QG N ) ) ) x. ( # ` N ) ) )
87 22 31 43 44 86 mulcan2ad
 |-  ( ph -> ( # ` ( P pSyl G ) ) = ( # ` ( X /. ( G ~QG N ) ) ) )