let n be Nat; for K being Field
for M being Matrix of n,K
for R being Element of Permutations n st R = Rev (idseq n) & ( for i, j being Nat st i in Seg n & j in Seg n & i + j <= n holds
M * (i,j) = 0. K or for i, j being Nat st i in Seg n & j in Seg n & i + j > n + 1 holds
M * (i,j) = 0. K ) holds
Det M = - (( the multF of K "**" (Path_matrix (R,M))),R)
let K be Field; for M being Matrix of n,K
for R being Element of Permutations n st R = Rev (idseq n) & ( for i, j being Nat st i in Seg n & j in Seg n & i + j <= n holds
M * (i,j) = 0. K or for i, j being Nat st i in Seg n & j in Seg n & i + j > n + 1 holds
M * (i,j) = 0. K ) holds
Det M = - (( the multF of K "**" (Path_matrix (R,M))),R)
let M be Matrix of n,K; for R being Element of Permutations n st R = Rev (idseq n) & ( for i, j being Nat st i in Seg n & j in Seg n & i + j <= n holds
M * (i,j) = 0. K or for i, j being Nat st i in Seg n & j in Seg n & i + j > n + 1 holds
M * (i,j) = 0. K ) holds
Det M = - (( the multF of K "**" (Path_matrix (R,M))),R)
let R be Element of Permutations n; ( R = Rev (idseq n) & ( for i, j being Nat st i in Seg n & j in Seg n & i + j <= n holds
M * (i,j) = 0. K or for i, j being Nat st i in Seg n & j in Seg n & i + j > n + 1 holds
M * (i,j) = 0. K ) implies Det M = - (( the multF of K "**" (Path_matrix (R,M))),R) )
assume that
A1:
R = Rev (idseq n)
and
A2:
( for i, j being Nat st i in Seg n & j in Seg n & i + j <= n holds
M * (i,j) = 0. K or for i, j being Nat st i in Seg n & j in Seg n & i + j > n + 1 holds
M * (i,j) = 0. K )
; Det M = - (( the multF of K "**" (Path_matrix (R,M))),R)
set mm = the multF of K;
idseq n is Element of (Group_of_Perm n)
by MATRIX_1:11;
then reconsider I = idseq n as Element of Permutations n by MATRIX_1:def 13;
set X = Seg n;
reconsider r = Rev (idseq n) as Permutation of (Seg n) by A1, MATRIX_1:def 12;
set Mr = M * r;
set PR = Path_matrix (R,M);
set PI = Path_matrix (I,(M * r));
A3:
len (Path_matrix (R,M)) = n
by MATRIX_3:def 7;
A4:
len (Path_matrix (I,(M * r))) = n
by MATRIX_3:def 7;
A5:
now the multF of K "**" (Path_matrix (I,(M * r))) = the multF of K "**" (Path_matrix (R,M))per cases
( n < 1 or n >= 1 )
;
suppose A8:
n >= 1
;
the multF of K "**" (Path_matrix (I,(M * r))) = the multF of K "**" (Path_matrix (R,M))
rng I = Seg n
;
then A9:
rng (Rev (idseq n)) = Seg n
by FINSEQ_5:57;
reconsider PRR =
(Path_matrix (R,M)) * R as
FinSequence of
K by A3, A8, MATRIX_7:34;
A10:
dom r = Seg n
by FUNCT_2:52;
dom (Path_matrix (R,M)) = Seg n
by A3, FINSEQ_1:def 3;
then A11:
dom PRR = dom R
by A1, A9, RELAT_1:27;
A12:
now for k being Nat st 1 <= k & k <= len (Path_matrix (I,(M * r))) holds
(Path_matrix (I,(M * r))) . k = PRR . kA13:
dom (Path_matrix (R,M)) = Seg n
by A3, FINSEQ_1:def 3;
A14:
dom (Path_matrix (I,(M * r))) = Seg n
by A4, FINSEQ_1:def 3;
let k be
Nat;
( 1 <= k & k <= len (Path_matrix (I,(M * r))) implies (Path_matrix (I,(M * r))) . k = PRR . k )assume that A15:
1
<= k
and A16:
k <= len (Path_matrix (I,(M * r)))
;
(Path_matrix (I,(M * r))) . k = PRR . kA17:
k in Seg n
by A4, A15, A16;
then A18:
(n - k) + 1
in Seg n
by FINSEQ_5:2;
I . k = k
by A17, FUNCT_1:17;
then A19:
(Path_matrix (I,(M * r))) . k = (M * r) * (
k,
k)
by A17, A14, MATRIX_3:def 7;
A20:
len (idseq n) = n
by CARD_1:def 7;
then
r . k = I . ((n - k) + 1)
by A10, A17, FINSEQ_5:def 3;
then A21:
r . k = (n - k) + 1
by A18, FUNCT_1:17;
A22:
Indices M = [:(Seg n),(Seg n):]
by MATRIX_0:24;
then
[k,k] in Indices M
by A17, ZFMISC_1:87;
then consider m being
Nat such that A23:
r . k = m
and A24:
[m,k] in Indices M
and A25:
(M * r) * (
k,
k)
= M * (
m,
k)
by MATRIX11:37;
A26:
m in Seg n
by A22, A24, ZFMISC_1:87;
then A27:
(n - m) + 1
in Seg n
by FINSEQ_5:2;
r . m = I . ((n - m) + 1)
by A10, A20, A26, FINSEQ_5:def 3;
then A28:
R . m = k
by A1, A23, A27, A21, FUNCT_1:17;
m in Seg n
by A22, A24, ZFMISC_1:87;
then
(Path_matrix (R,M)) . m = M * (
m,
k)
by A13, A28, MATRIX_3:def 7;
hence
(Path_matrix (I,(M * r))) . k = PRR . k
by A1, A11, A10, A17, A23, A25, A19, FUNCT_1:12;
verum end;
n is
Element of
NAT
by ORDINAL1:def 12;
then
len PRR = n
by A1, A11, A10, FINSEQ_1:def 3;
hence
the
multF of
K "**" (Path_matrix (I,(M * r))) = the
multF of
K "**" (Path_matrix (R,M))
by A4, A3, A8, A12, FINSEQ_1:14, MATRIX_7:33;
verum end; end; end;
( M * r is upper_triangular Matrix of n,K or M * r is lower_triangular Matrix of n,K )
by A2, Th12, Th13;
then A29: the multF of K $$ (diagonal_of_Matrix (M * r)) =
Det (M * r)
by Th7, Th8
.=
- ((Det M),R)
by A1, MATRIX11:46
;
then A30:
- ((Det M),R) = the multF of K $$ (Path_matrix (R,M))
by A5, Th6;
per cases
( R is even or R is odd )
;
suppose A31:
R is
odd
;
Det M = - (( the multF of K "**" (Path_matrix (R,M))),R)then A32:
- (
( the multF of K "**" (Path_matrix (R,M))),
R)
= - ( the multF of K "**" (Path_matrix (R,M)))
by MATRIX_1:def 16;
- (
(Det M),
R)
= - (Det M)
by A31, MATRIX_1:def 16;
then
(- (( the multF of K "**" (Path_matrix (R,M))),R)) + (- (Det M)) = 0. K
by A30, A32, VECTSP_1:19;
hence
Det M = - (
( the multF of K "**" (Path_matrix (R,M))),
R)
by VECTSP_1:19;
verum end; end;