Metamath Proof Explorer

Theorem nmoub2i

Description: An upper bound for an operator norm. (Contributed by NM, 11-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 nmoub2i ⊢ T : X ⟶ Y ∧ A ∈ ℝ ∧ 0 ≤ 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 2 3 4 5 6 7 nmoub3i ⊢ T : X ⟶ Y ∧ A ∈ ℝ ∧ ∀ x ∈ X M ⁡ T ⁡ x ≤ A ⁢ L ⁡ x → N ⁡ T ≤ A
9 8 3adant2r ⊢ T : X ⟶ Y ∧ A ∈ ℝ ∧ 0 ≤ A ∧ ∀ x ∈ X M ⁡ T ⁡ x ≤ A ⁢ L ⁡ x → N ⁡ T ≤ A
10 absid ⊢ A ∈ ℝ ∧ 0 ≤ A → A = A
11 10 3ad2ant2 ⊢ T : X ⟶ Y ∧ A ∈ ℝ ∧ 0 ≤ A ∧ ∀ x ∈ X M ⁡ T ⁡ x ≤ A ⁢ L ⁡ x → A = A
12 9 11 breqtrd ⊢ T : X ⟶ Y ∧ A ∈ ℝ ∧ 0 ≤ A ∧ ∀ x ∈ X M ⁡ T ⁡ x ≤ A ⁢ L ⁡ x → N ⁡ T ≤ A