Theorem gsummpt2d 30682

Description: Express a finite sum over a two-dimensional range as a double sum. See also gsum2d 19086. (Contributed by Thierry Arnoux, 27-Apr-2020.)

Hypotheses

Ref	Expression
gsummpt2d.c	⊢ Ⅎ𝑧𝐶
gsummpt2d.0	⊢ Ⅎ𝑦𝜑
gsummpt2d.b	⊢ 𝐵 = (Base‘𝑊)
gsummpt2d.1	⊢ (𝑥 = ⟨𝑦, 𝑧⟩ → 𝐶 = 𝐷)
gsummpt2d.r	⊢ (𝜑 → Rel 𝐴)
gsummpt2d.2	⊢ (𝜑 → 𝐴 ∈ Fin)
gsummpt2d.m	⊢ (𝜑 → 𝑊 ∈ CMnd)
gsummpt2d.3	⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ 𝐵)

Assertion

Ref	Expression
gsummpt2d	⊢ (𝜑 → (𝑊 Σg (𝑥 ∈ 𝐴 ↦ 𝐶)) = (𝑊 Σg (𝑦 ∈ dom 𝐴 ↦ (𝑊 Σg (𝑧 ∈ (𝐴 “ {𝑦}) ↦ 𝐷)))))

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

Allowed substitution hints:   𝜑(𝑦)   𝐶(𝑥,𝑧)   𝐷(𝑦,𝑧)   𝑊(𝑧)

Proof of Theorem gsummpt2d

Step	Hyp	Ref	Expression
1		gsummpt2d.b	. . 3 ⊢ 𝐵 = (Base‘𝑊)
2		eqid 2821	. . 3 ⊢ (0g‘𝑊) = (0g‘𝑊)
3		gsummpt2d.m	. . 3 ⊢ (𝜑 → 𝑊 ∈ CMnd)
4		gsummpt2d.2	. . 3 ⊢ (𝜑 → 𝐴 ∈ Fin)
5	4	dmexd 7609	. . 3 ⊢ (𝜑 → dom 𝐴 ∈ V)
6		gsummpt2d.3	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ 𝐵)
7		gsummpt2d.r	. . . 4 ⊢ (𝜑 → Rel 𝐴)
8		1stdm 7733	. . . 4 ⊢ ((Rel 𝐴 ∧ 𝑥 ∈ 𝐴) → (1st ‘𝑥) ∈ dom 𝐴)
9	7, 8	sylan 582	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (1st ‘𝑥) ∈ dom 𝐴)
10		fo1st 7703	. . . . . 6 ⊢ 1st :V–onto→V
11		fofn 6587	. . . . . 6 ⊢ (1st :V–onto→V → 1st Fn V)
12		dffn5 6719	. . . . . . 7 ⊢ (1st Fn V ↔ 1st = (𝑥 ∈ V ↦ (1st ‘𝑥)))
13	12	biimpi 218	. . . . . 6 ⊢ (1st Fn V → 1st = (𝑥 ∈ V ↦ (1st ‘𝑥)))
14	10, 11, 13	mp2b 10	. . . . 5 ⊢ 1st = (𝑥 ∈ V ↦ (1st ‘𝑥))
15	14	reseq1i 5844	. . . 4 ⊢ (1st ↾ 𝐴) = ((𝑥 ∈ V ↦ (1st ‘𝑥)) ↾ 𝐴)
16		ssv 3991	. . . . 5 ⊢ 𝐴 ⊆ V
17		resmpt 5900	. . . . 5 ⊢ (𝐴 ⊆ V → ((𝑥 ∈ V ↦ (1st ‘𝑥)) ↾ 𝐴) = (𝑥 ∈ 𝐴 ↦ (1st ‘𝑥)))
18	16, 17	ax-mp 5	. . . 4 ⊢ ((𝑥 ∈ V ↦ (1st ‘𝑥)) ↾ 𝐴) = (𝑥 ∈ 𝐴 ↦ (1st ‘𝑥))
19	15, 18	eqtri 2844	. . 3 ⊢ (1st ↾ 𝐴) = (𝑥 ∈ 𝐴 ↦ (1st ‘𝑥))
20	1, 2, 3, 4, 5, 6, 9, 19	gsummpt2co 30681	. 2 ⊢ (𝜑 → (𝑊 Σg (𝑥 ∈ 𝐴 ↦ 𝐶)) = (𝑊 Σg (𝑦 ∈ dom 𝐴 ↦ (𝑊 Σg (𝑥 ∈ (◡(1st ↾ 𝐴) “ {𝑦}) ↦ 𝐶)))))
21		gsummpt2d.0	. . . 4 ⊢ Ⅎ𝑦𝜑
22	3	adantr 483	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ dom 𝐴) → 𝑊 ∈ CMnd)
23	4	adantr 483	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ dom 𝐴) → 𝐴 ∈ Fin)
24		imaexg 7614	. . . . . . 7 ⊢ (𝐴 ∈ Fin → (𝐴 “ {𝑦}) ∈ V)
25	23, 24	syl 17	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ dom 𝐴) → (𝐴 “ {𝑦}) ∈ V)
26		gsummpt2d.1	. . . . . . . . . 10 ⊢ (𝑥 = ⟨𝑦, 𝑧⟩ → 𝐶 = 𝐷)
27	26	adantl 484	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑦 ∈ dom 𝐴) ∧ 𝑧 ∈ (𝐴 “ {𝑦})) ∧ 𝑥 ∈ 𝐴) ∧ 𝑥 = ⟨𝑦, 𝑧⟩) → 𝐶 = 𝐷)
28		simp-4l 781	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑦 ∈ dom 𝐴) ∧ 𝑧 ∈ (𝐴 “ {𝑦})) ∧ 𝑥 ∈ 𝐴) ∧ 𝑥 = ⟨𝑦, 𝑧⟩) → 𝜑)
29		simplr 767	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑦 ∈ dom 𝐴) ∧ 𝑧 ∈ (𝐴 “ {𝑦})) ∧ 𝑥 ∈ 𝐴) ∧ 𝑥 = ⟨𝑦, 𝑧⟩) → 𝑥 ∈ 𝐴)
30	28, 29, 6	syl2anc 586	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑦 ∈ dom 𝐴) ∧ 𝑧 ∈ (𝐴 “ {𝑦})) ∧ 𝑥 ∈ 𝐴) ∧ 𝑥 = ⟨𝑦, 𝑧⟩) → 𝐶 ∈ 𝐵)
31	27, 30	eqeltrrd 2914	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝑦 ∈ dom 𝐴) ∧ 𝑧 ∈ (𝐴 “ {𝑦})) ∧ 𝑥 ∈ 𝐴) ∧ 𝑥 = ⟨𝑦, 𝑧⟩) → 𝐷 ∈ 𝐵)
32		vex 3498	. . . . . . . . . . . 12 ⊢ 𝑦 ∈ V
33		vex 3498	. . . . . . . . . . . 12 ⊢ 𝑧 ∈ V
34	32, 33	elimasn 5949	. . . . . . . . . . 11 ⊢ (𝑧 ∈ (𝐴 “ {𝑦}) ↔ ⟨𝑦, 𝑧⟩ ∈ 𝐴)
35	34	biimpi 218	. . . . . . . . . 10 ⊢ (𝑧 ∈ (𝐴 “ {𝑦}) → ⟨𝑦, 𝑧⟩ ∈ 𝐴)
36	35	adantl 484	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑦 ∈ dom 𝐴) ∧ 𝑧 ∈ (𝐴 “ {𝑦})) → ⟨𝑦, 𝑧⟩ ∈ 𝐴)
37		simpr 487	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑦 ∈ dom 𝐴) ∧ 𝑧 ∈ (𝐴 “ {𝑦})) ∧ 𝑥 = ⟨𝑦, 𝑧⟩) → 𝑥 = ⟨𝑦, 𝑧⟩)
38	37	eqeq1d 2823	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑦 ∈ dom 𝐴) ∧ 𝑧 ∈ (𝐴 “ {𝑦})) ∧ 𝑥 = ⟨𝑦, 𝑧⟩) → (𝑥 = ⟨𝑦, 𝑧⟩ ↔ ⟨𝑦, 𝑧⟩ = ⟨𝑦, 𝑧⟩))
39		eqidd 2822	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑦 ∈ dom 𝐴) ∧ 𝑧 ∈ (𝐴 “ {𝑦})) → ⟨𝑦, 𝑧⟩ = ⟨𝑦, 𝑧⟩)
40	36, 38, 39	rspcedvd 3626	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑦 ∈ dom 𝐴) ∧ 𝑧 ∈ (𝐴 “ {𝑦})) → ∃𝑥 ∈ 𝐴 𝑥 = ⟨𝑦, 𝑧⟩)
41	31, 40	r19.29a 3289	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑦 ∈ dom 𝐴) ∧ 𝑧 ∈ (𝐴 “ {𝑦})) → 𝐷 ∈ 𝐵)
42	41	fmpttd 6874	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ dom 𝐴) → (𝑧 ∈ (𝐴 “ {𝑦}) ↦ 𝐷):(𝐴 “ {𝑦})⟶𝐵)
43		eqid 2821	. . . . . . 7 ⊢ (𝑧 ∈ (𝐴 “ {𝑦}) ↦ 𝐷) = (𝑧 ∈ (𝐴 “ {𝑦}) ↦ 𝐷)
44		imafi2 30441	. . . . . . . . 9 ⊢ (𝐴 ∈ Fin → (𝐴 “ {𝑦}) ∈ Fin)
45	4, 44	syl 17	. . . . . . . 8 ⊢ (𝜑 → (𝐴 “ {𝑦}) ∈ Fin)
46	45	adantr 483	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ dom 𝐴) → (𝐴 “ {𝑦}) ∈ Fin)
47		fvex 6678	. . . . . . . 8 ⊢ (0g‘𝑊) ∈ V
48	47	a1i 11	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ dom 𝐴) → (0g‘𝑊) ∈ V)
49	43, 46, 41, 48	fsuppmptdm 8838	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ dom 𝐴) → (𝑧 ∈ (𝐴 “ {𝑦}) ↦ 𝐷) finSupp (0g‘𝑊))
50		2ndconst 7790	. . . . . . . 8 ⊢ (𝑦 ∈ dom 𝐴 → (2nd ↾ ({𝑦} × (𝐴 “ {𝑦}))):({𝑦} × (𝐴 “ {𝑦}))–1-1-onto→(𝐴 “ {𝑦}))
51	50	adantl 484	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ dom 𝐴) → (2nd ↾ ({𝑦} × (𝐴 “ {𝑦}))):({𝑦} × (𝐴 “ {𝑦}))–1-1-onto→(𝐴 “ {𝑦}))
52		1stpreimas 30435	. . . . . . . . . 10 ⊢ ((Rel 𝐴 ∧ 𝑦 ∈ dom 𝐴) → (◡(1st ↾ 𝐴) “ {𝑦}) = ({𝑦} × (𝐴 “ {𝑦})))
53	7, 52	sylan 582	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ dom 𝐴) → (◡(1st ↾ 𝐴) “ {𝑦}) = ({𝑦} × (𝐴 “ {𝑦})))
54	53	reseq2d 5848	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ dom 𝐴) → (2nd ↾ (◡(1st ↾ 𝐴) “ {𝑦})) = (2nd ↾ ({𝑦} × (𝐴 “ {𝑦}))))
55		f1oeq1 6599	. . . . . . . 8 ⊢ ((2nd ↾ (◡(1st ↾ 𝐴) “ {𝑦})) = (2nd ↾ ({𝑦} × (𝐴 “ {𝑦}))) → ((2nd ↾ (◡(1st ↾ 𝐴) “ {𝑦})):({𝑦} × (𝐴 “ {𝑦}))–1-1-onto→(𝐴 “ {𝑦}) ↔ (2nd ↾ ({𝑦} × (𝐴 “ {𝑦}))):({𝑦} × (𝐴 “ {𝑦}))–1-1-onto→(𝐴 “ {𝑦})))
56	54, 55	syl 17	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ dom 𝐴) → ((2nd ↾ (◡(1st ↾ 𝐴) “ {𝑦})):({𝑦} × (𝐴 “ {𝑦}))–1-1-onto→(𝐴 “ {𝑦}) ↔ (2nd ↾ ({𝑦} × (𝐴 “ {𝑦}))):({𝑦} × (𝐴 “ {𝑦}))–1-1-onto→(𝐴 “ {𝑦})))
57	51, 56	mpbird 259	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ dom 𝐴) → (2nd ↾ (◡(1st ↾ 𝐴) “ {𝑦})):({𝑦} × (𝐴 “ {𝑦}))–1-1-onto→(𝐴 “ {𝑦}))
58	1, 2, 22, 25, 42, 49, 57	gsumf1o 19030	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ dom 𝐴) → (𝑊 Σg (𝑧 ∈ (𝐴 “ {𝑦}) ↦ 𝐷)) = (𝑊 Σg ((𝑧 ∈ (𝐴 “ {𝑦}) ↦ 𝐷) ∘ (2nd ↾ (◡(1st ↾ 𝐴) “ {𝑦})))))
59		simpr 487	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑦 ∈ dom 𝐴) ∧ 𝑥 ∈ (◡(1st ↾ 𝐴) “ {𝑦})) → 𝑥 ∈ (◡(1st ↾ 𝐴) “ {𝑦}))
60	53	adantr 483	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑦 ∈ dom 𝐴) ∧ 𝑥 ∈ (◡(1st ↾ 𝐴) “ {𝑦})) → (◡(1st ↾ 𝐴) “ {𝑦}) = ({𝑦} × (𝐴 “ {𝑦})))
61	59, 60	eleqtrd 2915	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ dom 𝐴) ∧ 𝑥 ∈ (◡(1st ↾ 𝐴) “ {𝑦})) → 𝑥 ∈ ({𝑦} × (𝐴 “ {𝑦})))
62		xp2nd 7716	. . . . . . . . . 10 ⊢ (𝑥 ∈ ({𝑦} × (𝐴 “ {𝑦})) → (2nd ‘𝑥) ∈ (𝐴 “ {𝑦}))
63	61, 62	syl 17	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑦 ∈ dom 𝐴) ∧ 𝑥 ∈ (◡(1st ↾ 𝐴) “ {𝑦})) → (2nd ‘𝑥) ∈ (𝐴 “ {𝑦}))
64	63	ralrimiva 3182	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ dom 𝐴) → ∀𝑥 ∈ (◡(1st ↾ 𝐴) “ {𝑦})(2nd ‘𝑥) ∈ (𝐴 “ {𝑦}))
65		fo2nd 7704	. . . . . . . . . . . 12 ⊢ 2nd :V–onto→V
66		fofn 6587	. . . . . . . . . . . 12 ⊢ (2nd :V–onto→V → 2nd Fn V)
67		dffn5 6719	. . . . . . . . . . . . 13 ⊢ (2nd Fn V ↔ 2nd = (𝑥 ∈ V ↦ (2nd ‘𝑥)))
68	67	biimpi 218	. . . . . . . . . . . 12 ⊢ (2nd Fn V → 2nd = (𝑥 ∈ V ↦ (2nd ‘𝑥)))
69	65, 66, 68	mp2b 10	. . . . . . . . . . 11 ⊢ 2nd = (𝑥 ∈ V ↦ (2nd ‘𝑥))
70	69	reseq1i 5844	. . . . . . . . . 10 ⊢ (2nd ↾ (◡(1st ↾ 𝐴) “ {𝑦})) = ((𝑥 ∈ V ↦ (2nd ‘𝑥)) ↾ (◡(1st ↾ 𝐴) “ {𝑦}))
71		ssv 3991	. . . . . . . . . . 11 ⊢ (◡(1st ↾ 𝐴) “ {𝑦}) ⊆ V
72		resmpt 5900	. . . . . . . . . . 11 ⊢ ((◡(1st ↾ 𝐴) “ {𝑦}) ⊆ V → ((𝑥 ∈ V ↦ (2nd ‘𝑥)) ↾ (◡(1st ↾ 𝐴) “ {𝑦})) = (𝑥 ∈ (◡(1st ↾ 𝐴) “ {𝑦}) ↦ (2nd ‘𝑥)))
73	71, 72	ax-mp 5	. . . . . . . . . 10 ⊢ ((𝑥 ∈ V ↦ (2nd ‘𝑥)) ↾ (◡(1st ↾ 𝐴) “ {𝑦})) = (𝑥 ∈ (◡(1st ↾ 𝐴) “ {𝑦}) ↦ (2nd ‘𝑥))
74	70, 73	eqtri 2844	. . . . . . . . 9 ⊢ (2nd ↾ (◡(1st ↾ 𝐴) “ {𝑦})) = (𝑥 ∈ (◡(1st ↾ 𝐴) “ {𝑦}) ↦ (2nd ‘𝑥))
75	74	a1i 11	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ dom 𝐴) → (2nd ↾ (◡(1st ↾ 𝐴) “ {𝑦})) = (𝑥 ∈ (◡(1st ↾ 𝐴) “ {𝑦}) ↦ (2nd ‘𝑥)))
76		eqidd 2822	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ dom 𝐴) → (𝑧 ∈ (𝐴 “ {𝑦}) ↦ 𝐷) = (𝑧 ∈ (𝐴 “ {𝑦}) ↦ 𝐷))
77	64, 75, 76	fmptcos 6888	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ dom 𝐴) → ((𝑧 ∈ (𝐴 “ {𝑦}) ↦ 𝐷) ∘ (2nd ↾ (◡(1st ↾ 𝐴) “ {𝑦}))) = (𝑥 ∈ (◡(1st ↾ 𝐴) “ {𝑦}) ↦ ⦋(2nd ‘𝑥) / 𝑧⦌𝐷))
78		nfv 1911	. . . . . . . . 9 ⊢ Ⅎ𝑧((𝜑 ∧ 𝑦 ∈ dom 𝐴) ∧ 𝑥 ∈ (◡(1st ↾ 𝐴) “ {𝑦}))
79		gsummpt2d.c	. . . . . . . . . 10 ⊢ Ⅎ𝑧𝐶
80	79	a1i 11	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑦 ∈ dom 𝐴) ∧ 𝑥 ∈ (◡(1st ↾ 𝐴) “ {𝑦})) → Ⅎ𝑧𝐶)
81	61	adantr 483	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑦 ∈ dom 𝐴) ∧ 𝑥 ∈ (◡(1st ↾ 𝐴) “ {𝑦})) ∧ 𝑧 = (2nd ‘𝑥)) → 𝑥 ∈ ({𝑦} × (𝐴 “ {𝑦})))
82		xp1st 7715	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ ({𝑦} × (𝐴 “ {𝑦})) → (1st ‘𝑥) ∈ {𝑦})
83	81, 82	syl 17	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑦 ∈ dom 𝐴) ∧ 𝑥 ∈ (◡(1st ↾ 𝐴) “ {𝑦})) ∧ 𝑧 = (2nd ‘𝑥)) → (1st ‘𝑥) ∈ {𝑦})
84		fvex 6678	. . . . . . . . . . . . . 14 ⊢ (1st ‘𝑥) ∈ V
85	84	elsn 4576	. . . . . . . . . . . . 13 ⊢ ((1st ‘𝑥) ∈ {𝑦} ↔ (1st ‘𝑥) = 𝑦)
86	83, 85	sylib 220	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑦 ∈ dom 𝐴) ∧ 𝑥 ∈ (◡(1st ↾ 𝐴) “ {𝑦})) ∧ 𝑧 = (2nd ‘𝑥)) → (1st ‘𝑥) = 𝑦)
87		simpr 487	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑦 ∈ dom 𝐴) ∧ 𝑥 ∈ (◡(1st ↾ 𝐴) “ {𝑦})) ∧ 𝑧 = (2nd ‘𝑥)) → 𝑧 = (2nd ‘𝑥))
88	87	eqcomd 2827	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑦 ∈ dom 𝐴) ∧ 𝑥 ∈ (◡(1st ↾ 𝐴) “ {𝑦})) ∧ 𝑧 = (2nd ‘𝑥)) → (2nd ‘𝑥) = 𝑧)
89		eqopi 7719	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ ({𝑦} × (𝐴 “ {𝑦})) ∧ ((1st ‘𝑥) = 𝑦 ∧ (2nd ‘𝑥) = 𝑧)) → 𝑥 = ⟨𝑦, 𝑧⟩)
90	81, 86, 88, 89	syl12anc 834	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑦 ∈ dom 𝐴) ∧ 𝑥 ∈ (◡(1st ↾ 𝐴) “ {𝑦})) ∧ 𝑧 = (2nd ‘𝑥)) → 𝑥 = ⟨𝑦, 𝑧⟩)
91	90, 26	syl 17	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑦 ∈ dom 𝐴) ∧ 𝑥 ∈ (◡(1st ↾ 𝐴) “ {𝑦})) ∧ 𝑧 = (2nd ‘𝑥)) → 𝐶 = 𝐷)
92	91	eqcomd 2827	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑦 ∈ dom 𝐴) ∧ 𝑥 ∈ (◡(1st ↾ 𝐴) “ {𝑦})) ∧ 𝑧 = (2nd ‘𝑥)) → 𝐷 = 𝐶)
93	78, 80, 63, 92	csbiedf 3913	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑦 ∈ dom 𝐴) ∧ 𝑥 ∈ (◡(1st ↾ 𝐴) “ {𝑦})) → ⦋(2nd ‘𝑥) / 𝑧⦌𝐷 = 𝐶)
94	93	mpteq2dva 5154	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ dom 𝐴) → (𝑥 ∈ (◡(1st ↾ 𝐴) “ {𝑦}) ↦ ⦋(2nd ‘𝑥) / 𝑧⦌𝐷) = (𝑥 ∈ (◡(1st ↾ 𝐴) “ {𝑦}) ↦ 𝐶))
95	77, 94	eqtrd 2856	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ dom 𝐴) → ((𝑧 ∈ (𝐴 “ {𝑦}) ↦ 𝐷) ∘ (2nd ↾ (◡(1st ↾ 𝐴) “ {𝑦}))) = (𝑥 ∈ (◡(1st ↾ 𝐴) “ {𝑦}) ↦ 𝐶))
96	95	oveq2d 7166	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ dom 𝐴) → (𝑊 Σg ((𝑧 ∈ (𝐴 “ {𝑦}) ↦ 𝐷) ∘ (2nd ↾ (◡(1st ↾ 𝐴) “ {𝑦})))) = (𝑊 Σg (𝑥 ∈ (◡(1st ↾ 𝐴) “ {𝑦}) ↦ 𝐶)))
97	58, 96	eqtr2d 2857	. . . 4 ⊢ ((𝜑 ∧ 𝑦 ∈ dom 𝐴) → (𝑊 Σg (𝑥 ∈ (◡(1st ↾ 𝐴) “ {𝑦}) ↦ 𝐶)) = (𝑊 Σg (𝑧 ∈ (𝐴 “ {𝑦}) ↦ 𝐷)))
98	21, 97	mpteq2da 5153	. . 3 ⊢ (𝜑 → (𝑦 ∈ dom 𝐴 ↦ (𝑊 Σg (𝑥 ∈ (◡(1st ↾ 𝐴) “ {𝑦}) ↦ 𝐶))) = (𝑦 ∈ dom 𝐴 ↦ (𝑊 Σg (𝑧 ∈ (𝐴 “ {𝑦}) ↦ 𝐷))))
99	98	oveq2d 7166	. 2 ⊢ (𝜑 → (𝑊 Σg (𝑦 ∈ dom 𝐴 ↦ (𝑊 Σg (𝑥 ∈ (◡(1st ↾ 𝐴) “ {𝑦}) ↦ 𝐶)))) = (𝑊 Σg (𝑦 ∈ dom 𝐴 ↦ (𝑊 Σg (𝑧 ∈ (𝐴 “ {𝑦}) ↦ 𝐷)))))
100	20, 99	eqtrd 2856	1 ⊢ (𝜑 → (𝑊 Σg (𝑥 ∈ 𝐴 ↦ 𝐶)) = (𝑊 Σg (𝑦 ∈ dom 𝐴 ↦ (𝑊 Σg (𝑧 ∈ (𝐴 “ {𝑦}) ↦ 𝐷)))))

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 398   = wceq 1533  Ⅎwnf 1780   ∈ wcel 2110  Ⅎwnfc 2961  Vcvv 3495  ⦋csb 3883   ⊆ wss 3936  {csn 4561  ⟨cop 4567   ↦ cmpt 5139   × cxp 5548  ^◡ccnv 5549  dom cdm 5550   ↾ cres 5552   “ cima 5553   ∘ ccom 5554  Rel wrel 5555   Fn wfn 6345  –onto→wfo 6348  –1-1-onto→wf1o 6349  ‘cfv 6350  (class class class)co 7150  1^st c1st 7681  2^nd c2nd 7682  Fincfn 8503  Basecbs 16477  0_gc0g 16707   Σ_g cgsu 16708  CMndccmn 18900

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2156  ax-12 2172  ax-ext 2793  ax-rep 5183  ax-sep 5196  ax-nul 5203  ax-pow 5259  ax-pr 5322  ax-un 7455  ax-cnex 10587  ax-resscn 10588  ax-1cn 10589  ax-icn 10590  ax-addcl 10591  ax-addrcl 10592  ax-mulcl 10593  ax-mulrcl 10594  ax-mulcom 10595  ax-addass 10596  ax-mulass 10597  ax-distr 10598  ax-i2m1 10599  ax-1ne0 10600  ax-1rid 10601  ax-rnegex 10602  ax-rrecex 10603  ax-cnre 10604  ax-pre-lttri 10605  ax-pre-lttrn 10606  ax-pre-ltadd 10607  ax-pre-mulgt0 10608

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-mo 2618  df-eu 2650  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-nel 3124  df-ral 3143  df-rex 3144  df-reu 3145  df-rmo 3146  df-rab 3147  df-v 3497  df-sbc 3773  df-csb 3884  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-pss 3954  df-nul 4292  df-if 4468  df-pw 4541  df-sn 4562  df-pr 4564  df-tp 4566  df-op 4568  df-uni 4833  df-int 4870  df-iun 4914  df-iin 4915  df-br 5060  df-opab 5122  df-mpt 5140  df-tr 5166  df-id 5455  df-eprel 5460  df-po 5469  df-so 5470  df-fr 5509  df-se 5510  df-we 5511  df-xp 5556  df-rel 5557  df-cnv 5558  df-co 5559  df-dm 5560  df-rn 5561  df-res 5562  df-ima 5563  df-pred 6143  df-ord 6189  df-on 6190  df-lim 6191  df-suc 6192  df-iota 6309  df-fun 6352  df-fn 6353  df-f 6354  df-f1 6355  df-fo 6356  df-f1o 6357  df-fv 6358  df-isom 6359  df-riota 7108  df-ov 7153  df-oprab 7154  df-mpo 7155  df-of 7403  df-om 7575  df-1st 7683  df-2nd 7684  df-supp 7825  df-wrecs 7941  df-recs 8002  df-rdg 8040  df-1o 8096  df-oadd 8100  df-er 8283  df-en 8504  df-dom 8505  df-sdom 8506  df-fin 8507  df-fsupp 8828  df-oi 8968  df-card 9362  df-pnf 10671  df-mnf 10672  df-xr 10673  df-ltxr 10674  df-le 10675  df-sub 10866  df-neg 10867  df-nn 11633  df-2 11694  df-n0 11892  df-z 11976  df-uz 12238  df-fz 12887  df-fzo 13028  df-seq 13364  df-hash 13685  df-ndx 16480  df-slot 16481  df-base 16483  df-sets 16484  df-ress 16485  df-plusg 16572  df-0g 16709  df-gsum 16710  df-mre 16851  df-mrc 16852  df-acs 16854  df-mgm 17846  df-sgrp 17895  df-mnd 17906  df-submnd 17951  df-mulg 18219  df-cntz 18441  df-cmn 18902

This theorem is referenced by:  esum2d  31347