Step | Hyp | Ref
| Expression |
1 | | csbeq1a 3851 |
. . . 4
⊢ (𝑥 = 〈(2nd
‘𝑦), (1st
‘𝑦)〉 →
𝐵 =
⦋〈(2nd ‘𝑦), (1st ‘𝑦)〉 / 𝑥⦌𝐵) |
2 | | fvex 6784 |
. . . . 5
⊢
(2nd ‘𝑦) ∈ V |
3 | | fvex 6784 |
. . . . 5
⊢
(1st ‘𝑦) ∈ V |
4 | | opex 5383 |
. . . . . . 7
⊢
〈𝑗, 𝑘〉 ∈ V |
5 | | fsumcnv.1 |
. . . . . . 7
⊢ (𝑥 = 〈𝑗, 𝑘〉 → 𝐵 = 𝐷) |
6 | 4, 5 | csbie 3873 |
. . . . . 6
⊢
⦋〈𝑗, 𝑘〉 / 𝑥⦌𝐵 = 𝐷 |
7 | | opeq12 4812 |
. . . . . . 7
⊢ ((𝑗 = (2nd ‘𝑦) ∧ 𝑘 = (1st ‘𝑦)) → 〈𝑗, 𝑘〉 = 〈(2nd ‘𝑦), (1st ‘𝑦)〉) |
8 | 7 | csbeq1d 3841 |
. . . . . 6
⊢ ((𝑗 = (2nd ‘𝑦) ∧ 𝑘 = (1st ‘𝑦)) → ⦋〈𝑗, 𝑘〉 / 𝑥⦌𝐵 = ⦋〈(2nd
‘𝑦), (1st
‘𝑦)〉 / 𝑥⦌𝐵) |
9 | 6, 8 | eqtr3id 2794 |
. . . . 5
⊢ ((𝑗 = (2nd ‘𝑦) ∧ 𝑘 = (1st ‘𝑦)) → 𝐷 = ⦋〈(2nd
‘𝑦), (1st
‘𝑦)〉 / 𝑥⦌𝐵) |
10 | 2, 3, 9 | csbie2 3879 |
. . . 4
⊢
⦋(2nd ‘𝑦) / 𝑗⦌⦋(1st
‘𝑦) / 𝑘⦌𝐷 = ⦋〈(2nd
‘𝑦), (1st
‘𝑦)〉 / 𝑥⦌𝐵 |
11 | 1, 10 | eqtr4di 2798 |
. . 3
⊢ (𝑥 = 〈(2nd
‘𝑦), (1st
‘𝑦)〉 →
𝐵 =
⦋(2nd ‘𝑦) / 𝑗⦌⦋(1st
‘𝑦) / 𝑘⦌𝐷) |
12 | | fsumcnv.3 |
. . . 4
⊢ (𝜑 → 𝐴 ∈ Fin) |
13 | | cnvfi 8945 |
. . . 4
⊢ (𝐴 ∈ Fin → ◡𝐴 ∈ Fin) |
14 | 12, 13 | syl 17 |
. . 3
⊢ (𝜑 → ◡𝐴 ∈ Fin) |
15 | | relcnv 6011 |
. . . . 5
⊢ Rel ◡𝐴 |
16 | | cnvf1o 7942 |
. . . . 5
⊢ (Rel
◡𝐴 → (𝑧 ∈ ◡𝐴 ↦ ∪ ◡{𝑧}):◡𝐴–1-1-onto→◡◡𝐴) |
17 | 15, 16 | ax-mp 5 |
. . . 4
⊢ (𝑧 ∈ ◡𝐴 ↦ ∪ ◡{𝑧}):◡𝐴–1-1-onto→◡◡𝐴 |
18 | | fsumcnv.4 |
. . . . . 6
⊢ (𝜑 → Rel 𝐴) |
19 | | dfrel2 6091 |
. . . . . 6
⊢ (Rel
𝐴 ↔ ◡◡𝐴 = 𝐴) |
20 | 18, 19 | sylib 217 |
. . . . 5
⊢ (𝜑 → ◡◡𝐴 = 𝐴) |
21 | 20 | f1oeq3d 6711 |
. . . 4
⊢ (𝜑 → ((𝑧 ∈ ◡𝐴 ↦ ∪ ◡{𝑧}):◡𝐴–1-1-onto→◡◡𝐴 ↔ (𝑧 ∈ ◡𝐴 ↦ ∪ ◡{𝑧}):◡𝐴–1-1-onto→𝐴)) |
22 | 17, 21 | mpbii 232 |
. . 3
⊢ (𝜑 → (𝑧 ∈ ◡𝐴 ↦ ∪ ◡{𝑧}):◡𝐴–1-1-onto→𝐴) |
23 | | 1st2nd 7873 |
. . . . . . 7
⊢ ((Rel
◡𝐴 ∧ 𝑦 ∈ ◡𝐴) → 𝑦 = 〈(1st ‘𝑦), (2nd ‘𝑦)〉) |
24 | 15, 23 | mpan 687 |
. . . . . 6
⊢ (𝑦 ∈ ◡𝐴 → 𝑦 = 〈(1st ‘𝑦), (2nd ‘𝑦)〉) |
25 | 24 | fveq2d 6775 |
. . . . 5
⊢ (𝑦 ∈ ◡𝐴 → ((𝑧 ∈ ◡𝐴 ↦ ∪ ◡{𝑧})‘𝑦) = ((𝑧 ∈ ◡𝐴 ↦ ∪ ◡{𝑧})‘〈(1st ‘𝑦), (2nd ‘𝑦)〉)) |
26 | | id 22 |
. . . . . . 7
⊢ (𝑦 ∈ ◡𝐴 → 𝑦 ∈ ◡𝐴) |
27 | 24, 26 | eqeltrrd 2842 |
. . . . . 6
⊢ (𝑦 ∈ ◡𝐴 → 〈(1st ‘𝑦), (2nd ‘𝑦)〉 ∈ ◡𝐴) |
28 | | sneq 4577 |
. . . . . . . . . 10
⊢ (𝑧 = 〈(1st
‘𝑦), (2nd
‘𝑦)〉 →
{𝑧} =
{〈(1st ‘𝑦), (2nd ‘𝑦)〉}) |
29 | 28 | cnveqd 5783 |
. . . . . . . . 9
⊢ (𝑧 = 〈(1st
‘𝑦), (2nd
‘𝑦)〉 →
◡{𝑧} = ◡{〈(1st ‘𝑦), (2nd ‘𝑦)〉}) |
30 | 29 | unieqd 4859 |
. . . . . . . 8
⊢ (𝑧 = 〈(1st
‘𝑦), (2nd
‘𝑦)〉 →
∪ ◡{𝑧} = ∪
◡{〈(1st ‘𝑦), (2nd ‘𝑦)〉}) |
31 | | opswap 6131 |
. . . . . . . 8
⊢ ∪ ◡{〈(1st ‘𝑦), (2nd ‘𝑦)〉} = 〈(2nd
‘𝑦), (1st
‘𝑦)〉 |
32 | 30, 31 | eqtrdi 2796 |
. . . . . . 7
⊢ (𝑧 = 〈(1st
‘𝑦), (2nd
‘𝑦)〉 →
∪ ◡{𝑧} = 〈(2nd
‘𝑦), (1st
‘𝑦)〉) |
33 | | eqid 2740 |
. . . . . . 7
⊢ (𝑧 ∈ ◡𝐴 ↦ ∪ ◡{𝑧}) = (𝑧 ∈ ◡𝐴 ↦ ∪ ◡{𝑧}) |
34 | | opex 5383 |
. . . . . . 7
⊢
〈(2nd ‘𝑦), (1st ‘𝑦)〉 ∈ V |
35 | 32, 33, 34 | fvmpt 6872 |
. . . . . 6
⊢
(〈(1st ‘𝑦), (2nd ‘𝑦)〉 ∈ ◡𝐴 → ((𝑧 ∈ ◡𝐴 ↦ ∪ ◡{𝑧})‘〈(1st ‘𝑦), (2nd ‘𝑦)〉) = 〈(2nd
‘𝑦), (1st
‘𝑦)〉) |
36 | 27, 35 | syl 17 |
. . . . 5
⊢ (𝑦 ∈ ◡𝐴 → ((𝑧 ∈ ◡𝐴 ↦ ∪ ◡{𝑧})‘〈(1st ‘𝑦), (2nd ‘𝑦)〉) = 〈(2nd
‘𝑦), (1st
‘𝑦)〉) |
37 | 25, 36 | eqtrd 2780 |
. . . 4
⊢ (𝑦 ∈ ◡𝐴 → ((𝑧 ∈ ◡𝐴 ↦ ∪ ◡{𝑧})‘𝑦) = 〈(2nd ‘𝑦), (1st ‘𝑦)〉) |
38 | 37 | adantl 482 |
. . 3
⊢ ((𝜑 ∧ 𝑦 ∈ ◡𝐴) → ((𝑧 ∈ ◡𝐴 ↦ ∪ ◡{𝑧})‘𝑦) = 〈(2nd ‘𝑦), (1st ‘𝑦)〉) |
39 | | fsumcnv.5 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℂ) |
40 | 11, 14, 22, 38, 39 | fsumf1o 15433 |
. 2
⊢ (𝜑 → Σ𝑥 ∈ 𝐴 𝐵 = Σ𝑦 ∈ ◡ 𝐴⦋(2nd ‘𝑦) / 𝑗⦌⦋(1st
‘𝑦) / 𝑘⦌𝐷) |
41 | | csbeq1a 3851 |
. . . . 5
⊢ (𝑦 = 〈(1st
‘𝑦), (2nd
‘𝑦)〉 →
𝐶 =
⦋〈(1st ‘𝑦), (2nd ‘𝑦)〉 / 𝑦⦌𝐶) |
42 | 24, 41 | syl 17 |
. . . 4
⊢ (𝑦 ∈ ◡𝐴 → 𝐶 = ⦋〈(1st
‘𝑦), (2nd
‘𝑦)〉 / 𝑦⦌𝐶) |
43 | | opex 5383 |
. . . . . . 7
⊢
〈𝑘, 𝑗〉 ∈ V |
44 | | fsumcnv.2 |
. . . . . . 7
⊢ (𝑦 = 〈𝑘, 𝑗〉 → 𝐶 = 𝐷) |
45 | 43, 44 | csbie 3873 |
. . . . . 6
⊢
⦋〈𝑘, 𝑗〉 / 𝑦⦌𝐶 = 𝐷 |
46 | | opeq12 4812 |
. . . . . . . 8
⊢ ((𝑘 = (1st ‘𝑦) ∧ 𝑗 = (2nd ‘𝑦)) → 〈𝑘, 𝑗〉 = 〈(1st ‘𝑦), (2nd ‘𝑦)〉) |
47 | 46 | ancoms 459 |
. . . . . . 7
⊢ ((𝑗 = (2nd ‘𝑦) ∧ 𝑘 = (1st ‘𝑦)) → 〈𝑘, 𝑗〉 = 〈(1st ‘𝑦), (2nd ‘𝑦)〉) |
48 | 47 | csbeq1d 3841 |
. . . . . 6
⊢ ((𝑗 = (2nd ‘𝑦) ∧ 𝑘 = (1st ‘𝑦)) → ⦋〈𝑘, 𝑗〉 / 𝑦⦌𝐶 = ⦋〈(1st
‘𝑦), (2nd
‘𝑦)〉 / 𝑦⦌𝐶) |
49 | 45, 48 | eqtr3id 2794 |
. . . . 5
⊢ ((𝑗 = (2nd ‘𝑦) ∧ 𝑘 = (1st ‘𝑦)) → 𝐷 = ⦋〈(1st
‘𝑦), (2nd
‘𝑦)〉 / 𝑦⦌𝐶) |
50 | 2, 3, 49 | csbie2 3879 |
. . . 4
⊢
⦋(2nd ‘𝑦) / 𝑗⦌⦋(1st
‘𝑦) / 𝑘⦌𝐷 = ⦋〈(1st
‘𝑦), (2nd
‘𝑦)〉 / 𝑦⦌𝐶 |
51 | 42, 50 | eqtr4di 2798 |
. . 3
⊢ (𝑦 ∈ ◡𝐴 → 𝐶 = ⦋(2nd
‘𝑦) / 𝑗⦌⦋(1st
‘𝑦) / 𝑘⦌𝐷) |
52 | 51 | sumeq2i 15409 |
. 2
⊢
Σ𝑦 ∈
◡ 𝐴𝐶 = Σ𝑦 ∈ ◡ 𝐴⦋(2nd ‘𝑦) / 𝑗⦌⦋(1st
‘𝑦) / 𝑘⦌𝐷 |
53 | 40, 52 | eqtr4di 2798 |
1
⊢ (𝜑 → Σ𝑥 ∈ 𝐴 𝐵 = Σ𝑦 ∈ ◡ 𝐴𝐶) |