:: AFPROJ semantic presentation

theorem Th1: :: AFPROJ:1

for AS being AffinSpace
for X being Subset of AS st AS is AffinPlane & X = the carrier of AS holds
X is_plane

proof end;

theorem Th2: :: AFPROJ:2

for AS being AffinSpace
for X being Subset of AS st AS is AffinPlane & X is_plane holds
X = the carrier of AS

proof end;

theorem Th3: :: AFPROJ:3

for AS being AffinSpace
for X, Y being Subset of AS st AS is AffinPlane & X is_plane & Y is_plane holds
X = Y

proof end;

theorem :: AFPROJ:4

for AS being AffinSpace
for X being Subset of AS st X = the carrier of AS & X is_plane holds
AS is AffinPlane

proof end;

theorem Th5: :: AFPROJ:5

for AS being AffinSpace
for A, K, X, Y being Subset of AS st not A // K & A '||' X & A '||' Y & K '||' X & K '||' Y & A is_line & K is_line & X is_plane & Y is_plane holds
X '||' Y

proof end;

theorem Th6: :: AFPROJ:6

for AS being AffinSpace
for X, A, Y being Subset of AS st X is_plane & A '||' X & X '||' Y holds
A '||' Y

proof end;

definition

let AS be AffinSpace;
func AfLines AS -> Subset-Family of AS equals :: AFPROJ:def 1
{ A where A is Subset of AS : A is_line } ;
coherence

proof end;

end;

:: deftheorem defines AfLines AFPROJ:def 1 :

definition

let AS be AffinSpace;
func AfPlanes AS -> Subset-Family of AS equals :: AFPROJ:def 2
{ A where A is Subset of AS : A is_plane } ;
coherence

proof end;

end;

:: deftheorem defines AfPlanes AFPROJ:def 2 :

theorem Th7: :: AFPROJ:7

for AS being AffinSpace
for x being set holds
( x in AfLines AS iff ex X being Subset of AS st
( x = X & X is_line ) ) ;

theorem Th8: :: AFPROJ:8

for AS being AffinSpace
for x being set holds
( x in AfPlanes AS iff ex X being Subset of AS st
( x = X & X is_plane ) ) ;

definition

let AS be AffinSpace;
func LinesParallelity AS -> Equivalence_Relation of AfLines AS equals :: AFPROJ:def 3
{ [K,M] where K, M is Subset of AS : ( K is_line & M is_line & K '||' M ) } ;
coherence

proof end;

end;

:: deftheorem defines LinesParallelity AFPROJ:def 3 :

definition

let AS be AffinSpace;
func PlanesParallelity AS -> Equivalence_Relation of AfPlanes AS equals :: AFPROJ:def 4
{ [X,Y] where X, Y is Subset of AS : ( X is_plane & Y is_plane & X '||' Y ) } ;
coherence

proof end;

end;

:: deftheorem defines PlanesParallelity AFPROJ:def 4 :

definition

let AS be AffinSpace;
let X be Subset of AS;
assume X is_line ;
func LDir X -> Subset of (AfLines AS) equals :Def5: :: AFPROJ:def 5
Class (LinesParallelity AS),X;
correctness ;

end;

:: deftheorem Def5 defines LDir AFPROJ:def 5 :

definition

let AS be AffinSpace;
let X be Subset of AS;
assume X is_plane ;
func PDir X -> Subset of (AfPlanes AS) equals :Def6: :: AFPROJ:def 6
Class (PlanesParallelity AS),X;
correctness ;

end;

:: deftheorem Def6 defines PDir AFPROJ:def 6 :

theorem Th9: :: AFPROJ:9

for AS being AffinSpace
for X being Subset of AS st X is_line holds
for x being set holds
( x in LDir X iff ex Y being Subset of AS st
( x = Y & Y is_line & X '||' Y ) )

proof end;

theorem Th10: :: AFPROJ:10

for AS being AffinSpace
for X being Subset of AS st X is_plane holds
for x being set holds
( x in PDir X iff ex Y being Subset of AS st
( x = Y & Y is_plane & X '||' Y ) )

proof end;

theorem Th11: :: AFPROJ:11

for AS being AffinSpace
for X, Y being Subset of AS st X is_line & Y is_line holds
( LDir X = LDir Y iff X // Y )

proof end;

theorem Th12: :: AFPROJ:12

for AS being AffinSpace
for X, Y being Subset of AS st X is_line & Y is_line holds
( LDir X = LDir Y iff X '||' Y )

proof end;

theorem Th13: :: AFPROJ:13

for AS being AffinSpace
for X, Y being Subset of AS st X is_plane & Y is_plane holds
( PDir X = PDir Y iff X '||' Y )

proof end;

definition

let AS be AffinSpace;
func Dir_of_Lines AS -> non empty set equals :: AFPROJ:def 7
Class (LinesParallelity AS);
coherence

proof end;

end;

:: deftheorem defines Dir_of_Lines AFPROJ:def 7 :

definition

let AS be AffinSpace;
func Dir_of_Planes AS -> non empty set equals :: AFPROJ:def 8
Class (PlanesParallelity AS);
coherence

proof end;

end;

:: deftheorem defines Dir_of_Planes AFPROJ:def 8 :

theorem Th14: :: AFPROJ:14

for AS being AffinSpace
for x being set holds
( x in Dir_of_Lines AS iff ex X being Subset of AS st
( x = LDir X & X is_line ) )

proof end;

theorem Th15: :: AFPROJ:15

for AS being AffinSpace
for x being set holds
( x in Dir_of_Planes AS iff ex X being Subset of AS st
( x = PDir X & X is_plane ) )

proof end;

theorem Th16: :: AFPROJ:16

for AS being AffinSpace holds the carrier of AS misses Dir_of_Lines AS

proof end;

theorem :: AFPROJ:17

for AS being AffinSpace st AS is AffinPlane holds
AfLines AS misses Dir_of_Planes AS

proof end;

theorem Th18: :: AFPROJ:18

for AS being AffinSpace
for x being set holds
( x in [:(AfLines AS),{1}:] iff ex X being Subset of AS st
( x = [X,1] & X is_line ) )

proof end;

theorem Th19: :: AFPROJ:19

for AS being AffinSpace
for x being set holds
( x in [:(Dir_of_Planes AS),{2}:] iff ex X being Subset of AS st
( x = [(PDir X),2] & X is_plane ) )

proof end;

definition

let AS be AffinSpace;
func ProjectivePoints AS -> non empty set equals :: AFPROJ:def 9
the carrier of AS \/ (Dir_of_Lines AS);
correctness ;

end;

:: deftheorem defines ProjectivePoints AFPROJ:def 9 :

definition

let AS be AffinSpace;
func ProjectiveLines AS -> non empty set equals :: AFPROJ:def 10
[:(AfLines AS),{1}:] \/ [:(Dir_of_Planes AS),{2}:];
coherence ;

end;

:: deftheorem defines ProjectiveLines AFPROJ:def 10 :

definition

let AS be AffinSpace;
func Proj_Inc AS -> Relation of ProjectivePoints AS, ProjectiveLines AS means :Def11: :: AFPROJ:def 11
for x, y being set holds
( [x,y] in it iff ( ex K being Subset of AS st
( K is_line & y = [K,1] & ( ( x in the carrier of AS & x in K ) or x = LDir K ) ) or ex K, X being Subset of AS st
( K is_line & X is_plane & x = LDir K & y = [(PDir X),2] & K '||' X ) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def11 defines Proj_Inc AFPROJ:def 11 :

definition

let AS be AffinSpace;
func Inc_of_Dir AS -> Relation of Dir_of_Lines AS, Dir_of_Planes AS means :Def12: :: AFPROJ:def 12
for x, y being set holds
( [x,y] in it iff ex A, X being Subset of AS st
( x = LDir A & y = PDir X & A is_line & X is_plane & A '||' X ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def12 defines Inc_of_Dir AFPROJ:def 12 :

definition

let AS be AffinSpace;
func IncProjSp_of AS -> strict IncProjStr equals :: AFPROJ:def 13
IncProjStr(# (ProjectivePoints AS),(ProjectiveLines AS),(Proj_Inc AS) #);
correctness ;

end;

:: deftheorem defines IncProjSp_of AFPROJ:def 13 :

definition

let AS be AffinSpace;
func ProjHorizon AS -> strict IncProjStr equals :: AFPROJ:def 14
IncProjStr(# (Dir_of_Lines AS),(Dir_of_Planes AS),(Inc_of_Dir AS) #);
correctness ;

end;

:: deftheorem defines ProjHorizon AFPROJ:def 14 :

theorem Th20: :: AFPROJ:20

for AS being AffinSpace
for x being set holds
( x is POINT of (IncProjSp_of AS) iff ( x is Element of AS or ex X being Subset of AS st
( x = LDir X & X is_line ) ) )

proof end;

theorem Th21: :: AFPROJ:21

for AS being AffinSpace
for x being set holds
( x is Element of the Points of (ProjHorizon AS) iff ex X being Subset of AS st
( x = LDir X & X is_line ) ) by Th14;

theorem Th22: :: AFPROJ:22

for AS being AffinSpace
for x being set st x is Element of the Points of (ProjHorizon AS) holds
x is POINT of (IncProjSp_of AS)

proof end;

theorem Th23: :: AFPROJ:23

for AS being AffinSpace
for x being set holds
( x is LINE of (IncProjSp_of AS) iff ex X being Subset of AS st
( ( x = [X,1] & X is_line ) or ( x = [(PDir X),2] & X is_plane ) ) )

proof end;

theorem Th24: :: AFPROJ:24

for AS being AffinSpace
for x being set holds
( x is Element of the Lines of (ProjHorizon AS) iff ex X being Subset of AS st
( x = PDir X & X is_plane ) ) by Th15;

theorem Th25: :: AFPROJ:25

for AS being AffinSpace
for x being set st x is Element of the Lines of (ProjHorizon AS) holds
[x,2] is LINE of (IncProjSp_of AS)

proof end;

theorem Th26: :: AFPROJ:26

for AS being AffinSpace
for x being Element of AS
for X being Subset of AS
for a being POINT of (IncProjSp_of AS)
for A being LINE of (IncProjSp_of AS) st x = a & [X,1] = A holds
( a on A iff ( X is_line & x in X ) )

proof end;

theorem Th27: :: AFPROJ:27

for AS being AffinSpace
for x being Element of AS
for X being Subset of AS
for a being POINT of (IncProjSp_of AS)
for A being LINE of (IncProjSp_of AS) st x = a & [(PDir X),2] = A & X is_plane holds
not a on A

proof end;

theorem Th28: :: AFPROJ:28

for AS being AffinSpace
for Y, X being Subset of AS
for a being POINT of (IncProjSp_of AS)
for A being LINE of (IncProjSp_of AS) st a = LDir Y & [X,1] = A & Y is_line & X is_line holds
( a on A iff Y '||' X )

proof end;

theorem Th29: :: AFPROJ:29

for AS being AffinSpace
for Y, X being Subset of AS
for a being POINT of (IncProjSp_of AS)
for A being LINE of (IncProjSp_of AS) st a = LDir Y & A = [(PDir X),2] & Y is_line & X is_plane holds
( a on A iff Y '||' X )

proof end;

theorem Th30: :: AFPROJ:30

for AS being AffinSpace
for X being Subset of AS
for a being POINT of (IncProjSp_of AS)
for A being LINE of (IncProjSp_of AS) st X is_line & a = LDir X & A = [X,1] holds
a on A

proof end;

theorem Th31: :: AFPROJ:31

for AS being AffinSpace
for X, Y being Subset of AS
for a being POINT of (IncProjSp_of AS)
for A being LINE of (IncProjSp_of AS) st X is_line & Y is_plane & X c= Y & a = LDir X & A = [(PDir Y),2] holds
a on A

proof end;

theorem Th32: :: AFPROJ:32

for AS being AffinSpace
for Y, X, X' being Subset of AS
for a being POINT of (IncProjSp_of AS)
for A being LINE of (IncProjSp_of AS) st Y is_plane & X c= Y & X' // X & a = LDir X' & A = [(PDir Y),2] holds
a on A

proof end;

theorem :: AFPROJ:33

for AS being AffinSpace
for X being Subset of AS
for a being POINT of (IncProjSp_of AS)
for A being LINE of (IncProjSp_of AS) st A = [(PDir X),2] & X is_plane & a on A holds
not a is Element of AS by Th27;

theorem Th34: :: AFPROJ:34

for AS being AffinSpace
for X being Subset of AS
for p being POINT of (IncProjSp_of AS)
for A being LINE of (IncProjSp_of AS) st A = [X,1] & X is_line & p on A & p is not Element of AS holds
p = LDir X

proof end;

theorem Th35: :: AFPROJ:35

for AS being AffinSpace
for X being Subset of AS
for p, a being POINT of (IncProjSp_of AS)
for A being LINE of (IncProjSp_of AS) st A = [X,1] & X is_line & p on A & a on A & a <> p & p is not Element of the carrier of AS holds
a is Element of AS

proof end;

theorem Th36: :: AFPROJ:36

for AS being AffinSpace
for X, Y being Subset of AS
for a being Element of the Points of (ProjHorizon AS)
for A being Element of the Lines of (ProjHorizon AS) st a = LDir X & A = PDir Y & X is_line & Y is_plane holds
( a on A iff X '||' Y )

proof end;

theorem Th37: :: AFPROJ:37

for AS being AffinSpace
for a being Element of the Points of (ProjHorizon AS)
for a' being Element of the Points of (IncProjSp_of AS)
for A being Element of the Lines of (ProjHorizon AS)
for A' being LINE of (IncProjSp_of AS) st a' = a & A' = [A,2] holds
( a on A iff a' on A' )

proof end;

theorem Th38: :: AFPROJ:38

for AS being AffinSpace
for a, b being Element of the Points of (ProjHorizon AS)
for A, K being Element of the Lines of (ProjHorizon AS) st a on A & a on K & b on A & b on K & not a = b holds
A = K

proof end;

theorem Th39: :: AFPROJ:39

for AS being AffinSpace
for A being Element of the Lines of (ProjHorizon AS) ex a, b, c being Element of the Points of (ProjHorizon AS) st
( a on A & b on A & c on A & a <> b & b <> c & c <> a )

proof end;

theorem Th40: :: AFPROJ:40

for AS being AffinSpace
for a, b being Element of the Points of (ProjHorizon AS) ex A being Element of the Lines of (ProjHorizon AS) st
( a on A & b on A )

proof end;

Lm1: for AS being AffinSpace st AS is not AffinPlane holds
ex a being Element of the Points of (ProjHorizon AS) ex A being Element of the Lines of (ProjHorizon AS) st not a on A

proof end;

Lm2: for AS being AffinSpace
for a, b being POINT of (IncProjSp_of AS)
for A, K being LINE of (IncProjSp_of AS) st a on A & a on K & b on A & b on K & not a = b holds
A = K

proof end;

Lm3: for AS being AffinSpace
for A being LINE of (IncProjSp_of AS) ex a, b, c being POINT of (IncProjSp_of AS) st
( a on A & b on A & c on A & a <> b & b <> c & c <> a )

proof end;

Lm4: for AS being AffinSpace
for a, b being POINT of (IncProjSp_of AS) ex A being LINE of (IncProjSp_of AS) st
( a on A & b on A )

proof end;

Lm5: for AS being AffinSpace
for A, K being LINE of (IncProjSp_of AS) st AS is AffinPlane holds
ex a being POINT of (IncProjSp_of AS) st
( a on A & a on K )

proof end;

Lm6: for AS being AffinSpace holds
not for a being POINT of (IncProjSp_of AS)
for A being LINE of (IncProjSp_of AS) holds a on A

proof end;

theorem Th41: :: AFPROJ:41

for AS being AffinSpace
for x, y being Element of the Points of (ProjHorizon AS)
for X being Element of the Lines of (IncProjSp_of AS) st x <> y & [x,X] in the Inc of (IncProjSp_of AS) & [y,X] in the Inc of (IncProjSp_of AS) holds
ex Y being Element of the Lines of (ProjHorizon AS) st X = [Y,2]

proof end;

theorem Th42: :: AFPROJ:42

for AS being AffinSpace
for x being POINT of (IncProjSp_of AS)
for X being Element of the Lines of (ProjHorizon AS) st [x,[X,2]] in the Inc of (IncProjSp_of AS) holds
x is Element of the Points of (ProjHorizon AS)

proof end;

Lm7: for AS being AffinSpace
for x being Element of AS
for X, X', Y, Y' being Subset of AS
for p, b, c being POINT of (IncProjSp_of AS)
for A, K, M being LINE of (IncProjSp_of AS) st X is_line & X' is_line & Y is_plane & X c= Y & X' c= Y & x = p & A = [X,1] & K = [X',1] & A <> K & b on A & c on K & b on M & c on M & b <> c & M = [Y',1] & Y' is_line holds
Y' c= Y

proof end;

Lm8: for AS being AffinSpace
for x being Element of AS
for X, X', Y, Y' being Subset of AS
for p, b, c being POINT of (IncProjSp_of AS)
for A, K, M being LINE of (IncProjSp_of AS) st X is_line & X' is_line & Y is_plane & X c= Y & X' c= Y & x = p & A = [X,1] & K = [X',1] & A <> K & b on A & c on K & b on M & c on M & b <> c & M = [(PDir Y'),2] & Y' is_plane holds
( Y' '||' Y & Y '||' Y' )

proof end;

theorem Th43: :: AFPROJ:43

for AS being AffinSpace
for Y, X, X' being Subset of AS
for P, Q being LINE of (IncProjSp_of AS) st Y is_plane & X is_line & X' is_line & X c= Y & X' c= Y & P = [X,1] & Q = [X',1] holds
ex q being POINT of (IncProjSp_of AS) st
( q on P & q on Q )

proof end;

Lm9: for AS being AffinSpace
for a, b, c, d, p being POINT of (IncProjSp_of AS)
for M, N, P, Q being LINE of (IncProjSp_of AS) 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 & p is Element of AS holds
ex q being POINT of (IncProjSp_of AS) st
( q on P & q on Q )

proof end;

Lm10: for AS being AffinSpace
for a, b, c, d, p being POINT of (IncProjSp_of AS)
for M, N, P, Q being LINE of (IncProjSp_of AS) 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 & p is not Element of AS & a is Element of AS holds
ex q being POINT of (IncProjSp_of AS) st
( q on P & q on Q )

proof end;

Lm11: for AS being AffinSpace
for a, b, c, d, p being POINT of (IncProjSp_of AS)
for M, N, P, Q being LINE of (IncProjSp_of AS) 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 & p is not Element of AS & ( a is Element of AS or b is Element of AS or c is Element of AS or d is Element of AS ) holds
ex q being POINT of (IncProjSp_of AS) st
( q on P & q on Q )

proof end;

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

proof end;

theorem Th44: :: AFPROJ:44

for AS being AffinSpace
for a, b, c, d, p being Element of the Points of (ProjHorizon AS)
for M, N, P, Q being Element of the Lines of (ProjHorizon AS) 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 Element of the Points of (ProjHorizon AS) st
( q on P & q on Q )

proof end;

registration

let AS be AffinSpace;
cluster IncProjSp_of AS -> strict partial linear up-2-dimensional up-3-rank Vebleian ;
correctness

proof end;

end;

registration

cluster strict 2-dimensional IncProjStr ;
existence

proof end;

end;

registration

let AS be AffinPlane;
cluster IncProjSp_of AS -> strict partial linear up-2-dimensional up-3-rank Vebleian 2-dimensional ;
correctness

proof end;

end;

theorem :: AFPROJ:45

for AS being AffinSpace st IncProjSp_of AS is 2-dimensional holds
AS is AffinPlane

proof end;

theorem :: AFPROJ:46

for AS being AffinSpace st AS is not AffinPlane holds
ProjHorizon AS is IncProjSp

proof end;

theorem :: AFPROJ:47

for AS being AffinSpace st ProjHorizon AS is IncProjSp holds
not AS is AffinPlane

proof end;

theorem Th48: :: AFPROJ:48

for AS being AffinSpace
for M, N being Subset of AS
for o, a, b, c, a', b', c' being Element of the carrier of AS st M is_line & N is_line & M <> N & o in M & o in N & o <> a & o <> a' & o <> b & o <> b' & o <> c & o <> c' & a in M & b in M & c in M & a' in N & b' in N & c' in N & a,b' // b,a' & b,c' // c,b' & ( a = b or b = c or a = c ) holds
a,c' // c,a'

proof end;

theorem :: AFPROJ:49

for AS being AffinSpace st IncProjSp_of AS is Pappian holds
AS is Pappian

proof end;

theorem Th50: :: AFPROJ:50

for AS being AffinSpace
for A, P, C being Subset of AS
for o, a, b, c, a', b', c' being Element of the carrier of AS st o in A & o in P & o in C & o <> a & o <> b & o <> c & a in A & a' in A & b in P & b' in P & c in C & c' in C & A is_line & P is_line & C is_line & A <> P & A <> C & a,b // a',b' & a,c // a',c' & ( o = a' or a = a' ) holds
b,c // b',c'

proof end;

theorem :: AFPROJ:51

for AS being AffinSpace st IncProjSp_of AS is Desarguesian holds
AS is Desarguesian

proof end;

theorem :: AFPROJ:52

for AS being AffinSpace st IncProjSp_of AS is Fanoian holds
AS is Fanoian

proof end;