# Metamath Proof Explorer

## Theorem nmoprepnf

Description: The norm of a Hilbert space operator is either real or plus infinity. (Contributed by NM, 5-Feb-2006) (New usage is discouraged.)

Ref Expression
Assertion nmoprepnf ( 𝑇 : ℋ ⟶ ℋ → ( ( normop𝑇 ) ∈ ℝ ↔ ( normop𝑇 ) ≠ +∞ ) )

### Proof

Step Hyp Ref Expression
1 nmopsetretHIL ( 𝑇 : ℋ ⟶ ℋ → { 𝑥 ∣ ∃ 𝑦 ∈ ℋ ( ( norm𝑦 ) ≤ 1 ∧ 𝑥 = ( norm ‘ ( 𝑇𝑦 ) ) ) } ⊆ ℝ )
2 nmopsetn0 ( norm ‘ ( 𝑇 ‘ 0 ) ) ∈ { 𝑥 ∣ ∃ 𝑦 ∈ ℋ ( ( norm𝑦 ) ≤ 1 ∧ 𝑥 = ( norm ‘ ( 𝑇𝑦 ) ) ) }
3 2 ne0ii { 𝑥 ∣ ∃ 𝑦 ∈ ℋ ( ( norm𝑦 ) ≤ 1 ∧ 𝑥 = ( norm ‘ ( 𝑇𝑦 ) ) ) } ≠ ∅
4 supxrre2 ( ( { 𝑥 ∣ ∃ 𝑦 ∈ ℋ ( ( norm𝑦 ) ≤ 1 ∧ 𝑥 = ( norm ‘ ( 𝑇𝑦 ) ) ) } ⊆ ℝ ∧ { 𝑥 ∣ ∃ 𝑦 ∈ ℋ ( ( norm𝑦 ) ≤ 1 ∧ 𝑥 = ( norm ‘ ( 𝑇𝑦 ) ) ) } ≠ ∅ ) → ( sup ( { 𝑥 ∣ ∃ 𝑦 ∈ ℋ ( ( norm𝑦 ) ≤ 1 ∧ 𝑥 = ( norm ‘ ( 𝑇𝑦 ) ) ) } , ℝ* , < ) ∈ ℝ ↔ sup ( { 𝑥 ∣ ∃ 𝑦 ∈ ℋ ( ( norm𝑦 ) ≤ 1 ∧ 𝑥 = ( norm ‘ ( 𝑇𝑦 ) ) ) } , ℝ* , < ) ≠ +∞ ) )
5 1 3 4 sylancl ( 𝑇 : ℋ ⟶ ℋ → ( sup ( { 𝑥 ∣ ∃ 𝑦 ∈ ℋ ( ( norm𝑦 ) ≤ 1 ∧ 𝑥 = ( norm ‘ ( 𝑇𝑦 ) ) ) } , ℝ* , < ) ∈ ℝ ↔ sup ( { 𝑥 ∣ ∃ 𝑦 ∈ ℋ ( ( norm𝑦 ) ≤ 1 ∧ 𝑥 = ( norm ‘ ( 𝑇𝑦 ) ) ) } , ℝ* , < ) ≠ +∞ ) )
6 nmopval ( 𝑇 : ℋ ⟶ ℋ → ( normop𝑇 ) = sup ( { 𝑥 ∣ ∃ 𝑦 ∈ ℋ ( ( norm𝑦 ) ≤ 1 ∧ 𝑥 = ( norm ‘ ( 𝑇𝑦 ) ) ) } , ℝ* , < ) )
7 6 eleq1d ( 𝑇 : ℋ ⟶ ℋ → ( ( normop𝑇 ) ∈ ℝ ↔ sup ( { 𝑥 ∣ ∃ 𝑦 ∈ ℋ ( ( norm𝑦 ) ≤ 1 ∧ 𝑥 = ( norm ‘ ( 𝑇𝑦 ) ) ) } , ℝ* , < ) ∈ ℝ ) )
8 6 neeq1d ( 𝑇 : ℋ ⟶ ℋ → ( ( normop𝑇 ) ≠ +∞ ↔ sup ( { 𝑥 ∣ ∃ 𝑦 ∈ ℋ ( ( norm𝑦 ) ≤ 1 ∧ 𝑥 = ( norm ‘ ( 𝑇𝑦 ) ) ) } , ℝ* , < ) ≠ +∞ ) )
9 5 7 8 3bitr4d ( 𝑇 : ℋ ⟶ ℋ → ( ( normop𝑇 ) ∈ ℝ ↔ ( normop𝑇 ) ≠ +∞ ) )