HSE Home Hilbert Space Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  HSE Home  >  Th. List  >  ax-his1 Structured version   Visualization version   GIF version

Axiom ax-his1 30839
Description: Conjugate law for inner product. Postulate (S1) of [Beran] p. 95. Note that โˆ—โ€˜๐‘ฅ is the complex conjugate cjval 15052 of ๐‘ฅ. In the literature, the inner product of ๐ด and ๐ต is usually written โŸจ๐ด, ๐ตโŸฉ, but our operation notation co 7404 allows to use existing theorems about operations and also avoids a clash with the definition of an ordered pair df-op 4630. Physicists use โŸจ๐ต โˆฃ ๐ดโŸฉ, called Dirac bra-ket notation, to represent this operation; see comments in df-bra 31607. (Contributed by NM, 29-Jul-1999.) (New usage is discouraged.)
Assertion
Ref Expression
ax-his1 ((๐ด โˆˆ โ„‹ โˆง ๐ต โˆˆ โ„‹) โ†’ (๐ด ยทih ๐ต) = (โˆ—โ€˜(๐ต ยทih ๐ด)))

Detailed syntax breakdown of Axiom ax-his1
StepHypRef Expression
1 cA . . . 4 class ๐ด
2 chba 30676 . . . 4 class โ„‹
31, 2wcel 2098 . . 3 wff ๐ด โˆˆ โ„‹
4 cB . . . 4 class ๐ต
54, 2wcel 2098 . . 3 wff ๐ต โˆˆ โ„‹
63, 5wa 395 . 2 wff (๐ด โˆˆ โ„‹ โˆง ๐ต โˆˆ โ„‹)
7 csp 30679 . . . 4 class ยทih
81, 4, 7co 7404 . . 3 class (๐ด ยทih ๐ต)
94, 1, 7co 7404 . . . 4 class (๐ต ยทih ๐ด)
10 ccj 15046 . . . 4 class โˆ—
119, 10cfv 6536 . . 3 class (โˆ—โ€˜(๐ต ยทih ๐ด))
128, 11wceq 1533 . 2 wff (๐ด ยทih ๐ต) = (โˆ—โ€˜(๐ต ยทih ๐ด))
136, 12wi 4 1 wff ((๐ด โˆˆ โ„‹ โˆง ๐ต โˆˆ โ„‹) โ†’ (๐ด ยทih ๐ต) = (โˆ—โ€˜(๐ต ยทih ๐ด)))
Colors of variables: wff setvar class
This axiom is referenced by:  his5  30843  his7  30847  his2sub2  30850  hire  30851  hi02  30854  his1i  30857  abshicom  30858  hial2eq2  30864  orthcom  30865  adjsym  31590  cnvadj  31649  adj2  31691
  Copyright terms: Public domain W3C validator