:: by Artur Korni{\l}owicz and Karol P\kak

::

:: Received May 25, 2017

:: Copyright (c) 2017-2019 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);

coherence

F * f is FinSequence-like by FINSEQ_2:40;

end;
let f be Function of (dom F),(dom F);

coherence

F * f is FinSequence-like by FINSEQ_2:40;

registration
end;

registration

let L be almost_left_invertible multLoopStr_0 ;

coherence

for b_{1} being Element of L st not b_{1} is zero holds

b_{1} is left_invertible
by ALGSTR_0:def 39;

end;
coherence

for b

b

registration

let L be almost_right_invertible multLoopStr_0 ;

coherence

for b_{1} being Element of L st not b_{1} is zero holds

b_{1} is right_invertible
by ALGSTR_0:def 40;

end;
coherence

for b

b

registration

let L be almost_left_cancelable multLoopStr_0 ;

coherence

for b_{1} being Element of L st not b_{1} is zero holds

b_{1} is left_mult-cancelable
by ALGSTR_0:def 36;

end;
coherence

for b

b

registration

let L be almost_right_cancelable multLoopStr_0 ;

coherence

for b_{1} being Element of L st not b_{1} is zero holds

b_{1} is right_mult-cancelable
by ALGSTR_0:def 37;

end;
coherence

for b

b

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

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;

coherence

<%z0,z1%> is non-zero

<%z1,z0%> is non-zero

end;
let z0 be Element of L;

let z1 be non zero Element of L;

coherence

<%z0,z1%> is non-zero

proof end;

coherence <%z1,z0%> is non-zero

proof 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%>

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%>

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%>

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

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) )

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))}

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

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

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))}

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

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))

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)

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 ) )

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;

ex b_{1} being FinSequence of L st

( len b_{1} = len E & ( for n being Nat st 1 <= n & n <= len b_{1} holds

b_{1} . n = ((B * E) . n) * (E /. n) ) )

for b_{1}, b_{2} being FinSequence of L st len b_{1} = len E & ( for n being Nat st 1 <= n & n <= len b_{1} holds

b_{1} . n = ((B * E) . n) * (E /. n) ) & len b_{2} = len E & ( for n being Nat st 1 <= n & n <= len b_{2} holds

b_{2} . n = ((B * E) . n) * (E /. n) ) holds

b_{1} = b_{2}

end;
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 ( len it = len E & ( for n being Nat st 1 <= n & n <= len it holds

it . n = ((B * E) . n) * (E /. n) ) );

ex b

( len b

b

proof end;

uniqueness for b

b

b

b

proof 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_{1} -valued FinSequence

for b_{4} being FinSequence of L holds

( b_{4} = B (++) E iff ( len b_{4} = len E & ( for n being Nat st 1 <= n & n <= len b_{4} holds

b_{4} . n = ((B * E) . n) * (E /. n) ) ) );

for L being non empty doubleLoopStr

for B being bag of the carrier of L

for E being the carrier of b

for b

( b

b

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 = {}

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_{1} -valued FinSequence holds (B1 + B2) (++) E = (B1 (++) E) + (B2 (++) E)

for B1, B2 being bag of the carrier of L

for E being the carrier of b

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_{1} -valued FinSequence holds B (++) (E ^ F) = (B (++) E) ^ (B (++) F)

for B being bag of the carrier of L

for E, F being the carrier of b

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_{1} -valued FinSequence holds (B1 + B2) (++) (E ^ F) = ((B1 (++) E) ^ (B1 (++) F)) + ((B2 (++) E) ^ (B2 (++) F))

for B1, B2 being bag of the carrier of L

for E, F being the carrier of b

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)

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)

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))))

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)

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;

coherence

Sum ((BRoots p) (++) (canFS (Roots p))) is Element of L ;

end;
let p be non-zero Polynomial of L;

coherence

Sum ((BRoots p) (++) (canFS (Roots p))) is Element of L ;

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

for L being domRing

for p being non-zero Polynomial of L holds SumRoots p = Sum ((BRoots p) (++) (canFS (Roots p)));

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)

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)

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))

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)

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

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)))

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;