This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem hhnmoi

Description: The norm of an operator in Hilbert space. (Contributed by NM, 19-Nov-2007) (Revised by Mario Carneiro, 17-Nov-2013) (New usage is discouraged.)

Ref Expression
Hypotheses hhnmo.1 ⊢ U = + ℎ ⋅ ℎ norm ℎ
hhnmo.2 ⊢ N = U normOp OLD U
Assertion hhnmoi ⊢ norm op = N

Proof

Step Hyp Ref Expression
1 hhnmo.1 ⊢ U = + ℎ ⋅ ℎ norm ℎ
2 hhnmo.2 ⊢ N = U normOp OLD U
3 df-nmop ⊢ norm op = t ∈ ℋ ℋ ⟼ sup x | ∃ y ∈ ℋ norm ℎ ⁡ y ≤ 1 ∧ x = norm ℎ ⁡ t ⁡ y ℝ * <
4 1 hhnv ⊢ U ∈ NrmCVec
5 1 hhba ⊢ ℋ = BaseSet ⁡ U
6 1 hhnm ⊢ norm ℎ = norm CV ⁡ U
7 5 5 6 6 2 nmoofval ⊢ U ∈ NrmCVec ∧ U ∈ NrmCVec → N = t ∈ ℋ ℋ ⟼ sup x | ∃ y ∈ ℋ norm ℎ ⁡ y ≤ 1 ∧ x = norm ℎ ⁡ t ⁡ y ℝ * <
8 4 4 7 mp2an ⊢ N = t ∈ ℋ ℋ ⟼ sup x | ∃ y ∈ ℋ norm ℎ ⁡ y ≤ 1 ∧ x = norm ℎ ⁡ t ⁡ y ℝ * <
9 3 8 eqtr4i ⊢ norm op = N