This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ) ) )