Metamath Proof Explorer


Theorem scmsuppfi

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

Proof

Step Hyp Ref Expression
1 scmsuppfi.s 𝑆 = ( Scalar ‘ 𝑀 )
2 scmsuppfi.r 𝑅 = ( Base ‘ 𝑆 )
3 simp3 ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ 𝐴 ∈ ( 𝑅m 𝑉 ) ∧ ( 𝐴 supp ( 0g𝑆 ) ) ∈ Fin ) → ( 𝐴 supp ( 0g𝑆 ) ) ∈ Fin )
4 simpll ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ 𝐴 ∈ ( 𝑅m 𝑉 ) ) → 𝑀 ∈ LMod )
5 simplr ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ 𝐴 ∈ ( 𝑅m 𝑉 ) ) → 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) )
6 simpr ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ 𝐴 ∈ ( 𝑅m 𝑉 ) ) → 𝐴 ∈ ( 𝑅m 𝑉 ) )
7 4 5 6 3jca ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ 𝐴 ∈ ( 𝑅m 𝑉 ) ) → ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ∧ 𝐴 ∈ ( 𝑅m 𝑉 ) ) )
8 7 3adant3 ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ 𝐴 ∈ ( 𝑅m 𝑉 ) ∧ ( 𝐴 supp ( 0g𝑆 ) ) ∈ Fin ) → ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ∧ 𝐴 ∈ ( 𝑅m 𝑉 ) ) )
9 1 2 scmsuppss ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ∧ 𝐴 ∈ ( 𝑅m 𝑉 ) ) → ( ( 𝑣𝑉 ↦ ( ( 𝐴𝑣 ) ( ·𝑠𝑀 ) 𝑣 ) ) supp ( 0g𝑀 ) ) ⊆ ( 𝐴 supp ( 0g𝑆 ) ) )
10 8 9 syl ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ 𝐴 ∈ ( 𝑅m 𝑉 ) ∧ ( 𝐴 supp ( 0g𝑆 ) ) ∈ Fin ) → ( ( 𝑣𝑉 ↦ ( ( 𝐴𝑣 ) ( ·𝑠𝑀 ) 𝑣 ) ) supp ( 0g𝑀 ) ) ⊆ ( 𝐴 supp ( 0g𝑆 ) ) )
11 ssfi ( ( ( 𝐴 supp ( 0g𝑆 ) ) ∈ Fin ∧ ( ( 𝑣𝑉 ↦ ( ( 𝐴𝑣 ) ( ·𝑠𝑀 ) 𝑣 ) ) supp ( 0g𝑀 ) ) ⊆ ( 𝐴 supp ( 0g𝑆 ) ) ) → ( ( 𝑣𝑉 ↦ ( ( 𝐴𝑣 ) ( ·𝑠𝑀 ) 𝑣 ) ) supp ( 0g𝑀 ) ) ∈ Fin )
12 3 10 11 syl2anc ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ 𝐴 ∈ ( 𝑅m 𝑉 ) ∧ ( 𝐴 supp ( 0g𝑆 ) ) ∈ Fin ) → ( ( 𝑣𝑉 ↦ ( ( 𝐴𝑣 ) ( ·𝑠𝑀 ) 𝑣 ) ) supp ( 0g𝑀 ) ) ∈ Fin )