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