Definition df-aj 30732

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 30730	. 2 class adj
2		vu	. . 3 setvar 𝑢
3		vw	. . 3 setvar 𝑤
4		cnv 30566	. . 3 class NrmCVec
5	2	cv 1540	. . . . . . 7 class 𝑢
6		cba 30568	. . . . . . 7 class BaseSet
7	5, 6	cfv 6486	. . . . . 6 class (BaseSet‘𝑢)
8	3	cv 1540	. . . . . . 7 class 𝑤
9	8, 6	cfv 6486	. . . . . 6 class (BaseSet‘𝑤)
10		vt	. . . . . . 7 setvar 𝑡
11	10	cv 1540	. . . . . 6 class 𝑡
12	7, 9, 11	wf 6482	. . . . 5 wff 𝑡:(BaseSet‘𝑢)⟶(BaseSet‘𝑤)
13		vs	. . . . . . 7 setvar 𝑠
14	13	cv 1540	. . . . . 6 class 𝑠
15	9, 7, 14	wf 6482	. . . . 5 wff 𝑠:(BaseSet‘𝑤)⟶(BaseSet‘𝑢)
16		vx	. . . . . . . . . . 11 setvar 𝑥
17	16	cv 1540	. . . . . . . . . 10 class 𝑥
18	17, 11	cfv 6486	. . . . . . . . 9 class (𝑡‘𝑥)
19		vy	. . . . . . . . . 10 setvar 𝑦
20	19	cv 1540	. . . . . . . . 9 class 𝑦
21		cdip 30682	. . . . . . . . . 10 class ·𝑖OLD
22	8, 21	cfv 6486	. . . . . . . . 9 class (·𝑖OLD‘𝑤)
23	18, 20, 22	co 7352	. . . . . . . 8 class ((𝑡‘𝑥)(·𝑖OLD‘𝑤)𝑦)
24	20, 14	cfv 6486	. . . . . . . . 9 class (𝑠‘𝑦)
25	5, 21	cfv 6486	. . . . . . . . 9 class (·𝑖OLD‘𝑢)
26	17, 24, 25	co 7352	. . . . . . . 8 class (𝑥(·𝑖OLD‘𝑢)(𝑠‘𝑦))
27	23, 26	wceq 1541	. . . . . . 7 wff ((𝑡‘𝑥)(·𝑖OLD‘𝑤)𝑦) = (𝑥(·𝑖OLD‘𝑢)(𝑠‘𝑦))
28	27, 19, 9	wral 3048	. . . . . 6 wff ∀𝑦 ∈ (BaseSet‘𝑤)((𝑡‘𝑥)(·𝑖OLD‘𝑤)𝑦) = (𝑥(·𝑖OLD‘𝑢)(𝑠‘𝑦))
29	28, 16, 7	wral 3048	. . . . 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 5155	. . 3 class {⟨𝑡, 𝑠⟩ ∣ (𝑡:(BaseSet‘𝑢)⟶(BaseSet‘𝑤) ∧ 𝑠:(BaseSet‘𝑤)⟶(BaseSet‘𝑢) ∧ ∀𝑥 ∈ (BaseSet‘𝑢)∀𝑦 ∈ (BaseSet‘𝑤)((𝑡‘𝑥)(·𝑖OLD‘𝑤)𝑦) = (𝑥(·𝑖OLD‘𝑢)(𝑠‘𝑦)))}
32	2, 3, 4, 4, 31	cmpo 7354	. 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  30791