let L be Field; for p being non-zero Polynomial of L
for a being Element of L
for b being non zero Element of L holds SumRoots (<%a,b%> *' p) = (- (a / b)) + (SumRoots p)
let p be non-zero Polynomial of L; for a being Element of L
for b being non zero Element of L holds SumRoots (<%a,b%> *' p) = (- (a / b)) + (SumRoots p)
let a be Element of L; for b being non zero Element of L holds SumRoots (<%a,b%> *' p) = (- (a / b)) + (SumRoots p)
let b be non zero Element of L; SumRoots (<%a,b%> *' p) = (- (a / b)) + (SumRoots p)
set q = <%a,b%>;
set B = BRoots p;
set C = canFS (Roots p);
set E = canFS (Roots (<%a,b%> *' p));
set F = (BRoots (<%a,b%> *' p)) (++) (canFS (Roots (<%a,b%> *' p)));
set G = (BRoots p) (++) (canFS (Roots p));
consider g being sequence of L such that
A1:
SumRoots p = g . (len ((BRoots p) (++) (canFS (Roots p))))
and
A2:
g . 0 = 0. L
and
A3:
for j being Nat
for v being Element of L st j < len ((BRoots p) (++) (canFS (Roots p))) & v = ((BRoots p) (++) (canFS (Roots p))) . (j + 1) holds
g . (j + 1) = (g . j) + v
by RLVECT_1:def 12;
A4:
len ((BRoots p) (++) (canFS (Roots p))) = len (canFS (Roots p))
by Def1;
A5:
len (canFS (Roots p)) = card (Roots p)
by FINSEQ_1:93;
A6:
dom g = NAT
by FUNCT_2:def 1;
per cases
( not - (a / b) in Roots p or - (a / b) in Roots p )
;
suppose A7:
not
- (a / b) in Roots p
;
SumRoots (<%a,b%> *' p) = (- (a / b)) + (SumRoots p)then reconsider N =
(canFS (Roots p)) ^ <*(- (a / b))*> as
Enumeration of
Roots (<%a,b%> *' p) by Th16;
A8:
len N = 1
+ (card (Roots p))
by Th17;
set BN =
(BRoots (<%a,b%> *' p)) (++) N;
A9:
len ((BRoots (<%a,b%> *' p)) (++) N) = len N
by Def1;
A10:
Sum ((BRoots (<%a,b%> *' p)) (++) N) = SumRoots (<%a,b%> *' p)
by A7, Th24;
set f =
g +* (
(1 + (len ((BRoots p) (++) (canFS (Roots p))))),
((- (a / b)) + (SumRoots p)));
A11:
(g +* ((1 + (len ((BRoots p) (++) (canFS (Roots p))))),((- (a / b)) + (SumRoots p)))) . 0 = g . 0
by FUNCT_7:32;
A12:
(g +* ((1 + (len ((BRoots p) (++) (canFS (Roots p))))),((- (a / b)) + (SumRoots p)))) . (len ((BRoots (<%a,b%> *' p)) (++) N)) = (- (a / b)) + (SumRoots p)
by A5, A9, A8, A4, A6, FUNCT_7:31;
now for j being Nat
for v being Element of L st j < len ((BRoots (<%a,b%> *' p)) (++) N) & v = ((BRoots (<%a,b%> *' p)) (++) N) . (j + 1) holds
(g +* ((1 + (len ((BRoots p) (++) (canFS (Roots p))))),((- (a / b)) + (SumRoots p)))) . (j + 1) = ((g +* ((1 + (len ((BRoots p) (++) (canFS (Roots p))))),((- (a / b)) + (SumRoots p)))) . j) + vlet j be
Nat;
for v being Element of L st j < len ((BRoots (<%a,b%> *' p)) (++) N) & v = ((BRoots (<%a,b%> *' p)) (++) N) . (j + 1) holds
(g +* ((1 + (len ((BRoots p) (++) (canFS (Roots p))))),((- (a / b)) + (SumRoots p)))) . (b2 + 1) = ((g +* ((1 + (len ((BRoots p) (++) (canFS (Roots p))))),((- (a / b)) + (SumRoots p)))) . b2) + b3let v be
Element of
L;
( j < len ((BRoots (<%a,b%> *' p)) (++) N) & v = ((BRoots (<%a,b%> *' p)) (++) N) . (j + 1) implies (g +* ((1 + (len ((BRoots p) (++) (canFS (Roots p))))),((- (a / b)) + (SumRoots p)))) . (b1 + 1) = ((g +* ((1 + (len ((BRoots p) (++) (canFS (Roots p))))),((- (a / b)) + (SumRoots p)))) . b1) + b2 )assume that A13:
j < len ((BRoots (<%a,b%> *' p)) (++) N)
and A14:
v = ((BRoots (<%a,b%> *' p)) (++) N) . (j + 1)
;
(g +* ((1 + (len ((BRoots p) (++) (canFS (Roots p))))),((- (a / b)) + (SumRoots p)))) . (b1 + 1) = ((g +* ((1 + (len ((BRoots p) (++) (canFS (Roots p))))),((- (a / b)) + (SumRoots p)))) . b1) + b2reconsider C =
canFS (Roots p) as
Enumeration of
Roots p by Th2;
A15:
(g +* ((1 + (len ((BRoots p) (++) (canFS (Roots p))))),((- (a / b)) + (SumRoots p)))) . j = g . j
by A5, A9, A8, A4, A13, FUNCT_7:32;
A16:
j + 1
<= len ((BRoots (<%a,b%> *' p)) (++) N)
by A13, NAT_1:13;
then A17:
((BRoots (<%a,b%> *' p)) (++) N) . (j + 1) = (((BRoots (<%a,b%> *' p)) * N) . (j + 1)) * (N /. (j + 1))
by Def1, NAT_1:11;
A18:
j + 1
in dom N
by A9, A16, NAT_1:11, FINSEQ_3:25;
then A19:
N . (j + 1) = N /. (j + 1)
by PARTFUN1:def 6;
A20:
multiplicity (
(<%a,b%> *' p),
(N /. (j + 1)))
= (multiplicity (<%a,b%>,(N /. (j + 1)))) + (multiplicity (p,(N /. (j + 1))))
by UPROOTS:55;
j <= len ((BRoots p) (++) (canFS (Roots p)))
by A5, A9, A8, A4, A13, NAT_1:13;
per cases then
( j < len ((BRoots p) (++) (canFS (Roots p))) or j = len ((BRoots p) (++) (canFS (Roots p))) )
by XXREAL_0:1;
suppose A21:
j < len ((BRoots p) (++) (canFS (Roots p)))
;
(g +* ((1 + (len ((BRoots p) (++) (canFS (Roots p))))),((- (a / b)) + (SumRoots p)))) . (b1 + 1) = ((g +* ((1 + (len ((BRoots p) (++) (canFS (Roots p))))),((- (a / b)) + (SumRoots p)))) . b1) + b2then
j + 1
< 1
+ (len ((BRoots p) (++) (canFS (Roots p))))
by XREAL_1:8;
then A22:
(g +* ((1 + (len ((BRoots p) (++) (canFS (Roots p))))),((- (a / b)) + (SumRoots p)))) . (j + 1) = g . (j + 1)
by FUNCT_7:32;
A23:
j + 1
<= len ((BRoots p) (++) (canFS (Roots p)))
by A21, NAT_1:13;
A24:
j + 1
in dom C
by A4, A23, NAT_1:11, FINSEQ_3:25;
then A25:
C . (j + 1) = C /. (j + 1)
by PARTFUN1:def 6;
A26:
N /. (j + 1) = C /. (j + 1)
by A4, A5, A23, A19, A25, Th17, NAT_1:11;
then A30:
multiplicity (
<%a,b%>,
(N /. (j + 1)))
= 0
by NAT_1:14, UPROOTS:52;
A31:
((BRoots (<%a,b%> *' p)) * N) . (j + 1) =
(BRoots (<%a,b%> *' p)) . (N . (j + 1))
by A18, FUNCT_1:13
.=
multiplicity (
(<%a,b%> *' p),
(N /. (j + 1)))
by A19, UPROOTS:def 9
.=
(BRoots p) . (C . (j + 1))
by A25, A26, A20, A30, UPROOTS:def 9
.=
((BRoots p) * C) . (j + 1)
by A24, FUNCT_1:13
;
((BRoots (<%a,b%> *' p)) (++) N) . (j + 1) = ((BRoots p) (++) (canFS (Roots p))) . (j + 1)
by A23, A26, A31, A17, Def1, NAT_1:11;
hence
(g +* ((1 + (len ((BRoots p) (++) (canFS (Roots p))))),((- (a / b)) + (SumRoots p)))) . (j + 1) = ((g +* ((1 + (len ((BRoots p) (++) (canFS (Roots p))))),((- (a / b)) + (SumRoots p)))) . j) + v
by A21, A3, A14, A15, A22;
verum end; suppose A32:
j = len ((BRoots p) (++) (canFS (Roots p)))
;
(g +* ((1 + (len ((BRoots p) (++) (canFS (Roots p))))),((- (a / b)) + (SumRoots p)))) . (b1 + 1) = ((g +* ((1 + (len ((BRoots p) (++) (canFS (Roots p))))),((- (a / b)) + (SumRoots p)))) . b1) + b2then A33:
(g +* ((1 + (len ((BRoots p) (++) (canFS (Roots p))))),((- (a / b)) + (SumRoots p)))) . (j + 1) = (- (a / b)) + (SumRoots p)
by A6, FUNCT_7:31;
A34:
((BRoots (<%a,b%> *' p)) * N) . (j + 1) = (BRoots (<%a,b%> *' p)) . (N . (j + 1))
by A18, FUNCT_1:13;
not
- (a / b) is_a_root_of p
by A7, POLYNOM5:def 10;
then A35:
multiplicity (
p,
(- (a / b)))
= 0
by NAT_1:14, UPROOTS:52;
(BRoots (<%a,b%> *' p)) . (N . (j + 1)) =
(multiplicity (<%a,b%>,(- (a / b)))) + (multiplicity (p,(- (a / b))))
by A4, A19, A20, A32, UPROOTS:def 9
.=
1
by A35, Th11
;
hence
(g +* ((1 + (len ((BRoots p) (++) (canFS (Roots p))))),((- (a / b)) + (SumRoots p)))) . (j + 1) = ((g +* ((1 + (len ((BRoots p) (++) (canFS (Roots p))))),((- (a / b)) + (SumRoots p)))) . j) + v
by A1, A4, A14, A15, A17, A19, A32, A33, A34, BINOM:13;
verum end; end; end; hence
SumRoots (<%a,b%> *' p) = (- (a / b)) + (SumRoots p)
by A2, A12, A11, A10, RLVECT_1:def 12;
verum end; suppose A36:
- (a / b) in Roots p
;
SumRoots (<%a,b%> *' p) = (- (a / b)) + (SumRoots p)
Roots <%a,b%> = {(- (a / b))}
by Th10;
then A37:
Roots p =
(Roots <%a,b%>) \/ (Roots p)
by A36, XBOOLE_1:12, ZFMISC_1:31
.=
Roots (<%a,b%> *' p)
by UPROOTS:23
;
reconsider E =
canFS (Roots (<%a,b%> *' p)) as
Enumeration of
Roots (<%a,b%> *' p) by Th2;
A38:
len ((BRoots p) (++) E) = len E
by Def1;
A39:
Sum ((BRoots <%a,b%>) (++) E) = - (a / b)
by Th25;
len ((BRoots <%a,b%>) (++) E) = len E
by Def1;
then A40:
(BRoots <%a,b%>) (++) E is
Element of
(len E) -tuples_on the
carrier of
L
by FINSEQ_2:92;
A41:
(BRoots p) (++) E is
Element of
(len E) -tuples_on the
carrier of
L
by A38, FINSEQ_2:92;
BRoots (<%a,b%> *' p) = (BRoots <%a,b%>) + (BRoots p)
by UPROOTS:56;
hence SumRoots (<%a,b%> *' p) =
Sum (((BRoots <%a,b%>) (++) E) + ((BRoots p) (++) E))
by Th19
.=
(- (a / b)) + (SumRoots p)
by A37, A39, A40, A41, FVSUM_1:76
;
verum end; end;