Theorem ocel

Description: Membership in orthogonal complement of H subset. (Contributed by NM, 7-Aug-2000) (New usage is discouraged.)

	Ref	Expression
Assertion	ocel	$$⊢H\subseteq \mathscr{H}\to \left(A\in \perp \left(H\right)\leftrightarrow \left(A\in \mathscr{H}\wedge \forall x\in HA{\cdot }_{\mathrm{ih}}x=0\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		ocval	$$⊢H\subseteq \mathscr{H}\to \perp \left(H\right)=\left\{y\in \mathscr{H}|\forall x\in Hy{\cdot }_{\mathrm{ih}}x=0\right\}$$
2	1	eleq2d	$$⊢H\subseteq \mathscr{H}\to \left(A\in \perp \left(H\right)\leftrightarrow A\in \left\{y\in \mathscr{H}|\forall x\in Hy{\cdot }_{\mathrm{ih}}x=0\right\}\right)$$
3		oveq1	$$⊢y=A\to y{\cdot }_{\mathrm{ih}}x=A{\cdot }_{\mathrm{ih}}x$$
4	3	eqeq1d	$$⊢y=A\to \left(y{\cdot }_{\mathrm{ih}}x=0\leftrightarrow A{\cdot }_{\mathrm{ih}}x=0\right)$$
5	4	ralbidv	$$⊢y=A\to \left(\forall x\in Hy{\cdot }_{\mathrm{ih}}x=0\leftrightarrow \forall x\in HA{\cdot }_{\mathrm{ih}}x=0\right)$$
6	5	elrab	$$⊢A\in \left\{y\in \mathscr{H}|\forall x\in Hy{\cdot }_{\mathrm{ih}}x=0\right\}\leftrightarrow \left(A\in \mathscr{H}\wedge \forall x\in HA{\cdot }_{\mathrm{ih}}x=0\right)$$
7	2 6	bitrdi	$$⊢H\subseteq \mathscr{H}\to \left(A\in \perp \left(H\right)\leftrightarrow \left(A\in \mathscr{H}\wedge \forall x\in HA{\cdot }_{\mathrm{ih}}x=0\right)\right)$$