Metamath Proof Explorer

Theorem mndpfsupp

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

Proof

Step Hyp Ref Expression
1 mndpsuppfi.r 
 |-  R = ( Base ` M )
2 elmapfn 
 |-  ( A e. ( R ^m V ) -> A Fn V )
3 2 adantr 
 |-  ( ( A e. ( R ^m V ) /\ B e. ( R ^m V ) ) -> A Fn V )
4 3 3ad2ant2 
 |-  ( ( ( M e. Mnd /\ V e. X ) /\ ( A e. ( R ^m V ) /\ B e. ( R ^m V ) ) /\ ( A finSupp ( 0g ` M ) /\ B finSupp ( 0g ` M ) ) ) -> A Fn V )
5 elmapfn 
 |-  ( B e. ( R ^m V ) -> B Fn V )
6 5 adantl 
 |-  ( ( A e. ( R ^m V ) /\ B e. ( R ^m V ) ) -> B Fn V )
7 6 3ad2ant2 
 |-  ( ( ( M e. Mnd /\ V e. X ) /\ ( A e. ( R ^m V ) /\ B e. ( R ^m V ) ) /\ ( A finSupp ( 0g ` M ) /\ B finSupp ( 0g ` M ) ) ) -> B Fn V )
8 simp1r 
 |-  ( ( ( M e. Mnd /\ V e. X ) /\ ( A e. ( R ^m V ) /\ B e. ( R ^m V ) ) /\ ( A finSupp ( 0g ` M ) /\ B finSupp ( 0g ` M ) ) ) -> V e. X )
9 4 7 8 8 offun 
 |-  ( ( ( M e. Mnd /\ V e. X ) /\ ( A e. ( R ^m V ) /\ B e. ( R ^m V ) ) /\ ( A finSupp ( 0g ` M ) /\ B finSupp ( 0g ` M ) ) ) -> Fun ( A oF ( +g ` M ) B ) )
10 id 
 |-  ( A finSupp ( 0g ` M ) -> A finSupp ( 0g ` M ) )
11 10 fsuppimpd 
 |-  ( A finSupp ( 0g ` M ) -> ( A supp ( 0g ` M ) ) e. Fin )
12 id 
 |-  ( B finSupp ( 0g ` M ) -> B finSupp ( 0g ` M ) )
13 12 fsuppimpd 
 |-  ( B finSupp ( 0g ` M ) -> ( B supp ( 0g ` M ) ) e. Fin )
14 11 13 anim12i 
 |-  ( ( A finSupp ( 0g ` M ) /\ B finSupp ( 0g ` M ) ) -> ( ( A supp ( 0g ` M ) ) e. Fin /\ ( B supp ( 0g ` M ) ) e. Fin ) )
15 1 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 )
16 14 15 syl3an3 
 |-  ( ( ( M e. Mnd /\ V e. X ) /\ ( A e. ( R ^m V ) /\ B e. ( R ^m V ) ) /\ ( A finSupp ( 0g ` M ) /\ B finSupp ( 0g ` M ) ) ) -> ( ( A oF ( +g ` M ) B ) supp ( 0g ` M ) ) e. Fin )
17 ovex 
 |-  ( A oF ( +g ` M ) B ) e. _V
18 fvexd 
 |-  ( ( ( M e. Mnd /\ V e. X ) /\ ( A e. ( R ^m V ) /\ B e. ( R ^m V ) ) /\ ( A finSupp ( 0g ` M ) /\ B finSupp ( 0g ` M ) ) ) -> ( 0g ` M ) e. _V )
19 isfsupp 
 |-  ( ( ( A oF ( +g ` M ) B ) e. _V /\ ( 0g ` M ) e. _V ) -> ( ( A oF ( +g ` M ) B ) finSupp ( 0g ` M ) <-> ( Fun ( A oF ( +g ` M ) B ) /\ ( ( A oF ( +g ` M ) B ) supp ( 0g ` M ) ) e. Fin ) ) )
20 17 18 19 sylancr 
 |-  ( ( ( M e. Mnd /\ V e. X ) /\ ( A e. ( R ^m V ) /\ B e. ( R ^m V ) ) /\ ( A finSupp ( 0g ` M ) /\ B finSupp ( 0g ` M ) ) ) -> ( ( A oF ( +g ` M ) B ) finSupp ( 0g ` M ) <-> ( Fun ( A oF ( +g ` M ) B ) /\ ( ( A oF ( +g ` M ) B ) supp ( 0g ` M ) ) e. Fin ) ) )
21 9 16 20 mpbir2and 
 |-  ( ( ( M e. Mnd /\ V e. X ) /\ ( A e. ( R ^m V ) /\ B e. ( R ^m V ) ) /\ ( A finSupp ( 0g ` M ) /\ B finSupp ( 0g ` M ) ) ) -> ( A oF ( +g ` M ) B ) finSupp ( 0g ` M ) )