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 Polynomial of n,L st f in P -Ideal holds
PolyRedRel (P,T) reduces f, 0_ (n,L) ) holds
for f being non-zero Polynomial of n,L st f in P -Ideal holds
f is_reducible_wrt P,T
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 Polynomial of n,L st f in P -Ideal holds
PolyRedRel (P,T) reduces f, 0_ (n,L) ) holds
for f being non-zero Polynomial of n,L st f in P -Ideal holds
f is_reducible_wrt P,T
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 Polynomial of n,L st f in P -Ideal holds
PolyRedRel (P,T) reduces f, 0_ (n,L) ) holds
for f being non-zero Polynomial of n,L st f in P -Ideal holds
f is_reducible_wrt P,T
let P be Subset of (Polynom-Ring (n,L)); ( ( for f being Polynomial of n,L st f in P -Ideal holds
PolyRedRel (P,T) reduces f, 0_ (n,L) ) implies for f being non-zero Polynomial of n,L st f in P -Ideal holds
f is_reducible_wrt P,T )
assume A1:
for f being Polynomial of n,L st f in P -Ideal holds
PolyRedRel (P,T) reduces f, 0_ (n,L)
; for f being non-zero Polynomial of n,L st f in P -Ideal holds
f is_reducible_wrt P,T
now for f being non-zero Polynomial of n,L st f in P -Ideal holds
f is_reducible_wrt P,Tlet f be
non-zero Polynomial of
n,
L;
( f in P -Ideal implies f is_reducible_wrt P,T )assume
f in P -Ideal
;
f is_reducible_wrt P,Tthen A2:
PolyRedRel (
P,
T)
reduces f,
0_ (
n,
L)
by A1;
f <> 0_ (
n,
L)
by POLYNOM7:def 1;
then
ex
g being
Polynomial of
n,
L st
(
f reduces_to g,
P,
T &
PolyRedRel (
P,
T)
reduces g,
0_ (
n,
L) )
by A2, Lm5;
hence
f is_reducible_wrt P,
T
by POLYRED:def 9;
verum end;
hence
for f being non-zero Polynomial of n,L st f in P -Ideal holds
f is_reducible_wrt P,T
; verum