let n be Nat; :: thesis: for K being commutative Ring st not K is degenerated & K is well-unital & K is domRing-like holds
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 commutative Ring; :: thesis: ( not K is degenerated & K is well-unital & K is domRing-like implies 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) )
assume A0: ( not K is degenerated & K is well-unital & K is domRing-like ) ; :: 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 A0, 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 A0, Th26
.= (sgn (perm2,K)) * ((sgn (p2,K)) * ( the multF of K $$ (Path_matrix (q2,M)))) by GROUP_1:def 3
.= (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, A0
.= (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