let n be Nat; 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 non empty Subset of (Polynom-Ring (n,L))
for f, p, h being Element of (Polynom-Ring (n,L)) st p in P & p <> 0_ (n,L) & h <> 0_ (n,L) holds
f,f + (h * p) are_convertible_wrt PolyRedRel (P,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 P being non empty Subset of (Polynom-Ring (n,L))
for f, p, h being Element of (Polynom-Ring (n,L)) st p in P & p <> 0_ (n,L) & h <> 0_ (n,L) holds
f,f + (h * p) are_convertible_wrt PolyRedRel (P,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 P being non empty Subset of (Polynom-Ring (n,L))
for f, p, h being Element of (Polynom-Ring (n,L)) st p in P & p <> 0_ (n,L) & h <> 0_ (n,L) holds
f,f + (h * p) are_convertible_wrt PolyRedRel (P,T)
let P be non empty Subset of (Polynom-Ring (n,L)); for f, p, h being Element of (Polynom-Ring (n,L)) st p in P & p <> 0_ (n,L) & h <> 0_ (n,L) holds
f,f + (h * p) are_convertible_wrt PolyRedRel (P,T)
let f, p, h be Element of (Polynom-Ring (n,L)); ( p in P & p <> 0_ (n,L) & h <> 0_ (n,L) implies f,f + (h * p) are_convertible_wrt PolyRedRel (P,T) )
assume that
A1:
p in P
and
A2:
p <> 0_ (n,L)
and
A3:
h <> 0_ (n,L)
; f,f + (h * p) are_convertible_wrt PolyRedRel (P,T)
set PR = Polynom-Ring (n,L);
reconsider f9 = f, h9 = h, p9 = p as Element of (Polynom-Ring (n,L)) ;
reconsider f9 = f9, p9 = p9, h9 = h9 as Polynomial of n,L by POLYNOM1:def 11;
reconsider h9 = h9, p9 = p9 as non-zero Polynomial of n,L by A2, A3, POLYNOM7:def 1;
A4:
PolyRedRel (P,T) reduces h9 *' p9, 0_ (n,L)
by A1, Th45;
now ( ( f9 = 0_ (n,L) & f,f + (h * p) are_convertible_wrt PolyRedRel (P,T) ) or ( f9 <> 0_ (n,L) & f,f + (h * p) are_convertible_wrt PolyRedRel (P,T) ) )per cases
( f9 = 0_ (n,L) or f9 <> 0_ (n,L) )
;
case
f9 <> 0_ (
n,
L)
;
f,f + (h * p) are_convertible_wrt PolyRedRel (P,T)then reconsider f9 =
f9 as
non-zero Polynomial of
n,
L by POLYNOM7:def 1;
(f9 + (h9 *' p9)) - f9 =
(f9 + (h9 *' p9)) + (- f9)
by POLYNOM1:def 7
.=
(h9 *' p9) + (f9 + (- f9))
by POLYNOM1:21
.=
(0_ (n,L)) + (h9 *' p9)
by Th3
.=
h9 *' p9
by Th2
;
then A6:
PolyRedRel (
P,
T)
reduces (f9 + (h9 *' p9)) - f9,
0_ (
n,
L)
by A1, Th45;
now ( ( f9 + (h9 *' p9) <> 0_ (n,L) & f,f + (h * p) are_convertible_wrt PolyRedRel (P,T) ) or ( f9 + (h9 *' p9) = 0_ (n,L) & f,f + (h * p) are_convertible_wrt PolyRedRel (P,T) ) )per cases
( f9 + (h9 *' p9) <> 0_ (n,L) or f9 + (h9 *' p9) = 0_ (n,L) )
;
case A7:
f9 + (h9 *' p9) = 0_ (
n,
L)
;
f,f + (h * p) are_convertible_wrt PolyRedRel (P,T)then reconsider mh9 =
- h9 as
non-zero Polynomial of
n,
L by POLYNOM7:def 1;
reconsider x =
mh9 as
Element of
(Polynom-Ring (n,L)) by POLYNOM1:def 11;
reconsider x =
x as
Element of
(Polynom-Ring (n,L)) ;
h + x =
mh9 + h9
by POLYNOM1:def 11
.=
0_ (
n,
L)
by Th3
.=
0. (Polynom-Ring (n,L))
by POLYNOM1:def 11
;
then
- h = mh9
by RLVECT_1:6;
then A10:
(- h) * p = mh9 *' p9
by POLYNOM1:def 11;
PolyRedRel (
P,
T)
reduces mh9 *' p9,
0_ (
n,
L)
by A1, Th45;
then A11:
mh9 *' p9,
0_ (
n,
L)
are_convertible_wrt PolyRedRel (
P,
T)
by REWRITE1:25;
h9 *' p9 = h * p
by POLYNOM1:def 11;
then A12:
f + (h * p) =
0_ (
n,
L)
by A7, POLYNOM1:def 11
.=
0. (Polynom-Ring (n,L))
by POLYNOM1:def 11
;
then f =
- (h * p)
by RLVECT_1:6
.=
(- h) * p
by VECTSP_1:9
;
hence
f,
f + (h * p) are_convertible_wrt PolyRedRel (
P,
T)
by A12, A11, A10, POLYNOM1:def 11;
verum end; end; end; hence
f,
f + (h * p) are_convertible_wrt PolyRedRel (
P,
T)
;
verum end; end; end;
hence
f,f + (h * p) are_convertible_wrt PolyRedRel (P,T)
; verum