This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem hoaddrid

Description: Sum of a Hilbert space operator with the zero operator. (Contributed by NM, 25-Jul-2006) (New usage is discouraged.)

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

Proof

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