Loading [MathJax]/extensions/tex2jax.js
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)
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
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 )
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 )
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 )
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) )
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 )
theorem Prelim10:
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) )
theorem Prelim11:
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) )
theorem Satz8p10:
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
::
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) ) );
theorem Satz8p15a:
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
theorem Satz8p15:
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 )
theorem
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 ) )
::
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 ) );
theorem Satz8p18Uniqueness:
theorem Satz8p18Lemma:
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
theorem Satz8p18pExistence:
theorem Lemma8p20:
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 ) )
theorem Satz8p21p1:
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 )
theorem Satz8p21:
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 )
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
theorem Satz8p22lemma:
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
theorem
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 )
theorem
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
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
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
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
theorem ExtPerp5:
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
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
theorem
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;