:: Introduction to Rational Functions :: by Christoph Schwarzweller :: :: Received February 8, 2012 :: Copyright (c) 2012 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; 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, NAT_1, GROUP_1, INT_1, FINSEQ_3, VFUNCT_1, RFINSEQ, NORMSP_1, POLYNOM3, POLYNOM4, FINSEQ_5, POLYNOM5, STRUCT_0, ALGSEQ_1, 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; 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; requirements NUMERALS, SUBSET, REAL, BOOLE, ARITHM; definitions FINSEQ_1, POLYNOM3, SQUARE_1, STRUCT_0, ALGSTR_0, VECTSP_1, RFINSEQ, FINSEQ_5, VECTSP_2, XREAL_0, XXREAL_0, ALGSTR_1, ARYTM_3, ALGSEQ_1, POLYNOM4, POLYNOM5, HURWITZ, FINSEQ_3, ALGSTR_2, GROUP_1; 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, MCART_1, STRUCT_0, XREAL_0, FINSEQ_4, GROUP_4, ALGSTR_0, FINSEQ_5, RFINSEQ, XTUPLE_0; schemes NAT_1, INT_1; begin :: Preliminaries theorem df: 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 AS: len p = len q & for i being Element of NAT st i in dom p holds q/.i = a * (p/.i); consider fq being Function of NAT,the carrier of L such that A6: Sum q = fq.(len q) and A7: fq.0 = 0.L and A8: for j being Element of 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 Function of NAT,the carrier of L such that A12: Sum p = fp.(len p) and A13: fp.0 = 0.L and A14: for j being Element of 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); B1: P[0] by A13,A7,VECTSP_1:6; B2: 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 A18: 0 <= j & j < len p; assume A19: P[j]; B3: 1 <= j + 1 by NAT_1:11; B4: j + 1 <= len p by A18,NAT_1:13; then j+1 in Seg(len q) by B3,AS; then A20: j+1 in dom q by FINSEQ_1:def 3; j+1 in Seg(len p) by B3,B4; then A20a: j+1 in dom p by FINSEQ_1:def 3; set vq = q/.(j+1), vp = p/.(j+1); A21: vq = q.(j+1) by A20,PARTFUN1:def 6; A21a: vp = p.(j+1) by A20a,PARTFUN1:def 6; fq.(j+1) = (a * fp.j) + vq by A19,AS,A21,A18,A8 .= (a * fp.j) + (a * vp) by AS,A20a .= a * (fp.j + vp) by VECTSP_1:def 2 .= a * fp.(j+1) by A21a,A18,A14; 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(B1,B2); hence thesis by AS,A12,A6; end; theorem del1a: 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 AS: i in dom f & j = i-1; then consider n being Nat such that H0: len f = n+1 & len Del(f,i) = n by FINSEQ_3:104; dom f = Seg(n+1) by H0,FINSEQ_1:def 3; then consider ii being Element of NAT such that H1: i = ii & 1 <= ii & ii <= n + 1 by AS; i-1 < i-0 by XREAL_1:15; then j < n+1 by AS,H1,XXREAL_0:2; then H2: j <= n by NAT_1:13; H3: len g = (len Del(f,i) + 1) by FINSEQ_5:69; now let k be Nat; assume B: 1 <= k & k <= len g; then k in Seg(len g) by FINSEQ_1:1; then D: k in dom g by FINSEQ_1:def 3; now per cases by XXREAL_0:1; suppose C: 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 B,AS,H2,H0,FINSEQ_1:59; then k in Seg(len(Del(f,i)|j)) by FINSEQ_1:1; then D1: k in dom(Del(f,i)|j) by FINSEQ_1:def 3; k < n+1 by H1,C,XXREAL_0:2; then k <= n by NAT_1:13; then k in Seg(len(Del(f,i))) by H0,B,FINSEQ_1:1; then D2: k in dom(Del(f,i)) by FINSEQ_1:def 3; g/.k = Del(f,i)/.k by D1,FINSEQ_5:72 .= Del(f,i).k by D2,PARTFUN1:def 6 .= f.k by C,FINSEQ_3:110; hence g.k = f.k by D,PARTFUN1:def 6; end; suppose C: k = i; then k = j + 1 by AS; then E: g/.k = f/.i by H0,H2,FINSEQ_5:73; thus g.k = g/.k by D,PARTFUN1:def 6 .= f.k by AS,C,E,PARTFUN1:def 6; end; suppose C: k > i; then reconsider k1 = k-1 as Element of NAT by H1,XXREAL_0:2,INT_1:5; C2: k-1 <= n+1-1 by B,H0,H3,XREAL_1:9; 1 < k1+1 by C,H1,XXREAL_0:2; then 1 <= k1 by NAT_1:13; then k1 in Seg(n) by C2; then D1: k1 in dom(Del(f,i)) by H0,FINSEQ_1:def 3; i < k1 + 1 by C; then C1: j+1 <= k-1 by AS,NAT_1:13; then g/.(k1+1) = Del(f,i)/.k1 by C2,H0,FINSEQ_5:74 .= Del(f,i).k1 by D1,PARTFUN1:def 6 .= f.(k1+1) by C1,C2,H0,AS,FINSEQ_3:111; hence f.k = g.k by D,PARTFUN1:def 6; end; end; hence g.k = f.k; end; hence thesis by H0,FINSEQ_5:69,FINSEQ_1:14; end; theorem del1: 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 AS: i in dom f; then i in Seg(len f) by FINSEQ_1:def 3; then consider ii being Element of NAT such that H: ii = i & 1 <= ii & ii <= len f; reconsider j = i-1 as Element of NAT by H,INT_1:5; set g = Del(f,i); thus Product f = Product( Ins(g,j,f/.i) ) by AS,del1a .= 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 by VECTSP_1:7; 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 B: L is domRing-like; let x be Element of L; assume A: 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 A,B,VECTSP_2:def 1; 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 B: L is domRing-like; let x be Element of L; assume A: 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 A,B,VECTSP_2:def 1; 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 maxx: 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 A: 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 A,XXREAL_0:def 10; end; suppose A: 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 A,XXREAL_0:def 10; end; end; begin :: More on Polynomials definition let L be non empty ZeroStr; let p be Polynomial of L; attr p is zero means :defzer: p = 0_.(L); attr p is constant means :defconst: deg p <= 0; end; registration let L be non trivial ZeroStr; cluster non zero for Polynomial of L; existence proof now assume AS: 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 AS .= x by AS; end; hence contradiction by STRUCT_0:def 10; end; then consider x being Element of the carrier of L such that C: 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 AS: i >= 1; B: i in NAT by ORDINAL1:def 12; thus p.i = (0_.(L)).i by AS,FUNCT_7:32 .= 0.L by B,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 A: i = 0 by NAT_1:14; i in NAT by ORDINAL1:def 12; then 0 in dom(0_.L) by A,FUNCT_2:def 1; hence p.i <> 0.L by C,A,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 proof deg 0_.(L) = -1 by HURWITZ:20; hence thesis by defconst,defzer; end; end; registration let L be non degenerated multLoopStr_0; cluster 1_.(L) -> non zero; coherence proof A: (1_.(L)).0 = 1.L by POLYNOM3:30; (0_.(L)).0 = 0.L by FUNCOP_1:7; hence thesis by defzer,A; end; end; registration let L be non empty multLoopStr_0; cluster 1_.(L) -> constant; coherence proof set p = 1_.(L); now per cases; suppose I: 0.L = 1.L; A: dom p = NAT by FUNCT_2:def 1 .= dom(0_.(L)) by FUNCT_2:def 1; now let x be set; assume x in dom p; then reconsider xx = x as Element of NAT; B: (0_.(L)).xx = 0.L by FUNCOP_1:7; xx = 0 or xx <> 0; hence p.x = (0_.(L)).x by I,B,POLYNOM3:30; end; hence thesis by A,FUNCT_1:2; end; suppose I: 0.L <> 1.L; now let i be Nat; assume AS: i >= 1; B: i in NAT by ORDINAL1:def 12; thus p.i = (0_.(L)).i by AS,FUNCT_7:32 .= 0.L by B,FUNCOP_1:7; end; then D: 1 is_at_least_length_of p by ALGSEQ_1:def 2; now let m be Nat; assume AS: m is_at_least_length_of p; now assume m < 1; then m < 1 + 0; then m <= 0 by NAT_1:13; then E: p.0 = 0.L by AS,ALGSEQ_1:def 2; dom(0_.(L)) = NAT by FUNCOP_1:13; hence contradiction by I,E,FUNCT_7:31; end; hence 1 <= m; end; then len p = 1 by D,ALGSEQ_1:def 3; then deg p = 0; hence thesis by defconst; end; end; hence thesis; end; end; registration let L be non empty ZeroStr; cluster zero -> constant for Polynomial of L; coherence proof let p be Polynomial of L; assume p is zero; then p = 0_.(L) by defzer; hence thesis; end; 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 AS: 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 AS .= x by AS; end; hence contradiction by STRUCT_0:def 10; end; then consider x being Element of the carrier of L such that C: 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 AS: i >= 2; then C: 1 <> i; B: i in NAT by ORDINAL1:def 12; thus p.i = (0_.(L)+*(0,x)).i by C,FUNCT_7:32 .= (0_.(L)).i by AS,FUNCT_7:32 .= 0.L by B,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 AS: i >= 2; then C: 1 <> i; B: i in NAT by ORDINAL1:def 12; thus p.i = (0_.(L)+*(0,x)).i by C,FUNCT_7:32 .= (0_.(L)).i by AS,FUNCT_7:32 .= 0.L by B,FUNCOP_1:7; end; then D: 2 is_at_least_length_of p by ALGSEQ_1:def 2; now let m be Nat; assume AS: m is_at_least_length_of p; now assume m < 2; then m < 1 + 1; then m <= 1 by NAT_1:13; then E: p.1 = 0.L by AS,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 C,E,FUNCT_7:31; end; hence 2 <= m; end; then len p = 2 by D,ALGSEQ_1:def 3; then deg p = 1; hence thesis by defconst; 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 by defzer; 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 by STRUCT_0:def 8; 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 aa: x*y = 0.Q; assume AS: 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 AS,POLYNOM3:def 10; then reconsider p as non zero Polynomial of L by defzer; q <> 0_.(L) by AS,POLYNOM3:def 10; then reconsider q as non zero Polynomial of L by defzer; p <> 0_.(L); then deg p <> -1 by HURWITZ:20; then Ap: len p <> 0; len p + 1 > 0 + 1 by Ap,XREAL_1:8; then Dp: len p >= 1 by NAT_1:13; then len p - 1 >= 1 - 1 by XREAL_1:9; then Cp: 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 Aq: len q <> 0; len q + 1 > 0 + 1 by Aq,XREAL_1:8; then Dq: len q >= 1 by NAT_1:13; then Eq: 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 Dp,Dq,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 X: 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 X1a: (m+1)-' len p = lq by XREAL_0:def 2; X6: len p + 0 <= len p + (len q - 1) by Eq,XREAL_1:6; then len p in Seg(len r) by Dp,X; then X1: len p in dom r by FINSEQ_1:def 3; then X2: r.(len p) = p.lp * q.lq by X1a,Cp,X; X4: now let k be Element of NAT; assume Y: k in dom r & k <> len p; now per cases; suppose k > len p; then k >= len p + 1 by NAT_1:13; then H: k-1 >= (len p + 1) - 1 by XREAL_1:9; k-'1 >= len p by H,XREAL_0:def 2; then p.(k-'1)= 0.L by ALGSEQ_1:8; then p.(k-'1) * q.(m+1-'k) = 0.L by VECTSP_1:7; hence r.k = 0.L by Y,X; end; suppose U: k <= len p; k < len p by Y,U,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 by VECTSP_1:6; hence r.k = 0.L by Y,X; end; end; hence r.k = 0.L; end; X3: now let i be Element of NAT; assume Y: 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 Y,X4; end; X5: (p*'q).m = r/.(len p) by X,X1,X3,POLYNOM2:3 .= p.lp * q.lq by X2,X6,Dp,X,FINSEQ_4:15; len p = lp + 1; then XX: p.lp <> 0.L by ALGSEQ_1:10; len q = lq + 1; then q.lq <> 0.L by ALGSEQ_1:10; then X6: (p*'q).m <> 0.L by XX,X5,VECTSP_2:def 1; (0_.(L)).m = 0.L by FUNCOP_1:7; then p*'q <> 0.Q by X6,POLYNOM3:def 10; hence thesis by aa,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); A: dom f = NAT by FUNCT_2:def 1 .= dom g by FUNCT_2:def 1; now let i be set; assume i in dom f; then reconsider n = i as Element of NAT; consider fr being FinSequence of the carrier of L such that A1: 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 A2: 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 A1,A2,FINSEQ_1:def 3; then A4: dom fa = dom fr by FINSEQ_1:def 3; A3: now let k be Element of NAT; assume A3a: 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 A3a,A4,PARTFUN1:def 6 .= (a*p).(k-'1) * q.(n+1-'k) by A4,A3a,A1 .= (a * p.(k-'1)) * q.(n+1-'k) by POLYNOM5:def 3 .= a* (p.(k-'1) * q.(n+1-'k)) by GROUP_1:def 3 .= a * x by A3a,A2 .= a * (fa/.k) by A3a,PARTFUN1:def 6; end; g.n = a * (Sum fa) by A2,POLYNOM5:def 3 .= f.n by A3,A2,A1,df; hence f.i = g.i; end; hence thesis by A,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); A: dom f = NAT by FUNCT_2:def 1 .= dom g by FUNCT_2:def 1; now let i be set; assume i in dom f; then reconsider n = i as Element of NAT; consider fr being FinSequence of the carrier of L such that A1: 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 A2: 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 A1,A2,FINSEQ_1:def 3; then A4: dom fa = dom fr by FINSEQ_1:def 3; A3: now let k be Element of NAT; assume A3a: 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 A3a,A4,PARTFUN1:def 6 .= p.(k-'1) * (a*q).(n+1-'k) by A4,A3a,A1 .= p.(k-'1) * (a * q.(n+1-'k)) by POLYNOM5:def 3 .= a* (p.(k-'1) * q.(n+1-'k)) by GROUP_1:def 3 .= a * x by A3a,A2 .= a * (fa/.k) by A3a,PARTFUN1:def 6; end; g.n = a * (Sum fa) by A2,POLYNOM5:def 3 .= f.n by A3,df,A2,A1; hence f.i = g.i; end; hence thesis by A,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,POLYNOM4:5; hence thesis by defzer; 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 A: 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 A,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 by defzer; end; end; theorem thequiv1: 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 AS: 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 A: x3 <> 0.Polynom-Ring(L) by POLYNOM3:def 10; B: x1 * x3 = p2 *' p3 by AS,POLYNOM3:def 10 .= x2 * x3 by POLYNOM3:def 10; x3 is right_mult-cancelable by A,ALGSTR_0:def 37; hence thesis by B,ALGSTR_0:def 21; 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:7,INT_1:3; hence thesis; end; end; theorem degrat2: 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 AS: 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 6; then p is with_roots by POLYNOM5:def 7; hence contradiction by AS,HURWITZ:24; end; theorem div1: 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; A: now assume rpoly(1,x) divides p; then p mod rpoly(1,x) = 0_.(L) by HURWITZ:def 7; 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 B: (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; C: 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 C,B,POLYNOM4:24 .= 0.L by VECTSP_1:6; end; eval(p,x) = 0.L implies rpoly(1,x) divides p by HURWITZ:35,POLYNOM5:def 6; hence thesis by A; end; theorem div3: 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 div1; then A: eval(p,x) * eval(q,x) = 0.L by POLYNOM4:24; per cases by A,VECTSP_2:def 1; suppose eval(p,x) = 0.L; hence thesis by div1; end; suppose eval(q,x) = 0.L; hence thesis by div1; end; end; theorem div4: 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 AS1: 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 AS2: 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 A1: 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 A2: p = Product f; f = <*>(the carrier of Polynom-Ring(L)) by A1; then p = 1_(Polynom-Ring(L)) by A2,GROUP_4:8 .= 1.(Polynom-Ring(L)); then p <> 0.(Polynom-Ring(L)); hence p <> 0_.(L) by POLYNOM3:def 10; end; then IA: P[0]; IS:now let n be Nat; assume IV: P[n]; now let f be FinSequence of Polynom-Ring(L); assume A1: 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 A2: p = Product f; f <> {} by A1; then consider g being FinSequence, u being set such that A6: f = g ^ <*u*> by FINSEQ_1:46; reconsider g as FinSequence of Polynom-Ring(L) by A6,FINSEQ_1:36; A2c: dom f = Seg(n+1) by A1,FINSEQ_1:def 3; 1 <= n+1 by NAT_1:11; then A2a: n+1 in dom f by A2c; A2c: n+1 = len g + len <*u*> by A1,A6,FINSEQ_1:22 .= len g + 1 by FINSEQ_1:40; then f.(n+1) = u by A6,FINSEQ_1:42; then consider z being Element of L such that U: u = rpoly(1,z) by A1,A2a; reconsider u as Element of Polynom-Ring(L) by U,POLYNOM3:def 10; reconsider q = Product g as Polynomial of L by POLYNOM3:def 10; A4: Product f = (Product g) * u by A6,GROUP_4:6; A3: u <> 0.(Polynom-Ring(L)) by U,POLYNOM3:def 10; now let i be Nat; assume G: i in dom g; then H: g.i = f.i by A6,FINSEQ_1:def 7; dom g c= dom f by A6,FINSEQ_1:26; hence ex z being Element of L st g.i = rpoly(1,z) by G,H,A1; end; then q <> 0_.(L) by IV,A2c; then q <> 0.(Polynom-Ring(L)) by POLYNOM3:def 10; then p <> 0.(Polynom-Ring(L)) by A2,A3,A4,VECTSP_2:def 1; hence p <> 0_.(L) by POLYNOM3:def 10; end; hence P[n+1]; end; I: for n being Nat holds P[n] from NAT_1:sch 2(IA,IS); len f is Nat; hence thesis by AS1,AS2,I; end; theorem div2: 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 AS1: 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 AS2: p = Product f; let x be Element of L; A: now assume ex i being Nat st i in dom f & f.i = rpoly(1,x); then consider i being Nat such that A1: 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; A2: f/.i = rpoly(1,x) by A1,PARTFUN1:def 6; Product f = (f/.i) * Product g by A1,del1; then p = rpoly(1,x) *' q by AS2,A2,POLYNOM3:def 10; then A3: 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 A3,VECTSP_1:7; end; now assume A0: 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 A1: 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 A2: p = Product f; let x be Element of L; assume A3: eval(p,x) = 0.L; f = <*>(the carrier of Polynom-Ring(L)) by A1; then p = 1_(Polynom-Ring(L)) by A2,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 A3,POLYNOM4:18; end; then IA: P[0]; IS:now let n be Nat; assume IV: P[n]; now let f be FinSequence of Polynom-Ring(L); assume A1: 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 A2: p = Product f; let x be Element of L; assume A3: eval(p,x) = 0.L; f <> {} by A1; then consider g being FinSequence, u being set such that A6: f = g ^ <*u*> by FINSEQ_1:46; reconsider g as FinSequence of Polynom-Ring(L) by A6,FINSEQ_1:36; A2c: dom f = Seg(n+1) by A1,FINSEQ_1:def 3; 1 <= n+1 by NAT_1:11; then A2a: n+1 in dom f by A2c; A2c: n+1 = len g + len <*u*> by A1,A6,FINSEQ_1:22 .= len g + 1 by FINSEQ_1:40; A2b: f.(n+1) = u by A2c,A6,FINSEQ_1:42; then consider z being Element of L such that U: u = rpoly(1,z) by A1,A2a; reconsider u as Element of Polynom-Ring(L) by U,POLYNOM3:def 10; reconsider q = Product g as Polynomial of L by POLYNOM3:def 10; Product f = (Product g) * u by A6,GROUP_4:6 .= q *' rpoly(1,z) by U,POLYNOM3:def 10; then A4: eval(p,x) = eval(q,x) * eval(rpoly(1,z),x) by A2,POLYNOM4:24; A10: now let i be Nat; assume C1: i in dom g; C2: dom g c= dom f by A6,FINSEQ_1:26; g.i = f.i by C1,A6,FINSEQ_1:def 7; hence ex z being Element of L st g.i = rpoly(1,z) by C1,C2,A1; end; now per cases by A4,A3,VECTSP_2:def 1; suppose eval(q,x) = 0.L; then consider i being Nat such that B1: i in dom g & g.i = rpoly(1,x) by A2c,A10,IV; B2: dom g c= dom f by A6,FINSEQ_1:26; f.i = rpoly(1,x) by B1,A6,FINSEQ_1:def 7; hence ex i being Nat st i in dom f & f.i = rpoly(1,x) by B2,B1; 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 A2a,A2b,U; end; end; hence ex i being Nat st i in dom f & f.i = rpoly(1,x); end; hence P[n+1]; end; I: for n being Nat holds P[n] from NAT_1:sch 2(IA,IS); len f is Nat; hence ex i being Nat st i in dom f & f.i = rpoly(1,x) by A0,AS1,AS2,I; end; hence thesis by A; 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 :root1: 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 :root2: 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 root3: 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 AS: x is_a_root_of p; eval(-p,x) = - eval(p,x) by POLYNOM4:20 .= - 0.L by AS,POLYNOM5:def 6 .= 0.L by RLVECT_1:12; hence x is_a_root_of -p by POLYNOM5:def 6; end; theorem root4: 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 by root1; then AS: eval(p1,x) = 0.L & eval(p2,x) = 0.L by POLYNOM5:def 6; eval(p1+p2,x) = 0.L + 0.L by AS,POLYNOM4:19 .= 0.L by RLVECT_1:def 4; hence x is_a_root_of p1+p2 by POLYNOM5:def 6; 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 root3,root4; 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 H: x is_a_root_of p & x is_a_root_of q by root1; then H1: eval(p,x) = 0.L by POLYNOM5:def 6; H2: eval(q,x) = 0.L by H,POLYNOM5:def 6; eval(p+q,x) = 0.L + 0.L by H1,H2,POLYNOM4:19 .= 0.L by RLVECT_1:def 4; hence thesis by POLYNOM5:def 6; 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 AS: p1 divides p2 & p1 is with_roots; per cases; suppose A: p1 = 0_.(L); p2 mod p1 = 0_.(L) by AS,HURWITZ:def 7; then 0_.(L) = p2 - 0_.(L)by A,POLYNOM3:34 .= p2 + 0_.(L) by HURWITZ:9; then B: 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 6; then 0.L is_a_common_root_of p1,p2 by A,B,root1; hence thesis by root2; end; suppose p1 <> 0_.(L); then consider s being Polynomial of L such that A: s *' p1 = p2 by AS,HURWITZ:34; consider x being Element of L such that B: x is_a_root_of p1 by AS,POLYNOM5:def 7; C: eval(p1,x) = 0.L by B,POLYNOM5:def 6; eval(p2,x) = eval(s,x) * eval(p1,x) by A,POLYNOM4:24 .= 0.L by C,VECTSP_1:6; then x is_a_root_of p2 by POLYNOM5:def 6; then x is_a_common_root_of p1,p2 by B,root1; hence thesis by root2; 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 set; 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 by STRUCT_0:def 12; end; end; theorem lcp1: 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 A: a = 0.L; then B: a * LC(p) = 0.L by VECTSP_1:6; a * p = 0_.(L) by A,POLYNOM5:26; hence thesis by B,FUNCOP_1:7; end; suppose A: a <> 0.L; thus LC(a * p) = a * (p.(len(a*p)-'1)) by POLYNOM5:def 3 .= a * LC(p) by A,POLYNOM5:25; end; end; definition let L be non empty doubleLoopStr; let p be Polynomial of L; attr p is normalized means :defnormp: 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 A: LC p <> 0.L; LC((1.L / LC p) * p) = (1.L / LC p) * LC(p) by lcp1 .= 1.L * ((LC p)" * LC(p)) by GROUP_1:def 3 .= 1.L * 1.L by A,VECTSP_1:def 10 .= 1.L by VECTSP_1:def 4; hence thesis by defnormp; 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; A: p <> 0_.L; then q.(len p-'1) = 1.L by POLYNOM5:56,POLYNOM4:5; then LC q = 1.L by A,POLYNOM5:57,POLYNOM4:5; hence thesis by defnormp; end; end; begin :: Rational Functions definition let L be non trivial multLoopStr_0; mode rational_function of L means :defratf: ex p1 being Polynomial of L st ex p2 being non zero Polynomial of L st it = [p1,p2]; existence proof take [the Polynomial of L,the non zero Polynomial of L]; 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 by defratf; 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 H: ex p2 being non zero Polynomial of L st z = [p1,p2] by defratf; consider p2 being non zero Polynomial of L such that H1: z = [p1,p2] by H; thus thesis by H1,XTUPLE_0:def 2; end; redefine func z`2 -> non zero Polynomial of L; coherence proof consider p1 being Polynomial of L such that H: ex p2 being non zero Polynomial of L st z = [p1,p2] by defratf; consider p2 being non zero Polynomial of L such that H1: z = [p1,p2] by H; thus thesis by H1,XTUPLE_0:def 3; end; end; definition let L be non trivial multLoopStr_0; let z be rational_function of L; attr z is zero means :defzerrat: 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]; H: p1 = [p1,p2]`1; p1 <> 0_.(L); hence thesis by H,defzerrat; end; end; theorem ttt: 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 H1: ex p2 being non zero Polynomial of L st z = [p1,p2] by defratf; consider p2 being non zero Polynomial of L such that H2: z = [p1,p2] by H1; z`1 = p1 & z`2 = p2 by H2,XTUPLE_0:def 2,XTUPLE_0:def 3; hence thesis by H2; 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 :defirred: 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 :defnorm: 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 by defnorm; 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 defzerrat; then reconsider z1 = z`1 as non zero Polynomial of L by defzer; (1.L / LC(z`2)) * z1 is non zero; then (NormRatF z)`1 <> 0_.(L) by XTUPLE_0:def 2; hence thesis by defzerrat; 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 B: x is_a_common_root_of p1,p2 by root2; x is_a_root_of p2 by B,root1; then eval(p2,x) = 0.L by POLYNOM5:def 6; hence contradiction by POLYNOM4:18; end; then B: z is irreducible by defirred; C: len(1_.(L)) = 1 by POLYNOM4:4; len(1_.(L))-'1 = 1 - 1 by C,XREAL_0:def 2; then LC(1_.(L)) = 1.L by POLYNOM3:30; then p2 is normalized by defnormp; hence thesis by B,defnorm; end; end; registration let L be non degenerated multLoopStr_0; cluster 1._(L) -> non zero; coherence proof (1._(L))`1 <> 0_.(L) by XTUPLE_0:def 2; hence thesis by defzerrat; end; 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 B: x is_a_common_root_of p1,p2 by root2; x is_a_root_of p2 by B,root1; then eval(p2,x) = 0.L by POLYNOM5:def 6; hence contradiction by POLYNOM4:18; end; hence thesis by defirred; 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) ]; C: [ rpoly(1,x), rpoly(1,x) ]`1 = 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 by root1; then z`1, z`2 have_common_roots by root2; then z is reducible by defirred; hence thesis by C,defzerrat; 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 proof (0._(L))`1 = 0_.(L) by XTUPLE_0:def 2; hence thesis by defzerrat; end; 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 by defnormp; hence 1._(L) is normalized by defnorm; 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 tw2: 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]; A: now assume A0: p is irreducible; assume ap is reducible; then ap`1, ap`2 have_common_roots by defirred; then consider x being Element of L such that A1: x is_a_common_root_of ap`1, ap`2 by root2; x is_a_root_of ap`1 & x is_a_root_of ap`2 by A1,root1; then A2: eval(ap`1,x) = 0.L & eval(ap`2,x) = 0.L by POLYNOM5:def 6; 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 A3: x is_a_root_of p`1 by POLYNOM5:def 6; eval(a * p`2,x) = 0.L by A2; 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 6; then x is_a_common_root_of p`1,p`2 by A3,root1; then p`1,p`2 have_common_roots by root2; hence [a * p`1, a * p`2] is irreducible by A0,defirred; end; now assume A0: ap is irreducible; assume p is reducible; then p`1, p`2 have_common_roots by defirred; then consider x being Element of L such that A1: x is_a_common_root_of p`1, p`2 by root2; x is_a_root_of p`1 & x is_a_root_of p`2 by A1,root1; then A2: eval(p`1,x) = 0.L & eval(p`2,x) = 0.L by POLYNOM5:def 6; then a * eval(p`1,x) = 0.L by VECTSP_1:6; then eval(a * p`1,x) = 0.L by POLYNOM5:30; then eval(ap`1,x) = 0.L; then A3: x is_a_root_of ap`1 by POLYNOM5:def 6; a * eval(p`2,x) = 0.L by A2,VECTSP_1:6; 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 6; then x is_a_common_root_of ap`1,ap`2 by A3,root1; then ap`1,ap`2 have_common_roots by root2; hence p is irreducible by A0,defirred; end; hence thesis by A; end; begin :: Normalized Rational Functions polynormirred: 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 AS: 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 ttt .= [e*'z`1,z`2] by POLYNOM3:35 .= [e*'z`1,e*'z`2] by POLYNOM3:35; thus z is irreducible by AS; take f; Product f = 1_(Polynom-Ring(L)) by GROUP_4:8; hence thesis by POLYNOM3:def 10; end; theorem ratfuncNF: 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 B: deg(z`2) = 0; A: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 H: y is_a_root_of z`2; eval(z`2,y) = 0.L by H,POLYNOM5:def 6; hence contradiction by B,degrat2; end; now assume z is reducible; then z`1,z`2 have_common_roots by defirred; then consider x being Element of L such that H: x is_a_common_root_of z`1,z`2 by root2; x is_a_root_of z`2 by H,root1; hence contradiction by A; 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 polynormirred; end; then IA: P[0]; IS: now let n be Nat; assume AS: 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 AS1: max(deg(z`1),deg(z`2)) = n+1; per cases; suppose z is irreducible; hence thesis by polynormirred; end; suppose z is reducible; then z`1,z`2 have_common_roots by defirred; then consider x being Element of L such that H: x is_a_common_root_of z`1,z`2 by root2; H3: x is_a_root_of z`1 & x is_a_root_of z`2 by H,root1; consider q2 being Polynomial of L such that H2: z`2 = rpoly(1,x) *' q2 by H3,HURWITZ:33; consider q1 being Polynomial of L such that H1: z`1 = rpoly(1,x) *' q1 by H3,HURWITZ:33; q2 <> 0_.(L) by H2,POLYNOM3:34; then reconsider q2 as non zero Polynomial of L by defzer; set q = [q1,q2]; max(deg(q`1),deg(q`2)) = n proof A2: deg(z`2) = deg(rpoly(1,x)) + deg(q2) by H2,HURWITZ:23 .= 1 + deg(q2) by HURWITZ:27; per cases by XXREAL_0:16; suppose A5: max(deg(z`1),deg(z`2)) = deg(z`1); then z`1 <> 0_.(L) by AS1,HURWITZ:20; then q1 <> 0_.(L) by H1,POLYNOM3:34; then A3: deg(z`1) = deg(rpoly(1,x)) + deg(q1) by H1,HURWITZ:23 .= 1 + deg(q1) by HURWITZ:27; A6: deg(z`2) <= n + 1 by AS1,XXREAL_0:25; deg q2 + 1 - 1 <= n + 1 - 1 by A2,A6,XREAL_1:9; hence thesis by A3,A5,AS1,XXREAL_0:def 10; end; suppose A3: max(deg(z`1),deg(z`2)) = deg(z`2); A6: deg(z`1) <= n + 1 by AS1,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 H1,HURWITZ:23 .= 1 + deg(q1) by HURWITZ:27; hence deg q1 <= deg q2 by A6,A2,A3,AS1,XREAL_1:9; end; end; hence thesis by A3,A2,AS1,XXREAL_0:def 10; end; end; then consider z1q being rational_function of L, z2q being non zero Polynomial of L such that IQ: 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 AS; 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 IQ2: 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 IQ; reconsider rp = rpoly(1,x) as Element of Polynom-Ring(L) by POLYNOM3:def 10; set f = <*rp*> ^ fq; IQ3: Product f = rp * Product(fq) by GROUP_4:7 .= z2 by IQ2,POLYNOM3:def 10; IQ4: z = [z2*'z1`1,z2*'z1`2] proof X: q1 = z2q*' z1q`1 by IQ,XTUPLE_0:def 2; Z: q2 = z2q*' z1q`2 by IQ,XTUPLE_0:def 3; Y: (z2 *' z1`1) = z`1 by X,H1,POLYNOM3:33; A: (z2 *' z1`2) = z`2 by Z,H2,POLYNOM3:33; thus z = [z2*'z1`1,z2*'z1`2] by Y,A,ttt; end; IQ5: now let i be Element of NAT; assume C1: i in dom f; now per cases by C1,FINSEQ_1:25; suppose C2: i in dom<*rp*>; then C3: i in {1} by FINSEQ_1:2,FINSEQ_1:38; f.i = <*rp*>.i by C2,FINSEQ_1:def 7 .= <*rp*>.1 by C3,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 H; end; suppose ex n being Nat st n in dom fq & i = len<*rp*> + n; then consider n being Nat such that C2: n in dom fq & i = len<*rp*> + n; f.i = fq.n by C2,FINSEQ_1:def 7; then consider y being Element of L such that C3: y is_a_common_root_of q`1,q`2 & f.i = rpoly(1,y) by C2,IQ2; C4: y is_a_root_of q`1 & y is_a_root_of q`2 by C3,root1; then C5: 0.L = eval(q1,y) by POLYNOM5:def 6; C8: eval(z`1,y) = eval(rpoly(1,x),y) * eval(q1,y) by H1,POLYNOM4:24 .= 0.L by C5,VECTSP_1:7; C6: 0.L = eval(q2,y) by C4,POLYNOM5:def 6; eval(z`2,y) = eval(rpoly(1,x),y) * eval(q2,y) by H2,POLYNOM4:24 .= 0.L by C6,VECTSP_1:7; then y is_a_root_of z`1 & y is_a_root_of z`2 by C8,POLYNOM5:def 6; then y is_a_common_root_of z`1,z`2 by root1; hence ex x being Element of L st x is_a_common_root_of z`1,z`2 & f.i = rpoly(1,x) by C3; 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 IQ,IQ3,IQ4,IQ5; end; end; hence P[n+1]; end; I: for n being Nat holds P[n] from NAT_1:sch 2(IA,IS); 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 I; end; ratfuncNFunique1: 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 AS: z is irreducible; let z1 be rational_function of L, z2 be non zero Polynomial of L; assume A: 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 B: 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 C: 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 A; now assume f <> <*>(the carrier of Polynom-Ring(L)); then G: dom f <> {}; let i be Element of dom f; reconsider i as Nat; D1: i in dom f by G; consider x being Element of L such that D2: x is_a_common_root_of z`1,z`2 & f.i = rpoly(1,x) by D1,C; z`1,z`2 have_common_roots by D2,root2; hence contradiction by AS,defirred; end; hence D2: z2 = 1_(Polynom-Ring(L)) by C,GROUP_4:8 .= 1_.(L) by POLYNOM3:def 10; then D1: z2 *' z1`1 = z1`1 by POLYNOM3:35; z2 *' z1`2 = z1`2 by D2,POLYNOM3:35; then D: z = z1 by D1,A,ttt; consider h being FinSequence of Polynom-Ring(L) such that E: 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 B; now assume h <> <*>(the carrier of Polynom-Ring(L)); then G: dom h <> {}; let i be Element of dom h; reconsider i as Nat; D1: i in dom h by G; consider x being Element of L such that D2: x is_a_common_root_of z`1,z`2 & h.i = rpoly(1,x) by D1,E; z`1,z`2 have_common_roots by D2,root2; hence contradiction by AS,defirred; end; hence E2: g2 = 1_(Polynom-Ring(L)) by E,GROUP_4:8 .= 1_.(L) by POLYNOM3:def 10; then E1: g2 *' g1`1 = g1`1 by POLYNOM3:35; g2 *' g1`2 = g1`2 by E2,POLYNOM3:35; hence z1 = g1 by D,E1,B,ttt; end; ratfuncNFunique2: 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 H1: 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 H2: 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 B: deg(z`2) = 0; let z1 be rational_function of L, z2 be non zero Polynomial of L; assume H1: 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 H2: 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); A: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 H: y is_a_root_of z`2; eval(z`2,y) = 0.L by H,POLYNOM5:def 6; hence contradiction by B,degrat2; end; B:now assume z is reducible; then z`1,z`2 have_common_roots by defirred; then consider x being Element of L such that H: x is_a_common_root_of z`1,z`2 by root2; x is_a_root_of z`2 by H,root1; hence contradiction by A; end; thus g1 = z1 by B,H1,H2,ratfuncNFunique1; end; then IA: P[0]; IS: now let n be Nat; assume IV: 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 AS1: 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 H1: 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 H1a: 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 H1; let g1 be rational_function of L, g2 be non zero Polynomial of L such that H2: 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 H2a: 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 H2; per cases; suppose B: z is irreducible; thus g1 = z1 by B,H1,H2,ratfuncNFunique1; end; suppose z is reducible; then z`1,z`2 have_common_roots by defirred; then consider x being Element of L such that H: x is_a_common_root_of z`1,z`2 by root2; H3: x is_a_root_of z`1 & x is_a_root_of z`2 by H,root1; consider q2 being Polynomial of L such that HY: z`2 = rpoly(1,x) *' q2 by H3,HURWITZ:33; consider q1 being Polynomial of L such that HX: z`1 = rpoly(1,x) *' q1 by H3,HURWITZ:33; q2 <> 0_.(L) by HY,POLYNOM3:34; then reconsider q2 as non zero Polynomial of L by defzer; set q = [q1,q2]; z`1 <> 0_.(L) by defzerrat; then q1 <> 0_.(L) by HX,POLYNOM3:34; then q`1 <> 0_.(L); then reconsider q as non zero rational_function of L by defzerrat; AS2: max(deg(q`1),deg(q`2)) = n proof A2: deg(z`2) = deg(rpoly(1,x)) + deg(q2) by HY,HURWITZ:23 .= 1 + deg(q2) by HURWITZ:27; A7: max(deg(q`1),deg(q`2)) = max(deg(q1),deg(q`2)) by XTUPLE_0:def 2 .= max(deg(q1),deg(q2)) by XTUPLE_0:def 3; per cases by XXREAL_0:16; suppose A5: max(deg(z`1),deg(z`2)) = deg(z`1); then z`1 <> 0_.(L) by AS1,HURWITZ:20; then q1 <> 0_.(L) by HX,POLYNOM3:34; then A3: deg(z`1) = deg(rpoly(1,x)) + deg(q1) by HX,HURWITZ:23 .= 1 + deg(q1) by HURWITZ:27; deg(z`2) <= n + 1 by AS1,XXREAL_0:25; then deg q2 + 1 - 1 <= n + 1 - 1 by A2,XREAL_1:9; hence thesis by A7,A3,A5,AS1,XXREAL_0:def 10; end; suppose A3: max(deg(z`1),deg(z`2)) = deg(z`2); A6: deg(z`1) <= n + 1 by AS1,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 HX,HURWITZ:23 .= 1 + deg(q1) by HURWITZ:27; hence deg q1 <= deg q2 by A6,A3,A2,AS1,XREAL_1:9; end; end; hence thesis by A7,A2,A3,AS1,XXREAL_0:def 10; end; end; ZZ1: 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 H1a; 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 HX,H1,XTUPLE_0:def 2; then Z11: rpoly(1,x) divides (z2 *' z1`1) by HURWITZ:34; z2*'z1`2 = rpoly(1,x)*'q2 by HY,H1,XTUPLE_0:def 3; then Z11a: rpoly(1,x) divides (z2 *' z1`2) by HURWITZ:34; now per cases by Z11,Z11a,div3; case rpoly(1,x) divides z2; then eval(z2,x) = 0.L by div1; then consider i being Nat such that Z3: i in dom f & f.i = rpoly(1,x) by div2,H1a,ZZ1; take i; thus thesis by Z3; 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 div1; then x is_a_root_of z1`1 & x is_a_root_of z1`2 by POLYNOM5:def 6; then Z3: x is_a_common_root_of z1`1,z1`2 by root1; z1`1,z1`2 have_no_common_roots by H1,defirred; hence thesis by Z3,root2; end; end; hence thesis; end; then consider i being Nat such that H5: i in dom f & f.i = rpoly(1,x); ZZ1a: now let j be Nat; assume j in dom g; then consider x being Element of L such that A: x is_a_common_root_of z`1,z`2 & g.j = rpoly(1,x) by H2a; thus ex z being Element of L st g.j = rpoly(1,z) by A; end; ex j being Nat st j in dom g & g.j = rpoly(1,x) proof g2*'g1`1 = rpoly(1,x)*'q1 by HX,H2,XTUPLE_0:def 2; then Z11: rpoly(1,x) divides (g2 *' g1`1) by HURWITZ:34; g2*'g1`2 = rpoly(1,x)*'q2 by HY,H2,XTUPLE_0:def 3; then Z11a: rpoly(1,x) divides (g2 *' g1`2) by HURWITZ:34; now per cases by Z11,Z11a,div3; case rpoly(1,x) divides g2; then eval(g2,x) = 0.L by div1; then consider i being Nat such that Z3: i in dom g & g.i = rpoly(1,x) by div2,H2a,ZZ1a; take i; thus thesis by Z3; 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 div1; then x is_a_root_of g1`1 & x is_a_root_of g1`2 by POLYNOM5:def 6; then Z3: x is_a_common_root_of g1`1,g1`2 by root1; g1`1,g1`2 have_no_common_roots by H2,defirred; hence thesis by Z3,root2; end; end; hence thesis; end; then consider j being Nat such that H6: 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; X100: now let k be Nat; assume H11: k in dom fq; consider m being Nat such that H14: len f = m + 1 & len fq = m by H5,FINSEQ_3:104; H14a: k in Seg m by H11,H14,FINSEQ_1:def 3; Seg m c= Seg(m+1) by FINSEQ_3:18; then k in Seg(m+1) by H14a; then H13: k in dom f by H14,FINSEQ_1:def 3; H14b: k <= m by H14a,FINSEQ_1:1; then H14d: k+1 <= m+1 by XREAL_1:6; 1 <= k+1 by NAT_1:11; then k+1 in Seg(m+1) by H14d; then H14c: k+1 in dom f by H14,FINSEQ_1:def 3; now per cases; suppose H12: 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 H13,H1a; hence ex x being Element of L st fq.k = rpoly(1,x) by H12,FINSEQ_3:110; end; suppose H12: 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 H1a,H14c; hence ex x being Element of L st fq.k = rpoly(1,x) by H12,H14b,H5,H14,FINSEQ_3:111; end; end; hence ex x being Element of L st fq.k = rpoly(1,x); end; X101: now let k be Nat; assume H11: k in dom gq; consider m being Nat such that H14: len g = m + 1 & len gq = m by H6,FINSEQ_3:104; H14a: k in Seg m by H11,H14,FINSEQ_1:def 3; Seg m c= Seg(m+1) by FINSEQ_3:18; then k in Seg(m+1) by H14a; then H13: k in dom g by H14,FINSEQ_1:def 3; H14b: k <= m by H14a,FINSEQ_1:1; then H14d: k+1 <= m+1 by XREAL_1:6; 1 <= k+1 by NAT_1:11; then k+1 in Seg(m+1) by H14d; then H14c: k+1 in dom g by H14,FINSEQ_1:def 3; now per cases; suppose H12: 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 H13,H2a; hence ex x being Element of L st gq.k = rpoly(1,x) by H12,FINSEQ_3:110; end; suppose H12: 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 H2a,H14c; hence ex x being Element of L st gq.k = rpoly(1,x) by H12,H14b,H6,H14,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 X100,div4; then reconsider z2q as non zero Polynomial of L by defzer; reconsider g2q = Product gq as Polynomial of L by POLYNOM3:def 10; g2q <> 0_.(L) by X101,div4; then reconsider g2q as non zero Polynomial of L by defzer; H7: Product f = f/.i * Product fq by H5,del1; H7a: Product g = g/.j * Product gq by H6,del1; Seg(len f) = dom f by FINSEQ_1:def 3; then 1 <= i & i <= len f by H5,FINSEQ_1:1; then f/.i = rpoly(1,x) by H5,FINSEQ_4:15; then H9: rpoly(1,x) *' z2q = Product f by H7,POLYNOM3:def 10; then H8: rpoly(1,x) *' (z2q *' z1`1) = z2 *' z1`1 by H1a,POLYNOM3:33 .= rpoly(1,x) *' q1 by HX,H1,XTUPLE_0:def 2 .= rpoly(1,x) *' q`1 by XTUPLE_0:def 2; then H8b: z2q *' z1`1 = q`1 by thequiv1; H8a: rpoly(1,x) *' (z2q *' z1`2) = z2 *' z1`2 by H9,H1a,POLYNOM3:33 .= rpoly(1,x) *' q2 by HY,H1,XTUPLE_0:def 3 .= rpoly(1,x) *' q`2 by XTUPLE_0:def 3; then z2q *' z1`2 = q`2 by thequiv1; then I1: q = [z2q*'z1`1,z2q*'z1`2] by H8b,MCART_1:8; I3: now let k be Element of NAT; assume H11: k in dom fq; consider m being Nat such that H14: len f = m + 1 & len fq = m by H5,FINSEQ_3:104; H14a: k in Seg m by H11,H14,FINSEQ_1:def 3; Seg m c= Seg(m+1) by FINSEQ_3:18; then k in Seg(m+1) by H14a; then H13: k in dom f by H14,FINSEQ_1:def 3; H14b: k <= m by H14a,FINSEQ_1:1; then H14d: k+1 <= m+1 by XREAL_1:6; 1 <= k+1 by NAT_1:11; then k+1 in Seg(m+1) by H14d; then H14c: k+1 in dom f by H14,FINSEQ_1:def 3; now per cases; suppose H12: k < i; then H12a: f.k = fq.k by FINSEQ_3:110; consider y being Element of L such that H10: y is_a_common_root_of z`1,z`2 & f.k = rpoly(1,y) by H13,H1a; H25: eval(z2q,y) = 0.L by H12a,H10,H11,X100,div2; then 0.L = eval(z2q,y) * eval(z1`1,y) by VECTSP_1:7 .= eval(z2q*'z1`1,y) by POLYNOM4:24 .= eval(q`1,y) by H8,thequiv1; then A1: y is_a_root_of q`1 by POLYNOM5:def 6; 0.L = eval(z2q,y) * eval(z1`2,y) by VECTSP_1:7,H25 .= eval(z2q*'z1`2,y) by POLYNOM4:24 .= eval(q`2,y) by H8a,thequiv1; then y is_a_root_of q`2 by POLYNOM5:def 6; then y is_a_common_root_of q`1,q`2 by A1,root1; hence ex x being Element of L st x is_a_common_root_of q`1,q`2 & fq.k = rpoly(1,x) by H10,H12,FINSEQ_3:110; end; suppose H12: i <= k; then H12a: f.(k+1) = fq.k by H14b,H5,H14,FINSEQ_3:111; consider y being Element of L such that H10: y is_a_common_root_of z`1,z`2 & f.(k+1) = rpoly(1,y) by H1a,H14c; H25: eval(z2q,y) = 0.L by H12a,H10,H11,X100,div2; then 0.L = eval(z2q,y) * eval(z1`1,y) by VECTSP_1:7 .= eval(z2q*'z1`1,y) by POLYNOM4:24 .= eval(q`1,y) by H8,thequiv1; then A1: y is_a_root_of q`1 by POLYNOM5:def 6; 0.L = eval(z2q,y) * eval(z1`2,y) by VECTSP_1:7,H25 .= eval(z2q*'z1`2,y) by POLYNOM4:24 .= eval(q`2,y) by H8a,thequiv1; then y is_a_root_of q`2 by POLYNOM5:def 6; then y is_a_common_root_of q`1,q`2 by A1,root1; hence ex x being Element of L st x is_a_common_root_of q`1,q`2 & fq.k = rpoly(1,x) by H10,H12,H14b,H5,H14,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 H6,FINSEQ_1:1; then g/.j = rpoly(1,x) by H6,FINSEQ_4:15; then H9: rpoly(1,x) *' g2q = Product g by H7a,POLYNOM3:def 10; then H8: rpoly(1,x) *' (g2q *' g1`1) = g2 *' g1`1 by H2a,POLYNOM3:33 .= z`1 by H2,XTUPLE_0:def 2 .= rpoly(1,x) *' q`1 by HX,XTUPLE_0:def 2; then H8b: g2q *' g1`1 = q`1 by thequiv1; H8a: rpoly(1,x) *' (g2q *' g1`2) = g2 *' g1`2 by H9,H2a,POLYNOM3:33 .= z`2 by H2,XTUPLE_0:def 3 .= rpoly(1,x) *' q`2 by HY,XTUPLE_0:def 3; then g2q *' g1`2 = q`2 by thequiv1; then I2: q = [g2q*'g1`1,g2q*'g1`2] by H8b,MCART_1:8; I4: now let k be Element of NAT; assume H11: k in dom gq; consider m being Nat such that H14: len g = m + 1 & len gq = m by H6,FINSEQ_3:104; H14a: k in Seg m by H11,H14,FINSEQ_1:def 3; Seg m c= Seg(m+1) by FINSEQ_3:18; then k in Seg(m+1) by H14a; then H13: k in dom g by H14,FINSEQ_1:def 3; H14b: k <= m by H14a,FINSEQ_1:1; then H14d: k+1 <= m+1 by XREAL_1:6; 1 <= k+1 by NAT_1:11; then k+1 in Seg(m+1) by H14d; then H14c: k+1 in dom g by H14,FINSEQ_1:def 3; now per cases; suppose H12: k < j; then H12a: g.k = gq.k by FINSEQ_3:110; consider y being Element of L such that H10: y is_a_common_root_of z`1,z`2 & g.k = rpoly(1,y) by H13,H2a; H25: eval(g2q,y) = 0.L by H12a,H10,H11,X101,div2; then 0.L = eval(g2q,y) * eval(g1`1,y) by VECTSP_1:7 .= eval(g2q*'g1`1,y) by POLYNOM4:24 .= eval(q`1,y) by H8,thequiv1; then A1: y is_a_root_of q`1 by POLYNOM5:def 6; 0.L = eval(g2q,y) * eval(g1`2,y) by VECTSP_1:7,H25 .= eval(g2q*'g1`2,y) by POLYNOM4:24 .= eval(q`2,y) by H8a,thequiv1; then y is_a_root_of q`2 by POLYNOM5:def 6; then y is_a_common_root_of q`1,q`2 by A1,root1; hence ex x being Element of L st x is_a_common_root_of q`1,q`2 & gq.k = rpoly(1,x) by H10,H12,FINSEQ_3:110; end; suppose H12: j <= k; then H13: g.(k+1) = gq.k by H14b,H6,H14,FINSEQ_3:111; consider y being Element of L such that H10: y is_a_common_root_of z`1,z`2 & g.(k+1) = rpoly(1,y) by H2a,H14c; H25: eval(g2q,y) = 0.L by H13,H10,H11,X101,div2; then 0.L = eval(g2q,y) * eval(g1`1,y) by VECTSP_1:7 .= eval(g2q*'g1`1,y) by POLYNOM4:24 .= eval(q`1,y) by H8,thequiv1; then A1: y is_a_root_of q`1 by POLYNOM5:def 6; 0.L = eval(g2q,y) * eval(g1`2,y) by VECTSP_1:7,H25 .= eval(g2q*'g1`2,y) by POLYNOM4:24 .= eval(q`2,y) by H8a,thequiv1; then y is_a_root_of q`2 by POLYNOM5:def 6; then y is_a_common_root_of q`1,q`2 by A1,root1; hence ex x being Element of L st x is_a_common_root_of q`1,q`2 & gq.k = rpoly(1,x) by H10,H12,H14b,H6,H14,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 H1,H2,I1,I2,I3,I4,AS2,IV; end; end; hence P[n+1]; end; I: for n being Nat holds P[n] from NAT_1:sch 2(IA,IS); 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 I,H1,H2; 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 :defNF: 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 H: 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 ratfuncNF; 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 H; hence thesis; end; suppose z is zero; hence thesis; end; end; uniqueness by ratfuncNFunique2; 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 H: 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 defNF; A: NF z is irreducible by H,tw2; (NF z)`2 = (1.L / LC(z1`2)) * z1`2 by H,XTUPLE_0:def 3; hence thesis by A,defnorm; end; suppose z is zero; then NF z = 0._(L) by defNF; 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 H: 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 defNF; now assume z1`1 = 0_.(L); then 0_.(L) = z2 *' z1`1 by POLYNOM3:34 .= z`1 by H,XTUPLE_0:def 2; hence contradiction by defzerrat; end; then z1 is non zero by defzerrat; hence thesis by H; end; end; defnf1a: 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 defNF; 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 AS: f <> <*>(the carrier of Polynom-Ring(L)); let i be Element of dom f; dom f <> {} by AS; 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,AS; z`1,z`2 have_common_roots by A4,root2; hence contradiction by defirred; 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 ttt; 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 defNF; 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 defNF; 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); B: NF z = NormRatF z by defnf1a .= [(1.L / LC(z`2)) * z`1, (1.L / LC(z`2)) * z`2]; z`2 is normalized by defnorm; then D: LC(z`2) = 1.L by defnormp; C: 1.L / LC(z`2) = 1.L by D,VECTSP_1:def 10; hence NF z = [z`1, (1.L / LC(z`2)) * z`2] by B,POLYNOM5:27 .= [z`1, z`2] by C,POLYNOM5:27 .= z by ttt; 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 defnf1a; tt2: 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 AS: 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 defzer; x1 *' x2 is non zero; hence contradiction by AS; end; hence thesis; end; theorem nfequiv: 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 A: 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 defNF; consider f being FinSequence of Polynom-Ring(L) such that A2: 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 A1; set q = [rpoly(1,x) *' z`1, rpoly(1,x) *' z`2]; now assume q`1 = 0_.(L); then rpoly(1,x) *' z`1 = 0_.(L); then z`1 = 0_.(L) by tt2; hence contradiction by A,defzerrat; end; then reconsider q as non zero rational_function of L by defzerrat; 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 Y: i in dom g; now per cases by Y,FINSEQ_1:25; suppose X: i in dom <*rp*>; then i in {1} by FINSEQ_1:2,FINSEQ_1:38; then i = 1 by TARSKI:def 1; then g.i = <*rp*>.1 by X,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 H: n in dom f & i = len(<*rp*>) + n; J: g.i = f.n by H,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 H,A2; hence ex z being Element of L st g.i = rpoly(1,z) by J; end; end; hence ex z being Element of L st g.i = rpoly(1,z); end; then g2 <> 0_.(L) by div4; then reconsider g2 as non zero Polynomial of L by defzer,POLYNOM3:def 10; A3: now let i be Element of NAT; assume Y: i in dom g; now per cases by Y,FINSEQ_1:25; suppose X: i in dom <*rp*>; then i in {1} by FINSEQ_1:2,FINSEQ_1:38; then i = 1 by TARSKI:def 1; then I: g.i = <*rp*>.1 by X,FINSEQ_1:def 7 .= rp by FINSEQ_1:40; H: 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) by VECTSP_1:7 .= eval(rpoly(1,x) *' z`1,x) by POLYNOM4:24; then x is_a_root_of rpoly(1,x) *' z`1 by POLYNOM5:def 6; then J: x is_a_root_of q`1 by XTUPLE_0:def 2; 0.L = eval(rpoly(1,x),x) * eval(z`2,x) by H,VECTSP_1:7 .= eval(rpoly(1,x) *' z`2,x) by POLYNOM4:24; then x is_a_root_of rpoly(1,x) *' z`2 by POLYNOM5:def 6; then x is_a_root_of q`2 by XTUPLE_0:def 3; then x is_a_common_root_of q`1,q`2 by J,root1; hence ex z being Element of L st z is_a_common_root_of q`1,q`2 & g.i = rpoly(1,z) by I; end; suppose ex n being Nat st n in dom f & i = len(<*rp*>) + n; then consider n being Nat such that H: n in dom f & i = len(<*rp*>) + n; J: g.i = f.n by H,FINSEQ_1:def 7; consider y being Element of L such that I: y is_a_common_root_of z`1,z`2 & f.n = rpoly(1,y) by H,A2; y is_a_root_of z`1 by I,root1; then eval(z`1,y) = 0.L by POLYNOM5:def 6; then 0.L = eval(rpoly(1,x),y) * eval(z`1,y) by VECTSP_1:6 .= eval(rpoly(1,x) *' z`1,y) by POLYNOM4:24; then y is_a_root_of rpoly(1,x) *' z`1 by POLYNOM5:def 6; then K: y is_a_root_of q`1 by XTUPLE_0:def 2; y is_a_root_of z`2 by I,root1; then eval(z`2,y) = 0.L by POLYNOM5:def 6; then 0.L = eval(rpoly(1,x),y) * eval(z`2,y) by VECTSP_1:6 .= eval(rpoly(1,x) *' z`2,y) by POLYNOM4:24; then y is_a_root_of rpoly(1,x) *' z`2 by POLYNOM5:def 6; then y is_a_root_of q`2 by XTUPLE_0:def 3; then y is_a_common_root_of q`1,q`2 by K,root1; hence ex z being Element of L st z is_a_common_root_of q`1,q`2 & g.i = rpoly(1,z) by J,I; 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; A4: Product g = rp * Product f by GROUP_4:7; A5: q`1 = rpoly(1,x) *' z`1 by XTUPLE_0:def 2 .= rpoly(1,x) *' (z2 *' z1`1) by A1,XTUPLE_0:def 2 .= (rpoly(1,x) *' z2) *' z1`1 by POLYNOM3:33 .= g2 *' z1`1 by A4,A2,POLYNOM3:def 10; q`2 = rpoly(1,x) *' z`2 by XTUPLE_0:def 3 .= rpoly(1,x) *' (z2 *' z1`2) by A1,XTUPLE_0:def 3 .= (rpoly(1,x) *' z2) *' z1`2 by POLYNOM3:33 .= g2 *' z1`2 by A4,A2,POLYNOM3:def 10; then q = [g2 *' z1`1, g2 *' z1`2] by A5,ttt; hence thesis by A1,A3,defNF; end; suppose A: z is zero; then z`1 = 0_.(L) by defzerrat; 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 by defzerrat; then NF [rpoly(1,x) *' z`1, rpoly(1,x) *' z`2] = 0._(L) by defNF; hence thesis by A,defNF; 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 A: NF z = 0._(L) by defNF; thus thesis by A,defNF; end; suppose A: z is non zero; H: 1.L <> 0.L; B: NF nfz = NormRatF nfz by A,defnf1a .= [(1.L/LC(nfz`2)) * nfz`1, (1.L/LC(nfz`2)) * nfz`2]; nfz`2 is normalized by defnorm; then D: LC(nfz`2) = 1.L by defnormp; C: 1.L / LC(nfz`2) = 1.L by H,D,VECTSP_1:def 10; then NF nfz = [nfz`1, (1.L / LC(nfz`2)) * nfz`2] by B,POLYNOM5:27 .= [nfz`1, nfz`2] by C,POLYNOM5:27 .= nfz by ttt; hence thesis; end; end; theorem th3: 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 AB: a = 0.L; then AC: a * (LC q) = 0.L by VECTSP_1:7; a <> 1.L by AB; hence contradiction by AC,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; A: now assume z is irreducible; then NF z = NormRatF z by defnf1a .= [(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 H0: 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 H0; H1: x`1 = a * (z`1) & x`2 = a * (z`2) by XTUPLE_0:def 2, XTUPLE_0:def 3; now assume z`1, z`2 have_a_common_root; then consider u being Element of L such that C1: u is_a_common_root_of z`1, z`2 by root2; u is_a_root_of z`1 & u is_a_root_of z`2 by root1,C1; then C3: eval(z`1,u) = 0.L & eval(z`2,u) = 0.L by POLYNOM5:def 6; eval(x`1,u) = a * eval(z`1,u) by H1,POLYNOM5:30; then eval(x`1,u) = 0.L by C3,VECTSP_1:6; then C2: u is_a_root_of x`1 by POLYNOM5:def 6; eval(x`2,u) = a * eval(z`2,u) by H1,POLYNOM5:30; then eval(x`2,u) = 0.L by C3,VECTSP_1:7; then u is_a_root_of x`2 by POLYNOM5:def 6; then u is_a_common_root_of x`1, x`2 by C2,root1; then x`1,x`2 have_a_common_root by root2; hence contradiction by defirred,H0; end; hence z is irreducible by defirred; end; hence thesis by A; 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; th1a: 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 H: a <> 0.L & [a * (z`1), a * (z`2)] = NF(z) by th3; a is non zero by H,STRUCT_0:def 12; then reconsider az2 = a * (z`2) as non zero Polynomial of L; H3: (NF z)`2 = a * (z`2) by H,XTUPLE_0:def 3; thus degree z = max(deg(a * (z`1)), deg(a * (z`2))) by H,XTUPLE_0:def 2,H3 .= max(deg(z`1),deg(az2)) by H,POLYNOM5:25 .= max(degree(z`1),degree(z`2)) by H,POLYNOM5:25; end; theorem th1: 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 H: z is zero; then A: NF z = 0._(L) by defNF .= [0_.(L),1_.(L)]; z`1 = 0_.(L) by H,defzerrat; then B: deg(z`1) = -1 by HURWITZ:20; E: deg 1_.(L) = 1 - 1 by POLYNOM4:4; deg z = max(deg 0_.(L),degree((NF z)`2)) by A,XTUPLE_0:def 2 .= max(deg 0_.(L),deg 1_.(L)) by A,XTUPLE_0:def 3 .= max(-1,deg 1_.(L)) by HURWITZ:20 .= 0 by E,XXREAL_0:def 10; hence thesis by B,XXREAL_0:def 10; end; suppose A: 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 AS: max(degree(z`1),degree(z`2)) = 0; now per cases by AS,XXREAL_0:16; suppose H: degree(z`1) = 0; now assume z`1,z`2 have_common_roots; then consider x being Element of L such that HH: x is_a_common_root_of z`1,z`2 by root2; x is_a_root_of z`1 by HH,root1; then z`1 is with_roots by POLYNOM5:def 7; hence contradiction by HURWITZ:24,H; end; hence z`1,z`2 have_no_common_roots; end; suppose H: degree(z`2) = 0; now assume z`1,z`2 have_common_roots; then consider x being Element of L such that HH: x is_a_common_root_of z`1,z`2 by root2; x is_a_root_of z`2 by HH,root1; then z`2 is with_roots by POLYNOM5:def 7; hence contradiction by HURWITZ:24,H; end; hence z`1,z`2 have_no_common_roots; end; end; then z is irreducible by defirred; then degree z = max(degree(z`1),degree(z`2)) by th1a; hence max(degree((NF z)`1),degree((NF z)`2)) <= max(degree(z`1),degree(z`2)); end; then IA: P[0]; IS: now let n be Nat; assume IV: P[n]; now let z be non zero rational_function of L; assume AS: 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 th1a; 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 by defirred; then consider x being Element of L such that H: x is_a_common_root_of z`1,z`2 by root2; H3: x is_a_root_of z`1 & x is_a_root_of z`2 by H,root1; consider q2 being Polynomial of L such that HY: z`2 = rpoly(1,x) *' q2 by H3,HURWITZ:33; consider q1 being Polynomial of L such that HX: z`1 = rpoly(1,x) *' q1 by H3,HURWITZ:33; q1 <> 0_.(L) by defzerrat,HX,POLYNOM3:34; then reconsider q1 as non zero Polynomial of L by defzer; q2 <> 0_.(L) by HY,POLYNOM3:34; then reconsider q2 as non zero Polynomial of L by defzer; set q = [q1,q2]; now assume q is zero; then q`1 = 0_.(L) by defzerrat; hence contradiction; end; then reconsider q as non zero rational_function of L; z = [rpoly(1,x) *' q1,rpoly(1,x) *' q2] by ttt,HX,HY .= [rpoly(1,x) *' q`1,rpoly(1,x) *' q2] by XTUPLE_0:def 2 .= [rpoly(1,x) *' q`1,rpoly(1,x) *' q`2] by XTUPLE_0:def 3; then HZ: NF z = NF q by nfequiv; HV: n <= n+1 by NAT_1:11; W4: deg z`1 = deg rpoly(1,x) + deg q1 by HX,HURWITZ:23 .= 1 + deg q1 by HURWITZ:27 .= 1 + deg q`1 by XTUPLE_0:def 2; deg z`2 = deg rpoly(1,x) + deg q2 by HY,HURWITZ:23 .= 1 + deg q2 by HURWITZ:27 .= 1 + deg q`2 by XTUPLE_0:def 3; then HU: max(degree(z`1),degree(z`2)) = 1 + max(degree(q`1), degree(q`2)) by W4,maxx; then max(degree((NF z)`1),degree((NF z)`2)) <= max(degree(q`1),degree(q`2)) by IV,HZ,AS; hence max(degree((NF z)`1),degree((NF z)`2)) <= max(degree(z`1),degree(z`2)) by HV,HU,AS,XXREAL_0:2; end; end; hence P[n+1]; end; I: for n being Nat holds P[n] from NAT_1:sch 2(IA,IS); 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 A,I; 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; A: now 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 th3; A2: degree(a * (z`1)) = degree(z`1) by POLYNOM5:25,A1; A3: degree(a * (z`2)) = degree(z`2) by POLYNOM5:25,A1; degree((NF(z))`1) = degree(z`1) by A2,A1,XTUPLE_0:def 2; hence degree z = max(degree(z`1),degree(z`2)) by A3,A1,XTUPLE_0:def 3; end; now assume AS: degree z = max( degree(z`1), degree(z`2)); now assume not(z is irreducible); then p1, p2 have_a_common_root by defirred; then consider x being Element of L such that A1: x is_a_common_root_of p1,p2 by root2; A2: x is_a_root_of p1 & x is_a_root_of p2 by A1,root1; then consider q1 being Polynomial of L such that A3: p1 = rpoly(1,x) *' q1 by HURWITZ:33; consider q2 being Polynomial of L such that A4: p2 = rpoly(1,x) *' q2 by A2,HURWITZ:33; q2 <> 0_.(L) by A4,POLYNOM3:34; then reconsider q2 as non zero Polynomial of L by defzer; set zz = [q1,q2]; H1: zz`1 = q1 & zz`2 = q2; z = [rpoly(1,x) *' zz`1,rpoly(1,x) *' zz`2] by ttt,A3,A4; then NF(z) = NF(zz) by nfequiv; then degree z = degree zz; then A8: degree(z) <= max(degree(q1),degree(q2)) by th1,H1; now per cases; suppose B0: p1 = 0_.(L); B4: q1 = 0_.(L) by B0,A3,tt2; deg(rpoly(1,x)*'q2) + 0 = deg(rpoly(1,x)) + deg(q2) by HURWITZ:23 .= 1 + deg(q2) by HURWITZ:27; then C: deg(q2) < deg(p2) by A4,XREAL_1:8; deg(p1) <= deg(p2) by HURWITZ:20,B0; then B3: max(deg(p1),deg(p2)) = deg(p2) by XXREAL_0:def 10; deg(q1) <= deg(q2) by HURWITZ:20,B4; hence contradiction by B3,C,AS,A8,XXREAL_0:def 10; end; suppose p1 <> 0_.(L); then reconsider p1 as non zero Polynomial of L by defzer; now assume q1 = 0_.(L); then p1 = 0_.(L) by A3,POLYNOM3:34; hence contradiction; end; then reconsider q1 as non zero Polynomial of L by defzer; deg(p1) + 0 = deg(rpoly(1,x)) + deg(q1) by A3,HURWITZ:23 .= 1 + deg(q1) by HURWITZ:27; then H2: deg(q1) < deg(p1) by XREAL_1:8; deg(p2) + 0 = deg(rpoly(1,x)) + deg(q2) by A4,HURWITZ:23 .= 1 + deg(q2) by HURWITZ:27; then deg(q2) < deg(p2) by XREAL_1:8; hence contradiction by AS,A8,H2,XXREAL_0:27; end; end; hence contradiction; end; hence z is irreducible; end; hence thesis by A; 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 ev0: 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)" by XTUPLE_0:def 2 .= 0.L * eval((0._(L))`2,x)" by POLYNOM4:17 .= 0.L by VECTSP_1:7; 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; A: 1.L <> 0.L; thus eval(1._(L),x) = eval(1_.(L),x) * eval((1._(L))`2,x)" by XTUPLE_0:def 2 .= 1.L * eval((1._(L))`2,x)" by POLYNOM4:18 .= 1.L * eval(1_.(L),x)" by XTUPLE_0:def 3 .= 1.L * (1.L)" by POLYNOM4:18 .= 1.L by A,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 AS: 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)" by XTUPLE_0:def 2 .= eval(p`1 *' q`2 + p`2 *' q`1,x) * eval(p`2 *' q`2,x)" by XTUPLE_0:def 3 .= 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 AS,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 AS,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)")) by VECTSP_1:def 8 .= (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 AS,VECTSP_1:def 10 .= eval(p,x) + eval(q,x) by VECTSP_1:def 8; 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 AS: 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)" by XTUPLE_0:def 2 .= eval(p`1 *' q`1,x) * eval(p`2 *' q`2,x)" by XTUPLE_0:def 3 .= 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 AS,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 ev4: 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 AS: eval(p`2,x) <> 0.L; set np = NormRationalFunction p; H: 1.L / LC(p`2) <> 0.L; thus eval(np,x) = eval(1.L / LC(p`2) * p`1,x) * eval(np`2,x)" by XTUPLE_0:def 2 .= eval(1.L / LC(p`2) * p`1,x) * eval(1.L / LC(p`2) * p`2,x)" by XTUPLE_0:def 3 .= (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 AS,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 H,VECTSP_1:def 10 .= eval(p,x) by VECTSP_1:def 8; 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 AS1: eval(p`2,x) <> 0.L; assume AS: not(x is_a_common_root_of p`1,p`2); per cases; suppose H: p is zero; then H1: p`1 = 0_.(L) by defzerrat; H2: NF p = 0._(L) by H,defNF; thus eval(p,x) = 0.L * (eval(p`2,x))" by H1,POLYNOM4:17 .= 0.L by VECTSP_1:7 .= eval(NF p,x) by H2,ev0; end; suppose p is non zero; then consider z1 being rational_function of L, z2 being non zero Polynomial of L such that H: 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 defNF; H1: p`1 = z2 *' z1`1 by H,XTUPLE_0:def 2; H2: p`2 = z2 *' z1`2 by H,XTUPLE_0:def 3; H3: now assume A: eval(z2,x) = 0.L; eval(z2 *' z1`1,x) = eval(z2,x) * eval(z1`1,x) by POLYNOM4:24 .= 0.L by A,VECTSP_1:7; then B: x is_a_root_of p`1 by H1,POLYNOM5:def 6; eval(z2 *' z1`2,x) = eval(z2,x) * eval(z1`2,x) by POLYNOM4:24 .= 0.L by A,VECTSP_1:7; then x is_a_root_of p`2 by H2,POLYNOM5:def 6; hence contradiction by AS,B,root1; end; H6: now assume eval(z1`2,x) = 0.L; then 0.L = eval(z2,x) * eval(z1`2,x) by VECTSP_1:7 .= eval(z2 *' z1`2,x) by POLYNOM4:24; hence contradiction by H,XTUPLE_0:def 3,AS1; end; eval(p,x) = eval(z2 *' z1`1,x) * (eval(z2 *' z1`2,x))" by H,XTUPLE_0:def 3,H1 .= (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 H3,H6,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 H3,VECTSP_1:def 10 .= eval(z1,x) by VECTSP_1:def 8; hence eval(NF p,x) = eval(p,x) by H,H6,ev4; end; end;