Theorem fsum2dlem 15722

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

Hypotheses

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

Assertion

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

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

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

Proof of Theorem fsum2dlem

Dummy variable 𝑚 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		simpr 484	. . . 4 ⊢ ((𝜑 ∧ 𝜓) → 𝜓)
2		fsum2d.7	. . . 4 ⊢ (𝜓 ↔ Σ𝑗 ∈ 𝑥 Σ𝑘 ∈ 𝐵 𝐶 = Σ𝑧 ∈ ∪ 𝑗 ∈ 𝑥 ({𝑗} × 𝐵)𝐷)
3	1, 2	sylib 217	. . 3 ⊢ ((𝜑 ∧ 𝜓) → Σ𝑗 ∈ 𝑥 Σ𝑘 ∈ 𝐵 𝐶 = Σ𝑧 ∈ ∪ 𝑗 ∈ 𝑥 ({𝑗} × 𝐵)𝐷)
4		nfcv 2897	. . . . . 6 ⊢ Ⅎ𝑚Σ𝑘 ∈ 𝐵 𝐶
5		nfcsb1v 3913	. . . . . . 7 ⊢ Ⅎ𝑗⦋𝑚 / 𝑗⦌𝐵
6		nfcsb1v 3913	. . . . . . 7 ⊢ Ⅎ𝑗⦋𝑚 / 𝑗⦌𝐶
7	5, 6	nfsum 15643	. . . . . 6 ⊢ Ⅎ𝑗Σ𝑘 ∈ ⦋ 𝑚 / 𝑗⦌𝐵⦋𝑚 / 𝑗⦌𝐶
8		csbeq1a 3902	. . . . . . 7 ⊢ (𝑗 = 𝑚 → 𝐵 = ⦋𝑚 / 𝑗⦌𝐵)
9		csbeq1a 3902	. . . . . . . 8 ⊢ (𝑗 = 𝑚 → 𝐶 = ⦋𝑚 / 𝑗⦌𝐶)
10	9	adantr 480	. . . . . . 7 ⊢ ((𝑗 = 𝑚 ∧ 𝑘 ∈ 𝐵) → 𝐶 = ⦋𝑚 / 𝑗⦌𝐶)
11	8, 10	sumeq12dv 15658	. . . . . 6 ⊢ (𝑗 = 𝑚 → Σ𝑘 ∈ 𝐵 𝐶 = Σ𝑘 ∈ ⦋ 𝑚 / 𝑗⦌𝐵⦋𝑚 / 𝑗⦌𝐶)
12	4, 7, 11	cbvsumi 15649	. . . . 5 ⊢ Σ𝑗 ∈ {𝑦}Σ𝑘 ∈ 𝐵 𝐶 = Σ𝑚 ∈ {𝑦}Σ𝑘 ∈ ⦋ 𝑚 / 𝑗⦌𝐵⦋𝑚 / 𝑗⦌𝐶
13		fsum2d.6	. . . . . . . . 9 ⊢ (𝜑 → (𝑥 ∪ {𝑦}) ⊆ 𝐴)
14	13	unssbd 4183	. . . . . . . 8 ⊢ (𝜑 → {𝑦} ⊆ 𝐴)
15		vex 3472	. . . . . . . . 9 ⊢ 𝑦 ∈ V
16	15	snss 4784	. . . . . . . 8 ⊢ (𝑦 ∈ 𝐴 ↔ {𝑦} ⊆ 𝐴)
17	14, 16	sylibr 233	. . . . . . 7 ⊢ (𝜑 → 𝑦 ∈ 𝐴)
18		fsum2d.3	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → 𝐵 ∈ Fin)
19	18	ralrimiva 3140	. . . . . . . . 9 ⊢ (𝜑 → ∀𝑗 ∈ 𝐴 𝐵 ∈ Fin)
20		nfcsb1v 3913	. . . . . . . . . . 11 ⊢ Ⅎ𝑗⦋𝑦 / 𝑗⦌𝐵
21	20	nfel1 2913	. . . . . . . . . 10 ⊢ Ⅎ𝑗⦋𝑦 / 𝑗⦌𝐵 ∈ Fin
22		csbeq1a 3902	. . . . . . . . . . 11 ⊢ (𝑗 = 𝑦 → 𝐵 = ⦋𝑦 / 𝑗⦌𝐵)
23	22	eleq1d 2812	. . . . . . . . . 10 ⊢ (𝑗 = 𝑦 → (𝐵 ∈ Fin ↔ ⦋𝑦 / 𝑗⦌𝐵 ∈ Fin))
24	21, 23	rspc 3594	. . . . . . . . 9 ⊢ (𝑦 ∈ 𝐴 → (∀𝑗 ∈ 𝐴 𝐵 ∈ Fin → ⦋𝑦 / 𝑗⦌𝐵 ∈ Fin))
25	17, 19, 24	sylc 65	. . . . . . . 8 ⊢ (𝜑 → ⦋𝑦 / 𝑗⦌𝐵 ∈ Fin)
26		fsum2d.4	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵)) → 𝐶 ∈ ℂ)
27	26	ralrimivva 3194	. . . . . . . . . 10 ⊢ (𝜑 → ∀𝑗 ∈ 𝐴 ∀𝑘 ∈ 𝐵 𝐶 ∈ ℂ)
28		nfcsb1v 3913	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑗⦋𝑦 / 𝑗⦌𝐶
29	28	nfel1 2913	. . . . . . . . . . . 12 ⊢ Ⅎ𝑗⦋𝑦 / 𝑗⦌𝐶 ∈ ℂ
30	20, 29	nfralw 3302	. . . . . . . . . . 11 ⊢ Ⅎ𝑗∀𝑘 ∈ ⦋ 𝑦 / 𝑗⦌𝐵⦋𝑦 / 𝑗⦌𝐶 ∈ ℂ
31		csbeq1a 3902	. . . . . . . . . . . . 13 ⊢ (𝑗 = 𝑦 → 𝐶 = ⦋𝑦 / 𝑗⦌𝐶)
32	31	eleq1d 2812	. . . . . . . . . . . 12 ⊢ (𝑗 = 𝑦 → (𝐶 ∈ ℂ ↔ ⦋𝑦 / 𝑗⦌𝐶 ∈ ℂ))
33	22, 32	raleqbidv 3336	. . . . . . . . . . 11 ⊢ (𝑗 = 𝑦 → (∀𝑘 ∈ 𝐵 𝐶 ∈ ℂ ↔ ∀𝑘 ∈ ⦋ 𝑦 / 𝑗⦌𝐵⦋𝑦 / 𝑗⦌𝐶 ∈ ℂ))
34	30, 33	rspc 3594	. . . . . . . . . 10 ⊢ (𝑦 ∈ 𝐴 → (∀𝑗 ∈ 𝐴 ∀𝑘 ∈ 𝐵 𝐶 ∈ ℂ → ∀𝑘 ∈ ⦋ 𝑦 / 𝑗⦌𝐵⦋𝑦 / 𝑗⦌𝐶 ∈ ℂ))
35	17, 27, 34	sylc 65	. . . . . . . . 9 ⊢ (𝜑 → ∀𝑘 ∈ ⦋ 𝑦 / 𝑗⦌𝐵⦋𝑦 / 𝑗⦌𝐶 ∈ ℂ)
36	35	r19.21bi 3242	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ ⦋𝑦 / 𝑗⦌𝐵) → ⦋𝑦 / 𝑗⦌𝐶 ∈ ℂ)
37	25, 36	fsumcl 15685	. . . . . . 7 ⊢ (𝜑 → Σ𝑘 ∈ ⦋ 𝑦 / 𝑗⦌𝐵⦋𝑦 / 𝑗⦌𝐶 ∈ ℂ)
38		csbeq1 3891	. . . . . . . . 9 ⊢ (𝑚 = 𝑦 → ⦋𝑚 / 𝑗⦌𝐵 = ⦋𝑦 / 𝑗⦌𝐵)
39		csbeq1 3891	. . . . . . . . . 10 ⊢ (𝑚 = 𝑦 → ⦋𝑚 / 𝑗⦌𝐶 = ⦋𝑦 / 𝑗⦌𝐶)
40	39	adantr 480	. . . . . . . . 9 ⊢ ((𝑚 = 𝑦 ∧ 𝑘 ∈ ⦋𝑚 / 𝑗⦌𝐵) → ⦋𝑚 / 𝑗⦌𝐶 = ⦋𝑦 / 𝑗⦌𝐶)
41	38, 40	sumeq12dv 15658	. . . . . . . 8 ⊢ (𝑚 = 𝑦 → Σ𝑘 ∈ ⦋ 𝑚 / 𝑗⦌𝐵⦋𝑚 / 𝑗⦌𝐶 = Σ𝑘 ∈ ⦋ 𝑦 / 𝑗⦌𝐵⦋𝑦 / 𝑗⦌𝐶)
42	41	sumsn 15698	. . . . . . 7 ⊢ ((𝑦 ∈ 𝐴 ∧ Σ𝑘 ∈ ⦋ 𝑦 / 𝑗⦌𝐵⦋𝑦 / 𝑗⦌𝐶 ∈ ℂ) → Σ𝑚 ∈ {𝑦}Σ𝑘 ∈ ⦋ 𝑚 / 𝑗⦌𝐵⦋𝑚 / 𝑗⦌𝐶 = Σ𝑘 ∈ ⦋ 𝑦 / 𝑗⦌𝐵⦋𝑦 / 𝑗⦌𝐶)
43	17, 37, 42	syl2anc 583	. . . . . 6 ⊢ (𝜑 → Σ𝑚 ∈ {𝑦}Σ𝑘 ∈ ⦋ 𝑚 / 𝑗⦌𝐵⦋𝑚 / 𝑗⦌𝐶 = Σ𝑘 ∈ ⦋ 𝑦 / 𝑗⦌𝐵⦋𝑦 / 𝑗⦌𝐶)
44		nfcv 2897	. . . . . . . 8 ⊢ Ⅎ𝑚⦋𝑦 / 𝑗⦌𝐶
45		nfcsb1v 3913	. . . . . . . 8 ⊢ Ⅎ𝑘⦋𝑚 / 𝑘⦌⦋𝑦 / 𝑗⦌𝐶
46		csbeq1a 3902	. . . . . . . 8 ⊢ (𝑘 = 𝑚 → ⦋𝑦 / 𝑗⦌𝐶 = ⦋𝑚 / 𝑘⦌⦋𝑦 / 𝑗⦌𝐶)
47	44, 45, 46	cbvsumi 15649	. . . . . . 7 ⊢ Σ𝑘 ∈ ⦋ 𝑦 / 𝑗⦌𝐵⦋𝑦 / 𝑗⦌𝐶 = Σ𝑚 ∈ ⦋ 𝑦 / 𝑗⦌𝐵⦋𝑚 / 𝑘⦌⦋𝑦 / 𝑗⦌𝐶
48		csbeq1 3891	. . . . . . . . 9 ⊢ (𝑚 = (2nd ‘𝑧) → ⦋𝑚 / 𝑘⦌⦋𝑦 / 𝑗⦌𝐶 = ⦋(2nd ‘𝑧) / 𝑘⦌⦋𝑦 / 𝑗⦌𝐶)
49		snfi 9046	. . . . . . . . . 10 ⊢ {𝑦} ∈ Fin
50		xpfi 9319	. . . . . . . . . 10 ⊢ (({𝑦} ∈ Fin ∧ ⦋𝑦 / 𝑗⦌𝐵 ∈ Fin) → ({𝑦} × ⦋𝑦 / 𝑗⦌𝐵) ∈ Fin)
51	49, 25, 50	sylancr 586	. . . . . . . . 9 ⊢ (𝜑 → ({𝑦} × ⦋𝑦 / 𝑗⦌𝐵) ∈ Fin)
52		2ndconst 8087	. . . . . . . . . 10 ⊢ (𝑦 ∈ 𝐴 → (2nd ↾ ({𝑦} × ⦋𝑦 / 𝑗⦌𝐵)):({𝑦} × ⦋𝑦 / 𝑗⦌𝐵)–1-1-onto→⦋𝑦 / 𝑗⦌𝐵)
53	17, 52	syl 17	. . . . . . . . 9 ⊢ (𝜑 → (2nd ↾ ({𝑦} × ⦋𝑦 / 𝑗⦌𝐵)):({𝑦} × ⦋𝑦 / 𝑗⦌𝐵)–1-1-onto→⦋𝑦 / 𝑗⦌𝐵)
54		fvres 6904	. . . . . . . . . 10 ⊢ (𝑧 ∈ ({𝑦} × ⦋𝑦 / 𝑗⦌𝐵) → ((2nd ↾ ({𝑦} × ⦋𝑦 / 𝑗⦌𝐵))‘𝑧) = (2nd ‘𝑧))
55	54	adantl 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑧 ∈ ({𝑦} × ⦋𝑦 / 𝑗⦌𝐵)) → ((2nd ↾ ({𝑦} × ⦋𝑦 / 𝑗⦌𝐵))‘𝑧) = (2nd ‘𝑧))
56	45	nfel1 2913	. . . . . . . . . . 11 ⊢ Ⅎ𝑘⦋𝑚 / 𝑘⦌⦋𝑦 / 𝑗⦌𝐶 ∈ ℂ
57	46	eleq1d 2812	. . . . . . . . . . 11 ⊢ (𝑘 = 𝑚 → (⦋𝑦 / 𝑗⦌𝐶 ∈ ℂ ↔ ⦋𝑚 / 𝑘⦌⦋𝑦 / 𝑗⦌𝐶 ∈ ℂ))
58	56, 57	rspc 3594	. . . . . . . . . 10 ⊢ (𝑚 ∈ ⦋𝑦 / 𝑗⦌𝐵 → (∀𝑘 ∈ ⦋ 𝑦 / 𝑗⦌𝐵⦋𝑦 / 𝑗⦌𝐶 ∈ ℂ → ⦋𝑚 / 𝑘⦌⦋𝑦 / 𝑗⦌𝐶 ∈ ℂ))
59	35, 58	mpan9 506	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑚 ∈ ⦋𝑦 / 𝑗⦌𝐵) → ⦋𝑚 / 𝑘⦌⦋𝑦 / 𝑗⦌𝐶 ∈ ℂ)
60	48, 51, 53, 55, 59	fsumf1o 15675	. . . . . . . 8 ⊢ (𝜑 → Σ𝑚 ∈ ⦋ 𝑦 / 𝑗⦌𝐵⦋𝑚 / 𝑘⦌⦋𝑦 / 𝑗⦌𝐶 = Σ𝑧 ∈ ({𝑦} × ⦋𝑦 / 𝑗⦌𝐵)⦋(2nd ‘𝑧) / 𝑘⦌⦋𝑦 / 𝑗⦌𝐶)
61		elxp 5692	. . . . . . . . . . . 12 ⊢ (𝑧 ∈ ({𝑦} × ⦋𝑦 / 𝑗⦌𝐵) ↔ ∃𝑚∃𝑘(𝑧 = ⟨𝑚, 𝑘⟩ ∧ (𝑚 ∈ {𝑦} ∧ 𝑘 ∈ ⦋𝑦 / 𝑗⦌𝐵)))
62		nfv 1909	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑗 𝑧 = ⟨𝑚, 𝑘⟩
63		nfv 1909	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑗 𝑚 ∈ {𝑦}
64	20	nfcri 2884	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑗 𝑘 ∈ ⦋𝑦 / 𝑗⦌𝐵
65	63, 64	nfan 1894	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑗(𝑚 ∈ {𝑦} ∧ 𝑘 ∈ ⦋𝑦 / 𝑗⦌𝐵)
66	62, 65	nfan 1894	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑗(𝑧 = ⟨𝑚, 𝑘⟩ ∧ (𝑚 ∈ {𝑦} ∧ 𝑘 ∈ ⦋𝑦 / 𝑗⦌𝐵))
67	66	nfex 2311	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑗∃𝑘(𝑧 = ⟨𝑚, 𝑘⟩ ∧ (𝑚 ∈ {𝑦} ∧ 𝑘 ∈ ⦋𝑦 / 𝑗⦌𝐵))
68		nfv 1909	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑚∃𝑘(𝑧 = ⟨𝑗, 𝑘⟩ ∧ (𝑗 = 𝑦 ∧ 𝑘 ∈ 𝐵))
69		opeq1 4868	. . . . . . . . . . . . . . . 16 ⊢ (𝑚 = 𝑗 → ⟨𝑚, 𝑘⟩ = ⟨𝑗, 𝑘⟩)
70	69	eqeq2d 2737	. . . . . . . . . . . . . . 15 ⊢ (𝑚 = 𝑗 → (𝑧 = ⟨𝑚, 𝑘⟩ ↔ 𝑧 = ⟨𝑗, 𝑘⟩))
71		velsn 4639	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑚 ∈ {𝑦} ↔ 𝑚 = 𝑦)
72	71	anbi1i 623	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑚 ∈ {𝑦} ∧ 𝑘 ∈ ⦋𝑦 / 𝑗⦌𝐵) ↔ (𝑚 = 𝑦 ∧ 𝑘 ∈ ⦋𝑦 / 𝑗⦌𝐵))
73		eqtr2 2750	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑚 = 𝑗 ∧ 𝑚 = 𝑦) → 𝑗 = 𝑦)
74	73, 22	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑚 = 𝑗 ∧ 𝑚 = 𝑦) → 𝐵 = ⦋𝑦 / 𝑗⦌𝐵)
75	74	eleq2d 2813	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑚 = 𝑗 ∧ 𝑚 = 𝑦) → (𝑘 ∈ 𝐵 ↔ 𝑘 ∈ ⦋𝑦 / 𝑗⦌𝐵))
76	75	pm5.32da 578	. . . . . . . . . . . . . . . . 17 ⊢ (𝑚 = 𝑗 → ((𝑚 = 𝑦 ∧ 𝑘 ∈ 𝐵) ↔ (𝑚 = 𝑦 ∧ 𝑘 ∈ ⦋𝑦 / 𝑗⦌𝐵)))
77	72, 76	bitr4id 290	. . . . . . . . . . . . . . . 16 ⊢ (𝑚 = 𝑗 → ((𝑚 ∈ {𝑦} ∧ 𝑘 ∈ ⦋𝑦 / 𝑗⦌𝐵) ↔ (𝑚 = 𝑦 ∧ 𝑘 ∈ 𝐵)))
78		equequ1 2020	. . . . . . . . . . . . . . . . 17 ⊢ (𝑚 = 𝑗 → (𝑚 = 𝑦 ↔ 𝑗 = 𝑦))
79	78	anbi1d 629	. . . . . . . . . . . . . . . 16 ⊢ (𝑚 = 𝑗 → ((𝑚 = 𝑦 ∧ 𝑘 ∈ 𝐵) ↔ (𝑗 = 𝑦 ∧ 𝑘 ∈ 𝐵)))
80	77, 79	bitrd 279	. . . . . . . . . . . . . . 15 ⊢ (𝑚 = 𝑗 → ((𝑚 ∈ {𝑦} ∧ 𝑘 ∈ ⦋𝑦 / 𝑗⦌𝐵) ↔ (𝑗 = 𝑦 ∧ 𝑘 ∈ 𝐵)))
81	70, 80	anbi12d 630	. . . . . . . . . . . . . 14 ⊢ (𝑚 = 𝑗 → ((𝑧 = ⟨𝑚, 𝑘⟩ ∧ (𝑚 ∈ {𝑦} ∧ 𝑘 ∈ ⦋𝑦 / 𝑗⦌𝐵)) ↔ (𝑧 = ⟨𝑗, 𝑘⟩ ∧ (𝑗 = 𝑦 ∧ 𝑘 ∈ 𝐵))))
82	81	exbidv 1916	. . . . . . . . . . . . 13 ⊢ (𝑚 = 𝑗 → (∃𝑘(𝑧 = ⟨𝑚, 𝑘⟩ ∧ (𝑚 ∈ {𝑦} ∧ 𝑘 ∈ ⦋𝑦 / 𝑗⦌𝐵)) ↔ ∃𝑘(𝑧 = ⟨𝑗, 𝑘⟩ ∧ (𝑗 = 𝑦 ∧ 𝑘 ∈ 𝐵))))
83	67, 68, 82	cbvexv1 2332	. . . . . . . . . . . 12 ⊢ (∃𝑚∃𝑘(𝑧 = ⟨𝑚, 𝑘⟩ ∧ (𝑚 ∈ {𝑦} ∧ 𝑘 ∈ ⦋𝑦 / 𝑗⦌𝐵)) ↔ ∃𝑗∃𝑘(𝑧 = ⟨𝑗, 𝑘⟩ ∧ (𝑗 = 𝑦 ∧ 𝑘 ∈ 𝐵)))
84	61, 83	bitri 275	. . . . . . . . . . 11 ⊢ (𝑧 ∈ ({𝑦} × ⦋𝑦 / 𝑗⦌𝐵) ↔ ∃𝑗∃𝑘(𝑧 = ⟨𝑗, 𝑘⟩ ∧ (𝑗 = 𝑦 ∧ 𝑘 ∈ 𝐵)))
85		nfv 1909	. . . . . . . . . . . 12 ⊢ Ⅎ𝑗𝜑
86		nfcv 2897	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑗(2nd ‘𝑧)
87	86, 28	nfcsbw 3915	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑗⦋(2nd ‘𝑧) / 𝑘⦌⦋𝑦 / 𝑗⦌𝐶
88	87	nfeq2 2914	. . . . . . . . . . . 12 ⊢ Ⅎ𝑗 𝐷 = ⦋(2nd ‘𝑧) / 𝑘⦌⦋𝑦 / 𝑗⦌𝐶
89		nfv 1909	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑘𝜑
90		nfcsb1v 3913	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑘⦋(2nd ‘𝑧) / 𝑘⦌⦋𝑦 / 𝑗⦌𝐶
91	90	nfeq2 2914	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑘 𝐷 = ⦋(2nd ‘𝑧) / 𝑘⦌⦋𝑦 / 𝑗⦌𝐶
92		fsum2d.1	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 = ⟨𝑗, 𝑘⟩ → 𝐷 = 𝐶)
93	92	ad2antlr 724	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑧 = ⟨𝑗, 𝑘⟩) ∧ (𝑗 = 𝑦 ∧ 𝑘 ∈ 𝐵)) → 𝐷 = 𝐶)
94	31	ad2antrl 725	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑧 = ⟨𝑗, 𝑘⟩) ∧ (𝑗 = 𝑦 ∧ 𝑘 ∈ 𝐵)) → 𝐶 = ⦋𝑦 / 𝑗⦌𝐶)
95		fveq2 6885	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 = ⟨𝑗, 𝑘⟩ → (2nd ‘𝑧) = (2nd ‘⟨𝑗, 𝑘⟩))
96		vex 3472	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝑗 ∈ V
97		vex 3472	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝑘 ∈ V
98	96, 97	op2nd 7983	. . . . . . . . . . . . . . . . . 18 ⊢ (2nd ‘⟨𝑗, 𝑘⟩) = 𝑘
99	95, 98	eqtr2di 2783	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 = ⟨𝑗, 𝑘⟩ → 𝑘 = (2nd ‘𝑧))
100	99	ad2antlr 724	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑧 = ⟨𝑗, 𝑘⟩) ∧ (𝑗 = 𝑦 ∧ 𝑘 ∈ 𝐵)) → 𝑘 = (2nd ‘𝑧))
101		csbeq1a 3902	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 = (2nd ‘𝑧) → ⦋𝑦 / 𝑗⦌𝐶 = ⦋(2nd ‘𝑧) / 𝑘⦌⦋𝑦 / 𝑗⦌𝐶)
102	100, 101	syl 17	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑧 = ⟨𝑗, 𝑘⟩) ∧ (𝑗 = 𝑦 ∧ 𝑘 ∈ 𝐵)) → ⦋𝑦 / 𝑗⦌𝐶 = ⦋(2nd ‘𝑧) / 𝑘⦌⦋𝑦 / 𝑗⦌𝐶)
103	93, 94, 102	3eqtrd 2770	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑧 = ⟨𝑗, 𝑘⟩) ∧ (𝑗 = 𝑦 ∧ 𝑘 ∈ 𝐵)) → 𝐷 = ⦋(2nd ‘𝑧) / 𝑘⦌⦋𝑦 / 𝑗⦌𝐶)
104	103	expl 457	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑧 = ⟨𝑗, 𝑘⟩ ∧ (𝑗 = 𝑦 ∧ 𝑘 ∈ 𝐵)) → 𝐷 = ⦋(2nd ‘𝑧) / 𝑘⦌⦋𝑦 / 𝑗⦌𝐶))
105	89, 91, 104	exlimd 2203	. . . . . . . . . . . 12 ⊢ (𝜑 → (∃𝑘(𝑧 = ⟨𝑗, 𝑘⟩ ∧ (𝑗 = 𝑦 ∧ 𝑘 ∈ 𝐵)) → 𝐷 = ⦋(2nd ‘𝑧) / 𝑘⦌⦋𝑦 / 𝑗⦌𝐶))
106	85, 88, 105	exlimd 2203	. . . . . . . . . . 11 ⊢ (𝜑 → (∃𝑗∃𝑘(𝑧 = ⟨𝑗, 𝑘⟩ ∧ (𝑗 = 𝑦 ∧ 𝑘 ∈ 𝐵)) → 𝐷 = ⦋(2nd ‘𝑧) / 𝑘⦌⦋𝑦 / 𝑗⦌𝐶))
107	84, 106	biimtrid 241	. . . . . . . . . 10 ⊢ (𝜑 → (𝑧 ∈ ({𝑦} × ⦋𝑦 / 𝑗⦌𝐵) → 𝐷 = ⦋(2nd ‘𝑧) / 𝑘⦌⦋𝑦 / 𝑗⦌𝐶))
108	107	imp 406	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑧 ∈ ({𝑦} × ⦋𝑦 / 𝑗⦌𝐵)) → 𝐷 = ⦋(2nd ‘𝑧) / 𝑘⦌⦋𝑦 / 𝑗⦌𝐶)
109	108	sumeq2dv 15655	. . . . . . . 8 ⊢ (𝜑 → Σ𝑧 ∈ ({𝑦} × ⦋𝑦 / 𝑗⦌𝐵)𝐷 = Σ𝑧 ∈ ({𝑦} × ⦋𝑦 / 𝑗⦌𝐵)⦋(2nd ‘𝑧) / 𝑘⦌⦋𝑦 / 𝑗⦌𝐶)
110	60, 109	eqtr4d 2769	. . . . . . 7 ⊢ (𝜑 → Σ𝑚 ∈ ⦋ 𝑦 / 𝑗⦌𝐵⦋𝑚 / 𝑘⦌⦋𝑦 / 𝑗⦌𝐶 = Σ𝑧 ∈ ({𝑦} × ⦋𝑦 / 𝑗⦌𝐵)𝐷)
111	47, 110	eqtrid 2778	. . . . . 6 ⊢ (𝜑 → Σ𝑘 ∈ ⦋ 𝑦 / 𝑗⦌𝐵⦋𝑦 / 𝑗⦌𝐶 = Σ𝑧 ∈ ({𝑦} × ⦋𝑦 / 𝑗⦌𝐵)𝐷)
112	43, 111	eqtrd 2766	. . . . 5 ⊢ (𝜑 → Σ𝑚 ∈ {𝑦}Σ𝑘 ∈ ⦋ 𝑚 / 𝑗⦌𝐵⦋𝑚 / 𝑗⦌𝐶 = Σ𝑧 ∈ ({𝑦} × ⦋𝑦 / 𝑗⦌𝐵)𝐷)
113	12, 112	eqtrid 2778	. . . 4 ⊢ (𝜑 → Σ𝑗 ∈ {𝑦}Σ𝑘 ∈ 𝐵 𝐶 = Σ𝑧 ∈ ({𝑦} × ⦋𝑦 / 𝑗⦌𝐵)𝐷)
114	113	adantr 480	. . 3 ⊢ ((𝜑 ∧ 𝜓) → Σ𝑗 ∈ {𝑦}Σ𝑘 ∈ 𝐵 𝐶 = Σ𝑧 ∈ ({𝑦} × ⦋𝑦 / 𝑗⦌𝐵)𝐷)
115	3, 114	oveq12d 7423	. 2 ⊢ ((𝜑 ∧ 𝜓) → (Σ𝑗 ∈ 𝑥 Σ𝑘 ∈ 𝐵 𝐶 + Σ𝑗 ∈ {𝑦}Σ𝑘 ∈ 𝐵 𝐶) = (Σ𝑧 ∈ ∪ 𝑗 ∈ 𝑥 ({𝑗} × 𝐵)𝐷 + Σ𝑧 ∈ ({𝑦} × ⦋𝑦 / 𝑗⦌𝐵)𝐷))
116		fsum2d.5	. . . . 5 ⊢ (𝜑 → ¬ 𝑦 ∈ 𝑥)
117		disjsn 4710	. . . . 5 ⊢ ((𝑥 ∩ {𝑦}) = ∅ ↔ ¬ 𝑦 ∈ 𝑥)
118	116, 117	sylibr 233	. . . 4 ⊢ (𝜑 → (𝑥 ∩ {𝑦}) = ∅)
119		eqidd 2727	. . . 4 ⊢ (𝜑 → (𝑥 ∪ {𝑦}) = (𝑥 ∪ {𝑦}))
120		fsum2d.2	. . . . 5 ⊢ (𝜑 → 𝐴 ∈ Fin)
121	120, 13	ssfid 9269	. . . 4 ⊢ (𝜑 → (𝑥 ∪ {𝑦}) ∈ Fin)
122	13	sselda 3977	. . . . 5 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑥 ∪ {𝑦})) → 𝑗 ∈ 𝐴)
123	26	anassrs 467	. . . . . 6 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝐴) ∧ 𝑘 ∈ 𝐵) → 𝐶 ∈ ℂ)
124	18, 123	fsumcl 15685	. . . . 5 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → Σ𝑘 ∈ 𝐵 𝐶 ∈ ℂ)
125	122, 124	syldan 590	. . . 4 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑥 ∪ {𝑦})) → Σ𝑘 ∈ 𝐵 𝐶 ∈ ℂ)
126	118, 119, 121, 125	fsumsplit 15693	. . 3 ⊢ (𝜑 → Σ𝑗 ∈ (𝑥 ∪ {𝑦})Σ𝑘 ∈ 𝐵 𝐶 = (Σ𝑗 ∈ 𝑥 Σ𝑘 ∈ 𝐵 𝐶 + Σ𝑗 ∈ {𝑦}Σ𝑘 ∈ 𝐵 𝐶))
127	126	adantr 480	. 2 ⊢ ((𝜑 ∧ 𝜓) → Σ𝑗 ∈ (𝑥 ∪ {𝑦})Σ𝑘 ∈ 𝐵 𝐶 = (Σ𝑗 ∈ 𝑥 Σ𝑘 ∈ 𝐵 𝐶 + Σ𝑗 ∈ {𝑦}Σ𝑘 ∈ 𝐵 𝐶))
128		eliun 4994	. . . . . . . . . 10 ⊢ (𝑧 ∈ ∪ 𝑗 ∈ 𝑥 ({𝑗} × 𝐵) ↔ ∃𝑗 ∈ 𝑥 𝑧 ∈ ({𝑗} × 𝐵))
129		xp1st 8006	. . . . . . . . . . . . . 14 ⊢ (𝑧 ∈ ({𝑗} × 𝐵) → (1st ‘𝑧) ∈ {𝑗})
130		elsni 4640	. . . . . . . . . . . . . 14 ⊢ ((1st ‘𝑧) ∈ {𝑗} → (1st ‘𝑧) = 𝑗)
131	129, 130	syl 17	. . . . . . . . . . . . 13 ⊢ (𝑧 ∈ ({𝑗} × 𝐵) → (1st ‘𝑧) = 𝑗)
132	131	adantl 481	. . . . . . . . . . . 12 ⊢ ((𝑗 ∈ 𝑥 ∧ 𝑧 ∈ ({𝑗} × 𝐵)) → (1st ‘𝑧) = 𝑗)
133		simpl 482	. . . . . . . . . . . 12 ⊢ ((𝑗 ∈ 𝑥 ∧ 𝑧 ∈ ({𝑗} × 𝐵)) → 𝑗 ∈ 𝑥)
134	132, 133	eqeltrd 2827	. . . . . . . . . . 11 ⊢ ((𝑗 ∈ 𝑥 ∧ 𝑧 ∈ ({𝑗} × 𝐵)) → (1st ‘𝑧) ∈ 𝑥)
135	134	rexlimiva 3141	. . . . . . . . . 10 ⊢ (∃𝑗 ∈ 𝑥 𝑧 ∈ ({𝑗} × 𝐵) → (1st ‘𝑧) ∈ 𝑥)
136	128, 135	sylbi 216	. . . . . . . . 9 ⊢ (𝑧 ∈ ∪ 𝑗 ∈ 𝑥 ({𝑗} × 𝐵) → (1st ‘𝑧) ∈ 𝑥)
137		xp1st 8006	. . . . . . . . 9 ⊢ (𝑧 ∈ ({𝑦} × ⦋𝑦 / 𝑗⦌𝐵) → (1st ‘𝑧) ∈ {𝑦})
138	136, 137	anim12i 612	. . . . . . . 8 ⊢ ((𝑧 ∈ ∪ 𝑗 ∈ 𝑥 ({𝑗} × 𝐵) ∧ 𝑧 ∈ ({𝑦} × ⦋𝑦 / 𝑗⦌𝐵)) → ((1st ‘𝑧) ∈ 𝑥 ∧ (1st ‘𝑧) ∈ {𝑦}))
139		elin 3959	. . . . . . . 8 ⊢ (𝑧 ∈ (∪ 𝑗 ∈ 𝑥 ({𝑗} × 𝐵) ∩ ({𝑦} × ⦋𝑦 / 𝑗⦌𝐵)) ↔ (𝑧 ∈ ∪ 𝑗 ∈ 𝑥 ({𝑗} × 𝐵) ∧ 𝑧 ∈ ({𝑦} × ⦋𝑦 / 𝑗⦌𝐵)))
140		elin 3959	. . . . . . . 8 ⊢ ((1st ‘𝑧) ∈ (𝑥 ∩ {𝑦}) ↔ ((1st ‘𝑧) ∈ 𝑥 ∧ (1st ‘𝑧) ∈ {𝑦}))
141	138, 139, 140	3imtr4i 292	. . . . . . 7 ⊢ (𝑧 ∈ (∪ 𝑗 ∈ 𝑥 ({𝑗} × 𝐵) ∩ ({𝑦} × ⦋𝑦 / 𝑗⦌𝐵)) → (1st ‘𝑧) ∈ (𝑥 ∩ {𝑦}))
142	118	eleq2d 2813	. . . . . . . 8 ⊢ (𝜑 → ((1st ‘𝑧) ∈ (𝑥 ∩ {𝑦}) ↔ (1st ‘𝑧) ∈ ∅))
143		noel 4325	. . . . . . . . 9 ⊢ ¬ (1st ‘𝑧) ∈ ∅
144	143	pm2.21i 119	. . . . . . . 8 ⊢ ((1st ‘𝑧) ∈ ∅ → 𝑧 ∈ ∅)
145	142, 144	biimtrdi 252	. . . . . . 7 ⊢ (𝜑 → ((1st ‘𝑧) ∈ (𝑥 ∩ {𝑦}) → 𝑧 ∈ ∅))
146	141, 145	syl5 34	. . . . . 6 ⊢ (𝜑 → (𝑧 ∈ (∪ 𝑗 ∈ 𝑥 ({𝑗} × 𝐵) ∩ ({𝑦} × ⦋𝑦 / 𝑗⦌𝐵)) → 𝑧 ∈ ∅))
147	146	ssrdv 3983	. . . . 5 ⊢ (𝜑 → (∪ 𝑗 ∈ 𝑥 ({𝑗} × 𝐵) ∩ ({𝑦} × ⦋𝑦 / 𝑗⦌𝐵)) ⊆ ∅)
148		ss0 4393	. . . . 5 ⊢ ((∪ 𝑗 ∈ 𝑥 ({𝑗} × 𝐵) ∩ ({𝑦} × ⦋𝑦 / 𝑗⦌𝐵)) ⊆ ∅ → (∪ 𝑗 ∈ 𝑥 ({𝑗} × 𝐵) ∩ ({𝑦} × ⦋𝑦 / 𝑗⦌𝐵)) = ∅)
149	147, 148	syl 17	. . . 4 ⊢ (𝜑 → (∪ 𝑗 ∈ 𝑥 ({𝑗} × 𝐵) ∩ ({𝑦} × ⦋𝑦 / 𝑗⦌𝐵)) = ∅)
150		iunxun 5090	. . . . . 6 ⊢ ∪ 𝑗 ∈ (𝑥 ∪ {𝑦})({𝑗} × 𝐵) = (∪ 𝑗 ∈ 𝑥 ({𝑗} × 𝐵) ∪ ∪ 𝑗 ∈ {𝑦} ({𝑗} × 𝐵))
151		nfcv 2897	. . . . . . . . 9 ⊢ Ⅎ𝑚({𝑗} × 𝐵)
152		nfcv 2897	. . . . . . . . . 10 ⊢ Ⅎ𝑗{𝑚}
153	152, 5	nfxp 5702	. . . . . . . . 9 ⊢ Ⅎ𝑗({𝑚} × ⦋𝑚 / 𝑗⦌𝐵)
154		sneq 4633	. . . . . . . . . 10 ⊢ (𝑗 = 𝑚 → {𝑗} = {𝑚})
155	154, 8	xpeq12d 5700	. . . . . . . . 9 ⊢ (𝑗 = 𝑚 → ({𝑗} × 𝐵) = ({𝑚} × ⦋𝑚 / 𝑗⦌𝐵))
156	151, 153, 155	cbviun 5032	. . . . . . . 8 ⊢ ∪ 𝑗 ∈ {𝑦} ({𝑗} × 𝐵) = ∪ 𝑚 ∈ {𝑦} ({𝑚} × ⦋𝑚 / 𝑗⦌𝐵)
157		sneq 4633	. . . . . . . . . 10 ⊢ (𝑚 = 𝑦 → {𝑚} = {𝑦})
158	157, 38	xpeq12d 5700	. . . . . . . . 9 ⊢ (𝑚 = 𝑦 → ({𝑚} × ⦋𝑚 / 𝑗⦌𝐵) = ({𝑦} × ⦋𝑦 / 𝑗⦌𝐵))
159	15, 158	iunxsn 5087	. . . . . . . 8 ⊢ ∪ 𝑚 ∈ {𝑦} ({𝑚} × ⦋𝑚 / 𝑗⦌𝐵) = ({𝑦} × ⦋𝑦 / 𝑗⦌𝐵)
160	156, 159	eqtri 2754	. . . . . . 7 ⊢ ∪ 𝑗 ∈ {𝑦} ({𝑗} × 𝐵) = ({𝑦} × ⦋𝑦 / 𝑗⦌𝐵)
161	160	uneq2i 4155	. . . . . 6 ⊢ (∪ 𝑗 ∈ 𝑥 ({𝑗} × 𝐵) ∪ ∪ 𝑗 ∈ {𝑦} ({𝑗} × 𝐵)) = (∪ 𝑗 ∈ 𝑥 ({𝑗} × 𝐵) ∪ ({𝑦} × ⦋𝑦 / 𝑗⦌𝐵))
162	150, 161	eqtri 2754	. . . . 5 ⊢ ∪ 𝑗 ∈ (𝑥 ∪ {𝑦})({𝑗} × 𝐵) = (∪ 𝑗 ∈ 𝑥 ({𝑗} × 𝐵) ∪ ({𝑦} × ⦋𝑦 / 𝑗⦌𝐵))
163	162	a1i 11	. . . 4 ⊢ (𝜑 → ∪ 𝑗 ∈ (𝑥 ∪ {𝑦})({𝑗} × 𝐵) = (∪ 𝑗 ∈ 𝑥 ({𝑗} × 𝐵) ∪ ({𝑦} × ⦋𝑦 / 𝑗⦌𝐵)))
164		snfi 9046	. . . . . . 7 ⊢ {𝑗} ∈ Fin
165	122, 18	syldan 590	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑥 ∪ {𝑦})) → 𝐵 ∈ Fin)
166		xpfi 9319	. . . . . . 7 ⊢ (({𝑗} ∈ Fin ∧ 𝐵 ∈ Fin) → ({𝑗} × 𝐵) ∈ Fin)
167	164, 165, 166	sylancr 586	. . . . . 6 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑥 ∪ {𝑦})) → ({𝑗} × 𝐵) ∈ Fin)
168	167	ralrimiva 3140	. . . . 5 ⊢ (𝜑 → ∀𝑗 ∈ (𝑥 ∪ {𝑦})({𝑗} × 𝐵) ∈ Fin)
169		iunfi 9342	. . . . 5 ⊢ (((𝑥 ∪ {𝑦}) ∈ Fin ∧ ∀𝑗 ∈ (𝑥 ∪ {𝑦})({𝑗} × 𝐵) ∈ Fin) → ∪ 𝑗 ∈ (𝑥 ∪ {𝑦})({𝑗} × 𝐵) ∈ Fin)
170	121, 168, 169	syl2anc 583	. . . 4 ⊢ (𝜑 → ∪ 𝑗 ∈ (𝑥 ∪ {𝑦})({𝑗} × 𝐵) ∈ Fin)
171		eliun 4994	. . . . . 6 ⊢ (𝑧 ∈ ∪ 𝑗 ∈ (𝑥 ∪ {𝑦})({𝑗} × 𝐵) ↔ ∃𝑗 ∈ (𝑥 ∪ {𝑦})𝑧 ∈ ({𝑗} × 𝐵))
172		elxp 5692	. . . . . . . 8 ⊢ (𝑧 ∈ ({𝑗} × 𝐵) ↔ ∃𝑚∃𝑘(𝑧 = ⟨𝑚, 𝑘⟩ ∧ (𝑚 ∈ {𝑗} ∧ 𝑘 ∈ 𝐵)))
173		simprl 768	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ (𝑥 ∪ {𝑦})) ∧ (𝑧 = ⟨𝑚, 𝑘⟩ ∧ (𝑚 ∈ {𝑗} ∧ 𝑘 ∈ 𝐵))) → 𝑧 = ⟨𝑚, 𝑘⟩)
174		simprrl 778	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ (𝑥 ∪ {𝑦})) ∧ (𝑧 = ⟨𝑚, 𝑘⟩ ∧ (𝑚 ∈ {𝑗} ∧ 𝑘 ∈ 𝐵))) → 𝑚 ∈ {𝑗})
175		elsni 4640	. . . . . . . . . . . . . . 15 ⊢ (𝑚 ∈ {𝑗} → 𝑚 = 𝑗)
176	174, 175	syl 17	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ (𝑥 ∪ {𝑦})) ∧ (𝑧 = ⟨𝑚, 𝑘⟩ ∧ (𝑚 ∈ {𝑗} ∧ 𝑘 ∈ 𝐵))) → 𝑚 = 𝑗)
177	176	opeq1d 4874	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ (𝑥 ∪ {𝑦})) ∧ (𝑧 = ⟨𝑚, 𝑘⟩ ∧ (𝑚 ∈ {𝑗} ∧ 𝑘 ∈ 𝐵))) → ⟨𝑚, 𝑘⟩ = ⟨𝑗, 𝑘⟩)
178	173, 177	eqtrd 2766	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑗 ∈ (𝑥 ∪ {𝑦})) ∧ (𝑧 = ⟨𝑚, 𝑘⟩ ∧ (𝑚 ∈ {𝑗} ∧ 𝑘 ∈ 𝐵))) → 𝑧 = ⟨𝑗, 𝑘⟩)
179	178, 92	syl 17	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑗 ∈ (𝑥 ∪ {𝑦})) ∧ (𝑧 = ⟨𝑚, 𝑘⟩ ∧ (𝑚 ∈ {𝑗} ∧ 𝑘 ∈ 𝐵))) → 𝐷 = 𝐶)
180		simpll 764	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑗 ∈ (𝑥 ∪ {𝑦})) ∧ (𝑧 = ⟨𝑚, 𝑘⟩ ∧ (𝑚 ∈ {𝑗} ∧ 𝑘 ∈ 𝐵))) → 𝜑)
181	122	adantr 480	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑗 ∈ (𝑥 ∪ {𝑦})) ∧ (𝑧 = ⟨𝑚, 𝑘⟩ ∧ (𝑚 ∈ {𝑗} ∧ 𝑘 ∈ 𝐵))) → 𝑗 ∈ 𝐴)
182		simprrr 779	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑗 ∈ (𝑥 ∪ {𝑦})) ∧ (𝑧 = ⟨𝑚, 𝑘⟩ ∧ (𝑚 ∈ {𝑗} ∧ 𝑘 ∈ 𝐵))) → 𝑘 ∈ 𝐵)
183	180, 181, 182, 26	syl12anc 834	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑗 ∈ (𝑥 ∪ {𝑦})) ∧ (𝑧 = ⟨𝑚, 𝑘⟩ ∧ (𝑚 ∈ {𝑗} ∧ 𝑘 ∈ 𝐵))) → 𝐶 ∈ ℂ)
184	179, 183	eqeltrd 2827	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑗 ∈ (𝑥 ∪ {𝑦})) ∧ (𝑧 = ⟨𝑚, 𝑘⟩ ∧ (𝑚 ∈ {𝑗} ∧ 𝑘 ∈ 𝐵))) → 𝐷 ∈ ℂ)
185	184	ex 412	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑥 ∪ {𝑦})) → ((𝑧 = ⟨𝑚, 𝑘⟩ ∧ (𝑚 ∈ {𝑗} ∧ 𝑘 ∈ 𝐵)) → 𝐷 ∈ ℂ))
186	185	exlimdvv 1929	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑥 ∪ {𝑦})) → (∃𝑚∃𝑘(𝑧 = ⟨𝑚, 𝑘⟩ ∧ (𝑚 ∈ {𝑗} ∧ 𝑘 ∈ 𝐵)) → 𝐷 ∈ ℂ))
187	172, 186	biimtrid 241	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑥 ∪ {𝑦})) → (𝑧 ∈ ({𝑗} × 𝐵) → 𝐷 ∈ ℂ))
188	187	rexlimdva 3149	. . . . . 6 ⊢ (𝜑 → (∃𝑗 ∈ (𝑥 ∪ {𝑦})𝑧 ∈ ({𝑗} × 𝐵) → 𝐷 ∈ ℂ))
189	171, 188	biimtrid 241	. . . . 5 ⊢ (𝜑 → (𝑧 ∈ ∪ 𝑗 ∈ (𝑥 ∪ {𝑦})({𝑗} × 𝐵) → 𝐷 ∈ ℂ))
190	189	imp 406	. . . 4 ⊢ ((𝜑 ∧ 𝑧 ∈ ∪ 𝑗 ∈ (𝑥 ∪ {𝑦})({𝑗} × 𝐵)) → 𝐷 ∈ ℂ)
191	149, 163, 170, 190	fsumsplit 15693	. . 3 ⊢ (𝜑 → Σ𝑧 ∈ ∪ 𝑗 ∈ (𝑥 ∪ {𝑦})({𝑗} × 𝐵)𝐷 = (Σ𝑧 ∈ ∪ 𝑗 ∈ 𝑥 ({𝑗} × 𝐵)𝐷 + Σ𝑧 ∈ ({𝑦} × ⦋𝑦 / 𝑗⦌𝐵)𝐷))
192	191	adantr 480	. 2 ⊢ ((𝜑 ∧ 𝜓) → Σ𝑧 ∈ ∪ 𝑗 ∈ (𝑥 ∪ {𝑦})({𝑗} × 𝐵)𝐷 = (Σ𝑧 ∈ ∪ 𝑗 ∈ 𝑥 ({𝑗} × 𝐵)𝐷 + Σ𝑧 ∈ ({𝑦} × ⦋𝑦 / 𝑗⦌𝐵)𝐷))
193	115, 127, 192	3eqtr4d 2776	1 ⊢ ((𝜑 ∧ 𝜓) → Σ𝑗 ∈ (𝑥 ∪ {𝑦})Σ𝑘 ∈ 𝐵 𝐶 = Σ𝑧 ∈ ∪ 𝑗 ∈ (𝑥 ∪ {𝑦})({𝑗} × 𝐵)𝐷)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∧ wa 395   = wceq 1533  ∃wex 1773   ∈ wcel 2098  ∀wral 3055  ∃wrex 3064  ⦋csb 3888   ∪ cun 3941   ∩ cin 3942   ⊆ wss 3943  ∅c0 4317  {csn 4623  ⟨cop 4629  ∪ ciun 4990   × cxp 5667   ↾ cres 5671  –1-1-onto→wf1o 6536  ‘cfv 6537  (class class class)co 7405  1^st c1st 7972  2^nd c2nd 7973  Fincfn 8941  ℂcc 11110   + caddc 11115  Σcsu 15638

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2163  ax-ext 2697  ax-rep 5278  ax-sep 5292  ax-nul 5299  ax-pow 5356  ax-pr 5420  ax-un 7722  ax-inf2 9638  ax-cnex 11168  ax-resscn 11169  ax-1cn 11170  ax-icn 11171  ax-addcl 11172  ax-addrcl 11173  ax-mulcl 11174  ax-mulrcl 11175  ax-mulcom 11176  ax-addass 11177  ax-mulass 11178  ax-distr 11179  ax-i2m1 11180  ax-1ne0 11181  ax-1rid 11182  ax-rnegex 11183  ax-rrecex 11184  ax-cnre 11185  ax-pre-lttri 11186  ax-pre-lttrn 11187  ax-pre-ltadd 11188  ax-pre-mulgt0 11189  ax-pre-sup 11190

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2528  df-eu 2557  df-clab 2704  df-cleq 2718  df-clel 2804  df-nfc 2879  df-ne 2935  df-nel 3041  df-ral 3056  df-rex 3065  df-rmo 3370  df-reu 3371  df-rab 3427  df-v 3470  df-sbc 3773  df-csb 3889  df-dif 3946  df-un 3948  df-in 3950  df-ss 3960  df-pss 3962  df-nul 4318  df-if 4524  df-pw 4599  df-sn 4624  df-pr 4626  df-op 4630  df-uni 4903  df-int 4944  df-iun 4992  df-br 5142  df-opab 5204  df-mpt 5225  df-tr 5259  df-id 5567  df-eprel 5573  df-po 5581  df-so 5582  df-fr 5624  df-se 5625  df-we 5626  df-xp 5675  df-rel 5676  df-cnv 5677  df-co 5678  df-dm 5679  df-rn 5680  df-res 5681  df-ima 5682  df-pred 6294  df-ord 6361  df-on 6362  df-lim 6363  df-suc 6364  df-iota 6489  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544  df-fv 6545  df-isom 6546  df-riota 7361  df-ov 7408  df-oprab 7409  df-mpo 7410  df-om 7853  df-1st 7974  df-2nd 7975  df-frecs 8267  df-wrecs 8298  df-recs 8372  df-rdg 8411  df-1o 8467  df-er 8705  df-en 8942  df-dom 8943  df-sdom 8944  df-fin 8945  df-sup 9439  df-oi 9507  df-card 9936  df-pnf 11254  df-mnf 11255  df-xr 11256  df-ltxr 11257  df-le 11258  df-sub 11450  df-neg 11451  df-div 11876  df-nn 12217  df-2 12279  df-3 12280  df-n0 12477  df-z 12563  df-uz 12827  df-rp 12981  df-fz 13491  df-fzo 13634  df-seq 13973  df-exp 14033  df-hash 14296  df-cj 15052  df-re 15053  df-im 15054  df-sqrt 15188  df-abs 15189  df-clim 15438  df-sum 15639

This theorem is referenced by:  fsum2d  15723