:: 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
for a, b being POINT of S holds Line (a,b) = Line (b,a) 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 :
for S being satisfying_CongruenceSymmetry satisfying_CongruenceEquivalenceRelation satisfying_CongruenceIdentity satisfying_SegmentConstruction satisfying_SAS satisfying_BetweennessIdentity TarskiGeometryStruct
for a, b, c being POINT of S holds
( right_angle a,b,c iff a,c equiv a, reflection (b,c) );

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

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

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

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

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

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

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

:: WP: 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 :
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 & ( for u, v being POINT of S st u in A & v in A9 holds
right_angle u,x,v ) ) );

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 :
for S being non empty satisfying_Tarski-model TarskiGeometryStruct
for A, A9 being Subset of S holds
( are_orthogonal A,A9 iff ex x being POINT of S st are_orthogonal A,x,A9 );

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 :
for S being non empty satisfying_Tarski-model TarskiGeometryStruct
for A being Subset of S
for x, c, d being POINT of S holds
( are_lorthogonal A,x,c,d iff ( c <> d & are_orthogonal A,x, Line (c,d) ) );

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 :
for S being non empty satisfying_Tarski-model TarskiGeometryStruct
for a, b, x, c, d being POINT of S holds
( are_orthogonal a,b,x,c,d iff ( a <> b & c <> d & are_orthogonal Line (a,b),x, Line (c,d) ) );

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 :
for S being non empty satisfying_Tarski-model TarskiGeometryStruct
for a, b, c, d being POINT of S holds
( are_orthogonal a,b,c,d iff ( a <> b & c <> d & are_orthogonal Line (a,b), Line (c,d) ) );

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

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

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

:: WP: 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 :
for S being non empty TarskiGeometryStruct
for A, B being Subset of S
for x being POINT of S holds
( A,B Is x iff ( A is_line & B is_line & A <> B & x in A & x in B ) );

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

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

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

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

:: WP: 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 :
for S being non empty satisfying_Tarski-model TarskiGeometryStruct
for a, b, c, x being POINT of S holds
( x is_foot a,b,c iff ( Collinear a,b,x & are_orthogonal a,b,c,x ) );

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

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

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

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

:: WP: 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
ex b1 being POINT of S st Middle a,b1,b by Satz8p22;
uniqueness
for b1, b2 being POINT of S st Middle a,b1,b & Middle a,b2,b holds
b1 = b2 by GTARSKI3:108;
end;

:: deftheorem defines Midpoint GTARSKI4:def 9 :
for S being non empty satisfying_Tarski-model satisfying_Lower_Dimension_Axiom TarskiGeometryStruct
for a, b, b4 being POINT of S holds
( b4 = Midpoint (a,b) iff Middle a,b4,b );

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