Journal of Formalized Mathematics
Volume 2, 1990
University of Bialystok
Copyright (c) 1990 Association of Mizar Users

### Incidence Projective Spaces

by
Wojciech Leonczuk, and
Krzysztof Prazmowski

MML identifier: INCPROJ
[ Mizar article, MML identifier index ]

```environ

vocabulary COLLSP, PRE_TOPC, INCSP_1, RELAT_1, ANPROJ_2, ANALOAF, VECTSP_1,
AFF_2, INCPROJ;
notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELSET_1, STRUCT_0, PRE_TOPC,
INCSP_1, COLLSP, ANPROJ_2;
constructors INCSP_1, ANPROJ_2, DOMAIN_1, XBOOLE_0;
clusters ANPROJ_2, RELSET_1, STRUCT_0, SUBSET_1, ZFMISC_1, XBOOLE_0;
requirements SUBSET, BOOLE;

begin

reserve CPS for proper CollSp,
B for Element of bool the carrier of CPS,
p for Point of CPS,
x, y, z, Y for set;

definition let CPS;
redefine mode LINE of CPS -> Element of bool the carrier of CPS;
end;

definition let CPS;
func ProjectiveLines(CPS) -> set equals
:: INCPROJ:def 1
{B : B is LINE of CPS};
end;

definition let CPS;
cluster ProjectiveLines(CPS) -> non empty;
end;

canceled;

theorem :: INCPROJ:2
x is LINE of CPS iff x is Element of ProjectiveLines(CPS);

definition let CPS;
func Proj_Inc(CPS) -> Relation of the carrier of CPS, ProjectiveLines(CPS)
means
:: INCPROJ:def 2
for x,y holds [x,y] in it iff x in the carrier of CPS &
y in ProjectiveLines(CPS) & ex Y st y=Y & x in Y;
end;

definition let CPS;
func IncProjSp_of(CPS) -> IncProjStr equals
:: INCPROJ:def 3
IncProjStr (# the carrier of CPS, ProjectiveLines(CPS), Proj_Inc(CPS) #);
end;

definition let CPS;
cluster IncProjSp_of(CPS) -> strict;
end;

canceled;

theorem :: INCPROJ:4
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:5
x is Point of CPS iff x is POINT of IncProjSp_of(CPS);

theorem :: INCPROJ:6
x is LINE of CPS iff x is LINE of IncProjSp_of(CPS);

reserve a,b,c,p,q,s for POINT of IncProjSp_of(CPS),
P,Q,S for LINE of IncProjSp_of(CPS),
a',b',c',p',q',r' for Point of CPS,
P' for LINE of CPS;

canceled;

theorem :: INCPROJ:8
s on S iff [s,S] in Proj_Inc(CPS);

theorem :: INCPROJ:9
p = p' & P = P' implies (p on P iff p' in P');

theorem :: INCPROJ:10
ex a', b', c' st a'<>b' & b'<>c' & c'<>a';

theorem :: INCPROJ:11
ex b' st a'<>b';

theorem :: INCPROJ:12
p on P & q on P & p on Q & q on Q implies p = q or P = Q;

theorem :: INCPROJ:13
ex P st p on P & q on P;

theorem :: INCPROJ:14
a = a' & b = b' & c = c'
implies
(a',b',c' is_collinear iff ex P st a on P & b on P & c on P);

theorem :: INCPROJ:15
ex p, P st not p on P;

reserve CPS for CollProjectiveSpace;

reserve a,b,c,d,p,q for POINT of IncProjSp_of(CPS),
P,Q,S,M,N for LINE of IncProjSp_of(CPS),
a',b',c',d',p',q' for Point of CPS;

theorem :: INCPROJ:16
ex a, b, c st a<>b & b<>c & c <>a & a on P & b on P & c on P;

theorem :: INCPROJ:17
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;

theorem :: INCPROJ:18
(for a',b',c',d' ex p' st a', b', p' is_collinear & c', d', p' is_collinear)
implies
for M, N ex q st q on M & q on N;

theorem :: INCPROJ:19
(ex p, p1, r, r1 being Point of CPS st not ex s being Point of CPS st
(p, p1, s is_collinear & r, r1, s is_collinear))
implies
(ex M, N st not ex q st q on M & q on N);

theorem :: INCPROJ:20
(for p, p1, q, q1, r2 being Point of CPS
ex r, r1 being Point of CPS st
p,q,r is_collinear & p1,q1,r1 is_collinear & r2,r,r1 is_collinear)
implies
(for a, M, N ex b, c, S st a on S & b on S & c on S & b on M & c on N);

definition let x, y, z be set;
canceled;

pred x,y,z are_mutually_different means
:: INCPROJ:def 5

x <> y & y <> z & z <> x;

let u be set;
pred x, y, z, u are_mutually_different means
:: INCPROJ:def 6

x <> y & y <> z & z <> x & u <> x & u <> y & u <> z;
end;

definition
let CS be IncProjStr, a,b be POINT of CS,
M be LINE of CS;
pred a,b on M means
:: INCPROJ:def 7

a on M & b on M;

let c be POINT of CS;
pred a,b,c on M means
:: INCPROJ:def 8

a on M & b on M & c on M;
end;

theorem :: INCPROJ:21
(for p1, r2, q, r1, q1, p, r being Point of CPS holds
(p1,r2,q is_collinear & r1,q1,q is_collinear &
p1,r1,p is_collinear & r2,q1,p is_collinear &
p1,q1,r is_collinear & r2,r1,r is_collinear & p,q,r is_collinear
implies
(p1,r2,q1 is_collinear or p1,r2,r1 is_collinear or
p1,r1,q1 is_collinear or r2,r1,q1 is_collinear)))
implies
(for p, q, r, s, a, b, c being POINT of IncProjSp_of(CPS)
for L, Q, R, S, A, B, C being 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 &
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);

theorem :: INCPROJ:22
(for o,p1,p2,p3,q1,q2,q3,r1,r2,r3 being Point of CPS st
o<>q1 & p1<>q1 & o<>q2 & p2<>q2 & o<>q3 & p3<>q3 &
not o,p1,p2 is_collinear & not o,p1,p3 is_collinear &
not o,p2,p3 is_collinear &
p1,p2,r3 is_collinear & q1,q2,r3 is_collinear &
p2,p3,r1 is_collinear & q2,q3,r1 is_collinear &
p1,p3,r2 is_collinear & q1,q3,r2 is_collinear &
o,p1,q1 is_collinear & o,p2,q2 is_collinear & o,p3,q3 is_collinear
holds
r1,r2,r3 is_collinear)
implies
(for o,b1,a1,b2,a2,b3,a3,r,s,t being POINT of IncProjSp_of(CPS)
for C1,C2,C3,A1,A2,A3,B1,B2,B3 being 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_different &
o<>a1 & o<>a2 & o<>a3 & o<>b1 & o<>b2 & o<>b3 & a1<>b1 & a2<>b2 & a3<>b3
holds
ex O being LINE of IncProjSp_of(CPS) st r,s,t on O);

theorem :: INCPROJ:23
(for o,p1,p2,p3,q1,q2,q3,r1,r2,r3 being 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 is_collinear & o,p1,p2 is_collinear &
o,p1,p3 is_collinear & o,q1,q2 is_collinear & o,q1,q3 is_collinear &
p1,q2,r3 is_collinear & q1,p2,r3 is_collinear & p1,q3,r2 is_collinear &
p3,q1,r2 is_collinear & p2,q3,r1 is_collinear & p3,q2,r1 is_collinear
holds
r1,r2,r3 is_collinear)
implies
(for o,a1,a2,a3,b1,b2,b3,c1,c2,c3 being POINT of IncProjSp_of(CPS)
for A1,A2,A3,B1,B2,B3,C1,C2,C3 being LINE of IncProjSp_of(CPS) st
o,a1,a2,a3 are_mutually_different & o,b1,b2,b3 are_mutually_different &
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);

definition let IT be IncProjStr;
attr IT is partial means
:: INCPROJ:def 9

for p, q being POINT of IT, P, Q being LINE of IT st
p on P & q on P & p on Q & q on Q holds
p = q or P = Q;

attr IT is linear means
:: INCPROJ:def 10

for p,q being POINT of IT ex P being LINE of IT st p on P & q on P;

attr IT is up-2-dimensional means
:: INCPROJ:def 11

ex p being POINT of IT, P being LINE of IT st not p on P;

attr IT is up-3-rank means
:: INCPROJ:def 12

for P being LINE of IT ex a, b, c being POINT of IT st
a <> b & b <> c & c <> a & a on P & b on P & c on P;

attr IT is Vebleian means
:: INCPROJ:def 13

for a, b, c, d, p, q being POINT of IT
for M, N, P, Q being LINE of IT 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 being POINT of IT st q on P & q on Q;
end;

definition
let CPS be CollProjectiveSpace;
cluster IncProjSp_of(CPS) -> partial linear up-2-dimensional
up-3-rank Vebleian;
end;

definition
cluster strict partial linear up-2-dimensional up-3-rank
Vebleian IncProjStr;
end;

definition
mode IncProjSp is partial linear up-2-dimensional up-3-rank Vebleian
IncProjStr;
end;

definition
let CPS be CollProjectiveSpace;
cluster IncProjSp_of(CPS) -> partial linear up-2-dimensional up-3-rank
Vebleian;
end;

definition let IT be IncProjSp;
attr IT is 2-dimensional means
:: INCPROJ:def 14

for M,N being LINE of IT ex q being POINT of IT st q on M & q on N;
antonym IT is up-3-dimensional;
end;

definition
let IT be IncProjSp;
canceled;

attr IT is at_most-3-dimensional means
:: INCPROJ:def 16

for a being POINT of IT, M, N being LINE of IT
ex b,c being POINT of IT, S being 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;
attr IT is 3-dimensional means
:: INCPROJ:def 17
IT is at_most-3-dimensional up-3-dimensional;
end;

definition let IT be IncProjSp;
attr IT is Fanoian means
:: INCPROJ:def 18

for p,q,r,s,a,b,c being POINT of IT
for L,Q,R,S,A,B,C being 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 IncProjSp;
attr IT is Desarguesian means
:: INCPROJ:def 19

for o,b1,a1,b2,a2,b3,a3,r,s,t being POINT of IT
for C1,C2,C3,A1,A2,A3,B1,B2,B3 being 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_different &
o<>a1 & o<>a2 & o<>a3 & o<>b1 & o<>b2 & o<>b3 & a1<>b1 & a2<>b2 & a3<>b3
holds
ex O being LINE of IT st r,s,t on O;
end;

definition let IT be IncProjSp;
attr IT is Pappian means
:: INCPROJ:def 20

for o,a1,a2,a3,b1,b2,b3,c1,c2,c3 being POINT of IT
for A1,A2,A3,B1,B2,B3,C1,C2,C3 being LINE of IT st
o,a1,a2,a3 are_mutually_different & o,b1,b2,b3 are_mutually_different &
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;

definition
cluster Desarguesian Fanoian at_most-3-dimensional up-3-dimensional
IncProjSp;
end;

definition
cluster Pappian Fanoian at_most-3-dimensional up-3-dimensional
IncProjSp;
end;

definition
cluster Desarguesian Fanoian 2-dimensional IncProjSp;
end;

definition
cluster Pappian Fanoian 2-dimensional IncProjSp;
end;
```