lspsnne2

Description: Two ways to express that vectors have different spans. (Contributed by NM, 20-May-2015)

Step	Hyp	Ref	Expression
1		lspsnne2.v	$⊢ V = {Base}_{W}$
2		lspsnne2.n	$⊢ N = LSpan (W)$
3		lspsnne2.w	$⊢ φ \to W \in LMod$
4		lspsnne2.x	$⊢ φ \to X \in V$
5		lspsnne2.y	$⊢ φ \to Y \in V$
6		lspsnne2.e	$⊢ φ \to \neg X \in N (\{Y\})$
7		eqimss	$⊢ N (\{X\}) = N (\{Y\}) \to N (\{X\}) \subseteq N (\{Y\})$
8		eqid	$⊢ LSubSp (W) = LSubSp (W)$
9	1 8 2	lspsncl	$⊢ (W \in LMod \land Y \in V) \to N (\{Y\}) \in LSubSp (W)$
10	3 5 9	syl2anc	$⊢ φ \to N (\{Y\}) \in LSubSp (W)$
11	1 8 2 3 10 4	ellspsn5b	$⊢ φ \to (X \in N (\{Y\}) \leftrightarrow N (\{X\}) \subseteq N (\{Y\}))$
12	7 11	imbitrrid	$⊢ φ \to (N (\{X\}) = N (\{Y\}) \to X \in N (\{Y\}))$
13	12	necon3bd	$⊢ φ \to (\neg X \in N (\{Y\}) \to N (\{X\}) \neq N (\{Y\}))$
14	6 13	mpd	$⊢ φ \to N (\{X\}) \neq N (\{Y\})$

Metamath Proof Explorer