P. 258 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 25701-25800   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	iscgra 25701*	Property for two angles ABC and DEF to be congruent. This is a modified version of the definition 11.3 of [Schwabhauser] p. 95. where the number of constructed points has been reduced to two. We chose this version rather than the textbook version because it is shorter and therefore simpler to work with. Theorem dfcgra2 25721 shows that those definitions are indeed equivalent. (Contributed by Thierry Arnoux, 31-Jul-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 -> D e. P )   &    |- ( ph -> E e. P )   &    |- ( ph -> F e. P )   =>    |- ( ph -> ( <" A B C "> (cgrA ` G ) <" D E F "> <-> E. x e. P E. y e. P ( <" A B C "> (cgrG ` G ) <" x E y "> /\ x ( K ` E ) D /\ y ( K ` E ) F ) ) )
Theorem	iscgra1 25702*	A special version of iscgra 25701 where one distance is known to be equal. In this case, angle congruence can be written with only one quantifier. (Contributed by Thierry Arnoux, 9-Aug-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 -> D e. P )   &    |- ( ph -> E e. P )   &    |- ( ph -> F e. P )   &    |- .- = ( dist ` G )   &    |- ( ph -> A =/= B )   &    |- ( ph -> ( A .- B ) = ( D .- E ) )   =>    |- ( ph -> ( <" A B C "> (cgrA ` G ) <" D E F "> <-> E. x e. P ( <" A B C "> (cgrG ` G ) <" D E x "> /\ x ( K ` E ) F ) ) )
Theorem	iscgrad 25703	Sufficient conditions for angle congruence, deduction version. (Contributed by Thierry Arnoux, 1-Aug-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 -> D e. P )   &    |- ( ph -> E e. P )   &    |- ( ph -> F e. P )   &    |- ( ph -> X e. P )   &    |- ( ph -> Y e. P )   &    |- ( ph -> <" A B C "> (cgrG ` G ) <" X E Y "> )   &    |- ( ph -> X ( K ` E ) D )   &    |- ( ph -> Y ( K ` E ) F )   =>    |- ( ph -> <" A B C "> (cgrA ` G ) <" D E F "> )
Theorem	cgrane1 25704	Angles imply inequality. (Contributed by Thierry Arnoux, 1-Aug-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 -> D e. P )   &    |- ( ph -> E e. P )   &    |- ( ph -> F e. P )   &    |- ( ph -> <" A B C "> (cgrA ` G ) <" D E F "> )   =>    |- ( ph -> A =/= B )
Theorem	cgrane2 25705	Angles imply inequality. (Contributed by Thierry Arnoux, 1-Aug-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 -> D e. P )   &    |- ( ph -> E e. P )   &    |- ( ph -> F e. P )   &    |- ( ph -> <" A B C "> (cgrA ` G ) <" D E F "> )   =>    |- ( ph -> B =/= C )
Theorem	cgrane3 25706	Angles imply inequality. (Contributed by Thierry Arnoux, 1-Aug-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 -> D e. P )   &    |- ( ph -> E e. P )   &    |- ( ph -> F e. P )   &    |- ( ph -> <" A B C "> (cgrA ` G ) <" D E F "> )   =>    |- ( ph -> E =/= D )
Theorem	cgrane4 25707	Angles imply inequality. (Contributed by Thierry Arnoux, 1-Aug-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 -> D e. P )   &    |- ( ph -> E e. P )   &    |- ( ph -> F e. P )   &    |- ( ph -> <" A B C "> (cgrA ` G ) <" D E F "> )   =>    |- ( ph -> E =/= F )
Theorem	cgrahl1 25708	Angle congruence is independent of the choice of points on the rays. Proposition 11.10 of [Schwabhauser] p. 95. (Contributed by Thierry Arnoux, 1-Aug-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 -> D e. P )   &    |- ( ph -> E e. P )   &    |- ( ph -> F e. P )   &    |- ( ph -> <" A B C "> (cgrA ` G ) <" D E F "> )   &    |- ( ph -> X e. P )   &    |- ( ph -> X ( K ` E ) D )   =>    |- ( ph -> <" A B C "> (cgrA ` G ) <" X E F "> )
Theorem	cgrahl2 25709	Angle congruence is independent of the choice of points on the rays. Proposition 11.10 of [Schwabhauser] p. 95. (Contributed by Thierry Arnoux, 1-Aug-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 -> D e. P )   &    |- ( ph -> E e. P )   &    |- ( ph -> F e. P )   &    |- ( ph -> <" A B C "> (cgrA ` G ) <" D E F "> )   &    |- ( ph -> X e. P )   &    |- ( ph -> X ( K ` E ) F )   =>    |- ( ph -> <" A B C "> (cgrA ` G ) <" D E X "> )
Theorem	cgracgr 25710	First direction of proposition 11.4 of [Schwabhauser] p. 95. Again, this is "half" of the proposition, i.e. only two additional points are used, while Schwabhauser has four. (Contributed by Thierry Arnoux, 31-Jul-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 -> D e. P )   &    |- ( ph -> E e. P )   &    |- ( ph -> F e. P )   &    |- ( ph -> <" A B C "> (cgrA ` G ) <" D E F "> )   &    |- ( ph -> X e. P )   &    |- .- = ( dist ` G )   &    |- ( ph -> Y e. P )   &    |- ( ph -> X ( K ` B ) A )   &    |- ( ph -> Y ( K ` B ) C )   &    |- ( ph -> ( B .- X ) = ( E .- D ) )   &    |- ( ph -> ( B .- Y ) = ( E .- F ) )   =>    |- ( ph -> ( X .- Y ) = ( D .- F ) )
Theorem	cgraid 25711	Angle congruence is reflexive. Theorem 11.6 of [Schwabhauser] p. 96. (Contributed by Thierry Arnoux, 31-Jul-2020.)
|- P = ( Base ` G )   &    |- I = (Itv ` G )   &    |- ( ph -> G e. TarskiG )   &    |- K = (hlG ` G )   &    |- ( ph -> A e. P )   &    |- ( ph -> B e. P )   &    |- ( ph -> C e. P )   &    |- ( ph -> A =/= B )   &    |- ( ph -> B =/= C )   =>    |- ( ph -> <" A B C "> (cgrA ` G ) <" A B C "> )
Theorem	cgraswap 25712	Swap rays in a congruence relation. Theorem 11.9 of [Schwabhauser] p. 96. (Contributed by Thierry Arnoux, 5-Mar-2020.)
|- P = ( Base ` G )   &    |- I = (Itv ` G )   &    |- ( ph -> G e. TarskiG )   &    |- K = (hlG ` G )   &    |- ( ph -> A e. P )   &    |- ( ph -> B e. P )   &    |- ( ph -> C e. P )   &    |- ( ph -> A =/= B )   &    |- ( ph -> B =/= C )   =>    |- ( ph -> <" A B C "> (cgrA ` G ) <" C B A "> )
Theorem	cgrcgra 25713	Triangle congruence implies angle congruence. (Contributed by Thierry Arnoux, 2-Aug-2020.)
|- P = ( Base ` G )   &    |- I = (Itv ` G )   &    |- ( ph -> G e. TarskiG )   &    |- K = (hlG ` G )   &    |- ( 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 )   &    |- ( ph -> B =/= C )   &    |- ( ph -> <" A B C "> (cgrG ` G ) <" D E F "> )   =>    |- ( ph -> <" A B C "> (cgrA ` G ) <" D E F "> )
Theorem	cgracom 25714	Angle congruence commutes. Theorem 11.7 of [Schwabhauser] p. 97. (Contributed by Thierry Arnoux, 5-Mar-2020.)
|- P = ( Base ` G )   &    |- I = (Itv ` G )   &    |- ( ph -> G e. TarskiG )   &    |- K = (hlG ` G )   &    |- ( 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 "> (cgrA ` G ) <" D E F "> )   =>    |- ( ph -> <" D E F "> (cgrA ` G ) <" A B C "> )
Theorem	cgratr 25715	Angle congruence is transitive. Theorem 11.8 of [Schwabhauser] p. 97. (Contributed by Thierry Arnoux, 5-Mar-2020.)
|- P = ( Base ` G )   &    |- I = (Itv ` G )   &    |- ( ph -> G e. TarskiG )   &    |- K = (hlG ` G )   &    |- ( 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 "> (cgrA ` G ) <" D E F "> )   &    |- ( ph -> H e. P )   &    |- ( ph -> U e. P )   &    |- ( ph -> J e. P )   &    |- ( ph -> <" D E F "> (cgrA ` G ) <" H U J "> )   =>    |- ( ph -> <" A B C "> (cgrA ` G ) <" H U J "> )
Theorem	cgraswaplr 25716	Swap both side of angle congruence. (Contributed by Thierry Arnoux, 5-Oct-2020.)
|- P = ( Base ` G )   &    |- I = (Itv ` G )   &    |- .- = ( dist ` G )   &    |- ( ph -> G e. TarskiG )   &    |- ( ph -> A e. P )   &    |- ( ph -> B e. P )   &    |- ( ph -> C e. P )   &    |- ( ph -> D e. P )   &    |- ( ph -> E e. P )   &    |- ( ph -> F e. P )   &    |- ( ph -> <" A B C "> (cgrA ` G ) <" D E F "> )   =>    |- ( ph -> <" C B A "> (cgrA ` G ) <" F E D "> )
Theorem	cgrabtwn 25717	Angle congruence preserves flat angles. Part of Theorem 11.21 of [Schwabhauser] p. 97. (Contributed by Thierry Arnoux, 9-Aug-2020.)
|- P = ( Base ` G )   &    |- I = (Itv ` G )   &    |- .- = ( dist ` G )   &    |- ( ph -> G e. TarskiG )   &    |- ( ph -> A e. P )   &    |- ( ph -> B e. P )   &    |- ( ph -> C e. P )   &    |- ( ph -> D e. P )   &    |- ( ph -> E e. P )   &    |- ( ph -> F e. P )   &    |- ( ph -> <" A B C "> (cgrA ` G ) <" D E F "> )   &    |- ( ph -> B e. ( A I C ) )   =>    |- ( ph -> E e. ( D I F ) )
Theorem	cgrahl 25718	Angle congruence preserves null angles. Part of Theorem 11.21 of [Schwabhauser] p. 97. (Contributed by Thierry Arnoux, 9-Aug-2020.)
|- P = ( Base ` G )   &    |- I = (Itv ` G )   &    |- .- = ( dist ` G )   &    |- ( ph -> G e. TarskiG )   &    |- ( ph -> A e. P )   &    |- ( ph -> B e. P )   &    |- ( ph -> C e. P )   &    |- ( ph -> D e. P )   &    |- ( ph -> E e. P )   &    |- ( ph -> F e. P )   &    |- ( ph -> <" A B C "> (cgrA ` G ) <" D E F "> )   &    |- K = (hlG ` G )   &    |- ( ph -> A ( K ` B ) C )   =>    |- ( ph -> D ( K ` E ) F )
Theorem	cgracol 25719	Angle congruence preserves colinearity. (Contributed by Thierry Arnoux, 9-Aug-2020.)
|- P = ( Base ` G )   &    |- I = (Itv ` G )   &    |- .- = ( dist ` G )   &    |- ( ph -> G e. TarskiG )   &    |- ( ph -> A e. P )   &    |- ( ph -> B e. P )   &    |- ( ph -> C e. P )   &    |- ( ph -> D e. P )   &    |- ( ph -> E e. P )   &    |- ( ph -> F e. P )   &    |- ( ph -> <" A B C "> (cgrA ` G ) <" D E F "> )   &    |- L = (LineG ` G )   &    |- ( ph -> ( C e. ( A L B ) \/ A = B ) )   =>    |- ( ph -> ( F e. ( D L E ) \/ D = E ) )
Theorem	cgrancol 25720	Angle congruence preserves non-colinearity. (Contributed by Thierry Arnoux, 9-Aug-2020.)
|- P = ( Base ` G )   &    |- I = (Itv ` G )   &    |- .- = ( dist ` G )   &    |- ( ph -> G e. TarskiG )   &    |- ( ph -> A e. P )   &    |- ( ph -> B e. P )   &    |- ( ph -> C e. P )   &    |- ( ph -> D e. P )   &    |- ( ph -> E e. P )   &    |- ( ph -> F e. P )   &    |- ( ph -> <" A B C "> (cgrA ` G ) <" D E F "> )   &    |- L = (LineG ` G )   &    |- ( ph -> -. ( C e. ( A L B ) \/ A = B ) )   =>    |- ( ph -> -. ( F e. ( D L E ) \/ D = E ) )
Theorem	dfcgra2 25721*	This is the full statement of definition 11.2 of [Schwabhauser] p. 95. This proof serves to confirm that the definition we have chosen, df-cgra 25700 is indeed equivalent with the textbook's definition. (Contributed by Thierry Arnoux, 2-Aug-2020.)
|- P = ( Base ` G )   &    |- I = (Itv ` G )   &    |- .- = ( dist ` G )   &    |- ( ph -> G e. TarskiG )   &    |- ( ph -> A e. P )   &    |- ( ph -> B e. P )   &    |- ( ph -> C e. P )   &    |- ( ph -> D e. P )   &    |- ( ph -> E e. P )   &    |- ( ph -> F e. P )   =>    |- ( ph -> ( <" A B C "> (cgrA ` G ) <" D E F "> <-> ( ( A =/= B /\ C =/= B ) /\ ( D =/= E /\ F =/= E ) /\ E. a e. P E. c e. P E. d e. P E. f e. P ( ( ( A e. ( B I a ) /\ ( A .- a ) = ( E .- D ) ) /\ ( C e. ( B I c ) /\ ( C .- c ) = ( E .- F ) ) ) /\ ( ( D e. ( E I d ) /\ ( D .- d ) = ( B .- A ) ) /\ ( F e. ( E I f ) /\ ( F .- f ) = ( B .- C ) ) ) /\ ( a .- c ) = ( d .- f ) ) ) ) )
Theorem	sacgr 25722	Supplementary angles of congruent angles are themselves congruent. Theorem 11.13 of [Schwabhauser] p. 98. (Contributed by Thierry Arnoux, 30-Sep-2020.)
|- P = ( Base ` G )   &    |- I = (Itv ` G )   &    |- .- = ( dist ` 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 -> X e. P )   &    |- ( ph -> Y e. P )   &    |- ( ph -> <" A B C "> (cgrA ` G ) <" D E F "> )   &    |- ( ph -> B e. ( A I X ) )   &    |- ( ph -> E e. ( D I Y ) )   &    |- ( ph -> B =/= X )   &    |- ( ph -> E =/= Y )   =>    |- ( ph -> <" X B C "> (cgrA ` G ) <" Y E F "> )
Theorem	oacgr 25723	Vertical angle theorem. Vertical, or opposite angles are the facing pair of angles formed when two lines intersect. Eudemus of Rhodes attributed the proof to Thales of Miletus. The proposition showed that since both of a pair of vertical angles are supplementary to both of the adjacent angles, the vertical angles are equal in measure. We follow the same path. Theorem 11.14 of [Schwabhauser] p. 98. (Contributed by Thierry Arnoux, 27-Sep-2020.)
|- P = ( Base ` G )   &    |- I = (Itv ` G )   &    |- .- = ( dist ` G )   &    |- ( ph -> G e. TarskiG )   &    |- ( ph -> A e. P )   &    |- ( ph -> B e. P )   &    |- ( ph -> C e. P )   &    |- ( ph -> D e. P )   &    |- ( ph -> E e. P )   &    |- ( ph -> F e. P )   &    |- ( ph -> B e. ( A I D ) )   &    |- ( ph -> B e. ( C I F ) )   &    |- ( ph -> B =/= A )   &    |- ( ph -> B =/= C )   &    |- ( ph -> B =/= D )   &    |- ( ph -> B =/= F )   =>    |- ( ph -> <" A B C "> (cgrA ` G ) <" D B F "> )
Theorem	acopy 25724*	Angle construction. Theorem 11.15 of [Schwabhauser] p. 98. This is Hilbert's axiom III.4 for geometry. (Contributed by Thierry Arnoux, 9-Aug-2020.)
|- P = ( Base ` G )   &    |- I = (Itv ` G )   &    |- .- = ( dist ` 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 )   &    |- L = (LineG ` G )   &    |- ( ph -> -. ( A e. ( B L C ) \/ B = C ) )   &    |- ( ph -> -. ( D e. ( E L F ) \/ E = F ) )   =>    |- ( ph -> E. f e. P ( <" A B C "> (cgrA ` G ) <" D E f "> /\ f ( (hpG ` G ) ` ( D L E ) ) F ) )
Theorem	acopyeu 25725	Angle construction. Theorem 11.15 of [Schwabhauser] p. 98. This is Hilbert's axiom III.4 for geometry. Akin to a uniqueness theorem, this states that if two points X and Y both fulfill the conditions, then they are on the same half-line. (Contributed by Thierry Arnoux, 9-Aug-2020.)
|- P = ( Base ` G )   &    |- I = (Itv ` G )   &    |- .- = ( dist ` 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 )   &    |- L = (LineG ` G )   &    |- ( ph -> -. ( A e. ( B L C ) \/ B = C ) )   &    |- ( ph -> -. ( D e. ( E L F ) \/ E = F ) )   &    |- ( ph -> X e. P )   &    |- ( ph -> Y e. P )   &    |- K = (hlG ` G )   &    |- ( ph -> <" A B C "> (cgrA ` G ) <" D E X "> )   &    |- ( ph -> <" A B C "> (cgrA ` G ) <" D E Y "> )   &    |- ( ph -> X ( (hpG ` G ) ` ( D L E ) ) F )   &    |- ( ph -> Y ( (hpG ` G ) ` ( D L E ) ) F )   =>    |- ( ph -> X ( K ` E ) Y )
15.2.17  Angle Comparisons
Syntax	cinag 25726	Extend class relation with the geometrical "point in angle" relation.
class inA
Syntax	cleag 25727	Extend class relation with the "angle less than" relation.
class ≤∠
Definition	df-inag 25728*	Definition of the geometrical "in angle" relation. (Contributed by Thierry Arnoux, 15-Aug-2020.)
|- inA = ( g e. _V |-> { <. p , t >. | ( ( p e. ( Base ` g ) /\ t e. ( ( Base ` g ) ^m ( 0..^ 3 ) ) ) /\ ( ( ( t ` 0 ) =/= ( t ` 1 ) /\ ( t ` 2 ) =/= ( t ` 1 ) /\ p =/= ( t ` 1 ) ) /\ E. x e. ( Base ` g ) ( x e. ( ( t ` 0 ) (Itv ` g ) ( t ` 2 ) ) /\ ( x = ( t ` 1 ) \/ x ( (hlG ` g ) ` ( t ` 1 ) ) p ) ) ) ) } )
Theorem	isinag 25729*	Property for point X to lie in the angle <" A B C "> Defnition 11.23 of [Schwabhauser] p. 101. (Contributed by Thierry Arnoux, 15-Aug-2020.)
|- P = ( Base ` G )   &    |- I = (Itv ` G )   &    |- K = (hlG ` G )   &    |- ( ph -> X e. P )   &    |- ( ph -> A e. P )   &    |- ( ph -> B e. P )   &    |- ( ph -> C e. P )   &    |- ( ph -> G e. V )   =>    |- ( ph -> ( X (inA ` G ) <" A B C "> <-> ( ( A =/= B /\ C =/= B /\ X =/= B ) /\ E. x e. P ( x e. ( A I C ) /\ ( x = B \/ x ( K ` B ) X ) ) ) ) )
Theorem	inagswap 25730	Swap the order of the half lines delimiting the angle. Theorem 11.24 of [Schwabhauser] p. 101. (Contributed by Thierry Arnoux, 15-Aug-2020.)
|- P = ( Base ` G )   &    |- I = (Itv ` G )   &    |- K = (hlG ` G )   &    |- ( ph -> X e. P )   &    |- ( ph -> A e. P )   &    |- ( ph -> B e. P )   &    |- ( ph -> C e. P )   &    |- ( ph -> G e. TarskiG )   &    |- ( ph -> X (inA ` G ) <" A B C "> )   =>    |- ( ph -> X (inA ` G ) <" C B A "> )
Theorem	inaghl 25731	The "point lie in angle" relation is independent of the points chosen on the half lines starting from B. Theorem 11.25 of [Schwabhauser] p. 101. (Contributed by Thierry Arnoux, 27-Sep-2020.)
|- P = ( Base ` G )   &    |- I = (Itv ` G )   &    |- K = (hlG ` G )   &    |- ( ph -> X e. P )   &    |- ( ph -> A e. P )   &    |- ( ph -> B e. P )   &    |- ( ph -> C e. P )   &    |- ( ph -> G e. TarskiG )   &    |- ( ph -> X (inA ` G ) <" A B C "> )   &    |- ( ph -> D e. P )   &    |- ( ph -> F e. P )   &    |- ( ph -> Y e. P )   &    |- ( ph -> D ( K ` B ) A )   &    |- ( ph -> F ( K ` B ) C )   &    |- ( ph -> Y ( K ` B ) X )   =>    |- ( ph -> Y (inA ` G ) <" D B F "> )
Definition	df-leag 25732*	Definition of the geometrical "angle less than" relation. Definition 11.27 of [Schwabhauser] p. 102. (Contributed by Thierry Arnoux, 7-Oct-2020.)
|- ≤∠ = ( g e. _V |-> { <. a , b >. | ( ( a e. ( ( Base ` g ) ^m ( 0..^ 3 ) ) /\ b e. ( ( Base ` g ) ^m ( 0..^ 3 ) ) ) /\ E. x e. ( Base ` g ) ( x (inA ` g ) <" ( b ` 0 ) ( b ` 1 ) ( b ` 2 ) "> /\ <" ( a ` 0 ) ( a ` 1 ) ( a ` 2 ) "> (cgrA ` g ) <" ( b ` 0 ) ( b ` 1 ) x "> ) ) } )
Theorem	isleag 25733*	Geometrical "less than" property for angles. Definition 11.27 of [Schwabhauser] p. 102. (Contributed by Thierry Arnoux, 7-Oct-2020.)
|- P = ( Base ` G )   &    |- ( ph -> G e. TarskiG )   &    |- ( ph -> A e. P )   &    |- ( ph -> B e. P )   &    |- ( ph -> C e. P )   &    |- ( ph -> D e. P )   &    |- ( ph -> E e. P )   &    |- ( ph -> F e. P )   =>    |- ( ph -> ( <" A B C "> (≤∠ ` G ) <" D E F "> <-> E. x e. P ( x (inA ` G ) <" D E F "> /\ <" A B C "> (cgrA ` G ) <" D E x "> ) ) )
Theorem	cgrg3col4 25734*	Lemma 11.28 of [Schwabhauser] p. 102. Extend a congruence of three points with a fourth colinear point. (Contributed by Thierry Arnoux, 8-Oct-2020.)
|- P = ( Base ` 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 )   &    |- L = (LineG ` G )   &    |- ( ph -> X e. P )   &    |- ( ph -> <" A B C "> (cgrG ` G ) <" D E F "> )   &    |- ( ph -> ( X e. ( A L C ) \/ A = C ) )   =>    |- ( ph -> E. y e. P <" A B C X "> (cgrG ` G ) <" D E F y "> )
15.2.18  Congruence Theorems
Theorem	tgsas1 25735	First congruence theorem: SAS (Side-Angle-Side): If two pairs of sides of two triangles are equal in length, and the included angles are equal in measurement, then third sides are equal in length. Theorem 11.49 of [Schwabhauser] p. 107. (Contributed by Thierry Arnoux, 1-Aug-2020.)
|- P = ( Base ` G )   &    |- .- = ( dist ` G )   &    |- I = (Itv ` G )   &    |- ( ph -> G e. TarskiG )   &    |- ( ph -> A e. P )   &    |- ( ph -> B e. P )   &    |- ( ph -> C e. P )   &    |- ( ph -> D e. P )   &    |- ( ph -> E e. P )   &    |- ( ph -> F e. P )   &    |- ( ph -> ( A .- B ) = ( D .- E ) )   &    |- ( ph -> <" A B C "> (cgrA ` G ) <" D E F "> )   &    |- ( ph -> ( B .- C ) = ( E .- F ) )   =>    |- ( ph -> ( C .- A ) = ( F .- D ) )
Theorem	tgsas 25736	First congruence theorem: SAS (Side-Angle-Side): If two pairs of sides of two triangles are equal in length, and the included angles are equal in measurement, then the triangles are congruent. Theorem 11.49 of [Schwabhauser] p. 107. (Contributed by Thierry Arnoux, 1-Aug-2020.)
|- P = ( Base ` G )   &    |- .- = ( dist ` G )   &    |- I = (Itv ` G )   &    |- ( ph -> G e. TarskiG )   &    |- ( ph -> A e. P )   &    |- ( ph -> B e. P )   &    |- ( ph -> C e. P )   &    |- ( ph -> D e. P )   &    |- ( ph -> E e. P )   &    |- ( ph -> F e. P )   &    |- ( ph -> ( A .- B ) = ( D .- E ) )   &    |- ( ph -> <" A B C "> (cgrA ` G ) <" D E F "> )   &    |- ( ph -> ( B .- C ) = ( E .- F ) )   =>    |- ( ph -> <" A B C "> (cgrG ` G ) <" D E F "> )
Theorem	tgsas2 25737	First congruence theorem: SAS. Theorem 11.49 of [Schwabhauser] p. 107. (Contributed by Thierry Arnoux, 1-Aug-2020.)
|- P = ( Base ` G )   &    |- .- = ( dist ` G )   &    |- I = (Itv ` G )   &    |- ( ph -> G e. TarskiG )   &    |- ( ph -> A e. P )   &    |- ( ph -> B e. P )   &    |- ( ph -> C e. P )   &    |- ( ph -> D e. P )   &    |- ( ph -> E e. P )   &    |- ( ph -> F e. P )   &    |- ( ph -> ( A .- B ) = ( D .- E ) )   &    |- ( ph -> <" A B C "> (cgrA ` G ) <" D E F "> )   &    |- ( ph -> ( B .- C ) = ( E .- F ) )   &    |- ( ph -> A =/= C )   =>    |- ( ph -> <" C A B "> (cgrA ` G ) <" F D E "> )
Theorem	tgsas3 25738	First congruence theorem: SAS. Theorem 11.49 of [Schwabhauser] p. 107. (Contributed by Thierry Arnoux, 1-Aug-2020.)
|- P = ( Base ` G )   &    |- .- = ( dist ` G )   &    |- I = (Itv ` G )   &    |- ( ph -> G e. TarskiG )   &    |- ( ph -> A e. P )   &    |- ( ph -> B e. P )   &    |- ( ph -> C e. P )   &    |- ( ph -> D e. P )   &    |- ( ph -> E e. P )   &    |- ( ph -> F e. P )   &    |- ( ph -> ( A .- B ) = ( D .- E ) )   &    |- ( ph -> <" A B C "> (cgrA ` G ) <" D E F "> )   &    |- ( ph -> ( B .- C ) = ( E .- F ) )   &    |- ( ph -> A =/= C )   =>    |- ( ph -> <" B C A "> (cgrA ` G ) <" E F D "> )
Theorem	tgasa1 25739	Second congruence theorem: ASA. (Angle-Side-Angle): If two pairs of angles of two triangles are equal in measurement, and the included sides are equal in length, then the triangles are congruent. Theorem 11.50 of [Schwabhauser] p. 108. (Contributed by Thierry Arnoux, 15-Aug-2020.)
|- P = ( Base ` G )   &    |- .- = ( dist ` G )   &    |- I = (Itv ` G )   &    |- ( ph -> G e. TarskiG )   &    |- ( ph -> A e. P )   &    |- ( ph -> B e. P )   &    |- ( ph -> C e. P )   &    |- ( ph -> D e. P )   &    |- ( ph -> E e. P )   &    |- ( ph -> F e. P )   &    |- L = (LineG ` G )   &    |- ( ph -> -. ( C e. ( A L B ) \/ A = B ) )   &    |- ( ph -> ( A .- B ) = ( D .- E ) )   &    |- ( ph -> <" A B C "> (cgrA ` G ) <" D E F "> )   &    |- ( ph -> <" C A B "> (cgrA ` G ) <" F D E "> )   =>    |- ( ph -> ( B .- C ) = ( E .- F ) )
Theorem	tgasa 25740	Second congruence theorem: ASA. (Angle-Side-Angle): If two pairs of angles of two triangles are equal in measurement, and the included sides are equal in length, then the triangles are congruent. Theorem 11.50 of [Schwabhauser] p. 108. (Contributed by Thierry Arnoux, 15-Aug-2020.)
|- P = ( Base ` G )   &    |- .- = ( dist ` G )   &    |- I = (Itv ` G )   &    |- ( ph -> G e. TarskiG )   &    |- ( ph -> A e. P )   &    |- ( ph -> B e. P )   &    |- ( ph -> C e. P )   &    |- ( ph -> D e. P )   &    |- ( ph -> E e. P )   &    |- ( ph -> F e. P )   &    |- L = (LineG ` G )   &    |- ( ph -> -. ( C e. ( A L B ) \/ A = B ) )   &    |- ( ph -> ( A .- B ) = ( D .- E ) )   &    |- ( ph -> <" A B C "> (cgrA ` G ) <" D E F "> )   &    |- ( ph -> <" C A B "> (cgrA ` G ) <" F D E "> )   =>    |- ( ph -> <" A B C "> (cgrG ` G ) <" D E F "> )
Theorem	tgsss1 25741	Third congruence theorem: SSS (Side-Side-Side): If the three pairs of sides of two triangles are equal in length, then the triangles are congruent. Theorem 11.51 of [Schwabhauser] p. 109. (Contributed by Thierry Arnoux, 1-Aug-2020.)
|- P = ( Base ` G )   &    |- .- = ( dist ` G )   &    |- I = (Itv ` G )   &    |- ( ph -> G e. TarskiG )   &    |- ( ph -> A e. P )   &    |- ( ph -> B e. P )   &    |- ( ph -> C e. P )   &    |- ( ph -> D e. P )   &    |- ( ph -> E e. P )   &    |- ( ph -> F e. P )   &    |- ( ph -> ( A .- B ) = ( D .- E ) )   &    |- ( ph -> ( B .- C ) = ( E .- F ) )   &    |- ( ph -> ( C .- A ) = ( F .- D ) )   &    |- ( ph -> A =/= B )   &    |- ( ph -> B =/= C )   &    |- ( ph -> C =/= A )   =>    |- ( ph -> <" A B C "> (cgrA ` G ) <" D E F "> )
Theorem	tgsss2 25742	Third congruence theorem: SSS. Theorem 11.51 of [Schwabhauser] p. 109. (Contributed by Thierry Arnoux, 1-Aug-2020.)
|- P = ( Base ` G )   &    |- .- = ( dist ` G )   &    |- I = (Itv ` G )   &    |- ( ph -> G e. TarskiG )   &    |- ( ph -> A e. P )   &    |- ( ph -> B e. P )   &    |- ( ph -> C e. P )   &    |- ( ph -> D e. P )   &    |- ( ph -> E e. P )   &    |- ( ph -> F e. P )   &    |- ( ph -> ( A .- B ) = ( D .- E ) )   &    |- ( ph -> ( B .- C ) = ( E .- F ) )   &    |- ( ph -> ( C .- A ) = ( F .- D ) )   &    |- ( ph -> A =/= B )   &    |- ( ph -> B =/= C )   &    |- ( ph -> C =/= A )   =>    |- ( ph -> <" C A B "> (cgrA ` G ) <" F D E "> )
Theorem	tgsss3 25743	Third congruence theorem: SSS. Theorem 11.51 of [Schwabhauser] p. 109. (Contributed by Thierry Arnoux, 1-Aug-2020.)
|- P = ( Base ` G )   &    |- .- = ( dist ` G )   &    |- I = (Itv ` G )   &    |- ( ph -> G e. TarskiG )   &    |- ( ph -> A e. P )   &    |- ( ph -> B e. P )   &    |- ( ph -> C e. P )   &    |- ( ph -> D e. P )   &    |- ( ph -> E e. P )   &    |- ( ph -> F e. P )   &    |- ( ph -> ( A .- B ) = ( D .- E ) )   &    |- ( ph -> ( B .- C ) = ( E .- F ) )   &    |- ( ph -> ( C .- A ) = ( F .- D ) )   &    |- ( ph -> A =/= B )   &    |- ( ph -> B =/= C )   &    |- ( ph -> C =/= A )   =>    |- ( ph -> <" B C A "> (cgrA ` G ) <" E F D "> )
Theorem	isoas 25744	Congruence theorem for isocele triangles: if two angles of a triangle are congruent, then the corresponding sides also are. (Contributed by Thierry Arnoux, 5-Oct-2020.)
|- 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 -> -. ( C e. ( A L B ) \/ A = B ) )   &    |- ( ph -> <" A B C "> (cgrA ` G ) <" A C B "> )   =>    |- ( ph -> ( A .- B ) = ( A .- C ) )
15.2.19  Equilateral triangles
Syntax	ceqlg 25745	Declare the class of equilateral triangles.
class eqltrG
Definition	df-eqlg 25746*	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 ) "> } )
Theorem	iseqlg 25747	Property of a triangle being equilateral. (Contributed by Thierry Arnoux, 5-Oct-2020.)
|- 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 C "> e. (eqltrG ` G ) <-> <" A B C "> (cgrG ` G ) <" B C A "> ) )
Theorem	iseqlgd 25748	Condition for a triangle to be equilateral. (Contributed by Thierry Arnoux, 5-Oct-2020.)
|- 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 ) = ( B .- C ) )   &    |- ( ph -> ( B .- C ) = ( C .- A ) )   &    |- ( ph -> ( C .- A ) = ( A .- B ) )   =>    |- ( ph -> <" A B C "> e. (eqltrG ` G ) )
15.3  Properties of geometries
15.3.1  Isomorphisms between geometries
Theorem	f1otrgds 25749*	Convenient lemma for f1otrg 25751. (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 25750*	Convenient lemma for f1otrg 25751. (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 25751*	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 25752*	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 25753	Function to convert an algebraic structure to a Tarski geometry.
class toTG
Definition	df-ttg 25754*	Define a function converting a subcomplex 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 25755*	Define a function to augment a subcomplex 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 25756	Lemma for ttgbas 25757 and ttgvsca 25760. (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 25757	The base set of a subcomplex Hilbert space augmented with betweenness. (Contributed by Thierry Arnoux, 25-Mar-2019.)
|- G = (toTG ` H )   &    |- B = ( Base ` H )   =>    |- B = ( Base ` G )
Theorem	ttgplusg 25758	The addition operation of a subcomplex Hilbert space augmented with betweenness. (Contributed by Thierry Arnoux, 25-Mar-2019.)
|- G = (toTG ` H )   &    |- .+ = ( +g ` H )   =>    |- .+ = ( +g ` G )
Theorem	ttgsub 25759	The subtraction operation of a subcomplex Hilbert space augmented with betweenness. (Contributed by Thierry Arnoux, 25-Mar-2019.)
|- G = (toTG ` H )   &    |- .- = ( -g ` H )   =>    |- .- = ( -g ` G )
Theorem	ttgvsca 25760	The scalar product of a subcomplex Hilbert space augmented with betweenness. (Contributed by Thierry Arnoux, 25-Mar-2019.)
|- G = (toTG ` H )   &    |- .x. = ( .s ` H )   =>    |- .x. = ( .s ` G )
Theorem	ttgds 25761	The metric of a subcomplex Hilbert space augmented with betweenness. (Contributed by Thierry Arnoux, 25-Mar-2019.)
|- G = (toTG ` H )   &    |- D = ( dist ` H )   =>    |- D = ( dist ` G )
Theorem	ttgitvval 25762*	Betweenness for a subcomplex 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 25763*	Betweenness for a subcomplex 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 25764	Any subcomplex 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 25765	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 25766	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 25767*	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 25768	Declare the syntax for the Euclidean space generator.
class EE
Syntax	cbtwn 25769	Declare the syntax for the Euclidean betweenness predicate.
class Btwn
Syntax	ccgr 25770	Declare the syntax for the Euclidean congruence predicate.
class Cgr
Definition	df-ee 25771	Define the Euclidean space generator. For details, see elee 25774. (Contributed by Scott Fenton, 3-Jun-2013.)
|- EE = ( n e. NN |-> ( RR ^m ( 1 ... n ) ) )
Definition	df-btwn 25772*	Define the Euclidean betweenness predicate. For details, see brbtwn 25779. (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 25773*	Define the Euclidean congruence predicate. For details, see brcgr 25780. (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 25774	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 25775*	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 25776	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 25777	The forward direction of elee 25774. (Contributed by Scott Fenton, 1-Jul-2013.)
|- ( A e. ( EE ` N ) -> A : ( 1 ... N ) --> RR )
Theorem	eedimeq 25778	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 25779*	The binary relation 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 25780*	The binary relation 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 25781	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 25782	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 25783*	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 25784*	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 25785*	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 25786	Lemma for colinearalg 25790. 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 25787*	Lemma for colinearalg 25790. 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 25788*	Lemma for colinearalg 25790. 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 25789*	Lemma for colinearalg 25790. 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 25790*	An algebraic characterization of colinearity. Note the similarity to brbtwn2 25785. (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 25791*	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 25792*	Membership of a subtraction mapping in a Euclidean space. Deduction form of eleesub 25791. (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 25793	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 25794	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 25795	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 25796	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 25797*	Lemma for axsegcon 25807. 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 25798*	Lemma for axsegcon 25807. 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 25799*	Lemma for axsegcon 25807. 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 25800*	Lemma for axsegcon 25807. 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 )