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 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; :: thesis: 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 ; :: 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 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 :: thesis: ( ( 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) ; :: 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 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 :: thesis: ( ( 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 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 1;
h9 *' p9 = h * p by POLYNOM1:def 11;
then g9 = f + (h * p) by POLYNOM1:def 11;
hence f,f + (h * p) are_convertible_wrt PolyRedRel (P,T) by A6, Th51, REWRITE1:31; :: thesis: verum
end;
case A7: f9 + (h9 *' p9) = 0_ (n,L) ; :: thesis: f,f + (h * p) are_convertible_wrt PolyRedRel (P,T)
now :: thesis: not - h9 = 0_ (n,L)
assume A8: - h9 = 0_ (n,L) ; :: thesis: contradiction
A9: now :: thesis: for u being object st u in dom h9 holds
h9 . u = (0_ (n,L)) . u
let u be object ; :: 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 ;
- (h9 . u9) = (- h9) . u9 by POLYNOM1:17
.= 0. L by A8, POLYNOM1:22 ;
then h9 . u9 = - (0. L) by RLVECT_1:17
.= 0. L by RLVECT_1:12
.= (0_ (n,L)) . u9 by POLYNOM1:22 ;
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:2; :: thesis: verum
end;
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; :: 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