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 add-associative right_zeroed 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 associative commutative well-unital distributive add-associative right_zeroed 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 associative commutative well-unital distributive add-associative right_zeroed 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 ) )
;
suppose A1:
m1 = 0_ n,
L
;
:: thesis: S-Poly m1,m2,T = 0_ n,LA2:
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:87
.=
(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:83
;
:: thesis: verum end; suppose A3:
m2 = 0_ n,
L
;
:: thesis: S-Poly m1,m2,T = 0_ n,LA4:
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:87
.=
((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:83
;
:: thesis: verum end; suppose
(
m1 <> 0_ n,
L &
m2 <> 0_ n,
L )
;
:: thesis: S-Poly m1,m2,T = 0_ n,Lthen
(
HC m1,
T <> 0. L &
HC m2,
T <> 0. L )
by TERMORD:17;
then A5:
( not
HC m1,
T is
zero & not
HC m2,
T is
zero )
by STRUCT_0:def 15;
A6:
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
;
A7:
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
;
A8:
HT m1,
T divides lcm (HT m1,T),
(HT m2,T)
by Th7;
A9:
(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 A5, A6, TERMORD:3
.=
Monom ((HC m2,T) * (HC m1,T)),
(lcm (HT m1,T),(HT m2,T))
by A8, Def1
;
A10:
HT m2,
T divides lcm (HT m1,T),
(HT m2,T)
by Th7;
(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 A5, A7, 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 A9, POLYNOM1:83;
:: thesis: verum end;