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 ) |
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 ) |