This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Definition df-adjh

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 ) that the adjoint exists for a bounded linear operator. (Contributed by NM, 20-Feb-2006) (New usage is discouraged.)

Ref Expression
Assertion 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 ) ) ) }

Detailed syntax breakdown

Step Hyp Ref Expression
0 cado 
 |-  adjh
1 vt 
 |-  t
2 vu 
 |-  u
3 1 cv 
 |-  t
4 chba 
 |-  ~H
5 4 4 3 wf 
 |-  t : ~H --> ~H
6 2 cv 
 |-  u
7 4 4 6 wf 
 |-  u : ~H --> ~H
8 vx 
 |-  x
9 vy 
 |-  y
10 8 cv 
 |-  x
11 10 3 cfv 
 |-  ( t ` x )
12 csp 
 |-  .ih
13 9 cv 
 |-  y
14 11 13 12 co 
 |-  ( ( t ` x ) .ih y )
15 13 6 cfv 
 |-  ( u ` y )
16 10 15 12 co 
 |-  ( x .ih ( u ` y ) )
17 14 16 wceq 
 |-  ( ( t ` x ) .ih y ) = ( x .ih ( u ` y ) )
18 17 9 4 wral 
 |-  A. y e. ~H ( ( t ` x ) .ih y ) = ( x .ih ( u ` y ) )
19 18 8 4 wral 
 |-  A. x e. ~H A. y e. ~H ( ( t ` x ) .ih y ) = ( x .ih ( u ` y ) )
20 5 7 19 w3a 
 |-  ( t : ~H --> ~H /\ u : ~H --> ~H /\ A. x e. ~H A. y e. ~H ( ( t ` x ) .ih y ) = ( x .ih ( u ` y ) ) )
21 20 1 2 copab 
 |-  { <. t , u >. | ( t : ~H --> ~H /\ u : ~H --> ~H /\ A. x e. ~H A. y e. ~H ( ( t ` x ) .ih y ) = ( x .ih ( u ` y ) ) ) }
22 0 21 wceq 
 |-  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 ) ) ) }