:: Tarski Geometry Axioms -- Part {II}
:: by Roland Coghetto and Adam Grabowski
::
:: Copyright (c) 2016-2018 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 () 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 () 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 () 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 () 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 (,|[1,0]|) = 1
proof end;

theorem THY2: :: GTARSKI2:10
dist (,|[0,1]|) = 1
proof end;

theorem THY3: :: GTARSKI2:11
dist (|[1,0]|,|[0,1]|) = sqrt 2
proof end;

definition
let n be Nat;
coherence ;
end;

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

definition
coherence ;
end;

:: deftheorem defines TarskiEuclid2Space GTARSKI2:def 2 :

registration
let n be Nat;
coherence
not TarskiEuclidSpace n is empty
;
end;

registration
coherence ;
end;

registration
let n be Nat;
coherence ;
end;

definition
let n be Nat;
let P be POINT of ;
func Tn2TR P -> Element of () equals :: GTARSKI2:def 3
P;
coherence
P is Element of ()
proof end;
end;

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

definition
let P be POINT of TarskiEuclid2Space;
func Tn2TR P -> Element of () equals :: GTARSKI2:def 4
P;
coherence
P is Element of ()
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 () equals :: GTARSKI2:def 5
P;
coherence
P is Point of ()
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
for p1, q1 being Element of () st p = p1 & q = q1 holds
( dist (p,q) = () . (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 ((),(),()))))
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 ((),(),()) < PI & angle ((),(),()) = (angle ((),(),())) / 3 & angle ((),(),()) = (angle ((),(),())) / 3 & angle ((),(),()) = (angle ((),(),())) / 3 & angle ((),(),()) = (angle ((),(),())) / 3 & angle ((),(),()) = (angle ((),(),())) / 3 & angle ((),(),()) = (angle ((),(),())) / 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
for p1, q1 being Element of () 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 ((((() 1) - (() 1)) ^2) + (((() 2) - (() 2)) ^2))
proof end;

theorem ThConv3: :: GTARSKI2:17
for A, B being POINT of TarskiEuclid2Space holds
( dist (A,B) = |.(() - ()).| & dist (A,B) = |.((Tn2R A) - (Tn2R B)).| )
proof end;

theorem ThConv4: :: GTARSKI2:18
for a, b, c, d being POINT of TarskiEuclid2Space holds
( |.(() - ()).| = |.(() - ()).| 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 ((),()) )
proof end;

theorem ThConv6: :: GTARSKI2:20
for p, q, r being POINT of TarskiEuclid2Space holds
( between p,q,r iff Tn2TR q in LSeg ((),()) )
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:
proof end;

ThCongruenceEquivalenceRelation:
proof end;

ThCongruenceIdentity:
proof end;

ThSegmentConstruction:
proof end;

ThSAS:
proof end;

ThBetweennessIdentity:
proof end;

theorem THQQ: :: GTARSKI2:30
proof end;

theorem THSS: :: GTARSKI2:31
for a, b, c being Element of (OASpace ()) holds
( Mid a,b,c iff ( a = b or b = c or ex u, v being Point of () st
( u = a & v = c & b in LSeg (u,v) ) ) )
proof end;

theorem THSS2: :: GTARSKI2:32
for a, b, c being Element of (OASpace ()) holds
( Mid a,b,c iff ex u, v being Point of () st
( u = a & v = c & b in LSeg (u,v) ) )
proof end;

theorem THSS3: :: GTARSKI2:33
for a, b, c being Element of (OASpace ())
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 () 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 () 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 () 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:
proof end;

registration end;

theorem ThAZ9: :: GTARSKI2:41
for P, Q, R being Point of ()
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 ((),()) holds
ex jj being Real st
( 0 <= jj & jj <= 1 & () - () = jj * (() - ()) )
proof end;

theorem :: GTARSKI2:43
for n being Nat
for a, b, c being Element of st Tn2TR b in LSeg ((),()) holds
ex jj being Real st
( 0 <= jj & jj <= 1 & () - () = jj * (() - ()) )
proof end;

theorem ThConvAGI: :: GTARSKI2:44
for a, b, c being Element of TarskiEuclid2Space st ex jj being Real st
( 0 <= jj & jj <= 1 & () - () = jj * (() - ()) ) holds
Tn2TR b in LSeg ((),())
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 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 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 ((),()) & Y c= Line ((),()) )
proof end;