# 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 ${⊢}{T}\in \mathrm{BndLinOp}$
Assertion nmbdoplbi ${⊢}{A}\in ℋ\to {norm}_{ℎ}\left({T}\left({A}\right)\right)\le {norm}_{\mathrm{op}}\left({T}\right){norm}_{ℎ}\left({A}\right)$

### Proof

Step Hyp Ref Expression
1 nmbdoplb.1 ${⊢}{T}\in \mathrm{BndLinOp}$
2 fveq2 ${⊢}{A}={0}_{ℎ}\to {T}\left({A}\right)={T}\left({0}_{ℎ}\right)$
3 2 fveq2d ${⊢}{A}={0}_{ℎ}\to {norm}_{ℎ}\left({T}\left({A}\right)\right)={norm}_{ℎ}\left({T}\left({0}_{ℎ}\right)\right)$
4 fveq2 ${⊢}{A}={0}_{ℎ}\to {norm}_{ℎ}\left({A}\right)={norm}_{ℎ}\left({0}_{ℎ}\right)$
5 4 oveq2d ${⊢}{A}={0}_{ℎ}\to {norm}_{\mathrm{op}}\left({T}\right){norm}_{ℎ}\left({A}\right)={norm}_{\mathrm{op}}\left({T}\right){norm}_{ℎ}\left({0}_{ℎ}\right)$
6 3 5 breq12d ${⊢}{A}={0}_{ℎ}\to \left({norm}_{ℎ}\left({T}\left({A}\right)\right)\le {norm}_{\mathrm{op}}\left({T}\right){norm}_{ℎ}\left({A}\right)↔{norm}_{ℎ}\left({T}\left({0}_{ℎ}\right)\right)\le {norm}_{\mathrm{op}}\left({T}\right){norm}_{ℎ}\left({0}_{ℎ}\right)\right)$
7 bdopln ${⊢}{T}\in \mathrm{BndLinOp}\to {T}\in \mathrm{LinOp}$
8 1 7 ax-mp ${⊢}{T}\in \mathrm{LinOp}$
9 8 lnopfi ${⊢}{T}:ℋ⟶ℋ$
10 9 ffvelrni ${⊢}{A}\in ℋ\to {T}\left({A}\right)\in ℋ$
11 normcl ${⊢}{T}\left({A}\right)\in ℋ\to {norm}_{ℎ}\left({T}\left({A}\right)\right)\in ℝ$
12 10 11 syl ${⊢}{A}\in ℋ\to {norm}_{ℎ}\left({T}\left({A}\right)\right)\in ℝ$
13 12 adantr ${⊢}\left({A}\in ℋ\wedge {A}\ne {0}_{ℎ}\right)\to {norm}_{ℎ}\left({T}\left({A}\right)\right)\in ℝ$
14 13 recnd ${⊢}\left({A}\in ℋ\wedge {A}\ne {0}_{ℎ}\right)\to {norm}_{ℎ}\left({T}\left({A}\right)\right)\in ℂ$
15 normcl ${⊢}{A}\in ℋ\to {norm}_{ℎ}\left({A}\right)\in ℝ$
16 15 adantr ${⊢}\left({A}\in ℋ\wedge {A}\ne {0}_{ℎ}\right)\to {norm}_{ℎ}\left({A}\right)\in ℝ$
17 16 recnd ${⊢}\left({A}\in ℋ\wedge {A}\ne {0}_{ℎ}\right)\to {norm}_{ℎ}\left({A}\right)\in ℂ$
18 normne0 ${⊢}{A}\in ℋ\to \left({norm}_{ℎ}\left({A}\right)\ne 0↔{A}\ne {0}_{ℎ}\right)$
19 18 biimpar ${⊢}\left({A}\in ℋ\wedge {A}\ne {0}_{ℎ}\right)\to {norm}_{ℎ}\left({A}\right)\ne 0$
20 14 17 19 divrec2d ${⊢}\left({A}\in ℋ\wedge {A}\ne {0}_{ℎ}\right)\to \frac{{norm}_{ℎ}\left({T}\left({A}\right)\right)}{{norm}_{ℎ}\left({A}\right)}=\left(\frac{1}{{norm}_{ℎ}\left({A}\right)}\right){norm}_{ℎ}\left({T}\left({A}\right)\right)$
21 16 19 rereccld ${⊢}\left({A}\in ℋ\wedge {A}\ne {0}_{ℎ}\right)\to \frac{1}{{norm}_{ℎ}\left({A}\right)}\in ℝ$
22 21 recnd ${⊢}\left({A}\in ℋ\wedge {A}\ne {0}_{ℎ}\right)\to \frac{1}{{norm}_{ℎ}\left({A}\right)}\in ℂ$
23 simpl ${⊢}\left({A}\in ℋ\wedge {A}\ne {0}_{ℎ}\right)\to {A}\in ℋ$
24 8 lnopmuli ${⊢}\left(\frac{1}{{norm}_{ℎ}\left({A}\right)}\in ℂ\wedge {A}\in ℋ\right)\to {T}\left(\left(\frac{1}{{norm}_{ℎ}\left({A}\right)}\right){\cdot }_{ℎ}{A}\right)=\left(\frac{1}{{norm}_{ℎ}\left({A}\right)}\right){\cdot }_{ℎ}{T}\left({A}\right)$
25 22 23 24 syl2anc ${⊢}\left({A}\in ℋ\wedge {A}\ne {0}_{ℎ}\right)\to {T}\left(\left(\frac{1}{{norm}_{ℎ}\left({A}\right)}\right){\cdot }_{ℎ}{A}\right)=\left(\frac{1}{{norm}_{ℎ}\left({A}\right)}\right){\cdot }_{ℎ}{T}\left({A}\right)$
26 25 fveq2d ${⊢}\left({A}\in ℋ\wedge {A}\ne {0}_{ℎ}\right)\to {norm}_{ℎ}\left({T}\left(\left(\frac{1}{{norm}_{ℎ}\left({A}\right)}\right){\cdot }_{ℎ}{A}\right)\right)={norm}_{ℎ}\left(\left(\frac{1}{{norm}_{ℎ}\left({A}\right)}\right){\cdot }_{ℎ}{T}\left({A}\right)\right)$
27 10 adantr ${⊢}\left({A}\in ℋ\wedge {A}\ne {0}_{ℎ}\right)\to {T}\left({A}\right)\in ℋ$
28 norm-iii ${⊢}\left(\frac{1}{{norm}_{ℎ}\left({A}\right)}\in ℂ\wedge {T}\left({A}\right)\in ℋ\right)\to {norm}_{ℎ}\left(\left(\frac{1}{{norm}_{ℎ}\left({A}\right)}\right){\cdot }_{ℎ}{T}\left({A}\right)\right)=\left|\frac{1}{{norm}_{ℎ}\left({A}\right)}\right|{norm}_{ℎ}\left({T}\left({A}\right)\right)$
29 22 27 28 syl2anc ${⊢}\left({A}\in ℋ\wedge {A}\ne {0}_{ℎ}\right)\to {norm}_{ℎ}\left(\left(\frac{1}{{norm}_{ℎ}\left({A}\right)}\right){\cdot }_{ℎ}{T}\left({A}\right)\right)=\left|\frac{1}{{norm}_{ℎ}\left({A}\right)}\right|{norm}_{ℎ}\left({T}\left({A}\right)\right)$
30 normgt0 ${⊢}{A}\in ℋ\to \left({A}\ne {0}_{ℎ}↔0<{norm}_{ℎ}\left({A}\right)\right)$
31 30 biimpa ${⊢}\left({A}\in ℋ\wedge {A}\ne {0}_{ℎ}\right)\to 0<{norm}_{ℎ}\left({A}\right)$
32 16 31 recgt0d ${⊢}\left({A}\in ℋ\wedge {A}\ne {0}_{ℎ}\right)\to 0<\frac{1}{{norm}_{ℎ}\left({A}\right)}$
33 0re ${⊢}0\in ℝ$
34 ltle ${⊢}\left(0\in ℝ\wedge \frac{1}{{norm}_{ℎ}\left({A}\right)}\in ℝ\right)\to \left(0<\frac{1}{{norm}_{ℎ}\left({A}\right)}\to 0\le \frac{1}{{norm}_{ℎ}\left({A}\right)}\right)$
35 33 34 mpan ${⊢}\frac{1}{{norm}_{ℎ}\left({A}\right)}\in ℝ\to \left(0<\frac{1}{{norm}_{ℎ}\left({A}\right)}\to 0\le \frac{1}{{norm}_{ℎ}\left({A}\right)}\right)$
36 21 32 35 sylc ${⊢}\left({A}\in ℋ\wedge {A}\ne {0}_{ℎ}\right)\to 0\le \frac{1}{{norm}_{ℎ}\left({A}\right)}$
37 21 36 absidd ${⊢}\left({A}\in ℋ\wedge {A}\ne {0}_{ℎ}\right)\to \left|\frac{1}{{norm}_{ℎ}\left({A}\right)}\right|=\frac{1}{{norm}_{ℎ}\left({A}\right)}$
38 37 oveq1d ${⊢}\left({A}\in ℋ\wedge {A}\ne {0}_{ℎ}\right)\to \left|\frac{1}{{norm}_{ℎ}\left({A}\right)}\right|{norm}_{ℎ}\left({T}\left({A}\right)\right)=\left(\frac{1}{{norm}_{ℎ}\left({A}\right)}\right){norm}_{ℎ}\left({T}\left({A}\right)\right)$
39 26 29 38 3eqtrrd ${⊢}\left({A}\in ℋ\wedge {A}\ne {0}_{ℎ}\right)\to \left(\frac{1}{{norm}_{ℎ}\left({A}\right)}\right){norm}_{ℎ}\left({T}\left({A}\right)\right)={norm}_{ℎ}\left({T}\left(\left(\frac{1}{{norm}_{ℎ}\left({A}\right)}\right){\cdot }_{ℎ}{A}\right)\right)$
40 20 39 eqtrd ${⊢}\left({A}\in ℋ\wedge {A}\ne {0}_{ℎ}\right)\to \frac{{norm}_{ℎ}\left({T}\left({A}\right)\right)}{{norm}_{ℎ}\left({A}\right)}={norm}_{ℎ}\left({T}\left(\left(\frac{1}{{norm}_{ℎ}\left({A}\right)}\right){\cdot }_{ℎ}{A}\right)\right)$
41 hvmulcl ${⊢}\left(\frac{1}{{norm}_{ℎ}\left({A}\right)}\in ℂ\wedge {A}\in ℋ\right)\to \left(\frac{1}{{norm}_{ℎ}\left({A}\right)}\right){\cdot }_{ℎ}{A}\in ℋ$
42 22 23 41 syl2anc ${⊢}\left({A}\in ℋ\wedge {A}\ne {0}_{ℎ}\right)\to \left(\frac{1}{{norm}_{ℎ}\left({A}\right)}\right){\cdot }_{ℎ}{A}\in ℋ$
43 normcl ${⊢}\left(\frac{1}{{norm}_{ℎ}\left({A}\right)}\right){\cdot }_{ℎ}{A}\in ℋ\to {norm}_{ℎ}\left(\left(\frac{1}{{norm}_{ℎ}\left({A}\right)}\right){\cdot }_{ℎ}{A}\right)\in ℝ$
44 42 43 syl ${⊢}\left({A}\in ℋ\wedge {A}\ne {0}_{ℎ}\right)\to {norm}_{ℎ}\left(\left(\frac{1}{{norm}_{ℎ}\left({A}\right)}\right){\cdot }_{ℎ}{A}\right)\in ℝ$
45 norm1 ${⊢}\left({A}\in ℋ\wedge {A}\ne {0}_{ℎ}\right)\to {norm}_{ℎ}\left(\left(\frac{1}{{norm}_{ℎ}\left({A}\right)}\right){\cdot }_{ℎ}{A}\right)=1$
46 eqle ${⊢}\left({norm}_{ℎ}\left(\left(\frac{1}{{norm}_{ℎ}\left({A}\right)}\right){\cdot }_{ℎ}{A}\right)\in ℝ\wedge {norm}_{ℎ}\left(\left(\frac{1}{{norm}_{ℎ}\left({A}\right)}\right){\cdot }_{ℎ}{A}\right)=1\right)\to {norm}_{ℎ}\left(\left(\frac{1}{{norm}_{ℎ}\left({A}\right)}\right){\cdot }_{ℎ}{A}\right)\le 1$
47 44 45 46 syl2anc ${⊢}\left({A}\in ℋ\wedge {A}\ne {0}_{ℎ}\right)\to {norm}_{ℎ}\left(\left(\frac{1}{{norm}_{ℎ}\left({A}\right)}\right){\cdot }_{ℎ}{A}\right)\le 1$
48 nmoplb ${⊢}\left({T}:ℋ⟶ℋ\wedge \left(\frac{1}{{norm}_{ℎ}\left({A}\right)}\right){\cdot }_{ℎ}{A}\in ℋ\wedge {norm}_{ℎ}\left(\left(\frac{1}{{norm}_{ℎ}\left({A}\right)}\right){\cdot }_{ℎ}{A}\right)\le 1\right)\to {norm}_{ℎ}\left({T}\left(\left(\frac{1}{{norm}_{ℎ}\left({A}\right)}\right){\cdot }_{ℎ}{A}\right)\right)\le {norm}_{\mathrm{op}}\left({T}\right)$
49 9 48 mp3an1 ${⊢}\left(\left(\frac{1}{{norm}_{ℎ}\left({A}\right)}\right){\cdot }_{ℎ}{A}\in ℋ\wedge {norm}_{ℎ}\left(\left(\frac{1}{{norm}_{ℎ}\left({A}\right)}\right){\cdot }_{ℎ}{A}\right)\le 1\right)\to {norm}_{ℎ}\left({T}\left(\left(\frac{1}{{norm}_{ℎ}\left({A}\right)}\right){\cdot }_{ℎ}{A}\right)\right)\le {norm}_{\mathrm{op}}\left({T}\right)$
50 42 47 49 syl2anc ${⊢}\left({A}\in ℋ\wedge {A}\ne {0}_{ℎ}\right)\to {norm}_{ℎ}\left({T}\left(\left(\frac{1}{{norm}_{ℎ}\left({A}\right)}\right){\cdot }_{ℎ}{A}\right)\right)\le {norm}_{\mathrm{op}}\left({T}\right)$
51 40 50 eqbrtrd ${⊢}\left({A}\in ℋ\wedge {A}\ne {0}_{ℎ}\right)\to \frac{{norm}_{ℎ}\left({T}\left({A}\right)\right)}{{norm}_{ℎ}\left({A}\right)}\le {norm}_{\mathrm{op}}\left({T}\right)$
52 nmopre ${⊢}{T}\in \mathrm{BndLinOp}\to {norm}_{\mathrm{op}}\left({T}\right)\in ℝ$
53 1 52 ax-mp ${⊢}{norm}_{\mathrm{op}}\left({T}\right)\in ℝ$
54 53 a1i ${⊢}\left({A}\in ℋ\wedge {A}\ne {0}_{ℎ}\right)\to {norm}_{\mathrm{op}}\left({T}\right)\in ℝ$
55 ledivmul2 ${⊢}\left({norm}_{ℎ}\left({T}\left({A}\right)\right)\in ℝ\wedge {norm}_{\mathrm{op}}\left({T}\right)\in ℝ\wedge \left({norm}_{ℎ}\left({A}\right)\in ℝ\wedge 0<{norm}_{ℎ}\left({A}\right)\right)\right)\to \left(\frac{{norm}_{ℎ}\left({T}\left({A}\right)\right)}{{norm}_{ℎ}\left({A}\right)}\le {norm}_{\mathrm{op}}\left({T}\right)↔{norm}_{ℎ}\left({T}\left({A}\right)\right)\le {norm}_{\mathrm{op}}\left({T}\right){norm}_{ℎ}\left({A}\right)\right)$
56 13 54 16 31 55 syl112anc ${⊢}\left({A}\in ℋ\wedge {A}\ne {0}_{ℎ}\right)\to \left(\frac{{norm}_{ℎ}\left({T}\left({A}\right)\right)}{{norm}_{ℎ}\left({A}\right)}\le {norm}_{\mathrm{op}}\left({T}\right)↔{norm}_{ℎ}\left({T}\left({A}\right)\right)\le {norm}_{\mathrm{op}}\left({T}\right){norm}_{ℎ}\left({A}\right)\right)$
57 51 56 mpbid ${⊢}\left({A}\in ℋ\wedge {A}\ne {0}_{ℎ}\right)\to {norm}_{ℎ}\left({T}\left({A}\right)\right)\le {norm}_{\mathrm{op}}\left({T}\right){norm}_{ℎ}\left({A}\right)$
58 0le0 ${⊢}0\le 0$
59 8 lnop0i ${⊢}{T}\left({0}_{ℎ}\right)={0}_{ℎ}$
60 59 fveq2i ${⊢}{norm}_{ℎ}\left({T}\left({0}_{ℎ}\right)\right)={norm}_{ℎ}\left({0}_{ℎ}\right)$
61 norm0 ${⊢}{norm}_{ℎ}\left({0}_{ℎ}\right)=0$
62 60 61 eqtri ${⊢}{norm}_{ℎ}\left({T}\left({0}_{ℎ}\right)\right)=0$
63 61 oveq2i ${⊢}{norm}_{\mathrm{op}}\left({T}\right){norm}_{ℎ}\left({0}_{ℎ}\right)={norm}_{\mathrm{op}}\left({T}\right)\cdot 0$
64 53 recni ${⊢}{norm}_{\mathrm{op}}\left({T}\right)\in ℂ$
65 64 mul01i ${⊢}{norm}_{\mathrm{op}}\left({T}\right)\cdot 0=0$
66 63 65 eqtri ${⊢}{norm}_{\mathrm{op}}\left({T}\right){norm}_{ℎ}\left({0}_{ℎ}\right)=0$
67 58 62 66 3brtr4i ${⊢}{norm}_{ℎ}\left({T}\left({0}_{ℎ}\right)\right)\le {norm}_{\mathrm{op}}\left({T}\right){norm}_{ℎ}\left({0}_{ℎ}\right)$
68 67 a1i ${⊢}{A}\in ℋ\to {norm}_{ℎ}\left({T}\left({0}_{ℎ}\right)\right)\le {norm}_{\mathrm{op}}\left({T}\right){norm}_{ℎ}\left({0}_{ℎ}\right)$
69 6 57 68 pm2.61ne ${⊢}{A}\in ℋ\to {norm}_{ℎ}\left({T}\left({A}\right)\right)\le {norm}_{\mathrm{op}}\left({T}\right){norm}_{ℎ}\left({A}\right)$