Volume 2, 1990

University of Bialystok

Copyright (c) 1990 Association of Mizar Users

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

Back to top