Metamath Proof Explorer


Theorem slmd0vlid

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