let a be Complex; for M being Matrix of COMPLEX holds (a * M) *' = (a *') * (M *')
let M be Matrix of COMPLEX; (a * M) *' = (a *') * (M *')
reconsider aa = a as Element of COMPLEX by XCMPLX_0:def 2;
A1:
len (a * M) = len M
by Th2;
A2:
width (a * M) = width M
by Th2;
A3:
width M = width (M *')
by Def1;
A4:
len ((a * M) *') = len (a * M)
by Def1;
A5:
width ((a * M) *') = width (a * M)
by Def1;
A6:
len M = len (M *')
by Def1;
A7:
now for i, j being Nat st [i,j] in Indices ((a * M) *') holds
((a * M) *') * (i,j) = ((a *') * (M *')) * (i,j)let i,
j be
Nat;
( [i,j] in Indices ((a * M) *') implies ((a * M) *') * (i,j) = ((a *') * (M *')) * (i,j) )assume A8:
[i,j] in Indices ((a * M) *')
;
((a * M) *') * (i,j) = ((a *') * (M *')) * (i,j)then A9:
1
<= i
by Th1;
A10:
1
<= j
by A8, Th1;
A11:
j <= width (a * M)
by A5, A8, Th1;
A12:
i <= len (a * M)
by A4, A8, Th1;
then A13:
[i,j] in Indices M
by A1, A2, A9, A10, A11, Th1;
A14:
[i,j] in Indices (M *')
by A1, A6, A2, A3, A9, A12, A10, A11, Th1;
[i,j] in Indices (a * M)
by A9, A12, A10, A11, Th1;
then
((a * M) *') * (
i,
j)
= ((a * M) * (i,j)) *'
by Def1;
hence ((a * M) *') * (
i,
j) =
(aa * (M * (i,j))) *'
by A13, Th3
.=
(aa *') * ((M * (i,j)) *')
by COMPLEX1:35
.=
(a *') * ((M *') * (i,j))
by A13, Def1
.=
((a *') * (M *')) * (
i,
j)
by A14, Th3
;
verum end;
len ((a *') * (M *')) = len (M *')
by Th2;
then
len ((a *') * (M *')) = len M
by Def1;
then A15:
len ((a * M) *') = len ((a *') * (M *'))
by A4, Th2;
width ((a *') * (M *')) = width (M *')
by Th2;
then
width ((a *') * (M *')) = width M
by Def1;
hence
(a * M) *' = (a *') * (M *')
by A15, A5, A7, Th2, MATRIX_0:21; verum