Metamath Proof Explorer

Theorem sigaras

Description: Signed area is additive 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 sigaras 
|- ( ( 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 addcld 
 |-  ( ( 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 sigaraf 
 |-  ( ( 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 15 20 negdid 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> -u ( ( B G A ) + ( C G A ) ) = ( -u ( B G A ) + -u ( C G A ) ) )
22 10 21 eqtrd 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> -u ( ( B + C ) G A ) = ( -u ( B G A ) + -u ( C G A ) ) )
23 1 sigarac 
 |-  ( ( A e. CC /\ B e. CC ) -> ( A G B ) = -u ( B G A ) )
24 2 3 23 syl2anc 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( A G B ) = -u ( B G A ) )
25 24 eqcomd 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> -u ( B G A ) = ( A G B ) )
26 1 sigarac 
 |-  ( ( A e. CC /\ C e. CC ) -> ( A G C ) = -u ( C G A ) )
27 2 4 26 syl2anc 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( A G C ) = -u ( C G A ) )
28 27 eqcomd 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> -u ( C G A ) = ( A G C ) )
29 25 28 oveq12d 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( -u ( B G A ) + -u ( C G A ) ) = ( ( A G B ) + ( A G C ) ) )
30 7 22 29 3eqtrd 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( A G ( B + C ) ) = ( ( A G B ) + ( A G C ) ) )