let a, b be Real; for A being Matrix of REAL holds (a + b) * A = (a * A) + (b * A)
let A be Matrix of REAL; (a + b) * A = (a * A) + (b * A)
A1:
( len (a * A) = len A & width (a * A) = width A )
by MATRIXR1:27;
A2:
( len ((a + b) * A) = len A & width ((a + b) * A) = width A )
by MATRIXR1:27;
A3:
for i, j being Nat st [i,j] in Indices ((a + b) * A) holds
((a + b) * A) * (i,j) = ((a * A) + (b * A)) * (i,j)
proof
let i,
j be
Nat;
( [i,j] in Indices ((a + b) * A) implies ((a + b) * A) * (i,j) = ((a * A) + (b * A)) * (i,j) )
assume A4:
[i,j] in Indices ((a + b) * A)
;
((a + b) * A) * (i,j) = ((a * A) + (b * A)) * (i,j)
reconsider i0 =
i,
j0 =
j as
Nat ;
A5:
Indices ((a + b) * A) = Indices A
by A2, MATRIX_4:55;
Indices (a * A) = Indices A
by A1, MATRIX_4:55;
then ((a * A) + (b * A)) * (
i,
j) =
((a * A) * (i0,j0)) + ((b * A) * (i0,j0))
by A4, A5, MATRIXR1:25
.=
(a * (A * (i0,j0))) + ((b * A) * (i0,j0))
by A4, A5, MATRIXR1:29
.=
(a * (A * (i0,j0))) + (b * (A * (i0,j0)))
by A4, A5, MATRIXR1:29
.=
(a + b) * (A * (i,j))
;
hence
((a + b) * A) * (
i,
j)
= ((a * A) + (b * A)) * (
i,
j)
by A4, A5, MATRIXR1:29;
verum
end;
( len ((a * A) + (b * A)) = len (a * A) & width ((a * A) + (b * A)) = width (a * A) )
by MATRIX_3:def 3;
hence
(a + b) * A = (a * A) + (b * A)
by A2, A1, A3, MATRIX_0:21; verum