Metamath Proof Explorer

Theorem fsumcom2

Description: Interchange order of summation. Note that B ( j ) and D ( k ) are not necessarily constant expressions. (Contributed by Mario Carneiro, 28-Apr-2014) (Revised by Mario Carneiro, 8-Apr-2016) (Proof shortened by JJ, 2-Aug-2021)

Ref Expression
Hypotheses fsumcom2.1 ⊢ ( 𝜑 → 𝐴 ∈ Fin )
fsumcom2.2 ⊢ ( 𝜑 → 𝐶 ∈ Fin )
fsumcom2.3 ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) → 𝐵 ∈ Fin )
fsumcom2.4 ⊢ ( 𝜑 → ( ( 𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ) ↔ ( 𝑘 ∈ 𝐶 ∧ 𝑗 ∈ 𝐷 ) ) )
fsumcom2.5 ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ) ) → 𝐸 ∈ ℂ )
Assertion fsumcom2 ( 𝜑 → Σ 𝑗 ∈ 𝐴 Σ 𝑘 ∈ 𝐵 𝐸 = Σ 𝑘 ∈ 𝐶 Σ 𝑗 ∈ 𝐷 𝐸 )

Proof

Step Hyp Ref Expression
1 fsumcom2.1 ⊢ ( 𝜑 → 𝐴 ∈ Fin )
2 fsumcom2.2 ⊢ ( 𝜑 → 𝐶 ∈ Fin )
3 fsumcom2.3 ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) → 𝐵 ∈ Fin )
4 fsumcom2.4 ⊢ ( 𝜑 → ( ( 𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ) ↔ ( 𝑘 ∈ 𝐶 ∧ 𝑗 ∈ 𝐷 ) ) )
5 fsumcom2.5 ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ) ) → 𝐸 ∈ ℂ )
6 relxp ⊢ Rel ( { 𝑗 } × 𝐵 )
7 6 rgenw ⊢ ∀ 𝑗 ∈ 𝐴 Rel ( { 𝑗 } × 𝐵 )
8 reliun ⊢ ( Rel ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ↔ ∀ 𝑗 ∈ 𝐴 Rel ( { 𝑗 } × 𝐵 ) )
9 7 8 mpbir ⊢ Rel ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 )
10 relcnv ⊢ Rel ◡ ∪ 𝑘 ∈ 𝐶 ( { 𝑘 } × 𝐷 )
11 ancom ⊢ ( ( 𝑥 = 𝑗 ∧ 𝑦 = 𝑘 ) ↔ ( 𝑦 = 𝑘 ∧ 𝑥 = 𝑗 ) )
12 vex ⊢ 𝑥 ∈ V
13 vex ⊢ 𝑦 ∈ V
14 12 13 opth ⊢ ( ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝑗 , 𝑘 ⟩ ↔ ( 𝑥 = 𝑗 ∧ 𝑦 = 𝑘 ) )
15 13 12 opth ⊢ ( ⟨ 𝑦 , 𝑥 ⟩ = ⟨ 𝑘 , 𝑗 ⟩ ↔ ( 𝑦 = 𝑘 ∧ 𝑥 = 𝑗 ) )
16 11 14 15 3bitr4i ⊢ ( ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝑗 , 𝑘 ⟩ ↔ ⟨ 𝑦 , 𝑥 ⟩ = ⟨ 𝑘 , 𝑗 ⟩ )
17 16 a1i ⊢ ( 𝜑 → ( ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝑗 , 𝑘 ⟩ ↔ ⟨ 𝑦 , 𝑥 ⟩ = ⟨ 𝑘 , 𝑗 ⟩ ) )
18 17 4 anbi12d ⊢ ( 𝜑 → ( ( ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝑗 , 𝑘 ⟩ ∧ ( 𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ) ) ↔ ( ⟨ 𝑦 , 𝑥 ⟩ = ⟨ 𝑘 , 𝑗 ⟩ ∧ ( 𝑘 ∈ 𝐶 ∧ 𝑗 ∈ 𝐷 ) ) ) )
19 18 2exbidv ⊢ ( 𝜑 → ( ∃ 𝑗 ∃ 𝑘 ( ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝑗 , 𝑘 ⟩ ∧ ( 𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ) ) ↔ ∃ 𝑗 ∃ 𝑘 ( ⟨ 𝑦 , 𝑥 ⟩ = ⟨ 𝑘 , 𝑗 ⟩ ∧ ( 𝑘 ∈ 𝐶 ∧ 𝑗 ∈ 𝐷 ) ) ) )
20 eliunxp ⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ↔ ∃ 𝑗 ∃ 𝑘 ( ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝑗 , 𝑘 ⟩ ∧ ( 𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ) ) )
21 12 13 opelcnv ⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ◡ ∪ 𝑘 ∈ 𝐶 ( { 𝑘 } × 𝐷 ) ↔ ⟨ 𝑦 , 𝑥 ⟩ ∈ ∪ 𝑘 ∈ 𝐶 ( { 𝑘 } × 𝐷 ) )
22 eliunxp ⊢ ( ⟨ 𝑦 , 𝑥 ⟩ ∈ ∪ 𝑘 ∈ 𝐶 ( { 𝑘 } × 𝐷 ) ↔ ∃ 𝑘 ∃ 𝑗 ( ⟨ 𝑦 , 𝑥 ⟩ = ⟨ 𝑘 , 𝑗 ⟩ ∧ ( 𝑘 ∈ 𝐶 ∧ 𝑗 ∈ 𝐷 ) ) )
23 excom ⊢ ( ∃ 𝑘 ∃ 𝑗 ( ⟨ 𝑦 , 𝑥 ⟩ = ⟨ 𝑘 , 𝑗 ⟩ ∧ ( 𝑘 ∈ 𝐶 ∧ 𝑗 ∈ 𝐷 ) ) ↔ ∃ 𝑗 ∃ 𝑘 ( ⟨ 𝑦 , 𝑥 ⟩ = ⟨ 𝑘 , 𝑗 ⟩ ∧ ( 𝑘 ∈ 𝐶 ∧ 𝑗 ∈ 𝐷 ) ) )
24 21 22 23 3bitri ⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ◡ ∪ 𝑘 ∈ 𝐶 ( { 𝑘 } × 𝐷 ) ↔ ∃ 𝑗 ∃ 𝑘 ( ⟨ 𝑦 , 𝑥 ⟩ = ⟨ 𝑘 , 𝑗 ⟩ ∧ ( 𝑘 ∈ 𝐶 ∧ 𝑗 ∈ 𝐷 ) ) )
25 19 20 24 3bitr4g ⊢ ( 𝜑 → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ ◡ ∪ 𝑘 ∈ 𝐶 ( { 𝑘 } × 𝐷 ) ) )
26 9 10 25 eqrelrdv ⊢ ( 𝜑 → ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) = ◡ ∪ 𝑘 ∈ 𝐶 ( { 𝑘 } × 𝐷 ) )
27 nfcv ⊢ Ⅎ 𝑚 ( { 𝑗 } × 𝐵 )
28 nfcv ⊢ Ⅎ 𝑗 { 𝑚 }
29 nfcsb1v ⊢ Ⅎ 𝑗 ⦋ 𝑚 / 𝑗 ⦌ 𝐵
30 28 29 nfxp ⊢ Ⅎ 𝑗 ( { 𝑚 } × ⦋ 𝑚 / 𝑗 ⦌ 𝐵 )
31 sneq ⊢ ( 𝑗 = 𝑚 → { 𝑗 } = { 𝑚 } )
32 csbeq1a ⊢ ( 𝑗 = 𝑚 → 𝐵 = ⦋ 𝑚 / 𝑗 ⦌ 𝐵 )
33 31 32 xpeq12d ⊢ ( 𝑗 = 𝑚 → ( { 𝑗 } × 𝐵 ) = ( { 𝑚 } × ⦋ 𝑚 / 𝑗 ⦌ 𝐵 ) )
34 27 30 33 cbviun ⊢ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) = ∪ 𝑚 ∈ 𝐴 ( { 𝑚 } × ⦋ 𝑚 / 𝑗 ⦌ 𝐵 )
35 nfcv ⊢ Ⅎ 𝑛 ( { 𝑘 } × 𝐷 )
36 nfcv ⊢ Ⅎ 𝑘 { 𝑛 }
37 nfcsb1v ⊢ Ⅎ 𝑘 ⦋ 𝑛 / 𝑘 ⦌ 𝐷
38 36 37 nfxp ⊢ Ⅎ 𝑘 ( { 𝑛 } × ⦋ 𝑛 / 𝑘 ⦌ 𝐷 )
39 sneq ⊢ ( 𝑘 = 𝑛 → { 𝑘 } = { 𝑛 } )
40 csbeq1a ⊢ ( 𝑘 = 𝑛 → 𝐷 = ⦋ 𝑛 / 𝑘 ⦌ 𝐷 )
41 39 40 xpeq12d ⊢ ( 𝑘 = 𝑛 → ( { 𝑘 } × 𝐷 ) = ( { 𝑛 } × ⦋ 𝑛 / 𝑘 ⦌ 𝐷 ) )
42 35 38 41 cbviun ⊢ ∪ 𝑘 ∈ 𝐶 ( { 𝑘 } × 𝐷 ) = ∪ 𝑛 ∈ 𝐶 ( { 𝑛 } × ⦋ 𝑛 / 𝑘 ⦌ 𝐷 )
43 42 cnveqi ⊢ ◡ ∪ 𝑘 ∈ 𝐶 ( { 𝑘 } × 𝐷 ) = ◡ ∪ 𝑛 ∈ 𝐶 ( { 𝑛 } × ⦋ 𝑛 / 𝑘 ⦌ 𝐷 )
44 26 34 43 3eqtr3g ⊢ ( 𝜑 → ∪ 𝑚 ∈ 𝐴 ( { 𝑚 } × ⦋ 𝑚 / 𝑗 ⦌ 𝐵 ) = ◡ ∪ 𝑛 ∈ 𝐶 ( { 𝑛 } × ⦋ 𝑛 / 𝑘 ⦌ 𝐷 ) )
45 44 sumeq1d ⊢ ( 𝜑 → Σ 𝑧 ∈ ∪ 𝑚 ∈ 𝐴 ( { 𝑚 } × ⦋ 𝑚 / 𝑗 ⦌ 𝐵 ) ⦋ ( 2nd ‘ 𝑧 ) / 𝑘 ⦌ ⦋ ( 1st ‘ 𝑧 ) / 𝑗 ⦌ 𝐸 = Σ 𝑧 ∈ ◡ ∪ 𝑛 ∈ 𝐶 ( { 𝑛 } × ⦋ 𝑛 / 𝑘 ⦌ 𝐷 ) ⦋ ( 2nd ‘ 𝑧 ) / 𝑘 ⦌ ⦋ ( 1st ‘ 𝑧 ) / 𝑗 ⦌ 𝐸 )
46 vex ⊢ 𝑛 ∈ V
47 vex ⊢ 𝑚 ∈ V
48 46 47 op1std ⊢ ( 𝑤 = ⟨ 𝑛 , 𝑚 ⟩ → ( 1st ‘ 𝑤 ) = 𝑛 )
49 48 csbeq1d ⊢ ( 𝑤 = ⟨ 𝑛 , 𝑚 ⟩ → ⦋ ( 1st ‘ 𝑤 ) / 𝑘 ⦌ ⦋ ( 2nd ‘ 𝑤 ) / 𝑗 ⦌ 𝐸 = ⦋ 𝑛 / 𝑘 ⦌ ⦋ ( 2nd ‘ 𝑤 ) / 𝑗 ⦌ 𝐸 )
50 46 47 op2ndd ⊢ ( 𝑤 = ⟨ 𝑛 , 𝑚 ⟩ → ( 2nd ‘ 𝑤 ) = 𝑚 )
51 50 csbeq1d ⊢ ( 𝑤 = ⟨ 𝑛 , 𝑚 ⟩ → ⦋ ( 2nd ‘ 𝑤 ) / 𝑗 ⦌ 𝐸 = ⦋ 𝑚 / 𝑗 ⦌ 𝐸 )
52 51 csbeq2dv ⊢ ( 𝑤 = ⟨ 𝑛 , 𝑚 ⟩ → ⦋ 𝑛 / 𝑘 ⦌ ⦋ ( 2nd ‘ 𝑤 ) / 𝑗 ⦌ 𝐸 = ⦋ 𝑛 / 𝑘 ⦌ ⦋ 𝑚 / 𝑗 ⦌ 𝐸 )
53 49 52 eqtrd ⊢ ( 𝑤 = ⟨ 𝑛 , 𝑚 ⟩ → ⦋ ( 1st ‘ 𝑤 ) / 𝑘 ⦌ ⦋ ( 2nd ‘ 𝑤 ) / 𝑗 ⦌ 𝐸 = ⦋ 𝑛 / 𝑘 ⦌ ⦋ 𝑚 / 𝑗 ⦌ 𝐸 )
54 47 46 op2ndd ⊢ ( 𝑧 = ⟨ 𝑚 , 𝑛 ⟩ → ( 2nd ‘ 𝑧 ) = 𝑛 )
55 54 csbeq1d ⊢ ( 𝑧 = ⟨ 𝑚 , 𝑛 ⟩ → ⦋ ( 2nd ‘ 𝑧 ) / 𝑘 ⦌ ⦋ ( 1st ‘ 𝑧 ) / 𝑗 ⦌ 𝐸 = ⦋ 𝑛 / 𝑘 ⦌ ⦋ ( 1st ‘ 𝑧 ) / 𝑗 ⦌ 𝐸 )
56 47 46 op1std ⊢ ( 𝑧 = ⟨ 𝑚 , 𝑛 ⟩ → ( 1st ‘ 𝑧 ) = 𝑚 )
57 56 csbeq1d ⊢ ( 𝑧 = ⟨ 𝑚 , 𝑛 ⟩ → ⦋ ( 1st ‘ 𝑧 ) / 𝑗 ⦌ 𝐸 = ⦋ 𝑚 / 𝑗 ⦌ 𝐸 )
58 57 csbeq2dv ⊢ ( 𝑧 = ⟨ 𝑚 , 𝑛 ⟩ → ⦋ 𝑛 / 𝑘 ⦌ ⦋ ( 1st ‘ 𝑧 ) / 𝑗 ⦌ 𝐸 = ⦋ 𝑛 / 𝑘 ⦌ ⦋ 𝑚 / 𝑗 ⦌ 𝐸 )
59 55 58 eqtrd ⊢ ( 𝑧 = ⟨ 𝑚 , 𝑛 ⟩ → ⦋ ( 2nd ‘ 𝑧 ) / 𝑘 ⦌ ⦋ ( 1st ‘ 𝑧 ) / 𝑗 ⦌ 𝐸 = ⦋ 𝑛 / 𝑘 ⦌ ⦋ 𝑚 / 𝑗 ⦌ 𝐸 )
60 snfi ⊢ { 𝑛 } ∈ Fin
61 1 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐶 ) → 𝐴 ∈ Fin )
62 47 46 opelcnv ⊢ ( ⟨ 𝑚 , 𝑛 ⟩ ∈ ◡ ∪ 𝑘 ∈ 𝐶 ( { 𝑘 } × 𝐷 ) ↔ ⟨ 𝑛 , 𝑚 ⟩ ∈ ∪ 𝑘 ∈ 𝐶 ( { 𝑘 } × 𝐷 ) )
63 37 40 opeliunxp2f ⊢ ( ⟨ 𝑛 , 𝑚 ⟩ ∈ ∪ 𝑘 ∈ 𝐶 ( { 𝑘 } × 𝐷 ) ↔ ( 𝑛 ∈ 𝐶 ∧ 𝑚 ∈ ⦋ 𝑛 / 𝑘 ⦌ 𝐷 ) )
64 62 63 sylbbr ⊢ ( ( 𝑛 ∈ 𝐶 ∧ 𝑚 ∈ ⦋ 𝑛 / 𝑘 ⦌ 𝐷 ) → ⟨ 𝑚 , 𝑛 ⟩ ∈ ◡ ∪ 𝑘 ∈ 𝐶 ( { 𝑘 } × 𝐷 ) )
65 64 adantl ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ 𝐶 ∧ 𝑚 ∈ ⦋ 𝑛 / 𝑘 ⦌ 𝐷 ) ) → ⟨ 𝑚 , 𝑛 ⟩ ∈ ◡ ∪ 𝑘 ∈ 𝐶 ( { 𝑘 } × 𝐷 ) )
66 26 adantr ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ 𝐶 ∧ 𝑚 ∈ ⦋ 𝑛 / 𝑘 ⦌ 𝐷 ) ) → ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) = ◡ ∪ 𝑘 ∈ 𝐶 ( { 𝑘 } × 𝐷 ) )
67 65 66 eleqtrrd ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ 𝐶 ∧ 𝑚 ∈ ⦋ 𝑛 / 𝑘 ⦌ 𝐷 ) ) → ⟨ 𝑚 , 𝑛 ⟩ ∈ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) )
68 eliun ⊢ ( ⟨ 𝑚 , 𝑛 ⟩ ∈ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ↔ ∃ 𝑗 ∈ 𝐴 ⟨ 𝑚 , 𝑛 ⟩ ∈ ( { 𝑗 } × 𝐵 ) )
69 67 68 sylib ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ 𝐶 ∧ 𝑚 ∈ ⦋ 𝑛 / 𝑘 ⦌ 𝐷 ) ) → ∃ 𝑗 ∈ 𝐴 ⟨ 𝑚 , 𝑛 ⟩ ∈ ( { 𝑗 } × 𝐵 ) )
70 opelxp ⊢ ( ⟨ 𝑚 , 𝑛 ⟩ ∈ ( { 𝑗 } × 𝐵 ) ↔ ( 𝑚 ∈ { 𝑗 } ∧ 𝑛 ∈ 𝐵 ) )
71 70 bilani ⊢ ( ( 𝑗 ∈ 𝐴 ∧ ⟨ 𝑚 , 𝑛 ⟩ ∈ ( { 𝑗 } × 𝐵 ) ) → ( 𝑚 ∈ { 𝑗 } ∧ 𝑛 ∈ 𝐵 ) )
72 71 simpld ⊢ ( ( 𝑗 ∈ 𝐴 ∧ ⟨ 𝑚 , 𝑛 ⟩ ∈ ( { 𝑗 } × 𝐵 ) ) → 𝑚 ∈ { 𝑗 } )
73 elsni ⊢ ( 𝑚 ∈ { 𝑗 } → 𝑚 = 𝑗 )
74 72 73 syl ⊢ ( ( 𝑗 ∈ 𝐴 ∧ ⟨ 𝑚 , 𝑛 ⟩ ∈ ( { 𝑗 } × 𝐵 ) ) → 𝑚 = 𝑗 )
75 simpl ⊢ ( ( 𝑗 ∈ 𝐴 ∧ ⟨ 𝑚 , 𝑛 ⟩ ∈ ( { 𝑗 } × 𝐵 ) ) → 𝑗 ∈ 𝐴 )
76 74 75 eqeltrd ⊢ ( ( 𝑗 ∈ 𝐴 ∧ ⟨ 𝑚 , 𝑛 ⟩ ∈ ( { 𝑗 } × 𝐵 ) ) → 𝑚 ∈ 𝐴 )
77 76 rexlimiva ⊢ ( ∃ 𝑗 ∈ 𝐴 ⟨ 𝑚 , 𝑛 ⟩ ∈ ( { 𝑗 } × 𝐵 ) → 𝑚 ∈ 𝐴 )
78 69 77 syl ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ 𝐶 ∧ 𝑚 ∈ ⦋ 𝑛 / 𝑘 ⦌ 𝐷 ) ) → 𝑚 ∈ 𝐴 )
79 78 expr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐶 ) → ( 𝑚 ∈ ⦋ 𝑛 / 𝑘 ⦌ 𝐷 → 𝑚 ∈ 𝐴 ) )
80 79 ssrdv ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐶 ) → ⦋ 𝑛 / 𝑘 ⦌ 𝐷 ⊆ 𝐴 )
81 61 80 ssfid ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐶 ) → ⦋ 𝑛 / 𝑘 ⦌ 𝐷 ∈ Fin )
82 xpfi ⊢ ( ( { 𝑛 } ∈ Fin ∧ ⦋ 𝑛 / 𝑘 ⦌ 𝐷 ∈ Fin ) → ( { 𝑛 } × ⦋ 𝑛 / 𝑘 ⦌ 𝐷 ) ∈ Fin )
83 60 81 82 sylancr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐶 ) → ( { 𝑛 } × ⦋ 𝑛 / 𝑘 ⦌ 𝐷 ) ∈ Fin )
84 83 ralrimiva ⊢ ( 𝜑 → ∀ 𝑛 ∈ 𝐶 ( { 𝑛 } × ⦋ 𝑛 / 𝑘 ⦌ 𝐷 ) ∈ Fin )
85 iunfi ⊢ ( ( 𝐶 ∈ Fin ∧ ∀ 𝑛 ∈ 𝐶 ( { 𝑛 } × ⦋ 𝑛 / 𝑘 ⦌ 𝐷 ) ∈ Fin ) → ∪ 𝑛 ∈ 𝐶 ( { 𝑛 } × ⦋ 𝑛 / 𝑘 ⦌ 𝐷 ) ∈ Fin )
86 2 84 85 syl2anc ⊢ ( 𝜑 → ∪ 𝑛 ∈ 𝐶 ( { 𝑛 } × ⦋ 𝑛 / 𝑘 ⦌ 𝐷 ) ∈ Fin )
87 reliun ⊢ ( Rel ∪ 𝑛 ∈ 𝐶 ( { 𝑛 } × ⦋ 𝑛 / 𝑘 ⦌ 𝐷 ) ↔ ∀ 𝑛 ∈ 𝐶 Rel ( { 𝑛 } × ⦋ 𝑛 / 𝑘 ⦌ 𝐷 ) )
88 relxp ⊢ Rel ( { 𝑛 } × ⦋ 𝑛 / 𝑘 ⦌ 𝐷 )
89 88 a1i ⊢ ( 𝑛 ∈ 𝐶 → Rel ( { 𝑛 } × ⦋ 𝑛 / 𝑘 ⦌ 𝐷 ) )
90 87 89 mprgbir ⊢ Rel ∪ 𝑛 ∈ 𝐶 ( { 𝑛 } × ⦋ 𝑛 / 𝑘 ⦌ 𝐷 )
91 90 a1i ⊢ ( 𝜑 → Rel ∪ 𝑛 ∈ 𝐶 ( { 𝑛 } × ⦋ 𝑛 / 𝑘 ⦌ 𝐷 ) )
92 csbeq1 ⊢ ( 𝑚 = ( 2nd ‘ 𝑤 ) → ⦋ 𝑚 / 𝑗 ⦌ 𝐸 = ⦋ ( 2nd ‘ 𝑤 ) / 𝑗 ⦌ 𝐸 )
93 92 csbeq2dv ⊢ ( 𝑚 = ( 2nd ‘ 𝑤 ) → ⦋ ( 1st ‘ 𝑤 ) / 𝑘 ⦌ ⦋ 𝑚 / 𝑗 ⦌ 𝐸 = ⦋ ( 1st ‘ 𝑤 ) / 𝑘 ⦌ ⦋ ( 2nd ‘ 𝑤 ) / 𝑗 ⦌ 𝐸 )
94 93 eleq1d ⊢ ( 𝑚 = ( 2nd ‘ 𝑤 ) → ( ⦋ ( 1st ‘ 𝑤 ) / 𝑘 ⦌ ⦋ 𝑚 / 𝑗 ⦌ 𝐸 ∈ ℂ ↔ ⦋ ( 1st ‘ 𝑤 ) / 𝑘 ⦌ ⦋ ( 2nd ‘ 𝑤 ) / 𝑗 ⦌ 𝐸 ∈ ℂ ) )
95 csbeq1 ⊢ ( 𝑛 = ( 1st ‘ 𝑤 ) → ⦋ 𝑛 / 𝑘 ⦌ 𝐷 = ⦋ ( 1st ‘ 𝑤 ) / 𝑘 ⦌ 𝐷 )
96 csbeq1 ⊢ ( 𝑛 = ( 1st ‘ 𝑤 ) → ⦋ 𝑛 / 𝑘 ⦌ ⦋ 𝑚 / 𝑗 ⦌ 𝐸 = ⦋ ( 1st ‘ 𝑤 ) / 𝑘 ⦌ ⦋ 𝑚 / 𝑗 ⦌ 𝐸 )
97 96 eleq1d ⊢ ( 𝑛 = ( 1st ‘ 𝑤 ) → ( ⦋ 𝑛 / 𝑘 ⦌ ⦋ 𝑚 / 𝑗 ⦌ 𝐸 ∈ ℂ ↔ ⦋ ( 1st ‘ 𝑤 ) / 𝑘 ⦌ ⦋ 𝑚 / 𝑗 ⦌ 𝐸 ∈ ℂ ) )
98 95 97 raleqbidv ⊢ ( 𝑛 = ( 1st ‘ 𝑤 ) → ( ∀ 𝑚 ∈ ⦋ 𝑛 / 𝑘 ⦌ 𝐷 ⦋ 𝑛 / 𝑘 ⦌ ⦋ 𝑚 / 𝑗 ⦌ 𝐸 ∈ ℂ ↔ ∀ 𝑚 ∈ ⦋ ( 1st ‘ 𝑤 ) / 𝑘 ⦌ 𝐷 ⦋ ( 1st ‘ 𝑤 ) / 𝑘 ⦌ ⦋ 𝑚 / 𝑗 ⦌ 𝐸 ∈ ℂ ) )
99 simpl ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ 𝐶 ∧ 𝑚 ∈ ⦋ 𝑛 / 𝑘 ⦌ 𝐷 ) ) → 𝜑 )
100 29 nfcri ⊢ Ⅎ 𝑗 𝑛 ∈ ⦋ 𝑚 / 𝑗 ⦌ 𝐵
101 73 equcomd ⊢ ( 𝑚 ∈ { 𝑗 } → 𝑗 = 𝑚 )
102 101 32 syl ⊢ ( 𝑚 ∈ { 𝑗 } → 𝐵 = ⦋ 𝑚 / 𝑗 ⦌ 𝐵 )
103 102 eleq2d ⊢ ( 𝑚 ∈ { 𝑗 } → ( 𝑛 ∈ 𝐵 ↔ 𝑛 ∈ ⦋ 𝑚 / 𝑗 ⦌ 𝐵 ) )
104 103 biimpa ⊢ ( ( 𝑚 ∈ { 𝑗 } ∧ 𝑛 ∈ 𝐵 ) → 𝑛 ∈ ⦋ 𝑚 / 𝑗 ⦌ 𝐵 )
105 70 104 sylbi ⊢ ( ⟨ 𝑚 , 𝑛 ⟩ ∈ ( { 𝑗 } × 𝐵 ) → 𝑛 ∈ ⦋ 𝑚 / 𝑗 ⦌ 𝐵 )
106 105 a1i ⊢ ( 𝑗 ∈ 𝐴 → ( ⟨ 𝑚 , 𝑛 ⟩ ∈ ( { 𝑗 } × 𝐵 ) → 𝑛 ∈ ⦋ 𝑚 / 𝑗 ⦌ 𝐵 ) )
107 100 106 rexlimi ⊢ ( ∃ 𝑗 ∈ 𝐴 ⟨ 𝑚 , 𝑛 ⟩ ∈ ( { 𝑗 } × 𝐵 ) → 𝑛 ∈ ⦋ 𝑚 / 𝑗 ⦌ 𝐵 )
108 69 107 syl ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ 𝐶 ∧ 𝑚 ∈ ⦋ 𝑛 / 𝑘 ⦌ 𝐷 ) ) → 𝑛 ∈ ⦋ 𝑚 / 𝑗 ⦌ 𝐵 )
109 5 ralrimivva ⊢ ( 𝜑 → ∀ 𝑗 ∈ 𝐴 ∀ 𝑘 ∈ 𝐵 𝐸 ∈ ℂ )
110 nfcsb1v ⊢ Ⅎ 𝑗 ⦋ 𝑚 / 𝑗 ⦌ 𝐸
111 110 nfel1 ⊢ Ⅎ 𝑗 ⦋ 𝑚 / 𝑗 ⦌ 𝐸 ∈ ℂ
112 29 111 nfralw ⊢ Ⅎ 𝑗 ∀ 𝑘 ∈ ⦋ 𝑚 / 𝑗 ⦌ 𝐵 ⦋ 𝑚 / 𝑗 ⦌ 𝐸 ∈ ℂ
113 csbeq1a ⊢ ( 𝑗 = 𝑚 → 𝐸 = ⦋ 𝑚 / 𝑗 ⦌ 𝐸 )
114 113 eleq1d ⊢ ( 𝑗 = 𝑚 → ( 𝐸 ∈ ℂ ↔ ⦋ 𝑚 / 𝑗 ⦌ 𝐸 ∈ ℂ ) )
115 32 114 raleqbidv ⊢ ( 𝑗 = 𝑚 → ( ∀ 𝑘 ∈ 𝐵 𝐸 ∈ ℂ ↔ ∀ 𝑘 ∈ ⦋ 𝑚 / 𝑗 ⦌ 𝐵 ⦋ 𝑚 / 𝑗 ⦌ 𝐸 ∈ ℂ ) )
116 112 115 rspc ⊢ ( 𝑚 ∈ 𝐴 → ( ∀ 𝑗 ∈ 𝐴 ∀ 𝑘 ∈ 𝐵 𝐸 ∈ ℂ → ∀ 𝑘 ∈ ⦋ 𝑚 / 𝑗 ⦌ 𝐵 ⦋ 𝑚 / 𝑗 ⦌ 𝐸 ∈ ℂ ) )
117 109 116 mpan9 ⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝐴 ) → ∀ 𝑘 ∈ ⦋ 𝑚 / 𝑗 ⦌ 𝐵 ⦋ 𝑚 / 𝑗 ⦌ 𝐸 ∈ ℂ )
118 nfcsb1v ⊢ Ⅎ 𝑘 ⦋ 𝑛 / 𝑘 ⦌ ⦋ 𝑚 / 𝑗 ⦌ 𝐸
119 118 nfel1 ⊢ Ⅎ 𝑘 ⦋ 𝑛 / 𝑘 ⦌ ⦋ 𝑚 / 𝑗 ⦌ 𝐸 ∈ ℂ
120 csbeq1a ⊢ ( 𝑘 = 𝑛 → ⦋ 𝑚 / 𝑗 ⦌ 𝐸 = ⦋ 𝑛 / 𝑘 ⦌ ⦋ 𝑚 / 𝑗 ⦌ 𝐸 )
121 120 eleq1d ⊢ ( 𝑘 = 𝑛 → ( ⦋ 𝑚 / 𝑗 ⦌ 𝐸 ∈ ℂ ↔ ⦋ 𝑛 / 𝑘 ⦌ ⦋ 𝑚 / 𝑗 ⦌ 𝐸 ∈ ℂ ) )
122 119 121 rspc ⊢ ( 𝑛 ∈ ⦋ 𝑚 / 𝑗 ⦌ 𝐵 → ( ∀ 𝑘 ∈ ⦋ 𝑚 / 𝑗 ⦌ 𝐵 ⦋ 𝑚 / 𝑗 ⦌ 𝐸 ∈ ℂ → ⦋ 𝑛 / 𝑘 ⦌ ⦋ 𝑚 / 𝑗 ⦌ 𝐸 ∈ ℂ ) )
123 117 122 syl5com ⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝐴 ) → ( 𝑛 ∈ ⦋ 𝑚 / 𝑗 ⦌ 𝐵 → ⦋ 𝑛 / 𝑘 ⦌ ⦋ 𝑚 / 𝑗 ⦌ 𝐸 ∈ ℂ ) )
124 123 impr ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ 𝐴 ∧ 𝑛 ∈ ⦋ 𝑚 / 𝑗 ⦌ 𝐵 ) ) → ⦋ 𝑛 / 𝑘 ⦌ ⦋ 𝑚 / 𝑗 ⦌ 𝐸 ∈ ℂ )
125 99 78 108 124 syl12anc ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ 𝐶 ∧ 𝑚 ∈ ⦋ 𝑛 / 𝑘 ⦌ 𝐷 ) ) → ⦋ 𝑛 / 𝑘 ⦌ ⦋ 𝑚 / 𝑗 ⦌ 𝐸 ∈ ℂ )
126 125 ralrimivva ⊢ ( 𝜑 → ∀ 𝑛 ∈ 𝐶 ∀ 𝑚 ∈ ⦋ 𝑛 / 𝑘 ⦌ 𝐷 ⦋ 𝑛 / 𝑘 ⦌ ⦋ 𝑚 / 𝑗 ⦌ 𝐸 ∈ ℂ )
127 126 adantr ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ∪ 𝑛 ∈ 𝐶 ( { 𝑛 } × ⦋ 𝑛 / 𝑘 ⦌ 𝐷 ) ) → ∀ 𝑛 ∈ 𝐶 ∀ 𝑚 ∈ ⦋ 𝑛 / 𝑘 ⦌ 𝐷 ⦋ 𝑛 / 𝑘 ⦌ ⦋ 𝑚 / 𝑗 ⦌ 𝐸 ∈ ℂ )
128 eliun ⊢ ( 𝑤 ∈ ∪ 𝑛 ∈ 𝐶 ( { 𝑛 } × ⦋ 𝑛 / 𝑘 ⦌ 𝐷 ) ↔ ∃ 𝑛 ∈ 𝐶 𝑤 ∈ ( { 𝑛 } × ⦋ 𝑛 / 𝑘 ⦌ 𝐷 ) )
129 128 bilani ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ∪ 𝑛 ∈ 𝐶 ( { 𝑛 } × ⦋ 𝑛 / 𝑘 ⦌ 𝐷 ) ) → ∃ 𝑛 ∈ 𝐶 𝑤 ∈ ( { 𝑛 } × ⦋ 𝑛 / 𝑘 ⦌ 𝐷 ) )
130 xp1st ⊢ ( 𝑤 ∈ ( { 𝑛 } × ⦋ 𝑛 / 𝑘 ⦌ 𝐷 ) → ( 1st ‘ 𝑤 ) ∈ { 𝑛 } )
131 130 adantl ⊢ ( ( 𝑛 ∈ 𝐶 ∧ 𝑤 ∈ ( { 𝑛 } × ⦋ 𝑛 / 𝑘 ⦌ 𝐷 ) ) → ( 1st ‘ 𝑤 ) ∈ { 𝑛 } )
132 elsni ⊢ ( ( 1st ‘ 𝑤 ) ∈ { 𝑛 } → ( 1st ‘ 𝑤 ) = 𝑛 )
133 131 132 syl ⊢ ( ( 𝑛 ∈ 𝐶 ∧ 𝑤 ∈ ( { 𝑛 } × ⦋ 𝑛 / 𝑘 ⦌ 𝐷 ) ) → ( 1st ‘ 𝑤 ) = 𝑛 )
134 simpl ⊢ ( ( 𝑛 ∈ 𝐶 ∧ 𝑤 ∈ ( { 𝑛 } × ⦋ 𝑛 / 𝑘 ⦌ 𝐷 ) ) → 𝑛 ∈ 𝐶 )
135 133 134 eqeltrd ⊢ ( ( 𝑛 ∈ 𝐶 ∧ 𝑤 ∈ ( { 𝑛 } × ⦋ 𝑛 / 𝑘 ⦌ 𝐷 ) ) → ( 1st ‘ 𝑤 ) ∈ 𝐶 )
136 135 rexlimiva ⊢ ( ∃ 𝑛 ∈ 𝐶 𝑤 ∈ ( { 𝑛 } × ⦋ 𝑛 / 𝑘 ⦌ 𝐷 ) → ( 1st ‘ 𝑤 ) ∈ 𝐶 )
137 129 136 syl ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ∪ 𝑛 ∈ 𝐶 ( { 𝑛 } × ⦋ 𝑛 / 𝑘 ⦌ 𝐷 ) ) → ( 1st ‘ 𝑤 ) ∈ 𝐶 )
138 98 127 137 rspcdva ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ∪ 𝑛 ∈ 𝐶 ( { 𝑛 } × ⦋ 𝑛 / 𝑘 ⦌ 𝐷 ) ) → ∀ 𝑚 ∈ ⦋ ( 1st ‘ 𝑤 ) / 𝑘 ⦌ 𝐷 ⦋ ( 1st ‘ 𝑤 ) / 𝑘 ⦌ ⦋ 𝑚 / 𝑗 ⦌ 𝐸 ∈ ℂ )
139 xp2nd ⊢ ( 𝑤 ∈ ( { 𝑛 } × ⦋ 𝑛 / 𝑘 ⦌ 𝐷 ) → ( 2nd ‘ 𝑤 ) ∈ ⦋ 𝑛 / 𝑘 ⦌ 𝐷 )
140 139 adantl ⊢ ( ( 𝑛 ∈ 𝐶 ∧ 𝑤 ∈ ( { 𝑛 } × ⦋ 𝑛 / 𝑘 ⦌ 𝐷 ) ) → ( 2nd ‘ 𝑤 ) ∈ ⦋ 𝑛 / 𝑘 ⦌ 𝐷 )
141 133 csbeq1d ⊢ ( ( 𝑛 ∈ 𝐶 ∧ 𝑤 ∈ ( { 𝑛 } × ⦋ 𝑛 / 𝑘 ⦌ 𝐷 ) ) → ⦋ ( 1st ‘ 𝑤 ) / 𝑘 ⦌ 𝐷 = ⦋ 𝑛 / 𝑘 ⦌ 𝐷 )
142 140 141 eleqtrrd ⊢ ( ( 𝑛 ∈ 𝐶 ∧ 𝑤 ∈ ( { 𝑛 } × ⦋ 𝑛 / 𝑘 ⦌ 𝐷 ) ) → ( 2nd ‘ 𝑤 ) ∈ ⦋ ( 1st ‘ 𝑤 ) / 𝑘 ⦌ 𝐷 )
143 142 rexlimiva ⊢ ( ∃ 𝑛 ∈ 𝐶 𝑤 ∈ ( { 𝑛 } × ⦋ 𝑛 / 𝑘 ⦌ 𝐷 ) → ( 2nd ‘ 𝑤 ) ∈ ⦋ ( 1st ‘ 𝑤 ) / 𝑘 ⦌ 𝐷 )
144 129 143 syl ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ∪ 𝑛 ∈ 𝐶 ( { 𝑛 } × ⦋ 𝑛 / 𝑘 ⦌ 𝐷 ) ) → ( 2nd ‘ 𝑤 ) ∈ ⦋ ( 1st ‘ 𝑤 ) / 𝑘 ⦌ 𝐷 )
145 94 138 144 rspcdva ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ∪ 𝑛 ∈ 𝐶 ( { 𝑛 } × ⦋ 𝑛 / 𝑘 ⦌ 𝐷 ) ) → ⦋ ( 1st ‘ 𝑤 ) / 𝑘 ⦌ ⦋ ( 2nd ‘ 𝑤 ) / 𝑗 ⦌ 𝐸 ∈ ℂ )
146 53 59 86 91 145 fsumcnv ⊢ ( 𝜑 → Σ 𝑤 ∈ ∪ 𝑛 ∈ 𝐶 ( { 𝑛 } × ⦋ 𝑛 / 𝑘 ⦌ 𝐷 ) ⦋ ( 1st ‘ 𝑤 ) / 𝑘 ⦌ ⦋ ( 2nd ‘ 𝑤 ) / 𝑗 ⦌ 𝐸 = Σ 𝑧 ∈ ◡ ∪ 𝑛 ∈ 𝐶 ( { 𝑛 } × ⦋ 𝑛 / 𝑘 ⦌ 𝐷 ) ⦋ ( 2nd ‘ 𝑧 ) / 𝑘 ⦌ ⦋ ( 1st ‘ 𝑧 ) / 𝑗 ⦌ 𝐸 )
147 45 146 eqtr4d ⊢ ( 𝜑 → Σ 𝑧 ∈ ∪ 𝑚 ∈ 𝐴 ( { 𝑚 } × ⦋ 𝑚 / 𝑗 ⦌ 𝐵 ) ⦋ ( 2nd ‘ 𝑧 ) / 𝑘 ⦌ ⦋ ( 1st ‘ 𝑧 ) / 𝑗 ⦌ 𝐸 = Σ 𝑤 ∈ ∪ 𝑛 ∈ 𝐶 ( { 𝑛 } × ⦋ 𝑛 / 𝑘 ⦌ 𝐷 ) ⦋ ( 1st ‘ 𝑤 ) / 𝑘 ⦌ ⦋ ( 2nd ‘ 𝑤 ) / 𝑗 ⦌ 𝐸 )
148 3 ralrimiva ⊢ ( 𝜑 → ∀ 𝑗 ∈ 𝐴 𝐵 ∈ Fin )
149 29 nfel1 ⊢ Ⅎ 𝑗 ⦋ 𝑚 / 𝑗 ⦌ 𝐵 ∈ Fin
150 32 eleq1d ⊢ ( 𝑗 = 𝑚 → ( 𝐵 ∈ Fin ↔ ⦋ 𝑚 / 𝑗 ⦌ 𝐵 ∈ Fin ) )
151 149 150 rspc ⊢ ( 𝑚 ∈ 𝐴 → ( ∀ 𝑗 ∈ 𝐴 𝐵 ∈ Fin → ⦋ 𝑚 / 𝑗 ⦌ 𝐵 ∈ Fin ) )
152 148 151 mpan9 ⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝐴 ) → ⦋ 𝑚 / 𝑗 ⦌ 𝐵 ∈ Fin )
153 59 1 152 124 fsum2d ⊢ ( 𝜑 → Σ 𝑚 ∈ 𝐴 Σ 𝑛 ∈ ⦋ 𝑚 / 𝑗 ⦌ 𝐵 ⦋ 𝑛 / 𝑘 ⦌ ⦋ 𝑚 / 𝑗 ⦌ 𝐸 = Σ 𝑧 ∈ ∪ 𝑚 ∈ 𝐴 ( { 𝑚 } × ⦋ 𝑚 / 𝑗 ⦌ 𝐵 ) ⦋ ( 2nd ‘ 𝑧 ) / 𝑘 ⦌ ⦋ ( 1st ‘ 𝑧 ) / 𝑗 ⦌ 𝐸 )
154 53 2 81 125 fsum2d ⊢ ( 𝜑 → Σ 𝑛 ∈ 𝐶 Σ 𝑚 ∈ ⦋ 𝑛 / 𝑘 ⦌ 𝐷 ⦋ 𝑛 / 𝑘 ⦌ ⦋ 𝑚 / 𝑗 ⦌ 𝐸 = Σ 𝑤 ∈ ∪ 𝑛 ∈ 𝐶 ( { 𝑛 } × ⦋ 𝑛 / 𝑘 ⦌ 𝐷 ) ⦋ ( 1st ‘ 𝑤 ) / 𝑘 ⦌ ⦋ ( 2nd ‘ 𝑤 ) / 𝑗 ⦌ 𝐸 )
155 147 153 154 3eqtr4d ⊢ ( 𝜑 → Σ 𝑚 ∈ 𝐴 Σ 𝑛 ∈ ⦋ 𝑚 / 𝑗 ⦌ 𝐵 ⦋ 𝑛 / 𝑘 ⦌ ⦋ 𝑚 / 𝑗 ⦌ 𝐸 = Σ 𝑛 ∈ 𝐶 Σ 𝑚 ∈ ⦋ 𝑛 / 𝑘 ⦌ 𝐷 ⦋ 𝑛 / 𝑘 ⦌ ⦋ 𝑚 / 𝑗 ⦌ 𝐸 )
156 csbeq1a ⊢ ( 𝑘 = 𝑛 → 𝐸 = ⦋ 𝑛 / 𝑘 ⦌ 𝐸 )
157 nfcv ⊢ Ⅎ 𝑛 𝐸
158 nfcsb1v ⊢ Ⅎ 𝑘 ⦋ 𝑛 / 𝑘 ⦌ 𝐸
159 156 157 158 cbvsum ⊢ Σ 𝑘 ∈ 𝐵 𝐸 = Σ 𝑛 ∈ 𝐵 ⦋ 𝑛 / 𝑘 ⦌ 𝐸
160 113 csbeq2dv ⊢ ( 𝑗 = 𝑚 → ⦋ 𝑛 / 𝑘 ⦌ 𝐸 = ⦋ 𝑛 / 𝑘 ⦌ ⦋ 𝑚 / 𝑗 ⦌ 𝐸 )
161 160 adantr ⊢ ( ( 𝑗 = 𝑚 ∧ 𝑛 ∈ 𝐵 ) → ⦋ 𝑛 / 𝑘 ⦌ 𝐸 = ⦋ 𝑛 / 𝑘 ⦌ ⦋ 𝑚 / 𝑗 ⦌ 𝐸 )
162 32 161 sumeq12dv ⊢ ( 𝑗 = 𝑚 → Σ 𝑛 ∈ 𝐵 ⦋ 𝑛 / 𝑘 ⦌ 𝐸 = Σ 𝑛 ∈ ⦋ 𝑚 / 𝑗 ⦌ 𝐵 ⦋ 𝑛 / 𝑘 ⦌ ⦋ 𝑚 / 𝑗 ⦌ 𝐸 )
163 159 162 eqtrid ⊢ ( 𝑗 = 𝑚 → Σ 𝑘 ∈ 𝐵 𝐸 = Σ 𝑛 ∈ ⦋ 𝑚 / 𝑗 ⦌ 𝐵 ⦋ 𝑛 / 𝑘 ⦌ ⦋ 𝑚 / 𝑗 ⦌ 𝐸 )
164 nfcv ⊢ Ⅎ 𝑚 Σ 𝑘 ∈ 𝐵 𝐸
165 nfcv ⊢ Ⅎ 𝑗 𝑛
166 165 110 nfcsbw ⊢ Ⅎ 𝑗 ⦋ 𝑛 / 𝑘 ⦌ ⦋ 𝑚 / 𝑗 ⦌ 𝐸
167 29 166 nfsum ⊢ Ⅎ 𝑗 Σ 𝑛 ∈ ⦋ 𝑚 / 𝑗 ⦌ 𝐵 ⦋ 𝑛 / 𝑘 ⦌ ⦋ 𝑚 / 𝑗 ⦌ 𝐸
168 163 164 167 cbvsum ⊢ Σ 𝑗 ∈ 𝐴 Σ 𝑘 ∈ 𝐵 𝐸 = Σ 𝑚 ∈ 𝐴 Σ 𝑛 ∈ ⦋ 𝑚 / 𝑗 ⦌ 𝐵 ⦋ 𝑛 / 𝑘 ⦌ ⦋ 𝑚 / 𝑗 ⦌ 𝐸
169 nfcv ⊢ Ⅎ 𝑚 𝐸
170 113 169 110 cbvsum ⊢ Σ 𝑗 ∈ 𝐷 𝐸 = Σ 𝑚 ∈ 𝐷 ⦋ 𝑚 / 𝑗 ⦌ 𝐸
171 120 adantr ⊢ ( ( 𝑘 = 𝑛 ∧ 𝑚 ∈ 𝐷 ) → ⦋ 𝑚 / 𝑗 ⦌ 𝐸 = ⦋ 𝑛 / 𝑘 ⦌ ⦋ 𝑚 / 𝑗 ⦌ 𝐸 )
172 40 171 sumeq12dv ⊢ ( 𝑘 = 𝑛 → Σ 𝑚 ∈ 𝐷 ⦋ 𝑚 / 𝑗 ⦌ 𝐸 = Σ 𝑚 ∈ ⦋ 𝑛 / 𝑘 ⦌ 𝐷 ⦋ 𝑛 / 𝑘 ⦌ ⦋ 𝑚 / 𝑗 ⦌ 𝐸 )
173 170 172 eqtrid ⊢ ( 𝑘 = 𝑛 → Σ 𝑗 ∈ 𝐷 𝐸 = Σ 𝑚 ∈ ⦋ 𝑛 / 𝑘 ⦌ 𝐷 ⦋ 𝑛 / 𝑘 ⦌ ⦋ 𝑚 / 𝑗 ⦌ 𝐸 )
174 nfcv ⊢ Ⅎ 𝑛 Σ 𝑗 ∈ 𝐷 𝐸
175 37 118 nfsum ⊢ Ⅎ 𝑘 Σ 𝑚 ∈ ⦋ 𝑛 / 𝑘 ⦌ 𝐷 ⦋ 𝑛 / 𝑘 ⦌ ⦋ 𝑚 / 𝑗 ⦌ 𝐸
176 173 174 175 cbvsum ⊢ Σ 𝑘 ∈ 𝐶 Σ 𝑗 ∈ 𝐷 𝐸 = Σ 𝑛 ∈ 𝐶 Σ 𝑚 ∈ ⦋ 𝑛 / 𝑘 ⦌ 𝐷 ⦋ 𝑛 / 𝑘 ⦌ ⦋ 𝑚 / 𝑗 ⦌ 𝐸
177 155 168 176 3eqtr4g ⊢ ( 𝜑 → Σ 𝑗 ∈ 𝐴 Σ 𝑘 ∈ 𝐵 𝐸 = Σ 𝑘 ∈ 𝐶 Σ 𝑗 ∈ 𝐷 𝐸 )