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ℎ ‘ ( 𝑇 ‘ 𝑥 ) ) ≤ 𝐴 ) ) )