let n be Nat; :: 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 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; :: 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 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 associative commutative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; :: thesis: 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); :: thesis: 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); :: thesis: ( 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 ; :: thesis: 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 27;
reconsider h9 = h9, p9 = p9 as non-zero Polynomial of n,L by A2, A3, POLYNOM7:def 2;
A4: PolyRedRel P,T reduces h9 *' p9, 0_ n,L by A1, Th45;
now
per cases ( f9 = 0_ n,L or f9 <> 0_ n,L ) ;
case f9 <> 0_ n,L ; :: thesis: f,f + (h * p) are_convertible_wrt PolyRedRel P,T
then reconsider f9 = f9 as non-zero Polynomial of n,L by POLYNOM7:def 2;
(f9 + (h9 *' p9)) - f9 = (f9 + (h9 *' p9)) + (- f9) by POLYNOM1:def 23
.= (h9 *' p9) + (f9 + (- f9)) by POLYNOM1:80
.= (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
per cases ( f9 + (h9 *' p9) <> 0_ n,L or f9 + (h9 *' p9) = 0_ n,L ) ;
case f9 + (h9 *' p9) <> 0_ n,L ; :: thesis: f,f + (h * p) are_convertible_wrt PolyRedRel P,T
then reconsider g9 = f9 + (h9 *' p9) as non-zero Polynomial of n,L by POLYNOM7:def 2;
h9 *' p9 = h * p by POLYNOM1:def 27;
then g9 = f + (h * p) by POLYNOM1:def 27;
hence f,f + (h * p) are_convertible_wrt PolyRedRel P,T by A6, Th51, REWRITE1:32; :: thesis: verum
end;
case A7: f9 + (h9 *' p9) = 0_ n,L ; :: thesis: f,f + (h * p) are_convertible_wrt PolyRedRel P,T
now
assume A8: - h9 = 0_ n,L ; :: thesis: contradiction
A9: now
let u be set ; :: thesis: ( u in dom h9 implies h9 . u = (0_ n,L) . u )
assume u in dom h9 ; :: thesis: h9 . u = (0_ n,L) . u
then reconsider u9 = u as bag of n by PRE_POLY:def 12;
- (h9 . u9) = (- h9) . u9 by POLYNOM1:def 22
.= 0. L by A8, POLYNOM1:81 ;
then h9 . u9 = - (0. L) by RLVECT_1:30
.= 0. L by RLVECT_1:25
.= (0_ n,L) . u9 by POLYNOM1:81 ;
hence h9 . u = (0_ n,L) . u ; :: thesis: verum
end;
dom h9 = Bags n by FUNCT_2:def 1
.= dom (0_ n,L) by FUNCT_2:def 1 ;
hence contradiction by A3, A9, FUNCT_1:9; :: thesis: verum
end;
then reconsider mh9 = - h9 as non-zero Polynomial of n,L by POLYNOM7:def 2;
reconsider x = mh9 as Element of (Polynom-Ring n,L) by POLYNOM1:def 27;
reconsider x = x as Element of (Polynom-Ring n,L) ;
h + x = mh9 + h9 by POLYNOM1:def 27
.= 0_ n,L by Th3
.= 0. (Polynom-Ring n,L) by POLYNOM1:def 27 ;
then - h = mh9 by RLVECT_1:19;
then A10: (- h) * p = mh9 *' p9 by POLYNOM1:def 27;
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:26;
h9 *' p9 = h * p by POLYNOM1:def 27;
then A12: f + (h * p) = 0_ n,L by A7, POLYNOM1:def 27
.= 0. (Polynom-Ring n,L) by POLYNOM1:def 27 ;
then f = - (h * p) by RLVECT_1:19
.= (- h) * p by VECTSP_1:41 ;
hence f,f + (h * p) are_convertible_wrt PolyRedRel P,T by A12, A11, A10, POLYNOM1:def 27; :: thesis: verum
end;
end;
end;
hence f,f + (h * p) are_convertible_wrt PolyRedRel P,T ; :: thesis: verum
end;
end;
end;
hence f,f + (h * p) are_convertible_wrt PolyRedRel P,T ; :: thesis: verum