defpred S₁[ 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₁[ 0 ]

proof

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;

P1: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume P10: S₁[n] ; :: thesis: S₁[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

proof

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))

proof

per cases ( 0 < n or not 0 < n ) ;

suppose 0 < n ; :: thesis: Det (Delete (M,i,j)) = Det (Delete (H,i,j))

hence Det (Delete (M,i,j)) = Det (Delete (H,i,j)) by AS1, P10, X41, Y1, LmSign1E; :: thesis: verum

end;

suppose not 0 < n ; :: thesis: Det (Delete (M,i,j)) = Det (Delete (H,i,j))

then Y2: n = 0 ;
then Det (Delete (M,i,j)) = 1. F_Real by Y1, MATRIXR2:41
.= 1. F_Rat
.= Det (Delete (H,i,j)) by Y2, MATRIXR2:41, Y1 ;
hence Det (Delete (M,i,j)) = Det (Delete (H,i,j)) ; :: thesis: verum

end;

end;

end;

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

end;

then LaplaceExpC (M,j) = LaplaceExpC (H,j) by Y3;
hence Det M = Det H by X1, HX1, ZMATRLIN42; :: thesis: verum

end;

for n being Nat holds S₁[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