Metamath Proof Explorer

Theorem nmoub3i

Description: An upper bound for an operator norm. (Contributed by NM, 12-Dec-2007) (New usage is discouraged.)

Ref Expression
Hypotheses nmoubi.1 ${⊢}{X}=\mathrm{BaseSet}\left({U}\right)$
nmoubi.y ${⊢}{Y}=\mathrm{BaseSet}\left({W}\right)$
nmoubi.l ${⊢}{L}={norm}_{CV}\left({U}\right)$
nmoubi.m ${⊢}{M}={norm}_{CV}\left({W}\right)$
nmoubi.3 ${⊢}{N}={U}{normOp}_{\mathrm{OLD}}{W}$
nmoubi.u ${⊢}{U}\in \mathrm{NrmCVec}$
nmoubi.w ${⊢}{W}\in \mathrm{NrmCVec}$
Assertion nmoub3i ${⊢}\left({T}:{X}⟶{Y}\wedge {A}\in ℝ\wedge \forall {x}\in {X}\phantom{\rule{.4em}{0ex}}{M}\left({T}\left({x}\right)\right)\le {A}{L}\left({x}\right)\right)\to {N}\left({T}\right)\le \left|{A}\right|$

Proof

Step Hyp Ref Expression
1 nmoubi.1 ${⊢}{X}=\mathrm{BaseSet}\left({U}\right)$
2 nmoubi.y ${⊢}{Y}=\mathrm{BaseSet}\left({W}\right)$
3 nmoubi.l ${⊢}{L}={norm}_{CV}\left({U}\right)$
4 nmoubi.m ${⊢}{M}={norm}_{CV}\left({W}\right)$
5 nmoubi.3 ${⊢}{N}={U}{normOp}_{\mathrm{OLD}}{W}$
6 nmoubi.u ${⊢}{U}\in \mathrm{NrmCVec}$
7 nmoubi.w ${⊢}{W}\in \mathrm{NrmCVec}$
8 1 3 nvcl ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {x}\in {X}\right)\to {L}\left({x}\right)\in ℝ$
9 6 8 mpan ${⊢}{x}\in {X}\to {L}\left({x}\right)\in ℝ$
10 remulcl ${⊢}\left({A}\in ℝ\wedge {L}\left({x}\right)\in ℝ\right)\to {A}{L}\left({x}\right)\in ℝ$
11 9 10 sylan2 ${⊢}\left({A}\in ℝ\wedge {x}\in {X}\right)\to {A}{L}\left({x}\right)\in ℝ$
12 11 adantr ${⊢}\left(\left({A}\in ℝ\wedge {x}\in {X}\right)\wedge {L}\left({x}\right)\le 1\right)\to {A}{L}\left({x}\right)\in ℝ$
13 recn ${⊢}{A}\in ℝ\to {A}\in ℂ$
14 13 abscld ${⊢}{A}\in ℝ\to \left|{A}\right|\in ℝ$
15 remulcl ${⊢}\left(\left|{A}\right|\in ℝ\wedge {L}\left({x}\right)\in ℝ\right)\to \left|{A}\right|{L}\left({x}\right)\in ℝ$
16 14 9 15 syl2an ${⊢}\left({A}\in ℝ\wedge {x}\in {X}\right)\to \left|{A}\right|{L}\left({x}\right)\in ℝ$
17 16 adantr ${⊢}\left(\left({A}\in ℝ\wedge {x}\in {X}\right)\wedge {L}\left({x}\right)\le 1\right)\to \left|{A}\right|{L}\left({x}\right)\in ℝ$
18 14 ad2antrr ${⊢}\left(\left({A}\in ℝ\wedge {x}\in {X}\right)\wedge {L}\left({x}\right)\le 1\right)\to \left|{A}\right|\in ℝ$
19 simpl ${⊢}\left({A}\in ℝ\wedge {x}\in {X}\right)\to {A}\in ℝ$
20 14 adantr ${⊢}\left({A}\in ℝ\wedge {x}\in {X}\right)\to \left|{A}\right|\in ℝ$
21 1 3 nvge0 ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {x}\in {X}\right)\to 0\le {L}\left({x}\right)$
22 6 21 mpan ${⊢}{x}\in {X}\to 0\le {L}\left({x}\right)$
23 9 22 jca ${⊢}{x}\in {X}\to \left({L}\left({x}\right)\in ℝ\wedge 0\le {L}\left({x}\right)\right)$
24 23 adantl ${⊢}\left({A}\in ℝ\wedge {x}\in {X}\right)\to \left({L}\left({x}\right)\in ℝ\wedge 0\le {L}\left({x}\right)\right)$
25 leabs ${⊢}{A}\in ℝ\to {A}\le \left|{A}\right|$
26 25 adantr ${⊢}\left({A}\in ℝ\wedge {x}\in {X}\right)\to {A}\le \left|{A}\right|$
27 lemul1a ${⊢}\left(\left({A}\in ℝ\wedge \left|{A}\right|\in ℝ\wedge \left({L}\left({x}\right)\in ℝ\wedge 0\le {L}\left({x}\right)\right)\right)\wedge {A}\le \left|{A}\right|\right)\to {A}{L}\left({x}\right)\le \left|{A}\right|{L}\left({x}\right)$
28 19 20 24 26 27 syl31anc ${⊢}\left({A}\in ℝ\wedge {x}\in {X}\right)\to {A}{L}\left({x}\right)\le \left|{A}\right|{L}\left({x}\right)$
29 28 adantr ${⊢}\left(\left({A}\in ℝ\wedge {x}\in {X}\right)\wedge {L}\left({x}\right)\le 1\right)\to {A}{L}\left({x}\right)\le \left|{A}\right|{L}\left({x}\right)$
30 9 adantl ${⊢}\left({A}\in ℝ\wedge {x}\in {X}\right)\to {L}\left({x}\right)\in ℝ$
31 1red ${⊢}\left({A}\in ℝ\wedge {x}\in {X}\right)\to 1\in ℝ$
32 13 absge0d ${⊢}{A}\in ℝ\to 0\le \left|{A}\right|$
33 32 adantr ${⊢}\left({A}\in ℝ\wedge {x}\in {X}\right)\to 0\le \left|{A}\right|$
34 20 33 jca ${⊢}\left({A}\in ℝ\wedge {x}\in {X}\right)\to \left(\left|{A}\right|\in ℝ\wedge 0\le \left|{A}\right|\right)$
35 30 31 34 3jca ${⊢}\left({A}\in ℝ\wedge {x}\in {X}\right)\to \left({L}\left({x}\right)\in ℝ\wedge 1\in ℝ\wedge \left(\left|{A}\right|\in ℝ\wedge 0\le \left|{A}\right|\right)\right)$
36 lemul2a ${⊢}\left(\left({L}\left({x}\right)\in ℝ\wedge 1\in ℝ\wedge \left(\left|{A}\right|\in ℝ\wedge 0\le \left|{A}\right|\right)\right)\wedge {L}\left({x}\right)\le 1\right)\to \left|{A}\right|{L}\left({x}\right)\le \left|{A}\right|\cdot 1$
37 35 36 sylan ${⊢}\left(\left({A}\in ℝ\wedge {x}\in {X}\right)\wedge {L}\left({x}\right)\le 1\right)\to \left|{A}\right|{L}\left({x}\right)\le \left|{A}\right|\cdot 1$
38 14 recnd ${⊢}{A}\in ℝ\to \left|{A}\right|\in ℂ$
39 38 mulid1d ${⊢}{A}\in ℝ\to \left|{A}\right|\cdot 1=\left|{A}\right|$
40 39 ad2antrr ${⊢}\left(\left({A}\in ℝ\wedge {x}\in {X}\right)\wedge {L}\left({x}\right)\le 1\right)\to \left|{A}\right|\cdot 1=\left|{A}\right|$
41 37 40 breqtrd ${⊢}\left(\left({A}\in ℝ\wedge {x}\in {X}\right)\wedge {L}\left({x}\right)\le 1\right)\to \left|{A}\right|{L}\left({x}\right)\le \left|{A}\right|$
42 12 17 18 29 41 letrd ${⊢}\left(\left({A}\in ℝ\wedge {x}\in {X}\right)\wedge {L}\left({x}\right)\le 1\right)\to {A}{L}\left({x}\right)\le \left|{A}\right|$
43 42 adantlll ${⊢}\left(\left(\left({T}:{X}⟶{Y}\wedge {A}\in ℝ\right)\wedge {x}\in {X}\right)\wedge {L}\left({x}\right)\le 1\right)\to {A}{L}\left({x}\right)\le \left|{A}\right|$
44 ffvelrn ${⊢}\left({T}:{X}⟶{Y}\wedge {x}\in {X}\right)\to {T}\left({x}\right)\in {Y}$
45 2 4 nvcl ${⊢}\left({W}\in \mathrm{NrmCVec}\wedge {T}\left({x}\right)\in {Y}\right)\to {M}\left({T}\left({x}\right)\right)\in ℝ$
46 7 44 45 sylancr ${⊢}\left({T}:{X}⟶{Y}\wedge {x}\in {X}\right)\to {M}\left({T}\left({x}\right)\right)\in ℝ$
47 46 adantlr ${⊢}\left(\left({T}:{X}⟶{Y}\wedge {A}\in ℝ\right)\wedge {x}\in {X}\right)\to {M}\left({T}\left({x}\right)\right)\in ℝ$
48 11 adantll ${⊢}\left(\left({T}:{X}⟶{Y}\wedge {A}\in ℝ\right)\wedge {x}\in {X}\right)\to {A}{L}\left({x}\right)\in ℝ$
49 14 ad2antlr ${⊢}\left(\left({T}:{X}⟶{Y}\wedge {A}\in ℝ\right)\wedge {x}\in {X}\right)\to \left|{A}\right|\in ℝ$
50 letr ${⊢}\left({M}\left({T}\left({x}\right)\right)\in ℝ\wedge {A}{L}\left({x}\right)\in ℝ\wedge \left|{A}\right|\in ℝ\right)\to \left(\left({M}\left({T}\left({x}\right)\right)\le {A}{L}\left({x}\right)\wedge {A}{L}\left({x}\right)\le \left|{A}\right|\right)\to {M}\left({T}\left({x}\right)\right)\le \left|{A}\right|\right)$
51 47 48 49 50 syl3anc ${⊢}\left(\left({T}:{X}⟶{Y}\wedge {A}\in ℝ\right)\wedge {x}\in {X}\right)\to \left(\left({M}\left({T}\left({x}\right)\right)\le {A}{L}\left({x}\right)\wedge {A}{L}\left({x}\right)\le \left|{A}\right|\right)\to {M}\left({T}\left({x}\right)\right)\le \left|{A}\right|\right)$
52 51 adantr ${⊢}\left(\left(\left({T}:{X}⟶{Y}\wedge {A}\in ℝ\right)\wedge {x}\in {X}\right)\wedge {L}\left({x}\right)\le 1\right)\to \left(\left({M}\left({T}\left({x}\right)\right)\le {A}{L}\left({x}\right)\wedge {A}{L}\left({x}\right)\le \left|{A}\right|\right)\to {M}\left({T}\left({x}\right)\right)\le \left|{A}\right|\right)$
53 43 52 mpan2d ${⊢}\left(\left(\left({T}:{X}⟶{Y}\wedge {A}\in ℝ\right)\wedge {x}\in {X}\right)\wedge {L}\left({x}\right)\le 1\right)\to \left({M}\left({T}\left({x}\right)\right)\le {A}{L}\left({x}\right)\to {M}\left({T}\left({x}\right)\right)\le \left|{A}\right|\right)$
54 53 ex ${⊢}\left(\left({T}:{X}⟶{Y}\wedge {A}\in ℝ\right)\wedge {x}\in {X}\right)\to \left({L}\left({x}\right)\le 1\to \left({M}\left({T}\left({x}\right)\right)\le {A}{L}\left({x}\right)\to {M}\left({T}\left({x}\right)\right)\le \left|{A}\right|\right)\right)$
55 54 com23 ${⊢}\left(\left({T}:{X}⟶{Y}\wedge {A}\in ℝ\right)\wedge {x}\in {X}\right)\to \left({M}\left({T}\left({x}\right)\right)\le {A}{L}\left({x}\right)\to \left({L}\left({x}\right)\le 1\to {M}\left({T}\left({x}\right)\right)\le \left|{A}\right|\right)\right)$
56 55 ralimdva ${⊢}\left({T}:{X}⟶{Y}\wedge {A}\in ℝ\right)\to \left(\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}{M}\left({T}\left({x}\right)\right)\le {A}{L}\left({x}\right)\to \forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\left({L}\left({x}\right)\le 1\to {M}\left({T}\left({x}\right)\right)\le \left|{A}\right|\right)\right)$
57 56 imp ${⊢}\left(\left({T}:{X}⟶{Y}\wedge {A}\in ℝ\right)\wedge \forall {x}\in {X}\phantom{\rule{.4em}{0ex}}{M}\left({T}\left({x}\right)\right)\le {A}{L}\left({x}\right)\right)\to \forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\left({L}\left({x}\right)\le 1\to {M}\left({T}\left({x}\right)\right)\le \left|{A}\right|\right)$
58 14 rexrd ${⊢}{A}\in ℝ\to \left|{A}\right|\in {ℝ}^{*}$
59 1 2 3 4 5 6 7 nmoubi ${⊢}\left({T}:{X}⟶{Y}\wedge \left|{A}\right|\in {ℝ}^{*}\right)\to \left({N}\left({T}\right)\le \left|{A}\right|↔\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\left({L}\left({x}\right)\le 1\to {M}\left({T}\left({x}\right)\right)\le \left|{A}\right|\right)\right)$
60 58 59 sylan2 ${⊢}\left({T}:{X}⟶{Y}\wedge {A}\in ℝ\right)\to \left({N}\left({T}\right)\le \left|{A}\right|↔\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\left({L}\left({x}\right)\le 1\to {M}\left({T}\left({x}\right)\right)\le \left|{A}\right|\right)\right)$
61 60 biimpar ${⊢}\left(\left({T}:{X}⟶{Y}\wedge {A}\in ℝ\right)\wedge \forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\left({L}\left({x}\right)\le 1\to {M}\left({T}\left({x}\right)\right)\le \left|{A}\right|\right)\right)\to {N}\left({T}\right)\le \left|{A}\right|$
62 57 61 syldan ${⊢}\left(\left({T}:{X}⟶{Y}\wedge {A}\in ℝ\right)\wedge \forall {x}\in {X}\phantom{\rule{.4em}{0ex}}{M}\left({T}\left({x}\right)\right)\le {A}{L}\left({x}\right)\right)\to {N}\left({T}\right)\le \left|{A}\right|$
63 62 3impa ${⊢}\left({T}:{X}⟶{Y}\wedge {A}\in ℝ\wedge \forall {x}\in {X}\phantom{\rule{.4em}{0ex}}{M}\left({T}\left({x}\right)\right)\le {A}{L}\left({x}\right)\right)\to {N}\left({T}\right)\le \left|{A}\right|$