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

Metamath Proof Explorer

Theorem lspsn0

Description: Span of the singleton of the zero vector. ( spansn0 analog.) (Contributed by NM, 15-Jan-2014) (Proof shortened by Mario Carneiro, 19-Jun-2014)

	Ref	Expression
Hypotheses	lspsn0.z	$⊢ \underset{˙}{0} = 0_{W}$
	lspsn0.n	$⊢ N = LSpan (W)$
Assertion	lspsn0	$⊢ W \in LMod \to N (\{\underset{˙}{0}\}) = \{\underset{˙}{0}\}$

Proof

Step	Hyp	Ref	Expression
1		lspsn0.z	$⊢ \underset{˙}{0} = 0_{W}$
2		lspsn0.n	$⊢ N = LSpan (W)$
3		eqid	$⊢ LSubSp (W) = LSubSp (W)$
4	1 3	lsssn0	$⊢ W \in LMod \to \{\underset{˙}{0}\} \in LSubSp (W)$
5	3 2	lspid	$⊢ (W \in LMod \land \{\underset{˙}{0}\} \in LSubSp (W)) \to N (\{\underset{˙}{0}\}) = \{\underset{˙}{0}\}$
6	4 5	mpdan	$⊢ W \in LMod \to N (\{\underset{˙}{0}\}) = \{\underset{˙}{0}\}$