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

Metamath Proof Explorer

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 ( 𝑇 : ℋ ⟶ ℋ , 𝑇 , 0_hop ) → ( 𝑇 +_op ( - 1 ·_op 𝑈 ) ) = ( if ( 𝑇 : ℋ ⟶ ℋ , 𝑇 , 0_hop ) +_op ( - 1 ·_op 𝑈 ) ) )
2		oveq1	⊢ ( 𝑇 = if ( 𝑇 : ℋ ⟶ ℋ , 𝑇 , 0_hop ) → ( 𝑇 −_op 𝑈 ) = ( if ( 𝑇 : ℋ ⟶ ℋ , 𝑇 , 0_hop ) −_op 𝑈 ) )
3	1 2	eqeq12d	⊢ ( 𝑇 = if ( 𝑇 : ℋ ⟶ ℋ , 𝑇 , 0_hop ) → ( ( 𝑇 +_op ( - 1 ·_op 𝑈 ) ) = ( 𝑇 −_op 𝑈 ) ↔ ( if ( 𝑇 : ℋ ⟶ ℋ , 𝑇 , 0_hop ) +_op ( - 1 ·_op 𝑈 ) ) = ( if ( 𝑇 : ℋ ⟶ ℋ , 𝑇 , 0_hop ) −_op 𝑈 ) ) )
4		oveq2	⊢ ( 𝑈 = if ( 𝑈 : ℋ ⟶ ℋ , 𝑈 , 0_hop ) → ( - 1 ·_op 𝑈 ) = ( - 1 ·_op if ( 𝑈 : ℋ ⟶ ℋ , 𝑈 , 0_hop ) ) )
5	4	oveq2d	⊢ ( 𝑈 = if ( 𝑈 : ℋ ⟶ ℋ , 𝑈 , 0_hop ) → ( if ( 𝑇 : ℋ ⟶ ℋ , 𝑇 , 0_hop ) +_op ( - 1 ·_op 𝑈 ) ) = ( if ( 𝑇 : ℋ ⟶ ℋ , 𝑇 , 0_hop ) +_op ( - 1 ·_op if ( 𝑈 : ℋ ⟶ ℋ , 𝑈 , 0_hop ) ) ) )
6		oveq2	⊢ ( 𝑈 = if ( 𝑈 : ℋ ⟶ ℋ , 𝑈 , 0_hop ) → ( if ( 𝑇 : ℋ ⟶ ℋ , 𝑇 , 0_hop ) −_op 𝑈 ) = ( if ( 𝑇 : ℋ ⟶ ℋ , 𝑇 , 0_hop ) −_op if ( 𝑈 : ℋ ⟶ ℋ , 𝑈 , 0_hop ) ) )
7	5 6	eqeq12d	⊢ ( 𝑈 = if ( 𝑈 : ℋ ⟶ ℋ , 𝑈 , 0_hop ) → ( ( if ( 𝑇 : ℋ ⟶ ℋ , 𝑇 , 0_hop ) +_op ( - 1 ·_op 𝑈 ) ) = ( if ( 𝑇 : ℋ ⟶ ℋ , 𝑇 , 0_hop ) −_op 𝑈 ) ↔ ( if ( 𝑇 : ℋ ⟶ ℋ , 𝑇 , 0_hop ) +_op ( - 1 ·_op if ( 𝑈 : ℋ ⟶ ℋ , 𝑈 , 0_hop ) ) ) = ( if ( 𝑇 : ℋ ⟶ ℋ , 𝑇 , 0_hop ) −_op if ( 𝑈 : ℋ ⟶ ℋ , 𝑈 , 0_hop ) ) ) )
8		ho0f	⊢ 0_hop : ℋ ⟶ ℋ
9	8	elimf	⊢ if ( 𝑇 : ℋ ⟶ ℋ , 𝑇 , 0_hop ) : ℋ ⟶ ℋ
10	8	elimf	⊢ if ( 𝑈 : ℋ ⟶ ℋ , 𝑈 , 0_hop ) : ℋ ⟶ ℋ
11	9 10	honegsubi	⊢ ( if ( 𝑇 : ℋ ⟶ ℋ , 𝑇 , 0_hop ) +_op ( - 1 ·_op if ( 𝑈 : ℋ ⟶ ℋ , 𝑈 , 0_hop ) ) ) = ( if ( 𝑇 : ℋ ⟶ ℋ , 𝑇 , 0_hop ) −_op if ( 𝑈 : ℋ ⟶ ℋ , 𝑈 , 0_hop ) )
12	3 7 11	dedth2h	⊢ ( ( 𝑇 : ℋ ⟶ ℋ ∧ 𝑈 : ℋ ⟶ ℋ ) → ( 𝑇 +_op ( - 1 ·_op 𝑈 ) ) = ( 𝑇 −_op 𝑈 ) )