# Metamath Proof Explorer

## Theorem nmopval

Description: Value of the norm of a Hilbert space operator. (Contributed by NM, 18-Jan-2006) (Revised by Mario Carneiro, 16-Nov-2013) (New usage is discouraged.)

Ref Expression
Assertion nmopval ( 𝑇 : ℋ ⟶ ℋ → ( normop𝑇 ) = sup ( { 𝑥 ∣ ∃ 𝑦 ∈ ℋ ( ( norm𝑦 ) ≤ 1 ∧ 𝑥 = ( norm ‘ ( 𝑇𝑦 ) ) ) } , ℝ* , < ) )

### Proof

Step Hyp Ref Expression
1 xrltso < Or ℝ*
2 1 supex sup ( { 𝑥 ∣ ∃ 𝑦 ∈ ℋ ( ( norm𝑦 ) ≤ 1 ∧ 𝑥 = ( norm ‘ ( 𝑇𝑦 ) ) ) } , ℝ* , < ) ∈ V
3 ax-hilex ℋ ∈ V
4 fveq1 ( 𝑡 = 𝑇 → ( 𝑡𝑦 ) = ( 𝑇𝑦 ) )
5 4 fveq2d ( 𝑡 = 𝑇 → ( norm ‘ ( 𝑡𝑦 ) ) = ( norm ‘ ( 𝑇𝑦 ) ) )
6 5 eqeq2d ( 𝑡 = 𝑇 → ( 𝑥 = ( norm ‘ ( 𝑡𝑦 ) ) ↔ 𝑥 = ( norm ‘ ( 𝑇𝑦 ) ) ) )
7 6 anbi2d ( 𝑡 = 𝑇 → ( ( ( norm𝑦 ) ≤ 1 ∧ 𝑥 = ( norm ‘ ( 𝑡𝑦 ) ) ) ↔ ( ( norm𝑦 ) ≤ 1 ∧ 𝑥 = ( norm ‘ ( 𝑇𝑦 ) ) ) ) )
8 7 rexbidv ( 𝑡 = 𝑇 → ( ∃ 𝑦 ∈ ℋ ( ( norm𝑦 ) ≤ 1 ∧ 𝑥 = ( norm ‘ ( 𝑡𝑦 ) ) ) ↔ ∃ 𝑦 ∈ ℋ ( ( norm𝑦 ) ≤ 1 ∧ 𝑥 = ( norm ‘ ( 𝑇𝑦 ) ) ) ) )
9 8 abbidv ( 𝑡 = 𝑇 → { 𝑥 ∣ ∃ 𝑦 ∈ ℋ ( ( norm𝑦 ) ≤ 1 ∧ 𝑥 = ( norm ‘ ( 𝑡𝑦 ) ) ) } = { 𝑥 ∣ ∃ 𝑦 ∈ ℋ ( ( norm𝑦 ) ≤ 1 ∧ 𝑥 = ( norm ‘ ( 𝑇𝑦 ) ) ) } )
10 9 supeq1d ( 𝑡 = 𝑇 → sup ( { 𝑥 ∣ ∃ 𝑦 ∈ ℋ ( ( norm𝑦 ) ≤ 1 ∧ 𝑥 = ( norm ‘ ( 𝑡𝑦 ) ) ) } , ℝ* , < ) = sup ( { 𝑥 ∣ ∃ 𝑦 ∈ ℋ ( ( norm𝑦 ) ≤ 1 ∧ 𝑥 = ( norm ‘ ( 𝑇𝑦 ) ) ) } , ℝ* , < ) )
11 df-nmop normop = ( 𝑡 ∈ ( ℋ ↑m ℋ ) ↦ sup ( { 𝑥 ∣ ∃ 𝑦 ∈ ℋ ( ( norm𝑦 ) ≤ 1 ∧ 𝑥 = ( norm ‘ ( 𝑡𝑦 ) ) ) } , ℝ* , < ) )
12 2 3 3 10 11 fvmptmap ( 𝑇 : ℋ ⟶ ℋ → ( normop𝑇 ) = sup ( { 𝑥 ∣ ∃ 𝑦 ∈ ℋ ( ( norm𝑦 ) ≤ 1 ∧ 𝑥 = ( norm ‘ ( 𝑇𝑦 ) ) ) } , ℝ* , < ) )