let N1, N2 be invertible Matrix of 3,F_Real; :: thesis: for P being Point of (ProjectiveSpace (TOP-REAL 3)) holds (homography N1) . ((homography N2) . P) = (homography (N1 * N2)) . P

let P be Point of (ProjectiveSpace (TOP-REAL 3)); :: thesis: (homography N1) . ((homography N2) . P) = (homography (N1 * N2)) . P

consider u12, v12 being Element of (TOP-REAL 3), u12f being FinSequence of F_Real, p12 being FinSequence of 1 -tuples_on REAL such that

A1: P = Dir u12 and

A2: not u12 is zero and

A3: u12 = u12f and

A4: p12 = (N1 * N2) * u12f and

A5: v12 = M2F p12 and

A6: not v12 is zero and

A7: (homography (N1 * N2)) . P = Dir v12 by ANPROJ_8:def 4;

consider u2, v2 being Element of (TOP-REAL 3), u2f being FinSequence of F_Real, p2 being FinSequence of 1 -tuples_on REAL such that

A8: P = Dir u2 and

A9: not u2 is zero and

A10: u2 = u2f and

A11: p2 = N2 * u2f and

A12: v2 = M2F p2 and

A13: not v2 is zero and

A14: (homography N2) . P = Dir v2 by ANPROJ_8:def 4;

consider u1, v1 being Element of (TOP-REAL 3), u1f being FinSequence of F_Real, p1 being FinSequence of 1 -tuples_on REAL such that

A15: (homography N2) . P = Dir u1 and

A16: not u1 is zero and

A17: u1 = u1f and

A18: p1 = N1 * u1f and

A19: v1 = M2F p1 and

A20: not v1 is zero and

A21: (homography N1) . ((homography N2) . P) = Dir v1 by ANPROJ_8:def 4;

are_Prop u12,u2 by A1, A8, A2, A9, ANPROJ_1:22;

then consider a being Real such that

A22: a <> 0 and

A23: u2 = a * u12 by ANPROJ_1:1;

are_Prop v2,u1 by A14, A15, A16, A13, ANPROJ_1:22;

then consider b being Real such that

A24: b <> 0 and

A25: u1 = b * v2 by ANPROJ_1:1;

u1 in TOP-REAL 3 ;

then F2: u1 in REAL 3 by EUCLID:22;

width <*u1f*> = len u1 by A17, ANPROJ_8:75

.= 3 by F2, EUCLID_8:50 ;

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

.= len u1 by ANPROJ_8:75, A17

.= 3 by F2, EUCLID_8:50 ;

then A26: width N1 = len (<*u1f*> @) by MATRIX_0:24;

A27: len (N1 * u1f) = len (N1 * (<*u1f*> @)) by LAPLACE:def 9

.= len N1 by A26, MATRIX_3:def 4

.= 3 by MATRIX_0:24 ;

A28: v1 = <*((N1 * (<*u1f*> @)) * (1,1)),((N1 * (<*u1f*> @)) * (2,1)),((N1 * (<*u1f*> @)) * (3,1))*>

then A29: u2 in REAL 3 by EUCLID:22;

width <*u2f*> = len u2 by A10, ANPROJ_8:75

.= 3 by A29, EUCLID_8:50 ;

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

.= len u2 by ANPROJ_8:75, A10

.= 3 by A29, EUCLID_8:50 ;

then A30: width N2 = len (<*u2f*> @) by MATRIX_0:24;

A31: len (N2 * u2f) = len (N2 * (<*u2f*> @)) by LAPLACE:def 9

.= len N2 by A30, MATRIX_3:def 4

.= 3 by MATRIX_0:24 ;

A32: v2 = <*((N2 * (<*u2f*> @)) * (1,1)),((N2 * (<*u2f*> @)) * (2,1)),((N2 * (<*u2f*> @)) * (3,1))*>

then A33: u12 in REAL 3 by EUCLID:22;

width <*u12f*> = len u12 by A3, ANPROJ_8:75

.= 3 by A33, EUCLID_8:50 ;

then A34: len (<*u12f*> @) = width <*u12f*> by MATRIX_0:29

.= len u12 by ANPROJ_8:75, A3

.= 3 by A33, EUCLID_8:50 ;

A35: width (N1 * N2) = len (<*u12f*> @) by MATRIX_0:24, A34;

A36: len ((N1 * N2) * u12f) = len ((N1 * N2) * (<*u12f*> @)) by LAPLACE:def 9

.= len (N1 * N2) by A35, MATRIX_3:def 4

.= 3 by MATRIX_0:24 ;

A37: v12 = <*(((N1 * N2) * (<*u12f*> @)) * (1,1)),(((N1 * N2) * (<*u12f*> @)) * (2,1)),(((N1 * N2) * (<*u12f*> @)) * (3,1))*>

reconsider invb = 1 / b as Real ;

A38: v2f = invb * u1

then A39: ( (N1 * (<*u1f*> @)) * (1,1) = (1 / invb) * ((Line (N1,1)) "*" v2f) & (N1 * (<*u1f*> @)) * (2,1) = (1 / invb) * ((Line (N1,2)) "*" v2f) & (N1 * (<*u1f*> @)) * (3,1) = (1 / invb) * ((Line (N1,3)) "*" v2f) ) by A24, XCMPLX_1:50, A38, A17, Lem03;

A40: ( len (Line (N1,1)) = width N1 & len (Line (N1,2)) = width N1 & len (Line (N1,3)) = width N1 ) by MATRIX_0:def 7;

width N1 = 3 by MATRIX_0:24;

then ( 1 in Seg (width N1) & 2 in Seg (width N1) & 3 in Seg (width N1) ) by FINSEQ_1:1;

then A41: ( (Line (N1,1)) . 1 = N1 * (1,1) & (Line (N1,1)) . 2 = N1 * (1,2) & (Line (N1,1)) . 3 = N1 * (1,3) & (Line (N1,2)) . 1 = N1 * (2,1) & (Line (N1,2)) . 2 = N1 * (2,2) & (Line (N1,2)) . 3 = N1 * (2,3) & (Line (N1,3)) . 1 = N1 * (3,1) & (Line (N1,3)) . 2 = N1 * (3,2) & (Line (N1,3)) . 3 = N1 * (3,3) ) by MATRIX_0:def 7;

then A42: ( Line (N1,1) = <*(N1 * (1,1)),(N1 * (1,2)),(N1 * (1,3))*> & Line (N1,2) = <*(N1 * (2,1)),(N1 * (2,2)),(N1 * (2,3))*> & Line (N1,3) = <*(N1 * (3,1)),(N1 * (3,2)),(N1 * (3,3))*> ) by A40, MATRIX_0:24, FINSEQ_1:45;

A43: ( len (Line ((N1 * N2),1)) = width (N1 * N2) & len (Line ((N1 * N2),2)) = width (N1 * N2) & len (Line ((N1 * N2),3)) = width (N1 * N2) ) by MATRIX_0:def 7;

width (N1 * N2) = 3 by MATRIX_0:24;

then ( 1 in Seg (width (N1 * N2)) & 2 in Seg (width (N1 * N2)) & 3 in Seg (width (N1 * N2)) ) by FINSEQ_1:1;

then A44: ( (Line ((N1 * N2),1)) . 1 = (N1 * N2) * (1,1) & (Line ((N1 * N2),1)) . 2 = (N1 * N2) * (1,2) & (Line ((N1 * N2),1)) . 3 = (N1 * N2) * (1,3) & (Line ((N1 * N2),2)) . 1 = (N1 * N2) * (2,1) & (Line ((N1 * N2),2)) . 2 = (N1 * N2) * (2,2) & (Line ((N1 * N2),2)) . 3 = (N1 * N2) * (2,3) & (Line ((N1 * N2),3)) . 1 = (N1 * N2) * (3,1) & (Line ((N1 * N2),3)) . 2 = (N1 * N2) * (3,2) & (Line ((N1 * N2),3)) . 3 = (N1 * N2) * (3,3) ) by MATRIX_0:def 7;

reconsider fa = a as Element of F_Real by XREAL_0:def 1;

A45: ( v1 . 1 = (N1 * (<*u1f*> @)) * (1,1) & v1 . 2 = (N1 * (<*u1f*> @)) * (2,1) & v1 . 3 = (N1 * (<*u1f*> @)) * (3,1) ) by A28, FINSEQ_1:45;

reconsider t1 = v2f . 1, t2 = v2f . 2, t3 = v2f . 3 as Element of F_Real by A32, FINSEQ_1:45;

len v2f = 3 by A32, FINSEQ_1:45;

then A46: v2f = <*t1,t2,t3*> by FINSEQ_1:45;

N2 * (<*u2f*> @) is Matrix of 3,1,F_Real by A10, FINSEQ_3:153, ANPROJ_8:91;

then A47: ( [1,1] in Indices (N2 * (<*u2f*> @)) & [2,1] in Indices (N2 * (<*u2f*> @)) & [3,1] in Indices (N2 * (<*u2f*> @)) ) by ANPROJ_8:2, MATRIX_0:23;

A48: t1 = (N2 * (<*u2f*> @)) * (1,1) by A32, FINSEQ_1:45

.= (Line (N2,1)) "*" (Col ((<*u2f*> @),1)) by A30, A47, MATRIX_3:def 4

.= (Line (N2,1)) "*" u2f by ANPROJ_8:93 ;

A49: t2 = (N2 * (<*u2f*> @)) * (2,1) by A32, FINSEQ_1:45

.= (Line (N2,2)) "*" (Col ((<*u2f*> @),1)) by A30, A47, MATRIX_3:def 4

.= (Line (N2,2)) "*" u2f by ANPROJ_8:93 ;

A50: t3 = (N2 * (<*u2f*> @)) * (3,1) by A32, FINSEQ_1:45

.= (Line (N2,3)) "*" (Col ((<*u2f*> @),1)) by A30, A47, MATRIX_3:def 4

.= (Line (N2,3)) "*" u2f by ANPROJ_8:93 ;

reconsider ru121 = u12f . 1, ru122 = u12f . 2, ru123 = u12f . 3 as Element of F_Real by XREAL_0:def 1;

( len (Line (N2,1)) = width N2 & len (Line (N2,2)) = width N2 & len (Line (N2,3)) = width N2 ) by MATRIX_0:def 7;

then A51: ( Line (N2,1) = <*l11,l12,l13*> & Line (N2,2) = <*l21,l22,l23*> & Line (N2,3) = <*l31,l32,l33*> ) by MATRIX_0:23, FINSEQ_1:45;

reconsider ru21 = u2 . 1, ru22 = u2 . 2, ru23 = u2 . 3 as Element of F_Real by XREAL_0:def 1;

A52: ( ru21 = a * (u12f . 1) & ru22 = a * (u12f . 2) & ru23 = a * (u12f . 3) ) by A3, A23, RVSUM_1:44;

len u2 = 3 by A29, EUCLID_8:50;

then A53: u2f = <*ru21,ru22,ru23*> by A10, FINSEQ_1:45;

reconsider t121 = v12 . 1, t122 = v12 . 2, t123 = v12 . 3 as Element of F_Real by A37, FINSEQ_1:45;

reconsider v12f = v12 as FinSequence of F_Real by RVSUM_1:145;

width N1 = 3 by MATRIX_0:24;

then A54: width N1 = len N2 by MATRIX_0:24;

A55: ( [1,1] in Indices (N1 * N2) & [1,2] in Indices (N1 * N2) & [1,3] in Indices (N1 * N2) & [2,1] in Indices (N1 * N2) & [2,2] in Indices (N1 * N2) & [2,3] in Indices (N1 * N2) & [3,1] in Indices (N1 * N2) & [3,2] in Indices (N1 * N2) & [3,3] in Indices (N1 * N2) ) by ANPROJ_8:1, MATRIX_0:23;

A56: width (N1 * N2) = len (<*u12f*> @) by A34, MATRIX_0:24;

u12 in TOP-REAL 3 ;

then u12f in REAL 3 by EUCLID:22, A3;

then A57: len u12f = 3 by EUCLID_8:50;

(N1 * N2) * (<*u12f*> @) is Matrix of 3,1,F_Real by A3, FINSEQ_3:153, ANPROJ_8:91;

then A58: ( [1,1] in Indices ((N1 * N2) * (<*u12f*> @)) & [2,1] in Indices ((N1 * N2) * (<*u12f*> @)) & [3,1] in Indices ((N1 * N2) * (<*u12f*> @)) ) by MATRIX_0:23, ANPROJ_8:2;

A59: u12f = <*ru121,ru122,ru123*> by A57, FINSEQ_1:45;

A60: ( Col (N2,1) = <*l11,l21,l31*> & Col (N2,2) = <*l12,l22,l32*> & Col (N2,3) = <*l13,l23,l33*> )

let P be Point of (ProjectiveSpace (TOP-REAL 3)); :: thesis: (homography N1) . ((homography N2) . P) = (homography (N1 * N2)) . P

consider u12, v12 being Element of (TOP-REAL 3), u12f being FinSequence of F_Real, p12 being FinSequence of 1 -tuples_on REAL such that

A1: P = Dir u12 and

A2: not u12 is zero and

A3: u12 = u12f and

A4: p12 = (N1 * N2) * u12f and

A5: v12 = M2F p12 and

A6: not v12 is zero and

A7: (homography (N1 * N2)) . P = Dir v12 by ANPROJ_8:def 4;

consider u2, v2 being Element of (TOP-REAL 3), u2f being FinSequence of F_Real, p2 being FinSequence of 1 -tuples_on REAL such that

A8: P = Dir u2 and

A9: not u2 is zero and

A10: u2 = u2f and

A11: p2 = N2 * u2f and

A12: v2 = M2F p2 and

A13: not v2 is zero and

A14: (homography N2) . P = Dir v2 by ANPROJ_8:def 4;

consider u1, v1 being Element of (TOP-REAL 3), u1f being FinSequence of F_Real, p1 being FinSequence of 1 -tuples_on REAL such that

A15: (homography N2) . P = Dir u1 and

A16: not u1 is zero and

A17: u1 = u1f and

A18: p1 = N1 * u1f and

A19: v1 = M2F p1 and

A20: not v1 is zero and

A21: (homography N1) . ((homography N2) . P) = Dir v1 by ANPROJ_8:def 4;

are_Prop u12,u2 by A1, A8, A2, A9, ANPROJ_1:22;

then consider a being Real such that

A22: a <> 0 and

A23: u2 = a * u12 by ANPROJ_1:1;

are_Prop v2,u1 by A14, A15, A16, A13, ANPROJ_1:22;

then consider b being Real such that

A24: b <> 0 and

A25: u1 = b * v2 by ANPROJ_1:1;

u1 in TOP-REAL 3 ;

then F2: u1 in REAL 3 by EUCLID:22;

width <*u1f*> = len u1 by A17, ANPROJ_8:75

.= 3 by F2, EUCLID_8:50 ;

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

.= len u1 by ANPROJ_8:75, A17

.= 3 by F2, EUCLID_8:50 ;

then A26: width N1 = len (<*u1f*> @) by MATRIX_0:24;

A27: len (N1 * u1f) = len (N1 * (<*u1f*> @)) by LAPLACE:def 9

.= len N1 by A26, MATRIX_3:def 4

.= 3 by MATRIX_0:24 ;

A28: v1 = <*((N1 * (<*u1f*> @)) * (1,1)),((N1 * (<*u1f*> @)) * (2,1)),((N1 * (<*u1f*> @)) * (3,1))*>

proof

u2 in TOP-REAL 3
;
( p1 . 1 = <*((N1 * (<*u1f*> @)) * (1,1))*> & p1 . 2 = <*((N1 * (<*u1f*> @)) * (2,1))*> & p1 . 3 = <*((N1 * (<*u1f*> @)) * (3,1))*> )
by A17, A18, FINSEQ_1:1, Lem02;

then ( (p1 . 1) . 1 = (N1 * (<*u1f*> @)) * (1,1) & (p1 . 2) . 1 = (N1 * (<*u1f*> @)) * (2,1) & (p1 . 3) . 1 = (N1 * (<*u1f*> @)) * (3,1) ) by FINSEQ_1:40;

hence v1 = <*((N1 * (<*u1f*> @)) * (1,1)),((N1 * (<*u1f*> @)) * (2,1)),((N1 * (<*u1f*> @)) * (3,1))*> by A19, A27, A18, ANPROJ_8:def 2; :: thesis: verum

end;then ( (p1 . 1) . 1 = (N1 * (<*u1f*> @)) * (1,1) & (p1 . 2) . 1 = (N1 * (<*u1f*> @)) * (2,1) & (p1 . 3) . 1 = (N1 * (<*u1f*> @)) * (3,1) ) by FINSEQ_1:40;

hence v1 = <*((N1 * (<*u1f*> @)) * (1,1)),((N1 * (<*u1f*> @)) * (2,1)),((N1 * (<*u1f*> @)) * (3,1))*> by A19, A27, A18, ANPROJ_8:def 2; :: thesis: verum

then A29: u2 in REAL 3 by EUCLID:22;

width <*u2f*> = len u2 by A10, ANPROJ_8:75

.= 3 by A29, EUCLID_8:50 ;

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

.= len u2 by ANPROJ_8:75, A10

.= 3 by A29, EUCLID_8:50 ;

then A30: width N2 = len (<*u2f*> @) by MATRIX_0:24;

A31: len (N2 * u2f) = len (N2 * (<*u2f*> @)) by LAPLACE:def 9

.= len N2 by A30, MATRIX_3:def 4

.= 3 by MATRIX_0:24 ;

A32: v2 = <*((N2 * (<*u2f*> @)) * (1,1)),((N2 * (<*u2f*> @)) * (2,1)),((N2 * (<*u2f*> @)) * (3,1))*>

proof

u12 in TOP-REAL 3
;
( p2 . 1 = <*((N2 * (<*u2f*> @)) * (1,1))*> & p2 . 2 = <*((N2 * (<*u2f*> @)) * (2,1))*> & p2 . 3 = <*((N2 * (<*u2f*> @)) * (3,1))*> )
by A10, A11, FINSEQ_1:1, Lem02;

then ( (p2 . 1) . 1 = (N2 * (<*u2f*> @)) * (1,1) & (p2 . 2) . 1 = (N2 * (<*u2f*> @)) * (2,1) & (p2 . 3) . 1 = (N2 * (<*u2f*> @)) * (3,1) ) by FINSEQ_1:40;

hence v2 = <*((N2 * (<*u2f*> @)) * (1,1)),((N2 * (<*u2f*> @)) * (2,1)),((N2 * (<*u2f*> @)) * (3,1))*> by A12, A31, A11, ANPROJ_8:def 2; :: thesis: verum

end;then ( (p2 . 1) . 1 = (N2 * (<*u2f*> @)) * (1,1) & (p2 . 2) . 1 = (N2 * (<*u2f*> @)) * (2,1) & (p2 . 3) . 1 = (N2 * (<*u2f*> @)) * (3,1) ) by FINSEQ_1:40;

hence v2 = <*((N2 * (<*u2f*> @)) * (1,1)),((N2 * (<*u2f*> @)) * (2,1)),((N2 * (<*u2f*> @)) * (3,1))*> by A12, A31, A11, ANPROJ_8:def 2; :: thesis: verum

then A33: u12 in REAL 3 by EUCLID:22;

width <*u12f*> = len u12 by A3, ANPROJ_8:75

.= 3 by A33, EUCLID_8:50 ;

then A34: len (<*u12f*> @) = width <*u12f*> by MATRIX_0:29

.= len u12 by ANPROJ_8:75, A3

.= 3 by A33, EUCLID_8:50 ;

A35: width (N1 * N2) = len (<*u12f*> @) by MATRIX_0:24, A34;

A36: len ((N1 * N2) * u12f) = len ((N1 * N2) * (<*u12f*> @)) by LAPLACE:def 9

.= len (N1 * N2) by A35, MATRIX_3:def 4

.= 3 by MATRIX_0:24 ;

A37: v12 = <*(((N1 * N2) * (<*u12f*> @)) * (1,1)),(((N1 * N2) * (<*u12f*> @)) * (2,1)),(((N1 * N2) * (<*u12f*> @)) * (3,1))*>

proof

reconsider v2f = v2 as FinSequence of F_Real by RVSUM_1:145;
( p12 . 1 = <*(((N1 * N2) * (<*u12f*> @)) * (1,1))*> & p12 . 2 = <*(((N1 * N2) * (<*u12f*> @)) * (2,1))*> & p12 . 3 = <*(((N1 * N2) * (<*u12f*> @)) * (3,1))*> )
by A3, A4, FINSEQ_1:1, Lem02;

then ( (p12 . 1) . 1 = ((N1 * N2) * (<*u12f*> @)) * (1,1) & (p12 . 2) . 1 = ((N1 * N2) * (<*u12f*> @)) * (2,1) & (p12 . 3) . 1 = ((N1 * N2) * (<*u12f*> @)) * (3,1) ) by FINSEQ_1:40;

hence v12 = <*(((N1 * N2) * (<*u12f*> @)) * (1,1)),(((N1 * N2) * (<*u12f*> @)) * (2,1)),(((N1 * N2) * (<*u12f*> @)) * (3,1))*> by A5, A36, A4, ANPROJ_8:def 2; :: thesis: verum

end;then ( (p12 . 1) . 1 = ((N1 * N2) * (<*u12f*> @)) * (1,1) & (p12 . 2) . 1 = ((N1 * N2) * (<*u12f*> @)) * (2,1) & (p12 . 3) . 1 = ((N1 * N2) * (<*u12f*> @)) * (3,1) ) by FINSEQ_1:40;

hence v12 = <*(((N1 * N2) * (<*u12f*> @)) * (1,1)),(((N1 * N2) * (<*u12f*> @)) * (2,1)),(((N1 * N2) * (<*u12f*> @)) * (3,1))*> by A5, A36, A4, ANPROJ_8:def 2; :: thesis: verum

reconsider invb = 1 / b as Real ;

A38: v2f = invb * u1

proof

( 1 in Seg 3 & 2 in Seg 3 & 3 in Seg 3 )
by FINSEQ_1:1;
invb * u1 =
(invb * b) * v2f
by A25, RVSUM_1:49

.= 1 * v2f by A24, XCMPLX_1:106

.= v2f by RVSUM_1:52 ;

hence v2f = invb * u1 ; :: thesis: verum

end;.= 1 * v2f by A24, XCMPLX_1:106

.= v2f by RVSUM_1:52 ;

hence v2f = invb * u1 ; :: thesis: verum

then A39: ( (N1 * (<*u1f*> @)) * (1,1) = (1 / invb) * ((Line (N1,1)) "*" v2f) & (N1 * (<*u1f*> @)) * (2,1) = (1 / invb) * ((Line (N1,2)) "*" v2f) & (N1 * (<*u1f*> @)) * (3,1) = (1 / invb) * ((Line (N1,3)) "*" v2f) ) by A24, XCMPLX_1:50, A38, A17, Lem03;

A40: ( len (Line (N1,1)) = width N1 & len (Line (N1,2)) = width N1 & len (Line (N1,3)) = width N1 ) by MATRIX_0:def 7;

width N1 = 3 by MATRIX_0:24;

then ( 1 in Seg (width N1) & 2 in Seg (width N1) & 3 in Seg (width N1) ) by FINSEQ_1:1;

then A41: ( (Line (N1,1)) . 1 = N1 * (1,1) & (Line (N1,1)) . 2 = N1 * (1,2) & (Line (N1,1)) . 3 = N1 * (1,3) & (Line (N1,2)) . 1 = N1 * (2,1) & (Line (N1,2)) . 2 = N1 * (2,2) & (Line (N1,2)) . 3 = N1 * (2,3) & (Line (N1,3)) . 1 = N1 * (3,1) & (Line (N1,3)) . 2 = N1 * (3,2) & (Line (N1,3)) . 3 = N1 * (3,3) ) by MATRIX_0:def 7;

then A42: ( Line (N1,1) = <*(N1 * (1,1)),(N1 * (1,2)),(N1 * (1,3))*> & Line (N1,2) = <*(N1 * (2,1)),(N1 * (2,2)),(N1 * (2,3))*> & Line (N1,3) = <*(N1 * (3,1)),(N1 * (3,2)),(N1 * (3,3))*> ) by A40, MATRIX_0:24, FINSEQ_1:45;

A43: ( len (Line ((N1 * N2),1)) = width (N1 * N2) & len (Line ((N1 * N2),2)) = width (N1 * N2) & len (Line ((N1 * N2),3)) = width (N1 * N2) ) by MATRIX_0:def 7;

width (N1 * N2) = 3 by MATRIX_0:24;

then ( 1 in Seg (width (N1 * N2)) & 2 in Seg (width (N1 * N2)) & 3 in Seg (width (N1 * N2)) ) by FINSEQ_1:1;

then A44: ( (Line ((N1 * N2),1)) . 1 = (N1 * N2) * (1,1) & (Line ((N1 * N2),1)) . 2 = (N1 * N2) * (1,2) & (Line ((N1 * N2),1)) . 3 = (N1 * N2) * (1,3) & (Line ((N1 * N2),2)) . 1 = (N1 * N2) * (2,1) & (Line ((N1 * N2),2)) . 2 = (N1 * N2) * (2,2) & (Line ((N1 * N2),2)) . 3 = (N1 * N2) * (2,3) & (Line ((N1 * N2),3)) . 1 = (N1 * N2) * (3,1) & (Line ((N1 * N2),3)) . 2 = (N1 * N2) * (3,2) & (Line ((N1 * N2),3)) . 3 = (N1 * N2) * (3,3) ) by MATRIX_0:def 7;

reconsider fa = a as Element of F_Real by XREAL_0:def 1;

A45: ( v1 . 1 = (N1 * (<*u1f*> @)) * (1,1) & v1 . 2 = (N1 * (<*u1f*> @)) * (2,1) & v1 . 3 = (N1 * (<*u1f*> @)) * (3,1) ) by A28, FINSEQ_1:45;

reconsider t1 = v2f . 1, t2 = v2f . 2, t3 = v2f . 3 as Element of F_Real by A32, FINSEQ_1:45;

len v2f = 3 by A32, FINSEQ_1:45;

then A46: v2f = <*t1,t2,t3*> by FINSEQ_1:45;

N2 * (<*u2f*> @) is Matrix of 3,1,F_Real by A10, FINSEQ_3:153, ANPROJ_8:91;

then A47: ( [1,1] in Indices (N2 * (<*u2f*> @)) & [2,1] in Indices (N2 * (<*u2f*> @)) & [3,1] in Indices (N2 * (<*u2f*> @)) ) by ANPROJ_8:2, MATRIX_0:23;

A48: t1 = (N2 * (<*u2f*> @)) * (1,1) by A32, FINSEQ_1:45

.= (Line (N2,1)) "*" (Col ((<*u2f*> @),1)) by A30, A47, MATRIX_3:def 4

.= (Line (N2,1)) "*" u2f by ANPROJ_8:93 ;

A49: t2 = (N2 * (<*u2f*> @)) * (2,1) by A32, FINSEQ_1:45

.= (Line (N2,2)) "*" (Col ((<*u2f*> @),1)) by A30, A47, MATRIX_3:def 4

.= (Line (N2,2)) "*" u2f by ANPROJ_8:93 ;

A50: t3 = (N2 * (<*u2f*> @)) * (3,1) by A32, FINSEQ_1:45

.= (Line (N2,3)) "*" (Col ((<*u2f*> @),1)) by A30, A47, MATRIX_3:def 4

.= (Line (N2,3)) "*" u2f by ANPROJ_8:93 ;

now :: thesis: ( (Line (N2,1)) . 1 = N2 * (1,1) & (Line (N2,1)) . 2 = N2 * (1,2) & (Line (N2,1)) . 3 = N2 * (1,3) & (Line (N2,2)) . 1 = N2 * (2,1) & (Line (N2,2)) . 2 = N2 * (2,2) & (Line (N2,2)) . 3 = N2 * (2,3) & (Line (N2,3)) . 1 = N2 * (3,1) & (Line (N2,3)) . 2 = N2 * (3,2) & (Line (N2,3)) . 3 = N2 * (3,3) & [1,1] in Indices N2 & [1,2] in Indices N2 & [1,3] in Indices N2 & [2,1] in Indices N2 & [2,2] in Indices N2 & [2,3] in Indices N2 & [3,1] in Indices N2 & [3,2] in Indices N2 & [3,3] in Indices N2 )

then reconsider l11 = (Line (N2,1)) . 1, l12 = (Line (N2,1)) . 2, l13 = (Line (N2,1)) . 3, l21 = (Line (N2,2)) . 1, l22 = (Line (N2,2)) . 2, l23 = (Line (N2,2)) . 3, l31 = (Line (N2,3)) . 1, l32 = (Line (N2,3)) . 2, l33 = (Line (N2,3)) . 3 as Element of F_Real ;
width N2 = 3
by MATRIX_0:23;

then ( 1 in Seg (width N2) & 2 in Seg (width N2) & 3 in Seg (width N2) ) by FINSEQ_1:1;

hence ( (Line (N2,1)) . 1 = N2 * (1,1) & (Line (N2,1)) . 2 = N2 * (1,2) & (Line (N2,1)) . 3 = N2 * (1,3) & (Line (N2,2)) . 1 = N2 * (2,1) & (Line (N2,2)) . 2 = N2 * (2,2) & (Line (N2,2)) . 3 = N2 * (2,3) & (Line (N2,3)) . 1 = N2 * (3,1) & (Line (N2,3)) . 2 = N2 * (3,2) & (Line (N2,3)) . 3 = N2 * (3,3) ) by MATRIX_0:def 7; :: thesis: ( [1,1] in Indices N2 & [1,2] in Indices N2 & [1,3] in Indices N2 & [2,1] in Indices N2 & [2,2] in Indices N2 & [2,3] in Indices N2 & [3,1] in Indices N2 & [3,2] in Indices N2 & [3,3] in Indices N2 )

thus ( [1,1] in Indices N2 & [1,2] in Indices N2 & [1,3] in Indices N2 & [2,1] in Indices N2 & [2,2] in Indices N2 & [2,3] in Indices N2 & [3,1] in Indices N2 & [3,2] in Indices N2 & [3,3] in Indices N2 ) by ANPROJ_8:1, MATRIX_0:23; :: thesis: verum

end;then ( 1 in Seg (width N2) & 2 in Seg (width N2) & 3 in Seg (width N2) ) by FINSEQ_1:1;

hence ( (Line (N2,1)) . 1 = N2 * (1,1) & (Line (N2,1)) . 2 = N2 * (1,2) & (Line (N2,1)) . 3 = N2 * (1,3) & (Line (N2,2)) . 1 = N2 * (2,1) & (Line (N2,2)) . 2 = N2 * (2,2) & (Line (N2,2)) . 3 = N2 * (2,3) & (Line (N2,3)) . 1 = N2 * (3,1) & (Line (N2,3)) . 2 = N2 * (3,2) & (Line (N2,3)) . 3 = N2 * (3,3) ) by MATRIX_0:def 7; :: thesis: ( [1,1] in Indices N2 & [1,2] in Indices N2 & [1,3] in Indices N2 & [2,1] in Indices N2 & [2,2] in Indices N2 & [2,3] in Indices N2 & [3,1] in Indices N2 & [3,2] in Indices N2 & [3,3] in Indices N2 )

thus ( [1,1] in Indices N2 & [1,2] in Indices N2 & [1,3] in Indices N2 & [2,1] in Indices N2 & [2,2] in Indices N2 & [2,3] in Indices N2 & [3,1] in Indices N2 & [3,2] in Indices N2 & [3,3] in Indices N2 ) by ANPROJ_8:1, MATRIX_0:23; :: thesis: verum

reconsider ru121 = u12f . 1, ru122 = u12f . 2, ru123 = u12f . 3 as Element of F_Real by XREAL_0:def 1;

( len (Line (N2,1)) = width N2 & len (Line (N2,2)) = width N2 & len (Line (N2,3)) = width N2 ) by MATRIX_0:def 7;

then A51: ( Line (N2,1) = <*l11,l12,l13*> & Line (N2,2) = <*l21,l22,l23*> & Line (N2,3) = <*l31,l32,l33*> ) by MATRIX_0:23, FINSEQ_1:45;

reconsider ru21 = u2 . 1, ru22 = u2 . 2, ru23 = u2 . 3 as Element of F_Real by XREAL_0:def 1;

A52: ( ru21 = a * (u12f . 1) & ru22 = a * (u12f . 2) & ru23 = a * (u12f . 3) ) by A3, A23, RVSUM_1:44;

len u2 = 3 by A29, EUCLID_8:50;

then A53: u2f = <*ru21,ru22,ru23*> by A10, FINSEQ_1:45;

reconsider t121 = v12 . 1, t122 = v12 . 2, t123 = v12 . 3 as Element of F_Real by A37, FINSEQ_1:45;

reconsider v12f = v12 as FinSequence of F_Real by RVSUM_1:145;

width N1 = 3 by MATRIX_0:24;

then A54: width N1 = len N2 by MATRIX_0:24;

A55: ( [1,1] in Indices (N1 * N2) & [1,2] in Indices (N1 * N2) & [1,3] in Indices (N1 * N2) & [2,1] in Indices (N1 * N2) & [2,2] in Indices (N1 * N2) & [2,3] in Indices (N1 * N2) & [3,1] in Indices (N1 * N2) & [3,2] in Indices (N1 * N2) & [3,3] in Indices (N1 * N2) ) by ANPROJ_8:1, MATRIX_0:23;

A56: width (N1 * N2) = len (<*u12f*> @) by A34, MATRIX_0:24;

u12 in TOP-REAL 3 ;

then u12f in REAL 3 by EUCLID:22, A3;

then A57: len u12f = 3 by EUCLID_8:50;

(N1 * N2) * (<*u12f*> @) is Matrix of 3,1,F_Real by A3, FINSEQ_3:153, ANPROJ_8:91;

then A58: ( [1,1] in Indices ((N1 * N2) * (<*u12f*> @)) & [2,1] in Indices ((N1 * N2) * (<*u12f*> @)) & [3,1] in Indices ((N1 * N2) * (<*u12f*> @)) ) by MATRIX_0:23, ANPROJ_8:2;

A59: u12f = <*ru121,ru122,ru123*> by A57, FINSEQ_1:45;

A60: ( Col (N2,1) = <*l11,l21,l31*> & Col (N2,2) = <*l12,l22,l32*> & Col (N2,3) = <*l13,l23,l33*> )

proof

end;

Dir v1 = Dir v12
now :: thesis: ( len (Col (N2,1)) = 3 & len (Col (N2,2)) = 3 & len (Col (N2,3)) = 3 & (Col (N2,1)) . 1 = l11 & (Col (N2,2)) . 1 = l12 & (Col (N2,3)) . 1 = l13 & (Col (N2,1)) . 2 = l21 & (Col (N2,2)) . 2 = l22 & (Col (N2,3)) . 2 = l23 & (Col (N2,1)) . 3 = l31 & (Col (N2,2)) . 3 = l32 & (Col (N2,3)) . 3 = l33 )

hence
( Col (N2,1) = <*l11,l21,l31*> & Col (N2,2) = <*l12,l22,l32*> & Col (N2,3) = <*l13,l23,l33*> )
by FINSEQ_1:45; :: thesis: verum
len N2 = 3
by MATRIX_0:24;

hence ( len (Col (N2,1)) = 3 & len (Col (N2,2)) = 3 & len (Col (N2,3)) = 3 ) by MATRIX_0:def 8; :: thesis: ( (Col (N2,1)) . 1 = l11 & (Col (N2,2)) . 1 = l12 & (Col (N2,3)) . 1 = l13 & (Col (N2,1)) . 2 = l21 & (Col (N2,2)) . 2 = l22 & (Col (N2,3)) . 2 = l23 & (Col (N2,1)) . 3 = l31 & (Col (N2,2)) . 3 = l32 & (Col (N2,3)) . 3 = l33 )

( len N2 = 3 & width N2 = 3 ) by MATRIX_0:24;

then ( dom N2 = Seg 3 & Seg (width N2) = Seg 3 ) by FINSEQ_1:def 3;

then ( 1 in dom N2 & 2 in dom N2 & 3 in dom N2 & 1 in Seg (width N2) & 2 in Seg (width N2) & 3 in Seg (width N2) ) by FINSEQ_1:1;

hence ( (Col (N2,1)) . 1 = l11 & (Col (N2,2)) . 1 = l12 & (Col (N2,3)) . 1 = l13 & (Col (N2,1)) . 2 = l21 & (Col (N2,2)) . 2 = l22 & (Col (N2,3)) . 2 = l23 & (Col (N2,1)) . 3 = l31 & (Col (N2,2)) . 3 = l32 & (Col (N2,3)) . 3 = l33 ) by MATRIX_0:42; :: thesis: verum

end;hence ( len (Col (N2,1)) = 3 & len (Col (N2,2)) = 3 & len (Col (N2,3)) = 3 ) by MATRIX_0:def 8; :: thesis: ( (Col (N2,1)) . 1 = l11 & (Col (N2,2)) . 1 = l12 & (Col (N2,3)) . 1 = l13 & (Col (N2,1)) . 2 = l21 & (Col (N2,2)) . 2 = l22 & (Col (N2,3)) . 2 = l23 & (Col (N2,1)) . 3 = l31 & (Col (N2,2)) . 3 = l32 & (Col (N2,3)) . 3 = l33 )

( len N2 = 3 & width N2 = 3 ) by MATRIX_0:24;

then ( dom N2 = Seg 3 & Seg (width N2) = Seg 3 ) by FINSEQ_1:def 3;

then ( 1 in dom N2 & 2 in dom N2 & 3 in dom N2 & 1 in Seg (width N2) & 2 in Seg (width N2) & 3 in Seg (width N2) ) by FINSEQ_1:1;

hence ( (Col (N2,1)) . 1 = l11 & (Col (N2,2)) . 1 = l12 & (Col (N2,3)) . 1 = l13 & (Col (N2,1)) . 2 = l21 & (Col (N2,2)) . 2 = l22 & (Col (N2,3)) . 2 = l23 & (Col (N2,1)) . 3 = l31 & (Col (N2,2)) . 3 = l32 & (Col (N2,3)) . 3 = l33 ) by MATRIX_0:42; :: thesis: verum

proof

hence
(homography N1) . ((homography N2) . P) = (homography (N1 * N2)) . P
by A7, A21; :: thesis: verum
ex c being Real st

( c <> 0 & v1 = c * v12 )

hence Dir v1 = Dir v12 by A6, A20, ANPROJ_1:22; :: thesis: verum

end;( c <> 0 & v1 = c * v12 )

proof

then
are_Prop v1,v12
by ANPROJ_1:1;
set c = a * b;

take a * b ; :: thesis: ( a * b <> 0 & v1 = (a * b) * v12 )

thus a * b <> 0 by A22, A24, XCMPLX_1:6; :: thesis: v1 = (a * b) * v12

.= (a * b) * <*(((N1 * N2) * (<*u12f*> @)) * (1,1)),(((N1 * N2) * (<*u12f*> @)) * (2,1)),(((N1 * N2) * (<*u12f*> @)) * (3,1))*> ;

hence v1 = (a * b) * v12 by A28, A37, A61; :: thesis: verum

end;take a * b ; :: thesis: ( a * b <> 0 & v1 = (a * b) * v12 )

thus a * b <> 0 by A22, A24, XCMPLX_1:6; :: thesis: v1 = (a * b) * v12

A61: now :: thesis: ( (N1 * (<*u1f*> @)) * (1,1) = (a * b) * (((N1 * N2) * (<*u12f*> @)) * (1,1)) & (N1 * (<*u1f*> @)) * (2,1) = (a * b) * (((N1 * N2) * (<*u12f*> @)) * (2,1)) & (N1 * (<*u1f*> @)) * (3,1) = (a * b) * (((N1 * N2) * (<*u12f*> @)) * (3,1)) )

<*((a * b) * (((N1 * N2) * (<*u12f*> @)) * (1,1))),((a * b) * (((N1 * N2) * (<*u12f*> @)) * (2,1))),((a * b) * (((N1 * N2) * (<*u12f*> @)) * (3,1)))*> =
(a * b) * |[(((N1 * N2) * (<*u12f*> @)) * (1,1)),(((N1 * N2) * (<*u12f*> @)) * (2,1)),(((N1 * N2) * (<*u12f*> @)) * (3,1))]|
by EUCLID_5:8
thus
(N1 * (<*u1f*> @)) * (1,1) = (a * b) * (((N1 * N2) * (<*u12f*> @)) * (1,1))
:: thesis: ( (N1 * (<*u1f*> @)) * (2,1) = (a * b) * (((N1 * N2) * (<*u12f*> @)) * (2,1)) & (N1 * (<*u1f*> @)) * (3,1) = (a * b) * (((N1 * N2) * (<*u12f*> @)) * (3,1)) )

end;proof

thus
(N1 * (<*u1f*> @)) * (2,1) = (a * b) * (((N1 * N2) * (<*u12f*> @)) * (2,1))
:: thesis: (N1 * (<*u1f*> @)) * (3,1) = (a * b) * (((N1 * N2) * (<*u12f*> @)) * (3,1))
v1 . 1 = (a * b) * (v12 . 1)

end;proof

hence
(N1 * (<*u1f*> @)) * (1,1) = (a * b) * (((N1 * N2) * (<*u12f*> @)) * (1,1))
by A45, A37, FINSEQ_1:45; :: thesis: verum
reconsider s1 = N1 * (1,1), s2 = N1 * (1,2), s3 = N1 * (1,3) as Element of F_Real ;

A62: (Line (N1,1)) "*" v2f = ((s1 * (<*l11,l12,l13*> "*" <*ru21,ru22,ru23*>)) + (s2 * (<*l21,l22,l23*> "*" <*ru21,ru22,ru23*>))) + (s3 * (<*l31,l32,l33*> "*" <*ru21,ru22,ru23*>)) by A51, A53, A48, A49, A50, A42, A46, ANPROJ_8:7

.= ((s1 * (((l11 * ru21) + (l12 * ru22)) + (l13 * ru23))) + (s2 * ((Line (N2,2)) "*" u2f))) + (s3 * ((Line (N2,3)) "*" u2f)) by A51, A53, ANPROJ_8:7

.= ((s1 * (((l11 * ru21) + (l12 * ru22)) + (l13 * ru23))) + (s2 * (((l21 * ru21) + (l22 * ru22)) + (l23 * ru23)))) + (s3 * ((Line (N2,3)) "*" u2f)) by A51, A53, ANPROJ_8:7

.= ((s1 * (((l11 * ru21) + (l12 * ru22)) + (l13 * ru23))) + (s2 * (((l21 * ru21) + (l22 * ru22)) + (l23 * ru23)))) + (s3 * (((l31 * ru21) + (l32 * ru22)) + (l33 * ru23))) by A51, A53, ANPROJ_8:7

.= a * ((((((s1 * l11) + (s2 * l21)) + (s3 * l31)) * ru121) + ((((s1 * l12) + (s2 * l22)) + (s3 * l32)) * ru122)) + ((((s1 * l13) + (s2 * l23)) + (s3 * l33)) * ru123)) by A52 ;

reconsider s121 = (N1 * N2) * (1,1), s122 = (N1 * N2) * (1,2), s123 = (N1 * N2) * (1,3) as Element of F_Real ;

A63: t121 = ((N1 * N2) * (<*u12f*> @)) * (1,1) by A37, FINSEQ_1:45

.= (Line ((N1 * N2),1)) "*" (Col ((<*u12f*> @),1)) by A56, A58, MATRIX_3:def 4

.= (Line ((N1 * N2),1)) "*" u12f by ANPROJ_8:93

.= <*s121,s122,s123*> "*" <*ru121,ru122,ru123*> by A59, A44, A43, MATRIX_0:24, FINSEQ_1:45

.= ((s121 * ru121) + (s122 * ru122)) + (s123 * ru123) by ANPROJ_8:7 ;

.= (N1 * (<*u1f*> @)) * (1,1) by A39, XCMPLX_1:52

.= v1 . 1 by A28, FINSEQ_1:45 ;

hence v1 . 1 = (a * b) * (v12 . 1) ; :: thesis: verum

end;A62: (Line (N1,1)) "*" v2f = ((s1 * (<*l11,l12,l13*> "*" <*ru21,ru22,ru23*>)) + (s2 * (<*l21,l22,l23*> "*" <*ru21,ru22,ru23*>))) + (s3 * (<*l31,l32,l33*> "*" <*ru21,ru22,ru23*>)) by A51, A53, A48, A49, A50, A42, A46, ANPROJ_8:7

.= ((s1 * (((l11 * ru21) + (l12 * ru22)) + (l13 * ru23))) + (s2 * ((Line (N2,2)) "*" u2f))) + (s3 * ((Line (N2,3)) "*" u2f)) by A51, A53, ANPROJ_8:7

.= ((s1 * (((l11 * ru21) + (l12 * ru22)) + (l13 * ru23))) + (s2 * (((l21 * ru21) + (l22 * ru22)) + (l23 * ru23)))) + (s3 * ((Line (N2,3)) "*" u2f)) by A51, A53, ANPROJ_8:7

.= ((s1 * (((l11 * ru21) + (l12 * ru22)) + (l13 * ru23))) + (s2 * (((l21 * ru21) + (l22 * ru22)) + (l23 * ru23)))) + (s3 * (((l31 * ru21) + (l32 * ru22)) + (l33 * ru23))) by A51, A53, ANPROJ_8:7

.= a * ((((((s1 * l11) + (s2 * l21)) + (s3 * l31)) * ru121) + ((((s1 * l12) + (s2 * l22)) + (s3 * l32)) * ru122)) + ((((s1 * l13) + (s2 * l23)) + (s3 * l33)) * ru123)) by A52 ;

reconsider s121 = (N1 * N2) * (1,1), s122 = (N1 * N2) * (1,2), s123 = (N1 * N2) * (1,3) as Element of F_Real ;

A63: t121 = ((N1 * N2) * (<*u12f*> @)) * (1,1) by A37, FINSEQ_1:45

.= (Line ((N1 * N2),1)) "*" (Col ((<*u12f*> @),1)) by A56, A58, MATRIX_3:def 4

.= (Line ((N1 * N2),1)) "*" u12f by ANPROJ_8:93

.= <*s121,s122,s123*> "*" <*ru121,ru122,ru123*> by A59, A44, A43, MATRIX_0:24, FINSEQ_1:45

.= ((s121 * ru121) + (s122 * ru122)) + (s123 * ru123) by ANPROJ_8:7 ;

now :: thesis: ( s121 = ((s1 * l11) + (s2 * l21)) + (s3 * l31) & s122 = ((s1 * l12) + (s2 * l22)) + (s3 * l32) & s123 = ((s1 * l13) + (s2 * l23)) + (s3 * l33) )

then (a * b) * t121 =
b * ((Line (N1,1)) "*" v2f)
by A63, A62
thus s121 =
(Line (N1,1)) "*" (Col (N2,1))
by A54, A55, MATRIX_3:def 4

.= <*s1,s2,s3*> "*" (Col (N2,1)) by A41, A40, MATRIX_0:24, FINSEQ_1:45

.= ((s1 * l11) + (s2 * l21)) + (s3 * l31) by A60, ANPROJ_8:7 ; :: thesis: ( s122 = ((s1 * l12) + (s2 * l22)) + (s3 * l32) & s123 = ((s1 * l13) + (s2 * l23)) + (s3 * l33) )

thus s122 = (Line (N1,1)) "*" (Col (N2,2)) by A54, A55, MATRIX_3:def 4

.= <*s1,s2,s3*> "*" (Col (N2,2)) by A41, A40, MATRIX_0:24, FINSEQ_1:45

.= ((s1 * l12) + (s2 * l22)) + (s3 * l32) by A60, ANPROJ_8:7 ; :: thesis: s123 = ((s1 * l13) + (s2 * l23)) + (s3 * l33)

thus s123 = (Line (N1,1)) "*" (Col (N2,3)) by A54, A55, MATRIX_3:def 4

.= <*s1,s2,s3*> "*" (Col (N2,3)) by A41, A40, MATRIX_0:24, FINSEQ_1:45

.= ((s1 * l13) + (s2 * l23)) + (s3 * l33) by A60, ANPROJ_8:7 ; :: thesis: verum

end;.= <*s1,s2,s3*> "*" (Col (N2,1)) by A41, A40, MATRIX_0:24, FINSEQ_1:45

.= ((s1 * l11) + (s2 * l21)) + (s3 * l31) by A60, ANPROJ_8:7 ; :: thesis: ( s122 = ((s1 * l12) + (s2 * l22)) + (s3 * l32) & s123 = ((s1 * l13) + (s2 * l23)) + (s3 * l33) )

thus s122 = (Line (N1,1)) "*" (Col (N2,2)) by A54, A55, MATRIX_3:def 4

.= <*s1,s2,s3*> "*" (Col (N2,2)) by A41, A40, MATRIX_0:24, FINSEQ_1:45

.= ((s1 * l12) + (s2 * l22)) + (s3 * l32) by A60, ANPROJ_8:7 ; :: thesis: s123 = ((s1 * l13) + (s2 * l23)) + (s3 * l33)

thus s123 = (Line (N1,1)) "*" (Col (N2,3)) by A54, A55, MATRIX_3:def 4

.= <*s1,s2,s3*> "*" (Col (N2,3)) by A41, A40, MATRIX_0:24, FINSEQ_1:45

.= ((s1 * l13) + (s2 * l23)) + (s3 * l33) by A60, ANPROJ_8:7 ; :: thesis: verum

.= (N1 * (<*u1f*> @)) * (1,1) by A39, XCMPLX_1:52

.= v1 . 1 by A28, FINSEQ_1:45 ;

hence v1 . 1 = (a * b) * (v12 . 1) ; :: thesis: verum

proof

thus
(N1 * (<*u1f*> @)) * (3,1) = (a * b) * (((N1 * N2) * (<*u12f*> @)) * (3,1))
:: thesis: verum
v1 . 2 = (a * b) * (v12 . 2)

end;proof

hence
(N1 * (<*u1f*> @)) * (2,1) = (a * b) * (((N1 * N2) * (<*u12f*> @)) * (2,1))
by A45, A37, FINSEQ_1:45; :: thesis: verum
reconsider s1 = N1 * (2,1), s2 = N1 * (2,2), s3 = N1 * (2,3) as Element of F_Real ;

A64: (Line (N1,2)) "*" v2f = ((s1 * (<*l11,l12,l13*> "*" <*ru21,ru22,ru23*>)) + (s2 * (<*l21,l22,l23*> "*" <*ru21,ru22,ru23*>))) + (s3 * (<*l31,l32,l33*> "*" <*ru21,ru22,ru23*>)) by A51, A53, A48, A49, A50, A42, A46, ANPROJ_8:7

.= ((s1 * (((l11 * ru21) + (l12 * ru22)) + (l13 * ru23))) + (s2 * ((Line (N2,2)) "*" u2f))) + (s3 * ((Line (N2,3)) "*" u2f)) by A51, A53, ANPROJ_8:7

.= ((s1 * (((l11 * ru21) + (l12 * ru22)) + (l13 * ru23))) + (s2 * (((l21 * ru21) + (l22 * ru22)) + (l23 * ru23)))) + (s3 * ((Line (N2,3)) "*" u2f)) by A51, A53, ANPROJ_8:7

.= ((s1 * (((l11 * ru21) + (l12 * ru22)) + (l13 * ru23))) + (s2 * (((l21 * ru21) + (l22 * ru22)) + (l23 * ru23)))) + (s3 * (((l31 * ru21) + (l32 * ru22)) + (l33 * ru23))) by A51, A53, ANPROJ_8:7

.= a * ((((((s1 * l11) + (s2 * l21)) + (s3 * l31)) * ru121) + ((((s1 * l12) + (s2 * l22)) + (s3 * l32)) * ru122)) + ((((s1 * l13) + (s2 * l23)) + (s3 * l33)) * ru123)) by A52 ;

reconsider s121 = (N1 * N2) * (2,1), s122 = (N1 * N2) * (2,2), s123 = (N1 * N2) * (2,3) as Element of F_Real ;

A65: t122 = ((N1 * N2) * (<*u12f*> @)) * (2,1) by A37, FINSEQ_1:45

.= (Line ((N1 * N2),2)) "*" (Col ((<*u12f*> @),1)) by A56, A58, MATRIX_3:def 4

.= (Line ((N1 * N2),2)) "*" u12f by ANPROJ_8:93

.= <*s121,s122,s123*> "*" <*ru121,ru122,ru123*> by A59, A44, A43, MATRIX_0:24, FINSEQ_1:45

.= ((s121 * ru121) + (s122 * ru122)) + (s123 * ru123) by ANPROJ_8:7 ;

.= (N1 * (<*u1f*> @)) * (2,1) by A39, XCMPLX_1:52

.= v1 . 2 by A28, FINSEQ_1:45 ;

hence v1 . 2 = (a * b) * (v12 . 2) ; :: thesis: verum

end;A64: (Line (N1,2)) "*" v2f = ((s1 * (<*l11,l12,l13*> "*" <*ru21,ru22,ru23*>)) + (s2 * (<*l21,l22,l23*> "*" <*ru21,ru22,ru23*>))) + (s3 * (<*l31,l32,l33*> "*" <*ru21,ru22,ru23*>)) by A51, A53, A48, A49, A50, A42, A46, ANPROJ_8:7

.= ((s1 * (((l11 * ru21) + (l12 * ru22)) + (l13 * ru23))) + (s2 * ((Line (N2,2)) "*" u2f))) + (s3 * ((Line (N2,3)) "*" u2f)) by A51, A53, ANPROJ_8:7

.= ((s1 * (((l11 * ru21) + (l12 * ru22)) + (l13 * ru23))) + (s2 * (((l21 * ru21) + (l22 * ru22)) + (l23 * ru23)))) + (s3 * ((Line (N2,3)) "*" u2f)) by A51, A53, ANPROJ_8:7

.= ((s1 * (((l11 * ru21) + (l12 * ru22)) + (l13 * ru23))) + (s2 * (((l21 * ru21) + (l22 * ru22)) + (l23 * ru23)))) + (s3 * (((l31 * ru21) + (l32 * ru22)) + (l33 * ru23))) by A51, A53, ANPROJ_8:7

.= a * ((((((s1 * l11) + (s2 * l21)) + (s3 * l31)) * ru121) + ((((s1 * l12) + (s2 * l22)) + (s3 * l32)) * ru122)) + ((((s1 * l13) + (s2 * l23)) + (s3 * l33)) * ru123)) by A52 ;

reconsider s121 = (N1 * N2) * (2,1), s122 = (N1 * N2) * (2,2), s123 = (N1 * N2) * (2,3) as Element of F_Real ;

A65: t122 = ((N1 * N2) * (<*u12f*> @)) * (2,1) by A37, FINSEQ_1:45

.= (Line ((N1 * N2),2)) "*" (Col ((<*u12f*> @),1)) by A56, A58, MATRIX_3:def 4

.= (Line ((N1 * N2),2)) "*" u12f by ANPROJ_8:93

.= <*s121,s122,s123*> "*" <*ru121,ru122,ru123*> by A59, A44, A43, MATRIX_0:24, FINSEQ_1:45

.= ((s121 * ru121) + (s122 * ru122)) + (s123 * ru123) by ANPROJ_8:7 ;

now :: thesis: ( s121 = ((s1 * l11) + (s2 * l21)) + (s3 * l31) & s122 = ((s1 * l12) + (s2 * l22)) + (s3 * l32) & s123 = ((s1 * l13) + (s2 * l23)) + (s3 * l33) )

then (a * b) * t122 =
b * ((Line (N1,2)) "*" v2f)
by A65, A64
thus s121 =
(Line (N1,2)) "*" (Col (N2,1))
by A54, A55, MATRIX_3:def 4

.= <*s1,s2,s3*> "*" (Col (N2,1)) by A41, A40, MATRIX_0:24, FINSEQ_1:45

.= ((s1 * l11) + (s2 * l21)) + (s3 * l31) by A60, ANPROJ_8:7 ; :: thesis: ( s122 = ((s1 * l12) + (s2 * l22)) + (s3 * l32) & s123 = ((s1 * l13) + (s2 * l23)) + (s3 * l33) )

thus s122 = (Line (N1,2)) "*" (Col (N2,2)) by A54, A55, MATRIX_3:def 4

.= <*s1,s2,s3*> "*" (Col (N2,2)) by A41, A40, MATRIX_0:24, FINSEQ_1:45

.= ((s1 * l12) + (s2 * l22)) + (s3 * l32) by A60, ANPROJ_8:7 ; :: thesis: s123 = ((s1 * l13) + (s2 * l23)) + (s3 * l33)

thus s123 = (Line (N1,2)) "*" (Col (N2,3)) by A54, A55, MATRIX_3:def 4

.= <*s1,s2,s3*> "*" (Col (N2,3)) by A41, A40, MATRIX_0:24, FINSEQ_1:45

.= ((s1 * l13) + (s2 * l23)) + (s3 * l33) by A60, ANPROJ_8:7 ; :: thesis: verum

end;.= <*s1,s2,s3*> "*" (Col (N2,1)) by A41, A40, MATRIX_0:24, FINSEQ_1:45

.= ((s1 * l11) + (s2 * l21)) + (s3 * l31) by A60, ANPROJ_8:7 ; :: thesis: ( s122 = ((s1 * l12) + (s2 * l22)) + (s3 * l32) & s123 = ((s1 * l13) + (s2 * l23)) + (s3 * l33) )

thus s122 = (Line (N1,2)) "*" (Col (N2,2)) by A54, A55, MATRIX_3:def 4

.= <*s1,s2,s3*> "*" (Col (N2,2)) by A41, A40, MATRIX_0:24, FINSEQ_1:45

.= ((s1 * l12) + (s2 * l22)) + (s3 * l32) by A60, ANPROJ_8:7 ; :: thesis: s123 = ((s1 * l13) + (s2 * l23)) + (s3 * l33)

thus s123 = (Line (N1,2)) "*" (Col (N2,3)) by A54, A55, MATRIX_3:def 4

.= <*s1,s2,s3*> "*" (Col (N2,3)) by A41, A40, MATRIX_0:24, FINSEQ_1:45

.= ((s1 * l13) + (s2 * l23)) + (s3 * l33) by A60, ANPROJ_8:7 ; :: thesis: verum

.= (N1 * (<*u1f*> @)) * (2,1) by A39, XCMPLX_1:52

.= v1 . 2 by A28, FINSEQ_1:45 ;

hence v1 . 2 = (a * b) * (v12 . 2) ; :: thesis: verum

proof

v1 . 3 = (a * b) * (v12 . 3)

end;proof

hence
(N1 * (<*u1f*> @)) * (3,1) = (a * b) * (((N1 * N2) * (<*u12f*> @)) * (3,1))
by A45, A37, FINSEQ_1:45; :: thesis: verum
reconsider s1 = N1 * (3,1), s2 = N1 * (3,2), s3 = N1 * (3,3) as Element of F_Real ;

A66: (Line (N1,3)) "*" v2f = ((s1 * (<*l11,l12,l13*> "*" <*ru21,ru22,ru23*>)) + (s2 * (<*l21,l22,l23*> "*" <*ru21,ru22,ru23*>))) + (s3 * (<*l31,l32,l33*> "*" <*ru21,ru22,ru23*>)) by A51, A53, A48, A49, A50, A42, A46, ANPROJ_8:7

.= ((s1 * (((l11 * ru21) + (l12 * ru22)) + (l13 * ru23))) + (s2 * ((Line (N2,2)) "*" u2f))) + (s3 * ((Line (N2,3)) "*" u2f)) by A51, A53, ANPROJ_8:7

.= ((s1 * (((l11 * ru21) + (l12 * ru22)) + (l13 * ru23))) + (s2 * (((l21 * ru21) + (l22 * ru22)) + (l23 * ru23)))) + (s3 * ((Line (N2,3)) "*" u2f)) by A51, A53, ANPROJ_8:7

.= ((s1 * (((l11 * ru21) + (l12 * ru22)) + (l13 * ru23))) + (s2 * (((l21 * ru21) + (l22 * ru22)) + (l23 * ru23)))) + (s3 * (((l31 * ru21) + (l32 * ru22)) + (l33 * ru23))) by A51, A53, ANPROJ_8:7

.= a * ((((((s1 * l11) + (s2 * l21)) + (s3 * l31)) * ru121) + ((((s1 * l12) + (s2 * l22)) + (s3 * l32)) * ru122)) + ((((s1 * l13) + (s2 * l23)) + (s3 * l33)) * ru123)) by A52 ;

reconsider s121 = (N1 * N2) * (3,1), s122 = (N1 * N2) * (3,2), s123 = (N1 * N2) * (3,3) as Element of F_Real ;

A67: t123 = ((N1 * N2) * (<*u12f*> @)) * (3,1) by A37, FINSEQ_1:45

.= (Line ((N1 * N2),3)) "*" (Col ((<*u12f*> @),1)) by A56, A58, MATRIX_3:def 4

.= (Line ((N1 * N2),3)) "*" u12f by ANPROJ_8:93

.= <*s121,s122,s123*> "*" <*ru121,ru122,ru123*> by A59, A44, A43, MATRIX_0:24, FINSEQ_1:45

.= ((s121 * ru121) + (s122 * ru122)) + (s123 * ru123) by ANPROJ_8:7 ;

.= (N1 * (<*u1f*> @)) * (3,1) by A39, XCMPLX_1:52

.= v1 . 3 by A28, FINSEQ_1:45 ;

hence v1 . 3 = (a * b) * (v12 . 3) ; :: thesis: verum

end;A66: (Line (N1,3)) "*" v2f = ((s1 * (<*l11,l12,l13*> "*" <*ru21,ru22,ru23*>)) + (s2 * (<*l21,l22,l23*> "*" <*ru21,ru22,ru23*>))) + (s3 * (<*l31,l32,l33*> "*" <*ru21,ru22,ru23*>)) by A51, A53, A48, A49, A50, A42, A46, ANPROJ_8:7

.= ((s1 * (((l11 * ru21) + (l12 * ru22)) + (l13 * ru23))) + (s2 * ((Line (N2,2)) "*" u2f))) + (s3 * ((Line (N2,3)) "*" u2f)) by A51, A53, ANPROJ_8:7

.= ((s1 * (((l11 * ru21) + (l12 * ru22)) + (l13 * ru23))) + (s2 * (((l21 * ru21) + (l22 * ru22)) + (l23 * ru23)))) + (s3 * ((Line (N2,3)) "*" u2f)) by A51, A53, ANPROJ_8:7

.= ((s1 * (((l11 * ru21) + (l12 * ru22)) + (l13 * ru23))) + (s2 * (((l21 * ru21) + (l22 * ru22)) + (l23 * ru23)))) + (s3 * (((l31 * ru21) + (l32 * ru22)) + (l33 * ru23))) by A51, A53, ANPROJ_8:7

.= a * ((((((s1 * l11) + (s2 * l21)) + (s3 * l31)) * ru121) + ((((s1 * l12) + (s2 * l22)) + (s3 * l32)) * ru122)) + ((((s1 * l13) + (s2 * l23)) + (s3 * l33)) * ru123)) by A52 ;

reconsider s121 = (N1 * N2) * (3,1), s122 = (N1 * N2) * (3,2), s123 = (N1 * N2) * (3,3) as Element of F_Real ;

A67: t123 = ((N1 * N2) * (<*u12f*> @)) * (3,1) by A37, FINSEQ_1:45

.= (Line ((N1 * N2),3)) "*" (Col ((<*u12f*> @),1)) by A56, A58, MATRIX_3:def 4

.= (Line ((N1 * N2),3)) "*" u12f by ANPROJ_8:93

.= <*s121,s122,s123*> "*" <*ru121,ru122,ru123*> by A59, A44, A43, MATRIX_0:24, FINSEQ_1:45

.= ((s121 * ru121) + (s122 * ru122)) + (s123 * ru123) by ANPROJ_8:7 ;

now :: thesis: ( s121 = ((s1 * l11) + (s2 * l21)) + (s3 * l31) & s122 = ((s1 * l12) + (s2 * l22)) + (s3 * l32) & s123 = ((s1 * l13) + (s2 * l23)) + (s3 * l33) )

then (a * b) * t123 =
b * ((Line (N1,3)) "*" v2f)
by A67, A66
thus s121 =
(Line (N1,3)) "*" (Col (N2,1))
by A54, A55, MATRIX_3:def 4

.= <*s1,s2,s3*> "*" (Col (N2,1)) by A41, A40, MATRIX_0:24, FINSEQ_1:45

.= ((s1 * l11) + (s2 * l21)) + (s3 * l31) by A60, ANPROJ_8:7 ; :: thesis: ( s122 = ((s1 * l12) + (s2 * l22)) + (s3 * l32) & s123 = ((s1 * l13) + (s2 * l23)) + (s3 * l33) )

thus s122 = (Line (N1,3)) "*" (Col (N2,2)) by A54, A55, MATRIX_3:def 4

.= <*s1,s2,s3*> "*" (Col (N2,2)) by A41, A40, MATRIX_0:24, FINSEQ_1:45

.= ((s1 * l12) + (s2 * l22)) + (s3 * l32) by A60, ANPROJ_8:7 ; :: thesis: s123 = ((s1 * l13) + (s2 * l23)) + (s3 * l33)

thus s123 = (Line (N1,3)) "*" (Col (N2,3)) by A54, A55, MATRIX_3:def 4

.= <*s1,s2,s3*> "*" (Col (N2,3)) by A41, A40, MATRIX_0:24, FINSEQ_1:45

.= ((s1 * l13) + (s2 * l23)) + (s3 * l33) by A60, ANPROJ_8:7 ; :: thesis: verum

end;.= <*s1,s2,s3*> "*" (Col (N2,1)) by A41, A40, MATRIX_0:24, FINSEQ_1:45

.= ((s1 * l11) + (s2 * l21)) + (s3 * l31) by A60, ANPROJ_8:7 ; :: thesis: ( s122 = ((s1 * l12) + (s2 * l22)) + (s3 * l32) & s123 = ((s1 * l13) + (s2 * l23)) + (s3 * l33) )

thus s122 = (Line (N1,3)) "*" (Col (N2,2)) by A54, A55, MATRIX_3:def 4

.= <*s1,s2,s3*> "*" (Col (N2,2)) by A41, A40, MATRIX_0:24, FINSEQ_1:45

.= ((s1 * l12) + (s2 * l22)) + (s3 * l32) by A60, ANPROJ_8:7 ; :: thesis: s123 = ((s1 * l13) + (s2 * l23)) + (s3 * l33)

thus s123 = (Line (N1,3)) "*" (Col (N2,3)) by A54, A55, MATRIX_3:def 4

.= <*s1,s2,s3*> "*" (Col (N2,3)) by A41, A40, MATRIX_0:24, FINSEQ_1:45

.= ((s1 * l13) + (s2 * l23)) + (s3 * l33) by A60, ANPROJ_8:7 ; :: thesis: verum

.= (N1 * (<*u1f*> @)) * (3,1) by A39, XCMPLX_1:52

.= v1 . 3 by A28, FINSEQ_1:45 ;

hence v1 . 3 = (a * b) * (v12 . 3) ; :: thesis: verum

.= (a * b) * <*(((N1 * N2) * (<*u12f*> @)) * (1,1)),(((N1 * N2) * (<*u12f*> @)) * (2,1)),(((N1 * N2) * (<*u12f*> @)) * (3,1))*> ;

hence v1 = (a * b) * v12 by A28, A37, A61; :: thesis: verum

hence Dir v1 = Dir v12 by A6, A20, ANPROJ_1:22; :: thesis: verum