Metamath Proof Explorer

Theorem sigarac

Description: Signed area is anticommutative. (Contributed by Saveliy Skresanov, 19-Sep-2017)

Ref Expression
Hypothesis sigar ⊢ G = x ∈ ℂ , y ∈ ℂ ⟼ ℑ ⁡ x ‾ ⁢ y
Assertion sigarac ⊢ A ∈ ℂ ∧ B ∈ ℂ → A G B = − B G A

Proof

Step Hyp Ref Expression
1 sigar ⊢ G = x ∈ ℂ , y ∈ ℂ ⟼ ℑ ⁡ x ‾ ⁢ y
2 1 sigarval ⊢ A ∈ ℂ ∧ B ∈ ℂ → A G B = ℑ ⁡ A ‾ ⁢ B
3 cjcl ⊢ B ∈ ℂ → B ‾ ∈ ℂ
4 3 adantl ⊢ A ∈ ℂ ∧ B ∈ ℂ → B ‾ ∈ ℂ
5 simpl ⊢ A ∈ ℂ ∧ B ∈ ℂ → A ∈ ℂ
6 4 5 cjmuld ⊢ A ∈ ℂ ∧ B ∈ ℂ → B ‾ ⁢ A ‾ = B ‾ ‾ ⁢ A ‾
7 simpr ⊢ A ∈ ℂ ∧ B ∈ ℂ → B ∈ ℂ
8 7 cjcjd ⊢ A ∈ ℂ ∧ B ∈ ℂ → B ‾ ‾ = B
9 8 oveq1d ⊢ A ∈ ℂ ∧ B ∈ ℂ → B ‾ ‾ ⁢ A ‾ = B ⁢ A ‾
10 5 cjcld ⊢ A ∈ ℂ ∧ B ∈ ℂ → A ‾ ∈ ℂ
11 7 10 mulcomd ⊢ A ∈ ℂ ∧ B ∈ ℂ → B ⁢ A ‾ = A ‾ ⁢ B
12 6 9 11 3eqtrrd ⊢ A ∈ ℂ ∧ B ∈ ℂ → A ‾ ⁢ B = B ‾ ⁢ A ‾
13 12 fveq2d ⊢ A ∈ ℂ ∧ B ∈ ℂ → ℑ ⁡ A ‾ ⁢ B = ℑ ⁡ B ‾ ⁢ A ‾
14 4 5 mulcld ⊢ A ∈ ℂ ∧ B ∈ ℂ → B ‾ ⁢ A ∈ ℂ
15 14 imcjd ⊢ A ∈ ℂ ∧ B ∈ ℂ → ℑ ⁡ B ‾ ⁢ A ‾ = − ℑ ⁡ B ‾ ⁢ A
16 2 13 15 3eqtrd ⊢ A ∈ ℂ ∧ B ∈ ℂ → A G B = − ℑ ⁡ B ‾ ⁢ A
17 1 sigarval ⊢ B ∈ ℂ ∧ A ∈ ℂ → B G A = ℑ ⁡ B ‾ ⁢ A
18 17 ancoms ⊢ A ∈ ℂ ∧ B ∈ ℂ → B G A = ℑ ⁡ B ‾ ⁢ A
19 18 negeqd ⊢ A ∈ ℂ ∧ B ∈ ℂ → − B G A = − ℑ ⁡ B ‾ ⁢ A
20 16 19 eqtr4d ⊢ A ∈ ℂ ∧ B ∈ ℂ → A G B = − B G A