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

Axiom ax-his3 21493
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 22260 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 8615 . . . 4  class  CC
31, 2wcel 1621 . . 3  wff  A  e.  CC
4 cB . . . 4  class  B
5 chil 21329 . . . 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 21331 . . . . 5  class  .h
111, 4, 10co 5710 . . . 4  class  ( A  .h  B )
12 csp 21332 . . . 4  class  .ih
1311, 7, 12co 5710 . . 3  class  ( ( A  .h  B ) 
.ih  C )
144, 7, 12co 5710 . . . 4  class  ( B 
.ih  C )
15 cmul 8622 . . . 4  class  x.
161, 14, 15co 5710 . . 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  21495  his35  21497  hiassdi  21500  his2sub  21501  hi01  21505  normlem0  21518  normlem9  21527  bcseqi  21529  polid2i  21566  ocsh  21692  h1de2i  21962  normcan  21985  eigrei  22244  eigorthi  22247  bramul  22356  lnopunilem1  22420  hmopm  22431  riesz3i  22472  cnlnadjlem2  22478  adjmul  22502  branmfn  22515  kbass2  22527  kbass5  22530  leopmuli  22543  leopnmid  22548
  Copyright terms: Public domain W3C validator