let L be Field; :: thesis: for m, n, k being Element of NAT st m > 0 & n > 0 holds
for M1 being Matrix of m,n,L
for M2 being Matrix of n,k,L holds ((emb (m,L)) * M1) * M2 = (emb (m,L)) * (M1 * M2)
let m, n, k be Element of NAT ; :: thesis: ( m > 0 & n > 0 implies for M1 being Matrix of m,n,L
for M2 being Matrix of n,k,L holds ((emb (m,L)) * M1) * M2 = (emb (m,L)) * (M1 * M2) )
assume that
A1: m > 0 and
A2: n > 0 ; :: thesis: for M1 being Matrix of m,n,L
for M2 being Matrix of n,k,L holds ((emb (m,L)) * M1) * M2 = (emb (m,L)) * (M1 * M2)
let M1 be Matrix of m,n,L; :: thesis: for M2 being Matrix of n,k,L holds ((emb (m,L)) * M1) * M2 = (emb (m,L)) * (M1 * M2)
let M2 be Matrix of n,k,L; :: thesis: ((emb (m,L)) * M1) * M2 = (emb (m,L)) * (M1 * M2)
A3: width M1 = n by A1, MATRIX_0:23
.= len M2 by A2, MATRIX_0:23 ;
A4: width ((emb (m,L)) * M1) = width M1 by MATRIX_3:def 5
.= n by A1, MATRIX_0:23
.= len M2 by A2, MATRIX_0:23 ;
A5: for i, j being Nat st [i,j] in Indices (((emb (m,L)) * M1) * M2) holds
(((emb (m,L)) * M1) * M2) * (i,j) = ((emb (m,L)) * (M1 * M2)) * (i,j)

proof

let i, j be Nat; :: thesis: ( [i,j] in Indices (((emb (m,L)) * M1) * M2) implies (((emb (m,L)) * M1) * M2) * (i,j) = ((emb (m,L)) * (M1 * M2)) * (i,j) )
A6: len M1 = len (M1 * M2) by A3, MATRIX_3:def 4;
len (((emb (m,L)) * M1) * M2) = len ((emb (m,L)) * M1) by A4, MATRIX_3:def 4
.= len M1 by MATRIX_3:def 5 ;
then A7: dom (((emb (m,L)) * M1) * M2) = Seg (len M1) by FINSEQ_1:def 3
.= dom (M1 * M2) by A6, FINSEQ_1:def 3 ;
Seg (len ((emb (m,L)) * (Line (M1,i)))) = dom ((emb (m,L)) * (Line (M1,i))) by FINSEQ_1:def 3
.= dom (Line (M1,i)) by POLYNOM1:def 1
.= Seg (len (Line (M1,i))) by FINSEQ_1:def 3 ;
then A8: len ((emb (m,L)) * (Line (M1,i))) = len (Line (M1,i)) by FINSEQ_1:6
.= width M1 by MATRIX_0:def 7 ;
A9: len (Line (M1,i)) = len M2 by A3, MATRIX_0:def 7
.= len (Col (M2,j)) by MATRIX_0:def 8 ;
assume A10: [i,j] in Indices (((emb (m,L)) * M1) * M2) ; :: thesis: (((emb (m,L)) * M1) * M2) * (i,j) = ((emb (m,L)) * (M1 * M2)) * (i,j)
then A11: (((emb (m,L)) * M1) * M2) * (i,j) = (Line (((emb (m,L)) * M1),i)) "*" (Col (M2,j)) by A4, MATRIX_3:def 4
.= Sum (mlt ((Line (((emb (m,L)) * M1),i)),(Col (M2,j)))) by FVSUM_1:def 9 ;
len (Line (((emb (m,L)) * M1),i)) = width ((emb (m,L)) * M1) by MATRIX_0:def 7
.= width M1 by MATRIX_3:def 5 ;
then dom (Line (((emb (m,L)) * M1),i)) = Seg (width M1) by FINSEQ_1:def 3;
then A12: dom (Line (((emb (m,L)) * M1),i)) = dom ((emb (m,L)) * (Line (M1,i))) by A8, FINSEQ_1:def 3;
for k being Nat st k in dom (Line (((emb (m,L)) * M1),i)) holds
(Line (((emb (m,L)) * M1),i)) . k = ((emb (m,L)) * (Line (M1,i))) . k

proof

len (M1 * M2) = len M1 by A3, MATRIX_3:def 4
.= m by A1, MATRIX_0:23 ;
then A13: dom (M1 * M2) = Seg m by FINSEQ_1:def 3;
A14: ( Indices M1 = [:(Seg m),(Seg n):] & i in dom (M1 * M2) ) by A1, A10, A7, MATRIX_0:23, ZFMISC_1:87;
let k be Nat; :: thesis: ( k in dom (Line (((emb (m,L)) * M1),i)) implies (Line (((emb (m,L)) * M1),i)) . k = ((emb (m,L)) * (Line (M1,i))) . k )
assume A15: k in dom (Line (((emb (m,L)) * M1),i)) ; :: thesis: (Line (((emb (m,L)) * M1),i)) . k = ((emb (m,L)) * (Line (M1,i))) . k
A16: len (Line (((emb (m,L)) * M1),i)) = width ((emb (m,L)) * M1) by MATRIX_0:def 7
.= width M1 by MATRIX_3:def 5 ;
then A17: k in Seg (width M1) by A15, FINSEQ_1:def 3;
len (Line (M1,i)) = width M1 by MATRIX_0:def 7;
then k in dom (Line (M1,i)) by A17, FINSEQ_1:def 3;
then (Line (M1,i)) . k = (Line (M1,i)) /. k by PARTFUN1:def 6;
then reconsider a = (Line (M1,i)) . k as Element of L ;
A18: a = M1 * (i,k) by A17, MATRIX_0:def 7;
k in Seg n by A1, A17, MATRIX_0:23;
then [i,k] in Indices M1 by A14, A13, ZFMISC_1:87;
then A19: (emb (m,L)) * a = ((emb (m,L)) * M1) * (i,k) by A18, MATRIX_3:def 5;
dom (Line (((emb (m,L)) * M1),i)) = Seg (width M1) by A16, FINSEQ_1:def 3;
then A20: k in Seg (width ((emb (m,L)) * M1)) by A15, MATRIX_3:def 5;
((emb (m,L)) * (Line (M1,i))) . k = (emb (m,L)) * a by A12, A15, FVSUM_1:50;
hence (Line (((emb (m,L)) * M1),i)) . k = ((emb (m,L)) * (Line (M1,i))) . k by A20, A19, MATRIX_0:def 7; :: thesis: verum

end;

then A21: Line (((emb (m,L)) * M1),i) = (emb (m,L)) * (Line (M1,i)) by A12, FINSEQ_1:13;
Seg (len ((emb (m,L)) * (Line (M1,i)))) = dom ((emb (m,L)) * (Line (M1,i))) by FINSEQ_1:def 3
.= dom (Line (M1,i)) by POLYNOM1:def 1
.= Seg (len (Line (M1,i))) by FINSEQ_1:def 3 ;
then A22: len ((emb (m,L)) * (Line (M1,i))) = len (Line (M1,i)) by FINSEQ_1:6
.= len M2 by A3, MATRIX_0:def 7
.= len (Col (M2,j)) by MATRIX_0:def 8 ;
A23: dom ((emb (m,L)) * (Line (M1,i))) = Seg (len ((emb (m,L)) * (Line (M1,i)))) by FINSEQ_1:def 3
.= Seg (len (mlt (((emb (m,L)) * (Line (M1,i))),(Col (M2,j))))) by A22, MATRIX_3:6
.= dom (mlt (((emb (m,L)) * (Line (M1,i))),(Col (M2,j)))) by FINSEQ_1:def 3 ;
A24: dom ((emb (m,L)) * (Line (M1,i))) = dom (Line (M1,i)) by POLYNOM1:def 1
.= Seg (len (Line (M1,i))) by FINSEQ_1:def 3
.= Seg (len (mlt ((Line (M1,i)),(Col (M2,j))))) by A9, MATRIX_3:6
.= dom (mlt ((Line (M1,i)),(Col (M2,j)))) by FINSEQ_1:def 3 ;
then A25: dom (mlt (((emb (m,L)) * (Line (M1,i))),(Col (M2,j)))) = dom ((emb (m,L)) * (mlt ((Line (M1,i)),(Col (M2,j))))) by A23, POLYNOM1:def 1;
for k being Nat st k in dom (mlt (((emb (m,L)) * (Line (M1,i))),(Col (M2,j)))) holds
(mlt (((emb (m,L)) * (Line (M1,i))),(Col (M2,j)))) . k = ((emb (m,L)) * (mlt ((Line (M1,i)),(Col (M2,j))))) . k

proof

A26: len (Line (M1,i)) = len M2 by A3, MATRIX_0:def 7
.= len (Col (M2,j)) by MATRIX_0:def 8 ;
A27: len (Line (M1,i)) = width M1 by MATRIX_0:def 7;
let k be Nat; :: thesis: ( k in dom (mlt (((emb (m,L)) * (Line (M1,i))),(Col (M2,j)))) implies (mlt (((emb (m,L)) * (Line (M1,i))),(Col (M2,j)))) . k = ((emb (m,L)) * (mlt ((Line (M1,i)),(Col (M2,j))))) . k )
assume A28: k in dom (mlt (((emb (m,L)) * (Line (M1,i))),(Col (M2,j)))) ; :: thesis: (mlt (((emb (m,L)) * (Line (M1,i))),(Col (M2,j)))) . k = ((emb (m,L)) * (mlt ((Line (M1,i)),(Col (M2,j))))) . k
dom (Line (M1,i)) = Seg (len (Line (M1,i))) by FINSEQ_1:def 3
.= Seg (len (mlt ((Line (M1,i)),(Col (M2,j))))) by A26, MATRIX_3:6
.= dom (mlt ((Line (M1,i)),(Col (M2,j)))) by FINSEQ_1:def 3 ;
then A29: k in Seg (width M1) by A23, A24, A28, A27, FINSEQ_1:def 3;
then k in dom M2 by A3, FINSEQ_1:def 3;
then A30: (Col (M2,j)) . k = M2 * (k,j) by MATRIX_0:def 8;
(Line (M1,i)) . k = M1 * (i,k) by A29, MATRIX_0:def 7;
then reconsider c = (Col (M2,j)) . k, d = (Line (M1,i)) . k as Element of L by A30;
(mlt ((Line (M1,i)),(Col (M2,j)))) . k = c * d by A23, A24, A28, FVSUM_1:60;
then reconsider a = (mlt ((Line (M1,i)),(Col (M2,j)))) . k as Element of L ;
A31: ((emb (m,L)) * (mlt ((Line (M1,i)),(Col (M2,j))))) . k = (emb (m,L)) * a by A25, A28, FVSUM_1:50;
((emb (m,L)) * (Line (M1,i))) . k = (emb (m,L)) * d by A23, A28, FVSUM_1:50;
then reconsider b = ((emb (m,L)) * (Line (M1,i))) . k as Element of L ;
b * c = ((emb (m,L)) * d) * c by A23, A28, FVSUM_1:50
.= (emb (m,L)) * (d * c) by GROUP_1:def 3
.= (emb (m,L)) * a by A23, A24, A28, FVSUM_1:60 ;
hence (mlt (((emb (m,L)) * (Line (M1,i))),(Col (M2,j)))) . k = ((emb (m,L)) * (mlt ((Line (M1,i)),(Col (M2,j))))) . k by A28, A31, FVSUM_1:60; :: thesis: verum

end;

then A32: (emb (m,L)) * (mlt ((Line (M1,i)),(Col (M2,j)))) = mlt ((Line (((emb (m,L)) * M1),i)),(Col (M2,j))) by A21, A25, FINSEQ_1:13;
Seg (width (((emb (m,L)) * M1) * M2)) = Seg (width M2) by A4, MATRIX_3:def 4
.= Seg (width (M1 * M2)) by A3, MATRIX_3:def 4 ;
then A33: [i,j] in Indices (M1 * M2) by A10, A7;
then ((emb (m,L)) * (M1 * M2)) * (i,j) = (emb (m,L)) * ((M1 * M2) * (i,j)) by MATRIX_3:def 5
.= (emb (m,L)) * ((Line (M1,i)) "*" (Col (M2,j))) by A3, A33, MATRIX_3:def 4
.= (emb (m,L)) * (Sum (mlt ((Line (M1,i)),(Col (M2,j))))) by FVSUM_1:def 9 ;
hence (((emb (m,L)) * M1) * M2) * (i,j) = ((emb (m,L)) * (M1 * M2)) * (i,j) by A11, A32, FVSUM_1:73; :: thesis: verum

end;

A34: len ((emb (m,L)) * (M1 * M2)) = len (M1 * M2) by MATRIX_3:def 5
.= len M1 by A3, MATRIX_3:def 4 ;
width ((emb (m,L)) * (M1 * M2)) = width (M1 * M2) by MATRIX_3:def 5
.= width M2 by A3, MATRIX_3:def 4 ;
then A35: width (((emb (m,L)) * M1) * M2) = width ((emb (m,L)) * (M1 * M2)) by A4, MATRIX_3:def 4;
len (((emb (m,L)) * M1) * M2) = len ((emb (m,L)) * M1) by A4, MATRIX_3:def 4
.= len M1 by MATRIX_3:def 5 ;
hence ((emb (m,L)) * M1) * M2 = (emb (m,L)) * (M1 * M2) by A34, A35, A5, MATRIX_0:21; :: thesis: verum