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	⊢ 𝐺 = ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( ℑ ‘ ( ( ∗ ‘ 𝑥 ) · 𝑦 ) ) )
	sigarcol.a	⊢ ( 𝜑 → ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) )
	sigarcol.b	⊢ ( 𝜑 → ¬ 𝐴 = 𝐵 )
Assertion	sigarcol	⊢ ( 𝜑 → ( ( ( 𝐴 − 𝐶 ) 𝐺 ( 𝐵 − 𝐶 ) ) = 0 ↔ ∃ 𝑡 ∈ ℝ 𝐶 = ( 𝐵 + ( 𝑡 · ( 𝐴 − 𝐵 ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		sigarcol.sigar	⊢ 𝐺 = ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( ℑ ‘ ( ( ∗ ‘ 𝑥 ) · 𝑦 ) ) )
2		sigarcol.a	⊢ ( 𝜑 → ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) )
3		sigarcol.b	⊢ ( 𝜑 → ¬ 𝐴 = 𝐵 )
4	2	simp2d	⊢ ( 𝜑 → 𝐵 ∈ ℂ )
5	2	simp3d	⊢ ( 𝜑 → 𝐶 ∈ ℂ )
6	2	simp1d	⊢ ( 𝜑 → 𝐴 ∈ ℂ )
7	4 5 6	3jca	⊢ ( 𝜑 → ( 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ∧ 𝐴 ∈ ℂ ) )
8	7	adantr	⊢ ( ( 𝜑 ∧ ( ( 𝐴 − 𝐶 ) 𝐺 ( 𝐵 − 𝐶 ) ) = 0 ) → ( 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ∧ 𝐴 ∈ ℂ ) )
9	3	adantr	⊢ ( ( 𝜑 ∧ ( ( 𝐴 − 𝐶 ) 𝐺 ( 𝐵 − 𝐶 ) ) = 0 ) → ¬ 𝐴 = 𝐵 )
10	1	sigarperm	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( ( 𝐴 − 𝐶 ) 𝐺 ( 𝐵 − 𝐶 ) ) = ( ( 𝐵 − 𝐴 ) 𝐺 ( 𝐶 − 𝐴 ) ) )
11	2 10	syl	⊢ ( 𝜑 → ( ( 𝐴 − 𝐶 ) 𝐺 ( 𝐵 − 𝐶 ) ) = ( ( 𝐵 − 𝐴 ) 𝐺 ( 𝐶 − 𝐴 ) ) )
12	1	sigarperm	⊢ ( ( 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ∧ 𝐴 ∈ ℂ ) → ( ( 𝐵 − 𝐴 ) 𝐺 ( 𝐶 − 𝐴 ) ) = ( ( 𝐶 − 𝐵 ) 𝐺 ( 𝐴 − 𝐵 ) ) )
13	7 12	syl	⊢ ( 𝜑 → ( ( 𝐵 − 𝐴 ) 𝐺 ( 𝐶 − 𝐴 ) ) = ( ( 𝐶 − 𝐵 ) 𝐺 ( 𝐴 − 𝐵 ) ) )
14	11 13	eqtrd	⊢ ( 𝜑 → ( ( 𝐴 − 𝐶 ) 𝐺 ( 𝐵 − 𝐶 ) ) = ( ( 𝐶 − 𝐵 ) 𝐺 ( 𝐴 − 𝐵 ) ) )
15	14	eqeq1d	⊢ ( 𝜑 → ( ( ( 𝐴 − 𝐶 ) 𝐺 ( 𝐵 − 𝐶 ) ) = 0 ↔ ( ( 𝐶 − 𝐵 ) 𝐺 ( 𝐴 − 𝐵 ) ) = 0 ) )
16	15	biimpa	⊢ ( ( 𝜑 ∧ ( ( 𝐴 − 𝐶 ) 𝐺 ( 𝐵 − 𝐶 ) ) = 0 ) → ( ( 𝐶 − 𝐵 ) 𝐺 ( 𝐴 − 𝐵 ) ) = 0 )
17	1 8 9 16	sigardiv	⊢ ( ( 𝜑 ∧ ( ( 𝐴 − 𝐶 ) 𝐺 ( 𝐵 − 𝐶 ) ) = 0 ) → ( ( 𝐶 − 𝐵 ) / ( 𝐴 − 𝐵 ) ) ∈ ℝ )
18	5 4	subcld	⊢ ( 𝜑 → ( 𝐶 − 𝐵 ) ∈ ℂ )
19	18	adantr	⊢ ( ( 𝜑 ∧ ( ( 𝐴 − 𝐶 ) 𝐺 ( 𝐵 − 𝐶 ) ) = 0 ) → ( 𝐶 − 𝐵 ) ∈ ℂ )
20	6 4	subcld	⊢ ( 𝜑 → ( 𝐴 − 𝐵 ) ∈ ℂ )
21	20	adantr	⊢ ( ( 𝜑 ∧ ( ( 𝐴 − 𝐶 ) 𝐺 ( 𝐵 − 𝐶 ) ) = 0 ) → ( 𝐴 − 𝐵 ) ∈ ℂ )
22	6	adantr	⊢ ( ( 𝜑 ∧ ( ( 𝐴 − 𝐶 ) 𝐺 ( 𝐵 − 𝐶 ) ) = 0 ) → 𝐴 ∈ ℂ )
23	4	adantr	⊢ ( ( 𝜑 ∧ ( ( 𝐴 − 𝐶 ) 𝐺 ( 𝐵 − 𝐶 ) ) = 0 ) → 𝐵 ∈ ℂ )
24	9	neqned	⊢ ( ( 𝜑 ∧ ( ( 𝐴 − 𝐶 ) 𝐺 ( 𝐵 − 𝐶 ) ) = 0 ) → 𝐴 ≠ 𝐵 )
25	22 23 24	subne0d	⊢ ( ( 𝜑 ∧ ( ( 𝐴 − 𝐶 ) 𝐺 ( 𝐵 − 𝐶 ) ) = 0 ) → ( 𝐴 − 𝐵 ) ≠ 0 )
26	19 21 25	divcan1d	⊢ ( ( 𝜑 ∧ ( ( 𝐴 − 𝐶 ) 𝐺 ( 𝐵 − 𝐶 ) ) = 0 ) → ( ( ( 𝐶 − 𝐵 ) / ( 𝐴 − 𝐵 ) ) · ( 𝐴 − 𝐵 ) ) = ( 𝐶 − 𝐵 ) )
27	26	oveq2d	⊢ ( ( 𝜑 ∧ ( ( 𝐴 − 𝐶 ) 𝐺 ( 𝐵 − 𝐶 ) ) = 0 ) → ( 𝐵 + ( ( ( 𝐶 − 𝐵 ) / ( 𝐴 − 𝐵 ) ) · ( 𝐴 − 𝐵 ) ) ) = ( 𝐵 + ( 𝐶 − 𝐵 ) ) )
28	5	adantr	⊢ ( ( 𝜑 ∧ ( ( 𝐴 − 𝐶 ) 𝐺 ( 𝐵 − 𝐶 ) ) = 0 ) → 𝐶 ∈ ℂ )
29	23 28	pncan3d	⊢ ( ( 𝜑 ∧ ( ( 𝐴 − 𝐶 ) 𝐺 ( 𝐵 − 𝐶 ) ) = 0 ) → ( 𝐵 + ( 𝐶 − 𝐵 ) ) = 𝐶 )
30	27 29	eqtr2d	⊢ ( ( 𝜑 ∧ ( ( 𝐴 − 𝐶 ) 𝐺 ( 𝐵 − 𝐶 ) ) = 0 ) → 𝐶 = ( 𝐵 + ( ( ( 𝐶 − 𝐵 ) / ( 𝐴 − 𝐵 ) ) · ( 𝐴 − 𝐵 ) ) ) )
31		oveq1	⊢ ( 𝑡 = ( ( 𝐶 − 𝐵 ) / ( 𝐴 − 𝐵 ) ) → ( 𝑡 · ( 𝐴 − 𝐵 ) ) = ( ( ( 𝐶 − 𝐵 ) / ( 𝐴 − 𝐵 ) ) · ( 𝐴 − 𝐵 ) ) )
32	31	oveq2d	⊢ ( 𝑡 = ( ( 𝐶 − 𝐵 ) / ( 𝐴 − 𝐵 ) ) → ( 𝐵 + ( 𝑡 · ( 𝐴 − 𝐵 ) ) ) = ( 𝐵 + ( ( ( 𝐶 − 𝐵 ) / ( 𝐴 − 𝐵 ) ) · ( 𝐴 − 𝐵 ) ) ) )
33	32	rspceeqv	⊢ ( ( ( ( 𝐶 − 𝐵 ) / ( 𝐴 − 𝐵 ) ) ∈ ℝ ∧ 𝐶 = ( 𝐵 + ( ( ( 𝐶 − 𝐵 ) / ( 𝐴 − 𝐵 ) ) · ( 𝐴 − 𝐵 ) ) ) ) → ∃ 𝑡 ∈ ℝ 𝐶 = ( 𝐵 + ( 𝑡 · ( 𝐴 − 𝐵 ) ) ) )
34	17 30 33	syl2anc	⊢ ( ( 𝜑 ∧ ( ( 𝐴 − 𝐶 ) 𝐺 ( 𝐵 − 𝐶 ) ) = 0 ) → ∃ 𝑡 ∈ ℝ 𝐶 = ( 𝐵 + ( 𝑡 · ( 𝐴 − 𝐵 ) ) ) )
35	34	ex	⊢ ( 𝜑 → ( ( ( 𝐴 − 𝐶 ) 𝐺 ( 𝐵 − 𝐶 ) ) = 0 → ∃ 𝑡 ∈ ℝ 𝐶 = ( 𝐵 + ( 𝑡 · ( 𝐴 − 𝐵 ) ) ) ) )
36	14	3ad2ant1	⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℝ ∧ 𝐶 = ( 𝐵 + ( 𝑡 · ( 𝐴 − 𝐵 ) ) ) ) → ( ( 𝐴 − 𝐶 ) 𝐺 ( 𝐵 − 𝐶 ) ) = ( ( 𝐶 − 𝐵 ) 𝐺 ( 𝐴 − 𝐵 ) ) )
37	4	3ad2ant1	⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℝ ∧ 𝐶 = ( 𝐵 + ( 𝑡 · ( 𝐴 − 𝐵 ) ) ) ) → 𝐵 ∈ ℂ )
38		simp2	⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℝ ∧ 𝐶 = ( 𝐵 + ( 𝑡 · ( 𝐴 − 𝐵 ) ) ) ) → 𝑡 ∈ ℝ )
39	38	recnd	⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℝ ∧ 𝐶 = ( 𝐵 + ( 𝑡 · ( 𝐴 − 𝐵 ) ) ) ) → 𝑡 ∈ ℂ )
40	6	3ad2ant1	⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℝ ∧ 𝐶 = ( 𝐵 + ( 𝑡 · ( 𝐴 − 𝐵 ) ) ) ) → 𝐴 ∈ ℂ )
41	40 37	subcld	⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℝ ∧ 𝐶 = ( 𝐵 + ( 𝑡 · ( 𝐴 − 𝐵 ) ) ) ) → ( 𝐴 − 𝐵 ) ∈ ℂ )
42	39 41	mulcld	⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℝ ∧ 𝐶 = ( 𝐵 + ( 𝑡 · ( 𝐴 − 𝐵 ) ) ) ) → ( 𝑡 · ( 𝐴 − 𝐵 ) ) ∈ ℂ )
43		simp3	⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℝ ∧ 𝐶 = ( 𝐵 + ( 𝑡 · ( 𝐴 − 𝐵 ) ) ) ) → 𝐶 = ( 𝐵 + ( 𝑡 · ( 𝐴 − 𝐵 ) ) ) )
44	37 42 43	mvrladdd	⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℝ ∧ 𝐶 = ( 𝐵 + ( 𝑡 · ( 𝐴 − 𝐵 ) ) ) ) → ( 𝐶 − 𝐵 ) = ( 𝑡 · ( 𝐴 − 𝐵 ) ) )
45	44	oveq1d	⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℝ ∧ 𝐶 = ( 𝐵 + ( 𝑡 · ( 𝐴 − 𝐵 ) ) ) ) → ( ( 𝐶 − 𝐵 ) 𝐺 ( 𝐴 − 𝐵 ) ) = ( ( 𝑡 · ( 𝐴 − 𝐵 ) ) 𝐺 ( 𝐴 − 𝐵 ) ) )
46	39 41	mulcomd	⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℝ ∧ 𝐶 = ( 𝐵 + ( 𝑡 · ( 𝐴 − 𝐵 ) ) ) ) → ( 𝑡 · ( 𝐴 − 𝐵 ) ) = ( ( 𝐴 − 𝐵 ) · 𝑡 ) )
47	46	oveq1d	⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℝ ∧ 𝐶 = ( 𝐵 + ( 𝑡 · ( 𝐴 − 𝐵 ) ) ) ) → ( ( 𝑡 · ( 𝐴 − 𝐵 ) ) 𝐺 ( 𝐴 − 𝐵 ) ) = ( ( ( 𝐴 − 𝐵 ) · 𝑡 ) 𝐺 ( 𝐴 − 𝐵 ) ) )
48	45 47	eqtrd	⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℝ ∧ 𝐶 = ( 𝐵 + ( 𝑡 · ( 𝐴 − 𝐵 ) ) ) ) → ( ( 𝐶 − 𝐵 ) 𝐺 ( 𝐴 − 𝐵 ) ) = ( ( ( 𝐴 − 𝐵 ) · 𝑡 ) 𝐺 ( 𝐴 − 𝐵 ) ) )
49	41 39	mulcld	⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℝ ∧ 𝐶 = ( 𝐵 + ( 𝑡 · ( 𝐴 − 𝐵 ) ) ) ) → ( ( 𝐴 − 𝐵 ) · 𝑡 ) ∈ ℂ )
50	1	sigarac	⊢ ( ( ( ( 𝐴 − 𝐵 ) · 𝑡 ) ∈ ℂ ∧ ( 𝐴 − 𝐵 ) ∈ ℂ ) → ( ( ( 𝐴 − 𝐵 ) · 𝑡 ) 𝐺 ( 𝐴 − 𝐵 ) ) = - ( ( 𝐴 − 𝐵 ) 𝐺 ( ( 𝐴 − 𝐵 ) · 𝑡 ) ) )
51	49 41 50	syl2anc	⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℝ ∧ 𝐶 = ( 𝐵 + ( 𝑡 · ( 𝐴 − 𝐵 ) ) ) ) → ( ( ( 𝐴 − 𝐵 ) · 𝑡 ) 𝐺 ( 𝐴 − 𝐵 ) ) = - ( ( 𝐴 − 𝐵 ) 𝐺 ( ( 𝐴 − 𝐵 ) · 𝑡 ) ) )
52	1	sigarls	⊢ ( ( ( 𝐴 − 𝐵 ) ∈ ℂ ∧ ( 𝐴 − 𝐵 ) ∈ ℂ ∧ 𝑡 ∈ ℝ ) → ( ( 𝐴 − 𝐵 ) 𝐺 ( ( 𝐴 − 𝐵 ) · 𝑡 ) ) = ( ( ( 𝐴 − 𝐵 ) 𝐺 ( 𝐴 − 𝐵 ) ) · 𝑡 ) )
53	41 41 38 52	syl3anc	⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℝ ∧ 𝐶 = ( 𝐵 + ( 𝑡 · ( 𝐴 − 𝐵 ) ) ) ) → ( ( 𝐴 − 𝐵 ) 𝐺 ( ( 𝐴 − 𝐵 ) · 𝑡 ) ) = ( ( ( 𝐴 − 𝐵 ) 𝐺 ( 𝐴 − 𝐵 ) ) · 𝑡 ) )
54	1	sigarid	⊢ ( ( 𝐴 − 𝐵 ) ∈ ℂ → ( ( 𝐴 − 𝐵 ) 𝐺 ( 𝐴 − 𝐵 ) ) = 0 )
55	41 54	syl	⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℝ ∧ 𝐶 = ( 𝐵 + ( 𝑡 · ( 𝐴 − 𝐵 ) ) ) ) → ( ( 𝐴 − 𝐵 ) 𝐺 ( 𝐴 − 𝐵 ) ) = 0 )
56	55	oveq1d	⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℝ ∧ 𝐶 = ( 𝐵 + ( 𝑡 · ( 𝐴 − 𝐵 ) ) ) ) → ( ( ( 𝐴 − 𝐵 ) 𝐺 ( 𝐴 − 𝐵 ) ) · 𝑡 ) = ( 0 · 𝑡 ) )
57	39	mul02d	⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℝ ∧ 𝐶 = ( 𝐵 + ( 𝑡 · ( 𝐴 − 𝐵 ) ) ) ) → ( 0 · 𝑡 ) = 0 )
58	53 56 57	3eqtrd	⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℝ ∧ 𝐶 = ( 𝐵 + ( 𝑡 · ( 𝐴 − 𝐵 ) ) ) ) → ( ( 𝐴 − 𝐵 ) 𝐺 ( ( 𝐴 − 𝐵 ) · 𝑡 ) ) = 0 )
59	58	negeqd	⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℝ ∧ 𝐶 = ( 𝐵 + ( 𝑡 · ( 𝐴 − 𝐵 ) ) ) ) → - ( ( 𝐴 − 𝐵 ) 𝐺 ( ( 𝐴 − 𝐵 ) · 𝑡 ) ) = - 0 )
60		neg0	⊢ - 0 = 0
61	60	a1i	⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℝ ∧ 𝐶 = ( 𝐵 + ( 𝑡 · ( 𝐴 − 𝐵 ) ) ) ) → - 0 = 0 )
62	51 59 61	3eqtrd	⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℝ ∧ 𝐶 = ( 𝐵 + ( 𝑡 · ( 𝐴 − 𝐵 ) ) ) ) → ( ( ( 𝐴 − 𝐵 ) · 𝑡 ) 𝐺 ( 𝐴 − 𝐵 ) ) = 0 )
63	36 48 62	3eqtrd	⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℝ ∧ 𝐶 = ( 𝐵 + ( 𝑡 · ( 𝐴 − 𝐵 ) ) ) ) → ( ( 𝐴 − 𝐶 ) 𝐺 ( 𝐵 − 𝐶 ) ) = 0 )
64	63	rexlimdv3a	⊢ ( 𝜑 → ( ∃ 𝑡 ∈ ℝ 𝐶 = ( 𝐵 + ( 𝑡 · ( 𝐴 − 𝐵 ) ) ) → ( ( 𝐴 − 𝐶 ) 𝐺 ( 𝐵 − 𝐶 ) ) = 0 ) )
65	35 64	impbid	⊢ ( 𝜑 → ( ( ( 𝐴 − 𝐶 ) 𝐺 ( 𝐵 − 𝐶 ) ) = 0 ↔ ∃ 𝑡 ∈ ℝ 𝐶 = ( 𝐵 + ( 𝑡 · ( 𝐴 − 𝐵 ) ) ) ) )