let l be Element of the Lines of (IncProjSp_of real_projective_plane); :: thesis: (line_homography (1. (F_Real,3))) . l = l

set X = { ((homography (1. (F_Real,3))) . P) where P is POINT of (IncProjSp_of real_projective_plane) : P on l } ;

A1: { ((homography (1. (F_Real,3))) . P) where P is POINT of (IncProjSp_of real_projective_plane) : P on l } c= l

set X = { ((homography (1. (F_Real,3))) . P) where P is POINT of (IncProjSp_of real_projective_plane) : P on l } ;

A1: { ((homography (1. (F_Real,3))) . P) where P is POINT of (IncProjSp_of real_projective_plane) : P on l } c= l

proof

l c= { ((homography (1. (F_Real,3))) . P) where P is POINT of (IncProjSp_of real_projective_plane) : P on l }
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { ((homography (1. (F_Real,3))) . P) where P is POINT of (IncProjSp_of real_projective_plane) : P on l } or x in l )

assume x in { ((homography (1. (F_Real,3))) . P) where P is POINT of (IncProjSp_of real_projective_plane) : P on l } ; :: thesis: x in l

then consider P being POINT of (IncProjSp_of real_projective_plane) such that

A2: x = (homography (1. (F_Real,3))) . P and

A3: P on l ;

A4: P is Point of real_projective_plane by INCPROJ:2;

then A5: x = P by A2, ANPROJ_9:14;

l is LINE of real_projective_plane by INCPROJ:4;

hence x in l by A4, A3, A5, INCPROJ:5; :: thesis: verum

end;assume x in { ((homography (1. (F_Real,3))) . P) where P is POINT of (IncProjSp_of real_projective_plane) : P on l } ; :: thesis: x in l

then consider P being POINT of (IncProjSp_of real_projective_plane) such that

A2: x = (homography (1. (F_Real,3))) . P and

A3: P on l ;

A4: P is Point of real_projective_plane by INCPROJ:2;

then A5: x = P by A2, ANPROJ_9:14;

l is LINE of real_projective_plane by INCPROJ:4;

hence x in l by A4, A3, A5, INCPROJ:5; :: thesis: verum

proof

hence
(line_homography (1. (F_Real,3))) . l = l
by A1, Def02; :: thesis: verum
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in l or x in { ((homography (1. (F_Real,3))) . P) where P is POINT of (IncProjSp_of real_projective_plane) : P on l } )

assume A6: x in l ; :: thesis: x in { ((homography (1. (F_Real,3))) . P) where P is POINT of (IncProjSp_of real_projective_plane) : P on l }

A7: l is LINE of real_projective_plane by INCPROJ:4;

l is Subset of real_projective_plane by INCPROJ:4;

then reconsider x9 = x as Point of real_projective_plane by A6;

reconsider l9 = l as LINE of (IncProjSp_of real_projective_plane) ;

reconsider x99 = x9 as POINT of (IncProjSp_of real_projective_plane) by INCPROJ:3;

A8: x99 on l by A7, A6, INCPROJ:5;

(homography (1. (F_Real,3))) . x99 = x99 by ANPROJ_9:14;

hence x in { ((homography (1. (F_Real,3))) . P) where P is POINT of (IncProjSp_of real_projective_plane) : P on l } by A8; :: thesis: verum

end;assume A6: x in l ; :: thesis: x in { ((homography (1. (F_Real,3))) . P) where P is POINT of (IncProjSp_of real_projective_plane) : P on l }

A7: l is LINE of real_projective_plane by INCPROJ:4;

l is Subset of real_projective_plane by INCPROJ:4;

then reconsider x9 = x as Point of real_projective_plane by A6;

reconsider l9 = l as LINE of (IncProjSp_of real_projective_plane) ;

reconsider x99 = x9 as POINT of (IncProjSp_of real_projective_plane) by INCPROJ:3;

A8: x99 on l by A7, A6, INCPROJ:5;

(homography (1. (F_Real,3))) . x99 = x99 by ANPROJ_9:14;

hence x in { ((homography (1. (F_Real,3))) . P) where P is POINT of (IncProjSp_of real_projective_plane) : P on l } by A8; :: thesis: verum