Metamath Proof Explorer

Theorem nmfnleub

Description: An upper bound for the norm of a functional. (Contributed by NM, 24-May-2006) (Revised by Mario Carneiro, 7-Sep-2014) (New usage is discouraged.)

Ref Expression
Assertion nmfnleub ⊢ T : ℋ ⟶ ℂ ∧ A ∈ ℝ * → norm fn ⁡ T ≤ A ↔ ∀ x ∈ ℋ norm ℎ ⁡ x ≤ 1 → T ⁡ x ≤ A

Proof

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