let K be Field; for n being 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 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( object ) -> Element of the carrier of K = IFEQ ((idseq n),$1,( the multF of K $$ (diagonal_of_Matrix A)),(0. K));
A4:
for x being object 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 object 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 object st x in Permutations n holds
f2 . x = H1(x)
;
A6:
p0 is even
by MATRIX_1:16;
A7:
for x being object st x in dom (Path_product A) holds
(Path_product A) . x = f2 . x
proof
let x be
object ;
( 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 ( ( p = idseq n & f2 . p = - (( the multF of K $$ (Path_matrix (p,A))),p) ) or ( p <> idseq n & f2 . p = - (( the multF of K $$ (Path_matrix (p,A))),p) ) )per cases
( p = idseq n or p <> idseq n )
;
case A9:
p = idseq n
;
f2 . p = - (( the multF of K $$ (Path_matrix (p,A))),p)A10:
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_1:9;
then A14:
- (
( the multF of K $$ (Path_matrix (p,A))),
p)
= the
multF of
K $$ (Path_matrix (p,A))
by A6, A9, MATRIX_1: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))),p)reconsider Ab =
NAT as non
empty set ;
defpred S1[
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
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 3;
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
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
Nat st
S1[
k] holds
S1[
k + 1]
proof
let k be
Nat;
( S1[k] implies S1[k + 1] )
assume A20:
S1[
k]
;
S1[k + 1]
now ( ( k + 1 < n & S1[k + 1] ) or ( k + 1 >= n & S1[k + 1] ) )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
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[
object ,
object ]
means ( ( $1
in Seg (k + 1) implies $2
= p3 . $1 ) & ( not $1
in Seg (k + 1) implies $2
= 0. K ) );
A25:
for
x being
object st
x in NAT holds
ex
y being
object st
(
y in the
carrier of
K &
S2[
x,
y] )
ex
f6 being
sequence of the
carrier of
K st
for
x being
object st
x in NAT holds
S2[
x,
f6 . x]
from FUNCT_2:sch 1(A25);
then consider f6 being
sequence of the
carrier of
K such that A28:
for
x being
object 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 3;
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:5;
reconsider q3 =
p3 ^ <*e*> as
FinSequence of
K ;
A29:
len q3 =
(len p3) + (len <*e*>)
by FINSEQ_1:22
.=
(k + 1) + 1
by A22, FINSEQ_1:40
;
A30:
for
n3 being
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
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 ( ( n3 < k + 1 & q3 . (n3 + 1) = the multF of K . ((q3 . n3),((Path_matrix (p,A)) . (n3 + 1))) ) or ( n3 >= k + 1 & q3 . (n3 + 1) = the multF of K . ((q3 . n3),((Path_matrix (p,A)) . (n3 + 1))) ) )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:24
.=
e
by A40
;
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:14;
A45:
dom p = Seg (len (Permutations n))
by FUNCT_2:52;
then A46:
dom p = Seg n
by MATRIX_1:9;
then
dom p = dom (idseq n)
by RELAT_1:45;
then consider i0 being
object such that A47:
i0 in dom p
and A48:
p . i0 <> (idseq n) . i0
by A15, FUNCT_1:2;
A49:
i0 in Seg n
by A45, A47, MATRIX_1:9;
reconsider i0 =
i0 as
Nat by A45, A47;
A50:
p . i0 <> i0
by A46, A47, A48, FUNCT_1:18;
p is
Permutation of
(Seg n)
by MATRIX_1:def 12;
then A51:
p . i0 in Seg n
by A46, A47, FUNCT_2:5;
then reconsider j0 =
p . i0 as
Nat ;
A52:
n - 1
= n -' 1
by A1, XREAL_1:233;
(
len q3 = 1 &
q3 . 1
= (Path_matrix (p,A)) . 1 )
by FINSEQ_1:40;
then A53:
S1[
0 ]
by A18;
for
k being
Nat holds
S1[
k]
from NAT_1:sch 2(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
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
sequence of 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
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
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:1;
then A68:
n -' i0 = n - i0
by XREAL_1:233;
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[
Nat]
means f4 . (i0 + $1) = 0. K;
A70:
0 < i0
by A45, A47, FINSEQ_1:1;
A71:
for
k being
Nat st
S3[
k] holds
S3[
k + 1]
proof
let k be
Nat;
( S3[k] implies S3[k + 1] )
A72:
1
<= 1
+ (i0 + k)
by NAT_1:12;
assume A73:
S3[
k]
;
S3[k + 1]
now ( ( (i0 + k) + 1 <= n & S3[k + 1] ) or ( (i0 + k) + 1 > n & S3[k + 1] ) )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 3;
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:1;
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
;
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:1;
now ( ( i0 <= 1 & S3[ 0 ] ) or ( i0 > 1 & S3[ 0 ] ) )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:14;
then A82:
i0 - 1
< len (Path_matrix (p,A))
by A67, A17, XXREAL_0:2;
i0 -' 1
= i0 - 1
by A81, XREAL_1:233;
then A83:
(i0 -' 1) + 1
= i0
;
i0 - 1
> 1
- 1
by A81, XREAL_1:14;
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
.=
0. K
;
hence
S3[
0 ]
;
verum end; then A84:
S3[
0 ]
;
for
k being
Nat holds
S3[
k]
from NAT_1:sch 2(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:2;
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 ) -> object = 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 = In ((Permutations n),(Fin (Permutations n)));
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 11(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:2;
A89:
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 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
S:
idseq n is Element of (Group_of_Perm n)
by MATRIX_1:11;
Permutations n in Fin (Permutations n)
by FINSUB_1:def 5;
then
( In ((Permutations n),(Fin (Permutations n))) = Permutations n & idseq n in the carrier of (Group_of_Perm n) )
by S, SUBSET_1:def 8;
then
the addF of K $$ ((In ((Permutations n),(Fin (Permutations n)))),(Path_product A)) = the multF of K $$ (diagonal_of_Matrix A)
by A115, A112, A107, A89, MATRIX_1:def 13, SETWISEO:def 3;
hence
Det A = the multF of K $$ (diagonal_of_Matrix A)
by MATRIX_3:def 9; verum