let n be Nat; :: thesis: for K being Field
for M being Matrix of n + 2,K
for perm2 being Element of Permutations (n + 2)
for Perm2 being Permutation of (Seg (n + 2)) st perm2 = Perm2 holds
for p2, q2 being Element of Permutations (n + 2) st q2 = p2 * (Perm2 " ) holds
(Path_product M) . q2 = (sgn perm2,K) * ((Path_product (M * Perm2)) . p2)
let K be Field; :: thesis: for M being Matrix of n + 2,K
for perm2 being Element of Permutations (n + 2)
for Perm2 being Permutation of (Seg (n + 2)) st perm2 = Perm2 holds
for p2, q2 being Element of Permutations (n + 2) st q2 = p2 * (Perm2 " ) holds
(Path_product M) . q2 = (sgn perm2,K) * ((Path_product (M * Perm2)) . p2)
let M be Matrix of n + 2,K; :: thesis: for perm2 being Element of Permutations (n + 2)
for Perm2 being Permutation of (Seg (n + 2)) st perm2 = Perm2 holds
for p2, q2 being Element of Permutations (n + 2) st q2 = p2 * (Perm2 " ) holds
(Path_product M) . q2 = (sgn perm2,K) * ((Path_product (M * Perm2)) . p2)
let perm2 be Element of Permutations (n + 2); :: thesis: for Perm2 being Permutation of (Seg (n + 2)) st perm2 = Perm2 holds
for p2, q2 being Element of Permutations (n + 2) st q2 = p2 * (Perm2 " ) holds
(Path_product M) . q2 = (sgn perm2,K) * ((Path_product (M * Perm2)) . p2)
let Perm2 be Permutation of (Seg (n + 2)); :: thesis: ( perm2 = Perm2 implies for p2, q2 being Element of Permutations (n + 2) st q2 = p2 * (Perm2 " ) holds
(Path_product M) . q2 = (sgn perm2,K) * ((Path_product (M * Perm2)) . p2) )
assume A1: perm2 = Perm2 ; :: thesis: for p2, q2 being Element of Permutations (n + 2) st q2 = p2 * (Perm2 " ) holds
(Path_product M) . q2 = (sgn perm2,K) * ((Path_product (M * Perm2)) . p2)
set P = Permutations (n + 2);
set mm = the multF of K;
let p2, q2 be Element of Permutations (n + 2); :: thesis: ( q2 = p2 * (Perm2 " ) implies (Path_product M) . q2 = (sgn perm2,K) * ((Path_product (M * Perm2)) . p2) )
assume A2: q2 = p2 * (Perm2 " ) ; :: thesis: (Path_product M) . q2 = (sgn perm2,K) * ((Path_product (M * Perm2)) . p2)
reconsider perm29 = perm2 " as Element of Permutations (n + 2) by MATRIX_7:18;
set PM = the multF of K $$ (Path_matrix q2,M);
set PMp = the multF of K $$ (Path_matrix p2,(M * Perm2));
sgn q2,K = (sgn p2,K) * (sgn perm29,K) by A1, A2, Th24
.= (sgn p2,K) * (sgn perm2,K) by Th42 ;
then - (the multF of K $$ (Path_matrix q2,M)),q2 = ((sgn perm2,K) * (sgn p2,K)) * (the multF of K $$ (Path_matrix q2,M)) by Th26
.= (sgn perm2,K) * ((sgn p2,K) * (the multF of K $$ (Path_matrix q2,M))) by GROUP_1:def 4
.= (sgn perm2,K) * ((sgn p2,K) * (the multF of K $$ (Path_matrix p2,(M * Perm2)))) by A2, Th41
.= (sgn perm2,K) * (- (the multF of K $$ (Path_matrix p2,(M * Perm2))),p2) by Th26
.= (sgn perm2,K) * ((Path_product (M * Perm2)) . p2) by MATRIX_3:def 8 ;
hence (Path_product M) . q2 = (sgn perm2,K) * ((Path_product (M * Perm2)) . p2) by MATRIX_3:def 8; :: thesis: verum