let n be Ordinal; :: thesis: for T being connected admissible TermOrder of n
for L being non empty non degenerated right_complementable almost_left_invertible associative commutative well-unital distributive Abelian add-associative right_zeroed 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; :: thesis: for L being non empty non degenerated right_complementable almost_left_invertible associative commutative well-unital distributive Abelian add-associative right_zeroed 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 associative commutative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; :: thesis: 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); :: thesis: 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; :: thesis: 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; :: thesis: ( PolyRedRel P,T reduces f,g implies PolyRedRel P,T reduces m *' f,m *' g )
assume A1:
PolyRedRel P,T reduces f,g
; :: thesis: 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
;
:: thesis: PolyRedRel P,T reduces m *' f,m *' gthen reconsider m =
m as
non-zero Monomial of
n,
L by POLYNOM7:def 2;
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;
A3:
S1[1]
by REWRITE1:13;
A4:
now let k be
Nat;
:: thesis: ( 1 <= k & S1[k] implies S1[k + 1] )assume A5:
1
<= k
;
:: thesis: ( S1[k] implies S1[k + 1] )thus
(
S1[
k] implies
S1[
k + 1] )
:: thesis: verumproof
assume A6:
S1[
k]
;
:: thesis: S1[k + 1]
now let f,
g be
Polynomial of
n,
L;
:: thesis: ( 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
;
:: thesis: 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;
:: thesis: ( p . 1 = f & p . (len p) = g & len p = k + 1 implies PolyRedRel P,T reduces m *' f,m *' g )assume A7:
(
p . 1
= f &
p . (len p) = g &
len p = k + 1 )
;
:: thesis: PolyRedRel P,T reduces m *' f,m *' gthen A8:
dom p = Seg (k + 1)
by FINSEQ_1:def 3;
A9:
k <= k + 1
by NAT_1:11;
then A10:
k in dom p
by A5, A8, FINSEQ_1:3;
k + 1
in dom p
by A8, FINSEQ_1:6;
then A11:
[(p . k),(p . (k + 1))] in PolyRedRel P,
T
by A10, REWRITE1:def 2;
set q =
p | (Seg k);
reconsider q =
p | (Seg k) as
FinSequence by FINSEQ_1:19;
set h =
q . (len q);
A12:
len q = k
by A7, A9, FINSEQ_1:21;
A13:
dom q = Seg k
by A7, A9, FINSEQ_1:21;
then
k in dom q
by A5, FINSEQ_1:3;
then A14:
[(q . (len q)),g] in PolyRedRel P,
T
by A7, A11, A12, FUNCT_1:70;
then consider h',
g' being
set such that A15:
(
[(q . (len q)),g] = [h',g'] &
h' in NonZero (Polynom-Ring n,L) &
g' in the
carrier of
(Polynom-Ring n,L) )
by RELSET_1:6;
A16:
q . (len q) =
[h',g'] `1
by A15, MCART_1:def 1
.=
h'
by MCART_1:def 1
;
0_ n,
L = 0. (Polynom-Ring n,L)
by POLYNOM1:def 27;
then
not
h' in {(0_ n,L)}
by A15, XBOOLE_0:def 5;
then
h' <> 0_ n,
L
by TARSKI:def 1;
then reconsider h =
q . (len q) as
non-zero Polynomial of
n,
L by A15, A16, POLYNOM1:def 27, POLYNOM7:def 2;
now let i be
Element of
NAT ;
:: thesis: ( i in dom q & i + 1 in dom q implies [(q . i),(q . (i + 1))] in PolyRedRel P,T )assume A17:
(
i in dom q &
i + 1
in dom q )
;
:: thesis: [(q . i),(q . (i + 1))] in PolyRedRel P,Tthen A18:
( 1
<= i &
i <= k & 1
<= i + 1 &
i + 1
<= k )
by A13, FINSEQ_1:3;
then A19:
(
i <= k + 1 &
i + 1
<= k + 1 )
by A9, XXREAL_0:2;
then A20:
i in dom p
by A8, A18, FINSEQ_1:3;
i + 1
in dom p
by A8, A18, A19, FINSEQ_1:3;
then A21:
[(p . i),(p . (i + 1))] in PolyRedRel P,
T
by A20, REWRITE1:def 2;
p . i = q . i
by A17, FUNCT_1:70;
hence
[(q . i),(q . (i + 1))] in PolyRedRel P,
T
by A17, A21, FUNCT_1:70;
:: thesis: verum end; then reconsider q =
q as
RedSequence of
PolyRedRel P,
T by A5, A12, REWRITE1:def 2;
1
in dom q
by A5, A13, FINSEQ_1:3;
then A22:
q . 1
= f
by A7, FUNCT_1:70;
then
PolyRedRel P,
T reduces f,
h
by REWRITE1:def 3;
then A23:
PolyRedRel P,
T reduces m *' f,
m *' h
by A6, A12, A22;
h reduces_to g,
P,
T
by A14, Def13;
then consider r being
Polynomial of
n,
L such that A24:
(
r in P &
h reduces_to g,
r,
T )
by Def7;
h reduces_to g,
P,
T
by A24, Def7;
then
m *' h reduces_to m *' g,
P,
T
by Th46;
then
[(m *' h),(m *' g)] in PolyRedRel P,
T
by Def13;
then
PolyRedRel P,
T reduces m *' h,
m *' g
by REWRITE1:16;
hence
PolyRedRel P,
T reduces m *' f,
m *' g
by A23, REWRITE1:17;
:: thesis: verum end;
hence
S1[
k + 1]
;
:: thesis: verum
end; end; A25:
for
k being
Nat st 1
<= k holds
S1[
k]
from NAT_1:sch 8(A3, A4);
consider p being
RedSequence of
PolyRedRel P,
T such that A26:
(
p . 1
= f &
p . (len p) = g )
by A1, REWRITE1:def 3;
consider k being
Nat such that A27:
len p = k
;
k > 0
by A27;
then
1
<= k
by NAT_1:14;
hence
PolyRedRel P,
T reduces m *' f,
m *' g
by A1, A25, A26, A27;
:: thesis: verum end;