:: INCPROJ semantic presentation

definition

let CPS be proper CollSp;
:: original: LINE
redefine mode LINE of CPS -> Subset of CPS;
coherence

proof end;

end;

definition

let CPS be proper CollSp;
func ProjectiveLines CPS -> set equals :: INCPROJ:def 1
{ B where B is Subset of CPS : B is LINE of CPS } ;
coherence ;

end;

:: deftheorem defines ProjectiveLines INCPROJ:def 1 :

registration

let CPS be proper CollSp;
cluster ProjectiveLines CPS -> non empty ;
coherence

proof end;

end;

theorem :: INCPROJ:1

canceled;

theorem Th2: :: INCPROJ:2

for CPS being proper CollSp
for x being set holds
( x is LINE of CPS iff x is Element of ProjectiveLines CPS )

proof end;

definition

let CPS be proper CollSp;
func Proj_Inc CPS -> Relation of the carrier of CPS, ProjectiveLines CPS means :Def2: :: INCPROJ:def 2
for x, y being set holds
( [x,y] in it iff ( x in the carrier of CPS & y in ProjectiveLines CPS & ex Y being set st
( y = Y & x in Y ) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def2 defines Proj_Inc INCPROJ:def 2 :

definition

let CPS be proper CollSp;
func IncProjSp_of CPS -> IncProjStr equals :: INCPROJ:def 3
IncProjStr(# the carrier of CPS,(ProjectiveLines CPS),(Proj_Inc CPS) #);
coherence ;

end;

:: deftheorem defines IncProjSp_of INCPROJ:def 3 :

registration

let CPS be proper CollSp;
cluster IncProjSp_of CPS -> strict ;
coherence ;

end;

theorem :: INCPROJ:3

canceled;

theorem :: INCPROJ:4

for CPS being proper CollSp holds
( 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

for CPS being proper CollSp
for x being set holds
( x is Point of CPS iff x is POINT of (IncProjSp_of CPS) ) ;

theorem Th6: :: INCPROJ:6

for CPS being proper CollSp
for x being set holds
( x is LINE of CPS iff x is LINE of (IncProjSp_of CPS) ) by Th2;

theorem :: INCPROJ:7

canceled;

theorem Th8: :: INCPROJ:8

for CPS being proper CollSp
for s being POINT of (IncProjSp_of CPS)
for S being LINE of (IncProjSp_of CPS) holds
( s on S iff [s,S] in Proj_Inc CPS ) by INCSP_1:def 1;

theorem Th9: :: INCPROJ:9

for CPS being proper CollSp
for p being POINT of (IncProjSp_of CPS)
for P being LINE of (IncProjSp_of CPS)
for p' being Point of CPS
for P' being LINE of CPS st p = p' & P = P' holds
( p on P iff p' in P' )

proof end;

theorem Th10: :: INCPROJ:10

for CPS being proper CollSp ex a', b', c' being Point of CPS st
( a' <> b' & b' <> c' & c' <> a' )

proof end;

theorem Th11: :: INCPROJ:11

for CPS being proper CollSp
for a' being Point of CPS ex b' being Point of CPS st a' <> b'

proof end;

theorem Th12: :: INCPROJ:12

for CPS being proper CollSp
for p, q being POINT of (IncProjSp_of CPS)
for P, Q being LINE of (IncProjSp_of CPS) st p on P & q on P & p on Q & q on Q & not p = q holds
P = Q

proof end;

theorem Th13: :: INCPROJ:13

for CPS being proper CollSp
for p, q being POINT of (IncProjSp_of CPS) ex P being LINE of (IncProjSp_of CPS) st
( p on P & q on P )

proof end;

theorem Th14: :: INCPROJ:14

for CPS being proper CollSp
for a, b, c being POINT of (IncProjSp_of CPS)
for a', b', c' being Point of CPS st a = a' & b = b' & c = c' holds
( a',b',c' is_collinear iff ex P being LINE of (IncProjSp_of CPS) st
( a on P & b on P & c on P ) )

proof end;

theorem Th15: :: INCPROJ:15

for CPS being proper CollSp holds
not for p being POINT of (IncProjSp_of CPS)
for P being LINE of (IncProjSp_of CPS) holds p on P

proof end;

theorem Th16: :: INCPROJ:16

for CPS being CollProjectiveSpace
for P being LINE of (IncProjSp_of CPS) ex a, b, c being POINT of (IncProjSp_of CPS) st
( a <> b & b <> c & c <> a & a on P & b on P & c on P )

proof end;

theorem Th17: :: INCPROJ:17

for CPS being CollProjectiveSpace
for a, b, c, d, p being POINT of (IncProjSp_of CPS)
for M, N, P, Q being LINE of (IncProjSp_of CPS) 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 (IncProjSp_of CPS) st
( q on P & q on Q )

proof end;

theorem Th18: :: INCPROJ:18

for CPS being CollProjectiveSpace st ( for a', b', c', d' being Point of CPS ex p' being Point of CPS st
( a',b',p' is_collinear & c',d',p' is_collinear ) ) holds
for M, N being LINE of (IncProjSp_of CPS) ex q being POINT of (IncProjSp_of CPS) st
( q on M & q on N )

proof end;

theorem Th19: :: INCPROJ:19

for CPS being CollProjectiveSpace st ex p, p1, r, r1 being Point of CPS st
for s being Point of CPS holds
( not p,p1,s is_collinear or not r,r1,s is_collinear ) holds
ex M, N being LINE of (IncProjSp_of CPS) st
for q being POINT of (IncProjSp_of CPS) holds
( not q on M or not q on N )

proof end;

theorem Th20: :: INCPROJ:20

for CPS being CollProjectiveSpace st ( 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 ) ) holds
for a being POINT of (IncProjSp_of CPS)
for M, N being LINE of (IncProjSp_of CPS) ex b, c being POINT of (IncProjSp_of CPS) ex S being LINE of (IncProjSp_of CPS) st
( a on S & b on S & c on S & b on M & c on N )

proof end;

definition

let x, y, z be set ;
canceled;
pred x,y,z are_mutually_different means :Def5: :: INCPROJ:def 5
( x <> y & y <> z & z <> x );
let u be set ;
pred x,y,z,u are_mutually_different means :Def6: :: INCPROJ:def 6
( x <> y & y <> z & z <> x & u <> x & u <> y & u <> z );

end;

:: deftheorem INCPROJ:def 4 :

:: deftheorem Def5 defines are_mutually_different INCPROJ:def 5 :

:: deftheorem Def6 defines are_mutually_different INCPROJ:def 6 :

definition

let CS be IncProjStr ;
let a, b be POINT of CS;
let M be LINE of CS;
pred a,b on M means :Def7: :: INCPROJ:def 7
( a on M & b on M );
let c be POINT of CS;
pred a,b,c on M means :Def8: :: INCPROJ:def 8
( a on M & b on M & c on M );

end;

:: deftheorem Def7 defines on INCPROJ:def 7 :

:: deftheorem Def8 defines on INCPROJ:def 8 :

theorem Th21: :: INCPROJ:21

for CPS being CollProjectiveSpace st ( for p1, r2, q, r1, q1, p, r being Point of CPS st 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 & not p1,r2,q1 is_collinear & not p1,r2,r1 is_collinear & not p1,r1,q1 is_collinear holds
r2,r1,q1 is_collinear ) holds
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

proof end;

theorem Th22: :: INCPROJ:22

for CPS being CollProjectiveSpace st ( 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 ) holds
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

proof end;

theorem Th23: :: INCPROJ:23

for CPS being CollProjectiveSpace st ( 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 ) holds
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

proof end;

definition

let IT be IncProjStr ;
attr IT is partial means :Def9: :: INCPROJ:def 9
for p, q being POINT of IT
for P, Q being LINE of IT st p on P & q on P & p on Q & q on Q & not p = q holds
P = Q;
attr IT is linear means :Def10: :: 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 :Def11: :: INCPROJ:def 11
not for p being POINT of IT
for P being LINE of IT holds p on P;
attr IT is up-3-rank means :Def12: :: 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 :Def13: :: 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;

:: deftheorem Def9 defines partial INCPROJ:def 9 :

:: deftheorem Def10 defines linear INCPROJ:def 10 :

:: deftheorem Def11 defines up-2-dimensional INCPROJ:def 11 :

:: deftheorem Def12 defines up-3-rank INCPROJ:def 12 :

:: deftheorem Def13 defines Vebleian INCPROJ:def 13 :

registration

let CPS be CollProjectiveSpace;
cluster IncProjSp_of CPS -> strict partial linear up-2-dimensional up-3-rank Vebleian ;
coherence

proof end;

end;

registration

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

proof 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 -> strict partial linear up-2-dimensional up-3-rank Vebleian ;
coherence ;

end;

definition

let IT be IncProjSp;
attr IT is 2-dimensional means :Def14: :: INCPROJ:def 14
for M, N being LINE of IT ex q being POINT of IT st
( q on M & q on N );

end;

:: deftheorem Def14 defines 2-dimensional INCPROJ:def 14 :

notation

let IT be IncProjSp;
antonym up-3-dimensional IT for 2-dimensional IT;

end;

definition

let IT be IncProjSp;
canceled;
attr IT is at_most-3-dimensional means :Def16: :: INCPROJ:def 16
for a being POINT of IT
for M, N being LINE of IT ex b, c being POINT of IT ex S being LINE of IT st
( a on S & b on S & c on S & b on M & c on N );

end;

:: deftheorem INCPROJ:def 15 :

:: deftheorem Def16 defines at_most-3-dimensional INCPROJ:def 16 :

definition

let IT be IncProjSp;
attr IT is 3-dimensional means :: INCPROJ:def 17
( IT is at_most-3-dimensional & not IT is 2-dimensional );

end;

:: deftheorem defines 3-dimensional INCPROJ:def 17 :

definition

let IT be IncProjSp;
attr IT is Fanoian means :Def18: :: 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;

:: deftheorem Def18 defines Fanoian INCPROJ:def 18 :

definition

let IT be IncProjSp;
attr IT is Desarguesian means :Def19: :: 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;

:: deftheorem Def19 defines Desarguesian INCPROJ:def 19 :

definition

let IT be IncProjSp;
attr IT is Pappian means :Def20: :: 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;

:: deftheorem Def20 defines Pappian INCPROJ:def 20 :

registration

cluster up-3-dimensional at_most-3-dimensional Fanoian Desarguesian IncProjStr ;
existence

proof end;

end;

registration

cluster up-3-dimensional at_most-3-dimensional Fanoian Pappian IncProjStr ;
existence

proof end;

end;

registration

cluster 2-dimensional Fanoian Desarguesian IncProjStr ;
existence

proof end;

end;

registration

cluster 2-dimensional Fanoian Pappian IncProjStr ;
existence

proof end;

end;