Metamath Proof Explorer


Theorem dfadj2

Description: Alternate definition of the adjoint of a Hilbert space operator. (Contributed by NM, 20-Feb-2006) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 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 ) ) ) }
2 adjsym
 |-  ( ( t : ~H --> ~H /\ u : ~H --> ~H ) -> ( A. x e. ~H A. y e. ~H ( x .ih ( t ` y ) ) = ( ( u ` x ) .ih y ) <-> A. x e. ~H A. y e. ~H ( x .ih ( u ` y ) ) = ( ( t ` x ) .ih y ) ) )
3 eqcom
 |-  ( ( ( t ` x ) .ih y ) = ( x .ih ( u ` y ) ) <-> ( x .ih ( u ` y ) ) = ( ( t ` x ) .ih y ) )
4 3 2ralbii
 |-  ( A. x e. ~H A. y e. ~H ( ( t ` x ) .ih y ) = ( x .ih ( u ` y ) ) <-> A. x e. ~H A. y e. ~H ( x .ih ( u ` y ) ) = ( ( t ` x ) .ih y ) )
5 2 4 syl6rbbr
 |-  ( ( t : ~H --> ~H /\ u : ~H --> ~H ) -> ( A. x e. ~H A. y e. ~H ( ( t ` x ) .ih y ) = ( x .ih ( u ` y ) ) <-> A. x e. ~H A. y e. ~H ( x .ih ( t ` y ) ) = ( ( u ` x ) .ih y ) ) )
6 5 pm5.32i
 |-  ( ( ( t : ~H --> ~H /\ u : ~H --> ~H ) /\ A. x e. ~H A. y e. ~H ( ( t ` x ) .ih y ) = ( x .ih ( u ` y ) ) ) <-> ( ( t : ~H --> ~H /\ u : ~H --> ~H ) /\ A. x e. ~H A. y e. ~H ( x .ih ( t ` y ) ) = ( ( u ` x ) .ih y ) ) )
7 df-3an
 |-  ( ( t : ~H --> ~H /\ u : ~H --> ~H /\ A. x e. ~H A. y e. ~H ( ( t ` x ) .ih y ) = ( x .ih ( u ` y ) ) ) <-> ( ( t : ~H --> ~H /\ u : ~H --> ~H ) /\ A. x e. ~H A. y e. ~H ( ( t ` x ) .ih y ) = ( x .ih ( u ` y ) ) ) )
8 df-3an
 |-  ( ( t : ~H --> ~H /\ u : ~H --> ~H /\ A. x e. ~H A. y e. ~H ( x .ih ( t ` y ) ) = ( ( u ` x ) .ih y ) ) <-> ( ( t : ~H --> ~H /\ u : ~H --> ~H ) /\ A. x e. ~H A. y e. ~H ( x .ih ( t ` y ) ) = ( ( u ` x ) .ih y ) ) )
9 6 7 8 3bitr4i
 |-  ( ( t : ~H --> ~H /\ u : ~H --> ~H /\ A. x e. ~H A. y e. ~H ( ( t ` x ) .ih y ) = ( x .ih ( u ` y ) ) ) <-> ( t : ~H --> ~H /\ u : ~H --> ~H /\ A. x e. ~H A. y e. ~H ( x .ih ( t ` y ) ) = ( ( u ` x ) .ih y ) ) )
10 9 opabbii
 |-  { <. t , u >. | ( t : ~H --> ~H /\ u : ~H --> ~H /\ A. x e. ~H A. y e. ~H ( ( t ` x ) .ih y ) = ( x .ih ( u ` y ) ) ) } = { <. t , u >. | ( t : ~H --> ~H /\ u : ~H --> ~H /\ A. x e. ~H A. y e. ~H ( x .ih ( t ` y ) ) = ( ( u ` x ) .ih y ) ) }
11 1 10 eqtri
 |-  adjh = { <. t , u >. | ( t : ~H --> ~H /\ u : ~H --> ~H /\ A. x e. ~H A. y e. ~H ( x .ih ( t ` y ) ) = ( ( u ` x ) .ih y ) ) }