let K be Ring; :: thesis: for n being Nat st n >= 1 holds
Det (0. (K,n,n)) = 0. K
let n be Nat; :: thesis: ( n >= 1 implies Det (0. (K,n,n)) = 0. K )
set B = In ((Permutations n),(Fin (Permutations n)));
set f = Path_product (0. (K,n,n));
set F = the addF of K;
set Y = the carrier of K;
set X = Permutations n;
reconsider G0 = (Fin (Permutations n)) --> (0. K) as Function of (Fin (Permutations n)), the carrier of K ;
A1: G0 . (In ((Permutations n),(Fin (Permutations n)))) = 0. K by FUNCOP_1:7;
A2: for e being Element of the carrier of K st e is_a_unity_wrt the addF of K holds
G0 . {} = e

proof

let e be Element of the carrier of K; :: thesis: ( e is_a_unity_wrt the addF of K implies G0 . {} = e )
0. K is_a_unity_wrt the addF of K by FVSUM_1:6;
then A3: the addF of K . ((0. K),e) = e by BINOP_1:3;
assume e is_a_unity_wrt the addF of K ; :: thesis: G0 . {} = e
then the addF of K . ((0. K),e) = 0. K by BINOP_1:3;
hence G0 . {} = e by A3, FINSUB_1:7, FUNCOP_1:7; :: thesis: verum

end;

assume A4: n >= 1 ; :: thesis: Det (0. (K,n,n)) = 0. K
A5: for x being object st x in dom (Path_product (0. (K,n,n))) holds
(Path_product (0. (K,n,n))) . x = ((Permutations n) --> (0. K)) . x

proof

let x be object ; :: thesis: ( x in dom (Path_product (0. (K,n,n))) implies (Path_product (0. (K,n,n))) . x = ((Permutations n) --> (0. K)) . x )
assume x in dom (Path_product (0. (K,n,n))) ; :: thesis: (Path_product (0. (K,n,n))) . x = ((Permutations n) --> (0. K)) . x
for p being Element of Permutations n holds ((Permutations n) --> (0. K)) . p = - (( the multF of K $$ (Path_matrix (p,(0. (K,n,n))))),p)

proof

defpred S₁[ Nat] means the multF of K $$ (($1 + 1) |-> (0. K)) = 0. K;
let p be Element of Permutations n; :: thesis: ((Permutations n) --> (0. K)) . p = - (( the multF of K $$ (Path_matrix (p,(0. (K,n,n))))),p)
A6: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
A7: ((k + 1) + 1) |-> (0. K) = ((k + 1) |-> (0. K)) ^ <*(0. K)*> by FINSEQ_2:60;
assume S₁[k] ; :: thesis: S₁[k + 1]
then the multF of K $$ (((k + 1) + 1) |-> (0. K)) = (0. K) * (0. K) by A7, FINSOP_1:4
.= 0. K ;
hence S₁[k + 1] ; :: thesis: verum

end;

1 |-> (0. K) = <*(0. K)*> by FINSEQ_2:59;
then A8: S₁[ 0 ] by FINSOP_1:11;
A9: for k being Nat holds S₁[k] from NAT_1:sch 2(A8, A6);

A10: now :: thesis: ( ( p is even & - ((0. K),p) = 0. K ) or ( not p is even & - ((0. K),p) = 0. K ) )

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

case p is even ; :: thesis: - ((0. K),p) = 0. K

hence - ((0. K),p) = 0. K by MATRIX_1:def 16; :: thesis: verum

end;

case not p is even ; :: thesis: - ((0. K),p) = 0. K

then - ((0. K),p) = - (0. K) by MATRIX_1:def 16
.= 0. K by RLVECT_1:12 ;
hence - ((0. K),p) = 0. K ; :: thesis: verum

end;

end;

end;

A11: for i, j being Nat st i in dom (n |-> (0. K)) & j = p . i holds
(n |-> (0. K)) . i = (0. (K,n,n)) * (i,j)

proof

let i, j be Nat; :: thesis: ( i in dom (n |-> (0. K)) & j = p . i implies (n |-> (0. K)) . i = (0. (K,n,n)) * (i,j) )
assume that
A12: i in dom (n |-> (0. K)) and
A13: j = p . i ; :: thesis: (n |-> (0. K)) . i = (0. (K,n,n)) * (i,j)
A14: i in Seg n by A12, FUNCOP_1:13;
then j in Seg n by A13, Th14;
then A15: j in Seg (width (0. (K,n,n))) by A4, MATRIX_0:23;
i in dom (0. (K,n,n)) by A14, Th13;
then A16: [i,j] in Indices (0. (K,n,n)) by A15, ZFMISC_1:def 2;
(n |-> (0. K)) . i = 0. K by A14, FUNCOP_1:7;
hence (n |-> (0. K)) . i = (0. (K,n,n)) * (i,j) by A16, MATRIX_3:1; :: thesis: verum

end;

len (n |-> (0. K)) = n by CARD_1:def 7;
then A17: Path_matrix (p,(0. (K,n,n))) = n |-> (0. K) by A11, MATRIX_3:def 7;
n -' 1 = n - 1 by A4, XREAL_1:233;
then A18: (n -' 1) + 1 = n ;
((Permutations n) --> (0. K)) . p = 0. K by FUNCOP_1:7;
hence ((Permutations n) --> (0. K)) . p = - (( the multF of K $$ (Path_matrix (p,(0. (K,n,n))))),p) by A17, A9, A18, A10; :: thesis: verum

end;

hence (Path_product (0. (K,n,n))) . x = ((Permutations n) --> (0. K)) . x by MATRIX_3:def 8; :: thesis: verum

end;

dom ((Permutations n) --> (0. K)) = Permutations n by FUNCOP_1:13;
then dom (Path_product (0. (K,n,n))) = dom ((Permutations n) --> (0. K)) by FUNCT_2:def 1;
then A19: Path_product (0. (K,n,n)) = (Permutations n) --> (0. K) by A5, FUNCT_1:2;
A20: for x being Element of Permutations n holds G0 . {x} = (Path_product (0. (K,n,n))) . x

proof

let x be Element of Permutations n; :: thesis: G0 . {x} = (Path_product (0. (K,n,n))) . x
G0 . {.x.} = 0. K by FUNCOP_1:7;
hence G0 . {x} = (Path_product (0. (K,n,n))) . x by A19, FUNCOP_1:7; :: thesis: verum

end;

A21: for B9 being Element of Fin (Permutations n) st B9 c= In ((Permutations n),(Fin (Permutations n))) & B9 <> {} holds
for x being Element of Permutations n st x in (In ((Permutations n),(Fin (Permutations n)))) \ B9 holds
G0 . (B9 \/ {x}) = the addF of K . ((G0 . B9),((Path_product (0. (K,n,n))) . x))

proof

let B9 be Element of Fin (Permutations n); :: thesis: ( B9 c= In ((Permutations n),(Fin (Permutations n))) & B9 <> {} implies for x being Element of Permutations n st x in (In ((Permutations n),(Fin (Permutations n)))) \ B9 holds
G0 . (B9 \/ {x}) = the addF of K . ((G0 . B9),((Path_product (0. (K,n,n))) . x)) )
assume that
B9 c= In ((Permutations n),(Fin (Permutations n))) and
B9 <> {} ; :: thesis: for x being Element of Permutations n st x in (In ((Permutations n),(Fin (Permutations n)))) \ B9 holds
G0 . (B9 \/ {x}) = the addF of K . ((G0 . B9),((Path_product (0. (K,n,n))) . x))
thus for x being Element of Permutations n st x in (In ((Permutations n),(Fin (Permutations n)))) \ B9 holds
G0 . (B9 \/ {x}) = the addF of K . ((G0 . B9),((Path_product (0. (K,n,n))) . x)) :: thesis: verum

proof

let x be Element of Permutations n; :: thesis: ( x in (In ((Permutations n),(Fin (Permutations n)))) \ B9 implies G0 . (B9 \/ {x}) = the addF of K . ((G0 . B9),((Path_product (0. (K,n,n))) . x)) )
assume x in (In ((Permutations n),(Fin (Permutations n)))) \ B9 ; :: thesis: G0 . (B9 \/ {x}) = the addF of K . ((G0 . B9),((Path_product (0. (K,n,n))) . x))
A22: ( G0 . (B9 \/ {.x.}) = 0. K & G0 . B9 = 0. K ) by FUNCOP_1:7;
( (Path_product (0. (K,n,n))) . x = 0. K & 0. K is_a_unity_wrt the addF of K ) by A19, FUNCOP_1:7, FVSUM_1:6;
hence G0 . (B9 \/ {x}) = the addF of K . ((G0 . B9),((Path_product (0. (K,n,n))) . x)) by A22, BINOP_1:3; :: thesis: verum

end;

end;

Permutations n in Fin (Permutations n) by FINSUB_1:def 5;
then In ((Permutations n),(Fin (Permutations n))) = Permutations n by SUBSET_1:def 8;
then ( In ((Permutations n),(Fin (Permutations n))) <> {} or the addF of K is having_a_unity ) ;
then the addF of K $$ ((In ((Permutations n),(Fin (Permutations n)))),(Path_product (0. (K,n,n)))) = 0. K by A1, A2, A20, A21, SETWISEO:def 3;
hence Det (0. (K,n,n)) = 0. K by MATRIX_3:def 9; :: thesis: verum