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

Metamath Proof Explorer

Theorem spansn0

Description: The span of the singleton of the zero vector is the zero subspace. (Contributed by NM, 14-Jan-2005) (New usage is discouraged.)

		Ref	Expression
	Assertion	spansn0	$⊢ span (\{0_{ℎ}\}) = 0_{ℋ}$

Step	Hyp	Ref	Expression
1		df-ch0	$⊢ 0_{ℋ} = \{0_{ℎ}\}$
2	1	fveq2i	$⊢ span (0_{ℋ}) = span (\{0_{ℎ}\})$
3		h0elsh	$⊢ 0_{ℋ} \in S_{ℋ}$
4		spanid	$⊢ 0_{ℋ} \in S_{ℋ} \to span (0_{ℋ}) = 0_{ℋ}$
5	3 4	ax-mp	$⊢ span (0_{ℋ}) = 0_{ℋ}$
6	2 5	eqtr3i	$⊢ span (\{0_{ℎ}\}) = 0_{ℋ}$