let a, b, c be non zero Element of F_Real; for M1, M2 being Matrix of 3,F_Real st M1 = <*<*a,0,0*>,<*0,b,0*>,<*0,0,c*>*> & M2 = <*<*(1 / a),0,0*>,<*0,(1 / b),0*>,<*0,0,(1 / c)*>*> holds
( M1 * M2 = 1. (F_Real,3) & M2 * M1 = 1. (F_Real,3) )
let M1, M2 be Matrix of 3,F_Real; ( M1 = <*<*a,0,0*>,<*0,b,0*>,<*0,0,c*>*> & M2 = <*<*(1 / a),0,0*>,<*0,(1 / b),0*>,<*0,0,(1 / c)*>*> implies ( M1 * M2 = 1. (F_Real,3) & M2 * M1 = 1. (F_Real,3) ) )
assume that
A1:
M1 = <*<*a,0,0*>,<*0,b,0*>,<*0,0,c*>*>
and
A2:
M2 = <*<*(1 / a),0,0*>,<*0,(1 / b),0*>,<*0,0,(1 / c)*>*>
; ( M1 * M2 = 1. (F_Real,3) & M2 * M1 = 1. (F_Real,3) )
reconsider z = 0 as Element of F_Real ;
reconsider ia = 1 / a, ib = 1 / b, ic = 1 / c as Element of F_Real by XREAL_0:def 1;
A4:
M2 = <*<*ia,z,z*>,<*z,ib,z*>,<*z,z,ic*>*>
by A2;
not a is zero
;
then A5:
( a * ia = 1 & b * ib = 1 & c * ic = 1 )
by XCMPLX_1:106;
A6:
len (M1 * M2) = 3
by MATRIX_0:23;
( (M1 * M2) . 1 = <*(((a * ia) + (z * z)) + (z * z)),(((a * z) + (z * ib)) + (z * z)),(((a * z) + (z * z)) + (z * ic))*> & (M1 * M2) . 2 = <*(((z * ia) + (b * z)) + (z * z)),(((z * z) + (b * ib)) + (z * z)),(((z * z) + (b * z)) + (z * ic))*> & (M1 * M2) . 3 = <*(((z * ia) + (z * z)) + (c * z)),(((z * z) + (z * ib)) + (c * z)),(((z * z) + (z * z)) + (c * ic))*> )
by A1, A2, Lem01;
hence
M1 * M2 = 1. (F_Real,3)
by A6, A5, FINSEQ_1:45, Th01; M2 * M1 = 1. (F_Real,3)
A7:
len (M2 * M1) = 3
by MATRIX_0:23;
( (M2 * M1) . 1 = <*(((ia * a) + (z * z)) + (z * z)),(((ia * z) + (z * b)) + (z * z)),(((ia * z) + (z * z)) + (z * c))*> & (M2 * M1) . 2 = <*(((z * a) + (ib * z)) + (z * z)),(((z * z) + (ib * b)) + (z * z)),(((z * z) + (ib * z)) + (z * c))*> & (M2 * M1) . 3 = <*(((z * a) + (z * z)) + (ic * z)),(((z * z) + (z * b)) + (ic * z)),(((z * z) + (z * z)) + (ic * c))*> )
by A1, A4, Lem01;
hence
M2 * M1 = 1. (F_Real,3)
by A7, A5, FINSEQ_1:45, Th01; verum