let n be Ordinal; 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; 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 ; 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; 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) ) )
;
suppose A1:
m1 = 0_ (
n,
L)
;
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
;
verum end; suppose A3:
m2 = 0_ (
n,
L)
;
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
;
verum end; suppose A5:
(
m1 <> 0_ (
n,
L) &
m2 <> 0_ (
n,
L) )
;
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;
verum end;