The abstract of the Mizar article:

On Projections in Projective Planes --- Part II

by

Eugeniusz Kusak,

Wojciech Leonczuk, and

Krzysztof Prazmowski

Received October 31, 1990

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);