![]() |
Metamath
Proof Explorer Theorem List (p. 283 of 481) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | ![]() (1-30640) |
![]() (30641-32163) |
![]() (32164-48040) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | tgcgreqb 28201 | Congruence and equality. (Contributed by Thierry Arnoux, 27-Aug-2019.) |
β’ π = (BaseβπΊ) & β’ β = (distβπΊ) & β’ πΌ = (ItvβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β π· β π) & β’ (π β (π΄ β π΅) = (πΆ β π·)) β β’ (π β (π΄ = π΅ β πΆ = π·)) | ||
Theorem | tgcgreq 28202 | Congruence and equality. (Contributed by Thierry Arnoux, 27-Aug-2019.) |
β’ π = (BaseβπΊ) & β’ β = (distβπΊ) & β’ πΌ = (ItvβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β π· β π) & β’ (π β (π΄ β π΅) = (πΆ β π·)) & β’ (π β π΄ = π΅) β β’ (π β πΆ = π·) | ||
Theorem | tgcgrneq 28203 | Congruence and equality. (Contributed by Thierry Arnoux, 27-Aug-2019.) |
β’ π = (BaseβπΊ) & β’ β = (distβπΊ) & β’ πΌ = (ItvβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β π· β π) & β’ (π β (π΄ β π΅) = (πΆ β π·)) & β’ (π β π΄ β π΅) β β’ (π β πΆ β π·) | ||
Theorem | tgcgrtriv 28204 | Degenerate segments are congruent. Theorem 2.8 of [Schwabhauser] p. 28. (Contributed by Thierry Arnoux, 23-Mar-2019.) |
β’ π = (BaseβπΊ) & β’ β = (distβπΊ) & β’ πΌ = (ItvβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β π΄ β π) & β’ (π β π΅ β π) β β’ (π β (π΄ β π΄) = (π΅ β π΅)) | ||
Theorem | tgcgrextend 28205 | Link congruence over a pair of line segments. Theorem 2.11 of [Schwabhauser] p. 29. (Contributed by Thierry Arnoux, 23-Mar-2019.) (Shortened by David A. Wheeler and Thierry Arnoux, 22-Apr-2020.) |
β’ π = (BaseβπΊ) & β’ β = (distβπΊ) & β’ πΌ = (ItvβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β π· β π) & β’ (π β πΈ β π) & β’ (π β πΉ β π) & β’ (π β π΅ β (π΄πΌπΆ)) & β’ (π β πΈ β (π·πΌπΉ)) & β’ (π β (π΄ β π΅) = (π· β πΈ)) & β’ (π β (π΅ β πΆ) = (πΈ β πΉ)) β β’ (π β (π΄ β πΆ) = (π· β πΉ)) | ||
Theorem | tgsegconeq 28206 | Two points that satisfy the conclusion of axtgsegcon 28184 are identical. Uniqueness portion of Theorem 2.12 of [Schwabhauser] p. 29. (Contributed by Thierry Arnoux, 23-Mar-2019.) |
β’ π = (BaseβπΊ) & β’ β = (distβπΊ) & β’ πΌ = (ItvβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β π· β π) & β’ (π β πΈ β π) & β’ (π β πΉ β π) & β’ (π β π· β π΄) & β’ (π β π΄ β (π·πΌπΈ)) & β’ (π β π΄ β (π·πΌπΉ)) & β’ (π β (π΄ β πΈ) = (π΅ β πΆ)) & β’ (π β (π΄ β πΉ) = (π΅ β πΆ)) β β’ (π β πΈ = πΉ) | ||
Theorem | tgbtwntriv2 28207 | Betweenness always holds for the second endpoint. Theorem 3.1 of [Schwabhauser] p. 30. (Contributed by Thierry Arnoux, 15-Mar-2019.) |
β’ π = (BaseβπΊ) & β’ β = (distβπΊ) & β’ πΌ = (ItvβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β π΄ β π) & β’ (π β π΅ β π) β β’ (π β π΅ β (π΄πΌπ΅)) | ||
Theorem | tgbtwncom 28208 | Betweenness commutes. Theorem 3.2 of [Schwabhauser] p. 30. (Contributed by Thierry Arnoux, 15-Mar-2019.) |
β’ π = (BaseβπΊ) & β’ β = (distβπΊ) & β’ πΌ = (ItvβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β π΅ β (π΄πΌπΆ)) β β’ (π β π΅ β (πΆπΌπ΄)) | ||
Theorem | tgbtwncomb 28209 | Betweenness commutes, biconditional version. (Contributed by Thierry Arnoux, 3-Apr-2019.) |
β’ π = (BaseβπΊ) & β’ β = (distβπΊ) & β’ πΌ = (ItvβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) β β’ (π β (π΅ β (π΄πΌπΆ) β π΅ β (πΆπΌπ΄))) | ||
Theorem | tgbtwnne 28210 | Betweenness and inequality. (Contributed by Thierry Arnoux, 1-Dec-2019.) |
β’ π = (BaseβπΊ) & β’ β = (distβπΊ) & β’ πΌ = (ItvβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β π΅ β (π΄πΌπΆ)) & β’ (π β π΅ β π΄) β β’ (π β π΄ β πΆ) | ||
Theorem | tgbtwntriv1 28211 | Betweenness always holds for the first endpoint. Theorem 3.3 of [Schwabhauser] p. 30. (Contributed by Thierry Arnoux, 15-Mar-2019.) |
β’ π = (BaseβπΊ) & β’ β = (distβπΊ) & β’ πΌ = (ItvβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β π΄ β π) & β’ (π β π΅ β π) β β’ (π β π΄ β (π΄πΌπ΅)) | ||
Theorem | tgbtwnswapid 28212 | If you can swap the first two arguments of a betweenness statement, then those arguments are identical. Theorem 3.4 of [Schwabhauser] p. 30. (Contributed by Thierry Arnoux, 16-Mar-2019.) |
β’ π = (BaseβπΊ) & β’ β = (distβπΊ) & β’ πΌ = (ItvβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β π΄ β (π΅πΌπΆ)) & β’ (π β π΅ β (π΄πΌπΆ)) β β’ (π β π΄ = π΅) | ||
Theorem | tgbtwnintr 28213 | Inner transitivity law for betweenness. Left-hand side of Theorem 3.5 of [Schwabhauser] p. 30. (Contributed by Thierry Arnoux, 18-Mar-2019.) |
β’ π = (BaseβπΊ) & β’ β = (distβπΊ) & β’ πΌ = (ItvβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β π· β π) & β’ (π β π΄ β (π΅πΌπ·)) & β’ (π β π΅ β (πΆπΌπ·)) β β’ (π β π΅ β (π΄πΌπΆ)) | ||
Theorem | tgbtwnexch3 28214 | Exchange the first endpoint in betweenness. Left-hand side of Theorem 3.6 of [Schwabhauser] p. 30. (Contributed by Thierry Arnoux, 18-Mar-2019.) |
β’ π = (BaseβπΊ) & β’ β = (distβπΊ) & β’ πΌ = (ItvβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β π· β π) & β’ (π β π΅ β (π΄πΌπΆ)) & β’ (π β πΆ β (π΄πΌπ·)) β β’ (π β πΆ β (π΅πΌπ·)) | ||
Theorem | tgbtwnouttr2 28215 | Outer transitivity law for betweenness. Left-hand side of Theorem 3.7 of [Schwabhauser] p. 30. (Contributed by Thierry Arnoux, 18-Mar-2019.) |
β’ π = (BaseβπΊ) & β’ β = (distβπΊ) & β’ πΌ = (ItvβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β π· β π) & β’ (π β π΅ β πΆ) & β’ (π β π΅ β (π΄πΌπΆ)) & β’ (π β πΆ β (π΅πΌπ·)) β β’ (π β πΆ β (π΄πΌπ·)) | ||
Theorem | tgbtwnexch2 28216 | Exchange the outer point of two betweenness statements. Right-hand side of Theorem 3.5 of [Schwabhauser] p. 30. (Contributed by Thierry Arnoux, 23-Mar-2019.) |
β’ π = (BaseβπΊ) & β’ β = (distβπΊ) & β’ πΌ = (ItvβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β π· β π) & β’ (π β π΅ β (π΄πΌπ·)) & β’ (π β πΆ β (π΅πΌπ·)) β β’ (π β πΆ β (π΄πΌπ·)) | ||
Theorem | tgbtwnouttr 28217 | Outer transitivity law for betweenness. Right-hand side of Theorem 3.7 of [Schwabhauser] p. 30. (Contributed by Thierry Arnoux, 23-Mar-2019.) |
β’ π = (BaseβπΊ) & β’ β = (distβπΊ) & β’ πΌ = (ItvβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β π· β π) & β’ (π β π΅ β πΆ) & β’ (π β π΅ β (π΄πΌπΆ)) & β’ (π β πΆ β (π΅πΌπ·)) β β’ (π β π΅ β (π΄πΌπ·)) | ||
Theorem | tgbtwnexch 28218 | Outer transitivity law for betweenness. Right-hand side of Theorem 3.6 of [Schwabhauser] p. 30. (Contributed by Thierry Arnoux, 23-Mar-2019.) |
β’ π = (BaseβπΊ) & β’ β = (distβπΊ) & β’ πΌ = (ItvβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β π· β π) & β’ (π β π΅ β (π΄πΌπΆ)) & β’ (π β πΆ β (π΄πΌπ·)) β β’ (π β π΅ β (π΄πΌπ·)) | ||
Theorem | tgtrisegint 28219* | A line segment between two sides of a triange intersects a segment crossing from the remaining side to the opposite vertex. Theorem 3.17 of [Schwabhauser] p. 33. (Contributed by Thierry Arnoux, 23-Mar-2019.) |
β’ π = (BaseβπΊ) & β’ β = (distβπΊ) & β’ πΌ = (ItvβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β π· β π) & β’ (π β πΈ β π) & β’ (π β πΉ β π) & β’ (π β π΅ β (π΄πΌπΆ)) & β’ (π β πΈ β (π·πΌπΆ)) & β’ (π β πΉ β (π΄πΌπ·)) β β’ (π β βπ β π (π β (πΉπΌπΆ) β§ π β (π΅πΌπΈ))) | ||
Theorem | tglowdim1 28220* | Lower dimension axiom for one dimension. In dimension at least 1, there are at least two distinct points. The condition "the space is of dimension 1 or more" is written here as 2 β€ (β―βπ) to avoid a new definition, but a different convention could be chosen. (Contributed by Thierry Arnoux, 23-Mar-2019.) |
β’ π = (BaseβπΊ) & β’ β = (distβπΊ) & β’ πΌ = (ItvβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β 2 β€ (β―βπ)) β β’ (π β βπ₯ β π βπ¦ β π π₯ β π¦) | ||
Theorem | tglowdim1i 28221* | Lower dimension axiom for one dimension. (Contributed by Thierry Arnoux, 28-May-2019.) |
β’ π = (BaseβπΊ) & β’ β = (distβπΊ) & β’ πΌ = (ItvβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β 2 β€ (β―βπ)) & β’ (π β π β π) β β’ (π β βπ¦ β π π β π¦) | ||
Theorem | tgldimor 28222 | Excluded-middle like statement allowing to treat dimension zero as a special case. (Contributed by Thierry Arnoux, 11-Apr-2019.) |
β’ π = (πΈβπΉ) & β’ (π β π΄ β π) β β’ (π β ((β―βπ) = 1 β¨ 2 β€ (β―βπ))) | ||
Theorem | tgldim0eq 28223 | In dimension zero, any two points are equal. (Contributed by Thierry Arnoux, 11-Apr-2019.) |
β’ π = (πΈβπΉ) & β’ (π β (β―βπ) = 1) & β’ (π β π΄ β π) & β’ (π β π΅ β π) β β’ (π β π΄ = π΅) | ||
Theorem | tgldim0itv 28224 | In dimension zero, any two points are equal. (Contributed by Thierry Arnoux, 12-Apr-2019.) |
β’ π = (BaseβπΊ) & β’ β = (distβπΊ) & β’ πΌ = (ItvβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β (β―βπ) = 1) β β’ (π β π΄ β (π΅πΌπΆ)) | ||
Theorem | tgldim0cgr 28225 | In dimension zero, any two pairs of points are congruent. (Contributed by Thierry Arnoux, 12-Apr-2019.) |
β’ π = (BaseβπΊ) & β’ β = (distβπΊ) & β’ πΌ = (ItvβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β (β―βπ) = 1) & β’ (π β π· β π) β β’ (π β (π΄ β π΅) = (πΆ β π·)) | ||
Theorem | tgbtwndiff 28226* | There is always a π distinct from π΅ such that π΅ lies between π΄ and π. Theorem 3.14 of [Schwabhauser] p. 32. The condition "the space is of dimension 1 or more" is written here as 2 β€ (β―βπ) for simplicity. (Contributed by Thierry Arnoux, 23-Mar-2019.) |
β’ π = (BaseβπΊ) & β’ β = (distβπΊ) & β’ πΌ = (ItvβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β 2 β€ (β―βπ)) β β’ (π β βπ β π (π΅ β (π΄πΌπ) β§ π΅ β π)) | ||
Theorem | tgdim01 28227 | In geometries of dimension less than 2, all points are colinear. (Contributed by Thierry Arnoux, 27-Aug-2019.) |
β’ π = (BaseβπΊ) & β’ πΌ = (ItvβπΊ) & β’ (π β πΊ β π) & β’ (π β Β¬ πΊDimTarskiGβ₯2) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π β π) β β’ (π β (π β (ππΌπ) β¨ π β (ππΌπ) β¨ π β (ππΌπ))) | ||
Theorem | tgifscgr 28228 | Inner five segment congruence. Take two triangles, π΄π·πΆ and πΈπ»πΎ, with π΅ between π΄ and πΆ and πΉ between πΈ and πΎ. If the other components of the triangles are congruent, then so are π΅π· and πΉπ». Theorem 4.2 of [Schwabhauser] p. 34. (Contributed by Thierry Arnoux, 24-Mar-2019.) |
β’ π = (BaseβπΊ) & β’ β = (distβπΊ) & β’ πΌ = (ItvβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β π· β π) & β’ (π β πΈ β π) & β’ (π β πΉ β π) & β’ (π β πΎ β π) & β’ (π β π» β π) & β’ (π β π΅ β (π΄πΌπΆ)) & β’ (π β πΉ β (πΈπΌπΎ)) & β’ (π β (π΄ β πΆ) = (πΈ β πΎ)) & β’ (π β (π΅ β πΆ) = (πΉ β πΎ)) & β’ (π β (π΄ β π·) = (πΈ β π»)) & β’ (π β (πΆ β π·) = (πΎ β π»)) β β’ (π β (π΅ β π·) = (πΉ β π»)) | ||
Theorem | tgcgrsub 28229 | Removing identical parts from the end of a line segment preserves congruence. Theorem 4.3 of [Schwabhauser] p. 35. (Contributed by Thierry Arnoux, 3-Apr-2019.) |
β’ π = (BaseβπΊ) & β’ β = (distβπΊ) & β’ πΌ = (ItvβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β π· β π) & β’ (π β πΈ β π) & β’ (π β πΉ β π) & β’ (π β π΅ β (π΄πΌπΆ)) & β’ (π β πΈ β (π·πΌπΉ)) & β’ (π β (π΄ β πΆ) = (π· β πΉ)) & β’ (π β (π΅ β πΆ) = (πΈ β πΉ)) β β’ (π β (π΄ β π΅) = (π· β πΈ)) | ||
Syntax | ccgrg 28230 | Declare the constant for the congruence between shapes relation. |
class cgrG | ||
Definition | df-cgrg 28231* |
Define the relation of congruence between shapes. Definition 4.4 of
[Schwabhauser] p. 35. A
"shape" is a finite sequence of points, and a
triangle can be represented as a shape with three points. Two shapes
are congruent if all corresponding segments between all corresponding
points are congruent.
Many systems of geometry define triangle congruence as requiring both segment congruence and angle congruence. Such systems, such as Hilbert's axiomatic system, typically have a primitive notion of angle congruence in addition to segment congruence. Here, angle congruence is instead a derived notion, defined later in df-cgra 28528 and expanded in iscgra 28529. This does not mean our system is weaker; dfcgrg2 28583 proves that these two definitions are equivalent, and using the Tarski definition instead (given in [Schwabhauser] p. 35) is simpler. Once two triangles are proven congruent as defined here, you can use various theorems to prove that corresponding parts of congruent triangles are congruent (CPCTC). For example, see cgr3simp1 28240, cgr3simp2 28241, cgr3simp3 28242, cgrcgra 28541, and permutation laws such as cgr3swap12 28243 and dfcgrg2 28583. Ideally, we would define this for functions of any set, but we will use words (see df-word 14462) in most cases. (Contributed by Thierry Arnoux, 3-Apr-2019.) |
β’ cgrG = (π β V β¦ {β¨π, πβ© β£ ((π β ((Baseβπ) βpm β) β§ π β ((Baseβπ) βpm β)) β§ (dom π = dom π β§ βπ β dom πβπ β dom π((πβπ)(distβπ)(πβπ)) = ((πβπ)(distβπ)(πβπ))))}) | ||
Theorem | iscgrg 28232* | The congruence property for sequences of points. (Contributed by Thierry Arnoux, 3-Apr-2019.) |
β’ π = (BaseβπΊ) & β’ β = (distβπΊ) & β’ βΌ = (cgrGβπΊ) β β’ (πΊ β π β (π΄ βΌ π΅ β ((π΄ β (π βpm β) β§ π΅ β (π βpm β)) β§ (dom π΄ = dom π΅ β§ βπ β dom π΄βπ β dom π΄((π΄βπ) β (π΄βπ)) = ((π΅βπ) β (π΅βπ)))))) | ||
Theorem | iscgrgd 28233* | The property for two sequences π΄ and π΅ of points to be congruent. (Contributed by Thierry Arnoux, 3-Apr-2019.) |
β’ π = (BaseβπΊ) & β’ β = (distβπΊ) & β’ βΌ = (cgrGβπΊ) & β’ (π β πΊ β π) & β’ (π β π· β β) & β’ (π β π΄:π·βΆπ) & β’ (π β π΅:π·βΆπ) β β’ (π β (π΄ βΌ π΅ β βπ β dom π΄βπ β dom π΄((π΄βπ) β (π΄βπ)) = ((π΅βπ) β (π΅βπ)))) | ||
Theorem | iscgrglt 28234* | The property for two sequences π΄ and π΅ of points to be congruent, where the congruence is only required for indices verifying a less-than relation. (Contributed by Thierry Arnoux, 7-Oct-2020.) |
β’ π = (BaseβπΊ) & β’ β = (distβπΊ) & β’ βΌ = (cgrGβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β π· β β) & β’ (π β π΄:π·βΆπ) & β’ (π β π΅:π·βΆπ) β β’ (π β (π΄ βΌ π΅ β βπ β dom π΄βπ β dom π΄(π < π β ((π΄βπ) β (π΄βπ)) = ((π΅βπ) β (π΅βπ))))) | ||
Theorem | trgcgrg 28235 | The property for two triangles to be congruent to each other. (Contributed by Thierry Arnoux, 3-Apr-2019.) |
β’ π = (BaseβπΊ) & β’ β = (distβπΊ) & β’ βΌ = (cgrGβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β π· β π) & β’ (π β πΈ β π) & β’ (π β πΉ β π) β β’ (π β (β¨βπ΄π΅πΆββ© βΌ β¨βπ·πΈπΉββ© β ((π΄ β π΅) = (π· β πΈ) β§ (π΅ β πΆ) = (πΈ β πΉ) β§ (πΆ β π΄) = (πΉ β π·)))) | ||
Theorem | trgcgr 28236 | Triangle congruence. (Contributed by Thierry Arnoux, 27-Apr-2019.) |
β’ π = (BaseβπΊ) & β’ β = (distβπΊ) & β’ βΌ = (cgrGβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β π· β π) & β’ (π β πΈ β π) & β’ (π β πΉ β π) & β’ (π β (π΄ β π΅) = (π· β πΈ)) & β’ (π β (π΅ β πΆ) = (πΈ β πΉ)) & β’ (π β (πΆ β π΄) = (πΉ β π·)) β β’ (π β β¨βπ΄π΅πΆββ© βΌ β¨βπ·πΈπΉββ©) | ||
Theorem | ercgrg 28237 | The shape congruence relation is an equivalence relation. Statement 4.4 of [Schwabhauser] p. 35. (Contributed by Thierry Arnoux, 9-Apr-2019.) |
β’ π = (BaseβπΊ) β β’ (πΊ β TarskiG β (cgrGβπΊ) Er (π βpm β)) | ||
Theorem | tgcgrxfr 28238* | A line segment can be divided at the same place as a congruent line segment is divided. Theorem 4.5 of [Schwabhauser] p. 35. (Contributed by Thierry Arnoux, 9-Apr-2019.) |
β’ π = (BaseβπΊ) & β’ β = (distβπΊ) & β’ πΌ = (ItvβπΊ) & β’ βΌ = (cgrGβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β π· β π) & β’ (π β πΉ β π) & β’ (π β π΅ β (π΄πΌπΆ)) & β’ (π β (π΄ β πΆ) = (π· β πΉ)) β β’ (π β βπ β π (π β (π·πΌπΉ) β§ β¨βπ΄π΅πΆββ© βΌ β¨βπ·ππΉββ©)) | ||
Theorem | cgr3id 28239 | Reflexivity law for three-place congruence. (Contributed by Thierry Arnoux, 28-Apr-2019.) |
β’ π = (BaseβπΊ) & β’ β = (distβπΊ) & β’ πΌ = (ItvβπΊ) & β’ βΌ = (cgrGβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) β β’ (π β β¨βπ΄π΅πΆββ© βΌ β¨βπ΄π΅πΆββ©) | ||
Theorem | cgr3simp1 28240 | Deduce segment congruence from a triangle congruence. This is a portion of the theorem that corresponding parts of congruent triangles are congruent (CPCTC), focusing on a specific segment. (Contributed by Thierry Arnoux, 27-Apr-2019.) |
β’ π = (BaseβπΊ) & β’ β = (distβπΊ) & β’ πΌ = (ItvβπΊ) & β’ βΌ = (cgrGβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β π· β π) & β’ (π β πΈ β π) & β’ (π β πΉ β π) & β’ (π β β¨βπ΄π΅πΆββ© βΌ β¨βπ·πΈπΉββ©) β β’ (π β (π΄ β π΅) = (π· β πΈ)) | ||
Theorem | cgr3simp2 28241 | Deduce segment congruence from a triangle congruence. This is a portion of CPCTC, focusing on a specific segment. (Contributed by Thierry Arnoux, 27-Apr-2019.) |
β’ π = (BaseβπΊ) & β’ β = (distβπΊ) & β’ πΌ = (ItvβπΊ) & β’ βΌ = (cgrGβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β π· β π) & β’ (π β πΈ β π) & β’ (π β πΉ β π) & β’ (π β β¨βπ΄π΅πΆββ© βΌ β¨βπ·πΈπΉββ©) β β’ (π β (π΅ β πΆ) = (πΈ β πΉ)) | ||
Theorem | cgr3simp3 28242 | Deduce segment congruence from a triangle congruence. This is a portion of CPCTC, focusing on a specific segment. (Contributed by Thierry Arnoux, 27-Apr-2019.) |
β’ π = (BaseβπΊ) & β’ β = (distβπΊ) & β’ πΌ = (ItvβπΊ) & β’ βΌ = (cgrGβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β π· β π) & β’ (π β πΈ β π) & β’ (π β πΉ β π) & β’ (π β β¨βπ΄π΅πΆββ© βΌ β¨βπ·πΈπΉββ©) β β’ (π β (πΆ β π΄) = (πΉ β π·)) | ||
Theorem | cgr3swap12 28243 | Permutation law for three-place congruence. (Contributed by Thierry Arnoux, 27-Apr-2019.) |
β’ π = (BaseβπΊ) & β’ β = (distβπΊ) & β’ πΌ = (ItvβπΊ) & β’ βΌ = (cgrGβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β π· β π) & β’ (π β πΈ β π) & β’ (π β πΉ β π) & β’ (π β β¨βπ΄π΅πΆββ© βΌ β¨βπ·πΈπΉββ©) β β’ (π β β¨βπ΅π΄πΆββ© βΌ β¨βπΈπ·πΉββ©) | ||
Theorem | cgr3swap23 28244 | Permutation law for three-place congruence. (Contributed by Thierry Arnoux, 27-Apr-2019.) |
β’ π = (BaseβπΊ) & β’ β = (distβπΊ) & β’ πΌ = (ItvβπΊ) & β’ βΌ = (cgrGβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β π· β π) & β’ (π β πΈ β π) & β’ (π β πΉ β π) & β’ (π β β¨βπ΄π΅πΆββ© βΌ β¨βπ·πΈπΉββ©) β β’ (π β β¨βπ΄πΆπ΅ββ© βΌ β¨βπ·πΉπΈββ©) | ||
Theorem | cgr3swap13 28245 | Permutation law for three-place congruence. (Contributed by Thierry Arnoux, 3-Oct-2020.) |
β’ π = (BaseβπΊ) & β’ β = (distβπΊ) & β’ πΌ = (ItvβπΊ) & β’ βΌ = (cgrGβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β π· β π) & β’ (π β πΈ β π) & β’ (π β πΉ β π) & β’ (π β β¨βπ΄π΅πΆββ© βΌ β¨βπ·πΈπΉββ©) β β’ (π β β¨βπΆπ΅π΄ββ© βΌ β¨βπΉπΈπ·ββ©) | ||
Theorem | cgr3rotr 28246 | Permutation law for three-place congruence. (Contributed by Thierry Arnoux, 1-Aug-2020.) |
β’ π = (BaseβπΊ) & β’ β = (distβπΊ) & β’ πΌ = (ItvβπΊ) & β’ βΌ = (cgrGβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β π· β π) & β’ (π β πΈ β π) & β’ (π β πΉ β π) & β’ (π β β¨βπ΄π΅πΆββ© βΌ β¨βπ·πΈπΉββ©) β β’ (π β β¨βπΆπ΄π΅ββ© βΌ β¨βπΉπ·πΈββ©) | ||
Theorem | cgr3rotl 28247 | Permutation law for three-place congruence. (Contributed by Thierry Arnoux, 1-Aug-2020.) |
β’ π = (BaseβπΊ) & β’ β = (distβπΊ) & β’ πΌ = (ItvβπΊ) & β’ βΌ = (cgrGβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β π· β π) & β’ (π β πΈ β π) & β’ (π β πΉ β π) & β’ (π β β¨βπ΄π΅πΆββ© βΌ β¨βπ·πΈπΉββ©) β β’ (π β β¨βπ΅πΆπ΄ββ© βΌ β¨βπΈπΉπ·ββ©) | ||
Theorem | trgcgrcom 28248 | Commutative law for three-place congruence. (Contributed by Thierry Arnoux, 27-Apr-2019.) |
β’ π = (BaseβπΊ) & β’ β = (distβπΊ) & β’ πΌ = (ItvβπΊ) & β’ βΌ = (cgrGβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β π· β π) & β’ (π β πΈ β π) & β’ (π β πΉ β π) & β’ (π β β¨βπ΄π΅πΆββ© βΌ β¨βπ·πΈπΉββ©) β β’ (π β β¨βπ·πΈπΉββ© βΌ β¨βπ΄π΅πΆββ©) | ||
Theorem | cgr3tr 28249 | Transitivity law for three-place congruence. (Contributed by Thierry Arnoux, 27-Apr-2019.) |
β’ π = (BaseβπΊ) & β’ β = (distβπΊ) & β’ πΌ = (ItvβπΊ) & β’ βΌ = (cgrGβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β π· β π) & β’ (π β πΈ β π) & β’ (π β πΉ β π) & β’ (π β β¨βπ΄π΅πΆββ© βΌ β¨βπ·πΈπΉββ©) & β’ (π β π½ β π) & β’ (π β πΎ β π) & β’ (π β πΏ β π) & β’ (π β β¨βπ·πΈπΉββ© βΌ β¨βπ½πΎπΏββ©) β β’ (π β β¨βπ΄π΅πΆββ© βΌ β¨βπ½πΎπΏββ©) | ||
Theorem | tgbtwnxfr 28250 | A condition for extending betweenness to a new set of points based on congruence with another set of points. Theorem 4.6 of [Schwabhauser] p. 36. (Contributed by Thierry Arnoux, 27-Apr-2019.) |
β’ π = (BaseβπΊ) & β’ β = (distβπΊ) & β’ πΌ = (ItvβπΊ) & β’ βΌ = (cgrGβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β π· β π) & β’ (π β πΈ β π) & β’ (π β πΉ β π) & β’ (π β β¨βπ΄π΅πΆββ© βΌ β¨βπ·πΈπΉββ©) & β’ (π β π΅ β (π΄πΌπΆ)) β β’ (π β πΈ β (π·πΌπΉ)) | ||
Theorem | tgcgr4 28251 | Two quadrilaterals to be congruent to each other if one triangle formed by their vertices is, and the additional points are equidistant too. (Contributed by Thierry Arnoux, 8-Oct-2020.) |
β’ π = (BaseβπΊ) & β’ β = (distβπΊ) & β’ πΌ = (ItvβπΊ) & β’ βΌ = (cgrGβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β π· β π) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π β π) β β’ (π β (β¨βπ΄π΅πΆπ·ββ© βΌ β¨βππππββ© β (β¨βπ΄π΅πΆββ© βΌ β¨βπππββ© β§ ((π΄ β π·) = (π β π) β§ (π΅ β π·) = (π β π) β§ (πΆ β π·) = (π β π))))) | ||
Syntax | cismt 28252 | Declare the constant for the isometry builder. |
class Ismt | ||
Definition | df-ismt 28253* | Define the set of isometries between two structures. Definition 4.8 of [Schwabhauser] p. 36. See isismt 28254. (Contributed by Thierry Arnoux, 13-Dec-2019.) |
β’ Ismt = (π β V, β β V β¦ {π β£ (π:(Baseβπ)β1-1-ontoβ(Baseββ) β§ βπ β (Baseβπ)βπ β (Baseβπ)((πβπ)(distββ)(πβπ)) = (π(distβπ)π))}) | ||
Theorem | isismt 28254* | Property of being an isometry. Compare with isismty 37159. (Contributed by Thierry Arnoux, 13-Dec-2019.) |
β’ π΅ = (BaseβπΊ) & β’ π = (Baseβπ») & β’ π· = (distβπΊ) & β’ β = (distβπ») β β’ ((πΊ β π β§ π» β π) β (πΉ β (πΊIsmtπ») β (πΉ:π΅β1-1-ontoβπ β§ βπ β π΅ βπ β π΅ ((πΉβπ) β (πΉβπ)) = (ππ·π)))) | ||
Theorem | ismot 28255* | Property of being an isometry mapping to the same space. In geometry, this is also called a motion. (Contributed by Thierry Arnoux, 15-Dec-2019.) |
β’ π = (BaseβπΊ) & β’ β = (distβπΊ) β β’ (πΊ β π β (πΉ β (πΊIsmtπΊ) β (πΉ:πβ1-1-ontoβπ β§ βπ β π βπ β π ((πΉβπ) β (πΉβπ)) = (π β π)))) | ||
Theorem | motcgr 28256 | Property of a motion: distances are preserved. (Contributed by Thierry Arnoux, 15-Dec-2019.) |
β’ π = (BaseβπΊ) & β’ β = (distβπΊ) & β’ (π β πΊ β π) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΉ β (πΊIsmtπΊ)) β β’ (π β ((πΉβπ΄) β (πΉβπ΅)) = (π΄ β π΅)) | ||
Theorem | idmot 28257 | The identity is a motion. (Contributed by Thierry Arnoux, 15-Dec-2019.) |
β’ π = (BaseβπΊ) & β’ β = (distβπΊ) & β’ (π β πΊ β π) β β’ (π β ( I βΎ π) β (πΊIsmtπΊ)) | ||
Theorem | motf1o 28258 | Motions are bijections. (Contributed by Thierry Arnoux, 15-Dec-2019.) |
β’ π = (BaseβπΊ) & β’ β = (distβπΊ) & β’ (π β πΊ β π) & β’ (π β πΉ β (πΊIsmtπΊ)) β β’ (π β πΉ:πβ1-1-ontoβπ) | ||
Theorem | motcl 28259 | Closure of motions. (Contributed by Thierry Arnoux, 15-Dec-2019.) |
β’ π = (BaseβπΊ) & β’ β = (distβπΊ) & β’ (π β πΊ β π) & β’ (π β πΉ β (πΊIsmtπΊ)) & β’ (π β π΄ β π) β β’ (π β (πΉβπ΄) β π) | ||
Theorem | motco 28260 | The composition of two motions is a motion. (Contributed by Thierry Arnoux, 15-Dec-2019.) |
β’ π = (BaseβπΊ) & β’ β = (distβπΊ) & β’ (π β πΊ β π) & β’ (π β πΉ β (πΊIsmtπΊ)) & β’ (π β π» β (πΊIsmtπΊ)) β β’ (π β (πΉ β π») β (πΊIsmtπΊ)) | ||
Theorem | cnvmot 28261 | The converse of a motion is a motion. (Contributed by Thierry Arnoux, 15-Dec-2019.) |
β’ π = (BaseβπΊ) & β’ β = (distβπΊ) & β’ (π β πΊ β π) & β’ (π β πΉ β (πΊIsmtπΊ)) β β’ (π β β‘πΉ β (πΊIsmtπΊ)) | ||
Theorem | motplusg 28262* | The operation for motions is their composition. (Contributed by Thierry Arnoux, 15-Dec-2019.) |
β’ π = (BaseβπΊ) & β’ β = (distβπΊ) & β’ (π β πΊ β π) & β’ πΌ = {β¨(Baseβndx), (πΊIsmtπΊ)β©, β¨(+gβndx), (π β (πΊIsmtπΊ), π β (πΊIsmtπΊ) β¦ (π β π))β©} & β’ (π β πΉ β (πΊIsmtπΊ)) & β’ (π β π» β (πΊIsmtπΊ)) β β’ (π β (πΉ(+gβπΌ)π») = (πΉ β π»)) | ||
Theorem | motgrp 28263* | The motions of a geometry form a group with respect to function composition, called the Isometry group. (Contributed by Thierry Arnoux, 15-Dec-2019.) |
β’ π = (BaseβπΊ) & β’ β = (distβπΊ) & β’ (π β πΊ β π) & β’ πΌ = {β¨(Baseβndx), (πΊIsmtπΊ)β©, β¨(+gβndx), (π β (πΊIsmtπΊ), π β (πΊIsmtπΊ) β¦ (π β π))β©} β β’ (π β πΌ β Grp) | ||
Theorem | motcgrg 28264* | Property of a motion: distances are preserved. (Contributed by Thierry Arnoux, 15-Dec-2019.) |
β’ π = (BaseβπΊ) & β’ β = (distβπΊ) & β’ (π β πΊ β π) & β’ πΌ = {β¨(Baseβndx), (πΊIsmtπΊ)β©, β¨(+gβndx), (π β (πΊIsmtπΊ), π β (πΊIsmtπΊ) β¦ (π β π))β©} & β’ βΌ = (cgrGβπΊ) & β’ (π β π β Word π) & β’ (π β πΉ β (πΊIsmtπΊ)) β β’ (π β (πΉ β π) βΌ π) | ||
Theorem | motcgr3 28265 | Property of a motion: distances are preserved, special case of triangles. (Contributed by Thierry Arnoux, 15-Dec-2019.) |
β’ π = (BaseβπΊ) & β’ β = (distβπΊ) & β’ βΌ = (cgrGβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β π· = (π»βπ΄)) & β’ (π β πΈ = (π»βπ΅)) & β’ (π β πΉ = (π»βπΆ)) & β’ (π β π» β (πΊIsmtπΊ)) β β’ (π β β¨βπ΄π΅πΆββ© βΌ β¨βπ·πΈπΉββ©) | ||
Theorem | tglng 28266* | Lines of a Tarski Geometry. This relates to both Definition 4.10 of [Schwabhauser] p. 36. and Definition 6.14 of [Schwabhauser] p. 45. (Contributed by Thierry Arnoux, 28-Mar-2019.) |
β’ π = (BaseβπΊ) & β’ πΏ = (LineGβπΊ) & β’ πΌ = (ItvβπΊ) β β’ (πΊ β TarskiG β πΏ = (π₯ β π, π¦ β (π β {π₯}) β¦ {π§ β π β£ (π§ β (π₯πΌπ¦) β¨ π₯ β (π§πΌπ¦) β¨ π¦ β (π₯πΌπ§))})) | ||
Theorem | tglnfn 28267 | Lines as functions. (Contributed by Thierry Arnoux, 25-May-2019.) |
β’ π = (BaseβπΊ) & β’ πΏ = (LineGβπΊ) & β’ πΌ = (ItvβπΊ) β β’ (πΊ β TarskiG β πΏ Fn ((π Γ π) β I )) | ||
Theorem | tglnunirn 28268 | Lines are sets of points. (Contributed by Thierry Arnoux, 25-May-2019.) |
β’ π = (BaseβπΊ) & β’ πΏ = (LineGβπΊ) & β’ πΌ = (ItvβπΊ) β β’ (πΊ β TarskiG β βͺ ran πΏ β π) | ||
Theorem | tglnpt 28269 | Lines are sets of points. (Contributed by Thierry Arnoux, 17-Oct-2019.) |
β’ π = (BaseβπΊ) & β’ πΏ = (LineGβπΊ) & β’ πΌ = (ItvβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β π΄ β ran πΏ) & β’ (π β π β π΄) β β’ (π β π β π) | ||
Theorem | tglngne 28270 | It takes two different points to form a line. (Contributed by Thierry Arnoux, 6-Aug-2019.) |
β’ π = (BaseβπΊ) & β’ πΏ = (LineGβπΊ) & β’ πΌ = (ItvβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π β (ππΏπ)) β β’ (π β π β π) | ||
Theorem | tglngval 28271* | The line going through points π and π. (Contributed by Thierry Arnoux, 28-Mar-2019.) |
β’ π = (BaseβπΊ) & β’ πΏ = (LineGβπΊ) & β’ πΌ = (ItvβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π β π) β β’ (π β (ππΏπ) = {π§ β π β£ (π§ β (ππΌπ) β¨ π β (π§πΌπ) β¨ π β (ππΌπ§))}) | ||
Theorem | tglnssp 28272 | Lines are subset of the geometry base set. That is, lines are sets of points. (Contributed by Thierry Arnoux, 17-May-2019.) |
β’ π = (BaseβπΊ) & β’ πΏ = (LineGβπΊ) & β’ πΌ = (ItvβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π β π) β β’ (π β (ππΏπ) β π) | ||
Theorem | tgellng 28273 | Property of lying on the line going through points π and π. Definition 4.10 of [Schwabhauser] p. 36. We choose the notation π β (π(LineGβπΊ)π) instead of "colinear" because LineG is a common structure slot for other axiomatizations of geometry. (Contributed by Thierry Arnoux, 28-Mar-2019.) |
β’ π = (BaseβπΊ) & β’ πΏ = (LineGβπΊ) & β’ πΌ = (ItvβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π β π) β β’ (π β (π β (ππΏπ) β (π β (ππΌπ) β¨ π β (ππΌπ) β¨ π β (ππΌπ)))) | ||
Theorem | tgcolg 28274 | We choose the notation (π β (ππΏπ) β¨ π = π) instead of "colinear" in order to avoid defining an additional symbol for colinearity because LineG is a common structure slot for other axiomatizations of geometry. (Contributed by Thierry Arnoux, 25-May-2019.) |
β’ π = (BaseβπΊ) & β’ πΏ = (LineGβπΊ) & β’ πΌ = (ItvβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π β π) β β’ (π β ((π β (ππΏπ) β¨ π = π) β (π β (ππΌπ) β¨ π β (ππΌπ) β¨ π β (ππΌπ)))) | ||
Theorem | btwncolg1 28275 | Betweenness implies colinearity. (Contributed by Thierry Arnoux, 28-Mar-2019.) |
β’ π = (BaseβπΊ) & β’ πΏ = (LineGβπΊ) & β’ πΌ = (ItvβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π β (ππΌπ)) β β’ (π β (π β (ππΏπ) β¨ π = π)) | ||
Theorem | btwncolg2 28276 | Betweenness implies colinearity. (Contributed by Thierry Arnoux, 28-Mar-2019.) |
β’ π = (BaseβπΊ) & β’ πΏ = (LineGβπΊ) & β’ πΌ = (ItvβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π β (ππΌπ)) β β’ (π β (π β (ππΏπ) β¨ π = π)) | ||
Theorem | btwncolg3 28277 | Betweenness implies colinearity. (Contributed by Thierry Arnoux, 28-Mar-2019.) |
β’ π = (BaseβπΊ) & β’ πΏ = (LineGβπΊ) & β’ πΌ = (ItvβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π β (ππΌπ)) β β’ (π β (π β (ππΏπ) β¨ π = π)) | ||
Theorem | colcom 28278 | 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.) |
β’ π = (BaseβπΊ) & β’ πΏ = (LineGβπΊ) & β’ πΌ = (ItvβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β (π β (ππΏπ) β¨ π = π)) β β’ (π β (π β (ππΏπ) β¨ π = π)) | ||
Theorem | colrot1 28279 | Rotating the points defining a line. Part of Theorem 4.11 of [Schwabhauser] p. 34. (Contributed by Thierry Arnoux, 3-Apr-2019.) |
β’ π = (BaseβπΊ) & β’ πΏ = (LineGβπΊ) & β’ πΌ = (ItvβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β (π β (ππΏπ) β¨ π = π)) β β’ (π β (π β (ππΏπ) β¨ π = π)) | ||
Theorem | colrot2 28280 | Rotating the points defining a line. Part of Theorem 4.11 of [Schwabhauser] p. 34. (Contributed by Thierry Arnoux, 3-Apr-2019.) |
β’ π = (BaseβπΊ) & β’ πΏ = (LineGβπΊ) & β’ πΌ = (ItvβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β (π β (ππΏπ) β¨ π = π)) β β’ (π β (π β (ππΏπ) β¨ π = π)) | ||
Theorem | ncolcom 28281 | Swapping non-colinear points. (Contributed by Thierry Arnoux, 19-Oct-2019.) |
β’ π = (BaseβπΊ) & β’ πΏ = (LineGβπΊ) & β’ πΌ = (ItvβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β Β¬ (π β (ππΏπ) β¨ π = π)) β β’ (π β Β¬ (π β (ππΏπ) β¨ π = π)) | ||
Theorem | ncolrot1 28282 | Rotating non-colinear points. (Contributed by Thierry Arnoux, 19-Oct-2019.) |
β’ π = (BaseβπΊ) & β’ πΏ = (LineGβπΊ) & β’ πΌ = (ItvβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β Β¬ (π β (ππΏπ) β¨ π = π)) β β’ (π β Β¬ (π β (ππΏπ) β¨ π = π)) | ||
Theorem | ncolrot2 28283 | Rotating non-colinear points. (Contributed by Thierry Arnoux, 19-Oct-2019.) |
β’ π = (BaseβπΊ) & β’ πΏ = (LineGβπΊ) & β’ πΌ = (ItvβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β Β¬ (π β (ππΏπ) β¨ π = π)) β β’ (π β Β¬ (π β (ππΏπ) β¨ π = π)) | ||
Theorem | tgdim01ln 28284 | In geometries of dimension less than two, then any three points are colinear. (Contributed by Thierry Arnoux, 27-Aug-2019.) |
β’ π = (BaseβπΊ) & β’ πΏ = (LineGβπΊ) & β’ πΌ = (ItvβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β Β¬ πΊDimTarskiGβ₯2) β β’ (π β (π β (ππΏπ) β¨ π = π)) | ||
Theorem | ncoltgdim2 28285 | If there are three non-colinear points, then the dimension is at least two. Converse of tglowdim2l 28370. (Contributed by Thierry Arnoux, 23-Feb-2020.) |
β’ π = (BaseβπΊ) & β’ πΏ = (LineGβπΊ) & β’ πΌ = (ItvβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β Β¬ (π β (ππΏπ) β¨ π = π)) β β’ (π β πΊDimTarskiGβ₯2) | ||
Theorem | lnxfr 28286 | Transfer law for colinearity. Theorem 4.13 of [Schwabhauser] p. 37. (Contributed by Thierry Arnoux, 27-Apr-2019.) |
β’ π = (BaseβπΊ) & β’ πΏ = (LineGβπΊ) & β’ πΌ = (ItvβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π β π) & β’ βΌ = (cgrGβπΊ) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β (π β (ππΏπ) β¨ π = π)) & β’ (π β β¨βπππββ© βΌ β¨βπ΄π΅πΆββ©) β β’ (π β (π΅ β (π΄πΏπΆ) β¨ π΄ = πΆ)) | ||
Theorem | lnext 28287* | Extend a line with a missing point. Theorem 4.14 of [Schwabhauser] p. 37. (Contributed by Thierry Arnoux, 27-Apr-2019.) |
β’ π = (BaseβπΊ) & β’ πΏ = (LineGβπΊ) & β’ πΌ = (ItvβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π β π) & β’ βΌ = (cgrGβπΊ) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ β = (distβπΊ) & β’ (π β (π β (ππΏπ) β¨ π = π)) & β’ (π β (π β π) = (π΄ β π΅)) β β’ (π β βπ β π β¨βπππββ© βΌ β¨βπ΄π΅πββ©) | ||
Theorem | tgfscgr 28288 | Congruence law for the general five segment configuration. Theorem 4.16 of [Schwabhauser] p. 37. (Contributed by Thierry Arnoux, 27-Apr-2019.) |
β’ π = (BaseβπΊ) & β’ πΏ = (LineGβπΊ) & β’ πΌ = (ItvβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π β π) & β’ βΌ = (cgrGβπΊ) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ β = (distβπΊ) & β’ (π β π β π) & β’ (π β πΆ β π) & β’ (π β π· β π) & β’ (π β (π β (ππΏπ) β¨ π = π)) & β’ (π β β¨βπππββ© βΌ β¨βπ΄π΅πΆββ©) & β’ (π β (π β π) = (π΄ β π·)) & β’ (π β (π β π) = (π΅ β π·)) & β’ (π β π β π) β β’ (π β (π β π) = (πΆ β π·)) | ||
Theorem | lncgr 28289 | Congruence rule for lines. Theorem 4.17 of [Schwabhauser] p. 37. (Contributed by Thierry Arnoux, 28-Apr-2019.) |
β’ π = (BaseβπΊ) & β’ πΏ = (LineGβπΊ) & β’ πΌ = (ItvβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π β π) & β’ βΌ = (cgrGβπΊ) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ β = (distβπΊ) & β’ (π β π β π) & β’ (π β (π β (ππΏπ) β¨ π = π)) & β’ (π β (π β π΄) = (π β π΅)) & β’ (π β (π β π΄) = (π β π΅)) β β’ (π β (π β π΄) = (π β π΅)) | ||
Theorem | lnid 28290 | Identity law for points on lines. Theorem 4.18 of [Schwabhauser] p. 38. (Contributed by Thierry Arnoux, 28-Apr-2019.) |
β’ π = (BaseβπΊ) & β’ πΏ = (LineGβπΊ) & β’ πΌ = (ItvβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π β π) & β’ βΌ = (cgrGβπΊ) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ β = (distβπΊ) & β’ (π β π β π) & β’ (π β (π β (ππΏπ) β¨ π = π)) & β’ (π β (π β π) = (π β π΄)) & β’ (π β (π β π) = (π β π΄)) β β’ (π β π = π΄) | ||
Theorem | tgidinside 28291 | Law for finding a point inside a segment. Theorem 4.19 of [Schwabhauser] p. 38. (Contributed by Thierry Arnoux, 28-Apr-2019.) |
β’ π = (BaseβπΊ) & β’ πΏ = (LineGβπΊ) & β’ πΌ = (ItvβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π β π) & β’ βΌ = (cgrGβπΊ) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ β = (distβπΊ) & β’ (π β π β (ππΌπ)) & β’ (π β (π β π) = (π β π΄)) & β’ (π β (π β π) = (π β π΄)) β β’ (π β π = π΄) | ||
Theorem | tgbtwnconn1lem1 28292 | Lemma for tgbtwnconn1 28295. (Contributed by Thierry Arnoux, 30-Apr-2019.) |
β’ π = (BaseβπΊ) & β’ πΌ = (ItvβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β π· β π) & β’ (π β π΄ β π΅) & β’ (π β π΅ β (π΄πΌπΆ)) & β’ (π β π΅ β (π΄πΌπ·)) & β’ β = (distβπΊ) & β’ (π β πΈ β π) & β’ (π β πΉ β π) & β’ (π β π» β π) & β’ (π β π½ β π) & β’ (π β π· β (π΄πΌπΈ)) & β’ (π β πΆ β (π΄πΌπΉ)) & β’ (π β πΈ β (π΄πΌπ»)) & β’ (π β πΉ β (π΄πΌπ½)) & β’ (π β (πΈ β π·) = (πΆ β π·)) & β’ (π β (πΆ β πΉ) = (πΆ β π·)) & β’ (π β (πΈ β π») = (π΅ β πΆ)) & β’ (π β (πΉ β π½) = (π΅ β π·)) β β’ (π β π» = π½) | ||
Theorem | tgbtwnconn1lem2 28293 | Lemma for tgbtwnconn1 28295. (Contributed by Thierry Arnoux, 30-Apr-2019.) |
β’ π = (BaseβπΊ) & β’ πΌ = (ItvβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β π· β π) & β’ (π β π΄ β π΅) & β’ (π β π΅ β (π΄πΌπΆ)) & β’ (π β π΅ β (π΄πΌπ·)) & β’ β = (distβπΊ) & β’ (π β πΈ β π) & β’ (π β πΉ β π) & β’ (π β π» β π) & β’ (π β π½ β π) & β’ (π β π· β (π΄πΌπΈ)) & β’ (π β πΆ β (π΄πΌπΉ)) & β’ (π β πΈ β (π΄πΌπ»)) & β’ (π β πΉ β (π΄πΌπ½)) & β’ (π β (πΈ β π·) = (πΆ β π·)) & β’ (π β (πΆ β πΉ) = (πΆ β π·)) & β’ (π β (πΈ β π») = (π΅ β πΆ)) & β’ (π β (πΉ β π½) = (π΅ β π·)) β β’ (π β (πΈ β πΉ) = (πΆ β π·)) | ||
Theorem | tgbtwnconn1lem3 28294 | Lemma for tgbtwnconn1 28295. (Contributed by Thierry Arnoux, 30-Apr-2019.) |
β’ π = (BaseβπΊ) & β’ πΌ = (ItvβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β π· β π) & β’ (π β π΄ β π΅) & β’ (π β π΅ β (π΄πΌπΆ)) & β’ (π β π΅ β (π΄πΌπ·)) & β’ β = (distβπΊ) & β’ (π β πΈ β π) & β’ (π β πΉ β π) & β’ (π β π» β π) & β’ (π β π½ β π) & β’ (π β π· β (π΄πΌπΈ)) & β’ (π β πΆ β (π΄πΌπΉ)) & β’ (π β πΈ β (π΄πΌπ»)) & β’ (π β πΉ β (π΄πΌπ½)) & β’ (π β (πΈ β π·) = (πΆ β π·)) & β’ (π β (πΆ β πΉ) = (πΆ β π·)) & β’ (π β (πΈ β π») = (π΅ β πΆ)) & β’ (π β (πΉ β π½) = (π΅ β π·)) & β’ (π β π β π) & β’ (π β π β (πΆπΌπΈ)) & β’ (π β π β (π·πΌπΉ)) & β’ (π β πΆ β πΈ) β β’ (π β π· = πΉ) | ||
Theorem | tgbtwnconn1 28295 | Connectivity law for betweenness. Theorem 5.1 of [Schwabhauser] p. 39-41. In earlier presentations of Tarski's axioms, this theorem appeared as an additional axiom. It was derived from the other axioms by Gupta, 1965. (Contributed by Thierry Arnoux, 30-Apr-2019.) |
β’ π = (BaseβπΊ) & β’ πΌ = (ItvβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β π· β π) & β’ (π β π΄ β π΅) & β’ (π β π΅ β (π΄πΌπΆ)) & β’ (π β π΅ β (π΄πΌπ·)) β β’ (π β (πΆ β (π΄πΌπ·) β¨ π· β (π΄πΌπΆ))) | ||
Theorem | tgbtwnconn2 28296 | Another connectivity law for betweenness. Theorem 5.2 of [Schwabhauser] p. 41. (Contributed by Thierry Arnoux, 17-May-2019.) |
β’ π = (BaseβπΊ) & β’ πΌ = (ItvβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β π· β π) & β’ (π β π΄ β π΅) & β’ (π β π΅ β (π΄πΌπΆ)) & β’ (π β π΅ β (π΄πΌπ·)) β β’ (π β (πΆ β (π΅πΌπ·) β¨ π· β (π΅πΌπΆ))) | ||
Theorem | tgbtwnconn3 28297 | Inner connectivity law for betweenness. Theorem 5.3 of [Schwabhauser] p. 41. (Contributed by Thierry Arnoux, 17-May-2019.) |
β’ π = (BaseβπΊ) & β’ πΌ = (ItvβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β π· β π) & β’ (π β π΅ β (π΄πΌπ·)) & β’ (π β πΆ β (π΄πΌπ·)) β β’ (π β (π΅ β (π΄πΌπΆ) β¨ πΆ β (π΄πΌπ΅))) | ||
Theorem | tgbtwnconnln3 28298 | Derive colinearity from betweenness. (Contributed by Thierry Arnoux, 17-May-2019.) |
β’ π = (BaseβπΊ) & β’ πΌ = (ItvβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β π· β π) & β’ (π β π΅ β (π΄πΌπ·)) & β’ (π β πΆ β (π΄πΌπ·)) & β’ πΏ = (LineGβπΊ) β β’ (π β (π΅ β (π΄πΏπΆ) β¨ π΄ = πΆ)) | ||
Theorem | tgbtwnconn22 28299 | Double connectivity law for betweenness. (Contributed by Thierry Arnoux, 1-Dec-2019.) |
β’ π = (BaseβπΊ) & β’ πΌ = (ItvβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β π· β π) & β’ (π β πΈ β π) & β’ (π β π΄ β π΅) & β’ (π β πΆ β π΅) & β’ (π β π΅ β (π΄πΌπΆ)) & β’ (π β π΅ β (π΄πΌπ·)) & β’ (π β π΅ β (πΆπΌπΈ)) β β’ (π β π΅ β (π·πΌπΈ)) | ||
Theorem | tgbtwnconnln1 28300 | Derive colinearity from betweenness. (Contributed by Thierry Arnoux, 17-May-2019.) |
β’ π = (BaseβπΊ) & β’ πΌ = (ItvβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β π· β π) & β’ πΏ = (LineGβπΊ) & β’ (π β π΄ β π΅) & β’ (π β π΅ β (π΄πΌπΆ)) & β’ (π β π΅ β (π΄πΌπ·)) β β’ (π β (π΄ β (πΆπΏπ·) β¨ πΆ = π·)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |