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 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; :: 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 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 ; :: thesis: 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); :: thesis: ( 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 )
assume A1:
PolyRedRel P,T is with_Church-Rosser_property
; :: thesis: 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;
now let f be
Polynomial of
n,
L;
:: thesis: ( f in P -Ideal implies PolyRedRel P,T reduces f, 0_ n,L )assume A2:
f in P -Ideal
;
:: thesis: PolyRedRel P,T reduces f, 0_ n,Lreconsider f' =
f as
Element of
(Polynom-Ring n,L) by POLYNOM1:def 27;
reconsider f' =
f' as
Element of
(Polynom-Ring n,L) ;
reconsider e =
0_ n,
L as
Element of
(Polynom-Ring n,L) by POLYNOM1:def 27;
reconsider e =
e as
Element of
(Polynom-Ring n,L) ;
f - (0_ n,L) = f' - e
by Lm2;
then
f' - e in P -Ideal
by A2, POLYRED:4;
then
f',
e are_congruent_mod P -Ideal
by POLYRED:def 14;
then
f',
e are_convertible_wrt PolyRedRel P,
T
by POLYRED:58;
then
f',
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 &
PolyRedRel P,
T reduces 0_ n,
L,
c )
by REWRITE1:def 7;
reconsider c' =
c as
Polynomial of
n,
L by A3, Lm4;
now assume
c' <> 0_ n,
L
;
:: thesis: contradictionthen consider h being
Polynomial of
n,
L such that A4:
(
0_ n,
L reduces_to h,
P,
T &
PolyRedRel P,
T reduces h,
c' )
by A3, Lm5;
consider pp being
Polynomial of
n,
L such that A5:
(
pp in P &
0_ n,
L reduces_to h,
pp,
T )
by A4, POLYRED:def 7;
0_ n,
L is_reducible_wrt pp,
T
by A5, POLYRED:def 8;
hence
contradiction
by POLYRED:37;
:: thesis: verum end; hence
PolyRedRel P,
T reduces f,
0_ n,
L
by A3;
:: thesis: verum end;
hence
for f being Polynomial of n,L st f in P -Ideal holds
PolyRedRel P,T reduces f, 0_ n,L
; :: thesis: verum