Metamath Proof Explorer

Theorem hodid

Description: Difference of a Hilbert space operator from itself. (Contributed by NM, 23-Jul-2006) (New usage is discouraged.)

Ref Expression
Assertion hodid 
|- ( T : ~H --> ~H -> ( T -op T ) = 0hop )

Proof

Step Hyp Ref Expression
1 id 
 |-  ( T = if ( T : ~H --> ~H , T , 0hop ) -> T = if ( T : ~H --> ~H , T , 0hop ) )
2 1 1 oveq12d 
 |-  ( T = if ( T : ~H --> ~H , T , 0hop ) -> ( T -op T ) = ( if ( T : ~H --> ~H , T , 0hop ) -op if ( T : ~H --> ~H , T , 0hop ) ) )
3 2 eqeq1d 
 |-  ( T = if ( T : ~H --> ~H , T , 0hop ) -> ( ( T -op T ) = 0hop <-> ( if ( T : ~H --> ~H , T , 0hop ) -op if ( T : ~H --> ~H , T , 0hop ) ) = 0hop ) )
4 ho0f 
 |-  0hop : ~H --> ~H
5 4 elimf 
 |-  if ( T : ~H --> ~H , T , 0hop ) : ~H --> ~H
6 5 hodidi 
 |-  ( if ( T : ~H --> ~H , T , 0hop ) -op if ( T : ~H --> ~H , T , 0hop ) ) = 0hop
7 3 6 dedth 
 |-  ( T : ~H --> ~H -> ( T -op T ) = 0hop )