Metamath Proof Explorer

Theorem mulsub2

Description: Swap the order of subtraction in a multiplication. (Contributed by Scott Fenton, 24-Jun-2013)

Ref Expression
Assertion mulsub2 ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ ) ) → ( ( 𝐴 − 𝐵 ) · ( 𝐶 − 𝐷 ) ) = ( ( 𝐵 − 𝐴 ) · ( 𝐷 − 𝐶 ) ) )

Proof

Step Hyp Ref Expression
1 subcl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝐴 − 𝐵 ) ∈ ℂ )
2 subcl ⊢ ( ( 𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ ) → ( 𝐶 − 𝐷 ) ∈ ℂ )
3 mul2neg ⊢ ( ( ( 𝐴 − 𝐵 ) ∈ ℂ ∧ ( 𝐶 − 𝐷 ) ∈ ℂ ) → ( - ( 𝐴 − 𝐵 ) · - ( 𝐶 − 𝐷 ) ) = ( ( 𝐴 − 𝐵 ) · ( 𝐶 − 𝐷 ) ) )
4 1 2 3 syl2an ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ ) ) → ( - ( 𝐴 − 𝐵 ) · - ( 𝐶 − 𝐷 ) ) = ( ( 𝐴 − 𝐵 ) · ( 𝐶 − 𝐷 ) ) )
5 negsubdi2 ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → - ( 𝐴 − 𝐵 ) = ( 𝐵 − 𝐴 ) )
6 negsubdi2 ⊢ ( ( 𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ ) → - ( 𝐶 − 𝐷 ) = ( 𝐷 − 𝐶 ) )
7 5 6 oveqan12d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ ) ) → ( - ( 𝐴 − 𝐵 ) · - ( 𝐶 − 𝐷 ) ) = ( ( 𝐵 − 𝐴 ) · ( 𝐷 − 𝐶 ) ) )
8 4 7 eqtr3d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ ) ) → ( ( 𝐴 − 𝐵 ) · ( 𝐶 − 𝐷 ) ) = ( ( 𝐵 − 𝐴 ) · ( 𝐷 − 𝐶 ) ) )