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