mndpsuppss

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
	Hypothesis	mndpsuppss.r	$⊢ R = {Base}_{M}$
	Assertion	mndpsuppss	$⊢ ((M \in Mnd \land V \in X) \land (A \in (R^{V}) \land B \in (R^{V}))) \to (A {+_{M}}_{f} B) supp 0_{M} \subseteq {supp}_{0_{M}} (A) \cup {supp}_{0_{M}} (B)$

Proof

Step	Hyp	Ref	Expression
1		mndpsuppss.r	$⊢ R = {Base}_{M}$
2		ioran	$⊢ \neg (A (x) \neq 0_{M} \lor B (x) \neq 0_{M}) \leftrightarrow (\neg A (x) \neq 0_{M} \land \neg B (x) \neq 0_{M})$
3		nne	$⊢ \neg A (x) \neq 0_{M} \leftrightarrow A (x) = 0_{M}$
4		nne	$⊢ \neg B (x) \neq 0_{M} \leftrightarrow B (x) = 0_{M}$
5	3 4	anbi12i	$⊢ (\neg A (x) \neq 0_{M} \land \neg B (x) \neq 0_{M}) \leftrightarrow (A (x) = 0_{M} \land B (x) = 0_{M})$
6	2 5	bitri	$⊢ \neg (A (x) \neq 0_{M} \lor B (x) \neq 0_{M}) \leftrightarrow (A (x) = 0_{M} \land B (x) = 0_{M})$
7		elmapfn	$⊢ A \in (R^{V}) \to A Fn V$
8	7	ad2antrl	$⊢ ((M \in Mnd \land V \in X) \land (A \in (R^{V}) \land B \in (R^{V}))) \to A Fn V$
9	8	adantr	$⊢ (((M \in Mnd \land V \in X) \land (A \in (R^{V}) \land B \in (R^{V}))) \land (A (x) = 0_{M} \land B (x) = 0_{M})) \to A Fn V$
10		elmapfn	$⊢ B \in (R^{V}) \to B Fn V$
11	10	ad2antll	$⊢ ((M \in Mnd \land V \in X) \land (A \in (R^{V}) \land B \in (R^{V}))) \to B Fn V$
12	11	adantr	$⊢ (((M \in Mnd \land V \in X) \land (A \in (R^{V}) \land B \in (R^{V}))) \land (A (x) = 0_{M} \land B (x) = 0_{M})) \to B Fn V$
13		simplr	$⊢ ((M \in Mnd \land V \in X) \land (A \in (R^{V}) \land B \in (R^{V}))) \to V \in X$
14	13	adantr	$⊢ (((M \in Mnd \land V \in X) \land (A \in (R^{V}) \land B \in (R^{V}))) \land (A (x) = 0_{M} \land B (x) = 0_{M})) \to V \in X$
15		inidm	$⊢ V \cap V = V$
16		simplrl	$⊢ ((((M \in Mnd \land V \in X) \land (A \in (R^{V}) \land B \in (R^{V}))) \land (A (x) = 0_{M} \land B (x) = 0_{M})) \land x \in V) \to A (x) = 0_{M}$
17		simplrr	$⊢ ((((M \in Mnd \land V \in X) \land (A \in (R^{V}) \land B \in (R^{V}))) \land (A (x) = 0_{M} \land B (x) = 0_{M})) \land x \in V) \to B (x) = 0_{M}$
18	9 12 14 14 15 16 17	ofval	$⊢ ((((M \in Mnd \land V \in X) \land (A \in (R^{V}) \land B \in (R^{V}))) \land (A (x) = 0_{M} \land B (x) = 0_{M})) \land x \in V) \to (A {+_{M}}_{f} B) (x) = 0_{M} +_{M} 0_{M}$
19	18	an32s	$⊢ ((((M \in Mnd \land V \in X) \land (A \in (R^{V}) \land B \in (R^{V}))) \land x \in V) \land (A (x) = 0_{M} \land B (x) = 0_{M})) \to (A {+_{M}}_{f} B) (x) = 0_{M} +_{M} 0_{M}$
20		eqid	$⊢ {Base}_{M} = {Base}_{M}$
21		eqid	$⊢ 0_{M} = 0_{M}$
22	20 21	mndidcl	$⊢ M \in Mnd \to 0_{M} \in {Base}_{M}$
23	22	ancli	$⊢ M \in Mnd \to (M \in Mnd \land 0_{M} \in {Base}_{M})$
24	23	ad4antr	$⊢ ((((M \in Mnd \land V \in X) \land (A \in (R^{V}) \land B \in (R^{V}))) \land x \in V) \land (A (x) = 0_{M} \land B (x) = 0_{M})) \to (M \in Mnd \land 0_{M} \in {Base}_{M})$
25		eqid	$⊢ +_{M} = +_{M}$
26	20 25 21	mndlid	$⊢ (M \in Mnd \land 0_{M} \in {Base}_{M}) \to 0_{M} +_{M} 0_{M} = 0_{M}$
27	24 26	syl	$⊢ ((((M \in Mnd \land V \in X) \land (A \in (R^{V}) \land B \in (R^{V}))) \land x \in V) \land (A (x) = 0_{M} \land B (x) = 0_{M})) \to 0_{M} +_{M} 0_{M} = 0_{M}$
28	19 27	eqtrd	$⊢ ((((M \in Mnd \land V \in X) \land (A \in (R^{V}) \land B \in (R^{V}))) \land x \in V) \land (A (x) = 0_{M} \land B (x) = 0_{M})) \to (A {+_{M}}_{f} B) (x) = 0_{M}$
29		nne	$⊢ \neg (A {+_{M}}_{f} B) (x) \neq 0_{M} \leftrightarrow (A {+_{M}}_{f} B) (x) = 0_{M}$
30	28 29	sylibr	$⊢ ((((M \in Mnd \land V \in X) \land (A \in (R^{V}) \land B \in (R^{V}))) \land x \in V) \land (A (x) = 0_{M} \land B (x) = 0_{M})) \to \neg (A {+_{M}}_{f} B) (x) \neq 0_{M}$
31	30	ex	$⊢ (((M \in Mnd \land V \in X) \land (A \in (R^{V}) \land B \in (R^{V}))) \land x \in V) \to ((A (x) = 0_{M} \land B (x) = 0_{M}) \to \neg (A {+_{M}}_{f} B) (x) \neq 0_{M})$
32	6 31	syl5bi	$⊢ (((M \in Mnd \land V \in X) \land (A \in (R^{V}) \land B \in (R^{V}))) \land x \in V) \to (\neg (A (x) \neq 0_{M} \lor B (x) \neq 0_{M}) \to \neg (A {+_{M}}_{f} B) (x) \neq 0_{M})$
33	32	con4d	$⊢ (((M \in Mnd \land V \in X) \land (A \in (R^{V}) \land B \in (R^{V}))) \land x \in V) \to ((A {+_{M}}_{f} B) (x) \neq 0_{M} \to (A (x) \neq 0_{M} \lor B (x) \neq 0_{M}))$
34	33	ss2rabdv	$⊢ ((M \in Mnd \land V \in X) \land (A \in (R^{V}) \land B \in (R^{V}))) \to \{x \in V \| (A {+_{M}}_{f} B) (x) \neq 0_{M}\} \subseteq \{x \in V \| (A (x) \neq 0_{M} \lor B (x) \neq 0_{M})\}$
35	8 11 13 13	offun	$⊢ ((M \in Mnd \land V \in X) \land (A \in (R^{V}) \land B \in (R^{V}))) \to Fun (A {+_{M}}_{f} B)$
36		ovexd	$⊢ ((M \in Mnd \land V \in X) \land (A \in (R^{V}) \land B \in (R^{V}))) \to A {+_{M}}_{f} B \in V$
37		fvexd	$⊢ ((M \in Mnd \land V \in X) \land (A \in (R^{V}) \land B \in (R^{V}))) \to 0_{M} \in V$
38		suppval1	$⊢ (Fun (A {+_{M}}_{f} B) \land A {+_{M}}_{f} B \in V \land 0_{M} \in V) \to (A {+_{M}}_{f} B) supp 0_{M} = \{x \in dom (A {+_{M}}_{f} B) \| (A {+_{M}}_{f} B) (x) \neq 0_{M}\}$
39	35 36 37 38	syl3anc	$⊢ ((M \in Mnd \land V \in X) \land (A \in (R^{V}) \land B \in (R^{V}))) \to (A {+_{M}}_{f} B) supp 0_{M} = \{x \in dom (A {+_{M}}_{f} B) \| (A {+_{M}}_{f} B) (x) \neq 0_{M}\}$
40	13 8 11	offvalfv	$⊢ ((M \in Mnd \land V \in X) \land (A \in (R^{V}) \land B \in (R^{V}))) \to A {+_{M}}_{f} B = (v \in V ⟼ A (v) +_{M} B (v))$
41	40	dmeqd	$⊢ ((M \in Mnd \land V \in X) \land (A \in (R^{V}) \land B \in (R^{V}))) \to dom (A {+_{M}}_{f} B) = dom (v \in V ⟼ A (v) +_{M} B (v))$
42		ovex	$⊢ A (v) +_{M} B (v) \in V$
43		eqid	$⊢ (v \in V ⟼ A (v) +_{M} B (v)) = (v \in V ⟼ A (v) +_{M} B (v))$
44	42 43	dmmpti	$⊢ dom (v \in V ⟼ A (v) +_{M} B (v)) = V$
45	41 44	eqtrdi	$⊢ ((M \in Mnd \land V \in X) \land (A \in (R^{V}) \land B \in (R^{V}))) \to dom (A {+_{M}}_{f} B) = V$
46	45	rabeqdv	$⊢ ((M \in Mnd \land V \in X) \land (A \in (R^{V}) \land B \in (R^{V}))) \to \{x \in dom (A {+_{M}}_{f} B) \| (A {+_{M}}_{f} B) (x) \neq 0_{M}\} = \{x \in V \| (A {+_{M}}_{f} B) (x) \neq 0_{M}\}$
47	39 46	eqtrd	$⊢ ((M \in Mnd \land V \in X) \land (A \in (R^{V}) \land B \in (R^{V}))) \to (A {+_{M}}_{f} B) supp 0_{M} = \{x \in V \| (A {+_{M}}_{f} B) (x) \neq 0_{M}\}$
48		elmapfun	$⊢ A \in (R^{V}) \to Fun A$
49		id	$⊢ A \in (R^{V}) \to A \in (R^{V})$
50		fvexd	$⊢ A \in (R^{V}) \to 0_{M} \in V$
51		suppval1	$⊢ (Fun A \land A \in (R^{V}) \land 0_{M} \in V) \to A supp 0_{M} = \{x \in dom A \| A (x) \neq 0_{M}\}$
52	48 49 50 51	syl3anc	$⊢ A \in (R^{V}) \to A supp 0_{M} = \{x \in dom A \| A (x) \neq 0_{M}\}$
53		elmapi	$⊢ A \in (R^{V}) \to A : V ⟶ R$
54		fdm	$⊢ A : V ⟶ R \to dom A = V$
55		rabeq	$⊢ dom A = V \to \{x \in dom A \| A (x) \neq 0_{M}\} = \{x \in V \| A (x) \neq 0_{M}\}$
56	53 54 55	3syl	$⊢ A \in (R^{V}) \to \{x \in dom A \| A (x) \neq 0_{M}\} = \{x \in V \| A (x) \neq 0_{M}\}$
57	52 56	eqtrd	$⊢ A \in (R^{V}) \to A supp 0_{M} = \{x \in V \| A (x) \neq 0_{M}\}$
58	57	ad2antrl	$⊢ ((M \in Mnd \land V \in X) \land (A \in (R^{V}) \land B \in (R^{V}))) \to A supp 0_{M} = \{x \in V \| A (x) \neq 0_{M}\}$
59		elmapfun	$⊢ B \in (R^{V}) \to Fun B$
60	59	ad2antll	$⊢ ((M \in Mnd \land V \in X) \land (A \in (R^{V}) \land B \in (R^{V}))) \to Fun B$
61		simprr	$⊢ ((M \in Mnd \land V \in X) \land (A \in (R^{V}) \land B \in (R^{V}))) \to B \in (R^{V})$
62		suppval1	$⊢ (Fun B \land B \in (R^{V}) \land 0_{M} \in V) \to B supp 0_{M} = \{x \in dom B \| B (x) \neq 0_{M}\}$
63	60 61 37 62	syl3anc	$⊢ ((M \in Mnd \land V \in X) \land (A \in (R^{V}) \land B \in (R^{V}))) \to B supp 0_{M} = \{x \in dom B \| B (x) \neq 0_{M}\}$
64		elmapi	$⊢ B \in (R^{V}) \to B : V ⟶ R$
65	64	fdmd	$⊢ B \in (R^{V}) \to dom B = V$
66	65	ad2antll	$⊢ ((M \in Mnd \land V \in X) \land (A \in (R^{V}) \land B \in (R^{V}))) \to dom B = V$
67	66	rabeqdv	$⊢ ((M \in Mnd \land V \in X) \land (A \in (R^{V}) \land B \in (R^{V}))) \to \{x \in dom B \| B (x) \neq 0_{M}\} = \{x \in V \| B (x) \neq 0_{M}\}$
68	63 67	eqtrd	$⊢ ((M \in Mnd \land V \in X) \land (A \in (R^{V}) \land B \in (R^{V}))) \to B supp 0_{M} = \{x \in V \| B (x) \neq 0_{M}\}$
69	58 68	uneq12d	$⊢ ((M \in Mnd \land V \in X) \land (A \in (R^{V}) \land B \in (R^{V}))) \to {supp}_{0_{M}} (A) \cup {supp}_{0_{M}} (B) = \{x \in V \| A (x) \neq 0_{M}\} \cup \{x \in V \| B (x) \neq 0_{M}\}$
70		unrab	$⊢ \{x \in V \| A (x) \neq 0_{M}\} \cup \{x \in V \| B (x) \neq 0_{M}\} = \{x \in V \| (A (x) \neq 0_{M} \lor B (x) \neq 0_{M})\}$
71	69 70	eqtrdi	$⊢ ((M \in Mnd \land V \in X) \land (A \in (R^{V}) \land B \in (R^{V}))) \to {supp}_{0_{M}} (A) \cup {supp}_{0_{M}} (B) = \{x \in V \| (A (x) \neq 0_{M} \lor B (x) \neq 0_{M})\}$
72	34 47 71	3sstr4d	$⊢ ((M \in Mnd \land V \in X) \land (A \in (R^{V}) \land B \in (R^{V}))) \to (A {+_{M}}_{f} B) supp 0_{M} \subseteq {supp}_{0_{M}} (A) \cup {supp}_{0_{M}} (B)$

Metamath Proof Explorer

Theorem mndpsuppss

Proof