:: GROEB_2 semantic presentation

theorem :: GROEB_2:1

canceled;

theorem Th2: :: GROEB_2:2

for L being non empty LoopStr
for p being FinSequence of L
for n, m being Nat st m <= n holds
(p | n) | m = p | m

proof end;

theorem :: GROEB_2:3

for L being non empty add-associative right_zeroed right_complementable LoopStr
for p being FinSequence of L
for n being Nat st ( for k being Nat st k in dom p & k > n holds
p . k = 0. L ) holds
Sum p = Sum (p | n)

proof end;

theorem :: GROEB_2:4

for L being non empty Abelian add-associative right_zeroed LoopStr
for f being FinSequence of L
for i, j being Nat holds Sum (Swap f,i,j) = Sum f

proof end;

definition

let X be set ;
let b1, b2 be bag of X;
assume A1: b2 divides b1 ;
func b1 / b2 -> bag of X means :Def1: :: GROEB_2:def 1
b2 + it = b1;
existence by A1, TERMORD:1;
uniqueness

proof end;

end;

:: deftheorem Def1 defines / GROEB_2:def 1 :

definition

let X be set ;
let b1, b2 be bag of X;
func lcm b1,b2 -> bag of X means :Def2: :: GROEB_2:def 2
for k being set holds it . k = max (b1 . k),(b2 . k);
existence

proof end;

uniqueness

proof end;

commutativity ;
idempotence ;

end;

:: deftheorem Def2 defines lcm GROEB_2:def 2 :

notation

let X be set ;
let b1, b2 be bag of X;
synonym b1 lcm b2 for lcm b1,b2;

end;

definition

let X be set ;
let b1, b2 be bag of X;
pred b1,b2 are_disjoint means :Def3: :: GROEB_2:def 3
for i being set holds
( b1 . i = 0 or b2 . i = 0 );

end;

:: deftheorem Def3 defines are_disjoint GROEB_2:def 3 :

notation

let X be set ;
let b1, b2 be bag of X;
antonym b1,b2 are_non_disjoint for b1,b2 are_disjoint ;

end;

theorem :: GROEB_2:5

canceled;

theorem :: GROEB_2:6

canceled;

theorem Th7: :: GROEB_2:7

for X being set
for b1, b2 being bag of X holds
( b1 divides lcm b1,b2 & b2 divides lcm b1,b2 )

proof end;

theorem Th8: :: GROEB_2:8

for X being set
for b1, b2, b3 being bag of X st b1 divides b3 & b2 divides b3 holds
lcm b1,b2 divides b3

proof end;

theorem :: GROEB_2:9

for X being set
for b1, b2 being bag of X holds
( b1,b2 are_disjoint iff lcm b1,b2 = b1 + b2 )

proof end;

theorem Th10: :: GROEB_2:10

for X being set
for b being bag of X holds b / b = EmptyBag X

proof end;

theorem Th11: :: GROEB_2:11

for X being set
for b1, b2 being bag of X holds
( b2 divides b1 iff lcm b1,b2 = b1 )

proof end;

theorem :: GROEB_2:12

for X being set
for b1, b2, b3 being bag of X st b1 divides lcm b2,b3 holds
lcm b2,b1 divides lcm b2,b3

proof end;

theorem :: GROEB_2:13

for X being set
for b1, b2, b3 being bag of X st lcm b2,b1 divides lcm b2,b3 holds
lcm b1,b3 divides lcm b2,b3

proof end;

theorem :: GROEB_2:14

for n being set
for b1, b2, b3 being bag of n st lcm b1,b3 divides lcm b2,b3 holds
b1 divides lcm b2,b3

proof end;

theorem :: GROEB_2:15

for n being Nat
for T being connected admissible TermOrder of n
for P being non empty Subset of (Bags n) ex b being bag of n st
( b in P & ( for b' being bag of n st b' in P holds
b <= b',T ) )

proof end;

registration

let L be add-associative right_zeroed right_complementable non trivial LoopStr ;
let a be non-zero Element of L;
cluster - a -> non-zero ;
coherence

proof end;

end;

registration

let X be set ;
let L be non empty right_zeroed distributive add-cancelable left_zeroed doubleLoopStr ;
let m be Monomial of X,L;
let a be Element of L;
cluster a * m -> monomial-like ;
coherence

proof end;

end;

registration

let n be Ordinal;
let L be right_zeroed distributive add-cancelable left_zeroed non trivial domRing-like doubleLoopStr ;
let p be non-zero Polynomial of n,L;
let a be non-zero Element of L;
cluster a * p -> non-zero ;
coherence

proof end;

end;

theorem Th16: :: GROEB_2:16

for n being Ordinal
for L being non empty right_zeroed right-distributive doubleLoopStr
for p, q being Series of n,L
for b being bag of n holds b *' (p + q) = (b *' p) + (b *' q)

proof end;

theorem Th17: :: GROEB_2:17

for n being Ordinal
for L being non empty add-associative right_zeroed right_complementable LoopStr
for p being Series of n,L
for b being bag of n holds b *' (- p) = - (b *' p)

proof end;

theorem Th18: :: GROEB_2:18

for n being Ordinal
for L being non empty right-distributive left_zeroed add-right-cancelable doubleLoopStr
for p being Series of n,L
for b being bag of n
for a being Element of L holds b *' (a * p) = a * (b *' p)

proof end;

theorem Th19: :: GROEB_2:19

for n being Ordinal
for L being non empty right-distributive doubleLoopStr
for p, q being Series of n,L
for a being Element of L holds a * (p + q) = (a * p) + (a * q)

proof end;

theorem Th20: :: GROEB_2:20

for X being set
for L being non empty add-associative right_zeroed right_complementable doubleLoopStr
for a being Element of L holds - (a | X,L) = (- a) | X,L

proof end;

Lm1: for n being Ordinal
for T being connected TermOrder of n
for L being unital associative commutative add-associative right_zeroed right_complementable distributive Field-like non trivial doubleLoopStr
for f being Polynomial of n,L
for g being set
for P being Subset of (Polynom-Ring n,L) st PolyRedRel P,T reduces f,g holds
g is Polynomial of n,L

proof end;

theorem Th21: :: GROEB_2:21

for n being Nat
for T being connected admissible TermOrder of n
for L being non empty unital associative commutative Abelian add-associative right_zeroed right_complementable distributive Field-like non degenerated doubleLoopStr
for P being Subset of (Polynom-Ring n,L) st not 0_ n,L in P & ( for p1, p2 being Polynomial of n,L st p1 <> p2 & p1 in P & p2 in P holds
for m1, m2 being Monomial of n,L st HM (m1 *' p1),T = HM (m2 *' p2),T holds
PolyRedRel P,T reduces (m1 *' p1) - (m2 *' p2), 0_ n,L ) holds
P is_Groebner_basis_wrt T

proof end;

definition

let n be Ordinal;
let T be connected TermOrder of n;
let L be unital associative commutative add-associative right_zeroed right_complementable distributive Field-like non trivial doubleLoopStr ;
let p1, p2 be Polynomial of n,L;
func S-Poly p1,p2,T -> Polynomial of n,L equals :: GROEB_2:def 4
((HC p2,T) * (((lcm (HT p1,T),(HT p2,T)) / (HT p1,T)) *' p1)) - ((HC p1,T) * (((lcm (HT p1,T),(HT p2,T)) / (HT p2,T)) *' p2));
coherence ;

end;

:: deftheorem defines S-Poly GROEB_2:def 4 :

Lm2: for L being non empty unital associative add-associative right_zeroed right_complementable distributive add-cancelable left_zeroed doubleLoopStr
for P being Subset of L
for p being Element of L st p in P holds
p in P -Ideal

proof end;

Lm3: for n being Ordinal
for T being connected TermOrder of n
for L being unital add-associative right_zeroed right_complementable distributive non trivial 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

proof end;

theorem Th22: :: GROEB_2:22

for n being Ordinal
for T being connected TermOrder of n
for L being unital associative commutative Abelian add-associative right_zeroed right_complementable distributive Field-like non trivial doubleLoopStr
for P being Subset of (Polynom-Ring n,L)
for p1, p2 being Polynomial of n,L st p1 in P & p2 in P holds
S-Poly p1,p2,T in P -Ideal

proof end;

theorem :: GROEB_2:23

for n being Ordinal
for T being connected TermOrder of n
for L being unital associative commutative add-associative right_zeroed right_complementable distributive Field-like non trivial doubleLoopStr
for p1, p2 being Polynomial of n,L st p1 = p2 holds
S-Poly p1,p2,T = 0_ n,L by POLYNOM1:83;

theorem Th24: :: GROEB_2:24

for n being Ordinal
for T being connected TermOrder of n
for L being unital associative commutative add-associative right_zeroed right_complementable distributive Field-like non trivial doubleLoopStr
for m1, m2 being Monomial of n,L holds S-Poly m1,m2,T = 0_ n,L

proof end;

theorem Th25: :: GROEB_2:25

for n being Ordinal
for T being connected TermOrder of n
for L being unital associative commutative add-associative right_zeroed right_complementable distributive Field-like non trivial doubleLoopStr
for p being Polynomial of n,L holds
( S-Poly p,(0_ n,L),T = 0_ n,L & S-Poly (0_ n,L),p,T = 0_ n,L )

proof end;

theorem :: GROEB_2:26

for n being Ordinal
for T being connected admissible TermOrder of n
for L being unital associative commutative add-associative right_zeroed right_complementable distributive Field-like non trivial doubleLoopStr
for p1, p2 being Polynomial of n,L holds
( S-Poly p1,p2,T = 0_ n,L or HT (S-Poly p1,p2,T),T < lcm (HT p1,T),(HT p2,T),T )

proof end;

theorem :: GROEB_2:27

for n being Ordinal
for T being connected TermOrder of n
for L being unital associative commutative add-associative right_zeroed right_complementable distributive Field-like non trivial doubleLoopStr
for p1, p2 being non-zero Polynomial of n,L st HT p2,T divides HT p1,T holds
(HC p2,T) * p1 top_reduces_to S-Poly p1,p2,T,p2,T

proof end;

theorem :: GROEB_2:28

for n being Nat
for T being connected admissible TermOrder of n
for L being non empty unital associative commutative Abelian add-associative right_zeroed right_complementable distributive Field-like non degenerated doubleLoopStr
for G being Subset of (Polynom-Ring n,L) st G is_Groebner_basis_wrt T holds
for g1, g2, h being Polynomial of n,L st g1 in G & g2 in G & h is_a_normal_form_of S-Poly g1,g2,T, PolyRedRel G,T holds
h = 0_ n,L

proof end;

theorem :: GROEB_2:29

for n being Nat
for T being connected admissible TermOrder of n
for L being non empty unital associative commutative Abelian add-associative right_zeroed right_complementable distributive Field-like non degenerated doubleLoopStr
for G being Subset of (Polynom-Ring n,L) st ( for g1, g2, h being Polynomial of n,L st g1 in G & g2 in G & h is_a_normal_form_of S-Poly g1,g2,T, PolyRedRel G,T holds
h = 0_ n,L ) holds
for g1, g2 being Polynomial of n,L st g1 in G & g2 in G holds
PolyRedRel G,T reduces S-Poly g1,g2,T, 0_ n,L

proof end;

theorem Th30: :: GROEB_2:30

for n being Nat
for T being connected admissible TermOrder of n
for L being non empty unital associative commutative Abelian add-associative right_zeroed right_complementable distributive Field-like non degenerated doubleLoopStr
for G being Subset of (Polynom-Ring n,L) st not 0_ n,L in G & ( for g1, g2 being Polynomial of n,L st g1 in G & g2 in G holds
PolyRedRel G,T reduces S-Poly g1,g2,T, 0_ n,L ) holds
G is_Groebner_basis_wrt T

proof end;

definition

let n be Ordinal;
let T be connected TermOrder of n;
let L be unital associative commutative add-associative right_zeroed right_complementable distributive Field-like non trivial doubleLoopStr ;
let P be Subset of (Polynom-Ring n,L);
func S-Poly P,T -> Subset of (Polynom-Ring n,L) equals :: GROEB_2:def 5
{ (S-Poly p1,p2,T) where p1, p2 is Polynomial of n,L : ( p1 in P & p2 in P ) } ;
coherence

proof end;

end;

:: deftheorem defines S-Poly GROEB_2:def 5 :

registration

proof end;

end;

theorem :: GROEB_2:31

for n being Nat
for T being connected admissible TermOrder of n
for L being non empty unital associative commutative Abelian add-associative right_zeroed right_complementable distributive Field-like non degenerated doubleLoopStr
for G being Subset of (Polynom-Ring n,L) st not 0_ n,L in G & ( for g being Polynomial of n,L st g in G holds
g is Monomial of n,L ) holds
G is_Groebner_basis_wrt T

proof end;

theorem :: GROEB_2:32

for L being non empty multLoopStr
for P being non empty Subset of L
for A being LeftLinearCombination of P
for i being Nat holds A | i is LeftLinearCombination of P

proof end;

theorem :: GROEB_2:33

for L being non empty multLoopStr
for P being non empty Subset of L
for A being LeftLinearCombination of P
for i being Nat holds A /^ i is LeftLinearCombination of P

proof end;

theorem :: GROEB_2:34

for L being non empty multLoopStr
for P, Q being non empty Subset of L
for A being LeftLinearCombination of P st P c= Q holds
A is LeftLinearCombination of Q

proof end;

definition

let n be Ordinal;
let L be non empty unital add-associative right_zeroed right_complementable distributive non trivial doubleLoopStr ;
let P be non empty Subset of (Polynom-Ring n,L);
let A, B be LeftLinearCombination of P;
:: original: ^
redefine func A ^ B -> LeftLinearCombination of P;
coherence

proof end;

end;

definition

let n be Ordinal;
let L be non empty unital add-associative right_zeroed right_complementable distributive non trivial doubleLoopStr ;
let f be Polynomial of n,L;
let P be non empty Subset of (Polynom-Ring n,L);
let A be LeftLinearCombination of P;
pred A is_MonomialRepresentation_of f means :Def6: :: GROEB_2:def 6
( Sum A = f & ( for i being Nat st i in dom A holds
ex m being Monomial of n,L ex p being Polynomial of n,L st
( p in P & A /. i = m *' p ) ) );

end;

:: deftheorem Def6 defines is_MonomialRepresentation_of GROEB_2:def 6 :

theorem :: GROEB_2:35

for n being Ordinal
for L being non empty unital add-associative right_zeroed right_complementable distributive non trivial doubleLoopStr
for f being Polynomial of n,L
for P being non empty Subset of (Polynom-Ring n,L)
for A being LeftLinearCombination of P st A is_MonomialRepresentation_of f holds
Support f c= union { (Support (m *' p)) where m is Monomial of n,L, p is Polynomial of n,L : ex i being Nat st
( i in dom A & A /. i = m *' p ) }

proof end;

theorem :: GROEB_2:36

for n being Ordinal
for L being non empty unital add-associative right_zeroed right_complementable distributive non trivial doubleLoopStr
for f, g being Polynomial of n,L
for P being non empty Subset of (Polynom-Ring n,L)
for A, B being LeftLinearCombination of P st A is_MonomialRepresentation_of f & B is_MonomialRepresentation_of g holds
A ^ B is_MonomialRepresentation_of f + g

proof end;

Lm4: for n being Ordinal
for T being connected TermOrder of n
for L being non empty unital add-associative right_zeroed right_complementable distributive non trivial doubleLoopStr
for f being Polynomial of n,L
for P being non empty Subset of (Polynom-Ring n,L)
for A being LeftLinearCombination of P st A is_MonomialRepresentation_of f holds
for b being bag of n st ( for i being Nat st i in dom A holds
for m being Monomial of n,L
for p being Polynomial of n,L st A . i = m *' p & p in P holds
(m *' p) . b = 0. L ) holds
f . b = 0. L

proof end;

definition

let n be Ordinal;
let T be connected TermOrder of n;
let L be non empty unital add-associative right_zeroed right_complementable distributive non trivial doubleLoopStr ;
let f be Polynomial of n,L;
let P be non empty Subset of (Polynom-Ring n,L);
let A be LeftLinearCombination of P;
let b be bag of n;
pred A is_Standard_Representation_of f,P,b,T means :Def7: :: GROEB_2:def 7
( Sum A = f & ( for i being 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 <= b,T ) ) );

end;

:: deftheorem Def7 defines is_Standard_Representation_of GROEB_2:def 7 :

definition

let n be Ordinal;
let T be connected TermOrder of n;
let L be non empty unital add-associative right_zeroed right_complementable distributive non trivial doubleLoopStr ;
let f be Polynomial of n,L;
let P be non empty Subset of (Polynom-Ring n,L);
let A be LeftLinearCombination of P;
pred A is_Standard_Representation_of f,P,T means :Def8: :: GROEB_2:def 8
A is_Standard_Representation_of f,P, HT f,T,T;

end;

:: deftheorem Def8 defines is_Standard_Representation_of GROEB_2:def 8 :

definition

let n be Ordinal;
let T be connected TermOrder of n;
let L be non empty unital add-associative right_zeroed right_complementable distributive non trivial doubleLoopStr ;
let f be Polynomial of n,L;
let P be non empty Subset of (Polynom-Ring n,L);
let b be bag of n;
pred f has_a_Standard_Representation_of P,b,T means :: GROEB_2:def 9
ex A being LeftLinearCombination of P st A is_Standard_Representation_of f,P,b,T;

end;

:: deftheorem defines has_a_Standard_Representation_of GROEB_2:def 9 :

definition

let n be Ordinal;
let T be connected TermOrder of n;
let L be non empty unital add-associative right_zeroed right_complementable distributive non trivial doubleLoopStr ;
let f be Polynomial of n,L;
let P be non empty Subset of (Polynom-Ring n,L);
pred f has_a_Standard_Representation_of P,T means :Def10: :: GROEB_2:def 10
ex A being LeftLinearCombination of P st A is_Standard_Representation_of f,P,T;

end;

:: deftheorem Def10 defines has_a_Standard_Representation_of GROEB_2:def 10 :

theorem Th37: :: GROEB_2:37

for n being Ordinal
for T being connected TermOrder of n
for L being non empty unital add-associative right_zeroed right_complementable distributive non trivial doubleLoopStr
for f being Polynomial of n,L
for P being non empty Subset of (Polynom-Ring n,L)
for A being LeftLinearCombination of P
for b being bag of n st A is_Standard_Representation_of f,P,b,T holds
A is_MonomialRepresentation_of f

proof end;

Lm5: for n being Ordinal
for T being connected admissible TermOrder of n
for L being non empty unital associative commutative Abelian add-associative right_zeroed right_complementable distributive Field-like non degenerated doubleLoopStr
for f, g being Polynomial of n,L
for f', g' being Element of (Polynom-Ring n,L) st f = f' & g = g' holds
for P being non empty Subset of (Polynom-Ring n,L) st PolyRedRel P,T reduces f,g holds
ex A being LeftLinearCombination of P st
( f' = g' + (Sum A) & ( for i being 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 ) ) )

proof end;

theorem :: GROEB_2:38

for n being Ordinal
for T being connected TermOrder of n
for L being non empty unital add-associative right_zeroed right_complementable distributive non trivial doubleLoopStr
for f, g being Polynomial of n,L
for P being non empty Subset of (Polynom-Ring n,L)
for A, B being LeftLinearCombination of P
for b being bag of n st A is_Standard_Representation_of f,P,b,T & B is_Standard_Representation_of g,P,b,T holds
A ^ B is_Standard_Representation_of f + g,P,b,T

proof end;

theorem :: GROEB_2:39

for n being Ordinal
for T being connected TermOrder of n
for L being non empty unital add-associative right_zeroed right_complementable distributive non trivial doubleLoopStr
for f, g being Polynomial of n,L
for P being non empty Subset of (Polynom-Ring n,L)
for A, B being LeftLinearCombination of P
for b being bag of n
for i being Nat st A is_Standard_Representation_of f,P,b,T & B = A | i & g = Sum (A /^ i) holds
B is_Standard_Representation_of f - g,P,b,T

proof end;

theorem :: GROEB_2:40

for n being Ordinal
for T being connected TermOrder of n
for L being non empty unital Abelian add-associative right_zeroed right_complementable distributive non trivial doubleLoopStr
for f, g being Polynomial of n,L
for P being non empty Subset of (Polynom-Ring n,L)
for A, B being LeftLinearCombination of P
for b being bag of n
for i being Nat st A is_Standard_Representation_of f,P,b,T & B = A /^ i & g = Sum (A | i) & i <= len A holds
B is_Standard_Representation_of f - g,P,b,T

proof end;

theorem Th41: :: GROEB_2:41

for n being Ordinal
for T being connected TermOrder of n
for L being non empty unital add-associative right_zeroed right_complementable distributive non trivial doubleLoopStr
for f being non-zero Polynomial of n,L
for P being non empty Subset of (Polynom-Ring n,L)
for A being LeftLinearCombination of P st A is_MonomialRepresentation_of f holds
ex i being Nat ex m being non-zero Monomial of n,L ex p being non-zero Polynomial of n,L st
( i in dom A & p in P & A . i = m *' p & HT f,T <= HT (m *' p),T,T )

proof end;

theorem Th42: :: GROEB_2:42

for n being Ordinal
for T being connected TermOrder of n
for L being non empty unital add-associative right_zeroed right_complementable distributive non trivial doubleLoopStr
for f being non-zero Polynomial of n,L
for P being non empty Subset of (Polynom-Ring n,L)
for A being LeftLinearCombination of P st A is_Standard_Representation_of f,P,T holds
ex i being Nat ex m being non-zero Monomial of n,L ex p being non-zero Polynomial of n,L st
( p in P & i in dom A & A /. i = m *' p & HT f,T = HT (m *' p),T )

proof end;

theorem Th43: :: GROEB_2:43

for n being Ordinal
for T being connected admissible TermOrder of n
for L being non empty unital associative commutative Abelian add-associative right_zeroed right_complementable distributive Field-like non degenerated 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

proof end;

theorem Th44: :: GROEB_2:44

for n being Ordinal
for T being connected admissible TermOrder of n
for L being unital associative commutative add-associative right_zeroed right_complementable distributive Field-like non trivial 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

proof end;

theorem :: GROEB_2:45

for n being Nat
for T being connected admissible TermOrder of n
for L being non empty unital associative commutative Abelian add-associative right_zeroed right_complementable distributive Field-like non degenerated doubleLoopStr
for G being non empty Subset of (Polynom-Ring n,L) holds
( G is_Groebner_basis_wrt T iff for f being non-zero Polynomial of n,L st f in G -Ideal holds
f has_a_Standard_Representation_of G,T )

proof end;