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

Metamath Proof Explorer

Theorem elunop2

Description: An operator is unitary iff it is linear, onto, and idempotent in the norm. Similar to theorem in AkhiezerGlazman p. 73, and its converse. (Contributed by NM, 24-Feb-2006) (New usage is discouraged.)

Ref Expression
Assertion elunop2 
|- ( T e. UniOp <-> ( T e. LinOp /\ T : ~H -onto-> ~H /\ A. x e. ~H ( normh ` ( T ` x ) ) = ( normh ` x ) ) )

Proof

Step Hyp Ref Expression
1 unoplin 
 |-  ( T e. UniOp -> T e. LinOp )
2 elunop 
 |-  ( T e. UniOp <-> ( T : ~H -onto-> ~H /\ A. x e. ~H A. y e. ~H ( ( T ` x ) .ih ( T ` y ) ) = ( x .ih y ) ) )
3 2 simplbi 
 |-  ( T e. UniOp -> T : ~H -onto-> ~H )
4 unopnorm 
 |-  ( ( T e. UniOp /\ x e. ~H ) -> ( normh ` ( T ` x ) ) = ( normh ` x ) )
5 4 ralrimiva 
 |-  ( T e. UniOp -> A. x e. ~H ( normh ` ( T ` x ) ) = ( normh ` x ) )
6 1 3 5 3jca 
 |-  ( T e. UniOp -> ( T e. LinOp /\ T : ~H -onto-> ~H /\ A. x e. ~H ( normh ` ( T ` x ) ) = ( normh ` x ) ) )
7 eleq1 
 |-  ( T = if ( ( T e. LinOp /\ T : ~H -onto-> ~H /\ A. x e. ~H ( normh ` ( T ` x ) ) = ( normh ` x ) ) , T , ( _I |` ~H ) ) -> ( T e. UniOp <-> if ( ( T e. LinOp /\ T : ~H -onto-> ~H /\ A. x e. ~H ( normh ` ( T ` x ) ) = ( normh ` x ) ) , T , ( _I |` ~H ) ) e. UniOp ) )
8 eleq1 
 |-  ( T = if ( ( T e. LinOp /\ T : ~H -onto-> ~H /\ A. x e. ~H ( normh ` ( T ` x ) ) = ( normh ` x ) ) , T , ( _I |` ~H ) ) -> ( T e. LinOp <-> if ( ( T e. LinOp /\ T : ~H -onto-> ~H /\ A. x e. ~H ( normh ` ( T ` x ) ) = ( normh ` x ) ) , T , ( _I |` ~H ) ) e. LinOp ) )
9 foeq1 
 |-  ( T = if ( ( T e. LinOp /\ T : ~H -onto-> ~H /\ A. x e. ~H ( normh ` ( T ` x ) ) = ( normh ` x ) ) , T , ( _I |` ~H ) ) -> ( T : ~H -onto-> ~H <-> if ( ( T e. LinOp /\ T : ~H -onto-> ~H /\ A. x e. ~H ( normh ` ( T ` x ) ) = ( normh ` x ) ) , T , ( _I |` ~H ) ) : ~H -onto-> ~H ) )
10 2fveq3 
 |-  ( x = y -> ( normh ` ( T ` x ) ) = ( normh ` ( T ` y ) ) )
11 fveq2 
 |-  ( x = y -> ( normh ` x ) = ( normh ` y ) )
12 10 11 eqeq12d 
 |-  ( x = y -> ( ( normh ` ( T ` x ) ) = ( normh ` x ) <-> ( normh ` ( T ` y ) ) = ( normh ` y ) ) )
13 12 cbvralvw 
 |-  ( A. x e. ~H ( normh ` ( T ` x ) ) = ( normh ` x ) <-> A. y e. ~H ( normh ` ( T ` y ) ) = ( normh ` y ) )
14 fveq1 
 |-  ( T = if ( ( T e. LinOp /\ T : ~H -onto-> ~H /\ A. x e. ~H ( normh ` ( T ` x ) ) = ( normh ` x ) ) , T , ( _I |` ~H ) ) -> ( T ` y ) = ( if ( ( T e. LinOp /\ T : ~H -onto-> ~H /\ A. x e. ~H ( normh ` ( T ` x ) ) = ( normh ` x ) ) , T , ( _I |` ~H ) ) ` y ) )
15 14 fveqeq2d 
 |-  ( T = if ( ( T e. LinOp /\ T : ~H -onto-> ~H /\ A. x e. ~H ( normh ` ( T ` x ) ) = ( normh ` x ) ) , T , ( _I |` ~H ) ) -> ( ( normh ` ( T ` y ) ) = ( normh ` y ) <-> ( normh ` ( if ( ( T e. LinOp /\ T : ~H -onto-> ~H /\ A. x e. ~H ( normh ` ( T ` x ) ) = ( normh ` x ) ) , T , ( _I |` ~H ) ) ` y ) ) = ( normh ` y ) ) )
16 15 ralbidv 
 |-  ( T = if ( ( T e. LinOp /\ T : ~H -onto-> ~H /\ A. x e. ~H ( normh ` ( T ` x ) ) = ( normh ` x ) ) , T , ( _I |` ~H ) ) -> ( A. y e. ~H ( normh ` ( T ` y ) ) = ( normh ` y ) <-> A. y e. ~H ( normh ` ( if ( ( T e. LinOp /\ T : ~H -onto-> ~H /\ A. x e. ~H ( normh ` ( T ` x ) ) = ( normh ` x ) ) , T , ( _I |` ~H ) ) ` y ) ) = ( normh ` y ) ) )
17 13 16 bitrid 
 |-  ( T = if ( ( T e. LinOp /\ T : ~H -onto-> ~H /\ A. x e. ~H ( normh ` ( T ` x ) ) = ( normh ` x ) ) , T , ( _I |` ~H ) ) -> ( A. x e. ~H ( normh ` ( T ` x ) ) = ( normh ` x ) <-> A. y e. ~H ( normh ` ( if ( ( T e. LinOp /\ T : ~H -onto-> ~H /\ A. x e. ~H ( normh ` ( T ` x ) ) = ( normh ` x ) ) , T , ( _I |` ~H ) ) ` y ) ) = ( normh ` y ) ) )
18 8 9 17 3anbi123d 
 |-  ( T = if ( ( T e. LinOp /\ T : ~H -onto-> ~H /\ A. x e. ~H ( normh ` ( T ` x ) ) = ( normh ` x ) ) , T , ( _I |` ~H ) ) -> ( ( T e. LinOp /\ T : ~H -onto-> ~H /\ A. x e. ~H ( normh ` ( T ` x ) ) = ( normh ` x ) ) <-> ( if ( ( T e. LinOp /\ T : ~H -onto-> ~H /\ A. x e. ~H ( normh ` ( T ` x ) ) = ( normh ` x ) ) , T , ( _I |` ~H ) ) e. LinOp /\ if ( ( T e. LinOp /\ T : ~H -onto-> ~H /\ A. x e. ~H ( normh ` ( T ` x ) ) = ( normh ` x ) ) , T , ( _I |` ~H ) ) : ~H -onto-> ~H /\ A. y e. ~H ( normh ` ( if ( ( T e. LinOp /\ T : ~H -onto-> ~H /\ A. x e. ~H ( normh ` ( T ` x ) ) = ( normh ` x ) ) , T , ( _I |` ~H ) ) ` y ) ) = ( normh ` y ) ) ) )
19 eleq1 
 |-  ( ( _I |` ~H ) = if ( ( T e. LinOp /\ T : ~H -onto-> ~H /\ A. x e. ~H ( normh ` ( T ` x ) ) = ( normh ` x ) ) , T , ( _I |` ~H ) ) -> ( ( _I |` ~H ) e. LinOp <-> if ( ( T e. LinOp /\ T : ~H -onto-> ~H /\ A. x e. ~H ( normh ` ( T ` x ) ) = ( normh ` x ) ) , T , ( _I |` ~H ) ) e. LinOp ) )
20 foeq1 
 |-  ( ( _I |` ~H ) = if ( ( T e. LinOp /\ T : ~H -onto-> ~H /\ A. x e. ~H ( normh ` ( T ` x ) ) = ( normh ` x ) ) , T , ( _I |` ~H ) ) -> ( ( _I |` ~H ) : ~H -onto-> ~H <-> if ( ( T e. LinOp /\ T : ~H -onto-> ~H /\ A. x e. ~H ( normh ` ( T ` x ) ) = ( normh ` x ) ) , T , ( _I |` ~H ) ) : ~H -onto-> ~H ) )
21 fveq1 
 |-  ( ( _I |` ~H ) = if ( ( T e. LinOp /\ T : ~H -onto-> ~H /\ A. x e. ~H ( normh ` ( T ` x ) ) = ( normh ` x ) ) , T , ( _I |` ~H ) ) -> ( ( _I |` ~H ) ` y ) = ( if ( ( T e. LinOp /\ T : ~H -onto-> ~H /\ A. x e. ~H ( normh ` ( T ` x ) ) = ( normh ` x ) ) , T , ( _I |` ~H ) ) ` y ) )
22 21 fveqeq2d 
 |-  ( ( _I |` ~H ) = if ( ( T e. LinOp /\ T : ~H -onto-> ~H /\ A. x e. ~H ( normh ` ( T ` x ) ) = ( normh ` x ) ) , T , ( _I |` ~H ) ) -> ( ( normh ` ( ( _I |` ~H ) ` y ) ) = ( normh ` y ) <-> ( normh ` ( if ( ( T e. LinOp /\ T : ~H -onto-> ~H /\ A. x e. ~H ( normh ` ( T ` x ) ) = ( normh ` x ) ) , T , ( _I |` ~H ) ) ` y ) ) = ( normh ` y ) ) )
23 22 ralbidv 
 |-  ( ( _I |` ~H ) = if ( ( T e. LinOp /\ T : ~H -onto-> ~H /\ A. x e. ~H ( normh ` ( T ` x ) ) = ( normh ` x ) ) , T , ( _I |` ~H ) ) -> ( A. y e. ~H ( normh ` ( ( _I |` ~H ) ` y ) ) = ( normh ` y ) <-> A. y e. ~H ( normh ` ( if ( ( T e. LinOp /\ T : ~H -onto-> ~H /\ A. x e. ~H ( normh ` ( T ` x ) ) = ( normh ` x ) ) , T , ( _I |` ~H ) ) ` y ) ) = ( normh ` y ) ) )
24 19 20 23 3anbi123d 
 |-  ( ( _I |` ~H ) = if ( ( T e. LinOp /\ T : ~H -onto-> ~H /\ A. x e. ~H ( normh ` ( T ` x ) ) = ( normh ` x ) ) , T , ( _I |` ~H ) ) -> ( ( ( _I |` ~H ) e. LinOp /\ ( _I |` ~H ) : ~H -onto-> ~H /\ A. y e. ~H ( normh ` ( ( _I |` ~H ) ` y ) ) = ( normh ` y ) ) <-> ( if ( ( T e. LinOp /\ T : ~H -onto-> ~H /\ A. x e. ~H ( normh ` ( T ` x ) ) = ( normh ` x ) ) , T , ( _I |` ~H ) ) e. LinOp /\ if ( ( T e. LinOp /\ T : ~H -onto-> ~H /\ A. x e. ~H ( normh ` ( T ` x ) ) = ( normh ` x ) ) , T , ( _I |` ~H ) ) : ~H -onto-> ~H /\ A. y e. ~H ( normh ` ( if ( ( T e. LinOp /\ T : ~H -onto-> ~H /\ A. x e. ~H ( normh ` ( T ` x ) ) = ( normh ` x ) ) , T , ( _I |` ~H ) ) ` y ) ) = ( normh ` y ) ) ) )
25 idlnop 
 |-  ( _I |` ~H ) e. LinOp
26 f1oi 
 |-  ( _I |` ~H ) : ~H -1-1-onto-> ~H
27 f1ofo 
 |-  ( ( _I |` ~H ) : ~H -1-1-onto-> ~H -> ( _I |` ~H ) : ~H -onto-> ~H )
28 26 27 ax-mp 
 |-  ( _I |` ~H ) : ~H -onto-> ~H
29 fvresi 
 |-  ( y e. ~H -> ( ( _I |` ~H ) ` y ) = y )
30 29 fveq2d 
 |-  ( y e. ~H -> ( normh ` ( ( _I |` ~H ) ` y ) ) = ( normh ` y ) )
31 30 rgen 
 |-  A. y e. ~H ( normh ` ( ( _I |` ~H ) ` y ) ) = ( normh ` y )
32 25 28 31 3pm3.2i 
 |-  ( ( _I |` ~H ) e. LinOp /\ ( _I |` ~H ) : ~H -onto-> ~H /\ A. y e. ~H ( normh ` ( ( _I |` ~H ) ` y ) ) = ( normh ` y ) )
33 18 24 32 elimhyp 
 |-  ( if ( ( T e. LinOp /\ T : ~H -onto-> ~H /\ A. x e. ~H ( normh ` ( T ` x ) ) = ( normh ` x ) ) , T , ( _I |` ~H ) ) e. LinOp /\ if ( ( T e. LinOp /\ T : ~H -onto-> ~H /\ A. x e. ~H ( normh ` ( T ` x ) ) = ( normh ` x ) ) , T , ( _I |` ~H ) ) : ~H -onto-> ~H /\ A. y e. ~H ( normh ` ( if ( ( T e. LinOp /\ T : ~H -onto-> ~H /\ A. x e. ~H ( normh ` ( T ` x ) ) = ( normh ` x ) ) , T , ( _I |` ~H ) ) ` y ) ) = ( normh ` y ) )
34 33 simp1i 
 |-  if ( ( T e. LinOp /\ T : ~H -onto-> ~H /\ A. x e. ~H ( normh ` ( T ` x ) ) = ( normh ` x ) ) , T , ( _I |` ~H ) ) e. LinOp
35 33 simp2i 
 |-  if ( ( T e. LinOp /\ T : ~H -onto-> ~H /\ A. x e. ~H ( normh ` ( T ` x ) ) = ( normh ` x ) ) , T , ( _I |` ~H ) ) : ~H -onto-> ~H
36 33 simp3i 
 |-  A. y e. ~H ( normh ` ( if ( ( T e. LinOp /\ T : ~H -onto-> ~H /\ A. x e. ~H ( normh ` ( T ` x ) ) = ( normh ` x ) ) , T , ( _I |` ~H ) ) ` y ) ) = ( normh ` y )
37 34 35 36 lnopunii 
 |-  if ( ( T e. LinOp /\ T : ~H -onto-> ~H /\ A. x e. ~H ( normh ` ( T ` x ) ) = ( normh ` x ) ) , T , ( _I |` ~H ) ) e. UniOp
38 7 37 dedth 
 |-  ( ( T e. LinOp /\ T : ~H -onto-> ~H /\ A. x e. ~H ( normh ` ( T ` x ) ) = ( normh ` x ) ) -> T e. UniOp )
39 6 38 impbii 
 |-  ( T e. UniOp <-> ( T e. LinOp /\ T : ~H -onto-> ~H /\ A. x e. ~H ( normh ` ( T ` x ) ) = ( normh ` x ) ) )