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 = BaseSet ⁡ U
nmoubi.y ⊢ Y = BaseSet ⁡ W
nmoubi.l ⊢ L = norm CV ⁡ U
nmoubi.m ⊢ M = norm CV ⁡ W
nmoubi.3 ⊢ N = U normOp OLD W
nmoubi.u ⊢ U ∈ NrmCVec
nmoubi.w ⊢ W ∈ NrmCVec
Assertion nmoub3i ⊢ T : X ⟶ Y ∧ A ∈ ℝ ∧ ∀ x ∈ X M ⁡ T ⁡ x ≤ A ⁢ L ⁡ x → N ⁡ T ≤ A

Proof

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