:: GROEB_3 semantic presentation

theorem Th1: :: GROEB_3:1

for b₁ being set
for b₂, b₃ being bag of b₁ holds (b₂ + b₃) / b₃ = b₂

proof end;

theorem Th2: :: GROEB_3:2

for b₁ being Ordinal
for b₂ being admissible TermOrder of b₁
for b₃, b₄, b₅ being bag of b₁ st b₃ <= b₄,b₂ holds
b₃ + b₅ <= b₄ + b₅,b₂

proof end;

theorem Th3: :: GROEB_3:3

for b₁ being Ordinal
for b₂ being TermOrder of b₁
for b₃, b₄, b₅ being bag of b₁ st b₃ <= b₄,b₂ & b₄ < b₅,b₂ holds
b₃ < b₅,b₂

proof end;

theorem Th4: :: GROEB_3:4

for b₁ being Ordinal
for b₂ being admissible TermOrder of b₁
for b₃, b₄, b₅ being bag of b₁ st b₃ < b₄,b₂ holds
b₃ + b₅ < b₄ + b₅,b₂

proof end;

theorem Th5: :: GROEB_3:5

for b₁ being Ordinal
for b₂ being admissible TermOrder of b₁
for b₃, b₄, b₅, b₆ being bag of b₁ st b₃ < b₄,b₂ & b₅ <= b₆,b₂ holds
b₃ + b₅ < b₄ + b₆,b₂

proof end;

theorem Th6: :: GROEB_3:6

for b₁ being Ordinal
for b₂ being admissible TermOrder of b₁
for b₃, b₄, b₅, b₆ being bag of b₁ st b₃ <= b₄,b₂ & b₅ < b₆,b₂ holds
b₃ + b₅ < b₄ + b₆,b₂

proof end;

theorem Th7: :: GROEB_3:7

for b₁ being Ordinal
for b₂ being add-associative right_zeroed right_complementable unital distributive non trivial domRing-like doubleLoopStr
for b₃, b₄ being non-zero Monomial of b₁,b₂ holds term (b₃ *' b₄) = (term b₃) + (term b₄)

proof end;

theorem Th8: :: GROEB_3:8

for b₁ being Ordinal
for b₂ being add-associative right_zeroed right_complementable unital distributive non trivial domRing-like doubleLoopStr
for b₃ being Polynomial of b₁,b₂
for b₄ being non-zero Monomial of b₁,b₂
for b₅ being bag of b₁ holds
( b₅ in Support b₃ iff (term b₄) + b₅ in Support (b₄ *' b₃) )

proof end;

theorem Th9: :: GROEB_3:9

for b₁ being Ordinal
for b₂ being add-associative right_zeroed right_complementable unital distributive non trivial domRing-like doubleLoopStr
for b₃ being Polynomial of b₁,b₂
for b₄ being non-zero Monomial of b₁,b₂ holds Support (b₄ *' b₃) = { ((term b₄) + b₅) where B is Element of Bags b₁ : b₅ in Support b₃ }

proof end;

theorem Th10: :: GROEB_3:10

for b₁ being Ordinal
for b₂ being add-associative right_zeroed right_complementable unital distributive non trivial left_zeroed domRing-like doubleLoopStr
for b₃ being Polynomial of b₁,b₂
for b₄ being non-zero Monomial of b₁,b₂ holds card (Support b₃) = card (Support (b₄ *' b₃))

proof end;

Lemma11: for b₁ being Ordinal
for b₂ being connected TermOrder of b₁
for b₃ being add-associative right_zeroed right_complementable associative commutative right_unital distributive left_unital Field-like non trivial doubleLoopStr
for b₄ being Polynomial of b₁,b₃
for b₅ being set
for b₆ being Subset of (Polynom-Ring b₁,b₃) st PolyRedRel b₆,b₂ reduces b₄,b₅ holds
b₅ is Polynomial of b₁,b₃

proof end;

theorem Th11: :: GROEB_3:11

for b₁ being Ordinal
for b₂ being connected TermOrder of b₁
for b₃ being add-associative right_zeroed right_complementable non trivial LoopStr holds Red (0_ b₁,b₃),b₂ = 0_ b₁,b₃

proof end;

theorem Th12: :: GROEB_3:12

for b₁ being Ordinal
for b₂ being Abelian add-associative right_zeroed right_complementable unital commutative distributive non trivial doubleLoopStr
for b₃, b₄ being Polynomial of b₁,b₂ st b₃ - b₄ = 0_ b₁,b₂ holds
b₃ = b₄

proof end;

theorem Th13: :: GROEB_3:13

for b₁ being set
for b₂ being non empty add-associative right_zeroed right_complementable LoopStr holds - (0_ b₁,b₂) = 0_ b₁,b₂

proof end;

theorem Th14: :: GROEB_3:14

for b₁ being set
for b₂ being non empty add-associative right_zeroed right_complementable LoopStr
for b₃ being Series of b₁,b₂ holds (0_ b₁,b₂) - b₃ = - b₃

proof end;

theorem Th15: :: GROEB_3:15

for b₁ being Ordinal
for b₂ being connected TermOrder of b₁
for b₃ being add-associative right_zeroed right_complementable non trivial doubleLoopStr
for b₄ being Polynomial of b₁,b₃ holds b₄ - (Red b₄,b₂) = HM b₄,b₂

proof end;

registration

let c₁ be Ordinal;
let c₂ be non empty add-associative right_zeroed right_complementable LoopStr ;
let c₃ be Polynomial of c₁,c₂;
cluster Support a₃ -> finite ;
coherence by POLYNOM1:def 10;

end;

definition

let c₁ be Ordinal;
let c₂ be add-associative right_zeroed right_complementable unital distributive non trivial doubleLoopStr ;
let c₃, c₄ be Polynomial of c₁,c₂;
redefine func { as {c₃,c₄} -> non empty finite Subset of (Polynom-Ring a₁,a₂);
coherence

proof end;

end;

definition

let c₁ be set ;
let c₂ be non empty ZeroStr ;
let c₃ be Series of c₁,c₂;
let c₄ be Subset of (Bags c₁);
func c₃ | c₄ -> Series of a₁,a₂ equals :: GROEB_3:def 1
a₃ +* (((Support a₃) \ a₄) --> (0. a₂));
coherence

proof end;

end;

:: deftheorem Def1 defines | GROEB_3:def 1 :

Lemma17: for b₁ being set
for b₂ being non empty ZeroStr
for b₃ being Series of b₁,b₂
for b₄ being Subset of (Bags b₁) holds Support (b₃ | b₄) c= Support b₃

proof end;

registration

let c₁ be Ordinal;
let c₂ be non empty ZeroStr ;
let c₃ be Polynomial of c₁,c₂;
let c₄ be Subset of (Bags c₁);
cluster a₃ | a₄ -> finite-Support ;
coherence

proof end;

end;

theorem Th16: :: GROEB_3:16

for b₁ being set
for b₂ being non empty ZeroStr
for b₃ being Series of b₁,b₂
for b₄ being Subset of (Bags b₁) holds
( Support (b₃ | b₄) = (Support b₃) /\ b₄ & ( for b₅ being bag of b₁ st b₅ in Support (b₃ | b₄) holds
(b₃ | b₄) . b₅ = b₃ . b₅ ) )

proof end;

theorem Th17: :: GROEB_3:17

for b₁ being set
for b₂ being non empty ZeroStr
for b₃ being Series of b₁,b₂
for b₄ being Subset of (Bags b₁) holds Support (b₃ | b₄) c= Support b₃ by Lemma17;

theorem Th18: :: GROEB_3:18

for b₁ being set
for b₂ being non empty ZeroStr
for b₃ being Series of b₁,b₂ holds
( b₃ | (Support b₃) = b₃ & b₃ | ({} (Bags b₁)) = 0_ b₁,b₂ )

proof end;

definition

let c₁ be Ordinal;
let c₂ be connected TermOrder of c₁;
let c₃ be non empty add-associative right_zeroed right_complementable LoopStr ;
let c₄ be Polynomial of c₁,c₃;
let c₅ be Nat;
assume E19: c₅ <= card (Support c₄) ;
func Upper_Support c₄,c₂,c₅ -> finite Subset of (Bags a₁) means :Def2: :: GROEB_3:def 2
( a₆ c= Support a₄ & card a₆ = a₅ & ( for b₁, b₂ being bag of a₁ st b₁ in a₆ & b₂ in Support a₄ & b₁ <= b₂,a₂ holds
b₂ in a₆ ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def2 defines Upper_Support GROEB_3:def 2 :

definition

let c₁ be Ordinal;
let c₂ be connected TermOrder of c₁;
let c₃ be non empty add-associative right_zeroed right_complementable LoopStr ;
let c₄ be Polynomial of c₁,c₃;
let c₅ be Nat;
func Lower_Support c₄,c₂,c₅ -> finite Subset of (Bags a₁) equals :: GROEB_3:def 3
(Support a₄) \ (Upper_Support a₄,a₂,a₅);
coherence

proof end;

end;

:: deftheorem Def3 defines Lower_Support GROEB_3:def 3 :

Lemma20: for b₁ being Ordinal
for b₂ being connected TermOrder of b₁
for b₃ being non empty add-associative right_zeroed right_complementable LoopStr
for b₄ being Polynomial of b₁,b₃
for b₅ being Nat st b₅ <= card (Support b₄) holds
Lower_Support b₄,b₂,b₅ c= Support b₄
by XBOOLE_1:36;

theorem Th19: :: GROEB_3:19

for b₁ being Ordinal
for b₂ being connected TermOrder of b₁
for b₃ being non empty add-associative right_zeroed right_complementable LoopStr
for b₄ being Polynomial of b₁,b₃
for b₅ being Nat st b₅ <= card (Support b₄) holds
( (Upper_Support b₄,b₂,b₅) \/ (Lower_Support b₄,b₂,b₅) = Support b₄ & (Upper_Support b₄,b₂,b₅) /\ (Lower_Support b₄,b₂,b₅) = {} )

proof end;

theorem Th20: :: GROEB_3:20

for b₁ being Ordinal
for b₂ being connected TermOrder of b₁
for b₃ being non empty add-associative right_zeroed right_complementable LoopStr
for b₄ being Polynomial of b₁,b₃
for b₅ being Nat st b₅ <= card (Support b₄) holds
for b₆, b₇ being bag of b₁ st b₆ in Upper_Support b₄,b₂,b₅ & b₇ in Lower_Support b₄,b₂,b₅ holds
b₇ < b₆,b₂

proof end;

theorem Th21: :: GROEB_3:21

for b₁ being Ordinal
for b₂ being connected TermOrder of b₁
for b₃ being non empty add-associative right_zeroed right_complementable LoopStr
for b₄ being Polynomial of b₁,b₃ holds
( Upper_Support b₄,b₂,0 = {} & Lower_Support b₄,b₂,0 = Support b₄ )

proof end;

theorem Th22: :: GROEB_3:22

for b₁ being Ordinal
for b₂ being connected TermOrder of b₁
for b₃ being non empty add-associative right_zeroed right_complementable LoopStr
for b₄ being Polynomial of b₁,b₃ holds
( Upper_Support b₄,b₂,(card (Support b₄)) = Support b₄ & Lower_Support b₄,b₂,(card (Support b₄)) = {} )

proof end;

theorem Th23: :: GROEB_3:23

for b₁ being Ordinal
for b₂ being connected TermOrder of b₁
for b₃ being add-associative right_zeroed right_complementable non trivial LoopStr
for b₄ being non-zero Polynomial of b₁,b₃
for b₅ being Nat st 1 <= b₅ & b₅ <= card (Support b₄) holds
HT b₄,b₂ in Upper_Support b₄,b₂,b₅

proof end;

theorem Th24: :: GROEB_3:24

for b₁ being Ordinal
for b₂ being connected TermOrder of b₁
for b₃ being non empty add-associative right_zeroed right_complementable LoopStr
for b₄ being Polynomial of b₁,b₃
for b₅ being Nat st b₅ <= card (Support b₄) holds
( Lower_Support b₄,b₂,b₅ c= Support b₄ & card (Lower_Support b₄,b₂,b₅) = (card (Support b₄)) - b₅ & ( for b₆, b₇ being bag of b₁ st b₆ in Lower_Support b₄,b₂,b₅ & b₇ in Support b₄ & b₇ <= b₆,b₂ holds
b₇ in Lower_Support b₄,b₂,b₅ ) )

proof end;

definition

let c₁ be Ordinal;
let c₂ be connected TermOrder of c₁;
let c₃ be non empty add-associative right_zeroed right_complementable LoopStr ;
let c₄ be Polynomial of c₁,c₃;
let c₅ be Nat;
func Up c₄,c₂,c₅ -> Polynomial of a₁,a₃ equals :: GROEB_3:def 4
a₄ | (Upper_Support a₄,a₂,a₅);
coherence ;
func Low c₄,c₂,c₅ -> Polynomial of a₁,a₃ equals :: GROEB_3:def 5
a₄ | (Lower_Support a₄,a₂,a₅);
coherence ;

end;

:: deftheorem Def4 defines Up GROEB_3:def 4 :

:: deftheorem Def5 defines Low GROEB_3:def 5 :

Lemma26: for b₁ being Ordinal
for b₂ being connected TermOrder of b₁
for b₃ being non empty add-associative right_zeroed right_complementable LoopStr
for b₄ being Polynomial of b₁,b₃
for b₅ being Nat st b₅ <= card (Support b₄) holds
( Support (b₄ | (Upper_Support b₄,b₂,b₅)) = Upper_Support b₄,b₂,b₅ & Support (b₄ | (Lower_Support b₄,b₂,b₅)) = Lower_Support b₄,b₂,b₅ )

proof end;

theorem Th25: :: GROEB_3:25

for b₁ being Ordinal
for b₂ being connected TermOrder of b₁
for b₃ being non empty add-associative right_zeroed right_complementable LoopStr
for b₄ being Polynomial of b₁,b₃
for b₅ being Nat st b₅ <= card (Support b₄) holds
( Support (Up b₄,b₂,b₅) = Upper_Support b₄,b₂,b₅ & Support (Low b₄,b₂,b₅) = Lower_Support b₄,b₂,b₅ ) by Lemma26;

theorem Th26: :: GROEB_3:26

proof end;

theorem Th27: :: GROEB_3:27

for b₁ being Ordinal
for b₂ being connected TermOrder of b₁
for b₃ being add-associative right_zeroed right_complementable non trivial LoopStr
for b₄ being Polynomial of b₁,b₃
for b₅ being Nat st 1 <= b₅ & b₅ <= card (Support b₄) holds
Support (Low b₄,b₂,b₅) c= Support (Red b₄,b₂)

proof end;

theorem Th28: :: GROEB_3:28

for b₁ being Ordinal
for b₂ being connected TermOrder of b₁
for b₃ being non empty add-associative right_zeroed right_complementable LoopStr
for b₄ being Polynomial of b₁,b₃
for b₅ being Nat st b₅ <= card (Support b₄) holds
for b₆ being bag of b₁ st b₆ in Support b₄ holds
( ( b₆ in Support (Up b₄,b₂,b₅) or b₆ in Support (Low b₄,b₂,b₅) ) & not b₆ in (Support (Up b₄,b₂,b₅)) /\ (Support (Low b₄,b₂,b₅)) )

proof end;

theorem Th29: :: GROEB_3:29

for b₁ being Ordinal
for b₂ being connected TermOrder of b₁
for b₃ being non empty add-associative right_zeroed right_complementable LoopStr
for b₄ being Polynomial of b₁,b₃
for b₅ being Nat st b₅ <= card (Support b₄) holds
for b₆, b₇ being bag of b₁ st b₆ in Support (Low b₄,b₂,b₅) & b₇ in Support (Up b₄,b₂,b₅) holds
b₆ < b₇,b₂

proof end;

theorem Th30: :: GROEB_3:30

proof end;

theorem Th31: :: GROEB_3:31

for b₁ being Ordinal
for b₂ being connected TermOrder of b₁
for b₃ being non empty add-associative right_zeroed right_complementable LoopStr
for b₄ being Polynomial of b₁,b₃
for b₅ being Nat st b₅ <= card (Support b₄) holds
for b₆ being bag of b₁ st b₆ in Support (Low b₄,b₂,b₅) holds
( (Low b₄,b₂,b₅) . b₆ = b₄ . b₆ & (Up b₄,b₂,b₅) . b₆ = 0. b₃ )

proof end;

theorem Th32: :: GROEB_3:32

for b₁ being Ordinal
for b₂ being connected TermOrder of b₁
for b₃ being non empty add-associative right_zeroed right_complementable LoopStr
for b₄ being Polynomial of b₁,b₃
for b₅ being Nat st b₅ <= card (Support b₄) holds
for b₆ being bag of b₁ st b₆ in Support (Up b₄,b₂,b₅) holds
( (Up b₄,b₂,b₅) . b₆ = b₄ . b₆ & (Low b₄,b₂,b₅) . b₆ = 0. b₃ )

proof end;

theorem Th33: :: GROEB_3:33

proof end;

theorem Th34: :: GROEB_3:34

for b₁ being Ordinal
for b₂ being connected TermOrder of b₁
for b₃ being non empty add-associative right_zeroed right_complementable LoopStr
for b₄ being Polynomial of b₁,b₃ holds
( Up b₄,b₂,0 = 0_ b₁,b₃ & Low b₄,b₂,0 = b₄ )

proof end;

theorem Th35: :: GROEB_3:35

for b₁ being Ordinal
for b₂ being connected TermOrder of b₁
for b₃ being non empty Abelian add-associative right_zeroed right_complementable doubleLoopStr
for b₄ being Polynomial of b₁,b₃ holds
( Up b₄,b₂,(card (Support b₄)) = b₄ & Low b₄,b₂,(card (Support b₄)) = 0_ b₁,b₃ )

proof end;

theorem Th36: :: GROEB_3:36

for b₁ being Ordinal
for b₂ being connected TermOrder of b₁
for b₃ being Abelian add-associative right_zeroed right_complementable non trivial doubleLoopStr
for b₄ being non-zero Polynomial of b₁,b₃ holds
( Up b₄,b₂,1 = HM b₄,b₂ & Low b₄,b₂,1 = Red b₄,b₂ )

proof end;

registration

let c₁ be Ordinal;
let c₂ be connected TermOrder of c₁;
let c₃ be add-associative right_zeroed right_complementable non trivial LoopStr ;
let c₄ be non-zero Polynomial of c₁,c₃;
cluster Up a₄,a₂,0 -> monomial-like ;
coherence

proof end;

end;

registration

let c₁ be Ordinal;
let c₂ be connected TermOrder of c₁;
let c₃ be Abelian add-associative right_zeroed right_complementable non trivial doubleLoopStr ;
let c₄ be non-zero Polynomial of c₁,c₃;
cluster Up a₄,a₂,1 -> non-zero monomial-like ;
coherence

proof end;

cluster Low a₄,a₂,(card (Support a₄)) -> monomial-like ;
coherence

proof end;

end;

theorem Th37: :: GROEB_3:37

for b₁ being Ordinal
for b₂ being connected TermOrder of b₁
for b₃ being add-associative right_zeroed right_complementable non trivial LoopStr
for b₄ being Polynomial of b₁,b₃
for b₅ being Nat st b₅ = (card (Support b₄)) - 1 holds
Low b₄,b₂,b₅ is non-zero Monomial of b₁,b₃

proof end;

theorem Th38: :: GROEB_3:38

for b₁ being Ordinal
for b₂ being connected admissible TermOrder of b₁
for b₃ being non empty add-associative right_zeroed right_complementable LoopStr
for b₄ being Polynomial of b₁,b₃
for b₅ being Nat st b₅ < card (Support b₄) holds
HT (Low b₄,b₂,(b₅ + 1)),b₂ <= HT (Low b₄,b₂,b₅),b₂,b₂

proof end;

theorem Th39: :: GROEB_3:39

proof end;

theorem Th40: :: GROEB_3:40

for b₁ being Ordinal
for b₂ being connected admissible TermOrder of b₁
for b₃ being add-associative right_zeroed right_complementable unital distributive non trivial domRing-like doubleLoopStr
for b₄ being Polynomial of b₁,b₃
for b₅ being non-zero Monomial of b₁,b₃
for b₆ being Nat st b₆ <= card (Support b₄) holds
for b₇ being bag of b₁ holds
( (term b₅) + b₇ in Support (Low (b₅ *' b₄),b₂,b₆) iff b₇ in Support (Low b₄,b₂,b₆) )

proof end;

theorem Th41: :: GROEB_3:41

for b₁ being Ordinal
for b₂ being connected admissible TermOrder of b₁
for b₃ being non empty add-associative right_zeroed right_complementable LoopStr
for b₄ being Polynomial of b₁,b₃
for b₅ being Nat st b₅ < card (Support b₄) holds
Support (Low b₄,b₂,(b₅ + 1)) c= Support (Low b₄,b₂,b₅)

proof end;

theorem Th42: :: GROEB_3:42

for b₁ being Ordinal
for b₂ being connected admissible TermOrder of b₁
for b₃ being non empty add-associative right_zeroed right_complementable LoopStr
for b₄ being Polynomial of b₁,b₃
for b₅ being Nat st b₅ < card (Support b₄) holds
(Support (Low b₄,b₂,b₅)) \ (Support (Low b₄,b₂,(b₅ + 1))) = {(HT (Low b₄,b₂,b₅),b₂)}

proof end;

theorem Th43: :: GROEB_3:43

for b₁ being Ordinal
for b₂ being connected admissible TermOrder of b₁
for b₃ being add-associative right_zeroed right_complementable non trivial LoopStr
for b₄ being Polynomial of b₁,b₃
for b₅ being Nat st b₅ < card (Support b₄) holds
Low b₄,b₂,(b₅ + 1) = Red (Low b₄,b₂,b₅),b₂

proof end;

theorem Th44: :: GROEB_3:44

for b₁ being Ordinal
for b₂ being connected admissible TermOrder of b₁
for b₃ being add-associative right_zeroed right_complementable unital distributive non trivial domRing-like doubleLoopStr
for b₄ being Polynomial of b₁,b₃
for b₅ being non-zero Monomial of b₁,b₃
for b₆ being Nat st b₆ <= card (Support b₄) holds
Low (b₅ *' b₄),b₂,b₆ = b₅ *' (Low b₄,b₂,b₆)

proof end;

Lemma47: for b₁ being Ordinal
for b₂ being connected TermOrder of b₁
for b₃ being add-associative right_zeroed right_complementable associative commutative right_unital distributive left_unital Field-like non trivial doubleLoopStr
for b₄ being Subset of (Polynom-Ring b₁,b₃)
for b₅ being RedSequence of PolyRedRel b₄,b₂
for b₆ being Nat st 1 <= b₆ & b₆ <= len b₅ & len b₅ > 1 holds
b₅ . b₆ is Polynomial of b₁,b₃

proof end;

theorem Th45: :: GROEB_3:45

proof end;

Lemma49: for b₁ being Ordinal
for b₂ being connected admissible TermOrder of b₁
for b₃ being add-associative right_zeroed right_complementable associative commutative right_unital distributive left_unital Field-like non trivial doubleLoopStr
for b₄, b₅ being Polynomial of b₁,b₃ st HT b₄,b₂, HT b₅,b₂ are_disjoint holds
for b₆, b₇ being bag of b₁ st b₆ in Support b₄ & b₇ in Support b₅ & ( not b₆ = HT b₄,b₂ or not b₇ = HT b₅,b₂ ) holds
not (HT b₄,b₂) + b₇ = (HT b₅,b₂) + b₆

proof end;

theorem Th46: :: GROEB_3:46

for b₁ being Ordinal
for b₂ being connected admissible TermOrder of b₁
for b₃ being Abelian add-associative right_zeroed right_complementable associative commutative right_unital distributive left_unital Field-like non trivial doubleLoopStr
for b₄, b₅, b₆, b₇ being Polynomial of b₁,b₃ st b₄ reduces_to b₅,{b₇},b₂ & ( for b₈ being bag of b₁ st b₈ in Support b₆ holds
not HT b₇,b₂ divides b₈ ) holds
b₄ + b₆ reduces_to b₅ + b₆,{b₇},b₂

proof end;

theorem Th47: :: GROEB_3:47

proof end;

theorem Th48: :: GROEB_3:48

for b₁ being Ordinal
for b₂ being connected admissible TermOrder of b₁
for b₃ being Abelian add-associative right_zeroed right_complementable associative commutative right_unital distributive left_unital Field-like non trivial doubleLoopStr
for b₄, b₅ being non-zero Polynomial of b₁,b₃
for b₆ being Polynomial of b₁,b₃ st b₆ . (HT (b₄ *' b₅),b₂) = 0. b₃ holds
(b₄ *' b₅) + b₆ reduces_to ((Red b₄,b₂) *' b₅) + b₆,{b₅},b₂

proof end;

theorem Th49: :: GROEB_3:49

for b₁ being Ordinal
for b₂ being connected admissible TermOrder of b₁
for b₃ being Abelian add-associative right_zeroed right_complementable associative commutative right_unital distributive left_unital Field-like non trivial doubleLoopStr
for b₄ being Subset of (Polynom-Ring b₁,b₃)
for b₅, b₆ being Polynomial of b₁,b₃ st PolyRedRel b₄,b₂ reduces b₅,b₆ holds
PolyRedRel b₄,b₂ reduces - b₅, - b₆

proof end;

theorem Th50: :: GROEB_3:50

for b₁ being Ordinal
for b₂ being connected admissible TermOrder of b₁
for b₃ being Abelian add-associative right_zeroed right_complementable associative commutative right_unital distributive left_unital Field-like non trivial doubleLoopStr
for b₄, b₅, b₆, b₇ being Polynomial of b₁,b₃ st PolyRedRel {b₇},b₂ reduces b₄,b₅ & ( for b₈ being bag of b₁ st b₈ in Support b₆ holds
not HT b₇,b₂ divides b₈ ) holds
PolyRedRel {b₇},b₂ reduces b₄ + b₆,b₅ + b₆

proof end;

theorem Th51: :: GROEB_3:51

proof end;

theorem Th52: :: GROEB_3:52

for b₁ being Ordinal
for b₂ being connected admissible TermOrder of b₁
for b₃ being add-associative right_zeroed right_complementable associative commutative right_unital distributive left_unital Field-like non trivial doubleLoopStr
for b₄, b₅ being Polynomial of b₁,b₃ st HT b₄,b₂, HT b₅,b₂ are_disjoint holds
for b₆, b₇ being bag of b₁ st b₆ in Support (Red b₄,b₂) & b₇ in Support (Red b₅,b₂) holds
not (HT b₄,b₂) + b₇ = (HT b₅,b₂) + b₆

proof end;

theorem Th53: :: GROEB_3:53

for b₁ being Ordinal
for b₂ being connected TermOrder of b₁
for b₃ being Abelian add-associative right_zeroed right_complementable associative commutative right_unital distributive left_unital Field-like non trivial doubleLoopStr
for b₄, b₅ being Polynomial of b₁,b₃ st HT b₄,b₂, HT b₅,b₂ are_disjoint holds
S-Poly b₄,b₅,b₂ = ((HM b₅,b₂) *' (Red b₄,b₂)) - ((HM b₄,b₂) *' (Red b₅,b₂))

proof end;

theorem Th54: :: GROEB_3:54

for b₁ being Ordinal
for b₂ being connected TermOrder of b₁
for b₃ being Abelian add-associative right_zeroed right_complementable associative commutative right_unital distributive left_unital Field-like non trivial doubleLoopStr
for b₄, b₅ being Polynomial of b₁,b₃ st HT b₄,b₂, HT b₅,b₂ are_disjoint holds
S-Poly b₄,b₅,b₂ = ((Red b₄,b₂) *' b₅) - ((Red b₅,b₂) *' b₄)

proof end;

theorem Th55: :: GROEB_3:55

for b₁ being Ordinal
for b₂ being connected admissible TermOrder of b₁
for b₃ being Abelian add-associative right_zeroed right_complementable associative commutative right_unital distributive left_unital Field-like non trivial doubleLoopStr
for b₄, b₅ being non-zero Polynomial of b₁,b₃ st HT b₄,b₂, HT b₅,b₂ are_disjoint & Red b₄,b₂ is non-zero & Red b₅,b₂ is non-zero holds
PolyRedRel {b₄},b₂ reduces ((HM b₅,b₂) *' (Red b₄,b₂)) - ((HM b₄,b₂) *' (Red b₅,b₂)),b₅ *' (Red b₄,b₂)

proof end;

theorem Th56: :: GROEB_3:56

for b₁ being Ordinal
for b₂ being connected admissible TermOrder of b₁
for b₃ being Abelian add-associative right_zeroed right_complementable associative commutative right_unital distributive left_unital Field-like non trivial doubleLoopStr
for b₄, b₅ being Polynomial of b₁,b₃ st HT b₄,b₂, HT b₅,b₂ are_disjoint holds
PolyRedRel {b₄,b₅},b₂ reduces S-Poly b₄,b₅,b₂, 0_ b₁,b₃

proof end;

theorem Th57: :: GROEB_3:57

for b₁ being Nat
for b₂ being connected admissible TermOrder of b₁
for b₃ being non empty Abelian add-associative right_zeroed right_complementable associative commutative right_unital distributive left_unital Field-like non degenerated doubleLoopStr
for b₄ being Subset of (Polynom-Ring b₁,b₃) st b₄ is_Groebner_basis_wrt b₂ holds
for b₅, b₆ being Polynomial of b₁,b₃ st b₅ in b₄ & b₆ in b₄ & not HT b₅,b₂, HT b₆,b₂ are_disjoint holds
PolyRedRel b₄,b₂ reduces S-Poly b₅,b₆,b₂, 0_ b₁,b₃

proof end;

theorem Th58: :: GROEB_3:58

for b₁ being Nat
for b₂ being connected admissible TermOrder of b₁
for b₃ being Abelian add-associative right_zeroed right_complementable associative commutative right_unital distributive left_unital Field-like non degenerated non trivial doubleLoopStr
for b₄ being Subset of (Polynom-Ring b₁,b₃) st not 0_ b₁,b₃ in b₄ & ( for b₅, b₆ being Polynomial of b₁,b₃ st b₅ in b₄ & b₆ in b₄ & not HT b₅,b₂, HT b₆,b₂ are_disjoint holds
PolyRedRel b₄,b₂ reduces S-Poly b₅,b₆,b₂, 0_ b₁,b₃ ) holds
for b₅, b₆, b₇ being Polynomial of b₁,b₃ st b₅ in b₄ & b₆ in b₄ & not HT b₅,b₂, HT b₆,b₂ are_disjoint & b₇ is_a_normal_form_of S-Poly b₅,b₆,b₂, PolyRedRel b₄,b₂ holds
b₇ = 0_ b₁,b₃

proof end;

theorem Th59: :: GROEB_3:59

for b₁ being Nat
for b₂ being connected admissible TermOrder of b₁
for b₃ being non empty Abelian add-associative right_zeroed right_complementable associative commutative right_unital distributive left_unital Field-like non degenerated doubleLoopStr
for b₄ being Subset of (Polynom-Ring b₁,b₃) st not 0_ b₁,b₃ in b₄ & ( for b₅, b₆, b₇ being Polynomial of b₁,b₃ st b₅ in b₄ & b₆ in b₄ & not HT b₅,b₂, HT b₆,b₂ are_disjoint & b₇ is_a_normal_form_of S-Poly b₅,b₆,b₂, PolyRedRel b₄,b₂ holds
b₇ = 0_ b₁,b₃ ) holds
b₄ is_Groebner_basis_wrt b₂

proof end;