# 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
`|- ( ( A e. CC /\ B e. ~H /\ C e. ~H ) -> ( ( A .h B ) .ih C ) = ( A x. ( B .ih C ) ) )`

### Detailed syntax breakdown

Step Hyp Ref Expression
0 cA
` |-  A`
1 cc
` |-  CC`
2 0 1 wcel
` |-  A e. CC`
3 cB
` |-  B`
4 chba
` |-  ~H`
5 3 4 wcel
` |-  B e. ~H`
6 cC
` |-  C`
7 6 4 wcel
` |-  C e. ~H`
8 2 5 7 w3a
` |-  ( A e. CC /\ B e. ~H /\ C e. ~H )`
9 csm
` |-  .h`
10 0 3 9 co
` |-  ( A .h B )`
11 csp
` |-  .ih`
12 10 6 11 co
` |-  ( ( A .h B ) .ih C )`
13 cmul
` |-  x.`
14 3 6 11 co
` |-  ( B .ih C )`
15 0 14 13 co
` |-  ( A x. ( B .ih C ) )`
16 12 15 wceq
` |-  ( ( A .h B ) .ih C ) = ( A x. ( B .ih C ) )`
17 8 16 wi
` |-  ( ( A e. CC /\ B e. ~H /\ C e. ~H ) -> ( ( A .h B ) .ih C ) = ( A x. ( B .ih C ) ) )`