Metamath Proof Explorer

Theorem sigarexp

Description: Expand the signed area formula by linearity. (Contributed by Saveliy Skresanov, 20-Sep-2017)

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

Proof

Step Hyp Ref Expression
1 sigar 
 |-  G = ( x e. CC , y e. CC |-> ( Im ` ( ( * ` x ) x. y ) ) )
2 simp2 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> B e. CC )
3 simp3 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> C e. CC )
4 2 3 subcld 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( B - C ) e. CC )
5 1 sigarmf 
 |-  ( ( A e. CC /\ ( B - C ) e. CC /\ C e. CC ) -> ( ( A - C ) G ( B - C ) ) = ( ( A G ( B - C ) ) - ( C G ( B - C ) ) ) )
6 4 5 syld3an2 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( A - C ) G ( B - C ) ) = ( ( A G ( B - C ) ) - ( C G ( B - C ) ) ) )
7 1 sigarms 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( A G ( B - C ) ) = ( ( A G B ) - ( A G C ) ) )
8 7 oveq1d 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( A G ( B - C ) ) - ( C G ( B - C ) ) ) = ( ( ( A G B ) - ( A G C ) ) - ( C G ( B - C ) ) ) )
9 1 sigarms 
 |-  ( ( C e. CC /\ B e. CC /\ C e. CC ) -> ( C G ( B - C ) ) = ( ( C G B ) - ( C G C ) ) )
10 3 9 syld3an1 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( C G ( B - C ) ) = ( ( C G B ) - ( C G C ) ) )
11 1 sigarid 
 |-  ( C e. CC -> ( C G C ) = 0 )
12 3 11 syl 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( C G C ) = 0 )
13 12 oveq2d 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( C G B ) - ( C G C ) ) = ( ( C G B ) - 0 ) )
14 1 sigarim 
 |-  ( ( C e. CC /\ B e. CC ) -> ( C G B ) e. RR )
15 14 recnd 
 |-  ( ( C e. CC /\ B e. CC ) -> ( C G B ) e. CC )
16 3 2 15 syl2anc 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( C G B ) e. CC )
17 16 subid1d 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( C G B ) - 0 ) = ( C G B ) )
18 10 13 17 3eqtrd 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( C G ( B - C ) ) = ( C G B ) )
19 18 oveq2d 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( ( A G B ) - ( A G C ) ) - ( C G ( B - C ) ) ) = ( ( ( A G B ) - ( A G C ) ) - ( C G B ) ) )
20 6 8 19 3eqtrd 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( A - C ) G ( B - C ) ) = ( ( ( A G B ) - ( A G C ) ) - ( C G B ) ) )