# Metamath Proof Explorer

## Theorem his52

Description: Associative law for inner product. (Contributed by NM, 13-Feb-2006) (New usage is discouraged.)

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

### Proof

Step Hyp Ref Expression
1 cjcl ${⊢}{A}\in ℂ\to \stackrel{‾}{{A}}\in ℂ$
2 his5 ${⊢}\left(\stackrel{‾}{{A}}\in ℂ\wedge {B}\in ℋ\wedge {C}\in ℋ\right)\to {B}{\cdot }_{\mathrm{ih}}\left(\stackrel{‾}{{A}}{\cdot }_{ℎ}{C}\right)=\stackrel{‾}{\stackrel{‾}{{A}}}\left({B}{\cdot }_{\mathrm{ih}}{C}\right)$
3 1 2 syl3an1 ${⊢}\left({A}\in ℂ\wedge {B}\in ℋ\wedge {C}\in ℋ\right)\to {B}{\cdot }_{\mathrm{ih}}\left(\stackrel{‾}{{A}}{\cdot }_{ℎ}{C}\right)=\stackrel{‾}{\stackrel{‾}{{A}}}\left({B}{\cdot }_{\mathrm{ih}}{C}\right)$
4 cjcj ${⊢}{A}\in ℂ\to \stackrel{‾}{\stackrel{‾}{{A}}}={A}$
5 4 oveq1d ${⊢}{A}\in ℂ\to \stackrel{‾}{\stackrel{‾}{{A}}}\left({B}{\cdot }_{\mathrm{ih}}{C}\right)={A}\left({B}{\cdot }_{\mathrm{ih}}{C}\right)$
6 5 3ad2ant1 ${⊢}\left({A}\in ℂ\wedge {B}\in ℋ\wedge {C}\in ℋ\right)\to \stackrel{‾}{\stackrel{‾}{{A}}}\left({B}{\cdot }_{\mathrm{ih}}{C}\right)={A}\left({B}{\cdot }_{\mathrm{ih}}{C}\right)$
7 3 6 eqtrd ${⊢}\left({A}\in ℂ\wedge {B}\in ℋ\wedge {C}\in ℋ\right)\to {B}{\cdot }_{\mathrm{ih}}\left(\stackrel{‾}{{A}}{\cdot }_{ℎ}{C}\right)={A}\left({B}{\cdot }_{\mathrm{ih}}{C}\right)$