Step | Hyp | Ref
| Expression |
1 | | csbeq1a 3825 |
. . . 4
⊢ (𝑘 = 𝑖 → 𝐵 = ⦋𝑖 / 𝑘⦌𝐵) |
2 | | nfcv 2904 |
. . . 4
⊢
Ⅎ𝑖𝐴 |
3 | | nfcv 2904 |
. . . 4
⊢
Ⅎ𝑘𝐴 |
4 | | nfcv 2904 |
. . . 4
⊢
Ⅎ𝑖𝐵 |
5 | | nfcsb1v 3836 |
. . . 4
⊢
Ⅎ𝑘⦋𝑖 / 𝑘⦌𝐵 |
6 | 1, 2, 3, 4, 5 | cbvsum 15259 |
. . 3
⊢
Σ𝑘 ∈
𝐴 𝐵 = Σ𝑖 ∈ 𝐴 ⦋𝑖 / 𝑘⦌𝐵 |
7 | 6 | a1i 11 |
. 2
⊢ (𝜑 → Σ𝑘 ∈ 𝐴 𝐵 = Σ𝑖 ∈ 𝐴 ⦋𝑖 / 𝑘⦌𝐵) |
8 | | nfv 1922 |
. . . . 5
⊢
Ⅎ𝑘 𝑖 = ⦋𝑗 / 𝑛⦌𝐺 |
9 | | nfcv 2904 |
. . . . . 6
⊢
Ⅎ𝑘⦋𝑗 / 𝑛⦌𝐷 |
10 | 5, 9 | nfeq 2917 |
. . . . 5
⊢
Ⅎ𝑘⦋𝑖 / 𝑘⦌𝐵 = ⦋𝑗 / 𝑛⦌𝐷 |
11 | 8, 10 | nfim 1904 |
. . . 4
⊢
Ⅎ𝑘(𝑖 = ⦋𝑗 / 𝑛⦌𝐺 → ⦋𝑖 / 𝑘⦌𝐵 = ⦋𝑗 / 𝑛⦌𝐷) |
12 | | eqeq1 2741 |
. . . . 5
⊢ (𝑘 = 𝑖 → (𝑘 = ⦋𝑗 / 𝑛⦌𝐺 ↔ 𝑖 = ⦋𝑗 / 𝑛⦌𝐺)) |
13 | 1 | eqeq1d 2739 |
. . . . 5
⊢ (𝑘 = 𝑖 → (𝐵 = ⦋𝑗 / 𝑛⦌𝐷 ↔ ⦋𝑖 / 𝑘⦌𝐵 = ⦋𝑗 / 𝑛⦌𝐷)) |
14 | 12, 13 | imbi12d 348 |
. . . 4
⊢ (𝑘 = 𝑖 → ((𝑘 = ⦋𝑗 / 𝑛⦌𝐺 → 𝐵 = ⦋𝑗 / 𝑛⦌𝐷) ↔ (𝑖 = ⦋𝑗 / 𝑛⦌𝐺 → ⦋𝑖 / 𝑘⦌𝐵 = ⦋𝑗 / 𝑛⦌𝐷))) |
15 | | nfcv 2904 |
. . . . . . 7
⊢
Ⅎ𝑛𝑘 |
16 | | nfcsb1v 3836 |
. . . . . . 7
⊢
Ⅎ𝑛⦋𝑗 / 𝑛⦌𝐺 |
17 | 15, 16 | nfeq 2917 |
. . . . . 6
⊢
Ⅎ𝑛 𝑘 = ⦋𝑗 / 𝑛⦌𝐺 |
18 | | nfcv 2904 |
. . . . . . 7
⊢
Ⅎ𝑛𝐵 |
19 | | nfcsb1v 3836 |
. . . . . . 7
⊢
Ⅎ𝑛⦋𝑗 / 𝑛⦌𝐷 |
20 | 18, 19 | nfeq 2917 |
. . . . . 6
⊢
Ⅎ𝑛 𝐵 = ⦋𝑗 / 𝑛⦌𝐷 |
21 | 17, 20 | nfim 1904 |
. . . . 5
⊢
Ⅎ𝑛(𝑘 = ⦋𝑗 / 𝑛⦌𝐺 → 𝐵 = ⦋𝑗 / 𝑛⦌𝐷) |
22 | | csbeq1a 3825 |
. . . . . . 7
⊢ (𝑛 = 𝑗 → 𝐺 = ⦋𝑗 / 𝑛⦌𝐺) |
23 | 22 | eqeq2d 2748 |
. . . . . 6
⊢ (𝑛 = 𝑗 → (𝑘 = 𝐺 ↔ 𝑘 = ⦋𝑗 / 𝑛⦌𝐺)) |
24 | | csbeq1a 3825 |
. . . . . . 7
⊢ (𝑛 = 𝑗 → 𝐷 = ⦋𝑗 / 𝑛⦌𝐷) |
25 | 24 | eqeq2d 2748 |
. . . . . 6
⊢ (𝑛 = 𝑗 → (𝐵 = 𝐷 ↔ 𝐵 = ⦋𝑗 / 𝑛⦌𝐷)) |
26 | 23, 25 | imbi12d 348 |
. . . . 5
⊢ (𝑛 = 𝑗 → ((𝑘 = 𝐺 → 𝐵 = 𝐷) ↔ (𝑘 = ⦋𝑗 / 𝑛⦌𝐺 → 𝐵 = ⦋𝑗 / 𝑛⦌𝐷))) |
27 | | fsumf1of.3 |
. . . . 5
⊢ (𝑘 = 𝐺 → 𝐵 = 𝐷) |
28 | 21, 26, 27 | chvarfv 2238 |
. . . 4
⊢ (𝑘 = ⦋𝑗 / 𝑛⦌𝐺 → 𝐵 = ⦋𝑗 / 𝑛⦌𝐷) |
29 | 11, 14, 28 | chvarfv 2238 |
. . 3
⊢ (𝑖 = ⦋𝑗 / 𝑛⦌𝐺 → ⦋𝑖 / 𝑘⦌𝐵 = ⦋𝑗 / 𝑛⦌𝐷) |
30 | | fsumf1of.4 |
. . 3
⊢ (𝜑 → 𝐶 ∈ Fin) |
31 | | fsumf1of.5 |
. . 3
⊢ (𝜑 → 𝐹:𝐶–1-1-onto→𝐴) |
32 | | fsumf1of.2 |
. . . . . 6
⊢
Ⅎ𝑛𝜑 |
33 | | nfv 1922 |
. . . . . 6
⊢
Ⅎ𝑛 𝑗 ∈ 𝐶 |
34 | 32, 33 | nfan 1907 |
. . . . 5
⊢
Ⅎ𝑛(𝜑 ∧ 𝑗 ∈ 𝐶) |
35 | | nfcv 2904 |
. . . . . 6
⊢
Ⅎ𝑛(𝐹‘𝑗) |
36 | 35, 16 | nfeq 2917 |
. . . . 5
⊢
Ⅎ𝑛(𝐹‘𝑗) = ⦋𝑗 / 𝑛⦌𝐺 |
37 | 34, 36 | nfim 1904 |
. . . 4
⊢
Ⅎ𝑛((𝜑 ∧ 𝑗 ∈ 𝐶) → (𝐹‘𝑗) = ⦋𝑗 / 𝑛⦌𝐺) |
38 | | eleq1w 2820 |
. . . . . 6
⊢ (𝑛 = 𝑗 → (𝑛 ∈ 𝐶 ↔ 𝑗 ∈ 𝐶)) |
39 | 38 | anbi2d 632 |
. . . . 5
⊢ (𝑛 = 𝑗 → ((𝜑 ∧ 𝑛 ∈ 𝐶) ↔ (𝜑 ∧ 𝑗 ∈ 𝐶))) |
40 | | fveq2 6717 |
. . . . . 6
⊢ (𝑛 = 𝑗 → (𝐹‘𝑛) = (𝐹‘𝑗)) |
41 | 40, 22 | eqeq12d 2753 |
. . . . 5
⊢ (𝑛 = 𝑗 → ((𝐹‘𝑛) = 𝐺 ↔ (𝐹‘𝑗) = ⦋𝑗 / 𝑛⦌𝐺)) |
42 | 39, 41 | imbi12d 348 |
. . . 4
⊢ (𝑛 = 𝑗 → (((𝜑 ∧ 𝑛 ∈ 𝐶) → (𝐹‘𝑛) = 𝐺) ↔ ((𝜑 ∧ 𝑗 ∈ 𝐶) → (𝐹‘𝑗) = ⦋𝑗 / 𝑛⦌𝐺))) |
43 | | fsumf1of.6 |
. . . 4
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶) → (𝐹‘𝑛) = 𝐺) |
44 | 37, 42, 43 | chvarfv 2238 |
. . 3
⊢ ((𝜑 ∧ 𝑗 ∈ 𝐶) → (𝐹‘𝑗) = ⦋𝑗 / 𝑛⦌𝐺) |
45 | | fsumf1of.1 |
. . . . . 6
⊢
Ⅎ𝑘𝜑 |
46 | | nfv 1922 |
. . . . . 6
⊢
Ⅎ𝑘 𝑖 ∈ 𝐴 |
47 | 45, 46 | nfan 1907 |
. . . . 5
⊢
Ⅎ𝑘(𝜑 ∧ 𝑖 ∈ 𝐴) |
48 | 5 | nfel1 2920 |
. . . . 5
⊢
Ⅎ𝑘⦋𝑖 / 𝑘⦌𝐵 ∈ ℂ |
49 | 47, 48 | nfim 1904 |
. . . 4
⊢
Ⅎ𝑘((𝜑 ∧ 𝑖 ∈ 𝐴) → ⦋𝑖 / 𝑘⦌𝐵 ∈ ℂ) |
50 | | eleq1w 2820 |
. . . . . 6
⊢ (𝑘 = 𝑖 → (𝑘 ∈ 𝐴 ↔ 𝑖 ∈ 𝐴)) |
51 | 50 | anbi2d 632 |
. . . . 5
⊢ (𝑘 = 𝑖 → ((𝜑 ∧ 𝑘 ∈ 𝐴) ↔ (𝜑 ∧ 𝑖 ∈ 𝐴))) |
52 | 1 | eleq1d 2822 |
. . . . 5
⊢ (𝑘 = 𝑖 → (𝐵 ∈ ℂ ↔ ⦋𝑖 / 𝑘⦌𝐵 ∈ ℂ)) |
53 | 51, 52 | imbi12d 348 |
. . . 4
⊢ (𝑘 = 𝑖 → (((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ) ↔ ((𝜑 ∧ 𝑖 ∈ 𝐴) → ⦋𝑖 / 𝑘⦌𝐵 ∈ ℂ))) |
54 | | fsumf1of.7 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ) |
55 | 49, 53, 54 | chvarfv 2238 |
. . 3
⊢ ((𝜑 ∧ 𝑖 ∈ 𝐴) → ⦋𝑖 / 𝑘⦌𝐵 ∈ ℂ) |
56 | 29, 30, 31, 44, 55 | fsumf1o 15287 |
. 2
⊢ (𝜑 → Σ𝑖 ∈ 𝐴 ⦋𝑖 / 𝑘⦌𝐵 = Σ𝑗 ∈ 𝐶 ⦋𝑗 / 𝑛⦌𝐷) |
57 | | nfcv 2904 |
. . . . 5
⊢
Ⅎ𝑗𝐶 |
58 | | nfcv 2904 |
. . . . 5
⊢
Ⅎ𝑛𝐶 |
59 | | nfcv 2904 |
. . . . 5
⊢
Ⅎ𝑗𝐷 |
60 | 24, 57, 58, 59, 19 | cbvsum 15259 |
. . . 4
⊢
Σ𝑛 ∈
𝐶 𝐷 = Σ𝑗 ∈ 𝐶 ⦋𝑗 / 𝑛⦌𝐷 |
61 | 60 | eqcomi 2746 |
. . 3
⊢
Σ𝑗 ∈
𝐶 ⦋𝑗 / 𝑛⦌𝐷 = Σ𝑛 ∈ 𝐶 𝐷 |
62 | 61 | a1i 11 |
. 2
⊢ (𝜑 → Σ𝑗 ∈ 𝐶 ⦋𝑗 / 𝑛⦌𝐷 = Σ𝑛 ∈ 𝐶 𝐷) |
63 | 7, 56, 62 | 3eqtrd 2781 |
1
⊢ (𝜑 → Σ𝑘 ∈ 𝐴 𝐵 = Σ𝑛 ∈ 𝐶 𝐷) |