let n be Ordinal; :: thesis: for T being connected TermOrder of n
for L being non trivial right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative doubleLoopStr
for P being Subset of (Polynom-Ring (n,L))
for f, g being Polynomial of n,L st PolyRedRel (P,T) reduces f,g holds
f - g in P -Ideal
let T be connected TermOrder of n; :: thesis: for L being non trivial right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative doubleLoopStr
for P being Subset of (Polynom-Ring (n,L))
for f, g being Polynomial of n,L st PolyRedRel (P,T) reduces f,g holds
f - g in P -Ideal
let L be non trivial right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative doubleLoopStr ; :: thesis: for P being Subset of (Polynom-Ring (n,L))
for f, g being Polynomial of n,L st PolyRedRel (P,T) reduces f,g holds
f - g in P -Ideal
let P be Subset of (Polynom-Ring (n,L)); :: thesis: for f, g being Polynomial of n,L st PolyRedRel (P,T) reduces f,g holds
f - g in P -Ideal
let f, g be Polynomial of n,L; :: thesis: ( PolyRedRel (P,T) reduces f,g implies f - g in P -Ideal )
reconsider f9 = f, g9 = g as Element of (Polynom-Ring (n,L)) by POLYNOM1:def 11;
reconsider f9 = f9, g9 = g9 as Element of (Polynom-Ring (n,L)) ;
set R = Polynom-Ring (n,L);
reconsider x = - g as Element of (Polynom-Ring (n,L)) by POLYNOM1:def 11;
reconsider x = x as Element of (Polynom-Ring (n,L)) ;
x + g9 = (- g) + g by POLYNOM1:def 11
.= 0_ (n,L) by Th3
.= 0. (Polynom-Ring (n,L)) by POLYNOM1:def 11 ;
then A1: - g9 = - g by RLVECT_1:6;
assume PolyRedRel (P,T) reduces f,g ; :: thesis: f - g in P -Ideal
then f,g are_convertible_wrt PolyRedRel (P,T) by REWRITE1:25;
then A2: f9,g9 are_congruent_mod P -Ideal by Th57;
f - g = f + (- g) by POLYNOM1:def 7
.= f9 + (- g9) by A1, POLYNOM1:def 11
.= f9 - g9 ;
hence f - g in P -Ideal by A2; :: thesis: verum