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

Definition df-aj 30769
Description: Define the adjoint of an operator (if it exists). The domain of 𝑈adj𝑊 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 adj = (𝑢 ∈ NrmCVec, 𝑤 ∈ NrmCVec ↦ {⟨𝑡, 𝑠⟩ ∣ (𝑡:(BaseSet‘𝑢)⟶(BaseSet‘𝑤) ∧ 𝑠:(BaseSet‘𝑤)⟶(BaseSet‘𝑢) ∧ ∀𝑥 ∈ (BaseSet‘𝑢)∀𝑦 ∈ (BaseSet‘𝑤)((𝑡𝑥)(·𝑖OLD𝑤)𝑦) = (𝑥(·𝑖OLD𝑢)(𝑠𝑦)))})
Distinct variable group:   𝑡,𝑠,𝑢,𝑤,𝑥,𝑦

Detailed syntax breakdown of Definition df-aj
StepHypRef Expression
1 caj 30767 . 2 class adj
2 vu . . 3 setvar 𝑢
3 vw . . 3 setvar 𝑤
4 cnv 30603 . . 3 class NrmCVec
52cv 1539 . . . . . . 7 class 𝑢
6 cba 30605 . . . . . . 7 class BaseSet
75, 6cfv 6561 . . . . . 6 class (BaseSet‘𝑢)
83cv 1539 . . . . . . 7 class 𝑤
98, 6cfv 6561 . . . . . 6 class (BaseSet‘𝑤)
10 vt . . . . . . 7 setvar 𝑡
1110cv 1539 . . . . . 6 class 𝑡
127, 9, 11wf 6557 . . . . 5 wff 𝑡:(BaseSet‘𝑢)⟶(BaseSet‘𝑤)
13 vs . . . . . . 7 setvar 𝑠
1413cv 1539 . . . . . 6 class 𝑠
159, 7, 14wf 6557 . . . . 5 wff 𝑠:(BaseSet‘𝑤)⟶(BaseSet‘𝑢)
16 vx . . . . . . . . . . 11 setvar 𝑥
1716cv 1539 . . . . . . . . . 10 class 𝑥
1817, 11cfv 6561 . . . . . . . . 9 class (𝑡𝑥)
19 vy . . . . . . . . . 10 setvar 𝑦
2019cv 1539 . . . . . . . . 9 class 𝑦
21 cdip 30719 . . . . . . . . . 10 class ·𝑖OLD
228, 21cfv 6561 . . . . . . . . 9 class (·𝑖OLD𝑤)
2318, 20, 22co 7431 . . . . . . . 8 class ((𝑡𝑥)(·𝑖OLD𝑤)𝑦)
2420, 14cfv 6561 . . . . . . . . 9 class (𝑠𝑦)
255, 21cfv 6561 . . . . . . . . 9 class (·𝑖OLD𝑢)
2617, 24, 25co 7431 . . . . . . . 8 class (𝑥(·𝑖OLD𝑢)(𝑠𝑦))
2723, 26wceq 1540 . . . . . . 7 wff ((𝑡𝑥)(·𝑖OLD𝑤)𝑦) = (𝑥(·𝑖OLD𝑢)(𝑠𝑦))
2827, 19, 9wral 3061 . . . . . 6 wff 𝑦 ∈ (BaseSet‘𝑤)((𝑡𝑥)(·𝑖OLD𝑤)𝑦) = (𝑥(·𝑖OLD𝑢)(𝑠𝑦))
2928, 16, 7wral 3061 . . . . 5 wff 𝑥 ∈ (BaseSet‘𝑢)∀𝑦 ∈ (BaseSet‘𝑤)((𝑡𝑥)(·𝑖OLD𝑤)𝑦) = (𝑥(·𝑖OLD𝑢)(𝑠𝑦))
3012, 15, 29w3a 1087 . . . 4 wff (𝑡:(BaseSet‘𝑢)⟶(BaseSet‘𝑤) ∧ 𝑠:(BaseSet‘𝑤)⟶(BaseSet‘𝑢) ∧ ∀𝑥 ∈ (BaseSet‘𝑢)∀𝑦 ∈ (BaseSet‘𝑤)((𝑡𝑥)(·𝑖OLD𝑤)𝑦) = (𝑥(·𝑖OLD𝑢)(𝑠𝑦)))
3130, 10, 13copab 5205 . . 3 class {⟨𝑡, 𝑠⟩ ∣ (𝑡:(BaseSet‘𝑢)⟶(BaseSet‘𝑤) ∧ 𝑠:(BaseSet‘𝑤)⟶(BaseSet‘𝑢) ∧ ∀𝑥 ∈ (BaseSet‘𝑢)∀𝑦 ∈ (BaseSet‘𝑤)((𝑡𝑥)(·𝑖OLD𝑤)𝑦) = (𝑥(·𝑖OLD𝑢)(𝑠𝑦)))}
322, 3, 4, 4, 31cmpo 7433 . 2 class (𝑢 ∈ NrmCVec, 𝑤 ∈ NrmCVec ↦ {⟨𝑡, 𝑠⟩ ∣ (𝑡:(BaseSet‘𝑢)⟶(BaseSet‘𝑤) ∧ 𝑠:(BaseSet‘𝑤)⟶(BaseSet‘𝑢) ∧ ∀𝑥 ∈ (BaseSet‘𝑢)∀𝑦 ∈ (BaseSet‘𝑤)((𝑡𝑥)(·𝑖OLD𝑤)𝑦) = (𝑥(·𝑖OLD𝑢)(𝑠𝑦)))})
331, 32wceq 1540 1 wff adj = (𝑢 ∈ NrmCVec, 𝑤 ∈ NrmCVec ↦ {⟨𝑡, 𝑠⟩ ∣ (𝑡:(BaseSet‘𝑢)⟶(BaseSet‘𝑤) ∧ 𝑠:(BaseSet‘𝑤)⟶(BaseSet‘𝑢) ∧ ∀𝑥 ∈ (BaseSet‘𝑢)∀𝑦 ∈ (BaseSet‘𝑤)((𝑡𝑥)(·𝑖OLD𝑤)𝑦) = (𝑥(·𝑖OLD𝑢)(𝑠𝑦)))})
Colors of variables: wff setvar class
This definition is referenced by:  ajfval  30828
  Copyright terms: Public domain W3C validator