let n be Element of NAT ; :: thesis: 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 non empty add-closed left-ideal Subset of (Polynom-Ring (n,L))

for G1, G2 being non empty finite Subset of (Polynom-Ring (n,L)) st G1 is_Groebner_basis_of I,T & G1 is_reduced_wrt T & G2 is_Groebner_basis_of I,T & G2 is_reduced_wrt T holds

G1 = G2

let T be connected admissible TermOrder of n; :: thesis: 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 non empty add-closed left-ideal Subset of (Polynom-Ring (n,L))

for G1, G2 being non empty finite Subset of (Polynom-Ring (n,L)) st G1 is_Groebner_basis_of I,T & G1 is_reduced_wrt T & G2 is_Groebner_basis_of I,T & G2 is_reduced_wrt T holds

G1 = G2

let L be non empty non degenerated right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative doubleLoopStr ; :: thesis: for I being non empty add-closed left-ideal Subset of (Polynom-Ring (n,L))

for G1, G2 being non empty finite Subset of (Polynom-Ring (n,L)) st G1 is_Groebner_basis_of I,T & G1 is_reduced_wrt T & G2 is_Groebner_basis_of I,T & G2 is_reduced_wrt T holds

G1 = G2

let I be non empty add-closed left-ideal Subset of (Polynom-Ring (n,L)); :: thesis: for G1, G2 being non empty finite Subset of (Polynom-Ring (n,L)) st G1 is_Groebner_basis_of I,T & G1 is_reduced_wrt T & G2 is_Groebner_basis_of I,T & G2 is_reduced_wrt T holds

G1 = G2

let G, H be non empty finite Subset of (Polynom-Ring (n,L)); :: thesis: ( G is_Groebner_basis_of I,T & G is_reduced_wrt T & H is_Groebner_basis_of I,T & H is_reduced_wrt T implies G = H )

assume that

A1: G is_Groebner_basis_of I,T and

A2: G is_reduced_wrt T and

A3: H is_Groebner_basis_of I,T and

A4: H is_reduced_wrt T ; :: thesis: G = H

A5: H -Ideal = I by A3;

set GH = (G \/ H) \ (G /\ H);

assume A6: G <> H ; :: thesis: contradiction

A14: g in GH and

A15: for q being Polynomial of n,L st q in GH holds

g <= q,T by POLYRED:31;

A16: G -Ideal = I by A1;

then for f being Polynomial of n,L st f in G -Ideal holds

PolyRedRel (G,T) reduces f, 0_ (n,L) by Th15;

then for f being non-zero Polynomial of n,L st f in G -Ideal holds

f is_reducible_wrt G,T by Th16;

then A23: for f being non-zero Polynomial of n,L st f in G -Ideal holds

f is_top_reducible_wrt G,T by Th17;

A24: for u being Polynomial of n,L st ( u in G or u in H ) holds

HC (u,T) = 1. L by Def6, A2, A4;

PolyRedRel (H,T) is locally-confluent by A3;

then for f being Polynomial of n,L st f in H -Ideal holds

PolyRedRel (H,T) reduces f, 0_ (n,L) by Th15;

then for f being non-zero Polynomial of n,L st f in H -Ideal holds

f is_reducible_wrt H,T by Th16;

then A31: for f being non-zero Polynomial of n,L st f in H -Ideal holds

f is_top_reducible_wrt H,T by Th17;

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 non empty add-closed left-ideal Subset of (Polynom-Ring (n,L))

for G1, G2 being non empty finite Subset of (Polynom-Ring (n,L)) st G1 is_Groebner_basis_of I,T & G1 is_reduced_wrt T & G2 is_Groebner_basis_of I,T & G2 is_reduced_wrt T holds

G1 = G2

let T be connected admissible TermOrder of n; :: thesis: 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 non empty add-closed left-ideal Subset of (Polynom-Ring (n,L))

for G1, G2 being non empty finite Subset of (Polynom-Ring (n,L)) st G1 is_Groebner_basis_of I,T & G1 is_reduced_wrt T & G2 is_Groebner_basis_of I,T & G2 is_reduced_wrt T holds

G1 = G2

let L be non empty non degenerated right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative doubleLoopStr ; :: thesis: for I being non empty add-closed left-ideal Subset of (Polynom-Ring (n,L))

for G1, G2 being non empty finite Subset of (Polynom-Ring (n,L)) st G1 is_Groebner_basis_of I,T & G1 is_reduced_wrt T & G2 is_Groebner_basis_of I,T & G2 is_reduced_wrt T holds

G1 = G2

let I be non empty add-closed left-ideal Subset of (Polynom-Ring (n,L)); :: thesis: for G1, G2 being non empty finite Subset of (Polynom-Ring (n,L)) st G1 is_Groebner_basis_of I,T & G1 is_reduced_wrt T & G2 is_Groebner_basis_of I,T & G2 is_reduced_wrt T holds

G1 = G2

let G, H be non empty finite Subset of (Polynom-Ring (n,L)); :: thesis: ( G is_Groebner_basis_of I,T & G is_reduced_wrt T & H is_Groebner_basis_of I,T & H is_reduced_wrt T implies G = H )

assume that

A1: G is_Groebner_basis_of I,T and

A2: G is_reduced_wrt T and

A3: H is_Groebner_basis_of I,T and

A4: H is_reduced_wrt T ; :: thesis: G = H

A5: H -Ideal = I by A3;

set GH = (G \/ H) \ (G /\ H);

assume A6: G <> H ; :: thesis: contradiction

now :: thesis: not (G \/ H) \ (G /\ H) = {}

then reconsider GH = (G \/ H) \ (G /\ H) as non empty Subset of (Polynom-Ring (n,L)) ;assume
(G \/ H) \ (G /\ H) = {}
; :: thesis: contradiction

then A7: G \/ H c= G /\ H by XBOOLE_1:37;

end;then A7: G \/ H c= G /\ H by XBOOLE_1:37;

A8: now :: thesis: for u being object st u in H holds

u in G

u in G

let u be object ; :: thesis: ( u in H implies u in G )

assume u in H ; :: thesis: u in G

then u in G \/ H by XBOOLE_0:def 3;

hence u in G by A7, XBOOLE_0:def 4; :: thesis: verum

end;assume u in H ; :: thesis: u in G

then u in G \/ H by XBOOLE_0:def 3;

hence u in G by A7, XBOOLE_0:def 4; :: thesis: verum

now :: thesis: for u being object st u in G holds

u in H

hence
contradiction
by A6, A8, TARSKI:2; :: thesis: verumu in H

let u be object ; :: thesis: ( u in G implies u in H )

assume u in G ; :: thesis: u in H

then u in G \/ H by XBOOLE_0:def 3;

hence u in H by A7, XBOOLE_0:def 4; :: thesis: verum

end;assume u in G ; :: thesis: u in H

then u in G \/ H by XBOOLE_0:def 3;

hence u in H by A7, XBOOLE_0:def 4; :: thesis: verum

A9: now :: thesis: for u being object st u in GH holds

u in (G \ H) \/ (H \ G)

consider g being Polynomial of n,L such that u in (G \ H) \/ (H \ G)

let u be object ; :: thesis: ( u in GH implies u in (G \ H) \/ (H \ G) )

assume A10: u in GH ; :: thesis: u in (G \ H) \/ (H \ G)

then A11: not u in G /\ H by XBOOLE_0:def 5;

A12: u in G \/ H by A10, XBOOLE_0:def 5;

( u in G \ H or u in H \ G )

end;assume A10: u in GH ; :: thesis: u in (G \ H) \/ (H \ G)

then A11: not u in G /\ H by XBOOLE_0:def 5;

A12: u in G \/ H by A10, XBOOLE_0:def 5;

( u in G \ H or u in H \ G )

proof

hence
u in (G \ H) \/ (H \ G)
by XBOOLE_0:def 3; :: thesis: verum
assume A13:
not u in G \ H
; :: thesis: u in H \ G

end;now :: thesis: ( ( not u in G & not u in G & u in H ) or ( u in H & u in H & not u in G ) )

hence
u in H \ G
by XBOOLE_0:def 5; :: thesis: verumend;

A14: g in GH and

A15: for q being Polynomial of n,L st q in GH holds

g <= q,T by POLYRED:31;

A16: G -Ideal = I by A1;

A17: now :: thesis: for u being set st ( u in G or u in H ) holds

( u is Polynomial of n,L & u <> 0_ (n,L) )

PolyRedRel (G,T) is locally-confluent
by A1;( u is Polynomial of n,L & u <> 0_ (n,L) )

let u be set ; :: thesis: ( ( u in G or u in H ) implies ( u is Polynomial of n,L & u <> 0_ (n,L) ) )

assume A18: ( u in G or u in H ) ; :: thesis: ( u is Polynomial of n,L & u <> 0_ (n,L) )

end;assume A18: ( u in G or u in H ) ; :: thesis: ( u is Polynomial of n,L & u <> 0_ (n,L) )

now :: thesis: ( ( u in G & u is Polynomial of n,L & u <> 0_ (n,L) ) or ( u in H & u is Polynomial of n,L & u <> 0_ (n,L) ) )end;

hence
( u is Polynomial of n,L & u <> 0_ (n,L) )
; :: thesis: verumper cases
( u in G or u in H )
by A18;

end;

case A19:
u in G
; :: thesis: ( u is Polynomial of n,L & u <> 0_ (n,L) )

then reconsider u9 = u as Element of (Polynom-Ring (n,L)) ;

reconsider u9 = u9 as Polynomial of n,L by POLYNOM1:def 11;

u9 is_monic_wrt T by A2, A19;

then A20: HC (u9,T) = 1. L ;

1. L <> 0. L ;

hence ( u is Polynomial of n,L & u <> 0_ (n,L) ) by A20, TERMORD:17; :: thesis: verum

end;reconsider u9 = u9 as Polynomial of n,L by POLYNOM1:def 11;

u9 is_monic_wrt T by A2, A19;

then A20: HC (u9,T) = 1. L ;

1. L <> 0. L ;

hence ( u is Polynomial of n,L & u <> 0_ (n,L) ) by A20, TERMORD:17; :: thesis: verum

case A21:
u in H
; :: thesis: ( u is Polynomial of n,L & u <> 0_ (n,L) )

then reconsider u9 = u as Element of (Polynom-Ring (n,L)) ;

reconsider u9 = u9 as Polynomial of n,L by POLYNOM1:def 11;

u9 is_monic_wrt T by A4, A21;

then A22: HC (u9,T) = 1. L ;

1. L <> 0. L ;

hence ( u is Polynomial of n,L & u <> 0_ (n,L) ) by A22, TERMORD:17; :: thesis: verum

end;reconsider u9 = u9 as Polynomial of n,L by POLYNOM1:def 11;

u9 is_monic_wrt T by A4, A21;

then A22: HC (u9,T) = 1. L ;

1. L <> 0. L ;

hence ( u is Polynomial of n,L & u <> 0_ (n,L) ) by A22, TERMORD:17; :: thesis: verum

then for f being Polynomial of n,L st f in G -Ideal holds

PolyRedRel (G,T) reduces f, 0_ (n,L) by Th15;

then for f being non-zero Polynomial of n,L st f in G -Ideal holds

f is_reducible_wrt G,T by Th16;

then A23: for f being non-zero Polynomial of n,L st f in G -Ideal holds

f is_top_reducible_wrt G,T by Th17;

A24: for u being Polynomial of n,L st ( u in G or u in H ) holds

HC (u,T) = 1. L by Def6, A2, A4;

A25: now :: thesis: for u being set holds

( not u in GH or u in G \ H or u in H \ G )

( not u in GH or u in G \ H or u in H \ G )

let u be set ; :: thesis: ( not u in GH or u in G \ H or u in H \ G )

assume A26: u in GH ; :: thesis: ( u in G \ H or u in H \ G )

then not u in G /\ H by XBOOLE_0:def 5;

then A27: ( not u in G or not u in H ) by XBOOLE_0:def 4;

A28: u in G \/ H by A26, XBOOLE_0:def 5;

end;assume A26: u in GH ; :: thesis: ( u in G \ H or u in H \ G )

then not u in G /\ H by XBOOLE_0:def 5;

then A27: ( not u in G or not u in H ) by XBOOLE_0:def 4;

A28: u in G \/ H by A26, XBOOLE_0:def 5;

now :: thesis: ( ( u in G & u in G \ H ) or ( u in H & u in H \ G ) )end;

hence
( u in G \ H or u in H \ G )
; :: thesis: verumnow :: thesis: for u being object st u in (G \ H) \/ (H \ G) holds

u in GH

then A30:
GH = (G \ H) \/ (H \ G)
by A9, TARSKI:2;u in GH

let u be object ; :: thesis: ( u in (G \ H) \/ (H \ G) implies u in GH )

assume A29: u in (G \ H) \/ (H \ G) ; :: thesis: u in GH

end;assume A29: u in (G \ H) \/ (H \ G) ; :: thesis: u in GH

now :: thesis: ( ( u in G \ H & u in G \/ H & not u in G /\ H ) or ( u in H \ G & u in G \/ H & not u in G /\ H ) )end;

hence
u in GH
by XBOOLE_0:def 5; :: thesis: verumper cases
( u in G \ H or u in H \ G )
by A29, XBOOLE_0:def 3;

end;

case
u in G \ H
; :: thesis: ( u in G \/ H & not u in G /\ H )

then
( u in G & not u in H )
by XBOOLE_0:def 5;

hence ( u in G \/ H & not u in G /\ H ) by XBOOLE_0:def 3, XBOOLE_0:def 4; :: thesis: verum

end;hence ( u in G \/ H & not u in G /\ H ) by XBOOLE_0:def 3, XBOOLE_0:def 4; :: thesis: verum

case
u in H \ G
; :: thesis: ( u in G \/ H & not u in G /\ H )

then
( u in H & not u in G )
by XBOOLE_0:def 5;

hence ( u in G \/ H & not u in G /\ H ) by XBOOLE_0:def 3, XBOOLE_0:def 4; :: thesis: verum

end;hence ( u in G \/ H & not u in G /\ H ) by XBOOLE_0:def 3, XBOOLE_0:def 4; :: thesis: verum

PolyRedRel (H,T) is locally-confluent by A3;

then for f being Polynomial of n,L st f in H -Ideal holds

PolyRedRel (H,T) reduces f, 0_ (n,L) by Th15;

then for f being non-zero Polynomial of n,L st f in H -Ideal holds

f is_reducible_wrt H,T by Th16;

then A31: for f being non-zero Polynomial of n,L st f in H -Ideal holds

f is_top_reducible_wrt H,T by Th17;

per cases
( g in G \ H or g in H \ G )
by A25, A14;

end;

suppose A32:
g in G \ H
; :: thesis: contradiction

then A33:
g in G
by XBOOLE_0:def 5;

then A34: g <> 0_ (n,L) by A17;

then reconsider g = g as non-zero Polynomial of n,L by POLYNOM7:def 1;

A35: G c= G -Ideal by IDEAL_1:def 14;

then HT (g,T) in HT ((H -Ideal),T) by A16, A5, A33, A34;

then consider b9 being bag of n such that

A36: b9 in HT (H,T) and

A37: b9 divides HT (g,T) by A31, Th18;

consider h being Polynomial of n,L such that

A38: b9 = HT (h,T) and

A39: h in H and

A40: h <> 0_ (n,L) by A36;

reconsider h = h as non-zero Polynomial of n,L by A40, POLYNOM7:def 1;

set f = g - h;

A41: h <> g by A32, A39, XBOOLE_0:def 5;

then HT (g,T) in Support g by TERMORD:def 6;

then A44: g is_reducible_wrt h,T by A37, A38, POLYRED:36;

then A45: ex r being Polynomial of n,L st g reduces_to r,h,T by POLYRED:def 8;

then g <= h,T by A15;

then not h < g,T by POLYRED:29;

then not HT (h,T) < HT (g,T),T by POLYRED:32;

then A49: HT (g,T) <= HT (h,T),T by TERMORD:5;

HT (h,T) <= HT (g,T),T by A44, Th9;

then A50: HT (h,T) = HT (g,T) by A49, TERMORD:7;

reconsider f = g - h as non-zero Polynomial of n,L by A42, POLYNOM7:def 1;

Support f <> {} by A42, POLYNOM7:1;

then A51: HT (f,T) in Support f by TERMORD:def 6;

f . (HT (g,T)) = (g + (- h)) . (HT (g,T)) by POLYNOM1:def 7

.= (g . (HT (g,T))) + ((- h) . (HT (g,T))) by POLYNOM1:15

.= (g . (HT (g,T))) + (- (h . (HT (h,T)))) by A50, POLYNOM1:17

.= (HC (g,T)) + (- (h . (HT (h,T)))) by TERMORD:def 7

.= (HC (g,T)) + (- (HC (h,T))) by TERMORD:def 7

.= (1. L) + (- (HC (h,T))) by A24, A33

.= (1. L) + (- (1. L)) by A24, A39

.= 0. L by RLVECT_1:5 ;

then A52: HT (f,T) <> HT (g,T) by A51, POLYNOM1:def 4;

HT (f,T) <= max ((HT (g,T)),(HT (h,T)),T),T by Th7;

then A53: HT (f,T) <= HT (g,T),T by A50, TERMORD:12;

reconsider g9 = g, h9 = h as Element of (Polynom-Ring (n,L)) by POLYNOM1:def 11;

reconsider g9 = g9, h9 = h9 as Element of (Polynom-Ring (n,L)) ;

H c= H -Ideal by IDEAL_1:def 14;

then g9 - h9 in I by A16, A5, A33, A35, A39, IDEAL_1:15;

then f in I by Lm2;

then A54: HT (f,T) in HT (I,T) by A42;

Support (g + (- h)) c= (Support g) \/ (Support (- h)) by POLYNOM1:20;

then Support f c= (Support g) \/ (Support (- h)) by POLYNOM1:def 7;

then A55: Support f c= (Support g) \/ (Support h) by Th5;

end;then A34: g <> 0_ (n,L) by A17;

then reconsider g = g as non-zero Polynomial of n,L by POLYNOM7:def 1;

A35: G c= G -Ideal by IDEAL_1:def 14;

then HT (g,T) in HT ((H -Ideal),T) by A16, A5, A33, A34;

then consider b9 being bag of n such that

A36: b9 in HT (H,T) and

A37: b9 divides HT (g,T) by A31, Th18;

consider h being Polynomial of n,L such that

A38: b9 = HT (h,T) and

A39: h in H and

A40: h <> 0_ (n,L) by A36;

reconsider h = h as non-zero Polynomial of n,L by A40, POLYNOM7:def 1;

set f = g - h;

A41: h <> g by A32, A39, XBOOLE_0:def 5;

A42: now :: thesis: not g - h = 0_ (n,L)

Support g <> {}
by A34, POLYNOM7:1;assume A43:
g - h = 0_ (n,L)
; :: thesis: contradiction

h = (0_ (n,L)) + h by POLYRED:2

.= (g + (- h)) + h by A43, POLYNOM1:def 7

.= g + ((- h) + h) by POLYNOM1:21

.= g + (0_ (n,L)) by POLYRED:3 ;

hence contradiction by A41, POLYNOM1:23; :: thesis: verum

end;h = (0_ (n,L)) + h by POLYRED:2

.= (g + (- h)) + h by A43, POLYNOM1:def 7

.= g + ((- h) + h) by POLYNOM1:21

.= g + (0_ (n,L)) by POLYRED:3 ;

hence contradiction by A41, POLYNOM1:23; :: thesis: verum

then HT (g,T) in Support g by TERMORD:def 6;

then A44: g is_reducible_wrt h,T by A37, A38, POLYRED:36;

then A45: ex r being Polynomial of n,L st g reduces_to r,h,T by POLYRED:def 8;

now :: thesis: h in H \ G

then
h in GH
by A30, XBOOLE_0:def 3;assume
not h in H \ G
; :: thesis: contradiction

then A46: h in G by A39, XBOOLE_0:def 5;

not h in {g} by A41, TARSKI:def 1;

then h in G \ {g} by A46, XBOOLE_0:def 5;

then consider r being Polynomial of n,L such that

A47: ( h in G \ {g} & g reduces_to r,h,T ) by A45;

A48: g reduces_to r,G \ {g},T by A47, POLYRED:def 7;

g is_irreducible_wrt G \ {g},T by A2, A33;

hence contradiction by A48, POLYRED:def 9; :: thesis: verum

end;then A46: h in G by A39, XBOOLE_0:def 5;

not h in {g} by A41, TARSKI:def 1;

then h in G \ {g} by A46, XBOOLE_0:def 5;

then consider r being Polynomial of n,L such that

A47: ( h in G \ {g} & g reduces_to r,h,T ) by A45;

A48: g reduces_to r,G \ {g},T by A47, POLYRED:def 7;

g is_irreducible_wrt G \ {g},T by A2, A33;

hence contradiction by A48, POLYRED:def 9; :: thesis: verum

then g <= h,T by A15;

then not h < g,T by POLYRED:29;

then not HT (h,T) < HT (g,T),T by POLYRED:32;

then A49: HT (g,T) <= HT (h,T),T by TERMORD:5;

HT (h,T) <= HT (g,T),T by A44, Th9;

then A50: HT (h,T) = HT (g,T) by A49, TERMORD:7;

reconsider f = g - h as non-zero Polynomial of n,L by A42, POLYNOM7:def 1;

Support f <> {} by A42, POLYNOM7:1;

then A51: HT (f,T) in Support f by TERMORD:def 6;

f . (HT (g,T)) = (g + (- h)) . (HT (g,T)) by POLYNOM1:def 7

.= (g . (HT (g,T))) + ((- h) . (HT (g,T))) by POLYNOM1:15

.= (g . (HT (g,T))) + (- (h . (HT (h,T)))) by A50, POLYNOM1:17

.= (HC (g,T)) + (- (h . (HT (h,T)))) by TERMORD:def 7

.= (HC (g,T)) + (- (HC (h,T))) by TERMORD:def 7

.= (1. L) + (- (HC (h,T))) by A24, A33

.= (1. L) + (- (1. L)) by A24, A39

.= 0. L by RLVECT_1:5 ;

then A52: HT (f,T) <> HT (g,T) by A51, POLYNOM1:def 4;

HT (f,T) <= max ((HT (g,T)),(HT (h,T)),T),T by Th7;

then A53: HT (f,T) <= HT (g,T),T by A50, TERMORD:12;

reconsider g9 = g, h9 = h as Element of (Polynom-Ring (n,L)) by POLYNOM1:def 11;

reconsider g9 = g9, h9 = h9 as Element of (Polynom-Ring (n,L)) ;

H c= H -Ideal by IDEAL_1:def 14;

then g9 - h9 in I by A16, A5, A33, A35, A39, IDEAL_1:15;

then f in I by Lm2;

then A54: HT (f,T) in HT (I,T) by A42;

Support (g + (- h)) c= (Support g) \/ (Support (- h)) by POLYNOM1:20;

then Support f c= (Support g) \/ (Support (- h)) by POLYNOM1:def 7;

then A55: Support f c= (Support g) \/ (Support h) by Th5;

now :: thesis: ( ( HT (f,T) in Support g & contradiction ) or ( HT (f,T) in Support h & contradiction ) )end;

hence
contradiction
; :: thesis: verumper cases
( HT (f,T) in Support g or HT (f,T) in Support h )
by A51, A55, XBOOLE_0:def 3;

end;

case A56:
HT (f,T) in Support g
; :: thesis: contradiction

consider b9 being bag of n such that

A57: b9 in HT (G,T) and

A58: b9 divides HT (f,T) by A16, A23, A54, Th18;

consider q being Polynomial of n,L such that

A59: b9 = HT (q,T) and

A60: q in G and

A61: q <> 0_ (n,L) by A57;

reconsider q = q as non-zero Polynomial of n,L by A61, POLYNOM7:def 1;

g is_reducible_wrt q,T by A56, A58, A59, POLYRED:36;

then consider r being Polynomial of n,L such that

A62: g reduces_to r,q,T by POLYRED:def 8;

HT (q,T) <= HT (f,T),T by A58, A59, TERMORD:10;

then q <> g by A53, A52, TERMORD:7;

then not q in {g} by TARSKI:def 1;

then q in G \ {g} by A60, XBOOLE_0:def 5;

then g reduces_to r,G \ {g},T by A62, POLYRED:def 7;

then g is_reducible_wrt G \ {g},T by POLYRED:def 9;

hence contradiction by A2, A33; :: thesis: verum

end;A57: b9 in HT (G,T) and

A58: b9 divides HT (f,T) by A16, A23, A54, Th18;

consider q being Polynomial of n,L such that

A59: b9 = HT (q,T) and

A60: q in G and

A61: q <> 0_ (n,L) by A57;

reconsider q = q as non-zero Polynomial of n,L by A61, POLYNOM7:def 1;

g is_reducible_wrt q,T by A56, A58, A59, POLYRED:36;

then consider r being Polynomial of n,L such that

A62: g reduces_to r,q,T by POLYRED:def 8;

HT (q,T) <= HT (f,T),T by A58, A59, TERMORD:10;

then q <> g by A53, A52, TERMORD:7;

then not q in {g} by TARSKI:def 1;

then q in G \ {g} by A60, XBOOLE_0:def 5;

then g reduces_to r,G \ {g},T by A62, POLYRED:def 7;

then g is_reducible_wrt G \ {g},T by POLYRED:def 9;

hence contradiction by A2, A33; :: thesis: verum

case A63:
HT (f,T) in Support h
; :: thesis: contradiction

consider b9 being bag of n such that

A64: b9 in HT (H,T) and

A65: b9 divides HT (f,T) by A5, A31, A54, Th18;

consider q being Polynomial of n,L such that

A66: b9 = HT (q,T) and

A67: q in H and

A68: q <> 0_ (n,L) by A64;

reconsider q = q as non-zero Polynomial of n,L by A68, POLYNOM7:def 1;

h is_reducible_wrt q,T by A63, A65, A66, POLYRED:36;

then consider r being Polynomial of n,L such that

A69: h reduces_to r,q,T by POLYRED:def 8;

HT (q,T) <= HT (f,T),T by A65, A66, TERMORD:10;

then q <> h by A50, A53, A52, TERMORD:7;

then not q in {h} by TARSKI:def 1;

then q in H \ {h} by A67, XBOOLE_0:def 5;

then h reduces_to r,H \ {h},T by A69, POLYRED:def 7;

then h is_reducible_wrt H \ {h},T by POLYRED:def 9;

hence contradiction by A4, A39; :: thesis: verum

end;A64: b9 in HT (H,T) and

A65: b9 divides HT (f,T) by A5, A31, A54, Th18;

consider q being Polynomial of n,L such that

A66: b9 = HT (q,T) and

A67: q in H and

A68: q <> 0_ (n,L) by A64;

reconsider q = q as non-zero Polynomial of n,L by A68, POLYNOM7:def 1;

h is_reducible_wrt q,T by A63, A65, A66, POLYRED:36;

then consider r being Polynomial of n,L such that

A69: h reduces_to r,q,T by POLYRED:def 8;

HT (q,T) <= HT (f,T),T by A65, A66, TERMORD:10;

then q <> h by A50, A53, A52, TERMORD:7;

then not q in {h} by TARSKI:def 1;

then q in H \ {h} by A67, XBOOLE_0:def 5;

then h reduces_to r,H \ {h},T by A69, POLYRED:def 7;

then h is_reducible_wrt H \ {h},T by POLYRED:def 9;

hence contradiction by A4, A39; :: thesis: verum

suppose A70:
g in H \ G
; :: thesis: contradiction

then A71:
not g in G
by XBOOLE_0:def 5;

A72: g in H by A70, XBOOLE_0:def 5;

then A73: g <> 0_ (n,L) by A17;

then reconsider g = g as non-zero Polynomial of n,L by POLYNOM7:def 1;

A74: H c= H -Ideal by IDEAL_1:def 14;

then HT (g,T) in HT ((G -Ideal),T) by A16, A5, A72, A73;

then consider b9 being bag of n such that

A75: b9 in HT (G,T) and

A76: b9 divides HT (g,T) by A23, Th18;

consider h being Polynomial of n,L such that

A77: b9 = HT (h,T) and

A78: h in G and

A79: h <> 0_ (n,L) by A75;

reconsider h = h as non-zero Polynomial of n,L by A79, POLYNOM7:def 1;

set f = g - h;

then HT (g,T) in Support g by TERMORD:def 6;

then A82: g is_reducible_wrt h,T by A76, A77, POLYRED:36;

then A83: ex r being Polynomial of n,L st g reduces_to r,h,T by POLYRED:def 8;

then g <= h,T by A15;

then not h < g,T by POLYRED:29;

then not HT (h,T) < HT (g,T),T by POLYRED:32;

then A87: HT (g,T) <= HT (h,T),T by TERMORD:5;

HT (h,T) <= HT (g,T),T by A82, Th9;

then A88: HT (h,T) = HT (g,T) by A87, TERMORD:7;

reconsider f = g - h as non-zero Polynomial of n,L by A80, POLYNOM7:def 1;

Support f <> {} by A80, POLYNOM7:1;

then A89: HT (f,T) in Support f by TERMORD:def 6;

f . (HT (g,T)) = (g + (- h)) . (HT (g,T)) by POLYNOM1:def 7

.= (g . (HT (g,T))) + ((- h) . (HT (g,T))) by POLYNOM1:15

.= (g . (HT (g,T))) + (- (h . (HT (h,T)))) by A88, POLYNOM1:17

.= (HC (g,T)) + (- (h . (HT (h,T)))) by TERMORD:def 7

.= (HC (g,T)) + (- (HC (h,T))) by TERMORD:def 7

.= (1. L) + (- (HC (h,T))) by A24, A72

.= (1. L) + (- (1. L)) by A24, A78

.= 0. L by RLVECT_1:5 ;

then A90: HT (f,T) <> HT (g,T) by A89, POLYNOM1:def 4;

HT (f,T) <= max ((HT (g,T)),(HT (h,T)),T),T by Th7;

then A91: HT (f,T) <= HT (g,T),T by A88, TERMORD:12;

reconsider g9 = g, h9 = h as Element of (Polynom-Ring (n,L)) by POLYNOM1:def 11;

reconsider g9 = g9, h9 = h9 as Element of (Polynom-Ring (n,L)) ;

G c= G -Ideal by IDEAL_1:def 14;

then g9 - h9 in I by A16, A5, A72, A74, A78, IDEAL_1:15;

then f in I by Lm2;

then A92: HT (f,T) in HT (I,T) by A80;

Support (g + (- h)) c= (Support g) \/ (Support (- h)) by POLYNOM1:20;

then Support f c= (Support g) \/ (Support (- h)) by POLYNOM1:def 7;

then A93: Support f c= (Support g) \/ (Support h) by Th5;

end;A72: g in H by A70, XBOOLE_0:def 5;

then A73: g <> 0_ (n,L) by A17;

then reconsider g = g as non-zero Polynomial of n,L by POLYNOM7:def 1;

A74: H c= H -Ideal by IDEAL_1:def 14;

then HT (g,T) in HT ((G -Ideal),T) by A16, A5, A72, A73;

then consider b9 being bag of n such that

A75: b9 in HT (G,T) and

A76: b9 divides HT (g,T) by A23, Th18;

consider h being Polynomial of n,L such that

A77: b9 = HT (h,T) and

A78: h in G and

A79: h <> 0_ (n,L) by A75;

reconsider h = h as non-zero Polynomial of n,L by A79, POLYNOM7:def 1;

set f = g - h;

A80: now :: thesis: not g - h = 0_ (n,L)

Support g <> {}
by A73, POLYNOM7:1;assume A81:
g - h = 0_ (n,L)
; :: thesis: contradiction

h = (0_ (n,L)) + h by POLYRED:2

.= (g + (- h)) + h by A81, POLYNOM1:def 7

.= g + ((- h) + h) by POLYNOM1:21

.= g + (0_ (n,L)) by POLYRED:3 ;

hence contradiction by A71, A78, POLYNOM1:23; :: thesis: verum

end;h = (0_ (n,L)) + h by POLYRED:2

.= (g + (- h)) + h by A81, POLYNOM1:def 7

.= g + ((- h) + h) by POLYNOM1:21

.= g + (0_ (n,L)) by POLYRED:3 ;

hence contradiction by A71, A78, POLYNOM1:23; :: thesis: verum

then HT (g,T) in Support g by TERMORD:def 6;

then A82: g is_reducible_wrt h,T by A76, A77, POLYRED:36;

then A83: ex r being Polynomial of n,L st g reduces_to r,h,T by POLYRED:def 8;

now :: thesis: h in G \ H

then
h in GH
by A30, XBOOLE_0:def 3;assume
not h in G \ H
; :: thesis: contradiction

then A84: h in H by A78, XBOOLE_0:def 5;

not h in {g} by A71, A78, TARSKI:def 1;

then h in H \ {g} by A84, XBOOLE_0:def 5;

then consider r being Polynomial of n,L such that

A85: ( h in H \ {g} & g reduces_to r,h,T ) by A83;

A86: g reduces_to r,H \ {g},T by A85, POLYRED:def 7;

g is_irreducible_wrt H \ {g},T by A4, A72;

hence contradiction by A86, POLYRED:def 9; :: thesis: verum

end;then A84: h in H by A78, XBOOLE_0:def 5;

not h in {g} by A71, A78, TARSKI:def 1;

then h in H \ {g} by A84, XBOOLE_0:def 5;

then consider r being Polynomial of n,L such that

A85: ( h in H \ {g} & g reduces_to r,h,T ) by A83;

A86: g reduces_to r,H \ {g},T by A85, POLYRED:def 7;

g is_irreducible_wrt H \ {g},T by A4, A72;

hence contradiction by A86, POLYRED:def 9; :: thesis: verum

then g <= h,T by A15;

then not h < g,T by POLYRED:29;

then not HT (h,T) < HT (g,T),T by POLYRED:32;

then A87: HT (g,T) <= HT (h,T),T by TERMORD:5;

HT (h,T) <= HT (g,T),T by A82, Th9;

then A88: HT (h,T) = HT (g,T) by A87, TERMORD:7;

reconsider f = g - h as non-zero Polynomial of n,L by A80, POLYNOM7:def 1;

Support f <> {} by A80, POLYNOM7:1;

then A89: HT (f,T) in Support f by TERMORD:def 6;

f . (HT (g,T)) = (g + (- h)) . (HT (g,T)) by POLYNOM1:def 7

.= (g . (HT (g,T))) + ((- h) . (HT (g,T))) by POLYNOM1:15

.= (g . (HT (g,T))) + (- (h . (HT (h,T)))) by A88, POLYNOM1:17

.= (HC (g,T)) + (- (h . (HT (h,T)))) by TERMORD:def 7

.= (HC (g,T)) + (- (HC (h,T))) by TERMORD:def 7

.= (1. L) + (- (HC (h,T))) by A24, A72

.= (1. L) + (- (1. L)) by A24, A78

.= 0. L by RLVECT_1:5 ;

then A90: HT (f,T) <> HT (g,T) by A89, POLYNOM1:def 4;

HT (f,T) <= max ((HT (g,T)),(HT (h,T)),T),T by Th7;

then A91: HT (f,T) <= HT (g,T),T by A88, TERMORD:12;

reconsider g9 = g, h9 = h as Element of (Polynom-Ring (n,L)) by POLYNOM1:def 11;

reconsider g9 = g9, h9 = h9 as Element of (Polynom-Ring (n,L)) ;

G c= G -Ideal by IDEAL_1:def 14;

then g9 - h9 in I by A16, A5, A72, A74, A78, IDEAL_1:15;

then f in I by Lm2;

then A92: HT (f,T) in HT (I,T) by A80;

Support (g + (- h)) c= (Support g) \/ (Support (- h)) by POLYNOM1:20;

then Support f c= (Support g) \/ (Support (- h)) by POLYNOM1:def 7;

then A93: Support f c= (Support g) \/ (Support h) by Th5;

now :: thesis: ( ( HT (f,T) in Support g & contradiction ) or ( HT (f,T) in Support h & contradiction ) )end;

hence
contradiction
; :: thesis: verumper cases
( HT (f,T) in Support g or HT (f,T) in Support h )
by A89, A93, XBOOLE_0:def 3;

end;

case A94:
HT (f,T) in Support g
; :: thesis: contradiction

consider b9 being bag of n such that

A95: b9 in HT (H,T) and

A96: b9 divides HT (f,T) by A5, A31, A92, Th18;

consider q being Polynomial of n,L such that

A97: b9 = HT (q,T) and

A98: q in H and

A99: q <> 0_ (n,L) by A95;

reconsider q = q as non-zero Polynomial of n,L by A99, POLYNOM7:def 1;

g is_reducible_wrt q,T by A94, A96, A97, POLYRED:36;

then consider r being Polynomial of n,L such that

A100: g reduces_to r,q,T by POLYRED:def 8;

HT (q,T) <= HT (f,T),T by A96, A97, TERMORD:10;

then q <> g by A91, A90, TERMORD:7;

then not q in {g} by TARSKI:def 1;

then q in H \ {g} by A98, XBOOLE_0:def 5;

then g reduces_to r,H \ {g},T by A100, POLYRED:def 7;

then g is_reducible_wrt H \ {g},T by POLYRED:def 9;

hence contradiction by A4, A72; :: thesis: verum

end;A95: b9 in HT (H,T) and

A96: b9 divides HT (f,T) by A5, A31, A92, Th18;

consider q being Polynomial of n,L such that

A97: b9 = HT (q,T) and

A98: q in H and

A99: q <> 0_ (n,L) by A95;

reconsider q = q as non-zero Polynomial of n,L by A99, POLYNOM7:def 1;

g is_reducible_wrt q,T by A94, A96, A97, POLYRED:36;

then consider r being Polynomial of n,L such that

A100: g reduces_to r,q,T by POLYRED:def 8;

HT (q,T) <= HT (f,T),T by A96, A97, TERMORD:10;

then q <> g by A91, A90, TERMORD:7;

then not q in {g} by TARSKI:def 1;

then q in H \ {g} by A98, XBOOLE_0:def 5;

then g reduces_to r,H \ {g},T by A100, POLYRED:def 7;

then g is_reducible_wrt H \ {g},T by POLYRED:def 9;

hence contradiction by A4, A72; :: thesis: verum

case A101:
HT (f,T) in Support h
; :: thesis: contradiction

consider b9 being bag of n such that

A102: b9 in HT (G,T) and

A103: b9 divides HT (f,T) by A16, A23, A92, Th18;

consider q being Polynomial of n,L such that

A104: b9 = HT (q,T) and

A105: q in G and

A106: q <> 0_ (n,L) by A102;

reconsider q = q as non-zero Polynomial of n,L by A106, POLYNOM7:def 1;

h is_reducible_wrt q,T by A101, A103, A104, POLYRED:36;

then consider r being Polynomial of n,L such that

A107: h reduces_to r,q,T by POLYRED:def 8;

HT (q,T) <= HT (f,T),T by A103, A104, TERMORD:10;

then HT (q,T) <> HT (h,T) by A88, A91, A90, TERMORD:7;

then not q in {h} by TARSKI:def 1;

then q in G \ {h} by A105, XBOOLE_0:def 5;

then h reduces_to r,G \ {h},T by A107, POLYRED:def 7;

then h is_reducible_wrt G \ {h},T by POLYRED:def 9;

hence contradiction by A2, A78; :: thesis: verum

end;A102: b9 in HT (G,T) and

A103: b9 divides HT (f,T) by A16, A23, A92, Th18;

consider q being Polynomial of n,L such that

A104: b9 = HT (q,T) and

A105: q in G and

A106: q <> 0_ (n,L) by A102;

reconsider q = q as non-zero Polynomial of n,L by A106, POLYNOM7:def 1;

h is_reducible_wrt q,T by A101, A103, A104, POLYRED:36;

then consider r being Polynomial of n,L such that

A107: h reduces_to r,q,T by POLYRED:def 8;

HT (q,T) <= HT (f,T),T by A103, A104, TERMORD:10;

then HT (q,T) <> HT (h,T) by A88, A91, A90, TERMORD:7;

then not q in {h} by TARSKI:def 1;

then q in G \ {h} by A105, XBOOLE_0:def 5;

then h reduces_to r,G \ {h},T by A107, POLYRED:def 7;

then h is_reducible_wrt G \ {h},T by POLYRED:def 9;

hence contradiction by A2, A78; :: thesis: verum