colline

Description: Three points are colinear iff there is a line through all three of them. Theorem 6.23 of Schwabhauser p. 46. (Contributed by Thierry Arnoux, 28-May-2019)

	Ref	Expression
Hypotheses	tglineintmo.p	$⊢ P = {Base}_{G}$
	tglineintmo.i	$⊢ I = Itv (G)$
	tglineintmo.l	$⊢ L = {Line}_{𝒢} (G)$
	tglineintmo.g	$⊢ φ \to G \in 𝒢_{Tarski}$
	colline.1	$⊢ φ \to X \in P$
	colline.2	$⊢ φ \to Y \in P$
	colline.3	$⊢ φ \to Z \in P$
	colline.4	$⊢ φ \to 2 \leq \|P\|$
Assertion	colline	$⊢ φ \to ((X \in (Y L Z) \lor Y = Z) \leftrightarrow \exists a \in ran L (X \in a \land Y \in a \land Z \in a))$

Proof

Step	Hyp	Ref	Expression
1		tglineintmo.p	$⊢ P = {Base}_{G}$
2		tglineintmo.i	$⊢ I = Itv (G)$
3		tglineintmo.l	$⊢ L = {Line}_{𝒢} (G)$
4		tglineintmo.g	$⊢ φ \to G \in 𝒢_{Tarski}$
5		colline.1	$⊢ φ \to X \in P$
6		colline.2	$⊢ φ \to Y \in P$
7		colline.3	$⊢ φ \to Z \in P$
8		colline.4	$⊢ φ \to 2 \leq \|P\|$
9	4	ad4antr	$⊢ ((((φ \land Y = Z) \land X = Z) \land x \in P) \land X \neq x) \to G \in 𝒢_{Tarski}$
10	5	ad4antr	$⊢ ((((φ \land Y = Z) \land X = Z) \land x \in P) \land X \neq x) \to X \in P$
11		simplr	$⊢ ((((φ \land Y = Z) \land X = Z) \land x \in P) \land X \neq x) \to x \in P$
12		simpr	$⊢ ((((φ \land Y = Z) \land X = Z) \land x \in P) \land X \neq x) \to X \neq x$
13	1 2 3 9 10 11 12	tgelrnln	$⊢ ((((φ \land Y = Z) \land X = Z) \land x \in P) \land X \neq x) \to X L x \in ran L$
14	1 2 3 9 10 11 12	tglinerflx1	$⊢ ((((φ \land Y = Z) \land X = Z) \land x \in P) \land X \neq x) \to X \in (X L x)$
15		simp-4r	$⊢ ((((φ \land Y = Z) \land X = Z) \land x \in P) \land X \neq x) \to Y = Z$
16		simpllr	$⊢ ((((φ \land Y = Z) \land X = Z) \land x \in P) \land X \neq x) \to X = Z$
17	16 14	eqeltrrd	$⊢ ((((φ \land Y = Z) \land X = Z) \land x \in P) \land X \neq x) \to Z \in (X L x)$
18	15 17	eqeltrd	$⊢ ((((φ \land Y = Z) \land X = Z) \land x \in P) \land X \neq x) \to Y \in (X L x)$
19		eleq2	$⊢ a = X L x \to (X \in a \leftrightarrow X \in (X L x))$
20		eleq2	$⊢ a = X L x \to (Y \in a \leftrightarrow Y \in (X L x))$
21		eleq2	$⊢ a = X L x \to (Z \in a \leftrightarrow Z \in (X L x))$
22	19 20 21	3anbi123d	$⊢ a = X L x \to ((X \in a \land Y \in a \land Z \in a) \leftrightarrow (X \in (X L x) \land Y \in (X L x) \land Z \in (X L x)))$
23	22	rspcev	$⊢ (X L x \in ran L \land (X \in (X L x) \land Y \in (X L x) \land Z \in (X L x))) \to \exists a \in ran L (X \in a \land Y \in a \land Z \in a)$
24	13 14 18 17 23	syl13anc	$⊢ ((((φ \land Y = Z) \land X = Z) \land x \in P) \land X \neq x) \to \exists a \in ran L (X \in a \land Y \in a \land Z \in a)$
25		eqid	$⊢ dist (G) = dist (G)$
26	1 25 2 4 8 5	tglowdim1i	$⊢ φ \to \exists x \in P X \neq x$
27	26	ad2antrr	$⊢ ((φ \land Y = Z) \land X = Z) \to \exists x \in P X \neq x$
28	24 27	r19.29a	$⊢ ((φ \land Y = Z) \land X = Z) \to \exists a \in ran L (X \in a \land Y \in a \land Z \in a)$
29	4	ad2antrr	$⊢ ((φ \land Y = Z) \land X \neq Z) \to G \in 𝒢_{Tarski}$
30	5	ad2antrr	$⊢ ((φ \land Y = Z) \land X \neq Z) \to X \in P$
31	7	ad2antrr	$⊢ ((φ \land Y = Z) \land X \neq Z) \to Z \in P$
32		simpr	$⊢ ((φ \land Y = Z) \land X \neq Z) \to X \neq Z$
33	1 2 3 29 30 31 32	tgelrnln	$⊢ ((φ \land Y = Z) \land X \neq Z) \to X L Z \in ran L$
34	1 2 3 29 30 31 32	tglinerflx1	$⊢ ((φ \land Y = Z) \land X \neq Z) \to X \in (X L Z)$
35		simplr	$⊢ ((φ \land Y = Z) \land X \neq Z) \to Y = Z$
36	1 2 3 29 30 31 32	tglinerflx2	$⊢ ((φ \land Y = Z) \land X \neq Z) \to Z \in (X L Z)$
37	35 36	eqeltrd	$⊢ ((φ \land Y = Z) \land X \neq Z) \to Y \in (X L Z)$
38		eleq2	$⊢ a = X L Z \to (X \in a \leftrightarrow X \in (X L Z))$
39		eleq2	$⊢ a = X L Z \to (Y \in a \leftrightarrow Y \in (X L Z))$
40		eleq2	$⊢ a = X L Z \to (Z \in a \leftrightarrow Z \in (X L Z))$
41	38 39 40	3anbi123d	$⊢ a = X L Z \to ((X \in a \land Y \in a \land Z \in a) \leftrightarrow (X \in (X L Z) \land Y \in (X L Z) \land Z \in (X L Z)))$
42	41	rspcev	$⊢ (X L Z \in ran L \land (X \in (X L Z) \land Y \in (X L Z) \land Z \in (X L Z))) \to \exists a \in ran L (X \in a \land Y \in a \land Z \in a)$
43	33 34 37 36 42	syl13anc	$⊢ ((φ \land Y = Z) \land X \neq Z) \to \exists a \in ran L (X \in a \land Y \in a \land Z \in a)$
44	28 43	pm2.61dane	$⊢ (φ \land Y = Z) \to \exists a \in ran L (X \in a \land Y \in a \land Z \in a)$
45	44	adantlr	$⊢ ((φ \land (X \in (Y L Z) \lor Y = Z)) \land Y = Z) \to \exists a \in ran L (X \in a \land Y \in a \land Z \in a)$
46		simpll	$⊢ ((φ \land (X \in (Y L Z) \lor Y = Z)) \land Y \neq Z) \to φ$
47		simpr	$⊢ ((φ \land (X \in (Y L Z) \lor Y = Z)) \land Y \neq Z) \to Y \neq Z$
48	47	neneqd	$⊢ ((φ \land (X \in (Y L Z) \lor Y = Z)) \land Y \neq Z) \to \neg Y = Z$
49		simplr	$⊢ ((φ \land (X \in (Y L Z) \lor Y = Z)) \land Y \neq Z) \to (X \in (Y L Z) \lor Y = Z)$
50		orel2	$⊢ \neg Y = Z \to ((X \in (Y L Z) \lor Y = Z) \to X \in (Y L Z))$
51	48 49 50	sylc	$⊢ ((φ \land (X \in (Y L Z) \lor Y = Z)) \land Y \neq Z) \to X \in (Y L Z)$
52	4	ad2antrr	$⊢ ((φ \land X \in (Y L Z)) \land Y \neq Z) \to G \in 𝒢_{Tarski}$
53	6	ad2antrr	$⊢ ((φ \land X \in (Y L Z)) \land Y \neq Z) \to Y \in P$
54	7	ad2antrr	$⊢ ((φ \land X \in (Y L Z)) \land Y \neq Z) \to Z \in P$
55		simpr	$⊢ ((φ \land X \in (Y L Z)) \land Y \neq Z) \to Y \neq Z$
56	1 2 3 52 53 54 55	tgelrnln	$⊢ ((φ \land X \in (Y L Z)) \land Y \neq Z) \to Y L Z \in ran L$
57	46 51 47 56	syl21anc	$⊢ ((φ \land (X \in (Y L Z) \lor Y = Z)) \land Y \neq Z) \to Y L Z \in ran L$
58	1 2 3 52 53 54 55	tglinerflx1	$⊢ ((φ \land X \in (Y L Z)) \land Y \neq Z) \to Y \in (Y L Z)$
59	46 51 47 58	syl21anc	$⊢ ((φ \land (X \in (Y L Z) \lor Y = Z)) \land Y \neq Z) \to Y \in (Y L Z)$
60	1 2 3 52 53 54 55	tglinerflx2	$⊢ ((φ \land X \in (Y L Z)) \land Y \neq Z) \to Z \in (Y L Z)$
61	46 51 47 60	syl21anc	$⊢ ((φ \land (X \in (Y L Z) \lor Y = Z)) \land Y \neq Z) \to Z \in (Y L Z)$
62		eleq2	$⊢ a = Y L Z \to (X \in a \leftrightarrow X \in (Y L Z))$
63		eleq2	$⊢ a = Y L Z \to (Y \in a \leftrightarrow Y \in (Y L Z))$
64		eleq2	$⊢ a = Y L Z \to (Z \in a \leftrightarrow Z \in (Y L Z))$
65	62 63 64	3anbi123d	$⊢ a = Y L Z \to ((X \in a \land Y \in a \land Z \in a) \leftrightarrow (X \in (Y L Z) \land Y \in (Y L Z) \land Z \in (Y L Z)))$
66	65	rspcev	$⊢ (Y L Z \in ran L \land (X \in (Y L Z) \land Y \in (Y L Z) \land Z \in (Y L Z))) \to \exists a \in ran L (X \in a \land Y \in a \land Z \in a)$
67	57 51 59 61 66	syl13anc	$⊢ ((φ \land (X \in (Y L Z) \lor Y = Z)) \land Y \neq Z) \to \exists a \in ran L (X \in a \land Y \in a \land Z \in a)$
68	45 67	pm2.61dane	$⊢ (φ \land (X \in (Y L Z) \lor Y = Z)) \to \exists a \in ran L (X \in a \land Y \in a \land Z \in a)$
69		df-ne	$⊢ Y \neq Z \leftrightarrow \neg Y = Z$
70		simplr1	$⊢ (((φ \land a \in ran L) \land (X \in a \land Y \in a \land Z \in a)) \land Y \neq Z) \to X \in a$
71	4	ad3antrrr	$⊢ (((φ \land a \in ran L) \land (X \in a \land Y \in a \land Z \in a)) \land Y \neq Z) \to G \in 𝒢_{Tarski}$
72	6	ad3antrrr	$⊢ (((φ \land a \in ran L) \land (X \in a \land Y \in a \land Z \in a)) \land Y \neq Z) \to Y \in P$
73	7	ad3antrrr	$⊢ (((φ \land a \in ran L) \land (X \in a \land Y \in a \land Z \in a)) \land Y \neq Z) \to Z \in P$
74		simpr	$⊢ (((φ \land a \in ran L) \land (X \in a \land Y \in a \land Z \in a)) \land Y \neq Z) \to Y \neq Z$
75		simpllr	$⊢ (((φ \land a \in ran L) \land (X \in a \land Y \in a \land Z \in a)) \land Y \neq Z) \to a \in ran L$
76		simplr2	$⊢ (((φ \land a \in ran L) \land (X \in a \land Y \in a \land Z \in a)) \land Y \neq Z) \to Y \in a$
77		simplr3	$⊢ (((φ \land a \in ran L) \land (X \in a \land Y \in a \land Z \in a)) \land Y \neq Z) \to Z \in a$
78	1 2 3 71 72 73 74 74 75 76 77	tglinethru	$⊢ (((φ \land a \in ran L) \land (X \in a \land Y \in a \land Z \in a)) \land Y \neq Z) \to a = Y L Z$
79	70 78	eleqtrd	$⊢ (((φ \land a \in ran L) \land (X \in a \land Y \in a \land Z \in a)) \land Y \neq Z) \to X \in (Y L Z)$
80	79	ex	$⊢ ((φ \land a \in ran L) \land (X \in a \land Y \in a \land Z \in a)) \to (Y \neq Z \to X \in (Y L Z))$
81	69 80	biimtrrid	$⊢ ((φ \land a \in ran L) \land (X \in a \land Y \in a \land Z \in a)) \to (\neg Y = Z \to X \in (Y L Z))$
82	81	orrd	$⊢ ((φ \land a \in ran L) \land (X \in a \land Y \in a \land Z \in a)) \to (Y = Z \lor X \in (Y L Z))$
83	82	orcomd	$⊢ ((φ \land a \in ran L) \land (X \in a \land Y \in a \land Z \in a)) \to (X \in (Y L Z) \lor Y = Z)$
84	83	r19.29an	$⊢ (φ \land \exists a \in ran L (X \in a \land Y \in a \land Z \in a)) \to (X \in (Y L Z) \lor Y = Z)$
85	68 84	impbida	$⊢ φ \to ((X \in (Y L Z) \lor Y = Z) \leftrightarrow \exists a \in ran L (X \in a \land Y \in a \land Z \in a))$

Metamath Proof Explorer

Theorem colline

Proof