Metamath Proof Explorer

Theorem nmobndi

Description: Two ways to express that an operator is bounded. (Contributed by NM, 11-Jan-2008) (New usage is discouraged.)

Ref Expression
Hypotheses nmoubi.1 ⊢X=BaseSet⁡U
nmoubi.y ⊢Y=BaseSet⁡W
nmoubi.l ⊢L=normCV⁡U
nmoubi.m ⊢M=normCV⁡W
nmoubi.3 ⊢N=UnormOpOLDW
nmoubi.u ⊢U∈NrmCVec
nmoubi.w ⊢W∈NrmCVec
Assertion nmobndi ⊢T:X⟶Y→N⁡T∈ℝ↔∃r∈ℝ∀y∈XL⁡y≤1→M⁡T⁡y≤r

Proof

Step Hyp Ref Expression
1 nmoubi.1 ⊢X=BaseSet⁡U
2 nmoubi.y ⊢Y=BaseSet⁡W
3 nmoubi.l ⊢L=normCV⁡U
4 nmoubi.m ⊢M=normCV⁡W
5 nmoubi.3 ⊢N=UnormOpOLDW
6 nmoubi.u ⊢U∈NrmCVec
7 nmoubi.w ⊢W∈NrmCVec
8 leid ⊢N⁡T∈ℝ→N⁡T≤N⁡T
9 breq2 ⊢r=N⁡T→N⁡T≤r↔N⁡T≤N⁡T
10 9 rspcev ⊢N⁡T∈ℝ∧N⁡T≤N⁡T→∃r∈ℝN⁡T≤r
11 8 10 mpdan ⊢N⁡T∈ℝ→∃r∈ℝN⁡T≤r
12 1 2 5 nmoxr ⊢U∈NrmCVec∧W∈NrmCVec∧T:X⟶Y→N⁡T∈ℝ*
13 6 7 12 mp3an12 ⊢T:X⟶Y→N⁡T∈ℝ*
14 13 adantr ⊢T:X⟶Y∧r∈ℝ∧N⁡T≤r→N⁡T∈ℝ*
15 simprl ⊢T:X⟶Y∧r∈ℝ∧N⁡T≤r→r∈ℝ
16 1 2 5 nmogtmnf ⊢U∈NrmCVec∧W∈NrmCVec∧T:X⟶Y→−∞<N⁡T
17 6 7 16 mp3an12 ⊢T:X⟶Y→−∞<N⁡T
18 17 adantr ⊢T:X⟶Y∧r∈ℝ∧N⁡T≤r→−∞<N⁡T
19 simprr ⊢T:X⟶Y∧r∈ℝ∧N⁡T≤r→N⁡T≤r
20 xrre ⊢N⁡T∈ℝ*∧r∈ℝ∧−∞<N⁡T∧N⁡T≤r→N⁡T∈ℝ
21 14 15 18 19 20 syl22anc ⊢T:X⟶Y∧r∈ℝ∧N⁡T≤r→N⁡T∈ℝ
22 21 rexlimdvaa ⊢T:X⟶Y→∃r∈ℝN⁡T≤r→N⁡T∈ℝ
23 11 22 impbid2 ⊢T:X⟶Y→N⁡T∈ℝ↔∃r∈ℝN⁡T≤r
24 rexr ⊢r∈ℝ→r∈ℝ*
25 1 2 3 4 5 6 7 nmoubi ⊢T:X⟶Y∧r∈ℝ*→N⁡T≤r↔∀y∈XL⁡y≤1→M⁡T⁡y≤r
26 24 25 sylan2 ⊢T:X⟶Y∧r∈ℝ→N⁡T≤r↔∀y∈XL⁡y≤1→M⁡T⁡y≤r
27 26 rexbidva ⊢T:X⟶Y→∃r∈ℝN⁡T≤r↔∃r∈ℝ∀y∈XL⁡y≤1→M⁡T⁡y≤r
28 23 27 bitrd ⊢T:X⟶Y→N⁡T∈ℝ↔∃r∈ℝ∀y∈XL⁡y≤1→M⁡T⁡y≤r