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 T LinOp
nmcopex.2 T ContOp
Assertion nmcoplbi A norm T A norm op T norm A

Proof

Step Hyp Ref Expression
1 nmcopex.1 T LinOp
2 nmcopex.2 T ContOp
3 0le0 0 0
4 3 a1i A = 0 0 0
5 fveq2 A = 0 T A = T 0
6 1 lnop0i T 0 = 0
7 5 6 syl6eq A = 0 T A = 0
8 7 fveq2d A = 0 norm T A = norm 0
9 norm0 norm 0 = 0
10 8 9 syl6eq A = 0 norm T A = 0
11 fveq2 A = 0 norm A = norm 0
12 11 9 syl6eq A = 0 norm A = 0
13 12 oveq2d A = 0 norm op T norm A = norm op T 0
14 1 2 nmcopexi norm op T
15 14 recni norm op T
16 15 mul01i norm op T 0 = 0
17 13 16 syl6eq A = 0 norm op T norm A = 0
18 4 10 17 3brtr4d A = 0 norm T A norm op T norm A
19 18 adantl A A = 0 norm T A norm op T norm A
20 normcl A norm A
21 20 adantr A A 0 norm A
22 normne0 A norm A 0 A 0
23 22 biimpar A A 0 norm A 0
24 21 23 rereccld A A 0 1 norm A
25 normgt0 A A 0 0 < norm A
26 25 biimpa A A 0 0 < norm A
27 21 26 recgt0d A A 0 0 < 1 norm A
28 0re 0
29 ltle 0 1 norm A 0 < 1 norm A 0 1 norm A
30 28 29 mpan 1 norm A 0 < 1 norm A 0 1 norm A
31 24 27 30 sylc A A 0 0 1 norm A
32 24 31 absidd A A 0 1 norm A = 1 norm A
33 32 oveq1d A A 0 1 norm A norm T A = 1 norm A norm T A
34 24 recnd A A 0 1 norm A
35 simpl A A 0 A
36 1 lnopmuli 1 norm A A T 1 norm A A = 1 norm A T A
37 34 35 36 syl2anc A A 0 T 1 norm A A = 1 norm A T A
38 37 fveq2d A A 0 norm T 1 norm A A = norm 1 norm A T A
39 1 lnopfi T :
40 39 ffvelrni A T A
41 40 adantr A A 0 T A
42 norm-iii 1 norm A T A norm 1 norm A T A = 1 norm A norm T A
43 34 41 42 syl2anc A A 0 norm 1 norm A T A = 1 norm A norm T A
44 38 43 eqtrd A A 0 norm T 1 norm A A = 1 norm A norm T A
45 normcl T A norm T A
46 40 45 syl A norm T A
47 46 adantr A A 0 norm T A
48 47 recnd A A 0 norm T A
49 21 recnd A A 0 norm A
50 48 49 23 divrec2d A A 0 norm T A norm A = 1 norm A norm T A
51 33 44 50 3eqtr4rd A A 0 norm T A norm A = norm T 1 norm A A
52 hvmulcl 1 norm A A 1 norm A A
53 34 35 52 syl2anc A A 0 1 norm A A
54 normcl 1 norm A A norm 1 norm A A
55 53 54 syl A A 0 norm 1 norm A A
56 norm1 A A 0 norm 1 norm A A = 1
57 eqle norm 1 norm A A norm 1 norm A A = 1 norm 1 norm A A 1
58 55 56 57 syl2anc A A 0 norm 1 norm A A 1
59 nmoplb T : 1 norm A A norm 1 norm A A 1 norm T 1 norm A A norm op T
60 39 59 mp3an1 1 norm A A norm 1 norm A A 1 norm T 1 norm A A norm op T
61 53 58 60 syl2anc A A 0 norm T 1 norm A A norm op T
62 51 61 eqbrtrd A A 0 norm T A norm A norm op T
63 14 a1i A A 0 norm op T
64 ledivmul2 norm T A norm op T norm A 0 < norm A norm T A norm A norm op T norm T A norm op T norm A
65 47 63 21 26 64 syl112anc A A 0 norm T A norm A norm op T norm T A norm op T norm A
66 62 65 mpbid A A 0 norm T A norm op T norm A
67 19 66 pm2.61dane A norm T A norm op T norm A