Metamath Proof Explorer

Theorem sigaradd

Description: Subtracting (double) area of A D C from A B C yields the (double) area of D B C . (Contributed by Saveliy Skresanov, 23-Sep-2017)

Ref Expression
Hypotheses sharhght.sigar 
|- G = ( x e. CC , y e. CC |-> ( Im ` ( ( * ` x ) x. y ) ) )
sharhght.a 
|- ( ph -> ( A e. CC /\ B e. CC /\ C e. CC ) )
sharhght.b 
|- ( ph -> ( D e. CC /\ ( ( A - D ) G ( B - D ) ) = 0 ) )
Assertion sigaradd 
|- ( ph -> ( ( ( B - C ) G ( A - C ) ) - ( ( D - C ) G ( A - C ) ) ) = ( ( B - C ) G ( D - C ) ) )

Proof

Step Hyp Ref Expression
1 sharhght.sigar 
 |-  G = ( x e. CC , y e. CC |-> ( Im ` ( ( * ` x ) x. y ) ) )
2 sharhght.a 
 |-  ( ph -> ( A e. CC /\ B e. CC /\ C e. CC ) )
3 sharhght.b 
 |-  ( ph -> ( D e. CC /\ ( ( A - D ) G ( B - D ) ) = 0 ) )
4 2 simp1d 
 |-  ( ph -> A e. CC )
5 2 simp3d 
 |-  ( ph -> C e. CC )
6 3 simpld 
 |-  ( ph -> D e. CC )
7 4 5 6 nnncan1d 
 |-  ( ph -> ( ( A - C ) - ( A - D ) ) = ( D - C ) )
8 7 oveq2d 
 |-  ( ph -> ( ( B - D ) G ( ( A - C ) - ( A - D ) ) ) = ( ( B - D ) G ( D - C ) ) )
9 2 simp2d 
 |-  ( ph -> B e. CC )
10 9 6 subcld 
 |-  ( ph -> ( B - D ) e. CC )
11 4 5 subcld 
 |-  ( ph -> ( A - C ) e. CC )
12 4 6 subcld 
 |-  ( ph -> ( A - D ) e. CC )
13 1 sigarms 
 |-  ( ( ( B - D ) e. CC /\ ( A - C ) e. CC /\ ( A - D ) e. CC ) -> ( ( B - D ) G ( ( A - C ) - ( A - D ) ) ) = ( ( ( B - D ) G ( A - C ) ) - ( ( B - D ) G ( A - D ) ) ) )
14 10 11 12 13 syl3anc 
 |-  ( ph -> ( ( B - D ) G ( ( A - C ) - ( A - D ) ) ) = ( ( ( B - D ) G ( A - C ) ) - ( ( B - D ) G ( A - D ) ) ) )
15 8 14 eqtr3d 
 |-  ( ph -> ( ( B - D ) G ( D - C ) ) = ( ( ( B - D ) G ( A - C ) ) - ( ( B - D ) G ( A - D ) ) ) )
16 1 sigarac 
 |-  ( ( ( A - D ) e. CC /\ ( B - D ) e. CC ) -> ( ( A - D ) G ( B - D ) ) = -u ( ( B - D ) G ( A - D ) ) )
17 12 10 16 syl2anc 
 |-  ( ph -> ( ( A - D ) G ( B - D ) ) = -u ( ( B - D ) G ( A - D ) ) )
18 3 simprd 
 |-  ( ph -> ( ( A - D ) G ( B - D ) ) = 0 )
19 17 18 eqtr3d 
 |-  ( ph -> -u ( ( B - D ) G ( A - D ) ) = 0 )
20 19 negeqd 
 |-  ( ph -> -u -u ( ( B - D ) G ( A - D ) ) = -u 0 )
21 10 12 jca 
 |-  ( ph -> ( ( B - D ) e. CC /\ ( A - D ) e. CC ) )
22 1 21 sigarimcd 
 |-  ( ph -> ( ( B - D ) G ( A - D ) ) e. CC )
23 22 negnegd 
 |-  ( ph -> -u -u ( ( B - D ) G ( A - D ) ) = ( ( B - D ) G ( A - D ) ) )
24 neg0 
 |-  -u 0 = 0
25 24 a1i 
 |-  ( ph -> -u 0 = 0 )
26 20 23 25 3eqtr3d 
 |-  ( ph -> ( ( B - D ) G ( A - D ) ) = 0 )
27 26 oveq2d 
 |-  ( ph -> ( ( ( B - D ) G ( A - C ) ) - ( ( B - D ) G ( A - D ) ) ) = ( ( ( B - D ) G ( A - C ) ) - 0 ) )
28 10 11 jca 
 |-  ( ph -> ( ( B - D ) e. CC /\ ( A - C ) e. CC ) )
29 1 28 sigarimcd 
 |-  ( ph -> ( ( B - D ) G ( A - C ) ) e. CC )
30 29 subid1d 
 |-  ( ph -> ( ( ( B - D ) G ( A - C ) ) - 0 ) = ( ( B - D ) G ( A - C ) ) )
31 15 27 30 3eqtrd 
 |-  ( ph -> ( ( B - D ) G ( D - C ) ) = ( ( B - D ) G ( A - C ) ) )
32 9 6 5 nnncan2d 
 |-  ( ph -> ( ( B - C ) - ( D - C ) ) = ( B - D ) )
33 32 oveq1d 
 |-  ( ph -> ( ( ( B - C ) - ( D - C ) ) G ( A - C ) ) = ( ( B - D ) G ( A - C ) ) )
34 9 5 subcld 
 |-  ( ph -> ( B - C ) e. CC )
35 6 5 subcld 
 |-  ( ph -> ( D - C ) e. CC )
36 1 sigarmf 
 |-  ( ( ( B - C ) e. CC /\ ( A - C ) e. CC /\ ( D - C ) e. CC ) -> ( ( ( B - C ) - ( D - C ) ) G ( A - C ) ) = ( ( ( B - C ) G ( A - C ) ) - ( ( D - C ) G ( A - C ) ) ) )
37 34 11 35 36 syl3anc 
 |-  ( ph -> ( ( ( B - C ) - ( D - C ) ) G ( A - C ) ) = ( ( ( B - C ) G ( A - C ) ) - ( ( D - C ) G ( A - C ) ) ) )
38 31 33 37 3eqtr2rd 
 |-  ( ph -> ( ( ( B - C ) G ( A - C ) ) - ( ( D - C ) G ( A - C ) ) ) = ( ( B - D ) G ( D - C ) ) )
39 5 6 subcld 
 |-  ( ph -> ( C - D ) e. CC )
40 1red 
 |-  ( ph -> 1 e. RR )
41 40 renegcld 
 |-  ( ph -> -u 1 e. RR )
42 1 sigarls 
 |-  ( ( ( B - D ) e. CC /\ ( C - D ) e. CC /\ -u 1 e. RR ) -> ( ( B - D ) G ( ( C - D ) x. -u 1 ) ) = ( ( ( B - D ) G ( C - D ) ) x. -u 1 ) )
43 10 39 41 42 syl3anc 
 |-  ( ph -> ( ( B - D ) G ( ( C - D ) x. -u 1 ) ) = ( ( ( B - D ) G ( C - D ) ) x. -u 1 ) )
44 39 mulm1d 
 |-  ( ph -> ( -u 1 x. ( C - D ) ) = -u ( C - D ) )
45 1cnd 
 |-  ( ph -> 1 e. CC )
46 45 negcld 
 |-  ( ph -> -u 1 e. CC )
47 46 39 mulcomd 
 |-  ( ph -> ( -u 1 x. ( C - D ) ) = ( ( C - D ) x. -u 1 ) )
48 5 6 negsubdi2d 
 |-  ( ph -> -u ( C - D ) = ( D - C ) )
49 44 47 48 3eqtr3d 
 |-  ( ph -> ( ( C - D ) x. -u 1 ) = ( D - C ) )
50 49 oveq2d 
 |-  ( ph -> ( ( B - D ) G ( ( C - D ) x. -u 1 ) ) = ( ( B - D ) G ( D - C ) ) )
51 10 39 jca 
 |-  ( ph -> ( ( B - D ) e. CC /\ ( C - D ) e. CC ) )
52 1 51 sigarimcd 
 |-  ( ph -> ( ( B - D ) G ( C - D ) ) e. CC )
53 52 mulm1d 
 |-  ( ph -> ( -u 1 x. ( ( B - D ) G ( C - D ) ) ) = -u ( ( B - D ) G ( C - D ) ) )
54 52 46 mulcomd 
 |-  ( ph -> ( ( ( B - D ) G ( C - D ) ) x. -u 1 ) = ( -u 1 x. ( ( B - D ) G ( C - D ) ) ) )
55 1 sigarac 
 |-  ( ( ( C - D ) e. CC /\ ( B - D ) e. CC ) -> ( ( C - D ) G ( B - D ) ) = -u ( ( B - D ) G ( C - D ) ) )
56 39 10 55 syl2anc 
 |-  ( ph -> ( ( C - D ) G ( B - D ) ) = -u ( ( B - D ) G ( C - D ) ) )
57 53 54 56 3eqtr4d 
 |-  ( ph -> ( ( ( B - D ) G ( C - D ) ) x. -u 1 ) = ( ( C - D ) G ( B - D ) ) )
58 43 50 57 3eqtr3d 
 |-  ( ph -> ( ( B - D ) G ( D - C ) ) = ( ( C - D ) G ( B - D ) ) )
59 1 sigarperm 
 |-  ( ( C e. CC /\ B e. CC /\ D e. CC ) -> ( ( C - D ) G ( B - D ) ) = ( ( B - C ) G ( D - C ) ) )
60 5 9 6 59 syl3anc 
 |-  ( ph -> ( ( C - D ) G ( B - D ) ) = ( ( B - C ) G ( D - C ) ) )
61 38 58 60 3eqtrd 
 |-  ( ph -> ( ( ( B - C ) G ( A - C ) ) - ( ( D - C ) G ( A - C ) ) ) = ( ( B - C ) G ( D - C ) ) )