:: 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 b₁ being non empty right_complementable right-distributive add-associative right_zeroed doubleLoopStr st b₁ is domRing-like holds
b₁ 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 b₁ being non empty right_complementable left-distributive add-associative right_zeroed doubleLoopStr st b₁ is domRing-like holds
b₁ 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 b₁ being Polynomial of L st b₁ 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 b₁ being Polynomial of L holds b₁ 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 b₁ being Polynomial of L st
( not b₁ is zero & b₁ 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 b₁ being Polynomial of L st b₁ is zero holds
b₁ 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 b₁ being Polynomial of L st not b₁ is constant holds
not b₁ 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 b₁ being Polynomial of L holds b₁ 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 b₁ being set ex p1 being Polynomial of L ex p2 being non zero Polynomial of L st b₁ = [p1,p2]

proof end;

end;

:: deftheorem Def8 defines rational_function RATFUNC1:def 8 :
for L being non trivial multLoopStr_0
for b₂ being set holds
( b₂ is rational_function of L iff ex p1 being Polynomial of L ex p2 being non zero Polynomial of L st b₂ = [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 b₁ being rational_function of L holds b₁ 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 b₁ being rational_function of L st b₁ is normalized holds
b₁ 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 b₁ being rational_function of L st
( b₁ is irreducible & not b₁ 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 b₁ being rational_function of L st b₁ = [(rpoly (1,x)),(rpoly (1,x))] holds
( not b₁ is irreducible & not b₁ 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 b₁ being rational_function of L st
( b₁ is reducible & not b₁ 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 b₁ being rational_function of L st b₁ 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 b₁, 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₁ = 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₁ being rational_function of L st b₁ = 0._ L ) )

proof end;

uniqueness
for b₁, b₂ 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₁ = 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₂ = 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₁ = b₂ ) & ( z is zero & b₁ = 0._ L & b₂ = 0._ L implies b₁ = b₂ ) ) by Lm3;
consistency
for b₁ 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, b₃ being rational_function of L holds
( ( not z is zero implies ( b₃ = 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₃ = 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₃ = NF z iff b₃ = 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;