let L be algebraic-closed domRing; for p being non-zero Polynomial of L
for r being FinSequence of L st r is one-to-one & len r = (len p) -' 1 & Roots p = rng r holds
Sum r = SumRoots p
let p be non-zero Polynomial of L; for r being FinSequence of L st r is one-to-one & len r = (len p) -' 1 & Roots p = rng r holds
Sum r = SumRoots p
let r be FinSequence of L; ( r is one-to-one & len r = (len p) -' 1 & Roots p = rng r implies Sum r = SumRoots p )
assume that
A1:
r is one-to-one
and
A2:
len r = (len p) -' 1
and
A3:
Roots p = rng r
; Sum r = SumRoots p
set B = BRoots p;
set s = support (BRoots p);
set L1 = (len r) |-> 1;
consider f being FinSequence of NAT such that
A4:
( degree (BRoots p) = Sum f & f = (BRoots p) * (canFS (support (BRoots p))) )
by UPROOTS:def 4;
A5:
degree (BRoots p) = (len p) -' 1
by UPROOTS:59;
A6:
( card (dom r) = card (rng r) & dom r = Seg (len r) )
by A1, CARD_1:70, FINSEQ_1:def 3;
A7:
support (BRoots p) = Roots p
by UPROOTS:def 9;
A8:
( support (BRoots p) c= dom (BRoots p) & rng (canFS (support (BRoots p))) = support (BRoots p) )
by PRE_POLY:37, FUNCT_2:def 3;
then A9:
dom f = dom (canFS (support (BRoots p)))
by A4, RELAT_1:27;
then A10:
( len f = len (canFS (support (BRoots p))) & len (canFS (support (BRoots p))) = card (support (BRoots p)) )
by FINSEQ_3:29, FINSEQ_1:93;
then A11:
len f = len r
by A3, A6, UPROOTS:def 9;
A12:
f is len r -element
by A10, A6, A7, A3, CARD_1:def 7;
reconsider E = canFS (support (BRoots p)) as FinSequence of L by A8, FINSEQ_1:def 4;
A13:
dom f = dom r
by A10, A6, A7, A3, FINSEQ_3:29;
A14:
for j being Nat st j in Seg (len r) holds
f . j >= ((len r) |-> 1) . j
proof
let j be
Nat;
( j in Seg (len r) implies f . j >= ((len r) |-> 1) . j )
assume A15:
j in Seg (len r)
;
f . j >= ((len r) |-> 1) . j
A16:
(canFS (support (BRoots p))) . j in support (BRoots p)
by A13, A9, A6, A8, A15, FUNCT_1:def 3;
then reconsider c =
E . j as
Element of
L ;
c is_a_root_of p
by A16, A7, POLYNOM5:def 10;
then
multiplicity (
p,
c)
>= 1
by UPROOTS:52;
then
(BRoots p) . c >= 1
by UPROOTS:def 9;
then
f . j >= 1
by A13, A6, A4, A15, FUNCT_1:12;
hence
f . j >= ((len r) |-> 1) . j
by A15, FINSEQ_2:57;
verum
end;
A17:
Sum ((len r) |-> 1) = 1 * (len r)
by RVSUM_1:80;
A18:
len ((BRoots p) (++) E) = len E
by Def1;
for j being Nat st 1 <= j & j <= len E holds
((BRoots p) (++) E) . j = E . j
proof
let j be
Nat;
( 1 <= j & j <= len E implies ((BRoots p) (++) E) . j = E . j )
assume A19:
( 1
<= j &
j <= len E )
;
((BRoots p) (++) E) . j = E . j
A20:
j in Seg (len r)
by A19, A11, A10;
then
(
f . j >= ((len r) |-> 1) . j &
f . j <= ((len r) |-> 1) . j &
((len r) |-> 1) . j = 1 )
by A2, A14, A12, A17, A4, A5, RVSUM_1:83, FINSEQ_2:57;
then A21:
f . j = 1
by XXREAL_0:1;
A22:
E /. j = E . j
by A20, A13, A9, A6, PARTFUN1:def 6;
((BRoots p) (++) E) . j = (f . j) * (E /. j)
by A4, A19, A18, Def1;
hence
((BRoots p) (++) E) . j = E . j
by BINOM:13, A21, A22;
verum
end;
then A23:
(BRoots p) (++) E = E
by A18, FINSEQ_1:14;
E,r are_fiberwise_equipotent
by A1, A3, A8, UPROOTS:def 9, RFINSEQ:26;
then
ex P being Permutation of (dom E) st E = r * P
by CLASSES1:80, A13, A9;
hence
Sum r = SumRoots p
by A23, RLVECT_2:7, A13, A9, A7; verum