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 S1[ 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:
S1[ 0 ]
A2:
for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be
Nat;
:: thesis: ( S1[n] implies S1[n + 1] )
assume A3:
S1[
n]
;
:: thesis: S1[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)) ) )
A4:
n + 1
in Seg (n + 1)
by FINSEQ_1:6;
defpred S2[
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) ) ) );
A5:
S2[
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;
A6:
for
m being
Nat st
S2[
m] holds
S2[
m + 1]
proof
let m be
Nat;
:: thesis: ( S2[m] implies S2[m + 1] )
assume A7:
S2[
m]
;
:: thesis: S2[m + 1]
set m1 =
m + 1;
assume A8:
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 A9:
len P <= (n + 1) + 1
and A10:
for
x being
Element of
K holds
eval P,
x = Sum ((LaplaceExpL (A + (x * B)),(n + 1)) | m)
by A7, NAT_1:13;
set DA =
Delete A,
(n + 1),
(m + 1);
set DB =
Delete B,
(n + 1),
(m + 1);
(n + 1) -' 1
= n
by NAT_D:34;
then consider P1 being
Polynomial of
K such that A11:
len P1 <= n + 1
and A12:
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 A3;
set pow =
(power K) . (- (1_ K)),
((m + 1) + (n + 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))))%>;
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 A11, XREAL_1:9;
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))))%>)) -' 1
<= ((n + 1) + 2) -' 1 &
((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, NAT_D:42;
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 XXREAL_0:2;
hence
len PP <= (n + 1) + 1
by A9, 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);
( 1
<= m + 1 &
n + 1
= len (LaplaceExpL (A + (x * B)),(n + 1)) )
by LAPLACE:def 7, NAT_1:11;
then A13:
(
m + 1
in Seg (n + 1) &
dom (LaplaceExpL (A + (x * B)),(n + 1)) = Seg (n + 1) )
by A8, FINSEQ_1:def 3;
then A14:
(
[(n + 1),(m + 1)] in [:(Seg (n + 1)),(Seg (n + 1)):] &
Indices B = [:(Seg (n + 1)),(Seg (n + 1)):] &
Indices A = [:(Seg (n + 1)),(Seg (n + 1)):] )
by A4, MATRIX_1:25, ZFMISC_1:106;
A15:
((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 A14, MATRIX_3:def 5
.=
((A + (x * B)) * (n + 1),(m + 1)) * ((power K) . (- (1_ K)),((m + 1) + (n + 1)))
by A14, MATRIX_3:def 3
;
A16:
(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 A4, A13, Th5
.=
Delete (A + (x * B)),
(n + 1),
(m + 1)
by A4, A13, Th4
;
A17:
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 A12
.=
(Minor (A + (x * B)),(n + 1),(m + 1)) * (((A + (x * B)) * (n + 1),(m + 1)) * ((power K) . (- (1_ K)),((m + 1) + (n + 1))))
by A15, A16, 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 A13, LAPLACE:def 7
;
(LaplaceExpL (A + (x * B)),(n + 1)) | (m + 1) = ((LaplaceExpL (A + (x * B)),(n + 1)) | m) ^ <*((LaplaceExpL (A + (x * B)),(n + 1)) . (m + 1))*>
by A13, FINSEQ_5:11;
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 A17, 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 A10
.=
eval PP,
x
by POLYNOM4:22
;
:: thesis: verum
end;
for
m being
Nat holds
S2[
m]
from NAT_1:sch 2(A5, A6);
then consider P being
Polynomial of
K such that A18:
len P <= (n + 1) + 1
and A19:
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 A18;
:: 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))
A20:
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 A19
.=
Sum (LaplaceExpL (A + (x * B)),(n + 1))
by A20, FINSEQ_1:79
.=
Det (A + (x * B))
by A4, LAPLACE:25
;
:: thesis: verum
end;
for n being Nat holds S1[n]
from NAT_1:sch 2(A1, A2);
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