Definition df-aj 29998

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

Step	Hyp	Ref	Expression
1		caj 29996	. 2 class adj
2		vu	. . 3 setvar 𝑢
3		vw	. . 3 setvar 𝑤
4		cnv 29832	. . 3 class NrmCVec
5	2	cv 1540	. . . . . . 7 class 𝑢
6		cba 29834	. . . . . . 7 class BaseSet
7	5, 6	cfv 6543	. . . . . 6 class (BaseSet‘𝑢)
8	3	cv 1540	. . . . . . 7 class 𝑤
9	8, 6	cfv 6543	. . . . . 6 class (BaseSet‘𝑤)
10		vt	. . . . . . 7 setvar 𝑡
11	10	cv 1540	. . . . . 6 class 𝑡
12	7, 9, 11	wf 6539	. . . . 5 wff 𝑡:(BaseSet‘𝑢)⟶(BaseSet‘𝑤)
13		vs	. . . . . . 7 setvar 𝑠
14	13	cv 1540	. . . . . 6 class 𝑠
15	9, 7, 14	wf 6539	. . . . 5 wff 𝑠:(BaseSet‘𝑤)⟶(BaseSet‘𝑢)
16		vx	. . . . . . . . . . 11 setvar 𝑥
17	16	cv 1540	. . . . . . . . . 10 class 𝑥
18	17, 11	cfv 6543	. . . . . . . . 9 class (𝑡‘𝑥)
19		vy	. . . . . . . . . 10 setvar 𝑦
20	19	cv 1540	. . . . . . . . 9 class 𝑦
21		cdip 29948	. . . . . . . . . 10 class ·𝑖OLD
22	8, 21	cfv 6543	. . . . . . . . 9 class (·𝑖OLD‘𝑤)
23	18, 20, 22	co 7408	. . . . . . . 8 class ((𝑡‘𝑥)(·𝑖OLD‘𝑤)𝑦)
24	20, 14	cfv 6543	. . . . . . . . 9 class (𝑠‘𝑦)
25	5, 21	cfv 6543	. . . . . . . . 9 class (·𝑖OLD‘𝑢)
26	17, 24, 25	co 7408	. . . . . . . 8 class (𝑥(·𝑖OLD‘𝑢)(𝑠‘𝑦))
27	23, 26	wceq 1541	. . . . . . 7 wff ((𝑡‘𝑥)(·𝑖OLD‘𝑤)𝑦) = (𝑥(·𝑖OLD‘𝑢)(𝑠‘𝑦))
28	27, 19, 9	wral 3061	. . . . . 6 wff ∀𝑦 ∈ (BaseSet‘𝑤)((𝑡‘𝑥)(·𝑖OLD‘𝑤)𝑦) = (𝑥(·𝑖OLD‘𝑢)(𝑠‘𝑦))
29	28, 16, 7	wral 3061	. . . . 5 wff ∀𝑥 ∈ (BaseSet‘𝑢)∀𝑦 ∈ (BaseSet‘𝑤)((𝑡‘𝑥)(·𝑖OLD‘𝑤)𝑦) = (𝑥(·𝑖OLD‘𝑢)(𝑠‘𝑦))
30	12, 15, 29	w3a 1087	. . . 4 wff (𝑡:(BaseSet‘𝑢)⟶(BaseSet‘𝑤) ∧ 𝑠:(BaseSet‘𝑤)⟶(BaseSet‘𝑢) ∧ ∀𝑥 ∈ (BaseSet‘𝑢)∀𝑦 ∈ (BaseSet‘𝑤)((𝑡‘𝑥)(·𝑖OLD‘𝑤)𝑦) = (𝑥(·𝑖OLD‘𝑢)(𝑠‘𝑦)))
31	30, 10, 13	copab 5210	. . 3 class {⟨𝑡, 𝑠⟩ ∣ (𝑡:(BaseSet‘𝑢)⟶(BaseSet‘𝑤) ∧ 𝑠:(BaseSet‘𝑤)⟶(BaseSet‘𝑢) ∧ ∀𝑥 ∈ (BaseSet‘𝑢)∀𝑦 ∈ (BaseSet‘𝑤)((𝑡‘𝑥)(·𝑖OLD‘𝑤)𝑦) = (𝑥(·𝑖OLD‘𝑢)(𝑠‘𝑦)))}
32	2, 3, 4, 4, 31	cmpo 7410	. 2 class (𝑢 ∈ NrmCVec, 𝑤 ∈ NrmCVec ↦ {⟨𝑡, 𝑠⟩ ∣ (𝑡:(BaseSet‘𝑢)⟶(BaseSet‘𝑤) ∧ 𝑠:(BaseSet‘𝑤)⟶(BaseSet‘𝑢) ∧ ∀𝑥 ∈ (BaseSet‘𝑢)∀𝑦 ∈ (BaseSet‘𝑤)((𝑡‘𝑥)(·𝑖OLD‘𝑤)𝑦) = (𝑥(·𝑖OLD‘𝑢)(𝑠‘𝑦)))})
33	1, 32	wceq 1541	1 wff adj = (𝑢 ∈ NrmCVec, 𝑤 ∈ NrmCVec ↦ {⟨𝑡, 𝑠⟩ ∣ (𝑡:(BaseSet‘𝑢)⟶(BaseSet‘𝑤) ∧ 𝑠:(BaseSet‘𝑤)⟶(BaseSet‘𝑢) ∧ ∀𝑥 ∈ (BaseSet‘𝑢)∀𝑦 ∈ (BaseSet‘𝑤)((𝑡‘𝑥)(·𝑖OLD‘𝑤)𝑦) = (𝑥(·𝑖OLD‘𝑢)(𝑠‘𝑦)))})

This definition is referenced by:  ajfval  30057