P. 256 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 25501-25600   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	hlne2 25501	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 -> B =/= C )
Theorem	hlln 25502	The half-line relation implies colinearity, part of Theorem 6.4 of [Schwabhauser] p. 44. (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. TarskiG )   &    |- L = (LineG ` G )   &    |- ( ph -> A ( K ` C ) B )   =>    |- ( ph -> A e. ( B L C ) )
Theorem	hleqnid 25503	The endpoint does not belong to the half-line. (Contributed by Thierry Arnoux, 3-Mar-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. TarskiG )   =>    |- ( ph -> -. A ( K ` A ) B )
Theorem	hlid 25504	The half-line relation is reflexive. Theorem 6.5 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. TarskiG )   &    |- ( ph -> A =/= C )   =>    |- ( ph -> A ( K ` C ) A )
Theorem	hltr 25505	The half-line relation is transitive. Theorem 6.7 of [Schwabhauser] p. 44. (Contributed by Thierry Arnoux, 23-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. TarskiG )   &    |- ( ph -> D e. P )   &    |- ( ph -> A ( K ` D ) B )   &    |- ( ph -> B ( K ` D ) C )   =>    |- ( ph -> A ( K ` D ) C )
Theorem	hlbtwn 25506	Betweenness is a sufficient condition to swap half-lines. (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. TarskiG )   &    |- ( ph -> D e. P )   &    |- ( ph -> D e. ( C I B ) )   &    |- ( ph -> B =/= C )   &    |- ( ph -> D =/= C )   =>    |- ( ph -> ( A ( K ` C ) B <-> A ( K ` C ) D ) )
Theorem	btwnhl1 25507	Deduce half-line from betweenness. (Contributed by Thierry Arnoux, 4-Mar-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. TarskiG )   &    |- ( ph -> D e. P )   &    |- ( ph -> C e. ( A I B ) )   &    |- ( ph -> A =/= B )   &    |- ( ph -> C =/= A )   =>    |- ( ph -> C ( K ` A ) B )
Theorem	btwnhl2 25508	Deduce half-line from betweenness. (Contributed by Thierry Arnoux, 4-Mar-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. TarskiG )   &    |- ( ph -> D e. P )   &    |- ( ph -> C e. ( A I B ) )   &    |- ( ph -> A =/= B )   &    |- ( ph -> C =/= B )   =>    |- ( ph -> C ( K ` B ) A )
Theorem	btwnhl 25509	Swap betweenness for a half-line. (Contributed by Thierry Arnoux, 2-Mar-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. TarskiG )   &    |- ( ph -> D e. P )   &    |- ( ph -> A ( K ` D ) B )   &    |- ( ph -> D e. ( A I C ) )   =>    |- ( ph -> D e. ( B I C ) )
Theorem	lnhl 25510	Either a point C on the line AB is on the same side as A or on the opposite side. (Contributed by Thierry Arnoux, 21-Sep-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. TarskiG )   &    |- ( ph -> D e. P )   &    |- L = (LineG ` G )   &    |- ( ph -> C e. ( A L B ) )   =>    |- ( ph -> ( C ( K ` B ) A \/ B e. ( A I C ) ) )
Theorem	hlcgrex 25511*	Construct a point on a half-line, at a given distance of its origin. (Contributed by Thierry Arnoux, 1-Aug-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. TarskiG )   &    |- ( ph -> D e. P )   &    |- .- = ( dist ` G )   &    |- ( ph -> D =/= A )   &    |- ( ph -> B =/= C )   =>    |- ( ph -> E. x e. P ( x ( K ` A ) D /\ ( A .- x ) = ( B .- C ) ) )
Theorem	hlcgreulem 25512	Lemma for hlcgreu 25513. (Contributed by Thierry Arnoux, 9-Aug-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. TarskiG )   &    |- ( ph -> D e. P )   &    |- .- = ( dist ` G )   &    |- ( ph -> D =/= A )   &    |- ( ph -> B =/= C )   &    |- ( ph -> X e. P )   &    |- ( ph -> Y e. P )   &    |- ( ph -> X ( K ` A ) D )   &    |- ( ph -> Y ( K ` A ) D )   &    |- ( ph -> ( A .- X ) = ( B .- C ) )   &    |- ( ph -> ( A .- Y ) = ( B .- C ) )   =>    |- ( ph -> X = Y )
Theorem	hlcgreu 25513*	The point constructed in hlcgrex 25511 is unique. Theorem 6.11 of [Schwabhauser] p. 44. (Contributed by Thierry Arnoux, 9-Aug-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. TarskiG )   &    |- ( ph -> D e. P )   &    |- .- = ( dist ` G )   &    |- ( ph -> D =/= A )   &    |- ( ph -> B =/= C )   =>    |- ( ph -> E! x e. P ( x ( K ` A ) D /\ ( A .- x ) = ( B .- C ) ) )
15.2.11  Lines
Theorem	btwnlng1 25514	Betweenness implies colinearity. (Contributed by Thierry Arnoux, 28-Mar-2019.)
|- P = ( Base ` G )   &    |- I = (Itv ` G )   &    |- L = (LineG ` G )   &    |- ( ph -> G e. TarskiG )   &    |- ( ph -> X e. P )   &    |- ( ph -> Y e. P )   &    |- ( ph -> Z e. P )   &    |- ( ph -> X =/= Y )   &    |- ( ph -> Z e. ( X I Y ) )   =>    |- ( ph -> Z e. ( X L Y ) )
Theorem	btwnlng2 25515	Betweenness implies colinearity. (Contributed by Thierry Arnoux, 28-Mar-2019.)
|- P = ( Base ` G )   &    |- I = (Itv ` G )   &    |- L = (LineG ` G )   &    |- ( ph -> G e. TarskiG )   &    |- ( ph -> X e. P )   &    |- ( ph -> Y e. P )   &    |- ( ph -> Z e. P )   &    |- ( ph -> X =/= Y )   &    |- ( ph -> X e. ( Z I Y ) )   =>    |- ( ph -> Z e. ( X L Y ) )
Theorem	btwnlng3 25516	Betweenness implies colinearity. (Contributed by Thierry Arnoux, 28-Mar-2019.)
|- P = ( Base ` G )   &    |- I = (Itv ` G )   &    |- L = (LineG ` G )   &    |- ( ph -> G e. TarskiG )   &    |- ( ph -> X e. P )   &    |- ( ph -> Y e. P )   &    |- ( ph -> Z e. P )   &    |- ( ph -> X =/= Y )   &    |- ( ph -> Y e. ( X I Z ) )   =>    |- ( ph -> Z e. ( X L Y ) )
Theorem	lncom 25517	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 )   &    |- I = (Itv ` G )   &    |- L = (LineG ` G )   &    |- ( ph -> G e. TarskiG )   &    |- ( ph -> X e. P )   &    |- ( ph -> Y e. P )   &    |- ( ph -> Z e. P )   &    |- ( ph -> X =/= Y )   &    |- ( ph -> Z e. ( Y L X ) )   =>    |- ( ph -> Z e. ( X L Y ) )
Theorem	lnrot1 25518	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 )   &    |- I = (Itv ` G )   &    |- L = (LineG ` G )   &    |- ( ph -> G e. TarskiG )   &    |- ( ph -> X e. P )   &    |- ( ph -> Y e. P )   &    |- ( ph -> Z e. P )   &    |- ( ph -> X =/= Y )   &    |- ( ph -> Y e. ( Z L X ) )   &    |- ( ph -> Z =/= X )   =>    |- ( ph -> Z e. ( X L Y ) )
Theorem	lnrot2 25519	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 )   &    |- I = (Itv ` G )   &    |- L = (LineG ` G )   &    |- ( ph -> G e. TarskiG )   &    |- ( ph -> X e. P )   &    |- ( ph -> Y e. P )   &    |- ( ph -> Z e. P )   &    |- ( ph -> X =/= Y )   &    |- ( ph -> X e. ( Y L Z ) )   &    |- ( ph -> Y =/= Z )   =>    |- ( ph -> Z e. ( X L Y ) )
Theorem	ncolne1 25520	Non-colinear points are different. (Contributed by Thierry Arnoux, 8-Aug-2019.)
|- B = ( Base ` G )   &    |- I = (Itv ` G )   &    |- L = (LineG ` G )   &    |- ( ph -> G e. TarskiG )   &    |- ( ph -> X e. B )   &    |- ( ph -> Y e. B )   &    |- ( ph -> Z e. B )   &    |- ( ph -> -. ( X e. ( Y L Z ) \/ Y = Z ) )   =>    |- ( ph -> X =/= Y )
Theorem	ncolne2 25521	Non-colinear points are different. (Contributed by Thierry Arnoux, 8-Aug-2019.) TODO (NM): maybe ncolne2 25521 could be simplified out and deleted, replaced by ncolcom 25456.
|- B = ( Base ` G )   &    |- I = (Itv ` G )   &    |- L = (LineG ` G )   &    |- ( ph -> G e. TarskiG )   &    |- ( ph -> X e. B )   &    |- ( ph -> Y e. B )   &    |- ( ph -> Z e. B )   &    |- ( ph -> -. ( X e. ( Y L Z ) \/ Y = Z ) )   =>    |- ( ph -> X =/= Z )
Theorem	tgisline 25522*	The property of being a proper line, generated by two distinct points. (Contributed by Thierry Arnoux, 25-May-2019.)
|- B = ( Base ` G )   &    |- I = (Itv ` G )   &    |- L = (LineG ` G )   &    |- ( ph -> G e. TarskiG )   &    |- ( ph -> A e. ran L )   =>    |- ( ph -> E. x e. B E. y e. B ( A = ( x L y ) /\ x =/= y ) )
Theorem	tglnne 25523	It takes two different points to form a line. (Contributed by Thierry Arnoux, 27-Nov-2019.)
|- B = ( Base ` G )   &    |- I = (Itv ` G )   &    |- L = (LineG ` G )   &    |- ( ph -> G e. TarskiG )   &    |- ( ph -> X e. B )   &    |- ( ph -> Y e. B )   &    |- ( ph -> ( X L Y ) e. ran L )   =>    |- ( ph -> X =/= Y )
Theorem	tglndim0 25524	There are no lines in dimension 0. (Contributed by Thierry Arnoux, 18-Oct-2019.)
|- B = ( Base ` G )   &    |- I = (Itv ` G )   &    |- L = (LineG ` G )   &    |- ( ph -> G e. TarskiG )   &    |- ( ph -> ( # ` B ) = 1 )   =>    |- ( ph -> -. A e. ran L )
Theorem	tgelrnln 25525	The property of being a proper line, generated by two distinct points. (Contributed by Thierry Arnoux, 25-May-2019.)
|- B = ( Base ` G )   &    |- I = (Itv ` G )   &    |- L = (LineG ` G )   &    |- ( ph -> G e. TarskiG )   &    |- ( ph -> X e. B )   &    |- ( ph -> Y e. B )   &    |- ( ph -> X =/= Y )   =>    |- ( ph -> ( X L Y ) e. ran L )
Theorem	tglineeltr 25526	Transitivity law for lines, one half of tglineelsb2 25527. (Contributed by Thierry Arnoux, 25-May-2019.)
|- B = ( Base ` G )   &    |- I = (Itv ` G )   &    |- L = (LineG ` G )   &    |- ( ph -> G e. TarskiG )   &    |- ( ph -> P e. B )   &    |- ( ph -> Q e. B )   &    |- ( ph -> P =/= Q )   &    |- ( ph -> S e. B )   &    |- ( ph -> S =/= P )   &    |- ( ph -> S e. ( P L Q ) )   &    |- ( ph -> R e. B )   &    |- ( ph -> R e. ( P L S ) )   =>    |- ( ph -> R e. ( P L Q ) )
Theorem	tglineelsb2 25527	If S lies on PQ , then PQ = PS . Theorem 6.16 of [Schwabhauser] p. 45. (Contributed by Thierry Arnoux, 17-May-2019.)
|- B = ( Base ` G )   &    |- I = (Itv ` G )   &    |- L = (LineG ` G )   &    |- ( ph -> G e. TarskiG )   &    |- ( ph -> P e. B )   &    |- ( ph -> Q e. B )   &    |- ( ph -> P =/= Q )   &    |- ( ph -> S e. B )   &    |- ( ph -> S =/= P )   &    |- ( ph -> S e. ( P L Q ) )   =>    |- ( ph -> ( P L Q ) = ( P L S ) )
Theorem	tglinerflx1 25528	Reflexivity law for line membership. Part of theorem 6.17 of [Schwabhauser] p. 45. (Contributed by Thierry Arnoux, 17-May-2019.)
|- B = ( Base ` G )   &    |- I = (Itv ` G )   &    |- L = (LineG ` G )   &    |- ( ph -> G e. TarskiG )   &    |- ( ph -> P e. B )   &    |- ( ph -> Q e. B )   &    |- ( ph -> P =/= Q )   =>    |- ( ph -> P e. ( P L Q ) )
Theorem	tglinerflx2 25529	Reflexivity law for line membership. Part of theorem 6.17 of [Schwabhauser] p. 45. (Contributed by Thierry Arnoux, 17-May-2019.)
|- B = ( Base ` G )   &    |- I = (Itv ` G )   &    |- L = (LineG ` G )   &    |- ( ph -> G e. TarskiG )   &    |- ( ph -> P e. B )   &    |- ( ph -> Q e. B )   &    |- ( ph -> P =/= Q )   =>    |- ( ph -> Q e. ( P L Q ) )
Theorem	tglinecom 25530	Commutativity law for lines. Part of theorem 6.17 of [Schwabhauser] p. 45. (Contributed by Thierry Arnoux, 17-May-2019.)
|- B = ( Base ` G )   &    |- I = (Itv ` G )   &    |- L = (LineG ` G )   &    |- ( ph -> G e. TarskiG )   &    |- ( ph -> P e. B )   &    |- ( ph -> Q e. B )   &    |- ( ph -> P =/= Q )   =>    |- ( ph -> ( P L Q ) = ( Q L P ) )
Theorem	tglinethru 25531	If A is a line containing two distinct points P and Q, then A is the line through P and Q. Theorem 6.18 of [Schwabhauser] p. 45. (Contributed by Thierry Arnoux, 25-May-2019.)
|- B = ( Base ` G )   &    |- I = (Itv ` G )   &    |- L = (LineG ` G )   &    |- ( ph -> G e. TarskiG )   &    |- ( ph -> P e. B )   &    |- ( ph -> Q e. B )   &    |- ( ph -> P =/= Q )   &    |- ( ph -> P =/= Q )   &    |- ( ph -> A e. ran L )   &    |- ( ph -> P e. A )   &    |- ( ph -> Q e. A )   =>    |- ( ph -> A = ( P L Q ) )
Theorem	tghilberti1 25532*	There is a line through any two distinct points. Hilbert's axiom I.1 for geometry. (Contributed by Thierry Arnoux, 25-May-2019.)
|- B = ( Base ` G )   &    |- I = (Itv ` G )   &    |- L = (LineG ` G )   &    |- ( ph -> G e. TarskiG )   &    |- ( ph -> P e. B )   &    |- ( ph -> Q e. B )   &    |- ( ph -> P =/= Q )   =>    |- ( ph -> E. x e. ran L ( P e. x /\ Q e. x ) )
Theorem	tghilberti2 25533*	There is at most one line through any two distinct points. Hilbert's axiom I.2 for geometry. (Contributed by Thierry Arnoux, 25-May-2019.)
|- B = ( Base ` G )   &    |- I = (Itv ` G )   &    |- L = (LineG ` G )   &    |- ( ph -> G e. TarskiG )   &    |- ( ph -> P e. B )   &    |- ( ph -> Q e. B )   &    |- ( ph -> P =/= Q )   =>    |- ( ph -> E* x e. ran L ( P e. x /\ Q e. x ) )
Theorem	tglinethrueu 25534*	There is a unique line going through any two distinct points. Theorem 6.19 of [Schwabhauser] p. 46. (Contributed by Thierry Arnoux, 25-May-2019.)
|- B = ( Base ` G )   &    |- I = (Itv ` G )   &    |- L = (LineG ` G )   &    |- ( ph -> G e. TarskiG )   &    |- ( ph -> P e. B )   &    |- ( ph -> Q e. B )   &    |- ( ph -> P =/= Q )   =>    |- ( ph -> E! x e. ran L ( P e. x /\ Q e. x ) )
Theorem	tglnne0 25535	A line A has at least one point. (Contributed by Thierry Arnoux, 4-Mar-2020.)
|- L = (LineG ` G )   &    |- ( ph -> G e. TarskiG )   &    |- ( ph -> A e. ran L )   =>    |- ( ph -> A =/= (/) )
Theorem	tglnpt2 25536*	Find a second point on a line. (Contributed by Thierry Arnoux, 18-Oct-2019.)
|- P = ( Base ` G )   &    |- I = (Itv ` G )   &    |- L = (LineG ` G )   &    |- ( ph -> G e. TarskiG )   &    |- ( ph -> A e. ran L )   &    |- ( ph -> X e. A )   =>    |- ( ph -> E. y e. A X =/= y )
Theorem	tglineintmo 25537*	Two distinct lines intersect in at most one point. Theorem 6.21 of [Schwabhauser] p. 46. (Contributed by Thierry Arnoux, 25-May-2019.)
|- P = ( Base ` G )   &    |- I = (Itv ` G )   &    |- L = (LineG ` G )   &    |- ( ph -> G e. TarskiG )   &    |- ( ph -> A e. ran L )   &    |- ( ph -> B e. ran L )   &    |- ( ph -> A =/= B )   =>    |- ( ph -> E* x ( x e. A /\ x e. B ) )
Theorem	tglineineq 25538	Two distinct lines intersect in at most one point, variation. Theorem 6.21 of [Schwabhauser] p. 46. (Contributed by Thierry Arnoux, 6-Aug-2019.)
|- P = ( Base ` G )   &    |- I = (Itv ` G )   &    |- L = (LineG ` G )   &    |- ( ph -> G e. TarskiG )   &    |- ( ph -> A e. ran L )   &    |- ( ph -> B e. ran L )   &    |- ( ph -> A =/= B )   &    |- ( ph -> X e. ( A i^i B ) )   &    |- ( ph -> Y e. ( A i^i B ) )   =>    |- ( ph -> X = Y )
Theorem	tglineneq 25539	Given three non-colinear points, build two different lines. (Contributed by Thierry Arnoux, 6-Aug-2019.)
|- P = ( Base ` G )   &    |- I = (Itv ` G )   &    |- L = (LineG ` 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 L C ) \/ B = C ) )   =>    |- ( ph -> ( A L B ) =/= ( C L D ) )
Theorem	tglineinteq 25540	Two distinct lines intersect in at most one point. Theorem 6.21 of [Schwabhauser] p. 46. (Contributed by Thierry Arnoux, 6-Aug-2019.)
|- P = ( Base ` G )   &    |- I = (Itv ` G )   &    |- L = (LineG ` 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 L C ) \/ B = C ) )   &    |- ( ph -> X e. ( A L B ) )   &    |- ( ph -> Y e. ( A L B ) )   &    |- ( ph -> X e. ( C L D ) )   &    |- ( ph -> Y e. ( C L D ) )   =>    |- ( ph -> X = Y )
Theorem	ncolncol 25541	Deduce non-colinearity from non-colinearity and colinearity. (Contributed by Thierry Arnoux, 27-Aug-2019.)
|- P = ( Base ` G )   &    |- I = (Itv ` G )   &    |- L = (LineG ` 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 L C ) \/ B = C ) )   &    |- ( ph -> D e. ( A L B ) )   &    |- ( ph -> D =/= B )   =>    |- ( ph -> -. ( D e. ( B L C ) \/ B = C ) )
Theorem	coltr 25542	A transitivity law for colinearity. (Contributed by Thierry Arnoux, 27-Nov-2019.)
|- P = ( Base ` G )   &    |- I = (Itv ` G )   &    |- L = (LineG ` 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 L C ) )   &    |- ( ph -> ( B e. ( C L D ) \/ C = D ) )   =>    |- ( ph -> ( A e. ( C L D ) \/ C = D ) )
Theorem	coltr3 25543	A transitivity law for colinearity. (Contributed by Thierry Arnoux, 27-Nov-2019.)
|- P = ( Base ` G )   &    |- I = (Itv ` G )   &    |- L = (LineG ` 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 L C ) )   &    |- ( ph -> D e. ( A I C ) )   =>    |- ( ph -> D e. ( B L C ) )
Theorem	colline 25544*	Three points are colinear iff there is a line through all three of them. Theorem 6.23 of [Schwabhauser] p. 46. (Contributed by Thierry Arnoux, 28-May-2019.)
|- P = ( Base ` G )   &    |- I = (Itv ` G )   &    |- L = (LineG ` G )   &    |- ( ph -> G e. TarskiG )   &    |- ( ph -> X e. P )   &    |- ( ph -> Y e. P )   &    |- ( ph -> Z e. P )   &    |- ( ph -> 2 <_ ( # ` P ) )   =>    |- ( ph -> ( ( X e. ( Y L Z ) \/ Y = Z ) <-> E. a e. ran L ( X e. a /\ Y e. a /\ Z e. a ) ) )
Theorem	tglowdim2l 25545*	Reformulation of the lower dimension axiom for dimension 2. There exist three non colinear points. Theorem 6.24 of [Schwabhauser] p. 46. (Contributed by Thierry Arnoux, 30-May-2019.)
|- P = ( Base ` G )   &    |- I = (Itv ` G )   &    |- L = (LineG ` G )   &    |- ( ph -> G e. TarskiG )   &    |- ( ph -> GDimTarskiG≥ 2 )   =>    |- ( ph -> E. a e. P E. b e. P E. c e. P -. ( c e. ( a L b ) \/ a = b ) )
Theorem	tglowdim2ln 25546*	There is always one point outside of any line. Theorem 6.25 of [Schwabhauser] p. 46. (Contributed by Thierry Arnoux, 16-Nov-2019.)
|- P = ( Base ` G )   &    |- I = (Itv ` G )   &    |- L = (LineG ` G )   &    |- ( ph -> G e. TarskiG )   &    |- ( ph -> GDimTarskiG≥ 2 )   &    |- ( ph -> A e. P )   &    |- ( ph -> B e. P )   &    |- ( ph -> A =/= B )   =>    |- ( ph -> E. c e. P -. c e. ( A L B ) )
15.2.12  Point inversions
Syntax	cmir 25547	Declare the constant for the point inversion function.
class pInvG
Definition	df-mir 25548*	Define the point inversion ("mirror") function. Definition 7.5 of [Schwabhauser] p. 49. See mirval 25550 and ismir 25554. (Contributed by Thierry Arnoux, 30-May-2019.)
|- pInvG = ( g e. _V |-> ( m e. ( Base ` g ) |-> ( a e. ( Base ` g ) |-> ( iota_ b e. ( Base ` g ) ( ( m ( dist ` g ) b ) = ( m ( dist ` g ) a ) /\ m e. ( b (Itv ` g ) a ) ) ) ) ) )
Theorem	mirreu3 25549*	Existential uniqueness of the mirror point. Theorem 7.8 of [Schwabhauser] p. 49. (Contributed by Thierry Arnoux, 30-May-2019.)
|- P = ( Base ` G )   &    |- .- = ( dist ` G )   &    |- I = (Itv ` G )   &    |- ( ph -> G e. TarskiG )   &    |- ( ph -> A e. P )   &    |- ( ph -> M e. P )   =>    |- ( ph -> E! b e. P ( ( M .- b ) = ( M .- A ) /\ M e. ( b I A ) ) )
Theorem	mirval 25550*	Value of the point inversion function S. Definition 7.5 of [Schwabhauser] p. 49. (Contributed by Thierry Arnoux, 30-May-2019.)
|- P = ( Base ` G )   &    |- .- = ( dist ` G )   &    |- I = (Itv ` G )   &    |- L = (LineG ` G )   &    |- S = (pInvG ` G )   &    |- ( ph -> G e. TarskiG )   &    |- ( ph -> A e. P )   =>    |- ( ph -> ( S ` A ) = ( y e. P |-> ( iota_ z e. P ( ( A .- z ) = ( A .- y ) /\ A e. ( z I y ) ) ) ) )
Theorem	mirfv 25551*	Value of the point inversion function M. Definition 7.5 of [Schwabhauser] p. 49. (Contributed by Thierry Arnoux, 30-May-2019.)
|- P = ( Base ` G )   &    |- .- = ( dist ` G )   &    |- I = (Itv ` G )   &    |- L = (LineG ` G )   &    |- S = (pInvG ` G )   &    |- ( ph -> G e. TarskiG )   &    |- ( ph -> A e. P )   &    |- M = ( S ` A )   &    |- ( ph -> B e. P )   =>    |- ( ph -> ( M ` B ) = ( iota_ z e. P ( ( A .- z ) = ( A .- B ) /\ A e. ( z I B ) ) ) )
Theorem	mircgr 25552	Property of the image by the point inversion function. Definition 7.5 of [Schwabhauser] p. 49. (Contributed by Thierry Arnoux, 3-Jun-2019.)
|- P = ( Base ` G )   &    |- .- = ( dist ` G )   &    |- I = (Itv ` G )   &    |- L = (LineG ` G )   &    |- S = (pInvG ` G )   &    |- ( ph -> G e. TarskiG )   &    |- ( ph -> A e. P )   &    |- M = ( S ` A )   &    |- ( ph -> B e. P )   =>    |- ( ph -> ( A .- ( M ` B ) ) = ( A .- B ) )
Theorem	mirbtwn 25553	Property of the image by the point inversion function. Definition 7.5 of [Schwabhauser] p. 49. (Contributed by Thierry Arnoux, 3-Jun-2019.)
|- P = ( Base ` G )   &    |- .- = ( dist ` G )   &    |- I = (Itv ` G )   &    |- L = (LineG ` G )   &    |- S = (pInvG ` G )   &    |- ( ph -> G e. TarskiG )   &    |- ( ph -> A e. P )   &    |- M = ( S ` A )   &    |- ( ph -> B e. P )   =>    |- ( ph -> A e. ( ( M ` B ) I B ) )
Theorem	ismir 25554	Property of the image by the point inversion function. Definition 7.5 of [Schwabhauser] p. 49. (Contributed by Thierry Arnoux, 3-Jun-2019.)
|- P = ( Base ` G )   &    |- .- = ( dist ` G )   &    |- I = (Itv ` G )   &    |- L = (LineG ` G )   &    |- S = (pInvG ` G )   &    |- ( ph -> G e. TarskiG )   &    |- ( ph -> A e. P )   &    |- M = ( S ` A )   &    |- ( ph -> B e. P )   &    |- ( ph -> C e. P )   &    |- ( ph -> ( A .- C ) = ( A .- B ) )   &    |- ( ph -> A e. ( C I B ) )   =>    |- ( ph -> C = ( M ` B ) )
Theorem	mirf 25555	Point inversion as function. (Contributed by Thierry Arnoux, 30-May-2019.)
|- P = ( Base ` G )   &    |- .- = ( dist ` G )   &    |- I = (Itv ` G )   &    |- L = (LineG ` G )   &    |- S = (pInvG ` G )   &    |- ( ph -> G e. TarskiG )   &    |- ( ph -> A e. P )   &    |- M = ( S ` A )   =>    |- ( ph -> M : P --> P )
Theorem	mircl 25556	Closure of the point inversion function. (Contributed by Thierry Arnoux, 20-Oct-2019.)
|- P = ( Base ` G )   &    |- .- = ( dist ` G )   &    |- I = (Itv ` G )   &    |- L = (LineG ` G )   &    |- S = (pInvG ` G )   &    |- ( ph -> G e. TarskiG )   &    |- ( ph -> A e. P )   &    |- M = ( S ` A )   &    |- ( ph -> X e. P )   =>    |- ( ph -> ( M ` X ) e. P )
Theorem	mirmir 25557	The point inversion function is an involution. Theorem 7.7 of [Schwabhauser] p. 49. (Contributed by Thierry Arnoux, 3-Jun-2019.)
|- P = ( Base ` G )   &    |- .- = ( dist ` G )   &    |- I = (Itv ` G )   &    |- L = (LineG ` G )   &    |- S = (pInvG ` G )   &    |- ( ph -> G e. TarskiG )   &    |- ( ph -> A e. P )   &    |- M = ( S ` A )   &    |- ( ph -> B e. P )   =>    |- ( ph -> ( M ` ( M ` B ) ) = B )
Theorem	mircom 25558	Variation on mirmir 25557. (Contributed by Thierry Arnoux, 10-Nov-2019.)
|- P = ( Base ` G )   &    |- .- = ( dist ` G )   &    |- I = (Itv ` G )   &    |- L = (LineG ` G )   &    |- S = (pInvG ` G )   &    |- ( ph -> G e. TarskiG )   &    |- ( ph -> A e. P )   &    |- M = ( S ` A )   &    |- ( ph -> B e. P )   &    |- ( ph -> ( M ` B ) = C )   =>    |- ( ph -> ( M ` C ) = B )
Theorem	mirreu 25559*	Any point has a unique antecedent through point inversion. Theorem 7.8 of [Schwabhauser] p. 50. (Contributed by Thierry Arnoux, 3-Jun-2019.)
|- P = ( Base ` G )   &    |- .- = ( dist ` G )   &    |- I = (Itv ` G )   &    |- L = (LineG ` G )   &    |- S = (pInvG ` G )   &    |- ( ph -> G e. TarskiG )   &    |- ( ph -> A e. P )   &    |- M = ( S ` A )   &    |- ( ph -> B e. P )   =>    |- ( ph -> E! a e. P ( M ` a ) = B )
Theorem	mireq 25560	Equality deduction for point inversion. Theorem 7.9 of [Schwabhauser] p. 50. (Contributed by Thierry Arnoux, 30-May-2019.)
|- P = ( Base ` G )   &    |- .- = ( dist ` G )   &    |- I = (Itv ` G )   &    |- L = (LineG ` G )   &    |- S = (pInvG ` G )   &    |- ( ph -> G e. TarskiG )   &    |- ( ph -> A e. P )   &    |- M = ( S ` A )   &    |- ( ph -> B e. P )   &    |- ( ph -> C e. P )   &    |- ( ph -> ( M ` B ) = ( M ` C ) )   =>    |- ( ph -> B = C )
Theorem	mirinv 25561	The only invariant point of a point inversion Theorem 7.3 of [Schwabhauser] p. 49, Theorem 7.10 of [Schwabhauser] p. 50. (Contributed by Thierry Arnoux, 30-Jul-2019.)
|- P = ( Base ` G )   &    |- .- = ( dist ` G )   &    |- I = (Itv ` G )   &    |- L = (LineG ` G )   &    |- S = (pInvG ` G )   &    |- ( ph -> G e. TarskiG )   &    |- ( ph -> A e. P )   &    |- M = ( S ` A )   &    |- ( ph -> B e. P )   =>    |- ( ph -> ( ( M ` B ) = B <-> A = B ) )
Theorem	mirne 25562	Mirror of non-center point cannot be the center point. (Contributed by Thierry Arnoux, 27-Sep-2020.)
|- P = ( Base ` G )   &    |- .- = ( dist ` G )   &    |- I = (Itv ` G )   &    |- L = (LineG ` G )   &    |- S = (pInvG ` G )   &    |- ( ph -> G e. TarskiG )   &    |- ( ph -> A e. P )   &    |- M = ( S ` A )   &    |- ( ph -> B e. P )   &    |- ( ph -> B =/= A )   =>    |- ( ph -> ( M ` B ) =/= A )
Theorem	mircinv 25563	The center point is invariant of a point inversion. (Contributed by Thierry Arnoux, 25-Aug-2019.)
|- P = ( Base ` G )   &    |- .- = ( dist ` G )   &    |- I = (Itv ` G )   &    |- L = (LineG ` G )   &    |- S = (pInvG ` G )   &    |- ( ph -> G e. TarskiG )   &    |- ( ph -> A e. P )   &    |- M = ( S ` A )   =>    |- ( ph -> ( M ` A ) = A )
Theorem	mirf1o 25564	The point inversion function M is a bijection. Theorem 7.11 of [Schwabhauser] p. 50. (Contributed by Thierry Arnoux, 6-Jun-2019.)
|- P = ( Base ` G )   &    |- .- = ( dist ` G )   &    |- I = (Itv ` G )   &    |- L = (LineG ` G )   &    |- S = (pInvG ` G )   &    |- ( ph -> G e. TarskiG )   &    |- ( ph -> A e. P )   &    |- M = ( S ` A )   =>    |- ( ph -> M : P -1-1-onto-> P )
Theorem	miriso 25565	The point inversion function is an isometry, i.e. it is conserves congruence. Because it is also a bijection, it is also a motion. Theorem 7.13 of [Schwabhauser] p. 50. (Contributed by Thierry Arnoux, 6-Jun-2019.)
|- P = ( Base ` G )   &    |- .- = ( dist ` G )   &    |- I = (Itv ` G )   &    |- L = (LineG ` G )   &    |- S = (pInvG ` G )   &    |- ( ph -> G e. TarskiG )   &    |- ( ph -> A e. P )   &    |- M = ( S ` A )   &    |- ( ph -> X e. P )   &    |- ( ph -> Y e. P )   =>    |- ( ph -> ( ( M ` X ) .- ( M ` Y ) ) = ( X .- Y ) )
Theorem	mirbtwni 25566	Point inversion preserves betweenness, first half of Theorem 7.15 of [Schwabhauser] p. 51. (Contributed by Thierry Arnoux, 9-Jun-2019.)
|- P = ( Base ` G )   &    |- .- = ( dist ` G )   &    |- I = (Itv ` G )   &    |- L = (LineG ` G )   &    |- S = (pInvG ` G )   &    |- ( ph -> G e. TarskiG )   &    |- ( ph -> A e. P )   &    |- M = ( S ` A )   &    |- ( ph -> X e. P )   &    |- ( ph -> Y e. P )   &    |- ( ph -> Z e. P )   &    |- ( ph -> Y e. ( X I Z ) )   =>    |- ( ph -> ( M ` Y ) e. ( ( M ` X ) I ( M ` Z ) ) )
Theorem	mirbtwnb 25567	Point inversion preserves betweenness. Theorem 7.15 of [Schwabhauser] p. 51. (Contributed by Thierry Arnoux, 9-Jun-2019.)
|- P = ( Base ` G )   &    |- .- = ( dist ` G )   &    |- I = (Itv ` G )   &    |- L = (LineG ` G )   &    |- S = (pInvG ` G )   &    |- ( ph -> G e. TarskiG )   &    |- ( ph -> A e. P )   &    |- M = ( S ` A )   &    |- ( ph -> X e. P )   &    |- ( ph -> Y e. P )   &    |- ( ph -> Z e. P )   =>    |- ( ph -> ( Y e. ( X I Z ) <-> ( M ` Y ) e. ( ( M ` X ) I ( M ` Z ) ) ) )
Theorem	mircgrs 25568	Point inversion preserves congruence. Theorem 7.16 of [Schwabhauser] p. 51. (Contributed by Thierry Arnoux, 30-Jul-2019.)
|- P = ( Base ` G )   &    |- .- = ( dist ` G )   &    |- I = (Itv ` G )   &    |- L = (LineG ` G )   &    |- S = (pInvG ` G )   &    |- ( ph -> G e. TarskiG )   &    |- ( ph -> A e. P )   &    |- M = ( S ` A )   &    |- ( ph -> X e. P )   &    |- ( ph -> Y e. P )   &    |- ( ph -> Z e. P )   &    |- ( ph -> T e. P )   &    |- ( ph -> ( X .- Y ) = ( Z .- T ) )   =>    |- ( ph -> ( ( M ` X ) .- ( M ` Y ) ) = ( ( M ` Z ) .- ( M ` T ) ) )
Theorem	mirmir2 25569	Point inversion of a point inversion through another point. (Contributed by Thierry Arnoux, 3-Nov-2019.)
|- P = ( Base ` G )   &    |- .- = ( dist ` G )   &    |- I = (Itv ` G )   &    |- L = (LineG ` G )   &    |- S = (pInvG ` G )   &    |- ( ph -> G e. TarskiG )   &    |- ( ph -> A e. P )   &    |- M = ( S ` A )   &    |- ( ph -> X e. P )   &    |- ( ph -> Y e. P )   =>    |- ( ph -> ( M ` ( ( S ` Y ) ` X ) ) = ( ( S ` ( M ` Y ) ) ` ( M ` X ) ) )
Theorem	mirmot 25570	Point investion is a motion of the geometric space. Theorem 7.14 of [Schwabhauser] p. 51. (Contributed by Thierry Arnoux, 15-Dec-2019.)
|- P = ( Base ` G )   &    |- .- = ( dist ` G )   &    |- I = (Itv ` G )   &    |- L = (LineG ` G )   &    |- S = (pInvG ` G )   &    |- ( ph -> G e. TarskiG )   &    |- M = ( S ` A )   &    |- ( ph -> A e. P )   =>    |- ( ph -> M e. ( GIsmt G ) )
Theorem	mirln 25571	If two points are on the same line, so is the mirror point of one through the other. (Contributed by Thierry Arnoux, 21-Dec-2019.)
|- P = ( Base ` G )   &    |- .- = ( dist ` G )   &    |- I = (Itv ` G )   &    |- L = (LineG ` G )   &    |- S = (pInvG ` G )   &    |- ( ph -> G e. TarskiG )   &    |- M = ( S ` A )   &    |- ( ph -> D e. ran L )   &    |- ( ph -> A e. D )   &    |- ( ph -> B e. D )   =>    |- ( ph -> ( M ` B ) e. D )
Theorem	mirln2 25572	If a point and its mirror point are both on the same line, so is the center of the point inversion. (Contributed by Thierry Arnoux, 3-Mar-2020.)
|- P = ( Base ` G )   &    |- .- = ( dist ` G )   &    |- I = (Itv ` G )   &    |- L = (LineG ` G )   &    |- S = (pInvG ` G )   &    |- ( ph -> G e. TarskiG )   &    |- M = ( S ` A )   &    |- ( ph -> D e. ran L )   &    |- ( ph -> A e. P )   &    |- ( ph -> B e. D )   &    |- ( ph -> ( M ` B ) e. D )   =>    |- ( ph -> A e. D )
Theorem	mirconn 25573	Point inversion of connectedness. (Contributed by Thierry Arnoux, 2-Mar-2020.)
|- P = ( Base ` G )   &    |- .- = ( dist ` G )   &    |- I = (Itv ` G )   &    |- L = (LineG ` G )   &    |- S = (pInvG ` G )   &    |- ( ph -> G e. TarskiG )   &    |- M = ( S ` A )   &    |- ( ph -> A e. P )   &    |- ( ph -> X e. P )   &    |- ( ph -> Y e. P )   &    |- ( ph -> ( X e. ( A I Y ) \/ Y e. ( A I X ) ) )   =>    |- ( ph -> A e. ( X I ( M ` Y ) ) )
Theorem	mirhl 25574	If two points X and Y are on the same half-line from Z, the same applies to the mirror points. (Contributed by Thierry Arnoux, 21-Feb-2020.)
|- P = ( Base ` G )   &    |- .- = ( dist ` G )   &    |- I = (Itv ` G )   &    |- L = (LineG ` G )   &    |- S = (pInvG ` G )   &    |- ( ph -> G e. TarskiG )   &    |- M = ( S ` A )   &    |- K = (hlG ` G )   &    |- ( ph -> A e. P )   &    |- ( ph -> X e. P )   &    |- ( ph -> Y e. P )   &    |- ( ph -> Z e. P )   &    |- ( ph -> X ( K ` Z ) Y )   =>    |- ( ph -> ( M ` X ) ( K ` ( M ` Z ) ) ( M ` Y ) )
Theorem	mirbtwnhl 25575	If the center of the point inversion A is between two points X and Y, then the half lines are mirrored. (Contributed by Thierry Arnoux, 3-Mar-2020.)
|- P = ( Base ` G )   &    |- .- = ( dist ` G )   &    |- I = (Itv ` G )   &    |- L = (LineG ` G )   &    |- S = (pInvG ` G )   &    |- ( ph -> G e. TarskiG )   &    |- M = ( S ` A )   &    |- K = (hlG ` G )   &    |- ( ph -> A e. P )   &    |- ( ph -> X e. P )   &    |- ( ph -> Y e. P )   &    |- ( ph -> Z e. P )   &    |- ( ph -> X =/= A )   &    |- ( ph -> Y =/= A )   &    |- ( ph -> A e. ( X I Y ) )   =>    |- ( ph -> ( Z ( K ` A ) X <-> ( M ` Z ) ( K ` A ) Y ) )
Theorem	mirhl2 25576	Deduce half-line relation from mirror point. (Contributed by Thierry Arnoux, 8-Aug-2020.)
|- P = ( Base ` G )   &    |- .- = ( dist ` G )   &    |- I = (Itv ` G )   &    |- L = (LineG ` G )   &    |- S = (pInvG ` G )   &    |- ( ph -> G e. TarskiG )   &    |- M = ( S ` A )   &    |- K = (hlG ` G )   &    |- ( ph -> A e. P )   &    |- ( ph -> X e. P )   &    |- ( ph -> Y e. P )   &    |- ( ph -> Z e. P )   &    |- ( ph -> X =/= A )   &    |- ( ph -> Y =/= A )   &    |- ( ph -> A e. ( X I ( M ` Y ) ) )   =>    |- ( ph -> X ( K ` A ) Y )
Theorem	mircgrextend 25577	Link congruence over a pair of mirror points. cf tgcgrextend 25380. (Contributed by Thierry Arnoux, 4-Oct-2020.)
|- P = ( Base ` G )   &    |- .- = ( dist ` G )   &    |- I = (Itv ` G )   &    |- L = (LineG ` G )   &    |- S = (pInvG ` G )   &    |- ( ph -> G e. TarskiG )   &    |- .~ = (cgrG ` G )   &    |- M = ( S ` B )   &    |- N = ( S ` Y )   &    |- ( ph -> A e. P )   &    |- ( ph -> B e. P )   &    |- ( ph -> X e. P )   &    |- ( ph -> Y e. P )   &    |- ( ph -> ( A .- B ) = ( X .- Y ) )   =>    |- ( ph -> ( A .- ( M ` A ) ) = ( X .- ( N ` X ) ) )
Theorem	mirtrcgr 25578	Point inversion of one point of a triangle around another point preserves triangle congruence. (Contributed by Thierry Arnoux, 4-Oct-2020.)
|- P = ( Base ` G )   &    |- .- = ( dist ` G )   &    |- I = (Itv ` G )   &    |- L = (LineG ` G )   &    |- S = (pInvG ` G )   &    |- ( ph -> G e. TarskiG )   &    |- .~ = (cgrG ` G )   &    |- M = ( S ` B )   &    |- N = ( S ` Y )   &    |- ( ph -> A e. P )   &    |- ( ph -> B e. P )   &    |- ( ph -> X e. P )   &    |- ( ph -> Y e. P )   &    |- ( ph -> C e. P )   &    |- ( ph -> Z e. P )   &    |- ( ph -> A =/= B )   &    |- ( ph -> <" A B C "> .~ <" X Y Z "> )   =>    |- ( ph -> <" ( M ` A ) B C "> .~ <" ( N ` X ) Y Z "> )
Theorem	mirauto 25579	Point inversion preserves point inversion. (Contributed by Thierry Arnoux, 30-Jul-2019.)
|- P = ( Base ` G )   &    |- .- = ( dist ` G )   &    |- I = (Itv ` G )   &    |- L = (LineG ` G )   &    |- S = (pInvG ` G )   &    |- ( ph -> G e. TarskiG )   &    |- M = ( S ` T )   &    |- X = ( M ` A )   &    |- Y = ( M ` B )   &    |- Z = ( M ` C )   &    |- ( ph -> T e. P )   &    |- ( ph -> A e. P )   &    |- ( ph -> B e. P )   &    |- ( ph -> C e. P )   &    |- ( ph -> ( ( S ` A ) ` B ) = C )   =>    |- ( ph -> ( ( S ` X ) ` Y ) = Z )
Theorem	miduniq 25580	Unicity of the middle point, expressed with point inversion. Theorem 7.17 of [Schwabhauser] p. 51. (Contributed by Thierry Arnoux, 30-Jul-2019.)
|- P = ( Base ` G )   &    |- .- = ( dist ` G )   &    |- I = (Itv ` G )   &    |- L = (LineG ` G )   &    |- S = (pInvG ` G )   &    |- ( ph -> G e. TarskiG )   &    |- ( ph -> A e. P )   &    |- ( ph -> B e. P )   &    |- ( ph -> X e. P )   &    |- ( ph -> Y e. P )   &    |- ( ph -> ( ( S ` A ) ` X ) = Y )   &    |- ( ph -> ( ( S ` B ) ` X ) = Y )   =>    |- ( ph -> A = B )
Theorem	miduniq1 25581	Unicity of the middle point, expressed with point inversion. Theorem 7.18 of [Schwabhauser] p. 52. (Contributed by Thierry Arnoux, 30-Jul-2019.)
|- P = ( Base ` G )   &    |- .- = ( dist ` G )   &    |- I = (Itv ` G )   &    |- L = (LineG ` G )   &    |- S = (pInvG ` G )   &    |- ( ph -> G e. TarskiG )   &    |- ( ph -> A e. P )   &    |- ( ph -> B e. P )   &    |- ( ph -> X e. P )   &    |- ( ph -> ( ( S ` A ) ` X ) = ( ( S ` B ) ` X ) )   =>    |- ( ph -> A = B )
Theorem	miduniq2 25582	If two point inversions commute, they are identical. Theorem 7.19 of [Schwabhauser] p. 52. (Contributed by Thierry Arnoux, 30-Jul-2019.)
|- P = ( Base ` G )   &    |- .- = ( dist ` G )   &    |- I = (Itv ` G )   &    |- L = (LineG ` G )   &    |- S = (pInvG ` G )   &    |- ( ph -> G e. TarskiG )   &    |- ( ph -> A e. P )   &    |- ( ph -> B e. P )   &    |- ( ph -> X e. P )   &    |- ( ph -> ( ( S ` A ) ` ( ( S ` B ) ` X ) ) = ( ( S ` B ) ` ( ( S ` A ) ` X ) ) )   =>    |- ( ph -> A = B )
Theorem	colmid 25583	Colinearity and equidistance implies midpoint. Theorem 7.20 of [Schwabhauser] p. 52. (Contributed by Thierry Arnoux, 30-Jul-2019.)
|- P = ( Base ` G )   &    |- .- = ( dist ` G )   &    |- I = (Itv ` G )   &    |- L = (LineG ` G )   &    |- S = (pInvG ` G )   &    |- ( ph -> G e. TarskiG )   &    |- M = ( S ` X )   &    |- ( ph -> A e. P )   &    |- ( ph -> B e. P )   &    |- ( ph -> X e. P )   &    |- ( ph -> ( X e. ( A L B ) \/ A = B ) )   &    |- ( ph -> ( X .- A ) = ( X .- B ) )   =>    |- ( ph -> ( B = ( M ` A ) \/ A = B ) )
Theorem	symquadlem 25584	Lemma of the symetrial quadrilateral. The diagonals of quadrilaterals with congruent opposing sides intersect at their middle point. In Euclidean geometry, such quadrilaterals are called parallelograms, as opposing sides are parallel. However, this is not necessarily true in the case of absolute geometry. Lemma 7.21 of [Schwabhauser] p. 52. (Contributed by Thierry Arnoux, 6-Aug-2019.)
|- P = ( Base ` G )   &    |- .- = ( dist ` G )   &    |- I = (Itv ` G )   &    |- L = (LineG ` G )   &    |- S = (pInvG ` G )   &    |- ( ph -> G e. TarskiG )   &    |- M = ( S ` X )   &    |- ( ph -> A e. P )   &    |- ( ph -> B e. P )   &    |- ( ph -> C e. P )   &    |- ( ph -> D e. P )   &    |- ( ph -> X e. P )   &    |- ( ph -> -. ( A e. ( B L C ) \/ B = C ) )   &    |- ( ph -> B =/= D )   &    |- ( ph -> ( A .- B ) = ( C .- D ) )   &    |- ( ph -> ( B .- C ) = ( D .- A ) )   &    |- ( ph -> ( X e. ( A L C ) \/ A = C ) )   &    |- ( ph -> ( X e. ( B L D ) \/ B = D ) )   =>    |- ( ph -> A = ( M ` C ) )
Theorem	krippenlem 25585	Lemma for krippen 25586. We can assume krippen.7 "without loss of generality" (Contributed by Thierry Arnoux, 12-Aug-2019.)
|- P = ( Base ` G )   &    |- .- = ( dist ` G )   &    |- I = (Itv ` G )   &    |- L = (LineG ` G )   &    |- S = (pInvG ` G )   &    |- ( ph -> G e. TarskiG )   &    |- M = ( S ` X )   &    |- N = ( S ` Y )   &    |- ( ph -> A e. P )   &    |- ( ph -> B e. P )   &    |- ( ph -> C e. P )   &    |- ( ph -> E e. P )   &    |- ( ph -> F e. P )   &    |- ( ph -> X e. P )   &    |- ( ph -> Y e. P )   &    |- ( ph -> C e. ( A I E ) )   &    |- ( ph -> C e. ( B I F ) )   &    |- ( ph -> ( C .- A ) = ( C .- B ) )   &    |- ( ph -> ( C .- E ) = ( C .- F ) )   &    |- ( ph -> B = ( M ` A ) )   &    |- ( ph -> F = ( N ` E ) )   &    |- .<_ = (≤G ` G )   &    |- ( ph -> ( C .- A ) .<_ ( C .- E ) )   =>    |- ( ph -> C e. ( X I Y ) )
Theorem	krippen 25586	Krippenlemma (German for crib's lemma) Lemma 7.22 of [Schwabhauser] p. 53. proven by Gupta 1965 as Theorem 3.45. (Contributed by Thierry Arnoux, 12-Aug-2019.)
|- P = ( Base ` G )   &    |- .- = ( dist ` G )   &    |- I = (Itv ` G )   &    |- L = (LineG ` G )   &    |- S = (pInvG ` G )   &    |- ( ph -> G e. TarskiG )   &    |- M = ( S ` X )   &    |- N = ( S ` Y )   &    |- ( ph -> A e. P )   &    |- ( ph -> B e. P )   &    |- ( ph -> C e. P )   &    |- ( ph -> E e. P )   &    |- ( ph -> F e. P )   &    |- ( ph -> X e. P )   &    |- ( ph -> Y e. P )   &    |- ( ph -> C e. ( A I E ) )   &    |- ( ph -> C e. ( B I F ) )   &    |- ( ph -> ( C .- A ) = ( C .- B ) )   &    |- ( ph -> ( C .- E ) = ( C .- F ) )   &    |- ( ph -> B = ( M ` A ) )   &    |- ( ph -> F = ( N ` E ) )   =>    |- ( ph -> C e. ( X I Y ) )
Theorem	midexlem 25587*	Lemma for the existence of a middle point. Lemma 7.25 of [Schwabhauser] p. 55. This proof of the existence of a midpoint requires the existence of a third point C equidistant to A and B This condition will be removed later. Because the operation notation ( A (midG ` G ) B ) for a midpoint implies its uniqueness, it cannot be used until uniqueness is proven, and until then, an equivalent mirror point notation B = ( M ` A ) has to be used. See mideu 25630 for the existence and uniqueness of the midpoint. (Contributed by Thierry Arnoux, 25-Aug-2019.)
|- P = ( Base ` G )   &    |- .- = ( dist ` G )   &    |- I = (Itv ` G )   &    |- L = (LineG ` G )   &    |- S = (pInvG ` G )   &    |- ( ph -> G e. TarskiG )   &    |- M = ( S ` x )   &    |- ( ph -> A e. P )   &    |- ( ph -> B e. P )   &    |- ( ph -> C e. P )   &    |- ( ph -> ( C .- A ) = ( C .- B ) )   =>    |- ( ph -> E. x e. P B = ( M ` A ) )
15.2.13  Right angles
Syntax	crag 25588	Declare the constant for the class of right angles.
class ∟G
Definition	df-rag 25589*	Define the class of right angles. Definition 8.1 of [Schwabhauser] p. 57. See israg 25592. (Contributed by Thierry Arnoux, 25-Aug-2019.)
|- ∟G = ( g e. _V |-> { w e. Word ( Base ` g ) | ( ( # ` w ) = 3 /\ ( ( w ` 0 ) ( dist ` g ) ( w ` 2 ) ) = ( ( w ` 0 ) ( dist ` g ) ( ( (pInvG ` g ) ` ( w ` 1 ) ) ` ( w ` 2 ) ) ) ) } )
Syntax	cperpg 25590	Declare the constant for the perpendicular relation.
class ⟂G
Definition	df-perpg 25591*	Define the "perpendicular" relation. Definition 8.11 of [Schwabhauser] p. 59. See isperp 25607. (Contributed by Thierry Arnoux, 8-Sep-2019.)
|- ⟂G = ( g e. _V |-> { <. a , b >. | ( ( a e. ran (LineG ` g ) /\ b e. ran (LineG ` g ) ) /\ E. x e. ( a i^i b ) A. u e. a A. v e. b <" u x v "> e. (∟G ` g ) ) } )
Theorem	israg 25592	Property for 3 points A, B, C to form a right angle. Definition 8.1 of [Schwabhauser] p. 57. (Contributed by Thierry Arnoux, 25-Aug-2019.)
|- P = ( Base ` G )   &    |- .- = ( dist ` G )   &    |- I = (Itv ` G )   &    |- L = (LineG ` G )   &    |- S = (pInvG ` G )   &    |- ( ph -> G e. TarskiG )   &    |- ( ph -> A e. P )   &    |- ( ph -> B e. P )   &    |- ( ph -> C e. P )   =>    |- ( ph -> ( <" A B C "> e. (∟G ` G ) <-> ( A .- C ) = ( A .- ( ( S ` B ) ` C ) ) ) )
Theorem	ragcom 25593	Commutative rule for right angles. Theorem 8.2 of [Schwabhauser] p. 57. (Contributed by Thierry Arnoux, 25-Aug-2019.)
|- P = ( Base ` G )   &    |- .- = ( dist ` G )   &    |- I = (Itv ` G )   &    |- L = (LineG ` G )   &    |- S = (pInvG ` G )   &    |- ( ph -> G e. TarskiG )   &    |- ( ph -> A e. P )   &    |- ( ph -> B e. P )   &    |- ( ph -> C e. P )   &    |- ( ph -> <" A B C "> e. (∟G ` G ) )   =>    |- ( ph -> <" C B A "> e. (∟G ` G ) )
Theorem	ragcol 25594	The right angle property is independent of the choice of point on one side. Theorem 8.3 of [Schwabhauser] p. 58. (Contributed by Thierry Arnoux, 25-Aug-2019.)
|- P = ( Base ` G )   &    |- .- = ( dist ` G )   &    |- I = (Itv ` G )   &    |- L = (LineG ` G )   &    |- S = (pInvG ` 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 "> e. (∟G ` G ) )   &    |- ( ph -> A =/= B )   &    |- ( ph -> ( A e. ( B L D ) \/ B = D ) )   =>    |- ( ph -> <" D B C "> e. (∟G ` G ) )
Theorem	ragmir 25595	Right angle property is preserved by point inversion. Theorem 8.4 of [Schwabhauser] p. 58. (Contributed by Thierry Arnoux, 25-Aug-2019.)
|- P = ( Base ` G )   &    |- .- = ( dist ` G )   &    |- I = (Itv ` G )   &    |- L = (LineG ` G )   &    |- S = (pInvG ` G )   &    |- ( ph -> G e. TarskiG )   &    |- ( ph -> A e. P )   &    |- ( ph -> B e. P )   &    |- ( ph -> C e. P )   &    |- ( ph -> <" A B C "> e. (∟G ` G ) )   =>    |- ( ph -> <" A B ( ( S ` B ) ` C ) "> e. (∟G ` G ) )
Theorem	mirrag 25596	Right angle is conserved by point inversion. (Contributed by Thierry Arnoux, 3-Nov-2019.)
|- P = ( Base ` G )   &    |- .- = ( dist ` G )   &    |- I = (Itv ` G )   &    |- L = (LineG ` G )   &    |- S = (pInvG ` G )   &    |- ( ph -> G e. TarskiG )   &    |- ( ph -> A e. P )   &    |- ( ph -> B e. P )   &    |- ( ph -> C e. P )   &    |- ( ph -> <" A B C "> e. (∟G ` G ) )   &    |- M = ( S ` D )   &    |- ( ph -> D e. P )   =>    |- ( ph -> <" ( M ` A ) ( M ` B ) ( M ` C ) "> e. (∟G ` G ) )
Theorem	ragtrivb 25597	Trivial right angle. Theorem 8.5 of [Schwabhauser] p. 58. (Contributed by Thierry Arnoux, 25-Aug-2019.)
|- P = ( Base ` G )   &    |- .- = ( dist ` G )   &    |- I = (Itv ` G )   &    |- L = (LineG ` G )   &    |- S = (pInvG ` G )   &    |- ( ph -> G e. TarskiG )   &    |- ( ph -> A e. P )   &    |- ( ph -> B e. P )   &    |- ( ph -> C e. P )   =>    |- ( ph -> <" A B B "> e. (∟G ` G ) )
Theorem	ragflat2 25598	Deduce equality from two right angles. Theorem 8.6 of [Schwabhauser] p. 58. (Contributed by Thierry Arnoux, 3-Sep-2019.)
|- P = ( Base ` G )   &    |- .- = ( dist ` G )   &    |- I = (Itv ` G )   &    |- L = (LineG ` G )   &    |- S = (pInvG ` 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 "> e. (∟G ` G ) )   &    |- ( ph -> <" D B C "> e. (∟G ` G ) )   &    |- ( ph -> C e. ( A I D ) )   =>    |- ( ph -> B = C )
Theorem	ragflat 25599	Deduce equality from two right angles. Theorem 8.7 of [Schwabhauser] p. 58. (Contributed by Thierry Arnoux, 3-Sep-2019.)
|- P = ( Base ` G )   &    |- .- = ( dist ` G )   &    |- I = (Itv ` G )   &    |- L = (LineG ` G )   &    |- S = (pInvG ` G )   &    |- ( ph -> G e. TarskiG )   &    |- ( ph -> A e. P )   &    |- ( ph -> B e. P )   &    |- ( ph -> C e. P )   &    |- ( ph -> <" A B C "> e. (∟G ` G ) )   &    |- ( ph -> <" A C B "> e. (∟G ` G ) )   =>    |- ( ph -> B = C )
Theorem	ragtriva 25600	Trivial right angle. Theorem 8.8 of [Schwabhauser] p. 58. (Contributed by Thierry Arnoux, 3-Sep-2019.)
|- P = ( Base ` G )   &    |- .- = ( dist ` G )   &    |- I = (Itv ` G )   &    |- L = (LineG ` G )   &    |- S = (pInvG ` G )   &    |- ( ph -> G e. TarskiG )   &    |- ( ph -> A e. P )   &    |- ( ph -> B e. P )   &    |- ( ph -> C e. P )   &    |- ( ph -> <" A B A "> e. (∟G ` G ) )   =>    |- ( ph -> A = B )