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		hoaddid1	|- ( T : ~H --> ~H -> ( T +op 0hop ) = T )
7	5 6	syl5eq	|- ( T : ~H --> ~H -> ( T +op ( 0hop -op 0hop ) ) = T )
8	3 7	eqtrd	|- ( T : ~H --> ~H -> ( T -op 0hop ) = T )