rmfsupp2

Description: A mapping of a multiplication of a constant with a function into a ring is finitely supported if the function is finitely supported. (Contributed by Thierry Arnoux, 3-Jun-2023)

	Ref	Expression
Hypotheses	rmfsuppf2.r	$⊢ R = {Base}_{M}$
	rmfsupp2.m	$⊢ φ \to M \in Ring$
	rmfsupp2.v	$⊢ φ \to V \in X$
	rmfsupp2.c	$⊢ (φ \land v \in V) \to C \in R$
	rmfsupp2.a	$⊢ φ \to A : V ⟶ R$
	rmfsupp2.1	$⊢ φ \to {finSupp}_{0_{M}} (A)$
Assertion	rmfsupp2	$⊢ φ \to {finSupp}_{0_{M}} ((v \in V ⟼ A (v) \cdot_{M} C))$

Proof

Step	Hyp	Ref	Expression
1		rmfsuppf2.r	$⊢ R = {Base}_{M}$
2		rmfsupp2.m	$⊢ φ \to M \in Ring$
3		rmfsupp2.v	$⊢ φ \to V \in X$
4		rmfsupp2.c	$⊢ (φ \land v \in V) \to C \in R$
5		rmfsupp2.a	$⊢ φ \to A : V ⟶ R$
6		rmfsupp2.1	$⊢ φ \to {finSupp}_{0_{M}} (A)$
7		funmpt	$⊢ Fun (v \in V ⟼ A (v) \cdot_{M} C)$
8	7	a1i	$⊢ φ \to Fun (v \in V ⟼ A (v) \cdot_{M} C)$
9	3	mptexd	$⊢ φ \to (v \in V ⟼ A (v) \cdot_{M} C) \in V$
10		ringgrp	$⊢ M \in Ring \to M \in Grp$
11		eqid	$⊢ 0_{M} = 0_{M}$
12	1 11	grpidcl	$⊢ M \in Grp \to 0_{M} \in R$
13	2 10 12	3syl	$⊢ φ \to 0_{M} \in R$
14		suppval1	$⊢ (Fun (v \in V ⟼ A (v) \cdot_{M} C) \land (v \in V ⟼ A (v) \cdot_{M} C) \in V \land 0_{M} \in R) \to (v \in V ⟼ A (v) \cdot_{M} C) supp 0_{M} = \{u \in dom (v \in V ⟼ A (v) \cdot_{M} C) \| (v \in V ⟼ A (v) \cdot_{M} C) (u) \neq 0_{M}\}$
15	8 9 13 14	syl3anc	$⊢ φ \to (v \in V ⟼ A (v) \cdot_{M} C) supp 0_{M} = \{u \in dom (v \in V ⟼ A (v) \cdot_{M} C) \| (v \in V ⟼ A (v) \cdot_{M} C) (u) \neq 0_{M}\}$
16		ovex	$⊢ A (v) \cdot_{M} C \in V$
17		eqid	$⊢ (v \in V ⟼ A (v) \cdot_{M} C) = (v \in V ⟼ A (v) \cdot_{M} C)$
18	16 17	dmmpti	$⊢ dom (v \in V ⟼ A (v) \cdot_{M} C) = V$
19	18	a1i	$⊢ φ \to dom (v \in V ⟼ A (v) \cdot_{M} C) = V$
20		ovex	$⊢ A (u) \cdot_{M} ⦋ u / v ⦌ C \in V$
21		nfcv	$⊢ \underline{Ⅎ} v u$
22		nfcv	$⊢ \underline{Ⅎ} v A (u)$
23		nfcv	$⊢ \underline{Ⅎ} v \cdot_{M}$
24		nfcsb1v	$⊢ \underline{Ⅎ} v ⦋ u / v ⦌ C$
25	22 23 24	nfov	$⊢ \underline{Ⅎ} v (A (u) \cdot_{M} ⦋ u / v ⦌ C)$
26		fveq2	$⊢ v = u \to A (v) = A (u)$
27		csbeq1a	$⊢ v = u \to C = ⦋ u / v ⦌ C$
28	26 27	oveq12d	$⊢ v = u \to A (v) \cdot_{M} C = A (u) \cdot_{M} ⦋ u / v ⦌ C$
29	21 25 28 17	fvmptf	$⊢ (u \in V \land A (u) \cdot_{M} ⦋ u / v ⦌ C \in V) \to (v \in V ⟼ A (v) \cdot_{M} C) (u) = A (u) \cdot_{M} ⦋ u / v ⦌ C$
30	20 29	mpan2	$⊢ u \in V \to (v \in V ⟼ A (v) \cdot_{M} C) (u) = A (u) \cdot_{M} ⦋ u / v ⦌ C$
31	30 18	eleq2s	$⊢ u \in dom (v \in V ⟼ A (v) \cdot_{M} C) \to (v \in V ⟼ A (v) \cdot_{M} C) (u) = A (u) \cdot_{M} ⦋ u / v ⦌ C$
32	31	adantl	$⊢ (φ \land u \in dom (v \in V ⟼ A (v) \cdot_{M} C)) \to (v \in V ⟼ A (v) \cdot_{M} C) (u) = A (u) \cdot_{M} ⦋ u / v ⦌ C$
33	32	neeq1d	$⊢ (φ \land u \in dom (v \in V ⟼ A (v) \cdot_{M} C)) \to ((v \in V ⟼ A (v) \cdot_{M} C) (u) \neq 0_{M} \leftrightarrow A (u) \cdot_{M} ⦋ u / v ⦌ C \neq 0_{M})$
34	19 33	rabeqbidva	$⊢ φ \to \{u \in dom (v \in V ⟼ A (v) \cdot_{M} C) \| (v \in V ⟼ A (v) \cdot_{M} C) (u) \neq 0_{M}\} = \{u \in V \| A (u) \cdot_{M} ⦋ u / v ⦌ C \neq 0_{M}\}$
35	5	fdmd	$⊢ φ \to dom A = V$
36	35	rabeqdv	$⊢ φ \to \{u \in dom A \| A (u) \neq 0_{M}\} = \{u \in V \| A (u) \neq 0_{M}\}$
37	5	ffund	$⊢ φ \to Fun A$
38	1	fvexi	$⊢ R \in V$
39	38	a1i	$⊢ φ \to R \in V$
40	39 3	elmapd	$⊢ φ \to (A \in (R^{V}) \leftrightarrow A : V ⟶ R)$
41	5 40	mpbird	$⊢ φ \to A \in (R^{V})$
42		suppval1	$⊢ (Fun A \land A \in (R^{V}) \land 0_{M} \in R) \to A supp 0_{M} = \{u \in dom A \| A (u) \neq 0_{M}\}$
43	37 41 13 42	syl3anc	$⊢ φ \to A supp 0_{M} = \{u \in dom A \| A (u) \neq 0_{M}\}$
44	6	fsuppimpd	$⊢ φ \to A supp 0_{M} \in Fin$
45	43 44	eqeltrrd	$⊢ φ \to \{u \in dom A \| A (u) \neq 0_{M}\} \in Fin$
46	36 45	eqeltrrd	$⊢ φ \to \{u \in V \| A (u) \neq 0_{M}\} \in Fin$
47		simpr	$⊢ ((φ \land u \in V) \land A (u) = 0_{M}) \to A (u) = 0_{M}$
48	47	oveq1d	$⊢ ((φ \land u \in V) \land A (u) = 0_{M}) \to A (u) \cdot_{M} ⦋ u / v ⦌ C = 0_{M} \cdot_{M} ⦋ u / v ⦌ C$
49	2	ad2antrr	$⊢ ((φ \land u \in V) \land A (u) = 0_{M}) \to M \in Ring$
50		simplr	$⊢ ((φ \land u \in V) \land A (u) = 0_{M}) \to u \in V$
51	4	ralrimiva	$⊢ φ \to \forall v \in V C \in R$
52	51	ad2antrr	$⊢ ((φ \land u \in V) \land A (u) = 0_{M}) \to \forall v \in V C \in R$
53		rspcsbela	$⊢ (u \in V \land \forall v \in V C \in R) \to ⦋ u / v ⦌ C \in R$
54	50 52 53	syl2anc	$⊢ ((φ \land u \in V) \land A (u) = 0_{M}) \to ⦋ u / v ⦌ C \in R$
55		eqid	$⊢ \cdot_{M} = \cdot_{M}$
56	1 55 11	ringlz	$⊢ (M \in Ring \land ⦋ u / v ⦌ C \in R) \to 0_{M} \cdot_{M} ⦋ u / v ⦌ C = 0_{M}$
57	49 54 56	syl2anc	$⊢ ((φ \land u \in V) \land A (u) = 0_{M}) \to 0_{M} \cdot_{M} ⦋ u / v ⦌ C = 0_{M}$
58	48 57	eqtrd	$⊢ ((φ \land u \in V) \land A (u) = 0_{M}) \to A (u) \cdot_{M} ⦋ u / v ⦌ C = 0_{M}$
59	58	ex	$⊢ (φ \land u \in V) \to (A (u) = 0_{M} \to A (u) \cdot_{M} ⦋ u / v ⦌ C = 0_{M})$
60	59	necon3d	$⊢ (φ \land u \in V) \to (A (u) \cdot_{M} ⦋ u / v ⦌ C \neq 0_{M} \to A (u) \neq 0_{M})$
61	60	ss2rabdv	$⊢ φ \to \{u \in V \| A (u) \cdot_{M} ⦋ u / v ⦌ C \neq 0_{M}\} \subseteq \{u \in V \| A (u) \neq 0_{M}\}$
62		ssfi	$⊢ (\{u \in V \| A (u) \neq 0_{M}\} \in Fin \land \{u \in V \| A (u) \cdot_{M} ⦋ u / v ⦌ C \neq 0_{M}\} \subseteq \{u \in V \| A (u) \neq 0_{M}\}) \to \{u \in V \| A (u) \cdot_{M} ⦋ u / v ⦌ C \neq 0_{M}\} \in Fin$
63	46 61 62	syl2anc	$⊢ φ \to \{u \in V \| A (u) \cdot_{M} ⦋ u / v ⦌ C \neq 0_{M}\} \in Fin$
64	34 63	eqeltrd	$⊢ φ \to \{u \in dom (v \in V ⟼ A (v) \cdot_{M} C) \| (v \in V ⟼ A (v) \cdot_{M} C) (u) \neq 0_{M}\} \in Fin$
65	15 64	eqeltrd	$⊢ φ \to (v \in V ⟼ A (v) \cdot_{M} C) supp 0_{M} \in Fin$
66		isfsupp	$⊢ ((v \in V ⟼ A (v) \cdot_{M} C) \in V \land 0_{M} \in R) \to ({finSupp}_{0_{M}} ((v \in V ⟼ A (v) \cdot_{M} C)) \leftrightarrow (Fun (v \in V ⟼ A (v) \cdot_{M} C) \land (v \in V ⟼ A (v) \cdot_{M} C) supp 0_{M} \in Fin))$
67	9 13 66	syl2anc	$⊢ φ \to ({finSupp}_{0_{M}} ((v \in V ⟼ A (v) \cdot_{M} C)) \leftrightarrow (Fun (v \in V ⟼ A (v) \cdot_{M} C) \land (v \in V ⟼ A (v) \cdot_{M} C) supp 0_{M} \in Fin))$
68	8 65 67	mpbir2and	$⊢ φ \to {finSupp}_{0_{M}} ((v \in V ⟼ A (v) \cdot_{M} C))$

Metamath Proof Explorer

Theorem rmfsupp2

Proof