Metamath Proof Explorer

Theorem nmooge0

Description: The norm of an operator is nonnegative. (Contributed by NM, 8-Dec-2007) (New usage is discouraged.)

Ref Expression
Hypotheses nmoxr.1 ⊢ X = BaseSet ⁡ U
nmoxr.2 ⊢ Y = BaseSet ⁡ W
nmoxr.3 ⊢ N = U normOp OLD W
Assertion nmooge0 ⊢ U ∈ NrmCVec ∧ W ∈ NrmCVec ∧ T : X ⟶ Y → 0 ≤ N ⁡ T

Proof

Step Hyp Ref Expression
1 nmoxr.1 ⊢ X = BaseSet ⁡ U
2 nmoxr.2 ⊢ Y = BaseSet ⁡ W
3 nmoxr.3 ⊢ N = U normOp OLD W
4 0xr ⊢ 0 ∈ ℝ *
5 4 a1i ⊢ U ∈ NrmCVec ∧ W ∈ NrmCVec ∧ T : X ⟶ Y → 0 ∈ ℝ *
6 simp2 ⊢ U ∈ NrmCVec ∧ W ∈ NrmCVec ∧ T : X ⟶ Y → W ∈ NrmCVec
7 eqid ⊢ 0 vec ⁡ U = 0 vec ⁡ U
8 1 7 nvzcl ⊢ U ∈ NrmCVec → 0 vec ⁡ U ∈ X
9 ffvelcdm ⊢ T : X ⟶ Y ∧ 0 vec ⁡ U ∈ X → T ⁡ 0 vec ⁡ U ∈ Y
10 8 9 sylan2 ⊢ T : X ⟶ Y ∧ U ∈ NrmCVec → T ⁡ 0 vec ⁡ U ∈ Y
11 10 ancoms ⊢ U ∈ NrmCVec ∧ T : X ⟶ Y → T ⁡ 0 vec ⁡ U ∈ Y
12 11 3adant2 ⊢ U ∈ NrmCVec ∧ W ∈ NrmCVec ∧ T : X ⟶ Y → T ⁡ 0 vec ⁡ U ∈ Y
13 eqid ⊢ norm CV ⁡ W = norm CV ⁡ W
14 2 13 nvcl ⊢ W ∈ NrmCVec ∧ T ⁡ 0 vec ⁡ U ∈ Y → norm CV ⁡ W ⁡ T ⁡ 0 vec ⁡ U ∈ ℝ
15 6 12 14 syl2anc ⊢ U ∈ NrmCVec ∧ W ∈ NrmCVec ∧ T : X ⟶ Y → norm CV ⁡ W ⁡ T ⁡ 0 vec ⁡ U ∈ ℝ
16 15 rexrd ⊢ U ∈ NrmCVec ∧ W ∈ NrmCVec ∧ T : X ⟶ Y → norm CV ⁡ W ⁡ T ⁡ 0 vec ⁡ U ∈ ℝ *
17 1 2 3 nmoxr ⊢ U ∈ NrmCVec ∧ W ∈ NrmCVec ∧ T : X ⟶ Y → N ⁡ T ∈ ℝ *
18 2 13 nvge0 ⊢ W ∈ NrmCVec ∧ T ⁡ 0 vec ⁡ U ∈ Y → 0 ≤ norm CV ⁡ W ⁡ T ⁡ 0 vec ⁡ U
19 6 12 18 syl2anc ⊢ U ∈ NrmCVec ∧ W ∈ NrmCVec ∧ T : X ⟶ Y → 0 ≤ norm CV ⁡ W ⁡ T ⁡ 0 vec ⁡ U
20 2 13 nmosetre ⊢ W ∈ NrmCVec ∧ T : X ⟶ Y → x | ∃ z ∈ X norm CV ⁡ U ⁡ z ≤ 1 ∧ x = norm CV ⁡ W ⁡ T ⁡ z ⊆ ℝ
21 ressxr ⊢ ℝ ⊆ ℝ *
22 20 21 sstrdi ⊢ W ∈ NrmCVec ∧ T : X ⟶ Y → x | ∃ z ∈ X norm CV ⁡ U ⁡ z ≤ 1 ∧ x = norm CV ⁡ W ⁡ T ⁡ z ⊆ ℝ *
23 eqid ⊢ norm CV ⁡ U = norm CV ⁡ U
24 1 7 23 nmosetn0 ⊢ U ∈ NrmCVec → norm CV ⁡ W ⁡ T ⁡ 0 vec ⁡ U ∈ x | ∃ z ∈ X norm CV ⁡ U ⁡ z ≤ 1 ∧ x = norm CV ⁡ W ⁡ T ⁡ z
25 supxrub ⊢ x | ∃ z ∈ X norm CV ⁡ U ⁡ z ≤ 1 ∧ x = norm CV ⁡ W ⁡ T ⁡ z ⊆ ℝ * ∧ norm CV ⁡ W ⁡ T ⁡ 0 vec ⁡ U ∈ x | ∃ z ∈ X norm CV ⁡ U ⁡ z ≤ 1 ∧ x = norm CV ⁡ W ⁡ T ⁡ z → norm CV ⁡ W ⁡ T ⁡ 0 vec ⁡ U ≤ sup x | ∃ z ∈ X norm CV ⁡ U ⁡ z ≤ 1 ∧ x = norm CV ⁡ W ⁡ T ⁡ z ℝ * <
26 22 24 25 syl2an ⊢ W ∈ NrmCVec ∧ T : X ⟶ Y ∧ U ∈ NrmCVec → norm CV ⁡ W ⁡ T ⁡ 0 vec ⁡ U ≤ sup x | ∃ z ∈ X norm CV ⁡ U ⁡ z ≤ 1 ∧ x = norm CV ⁡ W ⁡ T ⁡ z ℝ * <
27 26 3impa ⊢ W ∈ NrmCVec ∧ T : X ⟶ Y ∧ U ∈ NrmCVec → norm CV ⁡ W ⁡ T ⁡ 0 vec ⁡ U ≤ sup x | ∃ z ∈ X norm CV ⁡ U ⁡ z ≤ 1 ∧ x = norm CV ⁡ W ⁡ T ⁡ z ℝ * <
28 27 3comr ⊢ U ∈ NrmCVec ∧ W ∈ NrmCVec ∧ T : X ⟶ Y → norm CV ⁡ W ⁡ T ⁡ 0 vec ⁡ U ≤ sup x | ∃ z ∈ X norm CV ⁡ U ⁡ z ≤ 1 ∧ x = norm CV ⁡ W ⁡ T ⁡ z ℝ * <
29 1 2 23 13 3 nmooval ⊢ U ∈ NrmCVec ∧ W ∈ NrmCVec ∧ T : X ⟶ Y → N ⁡ T = sup x | ∃ z ∈ X norm CV ⁡ U ⁡ z ≤ 1 ∧ x = norm CV ⁡ W ⁡ T ⁡ z ℝ * <
30 28 29 breqtrrd ⊢ U ∈ NrmCVec ∧ W ∈ NrmCVec ∧ T : X ⟶ Y → norm CV ⁡ W ⁡ T ⁡ 0 vec ⁡ U ≤ N ⁡ T
31 5 16 17 19 30 xrletrd ⊢ U ∈ NrmCVec ∧ W ∈ NrmCVec ∧ T : X ⟶ Y → 0 ≤ N ⁡ T