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

Proof

Step	Hyp	Ref	Expression
1		df-ch0	$$⊢0_{\mathscr{H}}=\left\{0_{ℎ}\right\}$$
2	1	fveq2i	$$⊢\mathrm{span}\left(0_{\mathscr{H}}\right)=\mathrm{span}\left(\left\{0_{ℎ}\right\}\right)$$
3		h0elsh	$$⊢0_{\mathscr{H}}\in {\mathbf{S}}_{\mathscr{H}}$$
4		spanid	$$⊢0_{\mathscr{H}}\in {\mathbf{S}}_{\mathscr{H}}\to \mathrm{span}\left(0_{\mathscr{H}}\right)=0_{\mathscr{H}}$$
5	3 4	ax-mp	$$⊢\mathrm{span}\left(0_{\mathscr{H}}\right)=0_{\mathscr{H}}$$
6	2 5	eqtr3i	$$⊢\mathrm{span}\left(\left\{0_{ℎ}\right\}\right)=0_{\mathscr{H}}$$