Metamath Proof Explorer


Theorem nmbdoplbi

Description: A lower bound for the norm of a bounded linear operator. (Contributed by NM, 14-Feb-2006) (New usage is discouraged.)

Ref Expression
Hypothesis nmbdoplb.1 TBndLinOp
Assertion nmbdoplbi AnormTAnormopTnormA

Proof

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