let R be Ring; for S being RingExtension of R
for a being Element of S
for p being constant Polynomial of R holds Ext_eval (p,a) = LC p
let S be RingExtension of R; for a being Element of S
for p being constant Polynomial of R holds Ext_eval (p,a) = LC p
let a be Element of S; for p being constant Polynomial of R holds Ext_eval (p,a) = LC p
let p be constant Polynomial of R; Ext_eval (p,a) = LC p
A:
R is Subring of S
by FIELD_4:def 1;
per cases
( p = 0_. R or p <> 0_. R )
;
suppose A0:
p <> 0_. R
;
Ext_eval (p,a) = LC p
the
carrier of
R c= the
carrier of
S
by A, C0SP1:def 3;
then reconsider p0 =
p . 0 as
Element of
S ;
consider F being
FinSequence of
S such that A1:
Ext_eval (
p,
a)
= Sum F
and A2:
len F = len p
and A3:
for
n being
Element of
NAT st
n in dom F holds
F . n = (In ((p . (n -' 1)),S)) * ((power S) . (a,(n -' 1)))
by ALGNUM_1:def 1;
reconsider degp =
deg p as
Element of
NAT by A0, FIELD_1:1;
A7:
degp = 0
by RATFUNC1:def 2;
A6:
deg p = (len p) - 1
by HURWITZ:def 2;
then A4:
F . 1 =
(In ((p . (1 -' 1)),S)) * ((power S) . (a,(1 -' 1)))
by A7, A2, A3, FINSEQ_3:25
.=
(In ((p . 0),S)) * ((power S) . (a,(1 -' 1)))
by XREAL_1:232
.=
p0 * ((power S) . (a,0))
by XREAL_1:232
.=
p0 * (1_ S)
by GROUP_1:def 7
.=
p0
;
Sum F =
Sum <*p0*>
by A6, A7, A2, FINSEQ_1:40, A4
.=
p . (1 - 1)
by RLVECT_1:44
.=
p . (1 -' 1)
by XREAL_0:def 2
.=
LC p
by A6, A7, RATFUNC1:def 6
;
hence
Ext_eval (
p,
a)
= LC p
by A1;
verum