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)));
H: multiplicity (p,a) <= multiplicity (p,(@ (a,E))) by multi3a;
consider P being non empty finite Subset of NAT such that
A1: ( P = { k where k is Element of NAT : ex r being Polynomial of F st p = (<%(- a),(1. F)%> `^ k) *' r } & multiplicity (p,a) = max P ) by UPROOTS:def 8;
multiplicity (p,(@ (a,E))) = multiplicity (q,(@ (a,E))) by FIELD_14:def 6;
then B: (X- (@ (a,E))) `^ (multiplicity (p,(@ (a,E)))) divides q by FIELD_14:67;
D: ( (X- (@ (a,E))) `^ (multiplicity (p,(@ (a,E)))) is Element of the carrier of (Polynom-Ring E) & q is Element of the carrier of (Polynom-Ring E) & (X- a) `^ (multiplicity (p,(@ (a,E)))) 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),(1. F)%> = rpoly (1,a) & @ (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,E)))) = (X- (@ (a,E))) `^ (multiplicity (p,(@ (a,E)))) by FIELD_14:18;
then (X- a) `^ (multiplicity (p,(@ (a,E)))) divides p by B, D, FIELD_14:48;
then consider r being Polynomial of F such that
D: (<%(- a),(1. F)%> `^ (multiplicity (p,(@ (a,E))))) *' r = p by C, RING_4:1;
multiplicity (p,(@ (a,E))) in P by D, A1;
then multiplicity (p,(@ (a,E))) <= multiplicity (p,a) by A1, XXREAL_2:def 8;
hence multiplicity (p,a) = multiplicity (p,(@ (a,E))) by H, XXREAL_0:1; :: thesis: verum