let n be Element of NAT ; :: thesis: for T being connected admissible TermOrder of n

for L being non empty non degenerated right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative doubleLoopStr

for I being add-closed left-ideal Subset of (Polynom-Ring (n,L))

for G being Subset of (Polynom-Ring (n,L)) st G c= I & ( for f being non-zero Polynomial of n,L st f in I holds

f is_reducible_wrt G,T ) holds

for f being non-zero Polynomial of n,L st f in I holds

f is_top_reducible_wrt G,T

let T be connected admissible TermOrder of n; :: thesis: for L being non empty non degenerated right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative doubleLoopStr

for I being add-closed left-ideal Subset of (Polynom-Ring (n,L))

for G being Subset of (Polynom-Ring (n,L)) st G c= I & ( for f being non-zero Polynomial of n,L st f in I holds

f is_reducible_wrt G,T ) holds

for f being non-zero Polynomial of n,L st f in I holds

f is_top_reducible_wrt G,T

let L be non empty non degenerated right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative doubleLoopStr ; :: thesis: for I being add-closed left-ideal Subset of (Polynom-Ring (n,L))

for G being Subset of (Polynom-Ring (n,L)) st G c= I & ( for f being non-zero Polynomial of n,L st f in I holds

f is_reducible_wrt G,T ) holds

for f being non-zero Polynomial of n,L st f in I holds

f is_top_reducible_wrt G,T

let I be add-closed left-ideal Subset of (Polynom-Ring (n,L)); :: thesis: for G being Subset of (Polynom-Ring (n,L)) st G c= I & ( for f being non-zero Polynomial of n,L st f in I holds

f is_reducible_wrt G,T ) holds

for f being non-zero Polynomial of n,L st f in I holds

f is_top_reducible_wrt G,T

let P be Subset of (Polynom-Ring (n,L)); :: thesis: ( P c= I & ( for f being non-zero Polynomial of n,L st f in I holds

f is_reducible_wrt P,T ) implies for f being non-zero Polynomial of n,L st f in I holds

f is_top_reducible_wrt P,T )

assume A1: P c= I ; :: thesis: ( ex f being non-zero Polynomial of n,L st

( f in I & not f is_reducible_wrt P,T ) or for f being non-zero Polynomial of n,L st f in I holds

f is_top_reducible_wrt P,T )

assume A2: for f being non-zero Polynomial of n,L st f in I holds

f is_reducible_wrt P,T ; :: thesis: for f being non-zero Polynomial of n,L st f in I holds

f is_top_reducible_wrt P,T

thus for f being non-zero Polynomial of n,L st f in I holds

f is_top_reducible_wrt P,T :: thesis: verum

for L being non empty non degenerated right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative doubleLoopStr

for I being add-closed left-ideal Subset of (Polynom-Ring (n,L))

for G being Subset of (Polynom-Ring (n,L)) st G c= I & ( for f being non-zero Polynomial of n,L st f in I holds

f is_reducible_wrt G,T ) holds

for f being non-zero Polynomial of n,L st f in I holds

f is_top_reducible_wrt G,T

let T be connected admissible TermOrder of n; :: thesis: for L being non empty non degenerated right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative doubleLoopStr

for I being add-closed left-ideal Subset of (Polynom-Ring (n,L))

for G being Subset of (Polynom-Ring (n,L)) st G c= I & ( for f being non-zero Polynomial of n,L st f in I holds

f is_reducible_wrt G,T ) holds

for f being non-zero Polynomial of n,L st f in I holds

f is_top_reducible_wrt G,T

let L be non empty non degenerated right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative doubleLoopStr ; :: thesis: for I being add-closed left-ideal Subset of (Polynom-Ring (n,L))

for G being Subset of (Polynom-Ring (n,L)) st G c= I & ( for f being non-zero Polynomial of n,L st f in I holds

f is_reducible_wrt G,T ) holds

for f being non-zero Polynomial of n,L st f in I holds

f is_top_reducible_wrt G,T

let I be add-closed left-ideal Subset of (Polynom-Ring (n,L)); :: thesis: for G being Subset of (Polynom-Ring (n,L)) st G c= I & ( for f being non-zero Polynomial of n,L st f in I holds

f is_reducible_wrt G,T ) holds

for f being non-zero Polynomial of n,L st f in I holds

f is_top_reducible_wrt G,T

let P be Subset of (Polynom-Ring (n,L)); :: thesis: ( P c= I & ( for f being non-zero Polynomial of n,L st f in I holds

f is_reducible_wrt P,T ) implies for f being non-zero Polynomial of n,L st f in I holds

f is_top_reducible_wrt P,T )

assume A1: P c= I ; :: thesis: ( ex f being non-zero Polynomial of n,L st

( f in I & not f is_reducible_wrt P,T ) or for f being non-zero Polynomial of n,L st f in I holds

f is_top_reducible_wrt P,T )

assume A2: for f being non-zero Polynomial of n,L st f in I holds

f is_reducible_wrt P,T ; :: thesis: for f being non-zero Polynomial of n,L st f in I holds

f is_top_reducible_wrt P,T

thus for f being non-zero Polynomial of n,L st f in I holds

f is_top_reducible_wrt P,T :: thesis: verum

proof

set H = { g where g is non-zero Polynomial of n,L : ( g in I & not g is_top_reducible_wrt P,T ) } ;

let f be non-zero Polynomial of n,L; :: thesis: ( f in I implies f is_top_reducible_wrt P,T )

assume A3: f in I ; :: thesis: f is_top_reducible_wrt P,T

assume not f is_top_reducible_wrt P,T ; :: thesis: contradiction

then A4: f in { g where g is non-zero Polynomial of n,L : ( g in I & not g is_top_reducible_wrt P,T ) } by A3;

consider p being Polynomial of n,L such that

A5: p in H and

A6: for q being Polynomial of n,L st q in H holds

p <= q,T by POLYRED:31;

A7: ex p9 being non-zero Polynomial of n,L st

( p9 = p & p9 in I & not p9 is_top_reducible_wrt P,T ) by A5;

then reconsider p = p as non-zero Polynomial of n,L ;

p is_reducible_wrt P,T by A2, A7;

then consider q being Polynomial of n,L such that

A8: p reduces_to q,P,T by POLYRED:def 9;

consider u being Polynomial of n,L such that

A9: u in P and

A10: p reduces_to q,u,T by A8, POLYRED:def 7;

ex b being bag of n st p reduces_to q,u,b,T by A10, POLYRED:def 6;

then A11: u <> 0_ (n,L) by POLYRED:def 5;

then reconsider u = u as non-zero Polynomial of n,L by POLYNOM7:def 1;

consider b being bag of n such that

A12: p reduces_to q,u,b,T by A10, POLYRED:def 6;

A14: q = p - (m *' u) by A10, Th1;

reconsider uu = u, pp = p, mm = m as Element of (Polynom-Ring (n,L)) by POLYNOM1:def 11;

reconsider uu = uu, pp = pp, mm = mm as Element of (Polynom-Ring (n,L)) ;

mm * uu in I by A1, A9, IDEAL_1:def 2;

then - (mm * uu) in I by IDEAL_1:13;

then A15: pp + (- (mm * uu)) in I by A7, IDEAL_1:def 1;

mm * uu = m *' u by POLYNOM1:def 11;

then p - (m *' u) = pp - (mm * uu) by Lm2;

then A16: q in I by A14, A15;

A17: q < p,T by A10, POLYRED:43;

A18: p <> 0_ (n,L) by POLYNOM7:def 1;

then Support p <> {} by POLYNOM7:1;

then A19: HT (p,T) in Support p by TERMORD:def 6;

b in Support p by A12, POLYRED:def 5;

then b <= HT (p,T),T by TERMORD:def 6;

then b < HT (p,T),T by A13, TERMORD:def 3;

then A20: HT (p,T) in Support q by A19, A12, POLYRED:40;

end;let f be non-zero Polynomial of n,L; :: thesis: ( f in I implies f is_top_reducible_wrt P,T )

assume A3: f in I ; :: thesis: f is_top_reducible_wrt P,T

assume not f is_top_reducible_wrt P,T ; :: thesis: contradiction

then A4: f in { g where g is non-zero Polynomial of n,L : ( g in I & not g is_top_reducible_wrt P,T ) } by A3;

now :: thesis: for u being object st u in { g where g is non-zero Polynomial of n,L : ( g in I & not g is_top_reducible_wrt P,T ) } holds

u in the carrier of (Polynom-Ring (n,L))

then reconsider H = { g where g is non-zero Polynomial of n,L : ( g in I & not g is_top_reducible_wrt P,T ) } as non empty Subset of (Polynom-Ring (n,L)) by A4, TARSKI:def 3;u in the carrier of (Polynom-Ring (n,L))

let u be object ; :: thesis: ( u in { g where g is non-zero Polynomial of n,L : ( g in I & not g is_top_reducible_wrt P,T ) } implies u in the carrier of (Polynom-Ring (n,L)) )

assume u in { g where g is non-zero Polynomial of n,L : ( g in I & not g is_top_reducible_wrt P,T ) } ; :: thesis: u in the carrier of (Polynom-Ring (n,L))

then ex g9 being non-zero Polynomial of n,L st

( u = g9 & g9 in I & not g9 is_top_reducible_wrt P,T ) ;

hence u in the carrier of (Polynom-Ring (n,L)) ; :: thesis: verum

end;assume u in { g where g is non-zero Polynomial of n,L : ( g in I & not g is_top_reducible_wrt P,T ) } ; :: thesis: u in the carrier of (Polynom-Ring (n,L))

then ex g9 being non-zero Polynomial of n,L st

( u = g9 & g9 in I & not g9 is_top_reducible_wrt P,T ) ;

hence u in the carrier of (Polynom-Ring (n,L)) ; :: thesis: verum

consider p being Polynomial of n,L such that

A5: p in H and

A6: for q being Polynomial of n,L st q in H holds

p <= q,T by POLYRED:31;

A7: ex p9 being non-zero Polynomial of n,L st

( p9 = p & p9 in I & not p9 is_top_reducible_wrt P,T ) by A5;

then reconsider p = p as non-zero Polynomial of n,L ;

p is_reducible_wrt P,T by A2, A7;

then consider q being Polynomial of n,L such that

A8: p reduces_to q,P,T by POLYRED:def 9;

consider u being Polynomial of n,L such that

A9: u in P and

A10: p reduces_to q,u,T by A8, POLYRED:def 7;

ex b being bag of n st p reduces_to q,u,b,T by A10, POLYRED:def 6;

then A11: u <> 0_ (n,L) by POLYRED:def 5;

then reconsider u = u as non-zero Polynomial of n,L by POLYNOM7:def 1;

consider b being bag of n such that

A12: p reduces_to q,u,b,T by A10, POLYRED:def 6;

A13: now :: thesis: not b = HT (p,T)

consider m being Monomial of n,L such that assume
b = HT (p,T)
; :: thesis: contradiction

then p top_reduces_to q,u,T by A12, POLYRED:def 10;

then p is_top_reducible_wrt u,T by POLYRED:def 11;

hence contradiction by A7, A9, POLYRED:def 12; :: thesis: verum

end;then p top_reduces_to q,u,T by A12, POLYRED:def 10;

then p is_top_reducible_wrt u,T by POLYRED:def 11;

hence contradiction by A7, A9, POLYRED:def 12; :: thesis: verum

A14: q = p - (m *' u) by A10, Th1;

reconsider uu = u, pp = p, mm = m as Element of (Polynom-Ring (n,L)) by POLYNOM1:def 11;

reconsider uu = uu, pp = pp, mm = mm as Element of (Polynom-Ring (n,L)) ;

mm * uu in I by A1, A9, IDEAL_1:def 2;

then - (mm * uu) in I by IDEAL_1:13;

then A15: pp + (- (mm * uu)) in I by A7, IDEAL_1:def 1;

mm * uu = m *' u by POLYNOM1:def 11;

then p - (m *' u) = pp - (mm * uu) by Lm2;

then A16: q in I by A14, A15;

A17: q < p,T by A10, POLYRED:43;

A18: p <> 0_ (n,L) by POLYNOM7:def 1;

then Support p <> {} by POLYNOM7:1;

then A19: HT (p,T) in Support p by TERMORD:def 6;

b in Support p by A12, POLYRED:def 5;

then b <= HT (p,T),T by TERMORD:def 6;

then b < HT (p,T),T by A13, TERMORD:def 3;

then A20: HT (p,T) in Support q by A19, A12, POLYRED:40;

now :: thesis: ( ( q <> 0_ (n,L) & contradiction ) or ( q = 0_ (n,L) & contradiction ) )end;

hence
contradiction
; :: thesis: verumper cases
( q <> 0_ (n,L) or q = 0_ (n,L) )
;

end;

case A21:
q <> 0_ (n,L)
; :: thesis: contradiction

then reconsider q = q as non-zero Polynomial of n,L by POLYNOM7:def 1;

Support q <> {} by A21, POLYNOM7:1;

then HT (q,T) in Support q by TERMORD:def 6;

then A22: HT (q,T) <= HT (p,T),T by A10, POLYRED:42;

HT (p,T) <= HT (q,T),T by A20, TERMORD:def 6;

then A23: HT (q,T) = HT (p,T) by A22, TERMORD:7;

A24: u9 in P and

A25: q is_top_reducible_wrt u9,T by POLYRED:def 12;

consider q9 being Polynomial of n,L such that

A26: q top_reduces_to q9,u9,T by A25, POLYRED:def 11;

A27: p <> 0_ (n,L) by POLYNOM7:def 1;

then Support p <> {} by POLYNOM7:1;

then A28: HT (p,T) in Support p by TERMORD:def 6;

A29: q reduces_to q9,u9, HT (q,T),T by A26, POLYRED:def 10;

then consider s being bag of n such that

A30: s + (HT (u9,T)) = HT (q,T) and

q9 = q - (((q . (HT (q,T))) / (HC (u9,T))) * (s *' u9)) by POLYRED:def 5;

set qq = p - (((p . (HT (p,T))) / (HC (u9,T))) * (s *' u9));

u9 <> 0_ (n,L) by A29, POLYRED:def 5;

then p reduces_to p - (((p . (HT (p,T))) / (HC (u9,T))) * (s *' u9)),u9, HT (p,T),T by A23, A30, A27, A28, POLYRED:def 5;

then p top_reduces_to p - (((p . (HT (p,T))) / (HC (u9,T))) * (s *' u9)),u9,T by POLYRED:def 10;

then p is_top_reducible_wrt u9,T by POLYRED:def 11;

hence contradiction by A7, A24, POLYRED:def 12; :: thesis: verum

end;Support q <> {} by A21, POLYNOM7:1;

then HT (q,T) in Support q by TERMORD:def 6;

then A22: HT (q,T) <= HT (p,T),T by A10, POLYRED:42;

HT (p,T) <= HT (q,T),T by A20, TERMORD:def 6;

then A23: HT (q,T) = HT (p,T) by A22, TERMORD:7;

now :: thesis: q is_top_reducible_wrt P,T

then consider u9 being Polynomial of n,L such that assume
not q is_top_reducible_wrt P,T
; :: thesis: contradiction

then q in H by A16;

then p <= q,T by A6;

hence contradiction by A17, POLYRED:29; :: thesis: verum

end;then q in H by A16;

then p <= q,T by A6;

hence contradiction by A17, POLYRED:29; :: thesis: verum

A24: u9 in P and

A25: q is_top_reducible_wrt u9,T by POLYRED:def 12;

consider q9 being Polynomial of n,L such that

A26: q top_reduces_to q9,u9,T by A25, POLYRED:def 11;

A27: p <> 0_ (n,L) by POLYNOM7:def 1;

then Support p <> {} by POLYNOM7:1;

then A28: HT (p,T) in Support p by TERMORD:def 6;

A29: q reduces_to q9,u9, HT (q,T),T by A26, POLYRED:def 10;

then consider s being bag of n such that

A30: s + (HT (u9,T)) = HT (q,T) and

q9 = q - (((q . (HT (q,T))) / (HC (u9,T))) * (s *' u9)) by POLYRED:def 5;

set qq = p - (((p . (HT (p,T))) / (HC (u9,T))) * (s *' u9));

u9 <> 0_ (n,L) by A29, POLYRED:def 5;

then p reduces_to p - (((p . (HT (p,T))) / (HC (u9,T))) * (s *' u9)),u9, HT (p,T),T by A23, A30, A27, A28, POLYRED:def 5;

then p top_reduces_to p - (((p . (HT (p,T))) / (HC (u9,T))) * (s *' u9)),u9,T by POLYRED:def 10;

then p is_top_reducible_wrt u9,T by POLYRED:def 11;

hence contradiction by A7, A24, POLYRED:def 12; :: thesis: verum

case
q = 0_ (n,L)
; :: thesis: contradiction

then A31: m *' u =
(p - (m *' u)) + (m *' u)
by A14, POLYRED:2

.= (p + (- (m *' u))) + (m *' u) by POLYNOM1:def 7

.= p + ((- (m *' u)) + (m *' u)) by POLYNOM1:21

.= p + (0_ (n,L)) by POLYRED:3

.= p by POLYNOM1:23 ;

m <> 0_ (n,L) by A31, POLYRED:5, POLYNOM7:def 1;

then reconsider m = m as non-zero Polynomial of n,L by POLYNOM7:def 1;

set pp = p - (((p . (HT (p,T))) / (HC (u,T))) * ((HT (m,T)) *' u));

HT (p,T) = (HT (m,T)) + (HT (u,T)) by A31, TERMORD:31;

then p reduces_to p - (((p . (HT (p,T))) / (HC (u,T))) * ((HT (m,T)) *' u)),u, HT (p,T),T by A11, A18, A19, POLYRED:def 5;

then p top_reduces_to p - (((p . (HT (p,T))) / (HC (u,T))) * ((HT (m,T)) *' u)),u,T by POLYRED:def 10;

then p is_top_reducible_wrt u,T by POLYRED:def 11;

hence contradiction by A7, A9, POLYRED:def 12; :: thesis: verum

end;.= (p + (- (m *' u))) + (m *' u) by POLYNOM1:def 7

.= p + ((- (m *' u)) + (m *' u)) by POLYNOM1:21

.= p + (0_ (n,L)) by POLYRED:3

.= p by POLYNOM1:23 ;

m <> 0_ (n,L) by A31, POLYRED:5, POLYNOM7:def 1;

then reconsider m = m as non-zero Polynomial of n,L by POLYNOM7:def 1;

set pp = p - (((p . (HT (p,T))) / (HC (u,T))) * ((HT (m,T)) *' u));

HT (p,T) = (HT (m,T)) + (HT (u,T)) by A31, TERMORD:31;

then p reduces_to p - (((p . (HT (p,T))) / (HC (u,T))) * ((HT (m,T)) *' u)),u, HT (p,T),T by A11, A18, A19, POLYRED:def 5;

then p top_reduces_to p - (((p . (HT (p,T))) / (HC (u,T))) * ((HT (m,T)) *' u)),u,T by POLYRED:def 10;

then p is_top_reducible_wrt u,T by POLYRED:def 11;

hence contradiction by A7, A9, POLYRED:def 12; :: thesis: verum