Metamath Proof Explorer

Theorem nmcfnexi

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

Ref Expression
Hypotheses nmcfnex.1 
|- T e. LinFn
nmcfnex.2 
|- T e. ContFn
Assertion nmcfnexi 
|- ( normfn ` T ) e. RR

Proof

Step Hyp Ref Expression
1 nmcfnex.1 
 |-  T e. LinFn
2 nmcfnex.2 
 |-  T e. ContFn
3 ax-hv0cl 
 |-  0h e. ~H
4 1rp 
 |-  1 e. RR+
5 cnfnc 
 |-  ( ( T e. ContFn /\ 0h e. ~H /\ 1 e. RR+ ) -> E. y e. RR+ A. z e. ~H ( ( normh ` ( z -h 0h ) ) < y -> ( abs ` ( ( T ` z ) - ( T ` 0h ) ) ) < 1 ) )
6 2 3 4 5 mp3an 
 |-  E. y e. RR+ A. z e. ~H ( ( normh ` ( z -h 0h ) ) < y -> ( abs ` ( ( T ` z ) - ( 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 lnfn0i 
 |-  ( T ` 0h ) = 0
11 10 oveq2i 
 |-  ( ( T ` z ) - ( T ` 0h ) ) = ( ( T ` z ) - 0 )
12 1 lnfnfi 
 |-  T : ~H --> CC
13 12 ffvelrni 
 |-  ( z e. ~H -> ( T ` z ) e. CC )
14 13 subid1d 
 |-  ( z e. ~H -> ( ( T ` z ) - 0 ) = ( T ` z ) )
15 11 14 eqtrid 
 |-  ( z e. ~H -> ( ( T ` z ) - ( T ` 0h ) ) = ( T ` z ) )
16 15 fveq2d 
 |-  ( z e. ~H -> ( abs ` ( ( T ` z ) - ( T ` 0h ) ) ) = ( abs ` ( T ` z ) ) )
17 16 breq1d 
 |-  ( z e. ~H -> ( ( abs ` ( ( T ` z ) - ( T ` 0h ) ) ) < 1 <-> ( abs ` ( T ` z ) ) < 1 ) )
18 9 17 imbi12d 
 |-  ( z e. ~H -> ( ( ( normh ` ( z -h 0h ) ) < y -> ( abs ` ( ( T ` z ) - ( T ` 0h ) ) ) < 1 ) <-> ( ( normh ` z ) < y -> ( abs ` ( T ` z ) ) < 1 ) ) )
19 18 ralbiia 
 |-  ( A. z e. ~H ( ( normh ` ( z -h 0h ) ) < y -> ( abs ` ( ( T ` z ) - ( T ` 0h ) ) ) < 1 ) <-> A. z e. ~H ( ( normh ` z ) < y -> ( abs ` ( T ` z ) ) < 1 ) )
20 19 rexbii 
 |-  ( E. y e. RR+ A. z e. ~H ( ( normh ` ( z -h 0h ) ) < y -> ( abs ` ( ( T ` z ) - ( T ` 0h ) ) ) < 1 ) <-> E. y e. RR+ A. z e. ~H ( ( normh ` z ) < y -> ( abs ` ( T ` z ) ) < 1 ) )
21 6 20 mpbi 
 |-  E. y e. RR+ A. z e. ~H ( ( normh ` z ) < y -> ( abs ` ( T ` z ) ) < 1 )
22 nmfnval 
 |-  ( T : ~H --> CC -> ( normfn ` T ) = sup ( { m | E. x e. ~H ( ( normh ` x ) <_ 1 /\ m = ( abs ` ( T ` x ) ) ) } , RR* , < ) )
23 12 22 ax-mp 
 |-  ( normfn ` T ) = sup ( { m | E. x e. ~H ( ( normh ` x ) <_ 1 /\ m = ( abs ` ( T ` x ) ) ) } , RR* , < )
24 12 ffvelrni 
 |-  ( x e. ~H -> ( T ` x ) e. CC )
25 24 abscld 
 |-  ( x e. ~H -> ( abs ` ( T ` x ) ) e. RR )
26 10 fveq2i 
 |-  ( abs ` ( T ` 0h ) ) = ( abs ` 0 )
27 abs0 
 |-  ( abs ` 0 ) = 0
28 26 27 eqtri 
 |-  ( abs ` ( T ` 0h ) ) = 0
29 rpcn 
 |-  ( ( y / 2 ) e. RR+ -> ( y / 2 ) e. CC )
30 1 lnfnmuli 
 |-  ( ( ( y / 2 ) e. CC /\ x e. ~H ) -> ( T ` ( ( y / 2 ) .h x ) ) = ( ( y / 2 ) x. ( T ` x ) ) )
31 29 30 sylan 
 |-  ( ( ( y / 2 ) e. RR+ /\ x e. ~H ) -> ( T ` ( ( y / 2 ) .h x ) ) = ( ( y / 2 ) x. ( T ` x ) ) )
32 31 fveq2d 
 |-  ( ( ( y / 2 ) e. RR+ /\ x e. ~H ) -> ( abs ` ( T ` ( ( y / 2 ) .h x ) ) ) = ( abs ` ( ( y / 2 ) x. ( T ` x ) ) ) )
33 absmul 
 |-  ( ( ( y / 2 ) e. CC /\ ( T ` x ) e. CC ) -> ( abs ` ( ( y / 2 ) x. ( T ` x ) ) ) = ( ( abs ` ( y / 2 ) ) x. ( abs ` ( T ` x ) ) ) )
34 29 24 33 syl2an 
 |-  ( ( ( y / 2 ) e. RR+ /\ x e. ~H ) -> ( abs ` ( ( y / 2 ) x. ( T ` x ) ) ) = ( ( abs ` ( y / 2 ) ) x. ( abs ` ( T ` x ) ) ) )
35 rpre 
 |-  ( ( y / 2 ) e. RR+ -> ( y / 2 ) e. RR )
36 rpge0 
 |-  ( ( y / 2 ) e. RR+ -> 0 <_ ( y / 2 ) )
37 35 36 absidd 
 |-  ( ( y / 2 ) e. RR+ -> ( abs ` ( y / 2 ) ) = ( y / 2 ) )
38 37 adantr 
 |-  ( ( ( y / 2 ) e. RR+ /\ x e. ~H ) -> ( abs ` ( y / 2 ) ) = ( y / 2 ) )
39 38 oveq1d 
 |-  ( ( ( y / 2 ) e. RR+ /\ x e. ~H ) -> ( ( abs ` ( y / 2 ) ) x. ( abs ` ( T ` x ) ) ) = ( ( y / 2 ) x. ( abs ` ( T ` x ) ) ) )
40 32 34 39 3eqtrrd 
 |-  ( ( ( y / 2 ) e. RR+ /\ x e. ~H ) -> ( ( y / 2 ) x. ( abs ` ( T ` x ) ) ) = ( abs ` ( T ` ( ( y / 2 ) .h x ) ) ) )
41 21 23 25 28 40 nmcexi 
 |-  ( normfn ` T ) e. RR