Metamath Proof Explorer

Theorem mndpsuppfi

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
Hypothesis mndpsuppfi.r 
|- R = ( Base ` M )
Assertion mndpsuppfi 
|- ( ( ( M e. Mnd /\ V e. X ) /\ ( A e. ( R ^m V ) /\ B e. ( R ^m V ) ) /\ ( ( A supp ( 0g ` M ) ) e. Fin /\ ( B supp ( 0g ` M ) ) e. Fin ) ) -> ( ( A oF ( +g ` M ) B ) supp ( 0g ` M ) ) e. Fin )

Proof

Step Hyp Ref Expression
1 mndpsuppfi.r 
 |-  R = ( Base ` M )
2 unfi 
 |-  ( ( ( A supp ( 0g ` M ) ) e. Fin /\ ( B supp ( 0g ` M ) ) e. Fin ) -> ( ( A supp ( 0g ` M ) ) u. ( B supp ( 0g ` M ) ) ) e. Fin )
3 2 3ad2ant3 
 |-  ( ( ( M e. Mnd /\ V e. X ) /\ ( A e. ( R ^m V ) /\ B e. ( R ^m V ) ) /\ ( ( A supp ( 0g ` M ) ) e. Fin /\ ( B supp ( 0g ` M ) ) e. Fin ) ) -> ( ( A supp ( 0g ` M ) ) u. ( B supp ( 0g ` M ) ) ) e. Fin )
4 1 mndpsuppss 
 |-  ( ( ( M e. Mnd /\ V e. X ) /\ ( A e. ( R ^m V ) /\ B e. ( R ^m V ) ) ) -> ( ( A oF ( +g ` M ) B ) supp ( 0g ` M ) ) C_ ( ( A supp ( 0g ` M ) ) u. ( B supp ( 0g ` M ) ) ) )
5 4 3adant3 
 |-  ( ( ( M e. Mnd /\ V e. X ) /\ ( A e. ( R ^m V ) /\ B e. ( R ^m V ) ) /\ ( ( A supp ( 0g ` M ) ) e. Fin /\ ( B supp ( 0g ` M ) ) e. Fin ) ) -> ( ( A oF ( +g ` M ) B ) supp ( 0g ` M ) ) C_ ( ( A supp ( 0g ` M ) ) u. ( B supp ( 0g ` M ) ) ) )
6 ssfi 
 |-  ( ( ( ( A supp ( 0g ` M ) ) u. ( B supp ( 0g ` M ) ) ) e. Fin /\ ( ( A oF ( +g ` M ) B ) supp ( 0g ` M ) ) C_ ( ( A supp ( 0g ` M ) ) u. ( B supp ( 0g ` M ) ) ) ) -> ( ( A oF ( +g ` M ) B ) supp ( 0g ` M ) ) e. Fin )
7 3 5 6 syl2anc 
 |-  ( ( ( M e. Mnd /\ V e. X ) /\ ( A e. ( R ^m V ) /\ B e. ( R ^m V ) ) /\ ( ( A supp ( 0g ` M ) ) e. Fin /\ ( B supp ( 0g ` M ) ) e. Fin ) ) -> ( ( A oF ( +g ` M ) B ) supp ( 0g ` M ) ) e. Fin )