let L be domRing; :: thesis: for x being Element of L
for p, q being non-zero Polynomial of L holds multiplicity (p *' q),x = (multiplicity p,x) + (multiplicity q,x)
let x be Element of L; :: thesis: for p, q being non-zero Polynomial of L holds multiplicity (p *' q),x = (multiplicity p,x) + (multiplicity q,x)
let p, q be non-zero Polynomial of L; :: thesis: multiplicity (p *' q),x = (multiplicity p,x) + (multiplicity q,x)
set r = <%(- x),(1. L)%>;
consider F being non empty finite Subset of NAT such that
A1:
F = { k where k is Element of NAT : ex pqq being Polynomial of L st p *' q = (<%(- x),(1. L)%> `^ k) *' pqq }
and
A2:
multiplicity (p *' q),x = max F
by Def8;
consider f being non empty finite Subset of NAT such that
A3:
f = { k where k is Element of NAT : ex pq being Polynomial of L st p = (<%(- x),(1. L)%> `^ k) *' pq }
and
A4:
multiplicity p,x = max f
by Def8;
consider g being non empty finite Subset of NAT such that
A5:
g = { k where k is Element of NAT : ex qq being Polynomial of L st q = (<%(- x),(1. L)%> `^ k) *' qq }
and
A6:
multiplicity q,x = max g
by Def8;
max F in F
by XXREAL_2:def 8;
then consider k being Element of NAT such that
A7:
k = max F
and
A8:
ex pqq being Polynomial of L st p *' q = (<%(- x),(1. L)%> `^ k) *' pqq
by A1;
consider pqq being Polynomial of L such that
A9:
p *' q = (<%(- x),(1. L)%> `^ k) *' pqq
by A8;
max f in f
by XXREAL_2:def 8;
then consider i being Element of NAT such that
A10:
i = max f
and
A11:
ex pq being Polynomial of L st p = (<%(- x),(1. L)%> `^ i) *' pq
by A3;
consider pq being Polynomial of L such that
A12:
p = (<%(- x),(1. L)%> `^ i) *' pq
by A11;
max g in g
by XXREAL_2:def 8;
then consider j being Element of NAT such that
A13:
j = max g
and
A14:
ex qq being Polynomial of L st q = (<%(- x),(1. L)%> `^ j) *' qq
by A5;
consider qq being Polynomial of L such that
A15:
q = (<%(- x),(1. L)%> `^ j) *' qq
by A14;
A16: p *' q =
(((<%(- x),(1. L)%> `^ i) *' pq) *' (<%(- x),(1. L)%> `^ j)) *' qq
by A12, A15, POLYNOM3:34
.=
(((<%(- x),(1. L)%> `^ i) *' (<%(- x),(1. L)%> `^ j)) *' pq) *' qq
by POLYNOM3:34
.=
((<%(- x),(1. L)%> `^ (i + j)) *' pq) *' qq
by Th32
.=
(<%(- x),(1. L)%> `^ (i + j)) *' (pq *' qq)
by POLYNOM3:34
;
then
i + j in F
by A1;
then A17:
i + j <= k
by A7, XXREAL_2:def 8;
now assume
i + j < k
;
:: thesis: contradictionthen
0 + (i + j) < k
;
then A18:
0 < k - (i + j)
by XREAL_1:22;
then reconsider kij =
k - (i + j) as
Element of
NAT by INT_1:16;
consider kk being
Nat such that A19:
kij = kk + 1
by A18, NAT_1:6;
reconsider kk =
kk as
Element of
NAT by ORDINAL1:def 13;
(
(0_. L) . 1
= 0. L &
<%(- x),(1. L)%> . 1
= 1. L )
by FUNCOP_1:13, POLYNOM5:39;
then A20:
<%(- x),(1. L)%> `^ (i + j) <> 0_. L
by Th31;
k = kij + (i + j)
;
then A21:
p *' q =
((<%(- x),(1. L)%> `^ (i + j)) *' (<%(- x),(1. L)%> `^ kij)) *' pqq
by A9, Th32
.=
(<%(- x),(1. L)%> `^ (i + j)) *' ((<%(- x),(1. L)%> `^ kij) *' pqq)
by POLYNOM3:34
;
<%(- x),(1. L)%> `^ kij =
(<%(- x),(1. L)%> `^ 1) *' (<%(- x),(1. L)%> `^ kk)
by A19, Th32
.=
<%(- x),(1. L)%> *' (<%(- x),(1. L)%> `^ kk)
by POLYNOM5:17
;
then
(<%(- x),(1. L)%> `^ kij) *' pqq = <%(- x),(1. L)%> *' ((<%(- x),(1. L)%> `^ kk) *' pqq)
by POLYNOM3:34;
then
x is_a_root_of pq *' qq
by A16, A20, A21, Th30, Th51;
then
x in Roots (pq *' qq)
by POLYNOM5:def 9;
then A22:
x in (Roots pq) \/ (Roots qq)
by Th25;
per cases
( x in Roots pq or x in Roots qq )
by A22, XBOOLE_0:def 3;
suppose
x in Roots pq
;
:: thesis: contradictionthen
x is_a_root_of pq
by POLYNOM5:def 9;
then
pq = <%(- x),(1. L)%> *' (poly_quotient pq,x)
by Th52;
then p =
((<%(- x),(1. L)%> `^ i) *' <%(- x),(1. L)%>) *' (poly_quotient pq,x)
by A12, POLYNOM3:34
.=
((<%(- x),(1. L)%> `^ i) *' (<%(- x),(1. L)%> `^ 1)) *' (poly_quotient pq,x)
by POLYNOM5:17
.=
(<%(- x),(1. L)%> `^ (i + 1)) *' (poly_quotient pq,x)
by Th32
;
then
i + 1
in f
by A3;
then
i + 1
<= i
by A10, XXREAL_2:def 8;
hence
contradiction
by NAT_1:13;
:: thesis: verum end; suppose
x in Roots qq
;
:: thesis: contradictionthen
x is_a_root_of qq
by POLYNOM5:def 9;
then
qq = <%(- x),(1. L)%> *' (poly_quotient qq,x)
by Th52;
then q =
((<%(- x),(1. L)%> `^ j) *' <%(- x),(1. L)%>) *' (poly_quotient qq,x)
by A15, POLYNOM3:34
.=
((<%(- x),(1. L)%> `^ j) *' (<%(- x),(1. L)%> `^ 1)) *' (poly_quotient qq,x)
by POLYNOM5:17
.=
(<%(- x),(1. L)%> `^ (j + 1)) *' (poly_quotient qq,x)
by Th32
;
then
j + 1
in g
by A5;
then
j + 1
<= j
by A13, XXREAL_2:def 8;
hence
contradiction
by NAT_1:13;
:: thesis: verum end; end;
hence
multiplicity (p *' q),x = (multiplicity p,x) + (multiplicity q,x)
by A2, A4, A6, A7, A10, A13, A17, XXREAL_0:1; :: thesis: verum