let K be Field; for n being Element of NAT
for A being Matrix of n,K st n >= 1 & A is diagonal holds
Det A = the multF of K $$ (diagonal_of_Matrix A)
let n be Element of NAT ; for A being Matrix of n,K st n >= 1 & A is diagonal holds
Det A = the multF of K $$ (diagonal_of_Matrix A)
let A be Matrix of n,K; ( n >= 1 & A is diagonal implies Det A = the multF of K $$ (diagonal_of_Matrix A) )
assume that
A1:
n >= 1
and
A2:
A is diagonal
; Det A = the multF of K $$ (diagonal_of_Matrix A)
set k1 = the multF of K $$ (diagonal_of_Matrix A);
set X = Permutations n;
set Y = the carrier of K;
reconsider p0 = idseq n as Permutation of (Seg n) ;
A3:
len (diagonal_of_Matrix A) = n
by MATRIX_3:def 10;
deffunc H1( set ) -> Element of the carrier of K = IFEQ (idseq n),$1,(the multF of K $$ (diagonal_of_Matrix A)),(0. K);
A4:
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(A4);
then consider f2 being Function of (Permutations n),the carrier of K such that
A5:
for x being set st x in Permutations n holds
f2 . x = H1(x)
;
A6:
p0 is even
by MATRIX_2:29;
A7:
for x being set st x in dom (Path_product A) holds
(Path_product A) . x = f2 . x
proof
let x be
set ;
( x in dom (Path_product A) implies (Path_product A) . x = f2 . x )
assume
x in dom (Path_product A)
;
(Path_product A) . x = f2 . x
for
p being
Element of
Permutations n holds
f2 . p = - (the multF of K $$ (Path_matrix p,A)),
p
proof
let p be
Element of
Permutations n;
f2 . p = - (the multF of K $$ (Path_matrix p,A)),p
now per cases
( p = idseq n or p <> idseq n )
;
case A9:
p = idseq n
;
f2 . p = - (the multF of K $$ (Path_matrix p,A)),pA10:
for
i,
j being
Nat st
i in dom (diagonal_of_Matrix A) &
j = p . i holds
(diagonal_of_Matrix A) . i = A * i,
j
len (Permutations n) = n
by MATRIX_2:20;
then A14:
- (the multF of K $$ (Path_matrix p,A)),
p = the
multF of
K $$ (Path_matrix p,A)
by A6, A9, MATRIX_2:def 16;
f2 . p =
H1(
p)
by A5
.=
the
multF of
K $$ (diagonal_of_Matrix A)
by A9, FUNCOP_1:def 8
;
hence
f2 . p = - (the multF of K $$ (Path_matrix p,A)),
p
by A3, A14, A10, MATRIX_3:def 7;
verum end; case A15:
p <> idseq n
;
f2 . p = - (the multF of K $$ (Path_matrix p,A)),preconsider Ab =
NAT as non
empty set ;
defpred S1[
Element of
NAT ]
means ( $1
< n implies ex
p3 being
FinSequence of
K st
(
len p3 = $1
+ 1 &
p3 . 1
= (Path_matrix p,A) . 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,A) . (n3 + 1)) ) ) );
A16:
rng (Path_matrix p,A) c= the
carrier of
K
by FINSEQ_1:def 4;
A17:
len (Path_matrix p,A) = n
by MATRIX_3:def 7;
then
1
in Seg (len (Path_matrix p,A))
by A1;
then
1
in dom (Path_matrix p,A)
by FINSEQ_1:def 3;
then
(Path_matrix p,A) . 1
in rng (Path_matrix p,A)
by FUNCT_1:def 5;
then reconsider d =
(Path_matrix p,A) . 1 as
Element of
K by A16;
reconsider q3 =
<*d*> as
FinSequence of
K ;
A18:
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,A) . (n3 + 1))
by NAT_1:13;
A19:
for
k being
Element of
NAT st
S1[
k] holds
S1[
k + 1]
proof
let k be
Element of
NAT ;
( S1[k] implies S1[k + 1] )
assume A20:
S1[
k]
;
S1[k + 1]
now per cases
( k + 1 < n or k + 1 >= n )
;
case A21:
k + 1
< n
;
S1[k + 1]then consider p3 being
FinSequence of
K such that A22:
len p3 = k + 1
and A23:
p3 . 1
= (Path_matrix p,A) . 1
and A24:
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,A) . (n3 + 1))
by A20, NAT_1:12;
defpred S2[
set ,
set ]
means ( ( $1
in Seg (k + 1) implies $2
= p3 . $1 ) & ( not $1
in Seg (k + 1) implies $2
= 0. K ) );
A25:
for
x being
set st
x in NAT holds
ex
y being
set st
(
y in the
carrier of
K &
S2[
x,
y] )
ex
f6 being
Function of
NAT ,the
carrier of
K st
for
x being
set st
x in NAT holds
S2[
x,
f6 . x]
from FUNCT_2:sch 1(A25);
then consider f6 being
Function of
NAT ,the
carrier of
K such that A28:
for
x being
set st
x in NAT holds
S2[
x,
f6 . x]
;
( 1
<= (k + 1) + 1 &
(k + 1) + 1
<= n )
by A21, NAT_1:12, NAT_1:13;
then
(k + 1) + 1
in Seg (len (Path_matrix p,A))
by A17;
then
(k + 1) + 1
in dom (Path_matrix p,A)
by FINSEQ_1:def 3;
then
(
rng (Path_matrix p,A) c= the
carrier of
K &
(Path_matrix p,A) . ((k + 1) + 1) in rng (Path_matrix p,A) )
by FINSEQ_1:def 4, FUNCT_1:def 5;
then
[(f6 . (k + 1)),((Path_matrix p,A) . ((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,A) . ((k + 1) + 1)) as
Element of
K by FUNCT_2:7;
reconsider q3 =
p3 ^ <*e*> as
FinSequence of
K ;
A29:
len q3 =
(len p3) + (len <*e*>)
by FINSEQ_1:35
.=
(k + 1) + 1
by A22, FINSEQ_1:57
;
A30:
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,A) . (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,A) . (n3 + 1)) )
assume that A31:
0 <> n3
and A32:
n3 < (k + 1) + 1
and A33:
n3 < n
;
q3 . (n3 + 1) = the multF of K . (q3 . n3),((Path_matrix p,A) . (n3 + 1))
now per cases
( n3 < k + 1 or n3 >= k + 1 )
;
case A34:
n3 < k + 1
;
q3 . (n3 + 1) = the multF of K . (q3 . n3),((Path_matrix p,A) . (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 A22;
then
n3 + 1
in dom p3
by FINSEQ_1:def 3;
then A35:
p3 . (n3 + 1) = q3 . (n3 + 1)
by FINSEQ_1:def 7;
0 + 1
<= n3
by A31, NAT_1:13;
then
n3 in Seg (len p3)
by A22, A34;
then A36:
n3 in dom p3
by FINSEQ_1:def 3;
p3 . (n3 + 1) = the
multF of
K . (p3 . n3),
((Path_matrix p,A) . (n3 + 1))
by A24, A31, A33, A34;
hence
q3 . (n3 + 1) = the
multF of
K . (q3 . n3),
((Path_matrix p,A) . (n3 + 1))
by A35, A36, FINSEQ_1:def 7;
verum end; case A37:
n3 >= k + 1
;
q3 . (n3 + 1) = the multF of K . (q3 . n3),((Path_matrix p,A) . (n3 + 1))A38:
n3 + 1
<= (k + 1) + 1
by A32, NAT_1:13;
A39:
n3 + 1
> k + 1
by A37, NAT_1:13;
then
n3 + 1
>= (k + 1) + 1
by NAT_1:13;
then A40:
n3 + 1
= (k + 1) + 1
by A38, XXREAL_0:1;
1
<= k + 1
by NAT_1:12;
then A41:
k + 1
in Seg (k + 1)
;
then
k + 1
in dom p3
by A22, FINSEQ_1:def 3;
then A42:
q3 . (k + 1) = p3 . (k + 1)
by FINSEQ_1:def 7;
q3 . (n3 + 1) =
<*e*> . ((n3 + 1) - (k + 1))
by A22, A29, A39, A38, FINSEQ_1:37
.=
e
by A40, FINSEQ_1:def 8
;
hence
q3 . (n3 + 1) = the
multF of
K . (q3 . n3),
((Path_matrix p,A) . (n3 + 1))
by A28, A40, A41, A42;
verum end;
hence
q3 . (n3 + 1) = the
multF of
K . (q3 . n3),
((Path_matrix p,A) . (n3 + 1))
;
verum
end;
1
<= k + 1
by NAT_1:12;
then
1
in Seg (len p3)
by A22;
then
1
in dom p3
by FINSEQ_1:def 3;
then
q3 . 1
= (Path_matrix p,A) . 1
by A23, FINSEQ_1:def 7;
hence
S1[
k + 1]
by A29, A30;
verum end;
hence
S1[
k + 1]
;
verum
end; A43:
f2 . p =
H1(
p)
by A5
.=
0. K
by A15, FUNCOP_1:def 8
;
n < n + 1
by NAT_1:13;
then A44:
n - 1
< (n + 1) - 1
by XREAL_1:16;
A45:
dom p = Seg (len (Permutations n))
by FUNCT_2:67;
then A46:
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 A47:
i0 in dom p
and A48:
p . i0 <> (idseq n) . i0
by A15, FUNCT_1:9;
A49:
i0 in Seg n
by A45, A47, MATRIX_2:20;
reconsider i0 =
i0 as
Element of
NAT by A45, A47;
A50:
p . i0 <> i0
by A46, A47, A48, FUNCT_1:35;
p is
Permutation of
(Seg n)
by MATRIX_2:def 11;
then A51:
p . i0 in Seg n
by A46, A47, FUNCT_2:7;
then reconsider j0 =
p . i0 as
Element of
NAT ;
A52:
n - 1
= n -' 1
by A1, XREAL_1:235;
(
len q3 = 1 &
q3 . 1
= (Path_matrix p,A) . 1 )
by FINSEQ_1:57;
then A53:
S1[
0 ]
by A18;
for
k being
Element of
NAT holds
S1[
k]
from NAT_1:sch 1(A53, A19);
then consider p3 being
FinSequence of
K such that A54:
len p3 = (n -' 1) + 1
and A55:
p3 . 1
= (Path_matrix p,A) . 1
and A56:
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,A) . (n3 + 1))
by A52, A44;
defpred S2[
set ,
set ]
means ( ( $1
in Seg n implies $2
= p3 . $1 ) & ( not $1
in Seg n implies $2
= 0. K ) );
A57:
for
x3 being
Element of
Ab ex
y3 being
Element of
K st
S2[
x3,
y3]
ex
f4 being
Function of
Ab,the
carrier of
K st
for
x2 being
Element of
Ab holds
S2[
x2,
f4 . x2]
from FUNCT_2:sch 3(A57);
then consider f4 being
Function of
NAT ,the
carrier of
K such that A59:
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 ) )
;
A60:
for
n3 being
Element of
NAT st
0 <> n3 &
n3 < len (Path_matrix p,A) holds
f4 . (n3 + 1) = the
multF of
K . (f4 . n3),
((Path_matrix p,A) . (n3 + 1))
proof
let n3 be
Element of
NAT ;
( 0 <> n3 & n3 < len (Path_matrix p,A) implies f4 . (n3 + 1) = the multF of K . (f4 . n3),((Path_matrix p,A) . (n3 + 1)) )
assume that A61:
0 <> n3
and A62:
n3 < len (Path_matrix p,A)
;
f4 . (n3 + 1) = the multF of K . (f4 . n3),((Path_matrix p,A) . (n3 + 1))
A63:
n3 + 1
<= len (Path_matrix p,A)
by A62, NAT_1:13;
A64:
0 + 1
<= n3
by A61, NAT_1:13;
then A65:
n3 in Seg n
by A17, A62;
1
< n3 + 1
by A64, NAT_1:13;
then
n3 + 1
in Seg n
by A17, A63;
then A66:
f4 . (n3 + 1) = p3 . (n3 + 1)
by A59;
p3 . (n3 + 1) = the
multF of
K . (p3 . n3),
((Path_matrix p,A) . (n3 + 1))
by A17, A52, A56, A61, A62;
hence
f4 . (n3 + 1) = the
multF of
K . (f4 . n3),
((Path_matrix p,A) . (n3 + 1))
by A59, A66, A65;
verum
end; A67:
i0 <= n
by A46, A47, FINSEQ_1:3;
then A68:
n -' i0 = n - i0
by XREAL_1:235;
i0 in dom (Path_matrix p,A)
by A49, A17, FINSEQ_1:def 3;
then A69:
(Path_matrix p,A) . i0 = A * i0,
j0
by MATRIX_3:def 7;
defpred S3[
Element of
NAT ]
means f4 . (i0 + $1) = 0. K;
A70:
0 < i0
by A45, A47, FINSEQ_1:3;
A71:
for
k being
Element of
NAT st
S3[
k] holds
S3[
k + 1]
proof
let k be
Element of
NAT ;
( S3[k] implies S3[k + 1] )
A72:
1
<= 1
+ (i0 + k)
by NAT_1:12;
assume A73:
S3[
k]
;
S3[k + 1]
now per cases
( (i0 + k) + 1 <= n or (i0 + k) + 1 > n )
;
case A74:
(i0 + k) + 1
<= n
;
S3[k + 1]
1
<= 1
+ (i0 + k)
by NAT_1:12;
then
(i0 + k) + 1
in Seg (len (Path_matrix p,A))
by A17, A74;
then
(i0 + k) + 1
in dom (Path_matrix p,A)
by FINSEQ_1:def 3;
then A75:
(Path_matrix p,A) . ((i0 + k) + 1) in rng (Path_matrix p,A)
by FUNCT_1:def 5;
rng (Path_matrix p,A) c= the
carrier of
K
by FINSEQ_1:def 4;
then reconsider b =
(Path_matrix p,A) . ((i0 + k) + 1) as
Element of
K by A75;
i0 <= i0 + k
by NAT_1:12;
then A76:
0 < i0 + k
by A45, A47, FINSEQ_1:3;
A77:
i0 + k < n
by A74, NAT_1:13;
0 + 1
<= i0 + k
by A70, NAT_1:13;
then A78:
i0 + k in Seg n
by A77;
(i0 + k) + 1
in Seg n
by A72, A74;
then f4 . ((i0 + k) + 1) =
p3 . ((i0 + k) + 1)
by A59
.=
the
multF of
K . (p3 . (i0 + k)),
((Path_matrix p,A) . ((i0 + k) + 1))
by A52, A56, A77, A76
.=
(0. K) * b
by A59, A73, A78
.=
0. K
by VECTSP_1:36
;
hence
S3[
k + 1]
;
verum
hence
S3[
k + 1]
;
verum
end;
1
in Seg n
by A1;
then A79:
f4 . 1
= (Path_matrix p,A) . 1
by A55, A59;
A80:
1
<= i0
by A45, A47, FINSEQ_1:3;
now per cases
( i0 <= 1 or i0 > 1 )
;
case A81:
i0 > 1
;
S3[ 0 ]reconsider a =
f4 . (i0 -' 1) as
Element of
K ;
i0 < i0 + 1
by NAT_1:13;
then
i0 - 1
< (i0 + 1) - 1
by XREAL_1:16;
then A82:
i0 - 1
< len (Path_matrix p,A)
by A67, A17, XXREAL_0:2;
i0 -' 1
= i0 - 1
by A81, XREAL_1:235;
then A83:
(i0 -' 1) + 1
= i0
;
i0 - 1
> 1
- 1
by A81, XREAL_1:16;
then f4 . i0 =
the
multF of
K . (f4 . (i0 -' 1)),
((Path_matrix p,A) . i0)
by A60, A82, A83
.=
a * (0. K)
by A2, A49, A50, A51, A69, Def2
.=
0. K
by VECTSP_1:36
;
hence
S3[
0 ]
;
verum end; then A84:
S3[
0 ]
;
for
k being
Element of
NAT holds
S3[
k]
from NAT_1:sch 1(A84, A71);
then
S3[
n -' i0]
;
hence
f2 . p = - (the multF of K $$ (Path_matrix p,A)),
p
by A1, A8, A43, A17, A79, A60, A68, FINSOP_1:3;
verum end;
hence
f2 . p = - (the multF of K $$ (Path_matrix p,A)),
p
;
verum
end;
hence
(Path_product A) . x = f2 . x
by MATRIX_3:def 8;
verum
end;
deffunc H2( set ) -> set = IFIN (idseq n),$1,(the multF of K $$ (diagonal_of_Matrix A)),(0. K);
set F = the addF of K;
set f = Path_product A;
set B = FinOmega (Permutations n);
set F4 = diagonal_of_Matrix A;
A85:
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(A85);
then consider G0 being Function of (Fin (Permutations n)),the carrier of K such that
A86:
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 A87:
dom (Path_product A) = dom f2
by FUNCT_2:def 1;
then A88:
Path_product A = f2
by A7, FUNCT_1:9;
A89:
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 A) . x)
A107:
for x being Element of Permutations n holds G0 . {x} = (Path_product A) . x
A112:
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 A) = the multF of K $$ (diagonal_of_Matrix A)
by A115, A112, A107, A89, MATRIX_2:def 13, SETWISEO:def 3;
hence
Det A = the multF of K $$ (diagonal_of_Matrix A)
by MATRIX_3:def 9; verum