:: Tarski Geometry Axioms -- Part {II} :: by Roland Coghetto and Adam Grabowski :: :: Received June 30, 2016 :: Copyright (c) 2016-2021 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 Tn2TR P -> Element of TOP-REAL n equals :: GTARSKI2:def 3 P; end; definition let P be POINT of TarskiEuclid2Space; func Tn2TR P -> Element of TOP-REAL 2 equals :: GTARSKI2:def 4 P; end; definition let P be POINT of TarskiEuclid2Space; func Tn2E P -> Point of Euclid 2 equals :: GTARSKI2:def 5 P; end; definition let P be POINT of TarskiEuclid2Space; func Tn2R 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 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(Tn2TR a, Tn2TR b, Tn2TR c); theorem :: GTARSKI2:14 for a,b,c,e,f,g being POINT of TarskiEuclid2Space st Tn2TR a, Tn2TR b, Tn2TR c is_a_triangle & angle(Tn2TR a, Tn2TR b, Tn2TR c) < PI & angle(Tn2TR e, Tn2TR c, Tn2TR a) = angle(Tn2TR b,Tn2TR c,Tn2TR a) / 3 & angle(Tn2TR c, Tn2TR a, Tn2TR e) = angle(Tn2TR c, Tn2TR a, Tn2TR b) / 3 & angle(Tn2TR a, Tn2TR b, Tn2TR f) = angle(Tn2TR a, Tn2TR b, Tn2TR c) / 3 & angle(Tn2TR f, Tn2TR a, Tn2TR b) = angle(Tn2TR c, Tn2TR a, Tn2TR b) / 3 & angle(Tn2TR b, Tn2TR c, Tn2TR g) = angle(Tn2TR b, Tn2TR c, Tn2TR a) / 3 & angle(Tn2TR g, Tn2TR b, Tn2TR c) = angle(Tn2TR a, Tn2TR b, Tn2TR 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(((Tn2TR p)`1-(Tn2TR q)`1)^2 + (((Tn2TR p)`2-(Tn2TR q)`2)^2)); theorem :: GTARSKI2:17 for A,B being POINT of TarskiEuclid2Space holds dist(A,B) = |. Tn2TR A - Tn2TR B .| & dist(A,B) = |. Tn2R A - Tn2R B .|; theorem :: GTARSKI2:18 for a,b,c,d being POINT of TarskiEuclid2Space holds |. Tn2TR a - Tn2TR b .| = |. Tn2TR c - Tn2TR 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 Tn2TR p in LSeg(Tn2TR q, Tn2TR r); reserve n for Nat; theorem :: GTARSKI2:20 for p,q,r being POINT of TarskiEuclid2Space holds between p,q,r iff Tn2TR q in LSeg(Tn2TR p, Tn2TR 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 Tn2TR b in LSeg (Tn2TR a,Tn2TR c) implies ex jj being Real st 0 <= jj & jj <= 1 & Tn2TR b - Tn2TR a = jj * (Tn2TR c - Tn2TR a); theorem :: GTARSKI2:43 for n being Nat for a,b,c being Element of TarskiEuclidSpace n holds Tn2TR b in LSeg (Tn2TR a, Tn2TR c) implies ex jj being Real st 0 <= jj <= 1 & Tn2TR b - Tn2TR a = jj * (Tn2TR c - Tn2TR a); theorem :: GTARSKI2:44 for a,b,c being Element of TarskiEuclid2Space holds (ex jj being Real st 0 <= jj & jj <= 1 & Tn2TR b - Tn2TR a = jj * (Tn2TR c - Tn2TR a)) implies Tn2TR b in LSeg (Tn2TR a,Tn2TR c); begin :: Four Remaining Axioms of Tarski definition let S be TarskiGeometryStruct; 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 TarskiGeometryStruct; 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(Tn2TR a, Tn2TR b) & Y c= Line(Tn2TR a, Tn2TR b);