P. 239 of Theorem List - Metamath Proof Explorer

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

Type	Label	Description
Statement
Theorem	isperp2d 23801	One direction of isperp2 23800 (Contributed by Thierry Arnoux, 10-Nov-2019.)
|- P = ( Base ` G )   &    |- .- = ( dist ` G )   &    |- I = (Itv ` G )   &    |- L = (LineG ` G )   &    |- ( ph -> G e. TarskiG )   &    |- ( ph -> A e. ran L )   &    |- ( ph -> B e. ran L )   &    |- ( ph -> X e. ( A i^i B ) )   &    |- ( ph -> U e. A )   &    |- ( ph -> V e. B )   &    |- ( ph -> A (⟂G ` G ) B )   =>    |- ( ph -> <" U X V "> e. (∟G ` G ) )
Theorem	ragperp 23802	Deduce that two lines are perpendicular from a right angle statement. One direction of theorem 8.13 of [Schwabhauser] p. 59. (Contributed by Thierry Arnoux, 20-Oct-2019.)
|- P = ( Base ` G )   &    |- .- = ( dist ` G )   &    |- I = (Itv ` G )   &    |- L = (LineG ` G )   &    |- ( ph -> G e. TarskiG )   &    |- ( ph -> A e. ran L )   &    |- ( ph -> B e. ran L )   &    |- ( ph -> X e. ( A i^i B ) )   &    |- ( ph -> U e. A )   &    |- ( ph -> V e. B )   &    |- ( ph -> U =/= X )   &    |- ( ph -> V =/= X )   &    |- ( ph -> <" U X V "> e. (∟G ` G ) )   =>    |- ( ph -> A (⟂G ` G ) B )
Theorem	footex 23803*	Lemma for foot 23804: existence part. (Contributed by Thierry Arnoux, 19-Oct-2019.)
|- P = ( Base ` G )   &    |- .- = ( dist ` G )   &    |- I = (Itv ` G )   &    |- L = (LineG ` G )   &    |- ( ph -> G e. TarskiG )   &    |- ( ph -> A e. ran L )   &    |- ( ph -> C e. P )   &    |- ( ph -> -. C e. A )   =>    |- ( ph -> E. x e. A ( C L x ) (⟂G ` G ) A )
Theorem	foot 23804*	From a point C outside of a line A, there exists a unique point x on A such that ( C L x ) is perpendicular to A. That point is called the foot from C on A. Theorem 8.18 of [Schwabhauser] p. 60. (Contributed by Thierry Arnoux, 19-Oct-2019.)
|- P = ( Base ` G )   &    |- .- = ( dist ` G )   &    |- I = (Itv ` G )   &    |- L = (LineG ` G )   &    |- ( ph -> G e. TarskiG )   &    |- ( ph -> A e. ran L )   &    |- ( ph -> C e. P )   &    |- ( ph -> -. C e. A )   =>    |- ( ph -> E! x e. A ( C L x ) (⟂G ` G ) A )
Theorem	perprag 23805	Deduce a right angle from perpendicular lines. (Contributed by Thierry Arnoux, 10-Nov-2019.)
|- P = ( Base ` G )   &    |- .- = ( dist ` G )   &    |- I = (Itv ` G )   &    |- L = (LineG ` G )   &    |- ( ph -> G e. TarskiG )   &    |- ( ph -> A e. P )   &    |- ( ph -> B e. P )   &    |- ( ph -> C e. ( A L B ) )   &    |- ( ph -> D e. P )   &    |- ( ph -> ( A L B ) (⟂G ` G ) ( C L D ) )   =>    |- ( ph -> <" A C D "> e. (∟G ` G ) )
Theorem	perpdragALT 23806	Deduce a right angle from perpendicular lines. (Contributed by Thierry Arnoux, 12-Dec-2019.)
|- P = ( Base ` G )   &    |- .- = ( dist ` G )   &    |- I = (Itv ` G )   &    |- L = (LineG ` G )   &    |- ( ph -> G e. TarskiG )   &    |- ( ph -> A e. D )   &    |- ( ph -> B e. D )   &    |- ( ph -> C e. P )   &    |- ( ph -> D (⟂G ` G ) ( B L C ) )   =>    |- ( ph -> <" A B C "> e. (∟G ` G ) )
Theorem	perpdrag 23807	Deduce a right angle from perpendicular lines. (Contributed by Thierry Arnoux, 12-Dec-2019.)
|- P = ( Base ` G )   &    |- .- = ( dist ` G )   &    |- I = (Itv ` G )   &    |- L = (LineG ` G )   &    |- ( ph -> G e. TarskiG )   &    |- ( ph -> A e. D )   &    |- ( ph -> B e. D )   &    |- ( ph -> C e. P )   &    |- ( ph -> D (⟂G ` G ) ( B L C ) )   =>    |- ( ph -> <" A B C "> e. (∟G ` G ) )
Theorem	colperp 23808	Deduce a perpendicularity from perpendicularity and colinearity. (Contributed by Thierry Arnoux, 8-Dec-2019.)
|- P = ( Base ` G )   &    |- .- = ( dist ` G )   &    |- I = (Itv ` G )   &    |- L = (LineG ` G )   &    |- ( ph -> G e. TarskiG )   &    |- ( ph -> A e. P )   &    |- ( ph -> B e. P )   &    |- ( ph -> C e. P )   &    |- ( ph -> ( A L B ) (⟂G ` G ) D )   &    |- ( ph -> ( C e. ( A L B ) \/ A = B ) )   &    |- ( ph -> A =/= C )   =>    |- ( ph -> ( A L C ) (⟂G ` G ) D )
Theorem	colperpexlem1 23809	Lemma for colperp 23808. First part of lemma 8.20 of [Schwabhauser] p. 62. (Contributed by Thierry Arnoux, 27-Oct-2019.)
|- P = ( Base ` G )   &    |- .- = ( dist ` G )   &    |- I = (Itv ` G )   &    |- L = (LineG ` G )   &    |- ( ph -> G e. TarskiG )   &    |- S = (pInvG ` G )   &    |- M = ( S ` A )   &    |- N = ( S ` B )   &    |- K = ( S ` Q )   &    |- ( ph -> A e. P )   &    |- ( ph -> B e. P )   &    |- ( ph -> C e. P )   &    |- ( ph -> Q e. P )   &    |- ( ph -> <" A B C "> e. (∟G ` G ) )   &    |- ( ph -> ( K ` ( M ` C ) ) = ( N ` C ) )   =>    |- ( ph -> <" B A Q "> e. (∟G ` G ) )
Theorem	colperpexlem2 23810	Lemma for colperpex 23812. Second part of lemma 8.20 of [Schwabhauser] p. 62. (Contributed by Thierry Arnoux, 10-Nov-2019.)
|- P = ( Base ` G )   &    |- .- = ( dist ` G )   &    |- I = (Itv ` G )   &    |- L = (LineG ` G )   &    |- ( ph -> G e. TarskiG )   &    |- S = (pInvG ` G )   &    |- M = ( S ` A )   &    |- N = ( S ` B )   &    |- K = ( S ` Q )   &    |- ( ph -> A e. P )   &    |- ( ph -> B e. P )   &    |- ( ph -> C e. P )   &    |- ( ph -> Q e. P )   &    |- ( ph -> <" A B C "> e. (∟G ` G ) )   &    |- ( ph -> ( K ` ( M ` C ) ) = ( N ` C ) )   &    |- ( ph -> B =/= C )   =>    |- ( ph -> A =/= Q )
Theorem	colperpexlem3 23811*	Lemma for colperpex 23812. Case 1 of theorem 8.21 of [Schwabhauser] p. 63. (Contributed by Thierry Arnoux, 20-Nov-2019.)
|- P = ( Base ` G )   &    |- .- = ( dist ` G )   &    |- I = (Itv ` G )   &    |- L = (LineG ` G )   &    |- ( ph -> G e. TarskiG )   &    |- ( ph -> A e. P )   &    |- ( ph -> B e. P )   &    |- ( ph -> C e. P )   &    |- ( ph -> A =/= B )   &    |- ( ph -> -. C e. ( A L B ) )   =>    |- ( ph -> E. p e. P ( ( A L p ) (⟂G ` G ) ( A L B ) /\ E. t e. P ( ( t e. ( A L B ) \/ A = B ) /\ t e. ( C I p ) ) ) )
Theorem	colperpex 23812*	In dimension 2 and above, on a line ( A L B ) there is always a perpendicular P from A on a given plane (here given by C, in case C does not lie on the line). Theorem 8.21 of [Schwabhauser] p. 63. (Contributed by Thierry Arnoux, 20-Nov-2019.)
|- P = ( Base ` G )   &    |- .- = ( dist ` G )   &    |- I = (Itv ` G )   &    |- L = (LineG ` G )   &    |- ( ph -> G e. TarskiG )   &    |- ( ph -> A e. P )   &    |- ( ph -> B e. P )   &    |- ( ph -> C e. P )   &    |- ( ph -> A =/= B )   &    |- ( ph -> GDimTarskiG≥ 2 )   =>    |- ( ph -> E. p e. P ( ( A L p ) (⟂G ` G ) ( A L B ) /\ E. t e. P ( ( t e. ( A L B ) \/ A = B ) /\ t e. ( C I p ) ) ) )
Theorem	mideulem 23813*	Lemma for mideu 23814. We can assume mideulem.9 "without loss of generality" (Contributed by Thierry Arnoux, 25-Nov-2019.)
|- P = ( Base ` G )   &    |- .- = ( dist ` G )   &    |- I = (Itv ` G )   &    |- L = (LineG ` G )   &    |- ( ph -> G e. TarskiG )   &    |- S = (pInvG ` G )   &    |- ( ph -> A e. P )   &    |- ( ph -> B e. P )   &    |- ( ph -> A =/= B )   &    |- ( ph -> Q e. P )   &    |- ( ph -> O e. P )   &    |- ( ph -> T e. P )   &    |- ( ph -> ( A L B ) (⟂G ` G ) ( Q L B ) )   &    |- ( ph -> ( A L B ) (⟂G ` G ) ( A L O ) )   &    |- ( ph -> T e. ( A L B ) )   &    |- ( ph -> T e. ( Q I O ) )   &    |- ( ph -> ( A .- O ) (≤G ` G ) ( B .- Q ) )   =>    |- ( ph -> E. x e. P B = ( ( S ` x ) ` A ) )
Theorem	mideu 23814*	Existence and uniqueness of the midpoint, Theorem 8.22 of [Schwabhauser] p. 64. Note that this proof requires a construction in 2 dimensions or more, i.e. it does not prove the existence of a midpoint in dimension 1, for a geometry restricted to a line. (Contributed by Thierry Arnoux, 25-Nov-2019.)
|- P = ( Base ` G )   &    |- .- = ( dist ` G )   &    |- I = (Itv ` G )   &    |- L = (LineG ` G )   &    |- ( ph -> G e. TarskiG )   &    |- S = (pInvG ` G )   &    |- ( ph -> A e. P )   &    |- ( ph -> B e. P )   &    |- ( ph -> GDimTarskiG≥ 2 )   =>    |- ( ph -> E! x e. P B = ( ( S ` x ) ` A ) )
15.2.13  Midpoints and Line Mirroring
Syntax	cmid 23815	Declare the constant for the midpoint operation.
class midG
Syntax	clmi 23816	Declare the constant for the line mirroring function.
class lInvG
Definition	df-mid 23817*	Define the midpoint operation. Definition 10.1 of [Schwabhauser] p. 88. (Contributed by Thierry Arnoux, 9-Jun-2019.)
|- midG = ( g e. _V |-> ( a e. ( Base ` g ) , b e. ( Base ` g ) |-> ( iota_ m e. ( Base ` g ) b = ( ( (pInvG ` g ) ` m ) ` a ) ) ) )
Definition	df-lmi 23818*	Define the line mirroring function. Definition 10.3 of [Schwabhauser] p. 89. (Contributed by Thierry Arnoux, 1-Dec-2019.)
|- lInvG = ( g e. _V |-> ( m e. ran (LineG ` g ) |-> ( a e. ( Base ` g ) |-> ( iota_ b e. ( Base ` g ) ( ( a (midG ` g ) b ) e. m /\ ( m (⟂G ` g ) ( a (LineG ` g ) b ) \/ a = b ) ) ) ) ) )
Theorem	midf 23819	Midpoint as a function. (Contributed by Thierry Arnoux, 1-Dec-2019.)
|- P = ( Base ` G )   &    |- .- = ( dist ` G )   &    |- I = (Itv ` G )   &    |- ( ph -> G e. TarskiG )   &    |- ( ph -> GDimTarskiG≥ 2 )   =>    |- ( ph -> (midG ` G ) : ( P X. P ) --> P )
Theorem	midcl 23820	Closure of the midpoint. (Contributed by Thierry Arnoux, 1-Dec-2019.)
|- P = ( Base ` G )   &    |- .- = ( dist ` G )   &    |- I = (Itv ` G )   &    |- ( ph -> G e. TarskiG )   &    |- ( ph -> GDimTarskiG≥ 2 )   &    |- ( ph -> A e. P )   &    |- ( ph -> B e. P )   =>    |- ( ph -> ( A (midG ` G ) B ) e. P )
Theorem	ismidb 23821	Property of the midpoint. (Contributed by Thierry Arnoux, 1-Dec-2019.)
|- P = ( Base ` G )   &    |- .- = ( dist ` G )   &    |- I = (Itv ` G )   &    |- ( ph -> G e. TarskiG )   &    |- ( ph -> GDimTarskiG≥ 2 )   &    |- ( ph -> A e. P )   &    |- ( ph -> B e. P )   &    |- S = (pInvG ` G )   &    |- ( ph -> M e. P )   =>    |- ( ph -> ( B = ( ( S ` M ) ` A ) <-> ( A (midG ` G ) B ) = M ) )
Theorem	midbtwn 23822	Betweenness of midpoint. (Contributed by Thierry Arnoux, 7-Dec-2019.)
|- P = ( Base ` G )   &    |- .- = ( dist ` G )   &    |- I = (Itv ` G )   &    |- ( ph -> G e. TarskiG )   &    |- ( ph -> GDimTarskiG≥ 2 )   &    |- ( ph -> A e. P )   &    |- ( ph -> B e. P )   =>    |- ( ph -> ( A (midG ` G ) B ) e. ( A I B ) )
Theorem	midcgr 23823	Congruence of midpoint. (Contributed by Thierry Arnoux, 7-Dec-2019.)
|- P = ( Base ` G )   &    |- .- = ( dist ` G )   &    |- I = (Itv ` G )   &    |- ( ph -> G e. TarskiG )   &    |- ( ph -> GDimTarskiG≥ 2 )   &    |- ( ph -> A e. P )   &    |- ( ph -> B e. P )   &    |- ( ph -> ( A (midG ` G ) B ) = C )   =>    |- ( ph -> ( C .- A ) = ( C .- B ) )
Theorem	midid 23824	Midpoint of a null segment. (Contributed by Thierry Arnoux, 7-Dec-2019.)
|- P = ( Base ` G )   &    |- .- = ( dist ` G )   &    |- I = (Itv ` G )   &    |- ( ph -> G e. TarskiG )   &    |- ( ph -> GDimTarskiG≥ 2 )   &    |- ( ph -> A e. P )   &    |- ( ph -> B e. P )   =>    |- ( ph -> ( A (midG ` G ) A ) = A )
Theorem	midcom 23825	Commutativity rule for the midpoint. (Contributed by Thierry Arnoux, 2-Dec-2019.)
|- P = ( Base ` G )   &    |- .- = ( dist ` G )   &    |- I = (Itv ` G )   &    |- ( ph -> G e. TarskiG )   &    |- ( ph -> GDimTarskiG≥ 2 )   &    |- ( ph -> A e. P )   &    |- ( ph -> B e. P )   =>    |- ( ph -> ( A (midG ` G ) B ) = ( B (midG ` G ) A ) )
Theorem	mirmid 23826	Point inversion preserves midpoints. (Contributed by Thierry Arnoux, 12-Dec-2019.)
|- P = ( Base ` G )   &    |- .- = ( dist ` G )   &    |- I = (Itv ` G )   &    |- ( ph -> G e. TarskiG )   &    |- ( ph -> GDimTarskiG≥ 2 )   &    |- ( ph -> A e. P )   &    |- ( ph -> B e. P )   &    |- S = ( (pInvG ` G ) ` M )   &    |- ( ph -> M e. P )   =>    |- ( ph -> ( ( S ` A ) (midG ` G ) ( S ` B ) ) = ( S ` ( A (midG ` G ) B ) ) )
Theorem	lmieu 23827*	Uniqueness of the line mirror point. Theorem 10.2 of [Schwabhauser] p. 88. (Contributed by Thierry Arnoux, 1-Dec-2019.)
|- P = ( Base ` G )   &    |- .- = ( dist ` G )   &    |- I = (Itv ` G )   &    |- ( ph -> G e. TarskiG )   &    |- ( ph -> GDimTarskiG≥ 2 )   &    |- L = (LineG ` G )   &    |- ( ph -> D e. ran L )   &    |- ( ph -> A e. P )   =>    |- ( ph -> E! b e. P ( ( A (midG ` G ) b ) e. D /\ ( D (⟂G ` G ) ( A L b ) \/ A = b ) ) )
Theorem	lmif 23828	Line mirror as a function. (Contributed by Thierry Arnoux, 11-Dec-2019.)
|- P = ( Base ` G )   &    |- .- = ( dist ` G )   &    |- I = (Itv ` G )   &    |- ( ph -> G e. TarskiG )   &    |- ( ph -> GDimTarskiG≥ 2 )   &    |- M = ( (lInvG ` G ) ` D )   &    |- L = (LineG ` G )   &    |- ( ph -> D e. ran L )   =>    |- ( ph -> M : P --> P )
Theorem	lmicl 23829	Closure of the line mirror. (Contributed by Thierry Arnoux, 11-Dec-2019.)
|- P = ( Base ` G )   &    |- .- = ( dist ` G )   &    |- I = (Itv ` G )   &    |- ( ph -> G e. TarskiG )   &    |- ( ph -> GDimTarskiG≥ 2 )   &    |- M = ( (lInvG ` G ) ` D )   &    |- L = (LineG ` G )   &    |- ( ph -> D e. ran L )   &    |- ( ph -> A e. P )   =>    |- ( ph -> ( M ` A ) e. P )
Theorem	islmib 23830	Property of the line mirror. (Contributed by Thierry Arnoux, 11-Dec-2019.)
|- P = ( Base ` G )   &    |- .- = ( dist ` G )   &    |- I = (Itv ` G )   &    |- ( ph -> G e. TarskiG )   &    |- ( ph -> GDimTarskiG≥ 2 )   &    |- M = ( (lInvG ` G ) ` D )   &    |- L = (LineG ` G )   &    |- ( ph -> D e. ran L )   &    |- ( ph -> A e. P )   &    |- ( ph -> B e. P )   =>    |- ( ph -> ( B = ( M ` A ) <-> ( ( A (midG ` G ) B ) e. D /\ ( D (⟂G ` G ) ( A L B ) \/ A = B ) ) ) )
Theorem	lmicom 23831	The line mirroring function is an involution. Theorem 10.4 of [Schwabhauser] p. 89. (Contributed by Thierry Arnoux, 11-Dec-2019.)
|- P = ( Base ` G )   &    |- .- = ( dist ` G )   &    |- I = (Itv ` G )   &    |- ( ph -> G e. TarskiG )   &    |- ( ph -> GDimTarskiG≥ 2 )   &    |- M = ( (lInvG ` G ) ` D )   &    |- L = (LineG ` G )   &    |- ( ph -> D e. ran L )   &    |- ( ph -> A e. P )   &    |- ( ph -> B e. P )   &    |- ( ph -> ( M ` A ) = B )   =>    |- ( ph -> ( M ` B ) = A )
Theorem	lmilmi 23832	Line mirroring is an involution. Theorem 10.5 of [Schwabhauser] p. 89. (Contributed by Thierry Arnoux, 11-Dec-2019.)
|- P = ( Base ` G )   &    |- .- = ( dist ` G )   &    |- I = (Itv ` G )   &    |- ( ph -> G e. TarskiG )   &    |- ( ph -> GDimTarskiG≥ 2 )   &    |- M = ( (lInvG ` G ) ` D )   &    |- L = (LineG ` G )   &    |- ( ph -> D e. ran L )   &    |- ( ph -> A e. P )   =>    |- ( ph -> ( M ` ( M ` A ) ) = A )
Theorem	lmireu 23833*	Any point has a unique antecedent through line mirroring. Theorem 10.6 of [Schwabhauser] p. 89. (Contributed by Thierry Arnoux, 11-Dec-2019.)
|- P = ( Base ` G )   &    |- .- = ( dist ` G )   &    |- I = (Itv ` G )   &    |- ( ph -> G e. TarskiG )   &    |- ( ph -> GDimTarskiG≥ 2 )   &    |- M = ( (lInvG ` G ) ` D )   &    |- L = (LineG ` G )   &    |- ( ph -> D e. ran L )   &    |- ( ph -> A e. P )   =>    |- ( ph -> E! b e. P ( M ` b ) = A )
Theorem	lmieq 23834	Equality deduction for line mirroring. Theorem 10.7 of [Schwabhauser] p. 89. (Contributed by Thierry Arnoux, 11-Dec-2019.)
|- P = ( Base ` G )   &    |- .- = ( dist ` G )   &    |- I = (Itv ` G )   &    |- ( ph -> G e. TarskiG )   &    |- ( ph -> GDimTarskiG≥ 2 )   &    |- M = ( (lInvG ` G ) ` D )   &    |- L = (LineG ` G )   &    |- ( ph -> D e. ran L )   &    |- ( ph -> A e. P )   &    |- ( ph -> B e. P )   &    |- ( ph -> ( M ` A ) = ( M ` B ) )   =>    |- ( ph -> A = B )
Theorem	lmiinv 23835	The invariants of the line mirroring lie on the mirror line. Theorem 10.8 of [Schwabhauser] p. 89. (Contributed by Thierry Arnoux, 11-Dec-2019.)
|- P = ( Base ` G )   &    |- .- = ( dist ` G )   &    |- I = (Itv ` G )   &    |- ( ph -> G e. TarskiG )   &    |- ( ph -> GDimTarskiG≥ 2 )   &    |- M = ( (lInvG ` G ) ` D )   &    |- L = (LineG ` G )   &    |- ( ph -> D e. ran L )   &    |- ( ph -> A e. P )   =>    |- ( ph -> ( ( M ` A ) = A <-> A e. D ) )
Theorem	lmimid 23836	If we have a right angle, then the mirror point is the point inversion. (Contributed by Thierry Arnoux, 15-Dec-2019.)
|- P = ( Base ` G )   &    |- .- = ( dist ` G )   &    |- I = (Itv ` G )   &    |- ( ph -> G e. TarskiG )   &    |- ( ph -> GDimTarskiG≥ 2 )   &    |- M = ( (lInvG ` G ) ` D )   &    |- L = (LineG ` G )   &    |- ( ph -> D e. ran L )   &    |- ( ph -> A e. P )   &    |- S = ( (pInvG ` G ) ` B )   &    |- ( ph -> <" A B C "> e. (∟G ` G ) )   &    |- ( ph -> A e. D )   &    |- ( ph -> B e. D )   &    |- ( ph -> C e. P )   &    |- ( ph -> A =/= B )   =>    |- ( ph -> ( M ` C ) = ( S ` C ) )
Theorem	lmif1o 23837	The line mirroring function M is a bijection. Theorem 10.9 of [Schwabhauser] p. 89. (Contributed by Thierry Arnoux, 11-Dec-2019.)
|- P = ( Base ` G )   &    |- .- = ( dist ` G )   &    |- I = (Itv ` G )   &    |- ( ph -> G e. TarskiG )   &    |- ( ph -> GDimTarskiG≥ 2 )   &    |- M = ( (lInvG ` G ) ` D )   &    |- L = (LineG ` G )   &    |- ( ph -> D e. ran L )   =>    |- ( ph -> M : P -1-1-onto-> P )
Theorem	lmiisolem 23838	Lemma for lmiiso 23839 (Contributed by Thierry Arnoux, 14-Dec-2019.)
|- P = ( Base ` G )   &    |- .- = ( dist ` G )   &    |- I = (Itv ` G )   &    |- ( ph -> G e. TarskiG )   &    |- ( ph -> GDimTarskiG≥ 2 )   &    |- M = ( (lInvG ` G ) ` D )   &    |- L = (LineG ` G )   &    |- ( ph -> D e. ran L )   &    |- ( ph -> A e. P )   &    |- ( ph -> B e. P )   &    |- S = ( (pInvG ` G ) ` Z )   &    |- Z = ( ( A (midG ` G ) ( M ` A ) ) (midG ` G ) ( B (midG ` G ) ( M ` B ) ) )   =>    |- ( ph -> ( ( M ` A ) .- ( M ` B ) ) = ( A .- B ) )
Theorem	lmiiso 23839	The line mirroring function is an isometry, i.e. it is conserves congruence. Because it is also a bijection, it is also a motion. Theorem 10.10 of [Schwabhauser] p. 89. (Contributed by Thierry Arnoux, 11-Dec-2019.)
|- P = ( Base ` G )   &    |- .- = ( dist ` G )   &    |- I = (Itv ` G )   &    |- ( ph -> G e. TarskiG )   &    |- ( ph -> GDimTarskiG≥ 2 )   &    |- M = ( (lInvG ` G ) ` D )   &    |- L = (LineG ` G )   &    |- ( ph -> D e. ran L )   &    |- ( ph -> A e. P )   &    |- ( ph -> B e. P )   =>    |- ( ph -> ( ( M ` A ) .- ( M ` B ) ) = ( A .- B ) )
Theorem	lmimot 23840	Line mirroring is a motion of the geometric space. Theorem 10.11 of [Schwabhauser] p. 90. (Contributed by Thierry Arnoux, 15-Dec-2019.)
|- P = ( Base ` G )   &    |- .- = ( dist ` G )   &    |- I = (Itv ` G )   &    |- ( ph -> G e. TarskiG )   &    |- ( ph -> GDimTarskiG≥ 2 )   &    |- M = ( (lInvG ` G ) ` D )   &    |- L = (LineG ` G )   &    |- ( ph -> D e. ran L )   =>    |- ( ph -> M e. ( GIsmt G ) )
Theorem	hypcgrlem1 23841	Lemma for hypcgr 23843, case where triangles share a cathetus. (Contributed by Thierry Arnoux, 15-Dec-2019.)
|- P = ( Base ` G )   &    |- .- = ( dist ` G )   &    |- I = (Itv ` G )   &    |- ( ph -> G e. TarskiG )   &    |- ( ph -> GDimTarskiG≥ 2 )   &    |- ( 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 "> e. (∟G ` G ) )   &    |- ( ph -> <" D E F "> e. (∟G ` G ) )   &    |- ( ph -> ( A .- B ) = ( D .- E ) )   &    |- ( ph -> ( B .- C ) = ( E .- F ) )   &    |- ( ph -> B = E )   &    |- S = ( (lInvG ` G ) ` ( ( A (midG ` G ) D ) (LineG ` G ) B ) )   &    |- ( ph -> C = F )   =>    |- ( ph -> ( A .- C ) = ( D .- F ) )
Theorem	hypcgrlem2 23842	Lemma for hypcgr 23843, case where triangles share one vertex B. (Contributed by Thierry Arnoux, 16-Dec-2019.)
|- P = ( Base ` G )   &    |- .- = ( dist ` G )   &    |- I = (Itv ` G )   &    |- ( ph -> G e. TarskiG )   &    |- ( ph -> GDimTarskiG≥ 2 )   &    |- ( 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 "> e. (∟G ` G ) )   &    |- ( ph -> <" D E F "> e. (∟G ` G ) )   &    |- ( ph -> ( A .- B ) = ( D .- E ) )   &    |- ( ph -> ( B .- C ) = ( E .- F ) )   &    |- ( ph -> B = E )   &    |- S = ( (lInvG ` G ) ` ( ( C (midG ` G ) F ) (LineG ` G ) B ) )   =>    |- ( ph -> ( A .- C ) = ( D .- F ) )
Theorem	hypcgr 23843	If the catheti of two right-angled triangles are congruent, so is their hypothenuse. Theorem 10.12 of [Schwabhauser] p. 91. (Contributed by Thierry Arnoux, 16-Dec-2019.)
|- P = ( Base ` G )   &    |- .- = ( dist ` G )   &    |- I = (Itv ` G )   &    |- ( ph -> G e. TarskiG )   &    |- ( ph -> GDimTarskiG≥ 2 )   &    |- ( 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 "> e. (∟G ` G ) )   &    |- ( ph -> <" D E F "> e. (∟G ` G ) )   &    |- ( ph -> ( A .- B ) = ( D .- E ) )   &    |- ( ph -> ( B .- C ) = ( E .- F ) )   =>    |- ( ph -> ( A .- C ) = ( D .- F ) )
15.2.14  Congruence of angles
Syntax	ccgra 23844	Declare the constant for the congruence between angles relation.
class cgrA
Definition	df-cgra 23845*	Define the congruence relation bewteen angles. See definition 11.2 of [Schwabhauser] p. 95. As for triangles we use "words of points". (Contributed by Thierry Arnoux, 27-Nov-2019.)
|- cgrA = ( g e. _V |-> { <. a , b >. | ( ( a e. ( ( Base ` g ) ^m ( 0..^ 3 ) ) /\ b e. ( ( Base ` g ) ^m ( 0..^ 3 ) ) ) /\ ( ( b ` 0 ) =/= ( b ` 1 ) /\ ( b ` 1 ) =/= ( b ` 2 ) /\ E. x e. ( ( a ` 0 ) (LineG ` g ) ( a ` 1 ) ) E. y e. ( ( a ` 1 ) (LineG ` g ) ( a ` 2 ) ) <" x ( a ` 1 ) y "> (cgrG ` g ) b ) ) } )
15.2.15  Equilateral triangles
Syntax	ceqlg 23846	Declare the class of equilateral triangles.
class eqltrG
Definition	df-eqlg 23847*	Define the class of equilateral triangles. (Contributed by Thierry Arnoux, 27-Nov-2019.)
|- eqltrG = ( g e. _V |-> { x e. ( ( Base ` g ) ^m ( 0..^ 3 ) ) | x (cgrG ` g ) <" ( x ` 1 ) ( x ` 2 ) ( x ` 0 ) "> } )
15.3  Properties of geometries
15.3.1  Isomorphisms between geometries
Theorem	f1otrgds 23848*	Convenient lemma for f1otrg 23850 (Contributed by Thierry Arnoux, 19-Mar-2019.)
|- P = ( Base ` G )   &    |- D = ( dist ` G )   &    |- I = (Itv ` G )   &    |- B = ( Base ` H )   &    |- E = ( dist ` H )   &    |- J = (Itv ` H )   &    |- ( ph -> F : B -1-1-onto-> P )   &    |- ( ( ph /\ ( e e. B /\ f e. B ) ) -> ( e E f ) = ( ( F ` e ) D ( F ` f ) ) )   &    |- ( ( ph /\ ( e e. B /\ f e. B /\ g e. B ) ) -> ( g e. ( e J f ) <-> ( F ` g ) e. ( ( F ` e ) I ( F ` f ) ) ) )   &    |- ( ph -> X e. B )   &    |- ( ph -> Y e. B )   =>    |- ( ph -> ( X E Y ) = ( ( F ` X ) D ( F ` Y ) ) )
Theorem	f1otrgitv 23849*	Convenient lemma for f1otrg 23850 (Contributed by Thierry Arnoux, 19-Mar-2019.)
|- P = ( Base ` G )   &    |- D = ( dist ` G )   &    |- I = (Itv ` G )   &    |- B = ( Base ` H )   &    |- E = ( dist ` H )   &    |- J = (Itv ` H )   &    |- ( ph -> F : B -1-1-onto-> P )   &    |- ( ( ph /\ ( e e. B /\ f e. B ) ) -> ( e E f ) = ( ( F ` e ) D ( F ` f ) ) )   &    |- ( ( ph /\ ( e e. B /\ f e. B /\ g e. B ) ) -> ( g e. ( e J f ) <-> ( F ` g ) e. ( ( F ` e ) I ( F ` f ) ) ) )   &    |- ( ph -> X e. B )   &    |- ( ph -> Y e. B )   &    |- ( ph -> Z e. B )   =>    |- ( ph -> ( Z e. ( X J Y ) <-> ( F ` Z ) e. ( ( F ` X ) I ( F ` Y ) ) ) )
Theorem	f1otrg 23850*	A bijection between bases which conserves distances and intervals conserves also geometries. (Contributed by Thierry Arnoux, 23-Mar-2019.)
|- P = ( Base ` G )   &    |- D = ( dist ` G )   &    |- I = (Itv ` G )   &    |- B = ( Base ` H )   &    |- E = ( dist ` H )   &    |- J = (Itv ` H )   &    |- ( ph -> F : B -1-1-onto-> P )   &    |- ( ( ph /\ ( e e. B /\ f e. B ) ) -> ( e E f ) = ( ( F ` e ) D ( F ` f ) ) )   &    |- ( ( ph /\ ( e e. B /\ f e. B /\ g e. B ) ) -> ( g e. ( e J f ) <-> ( F ` g ) e. ( ( F ` e ) I ( F ` f ) ) ) )   &    |- ( ph -> H e. V )   &    |- ( ph -> G e. TarskiG )   &    |- ( ph -> (LineG ` H ) = ( x e. B , y e. ( B \ { x } ) |-> { z e. B | ( z e. ( x J y ) \/ x e. ( z J y ) \/ y e. ( x J z ) ) } ) )   =>    |- ( ph -> H e. TarskiG )
Theorem	f1otrge 23851*	A bijection between bases which conserves distances and intervals conserves also the property of being a Euclidean geometry. (Contributed by Thierry Arnoux, 23-Mar-2019.)
|- P = ( Base ` G )   &    |- D = ( dist ` G )   &    |- I = (Itv ` G )   &    |- B = ( Base ` H )   &    |- E = ( dist ` H )   &    |- J = (Itv ` H )   &    |- ( ph -> F : B -1-1-onto-> P )   &    |- ( ( ph /\ ( e e. B /\ f e. B ) ) -> ( e E f ) = ( ( F ` e ) D ( F ` f ) ) )   &    |- ( ( ph /\ ( e e. B /\ f e. B /\ g e. B ) ) -> ( g e. ( e J f ) <-> ( F ` g ) e. ( ( F ` e ) I ( F ` f ) ) ) )   &    |- ( ph -> H e. V )   &    |- ( ph -> G e. TarskiGE )   =>    |- ( ph -> H e. TarskiGE )
15.4  Geometry in Hilbert spaces
Syntax	cttg 23852	Function to convert an algebraic structure to a Tarski geometry.
class toTG
Definition	df-ttg 23853*	Define a function converting a complex Hilbert space to a Tarski Geometry. It does so by equipping the structure with a betweenness operation. Note that because the scalar product is applied over the interval ( 0 [,] 1 ), only spaces whose scalar field is a superset of that interval can be considered. (Contributed by Thierry Arnoux, 24-Mar-2019.)
|- toTG = ( w e. _V |-> [_ ( x e. ( Base ` w ) , y e. ( Base ` w ) |-> { z e. ( Base ` w ) | E. k e. ( 0 [,] 1 ) ( z ( -g ` w ) x ) = ( k ( .s ` w ) ( y ( -g ` w ) x ) ) } ) / i ]_ ( ( w sSet <. (Itv ` ndx ) , i >. ) sSet <. (LineG ` ndx ) , ( x e. ( Base ` w ) , y e. ( Base ` w ) |-> { z e. ( Base ` w ) | ( z e. ( x i y ) \/ x e. ( z i y ) \/ y e. ( x i z ) ) } ) >. ) )
Theorem	ttgval 23854*	Define a function to augment a complex Hilbert space with betweenness and a line definition. (Contributed by Thierry Arnoux, 25-Mar-2019.)
|- G = (toTG ` H )   &    |- B = ( Base ` H )   &    |- .- = ( -g ` H )   &    |- .x. = ( .s ` H )   &    |- I = (Itv ` G )   =>    |- ( H e. V -> ( G = ( ( H sSet <. (Itv ` ndx ) , ( x e. B , y e. B |-> { z e. B | E. k e. ( 0 [,] 1 ) ( z .- x ) = ( k .x. ( y .- x ) ) } ) >. ) sSet <. (LineG ` ndx ) , ( x e. B , y e. B |-> { z e. B | ( z e. ( x I y ) \/ x e. ( z I y ) \/ y e. ( x I z ) ) } ) >. ) /\ I = ( x e. B , y e. B |-> { z e. B | E. k e. ( 0 [,] 1 ) ( z .- x ) = ( k .x. ( y .- x ) ) } ) ) )
Theorem	ttglem 23855	Lemma for ttgbas 23856 and ttgvsca 23859. (Contributed by Thierry Arnoux, 15-Apr-2019.)
|- G = (toTG ` H )   &    |- E = Slot N   &    |- N e. NN   &    |- N < ; 1 6   =>    |- ( E ` H ) = ( E ` G )
Theorem	ttgbas 23856	The base set of a complex Hilbert space augmented with betweenness. (Contributed by Thierry Arnoux, 25-Mar-2019.)
|- G = (toTG ` H )   &    |- B = ( Base ` H )   =>    |- B = ( Base ` G )
Theorem	ttgplusg 23857	The addition operation of a complex Hilbert space augmented with betweenness. (Contributed by Thierry Arnoux, 25-Mar-2019.)
|- G = (toTG ` H )   &    |- .+ = ( +g ` H )   =>    |- .+ = ( +g ` G )
Theorem	ttgsub 23858	The subtraction operation of a complex Hilbert space augmented with betweenness. (Contributed by Thierry Arnoux, 25-Mar-2019.)
|- G = (toTG ` H )   &    |- .- = ( -g ` H )   =>    |- .- = ( -g ` G )
Theorem	ttgvsca 23859	The scalar product of a complex Hilbert space augmented with betweenness. (Contributed by Thierry Arnoux, 25-Mar-2019.)
|- G = (toTG ` H )   &    |- .x. = ( .s ` H )   =>    |- .x. = ( .s ` G )
Theorem	ttgds 23860	The metric of a complex Hilbert space augmented with betweenness. (Contributed by Thierry Arnoux, 25-Mar-2019.)
|- G = (toTG ` H )   &    |- D = ( dist ` H )   =>    |- D = ( dist ` G )
Theorem	ttgitvval 23861*	Betweenness for a complex Hilbert space augmented with betweenness. (Contributed by Thierry Arnoux, 25-Mar-2019.)
|- G = (toTG ` H )   &    |- I = (Itv ` G )   &    |- P = ( Base ` H )   &    |- .- = ( -g ` H )   &    |- .x. = ( .s ` H )   =>    |- ( ( H e. V /\ X e. P /\ Y e. P ) -> ( X I Y ) = { z e. P | E. k e. ( 0 [,] 1 ) ( z .- X ) = ( k .x. ( Y .- X ) ) } )
Theorem	ttgelitv 23862*	Betweenness for a complex Hilbert space augmented with betweenness. (Contributed by Thierry Arnoux, 25-Mar-2019.)
|- G = (toTG ` H )   &    |- I = (Itv ` G )   &    |- P = ( Base ` H )   &    |- .- = ( -g ` H )   &    |- .x. = ( .s ` H )   &    |- ( ph -> X e. P )   &    |- ( ph -> Y e. P )   &    |- ( ph -> H e. V )   &    |- ( ph -> Z e. P )   =>    |- ( ph -> ( Z e. ( X I Y ) <-> E. k e. ( 0 [,] 1 ) ( Z .- X ) = ( k .x. ( Y .- X ) ) ) )
Theorem	ttgbtwnid 23863	Any complex module equipped with the betweenness operation fulfills the identity of betweenness (Axiom A6). (Contributed by Thierry Arnoux, 26-Mar-2019.)
|- G = (toTG ` H )   &    |- I = (Itv ` G )   &    |- P = ( Base ` H )   &    |- .- = ( -g ` H )   &    |- .x. = ( .s ` H )   &    |- ( ph -> X e. P )   &    |- ( ph -> Y e. P )   &    |- R = ( Base ` (Scalar ` H ) )   &    |- ( ph -> ( 0 [,] 1 ) C_ R )   &    |- ( ph -> H e. CMod )   &    |- ( ph -> Y e. ( X I X ) )   =>    |- ( ph -> X = Y )
Theorem	ttgcontlem1 23864	Lemma for % ttgcont (Contributed by Thierry Arnoux, 24-May-2019.)
|- G = (toTG ` H )   &    |- I = (Itv ` G )   &    |- P = ( Base ` H )   &    |- .- = ( -g ` H )   &    |- .x. = ( .s ` H )   &    |- ( ph -> X e. P )   &    |- ( ph -> Y e. P )   &    |- R = ( Base ` (Scalar ` H ) )   &    |- ( ph -> ( 0 [,] 1 ) C_ R )   &    |- .+ = ( +g ` H )   &    |- ( ph -> H e. CVec )   &    |- ( ph -> A e. P )   &    |- ( ph -> N e. P )   &    |- ( ph -> M =/= 0 )   &    |- ( ph -> K =/= 0 )   &    |- ( ph -> K =/= 1 )   &    |- ( ph -> L =/= M )   &    |- ( ph -> L <_ ( M / K ) )   &    |- ( ph -> L e. ( 0 [,] 1 ) )   &    |- ( ph -> K e. ( 0 [,] 1 ) )   &    |- ( ph -> M e. ( 0 [,] L ) )   &    |- ( ph -> ( X .- A ) = ( K .x. ( Y .- A ) ) )   &    |- ( ph -> ( X .- A ) = ( M .x. ( N .- A ) ) )   &    |- ( ph -> B = ( A .+ ( L .x. ( N .- A ) ) ) )   =>    |- ( ph -> B e. ( X I Y ) )
Theorem	xmstrkgc 23865	Any metric space fulfills Tarski's geometry axioms of congruence. (Contributed by Thierry Arnoux, 13-Mar-2019.)
|- ( G e. *MetSp -> G e. TarskiGC )
15.4.1  Geometry in the complex plane
Theorem	cchhllem 23866*	Lemma for chlbas and chlvsca . (Contributed by Thierry Arnoux, 15-Apr-2019.)
|- C = ( ( (subringAlg ` ℂfld ) ` RR ) sSet <. ( .i ` ndx ) , ( x e. CC , y e. CC |-> ( x x. ( * ` y ) ) ) >. )   &    |- E = Slot N   &    |- N e. NN   &    |- ( N < 5 \/ 8 < N )   =>    |- ( E ` ℂfld ) = ( E ` C )
15.4.2  Geometry in Euclidean spaces
15.4.2.1  Definition of the Euclidean space
Syntax	cee 23867	Declare the syntax for the Euclidean space generator.
class EE
Syntax	cbtwn 23868	Declare the syntax for the Euclidean betweenness predicate.
class Btwn
Syntax	ccgr 23869	Declare the syntax for the Euclidean congruence predicate.
class Cgr
Definition	df-ee 23870	Define the Euclidean space generator. For details, see elee 23873. (Contributed by Scott Fenton, 3-Jun-2013.)
|- EE = ( n e. NN |-> ( RR ^m ( 1 ... n ) ) )
Definition	df-btwn 23871*	Define the Euclidean betweenness predicate. For details, see brbtwn 23878. (Contributed by Scott Fenton, 3-Jun-2013.)
|- Btwn = `' { <. <. x , z >. , y >. | E. n e. NN ( ( x e. ( EE ` n ) /\ z e. ( EE ` n ) /\ y e. ( EE ` n ) ) /\ E. t e. ( 0 [,] 1 ) A. i e. ( 1 ... n ) ( y ` i ) = ( ( ( 1 - t ) x. ( x ` i ) ) + ( t x. ( z ` i ) ) ) ) }
Definition	df-cgr 23872*	Define the Euclidean congruence predicate. For details, see brcgr 23879. (Contributed by Scott Fenton, 3-Jun-2013.)
|- Cgr = { <. x , y >. | E. n e. NN ( ( x e. ( ( EE ` n ) X. ( EE ` n ) ) /\ y e. ( ( EE ` n ) X. ( EE ` n ) ) ) /\ sum_ i e. ( 1 ... n ) ( ( ( ( 1st ` x ) ` i ) - ( ( 2nd ` x ) ` i ) ) ^ 2 ) = sum_ i e. ( 1 ... n ) ( ( ( ( 1st ` y ) ` i ) - ( ( 2nd ` y ) ` i ) ) ^ 2 ) ) }
Theorem	elee 23873	Membership in a Euclidean space. We define Euclidean space here using Cartesian coordinates over N space. We later abstract away from this using Tarski's geometry axioms, so this exact definition is unimportant. (Contributed by Scott Fenton, 3-Jun-2013.)
|- ( N e. NN -> ( A e. ( EE ` N ) <-> A : ( 1 ... N ) --> RR ) )
Theorem	mptelee 23874*	A condition for a mapping to be an element of a Euclidean space. (Contributed by Scott Fenton, 7-Jun-2013.)
|- ( N e. NN -> ( ( k e. ( 1 ... N ) |-> ( A F B ) ) e. ( EE ` N ) <-> A. k e. ( 1 ... N ) ( A F B ) e. RR ) )
Theorem	eleenn 23875	If A is in ( EE ` N ), then N is a natural. (Contributed by Scott Fenton, 1-Jul-2013.)
|- ( A e. ( EE ` N ) -> N e. NN )
Theorem	eleei 23876	The forward direction of elee 23873. (Contributed by Scott Fenton, 1-Jul-2013.)
|- ( A e. ( EE ` N ) -> A : ( 1 ... N ) --> RR )
Theorem	eedimeq 23877	A point belongs to at most one Euclidean space. (Contributed by Scott Fenton, 1-Jul-2013.)
|- ( ( A e. ( EE ` N ) /\ A e. ( EE ` M ) ) -> N = M )
Theorem	brbtwn 23878*	The binary relationship form of the betweenness predicate. The statement A Btwn <. B , C >. should be informally read as " A lies on a line segment between B and C. This exact definition is abstracted away by Tarski's geometry axioms later on. (Contributed by Scott Fenton, 3-Jun-2013.)
|- ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) -> ( A Btwn <. B , C >. <-> E. t e. ( 0 [,] 1 ) A. i e. ( 1 ... N ) ( A ` i ) = ( ( ( 1 - t ) x. ( B ` i ) ) + ( t x. ( C ` i ) ) ) ) )
Theorem	brcgr 23879*	The binary relationship form of the congruence predicate. The statement <. A , B >.Cgr <. C , D >. should be read informally as "the N dimensional point A is as far from B as C is from D, or "the line segment A B is congruent to the line segment C D. This particular definition is encapsulated by Tarski's axioms later on. (Contributed by Scott Fenton, 3-Jun-2013.)
|- ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) -> ( <. A , B >.Cgr <. C , D >. <-> sum_ i e. ( 1 ... N ) ( ( ( A ` i ) - ( B ` i ) ) ^ 2 ) = sum_ i e. ( 1 ... N ) ( ( ( C ` i ) - ( D ` i ) ) ^ 2 ) ) )
Theorem	fveere 23880	The function value of a point is a real. (Contributed by Scott Fenton, 10-Jun-2013.)
|- ( ( A e. ( EE ` N ) /\ I e. ( 1 ... N ) ) -> ( A ` I ) e. RR )
Theorem	fveecn 23881	The function value of a point is a complex. (Contributed by Scott Fenton, 10-Jun-2013.)
|- ( ( A e. ( EE ` N ) /\ I e. ( 1 ... N ) ) -> ( A ` I ) e. CC )
Theorem	eqeefv 23882*	Two points are equal iff they agree in all dimensions. (Contributed by Scott Fenton, 10-Jun-2013.)
|- ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) -> ( A = B <-> A. i e. ( 1 ... N ) ( A ` i ) = ( B ` i ) ) )
Theorem	eqeelen 23883*	Two points are equal iff the square of the distance between them is zero. (Contributed by Scott Fenton, 10-Jun-2013.) (Revised by Mario Carneiro, 22-May-2014.)
|- ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) -> ( A = B <-> sum_ i e. ( 1 ... N ) ( ( ( A ` i ) - ( B ` i ) ) ^ 2 ) = 0 ) )
Theorem	brbtwn2 23884*	Alternate characterization of betweenness, with no existential quantifiers. (Contributed by Scott Fenton, 24-Jun-2013.)
|- ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) -> ( A Btwn <. B , C >. <-> ( A. i e. ( 1 ... N ) ( ( ( B ` i ) - ( A ` i ) ) x. ( ( C ` i ) - ( A ` i ) ) ) <_ 0 /\ A. i e. ( 1 ... N ) A. j e. ( 1 ... N ) ( ( ( B ` i ) - ( A ` i ) ) x. ( ( C ` j ) - ( A ` j ) ) ) = ( ( ( B ` j ) - ( A ` j ) ) x. ( ( C ` i ) - ( A ` i ) ) ) ) ) )
Theorem	colinearalglem1 23885	Lemma for colinearalg 23889. Expand out a multiplication. (Contributed by Scott Fenton, 24-Jun-2013.)
|- ( ( ( A e. CC /\ B e. CC /\ C e. CC ) /\ ( D e. CC /\ E e. CC /\ F e. CC ) ) -> ( ( ( B - A ) x. ( F - D ) ) = ( ( E - D ) x. ( C - A ) ) <-> ( ( B x. F ) - ( ( A x. F ) + ( B x. D ) ) ) = ( ( C x. E ) - ( ( A x. E ) + ( C x. D ) ) ) ) )
Theorem	colinearalglem2 23886*	Lemma for colinearalg 23889. Translate between two forms of the colinearity condition. (Contributed by Scott Fenton, 24-Jun-2013.)
|- ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) -> ( A. i e. ( 1 ... N ) A. j e. ( 1 ... N ) ( ( ( B ` i ) - ( A ` i ) ) x. ( ( C ` j ) - ( A ` j ) ) ) = ( ( ( B ` j ) - ( A ` j ) ) x. ( ( C ` i ) - ( A ` i ) ) ) <-> A. i e. ( 1 ... N ) A. j e. ( 1 ... N ) ( ( ( C ` i ) - ( B ` i ) ) x. ( ( A ` j ) - ( B ` j ) ) ) = ( ( ( C ` j ) - ( B ` j ) ) x. ( ( A ` i ) - ( B ` i ) ) ) ) )
Theorem	colinearalglem3 23887*	Lemma for colinearalg 23889. Translate between two forms of the colinearity condition. (Contributed by Scott Fenton, 24-Jun-2013.)
|- ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) -> ( A. i e. ( 1 ... N ) A. j e. ( 1 ... N ) ( ( ( B ` i ) - ( A ` i ) ) x. ( ( C ` j ) - ( A ` j ) ) ) = ( ( ( B ` j ) - ( A ` j ) ) x. ( ( C ` i ) - ( A ` i ) ) ) <-> A. i e. ( 1 ... N ) A. j e. ( 1 ... N ) ( ( ( A ` i ) - ( C ` i ) ) x. ( ( B ` j ) - ( C ` j ) ) ) = ( ( ( A ` j ) - ( C ` j ) ) x. ( ( B ` i ) - ( C ` i ) ) ) ) )
Theorem	colinearalglem4 23888*	Lemma for colinearalg 23889. Prove a disjunction that will be needed in the final proof. (Contributed by Scott Fenton, 27-Jun-2013.)
|- ( ( ( A e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ K e. RR ) -> ( A. i e. ( 1 ... N ) ( ( ( ( K x. ( ( C ` i ) - ( A ` i ) ) ) + ( A ` i ) ) - ( A ` i ) ) x. ( ( C ` i ) - ( A ` i ) ) ) <_ 0 \/ A. i e. ( 1 ... N ) ( ( ( C ` i ) - ( ( K x. ( ( C ` i ) - ( A ` i ) ) ) + ( A ` i ) ) ) x. ( ( A ` i ) - ( ( K x. ( ( C ` i ) - ( A ` i ) ) ) + ( A ` i ) ) ) ) <_ 0 \/ A. i e. ( 1 ... N ) ( ( ( A ` i ) - ( C ` i ) ) x. ( ( ( K x. ( ( C ` i ) - ( A ` i ) ) ) + ( A ` i ) ) - ( C ` i ) ) ) <_ 0 ) )
Theorem	colinearalg 23889*	An algebraic characterization of colinearity. Note the similarity to brbtwn2 23884. (Contributed by Scott Fenton, 24-Jun-2013.)
|- ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) -> ( ( A Btwn <. B , C >. \/ B Btwn <. C , A >. \/ C Btwn <. A , B >. ) <-> A. i e. ( 1 ... N ) A. j e. ( 1 ... N ) ( ( ( B ` i ) - ( A ` i ) ) x. ( ( C ` j ) - ( A ` j ) ) ) = ( ( ( B ` j ) - ( A ` j ) ) x. ( ( C ` i ) - ( A ` i ) ) ) ) )
Theorem	eleesub 23890*	Membership of a subtraction mapping in a Euclidean space. (Contributed by Scott Fenton, 17-Jul-2013.)
|- C = ( i e. ( 1 ... N ) |-> ( ( A ` i ) - ( B ` i ) ) )   =>    |- ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) -> C e. ( EE ` N ) )
Theorem	eleesubd 23891*	Membership of a subtraction mapping in a Euclidean space. Deduction form of eleesub 23890. (Contributed by Scott Fenton, 17-Jul-2013.)
|- ( ph -> C = ( i e. ( 1 ... N ) |-> ( ( A ` i ) - ( B ` i ) ) ) )   =>    |- ( ( ph /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) -> C e. ( EE ` N ) )
15.4.2.2  Tarski's axioms for geometry for the Euclidean space
Theorem	axdimuniq 23892	The unique dimension axiom. If a point is in N dimensional space and in M dimensional space, then N = M. This axiom is not traditionally presented with Tarski's axioms, but we require it here as we are considering spaces in arbitrary dimensions. (Contributed by Scott Fenton, 24-Sep-2013.)
|- ( ( ( N e. NN /\ A e. ( EE ` N ) ) /\ ( M e. NN /\ A e. ( EE ` M ) ) ) -> N = M )
Theorem	axcgrrflx 23893	A is as far from B as B is from A. Axiom A1 of [Schwabhauser] p. 10. (Contributed by Scott Fenton, 3-Jun-2013.)
|- ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) -> <. A , B >.Cgr <. B , A >. )
Theorem	axcgrtr 23894	Congruence is transitive. Axiom A2 of [Schwabhauser] p. 10. (Contributed by Scott Fenton, 3-Jun-2013.)
|- ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) -> ( ( <. A , B >.Cgr <. C , D >. /\ <. A , B >.Cgr <. E , F >. ) -> <. C , D >.Cgr <. E , F >. ) )
Theorem	axcgrid 23895	If there is no distance between A and B, then A = B. Axiom A3 of [Schwabhauser] p. 10. (Contributed by Scott Fenton, 3-Jun-2013.)
|- ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) -> ( <. A , B >.Cgr <. C , C >. -> A = B ) )
Theorem	axsegconlem1 23896*	Lemma for axsegcon 23906. Handle the degenerate case. (Contributed by Scott Fenton, 7-Jun-2013.)
|- ( ( A = B /\ ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) ) -> E. x e. ( EE ` N ) E. t e. ( 0 [,] 1 ) ( A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - t ) x. ( A ` i ) ) + ( t x. ( x ` i ) ) ) /\ sum_ i e. ( 1 ... N ) ( ( ( B ` i ) - ( x ` i ) ) ^ 2 ) = sum_ i e. ( 1 ... N ) ( ( ( C ` i ) - ( D ` i ) ) ^ 2 ) ) )
Theorem	axsegconlem2 23897*	Lemma for axsegcon 23906. Show that the square of the distance between two points is a real number. (Contributed by Scott Fenton, 17-Sep-2013.)
|- S = sum_ p e. ( 1 ... N ) ( ( ( A ` p ) - ( B ` p ) ) ^ 2 )   =>    |- ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) -> S e. RR )
Theorem	axsegconlem3 23898*	Lemma for axsegcon 23906. Show that the square of the distance between two points is nonnegative. (Contributed by Scott Fenton, 17-Sep-2013.)
|- S = sum_ p e. ( 1 ... N ) ( ( ( A ` p ) - ( B ` p ) ) ^ 2 )   =>    |- ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) -> 0 <_ S )
Theorem	axsegconlem4 23899*	Lemma for axsegcon 23906. Show that the distance between two points is a real number. (Contributed by Scott Fenton, 17-Sep-2013.)
|- S = sum_ p e. ( 1 ... N ) ( ( ( A ` p ) - ( B ` p ) ) ^ 2 )   =>    |- ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) -> ( sqr ` S ) e. RR )
Theorem	axsegconlem5 23900*	Lemma for axsegcon 23906. Show that the distance between two points is nonnegative. (Contributed by Scott Fenton, 17-Sep-2013.)
|- S = sum_ p e. ( 1 ... N ) ( ( ( A ` p ) - ( B ` p ) ) ^ 2 )   =>    |- ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) -> 0 <_ ( sqr ` S ) )