Theorem pjscji

Description: The projection of orthogonal subspaces is the sum of the projections. (Contributed by NM, 11-Nov-2000) (New usage is discouraged.)

	Ref	Expression
Hypotheses	pjco.1	$$⊢G\in {\mathbf{C}}_{\mathscr{H}}$$
	pjco.2	$$⊢H\in {\mathbf{C}}_{\mathscr{H}}$$
Assertion	pjscji	$$⊢G\subseteq \perp \left(H\right)\to {\mathrm{proj}}_{ℎ}\left(G{\vee }_{\mathscr{H}}H\right)={\mathrm{proj}}_{ℎ}\left(G\right){+}_{\mathrm{op}}{\mathrm{proj}}_{ℎ}\left(H\right)$$

Proof

Step	Hyp	Ref	Expression
1		pjco.1	$$⊢G\in {\mathbf{C}}_{\mathscr{H}}$$
2		pjco.2	$$⊢H\in {\mathbf{C}}_{\mathscr{H}}$$
3		pjcjt2	$$⊢\left(G\in {\mathbf{C}}_{\mathscr{H}}\wedge H\in {\mathbf{C}}_{\mathscr{H}}\wedge x\in \mathscr{H}\right)\to \left(G\subseteq \perp \left(H\right)\to {\mathrm{proj}}_{ℎ}\left(G{\vee }_{\mathscr{H}}H\right)\left(x\right)={\mathrm{proj}}_{ℎ}\left(G\right)\left(x\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(H\right)\left(x\right)\right)$$
4	1 2 3	mp3an12	$$⊢x\in \mathscr{H}\to \left(G\subseteq \perp \left(H\right)\to {\mathrm{proj}}_{ℎ}\left(G{\vee }_{\mathscr{H}}H\right)\left(x\right)={\mathrm{proj}}_{ℎ}\left(G\right)\left(x\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(H\right)\left(x\right)\right)$$
5	4	impcom	$$⊢\left(G\subseteq \perp \left(H\right)\wedge x\in \mathscr{H}\right)\to {\mathrm{proj}}_{ℎ}\left(G{\vee }_{\mathscr{H}}H\right)\left(x\right)={\mathrm{proj}}_{ℎ}\left(G\right)\left(x\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(H\right)\left(x\right)$$
6	1	pjfi	$$⊢{\mathrm{proj}}_{ℎ}\left(G\right):\mathscr{H}⟶\mathscr{H}$$
7	2	pjfi	$$⊢{\mathrm{proj}}_{ℎ}\left(H\right):\mathscr{H}⟶\mathscr{H}$$
8		hosval	$$⊢\left({\mathrm{proj}}_{ℎ}\left(G\right):\mathscr{H}⟶\mathscr{H}\wedge {\mathrm{proj}}_{ℎ}\left(H\right):\mathscr{H}⟶\mathscr{H}\wedge x\in \mathscr{H}\right)\to \left({\mathrm{proj}}_{ℎ}\left(G\right){+}_{\mathrm{op}}{\mathrm{proj}}_{ℎ}\left(H\right)\right)\left(x\right)={\mathrm{proj}}_{ℎ}\left(G\right)\left(x\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(H\right)\left(x\right)$$
9	6 7 8	mp3an12	$$⊢x\in \mathscr{H}\to \left({\mathrm{proj}}_{ℎ}\left(G\right){+}_{\mathrm{op}}{\mathrm{proj}}_{ℎ}\left(H\right)\right)\left(x\right)={\mathrm{proj}}_{ℎ}\left(G\right)\left(x\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(H\right)\left(x\right)$$
10	9	adantl	$$⊢\left(G\subseteq \perp \left(H\right)\wedge x\in \mathscr{H}\right)\to \left({\mathrm{proj}}_{ℎ}\left(G\right){+}_{\mathrm{op}}{\mathrm{proj}}_{ℎ}\left(H\right)\right)\left(x\right)={\mathrm{proj}}_{ℎ}\left(G\right)\left(x\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(H\right)\left(x\right)$$
11	5 10	eqtr4d	$$⊢\left(G\subseteq \perp \left(H\right)\wedge x\in \mathscr{H}\right)\to {\mathrm{proj}}_{ℎ}\left(G{\vee }_{\mathscr{H}}H\right)\left(x\right)=\left({\mathrm{proj}}_{ℎ}\left(G\right){+}_{\mathrm{op}}{\mathrm{proj}}_{ℎ}\left(H\right)\right)\left(x\right)$$
12	11	ralrimiva	$$⊢G\subseteq \perp \left(H\right)\to \forall x\in \mathscr{H}{\mathrm{proj}}_{ℎ}\left(G{\vee }_{\mathscr{H}}H\right)\left(x\right)=\left({\mathrm{proj}}_{ℎ}\left(G\right){+}_{\mathrm{op}}{\mathrm{proj}}_{ℎ}\left(H\right)\right)\left(x\right)$$
13	1 2	chjcli	$$⊢G{\vee }_{\mathscr{H}}H\in {\mathbf{C}}_{\mathscr{H}}$$
14	13	pjfi	$$⊢{\mathrm{proj}}_{ℎ}\left(G{\vee }_{\mathscr{H}}H\right):\mathscr{H}⟶\mathscr{H}$$
15	6 7	hoaddcli	$$⊢\left({\mathrm{proj}}_{ℎ}\left(G\right){+}_{\mathrm{op}}{\mathrm{proj}}_{ℎ}\left(H\right)\right):\mathscr{H}⟶\mathscr{H}$$
16	14 15	hoeqi	$$⊢\forall x\in \mathscr{H}{\mathrm{proj}}_{ℎ}\left(G{\vee }_{\mathscr{H}}H\right)\left(x\right)=\left({\mathrm{proj}}_{ℎ}\left(G\right){+}_{\mathrm{op}}{\mathrm{proj}}_{ℎ}\left(H\right)\right)\left(x\right)\leftrightarrow {\mathrm{proj}}_{ℎ}\left(G{\vee }_{\mathscr{H}}H\right)={\mathrm{proj}}_{ℎ}\left(G\right){+}_{\mathrm{op}}{\mathrm{proj}}_{ℎ}\left(H\right)$$
17	12 16	sylib	$$⊢G\subseteq \perp \left(H\right)\to {\mathrm{proj}}_{ℎ}\left(G{\vee }_{\mathscr{H}}H\right)={\mathrm{proj}}_{ℎ}\left(G\right){+}_{\mathrm{op}}{\mathrm{proj}}_{ℎ}\left(H\right)$$