:: by Christoph Schwarzweller

::

:: Received February 8, 2012

:: Copyright (c) 2012-2018 Association of Mizar Users

theorem Th1: :: RATFUNC1:1

for L being non empty right_complementable right-distributive add-associative right_zeroed doubleLoopStr

for a being Element of L

for p, q being FinSequence of L st len p = len q & ( for i being Element of NAT st i in dom p holds

q /. i = a * (p /. i) ) holds

Sum q = a * (Sum p)

for a being Element of L

for p, q being FinSequence of L st len p = len q & ( for i being Element of NAT st i in dom p holds

q /. i = a * (p /. i) ) holds

Sum q = a * (Sum p)

proof end;

theorem Th2: :: RATFUNC1:2

for L being non empty right_complementable right-distributive add-associative right_zeroed doubleLoopStr

for f being FinSequence of L

for i, j being Element of NAT st i in dom f & j = i - 1 holds

Ins ((Del (f,i)),j,(f /. i)) = f

for f being FinSequence of L

for i, j being Element of NAT st i in dom f & j = i - 1 holds

Ins ((Del (f,i)),j,(f /. i)) = f

proof end;

theorem Th3: :: RATFUNC1:3

for L being non empty right_complementable right-distributive add-associative right_zeroed unital associative commutative doubleLoopStr

for f being FinSequence of L

for i being Element of NAT st i in dom f holds

Product f = (f /. i) * (Product (Del (f,i)))

for f being FinSequence of L

for i being Element of NAT st i in dom f holds

Product f = (f /. i) * (Product (Del (f,i)))

proof end;

registration

let L be non trivial right_complementable almost_left_invertible left-distributive well-unital add-associative right_zeroed associative commutative domRing-like doubleLoopStr ;

let x, y be non zero Element of L;

coherence

not x / y is zero

end;
let x, y be non zero Element of L;

coherence

not x / y is zero

proof end;

registration

for b_{1} being non empty right_complementable right-distributive add-associative right_zeroed doubleLoopStr st b_{1} is domRing-like holds

b_{1} is almost_left_cancelable

for b_{1} being non empty right_complementable left-distributive add-associative right_zeroed doubleLoopStr st b_{1} is domRing-like holds

b_{1} is almost_right_cancelable
end;

cluster non empty right_complementable right-distributive add-associative right_zeroed domRing-like -> non empty right_complementable almost_left_cancelable right-distributive add-associative right_zeroed for doubleLoopStr ;

coherence for b

b

proof end;

cluster non empty right_complementable left-distributive add-associative right_zeroed domRing-like -> non empty right_complementable almost_right_cancelable left-distributive add-associative right_zeroed for doubleLoopStr ;

coherence for b

b

proof end;

registration

let x, y be Integer;

coherence

max (x,y) is integer by XXREAL_0:16;

coherence

min (x,y) is integer by XXREAL_0:15;

end;
coherence

max (x,y) is integer by XXREAL_0:16;

coherence

min (x,y) is integer by XXREAL_0:15;

:: deftheorem defines constant RATFUNC1:def 2 :

for L being non empty ZeroStr

for p being Polynomial of L holds

( p is constant iff deg p <= 0 );

for L being non empty ZeroStr

for p being Polynomial of L holds

( p is constant iff deg p <= 0 );

registration

let L be non empty ZeroStr ;

ex b_{1} being Polynomial of L st b_{1} is zero

end;
cluster V1() V4( omega ) V5( the carrier of L) Function-like V11() total V18( omega , the carrier of L) finite-Support zero for Polynomial of ;

existence ex b

proof end;

registration

let L be non trivial ZeroStr ;

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

end;
cluster V1() V4( omega ) V5( the carrier of L) Function-like V11() total V18( omega , the carrier of L) finite-Support non zero for Polynomial of ;

existence not for b

proof end;

registration
end;

registration

let L be non degenerated multLoopStr_0 ;

ex b_{1} being Polynomial of L st

( not b_{1} is zero & b_{1} is constant )

end;
cluster V1() V4( omega ) V5( the carrier of L) Function-like V11() total V18( omega , the carrier of L) finite-Support non zero constant for Polynomial of ;

existence ex b

( not b

proof end;

registration

let L be non empty ZeroStr ;

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

b_{1} is constant
;

end;
cluster Function-like V18( omega , the carrier of L) finite-Support zero -> constant for Polynomial of ;

coherence for b

b

registration

let L be non empty ZeroStr ;

for b_{1} being Polynomial of L st not b_{1} is constant holds

not b_{1} is zero
;

end;
cluster Function-like V18( omega , the carrier of L) finite-Support non constant -> non zero for Polynomial of ;

coherence for b

not b

registration

let L be non trivial ZeroStr ;

not for b_{1} being Polynomial of L holds b_{1} is constant

end;
cluster V1() V4( omega ) V5( the carrier of L) Function-like V11() total V18( omega , the carrier of L) finite-Support non constant for Polynomial of ;

existence not for b

proof end;

registration

let L be non empty non degenerated well-unital doubleLoopStr ;

let z be Element of L;

let k be Element of NAT ;

coherence

not rpoly (k,z) is zero

end;
let z be Element of L;

let k be Element of NAT ;

coherence

not rpoly (k,z) is zero

proof end;

registration

let L be non degenerated right_complementable distributive add-associative right_zeroed doubleLoopStr ;

coherence

not Polynom-Ring L is degenerated

end;
coherence

not Polynom-Ring L is degenerated

proof end;

registration

let L be non trivial right_complementable distributive add-associative right_zeroed domRing-like doubleLoopStr ;

coherence

Polynom-Ring L is domRing-like

end;
coherence

Polynom-Ring L is domRing-like

proof end;

theorem :: RATFUNC1:5

for L being non empty right_complementable right-distributive add-associative right_zeroed associative doubleLoopStr

for p, q being Polynomial of L

for a being Element of L holds (a * p) *' q = a * (p *' q)

for p, q being Polynomial of L

for a being Element of L holds (a * p) *' q = a * (p *' q)

proof end;

theorem :: RATFUNC1:6

for L being non empty right_complementable right-distributive add-associative right_zeroed associative commutative doubleLoopStr

for p, q being Polynomial of L

for a being Element of L holds p *' (a * q) = a * (p *' q)

for p, q being Polynomial of L

for a being Element of L holds p *' (a * q) = a * (p *' q)

proof end;

registration

let L be non trivial right_complementable almost_left_invertible well-unital distributive add-associative right_zeroed associative commutative doubleLoopStr ;

let p be non zero Polynomial of L;

let a be non zero Element of L;

coherence

not a * p is zero

end;
let p be non zero Polynomial of L;

let a be non zero Element of L;

coherence

not a * p is zero

proof end;

registration

let L be non trivial right_complementable distributive add-associative right_zeroed domRing-like doubleLoopStr ;

let p1, p2 be non zero Polynomial of L;

coherence

not p1 *' p2 is zero

end;
let p1, p2 be non zero Polynomial of L;

coherence

not p1 *' p2 is zero

proof end;

theorem Th7: :: RATFUNC1:7

for L being non trivial right_complementable distributive Abelian add-associative right_zeroed domRing-like doubleLoopStr

for p1, p2 being Polynomial of L

for p3 being non zero Polynomial of L st p1 *' p3 = p2 *' p3 holds

p1 = p2

for p1, p2 being Polynomial of L

for p3 being non zero Polynomial of L st p1 *' p3 = p2 *' p3 holds

p1 = p2

proof end;

registration

let L be non trivial ZeroStr ;

let p be non zero Polynomial of L;

coherence

degree p is natural

end;
let p be non zero Polynomial of L;

coherence

degree p is natural

proof end;

theorem Th8: :: RATFUNC1:8

for L being non empty right_complementable right-distributive add-associative right_zeroed unital doubleLoopStr

for p being Polynomial of L st deg p = 0 holds

for x being Element of L holds eval (p,x) <> 0. L

for p being Polynomial of L st deg p = 0 holds

for x being Element of L holds eval (p,x) <> 0. L

proof end;

theorem Th9: :: RATFUNC1:9

for L being non degenerated right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative doubleLoopStr

for p being Polynomial of L

for x being Element of L holds

( eval (p,x) = 0. L iff rpoly (1,x) divides p )

for p being Polynomial of L

for x being Element of L holds

( eval (p,x) = 0. L iff rpoly (1,x) divides p )

proof end;

theorem Th10: :: RATFUNC1:10

for L being non degenerated right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative domRing-like doubleLoopStr

for p, q being Polynomial of L

for x being Element of L holds

( not rpoly (1,x) divides p *' q or rpoly (1,x) divides p or rpoly (1,x) divides q )

for p, q being Polynomial of L

for x being Element of L holds

( not rpoly (1,x) divides p *' q or rpoly (1,x) divides p or rpoly (1,x) divides q )

proof end;

theorem Th11: :: RATFUNC1:11

for L being non degenerated right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative doubleLoopStr

for f being FinSequence of (Polynom-Ring L) st ( for i being Nat st i in dom f holds

ex z being Element of L st f . i = rpoly (1,z) ) holds

for p being Polynomial of L st p = Product f holds

p <> 0_. L

for f being FinSequence of (Polynom-Ring L) st ( for i being Nat st i in dom f holds

ex z being Element of L st f . i = rpoly (1,z) ) holds

for p being Polynomial of L st p = Product f holds

p <> 0_. L

proof end;

theorem Th12: :: RATFUNC1:12

for L being non degenerated right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative domRing-like doubleLoopStr

for f being FinSequence of (Polynom-Ring L) st ( for i being Nat st i in dom f holds

ex z being Element of L st f . i = rpoly (1,z) ) holds

for p being Polynomial of L st p = Product f holds

for x being Element of L holds

( eval (p,x) = 0. L iff ex i being Nat st

( i in dom f & f . i = rpoly (1,x) ) )

for f being FinSequence of (Polynom-Ring L) st ( for i being Nat st i in dom f holds

ex z being Element of L st f . i = rpoly (1,z) ) holds

for p being Polynomial of L st p = Product f holds

for x being Element of L holds

( eval (p,x) = 0. L iff ex i being Nat st

( i in dom f & f . i = rpoly (1,x) ) )

proof end;

definition
end;

:: deftheorem defines is_a_common_root_of RATFUNC1:def 3 :

for L being non empty unital doubleLoopStr

for p1, p2 being Polynomial of L

for x being Element of L holds

( x is_a_common_root_of p1,p2 iff ( x is_a_root_of p1 & x is_a_root_of p2 ) );

for L being non empty unital doubleLoopStr

for p1, p2 being Polynomial of L

for x being Element of L holds

( x is_a_common_root_of p1,p2 iff ( x is_a_root_of p1 & x is_a_root_of p2 ) );

definition

let L be non empty unital doubleLoopStr ;

let p1, p2 be Polynomial of L;

end;
let p1, p2 be Polynomial of L;

pred p1,p2 have_a_common_root means :: RATFUNC1:def 4

ex x being Element of L st x is_a_common_root_of p1,p2;

ex x being Element of L st x is_a_common_root_of p1,p2;

:: deftheorem defines have_a_common_root RATFUNC1:def 4 :

for L being non empty unital doubleLoopStr

for p1, p2 being Polynomial of L holds

( p1,p2 have_a_common_root iff ex x being Element of L st x is_a_common_root_of p1,p2 );

for L being non empty unital doubleLoopStr

for p1, p2 being Polynomial of L holds

( p1,p2 have_a_common_root iff ex x being Element of L st x is_a_common_root_of p1,p2 );

notation

let L be non empty unital doubleLoopStr ;

let p1, p2 be Polynomial of L;

synonym p1,p2 have_common_roots for p1,p2 have_a_common_root ;

antonym p1,p2 have_no_common_roots for p1,p2 have_a_common_root ;

end;
let p1, p2 be Polynomial of L;

synonym p1,p2 have_common_roots for p1,p2 have_a_common_root ;

antonym p1,p2 have_no_common_roots for p1,p2 have_a_common_root ;

theorem Th13: :: RATFUNC1:13

for L being non empty right_complementable distributive Abelian add-associative right_zeroed unital doubleLoopStr

for p being Polynomial of L

for x being Element of L st x is_a_root_of p holds

x is_a_root_of - p

for p being Polynomial of L

for x being Element of L st x is_a_root_of p holds

x is_a_root_of - p

proof end;

theorem Th14: :: RATFUNC1:14

for L being non empty right_complementable left-distributive Abelian add-associative right_zeroed unital doubleLoopStr

for p1, p2 being Polynomial of L

for x being Element of L st x is_a_common_root_of p1,p2 holds

x is_a_root_of p1 + p2

for p1, p2 being Polynomial of L

for x being Element of L st x is_a_common_root_of p1,p2 holds

x is_a_root_of p1 + p2

proof end;

theorem :: RATFUNC1:15

for L being non empty right_complementable distributive Abelian add-associative right_zeroed unital doubleLoopStr

for p1, p2 being Polynomial of L

for x being Element of L st x is_a_common_root_of p1,p2 holds

x is_a_root_of - (p1 + p2) by Th13, Th14;

for p1, p2 being Polynomial of L

for x being Element of L st x is_a_common_root_of p1,p2 holds

x is_a_root_of - (p1 + p2) by Th13, Th14;

theorem :: RATFUNC1:16

for L being non empty right_complementable distributive Abelian add-associative right_zeroed unital doubleLoopStr

for p, q being Polynomial of L

for x being Element of L st x is_a_common_root_of p,q holds

x is_a_root_of p + q

for p, q being Polynomial of L

for x being Element of L st x is_a_common_root_of p,q holds

x is_a_root_of p + q

proof end;

theorem :: RATFUNC1:17

for L being non trivial right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative doubleLoopStr

for p1, p2 being Polynomial of L st p1 divides p2 & p1 is with_roots holds

p1,p2 have_common_roots

for p1, p2 being Polynomial of L st p1 divides p2 & p1 is with_roots holds

p1,p2 have_common_roots

proof end;

definition

let L be non empty unital doubleLoopStr ;

let p, q be Polynomial of L;

{ x where x is Element of L : x is_a_common_root_of p,q } is Subset of L

end;
let p, q be Polynomial of L;

func Common_Roots (p,q) -> Subset of L equals :: RATFUNC1:def 5

{ x where x is Element of L : x is_a_common_root_of p,q } ;

coherence { x where x is Element of L : x is_a_common_root_of p,q } ;

{ x where x is Element of L : x is_a_common_root_of p,q } is Subset of L

proof end;

:: deftheorem defines Common_Roots RATFUNC1:def 5 :

for L being non empty unital doubleLoopStr

for p, q being Polynomial of L holds Common_Roots (p,q) = { x where x is Element of L : x is_a_common_root_of p,q } ;

for L being non empty unital doubleLoopStr

for p, q being Polynomial of L holds Common_Roots (p,q) = { x where x is Element of L : x is_a_common_root_of p,q } ;

definition

let L be non empty ZeroStr ;

let p be Polynomial of L;

coherence

p . ((len p) -' 1) is Element of L ;

end;
let p be Polynomial of L;

coherence

p . ((len p) -' 1) is Element of L ;

:: deftheorem defines Leading-Coefficient RATFUNC1:def 6 :

for L being non empty ZeroStr

for p being Polynomial of L holds Leading-Coefficient p = p . ((len p) -' 1);

for L being non empty ZeroStr

for p being Polynomial of L holds Leading-Coefficient p = p . ((len p) -' 1);

notation
end;

registration

let L be non trivial doubleLoopStr ;

let p be non zero Polynomial of L;

coherence

not LC p is zero

end;
let p be non zero Polynomial of L;

coherence

not LC p is zero

proof end;

theorem Th18: :: RATFUNC1:18

for L being non empty right_complementable almost_left_invertible well-unital distributive add-associative right_zeroed associative commutative doubleLoopStr

for p being Polynomial of L

for a being Element of L holds LC (a * p) = a * (LC p)

for p being Polynomial of L

for a being Element of L holds LC (a * p) = a * (LC p)

proof end;

:: deftheorem defines normalized RATFUNC1:def 7 :

for L being non empty doubleLoopStr

for p being Polynomial of L holds

( p is normalized iff LC p = 1. L );

for L being non empty doubleLoopStr

for p being Polynomial of L holds

( p is normalized iff LC p = 1. L );

registration

let L be non trivial right_complementable almost_left_invertible well-unital distributive add-associative right_zeroed associative commutative doubleLoopStr ;

let p be non zero Polynomial of L;

coherence

((1. L) / (LC p)) * p is normalized

end;
let p be non zero Polynomial of L;

coherence

((1. L) / (LC p)) * p is normalized

proof end;

registration

let L be Field;

let p be non zero Polynomial of L;

coherence

NormPolynomial p is normalized

end;
let p be non zero Polynomial of L;

coherence

NormPolynomial p is normalized

proof end;

definition

let L be non trivial multLoopStr_0 ;

ex b_{1} being set ex p1 being Polynomial of L ex p2 being non zero Polynomial of L st b_{1} = [p1,p2]

end;
mode rational_function of L -> set means :Def8: :: RATFUNC1:def 8

ex p1 being Polynomial of L ex p2 being non zero Polynomial of L st it = [p1,p2];

existence ex p1 being Polynomial of L ex p2 being non zero Polynomial of L st it = [p1,p2];

ex b

proof end;

:: deftheorem Def8 defines rational_function RATFUNC1:def 8 :

for L being non trivial multLoopStr_0

for b_{2} being set holds

( b_{2} is rational_function of L iff ex p1 being Polynomial of L ex p2 being non zero Polynomial of L st b_{2} = [p1,p2] );

for L being non trivial multLoopStr_0

for b

( b

definition

let L be non trivial multLoopStr_0 ;

let p1 be Polynomial of L;

let p2 be non zero Polynomial of L;

:: original: [

redefine func [p1,p2] -> rational_function of L;

coherence

[p1,p2] is rational_function of L

end;
let p1 be Polynomial of L;

let p2 be non zero Polynomial of L;

:: original: [

redefine func [p1,p2] -> rational_function of L;

coherence

[p1,p2] is rational_function of L

proof end;

definition

let L be non trivial multLoopStr_0 ;

let z be rational_function of L;

:: original: `1

redefine func z `1 -> Polynomial of L;

coherence

z `1 is Polynomial of L

redefine func z `2 -> non zero Polynomial of L;

coherence

z `2 is non zero Polynomial of L

end;
let z be rational_function of L;

:: original: `1

redefine func z `1 -> Polynomial of L;

coherence

z `1 is Polynomial of L

proof end;

:: original: `2redefine func z `2 -> non zero Polynomial of L;

coherence

z `2 is non zero Polynomial of L

proof end;

:: deftheorem Def9 defines zero RATFUNC1:def 9 :

for L being non trivial multLoopStr_0

for z being rational_function of L holds

( z is zero iff z `1 = 0_. L );

for L being non trivial multLoopStr_0

for z being rational_function of L holds

( z is zero iff z `1 = 0_. L );

registration

let L be non trivial multLoopStr_0 ;

existence

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

end;
existence

not for b

proof end;

definition

let L be non trivial right_complementable distributive add-associative right_zeroed unital doubleLoopStr ;

let z be rational_function of L;

end;
let z be rational_function of L;

:: deftheorem Def10 defines irreducible RATFUNC1:def 10 :

for L being non trivial right_complementable distributive add-associative right_zeroed unital doubleLoopStr

for z being rational_function of L holds

( z is irreducible iff z `1 ,z `2 have_no_common_roots );

for L being non trivial right_complementable distributive add-associative right_zeroed unital doubleLoopStr

for z being rational_function of L holds

( z is irreducible iff z `1 ,z `2 have_no_common_roots );

notation

let L be non trivial right_complementable distributive add-associative right_zeroed unital doubleLoopStr ;

let z be rational_function of L;

antonym reducible z for irreducible ;

end;
let z be rational_function of L;

antonym reducible z for irreducible ;

definition

let L be non trivial right_complementable distributive add-associative right_zeroed unital doubleLoopStr ;

let z be rational_function of L;

end;
let z be rational_function of L;

:: deftheorem Def11 defines normalized RATFUNC1:def 11 :

for L being non trivial right_complementable distributive add-associative right_zeroed unital doubleLoopStr

for z being rational_function of L holds

( z is normalized iff ( z is irreducible & z `2 is normalized ) );

for L being non trivial right_complementable distributive add-associative right_zeroed unital doubleLoopStr

for z being rational_function of L holds

( z is normalized iff ( z is irreducible & z `2 is normalized ) );

registration

let L be non trivial right_complementable distributive add-associative right_zeroed unital doubleLoopStr ;

coherence

for b_{1} being rational_function of L st b_{1} is normalized holds

b_{1} is irreducible
;

end;
coherence

for b

b

registration

let L be non trivial right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative domRing-like doubleLoopStr ;

let z be rational_function of L;

coherence

not LC (z `2) is zero ;

end;
let z be rational_function of L;

coherence

not LC (z `2) is zero ;

definition

let L be non trivial right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative domRing-like doubleLoopStr ;

let z be rational_function of L;

[(((1. L) / (LC (z `2))) * (z `1)),(((1. L) / (LC (z `2))) * (z `2))] is rational_function of L ;

end;
let z be rational_function of L;

func NormRationalFunction z -> rational_function of L equals :: RATFUNC1:def 12

[(((1. L) / (LC (z `2))) * (z `1)),(((1. L) / (LC (z `2))) * (z `2))];

coherence [(((1. L) / (LC (z `2))) * (z `1)),(((1. L) / (LC (z `2))) * (z `2))];

[(((1. L) / (LC (z `2))) * (z `1)),(((1. L) / (LC (z `2))) * (z `2))] is rational_function of L ;

:: deftheorem defines NormRationalFunction RATFUNC1:def 12 :

for L being non trivial right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative domRing-like doubleLoopStr

for z being rational_function of L holds NormRationalFunction z = [(((1. L) / (LC (z `2))) * (z `1)),(((1. L) / (LC (z `2))) * (z `2))];

for L being non trivial right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative domRing-like doubleLoopStr

for z being rational_function of L holds NormRationalFunction z = [(((1. L) / (LC (z `2))) * (z `1)),(((1. L) / (LC (z `2))) * (z `2))];

notation

let L be non trivial right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative domRing-like doubleLoopStr ;

let z be rational_function of L;

synonym NormRatF z for NormRationalFunction z;

end;
let z be rational_function of L;

synonym NormRatF z for NormRationalFunction z;

registration

let L be non trivial right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative domRing-like doubleLoopStr ;

let z be non zero rational_function of L;

coherence

not NormRationalFunction z is zero

end;
let z be non zero rational_function of L;

coherence

not NormRationalFunction z is zero

proof end;

definition

let L be non degenerated multLoopStr_0 ;

coherence

[(0_. L),(1_. L)] is rational_function of L ;

coherence

[(1_. L),(1_. L)] is rational_function of L ;

end;
coherence

[(0_. L),(1_. L)] is rational_function of L ;

coherence

[(1_. L),(1_. L)] is rational_function of L ;

:: deftheorem defines 0._ RATFUNC1:def 13 :

for L being non degenerated multLoopStr_0 holds 0._ L = [(0_. L),(1_. L)];

for L being non degenerated multLoopStr_0 holds 0._ L = [(0_. L),(1_. L)];

:: deftheorem defines 1._ RATFUNC1:def 14 :

for L being non degenerated multLoopStr_0 holds 1._ L = [(1_. L),(1_. L)];

for L being non degenerated multLoopStr_0 holds 1._ L = [(1_. L),(1_. L)];

registration

let L be non degenerated right_complementable well-unital distributive add-associative right_zeroed associative doubleLoopStr ;

coherence

0._ L is normalized

end;
coherence

0._ L is normalized

proof end;

registration
end;

registration

let L be non degenerated right_complementable well-unital distributive add-associative right_zeroed associative doubleLoopStr ;

coherence

1._ L is irreducible

end;
coherence

1._ L is irreducible

proof end;

registration

let L be non degenerated right_complementable well-unital distributive add-associative right_zeroed associative doubleLoopStr ;

existence

ex b_{1} being rational_function of L st

( b_{1} is irreducible & not b_{1} is zero )

end;
existence

ex b

( b

proof end;

registration

let L be non degenerated right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr ;

let x be Element of L;

coherence

for b_{1} being rational_function of L st b_{1} = [(rpoly (1,x)),(rpoly (1,x))] holds

( not b_{1} is irreducible & not b_{1} is zero )

end;
let x be Element of L;

coherence

for b

( not b

proof end;

registration

let L be non degenerated right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr ;

existence

ex b_{1} being rational_function of L st

( b_{1} is reducible & not b_{1} is zero )

end;
existence

ex b

( b

proof end;

registration

let L be non degenerated right_complementable well-unital distributive add-associative right_zeroed associative doubleLoopStr ;

existence

ex b_{1} being rational_function of L st b_{1} is normalized

end;
existence

ex b

proof end;

registration
end;

registration

let L be non degenerated right_complementable well-unital distributive add-associative right_zeroed associative doubleLoopStr ;

coherence

1._ L is normalized

end;
coherence

1._ L is normalized

proof end;

definition

let L be non trivial right_complementable distributive add-associative right_zeroed domRing-like doubleLoopStr ;

let p, q be rational_function of L;

[(((p `1) *' (q `2)) + ((p `2) *' (q `1))),((p `2) *' (q `2))] is rational_function of L ;

end;
let p, q be rational_function of L;

func p + q -> rational_function of L equals :: RATFUNC1:def 15

[(((p `1) *' (q `2)) + ((p `2) *' (q `1))),((p `2) *' (q `2))];

coherence [(((p `1) *' (q `2)) + ((p `2) *' (q `1))),((p `2) *' (q `2))];

[(((p `1) *' (q `2)) + ((p `2) *' (q `1))),((p `2) *' (q `2))] is rational_function of L ;

:: deftheorem defines + RATFUNC1:def 15 :

for L being non trivial right_complementable distributive add-associative right_zeroed domRing-like doubleLoopStr

for p, q being rational_function of L holds p + q = [(((p `1) *' (q `2)) + ((p `2) *' (q `1))),((p `2) *' (q `2))];

for L being non trivial right_complementable distributive add-associative right_zeroed domRing-like doubleLoopStr

for p, q being rational_function of L holds p + q = [(((p `1) *' (q `2)) + ((p `2) *' (q `1))),((p `2) *' (q `2))];

definition

let L be non trivial right_complementable distributive add-associative right_zeroed domRing-like doubleLoopStr ;

let p, q be rational_function of L;

[((p `1) *' (q `1)),((p `2) *' (q `2))] is rational_function of L ;

end;
let p, q be rational_function of L;

func p *' q -> rational_function of L equals :: RATFUNC1:def 16

[((p `1) *' (q `1)),((p `2) *' (q `2))];

coherence [((p `1) *' (q `1)),((p `2) *' (q `2))];

[((p `1) *' (q `1)),((p `2) *' (q `2))] is rational_function of L ;

:: deftheorem defines *' RATFUNC1:def 16 :

for L being non trivial right_complementable distributive add-associative right_zeroed domRing-like doubleLoopStr

for p, q being rational_function of L holds p *' q = [((p `1) *' (q `1)),((p `2) *' (q `2))];

for L being non trivial right_complementable distributive add-associative right_zeroed domRing-like doubleLoopStr

for p, q being rational_function of L holds p *' q = [((p `1) *' (q `1)),((p `2) *' (q `2))];

theorem Th20: :: RATFUNC1:20

for L being non trivial right_complementable almost_left_invertible well-unital distributive add-associative right_zeroed associative commutative doubleLoopStr

for p being rational_function of L

for a being non zero Element of L holds

( [(a * (p `1)),(a * (p `2))] is irreducible iff p is irreducible )

for p being rational_function of L

for a being non zero Element of L holds

( [(a * (p `1)),(a * (p `2))] is irreducible iff p is irreducible )

proof end;

Lm1: for L being non trivial right_complementable well-unital distributive Abelian add-associative right_zeroed associative commutative domRing-like doubleLoopStr

for z being rational_function of L st z is irreducible holds

ex z1 being rational_function of L ex z2 being non zero Polynomial of L st

( z = [(z2 *' (z1 `1)),(z2 *' (z1 `2))] & z1 is irreducible & ex f being FinSequence of (Polynom-Ring L) st

( z2 = Product f & ( for i being Element of NAT st i in dom f holds

ex x being Element of L st

( x is_a_common_root_of z `1 ,z `2 & f . i = rpoly (1,x) ) ) ) )

proof end;

theorem Th21: :: RATFUNC1:21

for L being non trivial right_complementable well-unital distributive Abelian add-associative right_zeroed associative commutative domRing-like doubleLoopStr

for z being rational_function of L ex z1 being rational_function of L ex z2 being non zero Polynomial of L st

( z = [(z2 *' (z1 `1)),(z2 *' (z1 `2))] & z1 is irreducible & ex f being FinSequence of (Polynom-Ring L) st

( z2 = Product f & ( for i being Element of NAT st i in dom f holds

ex x being Element of L st

( x is_a_common_root_of z `1 ,z `2 & f . i = rpoly (1,x) ) ) ) )

for z being rational_function of L ex z1 being rational_function of L ex z2 being non zero Polynomial of L st

( z = [(z2 *' (z1 `1)),(z2 *' (z1 `2))] & z1 is irreducible & ex f being FinSequence of (Polynom-Ring L) st

( z2 = Product f & ( for i being Element of NAT st i in dom f holds

ex x being Element of L st

( x is_a_common_root_of z `1 ,z `2 & f . i = rpoly (1,x) ) ) ) )

proof end;

Lm2: for L being non trivial right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative domRing-like doubleLoopStr

for z being rational_function of L st z is irreducible holds

for z1 being rational_function of L

for z2 being non zero Polynomial of L st z = [(z2 *' (z1 `1)),(z2 *' (z1 `2))] & z1 is irreducible & ex f being FinSequence of (Polynom-Ring L) st

( z2 = Product f & ( for i being Element of NAT st i in dom f holds

ex x being Element of L st

( x is_a_common_root_of z `1 ,z `2 & f . i = rpoly (1,x) ) ) ) holds

for g1 being rational_function of L

for g2 being non zero Polynomial of L st z = [(g2 *' (g1 `1)),(g2 *' (g1 `2))] & g1 is irreducible & ex f being FinSequence of (Polynom-Ring L) st

( g2 = Product f & ( for i being Element of NAT st i in dom f holds

ex x being Element of L st

( x is_a_common_root_of z `1 ,z `2 & f . i = rpoly (1,x) ) ) ) holds

( z2 = 1_. L & g2 = 1_. L & z1 = g1 )

proof end;

Lm3: for L being non trivial right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative domRing-like doubleLoopStr

for z being non zero rational_function of L

for z1 being rational_function of L

for z2 being non zero Polynomial of L st z = [(z2 *' (z1 `1)),(z2 *' (z1 `2))] & z1 is irreducible & ex f being FinSequence of (Polynom-Ring L) st

( z2 = Product f & ( for i being Element of NAT st i in dom f holds

ex x being Element of L st

( x is_a_common_root_of z `1 ,z `2 & f . i = rpoly (1,x) ) ) ) holds

for g1 being rational_function of L

for g2 being non zero Polynomial of L st z = [(g2 *' (g1 `1)),(g2 *' (g1 `2))] & g1 is irreducible & ex g being FinSequence of (Polynom-Ring L) st

( g2 = Product g & ( for i being Element of NAT st i in dom g holds

ex x being Element of L st

( x is_a_common_root_of z `1 ,z `2 & g . i = rpoly (1,x) ) ) ) holds

z1 = g1

proof end;

definition

let L be non trivial right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative domRing-like doubleLoopStr ;

let z be rational_function of L;

( ( not z is zero implies ex b_{1}, z1 being rational_function of L ex z2 being non zero Polynomial of L st

( z = [(z2 *' (z1 `1)),(z2 *' (z1 `2))] & z1 is irreducible & b_{1} = NormRationalFunction z1 & ex f being FinSequence of (Polynom-Ring L) st

( z2 = Product f & ( for i being Element of NAT st i in dom f holds

ex x being Element of L st

( x is_a_common_root_of z `1 ,z `2 & f . i = rpoly (1,x) ) ) ) ) ) & ( z is zero implies ex b_{1} being rational_function of L st b_{1} = 0._ L ) )

for b_{1}, b_{2} being rational_function of L holds

( ( not z is zero & ex z1 being rational_function of L ex z2 being non zero Polynomial of L st

( z = [(z2 *' (z1 `1)),(z2 *' (z1 `2))] & z1 is irreducible & b_{1} = NormRationalFunction z1 & ex f being FinSequence of (Polynom-Ring L) st

( z2 = Product f & ( for i being Element of NAT st i in dom f holds

ex x being Element of L st

( x is_a_common_root_of z `1 ,z `2 & f . i = rpoly (1,x) ) ) ) ) & ex z1 being rational_function of L ex z2 being non zero Polynomial of L st

( z = [(z2 *' (z1 `1)),(z2 *' (z1 `2))] & z1 is irreducible & b_{2} = NormRationalFunction z1 & ex f being FinSequence of (Polynom-Ring L) st

( z2 = Product f & ( for i being Element of NAT st i in dom f holds

ex x being Element of L st

( x is_a_common_root_of z `1 ,z `2 & f . i = rpoly (1,x) ) ) ) ) implies b_{1} = b_{2} ) & ( z is zero & b_{1} = 0._ L & b_{2} = 0._ L implies b_{1} = b_{2} ) )
by Lm3;

consistency

for b_{1} being rational_function of L holds verum
;

end;
let z be rational_function of L;

func NF z -> rational_function of L means :Def17: :: RATFUNC1:def 17

ex z1 being rational_function of L ex z2 being non zero Polynomial of L st

( z = [(z2 *' (z1 `1)),(z2 *' (z1 `2))] & z1 is irreducible & it = NormRationalFunction z1 & ex f being FinSequence of (Polynom-Ring L) st

( z2 = Product f & ( for i being Element of NAT st i in dom f holds

ex x being Element of L st

( x is_a_common_root_of z `1 ,z `2 & f . i = rpoly (1,x) ) ) ) ) if not z is zero

otherwise it = 0._ L;

existence ex z1 being rational_function of L ex z2 being non zero Polynomial of L st

( z = [(z2 *' (z1 `1)),(z2 *' (z1 `2))] & z1 is irreducible & it = NormRationalFunction z1 & ex f being FinSequence of (Polynom-Ring L) st

( z2 = Product f & ( for i being Element of NAT st i in dom f holds

ex x being Element of L st

( x is_a_common_root_of z `1 ,z `2 & f . i = rpoly (1,x) ) ) ) ) if not z is zero

otherwise it = 0._ L;

( ( not z is zero implies ex b

( z = [(z2 *' (z1 `1)),(z2 *' (z1 `2))] & z1 is irreducible & b

( z2 = Product f & ( for i being Element of NAT st i in dom f holds

ex x being Element of L st

( x is_a_common_root_of z `1 ,z `2 & f . i = rpoly (1,x) ) ) ) ) ) & ( z is zero implies ex b

proof end;

uniqueness for b

( ( not z is zero & ex z1 being rational_function of L ex z2 being non zero Polynomial of L st

( z = [(z2 *' (z1 `1)),(z2 *' (z1 `2))] & z1 is irreducible & b

( z2 = Product f & ( for i being Element of NAT st i in dom f holds

ex x being Element of L st

( x is_a_common_root_of z `1 ,z `2 & f . i = rpoly (1,x) ) ) ) ) & ex z1 being rational_function of L ex z2 being non zero Polynomial of L st

( z = [(z2 *' (z1 `1)),(z2 *' (z1 `2))] & z1 is irreducible & b

( z2 = Product f & ( for i being Element of NAT st i in dom f holds

ex x being Element of L st

( x is_a_common_root_of z `1 ,z `2 & f . i = rpoly (1,x) ) ) ) ) implies b

consistency

for b

:: deftheorem Def17 defines NF RATFUNC1:def 17 :

for L being non trivial right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative domRing-like doubleLoopStr

for z, b_{3} being rational_function of L holds

( ( not z is zero implies ( b_{3} = NF z iff ex z1 being rational_function of L ex z2 being non zero Polynomial of L st

( z = [(z2 *' (z1 `1)),(z2 *' (z1 `2))] & z1 is irreducible & b_{3} = NormRationalFunction z1 & ex f being FinSequence of (Polynom-Ring L) st

( z2 = Product f & ( for i being Element of NAT st i in dom f holds

ex x being Element of L st

( x is_a_common_root_of z `1 ,z `2 & f . i = rpoly (1,x) ) ) ) ) ) ) & ( z is zero implies ( b_{3} = NF z iff b_{3} = 0._ L ) ) );

for L being non trivial right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative domRing-like doubleLoopStr

for z, b

( ( not z is zero implies ( b

( z = [(z2 *' (z1 `1)),(z2 *' (z1 `2))] & z1 is irreducible & b

( z2 = Product f & ( for i being Element of NAT st i in dom f holds

ex x being Element of L st

( x is_a_common_root_of z `1 ,z `2 & f . i = rpoly (1,x) ) ) ) ) ) ) & ( z is zero implies ( b

registration

let L be non trivial right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative domRing-like doubleLoopStr ;

let z be rational_function of L;

coherence

( NF z is normalized & NF z is irreducible )

end;
let z be rational_function of L;

coherence

( NF z is normalized & NF z is irreducible )

proof end;

registration

let L be non trivial right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative domRing-like doubleLoopStr ;

let z be non zero rational_function of L;

coherence

not NF z is zero

end;
let z be non zero rational_function of L;

coherence

not NF z is zero

proof end;

Lm4: for L being non trivial right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative domRing-like doubleLoopStr

for z being non zero irreducible rational_function of L holds NF z = NormRationalFunction z

proof end;

theorem :: RATFUNC1:22

for L being non trivial right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative domRing-like doubleLoopStr

for z being non zero rational_function of L

for z1 being rational_function of L

for z2 being non zero Polynomial of L st z = [(z2 *' (z1 `1)),(z2 *' (z1 `2))] & z1 is irreducible & ex f being FinSequence of (Polynom-Ring L) st

( z2 = Product f & ( for i being Element of NAT st i in dom f holds

ex x being Element of L st

( x is_a_common_root_of z `1 ,z `2 & f . i = rpoly (1,x) ) ) ) holds

NF z = NormRationalFunction z1 by Def17;

for z being non zero rational_function of L

for z1 being rational_function of L

for z2 being non zero Polynomial of L st z = [(z2 *' (z1 `1)),(z2 *' (z1 `2))] & z1 is irreducible & ex f being FinSequence of (Polynom-Ring L) st

( z2 = Product f & ( for i being Element of NAT st i in dom f holds

ex x being Element of L st

( x is_a_common_root_of z `1 ,z `2 & f . i = rpoly (1,x) ) ) ) holds

NF z = NormRationalFunction z1 by Def17;

theorem :: RATFUNC1:23

for L being non trivial right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative domRing-like doubleLoopStr holds NF (0._ L) = 0._ L by Def17;

theorem :: RATFUNC1:24

for L being non trivial right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative domRing-like doubleLoopStr holds NF (1._ L) = 1._ L

proof end;

theorem :: RATFUNC1:25

for L being non trivial right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative domRing-like doubleLoopStr

for z being non zero irreducible rational_function of L holds NF z = NormRationalFunction z by Lm4;

for z being non zero irreducible rational_function of L holds NF z = NormRationalFunction z by Lm4;

Lm5: for L being non trivial right_complementable distributive Abelian add-associative right_zeroed unital domRing-like left_zeroed doubleLoopStr

for p1, p2 being Polynomial of L holds

( not p1 *' p2 = 0_. L or p1 = 0_. L or p2 = 0_. L )

proof end;

theorem Th26: :: RATFUNC1:26

for L being non trivial right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative domRing-like doubleLoopStr

for z being rational_function of L

for x being Element of L holds NF [((rpoly (1,x)) *' (z `1)),((rpoly (1,x)) *' (z `2))] = NF z

for z being rational_function of L

for x being Element of L holds NF [((rpoly (1,x)) *' (z `1)),((rpoly (1,x)) *' (z `2))] = NF z

proof end;

theorem :: RATFUNC1:27

for L being non trivial right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative domRing-like doubleLoopStr

for z being rational_function of L holds NF (NF z) = NF z

for z being rational_function of L holds NF (NF z) = NF z

proof end;

theorem Th28: :: RATFUNC1:28

for L being non degenerated right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative domRing-like doubleLoopStr

for z being non zero rational_function of L holds

( z is irreducible iff ex a being Element of L st

( a <> 0. L & [(a * (z `1)),(a * (z `2))] = NF z ) )

for z being non zero rational_function of L holds

( z is irreducible iff ex a being Element of L st

( a <> 0. L & [(a * (z `1)),(a * (z `2))] = NF z ) )

proof end;

definition

let L be non trivial right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative domRing-like doubleLoopStr ;

let z be rational_function of L;

coherence

max ((degree ((NF z) `1)),(degree ((NF z) `2))) is Integer ;

end;
let z be rational_function of L;

coherence

max ((degree ((NF z) `1)),(degree ((NF z) `2))) is Integer ;

:: deftheorem defines degree RATFUNC1:def 18 :

for L being non trivial right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative domRing-like doubleLoopStr

for z being rational_function of L holds degree z = max ((degree ((NF z) `1)),(degree ((NF z) `2)));

for L being non trivial right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative domRing-like doubleLoopStr

for z being rational_function of L holds degree z = max ((degree ((NF z) `1)),(degree ((NF z) `2)));

notation

let L be non trivial right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative domRing-like doubleLoopStr ;

let z be rational_function of L;

synonym deg z for degree z;

end;
let z be rational_function of L;

synonym deg z for degree z;

Lm6: for L being non trivial right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative domRing-like doubleLoopStr

for z being non zero rational_function of L st z is irreducible holds

degree z = max ((degree (z `1)),(degree (z `2)))

proof end;

theorem Th29: :: RATFUNC1:29

for L being non trivial right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative domRing-like doubleLoopStr

for z being rational_function of L holds degree z <= max ((degree (z `1)),(degree (z `2)))

for z being rational_function of L holds degree z <= max ((degree (z `1)),(degree (z `2)))

proof end;

theorem :: RATFUNC1:30

for L being non trivial right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative domRing-like doubleLoopStr

for z being non zero rational_function of L holds

( z is irreducible iff degree z = max ((degree (z `1)),(degree (z `2))) )

for z being non zero rational_function of L holds

( z is irreducible iff degree z = max ((degree (z `1)),(degree (z `2))) )

proof end;

definition

let L be Field;

let z be rational_function of L;

let x be Element of L;

coherence

(eval ((z `1),x)) / (eval ((z `2),x)) is Element of L ;

end;
let z be rational_function of L;

let x be Element of L;

coherence

(eval ((z `1),x)) / (eval ((z `2),x)) is Element of L ;

:: deftheorem defines eval RATFUNC1:def 19 :

for L being Field

for z being rational_function of L

for x being Element of L holds eval (z,x) = (eval ((z `1),x)) / (eval ((z `2),x));

for L being Field

for z being rational_function of L

for x being Element of L holds eval (z,x) = (eval ((z `1),x)) / (eval ((z `2),x));

theorem :: RATFUNC1:33

for L being Field

for p, q being rational_function of L

for x being Element of L st eval ((p `2),x) <> 0. L & eval ((q `2),x) <> 0. L holds

eval ((p + q),x) = (eval (p,x)) + (eval (q,x))

for p, q being rational_function of L

for x being Element of L st eval ((p `2),x) <> 0. L & eval ((q `2),x) <> 0. L holds

eval ((p + q),x) = (eval (p,x)) + (eval (q,x))

proof end;

theorem :: RATFUNC1:34

for L being Field

for p, q being rational_function of L

for x being Element of L st eval ((p `2),x) <> 0. L & eval ((q `2),x) <> 0. L holds

eval ((p *' q),x) = (eval (p,x)) * (eval (q,x))

for p, q being rational_function of L

for x being Element of L st eval ((p `2),x) <> 0. L & eval ((q `2),x) <> 0. L holds

eval ((p *' q),x) = (eval (p,x)) * (eval (q,x))

proof end;

theorem Th35: :: RATFUNC1:35

for L being Field

for p being rational_function of L

for x being Element of L st eval ((p `2),x) <> 0. L holds

eval ((NormRationalFunction p),x) = eval (p,x)

for p being rational_function of L

for x being Element of L st eval ((p `2),x) <> 0. L holds

eval ((NormRationalFunction p),x) = eval (p,x)

proof end;

theorem :: RATFUNC1:36

for L being Field

for p being rational_function of L

for x being Element of L holds

( not eval ((p `2),x) <> 0. L or x is_a_common_root_of p `1 ,p `2 or eval ((NF p),x) = eval (p,x) )

for p being rational_function of L

for x being Element of L holds

( not eval ((p `2),x) <> 0. L or x is_a_common_root_of p `1 ,p `2 or eval ((NF p),x) = eval (p,x) )

proof end;