Metamath Proof Explorer

Theorem honegneg

Description: Double negative of a Hilbert space operator. (Contributed by NM, 24-Aug-2006) (New usage is discouraged.)

Ref Expression
Assertion honegneg 
|- ( T : ~H --> ~H -> ( -u 1 .op ( -u 1 .op T ) ) = T )

Proof

Step Hyp Ref Expression
1 neg1mulneg1e1 
 |-  ( -u 1 x. -u 1 ) = 1
2 1 oveq1i 
 |-  ( ( -u 1 x. -u 1 ) .op T ) = ( 1 .op T )
3 neg1cn 
 |-  -u 1 e. CC
4 homulass 
 |-  ( ( -u 1 e. CC /\ -u 1 e. CC /\ T : ~H --> ~H ) -> ( ( -u 1 x. -u 1 ) .op T ) = ( -u 1 .op ( -u 1 .op T ) ) )
5 3 3 4 mp3an12 
 |-  ( T : ~H --> ~H -> ( ( -u 1 x. -u 1 ) .op T ) = ( -u 1 .op ( -u 1 .op T ) ) )
6 homulid2 
 |-  ( T : ~H --> ~H -> ( 1 .op T ) = T )
7 2 5 6 3eqtr3a 
 |-  ( T : ~H --> ~H -> ( -u 1 .op ( -u 1 .op T ) ) = T )