let n be Nat; for K being Field
for A 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 * (1. K,n))) ) )
let K be Field; for A 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 * (1. K,n))) ) )
defpred S1[ Nat] means for A 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 * (1. K,$1))) ) );
A1:
for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be
Nat;
( S1[n] implies S1[n + 1] )
assume A2:
S1[
n]
;
S1[n + 1]
set n1 =
n + 1;
let A be
Matrix of
n + 1,
K;
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 * (1. K,(n + 1)))) ) )
set ONE =
1. K,
(n + 1);
A3:
Indices (1. K,(n + 1)) = Indices A
by MATRIX_1:27;
defpred S2[
Nat]
means ( 1
<= $1 & $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 * (1. K,(n + 1)))),1) | $1) ) ) );
A4:
(n + 1) -' 1
= n
by NAT_D:34;
A5:
1
<= n + 1
by NAT_1:11;
then A6:
1
in Seg (n + 1)
;
A7:
Indices A = [:(Seg (n + 1)),(Seg (n + 1)):]
by MATRIX_1:25;
A8:
for
k being
Nat st
S2[
k] holds
S2[
k + 1]
proof
let k be
Nat;
( S2[k] implies S2[k + 1] )
assume A9:
S2[
k]
;
S2[k + 1]
set k1 =
k + 1;
assume that A10:
1
<= k + 1
and A11:
k + 1
<= n + 1
;
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 * (1. K,(n + 1)))),1) | (k + 1)) ) )
set pow =
(power K) . (- (1_ K)),
((k + 1) + 1);
set P2 =
<%((A * 1,(k + 1)) * ((power K) . (- (1_ K)),((k + 1) + 1))),(((1. K,(n + 1)) * 1,(k + 1)) * ((power K) . (- (1_ K)),((k + 1) + 1)))%>;
A12:
k + 1
in Seg (n + 1)
by A10, A11;
then A13:
[1,(k + 1)] in Indices A
by A7, A6, ZFMISC_1:106;
per cases
( k = 0 or k >= 1 )
by NAT_1:14;
suppose A14:
k = 0
;
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 * (1. K,(n + 1)))),1) | (k + 1)) ) )then (power K) . (- (1_ K)),
((k + 1) + 1) =
(- (1_ K)) * (- (1_ K))
by GROUP_1:99
.=
(1_ K) * (1_ K)
by VECTSP_1:42
.=
1_ K
by VECTSP_1:def 13
;
then A15:
((1. K,(n + 1)) * 1,(k + 1)) * ((power K) . (- (1_ K)),((k + 1) + 1)) =
(1_ K) * (1_ K)
by A3, A13, A14, MATRIX_1:def 12
.=
1_ K
by VECTSP_1:def 13
;
then A16:
( 2
-' 1
= 2
- 1 &
<%((A * 1,(k + 1)) * ((power K) . (- (1_ K)),((k + 1) + 1))),(((1. K,(n + 1)) * 1,(k + 1)) * ((power K) . (- (1_ K)),((k + 1) + 1)))%> . 1
<> 0. K )
by POLYNOM5:39, XREAL_1:235;
((1. K,(n + 1)) * 1,(k + 1)) * ((power K) . (- (1_ K)),((k + 1) + 1)) <> 0. K
by A15;
then A17:
len <%((A * 1,(k + 1)) * ((power K) . (- (1_ K)),((k + 1) + 1))),(((1. K,(n + 1)) * 1,(k + 1)) * ((power K) . (- (1_ K)),((k + 1) + 1)))%> = 2
by POLYNOM5:41;
consider P being
Polynomial of
K such that A18:
len P = n + 1
and A19:
for
x being
Element of
K holds
eval P,
x = Det ((Delete A,1,1) + (x * (1. K,n)))
by A2, A4;
take PP =
<%((A * 1,(k + 1)) * ((power K) . (- (1_ K)),((k + 1) + 1))),(((1. K,(n + 1)) * 1,(k + 1)) * ((power K) . (- (1_ K)),((k + 1) + 1)))%> *' P;
( len PP = (n + 1) + 1 & ( for x being Element of K holds eval PP,x = Sum ((LaplaceExpL (A + (x * (1. K,(n + 1)))),1) | (k + 1)) ) )
P . n <> 0. K
by A18, ALGSEQ_1:25;
then
(<%((A * 1,(k + 1)) * ((power K) . (- (1_ K)),((k + 1) + 1))),(((1. K,(n + 1)) * 1,(k + 1)) * ((power K) . (- (1_ K)),((k + 1) + 1)))%> . ((len <%((A * 1,(k + 1)) * ((power K) . (- (1_ K)),((k + 1) + 1))),(((1. K,(n + 1)) * 1,(k + 1)) * ((power K) . (- (1_ K)),((k + 1) + 1)))%>) -' 1)) * (P . ((len P) -' 1)) <> 0. K
by A4, A18, A17, A16, VECTSP_1:44;
hence len PP =
((n + 1) + 2) - 1
by A18, A17, POLYNOM4:13
.=
(n + 1) + 1
;
for x being Element of K holds eval PP,x = Sum ((LaplaceExpL (A + (x * (1. K,(n + 1)))),1) | (k + 1))let x be
Element of
K;
eval PP,x = Sum ((LaplaceExpL (A + (x * (1. K,(n + 1)))),1) | (k + 1))A20:
(Delete A,1,1) + (x * (1. K,n)) =
(Delete A,1,1) + (x * (Delete (1. K,(n + 1)),1,1))
by A6, A4, Th6
.=
(Delete A,1,1) + (Delete (x * (1. K,(n + 1))),1,1)
by A12, A14, Th5
.=
Delete (A + (x * (1. K,(n + 1)))),1,1
by A6, Th4
;
A21:
((A * 1,(k + 1)) * ((power K) . (- (1_ K)),((k + 1) + 1))) + ((((1. K,(n + 1)) * 1,(k + 1)) * ((power K) . (- (1_ K)),((k + 1) + 1))) * x) =
((A * 1,(k + 1)) * ((power K) . (- (1_ K)),((k + 1) + 1))) + ((((1. K,(n + 1)) * 1,(k + 1)) * x) * ((power K) . (- (1_ K)),((k + 1) + 1)))
by GROUP_1:def 4
.=
((A * 1,(k + 1)) + (((1. K,(n + 1)) * 1,(k + 1)) * x)) * ((power K) . (- (1_ K)),((k + 1) + 1))
by VECTSP_1:def 11
.=
((A * 1,(k + 1)) + ((x * (1. K,(n + 1))) * 1,(k + 1))) * ((power K) . (- (1_ K)),((k + 1) + 1))
by A3, A13, MATRIX_3:def 5
.=
((A + (x * (1. K,(n + 1)))) * 1,(k + 1)) * ((power K) . (- (1_ K)),((k + 1) + 1))
by A13, MATRIX_3:def 3
;
set L =
LaplaceExpL (A + (x * (1. K,(n + 1)))),1;
A22:
dom (LaplaceExpL (A + (x * (1. K,(n + 1)))),1) = Seg (len (LaplaceExpL (A + (x * (1. K,(n + 1)))),1))
by FINSEQ_1:def 3;
A23:
len (LaplaceExpL (A + (x * (1. K,(n + 1)))),1) = n + 1
by LAPLACE:def 7;
A24:
eval (<%((A * 1,(k + 1)) * ((power K) . (- (1_ K)),((k + 1) + 1))),(((1. K,(n + 1)) * 1,(k + 1)) * ((power K) . (- (1_ K)),((k + 1) + 1)))%> *' P),
x =
(eval <%((A * 1,(k + 1)) * ((power K) . (- (1_ K)),((k + 1) + 1))),(((1. K,(n + 1)) * 1,(k + 1)) * ((power K) . (- (1_ K)),((k + 1) + 1)))%>,x) * (eval P,x)
by POLYNOM4:27
.=
(eval <%((A * 1,(k + 1)) * ((power K) . (- (1_ K)),((k + 1) + 1))),(((1. K,(n + 1)) * 1,(k + 1)) * ((power K) . (- (1_ K)),((k + 1) + 1)))%>,x) * (Det ((Delete A,1,1) + (x * (1. K,n))))
by A19
.=
(Minor (A + (x * (1. K,(n + 1)))),1,1) * (((A + (x * (1. K,(n + 1)))) * 1,1) * ((power K) . (- (1_ K)),((k + 1) + 1)))
by A14, A21, A20, POLYNOM5:45
.=
((A + (x * (1. K,(n + 1)))) * 1,1) * (Cofactor (A + (x * (1. K,(n + 1)))),1,1)
by A14, GROUP_1:def 4
.=
(LaplaceExpL (A + (x * (1. K,(n + 1)))),1) . 1
by A6, A22, A23, LAPLACE:def 7
;
thus Sum ((LaplaceExpL (A + (x * (1. K,(n + 1)))),1) | (k + 1)) =
Sum <*((LaplaceExpL (A + (x * (1. K,(n + 1)))),1) /. 1)*>
by A14, A23, CARD_1:47, FINSEQ_5:23
.=
Sum <*(eval (<%((A * 1,(k + 1)) * ((power K) . (- (1_ K)),((k + 1) + 1))),(((1. K,(n + 1)) * 1,(k + 1)) * ((power K) . (- (1_ K)),((k + 1) + 1)))%> *' P),x)*>
by A6, A22, A23, A24, PARTFUN1:def 8
.=
eval PP,
x
by FINSOP_1:12
;
verum end; suppose A25:
k >= 1
;
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 * (1. K,(n + 1)))),1) | (k + 1)) ) )consider P1 being
Polynomial of
K such that A26:
len P1 <= n + 1
and A27:
for
x being
Element of
K holds
eval P1,
x = Det ((Delete A,1,(k + 1)) + (x * (Delete (1. K,(n + 1)),1,(k + 1))))
by A4, Th7;
consider P being
Polynomial of
K such that A28:
len P = (n + 1) + 1
and A29:
for
x being
Element of
K holds
eval P,
x = Sum ((LaplaceExpL (A + (x * (1. K,(n + 1)))),1) | k)
by A9, A11, A25, NAT_1:13;
take PP =
P + (((A * 1,(k + 1)) * ((power K) . (- (1_ K)),((k + 1) + 1))) * P1);
( len PP = (n + 1) + 1 & ( for x being Element of K holds eval PP,x = Sum ((LaplaceExpL (A + (x * (1. K,(n + 1)))),1) | (k + 1)) ) )
(
(A * 1,(k + 1)) * ((power K) . (- (1_ K)),((k + 1) + 1)) = 0. K or
(A * 1,(k + 1)) * ((power K) . (- (1_ K)),((k + 1) + 1)) <> 0. K )
;
then
len (((A * 1,(k + 1)) * ((power K) . (- (1_ K)),((k + 1) + 1))) * P1) <= n + 1
by A26, POLYNOM5:25, POLYNOM5:26;
then A30:
len (((A * 1,(k + 1)) * ((power K) . (- (1_ K)),((k + 1) + 1))) * P1) < len P
by A28, NAT_1:13;
hence len PP =
max (len (((A * 1,(k + 1)) * ((power K) . (- (1_ K)),((k + 1) + 1))) * P1)),
(len P)
by POLYNOM4:10
.=
(n + 1) + 1
by A28, A30, XXREAL_0:def 10
;
for x being Element of K holds eval PP,x = Sum ((LaplaceExpL (A + (x * (1. K,(n + 1)))),1) | (k + 1))let x be
Element of
K;
eval PP,x = Sum ((LaplaceExpL (A + (x * (1. K,(n + 1)))),1) | (k + 1))set L =
LaplaceExpL (A + (x * (1. K,(n + 1)))),1;
A31:
(
dom (LaplaceExpL (A + (x * (1. K,(n + 1)))),1) = Seg (len (LaplaceExpL (A + (x * (1. K,(n + 1)))),1)) &
len (LaplaceExpL (A + (x * (1. K,(n + 1)))),1) = n + 1 )
by FINSEQ_1:def 3, LAPLACE:def 7;
then A32:
(LaplaceExpL (A + (x * (1. K,(n + 1)))),1) | (k + 1) = ((LaplaceExpL (A + (x * (1. K,(n + 1)))),1) | k) ^ <*((LaplaceExpL (A + (x * (1. K,(n + 1)))),1) . (k + 1))*>
by A12, FINSEQ_5:11;
A33:
k + 1
<> 1
by A25, NAT_1:13;
A34:
(A * 1,(k + 1)) * ((power K) . (- (1_ K)),((k + 1) + 1)) =
((A * 1,(k + 1)) + (0. K)) * ((power K) . (- (1_ K)),((k + 1) + 1))
by RLVECT_1:def 7
.=
((A * 1,(k + 1)) + (x * (0. K))) * ((power K) . (- (1_ K)),((k + 1) + 1))
by VECTSP_1:39
.=
((A * 1,(k + 1)) + (x * ((1. K,(n + 1)) * 1,(k + 1)))) * ((power K) . (- (1_ K)),((k + 1) + 1))
by A3, A13, A33, MATRIX_1:def 12
.=
((A * 1,(k + 1)) + ((x * (1. K,(n + 1))) * 1,(k + 1))) * ((power K) . (- (1_ K)),((k + 1) + 1))
by A3, A13, MATRIX_3:def 5
.=
((A + (x * (1. K,(n + 1)))) * 1,(k + 1)) * ((power K) . (- (1_ K)),((k + 1) + 1))
by A13, MATRIX_3:def 3
;
A35:
(Delete A,1,(k + 1)) + (x * (Delete (1. K,(n + 1)),1,(k + 1))) =
(Delete A,1,(k + 1)) + (Delete (x * (1. K,(n + 1))),1,(k + 1))
by A6, A12, Th5
.=
Delete (A + (x * (1. K,(n + 1)))),1,
(k + 1)
by A6, A12, Th4
;
eval (((A * 1,(k + 1)) * ((power K) . (- (1_ K)),((k + 1) + 1))) * P1),
x =
((A * 1,(k + 1)) * ((power K) . (- (1_ K)),((k + 1) + 1))) * (eval P1,x)
by POLYNOM5:31
.=
(Minor (A + (x * (1. K,(n + 1)))),1,(k + 1)) * (((A + (x * (1. K,(n + 1)))) * 1,(k + 1)) * ((power K) . (- (1_ K)),((k + 1) + 1)))
by A27, A34, A35
.=
((A + (x * (1. K,(n + 1)))) * 1,(k + 1)) * (Cofactor (A + (x * (1. K,(n + 1)))),1,(k + 1))
by GROUP_1:def 4
.=
(LaplaceExpL (A + (x * (1. K,(n + 1)))),1) . (k + 1)
by A12, A31, LAPLACE:def 7
;
hence Sum ((LaplaceExpL (A + (x * (1. K,(n + 1)))),1) | (k + 1)) =
(Sum ((LaplaceExpL (A + (x * (1. K,(n + 1)))),1) | k)) + (eval (((A * 1,(k + 1)) * ((power K) . (- (1_ K)),((k + 1) + 1))) * P1),x)
by A32, FVSUM_1:87
.=
(eval P,x) + (eval (((A * 1,(k + 1)) * ((power K) . (- (1_ K)),((k + 1) + 1))) * P1),x)
by A29
.=
eval PP,
x
by POLYNOM4:22
;
verum end;
end;
A36:
S2[
0 ]
;
for
k being
Nat holds
S2[
k]
from NAT_1:sch 2(A36, A8);
then consider P being
Polynomial of
K such that A37:
len P = (n + 1) + 1
and A38:
for
x being
Element of
K holds
eval P,
x = Sum ((LaplaceExpL (A + (x * (1. K,(n + 1)))),1) | (n + 1))
by A5;
take
P
;
( len P = (n + 1) + 1 & ( for x being Element of K holds eval P,x = Det (A + (x * (1. K,(n + 1)))) ) )
thus
len P = (n + 1) + 1
by A37;
for x being Element of K holds eval P,x = Det (A + (x * (1. K,(n + 1))))
let x be
Element of
K;
eval P,x = Det (A + (x * (1. K,(n + 1))))
set L =
LaplaceExpL (A + (x * (1. K,(n + 1)))),1;
len (LaplaceExpL (A + (x * (1. K,(n + 1)))),1) = n + 1
by LAPLACE:def 7;
hence eval P,
x =
Sum ((LaplaceExpL (A + (x * (1. K,(n + 1)))),1) | (len (LaplaceExpL (A + (x * (1. K,(n + 1)))),1)))
by A38
.=
Sum (LaplaceExpL (A + (x * (1. K,(n + 1)))),1)
by FINSEQ_1:79
.=
Det (A + (x * (1. K,(n + 1))))
by A6, LAPLACE:25
;
verum
end;
A39:
S1[ 0 ]
proof
let A be
Matrix of
0 ,
K;
ex P being Polynomial of K st
( len P = 0 + 1 & ( for x being Element of K holds eval P,x = Det (A + (x * (1. K,0 ))) ) )
take P =
1_. K;
( len P = 0 + 1 & ( for x being Element of K holds eval P,x = Det (A + (x * (1. K,0 ))) ) )
thus
len P = 0 + 1
by POLYNOM4:7;
for x being Element of K holds eval P,x = Det (A + (x * (1. K,0 )))
let x be
Element of
K;
eval P,x = Det (A + (x * (1. K,0 )))
thus Det (A + (x * (1. K,0 ))) =
1_ K
by MATRIXR2:41
.=
eval P,
x
by POLYNOM4:21
;
verum
end;
for n being Nat holds S1[n]
from NAT_1:sch 2(A39, A1);
hence
for A 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 * (1. K,n))) ) )
; verum