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 ⊢ T : ℋ ⟶ ℋ ∧ A ∈ ℝ * → norm op ⁡ T ≤ A ↔ ∀ x ∈ ℋ norm ℎ ⁡ x ≤ 1 → norm ℎ ⁡ T ⁡ x ≤ A

Proof

Step Hyp Ref Expression
1 nmopval ⊢ T : ℋ ⟶ ℋ → norm op ⁡ T = sup y | ∃ x ∈ ℋ norm ℎ ⁡ x ≤ 1 ∧ y = norm ℎ ⁡ T ⁡ x ℝ * <
2 1 adantr ⊢ T : ℋ ⟶ ℋ ∧ A ∈ ℝ * → norm op ⁡ T = sup y | ∃ x ∈ ℋ norm ℎ ⁡ x ≤ 1 ∧ y = norm ℎ ⁡ T ⁡ x ℝ * <
3 2 breq1d ⊢ T : ℋ ⟶ ℋ ∧ A ∈ ℝ * → norm op ⁡ T ≤ A ↔ sup y | ∃ x ∈ ℋ norm ℎ ⁡ x ≤ 1 ∧ y = norm ℎ ⁡ T ⁡ x ℝ * < ≤ A
4 nmopsetretALT ⊢ T : ℋ ⟶ ℋ → y | ∃ x ∈ ℋ norm ℎ ⁡ x ≤ 1 ∧ y = norm ℎ ⁡ T ⁡ x ⊆ ℝ
5 ressxr ⊢ ℝ ⊆ ℝ *
6 4 5 sstrdi ⊢ T : ℋ ⟶ ℋ → y | ∃ x ∈ ℋ norm ℎ ⁡ x ≤ 1 ∧ y = norm ℎ ⁡ T ⁡ x ⊆ ℝ *
7 supxrleub ⊢ y | ∃ x ∈ ℋ norm ℎ ⁡ x ≤ 1 ∧ y = norm ℎ ⁡ T ⁡ x ⊆ ℝ * ∧ A ∈ ℝ * → sup y | ∃ x ∈ ℋ norm ℎ ⁡ x ≤ 1 ∧ y = norm ℎ ⁡ T ⁡ x ℝ * < ≤ A ↔ ∀ z ∈ y | ∃ x ∈ ℋ norm ℎ ⁡ x ≤ 1 ∧ y = norm ℎ ⁡ T ⁡ x z ≤ A
8 6 7 sylan ⊢ T : ℋ ⟶ ℋ ∧ A ∈ ℝ * → sup y | ∃ x ∈ ℋ norm ℎ ⁡ x ≤ 1 ∧ y = norm ℎ ⁡ T ⁡ x ℝ * < ≤ A ↔ ∀ z ∈ y | ∃ x ∈ ℋ norm ℎ ⁡ x ≤ 1 ∧ y = norm ℎ ⁡ T ⁡ x z ≤ A
9 ancom ⊢ norm ℎ ⁡ x ≤ 1 ∧ y = norm ℎ ⁡ T ⁡ x ↔ y = norm ℎ ⁡ T ⁡ x ∧ norm ℎ ⁡ x ≤ 1
10 eqeq1 ⊢ y = z → y = norm ℎ ⁡ T ⁡ x ↔ z = norm ℎ ⁡ T ⁡ x
11 10 anbi1d ⊢ y = z → y = norm ℎ ⁡ T ⁡ x ∧ norm ℎ ⁡ x ≤ 1 ↔ z = norm ℎ ⁡ T ⁡ x ∧ norm ℎ ⁡ x ≤ 1
12 9 11 bitrid ⊢ y = z → norm ℎ ⁡ x ≤ 1 ∧ y = norm ℎ ⁡ T ⁡ x ↔ z = norm ℎ ⁡ T ⁡ x ∧ norm ℎ ⁡ x ≤ 1
13 12 rexbidv ⊢ y = z → ∃ x ∈ ℋ norm ℎ ⁡ x ≤ 1 ∧ y = norm ℎ ⁡ T ⁡ x ↔ ∃ x ∈ ℋ z = norm ℎ ⁡ T ⁡ x ∧ norm ℎ ⁡ x ≤ 1
14 13 ralab ⊢ ∀ z ∈ y | ∃ x ∈ ℋ norm ℎ ⁡ x ≤ 1 ∧ y = norm ℎ ⁡ T ⁡ x z ≤ A ↔ ∀ z ∃ x ∈ ℋ z = norm ℎ ⁡ T ⁡ x ∧ norm ℎ ⁡ x ≤ 1 → z ≤ A
15 ralcom4 ⊢ ∀ x ∈ ℋ ∀ z z = norm ℎ ⁡ T ⁡ x ∧ norm ℎ ⁡ x ≤ 1 → z ≤ A ↔ ∀ z ∀ x ∈ ℋ z = norm ℎ ⁡ T ⁡ x ∧ norm ℎ ⁡ x ≤ 1 → z ≤ A
16 impexp ⊢ z = norm ℎ ⁡ T ⁡ x ∧ norm ℎ ⁡ x ≤ 1 → z ≤ A ↔ z = norm ℎ ⁡ T ⁡ x → norm ℎ ⁡ x ≤ 1 → z ≤ A
17 16 albii ⊢ ∀ z z = norm ℎ ⁡ T ⁡ x ∧ norm ℎ ⁡ x ≤ 1 → z ≤ A ↔ ∀ z z = norm ℎ ⁡ T ⁡ x → norm ℎ ⁡ x ≤ 1 → z ≤ A
18 fvex ⊢ norm ℎ ⁡ T ⁡ x ∈ V
19 breq1 ⊢ z = norm ℎ ⁡ T ⁡ x → z ≤ A ↔ norm ℎ ⁡ T ⁡ x ≤ A
20 19 imbi2d ⊢ z = norm ℎ ⁡ T ⁡ x → norm ℎ ⁡ x ≤ 1 → z ≤ A ↔ norm ℎ ⁡ x ≤ 1 → norm ℎ ⁡ T ⁡ x ≤ A
21 18 20 ceqsalv ⊢ ∀ z z = norm ℎ ⁡ T ⁡ x → norm ℎ ⁡ x ≤ 1 → z ≤ A ↔ norm ℎ ⁡ x ≤ 1 → norm ℎ ⁡ T ⁡ x ≤ A
22 17 21 bitri ⊢ ∀ z z = norm ℎ ⁡ T ⁡ x ∧ norm ℎ ⁡ x ≤ 1 → z ≤ A ↔ norm ℎ ⁡ x ≤ 1 → norm ℎ ⁡ T ⁡ x ≤ A
23 22 ralbii ⊢ ∀ x ∈ ℋ ∀ z z = norm ℎ ⁡ T ⁡ x ∧ norm ℎ ⁡ x ≤ 1 → z ≤ A ↔ ∀ x ∈ ℋ norm ℎ ⁡ x ≤ 1 → norm ℎ ⁡ T ⁡ x ≤ A
24 r19.23v ⊢ ∀ x ∈ ℋ z = norm ℎ ⁡ T ⁡ x ∧ norm ℎ ⁡ x ≤ 1 → z ≤ A ↔ ∃ x ∈ ℋ z = norm ℎ ⁡ T ⁡ x ∧ norm ℎ ⁡ x ≤ 1 → z ≤ A
25 24 albii ⊢ ∀ z ∀ x ∈ ℋ z = norm ℎ ⁡ T ⁡ x ∧ norm ℎ ⁡ x ≤ 1 → z ≤ A ↔ ∀ z ∃ x ∈ ℋ z = norm ℎ ⁡ T ⁡ x ∧ norm ℎ ⁡ x ≤ 1 → z ≤ A
26 15 23 25 3bitr3i ⊢ ∀ x ∈ ℋ norm ℎ ⁡ x ≤ 1 → norm ℎ ⁡ T ⁡ x ≤ A ↔ ∀ z ∃ x ∈ ℋ z = norm ℎ ⁡ T ⁡ x ∧ norm ℎ ⁡ x ≤ 1 → z ≤ A
27 14 26 bitr4i ⊢ ∀ z ∈ y | ∃ x ∈ ℋ norm ℎ ⁡ x ≤ 1 ∧ y = norm ℎ ⁡ T ⁡ x z ≤ A ↔ ∀ x ∈ ℋ norm ℎ ⁡ x ≤ 1 → norm ℎ ⁡ T ⁡ x ≤ A
28 8 27 bitrdi ⊢ T : ℋ ⟶ ℋ ∧ A ∈ ℝ * → sup y | ∃ x ∈ ℋ norm ℎ ⁡ x ≤ 1 ∧ y = norm ℎ ⁡ T ⁡ x ℝ * < ≤ A ↔ ∀ x ∈ ℋ norm ℎ ⁡ x ≤ 1 → norm ℎ ⁡ T ⁡ x ≤ A
29 3 28 bitrd ⊢ T : ℋ ⟶ ℋ ∧ A ∈ ℝ * → norm op ⁡ T ≤ A ↔ ∀ x ∈ ℋ norm ℎ ⁡ x ≤ 1 → norm ℎ ⁡ T ⁡ x ≤ A