let R be Ring; for S being R -homomorphic Ring
for h being Homomorphism of R,S
for p, L being Element of the carrier of (Polynom-Ring R) st L = LM p holds
for a being Element of R holds h . (eval ((LM p),a)) = eval (((PolyHom h) . L),(h . a))
let S be R -homomorphic Ring; for h being Homomorphism of R,S
for p, L being Element of the carrier of (Polynom-Ring R) st L = LM p holds
for a being Element of R holds h . (eval ((LM p),a)) = eval (((PolyHom h) . L),(h . a))
let h be Homomorphism of R,S; for p, L being Element of the carrier of (Polynom-Ring R) st L = LM p holds
for a being Element of R holds h . (eval ((LM p),a)) = eval (((PolyHom h) . L),(h . a))
let p, L be Element of the carrier of (Polynom-Ring R); ( L = LM p implies for a being Element of R holds h . (eval ((LM p),a)) = eval (((PolyHom h) . L),(h . a)) )
assume A1:
L = LM p
; for a being Element of R holds h . (eval ((LM p),a)) = eval (((PolyHom h) . L),(h . a))
let a be Element of R; h . (eval ((LM p),a)) = eval (((PolyHom h) . L),(h . a))
per cases
( p = 0_. R or p <> 0_. R )
;
suppose A4:
p <> 0_. R
;
h . (eval ((LM p),a)) = eval (((PolyHom h) . L),(h . a))set f =
PolyHom h;
reconsider q =
(PolyHom h) . L as
Polynomial of
S ;
consider F being
FinSequence of the
carrier of
R such that A5:
(
eval (
(LM p),
a)
= Sum F &
len F = len (LM p) & ( for
n being
Element of
NAT st
n in dom F holds
F . n = ((LM p) . (n -' 1)) * ((power R) . (a,(n -' 1))) ) )
by POLYNOM4:def 2;
A6:
Sum F =
(p . ((len p) -' 1)) * ((power R) . (a,((len p) -' 1)))
by A5, POLYNOM4:22
.=
((LM p) . ((len p) -' 1)) * ((power R) . (a,((len p) -' 1)))
by POLYNOM4:def 1
;
consider G being
FinSequence of the
carrier of
S such that A7:
(
eval (
q,
(h . a))
= Sum G &
len G = len q & ( for
n being
Element of
NAT st
n in dom G holds
G . n = (q . (n -' 1)) * ((power S) . ((h . a),(n -' 1))) ) )
by POLYNOM4:def 2;
A8:
len q <= len L
by Lm2;
A9:
len G <= len F
by A1, A5, A7, Lm2;
A10:
len F = len p
by A5, POLYNOM4:15;
then A11:
len F <> 0
by A4, POLYNOM4:5;
then A12:
0 + 1
<= len F
by NAT_1:13;
A13:
(len p) -' 1
= (len p) - 1
by A11, A10, XREAL_0:def 2;
A15:
for
n being
Element of
NAT st
n in dom G holds
n in dom F
A16:
for
n being
Element of
NAT st
n in dom G holds
h . (F . n) = G . n
A18:
for
n being
Element of
NAT st
n in dom G &
n <> len p holds
G /. n = 0. S
per cases
( len G = len F or len G < len F )
by A9, XXREAL_0:1;
suppose A21:
len G = len F
;
h . (eval ((LM p),a)) = eval (((PolyHom h) . L),(h . a))then A22:
len G in dom G
by A12, FINSEQ_3:25;
Sum G =
G /. (len G)
by A18, A21, A10, POLYNOM2:3, A12, FINSEQ_3:25
.=
G . (len G)
by A22, PARTFUN1:def 6
.=
h . (F . (len F))
by A12, FINSEQ_3:25, A16, A21
.=
h . (Sum F)
by A6, FINSEQ_3:25, A12, A5, A10
;
hence
h . (eval ((LM p),a)) = eval (
((PolyHom h) . L),
(h . a))
by A5, A7;
verum end; suppose A23:
len G < len F
;
h . (eval ((LM p),a)) = eval (((PolyHom h) . L),(h . a))then 0. S =
h . (L . ((len L) -' 1))
by A7, A5, A1, Lm3
.=
h . (L . ((len p) -' 1))
by A1, POLYNOM4:15
.=
h . (p . ((len p) -' 1))
by A1, POLYNOM4:def 1
;
then A24:
0. S =
(h . (p . ((len p) -' 1))) * (h . ((power R) . (a,((len p) -' 1))))
.=
h . ((p . ((len p) -' 1)) * ((power R) . (a,((len p) -' 1))))
by GROUP_6:def 6
.=
h . (eval ((LM p),a))
by POLYNOM4:22
;
hence
h . (eval ((LM p),a)) = eval (
((PolyHom h) . L),
(h . a))
by A24, A7, POLYNOM3:1;
verum end; end; end; end;