Metamath Proof Explorer

Theorem nmcopexi

Description: The norm of a continuous linear Hilbert space operator exists. Theorem 3.5(i) of Beran p. 99. (Contributed by NM, 5-Feb-2006) (Proof shortened by Mario Carneiro, 17-Nov-2013) (New usage is discouraged.)

Ref Expression
Hypotheses nmcopex.1 
|- T e. LinOp
nmcopex.2 
|- T e. ContOp
Assertion nmcopexi 
|- ( normop ` T ) e. RR

Proof

Step Hyp Ref Expression
1 nmcopex.1 
 |-  T e. LinOp
2 nmcopex.2 
 |-  T e. ContOp
3 ax-hv0cl 
 |-  0h e. ~H
4 1rp 
 |-  1 e. RR+
5 cnopc 
 |-  ( ( T e. ContOp /\ 0h e. ~H /\ 1 e. RR+ ) -> E. y e. RR+ A. z e. ~H ( ( normh ` ( z -h 0h ) ) < y -> ( normh ` ( ( T ` z ) -h ( T ` 0h ) ) ) < 1 ) )
6 2 3 4 5 mp3an 
 |-  E. y e. RR+ A. z e. ~H ( ( normh ` ( z -h 0h ) ) < y -> ( normh ` ( ( T ` z ) -h ( T ` 0h ) ) ) < 1 )
7 hvsub0 
 |-  ( z e. ~H -> ( z -h 0h ) = z )
8 7 fveq2d 
 |-  ( z e. ~H -> ( normh ` ( z -h 0h ) ) = ( normh ` z ) )
9 8 breq1d 
 |-  ( z e. ~H -> ( ( normh ` ( z -h 0h ) ) < y <-> ( normh ` z ) < y ) )
10 1 lnop0i 
 |-  ( T ` 0h ) = 0h
11 10 oveq2i 
 |-  ( ( T ` z ) -h ( T ` 0h ) ) = ( ( T ` z ) -h 0h )
12 1 lnopfi 
 |-  T : ~H --> ~H
13 12 ffvelcdmi 
 |-  ( z e. ~H -> ( T ` z ) e. ~H )
14 hvsub0 
 |-  ( ( T ` z ) e. ~H -> ( ( T ` z ) -h 0h ) = ( T ` z ) )
15 13 14 syl 
 |-  ( z e. ~H -> ( ( T ` z ) -h 0h ) = ( T ` z ) )
16 11 15 eqtrid 
 |-  ( z e. ~H -> ( ( T ` z ) -h ( T ` 0h ) ) = ( T ` z ) )
17 16 fveq2d 
 |-  ( z e. ~H -> ( normh ` ( ( T ` z ) -h ( T ` 0h ) ) ) = ( normh ` ( T ` z ) ) )
18 17 breq1d 
 |-  ( z e. ~H -> ( ( normh ` ( ( T ` z ) -h ( T ` 0h ) ) ) < 1 <-> ( normh ` ( T ` z ) ) < 1 ) )
19 9 18 imbi12d 
 |-  ( z e. ~H -> ( ( ( normh ` ( z -h 0h ) ) < y -> ( normh ` ( ( T ` z ) -h ( T ` 0h ) ) ) < 1 ) <-> ( ( normh ` z ) < y -> ( normh ` ( T ` z ) ) < 1 ) ) )
20 19 ralbiia 
 |-  ( A. z e. ~H ( ( normh ` ( z -h 0h ) ) < y -> ( normh ` ( ( T ` z ) -h ( T ` 0h ) ) ) < 1 ) <-> A. z e. ~H ( ( normh ` z ) < y -> ( normh ` ( T ` z ) ) < 1 ) )
21 20 rexbii 
 |-  ( E. y e. RR+ A. z e. ~H ( ( normh ` ( z -h 0h ) ) < y -> ( normh ` ( ( T ` z ) -h ( T ` 0h ) ) ) < 1 ) <-> E. y e. RR+ A. z e. ~H ( ( normh ` z ) < y -> ( normh ` ( T ` z ) ) < 1 ) )
22 6 21 mpbi 
 |-  E. y e. RR+ A. z e. ~H ( ( normh ` z ) < y -> ( normh ` ( T ` z ) ) < 1 )
23 nmopval 
 |-  ( T : ~H --> ~H -> ( normop ` T ) = sup ( { m | E. x e. ~H ( ( normh ` x ) <_ 1 /\ m = ( normh ` ( T ` x ) ) ) } , RR* , < ) )
24 12 23 ax-mp 
 |-  ( normop ` T ) = sup ( { m | E. x e. ~H ( ( normh ` x ) <_ 1 /\ m = ( normh ` ( T ` x ) ) ) } , RR* , < )
25 12 ffvelcdmi 
 |-  ( x e. ~H -> ( T ` x ) e. ~H )
26 normcl 
 |-  ( ( T ` x ) e. ~H -> ( normh ` ( T ` x ) ) e. RR )
27 25 26 syl 
 |-  ( x e. ~H -> ( normh ` ( T ` x ) ) e. RR )
28 10 fveq2i 
 |-  ( normh ` ( T ` 0h ) ) = ( normh ` 0h )
29 norm0 
 |-  ( normh ` 0h ) = 0
30 28 29 eqtri 
 |-  ( normh ` ( T ` 0h ) ) = 0
31 rpcn 
 |-  ( ( y / 2 ) e. RR+ -> ( y / 2 ) e. CC )
32 1 lnopmuli 
 |-  ( ( ( y / 2 ) e. CC /\ x e. ~H ) -> ( T ` ( ( y / 2 ) .h x ) ) = ( ( y / 2 ) .h ( T ` x ) ) )
33 31 32 sylan 
 |-  ( ( ( y / 2 ) e. RR+ /\ x e. ~H ) -> ( T ` ( ( y / 2 ) .h x ) ) = ( ( y / 2 ) .h ( T ` x ) ) )
34 33 fveq2d 
 |-  ( ( ( y / 2 ) e. RR+ /\ x e. ~H ) -> ( normh ` ( T ` ( ( y / 2 ) .h x ) ) ) = ( normh ` ( ( y / 2 ) .h ( T ` x ) ) ) )
35 norm-iii 
 |-  ( ( ( y / 2 ) e. CC /\ ( T ` x ) e. ~H ) -> ( normh ` ( ( y / 2 ) .h ( T ` x ) ) ) = ( ( abs ` ( y / 2 ) ) x. ( normh ` ( T ` x ) ) ) )
36 31 25 35 syl2an 
 |-  ( ( ( y / 2 ) e. RR+ /\ x e. ~H ) -> ( normh ` ( ( y / 2 ) .h ( T ` x ) ) ) = ( ( abs ` ( y / 2 ) ) x. ( normh ` ( T ` x ) ) ) )
37 rpre 
 |-  ( ( y / 2 ) e. RR+ -> ( y / 2 ) e. RR )
38 rpge0 
 |-  ( ( y / 2 ) e. RR+ -> 0 <_ ( y / 2 ) )
39 37 38 absidd 
 |-  ( ( y / 2 ) e. RR+ -> ( abs ` ( y / 2 ) ) = ( y / 2 ) )
40 39 adantr 
 |-  ( ( ( y / 2 ) e. RR+ /\ x e. ~H ) -> ( abs ` ( y / 2 ) ) = ( y / 2 ) )
41 40 oveq1d 
 |-  ( ( ( y / 2 ) e. RR+ /\ x e. ~H ) -> ( ( abs ` ( y / 2 ) ) x. ( normh ` ( T ` x ) ) ) = ( ( y / 2 ) x. ( normh ` ( T ` x ) ) ) )
42 34 36 41 3eqtrrd 
 |-  ( ( ( y / 2 ) e. RR+ /\ x e. ~H ) -> ( ( y / 2 ) x. ( normh ` ( T ` x ) ) ) = ( normh ` ( T ` ( ( y / 2 ) .h x ) ) ) )
43 22 24 27 30 42 nmcexi 
 |-  ( normop ` T ) e. RR