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

Definition df-adjh 30620
Description: Define the adjoint of a Hilbert space operator (if it exists). The domain of adjโ„Ž is the set of all adjoint operators. Definition of adjoint in [Kalmbach2] p. 8. Unlike Kalmbach (and most authors), we do not demand that the operator be linear, but instead show (in adjbdln 30854) that the adjoint exists for a bounded linear operator. (Contributed by NM, 20-Feb-2006.) (New usage is discouraged.)
Assertion
Ref Expression
df-adjh adjโ„Ž = {โŸจ๐‘ก, ๐‘ขโŸฉ โˆฃ (๐‘ก: โ„‹โŸถ โ„‹ โˆง ๐‘ข: โ„‹โŸถ โ„‹ โˆง โˆ€๐‘ฅ โˆˆ โ„‹ โˆ€๐‘ฆ โˆˆ โ„‹ ((๐‘กโ€˜๐‘ฅ) ยทih ๐‘ฆ) = (๐‘ฅ ยทih (๐‘ขโ€˜๐‘ฆ)))}
Distinct variable group:   ๐‘ข,๐‘ก,๐‘ฅ,๐‘ฆ

Detailed syntax breakdown of Definition df-adjh
StepHypRef Expression
1 cado 29726 . 2 class adjโ„Ž
2 chba 29690 . . . . 5 class โ„‹
3 vt . . . . . 6 setvar ๐‘ก
43cv 1540 . . . . 5 class ๐‘ก
52, 2, 4wf 6489 . . . 4 wff ๐‘ก: โ„‹โŸถ โ„‹
6 vu . . . . . 6 setvar ๐‘ข
76cv 1540 . . . . 5 class ๐‘ข
82, 2, 7wf 6489 . . . 4 wff ๐‘ข: โ„‹โŸถ โ„‹
9 vx . . . . . . . . . 10 setvar ๐‘ฅ
109cv 1540 . . . . . . . . 9 class ๐‘ฅ
1110, 4cfv 6493 . . . . . . . 8 class (๐‘กโ€˜๐‘ฅ)
12 vy . . . . . . . . 9 setvar ๐‘ฆ
1312cv 1540 . . . . . . . 8 class ๐‘ฆ
14 csp 29693 . . . . . . . 8 class ยทih
1511, 13, 14co 7351 . . . . . . 7 class ((๐‘กโ€˜๐‘ฅ) ยทih ๐‘ฆ)
1613, 7cfv 6493 . . . . . . . 8 class (๐‘ขโ€˜๐‘ฆ)
1710, 16, 14co 7351 . . . . . . 7 class (๐‘ฅ ยทih (๐‘ขโ€˜๐‘ฆ))
1815, 17wceq 1541 . . . . . 6 wff ((๐‘กโ€˜๐‘ฅ) ยทih ๐‘ฆ) = (๐‘ฅ ยทih (๐‘ขโ€˜๐‘ฆ))
1918, 12, 2wral 3062 . . . . 5 wff โˆ€๐‘ฆ โˆˆ โ„‹ ((๐‘กโ€˜๐‘ฅ) ยทih ๐‘ฆ) = (๐‘ฅ ยทih (๐‘ขโ€˜๐‘ฆ))
2019, 9, 2wral 3062 . . . 4 wff โˆ€๐‘ฅ โˆˆ โ„‹ โˆ€๐‘ฆ โˆˆ โ„‹ ((๐‘กโ€˜๐‘ฅ) ยทih ๐‘ฆ) = (๐‘ฅ ยทih (๐‘ขโ€˜๐‘ฆ))
215, 8, 20w3a 1087 . . 3 wff (๐‘ก: โ„‹โŸถ โ„‹ โˆง ๐‘ข: โ„‹โŸถ โ„‹ โˆง โˆ€๐‘ฅ โˆˆ โ„‹ โˆ€๐‘ฆ โˆˆ โ„‹ ((๐‘กโ€˜๐‘ฅ) ยทih ๐‘ฆ) = (๐‘ฅ ยทih (๐‘ขโ€˜๐‘ฆ)))
2221, 3, 6copab 5165 . 2 class {โŸจ๐‘ก, ๐‘ขโŸฉ โˆฃ (๐‘ก: โ„‹โŸถ โ„‹ โˆง ๐‘ข: โ„‹โŸถ โ„‹ โˆง โˆ€๐‘ฅ โˆˆ โ„‹ โˆ€๐‘ฆ โˆˆ โ„‹ ((๐‘กโ€˜๐‘ฅ) ยทih ๐‘ฆ) = (๐‘ฅ ยทih (๐‘ขโ€˜๐‘ฆ)))}
231, 22wceq 1541 1 wff adjโ„Ž = {โŸจ๐‘ก, ๐‘ขโŸฉ โˆฃ (๐‘ก: โ„‹โŸถ โ„‹ โˆง ๐‘ข: โ„‹โŸถ โ„‹ โˆง โˆ€๐‘ฅ โˆˆ โ„‹ โˆ€๐‘ฆ โˆˆ โ„‹ ((๐‘กโ€˜๐‘ฅ) ยทih ๐‘ฆ) = (๐‘ฅ ยทih (๐‘ขโ€˜๐‘ฆ)))}
Colors of variables: wff setvar class
This definition is referenced by:  dfadj2  30656  adjeq  30706
  Copyright terms: Public domain W3C validator