let P1, P2, P3, P4, Q1, Q2, Q3, Q4 be Point of (ProjectiveSpace (TOP-REAL 3)); :: thesis: ( not P1,P2,P3 are_collinear & not P1,P2,P4 are_collinear & not P1,P3,P4 are_collinear & not P2,P3,P4 are_collinear & not Q1,Q2,Q3 are_collinear & not Q1,Q2,Q4 are_collinear & not Q1,Q3,Q4 are_collinear & not Q2,Q3,Q4 are_collinear implies ex N being invertible Matrix of 3,F_Real st
( (homography N) . P1 = Q1 & (homography N) . P2 = Q2 & (homography N) . P3 = Q3 & (homography N) . P4 = Q4 ) )
assume that
A1: ( not P1,P2,P3 are_collinear & not P1,P2,P4 are_collinear & not P1,P3,P4 are_collinear & not P2,P3,P4 are_collinear ) and
A2: ( not Q1,Q2,Q3 are_collinear & not Q1,Q2,Q4 are_collinear & not Q1,Q3,Q4 are_collinear & not Q2,Q3,Q4 are_collinear ) ; :: thesis: ex N being invertible Matrix of 3,F_Real st
( (homography N) . P1 = Q1 & (homography N) . P2 = Q2 & (homography N) . P3 = Q3 & (homography N) . P4 = Q4 )
consider N1 being invertible Matrix of 3,F_Real such that
A3: ( (homography N1) . P1 = Dir100 & (homography N1) . P2 = Dir010 & (homography N1) . P3 = Dir001 & (homography N1) . P4 = Dir111 ) by A1, Th26;
consider N2 being invertible Matrix of 3,F_Real such that
A4: ( (homography N2) . Q1 = Dir100 & (homography N2) . Q2 = Dir010 & (homography N2) . Q3 = Dir001 & (homography N2) . Q4 = Dir111 ) by A2, Th26;
reconsider N = (N2 ~) * N1 as invertible Matrix of 3,F_Real ;
take N ; :: thesis: ( (homography N) . P1 = Q1 & (homography N) . P2 = Q2 & (homography N) . P3 = Q3 & (homography N) . P4 = Q4 )
thus Q1 = (homography (N2 ~)) . ((homography N1) . P1) by A3, A4, Th16
.= (homography N) . P1 by Th14 ; :: thesis: ( (homography N) . P2 = Q2 & (homography N) . P3 = Q3 & (homography N) . P4 = Q4 )
thus Q2 = (homography (N2 ~)) . ((homography N1) . P2) by A3, A4, Th16
.= (homography N) . P2 by Th14 ; :: thesis: ( (homography N) . P3 = Q3 & (homography N) . P4 = Q4 )
thus Q3 = (homography (N2 ~)) . ((homography N1) . P3) by A3, A4, Th16
.= (homography N) . P3 by Th14 ; :: thesis: (homography N) . P4 = Q4
thus Q4 = (homography (N2 ~)) . ((homography N1) . P4) by A3, A4, Th16
.= (homography N) . P4 by Th14 ; :: thesis: verum