Metamath Proof Explorer

Theorem nmcexi

Description: Lemma for nmcopexi and nmcfnexi . The norm of a continuous linear Hilbert space operator or functional exists. Theorem 3.5(i) of Beran p. 99. (Contributed by Mario Carneiro, 17-Nov-2013) (Proof shortened by Mario Carneiro, 23-Dec-2013) (New usage is discouraged.)

Ref Expression
Hypotheses nmcex.1 
|- E. y e. RR+ A. z e. ~H ( ( normh ` z ) < y -> ( N ` ( T ` z ) ) < 1 )
nmcex.2 
|- ( S ` T ) = sup ( { m | E. x e. ~H ( ( normh ` x ) <_ 1 /\ m = ( N ` ( T ` x ) ) ) } , RR* , < )
nmcex.3 
|- ( x e. ~H -> ( N ` ( T ` x ) ) e. RR )
nmcex.4 
|- ( N ` ( T ` 0h ) ) = 0
nmcex.5 
|- ( ( ( y / 2 ) e. RR+ /\ x e. ~H ) -> ( ( y / 2 ) x. ( N ` ( T ` x ) ) ) = ( N ` ( T ` ( ( y / 2 ) .h x ) ) ) )
Assertion nmcexi 
|- ( S ` T ) e. RR

Proof

Step Hyp Ref Expression
1 nmcex.1 
 |-  E. y e. RR+ A. z e. ~H ( ( normh ` z ) < y -> ( N ` ( T ` z ) ) < 1 )
2 nmcex.2 
 |-  ( S ` T ) = sup ( { m | E. x e. ~H ( ( normh ` x ) <_ 1 /\ m = ( N ` ( T ` x ) ) ) } , RR* , < )
3 nmcex.3 
 |-  ( x e. ~H -> ( N ` ( T ` x ) ) e. RR )
4 nmcex.4 
 |-  ( N ` ( T ` 0h ) ) = 0
5 nmcex.5 
 |-  ( ( ( y / 2 ) e. RR+ /\ x e. ~H ) -> ( ( y / 2 ) x. ( N ` ( T ` x ) ) ) = ( N ` ( T ` ( ( y / 2 ) .h x ) ) ) )
6 eleq1 
 |-  ( m = ( N ` ( T ` x ) ) -> ( m e. RR <-> ( N ` ( T ` x ) ) e. RR ) )
7 3 6 syl5ibrcom 
 |-  ( x e. ~H -> ( m = ( N ` ( T ` x ) ) -> m e. RR ) )
8 7 imp 
 |-  ( ( x e. ~H /\ m = ( N ` ( T ` x ) ) ) -> m e. RR )
9 8 adantrl 
 |-  ( ( x e. ~H /\ ( ( normh ` x ) <_ 1 /\ m = ( N ` ( T ` x ) ) ) ) -> m e. RR )
10 9 rexlimiva 
 |-  ( E. x e. ~H ( ( normh ` x ) <_ 1 /\ m = ( N ` ( T ` x ) ) ) -> m e. RR )
11 10 abssi 
 |-  { m | E. x e. ~H ( ( normh ` x ) <_ 1 /\ m = ( N ` ( T ` x ) ) ) } C_ RR
12 ax-hv0cl 
 |-  0h e. ~H
13 norm0 
 |-  ( normh ` 0h ) = 0
14 0le1 
 |-  0 <_ 1
15 13 14 eqbrtri 
 |-  ( normh ` 0h ) <_ 1
16 4 eqcomi 
 |-  0 = ( N ` ( T ` 0h ) )
17 15 16 pm3.2i 
 |-  ( ( normh ` 0h ) <_ 1 /\ 0 = ( N ` ( T ` 0h ) ) )
18 fveq2 
 |-  ( x = 0h -> ( normh ` x ) = ( normh ` 0h ) )
19 18 breq1d 
 |-  ( x = 0h -> ( ( normh ` x ) <_ 1 <-> ( normh ` 0h ) <_ 1 ) )
20 2fveq3 
 |-  ( x = 0h -> ( N ` ( T ` x ) ) = ( N ` ( T ` 0h ) ) )
21 20 eqeq2d 
 |-  ( x = 0h -> ( 0 = ( N ` ( T ` x ) ) <-> 0 = ( N ` ( T ` 0h ) ) ) )
22 19 21 anbi12d 
 |-  ( x = 0h -> ( ( ( normh ` x ) <_ 1 /\ 0 = ( N ` ( T ` x ) ) ) <-> ( ( normh ` 0h ) <_ 1 /\ 0 = ( N ` ( T ` 0h ) ) ) ) )
23 22 rspcev 
 |-  ( ( 0h e. ~H /\ ( ( normh ` 0h ) <_ 1 /\ 0 = ( N ` ( T ` 0h ) ) ) ) -> E. x e. ~H ( ( normh ` x ) <_ 1 /\ 0 = ( N ` ( T ` x ) ) ) )
24 12 17 23 mp2an 
 |-  E. x e. ~H ( ( normh ` x ) <_ 1 /\ 0 = ( N ` ( T ` x ) ) )
25 c0ex 
 |-  0 e. _V
26 eqeq1 
 |-  ( m = 0 -> ( m = ( N ` ( T ` x ) ) <-> 0 = ( N ` ( T ` x ) ) ) )
27 26 anbi2d 
 |-  ( m = 0 -> ( ( ( normh ` x ) <_ 1 /\ m = ( N ` ( T ` x ) ) ) <-> ( ( normh ` x ) <_ 1 /\ 0 = ( N ` ( T ` x ) ) ) ) )
28 27 rexbidv 
 |-  ( m = 0 -> ( E. x e. ~H ( ( normh ` x ) <_ 1 /\ m = ( N ` ( T ` x ) ) ) <-> E. x e. ~H ( ( normh ` x ) <_ 1 /\ 0 = ( N ` ( T ` x ) ) ) ) )
29 25 28 elab 
 |-  ( 0 e. { m | E. x e. ~H ( ( normh ` x ) <_ 1 /\ m = ( N ` ( T ` x ) ) ) } <-> E. x e. ~H ( ( normh ` x ) <_ 1 /\ 0 = ( N ` ( T ` x ) ) ) )
30 24 29 mpbir 
 |-  0 e. { m | E. x e. ~H ( ( normh ` x ) <_ 1 /\ m = ( N ` ( T ` x ) ) ) }
31 30 ne0ii 
 |-  { m | E. x e. ~H ( ( normh ` x ) <_ 1 /\ m = ( N ` ( T ` x ) ) ) } =/= (/)
32 2rp 
 |-  2 e. RR+
33 rpdivcl 
 |-  ( ( 2 e. RR+ /\ y e. RR+ ) -> ( 2 / y ) e. RR+ )
34 32 33 mpan 
 |-  ( y e. RR+ -> ( 2 / y ) e. RR+ )
35 34 rpred 
 |-  ( y e. RR+ -> ( 2 / y ) e. RR )
36 35 adantr 
 |-  ( ( y e. RR+ /\ A. z e. ~H ( ( normh ` z ) < y -> ( N ` ( T ` z ) ) < 1 ) ) -> ( 2 / y ) e. RR )
37 rpre 
 |-  ( y e. RR+ -> y e. RR )
38 37 adantr 
 |-  ( ( y e. RR+ /\ ( x e. ~H /\ ( normh ` x ) <_ 1 ) ) -> y e. RR )
39 38 rehalfcld 
 |-  ( ( y e. RR+ /\ ( x e. ~H /\ ( normh ` x ) <_ 1 ) ) -> ( y / 2 ) e. RR )
40 39 recnd 
 |-  ( ( y e. RR+ /\ ( x e. ~H /\ ( normh ` x ) <_ 1 ) ) -> ( y / 2 ) e. CC )
41 simprl 
 |-  ( ( y e. RR+ /\ ( x e. ~H /\ ( normh ` x ) <_ 1 ) ) -> x e. ~H )
42 hvmulcl 
 |-  ( ( ( y / 2 ) e. CC /\ x e. ~H ) -> ( ( y / 2 ) .h x ) e. ~H )
43 40 41 42 syl2anc 
 |-  ( ( y e. RR+ /\ ( x e. ~H /\ ( normh ` x ) <_ 1 ) ) -> ( ( y / 2 ) .h x ) e. ~H )
44 normcl 
 |-  ( ( ( y / 2 ) .h x ) e. ~H -> ( normh ` ( ( y / 2 ) .h x ) ) e. RR )
45 43 44 syl 
 |-  ( ( y e. RR+ /\ ( x e. ~H /\ ( normh ` x ) <_ 1 ) ) -> ( normh ` ( ( y / 2 ) .h x ) ) e. RR )
46 simprr 
 |-  ( ( y e. RR+ /\ ( x e. ~H /\ ( normh ` x ) <_ 1 ) ) -> ( normh ` x ) <_ 1 )
47 normcl 
 |-  ( x e. ~H -> ( normh ` x ) e. RR )
48 47 ad2antrl 
 |-  ( ( y e. RR+ /\ ( x e. ~H /\ ( normh ` x ) <_ 1 ) ) -> ( normh ` x ) e. RR )
49 1red 
 |-  ( ( y e. RR+ /\ ( x e. ~H /\ ( normh ` x ) <_ 1 ) ) -> 1 e. RR )
50 rphalfcl 
 |-  ( y e. RR+ -> ( y / 2 ) e. RR+ )
51 50 adantr 
 |-  ( ( y e. RR+ /\ ( x e. ~H /\ ( normh ` x ) <_ 1 ) ) -> ( y / 2 ) e. RR+ )
52 48 49 51 lemul2d 
 |-  ( ( y e. RR+ /\ ( x e. ~H /\ ( normh ` x ) <_ 1 ) ) -> ( ( normh ` x ) <_ 1 <-> ( ( y / 2 ) x. ( normh ` x ) ) <_ ( ( y / 2 ) x. 1 ) ) )
53 46 52 mpbid 
 |-  ( ( y e. RR+ /\ ( x e. ~H /\ ( normh ` x ) <_ 1 ) ) -> ( ( y / 2 ) x. ( normh ` x ) ) <_ ( ( y / 2 ) x. 1 ) )
54 rpcn 
 |-  ( ( y / 2 ) e. RR+ -> ( y / 2 ) e. CC )
55 norm-iii 
 |-  ( ( ( y / 2 ) e. CC /\ x e. ~H ) -> ( normh ` ( ( y / 2 ) .h x ) ) = ( ( abs ` ( y / 2 ) ) x. ( normh ` x ) ) )
56 54 55 sylan 
 |-  ( ( ( y / 2 ) e. RR+ /\ x e. ~H ) -> ( normh ` ( ( y / 2 ) .h x ) ) = ( ( abs ` ( y / 2 ) ) x. ( normh ` x ) ) )
57 rpre 
 |-  ( ( y / 2 ) e. RR+ -> ( y / 2 ) e. RR )
58 rpge0 
 |-  ( ( y / 2 ) e. RR+ -> 0 <_ ( y / 2 ) )
59 57 58 absidd 
 |-  ( ( y / 2 ) e. RR+ -> ( abs ` ( y / 2 ) ) = ( y / 2 ) )
60 59 oveq1d 
 |-  ( ( y / 2 ) e. RR+ -> ( ( abs ` ( y / 2 ) ) x. ( normh ` x ) ) = ( ( y / 2 ) x. ( normh ` x ) ) )
61 60 adantr 
 |-  ( ( ( y / 2 ) e. RR+ /\ x e. ~H ) -> ( ( abs ` ( y / 2 ) ) x. ( normh ` x ) ) = ( ( y / 2 ) x. ( normh ` x ) ) )
62 56 61 eqtr2d 
 |-  ( ( ( y / 2 ) e. RR+ /\ x e. ~H ) -> ( ( y / 2 ) x. ( normh ` x ) ) = ( normh ` ( ( y / 2 ) .h x ) ) )
63 51 41 62 syl2anc 
 |-  ( ( y e. RR+ /\ ( x e. ~H /\ ( normh ` x ) <_ 1 ) ) -> ( ( y / 2 ) x. ( normh ` x ) ) = ( normh ` ( ( y / 2 ) .h x ) ) )
64 40 mulid1d 
 |-  ( ( y e. RR+ /\ ( x e. ~H /\ ( normh ` x ) <_ 1 ) ) -> ( ( y / 2 ) x. 1 ) = ( y / 2 ) )
65 53 63 64 3brtr3d 
 |-  ( ( y e. RR+ /\ ( x e. ~H /\ ( normh ` x ) <_ 1 ) ) -> ( normh ` ( ( y / 2 ) .h x ) ) <_ ( y / 2 ) )
66 rphalflt 
 |-  ( y e. RR+ -> ( y / 2 ) < y )
67 66 adantr 
 |-  ( ( y e. RR+ /\ ( x e. ~H /\ ( normh ` x ) <_ 1 ) ) -> ( y / 2 ) < y )
68 45 39 38 65 67 lelttrd 
 |-  ( ( y e. RR+ /\ ( x e. ~H /\ ( normh ` x ) <_ 1 ) ) -> ( normh ` ( ( y / 2 ) .h x ) ) < y )
69 fveq2 
 |-  ( z = ( ( y / 2 ) .h x ) -> ( normh ` z ) = ( normh ` ( ( y / 2 ) .h x ) ) )
70 69 breq1d 
 |-  ( z = ( ( y / 2 ) .h x ) -> ( ( normh ` z ) < y <-> ( normh ` ( ( y / 2 ) .h x ) ) < y ) )
71 2fveq3 
 |-  ( z = ( ( y / 2 ) .h x ) -> ( N ` ( T ` z ) ) = ( N ` ( T ` ( ( y / 2 ) .h x ) ) ) )
72 71 breq1d 
 |-  ( z = ( ( y / 2 ) .h x ) -> ( ( N ` ( T ` z ) ) < 1 <-> ( N ` ( T ` ( ( y / 2 ) .h x ) ) ) < 1 ) )
73 70 72 imbi12d 
 |-  ( z = ( ( y / 2 ) .h x ) -> ( ( ( normh ` z ) < y -> ( N ` ( T ` z ) ) < 1 ) <-> ( ( normh ` ( ( y / 2 ) .h x ) ) < y -> ( N ` ( T ` ( ( y / 2 ) .h x ) ) ) < 1 ) ) )
74 73 rspcv 
 |-  ( ( ( y / 2 ) .h x ) e. ~H -> ( A. z e. ~H ( ( normh ` z ) < y -> ( N ` ( T ` z ) ) < 1 ) -> ( ( normh ` ( ( y / 2 ) .h x ) ) < y -> ( N ` ( T ` ( ( y / 2 ) .h x ) ) ) < 1 ) ) )
75 43 74 syl 
 |-  ( ( y e. RR+ /\ ( x e. ~H /\ ( normh ` x ) <_ 1 ) ) -> ( A. z e. ~H ( ( normh ` z ) < y -> ( N ` ( T ` z ) ) < 1 ) -> ( ( normh ` ( ( y / 2 ) .h x ) ) < y -> ( N ` ( T ` ( ( y / 2 ) .h x ) ) ) < 1 ) ) )
76 68 75 mpid 
 |-  ( ( y e. RR+ /\ ( x e. ~H /\ ( normh ` x ) <_ 1 ) ) -> ( A. z e. ~H ( ( normh ` z ) < y -> ( N ` ( T ` z ) ) < 1 ) -> ( N ` ( T ` ( ( y / 2 ) .h x ) ) ) < 1 ) )
77 3 ad2antrl 
 |-  ( ( y e. RR+ /\ ( x e. ~H /\ ( normh ` x ) <_ 1 ) ) -> ( N ` ( T ` x ) ) e. RR )
78 77 49 51 ltmuldiv2d 
 |-  ( ( y e. RR+ /\ ( x e. ~H /\ ( normh ` x ) <_ 1 ) ) -> ( ( ( y / 2 ) x. ( N ` ( T ` x ) ) ) < 1 <-> ( N ` ( T ` x ) ) < ( 1 / ( y / 2 ) ) ) )
79 51 rprecred 
 |-  ( ( y e. RR+ /\ ( x e. ~H /\ ( normh ` x ) <_ 1 ) ) -> ( 1 / ( y / 2 ) ) e. RR )
80 ltle 
 |-  ( ( ( N ` ( T ` x ) ) e. RR /\ ( 1 / ( y / 2 ) ) e. RR ) -> ( ( N ` ( T ` x ) ) < ( 1 / ( y / 2 ) ) -> ( N ` ( T ` x ) ) <_ ( 1 / ( y / 2 ) ) ) )
81 77 79 80 syl2anc 
 |-  ( ( y e. RR+ /\ ( x e. ~H /\ ( normh ` x ) <_ 1 ) ) -> ( ( N ` ( T ` x ) ) < ( 1 / ( y / 2 ) ) -> ( N ` ( T ` x ) ) <_ ( 1 / ( y / 2 ) ) ) )
82 78 81 sylbid 
 |-  ( ( y e. RR+ /\ ( x e. ~H /\ ( normh ` x ) <_ 1 ) ) -> ( ( ( y / 2 ) x. ( N ` ( T ` x ) ) ) < 1 -> ( N ` ( T ` x ) ) <_ ( 1 / ( y / 2 ) ) ) )
83 51 41 5 syl2anc 
 |-  ( ( y e. RR+ /\ ( x e. ~H /\ ( normh ` x ) <_ 1 ) ) -> ( ( y / 2 ) x. ( N ` ( T ` x ) ) ) = ( N ` ( T ` ( ( y / 2 ) .h x ) ) ) )
84 83 breq1d 
 |-  ( ( y e. RR+ /\ ( x e. ~H /\ ( normh ` x ) <_ 1 ) ) -> ( ( ( y / 2 ) x. ( N ` ( T ` x ) ) ) < 1 <-> ( N ` ( T ` ( ( y / 2 ) .h x ) ) ) < 1 ) )
85 rpcn 
 |-  ( y e. RR+ -> y e. CC )
86 rpne0 
 |-  ( y e. RR+ -> y =/= 0 )
87 2cn 
 |-  2 e. CC
88 2ne0 
 |-  2 =/= 0
89 recdiv 
 |-  ( ( ( y e. CC /\ y =/= 0 ) /\ ( 2 e. CC /\ 2 =/= 0 ) ) -> ( 1 / ( y / 2 ) ) = ( 2 / y ) )
90 87 88 89 mpanr12 
 |-  ( ( y e. CC /\ y =/= 0 ) -> ( 1 / ( y / 2 ) ) = ( 2 / y ) )
91 85 86 90 syl2anc 
 |-  ( y e. RR+ -> ( 1 / ( y / 2 ) ) = ( 2 / y ) )
92 91 adantr 
 |-  ( ( y e. RR+ /\ ( x e. ~H /\ ( normh ` x ) <_ 1 ) ) -> ( 1 / ( y / 2 ) ) = ( 2 / y ) )
93 92 breq2d 
 |-  ( ( y e. RR+ /\ ( x e. ~H /\ ( normh ` x ) <_ 1 ) ) -> ( ( N ` ( T ` x ) ) <_ ( 1 / ( y / 2 ) ) <-> ( N ` ( T ` x ) ) <_ ( 2 / y ) ) )
94 82 84 93 3imtr3d 
 |-  ( ( y e. RR+ /\ ( x e. ~H /\ ( normh ` x ) <_ 1 ) ) -> ( ( N ` ( T ` ( ( y / 2 ) .h x ) ) ) < 1 -> ( N ` ( T ` x ) ) <_ ( 2 / y ) ) )
95 76 94 syld 
 |-  ( ( y e. RR+ /\ ( x e. ~H /\ ( normh ` x ) <_ 1 ) ) -> ( A. z e. ~H ( ( normh ` z ) < y -> ( N ` ( T ` z ) ) < 1 ) -> ( N ` ( T ` x ) ) <_ ( 2 / y ) ) )
96 95 imp 
 |-  ( ( ( y e. RR+ /\ ( x e. ~H /\ ( normh ` x ) <_ 1 ) ) /\ A. z e. ~H ( ( normh ` z ) < y -> ( N ` ( T ` z ) ) < 1 ) ) -> ( N ` ( T ` x ) ) <_ ( 2 / y ) )
97 96 an32s 
 |-  ( ( ( y e. RR+ /\ A. z e. ~H ( ( normh ` z ) < y -> ( N ` ( T ` z ) ) < 1 ) ) /\ ( x e. ~H /\ ( normh ` x ) <_ 1 ) ) -> ( N ` ( T ` x ) ) <_ ( 2 / y ) )
98 97 anassrs 
 |-  ( ( ( ( y e. RR+ /\ A. z e. ~H ( ( normh ` z ) < y -> ( N ` ( T ` z ) ) < 1 ) ) /\ x e. ~H ) /\ ( normh ` x ) <_ 1 ) -> ( N ` ( T ` x ) ) <_ ( 2 / y ) )
99 breq1 
 |-  ( n = ( N ` ( T ` x ) ) -> ( n <_ ( 2 / y ) <-> ( N ` ( T ` x ) ) <_ ( 2 / y ) ) )
100 98 99 syl5ibrcom 
 |-  ( ( ( ( y e. RR+ /\ A. z e. ~H ( ( normh ` z ) < y -> ( N ` ( T ` z ) ) < 1 ) ) /\ x e. ~H ) /\ ( normh ` x ) <_ 1 ) -> ( n = ( N ` ( T ` x ) ) -> n <_ ( 2 / y ) ) )
101 100 expimpd 
 |-  ( ( ( y e. RR+ /\ A. z e. ~H ( ( normh ` z ) < y -> ( N ` ( T ` z ) ) < 1 ) ) /\ x e. ~H ) -> ( ( ( normh ` x ) <_ 1 /\ n = ( N ` ( T ` x ) ) ) -> n <_ ( 2 / y ) ) )
102 101 rexlimdva 
 |-  ( ( y e. RR+ /\ A. z e. ~H ( ( normh ` z ) < y -> ( N ` ( T ` z ) ) < 1 ) ) -> ( E. x e. ~H ( ( normh ` x ) <_ 1 /\ n = ( N ` ( T ` x ) ) ) -> n <_ ( 2 / y ) ) )
103 102 alrimiv 
 |-  ( ( y e. RR+ /\ A. z e. ~H ( ( normh ` z ) < y -> ( N ` ( T ` z ) ) < 1 ) ) -> A. n ( E. x e. ~H ( ( normh ` x ) <_ 1 /\ n = ( N ` ( T ` x ) ) ) -> n <_ ( 2 / y ) ) )
104 eqeq1 
 |-  ( m = n -> ( m = ( N ` ( T ` x ) ) <-> n = ( N ` ( T ` x ) ) ) )
105 104 anbi2d 
 |-  ( m = n -> ( ( ( normh ` x ) <_ 1 /\ m = ( N ` ( T ` x ) ) ) <-> ( ( normh ` x ) <_ 1 /\ n = ( N ` ( T ` x ) ) ) ) )
106 105 rexbidv 
 |-  ( m = n -> ( E. x e. ~H ( ( normh ` x ) <_ 1 /\ m = ( N ` ( T ` x ) ) ) <-> E. x e. ~H ( ( normh ` x ) <_ 1 /\ n = ( N ` ( T ` x ) ) ) ) )
107 106 ralab 
 |-  ( A. n e. { m | E. x e. ~H ( ( normh ` x ) <_ 1 /\ m = ( N ` ( T ` x ) ) ) } n <_ z <-> A. n ( E. x e. ~H ( ( normh ` x ) <_ 1 /\ n = ( N ` ( T ` x ) ) ) -> n <_ z ) )
108 breq2 
 |-  ( z = ( 2 / y ) -> ( n <_ z <-> n <_ ( 2 / y ) ) )
109 108 imbi2d 
 |-  ( z = ( 2 / y ) -> ( ( E. x e. ~H ( ( normh ` x ) <_ 1 /\ n = ( N ` ( T ` x ) ) ) -> n <_ z ) <-> ( E. x e. ~H ( ( normh ` x ) <_ 1 /\ n = ( N ` ( T ` x ) ) ) -> n <_ ( 2 / y ) ) ) )
110 109 albidv 
 |-  ( z = ( 2 / y ) -> ( A. n ( E. x e. ~H ( ( normh ` x ) <_ 1 /\ n = ( N ` ( T ` x ) ) ) -> n <_ z ) <-> A. n ( E. x e. ~H ( ( normh ` x ) <_ 1 /\ n = ( N ` ( T ` x ) ) ) -> n <_ ( 2 / y ) ) ) )
111 107 110 syl5bb 
 |-  ( z = ( 2 / y ) -> ( A. n e. { m | E. x e. ~H ( ( normh ` x ) <_ 1 /\ m = ( N ` ( T ` x ) ) ) } n <_ z <-> A. n ( E. x e. ~H ( ( normh ` x ) <_ 1 /\ n = ( N ` ( T ` x ) ) ) -> n <_ ( 2 / y ) ) ) )
112 111 rspcev 
 |-  ( ( ( 2 / y ) e. RR /\ A. n ( E. x e. ~H ( ( normh ` x ) <_ 1 /\ n = ( N ` ( T ` x ) ) ) -> n <_ ( 2 / y ) ) ) -> E. z e. RR A. n e. { m | E. x e. ~H ( ( normh ` x ) <_ 1 /\ m = ( N ` ( T ` x ) ) ) } n <_ z )
113 36 103 112 syl2anc 
 |-  ( ( y e. RR+ /\ A. z e. ~H ( ( normh ` z ) < y -> ( N ` ( T ` z ) ) < 1 ) ) -> E. z e. RR A. n e. { m | E. x e. ~H ( ( normh ` x ) <_ 1 /\ m = ( N ` ( T ` x ) ) ) } n <_ z )
114 113 rexlimiva 
 |-  ( E. y e. RR+ A. z e. ~H ( ( normh ` z ) < y -> ( N ` ( T ` z ) ) < 1 ) -> E. z e. RR A. n e. { m | E. x e. ~H ( ( normh ` x ) <_ 1 /\ m = ( N ` ( T ` x ) ) ) } n <_ z )
115 1 114 ax-mp 
 |-  E. z e. RR A. n e. { m | E. x e. ~H ( ( normh ` x ) <_ 1 /\ m = ( N ` ( T ` x ) ) ) } n <_ z
116 supxrre 
 |-  ( ( { m | E. x e. ~H ( ( normh ` x ) <_ 1 /\ m = ( N ` ( T ` x ) ) ) } C_ RR /\ { m | E. x e. ~H ( ( normh ` x ) <_ 1 /\ m = ( N ` ( T ` x ) ) ) } =/= (/) /\ E. z e. RR A. n e. { m | E. x e. ~H ( ( normh ` x ) <_ 1 /\ m = ( N ` ( T ` x ) ) ) } n <_ z ) -> sup ( { m | E. x e. ~H ( ( normh ` x ) <_ 1 /\ m = ( N ` ( T ` x ) ) ) } , RR* , < ) = sup ( { m | E. x e. ~H ( ( normh ` x ) <_ 1 /\ m = ( N ` ( T ` x ) ) ) } , RR , < ) )
117 11 31 115 116 mp3an 
 |-  sup ( { m | E. x e. ~H ( ( normh ` x ) <_ 1 /\ m = ( N ` ( T ` x ) ) ) } , RR* , < ) = sup ( { m | E. x e. ~H ( ( normh ` x ) <_ 1 /\ m = ( N ` ( T ` x ) ) ) } , RR , < )
118 2 117 eqtri 
 |-  ( S ` T ) = sup ( { m | E. x e. ~H ( ( normh ` x ) <_ 1 /\ m = ( N ` ( T ` x ) ) ) } , RR , < )
119 suprcl 
 |-  ( ( { m | E. x e. ~H ( ( normh ` x ) <_ 1 /\ m = ( N ` ( T ` x ) ) ) } C_ RR /\ { m | E. x e. ~H ( ( normh ` x ) <_ 1 /\ m = ( N ` ( T ` x ) ) ) } =/= (/) /\ E. z e. RR A. n e. { m | E. x e. ~H ( ( normh ` x ) <_ 1 /\ m = ( N ` ( T ` x ) ) ) } n <_ z ) -> sup ( { m | E. x e. ~H ( ( normh ` x ) <_ 1 /\ m = ( N ` ( T ` x ) ) ) } , RR , < ) e. RR )
120 11 31 115 119 mp3an 
 |-  sup ( { m | E. x e. ~H ( ( normh ` x ) <_ 1 /\ m = ( N ` ( T ` x ) ) ) } , RR , < ) e. RR
121 118 120 eqeltri 
 |-  ( S ` T ) e. RR