let n be Ordinal; 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 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)) st PolyRedRel (P,T) reduces f,g 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 T be 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 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)) st PolyRedRel (P,T) reduces f,g 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 L be non empty non degenerated right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative doubleLoopStr ; 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)) st PolyRedRel (P,T) reduces f,g 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 f, g be 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)) st PolyRedRel (P,T) reduces f,g 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 f9, g9 be Element of (Polynom-Ring (n,L)); ( f = f9 & g = g9 implies 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
( 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 ) ) ) )
assume A1:
( f = f9 & g = g9 )
; 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
( 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 ) ) )
defpred S1[ 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)); ( PolyRedRel (P,T) reduces f,g implies 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 ) ) ) )
assume
PolyRedRel (P,T) reduces f,g
; 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 ) ) )
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 for k being Nat st 1 <= k & S1[k] holds
S1[k + 1]let k be
Nat;
( 1 <= k & S1[k] implies S1[k + 1] )assume A5:
1
<= k
;
( S1[k] implies S1[k + 1] )thus
(
S1[
k] implies
S1[
k + 1] )
verumproof
assume A6:
S1[
k]
;
S1[k + 1]
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;
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 ) ) )let f9,
g9 be
Element of
(Polynom-Ring (n,L));
( f = f9 & g = g9 implies 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 ) ) ) )
assume that A7:
f = f9
and A8:
g = g9
;
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 ) ) )
let P be 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 ) ) )let R be
RedSequence of
PolyRedRel (
P,
T);
( R . 1 = f & R . (len R) = g & len R = k + 1 implies 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 ) ) ) )
assume that A9:
R . 1
= f
and A10:
R . (len R) = g
and A11:
len R = k + 1
;
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 ) ) )
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 for i being Nat st i in dom Q & i + 1 in dom Q holds
[(Q . i),(Q . (i + 1))] in PolyRedRel (P,T)let i be
Nat;
( i in dom Q & i + 1 in dom Q implies [(Q . i),(Q . (i + 1))] in PolyRedRel (P,T) )assume that A16:
i in dom Q
and A17:
i + 1
in dom Q
;
[(Q . i),(Q . (i + 1))] in PolyRedRel (P,T)
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;
verum 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 ( ( u9 = g9 & 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 ) ) ) ) or ( u9 <> g9 & ex B, 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 ) ) ) ) )per cases
( u9 = g9 or u9 <> g9 )
;
case A34:
u9 <> g9
;
ex B, 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 ) ) )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 not p9 = 0_ (n,L)end; A42:
now not m9 = 0_ (n,L)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 for i being set st i in dom (A9 ^ <*mp*>) holds
ex u being Element of (Polynom-Ring (n,L)) ex a being Element of P st (A9 ^ <*mp*>) /. i = u * alet i be
set ;
( i in dom (A9 ^ <*mp*>) implies ex u being Element of (Polynom-Ring (n,L)) ex a being Element of P st (A9 ^ <*mp*>) /. i = u * a )assume A46:
i in dom (A9 ^ <*mp*>)
;
ex u being Element of (Polynom-Ring (n,L)) ex a being Element of P st (A9 ^ <*mp*>) /. i = u * athen 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 ( ( j = (len A9) + 1 & ex u being Element of (Polynom-Ring (n,L)) ex a being Element of P st (A9 ^ <*mp*>) /. i = u * a ) or ( j <> (len A9) + 1 & ex u being Element of (Polynom-Ring (n,L)) ex a being Element of P st (A9 ^ <*mp*>) /. i = u * a ) )per cases
( j = (len A9) + 1 or j <> (len A9) + 1 )
;
case
j <> (len A9) + 1
;
ex u being Element of (Polynom-Ring (n,L)) ex a being Element of P st (A9 ^ <*mp*>) /. i = u * athen
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
;
verum end; end; end; hence
ex
u being
Element of
(Polynom-Ring (n,L)) ex
a being
Element of
P st
(A9 ^ <*mp*>) /. i = u * a
;
verum 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 for i being Element of NAT st i in dom B holds
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 )let i be
Element of
NAT ;
( i in dom B implies 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 ) )assume A55:
i in dom B
;
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 )then A56:
i <= (len A9) + 1
by A44, FINSEQ_1:1;
A57:
1
<= i
by A44, A55, FINSEQ_1:1;
now ( ( i = (len A9) + 1 & 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 ) ) or ( i <> (len A9) + 1 & 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 ) ) )per cases
( i = (len A9) + 1 or i <> (len A9) + 1 )
;
case
i <> (len A9) + 1
;
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 )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;
verum end; end; 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 )
;
verum end; take B =
B;
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 ) ) )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;
verum end; end; end;
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 ) ) )
;
verum
end;
hence
S1[
k + 1]
;
verum
end; end;
A62:
S1[1]
proof
set A =
<*> the
carrier of
(Polynom-Ring (n,L));
let f,
g be
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 f9,
g9 be
Element of
(Polynom-Ring (n,L));
( f = f9 & g = g9 implies 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 ) ) ) )
assume A63:
(
f = f9 &
g = g9 )
;
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));
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 R be
RedSequence of
PolyRedRel (
P,
T);
( R . 1 = f & R . (len R) = g & len R = 1 implies 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 ) ) ) )
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 )
;
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 ) ) )
take
A
;
( 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 ) ) )
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 ) ) )
;
verum
end;
A65:
for k being Nat st 1 <= k holds
S1[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; verum