let n be Ordinal; :: thesis:
let T be connected admissible TermOrder of n; :: thesis:
let L be non empty non degenerated right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative doubleLoopStr ; :: thesis:
let f, g be Polynomial of n,L; :: thesis:
let f9, g9 be Element of (Polynom-Ring (n,L)); :: thesis:
assume A1: ( f = f9 & g = g9 ) ; :: thesis:
defpred S₁[ Nat] means for f, g being Polynomial of n,L
for f9, g9 being Element of (Polynom-Ring (n,L)) st f = f9 & g = g9 holds
for P being non empty Subset of (Polynom-Ring (n,L))
for R being RedSequence of PolyRedRel (P,T) st R . 1 = f & R . (len R) = g & len R = $1 holds
ex A being LeftLinearCombination of P st
( f9 = g9 + (Sum A) & ( for i being Element of 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 ) ) );
let P be non empty Subset of (Polynom-Ring (n,L)); :: thesis:
assume PolyRedRel (P,T) reduces f,g ; :: thesis:
then consider R being RedSequence of PolyRedRel (P,T) such that
A2: ( R . 1 = f & R . (len R) = g ) by REWRITE1:def 3;
A3: 0_ (n,L) = 0. (Polynom-Ring (n,L)) by POLYNOM1:def 11;

A4: now :: thesis:

let k be Nat; :: thesis:
assume A5: 1 <= k ; :: thesis:
thus ( S₁[k] implies S₁[k + 1] ) :: thesis:

proof

assume A6: S₁[k] ; :: thesis:
for f, g being Polynomial of n,L
for f9, g9 being Element of (Polynom-Ring (n,L)) st f = f9 & g = g9 holds
for P being non empty Subset of (Polynom-Ring (n,L))
for R being RedSequence of PolyRedRel (P,T) st R . 1 = f & R . (len R) = g & len R = k + 1 holds
ex A being LeftLinearCombination of P st
( f9 = g9 + (Sum A) & ( for i being Element of 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

let f, g be Polynomial of n,L; :: thesis:
let f9, g9 be Element of (Polynom-Ring (n,L)); :: thesis:
assume that
A7: f = f9 and
A8: g = g9 ; :: thesis:
let P be non empty Subset of (Polynom-Ring (n,L)); :: thesis:
let R be RedSequence of PolyRedRel (P,T); :: thesis:
assume that
A9: R . 1 = f and
A10: R . (len R) = g and
A11: len R = k + 1 ; :: thesis:
set Q = R | (Seg k);
reconsider Q = R | (Seg k) as FinSequence by FINSEQ_1:15;
A12: k <= k + 1 by NAT_1:11;
then A13: dom Q = Seg k by A11, FINSEQ_1:17;
A14: dom R = Seg (k + 1) by A11, FINSEQ_1:def 3;

A15: now :: thesis:

let i be Nat; :: thesis:
assume that
A16: i in dom Q and
A17: i + 1 in dom Q ; :: thesis:
i + 1 <= k by A13, A17, FINSEQ_1:1;
then A18: i + 1 <= k + 1 by A12, XXREAL_0:2;
i <= k by A13, A16, FINSEQ_1:1;
then A19: i <= k + 1 by A12, XXREAL_0:2;
1 <= i + 1 by A13, A17, FINSEQ_1:1;
then A20: i + 1 in dom R by A14, A18, FINSEQ_1:1;
1 <= i by A13, A16, FINSEQ_1:1;
then i in dom R by A14, A19, FINSEQ_1:1;
then A21: [(R . i),(R . (i + 1))] in PolyRedRel (P,T) by A20, REWRITE1:def 2;
R . i = Q . i by A16, FUNCT_1:47;
hence [(Q . i),(Q . (i + 1))] in PolyRedRel (P,T) by A17, A21, FUNCT_1:47; :: thesis:

end;

len Q = k by A11, A12, FINSEQ_1:17;
then reconsider Q = Q as RedSequence of PolyRedRel (P,T) by A5, A15, REWRITE1:def 2;
A22: 1 in dom Q by A5, A13, FINSEQ_1:1;
then A23: Q . 1 = f by A9, FUNCT_1:47;
1 <= k + 1 by NAT_1:11;
then A24: k + 1 in dom R by A14, FINSEQ_1:1;
k in dom R by A5, A14, A12, FINSEQ_1:1;
then A25: [(R . k),(R . (k + 1))] in PolyRedRel (P,T) by A24, REWRITE1:def 2;
then consider h9, g2 being object such that
A26: [(R . k),(R . (k + 1))] = [h9,g2] and
A27: h9 in NonZero (Polynom-Ring (n,L)) and
A28: g2 in the carrier of (Polynom-Ring (n,L)) by RELSET_1:2;
A29: R . k = h9 by A26, XTUPLE_0:1;
reconsider g2 = g2 as Polynomial of n,L by A28, POLYNOM1:def 11;
not h9 in {(0_ (n,L))} by A3, A27, XBOOLE_0:def 5;
then h9 <> 0_ (n,L) by TARSKI:def 1;
then reconsider h9 = h9 as non-zero Polynomial of n,L by A27, POLYNOM1:def 11, POLYNOM7:def 1;
A30: Q . k = h9 by A5, A13, A29, FINSEQ_1:3, FUNCT_1:47;
then reconsider u9 = Q . k as Element of (Polynom-Ring (n,L)) by POLYNOM1:def 11;
reconsider u = u9 as Polynomial of n,L by POLYNOM1:def 11;
Q . (len Q) = u by A11, A12, FINSEQ_1:17;
then consider A9 being LeftLinearCombination of P such that
A31: f9 = u9 + (Sum A9) and
A32: for i being Element of NAT st i in dom A9 holds
ex m being non-zero Monomial of n,L ex p being non-zero Polynomial of n,L st
( p in P & A9 . i = m *' p & HT ((m *' p),T) <= HT (f,T),T ) by A6, A7, A11, A12, A23, FINSEQ_1:17;
A33: k in dom Q by A5, A13, FINSEQ_1:3;

now :: thesis:

per cases ;

case u9 = g9 ; :: thesis:

hence ex A being LeftLinearCombination of P st
( f9 = g9 + (Sum A) & ( for i being Element of 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 ) ) ) by A31, A32; :: thesis:

end;

case A34: u9 <> g9 ; :: thesis:

reconsider hh = h9 as Element of (Polynom-Ring (n,L)) by POLYNOM1:def 11;
A35: PolyRedRel (P,T) reduces f,h9 by A5, A33, A30, A22, A23, REWRITE1:17;
A36: R . (k + 1) = g2 by A26, XTUPLE_0:1;
then reconsider gg = g2 as Element of (Polynom-Ring (n,L)) by A8, A10, A11;
h9 reduces_to g2,P,T by A25, A26, POLYRED:def 13;
then consider p9 being Polynomial of n,L such that
A37: p9 in P and
A38: h9 reduces_to g2,p9,T by POLYRED:def 7;
consider m9 being Monomial of n,L such that
A39: g2 = h9 - (m9 *' p9) and
not HT ((m9 *' p9),T) in Support g2 and
A40: HT ((m9 *' p9),T) <= HT (h9,T),T by A38, GROEB_1:2;

A41: now :: thesis:

assume p9 = 0_ (n,L) ; :: thesis:
then g2 = h9 - (0_ (n,L)) by A39, POLYRED:5
.= Q . k by A30, POLYRED:4 ;
hence contradiction by A8, A10, A11, A34, A36; :: thesis:

end;

A42: now :: thesis:

assume m9 = 0_ (n,L) ; :: thesis:
then g2 = h9 - (0_ (n,L)) by A39, POLYRED:5
.= Q . k by A30, POLYRED:4 ;
hence contradiction by A8, A10, A11, A34, A36; :: thesis:

end;

reconsider mp = m9 *' p9 as Element of (Polynom-Ring (n,L)) by POLYNOM1:def 11;
reconsider pp = p9 as Element of P by A37;
set B = A9 ^ <*mp*>;
reconsider mm = m9 as Element of (Polynom-Ring (n,L)) by POLYNOM1:def 11;
A43: gg = hh - mp by A39, Lm3;
reconsider m9 = m9 as non-zero Monomial of n,L by A42, POLYNOM7:def 1;
reconsider p9 = p9 as non-zero Polynomial of n,L by A41, POLYNOM7:def 1;
len (A9 ^ <*mp*>) = (len A9) + (len <*(m9 *' p9)*>) by FINSEQ_1:22
.= (len A9) + 1 by FINSEQ_1:40 ;
then A44: dom (A9 ^ <*mp*>) = Seg ((len A9) + 1) by FINSEQ_1:def 3;
A45: mp = mm * pp by POLYNOM1:def 11;

now :: thesis:

let i be set ; :: thesis:
assume A46: i in dom (A9 ^ <*mp*>) ; :: thesis:
then reconsider j = i as Element of NAT ;
A47: j <= (len A9) + 1 by A44, A46, FINSEQ_1:1;
A48: 1 <= j by A44, A46, FINSEQ_1:1;

now :: thesis:

per cases ;

case j = (len A9) + 1 ; :: thesis:

then mp = (A9 ^ <*mp*>) . j by FINSEQ_1:42
.= (A9 ^ <*mp*>) /. j by A46, PARTFUN1:def 6 ;
hence ex u being Element of (Polynom-Ring (n,L)) ex a being Element of P st (A9 ^ <*mp*>) /. i = u * a by A45; :: thesis:

end;

case j <> (len A9) + 1 ; :: thesis:

then j < (len A9) + 1 by A47, XXREAL_0:1;
then j <= len A9 by NAT_1:13;
then j in Seg (len A9) by A48, FINSEQ_1:1;
then A49: j in dom A9 by FINSEQ_1:def 3;
then consider m being non-zero Monomial of n,L, p being non-zero Polynomial of n,L such that
A50: p in P and
A51: A9 . j = m *' p and
HT ((m *' p),T) <= HT (f,T),T by A32;
reconsider a9 = p as Element of P by A50;
reconsider u9 = m as Element of (Polynom-Ring (n,L)) by POLYNOM1:def 11;
A52: (A9 ^ <*mp*>) . j = (A9 ^ <*mp*>) /. j by A46, PARTFUN1:def 6;
u9 * a9 = m *' p by POLYNOM1:def 11
.= (A9 ^ <*mp*>) /. j by A49, A51, A52, FINSEQ_1:def 7 ;
hence ex u being Element of (Polynom-Ring (n,L)) ex a being Element of P st (A9 ^ <*mp*>) /. i = u * a ; :: thesis:

end;

hence ex u being Element of (Polynom-Ring (n,L)) ex a being Element of P st (A9 ^ <*mp*>) /. i = u * a ; :: thesis:

end;

then reconsider B = A9 ^ <*mp*> as LeftLinearCombination of P by IDEAL_1:def 9;
h9 is_reducible_wrt p9,T by A38, POLYRED:def 8;
then h9 <> 0_ (n,L) by POLYRED:37;
then HT (h9,T) <= HT (f,T),T by A35, POLYRED:44;
then A53: HT ((m9 *' p9),T) <= HT (f,T),T by A40, TERMORD:8;

A54: now :: thesis:

let i be Element of NAT ; :: thesis:
assume A55: i in dom B ; :: thesis:
then A56: i <= (len A9) + 1 by A44, FINSEQ_1:1;
A57: 1 <= i by A44, A55, FINSEQ_1:1;

now :: thesis:

per cases ;

case i = (len A9) + 1 ; :: thesis:

hence ex m being non-zero Monomial of n,L ex p being non-zero Polynomial of n,L st
( p in P & B . i = m *' p & HT ((m *' p),T) <= HT (f,T),T ) by A37, A53, FINSEQ_1:42; :: thesis:

end;

case i <> (len A9) + 1 ; :: thesis:

then i < (len A9) + 1 by A56, XXREAL_0:1;
then i <= len A9 by NAT_1:13;
then i in Seg (len A9) by A57, FINSEQ_1:1;
then A58: i in dom A9 by FINSEQ_1:def 3;
then consider m being non-zero Monomial of n,L, p being non-zero Polynomial of n,L such that
A59: p in P and
A60: A9 . i = m *' p and
A61: HT ((m *' p),T) <= HT (f,T),T by A32;
B . i = m *' p by A58, A60, FINSEQ_1:def 7;
hence ex m being non-zero Monomial of n,L ex p being non-zero Polynomial of n,L st
( p in P & B . i = m *' p & HT ((m *' p),T) <= HT (f,T),T ) by A59, A61; :: thesis:

end;

hence ex m being non-zero Monomial of n,L ex p being non-zero Polynomial of n,L st
( p in P & B . i = m *' p & HT ((m *' p),T) <= HT (f,T),T ) ; :: thesis:

end;

take B = B; :: thesis:
gg + (Sum B) = gg + ((Sum A9) + (Sum <*mp*>)) by RLVECT_1:41
.= gg + ((Sum A9) + mp) by RLVECT_1:44
.= (hh + (- mp)) + ((Sum A9) + mp) by A43
.= hh + ((- mp) + ((Sum A9) + mp)) by RLVECT_1:def 3
.= hh + ((Sum A9) + ((- mp) + mp)) by RLVECT_1:def 3
.= hh + ((Sum A9) + (0. (Polynom-Ring (n,L)))) by RLVECT_1:5
.= hh + (Sum A9) by RLVECT_1:4
.= f9 by A5, A13, A29, A31, FINSEQ_1:3, FUNCT_1:47 ;
hence ex A being LeftLinearCombination of P st
( f9 = g9 + (Sum A) & ( for i being Element of 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 ) ) ) by A8, A10, A11, A36, A54; :: thesis:

end;

hence S₁[k + 1] ; :: thesis:

end;

A62: S₁[1]

proof

set A = <*> the carrier of (Polynom-Ring (n,L));
let f, g be Polynomial of n,L; :: thesis:
let f9, g9 be Element of (Polynom-Ring (n,L)); :: thesis:
assume A63: ( f = f9 & g = g9 ) ; :: thesis:
let P be non empty Subset of (Polynom-Ring (n,L)); :: thesis:
let R be RedSequence of PolyRedRel (P,T); :: thesis:
for i being set st i in dom (<*> the carrier of (Polynom-Ring (n,L))) holds
ex u being Element of (Polynom-Ring (n,L)) ex a being Element of P st (<*> the carrier of (Polynom-Ring (n,L))) /. i = u * a ;
then reconsider A = <*> the carrier of (Polynom-Ring (n,L)) as LeftLinearCombination of P by IDEAL_1:def 9;
assume A64: ( R . 1 = f & R . (len R) = g & len R = 1 ) ; :: thesis:
take A ; :: thesis:
f9 = g9 + (0. (Polynom-Ring (n,L))) by A63, A64, RLVECT_1:def 4
.= g9 + (Sum A) by RLVECT_1:43 ;
hence ( f9 = g9 + (Sum A) & ( for i being Element of 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 ) ) ) ; :: thesis:

end;

A65: for k being Nat st 1 <= k holds
S₁[k] from NAT_1:sch 8(A62, A4);
1 <= len R by NAT_1:14;
hence ex A being LeftLinearCombination of P st
( f9 = g9 + (Sum A) & ( for i being Element of 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 ) ) ) by A1, A65, A2; :: thesis: