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
A2:
for n, m being Nat st [n,m] in Indices M holds
S1[n,m,M * (n,m)]
from MATRIX_0:sch 2(A1);
reconsider M = M as Matrix of n,F_Real ;
A3:
Indices M = [:(Seg n),(Seg n):]
by MATRIX_0:24;
then A5:
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) );
A6:
len (diagonal_of_Matrix M) = n
by MATRIX_3:def 10;
A7:
for k being Nat st S2[k] holds
S2[k + 1]
proof
let k be
Nat;
( S2[k] implies S2[k + 1] )
assume A8:
S2[
k]
;
S2[k + 1]
set k1 =
k + 1;
set ki =
(k + 1) + i;
assume A9:
(k + 1) + i <= n
;
the multF of F_Real "**" ((diagonal_of_Matrix M) | ((k + 1) + i)) = - (1. F_Real)
A10:
(k + 1) + i = (k + i) + 1
;
then A11:
1
<= (k + 1) + i
by NAT_1:11;
then
(k + 1) + i in dom (diagonal_of_Matrix M)
by A6, A9, FINSEQ_3:25;
then A12:
(diagonal_of_Matrix M) | ((k + 1) + i) = ((diagonal_of_Matrix M) | (k + i)) ^ <*((diagonal_of_Matrix M) . ((k + 1) + i))*>
by A10, FINSEQ_5:10;
i <= k + i
by NAT_1:11;
then A13:
i < (k + 1) + i
by A10, NAT_1:13;
A14:
(k + 1) + i in Seg n
by A9, A11;
then
[((k + 1) + i),((k + 1) + i)] in Indices M
by A3, ZFMISC_1:87;
then 1. F_Real =
M * (
((k + 1) + i),
((k + 1) + i))
by A2, A13
.=
(diagonal_of_Matrix M) . ((k + 1) + i)
by A14, MATRIX_3:def 10
;
hence the
multF of
F_Real "**" ((diagonal_of_Matrix M) | ((k + 1) + i)) =
(- (1. F_Real)) * (1. F_Real)
by A8, A9, A10, A12, FINSOP_1:4, NAT_1:13
.=
(- (1. F_Real)) * 1
.=
- (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 );
A15:
S3[ 0 ]
assume A16:
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 A17:
1 <= i
by FINSEQ_1:1;
A18:
i <= n
by A16, FINSEQ_1:1;
then A19:
( (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 ) ) ) )
A20:
for k being Nat st S3[k] holds
S3[k + 1]
proof
let k be
Nat;
( S3[k] implies S3[k + 1] )
assume A21:
S3[
k]
;
S3[k + 1]
set k1 =
k + 1;
assume A22:
k + 1
< i
;
the multF of F_Real "**" ((diagonal_of_Matrix M) | (k + 1)) = 1. F_Real
then A23:
( 1
<= k + 1 &
k + 1
<= n )
by A18, NAT_1:14, XXREAL_0:2;
then
k + 1
in dom (diagonal_of_Matrix M)
by A6, FINSEQ_3:25;
then A24:
(diagonal_of_Matrix M) | (k + 1) = ((diagonal_of_Matrix M) | k) ^ <*((diagonal_of_Matrix M) . (k + 1))*>
by FINSEQ_5:10;
A25:
k + 1
in Seg n
by A23;
then
[(k + 1),(k + 1)] in Indices M
by A3, ZFMISC_1:87;
then 1. F_Real =
M * (
(k + 1),
(k + 1))
by A2, A22
.=
(diagonal_of_Matrix M) . (k + 1)
by A25, MATRIX_3:def 10
;
hence the
multF of
F_Real "**" ((diagonal_of_Matrix M) | (k + 1)) =
(1. F_Real) * (1. F_Real)
by A21, A22, A24, FINSOP_1:4, NAT_1:13
.=
(1. F_Real) * 1
.=
1. F_Real
;
verum
end;
A26:
for k being Nat holds S3[k]
from NAT_1:sch 2(A15, A20);
A27:
S2[ 0 ]
proof
reconsider I =
i - 1 as
Nat by A17;
assume
0 + i <= n
;
the multF of F_Real "**" ((diagonal_of_Matrix M) | (0 + i)) = - (1. F_Real)
A28:
I + 1
= i
;
then
I < i
by NAT_1:13;
then A29:
the
multF of
F_Real "**" ((diagonal_of_Matrix M) | I) = 1. F_Real
by A26;
1
<= i
by A16, FINSEQ_1:1;
then
i in dom (diagonal_of_Matrix M)
by A6, A18, FINSEQ_3:25;
then A30:
(diagonal_of_Matrix M) | i = ((diagonal_of_Matrix M) | I) ^ <*((diagonal_of_Matrix M) . i)*>
by A28, FINSEQ_5:10;
[i,i] in Indices M
by A3, A16, ZFMISC_1:87;
then - (1. F_Real) =
M * (
i,
i)
by A2
.=
(diagonal_of_Matrix M) . i
by A16, MATRIX_3:def 10
;
hence the
multF of
F_Real "**" ((diagonal_of_Matrix M) | (0 + i)) =
(1. F_Real) * (- (1. F_Real))
by A29, A30, FINSOP_1:4
.=
1
* (- (1. F_Real))
.=
- (1. F_Real)
;
verum
end;
for k being Nat holds S2[k]
from NAT_1:sch 2(A27, A7);
hence - (1. F_Real) =
the multF of F_Real "**" ((diagonal_of_Matrix M) | n)
by A19
.=
the multF of F_Real "**" (diagonal_of_Matrix M)
by A6, FINSEQ_1:58
.=
Det M
by A5, A17, A18, 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 A3, A16, ZFMISC_1:87;
hence
M * (i,i) = - (1. F_Real)
by A2; 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 A2; verum