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 associative commutative well-unital distributive Abelian add-associative right_zeroed 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 27;

A4: now

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:19;
A12: k <= k + 1 by NAT_1:11;
then A13: dom Q = Seg k by A11, FINSEQ_1:21;
A14: dom R = Seg (k + 1) by A11, FINSEQ_1:def 3;

A15: now

let i be Element of 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:3;
then A18: i + 1 <= k + 1 by A12, XXREAL_0:2;
i <= k by A13, A16, FINSEQ_1:3;
then A19: i <= k + 1 by A12, XXREAL_0:2;
1 <= i + 1 by A13, A17, FINSEQ_1:3;
then A20: i + 1 in dom R by A14, A18, FINSEQ_1:3;
1 <= i by A13, A16, FINSEQ_1:3;
then i in dom R by A14, A19, FINSEQ_1:3;
then A21: [(R . i),(R . (i + 1))] in PolyRedRel P,T by A20, REWRITE1:def 2;
R . i = Q . i by A16, FUNCT_1:70;
hence [(Q . i),(Q . (i + 1))] in PolyRedRel P,T by A17, A21, FUNCT_1:70; :: thesis:

end;

len Q = k by A11, A12, FINSEQ_1:21;
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:3;
then A23: Q . 1 = f by A9, FUNCT_1:70;
1 <= k + 1 by NAT_1:11;
then A24: k + 1 in dom R by A14, FINSEQ_1:3;
k in dom R by A5, A14, A12, FINSEQ_1:3;
then A25: [(R . k),(R . (k + 1))] in PolyRedRel P,T by A24, REWRITE1:def 2;
then consider h9, g2 being set 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:6;
A29: R . k = [h9,g2] `1 by A26, MCART_1:def 1
.= h9 by MCART_1:def 1 ;
reconsider g2 = g2 as Polynomial of n,L by A28, POLYNOM1:def 27;
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 27, POLYNOM7:def 2;
A30: Q . k = h9 by A5, A13, A29, FINSEQ_1:5, FUNCT_1:70;
then reconsider u9 = Q . k as Element of (Polynom-Ring n,L) by POLYNOM1:def 27;
reconsider u = u9 as Polynomial of n,L by POLYNOM1:def 27;
Q . (len Q) = u by A11, A12, FINSEQ_1:21;
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:21;
A33: k in dom Q by A5, A13, FINSEQ_1:5;

now

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 27;
A35: PolyRedRel P,T reduces f,h9 by A5, A33, A30, A22, A23, REWRITE1:18;
A36: R . (k + 1) = [h9,g2] `2 by A26, MCART_1:def 2
.= g2 by MCART_1:def 2 ;
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

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

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 27;
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 27;
A43: gg = hh - mp by A39, Lm3;
reconsider m9 = m9 as non-zero Monomial of n,L by A42, POLYNOM7:def 2;
reconsider p9 = p9 as non-zero Polynomial of n,L by A41, POLYNOM7:def 2;
len (A9 ^ <*mp*>) = (len A9) + (len <*(m9 *' p9)*>) by FINSEQ_1:35
.= (len A9) + 1 by FINSEQ_1:57 ;
then A44: dom (A9 ^ <*mp*>) = Seg ((len A9) + 1) by FINSEQ_1:def 3;
A45: mp = mm * pp by POLYNOM1:def 27;

now

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:3;
A48: 1 <= j by A44, A46, FINSEQ_1:3;

now

per cases ;

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

then mp = (A9 ^ <*mp*>) . j by FINSEQ_1:59
.= (A9 ^ <*mp*>) /. j by A46, PARTFUN1:def 8 ;
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:3;
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 27;
A52: (A9 ^ <*mp*>) . j = (A9 ^ <*mp*>) /. j by A46, PARTFUN1:def 8;
u9 * a9 = m *' p by POLYNOM1:def 27
.= (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 10;
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

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

now

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:59; :: 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:3;
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:58
.= gg + ((Sum A9) + mp) by RLVECT_1:61
.= (hh + (- mp)) + ((Sum A9) + mp) by A43, RLVECT_1:def 12
.= hh + ((- mp) + ((Sum A9) + mp)) by RLVECT_1:def 6
.= hh + ((Sum A9) + ((- mp) + mp)) by RLVECT_1:def 6
.= hh + ((Sum A9) + (0. (Polynom-Ring n,L))) by RLVECT_1:16
.= hh + (Sum A9) by RLVECT_1:10
.= f9 by A5, A13, A29, A31, FINSEQ_1:5, FUNCT_1:70 ;
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 10;
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 7
.= g9 + (Sum A) by RLVECT_1:60 ;
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);
len R > 0 by REWRITE1:def 2;
then 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: