# Metamath Proof Explorer

## Theorem 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}={\mathrm{Base}}_{{G}}$
tglineintmo.i ${⊢}{I}=\mathrm{Itv}\left({G}\right)$
tglineintmo.l ${⊢}{L}={Line}_{𝒢}\left({G}\right)$
tglineintmo.g ${⊢}{\phi }\to {G}\in {𝒢}_{\mathrm{Tarski}}$
colline.1 ${⊢}{\phi }\to {X}\in {P}$
colline.2 ${⊢}{\phi }\to {Y}\in {P}$
colline.3 ${⊢}{\phi }\to {Z}\in {P}$
colline.4 ${⊢}{\phi }\to 2\le \left|{P}\right|$
Assertion colline ${⊢}{\phi }\to \left(\left({X}\in \left({Y}{L}{Z}\right)\vee {Y}={Z}\right)↔\exists {a}\in \mathrm{ran}{L}\phantom{\rule{.4em}{0ex}}\left({X}\in {a}\wedge {Y}\in {a}\wedge {Z}\in {a}\right)\right)$

### Proof

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