let n be Ordinal; :: thesis: for T being connected admissible TermOrder of n
for L being non trivial right_complementable almost_left_invertible well-unital distributive add-associative right_zeroed associative commutative doubleLoopStr
for f being non-zero Polynomial of n,L
for P being non empty Subset of (Polynom-Ring (n,L)) st f has_a_Standard_Representation_of P,T holds
f is_top_reducible_wrt P,T
let T be connected admissible TermOrder of n; :: thesis: for L being non trivial right_complementable almost_left_invertible well-unital distributive add-associative right_zeroed associative commutative doubleLoopStr
for f being non-zero Polynomial of n,L
for P being non empty Subset of (Polynom-Ring (n,L)) st f has_a_Standard_Representation_of P,T holds
f is_top_reducible_wrt P,T
let L be non trivial right_complementable almost_left_invertible well-unital distributive add-associative right_zeroed associative commutative doubleLoopStr ; :: thesis: for f being non-zero Polynomial of n,L
for P being non empty Subset of (Polynom-Ring (n,L)) st f has_a_Standard_Representation_of P,T holds
f is_top_reducible_wrt P,T
let f be non-zero Polynomial of n,L; :: thesis: for P being non empty Subset of (Polynom-Ring (n,L)) st f has_a_Standard_Representation_of P,T holds
f is_top_reducible_wrt P,T
let P be non empty Subset of (Polynom-Ring (n,L)); :: thesis: ( f has_a_Standard_Representation_of P,T implies f is_top_reducible_wrt P,T )
assume f has_a_Standard_Representation_of P,T ; :: thesis: f is_top_reducible_wrt P,T
then consider A being LeftLinearCombination of P such that
A1: A is_Standard_Representation_of f,P,T ;
consider i being Element of NAT , m being non-zero Monomial of n,L, p being non-zero Polynomial of n,L such that
A2: p in P and
i in dom A and
A /. i = m *' p and
A3: HT (f,T) = HT ((m *' p),T) by A1, Th37;
set s = HT (m,T);
A4: HT (f,T) = (HT (m,T)) + (HT (p,T)) by A3, TERMORD:31;
set g = f - (((f . (HT (f,T))) / (HC (p,T))) * ((HT (m,T)) *' p));
A5: f <> 0_ (n,L) by POLYNOM7:def 1;
then Support f <> {} by POLYNOM7:1;
then ( p <> 0_ (n,L) & HT (f,T) in Support f ) by POLYNOM7:def 1, TERMORD:def 6;
then f reduces_to f - (((f . (HT (f,T))) / (HC (p,T))) * ((HT (m,T)) *' p)),p, HT (f,T),T by A5, A4, POLYRED:def 5;
then f top_reduces_to f - (((f . (HT (f,T))) / (HC (p,T))) * ((HT (m,T)) *' p)),p,T by POLYRED:def 10;
then f is_top_reducible_wrt p,T by POLYRED:def 11;
hence f is_top_reducible_wrt P,T by A2, POLYRED:def 12; :: thesis: verum