:: Tarski Geometry Axioms
:: by William Richter , Adam Grabowski and Jesse Alama
::
:: Copyright (c) 2014-2021 Association of Mizar Users

definition
attr c1 is strict ;
struct TarskiGeometryStruct -> 1-sorted ;
aggr TarskiGeometryStruct(# carrier, Betweenness, Equidistance #) -> TarskiGeometryStruct ;
sel Betweenness c1 -> Relation of [: the carrier of c1, the carrier of c1:], the carrier of c1;
sel Equidistance c1 -> Relation of [: the carrier of c1, the carrier of c1:],[: the carrier of c1, the carrier of c1:];
end;

definition end;

definition
let S be TarskiGeometryStruct ;
let a, b, c be POINT of S;
pred between a,b,c means :: GTARSKI1:def 1
[[a,b],c] in the Betweenness of S;
end;

:: deftheorem defines between GTARSKI1:def 1 :
for S being TarskiGeometryStruct
for a, b, c being POINT of S holds
( between a,b,c iff [[a,b],c] in the Betweenness of S );

definition
let S be TarskiGeometryStruct ;
let a, b, c, d be POINT of S;
pred a,b equiv c,d means :: GTARSKI1:def 2
[[a,b],[c,d]] in the Equidistance of S;
end;

:: deftheorem defines equiv GTARSKI1:def 2 :
for S being TarskiGeometryStruct
for a, b, c, d being POINT of S holds
( a,b equiv c,d iff [[a,b],[c,d]] in the Equidistance of S );

definition
let S be TarskiGeometryStruct ;
let a, b, c, x, y, z be POINT of S;
pred a,b,c cong x,y,z means :: GTARSKI1:def 3
( a,b equiv x,y & a,c equiv x,z & b,c equiv y,z );
end;

:: deftheorem defines cong GTARSKI1:def 3 :
for S being TarskiGeometryStruct
for a, b, c, x, y, z being POINT of S holds
( a,b,c cong x,y,z iff ( a,b equiv x,y & a,c equiv x,z & b,c equiv y,z ) );

definition
let S be TarskiGeometryStruct ;
let a, b, c, d be POINT of S;
pred a,b,c,d are_ordered means :: GTARSKI1:def 4
( between a,b,c & between a,b,d & between a,c,d & between b,c,d );
end;

:: deftheorem defines are_ordered GTARSKI1:def 4 :
for S being TarskiGeometryStruct
for a, b, c, d being POINT of S holds
( a,b,c,d are_ordered iff ( between a,b,c & between a,b,d & between a,c,d & between b,c,d ) );

definition
let S be TarskiGeometryStruct ;
attr S is satisfying_CongruenceSymmetry means :: GTARSKI1:def 5
for a, b being POINT of S holds a,b equiv b,a;
attr S is satisfying_CongruenceEquivalenceRelation means :: GTARSKI1:def 6
for a, b, p, q, r, s being POINT of S st a,b equiv p,q & a,b equiv r,s holds
p,q equiv r,s;
attr S is satisfying_CongruenceIdentity means :: GTARSKI1:def 7
for a, b, c being POINT of S st a,b equiv c,c holds
a = b;
attr S is satisfying_SegmentConstruction means :: GTARSKI1:def 8
for a, q, b, c being POINT of S ex x being POINT of S st
( between q,a,x & a,x equiv b,c );
attr S is satisfying_SAS means :: GTARSKI1:def 9
for a, b, c, x, a1, b1, c1, x1 being POINT of S st a <> b & a,b,c cong a1,b1,c1 & between a,b,x & between a1,b1,x1 & b,x equiv b1,x1 holds
c,x equiv c1,x1;
attr S is satisfying_BetweennessIdentity means :: GTARSKI1:def 10
for a, b being POINT of S st between a,b,a holds
a = b;
attr S is satisfying_Pasch means :: GTARSKI1:def 11
for a, b, p, q, z being POINT of S st between a,p,z & between b,q,z holds
ex x being POINT of S st
( between p,x,b & between q,x,a );
end;

:: deftheorem defines satisfying_CongruenceSymmetry GTARSKI1:def 5 :
for S being TarskiGeometryStruct holds
( S is satisfying_CongruenceSymmetry iff for a, b being POINT of S holds a,b equiv b,a );

:: deftheorem defines satisfying_CongruenceEquivalenceRelation GTARSKI1:def 6 :
for S being TarskiGeometryStruct holds
( S is satisfying_CongruenceEquivalenceRelation iff for a, b, p, q, r, s being POINT of S st a,b equiv p,q & a,b equiv r,s holds
p,q equiv r,s );

:: deftheorem defines satisfying_CongruenceIdentity GTARSKI1:def 7 :
for S being TarskiGeometryStruct holds
( S is satisfying_CongruenceIdentity iff for a, b, c being POINT of S st a,b equiv c,c holds
a = b );

:: deftheorem defines satisfying_SegmentConstruction GTARSKI1:def 8 :
for S being TarskiGeometryStruct holds
( S is satisfying_SegmentConstruction iff for a, q, b, c being POINT of S ex x being POINT of S st
( between q,a,x & a,x equiv b,c ) );

:: deftheorem defines satisfying_SAS GTARSKI1:def 9 :
for S being TarskiGeometryStruct holds
( S is satisfying_SAS iff for a, b, c, x, a1, b1, c1, x1 being POINT of S st a <> b & a,b,c cong a1,b1,c1 & between a,b,x & between a1,b1,x1 & b,x equiv b1,x1 holds
c,x equiv c1,x1 );

:: deftheorem defines satisfying_BetweennessIdentity GTARSKI1:def 10 :
for S being TarskiGeometryStruct holds
( S is satisfying_BetweennessIdentity iff for a, b being POINT of S st between a,b,a holds
a = b );

:: deftheorem defines satisfying_Pasch GTARSKI1:def 11 :
for S being TarskiGeometryStruct holds
( S is satisfying_Pasch iff for a, b, p, q, z being POINT of S st between a,p,z & between b,q,z holds
ex x being POINT of S st
( between p,x,b & between q,x,a ) );

definition
let S be TarskiGeometryStruct ;
end;

:: deftheorem defines satisfying_Tarski-model GTARSKI1:def 12 :

definition end;

definition
let M be MetrStruct ;
mode TarskiExtension of M -> MetrTarskiStr means :TADef: :: GTARSKI1:def 13
MetrStruct(# the carrier of it, the distance of it #) = MetrStruct(# the carrier of M, the distance of M #);
existence
ex b1 being MetrTarskiStr st MetrStruct(# the carrier of b1, the distance of b1 #) = MetrStruct(# the carrier of M, the distance of M #)
proof end;
end;

:: deftheorem TADef defines TarskiExtension GTARSKI1:def 13 :
for M being MetrStruct
for b2 being MetrTarskiStr holds
( b2 is TarskiExtension of M iff MetrStruct(# the carrier of b2, the distance of b2 #) = MetrStruct(# the carrier of M, the distance of M #) );

registration
let M be non empty MetrStruct ;
cluster -> non empty for TarskiExtension of M;
coherence
for b1 being TarskiExtension of M holds not b1 is empty
proof end;
end;

registration
let M be non empty Reflexive MetrStruct ;
cluster -> Reflexive for TarskiExtension of M;
coherence
for b1 being TarskiExtension of M holds b1 is Reflexive
proof end;
end;

registration
let M be non empty discerning MetrStruct ;
cluster -> discerning for TarskiExtension of M;
coherence
for b1 being TarskiExtension of M holds b1 is discerning
proof end;
end;

registration
let M be non empty symmetric MetrStruct ;
cluster -> symmetric for TarskiExtension of M;
coherence
for b1 being TarskiExtension of M holds b1 is symmetric
proof end;
end;

registration
let M be non empty triangle MetrStruct ;
cluster -> triangle for TarskiExtension of M;
coherence
for b1 being TarskiExtension of M holds b1 is triangle
proof end;
end;

definition
let S be MetrStruct ;
let p, q, r be Element of S;
pred q is_Between p,r means :: GTARSKI1:def 14
dist (p,r) = (dist (p,q)) + (dist (q,r));
end;

:: deftheorem defines is_Between GTARSKI1:def 14 :
for S being MetrStruct
for p, q, r being Element of S holds
( q is_Between p,r iff dist (p,r) = (dist (p,q)) + (dist (q,r)) );

definition
let M be MetrTarskiStr ;
attr M is naturally_generated means :NGDef: :: GTARSKI1:def 15
( ( for a, b, c being POINT of M holds
( between a,b,c iff b is_Between a,c ) ) & ( for a, b, c, d being POINT of M holds
( a,b equiv c,d iff dist (a,b) = dist (c,d) ) ) );
end;

:: deftheorem NGDef defines naturally_generated GTARSKI1:def 15 :
for M being MetrTarskiStr holds
( M is naturally_generated iff ( ( for a, b, c being POINT of M holds
( between a,b,c iff b is_Between a,c ) ) & ( for a, b, c, d being POINT of M holds
( a,b equiv c,d iff dist (a,b) = dist (c,d) ) ) ) );

theorem :: GTARSKI1:1
for M, N being MetrStruct
for x, y being Element of M
for a, b being Element of N st MetrStruct(# the carrier of M, the distance of M #) = MetrStruct(# the carrier of N, the distance of N #) & x = a & y = b holds
dist (x,y) = dist (a,b) ;

registration
let N be non empty MetrStruct ;
existence
ex b1 being TarskiExtension of N st b1 is naturally_generated
proof end;
end;

registration
existence
ex b1 being MetrSpace st
( b1 is trivial & not b1 is empty )
proof end;
end;

definition
coherence
the naturally_generated TarskiExtension of the non empty trivial MetrSpace is MetrTarskiStr
;
end;

:: deftheorem defines TrivialTarskiSpace GTARSKI1:def 16 :

registration
coherence
( TrivialTarskiSpace is trivial & not TrivialTarskiSpace is empty )
proof end;
end;

theorem TrivialBetween: :: GTARSKI1:2
for M being non empty trivial MetrSpace
for a, b, c being Element of M holds a is_Between b,c
proof end;

registration end;

registration
existence
ex b1 being TarskiGeometryStruct st
( b1 is satisfying_Tarski-model & not b1 is empty )
proof end;
end;

registration
coherence ;
coherence ;
end;

theorem A1: :: GTARSKI1:3
for S being satisfying_Tarski-model TarskiGeometryStruct
for a, b being POINT of S holds a,b equiv b,a
proof end;

theorem A2: :: GTARSKI1:4
for S being satisfying_Tarski-model TarskiGeometryStruct
for a, b, p, q, r, s being POINT of S st a,b equiv p,q & a,b equiv r,s holds
p,q equiv r,s
proof end;

theorem A3: :: GTARSKI1:5
for S being satisfying_Tarski-model TarskiGeometryStruct
for a, b, c being POINT of S st a,b equiv c,c holds
a = b
proof end;

theorem A4: :: GTARSKI1:6
for S being satisfying_Tarski-model TarskiGeometryStruct
for a, b, c, q being POINT of S ex x being POINT of S st
( between q,a,x & a,x equiv b,c )
proof end;

theorem A5: :: GTARSKI1:7
for S being satisfying_Tarski-model TarskiGeometryStruct
for a, b, c, x, a9, b9, c9, x9 being POINT of S st a <> b & a,b,c cong a9,b9,c9 & between a,b,x & between a9,b9,x9 & b,x equiv b9,x9 holds
c,x equiv c9,x9
proof end;

theorem A6: :: GTARSKI1:8
for S being satisfying_Tarski-model TarskiGeometryStruct
for a, b being POINT of S st between a,b,a holds
a = b
proof end;

theorem A7: :: GTARSKI1:9
for S being satisfying_Tarski-model TarskiGeometryStruct
for a, b, p, q, z being POINT of S st between a,p,z & between b,q,z holds
ex x being POINT of S st
( between p,x,b & between q,x,a )
proof end;

theorem EquivReflexive: :: GTARSKI1:10
for S being satisfying_Tarski-model TarskiGeometryStruct
for a, b being POINT of S holds a,b equiv a,b
proof end;

theorem EquivSymmetric: :: GTARSKI1:11
for S being satisfying_Tarski-model TarskiGeometryStruct
for a, b, c, d being POINT of S st a,b equiv c,d holds
c,d equiv a,b
proof end;

theorem EquivTransitive: :: GTARSKI1:12
for S being satisfying_Tarski-model TarskiGeometryStruct
for a, b, p, q, r, s being POINT of S st a,b equiv p,q & p,q equiv r,s holds
a,b equiv r,s
proof end;

theorem Baaa: :: GTARSKI1:13
for S being satisfying_Tarski-model TarskiGeometryStruct
for a, b being POINT of S holds
( between a,a,a & a,a equiv b,b )
proof end;

theorem Bqaa: :: GTARSKI1:14
for S being satisfying_Tarski-model TarskiGeometryStruct
for a, q being POINT of S holds between q,a,a
proof end;

theorem C1: :: GTARSKI1:15
for S being satisfying_Tarski-model TarskiGeometryStruct
for a, b, x, y being POINT of S st a <> b & between a,b,x & between a,b,y & b,x equiv b,y holds
x = y
proof end;

theorem Bsymmetry: :: GTARSKI1:16
for S being satisfying_Tarski-model TarskiGeometryStruct
for a, p, z being POINT of S st between a,p,z holds
between z,p,a
proof end;

theorem Baaq: :: GTARSKI1:17
for S being satisfying_Tarski-model TarskiGeometryStruct
for a, q being POINT of S holds between a,a,q by ;

theorem BEquality: :: GTARSKI1:18
for S being satisfying_Tarski-model TarskiGeometryStruct
for a, b, c being POINT of S st between a,b,c & between b,a,c holds
a = b
proof end;

theorem B124and234then123: :: GTARSKI1:19
for S being satisfying_Tarski-model TarskiGeometryStruct
for a, b, c, d being POINT of S st between a,b,d & between b,c,d holds
between a,b,c
proof end;

theorem BTransitivity: :: GTARSKI1:20
for S being satisfying_Tarski-model TarskiGeometryStruct
for a, b, c, d being POINT of S st b <> c & between a,b,c & between b,c,d holds
between a,c,d
proof end;

theorem BTransitivityOrdered: :: GTARSKI1:21
for S being satisfying_Tarski-model TarskiGeometryStruct
for a, b, c, d being POINT of S st b <> c & between a,b,c & between b,c,d holds
a,b,c,d are_ordered
proof end;

theorem :: GTARSKI1:22
for S being satisfying_Tarski-model TarskiGeometryStruct
for a, b, c, d being POINT of S st between a,b,d & between b,c,d holds
a,b,c,d are_ordered
proof end;

theorem B124and234Ordered: :: GTARSKI1:23
for S being satisfying_Tarski-model TarskiGeometryStruct
for a, b, c, d being POINT of S st between a,b,d & between b,c,d holds
a,b,c,d are_ordered
proof end;

for S being satisfying_Tarski-model TarskiGeometryStruct
for a, b, c, a9, b9, c9 being POINT of S st between a,b,c & between a9,b9,c9 & a,b equiv a9,b9 & b,c equiv b9,c9 holds
a,c equiv a9,c9
proof end;

theorem CongruenceDoubleSymmetry: :: GTARSKI1:25
for S being satisfying_Tarski-model TarskiGeometryStruct
for a, b, c, d being POINT of S st a,b equiv c,d holds
b,a equiv d,c
proof end;

theorem C1prime: :: GTARSKI1:26
for S being satisfying_Tarski-model TarskiGeometryStruct
for a, b, x, y being POINT of S st a <> b & between a,b,x & between a,b,y & a,x equiv a,y holds
x = y
proof end;

theorem :: GTARSKI1:27
for S being satisfying_Tarski-model TarskiGeometryStruct
for a, b, c, a9, b9, c9 being POINT of S st between a,b,c & between a9,b9,c9 & a,b equiv a9,b9 & a,c equiv a9,c9 holds
b,c equiv b9,c9
proof end;

theorem EasyAngleTransport: :: GTARSKI1:28
for S being satisfying_Tarski-model TarskiGeometryStruct
for a, b, o being POINT of S st o <> a holds
ex x, y being POINT of S st
( between b,o,x & between a,o,y & x,y,o cong a,b,o )
proof end;

theorem B123and134Ordered: :: GTARSKI1:29
for S being satisfying_Tarski-model TarskiGeometryStruct
for a, b, c, d being POINT of S st between a,b,c & between a,c,d holds
a,b,c,d are_ordered
proof end;

theorem BextendToLine: :: GTARSKI1:30
for S being satisfying_Tarski-model TarskiGeometryStruct
for a, b, c, d being POINT of S st a <> b & between a,b,c & between a,b,d holds
ex x being POINT of S st
( a,b,c,x are_ordered & a,b,d,x are_ordered )
proof end;

theorem :: GTARSKI1:31
for S being satisfying_Tarski-model TarskiGeometryStruct
for a, b, c, d being POINT of S st a <> b & between a,b,c & between a,b,d & b <> c & b <> d holds
not between c,b,d
proof end;

theorem Inner5Segments: :: GTARSKI1:32
for S being satisfying_Tarski-model TarskiGeometryStruct
for a, b, c, x, a9, b9, c9, x9 being POINT of S st a,b,c cong a9,b9,c9 & between a,x,c & between a9,x9,c9 & c,x equiv c9,x9 holds
b,x equiv b9,x9
proof end;

theorem RhombusDiagBisect: :: GTARSKI1:33
for S being satisfying_Tarski-model TarskiGeometryStruct
for b, c, d, c9, d9 being POINT of S st between b,c,d9 & between b,d,c9 & c,d9 equiv c,d & d,c9 equiv c,d & d9,c9 equiv c,d holds
ex e being POINT of S st
( between c,e,c9 & between d,e,d9 & c,e equiv c9,e & d,e equiv d9,e )
proof end;

theorem FlatNormal: :: GTARSKI1:34
for S being satisfying_Tarski-model TarskiGeometryStruct
for c, d, e, d9 being POINT of S st between d,e,d9 & c,d9 equiv c,d & d,e equiv d9,e & c <> d & e <> d holds
ex p, r, q being POINT of S st
( between p,r,q & between r,c,d9 & between e,c,p & r,c,p cong r,c,q & r,c equiv e,c & p,r equiv d,e )
proof end;

theorem EqDist2PointsBetween: :: GTARSKI1:35
for S being satisfying_Tarski-model TarskiGeometryStruct
for a, b, c, p, q being POINT of S st a <> b & between a,b,c & a,p equiv a,q & b,p equiv b,q holds
c,p equiv c,q
proof end;

theorem EqDist2PointsInnerBetween: :: GTARSKI1:36
for S being satisfying_Tarski-model TarskiGeometryStruct
for a, c, p, q, x being POINT of S st between a,x,c & a,p equiv a,q & c,p equiv c,q holds
x,p equiv x,q
proof end;

theorem Gupta: :: GTARSKI1:37
for S being satisfying_Tarski-model TarskiGeometryStruct
for a, b, c, d being POINT of S st a <> b & between a,b,c & between a,b,d & not between b,d,c holds
between b,c,d
proof end;

definition
let S be TarskiGeometryStruct ;
let a, b, c be POINT of S;
pred Collinear a,b,c means :: GTARSKI1:def 17
( between a,b,c or between b,c,a or between c,a,b );
end;

:: deftheorem defines Collinear GTARSKI1:def 17 :
for S being TarskiGeometryStruct
for a, b, c being POINT of S holds
( Collinear a,b,c iff ( between a,b,c or between b,c,a or between c,a,b ) );

definition
let S be satisfying_Tarski-model TarskiGeometryStruct ;
let a, b, x be POINT of S;
pred x on_line a,b means :: GTARSKI1:def 18
( a <> b & ( between a,b,x or between b,x,a or between x,a,b ) );
end;

:: deftheorem defines on_line GTARSKI1:def 18 :
for S being satisfying_Tarski-model TarskiGeometryStruct
for a, b, x being POINT of S holds
( x on_line a,b iff ( a <> b & ( between a,b,x or between b,x,a or between x,a,b ) ) );

definition
let S be satisfying_Tarski-model TarskiGeometryStruct ;
let a, b, x, y be POINT of S;
pred a,b equal_line x,y means :: GTARSKI1:def 19
( a <> b & x <> y & ( for c being POINT of S holds
( c on_line a,b iff c on_line x,y ) ) );
end;

:: deftheorem defines equal_line GTARSKI1:def 19 :
for S being satisfying_Tarski-model TarskiGeometryStruct
for a, b, x, y being POINT of S holds
( a,b equal_line x,y iff ( a <> b & x <> y & ( for c being POINT of S holds
( c on_line a,b iff c on_line x,y ) ) ) );

theorem I1part1: :: GTARSKI1:38
for S being satisfying_Tarski-model TarskiGeometryStruct
for a, b, c, x being POINT of S st a <> b & a <> x & x on_line a,b & c on_line a,b holds
c on_line a,x
proof end;

theorem I1part2: :: GTARSKI1:39
for S being satisfying_Tarski-model TarskiGeometryStruct
for a, b, x being POINT of S st a <> b & a <> x & x on_line a,b holds
a,b equal_line a,x
proof end;

theorem :: GTARSKI1:40
for S being satisfying_Tarski-model TarskiGeometryStruct
for a, b being POINT of S st a <> b holds
a,b equal_line a,b ;

theorem LineEqA1: :: GTARSKI1:41
for S being satisfying_Tarski-model TarskiGeometryStruct
for a, b being POINT of S st a <> b holds
a,b equal_line b,a
proof end;

theorem :: GTARSKI1:42
for S being satisfying_Tarski-model TarskiGeometryStruct
for a, b, c, d being POINT of S st a <> b & c <> d & a,b equal_line c,d holds
c,d equal_line a,b ;

theorem :: GTARSKI1:43
for S being satisfying_Tarski-model TarskiGeometryStruct
for a, b, c, d, e, f being POINT of S st a <> b & c <> d & e <> f & a,b equal_line c,d & c,d equal_line e,f holds
a,b equal_line e,f ;

theorem :: GTARSKI1:44
for S being satisfying_Tarski-model TarskiGeometryStruct
for a, b, c, d, x being POINT of S st x on_line a,b & a,b equal_line c,d holds
x on_line c,d ;

theorem I1part2Reverse: :: GTARSKI1:45
for S being satisfying_Tarski-model TarskiGeometryStruct
for a, b, y being POINT of S st a <> b & b <> y & y on_line a,b holds
a,b equal_line y,b
proof end;

theorem :: GTARSKI1:46
for S being satisfying_Tarski-model TarskiGeometryStruct
for a, b, x, y being POINT of S st a <> b & x <> y & a on_line x,y & b on_line x,y holds
x,y equal_line a,b
proof end;

definition
coherence ;
end;

:: deftheorem defines Tarski0Space GTARSKI1:def 20 :

registration
coherence
( Tarski0Space is Reflexive & Tarski0Space is symmetric & not Tarski0Space is empty )
;
end;

definition
let M be non empty MetrStruct ;
attr M is close-everywhere means :Lem1: :: GTARSKI1:def 21
for a, b being Element of M holds dist (a,b) = 0 ;
end;

:: deftheorem Lem1 defines close-everywhere GTARSKI1:def 21 :
for M being non empty MetrStruct holds
( M is close-everywhere iff for a, b being Element of M holds dist (a,b) = 0 );

registration
coherence
proof end;
end;

registration end;

definition
coherence ;
end;

:: deftheorem defines TarskiSpace GTARSKI1:def 22 :

registration
cluster TarskiSpace -> non empty ;
coherence
not TarskiSpace is empty
;
end;

registration
coherence ;
end;

registration
cluster -> real for Element of the carrier of TarskiSpace;
coherence
for b1 being Element of TarskiSpace holds b1 is real
proof end;
end;

registration
cluster -> real for Element of the carrier of RealSpace;
coherence
for b1 being Element of RealSpace holds b1 is real
;
end;

theorem :: GTARSKI1:47
for a, b, c being Element of RealSpace st b in [.a,c.] holds
b is_Between a,c
proof end;

registration end;