Copyright (c) 1990 Association of Mizar Users
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;
definitions TARSKI;
theorems TARSKI, PARTFUN1, INCPROJ, FUNCT_1, RELAT_1, RELSET_1, XBOOLE_0;
schemes PARTFUN1, XBOOLE_0;
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 Th1: ex a st not a on A
proof
consider p,L such that A1: not p on L by INCPROJ:def 11;
now
assume A2: A<>L;
now
consider q,r,s such that
A3: q<>r & r<>s & s<>q & q on L & r on L & s on L by INCPROJ:def 12;
not q on A or not r on A by A2,A3,INCPROJ:def 9;
hence thesis;
end;
hence thesis;
end;
hence thesis by A1;
end;
theorem Th2:
ex A st not a on A
proof
consider p,L such that
A1: not p on L by INCPROJ:def 11; now
now assume A2: a on L;
consider q,r,s such that
A3: q<>r & r<>s & s<>q & q on L & r on L & s on L by INCPROJ:def 12;
A4: now assume A5: a<>q;
consider S such that
A6: q on S & p on S by INCPROJ:def 10;
not a on S by A1,A2,A3,A5,A6,INCPROJ:def 9;
hence thesis; end;
now assume A7: a<>s;
consider S such that
A8: s on S & p on S by INCPROJ:def 10;
not a on S by A1,A2,A3,A7,A8,INCPROJ:def 9;
hence thesis; end; hence thesis by A3,A4; end; hence thesis; end;
hence thesis; end;
theorem Th3:
A<>B implies ex a,b st a on A & not a on B & b on B & not b on A
proof
assume A1: A<>B;
consider a,b,d such that
A2: a<>b & b<>d & d<>a & a on A & b on A & d on A by INCPROJ:def 12;
consider r,s,t such that
A3: r<>s & s<>t & t<>r & r on B & s on B & t on B by INCPROJ:def 12;
A4: not a on B or not b on B by A1,A2,INCPROJ:def 9; not r on A or
not s on A by A1,A3,INCPROJ:def 9;
hence thesis by A2,A3,A4; end;
theorem
a<>b implies ex A,B st a on A & not a on B & b on B & not b on A
proof
assume A1: a<>b;
consider Q such that
A2: a on Q & b on Q by INCPROJ:def 10;
consider q such that
A3: not q on Q by Th1;
consider A such that
A4: a on A & q on A by INCPROJ:def 10;
consider B such that
A5: b on B & q on B by INCPROJ:def 10;
A6: not b on A by A1,A2,A3,A4,INCPROJ:def 9; not a on B by A1,A2,A3,A5,INCPROJ:
def 9; hence thesis by A4,A5,A6; end;
theorem
ex A,B,C st a on A & a on B & a on C & A<>B & B<>C & C<>A
proof
consider Q such that
A1: not a on Q by Th2;
consider b1,b2,b3 being Element of the Points of IPP such that
A2: b1<>b2 & b2<>b3 & b3<>b1 & b1 on Q & b2 on Q & b3 on Q by INCPROJ:def 12;
consider B1 being LINE of IPP such that
A3: a on B1 & b1 on B1 by INCPROJ:def 10;
consider B2 being LINE of IPP such that
A4: a on B2 & b2 on B2 by INCPROJ:def 10;
consider B3 being Element of the Lines of IPP such that
A5: a on B3 & b3 on B3 by INCPROJ:def 10;
A6: not b1 on B2 by A1,A2,A4,INCPROJ:def 9; A7: not b2 on B3 by A1,A2,A5,
INCPROJ:def 9; not b3 on B1 by A1,A2,A3,INCPROJ:def 9; hence
thesis by A3,A4,A5,A6,A7; end;
theorem
ex a st not a on A & not a on B
proof
A1: A=B implies ex a st not a on A & not a on B
proof
assume A2:A=B;
ex a st not a on A by Th1;
hence thesis by A2;
end;
A<>B implies ex a st not a on A & not a on B
proof
assume A<>B;
then consider a,b such that
A3: a on A & not a on B & b on B & not b on A by Th3;
consider C such that
A4: a on C & b on C by INCPROJ:def 10;
consider c,d,e being Element of the Points of IPP such that
A5: c <>d & d<>e & e<>c & c on C & d on C & e on C by INCPROJ:def 12;
(not c on A & not c on B) or (not d on A & not d on B) or (not e on A
& not e on B) by A3,A4,A5,INCPROJ:def 9
; hence thesis; end; hence thesis by A1; end;
theorem Th7:
ex a st a on A
proof
consider a,b,c such that
A1: a<>b & b<>c & c <>a & a on A & b on A & c on A by INCPROJ:def 12;
take a;
thus thesis by A1;
end;
theorem Th8:
ex c st c on A & c <>a & c <>b
proof
consider p,q,r such that
A1: p<>q & q<>r & r<>p & p on A & q on A & r on A by INCPROJ:def 12;
(p<>a & p<>b) or (q<>a & q<>b) or (r<>a & r<>b) by A1;
hence thesis by A1;
end;
theorem
ex A st not a on A & not b on A
proof
now
consider A such that
A1: a on A & b on A by INCPROJ:def 10;
consider c such that
A2: c on A & c <>a & c <>b by Th8;
consider d such that
A3: not d on A by Th1;
consider B such that
A4: d on B & c on B by INCPROJ:def 10;
not a on B & not b on B by A1,A2,A3,A4,INCPROJ:def 9;
hence thesis;
end;
hence thesis;
end;
canceled 2;
theorem Th12: 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
proof assume A1: 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; assume not thesis; then P=B by A1,INCPROJ:def 9;
hence contradiction by A1,INCPROJ:def 9; end;
theorem Th13: 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
proof assume a,b,c on A; then a on A & b on A & c on A by INCPROJ:def 8;
hence thesis by INCPROJ:def 8; end;
theorem Th14: 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
proof let IPP be Desarguesian IncProjSp;
let o,b1,a1,b2,a2,b3,a3,r,s,t be POINT of IPP,
C1,C2,C3,A1,A2,A3,B1,B2,B3 be LINE of IPP; assume
A1: 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;
then A2: o on C1 & b1 on C1 & a1 on C1 & o on C2 & a2 on C2 & b2 on C2 &
o on C3 & a3 on C3 & b3 on C3 by INCPROJ:def 8; A3: a3 on A1 & a2 on A1 & t on
A1 & a3 on A2 & r on A2 &
a1 on A2 & a2 on A3 &
s on A3 & a1 on A3 by A1,INCPROJ:def 8; A4: t on B1 & b2 on B1 & b3 on B1 &
b1 on B2 & r on B2 &
b3 on B2 & b1 on B3 & s on B3 & b2 on B3 by A1,INCPROJ:def 8;
A5: C1<>C2 & C2<>C3 & C3<>C1 by A1,INCPROJ:def 5;
then A6: C1<>B3 & C2<>B3 by A1,A2,A4,INCPROJ:def 9;
A7: now assume A8: o=b3;
A9: now assume A10: a1=o;
A11: now assume A12: o=a2; A13: A2=C3 by A1,A2,A3,A10,INCPROJ:def 9
; B2=C1 by A1,A2,A4,A8,INCPROJ:def 9;
then A14: o=r by A2,A3,A4,A5,A13,INCPROJ:def 9; A15: A1=C3 by A1,A2,A3,A12,
INCPROJ:def 9;
B1=C2 by A1,A2,A4,A8,INCPROJ:def 9;
then A16: r=t by A2,A3,A4,A5,A14,A15,INCPROJ:def 9
; consider O being LINE of IPP
such that A17: t on O & s on O by INCPROJ:def 10; take O; thus r,s,t on O by
A16,A17,INCPROJ:def 8; end; now assume A18: o<>a2;
A19: C2=B1 by A1,A2,A4,A8,INCPROJ:def 9;
A20: C2=A3 by A2,A3,A10,A18,INCPROJ:def 9; A21: B2=C1 by A1,A2,A4,A8,INCPROJ:
def 9; A2=C3 by A1,A2,A3,A10,INCPROJ:def 9;
then A22: r=o by A2,A3,A4,A5,A21,INCPROJ:def 9;
take C2; thus r,s,t on C2 by A2,A3,A4,A19,A20,A22,INCPROJ:def 8; end;
hence thesis by A11; end; now assume A23: a1<>o; now
A24: now assume A25: o=a2; then C1=A3 by A2,A3,A23,INCPROJ:def 9;
then A26: b1=s by A2,A3,A4,A6,INCPROJ:def 9; A27: B1=C2 by A1,A2,A4,A8,INCPROJ:
def 9;
A1=C3 by A1,A2,A3,A25,INCPROJ:def 9;
then A28: s,r,t on B2 by A1,A2,A3,A4,A5,A26,A27,INCPROJ:def 9; take B2; thus
r,s,t on B2
by A28,Th13; end; now assume o<>a2; A29: B2=C1 by A1,A2,A4,A8,INCPROJ:def 9
;
A30: B1=C2 by A1,A2,A4,A8,INCPROJ:def 9;
A31: A2<>C1 by A1,A2,A3,A5,INCPROJ:def 9;
A32: A1<>C2 by A1,A2,A3,A5,INCPROJ:def 9;
r=a1 by A2,A3,A4,A29,A31,INCPROJ:def 9;
then A33: t,s,r on A3 by A1,A2,A3,A4,A30,A32,INCPROJ:def 9; take A3;
thus r,s,t on A3 by A33,Th13; end; hence thesis by A24; end; hence thesis;
end; hence thesis by A9; end; A34: now assume A35: o<>b3 & o=a1;
A36: now assume o=a2; then A37: A1=C3 by A1,A2,A3,INCPROJ:def 9;
A38: A2=C3 by A1,A2,A3,A35,INCPROJ:def 9;
A39: B2<>C3 by A1,A2,A4,A5,INCPROJ:def 9;
A40: B1<>C3 by A1,A2,A4,A5,INCPROJ:def 9;
r=b3 by A2,A3,A4,A38,A39,INCPROJ:def 9;
then A41: r=t by A2,A3,A4,A37,A40,INCPROJ:def 9; consider O being
LINE of IPP such that
A42: t on O & s on O by INCPROJ:def 10; take O; thus r,s,t on O by A41,A42,
INCPROJ:def 8; end; now assume A43: o<>a2; A44: now assume
A45: a3=b3; A46: A1<>B1 proof C2<>C3 & a2<>b2 & b3<>o & o on C2 & o on C3 &
a2 on C2 &
b2 on C2 & b3 on C3 & a2 on A1 & b3 on A1 & b2 on B1 & b3 on B1
by A1,A45,INCPROJ:def 5,def 8;
hence thesis by Th12; end; A47: B2<>C3 by A1,A2,A4,A5,INCPROJ:def 9; A2=C3
by A2,A3,A35,A45,INCPROJ:def 9; then r=b3 by A2,A3,A4,A47,INCPROJ:def 9;
then A48: r=t by A3,A4,A45,A46,INCPROJ:def 9;
consider O being LINE of IPP such that A49: t on O & s on O by INCPROJ:def 10;
take O; thus
r,s,t on O by A48,A49,INCPROJ:def 8; end; now assume a3<>b3;
A50: A3=C2 by A2,A3,A35,A43,INCPROJ:def 9; A51: A2=C3 by A1,A2,A3,A35,INCPROJ:
def 9;
A52: B3<>C2 by A1,A2,A4,A5,INCPROJ:def 9;
A53: B2<>C3 by A1,A2,A4,A5,INCPROJ:def 9;
s=b2 by A2,A3,A4,A50,A52,INCPROJ:def 9;
then A54: t,s,r on B1 by A1,A2,A3,A4,A51,A53,INCPROJ:def 9; take B1;
thus r,s,t on B1 by A54,Th13; end; hence thesis by A44; end; hence thesis
by A36; end; A55: now assume A56: o<>b3 & o<>a1 & o=a2;
A57: now assume A58: a1=b1; A59: now assume A60: a3=b3;
A61: A3<>B3 proof C1<>C2 & o<>b1 & a2<>b2 & o on C1 & o on C2 & b1 on C1 &
b1 on A3 &
a2 on C2 & b2 on C2 & a2 on A3 & b2 on B3 by A1,A58,INCPROJ:def 5,def 8;
hence thesis by Th12; end; A62: A1<>B1 proof C2<>C3 & a2<>b2 & o<>b3 &
o on C2 &
o on C3 & a2 on C2 & b2 on C2 & b3 on C3 & a2 on A1 & b3 on A1 & b2 on B1 &
b3 on B1 by A1,A60,INCPROJ:def 5,def 8
; hence thesis by Th12; end; s=b1 by A3,A4,A58,A61,INCPROJ:def 9;
then A63: s,r,t on B2 by A1,A3,A4,A60,A62,INCPROJ:def 9;
take B2; thus r,s,t on B2 by A63,Th13; end;
now assume A64: a3<>b3; A65: A3=C1 by A2,A3,A56,INCPROJ:def 9;
A66: A2<>B2 proof C1<>C3 & o<>a1 & a3<>b3 & o on C1 & o on C3 & a1 on C1 &
a3 on C3 &
b3 on C3 & a1 on A2 & a3 on A2 & a1 on B2 & b3 on B2 by A1,A58,A64,INCPROJ:def
5,def 8;
hence thesis by Th12; end;
A67: B3<>C1 by A1,A2,A4,A5,INCPROJ:def 9;
r=b1 by A3,A4,A58,A66,INCPROJ:def 9;
then A68: r=s by A3,A4,A58,A65,A67,INCPROJ:def 9; consider O
being LINE of IPP such that A69: t on O & s on O by INCPROJ:def 10;
take O; thus r,s,t on O by A68,A69,INCPROJ:def 8; end;
hence thesis by A59; end; now assume
A70: a1<>b1; A71: now assume A72: a3=b3; then A73: A1=C3 by A2,A3,A56,INCPROJ:
def 9;
A74: A2<>B2 proof C1<>C3 & a1<>b1 & o<>b3 & o on C1 & o on C3 & a1 on C1 &
b1 on C1 &
b3 on C3 & a1 on A2 & b3 on A2 & b1 on B2 & b3 on B2 by A1,A70,A72,INCPROJ:def
5,def 8;
hence thesis by Th12; end; A75: B1<>C3 by A1,A2,A4,A5,INCPROJ:def 9; r=b3
by A3,A4,A72,A74,INCPROJ:def 9;
then A76: r=t by A2,A3,A4,A73,A75,INCPROJ:def 9; consider O being Element of
the
Lines of IPP such that A77: t on O & s on O by INCPROJ:def 10;
take O; thus
r,s,t on O by A76,A77,INCPROJ:def 8; end; now assume a3<>b3;
A78: A3=C1 by A2,A3,A56,INCPROJ:def 9;
A79: A1=C3 by A1,A2,A3,A56,INCPROJ:def 9; A80: B3<>C1 by A1,A2,A4,A5,INCPROJ:
def 9;
A81: B1<>C3 by A1,A2,A4,A5,INCPROJ:def 9;
b1=s by A2,A3,A4,A78,A80,INCPROJ:def 9;
then A82: s,r,t on B2 by A1,A2,A3,A4,A79,A81,INCPROJ:def 9; take B2;
thus r,s,t on B2 by A82,Th13; end; hence thesis by A71; end; hence thesis
by A57; end; A83: now assume A84: o<>b3 & o<>a1 & o<>a2 & a1=b1;
A85: now assume A86: a3=b3;
then a2<>b2 & C2<>C3 & o<>b3 & o on C2 & a2 on C2 & b2 on C2 & o on C3 &
b3 on C3 & a2 on A1 &
b3 on A1 & b2 on B1 & b3 on B1 by A1,INCPROJ:def 5,def 8; then A87: A1<>B1 by
Th12;
b1<>o & a2<>b2 & C1<>C2 & b1 on C1 & o on C1 & a2 on C2 & b2 on C2 &
o on C2 & a2 on A3 &
b1 on A3 & b1 on B3 & b2 on B3 by A1,A84,INCPROJ:def 5,def 8; then A88: A3<>B3
by Th12;
t=b3 by A3,A4,A86,A87,INCPROJ:def 9;
then A89: s,r,t on B2 by A1,A3,A4,A84,A88,INCPROJ:def 9
; take B2; thus r,s,t on B2 by A89,Th13; end;
now assume A90: a3<>b3;
C1<>C2 & o<>b1 & a2<>b2 & a1 on C1 & b1 on C1 & o on C1 & a2 on C2 &
b2 on C2 & o on C2 &
b1 on B3 & b2 on B3 & b1 on A3 & a2 on A3 by A1,A84,INCPROJ:def 5,def 8;
then A3<>B3 by Th12;
then A91: b1=s by A3,A4,A84,INCPROJ:def 9; a3<>b3
& b1<>o & C1<>C3 & b1 on C1 & o on C1 & o on C3 & a3 on C3 & b3 on C3 &
b1 on A2 & a3 on A2 & b1 on B2
& b3 on B2 by A1,A84,A90,INCPROJ:def 5,def 8
; then A2<>B2 by Th12; then A92: s = r by A3,A4,A84,A91,INCPROJ:def 9;
consider O being LINE of IPP such that A93: t on O & s on O by INCPROJ:def 10;
take O; thus
r,s,t on O by A92,A93,INCPROJ:def 8; end; hence thesis by A85; end;
now assume A94: o<>b3 & o<>a1 & o<>a2 & a1<>b1 & a3=b3;
then A95: b3 on A2 & a1 on A2 & b3 on B2 & b1 on B2 & a1<>b1 & C1<>C3 & o<>b3 &
r on A2 & r on B2 by A1,INCPROJ:def 5,def 8
; A96: C2<>C3 & b3 on A1 & a2 on A1 & b2 on B1 & b3 on B1 & a2<>b2 & o<>b3 &
a2 on C2 & b2 on C2 & o on C2 & o on C3 & b3 on C3 & t on A1 & t on B1
by A1,A94,INCPROJ:def 5,def 8;
A97: A2<>B2 by A2,A95,Th12; A98: A1<>B1 by A96,Th12; b3 = r by A3,A4,A94,A97,
INCPROJ:def 9;
then A99: r = t by A96,A98,INCPROJ:def 9; consider O being Element of the
Lines of IPP such that A100: t on O & s on O by INCPROJ:def 10; take O;
thus r,s,t on O by A99,A100,INCPROJ:def 8; end;
hence thesis by A1,A7,A34,A55,A83,INCPROJ:def 19
; end;
Lm1: (ex o st o on A & o on B) & a on A & b on A & c on A & d on A &
a,b,c,d are_mutually_different implies
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
proof assume that A1: ex o st o on A & o on B and A2: a on A & b on A &
c on A & d on A &
a,b,c,d are_mutually_different; consider o such that A3: o on A & o on B by A1;
now assume A<>B;
then consider x,y such that A4: x on A & not x on B & y on B &
not y on A by Th3;
consider C such that A5: x on C & y on C by INCPROJ:def 10;
consider w such that A6: w on C & w<>x & w<>y by Th8;
A7: now let u; assume A8: u on A;
A9: now assume A10: u=o; consider D such that A11: w on D & u on D by INCPROJ:
def 10;
take v=o,D; thus v on B & w on D & u on D & v on D by A3,A10,A11; end;
now assume A12: u<>o & x<>u;
consider D such that A13: w on D & u on D by INCPROJ:def 10;
not x on D proof assume not thesis;
then u on C by A5,A6,A13,INCPROJ:def 9;
hence contradiction by A4,A5,A8,A12,INCPROJ:def 9; end;
then consider v such that A14: v on B & v on D
by A3,A4,A5,A6,A8,A13,INCPROJ:def 13;
take v,D;
thus v on B & w on D & u on D & v on D by A13,A14; end;
hence ex v,D st v on B & w on D & u on D & v on D by A4,A5,A6,A9; end;
A15: now let u1,u2,v1,v2 be POINT of IPP, D1,D2 be
LINE of IPP such that A16: u1 on A & u2 on A and
A17: v1 on B & w on D1 & u1 on D1 & v1 on D1 & v2 on B & w on D2 &
u2 on D2 & v2 on D2;
assume A18: u1<>u2; A19: not w on B by A4,A5,A6,INCPROJ:def 9;
A20: D1<>A by A4,A5,A6,A17,INCPROJ:def 9;
assume v1=v2; then D1=D2 by A17,A19,INCPROJ:def 9;hence contradiction by A16,
A17,A18,A20,INCPROJ:def 9; end;
consider p be POINT of IPP,D1 be Element of the Lines of
IPP such that A21: p on B & w on D1 & a on D1 & p on D1 by A2,A7;
consider q be POINT of IPP,D2 be Element of the Lines of
IPP such that A22: q on B & w on D2 & b on D2 & q on D2 by A2,A7;
consider r be POINT of IPP,D3 be Element of the Lines of
IPP such that A23: r on B & w on D3 & c on D3 & r on D3 by A2,A7;
consider s be POINT of IPP,D4 be Element of the Lines of
IPP such that A24: s on B & w on D4 & d on D4 & s on D4 by A2,A7;
a<>b & b<>c & c <>d & d<>a & d<>b & a<>c by A2,INCPROJ:def 6;
then p<>q & q<>r & r<>s & s<>p & s<>q & p<>r by A2,A15,A21,A22,A23,A24;
then p,q,r,s are_mutually_different by INCPROJ:def 6;
hence thesis by A21,A22,A23,A24; end; hence thesis by A2; end;
theorem
Th15: (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
proof given A,a,b,c,d such that A1: a on A & b on A & c on A & d on A &
a,b,c,d are_mutually_different; let B; consider x such that A2: x on A by Th7;
consider y such that A3: y on B by Th7; consider C such that
A4: x on C & y on C by INCPROJ:def 10;
ex p1,q1,r1,s1 being POINT of IPP st
p1 on C & q1 on C & r1 on C & s1 on C & p1,q1,r1,s1 are_mutually_different
by A1,A2,A4,Lm1;
hence thesis by A3,A4,Lm1; end;
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;
Lm2: ex p,q,r,s,a,b,c,A,B,C,Q,L,R,S,D,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 & b on D & c on D &
C,D,R,S are_mutually_different & d on A & c,d,p,q are_mutually_different
proof consider r,A such that A1: not r on A by INCPROJ:def 11;
consider p,q,c such that A2: p<>q & q<>c & c <>p & p on A & q on A & c on A by
INCPROJ:def 12;
consider B such that A3: r on B & c on B by INCPROJ:def 10;
consider s such that A4: s on B & s<>r & s<>c by Th8;
consider Q such that A5: r on Q & q on Q by INCPROJ:def 10;
consider L such that A6: p on L & s on L by INCPROJ:def 10;
consider S such that A7: p on S & r on S by INCPROJ:def 10;
consider R such that
A8: q on R & s on R by INCPROJ:def 10;
A9: R<>Q proof assume not thesis;
then B=Q by A3,A4,A5,A8,INCPROJ:def 9;
hence contradiction by A1,A2,A3,A5,INCPROJ:def 9; end;
then A10: not r on R by A1,A2,A5,A8,INCPROJ:def 9;
A11: not p on Q by A1,A2,A5,INCPROJ:def 9;
A12: not q on S by A1,A2,A7,INCPROJ:def 9;
A13: not q on L proof assume not thesis; then s on A by A2,A6,INCPROJ:def 9;
hence contradiction by A1,A2,A3,A4,INCPROJ:def 9; end;
A14: not p on R proof assume not thesis; then s on A by A2,A8,INCPROJ:def 9;
hence contradiction by A1,A2,A3,A4,INCPROJ:def 9; end;
A15: not c on Q by A1,A2,A5,INCPROJ:def 9;
not c on L proof assume not thesis; then p on B by A3,A4,A6,INCPROJ:def 9;
hence contradiction by A1,A2,A3,INCPROJ:def 9; end;
then consider a such that A16: a on Q & a on L
by A1,A2,A3,A4,A5,A6,A15,INCPROJ:def 13;
A17: not c on R by A2,A8,A14,INCPROJ:def 9;
A18: not c on S by A1,A2,A7,INCPROJ:def 9;
then consider b such that A19: b on R & b on S
by A1,A2,A3,A4,A7,A8,A17,INCPROJ:def 13;
consider C such that A20: a on C & b on C by INCPROJ:def 10;
A21: not s on Q by A3,A4,A5,A15,INCPROJ:def 9;
A22: S<>L by A3,A4,A6,A7,A18,INCPROJ:def 9;
then A23: not r on L by A1,A2,A6,A7,INCPROJ:def 9;
A24: not s on S by A3,A4,A7,A18,INCPROJ:def 9;
A25: 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
by A2,A3,A4,A5,A6,A7,A8,A16,A19,INCPROJ:def 8;
A26: a,b on C by A20,INCPROJ:def 7;
then A27: not c on C by A10,A11,A12,A13,A14,A21,A23,A24,A25,INCPROJ:def 18;
consider D such that A28: b on D & c on D by INCPROJ:def 10;
A29: a<>s by A3,A4,A5,A15,A16,INCPROJ:def 9;
A30: a<>r by A1,A2,A6,A7,A16,A22,INCPROJ:def 9; A31: S<>Q by A1,A2,A5,A7,
INCPROJ:def 9;
A32: not a on S by A5,A7,A12,A16,A30,INCPROJ:def 9; A33: S<>D by A1,A2,A7,A28,
INCPROJ:def 9; A34: R<>D by A2,A8,A14,A28,INCPROJ:def 9;
A35: R<>C by A6,A8,A14,A16,A20,A29,INCPROJ:def 9; A36: S<>C by A5,A7,A12,A16,
A20,A30,INCPROJ:def 9;
A37: C,D,R,S are_mutually_different by A7,A14,A20,A27,A28,A32,A33,A34,A35,
INCPROJ:def 6;
A38: not b on Q by A5,A8,A9,A12,A19,INCPROJ:def 9;
then not r on C by A5,A16,A20,A30,INCPROJ:def 9; then consider d such that
A39: d on A & d on C by A1,A2,A5,A7,A16,A19,A20,A31,INCPROJ:def 13;
A40: d<>q by A5,A13,A16,A20,A38,A39,INCPROJ:def 9;
d<>p by A7,A14,A19,A20,A36,A39,INCPROJ:def 9;
then c,d,p,q are_mutually_different by A2,A27,A39,A40,INCPROJ:def 6;
hence thesis by A10,A11,A12,A13,A14,A21,A23,A24,A25,A26,A27,A28,A37,A39; end;
theorem
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
proof ex p,q,r,s,a,b,c,A,B,C,Q,L,R,S,D,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 &
b on D & c on D & C,D,R,S are_mutually_different &
d on A & c,d,p,q are_mutually_different by Lm2; hence thesis; end;
theorem
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
proof consider p,q,r,s,a,b,c,A,B,C,Q,L,R,S,D,d such that
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
and A1: 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 and not c on C and A2: b on D & c on D &
C,D,R,S are_mutually_different and d on A & c,d,p,q are_mutually_different
by Lm2;
b on S & b on R & b on C by A1,INCPROJ:def 7,def 8; hence thesis by A2; end;
theorem
Th18: 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
proof consider p,q,r,s,a,b,c,A,B,C,Q,L,R,S,D,d such that
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
and A1: 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 and not c on C and
b on D & c on D & C,D,R,S are_mutually_different and
A2: d on A & c,d,p,q are_mutually_different by Lm2;
c on A & d on A & p on A & q on A by A1,A2,INCPROJ:def 8; hence thesis by A2
;
end;
theorem
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
proof 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 by Th18; hence thesis by Th15; end;
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 A1: not p on K & not p on L;
func IncProj(K,p,L) -> PartFunc of the Points of IPP,the Points of IPP means
:Def1: 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;
existence
proof set XX = the Points of IPP;
defpred P[set,set] means ex x,y st x = $1 & y = $2 &
x on K & y on L & ex X st p on X & x on X & y on X;
A2: for x,y being set st x in XX & P[x,y] holds y in XX;
A3: for x,y1,y2 being set st x in XX & P[x,y1] & P[x,y2] holds y1 = y2
proof let x,y1,y2 be set such that A4: x in XX and A5: P[x,y1] and
A6: P[x,y2];
reconsider y1,y2 as POINT of IPP by A5,A6;
reconsider x as POINT of IPP by A4;
consider A1 being Element of
the Lines of IPP such that A7: p on A1 & x on A1 & y1 on A1 by A5;
p on A1 & x on A1 & y2 on A1 by A1,A6,A7,INCPROJ:def 9;
hence thesis by A1,A5,A6,A7,INCPROJ:def 9; end; consider f such that A8: for x
being
set holds x in dom f iff x in XX & ex y being set st P[x,y] and
A9: for x being set st x in dom f holds P[x,f.x] from PartFuncEx(A2,A3);
take f; thus dom f c= the Points of IPP;
thus A10: x in dom f iff x on K proof A11: x in dom f implies x on K
proof assume x in dom f; then P[x,f.x] by A9; hence thesis; end;
x on K implies x in dom f proof assume A12: x on K;
consider X being LINE of IPP such that A13: p on X & x on X by INCPROJ:def 10;
ex y st y on L & y on X by INCPROJ:def 14; hence thesis by A8,A12,A13
;end; hence thesis by A11;end;
let x,y; assume A14: x on K & y on L;
thus f.x=y iff ex X st p on X & x on X & y on X
proof A15: f.x=y implies ex X st p on X & x on X & y on X
proof assume A16: f.x = y;
x in dom f by A10,A14; then P[x,f.x] by A9;
hence thesis by A16; end; (ex X st p on X & x on X & y on X) implies f.x = y
proof assume A17: ex X st p on X & x on X & y on X; x in dom f by A10,A14;
then P[x,f.x] by A9;
hence thesis by A3,A14,A17; end; hence thesis by A15; end; end;
uniqueness
proof let f1,f2 be PartFunc of the Points of IPP,the Points of IPP such that
A18: dom f1 c= the Points of IPP & for x holds x in dom f1 iff x on K and
A19: for x,y st x on K & y on L holds f1.x=y iff ex X st p on X & x on X &
y on X and
A20: dom f2 c= the Points of IPP & for x holds x in dom f2 iff x on K and
A21: for x,y st x on K & y on L holds f2.x=y iff ex X st p on X &
x on X & y on X;
for x being set holds x in dom f1 iff x in dom f2
proof let x be set; A22: x in dom f1 implies x in dom f2 proof assume
A23: x in dom f1; then reconsider x as Element of
the Points of IPP; x on K by A18,A23; hence thesis by A20; end;
x in dom f2 implies x in dom f1 proof assume A24: x in dom f2;
then reconsider x as Element of the Points of IPP; x on K by A20,A24;
hence thesis by A18; end; hence thesis by A22; end; then A25: dom f1 = dom f2
by TARSKI:2; for x being POINT of IPP st x in dom f1 holds f1.x =
f2.x proof let x be POINT of IPP; assume x in dom f1;
then A26: x on K by A18;
consider A2 be LINE of IPP such that
A27: p on A2 & x on A2 by INCPROJ:def 10;
consider y2 be POINT of IPP such that
A28: y2 on A2 & y2 on L by INCPROJ:def 14;
f2.x = y2 by A21,A26,A27,A28;
hence thesis by A19,A26,A27,A28; end; hence thesis by A25,PARTFUN1:34; end;
end;
canceled;
theorem Th21: not p on K implies (for x st x on K holds IncProj(K,p,K).x=x)
proof assume A1: not p on K; let x; assume A2: x on K;
ex X st p on X & x on X by INCPROJ:def 10;
hence thesis by A1,A2,Def1; end;
theorem
Th22: not p on K & not p on L & x on K implies
IncProj(K,p,L).x is POINT of IPP
proof assume not p on K & not p on L & x on K;
then x in dom IncProj(K,p,L) by Def1;
hence IncProj(K,p,L).x is POINT of IPP by PARTFUN1:27; end;
theorem Th23: not p on K & not p on L & x on K & y = IncProj
(K,p,L).x implies y on L
proof assume A1: not p on K & not p on L & x on K & y = IncProj(K,p,L).x;
consider X such that A2: p on X & x on X by INCPROJ:def 10;
ex z being POINT of IPP st z on L & z on X by INCPROJ:def 14;
hence thesis by A1,A2,Def1; end;
theorem not p on K & not p on L & y in rng IncProj(K,p,L) implies y on L
proof assume A1: not p on K & not p on L & y in rng IncProj(K,p,L);
then consider x being POINT of IPP such that
A2: x in dom IncProj(K,p,L) & y = IncProj(K,p,L).x by PARTFUN1:26;
x on K by A1,A2,Def1;hence thesis by A1,A2,Th23; end;
theorem Th25: 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)
proof assume A1: not p on K & not p on L & not q on L & not q on R;
thus dom (IncProj(L,q,R)*IncProj(K,p,L)) = dom IncProj(K,p,L)
proof for x being set holds x in dom (IncProj(L,q,R)*IncProj(K,p,L))
iff x in dom IncProj(K,p,L) proof let x be set;
x in dom IncProj(K,p,L) implies x in dom (IncProj(L,q,R)*IncProj(K,p,L))
proof assume A2: x in dom IncProj(K,p,L);
then reconsider x' = x as POINT of IPP;
A3: x' on K by A1,A2,Def1;
consider A such that A4: x' on A & p on A by INCPROJ:def 10;
consider y such that
A5: y on A & y on L by INCPROJ:def 14;
(IncProj(K,p,L)).x=y & y in dom IncProj(L,q,R) by A1,A3,A4,A5,Def1;
hence thesis by A2,FUNCT_1:21; end; hence thesis by FUNCT_1:21; end;
hence thesis by TARSKI:2; end;
thus rng (IncProj(L,q,R)*IncProj(K,p,L)) = rng IncProj(L,q,R)
proof dom IncProj(L,q,R) c= rng IncProj(K,p,L) proof for x being set st
x in dom IncProj(L,q,R) holds x in
rng IncProj(K,p,L) proof let x be set; assume
A6: x in dom IncProj(L,q,R); thus x in rng IncProj(K,p,L) proof
reconsider x' = x as
POINT of IPP by A6; A7: x' on L by A1,A6,Def1;
ex y st y in dom IncProj(K,p,L) & x' = (IncProj
(K,p,L)).y proof consider A such that
A8: x' on A & p on A by INCPROJ:def 10;
consider y being POINT of IPP such that
A9: y on A & y on K by INCPROJ:def 14;
take y; thus y in dom IncProj(K,p,L) by A1,A9,Def1; thus x' =
(IncProj
(K,p,L)).y by A1,A7,A8,A9,Def1; end; hence thesis by FUNCT_1:def 5; end; end;
hence thesis by TARSKI:def 3; end; hence thesis by RELAT_1:47; end; end;
theorem Th26: 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
proof let a1,b1,a2,b2 be POINT of IPP; assume A1: 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;
then reconsider a2=IncProj(K,p,L).a1
as POINT of IPP;
A2: a2 on L by A1,Th23; then consider A such that A3: p on A & a1 on A
& a2 on A by A1,Def1; reconsider b2=IncProj(K,p,L).b1
as Element of the Points
of IPP by A1; b2 on L by A1,Th23; then consider B such that
A4: p on B & b1 on B & b2 on B by A1,Def1;
A=B by A1,A2,A3,A4,INCPROJ:def 9; hence thesis by A1,A3,A4,INCPROJ:def 9;
end;
theorem Th27: not p on K & not p on L & x on K & x on L implies IncProj
(K,p,L).x=x
proof assume A1: not p on K & not p on L & x on K & x on L; ex A st
p on A & x on A by INCPROJ:def 10; hence thesis by A1,Def1; end;
reserve X for set;
theorem
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)
proof assume A1: 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;
A2: dom (IncProj(L,q,R)*IncProj(K,p,L)) c= (the Points of IPP)
& rng (IncProj(L,q,R)*IncProj(K,p,L)) c= (the Points of IPP)
proof set f = IncProj(L,q,R)*IncProj(K,p,L); A3: dom f = dom IncProj
(K,p,L) by A1,Th25;
A4: rng f = rng IncProj(L,q,R) by A1,Th25;thus
dom (IncProj(L,q,R)*IncProj(K,p,L)) c= (the Points of IPP) by A3;
thus rng (IncProj(L,q,R)*IncProj
(K,p,L)) c= (the Points of IPP) by A4,RELSET_1:12; end;
defpred P[set] means ex k being POINT of IPP st $1 = k & k on K;
consider X such that A5: for x being set holds x qua set in X iff
x qua set in (the Points of IPP) qua set & P[x] from Separation;
A6: now assume A7: p=q;
IncProj(L,q,R)*IncProj(K,p,L)=IncProj(K,p,R)
proof A8: X = dom (IncProj(L,q,R)*IncProj(K,p,L)) & X = dom IncProj(K,p,R)
proof thus X = dom (IncProj(L,q,R)*IncProj(K,p,L)) proof
A9: X c= dom (IncProj(L,q,R)*IncProj
(K,p,L)) proof let e be set; assume A10: e in X;
then reconsider e as POINT of IPP by A5
; A11: ex e' being Element of
the Points of IPP st e=e' & e' on K by A5,A10; dom
(IncProj(L,q,R)*IncProj(K,p,L))=dom IncProj(K,p,L) by A1,Th25;
hence thesis by A1,A11,Def1; end;
dom (IncProj(L,q,R)*IncProj(K,p,L)) c= X proof let e be set; assume
e in dom (IncProj(L,q,R)*IncProj(K,p,L)); then A12: e in dom IncProj
(K,p,L) by A1,Th25;
then reconsider e as POINT of IPP;
e on K by A1,A12,Def1;
hence thesis by A5
; end; hence thesis by A9,XBOOLE_0:def 10; end; thus X = dom IncProj(K,p,R)
proof A13: X c= dom IncProj
(K,p,R) proof let e be set; assume A14: e qua set in X;
then reconsider e as POINT of IPP by A5;
ex e' being POINT of IPP st e=e' & e' on K by A5,A14; hence thesis by A1,A7,
Def1;
end; dom IncProj(K,p,R) c= X proof let e be set; assume A15: e in dom
IncProj
(K,p,R);
then reconsider e as POINT of IPP; e on K by A1,A7,A15,Def1;hence thesis by A5
; end; hence thesis by A13,XBOOLE_0:def 10; end; end;
A16: for x being POINT of IPP st x in X holds
(IncProj(L,q,R)*IncProj(K,p,L)).x = IncProj(K,p,R).x proof
let x be POINT of IPP; assume A17: x in X;
then A18: x on K by A1,A7,A8,Def1;
A19: (IncProj(L,p,R)*IncProj(K,p,L)).x =
IncProj(L,p,R).(IncProj(K,p,L).x) by A7,A8,A17,FUNCT_1:22
; reconsider y = IncProj(K,p,L).x as
POINT of IPP by A1,A18,Th22; A20: y on L by A1,A18,Th23; consider A such that
A21: p on A & y on A by INCPROJ:def 10;
consider B such that
A22: p on B & x on B & y on B by A1,A18,A20,Def1; reconsider z = IncProj
(L,p,R).y as
POINT of IPP by A1,A7,A20,Th22; A23: z on R by A1,A7,A20,Th23; then consider C
such that
A24: p on C & y on C & z on C by A1,A7,A20,Def1
; A25: A=B by A1,A20,A21,A22,INCPROJ:def 9; A=C by A1,A20,A21,A24,INCPROJ:def 9
;
hence thesis by A1,A7,A18,A19,A22,A23,A24,A25,Def1; end;
(IncProj(L,q,R)*IncProj(K,p,L))is
PartFunc of the Points of IPP,the Points of IPP by A2,RELSET_1:11
; hence thesis by A8,A16,PARTFUN1:34; end; hence thesis by A1,A7; end;
now assume A26: p<>q;
consider A such that A27: p on A & q on A by INCPROJ:def 10;
consider c1 being POINT of IPP such that
A28: c1 on K & c1 on A by INCPROJ:def 14;
consider a1 being POINT of IPP such that
A29: a1 on K & c1<>a1 & c <>a1 by Th8; reconsider a2
=IncProj(K,p,L).a1 as POINT of IPP by A1,A29,Th22; A30: a2 on L by A1,A29,Th23;
then reconsider a3=IncProj(L,q,R).a2
as POINT of IPP
by A1,Th22; A31: a3 on R by A1,A30,Th23; consider B such that
A32: a1 on B & a3 on B by INCPROJ:def 10;
consider o being POINT of IPP such that
A33: o on A & o on B by INCPROJ:def 14;
reconsider c2=IncProj(K,p,L).c1 as Element of the
Points of IPP by A1,A28,Th22; A34: c2 on L by A1,A28,Th23;
then reconsider c3=IncProj(L,q,R).c2 as POINT of IPP by A1,Th22;
A35: c3 on R by A1,A34,Th23
; A36: not a1 on R by A1,A29,INCPROJ:def 9; A37: not a3 on K proof
assume a3 on K; then A38: c =a3 by A1,A31,INCPROJ:def 9;
ex C st q on C & c on C by INCPROJ:def 10;
then IncProj(L,q,R).c =a3 by A1,A38,Def1;
then A39: c =a2 by A1,A30,Th26; ex D st p on D & c on D by INCPROJ:def 10;
then IncProj(K,p,L).c =a2 by A1,A39,Def1;
hence contradiction by A1,A29,Th26; end;
A40: not o on K & not o on R proof assume A41: not thesis;
A42: now assume A43: o on K; then o=c1 by A1,A27,A28,A33,INCPROJ:def 9;
hence contradiction by A29,A32,A33,A37,A43,INCPROJ:def 9
; end; now assume A44: o on R;
A45:ex A1 being LINE of IPP st p on A1 & c1 on A1 &
c2 on A1 by A1,A28,A34,Def1; consider A2 being LINE of IPP such
that A46: q on A2 & c2 on A2 & c3 on A2 by A1,A34,A35,Def1;
c2 on A by A1,A27,A28,A45,INCPROJ:def 9; then A=A2 by A1,A27,A34,A46,INCPROJ:
def 9; then A47: o=c3 by A1,A33,A35,A44,A46,INCPROJ:def 9;
o=a3 by A31,A32,A33,A36,A44,INCPROJ:def 9;
then c2=a2 by A1,A30,A34,A47,Th26; hence
contradiction by A1,A28,A29,Th26; end; hence thesis by A41,A42; end;
A48: now assume A49: K=L; take q;
IncProj(L,q,R)*IncProj(K,p,L) = IncProj(K,q,R) proof
A50: X = dom (IncProj(L,q,R)*IncProj(K,p,L)) & X = dom IncProj(K,q,R) proof
thus X = dom (IncProj(L,q,R)*IncProj(K,p,L)) proof A51: X c= dom (IncProj
(L,q,R)*IncProj(K,p,L))
proof let e be set; assume A52: e in X;
then reconsider e as Element
of the Points of IPP by A5
; A53: ex e' being POINT of IPP st
e=e' & e' on K by A5,A52;
dom (IncProj(L,q,R)*IncProj(K,p,L)) = dom IncProj(K,p,L) by A1,Th25;
hence thesis by A1,A53,Def1; end;
dom (IncProj(L,q,R)*IncProj(K,p,L)) c= X proof let e be set; assume
e in dom (IncProj(L,q,R)*IncProj(K,p,L)); then A54: e in dom IncProj
(K,p,L) by A1,Th25;
then reconsider e as POINT of IPP;
e on K by A1,A54,Def1; hence thesis by A5; end; hence
thesis by A51,XBOOLE_0:def 10; end; thus X = dom IncProj(K,q,R) proof
A55: X c= dom IncProj(K,q,R) proof let e be set; assume A56: e qua set in X;
then reconsider e as POINT of IPP by A5;
ex e' being POINT of IPP st e=e' & e' on K by A5,A56;
hence thesis by A1,A49,Def1; end;
dom IncProj(K,q,R) c= X proof let e be set; assume A57: e in dom IncProj
(K,q,R);
then reconsider e as POINT of IPP; e on K by A1,A49,A57,Def1;hence thesis by A5
; end; hence thesis by A55,XBOOLE_0:def 10; end; end;
A58: for x being POINT of IPP st x in X holds
(IncProj(L,q,R)*IncProj(K,p,L)).x = IncProj
(K,q,R).x proof let x be Element of the Points of
IPP; assume A59: x in X; then A60: x on K by A1,A49,A50,Def1;
(IncProj(K,q,R)*IncProj(K,p,K)).x = IncProj(K,q,R).(IncProj
(K,p,K).x) by A49,A50,A59,FUNCT_1:22;
hence thesis by A1,A49,A60,Th21; end;
(IncProj(L,q,R)*IncProj(K,p,L)) is
PartFunc of the Points of IPP,the Points of IPP by A2,RELSET_1:11
; hence thesis by A50,A58,PARTFUN1:34; end; hence thesis by A1,A49; end;
A61: now assume A62: L=R;
take p; IncProj(L,q,R)*IncProj(K,p,L) = IncProj(K,p,R) proof
A63: X = dom (IncProj(L,q,R)*IncProj(K,p,L)) & X = dom IncProj(K,p,R) proof
thus X = dom (IncProj(L,q,R)*IncProj(K,p,L)) proof A64: X c= dom (IncProj
(L,q,R)*IncProj(K,p,L))
proof let e be set; assume A65:
e in X;
then reconsider e as Element of the Points
of IPP by A5
; A66: ex e' being POINT of IPP st e=e' &
e' on K by A5,A65; dom (IncProj(L,q,R)*IncProj(K,p,L))=dom IncProj(K,p,L) by A1
,Th25;hence thesis by A1,A66,Def1; end; dom (IncProj(L,q,R)*IncProj
(K,p,L)) c= X
proof let e be set; assume e in dom (IncProj(L,q,R)*IncProj(K,p,L));
then A67: e in dom IncProj(K,p,L) by A1,Th25;
then reconsider e as POINT of IPP; e on K by A1,A67,Def1;
hence thesis by A5; end; hence thesis by A64,XBOOLE_0:def 10; end;
thus X = dom IncProj(K,p,R) proof A68: X c= dom IncProj
(K,p,R) proof let e be set;
assume A69: e qua set in X;
then reconsider e as POINT of IPP by A5; ex e'
being POINT of IPP st e=e' & e' on K by A5,A69;
hence thesis by A1,A62,Def1; end;
dom IncProj(K,p,R) c= X proof let e be set; assume A70: e in dom IncProj
(K,p,R);
then reconsider e as POINT of IPP; e on K by A1,A62,A70,Def1;hence thesis by A5
; end; hence thesis by A68,XBOOLE_0:def 10; end; end;
A71: for x being POINT of IPP st x in X holds
(IncProj(L,q,R)*IncProj(K,p,L)).x = IncProj
(K,p,R).x proof let x be Element of the Points of
IPP; assume A72: x in X; then A73: x on K by A1,A62,A63,Def1;
A74: (IncProj(R,q,R)*IncProj(K,p,R)).x = IncProj(R,q,R).(IncProj
(K,p,R).x) by A62,A63,A72,FUNCT_1:22;
reconsider y =IncProj(K,p,R).x
as POINT of IPP by A1,A62,A73,Th22;
y on R by A1,A62,A73,Th23;
hence thesis by A1,A62,A74,Th21; end;
(IncProj(L,q,R)*IncProj(K,p,L)) is
PartFunc of the Points of IPP,the Points of IPP by A2,RELSET_1:11
; hence thesis by A63,A71,PARTFUN1:34; end; hence thesis by A1,A62; end;
now assume A75: L<>R & K<>L; IncProj(L,q,R)*IncProj(K,p,L)=IncProj
(K,o,R) proof
A76: X = dom (IncProj(L,q,R)*IncProj(K,p,L)) proof A77: X c= dom (IncProj
(L,q,R)*IncProj(K,p,L))
proof let e be set; assume A78: e in X;
then reconsider e as POINT of IPP by A5
; A79: ex e' being POINT of IPP st
e=e' & e' on K by A5,A78;
dom (IncProj(L,q,R)*IncProj(K,p,L)) = dom IncProj(K,p,L) by A1,Th25;
hence thesis by A1,A79,Def1; end;
dom (IncProj(L,q,R)*IncProj(K,p,L)) c= X proof let e be set; assume
e in dom (IncProj(L,q,R)*IncProj(K,p,L)); then A80: e in dom IncProj
(K,p,L) by A1,Th25;
then reconsider e as POINT of IPP;
e on K by A1,A80,Def1; hence thesis by A5; end; hence thesis by A77,XBOOLE_0:
def 10; end; A81: for x being POINT of IPP st x in X holds
(IncProj(L,q,R)*IncProj(K,p,L)).x = IncProj
(K,o,R).x proof let x be Element of the Points of
IPP; assume A82: x in X; A83: now assume A84: x=c; (IncProj(L,q,R)*IncProj
(K,p,L)).x =
IncProj(K,o,R).x proof (IncProj(L,q,R)*IncProj(K,p,L)).c =
IncProj(L,q,R).(IncProj(K,p,L).c) by A76,A82,A84,FUNCT_1:22;
then (IncProj(L,q,R)*IncProj(K,p,L)).c = IncProj(L,q,R).c by A1,Th27;
then (IncProj(L,q,R)*IncProj(K,p,L)).c =c by A1,Th27; hence
thesis by A1,A40,A84,Th27; end; hence thesis; end;
A85: now assume A86: x=c1; (IncProj(L,q,R)*IncProj(K,p,L)).x = IncProj
(K,o,R).x proof
A87: (IncProj(L,q,R)*IncProj(K,p,L)).c1 =c3 by A76,A82,A86,FUNCT_1:22
; A88: ex A1 being Element of the Lines
of IPP st p on A1 & c1 on A1 & c2 on A1 by A1,A28,A34,Def1;
consider A2 being LINE of IPP such that A89: q on A2 & c2 on A2 &
c3 on A2 by A1,A34,A35,Def1;
c2 on A by A1,A27,A28,A88,INCPROJ:def 9;
then A=A2 by A1,A27,A34,A89,INCPROJ:def 9;
hence thesis by A28,A33,A35,A40,A86,A87,A89,Def1; end; hence thesis; end;
A90: now assume A91: x=a1; (IncProj(L,q,R)*IncProj(K,p,L)).x = IncProj
(K,o,R).x proof
(IncProj(L,q,R)*IncProj(K,p,L)).a1 =a3 by A76,A82,A91,FUNCT_1:22;
hence thesis by A29,A31,A32,A33,A40,A91,Def1; end; hence thesis; end; now
assume A92: x<>c1 & x<>c & x<>a1;
(IncProj(L,q,R)*IncProj(K,p,L)).x = IncProj(K,o,R).x proof A93: dom (IncProj
(L,q,R)*IncProj(K,p,L))=
dom IncProj(K,p,L) by A1,Th25; then A94: x on K by A1,A76,A82,Def1;
then reconsider y = IncProj(K,p,L).x
as POINT of IPP by A1,Th22; A95: y on L by A1,A94,Th23;
then reconsider z = IncProj(L,q,R).y
as POINT of IPP by A1,Th22;
A96: z on R by A1,A95,Th23; consider A1 being LINE of IPP such that
A97: q on A1 & a2 on A1 & a3 on A1 by A1,A30,A31,Def1;
consider A3 being Element of the
Lines of IPP such that A98: p on A3 & a1 on A3 & a2 on A3 by A1,A29,A30,Def1;
consider B1 being LINE of IPP such that A99: q on B1 & y on B1 & z on B1
by A1,A95,A96,Def1; consider B3 being LINE of IPP such that
A100: p on B3 & x on B3 & y on B3 by A1,A94,A95,Def1;
A101: c on K & x on K & a1 on K by A1,A29,A76,A82,A93,Def1;
A102: o on B & a3 on B & a1 on B & c on K & x on K & a1 on K &
c on R & z on R & a3 on R by A1,A29,A30,A32,A33,A76,A82,A93,A95,Def1,Th23;
A103: A1<>A3 proof assume A1=A3; then A=A3 by A26,A27,A97,A98,INCPROJ:def 9;
hence
contradiction by A1,A28,A29,A98,INCPROJ:def 9
; end; A104: a2<>c proof assume A105: a2=c; IncProj(K,p,L).c = c by A1,Th27
;
hence contradiction by A1,A29,A105,Th26; end;
A106: a2<>a3 proof assume a2=a3;
then A107: IncProj(K,p,L).a1 = c by A1,A30,A31,A75,INCPROJ:def 9; IncProj(K,
p
,L).c = c by A1,Th27;
hence contradiction by A1,A29,A107,Th26; end;
A108: c <>y by A1,A92,A100,A101,INCPROJ:def 9;
a2,y,c on L & a2,a3,q on A1 & a2,p,a1 on A3 & p,o,q on A &
p,y,x on B3 & y,z,q on B1 & a3,o,a1 on B & x,c,a1 on K & a3,z,c on R &
A1,L,A3 are_mutually_different & a2<>p & a2<>c & a2<>a3 by A1,A27,A30,A33,A95,
A97,A98,A99,A100,A102,A103,A104,A106,INCPROJ:def 5,def 8
; then consider O being
LINE of IPP such that
A109: o,z,x on O by A108,Th14; A110: x on O & z on O & o on O
by A109,INCPROJ:def 8;
(IncProj(L,q,R)*IncProj(K,p,L)).x = IncProj(L,q,R).(IncProj
(K,p,L).x) by A76,A82,FUNCT_1:22;hence
thesis by A40,A94,A96,A110,Def1;end; hence thesis;end; hence
thesis by A83,A85,A90; end; A111: X = dom IncProj(K,o,R) proof A112: X c= dom
IncProj(K,o,R)
proof let e be set; assume A113: e qua set in X;
then reconsider e as POINT of IPP by A5;
ex e' being POINT of IPP st e=e' & e' on K by A5,A113; hence thesis by A40,
Def1;
end; dom IncProj(K,o,R) c= X proof let e be set; assume A114: e in
dom IncProj
(K,o,R);
then reconsider e as POINT of IPP; e on K by A40,A114,Def1;hence thesis by A5
; end; hence thesis by A112,XBOOLE_0:def 10; end; (IncProj(L,q,R)*
IncProj(K,p,L)) is PartFunc of the Points of IPP,the Points of IPP
by A2,RELSET_1:11; hence IncProj(L,q,R)*IncProj(K,p,L)=IncProj
(K,o,R) by A76,A81,A111,PARTFUN1:34; end; hence
thesis by A40; end; hence thesis by A48,A61; end; hence thesis by A6; end;