Journal of Formalized Mathematics
Volume 2, 1990
University of Bialystok
Copyright (c) 1990 Association of Mizar Users

### On Projections in Projective Planes --- Part II

by
Eugeniusz Kusak,
Wojciech Leonczuk, and
Krzysztof Prazmowski

MML identifier: PROJRED2
[ Mizar article, MML identifier index ]

```environ

vocabulary INCPROJ, INCSP_1, AFF_2, ANALOAF, PARTFUN1, PROJRED1, FUNCT_1,
RELAT_1, PROJRED2;
notation TARSKI, SUBSET_1, RELAT_1, RELSET_1, INCSP_1, INCPROJ, PARTFUN1,
FUNCT_1, PROJRED1;
constructors PROJRED1, XBOOLE_0;
clusters INCPROJ, FUNCT_1, RELSET_1, ZFMISC_1, XBOOLE_0;
requirements SUBSET, BOOLE;

begin

reserve IPS for IncProjSp,
z for POINT of IPS;

definition let IPS; let A,B,C be LINE of IPS;
pred A,B,C are_concurrent means
:: PROJRED2:def 1
ex o being Element of the Points of IPS st o on A & o on B & o on C;
end;

definition let IPS; let Z be LINE of IPS;
func CHAIN(Z) -> Subset of the Points of IPS equals
:: PROJRED2:def 2
{z: z on Z};
end;

reserve IPP for Desarguesian 2-dimensional IncProjSp,
a,b,c,d,p,pp',q,o,o',o'',oo' for POINT of IPP,
r,s,x,y,o1,o2 for POINT of IPP,
O1,O2,O3,O4,A,B,C,O,Q,Q1,Q2,Q3,R,S,X for LINE of IPP;

definition let IPP;
mode Projection of IPP -> PartFunc of the Points of IPP,the Points of IPP
means
:: PROJRED2:def 3
ex a,A,B st not a on A & not a on B & it = IncProj(A,a,B);
end;

theorem :: PROJRED2:1
A=B or B=C or C=A implies A,B,C are_concurrent;

theorem :: PROJRED2:2
A,B,C are_concurrent implies 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 :: PROJRED2:3
not o on A & not o on B & y on B implies ex x st x on A & IncProj
(A,o,B).x = y;

canceled;

theorem :: PROJRED2:5
not o on A & not o on B implies dom IncProj(A,o,B) = CHAIN(A);

theorem :: PROJRED2:6
not o on A & not o on B implies rng IncProj(A,o,B) = CHAIN(B);

theorem :: PROJRED2:7
for x being set holds x in CHAIN(A) iff ex a st x=a & a on A;

theorem :: PROJRED2:8
not o on A & not o on B implies IncProj(A,o,B) is one-to-one;

theorem :: PROJRED2:9
not o on A & not o on B implies IncProj(A,o,B)" = IncProj(B,o,A);

theorem :: PROJRED2:10
for f being Projection of IPP holds f" is Projection of IPP;

theorem :: PROJRED2:11
not o on A implies IncProj(A,o,A) = id CHAIN(A);

theorem :: PROJRED2:12
id CHAIN(A) is Projection of IPP;

theorem :: PROJRED2:13
not o on A & not o on B & not o on C implies IncProj(C,o,B)*IncProj(A,o,C) =
IncProj(A,o,B);

theorem :: PROJRED2:14
not o1 on O1 & not o1 on O2 & not o2 on O2 & not o2 on O3 &
O1,O2,O3 are_concurrent &
O1<>O3 implies ex o st not o on O1 & not o on O3 &
IncProj(O2,o2,O3)*IncProj(O1,o1,O2) = IncProj(O1,o,O3);

theorem :: PROJRED2:15
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 implies
IncProj(C,b,B)*IncProj(A,a,C) = IncProj(Q,b,B)*IncProj(A,q,Q);

theorem :: PROJRED2:16
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
implies IncProj(C,b,B)*IncProj(A,a,C) = IncProj(Q,b,B)*IncProj(A,q,Q);

theorem :: PROJRED2:17
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
implies q<>a & q<>b & not q on A & not q on Q;

theorem :: PROJRED2:18
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 implies
not q on A & not q on Q & b<>q;

theorem :: PROJRED2:19
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
implies Q<>A & Q<>C & not q on Q & not b on Q;

theorem :: PROJRED2:20
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 implies
not b on Q & not q on Q & A<>Q;

theorem :: PROJRED2:21
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 implies
ex q 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
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 implies
ex q 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
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
implies IncProj(C,b,B)*IncProj(A,a,C) = IncProj(Q,a,B)*IncProj(A,b,Q);

theorem :: PROJRED2:24
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 implies ex Q 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
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 implies ex Q 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);
```