Theorem gsumfs2d 33689

Description: Express a finite sum over a two-dimensional range as a double sum. Version of gsum2d 20213 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 7949	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ dom (𝐹 supp 0 )) → (𝐴 “ {𝑥}) ∈ V)
8		gsumfs2d.3	. . . . . . . 8 ⊢ (𝜑 → 𝐹:𝐴⟶𝐵)
9	8	ffnd 6729	. . . . . . 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 6919	. . . . . . 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 4054	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ dom (𝐹 supp 0 )) ∧ 𝑦 ∈ ((𝐴 “ {𝑥}) ∖ ((𝐹 supp 0 ) “ {𝑥}))) → 𝑦 ∈ (𝐴 “ {𝑥}))
16		vex 3458	. . . . . . . . . 10 ⊢ 𝑥 ∈ V
17		vex 3458	. . . . . . . . . 10 ⊢ 𝑦 ∈ V
18	16, 17	elimasn 6099	. . . . . . . . 9 ⊢ (𝑦 ∈ (𝐴 “ {𝑥}) ↔ ⟨𝑥, 𝑦⟩ ∈ 𝐴)
19	18	biimpi 219	. . . . . . . 8 ⊢ (𝑦 ∈ (𝐴 “ {𝑥}) → ⟨𝑥, 𝑦⟩ ∈ 𝐴)
20	15, 19	syl 18	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ dom (𝐹 supp 0 )) ∧ 𝑦 ∈ ((𝐴 “ {𝑥}) ∖ ((𝐹 supp 0 ) “ {𝑥}))) → ⟨𝑥, 𝑦⟩ ∈ 𝐴)
21	14	eldifbd 4055	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ dom (𝐹 supp 0 )) ∧ 𝑦 ∈ ((𝐴 “ {𝑥}) ∖ ((𝐹 supp 0 ) “ {𝑥}))) → ¬ 𝑦 ∈ ((𝐹 supp 0 ) “ {𝑥}))
22	16, 17	elimasn 6099	. . . . . . . . 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 4053	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ dom (𝐹 supp 0 )) ∧ 𝑦 ∈ ((𝐴 “ {𝑥}) ∖ ((𝐹 supp 0 ) “ {𝑥}))) → ⟨𝑥, 𝑦⟩ ∈ (𝐴 ∖ (𝐹 supp 0 )))
26	10, 11, 13, 25	fvdifsupp 8213	. . . . 5 ⊢ (((𝜑 ∧ 𝑥 ∈ dom (𝐹 supp 0 )) ∧ 𝑦 ∈ ((𝐴 “ {𝑥}) ∖ ((𝐹 supp 0 ) “ {𝑥}))) → (𝐹‘⟨𝑥, 𝑦⟩) = 0 )
27		gsumfs2d.2	. . . . . . . 8 ⊢ (𝜑 → 𝐹 finSupp 0 )
28	27	fsuppimpd 9386	. . . . . . 7 ⊢ (𝜑 → (𝐹 supp 0 ) ∈ Fin)
29	28	adantr 486	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ dom (𝐹 supp 0 )) → (𝐹 supp 0 ) ∈ Fin)
30		imafi2 9375	. . . . . 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 7106	. . . . 5 ⊢ (((𝜑 ∧ 𝑥 ∈ dom (𝐹 supp 0 )) ∧ 𝑦 ∈ (𝐴 “ {𝑥})) → (𝐹‘⟨𝑥, 𝑦⟩) ∈ 𝐵)
35		suppssdm 8219	. . . . . . . 8 ⊢ (𝐹 supp 0 ) ⊆ dom 𝐹
36	35, 8	fssdm 6748	. . . . . . 7 ⊢ (𝜑 → (𝐹 supp 0 ) ⊆ 𝐴)
37	36	adantr 486	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ dom (𝐹 supp 0 )) → (𝐹 supp 0 ) ⊆ 𝐴)
38		imass1 6065	. . . . . 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 33681	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ dom (𝐹 supp 0 )) → (𝑊 Σg (𝑦 ∈ (𝐴 “ {𝑥}) ↦ (𝐹‘⟨𝑥, 𝑦⟩))) = (𝑊 Σg (𝑦 ∈ ((𝐹 supp 0 ) “ {𝑥}) ↦ (𝐹‘⟨𝑥, 𝑦⟩))))
41	40	mpteq2dva 5201	. . 3 ⊢ (𝜑 → (𝑥 ∈ dom (𝐹 supp 0 ) ↦ (𝑊 Σg (𝑦 ∈ (𝐴 “ {𝑥}) ↦ (𝐹‘⟨𝑥, 𝑦⟩)))) = (𝑥 ∈ dom (𝐹 supp 0 ) ↦ (𝑊 Σg (𝑦 ∈ ((𝐹 supp 0 ) “ {𝑥}) ↦ (𝐹‘⟨𝑥, 𝑦⟩)))))
42	41	oveq2d 7456	. 2 ⊢ (𝜑 → (𝑊 Σg (𝑥 ∈ dom (𝐹 supp 0 ) ↦ (𝑊 Σg (𝑦 ∈ (𝐴 “ {𝑥}) ↦ (𝐹‘⟨𝑥, 𝑦⟩))))) = (𝑊 Σg (𝑥 ∈ dom (𝐹 supp 0 ) ↦ (𝑊 Σg (𝑦 ∈ ((𝐹 supp 0 ) “ {𝑥}) ↦ (𝐹‘⟨𝑥, 𝑦⟩))))))
43	5	dmexd 7936	. . 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 4055	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ (dom 𝐴 ∖ dom (𝐹 supp 0 ))) ∧ 𝑦 ∈ (𝐴 “ {𝑥})) → ¬ 𝑥 ∈ dom (𝐹 supp 0 ))
50	16, 17	opeldm 5895	. . . . . . . . 9 ⊢ (⟨𝑥, 𝑦⟩ ∈ (𝐹 supp 0 ) → 𝑥 ∈ dom (𝐹 supp 0 ))
51	49, 50	nsyl 141	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ (dom 𝐴 ∖ dom (𝐹 supp 0 ))) ∧ 𝑦 ∈ (𝐴 “ {𝑥})) → ¬ ⟨𝑥, 𝑦⟩ ∈ (𝐹 supp 0 ))
52	47, 51	eldifd 4053	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ (dom 𝐴 ∖ dom (𝐹 supp 0 ))) ∧ 𝑦 ∈ (𝐴 “ {𝑥})) → ⟨𝑥, 𝑦⟩ ∈ (𝐴 ∖ (𝐹 supp 0 )))
53	44, 45, 46, 52	fvdifsupp 8213	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ (dom 𝐴 ∖ dom (𝐹 supp 0 ))) ∧ 𝑦 ∈ (𝐴 “ {𝑥})) → (𝐹‘⟨𝑥, 𝑦⟩) = 0 )
54	53	mpteq2dva 5201	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ (dom 𝐴 ∖ dom (𝐹 supp 0 ))) → (𝑦 ∈ (𝐴 “ {𝑥}) ↦ (𝐹‘⟨𝑥, 𝑦⟩)) = (𝑦 ∈ (𝐴 “ {𝑥}) ↦ 0 ))
55	54	oveq2d 7456	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ (dom 𝐴 ∖ dom (𝐹 supp 0 ))) → (𝑊 Σg (𝑦 ∈ (𝐴 “ {𝑥}) ↦ (𝐹‘⟨𝑥, 𝑦⟩))) = (𝑊 Σg (𝑦 ∈ (𝐴 “ {𝑥}) ↦ 0 )))
56	3	cmnmndd 20045	. . . . 5 ⊢ (𝜑 → 𝑊 ∈ Mnd)
57	5	adantr 486	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (dom 𝐴 ∖ dom (𝐹 supp 0 ))) → 𝐴 ∈ 𝑋)
58	57	imaexd 7949	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ (dom 𝐴 ∖ dom (𝐹 supp 0 ))) → (𝐴 “ {𝑥}) ∈ V)
59	2	gsumz 19058	. . . . 5 ⊢ ((𝑊 ∈ Mnd ∧ (𝐴 “ {𝑥}) ∈ V) → (𝑊 Σg (𝑦 ∈ (𝐴 “ {𝑥}) ↦ 0 )) = 0 )
60	56, 58, 59	syl2an2r 698	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ (dom 𝐴 ∖ dom (𝐹 supp 0 ))) → (𝑊 Σg (𝑦 ∈ (𝐴 “ {𝑥}) ↦ 0 )) = 0 )
61	55, 60	eqtrd 2798	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ (dom 𝐴 ∖ dom (𝐹 supp 0 ))) → (𝑊 Σg (𝑦 ∈ (𝐴 “ {𝑥}) ↦ (𝐹‘⟨𝑥, 𝑦⟩))) = 0 )
62		dmfi 9349	. . . 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 7949	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐴) → (𝐴 “ {𝑥}) ∈ V)
67	8	ad2antrr 739	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐴) ∧ 𝑦 ∈ (𝐴 “ {𝑥})) → 𝐹:𝐴⟶𝐵)
68	19	adantl 487	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐴) ∧ 𝑦 ∈ (𝐴 “ {𝑥})) → ⟨𝑥, 𝑦⟩ ∈ 𝐴)
69	67, 68	ffvelcdmd 7106	. . . . 5 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐴) ∧ 𝑦 ∈ (𝐴 “ {𝑥})) → (𝐹‘⟨𝑥, 𝑦⟩) ∈ 𝐵)
70	69	fmpttd 7136	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐴) → (𝑦 ∈ (𝐴 “ {𝑥}) ↦ (𝐹‘⟨𝑥, 𝑦⟩)):(𝐴 “ {𝑥})⟶𝐵)
71	66	mptexd 7250	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐴) → (𝑦 ∈ (𝐴 “ {𝑥}) ↦ (𝐹‘⟨𝑥, 𝑦⟩)) ∈ V)
72	70	ffnd 6729	. . . . 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 2763	. . . . . . . 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 2864	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑥 ∈ dom 𝐴) ∧ 𝑡 ∈ (𝐴 “ {𝑥})) ∧ ¬ 𝑡 ∈ ((𝐹 supp 0 ) “ {𝑥})) ∧ 𝑦 = 𝑡) → 𝑦 ∈ (𝐴 “ {𝑥}))
82		simplr 781	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑥 ∈ dom 𝐴) ∧ 𝑡 ∈ (𝐴 “ {𝑥})) ∧ ¬ 𝑡 ∈ ((𝐹 supp 0 ) “ {𝑥})) ∧ 𝑦 = 𝑡) → ¬ 𝑡 ∈ ((𝐹 supp 0 ) “ {𝑥}))
83	79, 82	eqneltrd 2884	. . . . . . . . 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 4053	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑥 ∈ dom 𝐴) ∧ 𝑦 ∈ (𝐴 “ {𝑥})) ∧ ¬ 𝑦 ∈ ((𝐹 supp 0 ) “ {𝑥})) → ⟨𝑥, 𝑦⟩ ∈ (𝐴 ∖ (𝐹 supp 0 )))
91	84, 85, 86, 90	fvdifsupp 8213	. . . . . . . . 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 7022	. . . . . . 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 9389	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐴) → (𝑦 ∈ (𝐴 “ {𝑥}) ↦ (𝐹‘⟨𝑥, 𝑦⟩)) finSupp 0 )
99	1, 2, 64, 66, 70, 98	gsumcl 20156	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐴) → (𝑊 Σg (𝑦 ∈ (𝐴 “ {𝑥}) ↦ (𝐹‘⟨𝑥, 𝑦⟩))) ∈ 𝐵)
100		dmss 5890	. . . 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 33681	. 2 ⊢ (𝜑 → (𝑊 Σg (𝑥 ∈ dom 𝐴 ↦ (𝑊 Σg (𝑦 ∈ (𝐴 “ {𝑥}) ↦ (𝐹‘⟨𝑥, 𝑦⟩))))) = (𝑊 Σg (𝑥 ∈ dom (𝐹 supp 0 ) ↦ (𝑊 Σg (𝑦 ∈ (𝐴 “ {𝑥}) ↦ (𝐹‘⟨𝑥, 𝑦⟩))))))
103	8, 36	feqresmpt 6974	. . . 4 ⊢ (𝜑 → (𝐹 ↾ (𝐹 supp 0 )) = (𝑧 ∈ (𝐹 supp 0 ) ↦ (𝐹‘𝑧)))
104	103	oveq2d 7456	. . 3 ⊢ (𝜑 → (𝑊 Σg (𝐹 ↾ (𝐹 supp 0 ))) = (𝑊 Σg (𝑧 ∈ (𝐹 supp 0 ) ↦ (𝐹‘𝑧))))
105		ssidd 3936	. . . 4 ⊢ (𝜑 → (𝐹 supp 0 ) ⊆ (𝐹 supp 0 ))
106	1, 2, 3, 5, 8, 105, 27	gsumres 20154	. . 3 ⊢ (𝜑 → (𝑊 Σg (𝐹 ↾ (𝐹 supp 0 ))) = (𝑊 Σg 𝐹))
107		nfcv 2926	. . . 4 ⊢ Ⅎ𝑦(𝐹‘𝑧)
108		gsumfs2d.p	. . . 4 ⊢ Ⅎ𝑥𝜑
109		fveq2 6905	. . . 4 ⊢ (𝑧 = ⟨𝑥, 𝑦⟩ → (𝐹‘𝑧) = (𝐹‘⟨𝑥, 𝑦⟩))
110		gsumfs2d.r	. . . . 5 ⊢ (𝜑 → Rel 𝐴)
111		relss 5763	. . . . 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 3913	. . . . 5 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝐹 supp 0 )) → 𝑧 ∈ 𝐴)
115	113, 114	ffvelcdmd 7106	. . . 4 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝐹 supp 0 )) → (𝐹‘𝑧) ∈ 𝐵)
116	107, 108, 1, 109, 112, 28, 3, 115	gsummpt2d 33677	. . 3 ⊢ (𝜑 → (𝑊 Σg (𝑧 ∈ (𝐹 supp 0 ) ↦ (𝐹‘𝑧))) = (𝑊 Σg (𝑥 ∈ dom (𝐹 supp 0 ) ↦ (𝑊 Σg (𝑦 ∈ ((𝐹 supp 0 ) “ {𝑥}) ↦ (𝐹‘⟨𝑥, 𝑦⟩))))))
117	104, 106, 116	3eqtr3d 2806	. 2 ⊢ (𝜑 → (𝑊 Σg 𝐹) = (𝑊 Σg (𝑥 ∈ dom (𝐹 supp 0 ) ↦ (𝑊 Σg (𝑦 ∈ ((𝐹 supp 0 ) “ {𝑥}) ↦ (𝐹‘⟨𝑥, 𝑦⟩))))))
118	42, 102, 117	3eqtr4rd 2809	1 ⊢ (𝜑 → (𝑊 Σg 𝐹) = (𝑊 Σg (𝑥 ∈ dom 𝐴 ↦ (𝑊 Σg (𝑦 ∈ (𝐴 “ {𝑥}) ↦ (𝐹‘⟨𝑥, 𝑦⟩))))))

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ∧ wa 401   = wceq 1570  Ⅎwnf 1816   ∈ wcel 2147  Vcvv 3454   ⊆ wss 3900   ∖ cdif 4048  {csn 4588  ⟨cop 4838   class class class wbr 5106   ↦ cmpt 5189  dom cdm 5655   ↾ cres 5657   “ cima 5658  Rel wrel 5660   Fn wfn 6550  ⟶wf 6551  ‘cfv 6555  (class class class)co 7440   supp csupp 8201  Fincfn 8998   finSupp cfsupp 9378  Basecbs 17413  0_gc0g 17636   Σ_g cgsu 17637  Mndcmnd 18949  CMndccmn 20021

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-rep 5235  ax-sep 5252  ax-nul 5263  ax-pow 5331  ax-pr 5395  ax-un 7772  ax-cnex 11280  ax-resscn 11281  ax-1cn 11282  ax-icn 11283  ax-addcl 11284  ax-addrcl 11285  ax-mulcl 11286  ax-mulrcl 11287  ax-mulcom 11288  ax-addass 11289  ax-mulass 11290  ax-distr 11291  ax-i2m1 11292  ax-1ne0 11293  ax-1rid 11294  ax-rnegex 11295  ax-rrecex 11296  ax-cnre 11297  ax-pre-lttri 11298  ax-pre-lttrn 11299  ax-pre-ltadd 11300  ax-pre-mulgt0 11301

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 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ne 2960  df-nel 3066  df-ral 3081  df-rex 3091  df-rmo 3369  df-reu 3370  df-rab 3417  df-v 3456  df-sbc 3743  df-csb 3852  df-ss 3901  df-pss 4017  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-pw 4562  df-sn 4589  df-pr 4591  df-op 4839  df-uni 4871  df-int 4911  df-iun 4956  df-iin 4957  df-br 5107  df-opab 5171  df-mpt 5190  df-tr 5216  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 6319  df-ord 6380  df-on 6381  df-lim 6382  df-suc 6383  df-iota 6509  df-fun 6557  df-fn 6558  df-f 6559  df-f1 6560  df-fo 6561  df-f1o 6562  df-fv 6563  df-isom 6564  df-riota 7397  df-ov 7443  df-oprab 7444  df-mpo 7445  df-of 7714  df-om 7899  df-1st 8022  df-2nd 8023  df-supp 8202  df-frecs 8324  df-wrecs 8355  df-recs 8404  df-rdg 8443  df-1o 8501  df-2o 8502  df-er 8742  df-en 8999  df-dom 9000  df-sdom 9001  df-fin 9002  df-fsupp 9379  df-oi 9528  df-card 10044  df-pnf 11369  df-mnf 11370  df-xr 11371  df-ltxr 11372  df-le 11373  df-sub 11567  df-neg 11568  df-nn 12360  df-2 12429  df-n0 12631  df-z 12718  df-uz 12990  df-fz 13664  df-fzo 13813  df-seq 14169  df-hash 14499  df-sets 17368  df-slot 17386  df-ndx 17398  df-base 17414  df-ress 17435  df-plusg 17467  df-0g 17638  df-gsum 17639  df-mre 17782  df-mrc 17783  df-acs 17785  df-mgm 18842  df-sgrp 18934  df-mnd 18950  df-submnd 19005  df-mulg 19304  df-cntz 19558  df-cmn 20023

This theorem is used by:  gsumwrd2dccat  33706