:: Desargues Theorem In Projective 3-Space
:: by Eugeniusz Kusak
::
:: Received August 13, 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 INCSP_1, ANPROJ_2, SUBSET_1, AFF_2, PROJDES1, PENCIL_1;
notations STRUCT_0, COLLSP, ANPROJ_2;
constructors ANPROJ_2, COLLSP;
registrations ANPROJ_2;
theorems ANPROJ_2, COLLSP;
begin
reserve FCPS for up-3-dimensional CollProjectiveSpace;
reserve a,a9,b,b9,c,c9,d,d9,o,p,q,r,s,t,u,x,y,z for Element of FCPS;
theorem Th1:
a,b,c are_collinear implies b,c,a are_collinear & c,a,b
are_collinear & b,a,c are_collinear & a,c,b are_collinear &
c,b,a are_collinear
proof
assume
A1: a,b,c are_collinear;
then b,a,c are_collinear by COLLSP:4;
then
A2: b,c,a are_collinear by COLLSP:4;
a,c,b are_collinear by A1,COLLSP:4;
hence thesis by A2,COLLSP:4;
end;
theorem
ex q,r st not p,q,r are_collinear
proof
consider q such that
A1: p<>q and
p<>q and
p,p,q are_collinear by ANPROJ_2:def 10;
ex r st not p,q,r are_collinear by A1,COLLSP:12;
hence thesis;
end;
theorem
not a,b,c are_collinear & a,b,b9 are_collinear & a<>b9 implies not a,b9,
c are_collinear
proof
assume that
A1: not a,b,c are_collinear and
A2: a,b,b9 are_collinear and
A3: a<>b9;
assume
A4: not thesis;
a,b9,b are_collinear by A2,Th1;
hence contradiction by A1,A3,A4,COLLSP:6;
end;
theorem
not a,b,c are_collinear & a,b,d are_collinear & a,c,d are_collinear
implies a=d
proof
assume that
A1: not a,b,c are_collinear and
A2: a,b,d are_collinear & a,c,d are_collinear;
assume
A3: not thesis;
A4: a,d,a are_collinear by ANPROJ_2:def 7;
a,d,b are_collinear & a,d,c are_collinear by A2,Th1;
hence contradiction by A1,A3,A4,ANPROJ_2:def 8;
end;
theorem Th5:
not o,a,d are_collinear & o,d,d9 are_collinear & d<>d9 & a9,d9,s
are_collinear & o,a,a9 are_collinear & o<>a9 implies s<>d
proof
assume that
A1: not o,a,d are_collinear and
A2: o,d,d9 are_collinear and
A3: d<>d9 and
A4: a9,d9,s are_collinear and
A5: o,a,a9 are_collinear and
A6: o<>a9;
assume not thesis;
then
A7: d,d9,a9 are_collinear by A4,Th1;
d,d9,o are_collinear by A2,Th1;
then d,o,a9 are_collinear by A3,A7,COLLSP:6;
then
A8: o,a9,d are_collinear by Th1;
o,a9,a are_collinear by A5,Th1;
hence contradiction by A1,A6,A8,COLLSP:6;
end;
Lm1: not a,b,c are_collinear & a,b,b9 are_collinear & a,c,c9 are_collinear &
a<>
b9 implies b9<>c9
proof
assume that
A1: not a,b,c are_collinear and
A2: a,b,b9 are_collinear and
A3: a,c,c9 are_collinear and
A4: a<>b9;
assume not thesis;
then
A5: a,b9,c are_collinear by A3,Th1;
a,b9,b are_collinear by A2,Th1;
hence contradiction by A1,A4,A5,COLLSP:6;
end;
definition
let FCPS,a,b,c,d;
pred a,b,c,d are_coplanar means
ex x being Element of FCPS st a,b,x are_collinear & c,d,x are_collinear;
end;
theorem Th6:
a,b,c are_collinear or b,c,d are_collinear or c,d,a are_collinear
or d,a,b are_collinear implies a,b,c,d are_coplanar
proof
A1: now
A2: c,d,c are_collinear by ANPROJ_2:def 7;
assume a,b,c are_collinear;
hence thesis by A2;
end;
A3: now
A4: a,b,a are_collinear by ANPROJ_2:def 7;
assume c,d,a are_collinear;
hence thesis by A4;
end;
A5: now
assume d,a,b are_collinear;
then
A6: a,b,d are_collinear by Th1;
c,d,d are_collinear by ANPROJ_2:def 7;
hence thesis by A6;
end;
A7: now
assume b,c,d are_collinear;
then
A8: c,d,b are_collinear by Th1;
a,b,b are_collinear by ANPROJ_2:def 7;
hence thesis by A8;
end;
assume a,b,c are_collinear or b,c,d are_collinear or c,d,a are_collinear
or d,
a,b are_collinear;
hence thesis by A1,A7,A3,A5;
end;
Lm2: a,b,c,d are_coplanar implies b,a,c,d are_coplanar
proof
assume a,b,c,d are_coplanar;
then consider x such that
A1: a,b,x are_collinear and
A2: c,d,x are_collinear;
b,a,x are_collinear by A1,Th1;
hence thesis by A2;
end;
Lm3: a,b,c,d are_coplanar implies b,c,d,a are_coplanar
proof
assume a,b,c,d are_coplanar;
then consider x such that
A1: a,b,x are_collinear & c,d,x are_collinear;
b,x,a are_collinear & x,c,d are_collinear by A1,Th1;
then consider y such that
A2: b,c,y are_collinear and
A3: a,d,y are_collinear by ANPROJ_2:def 9;
d,a,y are_collinear by A3,Th1;
hence thesis by A2;
end;
theorem Th7:
a,b,c,d are_coplanar implies b,c,d,a are_coplanar & c,d,a,b
are_coplanar & d,a,b,c are_coplanar & b,a,c,d are_coplanar & c,b,d,a
are_coplanar & d,c,a,b are_coplanar & a,d,b,c are_coplanar & a,c,d,b
are_coplanar & b,d,a,c are_coplanar & c,a,b,d are_coplanar & d,b,c,a
are_coplanar & c,a,d,b are_coplanar & d,b,a,c are_coplanar & a,c,b,d
are_coplanar & b,d,c,a are_coplanar & a,b,d,c are_coplanar & a,d,c,b
are_coplanar & b,c,a,d are_coplanar & b,a,d,c are_coplanar & c,b,a,d
are_coplanar & c,d,b,a are_coplanar & d,a,c,b are_coplanar & d,c,b,a
are_coplanar
proof
assume
A1: a,b,c,d are_coplanar;
then
b,a,c,d are_coplanar by Lm2;
then a,c,d,b are_coplanar by Lm3;
then
A2: c,d,b,a are_coplanar by Lm3;
then
A3: d,b,a,c are_coplanar by Lm3;
then b,d,a,c are_coplanar by Lm2;
then
A4: d,a,c,b are_coplanar by Lm3;
then
a,c,b,d are_coplanar by Lm3;
then c,a,b,d are_coplanar by Lm2;
then
A5: a,b,d,c are_coplanar by Lm3;
then
A6: b,d,c,a are_coplanar by Lm3;
then
d,c,a,b are_coplanar by Lm3;
then c,d,a,b are_coplanar by Lm2;
then
A7: d,a,b,c are_coplanar by Lm3;
then a,d,b,c are_coplanar by Lm2;
then d,b,c,a are_coplanar by Lm3;
then b,c,a,d are_coplanar by Lm3;
hence thesis by A1,A2,A3,A4,A5,A6,A7,Lm2,Lm3;
end;
Lm4: not a,b,c are_collinear & a,b,c,p are_coplanar & a,b,c,q are_coplanar
implies a,b,p,q are_coplanar
proof
assume that
A1: not a,b,c are_collinear and
A2: a,b,c,p are_coplanar and
A3: a,b,c,q are_coplanar;
consider x such that
A4: a,b,x are_collinear and
A5: c,p,x are_collinear by A2;
consider y such that
A6: a,b,y are_collinear and
A7: c,q,y are_collinear by A3;
A8: now
assume
A9: a<>b;
b,a,x are_collinear & b,a,y are_collinear by A4,A6,Th1;
then b,x,y are_collinear by A9,COLLSP:6;
then
A10: x,y,b are_collinear by Th1;
a,x,y are_collinear by A4,A6,A9,COLLSP:6;
then
A11: x,y,a are_collinear by Th1;
A12: now
p,c,x are_collinear by A5,Th1;
then consider z such that
A13: p,q,z are_collinear and
A14: x,y,z are_collinear by A7,ANPROJ_2:def 9;
assume x<>y;
then a,b,z are_collinear by A11,A10,A14,ANPROJ_2:def 8;
hence thesis by A13;
end;
now
assume x=y;
then
A15: x,c,q are_collinear by A7,Th1;
x,c,p are_collinear by A5,Th1;
then x,p,q are_collinear by A1,A4,A15,COLLSP:6;
then p,q,x are_collinear by Th1;
hence thesis by A4;
end;
hence thesis by A12;
end;
now
assume a=b;
then a,b,p are_collinear by ANPROJ_2:def 7;
hence thesis by Th6;
end;
hence thesis by A8;
end;
theorem Th8:
not a,b,c are_collinear & a,b,c,p are_coplanar & a,b,c,q
are_coplanar & a,b,c,r are_coplanar & a,b,c,s are_coplanar implies
p,q,r,s are_coplanar
proof
assume that
A1: not a,b,c are_collinear and
A2: a,b,c,p are_coplanar and
A3: a,b,c,q are_coplanar and
A4: a,b,c,r are_coplanar and
A5: a,b,c,s are_coplanar;
A6: a,b,p,q are_coplanar by A1,A2,A3,Lm4;
A7: a,b,q,r are_coplanar by A1,A3,A4,Lm4;
A8: a,b,p,r are_coplanar by A1,A2,A4,Lm4;
A9: a,b,q,s are_coplanar by A1,A3,A5,Lm4;
A10: now
A11: q,a,b,r are_coplanar by A7,Th7;
assume
A12: not a,b,q are_collinear;
then
A13: not q,a,b are_collinear by Th1;
A14: q,a,b,p are_coplanar by A6,Th7;
then
A15: q,a,p,r are_coplanar by A13,A11,Lm4;
A16: q,a,b,s are_coplanar by A9,Th7;
then
A17: q,a,p,s are_coplanar by A13,A14,Lm4;
A18: now
assume not q,a,p are_collinear;
then
A19: not q,p,a are_collinear by Th1;
q,p,a,r are_coplanar & q,p,a,s are_coplanar by A15,A17,Th7;
then q,p,r,s are_coplanar by A19,Lm4;
hence thesis by Th7;
end;
A20: q,a,r,s are_coplanar by A13,A11,A16,Lm4;
A21: now
assume not q,a,r are_collinear;
then
A22: not q,r,a are_collinear by Th1;
q,r,a,p are_coplanar & q,r,a,s are_coplanar by A15,A20,Th7;
then q,r,p,s are_coplanar by A22,Lm4;
hence thesis by Th7;
end;
A23: q<>a by A12,ANPROJ_2:def 7;
now
assume q,a,p are_collinear & q,a,r are_collinear;
then q,p,r are_collinear by A23,COLLSP:6;
then p,q,r are_collinear by Th1;
hence thesis by Th6;
end;
hence thesis by A18,A21;
end;
A24: a,b,r,s are_coplanar by A1,A4,A5,Lm4;
A25: now
A26: r,a,b,q are_coplanar by A7,Th7;
assume
A27: not a,b,r are_collinear;
then
A28: not r,a,b are_collinear by Th1;
A29: r,a,b,p are_coplanar by A8,Th7;
then
A30: r,a,p,q are_coplanar by A28,A26,Lm4;
A31: r,a,b,s are_coplanar by A24,Th7;
then
A32: r,a,p,s are_coplanar by A28,A29,Lm4;
A33: now
assume not r,a,p are_collinear;
then
A34: not r,p,a are_collinear by Th1;
r,p,a,q are_coplanar & r,p,a,s are_coplanar by A30,A32,Th7;
then r,p,q,s are_coplanar by A34,Lm4;
hence thesis by Th7;
end;
A35: r,a,q,s are_coplanar by A28,A26,A31,Lm4;
A36: now
assume not r,a,q are_collinear;
then
A37: not r,q,a are_collinear by Th1;
r,q,a,p are_coplanar & r,q,a,s are_coplanar by A30,A35,Th7;
then r,q,p,s are_coplanar by A37,Lm4;
hence thesis by Th7;
end;
A38: r<>a by A27,ANPROJ_2:def 7;
now
assume r,a,p are_collinear & r,a,q are_collinear;
then r,p,q are_collinear by A38,COLLSP:6;
then p,q,r are_collinear by Th1;
hence thesis by Th6;
end;
hence thesis by A33,A36;
end;
A39: a,b,p,s are_coplanar by A1,A2,A5,Lm4;
A40: now
A41: p,a,b,r are_coplanar by A8,Th7;
assume
A42: not a,b,p are_collinear;
then
A43: not p,a,b are_collinear by Th1;
A44: p,a,b,q are_coplanar by A6,Th7;
then
A45: p,a,q,r are_coplanar by A43,A41,Lm4;
A46: p,a,b,s are_coplanar by A39,Th7;
then
A47: p,a,q,s are_coplanar by A43,A44,Lm4;
A48: now
assume not p,a,q are_collinear;
then
A49: not p,q,a are_collinear by Th1;
p,q,a,r are_coplanar & p,q,a,s are_coplanar by A45,A47,Th7;
hence thesis by A49,Lm4;
end;
A50: p,a,r,s are_coplanar by A43,A41,A46,Lm4;
A51: now
assume not p,a,r are_collinear;
then
A52: not p,r,a are_collinear by Th1;
p,r,a,q are_coplanar & p,r,a,s are_coplanar by A45,A50,Th7;
then p,r,q,s are_coplanar by A52,Lm4;
hence thesis by Th7;
end;
A53: p<>a by A42,ANPROJ_2:def 7;
now
assume p,a,q are_collinear & p,a,r are_collinear;
then p,q,r are_collinear by A53,COLLSP:6;
hence thesis by Th6;
end;
hence thesis by A48,A51;
end;
A54: a<>b by A1,ANPROJ_2:def 7;
now
assume a,b,p are_collinear & a,b,q are_collinear & a,b,r are_collinear;
then p,q,r are_collinear by A54,ANPROJ_2:def 8;
hence thesis by Th6;
end;
hence thesis by A40,A10,A25;
end;
Lm5: not a,b,c are_collinear & a,b,c,p are_coplanar & a,b,c,q are_coplanar & a,
b,c,r are_coplanar implies a,p,q,r are_coplanar
proof
assume that
A1: not a,b,c are_collinear and
A2: a,b,c,p are_coplanar and
A3: a,b,c,q are_coplanar and
A4: a,b,c,r are_coplanar;
now
A5: now
a,b,r,q are_coplanar by A1,A3,A4,Lm4;
then
A6: a,r,b,q are_coplanar by Th7;
a,b,r,p are_coplanar by A1,A2,A4,Lm4;
then
A7: a,r,b,p are_coplanar by Th7;
assume not a,r,b are_collinear;
then a,r,p,q are_coplanar by A7,A6,Lm4;
hence thesis by Th7;
end;
A8: now
a,b,p,r are_coplanar by A1,A2,A4,Lm4;
then
A9: a,p,b,r are_coplanar by Th7;
a,b,p,q are_coplanar by A1,A2,A3,Lm4;
then
A10: a,p,b,q are_coplanar by Th7;
assume not a,p,b are_collinear;
hence thesis by A10,A9,Lm4;
end;
A11: now
a,b,q,r are_coplanar by A1,A3,A4,Lm4;
then
A12: a,q,b,r are_coplanar by Th7;
a,b,q,p are_coplanar by A1,A2,A3,Lm4;
then
A13: a,q,b,p are_coplanar by Th7;
assume not a,q,b are_collinear;
then a,q,p,r are_coplanar by A13,A12,Lm4;
hence thesis by Th7;
end;
assume
A14: not p,q,r are_collinear;
a<>b by A1,ANPROJ_2:def 7;
then not a,b,p are_collinear or not a,b,q are_collinear or not a,b,r
are_collinear by A14,ANPROJ_2:def 8;
hence thesis by A8,A11,A5,Th1;
end;
hence thesis by Th6;
end;
theorem
not p,q,r are_collinear & a,b,c,p are_coplanar & a,b,c,r are_coplanar &
a,b,c,q are_coplanar & p,q,r,s are_coplanar implies a,b,c,s are_coplanar
proof
assume that
A1: not p,q,r are_collinear and
A2: a,b,c,p are_coplanar and
A3: a,b,c,r are_coplanar and
A4: a,b,c,q are_coplanar and
A5: p,q,r,s are_coplanar;
now
b,b,a are_collinear by ANPROJ_2:def 7;
then
A6: b,a,c,b are_coplanar by Th6;
A7: b,a,c,r are_coplanar by A3,Th7;
assume
A8: not a,b,c are_collinear;
then
A9: not b,a,c are_collinear by Th1;
a,p,q,r are_coplanar by A2,A3,A4,A8,Lm5;
then
A10: p,q,r,a are_coplanar by Th7;
A11: c,a,b,r are_coplanar by A3,Th7;
A12: not c,a,b are_collinear by A8,Th1;
c,a,b,p are_coplanar & c,a,b,q are_coplanar by A2,A4,Th7;
then c,p,q,r are_coplanar by A12,A11,Lm5;
then
A13: p,q,r,c are_coplanar by Th7;
b,a,c,p are_coplanar & b,a,c,q are_coplanar by A2,A4,Th7;
then p,q,r,b are_coplanar by A9,A6,A7,Th8;
hence thesis by A1,A5,A10,A13,Th8;
end;
hence thesis by Th6;
end;
Lm6: p<>q & p,q,r are_collinear & a,b,p,q are_coplanar implies a,b,p,r
are_coplanar
proof
assume that
A1: p<>q & p,q,r are_collinear and
A2: a,b,p,q are_coplanar;
consider x such that
A3: a,b,x are_collinear and
A4: p,q,x are_collinear by A2;
p,r,x are_collinear by A1,A4,COLLSP:6;
hence thesis by A3;
end;
theorem Th10:
p<>q & p,q,r are_collinear & a,b,c,p are_coplanar & a,b,c,q
are_coplanar implies a,b,c,r are_coplanar
proof
assume that
A1: p<>q and
A2: p,q,r are_collinear and
A3: a,b,c,p are_coplanar and
A4: a,b,c,q are_coplanar;
A5: q,p,r are_collinear by A2,Th1;
now
assume
A6: not a,b,c are_collinear;
then a,b,p,q are_coplanar by A3,A4,Lm4;
then
A7: a,b,p,r are_coplanar by A1,A2,Lm6;
A8: now
b,a,b are_collinear by ANPROJ_2:def 7;
then
A9: a,b,p,b are_coplanar by Th6;
a,a,b are_collinear by ANPROJ_2:def 7;
then
A10: a,b,p,a are_coplanar by Th6;
assume
A11: not a,b,p are_collinear;
a,b,p,c are_coplanar by A3,Th7;
hence thesis by A7,A11,A10,A9,Th8;
end;
a,b,q,p are_coplanar by A3,A4,A6,Lm4;
then
A12: a,b,q,r are_coplanar by A1,A5,Lm6;
A13: now
b,a,b are_collinear by ANPROJ_2:def 7;
then
A14: a,b,q,b are_coplanar by Th6;
a,a,b are_collinear by ANPROJ_2:def 7;
then
A15: a,b,q,a are_coplanar by Th6;
assume
A16: not a,b,q are_collinear;
a,b,q,c are_coplanar by A4,Th7;
hence thesis by A12,A16,A15,A14,Th8;
end;
now
assume a,b,p are_collinear & a,b,q are_collinear;
then a,b,r are_collinear by A1,A2,COLLSP:9;
then r,a,b are_collinear by Th1;
hence thesis by Th6;
end;
hence thesis by A8,A13;
end;
hence thesis by Th6;
end;
theorem
not a,b,c are_collinear & a,b,c,p are_coplanar & a,b,c,q are_coplanar &
a,b,c,r are_coplanar & a,b,c,s are_coplanar implies
ex x st p,q,x are_collinear & r,s,x are_collinear
proof
assume not a,b,c are_collinear & a,b,c,p are_coplanar &
a,b,c,q are_coplanar & a,b,c,r are_coplanar & a,b,c,s are_coplanar;
then p,q,r,s are_coplanar by Th8;
hence thesis;
end;
theorem Th12:
ex a,b,c,d st not a,b,c,d are_coplanar
proof
consider a,b,c,d such that
A1: not a,b,x are_collinear or not c,d,x are_collinear by ANPROJ_2:def 14;
take a,b,c,d;
thus thesis by A1;
end;
theorem Th13:
not p,q,r are_collinear implies ex s st not p,q,r,s are_coplanar
proof
assume
A1: not p,q,r are_collinear;
consider a,b,c,d such that
A2: not a,b,c,d are_coplanar by Th12;
assume
A3: not thesis;
then
A4: p,q,r,c are_coplanar & p,q,r,d are_coplanar;
p,q,r,a are_coplanar & p,q,r,b are_coplanar by A3;
hence contradiction by A1,A2,A4,Th8;
end;
theorem Th14:
a=b or a=c or b=c or a=d or b=d or d=c implies a,b,c,d are_coplanar
proof
A1: now
assume a=b or a=c or b=c;
then a,b,c are_collinear by ANPROJ_2:def 7;
hence thesis by Th6;
end;
A2: now
assume a=d or b=d;
then d,a,b are_collinear by ANPROJ_2:def 7;
hence thesis by Th6;
end;
A3: now
assume d=c;
then b,c,d are_collinear by ANPROJ_2:def 7;
hence thesis by Th6;
end;
assume a=b or a=c or b=c or a=d or b=d or d=c;
hence thesis by A1,A2,A3;
end;
theorem Th15:
not a,b,c,o are_coplanar & o,a,a9 are_collinear & a<>a9 implies
not a,b,c,a9 are_coplanar
proof
assume that
A1: not a,b,c,o are_coplanar and
A2: o,a,a9 are_collinear and
A3: a<>a9;
assume
A4: not thesis;
A5: a,b,c,a are_coplanar by Th14;
a,a9,o are_collinear by A2,Th1;
hence contradiction by A1,A3,A4,A5,Th10;
end;
theorem Th16:
not a,b,c are_collinear & not a9,b9,c9 are_collinear & a,b,c,p
are_coplanar & a,b,c,q are_coplanar & a,b,c,r are_coplanar & a9,b9,c9,p
are_coplanar & a9,b9,c9,q are_coplanar & a9,b9,c9,r are_coplanar & not a,b,c,a9
are_coplanar implies p,q,r are_collinear
proof
assume that
A1: not a,b,c are_collinear and
A2: not a9,b9,c9 are_collinear and
A3: a,b,c,p are_coplanar & a,b,c,q are_coplanar & a,b,c,r are_coplanar and
A4: a9,b9,c9,p are_coplanar & a9,b9,c9,q are_coplanar & a9,b9,c9,r
are_coplanar and
A5: not a,b,c,a9 are_coplanar;
a,b,c,a are_coplanar by Th14;
then
A6: p,q,r,a are_coplanar by A1,A3,Th8;
a9,b9,c9,a9 are_coplanar by Th14;
then
A7: p,q,r,a9 are_coplanar by A2,A4,Th8;
a,b,c,c are_coplanar by Th14;
then
A8: p,q,r,c are_coplanar by A1,A3,Th8;
a,b,c,b are_coplanar by Th14;
then
A9: p,q,r,b are_coplanar by A1,A3,Th8;
assume not thesis;
hence contradiction by A5,A6,A9,A8,A7,Th8;
end;
theorem Th17:
a<>a9 & o,a,a9 are_collinear & not a,b,c,o are_coplanar & not a9,
b9,c9 are_collinear & a,b,p are_collinear & a9,b9,p are_collinear & b,c,q
are_collinear & b9,c9,q are_collinear & a,c,r are_collinear &
a9,c9,r are_collinear
implies p,q,r are_collinear
proof
assume that
A1: a<>a9 & o,a,a9 are_collinear & not a,b,c,o are_coplanar and
A2: not a9,b9,c9 are_collinear and
A3: a,b,p are_collinear and
A4: a9,b9,p are_collinear and
A5: b,c,q are_collinear & b9,c9,q are_collinear and
A6: a,c,r are_collinear and
A7: a9,c9,r are_collinear;
A8: a,b,c,q are_coplanar & a9,b9,c9,q are_coplanar by A5,Th6;
c9,r,a9 are_collinear by A7,Th1;
then
A9: a9,b9,c9,r are_coplanar by Th6;
p,a9,b9 are_collinear by A4,Th1;
then
A10: a9,b9,c9,p are_coplanar by Th6;
c,r,a are_collinear by A6,Th1;
then
A11: a,b,c,r are_coplanar by Th6;
p,a,b are_collinear by A3,Th1;
then
A12: a,b,c,p are_coplanar by Th6;
( not a,b,c,a9 are_coplanar)& not a,b,c are_collinear by A1,Th6,Th15;
hence thesis by A2,A12,A11,A10,A8,A9,Th16;
end;
theorem Th18:
not a,b,c,d are_coplanar & a,b,c,o are_coplanar & not a,b,o
are_collinear implies not a,b,d,o are_coplanar
proof
assume that
A1: not a,b,c,d are_coplanar and
A2: a,b,c,o are_coplanar and
A3: not a,b,o are_collinear;
assume not thesis;
then
A4: a,b,o,d are_coplanar by Th7;
a,b,o,c are_coplanar by A2,Th7;
hence contradiction by A1,A3,A4,Lm4;
end;
theorem Th19:
not a,b,c,o are_coplanar & o,a,a9 are_collinear & o,b,b9
are_collinear & o,c,c9 are_collinear & o<>a9 & o<>b9 & o<>c9
implies not a9,b9,c9
are_collinear & not a9,b9,c9,o are_coplanar
proof
assume that
A1: ( not a,b,c,o are_coplanar)& o,a,a9 are_collinear and
A2: o,b,b9 are_collinear and
A3: o,c,c9 are_collinear and
A4: o<>a9 and
A5: o<>b9 and
A6: o<>c9;
a,o,a9 are_collinear & not o,b,c,a are_coplanar by A1,Th1,Th7;
then not o,b,c,a9 are_coplanar by A4,Th15;
then
A7: not o,a9,b,c are_coplanar by Th7;
c,o,c9 are_collinear by A3,Th1;
then not o,a9,b,c9 are_coplanar by A6,A7,Th15;
then
A8: not o,a9,c9,b are_coplanar by Th7;
b,o,b9 are_collinear by A2,Th1;
then not o,a9,c9,b9 are_coplanar by A5,A8,Th15;
then not a9,b9,c9,o are_coplanar by Th7;
hence thesis by Th6;
end;
theorem Th20:
a,b,c,o are_coplanar & not a,b,c,d are_coplanar & not a,b,d,o
are_coplanar & o,d,d9 are_collinear & o,a,a9 are_collinear &
o,b,b9 are_collinear
& a,d,s are_collinear & a9,d9,s are_collinear & b,d,t are_collinear & b9,d9,t
are_collinear & c,d,u are_collinear & o<>a9 & d<>d9 & o<>b9 implies not s,t,u
are_collinear
proof
assume that
A1: a,b,c,o are_coplanar and
A2: not a,b,c,d are_coplanar and
A3: not a,b,d,o are_coplanar and
A4: o,d,d9 are_collinear and
A5: o,a,a9 are_collinear and
A6: o,b,b9 are_collinear and
A7: a,d,s are_collinear and
A8: a9,d9,s are_collinear and
A9: b,d,t are_collinear and
A10: b9,d9,t are_collinear and
A11: c,d,u are_collinear and
A12: o<>a9 and
A13: d<>d9 and
A14: o<>b9;
A15: d,b,c,b are_coplanar by Th14;
A16: not d,b,c,a are_coplanar by A2,Th7;
then
A17: not d,b,c are_collinear by Th6;
not b,d,o are_collinear by A3,Th6;
then not o,b,d are_collinear by Th1;
then
A18: t<>d by A4,A6,A10,A13,A14,Th5;
d,b,t are_collinear & d,c,u are_collinear by A9,A11,Th1;
then
A19: t<>u by A17,A18,Lm1;
A20: d,b,c,d are_coplanar by Th14;
not d,o,a are_collinear by A3,Th6;
then not o,a,d are_collinear by Th1;
then s<>d by A4,A5,A8,A12,A13,Th5;
then
A21: not d,b,c,s are_coplanar by A7,A16,Th15;
b<>d by A2,Th14;
then
A22: d,b,c,t are_coplanar by A9,A15,A20,Th10;
d,b,c,c are_coplanar by Th14;
then d,b,c,u are_coplanar by A1,A3,A11,A20,Th10;
then not t,u,s are_collinear by A21,A22,A19,Th10;
hence thesis by Th1;
end;
definition
let FCPS,o,a,b,c;
pred o,a,b,c constitute_a_quadrangle means
not a,b,c are_collinear &
not o,a,b are_collinear & not o,b,c are_collinear & not o,c,a are_collinear;
end;
Lm7: o<>a9 & o<>b9 & o<>c9 & a<>a9 & b<>b9 & o,a,b,c constitute_a_quadrangle &
o,a,a9 are_collinear & o,b,b9 are_collinear & o,c,c9 are_collinear & a,b,p
are_collinear & a9,b9,p are_collinear & b,c,q are_collinear &
b9,c9,q are_collinear
& a,c,r are_collinear & a9,c9,r are_collinear implies p,q,r are_collinear
proof
assume that
A1: o<>a9 and
A2: o<>b9 and
A3: o<>c9 and
A4: a<>a9 and
A5: b<>b9 and
A6: o,a,b,c constitute_a_quadrangle and
A7: o,a,a9 are_collinear and
A8: o,b,b9 are_collinear and
A9: o,c,c9 are_collinear and
A10: a,b,p are_collinear and
A11: a9,b9,p are_collinear and
A12: b,c,q are_collinear and
A13: b9,c9,q are_collinear and
A14: a,c,r are_collinear and
A15: a9,c9,r are_collinear;
A16: not o,b,c are_collinear by A6;
A17: not a,b,c are_collinear by A6;
A18: not o,c,a are_collinear by A6;
A19: not o,a,b are_collinear by A6;
A20: now
assume
A21: a,b,c,o are_coplanar;
then
A22: b,c,a,o are_coplanar by Th7;
A23: a,c,b,o are_coplanar by A21,Th7;
consider d such that
A24: not a,b,c,d are_coplanar by A17,Th13;
A25: not a,c,b,d are_coplanar by A24,Th7;
A26: a,b,c,c are_coplanar by Th14;
A27: not b,c,a,d are_coplanar by A24,Th7;
consider d9 such that
A28: o<>d9 and
A29: d<>d9 and
A30: o,d,d9 are_collinear by ANPROJ_2:def 10;
a,o,a9 are_collinear by A7,Th1;
then consider s such that
A31: a,d,s are_collinear and
A32: a9,d9,s are_collinear by A30,ANPROJ_2:def 9;
A33: d,a,s are_collinear by A31,Th1;
b,o,b9 are_collinear by A8,Th1;
then consider t such that
A34: b,d,t are_collinear & b9,d9,t are_collinear by A30,ANPROJ_2:def 9;
c,o,c9 are_collinear by A9,Th1;
then consider u such that
A35: c,d,u are_collinear and
A36: c9,d9,u are_collinear by A30,ANPROJ_2:def 9;
A37: s,t,u,s are_coplanar by Th14;
not a,c,o are_collinear by A18,Th1;
then
A38: not a,c,d,o are_coplanar by A25,A23,Th18;
then not a9,c9,d9 are_collinear by A1,A3,A7,A9,A28,A30,Th19;
then r,u,s are_collinear by A4,A7,A14,A15,A31,A32,A35,A36,A38,Th17;
then
A39: s,u,r are_collinear by Th1;
not a,b,o are_collinear by A19,Th1;
then
A40: not a,b,d,o are_coplanar by A21,A24,Th18;
then not d,o,a are_collinear by Th6;
then
A41: not o,d,a are_collinear by Th1;
A42: s,t,u,u are_coplanar by Th14;
not b,c,o are_collinear by A16,Th1;
then
A43: not b,c,d,o are_coplanar by A27,A22,Th18;
then not b9,c9,d9 are_collinear by A2,A3,A8,A9,A28,A30,Th19;
then q,u,t are_collinear by A5,A8,A12,A13,A34,A35,A36,A43,Th17;
then
A44: u,t,q are_collinear by Th1;
A45: s,t,u,t are_coplanar by Th14;
d9,a9,s are_collinear by A32,Th1;
then s<>a by A4,A7,A28,A30,A41,Th5;
then
A46: not a,b,c,s are_coplanar by A24,A33,Th15;
A47: a,b,c,b are_coplanar by Th14;
not a9,b9,d9 are_collinear by A1,A2,A7,A8,A28,A30,A40,Th19;
then p,t,s are_collinear by A4,A7,A10,A11,A31,A32,A34,A40,Th17;
then
A48: t,s,p are_collinear by Th1;
A49: a,b,c,a are_coplanar by Th14;
A50: not s,t,u are_collinear by A1,A2,A7,A8,A21,A24,A29,A30,A31,A32,A34,A35,A40
,Th20;
then t<>u by ANPROJ_2:def 7;
then
A51: s,t,u,q are_coplanar by A44,A45,A42,Th10;
c <>a by A18,ANPROJ_2:def 7;
then
A52: a,b,c,r are_coplanar by A14,A49,A26,Th10;
b<>c by A16,ANPROJ_2:def 7;
then
A53: a,b,c,q are_coplanar by A12,A47,A26,Th10;
a<>b by A19,ANPROJ_2:def 7;
then
A54: a,b,c,p are_coplanar by A10,A49,A47,Th10;
u<>s by A50,ANPROJ_2:def 7;
then
A55: s,t,u,r are_coplanar by A39,A37,A42,Th10;
s<>t by A50,ANPROJ_2:def 7;
then s,t,u,p are_coplanar by A48,A37,A45,Th10;
hence thesis by A17,A50,A46,A54,A53,A52,A51,A55,Th16;
end;
now
assume
A56: not a,b,c,o are_coplanar;
then not a9,b9,c9 are_collinear by A1,A2,A3,A7,A8,A9,Th19;
hence thesis by A4,A7,A10,A11,A12,A13,A14,A15,A56,Th17;
end;
hence thesis by A20;
end;
theorem Th21:
not o,a,b are_collinear & not o,b,c are_collinear & not o,a,c
are_collinear & o,a,a9 are_collinear & o,b,b9 are_collinear &
o,c,c9 are_collinear
& a,b,p are_collinear & a9,b9,p are_collinear & a<>a9 & b,c,r are_collinear &
b9,
c9,r are_collinear & a,c,q are_collinear & b<>b9 & a9,c9,q are_collinear
& o<>a9 &
o<>b9 & o<>c9 implies r,q,p are_collinear
proof
assume that
A1: not o,a,b are_collinear and
A2: not o,b,c are_collinear and
A3: not o,a,c are_collinear and
A4: o,a,a9 are_collinear & o,b,b9 are_collinear & o,c,c9 are_collinear and
A5: a,b,p are_collinear and
A6: a9,b9,p are_collinear & a<>a9 and
A7: b,c,r are_collinear and
A8: b9,c9,r are_collinear and
A9: a,c,q are_collinear and
A10: b<>b9 & a9,c9,q are_collinear & o<>a9 & o<>b9 & o<>c9;
A11: now
A12: b<>c & b,c,b are_collinear by A2,ANPROJ_2:def 7;
assume
A13: a,b,c are_collinear;
then b,c,a are_collinear by Th1;
then
A14: a,b,r are_collinear by A7,A12,ANPROJ_2:def 8;
A15: c <>a & a,c,a are_collinear by A3,ANPROJ_2:def 7;
a,c,b are_collinear by A13,Th1;
then
A16: a,b,q are_collinear by A9,A15,ANPROJ_2:def 8;
a<>b by A1,ANPROJ_2:def 7;
hence thesis by A5,A14,A16,ANPROJ_2:def 8;
end;
A17: not o,c,a are_collinear by A3,Th1;
now
assume not a,b,c are_collinear;
then o,a,b,c constitute_a_quadrangle by A1,A2,A17;
then p,r,q are_collinear by A4,A5,A6,A7,A8,A9,A10,Lm7;
hence thesis by Th1;
end;
hence thesis by A11;
end;
theorem Th22:
for CS being up-3-dimensional CollProjectiveSpace holds CS is Desarguesian
proof
let CS be up-3-dimensional CollProjectiveSpace;
for o,a,b,c,a9,b9,c9,r,q,p being Element of CS st o<>a9 & a<>a9 & o<>b9
& b<>b9 & o<>c9 & c <>c9 & not o,a,b are_collinear &
not o,a,c are_collinear &
not o,b,c are_collinear & a,b,p are_collinear & a9,b9,p are_collinear
& b,c,r
are_collinear & b9,c9,r are_collinear & a,c,q are_collinear &
a9,c9,q are_collinear
& o,a,a9 are_collinear & o,b,b9 are_collinear & o,c,c9 are_collinear
holds r,q,p
are_collinear by Th21;
hence thesis by ANPROJ_2:def 12;
end;
registration
cluster -> Desarguesian for up-3-dimensional CollProjectiveSpace;
correctness by Th22;
end;