Theorem sigarcol 38467

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.)

Hypotheses

Ref	Expression
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

Ref	Expression
sigarcol	|- ( ph -> ( ( ( A - C ) G ( B - C ) ) = 0 <-> E. t e. RR C = ( B + ( t x. ( A - B ) ) ) ) )

Distinct variable groups:   x, t, y, A   t, B, x, y   t, C, x, y   t, G   ph, t

Allowed substitution hints:   ph( x, y)   G( x, y)

Proof of Theorem sigarcol

Step	Hyp	Ref	Expression
1		sigarcol.sigar	. . . . 5 |- G = ( x e. CC , y e. CC |-> ( Im ` ( ( * ` x ) x. y ) ) )
2		sigarcol.a	. . . . . . . 8 |- ( ph -> ( A e. CC /\ B e. CC /\ C e. CC ) )
3	2	simp2d 1020	. . . . . . 7 |- ( ph -> B e. CC )
4	2	simp3d 1021	. . . . . . 7 |- ( ph -> C e. CC )
5	2	simp1d 1019	. . . . . . 7 |- ( ph -> A e. CC )
6	3, 4, 5	3jca 1187	. . . . . 6 |- ( ph -> ( B e. CC /\ C e. CC /\ A e. CC ) )
7	6	adantr 467	. . . . 5 |- ( ( ph /\ ( ( A - C ) G ( B - C ) ) = 0 ) -> ( B e. CC /\ C e. CC /\ A e. CC ) )
8		sigarcol.b	. . . . . 6 |- ( ph -> -. A = B )
9	8	adantr 467	. . . . 5 |- ( ( ph /\ ( ( A - C ) G ( B - C ) ) = 0 ) -> -. A = B )
10	1	sigarperm 38463	. . . . . . . . 9 |- ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( A - C ) G ( B - C ) ) = ( ( B - A ) G ( C - A ) ) )
11	2, 10	syl 17	. . . . . . . 8 |- ( ph -> ( ( A - C ) G ( B - C ) ) = ( ( B - A ) G ( C - A ) ) )
12	1	sigarperm 38463	. . . . . . . . 9 |- ( ( B e. CC /\ C e. CC /\ A e. CC ) -> ( ( B - A ) G ( C - A ) ) = ( ( C - B ) G ( A - B ) ) )
13	6, 12	syl 17	. . . . . . . 8 |- ( ph -> ( ( B - A ) G ( C - A ) ) = ( ( C - B ) G ( A - B ) ) )
14	11, 13	eqtrd 2484	. . . . . . 7 |- ( ph -> ( ( A - C ) G ( B - C ) ) = ( ( C - B ) G ( A - B ) ) )
15	14	eqeq1d 2452	. . . . . 6 |- ( ph -> ( ( ( A - C ) G ( B - C ) ) = 0 <-> ( ( C - B ) G ( A - B ) ) = 0 ) )
16	15	biimpa 487	. . . . 5 |- ( ( ph /\ ( ( A - C ) G ( B - C ) ) = 0 ) -> ( ( C - B ) G ( A - B ) ) = 0 )
17	1, 7, 9, 16	sigardiv 38464	. . . 4 |- ( ( ph /\ ( ( A - C ) G ( B - C ) ) = 0 ) -> ( ( C - B ) / ( A - B ) ) e. RR )
18	4, 3	subcld 9983	. . . . . . . 8 |- ( ph -> ( C - B ) e. CC )
19	18	adantr 467	. . . . . . 7 |- ( ( ph /\ ( ( A - C ) G ( B - C ) ) = 0 ) -> ( C - B ) e. CC )
20	5, 3	subcld 9983	. . . . . . . 8 |- ( ph -> ( A - B ) e. CC )
21	20	adantr 467	. . . . . . 7 |- ( ( ph /\ ( ( A - C ) G ( B - C ) ) = 0 ) -> ( A - B ) e. CC )
22	5	adantr 467	. . . . . . . 8 |- ( ( ph /\ ( ( A - C ) G ( B - C ) ) = 0 ) -> A e. CC )
23	3	adantr 467	. . . . . . . 8 |- ( ( ph /\ ( ( A - C ) G ( B - C ) ) = 0 ) -> B e. CC )
24	9	neqned 2630	. . . . . . . 8 |- ( ( ph /\ ( ( A - C ) G ( B - C ) ) = 0 ) -> A =/= B )
25	22, 23, 24	subne0d 9992	. . . . . . 7 |- ( ( ph /\ ( ( A - C ) G ( B - C ) ) = 0 ) -> ( A - B ) =/= 0 )
26	19, 21, 25	divcan1d 10381	. . . . . 6 |- ( ( ph /\ ( ( A - C ) G ( B - C ) ) = 0 ) -> ( ( ( C - B ) / ( A - B ) ) x. ( A - B ) ) = ( C - B ) )
27	26	oveq2d 6304	. . . . 5 |- ( ( ph /\ ( ( A - C ) G ( B - C ) ) = 0 ) -> ( B + ( ( ( C - B ) / ( A - B ) ) x. ( A - B ) ) ) = ( B + ( C - B ) ) )
28	4	adantr 467	. . . . . 6 |- ( ( ph /\ ( ( A - C ) G ( B - C ) ) = 0 ) -> C e. CC )
29	23, 28	pncan3d 9986	. . . . 5 |- ( ( ph /\ ( ( A - C ) G ( B - C ) ) = 0 ) -> ( B + ( C - B ) ) = C )
30	27, 29	eqtr2d 2485	. . . 4 |- ( ( ph /\ ( ( A - C ) G ( B - C ) ) = 0 ) -> C = ( B + ( ( ( C - B ) / ( A - B ) ) x. ( A - B ) ) ) )
31		oveq1 6295	. . . . . . 7 |- ( t = ( ( C - B ) / ( A - B ) ) -> ( t x. ( A - B ) ) = ( ( ( C - B ) / ( A - B ) ) x. ( A - B ) ) )
32	31	oveq2d 6304	. . . . . 6 |- ( t = ( ( C - B ) / ( A - B ) ) -> ( B + ( t x. ( A - B ) ) ) = ( B + ( ( ( C - B ) / ( A - B ) ) x. ( A - B ) ) ) )
33	32	eqeq2d 2460	. . . . 5 |- ( t = ( ( C - B ) / ( A - B ) ) -> ( C = ( B + ( t x. ( A - B ) ) ) <-> C = ( B + ( ( ( C - B ) / ( A - B ) ) x. ( A - B ) ) ) ) )
34	33	rspcev 3149	. . . 4 |- ( ( ( ( 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 ) ) ) )
35	17, 30, 34	syl2anc 666	. . 3 |- ( ( ph /\ ( ( A - C ) G ( B - C ) ) = 0 ) -> E. t e. RR C = ( B + ( t x. ( A - B ) ) ) )
36	35	ex 436	. 2 |- ( ph -> ( ( ( A - C ) G ( B - C ) ) = 0 -> E. t e. RR C = ( B + ( t x. ( A - B ) ) ) ) )
37	14	3ad2ant1 1028	. . . 4 |- ( ( ph /\ t e. RR /\ C = ( B + ( t x. ( A - B ) ) ) ) -> ( ( A - C ) G ( B - C ) ) = ( ( C - B ) G ( A - B ) ) )
38		simp3 1009	. . . . . . . 8 |- ( ( ph /\ t e. RR /\ C = ( B + ( t x. ( A - B ) ) ) ) -> C = ( B + ( t x. ( A - B ) ) ) )
39	38	oveq1d 6303	. . . . . . 7 |- ( ( ph /\ t e. RR /\ C = ( B + ( t x. ( A - B ) ) ) ) -> ( C - B ) = ( ( B + ( t x. ( A - B ) ) ) - B ) )
40	3	3ad2ant1 1028	. . . . . . . 8 |- ( ( ph /\ t e. RR /\ C = ( B + ( t x. ( A - B ) ) ) ) -> B e. CC )
41		simp2 1008	. . . . . . . . . 10 |- ( ( ph /\ t e. RR /\ C = ( B + ( t x. ( A - B ) ) ) ) -> t e. RR )
42	41	recnd 9666	. . . . . . . . 9 |- ( ( ph /\ t e. RR /\ C = ( B + ( t x. ( A - B ) ) ) ) -> t e. CC )
43	5	3ad2ant1 1028	. . . . . . . . . 10 |- ( ( ph /\ t e. RR /\ C = ( B + ( t x. ( A - B ) ) ) ) -> A e. CC )
44	43, 40	subcld 9983	. . . . . . . . 9 |- ( ( ph /\ t e. RR /\ C = ( B + ( t x. ( A - B ) ) ) ) -> ( A - B ) e. CC )
45	42, 44	mulcld 9660	. . . . . . . 8 |- ( ( ph /\ t e. RR /\ C = ( B + ( t x. ( A - B ) ) ) ) -> ( t x. ( A - B ) ) e. CC )
46	40, 45	pncan2d 9985	. . . . . . 7 |- ( ( ph /\ t e. RR /\ C = ( B + ( t x. ( A - B ) ) ) ) -> ( ( B + ( t x. ( A - B ) ) ) - B ) = ( t x. ( A - B ) ) )
47	39, 46	eqtrd 2484	. . . . . 6 |- ( ( ph /\ t e. RR /\ C = ( B + ( t x. ( A - B ) ) ) ) -> ( C - B ) = ( t x. ( A - B ) ) )
48	47	oveq1d 6303	. . . . 5 |- ( ( ph /\ t e. RR /\ C = ( B + ( t x. ( A - B ) ) ) ) -> ( ( C - B ) G ( A - B ) ) = ( ( t x. ( A - B ) ) G ( A - B ) ) )
49	42, 44	mulcomd 9661	. . . . . 6 |- ( ( ph /\ t e. RR /\ C = ( B + ( t x. ( A - B ) ) ) ) -> ( t x. ( A - B ) ) = ( ( A - B ) x. t ) )
50	49	oveq1d 6303	. . . . 5 |- ( ( ph /\ t e. RR /\ C = ( B + ( t x. ( A - B ) ) ) ) -> ( ( t x. ( A - B ) ) G ( A - B ) ) = ( ( ( A - B ) x. t ) G ( A - B ) ) )
51	48, 50	eqtrd 2484	. . . 4 |- ( ( ph /\ t e. RR /\ C = ( B + ( t x. ( A - B ) ) ) ) -> ( ( C - B ) G ( A - B ) ) = ( ( ( A - B ) x. t ) G ( A - B ) ) )
52	44, 42	mulcld 9660	. . . . . 6 |- ( ( ph /\ t e. RR /\ C = ( B + ( t x. ( A - B ) ) ) ) -> ( ( A - B ) x. t ) e. CC )
53	1	sigarac 38455	. . . . . 6 |- ( ( ( ( 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 ) ) )
54	52, 44, 53	syl2anc 666	. . . . 5 |- ( ( 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 ) ) )
55	1	sigarls 38460	. . . . . . . 8 |- ( ( ( 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 ) )
56	44, 44, 41, 55	syl3anc 1267	. . . . . . 7 |- ( ( ph /\ t e. RR /\ C = ( B + ( t x. ( A - B ) ) ) ) -> ( ( A - B ) G ( ( A - B ) x. t ) ) = ( ( ( A - B ) G ( A - B ) ) x. t ) )
57	1	sigarid 38461	. . . . . . . . 9 |- ( ( A - B ) e. CC -> ( ( A - B ) G ( A - B ) ) = 0 )
58	44, 57	syl 17	. . . . . . . 8 |- ( ( ph /\ t e. RR /\ C = ( B + ( t x. ( A - B ) ) ) ) -> ( ( A - B ) G ( A - B ) ) = 0 )
59	58	oveq1d 6303	. . . . . . 7 |- ( ( ph /\ t e. RR /\ C = ( B + ( t x. ( A - B ) ) ) ) -> ( ( ( A - B ) G ( A - B ) ) x. t ) = ( 0 x. t ) )
60	42	mul02d 9828	. . . . . . 7 |- ( ( ph /\ t e. RR /\ C = ( B + ( t x. ( A - B ) ) ) ) -> ( 0 x. t ) = 0 )
61	56, 59, 60	3eqtrd 2488	. . . . . 6 |- ( ( ph /\ t e. RR /\ C = ( B + ( t x. ( A - B ) ) ) ) -> ( ( A - B ) G ( ( A - B ) x. t ) ) = 0 )
62	61	negeqd 9866	. . . . 5 |- ( ( ph /\ t e. RR /\ C = ( B + ( t x. ( A - B ) ) ) ) -> -u ( ( A - B ) G ( ( A - B ) x. t ) ) = -u 0 )
63		neg0 9917	. . . . . 6 |- -u 0 = 0
64	63	a1i 11	. . . . 5 |- ( ( ph /\ t e. RR /\ C = ( B + ( t x. ( A - B ) ) ) ) -> -u 0 = 0 )
65	54, 62, 64	3eqtrd 2488	. . . 4 |- ( ( ph /\ t e. RR /\ C = ( B + ( t x. ( A - B ) ) ) ) -> ( ( ( A - B ) x. t ) G ( A - B ) ) = 0 )
66	37, 51, 65	3eqtrd 2488	. . 3 |- ( ( ph /\ t e. RR /\ C = ( B + ( t x. ( A - B ) ) ) ) -> ( ( A - C ) G ( B - C ) ) = 0 )
67	66	rexlimdv3a 2880	. 2 |- ( ph -> ( E. t e. RR C = ( B + ( t x. ( A - B ) ) ) -> ( ( A - C ) G ( B - C ) ) = 0 ) )
68	36, 67	impbid 194	1 |- ( ph -> ( ( ( A - C ) G ( B - C ) ) = 0 <-> E. t e. RR C = ( B + ( t x. ( A - B ) ) ) ) )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 188   /\ wa 371   /\ w3a 984   = wceq 1443   e. wcel 1886   E.wrex 2737   ` cfv 5581  (class class class)co 6288   |-> cmpt2 6290   CCcc 9534   RRcr 9535   0cc0 9536   + caddc 9539   x. cmul 9541   - cmin 9857   -ucneg 9858   / cdiv 10266   *ccj 13152   Imcim 13154

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1668  ax-4 1681  ax-5 1757  ax-6 1804  ax-7 1850  ax-8 1888  ax-9 1895  ax-10 1914  ax-11 1919  ax-12 1932  ax-13 2090  ax-ext 2430  ax-sep 4524  ax-nul 4533  ax-pow 4580  ax-pr 4638  ax-un 6580  ax-resscn 9593  ax-1cn 9594  ax-icn 9595  ax-addcl 9596  ax-addrcl 9597  ax-mulcl 9598  ax-mulrcl 9599  ax-mulcom 9600  ax-addass 9601  ax-mulass 9602  ax-distr 9603  ax-i2m1 9604  ax-1ne0 9605  ax-1rid 9606  ax-rnegex 9607  ax-rrecex 9608  ax-cnre 9609  ax-pre-lttri 9610  ax-pre-lttrn 9611  ax-pre-ltadd 9612  ax-pre-mulgt0 9613

This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3or 985  df-3an 986  df-tru 1446  df-ex 1663  df-nf 1667  df-sb 1797  df-eu 2302  df-mo 2303  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2580  df-ne 2623  df-nel 2624  df-ral 2741  df-rex 2742  df-reu 2743  df-rmo 2744  df-rab 2745  df-v 3046  df-sbc 3267  df-csb 3363  df-dif 3406  df-un 3408  df-in 3410  df-ss 3417  df-nul 3731  df-if 3881  df-pw 3952  df-sn 3968  df-pr 3970  df-op 3974  df-uni 4198  df-br 4402  df-opab 4461  df-mpt 4462  df-id 4748  df-po 4754  df-so 4755  df-xp 4839  df-rel 4840  df-cnv 4841  df-co 4842  df-dm 4843  df-rn 4844  df-res 4845  df-ima 4846  df-iota 5545  df-fun 5583  df-fn 5584  df-f 5585  df-f1 5586  df-fo 5587  df-f1o 5588  df-fv 5589  df-riota 6250  df-ov 6291  df-oprab 6292  df-mpt2 6293  df-er 7360  df-en 7567  df-dom 7568  df-sdom 7569  df-pnf 9674  df-mnf 9675  df-xr 9676  df-ltxr 9677  df-le 9678  df-sub 9859  df-neg 9860  df-div 10267  df-2 10665  df-cj 13155  df-re 13156  df-im 13157

This theorem is referenced by: (None)