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

Metamath Proof Explorer

Theorem nmoubi

Description: An upper bound for an operator norm. (Contributed by NM, 11-Dec-2007) (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 nmoubi ( ( 𝑇 : 𝑋 ⟶ 𝑌 ∧ 𝐴 ∈ ℝ* ) → ( ( 𝑁 ‘ 𝑇 ) ≤ 𝐴 ↔ ∀ 𝑥 ∈ 𝑋 ( ( 𝐿 ‘ 𝑥 ) ≤ 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 1 2 3 4 5 nmooval ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 : 𝑋 ⟶ 𝑌 ) → ( 𝑁 ‘ 𝑇 ) = sup ( { 𝑦 ∣ ∃ 𝑥 ∈ 𝑋 ( ( 𝐿 ‘ 𝑥 ) ≤ 1 ∧ 𝑦 = ( 𝑀 ‘ ( 𝑇 ‘ 𝑥 ) ) ) } , ℝ* , < ) )
9 6 7 8 mp3an12 ⊢ ( 𝑇 : 𝑋 ⟶ 𝑌 → ( 𝑁 ‘ 𝑇 ) = sup ( { 𝑦 ∣ ∃ 𝑥 ∈ 𝑋 ( ( 𝐿 ‘ 𝑥 ) ≤ 1 ∧ 𝑦 = ( 𝑀 ‘ ( 𝑇 ‘ 𝑥 ) ) ) } , ℝ* , < ) )
10 9 breq1d ⊢ ( 𝑇 : 𝑋 ⟶ 𝑌 → ( ( 𝑁 ‘ 𝑇 ) ≤ 𝐴 ↔ sup ( { 𝑦 ∣ ∃ 𝑥 ∈ 𝑋 ( ( 𝐿 ‘ 𝑥 ) ≤ 1 ∧ 𝑦 = ( 𝑀 ‘ ( 𝑇 ‘ 𝑥 ) ) ) } , ℝ* , < ) ≤ 𝐴 ) )
11 10 adantr ⊢ ( ( 𝑇 : 𝑋 ⟶ 𝑌 ∧ 𝐴 ∈ ℝ* ) → ( ( 𝑁 ‘ 𝑇 ) ≤ 𝐴 ↔ sup ( { 𝑦 ∣ ∃ 𝑥 ∈ 𝑋 ( ( 𝐿 ‘ 𝑥 ) ≤ 1 ∧ 𝑦 = ( 𝑀 ‘ ( 𝑇 ‘ 𝑥 ) ) ) } , ℝ* , < ) ≤ 𝐴 ) )
12 2 4 nmosetre ⊢ ( ( 𝑊 ∈ NrmCVec ∧ 𝑇 : 𝑋 ⟶ 𝑌 ) → { 𝑦 ∣ ∃ 𝑥 ∈ 𝑋 ( ( 𝐿 ‘ 𝑥 ) ≤ 1 ∧ 𝑦 = ( 𝑀 ‘ ( 𝑇 ‘ 𝑥 ) ) ) } ⊆ ℝ )
13 7 12 mpan ⊢ ( 𝑇 : 𝑋 ⟶ 𝑌 → { 𝑦 ∣ ∃ 𝑥 ∈ 𝑋 ( ( 𝐿 ‘ 𝑥 ) ≤ 1 ∧ 𝑦 = ( 𝑀 ‘ ( 𝑇 ‘ 𝑥 ) ) ) } ⊆ ℝ )
14 ressxr ⊢ ℝ ⊆ ℝ*
15 13 14 sstrdi ⊢ ( 𝑇 : 𝑋 ⟶ 𝑌 → { 𝑦 ∣ ∃ 𝑥 ∈ 𝑋 ( ( 𝐿 ‘ 𝑥 ) ≤ 1 ∧ 𝑦 = ( 𝑀 ‘ ( 𝑇 ‘ 𝑥 ) ) ) } ⊆ ℝ* )
16 supxrleub ⊢ ( ( { 𝑦 ∣ ∃ 𝑥 ∈ 𝑋 ( ( 𝐿 ‘ 𝑥 ) ≤ 1 ∧ 𝑦 = ( 𝑀 ‘ ( 𝑇 ‘ 𝑥 ) ) ) } ⊆ ℝ* ∧ 𝐴 ∈ ℝ* ) → ( sup ( { 𝑦 ∣ ∃ 𝑥 ∈ 𝑋 ( ( 𝐿 ‘ 𝑥 ) ≤ 1 ∧ 𝑦 = ( 𝑀 ‘ ( 𝑇 ‘ 𝑥 ) ) ) } , ℝ* , < ) ≤ 𝐴 ↔ ∀ 𝑧 ∈ { 𝑦 ∣ ∃ 𝑥 ∈ 𝑋 ( ( 𝐿 ‘ 𝑥 ) ≤ 1 ∧ 𝑦 = ( 𝑀 ‘ ( 𝑇 ‘ 𝑥 ) ) ) } 𝑧 ≤ 𝐴 ) )
17 15 16 sylan ⊢ ( ( 𝑇 : 𝑋 ⟶ 𝑌 ∧ 𝐴 ∈ ℝ* ) → ( sup ( { 𝑦 ∣ ∃ 𝑥 ∈ 𝑋 ( ( 𝐿 ‘ 𝑥 ) ≤ 1 ∧ 𝑦 = ( 𝑀 ‘ ( 𝑇 ‘ 𝑥 ) ) ) } , ℝ* , < ) ≤ 𝐴 ↔ ∀ 𝑧 ∈ { 𝑦 ∣ ∃ 𝑥 ∈ 𝑋 ( ( 𝐿 ‘ 𝑥 ) ≤ 1 ∧ 𝑦 = ( 𝑀 ‘ ( 𝑇 ‘ 𝑥 ) ) ) } 𝑧 ≤ 𝐴 ) )
18 11 17 bitrd ⊢ ( ( 𝑇 : 𝑋 ⟶ 𝑌 ∧ 𝐴 ∈ ℝ* ) → ( ( 𝑁 ‘ 𝑇 ) ≤ 𝐴 ↔ ∀ 𝑧 ∈ { 𝑦 ∣ ∃ 𝑥 ∈ 𝑋 ( ( 𝐿 ‘ 𝑥 ) ≤ 1 ∧ 𝑦 = ( 𝑀 ‘ ( 𝑇 ‘ 𝑥 ) ) ) } 𝑧 ≤ 𝐴 ) )
19 eqeq1 ⊢ ( 𝑦 = 𝑧 → ( 𝑦 = ( 𝑀 ‘ ( 𝑇 ‘ 𝑥 ) ) ↔ 𝑧 = ( 𝑀 ‘ ( 𝑇 ‘ 𝑥 ) ) ) )
20 19 anbi2d ⊢ ( 𝑦 = 𝑧 → ( ( ( 𝐿 ‘ 𝑥 ) ≤ 1 ∧ 𝑦 = ( 𝑀 ‘ ( 𝑇 ‘ 𝑥 ) ) ) ↔ ( ( 𝐿 ‘ 𝑥 ) ≤ 1 ∧ 𝑧 = ( 𝑀 ‘ ( 𝑇 ‘ 𝑥 ) ) ) ) )
21 20 rexbidv ⊢ ( 𝑦 = 𝑧 → ( ∃ 𝑥 ∈ 𝑋 ( ( 𝐿 ‘ 𝑥 ) ≤ 1 ∧ 𝑦 = ( 𝑀 ‘ ( 𝑇 ‘ 𝑥 ) ) ) ↔ ∃ 𝑥 ∈ 𝑋 ( ( 𝐿 ‘ 𝑥 ) ≤ 1 ∧ 𝑧 = ( 𝑀 ‘ ( 𝑇 ‘ 𝑥 ) ) ) ) )
22 21 ralab ⊢ ( ∀ 𝑧 ∈ { 𝑦 ∣ ∃ 𝑥 ∈ 𝑋 ( ( 𝐿 ‘ 𝑥 ) ≤ 1 ∧ 𝑦 = ( 𝑀 ‘ ( 𝑇 ‘ 𝑥 ) ) ) } 𝑧 ≤ 𝐴 ↔ ∀ 𝑧 ( ∃ 𝑥 ∈ 𝑋 ( ( 𝐿 ‘ 𝑥 ) ≤ 1 ∧ 𝑧 = ( 𝑀 ‘ ( 𝑇 ‘ 𝑥 ) ) ) → 𝑧 ≤ 𝐴 ) )
23 ralcom4 ⊢ ( ∀ 𝑥 ∈ 𝑋 ∀ 𝑧 ( ( ( 𝐿 ‘ 𝑥 ) ≤ 1 ∧ 𝑧 = ( 𝑀 ‘ ( 𝑇 ‘ 𝑥 ) ) ) → 𝑧 ≤ 𝐴 ) ↔ ∀ 𝑧 ∀ 𝑥 ∈ 𝑋 ( ( ( 𝐿 ‘ 𝑥 ) ≤ 1 ∧ 𝑧 = ( 𝑀 ‘ ( 𝑇 ‘ 𝑥 ) ) ) → 𝑧 ≤ 𝐴 ) )
24 ancomst ⊢ ( ( ( ( 𝐿 ‘ 𝑥 ) ≤ 1 ∧ 𝑧 = ( 𝑀 ‘ ( 𝑇 ‘ 𝑥 ) ) ) → 𝑧 ≤ 𝐴 ) ↔ ( ( 𝑧 = ( 𝑀 ‘ ( 𝑇 ‘ 𝑥 ) ) ∧ ( 𝐿 ‘ 𝑥 ) ≤ 1 ) → 𝑧 ≤ 𝐴 ) )
25 impexp ⊢ ( ( ( 𝑧 = ( 𝑀 ‘ ( 𝑇 ‘ 𝑥 ) ) ∧ ( 𝐿 ‘ 𝑥 ) ≤ 1 ) → 𝑧 ≤ 𝐴 ) ↔ ( 𝑧 = ( 𝑀 ‘ ( 𝑇 ‘ 𝑥 ) ) → ( ( 𝐿 ‘ 𝑥 ) ≤ 1 → 𝑧 ≤ 𝐴 ) ) )
26 24 25 bitri ⊢ ( ( ( ( 𝐿 ‘ 𝑥 ) ≤ 1 ∧ 𝑧 = ( 𝑀 ‘ ( 𝑇 ‘ 𝑥 ) ) ) → 𝑧 ≤ 𝐴 ) ↔ ( 𝑧 = ( 𝑀 ‘ ( 𝑇 ‘ 𝑥 ) ) → ( ( 𝐿 ‘ 𝑥 ) ≤ 1 → 𝑧 ≤ 𝐴 ) ) )
27 26 albii ⊢ ( ∀ 𝑧 ( ( ( 𝐿 ‘ 𝑥 ) ≤ 1 ∧ 𝑧 = ( 𝑀 ‘ ( 𝑇 ‘ 𝑥 ) ) ) → 𝑧 ≤ 𝐴 ) ↔ ∀ 𝑧 ( 𝑧 = ( 𝑀 ‘ ( 𝑇 ‘ 𝑥 ) ) → ( ( 𝐿 ‘ 𝑥 ) ≤ 1 → 𝑧 ≤ 𝐴 ) ) )
28 fvex ⊢ ( 𝑀 ‘ ( 𝑇 ‘ 𝑥 ) ) ∈ V
29 breq1 ⊢ ( 𝑧 = ( 𝑀 ‘ ( 𝑇 ‘ 𝑥 ) ) → ( 𝑧 ≤ 𝐴 ↔ ( 𝑀 ‘ ( 𝑇 ‘ 𝑥 ) ) ≤ 𝐴 ) )
30 29 imbi2d ⊢ ( 𝑧 = ( 𝑀 ‘ ( 𝑇 ‘ 𝑥 ) ) → ( ( ( 𝐿 ‘ 𝑥 ) ≤ 1 → 𝑧 ≤ 𝐴 ) ↔ ( ( 𝐿 ‘ 𝑥 ) ≤ 1 → ( 𝑀 ‘ ( 𝑇 ‘ 𝑥 ) ) ≤ 𝐴 ) ) )
31 28 30 ceqsalv ⊢ ( ∀ 𝑧 ( 𝑧 = ( 𝑀 ‘ ( 𝑇 ‘ 𝑥 ) ) → ( ( 𝐿 ‘ 𝑥 ) ≤ 1 → 𝑧 ≤ 𝐴 ) ) ↔ ( ( 𝐿 ‘ 𝑥 ) ≤ 1 → ( 𝑀 ‘ ( 𝑇 ‘ 𝑥 ) ) ≤ 𝐴 ) )
32 27 31 bitri ⊢ ( ∀ 𝑧 ( ( ( 𝐿 ‘ 𝑥 ) ≤ 1 ∧ 𝑧 = ( 𝑀 ‘ ( 𝑇 ‘ 𝑥 ) ) ) → 𝑧 ≤ 𝐴 ) ↔ ( ( 𝐿 ‘ 𝑥 ) ≤ 1 → ( 𝑀 ‘ ( 𝑇 ‘ 𝑥 ) ) ≤ 𝐴 ) )
33 32 ralbii ⊢ ( ∀ 𝑥 ∈ 𝑋 ∀ 𝑧 ( ( ( 𝐿 ‘ 𝑥 ) ≤ 1 ∧ 𝑧 = ( 𝑀 ‘ ( 𝑇 ‘ 𝑥 ) ) ) → 𝑧 ≤ 𝐴 ) ↔ ∀ 𝑥 ∈ 𝑋 ( ( 𝐿 ‘ 𝑥 ) ≤ 1 → ( 𝑀 ‘ ( 𝑇 ‘ 𝑥 ) ) ≤ 𝐴 ) )
34 r19.23v ⊢ ( ∀ 𝑥 ∈ 𝑋 ( ( ( 𝐿 ‘ 𝑥 ) ≤ 1 ∧ 𝑧 = ( 𝑀 ‘ ( 𝑇 ‘ 𝑥 ) ) ) → 𝑧 ≤ 𝐴 ) ↔ ( ∃ 𝑥 ∈ 𝑋 ( ( 𝐿 ‘ 𝑥 ) ≤ 1 ∧ 𝑧 = ( 𝑀 ‘ ( 𝑇 ‘ 𝑥 ) ) ) → 𝑧 ≤ 𝐴 ) )
35 34 albii ⊢ ( ∀ 𝑧 ∀ 𝑥 ∈ 𝑋 ( ( ( 𝐿 ‘ 𝑥 ) ≤ 1 ∧ 𝑧 = ( 𝑀 ‘ ( 𝑇 ‘ 𝑥 ) ) ) → 𝑧 ≤ 𝐴 ) ↔ ∀ 𝑧 ( ∃ 𝑥 ∈ 𝑋 ( ( 𝐿 ‘ 𝑥 ) ≤ 1 ∧ 𝑧 = ( 𝑀 ‘ ( 𝑇 ‘ 𝑥 ) ) ) → 𝑧 ≤ 𝐴 ) )
36 23 33 35 3bitr3i ⊢ ( ∀ 𝑥 ∈ 𝑋 ( ( 𝐿 ‘ 𝑥 ) ≤ 1 → ( 𝑀 ‘ ( 𝑇 ‘ 𝑥 ) ) ≤ 𝐴 ) ↔ ∀ 𝑧 ( ∃ 𝑥 ∈ 𝑋 ( ( 𝐿 ‘ 𝑥 ) ≤ 1 ∧ 𝑧 = ( 𝑀 ‘ ( 𝑇 ‘ 𝑥 ) ) ) → 𝑧 ≤ 𝐴 ) )
37 22 36 bitr4i ⊢ ( ∀ 𝑧 ∈ { 𝑦 ∣ ∃ 𝑥 ∈ 𝑋 ( ( 𝐿 ‘ 𝑥 ) ≤ 1 ∧ 𝑦 = ( 𝑀 ‘ ( 𝑇 ‘ 𝑥 ) ) ) } 𝑧 ≤ 𝐴 ↔ ∀ 𝑥 ∈ 𝑋 ( ( 𝐿 ‘ 𝑥 ) ≤ 1 → ( 𝑀 ‘ ( 𝑇 ‘ 𝑥 ) ) ≤ 𝐴 ) )
38 18 37 bitrdi ⊢ ( ( 𝑇 : 𝑋 ⟶ 𝑌 ∧ 𝐴 ∈ ℝ* ) → ( ( 𝑁 ‘ 𝑇 ) ≤ 𝐴 ↔ ∀ 𝑥 ∈ 𝑋 ( ( 𝐿 ‘ 𝑥 ) ≤ 1 → ( 𝑀 ‘ ( 𝑇 ‘ 𝑥 ) ) ≤ 𝐴 ) ) )