Metamath Proof Explorer

Theorem cevathlem2

Description: Ceva's theorem second lemma. Relate (doubled) areas of triangles C A O and A B O with of segments B D and D C . (Contributed by Saveliy Skresanov, 24-Sep-2017)

Ref Expression
Hypotheses cevath.sigar 
|- G = ( x e. CC , y e. CC |-> ( Im ` ( ( * ` x ) x. y ) ) )
cevath.a 
|- ( ph -> ( A e. CC /\ B e. CC /\ C e. CC ) )
cevath.b 
|- ( ph -> ( F e. CC /\ D e. CC /\ E e. CC ) )
cevath.c 
|- ( ph -> O e. CC )
cevath.d 
|- ( ph -> ( ( ( A - O ) G ( D - O ) ) = 0 /\ ( ( B - O ) G ( E - O ) ) = 0 /\ ( ( C - O ) G ( F - O ) ) = 0 ) )
cevath.e 
|- ( ph -> ( ( ( A - F ) G ( B - F ) ) = 0 /\ ( ( B - D ) G ( C - D ) ) = 0 /\ ( ( C - E ) G ( A - E ) ) = 0 ) )
cevath.f 
|- ( ph -> ( ( ( A - O ) G ( B - O ) ) =/= 0 /\ ( ( B - O ) G ( C - O ) ) =/= 0 /\ ( ( C - O ) G ( A - O ) ) =/= 0 ) )
Assertion cevathlem2 
|- ( ph -> ( ( ( C - O ) G ( A - O ) ) x. ( B - D ) ) = ( ( ( A - O ) G ( B - O ) ) x. ( D - C ) ) )

Proof

Step Hyp Ref Expression
1 cevath.sigar 
 |-  G = ( x e. CC , y e. CC |-> ( Im ` ( ( * ` x ) x. y ) ) )
2 cevath.a 
 |-  ( ph -> ( A e. CC /\ B e. CC /\ C e. CC ) )
3 cevath.b 
 |-  ( ph -> ( F e. CC /\ D e. CC /\ E e. CC ) )
4 cevath.c 
 |-  ( ph -> O e. CC )
5 cevath.d 
 |-  ( ph -> ( ( ( A - O ) G ( D - O ) ) = 0 /\ ( ( B - O ) G ( E - O ) ) = 0 /\ ( ( C - O ) G ( F - O ) ) = 0 ) )
6 cevath.e 
 |-  ( ph -> ( ( ( A - F ) G ( B - F ) ) = 0 /\ ( ( B - D ) G ( C - D ) ) = 0 /\ ( ( C - E ) G ( A - E ) ) = 0 ) )
7 cevath.f 
 |-  ( ph -> ( ( ( A - O ) G ( B - O ) ) =/= 0 /\ ( ( B - O ) G ( C - O ) ) =/= 0 /\ ( ( C - O ) G ( A - O ) ) =/= 0 ) )
8 3 simp2d 
 |-  ( ph -> D e. CC )
9 2 simp1d 
 |-  ( ph -> A e. CC )
10 2 simp2d 
 |-  ( ph -> B e. CC )
11 8 9 10 3jca 
 |-  ( ph -> ( D e. CC /\ A e. CC /\ B e. CC ) )
12 9 4 subcld 
 |-  ( ph -> ( A - O ) e. CC )
13 8 4 subcld 
 |-  ( ph -> ( D - O ) e. CC )
14 12 13 jca 
 |-  ( ph -> ( ( A - O ) e. CC /\ ( D - O ) e. CC ) )
15 5 simp1d 
 |-  ( ph -> ( ( A - O ) G ( D - O ) ) = 0 )
16 1 14 15 sigariz 
 |-  ( ph -> ( ( D - O ) G ( A - O ) ) = 0 )
17 4 16 jca 
 |-  ( ph -> ( O e. CC /\ ( ( D - O ) G ( A - O ) ) = 0 ) )
18 1 11 17 sigaradd 
 |-  ( ph -> ( ( ( A - B ) G ( D - B ) ) - ( ( O - B ) G ( D - B ) ) ) = ( ( A - B ) G ( O - B ) ) )
19 1 sigarperm 
 |-  ( ( B e. CC /\ A e. CC /\ O e. CC ) -> ( ( B - O ) G ( A - O ) ) = ( ( A - B ) G ( O - B ) ) )
20 10 9 4 19 syl3anc 
 |-  ( ph -> ( ( B - O ) G ( A - O ) ) = ( ( A - B ) G ( O - B ) ) )
21 18 20 eqtr4d 
 |-  ( ph -> ( ( ( A - B ) G ( D - B ) ) - ( ( O - B ) G ( D - B ) ) ) = ( ( B - O ) G ( A - O ) ) )
22 21 oveq1d 
 |-  ( ph -> ( ( ( ( A - B ) G ( D - B ) ) - ( ( O - B ) G ( D - B ) ) ) x. ( C - D ) ) = ( ( ( B - O ) G ( A - O ) ) x. ( C - D ) ) )
23 9 10 subcld 
 |-  ( ph -> ( A - B ) e. CC )
24 8 10 subcld 
 |-  ( ph -> ( D - B ) e. CC )
25 23 24 jca 
 |-  ( ph -> ( ( A - B ) e. CC /\ ( D - B ) e. CC ) )
26 1 25 sigarimcd 
 |-  ( ph -> ( ( A - B ) G ( D - B ) ) e. CC )
27 4 10 subcld 
 |-  ( ph -> ( O - B ) e. CC )
28 27 24 jca 
 |-  ( ph -> ( ( O - B ) e. CC /\ ( D - B ) e. CC ) )
29 1 28 sigarimcd 
 |-  ( ph -> ( ( O - B ) G ( D - B ) ) e. CC )
30 2 simp3d 
 |-  ( ph -> C e. CC )
31 30 8 subcld 
 |-  ( ph -> ( C - D ) e. CC )
32 26 29 31 subdird 
 |-  ( ph -> ( ( ( ( A - B ) G ( D - B ) ) - ( ( O - B ) G ( D - B ) ) ) x. ( C - D ) ) = ( ( ( ( A - B ) G ( D - B ) ) x. ( C - D ) ) - ( ( ( O - B ) G ( D - B ) ) x. ( C - D ) ) ) )
33 22 32 eqtr3d 
 |-  ( ph -> ( ( ( B - O ) G ( A - O ) ) x. ( C - D ) ) = ( ( ( ( A - B ) G ( D - B ) ) x. ( C - D ) ) - ( ( ( O - B ) G ( D - B ) ) x. ( C - D ) ) ) )
34 10 30 9 3jca 
 |-  ( ph -> ( B e. CC /\ C e. CC /\ A e. CC ) )
35 6 simp2d 
 |-  ( ph -> ( ( B - D ) G ( C - D ) ) = 0 )
36 8 35 jca 
 |-  ( ph -> ( D e. CC /\ ( ( B - D ) G ( C - D ) ) = 0 ) )
37 1 34 36 sharhght 
 |-  ( ph -> ( ( ( A - B ) G ( D - B ) ) x. ( C - D ) ) = ( ( ( A - C ) G ( D - C ) ) x. ( B - D ) ) )
38 10 30 4 3jca 
 |-  ( ph -> ( B e. CC /\ C e. CC /\ O e. CC ) )
39 1 38 36 sharhght 
 |-  ( ph -> ( ( ( O - B ) G ( D - B ) ) x. ( C - D ) ) = ( ( ( O - C ) G ( D - C ) ) x. ( B - D ) ) )
40 37 39 oveq12d 
 |-  ( ph -> ( ( ( ( A - B ) G ( D - B ) ) x. ( C - D ) ) - ( ( ( O - B ) G ( D - B ) ) x. ( C - D ) ) ) = ( ( ( ( A - C ) G ( D - C ) ) x. ( B - D ) ) - ( ( ( O - C ) G ( D - C ) ) x. ( B - D ) ) ) )
41 9 30 subcld 
 |-  ( ph -> ( A - C ) e. CC )
42 8 30 subcld 
 |-  ( ph -> ( D - C ) e. CC )
43 1 sigarim 
 |-  ( ( ( A - C ) e. CC /\ ( D - C ) e. CC ) -> ( ( A - C ) G ( D - C ) ) e. RR )
44 41 42 43 syl2anc 
 |-  ( ph -> ( ( A - C ) G ( D - C ) ) e. RR )
45 44 recnd 
 |-  ( ph -> ( ( A - C ) G ( D - C ) ) e. CC )
46 4 30 subcld 
 |-  ( ph -> ( O - C ) e. CC )
47 46 42 jca 
 |-  ( ph -> ( ( O - C ) e. CC /\ ( D - C ) e. CC ) )
48 1 47 sigarimcd 
 |-  ( ph -> ( ( O - C ) G ( D - C ) ) e. CC )
49 10 8 subcld 
 |-  ( ph -> ( B - D ) e. CC )
50 45 48 49 subdird 
 |-  ( ph -> ( ( ( ( A - C ) G ( D - C ) ) - ( ( O - C ) G ( D - C ) ) ) x. ( B - D ) ) = ( ( ( ( A - C ) G ( D - C ) ) x. ( B - D ) ) - ( ( ( O - C ) G ( D - C ) ) x. ( B - D ) ) ) )
51 8 9 30 3jca 
 |-  ( ph -> ( D e. CC /\ A e. CC /\ C e. CC ) )
52 1 51 17 sigaradd 
 |-  ( ph -> ( ( ( A - C ) G ( D - C ) ) - ( ( O - C ) G ( D - C ) ) ) = ( ( A - C ) G ( O - C ) ) )
53 1 sigarperm 
 |-  ( ( C e. CC /\ A e. CC /\ O e. CC ) -> ( ( C - O ) G ( A - O ) ) = ( ( A - C ) G ( O - C ) ) )
54 30 9 4 53 syl3anc 
 |-  ( ph -> ( ( C - O ) G ( A - O ) ) = ( ( A - C ) G ( O - C ) ) )
55 52 54 eqtr4d 
 |-  ( ph -> ( ( ( A - C ) G ( D - C ) ) - ( ( O - C ) G ( D - C ) ) ) = ( ( C - O ) G ( A - O ) ) )
56 55 oveq1d 
 |-  ( ph -> ( ( ( ( A - C ) G ( D - C ) ) - ( ( O - C ) G ( D - C ) ) ) x. ( B - D ) ) = ( ( ( C - O ) G ( A - O ) ) x. ( B - D ) ) )
57 50 56 eqtr3d 
 |-  ( ph -> ( ( ( ( A - C ) G ( D - C ) ) x. ( B - D ) ) - ( ( ( O - C ) G ( D - C ) ) x. ( B - D ) ) ) = ( ( ( C - O ) G ( A - O ) ) x. ( B - D ) ) )
58 33 40 57 3eqtrrd 
 |-  ( ph -> ( ( ( C - O ) G ( A - O ) ) x. ( B - D ) ) = ( ( ( B - O ) G ( A - O ) ) x. ( C - D ) ) )
59 10 4 subcld 
 |-  ( ph -> ( B - O ) e. CC )
60 1 sigarac 
 |-  ( ( ( B - O ) e. CC /\ ( A - O ) e. CC ) -> ( ( B - O ) G ( A - O ) ) = -u ( ( A - O ) G ( B - O ) ) )
61 59 12 60 syl2anc 
 |-  ( ph -> ( ( B - O ) G ( A - O ) ) = -u ( ( A - O ) G ( B - O ) ) )
62 61 oveq1d 
 |-  ( ph -> ( ( ( B - O ) G ( A - O ) ) x. ( C - D ) ) = ( -u ( ( A - O ) G ( B - O ) ) x. ( C - D ) ) )
63 12 59 jca 
 |-  ( ph -> ( ( A - O ) e. CC /\ ( B - O ) e. CC ) )
64 1 63 sigarimcd 
 |-  ( ph -> ( ( A - O ) G ( B - O ) ) e. CC )
65 mulneg12 
 |-  ( ( ( ( A - O ) G ( B - O ) ) e. CC /\ ( C - D ) e. CC ) -> ( -u ( ( A - O ) G ( B - O ) ) x. ( C - D ) ) = ( ( ( A - O ) G ( B - O ) ) x. -u ( C - D ) ) )
66 64 31 65 syl2anc 
 |-  ( ph -> ( -u ( ( A - O ) G ( B - O ) ) x. ( C - D ) ) = ( ( ( A - O ) G ( B - O ) ) x. -u ( C - D ) ) )
67 30 8 negsubdi2d 
 |-  ( ph -> -u ( C - D ) = ( D - C ) )
68 67 oveq2d 
 |-  ( ph -> ( ( ( A - O ) G ( B - O ) ) x. -u ( C - D ) ) = ( ( ( A - O ) G ( B - O ) ) x. ( D - C ) ) )
69 66 68 eqtrd 
 |-  ( ph -> ( -u ( ( A - O ) G ( B - O ) ) x. ( C - D ) ) = ( ( ( A - O ) G ( B - O ) ) x. ( D - C ) ) )
70 58 62 69 3eqtrd 
 |-  ( ph -> ( ( ( C - O ) G ( A - O ) ) x. ( B - D ) ) = ( ( ( A - O ) G ( B - O ) ) x. ( D - C ) ) )