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

 Description: Define the adjoint of a Hilbert space operator (if it exists). The domain of 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 22493) that the adjoint exists for a bounded linear operator. (Contributed by NM, 20-Feb-2006.) (New usage is discouraged.)
Assertion
Ref Expression
Distinct variable group:   ,,,

Detailed syntax breakdown of Definition df-adjh
StepHypRef Expression
2 chil 21329 . . . . 5
3 vt . . . . . 6
43cv 1618 . . . . 5
52, 2, 4wf 4588 . . . 4
6 vu . . . . . 6
76cv 1618 . . . . 5
82, 2, 7wf 4588 . . . 4
9 vx . . . . . . . . . 10
109cv 1618 . . . . . . . . 9
1110, 4cfv 4592 . . . . . . . 8
12 vy . . . . . . . . 9
1312cv 1618 . . . . . . . 8
14 csp 21332 . . . . . . . 8
1511, 13, 14co 5710 . . . . . . 7
1613, 7cfv 4592 . . . . . . . 8
1710, 16, 14co 5710 . . . . . . 7
1815, 17wceq 1619 . . . . . 6
1918, 12, 2wral 2509 . . . . 5
2019, 9, 2wral 2509 . . . 4
215, 8, 20w3a 939 . . 3
2221, 3, 6copab 3973 . 2
231, 22wceq 1619 1
 Colors of variables: wff set class This definition is referenced by:  dfadj2  22295  adjeq  22345
 Copyright terms: Public domain W3C validator