lspsnne1

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

Step	Hyp	Ref	Expression
1		lspsnne1.v	$⊢ V = {Base}_{W}$
2		lspsnne1.o	$⊢ \underset{˙}{0} = 0_{W}$
3		lspsnne1.n	$⊢ N = LSpan (W)$
4		lspsnne1.w	$⊢ φ \to W \in LVec$
5		lspsnne1.x	$⊢ φ \to X \in (V ∖ \{\underset{˙}{0}\})$
6		lspsnne1.y	$⊢ φ \to Y \in V$
7		lspsnne1.e	$⊢ φ \to N (\{X\}) \neq N (\{Y\})$
8		eqid	$⊢ LSubSp (W) = LSubSp (W)$
9		lveclmod	$⊢ W \in LVec \to W \in LMod$
10	4 9	syl	$⊢ φ \to W \in LMod$
11	1 8 3	lspsncl	$⊢ (W \in LMod \land Y \in V) \to N (\{Y\}) \in LSubSp (W)$
12	10 6 11	syl2anc	$⊢ φ \to N (\{Y\}) \in LSubSp (W)$
13	5	eldifad	$⊢ φ \to X \in V$
14	1 8 3 10 12 13	ellspsn5b	$⊢ φ \to (X \in N (\{Y\}) \leftrightarrow N (\{X\}) \subseteq N (\{Y\}))$
15	14	notbid	$⊢ φ \to (\neg X \in N (\{Y\}) \leftrightarrow \neg N (\{X\}) \subseteq N (\{Y\}))$
16	1 2 3 4 5 6	lspsncmp	$⊢ φ \to (N (\{X\}) \subseteq N (\{Y\}) \leftrightarrow N (\{X\}) = N (\{Y\}))$
17	16	necon3bbid	$⊢ φ \to (\neg N (\{X\}) \subseteq N (\{Y\}) \leftrightarrow N (\{X\}) \neq N (\{Y\}))$
18	15 17	bitrd	$⊢ φ \to (\neg X \in N (\{Y\}) \leftrightarrow N (\{X\}) \neq N (\{Y\}))$
19	7 18	mpbird	$⊢ φ \to \neg X \in N (\{Y\})$

Metamath Proof Explorer