let R be Ring; :: thesis: for n, k, m being Nat st ( k = 0 implies m = 0 ) holds
for r being Element of R
for A being Matrix of k,m,R
for B being Matrix of m,n,R holds (r * A) * B = r * (A * B)
let n be Nat; :: thesis: for k, m being Nat st ( k = 0 implies m = 0 ) holds
for r being Element of R
for A being Matrix of k,m,R
for B being Matrix of m,n,R holds (r * A) * B = r * (A * B)
let k, m be Nat; :: thesis: ( ( k = 0 implies m = 0 ) implies for r being Element of R
for A being Matrix of k,m,R
for B being Matrix of m,n,R holds (r * A) * B = r * (A * B) )
assume A1: ( k = 0 implies m = 0 ) ; :: thesis: for r being Element of R
for A being Matrix of k,m,R
for B being Matrix of m,n,R holds (r * A) * B = r * (A * B)
let r be Element of R; :: thesis: for A being Matrix of k,m,R
for B being Matrix of m,n,R holds (r * A) * B = r * (A * B)
let A be Matrix of k,m,R; :: thesis: for B being Matrix of m,n,R holds (r * A) * B = r * (A * B)
let B be Matrix of m,n,R; :: thesis: (r * A) * B = r * (A * B)
set LHS = (r * A) * B;
set RHS = r * (A * B);

per cases ( k = 0 or k > 0 ) ;

suppose A2: k = 0 ; :: thesis: (r * A) * B = r * (A * B)

A3: len A = 0 by A2, MATRIX_0:25;
then A4: width A = 0 by MATRIX_0:def 3;
A5: len B = 0 by A1, A2, MATRIX_0:25;
A6: len (r * A) = 0 by A2, MATRIX_0:25;
then width (r * A) = 0 by MATRIX_0:def 3;
then A7: len ((r * A) * B) = 0 by A5, A6, MATRIX_3:def 4;
len (r * (A * B)) = len (A * B) by MATRIX_3:def 5
.= 0 by A3, A4, A5, MATRIX_3:def 4 ;
hence r * (A * B) = {}
.= (r * A) * B by A7 ;
:: thesis: verum

end;

suppose A8: k > 0 ; :: thesis: (r * A) * B = r * (A * B)

A9: ( width A = len B & width (r * A) = len B )

proof

thus width A = m by A8, MATRIX_0:23
.= len B by MATRIX_0:25 ; :: thesis: width (r * A) = len B
hence len B = width (r * A) by MATRIX_3:def 5; :: thesis: verum

end;

A10: ( len ((r * A) * B) = len (r * (A * B)) & width ((r * A) * B) = width (r * (A * B)) )

proof

thus len ((r * A) * B) = len (r * A) by A9, MATRIX_3:def 4
.= len A by MATRIX_3:def 5
.= len (A * B) by A9, MATRIX_3:def 4
.= len (r * (A * B)) by MATRIX_3:def 5 ; :: thesis: width ((r * A) * B) = width (r * (A * B))
thus width ((r * A) * B) = width B by A9, MATRIX_3:def 4
.= width (A * B) by A9, MATRIX_3:def 4
.= width (r * (A * B)) by MATRIX_3:def 5 ; :: thesis: verum

end;

for i, j being Nat st [i,j] in Indices ((r * A) * B) holds
((r * A) * B) * (i,j) = (r * (A * B)) * (i,j)

proof

let i, j be Nat; :: thesis: ( [i,j] in Indices ((r * A) * B) implies ((r * A) * B) * (i,j) = (r * (A * B)) * (i,j) )
assume A11: [i,j] in Indices ((r * A) * B) ; :: thesis: ((r * A) * B) * (i,j) = (r * (A * B)) * (i,j)
A12: [i,j] in Indices (r * (A * B))

proof

Indices ((r * A) * B) = [:(dom ((r * A) * B)),(Seg (width ((r * A) * B))):] by MATRIX_0:def 4
.= [:(Seg (len ((r * A) * B))),(Seg (width ((r * A) * B))):] by FINSEQ_1:def 3
.= [:(dom (r * (A * B))),(Seg (width (r * (A * B)))):] by A10, FINSEQ_1:def 3
.= Indices (r * (A * B)) by MATRIX_0:def 4 ;
hence [i,j] in Indices (r * (A * B)) by A11; :: thesis: verum

end;

A13: [i,j] in Indices (A * B)

proof

Indices (r * (A * B)) = [:(dom (r * (A * B))),(Seg (width (r * (A * B)))):] by MATRIX_0:def 4
.= [:(Seg (len (r * (A * B)))),(Seg (width (r * (A * B)))):] by FINSEQ_1:def 3
.= [:(Seg (len (A * B))),(Seg (width (r * (A * B)))):] by MATRIX_3:def 5
.= [:(Seg (len (A * B))),(Seg (width (A * B))):] by MATRIX_3:def 5
.= [:(dom (A * B)),(Seg (width (A * B))):] by FINSEQ_1:def 3
.= Indices (A * B) by MATRIX_0:def 4 ;
hence [i,j] in Indices (A * B) by A12; :: thesis: verum

end;

A14: Line ((r * A),i) = r * (Line (A,i))

proof

A15: width (r * A) = width A by MATRIX_3:def 5;
for j9 being Nat st j9 in Seg (width A) holds
(Line ((r * A),i)) . j9 = (r * (Line (A,i))) . j9

proof

let j9 be Nat; :: thesis: ( j9 in Seg (width A) implies (Line ((r * A),i)) . j9 = (r * (Line (A,i))) . j9 )
assume A16: j9 in Seg (width A) ; :: thesis: (Line ((r * A),i)) . j9 = (r * (Line (A,i))) . j9
[i,j] in [:(dom (A * B)),(Seg (width (A * B))):] by A13, MATRIX_0:def 4;
then i in dom (A * B) by ZFMISC_1:87;
then i in Seg (len (A * B)) by FINSEQ_1:def 3;
then i in Seg (len A) by A9, MATRIX_3:def 4;
then i in dom A by FINSEQ_1:def 3;
then [i,j9] in [:(dom A),(Seg (width A)):] by A16, ZFMISC_1:87;
then A17: [i,j9] in Indices A by MATRIX_0:def 4;
A18: (Line (A,i)) . j9 = A * (i,j9) by A16, MATRIX_0:def 7;
thus (Line ((r * A),i)) . j9 = (r * A) * (i,j9) by A15, A16, MATRIX_0:def 7
.= r * (A * (i,j9)) by A17, MATRIX_3:def 5
.= (r * (Line (A,i))) . j9 by A16, A18, FVSUM_1:51 ; :: thesis: verum

end;

hence Line ((r * A),i) = r * (Line (A,i)) by A15, FINSEQ_2:119; :: thesis: verum

end;

thus ((r * A) * B) * (i,j) = (Line ((r * A),i)) "*" (Col (B,j)) by A9, A11, MATRIX_3:def 4
.= Sum (mlt ((Line ((r * A),i)),(Col (B,j)))) by FVSUM_1:def 9
.= Sum (r * (mlt ((Line (A,i)),(Col (B,j))))) by A9, A14, FVSUM_1:68
.= r * (Sum (mlt ((Line (A,i)),(Col (B,j))))) by FVSUM_1:73
.= r * ((Line (A,i)) "*" (Col (B,j))) by FVSUM_1:def 9
.= r * ((A * B) * (i,j)) by A9, A13, MATRIX_3:def 4
.= (r * (A * B)) * (i,j) by A13, MATRIX_3:def 5 ; :: thesis: verum

end;

hence (r * A) * B = r * (A * B) by A10, MATRIX_0:21; :: thesis: verum

end;

end;