Metamath Proof Explorer

Theorem sigarmf

Description: Signed area is additive (with respect to subtraction) 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 sigarmf 
|- ( ( 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 cjsub 
 |-  ( ( 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 subdird 
 |-  ( ( 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 imsubd 
 |-  ( ( 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 subcld 
 |-  ( ( 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 ) ) )