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ℋ

Proof

Step	Hyp	Ref	Expression
1		df-ch0	⊢ 0ℋ = { 0ℎ }
2	1	fveq2i	⊢ ( span ‘ 0ℋ ) = ( span ‘ { 0ℎ } )
3		h0elsh	⊢ 0ℋ ∈ Sℋ
4		spanid	⊢ ( 0ℋ ∈ Sℋ → ( span ‘ 0ℋ ) = 0ℋ )
5	3 4	ax-mp	⊢ ( span ‘ 0ℋ ) = 0ℋ
6	2 5	eqtr3i	⊢ ( span ‘ { 0ℎ } ) = 0ℋ