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
for f, p, h being Element of 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
for f, p, h being Element of 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
for f, p, h being Element of 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 ; :: thesis: for f, p, h being Element of 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 ; :: 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 f' = f, h' = h, p' = p as Element of ;
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 A2, A3, POLYNOM7:def 2;
A4: 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 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 A6: 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 A6, Th51, REWRITE1:32; :: thesis: verum
end;
case A7: f' + (h' *' p') = 0_ n,L ; :: thesis: f,f + (h * p) are_convertible_wrt PolyRedRel P,T
now
assume A8: - h' = 0_ n,L ; :: thesis: contradiction
A9: 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 PRE_POLY:def 12;
- (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;
dom h' = 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 mh' = - h' as non-zero Polynomial of n,L by POLYNOM7:def 2;
reconsider x = mh' as Element of by POLYNOM1:def 27;
reconsider x = x as Element of ;
h + x = mh' + h' by POLYNOM1:def 27
.= 0_ n,L by Th3
.= 0. (Polynom-Ring n,L) by POLYNOM1:def 27 ;
then - h = mh' by RLVECT_1:19;
then A10: (- h) * p = mh' *' p' by POLYNOM1:def 27;
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' = 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