Metamath Proof Explorer

Theorem sigarms

Description: Signed area is additive (with respect to subtraction) by the second argument. (Contributed by Saveliy Skresanov, 19-Sep-2017)

Ref Expression
Hypothesis sigar 
|- G = ( x e. CC , y e. CC |-> ( Im ` ( ( * ` x ) x. y ) ) )
Assertion sigarms 
|- ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( A G ( B - C ) ) = ( ( A G B ) - ( A G C ) ) )

Proof

Step Hyp Ref Expression
1 sigar 
 |-  G = ( x e. CC , y e. CC |-> ( Im ` ( ( * ` x ) x. y ) ) )
2 simp1 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> A e. CC )
3 simp2 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> B e. CC )
4 simp3 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> C e. CC )
5 3 4 subcld 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( B - C ) e. CC )
6 1 sigarac 
 |-  ( ( A e. CC /\ ( B - C ) e. CC ) -> ( A G ( B - C ) ) = -u ( ( B - C ) G A ) )
7 2 5 6 syl2anc 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( A G ( B - C ) ) = -u ( ( B - C ) G A ) )
8 1 sigarmf 
 |-  ( ( B e. CC /\ A e. CC /\ C e. CC ) -> ( ( B - C ) G A ) = ( ( B G A ) - ( C G A ) ) )
9 8 negeqd 
 |-  ( ( B e. CC /\ A e. CC /\ C e. CC ) -> -u ( ( B - C ) G A ) = -u ( ( B G A ) - ( C G A ) ) )
10 9 3com12 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> -u ( ( B - C ) G A ) = -u ( ( B G A ) - ( C G A ) ) )
11 3simpa 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( A e. CC /\ B e. CC ) )
12 11 ancomd 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( B e. CC /\ A e. CC ) )
13 1 sigarim 
 |-  ( ( B e. CC /\ A e. CC ) -> ( B G A ) e. RR )
14 12 13 syl 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( B G A ) e. RR )
15 14 recnd 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( B G A ) e. CC )
16 3simpb 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( A e. CC /\ C e. CC ) )
17 16 ancomd 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( C e. CC /\ A e. CC ) )
18 1 sigarim 
 |-  ( ( C e. CC /\ A e. CC ) -> ( C G A ) e. RR )
19 17 18 syl 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( C G A ) e. RR )
20 19 recnd 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( C G A ) e. CC )
21 negsubdi 
 |-  ( ( ( B G A ) e. CC /\ ( C G A ) e. CC ) -> -u ( ( B G A ) - ( C G A ) ) = ( -u ( B G A ) + ( C G A ) ) )
22 simpl 
 |-  ( ( ( B G A ) e. CC /\ ( C G A ) e. CC ) -> ( B G A ) e. CC )
23 22 negcld 
 |-  ( ( ( B G A ) e. CC /\ ( C G A ) e. CC ) -> -u ( B G A ) e. CC )
24 simpr 
 |-  ( ( ( B G A ) e. CC /\ ( C G A ) e. CC ) -> ( C G A ) e. CC )
25 23 24 subnegd 
 |-  ( ( ( B G A ) e. CC /\ ( C G A ) e. CC ) -> ( -u ( B G A ) - -u ( C G A ) ) = ( -u ( B G A ) + ( C G A ) ) )
26 21 25 eqtr4d 
 |-  ( ( ( B G A ) e. CC /\ ( C G A ) e. CC ) -> -u ( ( B G A ) - ( C G A ) ) = ( -u ( B G A ) - -u ( C G A ) ) )
27 15 20 26 syl2anc 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> -u ( ( B G A ) - ( C G A ) ) = ( -u ( B G A ) - -u ( C G A ) ) )
28 10 27 eqtrd 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> -u ( ( B - C ) G A ) = ( -u ( B G A ) - -u ( C G A ) ) )
29 1 sigarac 
 |-  ( ( A e. CC /\ B e. CC ) -> ( A G B ) = -u ( B G A ) )
30 2 3 29 syl2anc 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( A G B ) = -u ( B G A ) )
31 30 eqcomd 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> -u ( B G A ) = ( A G B ) )
32 1 sigarac 
 |-  ( ( A e. CC /\ C e. CC ) -> ( A G C ) = -u ( C G A ) )
33 2 4 32 syl2anc 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( A G C ) = -u ( C G A ) )
34 33 eqcomd 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> -u ( C G A ) = ( A G C ) )
35 31 34 oveq12d 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( -u ( B G A ) - -u ( C G A ) ) = ( ( A G B ) - ( A G C ) ) )
36 7 28 35 3eqtrd 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( A G ( B - C ) ) = ( ( A G B ) - ( A G C ) ) )