:: Tarski Geometry Axioms. {P}art {IV } -- Right angle
:: by Roland Coghetto and Adam Grabowski
::
:: Received March 11, 2019
:: Copyright (c) 2019-2026 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 INCSP_1, GTARSKI1, GTARSKI2, GTARSKI3, XXREAL_0, XBOOLE_0,
SUBSET_1, RVSUM_1, GTARSKI4;
notations GTARSKI1, GTARSKI2, STRUCT_0, GTARSKI3;
constructors GTARSKI2, GTARSKI3;
registrations GTARSKI1, GTARSKI3;
theorems GTARSKI1, GTARSKI3;
begin :: Preliminaries
reserve S for non empty satisfying_Tarski-model
TarskiGeometryStruct,
a,b,c,d,c9,x,y,z,p,q,q9 for POINT of S;
definition let S be non empty satisfying_CongruenceIdentity
satisfying_SegmentConstruction satisfying_BetweennessIdentity
satisfying_Pasch TarskiGeometryStruct;
let a,b be POINT of S;
redefine func Line (a,b); :: redefines Line (GTARSKI3, definition)
commutativity by GTARSKI3:83;
end;
LemmaA1: Collinear a,b,c implies c in Line (a,b)
proof
assume Collinear a,b,c; then
c in {x where x is POINT of S: Collinear a,b,x};
hence thesis by GTARSKI3:def 10;
end;
LemmaA2: x in Line(a,p) implies Collinear x,a,p
proof
assume x in Line(a,p);
then x in {y where y is POINT of S:Collinear a,p,y} by GTARSKI3:def 10;
then ex y be POINT of S st x = y & Collinear a,p,y;
hence thesis by GTARSKI3:45;
end;
theorem Prelim01:
for S being satisfying_CongruenceSymmetry
satisfying_CongruenceEquivalenceRelation satisfying_CongruenceIdentity
TarskiGeometryStruct for a,b,c,d being POINT of S st a,b equiv c,d
holds a,b equiv d,c & b,a equiv c,d & b,a equiv d,c & c,d equiv a,b &
d,c equiv a,b & c,d equiv b,a & d,c equiv b,a
proof
let S be satisfying_CongruenceSymmetry
satisfying_CongruenceEquivalenceRelation satisfying_CongruenceIdentity
TarskiGeometryStruct;
let c1,c2,c3,c4 be POINT of S;
assume
A1: c1,c2 equiv c3,c4;
assume
A2: not (c1,c2 equiv c4,c3 & c2,c1 equiv c3,c4 & c2,c1 equiv c4,c3 &
c3,c4 equiv c1,c2 & c4,c3 equiv c1,c2 & c3,c4 equiv c2,c1 &
c4,c3 equiv c2,c1);
A3: c1,c2 equiv c2,c1 by GTARSKI1:def 5;
then
A4: c3,c4 equiv c2,c1 by A1,GTARSKI1:def 6;
c1,c2 equiv c1,c2 by GTARSKI3:1;
then
A5: c3,c4 equiv c1,c2 by A1,GTARSKI1:def 6;
c3,c4 equiv c4,c3 by GTARSKI1:def 5;
hence contradiction by A1,A2,A3,A4,A5,GTARSKI1:def 6;
end;
theorem Prelim02:
for S being satisfying_CongruenceSymmetry
satisfying_CongruenceEquivalenceRelation satisfying_CongruenceIdentity
TarskiGeometryStruct for p,q,a,b,c,d being POINT of S st
(p,q equiv a,b or p,q equiv b,a or q,p equiv a,b or q,p equiv b,a) &
(p,q equiv c,d or p,q equiv d,c or q,p equiv c,d or q,p equiv d,c)
holds a,b equiv d,c & b,a equiv c,d & b,a equiv d,c &
c,d equiv a,b & d,c equiv a,b & c,d equiv b,a & d,c equiv b,a
proof
let S be satisfying_CongruenceSymmetry
satisfying_CongruenceEquivalenceRelation satisfying_CongruenceIdentity
TarskiGeometryStruct;
let p,q,a,b,c,d be POINT of S;
assume (p,q equiv a,b or p,q equiv b,a or q,p equiv a,b or q,p equiv b,a) &
(p,q equiv c,d or p,q equiv d,c or q,p equiv c,d or q,p equiv d,c);
then p,q equiv a,b & p,q equiv c,d by Prelim01;
then a,b equiv c,d by GTARSKI1:def 6;
hence thesis by Prelim01;
end;
theorem Prelim03:
for S being satisfying_CongruenceSymmetry
satisfying_CongruenceEquivalenceRelation satisfying_CongruenceIdentity
TarskiGeometryStruct for p,q,a,b,c,d being POINT of S st
(p,q equiv a,b or p,q equiv b,a or q,p equiv a,b or q,p equiv b,a or
a,b equiv p,q or b,a equiv p,q or a,b equiv q,p or b,a equiv q,p) &
(p,q equiv c,d or p,q equiv d,c or q,p equiv c,d or q,p equiv d,c or
c,d equiv p,q or d,c equiv p,q or c,d equiv q,p or d,c equiv q,p)
holds a,b equiv d,c & b,a equiv c,d & b,a equiv d,c & c,d equiv a,b &
d,c equiv a,b & c,d equiv b,a & d,c equiv b,a & a,b equiv c,d
proof
let S be satisfying_CongruenceSymmetry
satisfying_CongruenceEquivalenceRelation satisfying_CongruenceIdentity
TarskiGeometryStruct;
let p,q,a,b,c,d be POINT of S;
assume (p,q equiv a,b or p,q equiv b,a or q,p equiv a,b or q,p equiv b,a or
a,b equiv p,q or b,a equiv p,q or a,b equiv q,p or b,a equiv q,p) &
(p,q equiv c,d or p,q equiv d,c or q,p equiv c,d or q,p equiv d,c or
c,d equiv p,q or d,c equiv p,q or c,d equiv q,p or d,c equiv q,p);
then p,q equiv a,b & p,q equiv c,d by Prelim01;
hence thesis by Prelim02;
end;
theorem Prelim05:
for S being satisfying_CongruenceIdentity satisfying_SegmentConstruction
satisfying_BetweennessIdentity satisfying_Pasch TarskiGeometryStruct
for a,b being POINT of S holds Collinear a,b,b & Collinear b,b,a &
Collinear b,a,b
proof
let S be satisfying_CongruenceIdentity
satisfying_SegmentConstruction satisfying_BetweennessIdentity
satisfying_Pasch TarskiGeometryStruct;
let a,b be POINT of S;
between a,b,b & between b,b,a by GTARSKI3:13,15;
hence thesis by GTARSKI1:def 17;
end;
theorem Prelim07:
for S being non empty satisfying_Tarski-model TarskiGeometryStruct
for p,q,r being POINT of S st p <> q & p <> r &
(Collinear p,q,r or Collinear q,r,p or Collinear r,p,q or
Collinear p,r,q or Collinear q,p,r or Collinear r,q,p ) holds
Line(p,q) = Line(p,r) & Line(p,q) = Line(r,p) &
Line(q,p) = Line(p,r) & Line(q,p) = Line(r,p)
proof
let S be non empty satisfying_Tarski-model TarskiGeometryStruct;
let p,q,r be POINT of S;
assume that
A1: p <> q and
A2: p <> r and
A3: Collinear p,q,r or Collinear q,r,p or Collinear r,p,q or
Collinear p,r,q or Collinear q,p,r or Collinear r,q,p;
Collinear p,q,r by A3,GTARSKI3:45;
then r on_line p,q by A1,GTARSKI3:84;
hence thesis by A1,A2,GTARSKI1:39,GTARSKI3:85;
end;
theorem Prelim08:
for S being TarskiGeometryStruct
for a,b,c being POINT of S st
(Middle a,b,c or between a,b,c) holds Collinear a,b,c
proof
let S be TarskiGeometryStruct;
let a,b,c be POINT of S;
assume Middle a,b,c or between a,b,c;
then between a,b,c by GTARSKI3:def 12;
hence thesis by GTARSKI1:def 17;
end;
theorem Prelim08a:
for S being satisfying_CongruenceIdentity
satisfying_SegmentConstruction satisfying_BetweennessIdentity
satisfying_Pasch TarskiGeometryStruct
for a,b,c being POINT of S st
(Middle a,b,c or between a,b,c) holds
Collinear a,b,c & Collinear b,c,a & Collinear c,a,b &
Collinear c,b,a & Collinear b,a,c & Collinear a,c,b
proof
let S be satisfying_CongruenceIdentity
satisfying_SegmentConstruction satisfying_BetweennessIdentity
satisfying_Pasch TarskiGeometryStruct;
let a,b,c be POINT of S;
assume Middle a,b,c or between a,b,c;
then Collinear a,b,c by Prelim08;
hence thesis by GTARSKI3:45;
end;
theorem Prelim08b: ::: Lemma ext1, Chap. 8A
for S being non empty satisfying_Tarski-model TarskiGeometryStruct
for a,b,c,d being POINT of S st a <> b & Collinear a,b,c &
Collinear a,b,d holds Collinear a,c,d
proof
let S be non empty satisfying_Tarski-model TarskiGeometryStruct;
let a,b,c,d be POINT of S;
assume that
A1: a <> b and
A2: Collinear a,b,c and
A3: Collinear a,b,d;
per cases;
suppose a = c;
hence thesis by Prelim05;
end;
suppose a <> c; then
A4: Line(a,b) = Line(a,c) by A1,A2,Prelim07;
d in {y where y is POINT of S: Collinear a,b,y} by A3;
then d in Line(a,c) by A4,GTARSKI3:def 10; then
Collinear d,a,c by LemmaA2;
hence thesis by GTARSKI3:45;
end;
end;
theorem Prelim09:
for S being non empty satisfying_Tarski-model TarskiGeometryStruct
for a,b being POINT of S st Middle a,a,b or Middle a,b,b or
Middle a,b,a holds a = b
proof
let S be non empty satisfying_Tarski-model TarskiGeometryStruct;
let a,b be POINT of S;
assume Middle a,a,b or Middle a,b,b or Middle a,b,a;
then a,a equiv a,b or b,a equiv b,b or Middle a,b,a by GTARSKI3:def 12;
hence thesis by GTARSKI1:def 7,GTARSKI3:3,GTARSKI3:97;
end;
theorem Prelim10:
(Middle a,b,c or Middle c,b,a) & (a <> b or b <> c) implies
(Line(b,a) = Line(b,c) & Line(a,b) = Line(b,c) &
Line(a,b) = Line(c,b) & Line(b,a) = Line(c,b))
proof
assume that
A1: (Middle a,b,c or Middle c,b,a) and
A2: a <> b or b <> c;
A3: Middle a,b,c by A1,GTARSKI3:96;
then between a,b,c by GTARSKI3:def 12;
then a4: Collinear a,b,c by GTARSKI1:def 17;
per cases by A2;
suppose
A5: a <> b;
then b <> c by A3,GTARSKI1:def 7,GTARSKI3:def 12;
hence thesis by a4,A5,GTARSKI3:82,LemmaA1;
end;
suppose
A6: b <> c;
then a <> b by A1,Prelim09;
hence thesis by a4,A6,GTARSKI3:82,LemmaA1;
end;
end;
theorem Prelim11:
a <> b & c <> c9 & (c in Line(a,b) or c in Line(b,a)) &
(c9 in Line(a,b) or c9 in Line(b,a)) implies
Line(c,c9) = Line(a,b) & Line(c,c9) = Line(b,a) &
Line(c9,c) = Line(b,a) & Line(c9,c) = Line(a,b)
proof
assume that
A1: a <> b and
A2: c <> c9 and
A3: c in Line(a,b) or c in Line(b,a) and
A4: c9 in Line(a,b) or c9 in Line(b,a);
Line(a,b) is_line by A1,GTARSKI3:def 11;
hence thesis by A3,A4,A2,GTARSKI3:87;
end;
theorem Prelim12:
Middle reflection(p,c),reflection(p,b),reflection(p,reflection(b,c))
proof
Middle c,b,reflection(b,c) by GTARSKI3:def 13;
then between reflection(p,c),reflection(p,b),reflection(p,reflection(b,c))
& reflection(p,b),reflection(p,c) equiv
reflection(p,b),reflection(p,reflection(b,c)) by GTARSKI3:def 12,106,107;
hence thesis by GTARSKI3:def 12;
end;
begin :: Right angle
definition
let S be satisfying_CongruenceIdentity
satisfying_CongruenceSymmetry
satisfying_CongruenceEquivalenceRelation
satisfying_SegmentConstruction
satisfying_BetweennessIdentity
satisfying_SAS
TarskiGeometryStruct;
let a,b,c be POINT of S;
pred right_angle a,b,c means
a,c equiv a,reflection(b,c);
end;
reserve S for satisfying_Tarski-model TarskiGeometryStruct,
a,a9,b,b9,c,c9 for POINT of S;
::$N 8.2 Satz
theorem Satz8p2:
right_angle a,b,c implies right_angle c,b,a
proof
assume right_angle a,b,c; then
A1: c,a equiv a,reflection(b,c) by GTARSKI3:6;
a,reflection(b,c) equiv reflection(b,a),reflection(b,reflection(b,c))
by GTARSKI3:105;
then a,reflection(b,c) equiv reflection(b,a),c by GTARSKI3:101;
then a,reflection(b,c) equiv c,reflection(b,a) by GTARSKI3:7;
hence thesis by A1,GTARSKI3:5;
end;
theorem Lem01:
reflection(a,a) = a
proof
Middle a,a,a by GTARSKI3:97;
hence thesis by GTARSKI3:100;
end;
::$N 8.3 Satz
theorem Satz8p3:
right_angle a,b,c & a <> b & Collinear b,a,a9 implies right_angle a9,b,c
proof
assume that
A1: right_angle a,b,c and
A2: a <> b and
A3: Collinear b,a,a9;
now
b,c equiv reflection(b,b),reflection(b,c) by GTARSKI3:105;
hence b,c equiv b,reflection(b,c) by Lem01;
end;
hence thesis by A1,A2,A3,GTARSKI3:53;
end;
theorem
right_angle a,b,c implies right_angle a,b,reflection(b,c)
proof
assume right_angle a,b,c;
then a,reflection(b,c) equiv a,c by GTARSKI3:4;
hence thesis by GTARSKI3:101;
end;
::$N 8.5 Satz
theorem Satz8p5:
right_angle a,b,b
proof
a,b equiv a,b by GTARSKI3:2;
hence thesis by Lem01;
end;
::$N 8.6 Satz
theorem Satz8p6:
right_angle a,b,c & right_angle a9,b,c & between a,c,a9 implies b = c
proof
assume right_angle a,b,c & right_angle a9,b,c & between a,c,a9;
then c = reflection(b,c) by GTARSKI3:55;
hence thesis by GTARSKI3:104;
end;
::$N 8.7 Satz
theorem Satz8p7:
right_angle a,b,c & right_angle a,c,b implies b = c
proof
assume that
A1: right_angle a,b,c and
A2: right_angle a,c,b;
assume
A3: b <> c;
set c9 = reflection(b,c),
a9 = reflection(c,a);
now
a9,c equiv a9,c9
proof
now
now
thus a,c9 equiv a,c by A1,GTARSKI3:4;
right_angle c,c,a by Satz8p2,Satz8p5;
hence a,c equiv a9,c by Prelim01;
end;
hence a,c9 equiv a9,c by GTARSKI3:5;
now
thus right_angle b,c,a by A2,Satz8p2;
thus b <> c by A3;
Middle c,b,c9 by GTARSKI3:def 13;
hence Collinear c,b,c9 by Prelim08a;
end;
then right_angle c9,c,a by Satz8p3; then
A4: right_angle a,c,c9 by Satz8p2;
a,reflection(c,c9) equiv
reflection(c,a),reflection(c,reflection(c,c9)) by GTARSKI3:105;
then a,c9 equiv a9,reflection(c,reflection(c,c9)) by A4,GTARSKI3:5;
hence a,c9 equiv a9,c9 by GTARSKI3:101;
end;
hence thesis by GTARSKI1:def 6;
end;
hence right_angle a9,b,c;
Middle a,c,a9 by GTARSKI3:def 13;
hence between a,c,a9 by GTARSKI3:def 12;
end;
hence contradiction by A1,A3,Satz8p6;
end;
::$N 8.8 Satz
theorem Satz8p8:
right_angle a,b,a implies a = b
proof
assume
A1: right_angle a,b,a;
right_angle a,a,b by Satz8p2,Satz8p5;
hence thesis by A1,Satz8p7;
end;
::$N 8.9 Satz
theorem Satz8p9:
right_angle a,b,c & Collinear a,b,c implies a = b or c = b
proof
assume
A1: right_angle a,b,c & Collinear a,b,c;
assume
A2: a <> b;
Collinear b,a,c by A1,GTARSKI3:45;
hence thesis by A1,A2,Satz8p3,Satz8p8;
end;
::$N 8.10 Satz
theorem Satz8p10:
right_angle a,b,c & a,b,c cong a9,b9,c9 implies right_angle a9,b9,c9
proof
assume that
A1: right_angle a,b,c and
A2: a,b,c cong a9,b9,c9;
per cases;
suppose b = c;
then a,b equiv a9,b9 & a,b equiv a9,c9 & b,b equiv b9,c9
by A2,GTARSKI1:def 3;
then b9 = c9 by GTARSKI1:def 7,GTARSKI3:4;
hence thesis by Satz8p5;
end;
suppose
A3: b <> c;
set d = reflection(b,c),
d9 = reflection(b9,c9);
A4: a,b equiv a9,b9 & a,c equiv a9,c9 & b,c equiv b9,c9 by A2,GTARSKI1:def 3;
now
Middle c,b,d & Middle c9,b9,d9 by GTARSKI3:def 13;
hence between c,b,d & between c9,b9,d9 by GTARSKI3:def 12;
thus b,a equiv b9,a9 & c,b equiv c9,b9 & c,a equiv c9,a9
by A4,Prelim01;
b,c equiv reflection(b,b),reflection(b,c) by GTARSKI3:105; then
A5: b9,c9 equiv reflection(b,b),reflection(b,c) by A4,GTARSKI1:def 6;
b9,c9 equiv reflection(b9,b9),reflection(b9,c9) by GTARSKI3:105;
then reflection(b,b),reflection(b,c) equiv
reflection(b9,b9),reflection(b9,c9) by A5,GTARSKI1:def 6;
then b,reflection(b,c) equiv reflection(b9,b9),reflection(b9,c9)
by GTARSKI3:104;
hence b,d equiv b9,d9 by GTARSKI3:104;
end;
then c,b,d,a AFS c9,b9,d9,a9 by GTARSKI3:def 2; then
A6: a,d equiv d9,a9 by A3,GTARSKI3:6,10;
a,c equiv d9,a9 by A1,A6,Prelim03;
hence thesis by A4,Prelim03;
end;
end;
definition
let S be non empty satisfying_Tarski-model TarskiGeometryStruct;
let A,A9 be Subset of S;
let x be POINT of S;
pred are_orthogonal A,x,A9 means
A is_line & A9 is_line & x in A & x in A9 &
(for u,v being POINT of S st u in A & v in A9 holds right_angle u,x,v);
end;
definition
let S be non empty satisfying_Tarski-model TarskiGeometryStruct;
let A,A9 be Subset of S;
pred are_orthogonal A,A9 means
ex x being POINT of S st are_orthogonal A,x,A9;
end;
definition
let S be non empty satisfying_Tarski-model TarskiGeometryStruct;
let A be Subset of S;
let x,c,d be POINT of S;
pred are_lorthogonal A,x,c,d means
c <> d & are_orthogonal A,x,Line(c,d);
end;
definition
let S be non empty satisfying_Tarski-model TarskiGeometryStruct;
let a,b,x,c,d be POINT of S;
pred are_orthogonal a,b,x,c,d means
a <> b & c <> d & are_orthogonal Line(a,b),x,Line(c,d);
end;
definition
let S be non empty satisfying_Tarski-model TarskiGeometryStruct;
let a,b,c,d be POINT of S;
pred are_orthogonal a,b,c,d means
a <> b & c <> d & are_orthogonal Line(a,b),Line(c,d);
end;
reserve S for non empty satisfying_Tarski-model
TarskiGeometryStruct,
A,A9 for Subset of S,
x,y,z,a,b,c,c9,d,u,p,q,q9 for POINT of S;
::$N 8.12 Satz
theorem Satz8p12:
are_orthogonal A,x,A9 iff are_orthogonal A9,x,A by Satz8p2;
::$N 8.13 Satz
theorem Satz8p13:
are_orthogonal A,x,A9 iff A is_line & A9 is_line & x in A & x in A9 &
(ex u,v being POINT of S st u in A & v in A9 & u <> x & v <> x &
right_angle u,x,v)
proof
hereby
assume
A1: are_orthogonal A,x,A9;
hence A is_line & A9 is_line & x in A & x in A9;
consider p,q be POINT of S such that
A2: p <> q and
A3: A = Line(p,q) by A1,GTARSKI3:def 11;
consider p9,q9 be POINT of S such that
A4: p9 <> q9 and
A5: A9 = Line(p9,q9) by A1,GTARSKI3:def 11;
thus ex u,v being POINT of S st u in A & v in A9 & u <> x & v <> x &
right_angle u,x,v
proof
per cases;
suppose
A6: x = p;
take q;
A7: q in A by A3,GTARSKI3:83;
per cases;
suppose
A8: x = p9;
take q9;
thus thesis by A8,A4,A6,A2,A1,A5,A7,GTARSKI3:83;
end;
suppose
A9: x <> p9;
take p9;
p9 in A9 by A5,GTARSKI3:83;
hence thesis by A9,A6,A2,A3,A1,GTARSKI3:83;
end;
end;
suppose
A10: x <> p;
take p;
A11: p in A by A3,GTARSKI3:83;
per cases;
suppose
A12: x = p9;
take q9;
q9 in A9 by A5,GTARSKI3:83;
hence thesis by A12,A4,A10,A3,GTARSKI3:83,A1;
end;
suppose
A13: x <> p9;
take p9;
thus thesis by A5,GTARSKI3:83,A13,A11,A10,A1;
end;
end;
end;
end;
assume that
A14: A is_line and
A15: A9 is_line and
A16: x in A and
A17: x in A9 and
A18: ex u,v being POINT of S st u in A & v in A9 & u <> x & v <> x &
right_angle u,x,v;
consider u9,v9 be POINT of S such that
A19: u9 in A and
A20: v9 in A9 and
A21: u9 <> x and
A22: v9 <> x and
A23: right_angle u9,x,v9 by A18;
now
let u,v be POINT of S;
assume that
A24: u in A and
A25: v in A9;
Collinear x,u9,u by A14,A16,A19,A24,A21,GTARSKI3:90;
then right_angle u,x,v9 by A23,A21,Satz8p3;
then
A26: right_angle v9,x,u by Satz8p2;
Collinear x,v9,v by A15,A17,A20,A25,A21,GTARSKI3:90;
then right_angle v,x,u by A22,A26,Satz8p3;
hence right_angle u,x,v by Satz8p2;
end;
hence are_orthogonal A,x,A9 by A14,A15,A16,A17;
end;
::$N 8.14 (i) Satz
theorem Satz8p14p1:
are_orthogonal A,A9 implies A <> A9
proof
assume are_orthogonal A,A9;
then consider x be POINT of S such that
A1: are_orthogonal A,x,A9;
A2: A is_line & A9 is_line & x in A & x in A9 & (ex u,v being POINT of S st
u in A & v in A9 & u <> x & v <> x & right_angle u,x,v) by A1,Satz8p13;
consider u,v be POINT of S such that
A3: u in A and
A4: v in A9 and
A5: u <> x and
A6: v <> x and
A7: right_angle u,x,v by A1,Satz8p13;
assume A = A9;
then Collinear u,x,v by A2,A3,A4,GTARSKI3:90;
hence contradiction by A5,A6,A7,Satz8p9;
end;
::$N 6.22 Satz
definition
let S be non empty TarskiGeometryStruct;
let A,B be Subset of S;
let x be POINT of S;
pred A,B Is x means ::: intersect at
A is_line & B is_line & A <> B & x in A & x in B;
end;
::$N 8.14 (ii) Satz
theorem Satz8p14p2:
are_orthogonal A,x,A9 iff are_orthogonal A,A9 & A,A9 Is x
proof
hereby
assume
A1: are_orthogonal A,x,A9;
hence are_orthogonal A,A9;
hence A,A9 Is x by A1,Satz8p14p1;
end;
assume
A2: are_orthogonal A,A9 & A,A9 Is x;
then ex y be POINT of S st are_orthogonal A,y,A9;
hence are_orthogonal A,x,A9 by A2,GTARSKI3:88;
end;
::$N 8.14 (iii) Satz
theorem
are_orthogonal A,x,A9 & are_orthogonal A,y,A9 implies x = y
proof
assume that
A1: are_orthogonal A,x,A9 and
A2: are_orthogonal A,y,A9;
A <> A9 by A1,Satz8p14p1,Satz8p14p2;
hence thesis by A1,A2,GTARSKI3:89;
end;
theorem Satz8p15a:
Collinear a,b,x & are_orthogonal a,b,c,x implies
are_orthogonal a,b,x,c,x
proof
assume
A2: Collinear a,b,x;
assume
A3: are_orthogonal a,b,c,x;
then Line(a,b),Line(c,x) Is x
by A2,LemmaA1,GTARSKI3:def 11,83,Satz8p14p1;
hence are_orthogonal a,b,x,c,x by A3,Satz8p14p2;
end;
::$N 8.15 Satz
theorem Satz8p15:
a <> b & Collinear a,b,x implies
(are_orthogonal a,b,c,x iff are_orthogonal a,b,x,c,x)
proof
assume that
A1: a <> b and
A2: Collinear a,b,x;
thus are_orthogonal a,b,c,x implies are_orthogonal a,b,x,c,x
by Satz8p15a,A2;
assume are_orthogonal a,b,x,c,x;
then c <> x & are_orthogonal Line(a,b),Line(c,x);
hence thesis by A1;
end;
::$N 8.16 Satz
theorem
a <> b & Collinear a,b,x & Collinear a,b,u & u <> x implies
(are_orthogonal a,b,c,x iff (not Collinear a,b,c & right_angle c,x,u))
proof
assume that
A1: a <> b and
A2: Collinear a,b,x and
A3: Collinear a,b,u and
A4: u <> x;
hereby
assume
A5: are_orthogonal a,b,c,x;
then are_orthogonal a,b,x,c,x by A2,Satz8p15; then
A6: a <> b & c <> x & are_orthogonal Line(a,b),x,Line(c,x);
A7: u in Line(a,b) & c in Line(c,x) by A3,LemmaA1,GTARSKI3:83;
then right_angle c,x,u by A6,Satz8p2; then
A8: not Collinear c,x,u by A4,A5,Satz8p9;
A9: not c in {y where y is POINT of S: Collinear u,x,y}
proof
assume c in {y where y is POINT of S: Collinear u,x,y};
then ex y be POINT of S st c = y & Collinear u,x,y;
hence contradiction by A8,GTARSKI3:45;
end;
Line(a,b) = Line(u,x)
proof
per cases;
suppose u = a;
hence thesis by A4,A1,GTARSKI3:82,A2,LemmaA1;
end;
suppose
A11: u <> a; then
Line(a,b) = Line(a,u) by A3,LemmaA1,A1,GTARSKI3:82;
hence thesis by A4,A11,GTARSKI3:82,A2,LemmaA1;
end;
end; then
not c in Line(a,b) by A9,GTARSKI3:def 10;
hence not Collinear a,b,c & right_angle c,x,u by A7,A6,Satz8p2,LemmaA1;
end;
assume
A14: not Collinear a,b,c & right_angle c,x,u;
now
thus Line(a,b) is_line by A1,GTARSKI3:def 11;
thus Line(c,x) is_line by A14,A2,GTARSKI3:def 11;
thus x in Line(a,b) by A2,LemmaA1;
thus x in Line(c,x) by GTARSKI3:83;
thus ex u,v being POINT of S st u in Line(a,b) & v in Line(c,x) &
u <> x & v <> x & right_angle u,x,v
proof
take u,c;
thus u in Line(a,b) by A3,LemmaA1;
thus c in Line(c,x) by GTARSKI3:83;
thus u <> x by A4;
thus c <> x by A14,A2;
thus right_angle u,x,c by A14,Satz8p2;
end;
end;
then are_orthogonal Line(a,b),Line(c,x) by Satz8p13;
hence are_orthogonal a,b,c,x by A1,A14,A2;
end;
::$N 8.17 Definition
definition
let S be non empty satisfying_Tarski-model TarskiGeometryStruct;
let a,b,c,x be POINT of S;
pred x is_foot a,b,c means
Collinear a,b,x & are_orthogonal a,b,c,x;
end;
::$N 8.18 Satz - Uniqueness
theorem Satz8p18Uniqueness:
x is_foot a,b,c & y is_foot a,b,c implies x = y
proof
assume that
A1: x is_foot a,b,c and
A2: y is_foot a,b,c;
A3: Collinear a,b,y & are_orthogonal a,b,c,y by A2;
A4: c in Line(c,x) & c in Line(c,y) by GTARSKI3:83;
are_orthogonal a,b,x,c,x & are_orthogonal a,b,y,c,y by A1,A3,Satz8p15;
then are_orthogonal Line(a,b),x,Line(c,x) &
are_orthogonal Line(a,b),y,Line(c,y);
then right_angle c,x,y & right_angle c,y,x by A4,Satz8p2;
hence thesis by Satz8p7;
end;
theorem Satz8p18Lemma:
not Collinear a,b,c & between b,a,y & a <> y &
between a,y,z & y,z equiv y,p & y <> p &
q9 = reflection(z,q) & Middle c,x,c9 & c <> y &
between q9,y,c9 & Middle y,p,c & between p,y,q & q <> q9
implies x <> y
proof
assume that
A1: not Collinear a,b,c and
A2: between b,a,y and
A3: a <> y and
A4: between a,y,z and
A5: y,z equiv y,p and
A6: y <> p and
A7: q9 = reflection(z,q) and
A8: Middle c,x,c9 and
A9: c <> y and
A10: between q9,y,c9 and
A11: Middle y,p,c and
A12: between p,y,q and
A13: q <> q9;
assume
A14: x = y;
now
Collinear b,a,y by A2,GTARSKI1:def 17;
hence y in Line(a,b) by LemmaA1;
thus a <> y by A3;
thus a <> b by A1,GTARSKI3:46;
end;
then
A15: Line(a,y) = Line(a,b) by GTARSKI3:82;
now
Collinear a,y,z by A4,GTARSKI1:def 17;
hence z in Line(y,a) by LemmaA1;
thus y <> a by A3;
thus y <> z by A5,A6,GTARSKI1:def 7,GTARSKI3:4;
end; then
A16: Line(y,z) = Line(a,b) by A15,GTARSKI3:82;
A17: Line(x,c) = Line(x,c9) by A8,A9,A14,Prelim10;
Collinear x,c9,q9 by A10,A14,GTARSKI1:def 17;
then
A18: q9 in Line(x,c) by A17,LemmaA1;
between c,p,x & between p,x,q & p <> x
by A14,A6,A11,A12,GTARSKI3:def 12,14;
then between c,x,q by GTARSKI3:19;
then Collinear c,x,q by GTARSKI1:def 17;
then q in Line(c,x) by LemmaA1;
then
A19: Line(q,q9) = Line(c,x) by A13,A9,A14,A18,Prelim11;
Middle q,z,q9 by A7,GTARSKI3:def 13;
then between q,z,q9 by GTARSKI3:def 12;
then Collinear q,z,q9 by GTARSKI1:def 17;
then Collinear q,q9,z by GTARSKI3:45;
then z in Line(c,x) by A19,LemmaA1; then
Collinear z,c,x by LemmaA2;
then Collinear y,z,c by A14,GTARSKI3:45;
then c in Line(a,b) by A16,LemmaA1; then
Collinear c,a,b by LemmaA2;
hence contradiction by A1,GTARSKI3:45;
end;
reserve S for non empty
satisfying_Lower_Dimension_Axiom
satisfying_Tarski-model
TarskiGeometryStruct,
a,b,c,p,q,x,y,z,t for POINT of S;
::$N 8.18 Satz - Existence
theorem Satz8p18pExistence:
not Collinear a,b,c implies ex x st x is_foot a,b,c
proof
assume
A1: not Collinear a,b,c;
consider y such that
A2: between b,a,y and
A3: a,y equiv a,c by GTARSKI1:def 8;
consider p such that
A4: Middle y,p,c by A3,GTARSKI3:117;
A5: right_angle a,p,y by A3,A4,GTARSKI3:def 13;
consider z such that
A6: between a,y,z and
A7: y,z equiv y,p by GTARSKI1:def 8;
consider q such that
A8: between p,y,q and
A9: y,q equiv y,a by GTARSKI1:def 8;
set q9 = reflection(z,q);
consider c9 being POINT of S such that
A10: between q9,y,c9 and
A11: y,c9 equiv y,c by GTARSKI1:def 8;
A12: a <> b by A1,GTARSKI3:46;
A13: a <> y
proof
assume a = y;
then a = c by A3,GTARSKI1:def 7,GTARSKI3:4;
then Collinear a,c,b by GTARSKI3:46;
hence contradiction by A1,GTARSKI3:45;
end;
now
thus between a,y,z by A6;
thus between q,y,p by A8,GTARSKI3:14;
y,a equiv y,q by A9,GTARSKI3:3;
then a,y equiv y,q by GTARSKI3:6;
hence a,y equiv q,y by GTARSKI3:7;
thus y,z equiv y,p by A7;
thus a,q equiv q,a by GTARSKI3:2,6;
thus y,q equiv y,a by A9;
end;
then
A14: a,y,z,q AFS q,y,p,a by GTARSKI3:def 2;
now
p,a equiv z,q by A14,A13,GTARSKI3:3,10;
then a,p equiv z,q by GTARSKI3:6;
hence a,p equiv q,z by GTARSKI3:7;
y,a equiv y,q by A9,GTARSKI3:3;
then a,y equiv y,q by GTARSKI3:6;
hence a,y equiv q,y by GTARSKI3:7;
y,p equiv y,z by A7,GTARSKI3:4;
then p,y equiv y,z by GTARSKI3:6;
hence p,y equiv z,y by GTARSKI3:7;
end;
then a,p,y cong q,z,y by GTARSKI1:def 3;
then right_angle q,z,y by A5,Satz8p10;
then
A15: right_angle y,z,q by Satz8p2;
A16: y,c equiv y,c9 by A11,GTARSKI3:3;
consider x such that
A17: Middle c,x,c9 by A11,GTARSKI3:3,117;
A18: y <> p
proof
assume y = p;
then y,c equiv y,y by A4,GTARSKI3:4,def 12;
then y = c by GTARSKI1:def 7;
then Collinear b,a,c by A2,GTARSKI1:def 17;
hence contradiction by A1,GTARSKI3:45;
end;
now
between q,y,p & between y,p,c by A4,A8,GTARSKI3:14,def 12;
hence between q,y,c by A18,GTARSKI3:19;
thus between q9,y,c9 by A10;
thus y,q equiv y,q9 by A15;
thus y,c equiv y,c9 by A11,GTARSKI3:3;
thus Middle q,z,q9 by GTARSKI3:def 13;
thus Middle c,x,c9 by A17;
end;
then Krippenfigur q,z,q9,y,c9,x,c by GTARSKI3:def 14;
then between z,y,x by GTARSKI3:116;
then
A19: Collinear z,y,x by GTARSKI1:def 17;
A20: c <> y
proof
assume y = c;
then Collinear b,a,c by A2,GTARSKI1:def 17;
hence contradiction by A1,GTARSKI3:45;
end;
A21: y <> z by A7,A18,GTARSKI1:def 7,GTARSKI3:4;
A22: q <> q9
proof
assume q = q9; then
A23: Middle q,z,q by GTARSKI3:def 13; then
A24: q = z by GTARSKI3:97;
A25: y <> q by A23,GTARSKI3:97,A21;
Collinear b,a,y by A2,GTARSKI1:def 17; then
A26: Line(y,a) = Line(a,b) by A12,A13,GTARSKI3:82,LemmaA1;
Collinear a,y,z by A6,GTARSKI1:def 17; then
A27: Line(y,q) = Line(a,b) by A13,A21,A26,GTARSKI3:82,A24,LemmaA1;
Collinear y,q,p by A8,GTARSKI1:def 17; then
A28: Line(y,p) = Line(a,b) by A25,A18,GTARSKI3:82,A27,LemmaA1;
between y,p,c by A4,GTARSKI3:def 12;
then Collinear y,p,c by GTARSKI1:def 17;
then c in Line(a,b) by A28,LemmaA1; then
Collinear c,a,b by LemmaA2;
hence contradiction by A1,GTARSKI3:45;
end;
now
Collinear b,a,y by A2,GTARSKI1:def 17;
hence y in Line(a,b) by LemmaA1;
thus a <> y by A13;
thus a <> b by A1,GTARSKI3:46;
end;
then
A29: Line(a,y) = Line(a,b) by GTARSKI3:82;
now
Collinear a,y,z by A6,GTARSKI1:def 17;
hence z in Line(y,a) by LemmaA1;
thus y <> a by A13;
thus y <> z by A7,A18,GTARSKI1:def 7,GTARSKI3:4;
end; then
A30: Line(y,z) = Line(a,b) by A29,GTARSKI3:82;
A31: c <> x
proof
assume c = x;
then c9 = reflection(c,c) by A17,GTARSKI3:def 13;
then between q9,y,c by A10,GTARSKI3:104;
then a32: Collinear y,c,q9 by GTARSKI1:def 17;
between y,p,c by A4,GTARSKI3:def 12;
then A33: Collinear y,p,c by GTARSKI1:def 17;
A34: q <> y by A13,A9,GTARSKI3:4,GTARSKI1:def 7;
y <> p by A4,A20,Prelim09; then
A35: Line(y,p) = Line(y,c) by A20,A33,GTARSKI3:82,LemmaA1;
Collinear p,y,q by A8,GTARSKI1:def 17; then
Line(y,q) = Line(y,c) by A34,A20,GTARSKI3:82,A35,LemmaA1; then
A37: Line(q,q9) = Line(y,c) by A22,A34,GTARSKI3:82,a32,LemmaA1;
Middle q,z,q9 by GTARSKI3:def 13;
then between q,z,q9 by GTARSKI3:def 12;
then Collinear q,z,q9 by GTARSKI1:def 17;
then Collinear q,q9,z by GTARSKI3:45;
then z in Line(y,c) by A37,LemmaA1;
then Collinear z,y,c by LemmaA2;
then c in Line(y,z) by LemmaA1;
then Collinear c,a,b by LemmaA2,A30;
hence contradiction by A1,GTARSKI3:45;
end;
take x;
now
now
thus Line(y,z) is_line by A21,GTARSKI3:def 11;
thus Line(c,x) is_line by A31,GTARSKI3:def 11;
thus x in Line(y,z) by LemmaA1,A19;
thus x in Line(c,x) by GTARSKI3:83;
thus ex u,v be POINT of S st u in Line(y,z) & v in Line(c,x) &
u <> x & v <> x & right_angle u,x,v
proof
take y,c;
thus y in Line(y,z) by GTARSKI3:83;
thus c in Line(c,x) by GTARSKI3:83;
thus y <> x
by Satz8p18Lemma,A1,A2,A13,A7,A18,A17,A20,A10,A4,A8,A22,A6;
thus c <> x by A31;
thus right_angle y,x,c by A16,A17,GTARSKI3:def 13;
end;
end;
then are_orthogonal Line(a,b),Line(c,x) by A30,Satz8p13;
hence are_orthogonal a,b,c,x by GTARSKI3:46,A1,A31;
x in Line(y,z) by LemmaA1,A19;
then Collinear x,a,b by LemmaA2,A30;
hence Collinear a,b,x by GTARSKI3:45;
end;
hence thesis;
end;
::$N 8.20 Lemma
theorem Lemma8p20:
right_angle a,b,c & Middle reflection(a,c),p,reflection(b,c) implies
right_angle b,a,p & (b <> c implies a <> p)
proof
assume that
A1: right_angle a,b,c and
A2: Middle reflection(a,c),p,reflection(b,c);
set d = reflection(b,c),
b9 = reflection(a,b),
c9 = reflection(a,c),
d9 = reflection(a,d),
p9 = reflection(a,p);
A3: right_angle b9,b,c
proof
per cases;
suppose a = b;
then reflection(a,b) = b by GTARSKI3:104;
hence thesis by Satz8p2,Satz8p5;
end;
suppose
A4: a <> b;
Middle b,a,b9 by GTARSKI3:def 13;
then between b,a,b9 by GTARSKI3:def 12;
then Collinear b,a,b9 by GTARSKI1:def 17;
hence thesis by A1,A4,Satz8p3;
end;
end;
A5: b9,b equiv b,b9
proof
b9,b equiv reflection(a,reflection(a,b)),reflection(a,b)
by GTARSKI3:105;
hence thesis by GTARSKI3:101;
end;
A6: b9,c equiv b,c9
proof
b9,c equiv reflection(a,b9),reflection(a,c) by GTARSKI3:105;
hence thesis by GTARSKI3:101;
end;
b9,b,c cong b,b9,c9
proof
b,c equiv b9,c9 by GTARSKI3:105;
hence thesis by A5,A6,GTARSKI1:def 3;
end; then
A7: right_angle b,b9,c9 by A3,Satz8p10;
A8: reflection(b9,c9) = d9 by Prelim12,GTARSKI3:100;
c9,p,d,b IFS d9,p9,c,b
proof
now
thus between c9,p,d by A2,GTARSKI3:def 12;
between d,p,c9 by A2,GTARSKI3:14,def 12;
then between reflection(a,d),reflection(a,p),reflection(a,c9)
by GTARSKI3:106;
hence between d9,p9,c by GTARSKI3:101;
reflection(a,c),reflection(b,c) equiv
reflection(a,(reflection(a,c))),reflection(a,reflection(b,c))
by GTARSKI3:105;
then reflection(a,c),reflection(b,c) equiv
c,reflection(a,reflection(b,c)) by GTARSKI3:101;
hence c9,d equiv d9,c by GTARSKI3:7;
now
thus p,d equiv p9,d9 by GTARSKI3:105;
A9: p,c9 equiv p,d by A2,GTARSKI3:def 12;
p,c9 equiv reflection(a,p),reflection(a,c9) by GTARSKI3:105;
then
A10: p,c9 equiv p9,c by GTARSKI3:101;
p,d equiv reflection(a,p),reflection(a,d) by GTARSKI3:105;
then p,c9 equiv reflection(a,p),reflection(a,d) by A9,GTARSKI3:5;
then reflection(a,p),reflection(a,d) equiv p,c9 by GTARSKI3:4;
hence p9,d9 equiv p9,c by A10,GTARSKI3:5;
end;
hence p,d equiv p9,c by GTARSKI3:5;
c9,b equiv b,d9 by A8,A7,GTARSKI3:6;
hence c9,b equiv d9,b by GTARSKI3:7;
Middle c,b,d by GTARSKI3:def 13;
then b,d equiv b,c by GTARSKI3:4,def 12;
then d,b equiv b,c by GTARSKI3:6;
hence d,b equiv c,b by GTARSKI3:7;
end;
hence thesis by GTARSKI3:def 5;
end;
then b,p equiv p9,b by GTARSKI3:6,41;
hence right_angle b,a,p by GTARSKI3:7;
thus b <> c implies a <> p
proof
assume
A11: b <> c;
assume
A12: a = p;
c = reflection(a,c9) by GTARSKI3:101
.= d by A12,A2,GTARSKI3:def 13;
then Middle c,b,c by GTARSKI3:def 13;
hence thesis by GTARSKI3:97,A11;
end;
end;
theorem Satz8p21p1:
not Collinear a,b,c implies ex p,t st are_orthogonal a,b,p,a &
Collinear a,b,t & between c,t,p
proof
assume
A1: not Collinear a,b,c;
then
A2: a <> b by GTARSKI3:46;
consider x such that
A3: x is_foot a,b,c by A1,Satz8p18pExistence;
Collinear a,b,x & are_orthogonal a,b,c,x by A3;
then are_orthogonal a,b,x,c,x by Satz8p15;
then
A4: a <> b & c <> x & are_orthogonal Line(a,b),x,Line(c,x);
A5: a in Line(a,b) & c in Line(c,x) by GTARSKI3:83;
then right_angle a,x,c by A4;
then
A6: a,reflection(x,c) equiv a,c by GTARSKI3:3;
Middle c,a,reflection(a,c) by GTARSKI3:def 13;
then a,c equiv a,reflection(a,c) by GTARSKI3:def 12;
then consider p such that
A7: Middle reflection(x,c),p,reflection(a,c) by A6,GTARSKI3:5,117;
A8: Middle reflection(a,c),p,reflection(x,c) by A7,GTARSKI3:96;
A9: right_angle a,x,c by A5,A4; then
A10: right_angle x,a,p & a <> p by A1,A3,A8,Lemma8p20;
now
Middle c,x,reflection(x,c) by GTARSKI3:def 13;
hence between reflection(x,c),x,c by GTARSKI3:14,def 12;
Middle c,a,reflection(a,c) by GTARSKI3:def 13;
hence between reflection(a,c),a,c by GTARSKI3:14,def 12;
thus between reflection(x,c),p,reflection(a,c) by A7,GTARSKI3:def 12;
end;
then consider t such that
A11: between p,t,c and
A12: between x,t,a by GTARSKI3:40;
Collinear x,t,a by A12,GTARSKI1:def 17;
then Collinear x,a,t by GTARSKI3:45; then
A13: t in Line(x,a) by LemmaA1;
per cases;
suppose
A16: x <> a; then
Line(a,b) = Line(x,a) by A2,A3,LemmaA1,GTARSKI3:82; then
a18: Collinear t,a,b by LemmaA2,A13;
take p,t;
now
thus a <> b by A1,GTARSKI3:46;
thus p <> a by A9,A1,A3,A8,Lemma8p20;
now
thus Line(a,b) is_line by A2,GTARSKI3:def 11;
thus Line(p,a) is_line by A10,GTARSKI3:def 11;
thus a in Line(a,b) by GTARSKI3:83;
thus a in Line(p,a) by GTARSKI3:83;
thus ex u,v being POINT of S st u in Line(a,b) & v in Line(p,a) &
u <> a & v <> a & right_angle u,a,v
proof
take x,p;
thus x in Line(a,b) by A3,LemmaA1;
thus p in Line(p,a) by GTARSKI3:83;
thus x <> a & p <> a by A16,A9,A1,A3,A8,Lemma8p20;
thus right_angle x,a,p by A9,A8,Lemma8p20;
end;
end;
hence are_orthogonal Line(a,b),Line(p,a) by Satz8p13;
end;
hence thesis by a18,A11,GTARSKI3:14,GTARSKI3:45;
end;
suppose
A19: x = a;
then
A20: a = t by A12,GTARSKI1:def 10;
a21: now
thus p <> a by A9,A1,A3,A8,Lemma8p20;
thus c <> a
proof
assume c = a;
then Collinear a,c,b by GTARSKI3:46;
hence contradiction by A1,GTARSKI3:45;
end;
Collinear p,a,c by A20,A11,GTARSKI1:def 17;
hence c in Line(a,p) by LemmaA1;
end;
take p,t;
Collinear a,b,a & are_orthogonal a,b,c,a by A3,A19;
hence thesis by a21,A11,GTARSKI3:14,82,A19,A12,GTARSKI1:def 10;
end;
end;
::$N 8.21 Satz
theorem Satz8p21:
a <> b implies ex p,t st are_orthogonal a,b,p,a & Collinear a,b,t &
between c,t,p
proof
assume
A1: a <> b;
per cases;
suppose
not Collinear a,b,c;
hence thesis by Satz8p21p1;
end;
suppose
A2: Collinear a,b,c;
consider c9 being POINT of S such that
A3: not Collinear a,b,c9 by A1,GTARSKI3:92;
ex p,t st are_orthogonal a,b,p,a & Collinear a,b,t & between c9,t,p
by A3,Satz8p21p1;
hence thesis by A2,GTARSKI3:15;
end;
end;
theorem Th01:
a <> b & a <> p & right_angle b,a,p & right_angle a,b,q implies
not Collinear p,a,q
proof
assume that
A1: a <> b and
A2: a <> p and
A3: right_angle b,a,p and
A4: right_angle a,b,q;
assume
A5: Collinear p,a,q;
now
A6: right_angle p,a,b by A3,Satz8p2;
right_angle a,b,q & a <> p & Collinear a,p,q by A2,A4,A5,GTARSKI3:45;
hence right_angle q,a,b by A6,Satz8p3;
thus right_angle q,b,a by A4,Satz8p2;
end;
hence contradiction by A1,Satz8p7;
end;
LemmaA3:
for S being non empty satisfying_Lower_Dimension_Axiom
satisfying_Tarski-model TarskiGeometryStruct
for a,b,p being POINT of S st a <> p holds
reflection(a,p) <> p
proof
let S be non empty satisfying_Lower_Dimension_Axiom
satisfying_Tarski-model TarskiGeometryStruct;
let a,b,p be POINT of S;
assume
A1: a <> p;
assume
A2: p = reflection(a,p);
Middle p,a,reflection(a,p) by GTARSKI3:def 13;
hence contradiction by GTARSKI3:97,A1,A2;
end;
theorem Satz8p22lemma:
for S being non empty satisfying_Lower_Dimension_Axiom
satisfying_Tarski-model TarskiGeometryStruct
for a,b,p,q,t being POINT of S st a,p <= b,q & are_orthogonal a,b,q,b &
are_orthogonal a,b,p,a & Collinear a,b,t & between q,t,p holds
ex x being POINT of S st Middle a,x,b
proof
let S be non empty satisfying_Lower_Dimension_Axiom
satisfying_Tarski-model TarskiGeometryStruct;
let a,b,p,q,t be POINT of S;
assume that
A1: a,p <= b,q and
A2: are_orthogonal a,b,q,b and
A3: are_orthogonal a,b,p,a and
A4: Collinear a,b,t and
A5: between q,t,p;
consider r be POINT of S such that
A6: between b,r,q and
A7: a,p equiv b,r by A1,GTARSKI3:def 7;
between p,t,q by A5,GTARSKI3:14;
then consider x be POINT of S such that
A8: between t,x,b and
A9: between r,x,p by A6,GTARSKI1:def 11;
A10: Collinear a,b,x
proof
per cases;
suppose b = t;
then x = b by A8,GTARSKI1:def 10;
then Collinear b,x,a by GTARSKI3:46;
hence thesis by GTARSKI3:45;
end;
suppose b <> t; then
A12: Line(t,b) = Line(a,b) by A2,GTARSKI3:82,A4,LemmaA1;
Collinear t,x,b by A8,GTARSKI1:def 17;
then Collinear t,b,x by GTARSKI3:45;
then x in Line(a,b) by A12,LemmaA1; then
Collinear x,a,b by LemmaA2;
hence thesis by GTARSKI3:45;
end;
end;
a <> b & q <> b & are_orthogonal Line(a,b),Line(q,b) by A2;
then consider x9 be POINT of S such that
A13: are_orthogonal Line(a,b),x9,Line(q,b);
b in Line(a,b) & b in Line(q,b) by GTARSKI3:83;
then right_angle b,x9,b by A13;
then b = reflection(x9,b) by GTARSKI1:def 7,GTARSKI3:4;
then Middle b,x9,b by GTARSKI3:100;
then
A14: x9 = b by GTARSKI3:97;
A15: a in Line(a,b) & q in Line(q,b) by GTARSKI3:83;
a <> b & p <> a & are_orthogonal Line(a,b),Line(p,a) by A3;
then consider y be POINT of S such that
A16: are_orthogonal Line(a,b),y,Line(p,a);
A17: b in Line(a,b) & p in Line(p,a) by GTARSKI3:83; then
A18: right_angle b,y,p by A16;
a in Line(a,b) & a in Line(p,a) by GTARSKI3:83;
then right_angle a,y,a by A16;
then a = reflection(y,a) by GTARSKI1:def 7,GTARSKI3:4;
then Middle a,y,a by GTARSKI3:100; then
A19: y = a by GTARSKI3:97;
right_angle q,b,a & q <> b & Collinear b,q,r
by A13,Satz8p2,A2,A6,A14,A15,Prelim08a; then
A20: right_angle r,b,a by Satz8p3;
A21: not Collinear b,a,p & not Collinear a,b,q
by A3,A15,A14,A13,A17,A16,A19,A2,Satz8p9;
A22: r <> b by A3,A7,GTARSKI1:5;
now
thus not Collinear a,p,b by A21,GTARSKI3:45;
thus p <> r
proof
assume
A23: p = r;
then p = x by A9,GTARSKI1:8;
then b = r by A20,A2,Satz8p9,A10,A23,Satz8p2;
hence contradiction by A23,A17,A19,A2,A16,Satz8p8;
end;
thus a,p equiv b,r by A7;
A24: x <> a
proof
assume x = a; then
A25: Collinear r,a,p by A9,GTARSKI1:def 17;
right_angle a,b,r by A20,Satz8p2;
then not Collinear p,a,r by A3,A18,A19,Th01;
hence contradiction by A25,GTARSKI3:45;
end;
thus p,b equiv r,a
proof
set p9 = reflection(a,p);
consider r9 be POINT of S such that
A26: between p9,x,r9 and
A27: x,r9 equiv x,r by GTARSKI1:def 8;
consider m be POINT of S such that
A28: Middle r9,m,r by A27,GTARSKI3:117;
A29: Middle r,m,r9 by A28,GTARSKI3:96;
A30: right_angle x,a,p by A17,A19,A10,A2,A16,Satz8p3;
A31: p <> p9 by A3,LemmaA3;
Collinear p,a,p9 by GTARSKI3:def 13,Prelim08; then
A32: Line(a,p) = Line(p,p9) by A31,A3,Prelim07;
A33: not Collinear x,p,p9
proof
assume Collinear x,p,p9;
then Collinear p,p9,x by GTARSKI3:45;
then x in Line(a,p) by A32,LemmaA1;
hence contradiction by A30,A24,A3,Satz8p9,LemmaA2;
end;
between p9,x,r9 & between p,x,r & x,p9 equiv x,p &
x,r9 equiv x,r & Middle p9,a,p & Middle r9,m,r
by A9,GTARSKI3:14,A26,A28,A30,Prelim01,A27,GTARSKI3:96,def 13;
then
A34: between a,x,m by GTARSKI3:115;
A35: x <> m
proof
assume
A36: x = m;
Collinear x,r9,p9 by A26,Prelim08a; then
A37: p9 in Line(x,r9) by LemmaA1;
A38: Collinear x,r,r9 by A36,A28,Prelim08a;
per cases;
suppose
A39: x <> r;
then x <> r9 by A27,GTARSKI1:5,GTARSKI3:4;
then Line(x,r) = Line(x,r9) by A39,A38,Prelim07; then
Collinear p9,x,r by A37,LemmaA2; then
A40: Collinear x,r,p9 by GTARSKI3:45;
Collinear x,r,p by A9,Prelim08a;
hence contradiction by A33,A39,Prelim08b,A40;
end;
suppose x = r;
hence contradiction by A20,A10,A2,A22,Satz8p2,Satz8p9;
end;
end;
Collinear a,x,m by A34,GTARSKI1:def 17; then
A41: m in Line(a,x) by LemmaA1; then
A43: m in Line(a,b) by A24,A2,GTARSKI3:82,A10,LemmaA1;
A44: reflection(m,r) = r9 by A28,GTARSKI3:96,100;
now
thus a <> b by A2;
thus
A45: r <> m by A43,LemmaA2,A20,A2,A22,Satz8p9;
thus are_orthogonal Line(a,b),Line(r,m)
proof
now
thus Line(a,b) is_line by A2,GTARSKI3:def 11;
thus Line(r,m) is_line by A45,GTARSKI3:def 11;
thus m in Line(a,b) by A10,LemmaA1,A41,A24,A2,GTARSKI3:82;
thus m in Line(r,m) by GTARSKI3:83;
b3: x in Line(a,b) by A10,LemmaA1;
b4: r in Line(r,m) by GTARSKI3:83;
right_angle x,m,r by A44,GTARSKI3:4,A27;
hence ex u,v be POINT of S st u <> m & v <> m & u in Line(a,b)
& v in Line(r,m) & right_angle u,m,v by A35,A45,b3,b4;
end;
hence thesis by Satz8p13;
end;
end; then
A46: are_orthogonal a,b,r,m;
Collinear m,a,b by A43,LemmaA2; then
A47: m is_foot a,b,r by A46,GTARSKI3:45;
now
thus Collinear a,b,b by Prelim05;
thus are_orthogonal a,b,r,b
proof
set A = Line(a,b), A9 = Line(r,b);
now
thus A is_line by A2,GTARSKI3:def 11;
thus A9 is_line by A22,GTARSKI3:def 11;
thus b in A & b in A9 by GTARSKI3:83;
thus ex u,v being POINT of S st u in A & v in A9 & u <> b &
v <> b & right_angle u,b,v
proof
take a,r;
thus a in A by GTARSKI3:83;
thus r in A9 by GTARSKI3:83;
thus a <> b by A2;
thus r <> b by A3,A7,GTARSKI1:5;
thus right_angle a,b,r by A20,Satz8p2;
end;
end;
then are_orthogonal A,A9 by Satz8p13;
hence thesis by A3,A7,GTARSKI1:5;
end;
end; then
A48: b is_foot a,b,r; then
A49: m = b by A47,Satz8p18Uniqueness;
A50: Middle r,b,r9 by A29,A47,A48,Satz8p18Uniqueness;
A51: Middle p,a,p9 by GTARSKI3:def 13;
now
thus
A52: Middle p9,a,p by GTARSKI3:96,def 13;
hence between p9,a,p by GTARSKI3:def 12;
thus between r,b,r9 by A50,GTARSKI3:def 12;
A53: a,p equiv a,p9 by A51,GTARSKI3:def 12;
A54: m,r9 equiv m,r by A28,GTARSKI3:def 12;
between p9,a,p & between r,m,r9 & p9,a equiv r,m &
a,p equiv m,r9
by A53,A29,GTARSKI3:def 12,A7,A54,A49,Prelim03,A52;
hence p9,p equiv r,r9 by GTARSKI3:11;
thus a,p equiv b,r9 by A7,A54,A49,Prelim03;
p9,r equiv p9,r by GTARSKI3:1;
hence p9,r equiv r,p9 by Prelim01;
between p,x,r & between p9,x,r9 & p,x equiv p9,x &
x,r equiv x,r9 by A26,A30,A9,GTARSKI3:14,Prelim01,A27;
then p,r equiv p9,r9 by GTARSKI3:11;
hence p,r equiv r9,p9 by Prelim01;
end;
then p9,a,p,r IFS r,b,r9,p9 by GTARSKI3:def 5;
then a,r equiv b,p9 by GTARSKI3:41;
hence thesis by A18,A19,Prelim03;
end;
thus Collinear a,x,b by A10,GTARSKI3:45;
Collinear r,x,p by A9,GTARSKI1:def 17;
hence Collinear p,x,r by GTARSKI3:45;
end;
then Middle a,x,b & Middle p,x,r by GTARSKI3:112;
hence thesis;
end;
::$N 8.22 Satz
theorem Satz8p22:
for S being non empty satisfying_Lower_Dimension_Axiom
satisfying_Tarski-model TarskiGeometryStruct
for a,b being POINT of S holds
ex x being POINT of S st Middle a,x,b
proof
let S be non empty satisfying_Lower_Dimension_Axiom
satisfying_Tarski-model TarskiGeometryStruct;
let a,b be POINT of S;
set c = the POINT of S;
per cases;
suppose a = b;
hence thesis by GTARSKI3:97;
end;
suppose
A1: a <> b;
then consider q,t be POINT of S such that
A2: are_orthogonal b,a,q,b and
Collinear b,a,t and
between c,t,q by Satz8p21;
A3: are_orthogonal a,b,q,b by A2;
consider p,t9 be POINT of S such that
A4: are_orthogonal a,b,p,a and
A5: Collinear a,b,t9 and
A6: between q,t9,p by A1,Satz8p21;
per cases by GTARSKI3:64;
suppose a,p <= b,q;
hence thesis by Satz8p22lemma,A3,A4,A5,A6;
end;
suppose
A7: b,q <= a,p;
are_orthogonal b,a,p,a & are_orthogonal b,a,q,b & Collinear b,a,t9 &
between p,t9,q by A6,A4,A2,A5,GTARSKI3:14,45;
then ex x be POINT of S st Middle b,x,a by Satz8p22lemma,A7;
hence thesis by GTARSKI3:96;
end;
end;
end;
definition
let S be non empty satisfying_Lower_Dimension_Axiom
satisfying_Tarski-model TarskiGeometryStruct;
let a,b be POINT of S;
func Midpoint (a,b) -> POINT of S means
Middle a,it,b;
existence by Satz8p22;
uniqueness by GTARSKI3:108;
end;
::$N 8.24 Lemma
theorem
for S being non empty satisfying_Lower_Dimension_Axiom
satisfying_Tarski-model TarskiGeometryStruct
for a,b,p,q,r,t being POINT of S st are_orthogonal p,a,a,b &
are_orthogonal q,b,a,b & Collinear a,b,t & between p,t,q &
between b,r,q & a,p equiv b,r holds
ex x being POINT of S st Middle a,x,b & Middle p,x,r
proof
let S be non empty satisfying_Lower_Dimension_Axiom
satisfying_Tarski-model TarskiGeometryStruct;
let a,b,p,q,r,t be POINT of S;
assume that
A1: are_orthogonal p,a,a,b and
A2: are_orthogonal q,b,a,b and
A3: Collinear a,b,t and
A4: between p,t,q and
A5: between b,r,q and
A6: a,p equiv b,r;
A7: q <> b & a <> b & are_orthogonal Line(q,b),Line(a,b) by A2;
A7BIS: are_orthogonal Line(p,a),Line(a,b) by A1;
consider x be POINT of S such that
A8: between t,x,b and
A9: between r,x,p by A4,A5,GTARSKI1:def 11;
A10: Collinear a,b,x
proof
per cases;
suppose b = t;
then x = b by A8,GTARSKI1:def 10;
then Collinear b,x,a by GTARSKI3:46;
hence thesis by GTARSKI3:45;
end;
suppose b <> t; then
A12: Line(t,b) = Line(a,b) by A2,GTARSKI3:82,A3,LemmaA1;
Collinear t,x,b by A8,GTARSKI1:def 17;
then Collinear t,b,x by GTARSKI3:45;
then x in Line(a,b) by A12,LemmaA1;
then Collinear x,a,b by LemmaA2;
hence thesis by GTARSKI3:45;
end;
end;
consider x9 be POINT of S such that
A13: are_orthogonal Line(a,b),x9,Line(q,b) by A7,Satz8p12;
b in Line(a,b) & b in Line(q,b) by GTARSKI3:83;
then right_angle b,x9,b by A13;
then b = reflection(x9,b) by GTARSKI1:def 7,GTARSKI3:4;
then Middle b,x9,b by GTARSKI3:100;
then
A14: x9 = b by GTARSKI3:97;
A15: a in Line(a,b) & q in Line(q,b) by GTARSKI3:83;
consider y be POINT of S such that
A16: are_orthogonal Line(a,b),y,Line(p,a) by A7BIS,Satz8p12;
A17: b in Line(a,b) & p in Line(p,a) by GTARSKI3:83; then
A18: right_angle b,y,p by A16;
a in Line(a,b) & a in Line(p,a) by GTARSKI3:83;
then right_angle a,y,a by A16;
then a = reflection(y,a) by GTARSKI1:def 7,GTARSKI3:4;
then Middle a,y,a by GTARSKI3:100; then
A19: y = a by GTARSKI3:97;
right_angle q,b,a & q <> b & Collinear b,q,r
by A13,Satz8p2,A2,A5,A14,A15,Prelim08a; then
A20: right_angle r,b,a by Satz8p3;
A21: not Collinear b,a,p & not Collinear a,b,q
by A15,A14,A13,A17,A16,A19,A2,Satz8p9,A1;
A22: r <> b by A6,GTARSKI1:5,A1;
now
thus not Collinear a,p,b by A21,GTARSKI3:45;
thus p <> r
proof
assume
A23: p = r;
then p = x by A9,GTARSKI1:8;
then b = r by A20,A2,Satz8p9,A10,A23,Satz8p2;
hence contradiction by A23,A17,A19,A2,A16,Satz8p8;
end;
thus a,p equiv b,r by A6;
A24: x <> a
proof
assume x = a; then
A25: Collinear r,a,p by A9,GTARSKI1:def 17;
right_angle a,b,r by A20,Satz8p2;
then not Collinear p,a,r by A18,A19,Th01,A1;
hence contradiction by A25,GTARSKI3:45;
end;
thus p,b equiv r,a
proof
set p9 = reflection(a,p);
consider r9 be POINT of S such that
A26: between p9,x,r9 and
A27: x,r9 equiv x,r by GTARSKI1:def 8;
consider m be POINT of S such that
A28: Middle r9,m,r by A27,GTARSKI3:117;
A29: Middle r,m,r9 by A28,GTARSKI3:96;
A30: right_angle x,a,p by A17,A19,A10,A2,A16,Satz8p3;
A31: p <> p9 by A1,LemmaA3;
Collinear p,a,p9 by GTARSKI3:def 13,Prelim08; then
A32: Line(a,p) = Line(p,p9) by A31,Prelim07,A1;
A33: not Collinear x,p,p9
proof
assume Collinear x,p,p9;
then Collinear p,p9,x by GTARSKI3:45;
then x in Line(a,p) by A32,LemmaA1;
hence contradiction by A30,A24,Satz8p9,A1,LemmaA2;
end;
between p9,x,r9 & between p,x,r & x,p9 equiv x,p &
x,r9 equiv x,r & Middle p9,a,p & Middle r9,m,r
by A9,GTARSKI3:14,A26,A28,A30,Prelim01,A27,GTARSKI3:96,def 13;
then
A34: between a,x,m by GTARSKI3:115;
A35: x <> m
proof
assume
A36: x = m;
Collinear x,r9,p9 by A26,Prelim08a; then
A37: p9 in Line(x,r9) by LemmaA1;
A38: Collinear x,r,r9 by A36,A28,Prelim08a;
per cases;
suppose
A39: x <> r;
then x <> r9 by A27,GTARSKI1:5,GTARSKI3:4;
then Line(x,r) = Line(x,r9) by A39,A38,Prelim07; then
Collinear p9,x,r by A37,LemmaA2; then
A40: Collinear x,r,p9 by GTARSKI3:45;
Collinear x,r,p by A9,Prelim08a;
hence contradiction by A33,A40,A39,Prelim08b;
end;
suppose x = r;
hence contradiction by A20,A10,A2,A22,Satz8p2,Satz8p9;
end;
end;
Collinear a,x,m by A34,GTARSKI1:def 17; then
A41: m in Line(a,x) by LemmaA1; then
A43: m in Line(a,b) by A24,A2,GTARSKI3:82,A10,LemmaA1;
A44: reflection(m,r) = r9 by A28,GTARSKI3:96,100;
now
thus a <> b by A2;
thus
A45: r <> m by A43,LemmaA2,A20,A2,A22,Satz8p9;
thus are_orthogonal Line(a,b),Line(r,m)
proof
now
thus Line(a,b) is_line by A2,GTARSKI3:def 11;
thus Line(r,m) is_line by A45,GTARSKI3:def 11;
thus m in Line(a,b) by A10,LemmaA1,A41,A24,A2,GTARSKI3:82;
thus m in Line(r,m) by GTARSKI3:83;
B3: x in Line(a,b) by A10,LemmaA1;
B4: r in Line(r,m) by GTARSKI3:83;
right_angle x,m,r by A44,GTARSKI3:4,A27;
hence ex u,v be POINT of S st u <> m & v <> m & u in Line(a,b)
& v in Line(r,m) & right_angle u,m,v by A35,A45,B3,B4;
end;
hence thesis by Satz8p13;
end;
end; then
A46: are_orthogonal a,b,r,m;
Collinear m,a,b by A43,LemmaA2; then
A47: m is_foot a,b,r by A46,GTARSKI3:45;
now
thus Collinear a,b,b by Prelim05;
thus are_orthogonal a,b,r,b
proof
set A = Line(a,b), A9 = Line(r,b);
now
thus A is_line by A2,GTARSKI3:def 11;
thus A9 is_line by A22,GTARSKI3:def 11;
thus b in A & b in A9 by GTARSKI3:83;
thus ex u,v being POINT of S st u in A & v in A9 & u <> b &
v <> b & right_angle u,b,v
proof
take a,r;
thus a in A by GTARSKI3:83;
thus r in A9 by GTARSKI3:83;
thus a <> b by A2;
thus r <> b by A6,GTARSKI1:5,A1;
thus right_angle a,b,r by A20,Satz8p2;
end;
end;
then are_orthogonal A,A9 by Satz8p13;
hence thesis by A6,GTARSKI1:5,A1;
end;
end; then
A48: b is_foot a,b,r; then
A49: m = b by A47,Satz8p18Uniqueness;
A50: Middle r,b,r9 by A29,A47,A48,Satz8p18Uniqueness;
now
A51: Middle p,a,p9 by GTARSKI3:def 13;
thus
A52: Middle p9,a,p by GTARSKI3:96,def 13;
hence between p9,a,p by GTARSKI3:def 12;
thus between r,b,r9 by A50,GTARSKI3:def 12;
A53: a,p equiv a,p9 by A51,GTARSKI3:def 12;
A54: m,r9 equiv m,r by A28,GTARSKI3:def 12;
between p9,a,p & between r,m,r9 & p9,a equiv r,m &
a,p equiv m,r9
by A53,A29,GTARSKI3:def 12,A6,A54,A49,Prelim03,A52;
hence p9,p equiv r,r9 by GTARSKI3:11;
thus a,p equiv b,r9 by A6,A54,A49,Prelim03;
p9,r equiv p9,r by GTARSKI3:1;
hence p9,r equiv r,p9 by Prelim01;
between p,x,r & between p9,x,r9 & p,x equiv p9,x &
x,r equiv x,r9 by A26,A30,A9,GTARSKI3:14,Prelim01,A27;
then p,r equiv p9,r9 by GTARSKI3:11;
hence p,r equiv r9,p9 by Prelim01;
end;
then p9,a,p,r IFS r,b,r9,p9 by GTARSKI3:def 5;
then a,r equiv b,p9 by GTARSKI3:41;
hence thesis by A18,A19,Prelim03;
end;
thus Collinear a,x,b by A10,GTARSKI3:45;
Collinear r,x,p by A9,GTARSKI1:def 17;
hence Collinear p,x,r by GTARSKI3:45;
end;
then Middle a,x,b & Middle p,x,r by GTARSKI3:112;
hence thesis;
end;
begin :: Chapter 8A
theorem :: ExtCol2
for a,b,c,d,x,p,q being POINT of S holds
c in Line(a,b) & d in Line(a,b) & a <> b & c <> d implies
Line (a,b) = Line (c,d) by Prelim11;
theorem :: ExtPerp:
for a,b,c,d,x,p,q being POINT of S holds
c in Line(a,b) & d in Line(a,b) & c <> d &
are_orthogonal a,b,x,p,q implies are_orthogonal c,d,x,p,q by Prelim11;
theorem :: ExtPerp2:
for a,b,c,d,p,q being POINT of S holds
p in Line(a,b) & q in Line(a,b) & a <> b &
are_orthogonal p,q,c,d implies are_orthogonal a,b,c,d by Prelim11;
theorem :: ExtPerp3:
for a,b,c,d being POINT of S holds
a <> b & b <> c & c <> d & a <> c & a <> d & b <> d &
are_orthogonal b,a,a,c & Collinear a,c,d implies
are_orthogonal b,a,a,d
proof
let a,b,c,d be POINT of S;
assume
A1: a <> b & b <> c & c <> d & a <> c & a <> d & b <> d &
are_orthogonal b,a,a,c & Collinear a,c,d; then
A3: d in Line(a,c) by LemmaA1;
a in Line(a,c) by GTARSKI3:83;
hence thesis by A1,A3,Prelim11;
end;
theorem :: ExtPerp4:
for a,b,p,q being POINT of S holds
are_orthogonal a,b,p,q implies are_orthogonal a,b,q,p;
theorem ExtPerp5:
for a,b,c,d,p,q being POINT of S holds
p in Line(a,b) & q in Line(a,b) & p <> q &
are_orthogonal a,b,c,d implies are_orthogonal p,q,c,d by Prelim11;
theorem :: ExtPerp5A:
for a,b,c,d,p,q being POINT of S holds
Collinear a,b,p & Collinear a,b,q & p <> q &
are_orthogonal a,b,c,d implies are_orthogonal p,q,c,d
proof
let a,b,c,d,p,q be POINT of S;
assume that
A1: Collinear a,b,p and
A2: Collinear a,b,q & p <> q & are_orthogonal a,b,c,d;
A3: p in Line (a,b) by A1,LemmaA1;
q in Line (a,b) by A2,LemmaA1;
hence thesis by ExtPerp5,A3,A2;
end;
theorem :: ExtPerp6:
for a,b,c,d,p,q being POINT of S holds
p in Line(a,b) & q in Line(a,b) & p <> q & a <> b &
are_orthogonal c,d,p,q implies are_orthogonal c,d,a,b by Prelim11;