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 \in ℂ, y \in ℂ ⟼ ℑ (\overline{x} y))$
	sigarcol.a	$⊢ φ \to (A \in ℂ \land B \in ℂ \land C \in ℂ)$
	sigarcol.b	$⊢ φ \to \neg A = B$
Assertion	sigarcol	$⊢ φ \to ((A - C) G (B - C) = 0 \leftrightarrow \exists t \in ℝ C = B + t (A - B))$

Proof

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

Metamath Proof Explorer

Theorem sigarcol

Proof