let P1, P2, P3 be Point of (); :: thesis: ( not P1,P2,P3 are_collinear implies ex N being invertible Matrix of 3,F_Real st
( () . P1 = Dir100 & () . P2 = Dir010 & () . P3 = Dir001 ) )

assume A1: not P1,P2,P3 are_collinear ; :: thesis: ex N being invertible Matrix of 3,F_Real st
( () . P1 = Dir100 & () . P2 = Dir010 & () . P3 = Dir001 )

consider u1 being Element of () such that
A2: not u1 is zero and
A3: P1 = Dir u1 by ANPROJ_1:26;
consider u2 being Element of () such that
A4: not u2 is zero and
A5: P2 = Dir u2 by ANPROJ_1:26;
consider u3 being Element of () such that
A6: not u3 is zero and
A7: P3 = Dir u3 by ANPROJ_1:26;
A8: |{u1,u2,u3}| <> 0 by ;
reconsider pf = u1, qf = u2, rf = u3 as FinSequence of F_Real by RVSUM_1:145;
consider N being Matrix of 3,F_Real such that
A9: N is invertible and
A10: N * pf = F2M <e1> and
A11: N * qf = F2M <e2> and
A12: N * rf = F2M <e3> by ;
reconsider N = N as invertible Matrix of 3,F_Real by A9;
A13: ( len <e1> = 3 & len <e2> = 3 & len <e3> = 3 ) by EUCLID_8:50;
take N ; :: thesis: ( () . P1 = Dir100 & () . P2 = Dir010 & () . P3 = Dir001 )
thus (homography N) . P1 = Dir100 :: thesis: ( () . P2 = Dir010 & () . P3 = Dir001 )
proof
consider nu1, nv1 being Element of (), u1f being FinSequence of F_Real, p1 being FinSequence of 1 -tuples_on REAL such that
A14: P1 = Dir nu1 and
A15: not nu1 is zero and
A16: nu1 = u1f and
A17: p1 = N * u1f and
A18: nv1 = M2F p1 and
A19: not nv1 is zero and
A20: (homography N) . P1 = Dir nv1 by ANPROJ_8:def 4;
are_Prop u1,nu1 by ;
then consider a being Real such that
A21: a <> 0 and
A22: u1 = a * nu1 by ANPROJ_1:1;
reconsider b = 1 / a as Real ;
nu1 in TOP-REAL 3 ;
then A23: nu1 in REAL 3 by EUCLID:22;
width <*u1f*> = len nu1 by
.= 3 by ;
then A24: len (<*u1f*> @) = width <*u1f*> by MATRIX_0:29
.= len nu1 by
.= 3 by ;
A25: width N = len (<*u1f*> @) by ;
A26: len (N * u1f) = len (N * (<*u1f*> @)) by LAPLACE:def 9
.= len N by
.= 3 by MATRIX_0:24 ;
len <e1> = 3 by ;
then A27: F2M <e1> = <*<*()*>,<*()*>,<*()*>*> by ANPROJ_8:def 1;
reconsider s1 = u1f . 1, s2 = u1f . 2, s3 = u1f . 3 as Element of F_Real by XREAL_0:def 1;
reconsider t1 = u1 . 1, t2 = u1 . 2, t3 = u1 . 3 as Element of F_Real by XREAL_0:def 1;
A28: ( (N * pf) . 1 = <*()*> & (N * pf) . 2 = <*()*> & (N * pf) . 3 = <*()*> ) by ;
A29: ((N * pf) . 1) . 1 = |[1,0,0]| . 1 by
.= |[1,0,0]| `1 by EUCLID_5:def 1
.= 1 by EUCLID_5:2 ;
A30: ((N * pf) . 2) . 1 = |[1,0,0]| . 2 by
.= |[1,0,0]| `2 by EUCLID_5:def 2
.= 0 by EUCLID_5:2 ;
A31: ((N * pf) . 3) . 1 = |[1,0,0]| . 3 by
.= |[1,0,0]| `3 by EUCLID_5:def 3
.= 0 by EUCLID_5:2 ;
( p1 . 1 = <*((N * (<*u1f*> @)) * (1,1))*> & p1 . 2 = <*((N * (<*u1f*> @)) * (2,1))*> & p1 . 3 = <*((N * (<*u1f*> @)) * (3,1))*> ) by ;
then reconsider p111 = (p1 . 1) . 1, p121 = (p1 . 2) . 1, p131 = (p1 . 3) . 1 as Real ;
A32: ( p111 = b * ((Line (N,1)) "*" pf) & p121 = b * ((Line (N,2)) "*" pf) & p131 = b * ((Line (N,3)) "*" pf) ) by ;
A33: a * p1 = N * pf
proof
consider pp1, pp2, pp3 being Real such that
A34: pp1 = (p1 . 1) . 1 and
A35: pp2 = (p1 . 2) . 1 and
A36: pp3 = (p1 . 3) . 1 and
A37: a * p1 = <*<*(a * pp1)*>,<*(a * pp2)*>,<*(a * pp3)*>*> by ;
now :: thesis: ( len (N * pf) = 3 & (N * pf) . 1 = <*(a * pp1)*> & (N * pf) . 2 = <*(a * pp2)*> & (N * pf) . 3 = <*(a * pp3)*> )
thus len (N * pf) = 3 by ; :: thesis: ( (N * pf) . 1 = <*(a * pp1)*> & (N * pf) . 2 = <*(a * pp2)*> & (N * pf) . 3 = <*(a * pp3)*> )
thus (N * pf) . 1 = <*(a * pp1)*> :: thesis: ( (N * pf) . 2 = <*(a * pp2)*> & (N * pf) . 3 = <*(a * pp3)*> )
proof
(Line (N,1)) "*" pf = ((N * pf) . 1) . 1 by ;
then ( len ((N * pf) . 1) = 1 & ((N * pf) . 1) . 1 = a * p111 ) by ;
hence (N * pf) . 1 = <*(a * pp1)*> by ; :: thesis: verum
end;
thus (N * pf) . 2 = <*(a * pp2)*> :: thesis: (N * pf) . 3 = <*(a * pp3)*>
proof
(Line (N,2)) "*" pf = ((N * pf) . 2) . 1 by ;
hence (N * pf) . 2 = <*(a * pp2)*> by ; :: thesis: verum
end;
(Line (N,3)) "*" pf = ((N * pf) . 3) . 1 by ;
hence (N * pf) . 3 = <*(a * pp3)*> by ; :: thesis: verum
end;
hence a * p1 = N * pf by ; :: thesis: verum
end;
len <e1> = 3 by EUCLID_8:50;
then A38: <e1> = M2F () by ANPROJ_8:86
.= a * nv1 by ;
( not nv1 is zero & not a * nv1 is zero & are_Prop nv1,a * nv1 ) by ;
hence (homography N) . P1 = Dir100 by ; :: thesis: verum
end;
thus (homography N) . P2 = Dir010 :: thesis: () . P3 = Dir001
proof
consider nu2, nv2 being Element of (), u2f being FinSequence of F_Real, p2 being FinSequence of 1 -tuples_on REAL such that
A39: P2 = Dir nu2 and
A40: not nu2 is zero and
A41: nu2 = u2f and
A42: p2 = N * u2f and
A43: nv2 = M2F p2 and
A44: not nv2 is zero and
A45: (homography N) . P2 = Dir nv2 by ANPROJ_8:def 4;
are_Prop u2,nu2 by ;
then consider a being Real such that
A46: a <> 0 and
A47: u2 = a * nu2 by ANPROJ_1:1;
reconsider b = 1 / a as Real ;
nu2 in TOP-REAL 3 ;
then A48: nu2 in REAL 3 by EUCLID:22;
width <*u2f*> = len nu2 by
.= 3 by ;
then A49: len (<*u2f*> @) = width <*u2f*> by MATRIX_0:29
.= len nu2 by
.= 3 by ;
A50: width N = len (<*u2f*> @) by ;
A51: len (N * u2f) = len (N * (<*u2f*> @)) by LAPLACE:def 9
.= len N by
.= 3 by MATRIX_0:24 ;
len <e2> = 3 by ;
then A52: F2M <e2> = <*<*()*>,<*()*>,<*()*>*> by ANPROJ_8:def 1;
reconsider s1 = u2f . 1, s2 = u2f . 2, s3 = u2f . 3 as Element of F_Real by XREAL_0:def 1;
reconsider t1 = u2 . 1, t2 = u2 . 2, t3 = u2 . 3 as Element of F_Real by XREAL_0:def 1;
A53: ( (N * qf) . 1 = <*()*> & (N * qf) . 2 = <*()*> & (N * qf) . 3 = <*()*> ) by ;
A54: ((N * qf) . 1) . 1 = |[0,1,0]| . 1 by
.= |[0,1,0]| `1 by EUCLID_5:def 1
.= 0 by EUCLID_5:2 ;
A55: ((N * qf) . 2) . 1 = |[0,1,0]| . 2 by
.= |[0,1,0]| `2 by EUCLID_5:def 2
.= 1 by EUCLID_5:2 ;
A56: ((N * qf) . 3) . 1 = |[0,1,0]| . 3 by
.= |[0,1,0]| `3 by EUCLID_5:def 3
.= 0 by EUCLID_5:2 ;
( p2 . 1 = <*((N * (<*u2f*> @)) * (1,1))*> & p2 . 2 = <*((N * (<*u2f*> @)) * (2,1))*> & p2 . 3 = <*((N * (<*u2f*> @)) * (3,1))*> ) by ;
then reconsider p211 = (p2 . 1) . 1, p221 = (p2 . 2) . 1, p231 = (p2 . 3) . 1 as Real ;
A57: ( p211 = b * ((Line (N,1)) "*" qf) & p221 = b * ((Line (N,2)) "*" qf) & p231 = b * ((Line (N,3)) "*" qf) ) by ;
A58: a * p2 = N * qf
proof
consider pp1, pp2, pp3 being Real such that
A59: pp1 = (p2 . 1) . 1 and
A60: pp2 = (p2 . 2) . 1 and
A61: pp3 = (p2 . 3) . 1 and
A62: a * p2 = <*<*(a * pp1)*>,<*(a * pp2)*>,<*(a * pp3)*>*> by ;
now :: thesis: ( len (N * qf) = 3 & (N * qf) . 1 = <*(a * pp1)*> & (N * qf) . 2 = <*(a * pp2)*> & (N * qf) . 3 = <*(a * pp3)*> )
thus len (N * qf) = 3 by ; :: thesis: ( (N * qf) . 1 = <*(a * pp1)*> & (N * qf) . 2 = <*(a * pp2)*> & (N * qf) . 3 = <*(a * pp3)*> )
(Line (N,1)) "*" qf = ((N * qf) . 1) . 1 by ;
hence (N * qf) . 1 = <*(a * pp1)*> by ; :: thesis: ( (N * qf) . 2 = <*(a * pp2)*> & (N * qf) . 3 = <*(a * pp3)*> )
thus (N * qf) . 2 = <*(a * pp2)*> :: thesis: (N * qf) . 3 = <*(a * pp3)*>
proof
(Line (N,2)) "*" qf = ((N * qf) . 2) . 1 by ;
then ( len ((N * qf) . 2) = 1 & ((N * qf) . 2) . 1 = a * p221 ) by ;
hence (N * qf) . 2 = <*(a * pp2)*> by ; :: thesis: verum
end;
(Line (N,3)) "*" qf = ((N * qf) . 3) . 1 by ;
hence (N * qf) . 3 = <*(a * pp3)*> by ; :: thesis: verum
end;
hence a * p2 = N * qf by ; :: thesis: verum
end;
len <e2> = 3 by EUCLID_8:50;
then A63: <e2> = M2F () by ANPROJ_8:86
.= a * nv2 by ;
( not nv2 is zero & not a * nv2 is zero & are_Prop nv2,a * nv2 ) by ;
hence (homography N) . P2 = Dir010 by ; :: thesis: verum
end;
thus (homography N) . P3 = Dir001 :: thesis: verum
proof
consider nu3, nv3 being Element of (), u3f being FinSequence of F_Real, p3 being FinSequence of 1 -tuples_on REAL such that
A64: P3 = Dir nu3 and
A65: not nu3 is zero and
A66: nu3 = u3f and
A67: p3 = N * u3f and
A68: nv3 = M2F p3 and
A69: not nv3 is zero and
A70: (homography N) . P3 = Dir nv3 by ANPROJ_8:def 4;
are_Prop u3,nu3 by ;
then consider a being Real such that
A71: a <> 0 and
A72: u3 = a * nu3 by ANPROJ_1:1;
reconsider b = 1 / a as Real ;
nu3 in TOP-REAL 3 ;
then A73: nu3 in REAL 3 by EUCLID:22;
width <*u3f*> = len nu3 by
.= 3 by ;
then A74: len (<*u3f*> @) = width <*u3f*> by MATRIX_0:29
.= len nu3 by
.= 3 by ;
A75: width N = len (<*u3f*> @) by ;
A76: len (N * u3f) = len (N * (<*u3f*> @)) by LAPLACE:def 9
.= len N by
.= 3 by MATRIX_0:24 ;
len <e3> = 3 by ;
then A77: F2M <e3> = <*<*()*>,<*()*>,<*()*>*> by ANPROJ_8:def 1;
reconsider s1 = u3f . 1, s2 = u3f . 2, s3 = u3f . 3 as Element of F_Real by XREAL_0:def 1;
reconsider t1 = u3 . 1, t2 = u3 . 2, t3 = u3 . 3 as Element of F_Real by XREAL_0:def 1;
A78: ( (N * rf) . 1 = <*()*> & (N * rf) . 2 = <*()*> & (N * rf) . 3 = <*()*> ) by ;
A79: ((N * rf) . 1) . 1 = |[0,0,1]| . 1 by
.= |[0,0,1]| `1 by EUCLID_5:def 1
.= 0 by EUCLID_5:2 ;
A80: ((N * rf) . 2) . 1 = |[0,0,1]| . 2 by
.= |[0,0,1]| `2 by EUCLID_5:def 2
.= 0 by EUCLID_5:2 ;
A81: ((N * rf) . 3) . 1 = |[0,0,1]| . 3 by
.= |[0,0,1]| `3 by EUCLID_5:def 3
.= 1 by EUCLID_5:2 ;
( p3 . 1 = <*((N * (<*u3f*> @)) * (1,1))*> & p3 . 2 = <*((N * (<*u3f*> @)) * (2,1))*> & p3 . 3 = <*((N * (<*u3f*> @)) * (3,1))*> ) by ;
then reconsider p311 = (p3 . 1) . 1, p321 = (p3 . 2) . 1, p331 = (p3 . 3) . 1 as Real ;
A82: ( p311 = b * ((Line (N,1)) "*" rf) & p321 = b * ((Line (N,2)) "*" rf) & p331 = b * ((Line (N,3)) "*" rf) ) by ;
A83: a * p3 = N * rf
proof
consider pp1, pp2, pp3 being Real such that
A84: pp1 = (p3 . 1) . 1 and
A85: pp2 = (p3 . 2) . 1 and
A86: pp3 = (p3 . 3) . 1 and
A87: a * p3 = <*<*(a * pp1)*>,<*(a * pp2)*>,<*(a * pp3)*>*> by ;
now :: thesis: ( len (N * rf) = 3 & (N * rf) . 1 = <*(a * pp1)*> & (N * rf) . 2 = <*(a * pp2)*> & (N * rf) . 3 = <*(a * pp3)*> )
thus len (N * rf) = 3 by ; :: thesis: ( (N * rf) . 1 = <*(a * pp1)*> & (N * rf) . 2 = <*(a * pp2)*> & (N * rf) . 3 = <*(a * pp3)*> )
(Line (N,1)) "*" rf = ((N * rf) . 1) . 1 by ;
hence (N * rf) . 1 = <*(a * pp1)*> by ; :: thesis: ( (N * rf) . 2 = <*(a * pp2)*> & (N * rf) . 3 = <*(a * pp3)*> )
(Line (N,2)) "*" rf = ((N * rf) . 2) . 1 by ;
hence (N * rf) . 2 = <*(a * pp2)*> by ; :: thesis: (N * rf) . 3 = <*(a * pp3)*>
thus (N * rf) . 3 = <*(a * pp3)*> :: thesis: verum
proof
(Line (N,3)) "*" rf = ((N * rf) . 3) . 1 by ;
then ( len ((N * rf) . 3) = 1 & ((N * rf) . 3) . 1 = a * p331 ) by ;
hence (N * rf) . 3 = <*(a * pp3)*> by ; :: thesis: verum
end;
end;
hence a * p3 = N * rf by ; :: thesis: verum
end;
len <e3> = 3 by EUCLID_8:50;
then A88: <e3> = M2F () by ANPROJ_8:86
.= a * nv3 by ;
( not nv3 is zero & not a * nv3 is zero & are_Prop nv3,a * nv3 ) by ;
hence (homography N) . P3 = Dir001 by ; :: thesis: verum
end;