:: by Roland Coghetto and Adam Grabowski

::

:: Received June 30, 2016

:: Copyright (c) 2016-2017 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))

u = (((r ^2) - (s ^2)) - (t ^2)) / (- ((2 * s) * t))

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)

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;

definition

let n be Nat;

the naturally_generated TarskiExtension of Euclid n is MetrTarskiStr ;

end;
func TarskiEuclidSpace n -> MetrTarskiStr equals :: GTARSKI2:def 1

the naturally_generated TarskiExtension of Euclid n;

coherence the naturally_generated TarskiExtension of Euclid n;

the naturally_generated TarskiExtension of Euclid n is MetrTarskiStr ;

:: deftheorem defines TarskiEuclidSpace GTARSKI2:def 1 :

for n being Nat holds TarskiEuclidSpace n = the naturally_generated TarskiExtension of Euclid n;

for n being Nat holds TarskiEuclidSpace n = the naturally_generated TarskiExtension of Euclid n;

registration

coherence

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

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

registration

let n be Nat;

coherence

( TarskiEuclidSpace n is Reflexive & TarskiEuclidSpace n is symmetric & TarskiEuclidSpace n is discerning ) ;

end;
coherence

( TarskiEuclidSpace n is Reflexive & TarskiEuclidSpace n is symmetric & TarskiEuclidSpace n is discerning ) ;

definition

let n be Nat;

let P be POINT of (TarskiEuclidSpace n);

coherence

P is Element of (TOP-REAL n)

end;
let P be POINT of (TarskiEuclidSpace n);

coherence

P is Element of (TOP-REAL n)

proof end;

:: deftheorem defines Tn2TR GTARSKI2:def 3 :

for n being Nat

for P being POINT of (TarskiEuclidSpace n) holds Tn2TR P = P;

for n being Nat

for P being POINT of (TarskiEuclidSpace n) holds Tn2TR P = P;

definition
end;

:: deftheorem defines Tn2TR GTARSKI2:def 4 :

for P being POINT of TarskiEuclid2Space holds Tn2TR P = P;

for P being POINT of TarskiEuclid2Space holds Tn2TR P = P;

:: deftheorem defines Tn2E GTARSKI2:def 5 :

for P being POINT of TarskiEuclid2Space holds Tn2E P = P;

for P being POINT of TarskiEuclid2Space holds Tn2E P = P;

:: deftheorem defines Tn2R GTARSKI2:def 6 :

for P being POINT of TarskiEuclid2Space holds Tn2R P = P;

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

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

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

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

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

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

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

( between p,q,r iff Tn2TR q in LSeg ((Tn2TR p),(Tn2TR r)) )

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 )

( a = b & c = d )

proof end;

theorem :: GTARSKI2:26

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

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

( (dist (a,b)) ^2 = (dist (c,d)) ^2 iff a,b equiv c,d )

proof end;

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

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

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

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)

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)

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

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)

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

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

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

between p,r,s

proof end;

ThPasch: TarskiEuclid2Space is satisfying_Pasch

proof end;

registration

( 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;

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;

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)

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

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

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

( 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 ;

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

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;

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

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

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

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

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

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 )

( not between a,b,c & not between b,c,a & not between c,a,b )

proof end;

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

between c,a,b

proof end;

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 )

ex x, y being Element of TarskiEuclid2Space st

( between a,b,x & between a,c,y & between x,t,y )

proof end;

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

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

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

end;

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;

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

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

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;

:: Lower dimension axiom