This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem lmod0vrid

Description: Right identity law for the zero vector. ( ax-hvaddid analog.) (Contributed by NM, 10-Jan-2014) (Revised by Mario Carneiro, 19-Jun-2014)

	Ref	Expression
Hypotheses	0vlid.v	$⊢ V = {Base}_{W}$
	0vlid.a	$⊢ \underset{˙}{+} = +_{W}$
	0vlid.z	$⊢ \underset{˙}{0} = 0_{W}$
Assertion	lmod0vrid	$⊢ (W \in LMod \land X \in V) \to X \underset{˙}{+} \underset{˙}{0} = X$

Proof

Step	Hyp	Ref	Expression
1		0vlid.v	$⊢ V = {Base}_{W}$
2		0vlid.a	$⊢ \underset{˙}{+} = +_{W}$
3		0vlid.z	$⊢ \underset{˙}{0} = 0_{W}$
4		lmodgrp	$⊢ W \in LMod \to W \in Grp$
5	1 2 3	grprid	$⊢ (W \in Grp \land X \in V) \to X \underset{˙}{+} \underset{˙}{0} = X$
6	4 5	sylan	$⊢ (W \in LMod \land X \in V) \to X \underset{˙}{+} \underset{˙}{0} = X$