Theorem his35i

Description: Move scalar multiplication to outside of inner product. (Contributed by NM, 1-Jul-2005) (Revised by Mario Carneiro, 15-May-2014) (New usage is discouraged.)

	Ref	Expression
Hypotheses	his35.1	$$⊢A\in ℂ$$
	his35.2	$$⊢B\in ℂ$$
	his35.3	$$⊢C\in \mathscr{H}$$
	his35.4	$$⊢D\in \mathscr{H}$$
Assertion	his35i	$$⊢\left(A{\cdot }_{ℎ}C\right){\cdot }_{\mathrm{ih}}\left(B{\cdot }_{ℎ}D\right)=A\bar{B}\left(C{\cdot }_{\mathrm{ih}}D\right)$$

Proof

Step	Hyp	Ref	Expression
1		his35.1	$$⊢A\in ℂ$$
2		his35.2	$$⊢B\in ℂ$$
3		his35.3	$$⊢C\in \mathscr{H}$$
4		his35.4	$$⊢D\in \mathscr{H}$$
5		his35	$$⊢\left(\left(A\in ℂ\wedge B\in ℂ\right)\wedge \left(C\in \mathscr{H}\wedge D\in \mathscr{H}\right)\right)\to \left(A{\cdot }_{ℎ}C\right){\cdot }_{\mathrm{ih}}\left(B{\cdot }_{ℎ}D\right)=A\bar{B}\left(C{\cdot }_{\mathrm{ih}}D\right)$$
6	1 2 3 4 5	mp4an	$$⊢\left(A{\cdot }_{ℎ}C\right){\cdot }_{\mathrm{ih}}\left(B{\cdot }_{ℎ}D\right)=A\bar{B}\left(C{\cdot }_{\mathrm{ih}}D\right)$$