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=normCV⁡U
isblo3i.n ⊢N=normCV⁡W
isblo3i.4 ⊢L=ULnOpW
isblo3i.5 ⊢B=UBLnOpW
isblo3i.u ⊢U∈NrmCVec
isblo3i.w ⊢W∈NrmCVec
Assertion isblo3i ⊢T∈B↔T∈L∧∃x∈ℝ∀y∈XN⁡T⁡y≤x⁢M⁡y

Proof

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