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 ⊢ T : ℋ ⟶ ℋ → T + op 0 hop = T

Proof

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