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,K
for perm being Element of Permutations n
for Perm being Permutation of (Seg n) st perm = Perm holds
Det (M * Perm) = - ((Det M),perm)
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,K
for perm being Element of Permutations n
for Perm being Permutation of (Seg n) st perm = Perm holds
Det (M * Perm) = - ((Det M),perm) )
assume A0: ( not K is degenerated & K is well-unital & K is domRing-like ) ; :: thesis: for M being Matrix of n,K
for perm being Element of Permutations n
for Perm being Permutation of (Seg n) st perm = Perm holds
Det (M * Perm) = - ((Det M),perm)
let M be Matrix of n,K; :: thesis: for perm being Element of Permutations n
for Perm being Permutation of (Seg n) st perm = Perm holds
Det (M * Perm) = - ((Det M),perm)
let perm be Element of Permutations n; :: thesis: for Perm being Permutation of (Seg n) st perm = Perm holds
Det (M * Perm) = - ((Det M),perm)
let Perm be Permutation of (Seg n); :: thesis: ( perm = Perm implies Det (M * Perm) = - ((Det M),perm) )
assume A1: Perm = perm ; :: thesis: Det (M * Perm) = - ((Det M),perm)
per cases ( n < 2 or n >= 2 ) ;
suppose A2: n < 2 ; :: thesis: Det (M * Perm) = - ((Det M),perm)
then perm = idseq n by Lm3;
then A3: M * perm = M by Th39;
perm is even by A2, Lm3;
hence Det (M * Perm) = - ((Det M),perm) by A1, A3, MATRIX_1:def 16; :: thesis: verum
end;
suppose n >= 2 ; :: thesis: Det (M * Perm) = - ((Det M),perm)
then reconsider n2 = n - 2 as Nat by NAT_1:21;
reconsider M9 = M as Matrix of n2 + 2,K ;
reconsider Perm2 = Perm as Permutation of (Seg (n2 + 2)) ;
reconsider perm2 = perm as Element of Permutations (n2 + 2) ;
Det (M9 * Perm2) = (sgn (perm2,K)) * (Det M9) by A0, A1, Th45;
hence Det (M * Perm) = - ((Det M),perm) by A0, Th26; :: thesis: verum
end;
end;