Theorem hoaddid1

Description: Sum of a Hilbert space operator with the zero operator. (Contributed by NM, 25-Jul-2006) (New usage is discouraged.)

	Ref	Expression
Assertion	hoaddid1	⊢ ( 𝑇 : ℋ ⟶ ℋ → ( 𝑇 +op 0hop ) = 𝑇 )

Proof

Step	Hyp	Ref	Expression
1		oveq1	⊢ ( 𝑇 = if ( 𝑇 : ℋ ⟶ ℋ , 𝑇 , 0hop ) → ( 𝑇 +op 0hop ) = ( if ( 𝑇 : ℋ ⟶ ℋ , 𝑇 , 0hop ) +op 0hop ) )
2		id	⊢ ( 𝑇 = if ( 𝑇 : ℋ ⟶ ℋ , 𝑇 , 0hop ) → 𝑇 = if ( 𝑇 : ℋ ⟶ ℋ , 𝑇 , 0hop ) )
3	1 2	eqeq12d	⊢ ( 𝑇 = if ( 𝑇 : ℋ ⟶ ℋ , 𝑇 , 0hop ) → ( ( 𝑇 +op 0hop ) = 𝑇 ↔ ( if ( 𝑇 : ℋ ⟶ ℋ , 𝑇 , 0hop ) +op 0hop ) = if ( 𝑇 : ℋ ⟶ ℋ , 𝑇 , 0hop ) ) )
4		ho0f	⊢ 0hop : ℋ ⟶ ℋ
5	4	elimf	⊢ if ( 𝑇 : ℋ ⟶ ℋ , 𝑇 , 0hop ) : ℋ ⟶ ℋ
6	5	hoaddid1i	⊢ ( if ( 𝑇 : ℋ ⟶ ℋ , 𝑇 , 0hop ) +op 0hop ) = if ( 𝑇 : ℋ ⟶ ℋ , 𝑇 , 0hop )
7	3 6	dedth	⊢ ( 𝑇 : ℋ ⟶ ℋ → ( 𝑇 +op 0hop ) = 𝑇 )