Metamath Proof Explorer


Theorem nmcfnlbi

Description: A lower bound for the norm of a continuous linear functional. Theorem 3.5(ii) of Beran p. 99. (Contributed by NM, 14-Feb-2006) (New usage is discouraged.)

Ref Expression
Hypotheses nmcfnex.1 TLinFn
nmcfnex.2 TContFn
Assertion nmcfnlbi ATAnormfnTnormA

Proof

Step Hyp Ref Expression
1 nmcfnex.1 TLinFn
2 nmcfnex.2 TContFn
3 fveq2 A=0TA=T0
4 1 lnfn0i T0=0
5 3 4 eqtrdi A=0TA=0
6 5 abs00bd A=0TA=0
7 0le0 00
8 fveq2 A=0normA=norm0
9 norm0 norm0=0
10 8 9 eqtrdi A=0normA=0
11 10 oveq2d A=0normfnTnormA=normfnT0
12 1 2 nmcfnexi normfnT
13 12 recni normfnT
14 13 mul01i normfnT0=0
15 11 14 eqtr2di A=00=normfnTnormA
16 7 15 breqtrid A=00normfnTnormA
17 6 16 eqbrtrd A=0TAnormfnTnormA
18 17 adantl AA=0TAnormfnTnormA
19 1 lnfnfi T:
20 19 ffvelrni ATA
21 20 abscld ATA
22 21 adantr A¬A=0TA
23 22 recnd A¬A=0TA
24 normcl AnormA
25 24 adantr A¬A=0normA
26 25 recnd A¬A=0normA
27 norm-i AnormA=0A=0
28 27 notbid A¬normA=0¬A=0
29 28 biimpar A¬A=0¬normA=0
30 29 neqned A¬A=0normA0
31 23 26 30 divrec2d A¬A=0TAnormA=1normATA
32 25 30 rereccld A¬A=01normA
33 32 recnd A¬A=01normA
34 simpl A¬A=0A
35 1 lnfnmuli 1normAAT1normAA=1normATA
36 33 34 35 syl2anc A¬A=0T1normAA=1normATA
37 36 fveq2d A¬A=0T1normAA=1normATA
38 20 adantr A¬A=0TA
39 33 38 absmuld A¬A=01normATA=1normATA
40 df-ne A0¬A=0
41 normgt0 AA00<normA
42 40 41 bitr3id A¬A=00<normA
43 42 biimpa A¬A=00<normA
44 25 43 recgt0d A¬A=00<1normA
45 0re 0
46 ltle 01normA0<1normA01normA
47 45 46 mpan 1normA0<1normA01normA
48 32 44 47 sylc A¬A=001normA
49 32 48 absidd A¬A=01normA=1normA
50 49 oveq1d A¬A=01normATA=1normATA
51 37 39 50 3eqtrrd A¬A=01normATA=T1normAA
52 31 51 eqtrd A¬A=0TAnormA=T1normAA
53 hvmulcl 1normAA1normAA
54 33 34 53 syl2anc A¬A=01normAA
55 normcl 1normAAnorm1normAA
56 54 55 syl A¬A=0norm1normAA
57 norm1 AA0norm1normAA=1
58 40 57 sylan2br A¬A=0norm1normAA=1
59 eqle norm1normAAnorm1normAA=1norm1normAA1
60 56 58 59 syl2anc A¬A=0norm1normAA1
61 nmfnlb T:1normAAnorm1normAA1T1normAAnormfnT
62 19 61 mp3an1 1normAAnorm1normAA1T1normAAnormfnT
63 54 60 62 syl2anc A¬A=0T1normAAnormfnT
64 52 63 eqbrtrd A¬A=0TAnormAnormfnT
65 12 a1i A¬A=0normfnT
66 ledivmul2 TAnormfnTnormA0<normATAnormAnormfnTTAnormfnTnormA
67 22 65 25 43 66 syl112anc A¬A=0TAnormAnormfnTTAnormfnTnormA
68 64 67 mpbid A¬A=0TAnormfnTnormA
69 18 68 pm2.61dan ATAnormfnTnormA