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 ABCABihC=ABihC

Detailed syntax breakdown

Step Hyp Ref Expression
0 cA classA
1 cc class
2 0 1 wcel wffA
3 cB classB
4 chba class
5 3 4 wcel wffB
6 cC classC
7 6 4 wcel wffC
8 2 5 7 w3a wffABC
9 csm class
10 0 3 9 co classAB
11 csp classih
12 10 6 11 co classABihC
13 cmul class×
14 3 6 11 co classBihC
15 0 14 13 co classABihC
16 12 15 wceq wffABihC=ABihC
17 8 16 wi wffABCABihC=ABihC