:: Tarski Geometry Axioms -- Part {II}
:: by Roland Coghetto and Adam Grabowski
::
:: Received June 30, 2016
:: Copyright (c) 2016 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 TARSKI, NUMBERS, SUBSET_1, COMPLEX1, REAL_1, RELAT_1, CARD_1,
ARYTM_1, SUPINF_2, XXREAL_2, NAT_1, ARYTM_3, SQUARE_1, XXREAL_0,
XBOOLE_0, RLTOPSP1, PRE_TOPC, MCART_1, EUCLID, INCSP_1, METRIC_1,
SIN_COS, COMPLEX2, PROJPL_1, GTARSKI1, PBOOLE, FINSEQ_2, QC_LANG1,
GTARSKI2, FUNCT_1, ROUGHS_4, RELAT_2, LATTICE3, EUCLIDLP, EUCLID12,
MEMBERED, ORDINAL2, ANALOAF, PASCH, RLVECT_1, ZFMISC_1, DIRAF, PENCIL_1,
PARSP_1;
notations XBOOLE_0, ORDINAL1, SUBSET_1, XXREAL_2, MEMBERED, TARSKI, XCMPLX_0,
NUMBERS, XREAL_0, COMPLEX1, METRIC_1, STRUCT_0, FINSEQ_2, SQUARE_1,
RVSUM_1, PRE_TOPC, XXREAL_0, RLVECT_1, SIN_COS, EUCLID_3, EUCLID_6,
GTARSKI1, EUCLID, BINOP_1, TOPREAL6, ANALOAF, DIRAF, PASCH, EUCLID12,
EUCLIDLP, EUCLID_4, RLTOPSP1;
constructors SQUARE_1, COMPLEX1, MONOID_0, SIN_COS, EUCLID_3, TOPREAL6,
GTARSKI1, SEQ_4, PASCH, DIRAF, EUCLID12, EUCLID_4;
registrations EUCLIDLP, RLTOPSP1, MONOID_0, RELSET_1, XXREAL_0, XREAL_0,
EUCLID, VALUED_0, SQUARE_1, ORDINAL1, SIN_COS, GTARSKI1, XCMPLX_0,
RLVECT_1, STRUCT_0, ZFMISC_1, ANALOAF, XXREAL_2, MEMBERED;
requirements BOOLE, SUBSET, NUMERALS, ARITHM, REAL;
begin :: Preliminaries
theorem :: GTARSKI2:1
for r,s,t,u being Real st s <> 0 & t <> 0 &
r^2 = s^2 + t^2 - 2*s*t*u holds u = (r^2 - s^2 - t^2)/(-2*s*t);
theorem :: GTARSKI2:2
for n being Nat
for u,v being Element of TOP-REAL n holds u + 0 * v = u;
theorem :: GTARSKI2:3
for n being Nat
for r,s being Real, u,v,w being Element of TOP-REAL n st
r * u - r * v = s * w - s * u holds (r + s) * u = r * v + s * w;
theorem :: GTARSKI2:4
for r,s being Real st 0 < r & 0 < s holds 0 <= r / (r+s) <= 1;
theorem :: GTARSKI2:5
for a being Real holds cos (3*PI - a) = -cos a;
theorem :: GTARSKI2:6
for n being Nat
for a,b,c being Element of TOP-REAL n st a - c = b - c holds a = b;
theorem :: GTARSKI2:7
for n being Nat
for a,b,c being Element of TOP-REAL n holds
c - a - (b - a) = c - b;
theorem :: GTARSKI2:8
for a,b,c,d being Real holds dist(|[a,b]|,|[c,d]|) = sqrt ((a-c)^2+(b-d)^2);
theorem :: GTARSKI2:9
dist(|[0,0]|,|[1,0]|) = 1;
theorem :: GTARSKI2:10
dist(|[0,0]|,|[0,1]|) = 1;
theorem :: GTARSKI2:11
dist(|[1,0]|,|[0,1]|) = sqrt 2;
definition let n be Nat;
func TarskiEuclidSpace n -> MetrTarskiStr equals
:: GTARSKI2:def 1
the naturally_generated TarskiExtension of Euclid n;
end;
definition
func TarskiEuclid2Space -> MetrTarskiStr equals
:: GTARSKI2:def 2
TarskiEuclidSpace 2;
end;
begin
registration let n be Nat;
cluster TarskiEuclidSpace n -> non empty;
end;
registration
cluster TarskiEuclid2Space -> Reflexive symmetric discerning;
end;
registration let n be Nat;
cluster TarskiEuclidSpace n -> Reflexive symmetric discerning;
end;
definition
let n be Nat;
let P be POINT of TarskiEuclidSpace n;
func #P -> Element of TOP-REAL n equals
:: GTARSKI2:def 3
P;
end;
definition
let P be POINT of TarskiEuclid2Space;
func #P -> Element of TOP-REAL 2 equals
:: GTARSKI2:def 4
P;
end;
definition
let P be POINT of TarskiEuclid2Space;
func @P -> Point of Euclid 2 equals
:: GTARSKI2:def 5
P;
end;
definition
let P be POINT of TarskiEuclid2Space;
func %P -> Element of REAL 2 equals
:: GTARSKI2:def 6
P;
end;
theorem :: GTARSKI2:12
for n being Nat
for p,q being POINT of TarskiEuclidSpace n,
p1,q1 being Element of TOP-REAL n st p = p1 & q = q1 holds
dist(p,q) = (Pitag_dist n).(p1, q1) & dist(p,q) = |. p1 - q1 .|;
theorem :: GTARSKI2:13
for a, b, c, x being POINT of TarskiEuclid2Space holds
(dist(c,a))^2 = (dist(a,b))^2 + (dist(b,c))^2 - 2 * dist(a,b) *
dist(b,c) * cos angle( #a, #b, #c);
theorem :: GTARSKI2:14
for a,b,c,d,e,f,g being POINT of TarskiEuclid2Space st
#a, #b, #c is_a_triangle & angle( #a, #b, #c) < PI &
angle( #e, #c, #a) = angle( #b,#c,#a) / 3 &
angle( #c, #a, #e) = angle( #c, #a, #b) / 3 &
angle( #a, #b, #f) = angle( #a, #b, #c) / 3 &
angle( #f, #a, #b) = angle( #c, #a, #b) / 3 &
angle( #b, #c, #g) = angle( #b, #c, #a) / 3 &
angle( #g, #b, #c) = angle( #a, #b, #c) / 3 holds
dist(f,e) = dist(g,f) & dist(f,e) = dist(e,g) & dist(g,f) = dist(e,g);
theorem :: GTARSKI2:15
for n being Nat
for p,q being Element of TarskiEuclidSpace n,
p1, q1 being Element of Euclid n st p = p1 & q = q1 holds
dist(p,q) = dist(p1, q1);
theorem :: GTARSKI2:16
for p,q being POINT of TarskiEuclid2Space holds
dist(p,q) = sqrt((( #p)`1-( #q)`1)^2 + ((( #p)`2-( #q)`2)^2));
theorem :: GTARSKI2:17
for A,B being POINT of TarskiEuclid2Space holds
dist(A,B) = |. #A - #B .| & dist(A,B) = |. %A - %B .|;
theorem :: GTARSKI2:18
for a,b,c,d being POINT of TarskiEuclid2Space holds
|. #a - #b .| = |. #c - #d .| iff a,b equiv c,d;
theorem :: GTARSKI2:19
for p,q,r being POINT of TarskiEuclid2Space holds
p is_Between q,r iff #p in LSeg( #q, #r );
reserve n for Nat;
theorem :: GTARSKI2:20
for p,q,r being POINT of TarskiEuclid2Space holds
between p,q,r iff #q in LSeg( #p, #r );
theorem :: GTARSKI2:21
for a,b being Point of TarskiEuclid2Space holds
between a,a,b & between a,b,b;
theorem :: GTARSKI2:22
for a,b,c being Point of TarskiEuclid2Space st
between a,b,c holds between c,b,a;
theorem :: GTARSKI2:23
for a,b being Point of TarskiEuclid2Space st between a,b,a holds a = b;
theorem :: GTARSKI2:24
for a, b being POINT of TarskiEuclid2Space holds a = b iff dist(a,b) = 0;
theorem :: GTARSKI2:25
for a,b,c,d being POINT of TarskiEuclid2Space st
dist(a,b) + dist(c,d) = 0 holds a = b & c = d;
theorem :: GTARSKI2:26
for a,b,c,a1,b1,c1 being POINT of TarskiEuclid2Space holds
a,b,c cong a1,b1,c1 iff (dist(a,b) = dist(a1,b1) &
dist(a,c) = dist(a1,c1) & dist(b,c) = dist(b1,c1));
theorem :: GTARSKI2:27
for a,b,c being POINT of TarskiEuclid2Space holds
between a,b,c iff dist(a,c) = dist(a,b) + dist(b,c);
theorem :: GTARSKI2:28
for a,b,c,d being POINT of TarskiEuclid2Space holds
dist(a,b)^2 = dist(c,d)^2 iff a,b equiv c,d;
theorem :: GTARSKI2:29
for a being Point of TarskiEuclid2Space holds between a,a,a;
begin :: Ordered Affine Space Generated by TOP-REAL 2
theorem :: GTARSKI2:30
OASpace(TOP-REAL 2) is OAffinSpace;
theorem :: GTARSKI2:31
for a,b,c being Element of OASpace(TOP-REAL 2) holds
Mid a,b,c iff a = b or b = c or
(ex u,v be Point of TOP-REAL 2 st u = a & v = c & b in LSeg(u,v));
theorem :: GTARSKI2:32
for a,b,c being Element of OASpace(TOP-REAL 2) holds
Mid a,b,c iff
(ex u,v be Point of TOP-REAL 2 st u = a & v = c & b in LSeg(u,v));
theorem :: GTARSKI2:33
for a,b,c being Element of OASpace(TOP-REAL 2),
ap,bp,cp being POINT of TarskiEuclid2Space st
a = ap & b = bp & c = cp holds Mid a,b,c iff between ap,bp,cp;
begin
theorem :: GTARSKI2:34
for A,B,C,D being Element of TOP-REAL 2 st
B in LSeg(A,C) & C in LSeg(A,D) holds B in LSeg(A,D);
theorem :: GTARSKI2:35
for A,B,C,D being Element of TOP-REAL 2 st
B <> C & B in LSeg(A,C) & C in LSeg(B,D) holds C in LSeg(A,D);
theorem :: GTARSKI2:36
for p,q,r,s being Point of TarskiEuclid2Space st
between p,q,r & between p,r,s holds between p,q,s;
theorem :: GTARSKI2:37
for A,B,C,D being Point of TOP-REAL 2 st
B in LSeg(A,C) & D in LSeg(A,B) holds
B in LSeg(D,C);
theorem :: GTARSKI2:38
for p,q,r,s being Point of TarskiEuclid2Space st
between p,q,r & between p,s,q holds between s,q,r;
theorem :: GTARSKI2:39
for p,q,r,s being Point of TarskiEuclid2Space st
q <> r & between p,q,r & between q,r,s holds between p,q,s;
theorem :: GTARSKI2:40
for p,q,r,s being Point of TarskiEuclid2Space st
q <> r & between p,q,r & between q,r,s holds between p,r,s;
registration
cluster TarskiEuclid2Space -> satisfying_CongruenceSymmetry
satisfying_CongruenceEquivalenceRelation
satisfying_CongruenceIdentity
satisfying_SegmentConstruction
satisfying_SAS
satisfying_BetweennessIdentity
satisfying_Pasch;
end;
registration
cluster TarskiEuclid2Space -> satisfying_Tarski-model;
end;
begin :: Preparatory Work for The Rest of Tarski's Axioms
theorem :: GTARSKI2:41
for P,Q,R being Point of TOP-REAL 2, L being Element of line_of_REAL 2
st P in L & Q in L & R in L holds P in LSeg(Q,R) or
Q in LSeg(R,P) or R in LSeg(P,Q);
theorem :: GTARSKI2:42
for a,b,c being Element of TarskiEuclid2Space holds
#b in LSeg ( #a,#c) implies
ex jj being Real st 0 <= jj & jj <= 1 & #b - #a = jj * ( #c - #a);
theorem :: GTARSKI2:43
for n being Nat
for a,b,c being Element of TarskiEuclidSpace n holds
#b in LSeg ( #a,#c) implies
ex jj being Real st 0 <= jj & jj <= 1 & #b - #a = jj * ( #c - #a);
theorem :: GTARSKI2:44
for a,b,c being Element of TarskiEuclid2Space holds
(ex jj being Real st 0 <= jj & jj <= 1 & #b - #a = jj * ( #c - #a))
implies
#b in LSeg ( #a,#c);
begin :: Four Remaining Axioms of Tarski
definition let S be TarskiPlane;
attr S is satisfying_A8 means
:: GTARSKI2:def 7 ::: Axiom A8
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 satisfying_A9 means
:: GTARSKI2:def 8 ::: Axiom A9
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 satisfying_A10 means
:: GTARSKI2:def 9 ::: Axiom A10
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 satisfying_A11 means
:: GTARSKI2:def 10 ::: Axiom A11
for X,Y being Subset of S 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);
end;
notation let S be TarskiPlane;
synonym S is satisfying_Lower_Dimension_Axiom for S is satisfying_A8;
synonym S is satisfying_Upper_Dimension_Axiom for S is satisfying_A9;
synonym S is satisfying_Euclid_Axiom for S is satisfying_A10;
synonym S is satisfying_Continuity_Axiom for S is satisfying_A11;
end;
:: Axiom A8 -- Lower Dimension Axiom
::$N Lower dimension axiom
theorem :: GTARSKI2:45 :: Axiom A8
ex a,b,c being Point of TarskiEuclid2Space st
not between a,b,c & not between b,c,a & not between c,a,b;
:: Axiom A9 -- Upper Dimension Axiom
::$N Upper dimension axiom
theorem :: GTARSKI2:46 :: Axiom A9
for a,b,c,p,q being Point of TarskiEuclid2Space 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;
:: Axiom A10 -- Axiom of Euclid
::$N Axiom of Euclid
theorem :: GTARSKI2:47 :: Axiom A10 -- Axiom of Euclid
for a,b,c,d,t being Element of TarskiEuclid2Space st
between a,d,t & between b,d,c & a <> d holds
ex x,y being Element of TarskiEuclid2Space st
between a,b,x & between a,c,y & between x,t,y;
begin :: Axiom A11 -- Axiom Schema of Continuity
::$N Axiom schema of continuity
theorem :: GTARSKI2:48 :: Axiom A11
for X,Y being Subset of TarskiEuclid2Space st
(ex a being Element of TarskiEuclid2Space st
for x,y being Element of TarskiEuclid2Space st x in X & y in Y holds
between a,x,y) holds
(ex b being Element of TarskiEuclid2Space st
for x,y being Element of TarskiEuclid2Space st
x in X & y in Y holds between x,b,y);
registration
cluster TarskiEuclid2Space ->
satisfying_Lower_Dimension_Axiom satisfying_Upper_Dimension_Axiom
satisfying_Euclid_Axiom satisfying_Continuity_Axiom;
end;
begin :: Corrolaries
reserve X,Y for Subset of TarskiEuclid2Space;
theorem :: GTARSKI2:49
for a being Element of TarskiEuclid2Space st
(for x,y being Element of TarskiEuclid2Space st x in X & y in Y holds
between a,x,y) & a in Y holds X = {a} or X is empty;
theorem :: GTARSKI2:50
for a being Element of TarskiEuclid2Space st
(for x,y being Element of TarskiEuclid2Space st x in X & y in Y holds
between a,x,y) & X is non empty & Y is non empty &
(X is trivial implies X <> {a}) holds
ex b being Element of TarskiEuclid2Space st
X c= Line( #a, #b) & Y c= Line( #a, #b);