begin
:: deftheorem Def1 defines are_concurrent PROJRED2:def 1 :
:: deftheorem defines CHAIN PROJRED2:def 2 :
:: deftheorem Def3 defines Projection PROJRED2:def 3 :
theorem Th1:
theorem
for
IPP being
2-dimensional Desarguesian IncProjSp for
A,
B,
C being
LINE of
IPP st
A,
B,
C are_concurrent holds
(
A,
C,
B are_concurrent &
B,
A,
C are_concurrent &
B,
C,
A are_concurrent &
C,
A,
B are_concurrent &
C,
B,
A are_concurrent )
theorem Th3:
theorem
canceled;
theorem Th5:
theorem Th6:
theorem
theorem Th8:
theorem Th9:
theorem
theorem Th11:
theorem
theorem
theorem
for
IPP being
2-dimensional Desarguesian IncProjSp for
o1,
o2 being
POINT of
IPP for
O1,
O2,
O3 being
LINE of
IPP st not
o1 on O1 & not
o1 on O2 & not
o2 on O2 & not
o2 on O3 &
O1,
O2,
O3 are_concurrent &
O1 <> O3 holds
ex
o being
POINT of
IPP st
( not
o on O1 & not
o on O3 &
(IncProj O2,o2,O3) * (IncProj O1,o1,O2) = IncProj O1,
o,
O3 )
theorem Th15:
for
IPP being
2-dimensional Desarguesian IncProjSp for
a,
b,
c,
d,
p,
q,
pp9 being
POINT of
IPP for
A,
B,
C,
Q,
O,
O1,
O2,
O3 being
LINE of
IPP st not
a on A & not
b on B & not
a on C & not
b on C & not
A,
B,
C are_concurrent &
c on A &
c on C &
c on Q & not
b on Q &
A <> Q &
a on O &
b on O & not
B,
C,
O are_concurrent &
d on C &
d on B &
a on O1 &
d on O1 &
p on A &
p on O1 &
q on O &
q on O2 &
p on O2 &
pp9 on O2 &
d on O3 &
b on O3 &
pp9 on O3 &
pp9 on Q &
q <> a & not
q on A & not
q on Q holds
(IncProj C,b,B) * (IncProj A,a,C) = (IncProj Q,b,B) * (IncProj A,q,Q)
theorem Th16:
for
IPP being
2-dimensional Desarguesian IncProjSp for
a,
b,
q,
c,
o,
o99,
d,
o9,
oo9 being
POINT of
IPP for
A,
C,
B,
Q,
O,
O1,
O2,
O3 being
LINE of
IPP st not
a on A & not
a on C & not
b on B & not
b on C & not
b on Q & not
A,
B,
C are_concurrent &
a <> b &
b <> q &
A <> Q &
{c,o} on A &
{o,o99,d} on B &
{c,d,o9} on C &
{a,b,d} on O &
{c,oo9} on Q &
{a,o,o9} on O1 &
{b,o9,oo9} on O2 &
{o,oo9,q} on O3 &
q on O holds
(IncProj C,b,B) * (IncProj A,a,C) = (IncProj Q,b,B) * (IncProj A,q,Q)
theorem Th17:
for
IPP being
2-dimensional Desarguesian IncProjSp for
a,
b,
c,
p,
d,
q,
pp9 being
POINT of
IPP for
A,
C,
Q,
B,
O,
O1,
O2,
O3 being
LINE of
IPP st not
a on A & not
a on C & not
b on C & not
b on Q & not
A,
B,
C are_concurrent & not
B,
C,
O are_concurrent &
A <> Q &
Q <> C &
a <> b &
{c,p} on A &
d on B &
{c,d} on C &
{a,b,q} on O &
{c,pp9} on Q &
{a,d,p} on O1 &
{q,p,pp9} on O2 &
{b,d,pp9} on O3 holds
(
q <> a &
q <> b & not
q on A & not
q on Q )
theorem Th18:
for
IPP being
2-dimensional Desarguesian IncProjSp for
a,
b,
c,
o,
o99,
d,
o9,
oo9,
q being
POINT of
IPP for
A,
C,
B,
Q,
O,
O1,
O2,
O3 being
LINE of
IPP st not
a on A & not
a on C & not
b on B & not
b on C & not
b on Q & not
A,
B,
C are_concurrent &
a <> b &
A <> Q &
{c,o} on A &
{o,o99,d} on B &
{c,d,o9} on C &
{a,b,d} on O &
{c,oo9} on Q &
{a,o,o9} on O1 &
{b,o9,oo9} on O2 &
{o,oo9,q} on O3 &
q on O holds
( not
q on A & not
q on Q &
b <> q )
theorem Th19:
for
IPP being
2-dimensional Desarguesian IncProjSp for
a,
b,
q,
c,
p,
d,
pp9 being
POINT of
IPP for
A,
C,
B,
O,
Q,
O1,
O2,
O3 being
LINE of
IPP st not
a on A & not
a on C & not
b on C & not
q on A & not
A,
B,
C are_concurrent & not
B,
C,
O are_concurrent &
a <> b &
b <> q &
q <> a &
{c,p} on A &
d on B &
{c,d} on C &
{a,b,q} on O &
{c,pp9} on Q &
{a,d,p} on O1 &
{q,p,pp9} on O2 &
{b,d,pp9} on O3 holds
(
Q <> A &
Q <> C & not
q on Q & not
b on Q )
theorem Th20:
for
IPP being
2-dimensional Desarguesian IncProjSp for
a,
b,
q,
c,
o,
o99,
d,
o9,
oo9 being
POINT of
IPP for
A,
C,
B,
O,
Q,
O1,
O2,
O3 being
LINE of
IPP st not
a on A & not
a on C & not
b on B & not
b on C & not
q on A & not
A,
B,
C are_concurrent &
a <> b &
b <> q &
{c,o} on A &
{o,o99,d} on B &
{c,d,o9} on C &
{a,b,d} on O &
{c,oo9} on Q &
{a,o,o9} on O1 &
{b,o9,oo9} on O2 &
{o,oo9,q} on O3 &
q on O holds
( not
b on Q & not
q on Q &
A <> Q )
Lm1:
for IPP being 2-dimensional Desarguesian IncProjSp
for a, b being POINT of IPP
for A, B, C, Q, O being LINE of IPP st not a on A & not b on B & not a on C & not b on C & not A,B,C are_concurrent & A,C,Q are_concurrent & not b on Q & A <> Q & a <> b & a on O & b on O & not B,C,O are_concurrent holds
ex q being POINT of IPP st
( q on O & not q on A & not q on Q & (IncProj C,b,B) * (IncProj A,a,C) = (IncProj Q,b,B) * (IncProj A,q,Q) )
Lm2:
for IPP being 2-dimensional Desarguesian IncProjSp
for a, b being POINT of IPP
for A, B, C, Q, O being LINE of IPP st not a on A & not b on B & not a on C & not b on C & not A,B,C are_concurrent & A,C,Q are_concurrent & not b on Q & A <> Q & a <> b & a on O & b on O & B,C,O are_concurrent holds
ex q being POINT of IPP st
( q on O & not q on A & not q on Q & (IncProj C,b,B) * (IncProj A,a,C) = (IncProj Q,b,B) * (IncProj A,q,Q) )
theorem Th21:
for
IPP being
2-dimensional Desarguesian IncProjSp for
a,
b being
POINT of
IPP for
A,
B,
C,
Q,
O being
LINE of
IPP st not
a on A & not
b on B & not
a on C & not
b on C & not
A,
B,
C are_concurrent &
A,
C,
Q are_concurrent & not
b on Q &
A <> Q &
a <> b &
a on O &
b on O holds
ex
q being
POINT of
IPP st
(
q on O & not
q on A & not
q on Q &
(IncProj C,b,B) * (IncProj A,a,C) = (IncProj Q,b,B) * (IncProj A,q,Q) )
theorem
for
IPP being
2-dimensional Desarguesian IncProjSp for
a,
b being
POINT of
IPP for
A,
B,
C,
Q,
O being
LINE of
IPP st not
a on A & not
b on B & not
a on C & not
b on C & not
A,
B,
C are_concurrent &
B,
C,
Q are_concurrent & not
a on Q &
B <> Q &
a <> b &
a on O &
b on O holds
ex
q being
POINT of
IPP st
(
q on O & not
q on B & not
q on Q &
(IncProj C,b,B) * (IncProj A,a,C) = (IncProj Q,q,B) * (IncProj A,a,Q) )
theorem
for
IPP being
2-dimensional Desarguesian IncProjSp for
a,
b,
c,
d,
s,
r being
POINT of
IPP for
A,
B,
C,
S,
R,
Q being
LINE of
IPP st not
a on A & not
b on B & not
a on C & not
b on C & not
a on B & not
b on A &
c on A &
c on C &
d on B &
d on C &
a on S &
d on S &
c on R &
b on R &
s on A &
s on S &
r on B &
r on R &
s on Q &
r on Q & not
A,
B,
C are_concurrent holds
(IncProj C,b,B) * (IncProj A,a,C) = (IncProj Q,a,B) * (IncProj A,b,Q)
Lm3:
for IPP being 2-dimensional Desarguesian IncProjSp
for a, b, c, q being POINT of IPP
for A, B, C, O being LINE of IPP st not a on A & not b on B & not a on C & not b on C & c on A & c on C & a <> b & a on O & b on O & q on O & not q on A & q <> b & not A,B,C are_concurrent & not B,C,O are_concurrent holds
ex Q being LINE of IPP st
( c on Q & not b on Q & not q on Q & (IncProj C,b,B) * (IncProj A,a,C) = (IncProj Q,b,B) * (IncProj A,q,Q) )
Lm4:
for IPP being 2-dimensional Desarguesian IncProjSp
for a, b, c, q being POINT of IPP
for A, B, C, O being LINE of IPP st not a on A & not b on B & not a on C & not b on C & c on A & c on C & a <> b & a on O & b on O & q on O & not q on A & q <> b & not A,B,C are_concurrent & B,C,O are_concurrent holds
ex Q being LINE of IPP st
( c on Q & not b on Q & not q on Q & (IncProj C,b,B) * (IncProj A,a,C) = (IncProj Q,b,B) * (IncProj A,q,Q) )
theorem Th24:
for
IPP being
2-dimensional Desarguesian IncProjSp for
a,
b,
q being
POINT of
IPP for
A,
B,
C,
O being
LINE of
IPP st not
a on A & not
b on B & not
a on C & not
b on C &
a <> b &
a on O &
b on O &
q on O & not
q on A &
q <> b & not
A,
B,
C are_concurrent holds
ex
Q being
LINE of
IPP st
(
A,
C,
Q are_concurrent & not
b on Q & not
q on Q &
(IncProj C,b,B) * (IncProj A,a,C) = (IncProj Q,b,B) * (IncProj A,q,Q) )
theorem
for
IPP being
2-dimensional Desarguesian IncProjSp for
a,
b,
q being
POINT of
IPP for
A,
B,
C,
O being
LINE of
IPP st not
a on A & not
b on B & not
a on C & not
b on C &
a <> b &
a on O &
b on O &
q on O & not
q on B &
q <> a & not
A,
B,
C are_concurrent holds
ex
Q being
LINE of
IPP st
(
B,
C,
Q are_concurrent & not
a on Q & not
q on Q &
(IncProj C,b,B) * (IncProj A,a,C) = (IncProj Q,q,B) * (IncProj A,a,Q) )