Theorem honegsub

Description: Relationship between Hilbert space operator addition and subtraction. (Contributed by NM, 24-Aug-2006) (New usage is discouraged.)

	Ref	Expression
Assertion	honegsub	|- ( ( T : ~H --> ~H /\ U : ~H --> ~H ) -> ( T +op ( -u 1 .op U ) ) = ( T -op U ) )

Proof

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