# Metamath Proof Explorer

## Theorem his35

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

Ref Expression
Assertion his35 ${⊢}\left(\left({A}\in ℂ\wedge {B}\in ℂ\right)\wedge \left({C}\in ℋ\wedge {D}\in ℋ\right)\right)\to \left({A}{\cdot }_{ℎ}{C}\right){\cdot }_{\mathrm{ih}}\left({B}{\cdot }_{ℎ}{D}\right)={A}\stackrel{‾}{{B}}\left({C}{\cdot }_{\mathrm{ih}}{D}\right)$

### Proof

Step Hyp Ref Expression
1 his5 ${⊢}\left({B}\in ℂ\wedge {C}\in ℋ\wedge {D}\in ℋ\right)\to {C}{\cdot }_{\mathrm{ih}}\left({B}{\cdot }_{ℎ}{D}\right)=\stackrel{‾}{{B}}\left({C}{\cdot }_{\mathrm{ih}}{D}\right)$
2 1 3expb ${⊢}\left({B}\in ℂ\wedge \left({C}\in ℋ\wedge {D}\in ℋ\right)\right)\to {C}{\cdot }_{\mathrm{ih}}\left({B}{\cdot }_{ℎ}{D}\right)=\stackrel{‾}{{B}}\left({C}{\cdot }_{\mathrm{ih}}{D}\right)$
3 2 adantll ${⊢}\left(\left({A}\in ℂ\wedge {B}\in ℂ\right)\wedge \left({C}\in ℋ\wedge {D}\in ℋ\right)\right)\to {C}{\cdot }_{\mathrm{ih}}\left({B}{\cdot }_{ℎ}{D}\right)=\stackrel{‾}{{B}}\left({C}{\cdot }_{\mathrm{ih}}{D}\right)$
4 3 oveq2d ${⊢}\left(\left({A}\in ℂ\wedge {B}\in ℂ\right)\wedge \left({C}\in ℋ\wedge {D}\in ℋ\right)\right)\to {A}\left({C}{\cdot }_{\mathrm{ih}}\left({B}{\cdot }_{ℎ}{D}\right)\right)={A}\stackrel{‾}{{B}}\left({C}{\cdot }_{\mathrm{ih}}{D}\right)$
5 simpll ${⊢}\left(\left({A}\in ℂ\wedge {B}\in ℂ\right)\wedge \left({C}\in ℋ\wedge {D}\in ℋ\right)\right)\to {A}\in ℂ$
6 simprl ${⊢}\left(\left({A}\in ℂ\wedge {B}\in ℂ\right)\wedge \left({C}\in ℋ\wedge {D}\in ℋ\right)\right)\to {C}\in ℋ$
7 hvmulcl ${⊢}\left({B}\in ℂ\wedge {D}\in ℋ\right)\to {B}{\cdot }_{ℎ}{D}\in ℋ$
8 7 ad2ant2l ${⊢}\left(\left({A}\in ℂ\wedge {B}\in ℂ\right)\wedge \left({C}\in ℋ\wedge {D}\in ℋ\right)\right)\to {B}{\cdot }_{ℎ}{D}\in ℋ$
9 ax-his3 ${⊢}\left({A}\in ℂ\wedge {C}\in ℋ\wedge {B}{\cdot }_{ℎ}{D}\in ℋ\right)\to \left({A}{\cdot }_{ℎ}{C}\right){\cdot }_{\mathrm{ih}}\left({B}{\cdot }_{ℎ}{D}\right)={A}\left({C}{\cdot }_{\mathrm{ih}}\left({B}{\cdot }_{ℎ}{D}\right)\right)$
10 5 6 8 9 syl3anc ${⊢}\left(\left({A}\in ℂ\wedge {B}\in ℂ\right)\wedge \left({C}\in ℋ\wedge {D}\in ℋ\right)\right)\to \left({A}{\cdot }_{ℎ}{C}\right){\cdot }_{\mathrm{ih}}\left({B}{\cdot }_{ℎ}{D}\right)={A}\left({C}{\cdot }_{\mathrm{ih}}\left({B}{\cdot }_{ℎ}{D}\right)\right)$
11 cjcl ${⊢}{B}\in ℂ\to \stackrel{‾}{{B}}\in ℂ$
12 11 ad2antlr ${⊢}\left(\left({A}\in ℂ\wedge {B}\in ℂ\right)\wedge \left({C}\in ℋ\wedge {D}\in ℋ\right)\right)\to \stackrel{‾}{{B}}\in ℂ$
13 hicl ${⊢}\left({C}\in ℋ\wedge {D}\in ℋ\right)\to {C}{\cdot }_{\mathrm{ih}}{D}\in ℂ$
14 13 adantl ${⊢}\left(\left({A}\in ℂ\wedge {B}\in ℂ\right)\wedge \left({C}\in ℋ\wedge {D}\in ℋ\right)\right)\to {C}{\cdot }_{\mathrm{ih}}{D}\in ℂ$
15 5 12 14 mulassd ${⊢}\left(\left({A}\in ℂ\wedge {B}\in ℂ\right)\wedge \left({C}\in ℋ\wedge {D}\in ℋ\right)\right)\to {A}\stackrel{‾}{{B}}\left({C}{\cdot }_{\mathrm{ih}}{D}\right)={A}\stackrel{‾}{{B}}\left({C}{\cdot }_{\mathrm{ih}}{D}\right)$
16 4 10 15 3eqtr4d ${⊢}\left(\left({A}\in ℂ\wedge {B}\in ℂ\right)\wedge \left({C}\in ℋ\wedge {D}\in ℋ\right)\right)\to \left({A}{\cdot }_{ℎ}{C}\right){\cdot }_{\mathrm{ih}}\left({B}{\cdot }_{ℎ}{D}\right)={A}\stackrel{‾}{{B}}\left({C}{\cdot }_{\mathrm{ih}}{D}\right)$