Theorem gsumfs2d 33533

Description: Express a finite sum over a two-dimensional range as a double sum. Version of gsum2d 20125 using finite support. (Contributed by Thierry Arnoux, 5-Oct-2025.)

Hypotheses

Ref	Expression
gsumfs2d.p	⊢ Ⅎ𝑥𝜑
gsumfs2d.b	⊢ 𝐵 = (Base‘𝑊)
gsumfs2d.1	⊢ 0 = (0g‘𝑊)
gsumfs2d.r	⊢ (𝜑 → Rel 𝐴)
gsumfs2d.2	⊢ (𝜑 → 𝐹 finSupp 0 )
gsumfs2d.w	⊢ (𝜑 → 𝑊 ∈ CMnd)
gsumfs2d.3	⊢ (𝜑 → 𝐹:𝐴⟶𝐵)
gsumfs2d.a	⊢ (𝜑 → 𝐴 ∈ 𝑋)

Assertion

Ref	Expression
gsumfs2d	⊢ (𝜑 → (𝑊 Σg 𝐹) = (𝑊 Σg (𝑥 ∈ dom 𝐴 ↦ (𝑊 Σg (𝑦 ∈ (𝐴 “ {𝑥}) ↦ (𝐹‘⟨𝑥, 𝑦⟩))))))

Distinct variable groups:   𝑥, 0 ,𝑦   𝑥,𝐴,𝑦   𝑥,𝐵,𝑦   𝑥,𝐹,𝑦   𝑥,𝑊,𝑦   𝜑,𝑥,𝑦

Allowed substitution hints:   𝑋(𝑥, 𝑦)

Proof of Theorem gsumfs2d

Dummy variables 𝑡 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		gsumfs2d.b	. . . . 5 ⊢ 𝐵 = (Base‘𝑊)
2		gsumfs2d.1	. . . . 5 ⊢ 0 = (0g‘𝑊)
3		gsumfs2d.w	. . . . . 6 ⊢ (𝜑 → 𝑊 ∈ CMnd)
4	3	adantr 486	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ dom (𝐹 supp 0 )) → 𝑊 ∈ CMnd)
5		gsumfs2d.a	. . . . . . 7 ⊢ (𝜑 → 𝐴 ∈ 𝑋)
6	5	adantr 486	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ dom (𝐹 supp 0 )) → 𝐴 ∈ 𝑋)
7	6	imaexd 7919	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ dom (𝐹 supp 0 )) → (𝐴 “ {𝑥}) ∈ V)
8		gsumfs2d.3	. . . . . . . 8 ⊢ (𝜑 → 𝐹:𝐴⟶𝐵)
9	8	ffnd 6706	. . . . . . 7 ⊢ (𝜑 → 𝐹 Fn 𝐴)
10	9	ad2antrr 739	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ dom (𝐹 supp 0 )) ∧ 𝑦 ∈ ((𝐴 “ {𝑥}) ∖ ((𝐹 supp 0 ) “ {𝑥}))) → 𝐹 Fn 𝐴)
11	5	ad2antrr 739	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ dom (𝐹 supp 0 )) ∧ 𝑦 ∈ ((𝐴 “ {𝑥}) ∖ ((𝐹 supp 0 ) “ {𝑥}))) → 𝐴 ∈ 𝑋)
12	2	fvexi 6895	. . . . . . 7 ⊢ 0 ∈ V
13	12	a1i 11	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ dom (𝐹 supp 0 )) ∧ 𝑦 ∈ ((𝐴 “ {𝑥}) ∖ ((𝐹 supp 0 ) “ {𝑥}))) → 0 ∈ V)
14		simpr 490	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ dom (𝐹 supp 0 )) ∧ 𝑦 ∈ ((𝐴 “ {𝑥}) ∖ ((𝐹 supp 0 ) “ {𝑥}))) → 𝑦 ∈ ((𝐴 “ {𝑥}) ∖ ((𝐹 supp 0 ) “ {𝑥})))
15	14	eldifad 3911	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ dom (𝐹 supp 0 )) ∧ 𝑦 ∈ ((𝐴 “ {𝑥}) ∖ ((𝐹 supp 0 ) “ {𝑥}))) → 𝑦 ∈ (𝐴 “ {𝑥}))
16		vex 3454	. . . . . . . . . 10 ⊢ 𝑥 ∈ V
17		vex 3454	. . . . . . . . . 10 ⊢ 𝑦 ∈ V
18	16, 17	elimasn 6088	. . . . . . . . 9 ⊢ (𝑦 ∈ (𝐴 “ {𝑥}) ↔ ⟨𝑥, 𝑦⟩ ∈ 𝐴)
19	18	biimpi 219	. . . . . . . 8 ⊢ (𝑦 ∈ (𝐴 “ {𝑥}) → ⟨𝑥, 𝑦⟩ ∈ 𝐴)
20	15, 19	syl 18	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ dom (𝐹 supp 0 )) ∧ 𝑦 ∈ ((𝐴 “ {𝑥}) ∖ ((𝐹 supp 0 ) “ {𝑥}))) → ⟨𝑥, 𝑦⟩ ∈ 𝐴)
21	14	eldifbd 3912	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ dom (𝐹 supp 0 )) ∧ 𝑦 ∈ ((𝐴 “ {𝑥}) ∖ ((𝐹 supp 0 ) “ {𝑥}))) → ¬ 𝑦 ∈ ((𝐹 supp 0 ) “ {𝑥}))
22	16, 17	elimasn 6088	. . . . . . . . 9 ⊢ (𝑦 ∈ ((𝐹 supp 0 ) “ {𝑥}) ↔ ⟨𝑥, 𝑦⟩ ∈ (𝐹 supp 0 ))
23	22	biimpri 231	. . . . . . . 8 ⊢ (⟨𝑥, 𝑦⟩ ∈ (𝐹 supp 0 ) → 𝑦 ∈ ((𝐹 supp 0 ) “ {𝑥}))
24	21, 23	nsyl 141	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ dom (𝐹 supp 0 )) ∧ 𝑦 ∈ ((𝐴 “ {𝑥}) ∖ ((𝐹 supp 0 ) “ {𝑥}))) → ¬ ⟨𝑥, 𝑦⟩ ∈ (𝐹 supp 0 ))
25	20, 24	eldifd 3910	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ dom (𝐹 supp 0 )) ∧ 𝑦 ∈ ((𝐴 “ {𝑥}) ∖ ((𝐹 supp 0 ) “ {𝑥}))) → ⟨𝑥, 𝑦⟩ ∈ (𝐴 ∖ (𝐹 supp 0 )))
26	10, 11, 13, 25	fvdifsupp 8174	. . . . 5 ⊢ (((𝜑 ∧ 𝑥 ∈ dom (𝐹 supp 0 )) ∧ 𝑦 ∈ ((𝐴 “ {𝑥}) ∖ ((𝐹 supp 0 ) “ {𝑥}))) → (𝐹‘⟨𝑥, 𝑦⟩) = 0 )
27		gsumfs2d.2	. . . . . . . 8 ⊢ (𝜑 → 𝐹 finSupp 0 )
28	27	fsuppimpd 9346	. . . . . . 7 ⊢ (𝜑 → (𝐹 supp 0 ) ∈ Fin)
29	28	adantr 486	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ dom (𝐹 supp 0 )) → (𝐹 supp 0 ) ∈ Fin)
30		imafi2 9335	. . . . . 6 ⊢ ((𝐹 supp 0 ) ∈ Fin → ((𝐹 supp 0 ) “ {𝑥}) ∈ Fin)
31	29, 30	syl 18	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ dom (𝐹 supp 0 )) → ((𝐹 supp 0 ) “ {𝑥}) ∈ Fin)
32	8	ad2antrr 739	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ dom (𝐹 supp 0 )) ∧ 𝑦 ∈ (𝐴 “ {𝑥})) → 𝐹:𝐴⟶𝐵)
33	19	adantl 487	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ dom (𝐹 supp 0 )) ∧ 𝑦 ∈ (𝐴 “ {𝑥})) → ⟨𝑥, 𝑦⟩ ∈ 𝐴)
34	32, 33	ffvelcdmd 7081	. . . . 5 ⊢ (((𝜑 ∧ 𝑥 ∈ dom (𝐹 supp 0 )) ∧ 𝑦 ∈ (𝐴 “ {𝑥})) → (𝐹‘⟨𝑥, 𝑦⟩) ∈ 𝐵)
35		suppssdm 8180	. . . . . . . 8 ⊢ (𝐹 supp 0 ) ⊆ dom 𝐹
36	35, 8	fssdm 6725	. . . . . . 7 ⊢ (𝜑 → (𝐹 supp 0 ) ⊆ 𝐴)
37	36	adantr 486	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ dom (𝐹 supp 0 )) → (𝐹 supp 0 ) ⊆ 𝐴)
38		imass1 6099	. . . . . 6 ⊢ ((𝐹 supp 0 ) ⊆ 𝐴 → ((𝐹 supp 0 ) “ {𝑥}) ⊆ (𝐴 “ {𝑥}))
39	37, 38	syl 18	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ dom (𝐹 supp 0 )) → ((𝐹 supp 0 ) “ {𝑥}) ⊆ (𝐴 “ {𝑥}))
40	1, 2, 4, 7, 26, 31, 34, 39	gsummptres2 33525	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ dom (𝐹 supp 0 )) → (𝑊 Σg (𝑦 ∈ (𝐴 “ {𝑥}) ↦ (𝐹‘⟨𝑥, 𝑦⟩))) = (𝑊 Σg (𝑦 ∈ ((𝐹 supp 0 ) “ {𝑥}) ↦ (𝐹‘⟨𝑥, 𝑦⟩))))
41	40	mpteq2dva 5198	. . 3 ⊢ (𝜑 → (𝑥 ∈ dom (𝐹 supp 0 ) ↦ (𝑊 Σg (𝑦 ∈ (𝐴 “ {𝑥}) ↦ (𝐹‘⟨𝑥, 𝑦⟩)))) = (𝑥 ∈ dom (𝐹 supp 0 ) ↦ (𝑊 Σg (𝑦 ∈ ((𝐹 supp 0 ) “ {𝑥}) ↦ (𝐹‘⟨𝑥, 𝑦⟩)))))
42	41	oveq2d 7432	. 2 ⊢ (𝜑 → (𝑊 Σg (𝑥 ∈ dom (𝐹 supp 0 ) ↦ (𝑊 Σg (𝑦 ∈ (𝐴 “ {𝑥}) ↦ (𝐹‘⟨𝑥, 𝑦⟩))))) = (𝑊 Σg (𝑥 ∈ dom (𝐹 supp 0 ) ↦ (𝑊 Σg (𝑦 ∈ ((𝐹 supp 0 ) “ {𝑥}) ↦ (𝐹‘⟨𝑥, 𝑦⟩))))))
43	5	dmexd 7906	. . 3 ⊢ (𝜑 → dom 𝐴 ∈ V)
44	9	ad2antrr 739	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ (dom 𝐴 ∖ dom (𝐹 supp 0 ))) ∧ 𝑦 ∈ (𝐴 “ {𝑥})) → 𝐹 Fn 𝐴)
45	5	ad2antrr 739	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ (dom 𝐴 ∖ dom (𝐹 supp 0 ))) ∧ 𝑦 ∈ (𝐴 “ {𝑥})) → 𝐴 ∈ 𝑋)
46	12	a1i 11	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ (dom 𝐴 ∖ dom (𝐹 supp 0 ))) ∧ 𝑦 ∈ (𝐴 “ {𝑥})) → 0 ∈ V)
47	19	adantl 487	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ (dom 𝐴 ∖ dom (𝐹 supp 0 ))) ∧ 𝑦 ∈ (𝐴 “ {𝑥})) → ⟨𝑥, 𝑦⟩ ∈ 𝐴)
48		simplr 781	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ (dom 𝐴 ∖ dom (𝐹 supp 0 ))) ∧ 𝑦 ∈ (𝐴 “ {𝑥})) → 𝑥 ∈ (dom 𝐴 ∖ dom (𝐹 supp 0 )))
49	48	eldifbd 3912	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ (dom 𝐴 ∖ dom (𝐹 supp 0 ))) ∧ 𝑦 ∈ (𝐴 “ {𝑥})) → ¬ 𝑥 ∈ dom (𝐹 supp 0 ))
50	16, 17	opeldm 5893	. . . . . . . . 9 ⊢ (⟨𝑥, 𝑦⟩ ∈ (𝐹 supp 0 ) → 𝑥 ∈ dom (𝐹 supp 0 ))
51	49, 50	nsyl 141	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ (dom 𝐴 ∖ dom (𝐹 supp 0 ))) ∧ 𝑦 ∈ (𝐴 “ {𝑥})) → ¬ ⟨𝑥, 𝑦⟩ ∈ (𝐹 supp 0 ))
52	47, 51	eldifd 3910	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ (dom 𝐴 ∖ dom (𝐹 supp 0 ))) ∧ 𝑦 ∈ (𝐴 “ {𝑥})) → ⟨𝑥, 𝑦⟩ ∈ (𝐴 ∖ (𝐹 supp 0 )))
53	44, 45, 46, 52	fvdifsupp 8174	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ (dom 𝐴 ∖ dom (𝐹 supp 0 ))) ∧ 𝑦 ∈ (𝐴 “ {𝑥})) → (𝐹‘⟨𝑥, 𝑦⟩) = 0 )
54	53	mpteq2dva 5198	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ (dom 𝐴 ∖ dom (𝐹 supp 0 ))) → (𝑦 ∈ (𝐴 “ {𝑥}) ↦ (𝐹‘⟨𝑥, 𝑦⟩)) = (𝑦 ∈ (𝐴 “ {𝑥}) ↦ 0 ))
55	54	oveq2d 7432	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ (dom 𝐴 ∖ dom (𝐹 supp 0 ))) → (𝑊 Σg (𝑦 ∈ (𝐴 “ {𝑥}) ↦ (𝐹‘⟨𝑥, 𝑦⟩))) = (𝑊 Σg (𝑦 ∈ (𝐴 “ {𝑥}) ↦ 0 )))
56	3	cmnmndd 19957	. . . . 5 ⊢ (𝜑 → 𝑊 ∈ Mnd)
57	5	adantr 486	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (dom 𝐴 ∖ dom (𝐹 supp 0 ))) → 𝐴 ∈ 𝑋)
58	57	imaexd 7919	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ (dom 𝐴 ∖ dom (𝐹 supp 0 ))) → (𝐴 “ {𝑥}) ∈ V)
59	2	gsumz 18971	. . . . 5 ⊢ ((𝑊 ∈ Mnd ∧ (𝐴 “ {𝑥}) ∈ V) → (𝑊 Σg (𝑦 ∈ (𝐴 “ {𝑥}) ↦ 0 )) = 0 )
60	56, 58, 59	syl2an2r 698	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ (dom 𝐴 ∖ dom (𝐹 supp 0 ))) → (𝑊 Σg (𝑦 ∈ (𝐴 “ {𝑥}) ↦ 0 )) = 0 )
61	55, 60	eqtrd 2795	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ (dom 𝐴 ∖ dom (𝐹 supp 0 ))) → (𝑊 Σg (𝑦 ∈ (𝐴 “ {𝑥}) ↦ (𝐹‘⟨𝑥, 𝑦⟩))) = 0 )
62		dmfi 9309	. . . 4 ⊢ ((𝐹 supp 0 ) ∈ Fin → dom (𝐹 supp 0 ) ∈ Fin)
63	28, 62	syl 18	. . 3 ⊢ (𝜑 → dom (𝐹 supp 0 ) ∈ Fin)
64	3	adantr 486	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐴) → 𝑊 ∈ CMnd)
65	5	adantr 486	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐴) → 𝐴 ∈ 𝑋)
66	65	imaexd 7919	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐴) → (𝐴 “ {𝑥}) ∈ V)
67	8	ad2antrr 739	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐴) ∧ 𝑦 ∈ (𝐴 “ {𝑥})) → 𝐹:𝐴⟶𝐵)
68	19	adantl 487	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐴) ∧ 𝑦 ∈ (𝐴 “ {𝑥})) → ⟨𝑥, 𝑦⟩ ∈ 𝐴)
69	67, 68	ffvelcdmd 7081	. . . . 5 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐴) ∧ 𝑦 ∈ (𝐴 “ {𝑥})) → (𝐹‘⟨𝑥, 𝑦⟩) ∈ 𝐵)
70	69	fmpttd 7111	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐴) → (𝑦 ∈ (𝐴 “ {𝑥}) ↦ (𝐹‘⟨𝑥, 𝑦⟩)):(𝐴 “ {𝑥})⟶𝐵)
71	66	mptexd 7226	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐴) → (𝑦 ∈ (𝐴 “ {𝑥}) ↦ (𝐹‘⟨𝑥, 𝑦⟩)) ∈ V)
72	70	ffnd 6706	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐴) → (𝑦 ∈ (𝐴 “ {𝑥}) ↦ (𝐹‘⟨𝑥, 𝑦⟩)) Fn (𝐴 “ {𝑥}))
73	12	a1i 11	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐴) → 0 ∈ V)
74	28	adantr 486	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐴) → (𝐹 supp 0 ) ∈ Fin)
75	74, 30	syl 18	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐴) → ((𝐹 supp 0 ) “ {𝑥}) ∈ Fin)
76		eqid 2760	. . . . . . . 8 ⊢ (𝑦 ∈ (𝐴 “ {𝑥}) ↦ (𝐹‘⟨𝑥, 𝑦⟩)) = (𝑦 ∈ (𝐴 “ {𝑥}) ↦ (𝐹‘⟨𝑥, 𝑦⟩))
77		simp-4l 795	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑥 ∈ dom 𝐴) ∧ 𝑡 ∈ (𝐴 “ {𝑥})) ∧ ¬ 𝑡 ∈ ((𝐹 supp 0 ) “ {𝑥})) ∧ 𝑦 = 𝑡) → 𝜑)
78		simp-4r 796	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑥 ∈ dom 𝐴) ∧ 𝑡 ∈ (𝐴 “ {𝑥})) ∧ ¬ 𝑡 ∈ ((𝐹 supp 0 ) “ {𝑥})) ∧ 𝑦 = 𝑡) → 𝑥 ∈ dom 𝐴)
79		simpr 490	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑥 ∈ dom 𝐴) ∧ 𝑡 ∈ (𝐴 “ {𝑥})) ∧ ¬ 𝑡 ∈ ((𝐹 supp 0 ) “ {𝑥})) ∧ 𝑦 = 𝑡) → 𝑦 = 𝑡)
80		simpllr 788	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑥 ∈ dom 𝐴) ∧ 𝑡 ∈ (𝐴 “ {𝑥})) ∧ ¬ 𝑡 ∈ ((𝐹 supp 0 ) “ {𝑥})) ∧ 𝑦 = 𝑡) → 𝑡 ∈ (𝐴 “ {𝑥}))
81	79, 80	eqeltrd 2860	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑥 ∈ dom 𝐴) ∧ 𝑡 ∈ (𝐴 “ {𝑥})) ∧ ¬ 𝑡 ∈ ((𝐹 supp 0 ) “ {𝑥})) ∧ 𝑦 = 𝑡) → 𝑦 ∈ (𝐴 “ {𝑥}))
82		simplr 781	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑥 ∈ dom 𝐴) ∧ 𝑡 ∈ (𝐴 “ {𝑥})) ∧ ¬ 𝑡 ∈ ((𝐹 supp 0 ) “ {𝑥})) ∧ 𝑦 = 𝑡) → ¬ 𝑡 ∈ ((𝐹 supp 0 ) “ {𝑥}))
83	79, 82	eqneltrd 2880	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑥 ∈ dom 𝐴) ∧ 𝑡 ∈ (𝐴 “ {𝑥})) ∧ ¬ 𝑡 ∈ ((𝐹 supp 0 ) “ {𝑥})) ∧ 𝑦 = 𝑡) → ¬ 𝑦 ∈ ((𝐹 supp 0 ) “ {𝑥}))
84	9	ad3antrrr 743	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑥 ∈ dom 𝐴) ∧ 𝑦 ∈ (𝐴 “ {𝑥})) ∧ ¬ 𝑦 ∈ ((𝐹 supp 0 ) “ {𝑥})) → 𝐹 Fn 𝐴)
85	5	ad3antrrr 743	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑥 ∈ dom 𝐴) ∧ 𝑦 ∈ (𝐴 “ {𝑥})) ∧ ¬ 𝑦 ∈ ((𝐹 supp 0 ) “ {𝑥})) → 𝐴 ∈ 𝑋)
86	12	a1i 11	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑥 ∈ dom 𝐴) ∧ 𝑦 ∈ (𝐴 “ {𝑥})) ∧ ¬ 𝑦 ∈ ((𝐹 supp 0 ) “ {𝑥})) → 0 ∈ V)
87	68	adantr 486	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑥 ∈ dom 𝐴) ∧ 𝑦 ∈ (𝐴 “ {𝑥})) ∧ ¬ 𝑦 ∈ ((𝐹 supp 0 ) “ {𝑥})) → ⟨𝑥, 𝑦⟩ ∈ 𝐴)
88	23	con3i 155	. . . . . . . . . . . 12 ⊢ (¬ 𝑦 ∈ ((𝐹 supp 0 ) “ {𝑥}) → ¬ ⟨𝑥, 𝑦⟩ ∈ (𝐹 supp 0 ))
89	88	adantl 487	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑥 ∈ dom 𝐴) ∧ 𝑦 ∈ (𝐴 “ {𝑥})) ∧ ¬ 𝑦 ∈ ((𝐹 supp 0 ) “ {𝑥})) → ¬ ⟨𝑥, 𝑦⟩ ∈ (𝐹 supp 0 ))
90	87, 89	eldifd 3910	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑥 ∈ dom 𝐴) ∧ 𝑦 ∈ (𝐴 “ {𝑥})) ∧ ¬ 𝑦 ∈ ((𝐹 supp 0 ) “ {𝑥})) → ⟨𝑥, 𝑦⟩ ∈ (𝐴 ∖ (𝐹 supp 0 )))
91	84, 85, 86, 90	fvdifsupp 8174	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑥 ∈ dom 𝐴) ∧ 𝑦 ∈ (𝐴 “ {𝑥})) ∧ ¬ 𝑦 ∈ ((𝐹 supp 0 ) “ {𝑥})) → (𝐹‘⟨𝑥, 𝑦⟩) = 0 )
92	77, 78, 81, 83, 91	syl1111anc 854	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝑥 ∈ dom 𝐴) ∧ 𝑡 ∈ (𝐴 “ {𝑥})) ∧ ¬ 𝑡 ∈ ((𝐹 supp 0 ) “ {𝑥})) ∧ 𝑦 = 𝑡) → (𝐹‘⟨𝑥, 𝑦⟩) = 0 )
93		simplr 781	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ dom 𝐴) ∧ 𝑡 ∈ (𝐴 “ {𝑥})) ∧ ¬ 𝑡 ∈ ((𝐹 supp 0 ) “ {𝑥})) → 𝑡 ∈ (𝐴 “ {𝑥}))
94	12	a1i 11	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ dom 𝐴) ∧ 𝑡 ∈ (𝐴 “ {𝑥})) ∧ ¬ 𝑡 ∈ ((𝐹 supp 0 ) “ {𝑥})) → 0 ∈ V)
95	76, 92, 93, 94	fvmptd2 6998	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑥 ∈ dom 𝐴) ∧ 𝑡 ∈ (𝐴 “ {𝑥})) ∧ ¬ 𝑡 ∈ ((𝐹 supp 0 ) “ {𝑥})) → ((𝑦 ∈ (𝐴 “ {𝑥}) ↦ (𝐹‘⟨𝑥, 𝑦⟩))‘𝑡) = 0 )
96	95	ex 418	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐴) ∧ 𝑡 ∈ (𝐴 “ {𝑥})) → (¬ 𝑡 ∈ ((𝐹 supp 0 ) “ {𝑥}) → ((𝑦 ∈ (𝐴 “ {𝑥}) ↦ (𝐹‘⟨𝑥, 𝑦⟩))‘𝑡) = 0 ))
97	96	orrd 877	. . . . 5 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐴) ∧ 𝑡 ∈ (𝐴 “ {𝑥})) → (𝑡 ∈ ((𝐹 supp 0 ) “ {𝑥}) ∨ ((𝑦 ∈ (𝐴 “ {𝑥}) ↦ (𝐹‘⟨𝑥, 𝑦⟩))‘𝑡) = 0 ))
98	71, 72, 73, 75, 97	finnzfsuppd 9350	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐴) → (𝑦 ∈ (𝐴 “ {𝑥}) ↦ (𝐹‘⟨𝑥, 𝑦⟩)) finSupp 0 )
99	1, 2, 64, 66, 70, 98	gsumcl 20068	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐴) → (𝑊 Σg (𝑦 ∈ (𝐴 “ {𝑥}) ↦ (𝐹‘⟨𝑥, 𝑦⟩))) ∈ 𝐵)
100		dmss 5888	. . . 4 ⊢ ((𝐹 supp 0 ) ⊆ 𝐴 → dom (𝐹 supp 0 ) ⊆ dom 𝐴)
101	36, 100	syl 18	. . 3 ⊢ (𝜑 → dom (𝐹 supp 0 ) ⊆ dom 𝐴)
102	1, 2, 3, 43, 61, 63, 99, 101	gsummptres2 33525	. 2 ⊢ (𝜑 → (𝑊 Σg (𝑥 ∈ dom 𝐴 ↦ (𝑊 Σg (𝑦 ∈ (𝐴 “ {𝑥}) ↦ (𝐹‘⟨𝑥, 𝑦⟩))))) = (𝑊 Σg (𝑥 ∈ dom (𝐹 supp 0 ) ↦ (𝑊 Σg (𝑦 ∈ (𝐴 “ {𝑥}) ↦ (𝐹‘⟨𝑥, 𝑦⟩))))))
103	8, 36	feqresmpt 6950	. . . 4 ⊢ (𝜑 → (𝐹 ↾ (𝐹 supp 0 )) = (𝑧 ∈ (𝐹 supp 0 ) ↦ (𝐹‘𝑧)))
104	103	oveq2d 7432	. . 3 ⊢ (𝜑 → (𝑊 Σg (𝐹 ↾ (𝐹 supp 0 ))) = (𝑊 Σg (𝑧 ∈ (𝐹 supp 0 ) ↦ (𝐹‘𝑧))))
105		ssidd 3954	. . . 4 ⊢ (𝜑 → (𝐹 supp 0 ) ⊆ (𝐹 supp 0 ))
106	1, 2, 3, 5, 8, 105, 27	gsumres 20066	. . 3 ⊢ (𝜑 → (𝑊 Σg (𝐹 ↾ (𝐹 supp 0 ))) = (𝑊 Σg 𝐹))
107		nfcv 2922	. . . 4 ⊢ Ⅎ𝑦(𝐹‘𝑧)
108		gsumfs2d.p	. . . 4 ⊢ Ⅎ𝑥𝜑
109		fveq2 6881	. . . 4 ⊢ (𝑧 = ⟨𝑥, 𝑦⟩ → (𝐹‘𝑧) = (𝐹‘⟨𝑥, 𝑦⟩))
110		gsumfs2d.r	. . . . 5 ⊢ (𝜑 → Rel 𝐴)
111		relss 5762	. . . . 5 ⊢ ((𝐹 supp 0 ) ⊆ 𝐴 → (Rel 𝐴 → Rel (𝐹 supp 0 )))
112	36, 110, 111	sylc 66	. . . 4 ⊢ (𝜑 → Rel (𝐹 supp 0 ))
113	8	adantr 486	. . . . 5 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝐹 supp 0 )) → 𝐹:𝐴⟶𝐵)
114	36	sselda 3931	. . . . 5 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝐹 supp 0 )) → 𝑧 ∈ 𝐴)
115	113, 114	ffvelcdmd 7081	. . . 4 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝐹 supp 0 )) → (𝐹‘𝑧) ∈ 𝐵)
116	107, 108, 1, 109, 112, 28, 3, 115	gsummpt2d 33521	. . 3 ⊢ (𝜑 → (𝑊 Σg (𝑧 ∈ (𝐹 supp 0 ) ↦ (𝐹‘𝑧))) = (𝑊 Σg (𝑥 ∈ dom (𝐹 supp 0 ) ↦ (𝑊 Σg (𝑦 ∈ ((𝐹 supp 0 ) “ {𝑥}) ↦ (𝐹‘⟨𝑥, 𝑦⟩))))))
117	104, 106, 116	3eqtr3d 2803	. 2 ⊢ (𝜑 → (𝑊 Σg 𝐹) = (𝑊 Σg (𝑥 ∈ dom (𝐹 supp 0 ) ↦ (𝑊 Σg (𝑦 ∈ ((𝐹 supp 0 ) “ {𝑥}) ↦ (𝐹‘⟨𝑥, 𝑦⟩))))))
118	42, 102, 117	3eqtr4rd 2806	1 ⊢ (𝜑 → (𝑊 Σg 𝐹) = (𝑊 Σg (𝑥 ∈ dom 𝐴 ↦ (𝑊 Σg (𝑦 ∈ (𝐴 “ {𝑥}) ↦ (𝐹‘⟨𝑥, 𝑦⟩))))))

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ∧ wa 401   = wceq 1570  Ⅎwnf 1816   ∈ wcel 2145  Vcvv 3450   ∖ cdif 3896   ⊆ wss 3899  {csn 4584  ⟨cop 4590   class class class wbr 5103   ↦ cmpt 5186  dom cdm 5655   ↾ cres 5657   “ cima 5658  Rel wrel 5660   Fn wfn 6530  ⟶wf 6531  ‘cfv 6535  (class class class)co 7416   supp csupp 8163  Fincfn 8959   finSupp cfsupp 9338  Basecbs 17326  0_gc0g 17549   Σ_g cgsu 17550  Mndcmnd 18862  CMndccmn 19933

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2732  ax-rep 5232  ax-sep 5251  ax-nul 5263  ax-pow 5330  ax-pr 5398  ax-un 7742  ax-cnex 11205  ax-resscn 11206  ax-1cn 11207  ax-icn 11208  ax-addcl 11209  ax-addrcl 11210  ax-mulcl 11211  ax-mulrcl 11212  ax-mulcom 11213  ax-addass 11214  ax-mulass 11215  ax-distr 11216  ax-i2m1 11217  ax-1ne0 11218  ax-1rid 11219  ax-rnegex 11220  ax-rrecex 11221  ax-cnre 11222  ax-pre-lttri 11223  ax-pre-lttrn 11224  ax-pre-ltadd 11225  ax-pre-mulgt0 11226

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-nel 3062  df-ral 3077  df-rex 3087  df-rmo 3365  df-reu 3366  df-rab 3413  df-v 3452  df-sbc 3740  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-pss 3919  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-int 4908  df-iun 4953  df-iin 4954  df-br 5104  df-opab 5168  df-mpt 5187  df-tr 5213  df-id 5550  df-eprel 5555  df-po 5563  df-so 5564  df-fr 5608  df-se 5609  df-we 5610  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-res 5667  df-ima 5668  df-pred 6301  df-ord 6362  df-on 6363  df-lim 6364  df-suc 6365  df-iota 6491  df-fun 6537  df-fn 6538  df-f 6539  df-f1 6540  df-fo 6541  df-f1o 6542  df-fv 6543  df-isom 6544  df-riota 7373  df-ov 7419  df-oprab 7420  df-mpo 7421  df-of 7684  df-om 7869  df-1st 7992  df-2nd 7993  df-supp 8164  df-frecs 8285  df-wrecs 8316  df-recs 8365  df-rdg 8404  df-1o 8462  df-2o 8463  df-er 8703  df-en 8960  df-dom 8961  df-sdom 8962  df-fin 8963  df-fsupp 9339  df-oi 9489  df-card 9969  df-pnf 11294  df-mnf 11295  df-xr 11296  df-ltxr 11297  df-le 11298  df-sub 11492  df-neg 11493  df-nn 12283  df-2 12352  df-n0 12554  df-z 12641  df-uz 12913  df-fz 13587  df-fzo 13735  df-seq 14091  df-hash 14420  df-sets 17281  df-slot 17299  df-ndx 17311  df-base 17327  df-ress 17348  df-plusg 17380  df-0g 17551  df-gsum 17552  df-mre 17695  df-mrc 17696  df-acs 17698  df-mgm 18755  df-sgrp 18847  df-mnd 18863  df-submnd 18918  df-mulg 19217  df-cntz 19470  df-cmn 19935

This theorem is used by:  gsumwrd2dccat  33550