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 A1: ( p in P & p <> 0_ n,L & h <> 0_ n,L ) ; :: thesis: f,f + (h * p) are_convertible_wrt PolyRedRel P,T
set PR = Polynom-Ring n,L;
reconsider f' = f, h' = h, p' = p as Element of (Polynom-Ring n,L) ;
reconsider f' = f', p' = p', h' = h' as Polynomial of n,L by POLYNOM1:def 27;
reconsider h' = h', p' = p' as non-zero Polynomial of n,L by A1, POLYNOM7:def 2;
A2: PolyRedRel P,T reduces h' *' p', 0_ n,L by A1, Th45;

now

per cases ( f' = 0_ n,L or f' <> 0_ n,L ) ;

case f' = 0_ n,L ; :: thesis: f,f + (h * p) are_convertible_wrt PolyRedRel P,T

then PolyRedRel P,T reduces f' + (h' *' p'),f' by A2, Th2;
then A3: f',f' + (h' *' p') are_convertible_wrt PolyRedRel P,T by REWRITE1:26;
h' *' p' = h * p by POLYNOM1:def 27;
hence f,f + (h * p) are_convertible_wrt PolyRedRel P,T by A3, POLYNOM1:def 27; :: thesis: verum

end;

case f' <> 0_ n,L ; :: thesis: f,f + (h * p) are_convertible_wrt PolyRedRel P,T

then reconsider f' = f' as non-zero Polynomial of n,L by POLYNOM7:def 2;
(f' + (h' *' p')) - f' = (f' + (h' *' p')) + (- f') by POLYNOM1:def 23
.= (h' *' p') + (f' + (- f')) by POLYNOM1:80
.= (0_ n,L) + (h' *' p') by Th3
.= h' *' p' by Th2 ;
then A4: PolyRedRel P,T reduces (f' + (h' *' p')) - f', 0_ n,L by A1, Th45;

now

per cases ( f' + (h' *' p') <> 0_ n,L or f' + (h' *' p') = 0_ n,L ) ;

case f' + (h' *' p') <> 0_ n,L ; :: thesis: f,f + (h * p) are_convertible_wrt PolyRedRel P,T

then reconsider g' = f' + (h' *' p') as non-zero Polynomial of n,L by POLYNOM7:def 2;
h' *' p' = h * p by POLYNOM1:def 27;
then g' = f + (h * p) by POLYNOM1:def 27;
hence f,f + (h * p) are_convertible_wrt PolyRedRel P,T by A4, Th51, REWRITE1:32; :: thesis: verum

end;

case A5: f' + (h' *' p') = 0_ n,L ; :: thesis: f,f + (h * p) are_convertible_wrt PolyRedRel P,T

h' *' p' = h * p by POLYNOM1:def 27;
then A6: f + (h * p) = 0_ n,L by A5, POLYNOM1:def 27
.= 0. (Polynom-Ring n,L) by POLYNOM1:def 27 ;
then A7: f = - (h * p) by RLVECT_1:19
.= (- h) * p by VECTSP_1:41 ;

now

assume A8: - h' = 0_ n,L ; :: thesis: contradiction
A9: dom h' = Bags n by FUNCT_2:def 1
.= dom (0_ n,L) by FUNCT_2:def 1 ;

now

let u be set ; :: thesis: ( u in dom h' implies h' . u = (0_ n,L) . u )
assume u in dom h' ; :: thesis: h' . u = (0_ n,L) . u
then reconsider u' = u as bag of n by POLYNOM1:def 14;
- (h' . u') = (- h') . u' by POLYNOM1:def 22
.= 0. L by A8, POLYNOM1:81 ;
then h' . u' = - (0. L) by RLVECT_1:30
.= 0. L by RLVECT_1:25
.= (0_ n,L) . u' by POLYNOM1:81 ;
hence h' . u = (0_ n,L) . u ; :: thesis: verum

end;

hence contradiction by A1, A9, FUNCT_1:9; :: thesis: verum

end;

then reconsider mh' = - h' as non-zero Polynomial of n,L by POLYNOM7:def 2;
reconsider x = mh' as Element of (Polynom-Ring n,L) by POLYNOM1:def 27;
reconsider x = x as Element of (Polynom-Ring n,L) ;
h + x = mh' + h' by POLYNOM1:def 27
.= 0_ n,L by Th3
.= 0. (Polynom-Ring n,L) by POLYNOM1:def 27 ;
then A10: - h = mh' by RLVECT_1:19;
PolyRedRel P,T reduces mh' *' p', 0_ n,L by A1, Th45;
then A11: mh' *' p', 0_ n,L are_convertible_wrt PolyRedRel P,T by REWRITE1:26;
(- h) * p = mh' *' p' by A10, POLYNOM1:def 27;
hence f,f + (h * p) are_convertible_wrt PolyRedRel P,T by A6, A7, A11, 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