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

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	$⊢ \underset{˙}{+} = +_{W}$
	slmd0vlid.z	$⊢ \underset{˙}{0} = 0_{W}$
Assertion	slmd0vrid	$⊢ (W \in SLMod \land X \in V) \to X \underset{˙}{+} \underset{˙}{0} = X$

Proof

Step	Hyp	Ref	Expression
1		slmd0vlid.v	$⊢ V = {Base}_{W}$
2		slmd0vlid.a	$⊢ \underset{˙}{+} = +_{W}$
3		slmd0vlid.z	$⊢ \underset{˙}{0} = 0_{W}$
4		slmdmnd	$⊢ W \in SLMod \to W \in Mnd$
5	1 2 3	mndrid	$⊢ (W \in Mnd \land X \in V) \to X \underset{˙}{+} \underset{˙}{0} = X$
6	4 5	sylan	$⊢ (W \in SLMod \land X \in V) \to X \underset{˙}{+} \underset{˙}{0} = X$