let K be Field; :: thesis: 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; :: thesis: 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; :: thesis: ( 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 ; :: thesis: (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;

hence (a * A) * B = a * (A * B) by A2, A4, A6, A7, MATRIX_0:21; :: thesis: verum

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; :: thesis: 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; :: thesis: ( 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 ; :: thesis: (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 :: thesis: for i, j being Nat st [i,j] in Indices (a * (A * B)) holds

(a * (A * B)) * (i,j) = ((a * A) * B) * (i,j)

( width (a * (A * B)) = width (A * B) & width B = width ((a * A) * B) )
by A1, A5, MATRIX_3:def 4, MATRIX_3:def 5;(a * (A * B)) * (i,j) = ((a * A) * B) * (i,j)

let i, j be Nat; :: thesis: ( [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)) ; :: thesis: (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 ; :: thesis: verum

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

hence (a * A) * B = a * (A * B) by A2, A4, A6, A7, MATRIX_0:21; :: thesis: verum