Metamath Proof Explorer

Theorem rmsuppfi

Description: The support of a mapping of a multiplication of a constant with a function into a ring is finite if the support of the function is finite. (Contributed by AV, 11-Apr-2019)

Ref Expression
Hypothesis rmsuppfi.r ⊢ R = Base M
Assertion rmsuppfi ⊢ M ∈ Ring ∧ V ∈ X ∧ C ∈ R ∧ A ∈ R V ∧ A supp 0 M ∈ Fin → v ∈ V ⟼ C ⋅ M A ⁡ v supp 0 M ∈ Fin

Proof

Step Hyp Ref Expression
1 rmsuppfi.r ⊢ R = Base M
2 simp3 ⊢ M ∈ Ring ∧ V ∈ X ∧ C ∈ R ∧ A ∈ R V ∧ A supp 0 M ∈ Fin → A supp 0 M ∈ Fin
3 1 rmsuppss ⊢ M ∈ Ring ∧ V ∈ X ∧ C ∈ R ∧ A ∈ R V → v ∈ V ⟼ C ⋅ M A ⁡ v supp 0 M ⊆ A supp 0 M
4 3 3adant3 ⊢ M ∈ Ring ∧ V ∈ X ∧ C ∈ R ∧ A ∈ R V ∧ A supp 0 M ∈ Fin → v ∈ V ⟼ C ⋅ M A ⁡ v supp 0 M ⊆ A supp 0 M
5 ssfi ⊢ A supp 0 M ∈ Fin ∧ v ∈ V ⟼ C ⋅ M A ⁡ v supp 0 M ⊆ A supp 0 M → v ∈ V ⟼ C ⋅ M A ⁡ v supp 0 M ∈ Fin
6 2 4 5 syl2anc ⊢ M ∈ Ring ∧ V ∈ X ∧ C ∈ R ∧ A ∈ R V ∧ A supp 0 M ∈ Fin → v ∈ V ⟼ C ⋅ M A ⁡ v supp 0 M ∈ Fin