Metamath Proof Explorer

Theorem nmopnegi

Description: Value of the norm of the negative of a Hilbert space operator. Unlike nmophmi , the operator does not have to be bounded. (Contributed by NM, 10-Mar-2006) (New usage is discouraged.)

Ref Expression
Hypothesis nmopneg.1 
|- T : ~H --> ~H
Assertion nmopnegi 
|- ( normop ` ( -u 1 .op T ) ) = ( normop ` T )

Proof

Step Hyp Ref Expression
1 nmopneg.1 
 |-  T : ~H --> ~H
2 neg1cn 
 |-  -u 1 e. CC
3 homval 
 |-  ( ( -u 1 e. CC /\ T : ~H --> ~H /\ y e. ~H ) -> ( ( -u 1 .op T ) ` y ) = ( -u 1 .h ( T ` y ) ) )
4 2 1 3 mp3an12 
 |-  ( y e. ~H -> ( ( -u 1 .op T ) ` y ) = ( -u 1 .h ( T ` y ) ) )
5 4 fveq2d 
 |-  ( y e. ~H -> ( normh ` ( ( -u 1 .op T ) ` y ) ) = ( normh ` ( -u 1 .h ( T ` y ) ) ) )
6 1 ffvelrni 
 |-  ( y e. ~H -> ( T ` y ) e. ~H )
7 normneg 
 |-  ( ( T ` y ) e. ~H -> ( normh ` ( -u 1 .h ( T ` y ) ) ) = ( normh ` ( T ` y ) ) )
8 6 7 syl 
 |-  ( y e. ~H -> ( normh ` ( -u 1 .h ( T ` y ) ) ) = ( normh ` ( T ` y ) ) )
9 5 8 eqtrd 
 |-  ( y e. ~H -> ( normh ` ( ( -u 1 .op T ) ` y ) ) = ( normh ` ( T ` y ) ) )
10 9 eqeq2d 
 |-  ( y e. ~H -> ( x = ( normh ` ( ( -u 1 .op T ) ` y ) ) <-> x = ( normh ` ( T ` y ) ) ) )
11 10 anbi2d 
 |-  ( y e. ~H -> ( ( ( normh ` y ) <_ 1 /\ x = ( normh ` ( ( -u 1 .op T ) ` y ) ) ) <-> ( ( normh ` y ) <_ 1 /\ x = ( normh ` ( T ` y ) ) ) ) )
12 11 rexbiia 
 |-  ( E. y e. ~H ( ( normh ` y ) <_ 1 /\ x = ( normh ` ( ( -u 1 .op T ) ` y ) ) ) <-> E. y e. ~H ( ( normh ` y ) <_ 1 /\ x = ( normh ` ( T ` y ) ) ) )
13 12 abbii 
 |-  { x | E. y e. ~H ( ( normh ` y ) <_ 1 /\ x = ( normh ` ( ( -u 1 .op T ) ` y ) ) ) } = { x | E. y e. ~H ( ( normh ` y ) <_ 1 /\ x = ( normh ` ( T ` y ) ) ) }
14 13 supeq1i 
 |-  sup ( { x | E. y e. ~H ( ( normh ` y ) <_ 1 /\ x = ( normh ` ( ( -u 1 .op T ) ` y ) ) ) } , RR* , < ) = sup ( { x | E. y e. ~H ( ( normh ` y ) <_ 1 /\ x = ( normh ` ( T ` y ) ) ) } , RR* , < )
15 homulcl 
 |-  ( ( -u 1 e. CC /\ T : ~H --> ~H ) -> ( -u 1 .op T ) : ~H --> ~H )
16 2 1 15 mp2an 
 |-  ( -u 1 .op T ) : ~H --> ~H
17 nmopval 
 |-  ( ( -u 1 .op T ) : ~H --> ~H -> ( normop ` ( -u 1 .op T ) ) = sup ( { x | E. y e. ~H ( ( normh ` y ) <_ 1 /\ x = ( normh ` ( ( -u 1 .op T ) ` y ) ) ) } , RR* , < ) )
18 16 17 ax-mp 
 |-  ( normop ` ( -u 1 .op T ) ) = sup ( { x | E. y e. ~H ( ( normh ` y ) <_ 1 /\ x = ( normh ` ( ( -u 1 .op T ) ` y ) ) ) } , RR* , < )
19 nmopval 
 |-  ( T : ~H --> ~H -> ( normop ` T ) = sup ( { x | E. y e. ~H ( ( normh ` y ) <_ 1 /\ x = ( normh ` ( T ` y ) ) ) } , RR* , < ) )
20 1 19 ax-mp 
 |-  ( normop ` T ) = sup ( { x | E. y e. ~H ( ( normh ` y ) <_ 1 /\ x = ( normh ` ( T ` y ) ) ) } , RR* , < )
21 14 18 20 3eqtr4i 
 |-  ( normop ` ( -u 1 .op T ) ) = ( normop ` T )