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