Metamath Proof Explorer

Definition df-aj

Description: Define the adjoint of an operator (if it exists). The domain of U adj W is the set of all operators from U to W that have an adjoint. Definition 3.9-1 of Kreyszig p. 196, although we don't require that U and W 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.)

Ref Expression
Assertion df-aj ⊢adj=u∈NrmCVec,w∈NrmCVec⟼ts|t:BaseSet⁡u⟶BaseSet⁡w∧s:BaseSet⁡w⟶BaseSet⁡u∧∀x∈BaseSet⁡u∀y∈BaseSet⁡wt⁡x⋅𝑖OLD⁡wy=x⋅𝑖OLD⁡us⁡y

Detailed syntax breakdown

Step Hyp Ref Expression
0 caj classadj
1 vu setvaru
2 cnv classNrmCVec
3 vw setvarw
4 vt setvart
5 vs setvars
6 4 cv setvart
7 cba classBaseSet
8 1 cv setvaru
9 8 7 cfv classBaseSet⁡u
10 3 cv setvarw
11 10 7 cfv classBaseSet⁡w
12 9 11 6 wf wfft:BaseSet⁡u⟶BaseSet⁡w
13 5 cv setvars
14 11 9 13 wf wffs:BaseSet⁡w⟶BaseSet⁡u
15 vx setvarx
16 vy setvary
17 15 cv setvarx
18 17 6 cfv classt⁡x
19 cdip class⋅𝑖OLD
20 10 19 cfv class⋅𝑖OLD⁡w
21 16 cv setvary
22 18 21 20 co classt⁡x⋅𝑖OLD⁡wy
23 8 19 cfv class⋅𝑖OLD⁡u
24 21 13 cfv classs⁡y
25 17 24 23 co classx⋅𝑖OLD⁡us⁡y
26 22 25 wceq wfft⁡x⋅𝑖OLD⁡wy=x⋅𝑖OLD⁡us⁡y
27 26 16 11 wral wff∀y∈BaseSet⁡wt⁡x⋅𝑖OLD⁡wy=x⋅𝑖OLD⁡us⁡y
28 27 15 9 wral wff∀x∈BaseSet⁡u∀y∈BaseSet⁡wt⁡x⋅𝑖OLD⁡wy=x⋅𝑖OLD⁡us⁡y
29 12 14 28 w3a wfft:BaseSet⁡u⟶BaseSet⁡w∧s:BaseSet⁡w⟶BaseSet⁡u∧∀x∈BaseSet⁡u∀y∈BaseSet⁡wt⁡x⋅𝑖OLD⁡wy=x⋅𝑖OLD⁡us⁡y
30 29 4 5 copab classts|t:BaseSet⁡u⟶BaseSet⁡w∧s:BaseSet⁡w⟶BaseSet⁡u∧∀x∈BaseSet⁡u∀y∈BaseSet⁡wt⁡x⋅𝑖OLD⁡wy=x⋅𝑖OLD⁡us⁡y
31 1 3 2 2 30 cmpo classu∈NrmCVec,w∈NrmCVec⟼ts|t:BaseSet⁡u⟶BaseSet⁡w∧s:BaseSet⁡w⟶BaseSet⁡u∧∀x∈BaseSet⁡u∀y∈BaseSet⁡wt⁡x⋅𝑖OLD⁡wy=x⋅𝑖OLD⁡us⁡y
32 0 31 wceq wffadj=u∈NrmCVec,w∈NrmCVec⟼ts|t:BaseSet⁡u⟶BaseSet⁡w∧s:BaseSet⁡w⟶BaseSet⁡u∧∀x∈BaseSet⁡u∀y∈BaseSet⁡wt⁡x⋅𝑖OLD⁡wy=x⋅𝑖OLD⁡us⁡y