:: Tarski Geometry Axioms -- Part {II}
:: by Roland Coghetto and Adam Grabowski
::
:: Received June 30, 2016
:: Copyright (c) 2016-2021 Association of Mizar Users

theorem Th1: :: 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))

proof end;

theorem THJE: :: GTARSKI2:2

for n being Nat
for u, v being Element of (TOP-REAL n) holds u + (0 * v) = u

proof end;

theorem THJC: :: GTARSKI2:3

for n being Nat
for r, s being Real
for 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)

proof end;

theorem THJD: :: GTARSKI2:4

for r, s being Real st 0 < r & 0 < s holds
( 0 <= r / (r + s) & r / (r + s) <= 1 )

proof end;

theorem Th2: :: GTARSKI2:5

for a being Real holds cos ((3 * PI) - a) = - (cos a)

proof end;

theorem THSD2: :: GTARSKI2:6

for n being Nat
for a, b, c being Element of (TOP-REAL n) st a - c = b - c holds
a = b

proof end;

theorem ThWW: :: GTARSKI2:7

for n being Nat
for a, b, c being Element of (TOP-REAL n) holds (c - a) - (b - a) = c - b

proof end;

theorem THYQ: :: GTARSKI2:8

for a, b, c, d being Real holds dist (|[a,b]|,|[c,d]|) = sqrt (((a - c) ^2) + ((b - d) ^2))

proof end;

theorem THY1: :: GTARSKI2:9

dist (|[0,0]|,|[1,0]|) = 1

proof end;

theorem THY2: :: GTARSKI2:10

dist (|[0,0]|,|[0,1]|) = 1

proof end;

theorem THY3: :: GTARSKI2:11

dist (|[1,0]|,|[0,1]|) = sqrt 2

proof end;

definition

let n be Nat;

func TarskiEuclidSpace n -> MetrTarskiStr equals :: GTARSKI2:def 1
the naturally_generated TarskiExtension of Euclid n;

coherence
the naturally_generated TarskiExtension of Euclid n is MetrTarskiStr ;

end;

:: deftheorem defines TarskiEuclidSpace GTARSKI2:def 1 :
for n being Nat holds TarskiEuclidSpace n = the naturally_generated TarskiExtension of Euclid n;

definition

func TarskiEuclid2Space -> MetrTarskiStr equals :: GTARSKI2:def 2
TarskiEuclidSpace 2;

coherence
TarskiEuclidSpace 2 is MetrTarskiStr ;

end;

:: deftheorem defines TarskiEuclid2Space GTARSKI2:def 2 :
TarskiEuclid2Space = TarskiEuclidSpace 2;

registration

let n be Nat;

cluster TarskiEuclidSpace n -> non empty ;

coherence
not TarskiEuclidSpace n is empty ;

end;

registration

cluster TarskiEuclid2Space -> Reflexive discerning symmetric ;

coherence
( TarskiEuclid2Space is Reflexive & TarskiEuclid2Space is symmetric & TarskiEuclid2Space is discerning ) ;

end;

registration

let n be Nat;

cluster TarskiEuclidSpace n -> Reflexive discerning symmetric ;

coherence
( TarskiEuclidSpace n is Reflexive & TarskiEuclidSpace n is symmetric & TarskiEuclidSpace n is 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;

coherence
P is Element of (TOP-REAL n)

proof end;

end;

:: deftheorem defines Tn2TR GTARSKI2:def 3 :
for n being Nat
for P being POINT of (TarskiEuclidSpace n) holds Tn2TR P = P;

definition

let P be POINT of TarskiEuclid2Space;

func Tn2TR P -> Element of (TOP-REAL 2) equals :: GTARSKI2:def 4
P;

coherence
P is Element of (TOP-REAL 2)

proof end;

end;

:: deftheorem defines Tn2TR GTARSKI2:def 4 :
for P being POINT of TarskiEuclid2Space holds Tn2TR P = P;

definition

let P be POINT of TarskiEuclid2Space;

func Tn2E P -> Point of (Euclid 2) equals :: GTARSKI2:def 5
P;

coherence
P is Point of (Euclid 2)

proof end;

end;

:: deftheorem defines Tn2E GTARSKI2:def 5 :
for P being POINT of TarskiEuclid2Space holds Tn2E P = P;

definition

let P be POINT of TarskiEuclid2Space;

func Tn2R P -> Element of REAL 2 equals :: GTARSKI2:def 6
P;

coherence
P is Element of REAL 2

proof end;

end;

:: deftheorem defines Tn2R GTARSKI2:def 6 :
for P being POINT of TarskiEuclid2Space holds Tn2R P = P;

theorem ThEquiv: :: GTARSKI2:12

for n being Nat
for p, q being POINT of (TarskiEuclidSpace n)
for 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).| )

proof end;

theorem ThLawOfCosines: :: 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)))))

proof end;

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) )

proof end;

theorem ThConv: :: GTARSKI2:15

for n being Nat
for p, q being Element of (TarskiEuclidSpace n)
for p1, q1 being Element of (Euclid n) st p = p1 & q = q1 holds
dist (p,q) = dist (p1,q1)

proof end;

theorem ThConv2: :: 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))

proof end;

theorem ThConv3: :: GTARSKI2:17

for A, B being POINT of TarskiEuclid2Space holds
( dist (A,B) = |.((Tn2TR A) - (Tn2TR B)).| & dist (A,B) = |.((Tn2R A) - (Tn2R B)).| )

proof end;

theorem ThConv4: :: 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 )

proof end;

theorem ThConv5: :: 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)) )

proof end;

theorem ThConv6: :: GTARSKI2:20

for p, q, r being POINT of TarskiEuclid2Space holds
( between p,q,r iff Tn2TR q in LSeg ((Tn2TR p),(Tn2TR r)) )

proof end;

theorem ThConv7: :: GTARSKI2:21

for a, b being Point of TarskiEuclid2Space holds
( between a,a,b & between a,b,b )

proof end;

theorem ThConv7bis: :: GTARSKI2:22

for a, b, c being Point of TarskiEuclid2Space st between a,b,c holds
between c,b,a

proof end;

theorem ThConv7ter: :: GTARSKI2:23

for a, b being Point of TarskiEuclid2Space st between a,b,a holds
a = b

proof end;

theorem ThEgal: :: GTARSKI2:24

for a, b being POINT of TarskiEuclid2Space holds
( a = b iff dist (a,b) = 0 )

proof end;

theorem ThNull: :: GTARSKI2:25

for a, b, c, d being POINT of TarskiEuclid2Space st (dist (a,b)) + (dist (c,d)) = 0 holds
( a = b & c = d )

proof end;

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) ) ) by GTARSKI1:def 15;

theorem ThConv8: :: 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)) )

proof end;

theorem ThConv9: :: 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 )

proof end;

theorem :: GTARSKI2:29

for a being Point of TarskiEuclid2Space holds between a,a,a by ThConv7;

ThCongruenceSymmetry: TarskiEuclid2Space is satisfying_CongruenceSymmetry

proof end;

ThCongruenceEquivalenceRelation: TarskiEuclid2Space is satisfying_CongruenceEquivalenceRelation

proof end;

ThCongruenceIdentity: TarskiEuclid2Space is satisfying_CongruenceIdentity

proof end;

ThSegmentConstruction: TarskiEuclid2Space is satisfying_SegmentConstruction

proof end;

ThSAS: TarskiEuclid2Space is satisfying_SAS

proof end;

ThBetweennessIdentity: TarskiEuclid2Space is satisfying_BetweennessIdentity

proof end;

theorem THQQ: :: GTARSKI2:30

OASpace (TOP-REAL 2) is OAffinSpace

proof end;

theorem THSS: :: 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 being Point of (TOP-REAL 2) st
( u = a & v = c & b in LSeg (u,v) ) ) )

proof end;

theorem THSS2: :: GTARSKI2:32

for a, b, c being Element of (OASpace (TOP-REAL 2)) holds
( Mid a,b,c iff ex u, v being Point of (TOP-REAL 2) st
( u = a & v = c & b in LSeg (u,v) ) )

proof end;

theorem THSS3: :: GTARSKI2:33

for a, b, c being Element of (OASpace (TOP-REAL 2))
for ap, bp, cp being POINT of TarskiEuclid2Space st a = ap & b = bp & c = cp holds
( Mid a,b,c iff between ap,bp,cp )

proof end;

theorem THORANGE: :: 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)

proof end;

theorem THORANGE2: :: 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)

proof end;

theorem THPOIRE: :: 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

proof end;

theorem THNOIX: :: 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)

proof end;

theorem THNOIX2: :: 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

proof end;

theorem THNOIX3: :: 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

proof end;

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

proof end;

ThPasch: TarskiEuclid2Space is satisfying_Pasch

proof end;

registration

cluster TarskiEuclid2Space -> satisfying_CongruenceSymmetry satisfying_CongruenceEquivalenceRelation satisfying_CongruenceIdentity satisfying_SegmentConstruction satisfying_SAS satisfying_BetweennessIdentity satisfying_Pasch ;

coherence
( TarskiEuclid2Space is satisfying_CongruenceSymmetry & TarskiEuclid2Space is satisfying_CongruenceEquivalenceRelation & TarskiEuclid2Space is satisfying_CongruenceIdentity & TarskiEuclid2Space is satisfying_SegmentConstruction & TarskiEuclid2Space is satisfying_SAS & TarskiEuclid2Space is satisfying_BetweennessIdentity & TarskiEuclid2Space is satisfying_Pasch ) by ThCongruenceSymmetry, ThCongruenceEquivalenceRelation, ThCongruenceIdentity, ThSegmentConstruction, ThSAS, ThBetweennessIdentity, ThPasch;

end;

registration

cluster TarskiEuclid2Space -> satisfying_Tarski-model ;

coherence
TarskiEuclid2Space is satisfying_Tarski-model ;

end;

theorem ThAZ9: :: GTARSKI2:41

for P, Q, R being Point of (TOP-REAL 2)
for L being Element of line_of_REAL 2 st P in L & Q in L & R in L & not P in LSeg (Q,R) & not Q in LSeg (R,P) holds
R in LSeg (P,Q)

proof end;

theorem ThConvAG: :: GTARSKI2:42

for a, b, c being Element of TarskiEuclid2Space st Tn2TR b in LSeg ((Tn2TR a),(Tn2TR c)) holds
ex jj being Real st
( 0 <= jj & jj <= 1 & (Tn2TR b) - (Tn2TR a) = jj * ((Tn2TR c) - (Tn2TR a)) )

proof end;

theorem :: GTARSKI2:43

for n being Nat
for a, b, c being Element of (TarskiEuclidSpace n) st Tn2TR b in LSeg ((Tn2TR a),(Tn2TR c)) holds
ex jj being Real st
( 0 <= jj & jj <= 1 & (Tn2TR b) - (Tn2TR a) = jj * ((Tn2TR c) - (Tn2TR a)) )

proof end;

theorem ThConvAGI: :: GTARSKI2:44

for a, b, c being Element of TarskiEuclid2Space st ex jj being Real st
( 0 <= jj & jj <= 1 & (Tn2TR b) - (Tn2TR a) = jj * ((Tn2TR c) - (Tn2TR a)) ) holds
Tn2TR b in LSeg ((Tn2TR a),(Tn2TR c))

proof end;

definition

let S be TarskiGeometryStruct ;

attr S is satisfying_A8 means :: GTARSKI2:def 7
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
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 & not between a,b,c & not between b,c,a holds
between c,a,b;

attr S is satisfying_A10 means :: GTARSKI2:def 9
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
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;

:: deftheorem defines satisfying_A8 GTARSKI2:def 7 :
for S being TarskiGeometryStruct holds
( S is satisfying_A8 iff ex a, b, c being POINT of S st
( not between a,b,c & not between b,c,a & not between c,a,b ) );

:: deftheorem defines satisfying_A9 GTARSKI2:def 8 :
for S being TarskiGeometryStruct holds
( S is satisfying_A9 iff 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 & not between a,b,c & not between b,c,a holds
between c,a,b );

:: deftheorem defines satisfying_A10 GTARSKI2:def 9 :
for S being TarskiGeometryStruct holds
( S is satisfying_A10 iff 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 ) );

:: deftheorem defines satisfying_A11 GTARSKI2:def 10 :
for S being TarskiGeometryStruct holds
( S is satisfying_A11 iff 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 );

notation

let S be TarskiGeometryStruct ;
synonym satisfying_Lower_Dimension_Axiom S for satisfying_A8 ;
synonym satisfying_Upper_Dimension_Axiom S for satisfying_A9 ;
synonym satisfying_Euclid_Axiom S for satisfying_A10 ;
synonym satisfying_Continuity_Axiom S for satisfying_A11 ;

end;

:: Axiom A8 -- Lower Dimension Axiom
:: Lower dimension axiom

theorem AxiomA8: :: GTARSKI2:45

ex a, b, c being Point of TarskiEuclid2Space st
( not between a,b,c & not between b,c,a & not between c,a,b )

proof end;

:: Axiom A9 -- Upper Dimension Axiom
:: Upper dimension axiom

theorem AxiomA9: :: GTARSKI2:46

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 & not between a,b,c & not between b,c,a holds
between c,a,b

proof end;

:: Axiom A10 -- Axiom of Euclid
:: Axiom of Euclid

theorem AxiomA10: :: GTARSKI2:47

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 )

proof end;

:: Axiom schema of continuity

theorem AxiomA11: :: GTARSKI2:48

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

proof end;

registration

cluster TarskiEuclid2Space -> satisfying_Lower_Dimension_Axiom satisfying_Upper_Dimension_Axiom satisfying_Euclid_Axiom satisfying_Continuity_Axiom ;

coherence
( TarskiEuclid2Space is satisfying_A8 & TarskiEuclid2Space is satisfying_A9 & TarskiEuclid2Space is satisfying_A10 & TarskiEuclid2Space is satisfying_A11 ) by AxiomA8, AxiomA9, AxiomA10, AxiomA11;

end;

theorem :: GTARSKI2:49

for X, Y being Subset of TarskiEuclid2Space
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 & not X = {a} holds
X is empty

proof end;

theorem :: GTARSKI2:50

for X, Y being Subset of TarskiEuclid2Space
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 ) & not X is empty & not Y is 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)) )

proof end;