Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Thierry Arnoux
Algebra
Semiring left modules
slmd0vlid
Metamath Proof Explorer
Description: Left identity law for the zero vector. ( hvaddid2 analog.)
(Contributed by NM , 10-Jan-2014) (Revised by Mario Carneiro , 19-Jun-2014) (Revised by Thierry Arnoux , 1-Apr-2018)
Ref
Expression
Hypotheses
slmd0vlid.v
⊢ V = Base W
slmd0vlid.a
⊢ + ˙ = + W
slmd0vlid.z
⊢ 0 ˙ = 0 W
Assertion
slmd0vlid
⊢ W ∈ SLMod ∧ X ∈ V → 0 ˙ + ˙ X = X
Proof
Step
Hyp
Ref
Expression
1
slmd0vlid.v
⊢ V = Base W
2
slmd0vlid.a
⊢ + ˙ = + W
3
slmd0vlid.z
⊢ 0 ˙ = 0 W
4
slmdmnd
⊢ W ∈ SLMod → W ∈ Mnd
5
1 2 3
mndlid
⊢ W ∈ Mnd ∧ X ∈ V → 0 ˙ + ˙ X = X
6
4 5
sylan
⊢ W ∈ SLMod ∧ X ∈ V → 0 ˙ + ˙ X = X