Theorem honegdi

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

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

Proof

Step	Hyp	Ref	Expression
1		neg1cn	⊢ - 1 ∈ ℂ
2		hoadddi	⊢ ( ( - 1 ∈ ℂ ∧ 𝑇 : ℋ ⟶ ℋ ∧ 𝑈 : ℋ ⟶ ℋ ) → ( - 1 ·op ( 𝑇 +op 𝑈 ) ) = ( ( - 1 ·op 𝑇 ) +op ( - 1 ·op 𝑈 ) ) )
3	1 2	mp3an1	⊢ ( ( 𝑇 : ℋ ⟶ ℋ ∧ 𝑈 : ℋ ⟶ ℋ ) → ( - 1 ·op ( 𝑇 +op 𝑈 ) ) = ( ( - 1 ·op 𝑇 ) +op ( - 1 ·op 𝑈 ) ) )