:: {T}arski Geometry Axioms -- Part {III}
:: by Roland Coghetto and Adam Grabowski
::
:: Received November 29, 2017
:: Copyright (c) 2017-2019 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies INCSP_1, GTARSKI1, GTARSKI2, GTARSKI3, ZFMISC_1, XXREAL_0,
PROB_1, XBOOLE_0, TARSKI, SUBSET_1, STRUCT_0;
notations GTARSKI1, GTARSKI2, TARSKI, ZFMISC_1, XBOOLE_0, STRUCT_0;
constructors GTARSKI2;
registrations GTARSKI1, GTARSKI2, STRUCT_0, ORDINAL1;
requirements BOOLE, NUMERALS, SUBSET;
begin :: Congruence properties
reserve S for satisfying_CongruenceSymmetry
satisfying_CongruenceEquivalenceRelation
TarskiGeometryStruct,
a,b,c,d,e,f for POINT of S;
::$N 2.1 Satz
theorem :: GTARSKI3:1 ::EquivReflexive ::GTARSKI1:10
a,b equiv a,b;
::$N 2.1 Satz bis
theorem :: GTARSKI3:2
for S being satisfying_CongruenceEquivalenceRelation
satisfying_SegmentConstruction
TarskiGeometryStruct
for a,b being POINT of S holds a,b equiv a,b;
::$N 2.2 Satz
theorem :: GTARSKI3:3 ::GTARSKI1:11 ::EquivSymmetric
a,b equiv c,d implies c,d equiv a,b;
::$N 2.2 Satz bis
theorem :: GTARSKI3:4
for S being satisfying_CongruenceEquivalenceRelation
satisfying_SegmentConstruction
TarskiGeometryStruct
for a,b,c,d being POINT of S st a,b equiv c,d holds c,d equiv a,b;
::$N 2.3 Satz
theorem :: GTARSKI3:5 ::GTARSKI1:12 ::EquivTransitive
a,b equiv c,d & c,d equiv e,f implies a,b equiv e,f;
::$N 2.4 Satz
theorem :: GTARSKI3:6
a,b equiv c,d implies b,a equiv c,d;
::$N 2.5 Satz
theorem :: GTARSKI3:7
a,b equiv c,d implies a,b equiv d,c;
::$N 2.8 Satz
theorem :: GTARSKI3:8 ::GTARSKI1:13 ::Baaa_2
for S being satisfying_CongruenceIdentity
satisfying_SegmentConstruction
TarskiGeometryStruct
for a,b being POINT of S holds a,a equiv b,b;
definition
let S be TarskiGeometryStruct;
attr S is satisfying_SST_A5 means
:: GTARSKI3:def 1
for a,b,c,d,a9,b9,c9,d9 being POINT of S st a <> b & between a,b,c &
between a9,b9,c9 & a,b equiv a9,b9 & b,c equiv b9,c9 & a,d equiv a9,d9 &
b,d equiv b9,d9 holds c,d equiv c9,d9;
end;
theorem :: GTARSKI3:9
S is satisfying_SAS iff S is satisfying_SST_A5;
registration
cluster satisfying_SST_A5 -> satisfying_SAS for
satisfying_CongruenceSymmetry
satisfying_CongruenceEquivalenceRelation
TarskiGeometryStruct;
end;
registration
cluster satisfying_SAS -> satisfying_SST_A5 for
satisfying_CongruenceSymmetry
satisfying_CongruenceEquivalenceRelation
TarskiGeometryStruct;
end;
definition
let S be TarskiGeometryStruct;
let a,b,c,d,a9,b9,c9,d9 being POINT of S;
pred a,b,c,d AFS a9,b9,c9,d9 means
:: GTARSKI3:def 2
between a,b,c & between a9,b9,c9 &
a,b equiv a9,b9 & b,c equiv b9,c9 & a,d equiv a9,d9 & b,d equiv b9,d9;
end;
theorem :: GTARSKI3:10
for S being satisfying_CongruenceSymmetry
satisfying_CongruenceEquivalenceRelation
satisfying_SAS
TarskiGeometryStruct
for a,b,c,d,a9,b9,c9,d9 being POINT of S st a,b,c,d AFS a9,b9,c9,d9 &
a <> b holds c,d equiv c9,d9;
reserve S for satisfying_CongruenceSymmetry
satisfying_CongruenceEquivalenceRelation
satisfying_CongruenceIdentity
satisfying_SegmentConstruction
satisfying_SAS
TarskiGeometryStruct,
q,a,b,c,a9,b9,c9,x1,x2 for POINT of S;
::$N 2.11 Satz
theorem :: GTARSKI3:11 ::GTARSKI1:24
between a,b,c & between a9,b9,c9 & a,b equiv a9,b9 & b,c equiv b9,c9
implies a,c equiv a9,c9;
::$N 2.12 Satz
theorem :: GTARSKI3:12 ::GTARSKI1:26
q <> a implies (for x1,x2 st between q,a,x1 & a,x1 equiv b,c &
between q,a,x2 & a,x2 equiv b,c holds x1 = x2);
begin :: Between properties
::$N 3.1 Satz
theorem :: GTARSKI3:13 ::Bqaa
for S being satisfying_CongruenceIdentity
satisfying_SegmentConstruction
TarskiGeometryStruct
for a,b being POINT of S holds between a,b,b;
reserve S for satisfying_CongruenceIdentity
satisfying_SegmentConstruction
satisfying_BetweennessIdentity
satisfying_Pasch
TarskiGeometryStruct,
a,b,c,d for POINT of S;
::$N 3.2 Satz
theorem :: GTARSKI3:14
between a,b,c implies between c,b,a;
::$N 3.3 Satz
theorem :: GTARSKI3:15 ::Baaa_1
between a,a,b;
::$N 3.4 Satz
theorem :: GTARSKI3:16
for S being satisfying_BetweennessIdentity
satisfying_Pasch
TarskiGeometryStruct
for a,b,c being POINT of S st between a,b,c & between b,a,c holds a = b;
reserve S for satisfying_Tarski-model TarskiGeometryStruct,
a,b,c,d for POINT of S;
::$N 3.5 Satz
theorem :: GTARSKI3:17
between a,b,d & between b,c,d implies between a,b,c & between a,c,d;
::$N 3.6 Satz
theorem :: GTARSKI3:18
between a,b,c & between a,c,d implies between b,c,d & between a,b,d;
::$N 3.7 Satz
theorem :: GTARSKI3:19
between a,b,c & between b,c,d & b <> c implies between a,c,d &
between a,b,d;
::$N 3.8 Definition (n = 4)
definition
let S be TarskiGeometryStruct;
let a,b,c,d be POINT of S;
pred between4 a,b,c,d means
:: GTARSKI3:def 3
between a,b,c & between a,b,d &
between a,c,d & between b,c,d;
end;
::$N 3.8 Definition (n = 5)
definition
let S be TarskiGeometryStruct;
let a,b,c,d,e be POINT of S;
pred between5 a,b,c,d,e means
:: GTARSKI3:def 4
between a,b,c & between a,b,d &
between a,b,e & between a,c,d &
between a,c,e & between a,d,e &
between b,c,d & between b,c,e &
between b,d,e & between c,d,e;
end;
reserve S for satisfying_CongruenceIdentity
satisfying_SegmentConstruction
satisfying_BetweennessIdentity
satisfying_Pasch
TarskiGeometryStruct,
a,b,c,d,e for POINT of S;
::$N 3.9 Satz (n = 3)
theorem :: GTARSKI3:20
between a,b,c implies between c,b,a;
::$N 3.9 Satz (n = 4)
theorem :: GTARSKI3:21
between4 a,b,c,d implies between4 d,c,b,a;
::$N 3.9 Satz (n = 5)
theorem :: GTARSKI3:22
between5 a,b,c,d,e implies between5 e,d,c,b,a;
::$N 3.10 Satz (n = 4)
theorem :: GTARSKI3:23
for S being satisfying_CongruenceIdentity
satisfying_SegmentConstruction
satisfying_BetweennessIdentity
satisfying_Pasch
TarskiGeometryStruct
for a,b,c,d being POINT of S st between4 a,b,c,d holds
between a,b,c & between a,b,d & between a,c,d & between b,c,d;
::$N 3.10 Satz (n = 5)
theorem :: GTARSKI3:24
between5 a,b,c,d,e implies between a,b,c & between a,b,d &
between a,b,e & between a,c,d & between a,c,e & between a,d,e &
between b,c,d & between b,c,e & between b,d,e & between c,d,e &
between4 a,b,c,d & between4 a,b,c,e & between4 a,c,d,e &
between4 b,c,d,e;
reserve S for satisfying_Tarski-model
TarskiGeometryStruct,
a,b,c,d,p for POINT of S;
::$N 3.11 Satz (n = 3, l = 1)
theorem :: GTARSKI3:25
between a,b,c & between a,p,b implies between4 a,p,b,c;
::$N 3.11 Satz (n = 3, l = 2)
theorem :: GTARSKI3:26
between a,b,c & between b,p,c implies between4 a,b,p,c;
::$N 3.11 Satz (n = 3, l = 1)
theorem :: GTARSKI3:27
between4 a,b,c,d & between a,p,b implies between5 a,p,b,c,d;
::$N 3.11 Satz (n = 3, l = 2)
theorem :: GTARSKI3:28
between4 a,b,c,d & between b,p,c implies between5 a,b,p,c,d;
::$N 3.11 Satz (n = 3, l = 3)
theorem :: GTARSKI3:29
between4 a,b,c,d & between c,p,d implies between5 a,b,c,p,d;
::$N 3.12 Satz (n = 3, l = 1)
theorem :: GTARSKI3:30
between a,b,c & between a,c,p implies between4 a,b,c,p & (a <> c implies
between4 a,b,c,p);
::$N 3.12 Satz (n = 3, l = 2)
theorem :: GTARSKI3:31
between a,b,c & between b,c,p implies between b,c,p & (b <> c implies
between4 a,b,c,p);
::$N 3.12 Satz (n = 4, l = 1)
theorem :: GTARSKI3:32
between4 a,b,c,d & between a,d,p implies between5 a,b,c,d,p &
(a <> d implies between5 a,b,c,d,p);
::$N 3.12 Satz (n = 4, l = 2)
theorem :: GTARSKI3:33
between4 a,b,c,d & between b,d,p implies between4 b,c,d,p &
(b <> d implies between5 a,b,c,d,p);
::$N 3.12 Satz (n = 4, l = 3)
theorem :: GTARSKI3:34
between4 a,b,c,d & between c,d,p implies between c,d,p &
(c <> d implies between5 a,b,c,d,p);
registration
cluster satisfying_Lower_Dimension_Axiom for satisfying_Tarski-model
TarskiGeometryStruct;
end;
::$N 3.13 Satz
theorem :: GTARSKI3:35
for S being satisfying_CongruenceIdentity
satisfying_SegmentConstruction
satisfying_Lower_Dimension_Axiom
TarskiGeometryStruct holds
ex a,b,c being POINT of S st not between a,b,c &
not between b,c,a & not between c,a,b & a <> b & b <> c & c <> a;
::$N 3.14 Satz
theorem :: GTARSKI3:36
for S being satisfying_CongruenceSymmetry
satisfying_CongruenceEquivalenceRelation
satisfying_CongruenceIdentity
satisfying_SegmentConstruction
satisfying_Lower_Dimension_Axiom
TarskiGeometryStruct holds
for a,b being POINT of S ex c being POINT of S st between a,b,c & b <> c;
::$N 3.15 Satz (n = 3)
theorem :: GTARSKI3:37
for S being satisfying_CongruenceSymmetry
satisfying_CongruenceEquivalenceRelation
satisfying_CongruenceIdentity
satisfying_SegmentConstruction
satisfying_BetweennessIdentity
satisfying_Lower_Dimension_Axiom
TarskiGeometryStruct holds
for a1,a2 being POINT of S st a1 <> a2 holds
ex a3 being POINT of S st between a1,a2,a3 & a1,a2,a3 are_mutually_distinct;
::$N 3.15 Satz (n = 4)
theorem :: GTARSKI3:38
for S being satisfying_Tarski-model
satisfying_Lower_Dimension_Axiom
TarskiGeometryStruct holds
for a1,a2 being POINT of S st a1 <> a2 holds
ex a3,a4 being POINT of S st between4 a1,a2,a3,a4 &
a1,a2,a3,a4 are_mutually_distinct;
::$N 3.15 Satz (n = 5)
theorem :: GTARSKI3:39
for S being satisfying_Tarski-model
satisfying_Lower_Dimension_Axiom
TarskiGeometryStruct holds
for a1,a2 being POINT of S st a1 <> a2 holds
ex a3,a4,a5 being POINT of S st between5 a1,a2,a3,a4,a5 &
a1,a2,a3,a4,a5 are_mutually_distinct;
::$N 3.17 Satz
theorem :: GTARSKI3:40
for S being satisfying_Tarski-model
TarskiGeometryStruct
for a,b,c,p,a9,b9,c9 being POINT of S st between a,b,c & between a9,b9,c &
between a,p,a9 holds ex q being POINT of S st between p,q,c & between b,q,b9;
begin :: Collinearity
definition
let S be TarskiGeometryStruct;
let a,b,c,d,a9,b9,c9,d9 be POINT of S;
pred a,b,c,d IFS a9,b9,c9,d9 means
:: GTARSKI3:def 5
between a,b,c & between a9,b9,c9 &
a,c equiv a9,c9 & b,c equiv b9,c9 &
a,d equiv a9,d9 & c,d equiv c9,d9;
end;
reserve S for satisfying_Tarski-model TarskiGeometryStruct,
a,b,c,d,a9,b9,c9,d9 for POINT of S;
::$N 4.2 Satz
theorem :: GTARSKI3:41
a,b,c,d IFS a9,b9,c9,d9 implies b,d equiv b9,d9;
::$N 4.3 Satz
theorem :: GTARSKI3:42
between a,b,c & between a9,b9,c9 & a,c equiv a9,c9 & b,c equiv b9,c9
implies a,b equiv a9,b9;
::$N 4.5 Satz
theorem :: GTARSKI3:43
between a,b,c & a,c equiv a9,c9 implies ex b9 st between a9,b9,c9 &
a,b,c cong a9,b9,c9;
::$N 4.6 Satz
theorem :: GTARSKI3:44
between a,b,c & a,b,c cong a9,b9,c9 implies between a9,b9,c9;
::$N 4.11 Satz
theorem :: GTARSKI3:45
for S being satisfying_CongruenceIdentity
satisfying_SegmentConstruction
satisfying_BetweennessIdentity
satisfying_Pasch
TarskiGeometryStruct
for a,b,c being POINT of S st Collinear a,b,c holds
Collinear b,c,a & Collinear c,a,b & Collinear c,b,a &
Collinear b,a,c & Collinear a,c,b;
::$N 4.12 Sazz
theorem :: GTARSKI3:46
for S being satisfying_CongruenceIdentity
satisfying_SegmentConstruction
TarskiGeometryStruct
for a,b being POINT of S holds Collinear a,a,b;
theorem :: GTARSKI3:47
for S being satisfying_CongruenceSymmetry
satisfying_CongruenceEquivalenceRelation
TarskiGeometryStruct
for a,b,c,a9,b9,c9 being POINT of S st a,b,c cong a9,b9,c9 holds
b,c,a cong b9,c9,a9;
::$N 4.13 Satz
theorem :: GTARSKI3:48
for S being satisfying_Tarski-model
TarskiGeometryStruct
for a,b,c,a9,b9,c9 being POINT of S st Collinear a,b,c &
a,b,c cong a9,b9,c9 holds Collinear a9,b9,c9;
theorem :: GTARSKI3:49
for S being satisfying_CongruenceSymmetry
satisfying_CongruenceEquivalenceRelation
TarskiGeometryStruct
for a,b,c,a9,b9,c9 being POINT of S st b,a,c cong b9,a9,c9 holds
a,b,c cong a9,b9,c9;
theorem :: GTARSKI3:50
for S being satisfying_CongruenceSymmetry
satisfying_CongruenceEquivalenceRelation
TarskiGeometryStruct
for a,b,c,a9,b9,c9 being POINT of S st
a,c,b cong a9,c9,b9 holds a,b,c cong a9,b9,c9;
reserve S for satisfying_Tarski-model
TarskiGeometryStruct,
a,b,c,d,a9,b9,c9,d9,p,q for POINT of S;
::$N 4.14 Satz
theorem :: GTARSKI3:51
Collinear a,b,c & a,b equiv a9,b9 implies ex c9 being POINT of S st
a,b,c cong a9,b9,c9;
definition
let S be TarskiGeometryStruct;
let a,b,c,d,a9,b9,c9,d9 be POINT of S;
pred a,b,c,d FS a9,b9,c9,d9 means
:: GTARSKI3:def 6
Collinear a,b,c &
a,b,c cong a9,b9,c9 &
a,d equiv a9,d9 & b,d equiv b9,d9;
end;
::$N 4.16 Satz
theorem :: GTARSKI3:52
a,b,c,d FS a9,b9,c9,d9 & a <> b implies c,d equiv c9,d9;
::$N 4.17 Satz
theorem :: GTARSKI3:53
a <> b & Collinear a,b,c & a,p equiv a,q & b,p equiv b,q implies
c,p equiv c,q;
::$N 4.18 Satz
theorem :: GTARSKI3:54
a <> b & Collinear a,b,c & a,c equiv a,c9 & b,c equiv b,c9 implies c = c9;
::$N 4.19 Satz
theorem :: GTARSKI3:55
between a,c,b & a,c equiv a,c9 & b,c equiv b,c9 implies c = c9;
begin :: Between transitivity le
reserve S for satisfying_Tarski-model
TarskiGeometryStruct,
a,b,c,d,e,f,a9,b9,c9,d9 for POINT of S;
::$N 5.1 Satz
theorem :: GTARSKI3:56 ::GTARSKI1:37
a <> b & between a,b,c & between a,b,d implies between a,c,d or between a,d,c
;
::$N 5.2 Satz
theorem :: GTARSKI3:57
a <> b & between a,b,c & between a,b,d implies between b,c,d or between b,d,c
;
::$N 5.3 Satz
theorem :: GTARSKI3:58
between a,b,d & between a,c,d implies between a,b,c or between a,c,b;
definition
let S be TarskiGeometryStruct;
let a,b,c,d be POINT of S;
pred a,b <= c,d means
:: GTARSKI3:def 7
ex y being POINT of S st between c,y,d & a,b equiv c,y;
end;
::$N 5.5 Satz
theorem :: GTARSKI3:59
a,b <= c,d iff
(ex x being POINT of S st between a,b,x & a,x equiv c,d);
::$N 5.6 Satz
theorem :: GTARSKI3:60
a,b <= c,d & a,b equiv a9,b9 & c,d equiv c9,d9 implies a9,b9 <= c9,d9;
::$N 5.7 Satz
theorem :: GTARSKI3:61
a,b <= a,b;
::$N 5.8 Satz
theorem :: GTARSKI3:62
a,b <= c,d & c,d <= e,f implies a,b <= e,f;
::$N 5.9 Satz
theorem :: GTARSKI3:63
a,b <= c,d & c,d <= a,b implies a,b equiv c,d;
::$N 5.10 Satz
theorem :: GTARSKI3:64
a,b <= c,d or c,d <= a,b;
::$N 5.11 Satz
theorem :: GTARSKI3:65
a,a <= b,c;
::$N 5.12 Lemma 1
theorem :: GTARSKI3:66
for S being satisfying_CongruenceIdentity
satisfying_SegmentConstruction
satisfying_BetweennessIdentity
satisfying_Pasch
satisfying_CongruenceSymmetry
satisfying_CongruenceEquivalenceRelation
TarskiGeometryStruct
for a,b,c,d being POINT of S holds
a,b <= c,d implies b,a <= c,d;
::$N 5.12 Lemma 2
theorem :: GTARSKI3:67
a,b <= c,d implies a,b <= d,c;
::$N 5.12 Lemma 3
theorem :: GTARSKI3:68
between a,b,c & a,c equiv a,b implies c = b;
::$N METAMATH: endofsegidand
theorem :: GTARSKI3:69
between a,c,b & a,b <= a,c implies b = c;
::$N 5.12 Satz
theorem :: GTARSKI3:70
Collinear a,b,c implies (between a,b,c iff (a,b <= a,c & b,c <= a,c));
begin :: Out lines
definition
let S be TarskiGeometryStruct;
let a,b,p be POINT of S;
pred p out a,b means
:: GTARSKI3:def 8
p <> a & p <> b & (between p,a,b or between p,b,a);
end;
reserve p for POINT of S;
::$N 6.2 Satz
theorem :: GTARSKI3:71
a <> p & b <> p & c <> p & between a,p,c implies
(between b,p,c iff p out a,b);
::$N 6.3 Satz
theorem :: GTARSKI3:72
p out a,b iff (a <> p & b <> p &
(ex c st c <> p & between a,p,c & between b,p,c));
::$N 6.4 Satz
theorem :: GTARSKI3:73
p out a,b iff (Collinear a,p,b & not between a,p,b);
::$N 6.5 Satz
theorem :: GTARSKI3:74
a <> p implies p out a,a;
::$N 6.6 Satz
theorem :: GTARSKI3:75
p out a,b implies p out b,a;
::$N 6.7 Satz
theorem :: GTARSKI3:76
p out a,b & p out b,c implies p out a,c;
::$N METAMATH: segcon2
theorem :: GTARSKI3:77
ex x being POINT of S st (between p,a,x or between p,x,a) & p,x equiv b,c;
reserve r for POINT of S;
::$N 6.11 Satz a)
theorem :: GTARSKI3:78
r <> a & b <> c implies ex x being POINT of S st (a out x,r & a,x equiv b,c);
definition
let S be TarskiGeometryStruct;
let a,p be POINT of S;
func halfline(p,a) -> set equals
:: GTARSKI3:def 9
{x where x is POINT of S: p out x,a};
end;
reserve x,y for POINT of S;
::$N 6.11 Satz b)
theorem :: GTARSKI3:79
r <> a & b <> c & (a out x,r & a,x equiv b,c) & (a out y,r & a,y equiv b,c)
implies x = y;
::$N 6.13 Satz
theorem :: GTARSKI3:80
p out a,b implies (p,a <= p,b iff between p,a,b);
::$N 6.14 Definition
definition
let S be non empty TarskiGeometryStruct;
let p,q be POINT of S;
func Line(p,q) -> Subset of S equals
:: GTARSKI3:def 10
{x where x is POINT of S: Collinear p,q,x};
end;
reserve S for non empty satisfying_Tarski-model TarskiGeometryStruct;
reserve p,q,r,s for POINT of S;
::$N 6.15 Satz
theorem :: GTARSKI3:81
p <> q & p <> r & between q,p,r implies
Line(p,q) = halfline(p,q) \/ {p} \/ halfline(p,r);
definition
let S be non empty TarskiGeometryStruct;
let A be Subset of S;
pred A is_line means
:: GTARSKI3:def 11
ex p,q being POINT of S st p <> q & A = Line(p,q);
end;
::$N 6.16 Satz
theorem :: GTARSKI3:82 :: GTARSKI1:45
p <> q & s <> p & s in Line(p,q) implies Line(p,q) = Line(p,s);
reserve S for non empty satisfying_CongruenceIdentity
satisfying_SegmentConstruction
satisfying_BetweennessIdentity
satisfying_Pasch
TarskiGeometryStruct,
a,b,p,q for POINT of S;
::$N 6.17 Satz
theorem :: GTARSKI3:83
p in Line(p,q) & q in Line(p,q) & Line(p,q) = Line(q,p);
reserve S for non empty satisfying_Tarski-model TarskiGeometryStruct,
A,B for Subset of S,
a,b,c,p,q,r,s for POINT of S;
theorem :: GTARSKI3:84
for S being satisfying_Tarski-model TarskiGeometryStruct
for a,b,c being Element of S holds
(a <> b & Collinear a,b,c) iff c on_line a,b;
theorem :: GTARSKI3:85
for S being satisfying_Tarski-model non empty TarskiGeometryStruct
for a,b,x,y being POINT of S st
a,b equal_line x,y holds Line(a,b) = Line(x,y);
theorem :: GTARSKI3:86
for S being satisfying_Tarski-model non empty TarskiGeometryStruct
for a,b,x,y being POINT of S st a <> b & x <> y &
Line(a,b) = Line(x,y) holds a,b equal_line x,y;
::$N 6.18 Satz
theorem :: GTARSKI3:87 ::GTARSKI_1:46
A is_line & a <> b & a in A & b in A implies A = Line(a,b);
::$N 6.19 Satz
theorem :: GTARSKI3:88
a <> b & A is_line & a in A & b in A & B is_line & a in B & b in B
implies A = B;
::$N 6.21 Satz
theorem :: GTARSKI3:89
A is_line & B is_line & A <> B &
a in A & a in B & b in A & b in B implies a = b;
::$N 6.23 Satz
theorem :: GTARSKI3:90
(ex p,q st p <> q) implies (Collinear a,b,c iff
(ex A st A is_line & a in A & b in A & c in A));
::$N 6.24 Satz
theorem :: GTARSKI3:91
for S being satisfying_A8 TarskiGeometryStruct
ex a,b,c being POINT of S st not Collinear a,b,c;
::$N 6.25 Satz
theorem :: GTARSKI3:92
for S being non empty satisfying_Tarski-model TarskiGeometryStruct
for a,b being POINT of S st
S is satisfying_A8 &
a <> b holds ex c being POINT of S st not Collinear a,b,c;
theorem :: GTARSKI3:93
for S being satisfying_Tarski-model TarskiGeometryStruct
for p,a,b being POINT of S st p out a,b & p,a <= p,b holds between p,a,b;
theorem :: GTARSKI3:94
for S being satisfying_Tarski-model TarskiGeometryStruct
for a,b,c,d,e,f,g,h being Element of S st
not c,d <= a,b & a,b equiv e,f & c,d equiv g,h holds
e,f <= g,h;
::$N 6.28 Satz, introduced by Beeson
theorem :: GTARSKI3:95
for S being satisfying_Tarski-model TarskiGeometryStruct
for a,b,c,a1,b1,c1 being Element of S st
b out a,c & b1 out a1,c1 & b,a equiv b1,a1 & b,c equiv b1,c1 holds
a,c equiv a1,c1;
begin :: Midpoint
definition
let S be TarskiGeometryStruct;
let a,b,m be POINT of S;
pred Middle a,m,b means
:: GTARSKI3:def 12
between a,m,b & m,a equiv m,b;
end;
reserve S for satisfying_CongruenceIdentity
satisfying_CongruenceSymmetry
satisfying_CongruenceEquivalenceRelation
satisfying_SegmentConstruction
satisfying_BetweennessIdentity
satisfying_Pasch
TarskiGeometryStruct,
a,b,m for POINT of S;
::$N 7.2 Satz
theorem :: GTARSKI3:96
Middle a,m,b implies Middle b,m,a;
reserve S for satisfying_CongruenceIdentity
satisfying_CongruenceSymmetry
satisfying_CongruenceEquivalenceRelation
satisfying_SegmentConstruction
satisfying_BetweennessIdentity
TarskiGeometryStruct,
a,b,m for POINT of S;
::$N 7.3 Satz
theorem :: GTARSKI3:97
Middle a,m,a iff m = a;
::$N 7.4 Existence
theorem :: GTARSKI3:98
for p being POINT of S holds ex p9 being POINT of S st Middle p,a,p9;
reserve S for satisfying_CongruenceIdentity
satisfying_CongruenceSymmetry
satisfying_CongruenceEquivalenceRelation
satisfying_SegmentConstruction
satisfying_SAS
TarskiGeometryStruct,
a for POINT of S;
::$N 7.4 Uniqueness
theorem :: GTARSKI3:99
for p,p1,p2 being POINT of S st Middle p,a,p1 & Middle p,a,p2 holds p1 = p2;
definition
let S be satisfying_CongruenceIdentity
satisfying_CongruenceSymmetry
satisfying_CongruenceEquivalenceRelation
satisfying_SegmentConstruction
satisfying_BetweennessIdentity
satisfying_SAS
TarskiGeometryStruct;
let a,p be POINT of S;
func reflection(a,p) -> POINT of S means
:: GTARSKI3:def 13
Middle p,a,it;
end;
reserve S for satisfying_CongruenceIdentity
satisfying_CongruenceSymmetry
satisfying_CongruenceEquivalenceRelation
satisfying_SegmentConstruction
satisfying_BetweennessIdentity
satisfying_SAS
TarskiGeometryStruct,
a,p,p9 for POINT of S;
::$N 7.6 Satz
theorem :: GTARSKI3:100
reflection(a,p) = p9 iff Middle p,a,p9;
reserve S for satisfying_CongruenceIdentity
satisfying_CongruenceSymmetry
satisfying_CongruenceEquivalenceRelation
satisfying_SegmentConstruction
satisfying_BetweennessIdentity
satisfying_SAS
satisfying_Pasch
TarskiGeometryStruct,
a,p,p9 for POINT of S;
::$N 7.7 Satz
theorem :: GTARSKI3:101
reflection(a,reflection(a,p)) = p;
::$N 7.8 Satz
theorem :: GTARSKI3:102
ex p st reflection(a,p) = p9;
::$N 7.9 Satz
theorem :: GTARSKI3:103
reflection(a,p) = reflection(a,p9) implies p = p9;
reserve S for satisfying_CongruenceIdentity
satisfying_CongruenceSymmetry
satisfying_CongruenceEquivalenceRelation
satisfying_SegmentConstruction
satisfying_BetweennessIdentity
satisfying_SAS
TarskiGeometryStruct,
a,p for POINT of S;
::$N 7.10 Satz
theorem :: GTARSKI3:104
reflection(a,p) = p iff p = a;
reserve S for satisfying_Tarski-model TarskiGeometryStruct,
a,b,c,d,m,p,p9,q,r,s for POINT of S;
::$N 7.13 Satz
theorem :: GTARSKI3:105
p,q equiv reflection(a,p),reflection(a,q);
::$N 7.15 Satz
theorem :: GTARSKI3:106
between p,q,r iff between reflection(a,p),reflection(a,q),reflection(a,r);
::$N 7.16 Satz
theorem :: GTARSKI3:107
p,q equiv r,s iff
reflection(a,p),reflection(a,q) equiv reflection(a,r),reflection(a,s);
::$N 7.17 Satz
theorem :: GTARSKI3:108
Middle p,a,p9 & Middle p,b,p9 implies a = b;
::$N 7.18 Satz
theorem :: GTARSKI3:109
reflection(a,p) = reflection(b,p) implies a = b;
::$N 7.19 Satz
theorem :: GTARSKI3:110
reflection(b,reflection(a,p)) = reflection(a,reflection(b,p)) iff a = b;
::$N 7.20 Satz
theorem :: GTARSKI3:111
Collinear a,m,b & m,a equiv m,b implies a = b or Middle a,m,b;
reserve S for non empty satisfying_Tarski-model TarskiGeometryStruct,
a,b,c,d,p for POINT of S;
::$N 7.21 Satz
theorem :: GTARSKI3:112
not Collinear a,b,c & b <> d & a,b equiv c,d & b,c equiv d,a &
Collinear a,p,c & Collinear b,p,d implies Middle a,p,c & Middle b,p,d;
reserve a1,a2,b1,b2,m1,m2 for POINT of S;
::$N 7.22 Satz, part 1
theorem :: GTARSKI3:113
between a1,c,a2 & between b1,c,b2 & c,a1 equiv c,b1 &
c,a2 equiv c,b2 & Middle a1,m1,b1 & Middle a2,m2,b2 &
c,a1 <= c,a2
implies between m1,c,m2;
::$N 7.22 Satz, part 2
theorem :: GTARSKI3:114
between a1,c,a2 & between b1,c,b2 & c,a1 equiv c,b1 &
c,a2 equiv c,b2 & Middle a1,m1,b1 & Middle a2,m2,b2 &
c,a2 <= c,a1
implies between m1,c,m2;
::$N 7.22 Satz: Krippenlemma, (Gupta 1965, 3.45 Theorem)
theorem :: GTARSKI3:115
between a1,c,a2 & between b1,c,b2 & c,a1 equiv c,b1 &
c,a2 equiv c,b2 & Middle a1,m1,b1 & Middle a2,m2,b2 implies between m1,c,m2;
definition
let S be TarskiGeometryStruct;
let a1,a2,b1,b2,c,m1,m2 be POINT of S;
pred Krippenfigur a1,m1,b1,c,b2,m2,a2 means
:: GTARSKI3:def 14
between a1,c,a2 & between b1,c,b2 & c,a1 equiv c,b1 &
c,a2 equiv c,b2 & Middle a1,m1,b1 & Middle a2,m2,b2;
end;
::$N Krippenfigur
theorem :: GTARSKI3:116
Krippenfigur a1,m1,b1,c,b2,m2,a2 implies between m1,c,m2;
registration
cluster non empty for satisfying_Lower_Dimension_Axiom
satisfying_Tarski-model TarskiGeometryStruct;
end;
reserve S for non empty
satisfying_Lower_Dimension_Axiom
satisfying_Tarski-model
TarskiGeometryStruct,
a,b,c,p,q,r for POINT of S;
::$ 7.25 Satz
theorem :: GTARSKI3:117
c,a equiv c,b implies ex x being POINT of S st Middle a,x,b;
begin :: Note about Makarios's simplification of Tarski's axiom of geometry
definition
let S be TarskiGeometryStruct;
attr S is (RE) means
:: GTARSKI3:def 15
for a,b being POINT of S holds a,b equiv b,a;
attr S is (TE) means
:: GTARSKI3:def 16
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 (IE) means
:: GTARSKI3:def 17
for a,b,c being POINT of S st a,b equiv c,c holds a = b;
attr S is (SC) means
:: GTARSKI3:def 18
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;
attr S is (FS) means
:: GTARSKI3:def 19
for a,b,c,d,a9,b9,c9,d9 being POINT of S st
a <> b & between a,b,c &
between a9,b9,c9 & a,b equiv a9,b9 &
b,c equiv b9,c9 & a,d equiv a9,d9 &
b,d equiv b9,d9 holds c,d equiv c9,d9;
attr S is (IB) means
:: GTARSKI3:def 20
for a,b being POINT of S st between a,b,a holds a = b;
attr S is (Pa) means
:: GTARSKI3:def 21
for a,b,c,p,q being POINT of S st
between a,p,c & between b,q,c holds
ex x being POINT of S st between p,x,b & between q,x,a;
attr S is (Lo2) means
:: GTARSKI3:def 22
ex a,b,c being POINT of S st
not between a,b,c & not between b,c,a & not between c,a,b;
attr S is (Up2) means
:: GTARSKI3:def 23
for a,b,c,p,q being POINT of S st p <> q &
a,p equiv a,q & b,p equiv b,q & c,p equiv c,q holds
between a,b,c or between b,c,a or between c,a,b;
attr S is (Eu) means
:: GTARSKI3:def 24
for a,b,c,d,t being POINT of S st
between a,d,t & between b,d,c & a <> d holds
ex x,y being POINT of S st
between a,b,x & between a,c,y & between x,t,y;
attr S is (Co) means
:: GTARSKI3:def 25
for X,Y being set st
(ex a being POINT of S st
(for x,y being POINT of S st x in X & y in Y holds between a,x,y))
holds
(ex b being POINT of S st
(for x,y being POINT of S st x in X & y in Y holds between x,b,y));
attr S is (FS') means
:: GTARSKI3:def 26
for a,b,c,d,a9,b9,c9,d9 being POINT of S st
a <> b & between a,b,c & between a9,b9,c9 &
a,b equiv a9,b9 &
b,c equiv b9,c9 & a,d equiv a9,d9 &
b,d equiv b9,d9 holds d,c equiv c9,d9;
end;
reserve S for TarskiGeometryStruct;
theorem :: GTARSKI3:118
S is satisfying_CongruenceSymmetry iff S is (RE);
theorem :: GTARSKI3:119
S is satisfying_CongruenceEquivalenceRelation iff S is (TE);
theorem :: GTARSKI3:120
S is satisfying_CongruenceIdentity iff S is (IE);
theorem :: GTARSKI3:121
S is satisfying_SegmentConstruction iff S is (SC);
theorem :: GTARSKI3:122
S is satisfying_BetweennessIdentity iff S is (IB);
theorem :: GTARSKI3:123
S is satisfying_Pasch iff S is (Pa);
theorem :: GTARSKI3:124
S is satisfying_Lower_Dimension_Axiom iff S is (Lo2);
theorem :: GTARSKI3:125
S is satisfying_Upper_Dimension_Axiom iff S is (Up2);
theorem :: GTARSKI3:126
S is satisfying_Euclid_Axiom iff S is (Eu);
theorem :: GTARSKI3:127
for S being satisfying_CongruenceSymmetry
satisfying_CongruenceEquivalenceRelation
TarskiGeometryStruct holds
S is satisfying_SAS iff S is (FS);
theorem :: GTARSKI3:128
for S being non empty TarskiGeometryStruct holds
S is satisfying_Continuity_Axiom iff S is (Co);
registration
cluster (RE) -> satisfying_CongruenceSymmetry for TarskiGeometryStruct;
cluster (TE) -> satisfying_CongruenceEquivalenceRelation
for TarskiGeometryStruct;
cluster (IE) -> satisfying_CongruenceIdentity for TarskiGeometryStruct;
cluster (SC) -> satisfying_SegmentConstruction for TarskiGeometryStruct;
cluster (IB) -> satisfying_BetweennessIdentity for TarskiGeometryStruct;
cluster (Pa) -> satisfying_Pasch for TarskiGeometryStruct;
cluster (Lo2) -> satisfying_Lower_Dimension_Axiom for TarskiGeometryStruct;
cluster (Up2) -> satisfying_Upper_Dimension_Axiom for TarskiGeometryStruct;
cluster (Eu) -> satisfying_Euclid_Axiom for TarskiGeometryStruct;
cluster (Co) -> satisfying_Continuity_Axiom for TarskiGeometryStruct;
end;
registration
cluster satisfying_CongruenceSymmetry -> (RE) for TarskiGeometryStruct;
cluster satisfying_CongruenceEquivalenceRelation ->
(TE) for TarskiGeometryStruct;
cluster satisfying_CongruenceIdentity -> (IE) for TarskiGeometryStruct;
cluster satisfying_SegmentConstruction -> (SC) for TarskiGeometryStruct;
cluster satisfying_BetweennessIdentity -> (IB) for TarskiGeometryStruct;
cluster satisfying_Pasch -> (Pa) for TarskiGeometryStruct;
cluster satisfying_Lower_Dimension_Axiom -> (Lo2) for TarskiGeometryStruct;
cluster satisfying_Upper_Dimension_Axiom -> (Up2) for TarskiGeometryStruct;
cluster satisfying_Euclid_Axiom -> (Eu) for TarskiGeometryStruct;
cluster satisfying_Continuity_Axiom -> (Co)
for non empty TarskiGeometryStruct;
end;
registration
cluster (RE) (TE) for TarskiGeometryStruct;
end;
theorem :: GTARSKI3:129
for S being (RE) (TE) TarskiGeometryStruct holds
S is satisfying_SAS iff S is (FS);
registration
cluster (FS) -> satisfying_SAS for (RE) (TE) TarskiGeometryStruct;
end;
registration
cluster (FS) for (RE) (TE) TarskiGeometryStruct;
end;
reserve S for TarskiGeometryStruct;
::$N Makarios: Lemma 6
theorem :: GTARSKI3:130
for S being TarskiGeometryStruct st
S is (RE) & S is (TE) holds
(S is (FS) iff S is (FS'));
theorem :: GTARSKI3:131
for S being (RE) (TE) TarskiGeometryStruct holds
S is (FS) iff S is (FS');
registration
cluster (FS') -> (FS) for (RE) (TE) TarskiGeometryStruct;
end;
registration
cluster (TE) (SC) for TarskiGeometryStruct;
end;
registration
cluster (FS') for (RE) (TE) TarskiGeometryStruct;
end;
registration
cluster (SC) for (RE) (TE) (FS') TarskiGeometryStruct;
end;
theorem :: GTARSKI3:132
for S being (TE) (SC) TarskiGeometryStruct holds
for a,b being POINT of S holds a,b equiv a,b;
theorem :: GTARSKI3:133
for S being (IE) (SC) TarskiGeometryStruct holds
for a,b being POINT of S holds between a,b,b;
theorem :: GTARSKI3:134
for S being (TE) (SC) TarskiGeometryStruct holds
for a,b,c,d being POINT of S st a,b equiv c,d holds c,d equiv a,b;
theorem :: GTARSKI3:135
for S being (TE) (SC) (FS') TarskiGeometryStruct holds
(for a,b,c,d,e,f being POINT of S st
a <> b & between b,a,c & between d,a,e &
b,a equiv d,a & a,c equiv a,e & b,f equiv d,f
holds
f,c equiv e,f);
definition
let S be TarskiGeometryStruct;
attr S is (RE') means
:: GTARSKI3:def 27
for a,b,c,d being POINT of S st a <> b & between b,a,c holds d,c equiv c,d;
end;
theorem :: GTARSKI3:136
for S being (TE) (SC) (FS') TarskiGeometryStruct holds S is (RE');
registration
cluster (TE) (SC) (FS') -> (RE') for TarskiGeometryStruct;
end;
registration
cluster (RE') for (IE) TarskiGeometryStruct;
end;
registration
cluster (SC) for (RE') (IE) TarskiGeometryStruct;
end;
registration
cluster trivial for (IE) non empty TarskiGeometryStruct;
end;
registration
cluster trivial for (IE) (SC) non empty TarskiGeometryStruct;
end;
theorem :: GTARSKI3:137
for S being trivial (IE) (SC) non empty TarskiGeometryStruct holds S is (RE);
registration
cluster (RE') for (TE) (IE) (SC) non empty TarskiGeometryStruct;
end;
theorem :: GTARSKI3:138
for S being (RE') (TE) (IE) (SC) non empty TarskiGeometryStruct holds
S is (RE);
registration
cluster (FS') for (TE) (IE) (SC) non empty TarskiGeometryStruct;
end;
theorem :: GTARSKI3:139
for S being (TE) (IE) (SC) (FS') non empty TarskiGeometryStruct holds
S is (RE);
theorem :: GTARSKI3:140
for S being (TE) (IE) (SC) (FS') non empty TarskiGeometryStruct holds
S is (FS);
begin :: Main results and Corollaries
::$N Main results
registration
cluster (RE) (TE) (FS) -> (FS') for TarskiGeometryStruct;
end;
registration
cluster (TE) (IE) (SC) (FS') -> (FS) for non empty TarskiGeometryStruct;
end;
registration
cluster (TE) (IE) (SC) (FS') -> (RE) for non empty TarskiGeometryStruct;
end;
registration
cluster (TE) (IE) (SC) (FS') -> satisfying_SAS
for non empty TarskiGeometryStruct;
end;
registration
cluster (RE) (TE) (IE) (SC) (FS) (IB) (Pa) (Lo2) (Up2) (Eu) (Co)
for non empty TarskiGeometryStruct;
end;
definition
mode Makarios_CE2 is (RE) (TE) (IE) (SC) (FS) (IB) (Pa) (Lo2) (Up2)
(Eu) (Co) non empty TarskiGeometryStruct;
end;
definition
mode Makarios_CE'2 is (TE) (IE) (SC) (FS') (IB) (Pa) (Lo2) (Up2)
(Eu) (Co) non empty TarskiGeometryStruct;
end;
theorem :: GTARSKI3:141
for TP being Makarios_CE2 holds TP is Makarios_CE'2;
theorem :: GTARSKI3:142
for TP being Makarios_CE'2 holds TP is Makarios_CE2;
theorem :: GTARSKI3:143
for TP being Makarios_CE2 holds
TP is satisfying_Tarski-model &
TP is satisfying_Lower_Dimension_Axiom &
TP is satisfying_Upper_Dimension_Axiom &
TP is satisfying_Euclid_Axiom &
TP is satisfying_Continuity_Axiom;
theorem :: GTARSKI3:144
for TP being Makarios_CE'2 holds
TP is satisfying_Tarski-model &
TP is satisfying_Lower_Dimension_Axiom &
TP is satisfying_Upper_Dimension_Axiom &
TP is satisfying_Euclid_Axiom &
TP is satisfying_Continuity_Axiom;