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 add-associative right_zeroed associative commutative doubleLoopStr
for p being Polynomial of n,L holds
( S-Poly (p,(0_ (n,L)),T) = 0_ (n,L) & S-Poly ((0_ (n,L)),p,T) = 0_ (n,L) )
let T be connected TermOrder of n; :: thesis: for L being non trivial right_complementable almost_left_invertible well-unital distributive add-associative right_zeroed associative commutative doubleLoopStr
for p being Polynomial of n,L holds
( S-Poly (p,(0_ (n,L)),T) = 0_ (n,L) & S-Poly ((0_ (n,L)),p,T) = 0_ (n,L) )
let L be non trivial right_complementable almost_left_invertible well-unital distributive add-associative right_zeroed associative commutative doubleLoopStr ; :: thesis: for p being Polynomial of n,L holds
( S-Poly (p,(0_ (n,L)),T) = 0_ (n,L) & S-Poly ((0_ (n,L)),p,T) = 0_ (n,L) )
let p be Polynomial of n,L; :: thesis: ( S-Poly (p,(0_ (n,L)),T) = 0_ (n,L) & S-Poly ((0_ (n,L)),p,T) = 0_ (n,L) )
set p2 = 0_ (n,L);
thus S-Poly (p,(0_ (n,L)),T) = ((HC ((0_ (n,L)),T)) * (((lcm ((HT (p,T)),(HT ((0_ (n,L)),T)))) / (HT (p,T))) *' p)) - ((Monom ((HC (p,T)),((lcm ((HT (p,T)),(HT ((0_ (n,L)),T)))) / (HT ((0_ (n,L)),T))))) *' (0_ (n,L))) by POLYRED:22
.= ((HC ((0_ (n,L)),T)) * (((lcm ((HT (p,T)),(HT ((0_ (n,L)),T)))) / (HT (p,T))) *' p)) - (0_ (n,L)) by POLYNOM1:28
.= ((0. L) * (((lcm ((HT (p,T)),(HT ((0_ (n,L)),T)))) / (HT (p,T))) *' p)) - (0_ (n,L)) by TERMORD:17
.= (((0. L) | (n,L)) *' (((lcm ((HT (p,T)),(HT ((0_ (n,L)),T)))) / (HT (p,T))) *' p)) - (0_ (n,L)) by POLYNOM7:27
.= ((0_ (n,L)) *' (((lcm ((HT (p,T)),(HT ((0_ (n,L)),T)))) / (HT (p,T))) *' p)) - (0_ (n,L)) by POLYNOM7:19
.= (0_ (n,L)) - (0_ (n,L)) by POLYRED:5
.= 0_ (n,L) by POLYRED:4 ; :: thesis: S-Poly ((0_ (n,L)),p,T) = 0_ (n,L)
thus S-Poly ((0_ (n,L)),p,T) = ((Monom ((HC (p,T)),((lcm ((HT ((0_ (n,L)),T)),(HT (p,T)))) / (HT ((0_ (n,L)),T))))) *' (0_ (n,L))) - ((HC ((0_ (n,L)),T)) * (((lcm ((HT ((0_ (n,L)),T)),(HT (p,T)))) / (HT (p,T))) *' p)) by POLYRED:22
.= (0_ (n,L)) - ((HC ((0_ (n,L)),T)) * (((lcm ((HT ((0_ (n,L)),T)),(HT (p,T)))) / (HT (p,T))) *' p)) by POLYNOM1:28
.= (0_ (n,L)) - ((0. L) * (((lcm ((HT ((0_ (n,L)),T)),(HT (p,T)))) / (HT (p,T))) *' p)) by TERMORD:17
.= (0_ (n,L)) - (((0. L) | (n,L)) *' (((lcm ((HT ((0_ (n,L)),T)),(HT (p,T)))) / (HT (p,T))) *' p)) by POLYNOM7:27
.= (0_ (n,L)) - ((0_ (n,L)) *' (((lcm ((HT ((0_ (n,L)),T)),(HT (p,T)))) / (HT (p,T))) *' p)) by POLYNOM7:19
.= (0_ (n,L)) - (0_ (n,L)) by POLYRED:5
.= 0_ (n,L) by POLYRED:4 ; :: thesis: verum