Theorem shocel

Description: Membership in orthogonal complement of H subspace. (Contributed by NM, 9-Oct-1999) (New usage is discouraged.)

	Ref	Expression
Assertion	shocel	$$⊢H\in {\mathbf{S}}_{\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		shss	$$⊢H\in {\mathbf{S}}_{\mathscr{H}}\to H\subseteq \mathscr{H}$$
2		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)$$
3	1 2	syl	$$⊢H\in {\mathbf{S}}_{\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)$$