let n be Nat; :: thesis: for K being Field
for A, B being Matrix of n,K ex P being Polynomial of K st
( len P <= n + 1 & ( for x being Element of K holds eval P,x = Det (A + (x * B)) ) )
let K be Field; :: thesis: for A, B being Matrix of n,K ex P being Polynomial of K st
( len P <= n + 1 & ( for x being Element of K holds eval P,x = Det (A + (x * B)) ) )
defpred S₁[ Nat] means for A, B being Matrix of $1,K ex P being Polynomial of K st
( len P <= $1 + 1 & ( for x being Element of K holds eval P,x = Det (A + (x * B)) ) );
A1: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A2: S₁[n] ; :: thesis: S₁[n + 1]
set n1 = n + 1;
let A, B be Matrix of n + 1,K; :: thesis: ex P being Polynomial of K st
( len P <= (n + 1) + 1 & ( for x being Element of K holds eval P,x = Det (A + (x * B)) ) )
defpred S₂[ Nat] means ( $1 <= n + 1 implies ex P being Polynomial of K st
( len P <= (n + 1) + 1 & ( for x being Element of K holds eval P,x = Sum ((LaplaceExpL (A + (x * B)),(n + 1)) | $1) ) ) );
A3: n + 1 in Seg (n + 1) by FINSEQ_1:6;
A4: for m being Nat st S₂[m] holds
S₂[m + 1]

proof

let m be Nat; :: thesis: ( S₂[m] implies S₂[m + 1] )
assume A5: S₂[m] ; :: thesis: S₂[m + 1]
set m1 = m + 1;
assume A6: m + 1 <= n + 1 ; :: thesis: ex P being Polynomial of K st
( len P <= (n + 1) + 1 & ( for x being Element of K holds eval P,x = Sum ((LaplaceExpL (A + (x * B)),(n + 1)) | (m + 1)) ) )
then consider P being Polynomial of K such that
A7: len P <= (n + 1) + 1 and
A8: for x being Element of K holds eval P,x = Sum ((LaplaceExpL (A + (x * B)),(n + 1)) | m) by A5, NAT_1:13;
1 <= m + 1 by NAT_1:11;
then A9: m + 1 in Seg (n + 1) by A6;
then A10: [(n + 1),(m + 1)] in [:(Seg (n + 1)),(Seg (n + 1)):] by A3, ZFMISC_1:106;
set pow = (power K) . (- (1_ K)),((m + 1) + (n + 1));
set DB = Delete B,(n + 1),(m + 1);
set DA = Delete A,(n + 1),(m + 1);
set P2 = <%((A * (n + 1),(m + 1)) * ((power K) . (- (1_ K)),((m + 1) + (n + 1)))),((B * (n + 1),(m + 1)) * ((power K) . (- (1_ K)),((m + 1) + (n + 1))))%>;
A11: Indices B = [:(Seg (n + 1)),(Seg (n + 1)):] by MATRIX_1:25;
(n + 1) -' 1 = n by NAT_D:34;
then consider P1 being Polynomial of K such that
A12: len P1 <= n + 1 and
A13: for x being Element of K holds eval P1,x = Det ((Delete A,(n + 1),(m + 1)) + (x * (Delete B,(n + 1),(m + 1)))) by A2;
take PP = P + (P1 *' <%((A * (n + 1),(m + 1)) * ((power K) . (- (1_ K)),((m + 1) + (n + 1)))),((B * (n + 1),(m + 1)) * ((power K) . (- (1_ K)),((m + 1) + (n + 1))))%>); :: thesis: ( len PP <= (n + 1) + 1 & ( for x being Element of K holds eval PP,x = Sum ((LaplaceExpL (A + (x * B)),(n + 1)) | (m + 1)) ) )
len <%((A * (n + 1),(m + 1)) * ((power K) . (- (1_ K)),((m + 1) + (n + 1)))),((B * (n + 1),(m + 1)) * ((power K) . (- (1_ K)),((m + 1) + (n + 1))))%> <= 2 by POLYNOM5:40;
then (len P1) + (len <%((A * (n + 1),(m + 1)) * ((power K) . (- (1_ K)),((m + 1) + (n + 1)))),((B * (n + 1),(m + 1)) * ((power K) . (- (1_ K)),((m + 1) + (n + 1))))%>) <= (n + 1) + 2 by A12, XREAL_1:9;
then A14: ((len P1) + (len <%((A * (n + 1),(m + 1)) * ((power K) . (- (1_ K)),((m + 1) + (n + 1)))),((B * (n + 1),(m + 1)) * ((power K) . (- (1_ K)),((m + 1) + (n + 1))))%>)) -' 1 <= ((n + 1) + 2) -' 1 by NAT_D:42;
( ((n + 2) + 1) -' 1 = n + 2 & len (P1 *' <%((A * (n + 1),(m + 1)) * ((power K) . (- (1_ K)),((m + 1) + (n + 1)))),((B * (n + 1),(m + 1)) * ((power K) . (- (1_ K)),((m + 1) + (n + 1))))%>) <= ((len P1) + (len <%((A * (n + 1),(m + 1)) * ((power K) . (- (1_ K)),((m + 1) + (n + 1)))),((B * (n + 1),(m + 1)) * ((power K) . (- (1_ K)),((m + 1) + (n + 1))))%>)) -' 1 ) by HILBASIS:21, NAT_D:34;
then len (P1 *' <%((A * (n + 1),(m + 1)) * ((power K) . (- (1_ K)),((m + 1) + (n + 1)))),((B * (n + 1),(m + 1)) * ((power K) . (- (1_ K)),((m + 1) + (n + 1))))%>) <= (n + 1) + 1 by A14, XXREAL_0:2;
hence len PP <= (n + 1) + 1 by A7, POLYNOM4:9; :: thesis: for x being Element of K holds eval PP,x = Sum ((LaplaceExpL (A + (x * B)),(n + 1)) | (m + 1))
let x be Element of K; :: thesis: eval PP,x = Sum ((LaplaceExpL (A + (x * B)),(n + 1)) | (m + 1))
set L = LaplaceExpL (A + (x * B)),(n + 1);
A15: Indices A = [:(Seg (n + 1)),(Seg (n + 1)):] by MATRIX_1:25;
A16: ((A * (n + 1),(m + 1)) * ((power K) . (- (1_ K)),((m + 1) + (n + 1)))) + (((B * (n + 1),(m + 1)) * ((power K) . (- (1_ K)),((m + 1) + (n + 1)))) * x) = ((A * (n + 1),(m + 1)) * ((power K) . (- (1_ K)),((m + 1) + (n + 1)))) + (((B * (n + 1),(m + 1)) * x) * ((power K) . (- (1_ K)),((m + 1) + (n + 1)))) by GROUP_1:def 4
.= ((A * (n + 1),(m + 1)) + ((B * (n + 1),(m + 1)) * x)) * ((power K) . (- (1_ K)),((m + 1) + (n + 1))) by VECTSP_1:def 11
.= ((A * (n + 1),(m + 1)) + ((x * B) * (n + 1),(m + 1))) * ((power K) . (- (1_ K)),((m + 1) + (n + 1))) by A10, A11, MATRIX_3:def 5
.= ((A + (x * B)) * (n + 1),(m + 1)) * ((power K) . (- (1_ K)),((m + 1) + (n + 1))) by A10, A15, MATRIX_3:def 3 ;
n + 1 = len (LaplaceExpL (A + (x * B)),(n + 1)) by LAPLACE:def 7;
then A17: dom (LaplaceExpL (A + (x * B)),(n + 1)) = Seg (n + 1) by FINSEQ_1:def 3;
then A18: (LaplaceExpL (A + (x * B)),(n + 1)) | (m + 1) = ((LaplaceExpL (A + (x * B)),(n + 1)) | m) ^ <*((LaplaceExpL (A + (x * B)),(n + 1)) . (m + 1))*> by A9, FINSEQ_5:11;
A19: (Delete A,(n + 1),(m + 1)) + (x * (Delete B,(n + 1),(m + 1))) = (Delete A,(n + 1),(m + 1)) + (Delete (x * B),(n + 1),(m + 1)) by A3, A9, Th5
.= Delete (A + (x * B)),(n + 1),(m + 1) by A3, A9, Th4 ;
eval (P1 *' <%((A * (n + 1),(m + 1)) * ((power K) . (- (1_ K)),((m + 1) + (n + 1)))),((B * (n + 1),(m + 1)) * ((power K) . (- (1_ K)),((m + 1) + (n + 1))))%>),x = (eval P1,x) * (eval <%((A * (n + 1),(m + 1)) * ((power K) . (- (1_ K)),((m + 1) + (n + 1)))),((B * (n + 1),(m + 1)) * ((power K) . (- (1_ K)),((m + 1) + (n + 1))))%>,x) by POLYNOM4:27
.= (Det ((Delete A,(n + 1),(m + 1)) + (x * (Delete B,(n + 1),(m + 1))))) * (eval <%((A * (n + 1),(m + 1)) * ((power K) . (- (1_ K)),((m + 1) + (n + 1)))),((B * (n + 1),(m + 1)) * ((power K) . (- (1_ K)),((m + 1) + (n + 1))))%>,x) by A13
.= (Minor (A + (x * B)),(n + 1),(m + 1)) * (((A + (x * B)) * (n + 1),(m + 1)) * ((power K) . (- (1_ K)),((m + 1) + (n + 1)))) by A16, A19, POLYNOM5:45
.= ((A + (x * B)) * (n + 1),(m + 1)) * (Cofactor (A + (x * B)),(n + 1),(m + 1)) by GROUP_1:def 4
.= (LaplaceExpL (A + (x * B)),(n + 1)) . (m + 1) by A9, A17, LAPLACE:def 7 ;
hence Sum ((LaplaceExpL (A + (x * B)),(n + 1)) | (m + 1)) = (Sum ((LaplaceExpL (A + (x * B)),(n + 1)) | m)) + (eval (P1 *' <%((A * (n + 1),(m + 1)) * ((power K) . (- (1_ K)),((m + 1) + (n + 1)))),((B * (n + 1),(m + 1)) * ((power K) . (- (1_ K)),((m + 1) + (n + 1))))%>),x) by A18, FVSUM_1:87
.= (eval P,x) + (eval (P1 *' <%((A * (n + 1),(m + 1)) * ((power K) . (- (1_ K)),((m + 1) + (n + 1)))),((B * (n + 1),(m + 1)) * ((power K) . (- (1_ K)),((m + 1) + (n + 1))))%>),x) by A8
.= eval PP,x by POLYNOM4:22 ;
:: thesis: verum

end;

A20: S₂[ 0 ]

proof

assume 0 <= n + 1 ; :: thesis: ex P being Polynomial of K st
( len P <= (n + 1) + 1 & ( for x being Element of K holds eval P,x = Sum ((LaplaceExpL (A + (x * B)),(n + 1)) | 0 ) ) )
take P = 0_. K; :: thesis: ( len P <= (n + 1) + 1 & ( for x being Element of K holds eval P,x = Sum ((LaplaceExpL (A + (x * B)),(n + 1)) | 0 ) ) )
thus len P <= (n + 1) + 1 by POLYNOM4:6; :: thesis: for x being Element of K holds eval P,x = Sum ((LaplaceExpL (A + (x * B)),(n + 1)) | 0 )
let x be Element of K; :: thesis: eval P,x = Sum ((LaplaceExpL (A + (x * B)),(n + 1)) | 0 )
(LaplaceExpL (A + (x * B)),(n + 1)) | 0 = <*> the carrier of K ;
hence Sum ((LaplaceExpL (A + (x * B)),(n + 1)) | 0 ) = 0. K by RLVECT_1:60
.= eval P,x by POLYNOM4:20 ;
:: thesis: verum

end;

for m being Nat holds S₂[m] from NAT_1:sch 2(A20, A4);
then consider P being Polynomial of K such that
A21: len P <= (n + 1) + 1 and
A22: for x being Element of K holds eval P,x = Sum ((LaplaceExpL (A + (x * B)),(n + 1)) | (n + 1)) ;
take P ; :: thesis: ( len P <= (n + 1) + 1 & ( for x being Element of K holds eval P,x = Det (A + (x * B)) ) )
thus len P <= (n + 1) + 1 by A21; :: thesis: for x being Element of K holds eval P,x = Det (A + (x * B))
let x be Element of K; :: thesis: eval P,x = Det (A + (x * B))
A23: len (LaplaceExpL (A + (x * B)),(n + 1)) = n + 1 by LAPLACE:def 7;
thus eval P,x = Sum ((LaplaceExpL (A + (x * B)),(n + 1)) | (n + 1)) by A22
.= Sum (LaplaceExpL (A + (x * B)),(n + 1)) by A23, FINSEQ_1:79
.= Det (A + (x * B)) by A3, LAPLACE:25 ; :: thesis: verum

end;

A24: S₁[ 0 ]

proof

let A, B be Matrix of 0 ,K; :: thesis: ex P being Polynomial of K st
( len P <= 0 + 1 & ( for x being Element of K holds eval P,x = Det (A + (x * B)) ) )
take P = 1_. K; :: thesis: ( len P <= 0 + 1 & ( for x being Element of K holds eval P,x = Det (A + (x * B)) ) )
thus len P <= 0 + 1 by POLYNOM4:7; :: thesis: for x being Element of K holds eval P,x = Det (A + (x * B))
let x be Element of K; :: thesis: eval P,x = Det (A + (x * B))
thus Det (A + (x * B)) = 1_ K by MATRIXR2:41
.= eval P,x by POLYNOM4:21 ; :: thesis: verum

end;

for n being Nat holds S₁[n] from NAT_1:sch 2(A24, A1);
hence for A, B being Matrix of n,K ex P being Polynomial of K st
( len P <= n + 1 & ( for x being Element of K holds eval P,x = Det (A + (x * B)) ) ) ; :: thesis: verum