Metamath Proof Explorer

Theorem slmdvscl

Description: Closure of scalar product for a semiring left module. ( hvmulcl analog.) (Contributed by NM, 8-Dec-2013) (Revised by Mario Carneiro, 19-Jun-2014) (Revised by Thierry Arnoux, 1-Apr-2018)

Ref Expression
Hypotheses slmdvscl.v ⊢ V = Base W
slmdvscl.f ⊢ F = Scalar ⁡ W
slmdvscl.s ⊢ · ˙ = ⋅ W
slmdvscl.k ⊢ K = Base F
Assertion slmdvscl ⊢ W ∈ SLMod ∧ R ∈ K ∧ X ∈ V → R · ˙ X ∈ V

Proof

Step Hyp Ref Expression
1 slmdvscl.v ⊢ V = Base W
2 slmdvscl.f ⊢ F = Scalar ⁡ W
3 slmdvscl.s ⊢ · ˙ = ⋅ W
4 slmdvscl.k ⊢ K = Base F
5 biid ⊢ W ∈ SLMod ↔ W ∈ SLMod
6 pm4.24 ⊢ R ∈ K ↔ R ∈ K ∧ R ∈ K
7 pm4.24 ⊢ X ∈ V ↔ X ∈ V ∧ X ∈ V
8 eqid ⊢ + W = + W
9 eqid ⊢ 0 W = 0 W
10 eqid ⊢ + F = + F
11 eqid ⊢ ⋅ F = ⋅ F
12 eqid ⊢ 1 F = 1 F
13 eqid ⊢ 0 F = 0 F
14 1 8 3 9 2 4 10 11 12 13 slmdlema ⊢ W ∈ SLMod ∧ R ∈ K ∧ R ∈ K ∧ X ∈ V ∧ X ∈ V → R · ˙ X ∈ V ∧ R · ˙ X + W X = R · ˙ X + W R · ˙ X ∧ R + F R · ˙ X = R · ˙ X + W R · ˙ X ∧ R ⋅ F R · ˙ X = R · ˙ R · ˙ X ∧ 1 F · ˙ X = X ∧ 0 F · ˙ X = 0 W
15 14 simpld ⊢ W ∈ SLMod ∧ R ∈ K ∧ R ∈ K ∧ X ∈ V ∧ X ∈ V → R · ˙ X ∈ V ∧ R · ˙ X + W X = R · ˙ X + W R · ˙ X ∧ R + F R · ˙ X = R · ˙ X + W R · ˙ X
16 15 simp1d ⊢ W ∈ SLMod ∧ R ∈ K ∧ R ∈ K ∧ X ∈ V ∧ X ∈ V → R · ˙ X ∈ V
17 5 6 7 16 syl3anb ⊢ W ∈ SLMod ∧ R ∈ K ∧ X ∈ V → R · ˙ X ∈ V