Step |
Hyp |
Ref |
Expression |
1 |
|
sylow2a.x |
⊢ 𝑋 = ( Base ‘ 𝐺 ) |
2 |
|
sylow2a.m |
⊢ ( 𝜑 → ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ) |
3 |
|
sylow2a.p |
⊢ ( 𝜑 → 𝑃 pGrp 𝐺 ) |
4 |
|
sylow2a.f |
⊢ ( 𝜑 → 𝑋 ∈ Fin ) |
5 |
|
sylow2a.y |
⊢ ( 𝜑 → 𝑌 ∈ Fin ) |
6 |
|
sylow2a.z |
⊢ 𝑍 = { 𝑢 ∈ 𝑌 ∣ ∀ ℎ ∈ 𝑋 ( ℎ ⊕ 𝑢 ) = 𝑢 } |
7 |
|
sylow2a.r |
⊢ ∼ = { 〈 𝑥 , 𝑦 〉 ∣ ( { 𝑥 , 𝑦 } ⊆ 𝑌 ∧ ∃ 𝑔 ∈ 𝑋 ( 𝑔 ⊕ 𝑥 ) = 𝑦 ) } |
8 |
1 2 3 4 5 6 7
|
sylow2alem2 |
⊢ ( 𝜑 → 𝑃 ∥ Σ 𝑧 ∈ ( ( 𝑌 / ∼ ) ∖ 𝒫 𝑍 ) ( ♯ ‘ 𝑧 ) ) |
9 |
|
inass |
⊢ ( ( ( 𝑌 / ∼ ) ∩ 𝒫 𝑍 ) ∩ ( ( 𝑌 / ∼ ) ∖ 𝒫 𝑍 ) ) = ( ( 𝑌 / ∼ ) ∩ ( 𝒫 𝑍 ∩ ( ( 𝑌 / ∼ ) ∖ 𝒫 𝑍 ) ) ) |
10 |
|
disjdif |
⊢ ( 𝒫 𝑍 ∩ ( ( 𝑌 / ∼ ) ∖ 𝒫 𝑍 ) ) = ∅ |
11 |
10
|
ineq2i |
⊢ ( ( 𝑌 / ∼ ) ∩ ( 𝒫 𝑍 ∩ ( ( 𝑌 / ∼ ) ∖ 𝒫 𝑍 ) ) ) = ( ( 𝑌 / ∼ ) ∩ ∅ ) |
12 |
|
in0 |
⊢ ( ( 𝑌 / ∼ ) ∩ ∅ ) = ∅ |
13 |
9 11 12
|
3eqtri |
⊢ ( ( ( 𝑌 / ∼ ) ∩ 𝒫 𝑍 ) ∩ ( ( 𝑌 / ∼ ) ∖ 𝒫 𝑍 ) ) = ∅ |
14 |
13
|
a1i |
⊢ ( 𝜑 → ( ( ( 𝑌 / ∼ ) ∩ 𝒫 𝑍 ) ∩ ( ( 𝑌 / ∼ ) ∖ 𝒫 𝑍 ) ) = ∅ ) |
15 |
|
inundif |
⊢ ( ( ( 𝑌 / ∼ ) ∩ 𝒫 𝑍 ) ∪ ( ( 𝑌 / ∼ ) ∖ 𝒫 𝑍 ) ) = ( 𝑌 / ∼ ) |
16 |
15
|
eqcomi |
⊢ ( 𝑌 / ∼ ) = ( ( ( 𝑌 / ∼ ) ∩ 𝒫 𝑍 ) ∪ ( ( 𝑌 / ∼ ) ∖ 𝒫 𝑍 ) ) |
17 |
16
|
a1i |
⊢ ( 𝜑 → ( 𝑌 / ∼ ) = ( ( ( 𝑌 / ∼ ) ∩ 𝒫 𝑍 ) ∪ ( ( 𝑌 / ∼ ) ∖ 𝒫 𝑍 ) ) ) |
18 |
|
pwfi |
⊢ ( 𝑌 ∈ Fin ↔ 𝒫 𝑌 ∈ Fin ) |
19 |
5 18
|
sylib |
⊢ ( 𝜑 → 𝒫 𝑌 ∈ Fin ) |
20 |
7 1
|
gaorber |
⊢ ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) → ∼ Er 𝑌 ) |
21 |
2 20
|
syl |
⊢ ( 𝜑 → ∼ Er 𝑌 ) |
22 |
21
|
qsss |
⊢ ( 𝜑 → ( 𝑌 / ∼ ) ⊆ 𝒫 𝑌 ) |
23 |
19 22
|
ssfid |
⊢ ( 𝜑 → ( 𝑌 / ∼ ) ∈ Fin ) |
24 |
5
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝑌 / ∼ ) ) → 𝑌 ∈ Fin ) |
25 |
22
|
sselda |
⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝑌 / ∼ ) ) → 𝑧 ∈ 𝒫 𝑌 ) |
26 |
25
|
elpwid |
⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝑌 / ∼ ) ) → 𝑧 ⊆ 𝑌 ) |
27 |
24 26
|
ssfid |
⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝑌 / ∼ ) ) → 𝑧 ∈ Fin ) |
28 |
|
hashcl |
⊢ ( 𝑧 ∈ Fin → ( ♯ ‘ 𝑧 ) ∈ ℕ0 ) |
29 |
27 28
|
syl |
⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝑌 / ∼ ) ) → ( ♯ ‘ 𝑧 ) ∈ ℕ0 ) |
30 |
29
|
nn0cnd |
⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝑌 / ∼ ) ) → ( ♯ ‘ 𝑧 ) ∈ ℂ ) |
31 |
14 17 23 30
|
fsumsplit |
⊢ ( 𝜑 → Σ 𝑧 ∈ ( 𝑌 / ∼ ) ( ♯ ‘ 𝑧 ) = ( Σ 𝑧 ∈ ( ( 𝑌 / ∼ ) ∩ 𝒫 𝑍 ) ( ♯ ‘ 𝑧 ) + Σ 𝑧 ∈ ( ( 𝑌 / ∼ ) ∖ 𝒫 𝑍 ) ( ♯ ‘ 𝑧 ) ) ) |
32 |
21 5
|
qshash |
⊢ ( 𝜑 → ( ♯ ‘ 𝑌 ) = Σ 𝑧 ∈ ( 𝑌 / ∼ ) ( ♯ ‘ 𝑧 ) ) |
33 |
|
inss1 |
⊢ ( ( 𝑌 / ∼ ) ∩ 𝒫 𝑍 ) ⊆ ( 𝑌 / ∼ ) |
34 |
|
ssfi |
⊢ ( ( ( 𝑌 / ∼ ) ∈ Fin ∧ ( ( 𝑌 / ∼ ) ∩ 𝒫 𝑍 ) ⊆ ( 𝑌 / ∼ ) ) → ( ( 𝑌 / ∼ ) ∩ 𝒫 𝑍 ) ∈ Fin ) |
35 |
23 33 34
|
sylancl |
⊢ ( 𝜑 → ( ( 𝑌 / ∼ ) ∩ 𝒫 𝑍 ) ∈ Fin ) |
36 |
|
ax-1cn |
⊢ 1 ∈ ℂ |
37 |
|
fsumconst |
⊢ ( ( ( ( 𝑌 / ∼ ) ∩ 𝒫 𝑍 ) ∈ Fin ∧ 1 ∈ ℂ ) → Σ 𝑧 ∈ ( ( 𝑌 / ∼ ) ∩ 𝒫 𝑍 ) 1 = ( ( ♯ ‘ ( ( 𝑌 / ∼ ) ∩ 𝒫 𝑍 ) ) · 1 ) ) |
38 |
35 36 37
|
sylancl |
⊢ ( 𝜑 → Σ 𝑧 ∈ ( ( 𝑌 / ∼ ) ∩ 𝒫 𝑍 ) 1 = ( ( ♯ ‘ ( ( 𝑌 / ∼ ) ∩ 𝒫 𝑍 ) ) · 1 ) ) |
39 |
|
elin |
⊢ ( 𝑧 ∈ ( ( 𝑌 / ∼ ) ∩ 𝒫 𝑍 ) ↔ ( 𝑧 ∈ ( 𝑌 / ∼ ) ∧ 𝑧 ∈ 𝒫 𝑍 ) ) |
40 |
|
eqid |
⊢ ( 𝑌 / ∼ ) = ( 𝑌 / ∼ ) |
41 |
|
sseq1 |
⊢ ( [ 𝑤 ] ∼ = 𝑧 → ( [ 𝑤 ] ∼ ⊆ 𝑍 ↔ 𝑧 ⊆ 𝑍 ) ) |
42 |
|
velpw |
⊢ ( 𝑧 ∈ 𝒫 𝑍 ↔ 𝑧 ⊆ 𝑍 ) |
43 |
41 42
|
bitr4di |
⊢ ( [ 𝑤 ] ∼ = 𝑧 → ( [ 𝑤 ] ∼ ⊆ 𝑍 ↔ 𝑧 ∈ 𝒫 𝑍 ) ) |
44 |
|
breq1 |
⊢ ( [ 𝑤 ] ∼ = 𝑧 → ( [ 𝑤 ] ∼ ≈ 1o ↔ 𝑧 ≈ 1o ) ) |
45 |
43 44
|
imbi12d |
⊢ ( [ 𝑤 ] ∼ = 𝑧 → ( ( [ 𝑤 ] ∼ ⊆ 𝑍 → [ 𝑤 ] ∼ ≈ 1o ) ↔ ( 𝑧 ∈ 𝒫 𝑍 → 𝑧 ≈ 1o ) ) ) |
46 |
21
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑌 ) → ∼ Er 𝑌 ) |
47 |
|
simpr |
⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑌 ) → 𝑤 ∈ 𝑌 ) |
48 |
46 47
|
erref |
⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑌 ) → 𝑤 ∼ 𝑤 ) |
49 |
|
vex |
⊢ 𝑤 ∈ V |
50 |
49 49
|
elec |
⊢ ( 𝑤 ∈ [ 𝑤 ] ∼ ↔ 𝑤 ∼ 𝑤 ) |
51 |
48 50
|
sylibr |
⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑌 ) → 𝑤 ∈ [ 𝑤 ] ∼ ) |
52 |
|
ssel |
⊢ ( [ 𝑤 ] ∼ ⊆ 𝑍 → ( 𝑤 ∈ [ 𝑤 ] ∼ → 𝑤 ∈ 𝑍 ) ) |
53 |
51 52
|
syl5com |
⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑌 ) → ( [ 𝑤 ] ∼ ⊆ 𝑍 → 𝑤 ∈ 𝑍 ) ) |
54 |
1 2 3 4 5 6 7
|
sylow2alem1 |
⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑍 ) → [ 𝑤 ] ∼ = { 𝑤 } ) |
55 |
49
|
ensn1 |
⊢ { 𝑤 } ≈ 1o |
56 |
54 55
|
eqbrtrdi |
⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑍 ) → [ 𝑤 ] ∼ ≈ 1o ) |
57 |
56
|
ex |
⊢ ( 𝜑 → ( 𝑤 ∈ 𝑍 → [ 𝑤 ] ∼ ≈ 1o ) ) |
58 |
57
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑌 ) → ( 𝑤 ∈ 𝑍 → [ 𝑤 ] ∼ ≈ 1o ) ) |
59 |
53 58
|
syld |
⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑌 ) → ( [ 𝑤 ] ∼ ⊆ 𝑍 → [ 𝑤 ] ∼ ≈ 1o ) ) |
60 |
40 45 59
|
ectocld |
⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝑌 / ∼ ) ) → ( 𝑧 ∈ 𝒫 𝑍 → 𝑧 ≈ 1o ) ) |
61 |
60
|
impr |
⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ( 𝑌 / ∼ ) ∧ 𝑧 ∈ 𝒫 𝑍 ) ) → 𝑧 ≈ 1o ) |
62 |
39 61
|
sylan2b |
⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ( 𝑌 / ∼ ) ∩ 𝒫 𝑍 ) ) → 𝑧 ≈ 1o ) |
63 |
|
en1b |
⊢ ( 𝑧 ≈ 1o ↔ 𝑧 = { ∪ 𝑧 } ) |
64 |
62 63
|
sylib |
⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ( 𝑌 / ∼ ) ∩ 𝒫 𝑍 ) ) → 𝑧 = { ∪ 𝑧 } ) |
65 |
64
|
fveq2d |
⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ( 𝑌 / ∼ ) ∩ 𝒫 𝑍 ) ) → ( ♯ ‘ 𝑧 ) = ( ♯ ‘ { ∪ 𝑧 } ) ) |
66 |
|
vuniex |
⊢ ∪ 𝑧 ∈ V |
67 |
|
hashsng |
⊢ ( ∪ 𝑧 ∈ V → ( ♯ ‘ { ∪ 𝑧 } ) = 1 ) |
68 |
66 67
|
ax-mp |
⊢ ( ♯ ‘ { ∪ 𝑧 } ) = 1 |
69 |
65 68
|
eqtrdi |
⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ( 𝑌 / ∼ ) ∩ 𝒫 𝑍 ) ) → ( ♯ ‘ 𝑧 ) = 1 ) |
70 |
69
|
sumeq2dv |
⊢ ( 𝜑 → Σ 𝑧 ∈ ( ( 𝑌 / ∼ ) ∩ 𝒫 𝑍 ) ( ♯ ‘ 𝑧 ) = Σ 𝑧 ∈ ( ( 𝑌 / ∼ ) ∩ 𝒫 𝑍 ) 1 ) |
71 |
6
|
ssrab3 |
⊢ 𝑍 ⊆ 𝑌 |
72 |
|
ssfi |
⊢ ( ( 𝑌 ∈ Fin ∧ 𝑍 ⊆ 𝑌 ) → 𝑍 ∈ Fin ) |
73 |
5 71 72
|
sylancl |
⊢ ( 𝜑 → 𝑍 ∈ Fin ) |
74 |
|
hashcl |
⊢ ( 𝑍 ∈ Fin → ( ♯ ‘ 𝑍 ) ∈ ℕ0 ) |
75 |
73 74
|
syl |
⊢ ( 𝜑 → ( ♯ ‘ 𝑍 ) ∈ ℕ0 ) |
76 |
75
|
nn0cnd |
⊢ ( 𝜑 → ( ♯ ‘ 𝑍 ) ∈ ℂ ) |
77 |
76
|
mulid1d |
⊢ ( 𝜑 → ( ( ♯ ‘ 𝑍 ) · 1 ) = ( ♯ ‘ 𝑍 ) ) |
78 |
6 5
|
rabexd |
⊢ ( 𝜑 → 𝑍 ∈ V ) |
79 |
|
eqid |
⊢ ( 𝑤 ∈ 𝑍 ↦ { 𝑤 } ) = ( 𝑤 ∈ 𝑍 ↦ { 𝑤 } ) |
80 |
7
|
relopabiv |
⊢ Rel ∼ |
81 |
|
relssdmrn |
⊢ ( Rel ∼ → ∼ ⊆ ( dom ∼ × ran ∼ ) ) |
82 |
80 81
|
ax-mp |
⊢ ∼ ⊆ ( dom ∼ × ran ∼ ) |
83 |
|
erdm |
⊢ ( ∼ Er 𝑌 → dom ∼ = 𝑌 ) |
84 |
21 83
|
syl |
⊢ ( 𝜑 → dom ∼ = 𝑌 ) |
85 |
84 5
|
eqeltrd |
⊢ ( 𝜑 → dom ∼ ∈ Fin ) |
86 |
|
errn |
⊢ ( ∼ Er 𝑌 → ran ∼ = 𝑌 ) |
87 |
21 86
|
syl |
⊢ ( 𝜑 → ran ∼ = 𝑌 ) |
88 |
87 5
|
eqeltrd |
⊢ ( 𝜑 → ran ∼ ∈ Fin ) |
89 |
85 88
|
xpexd |
⊢ ( 𝜑 → ( dom ∼ × ran ∼ ) ∈ V ) |
90 |
|
ssexg |
⊢ ( ( ∼ ⊆ ( dom ∼ × ran ∼ ) ∧ ( dom ∼ × ran ∼ ) ∈ V ) → ∼ ∈ V ) |
91 |
82 89 90
|
sylancr |
⊢ ( 𝜑 → ∼ ∈ V ) |
92 |
|
simpr |
⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑍 ) → 𝑤 ∈ 𝑍 ) |
93 |
71 92
|
sselid |
⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑍 ) → 𝑤 ∈ 𝑌 ) |
94 |
|
ecelqsg |
⊢ ( ( ∼ ∈ V ∧ 𝑤 ∈ 𝑌 ) → [ 𝑤 ] ∼ ∈ ( 𝑌 / ∼ ) ) |
95 |
91 93 94
|
syl2an2r |
⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑍 ) → [ 𝑤 ] ∼ ∈ ( 𝑌 / ∼ ) ) |
96 |
54 95
|
eqeltrrd |
⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑍 ) → { 𝑤 } ∈ ( 𝑌 / ∼ ) ) |
97 |
|
snelpwi |
⊢ ( 𝑤 ∈ 𝑍 → { 𝑤 } ∈ 𝒫 𝑍 ) |
98 |
97
|
adantl |
⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑍 ) → { 𝑤 } ∈ 𝒫 𝑍 ) |
99 |
96 98
|
elind |
⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑍 ) → { 𝑤 } ∈ ( ( 𝑌 / ∼ ) ∩ 𝒫 𝑍 ) ) |
100 |
|
simpr |
⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ( 𝑌 / ∼ ) ∩ 𝒫 𝑍 ) ) → 𝑧 ∈ ( ( 𝑌 / ∼ ) ∩ 𝒫 𝑍 ) ) |
101 |
100
|
elin2d |
⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ( 𝑌 / ∼ ) ∩ 𝒫 𝑍 ) ) → 𝑧 ∈ 𝒫 𝑍 ) |
102 |
101
|
elpwid |
⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ( 𝑌 / ∼ ) ∩ 𝒫 𝑍 ) ) → 𝑧 ⊆ 𝑍 ) |
103 |
64 102
|
eqsstrrd |
⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ( 𝑌 / ∼ ) ∩ 𝒫 𝑍 ) ) → { ∪ 𝑧 } ⊆ 𝑍 ) |
104 |
66
|
snss |
⊢ ( ∪ 𝑧 ∈ 𝑍 ↔ { ∪ 𝑧 } ⊆ 𝑍 ) |
105 |
103 104
|
sylibr |
⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ( 𝑌 / ∼ ) ∩ 𝒫 𝑍 ) ) → ∪ 𝑧 ∈ 𝑍 ) |
106 |
|
sneq |
⊢ ( 𝑤 = ∪ 𝑧 → { 𝑤 } = { ∪ 𝑧 } ) |
107 |
106
|
eqeq2d |
⊢ ( 𝑤 = ∪ 𝑧 → ( 𝑧 = { 𝑤 } ↔ 𝑧 = { ∪ 𝑧 } ) ) |
108 |
64 107
|
syl5ibrcom |
⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ( 𝑌 / ∼ ) ∩ 𝒫 𝑍 ) ) → ( 𝑤 = ∪ 𝑧 → 𝑧 = { 𝑤 } ) ) |
109 |
108
|
adantrl |
⊢ ( ( 𝜑 ∧ ( 𝑤 ∈ 𝑍 ∧ 𝑧 ∈ ( ( 𝑌 / ∼ ) ∩ 𝒫 𝑍 ) ) ) → ( 𝑤 = ∪ 𝑧 → 𝑧 = { 𝑤 } ) ) |
110 |
|
unieq |
⊢ ( 𝑧 = { 𝑤 } → ∪ 𝑧 = ∪ { 𝑤 } ) |
111 |
49
|
unisn |
⊢ ∪ { 𝑤 } = 𝑤 |
112 |
110 111
|
eqtr2di |
⊢ ( 𝑧 = { 𝑤 } → 𝑤 = ∪ 𝑧 ) |
113 |
109 112
|
impbid1 |
⊢ ( ( 𝜑 ∧ ( 𝑤 ∈ 𝑍 ∧ 𝑧 ∈ ( ( 𝑌 / ∼ ) ∩ 𝒫 𝑍 ) ) ) → ( 𝑤 = ∪ 𝑧 ↔ 𝑧 = { 𝑤 } ) ) |
114 |
79 99 105 113
|
f1o2d |
⊢ ( 𝜑 → ( 𝑤 ∈ 𝑍 ↦ { 𝑤 } ) : 𝑍 –1-1-onto→ ( ( 𝑌 / ∼ ) ∩ 𝒫 𝑍 ) ) |
115 |
78 114
|
hasheqf1od |
⊢ ( 𝜑 → ( ♯ ‘ 𝑍 ) = ( ♯ ‘ ( ( 𝑌 / ∼ ) ∩ 𝒫 𝑍 ) ) ) |
116 |
115
|
oveq1d |
⊢ ( 𝜑 → ( ( ♯ ‘ 𝑍 ) · 1 ) = ( ( ♯ ‘ ( ( 𝑌 / ∼ ) ∩ 𝒫 𝑍 ) ) · 1 ) ) |
117 |
77 116
|
eqtr3d |
⊢ ( 𝜑 → ( ♯ ‘ 𝑍 ) = ( ( ♯ ‘ ( ( 𝑌 / ∼ ) ∩ 𝒫 𝑍 ) ) · 1 ) ) |
118 |
38 70 117
|
3eqtr4rd |
⊢ ( 𝜑 → ( ♯ ‘ 𝑍 ) = Σ 𝑧 ∈ ( ( 𝑌 / ∼ ) ∩ 𝒫 𝑍 ) ( ♯ ‘ 𝑧 ) ) |
119 |
118
|
oveq1d |
⊢ ( 𝜑 → ( ( ♯ ‘ 𝑍 ) + Σ 𝑧 ∈ ( ( 𝑌 / ∼ ) ∖ 𝒫 𝑍 ) ( ♯ ‘ 𝑧 ) ) = ( Σ 𝑧 ∈ ( ( 𝑌 / ∼ ) ∩ 𝒫 𝑍 ) ( ♯ ‘ 𝑧 ) + Σ 𝑧 ∈ ( ( 𝑌 / ∼ ) ∖ 𝒫 𝑍 ) ( ♯ ‘ 𝑧 ) ) ) |
120 |
31 32 119
|
3eqtr4rd |
⊢ ( 𝜑 → ( ( ♯ ‘ 𝑍 ) + Σ 𝑧 ∈ ( ( 𝑌 / ∼ ) ∖ 𝒫 𝑍 ) ( ♯ ‘ 𝑧 ) ) = ( ♯ ‘ 𝑌 ) ) |
121 |
|
hashcl |
⊢ ( 𝑌 ∈ Fin → ( ♯ ‘ 𝑌 ) ∈ ℕ0 ) |
122 |
5 121
|
syl |
⊢ ( 𝜑 → ( ♯ ‘ 𝑌 ) ∈ ℕ0 ) |
123 |
122
|
nn0cnd |
⊢ ( 𝜑 → ( ♯ ‘ 𝑌 ) ∈ ℂ ) |
124 |
|
diffi |
⊢ ( ( 𝑌 / ∼ ) ∈ Fin → ( ( 𝑌 / ∼ ) ∖ 𝒫 𝑍 ) ∈ Fin ) |
125 |
23 124
|
syl |
⊢ ( 𝜑 → ( ( 𝑌 / ∼ ) ∖ 𝒫 𝑍 ) ∈ Fin ) |
126 |
|
eldifi |
⊢ ( 𝑧 ∈ ( ( 𝑌 / ∼ ) ∖ 𝒫 𝑍 ) → 𝑧 ∈ ( 𝑌 / ∼ ) ) |
127 |
126 30
|
sylan2 |
⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ( 𝑌 / ∼ ) ∖ 𝒫 𝑍 ) ) → ( ♯ ‘ 𝑧 ) ∈ ℂ ) |
128 |
125 127
|
fsumcl |
⊢ ( 𝜑 → Σ 𝑧 ∈ ( ( 𝑌 / ∼ ) ∖ 𝒫 𝑍 ) ( ♯ ‘ 𝑧 ) ∈ ℂ ) |
129 |
123 76 128
|
subaddd |
⊢ ( 𝜑 → ( ( ( ♯ ‘ 𝑌 ) − ( ♯ ‘ 𝑍 ) ) = Σ 𝑧 ∈ ( ( 𝑌 / ∼ ) ∖ 𝒫 𝑍 ) ( ♯ ‘ 𝑧 ) ↔ ( ( ♯ ‘ 𝑍 ) + Σ 𝑧 ∈ ( ( 𝑌 / ∼ ) ∖ 𝒫 𝑍 ) ( ♯ ‘ 𝑧 ) ) = ( ♯ ‘ 𝑌 ) ) ) |
130 |
120 129
|
mpbird |
⊢ ( 𝜑 → ( ( ♯ ‘ 𝑌 ) − ( ♯ ‘ 𝑍 ) ) = Σ 𝑧 ∈ ( ( 𝑌 / ∼ ) ∖ 𝒫 𝑍 ) ( ♯ ‘ 𝑧 ) ) |
131 |
8 130
|
breqtrrd |
⊢ ( 𝜑 → 𝑃 ∥ ( ( ♯ ‘ 𝑌 ) − ( ♯ ‘ 𝑍 ) ) ) |