Metamath Proof Explorer


Theorem rmsuppfi

Description: The support of a mapping of a multiplication of a constant with a function into a ring is finite if the support of the function is finite. (Contributed by AV, 11-Apr-2019)

Ref Expression
Hypothesis rmsuppfi.r
|- R = ( Base ` M )
Assertion rmsuppfi
|- ( ( ( M e. Ring /\ V e. X /\ C e. R ) /\ A e. ( R ^m V ) /\ ( A supp ( 0g ` M ) ) e. Fin ) -> ( ( v e. V |-> ( C ( .r ` M ) ( A ` v ) ) ) supp ( 0g ` M ) ) e. Fin )

Proof

Step Hyp Ref Expression
1 rmsuppfi.r
 |-  R = ( Base ` M )
2 simp3
 |-  ( ( ( M e. Ring /\ V e. X /\ C e. R ) /\ A e. ( R ^m V ) /\ ( A supp ( 0g ` M ) ) e. Fin ) -> ( A supp ( 0g ` M ) ) e. Fin )
3 1 rmsuppss
 |-  ( ( ( M e. Ring /\ V e. X /\ C e. R ) /\ A e. ( R ^m V ) ) -> ( ( v e. V |-> ( C ( .r ` M ) ( A ` v ) ) ) supp ( 0g ` M ) ) C_ ( A supp ( 0g ` M ) ) )
4 3 3adant3
 |-  ( ( ( M e. Ring /\ V e. X /\ C e. R ) /\ A e. ( R ^m V ) /\ ( A supp ( 0g ` M ) ) e. Fin ) -> ( ( v e. V |-> ( C ( .r ` M ) ( A ` v ) ) ) supp ( 0g ` M ) ) C_ ( A supp ( 0g ` M ) ) )
5 ssfi
 |-  ( ( ( A supp ( 0g ` M ) ) e. Fin /\ ( ( v e. V |-> ( C ( .r ` M ) ( A ` v ) ) ) supp ( 0g ` M ) ) C_ ( A supp ( 0g ` M ) ) ) -> ( ( v e. V |-> ( C ( .r ` M ) ( A ` v ) ) ) supp ( 0g ` M ) ) e. Fin )
6 2 4 5 syl2anc
 |-  ( ( ( M e. Ring /\ V e. X /\ C e. R ) /\ A e. ( R ^m V ) /\ ( A supp ( 0g ` M ) ) e. Fin ) -> ( ( v e. V |-> ( C ( .r ` M ) ( A ` v ) ) ) supp ( 0g ` M ) ) e. Fin )