P. 255 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 25401-25500   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	tgbtwndiff 25401*	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 25402	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 ) ) )
15.2.4  Betweenness and Congruence
Theorem	tgifscgr 25403	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 25404	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 25405	Declare the constant for the congruence between shapes relation.
class cgrG
Definition	df-cgrg 25406*	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 25407*	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 25408*	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	iscgrglt 25409*	The property for two sequences A and B of points to be congruent, where the congruence is only required for indices verifying a less-than relation. (Contributed by Thierry Arnoux, 7-Oct-2020.)
|- P = ( Base ` G )   &    |- .- = ( dist ` G )   &    |- .~ = (cgrG ` G )   &    |- ( ph -> G e. TarskiG )   &    |- ( 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 ( i < j -> ( ( A ` i ) .- ( A ` j ) ) = ( ( B ` i ) .- ( B ` j ) ) ) ) )
Theorem	trgcgrg 25410	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 25411	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 25412	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 25413*	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 25414	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 25415	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 25416	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 25417	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 25418	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 25419	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	cgr3swap13 25420	Permutation law for three-place congruence. (Contributed by Thierry Arnoux, 3-Oct-2020.)
|- 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 B A "> .~ <" F E D "> )
Theorem	cgr3rotr 25421	Permutation law for three-place congruence. (Contributed by Thierry Arnoux, 1-Aug-2020.)
|- 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 B "> .~ <" F D E "> )
Theorem	cgr3rotl 25422	Permutation law for three-place congruence. (Contributed by Thierry Arnoux, 1-Aug-2020.)
|- 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 A "> .~ <" E F D "> )
Theorem	trgcgrcom 25423	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 25424	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 25425	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 ) )
Theorem	tgcgr4 25426	Two quadrilaterals to be congruent to each other if one triangle formed by their vertices is, and the additional points are equidistant too. (Contributed by Thierry Arnoux, 8-Oct-2020.)
|- 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 -> W e. P )   &    |- ( ph -> X e. P )   &    |- ( ph -> Y e. P )   &    |- ( ph -> Z e. P )   =>    |- ( ph -> ( <" A B C D "> .~ <" W X Y Z "> <-> ( <" A B C "> .~ <" W X Y "> /\ ( ( A .- D ) = ( W .- Z ) /\ ( B .- D ) = ( X .- Z ) /\ ( C .- D ) = ( Y .- Z ) ) ) ) )
15.2.6  Motions
Syntax	cismt 25427	Declare the constant for the isometry builder.
class Ismt
Definition	df-ismt 25428*	Define the set of isometries between two structures. Definition 4.8 of [Schwabhauser] p. 36. See isismt 25429. (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 25429*	Property of being an isometry. Compare with isismty 33600. (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 25430*	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 ) ) ) )
Theorem	motcgr 25431	Property of a motion: distances are preserved. (Contributed by Thierry Arnoux, 15-Dec-2019.)
|- P = ( Base ` G )   &    |- .- = ( dist ` G )   &    |- ( ph -> G e. V )   &    |- ( ph -> A e. P )   &    |- ( ph -> B e. P )   &    |- ( ph -> F e. ( GIsmt G ) )   =>    |- ( ph -> ( ( F ` A ) .- ( F ` B ) ) = ( A .- B ) )
Theorem	idmot 25432	The identity is a motion. (Contributed by Thierry Arnoux, 15-Dec-2019.)
|- P = ( Base ` G )   &    |- .- = ( dist ` G )   &    |- ( ph -> G e. V )   =>    |- ( ph -> ( _I |` P ) e. ( GIsmt G ) )
Theorem	motf1o 25433	Motions are bijections. (Contributed by Thierry Arnoux, 15-Dec-2019.)
|- P = ( Base ` G )   &    |- .- = ( dist ` G )   &    |- ( ph -> G e. V )   &    |- ( ph -> F e. ( GIsmt G ) )   =>    |- ( ph -> F : P -1-1-onto-> P )
Theorem	motcl 25434	Closure of motions. (Contributed by Thierry Arnoux, 15-Dec-2019.)
|- P = ( Base ` G )   &    |- .- = ( dist ` G )   &    |- ( ph -> G e. V )   &    |- ( ph -> F e. ( GIsmt G ) )   &    |- ( ph -> A e. P )   =>    |- ( ph -> ( F ` A ) e. P )
Theorem	motco 25435	The composition of two motions is a motion. (Contributed by Thierry Arnoux, 15-Dec-2019.)
|- P = ( Base ` G )   &    |- .- = ( dist ` G )   &    |- ( ph -> G e. V )   &    |- ( ph -> F e. ( GIsmt G ) )   &    |- ( ph -> H e. ( GIsmt G ) )   =>    |- ( ph -> ( F o. H ) e. ( GIsmt G ) )
Theorem	cnvmot 25436	The converse of a motion is a motion. (Contributed by Thierry Arnoux, 15-Dec-2019.)
|- P = ( Base ` G )   &    |- .- = ( dist ` G )   &    |- ( ph -> G e. V )   &    |- ( ph -> F e. ( GIsmt G ) )   =>    |- ( ph -> `' F e. ( GIsmt G ) )
Theorem	motplusg 25437*	The operation for motions is their composition. (Contributed by Thierry Arnoux, 15-Dec-2019.)
|- P = ( Base ` G )   &    |- .- = ( dist ` G )   &    |- ( ph -> G e. V )   &    |- I = { <. ( Base ` ndx ) , ( GIsmt G ) >. , <. ( +g ` ndx ) , ( f e. ( GIsmt G ) , g e. ( GIsmt G ) |-> ( f o. g ) ) >. }   &    |- ( ph -> F e. ( GIsmt G ) )   &    |- ( ph -> H e. ( GIsmt G ) )   =>    |- ( ph -> ( F ( +g ` I ) H ) = ( F o. H ) )
Theorem	motgrp 25438*	The motions of a geometry form a group with respect to function composition, called the Isometry group. (Contributed by Thierry Arnoux, 15-Dec-2019.)
|- P = ( Base ` G )   &    |- .- = ( dist ` G )   &    |- ( ph -> G e. V )   &    |- I = { <. ( Base ` ndx ) , ( GIsmt G ) >. , <. ( +g ` ndx ) , ( f e. ( GIsmt G ) , g e. ( GIsmt G ) |-> ( f o. g ) ) >. }   =>    |- ( ph -> I e. Grp )
Theorem	motcgrg 25439*	Property of a motion: distances are preserved. (Contributed by Thierry Arnoux, 15-Dec-2019.)
|- P = ( Base ` G )   &    |- .- = ( dist ` G )   &    |- ( ph -> G e. V )   &    |- I = { <. ( Base ` ndx ) , ( GIsmt G ) >. , <. ( +g ` ndx ) , ( f e. ( GIsmt G ) , g e. ( GIsmt G ) |-> ( f o. g ) ) >. }   &    |- .~ = (cgrG ` G )   &    |- ( ph -> T e. Word P )   &    |- ( ph -> F e. ( GIsmt G ) )   =>    |- ( ph -> ( F o. T ) .~ T )
Theorem	motcgr3 25440	Property of a motion: distances are preserved, special case of triangles. (Contributed by Thierry Arnoux, 15-Dec-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 = ( H ` A ) )   &    |- ( ph -> E = ( H ` B ) )   &    |- ( ph -> F = ( H ` C ) )   &    |- ( ph -> H e. ( GIsmt G ) )   =>    |- ( ph -> <" A B C "> .~ <" D E F "> )
15.2.7  Colinearity
Theorem	tglng 25441*	Lines of a Tarski Geometry. This relates to both Definition 4.10 of [Schwabhauser] p. 36. and Definition 6.14 of [Schwabhauser] p. 45. (Contributed by Thierry Arnoux, 28-Mar-2019.)
|- P = ( Base ` G )   &    |- L = (LineG ` G )   &    |- I = (Itv ` G )   =>    |- ( G e. TarskiG -> L = ( 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	tglnfn 25442	Lines as functions. (Contributed by Thierry Arnoux, 25-May-2019.)
|- P = ( Base ` G )   &    |- L = (LineG ` G )   &    |- I = (Itv ` G )   =>    |- ( G e. TarskiG -> L Fn ( ( P X. P ) \ _I ) )
Theorem	tglnunirn 25443	Lines are sets of points. (Contributed by Thierry Arnoux, 25-May-2019.)
|- P = ( Base ` G )   &    |- L = (LineG ` G )   &    |- I = (Itv ` G )   =>    |- ( G e. TarskiG -> U. ran L C_ P )
Theorem	tglnpt 25444	Lines are sets of points. (Contributed by Thierry Arnoux, 17-Oct-2019.)
|- P = ( Base ` G )   &    |- L = (LineG ` G )   &    |- I = (Itv ` G )   &    |- ( ph -> G e. TarskiG )   &    |- ( ph -> A e. ran L )   &    |- ( ph -> X e. A )   =>    |- ( ph -> X e. P )
Theorem	tglngne 25445	It takes two different points to form a line. (Contributed by Thierry Arnoux, 6-Aug-2019.)
|- P = ( Base ` G )   &    |- L = (LineG ` G )   &    |- I = (Itv ` G )   &    |- ( ph -> G e. TarskiG )   &    |- ( ph -> X e. P )   &    |- ( ph -> Y e. P )   &    |- ( ph -> Z e. ( X L Y ) )   =>    |- ( ph -> X =/= Y )
Theorem	tglngval 25446*	The line going through points X and Y. (Contributed by Thierry Arnoux, 28-Mar-2019.)
|- P = ( Base ` G )   &    |- L = (LineG ` G )   &    |- I = (Itv ` G )   &    |- ( ph -> G e. TarskiG )   &    |- ( ph -> X e. P )   &    |- ( ph -> Y e. P )   &    |- ( ph -> X =/= Y )   =>    |- ( ph -> ( X L Y ) = { z e. P | ( z e. ( X I Y ) \/ X e. ( z I Y ) \/ Y e. ( X I z ) ) } )
Theorem	tglnssp 25447	Lines are subset of the geometry base set. That is, lines are sets of points. (Contributed by Thierry Arnoux, 17-May-2019.)
|- P = ( Base ` G )   &    |- L = (LineG ` G )   &    |- I = (Itv ` G )   &    |- ( ph -> G e. TarskiG )   &    |- ( ph -> X e. P )   &    |- ( ph -> Y e. P )   &    |- ( ph -> X =/= Y )   =>    |- ( ph -> ( X L Y ) C_ P )
Theorem	tgellng 25448	Property of lying on the line going through points X and Y. Definition 4.10 of [Schwabhauser] p. 36. We choose the notation Z e. ( X (LineG ` G ) Y ) instead of "colinear" because LineG is a common structure slot for other axiomatizations of geometry. (Contributed by Thierry Arnoux, 28-Mar-2019.)
|- P = ( Base ` G )   &    |- L = (LineG ` G )   &    |- I = (Itv ` G )   &    |- ( ph -> G e. TarskiG )   &    |- ( ph -> X e. P )   &    |- ( ph -> Y e. P )   &    |- ( ph -> X =/= Y )   &    |- ( ph -> Z e. P )   =>    |- ( ph -> ( Z e. ( X L Y ) <-> ( Z e. ( X I Y ) \/ X e. ( Z I Y ) \/ Y e. ( X I Z ) ) ) )
Theorem	tgcolg 25449	We choose the notation ( Z e. ( X L Y ) \/ X = Y ) instead of "colinear" in order to avoid defining an additional symbol for colinearity because LineG is a common structure slot for other axiomatizations of geometry. (Contributed by Thierry Arnoux, 25-May-2019.)
|- P = ( Base ` G )   &    |- L = (LineG ` G )   &    |- I = (Itv ` G )   &    |- ( ph -> G e. TarskiG )   &    |- ( ph -> X e. P )   &    |- ( ph -> Y e. P )   &    |- ( ph -> Z e. P )   =>    |- ( ph -> ( ( Z e. ( X L Y ) \/ X = Y ) <-> ( Z e. ( X I Y ) \/ X e. ( Z I Y ) \/ Y e. ( X I Z ) ) ) )
Theorem	btwncolg1 25450	Betweenness implies colinearity. (Contributed by Thierry Arnoux, 28-Mar-2019.)
|- P = ( Base ` G )   &    |- L = (LineG ` G )   &    |- I = (Itv ` G )   &    |- ( ph -> G e. TarskiG )   &    |- ( ph -> X e. P )   &    |- ( ph -> Y e. P )   &    |- ( ph -> Z e. P )   &    |- ( ph -> Z e. ( X I Y ) )   =>    |- ( ph -> ( Z e. ( X L Y ) \/ X = Y ) )
Theorem	btwncolg2 25451	Betweenness implies colinearity. (Contributed by Thierry Arnoux, 28-Mar-2019.)
|- P = ( Base ` G )   &    |- L = (LineG ` G )   &    |- I = (Itv ` G )   &    |- ( ph -> G e. TarskiG )   &    |- ( ph -> X e. P )   &    |- ( ph -> Y e. P )   &    |- ( ph -> Z e. P )   &    |- ( ph -> X e. ( Z I Y ) )   =>    |- ( ph -> ( Z e. ( X L Y ) \/ X = Y ) )
Theorem	btwncolg3 25452	Betweenness implies colinearity. (Contributed by Thierry Arnoux, 28-Mar-2019.)
|- P = ( Base ` G )   &    |- L = (LineG ` G )   &    |- I = (Itv ` G )   &    |- ( ph -> G e. TarskiG )   &    |- ( ph -> X e. P )   &    |- ( ph -> Y e. P )   &    |- ( ph -> Z e. P )   &    |- ( ph -> Y e. ( X I Z ) )   =>    |- ( ph -> ( Z e. ( X L Y ) \/ X = Y ) )
Theorem	colcom 25453	Swapping the points defining a line keeps it unchanged. Part of Theorem 4.11 of [Schwabhauser] p. 34. (Contributed by Thierry Arnoux, 3-Apr-2019.)
|- P = ( Base ` G )   &    |- L = (LineG ` G )   &    |- I = (Itv ` G )   &    |- ( ph -> G e. TarskiG )   &    |- ( ph -> X e. P )   &    |- ( ph -> Y e. P )   &    |- ( ph -> Z e. P )   &    |- ( ph -> ( Z e. ( X L Y ) \/ X = Y ) )   =>    |- ( ph -> ( Z e. ( Y L X ) \/ Y = X ) )
Theorem	colrot1 25454	Rotating the points defining a line. Part of Theorem 4.11 of [Schwabhauser] p. 34. (Contributed by Thierry Arnoux, 3-Apr-2019.)
|- P = ( Base ` G )   &    |- L = (LineG ` G )   &    |- I = (Itv ` G )   &    |- ( ph -> G e. TarskiG )   &    |- ( ph -> X e. P )   &    |- ( ph -> Y e. P )   &    |- ( ph -> Z e. P )   &    |- ( ph -> ( Z e. ( X L Y ) \/ X = Y ) )   =>    |- ( ph -> ( X e. ( Y L Z ) \/ Y = Z ) )
Theorem	colrot2 25455	Rotating the points defining a line. Part of Theorem 4.11 of [Schwabhauser] p. 34. (Contributed by Thierry Arnoux, 3-Apr-2019.)
|- P = ( Base ` G )   &    |- L = (LineG ` G )   &    |- I = (Itv ` G )   &    |- ( ph -> G e. TarskiG )   &    |- ( ph -> X e. P )   &    |- ( ph -> Y e. P )   &    |- ( ph -> Z e. P )   &    |- ( ph -> ( Z e. ( X L Y ) \/ X = Y ) )   =>    |- ( ph -> ( Y e. ( Z L X ) \/ Z = X ) )
Theorem	ncolcom 25456	Swapping non-colinear points. (Contributed by Thierry Arnoux, 19-Oct-2019.)
|- P = ( Base ` G )   &    |- L = (LineG ` G )   &    |- I = (Itv ` G )   &    |- ( ph -> G e. TarskiG )   &    |- ( ph -> X e. P )   &    |- ( ph -> Y e. P )   &    |- ( ph -> Z e. P )   &    |- ( ph -> -. ( Z e. ( X L Y ) \/ X = Y ) )   =>    |- ( ph -> -. ( Z e. ( Y L X ) \/ Y = X ) )
Theorem	ncolrot1 25457	Rotating non-colinear points. (Contributed by Thierry Arnoux, 19-Oct-2019.)
|- P = ( Base ` G )   &    |- L = (LineG ` G )   &    |- I = (Itv ` G )   &    |- ( ph -> G e. TarskiG )   &    |- ( ph -> X e. P )   &    |- ( ph -> Y e. P )   &    |- ( ph -> Z e. P )   &    |- ( ph -> -. ( Z e. ( X L Y ) \/ X = Y ) )   =>    |- ( ph -> -. ( X e. ( Y L Z ) \/ Y = Z ) )
Theorem	ncolrot2 25458	Rotating non-colinear points. (Contributed by Thierry Arnoux, 19-Oct-2019.)
|- P = ( Base ` G )   &    |- L = (LineG ` G )   &    |- I = (Itv ` G )   &    |- ( ph -> G e. TarskiG )   &    |- ( ph -> X e. P )   &    |- ( ph -> Y e. P )   &    |- ( ph -> Z e. P )   &    |- ( ph -> -. ( Z e. ( X L Y ) \/ X = Y ) )   =>    |- ( ph -> -. ( Y e. ( Z L X ) \/ Z = X ) )
Theorem	tgdim01ln 25459	In geometries of dimension lower than 2, any 3 points are colinear. (Contributed by Thierry Arnoux, 27-Aug-2019.)
|- P = ( Base ` G )   &    |- L = (LineG ` G )   &    |- I = (Itv ` G )   &    |- ( ph -> G e. TarskiG )   &    |- ( ph -> X e. P )   &    |- ( ph -> Y e. P )   &    |- ( ph -> Z e. P )   &    |- ( ph -> -. GDimTarskiG≥ 2 )   =>    |- ( ph -> ( Z e. ( X L Y ) \/ X = Y ) )
Theorem	ncoltgdim2 25460	If there are 3 non-colinear points, dimension must be 2 or more. tglowdim2l 25545 converse. (Contributed by Thierry Arnoux, 23-Feb-2020.)
|- P = ( Base ` G )   &    |- L = (LineG ` G )   &    |- I = (Itv ` G )   &    |- ( ph -> G e. TarskiG )   &    |- ( ph -> X e. P )   &    |- ( ph -> Y e. P )   &    |- ( ph -> Z e. P )   &    |- ( ph -> -. ( Z e. ( X L Y ) \/ X = Y ) )   =>    |- ( ph -> GDimTarskiG≥ 2 )
Theorem	lnxfr 25461	Transfer law for colinearity. Theorem 4.13 of [Schwabhauser] p. 37. (Contributed by Thierry Arnoux, 27-Apr-2019.)
|- P = ( Base ` G )   &    |- L = (LineG ` G )   &    |- I = (Itv ` G )   &    |- ( ph -> G e. TarskiG )   &    |- ( ph -> X e. P )   &    |- ( ph -> Y e. P )   &    |- ( ph -> Z e. P )   &    |- .~ = (cgrG ` G )   &    |- ( ph -> A e. P )   &    |- ( ph -> B e. P )   &    |- ( ph -> C e. P )   &    |- ( ph -> ( Y e. ( X L Z ) \/ X = Z ) )   &    |- ( ph -> <" X Y Z "> .~ <" A B C "> )   =>    |- ( ph -> ( B e. ( A L C ) \/ A = C ) )
Theorem	lnext 25462*	Extend a line with a missing point. Theorem 4.14 of [Schwabhauser] p. 37. (Contributed by Thierry Arnoux, 27-Apr-2019.)
|- P = ( Base ` G )   &    |- L = (LineG ` G )   &    |- I = (Itv ` G )   &    |- ( ph -> G e. TarskiG )   &    |- ( ph -> X e. P )   &    |- ( ph -> Y e. P )   &    |- ( ph -> Z e. P )   &    |- .~ = (cgrG ` G )   &    |- ( ph -> A e. P )   &    |- ( ph -> B e. P )   &    |- .- = ( dist ` G )   &    |- ( ph -> ( Y e. ( X L Z ) \/ X = Z ) )   &    |- ( ph -> ( X .- Y ) = ( A .- B ) )   =>    |- ( ph -> E. c e. P <" X Y Z "> .~ <" A B c "> )
Theorem	tgfscgr 25463	Congruence law for the general five segment configuration. Theorem 4.16 of [Schwabhauser] p. 37. (Contributed by Thierry Arnoux, 27-Apr-2019.)
|- P = ( Base ` G )   &    |- L = (LineG ` G )   &    |- I = (Itv ` G )   &    |- ( ph -> G e. TarskiG )   &    |- ( ph -> X e. P )   &    |- ( ph -> Y e. P )   &    |- ( ph -> Z e. P )   &    |- .~ = (cgrG ` G )   &    |- ( ph -> A e. P )   &    |- ( ph -> B e. P )   &    |- .- = ( dist ` G )   &    |- ( ph -> T e. P )   &    |- ( ph -> C e. P )   &    |- ( ph -> D e. P )   &    |- ( ph -> ( Y e. ( X L Z ) \/ X = Z ) )   &    |- ( ph -> <" X Y Z "> .~ <" A B C "> )   &    |- ( ph -> ( X .- T ) = ( A .- D ) )   &    |- ( ph -> ( Y .- T ) = ( B .- D ) )   &    |- ( ph -> X =/= Y )   =>    |- ( ph -> ( Z .- T ) = ( C .- D ) )
Theorem	lncgr 25464	Congruence rule for lines. Theorem 4.17 of [Schwabhauser] p. 37. (Contributed by Thierry Arnoux, 28-Apr-2019.)
|- P = ( Base ` G )   &    |- L = (LineG ` G )   &    |- I = (Itv ` G )   &    |- ( ph -> G e. TarskiG )   &    |- ( ph -> X e. P )   &    |- ( ph -> Y e. P )   &    |- ( ph -> Z e. P )   &    |- .~ = (cgrG ` G )   &    |- ( ph -> A e. P )   &    |- ( ph -> B e. P )   &    |- .- = ( dist ` G )   &    |- ( ph -> X =/= Y )   &    |- ( ph -> ( Y e. ( X L Z ) \/ X = Z ) )   &    |- ( ph -> ( X .- A ) = ( X .- B ) )   &    |- ( ph -> ( Y .- A ) = ( Y .- B ) )   =>    |- ( ph -> ( Z .- A ) = ( Z .- B ) )
Theorem	lnid 25465	Identity law for points on lines. Theorem 4.18 of [Schwabhauser] p. 38. (Contributed by Thierry Arnoux, 28-Apr-2019.)
|- P = ( Base ` G )   &    |- L = (LineG ` G )   &    |- I = (Itv ` G )   &    |- ( ph -> G e. TarskiG )   &    |- ( ph -> X e. P )   &    |- ( ph -> Y e. P )   &    |- ( ph -> Z e. P )   &    |- .~ = (cgrG ` G )   &    |- ( ph -> A e. P )   &    |- ( ph -> B e. P )   &    |- .- = ( dist ` G )   &    |- ( ph -> X =/= Y )   &    |- ( ph -> ( Y e. ( X L Z ) \/ X = Z ) )   &    |- ( ph -> ( X .- Z ) = ( X .- A ) )   &    |- ( ph -> ( Y .- Z ) = ( Y .- A ) )   =>    |- ( ph -> Z = A )
Theorem	tgidinside 25466	Law for finding a point inside a segment. Theorem 4.19 of [Schwabhauser] p. 38. (Contributed by Thierry Arnoux, 28-Apr-2019.)
|- P = ( Base ` G )   &    |- L = (LineG ` G )   &    |- I = (Itv ` G )   &    |- ( ph -> G e. TarskiG )   &    |- ( ph -> X e. P )   &    |- ( ph -> Y e. P )   &    |- ( ph -> Z e. P )   &    |- .~ = (cgrG ` G )   &    |- ( ph -> A e. P )   &    |- ( ph -> B e. P )   &    |- .- = ( dist ` G )   &    |- ( ph -> Z e. ( X I Y ) )   &    |- ( ph -> ( X .- Z ) = ( X .- A ) )   &    |- ( ph -> ( Y .- Z ) = ( Y .- A ) )   =>    |- ( ph -> Z = A )
15.2.8  Connectivity of betweenness
Theorem	tgbtwnconn1lem1 25467	Lemma for tgbtwnconn1 25470. (Contributed by Thierry Arnoux, 30-Apr-2019.)
|- P = ( Base ` 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 )   &    |- ( ph -> B e. ( A I C ) )   &    |- ( ph -> B e. ( A I D ) )   &    |- .- = ( dist ` G )   &    |- ( ph -> E e. P )   &    |- ( ph -> F e. P )   &    |- ( ph -> H e. P )   &    |- ( ph -> J e. P )   &    |- ( ph -> D e. ( A I E ) )   &    |- ( ph -> C e. ( A I F ) )   &    |- ( ph -> E e. ( A I H ) )   &    |- ( ph -> F e. ( A I J ) )   &    |- ( ph -> ( E .- D ) = ( C .- D ) )   &    |- ( ph -> ( C .- F ) = ( C .- D ) )   &    |- ( ph -> ( E .- H ) = ( B .- C ) )   &    |- ( ph -> ( F .- J ) = ( B .- D ) )   =>    |- ( ph -> H = J )
Theorem	tgbtwnconn1lem2 25468	Lemma for tgbtwnconn1 25470. (Contributed by Thierry Arnoux, 30-Apr-2019.)
|- P = ( Base ` 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 )   &    |- ( ph -> B e. ( A I C ) )   &    |- ( ph -> B e. ( A I D ) )   &    |- .- = ( dist ` G )   &    |- ( ph -> E e. P )   &    |- ( ph -> F e. P )   &    |- ( ph -> H e. P )   &    |- ( ph -> J e. P )   &    |- ( ph -> D e. ( A I E ) )   &    |- ( ph -> C e. ( A I F ) )   &    |- ( ph -> E e. ( A I H ) )   &    |- ( ph -> F e. ( A I J ) )   &    |- ( ph -> ( E .- D ) = ( C .- D ) )   &    |- ( ph -> ( C .- F ) = ( C .- D ) )   &    |- ( ph -> ( E .- H ) = ( B .- C ) )   &    |- ( ph -> ( F .- J ) = ( B .- D ) )   =>    |- ( ph -> ( E .- F ) = ( C .- D ) )
Theorem	tgbtwnconn1lem3 25469	Lemma for tgbtwnconn1 25470. (Contributed by Thierry Arnoux, 30-Apr-2019.)
|- P = ( Base ` 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 )   &    |- ( ph -> B e. ( A I C ) )   &    |- ( ph -> B e. ( A I D ) )   &    |- .- = ( dist ` G )   &    |- ( ph -> E e. P )   &    |- ( ph -> F e. P )   &    |- ( ph -> H e. P )   &    |- ( ph -> J e. P )   &    |- ( ph -> D e. ( A I E ) )   &    |- ( ph -> C e. ( A I F ) )   &    |- ( ph -> E e. ( A I H ) )   &    |- ( ph -> F e. ( A I J ) )   &    |- ( ph -> ( E .- D ) = ( C .- D ) )   &    |- ( ph -> ( C .- F ) = ( C .- D ) )   &    |- ( ph -> ( E .- H ) = ( B .- C ) )   &    |- ( ph -> ( F .- J ) = ( B .- D ) )   &    |- ( ph -> X e. P )   &    |- ( ph -> X e. ( C I E ) )   &    |- ( ph -> X e. ( D I F ) )   &    |- ( ph -> C =/= E )   =>    |- ( ph -> D = F )
Theorem	tgbtwnconn1 25470	Connectivity law for betweenness. Theorem 5.1 of [Schwabhauser] p. 39-41. In earlier presentations of Tarski's axioms, this theorem appeared as an additional axiom. It was derived from the other axioms by Gupta, 1965. (Contributed by Thierry Arnoux, 30-Apr-2019.)
|- P = ( Base ` 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 )   &    |- ( ph -> B e. ( A I C ) )   &    |- ( ph -> B e. ( A I D ) )   =>    |- ( ph -> ( C e. ( A I D ) \/ D e. ( A I C ) ) )
Theorem	tgbtwnconn2 25471	Another connectivity law for betweenness. Theorem 5.2 of [Schwabhauser] p. 41. (Contributed by Thierry Arnoux, 17-May-2019.)
|- P = ( Base ` 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 )   &    |- ( ph -> B e. ( A I C ) )   &    |- ( ph -> B e. ( A I D ) )   =>    |- ( ph -> ( C e. ( B I D ) \/ D e. ( B I C ) ) )
Theorem	tgbtwnconn3 25472	Inner connectivity law for betweenness. Theorem 5.3 of [Schwabhauser] p. 41. (Contributed by Thierry Arnoux, 17-May-2019.)
|- P = ( Base ` 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. ( A I D ) )   =>    |- ( ph -> ( B e. ( A I C ) \/ C e. ( A I B ) ) )
Theorem	tgbtwnconnln3 25473	Derive colinearity from betweenness. (Contributed by Thierry Arnoux, 17-May-2019.)
|- P = ( Base ` 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. ( A I D ) )   &    |- L = (LineG ` G )   =>    |- ( ph -> ( B e. ( A L C ) \/ A = C ) )
Theorem	tgbtwnconn22 25474	Double connectivity law for betweenness. (Contributed by Thierry Arnoux, 1-Dec-2019.)
|- P = ( Base ` 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 -> A =/= B )   &    |- ( ph -> C =/= B )   &    |- ( ph -> B e. ( A I C ) )   &    |- ( ph -> B e. ( A I D ) )   &    |- ( ph -> B e. ( C I E ) )   =>    |- ( ph -> B e. ( D I E ) )
Theorem	tgbtwnconnln1 25475	Derive colinearity from betweenness. (Contributed by Thierry Arnoux, 17-May-2019.)
|- P = ( Base ` G )   &    |- I = (Itv ` G )   &    |- ( ph -> G e. TarskiG )   &    |- ( ph -> A e. P )   &    |- ( ph -> B e. P )   &    |- ( ph -> C e. P )   &    |- ( ph -> D e. P )   &    |- L = (LineG ` G )   &    |- ( ph -> A =/= B )   &    |- ( ph -> B e. ( A I C ) )   &    |- ( ph -> B e. ( A I D ) )   =>    |- ( ph -> ( A e. ( C L D ) \/ C = D ) )
Theorem	tgbtwnconnln2 25476	Derive colinearity from betweenness. (Contributed by Thierry Arnoux, 17-May-2019.)
|- P = ( Base ` G )   &    |- I = (Itv ` G )   &    |- ( ph -> G e. TarskiG )   &    |- ( ph -> A e. P )   &    |- ( ph -> B e. P )   &    |- ( ph -> C e. P )   &    |- ( ph -> D e. P )   &    |- L = (LineG ` G )   &    |- ( ph -> A =/= B )   &    |- ( ph -> B e. ( A I C ) )   &    |- ( ph -> B e. ( A I D ) )   =>    |- ( ph -> ( B e. ( C L D ) \/ C = D ) )
15.2.9  Less-than relation in geometric congruences
Syntax	cleg 25477	Less-than relation for geometric congruences.
class ≤G
Definition	df-leg 25478*	Define the less-than relationship between geometric distance congruence classes. See legval 25479. (Contributed by Thierry Arnoux, 21-Jun-2019.)
|- ≤G = ( g e. _V |-> { <. e , f >. | [. ( Base ` g ) / p ]. [. ( dist ` g ) / d ]. [. (Itv ` g ) / i ]. E. x e. p E. y e. p ( f = ( x d y ) /\ E. z e. p ( z e. ( x i y ) /\ e = ( x d z ) ) ) } )
Theorem	legval 25479*	Value of the less-than relationship. (Contributed by Thierry Arnoux, 21-Jun-2019.)
|- P = ( Base ` G )   &    |- .- = ( dist ` G )   &    |- I = (Itv ` G )   &    |- .<_ = (≤G ` G )   &    |- ( ph -> G e. TarskiG )   =>    |- ( ph -> .<_ = { <. e , f >. | E. x e. P E. y e. P ( f = ( x .- y ) /\ E. z e. P ( z e. ( x I y ) /\ e = ( x .- z ) ) ) } )
Theorem	legov 25480*	Value of the less-than relationship. Definition 5.4 of [Schwabhauser] p. 41. (Contributed by Thierry Arnoux, 21-Jun-2019.)
|- P = ( Base ` G )   &    |- .- = ( dist ` G )   &    |- I = (Itv ` G )   &    |- .<_ = (≤G ` 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 ) <-> E. z e. P ( z e. ( C I D ) /\ ( A .- B ) = ( C .- z ) ) ) )
Theorem	legov2 25481*	An equivalent definition of the less-than relationship. Definition 5.5 of [Schwabhauser] p. 41. (Contributed by Thierry Arnoux, 21-Jun-2019.)
|- P = ( Base ` G )   &    |- .- = ( dist ` G )   &    |- I = (Itv ` G )   &    |- .<_ = (≤G ` 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 ) <-> E. x e. P ( B e. ( A I x ) /\ ( A .- x ) = ( C .- D ) ) ) )
Theorem	legid 25482	Reflexivity of the less-than relationship. Proposition 5.7 of [Schwabhauser] p. 42. (Contributed by Thierry Arnoux, 27-Jun-2019.)
|- P = ( Base ` G )   &    |- .- = ( dist ` G )   &    |- I = (Itv ` G )   &    |- .<_ = (≤G ` G )   &    |- ( ph -> G e. TarskiG )   &    |- ( ph -> A e. P )   &    |- ( ph -> B e. P )   =>    |- ( ph -> ( A .- B ) .<_ ( A .- B ) )
Theorem	btwnleg 25483	Betweenness implies less-than relation. (Contributed by Thierry Arnoux, 3-Jul-2019.)
|- P = ( Base ` G )   &    |- .- = ( dist ` G )   &    |- I = (Itv ` G )   &    |- .<_ = (≤G ` G )   &    |- ( ph -> G e. TarskiG )   &    |- ( ph -> A e. P )   &    |- ( ph -> B e. P )   &    |- ( ph -> C e. P )   &    |- ( ph -> B e. ( A I C ) )   =>    |- ( ph -> ( A .- B ) .<_ ( A .- C ) )
Theorem	legtrd 25484	Transitivity of the less-than relationship. Proposition 5.8 of [Schwabhauser] p. 42. (Contributed by Thierry Arnoux, 27-Jun-2019.)
|- P = ( Base ` G )   &    |- .- = ( dist ` G )   &    |- I = (Itv ` G )   &    |- .<_ = (≤G ` 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 ) )   &    |- ( ph -> ( C .- D ) .<_ ( E .- F ) )   =>    |- ( ph -> ( A .- B ) .<_ ( E .- F ) )
Theorem	legtri3 25485	Equality from the less-than relationship. Proposition 5.9 of [Schwabhauser] p. 42. (Contributed by Thierry Arnoux, 27-Jun-2019.)
|- P = ( Base ` G )   &    |- .- = ( dist ` G )   &    |- I = (Itv ` G )   &    |- .<_ = (≤G ` 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 -> ( C .- D ) .<_ ( A .- B ) )   =>    |- ( ph -> ( A .- B ) = ( C .- D ) )
Theorem	legtrid 25486	Trichotomy law for the less-than relationship. Proposition 5.10 of [Schwabhauser] p. 42. (Contributed by Thierry Arnoux, 27-Jun-2019.)
|- P = ( Base ` G )   &    |- .- = ( dist ` G )   &    |- I = (Itv ` G )   &    |- .<_ = (≤G ` 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 ) \/ ( C .- D ) .<_ ( A .- B ) ) )
Theorem	leg0 25487	Degenerated (zero-length) segments are minimal. Proposition 5.11 of [Schwabhauser] p. 42. (Contributed by Thierry Arnoux, 27-Jun-2019.)
|- P = ( Base ` G )   &    |- .- = ( dist ` G )   &    |- I = (Itv ` G )   &    |- .<_ = (≤G ` G )   &    |- ( ph -> G e. TarskiG )   &    |- ( ph -> A e. P )   &    |- ( ph -> B e. P )   &    |- ( ph -> C e. P )   &    |- ( ph -> D e. P )   =>    |- ( ph -> ( A .- A ) .<_ ( C .- D ) )
Theorem	legeq 25488	Deduce equality from "less than" null segments. (Contributed by Thierry Arnoux, 12-Aug-2019.)
|- P = ( Base ` G )   &    |- .- = ( dist ` G )   &    |- I = (Itv ` G )   &    |- .<_ = (≤G ` 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 .- C ) )   =>    |- ( ph -> A = B )
Theorem	legbtwn 25489	Deduce betweenness from "less than" relation. Corresponds loosely to Proposition 6.13 of [Schwabhauser] p. 45. (Contributed by Thierry Arnoux, 25-Aug-2019.)
|- P = ( Base ` G )   &    |- .- = ( dist ` G )   &    |- I = (Itv ` G )   &    |- .<_ = (≤G ` G )   &    |- ( ph -> G e. TarskiG )   &    |- ( ph -> A e. P )   &    |- ( ph -> B e. P )   &    |- ( ph -> C e. P )   &    |- ( ph -> D e. P )   &    |- ( ph -> ( A e. ( C I B ) \/ B e. ( C I A ) ) )   &    |- ( ph -> ( C .- A ) .<_ ( C .- B ) )   =>    |- ( ph -> A e. ( C I B ) )
Theorem	tgcgrsub2 25490	Removing identical parts from the end of a line segment preserves congruence. In this version the order of points is not known. (Contributed by Thierry Arnoux, 3-Apr-2019.)
|- P = ( Base ` G )   &    |- .- = ( dist ` G )   &    |- I = (Itv ` G )   &    |- .<_ = (≤G ` G )   &    |- ( ph -> G e. TarskiG )   &    |- ( ph -> A e. P )   &    |- ( ph -> B e. P )   &    |- ( ph -> C e. P )   &    |- ( ph -> D e. P )   &    |- ( ph -> D e. P )   &    |- ( ph -> E e. P )   &    |- ( ph -> F e. P )   &    |- ( ph -> ( B e. ( A I C ) \/ C e. ( A I B ) ) )   &    |- ( ph -> ( E e. ( D I F ) \/ F e. ( D I E ) ) )   &    |- ( ph -> ( A .- B ) = ( D .- E ) )   &    |- ( ph -> ( A .- C ) = ( D .- F ) )   =>    |- ( ph -> ( B .- C ) = ( E .- F ) )
Theorem	ltgseg 25491*	The set E denotes the possible values of the congruence. (Contributed by Thierry Arnoux, 15-Dec-2019.)
|- P = ( Base ` G )   &    |- .- = ( dist ` G )   &    |- I = (Itv ` G )   &    |- .<_ = (≤G ` G )   &    |- ( ph -> G e. TarskiG )   &    |- E = ( .- " ( P X. P ) )   &    |- ( ph -> Fun .- )   &    |- ( ph -> A e. E )   =>    |- ( ph -> E. x e. P E. y e. P A = ( x .- y ) )
Theorem	ltgov 25492	Strict "shorter than" geometric relation between segments. (Contributed by Thierry Arnoux, 15-Dec-2019.)
|- P = ( Base ` G )   &    |- .- = ( dist ` G )   &    |- I = (Itv ` G )   &    |- .<_ = (≤G ` G )   &    |- ( ph -> G e. TarskiG )   &    |- E = ( .- " ( P X. P ) )   &    |- ( ph -> Fun .- )   &    |- .< = ( ( .<_ |` E ) \ _I )   &    |- ( ph -> ( P X. P ) C_ dom .- )   &    |- ( ph -> A e. P )   &    |- ( ph -> B e. P )   =>    |- ( ph -> ( ( A .- B ) .< ( C .- D ) <-> ( ( A .- B ) .<_ ( C .- D ) /\ ( A .- B ) =/= ( C .- D ) ) ) )
Theorem	legov3 25493	An equivalent definition of the less-than relationship, from the strict relation. (Contributed by Thierry Arnoux, 15-Dec-2019.)
|- P = ( Base ` G )   &    |- .- = ( dist ` G )   &    |- I = (Itv ` G )   &    |- .<_ = (≤G ` G )   &    |- ( ph -> G e. TarskiG )   &    |- E = ( .- " ( P X. P ) )   &    |- ( ph -> Fun .- )   &    |- .< = ( ( .<_ |` E ) \ _I )   &    |- ( ph -> ( P X. P ) C_ dom .- )   &    |- ( ph -> A e. P )   &    |- ( ph -> B e. P )   =>    |- ( ph -> ( ( A .- B ) .<_ ( C .- D ) <-> ( ( A .- B ) .< ( C .- D ) \/ ( A .- B ) = ( C .- D ) ) ) )
Theorem	legso 25494	The shorter-than relationship builds an order over pairs. Remark 5.13 of [Schwabhauser] p. 42. (Contributed by Thierry Arnoux, 27-Jun-2019.)
|- P = ( Base ` G )   &    |- .- = ( dist ` G )   &    |- I = (Itv ` G )   &    |- .<_ = (≤G ` G )   &    |- ( ph -> G e. TarskiG )   &    |- E = ( .- " ( P X. P ) )   &    |- ( ph -> Fun .- )   &    |- .< = ( ( .<_ |` E ) \ _I )   &    |- ( ph -> ( P X. P ) C_ dom .- )   =>    |- ( ph -> .< Or E )
15.2.10  Rays
Syntax	chlg 25495	Function producing the relation "belong to the same half-line".
class hlG
Definition	df-hlg 25496*	Define the function producting the relation "belong to the same half-line" (Contributed by Thierry Arnoux, 15-Aug-2020.)
|- hlG = ( g e. _V |-> ( c e. ( Base ` g ) |-> { <. a , b >. | ( ( a e. ( Base ` g ) /\ b e. ( Base ` g ) ) /\ ( a =/= c /\ b =/= c /\ ( a e. ( c (Itv ` g ) b ) \/ b e. ( c (Itv ` g ) a ) ) ) ) } ) )
Theorem	ishlg 25497	Rays : Definition 6.1 of [Schwabhauser] p. 43. With this definition, A ( K ` C ) B means that A and B are on the same ray with initial point C. This follows the same notation as Schwabhauser where rays are first defined as a relation. It is possible to recover the ray itself using e.g. ( ( K ` C ) " { A } ) (Contributed by Thierry Arnoux, 21-Dec-2019.)
|- P = ( Base ` G )   &    |- I = (Itv ` G )   &    |- K = (hlG ` G )   &    |- ( ph -> A e. P )   &    |- ( ph -> B e. P )   &    |- ( ph -> C e. P )   &    |- ( ph -> G e. V )   =>    |- ( ph -> ( A ( K ` C ) B <-> ( A =/= C /\ B =/= C /\ ( A e. ( C I B ) \/ B e. ( C I A ) ) ) ) )
Theorem	hlcomb 25498	The half-line relation commutes. Theorem 6.6 of [Schwabhauser] p. 44. (Contributed by Thierry Arnoux, 21-Feb-2020.)
|- P = ( Base ` G )   &    |- I = (Itv ` G )   &    |- K = (hlG ` G )   &    |- ( ph -> A e. P )   &    |- ( ph -> B e. P )   &    |- ( ph -> C e. P )   &    |- ( ph -> G e. V )   =>    |- ( ph -> ( A ( K ` C ) B <-> B ( K ` C ) A ) )
Theorem	hlcomd 25499	The half-line relation commutes. Theorem 6.6 of [Schwabhauser] p. 44. (Contributed by Thierry Arnoux, 21-Feb-2020.)
|- P = ( Base ` G )   &    |- I = (Itv ` G )   &    |- K = (hlG ` G )   &    |- ( ph -> A e. P )   &    |- ( ph -> B e. P )   &    |- ( ph -> C e. P )   &    |- ( ph -> G e. V )   &    |- ( ph -> A ( K ` C ) B )   =>    |- ( ph -> B ( K ` C ) A )
Theorem	hlne1 25500	The half-line relation implies inequality. (Contributed by Thierry Arnoux, 22-Feb-2020.)
|- P = ( Base ` G )   &    |- I = (Itv ` G )   &    |- K = (hlG ` G )   &    |- ( ph -> A e. P )   &    |- ( ph -> B e. P )   &    |- ( ph -> C e. P )   &    |- ( ph -> G e. V )   &    |- ( ph -> A ( K ` C ) B )   =>    |- ( ph -> A =/= C )