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	4 7 8 8	offun	$⊢ ((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)$
10		id	$⊢ {finSupp}_{0_{M}} (A) \to {finSupp}_{0_{M}} (A)$
11	10	fsuppimpd	$⊢ {finSupp}_{0_{M}} (A) \to A supp 0_{M} \in Fin$
12		id	$⊢ {finSupp}_{0_{M}} (B) \to {finSupp}_{0_{M}} (B)$
13	12	fsuppimpd	$⊢ {finSupp}_{0_{M}} (B) \to B supp 0_{M} \in Fin$
14	11 13	anim12i	$⊢ ({finSupp}_{0_{M}} (A) \land {finSupp}_{0_{M}} (B)) \to (A supp 0_{M} \in Fin \land B supp 0_{M} \in Fin)$
15	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$
16	14 15	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$
17		ovex	$⊢ A {+_{M}}_{f} B \in V$
18		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$
19		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))$
20	17 18 19	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))$
21	9 16 20	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