Metamath Proof Explorer

Theorem sigaraf

Description: Signed area is additive by the first argument. (Contributed by Saveliy Skresanov, 19-Sep-2017)

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

Proof

Step Hyp Ref Expression
1 sigar 
 |-  G = ( x e. CC , y e. CC |-> ( Im ` ( ( * ` x ) x. y ) ) )
2 cjadd 
 |-  ( ( A e. CC /\ C e. CC ) -> ( * ` ( A + C ) ) = ( ( * ` A ) + ( * ` C ) ) )
3 2 oveq1d 
 |-  ( ( A e. CC /\ C e. CC ) -> ( ( * ` ( A + C ) ) x. B ) = ( ( ( * ` A ) + ( * ` C ) ) x. B ) )
4 3 3adant2 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( * ` ( A + C ) ) x. B ) = ( ( ( * ` A ) + ( * ` C ) ) x. B ) )
5 simp1 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> A e. CC )
6 5 cjcld 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( * ` A ) e. CC )
7 simp3 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> C e. CC )
8 7 cjcld 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( * ` C ) e. CC )
9 simp2 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> B e. CC )
10 6 8 9 adddird 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( ( * ` A ) + ( * ` C ) ) x. B ) = ( ( ( * ` A ) x. B ) + ( ( * ` C ) x. B ) ) )
11 4 10 eqtrd 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( * ` ( A + C ) ) x. B ) = ( ( ( * ` A ) x. B ) + ( ( * ` C ) x. B ) ) )
12 11 fveq2d 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( Im ` ( ( * ` ( A + C ) ) x. B ) ) = ( Im ` ( ( ( * ` A ) x. B ) + ( ( * ` C ) x. B ) ) ) )
13 6 9 mulcld 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( * ` A ) x. B ) e. CC )
14 8 9 mulcld 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( * ` C ) x. B ) e. CC )
15 13 14 imaddd 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( Im ` ( ( ( * ` A ) x. B ) + ( ( * ` C ) x. B ) ) ) = ( ( Im ` ( ( * ` A ) x. B ) ) + ( Im ` ( ( * ` C ) x. B ) ) ) )
16 12 15 eqtrd 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( Im ` ( ( * ` ( A + C ) ) x. B ) ) = ( ( Im ` ( ( * ` A ) x. B ) ) + ( Im ` ( ( * ` C ) x. B ) ) ) )
17 5 7 addcld 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( A + C ) e. CC )
18 1 sigarval 
 |-  ( ( ( A + C ) e. CC /\ B e. CC ) -> ( ( A + C ) G B ) = ( Im ` ( ( * ` ( A + C ) ) x. B ) ) )
19 17 9 18 syl2anc 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( A + C ) G B ) = ( Im ` ( ( * ` ( A + C ) ) x. B ) ) )
20 1 sigarval 
 |-  ( ( A e. CC /\ B e. CC ) -> ( A G B ) = ( Im ` ( ( * ` A ) x. B ) ) )
21 20 3adant3 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( A G B ) = ( Im ` ( ( * ` A ) x. B ) ) )
22 3simpc 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( B e. CC /\ C e. CC ) )
23 22 ancomd 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( C e. CC /\ B e. CC ) )
24 1 sigarval 
 |-  ( ( C e. CC /\ B e. CC ) -> ( C G B ) = ( Im ` ( ( * ` C ) x. B ) ) )
25 23 24 syl 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( C G B ) = ( Im ` ( ( * ` C ) x. B ) ) )
26 21 25 oveq12d 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( A G B ) + ( C G B ) ) = ( ( Im ` ( ( * ` A ) x. B ) ) + ( Im ` ( ( * ` C ) x. B ) ) ) )
27 16 19 26 3eqtr4d 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( A + C ) G B ) = ( ( A G B ) + ( C G B ) ) )