let L be domRing; 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; 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; 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 Def7;
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 Def7;
max f in f
by XXREAL_2:def 8;
then consider i being Element of NAT such that
A5:
i = max f
and
A6:
ex pq being Polynomial of L st p = (<%(- x),(1. L)%> `^ i) *' pq
by A3;
consider pq being Polynomial of L such that
A7:
p = (<%(- x),(1. L)%> `^ i) *' pq
by A6;
consider g being non empty finite Subset of NAT such that
A8:
g = { k where k is Element of NAT : ex qq being Polynomial of L st q = (<%(- x),(1. L)%> `^ k) *' qq }
and
A9:
multiplicity (q,x) = max g
by Def7;
max F in F
by XXREAL_2:def 8;
then consider k being Element of NAT such that
A10:
k = max F
and
A11:
ex pqq being Polynomial of L st p *' q = (<%(- x),(1. L)%> `^ k) *' pqq
by A1;
consider pqq being Polynomial of L such that
A12:
p *' q = (<%(- x),(1. L)%> `^ k) *' pqq
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 A8;
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 A7, A15, POLYNOM3:33
.=
(((<%(- x),(1. L)%> `^ i) *' (<%(- x),(1. L)%> `^ j)) *' pq) *' qq
by POLYNOM3:33
.=
((<%(- x),(1. L)%> `^ (i + j)) *' pq) *' qq
by Th27
.=
(<%(- x),(1. L)%> `^ (i + j)) *' (pq *' qq)
by POLYNOM3:33
;
A17:
now not i + j < kassume
i + j < k
;
contradictionthen
0 + (i + j) < k
;
then A18:
0 < k - (i + j)
by XREAL_1:20;
then reconsider kij =
k - (i + j) as
Element of
NAT by INT_1:3;
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 12;
<%(- x),(1. L)%> `^ kij =
(<%(- x),(1. L)%> `^ 1) *' (<%(- x),(1. L)%> `^ kk)
by A19, Th27
.=
<%(- x),(1. L)%> *' (<%(- x),(1. L)%> `^ kk)
by POLYNOM5:16
;
then A20:
(<%(- x),(1. L)%> `^ kij) *' pqq = <%(- x),(1. L)%> *' ((<%(- x),(1. L)%> `^ kk) *' pqq)
by POLYNOM3:33;
(
(0_. L) . 1
= 0. L &
<%(- x),(1. L)%> . 1
= 1. L )
by FUNCOP_1:7, POLYNOM5:38;
then A21:
<%(- x),(1. L)%> `^ (i + j) <> 0_. L
by Th26;
k = kij + (i + j)
;
then p *' q =
((<%(- x),(1. L)%> `^ (i + j)) *' (<%(- x),(1. L)%> `^ kij)) *' pqq
by A12, Th27
.=
(<%(- x),(1. L)%> `^ (i + j)) *' ((<%(- x),(1. L)%> `^ kij) *' pqq)
by POLYNOM3:33
;
then
x is_a_root_of pq *' qq
by A16, A21, A20, Th25, Th46;
then
x in Roots (pq *' qq)
by POLYNOM5:def 10;
then A22:
x in (Roots pq) \/ (Roots qq)
by Th20;
per cases
( x in Roots pq or x in Roots qq )
by A22, XBOOLE_0:def 3;
suppose
x in Roots pq
;
contradictionthen
x is_a_root_of pq
by POLYNOM5:def 10;
then
pq = <%(- x),(1. L)%> *' (poly_quotient (pq,x))
by Th47;
then p =
((<%(- x),(1. L)%> `^ i) *' <%(- x),(1. L)%>) *' (poly_quotient (pq,x))
by A7, POLYNOM3:33
.=
((<%(- x),(1. L)%> `^ i) *' (<%(- x),(1. L)%> `^ 1)) *' (poly_quotient (pq,x))
by POLYNOM5:16
.=
(<%(- x),(1. L)%> `^ (i + 1)) *' (poly_quotient (pq,x))
by Th27
;
then
i + 1
in f
by A3;
then
i + 1
<= i
by A5, XXREAL_2:def 8;
hence
contradiction
by NAT_1:13;
verum end; suppose
x in Roots qq
;
contradictionthen
x is_a_root_of qq
by POLYNOM5:def 10;
then
qq = <%(- x),(1. L)%> *' (poly_quotient (qq,x))
by Th47;
then q =
((<%(- x),(1. L)%> `^ j) *' <%(- x),(1. L)%>) *' (poly_quotient (qq,x))
by A15, POLYNOM3:33
.=
((<%(- x),(1. L)%> `^ j) *' (<%(- x),(1. L)%> `^ 1)) *' (poly_quotient (qq,x))
by POLYNOM5:16
.=
(<%(- x),(1. L)%> `^ (j + 1)) *' (poly_quotient (qq,x))
by Th27
;
then
j + 1
in g
by A8;
then
j + 1
<= j
by A13, XXREAL_2:def 8;
hence
contradiction
by NAT_1:13;
verum end; end;
i + j in F
by A1, A16;
then
i + j <= k
by A10, XXREAL_2:def 8;
hence
multiplicity ((p *' q),x) = (multiplicity (p,x)) + (multiplicity (q,x))
by A2, A4, A9, A10, A5, A13, A17, XXREAL_0:1; verum