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 = norm CV ⁡ U
nmoubi.m ⊢ M = norm CV ⁡ W
nmoubi.3 ⊢ N = U normOp OLD W
nmoubi.u ⊢ U ∈ NrmCVec
nmoubi.w ⊢ W ∈ NrmCVec
Assertion nmobndi ⊢ T : X ⟶ Y → N ⁡ T ∈ ℝ ↔ ∃ r ∈ ℝ ∀ y ∈ X L ⁡ 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 = norm CV ⁡ U
4 nmoubi.m ⊢ M = norm CV ⁡ W
5 nmoubi.3 ⊢ N = U normOp OLD W
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 ∈ X L ⁡ y ≤ 1 → M ⁡ T ⁡ y ≤ r
26 24 25 sylan2 ⊢ T : X ⟶ Y ∧ r ∈ ℝ → N ⁡ T ≤ r ↔ ∀ y ∈ X L ⁡ y ≤ 1 → M ⁡ T ⁡ y ≤ r
27 26 rexbidva ⊢ T : X ⟶ Y → ∃ r ∈ ℝ N ⁡ T ≤ r ↔ ∃ r ∈ ℝ ∀ y ∈ X L ⁡ y ≤ 1 → M ⁡ T ⁡ y ≤ r
28 23 27 bitrd ⊢ T : X ⟶ Y → N ⁡ T ∈ ℝ ↔ ∃ r ∈ ℝ ∀ y ∈ X L ⁡ y ≤ 1 → M ⁡ T ⁡ y ≤ r