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