P. 239 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 23801-23900   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	ostth3 23801*	- Lemma for ostth 23802: 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 23802*	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 23828 et sequentes). This allows us to treat a Tarski structure as a special kind of extensible structure (see df-struct 14616). 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/. 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 23828), of "Euclidean dimensionless Tarski structures" (df-trkge 23825) and of "plane Euclidean Tarski structures" (df-trkg2d 23827). 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 the 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 23803	Extends class notation with the class of Tarski geometries.
class TarskiG
Syntax	cstrkgc 23804	Extends class notation with the class of geometries fulfilling the congruence axioms.
class TarskiGC
Syntax	cstrkgb 23805	Extends class notation with the class of geometries fulfilling the betweenness axioms.
class TarskiGB
Syntax	cstrkgcb 23806	Extends class notation with the class of geometries fulfilling the congruence and betweenness axioms.
class TarskiGCB
Syntax	cstrkgld 23807	Extends class notation with the relation for geometries fulfilling the lower dimension axioms.
class DimTarskiG≥
Syntax	cstrkg2d 23808	Extends class notation with the class of geometries fulfilling the planarity axioms.
class TarskiG2D
Syntax	cstrkge 23809	Extends class notation with the class of geometries fulfilling Euclid's axiom.
class TarskiGE
Syntax	citv 23810	Declare the syntax for the Interval (segment) index extractor.
class Itv
Syntax	clng 23811	Declare the syntax for the Line function.
class LineG
Definition	df-itv 23812	Define the Interval (segment) index extractor for Tarski geometries. (Contributed by Thierry Arnoux, 24-Aug-2017.)
|- Itv = Slot ; 1 6
Definition	df-lng 23813	Define the line index extractor for geometries. (Contributed by Thierry Arnoux, 27-Mar-2019.)
|- LineG = Slot ; 1 7
Theorem	itvndx 23814	Index value of the Interval (segment) slot. Use ndxarg 14634 (Contributed by Thierry Arnoux, 24-Aug-2017.)
|- (Itv ` ndx ) = ; 1 6
Theorem	lngndx 23815	Index value of the "line" slot. Use ndxarg 14634 (Contributed by Thierry Arnoux, 27-Mar-2019.)
|- (LineG ` ndx ) = ; 1 7
Theorem	itvid 23816	Utility theorem: index-independent form of df-itv 23812. (Contributed by Thierry Arnoux, 24-Aug-2017.)
|- Itv = Slot (Itv ` ndx )
Theorem	lngid 23817	Utility theorem: index-independent form of df-lng 23813. (Contributed by Thierry Arnoux, 27-Mar-2019.)
|- LineG = Slot (LineG ` ndx )
Theorem	trkgstr 23818	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 23819	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 23820	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 23821	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 23822*	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 2469, 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 23823*	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 23824*	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 23825*	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 23826*	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-trkg2d 23827*	Define the class of geometries fulfilling the lower dimension axiom, Axiom A8 of [Schwabhauser] p. 12, and the upper dimension axiom, Axiom A9 of [Schwabhauser] p. 13, for dimension 2. (Contributed by Thierry Arnoux, 14-Mar-2019.)
|- TarskiG2D = { f | [. ( Base ` f ) / p ]. [. ( dist ` f ) / d ]. [. (Itv ` f ) / i ]. ( 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 ) ) /\ A. x e. p A. y e. p A. z e. p A. u e. p A. v e. p ( ( ( ( x d u ) = ( x d v ) /\ ( y d u ) = ( y d v ) /\ ( z d u ) = ( z d v ) ) /\ u =/= v ) -> ( z e. ( x i y ) \/ x e. ( z i y ) \/ y e. ( x i z ) ) ) ) }
Definition	df-trkg 23828*	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 2484. 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 (TarskiGBC) A5 5-segment axiom (TarskiGBC) A6 Identity for the betweenness relation (TarskiGB) A7 Axiom of Pasch (TarskiGB) A8 Lower dimension axiom (TarskiG2D) A9 Upper dimension axiom (TarskiG2D) 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 TarskiG2D 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 23829*	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 23830*	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 23831*	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 23832*	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 23833*	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	istrkg2d 23834*	Property of fulfilling dimension 2 axiom (Contributed by Thierry Arnoux, 29-May-2019.)
|- P = ( Base ` G )   &    |- .- = ( dist ` G )   &    |- I = (Itv ` G )   =>    |- ( G e. TarskiG2D <-> ( G e. _V /\ ( 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 ) ) /\ A. x e. P A. y e. P A. z e. P A. u e. P A. v e. P ( ( ( ( x .- u ) = ( x .- v ) /\ ( y .- u ) = ( y .- v ) /\ ( z .- u ) = ( z .- v ) ) /\ u =/= v ) -> ( z e. ( x I y ) \/ x e. ( z I y ) \/ y e. ( x I z ) ) ) ) ) )
Theorem	istrkgld 23835*	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 23836*	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	axtgcgrrflx 23837	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 23838	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 23839*	Axiom of segment construction, Axiom A4 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 -> A e. P )   &    |- ( ph -> B e. P )   =>    |- ( ph -> E. z e. P ( Y e. ( X I z ) /\ ( Y .- z ) = ( A .- B ) ) )
Theorem	axtg5seg 23840	Five segments axiom, Axiom A5 of [Schwabhauser] p. 11. (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 23841	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 23842*	Axiom of Pasch, Axiom A7 of [Schwabhauser] p. 12. (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 23843*	Axiom of Continuity. Axiom A11 of [Schwabhauser] p. 13. (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 23844*	Axiom of Continuity. Axiom A11 of [Schwabhauser] p. 13. (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	axtglowdim2OLD 23845*	Lower dimension axiom for dimension 2, Axiom A8 of [Schwabhauser] p. 13. There exist 3 non-colinear points/ (Contributed by Thierry Arnoux, 29-May-2019.) (New usage is discouraged.) (Proof modification is discouraged.)
|- P = ( Base ` G )   &    |- .- = ( dist ` G )   &    |- I = (Itv ` G )   &    |- ( ph -> G e. TarskiG2D )   =>    |- ( 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	axtglowdim2 23846*	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 23847	Upper dimension axiom for dimension 2, Axiom A9 of [Schwabhauser] p. 13. (Contributed by Thierry Arnoux, 29-May-2019.)
|- P = ( Base ` G )   &    |- .- = ( dist ` G )   &    |- I = (Itv ` G )   &    |- ( ph -> G e. TarskiG2D )   &    |- ( ph -> X e. P )   &    |- ( ph -> Y e. P )   &    |- ( ph -> Z e. P )   &    |- ( ph -> U e. P )   &    |- ( ph -> V e. P )   &    |- ( ph -> U =/= V )   &    |- ( ph -> ( X .- U ) = ( X .- V ) )   &    |- ( ph -> ( Y .- U ) = ( Y .- V ) )   &    |- ( ph -> ( Z .- U ) = ( Z .- V ) )   =>    |- ( ph -> ( Z e. ( X I Y ) \/ X e. ( Z I Y ) \/ Y e. ( X I Z ) ) )
Theorem	axtgeucl 23848*	Euclid's Axiom. Axiom A10 of [Schwabhauser] p. 13. (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	tgcgrcomlr 23849	Congruence commutes on both sides. Theorem 2.5 of [Schwabhauser] p. 27. (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 23850	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 23851	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 23852	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 23853	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 23854	Link congruence over a pair of line segments. Theorem 2.11 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 -> 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 23855	Two points that satisfy the conclusion of axtgsegcon 23839 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 23856	Betweeness 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 23857	Betweeness 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 23858	Betweeness 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 23859	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 23860	Betweeness 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 23861	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 23862	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 23863	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 23864	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 23865	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 23866	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 23867	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 23868*	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 23869*	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 23870*	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 23871	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 23872	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 23873	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 23874	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 ) )
Theorem	tgbtwndiff 23875*	There is always a c distinct from B such that B lies between A and c. Theorem 3.14 of [Schwabhauser] p. 32. The condition "the space is of dimension 1 or more" is written here as 2 <_ ( # ` P ) for simplicity. (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 -> 2 <_ ( # ` P ) )   =>    |- ( ph -> E. c e. P ( B e. ( A I c ) /\ B =/= c ) )
Theorem	tgdim01 23876	In geometries of dimension lower than 2, all points are colinear. (Contributed by Thierry Arnoux, 27-Aug-2019.)
|- P = ( Base ` G )   &    |- I = (Itv ` G )   &    |- ( ph -> G e. V )   &    |- ( ph -> -. GDimTarskiG≥ 2 )   &    |- ( ph -> X e. P )   &    |- ( ph -> Y e. P )   &    |- ( ph -> Z e. P )   =>    |- ( ph -> ( Z e. ( X I Y ) \/ X e. ( Z I Y ) \/ Y e. ( X I Z ) ) )
Theorem	nehash2 23877	The cardinality of a set with two distinct elements. (Contributed by Thierry Arnoux, 27-Aug-2019.)
|- ( ph -> P e. V )   &    |- ( ph -> A e. P )   &    |- ( ph -> B e. P )   &    |- ( ph -> A =/= B )   =>    |- ( ph -> 2 <_ ( # ` P ) )
15.2.4  Betweenness and Congruence
Theorem	tgifscgr 23878	Inner five segment congruence. Take two triangles, A D C and E H K, with B between A and C and F between E and K. If the other components of the triangles are congruent, then so are B D and F H. Theorem 4.2 of [Schwabhauser] p. 34. (Contributed by Thierry Arnoux, 24-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 -> K e. P )   &    |- ( ph -> H e. P )   &    |- ( ph -> B e. ( A I C ) )   &    |- ( ph -> F e. ( E I K ) )   &    |- ( ph -> ( A .- C ) = ( E .- K ) )   &    |- ( ph -> ( B .- C ) = ( F .- K ) )   &    |- ( ph -> ( A .- D ) = ( E .- H ) )   &    |- ( ph -> ( C .- D ) = ( K .- H ) )   =>    |- ( ph -> ( B .- D ) = ( F .- H ) )
Theorem	tgcgrsub 23879	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.)
|- 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 .- C ) = ( D .- F ) )   &    |- ( ph -> ( B .- C ) = ( E .- F ) )   =>    |- ( ph -> ( A .- B ) = ( D .- E ) )
15.2.5  Congruence of a series of points
Syntax	ccgrg 23880	Declare the constant for the congruence between shapes relation.
class cgrG
Definition	df-cgrg 23881*	Define the relation congruence bewteen shapes. Definition 4.4 of [Schwabhauser] p. 35. Ideally, we would define this for functions of any set, but we will used words (functions over NN) in most cases. (Contributed by Thierry Arnoux, 3-Apr-2019.)
|- cgrG = ( g e. _V |-> { <. a , b >. | ( ( a e. ( ( Base ` g ) ^pm RR ) /\ b e. ( ( Base ` g ) ^pm RR ) ) /\ ( dom a = dom b /\ A. i e. dom a A. j e. dom a ( ( a ` i ) ( dist ` g ) ( a ` j ) ) = ( ( b ` i ) ( dist ` g ) ( b ` j ) ) ) ) } )
Theorem	iscgrg 23882*	The congruence property for sequences of points. (Contributed by Thierry Arnoux, 3-Apr-2019.)
|- P = ( Base ` G )   &    |- .- = ( dist ` G )   &    |- .~ = (cgrG ` G )   =>    |- ( G e. V -> ( A .~ B <-> ( ( A e. ( P ^pm RR ) /\ B e. ( P ^pm RR ) ) /\ ( dom A = dom B /\ A. i e. dom A A. j e. dom A ( ( A ` i ) .- ( A ` j ) ) = ( ( B ` i ) .- ( B ` j ) ) ) ) ) )
Theorem	iscgrgd 23883*	The property for two sequences A and B of points to be congruent. (Contributed by Thierry Arnoux, 3-Apr-2019.)
|- P = ( Base ` G )   &    |- .- = ( dist ` G )   &    |- .~ = (cgrG ` G )   &    |- ( ph -> G e. V )   &    |- ( ph -> D C_ RR )   &    |- ( ph -> A : D --> P )   &    |- ( ph -> B : D --> P )   =>    |- ( ph -> ( A .~ B <-> A. i e. dom A A. j e. dom A ( ( A ` i ) .- ( A ` j ) ) = ( ( B ` i ) .- ( B ` j ) ) ) )
Theorem	trgcgrg 23884	The property for two triangles to be congruent to each other. (Contributed by Thierry Arnoux, 3-Apr-2019.)
|- P = ( Base ` G )   &    |- .- = ( dist ` G )   &    |- .~ = (cgrG ` 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 -> ( <" A B C "> .~ <" D E F "> <-> ( ( A .- B ) = ( D .- E ) /\ ( B .- C ) = ( E .- F ) /\ ( C .- A ) = ( F .- D ) ) ) )
Theorem	trgcgr 23885	Triangle congruence. (Contributed by Thierry Arnoux, 27-Apr-2019.)
|- P = ( Base ` G )   &    |- .- = ( dist ` G )   &    |- .~ = (cgrG ` 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 -> ( A .- B ) = ( D .- E ) )   &    |- ( ph -> ( B .- C ) = ( E .- F ) )   &    |- ( ph -> ( C .- A ) = ( F .- D ) )   =>    |- ( ph -> <" A B C "> .~ <" D E F "> )
Theorem	ercgrg 23886	The shape congruence relation is an equivalence relation. Statement 4.4 of [Schwabhauser] p. 35. (Contributed by Thierry Arnoux, 9-Apr-2019.)
|- P = ( Base ` G )   =>    |- ( G e. TarskiG -> (cgrG ` G ) Er ( P ^pm RR ) )
Theorem	tgcgrxfr 23887*	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.)
|- P = ( Base ` G )   &    |- .- = ( dist ` G )   &    |- I = (Itv ` G )   &    |- .~ = (cgrG ` G )   &    |- ( ph -> G e. TarskiG )   &    |- ( ph -> A e. P )   &    |- ( ph -> B e. P )   &    |- ( ph -> C e. P )   &    |- ( ph -> D e. P )   &    |- ( ph -> F e. P )   &    |- ( ph -> B e. ( A I C ) )   &    |- ( ph -> ( A .- C ) = ( D .- F ) )   =>    |- ( ph -> E. e e. P ( e e. ( D I F ) /\ <" A B C "> .~ <" D e F "> ) )
Theorem	cgr3id 23888	Reflexivity law for three-place congruence. (Contributed by Thierry Arnoux, 28-Apr-2019.)
|- P = ( Base ` G )   &    |- .- = ( dist ` G )   &    |- I = (Itv ` G )   &    |- .~ = (cgrG ` G )   &    |- ( ph -> G e. TarskiG )   &    |- ( ph -> A e. P )   &    |- ( ph -> B e. P )   &    |- ( ph -> C e. P )   =>    |- ( ph -> <" A B C "> .~ <" A B C "> )
Theorem	cgr3simp1 23889	Deduce segment congruence from a triangle congruence (Contributed by Thierry Arnoux, 27-Apr-2019.)
|- P = ( Base ` G )   &    |- .- = ( dist ` G )   &    |- I = (Itv ` G )   &    |- .~ = (cgrG ` 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 -> <" A B C "> .~ <" D E F "> )   =>    |- ( ph -> ( A .- B ) = ( D .- E ) )
Theorem	cgr3simp2 23890	Deduce segment congruence from a triangle congruence (Contributed by Thierry Arnoux, 27-Apr-2019.)
|- P = ( Base ` G )   &    |- .- = ( dist ` G )   &    |- I = (Itv ` G )   &    |- .~ = (cgrG ` 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 -> <" A B C "> .~ <" D E F "> )   =>    |- ( ph -> ( B .- C ) = ( E .- F ) )
Theorem	cgr3simp3 23891	Deduce segment congruence from a triangle congruence (Contributed by Thierry Arnoux, 27-Apr-2019.)
|- P = ( Base ` G )   &    |- .- = ( dist ` G )   &    |- I = (Itv ` G )   &    |- .~ = (cgrG ` 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 -> <" A B C "> .~ <" D E F "> )   =>    |- ( ph -> ( C .- A ) = ( F .- D ) )
Theorem	cgr3swap12 23892	Permutation law for three-place congruence. (Contributed by Thierry Arnoux, 27-Apr-2019.)
|- P = ( Base ` G )   &    |- .- = ( dist ` G )   &    |- I = (Itv ` G )   &    |- .~ = (cgrG ` 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 -> <" A B C "> .~ <" D E F "> )   =>    |- ( ph -> <" B A C "> .~ <" E D F "> )
Theorem	cgr3swap23 23893	Permutation law for three-place congruence. (Contributed by Thierry Arnoux, 27-Apr-2019.)
|- P = ( Base ` G )   &    |- .- = ( dist ` G )   &    |- I = (Itv ` G )   &    |- .~ = (cgrG ` 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 -> <" A B C "> .~ <" D E F "> )   =>    |- ( ph -> <" A C B "> .~ <" D F E "> )
Theorem	trgcgrcom 23894	Commutative law for three-place congruence. (Contributed by Thierry Arnoux, 27-Apr-2019.)
|- P = ( Base ` G )   &    |- .- = ( dist ` G )   &    |- I = (Itv ` G )   &    |- .~ = (cgrG ` 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 -> <" A B C "> .~ <" D E F "> )   =>    |- ( ph -> <" D E F "> .~ <" A B C "> )
Theorem	cgr3tr 23895	Transitivity law for three-place congruence. (Contributed by Thierry Arnoux, 27-Apr-2019.)
|- P = ( Base ` G )   &    |- .- = ( dist ` G )   &    |- I = (Itv ` G )   &    |- .~ = (cgrG ` 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 -> <" A B C "> .~ <" D E F "> )   &    |- ( ph -> J e. P )   &    |- ( ph -> K e. P )   &    |- ( ph -> L e. P )   &    |- ( ph -> <" D E F "> .~ <" J K L "> )   =>    |- ( ph -> <" A B C "> .~ <" J K L "> )
Theorem	tgbtwnxfr 23896	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.)
|- P = ( Base ` G )   &    |- .- = ( dist ` G )   &    |- I = (Itv ` G )   &    |- .~ = (cgrG ` 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 -> <" A B C "> .~ <" D E F "> )   &    |- ( ph -> B e. ( A I C ) )   =>    |- ( ph -> E e. ( D I F ) )
15.2.6  Motions
Syntax	cismt 23897	Declare the constant for the isometry builder.
class Ismt
Definition	df-ismt 23898*	Define the set of isometries between two structures. Definition 4.8 of [Schwabhauser] p. 36. (Contributed by Thierry Arnoux, 13-Dec-2019.)
|- Ismt = ( g e. _V , h e. _V |-> { f | ( f : ( Base ` g ) -1-1-onto-> ( Base ` h ) /\ A. a e. ( Base ` g ) A. b e. ( Base ` g ) ( ( f ` a ) ( dist ` h ) ( f ` b ) ) = ( a ( dist ` g ) b ) ) } )
Theorem	isismt 23899*	Property of being an isometry. Compare with isismty 30273 (Contributed by Thierry Arnoux, 13-Dec-2019.)
|- B = ( Base ` G )   &    |- P = ( Base ` H )   &    |- D = ( dist ` G )   &    |- .- = ( dist ` H )   =>    |- ( ( G e. V /\ H e. W ) -> ( F e. ( GIsmt H ) <-> ( F : B -1-1-onto-> P /\ A. a e. B A. b e. B ( ( F ` a ) .- ( F ` b ) ) = ( a D b ) ) ) )
Theorem	ismot 23900*	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.)
|- P = ( Base ` G )   &    |- .- = ( dist ` G )   =>    |- ( G e. V -> ( F e. ( GIsmt G ) <-> ( F : P -1-1-onto-> P /\ A. a e. P A. b e. P ( ( F ` a ) .- ( F ` b ) ) = ( a .- b ) ) ) )