{{interfaces | imports = Interface:Triangle congruence | exports = Interface:Collinearity }}
This is part of a series of modules which prove a variety of geometrical theorems starting with Tarski's axioms for geometry. We follow the formalization of Julien Narboux<ref>The formal proofs are at http://www.lix.polytechnique.fr/Labo/Julien.Narboux/tarski.html Formalization of Tarski's geometry in the Coq proof assistant and are described in Julien Narboux (2007), "http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.158.8614 Mechanical Theorem Proving in Tarski’s Geometry", F. Botana and T. Recio (Eds.): ADG 2006, LNAI 4869, pp. 139–156</ref> which itself closely follows a treatise by Schwabhäuser, Szmielew, and Tarski.<ref>W. Schwabhäuser, W Szmielew, and A. Tarski (1983), ''Metamathematische Methoden in der Geometrie'', ISBN 0387129588</ref>
We import the theorems of propositional logic and predicate logic, and the geometry results so far and define some variables:
To say that three points are collinear is just to say that one of them is between the other two (in any order).<ref>Definition Col in Narboux</ref>
One way to express the "in any order" concept is to provide permutation theorems. The first is rotation: collinear x y z ↔ collinear y z x.<ref>col_permutation_1 and col_permutation_2 in Narboux</ref>
The next permutation swaps the second and third points.<ref>col_permutation_5 in Narboux, biconditionalized</ref>
To swap the first and second points, we rotate and then swap the second and third points.<ref>col_permutation_4 in Narboux, biconditionalized</ref>
To swap the first and third points, we rotate and then swap the first and second points.<ref>col_permutation_3 in Narboux, biconditionalized</ref>
A point is collinear with itself and any second point. That is, collinear A A B, and likewise for any other order of the three points.<ref>col_trivial_1, col_trivial_2, and col_trivial_3 in Narboux</ref>
The analogue to BetweennessDegenerateTriangle also holds for collinearity.<ref>l4_13 in Narboux</ref>
Equals can be substituted for equals in a collinearity.
Given a (degenerate) triangle and a line segment congruent to one of the sides of the triangle, we can construct a second triangle on the line segment which is congruent to the given triangle. Here we prove a degenerate case, in which the points of the given triangle are collinear. In symbols, collinear A B C ∧ A B ≡ A′ B′ → ∃ c′ A B C ≅ A′ B′ c′.<ref>l4_14 in Narboux</ref> This is an analogue to InnerDegenerateTriangle but for collinearity rather than betweenness.
There are three cases, corresponding to the three betweenness predicates which make up the definition of collinear.
The first lemma is basically predicate logic. It enables us to move the two antecedents inside the quantifier.
<gallery> File:Five segment.svg|Outer five segment File:Inner five segment.svg|Inner five segment </gallery> This five segment theorem combines inner and outer five segment. It is A ≠ B ∧ collinear A B C ∧ A B C ≅ A′ B′ C′ ∧ A D ≡ A′ D′ ∧ B D ≡ B′ D′ → C D ≡ C′ D′.<ref>l4_16 in Narboux</ref> The illustrations show the inner and outer cases. A, B, and C correspond to x, y, and z but can be in any order (as long as A and B are the ones with known congruences). D corresponds to u.
We prove the result separately for each of the three betweenness relationships which make up the definition of collinear. Each of those proofs is just a matter of applying either inner or outer five segment, so it is just a matter of rearranging the many conjuncts which make up the antecedent of each theorem. The first bunch of lemmas are for those rearrangements.
thumb|right|EquidistantLine If two given points are equidistant to each of two distinct points on a line, they are equidistant to every point on that line. That is, A ≠ B ∧ collinear A B C ∧ A P ≡ A Q ∧ B P ≡ B Q → C P ≡ C Q.<ref>l4_17 in Narboux</ref>
The proof applies FiveSegment with A B C as the collinear points for both parts and P and Q as the fourth points, respectively.
On a given line, the distance to two distinct points uniquely determines a point. That is, A ≠ B ∧ collinear A B C ∧ A C ≡ A C′ ∧ B C ≡ B C′ → C = C′. We prove this by applying EquidistantLine to the line A B C and the points C and C′, which gives us C C ≡ C C′.<ref>l4_18 in Narboux</ref>
A point on a line segment is uniquely determined by its distance to the two endpoints. That is, between A C B ∧ A C ≡ A C′ ∧ B C ≡ B C′ → C = C′.<ref>l4_19 in Narboux</ref>
We divide the proof into two cases, A = B and A ≠ B.
The A = B case is easy; C also equals A and so A C ≡ A C′ implies C = C′.
The A ≠ B case follows easily from CollinearTwoDistanceUniqueness.
We can now assemble the theorem.
We now export to Interface:Collinearity.
<references/>
{{DEFAULTSORT:{{PAGENAME}}}} Category:Euclidean geometries (general) and generalizations Category:Foundations of classical theories (including reverse mathematics)