let n be Nat; for K being commutative Ring
for p being Element of Permutations n
for A being Matrix of n,K st n >= 1 holds
Path_matrix ((p "),(A @)) = (Path_matrix (p,A)) * (p ")
let K be commutative Ring; for p being Element of Permutations n
for A being Matrix of n,K st n >= 1 holds
Path_matrix ((p "),(A @)) = (Path_matrix (p,A)) * (p ")
let p be Element of Permutations n; for A being Matrix of n,K st n >= 1 holds
Path_matrix ((p "),(A @)) = (Path_matrix (p,A)) * (p ")
let A be Matrix of n,K; ( n >= 1 implies Path_matrix ((p "),(A @)) = (Path_matrix (p,A)) * (p ") )
set f = Path_matrix (p,A);
reconsider fp = p " as Function of (Seg n),(Seg n) by MATRIX_1:def 12;
reconsider fp0 = p as Function of (Seg n),(Seg n) by MATRIX_1:def 12;
assume A1:
n >= 1
; Path_matrix ((p "),(A @)) = (Path_matrix (p,A)) * (p ")
then A2:
dom fp = Seg n
by FUNCT_2:def 1;
A3:
len (Path_matrix (p,A)) = n
by MATRIX_3:def 7;
then reconsider m = (Path_matrix (p,A)) * (p ") as FinSequence of K by A1, Th33;
p " is Permutation of (Seg n)
by MATRIX_1:def 12;
then A4:
rng fp = Seg n
by FUNCT_2:def 3;
then
rng (p ") c= dom (Path_matrix (p,A))
by A3, FINSEQ_1:def 3;
then A5:
dom ((Path_matrix (p,A)) * (p ")) = dom fp
by RELAT_1:27;
A6:
p is Permutation of (Seg n)
by MATRIX_1:def 12;
A7:
for i, j being Nat st i in dom m & j = (p ") . i holds
m . i = (A @) * (i,j)
proof
let i,
j be
Nat;
( i in dom m & j = (p ") . i implies m . i = (A @) * (i,j) )
assume that A8:
i in dom m
and A9:
j = (p ") . i
;
m . i = (A @) * (i,j)
A10:
j in Seg n
by A4, A5, A8, A9, FUNCT_1:def 3;
then A11:
j in dom (Path_matrix (p,A))
by A3, FINSEQ_1:def 3;
rng fp0 = Seg n
by A6, FUNCT_2:def 3;
then
i = p . j
by A5, A2, A8, A9, FUNCT_1:32;
then A12:
(Path_matrix (p,A)) . j = A * (
j,
i)
by A11, MATRIX_3:def 7;
A13:
dom A =
Seg (len A)
by FINSEQ_1:def 3
.=
Seg n
by MATRIX_0:def 2
;
len A = n
by MATRIX_0:def 2;
then
i in Seg (width A)
by A1, A5, A2, A8, MATRIX_0:20;
then A14:
[j,i] in Indices A
by A10, A13, ZFMISC_1:def 2;
((Path_matrix (p,A)) * (p ")) . i = (Path_matrix (p,A)) . ((p ") . i)
by A5, A8, FUNCT_1:13;
hence
m . i = (A @) * (
i,
j)
by A9, A12, A14, MATRIX_0:def 6;
verum
end;
n in NAT
by ORDINAL1:def 12;
then
len m = n
by A5, A2, FINSEQ_1:def 3;
hence
Path_matrix ((p "),(A @)) = (Path_matrix (p,A)) * (p ")
by A7, MATRIX_3:def 7; verum