let P be Point of (ProjectiveSpace (TOP-REAL 3)); :: thesis: ( not Dir100 , Dir010 ,P are_collinear & not Dir100 , Dir001 ,P are_collinear & not Dir010 , Dir001 ,P are_collinear implies ex a, b, c being non zero Element of F_Real st
for N being invertible Matrix of 3,F_Real st N = <*<*a,0,0*>,<*0,b,0*>,<*0,0,c*>*> holds
(homography N) . P = Dir111 )
assume that
A1: not Dir100 , Dir010 ,P are_collinear and
A2: not Dir100 , Dir001 ,P are_collinear and
A3: not Dir010 , Dir001 ,P are_collinear ; :: thesis: ex a, b, c being non zero Element of F_Real st
for N being invertible Matrix of 3,F_Real st N = <*<*a,0,0*>,<*0,b,0*>,<*0,0,c*>*> holds
(homography N) . P = Dir111
consider a, b, c being non zero Element of F_Real such that
A4: P = Dir |[a,b,c]| by Th23, A1, A2, A3;
reconsider ia = 1 / a, ib = 1 / b, ic = 1 / c as Element of F_Real by XREAL_0:def 1;
( not ia is zero & not ib is zero & not ic is zero ) by XCMPLX_1:50;
then reconsider ia = ia, ib = ib, ic = ic as non zero Element of F_Real ;
take ia ; :: thesis: ex b, c being non zero Element of F_Real st
for N being invertible Matrix of 3,F_Real st N = <*<*ia,0,0*>,<*0,b,0*>,<*0,0,c*>*> holds
(homography N) . P = Dir111
take ib ; :: thesis: ex c being non zero Element of F_Real st
for N being invertible Matrix of 3,F_Real st N = <*<*ia,0,0*>,<*0,ib,0*>,<*0,0,c*>*> holds
(homography N) . P = Dir111
take ic ; :: thesis: for N being invertible Matrix of 3,F_Real st N = <*<*ia,0,0*>,<*0,ib,0*>,<*0,0,ic*>*> holds
(homography N) . P = Dir111
thus for N being invertible Matrix of 3,F_Real st N = <*<*ia,0,0*>,<*0,ib,0*>,<*0,0,ic*>*> holds
(homography N) . P = Dir111 by A4, Th24; :: thesis: verum