let F be Field; :: thesis: for p being non zero Polynomial of F
for E being FieldExtension of F
for a being Element of F holds multiplicity (p,a) <= multiplicity (p,(@ (a,E)))
let p be non zero Polynomial of F; :: thesis: for E being FieldExtension of F
for a being Element of F holds multiplicity (p,a) <= multiplicity (p,(@ (a,E)))
let E be FieldExtension of F; :: thesis: for a being Element of F holds multiplicity (p,a) <= multiplicity (p,(@ (a,E)))
let a be Element of F; :: thesis: multiplicity (p,a) <= multiplicity (p,(@ (a,E)))
reconsider q = p as Polynomial of E by FIELD_4:8;
p <> 0_. F ;
then q <> 0_. E by FIELD_4:12;
then reconsider q = q as non zero Polynomial of E by UPROOTS:def 5;
set np = multiplicity (p,a);
set nq = multiplicity (p,(@ (a,E)));
consider Q being non empty finite Subset of NAT such that
A: ( Q = { k where k is Element of NAT : ex r being Polynomial of E st q = (<%(- (@ (a,E))),(1. E)%> `^ k) *' r } & multiplicity (q,(@ (a,E))) = max Q ) by UPROOTS:def 8;
B: (X- a) `^ (multiplicity (p,a)) divides p by FIELD_14:67;
D: ( (X- (@ (a,E))) `^ (multiplicity (p,a)) is Element of the carrier of (Polynom-Ring E) & q is Element of the carrier of (Polynom-Ring E) & (X- a) `^ (multiplicity (p,a)) is Element of the carrier of (Polynom-Ring F) & p is Element of the carrier of (Polynom-Ring F) ) by POLYNOM3:def 10;
C: ( <%(- (@ (a,E))),(1. E)%> = rpoly (1,(@ (a,E))) & X- a = rpoly (1,a) & X- (@ (a,E)) = rpoly (1,(@ (a,E))) & @ (a,E) = a ) by FIELD_7:def 4, RING_5:10;
then X- a = X- (@ (a,E)) by FIELD_4:21;
then (X- a) `^ (multiplicity (p,a)) = (X- (@ (a,E))) `^ (multiplicity (p,a)) by FIELD_14:18;
then (X- (@ (a,E))) `^ (multiplicity (p,a)) divides q by B, D, FIELD_14:48;
then consider r being Polynomial of E such that
D: (<%(- (@ (a,E))),(1. E)%> `^ (multiplicity (p,a))) *' r = q by C, RING_4:1;
multiplicity (p,a) in Q by D, A;
then multiplicity (p,a) <= multiplicity (q,(@ (a,E))) by A, XXREAL_2:def 8;
hence multiplicity (p,a) <= multiplicity (p,(@ (a,E))) by FIELD_14:def 6; :: thesis: verum