let n be Ordinal; :: thesis: for T being connected TermOrder of n
for L being non trivial right_complementable almost_left_invertible associative commutative well-unital distributive Abelian add-associative right_zeroed 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 associative commutative well-unital distributive Abelian add-associative right_zeroed 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 associative commutative well-unital distributive Abelian add-associative right_zeroed 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 27;
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 27;
reconsider x = x as Element of (Polynom-Ring n,L) ;
x + g9 = (- g) + g by POLYNOM1:def 27
.= 0_ n,L by Th3
.= 0. (Polynom-Ring n,L) by POLYNOM1:def 27 ;
then A1: - g9 = - g by RLVECT_1:19;
assume PolyRedRel P,T reduces f,g ; :: thesis: f - g in P -Ideal
then f,g are_convertible_wrt PolyRedRel P,T by REWRITE1:26;
then A2: f9,g9 are_congruent_mod P -Ideal by Th57;
f - g = f + (- g) by POLYNOM1:def 23
.= f9 + (- g9) by A1, POLYNOM1:def 27
.= f9 - g9 by RLVECT_1:def 12 ;
hence f - g in P -Ideal by A2, Def14; :: thesis: verum