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 associative commutative well-unital distributive Abelian add-associative right_zeroed 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 associative commutative well-unital distributive Abelian add-associative right_zeroed 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 associative commutative well-unital distributive Abelian add-associative right_zeroed 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
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
set H = { g where g is non-zero Polynomial of n,L : ( g in I & not g 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
let u be set ; :: 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 consider g' being non-zero Polynomial of n,L such that
A5: ( u = g' & g' in I & not g' is_top_reducible_wrt P,T ) ;
thus u in the carrier of (Polynom-Ring n,L) by A5; :: thesis: verum
end;
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;
consider p being Polynomial of n,L such that
A6: ( p in H & ( for q being Polynomial of n,L st q in H holds
p <= q,T ) ) by POLYRED:31;
consider p' being non-zero Polynomial of n,L such that
A7: ( p' = p & p' in I & not p' is_top_reducible_wrt P,T ) by A6;
reconsider p = p as non-zero Polynomial of n,L by A7;
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 & p reduces_to q,u,T ) by A8, POLYRED:def 7;
consider b being bag of such that
A10: p reduces_to q,u,b,T by A9, POLYRED:def 6;
A11: u <> 0_ n,L by A10, POLYRED:def 5;
then reconsider u = u as non-zero Polynomial of n,L by POLYNOM7:def 2;
A12: q < p,T by A9, POLYRED:43;
consider m being Monomial of n,L such that
A13: q = p - (m *' u) by A9, Th1;
reconsider uu = u, pp = p, mm = m as Element of (Polynom-Ring n,L) by POLYNOM1:def 27;
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 A14: pp + (- (mm * uu)) in I by A7, IDEAL_1:def 1;
mm * uu = m *' u by POLYNOM1:def 27;
then p - (m *' u) = pp - (mm * uu) by Lm2;
then A15: q in I by A13, A14, RLVECT_1:def 12;
A16: p <> 0_ n,L by POLYNOM7:def 2;
then Support p <> {} by POLYNOM7:1;
then A17: HT p,T in Support p by TERMORD:def 6;
consider b being bag of such that
A18: p reduces_to q,u,b,T by A9, POLYRED:def 6;
b in Support p by A18, POLYRED:def 5;
then A19: b <= HT p,T,T by TERMORD:def 6;
now
assume b = HT p,T ; :: thesis: contradiction
then p top_reduces_to q,u,T by A18, 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 b < HT p,T,T by A19, TERMORD:def 3;
then A20: HT p,T in Support q by A17, A18, POLYRED:40;
now
per cases ( q <> 0_ n,L or q = 0_ n,L ) ;
case A21: q <> 0_ n,L ; :: thesis: contradiction
then reconsider q = q as non-zero Polynomial of n,L by POLYNOM7:def 2;
Support q <> {} by A21, POLYNOM7:1;
then A22: HT q,T in Support q by TERMORD:def 6;
A23: HT p,T <= HT q,T,T by A20, TERMORD:def 6;
HT q,T <= HT p,T,T by A9, A22, POLYRED:42;
then A24: HT q,T = HT p,T by A23, TERMORD:7;
then consider u' being Polynomial of n,L such that
A25: ( u' in P & q is_top_reducible_wrt u',T ) by POLYRED:def 12;
consider q' being Polynomial of n,L such that
A26: q top_reduces_to q',u',T by A25, POLYRED:def 11;
A27: q reduces_to q',u', HT q,T,T by A26, POLYRED:def 10;
then A28: ( q <> 0_ n,L & u' <> 0_ n,L & HT q,T in Support q & ex s being bag of st
( s + (HT u',T) = HT q,T & q' = q - (((q . (HT q,T)) / (HC u',T)) * (s *' u')) ) ) by POLYRED:def 5;
consider s being bag of such that
A29: ( s + (HT u',T) = HT q,T & q' = q - (((q . (HT q,T)) / (HC u',T)) * (s *' u')) ) by A27, POLYRED:def 5;
set qq = p - (((p . (HT p,T)) / (HC u',T)) * (s *' u'));
A30: p <> 0_ n,L by POLYNOM7:def 2;
then Support p <> {} by POLYNOM7:1;
then HT p,T in Support p by TERMORD:def 6;
then p reduces_to p - (((p . (HT p,T)) / (HC u',T)) * (s *' u')),u', HT p,T,T by A24, A28, A29, A30, POLYRED:def 5;
then p top_reduces_to p - (((p . (HT p,T)) / (HC u',T)) * (s *' u')),u',T by POLYRED:def 10;
then p is_top_reducible_wrt u',T by POLYRED:def 11;
hence contradiction by A7, A25, POLYRED:def 12; :: thesis: verum
end;
case q = 0_ n,L ; :: thesis: contradiction
then A31: m *' u = (p - (m *' u)) + (m *' u) by A13, POLYRED:2
.= (p + (- (m *' u))) + (m *' u) by POLYNOM1:def 23
.= p + ((- (m *' u)) + (m *' u)) by POLYNOM1:80
.= p + (0_ n,L) by POLYRED:3
.= p by POLYNOM1:82 ;
then reconsider m = m as non-zero Polynomial of n,L by POLYNOM7:def 2;
A33: HT p,T = (HT m,T) + (HT u,T) by A31, TERMORD:31;
set pp = p - (((p . (HT p,T)) / (HC u,T)) * ((HT m,T) *' u));
p reduces_to p - (((p . (HT p,T)) / (HC u,T)) * ((HT m,T) *' u)),u, HT p,T,T by A11, A16, A17, A33, 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;
end;
end;
hence contradiction ; :: thesis: verum
end;