mndpfsupp

Description: A mapping of a scalar multiplication with a function of scalars is finitely supported if the function of scalars is finitely supported. (Contributed by AV, 9-Jun-2019)

		Ref	Expression
	Hypothesis	mndpsuppfi.r	$⊢ R = {Base}_{M}$
	Assertion	mndpfsupp	$⊢ ((M \in Mnd \land V \in X) \land (A \in (R^{V}) \land B \in (R^{V})) \land ({finSupp}_{0_{M}} (A) \land {finSupp}_{0_{M}} (B))) \to {finSupp}_{0_{M}} ((A {+_{M}}_{f} B))$

Proof

Step	Hyp	Ref	Expression
1		mndpsuppfi.r	$⊢ R = {Base}_{M}$
2		elmapfn	$⊢ A \in (R^{V}) \to A Fn V$
3	2	adantr	$⊢ (A \in (R^{V}) \land B \in (R^{V})) \to A Fn V$
4	3	3ad2ant2	$⊢ ((M \in Mnd \land V \in X) \land (A \in (R^{V}) \land B \in (R^{V})) \land ({finSupp}_{0_{M}} (A) \land {finSupp}_{0_{M}} (B))) \to A Fn V$
5		elmapfn	$⊢ B \in (R^{V}) \to B Fn V$
6	5	adantl	$⊢ (A \in (R^{V}) \land B \in (R^{V})) \to B Fn V$
7	6	3ad2ant2	$⊢ ((M \in Mnd \land V \in X) \land (A \in (R^{V}) \land B \in (R^{V})) \land ({finSupp}_{0_{M}} (A) \land {finSupp}_{0_{M}} (B))) \to B Fn V$
8		simp1r	$⊢ ((M \in Mnd \land V \in X) \land (A \in (R^{V}) \land B \in (R^{V})) \land ({finSupp}_{0_{M}} (A) \land {finSupp}_{0_{M}} (B))) \to V \in X$
9		inidm	$⊢ V \cap V = V$
10	4 7 8 8 9	offn	$⊢ ((M \in Mnd \land V \in X) \land (A \in (R^{V}) \land B \in (R^{V})) \land ({finSupp}_{0_{M}} (A) \land {finSupp}_{0_{M}} (B))) \to (A {+_{M}}_{f} B) Fn V$
11		fnfun	$⊢ (A {+_{M}}_{f} B) Fn V \to Fun (A {+_{M}}_{f} B)$
12	10 11	syl	$⊢ ((M \in Mnd \land V \in X) \land (A \in (R^{V}) \land B \in (R^{V})) \land ({finSupp}_{0_{M}} (A) \land {finSupp}_{0_{M}} (B))) \to Fun (A {+_{M}}_{f} B)$
13		id	$⊢ {finSupp}_{0_{M}} (A) \to {finSupp}_{0_{M}} (A)$
14	13	fsuppimpd	$⊢ {finSupp}_{0_{M}} (A) \to A supp 0_{M} \in Fin$
15		id	$⊢ {finSupp}_{0_{M}} (B) \to {finSupp}_{0_{M}} (B)$
16	15	fsuppimpd	$⊢ {finSupp}_{0_{M}} (B) \to B supp 0_{M} \in Fin$
17	14 16	anim12i	$⊢ ({finSupp}_{0_{M}} (A) \land {finSupp}_{0_{M}} (B)) \to (A supp 0_{M} \in Fin \land B supp 0_{M} \in Fin)$
18	1	mndpsuppfi	$⊢ ((M \in Mnd \land V \in X) \land (A \in (R^{V}) \land B \in (R^{V})) \land (A supp 0_{M} \in Fin \land B supp 0_{M} \in Fin)) \to (A {+_{M}}_{f} B) supp 0_{M} \in Fin$
19	17 18	syl3an3	$⊢ ((M \in Mnd \land V \in X) \land (A \in (R^{V}) \land B \in (R^{V})) \land ({finSupp}_{0_{M}} (A) \land {finSupp}_{0_{M}} (B))) \to (A {+_{M}}_{f} B) supp 0_{M} \in Fin$
20		ovex	$⊢ A {+_{M}}_{f} B \in V$
21		fvexd	$⊢ ((M \in Mnd \land V \in X) \land (A \in (R^{V}) \land B \in (R^{V})) \land ({finSupp}_{0_{M}} (A) \land {finSupp}_{0_{M}} (B))) \to 0_{M} \in V$
22		isfsupp	$⊢ (A {+_{M}}_{f} B \in V \land 0_{M} \in V) \to ({finSupp}_{0_{M}} ((A {+_{M}}_{f} B)) \leftrightarrow (Fun (A {+_{M}}_{f} B) \land (A {+_{M}}_{f} B) supp 0_{M} \in Fin))$
23	20 21 22	sylancr	$⊢ ((M \in Mnd \land V \in X) \land (A \in (R^{V}) \land B \in (R^{V})) \land ({finSupp}_{0_{M}} (A) \land {finSupp}_{0_{M}} (B))) \to ({finSupp}_{0_{M}} ((A {+_{M}}_{f} B)) \leftrightarrow (Fun (A {+_{M}}_{f} B) \land (A {+_{M}}_{f} B) supp 0_{M} \in Fin))$
24	12 19 23	mpbir2and	$⊢ ((M \in Mnd \land V \in X) \land (A \in (R^{V}) \land B \in (R^{V})) \land ({finSupp}_{0_{M}} (A) \land {finSupp}_{0_{M}} (B))) \to {finSupp}_{0_{M}} ((A {+_{M}}_{f} B))$

Metamath Proof Explorer

Theorem mndpfsupp

Proof