Metamath Proof Explorer

Theorem hoaddid1

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

Ref Expression
Assertion hoaddid1 
|- ( 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 hoaddid1i 
 |-  ( 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 )