Metamath Proof Explorer

Theorem sigariz

Description: If signed area is zero, the signed area with swapped arguments is also zero. Deduction version. (Contributed by Saveliy Skresanov, 23-Sep-2017)

Ref Expression
Hypotheses sigarimcd.sigar ⊢ G = x ∈ ℂ , y ∈ ℂ ⟼ ℑ ⁡ x ‾ ⁢ y
sigarimcd.a ⊢ φ → A ∈ ℂ ∧ B ∈ ℂ
sigariz.a ⊢ φ → A G B = 0
Assertion sigariz ⊢ φ → B G A = 0

Proof

Step Hyp Ref Expression
1 sigarimcd.sigar ⊢ G = x ∈ ℂ , y ∈ ℂ ⟼ ℑ ⁡ x ‾ ⁢ y
2 sigarimcd.a ⊢ φ → A ∈ ℂ ∧ B ∈ ℂ
3 sigariz.a ⊢ φ → A G B = 0
4 1 sigarac ⊢ A ∈ ℂ ∧ B ∈ ℂ → A G B = − B G A
5 2 4 syl ⊢ φ → A G B = − B G A
6 3 5 eqtr3d ⊢ φ → 0 = − B G A
7 6 negeqd ⊢ φ → − 0 = − − B G A
8 neg0 ⊢ − 0 = 0
9 8 a1i ⊢ φ → − 0 = 0
10 2 ancomd ⊢ φ → B ∈ ℂ ∧ A ∈ ℂ
11 1 10 sigarimcd ⊢ φ → B G A ∈ ℂ
12 11 negnegd ⊢ φ → − − B G A = B G A
13 7 9 12 3eqtr3rd ⊢ φ → B G A = 0