P. 257 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 25601-25700   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	ragflat3 25601	Right angle and colinearity. Theorem 8.9 of [Schwabhauser] p. 58. (Contributed by Thierry Arnoux, 4-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 -> ( C e. ( A L B ) \/ A = B ) )   =>    |- ( ph -> ( A = B \/ C = B ) )
Theorem	ragcgr 25602	Right angle and colinearity. Theorem 8.10 of [Schwabhauser] p. 58. (Contributed by Thierry Arnoux, 4-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 )   &    |- .~ = (cgrG ` G )   &    |- ( ph -> D e. P )   &    |- ( ph -> E e. P )   &    |- ( ph -> F e. P )   &    |- ( ph -> <" A B C "> e. (∟G ` G ) )   &    |- ( ph -> <" A B C "> .~ <" D E F "> )   =>    |- ( ph -> <" D E F "> e. (∟G ` G ) )
Theorem	motrag 25603	Right angles are preserved by motions. (Contributed by Thierry Arnoux, 16-Dec-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 -> F e. ( GIsmt G ) )   &    |- ( ph -> <" A B C "> e. (∟G ` G ) )   =>    |- ( ph -> <" ( F ` A ) ( F ` B ) ( F ` C ) "> e. (∟G ` G ) )
Theorem	ragncol 25604	Right angle implies non-colinearity. A consequence of theorem 8.9 of [Schwabhauser] p. 58. (Contributed by Thierry Arnoux, 1-Dec-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 )   &    |- ( ph -> C =/= B )   =>    |- ( ph -> -. ( C e. ( A L B ) \/ A = B ) )
Theorem	perpln1 25605	Derive a line from perpendicularity. (Contributed by Thierry Arnoux, 27-Nov-2019.)
|- L = (LineG ` G )   &    |- ( ph -> G e. TarskiG )   &    |- ( ph -> A (⟂G ` G ) B )   =>    |- ( ph -> A e. ran L )
Theorem	perpln2 25606	Derive a line from perpendicularity. (Contributed by Thierry Arnoux, 27-Nov-2019.)
|- L = (LineG ` G )   &    |- ( ph -> G e. TarskiG )   &    |- ( ph -> A (⟂G ` G ) B )   =>    |- ( ph -> B e. ran L )
Theorem	isperp 25607*	Property for 2 lines A, B to be perpendicular. Item (ii) of definition 8.11 of [Schwabhauser] p. 59. (Contributed by Thierry Arnoux, 16-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 -> ( A (⟂G ` G ) B <-> E. x e. ( A i^i B ) A. u e. A A. v e. B <" u x v "> e. (∟G ` G ) ) )
Theorem	perpcom 25608	The "perpendicular" relation commutes. Theorem 8.12 of [Schwabhauser] p. 59. (Contributed by Thierry Arnoux, 16-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 -> A (⟂G ` G ) B )   =>    |- ( ph -> B (⟂G ` G ) A )
Theorem	perpneq 25609	Two perpendicular lines are different. Theorem 8.14 of [Schwabhauser] p. 59. (Contributed by Thierry Arnoux, 18-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 -> A (⟂G ` G ) B )   =>    |- ( ph -> A =/= B )
Theorem	isperp2 25610*	Property for 2 lines A, B, intersecting at a point X to be perpendicular. Item (i) of definition 8.13 of [Schwabhauser] p. 59. (Contributed by Thierry Arnoux, 16-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 -> ( A (⟂G ` G ) B <-> A. u e. A A. v e. B <" u X v "> e. (∟G ` G ) ) )
Theorem	isperp2d 25611	One direction of isperp2 25610. (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 25612	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 25613*	Lemma for foot 25614: 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 25614*	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	footne 25615	Uniqueness of the foot point. (Contributed by Thierry Arnoux, 28-Feb-2020.)
|- P = ( Base ` G )   &    |- .- = ( dist ` G )   &    |- I = (Itv ` G )   &    |- L = (LineG ` G )   &    |- ( ph -> G e. TarskiG )   &    |- ( ph -> A e. ran L )   &    |- ( ph -> X e. A )   &    |- ( ph -> Y e. P )   &    |- ( ph -> ( X L Y ) (⟂G ` G ) A )   =>    |- ( ph -> -. Y e. A )
Theorem	footeq 25616	Uniqueness of the foot point. (Contributed by Thierry Arnoux, 1-Mar-2020.)
|- P = ( Base ` G )   &    |- .- = ( dist ` G )   &    |- I = (Itv ` G )   &    |- L = (LineG ` G )   &    |- ( ph -> G e. TarskiG )   &    |- ( ph -> A e. ran L )   &    |- ( ph -> X e. A )   &    |- ( ph -> Y e. A )   &    |- ( ph -> Z e. P )   &    |- ( ph -> ( X L Z ) (⟂G ` G ) A )   &    |- ( ph -> ( Y L Z ) (⟂G ` G ) A )   =>    |- ( ph -> X = Y )
Theorem	hlperpnel 25617	A point on a half-line which is perpendicular to a line cannot be on that line. (Contributed by Thierry Arnoux, 1-Mar-2020.)
|- P = ( Base ` G )   &    |- .- = ( dist ` G )   &    |- I = (Itv ` G )   &    |- L = (LineG ` G )   &    |- ( ph -> G e. TarskiG )   &    |- ( ph -> A e. ran L )   &    |- K = (hlG ` G )   &    |- ( ph -> U e. A )   &    |- ( ph -> V e. P )   &    |- ( ph -> W e. P )   &    |- ( ph -> A (⟂G ` G ) ( U L V ) )   &    |- ( ph -> V ( K ` U ) W )   =>    |- ( ph -> -. W e. A )
Theorem	perprag 25618	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 25619	Deduce a right angle from perpendicular lines. (Contributed by Thierry Arnoux, 12-Dec-2019.) (New usage is discouraged.) (Proof modification is discouraged.)
|- 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 25620	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 25621	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 25622	Lemma for colperp 25621. 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 25623	Lemma for colperpex 25625. 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 25624*	Lemma for colperpex 25625. 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 25625*	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	mideulem2 25626	Lemma for opphllem 25627, which is itself used for mideu 25630. (Contributed by Thierry Arnoux, 19-Feb-2020.)
|- 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 -> R e. P )   &    |- ( ph -> R e. ( B I Q ) )   &    |- ( ph -> ( A .- O ) = ( B .- R ) )   &    |- ( ph -> X e. P )   &    |- ( ph -> X e. ( T I B ) )   &    |- ( ph -> X e. ( R I O ) )   &    |- ( ph -> Z e. P )   &    |- ( ph -> X e. ( ( ( S ` A ) ` O ) I Z ) )   &    |- ( ph -> ( X .- Z ) = ( X .- R ) )   &    |- ( ph -> M e. P )   &    |- ( ph -> R = ( ( S ` M ) ` Z ) )   =>    |- ( ph -> B = M )
Theorem	opphllem 25627*	Lemma 8.24 of [Schwabhauser] p. 66. This is used later for mideulem 25628 and later for opphl 25646. (Contributed by Thierry Arnoux, 21-Dec-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 -> R e. P )   &    |- ( ph -> R e. ( B I Q ) )   &    |- ( ph -> ( A .- O ) = ( B .- R ) )   =>    |- ( ph -> E. x e. P ( B = ( ( S ` x ) ` A ) /\ O = ( ( S ` x ) ` R ) ) )
Theorem	mideulem 25628*	Lemma for mideu 25630. 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	midex 25629*	Existence of the midpoint, part 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 ) )
Theorem	mideu 25630*	Existence and uniqueness of the midpoint, Theorem 8.22 of [Schwabhauser] p. 64. (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.14  Half-planes
Theorem	islnopp 25631*	The property for two points A and B to lie on the opposite sides of a set D Definition 9.1 of [Schwabhauser] p. 67. (Contributed by Thierry Arnoux, 19-Dec-2019.)
|- P = ( Base ` G )   &    |- .- = ( dist ` G )   &    |- I = (Itv ` G )   &    |- O = { <. a , b >. | ( ( a e. ( P \ D ) /\ b e. ( P \ D ) ) /\ E. t e. D t e. ( a I b ) ) }   &    |- ( ph -> A e. P )   &    |- ( ph -> B e. P )   =>    |- ( ph -> ( A O B <-> ( ( -. A e. D /\ -. B e. D ) /\ E. t e. D t e. ( A I B ) ) ) )
Theorem	islnoppd 25632*	Deduce that A and B lie on opposite sides of line L. (Contributed by Thierry Arnoux, 16-Aug-2020.)
|- P = ( Base ` G )   &    |- .- = ( dist ` G )   &    |- I = (Itv ` G )   &    |- O = { <. a , b >. | ( ( a e. ( P \ D ) /\ b e. ( P \ D ) ) /\ E. t e. D t e. ( a I b ) ) }   &    |- ( ph -> A e. P )   &    |- ( ph -> B e. P )   &    |- ( ph -> C e. D )   &    |- ( ph -> -. A e. D )   &    |- ( ph -> -. B e. D )   &    |- ( ph -> C e. ( A I B ) )   =>    |- ( ph -> A O B )
Theorem	oppne1 25633*	Points lying on opposite sides of a line cannot be on the line. (Contributed by Thierry Arnoux, 3-Mar-2020.)
|- P = ( Base ` G )   &    |- .- = ( dist ` G )   &    |- I = (Itv ` G )   &    |- O = { <. a , b >. | ( ( a e. ( P \ D ) /\ b e. ( P \ D ) ) /\ E. t e. D t e. ( a I b ) ) }   &    |- L = (LineG ` G )   &    |- ( ph -> D e. ran L )   &    |- ( ph -> G e. TarskiG )   &    |- ( ph -> A e. P )   &    |- ( ph -> B e. P )   &    |- ( ph -> A O B )   =>    |- ( ph -> -. A e. D )
Theorem	oppne2 25634*	Points lying on opposite sides of a line cannot be on the line. (Contributed by Thierry Arnoux, 3-Mar-2020.)
|- P = ( Base ` G )   &    |- .- = ( dist ` G )   &    |- I = (Itv ` G )   &    |- O = { <. a , b >. | ( ( a e. ( P \ D ) /\ b e. ( P \ D ) ) /\ E. t e. D t e. ( a I b ) ) }   &    |- L = (LineG ` G )   &    |- ( ph -> D e. ran L )   &    |- ( ph -> G e. TarskiG )   &    |- ( ph -> A e. P )   &    |- ( ph -> B e. P )   &    |- ( ph -> A O B )   =>    |- ( ph -> -. B e. D )
Theorem	oppne3 25635*	Points lying on opposite sides of a line cannot be equal. (Contributed by Thierry Arnoux, 3-Aug-2020.)
|- P = ( Base ` G )   &    |- .- = ( dist ` G )   &    |- I = (Itv ` G )   &    |- O = { <. a , b >. | ( ( a e. ( P \ D ) /\ b e. ( P \ D ) ) /\ E. t e. D t e. ( a I b ) ) }   &    |- L = (LineG ` G )   &    |- ( ph -> D e. ran L )   &    |- ( ph -> G e. TarskiG )   &    |- ( ph -> A e. P )   &    |- ( ph -> B e. P )   &    |- ( ph -> A O B )   =>    |- ( ph -> A =/= B )
Theorem	oppcom 25636*	Commutativity rule for "opposite" Theorem 9.2 of [Schwabhauser] p. 67. (Contributed by Thierry Arnoux, 19-Dec-2019.)
|- P = ( Base ` G )   &    |- .- = ( dist ` G )   &    |- I = (Itv ` G )   &    |- O = { <. a , b >. | ( ( a e. ( P \ D ) /\ b e. ( P \ D ) ) /\ E. t e. D t e. ( a I b ) ) }   &    |- L = (LineG ` G )   &    |- ( ph -> D e. ran L )   &    |- ( ph -> G e. TarskiG )   &    |- ( ph -> A e. P )   &    |- ( ph -> B e. P )   &    |- ( ph -> A O B )   =>    |- ( ph -> B O A )
Theorem	opptgdim2 25637*	If two points opposite to a line exist, dimension must be 2 or more. (Contributed by Thierry Arnoux, 3-Mar-2020.)
|- P = ( Base ` G )   &    |- .- = ( dist ` G )   &    |- I = (Itv ` G )   &    |- O = { <. a , b >. | ( ( a e. ( P \ D ) /\ b e. ( P \ D ) ) /\ E. t e. D t e. ( a I b ) ) }   &    |- L = (LineG ` G )   &    |- ( ph -> D e. ran L )   &    |- ( ph -> G e. TarskiG )   &    |- ( ph -> A e. P )   &    |- ( ph -> B e. P )   &    |- ( ph -> A O B )   =>    |- ( ph -> GDimTarskiG≥ 2 )
Theorem	oppnid 25638*	The "opposite to a line" relation is irreflexive. (Contributed by Thierry Arnoux, 4-Mar-2020.)
|- P = ( Base ` G )   &    |- .- = ( dist ` G )   &    |- I = (Itv ` G )   &    |- O = { <. a , b >. | ( ( a e. ( P \ D ) /\ b e. ( P \ D ) ) /\ E. t e. D t e. ( a I b ) ) }   &    |- L = (LineG ` G )   &    |- ( ph -> D e. ran L )   &    |- ( ph -> G e. TarskiG )   &    |- ( ph -> A e. P )   =>    |- ( ph -> -. A O A )
Theorem	opphllem1 25639*	Lemma for opphl 25646. (Contributed by Thierry Arnoux, 20-Dec-2019.)
|- P = ( Base ` G )   &    |- .- = ( dist ` G )   &    |- I = (Itv ` G )   &    |- O = { <. a , b >. | ( ( a e. ( P \ D ) /\ b e. ( P \ D ) ) /\ E. t e. D t e. ( a I b ) ) }   &    |- L = (LineG ` G )   &    |- ( ph -> D e. ran L )   &    |- ( ph -> G e. TarskiG )   &    |- S = ( (pInvG ` G ) ` M )   &    |- ( ph -> A e. P )   &    |- ( ph -> B e. P )   &    |- ( ph -> C e. P )   &    |- ( ph -> R e. D )   &    |- ( ph -> A O C )   &    |- ( ph -> M e. D )   &    |- ( ph -> A = ( S ` C ) )   &    |- ( ph -> A =/= R )   &    |- ( ph -> B =/= R )   &    |- ( ph -> B e. ( R I A ) )   =>    |- ( ph -> B O C )
Theorem	opphllem2 25640*	Lemma for opphl 25646. Lemma 9.3 of [Schwabhauser] p. 68. (Contributed by Thierry Arnoux, 21-Dec-2019.)
|- P = ( Base ` G )   &    |- .- = ( dist ` G )   &    |- I = (Itv ` G )   &    |- O = { <. a , b >. | ( ( a e. ( P \ D ) /\ b e. ( P \ D ) ) /\ E. t e. D t e. ( a I b ) ) }   &    |- L = (LineG ` G )   &    |- ( ph -> D e. ran L )   &    |- ( ph -> G e. TarskiG )   &    |- S = ( (pInvG ` G ) ` M )   &    |- ( ph -> A e. P )   &    |- ( ph -> B e. P )   &    |- ( ph -> C e. P )   &    |- ( ph -> R e. D )   &    |- ( ph -> A O C )   &    |- ( ph -> M e. D )   &    |- ( ph -> A = ( S ` C ) )   &    |- ( ph -> A =/= R )   &    |- ( ph -> B =/= R )   &    |- ( ph -> ( A e. ( R I B ) \/ B e. ( R I A ) ) )   =>    |- ( ph -> B O C )
Theorem	opphllem3 25641*	Lemma for opphl 25646: We assume opphllem3.l "without loss of generality". (Contributed by Thierry Arnoux, 21-Feb-2020.)
|- P = ( Base ` G )   &    |- .- = ( dist ` G )   &    |- I = (Itv ` G )   &    |- O = { <. a , b >. | ( ( a e. ( P \ D ) /\ b e. ( P \ D ) ) /\ E. t e. D t e. ( a I b ) ) }   &    |- L = (LineG ` G )   &    |- ( ph -> D e. ran L )   &    |- ( ph -> G e. TarskiG )   &    |- K = (hlG ` G )   &    |- N = ( (pInvG ` G ) ` M )   &    |- ( ph -> A e. P )   &    |- ( ph -> C e. P )   &    |- ( ph -> R e. D )   &    |- ( ph -> S e. D )   &    |- ( ph -> M e. P )   &    |- ( ph -> A O C )   &    |- ( ph -> D (⟂G ` G ) ( A L R ) )   &    |- ( ph -> D (⟂G ` G ) ( C L S ) )   &    |- ( ph -> R =/= S )   &    |- ( ph -> ( S .- C ) (≤G ` G ) ( R .- A ) )   &    |- ( ph -> U e. P )   &    |- ( ph -> ( N ` R ) = S )   =>    |- ( ph -> ( U ( K ` R ) A <-> ( N ` U ) ( K ` S ) C ) )
Theorem	opphllem4 25642*	Lemma for opphl 25646. (Contributed by Thierry Arnoux, 22-Feb-2020.)
|- P = ( Base ` G )   &    |- .- = ( dist ` G )   &    |- I = (Itv ` G )   &    |- O = { <. a , b >. | ( ( a e. ( P \ D ) /\ b e. ( P \ D ) ) /\ E. t e. D t e. ( a I b ) ) }   &    |- L = (LineG ` G )   &    |- ( ph -> D e. ran L )   &    |- ( ph -> G e. TarskiG )   &    |- K = (hlG ` G )   &    |- N = ( (pInvG ` G ) ` M )   &    |- ( ph -> A e. P )   &    |- ( ph -> C e. P )   &    |- ( ph -> R e. D )   &    |- ( ph -> S e. D )   &    |- ( ph -> M e. P )   &    |- ( ph -> A O C )   &    |- ( ph -> D (⟂G ` G ) ( A L R ) )   &    |- ( ph -> D (⟂G ` G ) ( C L S ) )   &    |- ( ph -> R =/= S )   &    |- ( ph -> ( S .- C ) (≤G ` G ) ( R .- A ) )   &    |- ( ph -> U e. P )   &    |- ( ph -> ( N ` R ) = S )   &    |- ( ph -> V e. P )   &    |- ( ph -> U ( K ` R ) A )   &    |- ( ph -> V ( K ` S ) C )   =>    |- ( ph -> U O V )
Theorem	opphllem5 25643*	Second part of Lemma 9.4 of [Schwabhauser] p. 68. (Contributed by Thierry Arnoux, 2-Mar-2020.)
|- P = ( Base ` G )   &    |- .- = ( dist ` G )   &    |- I = (Itv ` G )   &    |- O = { <. a , b >. | ( ( a e. ( P \ D ) /\ b e. ( P \ D ) ) /\ E. t e. D t e. ( a I b ) ) }   &    |- L = (LineG ` G )   &    |- ( ph -> D e. ran L )   &    |- ( ph -> G e. TarskiG )   &    |- K = (hlG ` G )   &    |- N = ( (pInvG ` G ) ` M )   &    |- ( ph -> A e. P )   &    |- ( ph -> C e. P )   &    |- ( ph -> R e. D )   &    |- ( ph -> S e. D )   &    |- ( ph -> M e. P )   &    |- ( ph -> A O C )   &    |- ( ph -> D (⟂G ` G ) ( A L R ) )   &    |- ( ph -> D (⟂G ` G ) ( C L S ) )   &    |- ( ph -> U e. P )   &    |- ( ph -> V e. P )   &    |- ( ph -> U ( K ` R ) A )   &    |- ( ph -> V ( K ` S ) C )   =>    |- ( ph -> U O V )
Theorem	opphllem6 25644*	First part of Lemma 9.4 of [Schwabhauser] p. 68. (Contributed by Thierry Arnoux, 3-Mar-2020.)
|- P = ( Base ` G )   &    |- .- = ( dist ` G )   &    |- I = (Itv ` G )   &    |- O = { <. a , b >. | ( ( a e. ( P \ D ) /\ b e. ( P \ D ) ) /\ E. t e. D t e. ( a I b ) ) }   &    |- L = (LineG ` G )   &    |- ( ph -> D e. ran L )   &    |- ( ph -> G e. TarskiG )   &    |- K = (hlG ` G )   &    |- N = ( (pInvG ` G ) ` M )   &    |- ( ph -> A e. P )   &    |- ( ph -> C e. P )   &    |- ( ph -> R e. D )   &    |- ( ph -> S e. D )   &    |- ( ph -> M e. P )   &    |- ( ph -> A O C )   &    |- ( ph -> D (⟂G ` G ) ( A L R ) )   &    |- ( ph -> D (⟂G ` G ) ( C L S ) )   &    |- ( ph -> U e. P )   &    |- ( ph -> ( N ` R ) = S )   =>    |- ( ph -> ( U ( K ` R ) A <-> ( N ` U ) ( K ` S ) C ) )
Theorem	oppperpex 25645*	Restating colperpex 25625 using the "opposite side of a line" relation. (Contributed by Thierry Arnoux, 2-Aug-2020.)
|- P = ( Base ` G )   &    |- .- = ( dist ` G )   &    |- I = (Itv ` G )   &    |- O = { <. a , b >. | ( ( a e. ( P \ D ) /\ b e. ( P \ D ) ) /\ E. t e. D t e. ( a I b ) ) }   &    |- L = (LineG ` G )   &    |- ( ph -> D e. ran L )   &    |- ( ph -> G e. TarskiG )   &    |- K = (hlG ` G )   &    |- ( ph -> A e. D )   &    |- ( ph -> C e. P )   &    |- ( ph -> -. C e. D )   &    |- ( ph -> GDimTarskiG≥ 2 )   =>    |- ( ph -> E. p e. P ( ( A L p ) (⟂G ` G ) D /\ C O p ) )
Theorem	opphl 25646*	If two points A and C lie on the opposite side of a line D then any point of the half line ( R A) also lies opposite to C. Theorem 9.5 of [Schwabhauser] p. 69. (Contributed by Thierry Arnoux, 3-Mar-2019.)
|- P = ( Base ` G )   &    |- .- = ( dist ` G )   &    |- I = (Itv ` G )   &    |- O = { <. a , b >. | ( ( a e. ( P \ D ) /\ b e. ( P \ D ) ) /\ E. t e. D t e. ( a I b ) ) }   &    |- L = (LineG ` G )   &    |- ( ph -> D e. ran L )   &    |- ( ph -> G e. TarskiG )   &    |- K = (hlG ` G )   &    |- ( ph -> A e. P )   &    |- ( ph -> B e. P )   &    |- ( ph -> C e. P )   &    |- ( ph -> A O C )   &    |- ( ph -> R e. D )   &    |- ( ph -> A ( K ` R ) B )   =>    |- ( ph -> B O C )
Theorem	outpasch 25647*	Axiom of Pasch, outer form. This was proven by Gupta from other axioms and is therefore presented as Theorem 9.6 in [Schwabhauser] p. 70. (Contributed by Thierry Arnoux, 16-Aug-2020.)
|- 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 -> R e. P )   &    |- ( ph -> Q e. P )   &    |- ( ph -> C e. ( A I R ) )   &    |- ( ph -> Q e. ( B I C ) )   =>    |- ( ph -> E. x e. P ( x e. ( A I B ) /\ Q e. ( R I x ) ) )
Theorem	hlpasch 25648*	An application of the axiom of Pasch for half-lines. (Contributed by Thierry Arnoux, 15-Sep-2020.)
|- P = ( Base ` G )   &    |- I = (Itv ` G )   &    |- K = (hlG ` G )   &    |- ( ph -> G e. TarskiG )   &    |- ( ph -> A e. P )   &    |- ( ph -> B e. P )   &    |- ( ph -> C e. P )   &    |- ( ph -> X e. P )   &    |- ( ph -> D e. P )   &    |- ( ph -> A =/= B )   &    |- ( ph -> C ( K ` B ) D )   &    |- ( ph -> A e. ( X I C ) )   =>    |- ( ph -> E. e e. P ( A ( K ` B ) e /\ e e. ( X I D ) ) )
Syntax	chpg 25649	"Belong to the same open half-plane" relation for points in a geometry.
class hpG
Definition	df-hpg 25650*	Define the open half plane relation for a geometry G. Definition 9.7 of [Schwabhauser] p. 71. See hpgbr 25652 to find the same formulation. (Contributed by Thierry Arnoux, 4-Mar-2020.)
|- hpG = ( g e. _V |-> ( d e. ran (LineG ` g ) |-> { <. a , b >. | [. ( Base ` g ) / p ]. [. (Itv ` g ) / i ]. E. c e. p ( ( ( a e. ( p \ d ) /\ c e. ( p \ d ) ) /\ E. t e. d t e. ( a i c ) ) /\ ( ( b e. ( p \ d ) /\ c e. ( p \ d ) ) /\ E. t e. d t e. ( b i c ) ) ) } ) )
Theorem	ishpg 25651*	Value of the half-plane relation for a given line D. (Contributed by Thierry Arnoux, 4-Mar-2020.)
|- P = ( Base ` G )   &    |- I = (Itv ` G )   &    |- L = (LineG ` G )   &    |- O = { <. a , b >. | ( ( a e. ( P \ D ) /\ b e. ( P \ D ) ) /\ E. t e. D t e. ( a I b ) ) }   &    |- ( ph -> G e. TarskiG )   &    |- ( ph -> D e. ran L )   =>    |- ( ph -> ( (hpG ` G ) ` D ) = { <. a , b >. | E. c e. P ( a O c /\ b O c ) } )
Theorem	hpgbr 25652*	Half-planes : property for points A and B to belong to the same open half plane delimited by line D. Definition 9.7 of [Schwabhauser] p. 71. (Contributed by Thierry Arnoux, 4-Mar-2020.)
|- P = ( Base ` G )   &    |- I = (Itv ` G )   &    |- L = (LineG ` G )   &    |- O = { <. a , b >. | ( ( a e. ( P \ D ) /\ b e. ( P \ D ) ) /\ E. t e. D t e. ( a I b ) ) }   &    |- ( ph -> G e. TarskiG )   &    |- ( ph -> D e. ran L )   &    |- ( ph -> A e. P )   &    |- ( ph -> B e. P )   =>    |- ( ph -> ( A ( (hpG ` G ) ` D ) B <-> E. c e. P ( A O c /\ B O c ) ) )
Theorem	hpgne1 25653*	Points on the open half plane cannot lie on its border. (Contributed by Thierry Arnoux, 4-Mar-2020.)
|- P = ( Base ` G )   &    |- I = (Itv ` G )   &    |- L = (LineG ` G )   &    |- O = { <. a , b >. | ( ( a e. ( P \ D ) /\ b e. ( P \ D ) ) /\ E. t e. D t e. ( a I b ) ) }   &    |- ( ph -> G e. TarskiG )   &    |- ( ph -> D e. ran L )   &    |- ( ph -> A e. P )   &    |- ( ph -> B e. P )   &    |- ( ph -> A ( (hpG ` G ) ` D ) B )   =>    |- ( ph -> -. A e. D )
Theorem	hpgne2 25654*	Points on the open half plane cannot lie on its border. (Contributed by Thierry Arnoux, 4-Mar-2020.)
|- P = ( Base ` G )   &    |- I = (Itv ` G )   &    |- L = (LineG ` G )   &    |- O = { <. a , b >. | ( ( a e. ( P \ D ) /\ b e. ( P \ D ) ) /\ E. t e. D t e. ( a I b ) ) }   &    |- ( ph -> G e. TarskiG )   &    |- ( ph -> D e. ran L )   &    |- ( ph -> A e. P )   &    |- ( ph -> B e. P )   &    |- ( ph -> A ( (hpG ` G ) ` D ) B )   =>    |- ( ph -> -. B e. D )
Theorem	lnopp2hpgb 25655*	Theorem 9.8 of [Schwabhauser] p. 71. (Contributed by Thierry Arnoux, 4-Mar-2020.)
|- P = ( Base ` G )   &    |- I = (Itv ` G )   &    |- L = (LineG ` G )   &    |- O = { <. a , b >. | ( ( a e. ( P \ D ) /\ b e. ( P \ D ) ) /\ E. t e. D t e. ( a I b ) ) }   &    |- ( ph -> G e. TarskiG )   &    |- ( ph -> D e. ran L )   &    |- ( ph -> A e. P )   &    |- ( ph -> B e. P )   &    |- ( ph -> C e. P )   &    |- ( ph -> A O C )   =>    |- ( ph -> ( B O C <-> A ( (hpG ` G ) ` D ) B ) )
Theorem	lnoppnhpg 25656*	If two points lie on the opposite side of a line D, they are not on the same half-plane. Theorem 9.9 of [Schwabhauser] p. 72. (Contributed by Thierry Arnoux, 4-Mar-2020.)
|- P = ( Base ` G )   &    |- I = (Itv ` G )   &    |- L = (LineG ` G )   &    |- O = { <. a , b >. | ( ( a e. ( P \ D ) /\ b e. ( P \ D ) ) /\ E. t e. D t e. ( a I b ) ) }   &    |- ( ph -> G e. TarskiG )   &    |- ( ph -> D e. ran L )   &    |- ( ph -> A e. P )   &    |- ( ph -> B e. P )   &    |- ( ph -> A O B )   =>    |- ( ph -> -. A ( (hpG ` G ) ` D ) B )
Theorem	hpgerlem 25657*	Lemma for the proof that the half-plane relation is an equivalence relation. Lemma 9.10 of [Schwabhauser] p. 72. (Contributed by Thierry Arnoux, 4-Mar-2020.)
|- P = ( Base ` G )   &    |- I = (Itv ` G )   &    |- L = (LineG ` G )   &    |- ( ph -> G e. TarskiG )   &    |- ( ph -> D e. ran L )   &    |- ( ph -> A e. P )   &    |- O = { <. a , b >. | ( ( a e. ( P \ D ) /\ b e. ( P \ D ) ) /\ E. t e. D t e. ( a I b ) ) }   &    |- ( ph -> -. A e. D )   =>    |- ( ph -> E. c e. P A O c )
Theorem	hpgid 25658*	The half-plane relation is reflexive. Theorem 9.11 of [Schwabhauser] p. 72. (Contributed by Thierry Arnoux, 4-Mar-2020.)
|- P = ( Base ` G )   &    |- I = (Itv ` G )   &    |- L = (LineG ` G )   &    |- ( ph -> G e. TarskiG )   &    |- ( ph -> D e. ran L )   &    |- ( ph -> A e. P )   &    |- O = { <. a , b >. | ( ( a e. ( P \ D ) /\ b e. ( P \ D ) ) /\ E. t e. D t e. ( a I b ) ) }   &    |- ( ph -> -. A e. D )   =>    |- ( ph -> A ( (hpG ` G ) ` D ) A )
Theorem	hpgcom 25659*	The half-plane relation commutes. Theorem 9.12 of [Schwabhauser] p. 72. (Contributed by Thierry Arnoux, 4-Mar-2020.)
|- P = ( Base ` G )   &    |- I = (Itv ` G )   &    |- L = (LineG ` G )   &    |- ( ph -> G e. TarskiG )   &    |- ( ph -> D e. ran L )   &    |- ( ph -> A e. P )   &    |- O = { <. a , b >. | ( ( a e. ( P \ D ) /\ b e. ( P \ D ) ) /\ E. t e. D t e. ( a I b ) ) }   &    |- ( ph -> B e. P )   &    |- ( ph -> A ( (hpG ` G ) ` D ) B )   =>    |- ( ph -> B ( (hpG ` G ) ` D ) A )
Theorem	hpgtr 25660*	The half-plane relation is transitive. Theorem 9.13 of [Schwabhauser] p. 72. (Contributed by Thierry Arnoux, 4-Mar-2020.)
|- P = ( Base ` G )   &    |- I = (Itv ` G )   &    |- L = (LineG ` G )   &    |- ( ph -> G e. TarskiG )   &    |- ( ph -> D e. ran L )   &    |- ( ph -> A e. P )   &    |- O = { <. a , b >. | ( ( a e. ( P \ D ) /\ b e. ( P \ D ) ) /\ E. t e. D t e. ( a I b ) ) }   &    |- ( ph -> B e. P )   &    |- ( ph -> A ( (hpG ` G ) ` D ) B )   &    |- ( ph -> C e. P )   &    |- ( ph -> B ( (hpG ` G ) ` D ) C )   =>    |- ( ph -> A ( (hpG ` G ) ` D ) C )
Theorem	colopp 25661*	Opposite sides of a line for colinear points. Theorem 9.18 of [Schwabhauser] p. 73. (Contributed by Thierry Arnoux, 3-Aug-2020.)
|- P = ( Base ` G )   &    |- I = (Itv ` G )   &    |- L = (LineG ` G )   &    |- ( ph -> G e. TarskiG )   &    |- ( ph -> D e. ran L )   &    |- ( ph -> A e. P )   &    |- O = { <. a , b >. | ( ( a e. ( P \ D ) /\ b e. ( P \ D ) ) /\ E. t e. D t e. ( a I b ) ) }   &    |- ( ph -> B e. P )   &    |- ( ph -> C e. D )   &    |- ( ph -> ( C e. ( A L B ) \/ A = B ) )   =>    |- ( ph -> ( A O B <-> ( C e. ( A I B ) /\ -. A e. D /\ -. B e. D ) ) )
Theorem	colhp 25662*	Half-plane relation for colinear points. Theorem 9.19 of [Schwabhauser] p. 73. (Contributed by Thierry Arnoux, 3-Aug-2020.)
|- P = ( Base ` G )   &    |- I = (Itv ` G )   &    |- L = (LineG ` G )   &    |- ( ph -> G e. TarskiG )   &    |- ( ph -> D e. ran L )   &    |- ( ph -> A e. P )   &    |- O = { <. a , b >. | ( ( a e. ( P \ D ) /\ b e. ( P \ D ) ) /\ E. t e. D t e. ( a I b ) ) }   &    |- ( ph -> B e. P )   &    |- ( ph -> C e. D )   &    |- ( ph -> ( C e. ( A L B ) \/ A = B ) )   &    |- K = (hlG ` G )   =>    |- ( ph -> ( A ( (hpG ` G ) ` D ) B <-> ( A ( K ` C ) B /\ -. A e. D ) ) )
Theorem	hphl 25663*	If two points are on the same half-line with endpoint on a line, they are on the same half-plane defined by this line. (Contributed by Thierry Arnoux, 9-Aug-2020.)
|- P = ( Base ` G )   &    |- I = (Itv ` G )   &    |- L = (LineG ` G )   &    |- ( ph -> G e. TarskiG )   &    |- ( ph -> D e. ran L )   &    |- ( ph -> A e. P )   &    |- O = { <. a , b >. | ( ( a e. ( P \ D ) /\ b e. ( P \ D ) ) /\ E. t e. D t e. ( a I b ) ) }   &    |- K = (hlG ` G )   &    |- ( ph -> A e. D )   &    |- ( ph -> B e. P )   &    |- ( ph -> C e. P )   &    |- ( ph -> -. B e. D )   &    |- ( ph -> B ( K ` A ) C )   =>    |- ( ph -> B ( (hpG ` G ) ` D ) C )
15.2.15  Midpoints and Line Mirroring
Syntax	cmid 25664	Declare the constant for the midpoint operation.
class midG
Syntax	clmi 25665	Declare the constant for the line mirroring function.
class lInvG
Definition	df-mid 25666*	Define the midpoint operation. Definition 10.1 of [Schwabhauser] p. 88. See ismidb 25670, midbtwn 25671, and midcgr 25672. (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 25667*	Define the line mirroring function. Definition 10.3 of [Schwabhauser] p. 89. See islmib 25679. (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 25668	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 25669	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 25670	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 25671	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 25672	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 25673	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 25674	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 25675	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 25676*	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 25677	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 25678	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 25679	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 25680	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 25681	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 25682*	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 25683	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 25684	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	lmicinv 25685	The mirroring line is an invariant. (Contributed by Thierry Arnoux, 8-Aug-2020.)
|- 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 -> A e. D )   =>    |- ( ph -> ( M ` A ) = A )
Theorem	lmimid 25686	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 25687	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 25688	Lemma for lmiiso 25689. (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 25689	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 25690	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 25691	Lemma for hypcgr 25693, 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 25692	Lemma for hypcgr 25693, 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 25693	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 ) )
Theorem	lmiopp 25694*	Line mirroring produces points on the opposite side of the mirroring line. Theorem 10.14 of [Schwabhauser] p. 92. (Contributed by Thierry Arnoux, 2-Aug-2020.)
|- P = ( Base ` G )   &    |- .- = ( dist ` G )   &    |- I = (Itv ` G )   &    |- L = (LineG ` G )   &    |- ( ph -> G e. TarskiG )   &    |- ( ph -> GDimTarskiG≥ 2 )   &    |- ( ph -> D e. ran L )   &    |- O = { <. a , b >. | ( ( a e. ( P \ D ) /\ b e. ( P \ D ) ) /\ E. t e. D t e. ( a I b ) ) }   &    |- M = ( (lInvG ` G ) ` D )   &    |- ( ph -> A e. P )   &    |- ( ph -> -. A e. D )   =>    |- ( ph -> A O ( M ` A ) )
Theorem	lnperpex 25695*	Existence of a perpendicular to a line L at a given point A. Theorem 10.15 of [Schwabhauser] p. 92. (Contributed by Thierry Arnoux, 2-Aug-2020.)
|- P = ( Base ` G )   &    |- .- = ( dist ` G )   &    |- I = (Itv ` G )   &    |- L = (LineG ` G )   &    |- ( ph -> G e. TarskiG )   &    |- ( ph -> GDimTarskiG≥ 2 )   &    |- ( ph -> D e. ran L )   &    |- O = { <. a , b >. | ( ( a e. ( P \ D ) /\ b e. ( P \ D ) ) /\ E. t e. D t e. ( a I b ) ) }   &    |- ( ph -> A e. D )   &    |- ( ph -> Q e. P )   &    |- ( ph -> -. Q e. D )   =>    |- ( ph -> E. p e. P ( D (⟂G ` G ) ( p L A ) /\ p ( (hpG ` G ) ` D ) Q ) )
Theorem	trgcopy 25696*	Triangle construction: a copy of a given triangle can always be constructed in such a way that one side is lying on a half-line, and the third vertex is on a given half-plane: existence part. First part of Theorem 10.16 of [Schwabhauser] p. 92. (Contributed by Thierry Arnoux, 4-Aug-2020.)
|- P = ( Base ` G )   &    |- .- = ( dist ` G )   &    |- I = (Itv ` G )   &    |- L = (LineG ` G )   &    |- K = (hlG ` 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 e. ( B L C ) \/ B = C ) )   &    |- ( ph -> -. ( D e. ( E L F ) \/ E = F ) )   &    |- ( ph -> ( A .- B ) = ( D .- E ) )   =>    |- ( ph -> E. f e. P ( <" A B C "> (cgrG ` G ) <" D E f "> /\ f ( (hpG ` G ) ` ( D L E ) ) F ) )
Theorem	trgcopyeulem 25697*	Lemma for trgcopyeu 25698. (Contributed by Thierry Arnoux, 8-Aug-2020.)
|- P = ( Base ` G )   &    |- .- = ( dist ` G )   &    |- I = (Itv ` G )   &    |- L = (LineG ` G )   &    |- K = (hlG ` 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 e. ( B L C ) \/ B = C ) )   &    |- ( ph -> -. ( D e. ( E L F ) \/ E = F ) )   &    |- ( ph -> ( A .- B ) = ( D .- E ) )   &    |- O = { <. a , b >. | ( ( a e. ( P \ ( D L E ) ) /\ b e. ( P \ ( D L E ) ) ) /\ E. t e. ( D L E ) t e. ( a I b ) ) }   &    |- ( ph -> X e. P )   &    |- ( ph -> Y e. P )   &    |- ( ph -> <" A B C "> (cgrG ` G ) <" D E X "> )   &    |- ( ph -> <" A B C "> (cgrG ` G ) <" D E Y "> )   &    |- ( ph -> X ( (hpG ` G ) ` ( D L E ) ) F )   &    |- ( ph -> Y ( (hpG ` G ) ` ( D L E ) ) F )   =>    |- ( ph -> X = Y )
Theorem	trgcopyeu 25698*	Triangle construction: a copy of a given triangle can always be constructed in such a way that one side is lying on a half-line, and the third vertex is on a given half-plane: uniqueness part. Second part of Theorem 10.16 of [Schwabhauser] p. 92. (Contributed by Thierry Arnoux, 8-Aug-2020.)
|- P = ( Base ` G )   &    |- .- = ( dist ` G )   &    |- I = (Itv ` G )   &    |- L = (LineG ` G )   &    |- K = (hlG ` 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 e. ( B L C ) \/ B = C ) )   &    |- ( ph -> -. ( D e. ( E L F ) \/ E = F ) )   &    |- ( ph -> ( A .- B ) = ( D .- E ) )   =>    |- ( ph -> E! f e. P ( <" A B C "> (cgrG ` G ) <" D E f "> /\ f ( (hpG ` G ) ` ( D L E ) ) F ) )
15.2.16  Congruence of angles
Syntax	ccgra 25699	Declare the constant for the congruence between angles relation.
class cgrA
Definition	df-cgra 25700*	Define the congruence relation bewteen angles. As for triangles we use "words of points". See iscgra 25701 for a more human readable version. (Contributed by Thierry Arnoux, 30-Jul-2020.)
|- cgrA = ( g e. _V |-> { <. a , b >. | [. ( Base ` g ) / p ]. [. (hlG ` g ) / k ]. ( ( a e. ( p ^m ( 0..^ 3 ) ) /\ b e. ( p ^m ( 0..^ 3 ) ) ) /\ E. x e. p E. y e. p ( a (cgrG ` g ) <" x ( b ` 1 ) y "> /\ x ( k ` ( b ` 1 ) ) ( b ` 0 ) /\ y ( k ` ( b ` 1 ) ) ( b ` 2 ) ) ) } )