Theorem span0

Description: The span of the empty set is the zero subspace. Remark 11.6.e of Schechter p. 276. (Contributed by NM, 3-Jun-2004) (New usage is discouraged.)

	Ref	Expression
Assertion	span0	⊢ ( span ‘ ∅ ) = 0ℋ

Proof

Step	Hyp	Ref	Expression
1		h0elsh	⊢ 0ℋ ∈ Sℋ
2	1	shssii	⊢ 0ℋ ⊆ ℋ
3		0ss	⊢ ∅ ⊆ 0ℋ
4		spanss	⊢ ( ( 0ℋ ⊆ ℋ ∧ ∅ ⊆ 0ℋ ) → ( span ‘ ∅ ) ⊆ ( span ‘ 0ℋ ) )
5	2 3 4	mp2an	⊢ ( span ‘ ∅ ) ⊆ ( span ‘ 0ℋ )
6		spanid	⊢ ( 0ℋ ∈ Sℋ → ( span ‘ 0ℋ ) = 0ℋ )
7	1 6	ax-mp	⊢ ( span ‘ 0ℋ ) = 0ℋ
8	5 7	sseqtri	⊢ ( span ‘ ∅ ) ⊆ 0ℋ
9		0ss	⊢ ∅ ⊆ ℋ
10		spancl	⊢ ( ∅ ⊆ ℋ → ( span ‘ ∅ ) ∈ Sℋ )
11	9 10	ax-mp	⊢ ( span ‘ ∅ ) ∈ Sℋ
12		sh0le	⊢ ( ( span ‘ ∅ ) ∈ Sℋ → 0ℋ ⊆ ( span ‘ ∅ ) )
13	11 12	ax-mp	⊢ 0ℋ ⊆ ( span ‘ ∅ )
14	8 13	eqssi	⊢ ( span ‘ ∅ ) = 0ℋ