:: Incidence Projective Spaces
:: by Wojciech Leo\'nczuk and Krzysztof Pra\.zmowski
::
:: Received October 4, 1990
:: Copyright (c) 1990-2021 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 SUBSET_1, COLLSP, PRE_TOPC, INCSP_1, TARSKI, STRUCT_0, XBOOLE_0,
RELAT_1, ANPROJ_2, ZFMISC_1, FDIFF_1, ANALOAF, VECTSP_1, AFF_2, INCPROJ,
PENCIL_1;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, DOMAIN_1, RELSET_1, STRUCT_0,
PRE_TOPC, INCSP_1, COLLSP, ANPROJ_2;
constructors DOMAIN_1, INCSP_1, ANPROJ_2;
registrations RELSET_1, STRUCT_0, ANPROJ_2;
requirements SUBSET, BOOLE;
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;
redefine mode LINE of CPS -> Subset of CPS;
end;
definition
let CPS;
func ProjectiveLines(CPS) -> set equals
:: INCPROJ:def 1
{B : B is LINE of CPS};
end;
registration
let CPS;
cluster ProjectiveLines(CPS) -> non empty;
end;
theorem :: INCPROJ:1
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 being 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;
end;
definition
let CPS;
func IncProjSp_of(CPS) -> IncProjStr equals
:: INCPROJ:def 3
IncProjStr (# the carrier of CPS
, ProjectiveLines(CPS), Proj_Inc(CPS) #);
end;
registration
let CPS;
cluster IncProjSp_of(CPS) -> strict;
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);
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
p = p9 & P = P9 implies (p on P iff p9 in P9);
theorem :: INCPROJ:6
ex a9, b9, c9 st a9<>b9 & b9<>c9 & c9<>a9;
theorem :: INCPROJ:7
ex b9 st a9<>b9;
theorem :: INCPROJ:8
p on P & q on P & p on Q & q on Q implies p = q or P = Q;
theorem :: INCPROJ:9
ex P st p on P & q on P;
theorem :: INCPROJ:10
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);
theorem :: INCPROJ:11
ex p, P st not p on P;
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
ex a, b, c st a<>b & b<>c & c <>a & a on P & b on P & c on P;
theorem :: INCPROJ:13
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:14
(for a9,b9,c9,d9 ex p9 st a9, b9, p9 are_collinear & c9, d9, p9
are_collinear) implies for M, N ex q st q on M & q on N;
theorem :: INCPROJ:15
(ex p, p1, r, r1 being Point of CPS st not ex s being 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;
theorem :: INCPROJ:16
(for p, p1, q, q1, r2 being Point of CPS ex r, r1 being Point of
CPS st p,q,r are_collinear & p1,q1,r1 are_collinear & r2,r,r1 are_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;
theorem :: INCPROJ:17
(for p1, r2, q, r1, q1, p, r being 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 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 & {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:18
(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 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 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_distinct
& 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:19
(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 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 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_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;
definition
let S be IncProjStr;
attr S is partial means
:: INCPROJ:def 4
for p, q being POINT of S, P, Q being LINE of
S st p on P & q on P & p on Q & q on Q holds p = q or P = Q;
redefine attr S is linear means
:: INCPROJ:def 5
for p,q being POINT of S ex P being LINE of S st p on P & q on P;
end;
definition
let S be IncProjStr;
attr S is up-2-dimensional means
:: INCPROJ:def 6
ex p being POINT of S, P being LINE of S st not p on P;
attr S is up-3-rank means
:: INCPROJ:def 7
for P being LINE of S ex a, b, c being
POINT of S st a <> b & b <> c & c <> a & a on P & b on P & c on P;
attr S is Vebleian means
:: INCPROJ:def 8
for a, b, c, d, p, q being POINT of S for M
, N, P, Q being 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 being 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;
end;
registration
cluster strict partial linear up-2-dimensional up-3-rank Vebleian for
IncProjStr;
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;
end;
definition
let IT be IncProjSp;
attr IT is 2-dimensional means
:: INCPROJ:def 9
for M,N being LINE of IT ex q being 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;
attr IT is at_most-3-dimensional means
:: INCPROJ:def 10
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 11
IT is at_most-3-dimensional up-3-dimensional;
end;
definition
let IT be IncProjStr;
attr IT is Fanoian means
:: INCPROJ:def 12
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 IncProjStr;
attr IT is Desarguesian means
:: INCPROJ:def 13
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_distinct & 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 IncProjStr;
attr IT is Pappian means
:: INCPROJ:def 14
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_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;
end;
registration
cluster Pappian Fanoian at_most-3-dimensional up-3-dimensional for IncProjSp;
end;
registration
cluster Desarguesian Fanoian 2-dimensional for IncProjSp;
end;
registration
cluster Pappian Fanoian 2-dimensional for IncProjSp;
end;