let n be non empty Ordinal; :: thesis: 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 holds

not for P being Subset of (Polynom-Ring (n,L)) holds P is_Groebner_basis_wrt T

let T be connected admissible TermOrder of n; :: thesis: for L being non empty non degenerated right_complementable almost_left_invertible well-unital distributive add-associative right_zeroed associative commutative doubleLoopStr holds

not for P being Subset of (Polynom-Ring (n,L)) holds P is_Groebner_basis_wrt T

let L be non empty non degenerated right_complementable almost_left_invertible well-unital distributive add-associative right_zeroed associative commutative doubleLoopStr ; :: thesis: not for P being Subset of (Polynom-Ring (n,L)) holds P is_Groebner_basis_wrt T

set 1bag = (EmptyBag n) +* ({},1);

reconsider 1bag = (EmptyBag n) +* ({},1) as Element of Bags n by PRE_POLY:def 12;

set p = ((1. L) | (n,L)) +* (1bag,(1. L));

reconsider p = ((1. L) | (n,L)) +* (1bag,(1. L)) as Function of (Bags n),L ;

reconsider p = p as Series of n,L ;

A1: 1. L <> 0. L ;

set q = ((0. L) | (n,L)) +* (1bag,(1. L));

reconsider q = ((0. L) | (n,L)) +* (1bag,(1. L)) as Function of (Bags n),L ;

reconsider q = q as Series of n,L ;

then 1bag . {} = 1 by FUNCT_7:31;

then A8: EmptyBag n <> 1bag by PBOOLE:5;

then A9: q . (EmptyBag n) = ((0. L) | (n,L)) . (EmptyBag n) by FUNCT_7:32

.= (0_ (n,L)) . (EmptyBag n) by POLYNOM7:19

.= 0. L by POLYNOM1:22 ;

then A14: q . 1bag = 1. L by FUNCT_7:31;

then A15: q <> 0_ (n,L) by POLYNOM1:22;

then reconsider q = q as Polynomial of n,L by POLYNOM1:def 5;

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

set q1 = q - (((q . (HT (q,T))) / (HC (q,T))) * ((EmptyBag n) *' q));

Support q <> {} by A15, POLYNOM7:1;

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

(EmptyBag n) + (HT (q,T)) = HT (q,T) by PRE_POLY:53;

then q reduces_to q - (((q . (HT (q,T))) / (HC (q,T))) * ((EmptyBag n) *' q)),q, HT (q,T),T by A15, A17, POLYRED:def 5;

then A18: q reduces_to q - (((q . (HT (q,T))) / (HC (q,T))) * ((EmptyBag n) *' q)),q,T by POLYRED:def 6;

A19: q - (((q . (HT (q,T))) / (HC (q,T))) * ((EmptyBag n) *' q)) = q - (((HC (q,T)) / (HC (q,T))) * ((EmptyBag n) *' q)) by TERMORD:def 7

.= q - (((HC (q,T)) * ((HC (q,T)) ")) * ((EmptyBag n) *' q))

.= q - ((1. L) * ((EmptyBag n) *' q)) by VECTSP_1:def 10

.= q - ((1. L) * q) by POLYRED:17

.= q - (((1. L) | (n,L)) *' q) by POLYNOM7:27

.= q - ((1_ (n,L)) *' q) by POLYNOM7:20

.= q - q by POLYNOM1:30

.= 0_ (n,L) by POLYNOM1:24 ;

A20: dom ((1. L) | (n,L)) = Bags n by FUNCT_2:def 1;

then A21: p . 1bag = 1. L by FUNCT_7:31;

then A22: p <> 0_ (n,L) by A1, POLYNOM1:22;

A23: p . (EmptyBag n) = ((1. L) | (n,L)) . (EmptyBag n) by A8, FUNCT_7:32

.= (1_ (n,L)) . (EmptyBag n) by POLYNOM7:20

.= 1. L by POLYNOM1:25 ;

then reconsider p = p as Polynomial of n,L by POLYNOM1:def 5;

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

A26: (EmptyBag n) + (HT (p,T)) = HT (p,T) by PRE_POLY:53;

Support p <> {} by A22, POLYNOM7:1;

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

then A31: HT (p,T) = 1bag by A25, A27, TARSKI:def 2;

then HT (p,T) in Support q by A16, TARSKI:def 1;

then q reduces_to q - (((q . (HT (p,T))) / (HC (p,T))) * ((EmptyBag n) *' p)),p, HT (p,T),T by A22, A15, A26, POLYRED:def 5;

then A32: q reduces_to q - (((q . (HT (p,T))) / (HC (p,T))) * ((EmptyBag n) *' p)),p,T by POLYRED:def 6;

reconsider P = P as Subset of (Polynom-Ring (n,L)) ;

set R = PolyRedRel (P,T);

take P ; :: thesis: not P is_Groebner_basis_wrt T

A35: p in P by TARSKI:def 2;

q in P by TARSKI:def 2;

then q reduces_to 0_ (n,L),P,T by A18, A19, POLYRED:def 7;

then A36: [q,(0_ (n,L))] in PolyRedRel (P,T) by POLYRED:def 13;

q - (((q . (HT (p,T))) / (HC (p,T))) * ((EmptyBag n) *' p)) = q - (((1. L) / (p . 1bag)) * ((EmptyBag n) *' p)) by A14, A31, TERMORD:def 7

.= q - (((1. L) / (1. L)) * ((EmptyBag n) *' p)) by A20, FUNCT_7:31

.= q - (((1. L) * ((1. L) ")) * ((EmptyBag n) *' p))

.= q - ((1. L) * ((EmptyBag n) *' p)) by VECTSP_1:def 10

.= q - ((1. L) * p) by POLYRED:17

.= q - (((1. L) | (n,L)) *' p) by POLYNOM7:27

.= q - ((1_ (n,L)) *' p) by POLYNOM7:20

.= q - p by POLYNOM1:30 ;

then q reduces_to q - p,P,T by A32, A35, POLYRED:def 7;

then A37: [q,(q - p)] in PolyRedRel (P,T) by POLYRED:def 13;

for L being non empty non degenerated right_complementable almost_left_invertible well-unital distributive add-associative right_zeroed associative commutative doubleLoopStr holds

not for P being Subset of (Polynom-Ring (n,L)) holds P is_Groebner_basis_wrt T

let T be connected admissible TermOrder of n; :: thesis: for L being non empty non degenerated right_complementable almost_left_invertible well-unital distributive add-associative right_zeroed associative commutative doubleLoopStr holds

not for P being Subset of (Polynom-Ring (n,L)) holds P is_Groebner_basis_wrt T

let L be non empty non degenerated right_complementable almost_left_invertible well-unital distributive add-associative right_zeroed associative commutative doubleLoopStr ; :: thesis: not for P being Subset of (Polynom-Ring (n,L)) holds P is_Groebner_basis_wrt T

set 1bag = (EmptyBag n) +* ({},1);

reconsider 1bag = (EmptyBag n) +* ({},1) as Element of Bags n by PRE_POLY:def 12;

set p = ((1. L) | (n,L)) +* (1bag,(1. L));

reconsider p = ((1. L) | (n,L)) +* (1bag,(1. L)) as Function of (Bags n),L ;

reconsider p = p as Series of n,L ;

A1: 1. L <> 0. L ;

set q = ((0. L) | (n,L)) +* (1bag,(1. L));

reconsider q = ((0. L) | (n,L)) +* (1bag,(1. L)) as Function of (Bags n),L ;

reconsider q = q as Series of n,L ;

A2: now :: thesis: for u being bag of n st u <> EmptyBag n & u <> 1bag holds

p . u = 0. L

p . u = 0. L

let u be bag of n; :: thesis: ( u <> EmptyBag n & u <> 1bag implies p . u = 0. L )

assume that

A3: u <> EmptyBag n and

A4: u <> 1bag ; :: thesis: p . u = 0. L

p . u = ((1. L) | (n,L)) . u by A4, FUNCT_7:32;

then p . u = (1_ (n,L)) . u by POLYNOM7:20;

hence p . u = 0. L by A3, POLYNOM1:25; :: thesis: verum

end;assume that

A3: u <> EmptyBag n and

A4: u <> 1bag ; :: thesis: p . u = 0. L

p . u = ((1. L) | (n,L)) . u by A4, FUNCT_7:32;

then p . u = (1_ (n,L)) . u by POLYNOM7:20;

hence p . u = 0. L by A3, POLYNOM1:25; :: thesis: verum

A5: now :: thesis: for u9 being object st u9 in Support p holds

u9 in {(EmptyBag n),1bag}

( {} in n & dom (EmptyBag n) = n )
by ORDINAL1:14, PARTFUN1:def 2;u9 in {(EmptyBag n),1bag}

let u9 be object ; :: thesis: ( u9 in Support p implies u9 in {(EmptyBag n),1bag} )

assume A6: u9 in Support p ; :: thesis: u9 in {(EmptyBag n),1bag}

then reconsider u = u9 as Element of Bags n ;

A7: p . u <> 0. L by A6, POLYNOM1:def 4;

end;assume A6: u9 in Support p ; :: thesis: u9 in {(EmptyBag n),1bag}

then reconsider u = u9 as Element of Bags n ;

A7: p . u <> 0. L by A6, POLYNOM1:def 4;

now :: thesis: u in {(EmptyBag n),1bag}

hence
u9 in {(EmptyBag n),1bag}
; :: thesis: verumassume
not u in {(EmptyBag n),1bag}
; :: thesis: contradiction

then ( u <> EmptyBag n & u <> 1bag ) by TARSKI:def 2;

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

end;then ( u <> EmptyBag n & u <> 1bag ) by TARSKI:def 2;

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

then 1bag . {} = 1 by FUNCT_7:31;

then A8: EmptyBag n <> 1bag by PBOOLE:5;

then A9: q . (EmptyBag n) = ((0. L) | (n,L)) . (EmptyBag n) by FUNCT_7:32

.= (0_ (n,L)) . (EmptyBag n) by POLYNOM7:19

.= 0. L by POLYNOM1:22 ;

A10: now :: thesis: for u being bag of n st u <> 1bag holds

q . u = 0. L

q . u = 0. L

let u be bag of n; :: thesis: ( u <> 1bag implies q . u = 0. L )

assume u <> 1bag ; :: thesis: q . u = 0. L

then q . u = ((0. L) | (n,L)) . u by FUNCT_7:32;

then q . u = (0_ (n,L)) . u by POLYNOM7:19;

hence q . u = 0. L by POLYNOM1:22; :: thesis: verum

end;assume u <> 1bag ; :: thesis: q . u = 0. L

then q . u = ((0. L) | (n,L)) . u by FUNCT_7:32;

then q . u = (0_ (n,L)) . u by POLYNOM7:19;

hence q . u = 0. L by POLYNOM1:22; :: thesis: verum

A11: now :: thesis: for u9 being object st u9 in Support q holds

u9 in {1bag}

dom ((0. L) | (n,L)) = Bags n
by FUNCT_2:def 1;u9 in {1bag}

let u9 be object ; :: thesis: ( u9 in Support q implies u9 in {1bag} )

assume A12: u9 in Support q ; :: thesis: u9 in {1bag}

then reconsider u = u9 as Element of Bags n ;

A13: q . u <> 0. L by A12, POLYNOM1:def 4;

end;assume A12: u9 in Support q ; :: thesis: u9 in {1bag}

then reconsider u = u9 as Element of Bags n ;

A13: q . u <> 0. L by A12, POLYNOM1:def 4;

now :: thesis: u in {1bag}

hence
u9 in {1bag}
; :: thesis: verumassume
not u in {1bag}
; :: thesis: contradiction

then u <> 1bag by TARSKI:def 1;

hence contradiction by A10, A13; :: thesis: verum

end;then u <> 1bag by TARSKI:def 1;

hence contradiction by A10, A13; :: thesis: verum

then A14: q . 1bag = 1. L by FUNCT_7:31;

then A15: q <> 0_ (n,L) by POLYNOM1:22;

now :: thesis: for u being object st u in {1bag} holds

u in Support q

then A16:
Support q = {1bag}
by A11, TARSKI:2;u in Support q

let u be object ; :: thesis: ( u in {1bag} implies u in Support q )

assume u in {1bag} ; :: thesis: u in Support q

then u = 1bag by TARSKI:def 1;

hence u in Support q by A14, POLYNOM1:def 4; :: thesis: verum

end;assume u in {1bag} ; :: thesis: u in Support q

then u = 1bag by TARSKI:def 1;

hence u in Support q by A14, POLYNOM1:def 4; :: thesis: verum

then reconsider q = q as Polynomial of n,L by POLYNOM1:def 5;

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

set q1 = q - (((q . (HT (q,T))) / (HC (q,T))) * ((EmptyBag n) *' q));

Support q <> {} by A15, POLYNOM7:1;

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

(EmptyBag n) + (HT (q,T)) = HT (q,T) by PRE_POLY:53;

then q reduces_to q - (((q . (HT (q,T))) / (HC (q,T))) * ((EmptyBag n) *' q)),q, HT (q,T),T by A15, A17, POLYRED:def 5;

then A18: q reduces_to q - (((q . (HT (q,T))) / (HC (q,T))) * ((EmptyBag n) *' q)),q,T by POLYRED:def 6;

A19: q - (((q . (HT (q,T))) / (HC (q,T))) * ((EmptyBag n) *' q)) = q - (((HC (q,T)) / (HC (q,T))) * ((EmptyBag n) *' q)) by TERMORD:def 7

.= q - (((HC (q,T)) * ((HC (q,T)) ")) * ((EmptyBag n) *' q))

.= q - ((1. L) * ((EmptyBag n) *' q)) by VECTSP_1:def 10

.= q - ((1. L) * q) by POLYRED:17

.= q - (((1. L) | (n,L)) *' q) by POLYNOM7:27

.= q - ((1_ (n,L)) *' q) by POLYNOM7:20

.= q - q by POLYNOM1:30

.= 0_ (n,L) by POLYNOM1:24 ;

A20: dom ((1. L) | (n,L)) = Bags n by FUNCT_2:def 1;

then A21: p . 1bag = 1. L by FUNCT_7:31;

then A22: p <> 0_ (n,L) by A1, POLYNOM1:22;

A23: p . (EmptyBag n) = ((1. L) | (n,L)) . (EmptyBag n) by A8, FUNCT_7:32

.= (1_ (n,L)) . (EmptyBag n) by POLYNOM7:20

.= 1. L by POLYNOM1:25 ;

now :: thesis: for u being object st u in {(EmptyBag n),1bag} holds

u in Support p

then A25:
Support p = {(EmptyBag n),1bag}
by A5, TARSKI:2;u in Support p

let u be object ; :: thesis: ( u in {(EmptyBag n),1bag} implies u in Support p )

assume A24: u in {(EmptyBag n),1bag} ; :: thesis: u in Support p

end;assume A24: u in {(EmptyBag n),1bag} ; :: thesis: u in Support p

now :: thesis: ( ( u = EmptyBag n & u in Support p ) or ( u = 1bag & u in Support p ) )

hence
u in Support p
; :: thesis: verumend;

then reconsider p = p as Polynomial of n,L by POLYNOM1:def 5;

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

A26: (EmptyBag n) + (HT (p,T)) = HT (p,T) by PRE_POLY:53;

A27: now :: thesis: not HT (p,T) = EmptyBag n

set p1 = q - (((q . (HT (p,T))) / (HC (p,T))) * ((EmptyBag n) *' p));A28:
EmptyBag n <= 1bag,T
by TERMORD:9;

assume A29: HT (p,T) = EmptyBag n ; :: thesis: contradiction

1bag in Support p by A25, TARSKI:def 2;

then 1bag <= EmptyBag n,T by A29, TERMORD:def 6;

hence contradiction by A8, A28, TERMORD:7; :: thesis: verum

end;assume A29: HT (p,T) = EmptyBag n ; :: thesis: contradiction

1bag in Support p by A25, TARSKI:def 2;

then 1bag <= EmptyBag n,T by A29, TERMORD:def 6;

hence contradiction by A8, A28, TERMORD:7; :: thesis: verum

Support p <> {} by A22, POLYNOM7:1;

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

then A31: HT (p,T) = 1bag by A25, A27, TARSKI:def 2;

then HT (p,T) in Support q by A16, TARSKI:def 1;

then q reduces_to q - (((q . (HT (p,T))) / (HC (p,T))) * ((EmptyBag n) *' p)),p, HT (p,T),T by A22, A15, A26, POLYRED:def 5;

then A32: q reduces_to q - (((q . (HT (p,T))) / (HC (p,T))) * ((EmptyBag n) *' p)),p,T by POLYRED:def 6;

A33: now :: thesis: not Support q = Support p

assume
Support q = Support p
; :: thesis: contradiction

then EmptyBag n in {1bag} by A25, A16, TARSKI:def 2;

hence contradiction by A8, TARSKI:def 1; :: thesis: verum

end;then EmptyBag n in {1bag} by A25, A16, TARSKI:def 2;

hence contradiction by A8, TARSKI:def 1; :: thesis: verum

A34: now :: thesis: not q - p = 0_ (n,L)

set P = {p,q};assume
q - p = 0_ (n,L)
; :: thesis: contradiction

then p = (q - p) + p by POLYRED:2

.= (q + (- p)) + p by POLYNOM1:def 7

.= q + ((- p) + p) by POLYNOM1:21

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

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

end;then p = (q - p) + p by POLYRED:2

.= (q + (- p)) + p by POLYNOM1:def 7

.= q + ((- p) + p) by POLYNOM1:21

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

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

now :: thesis: for u being object st u in {p,q} holds

u in the carrier of (Polynom-Ring (n,L))

then reconsider P = {p,q} as Subset of (Polynom-Ring (n,L)) by TARSKI:def 3;u in the carrier of (Polynom-Ring (n,L))

let u be object ; :: thesis: ( u in {p,q} implies u in the carrier of (Polynom-Ring (n,L)) )

assume u in {p,q} ; :: thesis: u in the carrier of (Polynom-Ring (n,L))

then ( u = p or u = q ) by TARSKI:def 2;

hence u in the carrier of (Polynom-Ring (n,L)) by POLYNOM1:def 11; :: thesis: verum

end;assume u in {p,q} ; :: thesis: u in the carrier of (Polynom-Ring (n,L))

then ( u = p or u = q ) by TARSKI:def 2;

hence u in the carrier of (Polynom-Ring (n,L)) by POLYNOM1:def 11; :: thesis: verum

reconsider P = P as Subset of (Polynom-Ring (n,L)) ;

set R = PolyRedRel (P,T);

take P ; :: thesis: not P is_Groebner_basis_wrt T

A35: p in P by TARSKI:def 2;

q in P by TARSKI:def 2;

then q reduces_to 0_ (n,L),P,T by A18, A19, POLYRED:def 7;

then A36: [q,(0_ (n,L))] in PolyRedRel (P,T) by POLYRED:def 13;

q - (((q . (HT (p,T))) / (HC (p,T))) * ((EmptyBag n) *' p)) = q - (((1. L) / (p . 1bag)) * ((EmptyBag n) *' p)) by A14, A31, TERMORD:def 7

.= q - (((1. L) / (1. L)) * ((EmptyBag n) *' p)) by A20, FUNCT_7:31

.= q - (((1. L) * ((1. L) ")) * ((EmptyBag n) *' p))

.= q - ((1. L) * ((EmptyBag n) *' p)) by VECTSP_1:def 10

.= q - ((1. L) * p) by POLYRED:17

.= q - (((1. L) | (n,L)) *' p) by POLYNOM7:27

.= q - ((1_ (n,L)) *' p) by POLYNOM7:20

.= q - p by POLYNOM1:30 ;

then q reduces_to q - p,P,T by A32, A35, POLYRED:def 7;

then A37: [q,(q - p)] in PolyRedRel (P,T) by POLYRED:def 13;

now :: thesis: not PolyRedRel (P,T) is locally-confluent

then 0_ (n,L),q - p are_convergent_wrt PolyRedRel (P,T) by A37, A36, REWRITE1:def 24;

then consider c being object such that

A43: PolyRedRel (P,T) reduces 0_ (n,L),c and

A44: PolyRedRel (P,T) reduces q - p,c by REWRITE1:def 7;

reconsider c = c as Polynomial of n,L by A43, Lm4;

consider s being FinSequence such that

A45: len s > 0 and

A46: s . 1 = 0_ (n,L) and

A47: s . (len s) = c and

A48: for i being Nat st i in dom s & i + 1 in dom s holds

[(s . i),(s . (i + 1))] in PolyRedRel (P,T) by A43, REWRITE1:11;

A56: len s > 0 and

A57: s . 1 = q - p and

A58: s . (len s) = 0_ (n,L) and

A59: for i being Nat st i in dom s & i + 1 in dom s holds

[(s . i),(s . (i + 1))] in PolyRedRel (P,T) by A44, A46, A47, REWRITE1:11;

end;

hence
not P is_Groebner_basis_wrt T
; :: thesis: verumA38: now :: thesis: for u being object st u in Support (q - p) holds

u in {(EmptyBag n)}

assume
PolyRedRel (P,T) is locally-confluent
; :: thesis: contradictionu in {(EmptyBag n)}

let u be object ; :: thesis: ( u in Support (q - p) implies u in {(EmptyBag n)} )

then A39: {1bag} \/ {(EmptyBag n),1bag} = {(EmptyBag n),1bag} by XBOOLE_1:12;

A40: (q - p) . 1bag = (q + (- p)) . 1bag by POLYNOM1:def 7

.= (q . 1bag) + ((- p) . 1bag) by POLYNOM1:15

.= (q . 1bag) + (- (p . 1bag)) by POLYNOM1:17

.= (1. L) + (- (1. L)) by A20, A14, FUNCT_7:31

.= 0. L by RLVECT_1:5 ;

Support (q - p) = Support (q + (- p)) by POLYNOM1:def 7;

then Support (q - p) c= (Support q) \/ (Support (- p)) by POLYNOM1:20;

then A41: Support (q - p) c= {1bag} \/ {(EmptyBag n),1bag} by A25, A16, Th5;

assume A42: u in Support (q - p) ; :: thesis: u in {(EmptyBag n)}

then (q - p) . u <> 0. L by POLYNOM1:def 4;

then u = EmptyBag n by A42, A41, A39, A40, TARSKI:def 2;

hence u in {(EmptyBag n)} by TARSKI:def 1; :: thesis: verum

end;now :: thesis: for u being object st u in {1bag} holds

u in {(EmptyBag n),1bag}

then
{1bag} c= {(EmptyBag n),1bag}
;u in {(EmptyBag n),1bag}

let u be object ; :: thesis: ( u in {1bag} implies u in {(EmptyBag n),1bag} )

assume u in {1bag} ; :: thesis: u in {(EmptyBag n),1bag}

then u = 1bag by TARSKI:def 1;

hence u in {(EmptyBag n),1bag} by TARSKI:def 2; :: thesis: verum

end;assume u in {1bag} ; :: thesis: u in {(EmptyBag n),1bag}

then u = 1bag by TARSKI:def 1;

hence u in {(EmptyBag n),1bag} by TARSKI:def 2; :: thesis: verum

then A39: {1bag} \/ {(EmptyBag n),1bag} = {(EmptyBag n),1bag} by XBOOLE_1:12;

A40: (q - p) . 1bag = (q + (- p)) . 1bag by POLYNOM1:def 7

.= (q . 1bag) + ((- p) . 1bag) by POLYNOM1:15

.= (q . 1bag) + (- (p . 1bag)) by POLYNOM1:17

.= (1. L) + (- (1. L)) by A20, A14, FUNCT_7:31

.= 0. L by RLVECT_1:5 ;

Support (q - p) = Support (q + (- p)) by POLYNOM1:def 7;

then Support (q - p) c= (Support q) \/ (Support (- p)) by POLYNOM1:20;

then A41: Support (q - p) c= {1bag} \/ {(EmptyBag n),1bag} by A25, A16, Th5;

assume A42: u in Support (q - p) ; :: thesis: u in {(EmptyBag n)}

then (q - p) . u <> 0. L by POLYNOM1:def 4;

then u = EmptyBag n by A42, A41, A39, A40, TARSKI:def 2;

hence u in {(EmptyBag n)} by TARSKI:def 1; :: thesis: verum

then 0_ (n,L),q - p are_convergent_wrt PolyRedRel (P,T) by A37, A36, REWRITE1:def 24;

then consider c being object such that

A43: PolyRedRel (P,T) reduces 0_ (n,L),c and

A44: PolyRedRel (P,T) reduces q - p,c by REWRITE1:def 7;

reconsider c = c as Polynomial of n,L by A43, Lm4;

consider s being FinSequence such that

A45: len s > 0 and

A46: s . 1 = 0_ (n,L) and

A47: s . (len s) = c and

A48: for i being Nat st i in dom s & i + 1 in dom s holds

[(s . i),(s . (i + 1))] in PolyRedRel (P,T) by A43, REWRITE1:11;

now :: thesis: not len s <> 1

then consider s being FinSequence such that A49:
0 + 1 <= len s
by A45, NAT_1:13;

A50: dom s = Seg (len s) by FINSEQ_1:def 3;

assume len s <> 1 ; :: thesis: contradiction

then 1 < len s by A49, XXREAL_0:1;

then 1 + 1 <= len s by NAT_1:13;

then A51: 1 + 1 in dom s by A50, FINSEQ_1:1;

A52: 1 in dom s by A49, A50, FINSEQ_1:1;

then consider f9, h9 being object such that

A53: [(0_ (n,L)),(s . 2)] = [f9,h9] and

f9 in NonZero (Polynom-Ring (n,L)) and

A54: h9 in the carrier of (Polynom-Ring (n,L)) by A46, A48, A51, RELSET_1:2;

s . 2 = h9 by A53, XTUPLE_0:1;

then reconsider c9 = s . 2 as Polynomial of n,L by A54, POLYNOM1:def 11;

[(s . 1),(s . 2)] in PolyRedRel (P,T) by A48, A52, A51;

then 0_ (n,L) reduces_to c9,P,T by A46, POLYRED:def 13;

then consider g being Polynomial of n,L such that

g in P and

A55: 0_ (n,L) reduces_to c9,g,T by POLYRED:def 7;

0_ (n,L) is_reducible_wrt g,T by A55, POLYRED:def 8;

hence contradiction by POLYRED:37; :: thesis: verum

end;A50: dom s = Seg (len s) by FINSEQ_1:def 3;

assume len s <> 1 ; :: thesis: contradiction

then 1 < len s by A49, XXREAL_0:1;

then 1 + 1 <= len s by NAT_1:13;

then A51: 1 + 1 in dom s by A50, FINSEQ_1:1;

A52: 1 in dom s by A49, A50, FINSEQ_1:1;

then consider f9, h9 being object such that

A53: [(0_ (n,L)),(s . 2)] = [f9,h9] and

f9 in NonZero (Polynom-Ring (n,L)) and

A54: h9 in the carrier of (Polynom-Ring (n,L)) by A46, A48, A51, RELSET_1:2;

s . 2 = h9 by A53, XTUPLE_0:1;

then reconsider c9 = s . 2 as Polynomial of n,L by A54, POLYNOM1:def 11;

[(s . 1),(s . 2)] in PolyRedRel (P,T) by A48, A52, A51;

then 0_ (n,L) reduces_to c9,P,T by A46, POLYRED:def 13;

then consider g being Polynomial of n,L such that

g in P and

A55: 0_ (n,L) reduces_to c9,g,T by POLYRED:def 7;

0_ (n,L) is_reducible_wrt g,T by A55, POLYRED:def 8;

hence contradiction by POLYRED:37; :: thesis: verum

A56: len s > 0 and

A57: s . 1 = q - p and

A58: s . (len s) = 0_ (n,L) and

A59: for i being Nat st i in dom s & i + 1 in dom s holds

[(s . i),(s . (i + 1))] in PolyRedRel (P,T) by A44, A46, A47, REWRITE1:11;

A60: now :: thesis: not - (1. L) = 0. L

assume
- (1. L) = 0. L
; :: thesis: contradiction

then - (- (1. L)) = 0. L by RLVECT_1:12;

hence contradiction by RLVECT_1:17; :: thesis: verum

end;then - (- (1. L)) = 0. L by RLVECT_1:12;

hence contradiction by RLVECT_1:17; :: thesis: verum

now :: thesis: for u being object st u in {(EmptyBag n)} holds

u in Support (q - p)

then A62:
Support (q - p) = {(EmptyBag n)}
by A38, TARSKI:2;u in Support (q - p)

let u be object ; :: thesis: ( u in {(EmptyBag n)} implies u in Support (q - p) )

assume A61: u in {(EmptyBag n)} ; :: thesis: u in Support (q - p)

then reconsider u9 = u as Element of Bags n by TARSKI:def 1;

(q - p) . u9 = (q + (- p)) . u9 by POLYNOM1:def 7

.= (q . u9) + ((- p) . u9) by POLYNOM1:15

.= (q . u9) + (- (p . u9)) by POLYNOM1:17

.= (0. L) + (- (p . u9)) by A9, A61, TARSKI:def 1

.= (0. L) + (- (1. L)) by A23, A61, TARSKI:def 1

.= - (1. L) by ALGSTR_1:def 2 ;

hence u in Support (q - p) by A60, POLYNOM1:def 4; :: thesis: verum

end;assume A61: u in {(EmptyBag n)} ; :: thesis: u in Support (q - p)

then reconsider u9 = u as Element of Bags n by TARSKI:def 1;

(q - p) . u9 = (q + (- p)) . u9 by POLYNOM1:def 7

.= (q . u9) + ((- p) . u9) by POLYNOM1:15

.= (q . u9) + (- (p . u9)) by POLYNOM1:17

.= (0. L) + (- (p . u9)) by A9, A61, TARSKI:def 1

.= (0. L) + (- (1. L)) by A23, A61, TARSKI:def 1

.= - (1. L) by ALGSTR_1:def 2 ;

hence u in Support (q - p) by A60, POLYNOM1:def 4; :: thesis: verum

A63: now :: thesis: not q - p is_reducible_wrt P,T

assume
q - p is_reducible_wrt P,T
; :: thesis: contradiction

then consider g being Polynomial of n,L such that

A64: q - p reduces_to g,P,T by POLYRED:def 9;

consider h being Polynomial of n,L such that

A65: h in P and

A66: q - p reduces_to g,h,T by A64, POLYRED:def 7;

ex b being bag of n st q - p reduces_to g,h,b,T by A66, POLYRED:def 6;

then h <> 0_ (n,L) by POLYRED:def 5;

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

q - p is_reducible_wrt h,T by A66, POLYRED:def 8;

then consider b9 being bag of n such that

A67: b9 in Support (q - p) and

A68: HT (h,T) divides b9 by POLYRED:36;

A69: HT (h,T) = 1bag

hence contradiction by A8, A68, A69, PRE_POLY:58; :: thesis: verum

end;then consider g being Polynomial of n,L such that

A64: q - p reduces_to g,P,T by POLYRED:def 9;

consider h being Polynomial of n,L such that

A65: h in P and

A66: q - p reduces_to g,h,T by A64, POLYRED:def 7;

ex b being bag of n st q - p reduces_to g,h,b,T by A66, POLYRED:def 6;

then h <> 0_ (n,L) by POLYRED:def 5;

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

q - p is_reducible_wrt h,T by A66, POLYRED:def 8;

then consider b9 being bag of n such that

A67: b9 in Support (q - p) and

A68: HT (h,T) divides b9 by POLYRED:36;

A69: HT (h,T) = 1bag

proof

end;

b9 = EmptyBag n
by A62, A67, TARSKI:def 1;now :: thesis: ( ( h = p & HT (h,T) = 1bag ) or ( h = q & HT (h,T) = 1bag ) )

hence
HT (h,T) = 1bag
; :: thesis: verumend;

hence contradiction by A8, A68, A69, PRE_POLY:58; :: thesis: verum

now :: thesis: not len s <> 1

hence
contradiction
by A34, A57, A58; :: thesis: verumA70:
0 + 1 <= len s
by A56, NAT_1:13;

A71: dom s = Seg (len s) by FINSEQ_1:def 3;

assume len s <> 1 ; :: thesis: contradiction

then 1 < len s by A70, XXREAL_0:1;

then 1 + 1 <= len s by NAT_1:13;

then A72: 1 + 1 in dom s by A71, FINSEQ_1:1;

A73: 1 in dom s by A70, A71, FINSEQ_1:1;

then consider f9, h9 being object such that

A74: [(q - p),(s . 2)] = [f9,h9] and

f9 in NonZero (Polynom-Ring (n,L)) and

A75: h9 in the carrier of (Polynom-Ring (n,L)) by A57, A59, A72, RELSET_1:2;

s . 2 = h9 by A74, XTUPLE_0:1;

then reconsider c9 = s . 2 as Polynomial of n,L by A75, POLYNOM1:def 11;

[(q - p),(s . 2)] in PolyRedRel (P,T) by A57, A59, A73, A72;

then q - p reduces_to c9,P,T by POLYRED:def 13;

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

end;A71: dom s = Seg (len s) by FINSEQ_1:def 3;

assume len s <> 1 ; :: thesis: contradiction

then 1 < len s by A70, XXREAL_0:1;

then 1 + 1 <= len s by NAT_1:13;

then A72: 1 + 1 in dom s by A71, FINSEQ_1:1;

A73: 1 in dom s by A70, A71, FINSEQ_1:1;

then consider f9, h9 being object such that

A74: [(q - p),(s . 2)] = [f9,h9] and

f9 in NonZero (Polynom-Ring (n,L)) and

A75: h9 in the carrier of (Polynom-Ring (n,L)) by A57, A59, A72, RELSET_1:2;

s . 2 = h9 by A74, XTUPLE_0:1;

then reconsider c9 = s . 2 as Polynomial of n,L by A75, POLYNOM1:def 11;

[(q - p),(s . 2)] in PolyRedRel (P,T) by A57, A59, A73, A72;

then q - p reduces_to c9,P,T by POLYRED:def 13;

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