This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem subeqrev

Description: Reverse the order of subtraction in an equality. (Contributed by Scott Fenton, 8-Jul-2013)

Ref Expression
Assertion subeqrev ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ ) ) → ( ( 𝐴 − 𝐵 ) = ( 𝐶 − 𝐷 ) ↔ ( 𝐵 − 𝐴 ) = ( 𝐷 − 𝐶 ) ) )

Proof

Step Hyp Ref Expression
1 subcl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝐴 − 𝐵 ) ∈ ℂ )
2 subcl ⊢ ( ( 𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ ) → ( 𝐶 − 𝐷 ) ∈ ℂ )
3 neg11 ⊢ ( ( ( 𝐴 − 𝐵 ) ∈ ℂ ∧ ( 𝐶 − 𝐷 ) ∈ ℂ ) → ( - ( 𝐴 − 𝐵 ) = - ( 𝐶 − 𝐷 ) ↔ ( 𝐴 − 𝐵 ) = ( 𝐶 − 𝐷 ) ) )
4 1 2 3 syl2an ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ ) ) → ( - ( 𝐴 − 𝐵 ) = - ( 𝐶 − 𝐷 ) ↔ ( 𝐴 − 𝐵 ) = ( 𝐶 − 𝐷 ) ) )
5 negsubdi2 ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → - ( 𝐴 − 𝐵 ) = ( 𝐵 − 𝐴 ) )
6 negsubdi2 ⊢ ( ( 𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ ) → - ( 𝐶 − 𝐷 ) = ( 𝐷 − 𝐶 ) )
7 5 6 eqeqan12d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ ) ) → ( - ( 𝐴 − 𝐵 ) = - ( 𝐶 − 𝐷 ) ↔ ( 𝐵 − 𝐴 ) = ( 𝐷 − 𝐶 ) ) )
8 4 7 bitr3d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ ) ) → ( ( 𝐴 − 𝐵 ) = ( 𝐶 − 𝐷 ) ↔ ( 𝐵 − 𝐴 ) = ( 𝐷 − 𝐶 ) ) )