Metamath Proof Explorer

Theorem sigardiv

Description: If signed area between vectors B - A and C - A is zero, then those vectors lie on the same line. (Contributed by Saveliy Skresanov, 22-Sep-2017)

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

Proof

Step Hyp Ref Expression
1 sigar 
 |-  G = ( x e. CC , y e. CC |-> ( Im ` ( ( * ` x ) x. y ) ) )
2 sigardiv.a 
 |-  ( ph -> ( A e. CC /\ B e. CC /\ C e. CC ) )
3 sigardiv.b 
 |-  ( ph -> -. C = A )
4 sigardiv.c 
 |-  ( ph -> ( ( B - A ) G ( C - A ) ) = 0 )
5 2 simp2d 
 |-  ( ph -> B e. CC )
6 2 simp1d 
 |-  ( ph -> A e. CC )
7 5 6 subcld 
 |-  ( ph -> ( B - A ) e. CC )
8 2 simp3d 
 |-  ( ph -> C e. CC )
9 8 6 subcld 
 |-  ( ph -> ( C - A ) e. CC )
10 3 neqned 
 |-  ( ph -> C =/= A )
11 8 6 10 subne0d 
 |-  ( ph -> ( C - A ) =/= 0 )
12 7 9 11 cjdivd 
 |-  ( ph -> ( * ` ( ( B - A ) / ( C - A ) ) ) = ( ( * ` ( B - A ) ) / ( * ` ( C - A ) ) ) )
13 7 cjcld 
 |-  ( ph -> ( * ` ( B - A ) ) e. CC )
14 9 cjcld 
 |-  ( ph -> ( * ` ( C - A ) ) e. CC )
15 9 11 cjne0d 
 |-  ( ph -> ( * ` ( C - A ) ) =/= 0 )
16 13 14 9 15 11 divcan5rd 
 |-  ( ph -> ( ( ( * ` ( B - A ) ) x. ( C - A ) ) / ( ( * ` ( C - A ) ) x. ( C - A ) ) ) = ( ( * ` ( B - A ) ) / ( * ` ( C - A ) ) ) )
17 13 9 mulcld 
 |-  ( ph -> ( ( * ` ( B - A ) ) x. ( C - A ) ) e. CC )
18 1 sigarval 
 |-  ( ( ( B - A ) e. CC /\ ( C - A ) e. CC ) -> ( ( B - A ) G ( C - A ) ) = ( Im ` ( ( * ` ( B - A ) ) x. ( C - A ) ) ) )
19 7 9 18 syl2anc 
 |-  ( ph -> ( ( B - A ) G ( C - A ) ) = ( Im ` ( ( * ` ( B - A ) ) x. ( C - A ) ) ) )
20 19 4 eqtr3d 
 |-  ( ph -> ( Im ` ( ( * ` ( B - A ) ) x. ( C - A ) ) ) = 0 )
21 17 20 reim0bd 
 |-  ( ph -> ( ( * ` ( B - A ) ) x. ( C - A ) ) e. RR )
22 9 14 mulcomd 
 |-  ( ph -> ( ( C - A ) x. ( * ` ( C - A ) ) ) = ( ( * ` ( C - A ) ) x. ( C - A ) ) )
23 9 cjmulrcld 
 |-  ( ph -> ( ( C - A ) x. ( * ` ( C - A ) ) ) e. RR )
24 22 23 eqeltrrd 
 |-  ( ph -> ( ( * ` ( C - A ) ) x. ( C - A ) ) e. RR )
25 14 9 15 11 mulne0d 
 |-  ( ph -> ( ( * ` ( C - A ) ) x. ( C - A ) ) =/= 0 )
26 21 24 25 redivcld 
 |-  ( ph -> ( ( ( * ` ( B - A ) ) x. ( C - A ) ) / ( ( * ` ( C - A ) ) x. ( C - A ) ) ) e. RR )
27 16 26 eqeltrrd 
 |-  ( ph -> ( ( * ` ( B - A ) ) / ( * ` ( C - A ) ) ) e. RR )
28 12 27 eqeltrd 
 |-  ( ph -> ( * ` ( ( B - A ) / ( C - A ) ) ) e. RR )
29 28 cjred 
 |-  ( ph -> ( * ` ( * ` ( ( B - A ) / ( C - A ) ) ) ) = ( * ` ( ( B - A ) / ( C - A ) ) ) )
30 7 9 11 divcld 
 |-  ( ph -> ( ( B - A ) / ( C - A ) ) e. CC )
31 30 cjcjd 
 |-  ( ph -> ( * ` ( * ` ( ( B - A ) / ( C - A ) ) ) ) = ( ( B - A ) / ( C - A ) ) )
32 29 31 eqtr3d 
 |-  ( ph -> ( * ` ( ( B - A ) / ( C - A ) ) ) = ( ( B - A ) / ( C - A ) ) )
33 32 28 eqeltrrd 
 |-  ( ph -> ( ( B - A ) / ( C - A ) ) e. RR )