let A, B be Ring; for x being Element of A
for p being Polynomial of A st A is Subring of B holds
Ext_eval (p,(In (x,B))) = In ((eval (p,x)),B)
let x be Element of A; for p being Polynomial of A st A is Subring of B holds
Ext_eval (p,(In (x,B))) = In ((eval (p,x)),B)
let p be Polynomial of A; ( A is Subring of B implies Ext_eval (p,(In (x,B))) = In ((eval (p,x)),B) )
assume A0:
A is Subring of B
; Ext_eval (p,(In (x,B))) = In ((eval (p,x)),B)
consider F1 being FinSequence of B such that
A1:
Ext_eval (p,(In (x,B))) = Sum F1
and
A2:
len F1 = len p
and
A3:
for n being Element of NAT st n in dom F1 holds
F1 . n = (In ((p . (n -' 1)),B)) * ((power B) . ((In (x,B)),(n -' 1)))
by Def1;
consider F2 being FinSequence of A such that
A4:
eval (p,x) = Sum F2
and
A5:
len F2 = len p
and
A6:
for n being Element of NAT st n in dom F2 holds
F2 . n = (p . (n -' 1)) * ((power A) . (x,(n -' 1)))
by POLYNOM4:def 2;
F1 = F2
proof
A11:
rng F2 c= the
carrier of
A
;
A8:
dom F1 = dom F2
by A2, A5, FINSEQ_3:29;
for
k being
Nat st
k in dom F1 holds
F1 . k = F2 . k
proof
let k be
Nat;
( k in dom F1 implies F1 . k = F2 . k )
assume A10:
k in dom F1
;
F1 . k = F2 . k
then
F2 . k is
Element of
A
by A8, FUNCT_1:3, A11;
then A13:
F2 . k is
Element of
B
by A0, Lm6;
F1 . k =
(In ((p . (k -' 1)),B)) * ((power B) . ((In (x,B)),(k -' 1)))
by A3, A10
.=
In (
((p . (k -' 1)) * ((power A) . (x,(k -' 1)))),
B)
by A0, Th15
.=
In (
(F2 . k),
B)
by A6, A10, A8
.=
F2 . k
by A13, SUBSET_1:def 8
;
hence
F1 . k = F2 . k
;
verum
end;
hence
F1 = F2
by A2, A5, FINSEQ_3:29;
verum
end;
hence
Ext_eval (p,(In (x,B))) = In ((eval (p,x)),B)
by A1, A4, A0, Th14; verum