Definition df-aj 27605

Description: Define the adjoint of an operator (if it exists). The domain of U adj W is the set of all operators from U to W that have an adjoint. Definition 3.9-1 of [Kreyszig] p. 196, although we don't require that U and W 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 = ( u e. NrmCVec , w e. NrmCVec |-> { <. t , s >. | ( t : ( BaseSet ` u ) --> ( BaseSet ` w ) /\ s : ( BaseSet ` w ) --> ( BaseSet ` u ) /\ A. x e. ( BaseSet ` u ) A. y e. ( BaseSet ` w ) ( ( t ` x ) ( .iOLD ` w ) y ) = ( x ( .iOLD ` u ) ( s ` y ) ) ) } )

Distinct variable group:   t, s, u, w, x, y

Detailed syntax breakdown of Definition df-aj

Step	Hyp	Ref	Expression
1		caj 27603	. 2 class adj
2		vu	. . 3 setvar u
3		vw	. . 3 setvar w
4		cnv 27439	. . 3 class NrmCVec
5	2	cv 1482	. . . . . . 7 class u
6		cba 27441	. . . . . . 7 class BaseSet
7	5, 6	cfv 5888	. . . . . 6 class ( BaseSet ` u )
8	3	cv 1482	. . . . . . 7 class w
9	8, 6	cfv 5888	. . . . . 6 class ( BaseSet ` w )
10		vt	. . . . . . 7 setvar t
11	10	cv 1482	. . . . . 6 class t
12	7, 9, 11	wf 5884	. . . . 5 wff t : ( BaseSet ` u ) --> ( BaseSet ` w )
13		vs	. . . . . . 7 setvar s
14	13	cv 1482	. . . . . 6 class s
15	9, 7, 14	wf 5884	. . . . 5 wff s : ( BaseSet ` w ) --> ( BaseSet ` u )
16		vx	. . . . . . . . . . 11 setvar x
17	16	cv 1482	. . . . . . . . . 10 class x
18	17, 11	cfv 5888	. . . . . . . . 9 class ( t ` x )
19		vy	. . . . . . . . . 10 setvar y
20	19	cv 1482	. . . . . . . . 9 class y
21		cdip 27555	. . . . . . . . . 10 class .iOLD
22	8, 21	cfv 5888	. . . . . . . . 9 class ( .iOLD ` w )
23	18, 20, 22	co 6650	. . . . . . . 8 class ( ( t ` x ) ( .iOLD ` w ) y )
24	20, 14	cfv 5888	. . . . . . . . 9 class ( s ` y )
25	5, 21	cfv 5888	. . . . . . . . 9 class ( .iOLD ` u )
26	17, 24, 25	co 6650	. . . . . . . 8 class ( x ( .iOLD ` u ) ( s ` y ) )
27	23, 26	wceq 1483	. . . . . . 7 wff ( ( t ` x ) ( .iOLD ` w ) y ) = ( x ( .iOLD ` u ) ( s ` y ) )
28	27, 19, 9	wral 2912	. . . . . 6 wff A. y e. ( BaseSet ` w ) ( ( t ` x ) ( .iOLD ` w ) y ) = ( x ( .iOLD ` u ) ( s ` y ) )
29	28, 16, 7	wral 2912	. . . . 5 wff A. x e. ( BaseSet ` u ) A. y e. ( BaseSet ` w ) ( ( t ` x ) ( .iOLD ` w ) y ) = ( x ( .iOLD ` u ) ( s ` y ) )
30	12, 15, 29	w3a 1037	. . . 4 wff ( t : ( BaseSet ` u ) --> ( BaseSet ` w ) /\ s : ( BaseSet ` w ) --> ( BaseSet ` u ) /\ A. x e. ( BaseSet ` u ) A. y e. ( BaseSet ` w ) ( ( t ` x ) ( .iOLD ` w ) y ) = ( x ( .iOLD ` u ) ( s ` y ) ) )
31	30, 10, 13	copab 4712	. . 3 class { <. t , s >. | ( t : ( BaseSet ` u ) --> ( BaseSet ` w ) /\ s : ( BaseSet ` w ) --> ( BaseSet ` u ) /\ A. x e. ( BaseSet ` u ) A. y e. ( BaseSet ` w ) ( ( t ` x ) ( .iOLD ` w ) y ) = ( x ( .iOLD ` u ) ( s ` y ) ) ) }
32	2, 3, 4, 4, 31	cmpt2 6652	. 2 class ( u e. NrmCVec , w e. NrmCVec |-> { <. t , s >. | ( t : ( BaseSet ` u ) --> ( BaseSet ` w ) /\ s : ( BaseSet ` w ) --> ( BaseSet ` u ) /\ A. x e. ( BaseSet ` u ) A. y e. ( BaseSet ` w ) ( ( t ` x ) ( .iOLD ` w ) y ) = ( x ( .iOLD ` u ) ( s ` y ) ) ) } )
33	1, 32	wceq 1483	1 wff adj = ( u e. NrmCVec , w e. NrmCVec |-> { <. t , s >. | ( t : ( BaseSet ` u ) --> ( BaseSet ` w ) /\ s : ( BaseSet ` w ) --> ( BaseSet ` u ) /\ A. x e. ( BaseSet ` u ) A. y e. ( BaseSet ` w ) ( ( t ` x ) ( .iOLD ` w ) y ) = ( x ( .iOLD ` u ) ( s ` y ) ) ) } )

This definition is referenced by:  ajfval  27664