Metamath Proof Explorer

Theorem nmopun

Description: Norm of a unitary Hilbert space operator. (Contributed by NM, 25-Feb-2006) (New usage is discouraged.)

Ref Expression
Assertion nmopun 
|- ( ( ~H =/= 0H /\ T e. UniOp ) -> ( normop ` T ) = 1 )

Proof

Step Hyp Ref Expression
1 unoplin 
 |-  ( T e. UniOp -> T e. LinOp )
2 lnopf 
 |-  ( T e. LinOp -> T : ~H --> ~H )
3 1 2 syl 
 |-  ( T e. UniOp -> T : ~H --> ~H )
4 nmopval 
 |-  ( T : ~H --> ~H -> ( normop ` T ) = sup ( { x | E. y e. ~H ( ( normh ` y ) <_ 1 /\ x = ( normh ` ( T ` y ) ) ) } , RR* , < ) )
5 3 4 syl 
 |-  ( T e. UniOp -> ( normop ` T ) = sup ( { x | E. y e. ~H ( ( normh ` y ) <_ 1 /\ x = ( normh ` ( T ` y ) ) ) } , RR* , < ) )
6 5 adantl 
 |-  ( ( ~H =/= 0H /\ T e. UniOp ) -> ( normop ` T ) = sup ( { x | E. y e. ~H ( ( normh ` y ) <_ 1 /\ x = ( normh ` ( T ` y ) ) ) } , RR* , < ) )
7 nmopsetretHIL 
 |-  ( T : ~H --> ~H -> { x | E. y e. ~H ( ( normh ` y ) <_ 1 /\ x = ( normh ` ( T ` y ) ) ) } C_ RR )
8 ressxr 
 |-  RR C_ RR*
9 7 8 sstrdi 
 |-  ( T : ~H --> ~H -> { x | E. y e. ~H ( ( normh ` y ) <_ 1 /\ x = ( normh ` ( T ` y ) ) ) } C_ RR* )
10 3 9 syl 
 |-  ( T e. UniOp -> { x | E. y e. ~H ( ( normh ` y ) <_ 1 /\ x = ( normh ` ( T ` y ) ) ) } C_ RR* )
11 10 adantl 
 |-  ( ( ~H =/= 0H /\ T e. UniOp ) -> { x | E. y e. ~H ( ( normh ` y ) <_ 1 /\ x = ( normh ` ( T ` y ) ) ) } C_ RR* )
12 1xr 
 |-  1 e. RR*
13 11 12 jctir 
 |-  ( ( ~H =/= 0H /\ T e. UniOp ) -> ( { x | E. y e. ~H ( ( normh ` y ) <_ 1 /\ x = ( normh ` ( T ` y ) ) ) } C_ RR* /\ 1 e. RR* ) )
14 vex 
 |-  z e. _V
15 eqeq1 
 |-  ( x = z -> ( x = ( normh ` ( T ` y ) ) <-> z = ( normh ` ( T ` y ) ) ) )
16 15 anbi2d 
 |-  ( x = z -> ( ( ( normh ` y ) <_ 1 /\ x = ( normh ` ( T ` y ) ) ) <-> ( ( normh ` y ) <_ 1 /\ z = ( normh ` ( T ` y ) ) ) ) )
17 16 rexbidv 
 |-  ( x = z -> ( E. y e. ~H ( ( normh ` y ) <_ 1 /\ x = ( normh ` ( T ` y ) ) ) <-> E. y e. ~H ( ( normh ` y ) <_ 1 /\ z = ( normh ` ( T ` y ) ) ) ) )
18 14 17 elab 
 |-  ( z e. { x | E. y e. ~H ( ( normh ` y ) <_ 1 /\ x = ( normh ` ( T ` y ) ) ) } <-> E. y e. ~H ( ( normh ` y ) <_ 1 /\ z = ( normh ` ( T ` y ) ) ) )
19 unopnorm 
 |-  ( ( T e. UniOp /\ y e. ~H ) -> ( normh ` ( T ` y ) ) = ( normh ` y ) )
20 19 eqeq2d 
 |-  ( ( T e. UniOp /\ y e. ~H ) -> ( z = ( normh ` ( T ` y ) ) <-> z = ( normh ` y ) ) )
21 20 anbi2d 
 |-  ( ( T e. UniOp /\ y e. ~H ) -> ( ( ( normh ` y ) <_ 1 /\ z = ( normh ` ( T ` y ) ) ) <-> ( ( normh ` y ) <_ 1 /\ z = ( normh ` y ) ) ) )
22 breq1 
 |-  ( z = ( normh ` y ) -> ( z <_ 1 <-> ( normh ` y ) <_ 1 ) )
23 22 biimparc 
 |-  ( ( ( normh ` y ) <_ 1 /\ z = ( normh ` y ) ) -> z <_ 1 )
24 21 23 syl6bi 
 |-  ( ( T e. UniOp /\ y e. ~H ) -> ( ( ( normh ` y ) <_ 1 /\ z = ( normh ` ( T ` y ) ) ) -> z <_ 1 ) )
25 24 rexlimdva 
 |-  ( T e. UniOp -> ( E. y e. ~H ( ( normh ` y ) <_ 1 /\ z = ( normh ` ( T ` y ) ) ) -> z <_ 1 ) )
26 25 imp 
 |-  ( ( T e. UniOp /\ E. y e. ~H ( ( normh ` y ) <_ 1 /\ z = ( normh ` ( T ` y ) ) ) ) -> z <_ 1 )
27 18 26 sylan2b 
 |-  ( ( T e. UniOp /\ z e. { x | E. y e. ~H ( ( normh ` y ) <_ 1 /\ x = ( normh ` ( T ` y ) ) ) } ) -> z <_ 1 )
28 27 ralrimiva 
 |-  ( T e. UniOp -> A. z e. { x | E. y e. ~H ( ( normh ` y ) <_ 1 /\ x = ( normh ` ( T ` y ) ) ) } z <_ 1 )
29 28 adantl 
 |-  ( ( ~H =/= 0H /\ T e. UniOp ) -> A. z e. { x | E. y e. ~H ( ( normh ` y ) <_ 1 /\ x = ( normh ` ( T ` y ) ) ) } z <_ 1 )
30 hne0 
 |-  ( ~H =/= 0H <-> E. y e. ~H y =/= 0h )
31 norm1hex 
 |-  ( E. y e. ~H y =/= 0h <-> E. y e. ~H ( normh ` y ) = 1 )
32 30 31 sylbb 
 |-  ( ~H =/= 0H -> E. y e. ~H ( normh ` y ) = 1 )
33 32 adantr 
 |-  ( ( ~H =/= 0H /\ T e. UniOp ) -> E. y e. ~H ( normh ` y ) = 1 )
34 1le1 
 |-  1 <_ 1
35 breq1 
 |-  ( ( normh ` y ) = 1 -> ( ( normh ` y ) <_ 1 <-> 1 <_ 1 ) )
36 34 35 mpbiri 
 |-  ( ( normh ` y ) = 1 -> ( normh ` y ) <_ 1 )
37 36 a1i 
 |-  ( ( T e. UniOp /\ y e. ~H ) -> ( ( normh ` y ) = 1 -> ( normh ` y ) <_ 1 ) )
38 19 adantr 
 |-  ( ( ( T e. UniOp /\ y e. ~H ) /\ ( normh ` y ) = 1 ) -> ( normh ` ( T ` y ) ) = ( normh ` y ) )
39 eqeq2 
 |-  ( ( normh ` y ) = 1 -> ( ( normh ` ( T ` y ) ) = ( normh ` y ) <-> ( normh ` ( T ` y ) ) = 1 ) )
40 39 adantl 
 |-  ( ( ( T e. UniOp /\ y e. ~H ) /\ ( normh ` y ) = 1 ) -> ( ( normh ` ( T ` y ) ) = ( normh ` y ) <-> ( normh ` ( T ` y ) ) = 1 ) )
41 38 40 mpbid 
 |-  ( ( ( T e. UniOp /\ y e. ~H ) /\ ( normh ` y ) = 1 ) -> ( normh ` ( T ` y ) ) = 1 )
42 41 eqcomd 
 |-  ( ( ( T e. UniOp /\ y e. ~H ) /\ ( normh ` y ) = 1 ) -> 1 = ( normh ` ( T ` y ) ) )
43 42 ex 
 |-  ( ( T e. UniOp /\ y e. ~H ) -> ( ( normh ` y ) = 1 -> 1 = ( normh ` ( T ` y ) ) ) )
44 37 43 jcad 
 |-  ( ( T e. UniOp /\ y e. ~H ) -> ( ( normh ` y ) = 1 -> ( ( normh ` y ) <_ 1 /\ 1 = ( normh ` ( T ` y ) ) ) ) )
45 44 adantll 
 |-  ( ( ( ~H =/= 0H /\ T e. UniOp ) /\ y e. ~H ) -> ( ( normh ` y ) = 1 -> ( ( normh ` y ) <_ 1 /\ 1 = ( normh ` ( T ` y ) ) ) ) )
46 45 reximdva 
 |-  ( ( ~H =/= 0H /\ T e. UniOp ) -> ( E. y e. ~H ( normh ` y ) = 1 -> E. y e. ~H ( ( normh ` y ) <_ 1 /\ 1 = ( normh ` ( T ` y ) ) ) ) )
47 33 46 mpd 
 |-  ( ( ~H =/= 0H /\ T e. UniOp ) -> E. y e. ~H ( ( normh ` y ) <_ 1 /\ 1 = ( normh ` ( T ` y ) ) ) )
48 1ex 
 |-  1 e. _V
49 eqeq1 
 |-  ( x = 1 -> ( x = ( normh ` ( T ` y ) ) <-> 1 = ( normh ` ( T ` y ) ) ) )
50 49 anbi2d 
 |-  ( x = 1 -> ( ( ( normh ` y ) <_ 1 /\ x = ( normh ` ( T ` y ) ) ) <-> ( ( normh ` y ) <_ 1 /\ 1 = ( normh ` ( T ` y ) ) ) ) )
51 50 rexbidv 
 |-  ( x = 1 -> ( E. y e. ~H ( ( normh ` y ) <_ 1 /\ x = ( normh ` ( T ` y ) ) ) <-> E. y e. ~H ( ( normh ` y ) <_ 1 /\ 1 = ( normh ` ( T ` y ) ) ) ) )
52 48 51 elab 
 |-  ( 1 e. { x | E. y e. ~H ( ( normh ` y ) <_ 1 /\ x = ( normh ` ( T ` y ) ) ) } <-> E. y e. ~H ( ( normh ` y ) <_ 1 /\ 1 = ( normh ` ( T ` y ) ) ) )
53 47 52 sylibr 
 |-  ( ( ~H =/= 0H /\ T e. UniOp ) -> 1 e. { x | E. y e. ~H ( ( normh ` y ) <_ 1 /\ x = ( normh ` ( T ` y ) ) ) } )
54 53 adantr 
 |-  ( ( ( ~H =/= 0H /\ T e. UniOp ) /\ z e. RR ) -> 1 e. { x | E. y e. ~H ( ( normh ` y ) <_ 1 /\ x = ( normh ` ( T ` y ) ) ) } )
55 breq2 
 |-  ( w = 1 -> ( z < w <-> z < 1 ) )
56 55 rspcev 
 |-  ( ( 1 e. { x | E. y e. ~H ( ( normh ` y ) <_ 1 /\ x = ( normh ` ( T ` y ) ) ) } /\ z < 1 ) -> E. w e. { x | E. y e. ~H ( ( normh ` y ) <_ 1 /\ x = ( normh ` ( T ` y ) ) ) } z < w )
57 54 56 sylan 
 |-  ( ( ( ( ~H =/= 0H /\ T e. UniOp ) /\ z e. RR ) /\ z < 1 ) -> E. w e. { x | E. y e. ~H ( ( normh ` y ) <_ 1 /\ x = ( normh ` ( T ` y ) ) ) } z < w )
58 57 ex 
 |-  ( ( ( ~H =/= 0H /\ T e. UniOp ) /\ z e. RR ) -> ( z < 1 -> E. w e. { x | E. y e. ~H ( ( normh ` y ) <_ 1 /\ x = ( normh ` ( T ` y ) ) ) } z < w ) )
59 58 ralrimiva 
 |-  ( ( ~H =/= 0H /\ T e. UniOp ) -> A. z e. RR ( z < 1 -> E. w e. { x | E. y e. ~H ( ( normh ` y ) <_ 1 /\ x = ( normh ` ( T ` y ) ) ) } z < w ) )
60 supxr2 
 |-  ( ( ( { x | E. y e. ~H ( ( normh ` y ) <_ 1 /\ x = ( normh ` ( T ` y ) ) ) } C_ RR* /\ 1 e. RR* ) /\ ( A. z e. { x | E. y e. ~H ( ( normh ` y ) <_ 1 /\ x = ( normh ` ( T ` y ) ) ) } z <_ 1 /\ A. z e. RR ( z < 1 -> E. w e. { x | E. y e. ~H ( ( normh ` y ) <_ 1 /\ x = ( normh ` ( T ` y ) ) ) } z < w ) ) ) -> sup ( { x | E. y e. ~H ( ( normh ` y ) <_ 1 /\ x = ( normh ` ( T ` y ) ) ) } , RR* , < ) = 1 )
61 13 29 59 60 syl12anc 
 |-  ( ( ~H =/= 0H /\ T e. UniOp ) -> sup ( { x | E. y e. ~H ( ( normh ` y ) <_ 1 /\ x = ( normh ` ( T ` y ) ) ) } , RR* , < ) = 1 )
62 6 61 eqtrd 
 |-  ( ( ~H =/= 0H /\ T e. UniOp ) -> ( normop ` T ) = 1 )