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 ⊢ 𝐺 = ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( ℑ ‘ ( ( ∗ ‘ 𝑥 ) · 𝑦 ) ) )
Assertion sigarperm ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( ( 𝐴 − 𝐶 ) 𝐺 ( 𝐵 − 𝐶 ) ) = ( ( 𝐵 − 𝐴 ) 𝐺 ( 𝐶 − 𝐴 ) ) )

Proof

Step Hyp Ref Expression
1 sigar ⊢ 𝐺 = ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( ℑ ‘ ( ( ∗ ‘ 𝑥 ) · 𝑦 ) ) )
2 simp2 ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → 𝐵 ∈ ℂ )
3 simp3 ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → 𝐶 ∈ ℂ )
4 1 sigarim ⊢ ( ( 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( 𝐵 𝐺 𝐶 ) ∈ ℝ )
5 4 recnd ⊢ ( ( 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( 𝐵 𝐺 𝐶 ) ∈ ℂ )
6 2 3 5 syl2anc ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( 𝐵 𝐺 𝐶 ) ∈ ℂ )
7 simp1 ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → 𝐴 ∈ ℂ )
8 1 sigarim ⊢ ( ( 𝐵 ∈ ℂ ∧ 𝐴 ∈ ℂ ) → ( 𝐵 𝐺 𝐴 ) ∈ ℝ )
9 8 recnd ⊢ ( ( 𝐵 ∈ ℂ ∧ 𝐴 ∈ ℂ ) → ( 𝐵 𝐺 𝐴 ) ∈ ℂ )
10 2 7 9 syl2anc ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( 𝐵 𝐺 𝐴 ) ∈ ℂ )
11 6 10 negsubd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( ( 𝐵 𝐺 𝐶 ) + - ( 𝐵 𝐺 𝐴 ) ) = ( ( 𝐵 𝐺 𝐶 ) − ( 𝐵 𝐺 𝐴 ) ) )
12 1 sigarac ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝐴 𝐺 𝐵 ) = - ( 𝐵 𝐺 𝐴 ) )
13 7 2 12 syl2anc ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( 𝐴 𝐺 𝐵 ) = - ( 𝐵 𝐺 𝐴 ) )
14 13 eqcomd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → - ( 𝐵 𝐺 𝐴 ) = ( 𝐴 𝐺 𝐵 ) )
15 14 oveq2d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( ( 𝐵 𝐺 𝐶 ) + - ( 𝐵 𝐺 𝐴 ) ) = ( ( 𝐵 𝐺 𝐶 ) + ( 𝐴 𝐺 𝐵 ) ) )
16 11 15 eqtr3d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( ( 𝐵 𝐺 𝐶 ) − ( 𝐵 𝐺 𝐴 ) ) = ( ( 𝐵 𝐺 𝐶 ) + ( 𝐴 𝐺 𝐵 ) ) )
17 16 oveq1d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( ( ( 𝐵 𝐺 𝐶 ) − ( 𝐵 𝐺 𝐴 ) ) − ( 𝐴 𝐺 𝐶 ) ) = ( ( ( 𝐵 𝐺 𝐶 ) + ( 𝐴 𝐺 𝐵 ) ) − ( 𝐴 𝐺 𝐶 ) ) )
18 1 sigarexp ⊢ ( ( 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ∧ 𝐴 ∈ ℂ ) → ( ( 𝐵 − 𝐴 ) 𝐺 ( 𝐶 − 𝐴 ) ) = ( ( ( 𝐵 𝐺 𝐶 ) − ( 𝐵 𝐺 𝐴 ) ) − ( 𝐴 𝐺 𝐶 ) ) )
19 18 3comr ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( ( 𝐵 − 𝐴 ) 𝐺 ( 𝐶 − 𝐴 ) ) = ( ( ( 𝐵 𝐺 𝐶 ) − ( 𝐵 𝐺 𝐴 ) ) − ( 𝐴 𝐺 𝐶 ) ) )
20 1 sigarexp ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( ( 𝐴 − 𝐶 ) 𝐺 ( 𝐵 − 𝐶 ) ) = ( ( ( 𝐴 𝐺 𝐵 ) − ( 𝐴 𝐺 𝐶 ) ) − ( 𝐶 𝐺 𝐵 ) ) )
21 1 sigarim ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝐴 𝐺 𝐵 ) ∈ ℝ )
22 7 2 21 syl2anc ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( 𝐴 𝐺 𝐵 ) ∈ ℝ )
23 22 recnd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( 𝐴 𝐺 𝐵 ) ∈ ℂ )
24 1 sigarim ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( 𝐴 𝐺 𝐶 ) ∈ ℝ )
25 7 3 24 syl2anc ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( 𝐴 𝐺 𝐶 ) ∈ ℝ )
26 25 recnd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( 𝐴 𝐺 𝐶 ) ∈ ℂ )
27 1 sigarim ⊢ ( ( 𝐶 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝐶 𝐺 𝐵 ) ∈ ℝ )
28 3 2 27 syl2anc ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( 𝐶 𝐺 𝐵 ) ∈ ℝ )
29 28 recnd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( 𝐶 𝐺 𝐵 ) ∈ ℂ )
30 23 26 29 sub32d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( ( ( 𝐴 𝐺 𝐵 ) − ( 𝐴 𝐺 𝐶 ) ) − ( 𝐶 𝐺 𝐵 ) ) = ( ( ( 𝐴 𝐺 𝐵 ) − ( 𝐶 𝐺 𝐵 ) ) − ( 𝐴 𝐺 𝐶 ) ) )
31 6 23 addcomd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( ( 𝐵 𝐺 𝐶 ) + ( 𝐴 𝐺 𝐵 ) ) = ( ( 𝐴 𝐺 𝐵 ) + ( 𝐵 𝐺 𝐶 ) ) )
32 1 sigarac ⊢ ( ( 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( 𝐵 𝐺 𝐶 ) = - ( 𝐶 𝐺 𝐵 ) )
33 2 3 32 syl2anc ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( 𝐵 𝐺 𝐶 ) = - ( 𝐶 𝐺 𝐵 ) )
34 33 eqcomd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → - ( 𝐶 𝐺 𝐵 ) = ( 𝐵 𝐺 𝐶 ) )
35 34 oveq2d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( ( 𝐴 𝐺 𝐵 ) + - ( 𝐶 𝐺 𝐵 ) ) = ( ( 𝐴 𝐺 𝐵 ) + ( 𝐵 𝐺 𝐶 ) ) )
36 23 29 negsubd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( ( 𝐴 𝐺 𝐵 ) + - ( 𝐶 𝐺 𝐵 ) ) = ( ( 𝐴 𝐺 𝐵 ) − ( 𝐶 𝐺 𝐵 ) ) )
37 31 35 36 3eqtr2rd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( ( 𝐴 𝐺 𝐵 ) − ( 𝐶 𝐺 𝐵 ) ) = ( ( 𝐵 𝐺 𝐶 ) + ( 𝐴 𝐺 𝐵 ) ) )
38 37 oveq1d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( ( ( 𝐴 𝐺 𝐵 ) − ( 𝐶 𝐺 𝐵 ) ) − ( 𝐴 𝐺 𝐶 ) ) = ( ( ( 𝐵 𝐺 𝐶 ) + ( 𝐴 𝐺 𝐵 ) ) − ( 𝐴 𝐺 𝐶 ) ) )
39 20 30 38 3eqtrd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( ( 𝐴 − 𝐶 ) 𝐺 ( 𝐵 − 𝐶 ) ) = ( ( ( 𝐵 𝐺 𝐶 ) + ( 𝐴 𝐺 𝐵 ) ) − ( 𝐴 𝐺 𝐶 ) ) )
40 17 19 39 3eqtr4rd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( ( 𝐴 − 𝐶 ) 𝐺 ( 𝐵 − 𝐶 ) ) = ( ( 𝐵 − 𝐴 ) 𝐺 ( 𝐶 − 𝐴 ) ) )