# 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}\in \mathrm{LinOp}$
nmcopex.2 ${⊢}{T}\in \mathrm{ContOp}$
Assertion nmcoplbi ${⊢}{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 nmcopex.1 ${⊢}{T}\in \mathrm{LinOp}$
2 nmcopex.2 ${⊢}{T}\in \mathrm{ContOp}$
3 0le0 ${⊢}0\le 0$
4 3 a1i ${⊢}{A}={0}_{ℎ}\to 0\le 0$
5 fveq2 ${⊢}{A}={0}_{ℎ}\to {T}\left({A}\right)={T}\left({0}_{ℎ}\right)$
6 1 lnop0i ${⊢}{T}\left({0}_{ℎ}\right)={0}_{ℎ}$
7 5 6 syl6eq ${⊢}{A}={0}_{ℎ}\to {T}\left({A}\right)={0}_{ℎ}$
8 7 fveq2d ${⊢}{A}={0}_{ℎ}\to {norm}_{ℎ}\left({T}\left({A}\right)\right)={norm}_{ℎ}\left({0}_{ℎ}\right)$
9 norm0 ${⊢}{norm}_{ℎ}\left({0}_{ℎ}\right)=0$
10 8 9 syl6eq ${⊢}{A}={0}_{ℎ}\to {norm}_{ℎ}\left({T}\left({A}\right)\right)=0$
11 fveq2 ${⊢}{A}={0}_{ℎ}\to {norm}_{ℎ}\left({A}\right)={norm}_{ℎ}\left({0}_{ℎ}\right)$
12 11 9 syl6eq ${⊢}{A}={0}_{ℎ}\to {norm}_{ℎ}\left({A}\right)=0$
13 12 oveq2d ${⊢}{A}={0}_{ℎ}\to {norm}_{\mathrm{op}}\left({T}\right){norm}_{ℎ}\left({A}\right)={norm}_{\mathrm{op}}\left({T}\right)\cdot 0$
14 1 2 nmcopexi ${⊢}{norm}_{\mathrm{op}}\left({T}\right)\in ℝ$
15 14 recni ${⊢}{norm}_{\mathrm{op}}\left({T}\right)\in ℂ$
16 15 mul01i ${⊢}{norm}_{\mathrm{op}}\left({T}\right)\cdot 0=0$
17 13 16 syl6eq ${⊢}{A}={0}_{ℎ}\to {norm}_{\mathrm{op}}\left({T}\right){norm}_{ℎ}\left({A}\right)=0$
18 4 10 17 3brtr4d ${⊢}{A}={0}_{ℎ}\to {norm}_{ℎ}\left({T}\left({A}\right)\right)\le {norm}_{\mathrm{op}}\left({T}\right){norm}_{ℎ}\left({A}\right)$
19 18 adantl ${⊢}\left({A}\in ℋ\wedge {A}={0}_{ℎ}\right)\to {norm}_{ℎ}\left({T}\left({A}\right)\right)\le {norm}_{\mathrm{op}}\left({T}\right){norm}_{ℎ}\left({A}\right)$
20 normcl ${⊢}{A}\in ℋ\to {norm}_{ℎ}\left({A}\right)\in ℝ$
21 20 adantr ${⊢}\left({A}\in ℋ\wedge {A}\ne {0}_{ℎ}\right)\to {norm}_{ℎ}\left({A}\right)\in ℝ$
22 normne0 ${⊢}{A}\in ℋ\to \left({norm}_{ℎ}\left({A}\right)\ne 0↔{A}\ne {0}_{ℎ}\right)$
23 22 biimpar ${⊢}\left({A}\in ℋ\wedge {A}\ne {0}_{ℎ}\right)\to {norm}_{ℎ}\left({A}\right)\ne 0$
24 21 23 rereccld ${⊢}\left({A}\in ℋ\wedge {A}\ne {0}_{ℎ}\right)\to \frac{1}{{norm}_{ℎ}\left({A}\right)}\in ℝ$
25 normgt0 ${⊢}{A}\in ℋ\to \left({A}\ne {0}_{ℎ}↔0<{norm}_{ℎ}\left({A}\right)\right)$
26 25 biimpa ${⊢}\left({A}\in ℋ\wedge {A}\ne {0}_{ℎ}\right)\to 0<{norm}_{ℎ}\left({A}\right)$
27 21 26 recgt0d ${⊢}\left({A}\in ℋ\wedge {A}\ne {0}_{ℎ}\right)\to 0<\frac{1}{{norm}_{ℎ}\left({A}\right)}$
28 0re ${⊢}0\in ℝ$
29 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)$
30 28 29 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)$
31 24 27 30 sylc ${⊢}\left({A}\in ℋ\wedge {A}\ne {0}_{ℎ}\right)\to 0\le \frac{1}{{norm}_{ℎ}\left({A}\right)}$
32 24 31 absidd ${⊢}\left({A}\in ℋ\wedge {A}\ne {0}_{ℎ}\right)\to \left|\frac{1}{{norm}_{ℎ}\left({A}\right)}\right|=\frac{1}{{norm}_{ℎ}\left({A}\right)}$
33 32 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)$
34 24 recnd ${⊢}\left({A}\in ℋ\wedge {A}\ne {0}_{ℎ}\right)\to \frac{1}{{norm}_{ℎ}\left({A}\right)}\in ℂ$
35 simpl ${⊢}\left({A}\in ℋ\wedge {A}\ne {0}_{ℎ}\right)\to {A}\in ℋ$
36 1 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)$
37 34 35 36 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)$
38 37 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)$
39 1 lnopfi ${⊢}{T}:ℋ⟶ℋ$
40 39 ffvelrni ${⊢}{A}\in ℋ\to {T}\left({A}\right)\in ℋ$
41 40 adantr ${⊢}\left({A}\in ℋ\wedge {A}\ne {0}_{ℎ}\right)\to {T}\left({A}\right)\in ℋ$
42 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)$
43 34 41 42 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)$
44 38 43 eqtrd ${⊢}\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)=\left|\frac{1}{{norm}_{ℎ}\left({A}\right)}\right|{norm}_{ℎ}\left({T}\left({A}\right)\right)$
45 normcl ${⊢}{T}\left({A}\right)\in ℋ\to {norm}_{ℎ}\left({T}\left({A}\right)\right)\in ℝ$
46 40 45 syl ${⊢}{A}\in ℋ\to {norm}_{ℎ}\left({T}\left({A}\right)\right)\in ℝ$
47 46 adantr ${⊢}\left({A}\in ℋ\wedge {A}\ne {0}_{ℎ}\right)\to {norm}_{ℎ}\left({T}\left({A}\right)\right)\in ℝ$
48 47 recnd ${⊢}\left({A}\in ℋ\wedge {A}\ne {0}_{ℎ}\right)\to {norm}_{ℎ}\left({T}\left({A}\right)\right)\in ℂ$
49 21 recnd ${⊢}\left({A}\in ℋ\wedge {A}\ne {0}_{ℎ}\right)\to {norm}_{ℎ}\left({A}\right)\in ℂ$
50 48 49 23 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)$
51 33 44 50 3eqtr4rd ${⊢}\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)$
52 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 ℋ$
53 34 35 52 syl2anc ${⊢}\left({A}\in ℋ\wedge {A}\ne {0}_{ℎ}\right)\to \left(\frac{1}{{norm}_{ℎ}\left({A}\right)}\right){\cdot }_{ℎ}{A}\in ℋ$
54 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 ℝ$
55 53 54 syl ${⊢}\left({A}\in ℋ\wedge {A}\ne {0}_{ℎ}\right)\to {norm}_{ℎ}\left(\left(\frac{1}{{norm}_{ℎ}\left({A}\right)}\right){\cdot }_{ℎ}{A}\right)\in ℝ$
56 norm1 ${⊢}\left({A}\in ℋ\wedge {A}\ne {0}_{ℎ}\right)\to {norm}_{ℎ}\left(\left(\frac{1}{{norm}_{ℎ}\left({A}\right)}\right){\cdot }_{ℎ}{A}\right)=1$
57 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$
58 55 56 57 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$
59 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)$
60 39 59 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)$
61 53 58 60 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)$
62 51 61 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)$
63 14 a1i ${⊢}\left({A}\in ℋ\wedge {A}\ne {0}_{ℎ}\right)\to {norm}_{\mathrm{op}}\left({T}\right)\in ℝ$
64 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)$
65 47 63 21 26 64 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)$
66 62 65 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)$
67 19 66 pm2.61dane ${⊢}{A}\in ℋ\to {norm}_{ℎ}\left({T}\left({A}\right)\right)\le {norm}_{\mathrm{op}}\left({T}\right){norm}_{ℎ}\left({A}\right)$