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	$$⊢\mathrm{span}\left(\varnothing \right)=0_{\mathscr{H}}$$

Proof

Step	Hyp	Ref	Expression
1		h0elsh	$$⊢0_{\mathscr{H}}\in {\mathbf{S}}_{\mathscr{H}}$$
2	1	shssii	$$⊢0_{\mathscr{H}}\subseteq \mathscr{H}$$
3		0ss	$$⊢\varnothing \subseteq 0_{\mathscr{H}}$$
4		spanss	$$⊢\left(0_{\mathscr{H}}\subseteq \mathscr{H}\wedge \varnothing \subseteq 0_{\mathscr{H}}\right)\to \mathrm{span}\left(\varnothing \right)\subseteq \mathrm{span}\left(0_{\mathscr{H}}\right)$$
5	2 3 4	mp2an	$$⊢\mathrm{span}\left(\varnothing \right)\subseteq \mathrm{span}\left(0_{\mathscr{H}}\right)$$
6		spanid	$$⊢0_{\mathscr{H}}\in {\mathbf{S}}_{\mathscr{H}}\to \mathrm{span}\left(0_{\mathscr{H}}\right)=0_{\mathscr{H}}$$
7	1 6	ax-mp	$$⊢\mathrm{span}\left(0_{\mathscr{H}}\right)=0_{\mathscr{H}}$$
8	5 7	sseqtri	$$⊢\mathrm{span}\left(\varnothing \right)\subseteq 0_{\mathscr{H}}$$
9		0ss	$$⊢\varnothing \subseteq \mathscr{H}$$
10		spancl	$$⊢\varnothing \subseteq \mathscr{H}\to \mathrm{span}\left(\varnothing \right)\in {\mathbf{S}}_{\mathscr{H}}$$
11	9 10	ax-mp	$$⊢\mathrm{span}\left(\varnothing \right)\in {\mathbf{S}}_{\mathscr{H}}$$
12		sh0le	$$⊢\mathrm{span}\left(\varnothing \right)\in {\mathbf{S}}_{\mathscr{H}}\to 0_{\mathscr{H}}\subseteq \mathrm{span}\left(\varnothing \right)$$
13	11 12	ax-mp	$$⊢0_{\mathscr{H}}\subseteq \mathrm{span}\left(\varnothing \right)$$
14	8 13	eqssi	$$⊢\mathrm{span}\left(\varnothing \right)=0_{\mathscr{H}}$$