let i, n be Nat; ( i in Seg n implies ex M being Matrix of n,F_Real st
( Det M = - (1. F_Real) & M * (i,i) = - (1. F_Real) & ( for k, m being Nat st [k,m] in Indices M holds
( ( k = m & k <> i implies M * (k,k) = 1. F_Real ) & ( k <> m implies M * (k,m) = 0. F_Real ) ) ) ) )
set FR = the carrier of F_Real;
set mm = the multF of F_Real;
reconsider N = n as Element of NAT by ORDINAL1:def 12;
defpred S1[ set , set , set ] means ( ( $1 = $2 & $1 = i implies $3 = - (1. F_Real) ) & ( $1 = $2 & $1 <> i implies $3 = 1. F_Real ) & ( $1 <> $2 implies $3 = 0. F_Real ) );
A1:
for k, m being Nat st [k,m] in [:(Seg N),(Seg N):] holds
ex x being Element of F_Real st S1[k,m,x]
proof
let k,
m be
Nat;
( [k,m] in [:(Seg N),(Seg N):] implies ex x being Element of F_Real st S1[k,m,x] )
assume
[k,m] in [:(Seg N),(Seg N):]
;
ex x being Element of F_Real st S1[k,m,x]
( (
k = m &
k = i ) or (
k = m &
k <> i ) or
k <> m )
;
hence
ex
x being
Element of
F_Real st
S1[
k,
m,
x]
;
verum
end;
consider M being Matrix of N,F_Real such that
A3:
for n, m being Nat st [n,m] in Indices M holds
S1[n,m,M * (n,m)]
from MATRIX_1:sch 2(A1);
reconsider M = M as Matrix of n,F_Real ;
A4:
Indices M = [:(Seg n),(Seg n):]
by MATRIX_1:24;
then A6:
M is diagonal
by MATRIX_7:def 2;
set D = diagonal_of_Matrix M;
defpred S2[ Nat] means ( $1 + i <= n implies the multF of F_Real "**" ((diagonal_of_Matrix M) | ($1 + i)) = - (1. F_Real) );
A7:
len (diagonal_of_Matrix M) = n
by MATRIX_3:def 10;
A8:
for k being Nat st S2[k] holds
S2[k + 1]
proof
let k be
Nat;
( S2[k] implies S2[k + 1] )
assume A9:
S2[
k]
;
S2[k + 1]
set k1 =
k + 1;
set ki =
(k + 1) + i;
assume A10:
(k + 1) + i <= n
;
the multF of F_Real "**" ((diagonal_of_Matrix M) | ((k + 1) + i)) = - (1. F_Real)
A11:
(k + 1) + i = (k + i) + 1
;
then A12:
1
<= (k + 1) + i
by NAT_1:11;
then
(k + 1) + i in dom (diagonal_of_Matrix M)
by A7, A10, FINSEQ_3:25;
then A13:
(diagonal_of_Matrix M) | ((k + 1) + i) = ((diagonal_of_Matrix M) | (k + i)) ^ <*((diagonal_of_Matrix M) . ((k + 1) + i))*>
by A11, FINSEQ_5:10;
i <= k + i
by NAT_1:11;
then A14:
i < (k + 1) + i
by A11, NAT_1:13;
A15:
(k + 1) + i in Seg n
by A10, A12;
then
[((k + 1) + i),((k + 1) + i)] in Indices M
by A4, ZFMISC_1:87;
then 1. F_Real =
M * (
((k + 1) + i),
((k + 1) + i))
by A3, A14
.=
(diagonal_of_Matrix M) . ((k + 1) + i)
by A15, MATRIX_3:def 10
;
hence the
multF of
F_Real "**" ((diagonal_of_Matrix M) | ((k + 1) + i)) =
(- (1. F_Real)) * (1. F_Real)
by A9, A10, A11, A13, FINSOP_1:4, NAT_1:13
.=
- (1. F_Real)
;
verum
end;
defpred S3[ Nat] means ( $1 < i implies the multF of F_Real "**" ((diagonal_of_Matrix M) | $1) = 1. F_Real );
A16:
S3[ 0 ]
assume A17:
i in Seg n
; ex M being Matrix of n,F_Real st
( Det M = - (1. F_Real) & M * (i,i) = - (1. F_Real) & ( for k, m being Nat st [k,m] in Indices M holds
( ( k = m & k <> i implies M * (k,k) = 1. F_Real ) & ( k <> m implies M * (k,m) = 0. F_Real ) ) ) )
then A18:
1 <= i
by FINSEQ_1:1;
A19:
i <= n
by A17, FINSEQ_1:1;
then A20:
( (n - i) + i = n & n - i is Nat )
by NAT_1:21;
take
M
; ( Det M = - (1. F_Real) & M * (i,i) = - (1. F_Real) & ( for k, m being Nat st [k,m] in Indices M holds
( ( k = m & k <> i implies M * (k,k) = 1. F_Real ) & ( k <> m implies M * (k,m) = 0. F_Real ) ) ) )
A21:
for k being Nat st S3[k] holds
S3[k + 1]
proof
let k be
Nat;
( S3[k] implies S3[k + 1] )
assume A22:
S3[
k]
;
S3[k + 1]
set k1 =
k + 1;
assume A23:
k + 1
< i
;
the multF of F_Real "**" ((diagonal_of_Matrix M) | (k + 1)) = 1. F_Real
then A24:
( 1
<= k + 1 &
k + 1
<= n )
by A19, NAT_1:14, XXREAL_0:2;
then
k + 1
in dom (diagonal_of_Matrix M)
by A7, FINSEQ_3:25;
then A25:
(diagonal_of_Matrix M) | (k + 1) = ((diagonal_of_Matrix M) | k) ^ <*((diagonal_of_Matrix M) . (k + 1))*>
by FINSEQ_5:10;
A26:
k + 1
in Seg n
by A24;
then
[(k + 1),(k + 1)] in Indices M
by A4, ZFMISC_1:87;
then 1. F_Real =
M * (
(k + 1),
(k + 1))
by A3, A23
.=
(diagonal_of_Matrix M) . (k + 1)
by A26, MATRIX_3:def 10
;
hence the
multF of
F_Real "**" ((diagonal_of_Matrix M) | (k + 1)) =
(1. F_Real) * (1. F_Real)
by A22, A23, A25, FINSOP_1:4, NAT_1:13
.=
1. F_Real
;
verum
end;
A27:
for k being Nat holds S3[k]
from NAT_1:sch 2(A16, A21);
A28:
S2[ 0 ]
proof
reconsider I =
i - 1 as
Nat by A18, NAT_1:21;
assume
0 + i <= n
;
the multF of F_Real "**" ((diagonal_of_Matrix M) | (0 + i)) = - (1. F_Real)
A29:
I + 1
= i
;
then
I < i
by NAT_1:13;
then A30:
the
multF of
F_Real "**" ((diagonal_of_Matrix M) | I) = 1. F_Real
by A27;
1
<= i
by A17, FINSEQ_1:1;
then
i in dom (diagonal_of_Matrix M)
by A7, A19, FINSEQ_3:25;
then A31:
(diagonal_of_Matrix M) | i = ((diagonal_of_Matrix M) | I) ^ <*((diagonal_of_Matrix M) . i)*>
by A29, FINSEQ_5:10;
[i,i] in Indices M
by A4, A17, ZFMISC_1:87;
then - (1. F_Real) =
M * (
i,
i)
by A3
.=
(diagonal_of_Matrix M) . i
by A17, MATRIX_3:def 10
;
hence the
multF of
F_Real "**" ((diagonal_of_Matrix M) | (0 + i)) =
(1. F_Real) * (- (1. F_Real))
by A30, A31, FINSOP_1:4
.=
- (1. F_Real)
;
verum
end;
for k being Nat holds S2[k]
from NAT_1:sch 2(A28, A8);
hence - (1. F_Real) =
the multF of F_Real "**" ((diagonal_of_Matrix M) | n)
by A20
.=
the multF of F_Real "**" (diagonal_of_Matrix M)
by A7, FINSEQ_1:58
.=
Det M
by A6, A18, A19, MATRIX_7:17, XXREAL_0:2
;
( M * (i,i) = - (1. F_Real) & ( for k, m being Nat st [k,m] in Indices M holds
( ( k = m & k <> i implies M * (k,k) = 1. F_Real ) & ( k <> m implies M * (k,m) = 0. F_Real ) ) ) )
[i,i] in Indices M
by A4, A17, ZFMISC_1:87;
hence
M * (i,i) = - (1. F_Real)
by A3; for k, m being Nat st [k,m] in Indices M holds
( ( k = m & k <> i implies M * (k,k) = 1. F_Real ) & ( k <> m implies M * (k,m) = 0. F_Real ) )
let k, m be Nat; ( [k,m] in Indices M implies ( ( k = m & k <> i implies M * (k,k) = 1. F_Real ) & ( k <> m implies M * (k,m) = 0. F_Real ) ) )
assume
[k,m] in Indices M
; ( ( k = m & k <> i implies M * (k,k) = 1. F_Real ) & ( k <> m implies M * (k,m) = 0. F_Real ) )
hence
( ( k = m & k <> i implies M * (k,k) = 1. F_Real ) & ( k <> m implies M * (k,m) = 0. F_Real ) )
by A3; verum