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

Metamath Proof Explorer

Theorem lspsneq0

Description: Span of the singleton is the zero subspace iff the vector is zero. (Contributed by NM, 27-Apr-2014) (Revised by Mario Carneiro, 19-Jun-2014)

		Ref	Expression
	Hypotheses	lspsneq0.v	$⊢ V = {Base}_{W}$
		lspsneq0.z	$⊢ \underset{˙}{0} = 0_{W}$
		lspsneq0.n	$⊢ N = LSpan (W)$
	Assertion	lspsneq0	$⊢ (W \in LMod \land X \in V) \to (N (\{X\}) = \{\underset{˙}{0}\} \leftrightarrow X = \underset{˙}{0})$

Proof

Step	Hyp	Ref	Expression
1		lspsneq0.v	$⊢ V = {Base}_{W}$
2		lspsneq0.z	$⊢ \underset{˙}{0} = 0_{W}$
3		lspsneq0.n	$⊢ N = LSpan (W)$
4	1 3	lspsnid	$⊢ (W \in LMod \land X \in V) \to X \in N (\{X\})$
5		eleq2	$⊢ N (\{X\}) = \{\underset{˙}{0}\} \to (X \in N (\{X\}) \leftrightarrow X \in \{\underset{˙}{0}\})$
6	4 5	syl5ibcom	$⊢ (W \in LMod \land X \in V) \to (N (\{X\}) = \{\underset{˙}{0}\} \to X \in \{\underset{˙}{0}\})$
7		elsni	$⊢ X \in \{\underset{˙}{0}\} \to X = \underset{˙}{0}$
8	6 7	syl6	$⊢ (W \in LMod \land X \in V) \to (N (\{X\}) = \{\underset{˙}{0}\} \to X = \underset{˙}{0})$
9	2 3	lspsn0	$⊢ W \in LMod \to N (\{\underset{˙}{0}\}) = \{\underset{˙}{0}\}$
10	9	adantr	$⊢ (W \in LMod \land X \in V) \to N (\{\underset{˙}{0}\}) = \{\underset{˙}{0}\}$
11		sneq	$⊢ X = \underset{˙}{0} \to \{X\} = \{\underset{˙}{0}\}$
12	11	fveqeq2d	$⊢ X = \underset{˙}{0} \to (N (\{X\}) = \{\underset{˙}{0}\} \leftrightarrow N (\{\underset{˙}{0}\}) = \{\underset{˙}{0}\})$
13	10 12	syl5ibrcom	$⊢ (W \in LMod \land X \in V) \to (X = \underset{˙}{0} \to N (\{X\}) = \{\underset{˙}{0}\})$
14	8 13	impbid	$⊢ (W \in LMod \land X \in V) \to (N (\{X\}) = \{\underset{˙}{0}\} \leftrightarrow X = \underset{˙}{0})$