let n be Element of NAT ; :: thesis:
let T be connected admissible TermOrder of n; :: thesis:
let L be non empty non degenerated right_complementable almost_left_invertible associative commutative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; :: thesis:
let I be non empty add-closed left-ideal Subset of (Polynom-Ring n,L); :: thesis:
let P be non empty Subset of (Polynom-Ring n,L); :: thesis:
assume A1: P c= I ; :: thesis:
then A2: PolyRedRel P,T c= PolyRedRel I,T by Th4;
assume A3: HT I,T c= multiples (HT P,T) ; :: thesis:
set R = PolyRedRel P,T;
A4: for f being Polynomial of n,L st f in I & f <> 0_ n,L holds
f is_reducible_wrt P,T

proof

let f be Polynomial of n,L; :: thesis:
assume A5: ( f in I & f <> 0_ n,L ) ; :: thesis:
then HT f,T in { (HT p,T) where p is Polynomial of n,L : ( p in I & p <> 0_ n,L ) } ;
then HT f,T in multiples (HT P,T) by A3;
then consider b being Element of Bags n such that
A6: ( b = HT f,T & ex b' being bag of st
( b' in HT P,T & b' divides b ) ) ;
consider b' being bag of such that
A7: ( b' in HT P,T & b' divides HT f,T ) by A6;
consider p being Polynomial of n,L such that
A8: ( b' = HT p,T & p in P & p <> 0_ n,L ) by A7;
consider s being bag of such that
A9: b' + s = HT f,T by A7, TERMORD:1;
set g = f - (((f . (HT f,T)) / (HC p,T)) * (s *' p));
Support f <> {} by A5, POLYNOM7:1;
then HT f,T in Support f by TERMORD:def 6;
then f reduces_to f - (((f . (HT f,T)) / (HC p,T)) * (s *' p)),p, HT f,T,T by A5, A8, A9, POLYRED:def 5;
then f reduces_to f - (((f . (HT f,T)) / (HC p,T)) * (s *' p)),p,T by POLYRED:def 6;
then f reduces_to f - (((f . (HT f,T)) / (HC p,T)) * (s *' p)),P,T by A8, POLYRED:def 7;
hence f is_reducible_wrt P,T by POLYRED:def 9; :: thesis:

end;

A10: for f being Polynomial of n,L st f in I holds
PolyRedRel P,T reduces f, 0_ n,L

proof

let f be Polynomial of n,L; :: thesis:
assume A11: f in I ; :: thesis:

per cases ;

suppose f = 0_ n,L ; :: thesis:

hence PolyRedRel P,T reduces f, 0_ n,L by REWRITE1:13; :: thesis:

end;

suppose A12: f <> 0_ n,L ; :: thesis:

assume A13: not PolyRedRel P,T reduces f, 0_ n,L ; :: thesis:
f is_reducible_wrt P,T by A4, A11, A12;
then consider v being Polynomial of n,L such that
A14: f reduces_to v,P,T by POLYRED:def 9;
[f,v] in PolyRedRel P,T by A14, POLYRED:def 13;
then f in field (PolyRedRel P,T) by RELAT_1:30;
then f has_a_normal_form_wrt PolyRedRel P,T by REWRITE1:def 14;
then consider g being set such that
A15: g is_a_normal_form_of f, PolyRedRel P,T by REWRITE1:def 11;
A16: ( g is_a_normal_form_wrt PolyRedRel P,T & PolyRedRel P,T reduces f,g ) by A15, REWRITE1:def 6;
A17: g <> 0_ n,L by A13, A15, REWRITE1:def 6;
reconsider g' = g as Polynomial of n,L by A16, Lm4;
reconsider ff = f, gg = g' as Element of (Polynom-Ring n,L) by POLYNOM1:def 27;
reconsider ff = ff, gg = gg as Element of (Polynom-Ring n,L) ;
f - g' = ff - gg by Lm2;
then ff - gg in I -Ideal by A2, A16, POLYRED:59, REWRITE1:23;
then ff - gg in I by IDEAL_1:44;
then A18: (ff - gg) - ff in I by A11, IDEAL_1:16;
(ff - gg) - ff = (ff + (- gg)) - ff by RLVECT_1:def 12
.= (ff + (- gg)) + (- ff) by RLVECT_1:def 12
.= (ff + (- ff)) + (- gg) by RLVECT_1:def 6
.= (0. (Polynom-Ring n,L)) + (- gg) by RLVECT_1:16
.= - gg by ALGSTR_1:def 5 ;
then - (- gg) in I by A18, IDEAL_1:14;
then g in I by RLVECT_1:30;
then g' is_reducible_wrt P,T by A4, A17;
then consider u being Polynomial of n,L such that
A19: g' reduces_to u,P,T by POLYRED:def 9;
[g',u] in PolyRedRel P,T by A19, POLYRED:def 13;
hence contradiction by A16, REWRITE1:def 5; :: thesis:

end;

then A20: P -Ideal = I by A1, Lm7;

now

let a, b, c be set ; :: thesis:
assume A21: ( [a,b] in PolyRedRel P,T & [a,c] in PolyRedRel P,T ) ; :: thesis:
then consider a', b' being set such that
A22: ( a' in NonZero (Polynom-Ring n,L) & b' in the carrier of (Polynom-Ring n,L) & [a,b] = [a',b'] ) by ZFMISC_1:def 2;
A23: b' = [a,b] `2 by A22, MCART_1:def 2
.= b by MCART_1:def 2 ;
consider aa, c' being set such that
A24: ( aa in NonZero (Polynom-Ring n,L) & c' in the carrier of (Polynom-Ring n,L) & [a,c] = [aa,c'] ) by A21, ZFMISC_1:def 2;
A25: c' = [a,c] `2 by A24, MCART_1:def 2
.= c by MCART_1:def 2 ;
reconsider b' = b', c' = c' as Polynomial of n,L by A22, A24, POLYNOM1:def 27;
reconsider bb = b', cc = c' as Element of (Polynom-Ring n,L) by POLYNOM1:def 27;
reconsider bb = bb, cc = cc as Element of (Polynom-Ring n,L) ;
A26: b' - c' = bb - cc by Lm2;
a,b are_convertible_wrt PolyRedRel P,T by A21, REWRITE1:30;
then X: b,a are_convertible_wrt PolyRedRel P,T by REWRITE1:32;
a,c are_convertible_wrt PolyRedRel P,T by A21, REWRITE1:30;
then bb,cc are_congruent_mod I by A20, A23, A25, X, POLYRED:57, REWRITE1:31;
then bb - cc in I by POLYRED:def 14;
hence b,c are_convergent_wrt PolyRedRel P,T by A10, A23, A25, A26, POLYRED:50; :: thesis:

end;

then PolyRedRel P,T is locally-confluent by REWRITE1:def 24;
hence P is_Groebner_basis_of I,T by A20, Def4; :: thesis: