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

Definition df-aj 22243
 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 22241 . 2
2 vu . . 3
3 vw . . 3
4 cnv 22055 . . 3
52cv 1651 . . . . . . 7
6 cba 22057 . . . . . . 7
75, 6cfv 5446 . . . . . 6
83cv 1651 . . . . . . 7
98, 6cfv 5446 . . . . . 6
10 vt . . . . . . 7
1110cv 1651 . . . . . 6
127, 9, 11wf 5442 . . . . 5
13 vs . . . . . . 7
1413cv 1651 . . . . . 6
159, 7, 14wf 5442 . . . . 5
16 vx . . . . . . . . . . 11
1716cv 1651 . . . . . . . . . 10
1817, 11cfv 5446 . . . . . . . . 9
19 vy . . . . . . . . . 10
2019cv 1651 . . . . . . . . 9
21 cdip 22188 . . . . . . . . . 10
228, 21cfv 5446 . . . . . . . . 9
2318, 20, 22co 6073 . . . . . . . 8
2420, 14cfv 5446 . . . . . . . . 9
255, 21cfv 5446 . . . . . . . . 9
2617, 24, 25co 6073 . . . . . . . 8
2723, 26wceq 1652 . . . . . . 7
2827, 19, 9wral 2697 . . . . . 6
2928, 16, 7wral 2697 . . . . 5
3012, 15, 29w3a 936 . . . 4
3130, 10, 13copab 4257 . . 3
322, 3, 4, 4, 31cmpt2 6075 . 2
331, 32wceq 1652 1
 Colors of variables: wff set class This definition is referenced by:  ajfval  22302
 Copyright terms: Public domain W3C validator