let n be Ordinal; for T being connected TermOrder of n
for L being non trivial right_complementable almost_left_invertible well-unital distributive add-associative right_zeroed associative commutative doubleLoopStr
for P being Subset of (Polynom-Ring (n,L)) st ( for f being non-zero Polynomial of n,L st f in P -Ideal holds
f is_top_reducible_wrt P,T ) holds
for b being bag of n st b in HT ((P -Ideal),T) holds
ex b9 being bag of n st
( b9 in HT (P,T) & b9 divides b )
let T be connected TermOrder of n; for L being non trivial right_complementable almost_left_invertible well-unital distributive add-associative right_zeroed associative commutative doubleLoopStr
for P being Subset of (Polynom-Ring (n,L)) st ( for f being non-zero Polynomial of n,L st f in P -Ideal holds
f is_top_reducible_wrt P,T ) holds
for b being bag of n st b in HT ((P -Ideal),T) holds
ex b9 being bag of n st
( b9 in HT (P,T) & b9 divides b )
let L be non trivial right_complementable almost_left_invertible well-unital distributive add-associative right_zeroed associative commutative doubleLoopStr ; for P being Subset of (Polynom-Ring (n,L)) st ( for f being non-zero Polynomial of n,L st f in P -Ideal holds
f is_top_reducible_wrt P,T ) holds
for b being bag of n st b in HT ((P -Ideal),T) holds
ex b9 being bag of n st
( b9 in HT (P,T) & b9 divides b )
let P be Subset of (Polynom-Ring (n,L)); ( ( for f being non-zero Polynomial of n,L st f in P -Ideal holds
f is_top_reducible_wrt P,T ) implies for b being bag of n st b in HT ((P -Ideal),T) holds
ex b9 being bag of n st
( b9 in HT (P,T) & b9 divides b ) )
assume A1:
for f being non-zero Polynomial of n,L st f in P -Ideal holds
f is_top_reducible_wrt P,T
; for b being bag of n st b in HT ((P -Ideal),T) holds
ex b9 being bag of n st
( b9 in HT (P,T) & b9 divides b )
now for b being bag of n st b in HT ((P -Ideal),T) holds
ex b9 being bag of n st
( b9 in HT (P,T) & b9 divides b )let b be
bag of
n;
( b in HT ((P -Ideal),T) implies ex b9 being bag of n st
( b9 in HT (P,T) & b9 divides b ) )assume
b in HT (
(P -Ideal),
T)
;
ex b9 being bag of n st
( b9 in HT (P,T) & b9 divides b )then consider p being
Polynomial of
n,
L such that A2:
b = HT (
p,
T)
and A3:
p in P -Ideal
and A4:
p <> 0_ (
n,
L)
;
reconsider p =
p as
non-zero Polynomial of
n,
L by A4, POLYNOM7:def 1;
p is_top_reducible_wrt P,
T
by A1, A3;
then consider u being
Polynomial of
n,
L such that A5:
u in P
and A6:
p is_top_reducible_wrt u,
T
by POLYRED:def 12;
consider q being
Polynomial of
n,
L such that A7:
p top_reduces_to q,
u,
T
by A6, POLYRED:def 11;
A8:
p reduces_to q,
u,
HT (
p,
T),
T
by A7, POLYRED:def 10;
then
u <> 0_ (
n,
L)
by POLYRED:def 5;
then A9:
HT (
u,
T)
in { (HT (r,T)) where r is Polynomial of n,L : ( r in P & r <> 0_ (n,L) ) }
by A5;
ex
s being
bag of
n st
(
s + (HT (u,T)) = HT (
p,
T) &
q = p - (((p . (HT (p,T))) / (HC (u,T))) * (s *' u)) )
by A8, POLYRED:def 5;
hence
ex
b9 being
bag of
n st
(
b9 in HT (
P,
T) &
b9 divides b )
by A2, A9, PRE_POLY:50;
verum end;
hence
for b being bag of n st b in HT ((P -Ideal),T) holds
ex b9 being bag of n st
( b9 in HT (P,T) & b9 divides b )
; verum