rmsupp0

Description: The support of a mapping of a multiplication of zero with a function into a ring is empty. (Contributed by AV, 10-Apr-2019)

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

Proof

Step	Hyp	Ref	Expression
1		rmsuppss.r	$⊢ R = {Base}_{M}$
2		fveq2	$⊢ v = w \to A (v) = A (w)$
3	2	oveq2d	$⊢ v = w \to C \cdot_{M} A (v) = C \cdot_{M} A (w)$
4	3	cbvmptv	$⊢ (v \in V ⟼ C \cdot_{M} A (v)) = (w \in V ⟼ C \cdot_{M} A (w))$
5		simpl2	$⊢ ((M \in Ring \land V \in X \land C = 0_{M}) \land A \in (R^{V})) \to V \in X$
6		fvexd	$⊢ ((M \in Ring \land V \in X \land C = 0_{M}) \land A \in (R^{V})) \to 0_{M} \in V$
7		ovexd	$⊢ (((M \in Ring \land V \in X \land C = 0_{M}) \land A \in (R^{V})) \land w \in V) \to C \cdot_{M} A (w) \in V$
8	4 5 6 7	mptsuppd	$⊢ ((M \in Ring \land V \in X \land C = 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}\}$
9		simpll3	$⊢ (((M \in Ring \land V \in X \land C = 0_{M}) \land A \in (R^{V})) \land w \in V) \to C = 0_{M}$
10	9	oveq1d	$⊢ (((M \in Ring \land V \in X \land C = 0_{M}) \land A \in (R^{V})) \land w \in V) \to C \cdot_{M} A (w) = 0_{M} \cdot_{M} A (w)$
11		simpll1	$⊢ (((M \in Ring \land V \in X \land C = 0_{M}) \land A \in (R^{V})) \land w \in V) \to M \in Ring$
12		elmapi	$⊢ A \in (R^{V}) \to A : V ⟶ R$
13		ffvelrn	$⊢ (A : V ⟶ R \land w \in V) \to A (w) \in R$
14	13 1	eleqtrdi	$⊢ (A : V ⟶ R \land w \in V) \to A (w) \in {Base}_{M}$
15	14	ex	$⊢ A : V ⟶ R \to (w \in V \to A (w) \in {Base}_{M})$
16	12 15	syl	$⊢ A \in (R^{V}) \to (w \in V \to A (w) \in {Base}_{M})$
17	16	adantl	$⊢ ((M \in Ring \land V \in X \land C = 0_{M}) \land A \in (R^{V})) \to (w \in V \to A (w) \in {Base}_{M})$
18	17	imp	$⊢ (((M \in Ring \land V \in X \land C = 0_{M}) \land A \in (R^{V})) \land w \in V) \to A (w) \in {Base}_{M}$
19		eqid	$⊢ {Base}_{M} = {Base}_{M}$
20		eqid	$⊢ \cdot_{M} = \cdot_{M}$
21		eqid	$⊢ 0_{M} = 0_{M}$
22	19 20 21	ringlz	$⊢ (M \in Ring \land A (w) \in {Base}_{M}) \to 0_{M} \cdot_{M} A (w) = 0_{M}$
23	11 18 22	syl2anc	$⊢ (((M \in Ring \land V \in X \land C = 0_{M}) \land A \in (R^{V})) \land w \in V) \to 0_{M} \cdot_{M} A (w) = 0_{M}$
24	10 23	eqtrd	$⊢ (((M \in Ring \land V \in X \land C = 0_{M}) \land A \in (R^{V})) \land w \in V) \to C \cdot_{M} A (w) = 0_{M}$
25	24	neeq1d	$⊢ (((M \in Ring \land V \in X \land C = 0_{M}) \land A \in (R^{V})) \land w \in V) \to (C \cdot_{M} A (w) \neq 0_{M} \leftrightarrow 0_{M} \neq 0_{M})$
26	25	rabbidva	$⊢ ((M \in Ring \land V \in X \land C = 0_{M}) \land A \in (R^{V})) \to \{w \in V \| C \cdot_{M} A (w) \neq 0_{M}\} = \{w \in V \| 0_{M} \neq 0_{M}\}$
27		neirr	$⊢ \neg 0_{M} \neq 0_{M}$
28	27	a1i	$⊢ ((M \in Ring \land V \in X \land C = 0_{M}) \land A \in (R^{V})) \to \neg 0_{M} \neq 0_{M}$
29	28	ralrimivw	$⊢ ((M \in Ring \land V \in X \land C = 0_{M}) \land A \in (R^{V})) \to \forall w \in V \neg 0_{M} \neq 0_{M}$
30		rabeq0	$⊢ \{w \in V \| 0_{M} \neq 0_{M}\} = \emptyset \leftrightarrow \forall w \in V \neg 0_{M} \neq 0_{M}$
31	29 30	sylibr	$⊢ ((M \in Ring \land V \in X \land C = 0_{M}) \land A \in (R^{V})) \to \{w \in V \| 0_{M} \neq 0_{M}\} = \emptyset$
32	8 26 31	3eqtrd	$⊢ ((M \in Ring \land V \in X \land C = 0_{M}) \land A \in (R^{V})) \to (v \in V ⟼ C \cdot_{M} A (v)) supp 0_{M} = \emptyset$

Metamath Proof Explorer

Theorem rmsupp0

Proof