let n be Ordinal; 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 f being Polynomial of n,L
for P being non empty Subset of (Polynom-Ring (n,L)) st PolyRedRel (P,T) reduces f, 0_ (n,L) holds
f has_a_Standard_Representation_of 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 f being Polynomial of n,L
for P being non empty Subset of (Polynom-Ring (n,L)) st PolyRedRel (P,T) reduces f, 0_ (n,L) holds
f has_a_Standard_Representation_of 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 f being Polynomial of n,L
for P being non empty Subset of (Polynom-Ring (n,L)) st PolyRedRel (P,T) reduces f, 0_ (n,L) holds
f has_a_Standard_Representation_of P,T
let f be Polynomial of n,L; for P being non empty Subset of (Polynom-Ring (n,L)) st PolyRedRel (P,T) reduces f, 0_ (n,L) holds
f has_a_Standard_Representation_of P,T
let P be non empty Subset of (Polynom-Ring (n,L)); ( PolyRedRel (P,T) reduces f, 0_ (n,L) implies f has_a_Standard_Representation_of P,T )
reconsider f9 = f as Element of (Polynom-Ring (n,L)) by POLYNOM1:def 11;
A1:
0_ (n,L) = 0. (Polynom-Ring (n,L))
by POLYNOM1:def 11;
assume
PolyRedRel (P,T) reduces f, 0_ (n,L)
; f has_a_Standard_Representation_of P,T
then consider A being LeftLinearCombination of P such that
A2:
f9 = (0. (Polynom-Ring (n,L))) + (Sum A)
and
A3:
for i being Element of NAT st i in dom A holds
ex m being non-zero Monomial of n,L ex p being non-zero Polynomial of n,L st
( p in P & A . i = m *' p & HT ((m *' p),T) <= HT (f,T),T )
by A1, Lm5;
A4:
now for i being Element of NAT st i in dom A holds
ex m being non-zero Monomial of n,L ex p being non-zero Polynomial of n,L st
( p in P & A /. i = m *' p & HT ((m *' p),T) <= HT (f,T),T )let i be
Element of
NAT ;
( i in dom A implies ex m being non-zero Monomial of n,L ex p being non-zero Polynomial of n,L st
( p in P & A /. i = m *' p & HT ((m *' p),T) <= HT (f,T),T ) )assume A5:
i in dom A
;
ex m being non-zero Monomial of n,L ex p being non-zero Polynomial of n,L st
( p in P & A /. i = m *' p & HT ((m *' p),T) <= HT (f,T),T )then
ex
m being
non-zero Monomial of
n,
L ex
p being
non-zero Polynomial of
n,
L st
(
p in P &
A . i = m *' p &
HT (
(m *' p),
T)
<= HT (
f,
T),
T )
by A3;
hence
ex
m being
non-zero Monomial of
n,
L ex
p being
non-zero Polynomial of
n,
L st
(
p in P &
A /. i = m *' p &
HT (
(m *' p),
T)
<= HT (
f,
T),
T )
by A5, PARTFUN1:def 6;
verum end;
f = Sum A
by A2, RLVECT_1:def 4;
then
A is_Standard_Representation_of f,P, HT (f,T),T
by A4;
then
A is_Standard_Representation_of f,P,T
;
hence
f has_a_Standard_Representation_of P,T
; verum