Metamath Proof Explorer


Theorem slmd0vrid

Description: Right identity law for the zero vector. ( ax-hvaddid 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 slmd0vrid W SLMod X V X + ˙ 0 ˙ = 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 mndrid W Mnd X V X + ˙ 0 ˙ = X
6 4 5 sylan W SLMod X V X + ˙ 0 ˙ = X