Theorem css0

Description: The zero subspace is a closed subspace. (Contributed by Mario Carneiro, 13-Oct-2015)

	Ref	Expression
Hypotheses	css0.c	$$⊢C=\mathrm{ClSubSp}\left(W\right)$$
	css0.z	$$⊢\underset{\dot{}}{0}=0_W$$
Assertion	css0	$$⊢W\in \mathrm{PreHil}\to \left\{\underset{\dot{}}{0}\right\}\in C$$

Proof

Step	Hyp	Ref	Expression
1		css0.c	$$⊢C=\mathrm{ClSubSp}\left(W\right)$$
2		css0.z	$$⊢\underset{\dot{}}{0}=0_W$$
3		eqid	$$⊢{\mathrm{Base}}_W={\mathrm{Base}}_W$$
4		eqid	$$⊢\mathrm{ocv}\left(W\right)=\mathrm{ocv}\left(W\right)$$
5	3 4 2	ocv1	$$⊢W\in \mathrm{PreHil}\to \mathrm{ocv}\left(W\right)\left({\mathrm{Base}}_W\right)=\left\{\underset{\dot{}}{0}\right\}$$
6		ssid	$$⊢{\mathrm{Base}}_W\subseteq {\mathrm{Base}}_W$$
7	3 1 4	ocvcss	$$⊢\left(W\in \mathrm{PreHil}\wedge {\mathrm{Base}}_W\subseteq {\mathrm{Base}}_W\right)\to \mathrm{ocv}\left(W\right)\left({\mathrm{Base}}_W\right)\in C$$
8	6 7	mpan2	$$⊢W\in \mathrm{PreHil}\to \mathrm{ocv}\left(W\right)\left({\mathrm{Base}}_W\right)\in C$$
9	5 8	eqeltrrd	$$⊢W\in \mathrm{PreHil}\to \left\{\underset{\dot{}}{0}\right\}\in C$$