{{interfaces | imports = Interface:Midpoint | exports = Interface:Orthogonality 1 }}
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>
Here we prove results involving perpendicular lines. This also enables us to prove the existence of the midpoint of a line segment.
We import the theorems of propositional logic and predicate logic, and the geometry results so far and define some variables:
thumb|right Our treatment of perpendicularity, on the page and following ones, is in terms of three related concepts. First is the perpendicularity of a line segment and another line segment which share an endpoint, in this diagram whether A B is perpendicular to B C. The second is whether a line segment is perpendicular to another line segment at a given point, for example whether A B is perpendicular to C D (or whether they are perpendicular if A B is specified by A and another point, not shown, on the line A B). The third is similar, but just whether there is a point where the two lines are perpendicular, without needing to mention that point explicitly.
We start with the first of those, a predicate which can be thought of as recognizing whether A B is perpendicular to B C{{{. We call it {{{is-right-angle even though it is not tied to any larger theory of angles (that will come later).<ref>Definition Per in Narboux</ref> The definition can be read as "∠ A B C is a right angle iff the symmetric point of C around B is as far from A as C is".
As usual, we'll need to restate the definition as a theorem.
{{cleanup|moving applyCongruenceTransitivityInConsequent to where we define CongruenceTransitivity}}
Although it isn't obvious from the definition, the roles of the two points which aren't the vertex are equivalent.<ref>l8_2 in Narboux</ref> To prove this, expand is-right-angle A B C according to the definition into ∃ c′ (B is-midpoint-of C c′ ∧ A C ≡ A c′). Then let a′ be the symmetric point of A around B. Since reflecting through a point preserves distances (SymmetricPointDistance), A c′ ≡ a′ C. This allows us to show is-right-angle C B A by the definition.
Given a right angle A B C where A B is a line (that is, A ≠ B), picking a different point A′ on the line A B also produces a right angle A′ B C.<ref>l8_3 in Narboux</ref>
Reflecting one of the points of a right angle through the vertex of that angle produces a right angle. In symbols, is-right-angle A B C ∧ B is-midpoint-of C C′ → is-right-angle A B C′.<ref>l8_4 in Narboux</ref>.
The proof will start by expanding the definition of is-right-angle into ∃ c″ (B is-midpoint-of C c″ ∧ A C ≡ A c″). Then the result of reflecting C through B{{{ is unique, so {{{C″ = C′, which is our first lemma.
In defining is-right-angle we also encompassed degenerate cases, in this case where the vertex and one point defining a leg are the same.<ref>l8_5 in Narboux</ref>
There are a few cases which imply we are dealing with a degenerate is-right-angle. Here's one in which the point defining one leg is between two points which both lie on the perpendicular. Specifically, is-right-angle A B C ∧ is-right-angle A′ B C ∧ between A C A′ → B = C.<ref>l8_6 in Narboux</ref>
The proof first expands both occurrences of is-right-angle according to the definition to get points c′ and c″ for which (B is-midpoint-of C c′ ∧ A C ≡ A c′) ∧ (B is-midpoint-of C c″ ∧ A′ C ≡ A′ c″) ∧ between A C A′.
Then we apply SymmetricPointDistance to get C′ C″ ≡ C C, which in turn implies C′ = C″.
From here we get B is-midpoint-of C C by substituting C for C′, which in turn implies B = C.
We prove the builder for is-right-angle similarly to other builders: by applying builders for each of the expressions which make up the definition.<ref>not in Narboux</ref>
We now export to Interface:Orthogonality 1.
<references/>
{{DEFAULTSORT:{{PAGENAME}}}} Category:Euclidean geometries (general) and generalizations Category:Foundations of classical theories (including reverse mathematics)