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 ⟼ t s | t : BaseSet ⁡ u ⟶ BaseSet ⁡ w ∧ s : BaseSet ⁡ w ⟶ BaseSet ⁡ u ∧ ∀ x ∈ BaseSet ⁡ u ∀ y ∈ BaseSet ⁡ w t ⁡ x ⋅ 𝑖OLD ⁡ w y = x ⋅ 𝑖OLD ⁡ u s ⁡ y

Detailed syntax breakdown

Step Hyp Ref Expression
0 caj class adj
1 vu setvar u
2 cnv class NrmCVec
3 vw setvar w
4 vt setvar t
5 vs setvar s
6 4 cv setvar t
7 cba class BaseSet
8 1 cv setvar u
9 8 7 cfv class BaseSet ⁡ u
10 3 cv setvar w
11 10 7 cfv class BaseSet ⁡ w
12 9 11 6 wf wff t : BaseSet ⁡ u ⟶ BaseSet ⁡ w
13 5 cv setvar s
14 11 9 13 wf wff s : BaseSet ⁡ w ⟶ BaseSet ⁡ u
15 vx setvar x
16 vy setvar y
17 15 cv setvar x
18 17 6 cfv class t ⁡ x
19 cdip class ⋅ 𝑖OLD
20 10 19 cfv class ⋅ 𝑖OLD ⁡ w
21 16 cv setvar y
22 18 21 20 co class t ⁡ x ⋅ 𝑖OLD ⁡ w y
23 8 19 cfv class ⋅ 𝑖OLD ⁡ u
24 21 13 cfv class s ⁡ y
25 17 24 23 co class x ⋅ 𝑖OLD ⁡ u s ⁡ y
26 22 25 wceq wff t ⁡ x ⋅ 𝑖OLD ⁡ w y = x ⋅ 𝑖OLD ⁡ u s ⁡ y
27 26 16 11 wral wff ∀ y ∈ BaseSet ⁡ w t ⁡ x ⋅ 𝑖OLD ⁡ w y = x ⋅ 𝑖OLD ⁡ u s ⁡ y
28 27 15 9 wral wff ∀ x ∈ BaseSet ⁡ u ∀ y ∈ BaseSet ⁡ w t ⁡ x ⋅ 𝑖OLD ⁡ w y = x ⋅ 𝑖OLD ⁡ u s ⁡ y
29 12 14 28 w3a wff t : BaseSet ⁡ u ⟶ BaseSet ⁡ w ∧ s : BaseSet ⁡ w ⟶ BaseSet ⁡ u ∧ ∀ x ∈ BaseSet ⁡ u ∀ y ∈ BaseSet ⁡ w t ⁡ x ⋅ 𝑖OLD ⁡ w y = x ⋅ 𝑖OLD ⁡ u s ⁡ y
30 29 4 5 copab class t s | t : BaseSet ⁡ u ⟶ BaseSet ⁡ w ∧ s : BaseSet ⁡ w ⟶ BaseSet ⁡ u ∧ ∀ x ∈ BaseSet ⁡ u ∀ y ∈ BaseSet ⁡ w t ⁡ x ⋅ 𝑖OLD ⁡ w y = x ⋅ 𝑖OLD ⁡ u s ⁡ y
31 1 3 2 2 30 cmpo class u ∈ NrmCVec , w ∈ NrmCVec ⟼ t s | t : BaseSet ⁡ u ⟶ BaseSet ⁡ w ∧ s : BaseSet ⁡ w ⟶ BaseSet ⁡ u ∧ ∀ x ∈ BaseSet ⁡ u ∀ y ∈ BaseSet ⁡ w t ⁡ x ⋅ 𝑖OLD ⁡ w y = x ⋅ 𝑖OLD ⁡ u s ⁡ y
32 0 31 wceq wff adj = u ∈ NrmCVec , w ∈ NrmCVec ⟼ t s | t : BaseSet ⁡ u ⟶ BaseSet ⁡ w ∧ s : BaseSet ⁡ w ⟶ BaseSet ⁡ u ∧ ∀ x ∈ BaseSet ⁡ u ∀ y ∈ BaseSet ⁡ w t ⁡ x ⋅ 𝑖OLD ⁡ w y = x ⋅ 𝑖OLD ⁡ u s ⁡ y