:: Incidence Projective Space (a reduction theorem in a plane) :: by Eugeniusz Kusak and Wojciech Leo\'nczuk :: :: Received October 16, 1990 :: Copyright (c) 1990-2021 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies INCPROJ, INCSP_1, SUBSET_1, AFF_2, ZFMISC_1, VECTSP_1, ANALOAF, PARTFUN1, RELAT_1, TARSKI, FUNCT_1, PROJRED1; notations TARSKI, ZFMISC_1, SUBSET_1, DOMAIN_1, RELAT_1, RELSET_1, INCSP_1, INCPROJ, PARTFUN1, FUNCT_1; constructors DOMAIN_1, INCPROJ, RELSET_1; registrations FUNCT_1, RELSET_1, INCPROJ; 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; theorem :: PROJRED1:10 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 & c on Q implies P<>Q; theorem :: PROJRED1:11 {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:12 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_distinct & o<>a3 & o<>b1 & o<>b2 & a2<>b2 ex O being LINE of IPP st {r,s,t} on O; theorem :: PROJRED1:13 (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_distinct) 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_distinct; 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:14 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:15 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_distinct; theorem :: PROJRED1:16 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_distinct; theorem :: PROJRED1:17 ex p,q,r,s st p on B & q on B & r on B & s on B & p,q,r,s are_mutually_distinct; 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 that not p on K and 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; theorem :: PROJRED1:18 not p on K implies for x st x on K holds IncProj(K,p,K).x=x; theorem :: PROJRED1:19 not p on K & not p on L & x on K implies IncProj(K,p,L).x is POINT of IPP; theorem :: PROJRED1:20 not p on K & not p on L & x on K & y = IncProj (K,p,L).x implies y on L; theorem :: PROJRED1:21 not p on K & not p on L & y in rng IncProj(K,p,L) implies y on L; theorem :: PROJRED1:22 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:23 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:24 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:25 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);