let K be Ring; for A, B, C being Matrix of K st width A = len B & width B = len C holds
(A * B) * C = A * (B * C)
let A, B, C be Matrix of K; ( width A = len B & width B = len C implies (A * B) * C = A * (B * C) )
assume that
A1:
width A = len B
and
A2:
width B = len C
; (A * B) * C = A * (B * C)
A3:
len (B * C) = width A
by A1, A2, Def4;
A4:
width (B * C) = width C
by A2, Def4;
then A5:
width (A * (B * C)) = width C
by A3, Def4;
A6:
len (A * (B * C)) = len A
by A3, Def4;
then A7:
Indices (A * (B * C)) = [:(dom A),(Seg (width C)):]
by A5, FINSEQ_3:29;
A8:
width (A * B) = len C
by A1, A2, Def4;
then A9:
width ((A * B) * C) = width C
by Def4;
len (A * B) = len A
by A1, Def4;
then A10:
len ((A * B) * C) = len A
by A8, Def4;
then A11:
Indices ((A * B) * C) = [:(dom A),(Seg (width C)):]
by A9, FINSEQ_3:29;
A12:
width ((A * B) * C) = width (A * (B * C))
by A5, A8, Def4;
A13:
len ((A * B) * C) = len (A * (B * C))
by A6, A10;
for i, j being Nat st [i,j] in Indices ((A * B) * C) holds
((A * B) * C) * (i,j) = (A * (B * C)) * (i,j)
proof
let i,
j be
Nat;
( [i,j] in Indices ((A * B) * C) implies ((A * B) * C) * (i,j) = (A * (B * C)) * (i,j) )
assume
[i,j] in Indices ((A * B) * C)
;
((A * B) * C) * (i,j) = (A * (B * C)) * (i,j)
then A14:
(
[i,j] in Indices ((A * B) * C) &
[i,j] in Indices (A * (B * C)) )
by A7, A11;
reconsider X =
findom B as
Element of
Fin NAT ;
reconsider Y =
findom C as
Element of
Fin NAT ;
deffunc H1(
Element of
NAT ,
Element of
NAT )
-> Element of the
carrier of
K =
(A * (i,$1)) * ((B * ($1,$2)) * (C * ($2,j)));
consider f being
Function of
[:NAT,NAT:], the
carrier of
K such that A15:
for
k1,
k2 being
Element of
NAT holds
f . (
k1,
k2)
= H1(
k1,
k2)
from BINOP_1:sch 4();
A16:
for
k being
Element of
NAT st
k in NAT holds
((curry f) . k) | (dom C) = (A * (i,k)) * (mlt ((Line (B,k)),(Col (C,j))))
proof
let k be
Element of
NAT ;
( k in NAT implies ((curry f) . k) | (dom C) = (A * (i,k)) * (mlt ((Line (B,k)),(Col (C,j)))) )
assume
k in NAT
;
((curry f) . k) | (dom C) = (A * (i,k)) * (mlt ((Line (B,k)),(Col (C,j))))
A17:
{k} c= NAT
by ZFMISC_1:31;
A18:
dom (curry f) = NAT
by FUNCT_2:def 1;
dom f = [:NAT,NAT:]
by FUNCT_2:def 1;
then A19:
dom ((curry f) . k) =
proj2 ([:NAT,NAT:] /\ [:{k},(proj2 [:NAT,NAT:]):])
by A18, FUNCT_5:31
.=
proj2 ([:{k},NAT:] /\ [:NAT,NAT:])
by FUNCT_5:9
.=
proj2 [:{k},NAT:]
by A17, ZFMISC_1:101
.=
NAT
by FUNCT_5:9
;
then A20:
dom (((curry f) . k) | (dom C)) =
NAT /\ (dom C)
by RELAT_1:61
.=
dom C
by XBOOLE_1:28
;
reconsider a =
A * (
i,
k) as
Element of
K ;
reconsider p =
mlt (
(Line (B,k)),
(Col (C,j))) as
FinSequence of
K ;
A21:
len (mlt ((Line (B,k)),(Col (C,j)))) = len ( the multF of K .: ((Line (B,k)),(Col (C,j))))
by FVSUM_1:def 7;
len (Line (B,k)) =
len C
by A2, MATRIX_0:def 7
.=
len (Col (C,j))
by MATRIX_0:def 8
;
then A22:
len ( the multF of K .: ((Line (B,k)),(Col (C,j)))) =
len (Line (B,k))
by FINSEQ_2:72
.=
len C
by A2, MATRIX_0:def 7
;
dom (a multfield) = the
carrier of
K
by FUNCT_2:def 1;
then
(
a * p = (a multfield) * p &
rng p c= dom (a multfield) )
by FINSEQ_1:def 4, FVSUM_1:def 6;
then A23:
dom (a * p) = dom p
by RELAT_1:27;
then A24:
dom ((A * (i,k)) * (mlt ((Line (B,k)),(Col (C,j))))) = dom C
by A21, A22, FINSEQ_3:29;
for
l being
object st
l in dom C holds
(((curry f) . k) | (dom C)) . l = ((A * (i,k)) * (mlt ((Line (B,k)),(Col (C,j))))) . l
proof
let l be
object ;
( l in dom C implies (((curry f) . k) | (dom C)) . l = ((A * (i,k)) * (mlt ((Line (B,k)),(Col (C,j))))) . l )
assume A25:
l in dom C
;
(((curry f) . k) | (dom C)) . l = ((A * (i,k)) * (mlt ((Line (B,k)),(Col (C,j))))) . l
then reconsider l9 =
l as
Element of
NAT ;
A26:
l in dom (a * p)
by A21, A22, A23, A25, FINSEQ_3:29;
l9 in dom p
by A21, A22, A25, FINSEQ_3:29;
then reconsider b =
p . l9 as
Element of
K by FINSEQ_2:11;
dom ( the multF of K .: ((Line (B,k)),(Col (C,j)))) = Seg (len ( the multF of K .: ((Line (B,k)),(Col (C,j)))))
by FINSEQ_1:def 3;
then A27:
l9 in dom ( the multF of K .: ((Line (B,k)),(Col (C,j))))
by A22, A25, FINSEQ_1:def 3;
A28:
Seg (len C) = dom C
by FINSEQ_1:def 3;
thus (((curry f) . k) | (dom C)) . l =
((curry f) . k) . l9
by A25, FUNCT_1:49
.=
f . (
k,
l9)
by A18, A19, FUNCT_5:31
.=
(A * (i,k)) * ((B * (k,l9)) * (C * (l9,j)))
by A15
.=
the
multF of
K . (
(A * (i,k)),
( the multF of K . (((Line (B,k)) . l9),(C * (l9,j)))))
by A2, A28, A25, MATRIX_0:def 7
.=
the
multF of
K . (
(A * (i,k)),
( the multF of K . (((Line (B,k)) . l9),((Col (C,j)) . l9))))
by A25, MATRIX_0:def 8
.=
the
multF of
K . (
(A * (i,k)),
(( the multF of K .: ((Line (B,k)),(Col (C,j)))) . l9))
by A27, FUNCOP_1:22
.=
a * b
by FVSUM_1:def 7
.=
((A * (i,k)) * (mlt ((Line (B,k)),(Col (C,j))))) . l
by A26, FVSUM_1:50
;
verum
end;
hence
((curry f) . k) | (dom C) = (A * (i,k)) * (mlt ((Line (B,k)),(Col (C,j))))
by A20, A24, FUNCT_1:2;
verum
end;
deffunc H2(
Element of
NAT )
-> Element of the
carrier of
K = the
addF of
K $$ (
Y,
((curry f) . $1));
deffunc H3(
Element of
NAT )
-> Element of the
carrier of
K = the
addF of
K $$ (
X,
((curry' f) . $1));
consider g being
sequence of the
carrier of
K such that A29:
for
k being
Element of
NAT holds
g . k = H2(
k)
from FUNCT_2:sch 4();
A30:
dom (g | (dom B)) =
(dom g) /\ (dom B)
by RELAT_1:61
.=
NAT /\ (dom B)
by FUNCT_2:def 1
.=
dom B
by XBOOLE_1:28
;
len (Line ((A * B),i)) =
width (A * B)
by MATRIX_0:def 7
.=
len C
by A1, A2, Def4
.=
len (Col (C,j))
by MATRIX_0:def 8
;
then A31:
len ( the multF of K .: ((Line ((A * B),i)),(Col (C,j)))) =
len (Col (C,j))
by FINSEQ_2:72
.=
len C
by MATRIX_0:def 8
;
len (Col ((B * C),j)) =
len (B * C)
by MATRIX_0:def 8
.=
width A
by A1, A2, Def4
.=
len (Line (A,i))
by MATRIX_0:def 7
;
then A32:
len ( the multF of K .: ((Line (A,i)),(Col ((B * C),j)))) =
len (Line (A,i))
by FINSEQ_2:72
.=
width A
by MATRIX_0:def 7
;
A33:
i in dom A
by A11, A14, ZFMISC_1:87;
A34:
0. K = the_unity_wrt the
addF of
K
by FVSUM_1:7;
0. K is_a_unity_wrt the
addF of
K
by FVSUM_1:6;
then A35:
the
addF of
K is
having_a_unity
by SETWISEO:def 2;
A36:
for
k9 being
object st
k9 in dom B holds
(g | (dom B)) . k9 = (mlt ((Line (A,i)),(Col ((B * C),j)))) . k9
proof
let k9 be
object ;
( k9 in dom B implies (g | (dom B)) . k9 = (mlt ((Line (A,i)),(Col ((B * C),j)))) . k9 )
assume A37:
k9 in dom B
;
(g | (dom B)) . k9 = (mlt ((Line (A,i)),(Col ((B * C),j)))) . k9
then reconsider k =
k9 as
Element of
NAT ;
A38:
k in dom ( the multF of K .: ((Line (A,i)),(Col ((B * C),j))))
by A1, A32, A37, FINSEQ_3:29;
reconsider p =
mlt (
(Line (B,k)),
(Col (C,j))) as
FinSequence of
K ;
reconsider a =
A * (
i,
k) as
Element of
K ;
dom (a multfield) = the
carrier of
K
by FUNCT_2:def 1;
then
(
a * p = (a multfield) * p &
rng p c= dom (a multfield) )
by FINSEQ_1:def 4, FVSUM_1:def 6;
then A39:
dom (a * p) = dom p
by RELAT_1:27;
len (Line (B,k)) =
len C
by A2, MATRIX_0:def 7
.=
len (Col (C,j))
by MATRIX_0:def 8
;
then len ( the multF of K .: ((Line (B,k)),(Col (C,j)))) =
len (Line (B,k))
by FINSEQ_2:72
.=
len C
by A2, MATRIX_0:def 7
;
then
len C = len p
by FVSUM_1:def 7;
then A40:
dom ((A * (i,k)) * (mlt ((Line (B,k)),(Col (C,j))))) = dom C
by A39, FINSEQ_3:29;
then
([#] (((A * (i,k)) * (mlt ((Line (B,k)),(Col (C,j))))),(0. K))) | (dom C) = (A * (i,k)) * (mlt ((Line (B,k)),(Col (C,j))))
by SETWOP_2:21;
then A41:
([#] (((A * (i,k)) * (mlt ((Line (B,k)),(Col (C,j))))),(0. K))) | (dom C) = ((curry f) . k) | (dom C)
by A16;
[i,j] in Indices (A * (B * C))
by A14;
then
j in Seg (width C)
by A5, ZFMISC_1:87;
then A42:
j in Seg (width (B * C))
by A4;
dom (B * C) = dom B
by A1, A3, FINSEQ_3:29;
then
k in dom (B * C)
by A37;
then A43:
[k,j] in Indices (B * C)
by A42, ZFMISC_1:87;
k in Seg (width A)
by A1, A37, FINSEQ_1:def 3;
then
(
i in dom A &
k in Seg (width A) )
by A33;
then A44:
A * (
i,
k)
= (Line (A,i)) . k
by MATRIX_0:def 7;
dom (B * C) = dom B
by A1, A3, FINSEQ_3:29;
then
(
k in dom (B * C) &
j in Seg (width (B * C)) )
by A37, A42;
then A45:
(B * C) * (
k,
j)
= (Col ((B * C),j)) . k
by MATRIX_0:def 8;
thus (g | (dom B)) . k9 =
g . k
by A30, A37, FUNCT_1:47
.=
the
addF of
K $$ (
Y,
((curry f) . k))
by A29
.=
the
addF of
K $$ (
Y,
([#] (((A * (i,k)) * (mlt ((Line (B,k)),(Col (C,j))))),(0. K))))
by A41, FVSUM_1:8, SETWOP_2:7
.=
the
addF of
K $$ (a * p)
by A40, A35, A34, SETWOP_2:def 2
.=
Sum (a * p)
by FVSUM_1:def 8
.=
(A * (i,k)) * (Sum (mlt ((Line (B,k)),(Col (C,j)))))
by FVSUM_1:73
.=
(A * (i,k)) * ((Line (B,k)) "*" (Col (C,j)))
by FVSUM_1:def 9
.=
(A * (i,k)) * ((B * C) * (k,j))
by A2, A43, Def4
.=
( the multF of K .: ((Line (A,i)),(Col ((B * C),j)))) . k
by A38, A44, A45, FUNCOP_1:22
.=
(mlt ((Line (A,i)),(Col ((B * C),j)))) . k9
by FVSUM_1:def 7
;
verum
end;
consider h being
sequence of the
carrier of
K such that A46:
for
l being
Element of
NAT holds
h . l = H3(
l)
from FUNCT_2:sch 4();
A47:
dom (h | (dom C)) =
(dom h) /\ (dom C)
by RELAT_1:61
.=
NAT /\ (dom C)
by FUNCT_2:def 1
.=
dom C
by XBOOLE_1:28
;
A48:
for
l9 being
object st
l9 in dom C holds
(h | (dom C)) . l9 = (mlt ((Line ((A * B),i)),(Col (C,j)))) . l9
proof
let l9 be
object ;
( l9 in dom C implies (h | (dom C)) . l9 = (mlt ((Line ((A * B),i)),(Col (C,j)))) . l9 )
assume A49:
l9 in dom C
;
(h | (dom C)) . l9 = (mlt ((Line ((A * B),i)),(Col (C,j)))) . l9
then reconsider l =
l9 as
Element of
NAT ;
A50:
for
k being
Element of
NAT holds
((curry' f) . l) . k = ((A * (i,k)) * (B * (k,l))) * (C * (l,j))
proof
let k be
Element of
NAT ;
((curry' f) . l) . k = ((A * (i,k)) * (B * (k,l))) * (C * (l,j))
thus ((curry' f) . l) . k =
f . (
k,
l)
by FUNCT_5:70
.=
(A * (i,k)) * ((B * (k,l)) * (C * (l,j)))
by A15
.=
((A * (i,k)) * (B * (k,l))) * (C * (l,j))
by GROUP_1:def 3
;
verum
end;
reconsider p1 =
mlt (
(Line (A,i)),
(Col (B,l))) as
FinSequence of the
carrier of
K ;
A51:
len (Line (A,i)) =
len B
by A1, MATRIX_0:def 7
.=
len (Col (B,l))
by MATRIX_0:def 8
;
A52:
len (mlt ((Line (A,i)),(Col (B,l)))) =
len ( the multF of K .: ((Line (A,i)),(Col (B,l))))
by FVSUM_1:def 7
.=
len (Line (A,i))
by A51, FINSEQ_2:72
.=
len B
by A1, MATRIX_0:def 7
;
dom B = Seg (len B)
by FINSEQ_1:def 3;
then reconsider p2 =
((curry' f) . l) | (dom B) as
FinSequence of
K by FINSEQ_2:27;
A53:
dom p2 =
(dom ((curry' f) . l)) /\ (dom B)
by RELAT_1:61
.=
NAT /\ (dom B)
by FUNCT_2:def 1
.=
dom B
by XBOOLE_1:28
;
then A54:
findom p2 = X
;
then A55:
len p1 = len p2
by A52, FINSEQ_3:29;
A56:
([#] (p2,(0. K))) | (dom B) = p2
by A53, SETWOP_2:21;
for
i2 being
Element of
NAT for
k being
Element of
K st
i2 in dom p1 &
k = p1 . i2 holds
p2 . i2 = k * (C * (l,j))
proof
let i2 be
Element of
NAT ;
for k being Element of K st i2 in dom p1 & k = p1 . i2 holds
p2 . i2 = k * (C * (l,j))let k be
Element of
K;
( i2 in dom p1 & k = p1 . i2 implies p2 . i2 = k * (C * (l,j)) )
assume that A57:
i2 in dom p1
and A58:
k = p1 . i2
;
p2 . i2 = k * (C * (l,j))
A59:
i2 in dom (mlt ((Line (A,i)),(Col (B,l))))
by A57;
A60:
(
A * (
i,
i2)
= (Line (A,i)) . i2 &
(Col (B,l)) . i2 = B * (
i2,
l) )
proof
A61:
len (Line (A,i)) =
width A
by MATRIX_0:def 7
.=
len (Col (B,l))
by A1, MATRIX_0:def 8
;
width A =
len (Line (A,i))
by MATRIX_0:def 7
.=
len ( the multF of K .: ((Line (A,i)),(Col (B,l))))
by A61, FINSEQ_2:72
.=
len (mlt ((Line (A,i)),(Col (B,l))))
by FVSUM_1:def 7
;
then A62:
i2 in Seg (width A)
by A57, FINSEQ_1:def 3;
hence
A * (
i,
i2)
= (Line (A,i)) . i2
by MATRIX_0:def 7;
(Col (B,l)) . i2 = B * (i2,l)
width A = len B
by A1;
then
Seg (width A) = Seg (len B)
;
then
i2 in Seg (len B)
by A62;
then
i2 in dom B
by FINSEQ_1:def 3;
hence
(Col (B,l)) . i2 = B * (
i2,
l)
by MATRIX_0:def 8;
verum
end;
p1 . i2 = (A * (i,i2)) * (B * (i2,l))
by A60, A59, FVSUM_1:60;
then A63:
k = (A * (i,i2)) * (B * (i2,l))
by A58;
dom p1 = dom p2
by A55, FINSEQ_3:29;
then
i2 in dom p2
by A57;
then A64:
i2 in dom B
by A53;
thus p2 . i2 =
((curry' f) . l) . i2
by A64, FUNCT_1:49
.=
k * (C * (l,j))
by A63, A50
;
verum
end;
then A65:
Sum p2 = (Sum p1) * (C * (l,j))
by A55, Lm2;
width (A * B) = width B
by A1, Def4;
then A66:
Seg (width (A * B)) = dom C
by A2, FINSEQ_1:def 3;
then A67:
l in Seg (width (A * B))
by A49;
A68:
[i,l] in Indices (A * B)
A69:
((A * B) * (i,l)) * (C * (l,j)) = (mlt ((Line ((A * B),i)),(Col (C,j)))) . l
proof
A70:
(A * B) * (
i,
l)
= (Line ((A * B),i)) . l
by A67, MATRIX_0:def 7;
A71:
C * (
l,
j)
= (Col (C,j)) . l
by A67, A66, MATRIX_0:def 8;
A72:
len (Line ((A * B),i)) =
width (A * B)
by MATRIX_0:def 7
.=
len (Col (C,j))
by A8, MATRIX_0:def 8
;
len C =
len (Col (C,j))
by MATRIX_0:def 8
.=
len ( the multF of K .: ((Line ((A * B),i)),(Col (C,j))))
by A72, FINSEQ_2:72
.=
len (mlt ((Line ((A * B),i)),(Col (C,j))))
by FVSUM_1:def 7
;
then
l in dom (mlt ((Line ((A * B),i)),(Col (C,j))))
by A49, FINSEQ_3:29;
hence
((A * B) * (i,l)) * (C * (l,j)) = (mlt ((Line ((A * B),i)),(Col (C,j)))) . l
by A70, A71, FVSUM_1:60;
verum
end;
thus (h | (dom C)) . l9 =
h . l
by A47, A49, FUNCT_1:47
.=
the
addF of
K $$ (
X,
((curry' f) . l))
by A46
.=
the
addF of
K $$ (
X,
([#] (p2,(0. K))))
by A56, FVSUM_1:8, SETWOP_2:7
.=
the
addF of
K $$ p2
by A34, A54, FVSUM_1:8, SETWOP_2:def 2
.=
Sum p2
by FVSUM_1:def 8
.=
((Line (A,i)) "*" (Col (B,l))) * (C * (l,j))
by A65, FVSUM_1:def 9
.=
(mlt ((Line ((A * B),i)),(Col (C,j)))) . l9
by A1, A68, A69, Def4
;
verum
end;
A73:
len ( the multF of K .: ((Line (A,i)),(Col ((B * C),j)))) = len (mlt ((Line (A,i)),(Col ((B * C),j))))
by FVSUM_1:def 7;
then A74:
dom (mlt ((Line (A,i)),(Col ((B * C),j)))) = X
by A1, A32, FINSEQ_3:29;
A75:
dom (mlt ((Line (A,i)),(Col ((B * C),j)))) = dom B
by A1, A32, A73, FINSEQ_3:29;
then A76:
([#] ((mlt ((Line (A,i)),(Col ((B * C),j)))),(0. K))) | (dom B) = mlt (
(Line (A,i)),
(Col ((B * C),j)))
by SETWOP_2:21;
A77:
g | (dom B) = mlt (
(Line (A,i)),
(Col ((B * C),j)))
by A30, A36, A75, FUNCT_1:2;
len ( the multF of K .: ((Line ((A * B),i)),(Col (C,j)))) = len (mlt ((Line ((A * B),i)),(Col (C,j))))
by FVSUM_1:def 7;
then A78:
dom C = dom (mlt ((Line ((A * B),i)),(Col (C,j))))
by A31, FINSEQ_3:29;
then A79:
h | (dom C) = mlt (
(Line ((A * B),i)),
(Col (C,j)))
by A47, A48, FUNCT_1:2;
A80:
0. K = the_unity_wrt the
addF of
K
by FVSUM_1:7;
dom (mlt ((Line ((A * B),i)),(Col (C,j)))) = dom C
by A78;
then A81:
([#] ((mlt ((Line ((A * B),i)),(Col (C,j)))),(0. K))) | (dom C) = mlt (
(Line ((A * B),i)),
(Col (C,j)))
by SETWOP_2:21;
thus ((A * B) * C) * (
i,
j) =
(Line ((A * B),i)) "*" (Col (C,j))
by A8, A14, Def4
.=
Sum (mlt ((Line ((A * B),i)),(Col (C,j))))
by FVSUM_1:def 9
.=
the
addF of
K $$ (mlt ((Line ((A * B),i)),(Col (C,j))))
by FVSUM_1:def 8
.=
the
addF of
K $$ (
(findom C),
([#] ((mlt ((Line ((A * B),i)),(Col (C,j)))),(0. K))))
by A35, A80, A78, SETWOP_2:def 2
.=
the
addF of
K $$ (
Y,
h)
by A35, A81, A79, SETWOP_2:7
.=
the
addF of
K $$ (
[:X,Y:],
f)
by A35, A46, Th32
.=
the
addF of
K $$ (
X,
g)
by A35, A29, Th30
.=
the
addF of
K $$ (
(findom (mlt ((Line (A,i)),(Col ((B * C),j))))),
([#] ((mlt ((Line (A,i)),(Col ((B * C),j)))),(the_unity_wrt the addF of K))))
by A35, A80, A74, A76, A77, SETWOP_2:7
.=
the
addF of
K $$ (mlt ((Line (A,i)),(Col ((B * C),j))))
by A35, SETWOP_2:def 2
.=
Sum (mlt ((Line (A,i)),(Col ((B * C),j))))
by FVSUM_1:def 8
.=
(Line (A,i)) "*" (Col ((B * C),j))
by FVSUM_1:def 9
.=
(A * (B * C)) * (
i,
j)
by A3, A14, Def4
;
verum
end;
hence
(A * B) * C = A * (B * C)
by A12, A13, MATRIX_0:21; verum