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 ( 𝑇 : ℋ ⟶ ℋ → ( 𝑇 −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 )