Definition df-aj 30679

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 30677	. 2 class adj
2		vu	. . 3 setvar 𝑢
3		vw	. . 3 setvar 𝑤
4		cnv 30513	. . 3 class NrmCVec
5	2	cv 1539	. . . . . . 7 class 𝑢
6		cba 30515	. . . . . . 7 class BaseSet
7	5, 6	cfv 6511	. . . . . 6 class (BaseSet‘𝑢)
8	3	cv 1539	. . . . . . 7 class 𝑤
9	8, 6	cfv 6511	. . . . . 6 class (BaseSet‘𝑤)
10		vt	. . . . . . 7 setvar 𝑡
11	10	cv 1539	. . . . . 6 class 𝑡
12	7, 9, 11	wf 6507	. . . . 5 wff 𝑡:(BaseSet‘𝑢)⟶(BaseSet‘𝑤)
13		vs	. . . . . . 7 setvar 𝑠
14	13	cv 1539	. . . . . 6 class 𝑠
15	9, 7, 14	wf 6507	. . . . 5 wff 𝑠:(BaseSet‘𝑤)⟶(BaseSet‘𝑢)
16		vx	. . . . . . . . . . 11 setvar 𝑥
17	16	cv 1539	. . . . . . . . . 10 class 𝑥
18	17, 11	cfv 6511	. . . . . . . . 9 class (𝑡‘𝑥)
19		vy	. . . . . . . . . 10 setvar 𝑦
20	19	cv 1539	. . . . . . . . 9 class 𝑦
21		cdip 30629	. . . . . . . . . 10 class ·𝑖OLD
22	8, 21	cfv 6511	. . . . . . . . 9 class (·𝑖OLD‘𝑤)
23	18, 20, 22	co 7387	. . . . . . . 8 class ((𝑡‘𝑥)(·𝑖OLD‘𝑤)𝑦)
24	20, 14	cfv 6511	. . . . . . . . 9 class (𝑠‘𝑦)
25	5, 21	cfv 6511	. . . . . . . . 9 class (·𝑖OLD‘𝑢)
26	17, 24, 25	co 7387	. . . . . . . 8 class (𝑥(·𝑖OLD‘𝑢)(𝑠‘𝑦))
27	23, 26	wceq 1540	. . . . . . 7 wff ((𝑡‘𝑥)(·𝑖OLD‘𝑤)𝑦) = (𝑥(·𝑖OLD‘𝑢)(𝑠‘𝑦))
28	27, 19, 9	wral 3044	. . . . . 6 wff ∀𝑦 ∈ (BaseSet‘𝑤)((𝑡‘𝑥)(·𝑖OLD‘𝑤)𝑦) = (𝑥(·𝑖OLD‘𝑢)(𝑠‘𝑦))
29	28, 16, 7	wral 3044	. . . . 5 wff ∀𝑥 ∈ (BaseSet‘𝑢)∀𝑦 ∈ (BaseSet‘𝑤)((𝑡‘𝑥)(·𝑖OLD‘𝑤)𝑦) = (𝑥(·𝑖OLD‘𝑢)(𝑠‘𝑦))
30	12, 15, 29	w3a 1086	. . . 4 wff (𝑡:(BaseSet‘𝑢)⟶(BaseSet‘𝑤) ∧ 𝑠:(BaseSet‘𝑤)⟶(BaseSet‘𝑢) ∧ ∀𝑥 ∈ (BaseSet‘𝑢)∀𝑦 ∈ (BaseSet‘𝑤)((𝑡‘𝑥)(·𝑖OLD‘𝑤)𝑦) = (𝑥(·𝑖OLD‘𝑢)(𝑠‘𝑦)))
31	30, 10, 13	copab 5169	. . 3 class {⟨𝑡, 𝑠⟩ ∣ (𝑡:(BaseSet‘𝑢)⟶(BaseSet‘𝑤) ∧ 𝑠:(BaseSet‘𝑤)⟶(BaseSet‘𝑢) ∧ ∀𝑥 ∈ (BaseSet‘𝑢)∀𝑦 ∈ (BaseSet‘𝑤)((𝑡‘𝑥)(·𝑖OLD‘𝑤)𝑦) = (𝑥(·𝑖OLD‘𝑢)(𝑠‘𝑦)))}
32	2, 3, 4, 4, 31	cmpo 7389	. 2 class (𝑢 ∈ NrmCVec, 𝑤 ∈ NrmCVec ↦ {⟨𝑡, 𝑠⟩ ∣ (𝑡:(BaseSet‘𝑢)⟶(BaseSet‘𝑤) ∧ 𝑠:(BaseSet‘𝑤)⟶(BaseSet‘𝑢) ∧ ∀𝑥 ∈ (BaseSet‘𝑢)∀𝑦 ∈ (BaseSet‘𝑤)((𝑡‘𝑥)(·𝑖OLD‘𝑤)𝑦) = (𝑥(·𝑖OLD‘𝑢)(𝑠‘𝑦)))})
33	1, 32	wceq 1540	1 wff adj = (𝑢 ∈ NrmCVec, 𝑤 ∈ NrmCVec ↦ {⟨𝑡, 𝑠⟩ ∣ (𝑡:(BaseSet‘𝑢)⟶(BaseSet‘𝑤) ∧ 𝑠:(BaseSet‘𝑤)⟶(BaseSet‘𝑢) ∧ ∀𝑥 ∈ (BaseSet‘𝑢)∀𝑦 ∈ (BaseSet‘𝑤)((𝑡‘𝑥)(·𝑖OLD‘𝑤)𝑦) = (𝑥(·𝑖OLD‘𝑢)(𝑠‘𝑦)))})

This definition is referenced by:  ajfval  30738