let n be Nat; for T being connected admissible TermOrder of n
for L being non trivial right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative left_zeroed doubleLoopStr
for P being Subset of (Polynom-Ring (n,L))
for f, h being Polynomial of n,L st f in P holds
PolyRedRel (P,T) reduces h *' f, 0_ (n,L)
let T be connected admissible TermOrder of n; for L being non trivial right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative left_zeroed doubleLoopStr
for P being Subset of (Polynom-Ring (n,L))
for f, h being Polynomial of n,L st f in P holds
PolyRedRel (P,T) reduces h *' f, 0_ (n,L)
let L be non trivial right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative left_zeroed doubleLoopStr ; for P being Subset of (Polynom-Ring (n,L))
for f, h being Polynomial of n,L st f in P holds
PolyRedRel (P,T) reduces h *' f, 0_ (n,L)
let P be Subset of (Polynom-Ring (n,L)); for f, h being Polynomial of n,L st f in P holds
PolyRedRel (P,T) reduces h *' f, 0_ (n,L)
let f9, h9 be Polynomial of n,L; ( f9 in P implies PolyRedRel (P,T) reduces h9 *' f9, 0_ (n,L) )
assume A1:
f9 in P
; PolyRedRel (P,T) reduces h9 *' f9, 0_ (n,L)
per cases
( h9 = 0_ (n,L) or h9 <> 0_ (n,L) )
;
suppose
h9 <> 0_ (
n,
L)
;
PolyRedRel (P,T) reduces h9 *' f9, 0_ (n,L)then reconsider h =
h9 as
non-zero Polynomial of
n,
L by POLYNOM7:def 1;
set H =
{ g where g is Polynomial of n,L : not PolyRedRel (P,T) reduces g *' f9, 0_ (n,L) } ;
now ( ( f9 = 0_ (n,L) & PolyRedRel (P,T) reduces h9 *' f9, 0_ (n,L) ) or ( f9 <> 0_ (n,L) & ( not PolyRedRel (P,T) reduces h9 *' f9, 0_ (n,L) implies PolyRedRel (P,T) reduces h9 *' f9, 0_ (n,L) ) ) )per cases
( f9 = 0_ (n,L) or f9 <> 0_ (n,L) )
;
case
f9 <> 0_ (
n,
L)
;
( not PolyRedRel (P,T) reduces h9 *' f9, 0_ (n,L) implies PolyRedRel (P,T) reduces h9 *' f9, 0_ (n,L) )then reconsider f =
f9 as
non-zero Polynomial of
n,
L by POLYNOM7:def 1;
A2:
now for u being object st u in { g where g is Polynomial of n,L : not PolyRedRel (P,T) reduces g *' f9, 0_ (n,L) } holds
u in the carrier of (Polynom-Ring (n,L))let u be
object ;
( u in { g where g is Polynomial of n,L : not PolyRedRel (P,T) reduces g *' f9, 0_ (n,L) } implies u in the carrier of (Polynom-Ring (n,L)) )assume
u in { g where g is Polynomial of n,L : not PolyRedRel (P,T) reduces g *' f9, 0_ (n,L) }
;
u in the carrier of (Polynom-Ring (n,L))then
ex
g9 being
Polynomial of
n,
L st
(
u = g9 & not
PolyRedRel (
P,
T)
reduces g9 *' f,
0_ (
n,
L) )
;
hence
u in the
carrier of
(Polynom-Ring (n,L))
by POLYNOM1:def 11;
verum end; assume
not
PolyRedRel (
P,
T)
reduces h9 *' f9,
0_ (
n,
L)
;
PolyRedRel (P,T) reduces h9 *' f9, 0_ (n,L)then
h in { g where g is Polynomial of n,L : not PolyRedRel (P,T) reduces g *' f9, 0_ (n,L) }
;
then reconsider H =
{ g where g is Polynomial of n,L : not PolyRedRel (P,T) reduces g *' f9, 0_ (n,L) } as non
empty Subset of
(Polynom-Ring (n,L)) by A2, TARSKI:def 3;
now not H <> {} assume
H <> {}
;
contradictionreconsider H =
H as non
empty set ;
consider m being
Polynomial of
n,
L such that A3:
m in H
and A4:
for
m9 being
Polynomial of
n,
L st
m9 in H holds
m <= m9,
T
by Th31;
m <> 0_ (
n,
L)
then reconsider m =
m as
non-zero Polynomial of
n,
L by POLYNOM7:def 1;
Red (
m,
T)
< m,
T
by Th35;
then
not
m <= Red (
m,
T),
T
by Th29;
then
not
Red (
m,
T)
in H
by A4;
then A6:
PolyRedRel (
P,
T)
reduces (Red (m,T)) *' f,
0_ (
n,
L)
;
set g =
(m *' f) - ((((m *' f) . (HT ((m *' f),T))) / (HC (f,T))) * ((HT (m,T)) *' f));
A7:
m *' f <> 0_ (
n,
L)
by POLYNOM7:def 1;
A8:
HC (
f,
T)
<> 0. L
;
m *' f <> 0_ (
n,
L)
by POLYNOM7:def 1;
then
Support (m *' f) <> {}
by POLYNOM7:1;
then A9:
HT (
(m *' f),
T)
in Support (m *' f)
by TERMORD:def 6;
(((m *' f) . (HT ((m *' f),T))) / (HC (f,T))) * ((HT (m,T)) *' f) =
((HC ((m *' f),T)) / (HC (f,T))) * ((HT (m,T)) *' f)
by TERMORD:def 7
.=
(((HC (m,T)) * (HC (f,T))) / (HC (f,T))) * ((HT (m,T)) *' f)
by TERMORD:32
.=
(((HC (m,T)) * (HC (f,T))) * ((HC (f,T)) ")) * ((HT (m,T)) *' f)
.=
((HC (m,T)) * ((HC (f,T)) * ((HC (f,T)) "))) * ((HT (m,T)) *' f)
by GROUP_1:def 3
.=
((HC (m,T)) * (1. L)) * ((HT (m,T)) *' f)
by A8, VECTSP_1:def 10
.=
(HC (m,T)) * ((HT (m,T)) *' f)
.=
(Monom ((HC (m,T)),(HT (m,T)))) *' f
by Th22
.=
(HM (m,T)) *' f
by TERMORD:def 8
;
then A10:
(m *' f) - ((((m *' f) . (HT ((m *' f),T))) / (HC (f,T))) * ((HT (m,T)) *' f)) =
(m *' f) + (- ((HM (m,T)) *' f))
by POLYNOM1:def 7
.=
(f *' m) + (f *' (- (HM (m,T))))
by Th6
.=
(m + (- (HM (m,T)))) *' f
by POLYNOM1:26
.=
(m - (HM (m,T))) *' f
by POLYNOM1:def 7
.=
(Red (m,T)) *' f
by TERMORD:def 9
;
(
HT (
(m *' f),
T)
= (HT (m,T)) + (HT (f,T)) &
f <> 0_ (
n,
L) )
by POLYNOM7:def 1, TERMORD:31;
then
m *' f reduces_to (m *' f) - ((((m *' f) . (HT ((m *' f),T))) / (HC (f,T))) * ((HT (m,T)) *' f)),
f,
HT (
(m *' f),
T),
T
by A9, A7;
then
m *' f reduces_to (Red (m,T)) *' f,
f,
T
by A10;
then
m *' f reduces_to (Red (m,T)) *' f,
P,
T
by A1;
then
[(m *' f),((Red (m,T)) *' f)] in PolyRedRel (
P,
T)
by Def13;
then A11:
PolyRedRel (
P,
T)
reduces m *' f,
(Red (m,T)) *' f
by REWRITE1:15;
ex
u being
Polynomial of
n,
L st
(
m = u & not
PolyRedRel (
P,
T)
reduces u *' f,
0_ (
n,
L) )
by A3;
hence
contradiction
by A11, A6, REWRITE1:16;
verum end; hence
PolyRedRel (
P,
T)
reduces h9 *' f9,
0_ (
n,
L)
;
verum end; hence
PolyRedRel (
P,
T)
reduces h9 *' f9,
0_ (
n,
L)
;
verum end;