let m, n be Nat; for V1 being free finite-rank Z_Module
for M being Matrix of n,m,INT.Ring st n > 0 & m > 0 holds
for p, d being FinSequence of INT.Ring st len p = n & len d = m & ( for j being Nat st j in dom d holds
d /. j = Sum (mlt (p,(Col (M,j)))) ) holds
for b, c being FinSequence of V1 st len b = m & len c = n & ( for i being Nat st i in dom c holds
c /. i = Sum (lmlt ((Line (M,i)),b)) ) holds
Sum (lmlt (p,c)) = Sum (lmlt (d,b))
let V1 be free finite-rank Z_Module; for M being Matrix of n,m,INT.Ring st n > 0 & m > 0 holds
for p, d being FinSequence of INT.Ring st len p = n & len d = m & ( for j being Nat st j in dom d holds
d /. j = Sum (mlt (p,(Col (M,j)))) ) holds
for b, c being FinSequence of V1 st len b = m & len c = n & ( for i being Nat st i in dom c holds
c /. i = Sum (lmlt ((Line (M,i)),b)) ) holds
Sum (lmlt (p,c)) = Sum (lmlt (d,b))
let M be Matrix of n,m,INT.Ring; ( n > 0 & m > 0 implies for p, d being FinSequence of INT.Ring st len p = n & len d = m & ( for j being Nat st j in dom d holds
d /. j = Sum (mlt (p,(Col (M,j)))) ) holds
for b, c being FinSequence of V1 st len b = m & len c = n & ( for i being Nat st i in dom c holds
c /. i = Sum (lmlt ((Line (M,i)),b)) ) holds
Sum (lmlt (p,c)) = Sum (lmlt (d,b)) )
assume that
A1:
n > 0
and
A2:
m > 0
; for p, d being FinSequence of INT.Ring st len p = n & len d = m & ( for j being Nat st j in dom d holds
d /. j = Sum (mlt (p,(Col (M,j)))) ) holds
for b, c being FinSequence of V1 st len b = m & len c = n & ( for i being Nat st i in dom c holds
c /. i = Sum (lmlt ((Line (M,i)),b)) ) holds
Sum (lmlt (p,c)) = Sum (lmlt (d,b))
A3:
len M = n
by A1, MATRIX_0:23;
reconsider n1 = n, m1 = m as Element of NAT by ORDINAL1:def 12;
let p, d be FinSequence of INT.Ring; ( len p = n & len d = m & ( for j being Nat st j in dom d holds
d /. j = Sum (mlt (p,(Col (M,j)))) ) implies for b, c being FinSequence of V1 st len b = m & len c = n & ( for i being Nat st i in dom c holds
c /. i = Sum (lmlt ((Line (M,i)),b)) ) holds
Sum (lmlt (p,c)) = Sum (lmlt (d,b)) )
assume that
A4:
len p = n
and
A5:
len d = m
and
A6:
for j being Nat st j in dom d holds
d /. j = Sum (mlt (p,(Col (M,j))))
; for b, c being FinSequence of V1 st len b = m & len c = n & ( for i being Nat st i in dom c holds
c /. i = Sum (lmlt ((Line (M,i)),b)) ) holds
Sum (lmlt (p,c)) = Sum (lmlt (d,b))
let b, c be FinSequence of V1; ( len b = m & len c = n & ( for i being Nat st i in dom c holds
c /. i = Sum (lmlt ((Line (M,i)),b)) ) implies Sum (lmlt (p,c)) = Sum (lmlt (d,b)) )
assume that
A7:
len b = m
and
A8:
len c = n
and
A9:
for i being Nat st i in dom c holds
c /. i = Sum (lmlt ((Line (M,i)),b))
; Sum (lmlt (p,c)) = Sum (lmlt (d,b))
deffunc H1( Nat, Nat) -> Element of the carrier of V1 = ((p /. $1) * (M * ($1,$2))) * (b /. $2);
consider M1 being Matrix of n1,m1, the carrier of V1 such that
A10:
for i, j being Nat st [i,j] in Indices M1 holds
M1 * (i,j) = H1(i,j)
from MATRIX_0:sch 1();
A11: width M1 =
len (M1 @)
by MATRIX_0:def 6
.=
len (Sum (M1 @))
by MATRLIN:def 6
;
A12:
dom d = dom b
by A5, A7, FINSEQ_3:29;
then A13:
dom (lmlt (d,b)) = dom b
by Th12;
then A14: len (lmlt (d,b)) =
len b
by FINSEQ_3:29
.=
len (Sum (M1 @))
by A1, A7, A11, MATRIX_0:23
;
then A15:
dom (lmlt (d,b)) = Seg (len (Sum (M1 @)))
by FINSEQ_1:def 3;
A16:
width M1 = m
by A1, MATRIX_0:23;
A17:
len M1 = n
by A1, MATRIX_0:23;
A19:
now for j being Nat st j in dom (lmlt (d,b)) holds
(lmlt (d,b)) . j = (Sum (M1 @)) . jA20:
Seg (len (Sum (M1 @))) = dom (Sum (M1 @))
by FINSEQ_1:def 3;
let j be
Nat;
( j in dom (lmlt (d,b)) implies (lmlt (d,b)) . j = (Sum (M1 @)) . j )assume A21:
j in dom (lmlt (d,b))
;
(lmlt (d,b)) . j = (Sum (M1 @)) . jA22:
j in dom (Sum (M1 @))
by A15, A21, FINSEQ_1:def 3;
A23:
j in dom d
by A12, A21, Th12;
A24:
(
d /. j = d . j &
b /. j = b . j )
by A12, A13, A21, PARTFUN1:def 6;
len (Sum (M1 @)) = len (M1 @)
by MATRLIN:def 6;
then A25:
dom (Sum (M1 @)) = dom (M1 @)
by FINSEQ_3:29;
then A26:
(M1 @) /. j =
(M1 @) . j
by A22, PARTFUN1:def 6
.=
Line (
(M1 @),
j)
by A22, A25, MATRIX_0:60
;
reconsider H =
mlt (
p,
(Col (M,j))) as
FinSequence of
INT.Ring ;
deffunc H2(
Nat)
-> Element of the
carrier of
V1 =
(H /. $1) * (b /. j);
consider G being
FinSequence of
V1 such that A27:
(
len G = len p & ( for
i being
Nat st
i in dom G holds
G . i = H2(
i) ) )
from FINSEQ_2:sch 1();
A28:
len p = len (Col (M,j))
by A4, A3, MATRIX_0:def 8;
then A29:
len ( the multF of INT.Ring .: (p,(Col (M,j)))) = len p
by FINSEQ_2:72;
then A30:
dom H = dom G
by A27, FINSEQ_3:29;
A31:
dom p = dom G
by A27, FINSEQ_3:29;
A32:
len (Line ((M1 @),j)) =
width (M1 @)
by MATRIX_0:def 7
.=
len ((M1 @) @)
by MATRIX_0:def 6
.=
len G
by A1, A2, A4, A17, A16, A27, MATRIX_0:57
;
then A33:
dom (Line ((M1 @),j)) = Seg (len G)
by FINSEQ_1:def 3;
A34:
dom G = Seg (len p)
by A27, FINSEQ_1:def 3;
A35:
now for i being Nat st i in dom (Line ((M1 @),j)) holds
(Line ((M1 @),j)) . i = G . ilet i be
Nat;
( i in dom (Line ((M1 @),j)) implies (Line ((M1 @),j)) . i = G . i )A36:
dom M = Seg (len M)
by FINSEQ_1:def 3;
assume A37:
i in dom (Line ((M1 @),j))
;
(Line ((M1 @),j)) . i = G . ithen A38:
i in Seg (len ( the multF of INT.Ring .: (p,(Col (M,j)))))
by A27, A28, A33, FINSEQ_2:72;
then A39:
i in dom H
by FINSEQ_1:def 3;
A40:
i in dom (multint .: (p,(Col (M,j))))
by A38, FINSEQ_1:def 3;
A41:
Seg (len G) = dom G
by FINSEQ_1:def 3;
then
p /. i = p . i
by A31, A33, A37, PARTFUN1:def 6;
then A42:
(p /. i) * (M * (i,j)) =
multint . (
(p . i),
((Col (M,j)) . i))
by A4, A3, A27, A33, A37, A36, MATRIX_0:def 8
.=
(multint .: (p,(Col (M,j)))) . i
by A40, FUNCOP_1:22
.=
H /. i
by A39, PARTFUN1:def 6
;
dom M1 = dom G
by A4, A17, A27, FINSEQ_3:29;
then A43:
[i,j] in Indices M1
by A11, A15, A21, A33, A37, A41, ZFMISC_1:87;
i in Seg (width (M1 @))
by A32, A33, A37, MATRIX_0:def 7;
hence (Line ((M1 @),j)) . i =
(M1 @) * (
j,
i)
by MATRIX_0:def 7
.=
M1 * (
i,
j)
by A43, MATRIX_0:def 6
.=
(H /. i) * (b /. j)
by A10, A43, A42
.=
G . i
by A27, A34, A33, A37
;
verum end; thus (lmlt (d,b)) . j =
the
lmult of
V1 . (
(d . j),
(b . j))
by A21, FUNCOP_1:22
.=
(Sum H) * (b /. j)
by A6, A23, A24
.=
Sum G
by A27, A29, A30, Th10
.=
Sum ((M1 @) /. j)
by A32, A35, A26, FINSEQ_2:9
.=
(Sum (M1 @)) /. j
by A22, MATRLIN:def 6
.=
(Sum (M1 @)) . j
by A15, A21, A20, PARTFUN1:def 6
;
verum end;
A44:
dom p = dom c
by A4, A8, FINSEQ_3:29;
then A45:
dom (lmlt (p,c)) = dom p
by Th12;
then A46: len (lmlt (p,c)) =
len p
by FINSEQ_3:29
.=
len M1
by A4, MATRIX_0:def 2
.=
len (Sum M1)
by MATRLIN:def 6
;
now for i being Nat st i in dom (Sum M1) holds
(lmlt (p,c)) . i = (Sum M1) . ilet i be
Nat;
( i in dom (Sum M1) implies (lmlt (p,c)) . i = (Sum M1) . i )assume A47:
i in dom (Sum M1)
;
(lmlt (p,c)) . i = (Sum M1) . iA48:
i in dom c
by A44, A45, A46, A47, FINSEQ_3:29;
then A49:
(
c . i = c /. i &
p . i = p /. i )
by A44, PARTFUN1:def 6;
i in Seg (len (Sum M1))
by A47, FINSEQ_1:def 3;
then
i in Seg (len M1)
by MATRLIN:def 6;
then A50:
i in dom M1
by FINSEQ_1:def 3;
then A51:
M1 /. i =
M1 . i
by PARTFUN1:def 6
.=
Line (
M1,
i)
by A50, MATRIX_0:60
;
deffunc H2(
Nat)
-> Element of the
carrier of
V1 =
(p /. i) * ((lmlt ((Line (M,i)),b)) /. $1);
consider F being
FinSequence of
V1 such that A52:
(
len F = len b & ( for
j being
Nat st
j in dom F holds
F . j = H2(
j) ) )
from FINSEQ_2:sch 1();
A53:
len F = width M
by A1, A7, A52, MATRIX_0:23;
A54:
dom (Line (M,i)) =
Seg (len (Line (M,i)))
by FINSEQ_1:def 3
.=
dom b
by A52, A53, FINSEQ_1:def 3, MATRIX_0:def 7
;
then
dom (lmlt ((Line (M,i)),b)) = dom b
by Th12;
then A55:
(
len F = len (lmlt ((Line (M,i)),b)) &
dom F = dom (lmlt ((Line (M,i)),b)) )
by A52, FINSEQ_3:29;
A56:
len F = width M1
by A1, A7, A52, MATRIX_0:23;
then A57:
len (Line (M1,i)) = len F
by MATRIX_0:def 7;
then A58:
dom (M1 /. i) = Seg (len F)
by A51, FINSEQ_1:def 3;
A59:
dom F = Seg (len b)
by A52, FINSEQ_1:def 3;
A60:
now for j being Nat st j in dom (M1 /. i) holds
(M1 /. i) . j = F . jlet j be
Nat;
( j in dom (M1 /. i) implies (M1 /. i) . j = F . j )assume A61:
j in dom (M1 /. i)
;
(M1 /. i) . j = F . jthen A62:
(Line (M,i)) . j = M * (
i,
j)
by A53, A58, MATRIX_0:def 7;
A63:
[i,j] in Indices M1
by A56, A50, A58, A61, ZFMISC_1:87;
A64:
j in dom b
by A52, A58, A61, FINSEQ_1:def 3;
then A65:
b . j = b /. j
by PARTFUN1:def 6;
A66:
j in dom (lmlt ((Line (M,i)),b))
by A54, A64, Th12;
then A67:
(lmlt ((Line (M,i)),b)) /. j =
(lmlt ((Line (M,i)),b)) . j
by PARTFUN1:def 6
.=
(M * (i,j)) * (b /. j)
by A65, A62, A66, FUNCOP_1:22
;
thus (M1 /. i) . j =
M1 * (
i,
j)
by A56, A51, A58, A61, MATRIX_0:def 7
.=
((p /. i) * (M * (i,j))) * (b /. j)
by A10, A63
.=
(p /. i) * ((lmlt ((Line (M,i)),b)) /. j)
by A67, VECTSP_1:def 16
.=
F . j
by A52, A59, A58, A61
;
verum end; A68:
for
j being
Nat for
v being
Vector of
V1 st
j in dom F &
v = (lmlt ((Line (M,i)),b)) . j holds
F . j = (p /. i) * v
proof
let j be
Nat;
for v being Vector of V1 st j in dom F & v = (lmlt ((Line (M,i)),b)) . j holds
F . j = (p /. i) * vlet v be
Vector of
V1;
( j in dom F & v = (lmlt ((Line (M,i)),b)) . j implies F . j = (p /. i) * v )
assume A681:
(
j in dom F &
v = (lmlt ((Line (M,i)),b)) . j )
;
F . j = (p /. i) * v
thus F . j =
(p /. i) * ((lmlt ((Line (M,i)),b)) /. j)
by A52, A681
.=
(p /. i) * v
by A55, A681, PARTFUN1:def 6
;
verum
end;
i in dom ( the lmult of V1 .: (p,c))
by A46, A47, FINSEQ_3:29;
hence (lmlt (p,c)) . i =
the
lmult of
V1 . (
(p . i),
(c . i))
by FUNCOP_1:22
.=
(p /. i) * (Sum (lmlt ((Line (M,i)),b)))
by A9, A48, A49
.=
Sum F
by A55, A68, ZMODUL01:12
.=
Sum (M1 /. i)
by A57, A51, A60, FINSEQ_2:9
.=
(Sum M1) /. i
by A47, MATRLIN:def 6
.=
(Sum M1) . i
by A47, PARTFUN1:def 6
;
verum end;
hence Sum (lmlt (p,c)) =
Sum (Sum M1)
by A46, FINSEQ_2:9
.=
Sum (Sum (M1 @))
by Th32
.=
Sum (lmlt (d,b))
by A14, A19, FINSEQ_2:9
;
verum