let K be Field; for n being Element of NAT st n >= 1 holds
Det (1. K,n) = 1_ K
let n be Element of NAT ; ( n >= 1 implies Det (1. K,n) = 1_ K )
assume A1:
n >= 1
; Det (1. K,n) = 1_ K
deffunc H1( set ) -> Element of the carrier of K = IFEQ (idseq n),$1,(1_ K),(0. K);
set X = Permutations n;
set Y = the carrier of K;
A2:
for x being set st x in Permutations n holds
H1(x) in the carrier of K
;
ex f2 being Function of (Permutations n),the carrier of K st
for x being set st x in Permutations n holds
f2 . x = H1(x)
from FUNCT_2:sch 2(A2);
then consider f2 being Function of (Permutations n),the carrier of K such that
A3:
for x being set st x in Permutations n holds
f2 . x = H1(x)
;
A4:
id (Seg n) is even
by MATRIX_2:29;
A5:
for x being set st x in dom (Path_product (1. K,n)) holds
(Path_product (1. K,n)) . x = f2 . x
proof
let x be
set ;
( x in dom (Path_product (1. K,n)) implies (Path_product (1. K,n)) . x = f2 . x )
assume
x in dom (Path_product (1. K,n))
;
(Path_product (1. K,n)) . x = f2 . x
for
p being
Element of
Permutations n holds
f2 . p = - (the multF of K $$ (Path_matrix p,(1. K,n))),
p
proof
defpred S1[
Element of
NAT ]
means the
multF of
K $$ (($1 + 1) |-> (1_ K)) = 1_ K;
let p be
Element of
Permutations n;
f2 . p = - (the multF of K $$ (Path_matrix p,(1. K,n))),p
A6:
for
k being
Element of
NAT st
S1[
k] holds
S1[
k + 1]
n -' 1
= n - 1
by A1, XREAL_1:235;
then A9:
(n -' 1) + 1
= n
;
1
|-> (1_ K) = <*(1_ K)*>
by FINSEQ_2:73;
then A10:
S1[
0 ]
by FINSOP_1:12;
for
k being
Element of
NAT holds
S1[
k]
from NAT_1:sch 1(A10, A6);
then A11:
(
len (n |-> (1_ K)) = n & the
multF of
K $$ (n |-> (1_ K)) = 1_ K )
by A9, FINSEQ_1:def 18;
now per cases
( p = idseq n or p <> idseq n )
;
case A12:
p = idseq n
;
f2 . p = - (the multF of K $$ (Path_matrix p,(1. K,n))),pA13:
for
i,
j being
Nat st
i in dom (n |-> (1_ K)) &
j = p . i holds
(n |-> (1_ K)) . i = (1. K,n) * i,
j
proof
A14:
Indices (1. K,n) = [:(Seg n),(Seg n):]
by A1, MATRIX_1:24;
let i,
j be
Nat;
( i in dom (n |-> (1_ K)) & j = p . i implies (n |-> (1_ K)) . i = (1. K,n) * i,j )
assume that A15:
i in dom (n |-> (1_ K))
and A16:
j = p . i
;
(n |-> (1_ K)) . i = (1. K,n) * i,j
A17:
i in Seg n
by A15, FUNCOP_1:19;
then
j in Seg n
by A16, Th14;
then A18:
[i,j] in Indices (1. K,n)
by A17, A14, ZFMISC_1:def 2;
(
(n |-> (1_ K)) . i = 1_ K &
p . i = i )
by A12, A17, FUNCOP_1:13, FUNCT_1:34;
hence
(n |-> (1_ K)) . i = (1. K,n) * i,
j
by A16, A18, MATRIX_1:def 12;
verum
end;
len (Permutations n) = n
by MATRIX_2:20;
then A19:
- (the multF of K $$ (Path_matrix p,(1. K,n))),
p = the
multF of
K $$ (Path_matrix p,(1. K,n))
by A4, A12, MATRIX_2:def 16;
f2 . p =
H1(
p)
by A3
.=
1_ K
by A12, FUNCOP_1:def 8
;
hence
f2 . p = - (the multF of K $$ (Path_matrix p,(1. K,n))),
p
by A11, A19, A13, MATRIX_3:def 7;
verum end; case A20:
p <> idseq n
;
f2 . p = - (the multF of K $$ (Path_matrix p,(1. K,n))),preconsider A =
NAT as non
empty set ;
defpred S2[
Element of
NAT ]
means ( $1
< n implies ex
p3 being
FinSequence of
K st
(
len p3 = $1
+ 1 &
p3 . 1
= (Path_matrix p,(1. K,n)) . 1 & ( for
n3 being
Element of
NAT st
0 <> n3 &
n3 < $1
+ 1 &
n3 < n holds
p3 . (n3 + 1) = the
multF of
K . (p3 . n3),
((Path_matrix p,(1. K,n)) . (n3 + 1)) ) ) );
A21:
rng (Path_matrix p,(1. K,n)) c= the
carrier of
K
by FINSEQ_1:def 4;
A22:
len (Path_matrix p,(1. K,n)) = n
by MATRIX_3:def 7;
then
1
in Seg (len (Path_matrix p,(1. K,n)))
by A1;
then
1
in dom (Path_matrix p,(1. K,n))
by FINSEQ_1:def 3;
then
(Path_matrix p,(1. K,n)) . 1
in rng (Path_matrix p,(1. K,n))
by FUNCT_1:def 5;
then reconsider d =
(Path_matrix p,(1. K,n)) . 1 as
Element of
K by A21;
reconsider q3 =
<*d*> as
FinSequence of
K ;
A23:
for
n3 being
Element of
NAT st
0 <> n3 &
n3 < 0 + 1 &
n3 < n holds
q3 . (n3 + 1) = the
multF of
K . (q3 . n3),
((Path_matrix p,(1. K,n)) . (n3 + 1))
by NAT_1:13;
A24:
dom p = Seg (len (Permutations n))
by FUNCT_2:67;
then A25:
dom p = Seg n
by MATRIX_2:20;
then
dom p = dom (idseq n)
by RELAT_1:71;
then consider i0 being
set such that A26:
i0 in dom p
and A27:
p . i0 <> (idseq n) . i0
by A20, FUNCT_1:9;
reconsider i0 =
i0 as
Element of
NAT by A24, A26;
A28:
p . i0 <> i0
by A25, A26, A27, FUNCT_1:35;
A29:
for
k being
Element of
NAT st
S2[
k] holds
S2[
k + 1]
proof
let k be
Element of
NAT ;
( S2[k] implies S2[k + 1] )
assume A30:
S2[
k]
;
S2[k + 1]
now per cases
( k + 1 < n or k + 1 >= n )
;
case A31:
k + 1
< n
;
S2[k + 1]then consider p3 being
FinSequence of
K such that A32:
len p3 = k + 1
and A33:
p3 . 1
= (Path_matrix p,(1. K,n)) . 1
and A34:
for
n3 being
Element of
NAT st
0 <> n3 &
n3 < k + 1 &
n3 < n holds
p3 . (n3 + 1) = the
multF of
K . (p3 . n3),
((Path_matrix p,(1. K,n)) . (n3 + 1))
by A30, NAT_1:12;
defpred S3[
set ,
set ]
means ( ( $1
in Seg (k + 1) implies $2
= p3 . $1 ) & ( not $1
in Seg (k + 1) implies $2
= 0. K ) );
A35:
for
x being
set st
x in NAT holds
ex
y being
set st
(
y in the
carrier of
K &
S3[
x,
y] )
ex
f6 being
Function of
NAT ,the
carrier of
K st
for
x being
set st
x in NAT holds
S3[
x,
f6 . x]
from FUNCT_2:sch 1(A35);
then consider f6 being
Function of
NAT ,the
carrier of
K such that A38:
for
x being
set st
x in NAT holds
S3[
x,
f6 . x]
;
( 1
<= (k + 1) + 1 &
(k + 1) + 1
<= n )
by A31, NAT_1:12, NAT_1:13;
then
(k + 1) + 1
in Seg (len (Path_matrix p,(1. K,n)))
by A22;
then
(k + 1) + 1
in dom (Path_matrix p,(1. K,n))
by FINSEQ_1:def 3;
then
(
rng (Path_matrix p,(1. K,n)) c= the
carrier of
K &
(Path_matrix p,(1. K,n)) . ((k + 1) + 1) in rng (Path_matrix p,(1. K,n)) )
by FINSEQ_1:def 4, FUNCT_1:def 5;
then
[(f6 . (k + 1)),((Path_matrix p,(1. K,n)) . ((k + 1) + 1))] in [:the carrier of K,the carrier of K:]
by ZFMISC_1:def 2;
then reconsider e = the
multF of
K . (f6 . (k + 1)),
((Path_matrix p,(1. K,n)) . ((k + 1) + 1)) as
Element of
K by FUNCT_2:7;
reconsider q3 =
p3 ^ <*e*> as
FinSequence of
K ;
A39:
len q3 =
(len p3) + (len <*e*>)
by FINSEQ_1:35
.=
(k + 1) + 1
by A32, FINSEQ_1:57
;
A40:
for
n3 being
Element of
NAT st
0 <> n3 &
n3 < (k + 1) + 1 &
n3 < n holds
q3 . (n3 + 1) = the
multF of
K . (q3 . n3),
((Path_matrix p,(1. K,n)) . (n3 + 1))
proof
let n3 be
Element of
NAT ;
( 0 <> n3 & n3 < (k + 1) + 1 & n3 < n implies q3 . (n3 + 1) = the multF of K . (q3 . n3),((Path_matrix p,(1. K,n)) . (n3 + 1)) )
assume that A41:
0 <> n3
and A42:
n3 < (k + 1) + 1
and A43:
n3 < n
;
q3 . (n3 + 1) = the multF of K . (q3 . n3),((Path_matrix p,(1. K,n)) . (n3 + 1))
now per cases
( n3 < k + 1 or n3 >= k + 1 )
;
case A44:
n3 < k + 1
;
q3 . (n3 + 1) = the multF of K . (q3 . n3),((Path_matrix p,(1. K,n)) . (n3 + 1))then
( 1
<= n3 + 1 &
n3 + 1
<= k + 1 )
by NAT_1:12, NAT_1:13;
then
n3 + 1
in Seg (len p3)
by A32;
then
n3 + 1
in dom p3
by FINSEQ_1:def 3;
then A45:
p3 . (n3 + 1) = q3 . (n3 + 1)
by FINSEQ_1:def 7;
0 + 1
<= n3
by A41, NAT_1:13;
then
n3 in Seg (len p3)
by A32, A44;
then A46:
n3 in dom p3
by FINSEQ_1:def 3;
p3 . (n3 + 1) = the
multF of
K . (p3 . n3),
((Path_matrix p,(1. K,n)) . (n3 + 1))
by A34, A41, A43, A44;
hence
q3 . (n3 + 1) = the
multF of
K . (q3 . n3),
((Path_matrix p,(1. K,n)) . (n3 + 1))
by A45, A46, FINSEQ_1:def 7;
verum end; case A47:
n3 >= k + 1
;
q3 . (n3 + 1) = the multF of K . (q3 . n3),((Path_matrix p,(1. K,n)) . (n3 + 1))A48:
n3 + 1
<= (k + 1) + 1
by A42, NAT_1:13;
A49:
n3 + 1
> k + 1
by A47, NAT_1:13;
then
n3 + 1
>= (k + 1) + 1
by NAT_1:13;
then A50:
n3 + 1
= (k + 1) + 1
by A48, XXREAL_0:1;
1
<= k + 1
by NAT_1:12;
then A51:
k + 1
in Seg (k + 1)
;
then
k + 1
in dom p3
by A32, FINSEQ_1:def 3;
then A52:
q3 . (k + 1) = p3 . (k + 1)
by FINSEQ_1:def 7;
q3 . (n3 + 1) =
<*e*> . ((n3 + 1) - (k + 1))
by A32, A39, A49, A48, FINSEQ_1:37
.=
e
by A50, FINSEQ_1:def 8
;
hence
q3 . (n3 + 1) = the
multF of
K . (q3 . n3),
((Path_matrix p,(1. K,n)) . (n3 + 1))
by A38, A50, A51, A52;
verum end;
hence
q3 . (n3 + 1) = the
multF of
K . (q3 . n3),
((Path_matrix p,(1. K,n)) . (n3 + 1))
;
verum
end;
1
<= k + 1
by NAT_1:12;
then
1
in Seg (len p3)
by A32;
then
1
in dom p3
by FINSEQ_1:def 3;
then
q3 . 1
= (Path_matrix p,(1. K,n)) . 1
by A33, FINSEQ_1:def 7;
hence
S2[
k + 1]
by A39, A40;
verum end;
hence
S2[
k + 1]
;
verum
end;
n < n + 1
by NAT_1:13;
then A53:
n - 1
< (n + 1) - 1
by XREAL_1:16;
A54:
f2 . p =
H1(
p)
by A3
.=
0. K
by A20, FUNCOP_1:def 8
;
A55:
n - 1
= n -' 1
by A1, XREAL_1:235;
(
len q3 = 1 &
q3 . 1
= (Path_matrix p,(1. K,n)) . 1 )
by FINSEQ_1:57;
then A56:
S2[
0 ]
by A23;
for
k being
Element of
NAT holds
S2[
k]
from NAT_1:sch 1(A56, A29);
then consider p3 being
FinSequence of
K such that A57:
len p3 = (n -' 1) + 1
and A58:
p3 . 1
= (Path_matrix p,(1. K,n)) . 1
and A59:
for
n3 being
Element of
NAT st
0 <> n3 &
n3 < (n -' 1) + 1 &
n3 < n holds
p3 . (n3 + 1) = the
multF of
K . (p3 . n3),
((Path_matrix p,(1. K,n)) . (n3 + 1))
by A55, A53;
defpred S3[
set ,
set ]
means ( ( $1
in Seg n implies $2
= p3 . $1 ) & ( not $1
in Seg n implies $2
= 0. K ) );
A60:
for
x3 being
Element of
A ex
y3 being
Element of
K st
S3[
x3,
y3]
ex
f4 being
Function of
A,the
carrier of
K st
for
x2 being
Element of
A holds
S3[
x2,
f4 . x2]
from FUNCT_2:sch 3(A60);
then consider f4 being
Function of
NAT ,the
carrier of
K such that A62:
for
x4 being
Element of
NAT holds
( (
x4 in Seg n implies
f4 . x4 = p3 . x4 ) & ( not
x4 in Seg n implies
f4 . x4 = 0. K ) )
;
p is
Permutation of
(Seg n)
by MATRIX_2:def 11;
then A63:
p . i0 in Seg n
by A25, A26, FUNCT_2:7;
then reconsider j0 =
p . i0 as
Element of
NAT ;
Indices (1. K,n) = [:(Seg n),(Seg n):]
by A1, MATRIX_1:24;
then A64:
[i0,j0] in Indices (1. K,n)
by A25, A26, A63, ZFMISC_1:def 2;
i0 <= n
by A25, A26, FINSEQ_1:3;
then A65:
n -' i0 = n - i0
by XREAL_1:235;
i0 in dom (Path_matrix p,(1. K,n))
by A25, A26, A22, FINSEQ_1:def 3;
then A66:
(Path_matrix p,(1. K,n)) . i0 = (1. K,n) * i0,
j0
by MATRIX_3:def 7;
defpred S4[
Element of
NAT ]
means f4 . (i0 + $1) = 0. K;
A67:
0 < i0
by A24, A26, FINSEQ_1:3;
A68:
for
k being
Element of
NAT st
S4[
k] holds
S4[
k + 1]
proof
let k be
Element of
NAT ;
( S4[k] implies S4[k + 1] )
A69:
1
<= 1
+ (i0 + k)
by NAT_1:12;
assume A70:
S4[
k]
;
S4[k + 1]
now per cases
( (i0 + k) + 1 <= n or (i0 + k) + 1 > n )
;
case A71:
(i0 + k) + 1
<= n
;
S4[k + 1]
1
<= 1
+ (i0 + k)
by NAT_1:12;
then
(i0 + k) + 1
in Seg (len (Path_matrix p,(1. K,n)))
by A22, A71;
then
(i0 + k) + 1
in dom (Path_matrix p,(1. K,n))
by FINSEQ_1:def 3;
then A72:
(Path_matrix p,(1. K,n)) . ((i0 + k) + 1) in rng (Path_matrix p,(1. K,n))
by FUNCT_1:def 5;
rng (Path_matrix p,(1. K,n)) c= the
carrier of
K
by FINSEQ_1:def 4;
then reconsider b =
(Path_matrix p,(1. K,n)) . ((i0 + k) + 1) as
Element of
K by A72;
A73:
i0 + k < n
by A71, NAT_1:13;
0 + 1
<= i0 + k
by A67, NAT_1:13;
then A74:
i0 + k in Seg n
by A73;
(i0 + k) + 1
in Seg n
by A69, A71;
then f4 . ((i0 + k) + 1) =
p3 . ((i0 + k) + 1)
by A62
.=
the
multF of
K . (p3 . (i0 + k)),
((Path_matrix p,(1. K,n)) . ((i0 + k) + 1))
by A55, A59, A67, A73
.=
(0. K) * b
by A62, A70, A74
.=
0. K
by VECTSP_1:36
;
hence
S4[
k + 1]
;
verum
hence
S4[
k + 1]
;
verum
end;
1
in Seg n
by A1;
then A75:
f4 . 1
= (Path_matrix p,(1. K,n)) . 1
by A58, A62;
A76:
for
n3 being
Element of
NAT st
0 <> n3 &
n3 < len (Path_matrix p,(1. K,n)) holds
f4 . (n3 + 1) = the
multF of
K . (f4 . n3),
((Path_matrix p,(1. K,n)) . (n3 + 1))
proof
let n3 be
Element of
NAT ;
( 0 <> n3 & n3 < len (Path_matrix p,(1. K,n)) implies f4 . (n3 + 1) = the multF of K . (f4 . n3),((Path_matrix p,(1. K,n)) . (n3 + 1)) )
assume that A77:
0 <> n3
and A78:
n3 < len (Path_matrix p,(1. K,n))
;
f4 . (n3 + 1) = the multF of K . (f4 . n3),((Path_matrix p,(1. K,n)) . (n3 + 1))
A79:
n3 + 1
<= len (Path_matrix p,(1. K,n))
by A78, NAT_1:13;
A80:
0 + 1
<= n3
by A77, NAT_1:13;
then A81:
n3 in Seg n
by A22, A78;
1
< n3 + 1
by A80, NAT_1:13;
then
n3 + 1
in Seg n
by A22, A79;
then A82:
f4 . (n3 + 1) = p3 . (n3 + 1)
by A62;
p3 . (n3 + 1) = the
multF of
K . (p3 . n3),
((Path_matrix p,(1. K,n)) . (n3 + 1))
by A22, A55, A59, A77, A78;
hence
f4 . (n3 + 1) = the
multF of
K . (f4 . n3),
((Path_matrix p,(1. K,n)) . (n3 + 1))
by A62, A82, A81;
verum
end; A83:
1
<= i0
by A24, A26, FINSEQ_1:3;
now per cases
( i0 <= 1 or i0 > 1 )
;
case A84:
i0 > 1
;
S4[ 0 ]reconsider a =
f4 . (i0 -' 1) as
Element of
K ;
i0 < i0 + 1
by NAT_1:13;
then A85:
i0 - 1
< (i0 + 1) - 1
by XREAL_1:16;
i0 <= n
by A25, A26, FINSEQ_1:3;
then A86:
i0 - 1
< len (Path_matrix p,(1. K,n))
by A22, A85, XXREAL_0:2;
i0 -' 1
= i0 - 1
by A84, XREAL_1:235;
then A87:
(i0 -' 1) + 1
= i0
;
i0 - 1
> 1
- 1
by A84, XREAL_1:16;
then f4 . i0 =
the
multF of
K . (f4 . (i0 -' 1)),
((Path_matrix p,(1. K,n)) . i0)
by A76, A86, A87
.=
a * (0. K)
by A28, A66, A64, MATRIX_1:def 12
.=
0. K
by VECTSP_1:36
;
hence
S4[
0 ]
;
verum end; then A88:
S4[
0 ]
;
for
k being
Element of
NAT holds
S4[
k]
from NAT_1:sch 1(A88, A68);
then
S4[
n -' i0]
;
hence
f2 . p = - (the multF of K $$ (Path_matrix p,(1. K,n))),
p
by A1, A8, A54, A22, A75, A76, A65, FINSOP_1:3;
verum end;
hence
f2 . p = - (the multF of K $$ (Path_matrix p,(1. K,n))),
p
;
verum
end;
hence
(Path_product (1. K,n)) . x = f2 . x
by MATRIX_3:def 8;
verum
end;
deffunc H2( set ) -> set = IFIN (idseq n),$1,(1_ K),(0. K);
set F = the addF of K;
set f = Path_product (1. K,n);
set B = FinOmega (Permutations n);
A89:
for x being set st x in Fin (Permutations n) holds
H2(x) in the carrier of K
ex f2 being Function of (Fin (Permutations n)),the carrier of K st
for x being set st x in Fin (Permutations n) holds
f2 . x = H2(x)
from FUNCT_2:sch 2(A89);
then consider G0 being Function of (Fin (Permutations n)),the carrier of K such that
A90:
for x being set st x in Fin (Permutations n) holds
G0 . x = H2(x)
;
dom f2 = Permutations n
by FUNCT_2:def 1;
then A91:
dom (Path_product (1. K,n)) = dom f2
by FUNCT_2:def 1;
then A92:
Path_product (1. K,n) = f2
by A5, FUNCT_1:9;
A93:
for B9 being Element of Fin (Permutations n) st B9 c= FinOmega (Permutations n) & B9 <> {} holds
for x being Element of Permutations n st x in (FinOmega (Permutations n)) \ B9 holds
G0 . (B9 \/ {x}) = the addF of K . (G0 . B9),((Path_product (1. K,n)) . x)
proof
let B9 be
Element of
Fin (Permutations n);
( B9 c= FinOmega (Permutations n) & B9 <> {} implies for x being Element of Permutations n st x in (FinOmega (Permutations n)) \ B9 holds
G0 . (B9 \/ {x}) = the addF of K . (G0 . B9),((Path_product (1. K,n)) . x) )
assume that
B9 c= FinOmega (Permutations n)
and
B9 <> {}
;
for x being Element of Permutations n st x in (FinOmega (Permutations n)) \ B9 holds
G0 . (B9 \/ {x}) = the addF of K . (G0 . B9),((Path_product (1. K,n)) . x)
thus
for
x being
Element of
Permutations n st
x in (FinOmega (Permutations n)) \ B9 holds
G0 . (B9 \/ {x}) = the
addF of
K . (G0 . B9),
((Path_product (1. K,n)) . x)
verumproof
let x be
Element of
Permutations n;
( x in (FinOmega (Permutations n)) \ B9 implies G0 . (B9 \/ {x}) = the addF of K . (G0 . B9),((Path_product (1. K,n)) . x) )
assume A94:
x in (FinOmega (Permutations n)) \ B9
;
G0 . (B9 \/ {x}) = the addF of K . (G0 . B9),((Path_product (1. K,n)) . x)
A97:
0. K is_a_unity_wrt the
addF of
K
by FVSUM_1:8;
A100:
now assume A101:
not
idseq n in B9 \/ {x}
;
the addF of K . (G0 . B9),((Path_product (1. K,n)) . x) = 0. Kthen
not
idseq n in {x}
by XBOOLE_0:def 3;
then A102:
not
idseq n = x
by TARSKI:def 1;
(Path_product (1. K,n)) . x =
H1(
x)
by A3, A92
.=
0. K
by A102, FUNCOP_1:def 8
;
hence
the
addF of
K . (G0 . B9),
((Path_product (1. K,n)) . x) = 0. K
by A98, A97, A101, BINOP_1:11, XBOOLE_0:def 3;
verum end;
A105:
now assume
idseq n in B9 \/ {x}
;
the addF of K . (G0 . B9),((Path_product (1. K,n)) . x) = 1_ Kthen A106:
(
idseq n in B9 or
idseq n in {x} )
by XBOOLE_0:def 3;
now per cases
( idseq n in B9 or idseq n = x )
by A106, TARSKI:def 1;
case A107:
idseq n in B9
;
the addF of K . (G0 . B9),((Path_product (1. K,n)) . x) = 1_ KA108:
not
x in B9
by A94, XBOOLE_0:def 5;
(Path_product (1. K,n)) . x =
H1(
x)
by A3, A92
.=
0. K
by A107, A108, FUNCOP_1:def 8
;
hence
the
addF of
K . (G0 . B9),
((Path_product (1. K,n)) . x) = 1_ K
by A103, A97, A107, BINOP_1:11;
verum end; case A109:
idseq n = x
;
the addF of K . (G0 . B9),((Path_product (1. K,n)) . x) = 1_ K(Path_product (1. K,n)) . x =
H1(
x)
by A3, A92
.=
1_ K
by A109, FUNCOP_1:def 8
;
hence
the
addF of
K . (G0 . B9),
((Path_product (1. K,n)) . x) = 1_ K
by A94, A98, A97, A109, BINOP_1:11, XBOOLE_0:def 5;
verum end; hence
the
addF of
K . (G0 . B9),
((Path_product (1. K,n)) . x) = 1_ K
;
verum end;
hence
G0 . (B9 \/ {x}) = the
addF of
K . (G0 . B9),
((Path_product (1. K,n)) . x)
by A95, A105, A100;
verum
end;
end;
A111:
for x being Element of Permutations n holds G0 . {x} = (Path_product (1. K,n)) . x
A116:
for e being Element of the carrier of K st e is_a_unity_wrt the addF of K holds
G0 . {} = e
idseq n is Element of (Group_of_Perm n)
by MATRIX_2:23;
then
( FinOmega (Permutations n) = Permutations n & idseq n in the carrier of (Group_of_Perm n) )
by MATRIX_2:30, MATRIX_2:def 17;
then
the addF of K $$ (FinOmega (Permutations n)),(Path_product (1. K,n)) = 1_ K
by A119, A116, A111, A93, MATRIX_2:def 13, SETWISEO:def 3;
hence
Det (1. K,n) = 1_ K
by MATRIX_3:def 9; verum