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 ⊢ adj h = t u | t : ℋ ⟶ ℋ ∧ u : ℋ ⟶ ℋ ∧ ∀ x ∈ ℋ ∀ y ∈ ℋ t ⁡ x ⋅ ih y = x ⋅ ih u ⁡ y

Detailed syntax breakdown

Step Hyp Ref Expression
0 cado class adj h
1 vt setvar t
2 vu setvar u
3 1 cv setvar t
4 chba class ℋ
5 4 4 3 wf wff t : ℋ ⟶ ℋ
6 2 cv setvar u
7 4 4 6 wf wff u : ℋ ⟶ ℋ
8 vx setvar x
9 vy setvar y
10 8 cv setvar x
11 10 3 cfv class t ⁡ x
12 csp class ⋅ ih
13 9 cv setvar y
14 11 13 12 co class t ⁡ x ⋅ ih y
15 13 6 cfv class u ⁡ y
16 10 15 12 co class x ⋅ ih u ⁡ y
17 14 16 wceq wff t ⁡ x ⋅ ih y = x ⋅ ih u ⁡ y
18 17 9 4 wral wff ∀ y ∈ ℋ t ⁡ x ⋅ ih y = x ⋅ ih u ⁡ y
19 18 8 4 wral wff ∀ x ∈ ℋ ∀ y ∈ ℋ t ⁡ x ⋅ ih y = x ⋅ ih u ⁡ y
20 5 7 19 w3a wff t : ℋ ⟶ ℋ ∧ u : ℋ ⟶ ℋ ∧ ∀ x ∈ ℋ ∀ y ∈ ℋ t ⁡ x ⋅ ih y = x ⋅ ih u ⁡ y
21 20 1 2 copab class t u | t : ℋ ⟶ ℋ ∧ u : ℋ ⟶ ℋ ∧ ∀ x ∈ ℋ ∀ y ∈ ℋ t ⁡ x ⋅ ih y = x ⋅ ih u ⁡ y
22 0 21 wceq wff adj h = t u | t : ℋ ⟶ ℋ ∧ u : ℋ ⟶ ℋ ∧ ∀ x ∈ ℋ ∀ y ∈ ℋ t ⁡ x ⋅ ih y = x ⋅ ih u ⁡ y