:: Introduction to Rational Functions
:: by Christoph Schwarzweller
::
:: Received February 8, 2012
:: Copyright (c) 2012-2021 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)
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
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)))
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;
cluster x / y -> non zero ;
coherence
not x / y is zero
proof end;
end;

registration
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 b1 being non empty right_complementable right-distributive add-associative right_zeroed doubleLoopStr st b1 is domRing-like holds
b1 is almost_left_cancelable
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 b1 being non empty right_complementable left-distributive add-associative right_zeroed doubleLoopStr st b1 is domRing-like holds
b1 is almost_right_cancelable
proof end;
end;

registration
let x, y be Integer;
cluster max (x,y) -> integer ;
coherence
max (x,y) is integer
by XXREAL_0:16;
cluster min (x,y) -> integer ;
coherence
min (x,y) is integer
by XXREAL_0:15;
end;

theorem Th4: :: RATFUNC1:4
for x, y, z being Integer holds max ((x + y),(x + z)) = x + (max (y,z))
proof end;

notation
let L be non empty ZeroStr ;
let p be Polynomial of L;
antonym zero p for non-zero ;
end;

definition
let L be non empty ZeroStr ;
let p be Polynomial of L;
attr p is constant means :: RATFUNC1:def 2
deg p <= 0 ;
end;

:: deftheorem RATFUNC1:def 1 :
canceled;

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

registration
let L be non empty ZeroStr ;
cluster V1() V4( omega ) V5( the carrier of L) Function-like V11() total V18( omega , the carrier of L) finite-Support zero for Element of K19(K20(omega, the carrier of L));
existence
ex b1 being Polynomial of L st b1 is zero
proof end;
end;

registration
let L be non trivial ZeroStr ;
cluster V1() V4( omega ) V5( the carrier of L) Function-like V11() total V18( omega , the carrier of L) finite-Support non zero for Element of K19(K20(omega, the carrier of L));
existence
not for b1 being Polynomial of L holds b1 is zero
proof end;
end;

registration
let L be non empty ZeroStr ;
cluster 0_. L -> zero constant ;
coherence
( 0_. L is zero & 0_. L is constant )
by HURWITZ:20;
end;

registration
let L be non degenerated multLoopStr_0 ;
cluster 1_. L -> non zero ;
coherence
not 1_. L is zero
proof end;
end;

registration
let L be non empty multLoopStr_0 ;
cluster 1_. L -> constant ;
coherence
1_. L is constant
proof end;
end;

registration
let L be non degenerated multLoopStr_0 ;
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 Element of K19(K20(omega, the carrier of L));
existence
ex b1 being Polynomial of L st
( not b1 is zero & b1 is constant )
proof end;
end;

registration
let L be non empty ZeroStr ;
cluster Function-like V18( omega , the carrier of L) finite-Support zero -> constant for Element of K19(K20(omega, the carrier of L));
coherence
for b1 being Polynomial of L st b1 is zero holds
b1 is constant
;
end;

registration
let L be non empty ZeroStr ;
cluster Function-like V18( omega , the carrier of L) finite-Support non constant -> non zero for Element of K19(K20(omega, the carrier of L));
coherence
for b1 being Polynomial of L st not b1 is constant holds
not b1 is zero
;
end;

registration
let L be non trivial ZeroStr ;
cluster V1() V4( omega ) V5( the carrier of L) Function-like V11() total V18( omega , the carrier of L) finite-Support non constant for Element of K19(K20(omega, the carrier of L));
existence
not for b1 being Polynomial of L holds b1 is constant
proof end;
end;

registration
let L be non empty non degenerated well-unital doubleLoopStr ;
let z be Element of L;
let k be Element of NAT ;
cluster rpoly (k,z) -> non zero ;
coherence
not rpoly (k,z) is zero
proof end;
end;

registration
let L be non degenerated right_complementable distributive add-associative right_zeroed doubleLoopStr ;
cluster Polynom-Ring L -> non degenerated ;
coherence
not Polynom-Ring L is degenerated
proof end;
end;

registration
let L be non trivial right_complementable distributive add-associative right_zeroed domRing-like doubleLoopStr ;
cluster Polynom-Ring L -> domRing-like ;
coherence
Polynom-Ring L is domRing-like
;
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)
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)
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;
cluster a * p -> non zero ;
coherence
not a * p is zero
proof end;
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;
cluster p1 *' p2 -> non zero ;
coherence
not p1 *' p2 is zero
proof end;
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
proof end;

registration
let L be non trivial ZeroStr ;
let p be non zero Polynomial of L;
cluster degree p -> natural ;
coherence
degree p is natural
proof end;
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
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 )
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 )
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
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) ) )
proof end;

definition
let L be non empty unital doubleLoopStr ;
let p1, p2 be Polynomial of L;
let x be Element of L;
pred x is_a_common_root_of p1,p2 means :: RATFUNC1:def 3
( x is_a_root_of p1 & x is_a_root_of p2 );
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 ) );

definition
let L be non empty unital doubleLoopStr ;
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;
end;

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

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;

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

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
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
proof end;

definition
let L be non empty unital doubleLoopStr ;
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 } is Subset of L
proof end;
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 } ;

definition
let L be non empty ZeroStr ;
let p be Polynomial of L;
func Leading-Coefficient p -> Element of L equals :: RATFUNC1:def 6
p . ((len p) -' 1);
coherence
p . ((len p) -' 1) is Element of L
;
end;

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

notation
let L be non empty ZeroStr ;
let p be Polynomial of L;
synonym LC p for Leading-Coefficient p;
end;

registration
let L be non trivial doubleLoopStr ;
let p be non zero Polynomial of L;
cluster Leading-Coefficient p -> non zero ;
coherence
not LC p is zero
proof end;
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)
proof end;

definition
let L be non empty doubleLoopStr ;
let p be Polynomial of L;
attr p is normalized means :: RATFUNC1:def 7
LC p = 1. L;
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 );

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;
cluster ((1. L) / (LC p)) * p -> normalized ;
coherence
((1. L) / (LC p)) * p is normalized
proof end;
end;

registration
let L be Field;
let p be non zero Polynomial of L;
cluster NormPolynomial p -> normalized ;
coherence
NormPolynomial p is normalized
proof end;
end;

definition
let L be non trivial multLoopStr_0 ;
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 b1 being set ex p1 being Polynomial of L ex p2 being non zero Polynomial of L st b1 = [p1,p2]
proof end;
end;

:: deftheorem Def8 defines rational_function RATFUNC1:def 8 :
for L being non trivial multLoopStr_0
for b2 being set holds
( b2 is rational_function of L iff ex p1 being Polynomial of L ex p2 being non zero Polynomial of L st b2 = [p1,p2] );

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
proof end;
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
proof end;
:: original: `2
redefine func z `2 -> non zero Polynomial of L;
coherence
z `2 is non zero Polynomial of L
proof end;
end;

definition
let L be non trivial multLoopStr_0 ;
let z be rational_function of L;
attr z is zero means :Def9: :: RATFUNC1:def 9
z `1 = 0_. L;
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 );

registration
let L be non trivial multLoopStr_0 ;
cluster non zero for rational_function of L;
existence
not for b1 being rational_function of L holds b1 is zero
proof end;
end;

theorem Th19: :: RATFUNC1:19
for L being non trivial multLoopStr_0
for z being rational_function of L holds z = [(z `1),(z `2)]
proof end;

definition
let L be non trivial right_complementable distributive add-associative right_zeroed unital doubleLoopStr ;
let z be rational_function of L;
attr z is irreducible means :Def10: :: RATFUNC1:def 10
z `1 ,z `2 have_no_common_roots ;
end;

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

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;

definition
let L be non trivial right_complementable distributive add-associative right_zeroed unital doubleLoopStr ;
let z be rational_function of L;
attr z is normalized means :Def11: :: RATFUNC1:def 11
( z is irreducible & z `2 is normalized );
end;

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

registration
let L be non trivial right_complementable distributive add-associative right_zeroed unital doubleLoopStr ;
cluster normalized -> irreducible for rational_function of L;
coherence
for b1 being rational_function of L st b1 is normalized holds
b1 is irreducible
;
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 rational_function of L;
cluster Leading-Coefficient (z `2) -> non zero ;
coherence
not LC (z `2) is zero
;
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;
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))] is rational_function of L
;
end;

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

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;

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;
cluster NormRationalFunction z -> non zero ;
coherence
not NormRationalFunction z is zero
proof end;
end;

definition
let L be non degenerated multLoopStr_0 ;
func 0._ L -> rational_function of L equals :: RATFUNC1:def 13
[(0_. L),(1_. L)];
coherence
[(0_. L),(1_. L)] is rational_function of L
;
func 1._ L -> rational_function of L equals :: RATFUNC1:def 14
[(1_. L),(1_. L)];
coherence
[(1_. L),(1_. L)] is rational_function of L
;
end;

:: deftheorem defines 0._ RATFUNC1:def 13 :
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)];

registration
let L be non degenerated right_complementable well-unital distributive add-associative right_zeroed associative doubleLoopStr ;
cluster 0._ L -> normalized ;
coherence
0._ L is normalized
proof end;
end;

registration
let L be non degenerated multLoopStr_0 ;
cluster 1._ L -> non zero ;
coherence
not 1._ L is zero
;
end;

registration
let L be non degenerated right_complementable well-unital distributive add-associative right_zeroed associative doubleLoopStr ;
cluster 1._ L -> irreducible ;
coherence
1._ L is irreducible
proof end;
end;

registration
let L be non degenerated right_complementable well-unital distributive add-associative right_zeroed associative doubleLoopStr ;
cluster non zero irreducible for rational_function of L;
existence
ex b1 being rational_function of L st
( b1 is irreducible & not b1 is zero )
proof end;
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;
cluster [(rpoly (1,x)),(rpoly (1,x))] -> non zero reducible for rational_function of L;
coherence
for b1 being rational_function of L st b1 = [(rpoly (1,x)),(rpoly (1,x))] holds
( not b1 is irreducible & not b1 is zero )
proof end;
end;

registration
let L be non degenerated right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr ;
cluster non zero reducible for rational_function of L;
existence
ex b1 being rational_function of L st
( b1 is reducible & not b1 is zero )
proof end;
end;

registration
let L be non degenerated right_complementable well-unital distributive add-associative right_zeroed associative doubleLoopStr ;
cluster normalized for rational_function of L;
existence
ex b1 being rational_function of L st b1 is normalized
proof end;
end;

registration
let L be non degenerated multLoopStr_0 ;
cluster 0._ L -> zero ;
coherence
0._ L is zero
;
end;

registration
let L be non degenerated right_complementable well-unital distributive add-associative right_zeroed associative doubleLoopStr ;
cluster 1._ L -> normalized ;
coherence
1._ L is normalized
proof end;
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;
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))] is rational_function of L
;
end;

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

definition
let L be non trivial right_complementable distributive add-associative right_zeroed domRing-like doubleLoopStr ;
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))] is rational_function of L
;
end;

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

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 )
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) ) ) ) )
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;
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
( ( not z is zero implies ex b1, 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 & b1 = 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 b1 being rational_function of L st b1 = 0._ L ) )
proof end;
uniqueness
for b1, b2 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 & b1 = 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 & b2 = 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 b1 = b2 ) & ( z is zero & b1 = 0._ L & b2 = 0._ L implies b1 = b2 ) )
by Lm3;
consistency
for b1 being rational_function of L holds verum
;
end;

:: 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, b3 being rational_function of L holds
( ( not z is zero implies ( b3 = 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 & b3 = 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 ( b3 = NF z iff b3 = 0._ L ) ) );

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;
cluster NF z -> irreducible normalized ;
coherence
( NF z is normalized & NF z is irreducible )
proof end;
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;
cluster NF z -> non zero ;
coherence
not NF z is zero
proof end;
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;

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;

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
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
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 ) )
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;
func degree z -> Integer equals :: RATFUNC1:def 18
max ((degree ((NF z) `1)),(degree ((NF z) `2)));
coherence
max ((degree ((NF z) `1)),(degree ((NF z) `2))) is Integer
;
end;

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

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;

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)))
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))) )
proof end;

definition
let L be Field;
let z be rational_function of L;
let x be Element of L;
func eval (z,x) -> Element of L equals :: RATFUNC1:def 19
(eval ((z `1),x)) / (eval ((z `2),x));
coherence
(eval ((z `1),x)) / (eval ((z `2),x)) is Element of L
;
end;

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

theorem Th31: :: RATFUNC1:31
for L being Field
for x being Element of L holds eval ((0._ L),x) = 0. L
proof end;

theorem :: RATFUNC1:32
for L being Field
for x being Element of L holds eval ((1._ L),x) = 1. L
proof end;

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))
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))
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)
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) )
proof end;