let R be domRing; for B being bag of the carrier of R st card (support B) = 1 holds
ex p being Ppoly of R st
( deg p = card B & ( for a being Element of R holds multiplicity (p,a) = B . a ) )
let B be bag of the carrier of R; ( card (support B) = 1 implies ex p being Ppoly of R st
( deg p = card B & ( for a being Element of R holds multiplicity (p,a) = B . a ) ) )
assume
card (support B) = 1
; ex p being Ppoly of R st
( deg p = card B & ( for a being Element of R holds multiplicity (p,a) = B . a ) )
then consider x being object such that
A1:
support B = {x}
by CARD_2:42;
x in support B
by A1, TARSKI:def 1;
then reconsider a = x as Element of the carrier of R ;
reconsider q = rpoly (1,a) as Element of (Polynom-Ring R) by POLYNOM3:def 10;
deffunc H1( set ) -> Element of (Polynom-Ring R) = q;
consider F being FinSequence of (Polynom-Ring R) such that
A2:
( len F = B . a & ( for k being Nat st k in dom F holds
F . k = H1(k) ) )
from FINSEQ_2:sch 1();
reconsider F = F as non empty FinSequence of (Polynom-Ring R) by A1, A2, bb7;
reconsider p = Product F as Polynomial of R by POLYNOM3:def 10;
AS:
B = ({a},(B . a)) -bag
by A1, bb7;
A3:
for i being Nat st i in dom F holds
ex a being Element of R st F . i = rpoly (1,a)
by A2;
then reconsider p = p as Ppoly of R by dpp1;
take
p
; ( deg p = card B & ( for a being Element of R holds multiplicity (p,a) = B . a ) )
thus deg p =
B . a
by A2, A3, lemppoly
.=
card B
by AS, bb4
; for a being Element of R holds multiplicity (p,a) = B . a
A5:
(rpoly (1,a)) `^ (B . a) = p
by lempolybag1, A2;
now for o being Element of R holds multiplicity (p,o) = B . olet o be
Element of
R;
multiplicity (p,b1) = B . b1per cases
( o = a or o <> a )
;
suppose C:
o = a
;
multiplicity (p,b1) = B . b1
(rpoly (1,a)) `^ (B . a) = ((rpoly (1,a)) `^ (B . a)) *' (1_. R)
;
then B:
(rpoly (1,a)) `^ (B . a) divides p
by A5, RING_4:1;
E:
(rpoly (1,a)) `^ (B . a) <> 0_. R
;
(rpoly (1,a)) `^ ((B . a) + 1) = ((rpoly (1,a)) `^ (B . a)) *' (rpoly (1,a))
by POLYNOM5:19;
then deg ((rpoly (1,a)) `^ ((B . a) + 1)) =
(deg ((rpoly (1,a)) `^ (B . a))) + (deg (rpoly (1,a)))
by E, HURWITZ:23
.=
(deg ((rpoly (1,a)) `^ (B . a))) + 1
by HURWITZ:27
;
then
deg ((rpoly (1,a)) `^ ((B . a) + 1)) > deg ((rpoly (1,a)) `^ (B . a))
by XREAL_1:29;
hence
multiplicity (
p,
o)
= B . o
by C, B, A5, prl25, multip;
verum end; end;
hence
for a being Element of R holds multiplicity (p,a) = B . a
; verum