This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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

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 2 3 4 5 6 7 nmoub3i ⊢ ( ( 𝑇 : 𝑋 ⟶ 𝑌 ∧ 𝐴 ∈ ℝ ∧ ∀ 𝑥 ∈ 𝑋 ( 𝑀 ‘ ( 𝑇 ‘ 𝑥 ) ) ≤ ( 𝐴 · ( 𝐿 ‘ 𝑥 ) ) ) → ( 𝑁 ‘ 𝑇 ) ≤ ( abs ‘ 𝐴 ) )
9 8 3adant2r ⊢ ( ( 𝑇 : 𝑋 ⟶ 𝑌 ∧ ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ∀ 𝑥 ∈ 𝑋 ( 𝑀 ‘ ( 𝑇 ‘ 𝑥 ) ) ≤ ( 𝐴 · ( 𝐿 ‘ 𝑥 ) ) ) → ( 𝑁 ‘ 𝑇 ) ≤ ( abs ‘ 𝐴 ) )
10 absid ⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → ( abs ‘ 𝐴 ) = 𝐴 )
11 10 3ad2ant2 ⊢ ( ( 𝑇 : 𝑋 ⟶ 𝑌 ∧ ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ∀ 𝑥 ∈ 𝑋 ( 𝑀 ‘ ( 𝑇 ‘ 𝑥 ) ) ≤ ( 𝐴 · ( 𝐿 ‘ 𝑥 ) ) ) → ( abs ‘ 𝐴 ) = 𝐴 )
12 9 11 breqtrd ⊢ ( ( 𝑇 : 𝑋 ⟶ 𝑌 ∧ ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ∀ 𝑥 ∈ 𝑋 ( 𝑀 ‘ ( 𝑇 ‘ 𝑥 ) ) ≤ ( 𝐴 · ( 𝐿 ‘ 𝑥 ) ) ) → ( 𝑁 ‘ 𝑇 ) ≤ 𝐴 )