lsator0sp

Description: The span of a vector is either an atom or the zero subspace. (Contributed by NM, 15-Mar-2015)

Step	Hyp	Ref	Expression
1		lsator0sp.v	$⊢ V = {Base}_{W}$
2		lsator0sp.n	$⊢ N = LSpan (W)$
3		lsator0sp.o	$⊢ \underset{˙}{0} = 0_{W}$
4		lsator0sp.a	$⊢ A = LSAtoms (W)$
5		isator0sp.w	$⊢ φ \to W \in LMod$
6		isator0sp.x	$⊢ φ \to X \in V$
7	1 2 3 4 5 6	lsatspn0	$⊢ φ \to (N (\{X\}) \in A \leftrightarrow X \neq \underset{˙}{0})$
8	7	biimprd	$⊢ φ \to (X \neq \underset{˙}{0} \to N (\{X\}) \in A)$
9	8	necon1bd	$⊢ φ \to (\neg N (\{X\}) \in A \to X = \underset{˙}{0})$
10	1 3 2	lspsneq0	$⊢ (W \in LMod \land X \in V) \to (N (\{X\}) = \{\underset{˙}{0}\} \leftrightarrow X = \underset{˙}{0})$
11	5 6 10	syl2anc	$⊢ φ \to (N (\{X\}) = \{\underset{˙}{0}\} \leftrightarrow X = \underset{˙}{0})$
12	9 11	sylibrd	$⊢ φ \to (\neg N (\{X\}) \in A \to N (\{X\}) = \{\underset{˙}{0}\})$
13	12	orrd	$⊢ φ \to (N (\{X\}) \in A \lor N (\{X\}) = \{\underset{˙}{0}\})$

Metamath Proof Explorer