Metamath Proof Explorer

Theorem rmfsupp

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

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

Proof

Step Hyp Ref Expression
1 rmsuppfi.r 
 |-  R = ( Base ` M )
2 funmpt 
 |-  Fun ( v e. V |-> ( C ( .r ` M ) ( A ` v ) ) )
3 2 a1i 
 |-  ( ( ( M e. Ring /\ V e. X /\ C e. R ) /\ A e. ( R ^m V ) /\ A finSupp ( 0g ` M ) ) -> Fun ( v e. V |-> ( C ( .r ` M ) ( A ` v ) ) ) )
4 id 
 |-  ( A finSupp ( 0g ` M ) -> A finSupp ( 0g ` M ) )
5 4 fsuppimpd 
 |-  ( A finSupp ( 0g ` M ) -> ( A supp ( 0g ` M ) ) e. Fin )
6 1 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 )
7 5 6 syl3an3 
 |-  ( ( ( M e. Ring /\ V e. X /\ C e. R ) /\ A e. ( R ^m V ) /\ A finSupp ( 0g ` M ) ) -> ( ( v e. V |-> ( C ( .r ` M ) ( A ` v ) ) ) supp ( 0g ` M ) ) e. Fin )
8 mptexg 
 |-  ( V e. X -> ( v e. V |-> ( C ( .r ` M ) ( A ` v ) ) ) e. _V )
9 8 3ad2ant2 
 |-  ( ( M e. Ring /\ V e. X /\ C e. R ) -> ( v e. V |-> ( C ( .r ` M ) ( A ` v ) ) ) e. _V )
10 9 3ad2ant1 
 |-  ( ( ( M e. Ring /\ V e. X /\ C e. R ) /\ A e. ( R ^m V ) /\ A finSupp ( 0g ` M ) ) -> ( v e. V |-> ( C ( .r ` M ) ( A ` v ) ) ) e. _V )
11 fvex 
 |-  ( 0g ` M ) e. _V
12 isfsupp 
 |-  ( ( ( v e. V |-> ( C ( .r ` M ) ( A ` v ) ) ) e. _V /\ ( 0g ` M ) e. _V ) -> ( ( v e. V |-> ( C ( .r ` M ) ( A ` v ) ) ) finSupp ( 0g ` M ) <-> ( Fun ( v e. V |-> ( C ( .r ` M ) ( A ` v ) ) ) /\ ( ( v e. V |-> ( C ( .r ` M ) ( A ` v ) ) ) supp ( 0g ` M ) ) e. Fin ) ) )
13 10 11 12 sylancl 
 |-  ( ( ( M e. Ring /\ V e. X /\ C e. R ) /\ A e. ( R ^m V ) /\ A finSupp ( 0g ` M ) ) -> ( ( v e. V |-> ( C ( .r ` M ) ( A ` v ) ) ) finSupp ( 0g ` M ) <-> ( Fun ( v e. V |-> ( C ( .r ` M ) ( A ` v ) ) ) /\ ( ( v e. V |-> ( C ( .r ` M ) ( A ` v ) ) ) supp ( 0g ` M ) ) e. Fin ) ) )
14 3 7 13 mpbir2and 
 |-  ( ( ( M e. Ring /\ V e. X /\ C e. R ) /\ A e. ( R ^m V ) /\ A finSupp ( 0g ` M ) ) -> ( v e. V |-> ( C ( .r ` M ) ( A ` v ) ) ) finSupp ( 0g ` M ) )