Theorem pjid

Description: The projection of a vector in the projection subspace is itself. (Contributed by NM, 9-Apr-2006) (New usage is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		simpl	$$⊢\left(H\in {\mathbf{C}}_{\mathscr{H}}\wedge A\in H\right)\to H\in {\mathbf{C}}_{\mathscr{H}}$$
2		chel	$$⊢\left(H\in {\mathbf{C}}_{\mathscr{H}}\wedge A\in H\right)\to A\in \mathscr{H}$$
3	1 2	jca	$$⊢\left(H\in {\mathbf{C}}_{\mathscr{H}}\wedge A\in H\right)\to \left(H\in {\mathbf{C}}_{\mathscr{H}}\wedge A\in \mathscr{H}\right)$$
4		pjch	$$⊢\left(H\in {\mathbf{C}}_{\mathscr{H}}\wedge A\in \mathscr{H}\right)\to \left(A\in H\leftrightarrow {\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)=A\right)$$
5	4	biimpa	$$⊢\left(\left(H\in {\mathbf{C}}_{\mathscr{H}}\wedge A\in \mathscr{H}\right)\wedge A\in H\right)\to {\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)=A$$
6	3 5	sylancom	$$⊢\left(H\in {\mathbf{C}}_{\mathscr{H}}\wedge A\in H\right)\to {\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)=A$$