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 ⊢ X = BaseSet ⁡ U
isblo3i.m ⊢ M = norm CV ⁡ U
isblo3i.n ⊢ N = norm CV ⁡ W
isblo3i.4 ⊢ L = U LnOp W
isblo3i.5 ⊢ B = U BLnOp W
isblo3i.u ⊢ U ∈ NrmCVec
isblo3i.w ⊢ W ∈ NrmCVec
Assertion isblo3i ⊢ T ∈ B ↔ T ∈ L ∧ ∃ x ∈ ℝ ∀ y ∈ X N ⁡ T ⁡ y ≤ x ⁢ M ⁡ y

Proof

Step Hyp Ref Expression
1 isblo3i.1 ⊢ X = BaseSet ⁡ U
2 isblo3i.m ⊢ M = norm CV ⁡ U
3 isblo3i.n ⊢ N = norm CV ⁡ W
4 isblo3i.4 ⊢ L = U LnOp W
5 isblo3i.5 ⊢ B = U BLnOp W
6 isblo3i.u ⊢ U ∈ NrmCVec
7 isblo3i.w ⊢ W ∈ NrmCVec
8 4 5 bloln ⊢ U ∈ NrmCVec ∧ W ∈ NrmCVec ∧ T ∈ B → T ∈ L
9 6 7 8 mp3an12 ⊢ T ∈ B → T ∈ L
10 eqid ⊢ BaseSet ⁡ W = BaseSet ⁡ W
11 eqid ⊢ U normOp OLD W = U normOp OLD W
12 1 10 11 5 nmblore ⊢ U ∈ NrmCVec ∧ W ∈ NrmCVec ∧ T ∈ B → U normOp OLD W ⁡ T ∈ ℝ
13 6 7 12 mp3an12 ⊢ T ∈ B → U normOp OLD W ⁡ T ∈ ℝ
14 1 2 3 11 5 6 7 nmblolbi ⊢ T ∈ B ∧ y ∈ X → N ⁡ T ⁡ y ≤ U normOp OLD W ⁡ T ⁢ M ⁡ y
15 14 ralrimiva ⊢ T ∈ B → ∀ y ∈ X N ⁡ T ⁡ y ≤ U normOp OLD W ⁡ T ⁢ M ⁡ y
16 oveq1 ⊢ x = U normOp OLD W ⁡ T → x ⁢ M ⁡ y = U normOp OLD W ⁡ T ⁢ M ⁡ y
17 16 breq2d ⊢ x = U normOp OLD W ⁡ T → N ⁡ T ⁡ y ≤ x ⁢ M ⁡ y ↔ N ⁡ T ⁡ y ≤ U normOp OLD W ⁡ T ⁢ M ⁡ y
18 17 ralbidv ⊢ x = U normOp OLD W ⁡ T → ∀ y ∈ X N ⁡ T ⁡ y ≤ x ⁢ M ⁡ y ↔ ∀ y ∈ X N ⁡ T ⁡ y ≤ U normOp OLD W ⁡ T ⁢ M ⁡ y
19 18 rspcev ⊢ U normOp OLD W ⁡ T ∈ ℝ ∧ ∀ y ∈ X N ⁡ T ⁡ y ≤ U normOp OLD W ⁡ T ⁢ M ⁡ y → ∃ x ∈ ℝ ∀ y ∈ X N ⁡ T ⁡ y ≤ x ⁢ M ⁡ y
20 13 15 19 syl2anc ⊢ T ∈ B → ∃ x ∈ ℝ ∀ y ∈ X N ⁡ T ⁡ y ≤ x ⁢ M ⁡ y
21 9 20 jca ⊢ T ∈ B → T ∈ L ∧ ∃ x ∈ ℝ ∀ y ∈ X N ⁡ T ⁡ y ≤ x ⁢ M ⁡ y
22 simp1 ⊢ T ∈ L ∧ x ∈ ℝ ∧ ∀ y ∈ X N ⁡ T ⁡ y ≤ x ⁢ M ⁡ y → T ∈ L
23 1 10 4 lnof ⊢ U ∈ NrmCVec ∧ W ∈ NrmCVec ∧ T ∈ L → T : X ⟶ BaseSet ⁡ W
24 6 7 23 mp3an12 ⊢ T ∈ L → T : X ⟶ BaseSet ⁡ W
25 1 10 11 nmoxr ⊢ U ∈ NrmCVec ∧ W ∈ NrmCVec ∧ T : X ⟶ BaseSet ⁡ W → U normOp OLD W ⁡ T ∈ ℝ *
26 6 7 25 mp3an12 ⊢ T : X ⟶ BaseSet ⁡ W → U normOp OLD W ⁡ T ∈ ℝ *
27 26 3ad2ant1 ⊢ T : X ⟶ BaseSet ⁡ W ∧ x ∈ ℝ ∧ ∀ y ∈ X N ⁡ T ⁡ y ≤ x ⁢ M ⁡ y → U normOp OLD W ⁡ T ∈ ℝ *
28 recn ⊢ x ∈ ℝ → x ∈ ℂ
29 28 abscld ⊢ x ∈ ℝ → x ∈ ℝ
30 29 rexrd ⊢ x ∈ ℝ → x ∈ ℝ *
31 30 3ad2ant2 ⊢ T : X ⟶ BaseSet ⁡ W ∧ x ∈ ℝ ∧ ∀ y ∈ X N ⁡ T ⁡ y ≤ x ⁢ M ⁡ y → x ∈ ℝ *
32 pnfxr ⊢ +∞ ∈ ℝ *
33 32 a1i ⊢ T : X ⟶ BaseSet ⁡ W ∧ x ∈ ℝ ∧ ∀ y ∈ X N ⁡ T ⁡ y ≤ x ⁢ M ⁡ y → +∞ ∈ ℝ *
34 1 10 2 3 11 6 7 nmoub3i ⊢ T : X ⟶ BaseSet ⁡ W ∧ x ∈ ℝ ∧ ∀ y ∈ X N ⁡ T ⁡ y ≤ x ⁢ M ⁡ y → U normOp OLD W ⁡ T ≤ x
35 ltpnf ⊢ x ∈ ℝ → x < +∞
36 29 35 syl ⊢ x ∈ ℝ → x < +∞
37 36 3ad2ant2 ⊢ T : X ⟶ BaseSet ⁡ W ∧ x ∈ ℝ ∧ ∀ y ∈ X N ⁡ T ⁡ y ≤ x ⁢ M ⁡ y → x < +∞
38 27 31 33 34 37 xrlelttrd ⊢ T : X ⟶ BaseSet ⁡ W ∧ x ∈ ℝ ∧ ∀ y ∈ X N ⁡ T ⁡ y ≤ x ⁢ M ⁡ y → U normOp OLD W ⁡ T < +∞
39 24 38 syl3an1 ⊢ T ∈ L ∧ x ∈ ℝ ∧ ∀ y ∈ X N ⁡ T ⁡ y ≤ x ⁢ M ⁡ y → U normOp OLD W ⁡ T < +∞
40 11 4 5 isblo ⊢ U ∈ NrmCVec ∧ W ∈ NrmCVec → T ∈ B ↔ T ∈ L ∧ U normOp OLD W ⁡ T < +∞
41 6 7 40 mp2an ⊢ T ∈ B ↔ T ∈ L ∧ U normOp OLD W ⁡ T < +∞
42 22 39 41 sylanbrc ⊢ T ∈ L ∧ x ∈ ℝ ∧ ∀ y ∈ X N ⁡ T ⁡ y ≤ x ⁢ M ⁡ y → T ∈ B
43 42 rexlimdv3a ⊢ T ∈ L → ∃ x ∈ ℝ ∀ y ∈ X N ⁡ T ⁡ y ≤ x ⁢ M ⁡ y → T ∈ B
44 43 imp ⊢ T ∈ L ∧ ∃ x ∈ ℝ ∀ y ∈ X N ⁡ T ⁡ y ≤ x ⁢ M ⁡ y → T ∈ B
45 21 44 impbii ⊢ T ∈ B ↔ T ∈ L ∧ ∃ x ∈ ℝ ∀ y ∈ X N ⁡ T ⁡ y ≤ x ⁢ M ⁡ y