let a11, a12, a13, a21, a22, a23, a31, a32, a33, b11, b12, b13, b21, b22, b23, b31, b32, b33 be Element of F_Real; for A, B being Matrix of 3,F_Real st A = <*<*a11,a12,a13*>,<*a21,a22,a23*>,<*a31,a32,a33*>*> & B = <*<*b11,b12,b13*>,<*b21,b22,b23*>,<*b31,b32,b33*>*> holds
A * B = <*<*(((a11 * b11) + (a12 * b21)) + (a13 * b31)),(((a11 * b12) + (a12 * b22)) + (a13 * b32)),(((a11 * b13) + (a12 * b23)) + (a13 * b33))*>,<*(((a21 * b11) + (a22 * b21)) + (a23 * b31)),(((a21 * b12) + (a22 * b22)) + (a23 * b32)),(((a21 * b13) + (a22 * b23)) + (a23 * b33))*>,<*(((a31 * b11) + (a32 * b21)) + (a33 * b31)),(((a31 * b12) + (a32 * b22)) + (a33 * b32)),(((a31 * b13) + (a32 * b23)) + (a33 * b33))*>*>
let A, B be Matrix of 3,F_Real; ( A = <*<*a11,a12,a13*>,<*a21,a22,a23*>,<*a31,a32,a33*>*> & B = <*<*b11,b12,b13*>,<*b21,b22,b23*>,<*b31,b32,b33*>*> implies A * B = <*<*(((a11 * b11) + (a12 * b21)) + (a13 * b31)),(((a11 * b12) + (a12 * b22)) + (a13 * b32)),(((a11 * b13) + (a12 * b23)) + (a13 * b33))*>,<*(((a21 * b11) + (a22 * b21)) + (a23 * b31)),(((a21 * b12) + (a22 * b22)) + (a23 * b32)),(((a21 * b13) + (a22 * b23)) + (a23 * b33))*>,<*(((a31 * b11) + (a32 * b21)) + (a33 * b31)),(((a31 * b12) + (a32 * b22)) + (a33 * b32)),(((a31 * b13) + (a32 * b23)) + (a33 * b33))*>*> )
assume that
A1:
A = <*<*a11,a12,a13*>,<*a21,a22,a23*>,<*a31,a32,a33*>*>
and
A2:
B = <*<*b11,b12,b13*>,<*b21,b22,b23*>,<*b31,b32,b33*>*>
; A * B = <*<*(((a11 * b11) + (a12 * b21)) + (a13 * b31)),(((a11 * b12) + (a12 * b22)) + (a13 * b32)),(((a11 * b13) + (a12 * b23)) + (a13 * b33))*>,<*(((a21 * b11) + (a22 * b21)) + (a23 * b31)),(((a21 * b12) + (a22 * b22)) + (a23 * b32)),(((a21 * b13) + (a22 * b23)) + (a23 * b33))*>,<*(((a31 * b11) + (a32 * b21)) + (a33 * b31)),(((a31 * b12) + (a32 * b22)) + (a33 * b32)),(((a31 * b13) + (a32 * b23)) + (a33 * b33))*>*>
A3:
( width A = 3 & len B = 3 )
by MATRIX_0:23;
A4:
( [1,1] in Indices (A * B) & [1,2] in Indices (A * B) & [1,3] in Indices (A * B) & [2,1] in Indices (A * B) & [2,2] in Indices (A * B) & [2,3] in Indices (A * B) & [3,1] in Indices (A * B) & [3,2] in Indices (A * B) & [3,3] in Indices (A * B) )
by ANPROJ_8:1, MATRIX_0:23;
A5:
( Line (A,1) = <*a11,a12,a13*> & Line (A,2) = <*a21,a22,a23*> & Line (A,3) = <*a31,a32,a33*> )
by A1, Th05;
A6:
( Col (B,1) = <*b11,b21,b31*> & Col (B,2) = <*b12,b22,b32*> & Col (B,3) = <*b13,b23,b33*> )
by A2, Th06;
now ( (A * B) * (1,1) = ((a11 * b11) + (a12 * b21)) + (a13 * b31) & (A * B) * (1,2) = ((a11 * b12) + (a12 * b22)) + (a13 * b32) & (A * B) * (1,3) = ((a11 * b13) + (a12 * b23)) + (a13 * b33) & (A * B) * (2,1) = ((a21 * b11) + (a22 * b21)) + (a23 * b31) & (A * B) * (2,2) = ((a21 * b12) + (a22 * b22)) + (a23 * b32) & (A * B) * (2,3) = ((a21 * b13) + (a22 * b23)) + (a23 * b33) & (A * B) * (3,1) = ((a31 * b11) + (a32 * b21)) + (a33 * b31) & (A * B) * (3,2) = ((a31 * b12) + (a32 * b22)) + (a33 * b32) & (A * B) * (3,3) = ((a31 * b13) + (a32 * b23)) + (a33 * b33) )thus (A * B) * (1,1) =
(Line (A,1)) "*" (Col (B,1))
by A3, A4, MATRIX_3:def 4
.=
((a11 * b11) + (a12 * b21)) + (a13 * b31)
by A5, A6, ANPROJ_8:7
;
( (A * B) * (1,2) = ((a11 * b12) + (a12 * b22)) + (a13 * b32) & (A * B) * (1,3) = ((a11 * b13) + (a12 * b23)) + (a13 * b33) & (A * B) * (2,1) = ((a21 * b11) + (a22 * b21)) + (a23 * b31) & (A * B) * (2,2) = ((a21 * b12) + (a22 * b22)) + (a23 * b32) & (A * B) * (2,3) = ((a21 * b13) + (a22 * b23)) + (a23 * b33) & (A * B) * (3,1) = ((a31 * b11) + (a32 * b21)) + (a33 * b31) & (A * B) * (3,2) = ((a31 * b12) + (a32 * b22)) + (a33 * b32) & (A * B) * (3,3) = ((a31 * b13) + (a32 * b23)) + (a33 * b33) )thus (A * B) * (1,2) =
(Line (A,1)) "*" (Col (B,2))
by A3, A4, MATRIX_3:def 4
.=
((a11 * b12) + (a12 * b22)) + (a13 * b32)
by A5, A6, ANPROJ_8:7
;
( (A * B) * (1,3) = ((a11 * b13) + (a12 * b23)) + (a13 * b33) & (A * B) * (2,1) = ((a21 * b11) + (a22 * b21)) + (a23 * b31) & (A * B) * (2,2) = ((a21 * b12) + (a22 * b22)) + (a23 * b32) & (A * B) * (2,3) = ((a21 * b13) + (a22 * b23)) + (a23 * b33) & (A * B) * (3,1) = ((a31 * b11) + (a32 * b21)) + (a33 * b31) & (A * B) * (3,2) = ((a31 * b12) + (a32 * b22)) + (a33 * b32) & (A * B) * (3,3) = ((a31 * b13) + (a32 * b23)) + (a33 * b33) )thus (A * B) * (1,3) =
(Line (A,1)) "*" (Col (B,3))
by A3, A4, MATRIX_3:def 4
.=
((a11 * b13) + (a12 * b23)) + (a13 * b33)
by A5, A6, ANPROJ_8:7
;
( (A * B) * (2,1) = ((a21 * b11) + (a22 * b21)) + (a23 * b31) & (A * B) * (2,2) = ((a21 * b12) + (a22 * b22)) + (a23 * b32) & (A * B) * (2,3) = ((a21 * b13) + (a22 * b23)) + (a23 * b33) & (A * B) * (3,1) = ((a31 * b11) + (a32 * b21)) + (a33 * b31) & (A * B) * (3,2) = ((a31 * b12) + (a32 * b22)) + (a33 * b32) & (A * B) * (3,3) = ((a31 * b13) + (a32 * b23)) + (a33 * b33) )thus (A * B) * (2,1) =
(Line (A,2)) "*" (Col (B,1))
by A3, A4, MATRIX_3:def 4
.=
((a21 * b11) + (a22 * b21)) + (a23 * b31)
by A5, A6, ANPROJ_8:7
;
( (A * B) * (2,2) = ((a21 * b12) + (a22 * b22)) + (a23 * b32) & (A * B) * (2,3) = ((a21 * b13) + (a22 * b23)) + (a23 * b33) & (A * B) * (3,1) = ((a31 * b11) + (a32 * b21)) + (a33 * b31) & (A * B) * (3,2) = ((a31 * b12) + (a32 * b22)) + (a33 * b32) & (A * B) * (3,3) = ((a31 * b13) + (a32 * b23)) + (a33 * b33) )thus (A * B) * (2,2) =
(Line (A,2)) "*" (Col (B,2))
by A3, A4, MATRIX_3:def 4
.=
((a21 * b12) + (a22 * b22)) + (a23 * b32)
by A5, A6, ANPROJ_8:7
;
( (A * B) * (2,3) = ((a21 * b13) + (a22 * b23)) + (a23 * b33) & (A * B) * (3,1) = ((a31 * b11) + (a32 * b21)) + (a33 * b31) & (A * B) * (3,2) = ((a31 * b12) + (a32 * b22)) + (a33 * b32) & (A * B) * (3,3) = ((a31 * b13) + (a32 * b23)) + (a33 * b33) )thus (A * B) * (2,3) =
(Line (A,2)) "*" (Col (B,3))
by A3, A4, MATRIX_3:def 4
.=
((a21 * b13) + (a22 * b23)) + (a23 * b33)
by A5, A6, ANPROJ_8:7
;
( (A * B) * (3,1) = ((a31 * b11) + (a32 * b21)) + (a33 * b31) & (A * B) * (3,2) = ((a31 * b12) + (a32 * b22)) + (a33 * b32) & (A * B) * (3,3) = ((a31 * b13) + (a32 * b23)) + (a33 * b33) )thus (A * B) * (3,1) =
(Line (A,3)) "*" (Col (B,1))
by A3, A4, MATRIX_3:def 4
.=
((a31 * b11) + (a32 * b21)) + (a33 * b31)
by A5, A6, ANPROJ_8:7
;
( (A * B) * (3,2) = ((a31 * b12) + (a32 * b22)) + (a33 * b32) & (A * B) * (3,3) = ((a31 * b13) + (a32 * b23)) + (a33 * b33) )thus (A * B) * (3,2) =
(Line (A,3)) "*" (Col (B,2))
by A3, A4, MATRIX_3:def 4
.=
((a31 * b12) + (a32 * b22)) + (a33 * b32)
by A5, A6, ANPROJ_8:7
;
(A * B) * (3,3) = ((a31 * b13) + (a32 * b23)) + (a33 * b33)thus (A * B) * (3,3) =
(Line (A,3)) "*" (Col (B,3))
by A3, A4, MATRIX_3:def 4
.=
((a31 * b13) + (a32 * b23)) + (a33 * b33)
by A5, A6, ANPROJ_8:7
;
verum end;
hence
A * B = <*<*(((a11 * b11) + (a12 * b21)) + (a13 * b31)),(((a11 * b12) + (a12 * b22)) + (a13 * b32)),(((a11 * b13) + (a12 * b23)) + (a13 * b33))*>,<*(((a21 * b11) + (a22 * b21)) + (a23 * b31)),(((a21 * b12) + (a22 * b22)) + (a23 * b32)),(((a21 * b13) + (a22 * b23)) + (a23 * b33))*>,<*(((a31 * b11) + (a32 * b21)) + (a33 * b31)),(((a31 * b12) + (a32 * b22)) + (a33 * b32)),(((a31 * b13) + (a32 * b23)) + (a33 * b33))*>*>
by MATRIXR2:37; verum