let a, b, c be Element of F_Real; :: thesis:
let M, N be Matrix of 3,F_Real; :: thesis:
assume A1: N = <*<*a,0,0*>,<*0,b,0*>,<*0,0,c*>*> ; :: thesis:
reconsider a11 = a, a12 = 0 , a13 = 0 , a21 = 0 , a22 = b, a23 = 0 , a31 = 0 , a32 = 0 , a33 = c, b11 = M * (1,1), b12 = M * (1,2), b13 = M * (1,3), b21 = M * (2,1), b22 = M * (2,2), b23 = M * (2,3), b31 = M * (3,1), b32 = M * (3,2), b33 = M * (3,3) as Element of F_Real ;
A2: M = <*<*b11,b12,b13*>,<*b21,b22,b23*>,<*b31,b32,b33*>*> by MATRIXR2:37;
then A3: ( (N * M) * (1,1) = ((a11 * b11) + (a12 * b21)) + (a13 * b31) & (N * M) * (1,2) = ((a11 * b12) + (a12 * b22)) + (a13 * b32) & (N * M) * (1,3) = ((a11 * b13) + (a12 * b23)) + (a13 * b33) & (N * M) * (2,1) = ((a21 * b11) + (a22 * b21)) + (a23 * b31) & (N * M) * (2,2) = ((a21 * b12) + (a22 * b22)) + (a23 * b32) & (N * M) * (2,3) = ((a21 * b13) + (a22 * b23)) + (a23 * b33) & (N * M) * (3,1) = ((a31 * b11) + (a32 * b21)) + (a33 * b31) & (N * M) * (3,2) = ((a31 * b12) + (a32 * b22)) + (a33 * b32) & (N * M) * (3,3) = ((a31 * b13) + (a32 * b23)) + (a33 * b33) ) by A1, Lem09;
reconsider c11 = a * b11, c12 = a * b12, c13 = a * b13, c21 = b * b21, c22 = b * b22, c23 = b * b23, c31 = c * b31, c32 = c * b32, c33 = c * b33 as Element of F_Real ;
A4: N * M = <*<*c11,c12,c13*>,<*c21,c22,c23*>,<*c31,c32,c33*>*> by A3, MATRIXR2:37;
M @ = <*<*b11,b21,b31*>,<*b12,b22,b32*>,<*b13,b23,b33*>*> by A2, ANPROJ_8:22;
then ( ((M @) * (N * M)) * (1,1) = ((b11 * (a * b11)) + (b21 * (b * b21))) + (b31 * (c * b31)) & ((M @) * (N * M)) * (1,2) = ((b11 * (a * b12)) + (b21 * (b * b22))) + (b31 * (c * b32)) & ((M @) * (N * M)) * (1,3) = ((b11 * (a * b13)) + (b21 * (b * b23))) + (b31 * (c * b33)) & ((M @) * (N * M)) * (2,1) = ((b12 * (a * b11)) + (b22 * (b * b21))) + (b32 * (c * b31)) & ((M @) * (N * M)) * (2,2) = ((b12 * (a * b12)) + (b22 * (b * b22))) + (b32 * (c * b32)) & ((M @) * (N * M)) * (2,3) = ((b12 * (a * b13)) + (b22 * (b * b23))) + (b32 * (c * b33)) & ((M @) * (N * M)) * (3,1) = ((b13 * (a * b11)) + (b23 * (b * b21))) + (b33 * (c * b31)) & ((M @) * (N * M)) * (3,2) = ((b13 * (a * b12)) + (b23 * (b * b22))) + (b33 * (c * b32)) & ((M @) * (N * M)) * (3,3) = ((b13 * (a * b13)) + (b23 * (b * b23))) + (b33 * (c * b33)) ) by A4, Lem09;
hence ( ((M @) * (N * M)) * (1,1) = (((a * (M * (1,1))) * (M * (1,1))) + ((b * (M * (2,1))) * (M * (2,1)))) + ((c * (M * (3,1))) * (M * (3,1))) & ((M @) * (N * M)) * (1,2) = (((a * (M * (1,1))) * (M * (1,2))) + ((b * (M * (2,1))) * (M * (2,2)))) + ((c * (M * (3,1))) * (M * (3,2))) & ((M @) * (N * M)) * (1,3) = (((a * (M * (1,1))) * (M * (1,3))) + ((b * (M * (2,1))) * (M * (2,3)))) + ((c * (M * (3,1))) * (M * (3,3))) & ((M @) * (N * M)) * (2,1) = (((a * (M * (1,2))) * (M * (1,1))) + ((b * (M * (2,2))) * (M * (2,1)))) + ((c * (M * (3,2))) * (M * (3,1))) & ((M @) * (N * M)) * (2,2) = (((a * (M * (1,2))) * (M * (1,2))) + ((b * (M * (2,2))) * (M * (2,2)))) + ((c * (M * (3,2))) * (M * (3,2))) & ((M @) * (N * M)) * (2,3) = (((a * (M * (1,2))) * (M * (1,3))) + ((b * (M * (2,2))) * (M * (2,3)))) + ((c * (M * (3,2))) * (M * (3,3))) & ((M @) * (N * M)) * (3,1) = (((a * (M * (1,3))) * (M * (1,1))) + ((b * (M * (2,3))) * (M * (2,1)))) + ((c * (M * (3,3))) * (M * (3,1))) & ((M @) * (N * M)) * (3,2) = (((a * (M * (1,3))) * (M * (1,2))) + ((b * (M * (2,3))) * (M * (2,2)))) + ((c * (M * (3,3))) * (M * (3,2))) & ((M @) * (N * M)) * (3,3) = (((a * (M * (1,3))) * (M * (1,3))) + ((b * (M * (2,3))) * (M * (2,3)))) + ((c * (M * (3,3))) * (M * (3,3))) ) ; :: thesis: