![]() |
Metamath
Proof Explorer Theorem List (p. 280 of 480) | < 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-30438) |
![]() (30439-31961) |
![]() (31962-47939) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | precsexlem10 27901* | Lemma for surreal reciprocal. Show that the union of the left sets is less than the union of the right sets. Note that this is the first theorem in the surreal numbers to require the axiom of infinity. (Contributed by Scott Fenton, 15-Mar-2025.) |
β’ πΉ = rec((π β V β¦ β¦(1st βπ) / πβ¦β¦(2nd βπ) / πβ¦β¨(π βͺ ({π β£ βπ₯π β ( R βπ΄)βπ¦πΏ β π π = (( 1s +s ((π₯π -s π΄) Β·s π¦πΏ)) /su π₯π )} βͺ {π β£ βπ₯πΏ β {π₯ β ( L βπ΄) β£ 0s <s π₯}βπ¦π β π π = (( 1s +s ((π₯πΏ -s π΄) Β·s π¦π )) /su π₯πΏ)})), (π βͺ ({π β£ βπ₯πΏ β {π₯ β ( L βπ΄) β£ 0s <s π₯}βπ¦πΏ β π π = (( 1s +s ((π₯πΏ -s π΄) Β·s π¦πΏ)) /su π₯πΏ)} βͺ {π β£ βπ₯π β ( R βπ΄)βπ¦π β π π = (( 1s +s ((π₯π -s π΄) Β·s π¦π )) /su π₯π )}))β©), β¨{ 0s }, β β©) & β’ πΏ = (1st β πΉ) & β’ π = (2nd β πΉ) & β’ (π β π΄ β No ) & β’ (π β 0s <s π΄) & β’ (π β βπ₯π β (( L βπ΄) βͺ ( R βπ΄))( 0s <s π₯π β βπ¦ β No (π₯π Β·s π¦) = 1s )) β β’ (π β βͺ (πΏ β Ο) <<s βͺ (π β Ο)) | ||
Theorem | precsexlem11 27902* | Lemma for surreal reciprocal. Show that the cut of the left and right sets is a multiplicative inverse for π΄. (Contributed by Scott Fenton, 15-Mar-2025.) |
β’ πΉ = rec((π β V β¦ β¦(1st βπ) / πβ¦β¦(2nd βπ) / πβ¦β¨(π βͺ ({π β£ βπ₯π β ( R βπ΄)βπ¦πΏ β π π = (( 1s +s ((π₯π -s π΄) Β·s π¦πΏ)) /su π₯π )} βͺ {π β£ βπ₯πΏ β {π₯ β ( L βπ΄) β£ 0s <s π₯}βπ¦π β π π = (( 1s +s ((π₯πΏ -s π΄) Β·s π¦π )) /su π₯πΏ)})), (π βͺ ({π β£ βπ₯πΏ β {π₯ β ( L βπ΄) β£ 0s <s π₯}βπ¦πΏ β π π = (( 1s +s ((π₯πΏ -s π΄) Β·s π¦πΏ)) /su π₯πΏ)} βͺ {π β£ βπ₯π β ( R βπ΄)βπ¦π β π π = (( 1s +s ((π₯π -s π΄) Β·s π¦π )) /su π₯π )}))β©), β¨{ 0s }, β β©) & β’ πΏ = (1st β πΉ) & β’ π = (2nd β πΉ) & β’ (π β π΄ β No ) & β’ (π β 0s <s π΄) & β’ (π β βπ₯π β (( L βπ΄) βͺ ( R βπ΄))( 0s <s π₯π β βπ¦ β No (π₯π Β·s π¦) = 1s )) & β’ π = (βͺ (πΏ β Ο) |s βͺ (π β Ο)) β β’ (π β (π΄ Β·s π) = 1s ) | ||
Theorem | precsex 27903* | Every positive surreal has a reciprocal. Theorem 10(iv) of [Conway] p. 21. (Contributed by Scott Fenton, 15-Mar-2025.) |
β’ ((π΄ β No β§ 0s <s π΄) β βπ¦ β No (π΄ Β·s π¦) = 1s ) | ||
Theorem | recsex 27904* | A non-zero surreal has a reciprocal. (Contributed by Scott Fenton, 15-Mar-2025.) |
β’ ((π΄ β No β§ π΄ β 0s ) β βπ₯ β No (π΄ Β·s π₯) = 1s ) | ||
Theorem | recsexd 27905* | A non-zero surreal has a reciprocal. (Contributed by Scott Fenton, 16-Mar-2025.) |
β’ (π β π΄ β No ) & β’ (π β π΄ β 0s ) β β’ (π β βπ₯ β No (π΄ Β·s π₯) = 1s ) | ||
Theorem | divsmul 27906 | Relationship between surreal division and multiplication. (Contributed by Scott Fenton, 16-Mar-2025.) |
β’ ((π΄ β No β§ π΅ β No β§ (πΆ β No β§ πΆ β 0s )) β ((π΄ /su πΆ) = π΅ β (πΆ Β·s π΅) = π΄)) | ||
Theorem | divsmuld 27907 | Relationship between surreal division and multiplication. (Contributed by Scott Fenton, 16-Mar-2025.) |
β’ (π β π΄ β No ) & β’ (π β π΅ β No ) & β’ (π β πΆ β No ) & β’ (π β πΆ β 0s ) β β’ (π β ((π΄ /su πΆ) = π΅ β (πΆ Β·s π΅) = π΄)) | ||
Theorem | divscl 27908 | Surreal division closure law. (Contributed by Scott Fenton, 16-Mar-2025.) |
β’ ((π΄ β No β§ π΅ β No β§ π΅ β 0s ) β (π΄ /su π΅) β No ) | ||
Theorem | divscld 27909 | Surreal division closure law. (Contributed by Scott Fenton, 16-Mar-2025.) |
β’ (π β π΄ β No ) & β’ (π β π΅ β No ) & β’ (π β π΅ β 0s ) β β’ (π β (π΄ /su π΅) β No ) | ||
Theorem | divscan2d 27910 | A cancellation law for surreal division. (Contributed by Scott Fenton, 16-Mar-2025.) |
β’ (π β π΄ β No ) & β’ (π β π΅ β No ) & β’ (π β π΅ β 0s ) β β’ (π β (π΅ Β·s (π΄ /su π΅)) = π΄) | ||
Theorem | divscan1d 27911 | A cancellation law for surreal division. (Contributed by Scott Fenton, 16-Mar-2025.) |
β’ (π β π΄ β No ) & β’ (π β π΅ β No ) & β’ (π β π΅ β 0s ) β β’ (π β ((π΄ /su π΅) Β·s π΅) = π΄) | ||
Theorem | sltdivmuld 27912 | Surreal less-than relationship between division and multiplication. (Contributed by Scott Fenton, 16-Mar-2025.) |
β’ (π β π΄ β No ) & β’ (π β π΅ β No ) & β’ (π β πΆ β No ) & β’ (π β 0s <s πΆ) β β’ (π β ((π΄ /su πΆ) <s π΅ β π΄ <s (πΆ Β·s π΅))) | ||
Theorem | sltdivmul2d 27913 | Surreal less-than relationship between division and multiplication. (Contributed by Scott Fenton, 16-Mar-2025.) |
β’ (π β π΄ β No ) & β’ (π β π΅ β No ) & β’ (π β πΆ β No ) & β’ (π β 0s <s πΆ) β β’ (π β ((π΄ /su πΆ) <s π΅ β π΄ <s (π΅ Β·s πΆ))) | ||
Theorem | sltmuldivd 27914 | Surreal less-than relationship between division and multiplication. (Contributed by Scott Fenton, 16-Mar-2025.) |
β’ (π β π΄ β No ) & β’ (π β π΅ β No ) & β’ (π β πΆ β No ) & β’ (π β 0s <s πΆ) β β’ (π β ((π΄ Β·s πΆ) <s π΅ β π΄ <s (π΅ /su πΆ))) | ||
Theorem | sltmuldiv2d 27915 | Surreal less-than relationship between division and multiplication. (Contributed by Scott Fenton, 16-Mar-2025.) |
β’ (π β π΄ β No ) & β’ (π β π΅ β No ) & β’ (π β πΆ β No ) & β’ (π β 0s <s πΆ) β β’ (π β ((πΆ Β·s π΄) <s π΅ β π΄ <s (π΅ /su πΆ))) | ||
Theorem | divsassd 27916 | An associative law for surreal division. (Contributed by Scott Fenton, 16-Mar-2025.) |
β’ (π β π΄ β No ) & β’ (π β π΅ β No ) & β’ (π β πΆ β No ) & β’ (π β πΆ β 0s ) β β’ (π β ((π΄ Β·s π΅) /su πΆ) = (π΄ Β·s (π΅ /su πΆ))) | ||
Syntax | cons 27917 | Declare the syntax for surreal ordinals. |
class Ons | ||
Definition | df-ons 27918 | Define the surreal ordinals. These are the maximum members of each generation of surreals. Variant of definition from [Conway] p. 27. (Contributed by Scott Fenton, 18-Mar-2025.) |
β’ Ons = {π₯ β No β£ ( R βπ₯) = β } | ||
Theorem | elons 27919 | Membership in the class of surreal ordinals. (Contributed by Scott Fenton, 18-Mar-2025.) |
β’ (π΄ β Ons β (π΄ β No β§ ( R βπ΄) = β )) | ||
Theorem | onssno 27920 | The surreal ordinals are a subclass of the surreals. (Contributed by Scott Fenton, 18-Mar-2025.) |
β’ Ons β No | ||
Theorem | onsno 27921 | A surreal ordinal is a surreal. (Contributed by Scott Fenton, 18-Mar-2025.) |
β’ (π΄ β Ons β π΄ β No ) | ||
Theorem | 0ons 27922 | Surreal zero is a surreal ordinal. (Contributed by Scott Fenton, 18-Mar-2025.) |
β’ 0s β Ons | ||
Theorem | 1ons 27923 | Surreal one is a surreal ordinal. (Contributed by Scott Fenton, 18-Mar-2025.) |
β’ 1s β Ons | ||
Theorem | elons2 27924* | A surreal is ordinal iff it is the cut of some set of surreals and the empty set. Definition from [Conway] p. 27. (Contributed by Scott Fenton, 19-Mar-2025.) |
β’ (π΄ β Ons β βπ β π« No π΄ = (π |s β )) | ||
Theorem | elons2d 27925 | The cut of any set of surreals and the empty set is a surreal ordinal. (Contributed by Scott Fenton, 19-Mar-2025.) |
β’ (π β π΄ β π) & β’ (π β π΄ β No ) & β’ (π β π = (π΄ |s β )) β β’ (π β π β Ons) | ||
Theorem | sltonold 27926* | The class of ordinals less than any surreal is a subset of that surreal's old set. (Contributed by Scott Fenton, 22-Mar-2025.) |
β’ (π΄ β No β {π₯ β Ons β£ π₯ <s π΄} β ( O β( bday βπ΄))) | ||
Theorem | sltonex 27927* | The class of ordinals less than any particular surreal is a set. Theorem 14 of [Conway] p. 27. (Contributed by Scott Fenton, 22-Mar-2025.) |
β’ (π΄ β No β {π₯ β Ons β£ π₯ <s π΄} β V) | ||
Theorem | onscutleft 27928 | A surreal ordinal is equal to the cut of its left set and the empty set. (Contributed by Scott Fenton, 29-Mar-2025.) |
β’ (π΄ β Ons β π΄ = (( L βπ΄) |s β )) | ||
Syntax | cnn0s 27929 | Declare the syntax for surreal non-negative integers. |
class β0s | ||
Syntax | cnns 27930 | Declare the syntax for surreal positive integers. |
class βs | ||
Definition | df-n0s 27931 | Define the set of non-negative surreal integers. This set behaves similarly to Ο and β0, but it is a set of surreal numbers. Like those two sets, it satisfies the Peano axioms and is closed under (surreal) addition and multiplication. Compare df-nn 12217. (Contributed by Scott Fenton, 17-Mar-2025.) |
β’ β0s = (rec((π₯ β V β¦ (π₯ +s 1s )), 0s ) β Ο) | ||
Definition | df-nns 27932 | Define the set of positive surreal integers. (Contributed by Scott Fenton, 17-Mar-2025.) |
β’ βs = (β0s β { 0s }) | ||
Theorem | n0sex 27933 | The set of all non-negative surreal integers exists. (Contributed by Scott Fenton, 17-Mar-2025.) |
β’ β0s β V | ||
Theorem | nnsex 27934 | The set of all positive surreal integers exists. (Contributed by Scott Fenton, 17-Mar-2025.) |
β’ βs β V | ||
Theorem | peano5n0s 27935* | Peano's inductive postulate for non-negative surreal integers. (Contributed by Scott Fenton, 17-Mar-2025.) |
β’ (( 0s β π΄ β§ βπ₯ β π΄ (π₯ +s 1s ) β π΄) β β0s β π΄) | ||
Theorem | n0ssno 27936 | The non-negative surreal integers are a subset of the surreals. (Contributed by Scott Fenton, 17-Mar-2025.) |
β’ β0s β No | ||
Theorem | nnssn0s 27937 | The positive surreal integers are a subset of the non-negative surreal integers. (Contributed by Scott Fenton, 17-Mar-2025.) |
β’ βs β β0s | ||
Theorem | nnssno 27938 | The positive surreal integers are a subset of the surreals. (Contributed by Scott Fenton, 17-Mar-2025.) |
β’ βs β No | ||
Theorem | 0n0s 27939 | Peano postulate: 0s is a non-negative surreal integer. (Contributed by Scott Fenton, 17-Mar-2025.) |
β’ 0s β β0s | ||
Theorem | peano2n0s 27940 | Peano postulate: the successor of a non-negative surreal integer is a non-negative surreal integer. (Contributed by Scott Fenton, 17-Mar-2025.) |
β’ (π΄ β β0s β (π΄ +s 1s ) β β0s) | ||
Theorem | dfn0s2 27941* | Alternate definition of the set of non-negative surreal integers. (Contributed by Scott Fenton, 17-Mar-2025.) |
β’ β0s = β© {π₯ β£ ( 0s β π₯ β§ βπ¦ β π₯ (π¦ +s 1s ) β π₯)} | ||
Theorem | n0sind 27942* | Principle of Mathematical Induction (inference schema). Compare nnind 12234 and finds 7891. (Contributed by Scott Fenton, 17-Mar-2025.) |
β’ (π₯ = 0s β (π β π)) & β’ (π₯ = π¦ β (π β π)) & β’ (π₯ = (π¦ +s 1s ) β (π β π)) & β’ (π₯ = π΄ β (π β π)) & β’ π & β’ (π¦ β β0s β (π β π)) β β’ (π΄ β β0s β π) | ||
Theorem | n0scut 27943 | A cut form for surreal naturals. (Contributed by Scott Fenton, 2-Apr-2025.) |
β’ (π΄ β β0s β π΄ = ({(π΄ -s 1s )} |s β )) | ||
Theorem | n0ons 27944 | A surreal natural is a surreal ordinal. (Contributed by Scott Fenton, 2-Apr-2025.) |
β’ (π΄ β β0s β π΄ β Ons) | ||
This part develops elementary geometry based on Tarski's axioms, following [Schwabhauser]. Tarski's geometry is a first-order theory with one sort, the "points". It has two primitive notions, the ternary predicate of "betweenness" and the quaternary predicate of "congruence". To adapt this theory to the framework of set.mm, and to be able to talk of *a* Tarski structure as a space satisfying the given axioms, we use the following definition, stated informally: A Tarski structure π is a set (of points) (Baseβπ) together with functions (Itvβπ) and (distβπ) on ((Baseβπ) Γ (Baseβπ)) satisfying certain axioms (given in Definitions df-trkg 27971 et sequentes). This allows to treat a Tarski structure as a special kind of extensible structure (see df-struct 17084). The translation to and from Tarski's treatment is as follows (given, again, informally). Suppose that one is given an extensible structure π. One defines a betweenness ternary predicate Btw by positing that, for any π₯, π¦, π§ β (Baseβπ), one has "Btw π₯π¦π§ " if and only if π¦ β π₯(Itvβπ)π§, and a congruence quaternary predicate Congr by positing that, for any π₯, π¦, π§, π‘ β (Baseβπ), one has "Congr π₯π¦π§π‘ " if and only if π₯(distβπ)π¦ = π§(distβπ)π‘. It is easy to check that if π satisfies our Tarski axioms, then Btw and Congr satisfy Tarski's Tarski axioms when (Baseβπ) is interpreted as the universe of discourse. Conversely, suppose that one is given a set π, a ternary predicate Btw, and a quaternary predicate Congr. One defines the extensible structure π such that (Baseβπ) is π, and (Itvβπ) is the function which associates with each β¨π₯, π¦β© β (π Γ π) the set of points π§ β π such that "Btw π₯π§π¦", and (distβπ) is the function which associates with each β¨π₯, π¦β© β (π Γ π) the set of ordered pairs β¨π§, π‘β© β (π Γ π) such that "Congr π₯π¦π§π‘". It is easy to check that if Btw and Congr satisfy Tarski's Tarski axioms when π is interpreted as the universe of discourse, then π satisfies our Tarski axioms. We intentionally choose to represent congruence (without loss of generality) as π₯(distβπ)π¦ = π§(distβπ)π‘ instead of "Congr π₯π¦π§π‘", as it is more convenient. It is always possible to define dist for any particular geometry to produce equal results when conguence is desired, and in many cases there is an obvious interpretation of "distance" between two points that can be useful in other situations. Encoding congruence as an equality of distances makes it easier to use these theorems in cases where there is a preferred distance function. We prove that representing a congruence relationship using a distance in the form π₯(distβπ)π¦ = π§(distβπ)π‘ causes no loss of generality in tgjustc1 27993 and tgjustc2 27994, which in turn are supported by tgjustf 27991 and tgjustr 27992. A similar representation of congruence (using a "distance" function) is used in Axiom A1 of [Beeson2016] p. 5, which discusses how a large number of formalized proofs were found in Tarskian Geometry using OTTER. Their detailed proofs in Tarski Geometry, along with other information, are available at https://www.michaelbeeson.com/research/FormalTarski/ 27992. Most theorems are in deduction form, as this is a very general, simple, and convenient format to use in Metamath. An assertion in deduction form can be easily converted into an assertion in inference form (removing the antecedents π β) by insert a β€ β in each hypothesis, using a1i 11, then using mptru 1546 to remove the final β€ β prefix. In some cases we represent, without loss of generality, an implication antecedent in [Schwabhauser] as a hypothesis. The implication can be retrieved from the by using simpr 483, the theorem as stated, and ex 411. For descriptions of individual axioms, we refer to the specific definitions below. A particular feature of Tarski's axioms is modularity, so by using various subsets of the set of axioms, we can define the classes of "absolute dimensionless Tarski structures" (df-trkg 27971), of "Euclidean dimensionless Tarski structures" (df-trkge 27969) and of "Tarski structures of dimension no less than N" (df-trkgld 27970). In this system, angles are not a primitive notion, but instead a derived notion (see df-cgra 28326 and iscgra 28327). To maintain its simplicity, in this system congruence between shapes (a finite sequence of points) is the case where corresponding segments between all corresponding points are congruent. This includes triangles (a shape of 3 distinct points). Note that this definition has no direct regard for angles. For more details and rationale, see df-cgrg 28029. The first section is devoted to the definitions of these various structures. The second section ("Tarskian geometry") develops the synthetic treatment of geometry. The remaining sections prove that real Euclidean spaces and complex Hilbert spaces, with intended interpretations, are Euclidean Tarski structures. Most of the work in this part is due to Thierry Arnoux, with earlier work by Mario Carneiro and Scott Fenton. See also the credits in the comment of each statement. | ||
Syntax | cstrkg 27945 | Extends class notation with the class of Tarski geometries. |
class TarskiG | ||
Syntax | cstrkgc 27946 | Extends class notation with the class of geometries fulfilling the congruence axioms. |
class TarskiGC | ||
Syntax | cstrkgb 27947 | Extends class notation with the class of geometries fulfilling the betweenness axioms. |
class TarskiGB | ||
Syntax | cstrkgcb 27948 | Extends class notation with the class of geometries fulfilling the congruence and betweenness axioms. |
class TarskiGCB | ||
Syntax | cstrkgld 27949 | Extends class notation with the relation for geometries fulfilling the lower dimension axioms. |
class DimTarskiGβ₯ | ||
Syntax | cstrkge 27950 | Extends class notation with the class of geometries fulfilling Euclid's axiom. |
class TarskiGE | ||
Syntax | citv 27951 | Declare the syntax for the Interval (segment) index extractor. |
class Itv | ||
Syntax | clng 27952 | Declare the syntax for the Line function. |
class LineG | ||
Definition | df-itv 27953 | Define the Interval (segment) index extractor for Tarski geometries. (Contributed by Thierry Arnoux, 24-Aug-2017.) Use its index-independent form itvid 27957 instead. (New usage is discouraged.) |
β’ Itv = Slot ;16 | ||
Definition | df-lng 27954 | Define the line index extractor for geometries. (Contributed by Thierry Arnoux, 27-Mar-2019.) Use its index-independent form lngid 27958 instead. (New usage is discouraged.) |
β’ LineG = Slot ;17 | ||
Theorem | itvndx 27955 | Index value of the Interval (segment) slot. Use ndxarg 17133. (Contributed by Thierry Arnoux, 24-Aug-2017.) (New usage is discouraged.) |
β’ (Itvβndx) = ;16 | ||
Theorem | lngndx 27956 | Index value of the "line" slot. Use ndxarg 17133. (Contributed by Thierry Arnoux, 27-Mar-2019.) (New usage is discouraged.) |
β’ (LineGβndx) = ;17 | ||
Theorem | itvid 27957 | Utility theorem: index-independent form of df-itv 27953. (Contributed by Thierry Arnoux, 24-Aug-2017.) |
β’ Itv = Slot (Itvβndx) | ||
Theorem | lngid 27958 | Utility theorem: index-independent form of df-lng 27954. (Contributed by Thierry Arnoux, 27-Mar-2019.) |
β’ LineG = Slot (LineGβndx) | ||
Theorem | slotsinbpsd 27959 | The slots Base, +g, Β·π and dist are different from the slot Itv. Formerly part of ttglem 28395 and proofs using it. (Contributed by AV, 29-Oct-2024.) |
β’ (((Itvβndx) β (Baseβndx) β§ (Itvβndx) β (+gβndx)) β§ ((Itvβndx) β ( Β·π βndx) β§ (Itvβndx) β (distβndx))) | ||
Theorem | slotslnbpsd 27960 | The slots Base, +g, Β·π and dist are different from the slot LineG. Formerly part of ttglem 28395 and proofs using it. (Contributed by AV, 29-Oct-2024.) |
β’ (((LineGβndx) β (Baseβndx) β§ (LineGβndx) β (+gβndx)) β§ ((LineGβndx) β ( Β·π βndx) β§ (LineGβndx) β (distβndx))) | ||
Theorem | lngndxnitvndx 27961 | The slot for the line is not the slot for the Interval (segment) in an extensible structure. Formerly part of proof for ttgval 28393. (Contributed by AV, 9-Nov-2024.) |
β’ (LineGβndx) β (Itvβndx) | ||
Theorem | trkgstr 27962 | Functionality of a Tarski geometry. (Contributed by Thierry Arnoux, 24-Aug-2017.) |
β’ π = {β¨(Baseβndx), πβ©, β¨(distβndx), π·β©, β¨(Itvβndx), πΌβ©} β β’ π Struct β¨1, ;16β© | ||
Theorem | trkgbas 27963 | The base set of a Tarski geometry. (Contributed by Thierry Arnoux, 24-Aug-2017.) |
β’ π = {β¨(Baseβndx), πβ©, β¨(distβndx), π·β©, β¨(Itvβndx), πΌβ©} β β’ (π β π β π = (Baseβπ)) | ||
Theorem | trkgdist 27964 | The measure of a distance in a Tarski geometry. (Contributed by Thierry Arnoux, 24-Aug-2017.) |
β’ π = {β¨(Baseβndx), πβ©, β¨(distβndx), π·β©, β¨(Itvβndx), πΌβ©} β β’ (π· β π β π· = (distβπ)) | ||
Theorem | trkgitv 27965 | The congruence relation in a Tarski geometry. (Contributed by Thierry Arnoux, 24-Aug-2017.) |
β’ π = {β¨(Baseβndx), πβ©, β¨(distβndx), π·β©, β¨(Itvβndx), πΌβ©} β β’ (πΌ β π β πΌ = (Itvβπ)) | ||
Definition | df-trkgc 27966* | Define the class of geometries fulfilling the congruence axioms of reflexivity, identity and transitivity. These are axioms A1 to A3 of [Schwabhauser] p. 10. With our distance based notation for congruence, transitivity of congruence boils down to transitivity of equality and is already given by eqtr 2753, so it is not listed in this definition. (Contributed by Thierry Arnoux, 24-Aug-2017.) |
β’ TarskiGC = {π β£ [(Baseβπ) / π][(distβπ) / π](βπ₯ β π βπ¦ β π (π₯ππ¦) = (π¦ππ₯) β§ βπ₯ β π βπ¦ β π βπ§ β π ((π₯ππ¦) = (π§ππ§) β π₯ = π¦))} | ||
Definition | df-trkgb 27967* | Define the class of geometries fulfilling the 3 betweenness axioms in Tarski's Axiomatization of Geometry: identity, Axiom A6 of [Schwabhauser] p. 11, axiom of Pasch, Axiom A7 of [Schwabhauser] p. 12, and continuity, Axiom A11 of [Schwabhauser] p. 13. (Contributed by Thierry Arnoux, 24-Aug-2017.) |
β’ TarskiGB = {π β£ [(Baseβπ) / π][(Itvβπ) / π](βπ₯ β π βπ¦ β π (π¦ β (π₯ππ₯) β π₯ = π¦) β§ βπ₯ β π βπ¦ β π βπ§ β π βπ’ β π βπ£ β π ((π’ β (π₯ππ§) β§ π£ β (π¦ππ§)) β βπ β π (π β (π’ππ¦) β§ π β (π£ππ₯))) β§ βπ β π« πβπ‘ β π« π(βπ β π βπ₯ β π βπ¦ β π‘ π₯ β (πππ¦) β βπ β π βπ₯ β π βπ¦ β π‘ π β (π₯ππ¦)))} | ||
Definition | df-trkgcb 27968* | Define the class of geometries fulfilling the five segment axiom, Axiom A5 of [Schwabhauser] p. 11, and segment construction axiom, Axiom A4 of [Schwabhauser] p. 11. (Contributed by Thierry Arnoux, 14-Mar-2019.) |
β’ TarskiGCB = {π β£ [(Baseβπ) / π][(distβπ) / π][(Itvβπ) / π](βπ₯ β π βπ¦ β π βπ§ β π βπ’ β π βπ β π βπ β π βπ β π βπ£ β π (((π₯ β π¦ β§ π¦ β (π₯ππ§) β§ π β (πππ)) β§ (((π₯ππ¦) = (πππ) β§ (π¦ππ§) = (πππ)) β§ ((π₯ππ’) = (πππ£) β§ (π¦ππ’) = (πππ£)))) β (π§ππ’) = (πππ£)) β§ βπ₯ β π βπ¦ β π βπ β π βπ β π βπ§ β π (π¦ β (π₯ππ§) β§ (π¦ππ§) = (πππ)))} | ||
Definition | df-trkge 27969* | Define the class of geometries fulfilling Euclid's axiom, Axiom A10 of [Schwabhauser] p. 13. (Contributed by Thierry Arnoux, 14-Mar-2019.) |
β’ TarskiGE = {π β£ [(Baseβπ) / π][(Itvβπ) / π]βπ₯ β π βπ¦ β π βπ§ β π βπ’ β π βπ£ β π ((π’ β (π₯ππ£) β§ π’ β (π¦ππ§) β§ π₯ β π’) β βπ β π βπ β π (π¦ β (π₯ππ) β§ π§ β (π₯ππ) β§ π£ β (πππ)))} | ||
Definition | df-trkgld 27970* | Define the class of geometries fulfilling the lower dimension axiom for dimension π. For such geometries, there are three non-colinear points that are equidistant from π β 1 distinct points. Derived from remarks in Tarski's System of Geometry, Alfred Tarski and Steven Givant, Bulletin of Symbolic Logic, Volume 5, Number 2 (1999), 175-214. (Contributed by Scott Fenton, 22-Apr-2013.) (Revised by Thierry Arnoux, 23-Nov-2019.) |
β’ DimTarskiGβ₯ = {β¨π, πβ© β£ [(Baseβπ) / π][(distβπ) / π][(Itvβπ) / π]βπ(π:(1..^π)β1-1βπ β§ βπ₯ β π βπ¦ β π βπ§ β π (βπ β (2..^π)(((πβ1)ππ₯) = ((πβπ)ππ₯) β§ ((πβ1)ππ¦) = ((πβπ)ππ¦) β§ ((πβ1)ππ§) = ((πβπ)ππ§)) β§ Β¬ (π§ β (π₯ππ¦) β¨ π₯ β (π§ππ¦) β¨ π¦ β (π₯ππ§))))} | ||
Definition | df-trkg 27971* |
Define the class of Tarski geometries. A Tarski geometry is a set of
points, equipped with a betweenness relation (denoting that a point lies
on a line segment between two other points) and a congruence relation
(denoting equality of line segment lengths).
Here, we are using the following:
Tarski originally had more axioms, but later reduced his list to 11:
So our definition of a Tarskian Geometry includes the 3 axioms for the quaternary congruence relation (A1, A2, A3), the 3 axioms for the ternary betweenness relation (A6, A7, A11), and the 2 axioms of compatibility of the congruence and the betweenness relations (A4,A5). It does not include Euclid's axiom A10, nor the 2-dimensional axioms A8 (Lower dimension axiom) and A9 (Upper dimension axiom) so the number of dimensions of the geometry it formalizes is not constrained. Considering A2 as one of the 3 axioms for the quaternary congruence relation is somewhat conventional, because the transitivity of the congruence relation is automatically given by our choice to take the distance as this congruence relation in our definition of Tarski geometries. (Contributed by Thierry Arnoux, 24-Aug-2017.) (Revised by Thierry Arnoux, 27-Apr-2019.) |
β’ TarskiG = ((TarskiGC β© TarskiGB) β© (TarskiGCB β© {π β£ [(Baseβπ) / π][(Itvβπ) / π](LineGβπ) = (π₯ β π, π¦ β (π β {π₯}) β¦ {π§ β π β£ (π§ β (π₯ππ¦) β¨ π₯ β (π§ππ¦) β¨ π¦ β (π₯ππ§))})})) | ||
Theorem | istrkgc 27972* | Property of being a Tarski geometry - congruence part. (Contributed by Thierry Arnoux, 14-Mar-2019.) |
β’ π = (BaseβπΊ) & β’ β = (distβπΊ) & β’ πΌ = (ItvβπΊ) β β’ (πΊ β TarskiGC β (πΊ β V β§ (βπ₯ β π βπ¦ β π (π₯ β π¦) = (π¦ β π₯) β§ βπ₯ β π βπ¦ β π βπ§ β π ((π₯ β π¦) = (π§ β π§) β π₯ = π¦)))) | ||
Theorem | istrkgb 27973* | Property of being a Tarski geometry - betweenness part. (Contributed by Thierry Arnoux, 14-Mar-2019.) |
β’ π = (BaseβπΊ) & β’ β = (distβπΊ) & β’ πΌ = (ItvβπΊ) β β’ (πΊ β TarskiGB β (πΊ β V β§ (βπ₯ β π βπ¦ β π (π¦ β (π₯πΌπ₯) β π₯ = π¦) β§ βπ₯ β π βπ¦ β π βπ§ β π βπ’ β π βπ£ β π ((π’ β (π₯πΌπ§) β§ π£ β (π¦πΌπ§)) β βπ β π (π β (π’πΌπ¦) β§ π β (π£πΌπ₯))) β§ βπ β π« πβπ‘ β π« π(βπ β π βπ₯ β π βπ¦ β π‘ π₯ β (ππΌπ¦) β βπ β π βπ₯ β π βπ¦ β π‘ π β (π₯πΌπ¦))))) | ||
Theorem | istrkgcb 27974* | Property of being a Tarski geometry - congruence and betweenness part. (Contributed by Thierry Arnoux, 14-Mar-2019.) |
β’ π = (BaseβπΊ) & β’ β = (distβπΊ) & β’ πΌ = (ItvβπΊ) β β’ (πΊ β TarskiGCB β (πΊ β V β§ (βπ₯ β π βπ¦ β π βπ§ β π βπ’ β π βπ β π βπ β π βπ β π βπ£ β π (((π₯ β π¦ β§ π¦ β (π₯πΌπ§) β§ π β (ππΌπ)) β§ (((π₯ β π¦) = (π β π) β§ (π¦ β π§) = (π β π)) β§ ((π₯ β π’) = (π β π£) β§ (π¦ β π’) = (π β π£)))) β (π§ β π’) = (π β π£)) β§ βπ₯ β π βπ¦ β π βπ β π βπ β π βπ§ β π (π¦ β (π₯πΌπ§) β§ (π¦ β π§) = (π β π))))) | ||
Theorem | istrkge 27975* | Property of fulfilling Euclid's axiom. (Contributed by Thierry Arnoux, 14-Mar-2019.) |
β’ π = (BaseβπΊ) & β’ β = (distβπΊ) & β’ πΌ = (ItvβπΊ) β β’ (πΊ β TarskiGE β (πΊ β V β§ βπ₯ β π βπ¦ β π βπ§ β π βπ’ β π βπ£ β π ((π’ β (π₯πΌπ£) β§ π’ β (π¦πΌπ§) β§ π₯ β π’) β βπ β π βπ β π (π¦ β (π₯πΌπ) β§ π§ β (π₯πΌπ) β§ π£ β (ππΌπ))))) | ||
Theorem | istrkgl 27976* | Building lines from the segment property. (Contributed by Thierry Arnoux, 14-Mar-2019.) |
β’ π = (BaseβπΊ) & β’ β = (distβπΊ) & β’ πΌ = (ItvβπΊ) β β’ (πΊ β {π β£ [(Baseβπ) / π][(Itvβπ) / π](LineGβπ) = (π₯ β π, π¦ β (π β {π₯}) β¦ {π§ β π β£ (π§ β (π₯ππ¦) β¨ π₯ β (π§ππ¦) β¨ π¦ β (π₯ππ§))})} β (πΊ β V β§ (LineGβπΊ) = (π₯ β π, π¦ β (π β {π₯}) β¦ {π§ β π β£ (π§ β (π₯πΌπ¦) β¨ π₯ β (π§πΌπ¦) β¨ π¦ β (π₯πΌπ§))}))) | ||
Theorem | istrkgld 27977* | Property of fulfilling the lower dimension π axiom. (Contributed by Thierry Arnoux, 20-Nov-2019.) |
β’ π = (BaseβπΊ) & β’ β = (distβπΊ) & β’ πΌ = (ItvβπΊ) β β’ ((πΊ β π β§ π β (β€β₯β2)) β (πΊDimTarskiGβ₯π β βπ(π:(1..^π)β1-1βπ β§ βπ₯ β π βπ¦ β π βπ§ β π (βπ β (2..^π)(((πβ1) β π₯) = ((πβπ) β π₯) β§ ((πβ1) β π¦) = ((πβπ) β π¦) β§ ((πβ1) β π§) = ((πβπ) β π§)) β§ Β¬ (π§ β (π₯πΌπ¦) β¨ π₯ β (π§πΌπ¦) β¨ π¦ β (π₯πΌπ§)))))) | ||
Theorem | istrkg2ld 27978* | Property of fulfilling the lower dimension 2 axiom. (Contributed by Thierry Arnoux, 20-Nov-2019.) |
β’ π = (BaseβπΊ) & β’ β = (distβπΊ) & β’ πΌ = (ItvβπΊ) β β’ (πΊ β π β (πΊDimTarskiGβ₯2 β βπ₯ β π βπ¦ β π βπ§ β π Β¬ (π§ β (π₯πΌπ¦) β¨ π₯ β (π§πΌπ¦) β¨ π¦ β (π₯πΌπ§)))) | ||
Theorem | istrkg3ld 27979* | Property of fulfilling the lower dimension 3 axiom. (Contributed by Thierry Arnoux, 12-Jul-2020.) |
β’ π = (BaseβπΊ) & β’ β = (distβπΊ) & β’ πΌ = (ItvβπΊ) β β’ (πΊ β π β (πΊDimTarskiGβ₯3 β βπ’ β π βπ£ β π (π’ β π£ β§ βπ₯ β π βπ¦ β π βπ§ β π (((π’ β π₯) = (π£ β π₯) β§ (π’ β π¦) = (π£ β π¦) β§ (π’ β π§) = (π£ β π§)) β§ Β¬ (π§ β (π₯πΌπ¦) β¨ π₯ β (π§πΌπ¦) β¨ π¦ β (π₯πΌπ§)))))) | ||
Theorem | axtgcgrrflx 27980 | Axiom of reflexivity of congruence, Axiom A1 of [Schwabhauser] p. 10. (Contributed by Thierry Arnoux, 14-Mar-2019.) |
β’ π = (BaseβπΊ) & β’ β = (distβπΊ) & β’ πΌ = (ItvβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β π β π) & β’ (π β π β π) β β’ (π β (π β π) = (π β π)) | ||
Theorem | axtgcgrid 27981 | Axiom of identity of congruence, Axiom A3 of [Schwabhauser] p. 10. (Contributed by Thierry Arnoux, 14-Mar-2019.) |
β’ π = (BaseβπΊ) & β’ β = (distβπΊ) & β’ πΌ = (ItvβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β (π β π) = (π β π)) β β’ (π β π = π) | ||
Theorem | axtgsegcon 27982* | Axiom of segment construction, Axiom A4 of [Schwabhauser] p. 11. As discussed in Axiom 4 of [Tarski1999] p. 178, "The intuitive content [is that] given any line segment π΄π΅, one can construct a line segment congruent to it, starting at any point π and going in the direction of any ray containing π. The ray is determined by the point π and a second point π, the endpoint of the ray. The other endpoint of the line segment to be constructed is just the point π§ whose existence is asserted." (Contributed by Thierry Arnoux, 15-Mar-2019.) |
β’ π = (BaseβπΊ) & β’ β = (distβπΊ) & β’ πΌ = (ItvβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π΄ β π) & β’ (π β π΅ β π) β β’ (π β βπ§ β π (π β (ππΌπ§) β§ (π β π§) = (π΄ β π΅))) | ||
Theorem | axtg5seg 27983 | Five segments axiom, Axiom A5 of [Schwabhauser] p. 11. Take two triangles πππ and π΄πΆπ, a point π on ππ, and a point π΅ on π΄πΆ. If all corresponding line segments except for ππ and πΆπ are congruent ( i.e., ππ βΌ π΄π΅, ππ βΌ π΅πΆ, ππ βΌ π΄π, and ππ βΌ π΅π), then ππ and πΆπ are also congruent. As noted in Axiom 5 of [Tarski1999] p. 178, "this axiom is similar in character to the well-known theorems of Euclidean geometry that allow one to conclude, from hypotheses about the congruence of certain corresponding sides and angles in two triangles, the congruence of other corresponding sides and angles." (Contributed by Thierry Arnoux, 14-Mar-2019.) |
β’ π = (BaseβπΊ) & β’ β = (distβπΊ) & β’ πΌ = (ItvβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π β (ππΌπ)) & β’ (π β π΅ β (π΄πΌπΆ)) & β’ (π β (π β π) = (π΄ β π΅)) & β’ (π β (π β π) = (π΅ β πΆ)) & β’ (π β (π β π) = (π΄ β π)) & β’ (π β (π β π) = (π΅ β π)) β β’ (π β (π β π) = (πΆ β π)) | ||
Theorem | axtgbtwnid 27984 | Identity of Betweenness. Axiom A6 of [Schwabhauser] p. 11. (Contributed by Thierry Arnoux, 15-Mar-2019.) |
β’ π = (BaseβπΊ) & β’ β = (distβπΊ) & β’ πΌ = (ItvβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π β (ππΌπ)) β β’ (π β π = π) | ||
Theorem | axtgpasch 27985* | Axiom of (Inner) Pasch, Axiom A7 of [Schwabhauser] p. 12. Given triangle πππ, point π in segment ππ, and point π in segment ππ, there exists a point π on both the segment ππ and the segment ππ. This axiom is essentially a subset of the general Pasch axiom. The general Pasch axiom asserts that on a plane "a line intersecting a triangle in one of its sides, and not intersecting any of the vertices, must intersect one of the other two sides" (per the discussion about Axiom 7 of [Tarski1999] p. 179). The (general) Pasch axiom was used implicitly by Euclid, but never stated; Moritz Pasch discovered its omission in 1882. As noted in the Metamath book, this means that the omission of Pasch's axiom from Euclid went unnoticed for 2000 years. Only the inner Pasch algorithm is included as an axiom; the "outer" form of the Pasch axiom can be proved using the inner form (see theorem 9.6 of [Schwabhauser] p. 69 and the brief discussion in axiom 7.1 of [Tarski1999] p. 180). (Contributed by Thierry Arnoux, 15-Mar-2019.) |
β’ π = (BaseβπΊ) & β’ β = (distβπΊ) & β’ πΌ = (ItvβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π β (ππΌπ)) & β’ (π β π β (ππΌπ)) β β’ (π β βπ β π (π β (ππΌπ) β§ π β (ππΌπ))) | ||
Theorem | axtgcont1 27986* | Axiom of Continuity. Axiom A11 of [Schwabhauser] p. 13. This axiom (scheme) asserts that any two sets π and π (of points) such that the elements of π precede the elements of π with respect to some point π (that is, π₯ is between π and π¦ whenever π₯ is in π and π¦ is in π) are separated by some point π; this is explained in Axiom 11 of [Tarski1999] p. 185. (Contributed by Thierry Arnoux, 16-Mar-2019.) |
β’ π = (BaseβπΊ) & β’ β = (distβπΊ) & β’ πΌ = (ItvβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β π β π) & β’ (π β π β π) β β’ (π β (βπ β π βπ₯ β π βπ¦ β π π₯ β (ππΌπ¦) β βπ β π βπ₯ β π βπ¦ β π π β (π₯πΌπ¦))) | ||
Theorem | axtgcont 27987* | Axiom of Continuity. Axiom A11 of [Schwabhauser] p. 13. For more information see axtgcont1 27986. (Contributed by Thierry Arnoux, 16-Mar-2019.) |
β’ π = (BaseβπΊ) & β’ β = (distβπΊ) & β’ πΌ = (ItvβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π΄ β π) & β’ ((π β§ π’ β π β§ π£ β π) β π’ β (π΄πΌπ£)) β β’ (π β βπ β π βπ₯ β π βπ¦ β π π β (π₯πΌπ¦)) | ||
Theorem | axtglowdim2 27988* | Lower dimension axiom for dimension 2, Axiom A8 of [Schwabhauser] p. 13. There exist 3 non-colinear points. (Contributed by Thierry Arnoux, 20-Nov-2019.) |
β’ π = (BaseβπΊ) & β’ β = (distβπΊ) & β’ πΌ = (ItvβπΊ) & β’ (π β πΊ β π) & β’ (π β πΊDimTarskiGβ₯2) β β’ (π β βπ₯ β π βπ¦ β π βπ§ β π Β¬ (π§ β (π₯πΌπ¦) β¨ π₯ β (π§πΌπ¦) β¨ π¦ β (π₯πΌπ§))) | ||
Theorem | axtgupdim2 27989 | Upper dimension axiom for dimension 2, Axiom A9 of [Schwabhauser] p. 13. Three points π, π and π equidistant to two given two points π and π must be colinear. (Contributed by Thierry Arnoux, 29-May-2019.) (Revised by Thierry Arnoux, 11-Jul-2020.) |
β’ π = (BaseβπΊ) & β’ β = (distβπΊ) & β’ πΌ = (ItvβπΊ) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β (π β π) = (π β π)) & β’ (π β (π β π) = (π β π)) & β’ (π β (π β π) = (π β π)) & β’ (π β πΊ β π) & β’ (π β Β¬ πΊDimTarskiGβ₯3) β β’ (π β (π β (ππΌπ) β¨ π β (ππΌπ) β¨ π β (ππΌπ))) | ||
Theorem | axtgeucl 27990* | Euclid's Axiom. Axiom A10 of [Schwabhauser] p. 13. This is equivalent to Euclid's parallel postulate when combined with other axioms. (Contributed by Thierry Arnoux, 16-Mar-2019.) |
β’ π = (BaseβπΊ) & β’ β = (distβπΊ) & β’ πΌ = (ItvβπΊ) & β’ (π β πΊ β TarskiGE) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π β (ππΌπ)) & β’ (π β π β (ππΌπ)) & β’ (π β π β π) β β’ (π β βπ β π βπ β π (π β (ππΌπ) β§ π β (ππΌπ) β§ π β (ππΌπ))) | ||
Theorem | tgjustf 27991* | Given any function πΉ, equality of the image by πΉ is an equivalence relation. (Contributed by Thierry Arnoux, 25-Jan-2023.) |
β’ (π΄ β π β βπ(π Er π΄ β§ βπ₯ β π΄ βπ¦ β π΄ (π₯ππ¦ β (πΉβπ₯) = (πΉβπ¦)))) | ||
Theorem | tgjustr 27992* | Given any equivalence relation π , one can define a function π such that all elements of an equivalence classe of π have the same image by π. (Contributed by Thierry Arnoux, 25-Jan-2023.) |
β’ ((π΄ β π β§ π Er π΄) β βπ(π Fn π΄ β§ βπ₯ β π΄ βπ¦ β π΄ (π₯π π¦ β (πβπ₯) = (πβπ¦)))) | ||
Theorem | tgjustc1 27993* | A justification for using distance equality instead of the textbook relation on pairs of points for congruence. (Contributed by Thierry Arnoux, 29-Jan-2023.) |
β’ π = (BaseβπΊ) & β’ β = (distβπΊ) β β’ βπ(π Er (π Γ π) β§ βπ€ β π βπ₯ β π βπ¦ β π βπ§ β π (β¨π€, π₯β©πβ¨π¦, π§β© β (π€ β π₯) = (π¦ β π§))) | ||
Theorem | tgjustc2 27994* | A justification for using distance equality instead of the textbook relation on pairs of points for congruence. (Contributed by Thierry Arnoux, 29-Jan-2023.) |
β’ π = (BaseβπΊ) & β’ π Er (π Γ π) β β’ βπ(π Fn (π Γ π) β§ βπ€ β π βπ₯ β π βπ¦ β π βπ§ β π (β¨π€, π₯β©π β¨π¦, π§β© β (π€ππ₯) = (π¦ππ§))) | ||
Theorem | tgcgrcomimp 27995 | Congruence commutes on the RHS. Theorem 2.5 of [Schwabhauser] p. 27. (Contributed by David A. Wheeler, 29-Jun-2020.) |
β’ π = (BaseβπΊ) & β’ β = (distβπΊ) & β’ πΌ = (ItvβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β π· β π) β β’ (π β ((π΄ β π΅) = (πΆ β π·) β (π΄ β π΅) = (π· β πΆ))) | ||
Theorem | tgcgrcomr 27996 | Congruence commutes on the RHS. Variant of Theorem 2.5 of [Schwabhauser] p. 27, but in a convenient form for a common case. (Contributed by David A. Wheeler, 29-Jun-2020.) |
β’ π = (BaseβπΊ) & β’ β = (distβπΊ) & β’ πΌ = (ItvβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β π· β π) & β’ (π β (π΄ β π΅) = (πΆ β π·)) β β’ (π β (π΄ β π΅) = (π· β πΆ)) | ||
Theorem | tgcgrcoml 27997 | Congruence commutes on the LHS. Variant of Theorem 2.5 of [Schwabhauser] p. 27, but in a convenient form for a common case. (Contributed by David A. Wheeler, 29-Jun-2020.) |
β’ π = (BaseβπΊ) & β’ β = (distβπΊ) & β’ πΌ = (ItvβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β π· β π) & β’ (π β (π΄ β π΅) = (πΆ β π·)) β β’ (π β (π΅ β π΄) = (πΆ β π·)) | ||
Theorem | tgcgrcomlr 27998 | Congruence commutes on both sides. (Contributed by Thierry Arnoux, 23-Mar-2019.) |
β’ π = (BaseβπΊ) & β’ β = (distβπΊ) & β’ πΌ = (ItvβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β π· β π) & β’ (π β (π΄ β π΅) = (πΆ β π·)) β β’ (π β (π΅ β π΄) = (π· β πΆ)) | ||
Theorem | tgcgreqb 27999 | Congruence and equality. (Contributed by Thierry Arnoux, 27-Aug-2019.) |
β’ π = (BaseβπΊ) & β’ β = (distβπΊ) & β’ πΌ = (ItvβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β π· β π) & β’ (π β (π΄ β π΅) = (πΆ β π·)) β β’ (π β (π΄ = π΅ β πΆ = π·)) | ||
Theorem | tgcgreq 28000 | Congruence and equality. (Contributed by Thierry Arnoux, 27-Aug-2019.) |
β’ π = (BaseβπΊ) & β’ β = (distβπΊ) & β’ πΌ = (ItvβπΊ) & β’ (π β πΊ β TarskiG) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β π· β π) & β’ (π β (π΄ β π΅) = (πΆ β π·)) & β’ (π β π΄ = π΅) β β’ (π β πΆ = π·) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |