let n be Nat; for K being commutative Ring
for A being Matrix of n,K
for p being Element of Permutations n
for Perm being Permutation of (Seg n)
for q being Element of Permutations n st q = p * (Perm ") holds
Path_matrix (p,(A * Perm)) = (Path_matrix (q,A)) * Perm
let K be commutative Ring; for A being Matrix of n,K
for p being Element of Permutations n
for Perm being Permutation of (Seg n)
for q being Element of Permutations n st q = p * (Perm ") holds
Path_matrix (p,(A * Perm)) = (Path_matrix (q,A)) * Perm
let A be Matrix of n,K; for p being Element of Permutations n
for Perm being Permutation of (Seg n)
for q being Element of Permutations n st q = p * (Perm ") holds
Path_matrix (p,(A * Perm)) = (Path_matrix (q,A)) * Perm
let p be Element of Permutations n; for Perm being Permutation of (Seg n)
for q being Element of Permutations n st q = p * (Perm ") holds
Path_matrix (p,(A * Perm)) = (Path_matrix (q,A)) * Perm
let Perm be Permutation of (Seg n); for q being Element of Permutations n st q = p * (Perm ") holds
Path_matrix (p,(A * Perm)) = (Path_matrix (q,A)) * Perm
let q be Element of Permutations n; ( q = p * (Perm ") implies Path_matrix (p,(A * Perm)) = (Path_matrix (q,A)) * Perm )
assume A1:
q = p * (Perm ")
; Path_matrix (p,(A * Perm)) = (Path_matrix (q,A)) * Perm
reconsider perm = Perm as Element of Permutations n by MATRIX_1:def 12;
set Ap = A * Perm;
set P2 = Path_matrix (q,A);
set P1 = Path_matrix (p,(A * Perm));
A2:
dom perm = Seg n
by FUNCT_2:52;
A3:
p is Permutation of (Seg n)
by MATRIX_1:def 12;
then A4:
dom p = Seg n
by FUNCT_2:52;
A5:
rng p = Seg n
by A3, FUNCT_2:def 3;
A6:
q is Permutation of (Seg n)
by MATRIX_1:def 12;
then A7:
dom q = Seg n
by FUNCT_2:52;
len (Path_matrix (q,A)) = n
by MATRIX_3:def 7;
then A8:
dom (Path_matrix (q,A)) = Seg n
by FINSEQ_1:def 3;
A9:
rng perm = Seg n
by FUNCT_2:def 3;
then A10:
dom ((Path_matrix (q,A)) * perm) = Seg n
by A2, A8, RELAT_1:27;
then reconsider P2p = (Path_matrix (q,A)) * perm as FinSequence by FINSEQ_1:def 2;
A11:
len (Path_matrix (p,(A * Perm))) = n
by MATRIX_3:def 7;
A12:
rng q = Seg n
by A6, FUNCT_2:def 3;
A13:
now for k being Nat st 1 <= k & k <= len (Path_matrix (p,(A * Perm))) holds
P2p . k = (Path_matrix (p,(A * Perm))) . klet k be
Nat;
( 1 <= k & k <= len (Path_matrix (p,(A * Perm))) implies P2p . k = (Path_matrix (p,(A * Perm))) . k )assume that A14:
1
<= k
and A15:
k <= len (Path_matrix (p,(A * Perm)))
;
P2p . k = (Path_matrix (p,(A * Perm))) . kA16:
k in Seg n
by A11, A14, A15;
then A17:
p . k in Seg n
by A4, A5, FUNCT_1:3;
then reconsider pk =
p . k as
Element of
NAT ;
A18:
k = (perm ") . (perm . k)
by A2, A16, FUNCT_1:34;
[k,pk] in [:(Seg n),(Seg n):]
by A16, A17, ZFMISC_1:87;
then
[k,pk] in Indices A
by MATRIX_0:24;
then consider permk being
Nat such that A19:
perm . k = permk
and A20:
[permk,pk] in Indices A
and A21:
(A * Perm) * (
k,
pk)
= A * (
permk,
pk)
by Th37;
dom P2p = Seg n
by A2, A9, A8, RELAT_1:27;
then A22:
P2p . k = (Path_matrix (q,A)) . permk
by A16, A19, FUNCT_1:12;
Indices A = [:(Seg n),(Seg n):]
by MATRIX_0:24;
then A23:
permk in Seg n
by A20, ZFMISC_1:87;
then
q . permk in Seg n
by A7, A12, FUNCT_1:3;
then reconsider qpermk =
q . permk as
Element of
NAT ;
A24:
(Path_matrix (q,A)) . permk = A * (
permk,
qpermk)
by A8, A23, MATRIX_3:def 7;
A25:
dom (Path_matrix (p,(A * Perm))) = Seg n
by A11, FINSEQ_1:def 3;
q . permk = p . ((perm ") . (perm . k))
by A1, A7, A19, A23, FUNCT_1:12;
hence
P2p . k = (Path_matrix (p,(A * Perm))) . k
by A16, A21, A24, A22, A18, A25, MATRIX_3:def 7;
verum end;
n is Element of NAT
by ORDINAL1:def 12;
then
len P2p = n
by A10, FINSEQ_1:def 3;
hence
Path_matrix (p,(A * Perm)) = (Path_matrix (q,A)) * Perm
by A11, A13, FINSEQ_1:14; verum