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 ‘ ( 𝑇 ‘ 𝑦 ) ) ) } , ℝ* , < ) )