Definition df-aj 28527

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 28525	. 2 class adj
2		vu	. . 3 setvar 𝑢
3		vw	. . 3 setvar 𝑤
4		cnv 28361	. . 3 class NrmCVec
5	2	cv 1536	. . . . . . 7 class 𝑢
6		cba 28363	. . . . . . 7 class BaseSet
7	5, 6	cfv 6355	. . . . . 6 class (BaseSet‘𝑢)
8	3	cv 1536	. . . . . . 7 class 𝑤
9	8, 6	cfv 6355	. . . . . 6 class (BaseSet‘𝑤)
10		vt	. . . . . . 7 setvar 𝑡
11	10	cv 1536	. . . . . 6 class 𝑡
12	7, 9, 11	wf 6351	. . . . 5 wff 𝑡:(BaseSet‘𝑢)⟶(BaseSet‘𝑤)
13		vs	. . . . . . 7 setvar 𝑠
14	13	cv 1536	. . . . . 6 class 𝑠
15	9, 7, 14	wf 6351	. . . . 5 wff 𝑠:(BaseSet‘𝑤)⟶(BaseSet‘𝑢)
16		vx	. . . . . . . . . . 11 setvar 𝑥
17	16	cv 1536	. . . . . . . . . 10 class 𝑥
18	17, 11	cfv 6355	. . . . . . . . 9 class (𝑡‘𝑥)
19		vy	. . . . . . . . . 10 setvar 𝑦
20	19	cv 1536	. . . . . . . . 9 class 𝑦
21		cdip 28477	. . . . . . . . . 10 class ·𝑖OLD
22	8, 21	cfv 6355	. . . . . . . . 9 class (·𝑖OLD‘𝑤)
23	18, 20, 22	co 7156	. . . . . . . 8 class ((𝑡‘𝑥)(·𝑖OLD‘𝑤)𝑦)
24	20, 14	cfv 6355	. . . . . . . . 9 class (𝑠‘𝑦)
25	5, 21	cfv 6355	. . . . . . . . 9 class (·𝑖OLD‘𝑢)
26	17, 24, 25	co 7156	. . . . . . . 8 class (𝑥(·𝑖OLD‘𝑢)(𝑠‘𝑦))
27	23, 26	wceq 1537	. . . . . . 7 wff ((𝑡‘𝑥)(·𝑖OLD‘𝑤)𝑦) = (𝑥(·𝑖OLD‘𝑢)(𝑠‘𝑦))
28	27, 19, 9	wral 3138	. . . . . 6 wff ∀𝑦 ∈ (BaseSet‘𝑤)((𝑡‘𝑥)(·𝑖OLD‘𝑤)𝑦) = (𝑥(·𝑖OLD‘𝑢)(𝑠‘𝑦))
29	28, 16, 7	wral 3138	. . . . 5 wff ∀𝑥 ∈ (BaseSet‘𝑢)∀𝑦 ∈ (BaseSet‘𝑤)((𝑡‘𝑥)(·𝑖OLD‘𝑤)𝑦) = (𝑥(·𝑖OLD‘𝑢)(𝑠‘𝑦))
30	12, 15, 29	w3a 1083	. . . 4 wff (𝑡:(BaseSet‘𝑢)⟶(BaseSet‘𝑤) ∧ 𝑠:(BaseSet‘𝑤)⟶(BaseSet‘𝑢) ∧ ∀𝑥 ∈ (BaseSet‘𝑢)∀𝑦 ∈ (BaseSet‘𝑤)((𝑡‘𝑥)(·𝑖OLD‘𝑤)𝑦) = (𝑥(·𝑖OLD‘𝑢)(𝑠‘𝑦)))
31	30, 10, 13	copab 5128	. . 3 class {⟨𝑡, 𝑠⟩ ∣ (𝑡:(BaseSet‘𝑢)⟶(BaseSet‘𝑤) ∧ 𝑠:(BaseSet‘𝑤)⟶(BaseSet‘𝑢) ∧ ∀𝑥 ∈ (BaseSet‘𝑢)∀𝑦 ∈ (BaseSet‘𝑤)((𝑡‘𝑥)(·𝑖OLD‘𝑤)𝑦) = (𝑥(·𝑖OLD‘𝑢)(𝑠‘𝑦)))}
32	2, 3, 4, 4, 31	cmpo 7158	. 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  28586