Metamath Proof Explorer

Theorem adjmo

Description: Every Hilbert space operator has at most one adjoint. (Contributed by NM, 18-Feb-2006) (New usage is discouraged.)

Ref Expression
Assertion adjmo 
|- E* u ( 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 r19.26-2 
 |-  ( A. x e. ~H A. y e. ~H ( ( x .ih ( T ` y ) ) = ( ( u ` x ) .ih y ) /\ ( x .ih ( T ` y ) ) = ( ( v ` x ) .ih y ) ) <-> ( 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 ( T ` y ) ) = ( ( v ` x ) .ih y ) ) )
2 eqtr2 
 |-  ( ( ( x .ih ( T ` y ) ) = ( ( u ` x ) .ih y ) /\ ( x .ih ( T ` y ) ) = ( ( v ` x ) .ih y ) ) -> ( ( u ` x ) .ih y ) = ( ( v ` x ) .ih y ) )
3 2 2ralimi 
 |-  ( A. x e. ~H A. y e. ~H ( ( x .ih ( T ` y ) ) = ( ( u ` x ) .ih y ) /\ ( x .ih ( T ` y ) ) = ( ( v ` x ) .ih y ) ) -> A. x e. ~H A. y e. ~H ( ( u ` x ) .ih y ) = ( ( v ` x ) .ih y ) )
4 1 3 sylbir 
 |-  ( ( 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 ( T ` y ) ) = ( ( v ` x ) .ih y ) ) -> A. x e. ~H A. y e. ~H ( ( u ` x ) .ih y ) = ( ( v ` x ) .ih y ) )
5 hoeq1 
 |-  ( ( u : ~H --> ~H /\ v : ~H --> ~H ) -> ( A. x e. ~H A. y e. ~H ( ( u ` x ) .ih y ) = ( ( v ` x ) .ih y ) <-> u = v ) )
6 5 biimpa 
 |-  ( ( ( u : ~H --> ~H /\ v : ~H --> ~H ) /\ A. x e. ~H A. y e. ~H ( ( u ` x ) .ih y ) = ( ( v ` x ) .ih y ) ) -> u = v )
7 4 6 sylan2 
 |-  ( ( ( u : ~H --> ~H /\ v : ~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 ( T ` y ) ) = ( ( v ` x ) .ih y ) ) ) -> u = v )
8 7 an4s 
 |-  ( ( ( u : ~H --> ~H /\ A. x e. ~H A. y e. ~H ( x .ih ( T ` y ) ) = ( ( u ` x ) .ih y ) ) /\ ( v : ~H --> ~H /\ A. x e. ~H A. y e. ~H ( x .ih ( T ` y ) ) = ( ( v ` x ) .ih y ) ) ) -> u = v )
9 8 gen2 
 |-  A. u A. v ( ( ( u : ~H --> ~H /\ A. x e. ~H A. y e. ~H ( x .ih ( T ` y ) ) = ( ( u ` x ) .ih y ) ) /\ ( v : ~H --> ~H /\ A. x e. ~H A. y e. ~H ( x .ih ( T ` y ) ) = ( ( v ` x ) .ih y ) ) ) -> u = v )
10 feq1 
 |-  ( u = v -> ( u : ~H --> ~H <-> v : ~H --> ~H ) )
11 fveq1 
 |-  ( u = v -> ( u ` x ) = ( v ` x ) )
12 11 oveq1d 
 |-  ( u = v -> ( ( u ` x ) .ih y ) = ( ( v ` x ) .ih y ) )
13 12 eqeq2d 
 |-  ( u = v -> ( ( x .ih ( T ` y ) ) = ( ( u ` x ) .ih y ) <-> ( x .ih ( T ` y ) ) = ( ( v ` x ) .ih y ) ) )
14 13 2ralbidv 
 |-  ( u = v -> ( 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 ( T ` y ) ) = ( ( v ` x ) .ih y ) ) )
15 10 14 anbi12d 
 |-  ( u = v -> ( ( u : ~H --> ~H /\ A. x e. ~H A. y e. ~H ( x .ih ( T ` y ) ) = ( ( u ` x ) .ih y ) ) <-> ( v : ~H --> ~H /\ A. x e. ~H A. y e. ~H ( x .ih ( T ` y ) ) = ( ( v ` x ) .ih y ) ) ) )
16 15 mo4 
 |-  ( E* u ( u : ~H --> ~H /\ A. x e. ~H A. y e. ~H ( x .ih ( T ` y ) ) = ( ( u ` x ) .ih y ) ) <-> A. u A. v ( ( ( u : ~H --> ~H /\ A. x e. ~H A. y e. ~H ( x .ih ( T ` y ) ) = ( ( u ` x ) .ih y ) ) /\ ( v : ~H --> ~H /\ A. x e. ~H A. y e. ~H ( x .ih ( T ` y ) ) = ( ( v ` x ) .ih y ) ) ) -> u = v ) )
17 9 16 mpbir 
 |-  E* u ( u : ~H --> ~H /\ A. x e. ~H A. y e. ~H ( x .ih ( T ` y ) ) = ( ( u ` x ) .ih y ) )