begin
:: deftheorem Def1 defines are_concurrent PROJRED2:def 1 :
for IPS being IncProjSp
for A, B, C being LINE of IPS holds
( A,B,C are_concurrent iff ex o being Element of the Points of IPS st
( o on A & o on B & o on C ) );
:: deftheorem defines CHAIN PROJRED2:def 2 :
for IPS being IncProjSp
for Z being LINE of IPS holds CHAIN Z = { z where z is POINT of IPS : z on Z } ;
:: deftheorem Def3 defines Projection PROJRED2:def 3 :
for IPP being 2-dimensional Desarguesian IncProjSp
for b2 being PartFunc of the Points of IPP, the Points of IPP holds
( b2 is Projection of IPP iff ex a being POINT of IPP ex A, B being LINE of IPP st
( not a on A & not a on B & b2 = IncProj (A,a,B) ) );
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)) )