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 }

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

hence
(line_homography N1) . ((line_homography N2) . l) = (line_homography (N1 * N2)) . l
by A2, Def02; :: thesis: verum
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 }

end;proof

{ ((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 }
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;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

proof

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
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;

end;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;

now :: thesis: ( x = (homography N1) . P2 & P2 on l2 )

hence
x in { ((homography N1) . P) where P is POINT of (IncProjSp_of real_projective_plane) : P on l2 }
; :: thesis: verumthus
x = (homography N1) . P2
by A11, A9, ANPROJ_9:13; :: thesis: P2 on l2

A12: P2 in l2 by A10, A1;

l2 is LINE of real_projective_plane by INCPROJ:4;

hence P2 on l2 by A12, INCPROJ:5; :: thesis: verum

end;A12: P2 in l2 by A10, A1;

l2 is LINE of real_projective_plane by INCPROJ:4;

hence P2 on l2 by A12, INCPROJ:5; :: thesis: verum