Theorem pjoc2i

Description: Projection of a vector in the orthocomplement of the projection subspace. Lemma 4.4(iii) of Beran p. 111. (Contributed by NM, 27-Oct-1999) (New usage is discouraged.)

	Ref	Expression
Hypotheses	pjoc2.1	$$⊢H\in {\mathbf{C}}_{\mathscr{H}}$$
	pjoc2.2	$$⊢A\in \mathscr{H}$$
Assertion	pjoc2i	$$⊢A\in \perp \left(H\right)\leftrightarrow {\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)=0_{ℎ}$$

Proof

Step	Hyp	Ref	Expression
1		pjoc2.1	$$⊢H\in {\mathbf{C}}_{\mathscr{H}}$$
2		pjoc2.2	$$⊢A\in \mathscr{H}$$
3	1	choccli	$$⊢\perp \left(H\right)\in {\mathbf{C}}_{\mathscr{H}}$$
4	3 2	pjoc1i	$$⊢A\in \perp \left(H\right)\leftrightarrow {\mathrm{proj}}_{ℎ}\left(\perp \left(\perp \left(H\right)\right)\right)\left(A\right)=0_{ℎ}$$
5	1	pjococi	$$⊢\perp \left(\perp \left(H\right)\right)=H$$
6	5	fveq2i	$$⊢{\mathrm{proj}}_{ℎ}\left(\perp \left(\perp \left(H\right)\right)\right)={\mathrm{proj}}_{ℎ}\left(H\right)$$
7	6	fveq1i	$$⊢{\mathrm{proj}}_{ℎ}\left(\perp \left(\perp \left(H\right)\right)\right)\left(A\right)={\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)$$
8	7	eqeq1i	$$⊢{\mathrm{proj}}_{ℎ}\left(\perp \left(\perp \left(H\right)\right)\right)\left(A\right)=0_{ℎ}\leftrightarrow {\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)=0_{ℎ}$$
9	4 8	bitri	$$⊢A\in \perp \left(H\right)\leftrightarrow {\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)=0_{ℎ}$$