Metamath Proof Explorer

Theorem honegsubdi

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

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

Proof

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