Metamath Proof Explorer

Theorem cnvunop

Description: The inverse (converse) of a unitary operator in Hilbert space is unitary. Theorem in AkhiezerGlazman p. 72. (Contributed by NM, 22-Jan-2006) (New usage is discouraged.)

Ref Expression
Assertion cnvunop 
|- ( T e. UniOp -> `' T e. UniOp )

Proof

Step Hyp Ref Expression
1 unopf1o 
 |-  ( T e. UniOp -> T : ~H -1-1-onto-> ~H )
2 f1ocnv 
 |-  ( T : ~H -1-1-onto-> ~H -> `' T : ~H -1-1-onto-> ~H )
3 f1ofo 
 |-  ( `' T : ~H -1-1-onto-> ~H -> `' T : ~H -onto-> ~H )
4 2 3 syl 
 |-  ( T : ~H -1-1-onto-> ~H -> `' T : ~H -onto-> ~H )
5 1 4 syl 
 |-  ( T e. UniOp -> `' T : ~H -onto-> ~H )
6 simpl 
 |-  ( ( T e. UniOp /\ ( x e. ~H /\ y e. ~H ) ) -> T e. UniOp )
7 fof 
 |-  ( `' T : ~H -onto-> ~H -> `' T : ~H --> ~H )
8 5 7 syl 
 |-  ( T e. UniOp -> `' T : ~H --> ~H )
9 8 ffvelrnda 
 |-  ( ( T e. UniOp /\ x e. ~H ) -> ( `' T ` x ) e. ~H )
10 9 adantrr 
 |-  ( ( T e. UniOp /\ ( x e. ~H /\ y e. ~H ) ) -> ( `' T ` x ) e. ~H )
11 8 ffvelrnda 
 |-  ( ( T e. UniOp /\ y e. ~H ) -> ( `' T ` y ) e. ~H )
12 11 adantrl 
 |-  ( ( T e. UniOp /\ ( x e. ~H /\ y e. ~H ) ) -> ( `' T ` y ) e. ~H )
13 unop 
 |-  ( ( T e. UniOp /\ ( `' T ` x ) e. ~H /\ ( `' T ` y ) e. ~H ) -> ( ( T ` ( `' T ` x ) ) .ih ( T ` ( `' T ` y ) ) ) = ( ( `' T ` x ) .ih ( `' T ` y ) ) )
14 6 10 12 13 syl3anc 
 |-  ( ( T e. UniOp /\ ( x e. ~H /\ y e. ~H ) ) -> ( ( T ` ( `' T ` x ) ) .ih ( T ` ( `' T ` y ) ) ) = ( ( `' T ` x ) .ih ( `' T ` y ) ) )
15 f1ocnvfv2 
 |-  ( ( T : ~H -1-1-onto-> ~H /\ x e. ~H ) -> ( T ` ( `' T ` x ) ) = x )
16 15 adantrr 
 |-  ( ( T : ~H -1-1-onto-> ~H /\ ( x e. ~H /\ y e. ~H ) ) -> ( T ` ( `' T ` x ) ) = x )
17 f1ocnvfv2 
 |-  ( ( T : ~H -1-1-onto-> ~H /\ y e. ~H ) -> ( T ` ( `' T ` y ) ) = y )
18 17 adantrl 
 |-  ( ( T : ~H -1-1-onto-> ~H /\ ( x e. ~H /\ y e. ~H ) ) -> ( T ` ( `' T ` y ) ) = y )
19 16 18 oveq12d 
 |-  ( ( T : ~H -1-1-onto-> ~H /\ ( x e. ~H /\ y e. ~H ) ) -> ( ( T ` ( `' T ` x ) ) .ih ( T ` ( `' T ` y ) ) ) = ( x .ih y ) )
20 1 19 sylan 
 |-  ( ( T e. UniOp /\ ( x e. ~H /\ y e. ~H ) ) -> ( ( T ` ( `' T ` x ) ) .ih ( T ` ( `' T ` y ) ) ) = ( x .ih y ) )
21 14 20 eqtr3d 
 |-  ( ( T e. UniOp /\ ( x e. ~H /\ y e. ~H ) ) -> ( ( `' T ` x ) .ih ( `' T ` y ) ) = ( x .ih y ) )
22 21 ralrimivva 
 |-  ( T e. UniOp -> A. x e. ~H A. y e. ~H ( ( `' T ` x ) .ih ( `' T ` y ) ) = ( x .ih y ) )
23 elunop 
 |-  ( `' T e. UniOp <-> ( `' T : ~H -onto-> ~H /\ A. x e. ~H A. y e. ~H ( ( `' T ` x ) .ih ( `' T ` y ) ) = ( x .ih y ) ) )
24 5 22 23 sylanbrc 
 |-  ( T e. UniOp -> `' T e. UniOp )