let n be Element of NAT ; 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 P being non empty Subset of (Polynom-Ring n,L) st PolyRedRel P,T is with_Church-Rosser_property holds
for f being Polynomial of n,L st f in P -Ideal holds
PolyRedRel P,T reduces f, 0_ n,L
let T be 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 P being non empty Subset of (Polynom-Ring n,L) st PolyRedRel P,T is with_Church-Rosser_property holds
for f being Polynomial of n,L st f in P -Ideal holds
PolyRedRel P,T reduces f, 0_ n,L
let L be non empty non degenerated right_complementable almost_left_invertible associative commutative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; for P being non empty Subset of (Polynom-Ring n,L) st PolyRedRel P,T is with_Church-Rosser_property holds
for f being Polynomial of n,L st f in P -Ideal holds
PolyRedRel P,T reduces f, 0_ n,L
let P be non empty Subset of (Polynom-Ring n,L); ( PolyRedRel P,T is with_Church-Rosser_property implies for f being Polynomial of n,L st f in P -Ideal holds
PolyRedRel P,T reduces f, 0_ n,L )
set R = PolyRedRel P,T;
assume A1:
PolyRedRel P,T is with_Church-Rosser_property
; for f being Polynomial of n,L st f in P -Ideal holds
PolyRedRel P,T reduces f, 0_ n,L
now reconsider e =
0_ n,
L as
Element of
(Polynom-Ring n,L) by POLYNOM1:def 27;
let f be
Polynomial of
n,
L;
( f in P -Ideal implies PolyRedRel P,T reduces f, 0_ n,L )assume A2:
f in P -Ideal
;
PolyRedRel P,T reduces f, 0_ n,Lreconsider e =
e as
Element of
(Polynom-Ring n,L) ;
reconsider f9 =
f as
Element of
(Polynom-Ring n,L) by POLYNOM1:def 27;
reconsider f9 =
f9 as
Element of
(Polynom-Ring n,L) ;
f - (0_ n,L) = f9 - e
by Lm2;
then
f9 - e in P -Ideal
by A2, POLYRED:4;
then
f9,
e are_congruent_mod P -Ideal
by POLYRED:def 14;
then
f9,
e are_convertible_wrt PolyRedRel P,
T
by POLYRED:58;
then
f9,
e are_convergent_wrt PolyRedRel P,
T
by A1, REWRITE1:def 23;
then consider c being
set such that A3:
PolyRedRel P,
T reduces f,
c
and A4:
PolyRedRel P,
T reduces 0_ n,
L,
c
by REWRITE1:def 7;
reconsider c9 =
c as
Polynomial of
n,
L by A3, Lm4;
now assume
c9 <> 0_ n,
L
;
contradictionthen consider h being
Polynomial of
n,
L such that A5:
0_ n,
L reduces_to h,
P,
T
and
PolyRedRel P,
T reduces h,
c9
by A4, Lm5;
consider pp being
Polynomial of
n,
L such that
pp in P
and A6:
0_ n,
L reduces_to h,
pp,
T
by A5, POLYRED:def 7;
0_ n,
L is_reducible_wrt pp,
T
by A6, POLYRED:def 8;
hence
contradiction
by POLYRED:37;
verum end; hence
PolyRedRel P,
T reduces f,
0_ n,
L
by A3;
verum end;
hence
for f being Polynomial of n,L st f in P -Ideal holds
PolyRedRel P,T reduces f, 0_ n,L
; verum