Theorem ocval

Description: Value of orthogonal complement of a subset of Hilbert space. (Contributed by NM, 7-Aug-2000) (Revised by Mario Carneiro, 23-Dec-2013) (New usage is discouraged.)

	Ref	Expression
Assertion	ocval	$$⊢H\subseteq \mathscr{H}\to \perp \left(H\right)=\left\{x\in \mathscr{H}|\forall y\in Hx{\cdot }_{\mathrm{ih}}y=0\right\}$$

Proof

Step	Hyp	Ref	Expression
1		ax-hilex	$$⊢\mathscr{H}\in \mathrm{V}$$
2	1	elpw2	$$⊢H\in 𝒫\mathscr{H}\leftrightarrow H\subseteq \mathscr{H}$$
3		raleq	$$⊢z=H\to \left(\forall y\in zx{\cdot }_{\mathrm{ih}}y=0\leftrightarrow \forall y\in Hx{\cdot }_{\mathrm{ih}}y=0\right)$$
4	3	rabbidv	$$⊢z=H\to \left\{x\in \mathscr{H}|\forall y\in zx{\cdot }_{\mathrm{ih}}y=0\right\}=\left\{x\in \mathscr{H}|\forall y\in Hx{\cdot }_{\mathrm{ih}}y=0\right\}$$
5		df-oc	$$⊢\perp =\left(z\in 𝒫\mathscr{H}⟼\left\{x\in \mathscr{H}|\forall y\in zx{\cdot }_{\mathrm{ih}}y=0\right\}\right)$$
6	1	rabex	$$⊢\left\{x\in \mathscr{H}|\forall y\in Hx{\cdot }_{\mathrm{ih}}y=0\right\}\in \mathrm{V}$$
7	4 5 6	fvmpt	$$⊢H\in 𝒫\mathscr{H}\to \perp \left(H\right)=\left\{x\in \mathscr{H}|\forall y\in Hx{\cdot }_{\mathrm{ih}}y=0\right\}$$
8	2 7	sylbir	$$⊢H\subseteq \mathscr{H}\to \perp \left(H\right)=\left\{x\in \mathscr{H}|\forall y\in Hx{\cdot }_{\mathrm{ih}}y=0\right\}$$