Metamath Proof Explorer

Theorem scmsuppfi

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

Ref Expression
Hypotheses scmsuppfi.s 
|- S = ( Scalar ` M )
scmsuppfi.r 
|- R = ( Base ` S )
Assertion 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 )

Proof

Step Hyp Ref Expression
1 scmsuppfi.s 
 |-  S = ( Scalar ` M )
2 scmsuppfi.r 
 |-  R = ( Base ` S )
3 simp3 
 |-  ( ( ( M e. LMod /\ V e. ~P ( Base ` M ) ) /\ A e. ( R ^m V ) /\ ( A supp ( 0g ` S ) ) e. Fin ) -> ( A supp ( 0g ` S ) ) e. Fin )
4 simpll 
 |-  ( ( ( M e. LMod /\ V e. ~P ( Base ` M ) ) /\ A e. ( R ^m V ) ) -> M e. LMod )
5 simplr 
 |-  ( ( ( M e. LMod /\ V e. ~P ( Base ` M ) ) /\ A e. ( R ^m V ) ) -> V e. ~P ( Base ` M ) )
6 simpr 
 |-  ( ( ( M e. LMod /\ V e. ~P ( Base ` M ) ) /\ A e. ( R ^m V ) ) -> A e. ( R ^m V ) )
7 4 5 6 3jca 
 |-  ( ( ( M e. LMod /\ V e. ~P ( Base ` M ) ) /\ A e. ( R ^m V ) ) -> ( M e. LMod /\ V e. ~P ( Base ` M ) /\ A e. ( R ^m V ) ) )
8 7 3adant3 
 |-  ( ( ( M e. LMod /\ V e. ~P ( Base ` M ) ) /\ A e. ( R ^m V ) /\ ( A supp ( 0g ` S ) ) e. Fin ) -> ( M e. LMod /\ V e. ~P ( Base ` M ) /\ A e. ( R ^m V ) ) )
9 1 2 scmsuppss 
 |-  ( ( M e. LMod /\ V e. ~P ( Base ` M ) /\ A e. ( R ^m V ) ) -> ( ( v e. V |-> ( ( A ` v ) ( .s ` M ) v ) ) supp ( 0g ` M ) ) C_ ( A supp ( 0g ` S ) ) )
10 8 9 syl 
 |-  ( ( ( 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 ) ) C_ ( A supp ( 0g ` S ) ) )
11 ssfi 
 |-  ( ( ( A supp ( 0g ` S ) ) e. Fin /\ ( ( v e. V |-> ( ( A ` v ) ( .s ` M ) v ) ) supp ( 0g ` M ) ) C_ ( A supp ( 0g ` S ) ) ) -> ( ( v e. V |-> ( ( A ` v ) ( .s ` M ) v ) ) supp ( 0g ` M ) ) e. Fin )
12 3 10 11 syl2anc 
 |-  ( ( ( 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 )