let n be Nat; 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; ( 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 )
; 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; 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); 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)); ( 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
; 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); ( q2 = p2 * (Perm2 ") implies (Path_product M) . q2 = (sgn (perm2,K)) * ((Path_product (M * Perm2)) . p2) )
assume A2:
q2 = p2 * (Perm2 ")
; (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; verum