Definition df-adjh 28708

Description: Define the adjoint of a Hilbert space operator (if it exists). The domain of adjh 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 28942) that the adjoint exists for a bounded linear operator. (Contributed by NM, 20-Feb-2006.) (New usage is discouraged.)

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 27812	. 2 class adjh
2		chil 27776	. . . . 5 class ~H
3		vt	. . . . . 6 setvar t
4	3	cv 1482	. . . . 5 class t
5	2, 2, 4	wf 5884	. . . 4 wff t : ~H --> ~H
6		vu	. . . . . 6 setvar u
7	6	cv 1482	. . . . 5 class u
8	2, 2, 7	wf 5884	. . . 4 wff u : ~H --> ~H
9		vx	. . . . . . . . . 10 setvar x
10	9	cv 1482	. . . . . . . . 9 class x
11	10, 4	cfv 5888	. . . . . . . 8 class ( t ` x )
12		vy	. . . . . . . . 9 setvar y
13	12	cv 1482	. . . . . . . 8 class y
14		csp 27779	. . . . . . . 8 class .ih
15	11, 13, 14	co 6650	. . . . . . 7 class ( ( t ` x ) .ih y )
16	13, 7	cfv 5888	. . . . . . . 8 class ( u ` y )
17	10, 16, 14	co 6650	. . . . . . 7 class ( x .ih ( u ` y ) )
18	15, 17	wceq 1483	. . . . . 6 wff ( ( t ` x ) .ih y ) = ( x .ih ( u ` y ) )
19	18, 12, 2	wral 2912	. . . . 5 wff A. y e. ~H ( ( t ` x ) .ih y ) = ( x .ih ( u ` y ) )
20	19, 9, 2	wral 2912	. . . 4 wff A. x e. ~H A. y e. ~H ( ( t ` x ) .ih y ) = ( x .ih ( u ` y ) )
21	5, 8, 20	w3a 1037	. . 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 4712	. 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 1483	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  28744  adjeq  28794