Theorem gsumfs2d 33093

Description: Express a finite sum over a two-dimensional range as a double sum. Version of gsum2d 19899 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 7856	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ dom (𝐹 supp 0 )) → (𝐴 “ {𝑥}) ∈ V)
8		gsumfs2d.3	. . . . . . . 8 ⊢ (𝜑 → 𝐹:𝐴⟶𝐵)
9	8	ffnd 6661	. . . . . . 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 6846	. . . . . . 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 3911	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ dom (𝐹 supp 0 )) ∧ 𝑦 ∈ ((𝐴 “ {𝑥}) ∖ ((𝐹 supp 0 ) “ {𝑥}))) → 𝑦 ∈ (𝐴 “ {𝑥}))
16		vex 3442	. . . . . . . . . 10 ⊢ 𝑥 ∈ V
17		vex 3442	. . . . . . . . . 10 ⊢ 𝑦 ∈ V
18	16, 17	elimasn 6047	. . . . . . . . 9 ⊢ (𝑦 ∈ (𝐴 “ {𝑥}) ↔ ⟨𝑥, 𝑦⟩ ∈ 𝐴)
19	18	biimpi 216	. . . . . . . 8 ⊢ (𝑦 ∈ (𝐴 “ {𝑥}) → ⟨𝑥, 𝑦⟩ ∈ 𝐴)
20	15, 19	syl 17	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ dom (𝐹 supp 0 )) ∧ 𝑦 ∈ ((𝐴 “ {𝑥}) ∖ ((𝐹 supp 0 ) “ {𝑥}))) → ⟨𝑥, 𝑦⟩ ∈ 𝐴)
21	14	eldifbd 3912	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ dom (𝐹 supp 0 )) ∧ 𝑦 ∈ ((𝐴 “ {𝑥}) ∖ ((𝐹 supp 0 ) “ {𝑥}))) → ¬ 𝑦 ∈ ((𝐹 supp 0 ) “ {𝑥}))
22	16, 17	elimasn 6047	. . . . . . . . 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 3910	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ dom (𝐹 supp 0 )) ∧ 𝑦 ∈ ((𝐴 “ {𝑥}) ∖ ((𝐹 supp 0 ) “ {𝑥}))) → ⟨𝑥, 𝑦⟩ ∈ (𝐴 ∖ (𝐹 supp 0 )))
26	10, 11, 13, 25	fvdifsupp 8111	. . . . 5 ⊢ (((𝜑 ∧ 𝑥 ∈ dom (𝐹 supp 0 )) ∧ 𝑦 ∈ ((𝐴 “ {𝑥}) ∖ ((𝐹 supp 0 ) “ {𝑥}))) → (𝐹‘⟨𝑥, 𝑦⟩) = 0 )
27		gsumfs2d.2	. . . . . . . 8 ⊢ (𝜑 → 𝐹 finSupp 0 )
28	27	fsuppimpd 9270	. . . . . . 7 ⊢ (𝜑 → (𝐹 supp 0 ) ∈ Fin)
29	28	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ dom (𝐹 supp 0 )) → (𝐹 supp 0 ) ∈ Fin)
30		imafi2 9259	. . . . . 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 7028	. . . . 5 ⊢ (((𝜑 ∧ 𝑥 ∈ dom (𝐹 supp 0 )) ∧ 𝑦 ∈ (𝐴 “ {𝑥})) → (𝐹‘⟨𝑥, 𝑦⟩) ∈ 𝐵)
35		suppssdm 8117	. . . . . . . 8 ⊢ (𝐹 supp 0 ) ⊆ dom 𝐹
36	35, 8	fssdm 6679	. . . . . . 7 ⊢ (𝜑 → (𝐹 supp 0 ) ⊆ 𝐴)
37	36	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ dom (𝐹 supp 0 )) → (𝐹 supp 0 ) ⊆ 𝐴)
38		imass1 6058	. . . . . 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 33085	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ dom (𝐹 supp 0 )) → (𝑊 Σg (𝑦 ∈ (𝐴 “ {𝑥}) ↦ (𝐹‘⟨𝑥, 𝑦⟩))) = (𝑊 Σg (𝑦 ∈ ((𝐹 supp 0 ) “ {𝑥}) ↦ (𝐹‘⟨𝑥, 𝑦⟩))))
41	40	mpteq2dva 5189	. . 3 ⊢ (𝜑 → (𝑥 ∈ dom (𝐹 supp 0 ) ↦ (𝑊 Σg (𝑦 ∈ (𝐴 “ {𝑥}) ↦ (𝐹‘⟨𝑥, 𝑦⟩)))) = (𝑥 ∈ dom (𝐹 supp 0 ) ↦ (𝑊 Σg (𝑦 ∈ ((𝐹 supp 0 ) “ {𝑥}) ↦ (𝐹‘⟨𝑥, 𝑦⟩)))))
42	41	oveq2d 7372	. 2 ⊢ (𝜑 → (𝑊 Σg (𝑥 ∈ dom (𝐹 supp 0 ) ↦ (𝑊 Σg (𝑦 ∈ (𝐴 “ {𝑥}) ↦ (𝐹‘⟨𝑥, 𝑦⟩))))) = (𝑊 Σg (𝑥 ∈ dom (𝐹 supp 0 ) ↦ (𝑊 Σg (𝑦 ∈ ((𝐹 supp 0 ) “ {𝑥}) ↦ (𝐹‘⟨𝑥, 𝑦⟩))))))
43	5	dmexd 7843	. . 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 3912	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ (dom 𝐴 ∖ dom (𝐹 supp 0 ))) ∧ 𝑦 ∈ (𝐴 “ {𝑥})) → ¬ 𝑥 ∈ dom (𝐹 supp 0 ))
50	16, 17	opeldm 5854	. . . . . . . . 9 ⊢ (⟨𝑥, 𝑦⟩ ∈ (𝐹 supp 0 ) → 𝑥 ∈ dom (𝐹 supp 0 ))
51	49, 50	nsyl 140	. . . . . . . 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 8111	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ (dom 𝐴 ∖ dom (𝐹 supp 0 ))) ∧ 𝑦 ∈ (𝐴 “ {𝑥})) → (𝐹‘⟨𝑥, 𝑦⟩) = 0 )
54	53	mpteq2dva 5189	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ (dom 𝐴 ∖ dom (𝐹 supp 0 ))) → (𝑦 ∈ (𝐴 “ {𝑥}) ↦ (𝐹‘⟨𝑥, 𝑦⟩)) = (𝑦 ∈ (𝐴 “ {𝑥}) ↦ 0 ))
55	54	oveq2d 7372	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ (dom 𝐴 ∖ dom (𝐹 supp 0 ))) → (𝑊 Σg (𝑦 ∈ (𝐴 “ {𝑥}) ↦ (𝐹‘⟨𝑥, 𝑦⟩))) = (𝑊 Σg (𝑦 ∈ (𝐴 “ {𝑥}) ↦ 0 )))
56	3	cmnmndd 19731	. . . . 5 ⊢ (𝜑 → 𝑊 ∈ Mnd)
57	5	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (dom 𝐴 ∖ dom (𝐹 supp 0 ))) → 𝐴 ∈ 𝑋)
58	57	imaexd 7856	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ (dom 𝐴 ∖ dom (𝐹 supp 0 ))) → (𝐴 “ {𝑥}) ∈ V)
59	2	gsumz 18759	. . . . 5 ⊢ ((𝑊 ∈ Mnd ∧ (𝐴 “ {𝑥}) ∈ V) → (𝑊 Σg (𝑦 ∈ (𝐴 “ {𝑥}) ↦ 0 )) = 0 )
60	56, 58, 59	syl2an2r 685	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ (dom 𝐴 ∖ dom (𝐹 supp 0 ))) → (𝑊 Σg (𝑦 ∈ (𝐴 “ {𝑥}) ↦ 0 )) = 0 )
61	55, 60	eqtrd 2769	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ (dom 𝐴 ∖ dom (𝐹 supp 0 ))) → (𝑊 Σg (𝑦 ∈ (𝐴 “ {𝑥}) ↦ (𝐹‘⟨𝑥, 𝑦⟩))) = 0 )
62		dmfi 9233	. . . 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 7856	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐴) → (𝐴 “ {𝑥}) ∈ V)
67	8	ad2antrr 726	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐴) ∧ 𝑦 ∈ (𝐴 “ {𝑥})) → 𝐹:𝐴⟶𝐵)
68	19	adantl 481	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐴) ∧ 𝑦 ∈ (𝐴 “ {𝑥})) → ⟨𝑥, 𝑦⟩ ∈ 𝐴)
69	67, 68	ffvelcdmd 7028	. . . . 5 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐴) ∧ 𝑦 ∈ (𝐴 “ {𝑥})) → (𝐹‘⟨𝑥, 𝑦⟩) ∈ 𝐵)
70	69	fmpttd 7058	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐴) → (𝑦 ∈ (𝐴 “ {𝑥}) ↦ (𝐹‘⟨𝑥, 𝑦⟩)):(𝐴 “ {𝑥})⟶𝐵)
71	66	mptexd 7168	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐴) → (𝑦 ∈ (𝐴 “ {𝑥}) ↦ (𝐹‘⟨𝑥, 𝑦⟩)) ∈ V)
72	70	ffnd 6661	. . . . 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 2734	. . . . . . . 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 3910	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑥 ∈ dom 𝐴) ∧ 𝑦 ∈ (𝐴 “ {𝑥})) ∧ ¬ 𝑦 ∈ ((𝐹 supp 0 ) “ {𝑥})) → ⟨𝑥, 𝑦⟩ ∈ (𝐴 ∖ (𝐹 supp 0 )))
91	84, 85, 86, 90	fvdifsupp 8111	. . . . . . . . 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 6947	. . . . . . 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 9274	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐴) → (𝑦 ∈ (𝐴 “ {𝑥}) ↦ (𝐹‘⟨𝑥, 𝑦⟩)) finSupp 0 )
99	1, 2, 64, 66, 70, 98	gsumcl 19842	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐴) → (𝑊 Σg (𝑦 ∈ (𝐴 “ {𝑥}) ↦ (𝐹‘⟨𝑥, 𝑦⟩))) ∈ 𝐵)
100		dmss 5849	. . . 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 33085	. 2 ⊢ (𝜑 → (𝑊 Σg (𝑥 ∈ dom 𝐴 ↦ (𝑊 Σg (𝑦 ∈ (𝐴 “ {𝑥}) ↦ (𝐹‘⟨𝑥, 𝑦⟩))))) = (𝑊 Σg (𝑥 ∈ dom (𝐹 supp 0 ) ↦ (𝑊 Σg (𝑦 ∈ (𝐴 “ {𝑥}) ↦ (𝐹‘⟨𝑥, 𝑦⟩))))))
103	8, 36	feqresmpt 6901	. . . 4 ⊢ (𝜑 → (𝐹 ↾ (𝐹 supp 0 )) = (𝑧 ∈ (𝐹 supp 0 ) ↦ (𝐹‘𝑧)))
104	103	oveq2d 7372	. . 3 ⊢ (𝜑 → (𝑊 Σg (𝐹 ↾ (𝐹 supp 0 ))) = (𝑊 Σg (𝑧 ∈ (𝐹 supp 0 ) ↦ (𝐹‘𝑧))))
105		ssidd 3955	. . . 4 ⊢ (𝜑 → (𝐹 supp 0 ) ⊆ (𝐹 supp 0 ))
106	1, 2, 3, 5, 8, 105, 27	gsumres 19840	. . 3 ⊢ (𝜑 → (𝑊 Σg (𝐹 ↾ (𝐹 supp 0 ))) = (𝑊 Σg 𝐹))
107		nfcv 2896	. . . 4 ⊢ Ⅎ𝑦(𝐹‘𝑧)
108		gsumfs2d.p	. . . 4 ⊢ Ⅎ𝑥𝜑
109		fveq2 6832	. . . 4 ⊢ (𝑧 = ⟨𝑥, 𝑦⟩ → (𝐹‘𝑧) = (𝐹‘⟨𝑥, 𝑦⟩))
110		gsumfs2d.r	. . . . 5 ⊢ (𝜑 → Rel 𝐴)
111		relss 5729	. . . . 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 3931	. . . . 5 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝐹 supp 0 )) → 𝑧 ∈ 𝐴)
115	113, 114	ffvelcdmd 7028	. . . 4 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝐹 supp 0 )) → (𝐹‘𝑧) ∈ 𝐵)
116	107, 108, 1, 109, 112, 28, 3, 115	gsummpt2d 33081	. . 3 ⊢ (𝜑 → (𝑊 Σg (𝑧 ∈ (𝐹 supp 0 ) ↦ (𝐹‘𝑧))) = (𝑊 Σg (𝑥 ∈ dom (𝐹 supp 0 ) ↦ (𝑊 Σg (𝑦 ∈ ((𝐹 supp 0 ) “ {𝑥}) ↦ (𝐹‘⟨𝑥, 𝑦⟩))))))
117	104, 106, 116	3eqtr3d 2777	. 2 ⊢ (𝜑 → (𝑊 Σg 𝐹) = (𝑊 Σg (𝑥 ∈ dom (𝐹 supp 0 ) ↦ (𝑊 Σg (𝑦 ∈ ((𝐹 supp 0 ) “ {𝑥}) ↦ (𝐹‘⟨𝑥, 𝑦⟩))))))
118	42, 102, 117	3eqtr4rd 2780	1 ⊢ (𝜑 → (𝑊 Σg 𝐹) = (𝑊 Σg (𝑥 ∈ dom 𝐴 ↦ (𝑊 Σg (𝑦 ∈ (𝐴 “ {𝑥}) ↦ (𝐹‘⟨𝑥, 𝑦⟩))))))

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 395   = wceq 1541  Ⅎwnf 1784   ∈ wcel 2113  Vcvv 3438   ∖ cdif 3896   ⊆ wss 3899  {csn 4578  ⟨cop 4584   class class class wbr 5096   ↦ cmpt 5177  dom cdm 5622   ↾ cres 5624   “ cima 5625  Rel wrel 5627   Fn wfn 6485  ⟶wf 6486  ‘cfv 6490  (class class class)co 7356   supp csupp 8100  Fincfn 8881   finSupp cfsupp 9262  Basecbs 17134  0_gc0g 17357   Σ_g cgsu 17358  Mndcmnd 18657  CMndccmn 19707

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 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2182  ax-ext 2706  ax-rep 5222  ax-sep 5239  ax-nul 5249  ax-pow 5308  ax-pr 5375  ax-un 7678  ax-cnex 11080  ax-resscn 11081  ax-1cn 11082  ax-icn 11083  ax-addcl 11084  ax-addrcl 11085  ax-mulcl 11086  ax-mulrcl 11087  ax-mulcom 11088  ax-addass 11089  ax-mulass 11090  ax-distr 11091  ax-i2m1 11092  ax-1ne0 11093  ax-1rid 11094  ax-rnegex 11095  ax-rrecex 11096  ax-cnre 11097  ax-pre-lttri 11098  ax-pre-lttrn 11099  ax-pre-ltadd 11100  ax-pre-mulgt0 11101

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2537  df-eu 2567  df-clab 2713  df-cleq 2726  df-clel 2809  df-nfc 2883  df-ne 2931  df-nel 3035  df-ral 3050  df-rex 3059  df-rmo 3348  df-reu 3349  df-rab 3398  df-v 3440  df-sbc 3739  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-pss 3919  df-nul 4284  df-if 4478  df-pw 4554  df-sn 4579  df-pr 4581  df-op 4585  df-uni 4862  df-int 4901  df-iun 4946  df-iin 4947  df-br 5097  df-opab 5159  df-mpt 5178  df-tr 5204  df-id 5517  df-eprel 5522  df-po 5530  df-so 5531  df-fr 5575  df-se 5576  df-we 5577  df-xp 5628  df-rel 5629  df-cnv 5630  df-co 5631  df-dm 5632  df-rn 5633  df-res 5634  df-ima 5635  df-pred 6257  df-ord 6318  df-on 6319  df-lim 6320  df-suc 6321  df-iota 6446  df-fun 6492  df-fn 6493  df-f 6494  df-f1 6495  df-fo 6496  df-f1o 6497  df-fv 6498  df-isom 6499  df-riota 7313  df-ov 7359  df-oprab 7360  df-mpo 7361  df-of 7620  df-om 7807  df-1st 7931  df-2nd 7932  df-supp 8101  df-frecs 8221  df-wrecs 8252  df-recs 8301  df-rdg 8339  df-1o 8395  df-2o 8396  df-er 8633  df-en 8882  df-dom 8883  df-sdom 8884  df-fin 8885  df-fsupp 9263  df-oi 9413  df-card 9849  df-pnf 11166  df-mnf 11167  df-xr 11168  df-ltxr 11169  df-le 11170  df-sub 11364  df-neg 11365  df-nn 12144  df-2 12206  df-n0 12400  df-z 12487  df-uz 12750  df-fz 13422  df-fzo 13569  df-seq 13923  df-hash 14252  df-sets 17089  df-slot 17107  df-ndx 17119  df-base 17135  df-ress 17156  df-plusg 17188  df-0g 17359  df-gsum 17360  df-mre 17503  df-mrc 17504  df-acs 17506  df-mgm 18563  df-sgrp 18642  df-mnd 18658  df-submnd 18707  df-mulg 18996  df-cntz 19244  df-cmn 19709

This theorem is referenced by:  gsumwrd2dccat  33109