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

Axiom ax-his3 22539
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 23306 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 8944 . . . 4  class  CC
31, 2wcel 1721 . . 3  wff  A  e.  CC
4 cB . . . 4  class  B
5 chil 22375 . . . 4  class  ~H
64, 5wcel 1721 . . 3  wff  B  e. 
~H
7 cC . . . 4  class  C
87, 5wcel 1721 . . 3  wff  C  e. 
~H
93, 6, 8w3a 936 . 2  wff  ( A  e.  CC  /\  B  e.  ~H  /\  C  e. 
~H )
10 csm 22377 . . . . 5  class  .h
111, 4, 10co 6040 . . . 4  class  ( A  .h  B )
12 csp 22378 . . . 4  class  .ih
1311, 7, 12co 6040 . . 3  class  ( ( A  .h  B ) 
.ih  C )
144, 7, 12co 6040 . . . 4  class  ( B 
.ih  C )
15 cmul 8951 . . . 4  class  x.
161, 14, 15co 6040 . . 3  class  ( A  x.  ( B  .ih  C ) )
1713, 16wceq 1649 . 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  22541  his35  22543  hiassdi  22546  his2sub  22547  hi01  22551  normlem0  22564  normlem9  22573  bcseqi  22575  polid2i  22612  ocsh  22738  h1de2i  23008  normcan  23031  eigrei  23290  eigorthi  23293  bramul  23402  lnopunilem1  23466  hmopm  23477  riesz3i  23518  cnlnadjlem2  23524  adjmul  23548  branmfn  23561  kbass2  23573  kbass5  23576  leopmuli  23589  leopnmid  23594
  Copyright terms: Public domain W3C validator