let P1, P2, P3, P4 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 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 ; :: thesis: 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 ; :: thesis: ( (homography N) . P1 = Dir100 & (homography N) . P2 = Dir010 & (homography N) . P3 = Dir001 & (homography N) . P4 = Dir111 )

( (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 ; :: thesis: 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 ; :: thesis: ( (homography N) . P1 = Dir100 & (homography N) . P2 = Dir010 & (homography N) . P3 = Dir001 & (homography N) . P4 = Dir111 )

now :: thesis: ( Dir100 = (homography (N2 * N1)) . P1 & Dir010 = (homography (N2 * N1)) . P2 & Dir001 = (homography (N2 * N1)) . P3 & Dir111 = (homography (N2 * N1)) . P4 )

hence
( (homography N) . P1 = Dir100 & (homography N) . P2 = Dir010 & (homography N) . P3 = Dir001 & (homography N) . P4 = Dir111 )
; :: thesis: verumthus Dir100 =
(homography N2) . ((homography N1) . P1)
by A5, Th21

.= (homography (N2 * N1)) . P1 by Th14 ; :: thesis: ( Dir010 = (homography (N2 * N1)) . P2 & Dir001 = (homography (N2 * N1)) . P3 & Dir111 = (homography (N2 * N1)) . P4 )

thus Dir010 = (homography N2) . ((homography N1) . P2) by A6, Th21

.= (homography (N2 * N1)) . P2 by Th14 ; :: thesis: ( Dir001 = (homography (N2 * N1)) . P3 & Dir111 = (homography (N2 * N1)) . P4 )

thus Dir001 = (homography N2) . ((homography N1) . P3) by A7, Th21

.= (homography (N2 * N1)) . P3 by Th14 ; :: thesis: Dir111 = (homography (N2 * N1)) . P4

thus Dir111 = (homography N2) . ((homography N1) . P4) by A8

.= (homography (N2 * N1)) . P4 by Th14 ; :: thesis: verum

end;.= (homography (N2 * N1)) . P1 by Th14 ; :: thesis: ( Dir010 = (homography (N2 * N1)) . P2 & Dir001 = (homography (N2 * N1)) . P3 & Dir111 = (homography (N2 * N1)) . P4 )

thus Dir010 = (homography N2) . ((homography N1) . P2) by A6, Th21

.= (homography (N2 * N1)) . P2 by Th14 ; :: thesis: ( Dir001 = (homography (N2 * N1)) . P3 & Dir111 = (homography (N2 * N1)) . P4 )

thus Dir001 = (homography N2) . ((homography N1) . P3) by A7, Th21

.= (homography (N2 * N1)) . P3 by Th14 ; :: thesis: Dir111 = (homography (N2 * N1)) . P4

thus Dir111 = (homography N2) . ((homography N1) . P4) by A8

.= (homography (N2 * N1)) . P4 by Th14 ; :: thesis: verum