Theorem pjmuli

Description: Projection of scalar product is scalar product of projection. (Contributed by NM, 26-Nov-2000) (New usage is discouraged.)

	Ref	Expression
Hypothesis	pjadjt.1	$$⊢H\in {\mathbf{C}}_{\mathscr{H}}$$
Assertion	pjmuli	$$⊢\left(A\in ℂ\wedge B\in \mathscr{H}\right)\to {\mathrm{proj}}_{ℎ}\left(H\right)\left(A{\cdot }_{ℎ}B\right)=A{\cdot }_{ℎ}{\mathrm{proj}}_{ℎ}\left(H\right)\left(B\right)$$

Proof

Step	Hyp	Ref	Expression
1		pjadjt.1	$$⊢H\in {\mathbf{C}}_{\mathscr{H}}$$
2		fvoveq1	$$⊢A=if\left(A\in ℂ,A,0\right)\to {\mathrm{proj}}_{ℎ}\left(H\right)\left(A{\cdot }_{ℎ}B\right)={\mathrm{proj}}_{ℎ}\left(H\right)\left(if\left(A\in ℂ,A,0\right){\cdot }_{ℎ}B\right)$$
3		oveq1	$$⊢A=if\left(A\in ℂ,A,0\right)\to A{\cdot }_{ℎ}{\mathrm{proj}}_{ℎ}\left(H\right)\left(B\right)=if\left(A\in ℂ,A,0\right){\cdot }_{ℎ}{\mathrm{proj}}_{ℎ}\left(H\right)\left(B\right)$$
4	2 3	eqeq12d	$$⊢A=if\left(A\in ℂ,A,0\right)\to \left({\mathrm{proj}}_{ℎ}\left(H\right)\left(A{\cdot }_{ℎ}B\right)=A{\cdot }_{ℎ}{\mathrm{proj}}_{ℎ}\left(H\right)\left(B\right)\leftrightarrow {\mathrm{proj}}_{ℎ}\left(H\right)\left(if\left(A\in ℂ,A,0\right){\cdot }_{ℎ}B\right)=if\left(A\in ℂ,A,0\right){\cdot }_{ℎ}{\mathrm{proj}}_{ℎ}\left(H\right)\left(B\right)\right)$$
5		oveq2	$$⊢B=if\left(B\in \mathscr{H},B,0_{ℎ}\right)\to if\left(A\in ℂ,A,0\right){\cdot }_{ℎ}B=if\left(A\in ℂ,A,0\right){\cdot }_{ℎ}if\left(B\in \mathscr{H},B,0_{ℎ}\right)$$
6	5	fveq2d	$$⊢B=if\left(B\in \mathscr{H},B,0_{ℎ}\right)\to {\mathrm{proj}}_{ℎ}\left(H\right)\left(if\left(A\in ℂ,A,0\right){\cdot }_{ℎ}B\right)={\mathrm{proj}}_{ℎ}\left(H\right)\left(if\left(A\in ℂ,A,0\right){\cdot }_{ℎ}if\left(B\in \mathscr{H},B,0_{ℎ}\right)\right)$$
7		fveq2	$$⊢B=if\left(B\in \mathscr{H},B,0_{ℎ}\right)\to {\mathrm{proj}}_{ℎ}\left(H\right)\left(B\right)={\mathrm{proj}}_{ℎ}\left(H\right)\left(if\left(B\in \mathscr{H},B,0_{ℎ}\right)\right)$$
8	7	oveq2d	$$⊢B=if\left(B\in \mathscr{H},B,0_{ℎ}\right)\to if\left(A\in ℂ,A,0\right){\cdot }_{ℎ}{\mathrm{proj}}_{ℎ}\left(H\right)\left(B\right)=if\left(A\in ℂ,A,0\right){\cdot }_{ℎ}{\mathrm{proj}}_{ℎ}\left(H\right)\left(if\left(B\in \mathscr{H},B,0_{ℎ}\right)\right)$$
9	6 8	eqeq12d	$$⊢B=if\left(B\in \mathscr{H},B,0_{ℎ}\right)\to \left({\mathrm{proj}}_{ℎ}\left(H\right)\left(if\left(A\in ℂ,A,0\right){\cdot }_{ℎ}B\right)=if\left(A\in ℂ,A,0\right){\cdot }_{ℎ}{\mathrm{proj}}_{ℎ}\left(H\right)\left(B\right)\leftrightarrow {\mathrm{proj}}_{ℎ}\left(H\right)\left(if\left(A\in ℂ,A,0\right){\cdot }_{ℎ}if\left(B\in \mathscr{H},B,0_{ℎ}\right)\right)=if\left(A\in ℂ,A,0\right){\cdot }_{ℎ}{\mathrm{proj}}_{ℎ}\left(H\right)\left(if\left(B\in \mathscr{H},B,0_{ℎ}\right)\right)\right)$$
10		ifhvhv0	$$⊢if\left(B\in \mathscr{H},B,0_{ℎ}\right)\in \mathscr{H}$$
11		0cn	$$⊢0\in ℂ$$
12	11	elimel	$$⊢if\left(A\in ℂ,A,0\right)\in ℂ$$
13	1 10 12	pjmulii	$$⊢{\mathrm{proj}}_{ℎ}\left(H\right)\left(if\left(A\in ℂ,A,0\right){\cdot }_{ℎ}if\left(B\in \mathscr{H},B,0_{ℎ}\right)\right)=if\left(A\in ℂ,A,0\right){\cdot }_{ℎ}{\mathrm{proj}}_{ℎ}\left(H\right)\left(if\left(B\in \mathscr{H},B,0_{ℎ}\right)\right)$$
14	4 9 13	dedth2h	$$⊢\left(A\in ℂ\wedge B\in \mathscr{H}\right)\to {\mathrm{proj}}_{ℎ}\left(H\right)\left(A{\cdot }_{ℎ}B\right)=A{\cdot }_{ℎ}{\mathrm{proj}}_{ℎ}\left(H\right)\left(B\right)$$