let L be non degenerated comRing; :: thesis: for x being Element of L
for n being Element of NAT
for p being Polynomial of L st n < len p holds
eval (poly_shift p,n),x = (x * (eval (poly_shift p,(n + 1)),x)) + (p . n)
let x be Element of L; :: thesis: for n being Element of NAT
for p being Polynomial of L st n < len p holds
eval (poly_shift p,n),x = (x * (eval (poly_shift p,(n + 1)),x)) + (p . n)
let n be Element of NAT ; :: thesis: for p being Polynomial of L st n < len p holds
eval (poly_shift p,n),x = (x * (eval (poly_shift p,(n + 1)),x)) + (p . n)
let p be Polynomial of L; :: thesis: ( n < len p implies eval (poly_shift p,n),x = (x * (eval (poly_shift p,(n + 1)),x)) + (p . n) )
assume A1:
n < len p
; :: thesis: eval (poly_shift p,n),x = (x * (eval (poly_shift p,(n + 1)),x)) + (p . n)
A2:
1_ L = 1. L
;
set ps = poly_shift p,n;
set ps1 = poly_shift p,(n + 1);
consider f being FinSequence of L such that
A3:
eval (poly_shift p,n),x = Sum f
and
A4:
len f = len (poly_shift p,n)
and
A5:
for k being Element of NAT st k in dom f holds
f . k = ((poly_shift p,n) . (k -' 1)) * ((power L) . x,(k -' 1))
by POLYNOM4:def 2;
consider f1 being FinSequence of L such that
A6:
eval (poly_shift p,(n + 1)),x = Sum f1
and
A7:
len f1 = len (poly_shift p,(n + 1))
and
A8:
for k being Element of NAT st k in dom f1 holds
f1 . k = ((poly_shift p,(n + 1)) . (k -' 1)) * ((power L) . x,(k -' 1))
by POLYNOM4:def 2;
A9:
x * (Sum f1) = Sum (x * f1)
by FVSUM_1:92;
A10:
x * f1 = (x multfield ) * f1
by FVSUM_1:def 6;
( rng f1 c= the carrier of L & dom (x multfield ) = the carrier of L )
by FUNCT_2:def 1;
then A11:
dom ((x multfield ) * f1) = dom f1
by RELAT_1:46;
now thus
len f = len f
;
:: thesis: ( len (<*(p . n)*> ^ (x * f1)) = len f & ( for j being Nat st j in dom f holds
f . b2 = (<*(p . n)*> ^ (x * f1)) . b2 ) )A12:
n + 1
<= len p
by A1, NAT_1:13;
A13:
((len (poly_shift p,(n + 1))) + 1) + n =
(len (poly_shift p,(n + 1))) + (n + 1)
.=
len p
by A12, Th46
.=
(len (poly_shift p,n)) + n
by A1, Th46
;
A14:
len <*(p . n)*> = 1
by FINSEQ_1:57;
A15:
len (x * f1) = len f1
by A10, A11, FINSEQ_3:31;
hence
len (<*(p . n)*> ^ (x * f1)) = len f
by A4, A7, A13, A14, FINSEQ_1:35;
:: thesis: for j being Nat st j in dom f holds
f . b2 = (<*(p . n)*> ^ (x * f1)) . b2let j be
Nat;
:: thesis: ( j in dom f implies f . b1 = (<*(p . n)*> ^ (x * f1)) . b1 )assume A16:
j in dom f
;
:: thesis: f . b1 = (<*(p . n)*> ^ (x * f1)) . b1A18:
( 1
<= j &
j <= len f )
by A16, FINSEQ_3:27;
per cases
( j = 1 or 1 < j )
by A18, XXREAL_0:1;
suppose A19:
j = 1
;
:: thesis: f . b1 = (<*(p . n)*> ^ (x * f1)) . b1A20:
1
in dom <*(p . n)*>
by A14, FINSEQ_3:27;
thus f . j =
((poly_shift p,n) . (1 -' 1)) * ((power L) . x,(1 -' 1))
by A5, A16, A19
.=
((poly_shift p,n) . 0 ) * ((power L) . x,(1 -' 1))
by XREAL_1:234
.=
((poly_shift p,n) . 0 ) * ((power L) . x,0 )
by XREAL_1:234
.=
((poly_shift p,n) . 0 ) * (1. L)
by A2, GROUP_1:def 8
.=
(poly_shift p,n) . 0
by A2, GROUP_1:def 5
.=
p . (n + 0 )
by Def6
.=
<*(p . n)*> . 1
by FINSEQ_1:57
.=
(<*(p . n)*> ^ (x * f1)) . j
by A19, A20, FINSEQ_1:def 7
;
:: thesis: verum end; suppose
1
< j
;
:: thesis: f . b1 = (<*(p . n)*> ^ (x * f1)) . b1then A21:
1
+ 1
<= j
by NAT_1:13;
1
- 1
<= j - 1
by A18, XREAL_1:11;
then reconsider j1 =
j - 1 as
Element of
NAT by INT_1:16;
A22:
(1 + 1) - 1
<= j - 1
by A21, XREAL_1:11;
j - 1
<= ((len f1) + 1) - 1
by A4, A7, A13, A18, XREAL_1:11;
then A23:
j1 in dom f1
by A22, FINSEQ_3:27;
then reconsider f1j =
f1 . j1 as
Element of
L by FINSEQ_2:13;
j = j1 + 1
;
then A24:
j1 = j -' 1
by NAT_D:34;
consider j2 being
Nat such that A25:
j1 = j2 + 1
by A22, NAT_1:6;
A26:
(j1 -' 1) + 1
= j1
by A25, NAT_D:34;
thus f . j =
((poly_shift p,n) . (j -' 1)) * ((power L) . x,(j -' 1))
by A5, A16
.=
(p . (n + j1)) * ((power L) . x,j1)
by A24, Def6
.=
(p . ((n + 1) + (j1 -' 1))) * (((power L) . x,(j1 -' 1)) * x)
by A26, GROUP_1:def 8
.=
x * ((p . ((n + 1) + (j1 -' 1))) * ((power L) . x,(j1 -' 1)))
by GROUP_1:def 4
.=
x * (((poly_shift p,(n + 1)) . (j1 -' 1)) * ((power L) . x,(j1 -' 1)))
by Def6
.=
x * f1j
by A8, A23
.=
(x * f1) . j1
by A10, A11, A23, FVSUM_1:62
.=
(<*(p . n)*> ^ (x * f1)) . j
by A4, A7, A13, A14, A15, A18, A21, FINSEQ_1:36
;
:: thesis: verum end; end;
then
f = <*(p . n)*> ^ (x * f1)
by FINSEQ_2:10;
hence
eval (poly_shift p,n),x = (x * (eval (poly_shift p,(n + 1)),x)) + (p . n)
by A3, A6, A9, FVSUM_1:89; :: thesis: verum