Theorem pjoc1i

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

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

Proof

Step	Hyp	Ref	Expression
1		pjop.1	$$⊢H\in {\mathbf{C}}_{\mathscr{H}}$$
2		pjop.2	$$⊢A\in \mathscr{H}$$
3	1 2	pjopi	$$⊢{\mathrm{proj}}_{ℎ}\left(\perp \left(H\right)\right)\left(A\right)=A{-}_{ℎ}{\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)$$
4	1	chshii	$$⊢H\in {\mathbf{S}}_{\mathscr{H}}$$
5	1 2	pjclii	$$⊢{\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)\in H$$
6		shsubcl	$$⊢\left(H\in {\mathbf{S}}_{\mathscr{H}}\wedge A\in H\wedge {\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)\in H\right)\to A{-}_{ℎ}{\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)\in H$$
7	4 5 6	mp3an13	$$⊢A\in H\to A{-}_{ℎ}{\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)\in H$$
8	3 7	eqeltrid	$$⊢A\in H\to {\mathrm{proj}}_{ℎ}\left(\perp \left(H\right)\right)\left(A\right)\in H$$
9	1	choccli	$$⊢\perp \left(H\right)\in {\mathbf{C}}_{\mathscr{H}}$$
10	9 2	pjclii	$$⊢{\mathrm{proj}}_{ℎ}\left(\perp \left(H\right)\right)\left(A\right)\in \perp \left(H\right)$$
11	8 10	jctir	$$⊢A\in H\to \left({\mathrm{proj}}_{ℎ}\left(\perp \left(H\right)\right)\left(A\right)\in H\wedge {\mathrm{proj}}_{ℎ}\left(\perp \left(H\right)\right)\left(A\right)\in \perp \left(H\right)\right)$$
12		elin	$$⊢{\mathrm{proj}}_{ℎ}\left(\perp \left(H\right)\right)\left(A\right)\in \left(H\cap \perp \left(H\right)\right)\leftrightarrow \left({\mathrm{proj}}_{ℎ}\left(\perp \left(H\right)\right)\left(A\right)\in H\wedge {\mathrm{proj}}_{ℎ}\left(\perp \left(H\right)\right)\left(A\right)\in \perp \left(H\right)\right)$$
13	11 12	sylibr	$$⊢A\in H\to {\mathrm{proj}}_{ℎ}\left(\perp \left(H\right)\right)\left(A\right)\in \left(H\cap \perp \left(H\right)\right)$$
14		ocin	$$⊢H\in {\mathbf{S}}_{\mathscr{H}}\to H\cap \perp \left(H\right)=0_{\mathscr{H}}$$
15	4 14	ax-mp	$$⊢H\cap \perp \left(H\right)=0_{\mathscr{H}}$$
16	13 15	eleqtrdi	$$⊢A\in H\to {\mathrm{proj}}_{ℎ}\left(\perp \left(H\right)\right)\left(A\right)\in 0_{\mathscr{H}}$$
17		elch0	$$⊢{\mathrm{proj}}_{ℎ}\left(\perp \left(H\right)\right)\left(A\right)\in 0_{\mathscr{H}}\leftrightarrow {\mathrm{proj}}_{ℎ}\left(\perp \left(H\right)\right)\left(A\right)=0_{ℎ}$$
18	16 17	sylib	$$⊢A\in H\to {\mathrm{proj}}_{ℎ}\left(\perp \left(H\right)\right)\left(A\right)=0_{ℎ}$$
19	1 2	pjpji	$$⊢A={\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(\perp \left(H\right)\right)\left(A\right)$$
20		oveq2	$$⊢{\mathrm{proj}}_{ℎ}\left(\perp \left(H\right)\right)\left(A\right)=0_{ℎ}\to {\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(\perp \left(H\right)\right)\left(A\right)={\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right){+}_{ℎ}{0}_{ℎ}$$
21	19 20	syl5eq	$$⊢{\mathrm{proj}}_{ℎ}\left(\perp \left(H\right)\right)\left(A\right)=0_{ℎ}\to A={\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right){+}_{ℎ}{0}_{ℎ}$$
22	1 2	pjhclii	$$⊢{\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)\in \mathscr{H}$$
23		ax-hvaddid	$$⊢{\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)\in \mathscr{H}\to {\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right){+}_{ℎ}{0}_{ℎ}={\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)$$
24	22 23	ax-mp	$$⊢{\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right){+}_{ℎ}{0}_{ℎ}={\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)$$
25	21 24	eqtrdi	$$⊢{\mathrm{proj}}_{ℎ}\left(\perp \left(H\right)\right)\left(A\right)=0_{ℎ}\to A={\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)$$
26	25 5	eqeltrdi	$$⊢{\mathrm{proj}}_{ℎ}\left(\perp \left(H\right)\right)\left(A\right)=0_{ℎ}\to A\in H$$
27	18 26	impbii	$$⊢A\in H\leftrightarrow {\mathrm{proj}}_{ℎ}\left(\perp \left(H\right)\right)\left(A\right)=0_{ℎ}$$