Step | Hyp | Ref
| Expression |
1 | | isumshft.5 |
. . . . . . . . 9
⊢ (𝜑 → 𝑀 ∈ ℤ) |
2 | | isumshft.4 |
. . . . . . . . 9
⊢ (𝜑 → 𝐾 ∈ ℤ) |
3 | 1, 2 | zaddcld 11362 |
. . . . . . . 8
⊢ (𝜑 → (𝑀 + 𝐾) ∈ ℤ) |
4 | | isumshft.2 |
. . . . . . . . . 10
⊢ 𝑊 =
(ℤ≥‘(𝑀 + 𝐾)) |
5 | 4 | eleq2i 2680 |
. . . . . . . . 9
⊢ (𝑚 ∈ 𝑊 ↔ 𝑚 ∈ (ℤ≥‘(𝑀 + 𝐾))) |
6 | 2 | zcnd 11359 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐾 ∈ ℂ) |
7 | | eluzelcn 11575 |
. . . . . . . . . . . 12
⊢ (𝑚 ∈
(ℤ≥‘(𝑀 + 𝐾)) → 𝑚 ∈ ℂ) |
8 | 7, 4 | eleq2s 2706 |
. . . . . . . . . . 11
⊢ (𝑚 ∈ 𝑊 → 𝑚 ∈ ℂ) |
9 | | isumshft.1 |
. . . . . . . . . . . . . 14
⊢ 𝑍 =
(ℤ≥‘𝑀) |
10 | | fvex 6113 |
. . . . . . . . . . . . . 14
⊢
(ℤ≥‘𝑀) ∈ V |
11 | 9, 10 | eqeltri 2684 |
. . . . . . . . . . . . 13
⊢ 𝑍 ∈ V |
12 | 11 | mptex 6390 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ 𝑍 ↦ 𝐵) ∈ V |
13 | 12 | shftval 13662 |
. . . . . . . . . . 11
⊢ ((𝐾 ∈ ℂ ∧ 𝑚 ∈ ℂ) → (((𝑘 ∈ 𝑍 ↦ 𝐵) shift 𝐾)‘𝑚) = ((𝑘 ∈ 𝑍 ↦ 𝐵)‘(𝑚 − 𝐾))) |
14 | 6, 8, 13 | syl2an 493 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑚 ∈ 𝑊) → (((𝑘 ∈ 𝑍 ↦ 𝐵) shift 𝐾)‘𝑚) = ((𝑘 ∈ 𝑍 ↦ 𝐵)‘(𝑚 − 𝐾))) |
15 | | simpr 476 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝑘 ∈ 𝑍) |
16 | | eqid 2610 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑘 ∈ 𝑍 ↦ 𝐵) = (𝑘 ∈ 𝑍 ↦ 𝐵) |
17 | 16 | fvmpt2i 6199 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑘 ∈ 𝑍 → ((𝑘 ∈ 𝑍 ↦ 𝐵)‘𝑘) = ( I ‘𝐵)) |
18 | 15, 17 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → ((𝑘 ∈ 𝑍 ↦ 𝐵)‘𝑘) = ( I ‘𝐵)) |
19 | | eluzelcn 11575 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑘 ∈
(ℤ≥‘𝑀) → 𝑘 ∈ ℂ) |
20 | 19, 9 | eleq2s 2706 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑘 ∈ 𝑍 → 𝑘 ∈ ℂ) |
21 | | addcom 10101 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐾 ∈ ℂ ∧ 𝑘 ∈ ℂ) → (𝐾 + 𝑘) = (𝑘 + 𝐾)) |
22 | 6, 20, 21 | syl2an 493 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐾 + 𝑘) = (𝑘 + 𝐾)) |
23 | | id 22 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑘 ∈ 𝑍 → 𝑘 ∈ 𝑍) |
24 | 23, 9 | syl6eleq 2698 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑘 ∈ 𝑍 → 𝑘 ∈ (ℤ≥‘𝑀)) |
25 | | eluzadd 11592 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑘 ∈
(ℤ≥‘𝑀) ∧ 𝐾 ∈ ℤ) → (𝑘 + 𝐾) ∈
(ℤ≥‘(𝑀 + 𝐾))) |
26 | 24, 2, 25 | syl2anr 494 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝑘 + 𝐾) ∈
(ℤ≥‘(𝑀 + 𝐾))) |
27 | 22, 26 | eqeltrd 2688 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐾 + 𝑘) ∈ (ℤ≥‘(𝑀 + 𝐾))) |
28 | 27, 4 | syl6eleqr 2699 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐾 + 𝑘) ∈ 𝑊) |
29 | | isumshft.3 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑗 = (𝐾 + 𝑘) → 𝐴 = 𝐵) |
30 | | eqid 2610 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑗 ∈ 𝑊 ↦ 𝐴) = (𝑗 ∈ 𝑊 ↦ 𝐴) |
31 | 29, 30 | fvmpti 6190 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐾 + 𝑘) ∈ 𝑊 → ((𝑗 ∈ 𝑊 ↦ 𝐴)‘(𝐾 + 𝑘)) = ( I ‘𝐵)) |
32 | 28, 31 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → ((𝑗 ∈ 𝑊 ↦ 𝐴)‘(𝐾 + 𝑘)) = ( I ‘𝐵)) |
33 | 18, 32 | eqtr4d 2647 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → ((𝑘 ∈ 𝑍 ↦ 𝐵)‘𝑘) = ((𝑗 ∈ 𝑊 ↦ 𝐴)‘(𝐾 + 𝑘))) |
34 | 33 | ralrimiva 2949 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ∀𝑘 ∈ 𝑍 ((𝑘 ∈ 𝑍 ↦ 𝐵)‘𝑘) = ((𝑗 ∈ 𝑊 ↦ 𝐴)‘(𝐾 + 𝑘))) |
35 | | nffvmpt1 6111 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑘((𝑘 ∈ 𝑍 ↦ 𝐵)‘𝑛) |
36 | 35 | nfeq1 2764 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑘((𝑘 ∈ 𝑍 ↦ 𝐵)‘𝑛) = ((𝑗 ∈ 𝑊 ↦ 𝐴)‘(𝐾 + 𝑛)) |
37 | | fveq2 6103 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 = 𝑛 → ((𝑘 ∈ 𝑍 ↦ 𝐵)‘𝑘) = ((𝑘 ∈ 𝑍 ↦ 𝐵)‘𝑛)) |
38 | | oveq2 6557 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑘 = 𝑛 → (𝐾 + 𝑘) = (𝐾 + 𝑛)) |
39 | 38 | fveq2d 6107 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 = 𝑛 → ((𝑗 ∈ 𝑊 ↦ 𝐴)‘(𝐾 + 𝑘)) = ((𝑗 ∈ 𝑊 ↦ 𝐴)‘(𝐾 + 𝑛))) |
40 | 37, 39 | eqeq12d 2625 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 = 𝑛 → (((𝑘 ∈ 𝑍 ↦ 𝐵)‘𝑘) = ((𝑗 ∈ 𝑊 ↦ 𝐴)‘(𝐾 + 𝑘)) ↔ ((𝑘 ∈ 𝑍 ↦ 𝐵)‘𝑛) = ((𝑗 ∈ 𝑊 ↦ 𝐴)‘(𝐾 + 𝑛)))) |
41 | 36, 40 | rspc 3276 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ∈ 𝑍 → (∀𝑘 ∈ 𝑍 ((𝑘 ∈ 𝑍 ↦ 𝐵)‘𝑘) = ((𝑗 ∈ 𝑊 ↦ 𝐴)‘(𝐾 + 𝑘)) → ((𝑘 ∈ 𝑍 ↦ 𝐵)‘𝑛) = ((𝑗 ∈ 𝑊 ↦ 𝐴)‘(𝐾 + 𝑛)))) |
42 | 34, 41 | mpan9 485 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → ((𝑘 ∈ 𝑍 ↦ 𝐵)‘𝑛) = ((𝑗 ∈ 𝑊 ↦ 𝐴)‘(𝐾 + 𝑛))) |
43 | 42 | ralrimiva 2949 |
. . . . . . . . . . . 12
⊢ (𝜑 → ∀𝑛 ∈ 𝑍 ((𝑘 ∈ 𝑍 ↦ 𝐵)‘𝑛) = ((𝑗 ∈ 𝑊 ↦ 𝐴)‘(𝐾 + 𝑛))) |
44 | 43 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑚 ∈ 𝑊) → ∀𝑛 ∈ 𝑍 ((𝑘 ∈ 𝑍 ↦ 𝐵)‘𝑛) = ((𝑗 ∈ 𝑊 ↦ 𝐴)‘(𝐾 + 𝑛))) |
45 | 1 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑚 ∈ 𝑊) → 𝑀 ∈ ℤ) |
46 | 2 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑚 ∈ 𝑊) → 𝐾 ∈ ℤ) |
47 | | simpr 476 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑚 ∈ 𝑊) → 𝑚 ∈ 𝑊) |
48 | 47, 4 | syl6eleq 2698 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑚 ∈ 𝑊) → 𝑚 ∈ (ℤ≥‘(𝑀 + 𝐾))) |
49 | | eluzsub 11593 |
. . . . . . . . . . . . 13
⊢ ((𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ ∧ 𝑚 ∈
(ℤ≥‘(𝑀 + 𝐾))) → (𝑚 − 𝐾) ∈ (ℤ≥‘𝑀)) |
50 | 45, 46, 48, 49 | syl3anc 1318 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑚 ∈ 𝑊) → (𝑚 − 𝐾) ∈ (ℤ≥‘𝑀)) |
51 | 50, 9 | syl6eleqr 2699 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑚 ∈ 𝑊) → (𝑚 − 𝐾) ∈ 𝑍) |
52 | | fveq2 6103 |
. . . . . . . . . . . . 13
⊢ (𝑛 = (𝑚 − 𝐾) → ((𝑘 ∈ 𝑍 ↦ 𝐵)‘𝑛) = ((𝑘 ∈ 𝑍 ↦ 𝐵)‘(𝑚 − 𝐾))) |
53 | | oveq2 6557 |
. . . . . . . . . . . . . 14
⊢ (𝑛 = (𝑚 − 𝐾) → (𝐾 + 𝑛) = (𝐾 + (𝑚 − 𝐾))) |
54 | 53 | fveq2d 6107 |
. . . . . . . . . . . . 13
⊢ (𝑛 = (𝑚 − 𝐾) → ((𝑗 ∈ 𝑊 ↦ 𝐴)‘(𝐾 + 𝑛)) = ((𝑗 ∈ 𝑊 ↦ 𝐴)‘(𝐾 + (𝑚 − 𝐾)))) |
55 | 52, 54 | eqeq12d 2625 |
. . . . . . . . . . . 12
⊢ (𝑛 = (𝑚 − 𝐾) → (((𝑘 ∈ 𝑍 ↦ 𝐵)‘𝑛) = ((𝑗 ∈ 𝑊 ↦ 𝐴)‘(𝐾 + 𝑛)) ↔ ((𝑘 ∈ 𝑍 ↦ 𝐵)‘(𝑚 − 𝐾)) = ((𝑗 ∈ 𝑊 ↦ 𝐴)‘(𝐾 + (𝑚 − 𝐾))))) |
56 | 55 | rspccva 3281 |
. . . . . . . . . . 11
⊢
((∀𝑛 ∈
𝑍 ((𝑘 ∈ 𝑍 ↦ 𝐵)‘𝑛) = ((𝑗 ∈ 𝑊 ↦ 𝐴)‘(𝐾 + 𝑛)) ∧ (𝑚 − 𝐾) ∈ 𝑍) → ((𝑘 ∈ 𝑍 ↦ 𝐵)‘(𝑚 − 𝐾)) = ((𝑗 ∈ 𝑊 ↦ 𝐴)‘(𝐾 + (𝑚 − 𝐾)))) |
57 | 44, 51, 56 | syl2anc 691 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑚 ∈ 𝑊) → ((𝑘 ∈ 𝑍 ↦ 𝐵)‘(𝑚 − 𝐾)) = ((𝑗 ∈ 𝑊 ↦ 𝐴)‘(𝐾 + (𝑚 − 𝐾)))) |
58 | | pncan3 10168 |
. . . . . . . . . . . 12
⊢ ((𝐾 ∈ ℂ ∧ 𝑚 ∈ ℂ) → (𝐾 + (𝑚 − 𝐾)) = 𝑚) |
59 | 6, 8, 58 | syl2an 493 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑚 ∈ 𝑊) → (𝐾 + (𝑚 − 𝐾)) = 𝑚) |
60 | 59 | fveq2d 6107 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑚 ∈ 𝑊) → ((𝑗 ∈ 𝑊 ↦ 𝐴)‘(𝐾 + (𝑚 − 𝐾))) = ((𝑗 ∈ 𝑊 ↦ 𝐴)‘𝑚)) |
61 | 14, 57, 60 | 3eqtrrd 2649 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑚 ∈ 𝑊) → ((𝑗 ∈ 𝑊 ↦ 𝐴)‘𝑚) = (((𝑘 ∈ 𝑍 ↦ 𝐵) shift 𝐾)‘𝑚)) |
62 | 5, 61 | sylan2br 492 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑀 + 𝐾))) → ((𝑗 ∈ 𝑊 ↦ 𝐴)‘𝑚) = (((𝑘 ∈ 𝑍 ↦ 𝐵) shift 𝐾)‘𝑚)) |
63 | 3, 62 | seqfeq 12688 |
. . . . . . 7
⊢ (𝜑 → seq(𝑀 + 𝐾)( + , (𝑗 ∈ 𝑊 ↦ 𝐴)) = seq(𝑀 + 𝐾)( + , ((𝑘 ∈ 𝑍 ↦ 𝐵) shift 𝐾))) |
64 | 63 | breq1d 4593 |
. . . . . 6
⊢ (𝜑 → (seq(𝑀 + 𝐾)( + , (𝑗 ∈ 𝑊 ↦ 𝐴)) ⇝ 𝑥 ↔ seq(𝑀 + 𝐾)( + , ((𝑘 ∈ 𝑍 ↦ 𝐵) shift 𝐾)) ⇝ 𝑥)) |
65 | 12 | isershft 14242 |
. . . . . . 7
⊢ ((𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ) →
(seq𝑀( + , (𝑘 ∈ 𝑍 ↦ 𝐵)) ⇝ 𝑥 ↔ seq(𝑀 + 𝐾)( + , ((𝑘 ∈ 𝑍 ↦ 𝐵) shift 𝐾)) ⇝ 𝑥)) |
66 | 1, 2, 65 | syl2anc 691 |
. . . . . 6
⊢ (𝜑 → (seq𝑀( + , (𝑘 ∈ 𝑍 ↦ 𝐵)) ⇝ 𝑥 ↔ seq(𝑀 + 𝐾)( + , ((𝑘 ∈ 𝑍 ↦ 𝐵) shift 𝐾)) ⇝ 𝑥)) |
67 | 64, 66 | bitr4d 270 |
. . . . 5
⊢ (𝜑 → (seq(𝑀 + 𝐾)( + , (𝑗 ∈ 𝑊 ↦ 𝐴)) ⇝ 𝑥 ↔ seq𝑀( + , (𝑘 ∈ 𝑍 ↦ 𝐵)) ⇝ 𝑥)) |
68 | 67 | iotabidv 5789 |
. . . 4
⊢ (𝜑 → (℩𝑥seq(𝑀 + 𝐾)( + , (𝑗 ∈ 𝑊 ↦ 𝐴)) ⇝ 𝑥) = (℩𝑥seq𝑀( + , (𝑘 ∈ 𝑍 ↦ 𝐵)) ⇝ 𝑥)) |
69 | | df-fv 5812 |
. . . 4
⊢ ( ⇝
‘seq(𝑀 + 𝐾)( + , (𝑗 ∈ 𝑊 ↦ 𝐴))) = (℩𝑥seq(𝑀 + 𝐾)( + , (𝑗 ∈ 𝑊 ↦ 𝐴)) ⇝ 𝑥) |
70 | | df-fv 5812 |
. . . 4
⊢ ( ⇝
‘seq𝑀( + , (𝑘 ∈ 𝑍 ↦ 𝐵))) = (℩𝑥seq𝑀( + , (𝑘 ∈ 𝑍 ↦ 𝐵)) ⇝ 𝑥) |
71 | 68, 69, 70 | 3eqtr4g 2669 |
. . 3
⊢ (𝜑 → ( ⇝ ‘seq(𝑀 + 𝐾)( + , (𝑗 ∈ 𝑊 ↦ 𝐴))) = ( ⇝ ‘seq𝑀( + , (𝑘 ∈ 𝑍 ↦ 𝐵)))) |
72 | | eqidd 2611 |
. . . 4
⊢ ((𝜑 ∧ 𝑚 ∈ 𝑊) → ((𝑗 ∈ 𝑊 ↦ 𝐴)‘𝑚) = ((𝑗 ∈ 𝑊 ↦ 𝐴)‘𝑚)) |
73 | | isumshft.6 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑊) → 𝐴 ∈ ℂ) |
74 | 73, 30 | fmptd 6292 |
. . . . 5
⊢ (𝜑 → (𝑗 ∈ 𝑊 ↦ 𝐴):𝑊⟶ℂ) |
75 | | ffvelrn 6265 |
. . . . 5
⊢ (((𝑗 ∈ 𝑊 ↦ 𝐴):𝑊⟶ℂ ∧ 𝑚 ∈ 𝑊) → ((𝑗 ∈ 𝑊 ↦ 𝐴)‘𝑚) ∈ ℂ) |
76 | 74, 75 | sylan 487 |
. . . 4
⊢ ((𝜑 ∧ 𝑚 ∈ 𝑊) → ((𝑗 ∈ 𝑊 ↦ 𝐴)‘𝑚) ∈ ℂ) |
77 | 4, 3, 72, 76 | isum 14297 |
. . 3
⊢ (𝜑 → Σ𝑚 ∈ 𝑊 ((𝑗 ∈ 𝑊 ↦ 𝐴)‘𝑚) = ( ⇝ ‘seq(𝑀 + 𝐾)( + , (𝑗 ∈ 𝑊 ↦ 𝐴)))) |
78 | | eqidd 2611 |
. . . 4
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → ((𝑘 ∈ 𝑍 ↦ 𝐵)‘𝑛) = ((𝑘 ∈ 𝑍 ↦ 𝐵)‘𝑛)) |
79 | 74 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑗 ∈ 𝑊 ↦ 𝐴):𝑊⟶ℂ) |
80 | 28 | ralrimiva 2949 |
. . . . . . 7
⊢ (𝜑 → ∀𝑘 ∈ 𝑍 (𝐾 + 𝑘) ∈ 𝑊) |
81 | 38 | eleq1d 2672 |
. . . . . . . 8
⊢ (𝑘 = 𝑛 → ((𝐾 + 𝑘) ∈ 𝑊 ↔ (𝐾 + 𝑛) ∈ 𝑊)) |
82 | 81 | rspccva 3281 |
. . . . . . 7
⊢
((∀𝑘 ∈
𝑍 (𝐾 + 𝑘) ∈ 𝑊 ∧ 𝑛 ∈ 𝑍) → (𝐾 + 𝑛) ∈ 𝑊) |
83 | 80, 82 | sylan 487 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐾 + 𝑛) ∈ 𝑊) |
84 | | ffvelrn 6265 |
. . . . . 6
⊢ (((𝑗 ∈ 𝑊 ↦ 𝐴):𝑊⟶ℂ ∧ (𝐾 + 𝑛) ∈ 𝑊) → ((𝑗 ∈ 𝑊 ↦ 𝐴)‘(𝐾 + 𝑛)) ∈ ℂ) |
85 | 79, 83, 84 | syl2anc 691 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → ((𝑗 ∈ 𝑊 ↦ 𝐴)‘(𝐾 + 𝑛)) ∈ ℂ) |
86 | 42, 85 | eqeltrd 2688 |
. . . 4
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → ((𝑘 ∈ 𝑍 ↦ 𝐵)‘𝑛) ∈ ℂ) |
87 | 9, 1, 78, 86 | isum 14297 |
. . 3
⊢ (𝜑 → Σ𝑛 ∈ 𝑍 ((𝑘 ∈ 𝑍 ↦ 𝐵)‘𝑛) = ( ⇝ ‘seq𝑀( + , (𝑘 ∈ 𝑍 ↦ 𝐵)))) |
88 | 71, 77, 87 | 3eqtr4d 2654 |
. 2
⊢ (𝜑 → Σ𝑚 ∈ 𝑊 ((𝑗 ∈ 𝑊 ↦ 𝐴)‘𝑚) = Σ𝑛 ∈ 𝑍 ((𝑘 ∈ 𝑍 ↦ 𝐵)‘𝑛)) |
89 | | sumfc 14287 |
. 2
⊢
Σ𝑚 ∈
𝑊 ((𝑗 ∈ 𝑊 ↦ 𝐴)‘𝑚) = Σ𝑗 ∈ 𝑊 𝐴 |
90 | | sumfc 14287 |
. 2
⊢
Σ𝑛 ∈
𝑍 ((𝑘 ∈ 𝑍 ↦ 𝐵)‘𝑛) = Σ𝑘 ∈ 𝑍 𝐵 |
91 | 88, 89, 90 | 3eqtr3g 2667 |
1
⊢ (𝜑 → Σ𝑗 ∈ 𝑊 𝐴 = Σ𝑘 ∈ 𝑍 𝐵) |