let a be Real; for n being Nat
for M being Matrix of n,REAL holds |:(a * M):| = |.a.| * |:M:|
let n be Nat; for M being Matrix of n,REAL holds |:(a * M):| = |.a.| * |:M:|
let M be Matrix of n,REAL; |:(a * M):| = |.a.| * |:M:|
A1:
( len (a * M) = len M & width (a * M) = width M )
by MATRIXR1:27;
len (|.a.| * |:M:|) = len |:M:|
by MATRIXR1:27;
then A2:
len (|.a.| * |:M:|) = len M
by Def7;
A3:
for i, j being Nat st [i,j] in Indices |:(a * M):| holds
|:(a * M):| * (i,j) = (|.a.| * |:M:|) * (i,j)
proof
A4:
Indices (a * M) = Indices M
by MATRIXR1:28;
A5:
Indices (a * M) = Indices M
by MATRIXR1:28;
let i,
j be
Nat;
( [i,j] in Indices |:(a * M):| implies |:(a * M):| * (i,j) = (|.a.| * |:M:|) * (i,j) )
assume A6:
[i,j] in Indices |:(a * M):|
;
|:(a * M):| * (i,j) = (|.a.| * |:M:|) * (i,j)
A7:
Indices |:M:| = Indices M
by Th5;
A8:
Indices |:(a * M):| = Indices (a * M)
by Th5;
then A9:
|:(a * M):| * (
i,
j) =
|.((a * M) * (i,j)).|
by A6, Def7
.=
|.(a * (M * (i,j))).|
by A6, A8, A4, Th4
.=
|.a.| * |.(M * (i,j)).|
by COMPLEX1:65
;
(|.a.| * |:M:|) * (
i,
j) =
|.a.| * (|:M:| * (i,j))
by A6, A8, A5, Th4, A7
.=
|:(a * M):| * (
i,
j)
by A6, A8, A9, A5, Def7
;
hence
|:(a * M):| * (
i,
j)
= (|.a.| * |:M:|) * (
i,
j)
;
verum
end;
width (|.a.| * |:M:|) = width |:M:|
by MATRIXR1:27;
then A10:
width (|.a.| * |:M:|) = width M
by Def7;
( len |:(a * M):| = len (a * M) & width |:(a * M):| = width (a * M) )
by Def7;
hence
|:(a * M):| = |.a.| * |:M:|
by A1, A2, A10, A3, MATRIX_0:21; verum