Metamath Proof Explorer

Definition df-adjh

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

Ref Expression
Assertion df-adjh ⊢adjh=tu|t:ℋ⟶ℋ∧u:ℋ⟶ℋ∧∀x∈ℋ∀y∈ℋt⁡x⋅ihy=x⋅ihu⁡y

Detailed syntax breakdown

Step Hyp Ref Expression
0 cado classadjh
1 vt setvart
2 vu setvaru
3 1 cv setvart
4 chba classℋ
5 4 4 3 wf wfft:ℋ⟶ℋ
6 2 cv setvaru
7 4 4 6 wf wffu:ℋ⟶ℋ
8 vx setvarx
9 vy setvary
10 8 cv setvarx
11 10 3 cfv classt⁡x
12 csp class⋅ih
13 9 cv setvary
14 11 13 12 co classt⁡x⋅ihy
15 13 6 cfv classu⁡y
16 10 15 12 co classx⋅ihu⁡y
17 14 16 wceq wfft⁡x⋅ihy=x⋅ihu⁡y
18 17 9 4 wral wff∀y∈ℋt⁡x⋅ihy=x⋅ihu⁡y
19 18 8 4 wral wff∀x∈ℋ∀y∈ℋt⁡x⋅ihy=x⋅ihu⁡y
20 5 7 19 w3a wfft:ℋ⟶ℋ∧u:ℋ⟶ℋ∧∀x∈ℋ∀y∈ℋt⁡x⋅ihy=x⋅ihu⁡y
21 20 1 2 copab classtu|t:ℋ⟶ℋ∧u:ℋ⟶ℋ∧∀x∈ℋ∀y∈ℋt⁡x⋅ihy=x⋅ihu⁡y
22 0 21 wceq wffadjh=tu|t:ℋ⟶ℋ∧u:ℋ⟶ℋ∧∀x∈ℋ∀y∈ℋt⁡x⋅ihy=x⋅ihu⁡y