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