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

Metamath Proof Explorer

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

Proof

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