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

Metamath Proof Explorer

Theorem lmodsubeq0

Description: If the difference between two vectors is zero, they are equal. ( hvsubeq0 analog.) (Contributed by NM, 31-Mar-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	lmodsubeq0	$⊢ (W \in LMod \land A \in V \land B \in V) \to (A \underset{˙}{-} B = \underset{˙}{0} \leftrightarrow A = B)$

Proof

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	grpsubeq0	$⊢ (W \in Grp \land A \in V \land B \in V) \to (A \underset{˙}{-} B = \underset{˙}{0} \leftrightarrow A = B)$
6	4 5	syl3an1	$⊢ (W \in LMod \land A \in V \land B \in V) \to (A \underset{˙}{-} B = \underset{˙}{0} \leftrightarrow A = B)$