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 A * (r * B) = (A * r) * 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 A * (r * B) = (A * r) * 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 A * (r * B) = (A * r) * 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 A * (r * B) = (A * r) * 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 A * (r * B) = (A * r) * B
let A be Matrix of k,m,R; :: thesis: for B being Matrix of m,n,R holds A * (r * B) = (A * r) * B
let B be Matrix of m,n,R; :: thesis: A * (r * B) = (A * r) * B
set LHS = A * (r * B);
set RHS = (A * r) * B;

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

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

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

end;

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

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

proof

thus width A = m by A5, MATRIX_0:23
.= len (r * B) by MATRIX_0:25 ; :: thesis: width (A * r) = len B
thus width (A * r) = m by A5, MATRIX_0:23
.= len B by MATRIX_0:25 ; :: thesis: verum

end;

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

proof

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

end;

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

proof

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

proof

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

end;

A10: mlt ((Line (A,i)),(Col ((r * B),j))) = mlt ((Line ((A * r),i)),(Col (B,j)))

proof

set a1 = Line (A,i);
set b1 = Col ((r * B),j);
set a2 = Line ((A * r),i);
set b2 = Col (B,j);
mlt ((Line (A,i)),(Col ((r * B),j))) = the multF of R .: ((Line (A,i)),(Col ((r * B),j))) by FVSUM_1:def 7;
then len (mlt ((Line (A,i)),(Col ((r * B),j)))) = min ((len (Line (A,i))),(len (Col ((r * B),j)))) by FINSEQ_2:71
.= min ((width A),(len (Col ((r * B),j)))) by MATRIX_0:def 7
.= min ((len (r * B)),(len (r * B))) by A6, MATRIX_0:def 8
.= len B by MATRIX_3:def 5 ;
then A11: Seg (len B) = dom (mlt ((Line (A,i)),(Col ((r * B),j)))) by FINSEQ_1:def 3;
mlt ((Line ((A * r),i)),(Col (B,j))) = the multF of R .: ((Line ((A * r),i)),(Col (B,j))) by FVSUM_1:def 7;
then len (mlt ((Line ((A * r),i)),(Col (B,j)))) = min ((len (Line ((A * r),i))),(len (Col (B,j)))) by FINSEQ_2:71
.= min ((width (A * r)),(len (Col (B,j)))) by MATRIX_0:def 7
.= min ((width (A * r)),(len B)) by MATRIX_0:def 8
.= len B by A6 ;
then A12: dom (mlt ((Line (A,i)),(Col ((r * B),j)))) = dom (mlt ((Line ((A * r),i)),(Col (B,j)))) by A11, FINSEQ_1:def 3;
for i9 being Nat st i9 in dom (mlt ((Line (A,i)),(Col ((r * B),j)))) holds
(mlt ((Line (A,i)),(Col ((r * B),j)))) . i9 = (mlt ((Line ((A * r),i)),(Col (B,j)))) . i9

proof

let i9 be Nat; :: thesis: ( i9 in dom (mlt ((Line (A,i)),(Col ((r * B),j)))) implies (mlt ((Line (A,i)),(Col ((r * B),j)))) . i9 = (mlt ((Line ((A * r),i)),(Col (B,j)))) . i9 )
assume A13: i9 in dom (mlt ((Line (A,i)),(Col ((r * B),j)))) ; :: thesis: (mlt ((Line (A,i)),(Col ((r * B),j)))) . i9 = (mlt ((Line ((A * r),i)),(Col (B,j)))) . i9
then A14: ( i9 in Seg (width (A * r)) & i9 in Seg (width A) ) by A6, A11, MATRIX_3:def 6;
then A15: ( (Line (A,i)) . i9 = A * (i,i9) & (Line ((A * r),i)) . i9 = (A * r) * (i,i9) ) by MATRIX_0:def 7;
A16: ( [i,i9] in Indices A & [i,i9] in Indices (A * r) )

proof

[i,j] in [:(dom (A * (r * B))),(Seg (width (A * (r * B)))):] by A8, MATRIX_0:def 4;
then ( i in dom (A * (r * B)) & j in Seg (width (A * (r * B))) ) by ZFMISC_1:87;
then i in Seg (len (A * (r * B))) by FINSEQ_1:def 3;
then A17: i in Seg (len A) by A6, MATRIX_3:def 4;
then i in dom A by FINSEQ_1:def 3;
then [i,i9] in [:(dom A),(Seg (width A)):] by A14, ZFMISC_1:87;
hence [i,i9] in Indices A by MATRIX_0:def 4; :: thesis: [i,i9] in Indices (A * r)
dom (A * r) = Seg (len (A * r)) by FINSEQ_1:def 3
.= Seg (len A) by MATRIX_3:def 6 ;
then [i,i9] in [:(dom (A * r)),(Seg (width (A * r))):] by A14, A17, ZFMISC_1:87;
hence [i,i9] in Indices (A * r) by MATRIX_0:def 4; :: thesis: verum

end;

consider aa1, aa2 being Element of R such that
A18: ( aa1 = A * (i,i9) & aa2 = (A * r) * (i,i9) ) ;
A19: ( i9 in dom B & i9 in dom (r * B) )

proof

thus i9 in dom B by A11, A13, FINSEQ_1:def 3; :: thesis: i9 in dom (r * B)
i9 in Seg (len (r * B)) by A11, A13, MATRIX_3:def 5;
hence i9 in dom (r * B) by FINSEQ_1:def 3; :: thesis: verum

end;

then A20: ( (Col ((r * B),j)) . i9 = (r * B) * (i9,j) & (Col (B,j)) . i9 = B * (i9,j) ) by MATRIX_0:def 8;
A21: ( [i9,j] in Indices (r * B) & [i9,j] in Indices B )

proof

[i,j] in [:(dom (A * (r * B))),(Seg (width (A * (r * B)))):] by A8, MATRIX_0:def 4;
then ( i in dom (A * (r * B)) & j in Seg (width (A * (r * B))) ) by ZFMISC_1:87;
then A22: j in Seg (width (r * B)) by A6, MATRIX_3:def 4;
then [i9,j] in [:(dom (r * B)),(Seg (width (r * B))):] by A19, ZFMISC_1:87;
hence [i9,j] in Indices (r * B) by MATRIX_0:def 4; :: thesis: [i9,j] in Indices B
j in Seg (width B) by A22, MATRIX_3:def 5;
then [i9,j] in [:(dom B),(Seg (width B)):] by A19, ZFMISC_1:87;
hence [i9,j] in Indices B by MATRIX_0:def 4; :: thesis: verum

end;

consider bb1, bb2 being Element of R such that
A23: ( bb1 = (r * B) * (i9,j) & bb2 = B * (i9,j) ) ;
aa1 * r = aa2 by A16, A18, MATRIX_3:def 6;
then A24: ( aa1 * r = aa2 & bb1 = r * bb2 ) by A21, A23, MATRIX_3:def 5;
A25: ( (Line ((A * r),i)) . i9 = aa2 & (Col (B,j)) . i9 = bb2 ) by A15, A18, A20, A23;
thus (mlt ((Line (A,i)),(Col ((r * B),j)))) . i9 = aa1 * bb1 by A13, A15, A18, A20, A23, FVSUM_1:60
.= (aa1 * r) * bb2 by A24, GROUP_1:def 3
.= (mlt ((Line ((A * r),i)),(Col (B,j)))) . i9 by A12, A13, A24, A25, FVSUM_1:60 ; :: thesis: verum

end;

hence mlt ((Line (A,i)),(Col ((r * B),j))) = mlt ((Line ((A * r),i)),(Col (B,j))) by A12, FINSEQ_1:13; :: thesis: verum

end;

A26: (Line (A,i)) "*" (Col ((r * B),j)) = Sum (mlt ((Line (A,i)),(Col ((r * B),j)))) by FVSUM_1:def 9
.= (Line ((A * r),i)) "*" (Col (B,j)) by A10, FVSUM_1:def 9 ;
thus (A * (r * B)) * (i,j) = (Line (A,i)) "*" (Col ((r * B),j)) by A6, A8, MATRIX_3:def 4
.= ((A * r) * B) * (i,j) by A6, A9, A26, MATRIX_3:def 4 ; :: thesis: verum

end;

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

end;

end;