Step | Hyp | Ref
| Expression |
1 | | csbeq1a 3066 |
. . . 4
⊢ (𝑥 = ⟨(2nd
‘𝑦), (1st
‘𝑦)⟩ →
𝐵 =
⦋⟨(2nd ‘𝑦), (1st ‘𝑦)⟩ / 𝑥⦌𝐵) |
2 | | 2ndexg 6168 |
. . . . . 6
⊢ (𝑦 ∈ V → (2nd
‘𝑦) ∈
V) |
3 | 2 | elv 2741 |
. . . . 5
⊢
(2nd ‘𝑦) ∈ V |
4 | | 1stexg 6167 |
. . . . . 6
⊢ (𝑦 ∈ V → (1st
‘𝑦) ∈
V) |
5 | 4 | elv 2741 |
. . . . 5
⊢
(1st ‘𝑦) ∈ V |
6 | | vex 2740 |
. . . . . . . 8
⊢ 𝑗 ∈ V |
7 | | vex 2740 |
. . . . . . . 8
⊢ 𝑘 ∈ V |
8 | 6, 7 | opex 4229 |
. . . . . . 7
⊢
⟨𝑗, 𝑘⟩ ∈ V |
9 | | fsumcnv.1 |
. . . . . . 7
⊢ (𝑥 = ⟨𝑗, 𝑘⟩ → 𝐵 = 𝐷) |
10 | 8, 9 | csbie 3102 |
. . . . . 6
⊢
⦋⟨𝑗, 𝑘⟩ / 𝑥⦌𝐵 = 𝐷 |
11 | | opeq12 3780 |
. . . . . . 7
⊢ ((𝑗 = (2nd ‘𝑦) ∧ 𝑘 = (1st ‘𝑦)) → ⟨𝑗, 𝑘⟩ = ⟨(2nd ‘𝑦), (1st ‘𝑦)⟩) |
12 | 11 | csbeq1d 3064 |
. . . . . 6
⊢ ((𝑗 = (2nd ‘𝑦) ∧ 𝑘 = (1st ‘𝑦)) → ⦋⟨𝑗, 𝑘⟩ / 𝑥⦌𝐵 = ⦋⟨(2nd
‘𝑦), (1st
‘𝑦)⟩ / 𝑥⦌𝐵) |
13 | 10, 12 | eqtr3id 2224 |
. . . . 5
⊢ ((𝑗 = (2nd ‘𝑦) ∧ 𝑘 = (1st ‘𝑦)) → 𝐷 = ⦋⟨(2nd
‘𝑦), (1st
‘𝑦)⟩ / 𝑥⦌𝐵) |
14 | 3, 5, 13 | csbie2 3106 |
. . . 4
⊢
⦋(2nd ‘𝑦) / 𝑗⦌⦋(1st
‘𝑦) / 𝑘⦌𝐷 = ⦋⟨(2nd
‘𝑦), (1st
‘𝑦)⟩ / 𝑥⦌𝐵 |
15 | 1, 14 | eqtr4di 2228 |
. . 3
⊢ (𝑥 = ⟨(2nd
‘𝑦), (1st
‘𝑦)⟩ →
𝐵 =
⦋(2nd ‘𝑦) / 𝑗⦌⦋(1st
‘𝑦) / 𝑘⦌𝐷) |
16 | | fsumcnv.4 |
. . . 4
⊢ (𝜑 → Rel 𝐴) |
17 | | fsumcnv.3 |
. . . 4
⊢ (𝜑 → 𝐴 ∈ Fin) |
18 | | relcnvfi 6939 |
. . . 4
⊢ ((Rel
𝐴 ∧ 𝐴 ∈ Fin) → ◡𝐴 ∈ Fin) |
19 | 16, 17, 18 | syl2anc 411 |
. . 3
⊢ (𝜑 → ◡𝐴 ∈ Fin) |
20 | | relcnv 5006 |
. . . . 5
⊢ Rel ◡𝐴 |
21 | | cnvf1o 6225 |
. . . . 5
⊢ (Rel
◡𝐴 → (𝑧 ∈ ◡𝐴 ↦ ∪ ◡{𝑧}):◡𝐴–1-1-onto→◡◡𝐴) |
22 | 20, 21 | ax-mp 5 |
. . . 4
⊢ (𝑧 ∈ ◡𝐴 ↦ ∪ ◡{𝑧}):◡𝐴–1-1-onto→◡◡𝐴 |
23 | | dfrel2 5079 |
. . . . . 6
⊢ (Rel
𝐴 ↔ ◡◡𝐴 = 𝐴) |
24 | 16, 23 | sylib 122 |
. . . . 5
⊢ (𝜑 → ◡◡𝐴 = 𝐴) |
25 | | f1oeq3 5451 |
. . . . 5
⊢ (◡◡𝐴 = 𝐴 → ((𝑧 ∈ ◡𝐴 ↦ ∪ ◡{𝑧}):◡𝐴–1-1-onto→◡◡𝐴 ↔ (𝑧 ∈ ◡𝐴 ↦ ∪ ◡{𝑧}):◡𝐴–1-1-onto→𝐴)) |
26 | 24, 25 | syl 14 |
. . . 4
⊢ (𝜑 → ((𝑧 ∈ ◡𝐴 ↦ ∪ ◡{𝑧}):◡𝐴–1-1-onto→◡◡𝐴 ↔ (𝑧 ∈ ◡𝐴 ↦ ∪ ◡{𝑧}):◡𝐴–1-1-onto→𝐴)) |
27 | 22, 26 | mpbii 148 |
. . 3
⊢ (𝜑 → (𝑧 ∈ ◡𝐴 ↦ ∪ ◡{𝑧}):◡𝐴–1-1-onto→𝐴) |
28 | | 1st2nd 6181 |
. . . . . . 7
⊢ ((Rel
◡𝐴 ∧ 𝑦 ∈ ◡𝐴) → 𝑦 = ⟨(1st ‘𝑦), (2nd ‘𝑦)⟩) |
29 | 20, 28 | mpan 424 |
. . . . . 6
⊢ (𝑦 ∈ ◡𝐴 → 𝑦 = ⟨(1st ‘𝑦), (2nd ‘𝑦)⟩) |
30 | 29 | fveq2d 5519 |
. . . . 5
⊢ (𝑦 ∈ ◡𝐴 → ((𝑧 ∈ ◡𝐴 ↦ ∪ ◡{𝑧})‘𝑦) = ((𝑧 ∈ ◡𝐴 ↦ ∪ ◡{𝑧})‘⟨(1st ‘𝑦), (2nd ‘𝑦)⟩)) |
31 | | id 19 |
. . . . . . 7
⊢ (𝑦 ∈ ◡𝐴 → 𝑦 ∈ ◡𝐴) |
32 | 29, 31 | eqeltrrd 2255 |
. . . . . 6
⊢ (𝑦 ∈ ◡𝐴 → ⟨(1st ‘𝑦), (2nd ‘𝑦)⟩ ∈ ◡𝐴) |
33 | | sneq 3603 |
. . . . . . . . . 10
⊢ (𝑧 = ⟨(1st
‘𝑦), (2nd
‘𝑦)⟩ →
{𝑧} =
{⟨(1st ‘𝑦), (2nd ‘𝑦)⟩}) |
34 | 33 | cnveqd 4803 |
. . . . . . . . 9
⊢ (𝑧 = ⟨(1st
‘𝑦), (2nd
‘𝑦)⟩ →
◡{𝑧} = ◡{⟨(1st ‘𝑦), (2nd ‘𝑦)⟩}) |
35 | 34 | unieqd 3820 |
. . . . . . . 8
⊢ (𝑧 = ⟨(1st
‘𝑦), (2nd
‘𝑦)⟩ →
∪ ◡{𝑧} = ∪
◡{⟨(1st ‘𝑦), (2nd ‘𝑦)⟩}) |
36 | | opswapg 5115 |
. . . . . . . . 9
⊢
(((1st ‘𝑦) ∈ V ∧ (2nd ‘𝑦) ∈ V) → ∪ ◡{⟨(1st ‘𝑦), (2nd ‘𝑦)⟩} = ⟨(2nd
‘𝑦), (1st
‘𝑦)⟩) |
37 | 5, 3, 36 | mp2an 426 |
. . . . . . . 8
⊢ ∪ ◡{⟨(1st ‘𝑦), (2nd ‘𝑦)⟩} = ⟨(2nd
‘𝑦), (1st
‘𝑦)⟩ |
38 | 35, 37 | eqtrdi 2226 |
. . . . . . 7
⊢ (𝑧 = ⟨(1st
‘𝑦), (2nd
‘𝑦)⟩ →
∪ ◡{𝑧} = ⟨(2nd
‘𝑦), (1st
‘𝑦)⟩) |
39 | | eqid 2177 |
. . . . . . 7
⊢ (𝑧 ∈ ◡𝐴 ↦ ∪ ◡{𝑧}) = (𝑧 ∈ ◡𝐴 ↦ ∪ ◡{𝑧}) |
40 | 3, 5 | opex 4229 |
. . . . . . 7
⊢
⟨(2nd ‘𝑦), (1st ‘𝑦)⟩ ∈ V |
41 | 38, 39, 40 | fvmpt 5593 |
. . . . . 6
⊢
(⟨(1st ‘𝑦), (2nd ‘𝑦)⟩ ∈ ◡𝐴 → ((𝑧 ∈ ◡𝐴 ↦ ∪ ◡{𝑧})‘⟨(1st ‘𝑦), (2nd ‘𝑦)⟩) = ⟨(2nd
‘𝑦), (1st
‘𝑦)⟩) |
42 | 32, 41 | syl 14 |
. . . . 5
⊢ (𝑦 ∈ ◡𝐴 → ((𝑧 ∈ ◡𝐴 ↦ ∪ ◡{𝑧})‘⟨(1st ‘𝑦), (2nd ‘𝑦)⟩) = ⟨(2nd
‘𝑦), (1st
‘𝑦)⟩) |
43 | 30, 42 | eqtrd 2210 |
. . . 4
⊢ (𝑦 ∈ ◡𝐴 → ((𝑧 ∈ ◡𝐴 ↦ ∪ ◡{𝑧})‘𝑦) = ⟨(2nd ‘𝑦), (1st ‘𝑦)⟩) |
44 | 43 | adantl 277 |
. . 3
⊢ ((𝜑 ∧ 𝑦 ∈ ◡𝐴) → ((𝑧 ∈ ◡𝐴 ↦ ∪ ◡{𝑧})‘𝑦) = ⟨(2nd ‘𝑦), (1st ‘𝑦)⟩) |
45 | | fsumcnv.5 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℂ) |
46 | 15, 19, 27, 44, 45 | fsumf1o 11397 |
. 2
⊢ (𝜑 → Σ𝑥 ∈ 𝐴 𝐵 = Σ𝑦 ∈ ◡ 𝐴⦋(2nd ‘𝑦) / 𝑗⦌⦋(1st
‘𝑦) / 𝑘⦌𝐷) |
47 | | csbeq1a 3066 |
. . . . 5
⊢ (𝑦 = ⟨(1st
‘𝑦), (2nd
‘𝑦)⟩ →
𝐶 =
⦋⟨(1st ‘𝑦), (2nd ‘𝑦)⟩ / 𝑦⦌𝐶) |
48 | 29, 47 | syl 14 |
. . . 4
⊢ (𝑦 ∈ ◡𝐴 → 𝐶 = ⦋⟨(1st
‘𝑦), (2nd
‘𝑦)⟩ / 𝑦⦌𝐶) |
49 | 7, 6 | opex 4229 |
. . . . . . 7
⊢
⟨𝑘, 𝑗⟩ ∈ V |
50 | | fsumcnv.2 |
. . . . . . 7
⊢ (𝑦 = ⟨𝑘, 𝑗⟩ → 𝐶 = 𝐷) |
51 | 49, 50 | csbie 3102 |
. . . . . 6
⊢
⦋⟨𝑘, 𝑗⟩ / 𝑦⦌𝐶 = 𝐷 |
52 | | opeq12 3780 |
. . . . . . . 8
⊢ ((𝑘 = (1st ‘𝑦) ∧ 𝑗 = (2nd ‘𝑦)) → ⟨𝑘, 𝑗⟩ = ⟨(1st ‘𝑦), (2nd ‘𝑦)⟩) |
53 | 52 | ancoms 268 |
. . . . . . 7
⊢ ((𝑗 = (2nd ‘𝑦) ∧ 𝑘 = (1st ‘𝑦)) → ⟨𝑘, 𝑗⟩ = ⟨(1st ‘𝑦), (2nd ‘𝑦)⟩) |
54 | 53 | csbeq1d 3064 |
. . . . . 6
⊢ ((𝑗 = (2nd ‘𝑦) ∧ 𝑘 = (1st ‘𝑦)) → ⦋⟨𝑘, 𝑗⟩ / 𝑦⦌𝐶 = ⦋⟨(1st
‘𝑦), (2nd
‘𝑦)⟩ / 𝑦⦌𝐶) |
55 | 51, 54 | eqtr3id 2224 |
. . . . 5
⊢ ((𝑗 = (2nd ‘𝑦) ∧ 𝑘 = (1st ‘𝑦)) → 𝐷 = ⦋⟨(1st
‘𝑦), (2nd
‘𝑦)⟩ / 𝑦⦌𝐶) |
56 | 3, 5, 55 | csbie2 3106 |
. . . 4
⊢
⦋(2nd ‘𝑦) / 𝑗⦌⦋(1st
‘𝑦) / 𝑘⦌𝐷 = ⦋⟨(1st
‘𝑦), (2nd
‘𝑦)⟩ / 𝑦⦌𝐶 |
57 | 48, 56 | eqtr4di 2228 |
. . 3
⊢ (𝑦 ∈ ◡𝐴 → 𝐶 = ⦋(2nd
‘𝑦) / 𝑗⦌⦋(1st
‘𝑦) / 𝑘⦌𝐷) |
58 | 57 | sumeq2i 11371 |
. 2
⊢
Σ𝑦 ∈
◡ 𝐴𝐶 = Σ𝑦 ∈ ◡ 𝐴⦋(2nd ‘𝑦) / 𝑗⦌⦋(1st
‘𝑦) / 𝑘⦌𝐷 |
59 | 46, 58 | eqtr4di 2228 |
1
⊢ (𝜑 → Σ𝑥 ∈ 𝐴 𝐵 = Σ𝑦 ∈ ◡ 𝐴𝐶) |