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 simpr ⊢ ( ( 𝑗 ∈ 𝐴 ∧ ⟨ 𝑚 , 𝑛 ⟩ ∈ ( { 𝑗 } × 𝐵 ) ) → ⟨ 𝑚 , 𝑛 ⟩ ∈ ( { 𝑗 } × 𝐵 ) )
71 opelxp ⊢ ( ⟨ 𝑚 , 𝑛 ⟩ ∈ ( { 𝑗 } × 𝐵 ) ↔ ( 𝑚 ∈ { 𝑗 } ∧ 𝑛 ∈ 𝐵 ) )
72 70 71 sylib ⊢ ( ( 𝑗 ∈ 𝐴 ∧ ⟨ 𝑚 , 𝑛 ⟩ ∈ ( { 𝑗 } × 𝐵 ) ) → ( 𝑚 ∈ { 𝑗 } ∧ 𝑛 ∈ 𝐵 ) )
73 72 simpld ⊢ ( ( 𝑗 ∈ 𝐴 ∧ ⟨ 𝑚 , 𝑛 ⟩ ∈ ( { 𝑗 } × 𝐵 ) ) → 𝑚 ∈ { 𝑗 } )
74 elsni ⊢ ( 𝑚 ∈ { 𝑗 } → 𝑚 = 𝑗 )
75 73 74 syl ⊢ ( ( 𝑗 ∈ 𝐴 ∧ ⟨ 𝑚 , 𝑛 ⟩ ∈ ( { 𝑗 } × 𝐵 ) ) → 𝑚 = 𝑗 )
76 simpl ⊢ ( ( 𝑗 ∈ 𝐴 ∧ ⟨ 𝑚 , 𝑛 ⟩ ∈ ( { 𝑗 } × 𝐵 ) ) → 𝑗 ∈ 𝐴 )
77 75 76 eqeltrd ⊢ ( ( 𝑗 ∈ 𝐴 ∧ ⟨ 𝑚 , 𝑛 ⟩ ∈ ( { 𝑗 } × 𝐵 ) ) → 𝑚 ∈ 𝐴 )
78 77 rexlimiva ⊢ ( ∃ 𝑗 ∈ 𝐴 ⟨ 𝑚 , 𝑛 ⟩ ∈ ( { 𝑗 } × 𝐵 ) → 𝑚 ∈ 𝐴 )
79 69 78 syl ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ 𝐶 ∧ 𝑚 ∈ ⦋ 𝑛 / 𝑘 ⦌ 𝐷 ) ) → 𝑚 ∈ 𝐴 )
80 79 expr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐶 ) → ( 𝑚 ∈ ⦋ 𝑛 / 𝑘 ⦌ 𝐷 → 𝑚 ∈ 𝐴 ) )
81 80 ssrdv ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐶 ) → ⦋ 𝑛 / 𝑘 ⦌ 𝐷 ⊆ 𝐴 )
82 61 81 ssfid ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐶 ) → ⦋ 𝑛 / 𝑘 ⦌ 𝐷 ∈ Fin )
83 xpfi ⊢ ( ( { 𝑛 } ∈ Fin ∧ ⦋ 𝑛 / 𝑘 ⦌ 𝐷 ∈ Fin ) → ( { 𝑛 } × ⦋ 𝑛 / 𝑘 ⦌ 𝐷 ) ∈ Fin )
84 60 82 83 sylancr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐶 ) → ( { 𝑛 } × ⦋ 𝑛 / 𝑘 ⦌ 𝐷 ) ∈ Fin )
85 84 ralrimiva ⊢ ( 𝜑 → ∀ 𝑛 ∈ 𝐶 ( { 𝑛 } × ⦋ 𝑛 / 𝑘 ⦌ 𝐷 ) ∈ Fin )
86 iunfi ⊢ ( ( 𝐶 ∈ Fin ∧ ∀ 𝑛 ∈ 𝐶 ( { 𝑛 } × ⦋ 𝑛 / 𝑘 ⦌ 𝐷 ) ∈ Fin ) → ∪ 𝑛 ∈ 𝐶 ( { 𝑛 } × ⦋ 𝑛 / 𝑘 ⦌ 𝐷 ) ∈ Fin )
87 2 85 86 syl2anc ⊢ ( 𝜑 → ∪ 𝑛 ∈ 𝐶 ( { 𝑛 } × ⦋ 𝑛 / 𝑘 ⦌ 𝐷 ) ∈ Fin )
88 reliun ⊢ ( Rel ∪ 𝑛 ∈ 𝐶 ( { 𝑛 } × ⦋ 𝑛 / 𝑘 ⦌ 𝐷 ) ↔ ∀ 𝑛 ∈ 𝐶 Rel ( { 𝑛 } × ⦋ 𝑛 / 𝑘 ⦌ 𝐷 ) )
89 relxp ⊢ Rel ( { 𝑛 } × ⦋ 𝑛 / 𝑘 ⦌ 𝐷 )
90 89 a1i ⊢ ( 𝑛 ∈ 𝐶 → Rel ( { 𝑛 } × ⦋ 𝑛 / 𝑘 ⦌ 𝐷 ) )
91 88 90 mprgbir ⊢ Rel ∪ 𝑛 ∈ 𝐶 ( { 𝑛 } × ⦋ 𝑛 / 𝑘 ⦌ 𝐷 )
92 91 a1i ⊢ ( 𝜑 → Rel ∪ 𝑛 ∈ 𝐶 ( { 𝑛 } × ⦋ 𝑛 / 𝑘 ⦌ 𝐷 ) )
93 csbeq1 ⊢ ( 𝑚 = ( 2nd ‘ 𝑤 ) → ⦋ 𝑚 / 𝑗 ⦌ 𝐸 = ⦋ ( 2nd ‘ 𝑤 ) / 𝑗 ⦌ 𝐸 )
94 93 csbeq2dv ⊢ ( 𝑚 = ( 2nd ‘ 𝑤 ) → ⦋ ( 1st ‘ 𝑤 ) / 𝑘 ⦌ ⦋ 𝑚 / 𝑗 ⦌ 𝐸 = ⦋ ( 1st ‘ 𝑤 ) / 𝑘 ⦌ ⦋ ( 2nd ‘ 𝑤 ) / 𝑗 ⦌ 𝐸 )
95 94 eleq1d ⊢ ( 𝑚 = ( 2nd ‘ 𝑤 ) → ( ⦋ ( 1st ‘ 𝑤 ) / 𝑘 ⦌ ⦋ 𝑚 / 𝑗 ⦌ 𝐸 ∈ ℂ ↔ ⦋ ( 1st ‘ 𝑤 ) / 𝑘 ⦌ ⦋ ( 2nd ‘ 𝑤 ) / 𝑗 ⦌ 𝐸 ∈ ℂ ) )
96 csbeq1 ⊢ ( 𝑛 = ( 1st ‘ 𝑤 ) → ⦋ 𝑛 / 𝑘 ⦌ 𝐷 = ⦋ ( 1st ‘ 𝑤 ) / 𝑘 ⦌ 𝐷 )
97 csbeq1 ⊢ ( 𝑛 = ( 1st ‘ 𝑤 ) → ⦋ 𝑛 / 𝑘 ⦌ ⦋ 𝑚 / 𝑗 ⦌ 𝐸 = ⦋ ( 1st ‘ 𝑤 ) / 𝑘 ⦌ ⦋ 𝑚 / 𝑗 ⦌ 𝐸 )
98 97 eleq1d ⊢ ( 𝑛 = ( 1st ‘ 𝑤 ) → ( ⦋ 𝑛 / 𝑘 ⦌ ⦋ 𝑚 / 𝑗 ⦌ 𝐸 ∈ ℂ ↔ ⦋ ( 1st ‘ 𝑤 ) / 𝑘 ⦌ ⦋ 𝑚 / 𝑗 ⦌ 𝐸 ∈ ℂ ) )
99 96 98 raleqbidv ⊢ ( 𝑛 = ( 1st ‘ 𝑤 ) → ( ∀ 𝑚 ∈ ⦋ 𝑛 / 𝑘 ⦌ 𝐷 ⦋ 𝑛 / 𝑘 ⦌ ⦋ 𝑚 / 𝑗 ⦌ 𝐸 ∈ ℂ ↔ ∀ 𝑚 ∈ ⦋ ( 1st ‘ 𝑤 ) / 𝑘 ⦌ 𝐷 ⦋ ( 1st ‘ 𝑤 ) / 𝑘 ⦌ ⦋ 𝑚 / 𝑗 ⦌ 𝐸 ∈ ℂ ) )
100 simpl ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ 𝐶 ∧ 𝑚 ∈ ⦋ 𝑛 / 𝑘 ⦌ 𝐷 ) ) → 𝜑 )
101 29 nfcri ⊢ Ⅎ 𝑗 𝑛 ∈ ⦋ 𝑚 / 𝑗 ⦌ 𝐵
102 74 equcomd ⊢ ( 𝑚 ∈ { 𝑗 } → 𝑗 = 𝑚 )
103 102 32 syl ⊢ ( 𝑚 ∈ { 𝑗 } → 𝐵 = ⦋ 𝑚 / 𝑗 ⦌ 𝐵 )
104 103 eleq2d ⊢ ( 𝑚 ∈ { 𝑗 } → ( 𝑛 ∈ 𝐵 ↔ 𝑛 ∈ ⦋ 𝑚 / 𝑗 ⦌ 𝐵 ) )
105 104 biimpa ⊢ ( ( 𝑚 ∈ { 𝑗 } ∧ 𝑛 ∈ 𝐵 ) → 𝑛 ∈ ⦋ 𝑚 / 𝑗 ⦌ 𝐵 )
106 71 105 sylbi ⊢ ( ⟨ 𝑚 , 𝑛 ⟩ ∈ ( { 𝑗 } × 𝐵 ) → 𝑛 ∈ ⦋ 𝑚 / 𝑗 ⦌ 𝐵 )
107 106 a1i ⊢ ( 𝑗 ∈ 𝐴 → ( ⟨ 𝑚 , 𝑛 ⟩ ∈ ( { 𝑗 } × 𝐵 ) → 𝑛 ∈ ⦋ 𝑚 / 𝑗 ⦌ 𝐵 ) )
108 101 107 rexlimi ⊢ ( ∃ 𝑗 ∈ 𝐴 ⟨ 𝑚 , 𝑛 ⟩ ∈ ( { 𝑗 } × 𝐵 ) → 𝑛 ∈ ⦋ 𝑚 / 𝑗 ⦌ 𝐵 )
109 69 108 syl ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ 𝐶 ∧ 𝑚 ∈ ⦋ 𝑛 / 𝑘 ⦌ 𝐷 ) ) → 𝑛 ∈ ⦋ 𝑚 / 𝑗 ⦌ 𝐵 )
110 5 ralrimivva ⊢ ( 𝜑 → ∀ 𝑗 ∈ 𝐴 ∀ 𝑘 ∈ 𝐵 𝐸 ∈ ℂ )
111 nfcsb1v ⊢ Ⅎ 𝑗 ⦋ 𝑚 / 𝑗 ⦌ 𝐸
112 111 nfel1 ⊢ Ⅎ 𝑗 ⦋ 𝑚 / 𝑗 ⦌ 𝐸 ∈ ℂ
113 29 112 nfralw ⊢ Ⅎ 𝑗 ∀ 𝑘 ∈ ⦋ 𝑚 / 𝑗 ⦌ 𝐵 ⦋ 𝑚 / 𝑗 ⦌ 𝐸 ∈ ℂ
114 csbeq1a ⊢ ( 𝑗 = 𝑚 → 𝐸 = ⦋ 𝑚 / 𝑗 ⦌ 𝐸 )
115 114 eleq1d ⊢ ( 𝑗 = 𝑚 → ( 𝐸 ∈ ℂ ↔ ⦋ 𝑚 / 𝑗 ⦌ 𝐸 ∈ ℂ ) )
116 32 115 raleqbidv ⊢ ( 𝑗 = 𝑚 → ( ∀ 𝑘 ∈ 𝐵 𝐸 ∈ ℂ ↔ ∀ 𝑘 ∈ ⦋ 𝑚 / 𝑗 ⦌ 𝐵 ⦋ 𝑚 / 𝑗 ⦌ 𝐸 ∈ ℂ ) )
117 113 116 rspc ⊢ ( 𝑚 ∈ 𝐴 → ( ∀ 𝑗 ∈ 𝐴 ∀ 𝑘 ∈ 𝐵 𝐸 ∈ ℂ → ∀ 𝑘 ∈ ⦋ 𝑚 / 𝑗 ⦌ 𝐵 ⦋ 𝑚 / 𝑗 ⦌ 𝐸 ∈ ℂ ) )
118 110 117 mpan9 ⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝐴 ) → ∀ 𝑘 ∈ ⦋ 𝑚 / 𝑗 ⦌ 𝐵 ⦋ 𝑚 / 𝑗 ⦌ 𝐸 ∈ ℂ )
119 nfcsb1v ⊢ Ⅎ 𝑘 ⦋ 𝑛 / 𝑘 ⦌ ⦋ 𝑚 / 𝑗 ⦌ 𝐸
120 119 nfel1 ⊢ Ⅎ 𝑘 ⦋ 𝑛 / 𝑘 ⦌ ⦋ 𝑚 / 𝑗 ⦌ 𝐸 ∈ ℂ
121 csbeq1a ⊢ ( 𝑘 = 𝑛 → ⦋ 𝑚 / 𝑗 ⦌ 𝐸 = ⦋ 𝑛 / 𝑘 ⦌ ⦋ 𝑚 / 𝑗 ⦌ 𝐸 )
122 121 eleq1d ⊢ ( 𝑘 = 𝑛 → ( ⦋ 𝑚 / 𝑗 ⦌ 𝐸 ∈ ℂ ↔ ⦋ 𝑛 / 𝑘 ⦌ ⦋ 𝑚 / 𝑗 ⦌ 𝐸 ∈ ℂ ) )
123 120 122 rspc ⊢ ( 𝑛 ∈ ⦋ 𝑚 / 𝑗 ⦌ 𝐵 → ( ∀ 𝑘 ∈ ⦋ 𝑚 / 𝑗 ⦌ 𝐵 ⦋ 𝑚 / 𝑗 ⦌ 𝐸 ∈ ℂ → ⦋ 𝑛 / 𝑘 ⦌ ⦋ 𝑚 / 𝑗 ⦌ 𝐸 ∈ ℂ ) )
124 118 123 syl5com ⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝐴 ) → ( 𝑛 ∈ ⦋ 𝑚 / 𝑗 ⦌ 𝐵 → ⦋ 𝑛 / 𝑘 ⦌ ⦋ 𝑚 / 𝑗 ⦌ 𝐸 ∈ ℂ ) )
125 124 impr ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ 𝐴 ∧ 𝑛 ∈ ⦋ 𝑚 / 𝑗 ⦌ 𝐵 ) ) → ⦋ 𝑛 / 𝑘 ⦌ ⦋ 𝑚 / 𝑗 ⦌ 𝐸 ∈ ℂ )
126 100 79 109 125 syl12anc ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ 𝐶 ∧ 𝑚 ∈ ⦋ 𝑛 / 𝑘 ⦌ 𝐷 ) ) → ⦋ 𝑛 / 𝑘 ⦌ ⦋ 𝑚 / 𝑗 ⦌ 𝐸 ∈ ℂ )
127 126 ralrimivva ⊢ ( 𝜑 → ∀ 𝑛 ∈ 𝐶 ∀ 𝑚 ∈ ⦋ 𝑛 / 𝑘 ⦌ 𝐷 ⦋ 𝑛 / 𝑘 ⦌ ⦋ 𝑚 / 𝑗 ⦌ 𝐸 ∈ ℂ )
128 127 adantr ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ∪ 𝑛 ∈ 𝐶 ( { 𝑛 } × ⦋ 𝑛 / 𝑘 ⦌ 𝐷 ) ) → ∀ 𝑛 ∈ 𝐶 ∀ 𝑚 ∈ ⦋ 𝑛 / 𝑘 ⦌ 𝐷 ⦋ 𝑛 / 𝑘 ⦌ ⦋ 𝑚 / 𝑗 ⦌ 𝐸 ∈ ℂ )
129 simpr ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ∪ 𝑛 ∈ 𝐶 ( { 𝑛 } × ⦋ 𝑛 / 𝑘 ⦌ 𝐷 ) ) → 𝑤 ∈ ∪ 𝑛 ∈ 𝐶 ( { 𝑛 } × ⦋ 𝑛 / 𝑘 ⦌ 𝐷 ) )
130 eliun ⊢ ( 𝑤 ∈ ∪ 𝑛 ∈ 𝐶 ( { 𝑛 } × ⦋ 𝑛 / 𝑘 ⦌ 𝐷 ) ↔ ∃ 𝑛 ∈ 𝐶 𝑤 ∈ ( { 𝑛 } × ⦋ 𝑛 / 𝑘 ⦌ 𝐷 ) )
131 129 130 sylib ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ∪ 𝑛 ∈ 𝐶 ( { 𝑛 } × ⦋ 𝑛 / 𝑘 ⦌ 𝐷 ) ) → ∃ 𝑛 ∈ 𝐶 𝑤 ∈ ( { 𝑛 } × ⦋ 𝑛 / 𝑘 ⦌ 𝐷 ) )
132 xp1st ⊢ ( 𝑤 ∈ ( { 𝑛 } × ⦋ 𝑛 / 𝑘 ⦌ 𝐷 ) → ( 1st ‘ 𝑤 ) ∈ { 𝑛 } )
133 132 adantl ⊢ ( ( 𝑛 ∈ 𝐶 ∧ 𝑤 ∈ ( { 𝑛 } × ⦋ 𝑛 / 𝑘 ⦌ 𝐷 ) ) → ( 1st ‘ 𝑤 ) ∈ { 𝑛 } )
134 elsni ⊢ ( ( 1st ‘ 𝑤 ) ∈ { 𝑛 } → ( 1st ‘ 𝑤 ) = 𝑛 )
135 133 134 syl ⊢ ( ( 𝑛 ∈ 𝐶 ∧ 𝑤 ∈ ( { 𝑛 } × ⦋ 𝑛 / 𝑘 ⦌ 𝐷 ) ) → ( 1st ‘ 𝑤 ) = 𝑛 )
136 simpl ⊢ ( ( 𝑛 ∈ 𝐶 ∧ 𝑤 ∈ ( { 𝑛 } × ⦋ 𝑛 / 𝑘 ⦌ 𝐷 ) ) → 𝑛 ∈ 𝐶 )
137 135 136 eqeltrd ⊢ ( ( 𝑛 ∈ 𝐶 ∧ 𝑤 ∈ ( { 𝑛 } × ⦋ 𝑛 / 𝑘 ⦌ 𝐷 ) ) → ( 1st ‘ 𝑤 ) ∈ 𝐶 )
138 137 rexlimiva ⊢ ( ∃ 𝑛 ∈ 𝐶 𝑤 ∈ ( { 𝑛 } × ⦋ 𝑛 / 𝑘 ⦌ 𝐷 ) → ( 1st ‘ 𝑤 ) ∈ 𝐶 )
139 131 138 syl ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ∪ 𝑛 ∈ 𝐶 ( { 𝑛 } × ⦋ 𝑛 / 𝑘 ⦌ 𝐷 ) ) → ( 1st ‘ 𝑤 ) ∈ 𝐶 )
140 99 128 139 rspcdva ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ∪ 𝑛 ∈ 𝐶 ( { 𝑛 } × ⦋ 𝑛 / 𝑘 ⦌ 𝐷 ) ) → ∀ 𝑚 ∈ ⦋ ( 1st ‘ 𝑤 ) / 𝑘 ⦌ 𝐷 ⦋ ( 1st ‘ 𝑤 ) / 𝑘 ⦌ ⦋ 𝑚 / 𝑗 ⦌ 𝐸 ∈ ℂ )
141 xp2nd ⊢ ( 𝑤 ∈ ( { 𝑛 } × ⦋ 𝑛 / 𝑘 ⦌ 𝐷 ) → ( 2nd ‘ 𝑤 ) ∈ ⦋ 𝑛 / 𝑘 ⦌ 𝐷 )
142 141 adantl ⊢ ( ( 𝑛 ∈ 𝐶 ∧ 𝑤 ∈ ( { 𝑛 } × ⦋ 𝑛 / 𝑘 ⦌ 𝐷 ) ) → ( 2nd ‘ 𝑤 ) ∈ ⦋ 𝑛 / 𝑘 ⦌ 𝐷 )
143 135 csbeq1d ⊢ ( ( 𝑛 ∈ 𝐶 ∧ 𝑤 ∈ ( { 𝑛 } × ⦋ 𝑛 / 𝑘 ⦌ 𝐷 ) ) → ⦋ ( 1st ‘ 𝑤 ) / 𝑘 ⦌ 𝐷 = ⦋ 𝑛 / 𝑘 ⦌ 𝐷 )
144 142 143 eleqtrrd ⊢ ( ( 𝑛 ∈ 𝐶 ∧ 𝑤 ∈ ( { 𝑛 } × ⦋ 𝑛 / 𝑘 ⦌ 𝐷 ) ) → ( 2nd ‘ 𝑤 ) ∈ ⦋ ( 1st ‘ 𝑤 ) / 𝑘 ⦌ 𝐷 )
145 144 rexlimiva ⊢ ( ∃ 𝑛 ∈ 𝐶 𝑤 ∈ ( { 𝑛 } × ⦋ 𝑛 / 𝑘 ⦌ 𝐷 ) → ( 2nd ‘ 𝑤 ) ∈ ⦋ ( 1st ‘ 𝑤 ) / 𝑘 ⦌ 𝐷 )
146 131 145 syl ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ∪ 𝑛 ∈ 𝐶 ( { 𝑛 } × ⦋ 𝑛 / 𝑘 ⦌ 𝐷 ) ) → ( 2nd ‘ 𝑤 ) ∈ ⦋ ( 1st ‘ 𝑤 ) / 𝑘 ⦌ 𝐷 )
147 95 140 146 rspcdva ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ∪ 𝑛 ∈ 𝐶 ( { 𝑛 } × ⦋ 𝑛 / 𝑘 ⦌ 𝐷 ) ) → ⦋ ( 1st ‘ 𝑤 ) / 𝑘 ⦌ ⦋ ( 2nd ‘ 𝑤 ) / 𝑗 ⦌ 𝐸 ∈ ℂ )
148 53 59 87 92 147 fsumcnv ⊢ ( 𝜑 → Σ 𝑤 ∈ ∪ 𝑛 ∈ 𝐶 ( { 𝑛 } × ⦋ 𝑛 / 𝑘 ⦌ 𝐷 ) ⦋ ( 1st ‘ 𝑤 ) / 𝑘 ⦌ ⦋ ( 2nd ‘ 𝑤 ) / 𝑗 ⦌ 𝐸 = Σ 𝑧 ∈ ◡ ∪ 𝑛 ∈ 𝐶 ( { 𝑛 } × ⦋ 𝑛 / 𝑘 ⦌ 𝐷 ) ⦋ ( 2nd ‘ 𝑧 ) / 𝑘 ⦌ ⦋ ( 1st ‘ 𝑧 ) / 𝑗 ⦌ 𝐸 )
149 45 148 eqtr4d ⊢ ( 𝜑 → Σ 𝑧 ∈ ∪ 𝑚 ∈ 𝐴 ( { 𝑚 } × ⦋ 𝑚 / 𝑗 ⦌ 𝐵 ) ⦋ ( 2nd ‘ 𝑧 ) / 𝑘 ⦌ ⦋ ( 1st ‘ 𝑧 ) / 𝑗 ⦌ 𝐸 = Σ 𝑤 ∈ ∪ 𝑛 ∈ 𝐶 ( { 𝑛 } × ⦋ 𝑛 / 𝑘 ⦌ 𝐷 ) ⦋ ( 1st ‘ 𝑤 ) / 𝑘 ⦌ ⦋ ( 2nd ‘ 𝑤 ) / 𝑗 ⦌ 𝐸 )
150 3 ralrimiva ⊢ ( 𝜑 → ∀ 𝑗 ∈ 𝐴 𝐵 ∈ Fin )
151 29 nfel1 ⊢ Ⅎ 𝑗 ⦋ 𝑚 / 𝑗 ⦌ 𝐵 ∈ Fin
152 32 eleq1d ⊢ ( 𝑗 = 𝑚 → ( 𝐵 ∈ Fin ↔ ⦋ 𝑚 / 𝑗 ⦌ 𝐵 ∈ Fin ) )
153 151 152 rspc ⊢ ( 𝑚 ∈ 𝐴 → ( ∀ 𝑗 ∈ 𝐴 𝐵 ∈ Fin → ⦋ 𝑚 / 𝑗 ⦌ 𝐵 ∈ Fin ) )
154 150 153 mpan9 ⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝐴 ) → ⦋ 𝑚 / 𝑗 ⦌ 𝐵 ∈ Fin )
155 59 1 154 125 fsum2d ⊢ ( 𝜑 → Σ 𝑚 ∈ 𝐴 Σ 𝑛 ∈ ⦋ 𝑚 / 𝑗 ⦌ 𝐵 ⦋ 𝑛 / 𝑘 ⦌ ⦋ 𝑚 / 𝑗 ⦌ 𝐸 = Σ 𝑧 ∈ ∪ 𝑚 ∈ 𝐴 ( { 𝑚 } × ⦋ 𝑚 / 𝑗 ⦌ 𝐵 ) ⦋ ( 2nd ‘ 𝑧 ) / 𝑘 ⦌ ⦋ ( 1st ‘ 𝑧 ) / 𝑗 ⦌ 𝐸 )
156 53 2 82 126 fsum2d ⊢ ( 𝜑 → Σ 𝑛 ∈ 𝐶 Σ 𝑚 ∈ ⦋ 𝑛 / 𝑘 ⦌ 𝐷 ⦋ 𝑛 / 𝑘 ⦌ ⦋ 𝑚 / 𝑗 ⦌ 𝐸 = Σ 𝑤 ∈ ∪ 𝑛 ∈ 𝐶 ( { 𝑛 } × ⦋ 𝑛 / 𝑘 ⦌ 𝐷 ) ⦋ ( 1st ‘ 𝑤 ) / 𝑘 ⦌ ⦋ ( 2nd ‘ 𝑤 ) / 𝑗 ⦌ 𝐸 )
157 149 155 156 3eqtr4d ⊢ ( 𝜑 → Σ 𝑚 ∈ 𝐴 Σ 𝑛 ∈ ⦋ 𝑚 / 𝑗 ⦌ 𝐵 ⦋ 𝑛 / 𝑘 ⦌ ⦋ 𝑚 / 𝑗 ⦌ 𝐸 = Σ 𝑛 ∈ 𝐶 Σ 𝑚 ∈ ⦋ 𝑛 / 𝑘 ⦌ 𝐷 ⦋ 𝑛 / 𝑘 ⦌ ⦋ 𝑚 / 𝑗 ⦌ 𝐸 )
158 nfcv ⊢ Ⅎ 𝑚 Σ 𝑘 ∈ 𝐵 𝐸
159 nfcv ⊢ Ⅎ 𝑗 𝑛
160 159 111 nfcsbw ⊢ Ⅎ 𝑗 ⦋ 𝑛 / 𝑘 ⦌ ⦋ 𝑚 / 𝑗 ⦌ 𝐸
161 29 160 nfsum ⊢ Ⅎ 𝑗 Σ 𝑛 ∈ ⦋ 𝑚 / 𝑗 ⦌ 𝐵 ⦋ 𝑛 / 𝑘 ⦌ ⦋ 𝑚 / 𝑗 ⦌ 𝐸
162 nfcv ⊢ Ⅎ 𝑛 𝐸
163 nfcsb1v ⊢ Ⅎ 𝑘 ⦋ 𝑛 / 𝑘 ⦌ 𝐸
164 csbeq1a ⊢ ( 𝑘 = 𝑛 → 𝐸 = ⦋ 𝑛 / 𝑘 ⦌ 𝐸 )
165 162 163 164 cbvsumi ⊢ Σ 𝑘 ∈ 𝐵 𝐸 = Σ 𝑛 ∈ 𝐵 ⦋ 𝑛 / 𝑘 ⦌ 𝐸
166 114 csbeq2dv ⊢ ( 𝑗 = 𝑚 → ⦋ 𝑛 / 𝑘 ⦌ 𝐸 = ⦋ 𝑛 / 𝑘 ⦌ ⦋ 𝑚 / 𝑗 ⦌ 𝐸 )
167 166 adantr ⊢ ( ( 𝑗 = 𝑚 ∧ 𝑛 ∈ 𝐵 ) → ⦋ 𝑛 / 𝑘 ⦌ 𝐸 = ⦋ 𝑛 / 𝑘 ⦌ ⦋ 𝑚 / 𝑗 ⦌ 𝐸 )
168 32 167 sumeq12dv ⊢ ( 𝑗 = 𝑚 → Σ 𝑛 ∈ 𝐵 ⦋ 𝑛 / 𝑘 ⦌ 𝐸 = Σ 𝑛 ∈ ⦋ 𝑚 / 𝑗 ⦌ 𝐵 ⦋ 𝑛 / 𝑘 ⦌ ⦋ 𝑚 / 𝑗 ⦌ 𝐸 )
169 165 168 eqtrid ⊢ ( 𝑗 = 𝑚 → Σ 𝑘 ∈ 𝐵 𝐸 = Σ 𝑛 ∈ ⦋ 𝑚 / 𝑗 ⦌ 𝐵 ⦋ 𝑛 / 𝑘 ⦌ ⦋ 𝑚 / 𝑗 ⦌ 𝐸 )
170 158 161 169 cbvsumi ⊢ Σ 𝑗 ∈ 𝐴 Σ 𝑘 ∈ 𝐵 𝐸 = Σ 𝑚 ∈ 𝐴 Σ 𝑛 ∈ ⦋ 𝑚 / 𝑗 ⦌ 𝐵 ⦋ 𝑛 / 𝑘 ⦌ ⦋ 𝑚 / 𝑗 ⦌ 𝐸
171 nfcv ⊢ Ⅎ 𝑛 Σ 𝑗 ∈ 𝐷 𝐸
172 37 119 nfsum ⊢ Ⅎ 𝑘 Σ 𝑚 ∈ ⦋ 𝑛 / 𝑘 ⦌ 𝐷 ⦋ 𝑛 / 𝑘 ⦌ ⦋ 𝑚 / 𝑗 ⦌ 𝐸
173 nfcv ⊢ Ⅎ 𝑚 𝐸
174 173 111 114 cbvsumi ⊢ Σ 𝑗 ∈ 𝐷 𝐸 = Σ 𝑚 ∈ 𝐷 ⦋ 𝑚 / 𝑗 ⦌ 𝐸
175 121 adantr ⊢ ( ( 𝑘 = 𝑛 ∧ 𝑚 ∈ 𝐷 ) → ⦋ 𝑚 / 𝑗 ⦌ 𝐸 = ⦋ 𝑛 / 𝑘 ⦌ ⦋ 𝑚 / 𝑗 ⦌ 𝐸 )
176 40 175 sumeq12dv ⊢ ( 𝑘 = 𝑛 → Σ 𝑚 ∈ 𝐷 ⦋ 𝑚 / 𝑗 ⦌ 𝐸 = Σ 𝑚 ∈ ⦋ 𝑛 / 𝑘 ⦌ 𝐷 ⦋ 𝑛 / 𝑘 ⦌ ⦋ 𝑚 / 𝑗 ⦌ 𝐸 )
177 174 176 eqtrid ⊢ ( 𝑘 = 𝑛 → Σ 𝑗 ∈ 𝐷 𝐸 = Σ 𝑚 ∈ ⦋ 𝑛 / 𝑘 ⦌ 𝐷 ⦋ 𝑛 / 𝑘 ⦌ ⦋ 𝑚 / 𝑗 ⦌ 𝐸 )
178 171 172 177 cbvsumi ⊢ Σ 𝑘 ∈ 𝐶 Σ 𝑗 ∈ 𝐷 𝐸 = Σ 𝑛 ∈ 𝐶 Σ 𝑚 ∈ ⦋ 𝑛 / 𝑘 ⦌ 𝐷 ⦋ 𝑛 / 𝑘 ⦌ ⦋ 𝑚 / 𝑗 ⦌ 𝐸
179 157 170 178 3eqtr4g ⊢ ( 𝜑 → Σ 𝑗 ∈ 𝐴 Σ 𝑘 ∈ 𝐵 𝐸 = Σ 𝑘 ∈ 𝐶 Σ 𝑗 ∈ 𝐷 𝐸 )