lspsnsubn0

Description: Unequal singleton spans imply nonzero vector subtraction. (Contributed by NM, 19-Mar-2015)

Step	Hyp	Ref	Expression
1		lspsnsubn0.v	$⊢ V = {Base}_{W}$
2		lspsnsubn0.o	$⊢ \underset{˙}{0} = 0_{W}$
3		lspsnsubn0.m	$⊢ \underset{˙}{-} = -_{W}$
4		lspsnsubn0.w	$⊢ φ \to W \in LMod$
5		lspsnsubn0.x	$⊢ φ \to X \in V$
6		lspsnsubn0.y	$⊢ φ \to Y \in V$
7		lspsnsubn0.e	$⊢ φ \to N (\{X\}) \neq N (\{Y\})$
8	1 2 3	lmodsubeq0	$⊢ (W \in LMod \land X \in V \land Y \in V) \to (X \underset{˙}{-} Y = \underset{˙}{0} \leftrightarrow X = Y)$
9	4 5 6 8	syl3anc	$⊢ φ \to (X \underset{˙}{-} Y = \underset{˙}{0} \leftrightarrow X = Y)$
10		sneq	$⊢ X = Y \to \{X\} = \{Y\}$
11	10	fveq2d	$⊢ X = Y \to N (\{X\}) = N (\{Y\})$
12	9 11	biimtrdi	$⊢ φ \to (X \underset{˙}{-} Y = \underset{˙}{0} \to N (\{X\}) = N (\{Y\}))$
13	12	necon3d	$⊢ φ \to (N (\{X\}) \neq N (\{Y\}) \to X \underset{˙}{-} Y \neq \underset{˙}{0})$
14	7 13	mpd	$⊢ φ \to X \underset{˙}{-} Y \neq \underset{˙}{0}$

Metamath Proof Explorer