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	⊢ ( 𝑇 : ℋ ⟶ ℋ → ( 𝑇 −op 0hop ) = 𝑇 )

Proof

Step	Hyp	Ref	Expression
1		ho0f	⊢ 0hop : ℋ ⟶ ℋ
2		ho0sub	⊢ ( ( 𝑇 : ℋ ⟶ ℋ ∧ 0hop : ℋ ⟶ ℋ ) → ( 𝑇 −op 0hop ) = ( 𝑇 +op ( 0hop −op 0hop ) ) )
3	1 2	mpan2	⊢ ( 𝑇 : ℋ ⟶ ℋ → ( 𝑇 −op 0hop ) = ( 𝑇 +op ( 0hop −op 0hop ) ) )
4	1	hodidi	⊢ ( 0hop −op 0hop ) = 0hop
5	4	oveq2i	⊢ ( 𝑇 +op ( 0hop −op 0hop ) ) = ( 𝑇 +op 0hop )
6		hoaddid1	⊢ ( 𝑇 : ℋ ⟶ ℋ → ( 𝑇 +op 0hop ) = 𝑇 )
7	5 6	syl5eq	⊢ ( 𝑇 : ℋ ⟶ ℋ → ( 𝑇 +op ( 0hop −op 0hop ) ) = 𝑇 )
8	3 7	eqtrd	⊢ ( 𝑇 : ℋ ⟶ ℋ → ( 𝑇 −op 0hop ) = 𝑇 )