Step |
Hyp |
Ref |
Expression |
1 |
|
sylow2a.x |
|- X = ( Base ` G ) |
2 |
|
sylow2a.m |
|- ( ph -> .(+) e. ( G GrpAct Y ) ) |
3 |
|
sylow2a.p |
|- ( ph -> P pGrp G ) |
4 |
|
sylow2a.f |
|- ( ph -> X e. Fin ) |
5 |
|
sylow2a.y |
|- ( ph -> Y e. Fin ) |
6 |
|
sylow2a.z |
|- Z = { u e. Y | A. h e. X ( h .(+) u ) = u } |
7 |
|
sylow2a.r |
|- .~ = { <. x , y >. | ( { x , y } C_ Y /\ E. g e. X ( g .(+) x ) = y ) } |
8 |
1 2 3 4 5 6 7
|
sylow2alem2 |
|- ( ph -> P || sum_ z e. ( ( Y /. .~ ) \ ~P Z ) ( # ` z ) ) |
9 |
|
inass |
|- ( ( ( Y /. .~ ) i^i ~P Z ) i^i ( ( Y /. .~ ) \ ~P Z ) ) = ( ( Y /. .~ ) i^i ( ~P Z i^i ( ( Y /. .~ ) \ ~P Z ) ) ) |
10 |
|
disjdif |
|- ( ~P Z i^i ( ( Y /. .~ ) \ ~P Z ) ) = (/) |
11 |
10
|
ineq2i |
|- ( ( Y /. .~ ) i^i ( ~P Z i^i ( ( Y /. .~ ) \ ~P Z ) ) ) = ( ( Y /. .~ ) i^i (/) ) |
12 |
|
in0 |
|- ( ( Y /. .~ ) i^i (/) ) = (/) |
13 |
9 11 12
|
3eqtri |
|- ( ( ( Y /. .~ ) i^i ~P Z ) i^i ( ( Y /. .~ ) \ ~P Z ) ) = (/) |
14 |
13
|
a1i |
|- ( ph -> ( ( ( Y /. .~ ) i^i ~P Z ) i^i ( ( Y /. .~ ) \ ~P Z ) ) = (/) ) |
15 |
|
inundif |
|- ( ( ( Y /. .~ ) i^i ~P Z ) u. ( ( Y /. .~ ) \ ~P Z ) ) = ( Y /. .~ ) |
16 |
15
|
eqcomi |
|- ( Y /. .~ ) = ( ( ( Y /. .~ ) i^i ~P Z ) u. ( ( Y /. .~ ) \ ~P Z ) ) |
17 |
16
|
a1i |
|- ( ph -> ( Y /. .~ ) = ( ( ( Y /. .~ ) i^i ~P Z ) u. ( ( Y /. .~ ) \ ~P Z ) ) ) |
18 |
|
pwfi |
|- ( Y e. Fin <-> ~P Y e. Fin ) |
19 |
5 18
|
sylib |
|- ( ph -> ~P Y e. Fin ) |
20 |
7 1
|
gaorber |
|- ( .(+) e. ( G GrpAct Y ) -> .~ Er Y ) |
21 |
2 20
|
syl |
|- ( ph -> .~ Er Y ) |
22 |
21
|
qsss |
|- ( ph -> ( Y /. .~ ) C_ ~P Y ) |
23 |
19 22
|
ssfid |
|- ( ph -> ( Y /. .~ ) e. Fin ) |
24 |
5
|
adantr |
|- ( ( ph /\ z e. ( Y /. .~ ) ) -> Y e. Fin ) |
25 |
22
|
sselda |
|- ( ( ph /\ z e. ( Y /. .~ ) ) -> z e. ~P Y ) |
26 |
25
|
elpwid |
|- ( ( ph /\ z e. ( Y /. .~ ) ) -> z C_ Y ) |
27 |
24 26
|
ssfid |
|- ( ( ph /\ z e. ( Y /. .~ ) ) -> z e. Fin ) |
28 |
|
hashcl |
|- ( z e. Fin -> ( # ` z ) e. NN0 ) |
29 |
27 28
|
syl |
|- ( ( ph /\ z e. ( Y /. .~ ) ) -> ( # ` z ) e. NN0 ) |
30 |
29
|
nn0cnd |
|- ( ( ph /\ z e. ( Y /. .~ ) ) -> ( # ` z ) e. CC ) |
31 |
14 17 23 30
|
fsumsplit |
|- ( ph -> sum_ z e. ( Y /. .~ ) ( # ` z ) = ( sum_ z e. ( ( Y /. .~ ) i^i ~P Z ) ( # ` z ) + sum_ z e. ( ( Y /. .~ ) \ ~P Z ) ( # ` z ) ) ) |
32 |
21 5
|
qshash |
|- ( ph -> ( # ` Y ) = sum_ z e. ( Y /. .~ ) ( # ` z ) ) |
33 |
|
inss1 |
|- ( ( Y /. .~ ) i^i ~P Z ) C_ ( Y /. .~ ) |
34 |
|
ssfi |
|- ( ( ( Y /. .~ ) e. Fin /\ ( ( Y /. .~ ) i^i ~P Z ) C_ ( Y /. .~ ) ) -> ( ( Y /. .~ ) i^i ~P Z ) e. Fin ) |
35 |
23 33 34
|
sylancl |
|- ( ph -> ( ( Y /. .~ ) i^i ~P Z ) e. Fin ) |
36 |
|
ax-1cn |
|- 1 e. CC |
37 |
|
fsumconst |
|- ( ( ( ( Y /. .~ ) i^i ~P Z ) e. Fin /\ 1 e. CC ) -> sum_ z e. ( ( Y /. .~ ) i^i ~P Z ) 1 = ( ( # ` ( ( Y /. .~ ) i^i ~P Z ) ) x. 1 ) ) |
38 |
35 36 37
|
sylancl |
|- ( ph -> sum_ z e. ( ( Y /. .~ ) i^i ~P Z ) 1 = ( ( # ` ( ( Y /. .~ ) i^i ~P Z ) ) x. 1 ) ) |
39 |
|
elin |
|- ( z e. ( ( Y /. .~ ) i^i ~P Z ) <-> ( z e. ( Y /. .~ ) /\ z e. ~P Z ) ) |
40 |
|
eqid |
|- ( Y /. .~ ) = ( Y /. .~ ) |
41 |
|
sseq1 |
|- ( [ w ] .~ = z -> ( [ w ] .~ C_ Z <-> z C_ Z ) ) |
42 |
|
velpw |
|- ( z e. ~P Z <-> z C_ Z ) |
43 |
41 42
|
bitr4di |
|- ( [ w ] .~ = z -> ( [ w ] .~ C_ Z <-> z e. ~P Z ) ) |
44 |
|
breq1 |
|- ( [ w ] .~ = z -> ( [ w ] .~ ~~ 1o <-> z ~~ 1o ) ) |
45 |
43 44
|
imbi12d |
|- ( [ w ] .~ = z -> ( ( [ w ] .~ C_ Z -> [ w ] .~ ~~ 1o ) <-> ( z e. ~P Z -> z ~~ 1o ) ) ) |
46 |
21
|
adantr |
|- ( ( ph /\ w e. Y ) -> .~ Er Y ) |
47 |
|
simpr |
|- ( ( ph /\ w e. Y ) -> w e. Y ) |
48 |
46 47
|
erref |
|- ( ( ph /\ w e. Y ) -> w .~ w ) |
49 |
|
vex |
|- w e. _V |
50 |
49 49
|
elec |
|- ( w e. [ w ] .~ <-> w .~ w ) |
51 |
48 50
|
sylibr |
|- ( ( ph /\ w e. Y ) -> w e. [ w ] .~ ) |
52 |
|
ssel |
|- ( [ w ] .~ C_ Z -> ( w e. [ w ] .~ -> w e. Z ) ) |
53 |
51 52
|
syl5com |
|- ( ( ph /\ w e. Y ) -> ( [ w ] .~ C_ Z -> w e. Z ) ) |
54 |
1 2 3 4 5 6 7
|
sylow2alem1 |
|- ( ( ph /\ w e. Z ) -> [ w ] .~ = { w } ) |
55 |
49
|
ensn1 |
|- { w } ~~ 1o |
56 |
54 55
|
eqbrtrdi |
|- ( ( ph /\ w e. Z ) -> [ w ] .~ ~~ 1o ) |
57 |
56
|
ex |
|- ( ph -> ( w e. Z -> [ w ] .~ ~~ 1o ) ) |
58 |
57
|
adantr |
|- ( ( ph /\ w e. Y ) -> ( w e. Z -> [ w ] .~ ~~ 1o ) ) |
59 |
53 58
|
syld |
|- ( ( ph /\ w e. Y ) -> ( [ w ] .~ C_ Z -> [ w ] .~ ~~ 1o ) ) |
60 |
40 45 59
|
ectocld |
|- ( ( ph /\ z e. ( Y /. .~ ) ) -> ( z e. ~P Z -> z ~~ 1o ) ) |
61 |
60
|
impr |
|- ( ( ph /\ ( z e. ( Y /. .~ ) /\ z e. ~P Z ) ) -> z ~~ 1o ) |
62 |
39 61
|
sylan2b |
|- ( ( ph /\ z e. ( ( Y /. .~ ) i^i ~P Z ) ) -> z ~~ 1o ) |
63 |
|
en1b |
|- ( z ~~ 1o <-> z = { U. z } ) |
64 |
62 63
|
sylib |
|- ( ( ph /\ z e. ( ( Y /. .~ ) i^i ~P Z ) ) -> z = { U. z } ) |
65 |
64
|
fveq2d |
|- ( ( ph /\ z e. ( ( Y /. .~ ) i^i ~P Z ) ) -> ( # ` z ) = ( # ` { U. z } ) ) |
66 |
|
vuniex |
|- U. z e. _V |
67 |
|
hashsng |
|- ( U. z e. _V -> ( # ` { U. z } ) = 1 ) |
68 |
66 67
|
ax-mp |
|- ( # ` { U. z } ) = 1 |
69 |
65 68
|
eqtrdi |
|- ( ( ph /\ z e. ( ( Y /. .~ ) i^i ~P Z ) ) -> ( # ` z ) = 1 ) |
70 |
69
|
sumeq2dv |
|- ( ph -> sum_ z e. ( ( Y /. .~ ) i^i ~P Z ) ( # ` z ) = sum_ z e. ( ( Y /. .~ ) i^i ~P Z ) 1 ) |
71 |
6
|
ssrab3 |
|- Z C_ Y |
72 |
|
ssfi |
|- ( ( Y e. Fin /\ Z C_ Y ) -> Z e. Fin ) |
73 |
5 71 72
|
sylancl |
|- ( ph -> Z e. Fin ) |
74 |
|
hashcl |
|- ( Z e. Fin -> ( # ` Z ) e. NN0 ) |
75 |
73 74
|
syl |
|- ( ph -> ( # ` Z ) e. NN0 ) |
76 |
75
|
nn0cnd |
|- ( ph -> ( # ` Z ) e. CC ) |
77 |
76
|
mulid1d |
|- ( ph -> ( ( # ` Z ) x. 1 ) = ( # ` Z ) ) |
78 |
6 5
|
rabexd |
|- ( ph -> Z e. _V ) |
79 |
|
eqid |
|- ( w e. Z |-> { w } ) = ( w e. Z |-> { w } ) |
80 |
7
|
relopabiv |
|- Rel .~ |
81 |
|
relssdmrn |
|- ( Rel .~ -> .~ C_ ( dom .~ X. ran .~ ) ) |
82 |
80 81
|
ax-mp |
|- .~ C_ ( dom .~ X. ran .~ ) |
83 |
|
erdm |
|- ( .~ Er Y -> dom .~ = Y ) |
84 |
21 83
|
syl |
|- ( ph -> dom .~ = Y ) |
85 |
84 5
|
eqeltrd |
|- ( ph -> dom .~ e. Fin ) |
86 |
|
errn |
|- ( .~ Er Y -> ran .~ = Y ) |
87 |
21 86
|
syl |
|- ( ph -> ran .~ = Y ) |
88 |
87 5
|
eqeltrd |
|- ( ph -> ran .~ e. Fin ) |
89 |
85 88
|
xpexd |
|- ( ph -> ( dom .~ X. ran .~ ) e. _V ) |
90 |
|
ssexg |
|- ( ( .~ C_ ( dom .~ X. ran .~ ) /\ ( dom .~ X. ran .~ ) e. _V ) -> .~ e. _V ) |
91 |
82 89 90
|
sylancr |
|- ( ph -> .~ e. _V ) |
92 |
|
simpr |
|- ( ( ph /\ w e. Z ) -> w e. Z ) |
93 |
71 92
|
sselid |
|- ( ( ph /\ w e. Z ) -> w e. Y ) |
94 |
|
ecelqsg |
|- ( ( .~ e. _V /\ w e. Y ) -> [ w ] .~ e. ( Y /. .~ ) ) |
95 |
91 93 94
|
syl2an2r |
|- ( ( ph /\ w e. Z ) -> [ w ] .~ e. ( Y /. .~ ) ) |
96 |
54 95
|
eqeltrrd |
|- ( ( ph /\ w e. Z ) -> { w } e. ( Y /. .~ ) ) |
97 |
|
snelpwi |
|- ( w e. Z -> { w } e. ~P Z ) |
98 |
97
|
adantl |
|- ( ( ph /\ w e. Z ) -> { w } e. ~P Z ) |
99 |
96 98
|
elind |
|- ( ( ph /\ w e. Z ) -> { w } e. ( ( Y /. .~ ) i^i ~P Z ) ) |
100 |
|
simpr |
|- ( ( ph /\ z e. ( ( Y /. .~ ) i^i ~P Z ) ) -> z e. ( ( Y /. .~ ) i^i ~P Z ) ) |
101 |
100
|
elin2d |
|- ( ( ph /\ z e. ( ( Y /. .~ ) i^i ~P Z ) ) -> z e. ~P Z ) |
102 |
101
|
elpwid |
|- ( ( ph /\ z e. ( ( Y /. .~ ) i^i ~P Z ) ) -> z C_ Z ) |
103 |
64 102
|
eqsstrrd |
|- ( ( ph /\ z e. ( ( Y /. .~ ) i^i ~P Z ) ) -> { U. z } C_ Z ) |
104 |
66
|
snss |
|- ( U. z e. Z <-> { U. z } C_ Z ) |
105 |
103 104
|
sylibr |
|- ( ( ph /\ z e. ( ( Y /. .~ ) i^i ~P Z ) ) -> U. z e. Z ) |
106 |
|
sneq |
|- ( w = U. z -> { w } = { U. z } ) |
107 |
106
|
eqeq2d |
|- ( w = U. z -> ( z = { w } <-> z = { U. z } ) ) |
108 |
64 107
|
syl5ibrcom |
|- ( ( ph /\ z e. ( ( Y /. .~ ) i^i ~P Z ) ) -> ( w = U. z -> z = { w } ) ) |
109 |
108
|
adantrl |
|- ( ( ph /\ ( w e. Z /\ z e. ( ( Y /. .~ ) i^i ~P Z ) ) ) -> ( w = U. z -> z = { w } ) ) |
110 |
|
unieq |
|- ( z = { w } -> U. z = U. { w } ) |
111 |
49
|
unisn |
|- U. { w } = w |
112 |
110 111
|
eqtr2di |
|- ( z = { w } -> w = U. z ) |
113 |
109 112
|
impbid1 |
|- ( ( ph /\ ( w e. Z /\ z e. ( ( Y /. .~ ) i^i ~P Z ) ) ) -> ( w = U. z <-> z = { w } ) ) |
114 |
79 99 105 113
|
f1o2d |
|- ( ph -> ( w e. Z |-> { w } ) : Z -1-1-onto-> ( ( Y /. .~ ) i^i ~P Z ) ) |
115 |
78 114
|
hasheqf1od |
|- ( ph -> ( # ` Z ) = ( # ` ( ( Y /. .~ ) i^i ~P Z ) ) ) |
116 |
115
|
oveq1d |
|- ( ph -> ( ( # ` Z ) x. 1 ) = ( ( # ` ( ( Y /. .~ ) i^i ~P Z ) ) x. 1 ) ) |
117 |
77 116
|
eqtr3d |
|- ( ph -> ( # ` Z ) = ( ( # ` ( ( Y /. .~ ) i^i ~P Z ) ) x. 1 ) ) |
118 |
38 70 117
|
3eqtr4rd |
|- ( ph -> ( # ` Z ) = sum_ z e. ( ( Y /. .~ ) i^i ~P Z ) ( # ` z ) ) |
119 |
118
|
oveq1d |
|- ( ph -> ( ( # ` Z ) + sum_ z e. ( ( Y /. .~ ) \ ~P Z ) ( # ` z ) ) = ( sum_ z e. ( ( Y /. .~ ) i^i ~P Z ) ( # ` z ) + sum_ z e. ( ( Y /. .~ ) \ ~P Z ) ( # ` z ) ) ) |
120 |
31 32 119
|
3eqtr4rd |
|- ( ph -> ( ( # ` Z ) + sum_ z e. ( ( Y /. .~ ) \ ~P Z ) ( # ` z ) ) = ( # ` Y ) ) |
121 |
|
hashcl |
|- ( Y e. Fin -> ( # ` Y ) e. NN0 ) |
122 |
5 121
|
syl |
|- ( ph -> ( # ` Y ) e. NN0 ) |
123 |
122
|
nn0cnd |
|- ( ph -> ( # ` Y ) e. CC ) |
124 |
|
diffi |
|- ( ( Y /. .~ ) e. Fin -> ( ( Y /. .~ ) \ ~P Z ) e. Fin ) |
125 |
23 124
|
syl |
|- ( ph -> ( ( Y /. .~ ) \ ~P Z ) e. Fin ) |
126 |
|
eldifi |
|- ( z e. ( ( Y /. .~ ) \ ~P Z ) -> z e. ( Y /. .~ ) ) |
127 |
126 30
|
sylan2 |
|- ( ( ph /\ z e. ( ( Y /. .~ ) \ ~P Z ) ) -> ( # ` z ) e. CC ) |
128 |
125 127
|
fsumcl |
|- ( ph -> sum_ z e. ( ( Y /. .~ ) \ ~P Z ) ( # ` z ) e. CC ) |
129 |
123 76 128
|
subaddd |
|- ( ph -> ( ( ( # ` Y ) - ( # ` Z ) ) = sum_ z e. ( ( Y /. .~ ) \ ~P Z ) ( # ` z ) <-> ( ( # ` Z ) + sum_ z e. ( ( Y /. .~ ) \ ~P Z ) ( # ` z ) ) = ( # ` Y ) ) ) |
130 |
120 129
|
mpbird |
|- ( ph -> ( ( # ` Y ) - ( # ` Z ) ) = sum_ z e. ( ( Y /. .~ ) \ ~P Z ) ( # ` z ) ) |
131 |
8 130
|
breqtrrd |
|- ( ph -> P || ( ( # ` Y ) - ( # ` Z ) ) ) |