Metamath Proof Explorer

Theorem unopf1o

Description: A unitary operator in Hilbert space is one-to-one and onto. (Contributed by NM, 22-Jan-2006) (New usage is discouraged.)

Ref Expression
Assertion unopf1o 
|- ( T e. UniOp -> T : ~H -1-1-onto-> ~H )

Proof

Step Hyp Ref Expression
1 elunop 
 |-  ( T e. UniOp <-> ( T : ~H -onto-> ~H /\ A. x e. ~H A. y e. ~H ( ( T ` x ) .ih ( T ` y ) ) = ( x .ih y ) ) )
2 1 simplbi 
 |-  ( T e. UniOp -> T : ~H -onto-> ~H )
3 fof 
 |-  ( T : ~H -onto-> ~H -> T : ~H --> ~H )
4 2 3 syl 
 |-  ( T e. UniOp -> T : ~H --> ~H )
5 unop 
 |-  ( ( T e. UniOp /\ x e. ~H /\ x e. ~H ) -> ( ( T ` x ) .ih ( T ` x ) ) = ( x .ih x ) )
6 5 3anidm23 
 |-  ( ( T e. UniOp /\ x e. ~H ) -> ( ( T ` x ) .ih ( T ` x ) ) = ( x .ih x ) )
7 6 3adant3 
 |-  ( ( T e. UniOp /\ x e. ~H /\ y e. ~H ) -> ( ( T ` x ) .ih ( T ` x ) ) = ( x .ih x ) )
8 unop 
 |-  ( ( T e. UniOp /\ y e. ~H /\ y e. ~H ) -> ( ( T ` y ) .ih ( T ` y ) ) = ( y .ih y ) )
9 8 3anidm23 
 |-  ( ( T e. UniOp /\ y e. ~H ) -> ( ( T ` y ) .ih ( T ` y ) ) = ( y .ih y ) )
10 9 3adant2 
 |-  ( ( T e. UniOp /\ x e. ~H /\ y e. ~H ) -> ( ( T ` y ) .ih ( T ` y ) ) = ( y .ih y ) )
11 7 10 oveq12d 
 |-  ( ( T e. UniOp /\ x e. ~H /\ y e. ~H ) -> ( ( ( T ` x ) .ih ( T ` x ) ) + ( ( T ` y ) .ih ( T ` y ) ) ) = ( ( x .ih x ) + ( y .ih y ) ) )
12 unop 
 |-  ( ( T e. UniOp /\ x e. ~H /\ y e. ~H ) -> ( ( T ` x ) .ih ( T ` y ) ) = ( x .ih y ) )
13 unop 
 |-  ( ( T e. UniOp /\ y e. ~H /\ x e. ~H ) -> ( ( T ` y ) .ih ( T ` x ) ) = ( y .ih x ) )
14 13 3com23 
 |-  ( ( T e. UniOp /\ x e. ~H /\ y e. ~H ) -> ( ( T ` y ) .ih ( T ` x ) ) = ( y .ih x ) )
15 12 14 oveq12d 
 |-  ( ( T e. UniOp /\ x e. ~H /\ y e. ~H ) -> ( ( ( T ` x ) .ih ( T ` y ) ) + ( ( T ` y ) .ih ( T ` x ) ) ) = ( ( x .ih y ) + ( y .ih x ) ) )
16 11 15 oveq12d 
 |-  ( ( T e. UniOp /\ x e. ~H /\ y e. ~H ) -> ( ( ( ( T ` x ) .ih ( T ` x ) ) + ( ( T ` y ) .ih ( T ` y ) ) ) - ( ( ( T ` x ) .ih ( T ` y ) ) + ( ( T ` y ) .ih ( T ` x ) ) ) ) = ( ( ( x .ih x ) + ( y .ih y ) ) - ( ( x .ih y ) + ( y .ih x ) ) ) )
17 16 3expb 
 |-  ( ( T e. UniOp /\ ( x e. ~H /\ y e. ~H ) ) -> ( ( ( ( T ` x ) .ih ( T ` x ) ) + ( ( T ` y ) .ih ( T ` y ) ) ) - ( ( ( T ` x ) .ih ( T ` y ) ) + ( ( T ` y ) .ih ( T ` x ) ) ) ) = ( ( ( x .ih x ) + ( y .ih y ) ) - ( ( x .ih y ) + ( y .ih x ) ) ) )
18 ffvelcdm 
 |-  ( ( T : ~H --> ~H /\ x e. ~H ) -> ( T ` x ) e. ~H )
19 ffvelcdm 
 |-  ( ( T : ~H --> ~H /\ y e. ~H ) -> ( T ` y ) e. ~H )
20 18 19 anim12dan 
 |-  ( ( T : ~H --> ~H /\ ( x e. ~H /\ y e. ~H ) ) -> ( ( T ` x ) e. ~H /\ ( T ` y ) e. ~H ) )
21 4 20 sylan 
 |-  ( ( T e. UniOp /\ ( x e. ~H /\ y e. ~H ) ) -> ( ( T ` x ) e. ~H /\ ( T ` y ) e. ~H ) )
22 normlem9at 
 |-  ( ( ( T ` x ) e. ~H /\ ( T ` y ) e. ~H ) -> ( ( ( T ` x ) -h ( T ` y ) ) .ih ( ( T ` x ) -h ( T ` y ) ) ) = ( ( ( ( T ` x ) .ih ( T ` x ) ) + ( ( T ` y ) .ih ( T ` y ) ) ) - ( ( ( T ` x ) .ih ( T ` y ) ) + ( ( T ` y ) .ih ( T ` x ) ) ) ) )
23 21 22 syl 
 |-  ( ( T e. UniOp /\ ( x e. ~H /\ y e. ~H ) ) -> ( ( ( T ` x ) -h ( T ` y ) ) .ih ( ( T ` x ) -h ( T ` y ) ) ) = ( ( ( ( T ` x ) .ih ( T ` x ) ) + ( ( T ` y ) .ih ( T ` y ) ) ) - ( ( ( T ` x ) .ih ( T ` y ) ) + ( ( T ` y ) .ih ( T ` x ) ) ) ) )
24 normlem9at 
 |-  ( ( x e. ~H /\ y e. ~H ) -> ( ( x -h y ) .ih ( x -h y ) ) = ( ( ( x .ih x ) + ( y .ih y ) ) - ( ( x .ih y ) + ( y .ih x ) ) ) )
25 24 adantl 
 |-  ( ( T e. UniOp /\ ( x e. ~H /\ y e. ~H ) ) -> ( ( x -h y ) .ih ( x -h y ) ) = ( ( ( x .ih x ) + ( y .ih y ) ) - ( ( x .ih y ) + ( y .ih x ) ) ) )
26 17 23 25 3eqtr4rd 
 |-  ( ( T e. UniOp /\ ( x e. ~H /\ y e. ~H ) ) -> ( ( x -h y ) .ih ( x -h y ) ) = ( ( ( T ` x ) -h ( T ` y ) ) .ih ( ( T ` x ) -h ( T ` y ) ) ) )
27 26 eqeq1d 
 |-  ( ( T e. UniOp /\ ( x e. ~H /\ y e. ~H ) ) -> ( ( ( x -h y ) .ih ( x -h y ) ) = 0 <-> ( ( ( T ` x ) -h ( T ` y ) ) .ih ( ( T ` x ) -h ( T ` y ) ) ) = 0 ) )
28 hvsubcl 
 |-  ( ( x e. ~H /\ y e. ~H ) -> ( x -h y ) e. ~H )
29 his6 
 |-  ( ( x -h y ) e. ~H -> ( ( ( x -h y ) .ih ( x -h y ) ) = 0 <-> ( x -h y ) = 0h ) )
30 28 29 syl 
 |-  ( ( x e. ~H /\ y e. ~H ) -> ( ( ( x -h y ) .ih ( x -h y ) ) = 0 <-> ( x -h y ) = 0h ) )
31 hvsubeq0 
 |-  ( ( x e. ~H /\ y e. ~H ) -> ( ( x -h y ) = 0h <-> x = y ) )
32 30 31 bitrd 
 |-  ( ( x e. ~H /\ y e. ~H ) -> ( ( ( x -h y ) .ih ( x -h y ) ) = 0 <-> x = y ) )
33 32 adantl 
 |-  ( ( T e. UniOp /\ ( x e. ~H /\ y e. ~H ) ) -> ( ( ( x -h y ) .ih ( x -h y ) ) = 0 <-> x = y ) )
34 hvsubcl 
 |-  ( ( ( T ` x ) e. ~H /\ ( T ` y ) e. ~H ) -> ( ( T ` x ) -h ( T ` y ) ) e. ~H )
35 his6 
 |-  ( ( ( T ` x ) -h ( T ` y ) ) e. ~H -> ( ( ( ( T ` x ) -h ( T ` y ) ) .ih ( ( T ` x ) -h ( T ` y ) ) ) = 0 <-> ( ( T ` x ) -h ( T ` y ) ) = 0h ) )
36 34 35 syl 
 |-  ( ( ( T ` x ) e. ~H /\ ( T ` y ) e. ~H ) -> ( ( ( ( T ` x ) -h ( T ` y ) ) .ih ( ( T ` x ) -h ( T ` y ) ) ) = 0 <-> ( ( T ` x ) -h ( T ` y ) ) = 0h ) )
37 hvsubeq0 
 |-  ( ( ( T ` x ) e. ~H /\ ( T ` y ) e. ~H ) -> ( ( ( T ` x ) -h ( T ` y ) ) = 0h <-> ( T ` x ) = ( T ` y ) ) )
38 36 37 bitrd 
 |-  ( ( ( T ` x ) e. ~H /\ ( T ` y ) e. ~H ) -> ( ( ( ( T ` x ) -h ( T ` y ) ) .ih ( ( T ` x ) -h ( T ` y ) ) ) = 0 <-> ( T ` x ) = ( T ` y ) ) )
39 21 38 syl 
 |-  ( ( T e. UniOp /\ ( x e. ~H /\ y e. ~H ) ) -> ( ( ( ( T ` x ) -h ( T ` y ) ) .ih ( ( T ` x ) -h ( T ` y ) ) ) = 0 <-> ( T ` x ) = ( T ` y ) ) )
40 27 33 39 3bitr3rd 
 |-  ( ( T e. UniOp /\ ( x e. ~H /\ y e. ~H ) ) -> ( ( T ` x ) = ( T ` y ) <-> x = y ) )
41 40 biimpd 
 |-  ( ( T e. UniOp /\ ( x e. ~H /\ y e. ~H ) ) -> ( ( T ` x ) = ( T ` y ) -> x = y ) )
42 41 ralrimivva 
 |-  ( T e. UniOp -> A. x e. ~H A. y e. ~H ( ( T ` x ) = ( T ` y ) -> x = y ) )
43 dff13 
 |-  ( T : ~H -1-1-> ~H <-> ( T : ~H --> ~H /\ A. x e. ~H A. y e. ~H ( ( T ` x ) = ( T ` y ) -> x = y ) ) )
44 4 42 43 sylanbrc 
 |-  ( T e. UniOp -> T : ~H -1-1-> ~H )
45 df-f1o 
 |-  ( T : ~H -1-1-onto-> ~H <-> ( T : ~H -1-1-> ~H /\ T : ~H -onto-> ~H ) )
46 44 2 45 sylanbrc 
 |-  ( T e. UniOp -> T : ~H -1-1-onto-> ~H )