The abstract of the Mizar article:

Incidence Projective Space (a reduction theorem in a plane)

by

Eugeniusz Kusak, and

Wojciech Leonczuk

Received October 16, 1990

MML identifier: PROJRED1

[ Mizar article, MML identifier index ]

environ

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


begin

reserve IPP for IncProjSp;
reserve a,b,c,d,p,q,o,r,s,t,u,v,w,x,y for POINT of IPP;
reserve A,B,C,D,L,P,Q,S for LINE of IPP;

theorem :: PROJRED1:1
ex a st not a on A;

theorem :: PROJRED1:2
  ex A st not a on A;

theorem :: PROJRED1:3
  A<>B implies ex a,b st a on A & not a on B & b on B & not b on A;

theorem :: PROJRED1:4
    a<>b implies ex A,B st a on A & not a on B & b on B & not b on A;

theorem :: PROJRED1:5
    ex A,B,C st a on A & a on B & a on C & A<>B & B<>C & C<>A;

theorem :: PROJRED1:6
    ex a st not a on A & not a on B;

theorem :: PROJRED1:7
  ex a st a on A;

theorem :: PROJRED1:8
  ex c st c on A & c <>a & c <>b;

theorem :: PROJRED1:9
    ex A st not a on A & not b on A;

canceled 2;

theorem :: PROJRED1:12
o on A & o on B & A<>B & a on A & o<>a & b on B & c on B &
b<>c & a on P & b on P &
  a on Q & c on Q implies P<>Q;

theorem :: PROJRED1:13
a,b,c on A implies a,c,b on A & b,a,c on A & b,c,a on A &
c,a,b on A & c,b,a on A;

theorem :: PROJRED1:14
for IPP being Desarguesian IncProjSp holds
for o,b1,a1,b2,a2,b3,a3,r,s,t being POINT of IPP,
C1,C2,C3,A1,A2,A3,B1,B2,B3 being LINE of IPP st o,b1,a1 on C1
& o,a2,b2 on C2 & o,a3,b3 on C3 & a3,a2,t on A1 & a3,r,a1 on A2 &
a2,s,a1 on A3 & t,b2,b3 on B1 & b1,r,b3 on B2 & b1,s,b2 on B3 &
C1,C2,C3 are_mutually_different & o<>a3 & o<>b1 & o<>b2 & a2<>b2
ex O being LINE of IPP st r,s,t on O;

theorem :: PROJRED1:15
 (ex A,a,b,c,d st a on A & b on A & c on A & d on A &
a,b,c,d are_mutually_different)
implies for B ex p,q,r,s st
p on B & q on B & r on B & s on B & p,q,r,s are_mutually_different;

reserve IPP for Fanoian IncProjSp;
reserve a,b,c,d,p,q,r,s for POINT of IPP;
reserve A,B,C,D,L,Q,R,S for LINE of IPP;

theorem :: PROJRED1:16
   ex p,q,r,s,a,b,c,A,B,C,Q,L,R,S,D st not q on L & not r on L & not p on Q &
 not s on Q &
not p on R & not r on R & not q on S & not s on S & a,p,s on L & a,q,r on Q &
b,q,s on R & b,p,r on S &
c,p,q on A & c,r,s on B & a,b on C & not c on C;

theorem :: PROJRED1:17
   ex a,A,B,C,D st a on A & a on B & a on C & a on D &
 A,B,C,D are_mutually_different;

theorem :: PROJRED1:18
 ex a,b,c,d,A st a on A & b on A & c on A & d on A &
a,b,c,d are_mutually_different;

theorem :: PROJRED1:19
   ex p,q,r,s st p on B & q on B & r on B & s on B &
 p,q,r,s are_mutually_different;

reserve IPP for Desarguesian 2-dimensional IncProjSp;
reserve c,p,q,x,y for POINT of IPP;
reserve A,B,C,D,K,L,R,X for LINE of IPP;

reserve f for PartFunc of the Points of IPP,the Points of IPP;

definition let IPP,K,L,p;
  assume  not p on K & not p on L;
  func IncProj(K,p,L) -> PartFunc of the Points of IPP,the Points of IPP means
:: PROJRED1:def 1
 dom it c= the Points of IPP & (for x holds x in dom it iff x on K) &
      for x,y st x on K & y on L holds it.x=y iff ex X st p on X & x on X &
      y on X;
end;

canceled;

theorem :: PROJRED1:21
not p on K implies (for x st x on K holds IncProj(K,p,K).x=x);

theorem :: PROJRED1:22
 not p on K & not p on L & x on K implies
  IncProj(K,p,L).x is POINT of IPP;

theorem :: PROJRED1:23
not p on K & not p on L & x on K & y = IncProj
(K,p,L).x implies y on L;

theorem :: PROJRED1:24
not p on K & not p on L & y in rng IncProj(K,p,L) implies y on L;

theorem :: PROJRED1:25
not p on K & not p on L & not q on L & not q on R implies
dom (IncProj(L,q,R)*IncProj(K,p,L)) = dom IncProj(K,p,L) &
rng (IncProj(L,q,R)*IncProj(K,p,L)) = rng IncProj(L,q,R);

theorem :: PROJRED1:26
for a1,b1,a2,b2 being POINT of IPP holds
not p on K & not p on L & a1 on K & b1 on K & IncProj(K,p,L).a1=a2 &
IncProj(K,p,L).b1=b2 & a2=b2
implies a1=b1;

theorem :: PROJRED1:27
not p on K & not p on L & x on K & x on L implies IncProj
(K,p,L).x=x;

reserve X for set;

theorem :: PROJRED1:28
   not p on K & not p on L & not q on L & not q on R & c on K & c on L &
 c on R & K <> R implies
ex o being POINT of IPP st not o on K & not o on R &
   IncProj(L,q,R)*IncProj(K,p,L)=IncProj(K,o,R);