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