let a be Real; :: thesis: for n being Nat

for M being Matrix of n,REAL holds |:(a * M):| = |.a.| * |:M:|

let n be Nat; :: thesis: for M being Matrix of n,REAL holds |:(a * M):| = |.a.| * |:M:|

let M be Matrix of n,REAL; :: thesis: |:(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)

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; :: thesis: verum

for M being Matrix of n,REAL holds |:(a * M):| = |.a.| * |:M:|

let n be Nat; :: thesis: for M being Matrix of n,REAL holds |:(a * M):| = |.a.| * |:M:|

let M be Matrix of n,REAL; :: thesis: |:(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

width (|.a.| * |:M:|) = width |:M:|
by MATRIXR1:27;
A4:
Indices (a * M) = Indices M
by MATRIXR1:28;

A5: Indices (a * M) = Indices M by MATRIXR1:28;

let i, j be Nat; :: thesis: ( [i,j] in Indices |:(a * M):| implies |:(a * M):| * (i,j) = (|.a.| * |:M:|) * (i,j) )

assume A6: [i,j] in Indices |:(a * M):| ; :: thesis: |:(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) ; :: thesis: verum

end;A5: Indices (a * M) = Indices M by MATRIXR1:28;

let i, j be Nat; :: thesis: ( [i,j] in Indices |:(a * M):| implies |:(a * M):| * (i,j) = (|.a.| * |:M:|) * (i,j) )

assume A6: [i,j] in Indices |:(a * M):| ; :: thesis: |:(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) ; :: thesis: verum

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; :: thesis: verum