let K be Field; for a being Element of K
for A, B being Matrix of K st width A = len B holds
A * (a * B) = a * (A * B)
let a be Element of K; for A, B being Matrix of K st width A = len B holds
A * (a * B) = a * (A * B)
let A, B be Matrix of K; ( width A = len B implies A * (a * B) = a * (A * B) )
set C = a * B;
set D = a * (A * B);
A1:
len (a * (A * B)) = len (A * B)
by MATRIX_3:def 5;
assume A2:
width A = len B
; A * (a * B) = a * (A * B)
then
width (A * B) = width B
by MATRIX_3:def 4;
then A3: width (a * (A * B)) =
width B
by MATRIX_3:def 5
.=
width (a * B)
by MATRIX_3:def 5
;
A4:
width B = width (a * B)
by MATRIX_3:def 5;
A5:
for i, j being Nat st [i,j] in Indices (a * (A * B)) holds
(a * (A * B)) * (i,j) = (Line (A,i)) "*" (Col ((a * B),j))
proof
let i,
j be
Nat;
( [i,j] in Indices (a * (A * B)) implies (a * (A * B)) * (i,j) = (Line (A,i)) "*" (Col ((a * B),j)) )
reconsider xo =
Col (
B,
j) as
Element of
(width A) -tuples_on the
carrier of
K by A2;
assume A6:
[i,j] in Indices (a * (A * B))
;
(a * (A * B)) * (i,j) = (Line (A,i)) "*" (Col ((a * B),j))
then
j in Seg (width B)
by A4, A3, ZFMISC_1:87;
then A7:
( 1
<= j &
j <= width B )
by FINSEQ_1:1;
dom (A * B) = dom (a * (A * B))
by A1, FINSEQ_3:29;
then A8:
[i,j] in Indices (A * B)
by A6, MATRIX_3:def 5;
then
(a * (A * B)) * (
i,
j)
= a * ((A * B) * (i,j))
by MATRIX_3:def 5;
then (a * (A * B)) * (
i,
j) =
a * ((Line (A,i)) "*" (Col (B,j)))
by A2, A8, MATRIX_3:def 4
.=
a * (Sum (mlt ((Line (A,i)),(Col (B,j)))))
by FVSUM_1:def 9
.=
Sum (a * (mlt ((Line (A,i)),(Col (B,j)))))
by FVSUM_1:73
.=
Sum (mlt ((Line (A,i)),(a * xo)))
by FVSUM_1:69
.=
Sum (mlt ((Line (A,i)),(Col ((a * B),j))))
by A7, Th19
;
hence
(a * (A * B)) * (
i,
j)
= (Line (A,i)) "*" (Col ((a * B),j))
by FVSUM_1:def 9;
verum
end;
( len (a * B) = len B & len (A * B) = len A )
by A2, MATRIX_3:def 4, MATRIX_3:def 5;
hence
A * (a * B) = a * (A * B)
by A2, A1, A3, A5, MATRIX_3:def 4; verum