let L be Field; for a being Element of L
for b being non zero Element of L holds SumRoots <%a,b%> = - (a / b)
let a be Element of L; for b being non zero Element of L holds SumRoots <%a,b%> = - (a / b)
let b be non zero Element of L; SumRoots <%a,b%> = - (a / b)
set p = <%a,b%>;
set B = BRoots <%a,b%>;
A1:
Roots <%a,b%> = {(- (a / b))}
by Th10;
reconsider E = canFS (Roots <%a,b%>) as Enumeration of Roots <%a,b%> by Th2;
set F = (BRoots <%a,b%>) (++) E;
consider g being sequence of L such that
A2:
Sum ((BRoots <%a,b%>) (++) E) = g . (len ((BRoots <%a,b%>) (++) E))
and
A3:
g . 0 = 0. L
and
A4:
for j being Nat
for v being Element of L st j < len ((BRoots <%a,b%>) (++) E) & v = ((BRoots <%a,b%>) (++) E) . (j + 1) holds
g . (j + 1) = (g . j) + v
by RLVECT_1:def 12;
A5:
E = <*(- (a / b))*>
by A1, FINSEQ_1:94;
A6:
len ((BRoots <%a,b%>) (++) E) = len E
by Def1;
A7:
len E = 1
by A5, FINSEQ_1:39;
A8:
1 in dom E
by A7, FINSEQ_3:25;
A9: ((BRoots <%a,b%>) * E) . 1 =
(BRoots <%a,b%>) . (E . 1)
by A8, FUNCT_1:13
.=
multiplicity (<%a,b%>,(- (a / b)))
by A5, UPROOTS:def 9
.=
1
by Th11
;
A10: ((BRoots <%a,b%>) (++) E) . 1 =
(((BRoots <%a,b%>) * E) . 1) * (E /. 1)
by A6, A7, Def1
.=
E /. 1
by A9, BINOM:13
;
then reconsider v = ((BRoots <%a,b%>) (++) E) . 1 as Element of L ;
A11:
0 < len ((BRoots <%a,b%>) (++) E)
by A7, Def1;
thus SumRoots <%a,b%> =
g . (0 + 1)
by A2, A7, Def1
.=
(g . 0) + v
by A4, A11
.=
- (a / b)
by A5, A3, A10, FINSEQ_4:16
; verum