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 ‘ 𝑀 ) )