let n be Nat; :: thesis: for K being Field

for p being Element of Permutations n

for M being Matrix of n,K st ex i being Element of NAT st

( i in Seg n & ( for k being Element of NAT st k in Seg n holds

(Col (M,i)) . k = 0. K ) ) holds

(Path_product M) . p = 0. K

let K be Field; :: thesis: for p being Element of Permutations n

for M being Matrix of n,K st ex i being Element of NAT st

( i in Seg n & ( for k being Element of NAT st k in Seg n holds

(Col (M,i)) . k = 0. K ) ) holds

(Path_product M) . p = 0. K

let p be Element of Permutations n; :: thesis: for M being Matrix of n,K st ex i being Element of NAT st

( i in Seg n & ( for k being Element of NAT st k in Seg n holds

(Col (M,i)) . k = 0. K ) ) holds

(Path_product M) . p = 0. K

let M be Matrix of n,K; :: thesis: ( ex i being Element of NAT st

( i in Seg n & ( for k being Element of NAT st k in Seg n holds

(Col (M,i)) . k = 0. K ) ) implies (Path_product M) . p = 0. K )

A1: (Path_product M) . p = - (( the multF of K $$ (Path_matrix (p,M))),p) by MATRIX_3:def 8

.= - ((Product (Path_matrix (p,M))),p) by GROUP_4:def 2 ;

assume ex i being Element of NAT st

( i in Seg n & ( for k being Element of NAT st k in Seg n holds

(Col (M,i)) . k = 0. K ) ) ; :: thesis: (Path_product M) . p = 0. K

then consider l being Element of NAT such that

A2: l in Seg n and

A3: (Path_matrix (p,M)) . l = 0. K by Th49;

set k = l;

len (Path_matrix (p,M)) = n by MATRIX_3:def 7;

then l in dom (Path_matrix (p,M)) by A2, FINSEQ_1:def 3;

then A4: Product (Path_matrix (p,M)) = 0. K by A3, FVSUM_1:82;

for p being Element of Permutations n

for M being Matrix of n,K st ex i being Element of NAT st

( i in Seg n & ( for k being Element of NAT st k in Seg n holds

(Col (M,i)) . k = 0. K ) ) holds

(Path_product M) . p = 0. K

let K be Field; :: thesis: for p being Element of Permutations n

for M being Matrix of n,K st ex i being Element of NAT st

( i in Seg n & ( for k being Element of NAT st k in Seg n holds

(Col (M,i)) . k = 0. K ) ) holds

(Path_product M) . p = 0. K

let p be Element of Permutations n; :: thesis: for M being Matrix of n,K st ex i being Element of NAT st

( i in Seg n & ( for k being Element of NAT st k in Seg n holds

(Col (M,i)) . k = 0. K ) ) holds

(Path_product M) . p = 0. K

let M be Matrix of n,K; :: thesis: ( ex i being Element of NAT st

( i in Seg n & ( for k being Element of NAT st k in Seg n holds

(Col (M,i)) . k = 0. K ) ) implies (Path_product M) . p = 0. K )

A1: (Path_product M) . p = - (( the multF of K $$ (Path_matrix (p,M))),p) by MATRIX_3:def 8

.= - ((Product (Path_matrix (p,M))),p) by GROUP_4:def 2 ;

assume ex i being Element of NAT st

( i in Seg n & ( for k being Element of NAT st k in Seg n holds

(Col (M,i)) . k = 0. K ) ) ; :: thesis: (Path_product M) . p = 0. K

then consider l being Element of NAT such that

A2: l in Seg n and

A3: (Path_matrix (p,M)) . l = 0. K by Th49;

set k = l;

len (Path_matrix (p,M)) = n by MATRIX_3:def 7;

then l in dom (Path_matrix (p,M)) by A2, FINSEQ_1:def 3;

then A4: Product (Path_matrix (p,M)) = 0. K by A3, FVSUM_1:82;

per cases
( p is even or p is odd )
;

end;

suppose
p is odd
; :: thesis: (Path_product M) . p = 0. K

then - ((Product (Path_matrix (p,M))),p) =
- (Product (Path_matrix (p,M)))
by MATRIX_1:def 16

.= 0. K by A4, RLVECT_1:12 ;

hence (Path_product M) . p = 0. K by A1; :: thesis: verum

end;.= 0. K by A4, RLVECT_1:12 ;

hence (Path_product M) . p = 0. K by A1; :: thesis: verum