defpred S_{1}[ Nat] means for M being Matrix of $1,F_Real

for H being Matrix of $1,F_Rat st M = H holds

Det M = Det H;

P0: S_{1}[ 0 ]
_{1}[n] holds

S_{1}[n + 1]
_{1}[n]
from NAT_1:sch 2(P0, P1);

hence for n being Nat

for M being Matrix of n,F_Real

for H being Matrix of n,F_Rat st M = H holds

Det M = Det H ; :: thesis: verum

for H being Matrix of $1,F_Rat st M = H holds

Det M = Det H;

P0: S

proof

P1:
for n being Nat st S
let M be Matrix of 0 ,F_Real; :: thesis: for H being Matrix of 0 ,F_Rat st M = H holds

Det M = Det H

let H be Matrix of 0 ,F_Rat; :: thesis: ( M = H implies Det M = Det H )

assume M = H ; :: thesis: Det M = Det H

Det M = 1. F_Real by MATRIXR2:41

.= 1. F_Rat

.= Det H by MATRIXR2:41 ;

hence Det M = Det H ; :: thesis: verum

end;Det M = Det H

let H be Matrix of 0 ,F_Rat; :: thesis: ( M = H implies Det M = Det H )

assume M = H ; :: thesis: Det M = Det H

Det M = 1. F_Real by MATRIXR2:41

.= 1. F_Rat

.= Det H by MATRIXR2:41 ;

hence Det M = Det H ; :: thesis: verum

S

proof

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

assume P10: S_{1}[n]
; :: thesis: S_{1}[n + 1]

let M be Matrix of n + 1,F_Real; :: thesis: for H being Matrix of n + 1,F_Rat st M = H holds

Det M = Det H

let H be Matrix of n + 1,F_Rat; :: thesis: ( M = H implies Det M = Det H )

assume AS1: M = H ; :: thesis: Det M = Det H

reconsider j = 1 as Nat ;

X0: ( 1 <= 1 & 1 <= n + 1 ) by NAT_1:14;

then JX: j in Seg (n + 1) ;

then X1: Det M = Sum (LaplaceExpC (M,j)) by LAPLACE:27;

HX1: Det H = Sum (LaplaceExpC (H,j)) by JX, LAPLACE:27;

set L = LaplaceExpC (M,j);

set I = LaplaceExpC (H,j);

X2: ( len (LaplaceExpC (M,j)) = n + 1 & ( for i being Nat st i in dom (LaplaceExpC (M,j)) holds

(LaplaceExpC (M,j)) . i = (M * (i,j)) * (Cofactor (M,i,j)) ) ) by LAPLACE:def 8;

Y3: dom (LaplaceExpC (M,j)) = Seg (len (LaplaceExpC (H,j))) by X2, FINSEQ_1:def 3, LAPLACE:def 8

.= dom (LaplaceExpC (H,j)) by FINSEQ_1:def 3 ;

for i being Nat st i in dom (LaplaceExpC (M,j)) holds

(LaplaceExpC (M,j)) . i = (LaplaceExpC (H,j)) . i

hence Det M = Det H by X1, HX1, ZMATRLIN42; :: thesis: verum

end;assume P10: S

let M be Matrix of n + 1,F_Real; :: thesis: for H being Matrix of n + 1,F_Rat st M = H holds

Det M = Det H

let H be Matrix of n + 1,F_Rat; :: thesis: ( M = H implies Det M = Det H )

assume AS1: M = H ; :: thesis: Det M = Det H

reconsider j = 1 as Nat ;

X0: ( 1 <= 1 & 1 <= n + 1 ) by NAT_1:14;

then JX: j in Seg (n + 1) ;

then X1: Det M = Sum (LaplaceExpC (M,j)) by LAPLACE:27;

HX1: Det H = Sum (LaplaceExpC (H,j)) by JX, LAPLACE:27;

set L = LaplaceExpC (M,j);

set I = LaplaceExpC (H,j);

X2: ( len (LaplaceExpC (M,j)) = n + 1 & ( for i being Nat st i in dom (LaplaceExpC (M,j)) holds

(LaplaceExpC (M,j)) . i = (M * (i,j)) * (Cofactor (M,i,j)) ) ) by LAPLACE:def 8;

Y3: dom (LaplaceExpC (M,j)) = Seg (len (LaplaceExpC (H,j))) by X2, FINSEQ_1:def 3, LAPLACE:def 8

.= dom (LaplaceExpC (H,j)) by FINSEQ_1:def 3 ;

for i being Nat st i in dom (LaplaceExpC (M,j)) holds

(LaplaceExpC (M,j)) . i = (LaplaceExpC (H,j)) . i

proof

then
LaplaceExpC (M,j) = LaplaceExpC (H,j)
by Y3;
let i be Nat; :: thesis: ( i in dom (LaplaceExpC (M,j)) implies (LaplaceExpC (M,j)) . i = (LaplaceExpC (H,j)) . i )

assume X30: i in dom (LaplaceExpC (M,j)) ; :: thesis: (LaplaceExpC (M,j)) . i = (LaplaceExpC (H,j)) . i

then X31: (LaplaceExpC (M,j)) . i = (M * (i,j)) * (Cofactor (M,i,j)) by LAPLACE:def 8;

HX31: (LaplaceExpC (H,j)) . i = (H * (i,j)) * (Cofactor (H,i,j)) by Y3, X30, LAPLACE:def 8;

( i in Seg (n + 1) & j in Seg (n + 1) ) by X0, X2, X30, FINSEQ_1:def 3;

then [i,j] in [:(Seg (n + 1)),(Seg (n + 1)):] by ZFMISC_1:87;

then X41: [i,j] in Indices M by MATRIX_0:24;

then X32: M * (i,j) = H * (i,j) by AS1, ZMATRLIN:1;

Y1: (n + 1) -' 1 = n by NAT_D:34;

set DD = Delete (M,i,j);

set EE = Delete (H,i,j);

Det (Delete (M,i,j)) = Det (Delete (H,i,j))

end;assume X30: i in dom (LaplaceExpC (M,j)) ; :: thesis: (LaplaceExpC (M,j)) . i = (LaplaceExpC (H,j)) . i

then X31: (LaplaceExpC (M,j)) . i = (M * (i,j)) * (Cofactor (M,i,j)) by LAPLACE:def 8;

HX31: (LaplaceExpC (H,j)) . i = (H * (i,j)) * (Cofactor (H,i,j)) by Y3, X30, LAPLACE:def 8;

( i in Seg (n + 1) & j in Seg (n + 1) ) by X0, X2, X30, FINSEQ_1:def 3;

then [i,j] in [:(Seg (n + 1)),(Seg (n + 1)):] by ZFMISC_1:87;

then X41: [i,j] in Indices M by MATRIX_0:24;

then X32: M * (i,j) = H * (i,j) by AS1, ZMATRLIN:1;

Y1: (n + 1) -' 1 = n by NAT_D:34;

set DD = Delete (M,i,j);

set EE = Delete (H,i,j);

Det (Delete (M,i,j)) = Det (Delete (H,i,j))

proof
end;

hence
(LaplaceExpC (M,j)) . i = (LaplaceExpC (H,j)) . i
by X32, X31, HX31, ZMATRLIN43; :: thesis: verumhence Det M = Det H by X1, HX1, ZMATRLIN42; :: thesis: verum

hence for n being Nat

for M being Matrix of n,F_Real

for H being Matrix of n,F_Rat st M = H holds

Det M = Det H ; :: thesis: verum