domnmsuppn0

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

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

Proof

Step	Hyp	Ref	Expression
1		rmsuppss.r	$⊢ R = {Base}_{M}$
2		elmapi	$⊢ A \in (R^{V}) \to A : V ⟶ R$
3		fdm	$⊢ A : V ⟶ R \to dom A = V$
4	3	eqcomd	$⊢ A : V ⟶ R \to V = dom A$
5	2 4	syl	$⊢ A \in (R^{V}) \to V = dom A$
6	5	3ad2ant3	$⊢ ((M \in Domn \land V \in X) \land (C \in R \land C \neq 0_{M}) \land A \in (R^{V})) \to V = dom A$
7		oveq2	$⊢ A (w) = 0_{M} \to C \cdot_{M} A (w) = C \cdot_{M} 0_{M}$
8		domnring	$⊢ M \in Domn \to M \in Ring$
9	8	adantr	$⊢ (M \in Domn \land V \in X) \to M \in Ring$
10		simpl	$⊢ (C \in R \land C \neq 0_{M}) \to C \in R$
11	9 10	anim12i	$⊢ ((M \in Domn \land V \in X) \land (C \in R \land C \neq 0_{M})) \to (M \in Ring \land C \in R)$
12	11	3adant3	$⊢ ((M \in Domn \land V \in X) \land (C \in R \land C \neq 0_{M}) \land A \in (R^{V})) \to (M \in Ring \land C \in R)$
13		eqid	$⊢ \cdot_{M} = \cdot_{M}$
14		eqid	$⊢ 0_{M} = 0_{M}$
15	1 13 14	ringrz	$⊢ (M \in Ring \land C \in R) \to C \cdot_{M} 0_{M} = 0_{M}$
16	12 15	syl	$⊢ ((M \in Domn \land V \in X) \land (C \in R \land C \neq 0_{M}) \land A \in (R^{V})) \to C \cdot_{M} 0_{M} = 0_{M}$
17	16	adantr	$⊢ (((M \in Domn \land V \in X) \land (C \in R \land C \neq 0_{M}) \land A \in (R^{V})) \land w \in V) \to C \cdot_{M} 0_{M} = 0_{M}$
18	7 17	sylan9eqr	$⊢ ((((M \in Domn \land V \in X) \land (C \in R \land C \neq 0_{M}) \land A \in (R^{V})) \land w \in V) \land A (w) = 0_{M}) \to C \cdot_{M} A (w) = 0_{M}$
19	18	ex	$⊢ (((M \in Domn \land V \in X) \land (C \in R \land C \neq 0_{M}) \land A \in (R^{V})) \land w \in V) \to (A (w) = 0_{M} \to C \cdot_{M} A (w) = 0_{M})$
20	19	necon3d	$⊢ (((M \in Domn \land V \in X) \land (C \in R \land C \neq 0_{M}) \land A \in (R^{V})) \land w \in V) \to (C \cdot_{M} A (w) \neq 0_{M} \to A (w) \neq 0_{M})$
21		simpl1l	$⊢ (((M \in Domn \land V \in X) \land (C \in R \land C \neq 0_{M}) \land A \in (R^{V})) \land w \in V) \to M \in Domn$
22	21	adantr	$⊢ ((((M \in Domn \land V \in X) \land (C \in R \land C \neq 0_{M}) \land A \in (R^{V})) \land w \in V) \land A (w) \neq 0_{M}) \to M \in Domn$
23		simpll2	$⊢ ((((M \in Domn \land V \in X) \land (C \in R \land C \neq 0_{M}) \land A \in (R^{V})) \land w \in V) \land A (w) \neq 0_{M}) \to (C \in R \land C \neq 0_{M})$
24		ffvelcdm	$⊢ (A : V ⟶ R \land w \in V) \to A (w) \in R$
25	24	ex	$⊢ A : V ⟶ R \to (w \in V \to A (w) \in R)$
26	2 25	syl	$⊢ A \in (R^{V}) \to (w \in V \to A (w) \in R)$
27	26	3ad2ant3	$⊢ ((M \in Domn \land V \in X) \land (C \in R \land C \neq 0_{M}) \land A \in (R^{V})) \to (w \in V \to A (w) \in R)$
28	27	imp	$⊢ (((M \in Domn \land V \in X) \land (C \in R \land C \neq 0_{M}) \land A \in (R^{V})) \land w \in V) \to A (w) \in R$
29	28	adantr	$⊢ ((((M \in Domn \land V \in X) \land (C \in R \land C \neq 0_{M}) \land A \in (R^{V})) \land w \in V) \land A (w) \neq 0_{M}) \to A (w) \in R$
30		simpr	$⊢ ((((M \in Domn \land V \in X) \land (C \in R \land C \neq 0_{M}) \land A \in (R^{V})) \land w \in V) \land A (w) \neq 0_{M}) \to A (w) \neq 0_{M}$
31	1 13 14	domnmuln0	$⊢ (M \in Domn \land (C \in R \land C \neq 0_{M}) \land (A (w) \in R \land A (w) \neq 0_{M})) \to C \cdot_{M} A (w) \neq 0_{M}$
32	22 23 29 30 31	syl112anc	$⊢ ((((M \in Domn \land V \in X) \land (C \in R \land C \neq 0_{M}) \land A \in (R^{V})) \land w \in V) \land A (w) \neq 0_{M}) \to C \cdot_{M} A (w) \neq 0_{M}$
33	32	ex	$⊢ (((M \in Domn \land V \in X) \land (C \in R \land C \neq 0_{M}) \land A \in (R^{V})) \land w \in V) \to (A (w) \neq 0_{M} \to C \cdot_{M} A (w) \neq 0_{M})$
34	20 33	impbid	$⊢ (((M \in Domn \land V \in X) \land (C \in R \land C \neq 0_{M}) \land A \in (R^{V})) \land w \in V) \to (C \cdot_{M} A (w) \neq 0_{M} \leftrightarrow A (w) \neq 0_{M})$
35	6 34	rabeqbidva	$⊢ ((M \in Domn \land V \in X) \land (C \in R \land C \neq 0_{M}) \land A \in (R^{V})) \to \{w \in V \| C \cdot_{M} A (w) \neq 0_{M}\} = \{w \in dom A \| A (w) \neq 0_{M}\}$
36		fveq2	$⊢ v = w \to A (v) = A (w)$
37	36	oveq2d	$⊢ v = w \to C \cdot_{M} A (v) = C \cdot_{M} A (w)$
38	37	cbvmptv	$⊢ (v \in V ⟼ C \cdot_{M} A (v)) = (w \in V ⟼ C \cdot_{M} A (w))$
39		simp1r	$⊢ ((M \in Domn \land V \in X) \land (C \in R \land C \neq 0_{M}) \land A \in (R^{V})) \to V \in X$
40		fvexd	$⊢ ((M \in Domn \land V \in X) \land (C \in R \land C \neq 0_{M}) \land A \in (R^{V})) \to 0_{M} \in V$
41		ovexd	$⊢ (((M \in Domn \land V \in X) \land (C \in R \land C \neq 0_{M}) \land A \in (R^{V})) \land w \in V) \to C \cdot_{M} A (w) \in V$
42	38 39 40 41	mptsuppd	$⊢ ((M \in Domn \land V \in X) \land (C \in R \land C \neq 0_{M}) \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}\}$
43		elmapfun	$⊢ A \in (R^{V}) \to Fun A$
44	43	3ad2ant3	$⊢ ((M \in Domn \land V \in X) \land (C \in R \land C \neq 0_{M}) \land A \in (R^{V})) \to Fun A$
45		simp3	$⊢ ((M \in Domn \land V \in X) \land (C \in R \land C \neq 0_{M}) \land A \in (R^{V})) \to A \in (R^{V})$
46		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}\}$
47	44 45 40 46	syl3anc	$⊢ ((M \in Domn \land V \in X) \land (C \in R \land C \neq 0_{M}) \land A \in (R^{V})) \to A supp 0_{M} = \{w \in dom A \| A (w) \neq 0_{M}\}$
48	35 42 47	3eqtr4d	$⊢ ((M \in Domn \land V \in X) \land (C \in R \land C \neq 0_{M}) \land A \in (R^{V})) \to (v \in V ⟼ C \cdot_{M} A (v)) supp 0_{M} = A supp 0_{M}$

Metamath Proof Explorer

Theorem domnmsuppn0

Proof