let S be 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 )
let a, b, p, q, r, t be POINT of S; ( 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 implies ex x being POINT of S st
( Middle a,x,b & Middle p,x,r ) )
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
; ex x being POINT of S st
( Middle a,x,b & Middle p,x,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 being 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
( b = t or b <> t )
;
suppose
b <> t
;
Collinear a,b,xthen 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
Collinear a,
b,
x
by GTARSKI3:45;
verum end; end;
end;
consider x9 being 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 being 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 ( not Collinear a,p,b & p <> r & a,p equiv b,r & p,b equiv r,a & Collinear a,x,b & Collinear p,x,r )thus
not
Collinear a,
p,
b
by A21, GTARSKI3:45;
( p <> r & a,p equiv b,r & p,b equiv r,a & Collinear a,x,b & Collinear p,x,r )thus
p <> r
( a,p equiv b,r & p,b equiv r,a & Collinear a,x,b & Collinear p,x,r )proof
assume A23:
p = r
;
contradiction
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;
verum
end; thus
a,
p equiv b,
r
by A6;
( p,b equiv r,a & Collinear a,x,b & Collinear p,x,r )A24:
x <> a
proof
assume
x = a
;
contradiction
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;
verum
end; thus
p,
b equiv r,
a
( Collinear a,x,b & Collinear p,x,r )proof
set p9 =
reflection (
a,
p);
consider r9 being
POINT of
S such that A26:
between reflection (
a,
p),
x,
r9
and A27:
x,
r9 equiv x,
r
by GTARSKI1:def 8;
consider m being
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 <> reflection (
a,
p)
by A1, LemmaA3;
Collinear p,
a,
reflection (
a,
p)
by GTARSKI3:def 13, Prelim08;
then A32:
Line (
a,
p)
= Line (
p,
(reflection (a,p)))
by A31, Prelim07, A1;
A33:
not
Collinear x,
p,
reflection (
a,
p)
proof
assume
Collinear x,
p,
reflection (
a,
p)
;
contradiction
then
Collinear p,
reflection (
a,
p),
x
by GTARSKI3:45;
then
x in Line (
a,
p)
by A32, LemmaA1;
hence
contradiction
by A30, A24, Satz8p9, A1, LemmaA2;
verum
end;
(
between reflection (
a,
p),
x,
r9 &
between p,
x,
r &
x,
reflection (
a,
p)
equiv x,
p &
x,
r9 equiv x,
r &
Middle reflection (
a,
p),
a,
p &
Middle r9,
m,
r )
by A9, GTARSKI3:14, A26, A28, A30, Prelim01, A27, GTARSKI3:96, GTARSKI3:def 13;
then A34:
between a,
x,
m
by GTARSKI3:115;
A35:
x <> m
proof
assume A36:
x = m
;
contradiction
Collinear x,
r9,
reflection (
a,
p)
by A26, Prelim08a;
then A37:
reflection (
a,
p)
in Line (
x,
r9)
by LemmaA1;
A38:
Collinear x,
r,
r9
by A36, A28, Prelim08a;
per cases
( x <> r or x = r )
;
suppose A39:
x <> r
;
contradictionthen
x <> r9
by A27, GTARSKI1:5, GTARSKI3:4;
then
Line (
x,
r)
= Line (
x,
r9)
by A39, A38, Prelim07;
then
Collinear reflection (
a,
p),
x,
r
by A37, LemmaA2;
then A40:
Collinear x,
r,
reflection (
a,
p)
by GTARSKI3:45;
Collinear x,
r,
p
by A9, Prelim08a;
hence
contradiction
by A33, A40, A39, Prelim08b;
verum end; 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, GTARSKI3:100;
now ( a <> b & r <> m & are_orthogonal Line (a,b), Line (r,m) )thus
a <> b
by A2;
( r <> m & are_orthogonal Line (a,b), Line (r,m) )thus A45:
r <> m
by A43, LemmaA2, A20, A2, A22, Satz8p9;
are_orthogonal Line (a,b), Line (r,m)thus
are_orthogonal Line (
a,
b),
Line (
r,
m)
verumproof
now ( Line (a,b) is_line & Line (r,m) is_line & m in Line (a,b) & m in Line (r,m) & ex u, v being POINT of S st
( u <> m & v <> m & u in Line (a,b) & v in Line (r,m) & right_angle u,m,v ) )thus
Line (
a,
b)
is_line
by A2, GTARSKI3:def 11;
( Line (r,m) is_line & m in Line (a,b) & m in Line (r,m) & ex u, v being POINT of S st
( u <> m & v <> m & u in Line (a,b) & v in Line (r,m) & right_angle u,m,v ) )thus
Line (
r,
m)
is_line
by A45, GTARSKI3:def 11;
( m in Line (a,b) & m in Line (r,m) & ex u, v being POINT of S st
( u <> m & v <> m & u in Line (a,b) & v in Line (r,m) & right_angle u,m,v ) )thus
m in Line (
a,
b)
by A10, LemmaA1, A41, A24, A2, GTARSKI3:82;
( m in Line (r,m) & ex u, v being POINT of S st
( u <> m & v <> m & u in Line (a,b) & v in Line (r,m) & right_angle u,m,v ) )thus
m in Line (
r,
m)
by GTARSKI3:83;
ex u, v being POINT of S st
( u <> m & v <> m & u in Line (a,b) & v in Line (r,m) & right_angle u,m,v )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 being
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;
verum end;
hence
are_orthogonal Line (
a,
b),
Line (
r,
m)
by Satz8p13;
verum
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 ( Collinear a,b,b & are_orthogonal a,b,r,b )thus
Collinear a,
b,
b
by Prelim05;
are_orthogonal a,b,r,bthus
are_orthogonal a,
b,
r,
b
verumproof
set A =
Line (
a,
b);
set A9 =
Line (
r,
b);
now ( Line (a,b) is_line & Line (r,b) is_line & b in Line (a,b) & b in Line (r,b) & ex u, v being POINT of S st
( u in Line (a,b) & v in Line (r,b) & u <> b & v <> b & right_angle u,b,v ) )thus
Line (
a,
b)
is_line
by A2, GTARSKI3:def 11;
( Line (r,b) is_line & b in Line (a,b) & b in Line (r,b) & ex u, v being POINT of S st
( u in Line (a,b) & v in Line (r,b) & u <> b & v <> b & right_angle u,b,v ) )thus
Line (
r,
b)
is_line
by A22, GTARSKI3:def 11;
( b in Line (a,b) & b in Line (r,b) & ex u, v being POINT of S st
( u in Line (a,b) & v in Line (r,b) & u <> b & v <> b & right_angle u,b,v ) )thus
(
b in Line (
a,
b) &
b in Line (
r,
b) )
by GTARSKI3:83;
ex u, v being POINT of S st
( u in Line (a,b) & v in Line (r,b) & u <> b & v <> b & right_angle u,b,v )thus
ex
u,
v being
POINT of
S st
(
u in Line (
a,
b) &
v in Line (
r,
b) &
u <> b &
v <> b &
right_angle u,
b,
v )
verumproof
take
a
;
ex v being POINT of S st
( a in Line (a,b) & v in Line (r,b) & a <> b & v <> b & right_angle a,b,v )
take
r
;
( a in Line (a,b) & r in Line (r,b) & a <> b & r <> b & right_angle a,b,r )
thus
a in Line (
a,
b)
by GTARSKI3:83;
( r in Line (r,b) & a <> b & r <> b & right_angle a,b,r )
thus
r in Line (
r,
b)
by GTARSKI3:83;
( a <> b & r <> b & right_angle a,b,r )
thus
a <> b
by A2;
( r <> b & right_angle a,b,r )
thus
r <> b
by A6, GTARSKI1:5, A1;
right_angle a,b,r
thus
right_angle a,
b,
r
by A20, Satz8p2;
verum
end; end;
then
are_orthogonal Line (
a,
b),
Line (
r,
b)
by Satz8p13;
hence
are_orthogonal a,
b,
r,
b
by A6, GTARSKI1:5, A1;
verum
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 ( Middle reflection (a,p),a,p & between reflection (a,p),a,p & between r,b,r9 & reflection (a,p),p equiv r,r9 & a,p equiv b,r9 & reflection (a,p),r equiv r, reflection (a,p) & p,r equiv r9, reflection (a,p) )A51:
Middle p,
a,
reflection (
a,
p)
by GTARSKI3:def 13;
thus A52:
Middle reflection (
a,
p),
a,
p
by GTARSKI3:96, GTARSKI3:def 13;
( between reflection (a,p),a,p & between r,b,r9 & reflection (a,p),p equiv r,r9 & a,p equiv b,r9 & reflection (a,p),r equiv r, reflection (a,p) & p,r equiv r9, reflection (a,p) )hence
between reflection (
a,
p),
a,
p
by GTARSKI3:def 12;
( between r,b,r9 & reflection (a,p),p equiv r,r9 & a,p equiv b,r9 & reflection (a,p),r equiv r, reflection (a,p) & p,r equiv r9, reflection (a,p) )thus
between r,
b,
r9
by A50, GTARSKI3:def 12;
( reflection (a,p),p equiv r,r9 & a,p equiv b,r9 & reflection (a,p),r equiv r, reflection (a,p) & p,r equiv r9, reflection (a,p) )A53:
a,
p equiv a,
reflection (
a,
p)
by A51, GTARSKI3:def 12;
A54:
m,
r9 equiv m,
r
by A28, GTARSKI3:def 12;
(
between reflection (
a,
p),
a,
p &
between r,
m,
r9 &
reflection (
a,
p),
a equiv r,
m &
a,
p equiv m,
r9 )
by A53, A29, GTARSKI3:def 12, A6, A54, A49, Prelim03, A52;
hence
reflection (
a,
p),
p equiv r,
r9
by GTARSKI3:11;
( a,p equiv b,r9 & reflection (a,p),r equiv r, reflection (a,p) & p,r equiv r9, reflection (a,p) )thus
a,
p equiv b,
r9
by A6, A54, A49, Prelim03;
( reflection (a,p),r equiv r, reflection (a,p) & p,r equiv r9, reflection (a,p) )
reflection (
a,
p),
r equiv reflection (
a,
p),
r
by GTARSKI3:1;
hence
reflection (
a,
p),
r equiv r,
reflection (
a,
p)
by Prelim01;
p,r equiv r9, reflection (a,p)
(
between p,
x,
r &
between reflection (
a,
p),
x,
r9 &
p,
x equiv reflection (
a,
p),
x &
x,
r equiv x,
r9 )
by A26, A30, A9, GTARSKI3:14, Prelim01, A27;
then
p,
r equiv reflection (
a,
p),
r9
by GTARSKI3:11;
hence
p,
r equiv r9,
reflection (
a,
p)
by Prelim01;
verum end;
then
reflection (
a,
p),
a,
p,
r IFS r,
b,
r9,
reflection (
a,
p)
by GTARSKI3:def 5;
then
a,
r equiv b,
reflection (
a,
p)
by GTARSKI3:41;
hence
p,
b equiv r,
a
by A18, A19, Prelim03;
verum
end; thus
Collinear a,
x,
b
by A10, GTARSKI3:45;
Collinear p,x,r
Collinear r,
x,
p
by A9, GTARSKI1:def 17;
hence
Collinear p,
x,
r
by GTARSKI3:45;
verum end;
then
( Middle a,x,b & Middle p,x,r )
by GTARSKI3:112;
hence
ex x being POINT of S st
( Middle a,x,b & Middle p,x,r )
; verum