Theorem hosubneg

Description: Relationship between operator subtraction and negative. (Contributed by NM, 25-Aug-2006) (New usage is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		neg1cn	⊢ - 1 ∈ ℂ
2		homulcl	⊢ ( ( - 1 ∈ ℂ ∧ 𝑈 : ℋ ⟶ ℋ ) → ( - 1 ·op 𝑈 ) : ℋ ⟶ ℋ )
3	1 2	mpan	⊢ ( 𝑈 : ℋ ⟶ ℋ → ( - 1 ·op 𝑈 ) : ℋ ⟶ ℋ )
4		honegsub	⊢ ( ( 𝑇 : ℋ ⟶ ℋ ∧ ( - 1 ·op 𝑈 ) : ℋ ⟶ ℋ ) → ( 𝑇 +op ( - 1 ·op ( - 1 ·op 𝑈 ) ) ) = ( 𝑇 −op ( - 1 ·op 𝑈 ) ) )
5	3 4	sylan2	⊢ ( ( 𝑇 : ℋ ⟶ ℋ ∧ 𝑈 : ℋ ⟶ ℋ ) → ( 𝑇 +op ( - 1 ·op ( - 1 ·op 𝑈 ) ) ) = ( 𝑇 −op ( - 1 ·op 𝑈 ) ) )
6		honegneg	⊢ ( 𝑈 : ℋ ⟶ ℋ → ( - 1 ·op ( - 1 ·op 𝑈 ) ) = 𝑈 )
7	6	oveq2d	⊢ ( 𝑈 : ℋ ⟶ ℋ → ( 𝑇 +op ( - 1 ·op ( - 1 ·op 𝑈 ) ) ) = ( 𝑇 +op 𝑈 ) )
8	7	adantl	⊢ ( ( 𝑇 : ℋ ⟶ ℋ ∧ 𝑈 : ℋ ⟶ ℋ ) → ( 𝑇 +op ( - 1 ·op ( - 1 ·op 𝑈 ) ) ) = ( 𝑇 +op 𝑈 ) )
9	5 8	eqtr3d	⊢ ( ( 𝑇 : ℋ ⟶ ℋ ∧ 𝑈 : ℋ ⟶ ℋ ) → ( 𝑇 −op ( - 1 ·op 𝑈 ) ) = ( 𝑇 +op 𝑈 ) )