This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem nmfnval

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

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

Proof

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