Metamath Proof Explorer

Theorem fsum2dlem

Description: Lemma for fsum2d - induction step. (Contributed by Mario Carneiro, 23-Apr-2014)

Ref Expression
Hypotheses fsum2d.1 ⊢ ( 𝑧 = ⟨ 𝑗 , 𝑘 ⟩ → 𝐷 = 𝐶 )
fsum2d.2 ⊢ ( 𝜑 → 𝐴 ∈ Fin )
fsum2d.3 ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) → 𝐵 ∈ Fin )
fsum2d.4 ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ) ) → 𝐶 ∈ ℂ )
fsum2d.5 ⊢ ( 𝜑 → ¬ 𝑦 ∈ 𝑥 )
fsum2d.6 ⊢ ( 𝜑 → ( 𝑥 ∪ { 𝑦 } ) ⊆ 𝐴 )
fsum2d.7 ⊢ ( 𝜓 ↔ Σ 𝑗 ∈ 𝑥 Σ 𝑘 ∈ 𝐵 𝐶 = Σ 𝑧 ∈ ∪ 𝑗 ∈ 𝑥 ( { 𝑗 } × 𝐵 ) 𝐷 )
Assertion fsum2dlem ( ( 𝜑 ∧ 𝜓 ) → Σ 𝑗 ∈ ( 𝑥 ∪ { 𝑦 } ) Σ 𝑘 ∈ 𝐵 𝐶 = Σ 𝑧 ∈ ∪ 𝑗 ∈ ( 𝑥 ∪ { 𝑦 } ) ( { 𝑗 } × 𝐵 ) 𝐷 )

Proof

Step Hyp Ref Expression
1 fsum2d.1 ⊢ ( 𝑧 = ⟨ 𝑗 , 𝑘 ⟩ → 𝐷 = 𝐶 )
2 fsum2d.2 ⊢ ( 𝜑 → 𝐴 ∈ Fin )
3 fsum2d.3 ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) → 𝐵 ∈ Fin )
4 fsum2d.4 ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ) ) → 𝐶 ∈ ℂ )
5 fsum2d.5 ⊢ ( 𝜑 → ¬ 𝑦 ∈ 𝑥 )
6 fsum2d.6 ⊢ ( 𝜑 → ( 𝑥 ∪ { 𝑦 } ) ⊆ 𝐴 )
7 fsum2d.7 ⊢ ( 𝜓 ↔ Σ 𝑗 ∈ 𝑥 Σ 𝑘 ∈ 𝐵 𝐶 = Σ 𝑧 ∈ ∪ 𝑗 ∈ 𝑥 ( { 𝑗 } × 𝐵 ) 𝐷 )
8 7 bilani ⊢ ( ( 𝜑 ∧ 𝜓 ) → Σ 𝑗 ∈ 𝑥 Σ 𝑘 ∈ 𝐵 𝐶 = Σ 𝑧 ∈ ∪ 𝑗 ∈ 𝑥 ( { 𝑗 } × 𝐵 ) 𝐷 )
9 csbeq1a ⊢ ( 𝑗 = 𝑚 → 𝐵 = ⦋ 𝑚 / 𝑗 ⦌ 𝐵 )
10 csbeq1a ⊢ ( 𝑗 = 𝑚 → 𝐶 = ⦋ 𝑚 / 𝑗 ⦌ 𝐶 )
11 10 adantr ⊢ ( ( 𝑗 = 𝑚 ∧ 𝑘 ∈ 𝐵 ) → 𝐶 = ⦋ 𝑚 / 𝑗 ⦌ 𝐶 )
12 9 11 sumeq12dv ⊢ ( 𝑗 = 𝑚 → Σ 𝑘 ∈ 𝐵 𝐶 = Σ 𝑘 ∈ ⦋ 𝑚 / 𝑗 ⦌ 𝐵 ⦋ 𝑚 / 𝑗 ⦌ 𝐶 )
13 nfcv ⊢ Ⅎ 𝑚 Σ 𝑘 ∈ 𝐵 𝐶
14 nfcsb1v ⊢ Ⅎ 𝑗 ⦋ 𝑚 / 𝑗 ⦌ 𝐵
15 nfcsb1v ⊢ Ⅎ 𝑗 ⦋ 𝑚 / 𝑗 ⦌ 𝐶
16 14 15 nfsum ⊢ Ⅎ 𝑗 Σ 𝑘 ∈ ⦋ 𝑚 / 𝑗 ⦌ 𝐵 ⦋ 𝑚 / 𝑗 ⦌ 𝐶
17 12 13 16 cbvsum ⊢ Σ 𝑗 ∈ { 𝑦 } Σ 𝑘 ∈ 𝐵 𝐶 = Σ 𝑚 ∈ { 𝑦 } Σ 𝑘 ∈ ⦋ 𝑚 / 𝑗 ⦌ 𝐵 ⦋ 𝑚 / 𝑗 ⦌ 𝐶
18 6 unssbd ⊢ ( 𝜑 → { 𝑦 } ⊆ 𝐴 )
19 vex ⊢ 𝑦 ∈ V
20 19 snss ⊢ ( 𝑦 ∈ 𝐴 ↔ { 𝑦 } ⊆ 𝐴 )
21 18 20 sylibr ⊢ ( 𝜑 → 𝑦 ∈ 𝐴 )
22 3 ralrimiva ⊢ ( 𝜑 → ∀ 𝑗 ∈ 𝐴 𝐵 ∈ Fin )
23 nfcsb1v ⊢ Ⅎ 𝑗 ⦋ 𝑦 / 𝑗 ⦌ 𝐵
24 23 nfel1 ⊢ Ⅎ 𝑗 ⦋ 𝑦 / 𝑗 ⦌ 𝐵 ∈ Fin
25 csbeq1a ⊢ ( 𝑗 = 𝑦 → 𝐵 = ⦋ 𝑦 / 𝑗 ⦌ 𝐵 )
26 25 eleq1d ⊢ ( 𝑗 = 𝑦 → ( 𝐵 ∈ Fin ↔ ⦋ 𝑦 / 𝑗 ⦌ 𝐵 ∈ Fin ) )
27 24 26 rspc ⊢ ( 𝑦 ∈ 𝐴 → ( ∀ 𝑗 ∈ 𝐴 𝐵 ∈ Fin → ⦋ 𝑦 / 𝑗 ⦌ 𝐵 ∈ Fin ) )
28 21 22 27 sylc ⊢ ( 𝜑 → ⦋ 𝑦 / 𝑗 ⦌ 𝐵 ∈ Fin )
29 4 ralrimivva ⊢ ( 𝜑 → ∀ 𝑗 ∈ 𝐴 ∀ 𝑘 ∈ 𝐵 𝐶 ∈ ℂ )
30 nfcsb1v ⊢ Ⅎ 𝑗 ⦋ 𝑦 / 𝑗 ⦌ 𝐶
31 30 nfel1 ⊢ Ⅎ 𝑗 ⦋ 𝑦 / 𝑗 ⦌ 𝐶 ∈ ℂ
32 23 31 nfralw ⊢ Ⅎ 𝑗 ∀ 𝑘 ∈ ⦋ 𝑦 / 𝑗 ⦌ 𝐵 ⦋ 𝑦 / 𝑗 ⦌ 𝐶 ∈ ℂ
33 csbeq1a ⊢ ( 𝑗 = 𝑦 → 𝐶 = ⦋ 𝑦 / 𝑗 ⦌ 𝐶 )
34 33 eleq1d ⊢ ( 𝑗 = 𝑦 → ( 𝐶 ∈ ℂ ↔ ⦋ 𝑦 / 𝑗 ⦌ 𝐶 ∈ ℂ ) )
35 25 34 raleqbidv ⊢ ( 𝑗 = 𝑦 → ( ∀ 𝑘 ∈ 𝐵 𝐶 ∈ ℂ ↔ ∀ 𝑘 ∈ ⦋ 𝑦 / 𝑗 ⦌ 𝐵 ⦋ 𝑦 / 𝑗 ⦌ 𝐶 ∈ ℂ ) )
36 32 35 rspc ⊢ ( 𝑦 ∈ 𝐴 → ( ∀ 𝑗 ∈ 𝐴 ∀ 𝑘 ∈ 𝐵 𝐶 ∈ ℂ → ∀ 𝑘 ∈ ⦋ 𝑦 / 𝑗 ⦌ 𝐵 ⦋ 𝑦 / 𝑗 ⦌ 𝐶 ∈ ℂ ) )
37 21 29 36 sylc ⊢ ( 𝜑 → ∀ 𝑘 ∈ ⦋ 𝑦 / 𝑗 ⦌ 𝐵 ⦋ 𝑦 / 𝑗 ⦌ 𝐶 ∈ ℂ )
38 37 r19.21bi ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ⦋ 𝑦 / 𝑗 ⦌ 𝐵 ) → ⦋ 𝑦 / 𝑗 ⦌ 𝐶 ∈ ℂ )
39 28 38 fsumcl ⊢ ( 𝜑 → Σ 𝑘 ∈ ⦋ 𝑦 / 𝑗 ⦌ 𝐵 ⦋ 𝑦 / 𝑗 ⦌ 𝐶 ∈ ℂ )
40 csbeq1 ⊢ ( 𝑚 = 𝑦 → ⦋ 𝑚 / 𝑗 ⦌ 𝐵 = ⦋ 𝑦 / 𝑗 ⦌ 𝐵 )
41 csbeq1 ⊢ ( 𝑚 = 𝑦 → ⦋ 𝑚 / 𝑗 ⦌ 𝐶 = ⦋ 𝑦 / 𝑗 ⦌ 𝐶 )
42 41 adantr ⊢ ( ( 𝑚 = 𝑦 ∧ 𝑘 ∈ ⦋ 𝑚 / 𝑗 ⦌ 𝐵 ) → ⦋ 𝑚 / 𝑗 ⦌ 𝐶 = ⦋ 𝑦 / 𝑗 ⦌ 𝐶 )
43 40 42 sumeq12dv ⊢ ( 𝑚 = 𝑦 → Σ 𝑘 ∈ ⦋ 𝑚 / 𝑗 ⦌ 𝐵 ⦋ 𝑚 / 𝑗 ⦌ 𝐶 = Σ 𝑘 ∈ ⦋ 𝑦 / 𝑗 ⦌ 𝐵 ⦋ 𝑦 / 𝑗 ⦌ 𝐶 )
44 43 sumsn ⊢ ( ( 𝑦 ∈ 𝐴 ∧ Σ 𝑘 ∈ ⦋ 𝑦 / 𝑗 ⦌ 𝐵 ⦋ 𝑦 / 𝑗 ⦌ 𝐶 ∈ ℂ ) → Σ 𝑚 ∈ { 𝑦 } Σ 𝑘 ∈ ⦋ 𝑚 / 𝑗 ⦌ 𝐵 ⦋ 𝑚 / 𝑗 ⦌ 𝐶 = Σ 𝑘 ∈ ⦋ 𝑦 / 𝑗 ⦌ 𝐵 ⦋ 𝑦 / 𝑗 ⦌ 𝐶 )
45 21 39 44 syl2anc ⊢ ( 𝜑 → Σ 𝑚 ∈ { 𝑦 } Σ 𝑘 ∈ ⦋ 𝑚 / 𝑗 ⦌ 𝐵 ⦋ 𝑚 / 𝑗 ⦌ 𝐶 = Σ 𝑘 ∈ ⦋ 𝑦 / 𝑗 ⦌ 𝐵 ⦋ 𝑦 / 𝑗 ⦌ 𝐶 )
46 csbeq1a ⊢ ( 𝑘 = 𝑚 → ⦋ 𝑦 / 𝑗 ⦌ 𝐶 = ⦋ 𝑚 / 𝑘 ⦌ ⦋ 𝑦 / 𝑗 ⦌ 𝐶 )
47 nfcv ⊢ Ⅎ 𝑚 ⦋ 𝑦 / 𝑗 ⦌ 𝐶
48 nfcsb1v ⊢ Ⅎ 𝑘 ⦋ 𝑚 / 𝑘 ⦌ ⦋ 𝑦 / 𝑗 ⦌ 𝐶
49 46 47 48 cbvsum ⊢ Σ 𝑘 ∈ ⦋ 𝑦 / 𝑗 ⦌ 𝐵 ⦋ 𝑦 / 𝑗 ⦌ 𝐶 = Σ 𝑚 ∈ ⦋ 𝑦 / 𝑗 ⦌ 𝐵 ⦋ 𝑚 / 𝑘 ⦌ ⦋ 𝑦 / 𝑗 ⦌ 𝐶
50 csbeq1 ⊢ ( 𝑚 = ( 2nd ‘ 𝑧 ) → ⦋ 𝑚 / 𝑘 ⦌ ⦋ 𝑦 / 𝑗 ⦌ 𝐶 = ⦋ ( 2nd ‘ 𝑧 ) / 𝑘 ⦌ ⦋ 𝑦 / 𝑗 ⦌ 𝐶 )
51 snfi ⊢ { 𝑦 } ∈ Fin
52 xpfi ⊢ ( ( { 𝑦 } ∈ Fin ∧ ⦋ 𝑦 / 𝑗 ⦌ 𝐵 ∈ Fin ) → ( { 𝑦 } × ⦋ 𝑦 / 𝑗 ⦌ 𝐵 ) ∈ Fin )
53 51 28 52 sylancr ⊢ ( 𝜑 → ( { 𝑦 } × ⦋ 𝑦 / 𝑗 ⦌ 𝐵 ) ∈ Fin )
54 2ndconst ⊢ ( 𝑦 ∈ 𝐴 → ( 2nd ↾ ( { 𝑦 } × ⦋ 𝑦 / 𝑗 ⦌ 𝐵 ) ) : ( { 𝑦 } × ⦋ 𝑦 / 𝑗 ⦌ 𝐵 ) –1-1-onto→ ⦋ 𝑦 / 𝑗 ⦌ 𝐵 )
55 21 54 syl ⊢ ( 𝜑 → ( 2nd ↾ ( { 𝑦 } × ⦋ 𝑦 / 𝑗 ⦌ 𝐵 ) ) : ( { 𝑦 } × ⦋ 𝑦 / 𝑗 ⦌ 𝐵 ) –1-1-onto→ ⦋ 𝑦 / 𝑗 ⦌ 𝐵 )
56 fvres ⊢ ( 𝑧 ∈ ( { 𝑦 } × ⦋ 𝑦 / 𝑗 ⦌ 𝐵 ) → ( ( 2nd ↾ ( { 𝑦 } × ⦋ 𝑦 / 𝑗 ⦌ 𝐵 ) ) ‘ 𝑧 ) = ( 2nd ‘ 𝑧 ) )
57 56 adantl ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( { 𝑦 } × ⦋ 𝑦 / 𝑗 ⦌ 𝐵 ) ) → ( ( 2nd ↾ ( { 𝑦 } × ⦋ 𝑦 / 𝑗 ⦌ 𝐵 ) ) ‘ 𝑧 ) = ( 2nd ‘ 𝑧 ) )
58 48 nfel1 ⊢ Ⅎ 𝑘 ⦋ 𝑚 / 𝑘 ⦌ ⦋ 𝑦 / 𝑗 ⦌ 𝐶 ∈ ℂ
59 46 eleq1d ⊢ ( 𝑘 = 𝑚 → ( ⦋ 𝑦 / 𝑗 ⦌ 𝐶 ∈ ℂ ↔ ⦋ 𝑚 / 𝑘 ⦌ ⦋ 𝑦 / 𝑗 ⦌ 𝐶 ∈ ℂ ) )
60 58 59 rspc ⊢ ( 𝑚 ∈ ⦋ 𝑦 / 𝑗 ⦌ 𝐵 → ( ∀ 𝑘 ∈ ⦋ 𝑦 / 𝑗 ⦌ 𝐵 ⦋ 𝑦 / 𝑗 ⦌ 𝐶 ∈ ℂ → ⦋ 𝑚 / 𝑘 ⦌ ⦋ 𝑦 / 𝑗 ⦌ 𝐶 ∈ ℂ ) )
61 37 60 mpan9 ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ⦋ 𝑦 / 𝑗 ⦌ 𝐵 ) → ⦋ 𝑚 / 𝑘 ⦌ ⦋ 𝑦 / 𝑗 ⦌ 𝐶 ∈ ℂ )
62 50 53 55 57 61 fsumf1o ⊢ ( 𝜑 → Σ 𝑚 ∈ ⦋ 𝑦 / 𝑗 ⦌ 𝐵 ⦋ 𝑚 / 𝑘 ⦌ ⦋ 𝑦 / 𝑗 ⦌ 𝐶 = Σ 𝑧 ∈ ( { 𝑦 } × ⦋ 𝑦 / 𝑗 ⦌ 𝐵 ) ⦋ ( 2nd ‘ 𝑧 ) / 𝑘 ⦌ ⦋ 𝑦 / 𝑗 ⦌ 𝐶 )
63 elxp ⊢ ( 𝑧 ∈ ( { 𝑦 } × ⦋ 𝑦 / 𝑗 ⦌ 𝐵 ) ↔ ∃ 𝑚 ∃ 𝑘 ( 𝑧 = ⟨ 𝑚 , 𝑘 ⟩ ∧ ( 𝑚 ∈ { 𝑦 } ∧ 𝑘 ∈ ⦋ 𝑦 / 𝑗 ⦌ 𝐵 ) ) )
64 nfv ⊢ Ⅎ 𝑗 𝑧 = ⟨ 𝑚 , 𝑘 ⟩
65 nfv ⊢ Ⅎ 𝑗 𝑚 ∈ { 𝑦 }
66 23 nfcri ⊢ Ⅎ 𝑗 𝑘 ∈ ⦋ 𝑦 / 𝑗 ⦌ 𝐵
67 65 66 nfan ⊢ Ⅎ 𝑗 ( 𝑚 ∈ { 𝑦 } ∧ 𝑘 ∈ ⦋ 𝑦 / 𝑗 ⦌ 𝐵 )
68 64 67 nfan ⊢ Ⅎ 𝑗 ( 𝑧 = ⟨ 𝑚 , 𝑘 ⟩ ∧ ( 𝑚 ∈ { 𝑦 } ∧ 𝑘 ∈ ⦋ 𝑦 / 𝑗 ⦌ 𝐵 ) )
69 68 nfex ⊢ Ⅎ 𝑗 ∃ 𝑘 ( 𝑧 = ⟨ 𝑚 , 𝑘 ⟩ ∧ ( 𝑚 ∈ { 𝑦 } ∧ 𝑘 ∈ ⦋ 𝑦 / 𝑗 ⦌ 𝐵 ) )
70 nfv ⊢ Ⅎ 𝑚 ∃ 𝑘 ( 𝑧 = ⟨ 𝑗 , 𝑘 ⟩ ∧ ( 𝑗 = 𝑦 ∧ 𝑘 ∈ 𝐵 ) )
71 opeq1 ⊢ ( 𝑚 = 𝑗 → ⟨ 𝑚 , 𝑘 ⟩ = ⟨ 𝑗 , 𝑘 ⟩ )
72 71 eqeq2d ⊢ ( 𝑚 = 𝑗 → ( 𝑧 = ⟨ 𝑚 , 𝑘 ⟩ ↔ 𝑧 = ⟨ 𝑗 , 𝑘 ⟩ ) )
73 velsn ⊢ ( 𝑚 ∈ { 𝑦 } ↔ 𝑚 = 𝑦 )
74 73 anbi1i ⊢ ( ( 𝑚 ∈ { 𝑦 } ∧ 𝑘 ∈ ⦋ 𝑦 / 𝑗 ⦌ 𝐵 ) ↔ ( 𝑚 = 𝑦 ∧ 𝑘 ∈ ⦋ 𝑦 / 𝑗 ⦌ 𝐵 ) )
75 eqtr2 ⊢ ( ( 𝑚 = 𝑗 ∧ 𝑚 = 𝑦 ) → 𝑗 = 𝑦 )
76 75 25 syl ⊢ ( ( 𝑚 = 𝑗 ∧ 𝑚 = 𝑦 ) → 𝐵 = ⦋ 𝑦 / 𝑗 ⦌ 𝐵 )
77 76 eleq2d ⊢ ( ( 𝑚 = 𝑗 ∧ 𝑚 = 𝑦 ) → ( 𝑘 ∈ 𝐵 ↔ 𝑘 ∈ ⦋ 𝑦 / 𝑗 ⦌ 𝐵 ) )
78 77 pm5.32da ⊢ ( 𝑚 = 𝑗 → ( ( 𝑚 = 𝑦 ∧ 𝑘 ∈ 𝐵 ) ↔ ( 𝑚 = 𝑦 ∧ 𝑘 ∈ ⦋ 𝑦 / 𝑗 ⦌ 𝐵 ) ) )
79 74 78 bitr4id ⊢ ( 𝑚 = 𝑗 → ( ( 𝑚 ∈ { 𝑦 } ∧ 𝑘 ∈ ⦋ 𝑦 / 𝑗 ⦌ 𝐵 ) ↔ ( 𝑚 = 𝑦 ∧ 𝑘 ∈ 𝐵 ) ) )
80 equequ1 ⊢ ( 𝑚 = 𝑗 → ( 𝑚 = 𝑦 ↔ 𝑗 = 𝑦 ) )
81 80 anbi1d ⊢ ( 𝑚 = 𝑗 → ( ( 𝑚 = 𝑦 ∧ 𝑘 ∈ 𝐵 ) ↔ ( 𝑗 = 𝑦 ∧ 𝑘 ∈ 𝐵 ) ) )
82 79 81 bitrd ⊢ ( 𝑚 = 𝑗 → ( ( 𝑚 ∈ { 𝑦 } ∧ 𝑘 ∈ ⦋ 𝑦 / 𝑗 ⦌ 𝐵 ) ↔ ( 𝑗 = 𝑦 ∧ 𝑘 ∈ 𝐵 ) ) )
83 72 82 anbi12d ⊢ ( 𝑚 = 𝑗 → ( ( 𝑧 = ⟨ 𝑚 , 𝑘 ⟩ ∧ ( 𝑚 ∈ { 𝑦 } ∧ 𝑘 ∈ ⦋ 𝑦 / 𝑗 ⦌ 𝐵 ) ) ↔ ( 𝑧 = ⟨ 𝑗 , 𝑘 ⟩ ∧ ( 𝑗 = 𝑦 ∧ 𝑘 ∈ 𝐵 ) ) ) )
84 83 exbidv ⊢ ( 𝑚 = 𝑗 → ( ∃ 𝑘 ( 𝑧 = ⟨ 𝑚 , 𝑘 ⟩ ∧ ( 𝑚 ∈ { 𝑦 } ∧ 𝑘 ∈ ⦋ 𝑦 / 𝑗 ⦌ 𝐵 ) ) ↔ ∃ 𝑘 ( 𝑧 = ⟨ 𝑗 , 𝑘 ⟩ ∧ ( 𝑗 = 𝑦 ∧ 𝑘 ∈ 𝐵 ) ) ) )
85 69 70 84 cbvexv1 ⊢ ( ∃ 𝑚 ∃ 𝑘 ( 𝑧 = ⟨ 𝑚 , 𝑘 ⟩ ∧ ( 𝑚 ∈ { 𝑦 } ∧ 𝑘 ∈ ⦋ 𝑦 / 𝑗 ⦌ 𝐵 ) ) ↔ ∃ 𝑗 ∃ 𝑘 ( 𝑧 = ⟨ 𝑗 , 𝑘 ⟩ ∧ ( 𝑗 = 𝑦 ∧ 𝑘 ∈ 𝐵 ) ) )
86 63 85 bitri ⊢ ( 𝑧 ∈ ( { 𝑦 } × ⦋ 𝑦 / 𝑗 ⦌ 𝐵 ) ↔ ∃ 𝑗 ∃ 𝑘 ( 𝑧 = ⟨ 𝑗 , 𝑘 ⟩ ∧ ( 𝑗 = 𝑦 ∧ 𝑘 ∈ 𝐵 ) ) )
87 nfv ⊢ Ⅎ 𝑗 𝜑
88 nfcv ⊢ Ⅎ 𝑗 ( 2nd ‘ 𝑧 )
89 88 30 nfcsbw ⊢ Ⅎ 𝑗 ⦋ ( 2nd ‘ 𝑧 ) / 𝑘 ⦌ ⦋ 𝑦 / 𝑗 ⦌ 𝐶
90 89 nfeq2 ⊢ Ⅎ 𝑗 𝐷 = ⦋ ( 2nd ‘ 𝑧 ) / 𝑘 ⦌ ⦋ 𝑦 / 𝑗 ⦌ 𝐶
91 nfv ⊢ Ⅎ 𝑘 𝜑
92 nfcsb1v ⊢ Ⅎ 𝑘 ⦋ ( 2nd ‘ 𝑧 ) / 𝑘 ⦌ ⦋ 𝑦 / 𝑗 ⦌ 𝐶
93 92 nfeq2 ⊢ Ⅎ 𝑘 𝐷 = ⦋ ( 2nd ‘ 𝑧 ) / 𝑘 ⦌ ⦋ 𝑦 / 𝑗 ⦌ 𝐶
94 1 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑧 = ⟨ 𝑗 , 𝑘 ⟩ ) ∧ ( 𝑗 = 𝑦 ∧ 𝑘 ∈ 𝐵 ) ) → 𝐷 = 𝐶 )
95 33 ad2antrl ⊢ ( ( ( 𝜑 ∧ 𝑧 = ⟨ 𝑗 , 𝑘 ⟩ ) ∧ ( 𝑗 = 𝑦 ∧ 𝑘 ∈ 𝐵 ) ) → 𝐶 = ⦋ 𝑦 / 𝑗 ⦌ 𝐶 )
96 fveq2 ⊢ ( 𝑧 = ⟨ 𝑗 , 𝑘 ⟩ → ( 2nd ‘ 𝑧 ) = ( 2nd ‘ ⟨ 𝑗 , 𝑘 ⟩ ) )
97 vex ⊢ 𝑗 ∈ V
98 vex ⊢ 𝑘 ∈ V
99 97 98 op2nd ⊢ ( 2nd ‘ ⟨ 𝑗 , 𝑘 ⟩ ) = 𝑘
100 96 99 eqtr2di ⊢ ( 𝑧 = ⟨ 𝑗 , 𝑘 ⟩ → 𝑘 = ( 2nd ‘ 𝑧 ) )
101 100 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑧 = ⟨ 𝑗 , 𝑘 ⟩ ) ∧ ( 𝑗 = 𝑦 ∧ 𝑘 ∈ 𝐵 ) ) → 𝑘 = ( 2nd ‘ 𝑧 ) )
102 csbeq1a ⊢ ( 𝑘 = ( 2nd ‘ 𝑧 ) → ⦋ 𝑦 / 𝑗 ⦌ 𝐶 = ⦋ ( 2nd ‘ 𝑧 ) / 𝑘 ⦌ ⦋ 𝑦 / 𝑗 ⦌ 𝐶 )
103 101 102 syl ⊢ ( ( ( 𝜑 ∧ 𝑧 = ⟨ 𝑗 , 𝑘 ⟩ ) ∧ ( 𝑗 = 𝑦 ∧ 𝑘 ∈ 𝐵 ) ) → ⦋ 𝑦 / 𝑗 ⦌ 𝐶 = ⦋ ( 2nd ‘ 𝑧 ) / 𝑘 ⦌ ⦋ 𝑦 / 𝑗 ⦌ 𝐶 )
104 94 95 103 3eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑧 = ⟨ 𝑗 , 𝑘 ⟩ ) ∧ ( 𝑗 = 𝑦 ∧ 𝑘 ∈ 𝐵 ) ) → 𝐷 = ⦋ ( 2nd ‘ 𝑧 ) / 𝑘 ⦌ ⦋ 𝑦 / 𝑗 ⦌ 𝐶 )
105 104 expl ⊢ ( 𝜑 → ( ( 𝑧 = ⟨ 𝑗 , 𝑘 ⟩ ∧ ( 𝑗 = 𝑦 ∧ 𝑘 ∈ 𝐵 ) ) → 𝐷 = ⦋ ( 2nd ‘ 𝑧 ) / 𝑘 ⦌ ⦋ 𝑦 / 𝑗 ⦌ 𝐶 ) )
106 91 93 105 exlimd ⊢ ( 𝜑 → ( ∃ 𝑘 ( 𝑧 = ⟨ 𝑗 , 𝑘 ⟩ ∧ ( 𝑗 = 𝑦 ∧ 𝑘 ∈ 𝐵 ) ) → 𝐷 = ⦋ ( 2nd ‘ 𝑧 ) / 𝑘 ⦌ ⦋ 𝑦 / 𝑗 ⦌ 𝐶 ) )
107 87 90 106 exlimd ⊢ ( 𝜑 → ( ∃ 𝑗 ∃ 𝑘 ( 𝑧 = ⟨ 𝑗 , 𝑘 ⟩ ∧ ( 𝑗 = 𝑦 ∧ 𝑘 ∈ 𝐵 ) ) → 𝐷 = ⦋ ( 2nd ‘ 𝑧 ) / 𝑘 ⦌ ⦋ 𝑦 / 𝑗 ⦌ 𝐶 ) )
108 86 107 biimtrid ⊢ ( 𝜑 → ( 𝑧 ∈ ( { 𝑦 } × ⦋ 𝑦 / 𝑗 ⦌ 𝐵 ) → 𝐷 = ⦋ ( 2nd ‘ 𝑧 ) / 𝑘 ⦌ ⦋ 𝑦 / 𝑗 ⦌ 𝐶 ) )
109 108 imp ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( { 𝑦 } × ⦋ 𝑦 / 𝑗 ⦌ 𝐵 ) ) → 𝐷 = ⦋ ( 2nd ‘ 𝑧 ) / 𝑘 ⦌ ⦋ 𝑦 / 𝑗 ⦌ 𝐶 )
110 109 sumeq2dv ⊢ ( 𝜑 → Σ 𝑧 ∈ ( { 𝑦 } × ⦋ 𝑦 / 𝑗 ⦌ 𝐵 ) 𝐷 = Σ 𝑧 ∈ ( { 𝑦 } × ⦋ 𝑦 / 𝑗 ⦌ 𝐵 ) ⦋ ( 2nd ‘ 𝑧 ) / 𝑘 ⦌ ⦋ 𝑦 / 𝑗 ⦌ 𝐶 )
111 62 110 eqtr4d ⊢ ( 𝜑 → Σ 𝑚 ∈ ⦋ 𝑦 / 𝑗 ⦌ 𝐵 ⦋ 𝑚 / 𝑘 ⦌ ⦋ 𝑦 / 𝑗 ⦌ 𝐶 = Σ 𝑧 ∈ ( { 𝑦 } × ⦋ 𝑦 / 𝑗 ⦌ 𝐵 ) 𝐷 )
112 49 111 eqtrid ⊢ ( 𝜑 → Σ 𝑘 ∈ ⦋ 𝑦 / 𝑗 ⦌ 𝐵 ⦋ 𝑦 / 𝑗 ⦌ 𝐶 = Σ 𝑧 ∈ ( { 𝑦 } × ⦋ 𝑦 / 𝑗 ⦌ 𝐵 ) 𝐷 )
113 45 112 eqtrd ⊢ ( 𝜑 → Σ 𝑚 ∈ { 𝑦 } Σ 𝑘 ∈ ⦋ 𝑚 / 𝑗 ⦌ 𝐵 ⦋ 𝑚 / 𝑗 ⦌ 𝐶 = Σ 𝑧 ∈ ( { 𝑦 } × ⦋ 𝑦 / 𝑗 ⦌ 𝐵 ) 𝐷 )
114 17 113 eqtrid ⊢ ( 𝜑 → Σ 𝑗 ∈ { 𝑦 } Σ 𝑘 ∈ 𝐵 𝐶 = Σ 𝑧 ∈ ( { 𝑦 } × ⦋ 𝑦 / 𝑗 ⦌ 𝐵 ) 𝐷 )
115 114 adantr ⊢ ( ( 𝜑 ∧ 𝜓 ) → Σ 𝑗 ∈ { 𝑦 } Σ 𝑘 ∈ 𝐵 𝐶 = Σ 𝑧 ∈ ( { 𝑦 } × ⦋ 𝑦 / 𝑗 ⦌ 𝐵 ) 𝐷 )
116 8 115 oveq12d ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( Σ 𝑗 ∈ 𝑥 Σ 𝑘 ∈ 𝐵 𝐶 + Σ 𝑗 ∈ { 𝑦 } Σ 𝑘 ∈ 𝐵 𝐶 ) = ( Σ 𝑧 ∈ ∪ 𝑗 ∈ 𝑥 ( { 𝑗 } × 𝐵 ) 𝐷 + Σ 𝑧 ∈ ( { 𝑦 } × ⦋ 𝑦 / 𝑗 ⦌ 𝐵 ) 𝐷 ) )
117 disjsn ⊢ ( ( 𝑥 ∩ { 𝑦 } ) = ∅ ↔ ¬ 𝑦 ∈ 𝑥 )
118 5 117 sylibr ⊢ ( 𝜑 → ( 𝑥 ∩ { 𝑦 } ) = ∅ )
119 eqidd ⊢ ( 𝜑 → ( 𝑥 ∪ { 𝑦 } ) = ( 𝑥 ∪ { 𝑦 } ) )
120 2 6 ssfid ⊢ ( 𝜑 → ( 𝑥 ∪ { 𝑦 } ) ∈ Fin )
121 6 sselda ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 𝑥 ∪ { 𝑦 } ) ) → 𝑗 ∈ 𝐴 )
122 4 anassrs ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) ∧ 𝑘 ∈ 𝐵 ) → 𝐶 ∈ ℂ )
123 3 122 fsumcl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) → Σ 𝑘 ∈ 𝐵 𝐶 ∈ ℂ )
124 121 123 syldan ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 𝑥 ∪ { 𝑦 } ) ) → Σ 𝑘 ∈ 𝐵 𝐶 ∈ ℂ )
125 118 119 120 124 fsumsplit ⊢ ( 𝜑 → Σ 𝑗 ∈ ( 𝑥 ∪ { 𝑦 } ) Σ 𝑘 ∈ 𝐵 𝐶 = ( Σ 𝑗 ∈ 𝑥 Σ 𝑘 ∈ 𝐵 𝐶 + Σ 𝑗 ∈ { 𝑦 } Σ 𝑘 ∈ 𝐵 𝐶 ) )
126 125 adantr ⊢ ( ( 𝜑 ∧ 𝜓 ) → Σ 𝑗 ∈ ( 𝑥 ∪ { 𝑦 } ) Σ 𝑘 ∈ 𝐵 𝐶 = ( Σ 𝑗 ∈ 𝑥 Σ 𝑘 ∈ 𝐵 𝐶 + Σ 𝑗 ∈ { 𝑦 } Σ 𝑘 ∈ 𝐵 𝐶 ) )
127 eliun ⊢ ( 𝑧 ∈ ∪ 𝑗 ∈ 𝑥 ( { 𝑗 } × 𝐵 ) ↔ ∃ 𝑗 ∈ 𝑥 𝑧 ∈ ( { 𝑗 } × 𝐵 ) )
128 xp1st ⊢ ( 𝑧 ∈ ( { 𝑗 } × 𝐵 ) → ( 1st ‘ 𝑧 ) ∈ { 𝑗 } )
129 elsni ⊢ ( ( 1st ‘ 𝑧 ) ∈ { 𝑗 } → ( 1st ‘ 𝑧 ) = 𝑗 )
130 128 129 syl ⊢ ( 𝑧 ∈ ( { 𝑗 } × 𝐵 ) → ( 1st ‘ 𝑧 ) = 𝑗 )
131 130 adantl ⊢ ( ( 𝑗 ∈ 𝑥 ∧ 𝑧 ∈ ( { 𝑗 } × 𝐵 ) ) → ( 1st ‘ 𝑧 ) = 𝑗 )
132 simpl ⊢ ( ( 𝑗 ∈ 𝑥 ∧ 𝑧 ∈ ( { 𝑗 } × 𝐵 ) ) → 𝑗 ∈ 𝑥 )
133 131 132 eqeltrd ⊢ ( ( 𝑗 ∈ 𝑥 ∧ 𝑧 ∈ ( { 𝑗 } × 𝐵 ) ) → ( 1st ‘ 𝑧 ) ∈ 𝑥 )
134 133 rexlimiva ⊢ ( ∃ 𝑗 ∈ 𝑥 𝑧 ∈ ( { 𝑗 } × 𝐵 ) → ( 1st ‘ 𝑧 ) ∈ 𝑥 )
135 127 134 sylbi ⊢ ( 𝑧 ∈ ∪ 𝑗 ∈ 𝑥 ( { 𝑗 } × 𝐵 ) → ( 1st ‘ 𝑧 ) ∈ 𝑥 )
136 xp1st ⊢ ( 𝑧 ∈ ( { 𝑦 } × ⦋ 𝑦 / 𝑗 ⦌ 𝐵 ) → ( 1st ‘ 𝑧 ) ∈ { 𝑦 } )
137 135 136 anim12i ⊢ ( ( 𝑧 ∈ ∪ 𝑗 ∈ 𝑥 ( { 𝑗 } × 𝐵 ) ∧ 𝑧 ∈ ( { 𝑦 } × ⦋ 𝑦 / 𝑗 ⦌ 𝐵 ) ) → ( ( 1st ‘ 𝑧 ) ∈ 𝑥 ∧ ( 1st ‘ 𝑧 ) ∈ { 𝑦 } ) )
138 elin ⊢ ( 𝑧 ∈ ( ∪ 𝑗 ∈ 𝑥 ( { 𝑗 } × 𝐵 ) ∩ ( { 𝑦 } × ⦋ 𝑦 / 𝑗 ⦌ 𝐵 ) ) ↔ ( 𝑧 ∈ ∪ 𝑗 ∈ 𝑥 ( { 𝑗 } × 𝐵 ) ∧ 𝑧 ∈ ( { 𝑦 } × ⦋ 𝑦 / 𝑗 ⦌ 𝐵 ) ) )
139 elin ⊢ ( ( 1st ‘ 𝑧 ) ∈ ( 𝑥 ∩ { 𝑦 } ) ↔ ( ( 1st ‘ 𝑧 ) ∈ 𝑥 ∧ ( 1st ‘ 𝑧 ) ∈ { 𝑦 } ) )
140 137 138 139 3imtr4i ⊢ ( 𝑧 ∈ ( ∪ 𝑗 ∈ 𝑥 ( { 𝑗 } × 𝐵 ) ∩ ( { 𝑦 } × ⦋ 𝑦 / 𝑗 ⦌ 𝐵 ) ) → ( 1st ‘ 𝑧 ) ∈ ( 𝑥 ∩ { 𝑦 } ) )
141 118 eleq2d ⊢ ( 𝜑 → ( ( 1st ‘ 𝑧 ) ∈ ( 𝑥 ∩ { 𝑦 } ) ↔ ( 1st ‘ 𝑧 ) ∈ ∅ ) )
142 noel ⊢ ¬ ( 1st ‘ 𝑧 ) ∈ ∅
143 142 pm2.21i ⊢ ( ( 1st ‘ 𝑧 ) ∈ ∅ → 𝑧 ∈ ∅ )
144 141 143 biimtrdi ⊢ ( 𝜑 → ( ( 1st ‘ 𝑧 ) ∈ ( 𝑥 ∩ { 𝑦 } ) → 𝑧 ∈ ∅ ) )
145 140 144 syl5 ⊢ ( 𝜑 → ( 𝑧 ∈ ( ∪ 𝑗 ∈ 𝑥 ( { 𝑗 } × 𝐵 ) ∩ ( { 𝑦 } × ⦋ 𝑦 / 𝑗 ⦌ 𝐵 ) ) → 𝑧 ∈ ∅ ) )
146 145 ssrdv ⊢ ( 𝜑 → ( ∪ 𝑗 ∈ 𝑥 ( { 𝑗 } × 𝐵 ) ∩ ( { 𝑦 } × ⦋ 𝑦 / 𝑗 ⦌ 𝐵 ) ) ⊆ ∅ )
147 ss0 ⊢ ( ( ∪ 𝑗 ∈ 𝑥 ( { 𝑗 } × 𝐵 ) ∩ ( { 𝑦 } × ⦋ 𝑦 / 𝑗 ⦌ 𝐵 ) ) ⊆ ∅ → ( ∪ 𝑗 ∈ 𝑥 ( { 𝑗 } × 𝐵 ) ∩ ( { 𝑦 } × ⦋ 𝑦 / 𝑗 ⦌ 𝐵 ) ) = ∅ )
148 146 147 syl ⊢ ( 𝜑 → ( ∪ 𝑗 ∈ 𝑥 ( { 𝑗 } × 𝐵 ) ∩ ( { 𝑦 } × ⦋ 𝑦 / 𝑗 ⦌ 𝐵 ) ) = ∅ )
149 iunxun ⊢ ∪ 𝑗 ∈ ( 𝑥 ∪ { 𝑦 } ) ( { 𝑗 } × 𝐵 ) = ( ∪ 𝑗 ∈ 𝑥 ( { 𝑗 } × 𝐵 ) ∪ ∪ 𝑗 ∈ { 𝑦 } ( { 𝑗 } × 𝐵 ) )
150 nfcv ⊢ Ⅎ 𝑚 ( { 𝑗 } × 𝐵 )
151 nfcv ⊢ Ⅎ 𝑗 { 𝑚 }
152 151 14 nfxp ⊢ Ⅎ 𝑗 ( { 𝑚 } × ⦋ 𝑚 / 𝑗 ⦌ 𝐵 )
153 sneq ⊢ ( 𝑗 = 𝑚 → { 𝑗 } = { 𝑚 } )
154 153 9 xpeq12d ⊢ ( 𝑗 = 𝑚 → ( { 𝑗 } × 𝐵 ) = ( { 𝑚 } × ⦋ 𝑚 / 𝑗 ⦌ 𝐵 ) )
155 150 152 154 cbviun ⊢ ∪ 𝑗 ∈ { 𝑦 } ( { 𝑗 } × 𝐵 ) = ∪ 𝑚 ∈ { 𝑦 } ( { 𝑚 } × ⦋ 𝑚 / 𝑗 ⦌ 𝐵 )
156 sneq ⊢ ( 𝑚 = 𝑦 → { 𝑚 } = { 𝑦 } )
157 156 40 xpeq12d ⊢ ( 𝑚 = 𝑦 → ( { 𝑚 } × ⦋ 𝑚 / 𝑗 ⦌ 𝐵 ) = ( { 𝑦 } × ⦋ 𝑦 / 𝑗 ⦌ 𝐵 ) )
158 19 157 iunxsn ⊢ ∪ 𝑚 ∈ { 𝑦 } ( { 𝑚 } × ⦋ 𝑚 / 𝑗 ⦌ 𝐵 ) = ( { 𝑦 } × ⦋ 𝑦 / 𝑗 ⦌ 𝐵 )
159 155 158 eqtri ⊢ ∪ 𝑗 ∈ { 𝑦 } ( { 𝑗 } × 𝐵 ) = ( { 𝑦 } × ⦋ 𝑦 / 𝑗 ⦌ 𝐵 )
160 159 uneq2i ⊢ ( ∪ 𝑗 ∈ 𝑥 ( { 𝑗 } × 𝐵 ) ∪ ∪ 𝑗 ∈ { 𝑦 } ( { 𝑗 } × 𝐵 ) ) = ( ∪ 𝑗 ∈ 𝑥 ( { 𝑗 } × 𝐵 ) ∪ ( { 𝑦 } × ⦋ 𝑦 / 𝑗 ⦌ 𝐵 ) )
161 149 160 eqtri ⊢ ∪ 𝑗 ∈ ( 𝑥 ∪ { 𝑦 } ) ( { 𝑗 } × 𝐵 ) = ( ∪ 𝑗 ∈ 𝑥 ( { 𝑗 } × 𝐵 ) ∪ ( { 𝑦 } × ⦋ 𝑦 / 𝑗 ⦌ 𝐵 ) )
162 161 a1i ⊢ ( 𝜑 → ∪ 𝑗 ∈ ( 𝑥 ∪ { 𝑦 } ) ( { 𝑗 } × 𝐵 ) = ( ∪ 𝑗 ∈ 𝑥 ( { 𝑗 } × 𝐵 ) ∪ ( { 𝑦 } × ⦋ 𝑦 / 𝑗 ⦌ 𝐵 ) ) )
163 snfi ⊢ { 𝑗 } ∈ Fin
164 121 3 syldan ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 𝑥 ∪ { 𝑦 } ) ) → 𝐵 ∈ Fin )
165 xpfi ⊢ ( ( { 𝑗 } ∈ Fin ∧ 𝐵 ∈ Fin ) → ( { 𝑗 } × 𝐵 ) ∈ Fin )
166 163 164 165 sylancr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 𝑥 ∪ { 𝑦 } ) ) → ( { 𝑗 } × 𝐵 ) ∈ Fin )
167 166 ralrimiva ⊢ ( 𝜑 → ∀ 𝑗 ∈ ( 𝑥 ∪ { 𝑦 } ) ( { 𝑗 } × 𝐵 ) ∈ Fin )
168 iunfi ⊢ ( ( ( 𝑥 ∪ { 𝑦 } ) ∈ Fin ∧ ∀ 𝑗 ∈ ( 𝑥 ∪ { 𝑦 } ) ( { 𝑗 } × 𝐵 ) ∈ Fin ) → ∪ 𝑗 ∈ ( 𝑥 ∪ { 𝑦 } ) ( { 𝑗 } × 𝐵 ) ∈ Fin )
169 120 167 168 syl2anc ⊢ ( 𝜑 → ∪ 𝑗 ∈ ( 𝑥 ∪ { 𝑦 } ) ( { 𝑗 } × 𝐵 ) ∈ Fin )
170 eliun ⊢ ( 𝑧 ∈ ∪ 𝑗 ∈ ( 𝑥 ∪ { 𝑦 } ) ( { 𝑗 } × 𝐵 ) ↔ ∃ 𝑗 ∈ ( 𝑥 ∪ { 𝑦 } ) 𝑧 ∈ ( { 𝑗 } × 𝐵 ) )
171 elxp ⊢ ( 𝑧 ∈ ( { 𝑗 } × 𝐵 ) ↔ ∃ 𝑚 ∃ 𝑘 ( 𝑧 = ⟨ 𝑚 , 𝑘 ⟩ ∧ ( 𝑚 ∈ { 𝑗 } ∧ 𝑘 ∈ 𝐵 ) ) )
172 simprl ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 𝑥 ∪ { 𝑦 } ) ) ∧ ( 𝑧 = ⟨ 𝑚 , 𝑘 ⟩ ∧ ( 𝑚 ∈ { 𝑗 } ∧ 𝑘 ∈ 𝐵 ) ) ) → 𝑧 = ⟨ 𝑚 , 𝑘 ⟩ )
173 simprrl ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 𝑥 ∪ { 𝑦 } ) ) ∧ ( 𝑧 = ⟨ 𝑚 , 𝑘 ⟩ ∧ ( 𝑚 ∈ { 𝑗 } ∧ 𝑘 ∈ 𝐵 ) ) ) → 𝑚 ∈ { 𝑗 } )
174 elsni ⊢ ( 𝑚 ∈ { 𝑗 } → 𝑚 = 𝑗 )
175 173 174 syl ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 𝑥 ∪ { 𝑦 } ) ) ∧ ( 𝑧 = ⟨ 𝑚 , 𝑘 ⟩ ∧ ( 𝑚 ∈ { 𝑗 } ∧ 𝑘 ∈ 𝐵 ) ) ) → 𝑚 = 𝑗 )
176 175 opeq1d ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 𝑥 ∪ { 𝑦 } ) ) ∧ ( 𝑧 = ⟨ 𝑚 , 𝑘 ⟩ ∧ ( 𝑚 ∈ { 𝑗 } ∧ 𝑘 ∈ 𝐵 ) ) ) → ⟨ 𝑚 , 𝑘 ⟩ = ⟨ 𝑗 , 𝑘 ⟩ )
177 172 176 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 𝑥 ∪ { 𝑦 } ) ) ∧ ( 𝑧 = ⟨ 𝑚 , 𝑘 ⟩ ∧ ( 𝑚 ∈ { 𝑗 } ∧ 𝑘 ∈ 𝐵 ) ) ) → 𝑧 = ⟨ 𝑗 , 𝑘 ⟩ )
178 177 1 syl ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 𝑥 ∪ { 𝑦 } ) ) ∧ ( 𝑧 = ⟨ 𝑚 , 𝑘 ⟩ ∧ ( 𝑚 ∈ { 𝑗 } ∧ 𝑘 ∈ 𝐵 ) ) ) → 𝐷 = 𝐶 )
179 simpll ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 𝑥 ∪ { 𝑦 } ) ) ∧ ( 𝑧 = ⟨ 𝑚 , 𝑘 ⟩ ∧ ( 𝑚 ∈ { 𝑗 } ∧ 𝑘 ∈ 𝐵 ) ) ) → 𝜑 )
180 121 adantr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 𝑥 ∪ { 𝑦 } ) ) ∧ ( 𝑧 = ⟨ 𝑚 , 𝑘 ⟩ ∧ ( 𝑚 ∈ { 𝑗 } ∧ 𝑘 ∈ 𝐵 ) ) ) → 𝑗 ∈ 𝐴 )
181 simprrr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 𝑥 ∪ { 𝑦 } ) ) ∧ ( 𝑧 = ⟨ 𝑚 , 𝑘 ⟩ ∧ ( 𝑚 ∈ { 𝑗 } ∧ 𝑘 ∈ 𝐵 ) ) ) → 𝑘 ∈ 𝐵 )
182 179 180 181 4 syl12anc ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 𝑥 ∪ { 𝑦 } ) ) ∧ ( 𝑧 = ⟨ 𝑚 , 𝑘 ⟩ ∧ ( 𝑚 ∈ { 𝑗 } ∧ 𝑘 ∈ 𝐵 ) ) ) → 𝐶 ∈ ℂ )
183 178 182 eqeltrd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 𝑥 ∪ { 𝑦 } ) ) ∧ ( 𝑧 = ⟨ 𝑚 , 𝑘 ⟩ ∧ ( 𝑚 ∈ { 𝑗 } ∧ 𝑘 ∈ 𝐵 ) ) ) → 𝐷 ∈ ℂ )
184 183 ex ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 𝑥 ∪ { 𝑦 } ) ) → ( ( 𝑧 = ⟨ 𝑚 , 𝑘 ⟩ ∧ ( 𝑚 ∈ { 𝑗 } ∧ 𝑘 ∈ 𝐵 ) ) → 𝐷 ∈ ℂ ) )
185 184 exlimdvv ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 𝑥 ∪ { 𝑦 } ) ) → ( ∃ 𝑚 ∃ 𝑘 ( 𝑧 = ⟨ 𝑚 , 𝑘 ⟩ ∧ ( 𝑚 ∈ { 𝑗 } ∧ 𝑘 ∈ 𝐵 ) ) → 𝐷 ∈ ℂ ) )
186 171 185 biimtrid ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 𝑥 ∪ { 𝑦 } ) ) → ( 𝑧 ∈ ( { 𝑗 } × 𝐵 ) → 𝐷 ∈ ℂ ) )
187 186 rexlimdva ⊢ ( 𝜑 → ( ∃ 𝑗 ∈ ( 𝑥 ∪ { 𝑦 } ) 𝑧 ∈ ( { 𝑗 } × 𝐵 ) → 𝐷 ∈ ℂ ) )
188 170 187 biimtrid ⊢ ( 𝜑 → ( 𝑧 ∈ ∪ 𝑗 ∈ ( 𝑥 ∪ { 𝑦 } ) ( { 𝑗 } × 𝐵 ) → 𝐷 ∈ ℂ ) )
189 188 imp ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ∪ 𝑗 ∈ ( 𝑥 ∪ { 𝑦 } ) ( { 𝑗 } × 𝐵 ) ) → 𝐷 ∈ ℂ )
190 148 162 169 189 fsumsplit ⊢ ( 𝜑 → Σ 𝑧 ∈ ∪ 𝑗 ∈ ( 𝑥 ∪ { 𝑦 } ) ( { 𝑗 } × 𝐵 ) 𝐷 = ( Σ 𝑧 ∈ ∪ 𝑗 ∈ 𝑥 ( { 𝑗 } × 𝐵 ) 𝐷 + Σ 𝑧 ∈ ( { 𝑦 } × ⦋ 𝑦 / 𝑗 ⦌ 𝐵 ) 𝐷 ) )
191 190 adantr ⊢ ( ( 𝜑 ∧ 𝜓 ) → Σ 𝑧 ∈ ∪ 𝑗 ∈ ( 𝑥 ∪ { 𝑦 } ) ( { 𝑗 } × 𝐵 ) 𝐷 = ( Σ 𝑧 ∈ ∪ 𝑗 ∈ 𝑥 ( { 𝑗 } × 𝐵 ) 𝐷 + Σ 𝑧 ∈ ( { 𝑦 } × ⦋ 𝑦 / 𝑗 ⦌ 𝐵 ) 𝐷 ) )
192 116 126 191 3eqtr4d ⊢ ( ( 𝜑 ∧ 𝜓 ) → Σ 𝑗 ∈ ( 𝑥 ∪ { 𝑦 } ) Σ 𝑘 ∈ 𝐵 𝐶 = Σ 𝑧 ∈ ∪ 𝑗 ∈ ( 𝑥 ∪ { 𝑦 } ) ( { 𝑗 } × 𝐵 ) 𝐷 )