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 ⊢T:ℋ⟶ℋ→normop⁡T=supx|∃y∈ℋnormℎ⁡y≤1∧x=normℎ⁡T⁡yℝ*<

Proof

Step Hyp Ref Expression
1 xrltso ⊢<Orℝ*
2 1 supex ⊢supx|∃y∈ℋnormℎ⁡y≤1∧x=normℎ⁡T⁡yℝ*<∈V
3 ax-hilex ⊢ℋ∈V
4 fveq1 ⊢t=T→t⁡y=T⁡y
5 4 fveq2d ⊢t=T→normℎ⁡t⁡y=normℎ⁡T⁡y
6 5 eqeq2d ⊢t=T→x=normℎ⁡t⁡y↔x=normℎ⁡T⁡y
7 6 anbi2d ⊢t=T→normℎ⁡y≤1∧x=normℎ⁡t⁡y↔normℎ⁡y≤1∧x=normℎ⁡T⁡y
8 7 rexbidv ⊢t=T→∃y∈ℋnormℎ⁡y≤1∧x=normℎ⁡t⁡y↔∃y∈ℋnormℎ⁡y≤1∧x=normℎ⁡T⁡y
9 8 abbidv ⊢t=T→x|∃y∈ℋnormℎ⁡y≤1∧x=normℎ⁡t⁡y=x|∃y∈ℋnormℎ⁡y≤1∧x=normℎ⁡T⁡y
10 9 supeq1d ⊢t=T→supx|∃y∈ℋnormℎ⁡y≤1∧x=normℎ⁡t⁡yℝ*<=supx|∃y∈ℋnormℎ⁡y≤1∧x=normℎ⁡T⁡yℝ*<
11 df-nmop ⊢normop=t∈ℋℋ⟼supx|∃y∈ℋnormℎ⁡y≤1∧x=normℎ⁡t⁡yℝ*<
12 2 3 3 10 11 fvmptmap ⊢T:ℋ⟶ℋ→normop⁡T=supx|∃y∈ℋnormℎ⁡y≤1∧x=normℎ⁡T⁡yℝ*<