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

Metamath Proof Explorer

Theorem ho0sub

Description: Subtraction of Hilbert space operators expressed in terms of difference from zero. (Contributed by NM, 25-Jul-2006) (New usage is discouraged.)

Ref Expression
Assertion ho0sub ( ( 𝑆 : ℋ ⟶ ℋ ∧ 𝑇 : ℋ ⟶ ℋ ) → ( 𝑆 −op 𝑇 ) = ( 𝑆 +op ( 0hop −op 𝑇 ) ) )

Proof

Step Hyp Ref Expression
1 oveq1 ⊢ ( 𝑆 = if ( 𝑆 : ℋ ⟶ ℋ , 𝑆 , 0hop ) → ( 𝑆 −op 𝑇 ) = ( if ( 𝑆 : ℋ ⟶ ℋ , 𝑆 , 0hop ) −op 𝑇 ) )
2 oveq1 ⊢ ( 𝑆 = if ( 𝑆 : ℋ ⟶ ℋ , 𝑆 , 0hop ) → ( 𝑆 +op ( 0hop −op 𝑇 ) ) = ( if ( 𝑆 : ℋ ⟶ ℋ , 𝑆 , 0hop ) +op ( 0hop −op 𝑇 ) ) )
3 1 2 eqeq12d ⊢ ( 𝑆 = if ( 𝑆 : ℋ ⟶ ℋ , 𝑆 , 0hop ) → ( ( 𝑆 −op 𝑇 ) = ( 𝑆 +op ( 0hop −op 𝑇 ) ) ↔ ( if ( 𝑆 : ℋ ⟶ ℋ , 𝑆 , 0hop ) −op 𝑇 ) = ( if ( 𝑆 : ℋ ⟶ ℋ , 𝑆 , 0hop ) +op ( 0hop −op 𝑇 ) ) ) )
4 oveq2 ⊢ ( 𝑇 = if ( 𝑇 : ℋ ⟶ ℋ , 𝑇 , 0hop ) → ( if ( 𝑆 : ℋ ⟶ ℋ , 𝑆 , 0hop ) −op 𝑇 ) = ( if ( 𝑆 : ℋ ⟶ ℋ , 𝑆 , 0hop ) −op if ( 𝑇 : ℋ ⟶ ℋ , 𝑇 , 0hop ) ) )
5 oveq2 ⊢ ( 𝑇 = if ( 𝑇 : ℋ ⟶ ℋ , 𝑇 , 0hop ) → ( 0hop −op 𝑇 ) = ( 0hop −op if ( 𝑇 : ℋ ⟶ ℋ , 𝑇 , 0hop ) ) )
6 5 oveq2d ⊢ ( 𝑇 = if ( 𝑇 : ℋ ⟶ ℋ , 𝑇 , 0hop ) → ( if ( 𝑆 : ℋ ⟶ ℋ , 𝑆 , 0hop ) +op ( 0hop −op 𝑇 ) ) = ( if ( 𝑆 : ℋ ⟶ ℋ , 𝑆 , 0hop ) +op ( 0hop −op if ( 𝑇 : ℋ ⟶ ℋ , 𝑇 , 0hop ) ) ) )
7 4 6 eqeq12d ⊢ ( 𝑇 = if ( 𝑇 : ℋ ⟶ ℋ , 𝑇 , 0hop ) → ( ( if ( 𝑆 : ℋ ⟶ ℋ , 𝑆 , 0hop ) −op 𝑇 ) = ( if ( 𝑆 : ℋ ⟶ ℋ , 𝑆 , 0hop ) +op ( 0hop −op 𝑇 ) ) ↔ ( if ( 𝑆 : ℋ ⟶ ℋ , 𝑆 , 0hop ) −op if ( 𝑇 : ℋ ⟶ ℋ , 𝑇 , 0hop ) ) = ( if ( 𝑆 : ℋ ⟶ ℋ , 𝑆 , 0hop ) +op ( 0hop −op if ( 𝑇 : ℋ ⟶ ℋ , 𝑇 , 0hop ) ) ) ) )
8 ho0f ⊢ 0hop : ℋ ⟶ ℋ
9 8 elimf ⊢ if ( 𝑆 : ℋ ⟶ ℋ , 𝑆 , 0hop ) : ℋ ⟶ ℋ
10 8 elimf ⊢ if ( 𝑇 : ℋ ⟶ ℋ , 𝑇 , 0hop ) : ℋ ⟶ ℋ
11 9 10 ho0subi ⊢ ( if ( 𝑆 : ℋ ⟶ ℋ , 𝑆 , 0hop ) −op if ( 𝑇 : ℋ ⟶ ℋ , 𝑇 , 0hop ) ) = ( if ( 𝑆 : ℋ ⟶ ℋ , 𝑆 , 0hop ) +op ( 0hop −op if ( 𝑇 : ℋ ⟶ ℋ , 𝑇 , 0hop ) ) )
12 3 7 11 dedth2h ⊢ ( ( 𝑆 : ℋ ⟶ ℋ ∧ 𝑇 : ℋ ⟶ ℋ ) → ( 𝑆 −op 𝑇 ) = ( 𝑆 +op ( 0hop −op 𝑇 ) ) )