This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem slmdmcl

Description: Closure of ring multiplication for a semimodule. (Contributed by NM, 14-Jan-2014) (Revised by Mario Carneiro, 19-Jun-2014) (Revised by Thierry Arnoux, 1-Apr-2018)

Ref Expression
Hypotheses slmdmcl.f ⊢ 𝐹 = ( Scalar ‘ 𝑊 )
slmdmcl.k ⊢ 𝐾 = ( Base ‘ 𝐹 )
slmdmcl.t ⊢ · = ( .r ‘ 𝐹 )
Assertion slmdmcl ( ( 𝑊 ∈ SLMod ∧ 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐾 ) → ( 𝑋 · 𝑌 ) ∈ 𝐾 )

Proof

Step Hyp Ref Expression
1 slmdmcl.f ⊢ 𝐹 = ( Scalar ‘ 𝑊 )
2 slmdmcl.k ⊢ 𝐾 = ( Base ‘ 𝐹 )
3 slmdmcl.t ⊢ · = ( .r ‘ 𝐹 )
4 1 slmdsrg ⊢ ( 𝑊 ∈ SLMod → 𝐹 ∈ SRing )
5 2 3 srgcl ⊢ ( ( 𝐹 ∈ SRing ∧ 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐾 ) → ( 𝑋 · 𝑌 ) ∈ 𝐾 )
6 4 5 syl3an1 ⊢ ( ( 𝑊 ∈ SLMod ∧ 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐾 ) → ( 𝑋 · 𝑌 ) ∈ 𝐾 )