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 ⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
nmoubi.y ⊢ 𝑌 = ( BaseSet ‘ 𝑊 )
nmoubi.l ⊢ 𝐿 = ( normCV ‘ 𝑈 )
nmoubi.m ⊢ 𝑀 = ( normCV ‘ 𝑊 )
nmoubi.3 ⊢ 𝑁 = ( 𝑈 normOpOLD 𝑊 )
nmoubi.u ⊢ 𝑈 ∈ NrmCVec
nmoubi.w ⊢ 𝑊 ∈ NrmCVec
Assertion nmoub3i ( ( 𝑇 : 𝑋 ⟶ 𝑌 ∧ 𝐴 ∈ ℝ ∧ ∀ 𝑥 ∈ 𝑋 ( 𝑀 ‘ ( 𝑇 ‘ 𝑥 ) ) ≤ ( 𝐴 · ( 𝐿 ‘ 𝑥 ) ) ) → ( 𝑁 ‘ 𝑇 ) ≤ ( abs ‘ 𝐴 ) )

Proof

Step Hyp Ref Expression
1 nmoubi.1 ⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
2 nmoubi.y ⊢ 𝑌 = ( BaseSet ‘ 𝑊 )
3 nmoubi.l ⊢ 𝐿 = ( normCV ‘ 𝑈 )
4 nmoubi.m ⊢ 𝑀 = ( normCV ‘ 𝑊 )
5 nmoubi.3 ⊢ 𝑁 = ( 𝑈 normOpOLD 𝑊 )
6 nmoubi.u ⊢ 𝑈 ∈ NrmCVec
7 nmoubi.w ⊢ 𝑊 ∈ NrmCVec
8 1 3 nvcl ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑥 ∈ 𝑋 ) → ( 𝐿 ‘ 𝑥 ) ∈ ℝ )
9 6 8 mpan ⊢ ( 𝑥 ∈ 𝑋 → ( 𝐿 ‘ 𝑥 ) ∈ ℝ )
10 remulcl ⊢ ( ( 𝐴 ∈ ℝ ∧ ( 𝐿 ‘ 𝑥 ) ∈ ℝ ) → ( 𝐴 · ( 𝐿 ‘ 𝑥 ) ) ∈ ℝ )
11 9 10 sylan2 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑥 ∈ 𝑋 ) → ( 𝐴 · ( 𝐿 ‘ 𝑥 ) ) ∈ ℝ )
12 11 adantr ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝑥 ∈ 𝑋 ) ∧ ( 𝐿 ‘ 𝑥 ) ≤ 1 ) → ( 𝐴 · ( 𝐿 ‘ 𝑥 ) ) ∈ ℝ )
13 recn ⊢ ( 𝐴 ∈ ℝ → 𝐴 ∈ ℂ )
14 13 abscld ⊢ ( 𝐴 ∈ ℝ → ( abs ‘ 𝐴 ) ∈ ℝ )
15 remulcl ⊢ ( ( ( abs ‘ 𝐴 ) ∈ ℝ ∧ ( 𝐿 ‘ 𝑥 ) ∈ ℝ ) → ( ( abs ‘ 𝐴 ) · ( 𝐿 ‘ 𝑥 ) ) ∈ ℝ )
16 14 9 15 syl2an ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑥 ∈ 𝑋 ) → ( ( abs ‘ 𝐴 ) · ( 𝐿 ‘ 𝑥 ) ) ∈ ℝ )
17 16 adantr ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝑥 ∈ 𝑋 ) ∧ ( 𝐿 ‘ 𝑥 ) ≤ 1 ) → ( ( abs ‘ 𝐴 ) · ( 𝐿 ‘ 𝑥 ) ) ∈ ℝ )
18 14 ad2antrr ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝑥 ∈ 𝑋 ) ∧ ( 𝐿 ‘ 𝑥 ) ≤ 1 ) → ( abs ‘ 𝐴 ) ∈ ℝ )
19 simpl ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑥 ∈ 𝑋 ) → 𝐴 ∈ ℝ )
20 14 adantr ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑥 ∈ 𝑋 ) → ( abs ‘ 𝐴 ) ∈ ℝ )
21 1 3 nvge0 ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑥 ∈ 𝑋 ) → 0 ≤ ( 𝐿 ‘ 𝑥 ) )
22 6 21 mpan ⊢ ( 𝑥 ∈ 𝑋 → 0 ≤ ( 𝐿 ‘ 𝑥 ) )
23 9 22 jca ⊢ ( 𝑥 ∈ 𝑋 → ( ( 𝐿 ‘ 𝑥 ) ∈ ℝ ∧ 0 ≤ ( 𝐿 ‘ 𝑥 ) ) )
24 23 adantl ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑥 ∈ 𝑋 ) → ( ( 𝐿 ‘ 𝑥 ) ∈ ℝ ∧ 0 ≤ ( 𝐿 ‘ 𝑥 ) ) )
25 leabs ⊢ ( 𝐴 ∈ ℝ → 𝐴 ≤ ( abs ‘ 𝐴 ) )
26 25 adantr ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑥 ∈ 𝑋 ) → 𝐴 ≤ ( abs ‘ 𝐴 ) )
27 lemul1a ⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( abs ‘ 𝐴 ) ∈ ℝ ∧ ( ( 𝐿 ‘ 𝑥 ) ∈ ℝ ∧ 0 ≤ ( 𝐿 ‘ 𝑥 ) ) ) ∧ 𝐴 ≤ ( abs ‘ 𝐴 ) ) → ( 𝐴 · ( 𝐿 ‘ 𝑥 ) ) ≤ ( ( abs ‘ 𝐴 ) · ( 𝐿 ‘ 𝑥 ) ) )
28 19 20 24 26 27 syl31anc ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑥 ∈ 𝑋 ) → ( 𝐴 · ( 𝐿 ‘ 𝑥 ) ) ≤ ( ( abs ‘ 𝐴 ) · ( 𝐿 ‘ 𝑥 ) ) )
29 28 adantr ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝑥 ∈ 𝑋 ) ∧ ( 𝐿 ‘ 𝑥 ) ≤ 1 ) → ( 𝐴 · ( 𝐿 ‘ 𝑥 ) ) ≤ ( ( abs ‘ 𝐴 ) · ( 𝐿 ‘ 𝑥 ) ) )
30 9 adantl ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑥 ∈ 𝑋 ) → ( 𝐿 ‘ 𝑥 ) ∈ ℝ )
31 1red ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑥 ∈ 𝑋 ) → 1 ∈ ℝ )
32 13 absge0d ⊢ ( 𝐴 ∈ ℝ → 0 ≤ ( abs ‘ 𝐴 ) )
33 32 adantr ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑥 ∈ 𝑋 ) → 0 ≤ ( abs ‘ 𝐴 ) )
34 20 33 jca ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑥 ∈ 𝑋 ) → ( ( abs ‘ 𝐴 ) ∈ ℝ ∧ 0 ≤ ( abs ‘ 𝐴 ) ) )
35 30 31 34 3jca ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑥 ∈ 𝑋 ) → ( ( 𝐿 ‘ 𝑥 ) ∈ ℝ ∧ 1 ∈ ℝ ∧ ( ( abs ‘ 𝐴 ) ∈ ℝ ∧ 0 ≤ ( abs ‘ 𝐴 ) ) ) )
36 lemul2a ⊢ ( ( ( ( 𝐿 ‘ 𝑥 ) ∈ ℝ ∧ 1 ∈ ℝ ∧ ( ( abs ‘ 𝐴 ) ∈ ℝ ∧ 0 ≤ ( abs ‘ 𝐴 ) ) ) ∧ ( 𝐿 ‘ 𝑥 ) ≤ 1 ) → ( ( abs ‘ 𝐴 ) · ( 𝐿 ‘ 𝑥 ) ) ≤ ( ( abs ‘ 𝐴 ) · 1 ) )
37 35 36 sylan ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝑥 ∈ 𝑋 ) ∧ ( 𝐿 ‘ 𝑥 ) ≤ 1 ) → ( ( abs ‘ 𝐴 ) · ( 𝐿 ‘ 𝑥 ) ) ≤ ( ( abs ‘ 𝐴 ) · 1 ) )
38 14 recnd ⊢ ( 𝐴 ∈ ℝ → ( abs ‘ 𝐴 ) ∈ ℂ )
39 38 mulid1d ⊢ ( 𝐴 ∈ ℝ → ( ( abs ‘ 𝐴 ) · 1 ) = ( abs ‘ 𝐴 ) )
40 39 ad2antrr ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝑥 ∈ 𝑋 ) ∧ ( 𝐿 ‘ 𝑥 ) ≤ 1 ) → ( ( abs ‘ 𝐴 ) · 1 ) = ( abs ‘ 𝐴 ) )
41 37 40 breqtrd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝑥 ∈ 𝑋 ) ∧ ( 𝐿 ‘ 𝑥 ) ≤ 1 ) → ( ( abs ‘ 𝐴 ) · ( 𝐿 ‘ 𝑥 ) ) ≤ ( abs ‘ 𝐴 ) )
42 12 17 18 29 41 letrd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝑥 ∈ 𝑋 ) ∧ ( 𝐿 ‘ 𝑥 ) ≤ 1 ) → ( 𝐴 · ( 𝐿 ‘ 𝑥 ) ) ≤ ( abs ‘ 𝐴 ) )
43 42 adantlll ⊢ ( ( ( ( 𝑇 : 𝑋 ⟶ 𝑌 ∧ 𝐴 ∈ ℝ ) ∧ 𝑥 ∈ 𝑋 ) ∧ ( 𝐿 ‘ 𝑥 ) ≤ 1 ) → ( 𝐴 · ( 𝐿 ‘ 𝑥 ) ) ≤ ( abs ‘ 𝐴 ) )
44 ffvelrn ⊢ ( ( 𝑇 : 𝑋 ⟶ 𝑌 ∧ 𝑥 ∈ 𝑋 ) → ( 𝑇 ‘ 𝑥 ) ∈ 𝑌 )
45 2 4 nvcl ⊢ ( ( 𝑊 ∈ NrmCVec ∧ ( 𝑇 ‘ 𝑥 ) ∈ 𝑌 ) → ( 𝑀 ‘ ( 𝑇 ‘ 𝑥 ) ) ∈ ℝ )
46 7 44 45 sylancr ⊢ ( ( 𝑇 : 𝑋 ⟶ 𝑌 ∧ 𝑥 ∈ 𝑋 ) → ( 𝑀 ‘ ( 𝑇 ‘ 𝑥 ) ) ∈ ℝ )
47 46 adantlr ⊢ ( ( ( 𝑇 : 𝑋 ⟶ 𝑌 ∧ 𝐴 ∈ ℝ ) ∧ 𝑥 ∈ 𝑋 ) → ( 𝑀 ‘ ( 𝑇 ‘ 𝑥 ) ) ∈ ℝ )
48 11 adantll ⊢ ( ( ( 𝑇 : 𝑋 ⟶ 𝑌 ∧ 𝐴 ∈ ℝ ) ∧ 𝑥 ∈ 𝑋 ) → ( 𝐴 · ( 𝐿 ‘ 𝑥 ) ) ∈ ℝ )
49 14 ad2antlr ⊢ ( ( ( 𝑇 : 𝑋 ⟶ 𝑌 ∧ 𝐴 ∈ ℝ ) ∧ 𝑥 ∈ 𝑋 ) → ( abs ‘ 𝐴 ) ∈ ℝ )
50 letr ⊢ ( ( ( 𝑀 ‘ ( 𝑇 ‘ 𝑥 ) ) ∈ ℝ ∧ ( 𝐴 · ( 𝐿 ‘ 𝑥 ) ) ∈ ℝ ∧ ( abs ‘ 𝐴 ) ∈ ℝ ) → ( ( ( 𝑀 ‘ ( 𝑇 ‘ 𝑥 ) ) ≤ ( 𝐴 · ( 𝐿 ‘ 𝑥 ) ) ∧ ( 𝐴 · ( 𝐿 ‘ 𝑥 ) ) ≤ ( abs ‘ 𝐴 ) ) → ( 𝑀 ‘ ( 𝑇 ‘ 𝑥 ) ) ≤ ( abs ‘ 𝐴 ) ) )
51 47 48 49 50 syl3anc ⊢ ( ( ( 𝑇 : 𝑋 ⟶ 𝑌 ∧ 𝐴 ∈ ℝ ) ∧ 𝑥 ∈ 𝑋 ) → ( ( ( 𝑀 ‘ ( 𝑇 ‘ 𝑥 ) ) ≤ ( 𝐴 · ( 𝐿 ‘ 𝑥 ) ) ∧ ( 𝐴 · ( 𝐿 ‘ 𝑥 ) ) ≤ ( abs ‘ 𝐴 ) ) → ( 𝑀 ‘ ( 𝑇 ‘ 𝑥 ) ) ≤ ( abs ‘ 𝐴 ) ) )
52 51 adantr ⊢ ( ( ( ( 𝑇 : 𝑋 ⟶ 𝑌 ∧ 𝐴 ∈ ℝ ) ∧ 𝑥 ∈ 𝑋 ) ∧ ( 𝐿 ‘ 𝑥 ) ≤ 1 ) → ( ( ( 𝑀 ‘ ( 𝑇 ‘ 𝑥 ) ) ≤ ( 𝐴 · ( 𝐿 ‘ 𝑥 ) ) ∧ ( 𝐴 · ( 𝐿 ‘ 𝑥 ) ) ≤ ( abs ‘ 𝐴 ) ) → ( 𝑀 ‘ ( 𝑇 ‘ 𝑥 ) ) ≤ ( abs ‘ 𝐴 ) ) )
53 43 52 mpan2d ⊢ ( ( ( ( 𝑇 : 𝑋 ⟶ 𝑌 ∧ 𝐴 ∈ ℝ ) ∧ 𝑥 ∈ 𝑋 ) ∧ ( 𝐿 ‘ 𝑥 ) ≤ 1 ) → ( ( 𝑀 ‘ ( 𝑇 ‘ 𝑥 ) ) ≤ ( 𝐴 · ( 𝐿 ‘ 𝑥 ) ) → ( 𝑀 ‘ ( 𝑇 ‘ 𝑥 ) ) ≤ ( abs ‘ 𝐴 ) ) )
54 53 ex ⊢ ( ( ( 𝑇 : 𝑋 ⟶ 𝑌 ∧ 𝐴 ∈ ℝ ) ∧ 𝑥 ∈ 𝑋 ) → ( ( 𝐿 ‘ 𝑥 ) ≤ 1 → ( ( 𝑀 ‘ ( 𝑇 ‘ 𝑥 ) ) ≤ ( 𝐴 · ( 𝐿 ‘ 𝑥 ) ) → ( 𝑀 ‘ ( 𝑇 ‘ 𝑥 ) ) ≤ ( abs ‘ 𝐴 ) ) ) )
55 54 com23 ⊢ ( ( ( 𝑇 : 𝑋 ⟶ 𝑌 ∧ 𝐴 ∈ ℝ ) ∧ 𝑥 ∈ 𝑋 ) → ( ( 𝑀 ‘ ( 𝑇 ‘ 𝑥 ) ) ≤ ( 𝐴 · ( 𝐿 ‘ 𝑥 ) ) → ( ( 𝐿 ‘ 𝑥 ) ≤ 1 → ( 𝑀 ‘ ( 𝑇 ‘ 𝑥 ) ) ≤ ( abs ‘ 𝐴 ) ) ) )
56 55 ralimdva ⊢ ( ( 𝑇 : 𝑋 ⟶ 𝑌 ∧ 𝐴 ∈ ℝ ) → ( ∀ 𝑥 ∈ 𝑋 ( 𝑀 ‘ ( 𝑇 ‘ 𝑥 ) ) ≤ ( 𝐴 · ( 𝐿 ‘ 𝑥 ) ) → ∀ 𝑥 ∈ 𝑋 ( ( 𝐿 ‘ 𝑥 ) ≤ 1 → ( 𝑀 ‘ ( 𝑇 ‘ 𝑥 ) ) ≤ ( abs ‘ 𝐴 ) ) ) )
57 56 imp ⊢ ( ( ( 𝑇 : 𝑋 ⟶ 𝑌 ∧ 𝐴 ∈ ℝ ) ∧ ∀ 𝑥 ∈ 𝑋 ( 𝑀 ‘ ( 𝑇 ‘ 𝑥 ) ) ≤ ( 𝐴 · ( 𝐿 ‘ 𝑥 ) ) ) → ∀ 𝑥 ∈ 𝑋 ( ( 𝐿 ‘ 𝑥 ) ≤ 1 → ( 𝑀 ‘ ( 𝑇 ‘ 𝑥 ) ) ≤ ( abs ‘ 𝐴 ) ) )
58 14 rexrd ⊢ ( 𝐴 ∈ ℝ → ( abs ‘ 𝐴 ) ∈ ℝ* )
59 1 2 3 4 5 6 7 nmoubi ⊢ ( ( 𝑇 : 𝑋 ⟶ 𝑌 ∧ ( abs ‘ 𝐴 ) ∈ ℝ* ) → ( ( 𝑁 ‘ 𝑇 ) ≤ ( abs ‘ 𝐴 ) ↔ ∀ 𝑥 ∈ 𝑋 ( ( 𝐿 ‘ 𝑥 ) ≤ 1 → ( 𝑀 ‘ ( 𝑇 ‘ 𝑥 ) ) ≤ ( abs ‘ 𝐴 ) ) ) )
60 58 59 sylan2 ⊢ ( ( 𝑇 : 𝑋 ⟶ 𝑌 ∧ 𝐴 ∈ ℝ ) → ( ( 𝑁 ‘ 𝑇 ) ≤ ( abs ‘ 𝐴 ) ↔ ∀ 𝑥 ∈ 𝑋 ( ( 𝐿 ‘ 𝑥 ) ≤ 1 → ( 𝑀 ‘ ( 𝑇 ‘ 𝑥 ) ) ≤ ( abs ‘ 𝐴 ) ) ) )
61 60 biimpar ⊢ ( ( ( 𝑇 : 𝑋 ⟶ 𝑌 ∧ 𝐴 ∈ ℝ ) ∧ ∀ 𝑥 ∈ 𝑋 ( ( 𝐿 ‘ 𝑥 ) ≤ 1 → ( 𝑀 ‘ ( 𝑇 ‘ 𝑥 ) ) ≤ ( abs ‘ 𝐴 ) ) ) → ( 𝑁 ‘ 𝑇 ) ≤ ( abs ‘ 𝐴 ) )
62 57 61 syldan ⊢ ( ( ( 𝑇 : 𝑋 ⟶ 𝑌 ∧ 𝐴 ∈ ℝ ) ∧ ∀ 𝑥 ∈ 𝑋 ( 𝑀 ‘ ( 𝑇 ‘ 𝑥 ) ) ≤ ( 𝐴 · ( 𝐿 ‘ 𝑥 ) ) ) → ( 𝑁 ‘ 𝑇 ) ≤ ( abs ‘ 𝐴 ) )
63 62 3impa ⊢ ( ( 𝑇 : 𝑋 ⟶ 𝑌 ∧ 𝐴 ∈ ℝ ∧ ∀ 𝑥 ∈ 𝑋 ( 𝑀 ‘ ( 𝑇 ‘ 𝑥 ) ) ≤ ( 𝐴 · ( 𝐿 ‘ 𝑥 ) ) ) → ( 𝑁 ‘ 𝑇 ) ≤ ( abs ‘ 𝐴 ) )