Metamath Proof Explorer


Theorem scmfsupp

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
Hypotheses scmsuppfi.s 𝑆 = ( Scalar ‘ 𝑀 )
scmsuppfi.r 𝑅 = ( Base ‘ 𝑆 )
Assertion scmfsupp ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ 𝐴 ∈ ( 𝑅m 𝑉 ) ∧ 𝐴 finSupp ( 0g𝑆 ) ) → ( 𝑣𝑉 ↦ ( ( 𝐴𝑣 ) ( ·𝑠𝑀 ) 𝑣 ) ) finSupp ( 0g𝑀 ) )

Proof

Step Hyp Ref Expression
1 scmsuppfi.s 𝑆 = ( Scalar ‘ 𝑀 )
2 scmsuppfi.r 𝑅 = ( Base ‘ 𝑆 )
3 funmpt Fun ( 𝑣𝑉 ↦ ( ( 𝐴𝑣 ) ( ·𝑠𝑀 ) 𝑣 ) )
4 3 a1i ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ 𝐴 ∈ ( 𝑅m 𝑉 ) ∧ 𝐴 finSupp ( 0g𝑆 ) ) → Fun ( 𝑣𝑉 ↦ ( ( 𝐴𝑣 ) ( ·𝑠𝑀 ) 𝑣 ) ) )
5 id ( 𝐴 finSupp ( 0g𝑆 ) → 𝐴 finSupp ( 0g𝑆 ) )
6 5 fsuppimpd ( 𝐴 finSupp ( 0g𝑆 ) → ( 𝐴 supp ( 0g𝑆 ) ) ∈ Fin )
7 1 2 scmsuppfi ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ 𝐴 ∈ ( 𝑅m 𝑉 ) ∧ ( 𝐴 supp ( 0g𝑆 ) ) ∈ Fin ) → ( ( 𝑣𝑉 ↦ ( ( 𝐴𝑣 ) ( ·𝑠𝑀 ) 𝑣 ) ) supp ( 0g𝑀 ) ) ∈ Fin )
8 6 7 syl3an3 ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ 𝐴 ∈ ( 𝑅m 𝑉 ) ∧ 𝐴 finSupp ( 0g𝑆 ) ) → ( ( 𝑣𝑉 ↦ ( ( 𝐴𝑣 ) ( ·𝑠𝑀 ) 𝑣 ) ) supp ( 0g𝑀 ) ) ∈ Fin )
9 mptexg ( 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) → ( 𝑣𝑉 ↦ ( ( 𝐴𝑣 ) ( ·𝑠𝑀 ) 𝑣 ) ) ∈ V )
10 9 adantl ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) → ( 𝑣𝑉 ↦ ( ( 𝐴𝑣 ) ( ·𝑠𝑀 ) 𝑣 ) ) ∈ V )
11 10 3ad2ant1 ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ 𝐴 ∈ ( 𝑅m 𝑉 ) ∧ 𝐴 finSupp ( 0g𝑆 ) ) → ( 𝑣𝑉 ↦ ( ( 𝐴𝑣 ) ( ·𝑠𝑀 ) 𝑣 ) ) ∈ V )
12 fvex ( 0g𝑀 ) ∈ V
13 isfsupp ( ( ( 𝑣𝑉 ↦ ( ( 𝐴𝑣 ) ( ·𝑠𝑀 ) 𝑣 ) ) ∈ V ∧ ( 0g𝑀 ) ∈ V ) → ( ( 𝑣𝑉 ↦ ( ( 𝐴𝑣 ) ( ·𝑠𝑀 ) 𝑣 ) ) finSupp ( 0g𝑀 ) ↔ ( Fun ( 𝑣𝑉 ↦ ( ( 𝐴𝑣 ) ( ·𝑠𝑀 ) 𝑣 ) ) ∧ ( ( 𝑣𝑉 ↦ ( ( 𝐴𝑣 ) ( ·𝑠𝑀 ) 𝑣 ) ) supp ( 0g𝑀 ) ) ∈ Fin ) ) )
14 11 12 13 sylancl ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ 𝐴 ∈ ( 𝑅m 𝑉 ) ∧ 𝐴 finSupp ( 0g𝑆 ) ) → ( ( 𝑣𝑉 ↦ ( ( 𝐴𝑣 ) ( ·𝑠𝑀 ) 𝑣 ) ) finSupp ( 0g𝑀 ) ↔ ( Fun ( 𝑣𝑉 ↦ ( ( 𝐴𝑣 ) ( ·𝑠𝑀 ) 𝑣 ) ) ∧ ( ( 𝑣𝑉 ↦ ( ( 𝐴𝑣 ) ( ·𝑠𝑀 ) 𝑣 ) ) supp ( 0g𝑀 ) ) ∈ Fin ) ) )
15 4 8 14 mpbir2and ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ 𝐴 ∈ ( 𝑅m 𝑉 ) ∧ 𝐴 finSupp ( 0g𝑆 ) ) → ( 𝑣𝑉 ↦ ( ( 𝐴𝑣 ) ( ·𝑠𝑀 ) 𝑣 ) ) finSupp ( 0g𝑀 ) )