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

Definition df-hmop 30615
Description: Define the set of Hermitian operators on Hilbert space. Some books call these "symmetric operators" and others call them "self-adjoint operators", sometimes with slightly different technical meanings. (Contributed by NM, 18-Jan-2006.) (New usage is discouraged.)
Assertion
Ref Expression
df-hmop HrmOp = {๐‘ก โˆˆ ( โ„‹ โ†‘m โ„‹) โˆฃ โˆ€๐‘ฅ โˆˆ โ„‹ โˆ€๐‘ฆ โˆˆ โ„‹ (๐‘ฅ ยทih (๐‘กโ€˜๐‘ฆ)) = ((๐‘กโ€˜๐‘ฅ) ยทih ๐‘ฆ)}
Distinct variable group:   ๐‘ฅ,๐‘ก,๐‘ฆ

Detailed syntax breakdown of Definition df-hmop
StepHypRef Expression
1 cho 29721 . 2 class HrmOp
2 vx . . . . . . . 8 setvar ๐‘ฅ
32cv 1540 . . . . . . 7 class ๐‘ฅ
4 vy . . . . . . . . 9 setvar ๐‘ฆ
54cv 1540 . . . . . . . 8 class ๐‘ฆ
6 vt . . . . . . . . 9 setvar ๐‘ก
76cv 1540 . . . . . . . 8 class ๐‘ก
85, 7cfv 6493 . . . . . . 7 class (๐‘กโ€˜๐‘ฆ)
9 csp 29693 . . . . . . 7 class ยทih
103, 8, 9co 7351 . . . . . 6 class (๐‘ฅ ยทih (๐‘กโ€˜๐‘ฆ))
113, 7cfv 6493 . . . . . . 7 class (๐‘กโ€˜๐‘ฅ)
1211, 5, 9co 7351 . . . . . 6 class ((๐‘กโ€˜๐‘ฅ) ยทih ๐‘ฆ)
1310, 12wceq 1541 . . . . 5 wff (๐‘ฅ ยทih (๐‘กโ€˜๐‘ฆ)) = ((๐‘กโ€˜๐‘ฅ) ยทih ๐‘ฆ)
14 chba 29690 . . . . 5 class โ„‹
1513, 4, 14wral 3062 . . . 4 wff โˆ€๐‘ฆ โˆˆ โ„‹ (๐‘ฅ ยทih (๐‘กโ€˜๐‘ฆ)) = ((๐‘กโ€˜๐‘ฅ) ยทih ๐‘ฆ)
1615, 2, 14wral 3062 . . 3 wff โˆ€๐‘ฅ โˆˆ โ„‹ โˆ€๐‘ฆ โˆˆ โ„‹ (๐‘ฅ ยทih (๐‘กโ€˜๐‘ฆ)) = ((๐‘กโ€˜๐‘ฅ) ยทih ๐‘ฆ)
17 cmap 8723 . . . 4 class โ†‘m
1814, 14, 17co 7351 . . 3 class ( โ„‹ โ†‘m โ„‹)
1916, 6, 18crab 3405 . 2 class {๐‘ก โˆˆ ( โ„‹ โ†‘m โ„‹) โˆฃ โˆ€๐‘ฅ โˆˆ โ„‹ โˆ€๐‘ฆ โˆˆ โ„‹ (๐‘ฅ ยทih (๐‘กโ€˜๐‘ฆ)) = ((๐‘กโ€˜๐‘ฅ) ยทih ๐‘ฆ)}
201, 19wceq 1541 1 wff HrmOp = {๐‘ก โˆˆ ( โ„‹ โ†‘m โ„‹) โˆฃ โˆ€๐‘ฅ โˆˆ โ„‹ โˆ€๐‘ฆ โˆˆ โ„‹ (๐‘ฅ ยทih (๐‘กโ€˜๐‘ฆ)) = ((๐‘กโ€˜๐‘ฅ) ยทih ๐‘ฆ)}
Colors of variables: wff setvar class
This definition is referenced by:  elhmop  30644
  Copyright terms: Public domain W3C validator