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 |
|
sylow3lem5.a |
|- .+ = ( +g ` G ) |
6 |
|
sylow3lem5.d |
|- .- = ( -g ` G ) |
7 |
|
sylow3lem5.k |
|- ( ph -> K e. ( P pSyl G ) ) |
8 |
|
sylow3lem5.m |
|- .(+) = ( x e. K , y e. ( P pSyl G ) |-> ran ( z e. y |-> ( ( x .+ z ) .- x ) ) ) |
9 |
|
sylow3lem6.n |
|- N = { x e. X | A. y e. X ( ( x .+ y ) e. s <-> ( y .+ x ) e. s ) } |
10 |
|
eqid |
|- ( Base ` ( G |`s K ) ) = ( Base ` ( G |`s K ) ) |
11 |
1 2 3 4 5 6 7 8
|
sylow3lem5 |
|- ( ph -> .(+) e. ( ( G |`s K ) GrpAct ( P pSyl G ) ) ) |
12 |
|
eqid |
|- ( G |`s K ) = ( G |`s K ) |
13 |
12
|
slwpgp |
|- ( K e. ( P pSyl G ) -> P pGrp ( G |`s K ) ) |
14 |
7 13
|
syl |
|- ( ph -> P pGrp ( G |`s K ) ) |
15 |
|
slwsubg |
|- ( K e. ( P pSyl G ) -> K e. ( SubGrp ` G ) ) |
16 |
7 15
|
syl |
|- ( ph -> K e. ( SubGrp ` G ) ) |
17 |
12
|
subgbas |
|- ( K e. ( SubGrp ` G ) -> K = ( Base ` ( G |`s K ) ) ) |
18 |
16 17
|
syl |
|- ( ph -> K = ( Base ` ( G |`s K ) ) ) |
19 |
1
|
subgss |
|- ( K e. ( SubGrp ` G ) -> K C_ X ) |
20 |
16 19
|
syl |
|- ( ph -> K C_ X ) |
21 |
3 20
|
ssfid |
|- ( ph -> K e. Fin ) |
22 |
18 21
|
eqeltrrd |
|- ( ph -> ( Base ` ( G |`s K ) ) e. Fin ) |
23 |
|
pwfi |
|- ( X e. Fin <-> ~P X e. Fin ) |
24 |
3 23
|
sylib |
|- ( ph -> ~P X e. Fin ) |
25 |
|
slwsubg |
|- ( x e. ( P pSyl G ) -> x e. ( SubGrp ` G ) ) |
26 |
1
|
subgss |
|- ( x e. ( SubGrp ` G ) -> x C_ X ) |
27 |
25 26
|
syl |
|- ( x e. ( P pSyl G ) -> x C_ X ) |
28 |
25 27
|
elpwd |
|- ( x e. ( P pSyl G ) -> x e. ~P X ) |
29 |
28
|
ssriv |
|- ( P pSyl G ) C_ ~P X |
30 |
|
ssfi |
|- ( ( ~P X e. Fin /\ ( P pSyl G ) C_ ~P X ) -> ( P pSyl G ) e. Fin ) |
31 |
24 29 30
|
sylancl |
|- ( ph -> ( P pSyl G ) e. Fin ) |
32 |
|
eqid |
|- { s e. ( P pSyl G ) | A. g e. ( Base ` ( G |`s K ) ) ( g .(+) s ) = s } = { s e. ( P pSyl G ) | A. g e. ( Base ` ( G |`s K ) ) ( g .(+) s ) = s } |
33 |
|
eqid |
|- { <. z , w >. | ( { z , w } C_ ( P pSyl G ) /\ E. h e. ( Base ` ( G |`s K ) ) ( h .(+) z ) = w ) } = { <. z , w >. | ( { z , w } C_ ( P pSyl G ) /\ E. h e. ( Base ` ( G |`s K ) ) ( h .(+) z ) = w ) } |
34 |
10 11 14 22 31 32 33
|
sylow2a |
|- ( ph -> P || ( ( # ` ( P pSyl G ) ) - ( # ` { s e. ( P pSyl G ) | A. g e. ( Base ` ( G |`s K ) ) ( g .(+) s ) = s } ) ) ) |
35 |
|
eqcom |
|- ( ran ( z e. s |-> ( ( g .+ z ) .- g ) ) = s <-> s = ran ( z e. s |-> ( ( g .+ z ) .- g ) ) ) |
36 |
20
|
adantr |
|- ( ( ph /\ s e. ( P pSyl G ) ) -> K C_ X ) |
37 |
36
|
sselda |
|- ( ( ( ph /\ s e. ( P pSyl G ) ) /\ g e. K ) -> g e. X ) |
38 |
37
|
biantrurd |
|- ( ( ( ph /\ s e. ( P pSyl G ) ) /\ g e. K ) -> ( s = ran ( z e. s |-> ( ( g .+ z ) .- g ) ) <-> ( g e. X /\ s = ran ( z e. s |-> ( ( g .+ z ) .- g ) ) ) ) ) |
39 |
35 38
|
syl5bb |
|- ( ( ( ph /\ s e. ( P pSyl G ) ) /\ g e. K ) -> ( ran ( z e. s |-> ( ( g .+ z ) .- g ) ) = s <-> ( g e. X /\ s = ran ( z e. s |-> ( ( g .+ z ) .- g ) ) ) ) ) |
40 |
|
simpr |
|- ( ( ( ph /\ s e. ( P pSyl G ) ) /\ g e. K ) -> g e. K ) |
41 |
|
simplr |
|- ( ( ( ph /\ s e. ( P pSyl G ) ) /\ g e. K ) -> s e. ( P pSyl G ) ) |
42 |
|
simpr |
|- ( ( x = g /\ y = s ) -> y = s ) |
43 |
|
simpl |
|- ( ( x = g /\ y = s ) -> x = g ) |
44 |
43
|
oveq1d |
|- ( ( x = g /\ y = s ) -> ( x .+ z ) = ( g .+ z ) ) |
45 |
44 43
|
oveq12d |
|- ( ( x = g /\ y = s ) -> ( ( x .+ z ) .- x ) = ( ( g .+ z ) .- g ) ) |
46 |
42 45
|
mpteq12dv |
|- ( ( x = g /\ y = s ) -> ( z e. y |-> ( ( x .+ z ) .- x ) ) = ( z e. s |-> ( ( g .+ z ) .- g ) ) ) |
47 |
46
|
rneqd |
|- ( ( x = g /\ y = s ) -> ran ( z e. y |-> ( ( x .+ z ) .- x ) ) = ran ( z e. s |-> ( ( g .+ z ) .- g ) ) ) |
48 |
|
vex |
|- s e. _V |
49 |
48
|
mptex |
|- ( z e. s |-> ( ( g .+ z ) .- g ) ) e. _V |
50 |
49
|
rnex |
|- ran ( z e. s |-> ( ( g .+ z ) .- g ) ) e. _V |
51 |
47 8 50
|
ovmpoa |
|- ( ( g e. K /\ s e. ( P pSyl G ) ) -> ( g .(+) s ) = ran ( z e. s |-> ( ( g .+ z ) .- g ) ) ) |
52 |
40 41 51
|
syl2anc |
|- ( ( ( ph /\ s e. ( P pSyl G ) ) /\ g e. K ) -> ( g .(+) s ) = ran ( z e. s |-> ( ( g .+ z ) .- g ) ) ) |
53 |
52
|
eqeq1d |
|- ( ( ( ph /\ s e. ( P pSyl G ) ) /\ g e. K ) -> ( ( g .(+) s ) = s <-> ran ( z e. s |-> ( ( g .+ z ) .- g ) ) = s ) ) |
54 |
|
slwsubg |
|- ( s e. ( P pSyl G ) -> s e. ( SubGrp ` G ) ) |
55 |
54
|
ad2antlr |
|- ( ( ( ph /\ s e. ( P pSyl G ) ) /\ g e. K ) -> s e. ( SubGrp ` G ) ) |
56 |
|
eqid |
|- ( z e. s |-> ( ( g .+ z ) .- g ) ) = ( z e. s |-> ( ( g .+ z ) .- g ) ) |
57 |
1 5 6 56 9
|
conjnmzb |
|- ( s e. ( SubGrp ` G ) -> ( g e. N <-> ( g e. X /\ s = ran ( z e. s |-> ( ( g .+ z ) .- g ) ) ) ) ) |
58 |
55 57
|
syl |
|- ( ( ( ph /\ s e. ( P pSyl G ) ) /\ g e. K ) -> ( g e. N <-> ( g e. X /\ s = ran ( z e. s |-> ( ( g .+ z ) .- g ) ) ) ) ) |
59 |
39 53 58
|
3bitr4d |
|- ( ( ( ph /\ s e. ( P pSyl G ) ) /\ g e. K ) -> ( ( g .(+) s ) = s <-> g e. N ) ) |
60 |
59
|
ralbidva |
|- ( ( ph /\ s e. ( P pSyl G ) ) -> ( A. g e. K ( g .(+) s ) = s <-> A. g e. K g e. N ) ) |
61 |
|
dfss3 |
|- ( K C_ N <-> A. g e. K g e. N ) |
62 |
60 61
|
bitr4di |
|- ( ( ph /\ s e. ( P pSyl G ) ) -> ( A. g e. K ( g .(+) s ) = s <-> K C_ N ) ) |
63 |
18
|
adantr |
|- ( ( ph /\ s e. ( P pSyl G ) ) -> K = ( Base ` ( G |`s K ) ) ) |
64 |
63
|
raleqdv |
|- ( ( ph /\ s e. ( P pSyl G ) ) -> ( A. g e. K ( g .(+) s ) = s <-> A. g e. ( Base ` ( G |`s K ) ) ( g .(+) s ) = s ) ) |
65 |
|
eqid |
|- ( Base ` ( G |`s N ) ) = ( Base ` ( G |`s N ) ) |
66 |
2
|
ad2antrr |
|- ( ( ( ph /\ s e. ( P pSyl G ) ) /\ K C_ N ) -> G e. Grp ) |
67 |
9 1 5
|
nmzsubg |
|- ( G e. Grp -> N e. ( SubGrp ` G ) ) |
68 |
66 67
|
syl |
|- ( ( ( ph /\ s e. ( P pSyl G ) ) /\ K C_ N ) -> N e. ( SubGrp ` G ) ) |
69 |
|
eqid |
|- ( G |`s N ) = ( G |`s N ) |
70 |
69
|
subgbas |
|- ( N e. ( SubGrp ` G ) -> N = ( Base ` ( G |`s N ) ) ) |
71 |
68 70
|
syl |
|- ( ( ( ph /\ s e. ( P pSyl G ) ) /\ K C_ N ) -> N = ( Base ` ( G |`s N ) ) ) |
72 |
3
|
ad2antrr |
|- ( ( ( ph /\ s e. ( P pSyl G ) ) /\ K C_ N ) -> X e. Fin ) |
73 |
1
|
subgss |
|- ( N e. ( SubGrp ` G ) -> N C_ X ) |
74 |
68 73
|
syl |
|- ( ( ( ph /\ s e. ( P pSyl G ) ) /\ K C_ N ) -> N C_ X ) |
75 |
72 74
|
ssfid |
|- ( ( ( ph /\ s e. ( P pSyl G ) ) /\ K C_ N ) -> N e. Fin ) |
76 |
71 75
|
eqeltrrd |
|- ( ( ( ph /\ s e. ( P pSyl G ) ) /\ K C_ N ) -> ( Base ` ( G |`s N ) ) e. Fin ) |
77 |
7
|
ad2antrr |
|- ( ( ( ph /\ s e. ( P pSyl G ) ) /\ K C_ N ) -> K e. ( P pSyl G ) ) |
78 |
|
simpr |
|- ( ( ( ph /\ s e. ( P pSyl G ) ) /\ K C_ N ) -> K C_ N ) |
79 |
69
|
subgslw |
|- ( ( N e. ( SubGrp ` G ) /\ K e. ( P pSyl G ) /\ K C_ N ) -> K e. ( P pSyl ( G |`s N ) ) ) |
80 |
68 77 78 79
|
syl3anc |
|- ( ( ( ph /\ s e. ( P pSyl G ) ) /\ K C_ N ) -> K e. ( P pSyl ( G |`s N ) ) ) |
81 |
|
simplr |
|- ( ( ( ph /\ s e. ( P pSyl G ) ) /\ K C_ N ) -> s e. ( P pSyl G ) ) |
82 |
54
|
ad2antlr |
|- ( ( ( ph /\ s e. ( P pSyl G ) ) /\ K C_ N ) -> s e. ( SubGrp ` G ) ) |
83 |
9 1 5
|
ssnmz |
|- ( s e. ( SubGrp ` G ) -> s C_ N ) |
84 |
82 83
|
syl |
|- ( ( ( ph /\ s e. ( P pSyl G ) ) /\ K C_ N ) -> s C_ N ) |
85 |
69
|
subgslw |
|- ( ( N e. ( SubGrp ` G ) /\ s e. ( P pSyl G ) /\ s C_ N ) -> s e. ( P pSyl ( G |`s N ) ) ) |
86 |
68 81 84 85
|
syl3anc |
|- ( ( ( ph /\ s e. ( P pSyl G ) ) /\ K C_ N ) -> s e. ( P pSyl ( G |`s N ) ) ) |
87 |
1
|
fvexi |
|- X e. _V |
88 |
9 87
|
rabex2 |
|- N e. _V |
89 |
69 5
|
ressplusg |
|- ( N e. _V -> .+ = ( +g ` ( G |`s N ) ) ) |
90 |
88 89
|
ax-mp |
|- .+ = ( +g ` ( G |`s N ) ) |
91 |
|
eqid |
|- ( -g ` ( G |`s N ) ) = ( -g ` ( G |`s N ) ) |
92 |
65 76 80 86 90 91
|
sylow2 |
|- ( ( ( ph /\ s e. ( P pSyl G ) ) /\ K C_ N ) -> E. g e. ( Base ` ( G |`s N ) ) K = ran ( z e. s |-> ( ( g .+ z ) ( -g ` ( G |`s N ) ) g ) ) ) |
93 |
9 1 5 69
|
nmznsg |
|- ( s e. ( SubGrp ` G ) -> s e. ( NrmSGrp ` ( G |`s N ) ) ) |
94 |
82 93
|
syl |
|- ( ( ( ph /\ s e. ( P pSyl G ) ) /\ K C_ N ) -> s e. ( NrmSGrp ` ( G |`s N ) ) ) |
95 |
|
eqid |
|- ( z e. s |-> ( ( g .+ z ) ( -g ` ( G |`s N ) ) g ) ) = ( z e. s |-> ( ( g .+ z ) ( -g ` ( G |`s N ) ) g ) ) |
96 |
65 90 91 95
|
conjnsg |
|- ( ( s e. ( NrmSGrp ` ( G |`s N ) ) /\ g e. ( Base ` ( G |`s N ) ) ) -> s = ran ( z e. s |-> ( ( g .+ z ) ( -g ` ( G |`s N ) ) g ) ) ) |
97 |
94 96
|
sylan |
|- ( ( ( ( ph /\ s e. ( P pSyl G ) ) /\ K C_ N ) /\ g e. ( Base ` ( G |`s N ) ) ) -> s = ran ( z e. s |-> ( ( g .+ z ) ( -g ` ( G |`s N ) ) g ) ) ) |
98 |
|
eqeq2 |
|- ( K = ran ( z e. s |-> ( ( g .+ z ) ( -g ` ( G |`s N ) ) g ) ) -> ( s = K <-> s = ran ( z e. s |-> ( ( g .+ z ) ( -g ` ( G |`s N ) ) g ) ) ) ) |
99 |
97 98
|
syl5ibrcom |
|- ( ( ( ( ph /\ s e. ( P pSyl G ) ) /\ K C_ N ) /\ g e. ( Base ` ( G |`s N ) ) ) -> ( K = ran ( z e. s |-> ( ( g .+ z ) ( -g ` ( G |`s N ) ) g ) ) -> s = K ) ) |
100 |
99
|
rexlimdva |
|- ( ( ( ph /\ s e. ( P pSyl G ) ) /\ K C_ N ) -> ( E. g e. ( Base ` ( G |`s N ) ) K = ran ( z e. s |-> ( ( g .+ z ) ( -g ` ( G |`s N ) ) g ) ) -> s = K ) ) |
101 |
92 100
|
mpd |
|- ( ( ( ph /\ s e. ( P pSyl G ) ) /\ K C_ N ) -> s = K ) |
102 |
|
simpr |
|- ( ( ( ph /\ s e. ( P pSyl G ) ) /\ s = K ) -> s = K ) |
103 |
16
|
ad2antrr |
|- ( ( ( ph /\ s e. ( P pSyl G ) ) /\ s = K ) -> K e. ( SubGrp ` G ) ) |
104 |
102 103
|
eqeltrd |
|- ( ( ( ph /\ s e. ( P pSyl G ) ) /\ s = K ) -> s e. ( SubGrp ` G ) ) |
105 |
104 83
|
syl |
|- ( ( ( ph /\ s e. ( P pSyl G ) ) /\ s = K ) -> s C_ N ) |
106 |
102 105
|
eqsstrrd |
|- ( ( ( ph /\ s e. ( P pSyl G ) ) /\ s = K ) -> K C_ N ) |
107 |
101 106
|
impbida |
|- ( ( ph /\ s e. ( P pSyl G ) ) -> ( K C_ N <-> s = K ) ) |
108 |
62 64 107
|
3bitr3d |
|- ( ( ph /\ s e. ( P pSyl G ) ) -> ( A. g e. ( Base ` ( G |`s K ) ) ( g .(+) s ) = s <-> s = K ) ) |
109 |
108
|
rabbidva |
|- ( ph -> { s e. ( P pSyl G ) | A. g e. ( Base ` ( G |`s K ) ) ( g .(+) s ) = s } = { s e. ( P pSyl G ) | s = K } ) |
110 |
|
rabsn |
|- ( K e. ( P pSyl G ) -> { s e. ( P pSyl G ) | s = K } = { K } ) |
111 |
7 110
|
syl |
|- ( ph -> { s e. ( P pSyl G ) | s = K } = { K } ) |
112 |
109 111
|
eqtrd |
|- ( ph -> { s e. ( P pSyl G ) | A. g e. ( Base ` ( G |`s K ) ) ( g .(+) s ) = s } = { K } ) |
113 |
112
|
fveq2d |
|- ( ph -> ( # ` { s e. ( P pSyl G ) | A. g e. ( Base ` ( G |`s K ) ) ( g .(+) s ) = s } ) = ( # ` { K } ) ) |
114 |
|
hashsng |
|- ( K e. ( P pSyl G ) -> ( # ` { K } ) = 1 ) |
115 |
7 114
|
syl |
|- ( ph -> ( # ` { K } ) = 1 ) |
116 |
113 115
|
eqtrd |
|- ( ph -> ( # ` { s e. ( P pSyl G ) | A. g e. ( Base ` ( G |`s K ) ) ( g .(+) s ) = s } ) = 1 ) |
117 |
116
|
oveq2d |
|- ( ph -> ( ( # ` ( P pSyl G ) ) - ( # ` { s e. ( P pSyl G ) | A. g e. ( Base ` ( G |`s K ) ) ( g .(+) s ) = s } ) ) = ( ( # ` ( P pSyl G ) ) - 1 ) ) |
118 |
34 117
|
breqtrd |
|- ( ph -> P || ( ( # ` ( P pSyl G ) ) - 1 ) ) |
119 |
|
prmnn |
|- ( P e. Prime -> P e. NN ) |
120 |
4 119
|
syl |
|- ( ph -> P e. NN ) |
121 |
|
hashcl |
|- ( ( P pSyl G ) e. Fin -> ( # ` ( P pSyl G ) ) e. NN0 ) |
122 |
31 121
|
syl |
|- ( ph -> ( # ` ( P pSyl G ) ) e. NN0 ) |
123 |
122
|
nn0zd |
|- ( ph -> ( # ` ( P pSyl G ) ) e. ZZ ) |
124 |
|
1zzd |
|- ( ph -> 1 e. ZZ ) |
125 |
|
moddvds |
|- ( ( P e. NN /\ ( # ` ( P pSyl G ) ) e. ZZ /\ 1 e. ZZ ) -> ( ( ( # ` ( P pSyl G ) ) mod P ) = ( 1 mod P ) <-> P || ( ( # ` ( P pSyl G ) ) - 1 ) ) ) |
126 |
120 123 124 125
|
syl3anc |
|- ( ph -> ( ( ( # ` ( P pSyl G ) ) mod P ) = ( 1 mod P ) <-> P || ( ( # ` ( P pSyl G ) ) - 1 ) ) ) |
127 |
118 126
|
mpbird |
|- ( ph -> ( ( # ` ( P pSyl G ) ) mod P ) = ( 1 mod P ) ) |
128 |
|
prmuz2 |
|- ( P e. Prime -> P e. ( ZZ>= ` 2 ) ) |
129 |
|
eluz2b2 |
|- ( P e. ( ZZ>= ` 2 ) <-> ( P e. NN /\ 1 < P ) ) |
130 |
|
nnre |
|- ( P e. NN -> P e. RR ) |
131 |
|
1mod |
|- ( ( P e. RR /\ 1 < P ) -> ( 1 mod P ) = 1 ) |
132 |
130 131
|
sylan |
|- ( ( P e. NN /\ 1 < P ) -> ( 1 mod P ) = 1 ) |
133 |
129 132
|
sylbi |
|- ( P e. ( ZZ>= ` 2 ) -> ( 1 mod P ) = 1 ) |
134 |
4 128 133
|
3syl |
|- ( ph -> ( 1 mod P ) = 1 ) |
135 |
127 134
|
eqtrd |
|- ( ph -> ( ( # ` ( P pSyl G ) ) mod P ) = 1 ) |