reconsider Mf = M * F as Matrix of n,m,D by Lm7;
let Mp be Matrix of n,m,D; ( Mp = F * M iff ( len Mp = len M & width Mp = width M & ( for i, j, k being Nat st [i,j] in Indices M & F . i = k holds
Mp * (i,j) = M * (k,j) ) ) )
thus
( Mp = M * F implies ( len Mp = len M & width Mp = width M & ( for i, j, k being Nat st [i,j] in Indices M & F . i = k holds
Mp * (i,j) = M * (k,j) ) ) )
( len Mp = len M & width Mp = width M & ( for i, j, k being Nat st [i,j] in Indices M & F . i = k holds
Mp * (i,j) = M * (k,j) ) implies Mp = F * M )proof
A1:
rng F c= Seg n
by RELAT_1:def 19;
assume A2:
Mp = M * F
;
( len Mp = len M & width Mp = width M & ( for i, j, k being Nat st [i,j] in Indices M & F . i = k holds
Mp * (i,j) = M * (k,j) ) )
A3:
len M = n
by MATRIX_0:def 2;
A4:
len Mp = n
by MATRIX_0:def 2;
hence
(
len Mp = len M &
width Mp = width M )
by A3, MATRIX_0:def 2;
for i, j, k being Nat st [i,j] in Indices M & F . i = k holds
Mp * (i,j) = M * (k,j)
let i,
j,
k be
Nat;
( [i,j] in Indices M & F . i = k implies Mp * (i,j) = M * (k,j) )
assume that A8:
[i,j] in Indices M
and A9:
F . i = k
;
Mp * (i,j) = M * (k,j)
Indices M = [:(Seg n),(Seg (width M)):]
by MATRIX_0:25;
then A10:
i in Seg n
by A8, ZFMISC_1:87;
then A11:
Line (
Mp,
i)
= Mp . i
by MATRIX_0:52;
dom F = Seg n
by FUNCT_2:52;
then A12:
F . i in rng F
by A10, FUNCT_1:def 3;
len Mp = n
by MATRIX_0:25;
then
dom Mp = Seg n
by FINSEQ_1:def 3;
then
Mp . i = M . k
by A2, A9, A10, FUNCT_1:12;
then A13:
Line (
Mp,
i)
= Line (
M,
k)
by A9, A12, A1, A11, MATRIX_0:52;
A14:
j in Seg (width M)
by A8, ZFMISC_1:87;
then
(Line (M,k)) . j = M * (
k,
j)
by MATRIX_0:def 7;
hence
Mp * (
i,
j)
= M * (
k,
j)
by A5, A14, A13, MATRIX_0:def 7;
verum
end;
assume that
A15:
len Mp = len M
and
A16:
width Mp = width M
; ( ex i, j, k being Nat st
( [i,j] in Indices M & F . i = k & not Mp * (i,j) = M * (k,j) ) or Mp = F * M )
assume A17:
for i, j, k being Nat st [i,j] in Indices M & F . i = k holds
Mp * (i,j) = M * (k,j)
; Mp = F * M
for i, j being Nat st [i,j] in Indices Mp holds
Mp * (i,j) = Mf * (i,j)
proof
A18:
Indices Mp = Indices M
by A15, A16, MATRIX_4:55;
let i,
j be
Nat;
( [i,j] in Indices Mp implies Mp * (i,j) = Mf * (i,j) )
assume A19:
[i,j] in Indices Mp
;
Mp * (i,j) = Mf * (i,j)
Indices Mp = [:(Seg n),(Seg (width M)):]
by A16, MATRIX_0:25;
then A20:
i in Seg n
by A19, ZFMISC_1:87;
then A21:
Line (
Mf,
i)
= Mf . i
by MATRIX_0:52;
A22:
rng F c= Seg n
by RELAT_1:def 19;
dom F = Seg n
by FUNCT_2:52;
then A23:
F . i in rng F
by A20, FUNCT_1:def 3;
then
F . i in Seg n
by A22;
then reconsider k =
F . i as
Element of
NAT ;
len Mf = n
by MATRIX_0:25;
then
dom Mf = Seg n
by FINSEQ_1:def 3;
then
Mf . i = M . k
by A20, FUNCT_1:12;
then A24:
Line (
Mf,
i)
= Line (
M,
k)
by A23, A22, A21, MATRIX_0:52;
A25:
width M = len (Line (M,k))
by MATRIX_0:def 7;
A26:
width Mf = len (Line (Mf,i))
by MATRIX_0:def 7;
A27:
j in Seg (width M)
by A16, A19, ZFMISC_1:87;
then
(Line (M,k)) . j = M * (
k,
j)
by MATRIX_0:def 7;
then
Mf * (
i,
j)
= M * (
k,
j)
by A27, A24, A25, A26, MATRIX_0:def 7;
hence
Mp * (
i,
j)
= Mf * (
i,
j)
by A17, A19, A18;
verum
end;
hence
Mp = F * M
by MATRIX_0:27; verum