Metamath Proof Explorer

Theorem isumshft

Description: Index shift of an infinite sum. (Contributed by Paul Chapman, 31-Oct-2007) (Revised by Mario Carneiro, 24-Apr-2014)

Ref Expression
Hypotheses isumshft.1 ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
isumshft.2 ⊢ 𝑊 = ( ℤ≥ ‘ ( 𝑀 + 𝐾 ) )
isumshft.3 ⊢ ( 𝑗 = ( 𝐾 + 𝑘 ) → 𝐴 = 𝐵 )
isumshft.4 ⊢ ( 𝜑 → 𝐾 ∈ ℤ )
isumshft.5 ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
isumshft.6 ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑊 ) → 𝐴 ∈ ℂ )
Assertion isumshft ( 𝜑 → Σ 𝑗 ∈ 𝑊 𝐴 = Σ 𝑘 ∈ 𝑍 𝐵 )

Proof

Step Hyp Ref Expression
1 isumshft.1 ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
2 isumshft.2 ⊢ 𝑊 = ( ℤ≥ ‘ ( 𝑀 + 𝐾 ) )
3 isumshft.3 ⊢ ( 𝑗 = ( 𝐾 + 𝑘 ) → 𝐴 = 𝐵 )
4 isumshft.4 ⊢ ( 𝜑 → 𝐾 ∈ ℤ )
5 isumshft.5 ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
6 isumshft.6 ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑊 ) → 𝐴 ∈ ℂ )
7 5 4 zaddcld ⊢ ( 𝜑 → ( 𝑀 + 𝐾 ) ∈ ℤ )
8 2 eleq2i ⊢ ( 𝑚 ∈ 𝑊 ↔ 𝑚 ∈ ( ℤ≥ ‘ ( 𝑀 + 𝐾 ) ) )
9 4 zcnd ⊢ ( 𝜑 → 𝐾 ∈ ℂ )
10 eluzelcn ⊢ ( 𝑚 ∈ ( ℤ≥ ‘ ( 𝑀 + 𝐾 ) ) → 𝑚 ∈ ℂ )
11 10 2 eleq2s ⊢ ( 𝑚 ∈ 𝑊 → 𝑚 ∈ ℂ )
12 1 fvexi ⊢ 𝑍 ∈ V
13 12 mptex ⊢ ( 𝑘 ∈ 𝑍 ↦ 𝐵 ) ∈ V
14 13 shftval ⊢ ( ( 𝐾 ∈ ℂ ∧ 𝑚 ∈ ℂ ) → ( ( ( 𝑘 ∈ 𝑍 ↦ 𝐵 ) shift 𝐾 ) ‘ 𝑚 ) = ( ( 𝑘 ∈ 𝑍 ↦ 𝐵 ) ‘ ( 𝑚 − 𝐾 ) ) )
15 9 11 14 syl2an ⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝑊 ) → ( ( ( 𝑘 ∈ 𝑍 ↦ 𝐵 ) shift 𝐾 ) ‘ 𝑚 ) = ( ( 𝑘 ∈ 𝑍 ↦ 𝐵 ) ‘ ( 𝑚 − 𝐾 ) ) )
16 simpr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → 𝑘 ∈ 𝑍 )
17 eqid ⊢ ( 𝑘 ∈ 𝑍 ↦ 𝐵 ) = ( 𝑘 ∈ 𝑍 ↦ 𝐵 )
18 17 fvmpt2i ⊢ ( 𝑘 ∈ 𝑍 → ( ( 𝑘 ∈ 𝑍 ↦ 𝐵 ) ‘ 𝑘 ) = ( I ‘ 𝐵 ) )
19 16 18 syl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( ( 𝑘 ∈ 𝑍 ↦ 𝐵 ) ‘ 𝑘 ) = ( I ‘ 𝐵 ) )
20 eluzelcn ⊢ ( 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑘 ∈ ℂ )
21 20 1 eleq2s ⊢ ( 𝑘 ∈ 𝑍 → 𝑘 ∈ ℂ )
22 addcom ⊢ ( ( 𝐾 ∈ ℂ ∧ 𝑘 ∈ ℂ ) → ( 𝐾 + 𝑘 ) = ( 𝑘 + 𝐾 ) )
23 9 21 22 syl2an ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐾 + 𝑘 ) = ( 𝑘 + 𝐾 ) )
24 id ⊢ ( 𝑘 ∈ 𝑍 → 𝑘 ∈ 𝑍 )
25 24 1 eleqtrdi ⊢ ( 𝑘 ∈ 𝑍 → 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) )
26 eluzadd ⊢ ( ( 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝐾 ∈ ℤ ) → ( 𝑘 + 𝐾 ) ∈ ( ℤ≥ ‘ ( 𝑀 + 𝐾 ) ) )
27 25 4 26 syl2anr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝑘 + 𝐾 ) ∈ ( ℤ≥ ‘ ( 𝑀 + 𝐾 ) ) )
28 23 27 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐾 + 𝑘 ) ∈ ( ℤ≥ ‘ ( 𝑀 + 𝐾 ) ) )
29 28 2 eleqtrrdi ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐾 + 𝑘 ) ∈ 𝑊 )
30 eqid ⊢ ( 𝑗 ∈ 𝑊 ↦ 𝐴 ) = ( 𝑗 ∈ 𝑊 ↦ 𝐴 )
31 3 30 fvmpti ⊢ ( ( 𝐾 + 𝑘 ) ∈ 𝑊 → ( ( 𝑗 ∈ 𝑊 ↦ 𝐴 ) ‘ ( 𝐾 + 𝑘 ) ) = ( I ‘ 𝐵 ) )
32 29 31 syl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( ( 𝑗 ∈ 𝑊 ↦ 𝐴 ) ‘ ( 𝐾 + 𝑘 ) ) = ( I ‘ 𝐵 ) )
33 19 32 eqtr4d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( ( 𝑘 ∈ 𝑍 ↦ 𝐵 ) ‘ 𝑘 ) = ( ( 𝑗 ∈ 𝑊 ↦ 𝐴 ) ‘ ( 𝐾 + 𝑘 ) ) )
34 33 ralrimiva ⊢ ( 𝜑 → ∀ 𝑘 ∈ 𝑍 ( ( 𝑘 ∈ 𝑍 ↦ 𝐵 ) ‘ 𝑘 ) = ( ( 𝑗 ∈ 𝑊 ↦ 𝐴 ) ‘ ( 𝐾 + 𝑘 ) ) )
35 nffvmpt1 ⊢ Ⅎ 𝑘 ( ( 𝑘 ∈ 𝑍 ↦ 𝐵 ) ‘ 𝑛 )
36 35 nfeq1 ⊢ Ⅎ 𝑘 ( ( 𝑘 ∈ 𝑍 ↦ 𝐵 ) ‘ 𝑛 ) = ( ( 𝑗 ∈ 𝑊 ↦ 𝐴 ) ‘ ( 𝐾 + 𝑛 ) )
37 fveq2 ⊢ ( 𝑘 = 𝑛 → ( ( 𝑘 ∈ 𝑍 ↦ 𝐵 ) ‘ 𝑘 ) = ( ( 𝑘 ∈ 𝑍 ↦ 𝐵 ) ‘ 𝑛 ) )
38 oveq2 ⊢ ( 𝑘 = 𝑛 → ( 𝐾 + 𝑘 ) = ( 𝐾 + 𝑛 ) )
39 38 fveq2d ⊢ ( 𝑘 = 𝑛 → ( ( 𝑗 ∈ 𝑊 ↦ 𝐴 ) ‘ ( 𝐾 + 𝑘 ) ) = ( ( 𝑗 ∈ 𝑊 ↦ 𝐴 ) ‘ ( 𝐾 + 𝑛 ) ) )
40 37 39 eqeq12d ⊢ ( 𝑘 = 𝑛 → ( ( ( 𝑘 ∈ 𝑍 ↦ 𝐵 ) ‘ 𝑘 ) = ( ( 𝑗 ∈ 𝑊 ↦ 𝐴 ) ‘ ( 𝐾 + 𝑘 ) ) ↔ ( ( 𝑘 ∈ 𝑍 ↦ 𝐵 ) ‘ 𝑛 ) = ( ( 𝑗 ∈ 𝑊 ↦ 𝐴 ) ‘ ( 𝐾 + 𝑛 ) ) ) )
41 36 40 rspc ⊢ ( 𝑛 ∈ 𝑍 → ( ∀ 𝑘 ∈ 𝑍 ( ( 𝑘 ∈ 𝑍 ↦ 𝐵 ) ‘ 𝑘 ) = ( ( 𝑗 ∈ 𝑊 ↦ 𝐴 ) ‘ ( 𝐾 + 𝑘 ) ) → ( ( 𝑘 ∈ 𝑍 ↦ 𝐵 ) ‘ 𝑛 ) = ( ( 𝑗 ∈ 𝑊 ↦ 𝐴 ) ‘ ( 𝐾 + 𝑛 ) ) ) )
42 34 41 mpan9 ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ( ( 𝑘 ∈ 𝑍 ↦ 𝐵 ) ‘ 𝑛 ) = ( ( 𝑗 ∈ 𝑊 ↦ 𝐴 ) ‘ ( 𝐾 + 𝑛 ) ) )
43 42 ralrimiva ⊢ ( 𝜑 → ∀ 𝑛 ∈ 𝑍 ( ( 𝑘 ∈ 𝑍 ↦ 𝐵 ) ‘ 𝑛 ) = ( ( 𝑗 ∈ 𝑊 ↦ 𝐴 ) ‘ ( 𝐾 + 𝑛 ) ) )
44 5 adantr ⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝑊 ) → 𝑀 ∈ ℤ )
45 4 adantr ⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝑊 ) → 𝐾 ∈ ℤ )
46 simpr ⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝑊 ) → 𝑚 ∈ 𝑊 )
47 46 2 eleqtrdi ⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝑊 ) → 𝑚 ∈ ( ℤ≥ ‘ ( 𝑀 + 𝐾 ) ) )
48 eluzsub ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ ∧ 𝑚 ∈ ( ℤ≥ ‘ ( 𝑀 + 𝐾 ) ) ) → ( 𝑚 − 𝐾 ) ∈ ( ℤ≥ ‘ 𝑀 ) )
49 44 45 47 48 syl3anc ⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝑊 ) → ( 𝑚 − 𝐾 ) ∈ ( ℤ≥ ‘ 𝑀 ) )
50 49 1 eleqtrrdi ⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝑊 ) → ( 𝑚 − 𝐾 ) ∈ 𝑍 )
51 fveq2 ⊢ ( 𝑛 = ( 𝑚 − 𝐾 ) → ( ( 𝑘 ∈ 𝑍 ↦ 𝐵 ) ‘ 𝑛 ) = ( ( 𝑘 ∈ 𝑍 ↦ 𝐵 ) ‘ ( 𝑚 − 𝐾 ) ) )
52 oveq2 ⊢ ( 𝑛 = ( 𝑚 − 𝐾 ) → ( 𝐾 + 𝑛 ) = ( 𝐾 + ( 𝑚 − 𝐾 ) ) )
53 52 fveq2d ⊢ ( 𝑛 = ( 𝑚 − 𝐾 ) → ( ( 𝑗 ∈ 𝑊 ↦ 𝐴 ) ‘ ( 𝐾 + 𝑛 ) ) = ( ( 𝑗 ∈ 𝑊 ↦ 𝐴 ) ‘ ( 𝐾 + ( 𝑚 − 𝐾 ) ) ) )
54 51 53 eqeq12d ⊢ ( 𝑛 = ( 𝑚 − 𝐾 ) → ( ( ( 𝑘 ∈ 𝑍 ↦ 𝐵 ) ‘ 𝑛 ) = ( ( 𝑗 ∈ 𝑊 ↦ 𝐴 ) ‘ ( 𝐾 + 𝑛 ) ) ↔ ( ( 𝑘 ∈ 𝑍 ↦ 𝐵 ) ‘ ( 𝑚 − 𝐾 ) ) = ( ( 𝑗 ∈ 𝑊 ↦ 𝐴 ) ‘ ( 𝐾 + ( 𝑚 − 𝐾 ) ) ) ) )
55 54 rspccva ⊢ ( ( ∀ 𝑛 ∈ 𝑍 ( ( 𝑘 ∈ 𝑍 ↦ 𝐵 ) ‘ 𝑛 ) = ( ( 𝑗 ∈ 𝑊 ↦ 𝐴 ) ‘ ( 𝐾 + 𝑛 ) ) ∧ ( 𝑚 − 𝐾 ) ∈ 𝑍 ) → ( ( 𝑘 ∈ 𝑍 ↦ 𝐵 ) ‘ ( 𝑚 − 𝐾 ) ) = ( ( 𝑗 ∈ 𝑊 ↦ 𝐴 ) ‘ ( 𝐾 + ( 𝑚 − 𝐾 ) ) ) )
56 43 50 55 syl2an2r ⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝑊 ) → ( ( 𝑘 ∈ 𝑍 ↦ 𝐵 ) ‘ ( 𝑚 − 𝐾 ) ) = ( ( 𝑗 ∈ 𝑊 ↦ 𝐴 ) ‘ ( 𝐾 + ( 𝑚 − 𝐾 ) ) ) )
57 pncan3 ⊢ ( ( 𝐾 ∈ ℂ ∧ 𝑚 ∈ ℂ ) → ( 𝐾 + ( 𝑚 − 𝐾 ) ) = 𝑚 )
58 9 11 57 syl2an ⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝑊 ) → ( 𝐾 + ( 𝑚 − 𝐾 ) ) = 𝑚 )
59 58 fveq2d ⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝑊 ) → ( ( 𝑗 ∈ 𝑊 ↦ 𝐴 ) ‘ ( 𝐾 + ( 𝑚 − 𝐾 ) ) ) = ( ( 𝑗 ∈ 𝑊 ↦ 𝐴 ) ‘ 𝑚 ) )
60 15 56 59 3eqtrrd ⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝑊 ) → ( ( 𝑗 ∈ 𝑊 ↦ 𝐴 ) ‘ 𝑚 ) = ( ( ( 𝑘 ∈ 𝑍 ↦ 𝐵 ) shift 𝐾 ) ‘ 𝑚 ) )
61 8 60 sylan2br ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( ℤ≥ ‘ ( 𝑀 + 𝐾 ) ) ) → ( ( 𝑗 ∈ 𝑊 ↦ 𝐴 ) ‘ 𝑚 ) = ( ( ( 𝑘 ∈ 𝑍 ↦ 𝐵 ) shift 𝐾 ) ‘ 𝑚 ) )
62 7 61 seqfeq ⊢ ( 𝜑 → seq ( 𝑀 + 𝐾 ) ( + , ( 𝑗 ∈ 𝑊 ↦ 𝐴 ) ) = seq ( 𝑀 + 𝐾 ) ( + , ( ( 𝑘 ∈ 𝑍 ↦ 𝐵 ) shift 𝐾 ) ) )
63 62 breq1d ⊢ ( 𝜑 → ( seq ( 𝑀 + 𝐾 ) ( + , ( 𝑗 ∈ 𝑊 ↦ 𝐴 ) ) ⇝ 𝑥 ↔ seq ( 𝑀 + 𝐾 ) ( + , ( ( 𝑘 ∈ 𝑍 ↦ 𝐵 ) shift 𝐾 ) ) ⇝ 𝑥 ) )
64 13 isershft ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ ) → ( seq 𝑀 ( + , ( 𝑘 ∈ 𝑍 ↦ 𝐵 ) ) ⇝ 𝑥 ↔ seq ( 𝑀 + 𝐾 ) ( + , ( ( 𝑘 ∈ 𝑍 ↦ 𝐵 ) shift 𝐾 ) ) ⇝ 𝑥 ) )
65 5 4 64 syl2anc ⊢ ( 𝜑 → ( seq 𝑀 ( + , ( 𝑘 ∈ 𝑍 ↦ 𝐵 ) ) ⇝ 𝑥 ↔ seq ( 𝑀 + 𝐾 ) ( + , ( ( 𝑘 ∈ 𝑍 ↦ 𝐵 ) shift 𝐾 ) ) ⇝ 𝑥 ) )
66 63 65 bitr4d ⊢ ( 𝜑 → ( seq ( 𝑀 + 𝐾 ) ( + , ( 𝑗 ∈ 𝑊 ↦ 𝐴 ) ) ⇝ 𝑥 ↔ seq 𝑀 ( + , ( 𝑘 ∈ 𝑍 ↦ 𝐵 ) ) ⇝ 𝑥 ) )
67 66 iotabidv ⊢ ( 𝜑 → ( ℩ 𝑥 seq ( 𝑀 + 𝐾 ) ( + , ( 𝑗 ∈ 𝑊 ↦ 𝐴 ) ) ⇝ 𝑥 ) = ( ℩ 𝑥 seq 𝑀 ( + , ( 𝑘 ∈ 𝑍 ↦ 𝐵 ) ) ⇝ 𝑥 ) )
68 df-fv ⊢ ( ⇝ ‘ seq ( 𝑀 + 𝐾 ) ( + , ( 𝑗 ∈ 𝑊 ↦ 𝐴 ) ) ) = ( ℩ 𝑥 seq ( 𝑀 + 𝐾 ) ( + , ( 𝑗 ∈ 𝑊 ↦ 𝐴 ) ) ⇝ 𝑥 )
69 df-fv ⊢ ( ⇝ ‘ seq 𝑀 ( + , ( 𝑘 ∈ 𝑍 ↦ 𝐵 ) ) ) = ( ℩ 𝑥 seq 𝑀 ( + , ( 𝑘 ∈ 𝑍 ↦ 𝐵 ) ) ⇝ 𝑥 )
70 67 68 69 3eqtr4g ⊢ ( 𝜑 → ( ⇝ ‘ seq ( 𝑀 + 𝐾 ) ( + , ( 𝑗 ∈ 𝑊 ↦ 𝐴 ) ) ) = ( ⇝ ‘ seq 𝑀 ( + , ( 𝑘 ∈ 𝑍 ↦ 𝐵 ) ) ) )
71 eqidd ⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝑊 ) → ( ( 𝑗 ∈ 𝑊 ↦ 𝐴 ) ‘ 𝑚 ) = ( ( 𝑗 ∈ 𝑊 ↦ 𝐴 ) ‘ 𝑚 ) )
72 6 fmpttd ⊢ ( 𝜑 → ( 𝑗 ∈ 𝑊 ↦ 𝐴 ) : 𝑊 ⟶ ℂ )
73 72 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝑊 ) → ( ( 𝑗 ∈ 𝑊 ↦ 𝐴 ) ‘ 𝑚 ) ∈ ℂ )
74 2 7 71 73 isum ⊢ ( 𝜑 → Σ 𝑚 ∈ 𝑊 ( ( 𝑗 ∈ 𝑊 ↦ 𝐴 ) ‘ 𝑚 ) = ( ⇝ ‘ seq ( 𝑀 + 𝐾 ) ( + , ( 𝑗 ∈ 𝑊 ↦ 𝐴 ) ) ) )
75 eqidd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ( ( 𝑘 ∈ 𝑍 ↦ 𝐵 ) ‘ 𝑛 ) = ( ( 𝑘 ∈ 𝑍 ↦ 𝐵 ) ‘ 𝑛 ) )
76 29 ralrimiva ⊢ ( 𝜑 → ∀ 𝑘 ∈ 𝑍 ( 𝐾 + 𝑘 ) ∈ 𝑊 )
77 38 eleq1d ⊢ ( 𝑘 = 𝑛 → ( ( 𝐾 + 𝑘 ) ∈ 𝑊 ↔ ( 𝐾 + 𝑛 ) ∈ 𝑊 ) )
78 77 rspccva ⊢ ( ( ∀ 𝑘 ∈ 𝑍 ( 𝐾 + 𝑘 ) ∈ 𝑊 ∧ 𝑛 ∈ 𝑍 ) → ( 𝐾 + 𝑛 ) ∈ 𝑊 )
79 76 78 sylan ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ( 𝐾 + 𝑛 ) ∈ 𝑊 )
80 ffvelcdm ⊢ ( ( ( 𝑗 ∈ 𝑊 ↦ 𝐴 ) : 𝑊 ⟶ ℂ ∧ ( 𝐾 + 𝑛 ) ∈ 𝑊 ) → ( ( 𝑗 ∈ 𝑊 ↦ 𝐴 ) ‘ ( 𝐾 + 𝑛 ) ) ∈ ℂ )
81 72 79 80 syl2an2r ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ( ( 𝑗 ∈ 𝑊 ↦ 𝐴 ) ‘ ( 𝐾 + 𝑛 ) ) ∈ ℂ )
82 42 81 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ( ( 𝑘 ∈ 𝑍 ↦ 𝐵 ) ‘ 𝑛 ) ∈ ℂ )
83 1 5 75 82 isum ⊢ ( 𝜑 → Σ 𝑛 ∈ 𝑍 ( ( 𝑘 ∈ 𝑍 ↦ 𝐵 ) ‘ 𝑛 ) = ( ⇝ ‘ seq 𝑀 ( + , ( 𝑘 ∈ 𝑍 ↦ 𝐵 ) ) ) )
84 70 74 83 3eqtr4d ⊢ ( 𝜑 → Σ 𝑚 ∈ 𝑊 ( ( 𝑗 ∈ 𝑊 ↦ 𝐴 ) ‘ 𝑚 ) = Σ 𝑛 ∈ 𝑍 ( ( 𝑘 ∈ 𝑍 ↦ 𝐵 ) ‘ 𝑛 ) )
85 sumfc ⊢ Σ 𝑚 ∈ 𝑊 ( ( 𝑗 ∈ 𝑊 ↦ 𝐴 ) ‘ 𝑚 ) = Σ 𝑗 ∈ 𝑊 𝐴
86 sumfc ⊢ Σ 𝑛 ∈ 𝑍 ( ( 𝑘 ∈ 𝑍 ↦ 𝐵 ) ‘ 𝑛 ) = Σ 𝑘 ∈ 𝑍 𝐵
87 84 85 86 3eqtr3g ⊢ ( 𝜑 → Σ 𝑗 ∈ 𝑊 𝐴 = Σ 𝑘 ∈ 𝑍 𝐵 )