Theorem obs2ocv

Description: The double orthocomplement (closure) of an orthonormal basis is the whole space. (Contributed by Mario Carneiro, 23-Oct-2015)

	Ref	Expression
Hypotheses	obs2ocv.o	$$⊢\underset{\dot{}}{\perp }=\mathrm{ocv}\left(W\right)$$
	obs2ocv.v	$$⊢V={\mathrm{Base}}_W$$
Assertion	obs2ocv	$$⊢B\in \mathrm{OBasis}\left(W\right)\to \underset{\dot{}}{\perp }\left(\underset{\dot{}}{\perp }\left(B\right)\right)=V$$

Proof

Step	Hyp	Ref	Expression
1		obs2ocv.o	$$⊢\underset{\dot{}}{\perp }=\mathrm{ocv}\left(W\right)$$
2		obs2ocv.v	$$⊢V={\mathrm{Base}}_W$$
3		eqid	$$⊢0_W=0_W$$
4	3 1	obsocv	$$⊢B\in \mathrm{OBasis}\left(W\right)\to \underset{\dot{}}{\perp }\left(B\right)=\left\{0_W\right\}$$
5	4	fveq2d	$$⊢B\in \mathrm{OBasis}\left(W\right)\to \underset{\dot{}}{\perp }\left(\underset{\dot{}}{\perp }\left(B\right)\right)=\underset{\dot{}}{\perp }\left(\left\{0_W\right\}\right)$$
6		obsrcl	$$⊢B\in \mathrm{OBasis}\left(W\right)\to W\in \mathrm{PreHil}$$
7	2 1 3	ocvz	$$⊢W\in \mathrm{PreHil}\to \underset{\dot{}}{\perp }\left(\left\{0_W\right\}\right)=V$$
8	6 7	syl	$$⊢B\in \mathrm{OBasis}\left(W\right)\to \underset{\dot{}}{\perp }\left(\left\{0_W\right\}\right)=V$$
9	5 8	eqtrd	$$⊢B\in \mathrm{OBasis}\left(W\right)\to \underset{\dot{}}{\perp }\left(\underset{\dot{}}{\perp }\left(B\right)\right)=V$$