Metamath Proof Explorer

Theorem nmfnval

Description: Value of the norm of a Hilbert space functional. (Contributed by NM, 11-Feb-2006) (Revised by Mario Carneiro, 16-Nov-2013) (New usage is discouraged.)

Ref Expression
Assertion nmfnval ⊢ T : ℋ ⟶ ℂ → norm fn ⁡ T = sup x | ∃ y ∈ ℋ norm ℎ ⁡ y ≤ 1 ∧ x = T ⁡ y ℝ * <

Proof

Step Hyp Ref Expression
1 xrltso ⊢ < Or ℝ *
2 1 supex ⊢ sup x | ∃ y ∈ ℋ norm ℎ ⁡ y ≤ 1 ∧ x = T ⁡ y ℝ * < ∈ V
3 ax-hilex ⊢ ℋ ∈ V
4 cnex ⊢ ℂ ∈ V
5 fveq1 ⊢ t = T → t ⁡ y = T ⁡ y
6 5 fveq2d ⊢ t = T → t ⁡ y = T ⁡ y
7 6 eqeq2d ⊢ t = T → x = t ⁡ y ↔ x = T ⁡ y
8 7 anbi2d ⊢ t = T → norm ℎ ⁡ y ≤ 1 ∧ x = t ⁡ y ↔ norm ℎ ⁡ y ≤ 1 ∧ x = T ⁡ y
9 8 rexbidv ⊢ t = T → ∃ y ∈ ℋ norm ℎ ⁡ y ≤ 1 ∧ x = t ⁡ y ↔ ∃ y ∈ ℋ norm ℎ ⁡ y ≤ 1 ∧ x = T ⁡ y
10 9 abbidv ⊢ t = T → x | ∃ y ∈ ℋ norm ℎ ⁡ y ≤ 1 ∧ x = t ⁡ y = x | ∃ y ∈ ℋ norm ℎ ⁡ y ≤ 1 ∧ x = T ⁡ y
11 10 supeq1d ⊢ t = T → sup x | ∃ y ∈ ℋ norm ℎ ⁡ y ≤ 1 ∧ x = t ⁡ y ℝ * < = sup x | ∃ y ∈ ℋ norm ℎ ⁡ y ≤ 1 ∧ x = T ⁡ y ℝ * <
12 df-nmfn ⊢ norm fn = t ∈ ℂ ℋ ⟼ sup x | ∃ y ∈ ℋ norm ℎ ⁡ y ≤ 1 ∧ x = t ⁡ y ℝ * <
13 2 3 4 11 12 fvmptmap ⊢ T : ℋ ⟶ ℂ → norm fn ⁡ T = sup x | ∃ y ∈ ℋ norm ℎ ⁡ y ≤ 1 ∧ x = T ⁡ y ℝ * <