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 well-unital distributive Abelian 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_reducible_wrt P,T ) holds
for f being non-zero Polynomial of n,L st f in P -Ideal holds
f is_top_reducible_wrt P,T
let T be connected admissible TermOrder of n; for L being non empty non degenerated right_complementable almost_left_invertible well-unital distributive Abelian 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_reducible_wrt P,T ) holds
for f being non-zero Polynomial of n,L st f in P -Ideal holds
f is_top_reducible_wrt P,T
let L be non empty non degenerated right_complementable almost_left_invertible well-unital distributive Abelian 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_reducible_wrt P,T ) holds
for f being non-zero Polynomial of n,L st f in P -Ideal holds
f is_top_reducible_wrt P,T
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_reducible_wrt P,T ) implies for f being non-zero Polynomial of n,L st f in P -Ideal holds
f is_top_reducible_wrt P,T )
assume A1:
for f being non-zero Polynomial of n,L st f in P -Ideal holds
f is_reducible_wrt P,T
; for f being non-zero Polynomial of n,L st f in P -Ideal holds
f is_top_reducible_wrt P,T
thus
for f being non-zero Polynomial of n,L st f in P -Ideal holds
f is_top_reducible_wrt P,T
verumproof
set H =
{ g where g is non-zero Polynomial of n,L : ( g in P -Ideal & not g is_top_reducible_wrt P,T ) } ;
let f be
non-zero Polynomial of
n,
L;
( f in P -Ideal implies f is_top_reducible_wrt P,T )
assume A2:
f in P -Ideal
;
f is_top_reducible_wrt P,T
assume
not
f is_top_reducible_wrt P,
T
;
contradiction
then A3:
f in { g where g is non-zero Polynomial of n,L : ( g in P -Ideal & not g is_top_reducible_wrt P,T ) }
by A2;
then reconsider H =
{ g where g is non-zero Polynomial of n,L : ( g in P -Ideal & not g is_top_reducible_wrt P,T ) } as non
empty Subset of
(Polynom-Ring (n,L)) by A3, TARSKI:def 3;
consider p being
Polynomial of
n,
L such that A4:
p in H
and A5:
for
q being
Polynomial of
n,
L st
q in H holds
p <= q,
T
by POLYRED:31;
A6:
ex
p9 being
non-zero Polynomial of
n,
L st
(
p9 = p &
p9 in P -Ideal & not
p9 is_top_reducible_wrt P,
T )
by A4;
then reconsider p =
p as
non-zero Polynomial of
n,
L ;
p is_reducible_wrt P,
T
by A1, A6;
then consider q being
Polynomial of
n,
L such that A7:
p reduces_to q,
P,
T
by POLYRED:def 9;
consider u being
Polynomial of
n,
L such that A8:
u in P
and A9:
p reduces_to q,
u,
T
by A7, POLYRED:def 7;
ex
b being
bag of
n st
p reduces_to q,
u,
b,
T
by A9, POLYRED:def 6;
then A10:
u <> 0_ (
n,
L)
by POLYRED:def 5;
then reconsider u =
u as
non-zero Polynomial of
n,
L by POLYNOM7:def 1;
consider b being
bag of
n such that A11:
p reduces_to q,
u,
b,
T
by A9, POLYRED:def 6;
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 11;
reconsider uu =
uu,
pp =
pp,
mm =
mm as
Element of
(Polynom-Ring (n,L)) ;
uu in P -Ideal
by A8, Lm1;
then
mm * uu in P -Ideal
by IDEAL_1:def 2;
then
- (mm * uu) in P -Ideal
by IDEAL_1:13;
then A14:
pp + (- (mm * uu)) in P -Ideal
by A6, IDEAL_1:def 1;
mm * uu = m *' u
by POLYNOM1:def 11;
then
p - (m *' u) = pp - (mm * uu)
by Lm2;
then A15:
q in P -Ideal
by A13, A14;
A16:
q < p,
T
by A9, POLYRED:43;
A17:
p <> 0_ (
n,
L)
by POLYNOM7:def 1;
then
Support p <> {}
by POLYNOM7:1;
then A18:
HT (
p,
T)
in Support p
by TERMORD:def 6;
b in Support p
by A11, POLYRED:def 5;
then
b <= HT (
p,
T),
T
by TERMORD:def 6;
then
b < HT (
p,
T),
T
by A12, TERMORD:def 3;
then A19:
HT (
p,
T)
in Support q
by A18, A11, POLYRED:40;
now ( ( q <> 0_ (n,L) & contradiction ) or ( q = 0_ (n,L) & contradiction ) )per cases
( q <> 0_ (n,L) or q = 0_ (n,L) )
;
case A20:
q <> 0_ (
n,
L)
;
contradictionthen reconsider q =
q as
non-zero Polynomial of
n,
L by POLYNOM7:def 1;
Support q <> {}
by A20, POLYNOM7:1;
then
HT (
q,
T)
in Support q
by TERMORD:def 6;
then A21:
HT (
q,
T)
<= HT (
p,
T),
T
by A9, POLYRED:42;
HT (
p,
T)
<= HT (
q,
T),
T
by A19, TERMORD:def 6;
then A22:
HT (
q,
T)
= HT (
p,
T)
by A21, TERMORD:7;
then consider u9 being
Polynomial of
n,
L such that A23:
u9 in P
and A24:
q is_top_reducible_wrt u9,
T
by POLYRED:def 12;
consider q9 being
Polynomial of
n,
L such that A25:
q top_reduces_to q9,
u9,
T
by A24, POLYRED:def 11;
A26:
p <> 0_ (
n,
L)
by POLYNOM7:def 1;
then
Support p <> {}
by POLYNOM7:1;
then A27:
HT (
p,
T)
in Support p
by TERMORD:def 6;
A28:
q reduces_to q9,
u9,
HT (
q,
T),
T
by A25, POLYRED:def 10;
then consider s being
bag of
n such that A29:
s + (HT (u9,T)) = HT (
q,
T)
and
q9 = q - (((q . (HT (q,T))) / (HC (u9,T))) * (s *' u9))
by POLYRED:def 5;
set qq =
p - (((p . (HT (p,T))) / (HC (u9,T))) * (s *' u9));
u9 <> 0_ (
n,
L)
by A28, POLYRED:def 5;
then
p reduces_to p - (((p . (HT (p,T))) / (HC (u9,T))) * (s *' u9)),
u9,
HT (
p,
T),
T
by A22, A29, A26, A27, POLYRED:def 5;
then
p top_reduces_to p - (((p . (HT (p,T))) / (HC (u9,T))) * (s *' u9)),
u9,
T
by POLYRED:def 10;
then
p is_top_reducible_wrt u9,
T
by POLYRED:def 11;
hence
contradiction
by A6, A23, POLYRED:def 12;
verum end; case
q = 0_ (
n,
L)
;
contradictionthen A30:
m *' u =
(p - (m *' u)) + (m *' u)
by A13, POLYRED:2
.=
(p + (- (m *' u))) + (m *' u)
by POLYNOM1:def 7
.=
p + ((- (m *' u)) + (m *' u))
by POLYNOM1:21
.=
p + (0_ (n,L))
by POLYRED:3
.=
p
by POLYNOM1:23
;
m <> 0_ (
n,
L)
by POLYNOM7:def 1, A30, POLYRED:5;
then reconsider m =
m as
non-zero Polynomial of
n,
L by POLYNOM7:def 1;
set pp =
p - (((p . (HT (p,T))) / (HC (u,T))) * ((HT (m,T)) *' u));
HT (
p,
T)
= (HT (m,T)) + (HT (u,T))
by A30, TERMORD:31;
then
p reduces_to p - (((p . (HT (p,T))) / (HC (u,T))) * ((HT (m,T)) *' u)),
u,
HT (
p,
T),
T
by A10, A17, A18, 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 A6, A8, POLYRED:def 12;
verum end;
hence
contradiction
;
verum
end;