Theorem honegsubdi2

Description: Distribution of negative over subtraction. (Contributed by NM, 24-Aug-2006) (New usage is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		honegsubdi	⊢ ( ( 𝑇 : ℋ ⟶ ℋ ∧ 𝑈 : ℋ ⟶ ℋ ) → ( - 1 ·op ( 𝑇 −op 𝑈 ) ) = ( ( - 1 ·op 𝑇 ) +op 𝑈 ) )
2		neg1cn	⊢ - 1 ∈ ℂ
3		homulcl	⊢ ( ( - 1 ∈ ℂ ∧ 𝑇 : ℋ ⟶ ℋ ) → ( - 1 ·op 𝑇 ) : ℋ ⟶ ℋ )
4	2 3	mpan	⊢ ( 𝑇 : ℋ ⟶ ℋ → ( - 1 ·op 𝑇 ) : ℋ ⟶ ℋ )
5		hoaddcom	⊢ ( ( ( - 1 ·op 𝑇 ) : ℋ ⟶ ℋ ∧ 𝑈 : ℋ ⟶ ℋ ) → ( ( - 1 ·op 𝑇 ) +op 𝑈 ) = ( 𝑈 +op ( - 1 ·op 𝑇 ) ) )
6	4 5	sylan	⊢ ( ( 𝑇 : ℋ ⟶ ℋ ∧ 𝑈 : ℋ ⟶ ℋ ) → ( ( - 1 ·op 𝑇 ) +op 𝑈 ) = ( 𝑈 +op ( - 1 ·op 𝑇 ) ) )
7		honegsub	⊢ ( ( 𝑈 : ℋ ⟶ ℋ ∧ 𝑇 : ℋ ⟶ ℋ ) → ( 𝑈 +op ( - 1 ·op 𝑇 ) ) = ( 𝑈 −op 𝑇 ) )
8	7	ancoms	⊢ ( ( 𝑇 : ℋ ⟶ ℋ ∧ 𝑈 : ℋ ⟶ ℋ ) → ( 𝑈 +op ( - 1 ·op 𝑇 ) ) = ( 𝑈 −op 𝑇 ) )
9	1 6 8	3eqtrd	⊢ ( ( 𝑇 : ℋ ⟶ ℋ ∧ 𝑈 : ℋ ⟶ ℋ ) → ( - 1 ·op ( 𝑇 −op 𝑈 ) ) = ( 𝑈 −op 𝑇 ) )