Metamath Proof Explorer


Theorem lmod0vid

Description: Identity equivalent to the value of the zero vector. Provides a convenient way to compute the value. (Contributed by NM, 9-Mar-2014) (Revised by Mario Carneiro, 19-Jun-2014)

Ref Expression
Hypotheses 0vlid.v V = Base W
0vlid.a + ˙ = + W
0vlid.z 0 ˙ = 0 W
Assertion lmod0vid W LMod X V X + ˙ X = X 0 ˙ = X

Proof

Step Hyp Ref Expression
1 0vlid.v V = Base W
2 0vlid.a + ˙ = + W
3 0vlid.z 0 ˙ = 0 W
4 lmodgrp W LMod W Grp
5 1 2 3 grpid W Grp X V X + ˙ X = X 0 ˙ = X
6 4 5 sylan W LMod X V X + ˙ X = X 0 ˙ = X