:: Incidence Projective Space (a reduction theorem in a plane)
:: by Eugeniusz Kusak and Wojciech Leo\'nczuk
::
:: Received October 16, 1990
:: Copyright (c) 1990-2026 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;
definitions TARSKI;
expansions TARSKI;
theorems TARSKI, PARTFUN1, INCPROJ, FUNCT_1, RELAT_1, RELSET_1, XBOOLE_0,
ZFMISC_1, INCSP_1;
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 6;
now
assume
A2: A<>L;
now
consider q,r,s such that
A3: q<>r and
r<>s and
s<>q and
A4: q on L & r on L and
s on L by INCPROJ:def 7;
not q on A or not r on A by A2,A3,A4,INCPROJ:def 4;
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 6;
now
now
consider q,r,s such that
q<>r and
r<>s and
A2: s<>q and
A3: q on L and
r on L and
A4: s on L by INCPROJ:def 7;
assume
A5: a on L;
A6: now
consider S such that
A7: s on S & p on S by INCPROJ:def 5;
assume a<>s;
then not a on S by A1,A5,A4,A7,INCPROJ:def 4;
hence thesis;
end;
now
consider S such that
A8: q on S & p on S by INCPROJ:def 5;
assume a<>q;
then not a on S by A1,A5,A3,A8,INCPROJ:def 4;
hence thesis;
end;
hence thesis by A2,A6;
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
consider a,b,d such that
A1: a<>b and
b<>d and
d<>a and
A2: a on A & b on A and
d on A by INCPROJ:def 7;
consider r,s,t such that
A3: r<>s and
s<>t and
t<>r and
A4: r on B & s on B and
t on B by INCPROJ:def 7;
assume
A5: A<>B;
then
A6: not r on A or not s on A by A3,A4,INCPROJ:def 4;
not a on B or not b on B by A5,A1,A2,INCPROJ:def 4;
hence thesis by A2,A4,A6;
end;
theorem
a<>b implies ex A,B st a on A & not a on B & b on B & not b on A
proof
consider Q such that
A1: a on Q & b on Q by INCPROJ:def 5;
consider q such that
A2: not q on Q by Th1;
consider B such that
A3: b on B and
A4: q on B by INCPROJ:def 5;
assume
A5: a<>b;
then
A6: not a on B by A1,A2,A3,A4,INCPROJ:def 4;
consider A such that
A7: a on A and
A8: q on A by INCPROJ:def 5;
not b on A by A5,A1,A2,A7,A8,INCPROJ:def 4;
hence thesis by A7,A3,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 and
A3: b2<>b3 and
A4: b3<>b1 and
A5: b1 on Q and
A6: b2 on Q and
A7: b3 on Q by INCPROJ:def 7;
consider B1 being LINE of IPP such that
A8: a on B1 & b1 on B1 by INCPROJ:def 5;
A9: not b3 on B1 by A1,A4,A5,A7,A8,INCPROJ:def 4;
consider B2 being LINE of IPP such that
A10: a on B2 & b2 on B2 by INCPROJ:def 5;
consider B3 being Element of the Lines of IPP such that
A11: a on B3 & b3 on B3 by INCPROJ:def 5;
A12: not b2 on B3 by A1,A3,A6,A7,A11,INCPROJ:def 4;
not b1 on B2 by A1,A2,A5,A6,A10,INCPROJ:def 4;
hence thesis by A8,A10,A11,A12,A9;
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 A<>B;
then consider a,b such that
a on A and
A2: not a on B and
b on B and
A3: not b on A by Th3;
consider C such that
A4: a on C & b on C by INCPROJ:def 5;
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 7;
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 A2,A3,A4,A5,INCPROJ:def 4;
hence thesis;
end;
A=B implies ex a st not a on A & not a on B
proof
assume
A6: A=B;
ex a st not a on A by Th1;
hence thesis by A6;
end;
hence thesis by A1;
end;
theorem Th7:
ex a st a on A
proof
consider a,b,c such that
a<>b and
b<>c and
c <>a and
A1: a on A and
b on A and
c on A by INCPROJ:def 7;
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 and
A2: p on A & q on A & r on A by INCPROJ:def 7;
p<>a & p<>b or q<>a & q<>b or r<>a & r<>b by A1;
hence thesis by A2;
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 5;
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 5;
( not a on B)& not b on B by A1,A2,A3,A4,INCPROJ:def 4;
hence thesis;
end;
hence thesis;
end;
theorem Th10:
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
proof
assume that
A1: o on A & o on B & A<>B & a on A & o<>a and
A2: b on B & c on B & b<>c and
A3: a on P and
A4: b on P & c on Q;
assume not thesis;
then P=B by A2,A4,INCPROJ:def 4;
hence contradiction by A1,A3,INCPROJ:def 4;
end;
theorem Th11:
{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
A1: {a,b,c} on A;
then
A2: c on A by INCSP_1:2;
a on A & b on A by A1,INCSP_1:2;
hence thesis by A2,INCSP_1:2;
end;
theorem Th12:
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
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 that
A1: {o,b1,a1} on C1 and
A2: {o,a2,b2} on C2 and
A3: {o,a3,b3} on C3 and
A4: {a3,a2,t} on A1 and
A5: {a3,r,a1} on A2 and
A6: {a2,s,a1} on A3 and
A7: {t,b2,b3} on B1 and
A8: {b1,r,b3} on B2 and
A9: {b1,s,b2} on B3 and
A10: C1,C2,C3 are_mutually_distinct and
A11: o<>a3 and
A12: o<>b1 and
A13: o<>b2 and
A14: a2<>b2;
A15: r on A2 & r on B2 by A5,A8,INCSP_1:2;
A16: s on B3 by A9,INCSP_1:2;
A17: a3 on A1 by A4,INCSP_1:2;
A18: b3 on B1 by A7,INCSP_1:2;
A19: b2 on B1 by A7,INCSP_1:2;
A20: b3 on C3 by A3,INCSP_1:2;
A21: a1 on C1 by A1,INCSP_1:2;
A22: o on C2 by A2,INCSP_1:2;
A23: s on A3 by A6,INCSP_1:2;
A24: a1 on A3 by A6,INCSP_1:2;
A25: a1 on A2 by A5,INCSP_1:2;
A26: t on A1 by A4,INCSP_1:2;
A27: b1 on B2 by A8,INCSP_1:2;
A28: t on B1 by A7,INCSP_1:2;
A29: b1 on B3 by A9,INCSP_1:2;
A30: now
assume that
o<>b3 and
o<>a1 and
o<>a2 and
A31: a1=b1;
A32: now
A33: b3 on B2 by A8,INCSP_1:2;
consider O being LINE of IPP such that
A34: t on O & s on O by INCPROJ:def 5;
assume
A35: a3<>b3;
take O;
A36: b2 on C2 & o on C2 by A2,INCSP_1:2;
A37: o on C1 & a2 on C2 by A1,A2,INCSP_1:2;
A38: b1 on B3 & b2 on B3 by A9,INCSP_1:2;
A39: b1 on A2 & a3 on A2 by A5,A31,INCSP_1:2;
A40: a3 on C3 & b3 on C3 by A3,INCSP_1:2;
A41: o on C1 & o on C3 by A1,A3,INCSP_1:2;
A42: a2 on A3 by A6,INCSP_1:2;
C1<>C2 & b1 on C1 by A1,A10,INCSP_1:2,ZFMISC_1:def 5;
then A3<>B3 by A12,A14,A37,A36,A38,A42,Th10;
then
A43: b1=s by A23,A24,A29,A16,A31,INCPROJ:def 4;
C1<>C3 & b1 on C1 by A1,A10,INCSP_1:2,ZFMISC_1:def 5;
then A2<>B2 by A12,A35,A41,A40,A39,A33,Th10;
then s = r by A25,A27,A15,A31,A43,INCPROJ:def 4;
hence {r,s,t} on O by A34,INCSP_1:2;
end;
now
A44: a2 on A3 & b1 on A3 by A6,A31,INCSP_1:2;
A45: C2<>C3 & o on C2 by A2,A10,INCSP_1:2,ZFMISC_1:def 5;
A46: a2 on C2 & b2 on C2 by A2,INCSP_1:2;
A47: o on C1 & a2 on C2 by A1,A2,INCSP_1:2;
A48: b2 on B3 by A9,INCSP_1:2;
A49: a2 on A1 & b2 on B1 by A4,A7,INCSP_1:2;
A50: o on C3 & b3 on C3 by A3,INCSP_1:2;
assume
A51: a3=b3;
then b3 on A1 by A4,INCSP_1:2;
then A1<>B1 by A11,A14,A51,A45,A46,A50,A49,Th10;
then
A52: t=b3 by A17,A26,A28,A18,A51,INCPROJ:def 4;
take B2;
A53: b2 on C2 & o on C2 by A2,INCSP_1:2;
C1<>C2 & b1 on C1 by A1,A10,INCSP_1:2,ZFMISC_1:def 5;
then A3<>B3 by A12,A14,A47,A53,A44,A48,Th10;
then {s,r,t} on B2 by A8,A23,A24,A29,A16,A31,A52,INCPROJ:def 4;
hence {r,s,t} on B2 by Th11;
end;
hence thesis by A32;
end;
A54: o on C1 by A1,INCSP_1:2;
A55: C1<>C2 by A10,ZFMISC_1:def 5;
A56: b1 on C1 by A1,INCSP_1:2;
A57: a2 on A3 by A6,INCSP_1:2;
A58: b2 on C2 by A2,INCSP_1:2;
A59: C2<>C3 by A10,ZFMISC_1:def 5;
A60: a3 on C3 by A3,INCSP_1:2;
A61: b3 on B2 by A8,INCSP_1:2;
A62: a3 on A2 by A5,INCSP_1:2;
A63: a2 on A1 by A4,INCSP_1:2;
A64: o on C3 by A3,INCSP_1:2;
A65: b2 on B3 by A9,INCSP_1:2;
A66: now
assume that
A67: o<>b3 and
A68: o<>a1 and
A69: o=a2;
A70: now
assume
A71: a1=b1;
A72: now
A73: a2 on A1 & b2 on B1 by A4,A7,INCSP_1:2;
A74: b2 on C2 & b3 on C3 by A2,A3,INCSP_1:2;
A75: b2 on C2 & a2 on A3 by A2,A6,INCSP_1:2;
A76: o on C2 & b1 on C1 by A1,A2,INCSP_1:2;
A77: C1<>C2 & o on C1 by A1,A10,INCSP_1:2,ZFMISC_1:def 5;
assume
A78: a3=b3;
take B2;
A79: b2 on B3 by A9,INCSP_1:2;
b1 on A3 & a2 on C2 by A2,A6,A71,INCSP_1:2;
then A3<>B3 by A12,A14,A77,A76,A75,A79,Th10;
then
A80: s=b1 by A23,A24,A29,A16,A71,INCPROJ:def 4;
A81: o on C3 & a2 on C2 by A2,A3,INCSP_1:2;
A82: C2<>C3 & o on C2 by A2,A10,INCSP_1:2,ZFMISC_1:def 5;
b3 on A1 by A4,A78,INCSP_1:2;
then A1<>B1 by A11,A14,A78,A82,A81,A74,A73,Th10;
then {s,r,t} on B2 by A8,A17,A26,A28,A18,A78,A80,INCPROJ:def 4;
hence {r,s,t} on B2 by Th11;
end;
now
A83: o on C3 & a1 on C1 by A1,A3,INCSP_1:2;
A84: a1 on A2 & a3 on A2 by A5,INCSP_1:2;
A85: b3 on B2 by A8,INCSP_1:2;
consider O being LINE of IPP such that
A86: t on O & s on O by INCPROJ:def 5;
assume
A87: a3<>b3;
take O;
A88: a3 on C3 & b3 on C3 by A3,INCSP_1:2;
C1<>C3 & o on C1 by A1,A10,INCSP_1:2,ZFMISC_1:def 5;
then A2<>B2 by A12,A71,A87,A83,A88,A84,A85,Th10;
then
A89: r=b1 by A25,A27,A15,A71,INCPROJ:def 4;
A3=C1 & B3<>C1 by A13,A54,A21,A22,A58,A57,A24,A65,A55,A68,A69,
INCPROJ:def 4;
then r=s by A23,A24,A29,A16,A71,A89,INCPROJ:def 4;
hence {r,s,t} on O by A86,INCSP_1:2;
end;
hence thesis by A72;
end;
now
assume
A90: a1<>b1;
A91: now
A92: B1<>C3 by A13,A22,A58,A64,A19,A59,INCPROJ:def 4;
A93: o on C3 & a1 on C1 by A1,A3,INCSP_1:2;
consider O being Element of the Lines of IPP such that
A94: t on O & s on O by INCPROJ:def 5;
A95: C1<>C3 & o on C1 by A1,A10,INCSP_1:2,ZFMISC_1:def 5;
A96: a1 on A2 & b1 on B2 by A5,A8,INCSP_1:2;
A97: b1 on C1 & b3 on C3 by A1,A3,INCSP_1:2;
assume
A98: a3=b3;
then b3 on A2 by A5,INCSP_1:2;
then A2<>B2 by A11,A90,A98,A95,A93,A97,A96,Th10;
then
A99: r=b3 by A62,A15,A61,A98,INCPROJ:def 4;
take O;
A1=C3 by A64,A60,A17,A63,A67,A69,A98,INCPROJ:def 4;
then r=t by A20,A26,A28,A18,A92,A99,INCPROJ:def 4;
hence {r,s,t} on O by A94,INCSP_1:2;
end;
now
assume a3<>b3;
take B2;
A3=C1 & B3<>C1 by A13,A54,A21,A22,A58,A57,A24,A65,A55,A68,A69,
INCPROJ:def 4;
then
A100: b1=s by A56,A23,A29,A16,INCPROJ:def 4;
A1=C3 & B1<>C3 by A11,A13,A22,A58,A64,A60,A17,A63,A19,A59,A69,
INCPROJ:def 4;
then {s,r,t} on B2 by A8,A20,A26,A28,A18,A100,INCPROJ:def 4;
hence {r,s,t} on B2 by Th11;
end;
hence thesis by A91;
end;
hence thesis by A70;
end;
A101: C3<>C1 by A10,ZFMISC_1:def 5;
A102: a2 on C2 by A2,INCSP_1:2;
A103: now
assume that
A104: o<>b3 and
A105: o=a1;
A106: now
A107: now
A108: B2<>C3 by A12,A54,A56,A64,A27,A101,INCPROJ:def 4;
assume
A109: a3=b3;
then A2=C3 by A64,A60,A62,A25,A104,A105,INCPROJ:def 4;
then
A110: r=b3 by A20,A15,A61,A108,INCPROJ:def 4;
A111: b2 on C2 & b3 on C3 by A2,A3,INCSP_1:2;
A112: o on C3 & a2 on C2 by A2,A3,INCSP_1:2;
A113: a2 on A1 & b2 on B1 by A4,A7,INCSP_1:2;
consider O being LINE of IPP such that
A114: t on O & s on O by INCPROJ:def 5;
A115: C2<>C3 & o on C2 by A2,A10,INCSP_1:2,ZFMISC_1:def 5;
take O;
b3 on A1 by A4,A109,INCSP_1:2;
then A1<>B1 by A11,A14,A109,A115,A112,A111,A113,Th10;
then r=t by A17,A26,A28,A18,A109,A110,INCPROJ:def 4;
hence {r,s,t} on O by A114,INCSP_1:2;
end;
assume
A116: o<>a2;
now
assume a3<>b3;
take B1;
A3=C2 & B3<>C2 by A12,A54,A56,A22,A102,A57,A24,A29,A55,A105,A116,
INCPROJ:def 4;
then
A117: s=b2 by A58,A23,A16,A65,INCPROJ:def 4;
A2=C3 & B2<>C3 by A11,A12,A54,A56,A64,A60,A62,A25,A27,A101,A105,
INCPROJ:def 4;
then {t,s,r} on B1 by A7,A20,A15,A61,A117,INCPROJ:def 4;
hence {r,s,t} on B1 by Th11;
end;
hence thesis by A107;
end;
now
assume o=a2;
then
A118: A1=C3 by A11,A64,A60,A17,A63,INCPROJ:def 4;
A2=C3 & B2<>C3 by A11,A12,A54,A56,A64,A60,A62,A25,A27,A101,A105,
INCPROJ:def 4;
then
A119: r=b3 by A20,A15,A61,INCPROJ:def 4;
consider O being LINE of IPP such that
A120: t on O & s on O by INCPROJ:def 5;
take O;
B1<>C3 by A13,A22,A58,A64,A19,A59,INCPROJ:def 4;
then r=t by A20,A26,A28,A18,A118,A119,INCPROJ:def 4;
hence {r,s,t} on O by A120,INCSP_1:2;
end;
hence thesis by A106;
end;
A121: C1<>B3 by A13,A54,A22,A58,A65,A55,INCPROJ:def 4;
A122: now
assume
A123: o=b3;
A124: now
assume
A125: a1=o;
A126: now
assume o=a2;
then
A127: A1=C3 by A11,A64,A60,A17,A63,INCPROJ:def 4;
A2=C3 & B2=C1 by A11,A12,A54,A56,A64,A60,A62,A25,A27,A61,A123,A125,
INCPROJ:def 4;
then
A128: o=r by A54,A64,A15,A101,INCPROJ:def 4;
consider O being LINE of IPP such that
A129: t on O & s on O by INCPROJ:def 5;
take O;
B1=C2 by A13,A22,A58,A19,A18,A123,INCPROJ:def 4;
then r=t by A22,A64,A26,A28,A59,A128,A127,INCPROJ:def 4;
hence {r,s,t} on O by A129,INCSP_1:2;
end;
now
B2=C1 & A2=C3 by A11,A12,A54,A56,A64,A60,A62,A25,A27,A61,A123,A125,
INCPROJ:def 4;
then
A130: r=o by A54,A64,A15,A101,INCPROJ:def 4;
assume o<>a2;
then
A131: C2=A3 by A22,A102,A57,A24,A125,INCPROJ:def 4;
take C2;
C2=B1 by A13,A22,A58,A19,A18,A123,INCPROJ:def 4;
hence {r,s,t} on C2 by A22,A23,A28,A131,A130,INCSP_1:2;
end;
hence thesis by A126;
end;
now
assume
A132: a1<>o;
A133: now
assume
A134: o=a2;
then
A135: A1=C3 by A11,A64,A60,A17,A63,INCPROJ:def 4;
take B2;
C1=A3 by A54,A21,A57,A24,A132,A134,INCPROJ:def 4;
then
A136: b1=s by A56,A23,A29,A16,A121,INCPROJ:def 4;
B1=C2 by A13,A22,A58,A19,A18,A123,INCPROJ:def 4;
then {s,r,t} on B2 by A8,A20,A26,A28,A18,A59,A136,A135,INCPROJ:def 4;
hence {r,s,t} on B2 by Th11;
end;
now
assume o<>a2;
take A3;
B2=C1 & A2<>C1 by A11,A12,A54,A56,A64,A60,A62,A27,A61,A101,A123,
INCPROJ:def 4;
then
A137: r=a1 by A21,A25,A15,INCPROJ:def 4;
B1=C2 & A1<>C2 by A11,A13,A22,A58,A64,A60,A17,A19,A18,A59,A123,
INCPROJ:def 4;
then {t,s,r} on A3 by A6,A102,A63,A26,A28,A137,INCPROJ:def 4;
hence {r,s,t} on A3 by Th11;
end;
hence thesis by A133;
end;
hence thesis by A124;
end;
now
A138: b2 on B1 & a2 on C2 by A2,A7,INCSP_1:2;
A139: o on C3 & b3 on C3 by A3,INCSP_1:2;
A140: a1 on A2 & b1 on B2 by A5,A8,INCSP_1:2;
A141: b2 on C2 & o on C2 by A2,INCSP_1:2;
A142: b3 on B1 & t on A1 by A4,A7,INCSP_1:2;
A143: t on B1 by A7,INCSP_1:2;
consider O being Element of the Lines of IPP such that
A144: t on O & s on O by INCPROJ:def 5;
assume that
A145: o<>b3 and
o<>a1 and
o<>a2 and
A146: a1<>b1 and
A147: a3=b3;
take O;
A148: C1<>C3 by A10,ZFMISC_1:def 5;
b3 on A2 by A5,A147,INCSP_1:2;
then A2<>B2 by A54,A56,A21,A64,A20,A145,A146,A140,A148,Th10;
then
A149: b3 = r by A62,A15,A61,A147,INCPROJ:def 4;
A150: b3 on A1 by A4,A147,INCSP_1:2;
C2<>C3 & a2 on A1 by A4,A10,INCSP_1:2,ZFMISC_1:def 5;
then A1<>B1 by A14,A145,A150,A138,A141,A139,Th10;
then r = t by A150,A142,A143,A149,INCPROJ:def 4;
hence {r,s,t} on O by A144,INCSP_1:2;
end;
hence
thesis by A1,A2,A3,A4,A5,A6,A7,A8,A9,A10,A11,A12,A13,A14,A122,A103,A66,A30,
INCPROJ:def 13;
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_distinct 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_distinct
proof
assume that
A1: ex o st o on A & o on B and
A2: a on A and
A3: b on A and
A4: c on A and
A5: d on A and
A6: a,b,c,d are_mutually_distinct;
consider o such that
A7: o on A and
A8: o on B by A1;
now
assume A<>B;
then consider x,y such that
A9: x on A and
A10: not x on B and
A11: y on B and
A12: not y on A by Th3;
consider C such that
A13: x on C and
A14: y on C by INCPROJ:def 5;
consider w such that
A15: w on C and
A16: w<>x and
A17: w<>y by Th8;
A18: now
A19: not w on B by A10,A11,A13,A14,A15,A17,INCPROJ:def 4;
let u1,u2,v1,v2 be POINT of IPP, D1,D2 be LINE of IPP such that
A20: u1 on A & u2 on A and
A21: v1 on B and
A22: w on D1 and
A23: u1 on D1 and
A24: v1 on D1 and
v2 on B and
A25: w on D2 and
A26: u2 on D2 and
A27: v2 on D2;
A28: D1<>A by A9,A12,A13,A14,A15,A16,A22,INCPROJ:def 4;
assume
A29: u1<>u2;
assume v1=v2;
then D1=D2 by A21,A22,A24,A25,A27,A19,INCPROJ:def 4;
hence contradiction by A20,A23,A26,A29,A28,INCPROJ:def 4;
end;
A30: now
let u;
assume
A31: u on A;
A32: now
assume that
u<>o and
A33: x<>u;
consider D such that
A34: w on D & u on D by INCPROJ:def 5;
not x on D
proof
assume not thesis;
then u on C by A13,A15,A16,A34,INCPROJ:def 4;
hence contradiction by A9,A12,A13,A14,A31,A33,INCPROJ:def 4;
end;
then consider v such that
A35: v on B & v on D by A7,A8,A9,A10,A11,A12,A13,A14,A15,A31,A34,
INCPROJ:def 8;
take v,D;
thus v on B & w on D & u on D & v on D by A34,A35;
end;
now
consider D such that
A36: w on D & u on D by INCPROJ:def 5;
assume
A37: u=o;
take v=o,D;
thus v on B & w on D & u on D & v on D by A8,A37,A36;
end;
hence ex v,D st v on B & w on D & u on D & v on D by A11,A13,A14,A15,A32;
end;
then consider
p be POINT of IPP,D1 be Element of the Lines of IPP such that
A38: p on B and
A39: w on D1 & a on D1 & p on D1 by A2;
consider r be POINT of IPP,D3 be Element of the Lines of IPP such that
A40: r on B and
A41: w on D3 & c on D3 & r on D3 by A4,A30;
consider q be POINT of IPP,D2 be Element of the Lines of IPP such that
A42: q on B and
A43: w on D2 & b on D2 & q on D2 by A3,A30;
consider s be POINT of IPP,D4 be Element of the Lines of IPP such that
A44: s on B and
A45: w on D4 & d on D4 & s on D4 by A5,A30;
d<>a by A6,ZFMISC_1:def 6;
then
A46: s<>p by A2,A5,A18,A38,A39,A45;
a<>c by A6,ZFMISC_1:def 6;
then
A47: p<>r by A2,A4,A18,A38,A39,A41;
d<>b by A6,ZFMISC_1:def 6;
then
A48: s<>q by A3,A5,A18,A42,A43,A45;
c <>d by A6,ZFMISC_1:def 6;
then
A49: r<>s by A4,A5,A18,A40,A41,A45;
b<>c by A6,ZFMISC_1:def 6;
then
A50: q<>r by A3,A4,A18,A42,A43,A41;
a<>b by A6,ZFMISC_1:def 6;
then p<>q by A2,A3,A18,A38,A39,A43;
then p,q,r,s are_mutually_distinct by A50,A49,A46,A48,A47,ZFMISC_1:def 6;
hence thesis by A38,A42,A40,A44;
end;
hence thesis by A2,A3,A4,A5,A6;
end;
theorem Th13:
(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
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_distinct;
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 and
A5: y on C by INCPROJ:def 5;
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_distinct by A1,A2,A4,Lm1;
hence thesis by A3,A5,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_distinct & d
on A & c,d,p,q are_mutually_distinct
proof
consider r,A such that
A1: not r on A by INCPROJ:def 6;
consider p,q,c such that
A2: p<>q and
A3: q<>c and
A4: c <>p and
A5: p on A and
A6: q on A and
A7: c on A by INCPROJ:def 7;
consider B such that
A8: r on B and
A9: c on B by INCPROJ:def 5;
consider s such that
A10: s on B and
A11: s<>r and
A12: s<>c by Th8;
consider L such that
A13: p on L and
A14: s on L by INCPROJ:def 5;
consider Q such that
A15: r on Q and
A16: q on Q by INCPROJ:def 5;
A17: not p on Q by A1,A2,A5,A6,A15,A16,INCPROJ:def 4;
A18: not c on Q by A1,A3,A6,A7,A15,A16,INCPROJ:def 4;
then
A19: not s on Q by A8,A9,A10,A11,A15,INCPROJ:def 4;
not c on L
proof
assume not thesis;
then p on B by A9,A10,A12,A13,A14,INCPROJ:def 4;
hence contradiction by A1,A4,A5,A7,A8,A9,INCPROJ:def 4;
end;
then consider a such that
A20: a on Q and
A21: a on L by A1,A5,A6,A7,A8,A9,A10,A15,A16,A13,A14,A18,INCPROJ:def 8;
A22: {a,p,s} on L by A13,A14,A21,INCSP_1:2;
consider R such that
A23: q on R and
A24: s on R by INCPROJ:def 5;
consider S such that
A25: p on S and
A26: r on S by INCPROJ:def 5;
A27: not c on S by A1,A4,A5,A7,A25,A26,INCPROJ:def 4;
then
A28: not s on S by A8,A9,A10,A11,A26,INCPROJ:def 4;
A29: S<>L by A8,A9,A10,A11,A14,A26,A27,INCPROJ:def 4;
then
A30: not r on L by A1,A5,A13,A25,A26,INCPROJ:def 4;
A31: S<>Q by A1,A2,A5,A6,A15,A16,A25,INCPROJ:def 4;
A32: not q on S by A1,A2,A5,A6,A25,A26,INCPROJ:def 4;
A33: not q on L
proof
assume not thesis;
then s on A by A2,A5,A6,A13,A14,INCPROJ:def 4;
hence contradiction by A1,A7,A8,A9,A10,A12,INCPROJ:def 4;
end;
A34: not p on R
proof
assume not thesis;
then s on A by A2,A5,A6,A23,A24,INCPROJ:def 4;
hence contradiction by A1,A7,A8,A9,A10,A12,INCPROJ:def 4;
end;
then not c on R by A3,A5,A6,A7,A23,INCPROJ:def 4;
then consider b such that
A35: b on R and
A36: b on S by A1,A5,A6,A7,A8,A9,A10,A25,A26,A23,A24,A27,INCPROJ:def 8;
A37: {b,q,s} on R by A23,A24,A35,INCSP_1:2;
A38: R<>Q
proof
assume not thesis;
then B=Q by A8,A10,A11,A15,A24,INCPROJ:def 4;
hence contradiction by A1,A3,A6,A7,A8,A9,A16,INCPROJ:def 4;
end;
then
A39: not r on R by A1,A6,A15,A16,A23,INCPROJ:def 4;
A40: {c,r,s} on B by A8,A9,A10,INCSP_1:2;
A41: {b,p,r} on S by A25,A26,A36,INCSP_1:2;
A42: a<>r by A1,A5,A13,A25,A26,A21,A29,INCPROJ:def 4;
then
A43: not a on S by A15,A16,A26,A32,A20,INCPROJ:def 4;
A44: {a,q,r} on Q by A15,A16,A20,INCSP_1:2;
consider C such that
A45: a on C and
A46: b on C by INCPROJ:def 5;
a<>s by A8,A9,A10,A11,A15,A18,A20,INCPROJ:def 4;
then
A47: R<>C by A13,A14,A24,A34,A21,A45,INCPROJ:def 4;
A48: not b on Q by A16,A23,A38,A32,A35,A36,INCPROJ:def 4;
then not r on C by A15,A20,A45,A46,A42,INCPROJ:def 4;
then consider d such that
A49: d on A and
A50: d on C by A1,A5,A6,A15,A16,A25,A26,A20,A36,A45,A46,A31,INCPROJ:def 8;
S<>C by A15,A16,A26,A32,A20,A45,A42,INCPROJ:def 4;
then
A51: d<>p by A25,A34,A35,A36,A46,A50,INCPROJ:def 4;
A52: {c,p,q} on A by A5,A6,A7,INCSP_1:2;
A53: {a,b} on C by A45,A46,INCSP_1:1;
then
A54: not c on C by A39,A17,A32,A33,A34,A19,A30,A28,A22,A44,A37,A41,A52,A40,
INCPROJ:def 12;
consider D such that
A55: b on D and
A56: c on D by INCPROJ:def 5;
A57: R<>D by A3,A5,A6,A7,A23,A34,A56,INCPROJ:def 4;
d<>q by A16,A33,A20,A21,A45,A46,A48,A50,INCPROJ:def 4;
then
A58: c,d,p,q are_mutually_distinct by A2,A3,A4,A54,A50,A51,ZFMISC_1:def 6;
S<>D by A1,A4,A5,A7,A25,A26,A56,INCPROJ:def 4;
then C,D,R,S are_mutually_distinct by A25,A34,A45,A54,A56,A43,A57,A47,
ZFMISC_1:def 6;
hence
thesis by A39,A17,A32,A33,A34,A19,A30,A28,A22,A44,A37,A41,A52,A40,A53,A54,A55
,A56,A49,A58;
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_distinct & d
on A & c,d,p,q are_mutually_distinct 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_distinct
proof
consider p,q,r,s,a,b,c,A,B,C,Q,L,R,S,D,d such that
not q on L and
not r on L and
not p on Q and
not s on Q and
not p on R and
not r on R and
not q on S and
not s on S and
{a,p,s} on L and
{a,q,r} on Q and
A1: {b,q,s} on R & {b,p,r} on S and
{c,p,q} on A and
{c,r,s} on B and
A2: {a,b} on C and
not c on C and
A3: b on D and
c on D and
A4: C,D,R,S are_mutually_distinct and
d on A and
c,d,p,q are_mutually_distinct by Lm2;
A5: b on C by A2,INCSP_1:1;
b on S & b on R by A1,INCSP_1:2;
hence thesis by A3,A4,A5;
end;
theorem Th16:
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
proof
consider p,q,r,s,a,b,c,A,B,C,Q,L,R,S,D,d such that
not q on L and
not r on L and
not p on Q and
not s on Q and
not p on R and
not r on R and
not q on S and
not s on S and
{a,p,s} on L and
{a,q,r} on Q and
{b,q,s} on R and
{b,p,r} on S and
A1: {c,p,q} on A and
{c,r,s} on B and
{a,b} on C and
not c on C and
b on D and
c on D and
C,D,R,S are_mutually_distinct and
A2: d on A & c,d,p,q are_mutually_distinct by Lm2;
A3: q on A by A1,INCSP_1:2;
c on A & p on A by A1,INCSP_1:2;
hence thesis by A2,A3;
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_distinct
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_distinct by Th16;
hence thesis by Th13;
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 that
A1: not p on K and
A2: 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
defpred P[object,object] 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;
set XX = the Points of IPP;
A3: for x,y1,y2 being object st x in XX & P[x,y1] & P[x,y2] holds y1 = y2
proof
let x,y1,y2 be object such that
A4: x in XX and
A5: P[x,y1] and
A6: P[x,y2];
reconsider x as POINT of IPP by A4;
reconsider y1,y2 as POINT of IPP by A5,A6;
consider A1 being Element of the Lines of IPP such that
A7: p on A1 and
A8: x on A1 and
A9: y1 on A1 by A5;
y2 on A1 by A1,A6,A7,A8,INCPROJ:def 4;
hence thesis by A2,A5,A6,A7,A9,INCPROJ:def 4;
end;
A10: for x,y being object st x in XX & P[x,y] holds y in XX;
consider f such that
A11: for x being object holds x in dom f iff x in XX &
ex y being object st
P[x,y] and
A12: for x being object st x in dom f holds P[x,f.x] from PARTFUN1:sch 2(
A10, A3);
take f;
thus dom f c= the Points of IPP;
thus
A13: x in dom f iff x on K
proof
A14: x on K implies x in dom f
proof
consider X being LINE of IPP such that
A15: p on X & x on X by INCPROJ:def 5;
assume
A16: x on K;
ex y st y on L & y on X by INCPROJ:def 9;
hence thesis by A11,A16,A15;
end;
x in dom f implies x on K
proof
assume x in dom f;
then P[x,f.x] by A12;
hence thesis;
end;
hence thesis by A14;
end;
let x,y;
assume that
A17: x on K and
A18: y on L;
A19: f.x=y implies ex X st p on X & x on X & y on X
proof
x in dom f by A13,A17;
then
A20: P[x,f.x] by A12;
assume f.x = y;
hence thesis by A20;
end;
(ex X st p on X & x on X & y on X) implies f.x = y
proof
x in dom f by A13,A17;
then
A21: P[x,f.x] by A12;
assume ex X st p on X & x on X & y on X;
hence thesis by A3,A18,A21;
end;
hence f.x=y iff ex X st p on X & x on X & y on X by A19;
end;
uniqueness
proof
let f1,f2 be PartFunc of the Points of IPP,the Points of IPP such that
dom f1 c= the Points of IPP and
A22: for x holds x in dom f1 iff x on K and
A23: 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
dom f2 c= the Points of IPP and
A24: for x holds x in dom f2 iff x on K and
A25: 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 object holds x in dom f1 iff x in dom f2
by A24,A22;
then
A26: 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;
consider A2 be LINE of IPP such that
A27: p on A2 & x on A2 by INCPROJ:def 5;
consider y2 be POINT of IPP such that
A28: y2 on A2 & y2 on L by INCPROJ:def 9;
assume x in dom f1;
then
A29: x on K by A22;
then f2.x = y2 by A25,A27,A28;
hence thesis by A23,A29,A27,A28;
end;
hence thesis by A26,PARTFUN1:5;
end;
end;
theorem Th18:
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;
A2: ex X st p on X & x on X by INCPROJ:def 5;
assume x on K;
hence thesis by A1,A2,Def1;
end;
theorem Th19:
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 thesis by PARTFUN1:4;
end;
theorem Th20:
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 5;
ex z being POINT of IPP st z on L & z on X by INCPROJ:def 9;
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 that
A1: ( not p on K)& not p on L and
A2: y in rng IncProj(K,p,L);
consider x being POINT of IPP such that
A3: x in dom IncProj(K,p,L) and
A4: y = IncProj(K,p,L).x by A2,PARTFUN1:3;
x on K by A1,A3,Def1;
hence thesis by A1,A4,Th20;
end;
theorem Th22:
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 that
A1: ( not p on K)& not p on L and
A2: ( not q on L)& not q on R;
for x being object holds x in dom (IncProj(L,q,R)*IncProj(K,p,L)) iff x in
dom IncProj(K,p,L)
proof
let x be object;
x in dom IncProj(K,p,L) implies x in dom (IncProj(L,q,R)*IncProj(K,p,L ))
proof
assume
A3: x in dom IncProj(K,p,L);
then reconsider x9 = x as POINT of IPP;
consider A such that
A4: x9 on A & p on A by INCPROJ:def 5;
consider y such that
A5: y on A and
A6: y on L by INCPROJ:def 9;
A7: y in dom IncProj(L,q,R) by A2,A6,Def1;
x9 on K by A1,A3,Def1;
then (IncProj(K,p,L)).x=y by A1,A4,A5,A6,Def1;
hence thesis by A3,A7,FUNCT_1:11;
end;
hence thesis by FUNCT_1:11;
end;
hence dom (IncProj(L,q,R)*IncProj(K,p,L)) = dom IncProj(K,p,L) by TARSKI:2;
for x being object st x in dom IncProj(L,q,R) holds x in rng IncProj(K,p,L)
proof
let x be object;
assume
A8: x in dom IncProj(L,q,R);
thus x in rng IncProj(K,p,L)
proof
reconsider x9 = x as POINT of IPP by A8;
A9: x9 on L by A2,A8,Def1;
ex y st y in dom IncProj(K,p,L) & x9 = (IncProj (K,p,L)).y
proof
consider A such that
A10: x9 on A & p on A by INCPROJ:def 5;
consider y being POINT of IPP such that
A11: y on A and
A12: y on K by INCPROJ:def 9;
take y;
thus y in dom IncProj(K,p,L) by A1,A12,Def1;
thus thesis by A1,A9,A10,A11,A12,Def1;
end;
hence thesis by FUNCT_1:def 3;
end;
end;
then dom IncProj(L,q,R) c= rng IncProj(K,p,L);
hence rng (IncProj(L,q,R)*IncProj(K,p,L)) = rng IncProj(L,q,R) by RELAT_1:28;
end;
theorem Th23:
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 that
A1: not p on K and
A2: not p on L and
A3: a1 on K and
A4: b1 on K and
A5: IncProj(K,p,L).a1=a2 and
A6: IncProj (K,p,L).b1=b2 and
A7: a2=b2;
reconsider a2=IncProj(K,p,L).a1 as POINT of IPP by A5;
A8: a2 on L by A1,A2,A3,Th20;
then consider A such that
A9: p on A and
A10: a1 on A and
A11: a2 on A by A1,A2,A3,Def1;
reconsider b2=IncProj(K,p,L).b1 as Element of the Points of IPP by A6;
b2 on L by A1,A2,A4,Th20;
then consider B such that
A12: p on B and
A13: b1 on B and
A14: b2 on B by A1,A2,A4,Def1;
A=B by A2,A5,A6,A7,A8,A9,A11,A12,A14,INCPROJ:def 4;
hence thesis by A1,A3,A4,A9,A10,A13,INCPROJ:def 4;
end;
theorem Th24:
not p on K & not p on L & x on K & x on L implies IncProj (K,p,L ).x=x
proof
A1: ex A st p on A & x on A by INCPROJ:def 5;
assume ( not p on K)& not p on L & x on K & x on L;
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 that
A1: not p on K and
A2: not p on L and
A3: not q on L and
A4: not q on R and
A5: c on K and
A6: c on L and
A7: c on R and
A8: K <> R;
defpred P[object] means ex k being POINT of IPP st $1 = k & k on K;
consider X such that
A9: for x being object holds x in X iff x in (the Points
of IPP) qua set & P[x] from XBOOLE_0:sch 1;
A10: 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);
dom f = dom IncProj (K,p,L) by A1,A2,A3,A4,Th22;
hence dom (IncProj(L,q,R)*IncProj(K,p,L)) c= (the Points of IPP);
rng f = rng IncProj(L,q,R) by A1,A2,A3,A4,Th22;
hence thesis by RELAT_1:def 19;
end;
A11: now
A12: now
A13: X c= dom (IncProj (L,q,R)*IncProj(K,p,L))
proof
let e be object;
assume
A14: e in X;
then reconsider e as Element of the Points of IPP by A9;
A15: ex e9 being POINT of IPP st e=e9 & e9 on K by A9,A14;
dom (IncProj(L,q,R)*IncProj(K,p,L))=dom IncProj(K,p,L) by A1,A2,A3,A4
,Th22;
hence thesis by A1,A2,A15,Def1;
end;
assume
A16: L=R;
A17: X c= dom IncProj (K,p,R)
proof
let e be object;
assume
A18: e in X;
then reconsider e as POINT of IPP by A9;
ex e9 being POINT of IPP st e=e9 & e9 on K by A9,A18;
hence thesis by A1,A2,A16,Def1;
end;
A19: 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
A20: x in X;
then
A21: (IncProj(R,q,R)*IncProj(K,p,R)).x = IncProj(R,q,R).(IncProj (K,p
,R).x) by A16,A13,FUNCT_1:12;
A22: x on K by A1,A2,A16,A17,A20,Def1;
then reconsider y =IncProj(K,p,R).x as POINT of IPP by A1,A2,A16,Th19;
y on R by A1,A2,A16,A22,Th20;
hence thesis by A3,A16,A21,Th18;
end;
dom (IncProj(L,q,R)*IncProj (K,p,L)) c= X
proof
let e be object;
assume e in dom (IncProj(L,q,R)*IncProj(K,p,L));
then
A23: e in dom IncProj(K,p,L) by A1,A2,A3,A4,Th22;
then reconsider e as POINT of IPP;
e on K by A1,A2,A23,Def1;
hence thesis by A9;
end;
then
A24: X = dom (IncProj(L,q,R)*IncProj(K,p,L)) by A13,XBOOLE_0:def 10;
A25: (IncProj(L,q,R)*IncProj(K,p,L)) is PartFunc of the Points of IPP,
the Points of IPP by A10,RELSET_1:4;
take p;
dom IncProj(K,p,R) c= X
proof
let e be object;
assume
A26: e in dom IncProj (K,p,R);
then reconsider e as POINT of IPP;
e on K by A1,A2,A16,A26,Def1;
hence thesis by A9;
end;
then X = dom IncProj(K,p,R) by A17,XBOOLE_0:def 10;
hence thesis by A1,A2,A16,A24,A19,A25,PARTFUN1:5;
end;
consider A such that
A27: p on A and
A28: q on A by INCPROJ:def 5;
consider c1 being POINT of IPP such that
A29: c1 on K and
A30: c1 on A by INCPROJ:def 9;
reconsider c2=IncProj(K,p,L).c1 as Element of the Points of IPP by A1,A2
,A29,Th19;
A31: c2 on L by A1,A2,A29,Th20;
then reconsider c3=IncProj(L,q,R).c2 as POINT of IPP by A3,A4,Th19;
A32: c3 on R by A3,A4,A31,Th20;
consider a1 being POINT of IPP such that
A33: a1 on K and
A34: c1<>a1 and
A35: c <>a1 by Th8;
reconsider a2 =IncProj(K,p,L).a1 as POINT of IPP by A1,A2,A33,Th19;
A36: a2 on L by A1,A2,A33,Th20;
then reconsider a3=IncProj(L,q,R).a2 as POINT of IPP by A3,A4,Th19;
A37: a3 on R by A3,A4,A36,Th20;
A38: not a3 on K
proof
assume a3 on K;
then
A39: c =a3 by A5,A7,A8,A37,INCPROJ:def 4;
ex C st q on C & c on C by INCPROJ:def 5;
then IncProj(L,q,R).c =a3 by A3,A4,A6,A7,A39,Def1;
then
A40: c =a2 by A3,A4,A6,A36,Th23;
ex D st p on D & c on D by INCPROJ:def 5;
then IncProj(K,p,L).c =a2 by A1,A2,A5,A6,A40,Def1;
hence contradiction by A1,A2,A5,A33,A35,Th23;
end;
consider B such that
A41: a1 on B & a3 on B by INCPROJ:def 5;
consider o being POINT of IPP such that
A42: o on A and
A43: o on B by INCPROJ:def 9;
A44: not a1 on R by A5,A7,A8,A33,A35,INCPROJ:def 4;
A45: not o on K & not o on R
proof
A46: now
assume
A47: o on R;
then
A48: o=a3 by A37,A41,A43,A44,INCPROJ:def 4;
consider A2 being LINE of IPP such that
A49: q on A2 and
A50: c2 on A2 and
A51: c3 on A2 by A3,A4,A31,A32,Def1;
ex A1 being LINE of IPP st p on A1 & c1 on A1 & c2 on A1 by A1,A2,A29
,A31,Def1;
then c2 on A by A1,A27,A29,A30,INCPROJ:def 4;
then A=A2 by A3,A28,A31,A49,A50,INCPROJ:def 4;
then o=c3 by A4,A42,A32,A47,A49,A51,INCPROJ:def 4;
then c2=a2 by A3,A4,A36,A31,A48,Th23;
hence contradiction by A1,A2,A29,A33,A34,Th23;
end;
A52: now
assume
A53: o on K;
then o=c1 by A1,A27,A29,A30,A42,INCPROJ:def 4;
hence contradiction by A33,A34,A41,A43,A38,A53,INCPROJ:def 4;
end;
assume not thesis;
hence thesis by A52,A46;
end;
assume
A54: p<>q;
A55: now
assume that
A56: L<>R and
K<>L;
A57: X c= dom (IncProj (L,q,R)*IncProj(K,p,L))
proof
let e be object;
assume
A58: e in X;
then reconsider e as POINT of IPP by A9;
A59: ex e9 being POINT of IPP st e=e9 & e9 on K by A9,A58;
dom (IncProj(L,q,R)*IncProj(K,p,L)) = dom IncProj(K,p,L) by A1,A2,A3,A4
,Th22;
hence thesis by A1,A2,A59,Def1;
end;
A60: 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
A61: x in X;
A62: now
assume
A63: x=c;
then (IncProj(L,q,R)*IncProj(K,p,L)).c = IncProj(L,q,R).(IncProj(K,
p,L).c) by A57,A61,FUNCT_1:12;
then (IncProj(L,q,R)*IncProj(K,p,L)).c = IncProj(L,q,R).c by A1,A2,A5
,A6,Th24;
then (IncProj(L,q,R)*IncProj(K,p,L)).c =c by A3,A4,A6,A7,Th24;
hence thesis by A5,A7,A45,A63,Th24;
end;
A64: now
assume that
x<>c1 and
A65: x<>c and
x<>a1;
(IncProj(L,q,R)*IncProj(K,p,L)).x = IncProj(K,o,R).x
proof
A66: a2<>a3
proof
assume a2=a3;
then
A67: IncProj(K,p,L).a1 = c by A6,A7,A36,A37,A56,INCPROJ:def 4;
IncProj(K, p,L).c = c by A1,A2,A5,A6,Th24;
hence contradiction by A1,A2,A5,A33,A35,A67,Th23;
end;
A68: (IncProj(L,q,R)*IncProj(K,p,L)).x = IncProj(L,q,R).(IncProj
(K,p,L).x) by A57,A61,FUNCT_1:12;
A69: a2<>c
proof
assume
A70: a2=c;
IncProj(K,p,L).c = c by A1,A2,A5,A6,Th24;
hence contradiction by A1,A2,A5,A33,A35,A70,Th23;
end;
A71: a3 on R by A3,A4,A36,Th20;
A72: dom ( IncProj (L,q,R)*IncProj(K,p,L))= dom IncProj(K,p,L) by A1,A2
,A3,A4,Th22;
then
A73: x on K by A1,A2,A57,A61,Def1;
then reconsider y = IncProj(K,p,L).x as POINT of IPP by A1,A2,Th19;
A74: y on L by A1,A2,A73,Th20;
then reconsider z = IncProj(L,q,R).y as POINT of IPP by A3,A4,Th19;
consider B3 being LINE of IPP such that
A75: p on B3 & x on B3 & y on B3 by A1,A2,A73,A74,Def1;
x on K by A1,A2,A57,A61,A72,Def1;
then
A76: c <>y by A1,A5,A65,A75,INCPROJ:def 4;
consider A1 being LINE of IPP such that
A77: q on A1 and
A78: a2 on A1 & a3 on A1 by A3,A4,A36,A37,Def1;
A79: {a2,a3,q} on A1 by A77,A78,INCSP_1:2;
A80: z on R by A3,A4,A74,Th20;
then consider B1 being LINE of IPP such that
A81: q on B1 & y on B1 & z on B1 by A3,A4,A74,Def1;
x on K by A1,A2,A57,A61,A72,Def1;
then
A82: {x,c,a1} on K by A5,A33,INCSP_1:2;
consider A3 being Element of the Lines of IPP such that
A83: p on A3 and
A84: a1 on A3 and
A85: a2 on A3 by A1,A2,A33,A36,Def1;
A86: {a2,p,a1} on A3 by A83,A84,A85,INCSP_1:2;
A1<>A3
proof
assume A1=A3;
then A=A3 by A54,A27,A28,A77,A83,INCPROJ:def 4;
hence contradiction by A1,A29,A30,A33,A34,A83,A84,INCPROJ:def 4;
end;
then
A87: A1,L,A3 are_mutually_distinct by A2,A3,A77,A83,ZFMISC_1:def 5;
A88: {a2,y,c} on L by A6,A36,A74,INCSP_1:2;
A89: {p,y,x} on B3 by A75,INCSP_1:2;
z on R by A3,A4,A74,Th20;
then
A90: {a3,z,c} on R by A7,A71,INCSP_1:2;
A91: {p,o,q} on A & {a3,o,a1} on B by A27,A28,A41,A42,A43,INCSP_1:2;
A92: a2<>p by A1,A2,A33,Th20;
{y,z,q} on B1 by A81,INCSP_1:2;
then consider O being LINE of IPP such that
A93: {o,z,x} on O by A69,A66,A76,A88,A79,A86,A89,A91,A82,A90,A87,A92
,Th12;
A94: o on O by A93,INCSP_1:2;
x on O & z on O by A93,INCSP_1:2;
hence thesis by A45,A73,A80,A94,A68,Def1;
end;
hence thesis;
end;
A95: now
assume
A96: x=c1;
(IncProj(L,q,R)*IncProj(K,p,L)).x = IncProj (K,o,R).x
proof
A97: (IncProj(L,q,R)*IncProj(K,p,L)).c1 =c3 by A57,A61,A96,FUNCT_1:12;
consider A2 being LINE of IPP such that
A98: q on A2 & c2 on A2 and
A99: c3 on A2 by A3,A4,A31,A32,Def1;
ex A1 being Element of the Lines of IPP st p on A1 & c1 on
A1 & c2 on A1 by A1,A2,A29,A31,Def1;
then c2 on A by A1,A27,A29,A30,INCPROJ:def 4;
then A=A2 by A3,A28,A31,A98,INCPROJ:def 4;
hence thesis by A29,A30,A42,A32,A45,A96,A97,A99,Def1;
end;
hence thesis;
end;
now
assume
A100: x=a1;
then (IncProj(L,q,R)*IncProj(K,p,L)).a1 =a3 by A57,A61,FUNCT_1:12;
hence thesis by A33,A37,A41,A43,A45,A100,Def1;
end;
hence thesis by A62,A95,A64;
end;
A101: dom IncProj(K,o,R) c= X
proof
let e be object;
assume
A102: e in dom IncProj (K,o,R);
then reconsider e as POINT of IPP;
e on K by A45,A102,Def1;
hence thesis by A9;
end;
X c= dom IncProj(K,o,R)
proof
let e be object;
assume
A103: e in X;
then reconsider e as POINT of IPP by A9;
ex e9 being POINT of IPP st e=e9 & e9 on K by A9,A103;
hence thesis by A45,Def1;
end;
then
A104: X = dom IncProj(K,o,R ) by A101,XBOOLE_0:def 10;
A105: (IncProj(L,q,R)* IncProj(K,p,L)) is PartFunc of the Points of IPP,
the Points of IPP by A10,RELSET_1:4;
dom (IncProj(L,q,R)*IncProj(K,p,L)) c= X
proof
let e be object;
assume e in dom (IncProj(L,q,R)*IncProj(K,p,L));
then
A106: e in dom IncProj (K,p,L) by A1,A2,A3,A4,Th22;
then reconsider e as POINT of IPP;
e on K by A1,A2,A106,Def1;
hence thesis by A9;
end;
then X = dom (IncProj(L,q,R)*IncProj(K,p,L)) by A57,XBOOLE_0:def 10;
hence thesis by A45,A60,A104,A105,PARTFUN1:5;
end;
now
A107: X c= dom (IncProj (L,q,R)*IncProj(K,p,L))
proof
let e be object;
assume
A108: e in X;
then reconsider e as Element of the Points of IPP by A9;
A109: ex e9 being POINT of IPP st e=e9 & e9 on K by A9,A108;
dom (IncProj(L,q,R)*IncProj(K,p,L)) = dom IncProj(K,p,L) by A1,A2,A3,A4
,Th22;
hence thesis by A1,A2,A109,Def1;
end;
dom (IncProj(L,q,R)*IncProj(K,p,L)) c= X
proof
let e be object;
assume e in dom (IncProj(L,q,R)*IncProj(K,p,L));
then
A110: e in dom IncProj (K,p,L) by A1,A2,A3,A4,Th22;
then reconsider e as POINT of IPP;
e on K by A1,A2,A110,Def1;
hence thesis by A9;
end;
then
A111: X = dom (IncProj(L,q,R)*IncProj(K,p,L)) by A107,XBOOLE_0:def 10;
A112: (IncProj(L,q,R)*IncProj(K,p,L)) is PartFunc of the Points of IPP,
the Points of IPP by A10,RELSET_1:4;
assume
A113: K=L;
A114: X c= dom IncProj(K,q,R)
proof
let e be object;
assume
A115: e in X;
then reconsider e as POINT of IPP by A9;
ex e9 being POINT of IPP st e=e9 & e9 on K by A9,A115;
hence thesis by A3,A4,A113,Def1;
end;
A116: 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 x in X;
then x on K & (IncProj(K,q,R)*IncProj(K,p,K)).x = IncProj(K,q,R).(
IncProj (K,p,K) .x) by A3,A4,A113,A107,A114,Def1,FUNCT_1:12;
hence thesis by A1,A113,Th18;
end;
take q;
dom IncProj(K,q,R) c= X
proof
let e be object;
assume
A117: e in dom IncProj (K,q,R);
then reconsider e as POINT of IPP;
e on K by A3,A4,A113,A117,Def1;
hence thesis by A9;
end;
then X = dom IncProj(K,q,R) by A114,XBOOLE_0:def 10;
hence thesis by A3,A4,A113,A111,A116,A112,PARTFUN1:5;
end;
hence thesis by A12,A55;
end;
now
A118: X c= dom (IncProj(L,q,R)*IncProj (K,p,L))
proof
let e be object;
assume
A119: e in X;
then reconsider e as POINT of IPP by A9;
A120: ex e9 being Element of the Points of IPP st e=e9 & e9 on K by A9,A119;
dom (IncProj(L,q,R)*IncProj(K,p,L))=dom IncProj(K,p,L) by A1,A2,A3,A4
,Th22;
hence thesis by A1,A2,A120,Def1;
end;
assume
A121: p=q;
A122: X c= dom IncProj (K,p,R)
proof
let e be object;
assume
A123: e in X;
then reconsider e as POINT of IPP by A9;
ex e9 being POINT of IPP st e=e9 & e9 on K by A9,A123;
hence thesis by A1,A4,A121,Def1;
end;
A124: 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
A125: x in X;
then
A126: (IncProj(L,p,R)*IncProj(K,p,L)).x = IncProj(L,p,R).(IncProj(K,p,L).
x) by A121,A118,FUNCT_1:12;
A127: x on K by A1,A4,A121,A122,A125,Def1;
then reconsider y = IncProj(K,p,L).x as POINT of IPP by A1,A2,Th19;
A128: y on L by A1,A2,A127,Th20;
then reconsider z = IncProj (L,p,R).y as POINT of IPP by A2,A4,A121,Th19;
consider A such that
A129: p on A & y on A by INCPROJ:def 5;
A130: z on R by A2,A4,A121,A128,Th20;
then consider C such that
A131: p on C & y on C and
A132: z on C by A2,A4,A121,A128,Def1;
A133: A=C by A2,A128,A129,A131,INCPROJ:def 4;
consider B such that
A134: p on B and
A135: x on B and
A136: y on B by A1,A2,A127,A128,Def1;
A=B by A2,A128,A129,A134,A136,INCPROJ:def 4;
hence thesis by A1,A4,A121,A127,A126,A134,A135,A130,A132,A133,Def1;
end;
dom (IncProj(L,q,R)*IncProj(K,p,L)) c= X
proof
let e be object;
assume e in dom (IncProj(L,q,R)*IncProj(K,p,L));
then
A137: e in dom IncProj (K,p,L) by A1,A2,A3,A4,Th22;
then reconsider e as POINT of IPP;
e on K by A1,A2,A137,Def1;
hence thesis by A9;
end;
then
A138: X = dom (IncProj(L,q,R)*IncProj(K,p,L)) by A118,XBOOLE_0:def 10;
A139: (IncProj(L,q,R)*IncProj(K,p,L))is PartFunc of the Points of IPP,the
Points of IPP by A10,RELSET_1:4;
dom IncProj(K,p,R) c= X
proof
let e be object;
assume
A140: e in dom IncProj (K,p,R);
then reconsider e as POINT of IPP;
e on K by A1,A4,A121,A140,Def1;
hence thesis by A9;
end;
then X = dom IncProj(K,p,R) by A122,XBOOLE_0:def 10;
hence thesis by A1,A4,A121,A138,A124,A139,PARTFUN1:5;
end;
hence thesis by A11;
end;