This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem hoaddrid

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

Ref Expression
Assertion hoaddrid ( 𝑇 : ℋ ⟶ ℋ → ( 𝑇 +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 hoaddridi ⊢ ( if ( 𝑇 : ℋ ⟶ ℋ , 𝑇 , 0hop ) +op 0hop ) = if ( 𝑇 : ℋ ⟶ ℋ , 𝑇 , 0hop )
7 3 6 dedth ⊢ ( 𝑇 : ℋ ⟶ ℋ → ( 𝑇 +op 0hop ) = 𝑇 )