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

Metamath Proof Explorer

Theorem isblo3i

Description: The predicate "is a bounded linear operator." Definition 2.7-1 of Kreyszig p. 91. (Contributed by NM, 11-Dec-2007) (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 isblo3i ( 𝑇 ∈ 𝐵 ↔ ( 𝑇 ∈ 𝐿 ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝑋 ( 𝑁 ‘ ( 𝑇 ‘ 𝑦 ) ) ≤ ( 𝑥 · ( 𝑀 ‘ 𝑦 ) ) ) )

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 4 5 bloln ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ 𝐵 ) → 𝑇 ∈ 𝐿 )
9 6 7 8 mp3an12 ⊢ ( 𝑇 ∈ 𝐵 → 𝑇 ∈ 𝐿 )
10 eqid ⊢ ( BaseSet ‘ 𝑊 ) = ( BaseSet ‘ 𝑊 )
11 eqid ⊢ ( 𝑈 normOpOLD 𝑊 ) = ( 𝑈 normOpOLD 𝑊 )
12 1 10 11 5 nmblore ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ 𝐵 ) → ( ( 𝑈 normOpOLD 𝑊 ) ‘ 𝑇 ) ∈ ℝ )
13 6 7 12 mp3an12 ⊢ ( 𝑇 ∈ 𝐵 → ( ( 𝑈 normOpOLD 𝑊 ) ‘ 𝑇 ) ∈ ℝ )
14 1 2 3 11 5 6 7 nmblolbi ⊢ ( ( 𝑇 ∈ 𝐵 ∧ 𝑦 ∈ 𝑋 ) → ( 𝑁 ‘ ( 𝑇 ‘ 𝑦 ) ) ≤ ( ( ( 𝑈 normOpOLD 𝑊 ) ‘ 𝑇 ) · ( 𝑀 ‘ 𝑦 ) ) )
15 14 ralrimiva ⊢ ( 𝑇 ∈ 𝐵 → ∀ 𝑦 ∈ 𝑋 ( 𝑁 ‘ ( 𝑇 ‘ 𝑦 ) ) ≤ ( ( ( 𝑈 normOpOLD 𝑊 ) ‘ 𝑇 ) · ( 𝑀 ‘ 𝑦 ) ) )
16 oveq1 ⊢ ( 𝑥 = ( ( 𝑈 normOpOLD 𝑊 ) ‘ 𝑇 ) → ( 𝑥 · ( 𝑀 ‘ 𝑦 ) ) = ( ( ( 𝑈 normOpOLD 𝑊 ) ‘ 𝑇 ) · ( 𝑀 ‘ 𝑦 ) ) )
17 16 breq2d ⊢ ( 𝑥 = ( ( 𝑈 normOpOLD 𝑊 ) ‘ 𝑇 ) → ( ( 𝑁 ‘ ( 𝑇 ‘ 𝑦 ) ) ≤ ( 𝑥 · ( 𝑀 ‘ 𝑦 ) ) ↔ ( 𝑁 ‘ ( 𝑇 ‘ 𝑦 ) ) ≤ ( ( ( 𝑈 normOpOLD 𝑊 ) ‘ 𝑇 ) · ( 𝑀 ‘ 𝑦 ) ) ) )
18 17 ralbidv ⊢ ( 𝑥 = ( ( 𝑈 normOpOLD 𝑊 ) ‘ 𝑇 ) → ( ∀ 𝑦 ∈ 𝑋 ( 𝑁 ‘ ( 𝑇 ‘ 𝑦 ) ) ≤ ( 𝑥 · ( 𝑀 ‘ 𝑦 ) ) ↔ ∀ 𝑦 ∈ 𝑋 ( 𝑁 ‘ ( 𝑇 ‘ 𝑦 ) ) ≤ ( ( ( 𝑈 normOpOLD 𝑊 ) ‘ 𝑇 ) · ( 𝑀 ‘ 𝑦 ) ) ) )
19 18 rspcev ⊢ ( ( ( ( 𝑈 normOpOLD 𝑊 ) ‘ 𝑇 ) ∈ ℝ ∧ ∀ 𝑦 ∈ 𝑋 ( 𝑁 ‘ ( 𝑇 ‘ 𝑦 ) ) ≤ ( ( ( 𝑈 normOpOLD 𝑊 ) ‘ 𝑇 ) · ( 𝑀 ‘ 𝑦 ) ) ) → ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝑋 ( 𝑁 ‘ ( 𝑇 ‘ 𝑦 ) ) ≤ ( 𝑥 · ( 𝑀 ‘ 𝑦 ) ) )
20 13 15 19 syl2anc ⊢ ( 𝑇 ∈ 𝐵 → ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝑋 ( 𝑁 ‘ ( 𝑇 ‘ 𝑦 ) ) ≤ ( 𝑥 · ( 𝑀 ‘ 𝑦 ) ) )
21 9 20 jca ⊢ ( 𝑇 ∈ 𝐵 → ( 𝑇 ∈ 𝐿 ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝑋 ( 𝑁 ‘ ( 𝑇 ‘ 𝑦 ) ) ≤ ( 𝑥 · ( 𝑀 ‘ 𝑦 ) ) ) )
22 simp1 ⊢ ( ( 𝑇 ∈ 𝐿 ∧ 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ 𝑋 ( 𝑁 ‘ ( 𝑇 ‘ 𝑦 ) ) ≤ ( 𝑥 · ( 𝑀 ‘ 𝑦 ) ) ) → 𝑇 ∈ 𝐿 )
23 1 10 4 lnof ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ 𝐿 ) → 𝑇 : 𝑋 ⟶ ( BaseSet ‘ 𝑊 ) )
24 6 7 23 mp3an12 ⊢ ( 𝑇 ∈ 𝐿 → 𝑇 : 𝑋 ⟶ ( BaseSet ‘ 𝑊 ) )
25 1 10 11 nmoxr ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 : 𝑋 ⟶ ( BaseSet ‘ 𝑊 ) ) → ( ( 𝑈 normOpOLD 𝑊 ) ‘ 𝑇 ) ∈ ℝ* )
26 6 7 25 mp3an12 ⊢ ( 𝑇 : 𝑋 ⟶ ( BaseSet ‘ 𝑊 ) → ( ( 𝑈 normOpOLD 𝑊 ) ‘ 𝑇 ) ∈ ℝ* )
27 26 3ad2ant1 ⊢ ( ( 𝑇 : 𝑋 ⟶ ( BaseSet ‘ 𝑊 ) ∧ 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ 𝑋 ( 𝑁 ‘ ( 𝑇 ‘ 𝑦 ) ) ≤ ( 𝑥 · ( 𝑀 ‘ 𝑦 ) ) ) → ( ( 𝑈 normOpOLD 𝑊 ) ‘ 𝑇 ) ∈ ℝ* )
28 recn ⊢ ( 𝑥 ∈ ℝ → 𝑥 ∈ ℂ )
29 28 abscld ⊢ ( 𝑥 ∈ ℝ → ( abs ‘ 𝑥 ) ∈ ℝ )
30 29 rexrd ⊢ ( 𝑥 ∈ ℝ → ( abs ‘ 𝑥 ) ∈ ℝ* )
31 30 3ad2ant2 ⊢ ( ( 𝑇 : 𝑋 ⟶ ( BaseSet ‘ 𝑊 ) ∧ 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ 𝑋 ( 𝑁 ‘ ( 𝑇 ‘ 𝑦 ) ) ≤ ( 𝑥 · ( 𝑀 ‘ 𝑦 ) ) ) → ( abs ‘ 𝑥 ) ∈ ℝ* )
32 pnfxr ⊢ +∞ ∈ ℝ*
33 32 a1i ⊢ ( ( 𝑇 : 𝑋 ⟶ ( BaseSet ‘ 𝑊 ) ∧ 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ 𝑋 ( 𝑁 ‘ ( 𝑇 ‘ 𝑦 ) ) ≤ ( 𝑥 · ( 𝑀 ‘ 𝑦 ) ) ) → +∞ ∈ ℝ* )
34 1 10 2 3 11 6 7 nmoub3i ⊢ ( ( 𝑇 : 𝑋 ⟶ ( BaseSet ‘ 𝑊 ) ∧ 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ 𝑋 ( 𝑁 ‘ ( 𝑇 ‘ 𝑦 ) ) ≤ ( 𝑥 · ( 𝑀 ‘ 𝑦 ) ) ) → ( ( 𝑈 normOpOLD 𝑊 ) ‘ 𝑇 ) ≤ ( abs ‘ 𝑥 ) )
35 ltpnf ⊢ ( ( abs ‘ 𝑥 ) ∈ ℝ → ( abs ‘ 𝑥 ) < +∞ )
36 29 35 syl ⊢ ( 𝑥 ∈ ℝ → ( abs ‘ 𝑥 ) < +∞ )
37 36 3ad2ant2 ⊢ ( ( 𝑇 : 𝑋 ⟶ ( BaseSet ‘ 𝑊 ) ∧ 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ 𝑋 ( 𝑁 ‘ ( 𝑇 ‘ 𝑦 ) ) ≤ ( 𝑥 · ( 𝑀 ‘ 𝑦 ) ) ) → ( abs ‘ 𝑥 ) < +∞ )
38 27 31 33 34 37 xrlelttrd ⊢ ( ( 𝑇 : 𝑋 ⟶ ( BaseSet ‘ 𝑊 ) ∧ 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ 𝑋 ( 𝑁 ‘ ( 𝑇 ‘ 𝑦 ) ) ≤ ( 𝑥 · ( 𝑀 ‘ 𝑦 ) ) ) → ( ( 𝑈 normOpOLD 𝑊 ) ‘ 𝑇 ) < +∞ )
39 24 38 syl3an1 ⊢ ( ( 𝑇 ∈ 𝐿 ∧ 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ 𝑋 ( 𝑁 ‘ ( 𝑇 ‘ 𝑦 ) ) ≤ ( 𝑥 · ( 𝑀 ‘ 𝑦 ) ) ) → ( ( 𝑈 normOpOLD 𝑊 ) ‘ 𝑇 ) < +∞ )
40 11 4 5 isblo ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ) → ( 𝑇 ∈ 𝐵 ↔ ( 𝑇 ∈ 𝐿 ∧ ( ( 𝑈 normOpOLD 𝑊 ) ‘ 𝑇 ) < +∞ ) ) )
41 6 7 40 mp2an ⊢ ( 𝑇 ∈ 𝐵 ↔ ( 𝑇 ∈ 𝐿 ∧ ( ( 𝑈 normOpOLD 𝑊 ) ‘ 𝑇 ) < +∞ ) )
42 22 39 41 sylanbrc ⊢ ( ( 𝑇 ∈ 𝐿 ∧ 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ 𝑋 ( 𝑁 ‘ ( 𝑇 ‘ 𝑦 ) ) ≤ ( 𝑥 · ( 𝑀 ‘ 𝑦 ) ) ) → 𝑇 ∈ 𝐵 )
43 42 rexlimdv3a ⊢ ( 𝑇 ∈ 𝐿 → ( ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝑋 ( 𝑁 ‘ ( 𝑇 ‘ 𝑦 ) ) ≤ ( 𝑥 · ( 𝑀 ‘ 𝑦 ) ) → 𝑇 ∈ 𝐵 ) )
44 43 imp ⊢ ( ( 𝑇 ∈ 𝐿 ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝑋 ( 𝑁 ‘ ( 𝑇 ‘ 𝑦 ) ) ≤ ( 𝑥 · ( 𝑀 ‘ 𝑦 ) ) ) → 𝑇 ∈ 𝐵 )
45 21 44 impbii ⊢ ( 𝑇 ∈ 𝐵 ↔ ( 𝑇 ∈ 𝐿 ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝑋 ( 𝑁 ‘ ( 𝑇 ‘ 𝑦 ) ) ≤ ( 𝑥 · ( 𝑀 ‘ 𝑦 ) ) ) )