Metamath Proof Explorer


Theorem nmcoplbi

Description: A lower bound for the norm of a continuous linear operator. Theorem 3.5(ii) of Beran p. 99. (Contributed by NM, 7-Feb-2006) (Revised by Mario Carneiro, 17-Nov-2013) (New usage is discouraged.)

Ref Expression
Hypotheses nmcopex.1 TLinOp
nmcopex.2 TContOp
Assertion nmcoplbi AnormTAnormopTnormA

Proof

Step Hyp Ref Expression
1 nmcopex.1 TLinOp
2 nmcopex.2 TContOp
3 0le0 00
4 3 a1i A=000
5 fveq2 A=0TA=T0
6 1 lnop0i T0=0
7 5 6 eqtrdi A=0TA=0
8 7 fveq2d A=0normTA=norm0
9 norm0 norm0=0
10 8 9 eqtrdi A=0normTA=0
11 fveq2 A=0normA=norm0
12 11 9 eqtrdi A=0normA=0
13 12 oveq2d A=0normopTnormA=normopT0
14 1 2 nmcopexi normopT
15 14 recni normopT
16 15 mul01i normopT0=0
17 13 16 eqtrdi A=0normopTnormA=0
18 4 10 17 3brtr4d A=0normTAnormopTnormA
19 18 adantl AA=0normTAnormopTnormA
20 normcl AnormA
21 20 adantr AA0normA
22 normne0 AnormA0A0
23 22 biimpar AA0normA0
24 21 23 rereccld AA01normA
25 normgt0 AA00<normA
26 25 biimpa AA00<normA
27 21 26 recgt0d AA00<1normA
28 0re 0
29 ltle 01normA0<1normA01normA
30 28 29 mpan 1normA0<1normA01normA
31 24 27 30 sylc AA001normA
32 24 31 absidd AA01normA=1normA
33 32 oveq1d AA01normAnormTA=1normAnormTA
34 24 recnd AA01normA
35 simpl AA0A
36 1 lnopmuli 1normAAT1normAA=1normATA
37 34 35 36 syl2anc AA0T1normAA=1normATA
38 37 fveq2d AA0normT1normAA=norm1normATA
39 1 lnopfi T:
40 39 ffvelrni ATA
41 40 adantr AA0TA
42 norm-iii 1normATAnorm1normATA=1normAnormTA
43 34 41 42 syl2anc AA0norm1normATA=1normAnormTA
44 38 43 eqtrd AA0normT1normAA=1normAnormTA
45 normcl TAnormTA
46 40 45 syl AnormTA
47 46 adantr AA0normTA
48 47 recnd AA0normTA
49 21 recnd AA0normA
50 48 49 23 divrec2d AA0normTAnormA=1normAnormTA
51 33 44 50 3eqtr4rd AA0normTAnormA=normT1normAA
52 hvmulcl 1normAA1normAA
53 34 35 52 syl2anc AA01normAA
54 normcl 1normAAnorm1normAA
55 53 54 syl AA0norm1normAA
56 norm1 AA0norm1normAA=1
57 eqle norm1normAAnorm1normAA=1norm1normAA1
58 55 56 57 syl2anc AA0norm1normAA1
59 nmoplb T:1normAAnorm1normAA1normT1normAAnormopT
60 39 59 mp3an1 1normAAnorm1normAA1normT1normAAnormopT
61 53 58 60 syl2anc AA0normT1normAAnormopT
62 51 61 eqbrtrd AA0normTAnormAnormopT
63 14 a1i AA0normopT
64 ledivmul2 normTAnormopTnormA0<normAnormTAnormAnormopTnormTAnormopTnormA
65 47 63 21 26 64 syl112anc AA0normTAnormAnormopTnormTAnormopTnormA
66 62 65 mpbid AA0normTAnormopTnormA
67 19 66 pm2.61dane AnormTAnormopTnormA