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