Metamath Proof Explorer

Theorem sigarperm

Description: Signed area ( A - C ) G ( B - C ) acts as a double area of a triangle A B C . Here we prove that cyclically permuting the vertices doesn't change the area. (Contributed by Saveliy Skresanov, 20-Sep-2017)

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

Proof

Step Hyp Ref Expression
1 sigar ⊢ G = x ∈ ℂ , y ∈ ℂ ⟼ ℑ ⁡ x ‾ ⁢ y
2 simp2 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → B ∈ ℂ
3 simp3 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → C ∈ ℂ
4 1 sigarim ⊢ B ∈ ℂ ∧ C ∈ ℂ → B G C ∈ ℝ
5 4 recnd ⊢ B ∈ ℂ ∧ C ∈ ℂ → B G C ∈ ℂ
6 2 3 5 syl2anc ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → B G C ∈ ℂ
7 simp1 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → A ∈ ℂ
8 1 sigarim ⊢ B ∈ ℂ ∧ A ∈ ℂ → B G A ∈ ℝ
9 8 recnd ⊢ B ∈ ℂ ∧ A ∈ ℂ → B G A ∈ ℂ
10 2 7 9 syl2anc ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → B G A ∈ ℂ
11 6 10 negsubd ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → B G C + − B G A = B G C − B G A
12 1 sigarac ⊢ A ∈ ℂ ∧ B ∈ ℂ → A G B = − B G A
13 7 2 12 syl2anc ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → A G B = − B G A
14 13 eqcomd ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → − B G A = A G B
15 14 oveq2d ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → B G C + − B G A = B G C + A G B
16 11 15 eqtr3d ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → B G C − B G A = B G C + A G B
17 16 oveq1d ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → B G C - B G A - A G C = B G C + A G B - A G C
18 1 sigarexp ⊢ B ∈ ℂ ∧ C ∈ ℂ ∧ A ∈ ℂ → B − A G C − A = B G C - B G A - A G C
19 18 3comr ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → B − A G C − A = B G C - B G A - A G C
20 1 sigarexp ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → A − C G B − C = A G B - A G C - C G B
21 1 sigarim ⊢ A ∈ ℂ ∧ B ∈ ℂ → A G B ∈ ℝ
22 7 2 21 syl2anc ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → A G B ∈ ℝ
23 22 recnd ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → A G B ∈ ℂ
24 1 sigarim ⊢ A ∈ ℂ ∧ C ∈ ℂ → A G C ∈ ℝ
25 7 3 24 syl2anc ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → A G C ∈ ℝ
26 25 recnd ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → A G C ∈ ℂ
27 1 sigarim ⊢ C ∈ ℂ ∧ B ∈ ℂ → C G B ∈ ℝ
28 3 2 27 syl2anc ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → C G B ∈ ℝ
29 28 recnd ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → C G B ∈ ℂ
30 23 26 29 sub32d ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → A G B - A G C - C G B = A G B - C G B - A G C
31 6 23 addcomd ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → B G C + A G B = A G B + B G C
32 1 sigarac ⊢ B ∈ ℂ ∧ C ∈ ℂ → B G C = − C G B
33 2 3 32 syl2anc ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → B G C = − C G B
34 33 eqcomd ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → − C G B = B G C
35 34 oveq2d ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → A G B + − C G B = A G B + B G C
36 23 29 negsubd ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → A G B + − C G B = A G B − C G B
37 31 35 36 3eqtr2rd ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → A G B − C G B = B G C + A G B
38 37 oveq1d ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → A G B - C G B - A G C = B G C + A G B - A G C
39 20 30 38 3eqtrd ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → A − C G B − C = B G C + A G B - A G C
40 17 19 39 3eqtr4rd ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → A − C G B − C = B − A G C − A