let P1, P2, P3, P4 be Point of (ProjectiveSpace (TOP-REAL 3)); ( not P1,P2,P3 are_collinear & not P1,P2,P4 are_collinear & not P1,P3,P4 are_collinear & not P2,P3,P4 are_collinear implies ex N being invertible Matrix of 3,F_Real st
( (homography N) . P1 = Dir100 & (homography N) . P2 = Dir010 & (homography N) . P3 = Dir001 & (homography N) . P4 = Dir111 ) )
assume that
A1:
not P1,P2,P3 are_collinear
and
A2:
not P1,P2,P4 are_collinear
and
A3:
not P1,P3,P4 are_collinear
and
A4:
not P2,P3,P4 are_collinear
; ex N being invertible Matrix of 3,F_Real st
( (homography N) . P1 = Dir100 & (homography N) . P2 = Dir010 & (homography N) . P3 = Dir001 & (homography N) . P4 = Dir111 )
consider N1 being invertible Matrix of 3,F_Real such that
A5:
(homography N1) . P1 = Dir100
and
A6:
(homography N1) . P2 = Dir010
and
A7:
(homography N1) . P3 = Dir001
by A1, Th20;
set Q1 = (homography N1) . P1;
set Q2 = (homography N1) . P2;
set Q3 = (homography N1) . P3;
set Q4 = (homography N1) . P4;
( not (homography N1) . P1,(homography N1) . P2,(homography N1) . P3 are_collinear & not (homography N1) . P1,(homography N1) . P2,(homography N1) . P4 are_collinear & not (homography N1) . P1,(homography N1) . P3,(homography N1) . P4 are_collinear & not (homography N1) . P2,(homography N1) . P3,(homography N1) . P4 are_collinear )
by A1, A2, A3, A4, ANPROJ_8:102;
then consider a, b, c being non zero Element of F_Real such that
A8:
for N2 being invertible Matrix of 3,F_Real st N2 = <*<*a,0,0*>,<*0,b,0*>,<*0,0,c*>*> holds
(homography N2) . ((homography N1) . P4) = Dir111
by A5, A6, A7, Th25;
reconsider N2 = <*<*a,0,0*>,<*0,b,0*>,<*0,0,c*>*> as invertible Matrix of 3,F_Real by Th10;
reconsider N = N2 * N1 as invertible Matrix of 3,F_Real ;
take
N
; ( (homography N) . P1 = Dir100 & (homography N) . P2 = Dir010 & (homography N) . P3 = Dir001 & (homography N) . P4 = Dir111 )
hence
( (homography N) . P1 = Dir100 & (homography N) . P2 = Dir010 & (homography N) . P3 = Dir001 & (homography N) . P4 = Dir111 )
; verum