Home | Metamath
Proof Explorer Theorem List (p. 256 of 426) | < Previous Next > |
Browser slow? Try the
Unicode version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | Metamath Proof Explorer
(1-27775) |
Hilbert Space Explorer
(27776-29300) |
Users' Mathboxes
(29301-42551) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | hlne2 25501 | The half-line relation implies inequality. (Contributed by Thierry Arnoux, 22-Feb-2020.) |
Itv hlG | ||
Theorem | hlln 25502 | The half-line relation implies colinearity, part of Theorem 6.4 of [Schwabhauser] p. 44. (Contributed by Thierry Arnoux, 22-Feb-2020.) |
Itv hlG TarskiG LineG | ||
Theorem | hleqnid 25503 | The endpoint does not belong to the half-line. (Contributed by Thierry Arnoux, 3-Mar-2020.) |
Itv hlG TarskiG | ||
Theorem | hlid 25504 | The half-line relation is reflexive. Theorem 6.5 of [Schwabhauser] p. 44. (Contributed by Thierry Arnoux, 21-Feb-2020.) |
Itv hlG TarskiG | ||
Theorem | hltr 25505 | The half-line relation is transitive. Theorem 6.7 of [Schwabhauser] p. 44. (Contributed by Thierry Arnoux, 23-Feb-2020.) |
Itv hlG TarskiG | ||
Theorem | hlbtwn 25506 | Betweenness is a sufficient condition to swap half-lines. (Contributed by Thierry Arnoux, 21-Feb-2020.) |
Itv hlG TarskiG | ||
Theorem | btwnhl1 25507 | Deduce half-line from betweenness. (Contributed by Thierry Arnoux, 4-Mar-2020.) |
Itv hlG TarskiG | ||
Theorem | btwnhl2 25508 | Deduce half-line from betweenness. (Contributed by Thierry Arnoux, 4-Mar-2020.) |
Itv hlG TarskiG | ||
Theorem | btwnhl 25509 | Swap betweenness for a half-line. (Contributed by Thierry Arnoux, 2-Mar-2020.) |
Itv hlG TarskiG | ||
Theorem | lnhl 25510 | Either a point on the line AB is on the same side as or on the opposite side. (Contributed by Thierry Arnoux, 21-Sep-2020.) |
Itv hlG TarskiG LineG | ||
Theorem | hlcgrex 25511* | Construct a point on a half-line, at a given distance of its origin. (Contributed by Thierry Arnoux, 1-Aug-2020.) |
Itv hlG TarskiG | ||
Theorem | hlcgreulem 25512 | Lemma for hlcgreu 25513. (Contributed by Thierry Arnoux, 9-Aug-2020.) |
Itv hlG TarskiG | ||
Theorem | hlcgreu 25513* | The point constructed in hlcgrex 25511 is unique. Theorem 6.11 of [Schwabhauser] p. 44. (Contributed by Thierry Arnoux, 9-Aug-2020.) |
Itv hlG TarskiG | ||
Theorem | btwnlng1 25514 | Betweenness implies colinearity. (Contributed by Thierry Arnoux, 28-Mar-2019.) |
Itv LineG TarskiG | ||
Theorem | btwnlng2 25515 | Betweenness implies colinearity. (Contributed by Thierry Arnoux, 28-Mar-2019.) |
Itv LineG TarskiG | ||
Theorem | btwnlng3 25516 | Betweenness implies colinearity. (Contributed by Thierry Arnoux, 28-Mar-2019.) |
Itv LineG TarskiG | ||
Theorem | lncom 25517 | Swapping the points defining a line keeps it unchanged. Part of Theorem 4.11 of [Schwabhauser] p. 34. (Contributed by Thierry Arnoux, 3-Apr-2019.) |
Itv LineG TarskiG | ||
Theorem | lnrot1 25518 | Rotating the points defining a line. Part of Theorem 4.11 of [Schwabhauser] p. 34. (Contributed by Thierry Arnoux, 3-Apr-2019.) |
Itv LineG TarskiG | ||
Theorem | lnrot2 25519 | Rotating the points defining a line. Part of Theorem 4.11 of [Schwabhauser] p. 34. (Contributed by Thierry Arnoux, 3-Apr-2019.) |
Itv LineG TarskiG | ||
Theorem | ncolne1 25520 | Non-colinear points are different. (Contributed by Thierry Arnoux, 8-Aug-2019.) |
Itv LineG TarskiG | ||
Theorem | ncolne2 25521 | Non-colinear points are different. (Contributed by Thierry Arnoux, 8-Aug-2019.) TODO (NM): maybe ncolne2 25521 could be simplified out and deleted, replaced by ncolcom 25456. |
Itv LineG TarskiG | ||
Theorem | tgisline 25522* | The property of being a proper line, generated by two distinct points. (Contributed by Thierry Arnoux, 25-May-2019.) |
Itv LineG TarskiG | ||
Theorem | tglnne 25523 | It takes two different points to form a line. (Contributed by Thierry Arnoux, 27-Nov-2019.) |
Itv LineG TarskiG | ||
Theorem | tglndim0 25524 | There are no lines in dimension 0. (Contributed by Thierry Arnoux, 18-Oct-2019.) |
Itv LineG TarskiG | ||
Theorem | tgelrnln 25525 | The property of being a proper line, generated by two distinct points. (Contributed by Thierry Arnoux, 25-May-2019.) |
Itv LineG TarskiG | ||
Theorem | tglineeltr 25526 | Transitivity law for lines, one half of tglineelsb2 25527. (Contributed by Thierry Arnoux, 25-May-2019.) |
Itv LineG TarskiG | ||
Theorem | tglineelsb2 25527 | If lies on PQ , then PQ = PS . Theorem 6.16 of [Schwabhauser] p. 45. (Contributed by Thierry Arnoux, 17-May-2019.) |
Itv LineG TarskiG | ||
Theorem | tglinerflx1 25528 | Reflexivity law for line membership. Part of theorem 6.17 of [Schwabhauser] p. 45. (Contributed by Thierry Arnoux, 17-May-2019.) |
Itv LineG TarskiG | ||
Theorem | tglinerflx2 25529 | Reflexivity law for line membership. Part of theorem 6.17 of [Schwabhauser] p. 45. (Contributed by Thierry Arnoux, 17-May-2019.) |
Itv LineG TarskiG | ||
Theorem | tglinecom 25530 | Commutativity law for lines. Part of theorem 6.17 of [Schwabhauser] p. 45. (Contributed by Thierry Arnoux, 17-May-2019.) |
Itv LineG TarskiG | ||
Theorem | tglinethru 25531 | If is a line containing two distinct points and , then is the line through and . Theorem 6.18 of [Schwabhauser] p. 45. (Contributed by Thierry Arnoux, 25-May-2019.) |
Itv LineG TarskiG | ||
Theorem | tghilberti1 25532* | There is a line through any two distinct points. Hilbert's axiom I.1 for geometry. (Contributed by Thierry Arnoux, 25-May-2019.) |
Itv LineG TarskiG | ||
Theorem | tghilberti2 25533* | There is at most one line through any two distinct points. Hilbert's axiom I.2 for geometry. (Contributed by Thierry Arnoux, 25-May-2019.) |
Itv LineG TarskiG | ||
Theorem | tglinethrueu 25534* | There is a unique line going through any two distinct points. Theorem 6.19 of [Schwabhauser] p. 46. (Contributed by Thierry Arnoux, 25-May-2019.) |
Itv LineG TarskiG | ||
Theorem | tglnne0 25535 | A line has at least one point. (Contributed by Thierry Arnoux, 4-Mar-2020.) |
LineG TarskiG | ||
Theorem | tglnpt2 25536* | Find a second point on a line. (Contributed by Thierry Arnoux, 18-Oct-2019.) |
Itv LineG TarskiG | ||
Theorem | tglineintmo 25537* | Two distinct lines intersect in at most one point. Theorem 6.21 of [Schwabhauser] p. 46. (Contributed by Thierry Arnoux, 25-May-2019.) |
Itv LineG TarskiG | ||
Theorem | tglineineq 25538 | Two distinct lines intersect in at most one point, variation. Theorem 6.21 of [Schwabhauser] p. 46. (Contributed by Thierry Arnoux, 6-Aug-2019.) |
Itv LineG TarskiG | ||
Theorem | tglineneq 25539 | Given three non-colinear points, build two different lines. (Contributed by Thierry Arnoux, 6-Aug-2019.) |
Itv LineG TarskiG | ||
Theorem | tglineinteq 25540 | Two distinct lines intersect in at most one point. Theorem 6.21 of [Schwabhauser] p. 46. (Contributed by Thierry Arnoux, 6-Aug-2019.) |
Itv LineG TarskiG | ||
Theorem | ncolncol 25541 | Deduce non-colinearity from non-colinearity and colinearity. (Contributed by Thierry Arnoux, 27-Aug-2019.) |
Itv LineG TarskiG | ||
Theorem | coltr 25542 | A transitivity law for colinearity. (Contributed by Thierry Arnoux, 27-Nov-2019.) |
Itv LineG TarskiG | ||
Theorem | coltr3 25543 | A transitivity law for colinearity. (Contributed by Thierry Arnoux, 27-Nov-2019.) |
Itv LineG TarskiG | ||
Theorem | colline 25544* | Three points are colinear iff there is a line through all three of them. Theorem 6.23 of [Schwabhauser] p. 46. (Contributed by Thierry Arnoux, 28-May-2019.) |
Itv LineG TarskiG | ||
Theorem | tglowdim2l 25545* | Reformulation of the lower dimension axiom for dimension 2. There exist three non colinear points. Theorem 6.24 of [Schwabhauser] p. 46. (Contributed by Thierry Arnoux, 30-May-2019.) |
Itv LineG TarskiG DimTarskiG≥ | ||
Theorem | tglowdim2ln 25546* | There is always one point outside of any line. Theorem 6.25 of [Schwabhauser] p. 46. (Contributed by Thierry Arnoux, 16-Nov-2019.) |
Itv LineG TarskiG DimTarskiG≥ | ||
Syntax | cmir 25547 | Declare the constant for the point inversion function. |
pInvG | ||
Definition | df-mir 25548* | Define the point inversion ("mirror") function. Definition 7.5 of [Schwabhauser] p. 49. See mirval 25550 and ismir 25554. (Contributed by Thierry Arnoux, 30-May-2019.) |
pInvG Itv | ||
Theorem | mirreu3 25549* | Existential uniqueness of the mirror point. Theorem 7.8 of [Schwabhauser] p. 49. (Contributed by Thierry Arnoux, 30-May-2019.) |
Itv TarskiG | ||
Theorem | mirval 25550* | Value of the point inversion function . Definition 7.5 of [Schwabhauser] p. 49. (Contributed by Thierry Arnoux, 30-May-2019.) |
Itv LineG pInvG TarskiG | ||
Theorem | mirfv 25551* | Value of the point inversion function . Definition 7.5 of [Schwabhauser] p. 49. (Contributed by Thierry Arnoux, 30-May-2019.) |
Itv LineG pInvG TarskiG | ||
Theorem | mircgr 25552 | Property of the image by the point inversion function. Definition 7.5 of [Schwabhauser] p. 49. (Contributed by Thierry Arnoux, 3-Jun-2019.) |
Itv LineG pInvG TarskiG | ||
Theorem | mirbtwn 25553 | Property of the image by the point inversion function. Definition 7.5 of [Schwabhauser] p. 49. (Contributed by Thierry Arnoux, 3-Jun-2019.) |
Itv LineG pInvG TarskiG | ||
Theorem | ismir 25554 | Property of the image by the point inversion function. Definition 7.5 of [Schwabhauser] p. 49. (Contributed by Thierry Arnoux, 3-Jun-2019.) |
Itv LineG pInvG TarskiG | ||
Theorem | mirf 25555 | Point inversion as function. (Contributed by Thierry Arnoux, 30-May-2019.) |
Itv LineG pInvG TarskiG | ||
Theorem | mircl 25556 | Closure of the point inversion function. (Contributed by Thierry Arnoux, 20-Oct-2019.) |
Itv LineG pInvG TarskiG | ||
Theorem | mirmir 25557 | The point inversion function is an involution. Theorem 7.7 of [Schwabhauser] p. 49. (Contributed by Thierry Arnoux, 3-Jun-2019.) |
Itv LineG pInvG TarskiG | ||
Theorem | mircom 25558 | Variation on mirmir 25557. (Contributed by Thierry Arnoux, 10-Nov-2019.) |
Itv LineG pInvG TarskiG | ||
Theorem | mirreu 25559* | Any point has a unique antecedent through point inversion. Theorem 7.8 of [Schwabhauser] p. 50. (Contributed by Thierry Arnoux, 3-Jun-2019.) |
Itv LineG pInvG TarskiG | ||
Theorem | mireq 25560 | Equality deduction for point inversion. Theorem 7.9 of [Schwabhauser] p. 50. (Contributed by Thierry Arnoux, 30-May-2019.) |
Itv LineG pInvG TarskiG | ||
Theorem | mirinv 25561 | The only invariant point of a point inversion Theorem 7.3 of [Schwabhauser] p. 49, Theorem 7.10 of [Schwabhauser] p. 50. (Contributed by Thierry Arnoux, 30-Jul-2019.) |
Itv LineG pInvG TarskiG | ||
Theorem | mirne 25562 | Mirror of non-center point cannot be the center point. (Contributed by Thierry Arnoux, 27-Sep-2020.) |
Itv LineG pInvG TarskiG | ||
Theorem | mircinv 25563 | The center point is invariant of a point inversion. (Contributed by Thierry Arnoux, 25-Aug-2019.) |
Itv LineG pInvG TarskiG | ||
Theorem | mirf1o 25564 | The point inversion function is a bijection. Theorem 7.11 of [Schwabhauser] p. 50. (Contributed by Thierry Arnoux, 6-Jun-2019.) |
Itv LineG pInvG TarskiG | ||
Theorem | miriso 25565 | The point inversion function is an isometry, i.e. it is conserves congruence. Because it is also a bijection, it is also a motion. Theorem 7.13 of [Schwabhauser] p. 50. (Contributed by Thierry Arnoux, 6-Jun-2019.) |
Itv LineG pInvG TarskiG | ||
Theorem | mirbtwni 25566 | Point inversion preserves betweenness, first half of Theorem 7.15 of [Schwabhauser] p. 51. (Contributed by Thierry Arnoux, 9-Jun-2019.) |
Itv LineG pInvG TarskiG | ||
Theorem | mirbtwnb 25567 | Point inversion preserves betweenness. Theorem 7.15 of [Schwabhauser] p. 51. (Contributed by Thierry Arnoux, 9-Jun-2019.) |
Itv LineG pInvG TarskiG | ||
Theorem | mircgrs 25568 | Point inversion preserves congruence. Theorem 7.16 of [Schwabhauser] p. 51. (Contributed by Thierry Arnoux, 30-Jul-2019.) |
Itv LineG pInvG TarskiG | ||
Theorem | mirmir2 25569 | Point inversion of a point inversion through another point. (Contributed by Thierry Arnoux, 3-Nov-2019.) |
Itv LineG pInvG TarskiG | ||
Theorem | mirmot 25570 | Point investion is a motion of the geometric space. Theorem 7.14 of [Schwabhauser] p. 51. (Contributed by Thierry Arnoux, 15-Dec-2019.) |
Itv LineG pInvG TarskiG Ismt | ||
Theorem | mirln 25571 | If two points are on the same line, so is the mirror point of one through the other. (Contributed by Thierry Arnoux, 21-Dec-2019.) |
Itv LineG pInvG TarskiG | ||
Theorem | mirln2 25572 | If a point and its mirror point are both on the same line, so is the center of the point inversion. (Contributed by Thierry Arnoux, 3-Mar-2020.) |
Itv LineG pInvG TarskiG | ||
Theorem | mirconn 25573 | Point inversion of connectedness. (Contributed by Thierry Arnoux, 2-Mar-2020.) |
Itv LineG pInvG TarskiG | ||
Theorem | mirhl 25574 | If two points and are on the same half-line from , the same applies to the mirror points. (Contributed by Thierry Arnoux, 21-Feb-2020.) |
Itv LineG pInvG TarskiG hlG | ||
Theorem | mirbtwnhl 25575 | If the center of the point inversion is between two points and , then the half lines are mirrored. (Contributed by Thierry Arnoux, 3-Mar-2020.) |
Itv LineG pInvG TarskiG hlG | ||
Theorem | mirhl2 25576 | Deduce half-line relation from mirror point. (Contributed by Thierry Arnoux, 8-Aug-2020.) |
Itv LineG pInvG TarskiG hlG | ||
Theorem | mircgrextend 25577 | Link congruence over a pair of mirror points. cf tgcgrextend 25380. (Contributed by Thierry Arnoux, 4-Oct-2020.) |
Itv LineG pInvG TarskiG cgrG | ||
Theorem | mirtrcgr 25578 | Point inversion of one point of a triangle around another point preserves triangle congruence. (Contributed by Thierry Arnoux, 4-Oct-2020.) |
Itv LineG pInvG TarskiG cgrG | ||
Theorem | mirauto 25579 | Point inversion preserves point inversion. (Contributed by Thierry Arnoux, 30-Jul-2019.) |
Itv LineG pInvG TarskiG | ||
Theorem | miduniq 25580 | Unicity of the middle point, expressed with point inversion. Theorem 7.17 of [Schwabhauser] p. 51. (Contributed by Thierry Arnoux, 30-Jul-2019.) |
Itv LineG pInvG TarskiG | ||
Theorem | miduniq1 25581 | Unicity of the middle point, expressed with point inversion. Theorem 7.18 of [Schwabhauser] p. 52. (Contributed by Thierry Arnoux, 30-Jul-2019.) |
Itv LineG pInvG TarskiG | ||
Theorem | miduniq2 25582 | If two point inversions commute, they are identical. Theorem 7.19 of [Schwabhauser] p. 52. (Contributed by Thierry Arnoux, 30-Jul-2019.) |
Itv LineG pInvG TarskiG | ||
Theorem | colmid 25583 | Colinearity and equidistance implies midpoint. Theorem 7.20 of [Schwabhauser] p. 52. (Contributed by Thierry Arnoux, 30-Jul-2019.) |
Itv LineG pInvG TarskiG | ||
Theorem | symquadlem 25584 | Lemma of the symetrial quadrilateral. The diagonals of quadrilaterals with congruent opposing sides intersect at their middle point. In Euclidean geometry, such quadrilaterals are called parallelograms, as opposing sides are parallel. However, this is not necessarily true in the case of absolute geometry. Lemma 7.21 of [Schwabhauser] p. 52. (Contributed by Thierry Arnoux, 6-Aug-2019.) |
Itv LineG pInvG TarskiG | ||
Theorem | krippenlem 25585 | Lemma for krippen 25586. We can assume krippen.7 "without loss of generality" (Contributed by Thierry Arnoux, 12-Aug-2019.) |
Itv LineG pInvG TarskiG ≤G | ||
Theorem | krippen 25586 | Krippenlemma (German for crib's lemma) Lemma 7.22 of [Schwabhauser] p. 53. proven by Gupta 1965 as Theorem 3.45. (Contributed by Thierry Arnoux, 12-Aug-2019.) |
Itv LineG pInvG TarskiG | ||
Theorem | midexlem 25587* | Lemma for the existence of a middle point. Lemma 7.25 of [Schwabhauser] p. 55. This proof of the existence of a midpoint requires the existence of a third point equidistant to and This condition will be removed later. Because the operation notation midG for a midpoint implies its uniqueness, it cannot be used until uniqueness is proven, and until then, an equivalent mirror point notation has to be used. See mideu 25630 for the existence and uniqueness of the midpoint. (Contributed by Thierry Arnoux, 25-Aug-2019.) |
Itv LineG pInvG TarskiG | ||
Syntax | crag 25588 | Declare the constant for the class of right angles. |
∟G | ||
Definition | df-rag 25589* | Define the class of right angles. Definition 8.1 of [Schwabhauser] p. 57. See israg 25592. (Contributed by Thierry Arnoux, 25-Aug-2019.) |
∟G Word pInvG | ||
Syntax | cperpg 25590 | Declare the constant for the perpendicular relation. |
⟂G | ||
Definition | df-perpg 25591* | Define the "perpendicular" relation. Definition 8.11 of [Schwabhauser] p. 59. See isperp 25607. (Contributed by Thierry Arnoux, 8-Sep-2019.) |
⟂G LineG LineG ∟G | ||
Theorem | israg 25592 | Property for 3 points A, B, C to form a right angle. Definition 8.1 of [Schwabhauser] p. 57. (Contributed by Thierry Arnoux, 25-Aug-2019.) |
Itv LineG pInvG TarskiG ∟G | ||
Theorem | ragcom 25593 | Commutative rule for right angles. Theorem 8.2 of [Schwabhauser] p. 57. (Contributed by Thierry Arnoux, 25-Aug-2019.) |
Itv LineG pInvG TarskiG ∟G ∟G | ||
Theorem | ragcol 25594 | The right angle property is independent of the choice of point on one side. Theorem 8.3 of [Schwabhauser] p. 58. (Contributed by Thierry Arnoux, 25-Aug-2019.) |
Itv LineG pInvG TarskiG ∟G ∟G | ||
Theorem | ragmir 25595 | Right angle property is preserved by point inversion. Theorem 8.4 of [Schwabhauser] p. 58. (Contributed by Thierry Arnoux, 25-Aug-2019.) |
Itv LineG pInvG TarskiG ∟G ∟G | ||
Theorem | mirrag 25596 | Right angle is conserved by point inversion. (Contributed by Thierry Arnoux, 3-Nov-2019.) |
Itv LineG pInvG TarskiG ∟G ∟G | ||
Theorem | ragtrivb 25597 | Trivial right angle. Theorem 8.5 of [Schwabhauser] p. 58. (Contributed by Thierry Arnoux, 25-Aug-2019.) |
Itv LineG pInvG TarskiG ∟G | ||
Theorem | ragflat2 25598 | Deduce equality from two right angles. Theorem 8.6 of [Schwabhauser] p. 58. (Contributed by Thierry Arnoux, 3-Sep-2019.) |
Itv LineG pInvG TarskiG ∟G ∟G | ||
Theorem | ragflat 25599 | Deduce equality from two right angles. Theorem 8.7 of [Schwabhauser] p. 58. (Contributed by Thierry Arnoux, 3-Sep-2019.) |
Itv LineG pInvG TarskiG ∟G ∟G | ||
Theorem | ragtriva 25600 | Trivial right angle. Theorem 8.8 of [Schwabhauser] p. 58. (Contributed by Thierry Arnoux, 3-Sep-2019.) |
Itv LineG pInvG TarskiG ∟G |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |