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>
This page defines the midpoint of a line segment, proves a few basic midpoint results, and then proves a variety of results concerning reflection through a point (symmetric points).
A point is the midpoint of a line segment if it is between the endpoints and is equidistant from each one.
Whether a point is the midpoint does not depend on the order in which we list the endpoints.<ref>Lemma l7_2 in Narboux</ref> This is easily proved from the corresponding theorems for betweenness and congruence.
The only midpoint of an empty line segment is the endpoint of the line segment.<ref>l7_3 in Narboux</ref>
The endpoint of an empty line segment is a midpoint of that segment.<ref>Lemma l7_3_2 in Narboux</ref>
Point symmetry, or reflection through a point, refers to the process of starting with a single point (which in special cases might be called the origin or the center) and mapping every point to a point directly opposite the given point (at the same distance).
Given a point A, the symmetric point of P through A is a point P′ such that A is-midpoint-of P P′. This point always exists and is unique. We first prove existence.<ref>symmetric_point_construction in Narboux, with the cosmetic change that Narboux interchanges A and P</ref> The proof just applies line segment construction to extend the line segment P A to a point p′ by a distance of P A, or in other words, ∃ p′ (between P A p′ ∧ A p′ ≡ P A).
Uniqueness is A is-midpoint-of P P1 ∧ A is-midpoint-of P P2 → P1 = P2.<ref>symmetric_point_unicity in Narboux, again exchanging A and P</ref> We first consider the P = A case, which is just a matter of applying CongruenceIdentityFromEquality
The P ≠ A case is a straightforward application of SegmentConstructionUniqueness.
Combining the two cases completes the proof of uniqueness.
Reflecting through a point is one to one.<ref>Lemma l7_9 in Narboux</ref>
Reflecting through a point preserves distances. That is, A is-midpoint-of P′ P ∧ A is-midpoint-of Q′ Q → P Q ≡ P′ Q′.<ref>Lemma l7_13 in Narboux</ref>
thumb|right|Proof that reflecting through a point preserves distance The proof is a bit involved, so we'll start with a brief outline. The P = A case is trivial, so henceforth we assume P ≠ A. Starting with the line segment P P′, we extend the two endpoints to points X and X′ (by a distance of Q A in both cases). Then we do something similar: extend both ends of Q Q′ to Y and Y′ by a distance of P A.
The next step is X′ Y′ ≡ Y X, which we get by applying five segment to baselines X A X′ and Y′ A Y and points Y′ and X.
Then we apply inner five segment to baselines Y Q A and Y′ Q′ A and points X and X′, which gives Q X ≡ Q′ X′.
Finally, applying inner five segment to baselines X P A and X′ P′ A and points Q and Q′ yields P Q ≡ P′ Q′, as desired.
We start formalizing this proof with the P = A case. Because A is the midpoint of Q′ Q, we know that Q′ A ≡ Q A, and we can substitute P for A. We can also substitute P′ for A, as A = P′ follows from P = A and P′ A ≡ A P.
To understand the organization of the proof, it is based on the substitution A = P′ ∧ A = P → (Q′ A ≡ Q A ↔ Q′ P′ ≡ Q P).
The first step for the P ≠ A case is to construct the points we will need. The first lemma constructs two points (and we'll be able to use it twice, once for x and x′ and once for y and y′).
thumb|right|X′, P′, A, P, and X are in that order and so are Y′, Q′, A, Q, and Y Visually the diagram makes it clear that the points of each of the two lines are in a certain order: in the one case X′, P′, A, P, and X and in the other case Y′, Q′, A, Q, and Y. To express this formally involves a large number of betweenness formulas, and we now prove a number of them. The first is between A P X, which follows from between P′ A P and between P′ P X.
A similar result is between A Q Y, which follows from between Q′ A Q and between Q′ Q Y.
The next betweenness result is between A Q′ Y′. Unlike the previous two, we need to apply transitivity twice (because of the way we constructed Y′). The first application applies transitivity to between Q′ A Q and between Q′ Q Y to give between Q′ A Y.
The same reasoning applied to the other line gives between A P′ X′. The first application of transitivity is to between P′ A P and between P′ P X and gives between P′ A X.
thumb|right|A X, A Y, A X′, and A Y′ are all congruent From the diagram it should be clear that the line segments A X, A Y, A X′, and A Y′ are all congruent, as they each consist of one line segment congruent to P A plus one congruent to Q A. We formalize this through a series of lemmas which apply the three segment theorem.
We have one more similar congruence, A Y ≡ A Y′, which follows from outer three segment on lines A Q Y and A Q′ Y′.
Other similar congruences can be derived from those by transitivity. Here is A X ≡ A X′
All that seems fairly preparatory, and visually obvious. Now for a more substantial result: X′ Y′ ≡ Y X, which we get by applying outer five segment to baselines X A X′ and Y′ A Y and points Y′ and X. We break some of the antecedents of outer five segment into their own lemmas, and then proceed with outer five segment.
Now it is time to apply inner five segment to baselines Y Q A and Y′ Q′ A and points X and X′, which gives Q X ≡ Q′ X′.
The next step is another application of inner five segment, which proves P Q ≡ P′ Q′. It uses baselines X P A and X′ P′ A and points Q and Q′.
Combining the construction of the points and the proof of P Q ≡ P′ Q′ from those points gives us the P ≠ A case of the proof.
And finally we combine the P = A and P ≠ A cases.
Reflecting through a point preserves betweenness relationships. That is, if a point is between two points and we reflect all three points through a common point A, then the corresponding one symmetric point is between the corresponding two symmetric points. In symbols, A is-midpoint-of P P′ ∧ A is-midpoint-of Q Q′ ∧ A is-midpoint-of R R′ ∧ between P Q R → between P′ Q′ R′.<ref>l7_15 in Narboux</ref>
The proof first applies SymmetricPointDistance to each pair of points to prove the degenerate triangle congruence P Q R ≅ P′ Q′ R′. From there, it is a simple application of BetweennessDegenerateTriangle.
The reflections (through a common point) of congruent line segments are congruent. In symbols, A is-midpoint-of P P′ ∧ A is-midpoint-of Q Q′ ∧ A is-midpoint-of R R′ ∧ A is-midpoint-of S S′ ∧ P Q ≡ R S → P′ Q′ ≡ R′ S′.<ref>l7_16 in Narboux</ref>
The proof is just a matter of applying congruence transitivity to P Q ≡ P′ Q′ and R S ≡ R′ S′, which come from SymmetricPointDistance, and P Q ≡ R S (which we are given).
We now export to Interface:Symmetric point.