let a, b be Real; :: thesis: for A being Matrix of REAL holds (a + b) * A = (a * A) + (b * A)
let A be Matrix of REAL ; :: thesis: (a + b) * A = (a * A) + (b * A)
A1:
( len ((a + b) * A) = len A & width ((a + b) * A) = width A )
by MATRIXR1:27;
A2:
len ((a * A) + (b * A)) = len (a * A)
by MATRIX_3:def 3;
A3:
width ((a * A) + (b * A)) = width (a * A)
by MATRIX_3:def 3;
A4:
( len (a * A) = len A & width (a * A) = width A )
by MATRIXR1:27;
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;
:: thesis: ( [i,j] in Indices ((a + b) * A) implies ((a + b) * A) * i,j = ((a * A) + (b * A)) * i,j )
assume A5:
[i,j] in Indices ((a + b) * A)
;
:: thesis: ((a + b) * A) * i,j = ((a * A) + (b * A)) * i,j
A6:
Indices ((a + b) * A) = Indices A
by A1, MATRIX_4:55;
A7:
Indices (a * A) = Indices A
by A4, MATRIX_4:55;
reconsider i0 =
i,
j0 =
j as
Element of
NAT by ORDINAL1:def 13;
((a * A) + (b * A)) * i,
j =
((a * A) * i0,j0) + ((b * A) * i0,j0)
by A5, A6, A7, MATRIXR1:25
.=
(a * (A * i0,j0)) + ((b * A) * i0,j0)
by A5, A6, MATRIXR1:29
.=
(a * (A * i0,j0)) + (b * (A * i0,j0))
by A5, A6, MATRIXR1:29
.=
(a + b) * (A * i,j)
;
hence
((a + b) * A) * i,
j = ((a * A) + (b * A)) * i,
j
by A5, A6, MATRIXR1:29;
:: thesis: verum
end;
hence
(a + b) * A = (a * A) + (b * A)
by A1, A2, A3, A4, MATRIX_1:21; :: thesis: verum