P. 254 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 25301-25400   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	pnt3 25301	The Prime Number Theorem, version 3: the second Chebyshev function tends asymptotically to x. (Contributed by Mario Carneiro, 1-Jun-2016.)
|- ( x e. RR+ |-> ( (ψ ` x ) / x ) ) ~~> r 1
Theorem	pnt2 25302	The Prime Number Theorem, version 2: the first Chebyshev function tends asymptotically to x. (Contributed by Mario Carneiro, 1-Jun-2016.)
|- ( x e. RR+ |-> ( ( theta ` x ) / x ) ) ~~> r 1
Theorem	pnt 25303	The Prime Number Theorem: the number of prime numbers less than x tends asymptotically to x / log ( x ) as x goes to infinity. This is Metamath 100 proof #5. (Contributed by Mario Carneiro, 1-Jun-2016.)
|- ( x e. ( 1 (,) +oo ) |-> ( (π ` x ) / ( x / ( log ` x ) ) ) ) ~~> r 1
14.4.14  Ostrowski's theorem
Theorem	abvcxp 25304*	Raising an absolute value to a power less than one yields another absolute value. (Contributed by Mario Carneiro, 8-Sep-2014.)
|- A = (AbsVal ` R )   &    |- B = ( Base ` R )   &    |- G = ( x e. B |-> ( ( F ` x ) ^c S ) )   =>    |- ( ( F e. A /\ S e. ( 0 (,] 1 ) ) -> G e. A )
Theorem	padicfval 25305*	Value of the p-adic absolute value. (Contributed by Mario Carneiro, 8-Sep-2014.)
|- J = ( q e. Prime |-> ( x e. QQ |-> if ( x = 0 , 0 , ( q ^ -u ( q pCnt x ) ) ) ) )   =>    |- ( P e. Prime -> ( J ` P ) = ( x e. QQ |-> if ( x = 0 , 0 , ( P ^ -u ( P pCnt x ) ) ) ) )
Theorem	padicval 25306*	Value of the p-adic absolute value. (Contributed by Mario Carneiro, 8-Sep-2014.)
|- J = ( q e. Prime |-> ( x e. QQ |-> if ( x = 0 , 0 , ( q ^ -u ( q pCnt x ) ) ) ) )   =>    |- ( ( P e. Prime /\ X e. QQ ) -> ( ( J ` P ) ` X ) = if ( X = 0 , 0 , ( P ^ -u ( P pCnt X ) ) ) )
Theorem	ostth2lem1 25307*	Lemma for ostth2 25326, although it is just a simple statement about exponentials which does not involve any specifics of ostth2 25326. If a power is upper bounded by a linear term, the exponent must be less than one. Or in big-O notation, n e. o ( A ^ n ) for any 1 < A. (Contributed by Mario Carneiro, 10-Sep-2014.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ( ph /\ n e. NN ) -> ( A ^ n ) <_ ( n x. B ) )   =>    |- ( ph -> A <_ 1 )
Theorem	qrngbas 25308	The base set of the field of rationals. (Contributed by Mario Carneiro, 8-Sep-2014.)
|- Q = (ℂfld ↾s QQ )   =>    |- QQ = ( Base ` Q )
Theorem	qdrng 25309	The rationals form a division ring. (Contributed by Mario Carneiro, 8-Sep-2014.)
|- Q = (ℂfld ↾s QQ )   =>    |- Q e. DivRing
Theorem	qrng0 25310	The zero element of the field of rationals. (Contributed by Mario Carneiro, 8-Sep-2014.)
|- Q = (ℂfld ↾s QQ )   =>    |- 0 = ( 0g ` Q )
Theorem	qrng1 25311	The unit element of the field of rationals. (Contributed by Mario Carneiro, 8-Sep-2014.)
|- Q = (ℂfld ↾s QQ )   =>    |- 1 = ( 1r ` Q )
Theorem	qrngneg 25312	The additive inverse in the field of rationals. (Contributed by Mario Carneiro, 8-Sep-2014.)
|- Q = (ℂfld ↾s QQ )   =>    |- ( X e. QQ -> ( ( invg ` Q ) ` X ) = -u X )
Theorem	qrngdiv 25313	The division operation in the field of rationals. (Contributed by Mario Carneiro, 8-Sep-2014.)
|- Q = (ℂfld ↾s QQ )   =>    |- ( ( X e. QQ /\ Y e. QQ /\ Y =/= 0 ) -> ( X (/r ` Q ) Y ) = ( X / Y ) )
Theorem	qabvle 25314	By using induction on N, we show a long-range inequality coming from the triangle inequality. (Contributed by Mario Carneiro, 10-Sep-2014.)
|- Q = (ℂfld ↾s QQ )   &    |- A = (AbsVal ` Q )   =>    |- ( ( F e. A /\ N e. NN0 ) -> ( F ` N ) <_ N )
Theorem	qabvexp 25315	Induct the product rule abvmul 18829 to find the absolute value of a power. (Contributed by Mario Carneiro, 10-Sep-2014.)
|- Q = (ℂfld ↾s QQ )   &    |- A = (AbsVal ` Q )   =>    |- ( ( F e. A /\ M e. QQ /\ N e. NN0 ) -> ( F ` ( M ^ N ) ) = ( ( F ` M ) ^ N ) )
Theorem	ostthlem1 25316*	Lemma for ostth 25328. If two absolute values agree on the positive integers greater than one, then they agree for all rational numbers and thus are equal as functions. (Contributed by Mario Carneiro, 9-Sep-2014.)
|- Q = (ℂfld ↾s QQ )   &    |- A = (AbsVal ` Q )   &    |- ( ph -> F e. A )   &    |- ( ph -> G e. A )   &    |- ( ( ph /\ n e. ( ZZ>= ` 2 ) ) -> ( F ` n ) = ( G ` n ) )   =>    |- ( ph -> F = G )
Theorem	ostthlem2 25317*	Lemma for ostth 25328. Refine ostthlem1 25316 so that it is sufficient to only show equality on the primes. (Contributed by Mario Carneiro, 9-Sep-2014.) (Revised by Mario Carneiro, 20-Jun-2015.)
|- Q = (ℂfld ↾s QQ )   &    |- A = (AbsVal ` Q )   &    |- ( ph -> F e. A )   &    |- ( ph -> G e. A )   &    |- ( ( ph /\ p e. Prime ) -> ( F ` p ) = ( G ` p ) )   =>    |- ( ph -> F = G )
Theorem	qabsabv 25318	The regular absolute value function on the rationals is in fact an absolute value under our definition. (Contributed by Mario Carneiro, 9-Sep-2014.)
|- Q = (ℂfld ↾s QQ )   &    |- A = (AbsVal ` Q )   =>    |- ( abs |` QQ ) e. A
Theorem	padicabv 25319*	The p-adic absolute value (with arbitrary base) is an absolute value. (Contributed by Mario Carneiro, 9-Sep-2014.)
|- Q = (ℂfld ↾s QQ )   &    |- A = (AbsVal ` Q )   &    |- F = ( x e. QQ |-> if ( x = 0 , 0 , ( N ^ ( P pCnt x ) ) ) )   =>    |- ( ( P e. Prime /\ N e. ( 0 (,) 1 ) ) -> F e. A )
Theorem	padicabvf 25320*	The p-adic absolute value is an absolute value. (Contributed by Mario Carneiro, 9-Sep-2014.)
|- Q = (ℂfld ↾s QQ )   &    |- A = (AbsVal ` Q )   &    |- J = ( q e. Prime |-> ( x e. QQ |-> if ( x = 0 , 0 , ( q ^ -u ( q pCnt x ) ) ) ) )   =>    |- J : Prime --> A
Theorem	padicabvcxp 25321*	All positive powers of the p-adic absolute value are absolute values. (Contributed by Mario Carneiro, 9-Sep-2014.)
|- Q = (ℂfld ↾s QQ )   &    |- A = (AbsVal ` Q )   &    |- J = ( q e. Prime |-> ( x e. QQ |-> if ( x = 0 , 0 , ( q ^ -u ( q pCnt x ) ) ) ) )   =>    |- ( ( P e. Prime /\ R e. RR+ ) -> ( y e. QQ |-> ( ( ( J ` P ) ` y ) ^c R ) ) e. A )
Theorem	ostth1 25322*	- Lemma for ostth 25328: trivial case. (Not that the proof is trivial, but that we are proving that the function is trivial.) If F is equal to 1 on the primes, then by complete induction and the multiplicative property abvmul 18829 of the absolute value, F is equal to 1 on all the integers, and ostthlem1 25316 extends this to the other rational numbers. (Contributed by Mario Carneiro, 10-Sep-2014.)
|- Q = (ℂfld ↾s QQ )   &    |- A = (AbsVal ` Q )   &    |- J = ( q e. Prime |-> ( x e. QQ |-> if ( x = 0 , 0 , ( q ^ -u ( q pCnt x ) ) ) ) )   &    |- K = ( x e. QQ |-> if ( x = 0 , 0 , 1 ) )   &    |- ( ph -> F e. A )   &    |- ( ph -> A. n e. NN -. 1 < ( F ` n ) )   &    |- ( ph -> A. n e. Prime -. ( F ` n ) < 1 )   =>    |- ( ph -> F = K )
Theorem	ostth2lem2 25323*	Lemma for ostth2 25326. (Contributed by Mario Carneiro, 10-Sep-2014.)
|- Q = (ℂfld ↾s QQ )   &    |- A = (AbsVal ` Q )   &    |- J = ( q e. Prime |-> ( x e. QQ |-> if ( x = 0 , 0 , ( q ^ -u ( q pCnt x ) ) ) ) )   &    |- K = ( x e. QQ |-> if ( x = 0 , 0 , 1 ) )   &    |- ( ph -> F e. A )   &    |- ( ph -> N e. ( ZZ>= ` 2 ) )   &    |- ( ph -> 1 < ( F ` N ) )   &    |- R = ( ( log ` ( F ` N ) ) / ( log ` N ) )   &    |- ( ph -> M e. ( ZZ>= ` 2 ) )   &    |- S = ( ( log ` ( F ` M ) ) / ( log ` M ) )   &    |- T = if ( ( F ` M ) <_ 1 , 1 , ( F ` M ) )   =>    |- ( ( ph /\ X e. NN0 /\ Y e. ( 0 ... ( ( M ^ X ) - 1 ) ) ) -> ( F ` Y ) <_ ( ( M x. X ) x. ( T ^ X ) ) )
Theorem	ostth2lem3 25324*	Lemma for ostth2 25326. (Contributed by Mario Carneiro, 10-Sep-2014.)
|- Q = (ℂfld ↾s QQ )   &    |- A = (AbsVal ` Q )   &    |- J = ( q e. Prime |-> ( x e. QQ |-> if ( x = 0 , 0 , ( q ^ -u ( q pCnt x ) ) ) ) )   &    |- K = ( x e. QQ |-> if ( x = 0 , 0 , 1 ) )   &    |- ( ph -> F e. A )   &    |- ( ph -> N e. ( ZZ>= ` 2 ) )   &    |- ( ph -> 1 < ( F ` N ) )   &    |- R = ( ( log ` ( F ` N ) ) / ( log ` N ) )   &    |- ( ph -> M e. ( ZZ>= ` 2 ) )   &    |- S = ( ( log ` ( F ` M ) ) / ( log ` M ) )   &    |- T = if ( ( F ` M ) <_ 1 , 1 , ( F ` M ) )   &    |- U = ( ( log ` N ) / ( log ` M ) )   =>    |- ( ( ph /\ X e. NN ) -> ( ( ( F ` N ) / ( T ^c U ) ) ^ X ) <_ ( X x. ( ( M x. T ) x. ( U + 1 ) ) ) )
Theorem	ostth2lem4 25325*	Lemma for ostth2 25326. (Contributed by Mario Carneiro, 10-Sep-2014.)
|- Q = (ℂfld ↾s QQ )   &    |- A = (AbsVal ` Q )   &    |- J = ( q e. Prime |-> ( x e. QQ |-> if ( x = 0 , 0 , ( q ^ -u ( q pCnt x ) ) ) ) )   &    |- K = ( x e. QQ |-> if ( x = 0 , 0 , 1 ) )   &    |- ( ph -> F e. A )   &    |- ( ph -> N e. ( ZZ>= ` 2 ) )   &    |- ( ph -> 1 < ( F ` N ) )   &    |- R = ( ( log ` ( F ` N ) ) / ( log ` N ) )   &    |- ( ph -> M e. ( ZZ>= ` 2 ) )   &    |- S = ( ( log ` ( F ` M ) ) / ( log ` M ) )   &    |- T = if ( ( F ` M ) <_ 1 , 1 , ( F ` M ) )   &    |- U = ( ( log ` N ) / ( log ` M ) )   =>    |- ( ph -> ( 1 < ( F ` M ) /\ R <_ S ) )
Theorem	ostth2 25326*	- Lemma for ostth 25328: regular case. (Contributed by Mario Carneiro, 10-Sep-2014.)
|- Q = (ℂfld ↾s QQ )   &    |- A = (AbsVal ` Q )   &    |- J = ( q e. Prime |-> ( x e. QQ |-> if ( x = 0 , 0 , ( q ^ -u ( q pCnt x ) ) ) ) )   &    |- K = ( x e. QQ |-> if ( x = 0 , 0 , 1 ) )   &    |- ( ph -> F e. A )   &    |- ( ph -> N e. ( ZZ>= ` 2 ) )   &    |- ( ph -> 1 < ( F ` N ) )   &    |- R = ( ( log ` ( F ` N ) ) / ( log ` N ) )   =>    |- ( ph -> E. a e. ( 0 (,] 1 ) F = ( y e. QQ |-> ( ( abs ` y ) ^c a ) ) )
Theorem	ostth3 25327*	- Lemma for ostth 25328: p-adic case. (Contributed by Mario Carneiro, 10-Sep-2014.)
|- Q = (ℂfld ↾s QQ )   &    |- A = (AbsVal ` Q )   &    |- J = ( q e. Prime |-> ( x e. QQ |-> if ( x = 0 , 0 , ( q ^ -u ( q pCnt x ) ) ) ) )   &    |- K = ( x e. QQ |-> if ( x = 0 , 0 , 1 ) )   &    |- ( ph -> F e. A )   &    |- ( ph -> A. n e. NN -. 1 < ( F ` n ) )   &    |- ( ph -> P e. Prime )   &    |- ( ph -> ( F ` P ) < 1 )   &    |- R = -u ( ( log ` ( F ` P ) ) / ( log ` P ) )   &    |- S = if ( ( F ` P ) <_ ( F ` p ) , ( F ` p ) , ( F ` P ) )   =>    |- ( ph -> E. a e. RR+ F = ( y e. QQ |-> ( ( ( J ` P ) ` y ) ^c a ) ) )
Theorem	ostth 25328*	Ostrowski's theorem, which classifies all absolute values on QQ. Any such absolute value must either be the trivial absolute value K, a constant exponent 0 < a <_ 1 times the regular absolute value, or a positive exponent times the p-adic absolute value. (Contributed by Mario Carneiro, 10-Sep-2014.)
|- Q = (ℂfld ↾s QQ )   &    |- A = (AbsVal ` Q )   &    |- J = ( q e. Prime |-> ( x e. QQ |-> if ( x = 0 , 0 , ( q ^ -u ( q pCnt x ) ) ) ) )   &    |- K = ( x e. QQ |-> if ( x = 0 , 0 , 1 ) )   =>    |- ( F e. A <-> ( F = K \/ E. a e. ( 0 (,] 1 ) F = ( y e. QQ |-> ( ( abs ` y ) ^c a ) ) \/ E. a e. RR+ E. g e. ran J F = ( y e. QQ |-> ( ( g ` y ) ^c a ) ) ) )
PART 15  ELEMENTARY GEOMETRY 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 f is a set (of points) ( Base ` f ) together with functions (Itv ` f ) and ( dist ` f ) on ( ( Base ` f ) X. ( Base ` f ) ) satisfying certain axioms (given in the definitions df-trkg 25352 et sequentes). This allows us to treat a Tarski structure as a special kind of extensible structure (see df-struct 15859). The translation to and from Tarski's treatment is as follows (given, again, informally). Suppose that one is given an extensible structure f. One defines a betweenness ternary predicate Btw by positing that, for any x , y , z e. ( Base ` f ), one has "Btw x y z " if and only if y e. x (Itv ` f ) z, and a congruence quaternary predicate Congr by positing that, for any x , y , z , t e. ( Base ` f ), one has "Congr x y z t " if and only if x ( dist ` f ) y = z ( dist ` f ) t. It is easy to check that if f satisfies our Tarski axioms, then Btw and Congr satisfy Tarski's Tarski axioms when ( Base ` f ) is interpreted as the universe of discourse. Conversely, suppose that one is given a set a, a ternary predicate Btw, and a quaternary predicate Congr. One defines the extensible structure f such that ( Base ` f ) is a, and (Itv ` f ) is the function which associates with each <. x , y >. e. ( a X. a ) the set of points z e. a such that "Btw x z y", and ( dist ` f ) is the function which associates with each <. x , y >. e. ( a X. a ) the set of ordered pairs <. z , t >. e. ( a X. a ) such that "Congr x y z t". It is easy to check that if Btw and Congr satisfy Tarski's Tarski axioms when a is interpreted as the universe of discourse, then f satisfies our Tarski axioms. We intentionally choose to represent congruence (without loss of generality) as x ( dist ` f ) y = z ( dist ` f ) t instead of "Congr x y z t", 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. A similar representation 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 http://www.michaelbeeson.com/research/FormalTarski/. 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 ph ->) by insert a T. -> in each hypothesis, using a1i 11, then using trud 1493 to remove the final T. -> 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 477, the theorem as stated, and ex 450. 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 25352), of "Euclidean dimensionless Tarski structures" (df-trkge 25350) and of "Tarski structures of dimension no less than N" (df-trkgld 25351). 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.
15.1  Definition and Tarski's Axioms of Geometry
Syntax	cstrkg 25329	Extends class notation with the class of Tarski geometries.
class TarskiG
Syntax	cstrkgc 25330	Extends class notation with the class of geometries fulfilling the congruence axioms.
class TarskiGC
Syntax	cstrkgb 25331	Extends class notation with the class of geometries fulfilling the betweenness axioms.
class TarskiGB
Syntax	cstrkgcb 25332	Extends class notation with the class of geometries fulfilling the congruence and betweenness axioms.
class TarskiGCB
Syntax	cstrkgld 25333	Extends class notation with the relation for geometries fulfilling the lower dimension axioms.
class DimTarskiG≥
Syntax	cstrkge 25334	Extends class notation with the class of geometries fulfilling Euclid's axiom.
class TarskiGE
Syntax	citv 25335	Declare the syntax for the Interval (segment) index extractor.
class Itv
Syntax	clng 25336	Declare the syntax for the Line function.
class LineG
Definition	df-itv 25337	Define the Interval (segment) index extractor for Tarski geometries. (Contributed by Thierry Arnoux, 24-Aug-2017.)
|- Itv = Slot ; 1 6
Definition	df-lng 25338	Define the line index extractor for geometries. (Contributed by Thierry Arnoux, 27-Mar-2019.)
|- LineG = Slot ; 1 7
Theorem	itvndx 25339	Index value of the Interval (segment) slot. Use ndxarg 15882. (Contributed by Thierry Arnoux, 24-Aug-2017.)
|- (Itv ` ndx ) = ; 1 6
Theorem	lngndx 25340	Index value of the "line" slot. Use ndxarg 15882. (Contributed by Thierry Arnoux, 27-Mar-2019.)
|- (LineG ` ndx ) = ; 1 7
Theorem	itvid 25341	Utility theorem: index-independent form of df-itv 25337. (Contributed by Thierry Arnoux, 24-Aug-2017.)
|- Itv = Slot (Itv ` ndx )
Theorem	lngid 25342	Utility theorem: index-independent form of df-lng 25338. (Contributed by Thierry Arnoux, 27-Mar-2019.)
|- LineG = Slot (LineG ` ndx )
Theorem	trkgstr 25343	Functionality of a Tarski geometry. (Contributed by Thierry Arnoux, 24-Aug-2017.)
|- W = { <. ( Base ` ndx ) , U >. , <. ( dist ` ndx ) , D >. , <. (Itv ` ndx ) , I >. }   =>    |- W Struct <. 1 , ; 1 6 >.
Theorem	trkgbas 25344	The base set of a Tarski geometry. (Contributed by Thierry Arnoux, 24-Aug-2017.)
|- W = { <. ( Base ` ndx ) , U >. , <. ( dist ` ndx ) , D >. , <. (Itv ` ndx ) , I >. }   =>    |- ( U e. V -> U = ( Base ` W ) )
Theorem	trkgdist 25345	The measure of a distance in a Tarski geometry. (Contributed by Thierry Arnoux, 24-Aug-2017.)
|- W = { <. ( Base ` ndx ) , U >. , <. ( dist ` ndx ) , D >. , <. (Itv ` ndx ) , I >. }   =>    |- ( D e. V -> D = ( dist ` W ) )
Theorem	trkgitv 25346	The congruence relation in a Tarski geometry. (Contributed by Thierry Arnoux, 24-Aug-2017.)
|- W = { <. ( Base ` ndx ) , U >. , <. ( dist ` ndx ) , D >. , <. (Itv ` ndx ) , I >. }   =>    |- ( I e. V -> I = (Itv ` W ) )
Definition	df-trkgc 25347*	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 2641, so it is not listed in this definition. (Contributed by Thierry Arnoux, 24-Aug-2017.)
|- TarskiGC = { f | [. ( Base ` f ) / p ]. [. ( dist ` f ) / d ]. ( A. x e. p A. y e. p ( x d y ) = ( y d x ) /\ A. x e. p A. y e. p A. z e. p ( ( x d y ) = ( z d z ) -> x = y ) ) }
Definition	df-trkgb 25348*	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 = { f | [. ( Base ` f ) / p ]. [. (Itv ` f ) / i ]. ( A. x e. p A. y e. p ( y e. ( x i x ) -> x = y ) /\ A. x e. p A. y e. p A. z e. p A. u e. p A. v e. p ( ( u e. ( x i z ) /\ v e. ( y i z ) ) -> E. a e. p ( a e. ( u i y ) /\ a e. ( v i x ) ) ) /\ A. s e. ~P p A. t e. ~P p ( E. a e. p A. x e. s A. y e. t x e. ( a i y ) -> E. b e. p A. x e. s A. y e. t b e. ( x i y ) ) ) }
Definition	df-trkgcb 25349*	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 = { f | [. ( Base ` f ) / p ]. [. ( dist ` f ) / d ]. [. (Itv ` f ) / i ]. ( A. x e. p A. y e. p A. z e. p A. u e. p A. a e. p A. b e. p A. c e. p A. v e. p ( ( ( x =/= y /\ y e. ( x i z ) /\ b e. ( a i c ) ) /\ ( ( ( x d y ) = ( a d b ) /\ ( y d z ) = ( b d c ) ) /\ ( ( x d u ) = ( a d v ) /\ ( y d u ) = ( b d v ) ) ) ) -> ( z d u ) = ( c d v ) ) /\ A. x e. p A. y e. p A. a e. p A. b e. p E. z e. p ( y e. ( x i z ) /\ ( y d z ) = ( a d b ) ) ) }
Definition	df-trkge 25350*	Define the class of geometries fulfilling Euclid's axiom, Axiom A10 of [Schwabhauser] p. 13. (Contributed by Thierry Arnoux, 14-Mar-2019.)
|- TarskiGE = { f | [. ( Base ` f ) / p ]. [. (Itv ` f ) / i ]. A. x e. p A. y e. p A. z e. p A. u e. p A. v e. p ( ( u e. ( x i v ) /\ u e. ( y i z ) /\ x =/= u ) -> E. a e. p E. b e. p ( y e. ( x i a ) /\ z e. ( x i b ) /\ v e. ( a i b ) ) ) }
Definition	df-trkgld 25351*	Define the class of geometries fulfilling the lower dimension axiom for dimension n. For such geometries, there are three non-colinear points that are equidistant from n - 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≥ = { <. g , n >. | [. ( Base ` g ) / p ]. [. ( dist ` g ) / d ]. [. (Itv ` g ) / i ]. E. f ( f : ( 1..^ n ) -1-1-> p /\ E. x e. p E. y e. p E. z e. p ( A. j e. ( 2..^ n ) ( ( ( f ` 1 ) d x ) = ( ( f ` j ) d x ) /\ ( ( f ` 1 ) d y ) = ( ( f ` j ) d y ) /\ ( ( f ` 1 ) d z ) = ( ( f ` j ) d z ) ) /\ -. ( z e. ( x i y ) \/ x e. ( z i y ) \/ y e. ( x i z ) ) ) ) }
Definition	df-trkg 25352*	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: for congruence, ( x .- y ) = ( z .- w ) where .- = ( dist ` W ) for betweenness, y e. ( x I z ), where I = (Itv ` W ) With this definition, the axiom A2 is actually equivalent to the transitivity of addition, eqtrd 2656. Tarski originally had more axioms, but later reduced his list to 11: A1 A kind of reflexivity for the congruence relation (TarskiGC) A2 Transitivity for the congruence relation (TarskiGC) A3 Identity for the congruence relation (TarskiGC) A4 Axiom of segment construction (TarskiGCB) A5 5-segment axiom (TarskiGCB) A6 Identity for the betweenness relation (TarskiGB) A7 Axiom of Pasch (TarskiGB) A8 Lower dimension axiom (DimTarskiG≥ ` 2 ) A9 Upper dimension axiom ( _V \ (DimTarskiG≥ ` 3 ) ) A10 Euclid's axiom (TarskiGE) A11 Axiom of continuity (TarskiGB) Our definition is split into 5 parts: congruence axioms TarskiGC (which metric spaces fulfill) betweenness axioms TarskiGB congruence and betweenness axioms TarskiGCB upper and lower dimension axioms DimTarskiG≥ axiom of Euclid / parallel postulate TarskiGE 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 i^i TarskiGB ) i^i (TarskiGCB i^i { f | [. ( Base ` f ) / p ]. [. (Itv ` f ) / i ]. (LineG ` f ) = ( x e. p , y e. ( p \ { x } ) |-> { z e. p | ( z e. ( x i y ) \/ x e. ( z i y ) \/ y e. ( x i z ) ) } ) } ) )
Theorem	istrkgc 25353*	Property of being a Tarski geometry - congruence part. (Contributed by Thierry Arnoux, 14-Mar-2019.)
|- P = ( Base ` G )   &    |- .- = ( dist ` G )   &    |- I = (Itv ` G )   =>    |- ( G e. TarskiGC <-> ( G e. _V /\ ( A. x e. P A. y e. P ( x .- y ) = ( y .- x ) /\ A. x e. P A. y e. P A. z e. P ( ( x .- y ) = ( z .- z ) -> x = y ) ) ) )
Theorem	istrkgb 25354*	Property of being a Tarski geometry - betweenness part. (Contributed by Thierry Arnoux, 14-Mar-2019.)
|- P = ( Base ` G )   &    |- .- = ( dist ` G )   &    |- I = (Itv ` G )   =>    |- ( G e. TarskiGB <-> ( G e. _V /\ ( A. x e. P A. y e. P ( y e. ( x I x ) -> x = y ) /\ A. x e. P A. y e. P A. z e. P A. u e. P A. v e. P ( ( u e. ( x I z ) /\ v e. ( y I z ) ) -> E. a e. P ( a e. ( u I y ) /\ a e. ( v I x ) ) ) /\ A. s e. ~P P A. t e. ~P P ( E. a e. P A. x e. s A. y e. t x e. ( a I y ) -> E. b e. P A. x e. s A. y e. t b e. ( x I y ) ) ) ) )
Theorem	istrkgcb 25355*	Property of being a Tarski geometry - congruence and betweenness part. (Contributed by Thierry Arnoux, 14-Mar-2019.)
|- P = ( Base ` G )   &    |- .- = ( dist ` G )   &    |- I = (Itv ` G )   =>    |- ( G e. TarskiGCB <-> ( G e. _V /\ ( A. x e. P A. y e. P A. z e. P A. u e. P A. a e. P A. b e. P A. c e. P A. v e. P ( ( ( x =/= y /\ y e. ( x I z ) /\ b e. ( a I c ) ) /\ ( ( ( x .- y ) = ( a .- b ) /\ ( y .- z ) = ( b .- c ) ) /\ ( ( x .- u ) = ( a .- v ) /\ ( y .- u ) = ( b .- v ) ) ) ) -> ( z .- u ) = ( c .- v ) ) /\ A. x e. P A. y e. P A. a e. P A. b e. P E. z e. P ( y e. ( x I z ) /\ ( y .- z ) = ( a .- b ) ) ) ) )
Theorem	istrkge 25356*	Property of fulfilling Euclid's axiom. (Contributed by Thierry Arnoux, 14-Mar-2019.)
|- P = ( Base ` G )   &    |- .- = ( dist ` G )   &    |- I = (Itv ` G )   =>    |- ( G e. TarskiGE <-> ( G e. _V /\ A. x e. P A. y e. P A. z e. P A. u e. P A. v e. P ( ( u e. ( x I v ) /\ u e. ( y I z ) /\ x =/= u ) -> E. a e. P E. b e. P ( y e. ( x I a ) /\ z e. ( x I b ) /\ v e. ( a I b ) ) ) ) )
Theorem	istrkgl 25357*	Building lines from the segment property. (Contributed by Thierry Arnoux, 14-Mar-2019.)
|- P = ( Base ` G )   &    |- .- = ( dist ` G )   &    |- I = (Itv ` G )   =>    |- ( G e. { f | [. ( Base ` f ) / p ]. [. (Itv ` f ) / i ]. (LineG ` f ) = ( x e. p , y e. ( p \ { x } ) |-> { z e. p | ( z e. ( x i y ) \/ x e. ( z i y ) \/ y e. ( x i z ) ) } ) } <-> ( G e. _V /\ (LineG ` G ) = ( x e. P , y e. ( P \ { x } ) |-> { z e. P | ( z e. ( x I y ) \/ x e. ( z I y ) \/ y e. ( x I z ) ) } ) ) )
Theorem	istrkgld 25358*	Property of fulfilling the lower dimension N axiom. (Contributed by Thierry Arnoux, 20-Nov-2019.)
|- P = ( Base ` G )   &    |- .- = ( dist ` G )   &    |- I = (Itv ` G )   =>    |- ( ( G e. V /\ N e. ( ZZ>= ` 2 ) ) -> ( GDimTarskiG≥ N <-> E. f ( f : ( 1..^ N ) -1-1-> P /\ E. x e. P E. y e. P E. z e. P ( A. j e. ( 2..^ N ) ( ( ( f ` 1 ) .- x ) = ( ( f ` j ) .- x ) /\ ( ( f ` 1 ) .- y ) = ( ( f ` j ) .- y ) /\ ( ( f ` 1 ) .- z ) = ( ( f ` j ) .- z ) ) /\ -. ( z e. ( x I y ) \/ x e. ( z I y ) \/ y e. ( x I z ) ) ) ) ) )
Theorem	istrkg2ld 25359*	Property of fulfilling the lower dimension 2 axiom. (Contributed by Thierry Arnoux, 20-Nov-2019.)
|- P = ( Base ` G )   &    |- .- = ( dist ` G )   &    |- I = (Itv ` G )   =>    |- ( G e. V -> ( GDimTarskiG≥ 2 <-> E. x e. P E. y e. P E. z e. P -. ( z e. ( x I y ) \/ x e. ( z I y ) \/ y e. ( x I z ) ) ) )
Theorem	istrkg3ld 25360*	Property of fulfilling the lower dimension 3 axiom. (Contributed by Thierry Arnoux, 12-Jul-2020.)
|- P = ( Base ` G )   &    |- .- = ( dist ` G )   &    |- I = (Itv ` G )   =>    |- ( G e. V -> ( GDimTarskiG≥ 3 <-> E. u e. P E. v e. P ( u =/= v /\ E. x e. P E. y e. P E. z e. P ( ( ( u .- x ) = ( v .- x ) /\ ( u .- y ) = ( v .- y ) /\ ( u .- z ) = ( v .- z ) ) /\ -. ( z e. ( x I y ) \/ x e. ( z I y ) \/ y e. ( x I z ) ) ) ) ) )
Theorem	axtgcgrrflx 25361	Axiom of reflexivity of congruence, Axiom A1 of [Schwabhauser] p. 10. (Contributed by Thierry Arnoux, 14-Mar-2019.)
|- P = ( Base ` G )   &    |- .- = ( dist ` G )   &    |- I = (Itv ` G )   &    |- ( ph -> G e. TarskiG )   &    |- ( ph -> X e. P )   &    |- ( ph -> Y e. P )   =>    |- ( ph -> ( X .- Y ) = ( Y .- X ) )
Theorem	axtgcgrid 25362	Axiom of identity of congruence, Axiom A3 of [Schwabhauser] p. 10. (Contributed by Thierry Arnoux, 14-Mar-2019.)
|- P = ( Base ` G )   &    |- .- = ( dist ` G )   &    |- I = (Itv ` G )   &    |- ( ph -> G e. TarskiG )   &    |- ( ph -> X e. P )   &    |- ( ph -> Y e. P )   &    |- ( ph -> Z e. P )   &    |- ( ph -> ( X .- Y ) = ( Z .- Z ) )   =>    |- ( ph -> X = Y )
Theorem	axtgsegcon 25363*	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 A B, one can construct a line segment congruent to it, starting at any point Y and going in the direction of any ray containing Y. The ray is determined by the point Y and a second point X, the endpoint of the ray. The other endpoint of the line segment to be constructed is just the point z whose existence is asserted." (Contributed by Thierry Arnoux, 15-Mar-2019.)
|- P = ( Base ` G )   &    |- .- = ( dist ` G )   &    |- I = (Itv ` G )   &    |- ( ph -> G e. TarskiG )   &    |- ( ph -> X e. P )   &    |- ( ph -> Y e. P )   &    |- ( ph -> A e. P )   &    |- ( ph -> B e. P )   =>    |- ( ph -> E. z e. P ( Y e. ( X I z ) /\ ( Y .- z ) = ( A .- B ) ) )
Theorem	axtg5seg 25364	Five segments axiom, Axiom A5 of [Schwabhauser] p. 11. Take two triangles X Z U and A C V, a point Y on X Z, and a point B on A C. If all corresponding line segments except for Z U and C V are congruent ( i.e., X Y .~ A B, Y Z .~ B C, X U .~ A V, and Y U .~ B V), then Z U and C V 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.)
|- P = ( Base ` G )   &    |- .- = ( dist ` G )   &    |- I = (Itv ` G )   &    |- ( ph -> G e. TarskiG )   &    |- ( ph -> X e. P )   &    |- ( ph -> Y e. P )   &    |- ( ph -> Z e. P )   &    |- ( ph -> A e. P )   &    |- ( ph -> B e. P )   &    |- ( ph -> C e. P )   &    |- ( ph -> U e. P )   &    |- ( ph -> V e. P )   &    |- ( ph -> X =/= Y )   &    |- ( ph -> Y e. ( X I Z ) )   &    |- ( ph -> B e. ( A I C ) )   &    |- ( ph -> ( X .- Y ) = ( A .- B ) )   &    |- ( ph -> ( Y .- Z ) = ( B .- C ) )   &    |- ( ph -> ( X .- U ) = ( A .- V ) )   &    |- ( ph -> ( Y .- U ) = ( B .- V ) )   =>    |- ( ph -> ( Z .- U ) = ( C .- V ) )
Theorem	axtgbtwnid 25365	Identity of Betweenness. Axiom A6 of [Schwabhauser] p. 11. (Contributed by Thierry Arnoux, 15-Mar-2019.)
|- P = ( Base ` G )   &    |- .- = ( dist ` G )   &    |- I = (Itv ` G )   &    |- ( ph -> G e. TarskiG )   &    |- ( ph -> X e. P )   &    |- ( ph -> Y e. P )   &    |- ( ph -> Y e. ( X I X ) )   =>    |- ( ph -> X = Y )
Theorem	axtgpasch 25366*	Axiom of (Inner) Pasch, Axiom A7 of [Schwabhauser] p. 12. Given triangle X Y Z, point U in segment X Z, and point V in segment Y Z, there exists a point a on both the segment U Y and the segment V X. 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.)
|- P = ( Base ` G )   &    |- .- = ( dist ` G )   &    |- I = (Itv ` G )   &    |- ( ph -> G e. TarskiG )   &    |- ( ph -> X e. P )   &    |- ( ph -> Y e. P )   &    |- ( ph -> Z e. P )   &    |- ( ph -> U e. P )   &    |- ( ph -> V e. P )   &    |- ( ph -> U e. ( X I Z ) )   &    |- ( ph -> V e. ( Y I Z ) )   =>    |- ( ph -> E. a e. P ( a e. ( U I Y ) /\ a e. ( V I X ) ) )
Theorem	axtgcont1 25367*	Axiom of Continuity. Axiom A11 of [Schwabhauser] p. 13. This axiom (scheme) asserts that any two sets S and T (of points) such that the elements of S precede the elements of T with respect to some point a (that is, x is between a and y whenever x is in X and y is in Y) are separated by some point b; this is explained in Axiom 11 of [Tarski1999] p. 185. (Contributed by Thierry Arnoux, 16-Mar-2019.)
|- P = ( Base ` G )   &    |- .- = ( dist ` G )   &    |- I = (Itv ` G )   &    |- ( ph -> G e. TarskiG )   &    |- ( ph -> S C_ P )   &    |- ( ph -> T C_ P )   =>    |- ( ph -> ( E. a e. P A. x e. S A. y e. T x e. ( a I y ) -> E. b e. P A. x e. S A. y e. T b e. ( x I y ) ) )
Theorem	axtgcont 25368*	Axiom of Continuity. Axiom A11 of [Schwabhauser] p. 13. For more information see axtgcont1 25367. (Contributed by Thierry Arnoux, 16-Mar-2019.)
|- P = ( Base ` G )   &    |- .- = ( dist ` G )   &    |- I = (Itv ` G )   &    |- ( ph -> G e. TarskiG )   &    |- ( ph -> S C_ P )   &    |- ( ph -> T C_ P )   &    |- ( ph -> A e. P )   &    |- ( ( ph /\ u e. S /\ v e. T ) -> u e. ( A I v ) )   =>    |- ( ph -> E. b e. P A. x e. S A. y e. T b e. ( x I y ) )
Theorem	axtglowdim2 25369*	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.)
|- P = ( Base ` G )   &    |- .- = ( dist ` G )   &    |- I = (Itv ` G )   &    |- ( ph -> G e. V )   &    |- ( ph -> GDimTarskiG≥ 2 )   =>    |- ( ph -> E. x e. P E. y e. P E. z e. P -. ( z e. ( x I y ) \/ x e. ( z I y ) \/ y e. ( x I z ) ) )
Theorem	axtgupdim2 25370	Upper dimension axiom for dimension 2, Axiom A9 of [Schwabhauser] p. 13. Three points X, Y and Z equidistant to two given two points U and V must be colinear. (Contributed by Thierry Arnoux, 29-May-2019.) (Revised by Thierry Arnoux, 11-Jul-2020.)
|- P = ( Base ` G )   &    |- .- = ( dist ` G )   &    |- I = (Itv ` G )   &    |- ( ph -> X e. P )   &    |- ( ph -> Y e. P )   &    |- ( ph -> Z e. P )   &    |- ( ph -> U e. P )   &    |- ( ph -> V e. P )   &    |- ( ph -> U =/= V )   &    |- ( ph -> ( U .- X ) = ( V .- X ) )   &    |- ( ph -> ( U .- Y ) = ( V .- Y ) )   &    |- ( ph -> ( U .- Z ) = ( V .- Z ) )   &    |- ( ph -> G e. V )   &    |- ( ph -> -. GDimTarskiG≥ 3 )   =>    |- ( ph -> ( Z e. ( X I Y ) \/ X e. ( Z I Y ) \/ Y e. ( X I Z ) ) )
Theorem	axtgeucl 25371*	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.)
|- P = ( Base ` G )   &    |- .- = ( dist ` G )   &    |- I = (Itv ` G )   &    |- ( ph -> G e. TarskiGE )   &    |- ( ph -> X e. P )   &    |- ( ph -> Y e. P )   &    |- ( ph -> Z e. P )   &    |- ( ph -> U e. P )   &    |- ( ph -> V e. P )   &    |- ( ph -> U e. ( X I V ) )   &    |- ( ph -> U e. ( Y I Z ) )   &    |- ( ph -> X =/= U )   =>    |- ( ph -> E. a e. P E. b e. P ( Y e. ( X I a ) /\ Z e. ( X I b ) /\ V e. ( a I b ) ) )
15.2  Tarskian Geometry
15.2.1  Congruence
Theorem	tgcgrcomimp 25372	Congruence commutes on the RHS. Theorem 2.5 of [Schwabhauser] p. 27. (Contributed by David A. Wheeler, 29-Jun-2020.)
|- P = ( Base ` G )   &    |- .- = ( dist ` G )   &    |- I = (Itv ` G )   &    |- ( ph -> G e. TarskiG )   &    |- ( ph -> A e. P )   &    |- ( ph -> B e. P )   &    |- ( ph -> C e. P )   &    |- ( ph -> D e. P )   =>    |- ( ph -> ( ( A .- B ) = ( C .- D ) -> ( A .- B ) = ( D .- C ) ) )
Theorem	tgcgrcomr 25373	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.)
|- P = ( Base ` G )   &    |- .- = ( dist ` G )   &    |- I = (Itv ` G )   &    |- ( ph -> G e. TarskiG )   &    |- ( ph -> A e. P )   &    |- ( ph -> B e. P )   &    |- ( ph -> C e. P )   &    |- ( ph -> D e. P )   &    |- ( ph -> ( A .- B ) = ( C .- D ) )   =>    |- ( ph -> ( A .- B ) = ( D .- C ) )
Theorem	tgcgrcoml 25374	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.)
|- P = ( Base ` G )   &    |- .- = ( dist ` G )   &    |- I = (Itv ` G )   &    |- ( ph -> G e. TarskiG )   &    |- ( ph -> A e. P )   &    |- ( ph -> B e. P )   &    |- ( ph -> C e. P )   &    |- ( ph -> D e. P )   &    |- ( ph -> ( A .- B ) = ( C .- D ) )   =>    |- ( ph -> ( B .- A ) = ( C .- D ) )
Theorem	tgcgrcomlr 25375	Congruence commutes on both sides. (Contributed by Thierry Arnoux, 23-Mar-2019.)
|- P = ( Base ` G )   &    |- .- = ( dist ` G )   &    |- I = (Itv ` G )   &    |- ( ph -> G e. TarskiG )   &    |- ( ph -> A e. P )   &    |- ( ph -> B e. P )   &    |- ( ph -> C e. P )   &    |- ( ph -> D e. P )   &    |- ( ph -> ( A .- B ) = ( C .- D ) )   =>    |- ( ph -> ( B .- A ) = ( D .- C ) )
Theorem	tgcgreqb 25376	Congruence and equality. (Contributed by Thierry Arnoux, 27-Aug-2019.)
|- P = ( Base ` G )   &    |- .- = ( dist ` G )   &    |- I = (Itv ` G )   &    |- ( ph -> G e. TarskiG )   &    |- ( ph -> A e. P )   &    |- ( ph -> B e. P )   &    |- ( ph -> C e. P )   &    |- ( ph -> D e. P )   &    |- ( ph -> ( A .- B ) = ( C .- D ) )   =>    |- ( ph -> ( A = B <-> C = D ) )
Theorem	tgcgreq 25377	Congruence and equality. (Contributed by Thierry Arnoux, 27-Aug-2019.)
|- P = ( Base ` G )   &    |- .- = ( dist ` G )   &    |- I = (Itv ` G )   &    |- ( ph -> G e. TarskiG )   &    |- ( ph -> A e. P )   &    |- ( ph -> B e. P )   &    |- ( ph -> C e. P )   &    |- ( ph -> D e. P )   &    |- ( ph -> ( A .- B ) = ( C .- D ) )   &    |- ( ph -> A = B )   =>    |- ( ph -> C = D )
Theorem	tgcgrneq 25378	Congruence and equality. (Contributed by Thierry Arnoux, 27-Aug-2019.)
|- P = ( Base ` G )   &    |- .- = ( dist ` G )   &    |- I = (Itv ` G )   &    |- ( ph -> G e. TarskiG )   &    |- ( ph -> A e. P )   &    |- ( ph -> B e. P )   &    |- ( ph -> C e. P )   &    |- ( ph -> D e. P )   &    |- ( ph -> ( A .- B ) = ( C .- D ) )   &    |- ( ph -> A =/= B )   =>    |- ( ph -> C =/= D )
Theorem	tgcgrtriv 25379	Degenerate segments are congruent. Theorem 2.8 of [Schwabhauser] p. 28. (Contributed by Thierry Arnoux, 23-Mar-2019.)
|- P = ( Base ` G )   &    |- .- = ( dist ` G )   &    |- I = (Itv ` G )   &    |- ( ph -> G e. TarskiG )   &    |- ( ph -> A e. P )   &    |- ( ph -> B e. P )   =>    |- ( ph -> ( A .- A ) = ( B .- B ) )
Theorem	tgcgrextend 25380	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.)
|- P = ( Base ` G )   &    |- .- = ( dist ` G )   &    |- I = (Itv ` G )   &    |- ( ph -> G e. TarskiG )   &    |- ( ph -> A e. P )   &    |- ( ph -> B e. P )   &    |- ( ph -> C e. P )   &    |- ( ph -> D e. P )   &    |- ( ph -> E e. P )   &    |- ( ph -> F e. P )   &    |- ( ph -> B e. ( A I C ) )   &    |- ( ph -> E e. ( D I F ) )   &    |- ( ph -> ( A .- B ) = ( D .- E ) )   &    |- ( ph -> ( B .- C ) = ( E .- F ) )   =>    |- ( ph -> ( A .- C ) = ( D .- F ) )
Theorem	tgsegconeq 25381	Two points that satisfy the conclusion of axtgsegcon 25363 are identical. Uniqueness portion of Theorem 2.12 of [Schwabhauser] p. 29. (Contributed by Thierry Arnoux, 23-Mar-2019.)
|- P = ( Base ` G )   &    |- .- = ( dist ` G )   &    |- I = (Itv ` G )   &    |- ( ph -> G e. TarskiG )   &    |- ( ph -> A e. P )   &    |- ( ph -> B e. P )   &    |- ( ph -> C e. P )   &    |- ( ph -> D e. P )   &    |- ( ph -> E e. P )   &    |- ( ph -> F e. P )   &    |- ( ph -> D =/= A )   &    |- ( ph -> A e. ( D I E ) )   &    |- ( ph -> A e. ( D I F ) )   &    |- ( ph -> ( A .- E ) = ( B .- C ) )   &    |- ( ph -> ( A .- F ) = ( B .- C ) )   =>    |- ( ph -> E = F )
15.2.2  Betweenness
Theorem	tgbtwntriv2 25382	Betweenness always holds for the second endpoint. Theorem 3.1 of [Schwabhauser] p. 30. (Contributed by Thierry Arnoux, 15-Mar-2019.)
|- P = ( Base ` G )   &    |- .- = ( dist ` G )   &    |- I = (Itv ` G )   &    |- ( ph -> G e. TarskiG )   &    |- ( ph -> A e. P )   &    |- ( ph -> B e. P )   =>    |- ( ph -> B e. ( A I B ) )
Theorem	tgbtwncom 25383	Betweenness commutes. Theorem 3.2 of [Schwabhauser] p. 30. (Contributed by Thierry Arnoux, 15-Mar-2019.)
|- P = ( Base ` G )   &    |- .- = ( dist ` G )   &    |- I = (Itv ` G )   &    |- ( ph -> G e. TarskiG )   &    |- ( ph -> A e. P )   &    |- ( ph -> B e. P )   &    |- ( ph -> C e. P )   &    |- ( ph -> B e. ( A I C ) )   =>    |- ( ph -> B e. ( C I A ) )
Theorem	tgbtwncomb 25384	Betweenness commutes, biconditional version. (Contributed by Thierry Arnoux, 3-Apr-2019.)
|- P = ( Base ` G )   &    |- .- = ( dist ` G )   &    |- I = (Itv ` G )   &    |- ( ph -> G e. TarskiG )   &    |- ( ph -> A e. P )   &    |- ( ph -> B e. P )   &    |- ( ph -> C e. P )   =>    |- ( ph -> ( B e. ( A I C ) <-> B e. ( C I A ) ) )
Theorem	tgbtwnne 25385	Betweenness and inequality. (Contributed by Thierry Arnoux, 1-Dec-2019.)
|- P = ( Base ` G )   &    |- .- = ( dist ` G )   &    |- I = (Itv ` G )   &    |- ( ph -> G e. TarskiG )   &    |- ( ph -> A e. P )   &    |- ( ph -> B e. P )   &    |- ( ph -> C e. P )   &    |- ( ph -> B e. ( A I C ) )   &    |- ( ph -> B =/= A )   =>    |- ( ph -> A =/= C )
Theorem	tgbtwntriv1 25386	Betweenness always holds for the first endpoint. Theorem 3.3 of [Schwabhauser] p. 30. (Contributed by Thierry Arnoux, 15-Mar-2019.)
|- P = ( Base ` G )   &    |- .- = ( dist ` G )   &    |- I = (Itv ` G )   &    |- ( ph -> G e. TarskiG )   &    |- ( ph -> A e. P )   &    |- ( ph -> B e. P )   =>    |- ( ph -> A e. ( A I B ) )
Theorem	tgbtwnswapid 25387	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.)
|- P = ( Base ` G )   &    |- .- = ( dist ` G )   &    |- I = (Itv ` G )   &    |- ( ph -> G e. TarskiG )   &    |- ( ph -> A e. P )   &    |- ( ph -> B e. P )   &    |- ( ph -> C e. P )   &    |- ( ph -> A e. ( B I C ) )   &    |- ( ph -> B e. ( A I C ) )   =>    |- ( ph -> A = B )
Theorem	tgbtwnintr 25388	Inner transitivity law for betweenness. Left-hand side of Theorem 3.5 of [Schwabhauser] p. 30. (Contributed by Thierry Arnoux, 18-Mar-2019.)
|- P = ( Base ` G )   &    |- .- = ( dist ` G )   &    |- I = (Itv ` G )   &    |- ( ph -> G e. TarskiG )   &    |- ( ph -> A e. P )   &    |- ( ph -> B e. P )   &    |- ( ph -> C e. P )   &    |- ( ph -> D e. P )   &    |- ( ph -> A e. ( B I D ) )   &    |- ( ph -> B e. ( C I D ) )   =>    |- ( ph -> B e. ( A I C ) )
Theorem	tgbtwnexch3 25389	Exchange the first endpoint in betweenness. Left-hand side of Theorem 3.6 of [Schwabhauser] p. 30. (Contributed by Thierry Arnoux, 18-Mar-2019.)
|- P = ( Base ` G )   &    |- .- = ( dist ` G )   &    |- I = (Itv ` G )   &    |- ( ph -> G e. TarskiG )   &    |- ( ph -> A e. P )   &    |- ( ph -> B e. P )   &    |- ( ph -> C e. P )   &    |- ( ph -> D e. P )   &    |- ( ph -> B e. ( A I C ) )   &    |- ( ph -> C e. ( A I D ) )   =>    |- ( ph -> C e. ( B I D ) )
Theorem	tgbtwnouttr2 25390	Outer transitivity law for betweenness. Left-hand side of Theorem 3.7 of [Schwabhauser] p. 30. (Contributed by Thierry Arnoux, 18-Mar-2019.)
|- P = ( Base ` G )   &    |- .- = ( dist ` G )   &    |- I = (Itv ` G )   &    |- ( ph -> G e. TarskiG )   &    |- ( ph -> A e. P )   &    |- ( ph -> B e. P )   &    |- ( ph -> C e. P )   &    |- ( ph -> D e. P )   &    |- ( ph -> B =/= C )   &    |- ( ph -> B e. ( A I C ) )   &    |- ( ph -> C e. ( B I D ) )   =>    |- ( ph -> C e. ( A I D ) )
Theorem	tgbtwnexch2 25391	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.)
|- P = ( Base ` G )   &    |- .- = ( dist ` G )   &    |- I = (Itv ` G )   &    |- ( ph -> G e. TarskiG )   &    |- ( ph -> A e. P )   &    |- ( ph -> B e. P )   &    |- ( ph -> C e. P )   &    |- ( ph -> D e. P )   &    |- ( ph -> B e. ( A I D ) )   &    |- ( ph -> C e. ( B I D ) )   =>    |- ( ph -> C e. ( A I D ) )
Theorem	tgbtwnouttr 25392	Outer transitivity law for betweenness. Right-hand side of Theorem 3.7 of [Schwabhauser] p. 30. (Contributed by Thierry Arnoux, 23-Mar-2019.)
|- P = ( Base ` G )   &    |- .- = ( dist ` G )   &    |- I = (Itv ` G )   &    |- ( ph -> G e. TarskiG )   &    |- ( ph -> A e. P )   &    |- ( ph -> B e. P )   &    |- ( ph -> C e. P )   &    |- ( ph -> D e. P )   &    |- ( ph -> B =/= C )   &    |- ( ph -> B e. ( A I C ) )   &    |- ( ph -> C e. ( B I D ) )   =>    |- ( ph -> B e. ( A I D ) )
Theorem	tgbtwnexch 25393	Outer transitivity law for betweenness. Right-hand side of Theorem 3.6 of [Schwabhauser] p. 30. (Contributed by Thierry Arnoux, 23-Mar-2019.)
|- P = ( Base ` G )   &    |- .- = ( dist ` G )   &    |- I = (Itv ` G )   &    |- ( ph -> G e. TarskiG )   &    |- ( ph -> A e. P )   &    |- ( ph -> B e. P )   &    |- ( ph -> C e. P )   &    |- ( ph -> D e. P )   &    |- ( ph -> B e. ( A I C ) )   &    |- ( ph -> C e. ( A I D ) )   =>    |- ( ph -> B e. ( A I D ) )
Theorem	tgtrisegint 25394*	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.)
|- P = ( Base ` G )   &    |- .- = ( dist ` G )   &    |- I = (Itv ` G )   &    |- ( ph -> G e. TarskiG )   &    |- ( ph -> A e. P )   &    |- ( ph -> B e. P )   &    |- ( ph -> C e. P )   &    |- ( ph -> D e. P )   &    |- ( ph -> E e. P )   &    |- ( ph -> F e. P )   &    |- ( ph -> B e. ( A I C ) )   &    |- ( ph -> E e. ( D I C ) )   &    |- ( ph -> F e. ( A I D ) )   =>    |- ( ph -> E. q e. P ( q e. ( F I C ) /\ q e. ( B I E ) ) )
15.2.3  Dimension
Theorem	tglowdim1 25395*	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 <_ ( # ` P ) to avoid a new definition, but a different convention could be chosen. (Contributed by Thierry Arnoux, 23-Mar-2019.)
|- P = ( Base ` G )   &    |- .- = ( dist ` G )   &    |- I = (Itv ` G )   &    |- ( ph -> G e. TarskiG )   &    |- ( ph -> 2 <_ ( # ` P ) )   =>    |- ( ph -> E. x e. P E. y e. P x =/= y )
Theorem	tglowdim1i 25396*	Lower dimension axiom for one dimension. (Contributed by Thierry Arnoux, 28-May-2019.)
|- P = ( Base ` G )   &    |- .- = ( dist ` G )   &    |- I = (Itv ` G )   &    |- ( ph -> G e. TarskiG )   &    |- ( ph -> 2 <_ ( # ` P ) )   &    |- ( ph -> X e. P )   =>    |- ( ph -> E. y e. P X =/= y )
Theorem	tgldimor 25397	Excluded-middle like statement allowing to treat dimension zero as a special case. (Contributed by Thierry Arnoux, 11-Apr-2019.)
|- P = ( E ` F )   &    |- ( ph -> A e. P )   =>    |- ( ph -> ( ( # ` P ) = 1 \/ 2 <_ ( # ` P ) ) )
Theorem	tgldim0eq 25398	In dimension zero, any two points are equal. (Contributed by Thierry Arnoux, 11-Apr-2019.)
|- P = ( E ` F )   &    |- ( ph -> ( # ` P ) = 1 )   &    |- ( ph -> A e. P )   &    |- ( ph -> B e. P )   =>    |- ( ph -> A = B )
Theorem	tgldim0itv 25399	In dimension zero, any two points are equal. (Contributed by Thierry Arnoux, 12-Apr-2019.)
|- P = ( Base ` G )   &    |- .- = ( dist ` G )   &    |- I = (Itv ` G )   &    |- ( ph -> G e. TarskiG )   &    |- ( ph -> A e. P )   &    |- ( ph -> B e. P )   &    |- ( ph -> C e. P )   &    |- ( ph -> ( # ` P ) = 1 )   =>    |- ( ph -> A e. ( B I C ) )
Theorem	tgldim0cgr 25400	In dimension zero, any two pairs of points are congruent. (Contributed by Thierry Arnoux, 12-Apr-2019.)
|- P = ( Base ` G )   &    |- .- = ( dist ` G )   &    |- I = (Itv ` G )   &    |- ( ph -> G e. TarskiG )   &    |- ( ph -> A e. P )   &    |- ( ph -> B e. P )   &    |- ( ph -> C e. P )   &    |- ( ph -> ( # ` P ) = 1 )   &    |- ( ph -> D e. P )   =>    |- ( ph -> ( A .- B ) = ( C .- D ) )