Theorem gsum2d2lem 19764

Description: Lemma for gsum2d2 19765: show the function is finitely supported. (Contributed by Mario Carneiro, 28-Dec-2014.) (Revised by AV, 9-Jun-2019.)

Hypotheses

Ref	Expression
gsum2d2.b	⊢ 𝐵 = (Base‘𝐺)
gsum2d2.z	⊢ 0 = (0g‘𝐺)
gsum2d2.g	⊢ (𝜑 → 𝐺 ∈ CMnd)
gsum2d2.a	⊢ (𝜑 → 𝐴 ∈ 𝑉)
gsum2d2.r	⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → 𝐶 ∈ 𝑊)
gsum2d2.f	⊢ ((𝜑 ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐶)) → 𝑋 ∈ 𝐵)
gsum2d2.u	⊢ (𝜑 → 𝑈 ∈ Fin)
gsum2d2.n	⊢ ((𝜑 ∧ ((𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐶) ∧ ¬ 𝑗𝑈𝑘)) → 𝑋 = 0 )

Assertion

Ref	Expression
gsum2d2lem	⊢ (𝜑 → (𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋) finSupp 0 )

Distinct variable groups:   𝑗,𝑘,𝐵   𝜑,𝑗,𝑘   𝐴,𝑗,𝑘   𝑗,𝐺,𝑘   𝑈,𝑗,𝑘   𝐶,𝑘   𝑗,𝑉   0 ,𝑗,𝑘

Allowed substitution hints:   𝐶(𝑗)   𝑉(𝑘)   𝑊(𝑗,𝑘)   𝑋(𝑗,𝑘)

Proof of Theorem gsum2d2lem

Dummy variable 𝑧 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		eqid 2731	. . . 4 ⊢ (𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋) = (𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋)
2	1	mpofun 7485	. . 3 ⊢ Fun (𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋)
3	2	a1i 11	. 2 ⊢ (𝜑 → Fun (𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋))
4		gsum2d2.u	. . 3 ⊢ (𝜑 → 𝑈 ∈ Fin)
5		gsum2d2.f	. . . . . 6 ⊢ ((𝜑 ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐶)) → 𝑋 ∈ 𝐵)
6	5	ralrimivva 3193	. . . . 5 ⊢ (𝜑 → ∀𝑗 ∈ 𝐴 ∀𝑘 ∈ 𝐶 𝑋 ∈ 𝐵)
7	1	fmpox 8004	. . . . 5 ⊢ (∀𝑗 ∈ 𝐴 ∀𝑘 ∈ 𝐶 𝑋 ∈ 𝐵 ↔ (𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋):∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐶)⟶𝐵)
8	6, 7	sylib 217	. . . 4 ⊢ (𝜑 → (𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋):∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐶)⟶𝐵)
9		nfv 1917	. . . . . 6 ⊢ Ⅎ𝑗𝜑
10		nfiu1 4993	. . . . . . . 8 ⊢ Ⅎ𝑗∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐶)
11		nfcv 2902	. . . . . . . 8 ⊢ Ⅎ𝑗𝑈
12	10, 11	nfdif 4090	. . . . . . 7 ⊢ Ⅎ𝑗(∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐶) ∖ 𝑈)
13	12	nfcri 2889	. . . . . 6 ⊢ Ⅎ𝑗 𝑧 ∈ (∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐶) ∖ 𝑈)
14	9, 13	nfan 1902	. . . . 5 ⊢ Ⅎ𝑗(𝜑 ∧ 𝑧 ∈ (∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐶) ∖ 𝑈))
15		nfmpo1 7442	. . . . . . 7 ⊢ Ⅎ𝑗(𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋)
16		nfcv 2902	. . . . . . 7 ⊢ Ⅎ𝑗𝑧
17	15, 16	nffv 6857	. . . . . 6 ⊢ Ⅎ𝑗((𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋)‘𝑧)
18	17	nfeq1 2917	. . . . 5 ⊢ Ⅎ𝑗((𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋)‘𝑧) = 0
19		relxp 5656	. . . . . . . 8 ⊢ Rel ({𝑗} × 𝐶)
20	19	rgenw 3064	. . . . . . 7 ⊢ ∀𝑗 ∈ 𝐴 Rel ({𝑗} × 𝐶)
21		reliun 5777	. . . . . . 7 ⊢ (Rel ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐶) ↔ ∀𝑗 ∈ 𝐴 Rel ({𝑗} × 𝐶))
22	20, 21	mpbir 230	. . . . . 6 ⊢ Rel ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐶)
23		eldifi 4091	. . . . . . 7 ⊢ (𝑧 ∈ (∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐶) ∖ 𝑈) → 𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐶))
24	23	adantl 482	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ (∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐶) ∖ 𝑈)) → 𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐶))
25		elrel 5759	. . . . . 6 ⊢ ((Rel ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐶) ∧ 𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐶)) → ∃𝑗∃𝑘 𝑧 = ⟨𝑗, 𝑘⟩)
26	22, 24, 25	sylancr 587	. . . . 5 ⊢ ((𝜑 ∧ 𝑧 ∈ (∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐶) ∖ 𝑈)) → ∃𝑗∃𝑘 𝑧 = ⟨𝑗, 𝑘⟩)
27		nfv 1917	. . . . . 6 ⊢ Ⅎ𝑘(𝜑 ∧ 𝑧 ∈ (∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐶) ∖ 𝑈))
28		nfmpo2 7443	. . . . . . . 8 ⊢ Ⅎ𝑘(𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋)
29		nfcv 2902	. . . . . . . 8 ⊢ Ⅎ𝑘𝑧
30	28, 29	nffv 6857	. . . . . . 7 ⊢ Ⅎ𝑘((𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋)‘𝑧)
31	30	nfeq1 2917	. . . . . 6 ⊢ Ⅎ𝑘((𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋)‘𝑧) = 0
32		simprr 771	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑧 ∈ (∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐶) ∖ 𝑈) ∧ 𝑧 = ⟨𝑗, 𝑘⟩)) → 𝑧 = ⟨𝑗, 𝑘⟩)
33	32	fveq2d 6851	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑧 ∈ (∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐶) ∖ 𝑈) ∧ 𝑧 = ⟨𝑗, 𝑘⟩)) → ((𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋)‘𝑧) = ((𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋)‘⟨𝑗, 𝑘⟩))
34		df-ov 7365	. . . . . . . . 9 ⊢ (𝑗(𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋)𝑘) = ((𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋)‘⟨𝑗, 𝑘⟩)
35		simprl 769	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑧 ∈ (∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐶) ∖ 𝑈) ∧ 𝑧 = ⟨𝑗, 𝑘⟩)) → 𝑧 ∈ (∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐶) ∖ 𝑈))
36	32, 35	eqeltrrd 2833	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑧 ∈ (∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐶) ∖ 𝑈) ∧ 𝑧 = ⟨𝑗, 𝑘⟩)) → ⟨𝑗, 𝑘⟩ ∈ (∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐶) ∖ 𝑈))
37	36	eldifad 3925	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑧 ∈ (∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐶) ∖ 𝑈) ∧ 𝑧 = ⟨𝑗, 𝑘⟩)) → ⟨𝑗, 𝑘⟩ ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐶))
38		opeliunxp 5704	. . . . . . . . . . . 12 ⊢ (⟨𝑗, 𝑘⟩ ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐶) ↔ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐶))
39	37, 38	sylib 217	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑧 ∈ (∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐶) ∖ 𝑈) ∧ 𝑧 = ⟨𝑗, 𝑘⟩)) → (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐶))
40	39	simpld 495	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑧 ∈ (∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐶) ∖ 𝑈) ∧ 𝑧 = ⟨𝑗, 𝑘⟩)) → 𝑗 ∈ 𝐴)
41	39	simprd 496	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑧 ∈ (∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐶) ∖ 𝑈) ∧ 𝑧 = ⟨𝑗, 𝑘⟩)) → 𝑘 ∈ 𝐶)
42	39, 5	syldan 591	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑧 ∈ (∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐶) ∖ 𝑈) ∧ 𝑧 = ⟨𝑗, 𝑘⟩)) → 𝑋 ∈ 𝐵)
43	1	ovmpt4g 7507	. . . . . . . . . 10 ⊢ ((𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐶 ∧ 𝑋 ∈ 𝐵) → (𝑗(𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋)𝑘) = 𝑋)
44	40, 41, 42, 43	syl3anc 1371	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑧 ∈ (∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐶) ∖ 𝑈) ∧ 𝑧 = ⟨𝑗, 𝑘⟩)) → (𝑗(𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋)𝑘) = 𝑋)
45	34, 44	eqtr3id 2785	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑧 ∈ (∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐶) ∖ 𝑈) ∧ 𝑧 = ⟨𝑗, 𝑘⟩)) → ((𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋)‘⟨𝑗, 𝑘⟩) = 𝑋)
46		eldifn 4092	. . . . . . . . . . . 12 ⊢ (𝑧 ∈ (∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐶) ∖ 𝑈) → ¬ 𝑧 ∈ 𝑈)
47	46	ad2antrl 726	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑧 ∈ (∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐶) ∖ 𝑈) ∧ 𝑧 = ⟨𝑗, 𝑘⟩)) → ¬ 𝑧 ∈ 𝑈)
48	32	eleq1d 2817	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑧 ∈ (∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐶) ∖ 𝑈) ∧ 𝑧 = ⟨𝑗, 𝑘⟩)) → (𝑧 ∈ 𝑈 ↔ ⟨𝑗, 𝑘⟩ ∈ 𝑈))
49		df-br 5111	. . . . . . . . . . . 12 ⊢ (𝑗𝑈𝑘 ↔ ⟨𝑗, 𝑘⟩ ∈ 𝑈)
50	48, 49	bitr4di 288	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑧 ∈ (∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐶) ∖ 𝑈) ∧ 𝑧 = ⟨𝑗, 𝑘⟩)) → (𝑧 ∈ 𝑈 ↔ 𝑗𝑈𝑘))
51	47, 50	mtbid 323	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑧 ∈ (∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐶) ∖ 𝑈) ∧ 𝑧 = ⟨𝑗, 𝑘⟩)) → ¬ 𝑗𝑈𝑘)
52	39, 51	jca 512	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑧 ∈ (∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐶) ∖ 𝑈) ∧ 𝑧 = ⟨𝑗, 𝑘⟩)) → ((𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐶) ∧ ¬ 𝑗𝑈𝑘))
53		gsum2d2.n	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐶) ∧ ¬ 𝑗𝑈𝑘)) → 𝑋 = 0 )
54	52, 53	syldan 591	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑧 ∈ (∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐶) ∖ 𝑈) ∧ 𝑧 = ⟨𝑗, 𝑘⟩)) → 𝑋 = 0 )
55	33, 45, 54	3eqtrd 2775	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑧 ∈ (∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐶) ∖ 𝑈) ∧ 𝑧 = ⟨𝑗, 𝑘⟩)) → ((𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋)‘𝑧) = 0 )
56	55	expr 457	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ (∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐶) ∖ 𝑈)) → (𝑧 = ⟨𝑗, 𝑘⟩ → ((𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋)‘𝑧) = 0 ))
57	27, 31, 56	exlimd 2211	. . . . 5 ⊢ ((𝜑 ∧ 𝑧 ∈ (∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐶) ∖ 𝑈)) → (∃𝑘 𝑧 = ⟨𝑗, 𝑘⟩ → ((𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋)‘𝑧) = 0 ))
58	14, 18, 26, 57	exlimimdd 2212	. . . 4 ⊢ ((𝜑 ∧ 𝑧 ∈ (∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐶) ∖ 𝑈)) → ((𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋)‘𝑧) = 0 )
59	8, 58	suppss 8130	. . 3 ⊢ (𝜑 → ((𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋) supp 0 ) ⊆ 𝑈)
60	4, 59	ssfid 9218	. 2 ⊢ (𝜑 → ((𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋) supp 0 ) ∈ Fin)
61		gsum2d2.a	. . . 4 ⊢ (𝜑 → 𝐴 ∈ 𝑉)
62		gsum2d2.r	. . . . 5 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → 𝐶 ∈ 𝑊)
63	62	ralrimiva 3139	. . . 4 ⊢ (𝜑 → ∀𝑗 ∈ 𝐴 𝐶 ∈ 𝑊)
64	1	mpoexxg 8013	. . . 4 ⊢ ((𝐴 ∈ 𝑉 ∧ ∀𝑗 ∈ 𝐴 𝐶 ∈ 𝑊) → (𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋) ∈ V)
65	61, 63, 64	syl2anc 584	. . 3 ⊢ (𝜑 → (𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋) ∈ V)
66		gsum2d2.z	. . . . 5 ⊢ 0 = (0g‘𝐺)
67	66	fvexi 6861	. . . 4 ⊢ 0 ∈ V
68	67	a1i 11	. . 3 ⊢ (𝜑 → 0 ∈ V)
69		isfsupp 9316	. . 3 ⊢ (((𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋) ∈ V ∧ 0 ∈ V) → ((𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋) finSupp 0 ↔ (Fun (𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋) ∧ ((𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋) supp 0 ) ∈ Fin)))
70	65, 68, 69	syl2anc 584	. 2 ⊢ (𝜑 → ((𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋) finSupp 0 ↔ (Fun (𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋) ∧ ((𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋) supp 0 ) ∈ Fin)))
71	3, 60, 70	mpbir2and 711	1 ⊢ (𝜑 → (𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋) finSupp 0 )

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∧ wa 396   = wceq 1541  ∃wex 1781   ∈ wcel 2106  ∀wral 3060  Vcvv 3446   ∖ cdif 3910  {csn 4591  ⟨cop 4597  ∪ ciun 4959   class class class wbr 5110   × cxp 5636  Rel wrel 5643  Fun wfun 6495  ⟶wf 6497  ‘cfv 6501  (class class class)co 7362   ∈ cmpo 7364   supp csupp 8097  Fincfn 8890   finSupp cfsupp 9312  Basecbs 17094  0_gc0g 17335  CMndccmn 19576

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2702  ax-rep 5247  ax-sep 5261  ax-nul 5268  ax-pow 5325  ax-pr 5389  ax-un 7677

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2533  df-eu 2562  df-clab 2709  df-cleq 2723  df-clel 2809  df-nfc 2884  df-ne 2940  df-ral 3061  df-rex 3070  df-reu 3352  df-rab 3406  df-v 3448  df-sbc 3743  df-csb 3859  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-pss 3932  df-nul 4288  df-if 4492  df-pw 4567  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4871  df-iun 4961  df-br 5111  df-opab 5173  df-mpt 5194  df-tr 5228  df-id 5536  df-eprel 5542  df-po 5550  df-so 5551  df-fr 5593  df-we 5595  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-ord 6325  df-on 6326  df-lim 6327  df-suc 6328  df-iota 6453  df-fun 6503  df-fn 6504  df-f 6505  df-f1 6506  df-fo 6507  df-f1o 6508  df-fv 6509  df-ov 7365  df-oprab 7366  df-mpo 7367  df-om 7808  df-1st 7926  df-2nd 7927  df-supp 8098  df-1o 8417  df-en 8891  df-fin 8894  df-fsupp 9313

This theorem is referenced by:  gsum2d2  19765  gsumcom2  19766