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−CGB−C=B−AGC−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∈ℂ→BGC∈ℝ
5 4 recnd ⊢B∈ℂ∧C∈ℂ→BGC∈ℂ
6 2 3 5 syl2anc ⊢A∈ℂ∧B∈ℂ∧C∈ℂ→BGC∈ℂ
7 simp1 ⊢A∈ℂ∧B∈ℂ∧C∈ℂ→A∈ℂ
8 1 sigarim ⊢B∈ℂ∧A∈ℂ→BGA∈ℝ
9 8 recnd ⊢B∈ℂ∧A∈ℂ→BGA∈ℂ
10 2 7 9 syl2anc ⊢A∈ℂ∧B∈ℂ∧C∈ℂ→BGA∈ℂ
11 6 10 negsubd ⊢A∈ℂ∧B∈ℂ∧C∈ℂ→BGC+−BGA=BGC−BGA
12 1 sigarac ⊢A∈ℂ∧B∈ℂ→AGB=−BGA
13 7 2 12 syl2anc ⊢A∈ℂ∧B∈ℂ∧C∈ℂ→AGB=−BGA
14 13 eqcomd ⊢A∈ℂ∧B∈ℂ∧C∈ℂ→−BGA=AGB
15 14 oveq2d ⊢A∈ℂ∧B∈ℂ∧C∈ℂ→BGC+−BGA=BGC+AGB
16 11 15 eqtr3d ⊢A∈ℂ∧B∈ℂ∧C∈ℂ→BGC−BGA=BGC+AGB
17 16 oveq1d ⊢A∈ℂ∧B∈ℂ∧C∈ℂ→BGC-BGA-AGC=BGC+AGB-AGC
18 1 sigarexp ⊢B∈ℂ∧C∈ℂ∧A∈ℂ→B−AGC−A=BGC-BGA-AGC
19 18 3comr ⊢A∈ℂ∧B∈ℂ∧C∈ℂ→B−AGC−A=BGC-BGA-AGC
20 1 sigarexp ⊢A∈ℂ∧B∈ℂ∧C∈ℂ→A−CGB−C=AGB-AGC-CGB
21 1 sigarim ⊢A∈ℂ∧B∈ℂ→AGB∈ℝ
22 7 2 21 syl2anc ⊢A∈ℂ∧B∈ℂ∧C∈ℂ→AGB∈ℝ
23 22 recnd ⊢A∈ℂ∧B∈ℂ∧C∈ℂ→AGB∈ℂ
24 1 sigarim ⊢A∈ℂ∧C∈ℂ→AGC∈ℝ
25 7 3 24 syl2anc ⊢A∈ℂ∧B∈ℂ∧C∈ℂ→AGC∈ℝ
26 25 recnd ⊢A∈ℂ∧B∈ℂ∧C∈ℂ→AGC∈ℂ
27 1 sigarim ⊢C∈ℂ∧B∈ℂ→CGB∈ℝ
28 3 2 27 syl2anc ⊢A∈ℂ∧B∈ℂ∧C∈ℂ→CGB∈ℝ
29 28 recnd ⊢A∈ℂ∧B∈ℂ∧C∈ℂ→CGB∈ℂ
30 23 26 29 sub32d ⊢A∈ℂ∧B∈ℂ∧C∈ℂ→AGB-AGC-CGB=AGB-CGB-AGC
31 6 23 addcomd ⊢A∈ℂ∧B∈ℂ∧C∈ℂ→BGC+AGB=AGB+BGC
32 1 sigarac ⊢B∈ℂ∧C∈ℂ→BGC=−CGB
33 2 3 32 syl2anc ⊢A∈ℂ∧B∈ℂ∧C∈ℂ→BGC=−CGB
34 33 eqcomd ⊢A∈ℂ∧B∈ℂ∧C∈ℂ→−CGB=BGC
35 34 oveq2d ⊢A∈ℂ∧B∈ℂ∧C∈ℂ→AGB+−CGB=AGB+BGC
36 23 29 negsubd ⊢A∈ℂ∧B∈ℂ∧C∈ℂ→AGB+−CGB=AGB−CGB
37 31 35 36 3eqtr2rd ⊢A∈ℂ∧B∈ℂ∧C∈ℂ→AGB−CGB=BGC+AGB
38 37 oveq1d ⊢A∈ℂ∧B∈ℂ∧C∈ℂ→AGB-CGB-AGC=BGC+AGB-AGC
39 20 30 38 3eqtrd ⊢A∈ℂ∧B∈ℂ∧C∈ℂ→A−CGB−C=BGC+AGB-AGC
40 17 19 39 3eqtr4rd ⊢A∈ℂ∧B∈ℂ∧C∈ℂ→A−CGB−C=B−AGC−A