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 m1, m2 being Monomial of n,L holds S-Poly (m1,m2,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 m1, m2 being Monomial of n,L holds S-Poly (m1,m2,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 m1, m2 being Monomial of n,L holds S-Poly (m1,m2,T) = 0_ (n,L)

let m1, m2 be Monomial of n,L; :: thesis: S-Poly (m1,m2,T) = 0_ (n,L)

for L being non trivial right_complementable almost_left_invertible well-unital distributive add-associative right_zeroed associative commutative doubleLoopStr

for m1, m2 being Monomial of n,L holds S-Poly (m1,m2,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 m1, m2 being Monomial of n,L holds S-Poly (m1,m2,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 m1, m2 being Monomial of n,L holds S-Poly (m1,m2,T) = 0_ (n,L)

let m1, m2 be Monomial of n,L; :: thesis: S-Poly (m1,m2,T) = 0_ (n,L)

per cases
( m1 = 0_ (n,L) or m2 = 0_ (n,L) or ( m1 <> 0_ (n,L) & m2 <> 0_ (n,L) ) )
;

end;

suppose A1:
m1 = 0_ (n,L)
; :: thesis: S-Poly (m1,m2,T) = 0_ (n,L)

A2: HC ((Monom ((HC ((0_ (n,L)),T)),((lcm ((HT (m1,T)),(HT (m2,T)))) / (HT (m2,T))))),T) =
coefficient (Monom ((HC ((0_ (n,L)),T)),((lcm ((HT (m1,T)),(HT (m2,T)))) / (HT (m2,T)))))
by TERMORD:23

.= HC ((0_ (n,L)),T) by POLYNOM7:9

.= 0. L by TERMORD:17 ;

thus S-Poly (m1,m2,T) = ((Monom ((HC (m2,T)),((lcm ((HT (m1,T)),(HT (m2,T)))) / (HT (m1,T))))) *' (0_ (n,L))) - ((HC ((0_ (n,L)),T)) * (((lcm ((HT (m1,T)),(HT (m2,T)))) / (HT (m2,T))) *' m2)) by A1, POLYRED:22

.= (0_ (n,L)) - ((HC ((0_ (n,L)),T)) * (((lcm ((HT (m1,T)),(HT (m2,T)))) / (HT (m2,T))) *' m2)) by POLYNOM1:28

.= (0_ (n,L)) - ((Monom ((HC ((0_ (n,L)),T)),((lcm ((HT (m1,T)),(HT (m2,T)))) / (HT (m2,T))))) *' m2) by POLYRED:22

.= (0_ (n,L)) - ((0_ (n,L)) *' m2) by A2, TERMORD:17

.= (0_ (n,L)) - (0_ (n,L)) by POLYRED:5

.= 0_ (n,L) by POLYNOM1:24 ; :: thesis: verum

end;.= HC ((0_ (n,L)),T) by POLYNOM7:9

.= 0. L by TERMORD:17 ;

thus S-Poly (m1,m2,T) = ((Monom ((HC (m2,T)),((lcm ((HT (m1,T)),(HT (m2,T)))) / (HT (m1,T))))) *' (0_ (n,L))) - ((HC ((0_ (n,L)),T)) * (((lcm ((HT (m1,T)),(HT (m2,T)))) / (HT (m2,T))) *' m2)) by A1, POLYRED:22

.= (0_ (n,L)) - ((HC ((0_ (n,L)),T)) * (((lcm ((HT (m1,T)),(HT (m2,T)))) / (HT (m2,T))) *' m2)) by POLYNOM1:28

.= (0_ (n,L)) - ((Monom ((HC ((0_ (n,L)),T)),((lcm ((HT (m1,T)),(HT (m2,T)))) / (HT (m2,T))))) *' m2) by POLYRED:22

.= (0_ (n,L)) - ((0_ (n,L)) *' m2) by A2, TERMORD:17

.= (0_ (n,L)) - (0_ (n,L)) by POLYRED:5

.= 0_ (n,L) by POLYNOM1:24 ; :: thesis: verum

suppose A3:
m2 = 0_ (n,L)
; :: thesis: S-Poly (m1,m2,T) = 0_ (n,L)

A4: HC ((Monom ((HC ((0_ (n,L)),T)),((lcm ((HT (m1,T)),(HT (m2,T)))) / (HT (m1,T))))),T) =
coefficient (Monom ((HC ((0_ (n,L)),T)),((lcm ((HT (m1,T)),(HT (m2,T)))) / (HT (m1,T)))))
by TERMORD:23

.= HC ((0_ (n,L)),T) by POLYNOM7:9

.= 0. L by TERMORD:17 ;

thus S-Poly (m1,m2,T) = ((HC ((0_ (n,L)),T)) * (((lcm ((HT (m1,T)),(HT (m2,T)))) / (HT (m1,T))) *' m1)) - ((Monom ((HC (m1,T)),((lcm ((HT (m1,T)),(HT (m2,T)))) / (HT (m2,T))))) *' (0_ (n,L))) by A3, POLYRED:22

.= ((HC ((0_ (n,L)),T)) * (((lcm ((HT (m1,T)),(HT (m2,T)))) / (HT (m1,T))) *' m1)) - (0_ (n,L)) by POLYNOM1:28

.= ((Monom ((HC ((0_ (n,L)),T)),((lcm ((HT (m1,T)),(HT (m2,T)))) / (HT (m1,T))))) *' m1) - (0_ (n,L)) by POLYRED:22

.= ((0_ (n,L)) *' m1) - (0_ (n,L)) by A4, TERMORD:17

.= (0_ (n,L)) - (0_ (n,L)) by POLYRED:5

.= 0_ (n,L) by POLYNOM1:24 ; :: thesis: verum

end;.= HC ((0_ (n,L)),T) by POLYNOM7:9

.= 0. L by TERMORD:17 ;

thus S-Poly (m1,m2,T) = ((HC ((0_ (n,L)),T)) * (((lcm ((HT (m1,T)),(HT (m2,T)))) / (HT (m1,T))) *' m1)) - ((Monom ((HC (m1,T)),((lcm ((HT (m1,T)),(HT (m2,T)))) / (HT (m2,T))))) *' (0_ (n,L))) by A3, POLYRED:22

.= ((HC ((0_ (n,L)),T)) * (((lcm ((HT (m1,T)),(HT (m2,T)))) / (HT (m1,T))) *' m1)) - (0_ (n,L)) by POLYNOM1:28

.= ((Monom ((HC ((0_ (n,L)),T)),((lcm ((HT (m1,T)),(HT (m2,T)))) / (HT (m1,T))))) *' m1) - (0_ (n,L)) by POLYRED:22

.= ((0_ (n,L)) *' m1) - (0_ (n,L)) by A4, TERMORD:17

.= (0_ (n,L)) - (0_ (n,L)) by POLYRED:5

.= 0_ (n,L) by POLYNOM1:24 ; :: thesis: verum

suppose A5:
( m1 <> 0_ (n,L) & m2 <> 0_ (n,L) )
; :: thesis: S-Poly (m1,m2,T) = 0_ (n,L)

then
HC (m2,T) <> 0. L
by TERMORD:17;

then A6: not HC (m2,T) is zero ;

HC (m1,T) <> 0. L by A5, TERMORD:17;

then A7: not HC (m1,T) is zero ;

A8: HT (m2,T) divides lcm ((HT (m1,T)),(HT (m2,T))) by Th3;

A9: m2 = Monom ((coefficient m2),(term m2)) by POLYNOM7:11

.= Monom ((HC (m2,T)),(term m2)) by TERMORD:23

.= Monom ((HC (m2,T)),(HT (m2,T))) by TERMORD:23 ;

A10: HT (m1,T) divides lcm ((HT (m1,T)),(HT (m2,T))) by Th3;

A11: m1 = Monom ((coefficient m1),(term m1)) by POLYNOM7:11

.= Monom ((HC (m1,T)),(term m1)) by TERMORD:23

.= Monom ((HC (m1,T)),(HT (m1,T))) by TERMORD:23 ;

A12: (HC (m1,T)) * (((lcm ((HT (m1,T)),(HT (m2,T)))) / (HT (m2,T))) *' m2) = (Monom ((HC (m1,T)),((lcm ((HT (m1,T)),(HT (m2,T)))) / (HT (m2,T))))) *' m2 by POLYRED:22

.= Monom (((HC (m2,T)) * (HC (m1,T))),(((lcm ((HT (m1,T)),(HT (m2,T)))) / (HT (m2,T))) + (HT (m2,T)))) by A7, A6, A9, TERMORD:3

.= Monom (((HC (m2,T)) * (HC (m1,T))),(lcm ((HT (m1,T)),(HT (m2,T))))) by A8, Def1 ;

(HC (m2,T)) * (((lcm ((HT (m1,T)),(HT (m2,T)))) / (HT (m1,T))) *' m1) = (Monom ((HC (m2,T)),((lcm ((HT (m1,T)),(HT (m2,T)))) / (HT (m1,T))))) *' m1 by POLYRED:22

.= Monom (((HC (m2,T)) * (HC (m1,T))),(((lcm ((HT (m1,T)),(HT (m2,T)))) / (HT (m1,T))) + (HT (m1,T)))) by A7, A6, A11, TERMORD:3

.= Monom (((HC (m2,T)) * (HC (m1,T))),(lcm ((HT (m1,T)),(HT (m2,T))))) by A10, Def1 ;

hence S-Poly (m1,m2,T) = 0_ (n,L) by A12, POLYNOM1:24; :: thesis: verum

end;then A6: not HC (m2,T) is zero ;

HC (m1,T) <> 0. L by A5, TERMORD:17;

then A7: not HC (m1,T) is zero ;

A8: HT (m2,T) divides lcm ((HT (m1,T)),(HT (m2,T))) by Th3;

A9: m2 = Monom ((coefficient m2),(term m2)) by POLYNOM7:11

.= Monom ((HC (m2,T)),(term m2)) by TERMORD:23

.= Monom ((HC (m2,T)),(HT (m2,T))) by TERMORD:23 ;

A10: HT (m1,T) divides lcm ((HT (m1,T)),(HT (m2,T))) by Th3;

A11: m1 = Monom ((coefficient m1),(term m1)) by POLYNOM7:11

.= Monom ((HC (m1,T)),(term m1)) by TERMORD:23

.= Monom ((HC (m1,T)),(HT (m1,T))) by TERMORD:23 ;

A12: (HC (m1,T)) * (((lcm ((HT (m1,T)),(HT (m2,T)))) / (HT (m2,T))) *' m2) = (Monom ((HC (m1,T)),((lcm ((HT (m1,T)),(HT (m2,T)))) / (HT (m2,T))))) *' m2 by POLYRED:22

.= Monom (((HC (m2,T)) * (HC (m1,T))),(((lcm ((HT (m1,T)),(HT (m2,T)))) / (HT (m2,T))) + (HT (m2,T)))) by A7, A6, A9, TERMORD:3

.= Monom (((HC (m2,T)) * (HC (m1,T))),(lcm ((HT (m1,T)),(HT (m2,T))))) by A8, Def1 ;

(HC (m2,T)) * (((lcm ((HT (m1,T)),(HT (m2,T)))) / (HT (m1,T))) *' m1) = (Monom ((HC (m2,T)),((lcm ((HT (m1,T)),(HT (m2,T)))) / (HT (m1,T))))) *' m1 by POLYRED:22

.= Monom (((HC (m2,T)) * (HC (m1,T))),(((lcm ((HT (m1,T)),(HT (m2,T)))) / (HT (m1,T))) + (HT (m1,T)))) by A7, A6, A11, TERMORD:3

.= Monom (((HC (m2,T)) * (HC (m1,T))),(lcm ((HT (m1,T)),(HT (m2,T))))) by A10, Def1 ;

hence S-Poly (m1,m2,T) = 0_ (n,L) by A12, POLYNOM1:24; :: thesis: verum