GTARSKI4: Tarski Geometry Axioms. {P}art {IV } -- Right angle

:: Tarski Geometry Axioms. {P}art {IV } -- Right angle
:: by Roland Coghetto and Adam Grabowski
::
:: Received March 11, 2019
:: Copyright (c) 2019-2021 Association of Mizar Users

definition

let S be non empty satisfying_CongruenceIdentity satisfying_SegmentConstruction satisfying_BetweennessIdentity satisfying_Pasch TarskiGeometryStruct ;
let a, b be POINT of S;
:: original: Line
redefine func Line (a,b) -> M3(K16( the U1 of S));
commutativity by GTARSKI3:83;

end;

LemmaA1: for S being non empty satisfying_Tarski-model TarskiGeometryStruct
for a, b, c being POINT of S st Collinear a,b,c holds
c in Line (a,b)

proof end;

LemmaA2: for S being non empty satisfying_Tarski-model TarskiGeometryStruct
for a, x, p being POINT of S st x in Line (a,p) holds
Collinear x,a,p

proof end;

theorem Prelim01: :: GTARSKI4:1

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

theorem Prelim02: :: GTARSKI4:2

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

theorem Prelim03: :: GTARSKI4:3

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

theorem Prelim05: :: GTARSKI4:4

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

theorem Prelim07: :: GTARSKI4:5

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

theorem Prelim08: :: GTARSKI4:6

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

theorem Prelim08a: :: GTARSKI4:7

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

theorem Prelim08b: :: GTARSKI4:8

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

theorem Prelim09: :: GTARSKI4:9

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

theorem Prelim10: :: GTARSKI4:10

for S being non empty satisfying_Tarski-model TarskiGeometryStruct
for a, b, c being POINT of S st ( Middle a,b,c or Middle c,b,a ) & ( a <> b or b <> c ) holds
( 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 end;

theorem Prelim11: :: GTARSKI4:11

for S being non empty satisfying_Tarski-model TarskiGeometryStruct
for a, b, c, c9 being POINT of S st 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) ) holds
( 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 end;

theorem Prelim12: :: GTARSKI4:12

for S being non empty satisfying_Tarski-model TarskiGeometryStruct
for b, c, p being POINT of S holds Middle reflection (p,c), reflection (p,b), reflection (p,(reflection (b,c)))

proof end;

definition

let S be satisfying_CongruenceSymmetry satisfying_CongruenceEquivalenceRelation satisfying_CongruenceIdentity satisfying_SegmentConstruction satisfying_SAS satisfying_BetweennessIdentity TarskiGeometryStruct ;
let a, b, c be POINT of S;

pred right_angle a,b,c means :: GTARSKI4:def 1
a,c equiv a, reflection (b,c);

end;

:: deftheorem defines right_angle GTARSKI4:def 1 :

8.2 Satz

theorem Satz8p2: :: GTARSKI4:13

for S being satisfying_Tarski-model TarskiGeometryStruct
for a, b, c being POINT of S st right_angle a,b,c holds
right_angle c,b,a

proof end;

theorem Lem01: :: GTARSKI4:14

for S being satisfying_Tarski-model TarskiGeometryStruct
for a being POINT of S holds reflection (a,a) = a

proof end;

8.3 Satz

theorem Satz8p3: :: GTARSKI4:15

for S being satisfying_Tarski-model TarskiGeometryStruct
for a, a9, b, c being POINT of S st right_angle a,b,c & a <> b & Collinear b,a,a9 holds
right_angle a9,b,c

proof end;

theorem :: GTARSKI4:16

for S being satisfying_Tarski-model TarskiGeometryStruct
for a, b, c being POINT of S st right_angle a,b,c holds
right_angle a,b, reflection (b,c)

proof end;

8.5 Satz

theorem Satz8p5: :: GTARSKI4:17

for S being satisfying_Tarski-model TarskiGeometryStruct
for a, b being POINT of S holds right_angle a,b,b

proof end;

8.6 Satz

theorem Satz8p6: :: GTARSKI4:18

for S being satisfying_Tarski-model TarskiGeometryStruct
for a, a9, b, c being POINT of S st right_angle a,b,c & right_angle a9,b,c & between a,c,a9 holds
b = c

proof end;

8.7 Satz

theorem Satz8p7: :: GTARSKI4:19

for S being satisfying_Tarski-model TarskiGeometryStruct
for a, b, c being POINT of S st right_angle a,b,c & right_angle a,c,b holds
b = c

proof end;

8.8 Satz

theorem Satz8p8: :: GTARSKI4:20

for S being satisfying_Tarski-model TarskiGeometryStruct
for a, b being POINT of S st right_angle a,b,a holds
a = b

proof end;

8.9 Satz

theorem Satz8p9: :: GTARSKI4:21

for S being satisfying_Tarski-model TarskiGeometryStruct
for a, b, c being POINT of S st right_angle a,b,c & Collinear a,b,c & not a = b holds
c = b

proof end;

8.10 Satz

theorem Satz8p10: :: GTARSKI4:22

for S being satisfying_Tarski-model TarskiGeometryStruct
for a, a9, b, b9, c, c9 being POINT of S st right_angle a,b,c & a,b,c cong a9,b9,c9 holds
right_angle a9,b9,c9

proof 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 :: GTARSKI4:def 2
( 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;

:: deftheorem defines are_orthogonal GTARSKI4:def 2 :

definition

let S be non empty satisfying_Tarski-model TarskiGeometryStruct ;
let A, A9 be Subset of S;

pred are_orthogonal A,A9 means :: GTARSKI4:def 3
ex x being POINT of S st are_orthogonal A,x,A9;

end;

:: deftheorem defines are_orthogonal GTARSKI4:def 3 :

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 :: GTARSKI4:def 4
( c <> d & are_orthogonal A,x, Line (c,d) );

end;

:: deftheorem defines are_lorthogonal GTARSKI4:def 4 :

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 :: GTARSKI4:def 5
( a <> b & c <> d & are_orthogonal Line (a,b),x, Line (c,d) );

end;

:: deftheorem defines are_orthogonal GTARSKI4:def 5 :

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 :: GTARSKI4:def 6
( a <> b & c <> d & are_orthogonal Line (a,b), Line (c,d) );

end;

:: deftheorem defines are_orthogonal GTARSKI4:def 6 :

8.12 Satz

theorem Satz8p12: :: GTARSKI4:23

for S being non empty satisfying_Tarski-model TarskiGeometryStruct
for A, A9 being Subset of S
for x being POINT of S holds
( are_orthogonal A,x,A9 iff are_orthogonal A9,x,A ) by Satz8p2;

8.13 Satz

theorem Satz8p13: :: GTARSKI4:24

for S being non empty satisfying_Tarski-model TarskiGeometryStruct
for A, A9 being Subset of S
for x being POINT of S holds
( 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 end;

8.14 (i) Satz

theorem Satz8p14p1: :: GTARSKI4:25

for S being non empty satisfying_Tarski-model TarskiGeometryStruct
for A, A9 being Subset of S st are_orthogonal A,A9 holds
A <> A9

proof end;

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 :: GTARSKI4:def 7
( A is_line & B is_line & A <> B & x in A & x in B );

end;

:: deftheorem defines Is GTARSKI4:def 7 :

8.14 (ii) Satz

theorem Satz8p14p2: :: GTARSKI4:26

for S being non empty satisfying_Tarski-model TarskiGeometryStruct
for A, A9 being Subset of S
for x being POINT of S holds
( are_orthogonal A,x,A9 iff ( are_orthogonal A,A9 & A,A9 Is x ) )

proof end;

8.14 (iii) Satz

theorem :: GTARSKI4:27

for S being non empty satisfying_Tarski-model TarskiGeometryStruct
for A, A9 being Subset of S
for x, y being POINT of S st are_orthogonal A,x,A9 & are_orthogonal A,y,A9 holds
x = y

proof end;

theorem Satz8p15a: :: GTARSKI4:28

for S being non empty satisfying_Tarski-model TarskiGeometryStruct
for x, a, b, c being POINT of S st Collinear a,b,x & are_orthogonal a,b,c,x holds
are_orthogonal a,b,x,c,x

proof end;

8.15 Satz

theorem Satz8p15: :: GTARSKI4:29

for S being non empty satisfying_Tarski-model TarskiGeometryStruct
for x, a, b, c being POINT of S st a <> b & Collinear a,b,x holds
( are_orthogonal a,b,c,x iff are_orthogonal a,b,x,c,x )

proof end;

8.16 Satz

theorem :: GTARSKI4:30

for S being non empty satisfying_Tarski-model TarskiGeometryStruct
for x, a, b, c, u being POINT of S st a <> b & Collinear a,b,x & Collinear a,b,u & u <> x holds
( are_orthogonal a,b,c,x iff ( not Collinear a,b,c & right_angle c,x,u ) )

proof end;

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 :: GTARSKI4:def 8
( Collinear a,b,x & are_orthogonal a,b,c,x );

end;

:: deftheorem defines is_foot GTARSKI4:def 8 :

8.18 Satz - Uniqueness

theorem Satz8p18Uniqueness: :: GTARSKI4:31

for S being non empty satisfying_Tarski-model TarskiGeometryStruct
for x, y, a, b, c being POINT of S st x is_foot a,b,c & y is_foot a,b,c holds
x = y

proof end;

theorem Satz8p18Lemma: :: GTARSKI4:32

for S being non empty satisfying_Tarski-model TarskiGeometryStruct
for x, y, z, a, b, c, c9, p, q, q9 being POINT of S st 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 holds
x <> y

proof end;

8.18 Satz - Existence

theorem Satz8p18pExistence: :: GTARSKI4:33

for S being non empty satisfying_Tarski-model satisfying_Lower_Dimension_Axiom TarskiGeometryStruct
for a, b, c being POINT of S st not Collinear a,b,c holds
ex x being POINT of S st x is_foot a,b,c

proof end;

8.20 Lemma

theorem Lemma8p20: :: GTARSKI4:34

for S being non empty satisfying_Tarski-model satisfying_Lower_Dimension_Axiom TarskiGeometryStruct
for a, b, c, p being POINT of S st right_angle a,b,c & Middle reflection (a,c),p, reflection (b,c) holds
( right_angle b,a,p & ( b <> c implies a <> p ) )

proof end;

theorem Satz8p21p1: :: GTARSKI4:35

for S being non empty satisfying_Tarski-model satisfying_Lower_Dimension_Axiom TarskiGeometryStruct
for a, b, c being POINT of S st not Collinear a,b,c holds
ex p, t being POINT of S st
( are_orthogonal a,b,p,a & Collinear a,b,t & between c,t,p )

proof end;

8.21 Satz

theorem Satz8p21: :: GTARSKI4:36

for S being non empty satisfying_Tarski-model satisfying_Lower_Dimension_Axiom TarskiGeometryStruct
for a, b, c being POINT of S st a <> b holds
ex p, t being POINT of S st
( are_orthogonal a,b,p,a & Collinear a,b,t & between c,t,p )

proof end;

theorem Th01: :: GTARSKI4:37

for S being non empty satisfying_Tarski-model satisfying_Lower_Dimension_Axiom TarskiGeometryStruct
for a, b, p, q being POINT of S st a <> b & a <> p & right_angle b,a,p & right_angle a,b,q holds
not Collinear p,a,q

proof end;

LemmaA3: for S being non empty satisfying_Tarski-model satisfying_Lower_Dimension_Axiom TarskiGeometryStruct
for a, b, p being POINT of S st a <> p holds
reflection (a,p) <> p

proof end;

theorem Satz8p22lemma: :: GTARSKI4:38

for S being non empty satisfying_Tarski-model satisfying_Lower_Dimension_Axiom 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 end;

8.22 Satz

theorem Satz8p22: :: GTARSKI4:39

for S being non empty satisfying_Tarski-model satisfying_Lower_Dimension_Axiom TarskiGeometryStruct
for a, b being POINT of S ex x being POINT of S st Middle a,x,b

proof end;

definition

let S be non empty satisfying_Tarski-model satisfying_Lower_Dimension_Axiom TarskiGeometryStruct ;
let a, b be POINT of S;

func Midpoint (a,b) -> POINT of S means :: GTARSKI4:def 9
Middle a,it,b;

existence by Satz8p22;
uniqueness by GTARSKI3:108;

end;

:: deftheorem defines Midpoint GTARSKI4:def 9 :

8.24 Lemma

theorem :: GTARSKI4:40

for S being non empty satisfying_Tarski-model satisfying_Lower_Dimension_Axiom 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 end;

theorem :: GTARSKI4:41

for S being non empty satisfying_Tarski-model satisfying_Lower_Dimension_Axiom TarskiGeometryStruct
for a, b, c, d, x, p, q being POINT of S st c in Line (a,b) & d in Line (a,b) & a <> b & c <> d holds
Line (a,b) = Line (c,d) by Prelim11;

theorem :: GTARSKI4:42

for S being non empty satisfying_Tarski-model satisfying_Lower_Dimension_Axiom TarskiGeometryStruct
for a, b, c, d, x, p, q being POINT of S st c in Line (a,b) & d in Line (a,b) & c <> d & are_orthogonal a,b,x,p,q holds
are_orthogonal c,d,x,p,q by Prelim11;

theorem :: GTARSKI4:43

for S being non empty satisfying_Tarski-model satisfying_Lower_Dimension_Axiom TarskiGeometryStruct
for a, b, c, d, p, q being POINT of S st p in Line (a,b) & q in Line (a,b) & a <> b & are_orthogonal p,q,c,d holds
are_orthogonal a,b,c,d by Prelim11;

theorem :: GTARSKI4:44

for S being non empty satisfying_Tarski-model satisfying_Lower_Dimension_Axiom TarskiGeometryStruct
for a, b, c, d being POINT of S st a <> b & b <> c & c <> d & a <> c & a <> d & b <> d & are_orthogonal b,a,a,c & Collinear a,c,d holds
are_orthogonal b,a,a,d

proof end;

theorem :: GTARSKI4:45

for S being non empty satisfying_Tarski-model satisfying_Lower_Dimension_Axiom TarskiGeometryStruct
for a, b, p, q being POINT of S st are_orthogonal a,b,p,q holds
are_orthogonal a,b,q,p ;

theorem ExtPerp5: :: GTARSKI4:46

for S being non empty satisfying_Tarski-model satisfying_Lower_Dimension_Axiom TarskiGeometryStruct
for a, b, c, d, p, q being POINT of S st p in Line (a,b) & q in Line (a,b) & p <> q & are_orthogonal a,b,c,d holds
are_orthogonal p,q,c,d by Prelim11;

theorem :: GTARSKI4:47

for S being non empty satisfying_Tarski-model satisfying_Lower_Dimension_Axiom TarskiGeometryStruct
for a, b, c, d, p, q being POINT of S st Collinear a,b,p & Collinear a,b,q & p <> q & are_orthogonal a,b,c,d holds
are_orthogonal p,q,c,d

proof end;

theorem :: GTARSKI4:48

for S being non empty satisfying_Tarski-model satisfying_Lower_Dimension_Axiom TarskiGeometryStruct
for a, b, c, d, p, q being POINT of S st p in Line (a,b) & q in Line (a,b) & p <> q & a <> b & are_orthogonal c,d,p,q holds
are_orthogonal c,d,a,b by Prelim11;