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

Metamath Proof Explorer

Theorem ho0sub

Description: Subtraction of Hilbert space operators expressed in terms of difference from zero. (Contributed by NM, 25-Jul-2006) (New usage is discouraged.)

Ref Expression
Assertion ho0sub 
|- ( ( S : ~H --> ~H /\ T : ~H --> ~H ) -> ( S -op T ) = ( S +op ( 0hop -op T ) ) )

Proof

Step Hyp Ref Expression
1 oveq1 
 |-  ( S = if ( S : ~H --> ~H , S , 0hop ) -> ( S -op T ) = ( if ( S : ~H --> ~H , S , 0hop ) -op T ) )
2 oveq1 
 |-  ( S = if ( S : ~H --> ~H , S , 0hop ) -> ( S +op ( 0hop -op T ) ) = ( if ( S : ~H --> ~H , S , 0hop ) +op ( 0hop -op T ) ) )
3 1 2 eqeq12d 
 |-  ( S = if ( S : ~H --> ~H , S , 0hop ) -> ( ( S -op T ) = ( S +op ( 0hop -op T ) ) <-> ( if ( S : ~H --> ~H , S , 0hop ) -op T ) = ( if ( S : ~H --> ~H , S , 0hop ) +op ( 0hop -op T ) ) ) )
4 oveq2 
 |-  ( T = if ( T : ~H --> ~H , T , 0hop ) -> ( if ( S : ~H --> ~H , S , 0hop ) -op T ) = ( if ( S : ~H --> ~H , S , 0hop ) -op if ( T : ~H --> ~H , T , 0hop ) ) )
5 oveq2 
 |-  ( T = if ( T : ~H --> ~H , T , 0hop ) -> ( 0hop -op T ) = ( 0hop -op if ( T : ~H --> ~H , T , 0hop ) ) )
6 5 oveq2d 
 |-  ( T = if ( T : ~H --> ~H , T , 0hop ) -> ( if ( S : ~H --> ~H , S , 0hop ) +op ( 0hop -op T ) ) = ( if ( S : ~H --> ~H , S , 0hop ) +op ( 0hop -op if ( T : ~H --> ~H , T , 0hop ) ) ) )
7 4 6 eqeq12d 
 |-  ( T = if ( T : ~H --> ~H , T , 0hop ) -> ( ( if ( S : ~H --> ~H , S , 0hop ) -op T ) = ( if ( S : ~H --> ~H , S , 0hop ) +op ( 0hop -op T ) ) <-> ( if ( S : ~H --> ~H , S , 0hop ) -op if ( T : ~H --> ~H , T , 0hop ) ) = ( if ( S : ~H --> ~H , S , 0hop ) +op ( 0hop -op if ( T : ~H --> ~H , T , 0hop ) ) ) ) )
8 ho0f 
 |-  0hop : ~H --> ~H
9 8 elimf 
 |-  if ( S : ~H --> ~H , S , 0hop ) : ~H --> ~H
10 8 elimf 
 |-  if ( T : ~H --> ~H , T , 0hop ) : ~H --> ~H
11 9 10 ho0subi 
 |-  ( if ( S : ~H --> ~H , S , 0hop ) -op if ( T : ~H --> ~H , T , 0hop ) ) = ( if ( S : ~H --> ~H , S , 0hop ) +op ( 0hop -op if ( T : ~H --> ~H , T , 0hop ) ) )
12 3 7 11 dedth2h 
 |-  ( ( S : ~H --> ~H /\ T : ~H --> ~H ) -> ( S -op T ) = ( S +op ( 0hop -op T ) ) )