Theorem nmopxr

Description: The norm of a Hilbert space operator is an extended real. (Contributed by NM, 9-Feb-2006) (New usage is discouraged.)

	Ref	Expression
Assertion	nmopxr	⊢ ( 𝑇 : ℋ ⟶ ℋ → ( normop ‘ 𝑇 ) ∈ ℝ* )

Proof

Step	Hyp	Ref	Expression
1		nmopval	⊢ ( 𝑇 : ℋ ⟶ ℋ → ( normop ‘ 𝑇 ) = sup ( { 𝑥 ∣ ∃ 𝑦 ∈ ℋ ( ( normℎ ‘ 𝑦 ) ≤ 1 ∧ 𝑥 = ( normℎ ‘ ( 𝑇 ‘ 𝑦 ) ) ) } , ℝ* , < ) )
2		nmopsetretHIL	⊢ ( 𝑇 : ℋ ⟶ ℋ → { 𝑥 ∣ ∃ 𝑦 ∈ ℋ ( ( normℎ ‘ 𝑦 ) ≤ 1 ∧ 𝑥 = ( normℎ ‘ ( 𝑇 ‘ 𝑦 ) ) ) } ⊆ ℝ )
3		ressxr	⊢ ℝ ⊆ ℝ*
4	2 3	sstrdi	⊢ ( 𝑇 : ℋ ⟶ ℋ → { 𝑥 ∣ ∃ 𝑦 ∈ ℋ ( ( normℎ ‘ 𝑦 ) ≤ 1 ∧ 𝑥 = ( normℎ ‘ ( 𝑇 ‘ 𝑦 ) ) ) } ⊆ ℝ* )
5		supxrcl	⊢ ( { 𝑥 ∣ ∃ 𝑦 ∈ ℋ ( ( normℎ ‘ 𝑦 ) ≤ 1 ∧ 𝑥 = ( normℎ ‘ ( 𝑇 ‘ 𝑦 ) ) ) } ⊆ ℝ* → sup ( { 𝑥 ∣ ∃ 𝑦 ∈ ℋ ( ( normℎ ‘ 𝑦 ) ≤ 1 ∧ 𝑥 = ( normℎ ‘ ( 𝑇 ‘ 𝑦 ) ) ) } , ℝ* , < ) ∈ ℝ* )
6	4 5	syl	⊢ ( 𝑇 : ℋ ⟶ ℋ → sup ( { 𝑥 ∣ ∃ 𝑦 ∈ ℋ ( ( normℎ ‘ 𝑦 ) ≤ 1 ∧ 𝑥 = ( normℎ ‘ ( 𝑇 ‘ 𝑦 ) ) ) } , ℝ* , < ) ∈ ℝ* )
7	1 6	eqeltrd	⊢ ( 𝑇 : ℋ ⟶ ℋ → ( normop ‘ 𝑇 ) ∈ ℝ* )