Theorem honegsub

Description: Relationship between Hilbert space operator addition and subtraction. (Contributed by NM, 24-Aug-2006) (New usage is discouraged.)

	Ref	Expression
Assertion	honegsub	⊢ ( ( 𝑇 : ℋ ⟶ ℋ ∧ 𝑈 : ℋ ⟶ ℋ ) → ( 𝑇 +op ( - 1 ·op 𝑈 ) ) = ( 𝑇 −op 𝑈 ) )

Proof

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