Metamath Proof Explorer

Theorem rmfsupp

Description: A mapping of a multiplication of a constant with a function into a ring is finitely supported if the function is finitely supported. (Contributed by AV, 9-Jun-2019)

Ref Expression
Hypothesis rmsuppfi.r ⊢ 𝑅 = ( Base ‘ 𝑀 )
Assertion rmfsupp ( ( ( 𝑀 ∈ Ring ∧ 𝑉 ∈ 𝑋 ∧ 𝐶 ∈ 𝑅 ) ∧ 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝐴 finSupp ( 0g ‘ 𝑀 ) ) → ( 𝑣 ∈ 𝑉 ↦ ( 𝐶 ( .r ‘ 𝑀 ) ( 𝐴 ‘ 𝑣 ) ) ) finSupp ( 0g ‘ 𝑀 ) )

Proof

Step Hyp Ref Expression
1 rmsuppfi.r ⊢ 𝑅 = ( Base ‘ 𝑀 )
2 funmpt ⊢ Fun ( 𝑣 ∈ 𝑉 ↦ ( 𝐶 ( .r ‘ 𝑀 ) ( 𝐴 ‘ 𝑣 ) ) )
3 2 a1i ⊢ ( ( ( 𝑀 ∈ Ring ∧ 𝑉 ∈ 𝑋 ∧ 𝐶 ∈ 𝑅 ) ∧ 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝐴 finSupp ( 0g ‘ 𝑀 ) ) → Fun ( 𝑣 ∈ 𝑉 ↦ ( 𝐶 ( .r ‘ 𝑀 ) ( 𝐴 ‘ 𝑣 ) ) ) )
4 id ⊢ ( 𝐴 finSupp ( 0g ‘ 𝑀 ) → 𝐴 finSupp ( 0g ‘ 𝑀 ) )
5 4 fsuppimpd ⊢ ( 𝐴 finSupp ( 0g ‘ 𝑀 ) → ( 𝐴 supp ( 0g ‘ 𝑀 ) ) ∈ Fin )
6 1 rmsuppfi ⊢ ( ( ( 𝑀 ∈ Ring ∧ 𝑉 ∈ 𝑋 ∧ 𝐶 ∈ 𝑅 ) ∧ 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ∧ ( 𝐴 supp ( 0g ‘ 𝑀 ) ) ∈ Fin ) → ( ( 𝑣 ∈ 𝑉 ↦ ( 𝐶 ( .r ‘ 𝑀 ) ( 𝐴 ‘ 𝑣 ) ) ) supp ( 0g ‘ 𝑀 ) ) ∈ Fin )
7 5 6 syl3an3 ⊢ ( ( ( 𝑀 ∈ Ring ∧ 𝑉 ∈ 𝑋 ∧ 𝐶 ∈ 𝑅 ) ∧ 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝐴 finSupp ( 0g ‘ 𝑀 ) ) → ( ( 𝑣 ∈ 𝑉 ↦ ( 𝐶 ( .r ‘ 𝑀 ) ( 𝐴 ‘ 𝑣 ) ) ) supp ( 0g ‘ 𝑀 ) ) ∈ Fin )
8 mptexg ⊢ ( 𝑉 ∈ 𝑋 → ( 𝑣 ∈ 𝑉 ↦ ( 𝐶 ( .r ‘ 𝑀 ) ( 𝐴 ‘ 𝑣 ) ) ) ∈ V )
9 8 3ad2ant2 ⊢ ( ( 𝑀 ∈ Ring ∧ 𝑉 ∈ 𝑋 ∧ 𝐶 ∈ 𝑅 ) → ( 𝑣 ∈ 𝑉 ↦ ( 𝐶 ( .r ‘ 𝑀 ) ( 𝐴 ‘ 𝑣 ) ) ) ∈ V )
10 9 3ad2ant1 ⊢ ( ( ( 𝑀 ∈ Ring ∧ 𝑉 ∈ 𝑋 ∧ 𝐶 ∈ 𝑅 ) ∧ 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝐴 finSupp ( 0g ‘ 𝑀 ) ) → ( 𝑣 ∈ 𝑉 ↦ ( 𝐶 ( .r ‘ 𝑀 ) ( 𝐴 ‘ 𝑣 ) ) ) ∈ V )
11 fvex ⊢ ( 0g ‘ 𝑀 ) ∈ V
12 isfsupp ⊢ ( ( ( 𝑣 ∈ 𝑉 ↦ ( 𝐶 ( .r ‘ 𝑀 ) ( 𝐴 ‘ 𝑣 ) ) ) ∈ V ∧ ( 0g ‘ 𝑀 ) ∈ V ) → ( ( 𝑣 ∈ 𝑉 ↦ ( 𝐶 ( .r ‘ 𝑀 ) ( 𝐴 ‘ 𝑣 ) ) ) finSupp ( 0g ‘ 𝑀 ) ↔ ( Fun ( 𝑣 ∈ 𝑉 ↦ ( 𝐶 ( .r ‘ 𝑀 ) ( 𝐴 ‘ 𝑣 ) ) ) ∧ ( ( 𝑣 ∈ 𝑉 ↦ ( 𝐶 ( .r ‘ 𝑀 ) ( 𝐴 ‘ 𝑣 ) ) ) supp ( 0g ‘ 𝑀 ) ) ∈ Fin ) ) )
13 10 11 12 sylancl ⊢ ( ( ( 𝑀 ∈ Ring ∧ 𝑉 ∈ 𝑋 ∧ 𝐶 ∈ 𝑅 ) ∧ 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝐴 finSupp ( 0g ‘ 𝑀 ) ) → ( ( 𝑣 ∈ 𝑉 ↦ ( 𝐶 ( .r ‘ 𝑀 ) ( 𝐴 ‘ 𝑣 ) ) ) finSupp ( 0g ‘ 𝑀 ) ↔ ( Fun ( 𝑣 ∈ 𝑉 ↦ ( 𝐶 ( .r ‘ 𝑀 ) ( 𝐴 ‘ 𝑣 ) ) ) ∧ ( ( 𝑣 ∈ 𝑉 ↦ ( 𝐶 ( .r ‘ 𝑀 ) ( 𝐴 ‘ 𝑣 ) ) ) supp ( 0g ‘ 𝑀 ) ) ∈ Fin ) ) )
14 3 7 13 mpbir2and ⊢ ( ( ( 𝑀 ∈ Ring ∧ 𝑉 ∈ 𝑋 ∧ 𝐶 ∈ 𝑅 ) ∧ 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝐴 finSupp ( 0g ‘ 𝑀 ) ) → ( 𝑣 ∈ 𝑉 ↦ ( 𝐶 ( .r ‘ 𝑀 ) ( 𝐴 ‘ 𝑣 ) ) ) finSupp ( 0g ‘ 𝑀 ) )