Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-aj Unicode version

Definition df-aj 21158
 Description: Define the adjoint of an operator (if it exists). The domain of is the set of all operators from to that have an adjoint. Definition 3.9-1 of [Kreyszig] p. 196, although we don't require that and be Hilbert spaces nor that the operators be linear. Although we define it for any normed vector space for convenience, the definition is meaningful only for inner product spaces. (Contributed by NM, 25-Jan-2008.) (New usage is discouraged.)
Assertion
Ref Expression
df-aj
Distinct variable group:   ,,,,,

Detailed syntax breakdown of Definition df-aj
StepHypRef Expression
1 caj 21156 . 2
2 vu . . 3
3 vw . . 3
4 cnv 20970 . . 3
52cv 1618 . . . . . . 7
6 cba 20972 . . . . . . 7
75, 6cfv 4592 . . . . . 6
83cv 1618 . . . . . . 7
98, 6cfv 4592 . . . . . 6
10 vt . . . . . . 7
1110cv 1618 . . . . . 6
127, 9, 11wf 4588 . . . . 5
13 vs . . . . . . 7
1413cv 1618 . . . . . 6
159, 7, 14wf 4588 . . . . 5
16 vx . . . . . . . . . . 11
1716cv 1618 . . . . . . . . . 10
1817, 11cfv 4592 . . . . . . . . 9
19 vy . . . . . . . . . 10
2019cv 1618 . . . . . . . . 9
21 cdip 21103 . . . . . . . . . 10
228, 21cfv 4592 . . . . . . . . 9
2318, 20, 22co 5710 . . . . . . . 8
2420, 14cfv 4592 . . . . . . . . 9
255, 21cfv 4592 . . . . . . . . 9
2617, 24, 25co 5710 . . . . . . . 8
2723, 26wceq 1619 . . . . . . 7
2827, 19, 9wral 2509 . . . . . 6
2928, 16, 7wral 2509 . . . . 5
3012, 15, 29w3a 939 . . . 4
3130, 10, 13copab 3973 . . 3
322, 3, 4, 4, 31cmpt2 5712 . 2
331, 32wceq 1619 1
 Colors of variables: wff set class This definition is referenced by:  ajfval  21217
 Copyright terms: Public domain W3C validator