scmsuppss

Description: The support of a mapping of a scalar multiplication with a function of scalars is a subset of the support of the function of scalars. (Contributed by AV, 5-Apr-2019)

	Ref	Expression
Hypotheses	scmsuppss.s	$⊢ S = Scalar (M)$
	scmsuppss.r	$⊢ R = {Base}_{S}$
Assertion	scmsuppss	$⊢ (M \in LMod \land V \in 𝒫 {Base}_{M} \land A \in (R^{V})) \to (v \in V ⟼ A (v) \cdot_{M} v) supp 0_{M} \subseteq A supp 0_{S}$

Proof

Step	Hyp	Ref	Expression
1		scmsuppss.s	$⊢ S = Scalar (M)$
2		scmsuppss.r	$⊢ R = {Base}_{S}$
3		elmapi	$⊢ A \in (R^{V}) \to A : V ⟶ R$
4		fdm	$⊢ A : V ⟶ R \to dom A = V$
5		eqidd	$⊢ (((dom A = V \land A : V ⟶ R) \land (V \in 𝒫 {Base}_{M} \land M \in LMod)) \land x \in V) \to (v \in V ⟼ A (v) \cdot_{M} v) = (v \in V ⟼ A (v) \cdot_{M} v)$
6		fveq2	$⊢ v = x \to A (v) = A (x)$
7		id	$⊢ v = x \to v = x$
8	6 7	oveq12d	$⊢ v = x \to A (v) \cdot_{M} v = A (x) \cdot_{M} x$
9	8	adantl	$⊢ ((((dom A = V \land A : V ⟶ R) \land (V \in 𝒫 {Base}_{M} \land M \in LMod)) \land x \in V) \land v = x) \to A (v) \cdot_{M} v = A (x) \cdot_{M} x$
10		simpr	$⊢ (((dom A = V \land A : V ⟶ R) \land (V \in 𝒫 {Base}_{M} \land M \in LMod)) \land x \in V) \to x \in V$
11		ovex	$⊢ A (x) \cdot_{M} x \in V$
12	11	a1i	$⊢ (((dom A = V \land A : V ⟶ R) \land (V \in 𝒫 {Base}_{M} \land M \in LMod)) \land x \in V) \to A (x) \cdot_{M} x \in V$
13	5 9 10 12	fvmptd	$⊢ (((dom A = V \land A : V ⟶ R) \land (V \in 𝒫 {Base}_{M} \land M \in LMod)) \land x \in V) \to (v \in V ⟼ A (v) \cdot_{M} v) (x) = A (x) \cdot_{M} x$
14	13	neeq1d	$⊢ (((dom A = V \land A : V ⟶ R) \land (V \in 𝒫 {Base}_{M} \land M \in LMod)) \land x \in V) \to ((v \in V ⟼ A (v) \cdot_{M} v) (x) \neq 0_{M} \leftrightarrow A (x) \cdot_{M} x \neq 0_{M})$
15		oveq1	$⊢ A (x) = 0_{S} \to A (x) \cdot_{M} x = 0_{S} \cdot_{M} x$
16		simplrr	$⊢ (((dom A = V \land A : V ⟶ R) \land (V \in 𝒫 {Base}_{M} \land M \in LMod)) \land x \in V) \to M \in LMod$
17		elelpwi	$⊢ (x \in V \land V \in 𝒫 {Base}_{M}) \to x \in {Base}_{M}$
18	17	expcom	$⊢ V \in 𝒫 {Base}_{M} \to (x \in V \to x \in {Base}_{M})$
19	18	adantr	$⊢ (V \in 𝒫 {Base}_{M} \land M \in LMod) \to (x \in V \to x \in {Base}_{M})$
20	19	adantl	$⊢ ((dom A = V \land A : V ⟶ R) \land (V \in 𝒫 {Base}_{M} \land M \in LMod)) \to (x \in V \to x \in {Base}_{M})$
21	20	imp	$⊢ (((dom A = V \land A : V ⟶ R) \land (V \in 𝒫 {Base}_{M} \land M \in LMod)) \land x \in V) \to x \in {Base}_{M}$
22		eqid	$⊢ {Base}_{M} = {Base}_{M}$
23		eqid	$⊢ \cdot_{M} = \cdot_{M}$
24		eqid	$⊢ 0_{S} = 0_{S}$
25		eqid	$⊢ 0_{M} = 0_{M}$
26	22 1 23 24 25	lmod0vs	$⊢ (M \in LMod \land x \in {Base}_{M}) \to 0_{S} \cdot_{M} x = 0_{M}$
27	16 21 26	syl2anc	$⊢ (((dom A = V \land A : V ⟶ R) \land (V \in 𝒫 {Base}_{M} \land M \in LMod)) \land x \in V) \to 0_{S} \cdot_{M} x = 0_{M}$
28	15 27	sylan9eqr	$⊢ ((((dom A = V \land A : V ⟶ R) \land (V \in 𝒫 {Base}_{M} \land M \in LMod)) \land x \in V) \land A (x) = 0_{S}) \to A (x) \cdot_{M} x = 0_{M}$
29	28	ex	$⊢ (((dom A = V \land A : V ⟶ R) \land (V \in 𝒫 {Base}_{M} \land M \in LMod)) \land x \in V) \to (A (x) = 0_{S} \to A (x) \cdot_{M} x = 0_{M})$
30	29	necon3d	$⊢ (((dom A = V \land A : V ⟶ R) \land (V \in 𝒫 {Base}_{M} \land M \in LMod)) \land x \in V) \to (A (x) \cdot_{M} x \neq 0_{M} \to A (x) \neq 0_{S})$
31	14 30	sylbid	$⊢ (((dom A = V \land A : V ⟶ R) \land (V \in 𝒫 {Base}_{M} \land M \in LMod)) \land x \in V) \to ((v \in V ⟼ A (v) \cdot_{M} v) (x) \neq 0_{M} \to A (x) \neq 0_{S})$
32	31	ss2rabdv	$⊢ ((dom A = V \land A : V ⟶ R) \land (V \in 𝒫 {Base}_{M} \land M \in LMod)) \to \{x \in V \| (v \in V ⟼ A (v) \cdot_{M} v) (x) \neq 0_{M}\} \subseteq \{x \in V \| A (x) \neq 0_{S}\}$
33		ovex	$⊢ A (v) \cdot_{M} v \in V$
34		eqid	$⊢ (v \in V ⟼ A (v) \cdot_{M} v) = (v \in V ⟼ A (v) \cdot_{M} v)$
35	33 34	dmmpti	$⊢ dom (v \in V ⟼ A (v) \cdot_{M} v) = V$
36		rabeq	$⊢ dom (v \in V ⟼ A (v) \cdot_{M} v) = V \to \{x \in dom (v \in V ⟼ A (v) \cdot_{M} v) \| (v \in V ⟼ A (v) \cdot_{M} v) (x) \neq 0_{M}\} = \{x \in V \| (v \in V ⟼ A (v) \cdot_{M} v) (x) \neq 0_{M}\}$
37	35 36	mp1i	$⊢ dom A = V \to \{x \in dom (v \in V ⟼ A (v) \cdot_{M} v) \| (v \in V ⟼ A (v) \cdot_{M} v) (x) \neq 0_{M}\} = \{x \in V \| (v \in V ⟼ A (v) \cdot_{M} v) (x) \neq 0_{M}\}$
38		rabeq	$⊢ dom A = V \to \{x \in dom A \| A (x) \neq 0_{S}\} = \{x \in V \| A (x) \neq 0_{S}\}$
39	37 38	sseq12d	$⊢ dom A = V \to (\{x \in dom (v \in V ⟼ A (v) \cdot_{M} v) \| (v \in V ⟼ A (v) \cdot_{M} v) (x) \neq 0_{M}\} \subseteq \{x \in dom A \| A (x) \neq 0_{S}\} \leftrightarrow \{x \in V \| (v \in V ⟼ A (v) \cdot_{M} v) (x) \neq 0_{M}\} \subseteq \{x \in V \| A (x) \neq 0_{S}\})$
40	39	adantr	$⊢ (dom A = V \land A : V ⟶ R) \to (\{x \in dom (v \in V ⟼ A (v) \cdot_{M} v) \| (v \in V ⟼ A (v) \cdot_{M} v) (x) \neq 0_{M}\} \subseteq \{x \in dom A \| A (x) \neq 0_{S}\} \leftrightarrow \{x \in V \| (v \in V ⟼ A (v) \cdot_{M} v) (x) \neq 0_{M}\} \subseteq \{x \in V \| A (x) \neq 0_{S}\})$
41	40	adantr	$⊢ ((dom A = V \land A : V ⟶ R) \land (V \in 𝒫 {Base}_{M} \land M \in LMod)) \to (\{x \in dom (v \in V ⟼ A (v) \cdot_{M} v) \| (v \in V ⟼ A (v) \cdot_{M} v) (x) \neq 0_{M}\} \subseteq \{x \in dom A \| A (x) \neq 0_{S}\} \leftrightarrow \{x \in V \| (v \in V ⟼ A (v) \cdot_{M} v) (x) \neq 0_{M}\} \subseteq \{x \in V \| A (x) \neq 0_{S}\})$
42	32 41	mpbird	$⊢ ((dom A = V \land A : V ⟶ R) \land (V \in 𝒫 {Base}_{M} \land M \in LMod)) \to \{x \in dom (v \in V ⟼ A (v) \cdot_{M} v) \| (v \in V ⟼ A (v) \cdot_{M} v) (x) \neq 0_{M}\} \subseteq \{x \in dom A \| A (x) \neq 0_{S}\}$
43	42	exp43	$⊢ dom A = V \to (A : V ⟶ R \to (V \in 𝒫 {Base}_{M} \to (M \in LMod \to \{x \in dom (v \in V ⟼ A (v) \cdot_{M} v) \| (v \in V ⟼ A (v) \cdot_{M} v) (x) \neq 0_{M}\} \subseteq \{x \in dom A \| A (x) \neq 0_{S}\})))$
44	4 43	mpcom	$⊢ A : V ⟶ R \to (V \in 𝒫 {Base}_{M} \to (M \in LMod \to \{x \in dom (v \in V ⟼ A (v) \cdot_{M} v) \| (v \in V ⟼ A (v) \cdot_{M} v) (x) \neq 0_{M}\} \subseteq \{x \in dom A \| A (x) \neq 0_{S}\}))$
45	3 44	syl	$⊢ A \in (R^{V}) \to (V \in 𝒫 {Base}_{M} \to (M \in LMod \to \{x \in dom (v \in V ⟼ A (v) \cdot_{M} v) \| (v \in V ⟼ A (v) \cdot_{M} v) (x) \neq 0_{M}\} \subseteq \{x \in dom A \| A (x) \neq 0_{S}\}))$
46	45	com13	$⊢ M \in LMod \to (V \in 𝒫 {Base}_{M} \to (A \in (R^{V}) \to \{x \in dom (v \in V ⟼ A (v) \cdot_{M} v) \| (v \in V ⟼ A (v) \cdot_{M} v) (x) \neq 0_{M}\} \subseteq \{x \in dom A \| A (x) \neq 0_{S}\}))$
47	46	3imp	$⊢ (M \in LMod \land V \in 𝒫 {Base}_{M} \land A \in (R^{V})) \to \{x \in dom (v \in V ⟼ A (v) \cdot_{M} v) \| (v \in V ⟼ A (v) \cdot_{M} v) (x) \neq 0_{M}\} \subseteq \{x \in dom A \| A (x) \neq 0_{S}\}$
48		funmpt	$⊢ Fun (v \in V ⟼ A (v) \cdot_{M} v)$
49	48	a1i	$⊢ (M \in LMod \land V \in 𝒫 {Base}_{M} \land A \in (R^{V})) \to Fun (v \in V ⟼ A (v) \cdot_{M} v)$
50		mptexg	$⊢ V \in 𝒫 {Base}_{M} \to (v \in V ⟼ A (v) \cdot_{M} v) \in V$
51	50	3ad2ant2	$⊢ (M \in LMod \land V \in 𝒫 {Base}_{M} \land A \in (R^{V})) \to (v \in V ⟼ A (v) \cdot_{M} v) \in V$
52		fvexd	$⊢ (M \in LMod \land V \in 𝒫 {Base}_{M} \land A \in (R^{V})) \to 0_{M} \in V$
53		suppval1	$⊢ (Fun (v \in V ⟼ A (v) \cdot_{M} v) \land (v \in V ⟼ A (v) \cdot_{M} v) \in V \land 0_{M} \in V) \to (v \in V ⟼ A (v) \cdot_{M} v) supp 0_{M} = \{x \in dom (v \in V ⟼ A (v) \cdot_{M} v) \| (v \in V ⟼ A (v) \cdot_{M} v) (x) \neq 0_{M}\}$
54	49 51 52 53	syl3anc	$⊢ (M \in LMod \land V \in 𝒫 {Base}_{M} \land A \in (R^{V})) \to (v \in V ⟼ A (v) \cdot_{M} v) supp 0_{M} = \{x \in dom (v \in V ⟼ A (v) \cdot_{M} v) \| (v \in V ⟼ A (v) \cdot_{M} v) (x) \neq 0_{M}\}$
55		elmapfun	$⊢ A \in (R^{V}) \to Fun A$
56	55	3ad2ant3	$⊢ (M \in LMod \land V \in 𝒫 {Base}_{M} \land A \in (R^{V})) \to Fun A$
57		simp3	$⊢ (M \in LMod \land V \in 𝒫 {Base}_{M} \land A \in (R^{V})) \to A \in (R^{V})$
58		fvexd	$⊢ (M \in LMod \land V \in 𝒫 {Base}_{M} \land A \in (R^{V})) \to 0_{S} \in V$
59		suppval1	$⊢ (Fun A \land A \in (R^{V}) \land 0_{S} \in V) \to A supp 0_{S} = \{x \in dom A \| A (x) \neq 0_{S}\}$
60	56 57 58 59	syl3anc	$⊢ (M \in LMod \land V \in 𝒫 {Base}_{M} \land A \in (R^{V})) \to A supp 0_{S} = \{x \in dom A \| A (x) \neq 0_{S}\}$
61	47 54 60	3sstr4d	$⊢ (M \in LMod \land V \in 𝒫 {Base}_{M} \land A \in (R^{V})) \to (v \in V ⟼ A (v) \cdot_{M} v) supp 0_{M} \subseteq A supp 0_{S}$

Metamath Proof Explorer

Theorem scmsuppss

Proof