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 26795
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 26793 . 2 class adj
2 vu . . 3 setvar 𝑢
3 vw . . 3 setvar 𝑤
4 cnv 26607 . . 3 class NrmCVec
52cv 1473 . . . . . . 7 class 𝑢
6 cba 26609 . . . . . . 7 class BaseSet
75, 6cfv 5790 . . . . . 6 class (BaseSet‘𝑢)
83cv 1473 . . . . . . 7 class 𝑤
98, 6cfv 5790 . . . . . 6 class (BaseSet‘𝑤)
10 vt . . . . . . 7 setvar 𝑡
1110cv 1473 . . . . . 6 class 𝑡
127, 9, 11wf 5786 . . . . 5 wff 𝑡:(BaseSet‘𝑢)⟶(BaseSet‘𝑤)
13 vs . . . . . . 7 setvar 𝑠
1413cv 1473 . . . . . 6 class 𝑠
159, 7, 14wf 5786 . . . . 5 wff 𝑠:(BaseSet‘𝑤)⟶(BaseSet‘𝑢)
16 vx . . . . . . . . . . 11 setvar 𝑥
1716cv 1473 . . . . . . . . . 10 class 𝑥
1817, 11cfv 5790 . . . . . . . . 9 class (𝑡𝑥)
19 vy . . . . . . . . . 10 setvar 𝑦
2019cv 1473 . . . . . . . . 9 class 𝑦
21 cdip 26740 . . . . . . . . . 10 class ·𝑖OLD
228, 21cfv 5790 . . . . . . . . 9 class (·𝑖OLD𝑤)
2318, 20, 22co 6527 . . . . . . . 8 class ((𝑡𝑥)(·𝑖OLD𝑤)𝑦)
2420, 14cfv 5790 . . . . . . . . 9 class (𝑠𝑦)
255, 21cfv 5790 . . . . . . . . 9 class (·𝑖OLD𝑢)
2617, 24, 25co 6527 . . . . . . . 8 class (𝑥(·𝑖OLD𝑢)(𝑠𝑦))
2723, 26wceq 1474 . . . . . . 7 wff ((𝑡𝑥)(·𝑖OLD𝑤)𝑦) = (𝑥(·𝑖OLD𝑢)(𝑠𝑦))
2827, 19, 9wral 2895 . . . . . 6 wff 𝑦 ∈ (BaseSet‘𝑤)((𝑡𝑥)(·𝑖OLD𝑤)𝑦) = (𝑥(·𝑖OLD𝑢)(𝑠𝑦))
2928, 16, 7wral 2895 . . . . 5 wff 𝑥 ∈ (BaseSet‘𝑢)∀𝑦 ∈ (BaseSet‘𝑤)((𝑡𝑥)(·𝑖OLD𝑤)𝑦) = (𝑥(·𝑖OLD𝑢)(𝑠𝑦))
3012, 15, 29w3a 1030 . . . 4 wff (𝑡:(BaseSet‘𝑢)⟶(BaseSet‘𝑤) ∧ 𝑠:(BaseSet‘𝑤)⟶(BaseSet‘𝑢) ∧ ∀𝑥 ∈ (BaseSet‘𝑢)∀𝑦 ∈ (BaseSet‘𝑤)((𝑡𝑥)(·𝑖OLD𝑤)𝑦) = (𝑥(·𝑖OLD𝑢)(𝑠𝑦)))
3130, 10, 13copab 4636 . . 3 class {⟨𝑡, 𝑠⟩ ∣ (𝑡:(BaseSet‘𝑢)⟶(BaseSet‘𝑤) ∧ 𝑠:(BaseSet‘𝑤)⟶(BaseSet‘𝑢) ∧ ∀𝑥 ∈ (BaseSet‘𝑢)∀𝑦 ∈ (BaseSet‘𝑤)((𝑡𝑥)(·𝑖OLD𝑤)𝑦) = (𝑥(·𝑖OLD𝑢)(𝑠𝑦)))}
322, 3, 4, 4, 31cmpt2 6529 . 2 class (𝑢 ∈ NrmCVec, 𝑤 ∈ NrmCVec ↦ {⟨𝑡, 𝑠⟩ ∣ (𝑡:(BaseSet‘𝑢)⟶(BaseSet‘𝑤) ∧ 𝑠:(BaseSet‘𝑤)⟶(BaseSet‘𝑢) ∧ ∀𝑥 ∈ (BaseSet‘𝑢)∀𝑦 ∈ (BaseSet‘𝑤)((𝑡𝑥)(·𝑖OLD𝑤)𝑦) = (𝑥(·𝑖OLD𝑢)(𝑠𝑦)))})
331, 32wceq 1474 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  26854
  Copyright terms: Public domain W3C validator