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 𝑇 ) ) )