:: Introduction to Rational Functions
:: by Christoph Schwarzweller
::
:: Received February 8, 2012
:: Copyright (c) 2012-2017 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies ARYTM_3, POLYNOM2, POLYNOM1, ARYTM_1, FUNCT_1, FINSEQ_5,
POLYNOM3, RELAT_1, RLVECT_1, FINSEQ_1, GCD_1, VECTSP_1, CARD_1, ALGSEQ_1,
ALGSTR_1, CARD_3, SGRAPH1, INT_1, FUNCT_4, ALGSTR_0, POLYNOM5, RFINSEQ,
MCART_1, HURWITZ, ZFMISC_1, XBOOLE_0, TARSKI, YELLOW_8, LATTICES,
XCMPLX_0, VECTSP_2, MSALIMIT, STRUCT_0, SUBSET_1, SUPINF_2, NAT_1,
NUMBERS, MESFUNC1, XXREAL_0, RATFUNC1, GROUP_1, FINSEQ_3, BINOP_1,
PARTFUN1, ORDINAL4, ORDINAL1, VALUED_0;
notations TARSKI, SUBSET_1, ORDINAL1, XCMPLX_0, PARTFUN1, XXREAL_0, NAT_D,
GROUP_4, FUNCT_7, VECTSP_2, NUMBERS, XTUPLE_0, MCART_1, ALGSTR_0,
ALGSTR_1, VECTSP_1, RLVECT_1, ARYTM_3, RELSET_1, FINSEQ_1, FUNCT_1,
FUNCT_2, GROUP_1, INT_1, NAT_1, FINSEQ_3, VFUNCT_1, RFINSEQ, NORMSP_1,
POLYNOM3, POLYNOM4, FINSEQ_5, POLYNOM5, STRUCT_0, ALGSEQ_1,
UPROOTS, HURWITZ;
constructors BINOP_1, REAL_1, SQUARE_1, VECTSP_2, POLYNOM4, POLYNOM5,
XTUPLE_0, ALGSTR_2, HURWITZ, FUNCT_4, RELSET_1, ARYTM_3, FUNCT_7,
GROUP_4, NAT_D, VFUNCT_1, RFINSEQ, FINSEQ_5, NAT_1, ALGSEQ_1,
UPROOTS;
registrations XBOOLE_0, ORDINAL1, RELSET_1, XCMPLX_0, XXREAL_0, XREAL_0,
NAT_1, INT_1, MEMBERED, FINSEQ_1, STRUCT_0, VECTSP_1, ALGSTR_1, GCD_1,
POLYNOM3, POLYNOM4, POLYNOM5, POLYNOM1, FUNCT_2, VFUNCT_1, CARD_1,
RELAT_1, XTUPLE_0, UPROOTS;
requirements NUMERALS, SUBSET, REAL, BOOLE, ARITHM;
definitions STRUCT_0, ALGSTR_0, VECTSP_2, UPROOTS;
equalities FINSEQ_1, POLYNOM3, VECTSP_1, FINSEQ_5, HURWITZ, ALGSTR_0;
expansions FINSEQ_1, STRUCT_0, ALGSTR_0, VECTSP_2, HURWITZ, UPROOTS;
theorems GROUP_1, VECTSP_1, ALGSEQ_1, NAT_1, FUNCT_1, FUNCT_2, XREAL_1,
VECTSP_2, INT_1, FINSEQ_1, RLVECT_1, POLYNOM4, FUNCT_7, TARSKI, POLYNOM3,
POLYNOM2, FUNCOP_1, POLYNOM5, XXREAL_0, FINSEQ_3, ORDINAL1, PARTFUN1,
HURWITZ, STRUCT_0, XREAL_0, FINSEQ_4, GROUP_4, ALGSTR_0, FINSEQ_5,
RFINSEQ, XTUPLE_0, UPROOTS;
schemes NAT_1, INT_1;
begin :: Preliminaries
theorem Th1:
for L being add-associative right_zeroed right_complementable
right-distributive non empty 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
let L be add-associative right_zeroed right_complementable
right-distributive non empty doubleLoopStr,
a be Element of L,
p,q be FinSequence of L;
assume A1: len p = len q &
for i being Element of NAT st i in dom p
holds q/.i = a * (p/.i);
consider fq being sequence of the carrier of L such that
A2: Sum q = fq.(len q) and
A3: fq.0 = 0.L and
A4: for j being Nat, v being Element of L
st j < len q & v = q.(j + 1)
holds fq.(j + 1) = fq.j + v by RLVECT_1:def 12;
consider fp being sequence of the carrier of L such that
A5: Sum p = fp.(len p) and
A6: fp.0 = 0.L and
A7: for j being Nat, v being Element of L
st j < len p & v = p.(j + 1)
holds fp.(j + 1) = fp.j + v by RLVECT_1:def 12;
defpred P[Element of NAT] means fq.($1) = a * fp.($1);
A8: P[0] by A6,A3;
A9: for j being Element of NAT st 0 <= j & j < len p
holds P[j] implies P[j+1]
proof
let j be Element of NAT;
assume A10: 0 <= j & j < len p;
assume A11: P[j];
A12: 1 <= j + 1 by NAT_1:11;
A13: j + 1 <= len p by A10,NAT_1:13;
then j+1 in Seg(len q) by A12,A1;
then A14: j+1 in dom q by FINSEQ_1:def 3;
j+1 in Seg(len p) by A12,A13;
then A15: j+1 in dom p by FINSEQ_1:def 3;
set vq = q/.(j+1), vp = p/.(j+1);
A16: vq = q.(j+1) by A14,PARTFUN1:def 6;
A17: vp = p.(j+1) by A15,PARTFUN1:def 6;
fq.(j+1) = (a * fp.j) + vq by A11,A1,A16,A10,A4
.= (a * fp.j) + (a * vp) by A1,A15
.= a * (fp.j + vp) by VECTSP_1:def 2
.= a * fp.(j+1) by A17,A10,A7;
hence P[j+1];
end;
for j being Element of NAT st 0 <= j & j <= len p
holds P[j] from INT_1:sch 7(A8,A9);
hence thesis by A1,A5,A2;
end;
theorem Th2:
for L being add-associative right_zeroed right_complementable
right-distributive non empty 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
let L be add-associative right_zeroed right_complementable
right-distributive non empty doubleLoopStr;
let f be FinSequence of L;
let i,j be Element of NAT;
set g = Ins(Del(f,i),j,f/.i);
assume A1: i in dom f & j = i-1;
then consider n being Nat such that
A2: len f = n+1 & len Del(f,i) = n by FINSEQ_3:104;
dom f = Seg(n+1) by A2,FINSEQ_1:def 3;
then consider ii being Nat such that
A3: i = ii & 1 <= ii & ii <= n + 1 by A1;
i-1 < i-0 by XREAL_1:15;
then j < n+1 by A1,A3,XXREAL_0:2;
then A4: j <= n by NAT_1:13;
A5: len g = (len Del(f,i) + 1) by FINSEQ_5:69;
now let k be Nat;
assume A6: 1 <= k & k <= len g;
then k in Seg(len g);
then A7: k in dom g by FINSEQ_1:def 3;
now per cases by XXREAL_0:1;
suppose A8: k < i;
then k+1 <= i by NAT_1:13;
then k+1-1 <= i - 1 by XREAL_1:9;
then 1 <= k & k <= len(Del(f,i)|j) by A6,A1,A4,A2,FINSEQ_1:59;
then k in Seg(len(Del(f,i)|j));
then A9: k in dom(Del(f,i)|j) by FINSEQ_1:def 3;
k < n+1 by A3,A8,XXREAL_0:2;
then k <= n by NAT_1:13;
then k in Seg(len(Del(f,i))) by A2,A6;
then A10: k in dom(Del(f,i)) by FINSEQ_1:def 3;
g/.k = Del(f,i)/.k by A9,FINSEQ_5:72
.= Del(f,i).k by A10,PARTFUN1:def 6
.= f.k by A8,FINSEQ_3:110;
hence g.k = f.k by A7,PARTFUN1:def 6;
end;
suppose A11: k = i;
then k = j + 1 by A1;
then A12: g/.k = f/.i by A2,A4,FINSEQ_5:73;
thus g.k = g/.k by A7,PARTFUN1:def 6
.= f.k by A1,A11,A12,PARTFUN1:def 6;
end;
suppose A13: k > i;
then reconsider k1 = k-1 as Element of NAT by A3,INT_1:5,XXREAL_0:2;
A14: k-1 <= n+1-1 by A6,A2,A5,XREAL_1:9;
1 < k1+1 by A13,A3,XXREAL_0:2;
then 1 <= k1 by NAT_1:13;
then k1 in Seg(n) by A14;
then A15: k1 in dom(Del(f,i)) by A2,FINSEQ_1:def 3;
i < k1 + 1 by A13;
then A16: j+1 <= k-1 by A1,NAT_1:13;
then g/.(k1+1) = Del(f,i)/.k1 by A14,A2,FINSEQ_5:74
.= Del(f,i).k1 by A15,PARTFUN1:def 6
.= f.(k1+1) by A16,A14,A2,A1,FINSEQ_3:111;
hence f.k = g.k by A7,PARTFUN1:def 6;
end;
end;
hence g.k = f.k;
end;
hence thesis by A2,FINSEQ_5:69;
end;
theorem Th3:
for L being add-associative right_zeroed right_complementable
associative unital right-distributive commutative
non empty 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
let L be add-associative right_zeroed right_complementable
associative unital right-distributive commutative
non empty doubleLoopStr;
let f be FinSequence of L;
let i be Element of NAT;
assume A1: i in dom f;
then i in Seg(len f) by FINSEQ_1:def 3;
then consider ii being Nat such that
A2: ii = i & 1 <= ii & ii <= len f;
reconsider j = i-1 as Element of NAT by A2,INT_1:5;
set g = Del(f,i);
thus Product f = Product( Ins(g,j,f/.i) ) by A1,Th2
.= Product((g|j)^<*f/.i*>) * Product(g/^j) by GROUP_4:5
.= (Product(g|j) * f/.i) * Product(g/^j) by GROUP_4:6
.= f/.i * (Product(g|j) * Product(g/^j)) by GROUP_1:def 3
.= f/.i * (Product((g|j)^(g/^j))) by GROUP_4:5
.= f/.i * Product g by RFINSEQ:8;
end;
registration
let L be add-associative right_zeroed right_complementable
well-unital associative left-distributive commutative
almost_left_invertible domRing-like non trivial doubleLoopStr;
let x,y be non zero Element of L;
cluster x / y -> non zero;
coherence
proof
x <> 0.L & y <> 0.L;
then y" * y = 1.L by VECTSP_1:def 10;
then y" <> 0.L;
hence x / y <> 0.L by VECTSP_2:def 1;
end;
end;
registration
cluster domRing-like -> almost_left_cancelable
for add-associative right_zeroed right_complementable
right-distributive non empty doubleLoopStr;
coherence
proof
let L be add-associative right_zeroed right_complementable
right-distributive non empty doubleLoopStr;
assume A1: L is domRing-like;
let x be Element of L;
assume A2: x <> 0.L;
let y,z be Element of L;
assume x*y = x*z;
then (x*y) - (x*z) = 0.L by RLVECT_1:15;
then x * (y-z) = 0.L by VECTSP_1:11;
then y - z = 0.L by A2,A1;
hence y = z by RLVECT_1:21;
end;
cluster domRing-like -> almost_right_cancelable
for add-associative right_zeroed right_complementable
left-distributive non empty doubleLoopStr;
coherence
proof
let L be add-associative right_zeroed right_complementable
left-distributive non empty doubleLoopStr;
assume A3: L is domRing-like;
let x be Element of L;
assume A4: x <> 0.L;
let y,z be Element of L;
assume y*x = z*x;
then (y*x) - (z*x) = 0.L by RLVECT_1:15;
then (y-z) * x = 0.L by VECTSP_1:13;
then y - z = 0.L by A4,A3;
hence y = z by RLVECT_1:21;
end;
end;
registration
let x,y be Integer;
cluster max(x,y) -> integer;
coherence by XXREAL_0:16;
cluster min(x,y) -> integer;
coherence by XXREAL_0:15;
end;
theorem Th4:
for x,y,z being Integer holds max(x+y,x+z) = x + max(y,z)
proof
let x,y,z be Integer;
per cases;
suppose A1: y <= z;
then x+y <= x+z by XREAL_1:6;
hence max(x+y,x+z) = x+z by XXREAL_0:def 10
.= x + max(y,z) by A1,XXREAL_0:def 10;
end;
suppose A2: y > z;
then x+y > x+z by XREAL_1:8;
hence max(x+y,x+z) = x+y by XXREAL_0:def 10
.= x + max(y,z) by A2,XXREAL_0:def 10;
end;
end;
begin :: More on Polynomials
notation
let L be non empty ZeroStr;
let p be Polynomial of L;
antonym p is zero for p is non-zero;
end;
definition
::$CD
let L be non empty ZeroStr;
let p be Polynomial of L;
attr p is constant means
deg p <= 0;
end;
registration
let L be non empty ZeroStr;
cluster zero for Polynomial of L;
existence
proof
take 0_.L;
thus thesis;
end;
end;
registration
let L be non trivial ZeroStr;
cluster non zero for Polynomial of L;
existence
proof
now assume A1: not(ex x being Element of the carrier of L st x <> 0.L);
now let x,y be Element of the carrier of L;
thus y = 0.L by A1 .= x by A1;
end;
hence contradiction by STRUCT_0:def 10;
end;
then consider x being Element of the carrier of L such that
A2: x <> 0.L;
set p = 0_.(L)+*(0,x);
ex n being Nat st for i being Nat st i >= n holds p.i = 0.L
proof
take 1;
now let i be Nat;
assume A3: i >= 1;
A4: i in NAT by ORDINAL1:def 12;
thus p.i = (0_.(L)).i by A3,FUNCT_7:32
.= 0.L by A4,FUNCOP_1:7;
end;
hence thesis;
end;
then reconsider p as Polynomial of L by ALGSEQ_1:def 1;
take p;
now let i be Nat;
assume i < 1;
then A5: i = 0 by NAT_1:14;
i in NAT by ORDINAL1:def 12;
then 0 in dom(0_.L) by A5,FUNCT_2:def 1;
hence p.i <> 0.L by A2,A5,FUNCT_7:31;
end;
then len p <> 0 by ALGSEQ_1:9;
hence p <> 0_.L by POLYNOM4:3;
end;
end;
registration
let L be non empty ZeroStr;
cluster 0_.(L) -> zero constant;
coherence by HURWITZ:20;
end;
registration
let L be non degenerated multLoopStr_0;
cluster 1_.(L) -> non zero;
coherence
proof
A1: (1_.(L)).0 = 1.L by POLYNOM3:30;
(0_.(L)).0 = 0.L by FUNCOP_1:7;
hence thesis by A1;
end;
end;
registration
let L be non empty multLoopStr_0;
cluster 1_.(L) -> constant;
coherence
proof
set p = 1_.(L);
now per cases;
suppose A1: 0.L = 1.L;
A2: dom p = NAT by FUNCT_2:def 1 .= dom(0_.(L)) by FUNCT_2:def 1;
now let x be object;
assume x in dom p;
then reconsider xx = x as Element of NAT;
A3: (0_.(L)).xx = 0.L by FUNCOP_1:7;
xx = 0 or xx <> 0;
hence p.x = (0_.(L)).x by A1,A3,POLYNOM3:30;
end;
hence thesis by A2,FUNCT_1:2;
end;
suppose A4: 0.L <> 1.L;
now let i be Nat;
assume A5: i >= 1;
A6: i in NAT by ORDINAL1:def 12;
thus p.i = (0_.(L)).i by A5,FUNCT_7:32
.= 0.L by A6,FUNCOP_1:7;
end;
then A7: 1 is_at_least_length_of p by ALGSEQ_1:def 2;
now let m be Nat;
assume A8: m is_at_least_length_of p;
now assume m < 1;
then m < 1 + 0;
then m <= 0 by NAT_1:13;
then A9: p.0 = 0.L by A8,ALGSEQ_1:def 2;
dom(0_.(L)) = NAT by FUNCOP_1:13;
hence contradiction by A4,A9,FUNCT_7:31;
end;
hence 1 <= m;
end;
then len p = 1 by A7,ALGSEQ_1:def 3;
then deg p = 0;
hence thesis;
end;
end;
hence thesis;
end;
end;
registration
let L be non degenerated multLoopStr_0;
cluster non zero constant for Polynomial of L;
existence
proof
take 1_.(L);
thus thesis;
end;
end;
registration
let L be non empty ZeroStr;
cluster zero -> constant for Polynomial of L;
coherence;
end;
registration
let L be non empty ZeroStr;
cluster non constant -> non zero for Polynomial of L;
coherence;
end;
registration
let L be non trivial ZeroStr;
cluster non constant for Polynomial of L;
existence
proof
now assume A1: not(ex x being Element of the carrier of L st x <> 0.L);
now let x,y be Element of the carrier of L;
thus y = 0.L by A1 .= x by A1;
end;
hence contradiction by STRUCT_0:def 10;
end;
then consider x being Element of the carrier of L such that
A2: x <> 0.L;
set p = (0_.(L)+*(0,x))+*(1,x);
ex n being Nat st for i being Nat st i >= n holds p.i = 0.L
proof
take 2;
now let i be Nat;
assume A3: i >= 2;
then A4: 1 <> i;
A5: i in NAT by ORDINAL1:def 12;
thus p.i = (0_.(L)+*(0,x)).i by A4,FUNCT_7:32
.= (0_.(L)).i by A3,FUNCT_7:32
.= 0.L by A5,FUNCOP_1:7;
end;
hence thesis;
end;
then reconsider p as Polynomial of L by ALGSEQ_1:def 1;
take p;
now let i be Nat;
assume A6: i >= 2;
then A7: 1 <> i;
A8: i in NAT by ORDINAL1:def 12;
thus p.i = (0_.(L)+*(0,x)).i by A7,FUNCT_7:32
.= (0_.(L)).i by A6,FUNCT_7:32
.= 0.L by A8,FUNCOP_1:7;
end;
then A9: 2 is_at_least_length_of p by ALGSEQ_1:def 2;
now let m be Nat;
assume A10: m is_at_least_length_of p;
now assume m < 2;
then m < 1 + 1;
then m <= 1 by NAT_1:13;
then A11: p.1 = 0.L by A10,ALGSEQ_1:def 2;
dom(0_.(L)) = NAT by FUNCOP_1:13;
then dom(0_.(L)+*(0,x)) = NAT by FUNCT_7:30;
hence contradiction by A2,A11,FUNCT_7:31;
end;
hence 2 <= m;
end;
then len p = 2 by A9,ALGSEQ_1:def 3;
then deg p = 1;
hence thesis;
end;
end;
registration
let L be well-unital non degenerated non empty doubleLoopStr;
let z be Element of L;
let k be Element of NAT;
cluster rpoly(k,z) -> non zero;
coherence
proof
deg rpoly(k,z) = k by HURWITZ:27;
then rpoly(k,z) <> 0_.(L) by HURWITZ:20;
hence thesis;
end;
end;
registration
let L be add-associative right_zeroed right_complementable distributive
non degenerated doubleLoopStr;
cluster Polynom-Ring(L) -> non degenerated;
coherence
proof
set S = Polynom-Ring(L);
0.S = 0_.(L) & 1.S = 1_.(L) by POLYNOM3:def 10;
hence thesis;
end;
end;
registration
let L be domRing-like add-associative right_zeroed right_complementable
distributive non trivial doubleLoopStr;
cluster Polynom-Ring(L) -> domRing-like;
coherence
proof
set Q = Polynom-Ring(L);
let x,y be Element of Q;
assume A1: x*y = 0.Q;
assume A2: x <> 0.Q & y <> 0.Q;
reconsider p = x as Polynomial of L by POLYNOM3:def 10;
reconsider q = y as Polynomial of L by POLYNOM3:def 10;
p <> 0_.(L) by A2,POLYNOM3:def 10;
then reconsider p as non zero Polynomial of L by UPROOTS:def 5;
q <> 0_.(L) by A2,POLYNOM3:def 10;
then reconsider q as non zero Polynomial of L by UPROOTS:def 5;
p <> 0_.(L);
then deg p <> -1 by HURWITZ:20;
then A3: len p <> 0;
len p + 1 > 0 + 1 by A3,XREAL_1:8;
then A4: len p >= 1 by NAT_1:13;
then len p - 1 >= 1 - 1 by XREAL_1:9;
then A5: len p -' 1 = len p - 1 by XREAL_0:def 2;
then reconsider lp = len p - 1 as Nat;
q <> 0_.(L);
then deg q <> -1 by HURWITZ:20;
then A6: len q <> 0;
len q + 1 > 0 + 1 by A6,XREAL_1:8;
then A7: len q >= 1 by NAT_1:13;
then A8: len q - 1 >= 1 - 1 by XREAL_1:9;
then len q -' 1 = len q - 1 by XREAL_0:def 2;
then reconsider lq = len q - 1 as Nat;
set m = len p + len q - 2;
len p + len q >= 1 + 1 by A4,A7,XREAL_1:7;
then len p + len q - 2 >= 2 - 2 by XREAL_1:9;
then reconsider m as Element of NAT by INT_1:3;
consider r being FinSequence of the carrier of L such that
A9: len r = m+1 & (p*'q).m = Sum r &
for k be Element of NAT st k in dom r holds r.k = p.(k-'1) * q.(m+1-'k)
by POLYNOM3:def 9;
(len p + len q - 2) + 1 - len p = lq;
then A10: (m+1)-' len p = lq by XREAL_0:def 2;
A11: len p + 0 <= len p + (len q - 1) by A8,XREAL_1:6;
then len p in Seg(len r) by A4,A9;
then A12: len p in dom r by FINSEQ_1:def 3;
then A13: r.(len p) = p.lp * q.lq by A10,A5,A9;
A14: now let k be Element of NAT;
assume A15: k in dom r & k <> len p;
now per cases;
suppose k > len p;
then k >= len p + 1 by NAT_1:13;
then A16: k-1 >= (len p + 1) - 1 by XREAL_1:9;
k-'1 >= len p by A16,XREAL_0:def 2;
then p.(k-'1)= 0.L by ALGSEQ_1:8;
then p.(k-'1) * q.(m+1-'k) = 0.L;
hence r.k = 0.L by A15,A9;
end;
suppose A17: k <= len p;
k < len p by A15,A17,XXREAL_0:1;
then (m+1) - k > (m+1) - len p by XREAL_1:10;
then m+1 - k >= len q - 1 + 1 by INT_1:7;
then m+1 -' k >= len q by XREAL_0:def 2;
then q.(m+1-'k)= 0.L by ALGSEQ_1:8;
then p.(k-'1) * q.(m+1-'k) = 0.L;
hence r.k = 0.L by A15,A9;
end;
end;
hence r.k = 0.L;
end;
A18: now let i be Element of NAT;
assume A19: i in dom r & i <> len p;
then i in Seg(len r) by FINSEQ_1:def 3;
then 1 <= i & i <= len r by FINSEQ_1:1;
hence r/.i = r.i by FINSEQ_4:15 .= 0.L by A19,A14;
end;
A20: (p*'q).m = r/.(len p) by A9,A12,A18,POLYNOM2:3
.= p.lp * q.lq by A13,A11,A4,A9,FINSEQ_4:15;
len p = lp + 1;
then A21: p.lp <> 0.L by ALGSEQ_1:10;
len q = lq + 1;
then q.lq <> 0.L by ALGSEQ_1:10;
then A22: (p*'q).m <> 0.L by A21,A20,VECTSP_2:def 1;
(0_.(L)).m = 0.L by FUNCOP_1:7;
then p*'q <> 0.Q by A22,POLYNOM3:def 10;
hence thesis by A1,POLYNOM3:def 10;
end;
end;
theorem
for L being add-associative right_zeroed right_complementable
right-distributive associative non empty doubleLoopStr
for p,q being Polynomial of L
for a being Element of L
holds (a * p) *' q = a * (p *' q)
proof
let L be add-associative right_zeroed right_complementable
right-distributive associative non empty doubleLoopStr;
let p,q be Polynomial of L;
let a being Element of L;
set f = (a * p) *' q, g = a * (p *' q);
A1: dom f = NAT by FUNCT_2:def 1 .= dom g by FUNCT_2:def 1;
now let i be object;
assume i in dom f;
then reconsider n = i as Element of NAT;
consider fr being FinSequence of the carrier of L such that
A2: len fr = n+1 & f.i = Sum fr &
for k being Element of NAT st k in dom fr
holds fr.k = (a*p).(k-'1) * q.(n+1-'k) by POLYNOM3:def 9;
consider fa being FinSequence of the carrier of L such that
A3: len fa = n+1 & (p *' q).i = Sum fa &
for k being Element of NAT st k in dom fa
holds fa.k = p.(k-'1) * q.(n+1-'k) by POLYNOM3:def 9;
Seg(len fa) = dom fr by A2,A3,FINSEQ_1:def 3;
then A4: dom fa = dom fr by FINSEQ_1:def 3;
A5: now let k be Element of NAT;
assume A6: k in dom fa;
then fa.k = fa/.k by PARTFUN1:def 6;
then reconsider x = fa.k as Element of L;
thus fr/.k = fr.k by A6,A4,PARTFUN1:def 6
.= (a*p).(k-'1) * q.(n+1-'k) by A4,A6,A2
.= (a * p.(k-'1)) * q.(n+1-'k) by POLYNOM5:def 4
.= a* (p.(k-'1) * q.(n+1-'k)) by GROUP_1:def 3
.= a * x by A6,A3
.= a * (fa/.k) by A6,PARTFUN1:def 6;
end;
g.n = a * (Sum fa) by A3,POLYNOM5:def 4
.= f.n by A5,A3,A2,Th1;
hence f.i = g.i;
end;
hence thesis by A1,FUNCT_1:2;
end;
theorem
for L being add-associative right_zeroed right_complementable
right-distributive commutative associative
non empty doubleLoopStr
for p,q being Polynomial of L
for a being Element of L
holds p *' (a * q) = a * (p *' q)
proof
let L be add-associative right_zeroed right_complementable
right-distributive commutative associative non empty doubleLoopStr;
let p,q be Polynomial of L;
let a being Element of L;
set f = p *' (a * q) , g = a * (p *' q);
A1: dom f = NAT by FUNCT_2:def 1 .= dom g by FUNCT_2:def 1;
now let i be object;
assume i in dom f;
then reconsider n = i as Element of NAT;
consider fr being FinSequence of the carrier of L such that
A2: len fr = n+1 & f.i = Sum fr &
for k being Element of NAT st k in dom fr
holds fr.k = p.(k-'1) * (a*q).(n+1-'k) by POLYNOM3:def 9;
consider fa being FinSequence of the carrier of L such that
A3: len fa = n+1 & (p *' q).i = Sum fa &
for k being Element of NAT st k in dom fa
holds fa.k = p.(k-'1) * q.(n+1-'k) by POLYNOM3:def 9;
Seg(len fa) = dom fr by A2,A3,FINSEQ_1:def 3;
then A4: dom fa = dom fr by FINSEQ_1:def 3;
A5: now let k be Element of NAT;
assume A6: k in dom fa;
then fa.k = fa/.k by PARTFUN1:def 6;
then reconsider x = fa.k as Element of L;
thus fr/.k = fr.k by A6,A4,PARTFUN1:def 6
.= p.(k-'1) * (a*q).(n+1-'k) by A4,A6,A2
.= p.(k-'1) * (a * q.(n+1-'k)) by POLYNOM5:def 4
.= a* (p.(k-'1) * q.(n+1-'k)) by GROUP_1:def 3
.= a * x by A6,A3
.= a * (fa/.k) by A6,PARTFUN1:def 6;
end;
g.n = a * (Sum fa) by A3,POLYNOM5:def 4
.= f.n by A5,Th1,A3,A2;
hence f.i = g.i;
end;
hence thesis by A1,FUNCT_1:2;
end;
registration
let L be add-associative right_zeroed right_complementable
well-unital commutative associative distributive
almost_left_invertible non trivial doubleLoopStr;
let p be non zero Polynomial of L;
let a be non zero Element of L;
cluster a * p -> non zero;
coherence
proof
a <> 0.L;
then len(a*p) = len p by POLYNOM5:25;
then a*p <> 0_.(L) by POLYNOM4:3,5;
hence thesis;
end;
end;
registration
let L be domRing-like add-associative right_zeroed right_complementable
distributive non trivial doubleLoopStr;
let p1,p2 be non zero Polynomial of L;
cluster p1 *' p2 -> non zero;
coherence
proof
reconsider x1 = p1 as Element of Polynom-Ring(L) by POLYNOM3:def 10;
reconsider x2 = p2 as Element of Polynom-Ring(L) by POLYNOM3:def 10;
p1 <> 0_.(L); then
A1: x1 <> 0.Polynom-Ring(L) by POLYNOM3:def 10;
p2 <> 0_.(L); then
x2 <> 0.Polynom-Ring(L) by POLYNOM3:def 10;
then x1 * x2 <> 0.Polynom-Ring(L) by A1,VECTSP_2:def 1;
then p1 *' p2 <> 0.Polynom-Ring(L) by POLYNOM3:def 10;
then p1 *' p2 <> 0_.(L) by POLYNOM3:def 10;
hence thesis;
end;
end;
theorem Th7:
for L being add-associative right_zeroed right_complementable distributive
Abelian domRing-like non trivial 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
let L be add-associative right_zeroed right_complementable distributive
Abelian domRing-like non trivial doubleLoopStr;
let p1,p2 be Polynomial of L;
let p3 be non zero Polynomial of L;
assume A1: p1 *' p3 = p2 *' p3;
reconsider x1 = p1 as Element of Polynom-Ring(L) by POLYNOM3:def 10;
reconsider x2 = p2 as Element of Polynom-Ring(L) by POLYNOM3:def 10;
reconsider x3 = p3 as Element of Polynom-Ring(L) by POLYNOM3:def 10;
p3 <> 0_.(L); then
A2: x3 <> 0.Polynom-Ring(L) by POLYNOM3:def 10;
A3: x1 * x3 = p2 *' p3 by A1,POLYNOM3:def 10
.= x2 * x3 by POLYNOM3:def 10;
x3 is right_mult-cancelable by A2,ALGSTR_0:def 37;
hence thesis by A3;
end;
registration
let L be non trivial ZeroStr;
let p be non zero Polynomial of L;
cluster degree p -> natural;
coherence
proof
p <> 0_.(L);
then deg p <> -1 by HURWITZ:20;
then len p <> 0;
then deg p + 1 > 0;
then deg p in NAT by INT_1:3,7;
hence thesis;
end;
end;
theorem Th8:
for L being add-associative right_zeroed right_complementable
unital right-distributive non empty doubleLoopStr
for p being Polynomial of L st deg p = 0
for x being Element of L holds eval(p,x) <> 0.L
proof
let L be add-associative right_zeroed right_complementable
unital right-distributive non empty doubleLoopStr;
let p be Polynomial of L;
assume A1: deg p = 0;
let x be Element of L;
assume eval(p,x) = 0.L;
then x is_a_root_of p by POLYNOM5:def 7;
then p is with_roots by POLYNOM5:def 8;
hence contradiction by A1,HURWITZ:24;
end;
theorem Th9:
for L being Abelian add-associative right_zeroed right_complementable
well-unital associative commutative distributive
almost_left_invertible non degenerated 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
let L be Abelian add-associative right_zeroed right_complementable
well-unital associative commutative distributive
almost_left_invertible non degenerated doubleLoopStr;
let p be Polynomial of L;
let x be Element of L;
A1: now assume rpoly(1,x) divides p;
then p mod rpoly(1,x) = 0_.(L);
then (p - (p div rpoly(1,x)) *' rpoly(1,x))
+ (p div rpoly(1,x)) *' rpoly(1,x)
= (p div rpoly(1,x)) *' rpoly(1,x) by POLYNOM3:28;
then A2: (p div rpoly(1,x)) *' rpoly(1,x)
= p + (-(p div rpoly(1,x)) *' rpoly(1,x)
+ (p div rpoly(1,x)) *' rpoly(1,x)) by POLYNOM3:26
.= p + ( ((p div rpoly(1,x)) *' rpoly(1,x))
- ((p div rpoly(1,x)) *' rpoly(1,x)) )
.= p + 0_.(L) by POLYNOM3:29
.= p by POLYNOM3:28;
A3: eval(rpoly(1,x),x) = x - x by HURWITZ:29 .= 0.L by RLVECT_1:15;
thus eval(p,x) = eval(p div rpoly(1,x),x) * 0.L by A3,A2,POLYNOM4:24
.= 0.L;
end;
eval(p,x) = 0.L implies rpoly(1,x) divides p by HURWITZ:35,POLYNOM5:def 7;
hence thesis by A1;
end;
theorem Th10:
for L being Abelian add-associative right_zeroed right_complementable
well-unital associative commutative distributive
almost_left_invertible domRing-like
non degenerated doubleLoopStr
for p,q being Polynomial of L
for x being Element of L st rpoly(1,x) divides (p*'q)
holds rpoly(1,x) divides p or rpoly(1,x) divides q
proof
let L be Abelian add-associative right_zeroed right_complementable
well-unital associative commutative distributive domRing-like
almost_left_invertible non degenerated doubleLoopStr;
let p,q be Polynomial of L;
let x be Element of L;
assume rpoly(1,x) divides (p*'q);
then eval(p*'q,x) = 0.L by Th9;
then A1: eval(p,x) * eval(q,x) = 0.L by POLYNOM4:24;
per cases by A1,VECTSP_2:def 1;
suppose eval(p,x) = 0.L;
hence thesis by Th9;
end;
suppose eval(q,x) = 0.L;
hence thesis by Th9;
end;
end;
theorem Th11:
for L being Abelian add-associative right_zeroed right_complementable
well-unital associative commutative distributive
almost_left_invertible non degenerated doubleLoopStr
for f being FinSequence of Polynom-Ring(L)
st for i being Nat st i in dom f ex z being Element of L st f.i = rpoly(1,z)
for p being Polynomial of L st p = Product f
holds p <> 0_.(L)
proof
let L be Abelian add-associative right_zeroed right_complementable
well-unital associative commutative distributive
almost_left_invertible non degenerated doubleLoopStr;
let f be FinSequence of Polynom-Ring(L);
assume A1:
for i being Nat st i in dom f ex z being Element of L st f.i = rpoly(1,z);
let p be Polynomial of L;
assume A2: p = Product f;
defpred P[Nat] means
for f being FinSequence of Polynom-Ring(L)
st len f = $1 &
for i being Nat st i in dom f ex z being Element of L st f.i = rpoly(1,z)
for p being Polynomial of L st p = Product f
holds p <> 0_.(L);
now let f be FinSequence of Polynom-Ring(L);
assume A3: len f = 0 &
for i being Nat st i in dom f ex z being Element of L st f.i = rpoly(1,z);
let p be Polynomial of L;
assume A4: p = Product f;
f = <*>(the carrier of Polynom-Ring(L)) by A3;
then p = 1_(Polynom-Ring(L)) by A4,GROUP_4:8
.= 1.(Polynom-Ring(L));
then p <> 0.(Polynom-Ring(L));
hence p <> 0_.(L) by POLYNOM3:def 10;
end;
then A5: P[0];
A6:now let n be Nat;
assume A7: P[n];
now let f be FinSequence of Polynom-Ring(L);
assume A8: len f = n+1 &
for i being Nat st i in dom f ex z being Element of L st f.i = rpoly(1,z);
let p be Polynomial of L;
assume A9: p = Product f;
f <> {} by A8;
then consider g being FinSequence, u being object such that
A10: f = g ^ <*u*> by FINSEQ_1:46;
reconsider g as FinSequence of Polynom-Ring(L) by A10,FINSEQ_1:36;
A11: dom f = Seg(n+1) by A8,FINSEQ_1:def 3;
1 <= n+1 by NAT_1:11;
then A12: n+1 in dom f by A11;
A13: n+1 = len g + len <*u*> by A8,A10,FINSEQ_1:22
.= len g + 1 by FINSEQ_1:40;
then f.(n+1) = u by A10,FINSEQ_1:42;
then consider z being Element of L such that
A14: u = rpoly(1,z) by A8,A12;
reconsider u as Element of Polynom-Ring(L) by A14,POLYNOM3:def 10;
reconsider q = Product g as Polynomial of L by POLYNOM3:def 10;
A15: Product f = (Product g) * u by A10,GROUP_4:6;
A16: u <> 0.(Polynom-Ring(L)) by A14,POLYNOM3:def 10;
now let i be Nat;
assume A17: i in dom g;
then A18: g.i = f.i by A10,FINSEQ_1:def 7;
dom g c= dom f by A10,FINSEQ_1:26;
hence ex z being Element of L st g.i = rpoly(1,z) by A17,A18,A8;
end;
then q <> 0_.(L) by A7,A13;
then q <> 0.(Polynom-Ring(L)) by POLYNOM3:def 10;
then p <> 0.(Polynom-Ring(L)) by A9,A16,A15,VECTSP_2:def 1;
hence p <> 0_.(L) by POLYNOM3:def 10;
end;
hence P[n+1];
end;
A19: for n being Nat holds P[n] from NAT_1:sch 2(A5,A6);
len f is Nat;
hence thesis by A1,A2,A19;
end;
theorem Th12:
for L being Abelian add-associative right_zeroed right_complementable
well-unital associative commutative distributive
almost_left_invertible domRing-like
non degenerated doubleLoopStr
for f being FinSequence of Polynom-Ring(L)
st for i being Nat st i in dom f ex z being Element of L st f.i = rpoly(1,z)
for p being Polynomial of L st p = Product f
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
let L be Field;
let f be FinSequence of Polynom-Ring(L);
assume A1: for i being Nat st i in dom f
ex z being Element of L st f.i = rpoly(1,z);
let p be Polynomial of L;
assume A2: p = Product f;
let x be Element of L;
A3: now assume ex i being Nat st i in dom f & f.i = rpoly(1,x); then
consider i being Nat such that
A4: i in dom f & f.i = rpoly(1,x);
reconsider g = Del(f,i) as FinSequence of Polynom-Ring(L) by FINSEQ_3:105;
reconsider q = Product g as Polynomial of L by POLYNOM3:def 10;
A5: f/.i = rpoly(1,x) by A4,PARTFUN1:def 6;
Product f = (f/.i) * Product g by A4,Th3;
then p = rpoly(1,x) *' q by A2,A5,POLYNOM3:def 10;
then A6: eval(p,x) = eval(rpoly(1,x),x) * eval(q,x) by POLYNOM4:24;
eval(rpoly(1,x),x) = x - x by HURWITZ:29 .= 0.L by RLVECT_1:15;
hence eval(p,x) = 0.L by A6;
end;
now assume A7: eval(p,x) = 0.L;
defpred P[Nat] means
for f being FinSequence of Polynom-Ring(L)
st len f = $1 & for i being Nat st i in dom f
ex z being Element of L st f.i = rpoly(1,z)
for p being Polynomial of L st p = Product f
for x being Element of L holds
eval(p,x) = 0.L implies ex i being Nat st i in dom f & f.i = rpoly(1,x);
now let f be FinSequence of Polynom-Ring(L);
assume A8: len f = 0 & for i being Nat st i in dom f
ex z being Element of L st f.i = rpoly(1,z);
let p be Polynomial of L;
assume A9: p = Product f;
let x be Element of L;
assume A10: eval(p,x) = 0.L;
f = <*>(the carrier of Polynom-Ring(L)) by A8;
then p = 1_(Polynom-Ring(L)) by A9,GROUP_4:8
.= 1_.(L) by POLYNOM3:def 10;
hence ex i being Nat st i in dom f & f.i = rpoly(1,x) by A10,POLYNOM4:18;
end;
then A11: P[0];
A12:now let n be Nat;
assume A13: P[n];
now let f be FinSequence of Polynom-Ring(L);
assume A14: len f = n+1 & for i being Nat st i in dom f
ex z being Element of L st f.i = rpoly(1,z);
let p be Polynomial of L;
assume A15: p = Product f;
let x be Element of L;
assume A16: eval(p,x) = 0.L;
f <> {} by A14;
then consider g being FinSequence, u being object such that
A17: f = g ^ <*u*> by FINSEQ_1:46;
reconsider g as FinSequence of Polynom-Ring(L) by A17,FINSEQ_1:36;
A18: dom f = Seg(n+1) by A14,FINSEQ_1:def 3;
1 <= n+1 by NAT_1:11;
then A19: n+1 in dom f by A18;
A20: n+1 = len g + len <*u*> by A14,A17,FINSEQ_1:22
.= len g + 1 by FINSEQ_1:40;
A21: f.(n+1) = u by A20,A17,FINSEQ_1:42;
then consider z being Element of L such that
A22: u = rpoly(1,z) by A14,A19;
reconsider u as Element of Polynom-Ring(L) by A22,POLYNOM3:def 10;
reconsider q = Product g as Polynomial of L by POLYNOM3:def 10;
Product f = (Product g) * u by A17,GROUP_4:6
.= q *' rpoly(1,z) by A22,POLYNOM3:def 10;
then A23: eval(p,x)
= eval(q,x) * eval(rpoly(1,z),x) by A15,POLYNOM4:24;
A24: now let i be Nat;
assume A25: i in dom g;
A26: dom g c= dom f by A17,FINSEQ_1:26;
g.i = f.i by A25,A17,FINSEQ_1:def 7;
hence ex z being Element of L st g.i = rpoly(1,z) by A25,A26,A14;
end;
now per cases by A23,A16,VECTSP_2:def 1;
suppose eval(q,x) = 0.L;
then consider i being Nat such that
A27: i in dom g & g.i = rpoly(1,x) by A20,A24,A13;
A28: dom g c= dom f by A17,FINSEQ_1:26;
f.i = rpoly(1,x) by A27,A17,FINSEQ_1:def 7;
hence ex i being Nat st i in dom f & f.i = rpoly(1,x) by A28,A27;
end;
suppose eval(rpoly(1,z),x) = 0.L;
then x - z = 0.L by HURWITZ:29;
then x = z by RLVECT_1:21;
hence ex i being Nat st i in dom f & f.i = rpoly(1,x)
by A19,A21,A22;
end;
end;
hence ex i being Nat st i in dom f & f.i = rpoly(1,x);
end;
hence P[n+1];
end;
A29: for n being Nat holds P[n] from NAT_1:sch 2(A11,A12);
len f is Nat;
hence ex i being Nat st i in dom f & f.i = rpoly(1,x) by A7,A1,A2,A29;
end;
hence thesis by A3;
end;
begin :: Common Roots of Polynomials
definition
let L be unital non empty doubleLoopStr;
let p1,p2 be Polynomial of L;
let x be Element of L;
pred x is_a_common_root_of p1,p2 means
x is_a_root_of p1 & x is_a_root_of p2;
end;
definition
let L be unital non empty doubleLoopStr;
let p1,p2 be Polynomial of L;
pred p1,p2 have_a_common_root means
ex x being Element of L st x is_a_common_root_of p1,p2;
end;
notation
let L be unital non empty 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:
for L being Abelian add-associative right_zeroed right_complementable
unital distributive non empty 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
let L be Abelian add-associative right_zeroed right_complementable
unital distributive non empty doubleLoopStr;
let p be Polynomial of L;
let x be Element of L;
assume A1: x is_a_root_of p;
eval(-p,x) = - eval(p,x) by POLYNOM4:20
.= - 0.L by A1,POLYNOM5:def 7
.= 0.L by RLVECT_1:12;
hence x is_a_root_of -p by POLYNOM5:def 7;
end;
theorem Th14:
for L being Abelian add-associative right_zeroed right_complementable
unital left-distributive non empty 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
let L be Abelian add-associative right_zeroed right_complementable
unital left-distributive non empty doubleLoopStr;
let p1,p2 be Polynomial of L;
let x be Element of L;
assume x is_a_common_root_of p1,p2;
then x is_a_root_of p1 & x is_a_root_of p2;
then A1: eval(p1,x) = 0.L & eval(p2,x) = 0.L by POLYNOM5:def 7;
eval(p1+p2,x) = 0.L + 0.L by A1,POLYNOM4:19
.= 0.L by RLVECT_1:def 4;
hence x is_a_root_of p1+p2 by POLYNOM5:def 7;
end;
theorem
for L being Abelian add-associative right_zeroed right_complementable
unital distributive non empty 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
for L being Abelian add-associative right_zeroed right_complementable
unital distributive non empty 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
let L be Abelian add-associative right_zeroed right_complementable
unital distributive non empty doubleLoopStr;
let p,q be Polynomial of L;
let x be Element of L;
assume x is_a_common_root_of p,q;
then A1: x is_a_root_of p & x is_a_root_of q;
then A2: eval(p,x) = 0.L by POLYNOM5:def 7;
A3: eval(q,x) = 0.L by A1,POLYNOM5:def 7;
eval(p+q,x) = 0.L + 0.L by A2,A3,POLYNOM4:19
.= 0.L by RLVECT_1:def 4;
hence thesis by POLYNOM5:def 7;
end;
theorem
for L being Abelian add-associative right_zeroed right_complementable
well-unital associative commutative distributive
almost_left_invertible non trivial doubleLoopStr
for p1,p2 being Polynomial of L
st p1 divides p2 & p1 is with_roots holds p1,p2 have_common_roots
proof
let L be Abelian add-associative right_zeroed right_complementable
well-unital associative commutative distributive almost_left_invertible
non trivial doubleLoopStr;
let p1,p2 be Polynomial of L;
assume A1: p1 divides p2 & p1 is with_roots;
per cases;
suppose A2: p1 = 0_.(L);
p2 mod p1 = 0_.(L) by A1;
then 0_.(L) = p2 - 0_.(L)by A2,POLYNOM3:34
.= p2 + 0_.(L) by HURWITZ:9;
then A3: p2 = 0_.(L) by POLYNOM3:28;
eval(0_.(L),0.L) = 0.L by POLYNOM4:17;
then 0.L is_a_root_of 0_.(L) by POLYNOM5:def 7;
then 0.L is_a_common_root_of p1,p2 by A2,A3;
hence thesis;
end;
suppose p1 <> 0_.(L);
then consider s being Polynomial of L such that
A4: s *' p1 = p2 by A1,HURWITZ:34;
consider x being Element of L such that
A5: x is_a_root_of p1 by A1,POLYNOM5:def 8;
A6: eval(p1,x) = 0.L by A5,POLYNOM5:def 7;
eval(p2,x) = eval(s,x) * eval(p1,x) by A4,POLYNOM4:24
.= 0.L by A6;
then x is_a_root_of p2 by POLYNOM5:def 7;
then x is_a_common_root_of p1,p2 by A5;
hence thesis;
end;
end;
definition
let L be unital non empty doubleLoopStr;
let p,q be Polynomial of L;
func Common_Roots(p,q) -> Subset of L equals
{ x where x is Element of L : x is_a_common_root_of p,q };
coherence
proof
set M = { x where x is Element of L : x is_a_common_root_of p,q };
now let u be object;
assume u in M;
then ex x being Element of L st u = x & x is_a_common_root_of p,q;
hence u in the carrier of L;
end;
hence M is Subset of L by TARSKI:def 3;
end;
end;
begin :: Normalized Polynomials
definition
let L be non empty ZeroStr;
let p be Polynomial of L;
func Leading-Coefficient(p) -> Element of L equals
p.(len p-'1);
coherence;
end;
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 LC p -> non zero;
coherence
proof
p <> 0_.(L);
then len p <> 0 by POLYNOM4:5;
then 0 + 1 < len p + 1 by XREAL_1:8;
then len p >= 1 by NAT_1:13;
then (len p-'1) + 1 = len p by XREAL_1:235;
then p.(len p-'1) <> 0.L by ALGSEQ_1:10;
hence thesis;
end;
end;
theorem Th18:
for L being add-associative right_zeroed right_complementable
well-unital commutative associative distributive
almost_left_invertible non empty doubleLoopStr
for p being Polynomial of L
for a being Element of L holds LC(a * p) = a * LC(p)
proof
let L be add-associative right_zeroed right_complementable
well-unital commutative associative distributive
almost_left_invertible non empty doubleLoopStr;
let p be Polynomial of L;
let a be Element of L;
per cases;
suppose A1: a = 0.L;
then A2: a * LC(p) = 0.L;
a * p = 0_.(L) by A1,POLYNOM5:26;
hence thesis by A2,FUNCOP_1:7;
end;
suppose A3: a <> 0.L;
thus LC(a * p) = a * (p.(len(a*p)-'1)) by POLYNOM5:def 4
.= a * LC(p) by A3,POLYNOM5:25;
end;
end;
definition
let L be non empty doubleLoopStr;
let p be Polynomial of L;
attr p is normalized means
LC p = 1.L;
end;
registration
let L be add-associative right_zeroed right_complementable
well-unital commutative associative distributive
almost_left_invertible non trivial doubleLoopStr;
let p be non zero Polynomial of L;
cluster (1.L / LC p) * p -> normalized;
coherence
proof
A1: LC p <> 0.L;
LC((1.L / LC p) * p) = (1.L / LC p) * LC(p) by Th18
.= 1.L * ((LC p)" * LC(p))
.= 1.L * 1.L by A1,VECTSP_1:def 10
.= 1.L;
hence thesis;
end;
end;
registration
let L be Field;
let p be non zero Polynomial of L;
cluster NormPolynomial(p) -> normalized;
coherence
proof
set q = NormPolynomial p;
A1: p <> 0_.L;
then q.(len p-'1) = 1.L by POLYNOM4:5,POLYNOM5:56;
then LC q = 1.L by A1,POLYNOM4:5,POLYNOM5:57;
hence thesis;
end;
end;
begin :: Rational Functions
definition
let L be non trivial multLoopStr_0;
mode rational_function of L -> set means :Def8:
ex p1 being Polynomial of L st
ex p2 being non zero Polynomial of L st it = [p1,p2];
existence
proof
reconsider RF = [the Polynomial of L,the non zero Polynomial of L] as set
by TARSKI:1;
take RF;
thus thesis;
end;
end;
definition
let L be non trivial multLoopStr_0;
let p1 be Polynomial of L;
let p2 be non zero Polynomial of L;
redefine func [p1,p2] -> rational_function of L;
coherence
proof
reconsider p = [p1,p2] as set by TARSKI:1;
ex q1 being Polynomial of L st
ex q2 being non zero Polynomial of L st p = [q1,q2];
hence thesis by Def8;
end;
end;
definition
let L be non trivial multLoopStr_0;
let z be rational_function of L;
redefine func z`1 -> Polynomial of L;
coherence
proof
consider p1 being Polynomial of L such that
A1: ex p2 being non zero Polynomial of L st z = [p1,p2] by Def8;
consider p2 being non zero Polynomial of L such that
A2: z = [p1,p2] by A1;
thus thesis by A2;
end;
redefine func z`2 -> non zero Polynomial of L;
coherence
proof
consider p1 being Polynomial of L such that
A3: ex p2 being non zero Polynomial of L st z = [p1,p2] by Def8;
consider p2 being non zero Polynomial of L such that
A4: z = [p1,p2] by A3;
thus thesis by A4;
end;
end;
definition
let L be non trivial multLoopStr_0;
let z be rational_function of L;
attr z is zero means :Def9:
z`1 = 0_.(L);
end;
registration
let L be non trivial multLoopStr_0;
cluster non zero for rational_function of L;
existence
proof
set p1 = the non zero Polynomial of L;
set p2 = the non zero Polynomial of L;
take [p1,p2];
thus thesis;
end;
end;
theorem Th19:
for L being non trivial multLoopStr_0
for z being rational_function of L holds z = [z`1,z`2]
proof
let L be non trivial multLoopStr_0;
let z be rational_function of L;
consider p1 being Polynomial of L such that
A1: ex p2 being non zero Polynomial of L st z = [p1,p2] by Def8;
consider p2 being non zero Polynomial of L such that
A2: z = [p1,p2] by A1;
thus thesis by A2;
end;
definition
let L be add-associative right_zeroed right_complementable distributive
unital non trivial doubleLoopStr;
let z be rational_function of L;
attr z is irreducible means :Def10:
z`1, z`2 have_no_common_roots;
end;
notation
let L be add-associative right_zeroed right_complementable distributive
unital non trivial doubleLoopStr;
let z be rational_function of L;
antonym z is reducible for z is irreducible;
end;
definition
let L be add-associative right_zeroed right_complementable distributive
unital non trivial doubleLoopStr;
let z be rational_function of L;
attr z is normalized means :Def11:
z is irreducible & z`2 is normalized;
end;
registration
let L be add-associative right_zeroed right_complementable distributive
unital non trivial doubleLoopStr;
cluster normalized -> irreducible for rational_function of L;
coherence;
end;
registration
let L be Abelian add-associative right_zeroed right_complementable
well-unital associative distributive commutative
almost_left_invertible domRing-like non trivial doubleLoopStr;
let z be rational_function of L;
cluster LC(z`2) -> non zero;
coherence;
end;
definition
let L be Abelian add-associative right_zeroed right_complementable
well-unital associative distributive commutative
almost_left_invertible domRing-like non trivial doubleLoopStr;
let z be rational_function of L;
func NormRationalFunction z -> rational_function of L equals
[(1.L / LC(z`2)) * z`1, (1.L / LC(z`2)) * z`2];
coherence;
end;
notation
let L be Abelian add-associative right_zeroed right_complementable
well-unital associative distributive commutative
almost_left_invertible domRing-like non trivial doubleLoopStr;
let z be rational_function of L;
synonym NormRatF z for NormRationalFunction z;
end;
registration
let L be Abelian add-associative right_zeroed right_complementable
well-unital associative distributive commutative
almost_left_invertible domRing-like non trivial doubleLoopStr;
let z be non zero rational_function of L;
cluster NormRationalFunction z -> non zero;
coherence
proof
z`1 <> 0_.(L) by Def9; then
reconsider z1 = z`1 as non zero Polynomial of L by UPROOTS:def 5;
(1.L / LC(z`2)) * z1 is non zero;
then (NormRatF z)`1 <> 0_.(L);
hence thesis;
end;
end;
definition
let L be non degenerated multLoopStr_0;
func 0._(L) -> rational_function of L equals
[ 0_.(L), 1_.(L) ];
coherence;
func 1._(L) -> rational_function of L equals
[ 1_.(L), 1_.(L) ];
coherence;
end;
registration
let L be add-associative right_zeroed right_complementable distributive
associative well-unital non degenerated doubleLoopStr;
cluster 0._(L) -> normalized;
coherence
proof
set z = [ 0_.(L), 1_.(L) ]; set p1 = z`1, p2 = z`2;
now assume p1, p2 have_a_common_root;
then consider x being Element of L such that
A1: x is_a_common_root_of p1,p2;
x is_a_root_of p2 by A1;
then eval(p2,x) = 0.L by POLYNOM5:def 7;
hence contradiction by POLYNOM4:18;
end;
then A2: z is irreducible;
A3: len(1_.(L)) = 1 by POLYNOM4:4;
len(1_.(L))-'1 = 1 - 1 by A3,XREAL_0:def 2;
then LC(1_.(L)) = 1.L by POLYNOM3:30;
then p2 is normalized;
hence thesis by A2;
end;
end;
registration
let L be non degenerated multLoopStr_0;
cluster 1._(L) -> non zero;
coherence;
end;
registration
let L be add-associative right_zeroed right_complementable distributive
associative well-unital non degenerated doubleLoopStr;
cluster 1._(L) -> irreducible;
coherence
proof
set z = [ 1_.(L), 1_.(L) ];
set p1 = z`1, p2 = z`2;
now
assume p1, p2 have_a_common_root;
then consider x being Element of L such that
A1: x is_a_common_root_of p1,p2;
x is_a_root_of p2 by A1;
then eval(p2,x) = 0.L by POLYNOM5:def 7;
hence contradiction by POLYNOM4:18;
end;
hence thesis;
end;
end;
registration
let L be add-associative right_zeroed right_complementable distributive
associative well-unital non degenerated doubleLoopStr;
cluster irreducible non zero for rational_function of L;
existence
proof
take 1._(L);
thus thesis;
end;
end;
registration
let L be add-associative right_zeroed right_complementable distributive
Abelian associative well-unital non degenerated doubleLoopStr;
let x be Element of L;
cluster [ rpoly(1,x), rpoly(1,x) ] -> reducible non zero
for rational_function of L;
coherence
proof
set z = [ rpoly(1,x), rpoly(1,x) ];
x is_a_root_of rpoly(1,x) by HURWITZ:30;
then x is_a_root_of z`1;
then x is_a_common_root_of z`1,z`2;
then z`1, z`2 have_common_roots;
then z is reducible;
hence thesis;
end;
end;
registration
let L be add-associative right_zeroed right_complementable distributive
Abelian associative well-unital non degenerated doubleLoopStr;
cluster reducible non zero for rational_function of L;
existence
proof
set x = the Element of L;
take z = [ rpoly(1,x), rpoly(1,x) ];
thus thesis;
end;
end;
registration
let L be add-associative right_zeroed right_complementable distributive
associative well-unital non degenerated doubleLoopStr;
cluster normalized for rational_function of L;
existence
proof
take 0._(L);
thus thesis;
end;
end;
registration
let L be non degenerated multLoopStr_0;
cluster 0._(L) -> zero;
coherence;
end;
registration
let L be add-associative right_zeroed right_complementable distributive
associative well-unital non degenerated doubleLoopStr;
cluster 1._(L) -> normalized;
coherence
proof
len(1_.(L)) = 1 by POLYNOM4:4;
then len(1_.(L))-'1 = 1 - 1 by XREAL_0:def 2;
then LC(1_.(L)) = 1.L by POLYNOM3:30;
then [ 1_.(L), 1_.(L) ]`2 is normalized;
hence 1._(L) is normalized;
end;
end;
definition
let L be domRing-like add-associative right_zeroed right_complementable
distributive non trivial doubleLoopStr;
let p,q be rational_function of L;
func p + q -> rational_function of L equals
[ p`1 *' q`2 + p`2 *' q`1, p`2 *' q`2];
coherence;
end;
definition
let L be domRing-like add-associative right_zeroed right_complementable
distributive non trivial doubleLoopStr;
let p,q be rational_function of L;
func p *' q -> rational_function of L equals
[ p`1 *' q`1, p`2 *' q`2];
coherence;
end;
theorem Th20:
for L being add-associative right_zeroed right_complementable
well-unital commutative associative distributive
almost_left_invertible non trivial 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
let L be add-associative right_zeroed right_complementable
well-unital commutative associative distributive
almost_left_invertible non trivial doubleLoopStr;
let p be rational_function of L;
let a be non zero Element of L;
set ap = [a * p`1, a * p`2];
A1: now assume A2: p is irreducible;
assume ap is reducible;
then ap`1, ap`2 have_common_roots;
then consider x being Element of L such that
A3: x is_a_common_root_of ap`1, ap`2;
x is_a_root_of ap`1 & x is_a_root_of ap`2 by A3;
then A4: eval(ap`1,x) = 0.L & eval(ap`2,x) = 0.L by POLYNOM5:def 7;
then eval(a * p`1,x) = 0.L;
then a * eval(p`1,x) = 0.L by POLYNOM5:30;
then eval(p`1,x) = 0.L by VECTSP_2:def 1;
then A5: x is_a_root_of p`1 by POLYNOM5:def 7;
eval(a * p`2,x) = 0.L by A4;
then a * eval(p`2,x) = 0.L by POLYNOM5:30;
then eval(p`2,x) = 0.L by VECTSP_2:def 1;
then x is_a_root_of p`2 by POLYNOM5:def 7;
then x is_a_common_root_of p`1,p`2 by A5;
then p`1,p`2 have_common_roots;
hence [a * p`1, a * p`2] is irreducible by A2;
end;
now assume A6: ap is irreducible;
assume p is reducible;
then p`1, p`2 have_common_roots;
then consider x being Element of L such that
A7: x is_a_common_root_of p`1, p`2;
x is_a_root_of p`1 & x is_a_root_of p`2 by A7;
then A8: eval(p`1,x) = 0.L & eval(p`2,x) = 0.L by POLYNOM5:def 7;
then a * eval(p`1,x) = 0.L;
then eval(a * p`1,x) = 0.L by POLYNOM5:30;
then eval(ap`1,x) = 0.L;
then A9: x is_a_root_of ap`1 by POLYNOM5:def 7;
a * eval(p`2,x) = 0.L by A8;
then eval(a * p`2,x) = 0.L by POLYNOM5:30;
then eval(ap`2,x) = 0.L;
then x is_a_root_of ap`2 by POLYNOM5:def 7;
then x is_a_common_root_of ap`1,ap`2 by A9;
then ap`1,ap`2 have_common_roots;
hence p is irreducible by A6;
end;
hence thesis by A1;
end;
begin :: Normalized Rational Functions
Lm1:
for L be Abelian add-associative right_zeroed right_complementable
well-unital associative distributive commutative
domRing-like non trivial doubleLoopStr
for z be rational_function of L holds
z is irreducible implies
ex z1 being rational_function of L,
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
ex x being Element of L st x is_a_common_root_of z`1,z`2 &
f.i = rpoly(1,x)
proof
let L be Abelian add-associative right_zeroed right_complementable
well-unital associative distributive commutative
domRing-like non trivial doubleLoopStr;
let z be rational_function of L;
assume A1: z is irreducible;
take z;
reconsider e = 1_.(L) as non zero Polynomial of L;
take e;
reconsider f = <*>(the carrier of Polynom-Ring(L))
as FinSequence of Polynom-Ring(L);
thus z = [z`1,z`2] by Th19 .= [e*'z`1,z`2] by POLYNOM3:35
.= [e*'z`1,e*'z`2] by POLYNOM3:35;
thus z is irreducible by A1;
take f;
Product f = 1_(Polynom-Ring(L)) by GROUP_4:8;
hence thesis by POLYNOM3:def 10;
end;
theorem Th21:
for L being Abelian add-associative right_zeroed right_complementable
well-unital associative distributive commutative
domRing-like non trivial doubleLoopStr
for z being rational_function of L
ex z1 being rational_function of L,
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
ex x being Element of L st x is_a_common_root_of z`1,z`2 &
f.i = rpoly(1,x)
proof
let L be Abelian add-associative right_zeroed right_complementable
well-unital associative distributive commutative
domRing-like non trivial doubleLoopStr;
let z be rational_function of L;
defpred P[Nat] means
for z being rational_function of L st max(deg(z`1),deg(z`2)) = $1
ex z1 being rational_function of L,
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
ex x being Element of L st x is_a_common_root_of z`1,z`2 &
f.i = rpoly(1,x);
now let z be rational_function of L;
assume max(deg(z`1),deg(z`2)) = 0;
then deg(z`2) <= 0 by XXREAL_0:25;
then A1: deg(z`2) = 0;
A2:now assume ex x be Element of L st x is_a_root_of z`2;
then consider y being Element of L such that
A3: y is_a_root_of z`2;
eval(z`2,y) = 0.L by A3,POLYNOM5:def 7;
hence contradiction by A1,Th8;
end;
now assume z is reducible;
then z`1,z`2 have_common_roots;
then consider x being Element of L such that
A4: x is_a_common_root_of z`1,z`2;
x is_a_root_of z`2 by A4;
hence contradiction by A2;
end;
hence
ex z1 being rational_function of L,
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
ex x being Element of L st x is_a_common_root_of z`1,z`2 &
f.i = rpoly(1,x) by Lm1;
end;
then A5: P[0];
A6: now let n be Nat;
assume A7: P[n];
for z being rational_function of L st max(deg(z`1),deg(z`2)) = n+1
ex z1 being rational_function of L,
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
ex x being Element of L st x is_a_common_root_of z`1,z`2 &
f.i = rpoly(1,x)
proof
let z being rational_function of L;
assume A8: max(deg(z`1),deg(z`2)) = n+1;
per cases;
suppose z is irreducible;
hence thesis by Lm1;
end;
suppose z is reducible;
then z`1,z`2 have_common_roots;
then consider x being Element of L such that
A9: x is_a_common_root_of z`1,z`2;
A10: x is_a_root_of z`1 & x is_a_root_of z`2 by A9;
consider q2 being Polynomial of L such that
A11: z`2 = rpoly(1,x) *' q2 by A10,HURWITZ:33;
consider q1 being Polynomial of L such that
A12: z`1 = rpoly(1,x) *' q1 by A10,HURWITZ:33;
q2 <> 0_.(L) by A11,POLYNOM3:34;
then reconsider q2 as non zero Polynomial of L by UPROOTS:def 5;
set q = [q1,q2];
max(deg(q`1),deg(q`2)) = n
proof
A13: deg(z`2) = deg(rpoly(1,x)) + deg(q2) by A11,HURWITZ:23
.= 1 + deg(q2) by HURWITZ:27;
per cases by XXREAL_0:16;
suppose A14: max(deg(z`1),deg(z`2)) = deg(z`1);
then z`1 <> 0_.(L) by A8,HURWITZ:20;
then q1 <> 0_.(L) by A12,POLYNOM3:34; then
A15: deg(z`1) = deg(rpoly(1,x)) + deg(q1) by A12,HURWITZ:23
.= 1 + deg(q1) by HURWITZ:27;
A16: deg(z`2) <= n + 1 by A8,XXREAL_0:25;
deg q2 + 1 - 1 <= n + 1 - 1 by A13,A16,XREAL_1:9;
hence thesis by A15,A14,A8,XXREAL_0:def 10;
end;
suppose A17: max(deg(z`1),deg(z`2)) = deg(z`2);
A18: deg(z`1) <= n + 1 by A8,XXREAL_0:25;
now per cases;
suppose q1 = 0_.(L);
hence deg q1 <= deg q2 by HURWITZ:20;
end;
suppose q1 <> 0_.(L); then
deg(z`1) = deg(rpoly(1,x)) + deg(q1) by A12,HURWITZ:23
.= 1 + deg(q1) by HURWITZ:27;
hence deg q1 <= deg q2 by A18,A13,A17,A8,XREAL_1:9;
end;
end;
hence thesis by A17,A13,A8,XXREAL_0:def 10;
end;
end;
then consider z1q being rational_function of L,
z2q being non zero Polynomial of L such that
A19: q = [z2q*'z1q`1,z2q*'z1q`2] & z1q is irreducible &
ex f being FinSequence of Polynom-Ring(L)
st z2q = Product f &
for i being Element of NAT st i in dom f
ex x being Element of L st x is_a_common_root_of q`1,q`2 &
f.i = rpoly(1,x) by A7;
take z1 = z1q;
set z2 = rpoly(1,x) *' z2q;
reconsider z2 as non zero Polynomial of L;
take z2;
consider fq being FinSequence of Polynom-Ring(L) such that
A20: z2q = Product fq &
for i being Element of NAT st i in dom fq
ex x being Element of L st x is_a_common_root_of q`1,q`2 &
fq.i = rpoly(1,x) by A19;
reconsider rp = rpoly(1,x) as Element of Polynom-Ring(L)
by POLYNOM3:def 10;
set f = <*rp*> ^ fq;
A21: Product f = rp * Product(fq) by GROUP_4:7
.= z2 by A20,POLYNOM3:def 10;
A22: z = [z2*'z1`1,z2*'z1`2]
proof
A23: q1 = z2q*' z1q`1 by A19,XTUPLE_0:def 2;
A24: q2 = z2q*' z1q`2 by A19,XTUPLE_0:def 3;
A25: (z2 *' z1`1) = z`1 by A23,A12,POLYNOM3:33;
A26: (z2 *' z1`2) = z`2 by A24,A11,POLYNOM3:33;
thus z = [z2*'z1`1,z2*'z1`2] by A25,A26,Th19;
end;
A27: now let i be Element of NAT;
assume A28: i in dom f;
now per cases by A28,FINSEQ_1:25;
suppose A29: i in dom<*rp*>;
then A30: i in {1} by FINSEQ_1:2,38;
f.i = <*rp*>.i by A29,FINSEQ_1:def 7
.= <*rp*>.1 by A30,TARSKI:def 1
.= rpoly(1,x) by FINSEQ_1:40;
hence ex x being Element of L st x is_a_common_root_of z`1,z`2 &
f.i = rpoly(1,x) by A9;
end;
suppose ex n being Nat st n in dom fq & i = len<*rp*> + n;
then consider n being Nat such that
A31: n in dom fq & i = len<*rp*> + n;
f.i = fq.n by A31,FINSEQ_1:def 7;
then consider y being Element of L such that
A32: y is_a_common_root_of q`1,q`2 & f.i = rpoly(1,y) by A31,A20;
A33: y is_a_root_of q`1 & y is_a_root_of q`2 by A32;
then A34: 0.L = eval(q1,y) by POLYNOM5:def 7;
A35: eval(z`1,y) = eval(rpoly(1,x),y) * eval(q1,y) by A12
,POLYNOM4:24
.= 0.L by A34;
A36: 0.L = eval(q2,y) by A33,POLYNOM5:def 7;
eval(z`2,y) = eval(rpoly(1,x),y) * eval(q2,y) by A11,POLYNOM4:24
.= 0.L by A36;
then y is_a_root_of z`1 & y is_a_root_of z`2 by A35,POLYNOM5:def 7;
then y is_a_common_root_of z`1,z`2;
hence ex x being Element of L st x is_a_common_root_of z`1,z`2 &
f.i = rpoly(1,x) by A32;
end;
end;
hence ex x being Element of L st x is_a_common_root_of z`1,z`2 &
f.i = rpoly(1,x);
end;
thus thesis by A19,A21,A22,A27;
end;
end;
hence P[n+1];
end;
A37: for n being Nat holds P[n] from NAT_1:sch 2(A5,A6);
max(deg(z`1),deg(z`2)) >= deg(z`2) by XXREAL_0:25;
then max(deg(z`1),deg(z`2)) >= 0;
then max(deg(z`1),deg(z`2)) in NAT by INT_1:3;
hence thesis by A37;
end;
Lm2:
for L be Abelian add-associative right_zeroed right_complementable
well-unital associative distributive commutative
almost_left_invertible domRing-like non trivial doubleLoopStr
for z be rational_function of L st z is irreducible
for z1 being rational_function of L,
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
ex x being Element of L st x is_a_common_root_of z`1,z`2 &
f.i = rpoly(1,x)
for g1 being rational_function of L,
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
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
let L be Abelian add-associative right_zeroed right_complementable
well-unital associative distributive commutative
almost_left_invertible domRing-like non trivial doubleLoopStr;
let z be rational_function of L;
assume A1: z is irreducible;
let z1 be rational_function of L,
z2 be non zero Polynomial of L;
assume A2: 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
ex x being Element of L st x is_a_common_root_of z`1,z`2 &
f.i = rpoly(1,x);
let g1 be rational_function of L,
g2 be non zero Polynomial of L;
assume A3: 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
ex x being Element of L st x is_a_common_root_of z`1,z`2 &
f.i = rpoly(1,x);
consider f being FinSequence of Polynom-Ring(L) such that
A4: z2 = Product f &
for i being Element of NAT st i in dom f
ex x being Element of L st x is_a_common_root_of z`1,z`2 &
f.i = rpoly(1,x) by A2;
now assume f <> <*>(the carrier of Polynom-Ring(L));
then A5: dom f <> {};
let i be Element of dom f;
reconsider i as Nat;
A6: i in dom f by A5;
consider x being Element of L such that
A7: x is_a_common_root_of z`1,z`2 & f.i = rpoly(1,x) by A6,A4;
z`1,z`2 have_common_roots by A7;
hence contradiction by A1;
end;
hence A8: z2 = 1_(Polynom-Ring(L)) by A4,GROUP_4:8
.= 1_.(L) by POLYNOM3:def 10;
then A9: z2 *' z1`1 = z1`1 by POLYNOM3:35;
z2 *' z1`2 = z1`2 by A8,POLYNOM3:35;
then A10: z = z1 by A9,A2,Th19;
consider h being FinSequence of Polynom-Ring(L) such that
A11: g2 = Product h &
for i being Element of NAT st i in dom h
ex x being Element of L st x is_a_common_root_of z`1,z`2 &
h.i = rpoly(1,x) by A3;
now assume h <> <*>(the carrier of Polynom-Ring(L));
then A12: dom h <> {};
let i be Element of dom h;
reconsider i as Nat;
A13: i in dom h by A12;
consider x being Element of L such that
A14: x is_a_common_root_of z`1,z`2 & h.i = rpoly(1,x) by A13,A11;
z`1,z`2 have_common_roots by A14;
hence contradiction by A1;
end;
hence A15: g2 = 1_(Polynom-Ring(L)) by A11,GROUP_4:8
.= 1_.(L) by POLYNOM3:def 10;
then A16: g2 *' g1`1 = g1`1 by POLYNOM3:35;
g2 *' g1`2 = g1`2 by A15,POLYNOM3:35;
hence z1 = g1 by A10,A16,A3,Th19;
end;
Lm3:
for L be Abelian add-associative right_zeroed right_complementable
well-unital associative distributive commutative
almost_left_invertible domRing-like non trivial doubleLoopStr
for z be non zero rational_function of L
for z1 being rational_function of L,
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
ex x being Element of L st x is_a_common_root_of z`1,z`2 &
f.i = rpoly(1,x)
for g1 being rational_function of L,
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
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
let L be Field; let z be non zero rational_function of L;
let z1 be rational_function of L,
z2 be non zero Polynomial of L;
assume A1: 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
ex x being Element of L st x is_a_common_root_of z`1,z`2 &
f.i = rpoly(1,x);
let g1 be rational_function of L,
g2 be non zero Polynomial of L;
assume A2: 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
ex x being Element of L st x is_a_common_root_of z`1,z`2 &
g.i = rpoly(1,x);
defpred P[Nat] means
for z be non zero rational_function of L st max(deg(z`1),deg(z`2)) = $1
for z1 being rational_function of L,
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
ex x being Element of L st x is_a_common_root_of z`1,z`2 &
f.i = rpoly(1,x)
for g1 being rational_function of L,
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
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;
now let z be non zero rational_function of L;
assume max(deg(z`1),deg(z`2)) = 0;
then deg(z`2) <= 0 by XXREAL_0:25;
then A3: deg(z`2) = 0;
let z1 be rational_function of L,
z2 be non zero Polynomial of L;
assume A4: 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
ex x being Element of L st x is_a_common_root_of z`1,z`2 &
f.i = rpoly(1,x);
let g1 be rational_function of L,
g2 be non zero Polynomial of L;
assume A5: 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
ex x being Element of L st x is_a_common_root_of z`1,z`2 &
g.i = rpoly(1,x);
A6:now assume ex x be Element of L st x is_a_root_of z`2;
then consider y being Element of L such that
A7: y is_a_root_of z`2;
eval(z`2,y) = 0.L by A7,POLYNOM5:def 7;
hence contradiction by A3,Th8;
end;
A8:now assume z is reducible;
then z`1,z`2 have_common_roots;
then consider x being Element of L such that
A9: x is_a_common_root_of z`1,z`2;
x is_a_root_of z`2 by A9;
hence contradiction by A6;
end;
thus g1 = z1 by A8,A4,A5,Lm2;
end;
then A10: P[0];
A11: now let n be Nat;
assume A12: P[n];
for z be non zero rational_function of L st max(deg(z`1),deg(z`2)) = n+1
for z1 being rational_function of L,
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
ex x being Element of L st x is_a_common_root_of z`1,z`2 &
f.i = rpoly(1,x)
for g1 being rational_function of L,
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
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
let z be non zero rational_function of L;
assume A13: max(deg(z`1),deg(z`2)) = n+1;
let z1 be rational_function of L,
z2 be non zero Polynomial of L such that
A14: 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
ex x being Element of L st x is_a_common_root_of z`1,z`2 &
f.i = rpoly(1,x);
consider f being FinSequence of Polynom-Ring(L) such that
A15: z2 = Product f &
for i being Element of NAT st i in dom f
ex x being Element of L st x is_a_common_root_of z`1,z`2 &
f.i = rpoly(1,x) by A14;
let g1 be rational_function of L,
g2 be non zero Polynomial of L such that
A16: 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
ex x being Element of L st x is_a_common_root_of z`1,z`2 &
g.i = rpoly(1,x);
consider g being FinSequence of Polynom-Ring(L) such that
A17: g2 = Product g &
for i being Element of NAT st i in dom g
ex x being Element of L st x is_a_common_root_of z`1,z`2 &
g.i = rpoly(1,x) by A16;
per cases;
suppose A18: z is irreducible;
thus g1 = z1 by A18,A14,A16,Lm2;
end;
suppose z is reducible;
then z`1,z`2 have_common_roots;
then consider x being Element of L such that
A19: x is_a_common_root_of z`1,z`2;
A20: x is_a_root_of z`1 & x is_a_root_of z`2 by A19;
consider q2 being Polynomial of L such that
A21: z`2 = rpoly(1,x) *' q2 by A20,HURWITZ:33;
consider q1 being Polynomial of L such that
A22: z`1 = rpoly(1,x) *' q1 by A20,HURWITZ:33;
q2 <> 0_.(L) by A21,POLYNOM3:34;
then reconsider q2 as non zero Polynomial of L by UPROOTS:def 5;
set q = [q1,q2];
z`1 <> 0_.(L) by Def9; then
q1 <> 0_.(L) by A22,POLYNOM3:34; then
q`1 <> 0_.(L); then
reconsider q as non zero rational_function of L by Def9;
A23: max(deg(q`1),deg(q`2)) = n
proof
A24: deg(z`2) = deg(rpoly(1,x)) + deg(q2) by A21,HURWITZ:23
.= 1 + deg(q2) by HURWITZ:27;
per cases by XXREAL_0:16;
suppose A25: max(deg(z`1),deg(z`2)) = deg(z`1);
then z`1 <> 0_.(L) by A13,HURWITZ:20;
then q1 <> 0_.(L) by A22,POLYNOM3:34; then
A26: deg(z`1) = deg(rpoly(1,x)) + deg(q1) by A22,HURWITZ:23
.= 1 + deg(q1) by HURWITZ:27;
deg(z`2) <= n + 1 by A13,XXREAL_0:25;
then deg q2 + 1 - 1 <= n + 1 - 1 by A24,XREAL_1:9;
hence thesis by A26,A25,A13,XXREAL_0:def 10;
end;
suppose A27: max(deg(z`1),deg(z`2)) = deg(z`2);
A28: deg(z`1) <= n + 1 by A13,XXREAL_0:25;
now per cases;
suppose q1 = 0_.(L);
hence deg q1 <= deg q2 by HURWITZ:20;
end;
suppose q1 <> 0_.(L); then
deg(z`1) = deg(rpoly(1,x)) + deg(q1) by A22,HURWITZ:23
.= 1 + deg(q1) by HURWITZ:27;
hence deg q1 <= deg q2 by A28,A27,A24,A13,XREAL_1:9;
end;
end;
hence thesis by A24,A27,A13,XXREAL_0:def 10;
end;
end;
A29: now let i be Nat;
assume i in dom f;
then ex x being Element of L st
x is_a_common_root_of z`1,z`2 & f.i = rpoly(1,x) by A15;
hence ex z being Element of L st f.i = rpoly(1,z);
end;
ex i being Nat st i in dom f & f.i = rpoly(1,x)
proof
z2*'z1`1 = rpoly(1,x)*'q1 by A22,A14;
then A30: rpoly(1,x) divides (z2 *' z1`1) by HURWITZ:34;
z2*'z1`2 = rpoly(1,x)*'q2 by A21,A14;
then A31: rpoly(1,x) divides (z2 *' z1`2) by HURWITZ:34;
now per cases by A30,A31,Th10;
case rpoly(1,x) divides z2;
then eval(z2,x) = 0.L by Th9;
then consider i being Nat such that
A32: i in dom f & f.i = rpoly(1,x) by Th12,A15,A29;
take i;
thus thesis by A32;
end;
case rpoly(1,x) divides z1`1 & rpoly(1,x) divides z1`2;
then eval(z1`1,x) = 0.L & eval(z1`2,x) = 0.L by Th9;
then x is_a_root_of z1`1 & x is_a_root_of z1`2 by POLYNOM5:def 7;
then A33: x is_a_common_root_of z1`1,z1`2;
z1`1,z1`2 have_no_common_roots by A14;
hence thesis by A33;
end;
end;
hence thesis;
end;
then consider i being Nat such that A34: i in dom f & f.i = rpoly(1,x);
A35: now let j be Nat;
assume j in dom g;
then consider x being Element of L such that
A36: x is_a_common_root_of z`1,z`2 & g.j = rpoly(1,x) by A17;
thus ex z being Element of L st g.j = rpoly(1,z) by A36;
end;
ex j being Nat st j in dom g & g.j = rpoly(1,x)
proof
g2*'g1`1 = rpoly(1,x)*'q1 by A22,A16;
then A37: rpoly(1,x) divides (g2 *' g1`1) by HURWITZ:34;
g2*'g1`2 = rpoly(1,x)*'q2 by A21,A16;
then A38: rpoly(1,x) divides (g2 *' g1`2) by HURWITZ:34;
now per cases by A37,A38,Th10;
case rpoly(1,x) divides g2;
then eval(g2,x) = 0.L by Th9;
then consider i being Nat such that
A39: i in dom g & g.i = rpoly(1,x) by Th12,A17,A35;
take i;
thus thesis by A39;
end;
case rpoly(1,x) divides g1`1 & rpoly(1,x) divides g1`2;
then eval(g1`1,x) = 0.L & eval(g1`2,x) = 0.L by Th9;
then x is_a_root_of g1`1 & x is_a_root_of g1`2 by POLYNOM5:def 7;
then A40: x is_a_common_root_of g1`1,g1`2;
g1`1,g1`2 have_no_common_roots by A16;
hence thesis by A40;
end;
end;
hence thesis;
end;
then consider j being Nat such that A41: j in dom g & g.j = rpoly(1,x);
reconsider fq = Del(f,i) as FinSequence of Polynom-Ring(L) by FINSEQ_3:105;
reconsider gq = Del(g,j) as FinSequence of Polynom-Ring(L) by FINSEQ_3:105;
A42: now let k be Nat;
assume A43: k in dom fq;
consider m being Nat such that
A44: len f = m + 1 & len fq = m by A34,FINSEQ_3:104;
A45: k in Seg m by A43,A44,FINSEQ_1:def 3;
Seg m c= Seg(m+1) by FINSEQ_3:18;
then k in Seg(m+1) by A45;
then A46: k in dom f by A44,FINSEQ_1:def 3;
A47: k <= m by A45,FINSEQ_1:1;
then A48: k+1 <= m+1 by XREAL_1:6;
1 <= k+1 by NAT_1:11;
then k+1 in Seg(m+1) by A48;
then A49: k+1 in dom f by A44,FINSEQ_1:def 3;
now per cases;
suppose A50: k < i;
ex y being Element of L st
y is_a_common_root_of z`1,z`2 & f.k = rpoly(1,y) by A46,A15;
hence ex x being Element of L
st fq.k = rpoly(1,x) by A50,FINSEQ_3:110;
end;
suppose A51: i <= k;
ex y being Element of L st
y is_a_common_root_of z`1,z`2 & f.(k+1) = rpoly(1,y) by A15,A49;
hence ex x being Element of L
st fq.k = rpoly(1,x) by A51,A47,A34,A44,FINSEQ_3:111;
end;
end;
hence ex x being Element of L st fq.k = rpoly(1,x);
end;
A52: now let k be Nat;
assume A53: k in dom gq;
consider m being Nat such that
A54: len g = m + 1 & len gq = m by A41,FINSEQ_3:104;
A55: k in Seg m by A53,A54,FINSEQ_1:def 3;
Seg m c= Seg(m+1) by FINSEQ_3:18;
then k in Seg(m+1) by A55;
then A56: k in dom g by A54,FINSEQ_1:def 3;
A57: k <= m by A55,FINSEQ_1:1;
then A58: k+1 <= m+1 by XREAL_1:6;
1 <= k+1 by NAT_1:11;
then k+1 in Seg(m+1) by A58;
then A59: k+1 in dom g by A54,FINSEQ_1:def 3;
now per cases;
suppose A60: k < j;
ex y being Element of L st
y is_a_common_root_of z`1,z`2 & g.k = rpoly(1,y) by A56,A17;
hence ex x being Element of L
st gq.k = rpoly(1,x) by A60,FINSEQ_3:110;
end;
suppose A61: j <= k;
ex y being Element of L st
y is_a_common_root_of z`1,z`2 & g.(k+1) = rpoly(1,y) by A17,A59;
hence ex x being Element of L
st gq.k = rpoly(1,x) by A61,A57,A41,A54,FINSEQ_3:111;
end;
end;
hence ex x being Element of L st gq.k = rpoly(1,x);
end;
reconsider z2q = Product fq as Polynomial of L by POLYNOM3:def 10;
z2q <> 0_.(L) by A42,Th11; then
reconsider z2q as non zero Polynomial of L by UPROOTS:def 5;
reconsider g2q = Product gq as Polynomial of L by POLYNOM3:def 10;
g2q <> 0_.(L) by A52,Th11; then
reconsider g2q as non zero Polynomial of L by UPROOTS:def 5;
A62: Product f = f/.i * Product fq by A34,Th3;
A63: Product g = g/.j * Product gq by A41,Th3;
Seg(len f) = dom f by FINSEQ_1:def 3;
then 1 <= i & i <= len f by A34,FINSEQ_1:1;
then f/.i = rpoly(1,x) by A34,FINSEQ_4:15;
then A64: rpoly(1,x) *' z2q = Product f by A62,POLYNOM3:def 10;
then A65: rpoly(1,x) *' (z2q *' z1`1) = z2 *' z1`1 by A15,POLYNOM3:33
.= rpoly(1,x) *' q1 by A22,A14
.= rpoly(1,x) *' q`1;
then A66: z2q *' z1`1 = q`1 by Th7;
A67: rpoly(1,x) *' (z2q *' z1`2) = z2 *' z1`2 by A64,A15,POLYNOM3:33
.= rpoly(1,x) *' q2 by A21,A14
.= rpoly(1,x) *' q`2;
then z2q *' z1`2 = q`2 by Th7;
then A68: q = [z2q*'z1`1,z2q*'z1`2] by A66;
A69: now let k be Element of NAT;
assume A70: k in dom fq;
consider m being Nat such that
A71: len f = m + 1 & len fq = m by A34,FINSEQ_3:104;
A72: k in Seg m by A70,A71,FINSEQ_1:def 3;
Seg m c= Seg(m+1) by FINSEQ_3:18;
then k in Seg(m+1) by A72;
then A73: k in dom f by A71,FINSEQ_1:def 3;
A74: k <= m by A72,FINSEQ_1:1;
then A75: k+1 <= m+1 by XREAL_1:6;
1 <= k+1 by NAT_1:11;
then k+1 in Seg(m+1) by A75;
then A76: k+1 in dom f by A71,FINSEQ_1:def 3;
now per cases;
suppose A77: k < i;
then A78: f.k = fq.k by FINSEQ_3:110;
consider y being Element of L such that
A79: y is_a_common_root_of z`1,z`2 & f.k = rpoly(1,y)
by A73,A15;
A80: eval(z2q,y) = 0.L by A78,A79,A70,A42,Th12;
then 0.L = eval(z2q,y) * eval(z1`1,y)
.= eval(z2q*'z1`1,y) by POLYNOM4:24
.= eval(q`1,y) by A65,Th7;
then A81: y is_a_root_of q`1 by POLYNOM5:def 7;
0.L = eval(z2q,y) * eval(z1`2,y) by A80
.= eval(z2q*'z1`2,y) by POLYNOM4:24
.= eval(q`2,y) by A67,Th7;
then y is_a_root_of q`2 by POLYNOM5:def 7;
then y is_a_common_root_of q`1,q`2 by A81;
hence ex x being Element of L st x is_a_common_root_of q`1,q`2 &
fq.k = rpoly(1,x) by A79,A77,FINSEQ_3:110;
end;
suppose A82: i <= k;
then A83: f.(k+1) = fq.k by A74,A34,A71,FINSEQ_3:111;
consider y being Element of L such that
A84: y is_a_common_root_of z`1,z`2 & f.(k+1) = rpoly(1,y)
by A15,A76;
A85: eval(z2q,y) = 0.L by A83,A84,A70,A42,Th12;
then 0.L = eval(z2q,y) * eval(z1`1,y)
.= eval(z2q*'z1`1,y) by POLYNOM4:24
.= eval(q`1,y) by A65,Th7;
then A86: y is_a_root_of q`1 by POLYNOM5:def 7;
0.L = eval(z2q,y) * eval(z1`2,y) by A85
.= eval(z2q*'z1`2,y) by POLYNOM4:24
.= eval(q`2,y) by A67,Th7;
then y is_a_root_of q`2 by POLYNOM5:def 7;
then y is_a_common_root_of q`1,q`2 by A86;
hence ex x being Element of L st x is_a_common_root_of q`1,q`2 &
fq.k = rpoly(1,x) by A84,A82,A74,A34,A71,FINSEQ_3:111;
end;
end;
hence ex x being Element of L st x is_a_common_root_of q`1,q`2 &
fq.k = rpoly(1,x);
end;
Seg(len g) = dom g by FINSEQ_1:def 3;
then 1 <= j & j <= len g by A41,FINSEQ_1:1;
then g/.j = rpoly(1,x) by A41,FINSEQ_4:15;
then A87: rpoly(1,x) *' g2q = Product g by A63,POLYNOM3:def 10;
then A88: rpoly(1,x) *' (g2q *' g1`1) = g2 *' g1`1 by A17,POLYNOM3:33
.= z`1 by A16
.= rpoly(1,x) *' q`1 by A22;
then A89: g2q *' g1`1 = q`1 by Th7;
A90: rpoly(1,x) *' (g2q *' g1`2) = g2 *' g1`2 by A87,A17,POLYNOM3:33
.= z`2 by A16
.= rpoly(1,x) *' q`2 by A21;
then g2q *' g1`2 = q`2 by Th7;
then A91: q = [g2q*'g1`1,g2q*'g1`2] by A89;
A92: now let k be Element of NAT;
assume A93: k in dom gq;
consider m being Nat such that
A94: len g = m + 1 & len gq = m by A41,FINSEQ_3:104;
A95: k in Seg m by A93,A94,FINSEQ_1:def 3;
Seg m c= Seg(m+1) by FINSEQ_3:18;
then k in Seg(m+1) by A95;
then A96: k in dom g by A94,FINSEQ_1:def 3;
A97: k <= m by A95,FINSEQ_1:1;
then A98: k+1 <= m+1 by XREAL_1:6;
1 <= k+1 by NAT_1:11;
then k+1 in Seg(m+1) by A98;
then A99: k+1 in dom g by A94,FINSEQ_1:def 3;
now per cases;
suppose A100: k < j;
then A101: g.k = gq.k by FINSEQ_3:110;
consider y being Element of L such that
A102: y is_a_common_root_of z`1,z`2 & g.k = rpoly(1,y)
by A96,A17;
A103: eval(g2q,y) = 0.L by A101,A102,A93,A52,Th12;
then 0.L = eval(g2q,y) * eval(g1`1,y)
.= eval(g2q*'g1`1,y) by POLYNOM4:24
.= eval(q`1,y) by A88,Th7;
then A104: y is_a_root_of q`1 by POLYNOM5:def 7;
0.L = eval(g2q,y) * eval(g1`2,y) by A103
.= eval(g2q*'g1`2,y) by POLYNOM4:24
.= eval(q`2,y) by A90,Th7;
then y is_a_root_of q`2 by POLYNOM5:def 7;
then y is_a_common_root_of q`1,q`2 by A104;
hence ex x being Element of L st x is_a_common_root_of q`1,q`2 &
gq.k = rpoly(1,x) by A102,A100,FINSEQ_3:110;
end;
suppose A105: j <= k;
then A106: g.(k+1) = gq.k by A97,A41,A94,FINSEQ_3:111;
consider y being Element of L such that
A107: y is_a_common_root_of z`1,z`2 & g.(k+1) = rpoly(1,y)
by A17,A99;
A108: eval(g2q,y) = 0.L by A106,A107,A93,A52,Th12;
then 0.L = eval(g2q,y) * eval(g1`1,y)
.= eval(g2q*'g1`1,y) by POLYNOM4:24
.= eval(q`1,y) by A88,Th7;
then A109: y is_a_root_of q`1 by POLYNOM5:def 7;
0.L = eval(g2q,y) * eval(g1`2,y) by A108
.= eval(g2q*'g1`2,y) by POLYNOM4:24
.= eval(q`2,y) by A90,Th7;
then y is_a_root_of q`2 by POLYNOM5:def 7;
then y is_a_common_root_of q`1,q`2 by A109;
hence ex x being Element of L st x is_a_common_root_of q`1,q`2 &
gq.k = rpoly(1,x)
by A107,A105,A97,A41,A94,FINSEQ_3:111;
end;
end;
hence ex x being Element of L st x is_a_common_root_of q`1,q`2 &
gq.k = rpoly(1,x);
end;
thus z1 = g1 by A14,A16,A68,A91,A69,A92,A23,A12;
end;
end;
hence P[n+1];
end;
A110: for n being Nat holds P[n] from NAT_1:sch 2(A10,A11);
max(deg(z`1),deg(z`2)) >= deg(z`2) by XXREAL_0:25;
then max(deg(z`1),deg(z`2)) >= 0;
then max(deg(z`1),deg(z`2)) in NAT by INT_1:3;
hence z1 = g1 by A110,A1,A2;
end;
definition
let L be Abelian add-associative right_zeroed right_complementable
well-unital associative distributive commutative
almost_left_invertible domRing-like non trivial doubleLoopStr;
let z be rational_function of L;
func NF z -> rational_function of L means :Def17:
ex z1 being rational_function of L,
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
ex x being Element of L st x is_a_common_root_of z`1,z`2 &
f.i = rpoly(1,x)
if z is non zero otherwise it = 0._(L);
existence
proof
per cases;
suppose z is non zero;
consider z1 being rational_function of L,
z2 being non zero Polynomial of L such that
A1: 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
ex x being Element of L st x is_a_common_root_of z`1,z`2 &
f.i = rpoly(1,x) by Th21;
reconsider nfz = NormRatF z1 as rational_function of L;
ex zz1 being rational_function of L,
zz2 being non zero Polynomial of L
st nfz = NormRatF zz1 & zz1 is irreducible &
(ex f being FinSequence of Polynom-Ring(L)
st zz2 = Product f & z = [zz2*'zz1`1,zz2*'zz1`2] &
for i being Element of NAT st i in dom f
ex x being Element of L st x is_a_common_root_of z`1,z`2 &
f.i = rpoly(1,x)) by A1;
hence thesis;
end;
suppose z is zero;
hence thesis;
end;
end;
uniqueness by Lm3;
consistency;
end;
registration
let L be Abelian add-associative right_zeroed right_complementable
well-unital associative distributive commutative
almost_left_invertible domRing-like non trivial doubleLoopStr;
let z be rational_function of L;
cluster NF z -> normalized irreducible;
coherence
proof
per cases;
suppose z is non zero;
then consider z1 being rational_function of L,
z2 being non zero Polynomial of L such that
A1: z = [z2 *' z1`1, z2 *' z1`2] & z1 is irreducible &
NF z = NormRatF z1 &
ex f being FinSequence of Polynom-Ring(L)
st z2 = Product f &
for i being Element of NAT st i in dom f
ex x being Element of L st x is_a_common_root_of z`1,z`2 &
f.i = rpoly(1,x) by Def17;
A2: NF z is irreducible by A1,Th20;
(NF z)`2 = (1.L / LC(z1`2)) * z1`2 by A1;
hence thesis by A2;
end;
suppose z is zero;
then NF z = 0._(L) by Def17;
hence thesis;
end;
end;
end;
registration
let L be Abelian add-associative right_zeroed right_complementable
well-unital associative distributive commutative
almost_left_invertible domRing-like non trivial doubleLoopStr;
let z be non zero rational_function of L;
cluster NF z -> non zero;
coherence
proof
consider z1 being rational_function of L,
z2 being non zero Polynomial of L such that
A1: z = [z2 *' z1`1, z2 *' z1`2] & z1 is irreducible &
NF z = NormRatF z1 &
ex f being FinSequence of Polynom-Ring(L)
st z2 = Product f &
for i being Element of NAT st i in dom f
ex x being Element of L st x is_a_common_root_of z`1,z`2 &
f.i = rpoly(1,x) by Def17;
z1`1 <> 0_.(L) by A1,POLYNOM3:34,Def9;
then z1 is non zero;
hence thesis by A1;
end;
end;
Lm4:
for L being Abelian add-associative right_zeroed right_complementable
well-unital associative distributive commutative
almost_left_invertible domRing-like non trivial doubleLoopStr
for z being irreducible non zero rational_function of L
holds NF z = NormRationalFunction z
proof
let L be Abelian add-associative right_zeroed right_complementable
well-unital associative distributive commutative
almost_left_invertible domRing-like non trivial doubleLoopStr;
let z be irreducible non zero rational_function of L;
consider z1 being rational_function of L,
z2 being non zero Polynomial of L such that
A1: z = [z2 *' z1`1, z2 *' z1`2] & z1 is irreducible &
NF z = NormRatF z1 &
ex f being FinSequence of Polynom-Ring(L)
st z2 = Product f &
for i being Element of NAT st i in dom f
ex x being Element of L st x is_a_common_root_of z`1,z`2 &
f.i = rpoly(1,x) by Def17;
consider f being FinSequence of Polynom-Ring(L) such that
A2: z2 = Product f & z = [z2 *' z1`1, z2 *' z1`2] &
for i being Element of NAT st i in dom f
ex x being Element of L st x is_a_common_root_of z`1,z`2 &
f.i = rpoly(1,x) by A1;
now assume A3: f <> <*>(the carrier of Polynom-Ring(L));
let i be Element of dom f;
dom f <> {} by A3;
then i in dom f;
then reconsider i as Element of NAT;
consider x being Element of L such that
A4: x is_a_common_root_of z`1,z`2 & f.i = rpoly(1,x) by A2,A3;
z`1,z`2 have_common_roots by A4;
hence contradiction by Def10;
end;
then A5: Product f = 1_(Polynom-Ring(L)) by GROUP_4:8
.= 1_.(L) by POLYNOM3:def 10;
then z = [z1`1, z2 *' z1`2] by A2,POLYNOM3:35
.= [z1`1,z1`2] by A2,A5,POLYNOM3:35
.= z1 by Th19;
hence thesis by A1;
end;
theorem
for L be Abelian add-associative right_zeroed right_complementable
well-unital associative distributive commutative
almost_left_invertible domRing-like non trivial doubleLoopStr
for z be non zero rational_function of L
for z1 being rational_function of L,
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
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
for L be Abelian add-associative right_zeroed right_complementable
well-unital associative distributive commutative
almost_left_invertible domRing-like non trivial doubleLoopStr
holds NF 0._(L) = 0._(L) by Def17;
theorem
for L be Abelian add-associative right_zeroed right_complementable
well-unital associative distributive commutative
almost_left_invertible domRing-like non trivial doubleLoopStr
holds NF 1._(L) = 1._(L)
proof
let L be Abelian add-associative right_zeroed right_complementable
well-unital associative distributive commutative
almost_left_invertible domRing-like non trivial doubleLoopStr;
set z = 1._(L);
A1: NF z = NormRatF z by Lm4
.= [(1.L / LC(z`2)) * z`1, (1.L / LC(z`2)) * z`2];
z`2 is normalized by Def11;
then A2: LC(z`2) = 1.L;
A3: 1.L / LC(z`2) = (LC(z`2))"*LC(z`2) by A2
.= 1.L by VECTSP_1:def 10;
hence NF z = [z`1, (1.L / LC(z`2)) * z`2] by A1,POLYNOM5:27
.= [z`1, z`2] by A3,POLYNOM5:27
.= z;
end;
theorem
for L being Abelian add-associative right_zeroed right_complementable
well-unital associative distributive commutative
almost_left_invertible domRing-like non trivial doubleLoopStr
for z being irreducible non zero rational_function of L
holds NF z = NormRationalFunction z by Lm4;
Lm5:
for L being Abelian add-associative right_zeroed right_complementable unital
domRing-like left_zeroed distributive non trivial doubleLoopStr
for p1,p2 being Polynomial of L
holds p1 *' p2 = 0_.(L) implies p1 = 0_.(L) or p2 = 0_.(L)
proof
let L be Abelian add-associative right_zeroed right_complementable unital
domRing-like left_zeroed distributive non trivial doubleLoopStr;
let p1,p2 be Polynomial of L;
assume A1: p1 *' p2 = 0_.(L);
now assume p1 <> 0_.(L) & p2 <> 0_.(L);
then reconsider x1 = p1, x2 = p2 as non zero Polynomial of L
by UPROOTS:def 5;
x1 *' x2 is non zero;
hence contradiction by A1;
end;
hence thesis;
end;
theorem Th26:
for L be Abelian add-associative right_zeroed right_complementable
well-unital associative distributive commutative
almost_left_invertible domRing-like non trivial doubleLoopStr
for z be 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
let L be Abelian add-associative right_zeroed right_complementable
well-unital associative distributive commutative
almost_left_invertible domRing-like non trivial doubleLoopStr;
let z be rational_function of L;
let x be Element of L;
per cases;
suppose A1: z is non zero; then
consider z1 being rational_function of L,
z2 being non zero Polynomial of L such that
A2: z = [z2 *' z1`1, z2 *' z1`2] & z1 is irreducible &
NF z = NormRatF z1 &
ex f being FinSequence of Polynom-Ring(L)
st z2 = Product f &
for i being Element of NAT st i in dom f
ex x being Element of L st x is_a_common_root_of z`1,z`2 &
f.i = rpoly(1,x) by Def17;
consider f being FinSequence of Polynom-Ring(L) such that
A3: z2 = Product f &
for i being Element of NAT st i in dom f
ex x being Element of L st x is_a_common_root_of z`1,z`2 &
f.i = rpoly(1,x) by A2;
set q = [rpoly(1,x) *' z`1, rpoly(1,x) *' z`2];
q`1 <> 0_.(L) by A1,Lm5;
then reconsider q as non zero rational_function of L by Def9;
reconsider rp = rpoly(1,x) as Element of Polynom-Ring(L) by POLYNOM3:def 10;
set g = <*rp*> ^ f;
reconsider g as FinSequence of Polynom-Ring(L);
set g2 = Product g;
now let i be Nat;
assume A4: i in dom g;
now per cases by A4,FINSEQ_1:25;
suppose A5: i in dom <*rp*>;
then i in {1} by FINSEQ_1:2,38;
then i = 1 by TARSKI:def 1;
then g.i = <*rp*>.1 by A5,FINSEQ_1:def 7
.= rp by FINSEQ_1:40;
hence ex z being Element of L st g.i = rpoly(1,z);
end;
suppose ex n being Nat st n in dom f & i = len(<*rp*>) + n;
then consider n being Nat such that
A6: n in dom f & i = len(<*rp*>) + n;
A7: g.i = f.n by A6,FINSEQ_1:def 7;
ex x being Element of L st
x is_a_common_root_of z`1,z`2 & f.n = rpoly(1,x) by A6,A3;
hence ex z being Element of L st g.i = rpoly(1,z) by A7;
end;
end;
hence ex z being Element of L st g.i = rpoly(1,z);
end;
then g2 <> 0_.(L) by Th11;
then reconsider g2 as non zero Polynomial of L
by UPROOTS:def 5,POLYNOM3:def 10;
A8: now let i be Element of NAT;
assume A9: i in dom g;
now per cases by A9,FINSEQ_1:25;
suppose A10: i in dom <*rp*>;
then i in {1} by FINSEQ_1:2,38;
then i = 1 by TARSKI:def 1;
then A11: g.i = <*rp*>.1 by A10,FINSEQ_1:def 7
.= rp by FINSEQ_1:40;
A12: eval(rpoly(1,x),x) = x - x by HURWITZ:29 .= 0.L by RLVECT_1:15;
then 0.L = eval(rpoly(1,x),x) * eval(z`1,x)
.= eval(rpoly(1,x) *' z`1,x) by POLYNOM4:24;
then x is_a_root_of rpoly(1,x) *' z`1 by POLYNOM5:def 7;
then A13: x is_a_root_of q`1;
0.L = eval(rpoly(1,x),x) * eval(z`2,x) by A12
.= eval(rpoly(1,x) *' z`2,x) by POLYNOM4:24;
then x is_a_root_of rpoly(1,x) *' z`2 by POLYNOM5:def 7;
then x is_a_root_of q`2;
then x is_a_common_root_of q`1,q`2 by A13;
hence ex z being Element of L st z is_a_common_root_of q`1,q`2 &
g.i = rpoly(1,z) by A11;
end;
suppose ex n being Nat st n in dom f & i = len(<*rp*>) + n;
then consider n being Nat such that
A14: n in dom f & i = len(<*rp*>) + n;
A15: g.i = f.n by A14,FINSEQ_1:def 7;
consider y being Element of L such that
A16: y is_a_common_root_of z`1,z`2 & f.n = rpoly(1,y) by A14,A3;
y is_a_root_of z`1 by A16;
then eval(z`1,y) = 0.L by POLYNOM5:def 7;
then 0.L = eval(rpoly(1,x),y) * eval(z`1,y)
.= eval(rpoly(1,x) *' z`1,y) by POLYNOM4:24;
then y is_a_root_of rpoly(1,x) *' z`1 by POLYNOM5:def 7;
then A17: y is_a_root_of q`1;
y is_a_root_of z`2 by A16;
then eval(z`2,y) = 0.L by POLYNOM5:def 7;
then 0.L = eval(rpoly(1,x),y) * eval(z`2,y)
.= eval(rpoly(1,x) *' z`2,y) by POLYNOM4:24;
then y is_a_root_of rpoly(1,x) *' z`2 by POLYNOM5:def 7;
then y is_a_root_of q`2;
then y is_a_common_root_of q`1,q`2 by A17;
hence ex z being Element of L st z is_a_common_root_of q`1,q`2 &
g.i = rpoly(1,z) by A15,A16;
end;
end;
hence ex x being Element of L st x is_a_common_root_of q`1,q`2 &
g.i = rpoly(1,x);
end;
A18: Product g = rp * Product f by GROUP_4:7;
A19: q`1 = rpoly(1,x) *' z`1
.= rpoly(1,x) *' (z2 *' z1`1) by A2
.= (rpoly(1,x) *' z2) *' z1`1 by POLYNOM3:33
.= g2 *' z1`1 by A18,A3,POLYNOM3:def 10;
q`2 = rpoly(1,x) *' z`2
.= rpoly(1,x) *' (z2 *' z1`2) by A2
.= (rpoly(1,x) *' z2) *' z1`2 by POLYNOM3:33
.= g2 *' z1`2 by A18,A3,POLYNOM3:def 10;
then q = [g2 *' z1`1, g2 *' z1`2] by A19;
hence thesis by A2,A8,Def17;
end;
suppose A20: z is zero;
then z`1 = 0_.(L);
then rpoly(1,x) *' z`1 = 0_.(L) by POLYNOM3:34;
then [rpoly(1,x) *' z`1, rpoly(1,x) *' z`2]`1 = 0_.(L);
then [rpoly(1,x) *' z`1, rpoly(1,x) *' z`2] is zero;
then NF [rpoly(1,x) *' z`1, rpoly(1,x) *' z`2] = 0._(L) by Def17;
hence thesis by A20,Def17;
end;
end;
theorem
for L being Abelian add-associative right_zeroed right_complementable
well-unital associative distributive commutative
almost_left_invertible domRing-like non trivial doubleLoopStr
for z being rational_function of L
holds NF (NF z) = NF z
proof
let L be Abelian add-associative right_zeroed right_complementable
well-unital associative distributive commutative
almost_left_invertible domRing-like non trivial doubleLoopStr;
let z be rational_function of L;
set nfz = NF z;
per cases;
suppose z is zero;
then A1: NF z = 0._(L) by Def17;
thus thesis by A1,Def17;
end;
suppose A2: z is non zero;
A3: 1.L <> 0.L;
A4: NF nfz = NormRatF nfz by A2,Lm4
.= [(1.L/LC(nfz`2)) * nfz`1, (1.L/LC(nfz`2)) * nfz`2];
nfz`2 is normalized by Def11;
then A5: LC(nfz`2) = 1.L;
A6: 1.L / LC(nfz`2) = (LC(nfz`2))"*LC(nfz`2) by A5
.= 1.L by VECTSP_1:def 10,A3;
then NF nfz = [nfz`1, (1.L / LC(nfz`2)) * nfz`2] by A4,POLYNOM5:27
.= [nfz`1, nfz`2] by A6,POLYNOM5:27
.= nfz by Th19;
hence thesis;
end;
end;
theorem Th28:
for L being Abelian add-associative right_zeroed right_complementable
well-unital associative distributive commutative
almost_left_invertible domRing-like non degenerated 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
let L be Abelian add-associative right_zeroed right_complementable
well-unital associative distributive commutative
almost_left_invertible domRing-like non degenerated doubleLoopStr;
let z be non zero rational_function of L;
set q = z`2;
set a = (LC(z`2))";
now assume A1: a = 0.L;
then A2: a * (LC q) = 0.L;
a <> 1.L by A1;
hence contradiction by A2,VECTSP_1:def 10;
end;
then reconsider a as non zero Element of L by STRUCT_0:def 12;
reconsider x = [a * (z`1), a * (z`2)] as rational_function of L;
A3: now assume z is irreducible;
then NF z = NormRatF z by Lm4
.= [(1.L / LC(z`2)) * z`1, (1.L / LC(z`2)) * z`2];
hence ex a being Element of L st a <> 0.L &
[a * (z`1), a * (z`2)] = NF(z);
end;
now assume
ex a being Element of L st a <> 0.L & [a * (z`1), a * (z`2)] = NF(z);
then consider a being Element of L such that
A4: a <> 0.L & [a * (z`1), a * (z`2)] = NF(z);
reconsider x = [a * (z`1), a * (z`2)] as rational_function of L by A4;
now assume z`1, z`2 have_a_common_root;
then consider u being Element of L such that
A5: u is_a_common_root_of z`1, z`2;
u is_a_root_of z`1 & u is_a_root_of z`2 by A5;
then A6: eval(z`1,u) = 0.L & eval(z`2,u) = 0.L by POLYNOM5:def 7;
eval(x`1,u) = a * eval(z`1,u) by POLYNOM5:30;
then eval(x`1,u) = 0.L by A6;
then A7: u is_a_root_of x`1 by POLYNOM5:def 7;
eval(x`2,u) = a * eval(z`2,u) by POLYNOM5:30;
then eval(x`2,u) = 0.L by A6;
then u is_a_root_of x`2 by POLYNOM5:def 7;
then u is_a_common_root_of x`1, x`2 by A7;
then x`1,x`2 have_a_common_root;
hence contradiction by Def10,A4;
end;
hence z is irreducible;
end;
hence thesis by A3;
end;
begin :: Degree of Rational Functions
definition
let L be Abelian add-associative right_zeroed right_complementable
well-unital associative distributive commutative
almost_left_invertible domRing-like non trivial doubleLoopStr;
let z be rational_function of L;
func degree z -> Integer equals
max(degree((NF z)`1),degree((NF z)`2));
coherence;
end;
notation
let L be Abelian add-associative right_zeroed right_complementable
well-unital associative distributive commutative
almost_left_invertible domRing-like non trivial doubleLoopStr;
let z be rational_function of L;
synonym deg z for degree z;
end;
Lm6:
for L being Abelian add-associative right_zeroed right_complementable
well-unital associative distributive commutative
almost_left_invertible domRing-like non trivial 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
let L be Abelian add-associative right_zeroed right_complementable
well-unital associative distributive commutative
almost_left_invertible domRing-like non trivial doubleLoopStr;
let z be non zero rational_function of L;
assume z is irreducible;
then consider a being Element of L such that
A1: a <> 0.L & [a * (z`1), a * (z`2)] = NF(z) by Th28;
a is non zero by A1; then
reconsider az2 = a * (z`2) as non zero Polynomial of L;
thus degree z
= max(deg(a * (z`1)), deg(a * (z`2))) by A1
.= max(deg(z`1),deg(az2)) by A1,POLYNOM5:25
.= max(degree(z`1),degree(z`2)) by A1,POLYNOM5:25;
end;
theorem Th29:
for L being Abelian add-associative right_zeroed right_complementable
well-unital associative distributive commutative
almost_left_invertible domRing-like non trivial doubleLoopStr
for z being rational_function of L
holds degree(z) <= max(degree(z`1),degree(z`2))
proof
let L be Abelian add-associative right_zeroed right_complementable
well-unital associative distributive commutative
almost_left_invertible domRing-like non trivial doubleLoopStr;
let z be rational_function of L;
per cases;
suppose A1: z is zero;
then A2: NF z = 0._(L) by Def17 .= [0_.(L),1_.(L)];
z`1 = 0_.(L) by A1;
then A3: deg(z`1) = -1 by HURWITZ:20;
A4: deg 1_.(L) = 1 - 1 by POLYNOM4:4;
deg z = max(deg 0_.(L),degree((NF z)`2)) by A2
.= max(deg 0_.(L),deg 1_.(L)) by A2
.= max(-1,deg 1_.(L)) by HURWITZ:20
.= 0 by A4,XXREAL_0:def 10;
hence thesis by A3,XXREAL_0:def 10;
end;
suppose A5: z is non zero;
defpred P[Nat] means
for z be non zero rational_function of L
st max(degree(z`1),degree(z`2)) = $1
holds max(degree((NF z)`1),degree((NF z)`2))
<= max(degree(z`1),degree(z`2));
now let z be non zero rational_function of L,
z1 be rational_function of L,
z2 be non zero Polynomial of L;
let f be FinSequence of Polynom-Ring(L);
assume A6: max(degree(z`1),degree(z`2)) = 0;
now per cases by A6,XXREAL_0:16;
suppose A7: degree(z`1) = 0;
now assume z`1,z`2 have_common_roots;
then consider x being Element of L such that
A8: x is_a_common_root_of z`1,z`2;
x is_a_root_of z`1 by A8;
then z`1 is with_roots by POLYNOM5:def 8;
hence contradiction by A7,HURWITZ:24;
end;
hence z`1,z`2 have_no_common_roots;
end;
suppose A9: degree(z`2) = 0;
now assume z`1,z`2 have_common_roots;
then consider x being Element of L such that
A10: x is_a_common_root_of z`1,z`2;
x is_a_root_of z`2 by A10;
then z`2 is with_roots by POLYNOM5:def 8;
hence contradiction by A9,HURWITZ:24;
end;
hence z`1,z`2 have_no_common_roots;
end;
end;
then z is irreducible;
then degree z = max(degree(z`1),degree(z`2)) by Lm6;
hence max(degree((NF z)`1),degree((NF z)`2))
<= max(degree(z`1),degree(z`2));
end;
then A11: P[0];
A12: now let n be Nat;
assume A13: P[n];
now let z be non zero rational_function of L;
assume A14: max(degree(z`1),degree(z`2)) = n+1;
per cases;
suppose z is irreducible;
then degree z = max(degree(z`1),degree(z`2)) by Lm6;
hence max(degree((NF z)`1),degree((NF z)`2))
<= max(degree(z`1),degree(z`2));
end;
suppose z is reducible;
then z`1,z`2 have_common_roots;
then consider x being Element of L such that
A15: x is_a_common_root_of z`1,z`2;
A16: x is_a_root_of z`1 & x is_a_root_of z`2 by A15;
consider q2 being Polynomial of L such that
A17: z`2 = rpoly(1,x) *' q2 by A16,HURWITZ:33;
consider q1 being Polynomial of L such that
A18: z`1 = rpoly(1,x) *' q1 by A16,HURWITZ:33;
q1 <> 0_.(L) by Def9,A18,POLYNOM3:34;
then reconsider q1 as non zero Polynomial of L by UPROOTS:def 5;
q2 <> 0_.(L) by A17,POLYNOM3:34;
then reconsider q2 as non zero Polynomial of L by UPROOTS:def 5;
set q = [q1,q2];
q is non zero;
then reconsider q as non zero rational_function of L;
z = [rpoly(1,x) *' q1,rpoly(1,x) *' q2] by Th19,A18,A17
.= [rpoly(1,x) *' q`1,rpoly(1,x) *' q2]
.= [rpoly(1,x) *' q`1,rpoly(1,x) *' q`2];
then A19: NF z = NF q by Th26;
A20: n <= n+1 by NAT_1:11;
A21: deg z`1 = deg rpoly(1,x) + deg q1 by A18,HURWITZ:23
.= 1 + deg q1 by HURWITZ:27
.= 1 + deg q`1;
deg z`2 = deg rpoly(1,x) + deg q2 by A17,HURWITZ:23
.= 1 + deg q2 by HURWITZ:27
.= 1 + deg q`2;
then A22: max(degree(z`1),degree(z`2))
= 1 + max(degree(q`1), degree(q`2)) by A21,Th4;
then max(degree((NF z)`1),degree((NF z)`2))
<= max(degree(q`1),degree(q`2)) by A13,A19,A14;
hence max(degree((NF z)`1),degree((NF z)`2))
<= max(degree(z`1),degree(z`2)) by A20,A22,A14,XXREAL_0:2;
end;
end;
hence P[n+1];
end;
A23: for n being Nat holds P[n] from NAT_1:sch 2(A11,A12);
max(degree(z`1),degree(z`2)) >= 0 by XXREAL_0:25;
then max(degree(z`1),degree(z`2)) in NAT by INT_1:3;
hence thesis by A5,A23;
end;
end;
theorem
for L being Abelian add-associative right_zeroed right_complementable
well-unital associative distributive commutative
almost_left_invertible domRing-like non trivial 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
let L be Abelian add-associative right_zeroed right_complementable
well-unital associative distributive commutative
almost_left_invertible domRing-like non trivial doubleLoopStr;
let z be non zero rational_function of L;
set p1 = z`1, p2 = z`2;
A1: now assume z is irreducible;
then consider a being Element of L such that
A2: a <> 0.L & [a * (z`1), a * (z`2)] = NF(z) by Th28;
A3: degree(a * (z`1)) = degree(z`1) by A2,POLYNOM5:25;
A4: degree(a * (z`2)) = degree(z`2) by A2,POLYNOM5:25;
degree((NF(z))`1) = degree(z`1) by A3,A2;
hence degree z = max(degree(z`1),degree(z`2)) by A4,A2;
end;
now assume A5: degree z = max( degree(z`1), degree(z`2));
now assume not(z is irreducible);
then p1, p2 have_a_common_root;
then consider x being Element of L such that
A6: x is_a_common_root_of p1,p2;
A7: x is_a_root_of p1 & x is_a_root_of p2 by A6;
then consider q1 being Polynomial of L such that
A8: p1 = rpoly(1,x) *' q1 by HURWITZ:33;
consider q2 being Polynomial of L such that
A9: p2 = rpoly(1,x) *' q2 by A7,HURWITZ:33;
q2 <> 0_.(L) by A9,POLYNOM3:34;
then reconsider q2 as non zero Polynomial of L by UPROOTS:def 5;
set zz = [q1,q2];
A10: zz`1 = q1 & zz`2 = q2;
z = [rpoly(1,x) *' zz`1,rpoly(1,x) *' zz`2] by Th19,A8,A9;
then NF(z) = NF(zz) by Th26;
then degree z = degree zz;
then A11: degree(z) <= max(degree(q1),degree(q2)) by Th29,A10;
now per cases;
suppose A12: p1 = 0_.(L);
A13: q1 = 0_.(L) by A12,A8,Lm5;
deg(rpoly(1,x)*'q2) + 0
= deg(rpoly(1,x)) + deg(q2) by HURWITZ:23
.= 1 + deg(q2) by HURWITZ:27;
then A14: deg(q2) < deg(p2) by A9,XREAL_1:8;
deg(p1) <= deg(p2) by A12,HURWITZ:20;
then A15: max(deg(p1),deg(p2)) = deg(p2) by XXREAL_0:def 10;
deg(q1) <= deg(q2) by A13,HURWITZ:20;
hence contradiction by A15,A14,A5,A11,XXREAL_0:def 10;
end;
suppose p1 <> 0_.(L);
then reconsider p1 as non zero Polynomial of L by UPROOTS:def 5;
now assume q1 = 0_.(L);
then p1 = 0_.(L) by A8,POLYNOM3:34;
hence contradiction;
end;
then reconsider q1 as non zero Polynomial of L by UPROOTS:def 5;
deg(p1) + 0 = deg(rpoly(1,x)) + deg(q1) by A8,HURWITZ:23
.= 1 + deg(q1) by HURWITZ:27;
then A16: deg(q1) < deg(p1) by XREAL_1:8;
deg(p2) + 0 = deg(rpoly(1,x)) + deg(q2) by A9,HURWITZ:23
.= 1 + deg(q2) by HURWITZ:27;
then deg(q2) < deg(p2) by XREAL_1:8;
hence contradiction by A5,A11,A16,XXREAL_0:27;
end;
end;
hence contradiction;
end;
hence z is irreducible;
end;
hence thesis by A1;
end;
begin :: Evaluation of Rational Functions
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
eval(z`1,x) / eval(z`2,x);
coherence;
end;
theorem Th31:
for L being Field
for x being Element of L holds eval(0._(L),x) = 0.L
proof
let L be Field; let x be Element of L;
thus eval(0._(L),x) = eval(0_.(L),x) * eval((0._(L))`2,x)"
.= 0.L * eval((0._(L))`2,x)" by POLYNOM4:17
.= 0.L;
end;
theorem
for L being Field
for x being Element of L holds eval(1._(L),x) = 1.L
proof
let L be Field; let x be Element of L;
A1: 1.L <> 0.L;
thus eval(1._(L),x) = eval(1_.(L),x) * eval((1._(L))`2,x)"
.= 1.L * eval((1._(L))`2,x)" by POLYNOM4:18
.= 1.L * eval(1_.(L),x)"
.= 1.L * (1.L)" by POLYNOM4:18
.= 1.L by A1,VECTSP_1:def 10;
end;
theorem
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
let L be Field; let p,q be rational_function of L; let x be Element of L;
assume A1: eval(p`2,x) <> 0.L & eval(q`2,x) <> 0.L;
thus eval(p+q,x)
= eval(p`1 *' q`2 + p`2 *' q`1,x) * eval((p+q)`2,x)"
.= eval(p`1 *' q`2 + p`2 *' q`1,x) * eval(p`2 *' q`2,x)"
.= eval(p`1 *' q`2 + p`2 *' q`1,x) * (eval(p`2,x) * eval(q`2,x))"
by POLYNOM4:24
.= eval(p`1 *' q`2 + p`2 *' q`1,x) * (eval(q`2,x)" * eval(p`2,x)")
by A1,VECTSP_2:11
.= (eval(p`1 *' q`2,x) + eval(p`2 *' q`1,x)) * (eval(q`2,x)" * eval(p`2,x)")
by POLYNOM4:19
.= (eval(p`1 *' q`2,x) * (eval(q`2,x)" * eval(p`2,x)")) +
(eval(p`2 *' q`1,x) * (eval(q`2,x)" * eval(p`2,x)")) by VECTSP_1:def 3
.= ((eval(p`1,x) * eval(q`2,x)) * (eval(q`2,x)" * eval(p`2,x)")) +
(eval(p`2 *' q`1,x) * (eval(q`2,x)" * eval(p`2,x)")) by POLYNOM4:24
.= (eval(p`1,x) * (eval(q`2,x) * (eval(q`2,x)" * eval(p`2,x)"))) +
(eval(p`2 *' q`1,x) * (eval(q`2,x)" * eval(p`2,x)")) by GROUP_1:def 3
.= (eval(p`1,x) * ((eval(q`2,x) * eval(q`2,x)") * eval(p`2,x)")) +
(eval(p`2 *' q`1,x) * (eval(q`2,x)" * eval(p`2,x)")) by GROUP_1:def 3
.= (eval(p`1,x) * (1.L * eval(p`2,x)")) +
(eval(p`2 *' q`1,x) * (eval(q`2,x)" * eval(p`2,x)")) by A1,VECTSP_1:def 10
.= (eval(p`1,x) * eval(p`2,x)") +
(eval(p`2 *' q`1,x) * (eval(q`2,x)" * eval(p`2,x)"))
.= (eval(p`1,x) * eval(p`2,x)") +
((eval(p`2,x) * eval(q`1,x)) * (eval(q`2,x)" * eval(p`2,x)"))
by POLYNOM4:24
.= (eval(p`1,x) * eval(p`2,x)") +
(eval(q`1,x) * (eval(p`2,x) * (eval(p`2,x)" * eval(q`2,x)")))
by GROUP_1:def 3
.= (eval(p`1,x) * eval(p`2,x)") +
(eval(q`1,x) * ((eval(p`2,x) * eval(p`2,x)") * eval(q`2,x)"))
by GROUP_1:def 3
.= (eval(p`1,x) * eval(p`2,x)") +
(eval(q`1,x) * (1.L * eval(q`2,x)")) by A1,VECTSP_1:def 10
.= eval(p,x) + eval(q,x);
end;
theorem
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
let L be Field; let p,q be rational_function of L; let x be Element of L;
assume A1: eval(p`2,x) <> 0.L & eval(q`2,x) <> 0.L;
thus eval(p*'q,x)
= eval(p`1 *' q`1,x) * eval((p*'q)`2,x)"
.= eval(p`1 *' q`1,x) * eval(p`2 *' q`2,x)"
.= eval(p`1 *' q`1,x) * (eval(p`2,x) * eval(q`2,x))"
by POLYNOM4:24
.= eval(p`1 *' q`1,x) * (eval(q`2,x)" * eval(p`2,x)")
by A1,VECTSP_2:11
.= (eval(p`1,x) * eval(q`1,x)) * (eval(q`2,x)" * eval(p`2,x)")
by POLYNOM4:24
.= eval(p`1,x) * (eval(q`1,x) * (eval(q`2,x)" * eval(p`2,x)"))
by GROUP_1:def 3
.= eval(p`1,x) * (eval(p`2,x)" * (eval(q`2,x)" * eval(q`1,x)))
by GROUP_1:def 3
.= eval(p,x) * eval(q,x) by GROUP_1:def 3;
end;
theorem Th35:
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
let L be Field; let p be rational_function of L; let x be Element of L;
assume A1: eval(p`2,x) <> 0.L;
set np = NormRationalFunction p;
A2: 1.L / LC(p`2) <> 0.L;
thus eval(np,x)
= eval(1.L / LC(p`2) * p`1,x) * eval(np`2,x)"
.= eval(1.L / LC(p`2) * p`1,x) * eval(1.L / LC(p`2) * p`2,x)"
.= (1.L / LC(p`2) * eval(p`1,x)) * eval(1.L / LC(p`2) * p`2,x)"
by POLYNOM5:30
.= (1.L / LC(p`2) * eval(p`1,x)) * (1.L / LC(p`2) * eval(p`2,x))"
by POLYNOM5:30
.= (1.L / LC(p`2) * eval(p`1,x)) * ((1.L / LC(p`2))" * eval(p`2,x)")
by A1,VECTSP_2:11
.= eval(p`1,x) * (1.L / LC(p`2) * ((1.L / LC(p`2))" * eval(p`2,x)"))
by GROUP_1:def 3
.= eval(p`1,x) * ((1.L / LC(p`2) * (1.L / LC(p`2))") * eval(p`2,x)")
by GROUP_1:def 3
.= eval(p`1,x) * (1.L * eval(p`2,x)") by A2,VECTSP_1:def 10
.= eval(p,x);
end;
theorem
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 x is_a_common_root_of p`1,p`2 or eval(NF p,x) = eval(p,x)
proof
let L be Field;
let p be rational_function of L;
let x be Element of L;
assume A1: eval(p`2,x) <> 0.L;
assume A2: not(x is_a_common_root_of p`1,p`2);
per cases;
suppose A3: p is zero;
then A4: p`1 = 0_.(L);
A5: NF p = 0._(L) by A3,Def17;
thus eval(p,x)
= 0.L * (eval(p`2,x))" by A4,POLYNOM4:17
.= 0.L
.= eval(NF p,x) by A5,Th31;
end;
suppose p is non zero;
then consider z1 being rational_function of L,
z2 being non zero Polynomial of L such that
A6: p = [z2 *' z1`1, z2 *' z1`2] & z1 is irreducible &
NF p = NormRatF z1 &
ex f being FinSequence of Polynom-Ring(L)
st z2 = Product f &
for i being Element of NAT st i in dom f
ex x being Element of L st x is_a_common_root_of p`1,p`2 &
f.i = rpoly(1,x) by Def17;
A7: p`1 = z2 *' z1`1 by A6;
A8: p`2 = z2 *' z1`2 by A6;
A9: now assume A10: eval(z2,x) = 0.L;
eval(z2 *' z1`1,x) = eval(z2,x) * eval(z1`1,x) by POLYNOM4:24
.= 0.L by A10;
then A11: x is_a_root_of p`1 by A7,POLYNOM5:def 7;
eval(z2 *' z1`2,x) = eval(z2,x) * eval(z1`2,x) by POLYNOM4:24
.= 0.L by A10;
then x is_a_root_of p`2 by A8,POLYNOM5:def 7;
hence contradiction by A2,A11;
end;
A12: now assume eval(z1`2,x) = 0.L;
then 0.L = eval(z2,x) * eval(z1`2,x)
.= eval(z2 *' z1`2,x) by POLYNOM4:24;
hence contradiction by A6,A1;
end;
eval(p,x) = eval(z2 *' z1`1,x) * (eval(z2 *' z1`2,x))"
by A6
.= (eval(z2,x) * eval(z1`1,x)) * (eval(z2 *' z1`2,x))"
by POLYNOM4:24
.= (eval(z2,x) * eval(z1`1,x)) *
((eval(z2,x) * eval(z1`2,x))" ) by POLYNOM4:24
.= (eval(z2,x) * eval(z1`1,x)) *
(eval(z1`2,x)" * eval(z2,x)") by A9,A12,VECTSP_2:11
.= eval(z2,x) * (eval(z1`1,x) *
(eval(z1`2,x)" * eval(z2,x)")) by GROUP_1:def 3
.= eval(z2,x) * (((eval(z1`1,x)) *
eval(z1`2,x)") * eval(z2,x)") by GROUP_1:def 3
.= (eval(z2,x) * eval(z2,x)") *
(eval(z1`1,x) * eval(z1`2,x)") by GROUP_1:def 3
.= 1.L * (eval(z1`1,x) * eval(z1`2,x)")
by A9,VECTSP_1:def 10
.= eval(z1,x);
hence eval(NF p,x) = eval(p,x) by A6,A12,Th35;
end;
end;