let n be Ordinal; :: thesis: for T being connected admissible TermOrder of n
for L being non trivial 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 st PolyRedRel P,T reduces f,g holds
PolyRedRel P,T reduces - f, - g
let T be connected admissible TermOrder of n; :: thesis: for L being non trivial 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 st PolyRedRel P,T reduces f,g holds
PolyRedRel P,T reduces - f, - g
let L be non trivial 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 st PolyRedRel P,T reduces f,g holds
PolyRedRel P,T reduces - f, - g
let P be Subset of (Polynom-Ring n,L); :: thesis: for f, g being Polynomial of n,L st PolyRedRel P,T reduces f,g holds
PolyRedRel P,T reduces - f, - g
let f, g be Polynomial of n,L; :: thesis: ( PolyRedRel P,T reduces f,g implies PolyRedRel P,T reduces - f, - g )
assume
PolyRedRel P,T reduces f,g
; :: thesis: PolyRedRel P,T reduces - f, - g
then consider R being RedSequence of PolyRedRel P,T such that
A1:
( R . 1 = f & R . (len R) = g )
by REWRITE1:def 3;
defpred S1[ Element of NAT ] means for q being Polynomial of n,L st q = R . $1 holds
PolyRedRel P,T reduces - f, - q;
A2:
S1[1]
by A1, REWRITE1:13;
A3:
now let k be
Element of
NAT ;
:: thesis: ( 1 <= k & k < len R & S1[k] implies S1[k + 1] )assume A4:
( 1
<= k &
k < len R )
;
:: thesis: ( S1[k] implies S1[k + 1] )assume A5:
S1[
k]
;
:: thesis: S1[k + 1]
1
< len R
by A4, XXREAL_0:2;
then reconsider p =
R . k as
Polynomial of
n,
L by A4, Lm4;
A6:
PolyRedRel P,
T reduces - f,
- p
by A5;
now let q be
Polynomial of
n,
L;
:: thesis: ( q = R . (k + 1) implies PolyRedRel P,T reduces - f, - q )assume A7:
q = R . (k + 1)
;
:: thesis: PolyRedRel P,T reduces - f, - qA8:
k in dom R
by A4, FINSEQ_3:27;
( 1
<= k + 1 &
k + 1
<= len R )
by A4, NAT_1:13;
then
k + 1
in dom R
by FINSEQ_3:27;
then
[(R . k),(R . (k + 1))] in PolyRedRel P,
T
by A8, REWRITE1:def 2;
then
p reduces_to q,
P,
T
by A7, POLYRED:def 13;
then consider l being
Polynomial of
n,
L such that A9:
(
l in P &
p reduces_to q,
l,
T )
by POLYRED:def 7;
- p reduces_to - q,
l,
T
by A9, Th45;
then
- p reduces_to - q,
P,
T
by A9, POLYRED:def 7;
then
[(- p),(- q)] in PolyRedRel P,
T
by POLYRED:def 13;
then
PolyRedRel P,
T reduces - p,
- q
by REWRITE1:16;
hence
PolyRedRel P,
T reduces - f,
- q
by A6, REWRITE1:17;
:: thesis: verum end; hence
S1[
k + 1]
;
:: thesis: verum end;
A10:
for i being Element of NAT st 1 <= i & i <= len R holds
S1[i]
from POLYNOM2:sch 4(A2, A3);
1 <= len R
by NAT_1:14;
hence
PolyRedRel P,T reduces - f, - g
by A1, A10; :: thesis: verum