let K be Field; for n being Element of NAT st n >= 1 holds
Per (0. (K,n,n)) = 0. K
let n be Element of NAT ; ( n >= 1 implies Per (0. (K,n,n)) = 0. K )
set B = In ((Permutations n),(Fin (Permutations n)));
set f = PPath_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:
for e being Element of the carrier of K st e is_a_unity_wrt the addF of K holds
G0 . {} = e
assume A3:
n >= 1
; Per (0. (K,n,n)) = 0. K
A4:
for x being object st x in dom (PPath_product (0. (K,n,n))) holds
(PPath_product (0. (K,n,n))) . x = ((Permutations n) --> (0. K)) . x
proof
let x be
object ;
( x in dom (PPath_product (0. (K,n,n))) implies (PPath_product (0. (K,n,n))) . x = ((Permutations n) --> (0. K)) . x )
assume
x in dom (PPath_product (0. (K,n,n)))
;
(PPath_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))))
proof
defpred S1[
Nat]
means the
multF of
K $$ (($1 + 1) |-> (0. K)) = 0. K;
let p be
Element of
Permutations n;
((Permutations n) --> (0. K)) . p = the multF of K $$ (Path_matrix (p,(0. (K,n,n))))
A5:
for
k being
Nat st
S1[
k] holds
S1[
k + 1]
A7:
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;
( i in dom (n |-> (0. K)) & j = p . i implies (n |-> (0. K)) . i = (0. (K,n,n)) * (i,j) )
assume that A8:
i in dom (n |-> (0. K))
and A9:
j = p . i
;
(n |-> (0. K)) . i = (0. (K,n,n)) * (i,j)
A10:
i in Seg n
by A8, FUNCOP_1:13;
then
j in Seg n
by A9, MATRIX_7:14;
then A11:
j in Seg (width (0. (K,n,n)))
by A3, MATRIX_0:23;
i in dom (0. (K,n,n))
by A10, MATRIX_7:13;
then
[i,j] in [:(dom (0. (K,n,n))),(Seg (width (0. (K,n,n)))):]
by A11, ZFMISC_1:def 2;
then A12:
[i,j] in Indices (0. (K,n,n))
by MATRIX_0:def 4;
(n |-> (0. K)) . i = 0. K
by A10, FUNCOP_1:7;
hence
(n |-> (0. K)) . i = (0. (K,n,n)) * (
i,
j)
by A12, MATRIX_3:1;
verum
end;
len (n |-> (0. K)) = n
by CARD_1:def 7;
then A13:
Path_matrix (
p,
(0. (K,n,n)))
= n |-> (0. K)
by A7, MATRIX_3:def 7;
A14:
(n -' 1) + 1
= n
by A3, XREAL_1:235;
1
|-> (0. K) = <*(0. K)*>
by FINSEQ_2:59;
then A15:
S1[
0 ]
by FINSOP_1:11;
for
k being
Nat holds
S1[
k]
from NAT_1:sch 2(A15, A5);
then
the
multF of
K $$ (Path_matrix (p,(0. (K,n,n)))) = 0. K
by A13, A14;
hence
((Permutations n) --> (0. K)) . p = the
multF of
K $$ (Path_matrix (p,(0. (K,n,n))))
by FUNCOP_1:7;
verum
end;
hence
(PPath_product (0. (K,n,n))) . x = ((Permutations n) --> (0. K)) . x
by Def1;
verum
end;
dom ((Permutations n) --> (0. K)) = Permutations n
by FUNCOP_1:13;
then
dom (PPath_product (0. (K,n,n))) = dom ((Permutations n) --> (0. K))
by FUNCT_2:def 1;
then A16:
PPath_product (0. (K,n,n)) = (Permutations n) --> (0. K)
by A4, FUNCT_1:2;
A17:
for x being Element of Permutations n holds G0 . {x} = (PPath_product (0. (K,n,n))) . x
A18:
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),((PPath_product (0. (K,n,n))) . x))
proof
let B9 be
Element of
Fin (Permutations n);
( 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),((PPath_product (0. (K,n,n))) . x)) )
assume that
B9 c= In (
(Permutations n),
(Fin (Permutations n)))
and
B9 <> {}
;
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),((PPath_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),
((PPath_product (0. (K,n,n))) . x))
verumproof
let x be
Element of
Permutations n;
( x in (In ((Permutations n),(Fin (Permutations n)))) \ B9 implies G0 . (B9 \/ {x}) = the addF of K . ((G0 . B9),((PPath_product (0. (K,n,n))) . x)) )
assume
x in (In ((Permutations n),(Fin (Permutations n)))) \ B9
;
G0 . (B9 \/ {x}) = the addF of K . ((G0 . B9),((PPath_product (0. (K,n,n))) . x))
A19:
(
G0 . (B9 \/ {.x.}) = 0. K &
G0 . B9 = 0. K )
by FUNCOP_1:7;
(
(PPath_product (0. (K,n,n))) . x = 0. K &
0. K is_a_unity_wrt the
addF of
K )
by A16, FUNCOP_1:7, FVSUM_1:6;
hence
G0 . (B9 \/ {x}) = the
addF of
K . (
(G0 . B9),
((PPath_product (0. (K,n,n))) . x))
by A19, BINOP_1:3;
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))) <> {} & G0 . (In ((Permutations n),(Fin (Permutations n)))) = 0. K )
by FUNCOP_1:7;
hence
Per (0. (K,n,n)) = 0. K
by A1, A17, A18, SETWISEO:def 3; verum