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

Metamath Proof Explorer

Theorem lmodsubid

Description: Subtraction of a vector from itself. ( hvsubid analog.) (Contributed by NM, 16-Apr-2014) (Revised by Mario Carneiro, 19-Jun-2014)

	Ref	Expression
Hypotheses	lmodsubeq0.v	$⊢ V = {Base}_{W}$
	lmodsubeq0.o	$⊢ \underset{˙}{0} = 0_{W}$
	lmodsubeq0.m	$⊢ \underset{˙}{-} = -_{W}$
Assertion	lmodsubid	$⊢ (W \in LMod \land A \in V) \to A \underset{˙}{-} A = \underset{˙}{0}$

Step	Hyp	Ref	Expression
1		lmodsubeq0.v	$⊢ V = {Base}_{W}$
2		lmodsubeq0.o	$⊢ \underset{˙}{0} = 0_{W}$
3		lmodsubeq0.m	$⊢ \underset{˙}{-} = -_{W}$
4		lmodgrp	$⊢ W \in LMod \to W \in Grp$
5	1 2 3	grpsubid	$⊢ (W \in Grp \land A \in V) \to A \underset{˙}{-} A = \underset{˙}{0}$
6	4 5	sylan	$⊢ (W \in LMod \land A \in V) \to A \underset{˙}{-} A = \underset{˙}{0}$