Theorem pjtoi

Description: Subspace sum of projection and projection of orthocomplement. (Contributed by NM, 16-Nov-2000) (New usage is discouraged.)

	Ref	Expression
Hypothesis	pjidmco.1	$$⊢H\in {\mathbf{C}}_{\mathscr{H}}$$
Assertion	pjtoi	$$⊢{\mathrm{proj}}_{ℎ}\left(H\right){+}_{\mathrm{op}}{\mathrm{proj}}_{ℎ}\left(\perp \left(H\right)\right)={\mathrm{proj}}_{ℎ}\left(\mathscr{H}\right)$$

Proof

Step	Hyp	Ref	Expression
1		pjidmco.1	$$⊢H\in {\mathbf{C}}_{\mathscr{H}}$$
2		axpjpj	$$⊢\left(H\in {\mathbf{C}}_{\mathscr{H}}\wedge x\in \mathscr{H}\right)\to x={\mathrm{proj}}_{ℎ}\left(H\right)\left(x\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(\perp \left(H\right)\right)\left(x\right)$$
3	1 2	mpan	$$⊢x\in \mathscr{H}\to x={\mathrm{proj}}_{ℎ}\left(H\right)\left(x\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(\perp \left(H\right)\right)\left(x\right)$$
4		pjch1	$$⊢x\in \mathscr{H}\to {\mathrm{proj}}_{ℎ}\left(\mathscr{H}\right)\left(x\right)=x$$
5	1	pjfi	$$⊢{\mathrm{proj}}_{ℎ}\left(H\right):\mathscr{H}⟶\mathscr{H}$$
6	1	choccli	$$⊢\perp \left(H\right)\in {\mathbf{C}}_{\mathscr{H}}$$
7	6	pjfi	$$⊢{\mathrm{proj}}_{ℎ}\left(\perp \left(H\right)\right):\mathscr{H}⟶\mathscr{H}$$
8		hosval	$$⊢\left({\mathrm{proj}}_{ℎ}\left(H\right):\mathscr{H}⟶\mathscr{H}\wedge {\mathrm{proj}}_{ℎ}\left(\perp \left(H\right)\right):\mathscr{H}⟶\mathscr{H}\wedge x\in \mathscr{H}\right)\to \left({\mathrm{proj}}_{ℎ}\left(H\right){+}_{\mathrm{op}}{\mathrm{proj}}_{ℎ}\left(\perp \left(H\right)\right)\right)\left(x\right)={\mathrm{proj}}_{ℎ}\left(H\right)\left(x\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(\perp \left(H\right)\right)\left(x\right)$$
9	5 7 8	mp3an12	$$⊢x\in \mathscr{H}\to \left({\mathrm{proj}}_{ℎ}\left(H\right){+}_{\mathrm{op}}{\mathrm{proj}}_{ℎ}\left(\perp \left(H\right)\right)\right)\left(x\right)={\mathrm{proj}}_{ℎ}\left(H\right)\left(x\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(\perp \left(H\right)\right)\left(x\right)$$
10	3 4 9	3eqtr4rd	$$⊢x\in \mathscr{H}\to \left({\mathrm{proj}}_{ℎ}\left(H\right){+}_{\mathrm{op}}{\mathrm{proj}}_{ℎ}\left(\perp \left(H\right)\right)\right)\left(x\right)={\mathrm{proj}}_{ℎ}\left(\mathscr{H}\right)\left(x\right)$$
11	10	rgen	$$⊢\forall x\in \mathscr{H}\left({\mathrm{proj}}_{ℎ}\left(H\right){+}_{\mathrm{op}}{\mathrm{proj}}_{ℎ}\left(\perp \left(H\right)\right)\right)\left(x\right)={\mathrm{proj}}_{ℎ}\left(\mathscr{H}\right)\left(x\right)$$
12	5 7	hoaddcli	$$⊢\left({\mathrm{proj}}_{ℎ}\left(H\right){+}_{\mathrm{op}}{\mathrm{proj}}_{ℎ}\left(\perp \left(H\right)\right)\right):\mathscr{H}⟶\mathscr{H}$$
13		helch	$$⊢\mathscr{H}\in {\mathbf{C}}_{\mathscr{H}}$$
14	13	pjfi	$$⊢{\mathrm{proj}}_{ℎ}\left(\mathscr{H}\right):\mathscr{H}⟶\mathscr{H}$$
15	12 14	hoeqi	$$⊢\forall x\in \mathscr{H}\left({\mathrm{proj}}_{ℎ}\left(H\right){+}_{\mathrm{op}}{\mathrm{proj}}_{ℎ}\left(\perp \left(H\right)\right)\right)\left(x\right)={\mathrm{proj}}_{ℎ}\left(\mathscr{H}\right)\left(x\right)\leftrightarrow {\mathrm{proj}}_{ℎ}\left(H\right){+}_{\mathrm{op}}{\mathrm{proj}}_{ℎ}\left(\perp \left(H\right)\right)={\mathrm{proj}}_{ℎ}\left(\mathscr{H}\right)$$
16	11 15	mpbi	$$⊢{\mathrm{proj}}_{ℎ}\left(H\right){+}_{\mathrm{op}}{\mathrm{proj}}_{ℎ}\left(\perp \left(H\right)\right)={\mathrm{proj}}_{ℎ}\left(\mathscr{H}\right)$$