Theorem fsum2dlemstep 11203

Description: Lemma for fsum2d 11204- induction step. (Contributed by Mario Carneiro, 23-Apr-2014.) (Revised by Jim Kingdon, 8-Oct-2022.)

Hypotheses

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

Assertion

Ref	Expression
fsum2dlemstep	⊢ ((𝜑 ∧ 𝜓) → Σ𝑗 ∈ (𝑥 ∪ {𝑦})Σ𝑘 ∈ 𝐵 𝐶 = Σ𝑧 ∈ ∪ 𝑗 ∈ (𝑥 ∪ {𝑦})({𝑗} × 𝐵)𝐷)

Distinct variable groups:   𝑗,𝑘,𝑥,𝑦,𝑧,𝐴   𝐵,𝑘,𝑥,𝑦,𝑧   𝐷,𝑗,𝑘,𝑥,𝑦   𝑥,𝐶,𝑦,𝑧   𝜑,𝑗,𝑘,𝑧

Allowed substitution hints:   𝜑(𝑥,𝑦)   𝜓(𝑥,𝑦,𝑧,𝑗,𝑘)   𝐵(𝑗)   𝐶(𝑗,𝑘)   𝐷(𝑧)

Proof of Theorem fsum2dlemstep

Dummy variable 𝑚 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		simpr 109	. . . 4 ⊢ ((𝜑 ∧ 𝜓) → 𝜓)
2		fsum2d.7	. . . 4 ⊢ (𝜓 ↔ Σ𝑗 ∈ 𝑥 Σ𝑘 ∈ 𝐵 𝐶 = Σ𝑧 ∈ ∪ 𝑗 ∈ 𝑥 ({𝑗} × 𝐵)𝐷)
3	1, 2	sylib 121	. . 3 ⊢ ((𝜑 ∧ 𝜓) → Σ𝑗 ∈ 𝑥 Σ𝑘 ∈ 𝐵 𝐶 = Σ𝑧 ∈ ∪ 𝑗 ∈ 𝑥 ({𝑗} × 𝐵)𝐷)
4		nfcv 2281	. . . . . 6 ⊢ Ⅎ𝑚Σ𝑘 ∈ 𝐵 𝐶
5		nfcsb1v 3035	. . . . . . 7 ⊢ Ⅎ𝑗⦋𝑚 / 𝑗⦌𝐵
6		nfcsb1v 3035	. . . . . . 7 ⊢ Ⅎ𝑗⦋𝑚 / 𝑗⦌𝐶
7	5, 6	nfsum 11126	. . . . . 6 ⊢ Ⅎ𝑗Σ𝑘 ∈ ⦋ 𝑚 / 𝑗⦌𝐵⦋𝑚 / 𝑗⦌𝐶
8		csbeq1a 3012	. . . . . . 7 ⊢ (𝑗 = 𝑚 → 𝐵 = ⦋𝑚 / 𝑗⦌𝐵)
9		csbeq1a 3012	. . . . . . . 8 ⊢ (𝑗 = 𝑚 → 𝐶 = ⦋𝑚 / 𝑗⦌𝐶)
10	9	adantr 274	. . . . . . 7 ⊢ ((𝑗 = 𝑚 ∧ 𝑘 ∈ 𝐵) → 𝐶 = ⦋𝑚 / 𝑗⦌𝐶)
11	8, 10	sumeq12dv 11141	. . . . . 6 ⊢ (𝑗 = 𝑚 → Σ𝑘 ∈ 𝐵 𝐶 = Σ𝑘 ∈ ⦋ 𝑚 / 𝑗⦌𝐵⦋𝑚 / 𝑗⦌𝐶)
12	4, 7, 11	cbvsumi 11131	. . . . 5 ⊢ Σ𝑗 ∈ {𝑦}Σ𝑘 ∈ 𝐵 𝐶 = Σ𝑚 ∈ {𝑦}Σ𝑘 ∈ ⦋ 𝑚 / 𝑗⦌𝐵⦋𝑚 / 𝑗⦌𝐶
13		fsum2d.6	. . . . . . . . 9 ⊢ (𝜑 → (𝑥 ∪ {𝑦}) ⊆ 𝐴)
14	13	unssbd 3254	. . . . . . . 8 ⊢ (𝜑 → {𝑦} ⊆ 𝐴)
15		vex 2689	. . . . . . . . 9 ⊢ 𝑦 ∈ V
16	15	snss 3649	. . . . . . . 8 ⊢ (𝑦 ∈ 𝐴 ↔ {𝑦} ⊆ 𝐴)
17	14, 16	sylibr 133	. . . . . . 7 ⊢ (𝜑 → 𝑦 ∈ 𝐴)
18		fsum2d.3	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → 𝐵 ∈ Fin)
19	18	ralrimiva 2505	. . . . . . . . 9 ⊢ (𝜑 → ∀𝑗 ∈ 𝐴 𝐵 ∈ Fin)
20		nfcsb1v 3035	. . . . . . . . . . 11 ⊢ Ⅎ𝑗⦋𝑦 / 𝑗⦌𝐵
21	20	nfel1 2292	. . . . . . . . . 10 ⊢ Ⅎ𝑗⦋𝑦 / 𝑗⦌𝐵 ∈ Fin
22		csbeq1a 3012	. . . . . . . . . . 11 ⊢ (𝑗 = 𝑦 → 𝐵 = ⦋𝑦 / 𝑗⦌𝐵)
23	22	eleq1d 2208	. . . . . . . . . 10 ⊢ (𝑗 = 𝑦 → (𝐵 ∈ Fin ↔ ⦋𝑦 / 𝑗⦌𝐵 ∈ Fin))
24	21, 23	rspc 2783	. . . . . . . . 9 ⊢ (𝑦 ∈ 𝐴 → (∀𝑗 ∈ 𝐴 𝐵 ∈ Fin → ⦋𝑦 / 𝑗⦌𝐵 ∈ Fin))
25	17, 19, 24	sylc 62	. . . . . . . 8 ⊢ (𝜑 → ⦋𝑦 / 𝑗⦌𝐵 ∈ Fin)
26		fsum2d.4	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵)) → 𝐶 ∈ ℂ)
27	26	ralrimivva 2514	. . . . . . . . . 10 ⊢ (𝜑 → ∀𝑗 ∈ 𝐴 ∀𝑘 ∈ 𝐵 𝐶 ∈ ℂ)
28		nfcsb1v 3035	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑗⦋𝑦 / 𝑗⦌𝐶
29	28	nfel1 2292	. . . . . . . . . . . 12 ⊢ Ⅎ𝑗⦋𝑦 / 𝑗⦌𝐶 ∈ ℂ
30	20, 29	nfralxy 2471	. . . . . . . . . . 11 ⊢ Ⅎ𝑗∀𝑘 ∈ ⦋ 𝑦 / 𝑗⦌𝐵⦋𝑦 / 𝑗⦌𝐶 ∈ ℂ
31		csbeq1a 3012	. . . . . . . . . . . . 13 ⊢ (𝑗 = 𝑦 → 𝐶 = ⦋𝑦 / 𝑗⦌𝐶)
32	31	eleq1d 2208	. . . . . . . . . . . 12 ⊢ (𝑗 = 𝑦 → (𝐶 ∈ ℂ ↔ ⦋𝑦 / 𝑗⦌𝐶 ∈ ℂ))
33	22, 32	raleqbidv 2638	. . . . . . . . . . 11 ⊢ (𝑗 = 𝑦 → (∀𝑘 ∈ 𝐵 𝐶 ∈ ℂ ↔ ∀𝑘 ∈ ⦋ 𝑦 / 𝑗⦌𝐵⦋𝑦 / 𝑗⦌𝐶 ∈ ℂ))
34	30, 33	rspc 2783	. . . . . . . . . 10 ⊢ (𝑦 ∈ 𝐴 → (∀𝑗 ∈ 𝐴 ∀𝑘 ∈ 𝐵 𝐶 ∈ ℂ → ∀𝑘 ∈ ⦋ 𝑦 / 𝑗⦌𝐵⦋𝑦 / 𝑗⦌𝐶 ∈ ℂ))
35	17, 27, 34	sylc 62	. . . . . . . . 9 ⊢ (𝜑 → ∀𝑘 ∈ ⦋ 𝑦 / 𝑗⦌𝐵⦋𝑦 / 𝑗⦌𝐶 ∈ ℂ)
36	35	r19.21bi 2520	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ ⦋𝑦 / 𝑗⦌𝐵) → ⦋𝑦 / 𝑗⦌𝐶 ∈ ℂ)
37	25, 36	fsumcl 11169	. . . . . . 7 ⊢ (𝜑 → Σ𝑘 ∈ ⦋ 𝑦 / 𝑗⦌𝐵⦋𝑦 / 𝑗⦌𝐶 ∈ ℂ)
38		csbeq1 3006	. . . . . . . . 9 ⊢ (𝑚 = 𝑦 → ⦋𝑚 / 𝑗⦌𝐵 = ⦋𝑦 / 𝑗⦌𝐵)
39		csbeq1 3006	. . . . . . . . . 10 ⊢ (𝑚 = 𝑦 → ⦋𝑚 / 𝑗⦌𝐶 = ⦋𝑦 / 𝑗⦌𝐶)
40	39	adantr 274	. . . . . . . . 9 ⊢ ((𝑚 = 𝑦 ∧ 𝑘 ∈ ⦋𝑚 / 𝑗⦌𝐵) → ⦋𝑚 / 𝑗⦌𝐶 = ⦋𝑦 / 𝑗⦌𝐶)
41	38, 40	sumeq12dv 11141	. . . . . . . 8 ⊢ (𝑚 = 𝑦 → Σ𝑘 ∈ ⦋ 𝑚 / 𝑗⦌𝐵⦋𝑚 / 𝑗⦌𝐶 = Σ𝑘 ∈ ⦋ 𝑦 / 𝑗⦌𝐵⦋𝑦 / 𝑗⦌𝐶)
42	41	sumsn 11180	. . . . . . 7 ⊢ ((𝑦 ∈ 𝐴 ∧ Σ𝑘 ∈ ⦋ 𝑦 / 𝑗⦌𝐵⦋𝑦 / 𝑗⦌𝐶 ∈ ℂ) → Σ𝑚 ∈ {𝑦}Σ𝑘 ∈ ⦋ 𝑚 / 𝑗⦌𝐵⦋𝑚 / 𝑗⦌𝐶 = Σ𝑘 ∈ ⦋ 𝑦 / 𝑗⦌𝐵⦋𝑦 / 𝑗⦌𝐶)
43	17, 37, 42	syl2anc 408	. . . . . 6 ⊢ (𝜑 → Σ𝑚 ∈ {𝑦}Σ𝑘 ∈ ⦋ 𝑚 / 𝑗⦌𝐵⦋𝑚 / 𝑗⦌𝐶 = Σ𝑘 ∈ ⦋ 𝑦 / 𝑗⦌𝐵⦋𝑦 / 𝑗⦌𝐶)
44		nfcv 2281	. . . . . . . 8 ⊢ Ⅎ𝑚⦋𝑦 / 𝑗⦌𝐶
45		nfcsb1v 3035	. . . . . . . 8 ⊢ Ⅎ𝑘⦋𝑚 / 𝑘⦌⦋𝑦 / 𝑗⦌𝐶
46		csbeq1a 3012	. . . . . . . 8 ⊢ (𝑘 = 𝑚 → ⦋𝑦 / 𝑗⦌𝐶 = ⦋𝑚 / 𝑘⦌⦋𝑦 / 𝑗⦌𝐶)
47	44, 45, 46	cbvsumi 11131	. . . . . . 7 ⊢ Σ𝑘 ∈ ⦋ 𝑦 / 𝑗⦌𝐵⦋𝑦 / 𝑗⦌𝐶 = Σ𝑚 ∈ ⦋ 𝑦 / 𝑗⦌𝐵⦋𝑚 / 𝑘⦌⦋𝑦 / 𝑗⦌𝐶
48		csbeq1 3006	. . . . . . . . 9 ⊢ (𝑚 = (2nd ‘𝑧) → ⦋𝑚 / 𝑘⦌⦋𝑦 / 𝑗⦌𝐶 = ⦋(2nd ‘𝑧) / 𝑘⦌⦋𝑦 / 𝑗⦌𝐶)
49		snfig 6708	. . . . . . . . . . 11 ⊢ (𝑦 ∈ V → {𝑦} ∈ Fin)
50	49	elv 2690	. . . . . . . . . 10 ⊢ {𝑦} ∈ Fin
51		xpfi 6818	. . . . . . . . . 10 ⊢ (({𝑦} ∈ Fin ∧ ⦋𝑦 / 𝑗⦌𝐵 ∈ Fin) → ({𝑦} × ⦋𝑦 / 𝑗⦌𝐵) ∈ Fin)
52	50, 25, 51	sylancr 410	. . . . . . . . 9 ⊢ (𝜑 → ({𝑦} × ⦋𝑦 / 𝑗⦌𝐵) ∈ Fin)
53		2ndconst 6119	. . . . . . . . . 10 ⊢ (𝑦 ∈ 𝐴 → (2nd ↾ ({𝑦} × ⦋𝑦 / 𝑗⦌𝐵)):({𝑦} × ⦋𝑦 / 𝑗⦌𝐵)–1-1-onto→⦋𝑦 / 𝑗⦌𝐵)
54	17, 53	syl 14	. . . . . . . . 9 ⊢ (𝜑 → (2nd ↾ ({𝑦} × ⦋𝑦 / 𝑗⦌𝐵)):({𝑦} × ⦋𝑦 / 𝑗⦌𝐵)–1-1-onto→⦋𝑦 / 𝑗⦌𝐵)
55		fvres 5445	. . . . . . . . . 10 ⊢ (𝑧 ∈ ({𝑦} × ⦋𝑦 / 𝑗⦌𝐵) → ((2nd ↾ ({𝑦} × ⦋𝑦 / 𝑗⦌𝐵))‘𝑧) = (2nd ‘𝑧))
56	55	adantl 275	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑧 ∈ ({𝑦} × ⦋𝑦 / 𝑗⦌𝐵)) → ((2nd ↾ ({𝑦} × ⦋𝑦 / 𝑗⦌𝐵))‘𝑧) = (2nd ‘𝑧))
57	45	nfel1 2292	. . . . . . . . . . 11 ⊢ Ⅎ𝑘⦋𝑚 / 𝑘⦌⦋𝑦 / 𝑗⦌𝐶 ∈ ℂ
58	46	eleq1d 2208	. . . . . . . . . . 11 ⊢ (𝑘 = 𝑚 → (⦋𝑦 / 𝑗⦌𝐶 ∈ ℂ ↔ ⦋𝑚 / 𝑘⦌⦋𝑦 / 𝑗⦌𝐶 ∈ ℂ))
59	57, 58	rspc 2783	. . . . . . . . . 10 ⊢ (𝑚 ∈ ⦋𝑦 / 𝑗⦌𝐵 → (∀𝑘 ∈ ⦋ 𝑦 / 𝑗⦌𝐵⦋𝑦 / 𝑗⦌𝐶 ∈ ℂ → ⦋𝑚 / 𝑘⦌⦋𝑦 / 𝑗⦌𝐶 ∈ ℂ))
60	35, 59	mpan9 279	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑚 ∈ ⦋𝑦 / 𝑗⦌𝐵) → ⦋𝑚 / 𝑘⦌⦋𝑦 / 𝑗⦌𝐶 ∈ ℂ)
61	48, 52, 54, 56, 60	fsumf1o 11159	. . . . . . . 8 ⊢ (𝜑 → Σ𝑚 ∈ ⦋ 𝑦 / 𝑗⦌𝐵⦋𝑚 / 𝑘⦌⦋𝑦 / 𝑗⦌𝐶 = Σ𝑧 ∈ ({𝑦} × ⦋𝑦 / 𝑗⦌𝐵)⦋(2nd ‘𝑧) / 𝑘⦌⦋𝑦 / 𝑗⦌𝐶)
62		elxp 4556	. . . . . . . . . . . 12 ⊢ (𝑧 ∈ ({𝑦} × ⦋𝑦 / 𝑗⦌𝐵) ↔ ∃𝑚∃𝑘(𝑧 = ⟨𝑚, 𝑘⟩ ∧ (𝑚 ∈ {𝑦} ∧ 𝑘 ∈ ⦋𝑦 / 𝑗⦌𝐵)))
63		nfv 1508	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑗 𝑧 = ⟨𝑚, 𝑘⟩
64		nfv 1508	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑗 𝑚 ∈ {𝑦}
65	20	nfcri 2275	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑗 𝑘 ∈ ⦋𝑦 / 𝑗⦌𝐵
66	64, 65	nfan 1544	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑗(𝑚 ∈ {𝑦} ∧ 𝑘 ∈ ⦋𝑦 / 𝑗⦌𝐵)
67	63, 66	nfan 1544	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑗(𝑧 = ⟨𝑚, 𝑘⟩ ∧ (𝑚 ∈ {𝑦} ∧ 𝑘 ∈ ⦋𝑦 / 𝑗⦌𝐵))
68	67	nfex 1616	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑗∃𝑘(𝑧 = ⟨𝑚, 𝑘⟩ ∧ (𝑚 ∈ {𝑦} ∧ 𝑘 ∈ ⦋𝑦 / 𝑗⦌𝐵))
69		nfv 1508	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑚∃𝑘(𝑧 = ⟨𝑗, 𝑘⟩ ∧ (𝑗 = 𝑦 ∧ 𝑘 ∈ 𝐵))
70		opeq1 3705	. . . . . . . . . . . . . . . 16 ⊢ (𝑚 = 𝑗 → ⟨𝑚, 𝑘⟩ = ⟨𝑗, 𝑘⟩)
71	70	eqeq2d 2151	. . . . . . . . . . . . . . 15 ⊢ (𝑚 = 𝑗 → (𝑧 = ⟨𝑚, 𝑘⟩ ↔ 𝑧 = ⟨𝑗, 𝑘⟩))
72		eqtr2 2158	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑚 = 𝑗 ∧ 𝑚 = 𝑦) → 𝑗 = 𝑦)
73	72, 22	syl 14	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑚 = 𝑗 ∧ 𝑚 = 𝑦) → 𝐵 = ⦋𝑦 / 𝑗⦌𝐵)
74	73	eleq2d 2209	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑚 = 𝑗 ∧ 𝑚 = 𝑦) → (𝑘 ∈ 𝐵 ↔ 𝑘 ∈ ⦋𝑦 / 𝑗⦌𝐵))
75	74	pm5.32da 447	. . . . . . . . . . . . . . . . 17 ⊢ (𝑚 = 𝑗 → ((𝑚 = 𝑦 ∧ 𝑘 ∈ 𝐵) ↔ (𝑚 = 𝑦 ∧ 𝑘 ∈ ⦋𝑦 / 𝑗⦌𝐵)))
76		velsn 3544	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑚 ∈ {𝑦} ↔ 𝑚 = 𝑦)
77	76	anbi1i 453	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑚 ∈ {𝑦} ∧ 𝑘 ∈ ⦋𝑦 / 𝑗⦌𝐵) ↔ (𝑚 = 𝑦 ∧ 𝑘 ∈ ⦋𝑦 / 𝑗⦌𝐵))
78	75, 77	syl6rbbr 198	. . . . . . . . . . . . . . . 16 ⊢ (𝑚 = 𝑗 → ((𝑚 ∈ {𝑦} ∧ 𝑘 ∈ ⦋𝑦 / 𝑗⦌𝐵) ↔ (𝑚 = 𝑦 ∧ 𝑘 ∈ 𝐵)))
79		equequ1 1688	. . . . . . . . . . . . . . . . 17 ⊢ (𝑚 = 𝑗 → (𝑚 = 𝑦 ↔ 𝑗 = 𝑦))
80	79	anbi1d 460	. . . . . . . . . . . . . . . 16 ⊢ (𝑚 = 𝑗 → ((𝑚 = 𝑦 ∧ 𝑘 ∈ 𝐵) ↔ (𝑗 = 𝑦 ∧ 𝑘 ∈ 𝐵)))
81	78, 80	bitrd 187	. . . . . . . . . . . . . . 15 ⊢ (𝑚 = 𝑗 → ((𝑚 ∈ {𝑦} ∧ 𝑘 ∈ ⦋𝑦 / 𝑗⦌𝐵) ↔ (𝑗 = 𝑦 ∧ 𝑘 ∈ 𝐵)))
82	71, 81	anbi12d 464	. . . . . . . . . . . . . 14 ⊢ (𝑚 = 𝑗 → ((𝑧 = ⟨𝑚, 𝑘⟩ ∧ (𝑚 ∈ {𝑦} ∧ 𝑘 ∈ ⦋𝑦 / 𝑗⦌𝐵)) ↔ (𝑧 = ⟨𝑗, 𝑘⟩ ∧ (𝑗 = 𝑦 ∧ 𝑘 ∈ 𝐵))))
83	82	exbidv 1797	. . . . . . . . . . . . 13 ⊢ (𝑚 = 𝑗 → (∃𝑘(𝑧 = ⟨𝑚, 𝑘⟩ ∧ (𝑚 ∈ {𝑦} ∧ 𝑘 ∈ ⦋𝑦 / 𝑗⦌𝐵)) ↔ ∃𝑘(𝑧 = ⟨𝑗, 𝑘⟩ ∧ (𝑗 = 𝑦 ∧ 𝑘 ∈ 𝐵))))
84	68, 69, 83	cbvex 1729	. . . . . . . . . . . 12 ⊢ (∃𝑚∃𝑘(𝑧 = ⟨𝑚, 𝑘⟩ ∧ (𝑚 ∈ {𝑦} ∧ 𝑘 ∈ ⦋𝑦 / 𝑗⦌𝐵)) ↔ ∃𝑗∃𝑘(𝑧 = ⟨𝑗, 𝑘⟩ ∧ (𝑗 = 𝑦 ∧ 𝑘 ∈ 𝐵)))
85	62, 84	bitri 183	. . . . . . . . . . 11 ⊢ (𝑧 ∈ ({𝑦} × ⦋𝑦 / 𝑗⦌𝐵) ↔ ∃𝑗∃𝑘(𝑧 = ⟨𝑗, 𝑘⟩ ∧ (𝑗 = 𝑦 ∧ 𝑘 ∈ 𝐵)))
86		nfv 1508	. . . . . . . . . . . 12 ⊢ Ⅎ𝑗𝜑
87		nfcv 2281	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑗(2nd ‘𝑧)
88	87, 28	nfcsb 3037	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑗⦋(2nd ‘𝑧) / 𝑘⦌⦋𝑦 / 𝑗⦌𝐶
89	88	nfeq2 2293	. . . . . . . . . . . 12 ⊢ Ⅎ𝑗 𝐷 = ⦋(2nd ‘𝑧) / 𝑘⦌⦋𝑦 / 𝑗⦌𝐶
90		nfv 1508	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑘𝜑
91		nfcsb1v 3035	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑘⦋(2nd ‘𝑧) / 𝑘⦌⦋𝑦 / 𝑗⦌𝐶
92	91	nfeq2 2293	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑘 𝐷 = ⦋(2nd ‘𝑧) / 𝑘⦌⦋𝑦 / 𝑗⦌𝐶
93		fsum2d.1	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 = ⟨𝑗, 𝑘⟩ → 𝐷 = 𝐶)
94	93	ad2antlr 480	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑧 = ⟨𝑗, 𝑘⟩) ∧ (𝑗 = 𝑦 ∧ 𝑘 ∈ 𝐵)) → 𝐷 = 𝐶)
95	31	ad2antrl 481	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑧 = ⟨𝑗, 𝑘⟩) ∧ (𝑗 = 𝑦 ∧ 𝑘 ∈ 𝐵)) → 𝐶 = ⦋𝑦 / 𝑗⦌𝐶)
96		fveq2 5421	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 = ⟨𝑗, 𝑘⟩ → (2nd ‘𝑧) = (2nd ‘⟨𝑗, 𝑘⟩))
97		vex 2689	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝑗 ∈ V
98		vex 2689	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝑘 ∈ V
99	97, 98	op2nd 6045	. . . . . . . . . . . . . . . . . 18 ⊢ (2nd ‘⟨𝑗, 𝑘⟩) = 𝑘
100	96, 99	syl6req 2189	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 = ⟨𝑗, 𝑘⟩ → 𝑘 = (2nd ‘𝑧))
101	100	ad2antlr 480	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑧 = ⟨𝑗, 𝑘⟩) ∧ (𝑗 = 𝑦 ∧ 𝑘 ∈ 𝐵)) → 𝑘 = (2nd ‘𝑧))
102		csbeq1a 3012	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 = (2nd ‘𝑧) → ⦋𝑦 / 𝑗⦌𝐶 = ⦋(2nd ‘𝑧) / 𝑘⦌⦋𝑦 / 𝑗⦌𝐶)
103	101, 102	syl 14	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑧 = ⟨𝑗, 𝑘⟩) ∧ (𝑗 = 𝑦 ∧ 𝑘 ∈ 𝐵)) → ⦋𝑦 / 𝑗⦌𝐶 = ⦋(2nd ‘𝑧) / 𝑘⦌⦋𝑦 / 𝑗⦌𝐶)
104	94, 95, 103	3eqtrd 2176	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑧 = ⟨𝑗, 𝑘⟩) ∧ (𝑗 = 𝑦 ∧ 𝑘 ∈ 𝐵)) → 𝐷 = ⦋(2nd ‘𝑧) / 𝑘⦌⦋𝑦 / 𝑗⦌𝐶)
105	104	expl 375	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑧 = ⟨𝑗, 𝑘⟩ ∧ (𝑗 = 𝑦 ∧ 𝑘 ∈ 𝐵)) → 𝐷 = ⦋(2nd ‘𝑧) / 𝑘⦌⦋𝑦 / 𝑗⦌𝐶))
106	90, 92, 105	exlimd 1576	. . . . . . . . . . . 12 ⊢ (𝜑 → (∃𝑘(𝑧 = ⟨𝑗, 𝑘⟩ ∧ (𝑗 = 𝑦 ∧ 𝑘 ∈ 𝐵)) → 𝐷 = ⦋(2nd ‘𝑧) / 𝑘⦌⦋𝑦 / 𝑗⦌𝐶))
107	86, 89, 106	exlimd 1576	. . . . . . . . . . 11 ⊢ (𝜑 → (∃𝑗∃𝑘(𝑧 = ⟨𝑗, 𝑘⟩ ∧ (𝑗 = 𝑦 ∧ 𝑘 ∈ 𝐵)) → 𝐷 = ⦋(2nd ‘𝑧) / 𝑘⦌⦋𝑦 / 𝑗⦌𝐶))
108	85, 107	syl5bi 151	. . . . . . . . . 10 ⊢ (𝜑 → (𝑧 ∈ ({𝑦} × ⦋𝑦 / 𝑗⦌𝐵) → 𝐷 = ⦋(2nd ‘𝑧) / 𝑘⦌⦋𝑦 / 𝑗⦌𝐶))
109	108	imp 123	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑧 ∈ ({𝑦} × ⦋𝑦 / 𝑗⦌𝐵)) → 𝐷 = ⦋(2nd ‘𝑧) / 𝑘⦌⦋𝑦 / 𝑗⦌𝐶)
110	109	sumeq2dv 11137	. . . . . . . 8 ⊢ (𝜑 → Σ𝑧 ∈ ({𝑦} × ⦋𝑦 / 𝑗⦌𝐵)𝐷 = Σ𝑧 ∈ ({𝑦} × ⦋𝑦 / 𝑗⦌𝐵)⦋(2nd ‘𝑧) / 𝑘⦌⦋𝑦 / 𝑗⦌𝐶)
111	61, 110	eqtr4d 2175	. . . . . . 7 ⊢ (𝜑 → Σ𝑚 ∈ ⦋ 𝑦 / 𝑗⦌𝐵⦋𝑚 / 𝑘⦌⦋𝑦 / 𝑗⦌𝐶 = Σ𝑧 ∈ ({𝑦} × ⦋𝑦 / 𝑗⦌𝐵)𝐷)
112	47, 111	syl5eq 2184	. . . . . 6 ⊢ (𝜑 → Σ𝑘 ∈ ⦋ 𝑦 / 𝑗⦌𝐵⦋𝑦 / 𝑗⦌𝐶 = Σ𝑧 ∈ ({𝑦} × ⦋𝑦 / 𝑗⦌𝐵)𝐷)
113	43, 112	eqtrd 2172	. . . . 5 ⊢ (𝜑 → Σ𝑚 ∈ {𝑦}Σ𝑘 ∈ ⦋ 𝑚 / 𝑗⦌𝐵⦋𝑚 / 𝑗⦌𝐶 = Σ𝑧 ∈ ({𝑦} × ⦋𝑦 / 𝑗⦌𝐵)𝐷)
114	12, 113	syl5eq 2184	. . . 4 ⊢ (𝜑 → Σ𝑗 ∈ {𝑦}Σ𝑘 ∈ 𝐵 𝐶 = Σ𝑧 ∈ ({𝑦} × ⦋𝑦 / 𝑗⦌𝐵)𝐷)
115	114	adantr 274	. . 3 ⊢ ((𝜑 ∧ 𝜓) → Σ𝑗 ∈ {𝑦}Σ𝑘 ∈ 𝐵 𝐶 = Σ𝑧 ∈ ({𝑦} × ⦋𝑦 / 𝑗⦌𝐵)𝐷)
116	3, 115	oveq12d 5792	. 2 ⊢ ((𝜑 ∧ 𝜓) → (Σ𝑗 ∈ 𝑥 Σ𝑘 ∈ 𝐵 𝐶 + Σ𝑗 ∈ {𝑦}Σ𝑘 ∈ 𝐵 𝐶) = (Σ𝑧 ∈ ∪ 𝑗 ∈ 𝑥 ({𝑗} × 𝐵)𝐷 + Σ𝑧 ∈ ({𝑦} × ⦋𝑦 / 𝑗⦌𝐵)𝐷))
117		fsum2d.5	. . . . 5 ⊢ (𝜑 → ¬ 𝑦 ∈ 𝑥)
118		disjsn 3585	. . . . 5 ⊢ ((𝑥 ∩ {𝑦}) = ∅ ↔ ¬ 𝑦 ∈ 𝑥)
119	117, 118	sylibr 133	. . . 4 ⊢ (𝜑 → (𝑥 ∩ {𝑦}) = ∅)
120		eqidd 2140	. . . 4 ⊢ (𝜑 → (𝑥 ∪ {𝑦}) = (𝑥 ∪ {𝑦}))
121		fsum2dlemstep.x	. . . . 5 ⊢ (𝜑 → 𝑥 ∈ Fin)
122	50	a1i 9	. . . . 5 ⊢ (𝜑 → {𝑦} ∈ Fin)
123		unfidisj 6810	. . . . 5 ⊢ ((𝑥 ∈ Fin ∧ {𝑦} ∈ Fin ∧ (𝑥 ∩ {𝑦}) = ∅) → (𝑥 ∪ {𝑦}) ∈ Fin)
124	121, 122, 119, 123	syl3anc 1216	. . . 4 ⊢ (𝜑 → (𝑥 ∪ {𝑦}) ∈ Fin)
125	13	sselda 3097	. . . . 5 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑥 ∪ {𝑦})) → 𝑗 ∈ 𝐴)
126	26	anassrs 397	. . . . . 6 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝐴) ∧ 𝑘 ∈ 𝐵) → 𝐶 ∈ ℂ)
127	18, 126	fsumcl 11169	. . . . 5 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → Σ𝑘 ∈ 𝐵 𝐶 ∈ ℂ)
128	125, 127	syldan 280	. . . 4 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑥 ∪ {𝑦})) → Σ𝑘 ∈ 𝐵 𝐶 ∈ ℂ)
129	119, 120, 124, 128	fsumsplit 11176	. . 3 ⊢ (𝜑 → Σ𝑗 ∈ (𝑥 ∪ {𝑦})Σ𝑘 ∈ 𝐵 𝐶 = (Σ𝑗 ∈ 𝑥 Σ𝑘 ∈ 𝐵 𝐶 + Σ𝑗 ∈ {𝑦}Σ𝑘 ∈ 𝐵 𝐶))
130	129	adantr 274	. 2 ⊢ ((𝜑 ∧ 𝜓) → Σ𝑗 ∈ (𝑥 ∪ {𝑦})Σ𝑘 ∈ 𝐵 𝐶 = (Σ𝑗 ∈ 𝑥 Σ𝑘 ∈ 𝐵 𝐶 + Σ𝑗 ∈ {𝑦}Σ𝑘 ∈ 𝐵 𝐶))
131		eliun 3817	. . . . . . . . . 10 ⊢ (𝑧 ∈ ∪ 𝑗 ∈ 𝑥 ({𝑗} × 𝐵) ↔ ∃𝑗 ∈ 𝑥 𝑧 ∈ ({𝑗} × 𝐵))
132		xp1st 6063	. . . . . . . . . . . . . 14 ⊢ (𝑧 ∈ ({𝑗} × 𝐵) → (1st ‘𝑧) ∈ {𝑗})
133		elsni 3545	. . . . . . . . . . . . . 14 ⊢ ((1st ‘𝑧) ∈ {𝑗} → (1st ‘𝑧) = 𝑗)
134	132, 133	syl 14	. . . . . . . . . . . . 13 ⊢ (𝑧 ∈ ({𝑗} × 𝐵) → (1st ‘𝑧) = 𝑗)
135	134	adantl 275	. . . . . . . . . . . 12 ⊢ ((𝑗 ∈ 𝑥 ∧ 𝑧 ∈ ({𝑗} × 𝐵)) → (1st ‘𝑧) = 𝑗)
136		simpl 108	. . . . . . . . . . . 12 ⊢ ((𝑗 ∈ 𝑥 ∧ 𝑧 ∈ ({𝑗} × 𝐵)) → 𝑗 ∈ 𝑥)
137	135, 136	eqeltrd 2216	. . . . . . . . . . 11 ⊢ ((𝑗 ∈ 𝑥 ∧ 𝑧 ∈ ({𝑗} × 𝐵)) → (1st ‘𝑧) ∈ 𝑥)
138	137	rexlimiva 2544	. . . . . . . . . 10 ⊢ (∃𝑗 ∈ 𝑥 𝑧 ∈ ({𝑗} × 𝐵) → (1st ‘𝑧) ∈ 𝑥)
139	131, 138	sylbi 120	. . . . . . . . 9 ⊢ (𝑧 ∈ ∪ 𝑗 ∈ 𝑥 ({𝑗} × 𝐵) → (1st ‘𝑧) ∈ 𝑥)
140		xp1st 6063	. . . . . . . . 9 ⊢ (𝑧 ∈ ({𝑦} × ⦋𝑦 / 𝑗⦌𝐵) → (1st ‘𝑧) ∈ {𝑦})
141	139, 140	anim12i 336	. . . . . . . 8 ⊢ ((𝑧 ∈ ∪ 𝑗 ∈ 𝑥 ({𝑗} × 𝐵) ∧ 𝑧 ∈ ({𝑦} × ⦋𝑦 / 𝑗⦌𝐵)) → ((1st ‘𝑧) ∈ 𝑥 ∧ (1st ‘𝑧) ∈ {𝑦}))
142		elin 3259	. . . . . . . 8 ⊢ (𝑧 ∈ (∪ 𝑗 ∈ 𝑥 ({𝑗} × 𝐵) ∩ ({𝑦} × ⦋𝑦 / 𝑗⦌𝐵)) ↔ (𝑧 ∈ ∪ 𝑗 ∈ 𝑥 ({𝑗} × 𝐵) ∧ 𝑧 ∈ ({𝑦} × ⦋𝑦 / 𝑗⦌𝐵)))
143		elin 3259	. . . . . . . 8 ⊢ ((1st ‘𝑧) ∈ (𝑥 ∩ {𝑦}) ↔ ((1st ‘𝑧) ∈ 𝑥 ∧ (1st ‘𝑧) ∈ {𝑦}))
144	141, 142, 143	3imtr4i 200	. . . . . . 7 ⊢ (𝑧 ∈ (∪ 𝑗 ∈ 𝑥 ({𝑗} × 𝐵) ∩ ({𝑦} × ⦋𝑦 / 𝑗⦌𝐵)) → (1st ‘𝑧) ∈ (𝑥 ∩ {𝑦}))
145	119	eleq2d 2209	. . . . . . . 8 ⊢ (𝜑 → ((1st ‘𝑧) ∈ (𝑥 ∩ {𝑦}) ↔ (1st ‘𝑧) ∈ ∅))
146		noel 3367	. . . . . . . . 9 ⊢ ¬ (1st ‘𝑧) ∈ ∅
147	146	pm2.21i 635	. . . . . . . 8 ⊢ ((1st ‘𝑧) ∈ ∅ → 𝑧 ∈ ∅)
148	145, 147	syl6bi 162	. . . . . . 7 ⊢ (𝜑 → ((1st ‘𝑧) ∈ (𝑥 ∩ {𝑦}) → 𝑧 ∈ ∅))
149	144, 148	syl5 32	. . . . . 6 ⊢ (𝜑 → (𝑧 ∈ (∪ 𝑗 ∈ 𝑥 ({𝑗} × 𝐵) ∩ ({𝑦} × ⦋𝑦 / 𝑗⦌𝐵)) → 𝑧 ∈ ∅))
150	149	ssrdv 3103	. . . . 5 ⊢ (𝜑 → (∪ 𝑗 ∈ 𝑥 ({𝑗} × 𝐵) ∩ ({𝑦} × ⦋𝑦 / 𝑗⦌𝐵)) ⊆ ∅)
151		ss0 3403	. . . . 5 ⊢ ((∪ 𝑗 ∈ 𝑥 ({𝑗} × 𝐵) ∩ ({𝑦} × ⦋𝑦 / 𝑗⦌𝐵)) ⊆ ∅ → (∪ 𝑗 ∈ 𝑥 ({𝑗} × 𝐵) ∩ ({𝑦} × ⦋𝑦 / 𝑗⦌𝐵)) = ∅)
152	150, 151	syl 14	. . . 4 ⊢ (𝜑 → (∪ 𝑗 ∈ 𝑥 ({𝑗} × 𝐵) ∩ ({𝑦} × ⦋𝑦 / 𝑗⦌𝐵)) = ∅)
153		iunxun 3892	. . . . . 6 ⊢ ∪ 𝑗 ∈ (𝑥 ∪ {𝑦})({𝑗} × 𝐵) = (∪ 𝑗 ∈ 𝑥 ({𝑗} × 𝐵) ∪ ∪ 𝑗 ∈ {𝑦} ({𝑗} × 𝐵))
154		nfcv 2281	. . . . . . . . 9 ⊢ Ⅎ𝑚({𝑗} × 𝐵)
155		nfcv 2281	. . . . . . . . . 10 ⊢ Ⅎ𝑗{𝑚}
156	155, 5	nfxp 4566	. . . . . . . . 9 ⊢ Ⅎ𝑗({𝑚} × ⦋𝑚 / 𝑗⦌𝐵)
157		sneq 3538	. . . . . . . . . 10 ⊢ (𝑗 = 𝑚 → {𝑗} = {𝑚})
158	157, 8	xpeq12d 4564	. . . . . . . . 9 ⊢ (𝑗 = 𝑚 → ({𝑗} × 𝐵) = ({𝑚} × ⦋𝑚 / 𝑗⦌𝐵))
159	154, 156, 158	cbviun 3850	. . . . . . . 8 ⊢ ∪ 𝑗 ∈ {𝑦} ({𝑗} × 𝐵) = ∪ 𝑚 ∈ {𝑦} ({𝑚} × ⦋𝑚 / 𝑗⦌𝐵)
160		sneq 3538	. . . . . . . . . 10 ⊢ (𝑚 = 𝑦 → {𝑚} = {𝑦})
161	160, 38	xpeq12d 4564	. . . . . . . . 9 ⊢ (𝑚 = 𝑦 → ({𝑚} × ⦋𝑚 / 𝑗⦌𝐵) = ({𝑦} × ⦋𝑦 / 𝑗⦌𝐵))
162	15, 161	iunxsn 3889	. . . . . . . 8 ⊢ ∪ 𝑚 ∈ {𝑦} ({𝑚} × ⦋𝑚 / 𝑗⦌𝐵) = ({𝑦} × ⦋𝑦 / 𝑗⦌𝐵)
163	159, 162	eqtri 2160	. . . . . . 7 ⊢ ∪ 𝑗 ∈ {𝑦} ({𝑗} × 𝐵) = ({𝑦} × ⦋𝑦 / 𝑗⦌𝐵)
164	163	uneq2i 3227	. . . . . 6 ⊢ (∪ 𝑗 ∈ 𝑥 ({𝑗} × 𝐵) ∪ ∪ 𝑗 ∈ {𝑦} ({𝑗} × 𝐵)) = (∪ 𝑗 ∈ 𝑥 ({𝑗} × 𝐵) ∪ ({𝑦} × ⦋𝑦 / 𝑗⦌𝐵))
165	153, 164	eqtri 2160	. . . . 5 ⊢ ∪ 𝑗 ∈ (𝑥 ∪ {𝑦})({𝑗} × 𝐵) = (∪ 𝑗 ∈ 𝑥 ({𝑗} × 𝐵) ∪ ({𝑦} × ⦋𝑦 / 𝑗⦌𝐵))
166	165	a1i 9	. . . 4 ⊢ (𝜑 → ∪ 𝑗 ∈ (𝑥 ∪ {𝑦})({𝑗} × 𝐵) = (∪ 𝑗 ∈ 𝑥 ({𝑗} × 𝐵) ∪ ({𝑦} × ⦋𝑦 / 𝑗⦌𝐵)))
167		snfig 6708	. . . . . . . 8 ⊢ (𝑗 ∈ V → {𝑗} ∈ Fin)
168	167	elv 2690	. . . . . . 7 ⊢ {𝑗} ∈ Fin
169	125, 18	syldan 280	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑥 ∪ {𝑦})) → 𝐵 ∈ Fin)
170		xpfi 6818	. . . . . . 7 ⊢ (({𝑗} ∈ Fin ∧ 𝐵 ∈ Fin) → ({𝑗} × 𝐵) ∈ Fin)
171	168, 169, 170	sylancr 410	. . . . . 6 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑥 ∪ {𝑦})) → ({𝑗} × 𝐵) ∈ Fin)
172	171	ralrimiva 2505	. . . . 5 ⊢ (𝜑 → ∀𝑗 ∈ (𝑥 ∪ {𝑦})({𝑗} × 𝐵) ∈ Fin)
173		disjsnxp 6134	. . . . . 6 ⊢ Disj 𝑗 ∈ (𝑥 ∪ {𝑦})({𝑗} × 𝐵)
174	173	a1i 9	. . . . 5 ⊢ (𝜑 → Disj 𝑗 ∈ (𝑥 ∪ {𝑦})({𝑗} × 𝐵))
175		iunfidisj 6834	. . . . 5 ⊢ (((𝑥 ∪ {𝑦}) ∈ Fin ∧ ∀𝑗 ∈ (𝑥 ∪ {𝑦})({𝑗} × 𝐵) ∈ Fin ∧ Disj 𝑗 ∈ (𝑥 ∪ {𝑦})({𝑗} × 𝐵)) → ∪ 𝑗 ∈ (𝑥 ∪ {𝑦})({𝑗} × 𝐵) ∈ Fin)
176	124, 172, 174, 175	syl3anc 1216	. . . 4 ⊢ (𝜑 → ∪ 𝑗 ∈ (𝑥 ∪ {𝑦})({𝑗} × 𝐵) ∈ Fin)
177		eliun 3817	. . . . . 6 ⊢ (𝑧 ∈ ∪ 𝑗 ∈ (𝑥 ∪ {𝑦})({𝑗} × 𝐵) ↔ ∃𝑗 ∈ (𝑥 ∪ {𝑦})𝑧 ∈ ({𝑗} × 𝐵))
178		elxp 4556	. . . . . . . 8 ⊢ (𝑧 ∈ ({𝑗} × 𝐵) ↔ ∃𝑚∃𝑘(𝑧 = ⟨𝑚, 𝑘⟩ ∧ (𝑚 ∈ {𝑗} ∧ 𝑘 ∈ 𝐵)))
179		simprl 520	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ (𝑥 ∪ {𝑦})) ∧ (𝑧 = ⟨𝑚, 𝑘⟩ ∧ (𝑚 ∈ {𝑗} ∧ 𝑘 ∈ 𝐵))) → 𝑧 = ⟨𝑚, 𝑘⟩)
180		simprrl 528	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ (𝑥 ∪ {𝑦})) ∧ (𝑧 = ⟨𝑚, 𝑘⟩ ∧ (𝑚 ∈ {𝑗} ∧ 𝑘 ∈ 𝐵))) → 𝑚 ∈ {𝑗})
181		elsni 3545	. . . . . . . . . . . . . . 15 ⊢ (𝑚 ∈ {𝑗} → 𝑚 = 𝑗)
182	180, 181	syl 14	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ (𝑥 ∪ {𝑦})) ∧ (𝑧 = ⟨𝑚, 𝑘⟩ ∧ (𝑚 ∈ {𝑗} ∧ 𝑘 ∈ 𝐵))) → 𝑚 = 𝑗)
183	182	opeq1d 3711	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ (𝑥 ∪ {𝑦})) ∧ (𝑧 = ⟨𝑚, 𝑘⟩ ∧ (𝑚 ∈ {𝑗} ∧ 𝑘 ∈ 𝐵))) → ⟨𝑚, 𝑘⟩ = ⟨𝑗, 𝑘⟩)
184	179, 183	eqtrd 2172	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑗 ∈ (𝑥 ∪ {𝑦})) ∧ (𝑧 = ⟨𝑚, 𝑘⟩ ∧ (𝑚 ∈ {𝑗} ∧ 𝑘 ∈ 𝐵))) → 𝑧 = ⟨𝑗, 𝑘⟩)
185	184, 93	syl 14	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑗 ∈ (𝑥 ∪ {𝑦})) ∧ (𝑧 = ⟨𝑚, 𝑘⟩ ∧ (𝑚 ∈ {𝑗} ∧ 𝑘 ∈ 𝐵))) → 𝐷 = 𝐶)
186		simpll 518	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑗 ∈ (𝑥 ∪ {𝑦})) ∧ (𝑧 = ⟨𝑚, 𝑘⟩ ∧ (𝑚 ∈ {𝑗} ∧ 𝑘 ∈ 𝐵))) → 𝜑)
187	125	adantr 274	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑗 ∈ (𝑥 ∪ {𝑦})) ∧ (𝑧 = ⟨𝑚, 𝑘⟩ ∧ (𝑚 ∈ {𝑗} ∧ 𝑘 ∈ 𝐵))) → 𝑗 ∈ 𝐴)
188		simprrr 529	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑗 ∈ (𝑥 ∪ {𝑦})) ∧ (𝑧 = ⟨𝑚, 𝑘⟩ ∧ (𝑚 ∈ {𝑗} ∧ 𝑘 ∈ 𝐵))) → 𝑘 ∈ 𝐵)
189	186, 187, 188, 26	syl12anc 1214	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑗 ∈ (𝑥 ∪ {𝑦})) ∧ (𝑧 = ⟨𝑚, 𝑘⟩ ∧ (𝑚 ∈ {𝑗} ∧ 𝑘 ∈ 𝐵))) → 𝐶 ∈ ℂ)
190	185, 189	eqeltrd 2216	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑗 ∈ (𝑥 ∪ {𝑦})) ∧ (𝑧 = ⟨𝑚, 𝑘⟩ ∧ (𝑚 ∈ {𝑗} ∧ 𝑘 ∈ 𝐵))) → 𝐷 ∈ ℂ)
191	190	ex 114	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑥 ∪ {𝑦})) → ((𝑧 = ⟨𝑚, 𝑘⟩ ∧ (𝑚 ∈ {𝑗} ∧ 𝑘 ∈ 𝐵)) → 𝐷 ∈ ℂ))
192	191	exlimdvv 1869	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑥 ∪ {𝑦})) → (∃𝑚∃𝑘(𝑧 = ⟨𝑚, 𝑘⟩ ∧ (𝑚 ∈ {𝑗} ∧ 𝑘 ∈ 𝐵)) → 𝐷 ∈ ℂ))
193	178, 192	syl5bi 151	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑥 ∪ {𝑦})) → (𝑧 ∈ ({𝑗} × 𝐵) → 𝐷 ∈ ℂ))
194	193	rexlimdva 2549	. . . . . 6 ⊢ (𝜑 → (∃𝑗 ∈ (𝑥 ∪ {𝑦})𝑧 ∈ ({𝑗} × 𝐵) → 𝐷 ∈ ℂ))
195	177, 194	syl5bi 151	. . . . 5 ⊢ (𝜑 → (𝑧 ∈ ∪ 𝑗 ∈ (𝑥 ∪ {𝑦})({𝑗} × 𝐵) → 𝐷 ∈ ℂ))
196	195	imp 123	. . . 4 ⊢ ((𝜑 ∧ 𝑧 ∈ ∪ 𝑗 ∈ (𝑥 ∪ {𝑦})({𝑗} × 𝐵)) → 𝐷 ∈ ℂ)
197	152, 166, 176, 196	fsumsplit 11176	. . 3 ⊢ (𝜑 → Σ𝑧 ∈ ∪ 𝑗 ∈ (𝑥 ∪ {𝑦})({𝑗} × 𝐵)𝐷 = (Σ𝑧 ∈ ∪ 𝑗 ∈ 𝑥 ({𝑗} × 𝐵)𝐷 + Σ𝑧 ∈ ({𝑦} × ⦋𝑦 / 𝑗⦌𝐵)𝐷))
198	197	adantr 274	. 2 ⊢ ((𝜑 ∧ 𝜓) → Σ𝑧 ∈ ∪ 𝑗 ∈ (𝑥 ∪ {𝑦})({𝑗} × 𝐵)𝐷 = (Σ𝑧 ∈ ∪ 𝑗 ∈ 𝑥 ({𝑗} × 𝐵)𝐷 + Σ𝑧 ∈ ({𝑦} × ⦋𝑦 / 𝑗⦌𝐵)𝐷))
199	116, 130, 198	3eqtr4d 2182	1 ⊢ ((𝜑 ∧ 𝜓) → Σ𝑗 ∈ (𝑥 ∪ {𝑦})Σ𝑘 ∈ 𝐵 𝐶 = Σ𝑧 ∈ ∪ 𝑗 ∈ (𝑥 ∪ {𝑦})({𝑗} × 𝐵)𝐷)

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 103   ↔ wb 104   = wceq 1331  ∃wex 1468   ∈ wcel 1480  ∀wral 2416  ∃wrex 2417  Vcvv 2686  ⦋csb 3003   ∪ cun 3069   ∩ cin 3070   ⊆ wss 3071  ∅c0 3363  {csn 3527  ⟨cop 3530  ∪ ciun 3813  Disj wdisj 3906   × cxp 4537   ↾ cres 4541  –1-1-onto→wf1o 5122  ‘cfv 5123  (class class class)co 5774  1^st c1st 6036  2^nd c2nd 6037  Fincfn 6634  ℂcc 7618   + caddc 7623  Σcsu 11122

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 603  ax-in2 604  ax-io 698  ax-5 1423  ax-7 1424  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-10 1483  ax-11 1484  ax-i12 1485  ax-bndl 1486  ax-4 1487  ax-13 1491  ax-14 1492  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2121  ax-coll 4043  ax-sep 4046  ax-nul 4054  ax-pow 4098  ax-pr 4131  ax-un 4355  ax-setind 4452  ax-iinf 4502  ax-cnex 7711  ax-resscn 7712  ax-1cn 7713  ax-1re 7714  ax-icn 7715  ax-addcl 7716  ax-addrcl 7717  ax-mulcl 7718  ax-mulrcl 7719  ax-addcom 7720  ax-mulcom 7721  ax-addass 7722  ax-mulass 7723  ax-distr 7724  ax-i2m1 7725  ax-0lt1 7726  ax-1rid 7727  ax-0id 7728  ax-rnegex 7729  ax-precex 7730  ax-cnre 7731  ax-pre-ltirr 7732  ax-pre-ltwlin 7733  ax-pre-lttrn 7734  ax-pre-apti 7735  ax-pre-ltadd 7736  ax-pre-mulgt0 7737  ax-pre-mulext 7738  ax-arch 7739  ax-caucvg 7740

This theorem depends on definitions:  df-bi 116  df-dc 820  df-3or 963  df-3an 964  df-tru 1334  df-fal 1337  df-nf 1437  df-sb 1736  df-eu 2002  df-mo 2003  df-clab 2126  df-cleq 2132  df-clel 2135  df-nfc 2270  df-ne 2309  df-nel 2404  df-ral 2421  df-rex 2422  df-reu 2423  df-rmo 2424  df-rab 2425  df-v 2688  df-sbc 2910  df-csb 3004  df-dif 3073  df-un 3075  df-in 3077  df-ss 3084  df-nul 3364  df-if 3475  df-pw 3512  df-sn 3533  df-pr 3534  df-op 3536  df-uni 3737  df-int 3772  df-iun 3815  df-disj 3907  df-br 3930  df-opab 3990  df-mpt 3991  df-tr 4027  df-id 4215  df-po 4218  df-iso 4219  df-iord 4288  df-on 4290  df-ilim 4291  df-suc 4293  df-iom 4505  df-xp 4545  df-rel 4546  df-cnv 4547  df-co 4548  df-dm 4549  df-rn 4550  df-res 4551  df-ima 4552  df-iota 5088  df-fun 5125  df-fn 5126  df-f 5127  df-f1 5128  df-fo 5129  df-f1o 5130  df-fv 5131  df-isom 5132  df-riota 5730  df-ov 5777  df-oprab 5778  df-mpo 5779  df-1st 6038  df-2nd 6039  df-recs 6202  df-irdg 6267  df-frec 6288  df-1o 6313  df-oadd 6317  df-er 6429  df-en 6635  df-dom 6636  df-fin 6637  df-pnf 7802  df-mnf 7803  df-xr 7804  df-ltxr 7805  df-le 7806  df-sub 7935  df-neg 7936  df-reap 8337  df-ap 8344  df-div 8433  df-inn 8721  df-2 8779  df-3 8780  df-4 8781  df-n0 8978  df-z 9055  df-uz 9327  df-q 9412  df-rp 9442  df-fz 9791  df-fzo 9920  df-seqfrec 10219  df-exp 10293  df-ihash 10522  df-cj 10614  df-re 10615  df-im 10616  df-rsqrt 10770  df-abs 10771  df-clim 11048  df-sumdc 11123

This theorem is referenced by:  fsum2d  11204