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 ) ) )