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 aA = a * A;
set AB = A * B;
set aAB = a * (A * B);
assume A1:
width A = len B
; (a * A) * B = a * (A * B)
then A2:
width (A * B) = width B
by MATRIX_3:def 4;
A3:
len (a * (A * B)) = len (A * B)
by MATRIX_3:def 5;
then A4:
len (a * (A * B)) = len A
by A1, MATRIX_3:def 4;
A5:
width (a * A) = width A
by MATRIX_3:def 5;
then A6:
( len (a * A) = len A & len (a * A) = len ((a * A) * B) )
by A1, MATRIX_3:def 4, MATRIX_3:def 5;
A7:
now for i, j being Nat st [i,j] in Indices (a * (A * B)) holds
(a * (A * B)) * (i,j) = ((a * A) * B) * (i,j)let i,
j be
Nat;
( [i,j] in Indices (a * (A * B)) implies (a * (A * B)) * (i,j) = ((a * A) * B) * (i,j) )assume
[i,j] in Indices (a * (A * B))
;
(a * (A * B)) * (i,j) = ((a * A) * B) * (i,j)then A8:
[i,j] in Indices (A * B)
by MATRIXR1:18;
then
i in dom (A * B)
by ZFMISC_1:87;
then
i in Seg (len A)
by A3, A4, FINSEQ_1:def 3;
then A9:
( 1
<= i &
i <= len A )
by FINSEQ_1:1;
dom (A * B) =
Seg (len (A * B))
by FINSEQ_1:def 3
.=
dom ((a * A) * B)
by A3, A4, A6, FINSEQ_1:def 3
;
then A10:
[i,j] in Indices ((a * A) * B)
by A1, A5, A2, A8, MATRIX_3:def 4;
thus (a * (A * B)) * (
i,
j) =
a * ((A * B) * (i,j))
by A8, MATRIX_3:def 5
.=
a * ((Line (A,i)) "*" (Col (B,j)))
by A1, A8, MATRIX_3:def 4
.=
Sum (a * (mlt ((Line (A,i)),(Col (B,j)))))
by FVSUM_1:73
.=
Sum (mlt ((a * (Line (A,i))),(Col (B,j))))
by A1, FVSUM_1:68
.=
(Line ((a * A),i)) "*" (Col (B,j))
by A9, MATRIXR1:20
.=
((a * A) * B) * (
i,
j)
by A1, A5, A10, MATRIX_3:def 4
;
verum end;
( width (a * (A * B)) = width (A * B) & width B = width ((a * A) * B) )
by A1, A5, MATRIX_3:def 4, MATRIX_3:def 5;
hence
(a * A) * B = a * (A * B)
by A2, A4, A6, A7, MATRIX_0:21; verum