let i, n be Nat; :: thesis: ( 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 S_{1}[ 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 S_{1}[k,m,x]

A2: for n, m being Nat st [n,m] in Indices M holds

S_{1}[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;

set D = diagonal_of_Matrix M;

defpred S_{2}[ 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 S_{2}[k] holds

S_{2}[k + 1]
_{3}[ Nat] means ( $1 < i implies the multF of F_Real "**" ((diagonal_of_Matrix M) | $1) = 1. F_Real );

A15: S_{3}[ 0 ]

( 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 ; :: thesis: ( 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 S_{3}[k] holds

S_{3}[k + 1]
_{3}[k]
from NAT_1:sch 2(A15, A20);

A27: S_{2}[ 0 ]
_{2}[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 ;

:: thesis: ( 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; :: thesis: 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; :: thesis: ( [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 ; :: thesis: ( ( 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; :: thesis: verum

( 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 S

A1: for k, m being Nat st [k,m] in [:(Seg N),(Seg N):] holds

ex x being Element of F_Real st S

proof

consider M being Matrix of N,F_Real such that
let k, m be Nat; :: thesis: ( [k,m] in [:(Seg N),(Seg N):] implies ex x being Element of F_Real st S_{1}[k,m,x] )

assume [k,m] in [:(Seg N),(Seg N):] ; :: thesis: ex x being Element of F_Real st S_{1}[k,m,x]

( ( k = m & k = i ) or ( k = m & k <> i ) or k <> m ) ;

hence ex x being Element of F_Real st S_{1}[k,m,x]
; :: thesis: verum

end;assume [k,m] in [:(Seg N),(Seg N):] ; :: thesis: ex x being Element of F_Real st S

( ( k = m & k = i ) or ( k = m & k <> i ) or k <> m ) ;

hence ex x being Element of F_Real st S

A2: for n, m being Nat st [n,m] in Indices M holds

S

reconsider M = M as Matrix of n,F_Real ;

A3: Indices M = [:(Seg n),(Seg n):] by MATRIX_0:24;

now :: thesis: for k, m being Nat st k in Seg n & m in Seg n & k <> m holds

M * (k,m) = 0. F_Real

then A5:
M is V254( F_Real )
by MATRIX_7:def 2;M * (k,m) = 0. F_Real

let k, m be Nat; :: thesis: ( k in Seg n & m in Seg n & k <> m implies M * (k,m) = 0. F_Real )

assume ( k in Seg n & m in Seg n ) ; :: thesis: ( k <> m implies M * (k,m) = 0. F_Real )

then A4: [k,m] in Indices M by A3, ZFMISC_1:87;

assume k <> m ; :: thesis: M * (k,m) = 0. F_Real

hence M * (k,m) = 0. F_Real by A2, A4; :: thesis: verum

end;assume ( k in Seg n & m in Seg n ) ; :: thesis: ( k <> m implies M * (k,m) = 0. F_Real )

then A4: [k,m] in Indices M by A3, ZFMISC_1:87;

assume k <> m ; :: thesis: M * (k,m) = 0. F_Real

hence M * (k,m) = 0. F_Real by A2, A4; :: thesis: verum

set D = diagonal_of_Matrix M;

defpred S

A6: len (diagonal_of_Matrix M) = n by MATRIX_3:def 10;

A7: for k being Nat st S

S

proof

defpred S
let k be Nat; :: thesis: ( S_{2}[k] implies S_{2}[k + 1] )

assume A8: S_{2}[k]
; :: thesis: S_{2}[k + 1]

set k1 = k + 1;

set ki = (k + 1) + i;

assume A9: (k + 1) + i <= n ; :: thesis: 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) ;

:: thesis: verum

end;assume A8: S

set k1 = k + 1;

set ki = (k + 1) + i;

assume A9: (k + 1) + i <= n ; :: thesis: 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) ;

:: thesis: verum

A15: S

proof

assume A16:
i in Seg n
; :: thesis: ex M being Matrix of n,F_Real st
assume
0 < i
; :: thesis: the multF of F_Real "**" ((diagonal_of_Matrix M) | 0) = 1. F_Real

( (diagonal_of_Matrix M) | 0 = <*> the carrier of F_Real & the_unity_wrt the multF of F_Real = 1. F_Real ) by FVSUM_1:5;

hence the multF of F_Real "**" ((diagonal_of_Matrix M) | 0) = 1. F_Real by FINSOP_1:10; :: thesis: verum

end;( (diagonal_of_Matrix M) | 0 = <*> the carrier of F_Real & the_unity_wrt the multF of F_Real = 1. F_Real ) by FVSUM_1:5;

hence the multF of F_Real "**" ((diagonal_of_Matrix M) | 0) = 1. F_Real by FINSOP_1:10; :: thesis: verum

( 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 ; :: thesis: ( 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 S

S

proof

A26:
for k being Nat holds S
let k be Nat; :: thesis: ( S_{3}[k] implies S_{3}[k + 1] )

assume A21: S_{3}[k]
; :: thesis: S_{3}[k + 1]

set k1 = k + 1;

assume A22: k + 1 < i ; :: thesis: 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 ;

:: thesis: verum

end;assume A21: S

set k1 = k + 1;

assume A22: k + 1 < i ; :: thesis: 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 ;

:: thesis: verum

A27: S

proof

for k being Nat holds S
reconsider I = i - 1 as Nat by A17;

assume 0 + i <= n ; :: thesis: 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) ;

:: thesis: verum

end;assume 0 + i <= n ; :: thesis: 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) ;

:: thesis: verum

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 ;

:: thesis: ( 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; :: thesis: 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; :: thesis: ( [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 ; :: thesis: ( ( 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; :: thesis: verum