Theorem obsocv

Description: An orthonormal basis has trivial orthocomplement. (Contributed by Mario Carneiro, 23-Oct-2015)

	Ref	Expression
Hypotheses	obsocv.z	$$⊢\underset{\dot{}}{0}=0_W$$
	obsocv.o	$$⊢\underset{\dot{}}{\perp }=\mathrm{ocv}\left(W\right)$$
Assertion	obsocv	$$⊢B\in \mathrm{OBasis}\left(W\right)\to \underset{\dot{}}{\perp }\left(B\right)=\left\{\underset{\dot{}}{0}\right\}$$

Proof

Step	Hyp	Ref	Expression
1		obsocv.z	$$⊢\underset{\dot{}}{0}=0_W$$
2		obsocv.o	$$⊢\underset{\dot{}}{\perp }=\mathrm{ocv}\left(W\right)$$
3		eqid	$$⊢{\mathrm{Base}}_W={\mathrm{Base}}_W$$
4		eqid	$$⊢{\cdot }_{𝑖}\left(W\right)={\cdot }_{𝑖}\left(W\right)$$
5		eqid	$$⊢\mathrm{Scalar}\left(W\right)=\mathrm{Scalar}\left(W\right)$$
6		eqid	$$⊢1_{\mathrm{Scalar}\left(W\right)}=1_{\mathrm{Scalar}\left(W\right)}$$
7		eqid	$$⊢0_{\mathrm{Scalar}\left(W\right)}=0_{\mathrm{Scalar}\left(W\right)}$$
8	3 4 5 6 7 2 1	isobs	$$⊢B\in \mathrm{OBasis}\left(W\right)\leftrightarrow \left(W\in \mathrm{PreHil}\wedge B\subseteq {\mathrm{Base}}_W\wedge \left(\forall x\in B\forall y\in Bx{\cdot }_{𝑖}\left(W\right)y=if\left(x=y,1_{\mathrm{Scalar}\left(W\right)},0_{\mathrm{Scalar}\left(W\right)}\right)\wedge \underset{\dot{}}{\perp }\left(B\right)=\left\{\underset{\dot{}}{0}\right\}\right)\right)$$
9	8	simp3bi	$$⊢B\in \mathrm{OBasis}\left(W\right)\to \left(\forall x\in B\forall y\in Bx{\cdot }_{𝑖}\left(W\right)y=if\left(x=y,1_{\mathrm{Scalar}\left(W\right)},0_{\mathrm{Scalar}\left(W\right)}\right)\wedge \underset{\dot{}}{\perp }\left(B\right)=\left\{\underset{\dot{}}{0}\right\}\right)$$
10	9	simprd	$$⊢B\in \mathrm{OBasis}\left(W\right)\to \underset{\dot{}}{\perp }\left(B\right)=\left\{\underset{\dot{}}{0}\right\}$$