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:4;
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:87;
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_0:24;
(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:39;
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:7;
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:6; :: 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_0:24;
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 3
.= ((A * ((n + 1),(m + 1))) + ((B * ((n + 1),(m + 1))) * x)) * ((power K) . ((- (1_ K)),((m + 1) + (n + 1)))) by VECTSP_1:def 2
.= ((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:10;
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:24
.= (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:44
.= ((A + (x * B)) * ((n + 1),(m + 1))) * (Cofactor ((A + (x * B)),(n + 1),(m + 1))) by GROUP_1:def 3
.= (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:71
.= (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:19 ;
:: 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:3; :: 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:43
.= eval (P,x) by POLYNOM4:17 ;
:: 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:58
.= 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:4; :: 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:18 ; :: 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