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

Metamath Proof Explorer

Theorem blo3i

Description: Properties that determine a bounded linear operator. (Contributed by NM, 13-Jan-2008) (New usage is discouraged.)

Ref Expression
Hypotheses isblo3i.1 ⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
isblo3i.m ⊢ 𝑀 = ( normCV ‘ 𝑈 )
isblo3i.n ⊢ 𝑁 = ( normCV ‘ 𝑊 )
isblo3i.4 ⊢ 𝐿 = ( 𝑈 LnOp 𝑊 )
isblo3i.5 ⊢ 𝐵 = ( 𝑈 BLnOp 𝑊 )
isblo3i.u ⊢ 𝑈 ∈ NrmCVec
isblo3i.w ⊢ 𝑊 ∈ NrmCVec
Assertion blo3i ( ( 𝑇 ∈ 𝐿 ∧ 𝐴 ∈ ℝ ∧ ∀ 𝑦 ∈ 𝑋 ( 𝑁 ‘ ( 𝑇 ‘ 𝑦 ) ) ≤ ( 𝐴 · ( 𝑀 ‘ 𝑦 ) ) ) → 𝑇 ∈ 𝐵 )

Proof

Step Hyp Ref Expression
1 isblo3i.1 ⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
2 isblo3i.m ⊢ 𝑀 = ( normCV ‘ 𝑈 )
3 isblo3i.n ⊢ 𝑁 = ( normCV ‘ 𝑊 )
4 isblo3i.4 ⊢ 𝐿 = ( 𝑈 LnOp 𝑊 )
5 isblo3i.5 ⊢ 𝐵 = ( 𝑈 BLnOp 𝑊 )
6 isblo3i.u ⊢ 𝑈 ∈ NrmCVec
7 isblo3i.w ⊢ 𝑊 ∈ NrmCVec
8 oveq1 ⊢ ( 𝑥 = 𝐴 → ( 𝑥 · ( 𝑀 ‘ 𝑦 ) ) = ( 𝐴 · ( 𝑀 ‘ 𝑦 ) ) )
9 8 breq2d ⊢ ( 𝑥 = 𝐴 → ( ( 𝑁 ‘ ( 𝑇 ‘ 𝑦 ) ) ≤ ( 𝑥 · ( 𝑀 ‘ 𝑦 ) ) ↔ ( 𝑁 ‘ ( 𝑇 ‘ 𝑦 ) ) ≤ ( 𝐴 · ( 𝑀 ‘ 𝑦 ) ) ) )
10 9 ralbidv ⊢ ( 𝑥 = 𝐴 → ( ∀ 𝑦 ∈ 𝑋 ( 𝑁 ‘ ( 𝑇 ‘ 𝑦 ) ) ≤ ( 𝑥 · ( 𝑀 ‘ 𝑦 ) ) ↔ ∀ 𝑦 ∈ 𝑋 ( 𝑁 ‘ ( 𝑇 ‘ 𝑦 ) ) ≤ ( 𝐴 · ( 𝑀 ‘ 𝑦 ) ) ) )
11 10 rspcev ⊢ ( ( 𝐴 ∈ ℝ ∧ ∀ 𝑦 ∈ 𝑋 ( 𝑁 ‘ ( 𝑇 ‘ 𝑦 ) ) ≤ ( 𝐴 · ( 𝑀 ‘ 𝑦 ) ) ) → ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝑋 ( 𝑁 ‘ ( 𝑇 ‘ 𝑦 ) ) ≤ ( 𝑥 · ( 𝑀 ‘ 𝑦 ) ) )
12 1 2 3 4 5 6 7 isblo3i ⊢ ( 𝑇 ∈ 𝐵 ↔ ( 𝑇 ∈ 𝐿 ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝑋 ( 𝑁 ‘ ( 𝑇 ‘ 𝑦 ) ) ≤ ( 𝑥 · ( 𝑀 ‘ 𝑦 ) ) ) )
13 12 biimpri ⊢ ( ( 𝑇 ∈ 𝐿 ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝑋 ( 𝑁 ‘ ( 𝑇 ‘ 𝑦 ) ) ≤ ( 𝑥 · ( 𝑀 ‘ 𝑦 ) ) ) → 𝑇 ∈ 𝐵 )
14 11 13 sylan2 ⊢ ( ( 𝑇 ∈ 𝐿 ∧ ( 𝐴 ∈ ℝ ∧ ∀ 𝑦 ∈ 𝑋 ( 𝑁 ‘ ( 𝑇 ‘ 𝑦 ) ) ≤ ( 𝐴 · ( 𝑀 ‘ 𝑦 ) ) ) ) → 𝑇 ∈ 𝐵 )
15 14 3impb ⊢ ( ( 𝑇 ∈ 𝐿 ∧ 𝐴 ∈ ℝ ∧ ∀ 𝑦 ∈ 𝑋 ( 𝑁 ‘ ( 𝑇 ‘ 𝑦 ) ) ≤ ( 𝐴 · ( 𝑀 ‘ 𝑦 ) ) ) → 𝑇 ∈ 𝐵 )