Theorem gsummpt2d 30689

Description: Express a finite sum over a two-dimensional range as a double sum. See also gsum2d 19094. (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 2823	. . 3 ⊢ (0g‘𝑊) = (0g‘𝑊)
3		gsummpt2d.m	. . 3 ⊢ (𝜑 → 𝑊 ∈ CMnd)
4		gsummpt2d.2	. . 3 ⊢ (𝜑 → 𝐴 ∈ Fin)
5	4	dmexd 7617	. . 3 ⊢ (𝜑 → dom 𝐴 ∈ V)
6		gsummpt2d.3	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ 𝐵)
7		gsummpt2d.r	. . . 4 ⊢ (𝜑 → Rel 𝐴)
8		1stdm 7741	. . . 4 ⊢ ((Rel 𝐴 ∧ 𝑥 ∈ 𝐴) → (1st ‘𝑥) ∈ dom 𝐴)
9	7, 8	sylan 582	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (1st ‘𝑥) ∈ dom 𝐴)
10		fo1st 7711	. . . . . 6 ⊢ 1st :V–onto→V
11		fofn 6594	. . . . . 6 ⊢ (1st :V–onto→V → 1st Fn V)
12		dffn5 6726	. . . . . . 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 5851	. . . 4 ⊢ (1st ↾ 𝐴) = ((𝑥 ∈ V ↦ (1st ‘𝑥)) ↾ 𝐴)
16		ssv 3993	. . . . 5 ⊢ 𝐴 ⊆ V
17		resmpt 5907	. . . . 5 ⊢ (𝐴 ⊆ V → ((𝑥 ∈ V ↦ (1st ‘𝑥)) ↾ 𝐴) = (𝑥 ∈ 𝐴 ↦ (1st ‘𝑥)))
18	16, 17	ax-mp 5	. . . 4 ⊢ ((𝑥 ∈ V ↦ (1st ‘𝑥)) ↾ 𝐴) = (𝑥 ∈ 𝐴 ↦ (1st ‘𝑥))
19	15, 18	eqtri 2846	. . 3 ⊢ (1st ↾ 𝐴) = (𝑥 ∈ 𝐴 ↦ (1st ‘𝑥))
20	1, 2, 3, 4, 5, 6, 9, 19	gsummpt2co 30688	. 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 7622	. . . . . . 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 2916	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝑦 ∈ dom 𝐴) ∧ 𝑧 ∈ (𝐴 “ {𝑦})) ∧ 𝑥 ∈ 𝐴) ∧ 𝑥 = ⟨𝑦, 𝑧⟩) → 𝐷 ∈ 𝐵)
32		vex 3499	. . . . . . . . . . . 12 ⊢ 𝑦 ∈ V
33		vex 3499	. . . . . . . . . . . 12 ⊢ 𝑧 ∈ V
34	32, 33	elimasn 5956	. . . . . . . . . . 11 ⊢ (𝑧 ∈ (𝐴 “ {𝑦}) ↔ ⟨𝑦, 𝑧⟩ ∈ 𝐴)
35	34	biimpi 218	. . . . . . . . . 10 ⊢ (𝑧 ∈ (𝐴 “ {𝑦}) → ⟨𝑦, 𝑧⟩ ∈ 𝐴)
36	35	adantl 484	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑦 ∈ dom 𝐴) ∧ 𝑧 ∈ (𝐴 “ {𝑦})) → ⟨𝑦, 𝑧⟩ ∈ 𝐴)
37		simpr 487	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑦 ∈ dom 𝐴) ∧ 𝑧 ∈ (𝐴 “ {𝑦})) ∧ 𝑥 = ⟨𝑦, 𝑧⟩) → 𝑥 = ⟨𝑦, 𝑧⟩)
38	37	eqeq1d 2825	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑦 ∈ dom 𝐴) ∧ 𝑧 ∈ (𝐴 “ {𝑦})) ∧ 𝑥 = ⟨𝑦, 𝑧⟩) → (𝑥 = ⟨𝑦, 𝑧⟩ ↔ ⟨𝑦, 𝑧⟩ = ⟨𝑦, 𝑧⟩))
39		eqidd 2824	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑦 ∈ dom 𝐴) ∧ 𝑧 ∈ (𝐴 “ {𝑦})) → ⟨𝑦, 𝑧⟩ = ⟨𝑦, 𝑧⟩)
40	36, 38, 39	rspcedvd 3628	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑦 ∈ dom 𝐴) ∧ 𝑧 ∈ (𝐴 “ {𝑦})) → ∃𝑥 ∈ 𝐴 𝑥 = ⟨𝑦, 𝑧⟩)
41	31, 40	r19.29a 3291	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑦 ∈ dom 𝐴) ∧ 𝑧 ∈ (𝐴 “ {𝑦})) → 𝐷 ∈ 𝐵)
42	41	fmpttd 6881	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ dom 𝐴) → (𝑧 ∈ (𝐴 “ {𝑦}) ↦ 𝐷):(𝐴 “ {𝑦})⟶𝐵)
43		eqid 2823	. . . . . . 7 ⊢ (𝑧 ∈ (𝐴 “ {𝑦}) ↦ 𝐷) = (𝑧 ∈ (𝐴 “ {𝑦}) ↦ 𝐷)
44		imafi2 30449	. . . . . . . . 9 ⊢ (𝐴 ∈ Fin → (𝐴 “ {𝑦}) ∈ Fin)
45	4, 44	syl 17	. . . . . . . 8 ⊢ (𝜑 → (𝐴 “ {𝑦}) ∈ Fin)
46	45	adantr 483	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ dom 𝐴) → (𝐴 “ {𝑦}) ∈ Fin)
47		fvex 6685	. . . . . . . 8 ⊢ (0g‘𝑊) ∈ V
48	47	a1i 11	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ dom 𝐴) → (0g‘𝑊) ∈ V)
49	43, 46, 41, 48	fsuppmptdm 8846	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ dom 𝐴) → (𝑧 ∈ (𝐴 “ {𝑦}) ↦ 𝐷) finSupp (0g‘𝑊))
50		2ndconst 7798	. . . . . . . 8 ⊢ (𝑦 ∈ dom 𝐴 → (2nd ↾ ({𝑦} × (𝐴 “ {𝑦}))):({𝑦} × (𝐴 “ {𝑦}))–1-1-onto→(𝐴 “ {𝑦}))
51	50	adantl 484	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ dom 𝐴) → (2nd ↾ ({𝑦} × (𝐴 “ {𝑦}))):({𝑦} × (𝐴 “ {𝑦}))–1-1-onto→(𝐴 “ {𝑦}))
52		1stpreimas 30443	. . . . . . . . . 10 ⊢ ((Rel 𝐴 ∧ 𝑦 ∈ dom 𝐴) → (◡(1st ↾ 𝐴) “ {𝑦}) = ({𝑦} × (𝐴 “ {𝑦})))
53	7, 52	sylan 582	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ dom 𝐴) → (◡(1st ↾ 𝐴) “ {𝑦}) = ({𝑦} × (𝐴 “ {𝑦})))
54	53	reseq2d 5855	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ dom 𝐴) → (2nd ↾ (◡(1st ↾ 𝐴) “ {𝑦})) = (2nd ↾ ({𝑦} × (𝐴 “ {𝑦}))))
55		f1oeq1 6606	. . . . . . . 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 19038	. . . . 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 2917	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ dom 𝐴) ∧ 𝑥 ∈ (◡(1st ↾ 𝐴) “ {𝑦})) → 𝑥 ∈ ({𝑦} × (𝐴 “ {𝑦})))
62		xp2nd 7724	. . . . . . . . . 10 ⊢ (𝑥 ∈ ({𝑦} × (𝐴 “ {𝑦})) → (2nd ‘𝑥) ∈ (𝐴 “ {𝑦}))
63	61, 62	syl 17	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑦 ∈ dom 𝐴) ∧ 𝑥 ∈ (◡(1st ↾ 𝐴) “ {𝑦})) → (2nd ‘𝑥) ∈ (𝐴 “ {𝑦}))
64	63	ralrimiva 3184	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ dom 𝐴) → ∀𝑥 ∈ (◡(1st ↾ 𝐴) “ {𝑦})(2nd ‘𝑥) ∈ (𝐴 “ {𝑦}))
65		fo2nd 7712	. . . . . . . . . . . 12 ⊢ 2nd :V–onto→V
66		fofn 6594	. . . . . . . . . . . 12 ⊢ (2nd :V–onto→V → 2nd Fn V)
67		dffn5 6726	. . . . . . . . . . . . 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 5851	. . . . . . . . . 10 ⊢ (2nd ↾ (◡(1st ↾ 𝐴) “ {𝑦})) = ((𝑥 ∈ V ↦ (2nd ‘𝑥)) ↾ (◡(1st ↾ 𝐴) “ {𝑦}))
71		ssv 3993	. . . . . . . . . . 11 ⊢ (◡(1st ↾ 𝐴) “ {𝑦}) ⊆ V
72		resmpt 5907	. . . . . . . . . . 11 ⊢ ((◡(1st ↾ 𝐴) “ {𝑦}) ⊆ V → ((𝑥 ∈ V ↦ (2nd ‘𝑥)) ↾ (◡(1st ↾ 𝐴) “ {𝑦})) = (𝑥 ∈ (◡(1st ↾ 𝐴) “ {𝑦}) ↦ (2nd ‘𝑥)))
73	71, 72	ax-mp 5	. . . . . . . . . 10 ⊢ ((𝑥 ∈ V ↦ (2nd ‘𝑥)) ↾ (◡(1st ↾ 𝐴) “ {𝑦})) = (𝑥 ∈ (◡(1st ↾ 𝐴) “ {𝑦}) ↦ (2nd ‘𝑥))
74	70, 73	eqtri 2846	. . . . . . . . 9 ⊢ (2nd ↾ (◡(1st ↾ 𝐴) “ {𝑦})) = (𝑥 ∈ (◡(1st ↾ 𝐴) “ {𝑦}) ↦ (2nd ‘𝑥))
75	74	a1i 11	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ dom 𝐴) → (2nd ↾ (◡(1st ↾ 𝐴) “ {𝑦})) = (𝑥 ∈ (◡(1st ↾ 𝐴) “ {𝑦}) ↦ (2nd ‘𝑥)))
76		eqidd 2824	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ dom 𝐴) → (𝑧 ∈ (𝐴 “ {𝑦}) ↦ 𝐷) = (𝑧 ∈ (𝐴 “ {𝑦}) ↦ 𝐷))
77	64, 75, 76	fmptcos 6895	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ dom 𝐴) → ((𝑧 ∈ (𝐴 “ {𝑦}) ↦ 𝐷) ∘ (2nd ↾ (◡(1st ↾ 𝐴) “ {𝑦}))) = (𝑥 ∈ (◡(1st ↾ 𝐴) “ {𝑦}) ↦ ⦋(2nd ‘𝑥) / 𝑧⦌𝐷))
78		nfv 1915	. . . . . . . . 9 ⊢ Ⅎ𝑧((𝜑 ∧ 𝑦 ∈ dom 𝐴) ∧ 𝑥 ∈ (◡(1st ↾ 𝐴) “ {𝑦}))
79		gsummpt2d.c	. . . . . . . . . 10 ⊢ Ⅎ𝑧𝐶
80	79	a1i 11	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑦 ∈ dom 𝐴) ∧ 𝑥 ∈ (◡(1st ↾ 𝐴) “ {𝑦})) → Ⅎ𝑧𝐶)
81	61	adantr 483	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑦 ∈ dom 𝐴) ∧ 𝑥 ∈ (◡(1st ↾ 𝐴) “ {𝑦})) ∧ 𝑧 = (2nd ‘𝑥)) → 𝑥 ∈ ({𝑦} × (𝐴 “ {𝑦})))
82		xp1st 7723	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ ({𝑦} × (𝐴 “ {𝑦})) → (1st ‘𝑥) ∈ {𝑦})
83	81, 82	syl 17	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑦 ∈ dom 𝐴) ∧ 𝑥 ∈ (◡(1st ↾ 𝐴) “ {𝑦})) ∧ 𝑧 = (2nd ‘𝑥)) → (1st ‘𝑥) ∈ {𝑦})
84		fvex 6685	. . . . . . . . . . . . . 14 ⊢ (1st ‘𝑥) ∈ V
85	84	elsn 4584	. . . . . . . . . . . . 13 ⊢ ((1st ‘𝑥) ∈ {𝑦} ↔ (1st ‘𝑥) = 𝑦)
86	83, 85	sylib 220	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑦 ∈ dom 𝐴) ∧ 𝑥 ∈ (◡(1st ↾ 𝐴) “ {𝑦})) ∧ 𝑧 = (2nd ‘𝑥)) → (1st ‘𝑥) = 𝑦)
87		simpr 487	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑦 ∈ dom 𝐴) ∧ 𝑥 ∈ (◡(1st ↾ 𝐴) “ {𝑦})) ∧ 𝑧 = (2nd ‘𝑥)) → 𝑧 = (2nd ‘𝑥))
88	87	eqcomd 2829	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑦 ∈ dom 𝐴) ∧ 𝑥 ∈ (◡(1st ↾ 𝐴) “ {𝑦})) ∧ 𝑧 = (2nd ‘𝑥)) → (2nd ‘𝑥) = 𝑧)
89		eqopi 7727	. . . . . . . . . . . 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 2829	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑦 ∈ dom 𝐴) ∧ 𝑥 ∈ (◡(1st ↾ 𝐴) “ {𝑦})) ∧ 𝑧 = (2nd ‘𝑥)) → 𝐷 = 𝐶)
93	78, 80, 63, 92	csbiedf 3915	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑦 ∈ dom 𝐴) ∧ 𝑥 ∈ (◡(1st ↾ 𝐴) “ {𝑦})) → ⦋(2nd ‘𝑥) / 𝑧⦌𝐷 = 𝐶)
94	93	mpteq2dva 5163	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ dom 𝐴) → (𝑥 ∈ (◡(1st ↾ 𝐴) “ {𝑦}) ↦ ⦋(2nd ‘𝑥) / 𝑧⦌𝐷) = (𝑥 ∈ (◡(1st ↾ 𝐴) “ {𝑦}) ↦ 𝐶))
95	77, 94	eqtrd 2858	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ dom 𝐴) → ((𝑧 ∈ (𝐴 “ {𝑦}) ↦ 𝐷) ∘ (2nd ↾ (◡(1st ↾ 𝐴) “ {𝑦}))) = (𝑥 ∈ (◡(1st ↾ 𝐴) “ {𝑦}) ↦ 𝐶))
96	95	oveq2d 7174	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ dom 𝐴) → (𝑊 Σg ((𝑧 ∈ (𝐴 “ {𝑦}) ↦ 𝐷) ∘ (2nd ↾ (◡(1st ↾ 𝐴) “ {𝑦})))) = (𝑊 Σg (𝑥 ∈ (◡(1st ↾ 𝐴) “ {𝑦}) ↦ 𝐶)))
97	58, 96	eqtr2d 2859	. . . 4 ⊢ ((𝜑 ∧ 𝑦 ∈ dom 𝐴) → (𝑊 Σg (𝑥 ∈ (◡(1st ↾ 𝐴) “ {𝑦}) ↦ 𝐶)) = (𝑊 Σg (𝑧 ∈ (𝐴 “ {𝑦}) ↦ 𝐷)))
98	21, 97	mpteq2da 5162	. . 3 ⊢ (𝜑 → (𝑦 ∈ dom 𝐴 ↦ (𝑊 Σg (𝑥 ∈ (◡(1st ↾ 𝐴) “ {𝑦}) ↦ 𝐶))) = (𝑦 ∈ dom 𝐴 ↦ (𝑊 Σg (𝑧 ∈ (𝐴 “ {𝑦}) ↦ 𝐷))))
99	98	oveq2d 7174	. 2 ⊢ (𝜑 → (𝑊 Σg (𝑦 ∈ dom 𝐴 ↦ (𝑊 Σg (𝑥 ∈ (◡(1st ↾ 𝐴) “ {𝑦}) ↦ 𝐶)))) = (𝑊 Σg (𝑦 ∈ dom 𝐴 ↦ (𝑊 Σg (𝑧 ∈ (𝐴 “ {𝑦}) ↦ 𝐷)))))
100	20, 99	eqtrd 2858	1 ⊢ (𝜑 → (𝑊 Σg (𝑥 ∈ 𝐴 ↦ 𝐶)) = (𝑊 Σg (𝑦 ∈ dom 𝐴 ↦ (𝑊 Σg (𝑧 ∈ (𝐴 “ {𝑦}) ↦ 𝐷)))))

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 398   = wceq 1537  Ⅎwnf 1784   ∈ wcel 2114  Ⅎwnfc 2963  Vcvv 3496  ⦋csb 3885   ⊆ wss 3938  {csn 4569  ⟨cop 4575   ↦ cmpt 5148   × cxp 5555  ^◡ccnv 5556  dom cdm 5557   ↾ cres 5559   “ cima 5560   ∘ ccom 5561  Rel wrel 5562   Fn wfn 6352  –onto→wfo 6355  –1-1-onto→wf1o 6356  ‘cfv 6357  (class class class)co 7158  1^st c1st 7689  2^nd c2nd 7690  Fincfn 8511  Basecbs 16485  0_gc0g 16715   Σ_g cgsu 16716  CMndccmn 18908

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795  ax-rep 5192  ax-sep 5205  ax-nul 5212  ax-pow 5268  ax-pr 5332  ax-un 7463  ax-cnex 10595  ax-resscn 10596  ax-1cn 10597  ax-icn 10598  ax-addcl 10599  ax-addrcl 10600  ax-mulcl 10601  ax-mulrcl 10602  ax-mulcom 10603  ax-addass 10604  ax-mulass 10605  ax-distr 10606  ax-i2m1 10607  ax-1ne0 10608  ax-1rid 10609  ax-rnegex 10610  ax-rrecex 10611  ax-cnre 10612  ax-pre-lttri 10613  ax-pre-lttrn 10614  ax-pre-ltadd 10615  ax-pre-mulgt0 10616

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-ne 3019  df-nel 3126  df-ral 3145  df-rex 3146  df-reu 3147  df-rmo 3148  df-rab 3149  df-v 3498  df-sbc 3775  df-csb 3886  df-dif 3941  df-un 3943  df-in 3945  df-ss 3954  df-pss 3956  df-nul 4294  df-if 4470  df-pw 4543  df-sn 4570  df-pr 4572  df-tp 4574  df-op 4576  df-uni 4841  df-int 4879  df-iun 4923  df-iin 4924  df-br 5069  df-opab 5131  df-mpt 5149  df-tr 5175  df-id 5462  df-eprel 5467  df-po 5476  df-so 5477  df-fr 5516  df-se 5517  df-we 5518  df-xp 5563  df-rel 5564  df-cnv 5565  df-co 5566  df-dm 5567  df-rn 5568  df-res 5569  df-ima 5570  df-pred 6150  df-ord 6196  df-on 6197  df-lim 6198  df-suc 6199  df-iota 6316  df-fun 6359  df-fn 6360  df-f 6361  df-f1 6362  df-fo 6363  df-f1o 6364  df-fv 6365  df-isom 6366  df-riota 7116  df-ov 7161  df-oprab 7162  df-mpo 7163  df-of 7411  df-om 7583  df-1st 7691  df-2nd 7692  df-supp 7833  df-wrecs 7949  df-recs 8010  df-rdg 8048  df-1o 8104  df-oadd 8108  df-er 8291  df-en 8512  df-dom 8513  df-sdom 8514  df-fin 8515  df-fsupp 8836  df-oi 8976  df-card 9370  df-pnf 10679  df-mnf 10680  df-xr 10681  df-ltxr 10682  df-le 10683  df-sub 10874  df-neg 10875  df-nn 11641  df-2 11703  df-n0 11901  df-z 11985  df-uz 12247  df-fz 12896  df-fzo 13037  df-seq 13373  df-hash 13694  df-ndx 16488  df-slot 16489  df-base 16491  df-sets 16492  df-ress 16493  df-plusg 16580  df-0g 16717  df-gsum 16718  df-mre 16859  df-mrc 16860  df-acs 16862  df-mgm 17854  df-sgrp 17903  df-mnd 17914  df-submnd 17959  df-mulg 18227  df-cntz 18449  df-cmn 18910

This theorem is referenced by:  esum2d  31354