:: Vieta's Formula about the Sum of Roots of Polynomials
:: by Artur Korni{\l}owicz and Karol P\kak
::
:: Received May 25, 2017
:: Copyright (c) 2017-2021 Association of Mizar Users


Lm1: 2 -' 1 = 2 - 1
by XREAL_0:def 2;

Lm2: 2 -' 2 = 2 - 2
by XREAL_0:def 2;

registration
let F be FinSequence;
let f be Function of (dom F),(dom F);
cluster f * F -> FinSequence-like ;
coherence
F * f is FinSequence-like by FINSEQ_2:40;
end;

theorem :: POLYVIE1:1
for a, b being object holds
( not a <> b or canFS {a,b} = <*a,b*> or canFS {a,b} = <*b,a*> )
proof end;

theorem Th2: :: POLYVIE1:2
for X being finite set holds canFS X is Enumeration of X
proof end;

registration
let A be set ;
let X be finite Subset of A;
cluster canFS X -> A -valued ;
coherence
canFS X is A -valued
proof end;
end;

theorem :: POLYVIE1:3
for L being non empty right_zeroed addLoopStr
for a being Element of L holds 2 * a = a + a
proof end;

registration
let L be almost_left_invertible multLoopStr_0 ;
cluster non zero -> left_invertible for Element of the carrier of L;
coherence
for b1 being Element of L st not b1 is zero holds
b1 is left_invertible by ALGSTR_0:def 39;
end;

registration
let L be almost_right_invertible multLoopStr_0 ;
cluster non zero -> right_invertible for Element of the carrier of L;
coherence
for b1 being Element of L st not b1 is zero holds
b1 is right_invertible by ALGSTR_0:def 40;
end;

registration
let L be almost_left_cancelable multLoopStr_0 ;
cluster non zero -> left_mult-cancelable for Element of the carrier of L;
coherence
for b1 being Element of L st not b1 is zero holds
b1 is left_mult-cancelable by ALGSTR_0:def 36;
end;

registration
let L be almost_right_cancelable multLoopStr_0 ;
cluster non zero -> right_mult-cancelable for Element of the carrier of L;
coherence
for b1 being Element of L st not b1 is zero holds
b1 is right_mult-cancelable by ALGSTR_0:def 37;
end;

theorem Th4: :: POLYVIE1:4
for L being non trivial right_unital associative doubleLoopStr
for a, b being Element of L st b is left_invertible & b is right_mult-cancelable & b * (/ b) = (/ b) * b holds
(a * b) / b = a
proof end;

registration
let L be non degenerated ZeroOneStr ;
let z0 be Element of L;
let z1 be non zero Element of L;
cluster <%z0,z1%> -> non-zero ;
coherence
<%z0,z1%> is non-zero
proof end;
cluster <%z1,z0%> -> non-zero ;
coherence
<%z1,z0%> is non-zero
proof end;
end;

theorem :: POLYVIE1:5
for L being non trivial ZeroStr
for p being Polynomial of L st len p = 1 holds
ex a being non zero Element of L st p = <%a%>
proof end;

theorem Th6: :: POLYVIE1:6
for L being non trivial ZeroStr
for p being Polynomial of L st len p = 2 holds
ex a being Element of L ex b being non zero Element of L st p = <%a,b%>
proof end;

theorem :: POLYVIE1:7
for L being non trivial ZeroStr
for p being Polynomial of L st len p = 3 holds
ex a, b being Element of L ex c being non zero Element of L st p = <%a,b,c%>
proof end;

theorem Th8: :: POLYVIE1:8
for L being non empty right_complementable almost_left_invertible add-associative right_zeroed left-distributive well-unital associative commutative doubleLoopStr
for a, b, x being Element of L st b <> 0. L holds
eval (<%a,b%>,(- (a / b))) = 0. L
proof end;

theorem Th9: :: POLYVIE1:9
for L being Field
for a, x being Element of L
for b being non zero Element of L holds
( x is_a_root_of <%a,b%> iff x = - (a / b) )
proof end;

theorem Th10: :: POLYVIE1:10
for L being Field
for a being Element of L
for b being non zero Element of L holds Roots <%a,b%> = {(- (a / b))}
proof end;

theorem Th11: :: POLYVIE1:11
for L being Field
for a being Element of L
for b being non zero Element of L holds multiplicity (<%a,b%>,(- (a / b))) = 1
proof end;

theorem :: POLYVIE1:12
for L being Field
for a being Element of L
for b being non zero Element of L holds BRoots <%a,b%> = ({(- (a / b))},1) -bag
proof end;

theorem :: POLYVIE1:13
for L being Field
for a, c being Element of L
for b, d being non zero Element of L holds Roots (<%a,b%> *' <%c,d%>) = {(- (a / b)),(- (c / d))}
proof end;

theorem Th14: :: POLYVIE1:14
for L being Field
for a, x being Element of L
for b being non zero Element of L st x <> - (a / b) holds
multiplicity (<%a,b%>,x) = 0
proof end;

theorem Th15: :: POLYVIE1:15
for L being Field
for p being non-zero Polynomial of L
for a being Element of L
for b being non zero Element of L st not - (a / b) in Roots p holds
card (Roots (<%a,b%> *' p)) = 1 + (card (Roots p))
proof end;

theorem Th16: :: POLYVIE1:16
for L being Field
for p being non-zero Polynomial of L
for a being Element of L
for b being non zero Element of L st not - (a / b) in Roots p holds
(canFS (Roots p)) ^ <*(- (a / b))*> is Enumeration of Roots (<%a,b%> *' p)
proof end;

theorem Th17: :: POLYVIE1:17
for L being Field
for p being non-zero Polynomial of L
for a being Element of L
for b being non zero Element of L
for E being Enumeration of Roots (<%a,b%> *' p) st E = (canFS (Roots p)) ^ <*(- (a / b))*> holds
( len E = 1 + (card (Roots p)) & E . (1 + (card (Roots p))) = - (a / b) & ( for n being Nat st 1 <= n & n <= card (Roots p) holds
E . n = (canFS (Roots p)) . n ) )
proof end;

definition
let L be non empty doubleLoopStr ;
let B be bag of the carrier of L;
let E be the carrier of L -valued FinSequence;
func B (++) E -> FinSequence of L means :Def1: :: POLYVIE1:def 1
( len it = len E & ( for n being Nat st 1 <= n & n <= len it holds
it . n = ((B * E) . n) * (E /. n) ) );
existence
ex b1 being FinSequence of L st
( len b1 = len E & ( for n being Nat st 1 <= n & n <= len b1 holds
b1 . n = ((B * E) . n) * (E /. n) ) )
proof end;
uniqueness
for b1, b2 being FinSequence of L st len b1 = len E & ( for n being Nat st 1 <= n & n <= len b1 holds
b1 . n = ((B * E) . n) * (E /. n) ) & len b2 = len E & ( for n being Nat st 1 <= n & n <= len b2 holds
b2 . n = ((B * E) . n) * (E /. n) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def1 defines (++) POLYVIE1:def 1 :
for L being non empty doubleLoopStr
for B being bag of the carrier of L
for E being the carrier of b1 -valued FinSequence
for b4 being FinSequence of L holds
( b4 = B (++) E iff ( len b4 = len E & ( for n being Nat st 1 <= n & n <= len b4 holds
b4 . n = ((B * E) . n) * (E /. n) ) ) );

theorem Th18: :: POLYVIE1:18
for L being domRing
for p being non-zero Polynomial of L
for B being bag of the carrier of L
for E being Enumeration of Roots p st Roots p = {} holds
B (++) E = {}
proof end;

theorem Th19: :: POLYVIE1:19
for L being non empty left_zeroed add-associative doubleLoopStr
for B1, B2 being bag of the carrier of L
for E being the carrier of b1 -valued FinSequence holds (B1 + B2) (++) E = (B1 (++) E) + (B2 (++) E)
proof end;

theorem Th20: :: POLYVIE1:20
for L being non empty left_zeroed add-associative doubleLoopStr
for B being bag of the carrier of L
for E, F being the carrier of b1 -valued FinSequence holds B (++) (E ^ F) = (B (++) E) ^ (B (++) F)
proof end;

theorem :: POLYVIE1:21
for L being non empty left_zeroed add-associative doubleLoopStr
for B1, B2 being bag of the carrier of L
for E, F being the carrier of b1 -valued FinSequence holds (B1 + B2) (++) (E ^ F) = ((B1 (++) E) ^ (B1 (++) F)) + ((B2 (++) E) ^ (B2 (++) F))
proof end;

theorem Th22: :: POLYVIE1:22
for L being Field
for p being non-zero Polynomial of L
for a being Element of L
for b being non zero Element of L
for E being Enumeration of Roots (<%a,b%> *' p)
for P being Permutation of (dom E) holds ((BRoots (<%a,b%> *' p)) (++) E) * P = (BRoots (<%a,b%> *' p)) (++) (E * P)
proof end;

theorem Th23: :: POLYVIE1:23
for L being Field
for p being non-zero Polynomial of L
for a being Element of L
for b being non zero Element of L st not - (a / b) in Roots p holds
for E being Enumeration of Roots (<%a,b%> *' p) st E = (canFS (Roots p)) ^ <*(- (a / b))*> holds
((canFS (Roots (<%a,b%> *' p))) ") * E is Permutation of (dom E)
proof end;

theorem Th24: :: POLYVIE1:24
for L being Field
for p being non-zero Polynomial of L
for a being Element of L
for b being non zero Element of L st not - (a / b) in Roots p holds
for E being Enumeration of Roots (<%a,b%> *' p) st E = (canFS (Roots p)) ^ <*(- (a / b))*> holds
Sum ((BRoots (<%a,b%> *' p)) (++) E) = Sum ((BRoots (<%a,b%> *' p)) (++) (canFS (Roots (<%a,b%> *' p))))
proof end;

theorem Th25: :: POLYVIE1:25
for L being Field
for p being non-zero Polynomial of L
for a being Element of L
for b being non zero Element of L
for E being Enumeration of Roots (<%a,b%> *' p) holds Sum ((BRoots <%a,b%>) (++) E) = - (a / b)
proof end;

definition
let L be domRing;
let p be non-zero Polynomial of L;
func SumRoots p -> Element of L equals :: POLYVIE1:def 2
 Sum ((BRoots p) (++) (canFS (Roots p)));
coherence
Sum ((BRoots p) (++) (canFS (Roots p))) is Element of L ;
end;

:: deftheorem defines SumRoots POLYVIE1:def 2 :
for L being domRing
for p being non-zero Polynomial of L holds SumRoots p = Sum ((BRoots p) (++) (canFS (Roots p)));

theorem :: POLYVIE1:26
for L being domRing
for p being non-zero Polynomial of L st Roots p = {} holds
SumRoots p = 0. L
proof end;

theorem Th27: :: POLYVIE1:27
for L being Field
for a being Element of L
for b being non zero Element of L holds SumRoots <%a,b%> = - (a / b)
proof end;

theorem Th28: :: POLYVIE1:28
for L being 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)
proof end;

theorem :: POLYVIE1:29
for L being Field
for a, c being Element of L
for b, d being non zero Element of L holds SumRoots (<%a,b%> *' <%c,d%>) = (- (a / b)) + (- (c / d))
proof end;

theorem :: POLYVIE1:30
for L being algebraic-closed Field
for p, q being non-zero Polynomial of L st len p >= 2 holds
SumRoots (p *' q) = (SumRoots p) + (SumRoots q)
proof end;

theorem :: POLYVIE1:31
for L being 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
proof end;

:: WP: Vieta's formula about the sum of roots
theorem :: POLYVIE1:32
for L being algebraic-closed Field
for p being non-zero Polynomial of L st len p >= 2 holds
SumRoots p = - ((p . ((len p) -' 2)) / (p . ((len p) -' 1)))
proof end;