# Metamath Proof Explorer

## Theorem his5

Description: Associative law for inner product. Lemma 3.1(S5) of Beran p. 95. (Contributed by NM, 29-Jul-1999) (New usage is discouraged.)

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

### Proof

Step Hyp Ref Expression
1 hvmulcl ${⊢}\left({A}\in ℂ\wedge {C}\in ℋ\right)\to {A}{\cdot }_{ℎ}{C}\in ℋ$
2 ax-his1 ${⊢}\left({B}\in ℋ\wedge {A}{\cdot }_{ℎ}{C}\in ℋ\right)\to {B}{\cdot }_{\mathrm{ih}}\left({A}{\cdot }_{ℎ}{C}\right)=\stackrel{‾}{\left({A}{\cdot }_{ℎ}{C}\right){\cdot }_{\mathrm{ih}}{B}}$
3 1 2 sylan2 ${⊢}\left({B}\in ℋ\wedge \left({A}\in ℂ\wedge {C}\in ℋ\right)\right)\to {B}{\cdot }_{\mathrm{ih}}\left({A}{\cdot }_{ℎ}{C}\right)=\stackrel{‾}{\left({A}{\cdot }_{ℎ}{C}\right){\cdot }_{\mathrm{ih}}{B}}$
4 3 3impb ${⊢}\left({B}\in ℋ\wedge {A}\in ℂ\wedge {C}\in ℋ\right)\to {B}{\cdot }_{\mathrm{ih}}\left({A}{\cdot }_{ℎ}{C}\right)=\stackrel{‾}{\left({A}{\cdot }_{ℎ}{C}\right){\cdot }_{\mathrm{ih}}{B}}$
5 4 3com12 ${⊢}\left({A}\in ℂ\wedge {B}\in ℋ\wedge {C}\in ℋ\right)\to {B}{\cdot }_{\mathrm{ih}}\left({A}{\cdot }_{ℎ}{C}\right)=\stackrel{‾}{\left({A}{\cdot }_{ℎ}{C}\right){\cdot }_{\mathrm{ih}}{B}}$
6 ax-his3 ${⊢}\left({A}\in ℂ\wedge {C}\in ℋ\wedge {B}\in ℋ\right)\to \left({A}{\cdot }_{ℎ}{C}\right){\cdot }_{\mathrm{ih}}{B}={A}\left({C}{\cdot }_{\mathrm{ih}}{B}\right)$
7 6 3com23 ${⊢}\left({A}\in ℂ\wedge {B}\in ℋ\wedge {C}\in ℋ\right)\to \left({A}{\cdot }_{ℎ}{C}\right){\cdot }_{\mathrm{ih}}{B}={A}\left({C}{\cdot }_{\mathrm{ih}}{B}\right)$
8 7 fveq2d ${⊢}\left({A}\in ℂ\wedge {B}\in ℋ\wedge {C}\in ℋ\right)\to \stackrel{‾}{\left({A}{\cdot }_{ℎ}{C}\right){\cdot }_{\mathrm{ih}}{B}}=\stackrel{‾}{{A}\left({C}{\cdot }_{\mathrm{ih}}{B}\right)}$
9 hicl ${⊢}\left({C}\in ℋ\wedge {B}\in ℋ\right)\to {C}{\cdot }_{\mathrm{ih}}{B}\in ℂ$
10 cjmul ${⊢}\left({A}\in ℂ\wedge {C}{\cdot }_{\mathrm{ih}}{B}\in ℂ\right)\to \stackrel{‾}{{A}\left({C}{\cdot }_{\mathrm{ih}}{B}\right)}=\stackrel{‾}{{A}}\stackrel{‾}{{C}{\cdot }_{\mathrm{ih}}{B}}$
11 9 10 sylan2 ${⊢}\left({A}\in ℂ\wedge \left({C}\in ℋ\wedge {B}\in ℋ\right)\right)\to \stackrel{‾}{{A}\left({C}{\cdot }_{\mathrm{ih}}{B}\right)}=\stackrel{‾}{{A}}\stackrel{‾}{{C}{\cdot }_{\mathrm{ih}}{B}}$
12 11 3impb ${⊢}\left({A}\in ℂ\wedge {C}\in ℋ\wedge {B}\in ℋ\right)\to \stackrel{‾}{{A}\left({C}{\cdot }_{\mathrm{ih}}{B}\right)}=\stackrel{‾}{{A}}\stackrel{‾}{{C}{\cdot }_{\mathrm{ih}}{B}}$
13 12 3com23 ${⊢}\left({A}\in ℂ\wedge {B}\in ℋ\wedge {C}\in ℋ\right)\to \stackrel{‾}{{A}\left({C}{\cdot }_{\mathrm{ih}}{B}\right)}=\stackrel{‾}{{A}}\stackrel{‾}{{C}{\cdot }_{\mathrm{ih}}{B}}$
14 ax-his1 ${⊢}\left({B}\in ℋ\wedge {C}\in ℋ\right)\to {B}{\cdot }_{\mathrm{ih}}{C}=\stackrel{‾}{{C}{\cdot }_{\mathrm{ih}}{B}}$
15 14 3adant1 ${⊢}\left({A}\in ℂ\wedge {B}\in ℋ\wedge {C}\in ℋ\right)\to {B}{\cdot }_{\mathrm{ih}}{C}=\stackrel{‾}{{C}{\cdot }_{\mathrm{ih}}{B}}$
16 15 oveq2d ${⊢}\left({A}\in ℂ\wedge {B}\in ℋ\wedge {C}\in ℋ\right)\to \stackrel{‾}{{A}}\left({B}{\cdot }_{\mathrm{ih}}{C}\right)=\stackrel{‾}{{A}}\stackrel{‾}{{C}{\cdot }_{\mathrm{ih}}{B}}$
17 13 16 eqtr4d ${⊢}\left({A}\in ℂ\wedge {B}\in ℋ\wedge {C}\in ℋ\right)\to \stackrel{‾}{{A}\left({C}{\cdot }_{\mathrm{ih}}{B}\right)}=\stackrel{‾}{{A}}\left({B}{\cdot }_{\mathrm{ih}}{C}\right)$
18 5 8 17 3eqtrd ${⊢}\left({A}\in ℂ\wedge {B}\in ℋ\wedge {C}\in ℋ\right)\to {B}{\cdot }_{\mathrm{ih}}\left({A}{\cdot }_{ℎ}{C}\right)=\stackrel{‾}{{A}}\left({B}{\cdot }_{\mathrm{ih}}{C}\right)$