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 RATFUNC1:def 1; 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 RATFUNC1:def 1; 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 RATFUNC1:def 1; 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 RATFUNC1:def 1; 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 RATFUNC1:def 1; 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;