let K be Field; 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:31;
then A6:
Indices (B * C) = [:(dom B),(Seg (width C)):]
by A4, MATRIX_1:def 5;
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:31;
then A9:
Indices (A * (B * C)) = [:(dom A),(Seg (width C)):]
by A5, MATRIX_1:def 5;
0. K is_a_unity_wrt the addF of K
by FVSUM_1:8;
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:31;
then A14:
Indices (A * B) = [:(dom A),(Seg (width B)):]
by A2, A11, MATRIX_1:def 5;
A15:
len ((A * B) * C) = len A
by A13, A11, Def4;
then A16:
dom ((A * B) * C) = dom A
by FINSEQ_3:31;
then A17:
Indices ((A * B) * C) = [:(dom A),(Seg (width C)):]
by A12, MATRIX_1:def 5;
A18:
Indices ((A * B) * C) = [:(dom A),(Seg (width C)):]
by A12, A16, MATRIX_1:def 5;
now 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:37;
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:38
.=
proj2 ([:{k},NAT :] /\ [:NAT ,NAT :])
by FUNCT_5:11
.=
proj2 [:{k},NAT :]
by A21, ZFMISC_1:124
.=
NAT
by FUNCT_5:11
;
then A24:
dom (((curry f) . k) | (dom B)) =
NAT /\ (dom B)
by RELAT_1:90
.=
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_1:def 8
.=
len (Col B,k)
by MATRIX_1:def 9
;
then A26:
len (the multF of K .: (Line A,i),(Col B,k)) =
len (Line A,i)
by FINSEQ_2:86
.=
len B
by A1, MATRIX_1:def 8
;
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:46;
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 let l be
set ;
( 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:31;
l9 in dom p
by A25, A26, A30, FINSEQ_3:31;
then reconsider b =
p . l9 as
Element of
K by FINSEQ_2:13;
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:72
.=
f . k,
l9
by A22, A23, FUNCT_5:38
.=
((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_1:def 8
.=
the
multF of
K . (the multF of K . ((Line A,i) . l9),((Col B,k) . l9)),
(C * k,j)
by A30, MATRIX_1:def 9
.=
the
multF of
K . ((the multF of K .: (Line A,i),(Col B,k)) . l9),
(C * k,j)
by A32, FUNCOP_1:28
.=
b * a
by FVSUM_1:def 7
.=
((C * k,j) * (mlt (Line A,i),(Col B,k))) . l
by A31, FVSUM_1:62
;
verum end;
dom ((C * k,j) * (mlt (Line A,i),(Col B,k))) = dom B
by A25, A26, A27, FINSEQ_3:31;
hence
((curry f) . k) | (dom B) = (C * k,j) * (mlt (Line A,i),(Col B,k))
by A24, A29, FUNCT_1:9;
verum
end; A33:
0. K = the_unity_wrt the
addF of
K
by FVSUM_1:9;
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
Function of
NAT ,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:90
.=
NAT /\ (dom C)
by FUNCT_2:def 1
.=
dom C
by XBOOLE_1:28
;
len (Line (A * B),i) =
width (A * B)
by MATRIX_1:def 8
.=
len C
by A1, A2, Def4
.=
len (Col C,j)
by MATRIX_1:def 9
;
then A36:
len (the multF of K .: (Line (A * B),i),(Col C,j)) =
len (Col C,j)
by FINSEQ_2:86
.=
len C
by MATRIX_1:def 9
;
assume A37:
[i,j] in Indices ((A * B) * C)
;
((A * B) * C) * i,j = (A * (B * C)) * i,jthen A38:
i in dom A
by A17, ZFMISC_1:106;
A39:
now let k9 be
set ;
( 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:31;
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:46;
len (Line A,i) =
len B
by A1, MATRIX_1:def 8
.=
len (Col B,k)
by MATRIX_1:def 9
;
then len (the multF of K .: (Line A,i),(Col B,k)) =
len (Line A,i)
by FINSEQ_2:86
.=
len B
by A1, MATRIX_1:def 8
;
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:31;
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:23;
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:106;
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:70
.=
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:10, SETWOP_2:9
.=
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:92
.=
(C * k,j) * ((Line A,i) "*" (Col B,k))
by FVSUM_1:def 10
.=
((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_1:def 8
.=
the
multF of
K . ((Line (A * B),i) . k),
((Col C,j) . k)
by A40, MATRIX_1:def 9
.=
(the multF of K .: (Line (A * B),i),(Col C,j)) . k
by A41, FUNCOP_1:28
.=
(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:31;
dom (mlt (Line (A * B),i),(Col C,j)) = dom C
by A36, A47, FINSEQ_3:31;
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:23;
len (Col (B * C),j) =
len (B * C)
by MATRIX_1:def 9
.=
width A
by A1, A2, Def4
.=
len (Line A,i)
by MATRIX_1:def 8
;
then A50:
len (the multF of K .: (Line A,i),(Col (B * C),j)) =
len (Line A,i)
by FINSEQ_2:86
.=
width A
by MATRIX_1:def 8
;
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:31;
dom (mlt (Line A,i),(Col (B * C),j)) = dom B
by A1, A50, A51, FINSEQ_3:31;
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:23;
consider h being
Function of
NAT ,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:90
.=
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:106;
A57:
now let k9 be
set ;
( 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:31;
A61:
[k,j] in Indices (B * C)
by A6, A56, A58, ZFMISC_1:106;
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
set st
x in NAT holds
G . x = f . x,
k ) )
by FUNCT_5:39;
then A64:
dom (((curry' f) . k) | (dom C)) =
NAT /\ (dom C)
by RELAT_1:90
.=
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:31;
len (Line B,k) =
len C
by A2, MATRIX_1:def 8
.=
len (Col C,j)
by MATRIX_1:def 9
;
then A66:
len (the multF of K .: (Line B,k),(Col C,j)) =
len (Line B,k)
by FINSEQ_2:86
.=
len C
by A2, MATRIX_1:def 8
;
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:46;
then A68:
dom ((A * i,k) * (mlt (Line B,k),(Col C,j))) = dom C
by A62, A66, FINSEQ_3:31;
A69:
now let l be
set ;
( 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:31;
l9 in dom p
by A62, A66, A70, FINSEQ_3:31;
then reconsider b =
p . l9 as
Element of
K by FINSEQ_2:13;
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:31;
thus (((curry' f) . k) | (dom C)) . l =
((curry' f) . k) . l9
by A70, FUNCT_1:72
.=
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 4
.=
the
multF of
K . (A * i,k),
(the multF of K . ((Line B,k) . l9),(C * l9,j))
by A72, MATRIX_1:def 8
.=
the
multF of
K . (A * i,k),
(the multF of K . ((Line B,k) . l9),((Col C,j) . l9))
by A70, MATRIX_1:def 9
.=
the
multF of
K . (A * i,k),
((the multF of K .: (Line B,k),(Col C,j)) . l9)
by A71, FUNCOP_1:28
.=
a * b
by FVSUM_1:def 7
.=
((A * i,k) * (mlt (Line B,k),(Col C,j))) . l
by A73, FVSUM_1:62
;
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:23;
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:9;
thus (h | (dom B)) . k9 =
h . k
by A55, A58, FUNCT_1:70
.=
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:10, SETWOP_2:9
.=
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:92
.=
(A * i,k) * ((Line B,k) "*" (Col C,j))
by FVSUM_1:def 10
.=
(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_1:def 8
.=
the
multF of
K . ((Line A,i) . k),
((Col (B * C),j) . k)
by A60, MATRIX_1:def 9
.=
(the multF of K .: (Line A,i),(Col (B * C),j)) . k
by A65, FUNCOP_1:28
.=
(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:31;
then A75:
h | (dom B) = mlt (Line A,i),
(Col (B * C),j)
by A55, A57, FUNCT_1:9;
dom (mlt (Line (A * B),i),(Col C,j)) = dom C
by A36, A47, FINSEQ_3:31;
then A76:
g | (dom C) = mlt (Line (A * B),i),
(Col C,j)
by A35, A39, FUNCT_1:9;
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 10
.=
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:9
.=
the
addF of
K $$ [:X,Y:],
f
by A10, A34, Th32
.=
the
addF of
K $$ Y,
h
by A10, A54, Th34
.=
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:9
.=
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 10
.=
(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_1:21; verum