{{interfaces | imports = Interface:Orthogonality 1 | exports = Interface:Orthogonality 2 }}
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 is one of several involving perpendicular lines. We prove some additional theorems about is-right-angle, and define a predicate saying that lines are perpendicular at a point. A future page will enable 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:
We've proved a number of the results relating to is-right-angle in Orthogonality definitions. Here we pick up a few more (particularly ones for which the automatic expansion of definitions in Orthogonality definitions is inconvenient, and ones which follow from those).
To prove is-right-angle from RightAngle requires that we come up with a point which satisfies the conditions of RightAngle. Here's a theorem which handles the logic involved in going from that point to an expression containing ∃.<ref>not in Narboux, as coq handles this sort of thing</ref>
Another degenerate case is is-right-angle A B C ∧ is-right-angle A C B → B = C.<ref>l8_7 in Narboux</ref>
Let A′ be the symmetric point of A through the point C.
First assume B ≠ C (if not, we are done). Then expand is-right-angle A B C by the definition: ∃ c′ (B is-midpoint-of C c′ ∧ A C ≡ A c′). We also flip is-right-angle A C B to is-right-angle B C A and expand it according to the definition: ∃ a′ (C is-midpoint-of A a′ ∧ B A ≡ B a′).
Now we apply RightAngleLeg to get is-right-angle c′ C A.
We can paraphrase the definition of is-right-angle C′ C A as "the symmetric point of A through C is the same distance from C′ as A is". By symmetric point uniqueness, said symmetric point is just A′. We express this via the "uniqueness lemma", is-right-angle C′ C A ∧ C is-midpoint-of A A′ → C′ A ≡ C′ A′, which we prove after a few lemmas which reflect parts of its proof.
Our next step is A′ C ≡ A′ C′.
Next is is-right-angle A′ B C.
Another degenerate case is is-right-angle A B A → A = B.<ref>l8_8 in Narboux</ref> The proof is that RightAngleVertexLeg gives us is-right-angle A B A ∧ is-right-angle A A B → A = B, but is-right-angle A A B is a theorem, so we are done.
If three points are both perpendicular and collinear, then one of the legs must be an empty line segment.<ref>l8_9 in Narboux</ref>
We'll want this straightforward consequence of RightAngleABB in a moment.
The only reason we rederive this theorem, rather than importing it, is to avoid editing all the interfaces between Betweenness of points and here.
That is, is-right-angle A B C ∧ A B C ≅ A′ B′ C′ → is-right-angle A′ B′ C′.<ref>l8_10 in Narboux</ref>
We start with the B = C case, where we first conclude B′ = C′ and so the conclusion follows from RightAngleABB.
Here's the sketch of the B ≠ C case. Let D be the point we get by expanding the definition of is-right-angle A B C (that is, B is-midpoint-of C D ∧ A C ≡ A D). Let D′ be the symmetric point of C′ through B′. Now we just need A′ C′ ≡ A′ D′. We apply outer five segment with baselines C B D{{{ and {{{C′ B′ D′ and points A and A′, which gives us D A ≡ D′ A′. We have A C ≡ A D from the construction of D and A′ C′ ≡ A C from A B C ≅ A′ B′ C′. So by transitivity, we have A′ C′ ≡ A′ D′ which is what we needed.
It will be most convenient to start with the construction of D and D′. First we construct D by expanding the definition of is-right-angle and moving terms inside the quantifier.
Next we construct D′ as the symmetric point of C′ through B′.
Having constructed our points, we can get going, starting with B′ ≠ C′, which follows from B ≠ C and A B C ≅ A′ B′ C′.
Next is outer five segment with baselines C B D{{{ and {{{C′ B′ D′ and points A and A′, to get D A ≡ D′ A′.
Now we apply transitivity on some line segment congruences which we already have to get A′ C′ ≡ A′ D′.
That's all the major pieces of is-right-angle A′ B′ C′. We just need to do a bit of assembly.
The line A B is perpendicular to the line C D at the point X if that point lies on both lines and if choosing one point from each line plus the vertex X always produces a right angle. In symbols, A B C D ⟂at X is defined as A ≠ B ∧ C ≠ D ∧ collinear X A B ∧ collinear X C D ∧ ∀ u ∀ v (collinear u A B ∧ collinear v C D → is-right-angle u X v).
As usual, we'll need a theorem form of the definition.
Here we prove A B C D ⟂at X ↔ C D A B ⟂at X.<ref>l8_12 and perp_in_symmetry in Narboux</ref> The concept is pretty simple: expand the definition and apply symmetry to each piece. The only thing which makes this proof a bit long is the number of pieces.
The definition of ⟂at might seem a bit odd, in that it would intuitively appear that one point on each line which forms a right angle would suffice, rather than needing to make an assertion about all points on those lines. In fact, this intuition is correct subject to the condition that the points being chosen on the line do not equal the vertex. In symbols, A ≠ B ∧ C ≠ D ∧ collinear X A B ∧ collinear X C D ∧ ∃ u ∃ v (collinear u A B ∧ collinear v C D ∧ u ≠ X ∧ v ≠ X ∧ is-right-angle u X v) → A B C D ⟂at X.<ref>l8_13_2 in Narboux</ref>
The proof is based on the idea that A, B, u are on a line and we'll also consider an arbitrary point, which we'll call U0, on that line. We'll use RightAngleLeg to turn is-right-angle u X v to is-right-angle U0 X v (and some collinearity transitivity to set up the hypotheses for RightAngleLeg). Then we'll do much the same for C, D, v, and an arbitrary point V0 on the line C D{{{, which will turn {{{is-right-angle v X U0 to is-right-angle V0 X U0. Fortunately, the first half and the similar half are similar enough that we can break it off into a lemma which we'll be able to apply twice.
The lemma is A ≠ B ∧ collinear A B U0 ∧ collinear A B X ∧ collinear A B U ∧ is-right-angle U X V ∧ U ≠ X → is-right-angle U0 X V. In this case, RightAngleLeg is is-right-angle U X V ∧ U ≠ X ∧ collinear X U U0 → is-right-angle U0 X V. The first two hypotheses we have, so the first part of our proof is headed towards collinear X U U0. We'll start by applying collinearity transitivity twice.<ref>based on Narboux's proof of l8_13_2 but streamlined, as Narboux also asserts collinear A X U0 and collinear A U X, which don't seem to be used.</ref>
The first collinearity is collinear B U U0 by transitivity from B ≠ A, collinear B A U and collinear B A U0.
The other collinearity is collinear B U X by transitivity from A ≠ B, collinear A B U and collinear A B X.
At this point we prove collinear X U U0 by considering B = U and B ≠ U cases.
For the B = U case, we first apply transitivity to give collinear B X U0 (from A ≠ B, A B X and A B U0).
The B ≠ U case applies transitivity to B ≠ U, collinear B U U0 and collinear B U X, to give collinear U U0 X.
We're now ready to prove the lemma A ≠ B ∧ collinear A B U0 ∧ collinear A B X ∧ collinear A B U ∧ is-right-angle U X V ∧ U ≠ X → is-right-angle U0 X V. We just need to apply RightAngleLeg which is is-right-angle U X V ∧ U ≠ X ∧ collinear X U U0 → is-right-angle U0 X V.
Now we apply this lemma twice to give A ≠ B ∧ C ≠ D ∧ collinear X A B ∧ collinear X C D ∧ (collinear U A B ∧ collinear V C D ∧ U ≠ X ∧ V ≠ X ∧ is-right-angle U X V) ∧ (collinear U0 A B ∧ collinear V0 C D) → is-right-angle U0 X V0.
The first application of the lemma is A ≠ B ∧ collinear A B U0 ∧ collinear A B X ∧ collinear A B U ∧ is-right-angle U X V ∧ U ≠ X → is-right-angle U0 X V.
Applying the lemma a second time is only slightly more complicated.
Now we need to handle the logic to turn that into our desired theorem.
Narboux doesn't explicitly state the following lemma (apparently his coq tactics cover it), but it states that if lines are perpendicular at a point, they form a right angle there. The proof may seem a bit long, but the idea is simple: expand A B C D ⟂at X according to the definition to get ∀ u ∀ v (collinear u A B ∧ collinear v C D → is-right-angle u X v). Substitute A for u and C for v to get collinear A A B ∧ collinear C C D → is-right-angle A X C, and then detach collinear A A B and collinear C C D as they are theorems.
Equals can be substituted for equals, in the context of ⟂at. Because the definition of ⟂at is long, this proof is kind of long, but it is just a straightforward application of the builders for everything making up the definition of ⟂at.
As with line segment congruence, we use the word ''commutativity'' to refer to exchanging the points within each line (that is, A B C D ⟂at X ↔ B A D C ⟂at X), and the word ''symmetry'' to exchanging the two lines (A B C D ⟂at X ↔ C D A B ⟂at X).
We already proved symmetry, so next is commutativity on the left side.<ref>perp_in_left_commutativity in Narboux</ref> The proof is a straightforward exercise in expanding the definition and then commuting the relevant pieces.
Right commutativity follows from left commutativity and symmetry.<ref>perp_in_right_commutativity in Narboux</ref>
Commutativity follows from left and right commutativity.<ref>perp_in_commutativity in Narboux</ref>
Here we show ¬ A B A B ⟂at X. The proof is by contradiction: A ≠ B from the definition, but A = B will follow from two applications of RightAngleLegItself.<ref>l8_14_1 in Narboux</ref>
We now export to Interface:Orthogonality 2.
Also, since this is currently the last proof module for geometry, we export to Interface:Basic geometry.
<references/>
{{DEFAULTSORT:{{PAGENAME}}}} Category:Euclidean geometries (general) and generalizations Category:Foundations of classical theories (including reverse mathematics)