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 e. CC , y e. CC |-> ( Im ` ( ( * ` x ) x. y ) ) )
Assertion sigarperm 
|- ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( A - C ) G ( B - C ) ) = ( ( B - A ) G ( C - A ) ) )

Proof

Step Hyp Ref Expression
1 sigar 
 |-  G = ( x e. CC , y e. CC |-> ( Im ` ( ( * ` x ) x. y ) ) )
2 simp2 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> B e. CC )
3 simp3 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> C e. CC )
4 1 sigarim 
 |-  ( ( B e. CC /\ C e. CC ) -> ( B G C ) e. RR )
5 4 recnd 
 |-  ( ( B e. CC /\ C e. CC ) -> ( B G C ) e. CC )
6 2 3 5 syl2anc 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( B G C ) e. CC )
7 simp1 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> A e. CC )
8 1 sigarim 
 |-  ( ( B e. CC /\ A e. CC ) -> ( B G A ) e. RR )
9 8 recnd 
 |-  ( ( B e. CC /\ A e. CC ) -> ( B G A ) e. CC )
10 2 7 9 syl2anc 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( B G A ) e. CC )
11 6 10 negsubd 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( B G C ) + -u ( B G A ) ) = ( ( B G C ) - ( B G A ) ) )
12 1 sigarac 
 |-  ( ( A e. CC /\ B e. CC ) -> ( A G B ) = -u ( B G A ) )
13 7 2 12 syl2anc 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( A G B ) = -u ( B G A ) )
14 13 eqcomd 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> -u ( B G A ) = ( A G B ) )
15 14 oveq2d 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( B G C ) + -u ( B G A ) ) = ( ( B G C ) + ( A G B ) ) )
16 11 15 eqtr3d 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( B G C ) - ( B G A ) ) = ( ( B G C ) + ( A G B ) ) )
17 16 oveq1d 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( ( B G C ) - ( B G A ) ) - ( A G C ) ) = ( ( ( B G C ) + ( A G B ) ) - ( A G C ) ) )
18 1 sigarexp 
 |-  ( ( B e. CC /\ C e. CC /\ A e. CC ) -> ( ( B - A ) G ( C - A ) ) = ( ( ( B G C ) - ( B G A ) ) - ( A G C ) ) )
19 18 3comr 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( B - A ) G ( C - A ) ) = ( ( ( B G C ) - ( B G A ) ) - ( A G C ) ) )
20 1 sigarexp 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( A - C ) G ( B - C ) ) = ( ( ( A G B ) - ( A G C ) ) - ( C G B ) ) )
21 1 sigarim 
 |-  ( ( A e. CC /\ B e. CC ) -> ( A G B ) e. RR )
22 7 2 21 syl2anc 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( A G B ) e. RR )
23 22 recnd 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( A G B ) e. CC )
24 1 sigarim 
 |-  ( ( A e. CC /\ C e. CC ) -> ( A G C ) e. RR )
25 7 3 24 syl2anc 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( A G C ) e. RR )
26 25 recnd 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( A G C ) e. CC )
27 1 sigarim 
 |-  ( ( C e. CC /\ B e. CC ) -> ( C G B ) e. RR )
28 3 2 27 syl2anc 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( C G B ) e. RR )
29 28 recnd 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( C G B ) e. CC )
30 23 26 29 sub32d 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( ( A G B ) - ( A G C ) ) - ( C G B ) ) = ( ( ( A G B ) - ( C G B ) ) - ( A G C ) ) )
31 6 23 addcomd 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( B G C ) + ( A G B ) ) = ( ( A G B ) + ( B G C ) ) )
32 1 sigarac 
 |-  ( ( B e. CC /\ C e. CC ) -> ( B G C ) = -u ( C G B ) )
33 2 3 32 syl2anc 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( B G C ) = -u ( C G B ) )
34 33 eqcomd 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> -u ( C G B ) = ( B G C ) )
35 34 oveq2d 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( A G B ) + -u ( C G B ) ) = ( ( A G B ) + ( B G C ) ) )
36 23 29 negsubd 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( A G B ) + -u ( C G B ) ) = ( ( A G B ) - ( C G B ) ) )
37 31 35 36 3eqtr2rd 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( A G B ) - ( C G B ) ) = ( ( B G C ) + ( A G B ) ) )
38 37 oveq1d 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( ( A G B ) - ( C G B ) ) - ( A G C ) ) = ( ( ( B G C ) + ( A G B ) ) - ( A G C ) ) )
39 20 30 38 3eqtrd 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( A - C ) G ( B - C ) ) = ( ( ( B G C ) + ( A G B ) ) - ( A G C ) ) )
40 17 19 39 3eqtr4rd 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( A - C ) G ( B - C ) ) = ( ( B - A ) G ( C - A ) ) )