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 ) ) )