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 ⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
nmoxr.2 ⊢ 𝑌 = ( BaseSet ‘ 𝑊 )
nmoxr.3 ⊢ 𝑁 = ( 𝑈 normOpOLD 𝑊 )
Assertion nmooge0 ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 : 𝑋 ⟶ 𝑌 ) → 0 ≤ ( 𝑁 ‘ 𝑇 ) )

Proof

Step Hyp Ref Expression
1 nmoxr.1 ⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
2 nmoxr.2 ⊢ 𝑌 = ( BaseSet ‘ 𝑊 )
3 nmoxr.3 ⊢ 𝑁 = ( 𝑈 normOpOLD 𝑊 )
4 0xr ⊢ 0 ∈ ℝ*
5 4 a1i ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 : 𝑋 ⟶ 𝑌 ) → 0 ∈ ℝ* )
6 simp2 ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 : 𝑋 ⟶ 𝑌 ) → 𝑊 ∈ NrmCVec )
7 eqid ⊢ ( 0vec ‘ 𝑈 ) = ( 0vec ‘ 𝑈 )
8 1 7 nvzcl ⊢ ( 𝑈 ∈ NrmCVec → ( 0vec ‘ 𝑈 ) ∈ 𝑋 )
9 ffvelrn ⊢ ( ( 𝑇 : 𝑋 ⟶ 𝑌 ∧ ( 0vec ‘ 𝑈 ) ∈ 𝑋 ) → ( 𝑇 ‘ ( 0vec ‘ 𝑈 ) ) ∈ 𝑌 )
10 8 9 sylan2 ⊢ ( ( 𝑇 : 𝑋 ⟶ 𝑌 ∧ 𝑈 ∈ NrmCVec ) → ( 𝑇 ‘ ( 0vec ‘ 𝑈 ) ) ∈ 𝑌 )
11 10 ancoms ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑇 : 𝑋 ⟶ 𝑌 ) → ( 𝑇 ‘ ( 0vec ‘ 𝑈 ) ) ∈ 𝑌 )
12 11 3adant2 ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 : 𝑋 ⟶ 𝑌 ) → ( 𝑇 ‘ ( 0vec ‘ 𝑈 ) ) ∈ 𝑌 )
13 eqid ⊢ ( normCV ‘ 𝑊 ) = ( normCV ‘ 𝑊 )
14 2 13 nvcl ⊢ ( ( 𝑊 ∈ NrmCVec ∧ ( 𝑇 ‘ ( 0vec ‘ 𝑈 ) ) ∈ 𝑌 ) → ( ( normCV ‘ 𝑊 ) ‘ ( 𝑇 ‘ ( 0vec ‘ 𝑈 ) ) ) ∈ ℝ )
15 6 12 14 syl2anc ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 : 𝑋 ⟶ 𝑌 ) → ( ( normCV ‘ 𝑊 ) ‘ ( 𝑇 ‘ ( 0vec ‘ 𝑈 ) ) ) ∈ ℝ )
16 15 rexrd ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 : 𝑋 ⟶ 𝑌 ) → ( ( normCV ‘ 𝑊 ) ‘ ( 𝑇 ‘ ( 0vec ‘ 𝑈 ) ) ) ∈ ℝ* )
17 1 2 3 nmoxr ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 : 𝑋 ⟶ 𝑌 ) → ( 𝑁 ‘ 𝑇 ) ∈ ℝ* )
18 2 13 nvge0 ⊢ ( ( 𝑊 ∈ NrmCVec ∧ ( 𝑇 ‘ ( 0vec ‘ 𝑈 ) ) ∈ 𝑌 ) → 0 ≤ ( ( normCV ‘ 𝑊 ) ‘ ( 𝑇 ‘ ( 0vec ‘ 𝑈 ) ) ) )
19 6 12 18 syl2anc ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 : 𝑋 ⟶ 𝑌 ) → 0 ≤ ( ( normCV ‘ 𝑊 ) ‘ ( 𝑇 ‘ ( 0vec ‘ 𝑈 ) ) ) )
20 2 13 nmosetre ⊢ ( ( 𝑊 ∈ NrmCVec ∧ 𝑇 : 𝑋 ⟶ 𝑌 ) → { 𝑥 ∣ ∃ 𝑧 ∈ 𝑋 ( ( ( normCV ‘ 𝑈 ) ‘ 𝑧 ) ≤ 1 ∧ 𝑥 = ( ( normCV ‘ 𝑊 ) ‘ ( 𝑇 ‘ 𝑧 ) ) ) } ⊆ ℝ )
21 ressxr ⊢ ℝ ⊆ ℝ*
22 20 21 sstrdi ⊢ ( ( 𝑊 ∈ NrmCVec ∧ 𝑇 : 𝑋 ⟶ 𝑌 ) → { 𝑥 ∣ ∃ 𝑧 ∈ 𝑋 ( ( ( normCV ‘ 𝑈 ) ‘ 𝑧 ) ≤ 1 ∧ 𝑥 = ( ( normCV ‘ 𝑊 ) ‘ ( 𝑇 ‘ 𝑧 ) ) ) } ⊆ ℝ* )
23 eqid ⊢ ( normCV ‘ 𝑈 ) = ( normCV ‘ 𝑈 )
24 1 7 23 nmosetn0 ⊢ ( 𝑈 ∈ NrmCVec → ( ( normCV ‘ 𝑊 ) ‘ ( 𝑇 ‘ ( 0vec ‘ 𝑈 ) ) ) ∈ { 𝑥 ∣ ∃ 𝑧 ∈ 𝑋 ( ( ( normCV ‘ 𝑈 ) ‘ 𝑧 ) ≤ 1 ∧ 𝑥 = ( ( normCV ‘ 𝑊 ) ‘ ( 𝑇 ‘ 𝑧 ) ) ) } )
25 supxrub ⊢ ( ( { 𝑥 ∣ ∃ 𝑧 ∈ 𝑋 ( ( ( normCV ‘ 𝑈 ) ‘ 𝑧 ) ≤ 1 ∧ 𝑥 = ( ( normCV ‘ 𝑊 ) ‘ ( 𝑇 ‘ 𝑧 ) ) ) } ⊆ ℝ* ∧ ( ( normCV ‘ 𝑊 ) ‘ ( 𝑇 ‘ ( 0vec ‘ 𝑈 ) ) ) ∈ { 𝑥 ∣ ∃ 𝑧 ∈ 𝑋 ( ( ( normCV ‘ 𝑈 ) ‘ 𝑧 ) ≤ 1 ∧ 𝑥 = ( ( normCV ‘ 𝑊 ) ‘ ( 𝑇 ‘ 𝑧 ) ) ) } ) → ( ( normCV ‘ 𝑊 ) ‘ ( 𝑇 ‘ ( 0vec ‘ 𝑈 ) ) ) ≤ sup ( { 𝑥 ∣ ∃ 𝑧 ∈ 𝑋 ( ( ( normCV ‘ 𝑈 ) ‘ 𝑧 ) ≤ 1 ∧ 𝑥 = ( ( normCV ‘ 𝑊 ) ‘ ( 𝑇 ‘ 𝑧 ) ) ) } , ℝ* , < ) )
26 22 24 25 syl2an ⊢ ( ( ( 𝑊 ∈ NrmCVec ∧ 𝑇 : 𝑋 ⟶ 𝑌 ) ∧ 𝑈 ∈ NrmCVec ) → ( ( normCV ‘ 𝑊 ) ‘ ( 𝑇 ‘ ( 0vec ‘ 𝑈 ) ) ) ≤ sup ( { 𝑥 ∣ ∃ 𝑧 ∈ 𝑋 ( ( ( normCV ‘ 𝑈 ) ‘ 𝑧 ) ≤ 1 ∧ 𝑥 = ( ( normCV ‘ 𝑊 ) ‘ ( 𝑇 ‘ 𝑧 ) ) ) } , ℝ* , < ) )
27 26 3impa ⊢ ( ( 𝑊 ∈ NrmCVec ∧ 𝑇 : 𝑋 ⟶ 𝑌 ∧ 𝑈 ∈ NrmCVec ) → ( ( normCV ‘ 𝑊 ) ‘ ( 𝑇 ‘ ( 0vec ‘ 𝑈 ) ) ) ≤ sup ( { 𝑥 ∣ ∃ 𝑧 ∈ 𝑋 ( ( ( normCV ‘ 𝑈 ) ‘ 𝑧 ) ≤ 1 ∧ 𝑥 = ( ( normCV ‘ 𝑊 ) ‘ ( 𝑇 ‘ 𝑧 ) ) ) } , ℝ* , < ) )
28 27 3comr ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 : 𝑋 ⟶ 𝑌 ) → ( ( normCV ‘ 𝑊 ) ‘ ( 𝑇 ‘ ( 0vec ‘ 𝑈 ) ) ) ≤ sup ( { 𝑥 ∣ ∃ 𝑧 ∈ 𝑋 ( ( ( normCV ‘ 𝑈 ) ‘ 𝑧 ) ≤ 1 ∧ 𝑥 = ( ( normCV ‘ 𝑊 ) ‘ ( 𝑇 ‘ 𝑧 ) ) ) } , ℝ* , < ) )
29 1 2 23 13 3 nmooval ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 : 𝑋 ⟶ 𝑌 ) → ( 𝑁 ‘ 𝑇 ) = sup ( { 𝑥 ∣ ∃ 𝑧 ∈ 𝑋 ( ( ( normCV ‘ 𝑈 ) ‘ 𝑧 ) ≤ 1 ∧ 𝑥 = ( ( normCV ‘ 𝑊 ) ‘ ( 𝑇 ‘ 𝑧 ) ) ) } , ℝ* , < ) )
30 28 29 breqtrrd ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 : 𝑋 ⟶ 𝑌 ) → ( ( normCV ‘ 𝑊 ) ‘ ( 𝑇 ‘ ( 0vec ‘ 𝑈 ) ) ) ≤ ( 𝑁 ‘ 𝑇 ) )
31 5 16 17 19 30 xrletrd ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 : 𝑋 ⟶ 𝑌 ) → 0 ≤ ( 𝑁 ‘ 𝑇 ) )