:: Some Algebraic Properties of Polynomial Rings :: by Christoph Schwarzweller , Artur Korni{\l}owicz and Agnieszka Rowinska-Schwarzweller :: :: Received June 30, 2016 :: Copyright (c) 2016-2021 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, POLYNOM1, ARYTM_1, FUNCT_1, TARSKI, POLYNOM3, RELAT_1, RLVECT_1, FINSEQ_1, GCD_1, ALGSEQ_1, REALSET1, FINSET_1, CARD_3, FDIFF_1, FUNCT_4, ALGSTR_0, INT_1, WELLORD1, YELLOW_8, HURWITZ, ZFMISC_1, XBOOLE_0, FUNCT_2, LATTICES, VECTSP10, XCMPLX_0, VECTSP_1, VECTSP_2, MSALIMIT, STRUCT_0, SUBSET_1, SUPINF_2, NAT_1, NUMBERS, CARD_1, MESFUNC1, XXREAL_0, RATFUNC1, FUNCSDOM, GROUP_1, INT_2, INT_3, CAT_1, PARTFUN1, POLYNOM2, POLYNOM5, QUOFIELD, BINOP_1, MSSUBFAM, MOD_4, IDEAL_1, RING_2, WAYBEL_6, RING_3, RING_4; notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, FUNCT_1, RELSET_1, PARTFUN1, ORDINAL1, FUNCT_2, QUOFIELD, BINOP_1, FINSEQ_1, REALSET1, FINSET_1, VFUNCT_1, FUNCT_7, NORMSP_1, ALGSEQ_1, XCMPLX_0, XXREAL_0, NAT_D, INT_1, INT_3, NUMBERS, STRUCT_0, MOD_4, GCD_1, ALGSTR_0, GROUP_1, GROUP_6, RLVECT_1, VECTSP_1, VECTSP_2, VECTSP10, POLYNOM1, POLYNOM3, POLYNOM4, POLYNOM5, HURWITZ, RATFUNC1, IDEAL_1, RINGCAT1, RING_1, RING_2, RING_3; constructors POLYNOM4, POLYNOM5, HURWITZ, FUNCT_4, RELSET_1, RINGCAT1, FUNCT_7, NAT_D, VFUNCT_1, RATFUNC1, GCD_1, REALSET1, FVSUM_1, RING_3, ALGSEQ_1, BINOP_2; registrations XBOOLE_0, ORDINAL1, RELSET_1, XCMPLX_0, XXREAL_0, XREAL_0, NAT_1, INT_1, MEMBERED, STRUCT_0, VECTSP_1, ALGSTR_1, POLYNOM3, POLYNOM4, POLYNOM5, FUNCT_2, ALGSTR_0, NAT_2, RLVECT_1, INT_3, CARD_1, RING_3, VFUNCT_1, FINSET_1, RATFUNC1, RING_2, RING_1, REALSET1, MOD_4; requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM; definitions STRUCT_0, VECTSP_1, GROUP_1, ALGSEQ_1, GROUP_6, RINGCAT1; equalities STRUCT_0, HURWITZ, INT_3, POLYNOM3, REALSET1, ALGSTR_0, BINOP_1, RATFUNC1; expansions STRUCT_0, ALGSTR_0, TARSKI, GCD_1; theorems GROUP_1, VECTSP_1, NAT_1, FUNCT_1, FUNCT_2, XREAL_1, INT_1, POLYNOM4, FUNCT_7, ALGSEQ_1, NORMSP_1, TARSKI, POLYNOM3, FUNCOP_1, RING_2, RING_1, POLYNOM1, POLYNOM5, XXREAL_0, FINSEQ_1, NAT_D, CARD_1, ORDINAL1, RLVECT_1, POLYNOM2, PARTFUN1, HURWITZ, REALSET1, STRUCT_0, IDEAL_1, RATFUNC1, GCD_1, RING_3, RINGCAT1, QUOFIELD, ALGSTR_0, ZFMISC_1, VECTSP10, UPROOTS; schemes NAT_1, FUNCT_2, BINOP_1; begin :: Preliminaries definition let R be non empty doubleLoopStr, a be Element of R; redefine func {a} -> Subset of R; coherence proof now let x be object; assume x in {a}; then x = a by TARSKI:def 1; hence x in the carrier of R; end; hence thesis by TARSKI:def 3; end; end; registration cluster almost_left_invertible commutative -> almost_right_invertible for Ring; coherence proof let R be Ring; assume AS: R is almost_left_invertible commutative; now let x be Element of R; assume x <> 0.R; then x is left_invertible by AS; then consider y being Element of R such that A1: y*x = 1.R; x * y = 1.R by A1,AS,GROUP_1:def 12; hence x is right_invertible; end; hence thesis; end; cluster almost_right_invertible commutative -> almost_left_invertible for Ring; coherence proof let R be Ring; assume AS: R is almost_right_invertible commutative; now let x be Element of R; assume x <> 0.R; then x is right_invertible by AS; then consider y being Element of R such that A1: x*y = 1.R; y * x = 1.R by A1,AS,GROUP_1:def 12; hence x is left_invertible; end; hence thesis; end; cluster almost_left_cancelable commutative -> almost_right_cancelable for Ring; coherence proof let R be Ring; assume AS: R is almost_left_cancelable commutative; now let x be Element of R; assume x <> 0.R; then AS1: x is left_mult-cancelable by AS; now let y,z be Element of R; assume y * x = z * x; then x * y = z * x by AS,GROUP_1:def 12 .= x * z by AS,GROUP_1:def 12; hence y = z by AS1; end; hence x is right_mult-cancelable; end; hence thesis; end; cluster almost_right_cancelable commutative -> almost_left_cancelable for Ring; coherence proof let R be Ring; assume AS: R is almost_right_cancelable commutative; now let x be Element of R; assume x <> 0.R; then AS1: x is right_mult-cancelable by AS; now let y,z be Element of R; assume x * y = x * z; then y * x = x * z by AS,GROUP_1:def 12 .= z * x by AS,GROUP_1:def 12; hence y = z by AS1; end; hence x is left_mult-cancelable; end; hence thesis; end; end; definition let L be non empty ZeroStr; let X be set; attr X is L-polynomial-membered means :polymem: for p being object st p in X holds p is Polynomial of L; end; definition let L be non empty ZeroStr; let X be 1-sorted; attr X is L-polynomial-membered means :polymem1: the carrier of X is L-polynomial-membered; end; registration let L be non empty ZeroStr; cluster non empty L-polynomial-membered for set; existence proof take s = {0_.(L)}; thus s is non empty; thus s is L-polynomial-membered by TARSKI:def 1; end; end; registration let L be non empty ZeroStr; cluster non empty L-polynomial-membered for 1-sorted; existence proof take 1-sorted(#the non empty L-polynomial-membered set#); thus thesis; end; end; registration let L be non empty ZeroStr; let X be non empty L-polynomial-membered 1-sorted; cluster the carrier of X -> L-polynomial-membered; coherence by polymem1; end; registration let L be add-associative right_zeroed right_complementable distributive non empty doubleLoopStr; cluster Polynom-Ring L -> L-polynomial-membered; coherence proof thus the carrier of Polynom-Ring L is L-polynomial-membered by POLYNOM3:def 10; end; end; definition let L be non empty ZeroStr; let X be non empty L-polynomial-membered set; redefine mode Element of X -> Polynomial of L; coherence by polymem; end; lm: now let L be add-associative right_zeroed right_complementable distributive non empty doubleLoopStr, a be Element of Polynom-Ring L,p be Polynomial of L; reconsider x = -p as Element of Polynom-Ring L by POLYNOM3:def 10; assume a = p; then a + x = p - p by POLYNOM3:def 10 .= 0_.(L) by POLYNOM3:29 .= 0.(Polynom-Ring(L)) by POLYNOM3:def 10; then a = - x by RLVECT_1:6; hence - a = -p; end; registration let R be Ring; cluster zero for Element of the carrier of Polynom-Ring R; existence proof take 0_.(R); thus thesis by POLYNOM3:def 10; end; cluster zero for Element of Polynom-Ring R; existence proof take 0.(Polynom-Ring R); thus thesis; end; cluster zero for Polynomial of R; existence proof take 0_.(R); thus thesis; end; end; registration let R be non degenerated Ring; cluster non zero for Element of the carrier of Polynom-Ring R; existence proof take 1_.(R); thus thesis by POLYNOM3:def 10; end; cluster non zero for Element of Polynom-Ring R; existence proof take 1.(Polynom-Ring R); thus thesis; end; end; T8a: for L being add-associative right_zeroed right_complementable distributive non trivial doubleLoopStr, p being Element of the carrier of Polynom-Ring L holds deg p is Element of NAT iff p <> 0.Polynom-Ring L proof let L be add-associative right_zeroed right_complementable distributive non trivial doubleLoopStr; let p be Element of the carrier of Polynom-Ring L; set R = Polynom-Ring L; reconsider pp = p as Polynomial of L; A: now assume deg p is Element of NAT; then p <> 0_.(L) by HURWITZ:20; hence p <> 0.R by POLYNOM3:def 10; end; now assume p <> 0.R; then p <> 0_.(L) by POLYNOM3:def 10; then len p <> 0 by POLYNOM4:5; then len p + 1 > 0 + 1 by XREAL_1:6; then len p >= 1 by NAT_1:13; then len p - 1 >= 1 - 1 by XREAL_1:9; hence deg p is Element of NAT by INT_1:3; end; hence thesis by A; end; T8b: for L being non empty ZeroStr, p being Polynomial of L holds deg p is Element of NAT iff p <> 0_.(L) proof let L be non empty ZeroStr;let p be Polynomial of L; now assume p <> 0_.(L); then len p <> 0 by POLYNOM4:5; then len p + 1 > 0 + 1 by XREAL_1:6; then len p >= 1 by NAT_1:13; then len p - 1 >= 1 - 1 by XREAL_1:9; hence deg(p) is Element of NAT by INT_1:3; end; hence thesis by HURWITZ:20; end; definition let L be add-associative right_zeroed right_complementable distributive non empty doubleLoopStr; let p,q be Polynomial of L; pred p divides q means ex a,b being Element of Polynom-Ring L st a = p & b = q & a divides b; end; theorem T2: for L being add-associative right_zeroed right_complementable distributive non empty doubleLoopStr for p,q be Polynomial of L holds p divides q iff ex r being Polynomial of L st p *' r = q proof let L be add-associative right_zeroed right_complementable distributive non empty doubleLoopStr; let p,q be Polynomial of L; X: now assume p divides q; then consider a,b being Element of Polynom-Ring L such that B: a = p & b = q & a divides b; consider u being Element of Polynom-Ring L such that C: a * u = b by B; reconsider z = u as Polynomial of L by POLYNOM3:def 10; q = p *' z by B,C,POLYNOM3:def 10; hence ex r being Polynomial of L st p *' r = q; end; now assume ex r being Polynomial of L st p *' r = q; then consider r being Polynomial of L such that H: q = p *' r; reconsider a=p,b=q,u=r as Element of Polynom-Ring L by POLYNOM3:def 10; b = a * u by H,POLYNOM3:def 10; then a divides b; hence p divides q; end; hence thesis by X; end; theorem div1: for F being Field, p,q being Polynomial of F st deg p < deg q holds p mod q = p proof let F be Field, p,q be Polynomial of F; assume A1: deg p < deg q; 0_.(F) = 0.Polynom-Ring(F) by POLYNOM3:def 10; then H: -(0_.(F)) = - 0.Polynom-Ring(F) by lm .= 0.Polynom-Ring(F); A0: now assume A0: q = 0_.(F); then deg p < - 1 by A1,HURWITZ:20; hence contradiction by A0,A1,T8b; end; p = 0_.(F) + p by POLYNOM3:28 .= ((0_.(F)) *' q) + p by POLYNOM3:34; hence p mod q = p - (0_.(F)) *' q by A0,A1,HURWITZ:def 5 .= p - 0_.(F) by POLYNOM3:34 .= p + 0_.(F) by H,POLYNOM3:def 10 .= p by POLYNOM3:28; end; div0: for F being Field, p,q being Polynomial of F st q divides p holds (p div q) *' q = p proof let F be Field, p,q be Polynomial of F; assume q divides p; then consider r being Polynomial of F such that A2: q *' r = p by T2; per cases; suppose A3: q = 0_.(F); thus (p div q) *' q = 0_.(F) by A3,POLYNOM3:34 .= p by A2,A3,POLYNOM3:34; end; suppose A3: q <> 0_.(F); A4: p = q *' r + 0_.(F) by A2,POLYNOM3:28; deg 0_.(F) = -1 by HURWITZ:20; then deg 0_.(F) < deg q by T8b,A3; hence (p div q) *' q = p by A2,A4,HURWITZ:def 5; end; end; theorem div2: for F being Field, p,q being Polynomial of F holds p mod q = 0_.(F) iff q divides p proof let F be Field, p,q be Polynomial of F; A: now assume p mod q = 0_.(F); then (p div q) *' q = (p - (p div q) *' q) + (p div q) *' q by POLYNOM3:28 .= p + (-((p div q) *' q) + (p div q) *' q) by POLYNOM3:26 .= p + ((p div q) *' q - (p div q) *' q) .= p + 0_.(F) by POLYNOM3:29 .= p by POLYNOM3:28; hence q divides p by T2; end; now assume A: q divides p; thus p mod q = p - p by A,div0 .= 0_.(F) by POLYNOM3:29; end; hence thesis by A; end; theorem div5: for F being Field, p,q being Polynomial of F holds p = (p div q) *' q + (p mod q) proof let F be Field, p,q be Polynomial of F; thus p = p + 0_.(F) by POLYNOM3:28 .= p + ((p div q) *' q - (p div q) *' q) by POLYNOM3:29 .= (p + -((p div q) *' q)) + (p div q) *' q by POLYNOM3:26 .= (p div q) *' q + (p mod q); end; theorem div4: for F being Field, p,r being Polynomial of F for q being non zero Polynomial of F holds (p + r) div q = (p div q) + (r div q) & (p + r) mod q = (p mod q) + (r mod q) proof let F be Field, p,r be Polynomial of F; let q be non zero Polynomial of F; H: q <> 0_.(F); A: p + r = ((p div q) *' q + (p mod q)) + r by div5 .= ((p div q) *' q + (p mod q)) + ((r div q) *' q + (r mod q)) by div5 .= (p div q) *' q + ((p mod q) + ((r div q) *' q + (r mod q))) by POLYNOM3:26 .= (p div q) *' q + (((p mod q) + (r mod q)) + ((r div q) *' q)) by POLYNOM3:26 .= ((p div q) *' q + (r div q) *' q) + ((p mod q) + (r mod q)) by POLYNOM3:26 .= ((p div q) + (r div q)) *' q + ((p mod q) + (r mod q)) by POLYNOM3:32; B: deg((p mod q) + (r mod q)) <= max(deg(p mod q),deg(r mod q)) by HURWITZ:22; C: deg(p mod q) < deg q by RING_2:29; deg(r mod q) < deg q by RING_2:29; then max(deg(p mod q),deg(r mod q)) < max(deg q,deg q) by C,XXREAL_0:27; then D: deg((p mod q) + (r mod q)) < deg q by B,XXREAL_0:2; hence (p + r) div q = (p div q) + (r div q) by A,H,HURWITZ:def 5; thus (p + r) mod q = ((p div q) + (r div q)) *' q + ((p mod q) + (r mod q)) - (((p div q) + (r div q)) *' q) by D,A,H,HURWITZ:def 5 .= (((p div q) + (r div q)) *' q - (((p div q) + (r div q)) *' q)) + ((p mod q) + (r mod q)) by POLYNOM3:26 .= 0_.(F) + ((p mod q) + (r mod q)) by POLYNOM3:29 .= (p mod q) + (r mod q) by POLYNOM3:28; end; theorem div3a: for F being Field, p,r being Polynomial of F for q being non zero Polynomial of F holds (p *' r) mod q = ((p mod q) *' (r mod q)) mod q proof let F be Field, p,r be Polynomial of F; let q be non zero Polynomial of F; H1: (((p div q) *' q) *' ((r div q) *' q) + ((p div q) *' q) *' (r mod q)) = ((((p div q) *' q) *' (r div q))) *' q + ((p div q) *' q) *' (r mod q) by POLYNOM3:33 .= q *' ((((p div q) *' q) *' (r div q))) + q *' ((p div q) *' (r mod q)) by POLYNOM3:33 .= q *' (((((p div q) *' q) *' (r div q))) + (p div q) *' (r mod q)) by POLYNOM3:31; H2: (p mod q) *' ((r div q) *' q) = q *' ((p mod q) *' (r div q)) by POLYNOM3:33; p *' r = ((p div q) *' q + (p mod q)) *' r by div5 .= ((p div q) *' q + (p mod q)) *' ((r div q) *' q + (r mod q)) by div5 .= ((p div q) *' q) *' ((r div q) *' q + (r mod q)) + (p mod q) *' ((r div q) *' q + (r mod q)) by POLYNOM3:31 .= (((p div q) *' q) *' ((r div q) *' q) + ((p div q) *' q) *' (r mod q)) + (p mod q) *' ((r div q) *' q + (r mod q)) by POLYNOM3:31 .= (((p div q) *' q) *' ((r div q) *' q) + ((p div q) *' q) *' (r mod q)) + ((p mod q) *' ((r div q) *' q) + (p mod q) *' (r mod q)) by POLYNOM3:31; hence (p *' r) mod q = ((((p div q) *' q) *' ((r div q) *' q) + ((p div q) *' q) *' (r mod q)) mod q) + (((p mod q) *' ((r div q) *' q) + (p mod q) *' (r mod q)) mod q) by div4 .= 0_.(F) + (((p mod q) *' ((r div q) *' q) + (p mod q) *' (r mod q)) mod q) by div2,H1,T2 .= (((p mod q) *' ((r div q) *' q) + (p mod q) *' (r mod q)) mod q) by POLYNOM3:28 .= (((p mod q) *' ((r div q) *' q)) mod q) + (((p mod q) *' (r mod q)) mod q) by div4 .= 0_.(F) + (((p mod q) *' (r mod q)) mod q) by div2,H2,T2 .= ((p mod q) *' (r mod q)) mod q by POLYNOM3:28; end; theorem div3: for F being Field, r,q,u being Polynomial of F for p being non zero Polynomial of F holds (((r *' q) mod p) *' u) mod p = (r *' q *' u) mod p proof let F be Field, r,q,u be Polynomial of F; let p be non zero Polynomial of F; A: (((r *' q) mod p) *' u) mod p = ((r *' q) *' u + (-((r *' q) div p) *' p) *' u) mod p by POLYNOM3:32 .= (((r *' q) *' u) mod p) + (((-((r *' q) div p) *' p) *' u) mod p) by div4; (-((r *' q) div p) *' p) *' u = (p *' (-((r *' q) div p))) *' u by HURWITZ:12 .= p *' ((-((r *' q) div p)) *' u) by POLYNOM3:33; hence (((r *' q) mod p) *' u) mod p = ((r *' q) *' u) mod p + 0_.(F) by A,div2,T2 .= (r *' q *' u) mod p by POLYNOM3:28; end; theorem for L being add-associative right_zeroed right_complementable left-distributive non empty doubleLoopStr, p being sequence of L holds 0.L * p = 0_.(L) proof let L be add-associative right_zeroed right_complementable left-distributive non empty doubleLoopStr, p be sequence of L; set t = 0.L * p; now let x be object; assume x in NAT; then reconsider i = x as Element of NAT; thus t.x = 0.L * (p.i) by POLYNOM5:def 4 .= (0_.(L)).x by FUNCOP_1:7; end; hence thesis by FUNCT_2:12; end; theorem poly2a: for L being left_unital non empty doubleLoopStr, p being sequence of L holds 1.L * p = p proof let L be left_unital non empty doubleLoopStr, p be sequence of L; set t = 1.L * p; now let x be object; assume x in NAT; then reconsider i = x as Element of NAT; thus t.x = 1.L * (p.i) by POLYNOM5:def 4 .= p.x; end; hence thesis by FUNCT_2:12; end; theorem poly2: for L being add-associative right_zeroed right_complementable right_unital distributive associative commutative non empty doubleLoopStr, p,q being sequence of L, a being Element of L holds a * (p *' q) = p *' (a * q) proof let R be add-associative right_zeroed right_complementable right_unital distributive associative commutative non empty doubleLoopStr, p,q be sequence of R, a be Element of R; set t = a * (p *' q); now let x be object; assume x in NAT; then reconsider i = x as Element of NAT; consider F being FinSequence of the carrier of R such that H1: len F = i+1 & (p*'q).i = Sum F & for k being Element of NAT st k in dom F holds F.k = p.(k-'1) * q.(i+1-'k) by POLYNOM3:def 9; consider G being FinSequence of the carrier of R such that H2: len G = i+1 & (p*'(a*q)).i = Sum G & for k being Element of NAT st k in dom G holds G.k = p.(k-'1) * (a*q).(i+1-'k) by POLYNOM3:def 9; H3: dom F = Seg(i+1) by H1,FINSEQ_1:def 3 .= dom G by H2,FINSEQ_1:def 3; now let x be object; assume H4: x in dom F; then reconsider j = x as Element of NAT; H5: F.j = p.(j-'1) * q.(i+1-'j) by H4,H1; G/.j = G.j by H3,H4,PARTFUN1:def 6 .= p.(j-'1) * (a*q).(i+1-'j) by H2,H4,H3 .= p.(j-'1) * (a * q.(i+1-'j)) by POLYNOM5:def 4 .= (p.(j-'1) * q.(i+1-'j)) * a by GROUP_1:def 3 .= a*(F/.j) by PARTFUN1:def 6,H5,H4; hence G/.x = a * (F/.x); end; then G = a * F by H3,POLYNOM1:def 1; then Sum G = a * (Sum F) by POLYNOM1:12; hence t.x = (p *' (a * q)).x by H1,POLYNOM5:def 4,H2; end; hence thesis by FUNCT_2:12; end; theorem poly3: for L being associative non empty multMagma, p being sequence of L, a,b being Element of L holds (a * b) * p = a * (b * p) proof let L be associative non empty multMagma, p being sequence of L, a,b being Element of L; now let x be object; assume x in NAT; then reconsider i = x as Element of NAT; thus ((a * b) * p).x = (a * b) * (p.i) by POLYNOM5:def 4 .= a * (b * (p.i)) by GROUP_1:def 3 .= a * ((b * p).i) by POLYNOM5:def 4 .= (a * (b * p)).x by POLYNOM5:def 4; end; hence thesis by FUNCT_2:12; end; theorem poly1: for L being add-associative right_zeroed right_complementable left-distributive left_unital non empty doubleLoopStr for p being sequence of L holds (1_.(L)) *' p = p proof let R be add-associative right_zeroed right_complementable left-distributive left_unital non empty doubleLoopStr, p be sequence of R; set q = 1_.(R); now let x be object; assume x in NAT; then reconsider i = x as Element of NAT; consider F being FinSequence of the carrier of R such that H: len F = i+1 & (q*'p).i = Sum F & for k being Element of NAT st k in dom F holds F.k = q.(k-'1) * p.(i+1-'k) by POLYNOM3:def 9; D: now let j be Element of NAT; assume B: j in dom F & j <> 1; then j in Seg(len F) by FINSEQ_1:def 3; then 1 <= j & j <= i+1 by H,FINSEQ_1:1; then j > 1 by B,XXREAL_0:1; then q.(j-'1) = 0.R by POLYNOM3:30,NAT_D:36; hence 0.R = q.(j-'1) * p.(i+1-'j) .= F.j by B,H .= F/.j by B,PARTFUN1:def 6; end; G: dom F = Seg(i+1) by H,FINSEQ_1:def 3; E: 1 <= 1 & 1 <= i + 1 by NAT_1:11; then F: Sum F = F/.1 by D,POLYNOM2:3,G,FINSEQ_1:1; F.1 = q.(1-'1) * p.(i+1-'1) by H,E,G,FINSEQ_1:1 .= q.0 * p.(i+1-'1) by XREAL_1:232 .= q.0 * p.i by NAT_D:34 .= 1.R * p.i by POLYNOM3:30 .= p.i; hence (q*'p).x = p.x by E,H,F,PARTFUN1:def 6,G,FINSEQ_1:1; end; hence thesis by FUNCT_2:12; end; registration let L be add-associative right_zeroed right_complementable well-unital distributive non empty doubleLoopStr; cluster Polynom-Ring L -> well-unital; coherence proof set R = Polynom-Ring L; now let x be Element of R; reconsider p = x as Polynomial of L by POLYNOM3:def 10; set e = 1.R; A2: 1.R = 1_.L by POLYNOM3:def 10; hence x*e = p*'1_.L by POLYNOM3:def 10 .= x by POLYNOM3:35; thus e*x = (1_.L)*'p by A2,POLYNOM3:def 10 .= x by poly1; end; hence thesis by VECTSP_1:def 6; end; end; begin :: Constant Polynomials definition let R be add-associative right_zeroed right_complementable distributive non empty doubleLoopStr; let x be Element of the carrier of Polynom-Ring R; attr x is constant means :defconst: deg x <= 0; end; registration let R be non degenerated Ring; cluster non zero constant for Element of Polynom-Ring R; existence proof reconsider a = 1_.(R) as Element of Polynom-Ring R by POLYNOM3:def 10; reconsider p = a as Element of the carrier of Polynom-Ring R; take a; thus a is non zero by POLYNOM3:def 10; thus a is constant by RATFUNC1:def 2; end; cluster non zero constant for Element of the carrier of Polynom-Ring R; existence proof reconsider a = 1_.(R) as Element of the carrier of Polynom-Ring R by POLYNOM3:def 10; take a; thus a is non zero; len 1_.(R) = 1 by POLYNOM4:4; hence a is constant; end; end; registration let R be domRing; cluster non constant for Element of Polynom-Ring R; existence proof set p = rpoly(1,0.R) *' rpoly(1,0.R); reconsider a = p as Element of Polynom-Ring R by POLYNOM3:def 10; take a; deg(rpoly(1,0.R) *' rpoly(1,0.R)) = deg rpoly(1,0.R) + deg rpoly(1,0.R) by HURWITZ:23 .= 1 + deg rpoly(1,0.R) by HURWITZ:27 .= 1 + 1 by HURWITZ:27; hence a is non constant; end; cluster non constant for Element of the carrier of Polynom-Ring R; existence proof set p = rpoly(1,0.R) *' rpoly(1,0.R); reconsider a = p as Element of Polynom-Ring R by POLYNOM3:def 10; take a; deg(rpoly(1,0.R) *' rpoly(1,0.R)) = deg rpoly(1,0.R) + deg rpoly(1,0.R) by HURWITZ:23 .= 1 + deg rpoly(1,0.R) by HURWITZ:27 .= 1 + 1 by HURWITZ:27; hence a is non constant; end; end; definition let L be non empty ZeroStr; let a be Element of L; func a|L -> sequence of L equals 0_.(L)+*(0,a); coherence; end; registration let L be non empty ZeroStr; let a be Element of L; cluster a|L -> finite-Support; coherence proof take 1; let i be Nat; assume i >=1; hence (a|L).i = (0_.(L)).i by FUNCT_7:32 .= 0.L by ORDINAL1:def 12,FUNCOP_1:7; end; end; Th28: for L be non empty ZeroStr, a be Element of L holds (a|L).0 = a & for n be Nat st n <> 0 holds (a|L).n = 0.L proof let L be non empty ZeroStr, a be Element of L; 0 in NAT; then 0 in dom 0_.(L) by FUNCT_2:def 1; hence (a|L).0 = a by FUNCT_7:31; let n be Nat; assume n <> 0; hence (a|L).n = (0_.(L)).n by FUNCT_7:32 .= 0.L by ORDINAL1:def 12,FUNCOP_1:7; end; T6: for L being non empty ZeroStr holds (0.L)|L = 0_.L proof let L be non empty ZeroStr; set p = (0.L)|L; A2: now let x be object; assume x in dom p; then reconsider i = x as Element of NAT; per cases; suppose i = 0; hence p.x = 0.L by Th28; end; suppose i <> 0; hence p.x = 0.L by Th28; end; end; dom p = NAT by NORMSP_1:12; hence thesis by A2,FUNCOP_1:11; end; registration let L be non empty ZeroStr; let a be Element of L; cluster a|L -> constant; coherence proof per cases; suppose a = 0.L; then (a|L) = 0_.L by T6; then len(a|L) = 0 by POLYNOM4:3; then deg(a|L) = -1; hence thesis by RATFUNC1:def 2; end; suppose A0: a <> 0.L; A1: now let i be Nat; assume that A2: i is_at_least_length_of a|L and A3: 0+1 > i; 0 >= i by A3,NAT_1:13; then (a|L).0 = 0.L by A2,ALGSEQ_1:def 2; hence contradiction by A0,Th28; end; for i be Nat st i >= 1 holds (a|L).i = 0.L by Th28; then len(a|L) = 1 by A1,ALGSEQ_1:def 3,ALGSEQ_1:def 2; then deg(a|L) = 0; hence thesis by RATFUNC1:def 2; end; end; end; registration let L be non trivial ZeroStr; let a be non zero Element of L; cluster a|L -> non zero; coherence proof (a|L).0 = a by Th28; then (a|L) <> 0_.L by FUNCOP_1:7; hence thesis by UPROOTS:def 5; end; end; registration let L be non trivial ZeroStr; cluster non zero constant for Polynomial of L; existence proof take (the non zero Element of L)|L; thus thesis; end; end; theorem for L being non empty ZeroStr holds (0.L)|L = 0_.L by T6; theorem for L being non empty multLoopStr_0 holds (1.L)|L = 1_.(L); registration let L be non empty ZeroStr; cluster (0.L)|L -> zero; coherence by T6; end; registration let L be non degenerated multLoopStr_0; cluster (1.L)|L -> non zero; coherence; end; theorem LX: for L being add-associative right_zeroed right_complementable distributive non empty doubleLoopStr, p being Element of the carrier of Polynom-Ring L holds p is non zero constant iff deg p = 0 proof let L be add-associative right_zeroed right_complementable distributive non empty doubleLoopStr, p be Element of the carrier of Polynom-Ring L; A: now assume AS: p is non zero constant; now assume deg p <> 0; then len p - 1 + 1 < 0 + 1 by AS,XREAL_1:6; then len p = 0 by NAT_1:14; then deg p = -1; then p = 0_.(L) by HURWITZ:20; hence contradiction by AS; end; hence deg p = 0; end; now assume AS: deg p = 0; then p <> 0_.(L) by HURWITZ:20; hence p is non zero by UPROOTS:def 5; thus p is constant by AS; end; hence thesis by A; end; theorem LX1: for L being add-associative right_zeroed right_complementable right-distributive right_unital non empty doubleLoopStr, a being Element of L holds a|L = a * 1_.(L) proof let L be add-associative right_zeroed right_complementable right-distributive right_unital non empty doubleLoopStr, a be Element of L; now let x be object; assume x in NAT; then reconsider i = x as Element of NAT; per cases; suppose A: i = 0; thus (a * 1_.(L)).x = a * (1_.(L)).i by POLYNOM5:def 4 .= a * 1.L by A,POLYNOM3:30 .= a .= (a|L).x by Th28,A; end; suppose A: i > 0; thus (a * 1_.(L)).x = a * (1_.(L)).i by POLYNOM5:def 4 .= a * 0.L by A,POLYNOM3:30 .= (a|L).x by Th28,A; end; end; hence thesis by FUNCT_2:12; end; theorem T4a: for R being Ring for a,b being Element of R holds a|R + b|R = (a + b)|R proof let R be Ring, a,b be Element of R; set p = (a|R) + (b|R), q = (a + b)|R; A: dom p = NAT by FUNCT_2:def 1 .= dom q by FUNCT_2:def 1; now let x be object; assume x in dom q; then reconsider i = x as Element of NAT; B: p.i = (a|R).i + (b|R).i by NORMSP_1:def 2; per cases; suppose S: i = 0; hence q.x = a + b by Th28 .= (a|R).i + b by S,Th28 .= p.x by B,S,Th28; end; suppose S: i <> 0; hence q.x = 0.R by Th28 .= (a|R).i + 0.R by S,Th28 .= p.x by B,S,Th28; end; end; hence thesis by A,FUNCT_1:2; end; theorem T4: for R being Ring for a,b being Element of R holds (a|R) *' (b|R) = (a * b)|R proof let R be Ring, a,b being Element of R; set p = a|R, q = b|R; now let x be object; assume x in NAT; then reconsider i = x as Element of NAT; consider F being FinSequence of the carrier of R such that H: len F = i+1 & (p*'q).i = Sum F & for k being Element of NAT st k in dom F holds F.k = p.(k-'1) * q.(i+1-'k) by POLYNOM3:def 9; per cases; suppose A: i = 0; then 1 in Seg(len F) by H,FINSEQ_1:1; then 1 in dom F by FINSEQ_1:def 3; then F.1 = p.(0+1-'1) * q.(i+1-'1) by H .= p.0 * q.(i+1-'1) by NAT_D:34 .= p.0 * q.0 by NAT_D:34,A .= a * q.0 by Th28 .= a * b by Th28; then F = <*a*b*> by FINSEQ_1:40,A,H; hence (p*'q).x = a * b by H,RLVECT_1:44 .= (a * b)|R.x by A,Th28; end; suppose A: i > 0; now let j be Element of NAT; assume B: j in dom F; then j in Seg(len F) by FINSEQ_1:def 3; then C: 1 <= j & j <= i+1 by H,FINSEQ_1:1; p.(j-'1) = 0.R or q.(i+1-'j) = 0.R proof assume p.(j-'1) <> 0.R; then j <= 1 by NAT_D:36,Th28; then j = 1 by C,XXREAL_0:1; then i + 1 -'j = i by NAT_D:34; hence q.(i+1-'j) = 0.R by A,Th28; end; hence 0.R = p.(j-'1) * q.(i+1-'j) .= F.j by B,H; end; hence (p*'q).x = 0.R by H,POLYNOM3:1 .= (a * b)|R.x by A,Th28; end; end; hence thesis by FUNCT_2:12; end; theorem T9: for R being Ring for a,b being Element of R holds a|R = b|R iff a = b proof let R be Ring, a,b be Element of R; now assume a|R = b|R; hence a = (b|R).0 by Th28 .= b by Th28; end; hence thesis; end; theorem T11: for R being Ring for p being Element of the carrier of Polynom-Ring R holds p is constant iff ex a being Element of R st p = a|R proof let L be Ring, p be Element of the carrier of Polynom-Ring L; reconsider g = p as Polynomial of L; now assume p is constant; then AS: (len p) - 1 + 1 <= 0+1 by XREAL_1:6; per cases by AS,NAT_1:25; suppose len p = 0; then p = 0_.(L) by POLYNOM4:5 .= (0.L)|L by T6; hence ex a being Element of L st p = a|L; end; suppose AS: len p = 1; set q = (p.0)|L; now let x be object; assume x in NAT; then reconsider i = x as Element of NAT; per cases; suppose i = 0; hence q.x = p.x by Th28; end; suppose B: i <> 0; then i + 1 > 0 + 1 by XREAL_1:6; then i >= len p by AS,NAT_1:13; hence p.x = 0.L by ALGSEQ_1:8 .= q.x by B,Th28; end; end; hence ex a being Element of L st p = a|L by FUNCT_2:12; end; end; hence thesis by RATFUNC1:def 2; end; theorem T11a: for R being Ring, a being Element of R holds deg(a|R) = 0 iff a <> 0.R proof let L be Ring, a be Element of L; now assume Y: a <> 0.L; now assume deg(a|L) < 0; then a|L = 0_.(L) by T8b .= (0.L)|L by T6; hence contradiction by Y,T9; end; hence deg(a|L) = 0 by RATFUNC1:def 2; end; hence thesis by T8b,T6; end; begin :: Monic Polynomials notation let L be non empty doubleLoopStr; let p be Polynomial of L; synonym p is monic for p is normalized; end; registration let L be non degenerated doubleLoopStr; cluster 1_.(L) -> monic; coherence proof len(1_.(L)) -' 1 = 1 -' 1 by POLYNOM4:4 .= 0 by XREAL_1:232; then LC(1_.(L)) = 1.L by POLYNOM3:30; hence 1_.(L) is monic by RATFUNC1:def 7; end; cluster 0_.(L) -> non monic; coherence proof C: 1.L <> 0.L; LC(0_.(L)) = 0.L by FUNCOP_1:7; hence 0_.(L) is non monic by C,RATFUNC1:def 7; end; end; registration let L be non degenerated doubleLoopStr; cluster monic for Polynomial of L; existence proof 1_.(L) is monic; hence thesis; end; cluster non monic for Polynomial of L; existence proof 0_.(L) is non monic; hence thesis; end; end; registration let L be add-associative right_zeroed right_complementable distributive non degenerated doubleLoopStr; cluster monic for Element of the carrier of Polynom-Ring L; existence proof 1_.(L) is Element of the carrier of Polynom-Ring L by POLYNOM3:def 10; hence thesis; end; cluster non monic for Element of the carrier of Polynom-Ring L; existence proof 0_.(L) is Element of the carrier of Polynom-Ring L by POLYNOM3:def 10; hence thesis; end; end; registration let L be well-unital non degenerated doubleLoopStr; let x be Element of L; cluster rpoly(1,x) -> monic; coherence proof set p = rpoly(1,x); 1 = deg p by HURWITZ:27 .= len(p) - 1; then 1 + 1 = len p; then len(p) -' 1 = 1 by NAT_D:34; then LC p = 1.L by HURWITZ:25; hence p is monic by RATFUNC1:def 7; end; end; definition let L be Field; let p be Element of the carrier of Polynom-Ring L; redefine func NormPolynomial p -> Element of the carrier of Polynom-Ring L; coherence by POLYNOM3:def 10; end; registration let F be Field; let p be non zero Polynomial of F; cluster NormPolynomial p -> monic; coherence; end; registration let L be Field; let p be non zero Element of the carrier of Polynom-Ring L; cluster NormPolynomial p -> monic; coherence; end; theorem npl0: for F being Field holds NormPolynomial(0_.(F)) = 0_.(F) proof let F be Field; set q = 0_.(F); set p = NormPolynomial q; now let x be object; assume x in NAT; then reconsider i = x as Element of NAT; p.i = q.i / q.(len q-'1) by POLYNOM5:def 11 .= 0.F * (q.(len q-'1))" by FUNCOP_1:7 .= q.i by FUNCOP_1:7; hence p.x = q.x; end; hence thesis by FUNCT_2:12; end; theorem npl: for F being Field, p being non zero Element of the carrier of Polynom-Ring F holds NormPolynomial p = (LC p)" * p proof let F be Field, p be non zero Element of the carrier of Polynom-Ring F; now let x be object; assume x in NAT; then reconsider i = x as Element of NAT; thus ((LC p)" * p).x = (LC p)" * (p.i) by POLYNOM5:def 4 .= p.i / p.(len p-'1) .= (NormPolynomial p).x by POLYNOM5:def 11; end; hence thesis by FUNCT_2:12; end; theorem for F being Field, p being non zero Element of the carrier of Polynom-Ring F holds p is monic iff NormPolynomial p = p proof let F be Field, p be non zero Element of the carrier of Polynom-Ring F; hereby assume p is monic; then LC p = 1.F by RATFUNC1:def 7; hence NormPolynomial p = (1.F)" * p by npl .= p by poly2a; end; thus thesis; end; theorem np1: for F being Field, p,q being Element of the carrier of Polynom-Ring F holds q divides p iff NormPolynomial(q) divides p proof let F be Field, p,q being Element of the carrier of Polynom-Ring F; per cases; suppose q = 0_.(F); hence thesis by npl0; end; suppose AS: q <> 0_.(F); then AS1: q is non zero by UPROOTS:def 5; A: now assume q divides p; then consider r being Polynomial of F such that A1: p = q *' r by T2; set a = (LC q)"; reconsider qq = NormPolynomial(q) as Polynomial of F; q is non zero by AS,UPROOTS:def 5; then LC q <> 0.F; then (LC q)" * (LC q) = 1.F by VECTSP_1:def 10; then a <> 0.F; then a" * a = 1.F by VECTSP_1:def 10; then p = (a * a") * p by poly2a .= (a * (a" * (q *' r))) by A1,poly3 .= (a * (q *' (a" * r))) by poly2 .= (a * q) *' (a" * r) by poly2 .= qq *' (a" * r) by AS1,npl; hence NormPolynomial(q) divides p by T2; end; now assume A0: NormPolynomial(q) divides p; reconsider qq = NormPolynomial(q) as Polynomial of F; consider r being Polynomial of F such that A1: p = qq *' r by A0,T2; p = ((LC q)" * q) *' r by AS1,A1,npl .= (LC q)" * (q *' r) by poly2 .= q *' ((LC q)" * r) by poly2; hence q divides p by T2; end; hence thesis by A; end; end; theorem np2: for F being Field, p,q being Element of the carrier of Polynom-Ring F holds q divides p iff q divides NormPolynomial(p) proof let F be Field, p,q being Element of the carrier of Polynom-Ring F; per cases; suppose p = 0_.(F); hence thesis by npl0; end; suppose AS: p <> 0_.(F); then AS1: p is non zero by UPROOTS:def 5; A: now assume q divides p; then consider r being Polynomial of F such that A1: p = q *' r by T2; set a = (LC p)"; NormPolynomial p = a * (q *' r) by AS1,A1,npl .= q *' (a * r) by poly2; hence q divides NormPolynomial(p) by T2; end; now assume q divides NormPolynomial(p); then consider r being Polynomial of F such that A1: NormPolynomial(p) = q *' r by T2; set a = (LC p)"; p is non zero by AS,UPROOTS:def 5; then LC p <> 0.F; then (LC p)" * (LC p) = 1.F by VECTSP_1:def 10; then a <> 0.F; then a" * a = 1.F by VECTSP_1:def 10; then p = (a" * a) * p by poly2a .= a" * (a * p) by poly3 .= a" * (q *' r) by AS1,A1,npl .= q *' (a" * r) by poly2; hence q divides p by T2; end; hence thesis by A; end; end; theorem np3: for F being Field, p being Element of the carrier of Polynom-Ring F holds NormPolynomial(p) is_associated_to p proof let F be Field, p be Element of the carrier of Polynom-Ring F; reconsider a = p, b = NormPolynomial(p) as Element of Polynom-Ring F; A: p *' 1_.(F) = p by POLYNOM3:35; then B: p divides NormPolynomial(p) by T2,np2; NormPolynomial(p) divides p by A,np1,T2; hence thesis by B; end; theorem thirr2: for F being Field, p being Element of the carrier of Polynom-Ring F holds NormPolynomial(p) is irreducible iff p is irreducible proof let F be Field, p be Element of the carrier of Polynom-Ring F; now assume B: NormPolynomial p is irreducible; NormPolynomial p is_associated_to p by np3; hence p is irreducible by B, RING_2:23; end; hence thesis by np3,RING_2:23; end; theorem np00: for R being domRing, p,q being Element of the carrier of Polynom-Ring R holds p is_associated_to q implies deg p = deg q proof let R be domRing, p,q be Element of the carrier of Polynom-Ring R; assume A: p is_associated_to q; then consider c being Element of Polynom-Ring R such that K2: q = p * c by GCD_1:def 1; reconsider r = c as Element of the carrier of Polynom-Ring R; consider d being Element of Polynom-Ring R such that K3: p = q * d by A,GCD_1:def 1; reconsider s = d as Element of the carrier of Polynom-Ring R; K4: q = p *' r by K2,POLYNOM3:def 10; K5: p = q *' s by K3,POLYNOM3:def 10; per cases; suppose p = 0_.(R); hence thesis by K4,POLYNOM3:34; end; suppose q = 0_.(R); hence thesis by K5,POLYNOM3:34; end; suppose A: p <> 0_.(R) & q <> 0_.(R); then A1: r <> 0_.(R) & s <> 0_.(R) by K4,K5,POLYNOM3:34; then A2: deg r is Element of NAT & deg s is Element of NAT by T8b; A3: deg q = deg p + deg r & deg p = deg q + deg s by A,A1,K4,K5,HURWITZ:23; then deg r + deg s = 0; then deg r = 0 & deg s = 0 by A2; hence thesis by A3; end; end; theorem np0: for R being domRing, p,q being monic Element of the carrier of Polynom-Ring R holds p is_associated_to q iff p = q proof let R be domRing, p,q be monic Element of the carrier of Polynom-Ring R; K1: LC p = 1.R & LC q = 1.R by RATFUNC1:def 7; now assume AS: p is_associated_to q; then consider c being Element of Polynom-Ring R such that K2: q = p * c by GCD_1:def 1; reconsider r = c as Element of the carrier of Polynom-Ring R; K3: q = p *' r by K2,POLYNOM3:def 10; r <> 0_.(R) by K3,POLYNOM3:34; then deg q = deg p + deg r by K3,HURWITZ:23 .= deg q + deg r by AS,np00; then r is constant; then consider a being Element of R such that K5: r = a|R by T11; X: deg p = deg q by AS,np00; r = a * 1_.(R) by K5,LX1; then q = a * (p *' 1_.(R)) by K3,poly2 .= a * p by poly1; then q.(len q-'1) = a * 1.R by X,K1,POLYNOM5:def 4 .= a; then r = 1_.(R) by K5,K1; hence p = q by K3,poly1; end; hence thesis; end; begin :: Canonical Homomorphism from R into R[X] definition let R be Ring; func canHom R -> Function of R, Polynom-Ring R means :defcanhom: for x being Element of R holds it.x = x|R; existence proof set B = Polynom-Ring R; defpred P[object,object] means ex a being Element of R st $1 = a & $2 = a|R; X: for x being object st x in the carrier of R ex y being object st y in the carrier of B & P[x,y] proof let x be object; assume x in the carrier of R; then reconsider a = x as Element of R; reconsider y = a|R as Element of B by POLYNOM3:def 10; take y; thus thesis; end; consider g being Function of the carrier of R,the carrier of B such that Z: for x being object st x in the carrier of R holds P[x,g.x] from FUNCT_2:sch 1(X); now let x be Element of R; consider a being Element of R such that H: x = a & g.x = a|R by Z; thus g.x = x|R by H; end; then consider f being Function of R,B such that Y: for x being Element of R holds f.x = x|R; take f; thus thesis by Y; end; uniqueness proof set B = Polynom-Ring R; let g1,g2 be Function of R,B such that A1: for a being Element of R holds g1.a = a|R and A2: for a being Element of R holds g2.a = a|R; A: dom g1 = the carrier of R by FUNCT_2:def 1 .= dom g2 by FUNCT_2:def 1; now let x be object; assume x in dom g1; then reconsider a = x as Element of R; thus g1.x = a|R by A1 .= g2.x by A2; end; hence thesis by A,FUNCT_1:2; end; end; registration let R be Ring; cluster canHom R -> additive multiplicative unity-preserving; coherence proof set f = canHom R; hereby let x,y be Element of R; f.x = x|R & f.y = y|R by defcanhom; hence f.x + f.y = (x|R) + (y|R) by POLYNOM3:def 10 .= (x + y)|R by T4a .= f.(x+y) by defcanhom; end; hereby let x,y be Element of R; f.x = x|R & f.y = y|R by defcanhom; hence f.x * f.y = (x|R) *' (y|R) by POLYNOM3:def 10 .= (x * y)|R by T4 .= f.(x*y) by defcanhom; end; thus f.1_R = (1.R)|R by defcanhom .= 1_.(R) .= 1_(Polynom-Ring R) by POLYNOM3:def 10; end; end; registration let R be Ring; cluster canHom R -> monomorphism; coherence proof set f = canHom R; A: f is linear by RINGCAT1:def 1; now let x1,x2 be object; assume AS: x1 in the carrier of R & x2 in the carrier of R & f.x1 = f.x2; then reconsider a = x1, b = x2 as Element of R; a|R = f.x2 by AS,defcanhom .= b|R by defcanhom; hence x1 = x2 by T9; end; then f is one-to-one by FUNCT_2:19; hence thesis by A; end; end; registration let R be Ring; cluster Polynom-Ring R -> R-homomorphic R-monomorphic; coherence proof A: canHom R is additive multiplicative unity-preserving monomorphism; hence Polynom-Ring R is R-homomorphic by RING_2:def 4; thus thesis by A,RING_3:def 3; end; end; theorem for R being Ring holds Char(Polynom-Ring R) = Char R by RING_3:88; registration let R be non degenerated Ring; cluster Polynom-Ring R -> infinite; coherence proof set PR = Polynom-Ring R; defpred P[Element of NAT,object] means $2 = rpoly($1,0.R); A0: for x be Element of NAT ex y being Element of the carrier of PR st P[x,y] proof let x be Element of NAT; take rpoly(x,0.R); thus thesis by POLYNOM3:def 10; end; consider f being Function of NAT,the carrier of PR such that A1: for x being Element of NAT holds P[x,f.x] from FUNCT_2:sch 3(A0); A2: dom f = NAT by FUNCT_2:def 1; now let x1,x2 be object; assume A3: x1 in NAT & x2 in NAT & f.x1 = f.x2; then reconsider n = x1, m = x2 as Element of NAT; rpoly(n,0.R) = f.m by A1,A3 .= rpoly(m,0.R) by A1; then n = deg(rpoly(m,0.R)) by HURWITZ:27 .= m by HURWITZ:27; hence x1 = x2; end; then f is one-to-one by FUNCT_2:19; then rng f is infinite by A2,CARD_1:59; hence thesis; end; end; registration cluster -> infinite for 0-characteristic Ring; coherence proof let R be 0-characteristic Ring; set f = canHom_Int R; dom f = the carrier of INT.Ring by FUNCT_2:def 1; then rng f is infinite by CARD_1:59; hence thesis; end; end; theorem for R being Ring st Char R = 0 holds R is infinite proof let R be Ring; assume Char R = 0; then R is 0-characteristic by RING_3:def 6; hence thesis; end; registration let n be non trivial Nat; cluster Polynom-Ring(Z/n) -> infinite; coherence; end; theorem for n being non trivial Nat holds Char Polynom-Ring(Z/n) <> 0; registration let n be non trivial Nat; cluster n-characteristic infinite for Ring; existence proof take Polynom-Ring(Z/n); thus thesis; end; end; begin :: Units and Irreducible Polynomials lemr: for R being domRing holds Polynom-Ring R is non almost_left_invertible proof let R be domRing; set PR = Polynom-Ring R; reconsider p = rpoly(2,0.R) as Element of the carrier of PR by POLYNOM3:def 10; A3: p <> 0.PR by POLYNOM3:def 10; now assume ex q being Element of PR st q*p = 1.PR; then consider q being Element of PR such that A1: q*p = 1.PR; A9: q <> 0.PR by A1; reconsider q as Element of the carrier of PR; A4: q <> 0_.(R) by A9,POLYNOM3:def 10; then A5: deg q is Element of NAT by T8b; q *' p = 1.PR by A1,POLYNOM3:def 10 .= 1_.(R) by POLYNOM3:def 10; then A2: deg q + deg p = deg(1_.(R)) by A4,HURWITZ:23; A8: len(1_.(R)) = 1 by POLYNOM4:4; deg p = 2 by HURWITZ:27; hence contradiction by A5,A8,A2; end; then not p is left_invertible; hence PR is non almost_left_invertible by A3; end; registration cluster non almost_left_invertible for domRing; existence proof take Polynom-Ring the Field; thus thesis by lemr; end; end; lemf: for R being domRing holds R is Field iff for a being NonUnit of R holds a = 0.R proof let R be domRing; A: now assume R is Field; then B: R is almost_left_invertible; let a be NonUnit of R; now assume a <> 0.R; then consider b being Element of R such that C: b * a = 1.R by B,ALGSTR_0:def 27; a divides 1.R by C; hence contradiction by GCD_1:def 2; end; hence a = 0.R; end; now assume B: for a being NonUnit of R holds a = 0.R; now let a be Element of R; assume a <> 0.R; then a is Unit of R by B; then a divides 1.R by GCD_1:def 2; then consider b being Element of R such that C: a * b = 1.R; thus a is left_invertible by C; end; then R is almost_left_invertible; hence R is Field; end; hence thesis by A; end; registration let R be non almost_left_invertible domRing; cluster non zero for NonUnit of R; existence proof consider a being NonUnit of R such that H: a <> 0.R by lemf; a is non zero by H; hence thesis; end; end; registration cluster INT.Ring -> non almost_left_invertible; coherence proof set R = INT.Ring; set a = 1.R + 1.R; now assume ex y being Element of R st y*a = 1.R; then consider y being Element of R such that A1: y*a = 1.R; reconsider i = y as Integer; consider k being Nat such that A2: k = 1 * 2" or -k = 1 * 2" by A1,INT_1:def 1; thus contradiction by A2,NAT_1:14; end; then not a is left_invertible; hence R is non almost_left_invertible; end; end; registration let R be domRing; cluster Polynom-Ring R -> non almost_left_invertible; coherence by lemr; end; theorem for R being domRing holds R is Field iff for a being NonUnit of R holds a = 0.R by lemf; theorem Th90: for R being domRing, a being Element of R holds a|R is Unit of Polynom-Ring R iff a is Unit of R proof let L be domRing, a be Element of L; set R = Polynom-Ring L; H1: 1.R = 1_.(L) by POLYNOM3:def 10; reconsider p = a|L as Element of Polynom-Ring L by POLYNOM3:def 10; A: now assume AS: p is Unit of R; then (a|L) divides 1_.(L) by H1,GCD_1:def 2; then consider q being Polynomial of L such that H3: (a|L) *' q = 1_.(L) by T2; reconsider qq = q as Element of R by POLYNOM3:def 10; p <> 0.R by AS; then H4: a|L <> 0_.(L) by POLYNOM3:def 10; q <> 0_.(L) by H3,POLYNOM3:34; then H6: deg(a|L) + deg(q) = deg(1_.(L)) by H3,H4,HURWITZ:23 .= 1 - 1 by POLYNOM4:4; deg(a|L) is Element of NAT by H4,T8b; then qq is constant by H6; then consider b being Element of L such that H5: qq = b|L by T11; (a*b)|L = (1.L)|L by H3,H5,T4; then a divides 1.L by T9; hence a is Unit of L by GCD_1:def 2; end; now assume a is Unit of L; then a divides 1.L by GCD_1:def 2; then consider b being Element of L such that H3: a * b = 1.L; (a|L) *' (b|L) = (1.L)|L by T4,H3 .= 1_.(L); then (a|L) divides 1_.(L) by T2; hence p is Unit of R by H1,GCD_1:def 2; end; hence thesis by A; end; theorem T88: for F being domRing, p being Element of the carrier of Polynom-Ring F holds p is Unit of Polynom-Ring F implies deg p = 0 proof let L be domRing; let p be Element of the carrier of Polynom-Ring L; set R = Polynom-Ring L; H: 1.R = 1_.(L) by POLYNOM3:def 10; assume AS: p is Unit of R; then H0: p <> 0.R; then H1: p <> 0_.(L) by POLYNOM3:def 10; reconsider degp = deg p as Element of NAT by H0,T8a; p divides 1_.(L) by AS,H,GCD_1:def 2; then consider t being Polynomial of L such that H3: p *' t = 1_.(L) by T2; reconsider t as Element of the carrier of R by POLYNOM3:def 10; H5: t <> 0_.(L) by POLYNOM3:34,H3; then t <> 0.R by POLYNOM3:def 10; then reconsider degt = deg t as Element of NAT by T8a; degt + degp = deg(1_.(L)) by H1,H3,H5,HURWITZ:23 .= 1 - 1 by POLYNOM4:4; hence deg p = 0; end; theorem T8: for F being Field, p being Element of the carrier of Polynom-Ring F holds p is Unit of Polynom-Ring F iff deg p = 0 proof let L be Field; let p be Element of the carrier of Polynom-Ring L; set R = Polynom-Ring L; H: 1.R = 1_.(L) by POLYNOM3:def 10; A: now assume AS: p is Unit of R; then H0: p <> 0.R; then H1: p <> 0_.(L) by POLYNOM3:def 10; reconsider degp = deg p as Element of NAT by H0,T8a; p divides 1_.(L) by AS,H,GCD_1:def 2; then consider t being Polynomial of L such that H3: p *' t = 1_.(L) by T2; reconsider t as Element of the carrier of R by POLYNOM3:def 10; H5: t <> 0_.(L) by POLYNOM3:34,H3; then t <> 0.R by POLYNOM3:def 10; then reconsider degt = deg t as Element of NAT by T8a; degt + degp = deg(1_.(L)) by H1,H3,H5,HURWITZ:23 .= 1 - 1 by POLYNOM4:4; hence deg p = 0; end; now assume AS: deg p = 0; then AS1: p <> 0_.(L) by HURWITZ:20; p <> 0.R by AS1,POLYNOM3:def 10; then reconsider degp = deg p as Nat by T8a; p is constant by AS; then consider a being Element of L such that X: p = a|L by T11; H3: a <> 0.L by X,AS,HURWITZ:20,UPROOTS:def 5; set t = (a")|L; t *' p = (a" * a) | L by X,T4 .= 1_.(L) by H3,VECTSP_1:def 10; then p divides 1_.(L) by T2; hence p is Unit of R by H,GCD_1:def 2; end; hence thesis by A; end; theorem for R being domRing, p being Element of the carrier of Polynom-Ring R holds p is Unit of Polynom-Ring R implies p is non zero constant proof let F be domRing, p be Element of the carrier of Polynom-Ring F; p is Unit of Polynom-Ring F implies deg p = 0 by T88; hence thesis by LX; end; theorem for F being Field, p being Element of the carrier of Polynom-Ring F holds p is Unit of Polynom-Ring F iff p is non zero constant proof let F be Field, p be Element of the carrier of Polynom-Ring F; p is Unit of Polynom-Ring F iff deg p = 0 by T8; hence thesis by LX; end; registration let R be domRing; cluster non constant -> non zero non unital for Element of Polynom-Ring R; coherence proof let a be Element of Polynom-Ring R; reconsider p = a as Element of the carrier of Polynom-Ring R; assume AS: a is non constant; then A: deg p > 0; now assume a = 0.(Polynom-Ring R); then p = 0_.(R) by POLYNOM3:def 10; then len p = 0 by POLYNOM4:3; hence contradiction by A; end; hence a is non zero; thus a is non unital by AS,T88; end; end; registration let F be domRing; cluster non constant -> non zero non unital for Element of the carrier of Polynom-Ring F; coherence proof let a be Element of the carrier of Polynom-Ring F; assume AS: a is non constant; now assume a = 0_.(F); then len a = 0 by POLYNOM4:3; hence contradiction by AS; end; hence a is non zero by UPROOTS:def 5; thus a is non unital by AS; end; end; registration let F be Field; cluster non zero constant -> unital for Element of Polynom-Ring F; coherence proof let p be Element of Polynom-Ring F; assume AS: p is non zero constant; then A: p <> 0_.(F) by POLYNOM3:def 10; reconsider pp = p as Element of the carrier of Polynom-Ring F; pp is non zero by A,UPROOTS:def 5; then deg pp = 0 by AS; hence p is unital by T8; end; cluster unital -> non zero constant for Element of Polynom-Ring F; coherence; end; registration let F be Field; cluster non zero constant -> unital for Element of the carrier of Polynom-Ring F; coherence proof let p be Element of the carrier of Polynom-Ring F; assume p is non zero constant; then deg p = 0; hence p is unital by T8; end; cluster unital -> non zero constant for Element of the carrier of Polynom-Ring F; coherence proof let a be Element of the carrier of Polynom-Ring F; reconsider p = a as Element of Polynom-Ring F; assume AS: a is unital; then deg a = 0 by T88; then a <> 0_.(F) by HURWITZ:20; hence a is non zero by UPROOTS:def 5; thus thesis by AS; end; end; theorem T88a: for R being domRing for p being Element of the carrier of Polynom-Ring R holds (ex q being Element of the carrier of Polynom-Ring R st q divides p & 1 <= deg q & deg q < deg p) implies p is reducible proof let R be domRing, p be Element of the carrier of Polynom-Ring R; set K = Polynom-Ring R; reconsider pp = p as Polynomial of R; assume ex q being Element of the carrier of Polynom-Ring R st q divides p & 1 <= deg q & deg q < deg p; then consider q being Element of the carrier of Polynom-Ring R such that A0: q divides p & 1 <= deg q & deg q < deg p; A1: not q is Unit of K by T88,A0; now assume q is_associated_to p; then consider r being Element of K such that A2: r is unital & q * r = p by GCD_1:18; reconsider rr = r as Element of the carrier of K; A5: p = q *' rr by A2,POLYNOM3:def 10; then A4: r <> 0_.(R) by HURWITZ:20,A0,POLYNOM3:34; q <> 0_.(R) by A5,A0,POLYNOM3:34; then deg p = deg q + deg rr by A4,A5,HURWITZ:23 .= deg q + 0 by A2,T88; hence contradiction by A0; end; hence p is reducible by A0,A1,RING_2:def 9; end; theorem T88b: for F being Field for p being Element of the carrier of Polynom-Ring F holds p is reducible iff (p = 0_.(F) or p is Unit of Polynom-Ring F or ex q being Element of the carrier of Polynom-Ring F st q divides p & 1 <= deg q & deg q < deg p) proof let R be Field, p be Element of the carrier of Polynom-Ring R; set K = Polynom-Ring R; reconsider pp = p as Polynomial of R; A: now assume p is reducible; then AS: p = 0.K or p is Unit of K or ex a being Element of K st a divides p & not(a is Unit of K) & not(a is_associated_to p) by RING_2:def 9; thus p = 0_.(R) or p is Unit of Polynom-Ring R or ex q being Element of the carrier of Polynom-Ring R st q divides p & 1 <= deg q & deg q < deg p proof assume A0: not(p = 0_.(R)) & not(p is Unit of K); then consider a being Element of K such that A1: a divides p & not(a is Unit of K) & not(a is_associated_to p) by AS,POLYNOM3:def 10; reconsider q = a as Polynomial of R by POLYNOM3:def 10; q divides pp by A1; then consider r being Polynomial of R such that A2: pp = q *' r by T2; reconsider rr = r as Element of K by POLYNOM3:def 10; A10: p = a * rr by A2,POLYNOM3:def 10; A5: q <> 0_.(R) by A0,A2,POLYNOM3:34; A6: r <> 0_.(R) by A0,A2,POLYNOM3:34; then A9: deg p = (deg q) + (deg r) by A2,A5,HURWITZ:23; A11: deg q is Element of NAT & deg r is Element of NAT by A5,A6,T8b; then A7: deg q <= deg p by A9,NAT_1:11; A3: now assume deg q = deg p; then rr is Unit of K by A9,T8; hence contradiction by A1,A10,GCD_1:18; end; thus ex b being Element of the carrier of K st b divides p & 1 <= deg b & deg b < deg p proof reconsider qq = q as Element of the carrier of K; take qq; thus qq divides p by A1; thus 1 <= deg qq by A1,A11,T8,NAT_1:14; thus deg qq < deg p by A3,A7,XXREAL_0:1; end; end; end; now assume AS: p = 0_.(R) or p is Unit of Polynom-Ring R or ex q being Element of the carrier of Polynom-Ring R st q divides p & 1 <= deg q & deg q < deg p; per cases by AS; suppose p = 0_.(R); then p = 0.K by POLYNOM3:def 10; hence p is reducible; end; suppose p is Unit of Polynom-Ring R; hence p is reducible; end; suppose ex q being Element of the carrier of Polynom-Ring R st q divides p & 1 <= deg q & deg q < deg p; hence p is reducible by T88a; end; end; hence thesis by A; end; theorem thirr0: for R being domRing, p being monic Element of the carrier of Polynom-Ring R st deg p = 1 holds p is irreducible proof let R be domRing, p be monic Element of the carrier of Polynom-Ring R; set K = Polynom-Ring R; reconsider x = p as Element of K; assume AS: deg p = 1; then len p -' 1 = 1 + 1 -' 1 .= 1 by NAT_D:34; then LC p = p.1; then E: p.1 = 1.R by RATFUNC1:def 7; p <> 0_.(R); then A: x <> 0.K by POLYNOM3:def 10; B: not x is Unit of K by AS,T88; now let a be Element of K; assume a divides x; then consider b being Element of K such that H1: a * b = x; reconsider q = a, r = b as Element of the carrier of K; q *' r = p by H1,POLYNOM3:def 10; then H2: q <> 0_.(R) & r <> 0_.(R) by POLYNOM3:34; then H4: deg q + deg r = deg(q *' r) by HURWITZ:23 .= 1 by AS,H1,POLYNOM3:def 10; per cases; suppose deg q = 0; then q is constant; then consider u being Element of R such that C1: q = u|R by T11; q = u * 1_.(R) by LX1,C1; then q *' r = u * ((1_.(R)) *' r) by poly2 .= u * r by poly1; then u * (r.1) = (q *'r).1 by POLYNOM5:def 4 .= 1.R by H1,POLYNOM3:def 10,E; then u divides 1.R; then u is Unit of R by GCD_1:def 2; hence a is Unit of K or a is_associated_to x by Th90,C1; end; suppose deg q <> 0; then deg q > 0 by H2,T8b; then deg q + deg r > 0 + deg r by XREAL_1:6; then r is constant by H4,NAT_1:14; then consider u being Element of R such that C1: r = u|R by T11; C3: r = u * 1_.(R) by LX1,C1; q *' r = u * ((1_.(R)) *' q) by C3,poly2 .= u * q by poly1; then u * (q.1) = (q *'r).1 by POLYNOM5:def 4 .= 1.R by H1,POLYNOM3:def 10,E; then u divides 1.R; then u is Unit of R by GCD_1:def 2; then r is Unit of K by Th90,C1; hence a is Unit of K or a is_associated_to x by H1,GCD_1:18; end; end; hence thesis by A,B,RING_2:def 9; end; theorem ex p being non monic Element of the carrier of Polynom-Ring(INT.Ring) st deg p = 1 & p is reducible proof set R = INT.Ring; set K = Polynom-Ring R; set a = 1.R + 1.R; set p = (a|R) *' rpoly(1,0.R); a <> 0.R; then reconsider a as non zero Element of R by STRUCT_0:def 12; reconsider q = a|R as Element of the carrier of K by POLYNOM3:def 10; q is constant by RATFUNC1:def 2; then reconsider q as non zero constant Element of the carrier of K; reconsider r = rpoly(1,0.R) as Element of the carrier of K by POLYNOM3:def 10; A1: p = (a * 1_.(R)) *' rpoly(1,0.R) by LX1 .= a * ((1_.(R)) *' rpoly(1,0.R)) by poly2 .= a * rpoly(1,0.R) by poly1; A2: deg p = deg q + deg rpoly(1,0.R) by HURWITZ:23 .= 0 + deg rpoly(1,0.R) by LX .= 1 by HURWITZ:27; then p.(len p -' 1) = (a * rpoly(1,0.R)).(2-1) by A1,XREAL_1:233 .= a * (rpoly(1,0.R)).1 by POLYNOM5:def 4 .= a * 1.R by HURWITZ:25 .= a; then LC p = a; then reconsider pp = p as non monic Element of the carrier of K by RATFUNC1:def 7,POLYNOM3:def 10; take pp; thus deg pp = 1 by A2; B0: p = q * r by POLYNOM3:def 10; B1: q divides pp by B0,GCD_1:def 1; B4: now assume q is Unit of K; then a is Unit of R by Th90; then a divides 1.R by GCD_1:def 2; then consider c being Element of the carrier of R such that C1: a * c = 1.R; thus contradiction by C1,INT_1:9; end; now assume q is_associated_to pp; then consider c being Element of the carrier of K such that C1: c is unital & q * c = p by GCD_1:18; C2: (a|R) *' c = p by C1,POLYNOM3:def 10; deg c = 0 by C1,T88; then c <> 0_.(R) by HURWITZ:20; then 1 = deg q + deg c by HURWITZ:23,C2,A2 .= 0 + deg c by LX; hence contradiction by C1,T88; end; hence pp is reducible by B1,B4,RING_2:def 9; end; theorem thirr: for F being Field, p being Element of the carrier of Polynom-Ring F st deg p = 1 holds p is irreducible proof let R be Field, p be Element of the carrier of Polynom-Ring R; set K = Polynom-Ring R; reconsider x = p as Element of K; assume AS: deg p = 1; then p <> 0_.(R) by HURWITZ:20; then A: x <> 0.K by POLYNOM3:def 10; B: not x is Unit of K by AS,T88; now let a be Element of K; assume a divides x; then consider b being Element of K such that H1: a * b = x; reconsider q = a, r = b as Element of the carrier of K; q *' r = p by H1,POLYNOM3:def 10; then H2: q <> 0_.(R) & r <> 0_.(R) by AS,HURWITZ:20,POLYNOM3:34; then H4: deg q + deg r = deg(q *' r) by HURWITZ:23 .= 1 by AS,H1,POLYNOM3:def 10; per cases; suppose C0: deg q = 0; then q is constant; then consider u being Element of R such that C1: q = u|R by T11; u is non zero by C1,C0,T11a; hence a is Unit of K or a is_associated_to x by Th90,C1; end; suppose deg q <> 0; then deg q > 0 by H2,T8b; then deg q + deg r > 0 + deg r by XREAL_1:6; then r is constant by H4,NAT_1:14; then consider u being Element of R such that C1: r = u|R by T11; u is non zero by C1,T6,H2; then r is Unit of K by Th90,C1; hence a is Unit of K or a is_associated_to x by H1,GCD_1:18; end; end; hence thesis by A,B,RING_2:def 9; end; theorem thirr1: for F being algebraic-closed Field, p being Element of the carrier of Polynom-Ring F holds p is irreducible iff deg p = 1 proof let R be algebraic-closed Field, p be Element of the carrier of Polynom-Ring R; set K = Polynom-Ring R; now assume AS: p is irreducible; then p is non constant; then (len p -1) + 1 > 0 + 1 by XREAL_1:6; then consider x being Element of R such that A: x is_a_root_of p by POLYNOM5:def 8,POLYNOM5:def 9; consider q being Polynomial of R such that B: p = rpoly(1,x) *' q by A,HURWITZ:33; reconsider y = q, z = rpoly(1,x) as Element of Polynom-Ring R by POLYNOM3:def 10; p = z * y by B,POLYNOM3:def 10; then z divides p; then C: z is Unit of K or z is_associated_to p by AS,RING_2:def 9; z is non constant by HURWITZ:27; then consider e being Element of K such that D: e is unital & z * e = p by C,GCD_1:18; reconsider u = e as Element of the carrier of K; F: deg u = 0 by D,T88; rpoly(1,x) *' u = p by D,POLYNOM3:def 10; hence deg p = deg(rpoly(1,x)) + deg u by D,HURWITZ:23 .= 1 by F,HURWITZ:27; end; hence thesis by thirr; end; theorem for F being Field holds F is algebraic-closed iff for p being monic Element of the carrier of Polynom-Ring F holds p is irreducible iff deg p = 1 proof let R be Field; now assume AS: for p being monic Element of the carrier of Polynom-Ring R holds p is irreducible iff deg p = 1; now let p be Polynomial of R; assume A: len p > 1; then A1: p <> 0_.(R) by POLYNOM4:3; A4: len p - 1 > 1 - 1 by A,XREAL_1:9; then deg p is Element of NAT by INT_1:3; then A3: deg p >= 1 by NAT_1:14,A4; defpred P[Nat] means for p being Polynomial of R st deg p = $1 holds p is with_roots; II: for k being Nat st k >= 1 & (for n being Nat st n >= 1 & n < k holds P[n]) holds P[k] proof let k be Nat; assume IAS: k >= 1 & for n being Nat st n >= 1 & n < k holds P[n]; per cases by IAS,XXREAL_0:1; suppose IA1: k = 1; thus P[k] proof now let p be Polynomial of R; assume deg p = 1; then consider x,z being Element of R such that I1: x <> 0.R & p = x * rpoly(1,z) by HURWITZ:28; eval(p,z) = x * eval(rpoly(1,z),z) by I1,POLYNOM5:30 .= x * (z - z) by HURWITZ:29 .= x *0.R by RLVECT_1:15; hence p is with_roots by POLYNOM5:def 8,POLYNOM5:def 7; end; hence thesis by IA1; end; end; suppose IA1: k > 1; thus P[k] proof now let p be Polynomial of R; reconsider pp = p as Element of Polynom-Ring R by POLYNOM3:def 10; set q = NormPolynomial(p); reconsider qq = q as Element of Polynom-Ring R by POLYNOM3:def 10; assume K: deg p = k; then len p <> 0; then I3: deg q > 1 by K,IA1,POLYNOM5:57; p <> 0_.(R) by K,HURWITZ:20; then p is non zero by UPROOTS:def 5; then I4: qq is reducible by AS,I3; I5: pp <> 0_.(R) by K,HURWITZ:20; not p is Unit of Polynom-Ring R by T8,K,IA1; then consider r being Element of the carrier of Polynom-Ring R such that I6: r divides p & 1 <= deg r & deg r < deg p by I4,I5,T88b,thirr2; r <> 0_.(R) by I6,HURWITZ:20; then deg r is Element of NAT by T8b; then consider x being Element of R such that I8: x is_a_root_of r by K,I6,IAS,POLYNOM5:def 8; reconsider rr=r,ppp=p as Element of Polynom-Ring R by POLYNOM3:def 10; rr divides ppp by I6; then consider u being Element of the carrier of Polynom-Ring R such that I10: ppp = rr * u; p = r *'u by I10,POLYNOM3:def 10; then eval(p,x) = eval(r,x) * eval(u,x) by POLYNOM4:24 .= 0.R * eval(u,x) by I8,POLYNOM5:def 7 .= 0.R; hence p is with_roots by POLYNOM5:def 8,POLYNOM5:def 7; end; hence thesis; end; end; end; I: for k being Nat st 1 <= k holds P[k] from NAT_1:sch 9(II); deg p is Element of NAT by A1,T8b; then consider n being Nat such that H: n >= 1 & deg p = n by A3; thus p is with_roots by H,I; end; hence R is algebraic-closed by POLYNOM5:def 9; end; hence thesis by thirr1; end; registration let R be domRing; cluster irreducible for Element of Polynom-Ring R; existence proof set K = Polynom-Ring R; reconsider x = rpoly(1,0.R) as Element of K by POLYNOM3:def 10; deg rpoly(1,0.R) = 1 by HURWITZ:27; then x is irreducible by thirr0; hence thesis; end; end; registration let R be domRing; cluster irreducible for Element of the carrier of Polynom-Ring R; existence proof set K = Polynom-Ring R; reconsider x = rpoly(1,0.R) as Element of the carrier of K by POLYNOM3:def 10; deg rpoly(1,0.R) = 1 by HURWITZ:27; then x is irreducible by thirr0; hence thesis; end; end; registration let R be Ring; cluster reducible for Element of Polynom-Ring R; existence proof take p = 0.(Polynom-Ring R); thus thesis; end; end; registration let R be Ring; cluster reducible for Element of the carrier of Polynom-Ring R; existence proof take p = 0_.(R); reconsider q = p as Element of Polynom-Ring R by POLYNOM3:def 10; q = 0.(Polynom-Ring R) by POLYNOM3:def 10; hence thesis; end; end; registration let R be domRing; cluster IRR(Polynom-Ring R) -> non empty; coherence proof now let p be irreducible Element of Polynom-Ring R; p in {x where x is Element of Polynom-Ring R : x is irreducible}; hence p in IRR(Polynom-Ring R) by RING_2:def 10; end; hence thesis; end; end; registration let F be Field; cluster constant -> reducible for Element of Polynom-Ring F; coherence; end; registration let F be Field; cluster constant -> reducible for Element of the carrier of Polynom-Ring F; coherence; end; registration let F be Field; cluster irreducible -> non constant for Element of Polynom-Ring F; coherence; end; registration let F be Field; cluster irreducible -> non constant for Element of the carrier of Polynom-Ring F; coherence; end; begin :: The Field F[X]/
registration let F be Field, p be Element of the carrier of Polynom-Ring F; cluster (Polynom-Ring F)/({p}-Ideal) -> Abelian add-associative right_zeroed right_complementable commutative associative well-unital distributive; coherence; end; registration let F be Field, p be irreducible Element of the carrier of Polynom-Ring F; cluster (Polynom-Ring F)/({p}-Ideal) -> non degenerated almost_left_invertible; coherence by RING_2:26,RING_1:21; end; definition let F be Field, p be Polynomial of F; func poly_mult_mod p -> BinOp of Polynom-Ring F means :defpmm: for r,q being Polynomial of F holds it.(r,q) = (r *' q) mod p; existence proof set B = Polynom-Ring F; set D = the carrier of B; defpred P[object,object,object] means ex r,q being Element of D st $1 = r & $2 = q & $3 = (r *' q) mod p; I: now let x,y be object; assume x in D & y in D; then reconsider xx=x,yy=y as Element of D; reconsider r=xx,q=yy as Polynomial of F; thus ex z being object st z in D & P[x,y,z] proof take s = (r *' q) mod p; thus s in D by POLYNOM3:def 10; take xx,yy; thus thesis; end; end; consider f being Function of [:D,D:],D such that H: for x,y being object st x in D & y in D holds P[x,y,f.(x,y)] from BINOP_1:sch 1(I); take f; now let r,q be Polynomial of F; r in D & q in D by POLYNOM3:def 10; then P[r,q,f.(r,q)] by H; then consider rr,qq being Element of D such that K: rr = r & qq = q & f.(rr,qq) = (rr *' qq) mod p; thus f.(r,q) = (r *' q) mod p by K; end; hence thesis; end; uniqueness proof set B = Polynom-Ring F; let g1,g2 be BinOp of B such that A1: for r,q being Polynomial of F holds g1.(r,q) = (r *' q) mod p and A2: for r,q being Polynomial of F holds g2.(r,q) = (r *' q) mod p; A: dom g1 = [:the carrier of B,the carrier of B:] by FUNCT_2:def 1 .= dom g2 by FUNCT_2:def 1; now let x be object; assume x in dom g1; then consider r,q being object such that H: r in the carrier of B & q in the carrier of B & x = [r,q] by ZFMISC_1:def 2; reconsider r,q as Polynomial of F by H,POLYNOM3:def 10; thus g1.x = g1.(r,q) by H .= (r *' q) mod p by A1 .= g2.(r,q) by A2 .= g2.x by H; end; hence thesis by A,FUNCT_1:2; end; end; pr1: for F be Field, p be Element of the carrier of Polynom-Ring F holds {q where q is Polynomial of F : deg q < deg p} is Preserv of (the addF of Polynom-Ring F) proof let F be Field, p be Element of the carrier of Polynom-Ring F; set C = {q where q is Polynomial of F : deg q < deg p}; now let x be set; assume x in C; then ex r being Polynomial of F st x = r & deg r < deg p; hence x in the carrier of Polynom-Ring F by POLYNOM3:def 10; end; then C c= the carrier of Polynom-Ring F; then reconsider C as Subset of the carrier of Polynom-Ring F; set A = the addF of Polynom-Ring F; now let x be set; assume x in [:C,C:]; then consider a,b being object such that A2: a in C and A3: b in C and A4: x = [a,b] by ZFMISC_1:def 2; consider u being Polynomial of F such that A5: a = u & deg u < deg p by A2; consider v being Polynomial of F such that A6: b = v & deg v < deg p by A3; reconsider a,b as Element of Polynom-Ring F by A5,A6,POLYNOM3:def 10; A7: deg(u+v) <= max(deg(u),deg(v)) by HURWITZ:22; max(deg(u),deg(v)) < deg p by A5,A6,XXREAL_0:29; then A8: deg(u+v) < deg p by A7,XXREAL_0:2; A.x = a + b by A4 .= u + v by A5,A6,POLYNOM3:def 10; hence A.x in C by A8; end; hence thesis by REALSET1:def 1; end; pr2: for F be Field, p be non constant Element of the carrier of Polynom-Ring F holds {q where q is Polynomial of F : deg q < deg p} is Preserv of (poly_mult_mod p) proof let F be Field, p be non constant Element of the carrier of Polynom-Ring F; set C = {q where q is Polynomial of F : deg q < deg p}; now let x be set; assume x in C; then ex r being Polynomial of F st x = r & deg r < deg p; hence x in the carrier of Polynom-Ring F by POLYNOM3:def 10; end; then C c= the carrier of Polynom-Ring F; then reconsider C as Subset of the carrier of Polynom-Ring F; set A = poly_mult_mod p; now let x be set; assume x in [:C,C:]; then consider a,b being object such that A2: a in C and A3: b in C and A4: x = [a,b] by ZFMISC_1:def 2; consider u being Polynomial of F such that A5: a = u & deg u < deg p by A2; consider v being Polynomial of F such that A6: b = v & deg v < deg p by A3; reconsider a,b as Element of Polynom-Ring F by A5,A6,POLYNOM3:def 10; A8: deg((u *' v) mod p) < deg p by RING_2:29; A.x = (poly_mult_mod p).(u,v) by A5,A6,A4 .= (u *' v) mod p by defpmm; hence A.x in C by A8; end; hence thesis by REALSET1:def 1; end; pr3: for F be Field, p be non constant Element of the carrier of Polynom-Ring F holds 1_.(F) in {q where q is Polynomial of F : deg q < deg p} proof let F be Field, p be non constant Element of the carrier of Polynom-Ring F; A: deg p > 0 by defconst; len 1_.(F) = 1 by POLYNOM4:4; then deg 1_.(F) = 0; hence thesis by A; end; pr4: for F be Field, p be non constant Element of the carrier of Polynom-Ring F holds 0_.(F) in {q where q is Polynomial of F : deg q < deg p} proof let F be Field, p be non constant Element of the carrier of Polynom-Ring F; deg 0_.(F) = -1 by HURWITZ:20; hence thesis; end; definition let F be Field, p be non constant Element of the carrier of Polynom-Ring F; func Polynom-Ring(p) -> strict doubleLoopStr means :defprfp: the carrier of it = {q where q is Polynomial of F : deg q < deg p} & the addF of it = (the addF of Polynom-Ring F)||(the carrier of it) & the multF of it = (poly_mult_mod p)||(the carrier of it) & the OneF of it = 1_.(F) & the ZeroF of it = 0_.(F); existence proof set B = Polynom-Ring F; set C = {q where q is Polynomial of F : deg q < deg p}; set A = the addF of B; set M = poly_mult_mod p; reconsider C1 = C as Preserv of A by pr1; reconsider ad = A||C1 as BinOp of C; reconsider C2 = C as Preserv of M by pr2; reconsider mu = M||C2 as BinOp of C; reconsider O = 1_.(F) as Element of C by pr3; reconsider Z = 0_.(F) as Element of C by pr4; take doubleLoopStr(#C,ad,mu,O,Z#); thus thesis; end; uniqueness; end; registration let F be Field, p be non constant Element of the carrier of Polynom-Ring F; cluster Polynom-Ring(p) -> non degenerated; coherence proof set P = Polynom-Ring(p); 1.P = 1_.(F) by defprfp; hence 0.P <> 1.P by defprfp; end; end; registration let F be Field, p be non constant Element of the carrier of Polynom-Ring F; cluster Polynom-Ring(p) -> Abelian add-associative right_zeroed right_complementable; coherence proof set P = Polynom-Ring(p); set C = {q where q is Polynomial of F : deg q < deg p}; H0: C = the carrier of P by defprfp; H1: 0.P = 0_.(F) by defprfp; now let x,y be Element of P; x in the carrier of P; then x in C by defprfp; then consider q being Polynomial of F such that A1: x = q & deg q < deg p; y in the carrier of P; then y in C by defprfp; then consider r being Polynomial of F such that A2: y = r & deg r < deg p; reconsider q,r as Element of Polynom-Ring F by POLYNOM3:def 10; A3: [x,y] in [:C,C:] & [y,x] in [:C,C:] by H0,ZFMISC_1:def 2; thus x + y = ((the addF of Polynom-Ring F)||C).(x,y) by H0,defprfp .= q + r by A1,A2,A3,FUNCT_1:49 .= (the addF of Polynom-Ring F).(y,x) by A1,A2,ALGSTR_0:def 1 .= ((the addF of Polynom-Ring F)||C).(y,x) by A3,FUNCT_1:49 .= y + x by H0,defprfp; end; hence P is Abelian by RLVECT_1:def 2; now let x,y,z be Element of P; x in the carrier of P; then x in C by defprfp; then consider q being Polynomial of F such that A1: x = q & deg q < deg p; y in the carrier of P; then y in C by defprfp; then consider r being Polynomial of F such that A2: y = r & deg r < deg p; z in the carrier of P; then z in C by defprfp; then consider u being Polynomial of F such that A3: z = u & deg u < deg p; A3a: [x,y] in [:C,C:] & [y,z] in [:C,C:] by H0,ZFMISC_1:def 2; A3b: [x+y,z] in [:C,C:] & [x,y+z] in [:C,C:] by H0,ZFMISC_1:def 2; reconsider q,r,u as Element of Polynom-Ring F by POLYNOM3:def 10; A4: x + y = ((the addF of Polynom-Ring F)||C).(x,y) by H0,defprfp .= q + r by A1,A2,A3a,FUNCT_1:49; A5: y + z = ((the addF of Polynom-Ring F)||C).(y,z) by H0,defprfp .= r + u by A3,A2,A3a,FUNCT_1:49; A6: (x + y) + z = ((the addF of Polynom-Ring F)||C).(x+y,z) by H0,defprfp .= (q + r) + u by A3,A4,A3b,FUNCT_1:49 .= q + (r + u) by RLVECT_1:def 3; thus x + (y + z) = ((the addF of Polynom-Ring F)||C).(x,y+z) by H0,defprfp .= (x + y) + z by A6,A5,A1,A3b,FUNCT_1:49; end; hence P is add-associative by RLVECT_1:def 3; now let x be Element of P; x in the carrier of P; then x in C by defprfp; then consider q being Polynomial of F such that A1: x = q & deg q < deg p; reconsider q1 = q as Element of Polynom-Ring F by POLYNOM3:def 10; reconsider r = 0_.(F) as Element of Polynom-Ring F by POLYNOM3:def 10; A3: [x,0.P] in [:C,C:] by H0,ZFMISC_1:def 2; thus x + 0.P = ((the addF of Polynom-Ring F)||C).(x,0.P) by H0,defprfp .= (the addF of Polynom-Ring F).(x,0.P) by A3,FUNCT_1:49 .= q1 + r by defprfp,A1 .= q + 0_.(F) by POLYNOM3:def 10 .= x by A1,POLYNOM3:28; end; hence P is right_zeroed by RLVECT_1:def 4; now let x be Element of P; x in the carrier of P; then x in C by defprfp; then consider q being Polynomial of F such that A1: x = q & deg q < deg p; reconsider q1 = q as Element of Polynom-Ring F by POLYNOM3:def 10; reconsider r = -q as Element of Polynom-Ring F by POLYNOM3:def 10; deg(-q) = deg q by POLYNOM4:8; then -q in C by A1; then reconsider y = -q as Element of P by defprfp; A3: [x,y] in [:C,C:] by H0,ZFMISC_1:def 2; x + y = ((the addF of Polynom-Ring F)||C).(x,y) by H0,defprfp .= q1 + r by A1,A3,FUNCT_1:49 .= q - q by POLYNOM3:def 10 .= 0_.(F) by POLYNOM3:29; hence x is right_complementable by H1; end; hence P is right_complementable; end; end; registration let F be Field, p be non constant Element of the carrier of Polynom-Ring F; cluster Polynom-Ring(p) -> associative well-unital distributive; coherence proof set P = Polynom-Ring(p); set C = {q where q is Polynomial of F : deg q < deg p}; H0: C = the carrier of P by defprfp; H2: 1.P = 1_.(F) by defprfp; reconsider p1 = p as Polynomial of F; now let x,y,z be Element of P; x in the carrier of P; then x in C by defprfp; then consider q being Polynomial of F such that A1: x = q & deg q < deg p; y in the carrier of P; then y in C by defprfp; then consider r being Polynomial of F such that A2: y = r & deg r < deg p; z in the carrier of P; then z in C by defprfp; then consider u being Polynomial of F such that A3: z = u & deg u < deg p; A3a: [x,y] in [:C,C:] & [y,z] in [:C,C:] by H0,ZFMISC_1:def 2; A3b: [x*y,z] in [:C,C:] & [x,y*z] in [:C,C:] by H0,ZFMISC_1:def 2; A4: x * y = ((poly_mult_mod p)||C).(x,y) by H0,defprfp .= (poly_mult_mod p).(x,y) by A3a,FUNCT_1:49 .= (q *' r) mod p1 by A1,A2,defpmm; A5: y * z = ((poly_mult_mod p)||C).(y,z) by H0,defprfp .= (poly_mult_mod p).(y,z) by A3a,FUNCT_1:49 .= (r *' u) mod p1 by A3,A2,defpmm; A6: (x * y) * z = ((poly_mult_mod p)||C).(x*y,z) by H0,defprfp .= (poly_mult_mod p).(x*y,z) by A3b,FUNCT_1:49 .= (((q *' r) mod p1) *' u) mod p1 by A3,A4,defpmm .= ( q *' r *' u) mod p1 by div3; thus x * (y * z) = ((poly_mult_mod p)||C).(x,y*z) by H0,defprfp .= (poly_mult_mod p).(x,y*z) by A3b,FUNCT_1:49 .= (((r *' u) mod p1) *' q) mod p1 by A1,A5,defpmm .= (r *' u *' q) mod p1 by div3 .= (x * y) * z by A6,POLYNOM3:33; end; hence P is associative by GROUP_1:def 3; now let x being Element of P; x in the carrier of P; then x in C by defprfp; then consider q being Polynomial of F such that A1: x = q & deg q < deg p; A3a: [x,1.P] in [:C,C:] & [1.P,x] in [:C,C:] by H0,ZFMISC_1:def 2; thus x * 1.P = ((poly_mult_mod p)||C).(x,1.P) by H0,defprfp .= (poly_mult_mod p).(x,1.P) by A3a,FUNCT_1:49 .= (q *' 1_.(F)) mod p1 by H2,A1,defpmm .= q mod p1 by POLYNOM3:35 .= x by A1,div1; thus 1.P * x = ((poly_mult_mod p)||C).(1.P,x) by H0,defprfp .= (poly_mult_mod p).(1.P,x) by A3a,FUNCT_1:49 .= ((1_.(F)) *' q) mod p1 by H2,A1,defpmm .= q mod p1 by POLYNOM3:35 .= x by A1,div1; end; hence P is well-unital by VECTSP_1:def 6; now let x,y,z be Element of P; x in the carrier of P; then x in C by defprfp; then consider q being Polynomial of F such that A1: x = q & deg q < deg p; y in the carrier of P; then y in C by defprfp; then consider r being Polynomial of F such that A2: y = r & deg r < deg p; z in the carrier of P; then z in C by defprfp; then consider u being Polynomial of F such that A3: z = u & deg u < deg p; reconsider q1=q,r1=r,u1=u as Element of Polynom-Ring F by POLYNOM3:def 10; A3a: [x,y] in [:C,C:] & [x,z] in [:C,C:] & [y,z] in [:C,C:] by H0,ZFMISC_1:def 2; A3b: [x*y,x*z] in [:C,C:] & [x,y*z] in [:C,C:] & [x,y+z] in [:C,C:] by H0,ZFMISC_1:def 2; A4: y + z = ((the addF of Polynom-Ring F)||C).(y,z) by H0,defprfp .= r1 + u1 by A2,A3,A3a,FUNCT_1:49 .= r + u by POLYNOM3:def 10; A5: x* (y+z) = ((poly_mult_mod p)||C).(x,y+z) by H0,defprfp .= (poly_mult_mod p).(x,y+z) by A3b,FUNCT_1:49 .= (q *' (r +u)) mod p1 by A1,A4,defpmm; A6: x * y = ((poly_mult_mod p)||C).(x,y) by H0,defprfp .= (poly_mult_mod p).(x,y) by A3a,FUNCT_1:49 .= (q *' r) mod p1 by A1,A2,defpmm; A7: x * z = ((poly_mult_mod p)||C).(x,z) by H0,defprfp .= (poly_mult_mod p).(x,z) by A3a,FUNCT_1:49 .= (q *' u) mod p1 by A1,A3,defpmm; reconsider s = (q*'r) mod p1 as Element of Polynom-Ring F by POLYNOM3:def 10; reconsider t = (q*'u) mod p1 as Element of Polynom-Ring F by POLYNOM3:def 10; thus x*y+x*z = ((the addF of Polynom-Ring F)||C).(x*y,x*z) by H0,defprfp .= s + t by A6,A7,A3b,FUNCT_1:49 .= ((q*'r) mod p1) + ((q*'u) mod p1) by POLYNOM3:def 10 .= (q*'r + q*'u) mod p1 by div4 .= x* (y+z) by A5,POLYNOM3:31; A3a: [y,x] in [:C,C:] & [z,x] in [:C,C:] & [y,z] in [:C,C:] by H0,ZFMISC_1:def 2; A3b: [y*x,z*x] in [:C,C:] & [x,y*z] in [:C,C:] & [y+z,x] in [:C,C:] by H0,ZFMISC_1:def 2; A4: y + z = ((the addF of Polynom-Ring F)||C).(y,z) by H0,defprfp .= r1 + u1 by A2,A3,A3a,FUNCT_1:49 .= r + u by POLYNOM3:def 10; A5: (y+z) * x = ((poly_mult_mod p)||C).(y+z,x) by H0,defprfp .= (poly_mult_mod p).(y+z,x) by A3b,FUNCT_1:49 .= ((r +u) *' q) mod p1 by A1,A4,defpmm; A6: y * x = ((poly_mult_mod p)||C).(y,x) by H0,defprfp .= (poly_mult_mod p).(y,x) by A3a,FUNCT_1:49 .= (r *' q) mod p1 by A1,A2,defpmm; A7: z * x = ((poly_mult_mod p)||C).(z,x) by H0,defprfp .= (poly_mult_mod p).(z,x) by A3a,FUNCT_1:49 .= (u *' q) mod p1 by A1,A3,defpmm; reconsider s = (r*'q) mod p1 as Element of Polynom-Ring F by POLYNOM3:def 10; reconsider t = (u*'q) mod p1 as Element of Polynom-Ring F by POLYNOM3:def 10; thus y*x+z*x = ((the addF of Polynom-Ring F)||C).(y*x,z*x) by H0,defprfp .= s + t by A6,A7,A3b,FUNCT_1:49 .= ((q*'r) mod p1) + ((q*'u) mod p1) by POLYNOM3:def 10 .= (q*'r + q*'u) mod p1 by div4 .= (y+z) * x by A5,POLYNOM3:31; end; hence P is distributive by VECTSP_1:def 7; end; end; definition let F be Field, p be non constant Element of the carrier of Polynom-Ring F; func poly_mod p -> Function of Polynom-Ring F, Polynom-Ring(p) means :dpm: for q being Polynomial of F holds it.q = q mod p; existence proof set B = Polynom-Ring F; set D = the carrier of B; defpred P[object,object] means ex q being Element of D st $1 = q & $2 = q mod p; now let x be object; assume x in D; then reconsider xx=x as Element of D; reconsider r=xx as Polynomial of F; thus ex z being object st z in the carrier of Polynom-Ring(p) & P[x,z] proof take s = r mod p; deg s < deg p by RING_2:29; then s in {q where q is Polynomial of F : deg q < deg p}; hence s in the carrier of Polynom-Ring(p) by defprfp; take xx; thus thesis; end; end; then I: for x being object st x in D ex y being object st y in the carrier of Polynom-Ring(p) & P[x,y]; consider f being Function of D,Polynom-Ring(p) such that H: for x being object st x in D holds P[x,f.x] from FUNCT_2:sch 1(I); reconsider f as Function of B,Polynom-Ring(p); take f; now let q be Polynomial of F; q in B by POLYNOM3:def 10; then P[q,f.q] by H; then consider qq being Element of D such that K: qq = q & f.qq = qq mod p; thus f.q = q mod p by K; end; hence thesis; end; uniqueness proof set B = Polynom-Ring F; let g1,g2 be Function of B,Polynom-Ring(p) such that A1: for q being Polynomial of F holds g1.q = q mod p and A2: for q being Polynomial of F holds g2.q = q mod p; A: dom g1 = the carrier of B by FUNCT_2:def 1 .= dom g2 by FUNCT_2:def 1; now let x be object; assume x in dom g1; then reconsider q = x as Polynomial of F by POLYNOM3:def 10; thus g1.x = q mod p by A1 .= g2.x by A2; end; hence thesis by A,FUNCT_1:2; end; end; registration let F be Field, p be non constant Element of the carrier of Polynom-Ring F; cluster poly_mod p -> additive multiplicative unity-preserving; coherence proof set f = poly_mod p, K = Polynom-Ring(p); set C = the carrier of K; hereby let x1,y1 be Element of Polynom-Ring F; reconsider x=x1,y=y1 as Element of the carrier of Polynom-Ring F; H: f.x = x mod p & f.y = y mod p by dpm; then reconsider fx = f.x, fy = f.y as Element of Polynom-Ring F by POLYNOM3:def 10; A3: [f.x,f.y] in [:C,C:] by ZFMISC_1:def 2; thus f.x1 + f.y1 = ((the addF of Polynom-Ring F)||(the carrier of K)).(f.x1,f.y1) by defprfp .= fx + fy by A3,FUNCT_1:49 .= (x mod p) + (y mod p) by H,POLYNOM3:def 10 .= (x + y) mod p by div4 .= f.(x+y) by dpm .= f.(x1+y1) by POLYNOM3:def 10; end; hereby let x1,y1 be Element of Polynom-Ring F; reconsider x=x1,y=y1 as Element of the carrier of Polynom-Ring F; H: f.x = x mod p & f.y = y mod p by dpm; then reconsider fx = f.x, fy = f.y as Element of Polynom-Ring F by POLYNOM3:def 10; A3: [f.x,f.y] in [:C,C:] by ZFMISC_1:def 2; thus f.x1 * f.y1 = ((poly_mult_mod p)||(the carrier of K)).(f.x1,f.y1) by defprfp .= (poly_mult_mod p).(f.x,f.y) by A3,FUNCT_1:49 .= ((x mod p) *' (y mod p)) mod p by H,defpmm .= (x *' y) mod p by div3a .= f.(x*'y) by dpm .= f.(x1*y1) by POLYNOM3:def 10; end; deg p > 0 by defconst; then H: deg 1_.(F) < deg p by RATFUNC1:def 2; thus f.(1_(Polynom-Ring F)) = f.(1_.(F)) by POLYNOM3:def 10 .= 1_.(F) mod p by dpm .= 1_.(F) by H,div1 .= 1_K by defprfp; end; end; registration let F be Field, p be non constant Element of the carrier of Polynom-Ring F; cluster Polynom-Ring(p) -> (Polynom-Ring F)-homomorphic; coherence proof poly_mod p is linear proof thus poly_mod p is additive multiplicative unity-preserving; end; hence thesis by RING_2:def 4; end; end; registration let F be Field, p be non constant Element of the carrier of Polynom-Ring F; cluster poly_mod p -> onto; coherence proof set f = poly_mod p; now let x be object; assume x in the carrier of Polynom-Ring(p); then x in {q where q is Polynomial of F : deg q < deg p} by defprfp; then consider q being Polynomial of F such that B: q = x & deg q < deg p; q mod p = q by B,div1; then C: f.x = q by B,dpm; dom f = the carrier of Polynom-Ring F by FUNCT_2:def 1; then q in dom f by POLYNOM3:def 10; hence x in rng f by B,C,FUNCT_1:def 3; end; then for x be object holds x in rng f iff x in the carrier of Polynom-Ring(p); hence thesis by FUNCT_2:def 3,TARSKI:2; end; end; lemminuspoly: for R be Ring, a be Element of Polynom-Ring R, b be Polynomial of R st a = b holds -a = -b proof let R be Ring, a be Element of Polynom-Ring R, b be Polynomial of R; assume AS: a = b; set K = Polynom-Ring R; reconsider c = -b as Element of Polynom-Ring R by POLYNOM3:def 10; a + c = b - b by AS,POLYNOM3:def 10 .= 0_.(R) by POLYNOM3:29 .= 0.K by POLYNOM3:def 10 .= a + (-a) by RLVECT_1:5; hence thesis by RLVECT_1:8; end; theorem kerp: for F being Field, p being non constant Element of the carrier of Polynom-Ring F holds ker(poly_mod p) = {p}-Ideal proof let F be Field, p be non constant Element of the carrier of Polynom-Ring F; set R = Polynom-Ring F, S = Polynom-Ring(p); set f = poly_mod p; reconsider p1 = p as Element of R; A: now let x be object; assume A0: x in ker f; then x in {v where v is Element of R : f.v = 0.S} by VECTSP10:def 9; then consider y being Element of R such that A1: y = x & f.y = 0.S; reconsider q = x as Element of the carrier of R by A0; reconsider q1 = x as Element of R by A0; A2: q - (q div p) *' p = q mod p .= 0.S by A1,dpm .= 0_.(F) by defprfp; reconsider qp = q div p as Element of R by POLYNOM3:def 10; qp * p1 = (q div p) *' p by POLYNOM3:def 10; then A3: -(qp * p1) = -((q div p) *' p) by lemminuspoly; q1 - qp * p1 = q + -((q div p) *' p) by A3,POLYNOM3:def 10 .= 0.R by A2,POLYNOM3:def 10; then qp * p1 = q1 by RLVECT_1:21; then q in the set of all p*r where r is Element of R; hence x in {p}-Ideal by IDEAL_1:64; end; now let x be object; assume x in {p}-Ideal; then x in the set of all p*r where r is Element of R by IDEAL_1:64; then consider y being Element of R such that A1: x = p * y; reconsider q = y as Element of the carrier of R; p * y = p *' q by POLYNOM3:def 10; then f.x = (p *' q) mod p by A1,dpm .= 0_.(F) by T2,div2 .= 0.S by defprfp; then x in {v where v is Element of R : f.v = 0.S} by A1; hence x in ker(poly_mod p) by VECTSP10:def 9; end; hence thesis by A,TARSKI:2; end; theorem ISO: for F being Field, p being non constant Element of the carrier of Polynom-Ring F holds (Polynom-Ring F)/({p}-Ideal), Polynom-Ring(p) are_isomorphic proof let F be Field, p be non constant Element of the carrier of Polynom-Ring F; set R = Polynom-Ring F, S = Polynom-Ring(p); R/ker(poly_mod p), S are_isomorphic by RING_2:16; hence thesis by kerp; end; registration let F be Field, p be non constant Element of the carrier of Polynom-Ring F; cluster Polynom-Ring(p) -> commutative; coherence proof set R = (Polynom-Ring F)/({p}-Ideal), S = Polynom-Ring(p); ex f being Function of R,S st f is RingIsomorphism by ISO,QUOFIELD:def 23; then Polynom-Ring(p) is R-isomorphic by RING_3:def 4; hence S is commutative; end; end; registration let F be Field, p be irreducible Element of the carrier of Polynom-Ring F; cluster Polynom-Ring(p) -> almost_left_invertible; coherence proof set R = (Polynom-Ring F)/({p}-Ideal), S = Polynom-Ring(p); ex f being Function of R,S st f is RingIsomorphism by ISO,QUOFIELD:def 23; then Polynom-Ring(p) is R-isomorphic by RING_3:def 4; hence thesis; end; end; begin :: Polynomial GCDs definition let L be non empty multMagma; let x,y be Element of L; let z be Element of L; attr z is x,y-gcd means :defGCD: z divides x & z divides y & for r being Element of L st r divides x & r divides y holds r divides z; end; registration let L be gcdDomain; let x,y be Element of L; cluster x,y-gcd for Element of L; existence proof consider z being Element of L such that H: z divides x & z divides y & for zz being Element of L st zz divides x & zz divides y holds zz divides z by GCD_1:def 11; take z; thus thesis by H; end; end; definition let L be gcdDomain; let x,y be Element of L; mode a_gcd of x,y is x,y-gcd Element of L; end; theorem gcd1: for L being gcdDomain for x,y being Element of L for u,v being a_gcd of x,y holds u is_associated_to v proof let L be gcdDomain; let p,q be Element of L; let u,v be a_gcd of p,q; A: u divides p & u divides q by defGCD; v divides p & v divides q by defGCD; hence thesis by A,defGCD; end; registration let L be gcdDomain; let x,y be Element of L; cluster x,y-gcd -> y,x-gcd for Element of L; coherence; end; definition let F be Field; let p,q be Element of the carrier of Polynom-Ring F; func p gcd q -> Element of the carrier of Polynom-Ring F means :dpg: it = 0_.(F) if p = 0_.(F) & q = 0_.(F) otherwise it is a_gcd of p,q & it is monic; existence proof per cases; suppose p = 0_.(F) & q = 0_.(F); hence thesis; end; suppose AS: p <> 0_.(F) or q <> 0_.(F); reconsider g = the a_gcd of p,q as Element of the carrier of Polynom-Ring F; reconsider p1 = p, q1 = q as Element of Polynom-Ring F; set r = NormPolynomial g; reconsider r1 = r as Element of Polynom-Ring F; A: now assume g is zero; then g = 0_.(F) by UPROOTS:def 5; then D1: g = 0.(Polynom-Ring F) by POLYNOM3:def 10; g divides p1 by defGCD; then consider u being Element of the carrier of Polynom-Ring F such that D2: g * u = p1; g divides q1 by defGCD; then consider v being Element of the carrier of Polynom-Ring F such that D4: g * v = q1; thus contradiction by D1,D4,D2,AS,POLYNOM3:def 10; end; g divides p1 by defGCD; then g divides p; then F: r divides p by np1; g divides q1 by defGCD; then g divides q; then B: r divides q by np1; now let z be Element of Polynom-Ring F; reconsider z1 = z as Element of the carrier of Polynom-Ring F; assume z divides p & z divides q; then z divides g by defGCD; then z1 divides g; then z1 divides r by np2; hence z divides r1; end; then r1 is p,q-gcd by B,F; hence thesis by A; end; end; uniqueness proof per cases; suppose p = 0_.(F) & q = 0_.(F); hence thesis; end; suppose p <> 0_.(F) or q <> 0_.(F); thus thesis by gcd1,np0; end; end; consistency; end; definition let F be Field; let p,q be Element of the carrier of Polynom-Ring F; redefine func p gcd q; commutativity proof now let p,q be Element of the carrier of Polynom-Ring F; per cases; suppose AS: p = 0_.(F) & q = 0_.(F); thus p gcd q = q gcd p by AS; end; suppose AS: p <> 0_.(F) or q <> 0_.(F); then (p gcd q) is a_gcd of p,q & (p gcd q) is monic by dpg; hence p gcd q = q gcd p by AS,dpg; end; end; hence thesis; end; end; definition let F be Field; let p,q be Element of Polynom-Ring F; redefine func p gcd q; commutativity proof for p,q being Element of Polynom-Ring F holds p gcd q = q gcd p; hence thesis; end; end; registration let F be Field; let p,q be Element of the carrier of Polynom-Ring F; cluster p gcd q -> p,q-gcd; coherence proof per cases; suppose A: p = 0_.(F) & q = 0_.(F); reconsider g = p gcd q as Element of Polynom-Ring F; g divides p & g divides q by A,dpg; hence thesis by A,dpg; end; suppose A: p <> 0_.(F) or q <> 0_.(F); set g = p gcd q; reconsider p1 = p, q1 = q as Element of Polynom-Ring F; set g1 = p1 gcd q1; reconsider g1 as Element of Polynom-Ring F; thus thesis by A,dpg; end; end; end; registration let F be Field; let p,q be Element of Polynom-Ring F; cluster p gcd q -> p,q-gcd; coherence; end; registration let F be Field; let p be Element of the carrier of Polynom-Ring F; let q be non zero Element of the carrier of Polynom-Ring F; cluster p gcd q -> non zero monic; coherence proof reconsider p1 = p, q1 = q as Element of Polynom-Ring F; set g1 = p1 gcd q1; set g = p gcd q; reconsider g1 as Element of Polynom-Ring F; D: now assume g is zero; then g = 0_.(F) by UPROOTS:def 5; then D1: g = 0.(Polynom-Ring F) by POLYNOM3:def 10; D3: q <> 0_.(F); g1 divides q1 by defGCD; then consider v being Element of the carrier of Polynom-Ring F such that D4: g1 * v = q; thus contradiction by D1,D4,D3,POLYNOM3:def 10; end; hence g is non zero; g <> 0_.(F) by D; hence thesis by dpg; end; end; registration let F be Field; let p be Element of Polynom-Ring F; let q be non zero Element of Polynom-Ring F; cluster p gcd q -> non zero monic; coherence proof set g = p gcd q; reconsider g1 = g as Element of Polynom-Ring F; q <> 0.(Polynom-Ring F); then D3: q <> 0_.(F) by POLYNOM3:def 10; now assume g is zero; then g = 0_.(F) by UPROOTS:def 5; then D1: g = 0.(Polynom-Ring F) by POLYNOM3:def 10; g1 divides q by defGCD; then consider v being Element of the carrier of Polynom-Ring F such that D4: g1 * v = q; thus contradiction by D1,D4; end; hence g is non zero; thus thesis by D3,dpg; end; end; registration let F be Field; let p,q be zero Element of the carrier of Polynom-Ring F; cluster p gcd q -> zero; coherence proof reconsider g = p gcd q as Element of Polynom-Ring F; p = 0_.(F) & q = 0_.(F) by UPROOTS:def 5; hence p gcd q is zero by dpg; end; end; registration let F be Field; let p,q be zero Element of Polynom-Ring F; cluster p gcd q -> zero; coherence proof reconsider g = p gcd q as Element of Polynom-Ring F; p = 0.(Polynom-Ring F) & q = 0.(Polynom-Ring F) by STRUCT_0:def 12; then p = 0_.(F) & q = 0_.(F) by POLYNOM3:def 10; hence p gcd q is zero; end; end; theorem for F being Field, p,q being Element of the carrier of Polynom-Ring F holds (p gcd q) divides p & (p gcd q) divides q & for r being Element of the carrier of Polynom-Ring F st r divides p & r divides q holds r divides (p gcd q) proof let F be Field, p,q be Element of the carrier of Polynom-Ring F; set g = p gcd q; reconsider g1 = p gcd q as Element of Polynom-Ring F; g1 divides p & g1 divides q by defGCD; hence g divides p & g divides q; now let r be Element of the carrier of Polynom-Ring F; reconsider r1 = r as Element of Polynom-Ring F; assume r divides p & r divides q; then r1 divides g1 by defGCD; hence r divides g; end; hence thesis; end; theorem for F being Field, p,q being Element of Polynom-Ring F holds (p gcd q) divides p & (p gcd q) divides q & for r being Element of Polynom-Ring F st r divides p & r divides q holds r divides (p gcd q) by defGCD; definition let F be Field; let p,q be Polynomial of F; func p gcd q -> Polynomial of F means :dd: ex a,b being Element of Polynom-Ring F st a = p & b = q & it = a gcd b; existence proof reconsider a = p, b = q as Element of Polynom-Ring F by POLYNOM3:def 10; take a gcd b; thus thesis; end; uniqueness; end; definition let F be Field; let p,q be Polynomial of F; redefine func p gcd q; commutativity proof now let p,q be Polynomial of F; reconsider a = p, b = q as Element of Polynom-Ring F by POLYNOM3:def 10; thus p gcd q = a gcd b by dd .= q gcd p by dd; end; hence thesis; end; end; registration let F be Field; let p be Polynomial of F; let q be non zero Polynomial of F; cluster p gcd q -> non zero monic; coherence proof reconsider a = p, b = q as Element of Polynom-Ring F by POLYNOM3:def 10; A0: p gcd q = a gcd b by dd; q <> 0_.(F); then q <> 0.(Polynom-Ring F) by POLYNOM3:def 10; then reconsider b as non zero Element of Polynom-Ring F by STRUCT_0:def 12; thus p gcd q is non zero by A0; thus thesis by A0; end; end; registration let F be Field; let p,q be zero Polynomial of F; cluster p gcd q -> zero; coherence proof p = 0_.(F) & q = 0_.(F) by UPROOTS:def 5; then p = 0.(Polynom-Ring F) & q = 0.(Polynom-Ring F) by POLYNOM3:def 10; then reconsider a = p, b = q as zero Element of Polynom-Ring F; p gcd q = a gcd b by dd; hence p gcd q is zero; end; end; theorem G1: for F being Field, p,q being Polynomial of F holds (p gcd q) divides p & (p gcd q) divides q & for r being Polynomial of F st r divides p & r divides q holds r divides (p gcd q) proof let F be Field, p,q being Polynomial of F; reconsider a = p, b = q as Element of Polynom-Ring F by POLYNOM3:def 10; set g = a gcd b; A0: p gcd q = g by dd; g divides a by defGCD; then consider c being Element of Polynom-Ring F such that A1: g * c = a; reconsider r = c as Polynomial of F by POLYNOM3:def 10; (p gcd q) *' r = p by A0,A1,POLYNOM3:def 10; hence p gcd q divides p by T2; g divides b by defGCD; then consider c being Element of Polynom-Ring F such that A1: g * c = b; reconsider r = c as Polynomial of F by POLYNOM3:def 10; (p gcd q) *' r = q by A0,A1,POLYNOM3:def 10; hence p gcd q divides q by T2; now let r be Polynomial of F; assume A1: r divides p & r divides q; reconsider c = r as Element of Polynom-Ring F by POLYNOM3:def 10; consider s being Polynomial of F such that A2: r *' s = p by A1,T2; consider t being Polynomial of F such that A3: r *' t = q by A1,T2; reconsider x=s, y=t as Element of Polynom-Ring F by POLYNOM3:def 10; c * x = a & c * y = b by A2,A3,POLYNOM3:def 10; then c divides a & c divides b; then c divides a gcd b by defGCD; hence r divides (p gcd q) by dd; end; hence thesis; end; theorem for F being Field for p being Polynomial of F for q being non zero Polynomial of F for s being monic Polynomial of F holds s = p gcd q iff (s divides p & s divides q & for r being Polynomial of F st r divides p & r divides q holds r divides s) proof let F be Field, p be Polynomial of F; let q be non zero Polynomial of F; let s be monic Polynomial of F; now assume AS: s divides p & s divides q & for r being Polynomial of F st r divides p & r divides q holds r divides s; reconsider a = p, b = q as Element of Polynom-Ring F by POLYNOM3:def 10; reconsider g = s as Element of the carrier of Polynom-Ring F by POLYNOM3:def 10; B: b <> 0_.(F); now let d be Element of Polynom-Ring F; assume C: d divides a & d divides b; reconsider h = d as Polynomial of F by POLYNOM3:def 10; h divides p & h divides q by C; then h divides s by AS; hence d divides g; end; then g is a,b-gcd by AS; then g = a gcd b by dpg,B; hence s = p gcd q by dd; end; hence thesis by G1; end;