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