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

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 ⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
nmoubi.y ⊢ 𝑌 = ( BaseSet ‘ 𝑊 )
nmoubi.l ⊢ 𝐿 = ( normCV ‘ 𝑈 )
nmoubi.m ⊢ 𝑀 = ( normCV ‘ 𝑊 )
nmoubi.3 ⊢ 𝑁 = ( 𝑈 normOpOLD 𝑊 )
nmoubi.u ⊢ 𝑈 ∈ NrmCVec
nmoubi.w ⊢ 𝑊 ∈ NrmCVec
Assertion nmobndi ( 𝑇 : 𝑋 ⟶ 𝑌 → ( ( 𝑁 ‘ 𝑇 ) ∈ ℝ ↔ ∃ 𝑟 ∈ ℝ ∀ 𝑦 ∈ 𝑋 ( ( 𝐿 ‘ 𝑦 ) ≤ 1 → ( 𝑀 ‘ ( 𝑇 ‘ 𝑦 ) ) ≤ 𝑟 ) ) )

Proof

Step Hyp Ref Expression
1 nmoubi.1 ⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
2 nmoubi.y ⊢ 𝑌 = ( BaseSet ‘ 𝑊 )
3 nmoubi.l ⊢ 𝐿 = ( normCV ‘ 𝑈 )
4 nmoubi.m ⊢ 𝑀 = ( normCV ‘ 𝑊 )
5 nmoubi.3 ⊢ 𝑁 = ( 𝑈 normOpOLD 𝑊 )
6 nmoubi.u ⊢ 𝑈 ∈ NrmCVec
7 nmoubi.w ⊢ 𝑊 ∈ NrmCVec
8 leid ⊢ ( ( 𝑁 ‘ 𝑇 ) ∈ ℝ → ( 𝑁 ‘ 𝑇 ) ≤ ( 𝑁 ‘ 𝑇 ) )
9 breq2 ⊢ ( 𝑟 = ( 𝑁 ‘ 𝑇 ) → ( ( 𝑁 ‘ 𝑇 ) ≤ 𝑟 ↔ ( 𝑁 ‘ 𝑇 ) ≤ ( 𝑁 ‘ 𝑇 ) ) )
10 9 rspcev ⊢ ( ( ( 𝑁 ‘ 𝑇 ) ∈ ℝ ∧ ( 𝑁 ‘ 𝑇 ) ≤ ( 𝑁 ‘ 𝑇 ) ) → ∃ 𝑟 ∈ ℝ ( 𝑁 ‘ 𝑇 ) ≤ 𝑟 )
11 8 10 mpdan ⊢ ( ( 𝑁 ‘ 𝑇 ) ∈ ℝ → ∃ 𝑟 ∈ ℝ ( 𝑁 ‘ 𝑇 ) ≤ 𝑟 )
12 1 2 5 nmoxr ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 : 𝑋 ⟶ 𝑌 ) → ( 𝑁 ‘ 𝑇 ) ∈ ℝ* )
13 6 7 12 mp3an12 ⊢ ( 𝑇 : 𝑋 ⟶ 𝑌 → ( 𝑁 ‘ 𝑇 ) ∈ ℝ* )
14 13 adantr ⊢ ( ( 𝑇 : 𝑋 ⟶ 𝑌 ∧ ( 𝑟 ∈ ℝ ∧ ( 𝑁 ‘ 𝑇 ) ≤ 𝑟 ) ) → ( 𝑁 ‘ 𝑇 ) ∈ ℝ* )
15 simprl ⊢ ( ( 𝑇 : 𝑋 ⟶ 𝑌 ∧ ( 𝑟 ∈ ℝ ∧ ( 𝑁 ‘ 𝑇 ) ≤ 𝑟 ) ) → 𝑟 ∈ ℝ )
16 1 2 5 nmogtmnf ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 : 𝑋 ⟶ 𝑌 ) → -∞ < ( 𝑁 ‘ 𝑇 ) )
17 6 7 16 mp3an12 ⊢ ( 𝑇 : 𝑋 ⟶ 𝑌 → -∞ < ( 𝑁 ‘ 𝑇 ) )
18 17 adantr ⊢ ( ( 𝑇 : 𝑋 ⟶ 𝑌 ∧ ( 𝑟 ∈ ℝ ∧ ( 𝑁 ‘ 𝑇 ) ≤ 𝑟 ) ) → -∞ < ( 𝑁 ‘ 𝑇 ) )
19 simprr ⊢ ( ( 𝑇 : 𝑋 ⟶ 𝑌 ∧ ( 𝑟 ∈ ℝ ∧ ( 𝑁 ‘ 𝑇 ) ≤ 𝑟 ) ) → ( 𝑁 ‘ 𝑇 ) ≤ 𝑟 )
20 xrre ⊢ ( ( ( ( 𝑁 ‘ 𝑇 ) ∈ ℝ* ∧ 𝑟 ∈ ℝ ) ∧ ( -∞ < ( 𝑁 ‘ 𝑇 ) ∧ ( 𝑁 ‘ 𝑇 ) ≤ 𝑟 ) ) → ( 𝑁 ‘ 𝑇 ) ∈ ℝ )
21 14 15 18 19 20 syl22anc ⊢ ( ( 𝑇 : 𝑋 ⟶ 𝑌 ∧ ( 𝑟 ∈ ℝ ∧ ( 𝑁 ‘ 𝑇 ) ≤ 𝑟 ) ) → ( 𝑁 ‘ 𝑇 ) ∈ ℝ )
22 21 rexlimdvaa ⊢ ( 𝑇 : 𝑋 ⟶ 𝑌 → ( ∃ 𝑟 ∈ ℝ ( 𝑁 ‘ 𝑇 ) ≤ 𝑟 → ( 𝑁 ‘ 𝑇 ) ∈ ℝ ) )
23 11 22 impbid2 ⊢ ( 𝑇 : 𝑋 ⟶ 𝑌 → ( ( 𝑁 ‘ 𝑇 ) ∈ ℝ ↔ ∃ 𝑟 ∈ ℝ ( 𝑁 ‘ 𝑇 ) ≤ 𝑟 ) )
24 rexr ⊢ ( 𝑟 ∈ ℝ → 𝑟 ∈ ℝ* )
25 1 2 3 4 5 6 7 nmoubi ⊢ ( ( 𝑇 : 𝑋 ⟶ 𝑌 ∧ 𝑟 ∈ ℝ* ) → ( ( 𝑁 ‘ 𝑇 ) ≤ 𝑟 ↔ ∀ 𝑦 ∈ 𝑋 ( ( 𝐿 ‘ 𝑦 ) ≤ 1 → ( 𝑀 ‘ ( 𝑇 ‘ 𝑦 ) ) ≤ 𝑟 ) ) )
26 24 25 sylan2 ⊢ ( ( 𝑇 : 𝑋 ⟶ 𝑌 ∧ 𝑟 ∈ ℝ ) → ( ( 𝑁 ‘ 𝑇 ) ≤ 𝑟 ↔ ∀ 𝑦 ∈ 𝑋 ( ( 𝐿 ‘ 𝑦 ) ≤ 1 → ( 𝑀 ‘ ( 𝑇 ‘ 𝑦 ) ) ≤ 𝑟 ) ) )
27 26 rexbidva ⊢ ( 𝑇 : 𝑋 ⟶ 𝑌 → ( ∃ 𝑟 ∈ ℝ ( 𝑁 ‘ 𝑇 ) ≤ 𝑟 ↔ ∃ 𝑟 ∈ ℝ ∀ 𝑦 ∈ 𝑋 ( ( 𝐿 ‘ 𝑦 ) ≤ 1 → ( 𝑀 ‘ ( 𝑇 ‘ 𝑦 ) ) ≤ 𝑟 ) ) )
28 23 27 bitrd ⊢ ( 𝑇 : 𝑋 ⟶ 𝑌 → ( ( 𝑁 ‘ 𝑇 ) ∈ ℝ ↔ ∃ 𝑟 ∈ ℝ ∀ 𝑦 ∈ 𝑋 ( ( 𝐿 ‘ 𝑦 ) ≤ 1 → ( 𝑀 ‘ ( 𝑇 ‘ 𝑦 ) ) ≤ 𝑟 ) ) )