Metamath Proof Explorer

Theorem nmopub

Description: An upper bound for an operator norm. (Contributed by NM, 7-Mar-2006) (New usage is discouraged.)

Ref Expression
Assertion nmopub ( ( 𝑇 : ℋ ⟶ ℋ ∧ 𝐴 ∈ ℝ* ) → ( ( normop𝑇 ) ≤ 𝐴 ↔ ∀ 𝑥 ∈ ℋ ( ( norm𝑥 ) ≤ 1 → ( norm ‘ ( 𝑇𝑥 ) ) ≤ 𝐴 ) ) )

Proof

Step Hyp Ref Expression
1 nmopval ( 𝑇 : ℋ ⟶ ℋ → ( normop𝑇 ) = sup ( { 𝑦 ∣ ∃ 𝑥 ∈ ℋ ( ( norm𝑥 ) ≤ 1 ∧ 𝑦 = ( norm ‘ ( 𝑇𝑥 ) ) ) } , ℝ* , < ) )
2 1 adantr ( ( 𝑇 : ℋ ⟶ ℋ ∧ 𝐴 ∈ ℝ* ) → ( normop𝑇 ) = sup ( { 𝑦 ∣ ∃ 𝑥 ∈ ℋ ( ( norm𝑥 ) ≤ 1 ∧ 𝑦 = ( norm ‘ ( 𝑇𝑥 ) ) ) } , ℝ* , < ) )
3 2 breq1d ( ( 𝑇 : ℋ ⟶ ℋ ∧ 𝐴 ∈ ℝ* ) → ( ( normop𝑇 ) ≤ 𝐴 ↔ sup ( { 𝑦 ∣ ∃ 𝑥 ∈ ℋ ( ( norm𝑥 ) ≤ 1 ∧ 𝑦 = ( norm ‘ ( 𝑇𝑥 ) ) ) } , ℝ* , < ) ≤ 𝐴 ) )
4 nmopsetretALT ( 𝑇 : ℋ ⟶ ℋ → { 𝑦 ∣ ∃ 𝑥 ∈ ℋ ( ( norm𝑥 ) ≤ 1 ∧ 𝑦 = ( norm ‘ ( 𝑇𝑥 ) ) ) } ⊆ ℝ )
5 ressxr ℝ ⊆ ℝ*
6 4 5 sstrdi ( 𝑇 : ℋ ⟶ ℋ → { 𝑦 ∣ ∃ 𝑥 ∈ ℋ ( ( norm𝑥 ) ≤ 1 ∧ 𝑦 = ( norm ‘ ( 𝑇𝑥 ) ) ) } ⊆ ℝ* )
7 supxrleub ( ( { 𝑦 ∣ ∃ 𝑥 ∈ ℋ ( ( norm𝑥 ) ≤ 1 ∧ 𝑦 = ( norm ‘ ( 𝑇𝑥 ) ) ) } ⊆ ℝ*𝐴 ∈ ℝ* ) → ( sup ( { 𝑦 ∣ ∃ 𝑥 ∈ ℋ ( ( norm𝑥 ) ≤ 1 ∧ 𝑦 = ( norm ‘ ( 𝑇𝑥 ) ) ) } , ℝ* , < ) ≤ 𝐴 ↔ ∀ 𝑧 ∈ { 𝑦 ∣ ∃ 𝑥 ∈ ℋ ( ( norm𝑥 ) ≤ 1 ∧ 𝑦 = ( norm ‘ ( 𝑇𝑥 ) ) ) } 𝑧𝐴 ) )
8 6 7 sylan ( ( 𝑇 : ℋ ⟶ ℋ ∧ 𝐴 ∈ ℝ* ) → ( sup ( { 𝑦 ∣ ∃ 𝑥 ∈ ℋ ( ( norm𝑥 ) ≤ 1 ∧ 𝑦 = ( norm ‘ ( 𝑇𝑥 ) ) ) } , ℝ* , < ) ≤ 𝐴 ↔ ∀ 𝑧 ∈ { 𝑦 ∣ ∃ 𝑥 ∈ ℋ ( ( norm𝑥 ) ≤ 1 ∧ 𝑦 = ( norm ‘ ( 𝑇𝑥 ) ) ) } 𝑧𝐴 ) )
9 ancom ( ( ( norm𝑥 ) ≤ 1 ∧ 𝑦 = ( norm ‘ ( 𝑇𝑥 ) ) ) ↔ ( 𝑦 = ( norm ‘ ( 𝑇𝑥 ) ) ∧ ( norm𝑥 ) ≤ 1 ) )
10 eqeq1 ( 𝑦 = 𝑧 → ( 𝑦 = ( norm ‘ ( 𝑇𝑥 ) ) ↔ 𝑧 = ( norm ‘ ( 𝑇𝑥 ) ) ) )
11 10 anbi1d ( 𝑦 = 𝑧 → ( ( 𝑦 = ( norm ‘ ( 𝑇𝑥 ) ) ∧ ( norm𝑥 ) ≤ 1 ) ↔ ( 𝑧 = ( norm ‘ ( 𝑇𝑥 ) ) ∧ ( norm𝑥 ) ≤ 1 ) ) )
12 9 11 syl5bb ( 𝑦 = 𝑧 → ( ( ( norm𝑥 ) ≤ 1 ∧ 𝑦 = ( norm ‘ ( 𝑇𝑥 ) ) ) ↔ ( 𝑧 = ( norm ‘ ( 𝑇𝑥 ) ) ∧ ( norm𝑥 ) ≤ 1 ) ) )
13 12 rexbidv ( 𝑦 = 𝑧 → ( ∃ 𝑥 ∈ ℋ ( ( norm𝑥 ) ≤ 1 ∧ 𝑦 = ( norm ‘ ( 𝑇𝑥 ) ) ) ↔ ∃ 𝑥 ∈ ℋ ( 𝑧 = ( norm ‘ ( 𝑇𝑥 ) ) ∧ ( norm𝑥 ) ≤ 1 ) ) )
14 13 ralab ( ∀ 𝑧 ∈ { 𝑦 ∣ ∃ 𝑥 ∈ ℋ ( ( norm𝑥 ) ≤ 1 ∧ 𝑦 = ( norm ‘ ( 𝑇𝑥 ) ) ) } 𝑧𝐴 ↔ ∀ 𝑧 ( ∃ 𝑥 ∈ ℋ ( 𝑧 = ( norm ‘ ( 𝑇𝑥 ) ) ∧ ( norm𝑥 ) ≤ 1 ) → 𝑧𝐴 ) )
15 ralcom4 ( ∀ 𝑥 ∈ ℋ ∀ 𝑧 ( ( 𝑧 = ( norm ‘ ( 𝑇𝑥 ) ) ∧ ( norm𝑥 ) ≤ 1 ) → 𝑧𝐴 ) ↔ ∀ 𝑧𝑥 ∈ ℋ ( ( 𝑧 = ( norm ‘ ( 𝑇𝑥 ) ) ∧ ( norm𝑥 ) ≤ 1 ) → 𝑧𝐴 ) )
16 impexp ( ( ( 𝑧 = ( norm ‘ ( 𝑇𝑥 ) ) ∧ ( norm𝑥 ) ≤ 1 ) → 𝑧𝐴 ) ↔ ( 𝑧 = ( norm ‘ ( 𝑇𝑥 ) ) → ( ( norm𝑥 ) ≤ 1 → 𝑧𝐴 ) ) )
17 16 albii ( ∀ 𝑧 ( ( 𝑧 = ( norm ‘ ( 𝑇𝑥 ) ) ∧ ( norm𝑥 ) ≤ 1 ) → 𝑧𝐴 ) ↔ ∀ 𝑧 ( 𝑧 = ( norm ‘ ( 𝑇𝑥 ) ) → ( ( norm𝑥 ) ≤ 1 → 𝑧𝐴 ) ) )
18 fvex ( norm ‘ ( 𝑇𝑥 ) ) ∈ V
19 breq1 ( 𝑧 = ( norm ‘ ( 𝑇𝑥 ) ) → ( 𝑧𝐴 ↔ ( norm ‘ ( 𝑇𝑥 ) ) ≤ 𝐴 ) )
20 19 imbi2d ( 𝑧 = ( norm ‘ ( 𝑇𝑥 ) ) → ( ( ( norm𝑥 ) ≤ 1 → 𝑧𝐴 ) ↔ ( ( norm𝑥 ) ≤ 1 → ( norm ‘ ( 𝑇𝑥 ) ) ≤ 𝐴 ) ) )
21 18 20 ceqsalv ( ∀ 𝑧 ( 𝑧 = ( norm ‘ ( 𝑇𝑥 ) ) → ( ( norm𝑥 ) ≤ 1 → 𝑧𝐴 ) ) ↔ ( ( norm𝑥 ) ≤ 1 → ( norm ‘ ( 𝑇𝑥 ) ) ≤ 𝐴 ) )
22 17 21 bitri ( ∀ 𝑧 ( ( 𝑧 = ( norm ‘ ( 𝑇𝑥 ) ) ∧ ( norm𝑥 ) ≤ 1 ) → 𝑧𝐴 ) ↔ ( ( norm𝑥 ) ≤ 1 → ( norm ‘ ( 𝑇𝑥 ) ) ≤ 𝐴 ) )
23 22 ralbii ( ∀ 𝑥 ∈ ℋ ∀ 𝑧 ( ( 𝑧 = ( norm ‘ ( 𝑇𝑥 ) ) ∧ ( norm𝑥 ) ≤ 1 ) → 𝑧𝐴 ) ↔ ∀ 𝑥 ∈ ℋ ( ( norm𝑥 ) ≤ 1 → ( norm ‘ ( 𝑇𝑥 ) ) ≤ 𝐴 ) )
24 r19.23v ( ∀ 𝑥 ∈ ℋ ( ( 𝑧 = ( norm ‘ ( 𝑇𝑥 ) ) ∧ ( norm𝑥 ) ≤ 1 ) → 𝑧𝐴 ) ↔ ( ∃ 𝑥 ∈ ℋ ( 𝑧 = ( norm ‘ ( 𝑇𝑥 ) ) ∧ ( norm𝑥 ) ≤ 1 ) → 𝑧𝐴 ) )
25 24 albii ( ∀ 𝑧𝑥 ∈ ℋ ( ( 𝑧 = ( norm ‘ ( 𝑇𝑥 ) ) ∧ ( norm𝑥 ) ≤ 1 ) → 𝑧𝐴 ) ↔ ∀ 𝑧 ( ∃ 𝑥 ∈ ℋ ( 𝑧 = ( norm ‘ ( 𝑇𝑥 ) ) ∧ ( norm𝑥 ) ≤ 1 ) → 𝑧𝐴 ) )
26 15 23 25 3bitr3i ( ∀ 𝑥 ∈ ℋ ( ( norm𝑥 ) ≤ 1 → ( norm ‘ ( 𝑇𝑥 ) ) ≤ 𝐴 ) ↔ ∀ 𝑧 ( ∃ 𝑥 ∈ ℋ ( 𝑧 = ( norm ‘ ( 𝑇𝑥 ) ) ∧ ( norm𝑥 ) ≤ 1 ) → 𝑧𝐴 ) )
27 14 26 bitr4i ( ∀ 𝑧 ∈ { 𝑦 ∣ ∃ 𝑥 ∈ ℋ ( ( norm𝑥 ) ≤ 1 ∧ 𝑦 = ( norm ‘ ( 𝑇𝑥 ) ) ) } 𝑧𝐴 ↔ ∀ 𝑥 ∈ ℋ ( ( norm𝑥 ) ≤ 1 → ( norm ‘ ( 𝑇𝑥 ) ) ≤ 𝐴 ) )
28 8 27 syl6bb ( ( 𝑇 : ℋ ⟶ ℋ ∧ 𝐴 ∈ ℝ* ) → ( sup ( { 𝑦 ∣ ∃ 𝑥 ∈ ℋ ( ( norm𝑥 ) ≤ 1 ∧ 𝑦 = ( norm ‘ ( 𝑇𝑥 ) ) ) } , ℝ* , < ) ≤ 𝐴 ↔ ∀ 𝑥 ∈ ℋ ( ( norm𝑥 ) ≤ 1 → ( norm ‘ ( 𝑇𝑥 ) ) ≤ 𝐴 ) ) )
29 3 28 bitrd ( ( 𝑇 : ℋ ⟶ ℋ ∧ 𝐴 ∈ ℝ* ) → ( ( normop𝑇 ) ≤ 𝐴 ↔ ∀ 𝑥 ∈ ℋ ( ( norm𝑥 ) ≤ 1 → ( norm ‘ ( 𝑇𝑥 ) ) ≤ 𝐴 ) ) )