Theorem pjo

Description: The orthogonal projection. Lemma 4.4(i) of Beran p. 111. (Contributed by NM, 30-Oct-1999) (New usage is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		pjch1	$$⊢A\in \mathscr{H}\to {\mathrm{proj}}_{ℎ}\left(\mathscr{H}\right)\left(A\right)=A$$
2	1	adantl	$$⊢\left(H\in {\mathbf{C}}_{\mathscr{H}}\wedge A\in \mathscr{H}\right)\to {\mathrm{proj}}_{ℎ}\left(\mathscr{H}\right)\left(A\right)=A$$
3		axpjpj	$$⊢\left(H\in {\mathbf{C}}_{\mathscr{H}}\wedge A\in \mathscr{H}\right)\to A={\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(\perp \left(H\right)\right)\left(A\right)$$
4	2 3	eqtr2d	$$⊢\left(H\in {\mathbf{C}}_{\mathscr{H}}\wedge A\in \mathscr{H}\right)\to {\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(\perp \left(H\right)\right)\left(A\right)={\mathrm{proj}}_{ℎ}\left(\mathscr{H}\right)\left(A\right)$$
5		helch	$$⊢\mathscr{H}\in {\mathbf{C}}_{\mathscr{H}}$$
6	5	pjcli	$$⊢A\in \mathscr{H}\to {\mathrm{proj}}_{ℎ}\left(\mathscr{H}\right)\left(A\right)\in \mathscr{H}$$
7	6	adantl	$$⊢\left(H\in {\mathbf{C}}_{\mathscr{H}}\wedge A\in \mathscr{H}\right)\to {\mathrm{proj}}_{ℎ}\left(\mathscr{H}\right)\left(A\right)\in \mathscr{H}$$
8		pjhcl	$$⊢\left(H\in {\mathbf{C}}_{\mathscr{H}}\wedge A\in \mathscr{H}\right)\to {\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)\in \mathscr{H}$$
9		choccl	$$⊢H\in {\mathbf{C}}_{\mathscr{H}}\to \perp \left(H\right)\in {\mathbf{C}}_{\mathscr{H}}$$
10		pjhcl	$$⊢\left(\perp \left(H\right)\in {\mathbf{C}}_{\mathscr{H}}\wedge A\in \mathscr{H}\right)\to {\mathrm{proj}}_{ℎ}\left(\perp \left(H\right)\right)\left(A\right)\in \mathscr{H}$$
11	9 10	sylan	$$⊢\left(H\in {\mathbf{C}}_{\mathscr{H}}\wedge A\in \mathscr{H}\right)\to {\mathrm{proj}}_{ℎ}\left(\perp \left(H\right)\right)\left(A\right)\in \mathscr{H}$$
12		hvsubadd	$$⊢\left({\mathrm{proj}}_{ℎ}\left(\mathscr{H}\right)\left(A\right)\in \mathscr{H}\wedge {\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)\in \mathscr{H}\wedge {\mathrm{proj}}_{ℎ}\left(\perp \left(H\right)\right)\left(A\right)\in \mathscr{H}\right)\to \left({\mathrm{proj}}_{ℎ}\left(\mathscr{H}\right)\left(A\right){-}_{ℎ}{\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)={\mathrm{proj}}_{ℎ}\left(\perp \left(H\right)\right)\left(A\right)\leftrightarrow {\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(\perp \left(H\right)\right)\left(A\right)={\mathrm{proj}}_{ℎ}\left(\mathscr{H}\right)\left(A\right)\right)$$
13	7 8 11 12	syl3anc	$$⊢\left(H\in {\mathbf{C}}_{\mathscr{H}}\wedge A\in \mathscr{H}\right)\to \left({\mathrm{proj}}_{ℎ}\left(\mathscr{H}\right)\left(A\right){-}_{ℎ}{\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)={\mathrm{proj}}_{ℎ}\left(\perp \left(H\right)\right)\left(A\right)\leftrightarrow {\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(\perp \left(H\right)\right)\left(A\right)={\mathrm{proj}}_{ℎ}\left(\mathscr{H}\right)\left(A\right)\right)$$
14	4 13	mpbird	$$⊢\left(H\in {\mathbf{C}}_{\mathscr{H}}\wedge A\in \mathscr{H}\right)\to {\mathrm{proj}}_{ℎ}\left(\mathscr{H}\right)\left(A\right){-}_{ℎ}{\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)={\mathrm{proj}}_{ℎ}\left(\perp \left(H\right)\right)\left(A\right)$$
15	14	eqcomd	$$⊢\left(H\in {\mathbf{C}}_{\mathscr{H}}\wedge A\in \mathscr{H}\right)\to {\mathrm{proj}}_{ℎ}\left(\perp \left(H\right)\right)\left(A\right)={\mathrm{proj}}_{ℎ}\left(\mathscr{H}\right)\left(A\right){-}_{ℎ}{\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)$$