let N1, N2 be invertible Matrix of 3,F_Real; :: thesis: for l being Element of the Lines of (IncProjSp_of real_projective_plane) holds (line_homography N1) . ((line_homography N2) . l) = (line_homography (N1 * N2)) . l
let l be Element of the Lines of (IncProjSp_of real_projective_plane); :: thesis: (line_homography N1) . ((line_homography N2) . l) = (line_homography (N1 * N2)) . l
reconsider l2 = (line_homography N2) . l as LINE of (IncProjSp_of real_projective_plane) ;
A1: l2 = { ((homography N2) . P) where P is POINT of (IncProjSp_of real_projective_plane) : P on l } by Def02;
A2: (line_homography N1) . ((line_homography N2) . l) = { ((homography N1) . P) where P is POINT of (IncProjSp_of real_projective_plane) : P on l2 } by Def02;
set X = { ((homography N1) . P) where P is POINT of (IncProjSp_of real_projective_plane) : P on l2 } ;
set Y = { ((homography (N1 * N2)) . P) where P is POINT of (IncProjSp_of real_projective_plane) : P on l } ;
{ ((homography N1) . P) where P is POINT of (IncProjSp_of real_projective_plane) : P on l2 } = { ((homography (N1 * N2)) . P) where P is POINT of (IncProjSp_of real_projective_plane) : P on l }
proof
A3: { ((homography N1) . P) where P is POINT of (IncProjSp_of real_projective_plane) : P on l2 } c= { ((homography (N1 * N2)) . P) where P is POINT of (IncProjSp_of real_projective_plane) : P on l }
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { ((homography N1) . P) where P is POINT of (IncProjSp_of real_projective_plane) : P on l2 } or x in { ((homography (N1 * N2)) . P) where P is POINT of (IncProjSp_of real_projective_plane) : P on l } )
assume x in { ((homography N1) . P) where P is POINT of (IncProjSp_of real_projective_plane) : P on l2 } ; :: thesis: x in { ((homography (N1 * N2)) . P) where P is POINT of (IncProjSp_of real_projective_plane) : P on l }
then consider P being POINT of (IncProjSp_of real_projective_plane) such that
A4: x = (homography N1) . P and
A5: P on l2 ;
A6: P is Point of real_projective_plane by INCPROJ:3;
l2 is LINE of real_projective_plane by INCPROJ:4;
then P in { ((homography N2) . P) where P is POINT of (IncProjSp_of real_projective_plane) : P on l } by A6, A1, A5, INCPROJ:5;
then consider P2 being POINT of (IncProjSp_of real_projective_plane) such that
A7: P = (homography N2) . P2 and
A8: P2 on l ;
P2 is Point of real_projective_plane by INCPROJ:3;
then x = (homography (N1 * N2)) . P2 by A4, A7, ANPROJ_9:13;
hence x in { ((homography (N1 * N2)) . P) where P is POINT of (IncProjSp_of real_projective_plane) : P on l } by A8; :: thesis: verum
end;
{ ((homography (N1 * N2)) . P) where P is POINT of (IncProjSp_of real_projective_plane) : P on l } c= { ((homography N1) . P) where P is POINT of (IncProjSp_of real_projective_plane) : P on l2 }
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { ((homography (N1 * N2)) . P) where P is POINT of (IncProjSp_of real_projective_plane) : P on l } or x in { ((homography N1) . P) where P is POINT of (IncProjSp_of real_projective_plane) : P on l2 } )
assume x in { ((homography (N1 * N2)) . P) where P is POINT of (IncProjSp_of real_projective_plane) : P on l } ; :: thesis: x in { ((homography N1) . P) where P is POINT of (IncProjSp_of real_projective_plane) : P on l2 }
then consider P being POINT of (IncProjSp_of real_projective_plane) such that
A9: x = (homography (N1 * N2)) . P and
A10: P on l ;
A11: P is Point of real_projective_plane by INCPROJ:3;
P is Element of (ProjectiveSpace (TOP-REAL 3)) by INCPROJ:3;
then (homography N2) . P is Point of real_projective_plane by FUNCT_2:5;
then reconsider P2 = (homography N2) . P as POINT of (IncProjSp_of real_projective_plane) by INCPROJ:3;
hence x in { ((homography N1) . P) where P is POINT of (IncProjSp_of real_projective_plane) : P on l2 } ; :: thesis: verum
end;
hence { ((homography N1) . P) where P is POINT of (IncProjSp_of real_projective_plane) : P on l2 } = { ((homography (N1 * N2)) . P) where P is POINT of (IncProjSp_of real_projective_plane) : P on l } by A3; :: thesis: verum
end;
hence (line_homography N1) . ((line_homography N2) . l) = (line_homography (N1 * N2)) . l by A2, Def02; :: thesis: verum