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=BaseW
slmd0vlid.a +˙=+W
slmd0vlid.z 0˙=0W
Assertion slmd0vrid WSLModXVX+˙0˙=X

Proof

Step Hyp Ref Expression
1 slmd0vlid.v V=BaseW
2 slmd0vlid.a +˙=+W
3 slmd0vlid.z 0˙=0W
4 slmdmnd WSLModWMnd
5 1 2 3 mndrid WMndXVX+˙0˙=X
6 4 5 sylan WSLModXVX+˙0˙=X