let i, j be Nat; :: thesis: for a being Complex
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; :: 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)) )
reconsider m1 = COMPLEX2Field M as Matrix of COMPLEX by COMPLFLD:def 1;
A1: M * (i,j) = m1 * (i,j) by MATRIX_5:def 1
.= (COMPLEX2Field M) * (i,j) by COMPLFLD:def 1 ;
assume [i,j] in Indices M ; :: thesis: (a * M) * (i,j) = a * (M * (i,j))
then A2: [i,j] in Indices (COMPLEX2Field M) by MATRIX_5:def 1;
a in COMPLEX by XCMPLX_0:def 2;
then reconsider aa = a as Element of F_Complex by COMPLFLD:def 1;
reconsider m = COMPLEX2Field (a * M) as Matrix of COMPLEX by COMPLFLD:def 1;
A3: COMPLEX2Field (a * M) = COMPLEX2Field (Field2COMPLEX (aa * (COMPLEX2Field M))) by MATRIX_5:def 7
.= aa * (COMPLEX2Field M) by MATRIX_5:6 ;
(a * M) * (i,j) = m * (i,j) by MATRIX_5:def 1
.= (aa * (COMPLEX2Field M)) * (i,j) by A3, COMPLFLD:def 1
.= aa * ((COMPLEX2Field M) * (i,j)) by A2, MATRIX_3:def 5
.= a * ((COMPLEX2Field M) * (i,j)) ;
hence (a * M) * (i,j) = a * (M * (i,j)) by A1; :: thesis: verum