# Metamath Proof Explorer

## Axiom ax-his3

Description: Associative law for inner product. Postulate (S3) of Beran p. 95. Warning: Mathematics textbooks usually use our version of the axiom. Physics textbooks, on the other hand, usually replace the left-hand side with ( B .ih ( A .h C ) ) (e.g., Equation 1.21b of Hughes p. 44; Definition (iii) of ReedSimon p. 36). See the comments in df-bra for why the physics definition is swapped. (Contributed by NM, 29-May-1999) (New usage is discouraged.)

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

### Detailed syntax breakdown

Step Hyp Ref Expression
0 cA ${class}{A}$
1 cc ${class}ℂ$
2 0 1 wcel ${wff}{A}\in ℂ$
3 cB ${class}{B}$
4 chba ${class}ℋ$
5 3 4 wcel ${wff}{B}\in ℋ$
6 cC ${class}{C}$
7 6 4 wcel ${wff}{C}\in ℋ$
8 2 5 7 w3a ${wff}\left({A}\in ℂ\wedge {B}\in ℋ\wedge {C}\in ℋ\right)$
9 csm ${class}{\cdot }_{ℎ}$
10 0 3 9 co ${class}\left({A}{\cdot }_{ℎ}{B}\right)$
11 csp ${class}{\cdot }_{\mathrm{ih}}$
12 10 6 11 co ${class}\left(\left({A}{\cdot }_{ℎ}{B}\right){\cdot }_{\mathrm{ih}}{C}\right)$
13 cmul ${class}×$
14 3 6 11 co ${class}\left({B}{\cdot }_{\mathrm{ih}}{C}\right)$
15 0 14 13 co ${class}{A}\left({B}{\cdot }_{\mathrm{ih}}{C}\right)$
16 12 15 wceq ${wff}\left({A}{\cdot }_{ℎ}{B}\right){\cdot }_{\mathrm{ih}}{C}={A}\left({B}{\cdot }_{\mathrm{ih}}{C}\right)$
17 8 16 wi ${wff}\left(\left({A}\in ℂ\wedge {B}\in ℋ\wedge {C}\in ℋ\right)\to \left({A}{\cdot }_{ℎ}{B}\right){\cdot }_{\mathrm{ih}}{C}={A}\left({B}{\cdot }_{\mathrm{ih}}{C}\right)\right)$