Theorem pjch

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

	Ref	Expression
Assertion	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)$$

Proof

Step	Hyp	Ref	Expression
1		eleq2	$$⊢H=if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,\mathscr{H}\right)\to \left(A\in H\leftrightarrow A\in if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,\mathscr{H}\right)\right)$$
2		fveq2	$$⊢H=if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,\mathscr{H}\right)\to {\mathrm{proj}}_{ℎ}\left(H\right)={\mathrm{proj}}_{ℎ}\left(if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,\mathscr{H}\right)\right)$$
3	2	fveq1d	$$⊢H=if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,\mathscr{H}\right)\to {\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)={\mathrm{proj}}_{ℎ}\left(if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,\mathscr{H}\right)\right)\left(A\right)$$
4	3	eqeq1d	$$⊢H=if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,\mathscr{H}\right)\to \left({\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)=A\leftrightarrow {\mathrm{proj}}_{ℎ}\left(if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,\mathscr{H}\right)\right)\left(A\right)=A\right)$$
5	1 4	bibi12d	$$⊢H=if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,\mathscr{H}\right)\to \left(\left(A\in H\leftrightarrow {\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)=A\right)\leftrightarrow \left(A\in if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,\mathscr{H}\right)\leftrightarrow {\mathrm{proj}}_{ℎ}\left(if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,\mathscr{H}\right)\right)\left(A\right)=A\right)\right)$$
6		eleq1	$$⊢A=if\left(A\in \mathscr{H},A,0_{ℎ}\right)\to \left(A\in if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,\mathscr{H}\right)\leftrightarrow if\left(A\in \mathscr{H},A,0_{ℎ}\right)\in if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,\mathscr{H}\right)\right)$$
7		fveq2	$$⊢A=if\left(A\in \mathscr{H},A,0_{ℎ}\right)\to {\mathrm{proj}}_{ℎ}\left(if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,\mathscr{H}\right)\right)\left(A\right)={\mathrm{proj}}_{ℎ}\left(if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,\mathscr{H}\right)\right)\left(if\left(A\in \mathscr{H},A,0_{ℎ}\right)\right)$$
8		id	$$⊢A=if\left(A\in \mathscr{H},A,0_{ℎ}\right)\to A=if\left(A\in \mathscr{H},A,0_{ℎ}\right)$$
9	7 8	eqeq12d	$$⊢A=if\left(A\in \mathscr{H},A,0_{ℎ}\right)\to \left({\mathrm{proj}}_{ℎ}\left(if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,\mathscr{H}\right)\right)\left(A\right)=A\leftrightarrow {\mathrm{proj}}_{ℎ}\left(if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,\mathscr{H}\right)\right)\left(if\left(A\in \mathscr{H},A,0_{ℎ}\right)\right)=if\left(A\in \mathscr{H},A,0_{ℎ}\right)\right)$$
10	6 9	bibi12d	$$⊢A=if\left(A\in \mathscr{H},A,0_{ℎ}\right)\to \left(\left(A\in if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,\mathscr{H}\right)\leftrightarrow {\mathrm{proj}}_{ℎ}\left(if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,\mathscr{H}\right)\right)\left(A\right)=A\right)\leftrightarrow \left(if\left(A\in \mathscr{H},A,0_{ℎ}\right)\in if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,\mathscr{H}\right)\leftrightarrow {\mathrm{proj}}_{ℎ}\left(if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,\mathscr{H}\right)\right)\left(if\left(A\in \mathscr{H},A,0_{ℎ}\right)\right)=if\left(A\in \mathscr{H},A,0_{ℎ}\right)\right)\right)$$
11		ifchhv	$$⊢if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,\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	pjchi	$$⊢if\left(A\in \mathscr{H},A,0_{ℎ}\right)\in if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,\mathscr{H}\right)\leftrightarrow {\mathrm{proj}}_{ℎ}\left(if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,\mathscr{H}\right)\right)\left(if\left(A\in \mathscr{H},A,0_{ℎ}\right)\right)=if\left(A\in \mathscr{H},A,0_{ℎ}\right)$$
14	5 10 13	dedth2h	$$⊢\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)$$