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 P being Subset of (Polynom-Ring (n,L))
for f, g being Polynomial of n,L
for m being Monomial of n,L st PolyRedRel (P,T) reduces f,g holds
PolyRedRel (P,T) reduces m *' f,m *' g
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 P being Subset of (Polynom-Ring (n,L))
for f, g being Polynomial of n,L
for m being Monomial of n,L st PolyRedRel (P,T) reduces f,g holds
PolyRedRel (P,T) reduces m *' f,m *' g
let L be non empty non degenerated right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative doubleLoopStr ; for P being Subset of (Polynom-Ring (n,L))
for f, g being Polynomial of n,L
for m being Monomial of n,L st PolyRedRel (P,T) reduces f,g holds
PolyRedRel (P,T) reduces m *' f,m *' g
let P be Subset of (Polynom-Ring (n,L)); for f, g being Polynomial of n,L
for m being Monomial of n,L st PolyRedRel (P,T) reduces f,g holds
PolyRedRel (P,T) reduces m *' f,m *' g
let f, g be Polynomial of n,L; for m being Monomial of n,L st PolyRedRel (P,T) reduces f,g holds
PolyRedRel (P,T) reduces m *' f,m *' g
let m be Monomial of n,L; ( PolyRedRel (P,T) reduces f,g implies PolyRedRel (P,T) reduces m *' f,m *' g )
assume A1:
PolyRedRel (P,T) reduces f,g
; PolyRedRel (P,T) reduces m *' f,m *' g
set R = PolyRedRel (P,T);
per cases
( m = 0_ (n,L) or m <> 0_ (n,L) )
;
suppose
m <> 0_ (
n,
L)
;
PolyRedRel (P,T) reduces m *' f,m *' gthen reconsider m =
m as
non-zero Monomial of
n,
L by POLYNOM7:def 1;
defpred S1[
Nat]
means for
f,
g being
Polynomial of
n,
L st
PolyRedRel (
P,
T)
reduces f,
g holds
for
p being
RedSequence of
PolyRedRel (
P,
T) st
p . 1
= f &
p . (len p) = g &
len p = $1 holds
PolyRedRel (
P,
T)
reduces m *' f,
m *' g;
consider p being
RedSequence of
PolyRedRel (
P,
T)
such that A3:
(
p . 1
= f &
p . (len p) = g )
by A1, REWRITE1:def 3;
consider k being
Nat such that A4:
len p = k
;
A5:
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 A6:
1
<= k
;
( S1[k] implies S1[k + 1] )thus
(
S1[
k] implies
S1[
k + 1] )
verumproof
assume A7:
S1[
k]
;
S1[k + 1]
now for f, g being Polynomial of n,L st PolyRedRel (P,T) reduces f,g holds
for p being RedSequence of PolyRedRel (P,T) st p . 1 = f & p . (len p) = g & len p = k + 1 holds
PolyRedRel (P,T) reduces m *' f,m *' glet f,
g be
Polynomial of
n,
L;
( PolyRedRel (P,T) reduces f,g implies for p being RedSequence of PolyRedRel (P,T) st p . 1 = f & p . (len p) = g & len p = k + 1 holds
PolyRedRel (P,T) reduces m *' f,m *' g )assume
PolyRedRel (
P,
T)
reduces f,
g
;
for p being RedSequence of PolyRedRel (P,T) st p . 1 = f & p . (len p) = g & len p = k + 1 holds
PolyRedRel (P,T) reduces m *' f,m *' glet p be
RedSequence of
PolyRedRel (
P,
T);
( p . 1 = f & p . (len p) = g & len p = k + 1 implies PolyRedRel (P,T) reduces m *' f,m *' g )assume that A8:
p . 1
= f
and A9:
p . (len p) = g
and A10:
len p = k + 1
;
PolyRedRel (P,T) reduces m *' f,m *' gA11:
dom p = Seg (k + 1)
by A10, FINSEQ_1:def 3;
then A12:
k + 1
in dom p
by FINSEQ_1:4;
set q =
p | (Seg k);
reconsider q =
p | (Seg k) as
FinSequence by FINSEQ_1:15;
A13:
k <= k + 1
by NAT_1:11;
then A14:
dom q = Seg k
by A10, FINSEQ_1:17;
then A15:
k in dom q
by A6, FINSEQ_1:1;
set h =
q . (len q);
A16:
len q = k
by A10, A13, FINSEQ_1:17;
k in dom p
by A6, A11, A13, FINSEQ_1:1;
then
[(p . k),(p . (k + 1))] in PolyRedRel (
P,
T)
by A12, REWRITE1:def 2;
then A17:
[(q . (len q)),g] in PolyRedRel (
P,
T)
by A9, A10, A16, A15, FUNCT_1:47;
then consider h9,
g9 being
object such that A18:
[(q . (len q)),g] = [h9,g9]
and A19:
h9 in NonZero (Polynom-Ring (n,L))
and
g9 in the
carrier of
(Polynom-Ring (n,L))
by RELSET_1:2;
A20:
q . (len q) = h9
by A18, XTUPLE_0:1;
A21:
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 A22:
i in dom q
and A23:
i + 1
in dom q
;
[(q . i),(q . (i + 1))] in PolyRedRel (P,T)
i + 1
<= k
by A14, A23, FINSEQ_1:1;
then A24:
i + 1
<= k + 1
by A13, XXREAL_0:2;
i <= k
by A14, A22, FINSEQ_1:1;
then A25:
i <= k + 1
by A13, XXREAL_0:2;
1
<= i + 1
by A14, A23, FINSEQ_1:1;
then A26:
i + 1
in dom p
by A11, A24, FINSEQ_1:1;
1
<= i
by A14, A22, FINSEQ_1:1;
then
i in dom p
by A11, A25, FINSEQ_1:1;
then A27:
[(p . i),(p . (i + 1))] in PolyRedRel (
P,
T)
by A26, REWRITE1:def 2;
p . i = q . i
by A22, FUNCT_1:47;
hence
[(q . i),(q . (i + 1))] in PolyRedRel (
P,
T)
by A23, A27, FUNCT_1:47;
verum end;
0_ (
n,
L)
= 0. (Polynom-Ring (n,L))
by POLYNOM1:def 11;
then
not
h9 in {(0_ (n,L))}
by A19, XBOOLE_0:def 5;
then
h9 <> 0_ (
n,
L)
by TARSKI:def 1;
then reconsider h =
q . (len q) as
non-zero Polynomial of
n,
L by A19, A20, POLYNOM1:def 11, POLYNOM7:def 1;
h reduces_to g,
P,
T
by A17, Def13;
then
m *' h reduces_to m *' g,
P,
T
by Th46;
then
[(m *' h),(m *' g)] in PolyRedRel (
P,
T)
by Def13;
then A28:
PolyRedRel (
P,
T)
reduces m *' h,
m *' g
by REWRITE1:15;
reconsider q =
q as
RedSequence of
PolyRedRel (
P,
T)
by A6, A16, A21, REWRITE1:def 2;
1
in dom q
by A6, A14, FINSEQ_1:1;
then A29:
q . 1
= f
by A8, FUNCT_1:47;
then
PolyRedRel (
P,
T)
reduces f,
h
by REWRITE1:def 3;
then
PolyRedRel (
P,
T)
reduces m *' f,
m *' h
by A7, A10, A13, A29, FINSEQ_1:17;
hence
PolyRedRel (
P,
T)
reduces m *' f,
m *' g
by A28, REWRITE1:16;
verum end;
hence
S1[
k + 1]
;
verum
end; end; A30:
S1[1]
by REWRITE1:12;
A31:
for
k being
Nat st 1
<= k holds
S1[
k]
from NAT_1:sch 8(A30, A5);
1
<= k
by A4, NAT_1:14;
hence
PolyRedRel (
P,
T)
reduces m *' f,
m *' g
by A1, A31, A3, A4;
verum end; end;