# Metamath Proof Explorer

Description: Sum of a Hilbert space operator with the zero operator. (Contributed by NM, 15-Nov-2000) (New usage is discouraged.)

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

### Proof

Step Hyp Ref Expression
` |-  T : ~H --> ~H`
2 ho0f
` |-  0hop : ~H --> ~H`
3 hosval
` |-  ( ( T : ~H --> ~H /\ 0hop : ~H --> ~H /\ x e. ~H ) -> ( ( T +op 0hop ) ` x ) = ( ( T ` x ) +h ( 0hop ` x ) ) )`
4 1 2 3 mp3an12
` |-  ( x e. ~H -> ( ( T +op 0hop ) ` x ) = ( ( T ` x ) +h ( 0hop ` x ) ) )`
5 ho0val
` |-  ( x e. ~H -> ( 0hop ` x ) = 0h )`
6 5 oveq2d
` |-  ( x e. ~H -> ( ( T ` x ) +h ( 0hop ` x ) ) = ( ( T ` x ) +h 0h ) )`
7 1 ffvelrni
` |-  ( x e. ~H -> ( T ` x ) e. ~H )`
` |-  ( ( T ` x ) e. ~H -> ( ( T ` x ) +h 0h ) = ( T ` x ) )`
` |-  ( x e. ~H -> ( ( T ` x ) +h 0h ) = ( T ` x ) )`
` |-  ( x e. ~H -> ( ( T +op 0hop ) ` x ) = ( T ` x ) )`
` |-  A. x e. ~H ( ( T +op 0hop ) ` x ) = ( T ` x )`
` |-  ( T +op 0hop ) : ~H --> ~H`
` |-  ( A. x e. ~H ( ( T +op 0hop ) ` x ) = ( T ` x ) <-> ( T +op 0hop ) = T )`
` |-  ( T +op 0hop ) = T`