defpred S1[ 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: S1[ 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 S1[n] holds
S1[n + 1]
proof
let n be Nat; :: thesis: ( S1[n] implies S1[n + 1] )
assume P10: S1[n] ; :: thesis: S1[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 ;
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
.= 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 ;
( i in Seg (n + 1) & j in Seg (n + 1) ) by ;
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 ;
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 ; :: 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
.= 1. F_Rat
.= Det (Delete (H,i,j)) by ;
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 ; :: thesis: verum
end;
then LaplaceExpC (M,j) = LaplaceExpC (H,j) by Y3;
hence Det M = Det H by ; :: thesis: verum
end;
for n being Nat holds S1[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