Theorem pjmulii

Description: Projection of (scalar) product is product of projection. (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}$$
	pjmul.3	$$⊢C\in ℂ$$
Assertion	pjmulii	$$⊢{\mathrm{proj}}_{ℎ}\left(H\right)\left(C{\cdot }_{ℎ}A\right)=C{\cdot }_{ℎ}{\mathrm{proj}}_{ℎ}\left(H\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		pjmul.3	$$⊢C\in ℂ$$
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	4	oveq2i	$$⊢C{\cdot }_{ℎ}A=C{\cdot }_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(\perp \left(H\right)\right)\left(A\right)\right)$$
6	1 2	pjhclii	$$⊢{\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)\in \mathscr{H}$$
7	1	choccli	$$⊢\perp \left(H\right)\in {\mathbf{C}}_{\mathscr{H}}$$
8	7 2	pjhclii	$$⊢{\mathrm{proj}}_{ℎ}\left(\perp \left(H\right)\right)\left(A\right)\in \mathscr{H}$$
9	3 6 8	hvdistr1i	$$⊢C{\cdot }_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(\perp \left(H\right)\right)\left(A\right)\right)=\left(C{\cdot }_{ℎ}{\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)\right){+}_{ℎ}\left(C{\cdot }_{ℎ}{\mathrm{proj}}_{ℎ}\left(\perp \left(H\right)\right)\left(A\right)\right)$$
10	5 9	eqtri	$$⊢C{\cdot }_{ℎ}A=\left(C{\cdot }_{ℎ}{\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)\right){+}_{ℎ}\left(C{\cdot }_{ℎ}{\mathrm{proj}}_{ℎ}\left(\perp \left(H\right)\right)\left(A\right)\right)$$
11	10	fveq2i	$$⊢{\mathrm{proj}}_{ℎ}\left(H\right)\left(C{\cdot }_{ℎ}A\right)={\mathrm{proj}}_{ℎ}\left(H\right)\left(\left(C{\cdot }_{ℎ}{\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)\right){+}_{ℎ}\left(C{\cdot }_{ℎ}{\mathrm{proj}}_{ℎ}\left(\perp \left(H\right)\right)\left(A\right)\right)\right)$$
12	1	chshii	$$⊢H\in {\mathbf{S}}_{\mathscr{H}}$$
13	1 2	pjclii	$$⊢{\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)\in H$$
14		shmulcl	$$⊢\left(H\in {\mathbf{S}}_{\mathscr{H}}\wedge C\in ℂ\wedge {\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)\in H\right)\to C{\cdot }_{ℎ}{\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)\in H$$
15	12 3 13 14	mp3an	$$⊢C{\cdot }_{ℎ}{\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)\in H$$
16	7	chshii	$$⊢\perp \left(H\right)\in {\mathbf{S}}_{\mathscr{H}}$$
17	7 2	pjclii	$$⊢{\mathrm{proj}}_{ℎ}\left(\perp \left(H\right)\right)\left(A\right)\in \perp \left(H\right)$$
18		shmulcl	$$⊢\left(\perp \left(H\right)\in {\mathbf{S}}_{\mathscr{H}}\wedge C\in ℂ\wedge {\mathrm{proj}}_{ℎ}\left(\perp \left(H\right)\right)\left(A\right)\in \perp \left(H\right)\right)\to C{\cdot }_{ℎ}{\mathrm{proj}}_{ℎ}\left(\perp \left(H\right)\right)\left(A\right)\in \perp \left(H\right)$$
19	16 3 17 18	mp3an	$$⊢C{\cdot }_{ℎ}{\mathrm{proj}}_{ℎ}\left(\perp \left(H\right)\right)\left(A\right)\in \perp \left(H\right)$$
20	1	pjcompi	$$⊢\left(C{\cdot }_{ℎ}{\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)\in H\wedge C{\cdot }_{ℎ}{\mathrm{proj}}_{ℎ}\left(\perp \left(H\right)\right)\left(A\right)\in \perp \left(H\right)\right)\to {\mathrm{proj}}_{ℎ}\left(H\right)\left(\left(C{\cdot }_{ℎ}{\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)\right){+}_{ℎ}\left(C{\cdot }_{ℎ}{\mathrm{proj}}_{ℎ}\left(\perp \left(H\right)\right)\left(A\right)\right)\right)=C{\cdot }_{ℎ}{\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)$$
21	15 19 20	mp2an	$$⊢{\mathrm{proj}}_{ℎ}\left(H\right)\left(\left(C{\cdot }_{ℎ}{\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)\right){+}_{ℎ}\left(C{\cdot }_{ℎ}{\mathrm{proj}}_{ℎ}\left(\perp \left(H\right)\right)\left(A\right)\right)\right)=C{\cdot }_{ℎ}{\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)$$
22	11 21	eqtri	$$⊢{\mathrm{proj}}_{ℎ}\left(H\right)\left(C{\cdot }_{ℎ}A\right)=C{\cdot }_{ℎ}{\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)$$