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