Theorem h1deoi

Description: Membership in orthocomplement of 1-dimensional subspace. (Contributed by NM, 7-Jul-2001) (New usage is discouraged.)

	Ref	Expression
Hypothesis	h1deot.1	$$⊢B\in \mathscr{H}$$
Assertion	h1deoi	$$⊢A\in \perp \left(\left\{B\right\}\right)\leftrightarrow \left(A\in \mathscr{H}\wedge A{\cdot }_{\mathrm{ih}}B=0\right)$$

Proof

Step	Hyp	Ref	Expression
1		h1deot.1	$$⊢B\in \mathscr{H}$$
2		snssi	$$⊢B\in \mathscr{H}\to \left\{B\right\}\subseteq \mathscr{H}$$
3		ocel	$$⊢\left\{B\right\}\subseteq \mathscr{H}\to \left(A\in \perp \left(\left\{B\right\}\right)\leftrightarrow \left(A\in \mathscr{H}\wedge \forall x\in \left\{B\right\}A{\cdot }_{\mathrm{ih}}x=0\right)\right)$$
4	1 2 3	mp2b	$$⊢A\in \perp \left(\left\{B\right\}\right)\leftrightarrow \left(A\in \mathscr{H}\wedge \forall x\in \left\{B\right\}A{\cdot }_{\mathrm{ih}}x=0\right)$$
5	1	elexi	$$⊢B\in \mathrm{V}$$
6		oveq2	$$⊢x=B\to A{\cdot }_{\mathrm{ih}}x=A{\cdot }_{\mathrm{ih}}B$$
7	6	eqeq1d	$$⊢x=B\to \left(A{\cdot }_{\mathrm{ih}}x=0\leftrightarrow A{\cdot }_{\mathrm{ih}}B=0\right)$$
8	5 7	ralsn	$$⊢\forall x\in \left\{B\right\}A{\cdot }_{\mathrm{ih}}x=0\leftrightarrow A{\cdot }_{\mathrm{ih}}B=0$$
9	8	anbi2i	$$⊢\left(A\in \mathscr{H}\wedge \forall x\in \left\{B\right\}A{\cdot }_{\mathrm{ih}}x=0\right)\leftrightarrow \left(A\in \mathscr{H}\wedge A{\cdot }_{\mathrm{ih}}B=0\right)$$
10	4 9	bitri	$$⊢A\in \perp \left(\left\{B\right\}\right)\leftrightarrow \left(A\in \mathscr{H}\wedge A{\cdot }_{\mathrm{ih}}B=0\right)$$