Theorem scmfsupp

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
Hypotheses	scmsuppfi.s	|- S = ( Scalar ` M )
	scmsuppfi.r	|- R = ( Base ` S )
Assertion	scmfsupp	|- ( ( ( M e. LMod /\ V e. ~P ( Base ` M ) ) /\ A e. ( R ^m V ) /\ A finSupp ( 0g ` S ) ) -> ( v e. V |-> ( ( A ` v ) ( .s ` M ) v ) ) finSupp ( 0g ` M ) )

Proof

Step	Hyp	Ref	Expression
1		scmsuppfi.s	|- S = ( Scalar ` M )
2		scmsuppfi.r	|- R = ( Base ` S )
3		funmpt	|- Fun ( v e. V |-> ( ( A ` v ) ( .s ` M ) v ) )
4	3	a1i	|- ( ( ( M e. LMod /\ V e. ~P ( Base ` M ) ) /\ A e. ( R ^m V ) /\ A finSupp ( 0g ` S ) ) -> Fun ( v e. V |-> ( ( A ` v ) ( .s ` M ) v ) ) )
5		id	|- ( A finSupp ( 0g ` S ) -> A finSupp ( 0g ` S ) )
6	5	fsuppimpd	|- ( A finSupp ( 0g ` S ) -> ( A supp ( 0g ` S ) ) e. Fin )
7	1 2	scmsuppfi	|- ( ( ( M e. LMod /\ V e. ~P ( Base ` M ) ) /\ A e. ( R ^m V ) /\ ( A supp ( 0g ` S ) ) e. Fin ) -> ( ( v e. V |-> ( ( A ` v ) ( .s ` M ) v ) ) supp ( 0g ` M ) ) e. Fin )
8	6 7	syl3an3	|- ( ( ( M e. LMod /\ V e. ~P ( Base ` M ) ) /\ A e. ( R ^m V ) /\ A finSupp ( 0g ` S ) ) -> ( ( v e. V |-> ( ( A ` v ) ( .s ` M ) v ) ) supp ( 0g ` M ) ) e. Fin )
9		mptexg	|- ( V e. ~P ( Base ` M ) -> ( v e. V |-> ( ( A ` v ) ( .s ` M ) v ) ) e. _V )
10	9	adantl	|- ( ( M e. LMod /\ V e. ~P ( Base ` M ) ) -> ( v e. V |-> ( ( A ` v ) ( .s ` M ) v ) ) e. _V )
11	10	3ad2ant1	|- ( ( ( M e. LMod /\ V e. ~P ( Base ` M ) ) /\ A e. ( R ^m V ) /\ A finSupp ( 0g ` S ) ) -> ( v e. V |-> ( ( A ` v ) ( .s ` M ) v ) ) e. _V )
12		fvex	|- ( 0g ` M ) e. _V
13		isfsupp	|- ( ( ( v e. V |-> ( ( A ` v ) ( .s ` M ) v ) ) e. _V /\ ( 0g ` M ) e. _V ) -> ( ( v e. V |-> ( ( A ` v ) ( .s ` M ) v ) ) finSupp ( 0g ` M ) <-> ( Fun ( v e. V |-> ( ( A ` v ) ( .s ` M ) v ) ) /\ ( ( v e. V |-> ( ( A ` v ) ( .s ` M ) v ) ) supp ( 0g ` M ) ) e. Fin ) ) )
14	11 12 13	sylancl	|- ( ( ( M e. LMod /\ V e. ~P ( Base ` M ) ) /\ A e. ( R ^m V ) /\ A finSupp ( 0g ` S ) ) -> ( ( v e. V |-> ( ( A ` v ) ( .s ` M ) v ) ) finSupp ( 0g ` M ) <-> ( Fun ( v e. V |-> ( ( A ` v ) ( .s ` M ) v ) ) /\ ( ( v e. V |-> ( ( A ` v ) ( .s ` M ) v ) ) supp ( 0g ` M ) ) e. Fin ) ) )
15	4 8 14	mpbir2and	|- ( ( ( M e. LMod /\ V e. ~P ( Base ` M ) ) /\ A e. ( R ^m V ) /\ A finSupp ( 0g ` S ) ) -> ( v e. V |-> ( ( A ` v ) ( .s ` M ) v ) ) finSupp ( 0g ` M ) )