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

Axiom ax-his3 21663
 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 (e.g. Equation 1.21b of [Hughes] p. 44; Definition (iii) of [ReedSimon] p. 36). See the comments in df-bra 22430 for why the physics definition is swapped. (Contributed by NM, 29-May-1999.) (New usage is discouraged.)
Assertion
Ref Expression
ax-his3

Detailed syntax breakdown of Axiom ax-his3
StepHypRef Expression
1 cA . . . 4
2 cc 8735 . . . 4
31, 2wcel 1684 . . 3
4 cB . . . 4
5 chil 21499 . . . 4
64, 5wcel 1684 . . 3
7 cC . . . 4
87, 5wcel 1684 . . 3
93, 6, 8w3a 934 . 2
10 csm 21501 . . . . 5
111, 4, 10co 5858 . . . 4
12 csp 21502 . . . 4
1311, 7, 12co 5858 . . 3
144, 7, 12co 5858 . . . 4
15 cmul 8742 . . . 4
161, 14, 15co 5858 . . 3
1713, 16wceq 1623 . 2
189, 17wi 4 1
 Colors of variables: wff set class This axiom is referenced by:  his5  21665  his35  21667  hiassdi  21670  his2sub  21671  hi01  21675  normlem0  21688  normlem9  21697  bcseqi  21699  polid2i  21736  ocsh  21862  h1de2i  22132  normcan  22155  eigrei  22414  eigorthi  22417  bramul  22526  lnopunilem1  22590  hmopm  22601  riesz3i  22642  cnlnadjlem2  22648  adjmul  22672  branmfn  22685  kbass2  22697  kbass5  22700  leopmuli  22713  leopnmid  22718
 Copyright terms: Public domain W3C validator