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

Det M in F_Rat ;

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 st M is Matrix of n,F_Rat holds

Det M in F_Rat ; :: thesis: verum

Det M in F_Rat ;

P0: S

proof

P1:
for n being Nat st S
let M be Matrix of 0 ,F_Real; :: thesis: ( M is Matrix of 0 ,F_Rat implies Det M in F_Rat )

assume M is Matrix of 0 ,F_Rat ; :: thesis: Det M in F_Rat

Det M = 1. F_Real by MATRIXR2:41

.= 1 ;

hence Det M in F_Rat ; :: thesis: verum

end;assume M is Matrix of 0 ,F_Rat ; :: thesis: Det M in F_Rat

Det M = 1. F_Real by MATRIXR2:41

.= 1 ;

hence Det M in F_Rat ; :: 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: ( M is Matrix of n + 1,F_Rat implies Det M in F_Rat )

assume AS1: M is Matrix of n + 1,F_Rat ; :: thesis: Det M in F_Rat

reconsider j = 1 as Nat ;

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

then j in Seg (n + 1) ;

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

set L = LaplaceExpC (M,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;

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

(LaplaceExpC (M,j)) . i in F_Rat

end;assume P10: S

let M be Matrix of n + 1,F_Real; :: thesis: ( M is Matrix of n + 1,F_Rat implies Det M in F_Rat )

assume AS1: M is Matrix of n + 1,F_Rat ; :: thesis: Det M in F_Rat

reconsider j = 1 as Nat ;

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

then j in Seg (n + 1) ;

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

set L = LaplaceExpC (M,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;

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

(LaplaceExpC (M,j)) . i in F_Rat

proof

hence
Det M in F_Rat
by X1, LmSign1C; :: thesis: verum
let i be Nat; :: thesis: ( i in dom (LaplaceExpC (M,j)) implies (LaplaceExpC (M,j)) . i in F_Rat )

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

then X31: (LaplaceExpC (M,j)) . i = (M * (i,j)) * (Cofactor (M,i,j)) by 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) is Element of F_Rat by AS1, ZMATRLIN:41;

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

then reconsider DD = Delete (M,i,j) as Matrix of n,F_Real ;

Det DD in F_Rat then A1: Minor (M,i,j) in F_Rat by NAT_D:34;

(power F_Real) . ((- (1_ F_Real)),(i + j)) in F_Rat by LmSign1D;

hence (LaplaceExpC (M,j)) . i in F_Rat by A1, X32, X31, RAT_1:def 2; :: thesis: verum

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

then X31: (LaplaceExpC (M,j)) . i = (M * (i,j)) * (Cofactor (M,i,j)) by 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) is Element of F_Rat by AS1, ZMATRLIN:41;

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

then reconsider DD = Delete (M,i,j) as Matrix of n,F_Real ;

Det DD in F_Rat then A1: Minor (M,i,j) in F_Rat by NAT_D:34;

(power F_Real) . ((- (1_ F_Real)),(i + j)) in F_Rat by LmSign1D;

hence (LaplaceExpC (M,j)) . i in F_Rat by A1, X32, X31, RAT_1:def 2; :: thesis: verum

hence for n being Nat

for M being Matrix of n,F_Real st M is Matrix of n,F_Rat holds

Det M in F_Rat ; :: thesis: verum