Theorem pjcji

Description: The projection on a subspace join is the sum of the projections. (Contributed by NM, 1-Nov-1999) (New usage is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		pjidm.1	$$⊢H\in {\mathbf{C}}_{\mathscr{H}}$$
2		pjidm.2	$$⊢A\in \mathscr{H}$$
3		pjsslem.1	$$⊢G\in {\mathbf{C}}_{\mathscr{H}}$$
4	3	choccli	$$⊢\perp \left(G\right)\in {\mathbf{C}}_{\mathscr{H}}$$
5	1 2 4	pjssmii	$$⊢H\subseteq \perp \left(G\right)\to {\mathrm{proj}}_{ℎ}\left(\perp \left(G\right)\right)\left(A\right){-}_{ℎ}{\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)={\mathrm{proj}}_{ℎ}\left(\perp \left(G\right)\cap \perp \left(H\right)\right)\left(A\right)$$
6	5	oveq2d	$$⊢H\subseteq \perp \left(G\right)\to A{-}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(\perp \left(G\right)\right)\left(A\right){-}_{ℎ}{\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)\right)=A{-}_{ℎ}{\mathrm{proj}}_{ℎ}\left(\perp \left(G\right)\cap \perp \left(H\right)\right)\left(A\right)$$
7	3 2	pjpoi	$$⊢{\mathrm{proj}}_{ℎ}\left(G\right)\left(A\right)=A{-}_{ℎ}{\mathrm{proj}}_{ℎ}\left(\perp \left(G\right)\right)\left(A\right)$$
8	7	oveq2i	$$⊢{\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(G\right)\left(A\right)={\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right){+}_{ℎ}\left(A{-}_{ℎ}{\mathrm{proj}}_{ℎ}\left(\perp \left(G\right)\right)\left(A\right)\right)$$
9	4 2	pjhclii	$$⊢{\mathrm{proj}}_{ℎ}\left(\perp \left(G\right)\right)\left(A\right)\in \mathscr{H}$$
10	1 2	pjhclii	$$⊢{\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)\in \mathscr{H}$$
11	9 10	hvnegdii	$$⊢-1{\cdot }_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(\perp \left(G\right)\right)\left(A\right){-}_{ℎ}{\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)\right)={\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right){-}_{ℎ}{\mathrm{proj}}_{ℎ}\left(\perp \left(G\right)\right)\left(A\right)$$
12	11	oveq2i	$$⊢A{+}_{ℎ}\left(-1{\cdot }_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(\perp \left(G\right)\right)\left(A\right){-}_{ℎ}{\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)\right)\right)=A{+}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right){-}_{ℎ}{\mathrm{proj}}_{ℎ}\left(\perp \left(G\right)\right)\left(A\right)\right)$$
13		hvaddsub12	$$⊢\left({\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)\in \mathscr{H}\wedge A\in \mathscr{H}\wedge {\mathrm{proj}}_{ℎ}\left(\perp \left(G\right)\right)\left(A\right)\in \mathscr{H}\right)\to {\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right){+}_{ℎ}\left(A{-}_{ℎ}{\mathrm{proj}}_{ℎ}\left(\perp \left(G\right)\right)\left(A\right)\right)=A{+}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right){-}_{ℎ}{\mathrm{proj}}_{ℎ}\left(\perp \left(G\right)\right)\left(A\right)\right)$$
14	10 2 9 13	mp3an	$$⊢{\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right){+}_{ℎ}\left(A{-}_{ℎ}{\mathrm{proj}}_{ℎ}\left(\perp \left(G\right)\right)\left(A\right)\right)=A{+}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right){-}_{ℎ}{\mathrm{proj}}_{ℎ}\left(\perp \left(G\right)\right)\left(A\right)\right)$$
15	12 14	eqtr4i	$$⊢A{+}_{ℎ}\left(-1{\cdot }_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(\perp \left(G\right)\right)\left(A\right){-}_{ℎ}{\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)\right)\right)={\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right){+}_{ℎ}\left(A{-}_{ℎ}{\mathrm{proj}}_{ℎ}\left(\perp \left(G\right)\right)\left(A\right)\right)$$
16	8 15	eqtr4i	$$⊢{\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(G\right)\left(A\right)=A{+}_{ℎ}\left(-1{\cdot }_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(\perp \left(G\right)\right)\left(A\right){-}_{ℎ}{\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)\right)\right)$$
17	9 10	hvsubcli	$$⊢{\mathrm{proj}}_{ℎ}\left(\perp \left(G\right)\right)\left(A\right){-}_{ℎ}{\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)\in \mathscr{H}$$
18	2 17	hvsubvali	$$⊢A{-}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(\perp \left(G\right)\right)\left(A\right){-}_{ℎ}{\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)\right)=A{+}_{ℎ}\left(-1{\cdot }_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(\perp \left(G\right)\right)\left(A\right){-}_{ℎ}{\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)\right)\right)$$
19	16 18	eqtr4i	$$⊢{\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(G\right)\left(A\right)=A{-}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(\perp \left(G\right)\right)\left(A\right){-}_{ℎ}{\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)\right)$$
20	1 3	chjcomi	$$⊢H{\vee }_{\mathscr{H}}G=G{\vee }_{\mathscr{H}}H$$
21	3 1	chdmm4i	$$⊢\perp \left(\perp \left(G\right)\cap \perp \left(H\right)\right)=G{\vee }_{\mathscr{H}}H$$
22	20 21	eqtr4i	$$⊢H{\vee }_{\mathscr{H}}G=\perp \left(\perp \left(G\right)\cap \perp \left(H\right)\right)$$
23	22	fveq2i	$$⊢{\mathrm{proj}}_{ℎ}\left(H{\vee }_{\mathscr{H}}G\right)={\mathrm{proj}}_{ℎ}\left(\perp \left(\perp \left(G\right)\cap \perp \left(H\right)\right)\right)$$
24	23	fveq1i	$$⊢{\mathrm{proj}}_{ℎ}\left(H{\vee }_{\mathscr{H}}G\right)\left(A\right)={\mathrm{proj}}_{ℎ}\left(\perp \left(\perp \left(G\right)\cap \perp \left(H\right)\right)\right)\left(A\right)$$
25	1	choccli	$$⊢\perp \left(H\right)\in {\mathbf{C}}_{\mathscr{H}}$$
26	4 25	chincli	$$⊢\perp \left(G\right)\cap \perp \left(H\right)\in {\mathbf{C}}_{\mathscr{H}}$$
27	26 2	pjopi	$$⊢{\mathrm{proj}}_{ℎ}\left(\perp \left(\perp \left(G\right)\cap \perp \left(H\right)\right)\right)\left(A\right)=A{-}_{ℎ}{\mathrm{proj}}_{ℎ}\left(\perp \left(G\right)\cap \perp \left(H\right)\right)\left(A\right)$$
28	24 27	eqtri	$$⊢{\mathrm{proj}}_{ℎ}\left(H{\vee }_{\mathscr{H}}G\right)\left(A\right)=A{-}_{ℎ}{\mathrm{proj}}_{ℎ}\left(\perp \left(G\right)\cap \perp \left(H\right)\right)\left(A\right)$$
29	6 19 28	3eqtr4g	$$⊢H\subseteq \perp \left(G\right)\to {\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(G\right)\left(A\right)={\mathrm{proj}}_{ℎ}\left(H{\vee }_{\mathscr{H}}G\right)\left(A\right)$$
30	29	eqcomd	$$⊢H\subseteq \perp \left(G\right)\to {\mathrm{proj}}_{ℎ}\left(H{\vee }_{\mathscr{H}}G\right)\left(A\right)={\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(G\right)\left(A\right)$$