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

Metamath Proof Explorer

Theorem hosubid1

Description: The zero operator subtracted from a Hilbert space operator. (Contributed by NM, 25-Jul-2006) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 ho0f 
 |-  0hop : ~H --> ~H
2 ho0sub 
 |-  ( ( T : ~H --> ~H /\ 0hop : ~H --> ~H ) -> ( T -op 0hop ) = ( T +op ( 0hop -op 0hop ) ) )
3 1 2 mpan2 
 |-  ( T : ~H --> ~H -> ( T -op 0hop ) = ( T +op ( 0hop -op 0hop ) ) )
4 1 hodidi 
 |-  ( 0hop -op 0hop ) = 0hop
5 4 oveq2i 
 |-  ( T +op ( 0hop -op 0hop ) ) = ( T +op 0hop )
6 hoaddrid 
 |-  ( T : ~H --> ~H -> ( T +op 0hop ) = T )
7 5 6 eqtrid 
 |-  ( T : ~H --> ~H -> ( T +op ( 0hop -op 0hop ) ) = T )
8 3 7 eqtrd 
 |-  ( T : ~H --> ~H -> ( T -op 0hop ) = T )