Theorem pjoc2

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

	Ref	Expression
Assertion	pjoc2	$$⊢\left(H\in {\mathbf{C}}_{\mathscr{H}}\wedge A\in \mathscr{H}\right)\to \left(A\in \perp \left(H\right)\leftrightarrow {\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)=0_{ℎ}\right)$$

Proof

Step	Hyp	Ref	Expression
1		fveq2	$$⊢H=if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,0_{\mathscr{H}}\right)\to \perp \left(H\right)=\perp \left(if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,0_{\mathscr{H}}\right)\right)$$
2	1	eleq2d	$$⊢H=if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,0_{\mathscr{H}}\right)\to \left(A\in \perp \left(H\right)\leftrightarrow A\in \perp \left(if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,0_{\mathscr{H}}\right)\right)\right)$$
3		fveq2	$$⊢H=if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,0_{\mathscr{H}}\right)\to {\mathrm{proj}}_{ℎ}\left(H\right)={\mathrm{proj}}_{ℎ}\left(if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,0_{\mathscr{H}}\right)\right)$$
4	3	fveq1d	$$⊢H=if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,0_{\mathscr{H}}\right)\to {\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)={\mathrm{proj}}_{ℎ}\left(if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,0_{\mathscr{H}}\right)\right)\left(A\right)$$
5	4	eqeq1d	$$⊢H=if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,0_{\mathscr{H}}\right)\to \left({\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)=0_{ℎ}\leftrightarrow {\mathrm{proj}}_{ℎ}\left(if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,0_{\mathscr{H}}\right)\right)\left(A\right)=0_{ℎ}\right)$$
6	2 5	bibi12d	$$⊢H=if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,0_{\mathscr{H}}\right)\to \left(\left(A\in \perp \left(H\right)\leftrightarrow {\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)=0_{ℎ}\right)\leftrightarrow \left(A\in \perp \left(if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,0_{\mathscr{H}}\right)\right)\leftrightarrow {\mathrm{proj}}_{ℎ}\left(if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,0_{\mathscr{H}}\right)\right)\left(A\right)=0_{ℎ}\right)\right)$$
7		eleq1	$$⊢A=if\left(A\in \mathscr{H},A,0_{ℎ}\right)\to \left(A\in \perp \left(if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,0_{\mathscr{H}}\right)\right)\leftrightarrow if\left(A\in \mathscr{H},A,0_{ℎ}\right)\in \perp \left(if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,0_{\mathscr{H}}\right)\right)\right)$$
8		fveqeq2	$$⊢A=if\left(A\in \mathscr{H},A,0_{ℎ}\right)\to \left({\mathrm{proj}}_{ℎ}\left(if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,0_{\mathscr{H}}\right)\right)\left(A\right)=0_{ℎ}\leftrightarrow {\mathrm{proj}}_{ℎ}\left(if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,0_{\mathscr{H}}\right)\right)\left(if\left(A\in \mathscr{H},A,0_{ℎ}\right)\right)=0_{ℎ}\right)$$
9	7 8	bibi12d	$$⊢A=if\left(A\in \mathscr{H},A,0_{ℎ}\right)\to \left(\left(A\in \perp \left(if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,0_{\mathscr{H}}\right)\right)\leftrightarrow {\mathrm{proj}}_{ℎ}\left(if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,0_{\mathscr{H}}\right)\right)\left(A\right)=0_{ℎ}\right)\leftrightarrow \left(if\left(A\in \mathscr{H},A,0_{ℎ}\right)\in \perp \left(if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,0_{\mathscr{H}}\right)\right)\leftrightarrow {\mathrm{proj}}_{ℎ}\left(if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,0_{\mathscr{H}}\right)\right)\left(if\left(A\in \mathscr{H},A,0_{ℎ}\right)\right)=0_{ℎ}\right)\right)$$
10		h0elch	$$⊢0_{\mathscr{H}}\in {\mathbf{C}}_{\mathscr{H}}$$
11	10	elimel	$$⊢if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,0_{\mathscr{H}}\right)\in {\mathbf{C}}_{\mathscr{H}}$$
12		ifhvhv0	$$⊢if\left(A\in \mathscr{H},A,0_{ℎ}\right)\in \mathscr{H}$$
13	11 12	pjoc2i	$$⊢if\left(A\in \mathscr{H},A,0_{ℎ}\right)\in \perp \left(if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,0_{\mathscr{H}}\right)\right)\leftrightarrow {\mathrm{proj}}_{ℎ}\left(if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,0_{\mathscr{H}}\right)\right)\left(if\left(A\in \mathscr{H},A,0_{ℎ}\right)\right)=0_{ℎ}$$
14	6 9 13	dedth2h	$$⊢\left(H\in {\mathbf{C}}_{\mathscr{H}}\wedge A\in \mathscr{H}\right)\to \left(A\in \perp \left(H\right)\leftrightarrow {\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)=0_{ℎ}\right)$$