let L be Field; for p, q being Polynomial of L
for x being Element of L holds eval ((Subst (p,q)),x) = eval (p,(eval (q,x)))
let p, q be Polynomial of L; for x being Element of L holds eval ((Subst (p,q)),x) = eval (p,(eval (q,x)))
let x be Element of L; eval ((Subst (p,q)),x) = eval (p,(eval (q,x)))
consider F1 being FinSequence of the carrier of L such that
A1:
eval (p,(eval (q,x))) = Sum F1
and
A2:
len F1 = len p
and
A3:
for n being Element of NAT st n in dom F1 holds
F1 . n = (p . (n -' 1)) * ((power L) . ((eval (q,x)),(n -' 1)))
by POLYNOM4:def 2;
consider F being FinSequence of the carrier of (Polynom-Ring L) such that
A4:
Subst (p,q) = Sum F
and
A5:
len F = len p
and
A6:
for n being Element of NAT st n in dom F holds
F . n = (p . (n -' 1)) * (q `^ (n -' 1))
by Def6;
defpred S1[ Nat] means for r being Polynomial of L st r = Sum (F | $1) holds
eval (r,x) = Sum (F1 | $1);
A7:
for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be
Nat;
( S1[n] implies S1[n + 1] )
reconsider nn =
n as
Element of
NAT by ORDINAL1:def 12;
assume A8:
for
r being
Polynomial of
L st
r = Sum (F | n) holds
eval (
r,
x)
= Sum (F1 | n)
;
S1[n + 1]
let r be
Polynomial of
L;
( r = Sum (F | (n + 1)) implies eval (r,x) = Sum (F1 | (n + 1)) )
assume A9:
r = Sum (F | (n + 1))
;
eval (r,x) = Sum (F1 | (n + 1))
per cases
( n + 1 <= len F or n + 1 > len F )
;
suppose A10:
n + 1
<= len F
;
eval (r,x) = Sum (F1 | (n + 1))then A11:
F1 | (n + 1) = (F1 | n) ^ <*(F1 /. (n + 1))*>
by A5, A2, FINSEQ_5:82;
F | (n + 1) = (F | n) ^ <*(F /. (n + 1))*>
by A10, FINSEQ_5:82;
then A12:
r = (Sum (F | n)) + (F /. (n + 1))
by A9, FVSUM_1:71;
reconsider r1 =
Sum (F | n) as
Polynomial of
L by POLYNOM3:def 10;
n + 1
>= 1
by NAT_1:11;
then A13:
n + 1
in dom F
by A10, FINSEQ_3:25;
A14:
dom F = dom F1
by A5, A2, FINSEQ_3:29;
then A15:
(p . ((n + 1) -' 1)) * ((power L) . ((eval (q,x)),((n + 1) -' 1))) =
F1 . (n + 1)
by A3, A13
.=
F1 /. (n + 1)
by A13, A14, PARTFUN1:def 6
;
F /. (n + 1) =
F . (n + 1)
by A13, PARTFUN1:def 6
.=
(p . ((n + 1) -' 1)) * (q `^ ((n + 1) -' 1))
by A6, A13
.=
(p . nn) * (q `^ ((n + 1) -' 1))
by NAT_D:34
.=
(p . nn) * (q `^ n)
by NAT_D:34
;
then
r = r1 + ((p . nn) * (q `^ n))
by A12, POLYNOM3:def 10;
hence eval (
r,
x) =
(eval (r1,x)) + (eval (((p . nn) * (q `^ n)),x))
by POLYNOM4:19
.=
(Sum (F1 | n)) + (eval (((p . nn) * (q `^ n)),x))
by A8
.=
(Sum (F1 | n)) + ((p . nn) * (eval ((q `^ n),x)))
by Th30
.=
(Sum (F1 | n)) + ((p . nn) * ((power L) . ((eval (q,x)),n)))
by Th22
.=
(Sum (F1 | n)) + ((p . ((n + 1) -' 1)) * ((power L) . ((eval (q,x)),n)))
by NAT_D:34
.=
(Sum (F1 | n)) + (F1 /. (n + 1))
by A15, NAT_D:34
.=
Sum (F1 | (n + 1))
by A11, FVSUM_1:71
;
verum end;
end;
A18:
( F | (len F) = F & F1 | (len F1) = F1 )
by FINSEQ_1:58;
A19:
S1[ 0 ]
for n being Nat holds S1[n]
from NAT_1:sch 2(A19, A7);
hence
eval ((Subst (p,q)),x) = eval (p,(eval (q,x)))
by A4, A5, A1, A2, A18; verum