:: by Henryk Oryszczyszyn and Krzysztof Pra\.zmowski

::

:: Received December 17, 1990

:: Copyright (c) 1990-2021 Association of Mizar Users

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 being_plane

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

X is being_plane

proof end;

theorem Th2: :: AFPROJ:2

for AS being AffinSpace

for X being Subset of AS st AS is AffinPlane & X is being_plane holds

X = the carrier of AS

for X being Subset of AS st AS is AffinPlane & X is being_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 being_plane & Y is being_plane holds

X = Y

for X, Y being Subset of AS st AS is AffinPlane & X is being_plane & Y is being_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 being_plane holds

AS is AffinPlane

for X being Subset of AS st X = the carrier of AS & X is being_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 being_line & K is being_line & X is being_plane & Y is being_plane holds

X '||' Y

for A, K, X, Y being Subset of AS st not A // K & A '||' X & A '||' Y & K '||' X & K '||' Y & A is being_line & K is being_line & X is being_plane & Y is being_plane holds

X '||' Y

proof end;

theorem :: AFPROJ:6

for AS being AffinSpace

for A, X, Y being Subset of AS st X is being_plane & A '||' X & X '||' Y holds

A '||' Y by AFF_4:59, AFF_4:60;

for A, X, Y being Subset of AS st X is being_plane & A '||' X & X '||' Y holds

A '||' Y by AFF_4:59, AFF_4:60;

:: Next we distinguish two sets, one consisting of the lines, the second

:: consisting of the planes of a given affine space and we consider two

:: equivalence relations defined on each of these sets; theses relations

:: are in fact the relation of parallelity restricted to suitable area.

:: Their equivalence classes are called directions (of lines and planes,

:: respectively); they are intended to be considered as new objects which

:: extend the given affine space to a projective space.

:: consisting of the planes of a given affine space and we consider two

:: equivalence relations defined on each of these sets; theses relations

:: are in fact the relation of parallelity restricted to suitable area.

:: Their equivalence classes are called directions (of lines and planes,

:: respectively); they are intended to be considered as new objects which

:: extend the given affine space to a projective space.

definition

let AS be AffinSpace;

{ A where A is Subset of AS : A is being_line } is Subset-Family of AS

end;
func AfLines AS -> Subset-Family of AS equals :: AFPROJ:def 1

{ A where A is Subset of AS : A is being_line } ;

coherence { A where A is Subset of AS : A is being_line } ;

{ A where A is Subset of AS : A is being_line } is Subset-Family of AS

proof end;

:: deftheorem defines AfLines AFPROJ:def 1 :

for AS being AffinSpace holds AfLines AS = { A where A is Subset of AS : A is being_line } ;

for AS being AffinSpace holds AfLines AS = { A where A is Subset of AS : A is being_line } ;

definition

let AS be AffinSpace;

{ A where A is Subset of AS : A is being_plane } is Subset-Family of AS

end;
func AfPlanes AS -> Subset-Family of AS equals :: AFPROJ:def 2

{ A where A is Subset of AS : A is being_plane } ;

coherence { A where A is Subset of AS : A is being_plane } ;

{ A where A is Subset of AS : A is being_plane } is Subset-Family of AS

proof end;

:: deftheorem defines AfPlanes AFPROJ:def 2 :

for AS being AffinSpace holds AfPlanes AS = { A where A is Subset of AS : A is being_plane } ;

for AS being AffinSpace holds AfPlanes AS = { A where A is Subset of AS : A is being_plane } ;

theorem :: 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 being_line ) ) ;

for x being set holds

( x in AfLines AS iff ex X being Subset of AS st

( x = X & X is being_line ) ) ;

theorem :: 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 being_plane ) ) ;

for x being set holds

( x in AfPlanes AS iff ex X being Subset of AS st

( x = X & X is being_plane ) ) ;

definition

let AS be AffinSpace;

{ [K,M] where K, M is Subset of AS : ( K is being_line & M is being_line & K '||' M ) } is Equivalence_Relation of (AfLines AS)

end;
func LinesParallelity AS -> Equivalence_Relation of (AfLines AS) equals :: AFPROJ:def 3

{ [K,M] where K, M is Subset of AS : ( K is being_line & M is being_line & K '||' M ) } ;

coherence { [K,M] where K, M is Subset of AS : ( K is being_line & M is being_line & K '||' M ) } ;

{ [K,M] where K, M is Subset of AS : ( K is being_line & M is being_line & K '||' M ) } is Equivalence_Relation of (AfLines AS)

proof end;

:: deftheorem defines LinesParallelity AFPROJ:def 3 :

for AS being AffinSpace holds LinesParallelity AS = { [K,M] where K, M is Subset of AS : ( K is being_line & M is being_line & K '||' M ) } ;

for AS being AffinSpace holds LinesParallelity AS = { [K,M] where K, M is Subset of AS : ( K is being_line & M is being_line & K '||' M ) } ;

definition

let AS be AffinSpace;

{ [X,Y] where X, Y is Subset of AS : ( X is being_plane & Y is being_plane & X '||' Y ) } is Equivalence_Relation of (AfPlanes AS)

end;
func PlanesParallelity AS -> Equivalence_Relation of (AfPlanes AS) equals :: AFPROJ:def 4

{ [X,Y] where X, Y is Subset of AS : ( X is being_plane & Y is being_plane & X '||' Y ) } ;

coherence { [X,Y] where X, Y is Subset of AS : ( X is being_plane & Y is being_plane & X '||' Y ) } ;

{ [X,Y] where X, Y is Subset of AS : ( X is being_plane & Y is being_plane & X '||' Y ) } is Equivalence_Relation of (AfPlanes AS)

proof end;

:: deftheorem defines PlanesParallelity AFPROJ:def 4 :

for AS being AffinSpace holds PlanesParallelity AS = { [X,Y] where X, Y is Subset of AS : ( X is being_plane & Y is being_plane & X '||' Y ) } ;

for AS being AffinSpace holds PlanesParallelity AS = { [X,Y] where X, Y is Subset of AS : ( X is being_plane & Y is being_plane & X '||' Y ) } ;

definition

let AS be AffinSpace;

let X be Subset of AS;

correctness

coherence

Class ((LinesParallelity AS),X) is Subset of (AfLines AS);

;

end;
let X be Subset of AS;

correctness

coherence

Class ((LinesParallelity AS),X) is Subset of (AfLines AS);

;

:: deftheorem defines LDir AFPROJ:def 5 :

for AS being AffinSpace

for X being Subset of AS holds LDir X = Class ((LinesParallelity AS),X);

for AS being AffinSpace

for X being Subset of AS holds LDir X = Class ((LinesParallelity AS),X);

definition

let AS be AffinSpace;

let X be Subset of AS;

correctness

coherence

Class ((PlanesParallelity AS),X) is Subset of (AfPlanes AS);

;

end;
let X be Subset of AS;

correctness

coherence

Class ((PlanesParallelity AS),X) is Subset of (AfPlanes AS);

;

:: deftheorem defines PDir AFPROJ:def 6 :

for AS being AffinSpace

for X being Subset of AS holds PDir X = Class ((PlanesParallelity AS),X);

for AS being AffinSpace

for X being Subset of AS holds PDir X = Class ((PlanesParallelity AS),X);

theorem Th9: :: AFPROJ:9

for AS being AffinSpace

for X being Subset of AS st X is being_line holds

for x being set holds

( x in LDir X iff ex Y being Subset of AS st

( x = Y & Y is being_line & X '||' Y ) )

for X being Subset of AS st X is being_line holds

for x being set holds

( x in LDir X iff ex Y being Subset of AS st

( x = Y & Y is being_line & X '||' Y ) )

proof end;

theorem Th10: :: AFPROJ:10

for AS being AffinSpace

for X being Subset of AS st X is being_plane holds

for x being set holds

( x in PDir X iff ex Y being Subset of AS st

( x = Y & Y is being_plane & X '||' Y ) )

for X being Subset of AS st X is being_plane holds

for x being set holds

( x in PDir X iff ex Y being Subset of AS st

( x = Y & Y is being_plane & X '||' Y ) )

proof end;

theorem Th11: :: AFPROJ:11

for AS being AffinSpace

for X, Y being Subset of AS st X is being_line & Y is being_line holds

( LDir X = LDir Y iff X // Y )

for X, Y being Subset of AS st X is being_line & Y is being_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 being_line & Y is being_line holds

( LDir X = LDir Y iff X '||' Y )

for X, Y being Subset of AS st X is being_line & Y is being_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 being_plane & Y is being_plane holds

( PDir X = PDir Y iff X '||' Y )

for X, Y being Subset of AS st X is being_plane & Y is being_plane holds

( PDir X = PDir Y iff X '||' Y )

proof end;

definition
end;

:: deftheorem defines Dir_of_Lines AFPROJ:def 7 :

for AS being AffinSpace holds Dir_of_Lines AS = Class (LinesParallelity AS);

for AS being AffinSpace holds Dir_of_Lines AS = Class (LinesParallelity AS);

definition
end;

:: deftheorem defines Dir_of_Planes AFPROJ:def 8 :

for AS being AffinSpace holds Dir_of_Planes AS = Class (PlanesParallelity AS);

for AS being AffinSpace holds Dir_of_Planes AS = Class (PlanesParallelity AS);

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 being_line ) )

for x being set holds

( x in Dir_of_Lines AS iff ex X being Subset of AS st

( x = LDir X & X is being_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 being_plane ) )

for x being set holds

( x in Dir_of_Planes AS iff ex X being Subset of AS st

( x = PDir X & X is being_plane ) )

proof end;

:: The point is to guarantee that the classes of new objects consist of really

:: new objects. Clearly the set of directions of lines and the set of affine

:: points do not intersect. However we cannot claim, in general, that the set

:: of affine lines and the set of directions of planes do not intersect; this

:: is evidently true only in the case of affine planes. Therefore we have to

:: modify (slightly) a construction of the set of lines of the projective

:: closure of affine space, when compared with (naive) intuitions.

:: new objects. Clearly the set of directions of lines and the set of affine

:: points do not intersect. However we cannot claim, in general, that the set

:: of affine lines and the set of directions of planes do not intersect; this

:: is evidently true only in the case of affine planes. Therefore we have to

:: modify (slightly) a construction of the set of lines of the projective

:: closure of affine space, when compared with (naive) intuitions.

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 being_line ) )

for x being set holds

( x in [:(AfLines AS),{1}:] iff ex X being Subset of AS st

( x = [X,1] & X is being_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 being_plane ) )

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 being_plane ) )

proof end;

definition

let AS be AffinSpace;

coherence

the carrier of AS \/ (Dir_of_Lines AS) is non empty set ;

;

end;
func ProjectivePoints AS -> non empty set equals :: AFPROJ:def 9

the carrier of AS \/ (Dir_of_Lines AS);

correctness the carrier of AS \/ (Dir_of_Lines AS);

coherence

the carrier of AS \/ (Dir_of_Lines AS) is non empty set ;

;

:: deftheorem defines ProjectivePoints AFPROJ:def 9 :

for AS being AffinSpace holds ProjectivePoints AS = the carrier of AS \/ (Dir_of_Lines AS);

for AS being AffinSpace holds ProjectivePoints AS = the carrier of AS \/ (Dir_of_Lines AS);

definition

let AS be AffinSpace;

[:(AfLines AS),{1}:] \/ [:(Dir_of_Planes AS),{2}:] is non empty set ;

end;
func ProjectiveLines AS -> non empty set equals :: AFPROJ:def 10

[:(AfLines AS),{1}:] \/ [:(Dir_of_Planes AS),{2}:];

coherence [:(AfLines AS),{1}:] \/ [:(Dir_of_Planes AS),{2}:];

[:(AfLines AS),{1}:] \/ [:(Dir_of_Planes AS),{2}:] is non empty set ;

:: deftheorem defines ProjectiveLines AFPROJ:def 10 :

for AS being AffinSpace holds ProjectiveLines AS = [:(AfLines AS),{1}:] \/ [:(Dir_of_Planes AS),{2}:];

for AS being AffinSpace holds ProjectiveLines AS = [:(AfLines AS),{1}:] \/ [:(Dir_of_Planes AS),{2}:];

definition

let AS be AffinSpace;

ex b_{1} being Relation of (ProjectivePoints AS),(ProjectiveLines AS) st

for x, y being object holds

( [x,y] in b_{1} iff ( ex K being Subset of AS st

( K is being_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 being_line & X is being_plane & x = LDir K & y = [(PDir X),2] & K '||' X ) ) )

for b_{1}, b_{2} being Relation of (ProjectivePoints AS),(ProjectiveLines AS) st ( for x, y being object holds

( [x,y] in b_{1} iff ( ex K being Subset of AS st

( K is being_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 being_line & X is being_plane & x = LDir K & y = [(PDir X),2] & K '||' X ) ) ) ) & ( for x, y being object holds

( [x,y] in b_{2} iff ( ex K being Subset of AS st

( K is being_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 being_line & X is being_plane & x = LDir K & y = [(PDir X),2] & K '||' X ) ) ) ) holds

b_{1} = b_{2}

end;
func Proj_Inc AS -> Relation of (ProjectivePoints AS),(ProjectiveLines AS) means :Def11: :: AFPROJ:def 11

for x, y being object holds

( [x,y] in it iff ( ex K being Subset of AS st

( K is being_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 being_line & X is being_plane & x = LDir K & y = [(PDir X),2] & K '||' X ) ) );

existence for x, y being object holds

( [x,y] in it iff ( ex K being Subset of AS st

( K is being_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 being_line & X is being_plane & x = LDir K & y = [(PDir X),2] & K '||' X ) ) );

ex b

for x, y being object holds

( [x,y] in b

( K is being_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 being_line & X is being_plane & x = LDir K & y = [(PDir X),2] & K '||' X ) ) )

proof end;

uniqueness for b

( [x,y] in b

( K is being_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 being_line & X is being_plane & x = LDir K & y = [(PDir X),2] & K '||' X ) ) ) ) & ( for x, y being object holds

( [x,y] in b

( K is being_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 being_line & X is being_plane & x = LDir K & y = [(PDir X),2] & K '||' X ) ) ) ) holds

b

proof end;

:: deftheorem Def11 defines Proj_Inc AFPROJ:def 11 :

for AS being AffinSpace

for b_{2} being Relation of (ProjectivePoints AS),(ProjectiveLines AS) holds

( b_{2} = Proj_Inc AS iff for x, y being object holds

( [x,y] in b_{2} iff ( ex K being Subset of AS st

( K is being_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 being_line & X is being_plane & x = LDir K & y = [(PDir X),2] & K '||' X ) ) ) );

for AS being AffinSpace

for b

( b

( [x,y] in b

( K is being_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 being_line & X is being_plane & x = LDir K & y = [(PDir X),2] & K '||' X ) ) ) );

definition

let AS be AffinSpace;

ex b_{1} being Relation of (Dir_of_Lines AS),(Dir_of_Planes AS) st

for x, y being object holds

( [x,y] in b_{1} iff ex A, X being Subset of AS st

( x = LDir A & y = PDir X & A is being_line & X is being_plane & A '||' X ) )

for b_{1}, b_{2} being Relation of (Dir_of_Lines AS),(Dir_of_Planes AS) st ( for x, y being object holds

( [x,y] in b_{1} iff ex A, X being Subset of AS st

( x = LDir A & y = PDir X & A is being_line & X is being_plane & A '||' X ) ) ) & ( for x, y being object holds

( [x,y] in b_{2} iff ex A, X being Subset of AS st

( x = LDir A & y = PDir X & A is being_line & X is being_plane & A '||' X ) ) ) holds

b_{1} = b_{2}

end;
func Inc_of_Dir AS -> Relation of (Dir_of_Lines AS),(Dir_of_Planes AS) means :Def12: :: AFPROJ:def 12

for x, y being object holds

( [x,y] in it iff ex A, X being Subset of AS st

( x = LDir A & y = PDir X & A is being_line & X is being_plane & A '||' X ) );

existence for x, y being object holds

( [x,y] in it iff ex A, X being Subset of AS st

( x = LDir A & y = PDir X & A is being_line & X is being_plane & A '||' X ) );

ex b

for x, y being object holds

( [x,y] in b

( x = LDir A & y = PDir X & A is being_line & X is being_plane & A '||' X ) )

proof end;

uniqueness for b

( [x,y] in b

( x = LDir A & y = PDir X & A is being_line & X is being_plane & A '||' X ) ) ) & ( for x, y being object holds

( [x,y] in b

( x = LDir A & y = PDir X & A is being_line & X is being_plane & A '||' X ) ) ) holds

b

proof end;

:: deftheorem Def12 defines Inc_of_Dir AFPROJ:def 12 :

for AS being AffinSpace

for b_{2} being Relation of (Dir_of_Lines AS),(Dir_of_Planes AS) holds

( b_{2} = Inc_of_Dir AS iff for x, y being object holds

( [x,y] in b_{2} iff ex A, X being Subset of AS st

( x = LDir A & y = PDir X & A is being_line & X is being_plane & A '||' X ) ) );

for AS being AffinSpace

for b

( b

( [x,y] in b

( x = LDir A & y = PDir X & A is being_line & X is being_plane & A '||' X ) ) );

definition

let AS be AffinSpace;

coherence

IncProjStr(# (ProjectivePoints AS),(ProjectiveLines AS),(Proj_Inc AS) #) is strict IncProjStr ;

;

end;
func IncProjSp_of AS -> strict IncProjStr equals :: AFPROJ:def 13

IncProjStr(# (ProjectivePoints AS),(ProjectiveLines AS),(Proj_Inc AS) #);

correctness IncProjStr(# (ProjectivePoints AS),(ProjectiveLines AS),(Proj_Inc AS) #);

coherence

IncProjStr(# (ProjectivePoints AS),(ProjectiveLines AS),(Proj_Inc AS) #) is strict IncProjStr ;

;

:: deftheorem defines IncProjSp_of AFPROJ:def 13 :

for AS being AffinSpace holds IncProjSp_of AS = IncProjStr(# (ProjectivePoints AS),(ProjectiveLines AS),(Proj_Inc AS) #);

for AS being AffinSpace holds IncProjSp_of AS = IncProjStr(# (ProjectivePoints AS),(ProjectiveLines AS),(Proj_Inc AS) #);

definition

let AS be AffinSpace;

coherence

IncProjStr(# (Dir_of_Lines AS),(Dir_of_Planes AS),(Inc_of_Dir AS) #) is strict IncProjStr ;

;

end;
func ProjHorizon AS -> strict IncProjStr equals :: AFPROJ:def 14

IncProjStr(# (Dir_of_Lines AS),(Dir_of_Planes AS),(Inc_of_Dir AS) #);

correctness IncProjStr(# (Dir_of_Lines AS),(Dir_of_Planes AS),(Inc_of_Dir AS) #);

coherence

IncProjStr(# (Dir_of_Lines AS),(Dir_of_Planes AS),(Inc_of_Dir AS) #) is strict IncProjStr ;

;

:: deftheorem defines ProjHorizon AFPROJ:def 14 :

for AS being AffinSpace holds ProjHorizon AS = IncProjStr(# (Dir_of_Lines AS),(Dir_of_Planes AS),(Inc_of_Dir AS) #);

for AS being AffinSpace holds ProjHorizon AS = IncProjStr(# (Dir_of_Lines AS),(Dir_of_Planes AS),(Inc_of_Dir AS) #);

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 being_line ) ) )

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 being_line ) ) )

proof end;

theorem :: 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 being_line ) ) by Th14;

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 being_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)

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 being_line ) or ( x = [(PDir X),2] & X is being_plane ) ) )

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 being_line ) or ( x = [(PDir X),2] & X is being_plane ) ) )

proof end;

theorem :: 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 being_plane ) ) by Th15;

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 being_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)

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 being_line & x in X ) )

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 being_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 holds

not a on A

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 holds

not a on A

proof end;

theorem Th28: :: AFPROJ:28

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 a = LDir Y & [X,1] = A & Y is being_line & X is being_line holds

( a on A iff Y '||' X )

for X, Y 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 being_line & X is being_line holds

( a on A iff Y '||' X )

proof end;

theorem Th29: :: AFPROJ:29

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 a = LDir Y & A = [(PDir X),2] & Y is being_line & X is being_plane holds

( a on A iff Y '||' X )

for X, Y 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 being_line & X is being_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 being_line & a = LDir X & A = [X,1] holds

a on A

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 being_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 being_line & Y is being_plane & X c= Y & a = LDir X & A = [(PDir Y),2] holds

a on A

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 being_line & Y is being_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 X, Y, X9 being Subset of AS

for a being POINT of (IncProjSp_of AS)

for A being LINE of (IncProjSp_of AS) st Y is being_plane & X c= Y & X9 // X & a = LDir X9 & A = [(PDir Y),2] holds

a on A

for X, Y, X9 being Subset of AS

for a being POINT of (IncProjSp_of AS)

for A being LINE of (IncProjSp_of AS) st Y is being_plane & X c= Y & X9 // X & a = LDir X9 & 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 being_plane & a on A holds

not a is Element of AS by Th27;

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 being_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 being_line & p on A & p is not Element of AS holds

p = LDir X

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 being_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 a, p being POINT of (IncProjSp_of AS)

for A being LINE of (IncProjSp_of AS) st A = [X,1] & X is being_line & p on A & a on A & a <> p & p is not Element of AS holds

a is Element of AS

for X being Subset of AS

for a, p being POINT of (IncProjSp_of AS)

for A being LINE of (IncProjSp_of AS) st A = [X,1] & X is being_line & p on A & a on A & a <> p & p is not Element 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 being_line & Y is being_plane holds

( a on A iff X '||' Y )

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 being_line & Y is being_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 a9 being Element of the Points of (IncProjSp_of AS)

for A being Element of the Lines of (ProjHorizon AS)

for A9 being LINE of (IncProjSp_of AS) st a9 = a & A9 = [A,2] holds

( a on A iff a9 on A9 )

for a being Element of the Points of (ProjHorizon AS)

for a9 being Element of the Points of (IncProjSp_of AS)

for A being Element of the Lines of (ProjHorizon AS)

for A9 being LINE of (IncProjSp_of AS) st a9 = a & A9 = [A,2] holds

( a on A iff a9 on A9 )

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

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 )

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 )

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]

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)

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, Y, X9, Y9 being Subset of AS

for b, c being POINT of (IncProjSp_of AS)

for A, K, M being LINE of (IncProjSp_of AS) st X is being_line & X9 is being_line & Y is being_plane & X c= Y & X9 c= Y & A = [X,1] & K = [X9,1] & b on A & c on K & b on M & c on M & b <> c & M = [Y9,1] & Y9 is being_line holds

Y9 c= Y

proof end;

Lm8: for AS being AffinSpace

for X, Y, X9, Y9 being Subset of AS

for b, c being POINT of (IncProjSp_of AS)

for A, K, M being LINE of (IncProjSp_of AS) st X is being_line & X9 is being_line & Y is being_plane & X c= Y & X9 c= Y & A = [X,1] & K = [X9,1] & b on A & c on K & b on M & c on M & b <> c & M = [(PDir Y9),2] & Y9 is being_plane holds

( Y9 '||' Y & Y '||' Y9 )

proof end;

theorem Th43: :: AFPROJ:43

for AS being AffinSpace

for X, Y, X9 being Subset of AS

for P, Q being LINE of (IncProjSp_of AS) st Y is being_plane & X is being_line & X9 is being_line & X c= Y & X9 c= Y & P = [X,1] & Q = [X9,1] holds

ex q being POINT of (IncProjSp_of AS) st

( q on P & q on Q )

for X, Y, X9 being Subset of AS

for P, Q being LINE of (IncProjSp_of AS) st Y is being_plane & X is being_line & X9 is being_line & X c= Y & X9 c= Y & P = [X,1] & Q = [X9,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 )

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;

correctness

coherence

( IncProjSp_of AS is partial & IncProjSp_of AS is linear & IncProjSp_of AS is up-2-dimensional & IncProjSp_of AS is up-3-rank & IncProjSp_of AS is Vebleian );

end;
correctness

coherence

( IncProjSp_of AS is partial & IncProjSp_of AS is linear & IncProjSp_of AS is up-2-dimensional & IncProjSp_of AS is up-3-rank & IncProjSp_of AS is Vebleian );

proof end;

registration
end;

registration
end;

theorem Th48: :: AFPROJ:48

for AS being AffinSpace

for M, N being Subset of AS

for o, a, b, c, a9, b9, c9 being Element of AS st M is being_line & N is being_line & M <> N & o in M & o in N & o <> b & o <> b9 & o <> c9 & b in M & c in M & a9 in N & b9 in N & c9 in N & a,b9 // b,a9 & b,c9 // c,b9 & ( a = b or b = c or a = c ) holds

a,c9 // c,a9

for M, N being Subset of AS

for o, a, b, c, a9, b9, c9 being Element of AS st M is being_line & N is being_line & M <> N & o in M & o in N & o <> b & o <> b9 & o <> c9 & b in M & c in M & a9 in N & b9 in N & c9 in N & a,b9 // b,a9 & b,c9 // c,b9 & ( a = b or b = c or a = c ) holds

a,c9 // c,a9

proof end;

theorem Th50: :: AFPROJ:50

for AS being AffinSpace

for A, P, C being Subset of AS

for o, a, b, c, a9, b9, c9 being Element of AS st o in A & o in P & o in C & o <> a & o <> b & o <> c & a in A & b in P & b9 in P & c in C & c9 in C & A is being_line & P is being_line & C is being_line & A <> P & A <> C & a,b // a9,b9 & a,c // a9,c9 & ( o = a9 or a = a9 ) holds

b,c // b9,c9

for A, P, C being Subset of AS

for o, a, b, c, a9, b9, c9 being Element of AS st o in A & o in P & o in C & o <> a & o <> b & o <> c & a in A & b in P & b9 in P & c in C & c9 in C & A is being_line & P is being_line & C is being_line & A <> P & A <> C & a,b // a9,b9 & a,c // a9,c9 & ( o = a9 or a = a9 ) holds

b,c // b9,c9

proof end;

:: the projective closure of an affine space. We begin with some evident

:: properties of planes in affine planes.