Theorem pjchi

Description: Projection of a vector in the projection subspace. Lemma 4.4(ii) of Beran p. 111. (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	pjchi	$$⊢A\in H\leftrightarrow {\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)=A$$

Proof

Step	Hyp	Ref	Expression
1		pjop.1	$$⊢H\in {\mathbf{C}}_{\mathscr{H}}$$
2		pjop.2	$$⊢A\in \mathscr{H}$$
3	1 2	pjhclii	$$⊢{\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)\in \mathscr{H}$$
4		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)$$
5	3 4	ax-mp	$$⊢{\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right){+}_{ℎ}{0}_{ℎ}={\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)$$
6	1 2	pjpji	$$⊢A={\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(\perp \left(H\right)\right)\left(A\right)$$
7	1 2	pjoc1i	$$⊢A\in H\leftrightarrow {\mathrm{proj}}_{ℎ}\left(\perp \left(H\right)\right)\left(A\right)=0_{ℎ}$$
8	7	biimpi	$$⊢A\in H\to {\mathrm{proj}}_{ℎ}\left(\perp \left(H\right)\right)\left(A\right)=0_{ℎ}$$
9	8	oveq2d	$$⊢A\in H\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}_{ℎ}$$
10	6 9	syl5req	$$⊢A\in H\to {\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right){+}_{ℎ}{0}_{ℎ}=A$$
11	5 10	syl5eqr	$$⊢A\in H\to {\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)=A$$
12	1 2	pjclii	$$⊢{\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)\in H$$
13		eleq1	$$⊢{\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)=A\to \left({\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)\in H\leftrightarrow A\in H\right)$$
14	12 13	mpbii	$$⊢{\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)=A\to A\in H$$
15	11 14	impbii	$$⊢A\in H\leftrightarrow {\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)=A$$