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ℋ

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ℋ