set g = PolyHom h;
set RP = Polynom-Ring R;
set SP = Polynom-Ring S;
reconsider 1RP = 1_ (Polynom-Ring R) as Element of the carrier of (Polynom-Ring R) ;
reconsider 1SP = 1_ (Polynom-Ring S) as Element of the carrier of (Polynom-Ring S) ;
hence
PolyHom h is additive
; ( PolyHom h is multiplicative & PolyHom h is unity-preserving )
now for a, b being Element of the carrier of (Polynom-Ring R) holds (PolyHom h) . (a * b) = ((PolyHom h) . a) * ((PolyHom h) . b)let a,
b be
Element of the
carrier of
(Polynom-Ring R);
(PolyHom h) . (a * b) = ((PolyHom h) . a) * ((PolyHom h) . b)reconsider ab =
a * b as
Element of the
carrier of
(Polynom-Ring R) ;
reconsider gab =
((PolyHom h) . a) * ((PolyHom h) . b) as
Element of the
carrier of
(Polynom-Ring S) ;
reconsider a1 =
a,
b1 =
b as
sequence of
R ;
reconsider ab1 =
a1 *' b1 as
sequence of
R ;
reconsider ga =
(PolyHom h) . a,
gb =
(PolyHom h) . b as
Element of the
carrier of
(Polynom-Ring S) ;
reconsider ga1 =
ga,
gb1 =
gb as
sequence of
S ;
set gab1 =
ga1 *' gb1;
now for m being Element of NAT holds ((PolyHom h) . (a * b)) . m = gab . mlet m be
Element of
NAT ;
((PolyHom h) . (a * b)) . m = gab . mconsider r being
FinSequence of the
carrier of
R such that A1:
(
len r = m + 1 &
ab1 . m = Sum r & ( for
k being
Element of
NAT st
k in dom r holds
r . k = (a1 . (k -' 1)) * (b1 . ((m + 1) -' k)) ) )
by POLYNOM3:def 9;
consider s being
FinSequence of the
carrier of
S such that A2:
(
len s = m + 1 &
(ga1 *' gb1) . m = Sum s & ( for
k being
Element of
NAT st
k in dom s holds
s . k = (ga1 . (k -' 1)) * (gb1 . ((m + 1) -' k)) ) )
by POLYNOM3:def 9;
A5:
dom r =
Seg (m + 1)
by A1, FINSEQ_1:def 3
.=
dom s
by A2, FINSEQ_1:def 3
;
A3:
for
k being
Element of
NAT st
k in dom r holds
h . (r . k) = s . k
reconsider m1 =
m + 1 as
Element of
NAT ;
A6:
1
<= m + 1
by NAT_1:11;
defpred S1[
Nat]
means h . (Sum (r | R)) = Sum (s | R);
A7:
S1[1]
proof
A8:
len (r | 1) = 1
by A1, NAT_1:11, FINSEQ_1:59;
A9:
dom (r | 1) = Seg 1
by A1, A6, FINSEQ_1:17;
then
(r | 1) . 1
in rng (r | 1)
by FINSEQ_1:3, FUNCT_1:3;
then reconsider a =
(r | 1) . 1 as
Element of the
carrier of
R ;
r | 1
= <*a*>
by A8, FINSEQ_1:40;
then A11:
h . (Sum (r | 1)) = h . a
by RLVECT_1:44;
A12:
len (s | 1) = 1
by A2, NAT_1:11, FINSEQ_1:59;
A13:
dom (s | 1) = Seg 1
by A2, A6, FINSEQ_1:17;
then
(s | 1) . 1
in rng (s | 1)
by FINSEQ_1:3, FUNCT_1:3;
then reconsider b =
(s | 1) . 1 as
Element of the
carrier of
S ;
A15:
s | 1
= <*b*>
by A12, FINSEQ_1:40;
A16:
dom r = Seg (m + 1)
by A1, FINSEQ_1:def 3;
A17:
1
in dom (s | (Seg 1))
by A13;
1
in dom (r | (Seg 1))
by A9;
then h . a =
h . (r . 1)
by FUNCT_1:47
.=
s . 1
by A16, A3, A6, FINSEQ_1:1
.=
b
by A17, FUNCT_1:47
;
hence
S1[1]
by A11, A15, RLVECT_1:44;
verum
end; A19:
now for j being Element of NAT st 1 <= j & j < m1 & S1[j] holds
S1[j + 1]let j be
Element of
NAT ;
( 1 <= j & j < m1 & S1[j] implies S1[j + 1] )assume A20:
( 1
<= j &
j < m1 )
;
( S1[j] implies S1[j + 1] )assume A21:
S1[
j]
;
S1[j + 1]A22:
j + 1
<= m + 1
by A20, NAT_1:13;
then A23:
len (r | (j + 1)) = j + 1
by A1, FINSEQ_1:59;
A24:
r | (Seg j) = r | j
;
then reconsider rj =
r | (Seg j) as
FinSequence of
R ;
(r | (j + 1)) | j = r | j
by NAT_1:11, FINSEQ_1:82;
then consider q being
FinSequence such that A25:
r | (j + 1) = rj ^ q
by FINSEQ_1:80;
a26:
1
<= j + 1
by NAT_1:11;
then A27:
r . (j + 1) in rng r
by FUNCT_1:3, A1, A22, FINSEQ_3:25;
A28:
j + 1 =
len (r | (j + 1))
by A22, A1, FINSEQ_1:59
.=
(len rj) + (len q)
by A25, FINSEQ_1:22
.=
j + (len q)
by A20, A24, A1, FINSEQ_1:59
;
then
dom q = Seg 1
by FINSEQ_1:def 3;
then A29:
1
in dom q
;
A30:
len (r | j) = j
by A20, A1, FINSEQ_1:59;
then A31:
(r | (j + 1)) . (j + 1) = q . 1
by A25, A29, FINSEQ_1:def 7;
dom (r | (j + 1)) = Seg (j + 1)
by A23, FINSEQ_1:def 3;
then A32:
r . (j + 1) = (r | (j + 1)) . (j + 1)
by FUNCT_1:47, FINSEQ_1:3;
then reconsider a =
q . 1 as
Element of
R by A30, A27, A25, A29, FINSEQ_1:def 7;
A33:
h . a = s . (j + 1)
by A31, A32, a26, A3, A1, A22, FINSEQ_3:25;
q = <*a*>
by A28, FINSEQ_1:40;
then h . (Sum (r | (j + 1))) =
(h . (Sum rj)) + (h . a)
by A25, Th17
.=
(Sum (s | j)) + (Sum <*(h . a)*>)
by RLVECT_1:44, A21
.=
Sum ((s | j) ^ <*(h . a)*>)
by RLVECT_1:41
.=
Sum (s | (j + 1))
by A20, A2, A33, FINSEQ_5:83
;
hence
S1[
j + 1]
;
verum end; A34:
for
i being
Element of
NAT st 1
<= i &
i <= m1 holds
S1[
i]
from INT_1:sch 7(A7, A19);
A35:
Sum s =
Sum (s | (m + 1))
by A2, FINSEQ_1:58
.=
h . (Sum (r | (m + 1)))
by A34, A6
.=
h . (Sum r)
by A1, FINSEQ_1:58
;
a1 *' b1 = a * b
by POLYNOM3:def 10;
then
((PolyHom h) . (a * b)) . m = (ga1 *' gb1) . m
by A35, A2, A1, Def2;
hence
((PolyHom h) . (a * b)) . m = gab . m
by POLYNOM3:def 10;
verum end; hence
(PolyHom h) . (a * b) = ((PolyHom h) . a) * ((PolyHom h) . b)
by FUNCT_2:63;
verum end;
hence
PolyHom h is multiplicative
; PolyHom h is unity-preserving
hence
PolyHom h is unity-preserving
by FUNCT_2:63; verum