Definition df-adjh 9692

Description: Define the adjoint of a Hilbert space operator (if it exists). The domain of adj_h 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 adjbdlnt 9931) that the adjoint exists for a bounded linear operator.

Assertion

Ref	Expression
df-adjh	|- adjh = {<.t, u>. | (t:H~-->H~ /\ u:H~-->H~ /\ A.x e. H~ A.y e. H~ ((t` x) .ih y) = (x .ih (u` y)))}

Distinct variable group:   u,t,x,y

Detailed syntax breakdown of Definition df-adjh

Step	Hyp	Ref	Expression
1		cado 8763	. 2 class adjh
2		chil 8727	. . . . 5 class H~
3		vt	. . . . . 6 set t
4	3	cv 952	. . . . 5 class t
5	2, 2, 4	wf 3168	. . . 4 wff t:H~-->H~
6		vu	. . . . . 6 set u
7	6	cv 952	. . . . 5 class u
8	2, 2, 7	wf 3168	. . . 4 wff u:H~-->H~
9		vx	. . . . . . . . . 10 set x
10	9	cv 952	. . . . . . . . 9 class x
11	10, 4	cfv 3172	. . . . . . . 8 class (t` x)
12		vy	. . . . . . . . 9 set y
13	12	cv 952	. . . . . . . 8 class y
14		csp 8732	. . . . . . . 8 class .ih
15	11, 13, 14	co 3948	. . . . . . 7 class ((t` x) .ih y)
16	13, 7	cfv 3172	. . . . . . . 8 class (u` y)
17	10, 16, 14	co 3948	. . . . . . 7 class (x .ih (u` y))
18	15, 17	wceq 953	. . . . . 6 wff ((t` x) .ih y) = (x .ih (u` y))
19	18, 12, 2	wral 1637	. . . . 5 wff A.y e. H~ ((t` x) .ih y) = (x .ih (u` y))
20	19, 9, 2	wral 1637	. . . 4 wff A.x e. H~ A.y e. H~ ((t` x) .ih y) = (x .ih (u` y))
21	5, 8, 20	w3a 773	. . 3 wff (t:H~-->H~ /\ u:H~-->H~ /\ A.x e. H~ A.y e. H~ ((t` x) .ih y) = (x .ih (u` y)))
22	21, 3, 6	copab 2656	. 2 class {<.t, u>. | (t:H~-->H~ /\ u:H~-->H~ /\ A.x e. H~ A.y e. H~ ((t` x) .ih y) = (x .ih (u` y)))}
23	1, 22	wceq 953	1 wff adjh = {<.t, u>. | (t:H~-->H~ /\ u:H~-->H~ /\ A.x e. H~ A.y e. H~ ((t` x) .ih y) = (x .ih (u` y)))}

This definition is referenced by:  dfadj2 9729  adjeqt 9775

Copyright terms: Public domain