Theorem hodid

Description: Difference of a Hilbert space operator from itself. (Contributed by NM, 23-Jul-2006) (New usage is discouraged.)

	Ref	Expression
Assertion	hodid	⊢ ( 𝑇 : ℋ ⟶ ℋ → ( 𝑇 −op 𝑇 ) = 0hop )

Proof

Step	Hyp	Ref	Expression
1		id	⊢ ( 𝑇 = if ( 𝑇 : ℋ ⟶ ℋ , 𝑇 , 0hop ) → 𝑇 = if ( 𝑇 : ℋ ⟶ ℋ , 𝑇 , 0hop ) )
2	1 1	oveq12d	⊢ ( 𝑇 = if ( 𝑇 : ℋ ⟶ ℋ , 𝑇 , 0hop ) → ( 𝑇 −op 𝑇 ) = ( if ( 𝑇 : ℋ ⟶ ℋ , 𝑇 , 0hop ) −op if ( 𝑇 : ℋ ⟶ ℋ , 𝑇 , 0hop ) ) )
3	2	eqeq1d	⊢ ( 𝑇 = if ( 𝑇 : ℋ ⟶ ℋ , 𝑇 , 0hop ) → ( ( 𝑇 −op 𝑇 ) = 0hop ↔ ( if ( 𝑇 : ℋ ⟶ ℋ , 𝑇 , 0hop ) −op if ( 𝑇 : ℋ ⟶ ℋ , 𝑇 , 0hop ) ) = 0hop ) )
4		ho0f	⊢ 0hop : ℋ ⟶ ℋ
5	4	elimf	⊢ if ( 𝑇 : ℋ ⟶ ℋ , 𝑇 , 0hop ) : ℋ ⟶ ℋ
6	5	hodidi	⊢ ( if ( 𝑇 : ℋ ⟶ ℋ , 𝑇 , 0hop ) −op if ( 𝑇 : ℋ ⟶ ℋ , 𝑇 , 0hop ) ) = 0hop
7	3 6	dedth	⊢ ( 𝑇 : ℋ ⟶ ℋ → ( 𝑇 −op 𝑇 ) = 0hop )