Definition df-adjh 32433

Description: Define the adjoint of a Hilbert space operator (if it exists). The domain of adj_ℎ is the set of all adjoint operators. Definition of adjoint in [Kalmbach2] p. 8. Unlike Kalmbach (and most authors), we do not demand that the operator be linear, but instead show (in adjbdln 32667) that the adjoint exists for a bounded linear operator. (Contributed by NM, 20-Feb-2006.) (New usage is discouraged.)

Assertion

Ref	Expression
df-adjh	⊢ adjℎ = {⟨𝑡, 𝑢⟩ ∣ (𝑡: ℋ⟶ ℋ ∧ 𝑢: ℋ⟶ ℋ ∧ ∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ ((𝑡‘𝑥) ·ih 𝑦) = (𝑥 ·ih (𝑢‘𝑦)))}

Distinct variable group:   𝑢,𝑡,𝑥,𝑦

Detailed syntax breakdown of Definition df-adjh

Step	Hyp	Ref	Expression
1		cado 31539	. 2 class adjℎ
2		chba 31503	. . . . 5 class ℋ
3		vt	. . . . . 6 setvar 𝑡
4	3	cv 1569	. . . . 5 class 𝑡
5	2, 2, 4	wf 6527	. . . 4 wff 𝑡: ℋ⟶ ℋ
6		vu	. . . . . 6 setvar 𝑢
7	6	cv 1569	. . . . 5 class 𝑢
8	2, 2, 7	wf 6527	. . . 4 wff 𝑢: ℋ⟶ ℋ
9		vx	. . . . . . . . . 10 setvar 𝑥
10	9	cv 1569	. . . . . . . . 9 class 𝑥
11	10, 4	cfv 6531	. . . . . . . 8 class (𝑡‘𝑥)
12		vy	. . . . . . . . 9 setvar 𝑦
13	12	cv 1569	. . . . . . . 8 class 𝑦
14		csp 31506	. . . . . . . 8 class ·ih
15	11, 13, 14	co 7412	. . . . . . 7 class ((𝑡‘𝑥) ·ih 𝑦)
16	13, 7	cfv 6531	. . . . . . . 8 class (𝑢‘𝑦)
17	10, 16, 14	co 7412	. . . . . . 7 class (𝑥 ·ih (𝑢‘𝑦))
18	15, 17	wceq 1570	. . . . . 6 wff ((𝑡‘𝑥) ·ih 𝑦) = (𝑥 ·ih (𝑢‘𝑦))
19	18, 12, 2	wral 3077	. . . . 5 wff ∀𝑦 ∈ ℋ ((𝑡‘𝑥) ·ih 𝑦) = (𝑥 ·ih (𝑢‘𝑦))
20	19, 9, 2	wral 3077	. . . 4 wff ∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ ((𝑡‘𝑥) ·ih 𝑦) = (𝑥 ·ih (𝑢‘𝑦))
21	5, 8, 20	w3a 1103	. . 3 wff (𝑡: ℋ⟶ ℋ ∧ 𝑢: ℋ⟶ ℋ ∧ ∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ ((𝑡‘𝑥) ·ih 𝑦) = (𝑥 ·ih (𝑢‘𝑦)))
22	21, 3, 6	copab 5167	. 2 class {⟨𝑡, 𝑢⟩ ∣ (𝑡: ℋ⟶ ℋ ∧ 𝑢: ℋ⟶ ℋ ∧ ∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ ((𝑡‘𝑥) ·ih 𝑦) = (𝑥 ·ih (𝑢‘𝑦)))}
23	1, 22	wceq 1570	1 wff adjℎ = {⟨𝑡, 𝑢⟩ ∣ (𝑡: ℋ⟶ ℋ ∧ 𝑢: ℋ⟶ ℋ ∧ ∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ ((𝑡‘𝑥) ·ih 𝑦) = (𝑥 ·ih (𝑢‘𝑦)))}

This definition is used by:  dfadj2  32469  adjeq  32519