:: On Projections in Projective Planes. Part II
:: by Eugeniusz Kusak, Wojciech Leo\'nczuk and Krzysztof Pra\.zmowski
::
:: Received October 31, 1990
:: Copyright (c) 1990 Association of Mizar Users
:: deftheorem Def1 defines are_concurrent PROJRED2:def 1 :
:: deftheorem defines CHAIN PROJRED2:def 2 :
:: deftheorem Def3 defines Projection PROJRED2:def 3 :
theorem Th1: :: PROJRED2:1
theorem :: PROJRED2:2
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: :: PROJRED2:3
theorem :: PROJRED2:4
canceled;
theorem Th5: :: PROJRED2:5
theorem Th6: :: PROJRED2:6
theorem :: PROJRED2:7
theorem Th8: :: PROJRED2:8
theorem Th9: :: PROJRED2:9
theorem :: PROJRED2:10
theorem Th11: :: PROJRED2:11
theorem :: PROJRED2:12
theorem :: PROJRED2:13
theorem :: PROJRED2:14
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: :: PROJRED2:15
for
IPP being
2-dimensional Desarguesian IncProjSp for
a,
b,
c,
q,
d,
p,
pp' 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 <> b &
b <> 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 &
pp' on O2 &
d on O3 &
b on O3 &
pp' on O3 &
pp' on Q &
Q <> C &
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: :: PROJRED2:16
for
IPP being
2-dimensional Desarguesian IncProjSp for
a,
b,
q,
c,
o,
o'',
d,
o',
oo' 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,o'',d} on B &
{c,d,o'} on C &
{a,b,d} on O &
{c,oo'} on Q &
{a,o,o'} on O1 &
{b,o',oo'} on O2 &
{o,oo',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: :: PROJRED2:17
for
IPP being
2-dimensional Desarguesian IncProjSp for
a,
b,
c,
p,
d,
q,
pp' 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 & 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,pp'} on Q &
{a,d,p} on O1 &
{q,p,pp'} on O2 &
{b,d,pp'} on O3 holds
(
q <> a &
q <> b & not
q on A & not
q on Q )
theorem Th18: :: PROJRED2:18
for
IPP being
2-dimensional Desarguesian IncProjSp for
a,
b,
c,
o,
o'',
d,
o',
oo',
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,o'',d} on B &
{c,d,o'} on C &
{a,b,d} on O &
{c,oo'} on Q &
{a,o,o'} on O1 &
{b,o',oo'} on O2 &
{o,oo',q} on O3 &
q on O holds
( not
q on A & not
q on Q &
b <> q )
theorem Th19: :: PROJRED2:19
for
IPP being
2-dimensional Desarguesian IncProjSp for
a,
b,
q,
c,
p,
d,
pp' 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 & 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,pp'} on Q &
{a,d,p} on O1 &
{q,p,pp'} on O2 &
{b,d,pp'} on O3 holds
(
Q <> A &
Q <> C & not
q on Q & not
b on Q )
theorem Th20: :: PROJRED2:20
for
IPP being
2-dimensional Desarguesian IncProjSp for
a,
b,
q,
c,
o,
o'',
d,
o',
oo' 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,o'',d} on B &
{c,d,o'} on C &
{a,b,d} on O &
{c,oo'} on Q &
{a,o,o'} on O1 &
{b,o',oo'} on O2 &
{o,oo',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: :: PROJRED2:21
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 :: PROJRED2:22
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 :: PROJRED2:23
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: :: PROJRED2:24
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 :: PROJRED2:25
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) )