let n be Nat; for K being commutative Ring st not K is degenerated & K is well-unital & K is domRing-like holds
for i, j being Nat st i in Seg n & j in Seg n & i < j holds
for M being Matrix of n,K st Line (M,i) = Line (M,j) holds
for p, q, tr being Element of Permutations n st q = p * tr & tr is being_transposition & tr . i = j holds
(Path_product M) . q = - ((Path_product M) . p)
let K be commutative Ring; ( not K is degenerated & K is well-unital & K is domRing-like implies for i, j being Nat st i in Seg n & j in Seg n & i < j holds
for M being Matrix of n,K st Line (M,i) = Line (M,j) holds
for p, q, tr being Element of Permutations n st q = p * tr & tr is being_transposition & tr . i = j holds
(Path_product M) . q = - ((Path_product M) . p) )
assume A0:
( not K is degenerated & K is well-unital & K is domRing-like )
; for i, j being Nat st i in Seg n & j in Seg n & i < j holds
for M being Matrix of n,K st Line (M,i) = Line (M,j) holds
for p, q, tr being Element of Permutations n st q = p * tr & tr is being_transposition & tr . i = j holds
(Path_product M) . q = - ((Path_product M) . p)
let i, j be Nat; ( i in Seg n & j in Seg n & i < j implies for M being Matrix of n,K st Line (M,i) = Line (M,j) holds
for p, q, tr being Element of Permutations n st q = p * tr & tr is being_transposition & tr . i = j holds
(Path_product M) . q = - ((Path_product M) . p) )
assume that
A1:
i in Seg n
and
A2:
j in Seg n
and
A3:
i < j
; for M being Matrix of n,K st Line (M,i) = Line (M,j) holds
for p, q, tr being Element of Permutations n st q = p * tr & tr is being_transposition & tr . i = j holds
(Path_product M) . q = - ((Path_product M) . p)
{i,j} in 2Set (Seg n)
by A1, A2, A3, Th1;
then reconsider n2 = n - 2 as Nat by Th2, NAT_1:21, NAT_1:23;
let M be Matrix of n,K; ( Line (M,i) = Line (M,j) implies for p, q, tr being Element of Permutations n st q = p * tr & tr is being_transposition & tr . i = j holds
(Path_product M) . q = - ((Path_product M) . p) )
assume A4:
Line (M,i) = Line (M,j)
; for p, q, tr being Element of Permutations n st q = p * tr & tr is being_transposition & tr . i = j holds
(Path_product M) . q = - ((Path_product M) . p)
reconsider M9 = M as Matrix of n2 + 2,K ;
let p, q, tr be Element of Permutations n; ( q = p * tr & tr is being_transposition & tr . i = j implies (Path_product M) . q = - ((Path_product M) . p) )
assume that
A5:
q = p * tr
and
A6:
tr is being_transposition
and
A7:
tr . i = j
; (Path_product M) . q = - ((Path_product M) . p)
reconsider TR = tr as Permutation of (Seg (n2 + 2)) by MATRIX_1:def 12;
set Mt = M9 * TR;
A8:
for k being Nat st 1 <= k & k <= len M9 holds
M9 . k = (M9 * TR) . k
proof
let k be
Nat;
( 1 <= k & k <= len M9 implies M9 . k = (M9 * TR) . k )
assume that A9:
1
<= k
and A10:
k <= len M9
;
M9 . k = (M9 * TR) . k
A11:
k in Seg (len M9)
by A9, A10;
A12:
Line (
M,
j)
= M . j
by A2, MATRIX_0:52;
A13:
dom TR = Seg n
by FUNCT_2:52;
A14:
Line (
M,
i)
= M . i
by A1, MATRIX_0:52;
A15:
len M9 = n
by MATRIX_0:def 2;
then A16:
Line (
(M9 * TR),
k)
= M . (tr . k)
by A11, Th38;
per cases
( k = i or k = j or ( k <> i & k <> j ) )
;
suppose A17:
k = j
;
M9 . k = (M9 * TR) . kthen A18:
M . k = M . i
by A2, A4, A14, MATRIX_0:52;
Line (
(M9 * TR),
k)
= M . i
by A3, A6, A7, A16, A17, Th8;
hence
M9 . k = (M9 * TR) . k
by A2, A17, A18, MATRIX_0:52;
verum end; suppose
(
k <> i &
k <> j )
;
M9 . k = (M9 * TR) . kthen
Line (
(M9 * TR),
k)
= M . k
by A3, A6, A7, A11, A15, A13, A16, Th8;
hence
M9 . k = (M9 * TR) . k
by A11, A15, MATRIX_0:52;
verum end;
end;
len (M9 * TR) = len M9
by Def4;
then A19:
M9 * TR = M
by A8;
reconsider Tr = tr, p2 = p as Element of Permutations (n2 + 2) ;
A20:
sgn (Tr,K) = - (1_ K)
by A6, Th14;
tr = tr "
by A6, Th20;
hence (Path_product M) . q =
(- (1_ K)) * ((Path_product M9) . p2)
by A0, A5, A19, A20, Th43
.=
- ((1_ K) * ((Path_product M9) . p2))
by VECTSP_1:9
.=
- ((Path_product M) . p)
;
verum