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

Axiom ax-his3 21609
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 22376 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 8689 . . . 4  class  CC
31, 2wcel 1621 . . 3  wff  A  e.  CC
4 cB . . . 4  class  B
5 chil 21445 . . . 4  class  ~H
64, 5wcel 1621 . . 3  wff  B  e. 
~H
7 cC . . . 4  class  C
87, 5wcel 1621 . . 3  wff  C  e. 
~H
93, 6, 8w3a 939 . 2  wff  ( A  e.  CC  /\  B  e.  ~H  /\  C  e. 
~H )
10 csm 21447 . . . . 5  class  .h
111, 4, 10co 5778 . . . 4  class  ( A  .h  B )
12 csp 21448 . . . 4  class  .ih
1311, 7, 12co 5778 . . 3  class  ( ( A  .h  B ) 
.ih  C )
144, 7, 12co 5778 . . . 4  class  ( B 
.ih  C )
15 cmul 8696 . . . 4  class  x.
161, 14, 15co 5778 . . 3  class  ( A  x.  ( B  .ih  C ) )
1713, 16wceq 1619 . 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  21611  his35  21613  hiassdi  21616  his2sub  21617  hi01  21621  normlem0  21634  normlem9  21643  bcseqi  21645  polid2i  21682  ocsh  21808  h1de2i  22078  normcan  22101  eigrei  22360  eigorthi  22363  bramul  22472  lnopunilem1  22536  hmopm  22547  riesz3i  22588  cnlnadjlem2  22594  adjmul  22618  branmfn  22631  kbass2  22643  kbass5  22646  leopmuli  22659  leopnmid  22664
  Copyright terms: Public domain W3C validator