HSE Home Hilbert Space Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  HSE Home  >  Th. List  >  ax-his3 Unicode version

Axiom ax-his3 21655
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 22422 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
StepHypRef Expression
1 cA . . . 4  class  A
2 cc 8730 . . . 4  class  CC
31, 2wcel 1688 . . 3  wff  A  e.  CC
4 cB . . . 4  class  B
5 chil 21491 . . . 4  class  ~H
64, 5wcel 1688 . . 3  wff  B  e. 
~H
7 cC . . . 4  class  C
87, 5wcel 1688 . . 3  wff  C  e. 
~H
93, 6, 8w3a 939 . 2  wff  ( A  e.  CC  /\  B  e.  ~H  /\  C  e. 
~H )
10 csm 21493 . . . . 5  class  .h
111, 4, 10co 5819 . . . 4  class  ( A  .h  B )
12 csp 21494 . . . 4  class  .ih
1311, 7, 12co 5819 . . 3  class  ( ( A  .h  B ) 
.ih  C )
144, 7, 12co 5819 . . . 4  class  ( B 
.ih  C )
15 cmul 8737 . . . 4  class  x.
161, 14, 15co 5819 . . 3  class  ( A  x.  ( B  .ih  C ) )
1713, 16wceq 1628 . 2  wff  ( ( A  .h  B ) 
.ih  C )  =  ( A  x.  ( B  .ih  C ) )
189, 17wi 6 1  wff  ( ( A  e.  CC  /\  B  e.  ~H  /\  C  e.  ~H )  ->  (
( A  .h  B
)  .ih  C )  =  ( A  x.  ( B  .ih  C ) ) )
Colors of variables: wff set class
This axiom is referenced by:  his5  21657  his35  21659  hiassdi  21662  his2sub  21663  hi01  21667  normlem0  21680  normlem9  21689  bcseqi  21691  polid2i  21728  ocsh  21854  h1de2i  22124  normcan  22147  eigrei  22406  eigorthi  22409  bramul  22518  lnopunilem1  22582  hmopm  22593  riesz3i  22634  cnlnadjlem2  22640  adjmul  22664  branmfn  22677  kbass2  22689  kbass5  22692  leopmuli  22705  leopnmid  22710
  Copyright terms: Public domain W3C validator