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 ≤ 𝐴 ) ∧ ∀ 𝑥 ∈ 𝑋 ( 𝑀 ‘ ( 𝑇 ‘ 𝑥 ) ) ≤ ( 𝐴 · ( 𝐿 ‘ 𝑥 ) ) ) → ( 𝑁 ‘ 𝑇 ) ≤ 𝐴 )