| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | csbeq1a 3913 | . . . 4
⊢ (𝑘 = 𝑖 → 𝐵 = ⦋𝑖 / 𝑘⦌𝐵) | 
| 2 |  | nfcv 2905 | . . . 4
⊢
Ⅎ𝑖𝐵 | 
| 3 |  | nfcsb1v 3923 | . . . 4
⊢
Ⅎ𝑘⦋𝑖 / 𝑘⦌𝐵 | 
| 4 | 1, 2, 3 | cbvsum 15731 | . . 3
⊢
Σ𝑘 ∈
𝐴 𝐵 = Σ𝑖 ∈ 𝐴 ⦋𝑖 / 𝑘⦌𝐵 | 
| 5 | 4 | a1i 11 | . 2
⊢ (𝜑 → Σ𝑘 ∈ 𝐴 𝐵 = Σ𝑖 ∈ 𝐴 ⦋𝑖 / 𝑘⦌𝐵) | 
| 6 |  | nfv 1914 | . . . . 5
⊢
Ⅎ𝑘 𝑖 = ⦋𝑗 / 𝑛⦌𝐺 | 
| 7 |  | nfcv 2905 | . . . . . 6
⊢
Ⅎ𝑘⦋𝑗 / 𝑛⦌𝐷 | 
| 8 | 3, 7 | nfeq 2919 | . . . . 5
⊢
Ⅎ𝑘⦋𝑖 / 𝑘⦌𝐵 = ⦋𝑗 / 𝑛⦌𝐷 | 
| 9 | 6, 8 | nfim 1896 | . . . 4
⊢
Ⅎ𝑘(𝑖 = ⦋𝑗 / 𝑛⦌𝐺 → ⦋𝑖 / 𝑘⦌𝐵 = ⦋𝑗 / 𝑛⦌𝐷) | 
| 10 |  | eqeq1 2741 | . . . . 5
⊢ (𝑘 = 𝑖 → (𝑘 = ⦋𝑗 / 𝑛⦌𝐺 ↔ 𝑖 = ⦋𝑗 / 𝑛⦌𝐺)) | 
| 11 | 1 | eqeq1d 2739 | . . . . 5
⊢ (𝑘 = 𝑖 → (𝐵 = ⦋𝑗 / 𝑛⦌𝐷 ↔ ⦋𝑖 / 𝑘⦌𝐵 = ⦋𝑗 / 𝑛⦌𝐷)) | 
| 12 | 10, 11 | imbi12d 344 | . . . 4
⊢ (𝑘 = 𝑖 → ((𝑘 = ⦋𝑗 / 𝑛⦌𝐺 → 𝐵 = ⦋𝑗 / 𝑛⦌𝐷) ↔ (𝑖 = ⦋𝑗 / 𝑛⦌𝐺 → ⦋𝑖 / 𝑘⦌𝐵 = ⦋𝑗 / 𝑛⦌𝐷))) | 
| 13 |  | nfcv 2905 | . . . . . . 7
⊢
Ⅎ𝑛𝑘 | 
| 14 |  | nfcsb1v 3923 | . . . . . . 7
⊢
Ⅎ𝑛⦋𝑗 / 𝑛⦌𝐺 | 
| 15 | 13, 14 | nfeq 2919 | . . . . . 6
⊢
Ⅎ𝑛 𝑘 = ⦋𝑗 / 𝑛⦌𝐺 | 
| 16 |  | nfcv 2905 | . . . . . . 7
⊢
Ⅎ𝑛𝐵 | 
| 17 |  | nfcsb1v 3923 | . . . . . . 7
⊢
Ⅎ𝑛⦋𝑗 / 𝑛⦌𝐷 | 
| 18 | 16, 17 | nfeq 2919 | . . . . . 6
⊢
Ⅎ𝑛 𝐵 = ⦋𝑗 / 𝑛⦌𝐷 | 
| 19 | 15, 18 | nfim 1896 | . . . . 5
⊢
Ⅎ𝑛(𝑘 = ⦋𝑗 / 𝑛⦌𝐺 → 𝐵 = ⦋𝑗 / 𝑛⦌𝐷) | 
| 20 |  | csbeq1a 3913 | . . . . . . 7
⊢ (𝑛 = 𝑗 → 𝐺 = ⦋𝑗 / 𝑛⦌𝐺) | 
| 21 | 20 | eqeq2d 2748 | . . . . . 6
⊢ (𝑛 = 𝑗 → (𝑘 = 𝐺 ↔ 𝑘 = ⦋𝑗 / 𝑛⦌𝐺)) | 
| 22 |  | csbeq1a 3913 | . . . . . . 7
⊢ (𝑛 = 𝑗 → 𝐷 = ⦋𝑗 / 𝑛⦌𝐷) | 
| 23 | 22 | eqeq2d 2748 | . . . . . 6
⊢ (𝑛 = 𝑗 → (𝐵 = 𝐷 ↔ 𝐵 = ⦋𝑗 / 𝑛⦌𝐷)) | 
| 24 | 21, 23 | imbi12d 344 | . . . . 5
⊢ (𝑛 = 𝑗 → ((𝑘 = 𝐺 → 𝐵 = 𝐷) ↔ (𝑘 = ⦋𝑗 / 𝑛⦌𝐺 → 𝐵 = ⦋𝑗 / 𝑛⦌𝐷))) | 
| 25 |  | fsumf1of.3 | . . . . 5
⊢ (𝑘 = 𝐺 → 𝐵 = 𝐷) | 
| 26 | 19, 24, 25 | chvarfv 2240 | . . . 4
⊢ (𝑘 = ⦋𝑗 / 𝑛⦌𝐺 → 𝐵 = ⦋𝑗 / 𝑛⦌𝐷) | 
| 27 | 9, 12, 26 | chvarfv 2240 | . . 3
⊢ (𝑖 = ⦋𝑗 / 𝑛⦌𝐺 → ⦋𝑖 / 𝑘⦌𝐵 = ⦋𝑗 / 𝑛⦌𝐷) | 
| 28 |  | fsumf1of.4 | . . 3
⊢ (𝜑 → 𝐶 ∈ Fin) | 
| 29 |  | fsumf1of.5 | . . 3
⊢ (𝜑 → 𝐹:𝐶–1-1-onto→𝐴) | 
| 30 |  | fsumf1of.2 | . . . . . 6
⊢
Ⅎ𝑛𝜑 | 
| 31 |  | nfv 1914 | . . . . . 6
⊢
Ⅎ𝑛 𝑗 ∈ 𝐶 | 
| 32 | 30, 31 | nfan 1899 | . . . . 5
⊢
Ⅎ𝑛(𝜑 ∧ 𝑗 ∈ 𝐶) | 
| 33 |  | nfcv 2905 | . . . . . 6
⊢
Ⅎ𝑛(𝐹‘𝑗) | 
| 34 | 33, 14 | nfeq 2919 | . . . . 5
⊢
Ⅎ𝑛(𝐹‘𝑗) = ⦋𝑗 / 𝑛⦌𝐺 | 
| 35 | 32, 34 | nfim 1896 | . . . 4
⊢
Ⅎ𝑛((𝜑 ∧ 𝑗 ∈ 𝐶) → (𝐹‘𝑗) = ⦋𝑗 / 𝑛⦌𝐺) | 
| 36 |  | eleq1w 2824 | . . . . . 6
⊢ (𝑛 = 𝑗 → (𝑛 ∈ 𝐶 ↔ 𝑗 ∈ 𝐶)) | 
| 37 | 36 | anbi2d 630 | . . . . 5
⊢ (𝑛 = 𝑗 → ((𝜑 ∧ 𝑛 ∈ 𝐶) ↔ (𝜑 ∧ 𝑗 ∈ 𝐶))) | 
| 38 |  | fveq2 6906 | . . . . . 6
⊢ (𝑛 = 𝑗 → (𝐹‘𝑛) = (𝐹‘𝑗)) | 
| 39 | 38, 20 | eqeq12d 2753 | . . . . 5
⊢ (𝑛 = 𝑗 → ((𝐹‘𝑛) = 𝐺 ↔ (𝐹‘𝑗) = ⦋𝑗 / 𝑛⦌𝐺)) | 
| 40 | 37, 39 | imbi12d 344 | . . . 4
⊢ (𝑛 = 𝑗 → (((𝜑 ∧ 𝑛 ∈ 𝐶) → (𝐹‘𝑛) = 𝐺) ↔ ((𝜑 ∧ 𝑗 ∈ 𝐶) → (𝐹‘𝑗) = ⦋𝑗 / 𝑛⦌𝐺))) | 
| 41 |  | fsumf1of.6 | . . . 4
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶) → (𝐹‘𝑛) = 𝐺) | 
| 42 | 35, 40, 41 | chvarfv 2240 | . . 3
⊢ ((𝜑 ∧ 𝑗 ∈ 𝐶) → (𝐹‘𝑗) = ⦋𝑗 / 𝑛⦌𝐺) | 
| 43 |  | fsumf1of.1 | . . . . . 6
⊢
Ⅎ𝑘𝜑 | 
| 44 |  | nfv 1914 | . . . . . 6
⊢
Ⅎ𝑘 𝑖 ∈ 𝐴 | 
| 45 | 43, 44 | nfan 1899 | . . . . 5
⊢
Ⅎ𝑘(𝜑 ∧ 𝑖 ∈ 𝐴) | 
| 46 | 3 | nfel1 2922 | . . . . 5
⊢
Ⅎ𝑘⦋𝑖 / 𝑘⦌𝐵 ∈ ℂ | 
| 47 | 45, 46 | nfim 1896 | . . . 4
⊢
Ⅎ𝑘((𝜑 ∧ 𝑖 ∈ 𝐴) → ⦋𝑖 / 𝑘⦌𝐵 ∈ ℂ) | 
| 48 |  | eleq1w 2824 | . . . . . 6
⊢ (𝑘 = 𝑖 → (𝑘 ∈ 𝐴 ↔ 𝑖 ∈ 𝐴)) | 
| 49 | 48 | anbi2d 630 | . . . . 5
⊢ (𝑘 = 𝑖 → ((𝜑 ∧ 𝑘 ∈ 𝐴) ↔ (𝜑 ∧ 𝑖 ∈ 𝐴))) | 
| 50 | 1 | eleq1d 2826 | . . . . 5
⊢ (𝑘 = 𝑖 → (𝐵 ∈ ℂ ↔ ⦋𝑖 / 𝑘⦌𝐵 ∈ ℂ)) | 
| 51 | 49, 50 | imbi12d 344 | . . . 4
⊢ (𝑘 = 𝑖 → (((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ) ↔ ((𝜑 ∧ 𝑖 ∈ 𝐴) → ⦋𝑖 / 𝑘⦌𝐵 ∈ ℂ))) | 
| 52 |  | fsumf1of.7 | . . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ) | 
| 53 | 47, 51, 52 | chvarfv 2240 | . . 3
⊢ ((𝜑 ∧ 𝑖 ∈ 𝐴) → ⦋𝑖 / 𝑘⦌𝐵 ∈ ℂ) | 
| 54 | 27, 28, 29, 42, 53 | fsumf1o 15759 | . 2
⊢ (𝜑 → Σ𝑖 ∈ 𝐴 ⦋𝑖 / 𝑘⦌𝐵 = Σ𝑗 ∈ 𝐶 ⦋𝑗 / 𝑛⦌𝐷) | 
| 55 |  | nfcv 2905 | . . . . 5
⊢
Ⅎ𝑗𝐷 | 
| 56 | 22, 55, 17 | cbvsum 15731 | . . . 4
⊢
Σ𝑛 ∈
𝐶 𝐷 = Σ𝑗 ∈ 𝐶 ⦋𝑗 / 𝑛⦌𝐷 | 
| 57 | 56 | eqcomi 2746 | . . 3
⊢
Σ𝑗 ∈
𝐶 ⦋𝑗 / 𝑛⦌𝐷 = Σ𝑛 ∈ 𝐶 𝐷 | 
| 58 | 57 | a1i 11 | . 2
⊢ (𝜑 → Σ𝑗 ∈ 𝐶 ⦋𝑗 / 𝑛⦌𝐷 = Σ𝑛 ∈ 𝐶 𝐷) | 
| 59 | 5, 54, 58 | 3eqtrd 2781 | 1
⊢ (𝜑 → Σ𝑘 ∈ 𝐴 𝐵 = Σ𝑛 ∈ 𝐶 𝐷) |