let P1, P2, P3 be Point of (ProjectiveSpace (TOP-REAL 3)); :: thesis: ( not P1,P2,P3 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 ) )

assume A1: not P1,P2,P3 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 )

consider u1 being Element of (TOP-REAL 3) such that

A2: not u1 is zero and

A3: P1 = Dir u1 by ANPROJ_1:26;

consider u2 being Element of (TOP-REAL 3) such that

A4: not u2 is zero and

A5: P2 = Dir u2 by ANPROJ_1:26;

consider u3 being Element of (TOP-REAL 3) such that

A6: not u3 is zero and

A7: P3 = Dir u3 by ANPROJ_1:26;

A8: |{u1,u2,u3}| <> 0 by ANPROJ_8:43, A1, A2, A3, A4, A5, A6, A7, ANPROJ_2:23;

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 A8, ANPROJ_8:94;

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

thus (homography N) . P1 = Dir100 :: thesis: ( (homography N) . P2 = Dir010 & (homography N) . P3 = Dir001 )

( (homography N) . P1 = Dir100 & (homography N) . P2 = Dir010 & (homography N) . P3 = Dir001 ) )

assume A1: not P1,P2,P3 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 )

consider u1 being Element of (TOP-REAL 3) such that

A2: not u1 is zero and

A3: P1 = Dir u1 by ANPROJ_1:26;

consider u2 being Element of (TOP-REAL 3) such that

A4: not u2 is zero and

A5: P2 = Dir u2 by ANPROJ_1:26;

consider u3 being Element of (TOP-REAL 3) such that

A6: not u3 is zero and

A7: P3 = Dir u3 by ANPROJ_1:26;

A8: |{u1,u2,u3}| <> 0 by ANPROJ_8:43, A1, A2, A3, A4, A5, A6, A7, ANPROJ_2:23;

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 A8, ANPROJ_8:94;

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

thus (homography N) . P1 = Dir100 :: thesis: ( (homography N) . P2 = Dir010 & (homography N) . P3 = Dir001 )

proof

thus
(homography N) . P2 = Dir010
:: thesis: (homography N) . P3 = Dir001
consider nu1, nv1 being Element of (TOP-REAL 3), 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 A2, A3, A14, A15, ANPROJ_1:22;

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 A16, ANPROJ_8:75

.= 3 by A23, EUCLID_8:50 ;

then A24: len (<*u1f*> @) = width <*u1f*> by MATRIX_0:29

.= len nu1 by ANPROJ_8:75, A16

.= 3 by A23, EUCLID_8:50 ;

A25: width N = len (<*u1f*> @) by MATRIX_0:24, A24;

A26: len (N * u1f) = len (N * (<*u1f*> @)) by LAPLACE:def 9

.= len N by A25, MATRIX_3:def 4

.= 3 by MATRIX_0:24 ;

len <e1> = 3 by EUCLID_8:def 1, FINSEQ_1:45;

then A27: F2M <e1> = <*<*(<e1> . 1)*>,<*(<e1> . 2)*>,<*(<e1> . 3)*>*> 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 = <*(<e1> . 1)*> & (N * pf) . 2 = <*(<e1> . 2)*> & (N * pf) . 3 = <*(<e1> . 3)*> ) by A10, A27, FINSEQ_1:45;

A29: ((N * pf) . 1) . 1 = |[1,0,0]| . 1 by A28, FINSEQ_1:40, EUCLID_8:def 1

.= |[1,0,0]| `1 by EUCLID_5:def 1

.= 1 by EUCLID_5:2 ;

A30: ((N * pf) . 2) . 1 = |[1,0,0]| . 2 by A28, FINSEQ_1:40, EUCLID_8:def 1

.= |[1,0,0]| `2 by EUCLID_5:def 2

.= 0 by EUCLID_5:2 ;

A31: ((N * pf) . 3) . 1 = |[1,0,0]| . 3 by A28, FINSEQ_1:40, EUCLID_8:def 1

.= |[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 A16, A17, FINSEQ_1:1, Lem02;

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 FINSEQ_1:1, A16, A17, A21, A22, Lem04;

A33: a * p1 = N * pf

then A38: <e1> = M2F (F2M <e1>) by ANPROJ_8:86

.= a * nv1 by A18, A33, A10, A26, A17, ANPROJ_8:83 ;

( not nv1 is zero & not a * nv1 is zero & are_Prop nv1,a * nv1 ) by A19, A21, Th04, ANPROJ_1:1;

hence (homography N) . P1 = Dir100 by A38, EUCLID_8:def 1, ANPROJ_1:22, A20; :: thesis: verum

end;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 A2, A3, A14, A15, ANPROJ_1:22;

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 A16, ANPROJ_8:75

.= 3 by A23, EUCLID_8:50 ;

then A24: len (<*u1f*> @) = width <*u1f*> by MATRIX_0:29

.= len nu1 by ANPROJ_8:75, A16

.= 3 by A23, EUCLID_8:50 ;

A25: width N = len (<*u1f*> @) by MATRIX_0:24, A24;

A26: len (N * u1f) = len (N * (<*u1f*> @)) by LAPLACE:def 9

.= len N by A25, MATRIX_3:def 4

.= 3 by MATRIX_0:24 ;

len <e1> = 3 by EUCLID_8:def 1, FINSEQ_1:45;

then A27: F2M <e1> = <*<*(<e1> . 1)*>,<*(<e1> . 2)*>,<*(<e1> . 3)*>*> 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 = <*(<e1> . 1)*> & (N * pf) . 2 = <*(<e1> . 2)*> & (N * pf) . 3 = <*(<e1> . 3)*> ) by A10, A27, FINSEQ_1:45;

A29: ((N * pf) . 1) . 1 = |[1,0,0]| . 1 by A28, FINSEQ_1:40, EUCLID_8:def 1

.= |[1,0,0]| `1 by EUCLID_5:def 1

.= 1 by EUCLID_5:2 ;

A30: ((N * pf) . 2) . 1 = |[1,0,0]| . 2 by A28, FINSEQ_1:40, EUCLID_8:def 1

.= |[1,0,0]| `2 by EUCLID_5:def 2

.= 0 by EUCLID_5:2 ;

A31: ((N * pf) . 3) . 1 = |[1,0,0]| . 3 by A28, FINSEQ_1:40, EUCLID_8:def 1

.= |[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 A16, A17, FINSEQ_1:1, Lem02;

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 FINSEQ_1:1, A16, A17, A21, A22, Lem04;

A33: a * p1 = N * pf

proof

len <e1> = 3
by EUCLID_8:50;
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 A17, A26, ANPROJ_8:def 3;

end;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 A17, A26, ANPROJ_8:def 3;

now :: thesis: ( len (N * pf) = 3 & (N * pf) . 1 = <*(a * pp1)*> & (N * pf) . 2 = <*(a * pp2)*> & (N * pf) . 3 = <*(a * pp3)*> )

hence
a * p1 = N * pf
by A37, FINSEQ_1:45; :: thesis: verumthus
len (N * pf) = 3
by A10, A13, ANPROJ_8:78; :: 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)*> )

hence (N * pf) . 3 = <*(a * pp3)*> by A36, FINSEQ_1:40, A28, A32, A31; :: thesis: verum

end;thus (N * pf) . 1 = <*(a * pp1)*> :: thesis: ( (N * pf) . 2 = <*(a * pp2)*> & (N * pf) . 3 = <*(a * pp3)*> )

proof

thus
(N * pf) . 2 = <*(a * pp2)*>
:: thesis: (N * pf) . 3 = <*(a * pp3)*>
(Line (N,1)) "*" pf = ((N * pf) . 1) . 1
by FINSEQ_1:1, Lem05;

then ( len ((N * pf) . 1) = 1 & ((N * pf) . 1) . 1 = a * p111 ) by A28, FINSEQ_1:40, A29, A32, A21, XCMPLX_1:87;

hence (N * pf) . 1 = <*(a * pp1)*> by A34, FINSEQ_1:40; :: thesis: verum

end;then ( len ((N * pf) . 1) = 1 & ((N * pf) . 1) . 1 = a * p111 ) by A28, FINSEQ_1:40, A29, A32, A21, XCMPLX_1:87;

hence (N * pf) . 1 = <*(a * pp1)*> by A34, FINSEQ_1:40; :: thesis: verum

proof

(Line (N,3)) "*" pf = ((N * pf) . 3) . 1
by FINSEQ_1:1, Lem05;
(Line (N,2)) "*" pf = ((N * pf) . 2) . 1
by FINSEQ_1:1, Lem05;

hence (N * pf) . 2 = <*(a * pp2)*> by A35, FINSEQ_1:40, A28, A30, A32; :: thesis: verum

end;hence (N * pf) . 2 = <*(a * pp2)*> by A35, FINSEQ_1:40, A28, A30, A32; :: thesis: verum

hence (N * pf) . 3 = <*(a * pp3)*> by A36, FINSEQ_1:40, A28, A32, A31; :: thesis: verum

then A38: <e1> = M2F (F2M <e1>) by ANPROJ_8:86

.= a * nv1 by A18, A33, A10, A26, A17, ANPROJ_8:83 ;

( not nv1 is zero & not a * nv1 is zero & are_Prop nv1,a * nv1 ) by A19, A21, Th04, ANPROJ_1:1;

hence (homography N) . P1 = Dir100 by A38, EUCLID_8:def 1, ANPROJ_1:22, A20; :: thesis: verum

proof

thus
(homography N) . P3 = Dir001
:: thesis: verum
consider nu2, nv2 being Element of (TOP-REAL 3), 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 A4, A5, A39, A40, ANPROJ_1:22;

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 A41, ANPROJ_8:75

.= 3 by A48, EUCLID_8:50 ;

then A49: len (<*u2f*> @) = width <*u2f*> by MATRIX_0:29

.= len nu2 by ANPROJ_8:75, A41

.= 3 by A48, EUCLID_8:50 ;

A50: width N = len (<*u2f*> @) by MATRIX_0:24, A49;

A51: len (N * u2f) = len (N * (<*u2f*> @)) by LAPLACE:def 9

.= len N by A50, MATRIX_3:def 4

.= 3 by MATRIX_0:24 ;

len <e2> = 3 by EUCLID_8:def 2, FINSEQ_1:45;

then A52: F2M <e2> = <*<*(<e2> . 1)*>,<*(<e2> . 2)*>,<*(<e2> . 3)*>*> 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 = <*(<e2> . 1)*> & (N * qf) . 2 = <*(<e2> . 2)*> & (N * qf) . 3 = <*(<e2> . 3)*> ) by A11, A52, FINSEQ_1:45;

A54: ((N * qf) . 1) . 1 = |[0,1,0]| . 1 by A53, FINSEQ_1:40, EUCLID_8:def 2

.= |[0,1,0]| `1 by EUCLID_5:def 1

.= 0 by EUCLID_5:2 ;

A55: ((N * qf) . 2) . 1 = |[0,1,0]| . 2 by A53, FINSEQ_1:40, EUCLID_8:def 2

.= |[0,1,0]| `2 by EUCLID_5:def 2

.= 1 by EUCLID_5:2 ;

A56: ((N * qf) . 3) . 1 = |[0,1,0]| . 3 by A53, FINSEQ_1:40, EUCLID_8:def 2

.= |[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 A41, A42, FINSEQ_1:1, Lem02;

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 FINSEQ_1:1, A41, A42, A46, A47, Lem04;

A58: a * p2 = N * qf

then A63: <e2> = M2F (F2M <e2>) by ANPROJ_8:86

.= a * nv2 by A43, A58, A11, A51, A42, ANPROJ_8:83 ;

( not nv2 is zero & not a * nv2 is zero & are_Prop nv2,a * nv2 ) by A44, A46, Th04, ANPROJ_1:1;

hence (homography N) . P2 = Dir010 by A63, EUCLID_8:def 2, ANPROJ_1:22, A45; :: thesis: verum

end;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 A4, A5, A39, A40, ANPROJ_1:22;

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 A41, ANPROJ_8:75

.= 3 by A48, EUCLID_8:50 ;

then A49: len (<*u2f*> @) = width <*u2f*> by MATRIX_0:29

.= len nu2 by ANPROJ_8:75, A41

.= 3 by A48, EUCLID_8:50 ;

A50: width N = len (<*u2f*> @) by MATRIX_0:24, A49;

A51: len (N * u2f) = len (N * (<*u2f*> @)) by LAPLACE:def 9

.= len N by A50, MATRIX_3:def 4

.= 3 by MATRIX_0:24 ;

len <e2> = 3 by EUCLID_8:def 2, FINSEQ_1:45;

then A52: F2M <e2> = <*<*(<e2> . 1)*>,<*(<e2> . 2)*>,<*(<e2> . 3)*>*> 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 = <*(<e2> . 1)*> & (N * qf) . 2 = <*(<e2> . 2)*> & (N * qf) . 3 = <*(<e2> . 3)*> ) by A11, A52, FINSEQ_1:45;

A54: ((N * qf) . 1) . 1 = |[0,1,0]| . 1 by A53, FINSEQ_1:40, EUCLID_8:def 2

.= |[0,1,0]| `1 by EUCLID_5:def 1

.= 0 by EUCLID_5:2 ;

A55: ((N * qf) . 2) . 1 = |[0,1,0]| . 2 by A53, FINSEQ_1:40, EUCLID_8:def 2

.= |[0,1,0]| `2 by EUCLID_5:def 2

.= 1 by EUCLID_5:2 ;

A56: ((N * qf) . 3) . 1 = |[0,1,0]| . 3 by A53, FINSEQ_1:40, EUCLID_8:def 2

.= |[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 A41, A42, FINSEQ_1:1, Lem02;

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 FINSEQ_1:1, A41, A42, A46, A47, Lem04;

A58: a * p2 = N * qf

proof

len <e2> = 3
by EUCLID_8:50;
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 A42, A51, ANPROJ_8:def 3;

end;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 A42, A51, ANPROJ_8:def 3;

now :: thesis: ( len (N * qf) = 3 & (N * qf) . 1 = <*(a * pp1)*> & (N * qf) . 2 = <*(a * pp2)*> & (N * qf) . 3 = <*(a * pp3)*> )

hence
a * p2 = N * qf
by A62, FINSEQ_1:45; :: thesis: verumthus
len (N * qf) = 3
by A11, A13, ANPROJ_8:78; :: 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 FINSEQ_1:1, Lem05;

hence (N * qf) . 1 = <*(a * pp1)*> by A59, FINSEQ_1:40, A53, A57, A54; :: thesis: ( (N * qf) . 2 = <*(a * pp2)*> & (N * qf) . 3 = <*(a * pp3)*> )

thus (N * qf) . 2 = <*(a * pp2)*> :: thesis: (N * qf) . 3 = <*(a * pp3)*>

hence (N * qf) . 3 = <*(a * pp3)*> by A61, FINSEQ_1:40, A53, A57, A56; :: thesis: verum

end;(Line (N,1)) "*" qf = ((N * qf) . 1) . 1 by FINSEQ_1:1, Lem05;

hence (N * qf) . 1 = <*(a * pp1)*> by A59, FINSEQ_1:40, A53, A57, A54; :: 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,3)) "*" qf = ((N * qf) . 3) . 1
by FINSEQ_1:1, Lem05;
(Line (N,2)) "*" qf = ((N * qf) . 2) . 1
by FINSEQ_1:1, Lem05;

then ( len ((N * qf) . 2) = 1 & ((N * qf) . 2) . 1 = a * p221 ) by A53, FINSEQ_1:40, A55, A57, A46, XCMPLX_1:87;

hence (N * qf) . 2 = <*(a * pp2)*> by A60, FINSEQ_1:40; :: thesis: verum

end;then ( len ((N * qf) . 2) = 1 & ((N * qf) . 2) . 1 = a * p221 ) by A53, FINSEQ_1:40, A55, A57, A46, XCMPLX_1:87;

hence (N * qf) . 2 = <*(a * pp2)*> by A60, FINSEQ_1:40; :: thesis: verum

hence (N * qf) . 3 = <*(a * pp3)*> by A61, FINSEQ_1:40, A53, A57, A56; :: thesis: verum

then A63: <e2> = M2F (F2M <e2>) by ANPROJ_8:86

.= a * nv2 by A43, A58, A11, A51, A42, ANPROJ_8:83 ;

( not nv2 is zero & not a * nv2 is zero & are_Prop nv2,a * nv2 ) by A44, A46, Th04, ANPROJ_1:1;

hence (homography N) . P2 = Dir010 by A63, EUCLID_8:def 2, ANPROJ_1:22, A45; :: thesis: verum

proof

consider nu3, nv3 being Element of (TOP-REAL 3), 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 A6, A7, A64, A65, ANPROJ_1:22;

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 A66, ANPROJ_8:75

.= 3 by A73, EUCLID_8:50 ;

then A74: len (<*u3f*> @) = width <*u3f*> by MATRIX_0:29

.= len nu3 by ANPROJ_8:75, A66

.= 3 by A73, EUCLID_8:50 ;

A75: width N = len (<*u3f*> @) by MATRIX_0:24, A74;

A76: len (N * u3f) = len (N * (<*u3f*> @)) by LAPLACE:def 9

.= len N by A75, MATRIX_3:def 4

.= 3 by MATRIX_0:24 ;

len <e3> = 3 by EUCLID_8:def 3, FINSEQ_1:45;

then A77: F2M <e3> = <*<*(<e3> . 1)*>,<*(<e3> . 2)*>,<*(<e3> . 3)*>*> 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 = <*(<e3> . 1)*> & (N * rf) . 2 = <*(<e3> . 2)*> & (N * rf) . 3 = <*(<e3> . 3)*> ) by A12, A77, FINSEQ_1:45;

A79: ((N * rf) . 1) . 1 = |[0,0,1]| . 1 by A78, FINSEQ_1:40, EUCLID_8:def 3

.= |[0,0,1]| `1 by EUCLID_5:def 1

.= 0 by EUCLID_5:2 ;

A80: ((N * rf) . 2) . 1 = |[0,0,1]| . 2 by A78, FINSEQ_1:40, EUCLID_8:def 3

.= |[0,0,1]| `2 by EUCLID_5:def 2

.= 0 by EUCLID_5:2 ;

A81: ((N * rf) . 3) . 1 = |[0,0,1]| . 3 by A78, FINSEQ_1:40, EUCLID_8:def 3

.= |[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 A66, A67, FINSEQ_1:1, Lem02;

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 FINSEQ_1:1, A66, A67, A71, A72, Lem04;

A83: a * p3 = N * rf

then A88: <e3> = M2F (F2M <e3>) by ANPROJ_8:86

.= a * nv3 by A68, A83, A12, A76, A67, ANPROJ_8:83 ;

( not nv3 is zero & not a * nv3 is zero & are_Prop nv3,a * nv3 ) by A69, A71, Th04, ANPROJ_1:1;

hence (homography N) . P3 = Dir001 by A88, EUCLID_8:def 3, ANPROJ_1:22, A70; :: thesis: verum

end;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 A6, A7, A64, A65, ANPROJ_1:22;

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 A66, ANPROJ_8:75

.= 3 by A73, EUCLID_8:50 ;

then A74: len (<*u3f*> @) = width <*u3f*> by MATRIX_0:29

.= len nu3 by ANPROJ_8:75, A66

.= 3 by A73, EUCLID_8:50 ;

A75: width N = len (<*u3f*> @) by MATRIX_0:24, A74;

A76: len (N * u3f) = len (N * (<*u3f*> @)) by LAPLACE:def 9

.= len N by A75, MATRIX_3:def 4

.= 3 by MATRIX_0:24 ;

len <e3> = 3 by EUCLID_8:def 3, FINSEQ_1:45;

then A77: F2M <e3> = <*<*(<e3> . 1)*>,<*(<e3> . 2)*>,<*(<e3> . 3)*>*> 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 = <*(<e3> . 1)*> & (N * rf) . 2 = <*(<e3> . 2)*> & (N * rf) . 3 = <*(<e3> . 3)*> ) by A12, A77, FINSEQ_1:45;

A79: ((N * rf) . 1) . 1 = |[0,0,1]| . 1 by A78, FINSEQ_1:40, EUCLID_8:def 3

.= |[0,0,1]| `1 by EUCLID_5:def 1

.= 0 by EUCLID_5:2 ;

A80: ((N * rf) . 2) . 1 = |[0,0,1]| . 2 by A78, FINSEQ_1:40, EUCLID_8:def 3

.= |[0,0,1]| `2 by EUCLID_5:def 2

.= 0 by EUCLID_5:2 ;

A81: ((N * rf) . 3) . 1 = |[0,0,1]| . 3 by A78, FINSEQ_1:40, EUCLID_8:def 3

.= |[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 A66, A67, FINSEQ_1:1, Lem02;

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 FINSEQ_1:1, A66, A67, A71, A72, Lem04;

A83: a * p3 = N * rf

proof

len <e3> = 3
by EUCLID_8:50;
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 A67, A76, ANPROJ_8:def 3;

end;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 A67, A76, ANPROJ_8:def 3;

now :: thesis: ( len (N * rf) = 3 & (N * rf) . 1 = <*(a * pp1)*> & (N * rf) . 2 = <*(a * pp2)*> & (N * rf) . 3 = <*(a * pp3)*> )

hence
a * p3 = N * rf
by A87, FINSEQ_1:45; :: thesis: verumthus
len (N * rf) = 3
by A12, A13, ANPROJ_8:78; :: 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 FINSEQ_1:1, Lem05;

hence (N * rf) . 1 = <*(a * pp1)*> by A84, FINSEQ_1:40, A78, A82, A79; :: thesis: ( (N * rf) . 2 = <*(a * pp2)*> & (N * rf) . 3 = <*(a * pp3)*> )

(Line (N,2)) "*" rf = ((N * rf) . 2) . 1 by FINSEQ_1:1, Lem05;

hence (N * rf) . 2 = <*(a * pp2)*> by A85, FINSEQ_1:40, A78, A82, A80; :: thesis: (N * rf) . 3 = <*(a * pp3)*>

thus (N * rf) . 3 = <*(a * pp3)*> :: thesis: verum

end;(Line (N,1)) "*" rf = ((N * rf) . 1) . 1 by FINSEQ_1:1, Lem05;

hence (N * rf) . 1 = <*(a * pp1)*> by A84, FINSEQ_1:40, A78, A82, A79; :: thesis: ( (N * rf) . 2 = <*(a * pp2)*> & (N * rf) . 3 = <*(a * pp3)*> )

(Line (N,2)) "*" rf = ((N * rf) . 2) . 1 by FINSEQ_1:1, Lem05;

hence (N * rf) . 2 = <*(a * pp2)*> by A85, FINSEQ_1:40, A78, A82, A80; :: thesis: (N * rf) . 3 = <*(a * pp3)*>

thus (N * rf) . 3 = <*(a * pp3)*> :: thesis: verum

then A88: <e3> = M2F (F2M <e3>) by ANPROJ_8:86

.= a * nv3 by A68, A83, A12, A76, A67, ANPROJ_8:83 ;

( not nv3 is zero & not a * nv3 is zero & are_Prop nv3,a * nv3 ) by A69, A71, Th04, ANPROJ_1:1;

hence (homography N) . P3 = Dir001 by A88, EUCLID_8:def 3, ANPROJ_1:22, A70; :: thesis: verum