{{interfaces | imports = Interface:Orthogonality 2 | exports = none yet }}
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 start with some theorems about the ⟂ (is perpendicular) predicate.
We import the theorems of propositional logic and predicate logic, and the geometry results so far and define some variables:
Saying that lines are perpendicular at a point is the main step towards saying those lines are perpendicular. The connection is pretty simple: A B ⟂ C D is defined as ∃ x A B C D ⟂at x.
As usual, we need a theorem corresponding to the definition.
Here we show ¬ A B ⟂ A B. The interesting part of the proof was already done as PerpendicularIrreflexivityAt.<ref>l8_14_1 in Narboux</ref>
That is, A B C D ⟂at X → A B ⟂ C D.<ref>l8_14_2_1a in Narboux</ref>
If two lines are perpendicular at a point, they intersect only at that point. In symbols, A B C D ⟂at X ∧ collinear Y A B ∧ collinear Y C D → X = Y.<ref>l8_14_2_1b in Narboux</ref>
To prove this we first show is-right-angle Y X Y which follows directly from the ∀ p ∀ q (collinear p A B ∧ collinear q C D → is-right-angle p X q) part of PerpendicularAt.
From is-right-angle Y X Y, it is a short step to X = Y.
If two lines are perpendicular and they intersect at a point, they are perpendicular at that point. In symbols, A B ⟂ C D ∧ collinear X A B ∧ collinear X C D → A B C D ⟂at X.<ref>l8_14_2_1b_bis in Narboux</ref>
The proof is a straightforward application of PerpendicularAtUniqueIntersection{{{. We start with a lemma performing a substitution. * #(→ (∧ (∧ (⟂at A B C D Y) (collinear X A B)) (collinear X C D)) (⟂at A B C D X))# ([/general/Orthogonality_3.gh/PerpendicularIntersectionPerpendicularAt-1 | PerpendicularIntersectionPerpendicularAt-1]) * #(→ (∧ (∧ (⟂ A B C D) (collinear X A B)) (collinear X C D)) (⟂at A B C D X))# ([/general/Orthogonality_3.gh/PerpendicularIntersectionPerpendicularAt | PerpendicularIntersectionPerpendicularAt]) === Perpendicular lines which intersect at one point are perpendicular at that point === Here is another theorem which relates being perpendicular to being perpendicular at a point: {{{A B ⟂ C D ∧ ∀ y (collinear y A B ∧ collinear y C D → X = y) → A B C D ⟂at X.<ref>l8_14_2_2 in Narboux</ref>
The proof only relies on PerpendicularAt, the definition of ⟂, and logic. Basically, we expand A B ⟂ C D to A B C D ⟂at X0, use the other hypothesis to conclude X = X0, and then substitute to turn A B C D ⟂at X0 into A B C D ⟂at X.
<references/>
{{DEFAULTSORT:{{PAGENAME}}}} Category:Euclidean geometries (general) and generalizations Category:Foundations of classical theories (including reverse mathematics)