let i, j be Nat; :: thesis: for a being complex number
for M being Matrix of COMPLEX st [i,j] in Indices M holds
(a * M) * i,j = a * (M * i,j)
let a be complex number ; :: thesis: for M being Matrix of COMPLEX st [i,j] in Indices M holds
(a * M) * i,j = a * (M * i,j)
let M be Matrix of COMPLEX ; :: thesis: ( [i,j] in Indices M implies (a * M) * i,j = a * (M * i,j) )
assume A1: [i,j] in Indices M ; :: thesis: (a * M) * i,j = a * (M * i,j)
a in COMPLEX by XCMPLX_0:def 2;
then reconsider aa = a as Element of F_Complex by COMPLFLD:def 1;
A2: COMPLEX2Field (a * M) = COMPLEX2Field (Field2COMPLEX (aa * (COMPLEX2Field M))) by MATRIX_5:def 7
.= aa * (COMPLEX2Field M) by MATRIX_5:6 ;
reconsider m1 = COMPLEX2Field M as Matrix of COMPLEX by COMPLFLD:def 1;
A3: M * i,j = m1 * i,j by MATRIX_5:def 1
.= (COMPLEX2Field M) * i,j by COMPLFLD:def 1 ;
reconsider m = COMPLEX2Field (a * M) as Matrix of COMPLEX by COMPLFLD:def 1;
A4: [i,j] in Indices (COMPLEX2Field M) by A1, MATRIX_5:def 1;
(a * M) * i,j = m * i,j by MATRIX_5:def 1
.= (aa * (COMPLEX2Field M)) * i,j by A2, COMPLFLD:def 1
.= aa * ((COMPLEX2Field M) * i,j) by A4, MATRIX_3:def 5
.= a * ((COMPLEX2Field M) * i,j) ;
hence (a * M) * i,j = a * (M * i,j) by A3; :: thesis: verum