environ
vocabularies HIDDEN, NUMBERS, ORDINAL1, RLVECT_1, ALGSTR_0, VECTSP_1, LATTICES, ZFMISC_1, POLYNOM1, SUBSET_1, STRUCT_0, RELAT_2, BAGORDER, BINOP_1, POLYRED, POLYNOM7, ARYTM_1, ARYTM_3, PRE_POLY, TERMORD, FUNCT_1, BROUWER, RELAT_1, XBOOLE_0, XXREAL_0, SUPINF_2, VALUED_0, XCMPLX_0, CAT_3, ALGSTR_1, IDEAL_1, FINSEQ_1, PARTFUN1, MESFUNC1, CARD_3, TARSKI, CARD_1, ORDERS_2, REWRITE1, INT_1, FUNCT_4, GROUP_1, ORDERS_1, DICKSON, RLVECT_2, FUNCOP_1, PBOOLE, FINSET_1, ORDINAL4, GROEB_1, NAT_1;
notations HIDDEN, TARSKI, RELAT_1, XBOOLE_0, RELAT_2, XCMPLX_0, XXREAL_0, RELSET_1, FUNCT_1, PARTFUN1, ORDINAL1, ALGSTR_0, ALGSTR_1, RLVECT_1, FINSET_1, FUNCT_7, DICKSON, CARD_3, CARD_1, SUBSET_1, XTUPLE_0, MCART_1, FINSEQ_1, YELLOW_1, ORDERS_1, PRALG_1, STRUCT_0, POLYNOM7, PBOOLE, FUNCOP_1, ORDERS_2, VFUNCT_1, POLYNOM1, IDEAL_1, REWRITE1, BAGORDER, VECTSP_1, TERMORD, GROUP_1, NUMBERS, NAT_1, PRE_POLY, POLYRED, RECDEF_1;
definitions TARSKI, RELAT_2, RELAT_1;
theorems TARSKI, RELSET_1, FINSEQ_1, RELAT_1, ZFMISC_1, VECTSP_1, POLYNOM1, RLVECT_1, NAT_1, ALGSTR_1, POLYNOM7, REWRITE1, XBOOLE_0, IDEAL_1, TERMORD, INT_1, FUNCT_1, ORDERS_2, FINSET_1, WELLORD2, XBOOLE_1, CARD_3, DICKSON, FUNCOP_1, PRALG_1, YELLOW_1, FUNCT_7, FUNCT_2, CARD_2, BAGORDER, ORDINAL1, VECTSP_2, POLYRED, RELAT_2, PARTFUN1, ORDERS_1, GROUP_1, XREAL_1, XXREAL_0, VALUED_0, STRUCT_0, PRE_POLY, XTUPLE_0, PBOOLE;
schemes RELSET_1, NAT_1, CLASSES1;
registrations XBOOLE_0, RELAT_1, ORDINAL1, FINSET_1, XREAL_0, NAT_1, INT_1, CARD_1, REWRITE1, STRUCT_0, VECTSP_1, ORDERS_2, ALGSTR_1, YELLOW_1, GCD_1, POLYNOM1, POLYNOM2, POLYNOM4, IDEAL_1, POLYNOM7, DICKSON, TERMORD, POLYRED, VALUED_0, ALGSTR_0, FINSEQ_1, SUBSET_1, PRE_POLY, FUNCOP_1, VFUNCT_1, FUNCT_1, FUNCT_2;
constructors HIDDEN, REWRITE1, VECTSP_2, PRALG_1, YELLOW_1, IDEAL_1, DICKSON, BAGORDER, TERMORD, POLYRED, RECDEF_1, DOMAIN_1, RELSET_1, PBOOLE, FUNCT_7, VFUNCT_1, XTUPLE_0;
requirements HIDDEN, NUMERALS, REAL, SUBSET, BOOLE, ARITHM;
equalities STRUCT_0, ALGSTR_0;
expansions TARSKI, RELAT_2, STRUCT_0;
theorem
for
n being
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,
p,
g being
Polynomial of
n,
L st
f reduces_to g,
p,
T holds
ex
m being
Monomial of
n,
L st
(
g = f - (m *' p) & not
HT (
(m *' p),
T)
in Support g &
HT (
(m *' p),
T)
<= HT (
f,
T),
T )
Lm1:
for L being non empty add-cancelable right_complementable well-unital distributive add-associative right_zeroed associative left_zeroed doubleLoopStr
for P being Subset of L
for p being Element of L st p in P holds
p in P -Ideal
Lm2:
for n being Ordinal
for T being connected admissible TermOrder of n
for L being non empty non degenerated right_complementable almost_left_invertible well-unital distributive add-associative right_zeroed associative commutative doubleLoopStr
for p, q being Polynomial of n,L
for f, g being Element of (Polynom-Ring (n,L)) st f = p & g = q holds
f - g = p - q
Lm3:
for n being Ordinal
for T being connected 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 Polynomial of n,L holds f is_irreducible_wrt 0_ (n,L),T
Lm4:
for n being Ordinal
for T being connected 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 Polynomial of n,L
for g being object
for P being Subset of (Polynom-Ring (n,L)) st PolyRedRel (P,T) reduces f,g holds
g is Polynomial of n,L
Lm5:
for n being Ordinal
for T being connected 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, g being Polynomial of n,L
for P being Subset of (Polynom-Ring (n,L)) st PolyRedRel (P,T) reduces f,g & g <> f holds
ex h being Polynomial of n,L st
( f reduces_to h,P,T & PolyRedRel (P,T) reduces h,g )
Lm6:
for n being Ordinal
for T being connected TermOrder of n
for L being non trivial right_complementable almost_left_invertible well-unital distributive add-associative right_zeroed associative commutative doubleLoopStr
for P being Subset of (Polynom-Ring (n,L))
for a, b being object st a <> b & PolyRedRel (P,T) reduces a,b holds
( a is Polynomial of n,L & b is Polynomial of n,L )
Lm7:
for n being Ordinal
for T being connected TermOrder of n
for L being non trivial right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative doubleLoopStr
for I being LeftIdeal of (Polynom-Ring (n,L))
for G being non empty Subset of (Polynom-Ring (n,L)) st G c= I & ( for f being Polynomial of n,L st f in I holds
PolyRedRel (G,T) reduces f, 0_ (n,L) ) holds
G -Ideal = I
Lm8:
for n being Ordinal
for b1, b2, b3 being bag of n st b1 divides b2 & b2 divides b3 holds
b1 divides b3
Lm9:
for L being non empty right_complementable well-unital distributive add-associative right_zeroed associative left_zeroed doubleLoopStr
for A, B being non empty Subset of L st B = A \ {(0. L)} holds
for f being LinearCombination of A
for u being set st u = Sum f holds
ex g being LinearCombination of B st u = Sum g
theorem Th37:
for
n being
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
I being
add-closed left-ideal Subset of
(Polynom-Ring (n,L)) for
m being
Monomial of
n,
L for
f,
g being
Polynomial of
n,
L st
f in I &
g in I &
HM (
f,
T)
= m &
HM (
g,
T)
= m & ( for
p being
Polynomial of
n,
L holds
( not
p in I or not
p < f,
T or not
HM (
p,
T)
= m ) ) & ( for
p being
Polynomial of
n,
L holds
( not
p in I or not
p < g,
T or not
HM (
p,
T)
= m ) ) holds
f = g
Lm10:
for n being 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 Polynomial of n,L
for I being non empty add-closed left-ideal Subset of (Polynom-Ring (n,L)) st p in I & p <> 0_ (n,L) holds
ex q being Polynomial of n,L st
( q in I & HM (q,T) = Monom ((1. L),(HT (p,T))) & q <> 0_ (n,L) )