defpred S1[ object , object ] means ex x being LINE of (IncProjSp_of real_projective_plane) st
( $1 = x & $2 = { ((homography N) . P) where P is POINT of (IncProjSp_of real_projective_plane) : P on x } );
A1:
for x being object st x in the Lines of (IncProjSp_of real_projective_plane) holds
ex y being object st
( y in the Lines of (IncProjSp_of real_projective_plane) & S1[x,y] )
proof
let x be
object ;
( x in the Lines of (IncProjSp_of real_projective_plane) implies ex y being object st
( y in the Lines of (IncProjSp_of real_projective_plane) & S1[x,y] ) )
assume
x in the
Lines of
(IncProjSp_of real_projective_plane)
;
ex y being object st
( y in the Lines of (IncProjSp_of real_projective_plane) & S1[x,y] )
then reconsider x9 =
x as
Element of the
Lines of
(IncProjSp_of real_projective_plane) ;
set y =
{ ((homography N) . P) where P is POINT of (IncProjSp_of real_projective_plane) : P on x9 } ;
consider p,
q being
Point of
real_projective_plane such that A2:
p <> q
and A3:
x9 = Line (
p,
q)
by COLLSP:def 7, INCPROJ:4;
reconsider p9 =
(homography N) . p,
q9 =
(homography N) . q as
Point of
real_projective_plane by FUNCT_2:5;
A4:
{ ((homography N) . P) where P is POINT of (IncProjSp_of real_projective_plane) : P on x9 } = Line (
p9,
q9)
proof
A5:
{ ((homography N) . P) where P is POINT of (IncProjSp_of real_projective_plane) : P on x9 } c= Line (
p9,
q9)
proof
let x be
object ;
TARSKI:def 3 ( not x in { ((homography N) . P) where P is POINT of (IncProjSp_of real_projective_plane) : P on x9 } or x in Line (p9,q9) )
assume
x in { ((homography N) . P) where P is POINT of (IncProjSp_of real_projective_plane) : P on x9 }
;
x in Line (p9,q9)
then consider Px being
POINT of
(IncProjSp_of real_projective_plane) such that A6:
x = (homography N) . Px
and A7:
Px on x9
;
reconsider Px =
Px as
Point of
real_projective_plane by INCPROJ:3;
x9 is
LINE of
real_projective_plane
by INCPROJ:4;
then A8:
Px in x9
by A7, INCPROJ:5;
reconsider p1 =
p,
q1 =
q,
r1 =
Px,
p2 =
p9,
q2 =
q9 as
Point of
(ProjectiveSpace (TOP-REAL 3)) ;
(homography N) . p1,
(homography N) . q1,
(homography N) . r1 are_collinear
by A8, A3, COLLSP:11, ANPROJ_8:102;
hence
x in Line (
p9,
q9)
by A6, COLLSP:11;
verum
end;
Line (
p9,
q9)
c= { ((homography N) . P) where P is POINT of (IncProjSp_of real_projective_plane) : P on x9 }
proof
let x be
object ;
TARSKI:def 3 ( not x in Line (p9,q9) or x in { ((homography N) . P) where P is POINT of (IncProjSp_of real_projective_plane) : P on x9 } )
assume
x in Line (
p9,
q9)
;
x in { ((homography N) . P) where P is POINT of (IncProjSp_of real_projective_plane) : P on x9 }
then
x in { p where p is Element of real_projective_plane : p9,q9,p are_collinear }
by COLLSP:def 5;
then consider x99 being
Element of
real_projective_plane such that A9:
x = x99
and A10:
p9,
q9,
x99 are_collinear
;
reconsider p1 =
p,
q1 =
q,
r1 =
x99,
p2 =
p9,
q2 =
q9 as
Point of
(ProjectiveSpace (TOP-REAL 3)) ;
reconsider r2 =
(homography (N ~)) . r1 as
Point of
(ProjectiveSpace (TOP-REAL 3)) ;
reconsider r3 =
r2 as
POINT of
(IncProjSp_of real_projective_plane) by INCPROJ:3;
A11:
r1 = (homography N) . r2
by ANPROJ_9:15;
A12:
x9 is
LINE of
real_projective_plane
by INCPROJ:4;
r2 in x9
by A3, A10, A11, ANPROJ_8:102, COLLSP:11;
then
r3 on x9
by A12, INCPROJ:5;
hence
x in { ((homography N) . P) where P is POINT of (IncProjSp_of real_projective_plane) : P on x9 }
by A11, A9;
verum
end;
hence
{ ((homography N) . P) where P is POINT of (IncProjSp_of real_projective_plane) : P on x9 } = Line (
p9,
q9)
by A5;
verum
end;
reconsider y9 =
Line (
p9,
q9) as
LINE of
real_projective_plane by A2, ANPROJ_9:16, COLLSP:def 7;
reconsider y =
y9 as
LINE of
(IncProjSp_of real_projective_plane) by INCPROJ:4;
y is
Element of the
Lines of
(IncProjSp_of real_projective_plane)
;
then reconsider y =
{ ((homography N) . P) where P is POINT of (IncProjSp_of real_projective_plane) : P on x9 } as
Element of the
Lines of
(IncProjSp_of real_projective_plane) by A4;
take
y
;
( y in the Lines of (IncProjSp_of real_projective_plane) & S1[x,y] )
thus
(
y in the
Lines of
(IncProjSp_of real_projective_plane) &
S1[
x,
y] )
;
verum
end;
consider f being Function of the Lines of (IncProjSp_of real_projective_plane), the Lines of (IncProjSp_of real_projective_plane) such that
A13:
for x being object st x in the Lines of (IncProjSp_of real_projective_plane) holds
S1[x,f . x]
from FUNCT_2:sch 1(A1);
for x being LINE of (IncProjSp_of real_projective_plane) holds f . x = { ((homography N) . P) where P is POINT of (IncProjSp_of real_projective_plane) : P on x }
hence
ex b1 being Function of the Lines of (IncProjSp_of real_projective_plane), the Lines of (IncProjSp_of real_projective_plane) st
for x being LINE of (IncProjSp_of real_projective_plane) holds b1 . x = { ((homography N) . P) where P is POINT of (IncProjSp_of real_projective_plane) : P on x }
; verum