Definition df-aj 30782

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 30780	. 2 class adj
2		vu	. . 3 setvar 𝑢
3		vw	. . 3 setvar 𝑤
4		cnv 30616	. . 3 class NrmCVec
5	2	cv 1536	. . . . . . 7 class 𝑢
6		cba 30618	. . . . . . 7 class BaseSet
7	5, 6	cfv 6573	. . . . . 6 class (BaseSet‘𝑢)
8	3	cv 1536	. . . . . . 7 class 𝑤
9	8, 6	cfv 6573	. . . . . 6 class (BaseSet‘𝑤)
10		vt	. . . . . . 7 setvar 𝑡
11	10	cv 1536	. . . . . 6 class 𝑡
12	7, 9, 11	wf 6569	. . . . 5 wff 𝑡:(BaseSet‘𝑢)⟶(BaseSet‘𝑤)
13		vs	. . . . . . 7 setvar 𝑠
14	13	cv 1536	. . . . . 6 class 𝑠
15	9, 7, 14	wf 6569	. . . . 5 wff 𝑠:(BaseSet‘𝑤)⟶(BaseSet‘𝑢)
16		vx	. . . . . . . . . . 11 setvar 𝑥
17	16	cv 1536	. . . . . . . . . 10 class 𝑥
18	17, 11	cfv 6573	. . . . . . . . 9 class (𝑡‘𝑥)
19		vy	. . . . . . . . . 10 setvar 𝑦
20	19	cv 1536	. . . . . . . . 9 class 𝑦
21		cdip 30732	. . . . . . . . . 10 class ·𝑖OLD
22	8, 21	cfv 6573	. . . . . . . . 9 class (·𝑖OLD‘𝑤)
23	18, 20, 22	co 7448	. . . . . . . 8 class ((𝑡‘𝑥)(·𝑖OLD‘𝑤)𝑦)
24	20, 14	cfv 6573	. . . . . . . . 9 class (𝑠‘𝑦)
25	5, 21	cfv 6573	. . . . . . . . 9 class (·𝑖OLD‘𝑢)
26	17, 24, 25	co 7448	. . . . . . . 8 class (𝑥(·𝑖OLD‘𝑢)(𝑠‘𝑦))
27	23, 26	wceq 1537	. . . . . . 7 wff ((𝑡‘𝑥)(·𝑖OLD‘𝑤)𝑦) = (𝑥(·𝑖OLD‘𝑢)(𝑠‘𝑦))
28	27, 19, 9	wral 3067	. . . . . 6 wff ∀𝑦 ∈ (BaseSet‘𝑤)((𝑡‘𝑥)(·𝑖OLD‘𝑤)𝑦) = (𝑥(·𝑖OLD‘𝑢)(𝑠‘𝑦))
29	28, 16, 7	wral 3067	. . . . 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 5228	. . 3 class {⟨𝑡, 𝑠⟩ ∣ (𝑡:(BaseSet‘𝑢)⟶(BaseSet‘𝑤) ∧ 𝑠:(BaseSet‘𝑤)⟶(BaseSet‘𝑢) ∧ ∀𝑥 ∈ (BaseSet‘𝑢)∀𝑦 ∈ (BaseSet‘𝑤)((𝑡‘𝑥)(·𝑖OLD‘𝑤)𝑦) = (𝑥(·𝑖OLD‘𝑢)(𝑠‘𝑦)))}
32	2, 3, 4, 4, 31	cmpo 7450	. 2 class (𝑢 ∈ NrmCVec, 𝑤 ∈ NrmCVec ↦ {⟨𝑡, 𝑠⟩ ∣ (𝑡:(BaseSet‘𝑢)⟶(BaseSet‘𝑤) ∧ 𝑠:(BaseSet‘𝑤)⟶(BaseSet‘𝑢) ∧ ∀𝑥 ∈ (BaseSet‘𝑢)∀𝑦 ∈ (BaseSet‘𝑤)((𝑡‘𝑥)(·𝑖OLD‘𝑤)𝑦) = (𝑥(·𝑖OLD‘𝑢)(𝑠‘𝑦)))})
33	1, 32	wceq 1537	1 wff adj = (𝑢 ∈ NrmCVec, 𝑤 ∈ NrmCVec ↦ {⟨𝑡, 𝑠⟩ ∣ (𝑡:(BaseSet‘𝑢)⟶(BaseSet‘𝑤) ∧ 𝑠:(BaseSet‘𝑤)⟶(BaseSet‘𝑢) ∧ ∀𝑥 ∈ (BaseSet‘𝑢)∀𝑦 ∈ (BaseSet‘𝑤)((𝑡‘𝑥)(·𝑖OLD‘𝑤)𝑦) = (𝑥(·𝑖OLD‘𝑢)(𝑠‘𝑦)))})

This definition is referenced by:  ajfval  30841