:: 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 b₁ being Element of L st not b₁ is zero holds
b₁ 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 b₁ being Element of L st not b₁ is zero holds
b₁ 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 b₁ being Element of L st not b₁ is zero holds
b₁ 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 b₁ being Element of L st not b₁ is zero holds
b₁ 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 b₁ being FinSequence of L st
( len b₁ = len E & ( for n being Nat st 1 <= n & n <= len b₁ holds
b₁ . n = ((B * E) . n) * (E /. n) ) )

proof end;

uniqueness
for b₁, b₂ being FinSequence of L st len b₁ = len E & ( for n being Nat st 1 <= n & n <= len b₁ holds
b₁ . n = ((B * E) . n) * (E /. n) ) & len b₂ = len E & ( for n being Nat st 1 <= n & n <= len b₂ holds
b₂ . n = ((B * E) . n) * (E /. n) ) holds
b₁ = b₂

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 b₁ -valued FinSequence
for b₄ being FinSequence of L holds
( b₄ = B (++) E iff ( len b₄ = len E & ( for n being Nat st 1 <= n & n <= len b₄ holds
b₄ . 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 b₁ -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 b₁ -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 b₁ -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;

:: 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;