rmsuppss

Description: The support of a mapping of a multiplication of a constant with a function into a ring is a subset of the support of the function. (Contributed by AV, 11-Apr-2019)

		Ref	Expression
	Hypothesis	rmsuppss.r	$⊢ R = {Base}_{M}$
	Assertion	rmsuppss	$⊢ ((M \in Ring \land V \in X \land C \in R) \land A \in (R^{V})) \to (v \in V ⟼ C \cdot_{M} A (v)) supp 0_{M} \subseteq A supp 0_{M}$

Proof

Step	Hyp	Ref	Expression
1		rmsuppss.r	$⊢ R = {Base}_{M}$
2		oveq2	$⊢ A (w) = 0_{M} \to C \cdot_{M} A (w) = C \cdot_{M} 0_{M}$
3		simpll1	$⊢ (((M \in Ring \land V \in X \land C \in R) \land A \in (R^{V})) \land w \in V) \to M \in Ring$
4		simpll3	$⊢ (((M \in Ring \land V \in X \land C \in R) \land A \in (R^{V})) \land w \in V) \to C \in R$
5		eqid	$⊢ \cdot_{M} = \cdot_{M}$
6		eqid	$⊢ 0_{M} = 0_{M}$
7	1 5 6	ringrz	$⊢ (M \in Ring \land C \in R) \to C \cdot_{M} 0_{M} = 0_{M}$
8	3 4 7	syl2anc	$⊢ (((M \in Ring \land V \in X \land C \in R) \land A \in (R^{V})) \land w \in V) \to C \cdot_{M} 0_{M} = 0_{M}$
9	2 8	sylan9eqr	$⊢ ((((M \in Ring \land V \in X \land C \in R) \land A \in (R^{V})) \land w \in V) \land A (w) = 0_{M}) \to C \cdot_{M} A (w) = 0_{M}$
10	9	ex	$⊢ (((M \in Ring \land V \in X \land C \in R) \land A \in (R^{V})) \land w \in V) \to (A (w) = 0_{M} \to C \cdot_{M} A (w) = 0_{M})$
11	10	necon3d	$⊢ (((M \in Ring \land V \in X \land C \in R) \land A \in (R^{V})) \land w \in V) \to (C \cdot_{M} A (w) \neq 0_{M} \to A (w) \neq 0_{M})$
12	11	ss2rabdv	$⊢ ((M \in Ring \land V \in X \land C \in R) \land A \in (R^{V})) \to \{w \in V \| C \cdot_{M} A (w) \neq 0_{M}\} \subseteq \{w \in V \| A (w) \neq 0_{M}\}$
13		elmapi	$⊢ A \in (R^{V}) \to A : V ⟶ R$
14	13	fdmd	$⊢ A \in (R^{V}) \to dom A = V$
15	14	adantl	$⊢ ((M \in Ring \land V \in X \land C \in R) \land A \in (R^{V})) \to dom A = V$
16		rabeq	$⊢ dom A = V \to \{w \in dom A \| A (w) \neq 0_{M}\} = \{w \in V \| A (w) \neq 0_{M}\}$
17	15 16	syl	$⊢ ((M \in Ring \land V \in X \land C \in R) \land A \in (R^{V})) \to \{w \in dom A \| A (w) \neq 0_{M}\} = \{w \in V \| A (w) \neq 0_{M}\}$
18	12 17	sseqtrrd	$⊢ ((M \in Ring \land V \in X \land C \in R) \land A \in (R^{V})) \to \{w \in V \| C \cdot_{M} A (w) \neq 0_{M}\} \subseteq \{w \in dom A \| A (w) \neq 0_{M}\}$
19		fveq2	$⊢ v = w \to A (v) = A (w)$
20	19	oveq2d	$⊢ v = w \to C \cdot_{M} A (v) = C \cdot_{M} A (w)$
21	20	cbvmptv	$⊢ (v \in V ⟼ C \cdot_{M} A (v)) = (w \in V ⟼ C \cdot_{M} A (w))$
22		simpl2	$⊢ ((M \in Ring \land V \in X \land C \in R) \land A \in (R^{V})) \to V \in X$
23		fvexd	$⊢ ((M \in Ring \land V \in X \land C \in R) \land A \in (R^{V})) \to 0_{M} \in V$
24		ovexd	$⊢ (((M \in Ring \land V \in X \land C \in R) \land A \in (R^{V})) \land w \in V) \to C \cdot_{M} A (w) \in V$
25	21 22 23 24	mptsuppd	$⊢ ((M \in Ring \land V \in X \land C \in R) \land A \in (R^{V})) \to (v \in V ⟼ C \cdot_{M} A (v)) supp 0_{M} = \{w \in V \| C \cdot_{M} A (w) \neq 0_{M}\}$
26		elmapfun	$⊢ A \in (R^{V}) \to Fun A$
27	26	adantl	$⊢ ((M \in Ring \land V \in X \land C \in R) \land A \in (R^{V})) \to Fun A$
28		simpr	$⊢ ((M \in Ring \land V \in X \land C \in R) \land A \in (R^{V})) \to A \in (R^{V})$
29		suppval1	$⊢ (Fun A \land A \in (R^{V}) \land 0_{M} \in V) \to A supp 0_{M} = \{w \in dom A \| A (w) \neq 0_{M}\}$
30	27 28 23 29	syl3anc	$⊢ ((M \in Ring \land V \in X \land C \in R) \land A \in (R^{V})) \to A supp 0_{M} = \{w \in dom A \| A (w) \neq 0_{M}\}$
31	18 25 30	3sstr4d	$⊢ ((M \in Ring \land V \in X \land C \in R) \land A \in (R^{V})) \to (v \in V ⟼ C \cdot_{M} A (v)) supp 0_{M} \subseteq A supp 0_{M}$

Metamath Proof Explorer

Theorem rmsuppss

Proof