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