let n be Ordinal; :: thesis: for T being connected admissible TermOrder of n
for L being non trivial right_complementable almost_left_invertible associative commutative well-unital distributive add-associative right_zeroed 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 associative commutative well-unital distributive add-associative right_zeroed 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 associative commutative well-unital distributive add-associative right_zeroed 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 by Def10;
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 & i in dom A & A /. i = m *' p & HT f,T = HT (m *' p),T ) by A1, Th42;
A3: ( i in dom A & p <> 0_ n,L & p in P & A /. i = m *' p ) by A2, POLYNOM7:def 2;
A4: f <> 0_ n,L by POLYNOM7:def 2;
then Support f <> {} by POLYNOM7:1;
then A5: HT f,T in Support f by TERMORD:def 6;
set s = HT m,T;
set g = f - (((f . (HT f,T)) / (HC p,T)) * ((HT m,T) *' p));
HT f,T = (HT m,T) + (HT p,T) by A2, TERMORD:31;
then f reduces_to f - (((f . (HT f,T)) / (HC p,T)) * ((HT m,T) *' p)),p, HT f,T,T by A3, A4, A5, 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