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 = 𝑁