incproj.miz
begin
reserve CPS for
proper
CollSp,
B for
Subset of CPS,
p for
Point of CPS,
x,y,z,Y for
set;
definition
let CPS;
:: original:
LINE
redefine
mode
LINE of CPS ->
Subset of CPS ;
coherence
proof
let x be
LINE of CPS;
x
c= the
carrier of CPS
proof
consider a,b be
Point of CPS such that a
<> b and
A1: x
= (
Line (a,b)) by
COLLSP:def 7;
let z be
object;
assume z
in x;
then z
in { p : (a,b,p)
are_collinear } by
A1,
COLLSP:def 5;
then ex p be
Point of CPS st z
= p & (a,b,p)
are_collinear ;
hence z
in the
carrier of CPS;
end;
hence thesis;
end;
end
definition
let CPS;
::
INCPROJ:def1
func
ProjectiveLines (CPS) ->
set equals { B : B is
LINE of CPS };
coherence ;
end
registration
let CPS;
cluster (
ProjectiveLines CPS) -> non
empty;
coherence
proof
set x = the
LINE of CPS;
x
in (
ProjectiveLines CPS);
hence thesis;
end;
end
theorem ::
INCPROJ:1
Th1: x is
LINE of CPS iff x is
Element of (
ProjectiveLines CPS)
proof
hereby
assume x is
LINE of CPS;
then x
in { B : B is
LINE of CPS };
hence x is
Element of (
ProjectiveLines CPS);
end;
assume x is
Element of (
ProjectiveLines CPS);
then x
in (
ProjectiveLines CPS);
then ex B st x
= B & B is
LINE of CPS;
hence thesis;
end;
definition
let CPS;
::
INCPROJ:def2
func
Proj_Inc (CPS) ->
Relation of the
carrier of CPS, (
ProjectiveLines CPS) means
:
Def2: for x,y be
object holds
[x, y]
in it iff x
in the
carrier of CPS & y
in (
ProjectiveLines CPS) & ex Y st y
= Y & x
in Y;
existence
proof
defpred
P[
object,
object] means ex Y st $2
= Y & $1
in Y;
ex IT be
Relation of the
carrier of CPS, (
ProjectiveLines CPS) st for x,y be
object holds
[x, y]
in IT iff x
in the
carrier of CPS & y
in (
ProjectiveLines CPS) &
P[x, y] from
RELSET_1:sch 1;
hence thesis;
end;
uniqueness
proof
let R1,R2 be
Relation of the
carrier of CPS, (
ProjectiveLines CPS) such that
A1: for x,y be
object holds
[x, y]
in R1 iff x
in the
carrier of CPS & y
in (
ProjectiveLines CPS) & ex Y st y
= Y & x
in Y and
A2: for x,y be
object holds
[x, y]
in R2 iff x
in the
carrier of CPS & y
in (
ProjectiveLines CPS) & ex Y st y
= Y & x
in Y;
now
let x,y be
object;
A3:
now
assume
A4:
[x, y]
in R2;
then
A5: ex Y st y
= Y & x
in Y by
A2;
x
in the
carrier of CPS & y
in (
ProjectiveLines CPS) by
A2,
A4;
hence
[x, y]
in R1 by
A1,
A5;
end;
now
assume
A6:
[x, y]
in R1;
then
A7: ex Y st y
= Y & x
in Y by
A1;
x
in the
carrier of CPS & y
in (
ProjectiveLines CPS) by
A1,
A6;
hence
[x, y]
in R2 by
A2,
A7;
end;
hence
[x, y]
in R1 iff
[x, y]
in R2 by
A3;
end;
hence R1
= R2 by
RELAT_1:def 2;
end;
end
definition
let CPS;
::
INCPROJ:def3
func
IncProjSp_of (CPS) ->
IncProjStr equals
IncProjStr (# the
carrier of CPS, (
ProjectiveLines CPS), (
Proj_Inc CPS) #);
coherence ;
end
registration
let CPS;
cluster (
IncProjSp_of CPS) ->
strict;
coherence ;
end
theorem ::
INCPROJ:2
the
Points of (
IncProjSp_of CPS)
= the
carrier of CPS & the
Lines of (
IncProjSp_of CPS)
= (
ProjectiveLines CPS) & the
Inc of (
IncProjSp_of CPS)
= (
Proj_Inc CPS);
theorem ::
INCPROJ:3
x is
Point of CPS iff x is
POINT of (
IncProjSp_of CPS);
theorem ::
INCPROJ:4
x is
LINE of CPS iff x is
LINE of (
IncProjSp_of CPS) by
Th1;
reserve a,b,c,p,q for
POINT of (
IncProjSp_of CPS),
P,Q for
LINE of (
IncProjSp_of CPS),
a9,b9,c9,p9,q9,r9 for
Point of CPS,
P9 for
LINE of CPS;
theorem ::
INCPROJ:5
Th5: p
= p9 & P
= P9 implies (p
on P iff p9
in P9)
proof
reconsider P99 = P9 as
LINE of (
IncProjSp_of CPS) by
Th1;
reconsider P999 = P99 as
Element of (
ProjectiveLines CPS);
assume
A1: p
= p9 & P
= P9;
hereby
assume p
on P;
then
[p9, P9]
in (
Proj_Inc CPS) by
A1;
then ex Y st P9
= Y & p9
in Y by
Def2;
hence p9
in P9;
end;
assume p9
in P9;
then
[p9, P999]
in (
Proj_Inc CPS) by
Def2;
hence thesis by
A1;
end;
theorem ::
INCPROJ:6
Th6: ex a9, b9, c9 st a9
<> b9 & b9
<> c9 & c9
<> a9
proof
consider a99,b99,c99 be
Point of CPS such that
A1: not (a99,b99,c99)
are_collinear by
COLLSP:def 6;
A2: c99
<> a99 by
A1,
COLLSP: 2;
a99
<> b99 & b99
<> c99 by
A1,
COLLSP: 2;
hence thesis by
A2;
end;
theorem ::
INCPROJ:7
Th7: ex b9 st a9
<> b9
proof
consider p9, q9, r9 such that
A1: p9
<> q9 and q9
<> r9 and r9
<> p9 by
Th6;
a9
<> p9 or a9
<> q9 by
A1;
hence thesis;
end;
theorem ::
INCPROJ:8
Th8: p
on P & q
on P & p
on Q & q
on Q implies p
= q or P
= Q
proof
reconsider p9 = p, q9 = q as
Point of CPS;
reconsider P9 = P, Q9 = Q as
LINE of CPS by
Th1;
assume that
A1: p
on P & q
on P and
A2: p
on Q & q
on Q and
A3: p
<> q;
A4: p9
in Q9 & q9
in Q9 by
A2,
Th5;
p9
in P9 & q9
in P9 by
A1,
Th5;
hence thesis by
A3,
A4,
COLLSP: 20;
end;
theorem ::
INCPROJ:9
Th9: ex P st p
on P & q
on P
proof
reconsider p9 = p, q9 = q as
Point of CPS;
A1:
now
consider r9 such that
A2: p9
<> r9 by
Th7;
consider P9 be
LINE of CPS such that
A3: p9
in P9 and r9
in P9 by
A2,
COLLSP: 15;
reconsider P = P9 as
LINE of (
IncProjSp_of CPS) by
Th1;
assume
A4: p9
= q9;
p
on P by
A3,
Th5;
hence thesis by
A4;
end;
now
assume p9
<> q9;
then
consider P9 be
LINE of CPS such that
A5: p9
in P9 & q9
in P9 by
COLLSP: 15;
reconsider P = P9 as
LINE of (
IncProjSp_of CPS) by
Th1;
p
on P & q
on P by
A5,
Th5;
hence thesis;
end;
hence thesis by
A1;
end;
theorem ::
INCPROJ:10
Th10: a
= a9 & b
= b9 & c
= c9 implies ((a9,b9,c9)
are_collinear iff ex P st a
on P & b
on P & c
on P)
proof
assume that
A1: a
= a9 and
A2: b
= b9 and
A3: c
= c9;
hereby
assume
A4: (a9,b9,c9)
are_collinear ;
A5:
now
set X = (
Line (a9,b9));
assume a9
<> b9;
then
reconsider P9 = X as
LINE of CPS by
COLLSP:def 7;
reconsider P = P9 as
LINE of (
IncProjSp_of CPS) by
Th1;
a9
in X by
COLLSP: 10;
then
A6: a
on P by
A1,
Th5;
b9
in X by
COLLSP: 10;
then
A7: b
on P by
A2,
Th5;
c9
in X by
A4,
COLLSP: 11;
then c
on P by
A3,
Th5;
hence ex P st a
on P & b
on P & c
on P by
A6,
A7;
end;
now
assume
A8: a9
= b9;
ex P st b
on P & c
on P by
Th9;
hence ex P st a
on P & b
on P & c
on P by
A1,
A2,
A8;
end;
hence ex P st a
on P & b
on P & c
on P by
A5;
end;
given P such that
A9: a
on P & b
on P and
A10: c
on P;
reconsider P9 = P as
LINE of CPS by
Th1;
A11: c9
in P9 by
A3,
A10,
Th5;
a9
in P9 & b9
in P9 by
A1,
A2,
A9,
Th5;
hence thesis by
A11,
COLLSP: 16;
end;
theorem ::
INCPROJ:11
Th11: ex p, P st not p
on P
proof
consider p9, q9, r9 such that
A1: not (p9,q9,r9)
are_collinear by
COLLSP:def 6;
set X = (
Line (p9,q9));
p9
<> q9 by
A1,
COLLSP: 2;
then
reconsider P9 = X as
LINE of CPS by
COLLSP:def 7;
reconsider P = P9 as
LINE of (
IncProjSp_of CPS) by
Th1;
reconsider r = r9 as
POINT of (
IncProjSp_of CPS);
not r
on P
proof
assume not thesis;
then r9
in X by
Th5;
hence contradiction by
A1,
COLLSP: 11;
end;
hence thesis;
end;
reserve CPS for
CollProjectiveSpace,
a,b,c,d,p,q for
POINT of (
IncProjSp_of CPS),
P,Q,S,M,N for
LINE of (
IncProjSp_of CPS),
a9,b9,c9,d9,p9,q9 for
Point of CPS;
theorem ::
INCPROJ:12
Th12: ex a, b, c st a
<> b & b
<> c & c
<> a & a
on P & b
on P & c
on P
proof
reconsider P9 = P as
LINE of CPS by
Th1;
consider a99,b99 be
Point of CPS such that
A1: a99
<> b99 and
A2: P9
= (
Line (a99,b99)) by
COLLSP:def 7;
consider c9 such that
A3: a99
<> c9 & b99
<> c9 and
A4: (a99,b99,c9)
are_collinear by
ANPROJ_2:def 10;
reconsider a = a99, b = b99, c = c9 as
POINT of (
IncProjSp_of CPS);
take a, b, c;
thus a
<> b & b
<> c & c
<> a by
A1,
A3;
a99
in P9 by
A2,
COLLSP: 10;
then
A5: a
on P by
Th5;
b99
in P9 by
A2,
COLLSP: 10;
then
A6: b
on P by
Th5;
ex Q st a
on Q & b
on Q & c
on Q by
A4,
Th10;
hence thesis by
A1,
A5,
A6,
Th8;
end;
theorem ::
INCPROJ:13
Th13: a
on M & b
on M & c
on N & d
on N & p
on M & p
on N & a
on P & c
on P & b
on Q & d
on Q & not p
on P & not p
on Q & M
<> N implies ex q st q
on P & q
on Q
proof
assume that
A1: a
on M and
A2: b
on M and
A3: c
on N and
A4: d
on N and
A5: p
on M & p
on N and
A6: a
on P and
A7: c
on P and
A8: b
on Q and
A9: d
on Q and
A10: not p
on P and
A11: not p
on Q and
A12: M
<> N;
reconsider a9 = a, b9 = b, c9 = c, d9 = d, p9 = p as
Point of CPS;
(b9,p9,a9)
are_collinear & (p9,d9,c9)
are_collinear by
A1,
A2,
A3,
A4,
A5,
Th10;
then
consider q9 such that
A13: (b9,d9,q9)
are_collinear and
A14: (a9,c9,q9)
are_collinear by
ANPROJ_2:def 9;
reconsider q = q9 as
POINT of (
IncProjSp_of CPS);
A15: ex P2 be
LINE of (
IncProjSp_of CPS) st b
on P2 & d
on P2 & q
on P2 by
A13,
Th10;
b
<> d by
A2,
A4,
A5,
A8,
A11,
A12,
Th8;
then
A16: q
on Q by
A8,
A9,
A15,
Th8;
A17: ex P1 be
LINE of (
IncProjSp_of CPS) st a
on P1 & c
on P1 & q
on P1 by
A14,
Th10;
a
<> c by
A1,
A3,
A5,
A6,
A10,
A12,
Th8;
then q
on P by
A6,
A7,
A17,
Th8;
hence thesis by
A16;
end;
theorem ::
INCPROJ:14
Th14: (for a9, b9, c9, d9 holds ex p9 st (a9,b9,p9)
are_collinear & (c9,d9,p9)
are_collinear ) implies for M, N holds ex q st q
on M & q
on N
proof
assume
A1: for a9, b9, c9, d9 holds ex p9 st (a9,b9,p9)
are_collinear & (c9,d9,p9)
are_collinear ;
let M, N;
reconsider M9 = M, N9 = N as
LINE of CPS by
Th1;
consider a9, b9 such that a9
<> b9 and
A2: M9
= (
Line (a9,b9)) by
COLLSP:def 7;
consider c9, d9 such that c9
<> d9 and
A3: N9
= (
Line (c9,d9)) by
COLLSP:def 7;
consider p9 such that
A4: (a9,b9,p9)
are_collinear and
A5: (c9,d9,p9)
are_collinear by
A1;
reconsider q = p9 as
POINT of (
IncProjSp_of CPS);
p9
in N9 by
A3,
A5,
COLLSP: 11;
then
A6: q
on N by
Th5;
p9
in M9 by
A2,
A4,
COLLSP: 11;
then q
on M by
Th5;
hence thesis by
A6;
end;
theorem ::
INCPROJ:15
Th15: (ex p,p1,r,r1 be
Point of CPS st not ex s be
Point of CPS st ((p,p1,s)
are_collinear & (r,r1,s)
are_collinear )) implies ex M, N st not ex q st q
on M & q
on N
proof
given p,p1,r,r1 be
Point of CPS such that
A1: not ex s be
Point of CPS st ((p,p1,s)
are_collinear & (r,r1,s)
are_collinear );
set M99 = (
Line (p,p1)), N99 = (
Line (r,r1));
p
<> p1 & r
<> r1
proof
A2:
now
assume p
= p1;
then
A3: (p,p1,r1)
are_collinear by
COLLSP: 2;
(r,r1,r1)
are_collinear by
COLLSP: 2;
hence contradiction by
A1,
A3;
end;
A4:
now
assume r
= r1;
then (p,p1,p1)
are_collinear & (r,r1,p1)
are_collinear by
COLLSP: 2;
hence contradiction by
A1;
end;
assume not thesis;
hence contradiction by
A2,
A4;
end;
then
reconsider M9 = M99, N9 = N99 as
LINE of CPS by
COLLSP:def 7;
reconsider M = M9, N = N9 as
LINE of (
IncProjSp_of CPS) by
Th1;
take M, N;
thus not ex q st q
on M & q
on N
proof
assume not thesis;
then
consider q such that
A5: q
on M and
A6: q
on N;
reconsider q9 = q as
Point of CPS;
q9
in N99 by
A6,
Th5;
then
A7: (r,r1,q9)
are_collinear by
COLLSP: 11;
q9
in M99 by
A5,
Th5;
then (p,p1,q9)
are_collinear by
COLLSP: 11;
hence contradiction by
A1,
A7;
end;
end;
theorem ::
INCPROJ:16
Th16: (for p,p1,q,q1,r2 be
Point of CPS holds ex r,r1 be
Point of CPS st (p,q,r)
are_collinear & (p1,q1,r1)
are_collinear & (r2,r,r1)
are_collinear ) implies for a, M, N holds ex b, c, S st a
on S & b
on S & c
on S & b
on M & c
on N
proof
assume
A1: for p,p1,q,q1,r2 be
Point of CPS holds ex r,r1 be
Point of CPS st (p,q,r)
are_collinear & (p1,q1,r1)
are_collinear & (r2,r,r1)
are_collinear ;
let a, M, N;
reconsider M9 = M, N9 = N as
LINE of CPS by
Th1;
reconsider a9 = a as
Point of CPS;
consider p,q be
Point of CPS such that p
<> q and
A2: M9
= (
Line (p,q)) by
COLLSP:def 7;
consider p1,q1 be
Point of CPS such that p1
<> q1 and
A3: N9
= (
Line (p1,q1)) by
COLLSP:def 7;
consider b9, c9 such that
A4: (p,q,b9)
are_collinear and
A5: (p1,q1,c9)
are_collinear and
A6: (a9,b9,c9)
are_collinear by
A1;
reconsider b = b9, c = c9 as
POINT of (
IncProjSp_of CPS);
b9
in M9 by
A2,
A4,
COLLSP: 11;
then
A7: b
on M by
Th5;
c9
in N9 by
A3,
A5,
COLLSP: 11;
then
A8: c
on N by
Th5;
ex S st a
on S & b
on S & c
on S by
A6,
Th10;
hence thesis by
A7,
A8;
end;
theorem ::
INCPROJ:17
Th17: (for p1,r2,q,r1,q1,p,r be
Point of CPS holds ((p1,r2,q)
are_collinear & (r1,q1,q)
are_collinear & (p1,r1,p)
are_collinear & (r2,q1,p)
are_collinear & (p1,q1,r)
are_collinear & (r2,r1,r)
are_collinear & (p,q,r)
are_collinear implies ((p1,r2,q1)
are_collinear or (p1,r2,r1)
are_collinear or (p1,r1,q1)
are_collinear or (r2,r1,q1)
are_collinear ))) implies for p,q,r,s,a,b,c be
POINT of (
IncProjSp_of CPS) holds for L,Q,R,S,A,B,C be
LINE of (
IncProjSp_of CPS) 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 &
{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 holds not c
on C
proof
assume
A1: for p1,r2,q,r1,q1,p,r be
Element of CPS holds ((p1,r2,q)
are_collinear & (r1,q1,q)
are_collinear & (p1,r1,p)
are_collinear & (r2,q1,p)
are_collinear & (p1,q1,r)
are_collinear & (r2,r1,r)
are_collinear & (p,q,r)
are_collinear implies ((p1,r2,q1)
are_collinear or (p1,r2,r1)
are_collinear or (p1,r1,q1)
are_collinear or (r2,r1,q1)
are_collinear ));
let p,q,r,s,a,b,c be
POINT of (
IncProjSp_of CPS);
let L,Q,R,S,A,B,C be
LINE of (
IncProjSp_of CPS) such that
A2: not q
on L and
A3: not r
on L and
A4: not p
on Q and
A5: not s
on Q and
A6: not p
on R and
A7: not r
on R and
A8:
{a, p, s}
on L and
A9:
{a, q, r}
on Q and
A10:
{b, q, s}
on R and
A11:
{b, p, r}
on S and
A12:
{c, p, q}
on A and
A13:
{c, r, s}
on B and
A14:
{a, b}
on C;
reconsider p9 = p, q9 = q, r9 = r, s9 = s, a9 = a, b9 = b, c9 = c as
Point of CPS;
A15: p
on L & s
on L by
A8,
INCSP_1: 2;
A16: s
on R by
A10,
INCSP_1: 2;
A17:
now
assume (p9,r9,s9)
are_collinear ;
then
A18: ex K be
LINE of (
IncProjSp_of CPS) st p
on K & r
on K & s
on K by
Th10;
hence s
on S by
A3,
A6,
A15,
A16,
Th8;
thus contradiction by
A3,
A6,
A15,
A16,
A18,
Th8;
end;
A19:
now
assume (p9,s9,q9)
are_collinear ;
then
A20: ex K be
LINE of (
IncProjSp_of CPS) st p
on K & s
on K & q
on K by
Th10;
hence p
on R by
A2,
A15,
A16,
Th8;
thus contradiction by
A2,
A6,
A15,
A16,
A20,
Th8;
end;
a
on L by
A8,
INCSP_1: 2;
then
A21: (p9,s9,a9)
are_collinear by
A15,
Th10;
assume
A22: not thesis;
a
on C & b
on C by
A14,
INCSP_1: 1;
then
A23: (a9,b9,c9)
are_collinear by
A22,
Th10;
A24: q
on Q & r
on Q by
A9,
INCSP_1: 2;
A25: q
on R by
A10,
INCSP_1: 2;
A26:
now
assume (p9,r9,q9)
are_collinear ;
then
A27: ex K be
LINE of (
IncProjSp_of CPS) st p
on K & r
on K & q
on K by
Th10;
hence q
on S by
A4,
A7,
A24,
A25,
Th8;
thus contradiction by
A4,
A7,
A24,
A25,
A27,
Th8;
end;
A28:
now
assume (r9,s9,q9)
are_collinear ;
then
A29: ex K be
LINE of (
IncProjSp_of CPS) st r
on K & s
on K & q
on K by
Th10;
hence r
on R by
A5,
A24,
A25,
Th8;
thus contradiction by
A5,
A7,
A24,
A25,
A29,
Th8;
end;
a
on Q by
A9,
INCSP_1: 2;
then
A30: (r9,q9,a9)
are_collinear by
A24,
Th10;
A31: r
on S by
A11,
INCSP_1: 2;
b
on S & p
on S by
A11,
INCSP_1: 2;
then
A32: (p9,r9,b9)
are_collinear by
A31,
Th10;
A33: s
on B by
A13,
INCSP_1: 2;
c
on B & r
on B by
A13,
INCSP_1: 2;
then
A34: (r9,s9,c9)
are_collinear by
A33,
Th10;
A35: q
on A by
A12,
INCSP_1: 2;
c
on A & p
on A by
A12,
INCSP_1: 2;
then
A36: (p9,q9,c9)
are_collinear by
A35,
Th10;
b
on R by
A10,
INCSP_1: 2;
then (s9,q9,b9)
are_collinear by
A25,
A16,
Th10;
hence contradiction by
A1,
A23,
A32,
A21,
A30,
A36,
A34,
A26,
A17,
A19,
A28;
end;
theorem ::
INCPROJ:18
Th18: (for o,p1,p2,p3,q1,q2,q3,r1,r2,r3 be
Point of CPS st o
<> q1 & p1
<> q1 & o
<> q2 & p2
<> q2 & o
<> q3 & p3
<> q3 & not (o,p1,p2)
are_collinear & not (o,p1,p3)
are_collinear & not (o,p2,p3)
are_collinear & (p1,p2,r3)
are_collinear & (q1,q2,r3)
are_collinear & (p2,p3,r1)
are_collinear & (q2,q3,r1)
are_collinear & (p1,p3,r2)
are_collinear & (q1,q3,r2)
are_collinear & (o,p1,q1)
are_collinear & (o,p2,q2)
are_collinear & (o,p3,q3)
are_collinear holds (r1,r2,r3)
are_collinear ) implies for o,b1,a1,b2,a2,b3,a3,r,s,t be
POINT of (
IncProjSp_of CPS) holds for C1,C2,C3,A1,A2,A3,B1,B2,B3 be
LINE of (
IncProjSp_of CPS) 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
<> a1 & o
<> a2 & o
<> a3 & o
<> b1 & o
<> b2 & o
<> b3 & a1
<> b1 & a2
<> b2 & a3
<> b3 holds ex O be
LINE of (
IncProjSp_of CPS) st
{r, s, t}
on O
proof
assume
A1: for o,p1,p2,p3,q1,q2,q3,r1,r2,r3 be
Element of CPS st o
<> q1 & p1
<> q1 & o
<> q2 & p2
<> q2 & o
<> q3 & p3
<> q3 & not (o,p1,p2)
are_collinear & not (o,p1,p3)
are_collinear & not (o,p2,p3)
are_collinear & (p1,p2,r3)
are_collinear & (q1,q2,r3)
are_collinear & (p2,p3,r1)
are_collinear & (q2,q3,r1)
are_collinear & (p1,p3,r2)
are_collinear & (q1,q3,r2)
are_collinear & (o,p1,q1)
are_collinear & (o,p2,q2)
are_collinear & (o,p3,q3)
are_collinear holds (r1,r2,r3)
are_collinear ;
let o,b1,a1,b2,a2,b3,a3,r,s,t be
POINT of (
IncProjSp_of CPS);
let C1,C2,C3,A1,A2,A3,B1,B2,B3 be
LINE of (
IncProjSp_of CPS) such that
A2:
{o, b1, a1}
on C1 and
A3:
{o, a2, b2}
on C2 and
A4:
{o, a3, b3}
on C3 and
A5:
{a3, a2, t}
on A1 and
A6:
{a3, r, a1}
on A2 and
A7:
{a2, s, a1}
on A3 and
A8:
{t, b2, b3}
on B1 and
A9:
{b1, r, b3}
on B2 and
A10:
{b1, s, b2}
on B3 and
A11: (C1,C2,C3)
are_mutually_distinct and
A12: o
<> a1 & o
<> a2 & o
<> a3 and
A13: o
<> b1 and
A14: o
<> b2 and
A15: o
<> b3 and
A16: a1
<> b1 & a2
<> b2 & a3
<> b3;
reconsider o9 = o, b19 = b1, a19 = a1, b29 = b2, a29 = a2, b39 = b3, a39 = a3, r9 = r, s9 = s, t9 = t as
Element of CPS;
A17: o
on C2 & b2
on C2 by
A3,
INCSP_1: 2;
A18: s
on B3 by
A10,
INCSP_1: 2;
b2
on B3 & b1
on B3 by
A10,
INCSP_1: 2;
then
A19: (b19,b29,s9)
are_collinear by
A18,
Th10;
A20: r
on B2 by
A9,
INCSP_1: 2;
b3
on B2 & b1
on B2 by
A9,
INCSP_1: 2;
then
A21: (b19,b39,r9)
are_collinear by
A20,
Th10;
A22: t
on B1 by
A8,
INCSP_1: 2;
b3
on B1 & b2
on B1 by
A8,
INCSP_1: 2;
then
A23: (b29,b39,t9)
are_collinear by
A22,
Th10;
A24: s
on A3 by
A7,
INCSP_1: 2;
a2
on A3 & a1
on A3 by
A7,
INCSP_1: 2;
then
A25: (a19,a29,s9)
are_collinear by
A24,
Th10;
A26: o
on C3 & b3
on C3 by
A4,
INCSP_1: 2;
a3
on C3 by
A4,
INCSP_1: 2;
then
A27: (o9,b39,a39)
are_collinear by
A26,
Th10;
a2
on C2 by
A3,
INCSP_1: 2;
then
A28: (o9,b29,a29)
are_collinear by
A17,
Th10;
A29: r
on A2 by
A6,
INCSP_1: 2;
a3
on A2 & a1
on A2 by
A6,
INCSP_1: 2;
then
A30: (a19,a39,r9)
are_collinear by
A29,
Th10;
A31: t
on A1 by
A5,
INCSP_1: 2;
a3
on A1 & a2
on A1 by
A5,
INCSP_1: 2;
then
A32: (a29,a39,t9)
are_collinear by
A31,
Th10;
A33: o
on C1 & b1
on C1 by
A2,
INCSP_1: 2;
A34: not (o9,b19,b29)
are_collinear & not (o9,b19,b39)
are_collinear & not (o9,b29,b39)
are_collinear
proof
A35:
now
assume (o9,b19,b39)
are_collinear ;
then
consider K be
LINE of (
IncProjSp_of CPS) such that
A36: o
on K & b1
on K & b3
on K by
Th10;
K
= C1 & K
= C3 by
A13,
A15,
A33,
A26,
A36,
Th8;
hence contradiction by
A11,
ZFMISC_1:def 5;
end;
A37:
now
assume (o9,b19,b29)
are_collinear ;
then
consider K be
LINE of (
IncProjSp_of CPS) such that
A38: o
on K & b1
on K & b2
on K by
Th10;
K
= C1 & K
= C2 by
A13,
A14,
A33,
A17,
A38,
Th8;
hence contradiction by
A11,
ZFMISC_1:def 5;
end;
A39:
now
assume (o9,b29,b39)
are_collinear ;
then
consider K be
LINE of (
IncProjSp_of CPS) such that
A40: o
on K & b2
on K & b3
on K by
Th10;
K
= C2 & K
= C3 by
A14,
A15,
A17,
A26,
A40,
Th8;
hence contradiction by
A11,
ZFMISC_1:def 5;
end;
assume not thesis;
hence contradiction by
A37,
A35,
A39;
end;
a1
on C1 by
A2,
INCSP_1: 2;
then (o9,b19,a19)
are_collinear by
A33,
Th10;
then (t9,r9,s9)
are_collinear by
A1,
A12,
A16,
A19,
A25,
A21,
A30,
A23,
A32,
A28,
A27,
A34;
then
consider O be
LINE of (
IncProjSp_of CPS) such that
A41: t
on O & r
on O & s
on O by
Th10;
{r, s, t}
on O by
A41,
INCSP_1: 2;
hence thesis;
end;
theorem ::
INCPROJ:19
Th19: (for o,p1,p2,p3,q1,q2,q3,r1,r2,r3 be
Point of CPS st o
<> p2 & o
<> p3 & p2
<> p3 & p1
<> p2 & p1
<> p3 & o
<> q2 & o
<> q3 & q2
<> q3 & q1
<> q2 & q1
<> q3 & not (o,p1,q1)
are_collinear & (o,p1,p2)
are_collinear & (o,p1,p3)
are_collinear & (o,q1,q2)
are_collinear & (o,q1,q3)
are_collinear & (p1,q2,r3)
are_collinear & (q1,p2,r3)
are_collinear & (p1,q3,r2)
are_collinear & (p3,q1,r2)
are_collinear & (p2,q3,r1)
are_collinear & (p3,q2,r1)
are_collinear holds (r1,r2,r3)
are_collinear ) implies for o,a1,a2,a3,b1,b2,b3,c1,c2,c3 be
POINT of (
IncProjSp_of CPS) holds for A1,A2,A3,B1,B2,B3,C1,C2,C3 be
LINE of (
IncProjSp_of CPS) st (o,a1,a2,a3)
are_mutually_distinct & (o,b1,b2,b3)
are_mutually_distinct & A3
<> B3 & o
on A3 & o
on B3 &
{a2, b3, c1}
on A1 &
{a3, b1, c2}
on B1 &
{a1, b2, c3}
on C1 &
{a1, b3, c2}
on A2 &
{a3, b2, c1}
on B2 &
{a2, b1, c3}
on C2 &
{b1, b2, b3}
on A3 &
{a1, a2, a3}
on B3 &
{c1, c2}
on C3 holds c3
on C3
proof
assume
A1: for o,p1,p2,p3,q1,q2,q3,r1,r2,r3 be
Point of CPS st o
<> p2 & o
<> p3 & p2
<> p3 & p1
<> p2 & p1
<> p3 & o
<> q2 & o
<> q3 & q2
<> q3 & q1
<> q2 & q1
<> q3 & not (o,p1,q1)
are_collinear & (o,p1,p2)
are_collinear & (o,p1,p3)
are_collinear & (o,q1,q2)
are_collinear & (o,q1,q3)
are_collinear & (p1,q2,r3)
are_collinear & (q1,p2,r3)
are_collinear & (p1,q3,r2)
are_collinear & (p3,q1,r2)
are_collinear & (p2,q3,r1)
are_collinear & (p3,q2,r1)
are_collinear holds (r1,r2,r3)
are_collinear ;
let o,a1,a2,a3,b1,b2,b3,c1,c2,c3 be
POINT of (
IncProjSp_of CPS);
let A1,A2,A3,B1,B2,B3,C1,C2,C3 be
LINE of (
IncProjSp_of CPS) such that
A2: (o,a1,a2,a3)
are_mutually_distinct and
A3: (o,b1,b2,b3)
are_mutually_distinct and
A4: A3
<> B3 and
A5: o
on A3 and
A6: o
on B3 and
A7:
{a2, b3, c1}
on A1 and
A8:
{a3, b1, c2}
on B1 and
A9:
{a1, b2, c3}
on C1 and
A10:
{a1, b3, c2}
on A2 and
A11:
{a3, b2, c1}
on B2 and
A12:
{a2, b1, c3}
on C2 and
A13:
{b1, b2, b3}
on A3 and
A14:
{a1, a2, a3}
on B3 and
A15:
{c1, c2}
on C3;
reconsider o9 = o, a19 = a1, a29 = a2, a39 = a3, b19 = b1, b29 = b2, b39 = b3, c19 = c1, c29 = c2, c39 = c3 as
Point of CPS;
A16: b1
on A3 by
A13,
INCSP_1: 2;
A17: c3
on C1 by
A9,
INCSP_1: 2;
a1
on C1 & b2
on C1 by
A9,
INCSP_1: 2;
then
A18: (a19,b29,c39)
are_collinear by
A17,
Th10;
A19: c1
on A1 by
A7,
INCSP_1: 2;
A20: o9
<> b39 & b29
<> b39 by
A3,
ZFMISC_1:def 6;
A21: a29
<> a39 & a19
<> a29 by
A2,
ZFMISC_1:def 6;
A22: b3
on A2 & c2
on A2 by
A10,
INCSP_1: 2;
A23: a1
on A2 by
A10,
INCSP_1: 2;
then
A24: (a19,b39,c29)
are_collinear by
A22,
Th10;
A25: b19
<> b29 & b19
<> b39 by
A3,
ZFMISC_1:def 6;
A26: b3
on A1 by
A7,
INCSP_1: 2;
A27: a1
on B3 by
A14,
INCSP_1: 2;
A28: not (o9,a19,b19)
are_collinear
proof
A29: o
<> a1 by
A2,
ZFMISC_1:def 6;
assume not thesis;
then
consider K be
LINE of (
IncProjSp_of CPS) such that
A30: o
on K and
A31: a1
on K and
A32: b1
on K by
Th10;
o
<> b1 by
A3,
ZFMISC_1:def 6;
then K
= A3 by
A5,
A16,
A30,
A32,
Th8;
hence contradiction by
A4,
A6,
A27,
A30,
A31,
A29,
Th8;
end;
A33: c3
on C2 by
A12,
INCSP_1: 2;
a2
on C2 & b1
on C2 by
A12,
INCSP_1: 2;
then
A34: (b19,a29,c39)
are_collinear by
A33,
Th10;
A35: a3
on B1 by
A8,
INCSP_1: 2;
A36: b2
on A3 by
A13,
INCSP_1: 2;
then
A37: (o9,b19,b29)
are_collinear by
A5,
A16,
Th10;
A38: a3
on B2 & c1
on B2 by
A11,
INCSP_1: 2;
A39: b2
on B2 by
A11,
INCSP_1: 2;
then
A40: (a39,b29,c19)
are_collinear by
A38,
Th10;
A41: b3
on A3 by
A13,
INCSP_1: 2;
then
A42: (o9,b19,b39)
are_collinear by
A5,
A16,
Th10;
A43: a19
<> a39 & o9
<> b29 by
A2,
A3,
ZFMISC_1:def 6;
A44: o9
<> a29 & o9
<> a39 by
A2,
ZFMISC_1:def 6;
A45: c2
on B1 by
A8,
INCSP_1: 2;
A46: a2
on A1 by
A7,
INCSP_1: 2;
then
A47: (a29,b39,c19)
are_collinear by
A26,
A19,
Th10;
A48: b1
<> b2 by
A3,
ZFMISC_1:def 6;
A49: a1
<> a2 by
A2,
ZFMISC_1:def 6;
A50: o
<> b3 by
A3,
ZFMISC_1:def 6;
A51: b1
on B1 by
A8,
INCSP_1: 2;
then
A52: (a39,b19,c29)
are_collinear by
A35,
A45,
Th10;
A53: a3
on B3 by
A14,
INCSP_1: 2;
then
A54: (o9,a19,a39)
are_collinear by
A6,
A27,
Th10;
A55: a2
on B3 by
A14,
INCSP_1: 2;
then (o9,a19,a29)
are_collinear by
A6,
A27,
Th10;
then (c19,c29,c39)
are_collinear by
A1,
A44,
A21,
A43,
A20,
A25,
A28,
A54,
A37,
A42,
A18,
A34,
A24,
A52,
A47,
A40;
then
A56: ex K be
LINE of (
IncProjSp_of CPS) st c1
on K & c2
on K & c3
on K by
Th10;
A57: o
<> a3 by
A2,
ZFMISC_1:def 6;
A58: c1
<> c2
proof
assume
A59: not thesis;
not a3
on A3 by
A4,
A5,
A6,
A57,
A53,
Th8;
then B1
<> B2 by
A48,
A35,
A51,
A39,
A16,
A36,
Th8;
then
A60: c1
= a3 by
A35,
A45,
A38,
A59,
Th8;
not b3
on B3 by
A4,
A5,
A6,
A50,
A41,
Th8;
then A1
<> A2 by
A49,
A46,
A26,
A23,
A27,
A55,
Th8;
then c1
= b3 by
A26,
A19,
A22,
A59,
Th8;
hence contradiction by
A4,
A5,
A6,
A50,
A41,
A53,
A60,
Th8;
end;
c1
on C3 & c2
on C3 by
A15,
INCSP_1: 1;
hence thesis by
A58,
A56,
Th8;
end;
definition
let S be
IncProjStr;
::
INCPROJ:def4
attr S is
partial means for p,q be
POINT of S, P,Q be
LINE of S st p
on P & q
on P & p
on Q & q
on Q holds p
= q or P
= Q;
:: original:
linear
redefine
::
INCPROJ:def5
attr S is
linear means for p,q be
POINT of S holds ex P be
LINE of S st p
on P & q
on P;
compatibility
proof
hereby
assume
A1: S is
linear;
let p,q be
POINT of S;
consider P be
LINE of S such that
A2:
{p, q}
on P by
A1;
take P;
thus p
on P & q
on P by
A2,
INCSP_1: 1;
end;
assume
A3: for p,q be
POINT of S holds ex P be
LINE of S st p
on P & q
on P;
let p,q be
POINT of S;
consider L be
LINE of S such that
A4: p
on L & q
on L by
A3;
{p, q}
on L by
A4,
INCSP_1: 1;
hence thesis;
end;
end
definition
let S be
IncProjStr;
::
INCPROJ:def6
attr S is
up-2-dimensional means ex p be
POINT of S, P be
LINE of S st not p
on P;
::
INCPROJ:def7
attr S is
up-3-rank means for P be
LINE of S holds ex a,b,c be
POINT of S st a
<> b & b
<> c & c
<> a & a
on P & b
on P & c
on P;
::
INCPROJ:def8
attr S is
Vebleian means for a,b,c,d,p,q be
POINT of S holds for M,N,P,Q be
LINE of S st a
on M & b
on M & c
on N & d
on N & p
on M & p
on N & a
on P & c
on P & b
on Q & d
on Q & not p
on P & not p
on Q & M
<> N holds ex q be
POINT of S st q
on P & q
on Q;
end
registration
let CPS be
CollProjectiveSpace;
cluster (
IncProjSp_of CPS) ->
partial
linear
up-2-dimensional
up-3-rank
Vebleian;
coherence by
Th13,
Th11,
Th12,
Th8,
Th9;
end
registration
cluster
strict
partial
linear
up-2-dimensional
up-3-rank
Vebleian for
IncProjStr;
existence
proof
set CPS = the
CollProjectiveSpace;
(
IncProjSp_of CPS) is
strict
partial
linear
up-2-dimensional
up-3-rank
Vebleian;
hence thesis;
end;
end
definition
mode
IncProjSp is
partial
linear
up-2-dimensional
up-3-rank
Vebleian
IncProjStr;
end
registration
let CPS be
CollProjectiveSpace;
cluster (
IncProjSp_of CPS) ->
partial
linear
up-2-dimensional
up-3-rank
Vebleian;
coherence ;
end
definition
let IT be
IncProjSp;
::
INCPROJ:def9
attr IT is
2-dimensional means for M,N be
LINE of IT holds ex q be
POINT of IT st q
on M & q
on N;
end
notation
let IT be
IncProjSp;
antonym IT is
up-3-dimensional for IT is
2-dimensional;
end
definition
let IT be
IncProjStr;
::
INCPROJ:def10
attr IT is
at_most-3-dimensional means for a be
POINT of IT, M,N be
LINE of IT holds ex b,c be
POINT of IT, S be
LINE of IT st a
on S & b
on S & c
on S & b
on M & c
on N;
end
definition
let IT be
IncProjSp;
::
INCPROJ:def11
attr IT is
3-dimensional means IT is
at_most-3-dimensional
up-3-dimensional;
end
definition
let IT be
IncProjStr;
::
INCPROJ:def12
attr IT is
Fanoian means for p,q,r,s,a,b,c be
POINT of IT holds for L,Q,R,S,A,B,C be
LINE of IT 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 holds not c
on C;
end
definition
let IT be
IncProjStr;
::
INCPROJ:def13
attr IT is
Desarguesian means for o,b1,a1,b2,a2,b3,a3,r,s,t be
POINT of IT holds for C1,C2,C3,A1,A2,A3,B1,B2,B3 be
LINE of IT 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
<> a1 & o
<> a2 & o
<> a3 & o
<> b1 & o
<> b2 & o
<> b3 & a1
<> b1 & a2
<> b2 & a3
<> b3 holds ex O be
LINE of IT st
{r, s, t}
on O;
end
definition
let IT be
IncProjStr;
::
INCPROJ:def14
attr IT is
Pappian means for o,a1,a2,a3,b1,b2,b3,c1,c2,c3 be
POINT of IT holds for A1,A2,A3,B1,B2,B3,C1,C2,C3 be
LINE of IT st (o,a1,a2,a3)
are_mutually_distinct & (o,b1,b2,b3)
are_mutually_distinct & A3
<> B3 & o
on A3 & o
on B3 &
{a2, b3, c1}
on A1 &
{a3, b1, c2}
on B1 &
{a1, b2, c3}
on C1 &
{a1, b3, c2}
on A2 &
{a3, b2, c1}
on B2 &
{a2, b1, c3}
on C2 &
{b1, b2, b3}
on A3 &
{a1, a2, a3}
on B3 &
{c1, c2}
on C3 holds c3
on C3;
end
registration
cluster
Desarguesian
Fanoian
at_most-3-dimensional
up-3-dimensional for
IncProjSp;
existence
proof
set CPS = the
Fanoian
Desarguesian
at_most-3-dimensional
up-3-dimensional
CollProjectiveSpace;
reconsider CPS9 = CPS as
CollProjectiveSpace;
take X = (
IncProjSp_of CPS9);
for o,p1,p2,p3,q1,q2,q3,r1,r2,r3 be
Point of CPS9 st o
<> q1 & p1
<> q1 & o
<> q2 & p2
<> q2 & o
<> q3 & p3
<> q3 & not (o,p1,p2)
are_collinear & not (o,p1,p3)
are_collinear & not (o,p2,p3)
are_collinear & (p1,p2,r3)
are_collinear & (q1,q2,r3)
are_collinear & (p2,p3,r1)
are_collinear & (q2,q3,r1)
are_collinear & (p1,p3,r2)
are_collinear & (q1,q3,r2)
are_collinear & (o,p1,q1)
are_collinear & (o,p2,q2)
are_collinear & (o,p3,q3)
are_collinear holds (r1,r2,r3)
are_collinear by
ANPROJ_2:def 12;
then
A1: for o,b1,a1,b2,a2,b3,a3,r,s,t be
POINT of X holds for C1,C2,C3,A1,A2,A3,B1,B2,B3 be
LINE of X 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
<> a1 & o
<> a2 & o
<> a3 & o
<> b1 & o
<> b2 & o
<> b3 & a1
<> b1 & a2
<> b2 & a3
<> b3 holds ex O be
LINE of X st
{r, s, t}
on O by
Th18;
ex p,p1,r,r1 be
Point of CPS9 st not ex s be
Point of CPS9 st ((p,p1,s)
are_collinear & (r,r1,s)
are_collinear ) by
ANPROJ_2:def 14;
then
A2: ex M,N be
LINE of X st not ex q be
POINT of X st q
on M & q
on N by
Th15;
for p,p1,q,q1,r2 be
Point of CPS9 holds ex r,r1 be
Point of CPS9 st (p,q,r)
are_collinear & (p1,q1,r1)
are_collinear & (r2,r,r1)
are_collinear by
ANPROJ_2:def 15;
then
A3: for a be
POINT of X, M,N be
LINE of X holds ex b,c be
POINT of X, S be
LINE of X st a
on S & b
on S & c
on S & b
on M & c
on N by
Th16;
for p1,r2,q,r1,q1,p,r be
Point of CPS9 holds ((p1,r2,q)
are_collinear & (r1,q1,q)
are_collinear & (p1,r1,p)
are_collinear & (r2,q1,p)
are_collinear & (p1,q1,r)
are_collinear & (r2,r1,r)
are_collinear & (p,q,r)
are_collinear implies ((p1,r2,q1)
are_collinear or (p1,r2,r1)
are_collinear or (p1,r1,q1)
are_collinear or (r2,r1,q1)
are_collinear )) by
ANPROJ_2:def 11;
then for p,q,r,s,a,b,c be
POINT of X holds for L,Q,R,S,A,B,C be
LINE of X 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 holds not c
on C by
Th17;
hence thesis by
A1,
A2,
A3;
end;
end
registration
cluster
Pappian
Fanoian
at_most-3-dimensional
up-3-dimensional for
IncProjSp;
existence
proof
set CPS = the
Fanoian
Pappian
at_most-3-dimensional
up-3-dimensional
CollProjectiveSpace;
reconsider CPS9 = CPS as
CollProjectiveSpace;
take X = (
IncProjSp_of CPS9);
for o,p1,p2,p3,q1,q2,q3,r1,r2,r3 be
Point of CPS9 st o
<> p2 & o
<> p3 & p2
<> p3 & p1
<> p2 & p1
<> p3 & o
<> q2 & o
<> q3 & q2
<> q3 & q1
<> q2 & q1
<> q3 & not (o,p1,q1)
are_collinear & (o,p1,p2)
are_collinear & (o,p1,p3)
are_collinear & (o,q1,q2)
are_collinear & (o,q1,q3)
are_collinear & (p1,q2,r3)
are_collinear & (q1,p2,r3)
are_collinear & (p1,q3,r2)
are_collinear & (p3,q1,r2)
are_collinear & (p2,q3,r1)
are_collinear & (p3,q2,r1)
are_collinear holds (r1,r2,r3)
are_collinear by
ANPROJ_2:def 13;
then
A1: for o,a1,a2,a3,b1,b2,b3,c1,c2,c3 be
POINT of X holds for A1,A2,A3,B1,B2,B3,C1,C2,C3 be
LINE of X st (o,a1,a2,a3)
are_mutually_distinct & (o,b1,b2,b3)
are_mutually_distinct & A3
<> B3 & o
on A3 & o
on B3 &
{a2, b3, c1}
on A1 &
{a3, b1, c2}
on B1 &
{a1, b2, c3}
on C1 &
{a1, b3, c2}
on A2 &
{a3, b2, c1}
on B2 &
{a2, b1, c3}
on C2 &
{b1, b2, b3}
on A3 &
{a1, a2, a3}
on B3 &
{c1, c2}
on C3 holds c3
on C3 by
Th19;
ex p,p1,r,r1 be
Point of CPS9 st not ex s be
Point of CPS9 st ((p,p1,s)
are_collinear & (r,r1,s)
are_collinear ) by
ANPROJ_2:def 14;
then
A2: ex M,N be
LINE of X st not ex q be
POINT of X st q
on M & q
on N by
Th15;
for p,p1,q,q1,r2 be
Point of CPS9 holds ex r,r1 be
Point of CPS9 st (p,q,r)
are_collinear & (p1,q1,r1)
are_collinear & (r2,r,r1)
are_collinear by
ANPROJ_2:def 15;
then
A3: for a be
POINT of X, M,N be
LINE of X holds ex b,c be
POINT of X, S be
LINE of X st a
on S & b
on S & c
on S & b
on M & c
on N by
Th16;
for p1,r2,q,r1,q1,p,r be
Point of CPS9 holds ((p1,r2,q)
are_collinear & (r1,q1,q)
are_collinear & (p1,r1,p)
are_collinear & (r2,q1,p)
are_collinear & (p1,q1,r)
are_collinear & (r2,r1,r)
are_collinear & (p,q,r)
are_collinear implies ((p1,r2,q1)
are_collinear or (p1,r2,r1)
are_collinear or (p1,r1,q1)
are_collinear or (r2,r1,q1)
are_collinear )) by
ANPROJ_2:def 11;
then for p,q,r,s,a,b,c be
POINT of X holds for L,Q,R,S,A,B,C be
LINE of X 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 holds not c
on C by
Th17;
hence thesis by
A1,
A2,
A3;
end;
end
registration
cluster
Desarguesian
Fanoian
2-dimensional for
IncProjSp;
existence
proof
set CPS = the
Fanoian
Desarguesian
CollProjectivePlane;
reconsider CPS9 = CPS as
CollProjectiveSpace;
take X = (
IncProjSp_of CPS9);
for o,p1,p2,p3,q1,q2,q3,r1,r2,r3 be
Point of CPS9 st o
<> q1 & p1
<> q1 & o
<> q2 & p2
<> q2 & o
<> q3 & p3
<> q3 & not (o,p1,p2)
are_collinear & not (o,p1,p3)
are_collinear & not (o,p2,p3)
are_collinear & (p1,p2,r3)
are_collinear & (q1,q2,r3)
are_collinear & (p2,p3,r1)
are_collinear & (q2,q3,r1)
are_collinear & (p1,p3,r2)
are_collinear & (q1,q3,r2)
are_collinear & (o,p1,q1)
are_collinear & (o,p2,q2)
are_collinear & (o,p3,q3)
are_collinear holds (r1,r2,r3)
are_collinear by
ANPROJ_2:def 12;
then
A1: for o,b1,a1,b2,a2,b3,a3,r,s,t be
POINT of X holds for C1,C2,C3,A1,A2,A3,B1,B2,B3 be
LINE of X 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
<> a1 & o
<> a2 & o
<> a3 & o
<> b1 & o
<> b2 & o
<> b3 & a1
<> b1 & a2
<> b2 & a3
<> b3 holds ex O be
LINE of X st
{r, s, t}
on O by
Th18;
for a,b,c,d be
Point of CPS9 holds ex p be
Point of CPS9 st (a,b,p)
are_collinear & (c,d,p)
are_collinear by
ANPROJ_2:def 14;
then
A2: for M,N be
LINE of X holds ex q be
POINT of X st q
on M & q
on N by
Th14;
for p1,r2,q,r1,q1,p,r be
Point of CPS9 holds ((p1,r2,q)
are_collinear & (r1,q1,q)
are_collinear & (p1,r1,p)
are_collinear & (r2,q1,p)
are_collinear & (p1,q1,r)
are_collinear & (r2,r1,r)
are_collinear & (p,q,r)
are_collinear implies ((p1,r2,q1)
are_collinear or (p1,r2,r1)
are_collinear or (p1,r1,q1)
are_collinear or (r2,r1,q1)
are_collinear )) by
ANPROJ_2:def 11;
then for p,q,r,s,a,b,c be
POINT of X holds for L,Q,R,S,A,B,C be
LINE of X 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 holds not c
on C by
Th17;
hence thesis by
A1,
A2;
end;
end
registration
cluster
Pappian
Fanoian
2-dimensional for
IncProjSp;
existence
proof
set CPS = the
Fanoian
Pappian
CollProjectivePlane;
reconsider CPS9 = CPS as
CollProjectiveSpace;
take X = (
IncProjSp_of CPS9);
for o,p1,p2,p3,q1,q2,q3,r1,r2,r3 be
Point of CPS9 st o
<> p2 & o
<> p3 & p2
<> p3 & p1
<> p2 & p1
<> p3 & o
<> q2 & o
<> q3 & q2
<> q3 & q1
<> q2 & q1
<> q3 & not (o,p1,q1)
are_collinear & (o,p1,p2)
are_collinear & (o,p1,p3)
are_collinear & (o,q1,q2)
are_collinear & (o,q1,q3)
are_collinear & (p1,q2,r3)
are_collinear & (q1,p2,r3)
are_collinear & (p1,q3,r2)
are_collinear & (p3,q1,r2)
are_collinear & (p2,q3,r1)
are_collinear & (p3,q2,r1)
are_collinear holds (r1,r2,r3)
are_collinear by
ANPROJ_2:def 13;
then
A1: for o,a1,a2,a3,b1,b2,b3,c1,c2,c3 be
POINT of X holds for A1,A2,A3,B1,B2,B3,C1,C2,C3 be
LINE of X st (o,a1,a2,a3)
are_mutually_distinct & (o,b1,b2,b3)
are_mutually_distinct & A3
<> B3 & o
on A3 & o
on B3 &
{a2, b3, c1}
on A1 &
{a3, b1, c2}
on B1 &
{a1, b2, c3}
on C1 &
{a1, b3, c2}
on A2 &
{a3, b2, c1}
on B2 &
{a2, b1, c3}
on C2 &
{b1, b2, b3}
on A3 &
{a1, a2, a3}
on B3 &
{c1, c2}
on C3 holds c3
on C3 by
Th19;
for a,b,c,d be
Point of CPS9 holds ex p be
Point of CPS9 st (a,b,p)
are_collinear & (c,d,p)
are_collinear by
ANPROJ_2:def 14;
then
A2: for M,N be
LINE of X holds ex q be
POINT of X st q
on M & q
on N by
Th14;
for p1,r2,q,r1,q1,p,r be
Point of CPS9 holds ((p1,r2,q)
are_collinear & (r1,q1,q)
are_collinear & (p1,r1,p)
are_collinear & (r2,q1,p)
are_collinear & (p1,q1,r)
are_collinear & (r2,r1,r)
are_collinear & (p,q,r)
are_collinear implies ((p1,r2,q1)
are_collinear or (p1,r2,r1)
are_collinear or (p1,r1,q1)
are_collinear or (r2,r1,q1)
are_collinear )) by
ANPROJ_2:def 11;
then for p,q,r,s,a,b,c be
POINT of X holds for L,Q,R,S,A,B,C be
LINE of X 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 holds not c
on C by
Th17;
hence thesis by
A1,
A2;
end;
end