Theorem pjaddii

Description: Projection of vector sum is sum of projections. (Contributed by NM, 31-Oct-1999) (New usage is discouraged.)

	Ref	Expression
Hypotheses	pjidm.1	$$⊢H\in {\mathbf{C}}_{\mathscr{H}}$$
	pjidm.2	$$⊢A\in \mathscr{H}$$
	pjadj.3	$$⊢B\in \mathscr{H}$$
Assertion	pjaddii	$$⊢{\mathrm{proj}}_{ℎ}\left(H\right)\left(A{+}_{ℎ}B\right)={\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(H\right)\left(B\right)$$

Proof

Step	Hyp	Ref	Expression
1		pjidm.1	$$⊢H\in {\mathbf{C}}_{\mathscr{H}}$$
2		pjidm.2	$$⊢A\in \mathscr{H}$$
3		pjadj.3	$$⊢B\in \mathscr{H}$$
4	1 2	pjpji	$$⊢A={\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(\perp \left(H\right)\right)\left(A\right)$$
5	1 3	pjpji	$$⊢B={\mathrm{proj}}_{ℎ}\left(H\right)\left(B\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(\perp \left(H\right)\right)\left(B\right)$$
6	4 5	oveq12i	$$⊢A{+}_{ℎ}B=\left({\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(\perp \left(H\right)\right)\left(A\right)\right){+}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(H\right)\left(B\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(\perp \left(H\right)\right)\left(B\right)\right)$$
7	1 2	pjhclii	$$⊢{\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)\in \mathscr{H}$$
8	1	choccli	$$⊢\perp \left(H\right)\in {\mathbf{C}}_{\mathscr{H}}$$
9	8 2	pjhclii	$$⊢{\mathrm{proj}}_{ℎ}\left(\perp \left(H\right)\right)\left(A\right)\in \mathscr{H}$$
10	1 3	pjhclii	$$⊢{\mathrm{proj}}_{ℎ}\left(H\right)\left(B\right)\in \mathscr{H}$$
11	8 3	pjhclii	$$⊢{\mathrm{proj}}_{ℎ}\left(\perp \left(H\right)\right)\left(B\right)\in \mathscr{H}$$
12	7 9 10 11	hvadd4i	$$⊢\left({\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(\perp \left(H\right)\right)\left(A\right)\right){+}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(H\right)\left(B\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(\perp \left(H\right)\right)\left(B\right)\right)=\left({\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(H\right)\left(B\right)\right){+}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(\perp \left(H\right)\right)\left(A\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(\perp \left(H\right)\right)\left(B\right)\right)$$
13	6 12	eqtri	$$⊢A{+}_{ℎ}B=\left({\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(H\right)\left(B\right)\right){+}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(\perp \left(H\right)\right)\left(A\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(\perp \left(H\right)\right)\left(B\right)\right)$$
14	13	fveq2i	$$⊢{\mathrm{proj}}_{ℎ}\left(H\right)\left(A{+}_{ℎ}B\right)={\mathrm{proj}}_{ℎ}\left(H\right)\left(\left({\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(H\right)\left(B\right)\right){+}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(\perp \left(H\right)\right)\left(A\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(\perp \left(H\right)\right)\left(B\right)\right)\right)$$
15	1	chshii	$$⊢H\in {\mathbf{S}}_{\mathscr{H}}$$
16	1 2	pjclii	$$⊢{\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)\in H$$
17	1 3	pjclii	$$⊢{\mathrm{proj}}_{ℎ}\left(H\right)\left(B\right)\in H$$
18		shaddcl	$$⊢\left(H\in {\mathbf{S}}_{\mathscr{H}}\wedge {\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)\in H\wedge {\mathrm{proj}}_{ℎ}\left(H\right)\left(B\right)\in H\right)\to {\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(H\right)\left(B\right)\in H$$
19	15 16 17 18	mp3an	$$⊢{\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(H\right)\left(B\right)\in H$$
20	8	chshii	$$⊢\perp \left(H\right)\in {\mathbf{S}}_{\mathscr{H}}$$
21	8 2	pjclii	$$⊢{\mathrm{proj}}_{ℎ}\left(\perp \left(H\right)\right)\left(A\right)\in \perp \left(H\right)$$
22	8 3	pjclii	$$⊢{\mathrm{proj}}_{ℎ}\left(\perp \left(H\right)\right)\left(B\right)\in \perp \left(H\right)$$
23		shaddcl	$$⊢\left(\perp \left(H\right)\in {\mathbf{S}}_{\mathscr{H}}\wedge {\mathrm{proj}}_{ℎ}\left(\perp \left(H\right)\right)\left(A\right)\in \perp \left(H\right)\wedge {\mathrm{proj}}_{ℎ}\left(\perp \left(H\right)\right)\left(B\right)\in \perp \left(H\right)\right)\to {\mathrm{proj}}_{ℎ}\left(\perp \left(H\right)\right)\left(A\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(\perp \left(H\right)\right)\left(B\right)\in \perp \left(H\right)$$
24	20 21 22 23	mp3an	$$⊢{\mathrm{proj}}_{ℎ}\left(\perp \left(H\right)\right)\left(A\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(\perp \left(H\right)\right)\left(B\right)\in \perp \left(H\right)$$
25	1	pjcompi	$$⊢\left({\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(H\right)\left(B\right)\in H\wedge {\mathrm{proj}}_{ℎ}\left(\perp \left(H\right)\right)\left(A\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(\perp \left(H\right)\right)\left(B\right)\in \perp \left(H\right)\right)\to {\mathrm{proj}}_{ℎ}\left(H\right)\left(\left({\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(H\right)\left(B\right)\right){+}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(\perp \left(H\right)\right)\left(A\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(\perp \left(H\right)\right)\left(B\right)\right)\right)={\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(H\right)\left(B\right)$$
26	19 24 25	mp2an	$$⊢{\mathrm{proj}}_{ℎ}\left(H\right)\left(\left({\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(H\right)\left(B\right)\right){+}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(\perp \left(H\right)\right)\left(A\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(\perp \left(H\right)\right)\left(B\right)\right)\right)={\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(H\right)\left(B\right)$$
27	14 26	eqtri	$$⊢{\mathrm{proj}}_{ℎ}\left(H\right)\left(A{+}_{ℎ}B\right)={\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(H\right)\left(B\right)$$