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

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 eqcom 
 |-  ( ( ( t ` x ) .ih y ) = ( x .ih ( u ` y ) ) <-> ( x .ih ( u ` y ) ) = ( ( t ` x ) .ih y ) )
3 2 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 ) )
4 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 ) ) )
5 3 4 bitr4id 
 |-  ( ( 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 ) ) }