Metamath Proof Explorer

Theorem nmopval

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

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

Proof

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