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

Axiom ax-his3 21679
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 22446 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 8751 . . . 4  class  CC
31, 2wcel 1696 . . 3  wff  A  e.  CC
4 cB . . . 4  class  B
5 chil 21515 . . . 4  class  ~H
64, 5wcel 1696 . . 3  wff  B  e. 
~H
7 cC . . . 4  class  C
87, 5wcel 1696 . . 3  wff  C  e. 
~H
93, 6, 8w3a 934 . 2  wff  ( A  e.  CC  /\  B  e.  ~H  /\  C  e. 
~H )
10 csm 21517 . . . . 5  class  .h
111, 4, 10co 5874 . . . 4  class  ( A  .h  B )
12 csp 21518 . . . 4  class  .ih
1311, 7, 12co 5874 . . 3  class  ( ( A  .h  B ) 
.ih  C )
144, 7, 12co 5874 . . . 4  class  ( B 
.ih  C )
15 cmul 8758 . . . 4  class  x.
161, 14, 15co 5874 . . 3  class  ( A  x.  ( B  .ih  C ) )
1713, 16wceq 1632 . 2  wff  ( ( A  .h  B ) 
.ih  C )  =  ( A  x.  ( B  .ih  C ) )
189, 17wi 4 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  21681  his35  21683  hiassdi  21686  his2sub  21687  hi01  21691  normlem0  21704  normlem9  21713  bcseqi  21715  polid2i  21752  ocsh  21878  h1de2i  22148  normcan  22171  eigrei  22430  eigorthi  22433  bramul  22542  lnopunilem1  22606  hmopm  22617  riesz3i  22658  cnlnadjlem2  22664  adjmul  22688  branmfn  22701  kbass2  22713  kbass5  22716  leopmuli  22729  leopnmid  22734
  Copyright terms: Public domain W3C validator