Theorem gsumfs2d 32995

Description: Express a finite sum over a two-dimensional range as a double sum. Version of gsum2d 19951 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 480	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ dom (𝐹 supp 0 )) → 𝑊 ∈ CMnd)
5		gsumfs2d.a	. . . . . . 7 ⊢ (𝜑 → 𝐴 ∈ 𝑋)
6	5	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ dom (𝐹 supp 0 )) → 𝐴 ∈ 𝑋)
7	6	imaexd 7910	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ dom (𝐹 supp 0 )) → (𝐴 “ {𝑥}) ∈ V)
8		gsumfs2d.3	. . . . . . . 8 ⊢ (𝜑 → 𝐹:𝐴⟶𝐵)
9	8	ffnd 6706	. . . . . . 7 ⊢ (𝜑 → 𝐹 Fn 𝐴)
10	9	ad2antrr 726	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ dom (𝐹 supp 0 )) ∧ 𝑦 ∈ ((𝐴 “ {𝑥}) ∖ ((𝐹 supp 0 ) “ {𝑥}))) → 𝐹 Fn 𝐴)
11	5	ad2antrr 726	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ dom (𝐹 supp 0 )) ∧ 𝑦 ∈ ((𝐴 “ {𝑥}) ∖ ((𝐹 supp 0 ) “ {𝑥}))) → 𝐴 ∈ 𝑋)
12	2	fvexi 6889	. . . . . . 7 ⊢ 0 ∈ V
13	12	a1i 11	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ dom (𝐹 supp 0 )) ∧ 𝑦 ∈ ((𝐴 “ {𝑥}) ∖ ((𝐹 supp 0 ) “ {𝑥}))) → 0 ∈ V)
14		simpr 484	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ dom (𝐹 supp 0 )) ∧ 𝑦 ∈ ((𝐴 “ {𝑥}) ∖ ((𝐹 supp 0 ) “ {𝑥}))) → 𝑦 ∈ ((𝐴 “ {𝑥}) ∖ ((𝐹 supp 0 ) “ {𝑥})))
15	14	eldifad 3938	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ dom (𝐹 supp 0 )) ∧ 𝑦 ∈ ((𝐴 “ {𝑥}) ∖ ((𝐹 supp 0 ) “ {𝑥}))) → 𝑦 ∈ (𝐴 “ {𝑥}))
16		vex 3463	. . . . . . . . . 10 ⊢ 𝑥 ∈ V
17		vex 3463	. . . . . . . . . 10 ⊢ 𝑦 ∈ V
18	16, 17	elimasn 6077	. . . . . . . . 9 ⊢ (𝑦 ∈ (𝐴 “ {𝑥}) ↔ ⟨𝑥, 𝑦⟩ ∈ 𝐴)
19	18	biimpi 216	. . . . . . . 8 ⊢ (𝑦 ∈ (𝐴 “ {𝑥}) → ⟨𝑥, 𝑦⟩ ∈ 𝐴)
20	15, 19	syl 17	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ dom (𝐹 supp 0 )) ∧ 𝑦 ∈ ((𝐴 “ {𝑥}) ∖ ((𝐹 supp 0 ) “ {𝑥}))) → ⟨𝑥, 𝑦⟩ ∈ 𝐴)
21	14	eldifbd 3939	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ dom (𝐹 supp 0 )) ∧ 𝑦 ∈ ((𝐴 “ {𝑥}) ∖ ((𝐹 supp 0 ) “ {𝑥}))) → ¬ 𝑦 ∈ ((𝐹 supp 0 ) “ {𝑥}))
22	16, 17	elimasn 6077	. . . . . . . . 9 ⊢ (𝑦 ∈ ((𝐹 supp 0 ) “ {𝑥}) ↔ ⟨𝑥, 𝑦⟩ ∈ (𝐹 supp 0 ))
23	22	biimpri 228	. . . . . . . 8 ⊢ (⟨𝑥, 𝑦⟩ ∈ (𝐹 supp 0 ) → 𝑦 ∈ ((𝐹 supp 0 ) “ {𝑥}))
24	21, 23	nsyl 140	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ dom (𝐹 supp 0 )) ∧ 𝑦 ∈ ((𝐴 “ {𝑥}) ∖ ((𝐹 supp 0 ) “ {𝑥}))) → ¬ ⟨𝑥, 𝑦⟩ ∈ (𝐹 supp 0 ))
25	20, 24	eldifd 3937	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ dom (𝐹 supp 0 )) ∧ 𝑦 ∈ ((𝐴 “ {𝑥}) ∖ ((𝐹 supp 0 ) “ {𝑥}))) → ⟨𝑥, 𝑦⟩ ∈ (𝐴 ∖ (𝐹 supp 0 )))
26	10, 11, 13, 25	fvdifsupp 8168	. . . . 5 ⊢ (((𝜑 ∧ 𝑥 ∈ dom (𝐹 supp 0 )) ∧ 𝑦 ∈ ((𝐴 “ {𝑥}) ∖ ((𝐹 supp 0 ) “ {𝑥}))) → (𝐹‘⟨𝑥, 𝑦⟩) = 0 )
27		gsumfs2d.2	. . . . . . . 8 ⊢ (𝜑 → 𝐹 finSupp 0 )
28	27	fsuppimpd 9379	. . . . . . 7 ⊢ (𝜑 → (𝐹 supp 0 ) ∈ Fin)
29	28	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ dom (𝐹 supp 0 )) → (𝐹 supp 0 ) ∈ Fin)
30		imafi2 32635	. . . . . 6 ⊢ ((𝐹 supp 0 ) ∈ Fin → ((𝐹 supp 0 ) “ {𝑥}) ∈ Fin)
31	29, 30	syl 17	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ dom (𝐹 supp 0 )) → ((𝐹 supp 0 ) “ {𝑥}) ∈ Fin)
32	8	ad2antrr 726	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ dom (𝐹 supp 0 )) ∧ 𝑦 ∈ (𝐴 “ {𝑥})) → 𝐹:𝐴⟶𝐵)
33	19	adantl 481	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ dom (𝐹 supp 0 )) ∧ 𝑦 ∈ (𝐴 “ {𝑥})) → ⟨𝑥, 𝑦⟩ ∈ 𝐴)
34	32, 33	ffvelcdmd 7074	. . . . 5 ⊢ (((𝜑 ∧ 𝑥 ∈ dom (𝐹 supp 0 )) ∧ 𝑦 ∈ (𝐴 “ {𝑥})) → (𝐹‘⟨𝑥, 𝑦⟩) ∈ 𝐵)
35		suppssdm 8174	. . . . . . . 8 ⊢ (𝐹 supp 0 ) ⊆ dom 𝐹
36	35, 8	fssdm 6724	. . . . . . 7 ⊢ (𝜑 → (𝐹 supp 0 ) ⊆ 𝐴)
37	36	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ dom (𝐹 supp 0 )) → (𝐹 supp 0 ) ⊆ 𝐴)
38		imass1 6088	. . . . . 6 ⊢ ((𝐹 supp 0 ) ⊆ 𝐴 → ((𝐹 supp 0 ) “ {𝑥}) ⊆ (𝐴 “ {𝑥}))
39	37, 38	syl 17	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ dom (𝐹 supp 0 )) → ((𝐹 supp 0 ) “ {𝑥}) ⊆ (𝐴 “ {𝑥}))
40	1, 2, 4, 7, 26, 31, 34, 39	gsummptres2 32993	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ dom (𝐹 supp 0 )) → (𝑊 Σg (𝑦 ∈ (𝐴 “ {𝑥}) ↦ (𝐹‘⟨𝑥, 𝑦⟩))) = (𝑊 Σg (𝑦 ∈ ((𝐹 supp 0 ) “ {𝑥}) ↦ (𝐹‘⟨𝑥, 𝑦⟩))))
41	40	mpteq2dva 5214	. . 3 ⊢ (𝜑 → (𝑥 ∈ dom (𝐹 supp 0 ) ↦ (𝑊 Σg (𝑦 ∈ (𝐴 “ {𝑥}) ↦ (𝐹‘⟨𝑥, 𝑦⟩)))) = (𝑥 ∈ dom (𝐹 supp 0 ) ↦ (𝑊 Σg (𝑦 ∈ ((𝐹 supp 0 ) “ {𝑥}) ↦ (𝐹‘⟨𝑥, 𝑦⟩)))))
42	41	oveq2d 7419	. 2 ⊢ (𝜑 → (𝑊 Σg (𝑥 ∈ dom (𝐹 supp 0 ) ↦ (𝑊 Σg (𝑦 ∈ (𝐴 “ {𝑥}) ↦ (𝐹‘⟨𝑥, 𝑦⟩))))) = (𝑊 Σg (𝑥 ∈ dom (𝐹 supp 0 ) ↦ (𝑊 Σg (𝑦 ∈ ((𝐹 supp 0 ) “ {𝑥}) ↦ (𝐹‘⟨𝑥, 𝑦⟩))))))
43	5	dmexd 7897	. . 3 ⊢ (𝜑 → dom 𝐴 ∈ V)
44	9	ad2antrr 726	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ (dom 𝐴 ∖ dom (𝐹 supp 0 ))) ∧ 𝑦 ∈ (𝐴 “ {𝑥})) → 𝐹 Fn 𝐴)
45	5	ad2antrr 726	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ (dom 𝐴 ∖ dom (𝐹 supp 0 ))) ∧ 𝑦 ∈ (𝐴 “ {𝑥})) → 𝐴 ∈ 𝑋)
46	12	a1i 11	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ (dom 𝐴 ∖ dom (𝐹 supp 0 ))) ∧ 𝑦 ∈ (𝐴 “ {𝑥})) → 0 ∈ V)
47	19	adantl 481	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ (dom 𝐴 ∖ dom (𝐹 supp 0 ))) ∧ 𝑦 ∈ (𝐴 “ {𝑥})) → ⟨𝑥, 𝑦⟩ ∈ 𝐴)
48		simplr 768	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ (dom 𝐴 ∖ dom (𝐹 supp 0 ))) ∧ 𝑦 ∈ (𝐴 “ {𝑥})) → 𝑥 ∈ (dom 𝐴 ∖ dom (𝐹 supp 0 )))
49	48	eldifbd 3939	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ (dom 𝐴 ∖ dom (𝐹 supp 0 ))) ∧ 𝑦 ∈ (𝐴 “ {𝑥})) → ¬ 𝑥 ∈ dom (𝐹 supp 0 ))
50	16, 17	opeldm 5887	. . . . . . . . 9 ⊢ (⟨𝑥, 𝑦⟩ ∈ (𝐹 supp 0 ) → 𝑥 ∈ dom (𝐹 supp 0 ))
51	49, 50	nsyl 140	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ (dom 𝐴 ∖ dom (𝐹 supp 0 ))) ∧ 𝑦 ∈ (𝐴 “ {𝑥})) → ¬ ⟨𝑥, 𝑦⟩ ∈ (𝐹 supp 0 ))
52	47, 51	eldifd 3937	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ (dom 𝐴 ∖ dom (𝐹 supp 0 ))) ∧ 𝑦 ∈ (𝐴 “ {𝑥})) → ⟨𝑥, 𝑦⟩ ∈ (𝐴 ∖ (𝐹 supp 0 )))
53	44, 45, 46, 52	fvdifsupp 8168	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ (dom 𝐴 ∖ dom (𝐹 supp 0 ))) ∧ 𝑦 ∈ (𝐴 “ {𝑥})) → (𝐹‘⟨𝑥, 𝑦⟩) = 0 )
54	53	mpteq2dva 5214	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ (dom 𝐴 ∖ dom (𝐹 supp 0 ))) → (𝑦 ∈ (𝐴 “ {𝑥}) ↦ (𝐹‘⟨𝑥, 𝑦⟩)) = (𝑦 ∈ (𝐴 “ {𝑥}) ↦ 0 ))
55	54	oveq2d 7419	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ (dom 𝐴 ∖ dom (𝐹 supp 0 ))) → (𝑊 Σg (𝑦 ∈ (𝐴 “ {𝑥}) ↦ (𝐹‘⟨𝑥, 𝑦⟩))) = (𝑊 Σg (𝑦 ∈ (𝐴 “ {𝑥}) ↦ 0 )))
56	3	cmnmndd 19783	. . . . 5 ⊢ (𝜑 → 𝑊 ∈ Mnd)
57	5	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (dom 𝐴 ∖ dom (𝐹 supp 0 ))) → 𝐴 ∈ 𝑋)
58	57	imaexd 7910	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ (dom 𝐴 ∖ dom (𝐹 supp 0 ))) → (𝐴 “ {𝑥}) ∈ V)
59	2	gsumz 18812	. . . . 5 ⊢ ((𝑊 ∈ Mnd ∧ (𝐴 “ {𝑥}) ∈ V) → (𝑊 Σg (𝑦 ∈ (𝐴 “ {𝑥}) ↦ 0 )) = 0 )
60	56, 58, 59	syl2an2r 685	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ (dom 𝐴 ∖ dom (𝐹 supp 0 ))) → (𝑊 Σg (𝑦 ∈ (𝐴 “ {𝑥}) ↦ 0 )) = 0 )
61	55, 60	eqtrd 2770	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ (dom 𝐴 ∖ dom (𝐹 supp 0 ))) → (𝑊 Σg (𝑦 ∈ (𝐴 “ {𝑥}) ↦ (𝐹‘⟨𝑥, 𝑦⟩))) = 0 )
62		dmfi 9345	. . . 4 ⊢ ((𝐹 supp 0 ) ∈ Fin → dom (𝐹 supp 0 ) ∈ Fin)
63	28, 62	syl 17	. . 3 ⊢ (𝜑 → dom (𝐹 supp 0 ) ∈ Fin)
64	3	adantr 480	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐴) → 𝑊 ∈ CMnd)
65	5	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐴) → 𝐴 ∈ 𝑋)
66	65	imaexd 7910	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐴) → (𝐴 “ {𝑥}) ∈ V)
67	8	ad2antrr 726	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐴) ∧ 𝑦 ∈ (𝐴 “ {𝑥})) → 𝐹:𝐴⟶𝐵)
68	19	adantl 481	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐴) ∧ 𝑦 ∈ (𝐴 “ {𝑥})) → ⟨𝑥, 𝑦⟩ ∈ 𝐴)
69	67, 68	ffvelcdmd 7074	. . . . 5 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐴) ∧ 𝑦 ∈ (𝐴 “ {𝑥})) → (𝐹‘⟨𝑥, 𝑦⟩) ∈ 𝐵)
70	69	fmpttd 7104	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐴) → (𝑦 ∈ (𝐴 “ {𝑥}) ↦ (𝐹‘⟨𝑥, 𝑦⟩)):(𝐴 “ {𝑥})⟶𝐵)
71	66	mptexd 7215	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐴) → (𝑦 ∈ (𝐴 “ {𝑥}) ↦ (𝐹‘⟨𝑥, 𝑦⟩)) ∈ V)
72	70	ffnd 6706	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐴) → (𝑦 ∈ (𝐴 “ {𝑥}) ↦ (𝐹‘⟨𝑥, 𝑦⟩)) Fn (𝐴 “ {𝑥}))
73	12	a1i 11	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐴) → 0 ∈ V)
74	28	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐴) → (𝐹 supp 0 ) ∈ Fin)
75	74, 30	syl 17	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐴) → ((𝐹 supp 0 ) “ {𝑥}) ∈ Fin)
76		eqid 2735	. . . . . . . 8 ⊢ (𝑦 ∈ (𝐴 “ {𝑥}) ↦ (𝐹‘⟨𝑥, 𝑦⟩)) = (𝑦 ∈ (𝐴 “ {𝑥}) ↦ (𝐹‘⟨𝑥, 𝑦⟩))
77		simp-4l 782	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑥 ∈ dom 𝐴) ∧ 𝑡 ∈ (𝐴 “ {𝑥})) ∧ ¬ 𝑡 ∈ ((𝐹 supp 0 ) “ {𝑥})) ∧ 𝑦 = 𝑡) → 𝜑)
78		simp-4r 783	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑥 ∈ dom 𝐴) ∧ 𝑡 ∈ (𝐴 “ {𝑥})) ∧ ¬ 𝑡 ∈ ((𝐹 supp 0 ) “ {𝑥})) ∧ 𝑦 = 𝑡) → 𝑥 ∈ dom 𝐴)
79		simpr 484	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑥 ∈ dom 𝐴) ∧ 𝑡 ∈ (𝐴 “ {𝑥})) ∧ ¬ 𝑡 ∈ ((𝐹 supp 0 ) “ {𝑥})) ∧ 𝑦 = 𝑡) → 𝑦 = 𝑡)
80		simpllr 775	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑥 ∈ dom 𝐴) ∧ 𝑡 ∈ (𝐴 “ {𝑥})) ∧ ¬ 𝑡 ∈ ((𝐹 supp 0 ) “ {𝑥})) ∧ 𝑦 = 𝑡) → 𝑡 ∈ (𝐴 “ {𝑥}))
81	79, 80	eqeltrd 2834	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑥 ∈ dom 𝐴) ∧ 𝑡 ∈ (𝐴 “ {𝑥})) ∧ ¬ 𝑡 ∈ ((𝐹 supp 0 ) “ {𝑥})) ∧ 𝑦 = 𝑡) → 𝑦 ∈ (𝐴 “ {𝑥}))
82		simplr 768	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑥 ∈ dom 𝐴) ∧ 𝑡 ∈ (𝐴 “ {𝑥})) ∧ ¬ 𝑡 ∈ ((𝐹 supp 0 ) “ {𝑥})) ∧ 𝑦 = 𝑡) → ¬ 𝑡 ∈ ((𝐹 supp 0 ) “ {𝑥}))
83	79, 82	eqneltrd 2854	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑥 ∈ dom 𝐴) ∧ 𝑡 ∈ (𝐴 “ {𝑥})) ∧ ¬ 𝑡 ∈ ((𝐹 supp 0 ) “ {𝑥})) ∧ 𝑦 = 𝑡) → ¬ 𝑦 ∈ ((𝐹 supp 0 ) “ {𝑥}))
84	9	ad3antrrr 730	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑥 ∈ dom 𝐴) ∧ 𝑦 ∈ (𝐴 “ {𝑥})) ∧ ¬ 𝑦 ∈ ((𝐹 supp 0 ) “ {𝑥})) → 𝐹 Fn 𝐴)
85	5	ad3antrrr 730	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑥 ∈ dom 𝐴) ∧ 𝑦 ∈ (𝐴 “ {𝑥})) ∧ ¬ 𝑦 ∈ ((𝐹 supp 0 ) “ {𝑥})) → 𝐴 ∈ 𝑋)
86	12	a1i 11	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑥 ∈ dom 𝐴) ∧ 𝑦 ∈ (𝐴 “ {𝑥})) ∧ ¬ 𝑦 ∈ ((𝐹 supp 0 ) “ {𝑥})) → 0 ∈ V)
87	68	adantr 480	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑥 ∈ dom 𝐴) ∧ 𝑦 ∈ (𝐴 “ {𝑥})) ∧ ¬ 𝑦 ∈ ((𝐹 supp 0 ) “ {𝑥})) → ⟨𝑥, 𝑦⟩ ∈ 𝐴)
88	23	con3i 154	. . . . . . . . . . . 12 ⊢ (¬ 𝑦 ∈ ((𝐹 supp 0 ) “ {𝑥}) → ¬ ⟨𝑥, 𝑦⟩ ∈ (𝐹 supp 0 ))
89	88	adantl 481	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑥 ∈ dom 𝐴) ∧ 𝑦 ∈ (𝐴 “ {𝑥})) ∧ ¬ 𝑦 ∈ ((𝐹 supp 0 ) “ {𝑥})) → ¬ ⟨𝑥, 𝑦⟩ ∈ (𝐹 supp 0 ))
90	87, 89	eldifd 3937	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑥 ∈ dom 𝐴) ∧ 𝑦 ∈ (𝐴 “ {𝑥})) ∧ ¬ 𝑦 ∈ ((𝐹 supp 0 ) “ {𝑥})) → ⟨𝑥, 𝑦⟩ ∈ (𝐴 ∖ (𝐹 supp 0 )))
91	84, 85, 86, 90	fvdifsupp 8168	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑥 ∈ dom 𝐴) ∧ 𝑦 ∈ (𝐴 “ {𝑥})) ∧ ¬ 𝑦 ∈ ((𝐹 supp 0 ) “ {𝑥})) → (𝐹‘⟨𝑥, 𝑦⟩) = 0 )
92	77, 78, 81, 83, 91	syl1111anc 840	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝑥 ∈ dom 𝐴) ∧ 𝑡 ∈ (𝐴 “ {𝑥})) ∧ ¬ 𝑡 ∈ ((𝐹 supp 0 ) “ {𝑥})) ∧ 𝑦 = 𝑡) → (𝐹‘⟨𝑥, 𝑦⟩) = 0 )
93		simplr 768	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ dom 𝐴) ∧ 𝑡 ∈ (𝐴 “ {𝑥})) ∧ ¬ 𝑡 ∈ ((𝐹 supp 0 ) “ {𝑥})) → 𝑡 ∈ (𝐴 “ {𝑥}))
94	12	a1i 11	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ dom 𝐴) ∧ 𝑡 ∈ (𝐴 “ {𝑥})) ∧ ¬ 𝑡 ∈ ((𝐹 supp 0 ) “ {𝑥})) → 0 ∈ V)
95	76, 92, 93, 94	fvmptd2 6993	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑥 ∈ dom 𝐴) ∧ 𝑡 ∈ (𝐴 “ {𝑥})) ∧ ¬ 𝑡 ∈ ((𝐹 supp 0 ) “ {𝑥})) → ((𝑦 ∈ (𝐴 “ {𝑥}) ↦ (𝐹‘⟨𝑥, 𝑦⟩))‘𝑡) = 0 )
96	95	ex 412	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐴) ∧ 𝑡 ∈ (𝐴 “ {𝑥})) → (¬ 𝑡 ∈ ((𝐹 supp 0 ) “ {𝑥}) → ((𝑦 ∈ (𝐴 “ {𝑥}) ↦ (𝐹‘⟨𝑥, 𝑦⟩))‘𝑡) = 0 ))
97	96	orrd 863	. . . . 5 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐴) ∧ 𝑡 ∈ (𝐴 “ {𝑥})) → (𝑡 ∈ ((𝐹 supp 0 ) “ {𝑥}) ∨ ((𝑦 ∈ (𝐴 “ {𝑥}) ↦ (𝐹‘⟨𝑥, 𝑦⟩))‘𝑡) = 0 ))
98	71, 72, 73, 75, 97	finnzfsuppd 9383	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐴) → (𝑦 ∈ (𝐴 “ {𝑥}) ↦ (𝐹‘⟨𝑥, 𝑦⟩)) finSupp 0 )
99	1, 2, 64, 66, 70, 98	gsumcl 19894	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐴) → (𝑊 Σg (𝑦 ∈ (𝐴 “ {𝑥}) ↦ (𝐹‘⟨𝑥, 𝑦⟩))) ∈ 𝐵)
100		dmss 5882	. . . 4 ⊢ ((𝐹 supp 0 ) ⊆ 𝐴 → dom (𝐹 supp 0 ) ⊆ dom 𝐴)
101	36, 100	syl 17	. . 3 ⊢ (𝜑 → dom (𝐹 supp 0 ) ⊆ dom 𝐴)
102	1, 2, 3, 43, 61, 63, 99, 101	gsummptres2 32993	. 2 ⊢ (𝜑 → (𝑊 Σg (𝑥 ∈ dom 𝐴 ↦ (𝑊 Σg (𝑦 ∈ (𝐴 “ {𝑥}) ↦ (𝐹‘⟨𝑥, 𝑦⟩))))) = (𝑊 Σg (𝑥 ∈ dom (𝐹 supp 0 ) ↦ (𝑊 Σg (𝑦 ∈ (𝐴 “ {𝑥}) ↦ (𝐹‘⟨𝑥, 𝑦⟩))))))
103	8, 36	feqresmpt 6947	. . . 4 ⊢ (𝜑 → (𝐹 ↾ (𝐹 supp 0 )) = (𝑧 ∈ (𝐹 supp 0 ) ↦ (𝐹‘𝑧)))
104	103	oveq2d 7419	. . 3 ⊢ (𝜑 → (𝑊 Σg (𝐹 ↾ (𝐹 supp 0 ))) = (𝑊 Σg (𝑧 ∈ (𝐹 supp 0 ) ↦ (𝐹‘𝑧))))
105		ssidd 3982	. . . 4 ⊢ (𝜑 → (𝐹 supp 0 ) ⊆ (𝐹 supp 0 ))
106	1, 2, 3, 5, 8, 105, 27	gsumres 19892	. . 3 ⊢ (𝜑 → (𝑊 Σg (𝐹 ↾ (𝐹 supp 0 ))) = (𝑊 Σg 𝐹))
107		nfcv 2898	. . . 4 ⊢ Ⅎ𝑦(𝐹‘𝑧)
108		gsumfs2d.p	. . . 4 ⊢ Ⅎ𝑥𝜑
109		fveq2 6875	. . . 4 ⊢ (𝑧 = ⟨𝑥, 𝑦⟩ → (𝐹‘𝑧) = (𝐹‘⟨𝑥, 𝑦⟩))
110		gsumfs2d.r	. . . . 5 ⊢ (𝜑 → Rel 𝐴)
111		relss 5760	. . . . 5 ⊢ ((𝐹 supp 0 ) ⊆ 𝐴 → (Rel 𝐴 → Rel (𝐹 supp 0 )))
112	36, 110, 111	sylc 65	. . . 4 ⊢ (𝜑 → Rel (𝐹 supp 0 ))
113	8	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝐹 supp 0 )) → 𝐹:𝐴⟶𝐵)
114	36	sselda 3958	. . . . 5 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝐹 supp 0 )) → 𝑧 ∈ 𝐴)
115	113, 114	ffvelcdmd 7074	. . . 4 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝐹 supp 0 )) → (𝐹‘𝑧) ∈ 𝐵)
116	107, 108, 1, 109, 112, 28, 3, 115	gsummpt2d 32989	. . 3 ⊢ (𝜑 → (𝑊 Σg (𝑧 ∈ (𝐹 supp 0 ) ↦ (𝐹‘𝑧))) = (𝑊 Σg (𝑥 ∈ dom (𝐹 supp 0 ) ↦ (𝑊 Σg (𝑦 ∈ ((𝐹 supp 0 ) “ {𝑥}) ↦ (𝐹‘⟨𝑥, 𝑦⟩))))))
117	104, 106, 116	3eqtr3d 2778	. 2 ⊢ (𝜑 → (𝑊 Σg 𝐹) = (𝑊 Σg (𝑥 ∈ dom (𝐹 supp 0 ) ↦ (𝑊 Σg (𝑦 ∈ ((𝐹 supp 0 ) “ {𝑥}) ↦ (𝐹‘⟨𝑥, 𝑦⟩))))))
118	42, 102, 117	3eqtr4rd 2781	1 ⊢ (𝜑 → (𝑊 Σg 𝐹) = (𝑊 Σg (𝑥 ∈ dom 𝐴 ↦ (𝑊 Σg (𝑦 ∈ (𝐴 “ {𝑥}) ↦ (𝐹‘⟨𝑥, 𝑦⟩))))))

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 395   = wceq 1540  Ⅎwnf 1783   ∈ wcel 2108  Vcvv 3459   ∖ cdif 3923   ⊆ wss 3926  {csn 4601  ⟨cop 4607   class class class wbr 5119   ↦ cmpt 5201  dom cdm 5654   ↾ cres 5656   “ cima 5657  Rel wrel 5659   Fn wfn 6525  ⟶wf 6526  ‘cfv 6530  (class class class)co 7403   supp csupp 8157  Fincfn 8957   finSupp cfsupp 9371  Basecbs 17226  0_gc0g 17451   Σ_g cgsu 17452  Mndcmnd 18710  CMndccmn 19759

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2707  ax-rep 5249  ax-sep 5266  ax-nul 5276  ax-pow 5335  ax-pr 5402  ax-un 7727  ax-cnex 11183  ax-resscn 11184  ax-1cn 11185  ax-icn 11186  ax-addcl 11187  ax-addrcl 11188  ax-mulcl 11189  ax-mulrcl 11190  ax-mulcom 11191  ax-addass 11192  ax-mulass 11193  ax-distr 11194  ax-i2m1 11195  ax-1ne0 11196  ax-1rid 11197  ax-rnegex 11198  ax-rrecex 11199  ax-cnre 11200  ax-pre-lttri 11201  ax-pre-lttrn 11202  ax-pre-ltadd 11203  ax-pre-mulgt0 11204

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2727  df-clel 2809  df-nfc 2885  df-ne 2933  df-nel 3037  df-ral 3052  df-rex 3061  df-rmo 3359  df-reu 3360  df-rab 3416  df-v 3461  df-sbc 3766  df-csb 3875  df-dif 3929  df-un 3931  df-in 3933  df-ss 3943  df-pss 3946  df-nul 4309  df-if 4501  df-pw 4577  df-sn 4602  df-pr 4604  df-op 4608  df-uni 4884  df-int 4923  df-iun 4969  df-iin 4970  df-br 5120  df-opab 5182  df-mpt 5202  df-tr 5230  df-id 5548  df-eprel 5553  df-po 5561  df-so 5562  df-fr 5606  df-se 5607  df-we 5608  df-xp 5660  df-rel 5661  df-cnv 5662  df-co 5663  df-dm 5664  df-rn 5665  df-res 5666  df-ima 5667  df-pred 6290  df-ord 6355  df-on 6356  df-lim 6357  df-suc 6358  df-iota 6483  df-fun 6532  df-fn 6533  df-f 6534  df-f1 6535  df-fo 6536  df-f1o 6537  df-fv 6538  df-isom 6539  df-riota 7360  df-ov 7406  df-oprab 7407  df-mpo 7408  df-of 7669  df-om 7860  df-1st 7986  df-2nd 7987  df-supp 8158  df-frecs 8278  df-wrecs 8309  df-recs 8383  df-rdg 8422  df-1o 8478  df-2o 8479  df-er 8717  df-en 8958  df-dom 8959  df-sdom 8960  df-fin 8961  df-fsupp 9372  df-oi 9522  df-card 9951  df-pnf 11269  df-mnf 11270  df-xr 11271  df-ltxr 11272  df-le 11273  df-sub 11466  df-neg 11467  df-nn 12239  df-2 12301  df-n0 12500  df-z 12587  df-uz 12851  df-fz 13523  df-fzo 13670  df-seq 14018  df-hash 14347  df-sets 17181  df-slot 17199  df-ndx 17211  df-base 17227  df-ress 17250  df-plusg 17282  df-0g 17453  df-gsum 17454  df-mre 17596  df-mrc 17597  df-acs 17599  df-mgm 18616  df-sgrp 18695  df-mnd 18711  df-submnd 18760  df-mulg 19049  df-cntz 19298  df-cmn 19761

This theorem is referenced by:  gsumwrd2dccat  33007