Axiom ax-his3 27941

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 28709 for why the physics definition is swapped. (Contributed by NM, 29-May-1999.) (New usage is discouraged.)

Assertion

Ref	Expression
ax-his3	|- ( ( A e. CC /\ B e. ~H /\ C e. ~H ) -> ( ( A .h B ) .ih C ) = ( A x. ( B .ih C ) ) )

Detailed syntax breakdown of Axiom ax-his3

Step	Hyp	Ref	Expression
1		cA	. . . 4 class A
2		cc 9934	. . . 4 class CC
3	1, 2	wcel 1990	. . 3 wff A e. CC
4		cB	. . . 4 class B
5		chil 27776	. . . 4 class ~H
6	4, 5	wcel 1990	. . 3 wff B e. ~H
7		cC	. . . 4 class C
8	7, 5	wcel 1990	. . 3 wff C e. ~H
9	3, 6, 8	w3a 1037	. 2 wff ( A e. CC /\ B e. ~H /\ C e. ~H )
10		csm 27778	. . . . 5 class .h
11	1, 4, 10	co 6650	. . . 4 class ( A .h B )
12		csp 27779	. . . 4 class .ih
13	11, 7, 12	co 6650	. . 3 class ( ( A .h B ) .ih C )
14	4, 7, 12	co 6650	. . . 4 class ( B .ih C )
15		cmul 9941	. . . 4 class x.
16	1, 14, 15	co 6650	. . 3 class ( A x. ( B .ih C ) )
17	13, 16	wceq 1483	. 2 wff ( ( A .h B ) .ih C ) = ( A x. ( B .ih C ) )
18	9, 17	wi 4	1 wff ( ( A e. CC /\ B e. ~H /\ C e. ~H ) -> ( ( A .h B ) .ih C ) = ( A x. ( B .ih C ) ) )

This axiom is referenced by:  his5  27943  his35  27945  hiassdi  27948  his2sub  27949  hi01  27953  normlem0  27966  normlem9  27975  bcseqi  27977  polid2i  28014  ocsh  28142  h1de2i  28412  normcan  28435  eigrei  28693  eigorthi  28696  bramul  28805  lnopunilem1  28869  hmopm  28880  riesz3i  28921  cnlnadjlem2  28927  adjmul  28951  branmfn  28964  kbass2  28976  kbass5  28979  leopmuli  28992  leopnmid  28997