let N1, N2 be invertible Matrix of 3,F_Real; :: thesis: for l being Element of the Lines of holds () . (() . l) = (line_homography (N1 * N2)) . l
let l be Element of the Lines of ; :: thesis: () . (() . l) = (line_homography (N1 * N2)) . l
reconsider l2 = () . l as LINE of ;
A1: l2 = { (() . P) where P is POINT of : P on l } by Def02;
A2: (line_homography N1) . (() . l) = { (() . P) where P is POINT of : P on l2 } by Def02;
set X = { (() . P) where P is POINT of : P on l2 } ;
set Y = { ((homography (N1 * N2)) . P) where P is POINT of : P on l } ;
{ ((homography N1) . P) where P is POINT of : P on l2 } = { ((homography (N1 * N2)) . P) where P is POINT of : P on l }
proof
A3: { ((homography N1) . P) where P is POINT of : P on l2 } c= { ((homography (N1 * N2)) . P) where P is POINT of : P on l }
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { (() . P) where P is POINT of : P on l2 } or x in { ((homography (N1 * N2)) . P) where P is POINT of : P on l } )
assume x in { (() . P) where P is POINT of : P on l2 } ; :: thesis: x in { ((homography (N1 * N2)) . P) where P is POINT of : P on l }
then consider P being POINT of such that
A4: x = () . 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 { (() . P) where P is POINT of : P on l } by ;
then consider P2 being POINT of such that
A7: P = () . P2 and
A8: P2 on l ;
P2 is Point of real_projective_plane by INCPROJ:3;
then x = (homography (N1 * N2)) . P2 by ;
hence x in { ((homography (N1 * N2)) . P) where P is POINT of : P on l } by A8; :: thesis: verum
end;
{ ((homography (N1 * N2)) . P) where P is POINT of : P on l } c= { (() . P) where P is POINT of : 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 : P on l } or x in { (() . P) where P is POINT of : P on l2 } )
assume x in { ((homography (N1 * N2)) . P) where P is POINT of : P on l } ; :: thesis: x in { (() . P) where P is POINT of : P on l2 }
then consider P being POINT of 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 () by INCPROJ:3;
then (homography N2) . P is Point of real_projective_plane by FUNCT_2:5;
then reconsider P2 = () . P as POINT of by INCPROJ:3;
now :: thesis: ( x = () . P2 & P2 on l2 )
thus x = () . P2 by ; :: thesis: P2 on l2
A12: P2 in l2 by ;
l2 is LINE of real_projective_plane by INCPROJ:4;
hence P2 on l2 by ; :: thesis: verum
end;
hence x in { (() . P) where P is POINT of : P on l2 } ; :: thesis: verum
end;
hence { ((homography N1) . P) where P is POINT of : P on l2 } = { ((homography (N1 * N2)) . P) where P is POINT of : P on l } by A3; :: thesis: verum
end;
hence (line_homography N1) . (() . l) = (line_homography (N1 * N2)) . l by ; :: thesis: verum