Metamath Proof Explorer

Theorem sigarcol

Description: Given three points A , B and C such that -. A = B , the point C lies on the line going through A and B iff the corresponding signed area is zero. That justifies the usage of signed area as a collinearity indicator. (Contributed by Saveliy Skresanov, 22-Sep-2017)

Ref Expression
Hypotheses sigarcol.sigar 
|- G = ( x e. CC , y e. CC |-> ( Im ` ( ( * ` x ) x. y ) ) )
sigarcol.a 
|- ( ph -> ( A e. CC /\ B e. CC /\ C e. CC ) )
sigarcol.b 
|- ( ph -> -. A = B )
Assertion sigarcol 
|- ( ph -> ( ( ( A - C ) G ( B - C ) ) = 0 <-> E. t e. RR C = ( B + ( t x. ( A - B ) ) ) ) )

Proof

Step Hyp Ref Expression
1 sigarcol.sigar 
 |-  G = ( x e. CC , y e. CC |-> ( Im ` ( ( * ` x ) x. y ) ) )
2 sigarcol.a 
 |-  ( ph -> ( A e. CC /\ B e. CC /\ C e. CC ) )
3 sigarcol.b 
 |-  ( ph -> -. A = B )
4 2 simp2d 
 |-  ( ph -> B e. CC )
5 2 simp3d 
 |-  ( ph -> C e. CC )
6 2 simp1d 
 |-  ( ph -> A e. CC )
7 4 5 6 3jca 
 |-  ( ph -> ( B e. CC /\ C e. CC /\ A e. CC ) )
8 7 adantr 
 |-  ( ( ph /\ ( ( A - C ) G ( B - C ) ) = 0 ) -> ( B e. CC /\ C e. CC /\ A e. CC ) )
9 3 adantr 
 |-  ( ( ph /\ ( ( A - C ) G ( B - C ) ) = 0 ) -> -. A = B )
10 1 sigarperm 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( A - C ) G ( B - C ) ) = ( ( B - A ) G ( C - A ) ) )
11 2 10 syl 
 |-  ( ph -> ( ( A - C ) G ( B - C ) ) = ( ( B - A ) G ( C - A ) ) )
12 1 sigarperm 
 |-  ( ( B e. CC /\ C e. CC /\ A e. CC ) -> ( ( B - A ) G ( C - A ) ) = ( ( C - B ) G ( A - B ) ) )
13 7 12 syl 
 |-  ( ph -> ( ( B - A ) G ( C - A ) ) = ( ( C - B ) G ( A - B ) ) )
14 11 13 eqtrd 
 |-  ( ph -> ( ( A - C ) G ( B - C ) ) = ( ( C - B ) G ( A - B ) ) )
15 14 eqeq1d 
 |-  ( ph -> ( ( ( A - C ) G ( B - C ) ) = 0 <-> ( ( C - B ) G ( A - B ) ) = 0 ) )
16 15 biimpa 
 |-  ( ( ph /\ ( ( A - C ) G ( B - C ) ) = 0 ) -> ( ( C - B ) G ( A - B ) ) = 0 )
17 1 8 9 16 sigardiv 
 |-  ( ( ph /\ ( ( A - C ) G ( B - C ) ) = 0 ) -> ( ( C - B ) / ( A - B ) ) e. RR )
18 5 4 subcld 
 |-  ( ph -> ( C - B ) e. CC )
19 18 adantr 
 |-  ( ( ph /\ ( ( A - C ) G ( B - C ) ) = 0 ) -> ( C - B ) e. CC )
20 6 4 subcld 
 |-  ( ph -> ( A - B ) e. CC )
21 20 adantr 
 |-  ( ( ph /\ ( ( A - C ) G ( B - C ) ) = 0 ) -> ( A - B ) e. CC )
22 6 adantr 
 |-  ( ( ph /\ ( ( A - C ) G ( B - C ) ) = 0 ) -> A e. CC )
23 4 adantr 
 |-  ( ( ph /\ ( ( A - C ) G ( B - C ) ) = 0 ) -> B e. CC )
24 9 neqned 
 |-  ( ( ph /\ ( ( A - C ) G ( B - C ) ) = 0 ) -> A =/= B )
25 22 23 24 subne0d 
 |-  ( ( ph /\ ( ( A - C ) G ( B - C ) ) = 0 ) -> ( A - B ) =/= 0 )
26 19 21 25 divcan1d 
 |-  ( ( ph /\ ( ( A - C ) G ( B - C ) ) = 0 ) -> ( ( ( C - B ) / ( A - B ) ) x. ( A - B ) ) = ( C - B ) )
27 26 oveq2d 
 |-  ( ( ph /\ ( ( A - C ) G ( B - C ) ) = 0 ) -> ( B + ( ( ( C - B ) / ( A - B ) ) x. ( A - B ) ) ) = ( B + ( C - B ) ) )
28 5 adantr 
 |-  ( ( ph /\ ( ( A - C ) G ( B - C ) ) = 0 ) -> C e. CC )
29 23 28 pncan3d 
 |-  ( ( ph /\ ( ( A - C ) G ( B - C ) ) = 0 ) -> ( B + ( C - B ) ) = C )
30 27 29 eqtr2d 
 |-  ( ( ph /\ ( ( A - C ) G ( B - C ) ) = 0 ) -> C = ( B + ( ( ( C - B ) / ( A - B ) ) x. ( A - B ) ) ) )
31 oveq1 
 |-  ( t = ( ( C - B ) / ( A - B ) ) -> ( t x. ( A - B ) ) = ( ( ( C - B ) / ( A - B ) ) x. ( A - B ) ) )
32 31 oveq2d 
 |-  ( t = ( ( C - B ) / ( A - B ) ) -> ( B + ( t x. ( A - B ) ) ) = ( B + ( ( ( C - B ) / ( A - B ) ) x. ( A - B ) ) ) )
33 32 rspceeqv 
 |-  ( ( ( ( C - B ) / ( A - B ) ) e. RR /\ C = ( B + ( ( ( C - B ) / ( A - B ) ) x. ( A - B ) ) ) ) -> E. t e. RR C = ( B + ( t x. ( A - B ) ) ) )
34 17 30 33 syl2anc 
 |-  ( ( ph /\ ( ( A - C ) G ( B - C ) ) = 0 ) -> E. t e. RR C = ( B + ( t x. ( A - B ) ) ) )
35 34 ex 
 |-  ( ph -> ( ( ( A - C ) G ( B - C ) ) = 0 -> E. t e. RR C = ( B + ( t x. ( A - B ) ) ) ) )
36 14 3ad2ant1 
 |-  ( ( ph /\ t e. RR /\ C = ( B + ( t x. ( A - B ) ) ) ) -> ( ( A - C ) G ( B - C ) ) = ( ( C - B ) G ( A - B ) ) )
37 4 3ad2ant1 
 |-  ( ( ph /\ t e. RR /\ C = ( B + ( t x. ( A - B ) ) ) ) -> B e. CC )
38 simp2 
 |-  ( ( ph /\ t e. RR /\ C = ( B + ( t x. ( A - B ) ) ) ) -> t e. RR )
39 38 recnd 
 |-  ( ( ph /\ t e. RR /\ C = ( B + ( t x. ( A - B ) ) ) ) -> t e. CC )
40 6 3ad2ant1 
 |-  ( ( ph /\ t e. RR /\ C = ( B + ( t x. ( A - B ) ) ) ) -> A e. CC )
41 40 37 subcld 
 |-  ( ( ph /\ t e. RR /\ C = ( B + ( t x. ( A - B ) ) ) ) -> ( A - B ) e. CC )
42 39 41 mulcld 
 |-  ( ( ph /\ t e. RR /\ C = ( B + ( t x. ( A - B ) ) ) ) -> ( t x. ( A - B ) ) e. CC )
43 simp3 
 |-  ( ( ph /\ t e. RR /\ C = ( B + ( t x. ( A - B ) ) ) ) -> C = ( B + ( t x. ( A - B ) ) ) )
44 37 42 43 mvrladdd 
 |-  ( ( ph /\ t e. RR /\ C = ( B + ( t x. ( A - B ) ) ) ) -> ( C - B ) = ( t x. ( A - B ) ) )
45 44 oveq1d 
 |-  ( ( ph /\ t e. RR /\ C = ( B + ( t x. ( A - B ) ) ) ) -> ( ( C - B ) G ( A - B ) ) = ( ( t x. ( A - B ) ) G ( A - B ) ) )
46 39 41 mulcomd 
 |-  ( ( ph /\ t e. RR /\ C = ( B + ( t x. ( A - B ) ) ) ) -> ( t x. ( A - B ) ) = ( ( A - B ) x. t ) )
47 46 oveq1d 
 |-  ( ( ph /\ t e. RR /\ C = ( B + ( t x. ( A - B ) ) ) ) -> ( ( t x. ( A - B ) ) G ( A - B ) ) = ( ( ( A - B ) x. t ) G ( A - B ) ) )
48 45 47 eqtrd 
 |-  ( ( ph /\ t e. RR /\ C = ( B + ( t x. ( A - B ) ) ) ) -> ( ( C - B ) G ( A - B ) ) = ( ( ( A - B ) x. t ) G ( A - B ) ) )
49 41 39 mulcld 
 |-  ( ( ph /\ t e. RR /\ C = ( B + ( t x. ( A - B ) ) ) ) -> ( ( A - B ) x. t ) e. CC )
50 1 sigarac 
 |-  ( ( ( ( A - B ) x. t ) e. CC /\ ( A - B ) e. CC ) -> ( ( ( A - B ) x. t ) G ( A - B ) ) = -u ( ( A - B ) G ( ( A - B ) x. t ) ) )
51 49 41 50 syl2anc 
 |-  ( ( ph /\ t e. RR /\ C = ( B + ( t x. ( A - B ) ) ) ) -> ( ( ( A - B ) x. t ) G ( A - B ) ) = -u ( ( A - B ) G ( ( A - B ) x. t ) ) )
52 1 sigarls 
 |-  ( ( ( A - B ) e. CC /\ ( A - B ) e. CC /\ t e. RR ) -> ( ( A - B ) G ( ( A - B ) x. t ) ) = ( ( ( A - B ) G ( A - B ) ) x. t ) )
53 41 41 38 52 syl3anc 
 |-  ( ( ph /\ t e. RR /\ C = ( B + ( t x. ( A - B ) ) ) ) -> ( ( A - B ) G ( ( A - B ) x. t ) ) = ( ( ( A - B ) G ( A - B ) ) x. t ) )
54 1 sigarid 
 |-  ( ( A - B ) e. CC -> ( ( A - B ) G ( A - B ) ) = 0 )
55 41 54 syl 
 |-  ( ( ph /\ t e. RR /\ C = ( B + ( t x. ( A - B ) ) ) ) -> ( ( A - B ) G ( A - B ) ) = 0 )
56 55 oveq1d 
 |-  ( ( ph /\ t e. RR /\ C = ( B + ( t x. ( A - B ) ) ) ) -> ( ( ( A - B ) G ( A - B ) ) x. t ) = ( 0 x. t ) )
57 39 mul02d 
 |-  ( ( ph /\ t e. RR /\ C = ( B + ( t x. ( A - B ) ) ) ) -> ( 0 x. t ) = 0 )
58 53 56 57 3eqtrd 
 |-  ( ( ph /\ t e. RR /\ C = ( B + ( t x. ( A - B ) ) ) ) -> ( ( A - B ) G ( ( A - B ) x. t ) ) = 0 )
59 58 negeqd 
 |-  ( ( ph /\ t e. RR /\ C = ( B + ( t x. ( A - B ) ) ) ) -> -u ( ( A - B ) G ( ( A - B ) x. t ) ) = -u 0 )
60 neg0 
 |-  -u 0 = 0
61 60 a1i 
 |-  ( ( ph /\ t e. RR /\ C = ( B + ( t x. ( A - B ) ) ) ) -> -u 0 = 0 )
62 51 59 61 3eqtrd 
 |-  ( ( ph /\ t e. RR /\ C = ( B + ( t x. ( A - B ) ) ) ) -> ( ( ( A - B ) x. t ) G ( A - B ) ) = 0 )
63 36 48 62 3eqtrd 
 |-  ( ( ph /\ t e. RR /\ C = ( B + ( t x. ( A - B ) ) ) ) -> ( ( A - C ) G ( B - C ) ) = 0 )
64 63 rexlimdv3a 
 |-  ( ph -> ( E. t e. RR C = ( B + ( t x. ( A - B ) ) ) -> ( ( A - C ) G ( B - C ) ) = 0 ) )
65 35 64 impbid 
 |-  ( ph -> ( ( ( A - C ) G ( B - C ) ) = 0 <-> E. t e. RR C = ( B + ( t x. ( A - B ) ) ) ) )