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

Axiom ax-his3 22588
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 23355 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 8990 . . . 4  class  CC
31, 2wcel 1726 . . 3  wff  A  e.  CC
4 cB . . . 4  class  B
5 chil 22424 . . . 4  class  ~H
64, 5wcel 1726 . . 3  wff  B  e. 
~H
7 cC . . . 4  class  C
87, 5wcel 1726 . . 3  wff  C  e. 
~H
93, 6, 8w3a 937 . 2  wff  ( A  e.  CC  /\  B  e.  ~H  /\  C  e. 
~H )
10 csm 22426 . . . . 5  class  .h
111, 4, 10co 6083 . . . 4  class  ( A  .h  B )
12 csp 22427 . . . 4  class  .ih
1311, 7, 12co 6083 . . 3  class  ( ( A  .h  B ) 
.ih  C )
144, 7, 12co 6083 . . . 4  class  ( B 
.ih  C )
15 cmul 8997 . . . 4  class  x.
161, 14, 15co 6083 . . 3  class  ( A  x.  ( B  .ih  C ) )
1713, 16wceq 1653 . 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  22590  his35  22592  hiassdi  22595  his2sub  22596  hi01  22600  normlem0  22613  normlem9  22622  bcseqi  22624  polid2i  22661  ocsh  22787  h1de2i  23057  normcan  23080  eigrei  23339  eigorthi  23342  bramul  23451  lnopunilem1  23515  hmopm  23526  riesz3i  23567  cnlnadjlem2  23573  adjmul  23597  branmfn  23610  kbass2  23622  kbass5  23625  leopmuli  23638  leopnmid  23643
  Copyright terms: Public domain W3C validator