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 ⊢ 𝑈 = ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩
hhnmo.2 ⊢ 𝑁 = ( 𝑈 normOpOLD 𝑈 )
Assertion hhnmoi normop = 𝑁

Proof

Step Hyp Ref Expression
1 hhnmo.1 ⊢ 𝑈 = ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩
2 hhnmo.2 ⊢ 𝑁 = ( 𝑈 normOpOLD 𝑈 )
3 df-nmop ⊢ normop = ( 𝑡 ∈ ( ℋ ↑m ℋ ) ↦ sup ( { 𝑥 ∣ ∃ 𝑦 ∈ ℋ ( ( normℎ ‘ 𝑦 ) ≤ 1 ∧ 𝑥 = ( normℎ ‘ ( 𝑡 ‘ 𝑦 ) ) ) } , ℝ* , < ) )
4 1 hhnv ⊢ 𝑈 ∈ NrmCVec
5 1 hhba ⊢ ℋ = ( BaseSet ‘ 𝑈 )
6 1 hhnm ⊢ normℎ = ( normCV ‘ 𝑈 )
7 5 5 6 6 2 nmoofval ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑈 ∈ NrmCVec ) → 𝑁 = ( 𝑡 ∈ ( ℋ ↑m ℋ ) ↦ sup ( { 𝑥 ∣ ∃ 𝑦 ∈ ℋ ( ( normℎ ‘ 𝑦 ) ≤ 1 ∧ 𝑥 = ( normℎ ‘ ( 𝑡 ‘ 𝑦 ) ) ) } , ℝ* , < ) ) )
8 4 4 7 mp2an ⊢ 𝑁 = ( 𝑡 ∈ ( ℋ ↑m ℋ ) ↦ sup ( { 𝑥 ∣ ∃ 𝑦 ∈ ℋ ( ( normℎ ‘ 𝑦 ) ≤ 1 ∧ 𝑥 = ( normℎ ‘ ( 𝑡 ‘ 𝑦 ) ) ) } , ℝ* , < ) )
9 3 8 eqtr4i ⊢ normop = 𝑁