let n be Element of NAT ; :: thesis: for T being connected admissible TermOrder of n
for L being non empty non degenerated right_complementable almost_left_invertible associative commutative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for G being Subset of (Polynom-Ring n,L) st not 0_ n,L in G & ( for g1, g2 being Polynomial of n,L st g1 in G & g2 in G holds
PolyRedRel G,T reduces S-Poly g1,g2,T, 0_ n,L ) holds
G is_Groebner_basis_wrt T
let T be connected admissible TermOrder of n; :: thesis: for L being non empty non degenerated right_complementable almost_left_invertible associative commutative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for G being Subset of (Polynom-Ring n,L) st not 0_ n,L in G & ( for g1, g2 being Polynomial of n,L st g1 in G & g2 in G holds
PolyRedRel G,T reduces S-Poly g1,g2,T, 0_ n,L ) holds
G is_Groebner_basis_wrt T
let L be non empty non degenerated right_complementable almost_left_invertible associative commutative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; :: thesis: for G being Subset of (Polynom-Ring n,L) st not 0_ n,L in G & ( for g1, g2 being Polynomial of n,L st g1 in G & g2 in G holds
PolyRedRel G,T reduces S-Poly g1,g2,T, 0_ n,L ) holds
G is_Groebner_basis_wrt T
let G be Subset of (Polynom-Ring n,L); :: thesis: ( not 0_ n,L in G & ( for g1, g2 being Polynomial of n,L st g1 in G & g2 in G holds
PolyRedRel G,T reduces S-Poly g1,g2,T, 0_ n,L ) implies G is_Groebner_basis_wrt T )
assume A1:
not 0_ n,L in G
; :: thesis: ( ex g1, g2 being Polynomial of n,L st
( g1 in G & g2 in G & not PolyRedRel G,T reduces S-Poly g1,g2,T, 0_ n,L ) or G is_Groebner_basis_wrt T )
assume A2:
for g1, g2 being Polynomial of n,L st g1 in G & g2 in G holds
PolyRedRel G,T reduces S-Poly g1,g2,T, 0_ n,L
; :: thesis: G is_Groebner_basis_wrt T
now let g1,
g2 be
Polynomial of
n,
L;
:: thesis: ( g1 <> g2 & g1 in G & g2 in G implies for m1, m2 being Monomial of n,L st HM (m1 *' g1),T = HM (m2 *' g2),T holds
PolyRedRel G,T reduces (m1 *' g1) - (m2 *' g2), 0_ n,L )assume A3:
(
g1 <> g2 &
g1 in G &
g2 in G )
;
:: thesis: for m1, m2 being Monomial of n,L st HM (m1 *' g1),T = HM (m2 *' g2),T holds
PolyRedRel G,T reduces (m1 *' g1) - (m2 *' g2), 0_ n,Lthus
for
m1,
m2 being
Monomial of
n,
L st
HM (m1 *' g1),
T = HM (m2 *' g2),
T holds
PolyRedRel G,
T reduces (m1 *' g1) - (m2 *' g2),
0_ n,
L
:: thesis: verumproof
let m1,
m2 be
Monomial of
n,
L;
:: thesis: ( HM (m1 *' g1),T = HM (m2 *' g2),T implies PolyRedRel G,T reduces (m1 *' g1) - (m2 *' g2), 0_ n,L )
assume A4:
HM (m1 *' g1),
T = HM (m2 *' g2),
T
;
:: thesis: PolyRedRel G,T reduces (m1 *' g1) - (m2 *' g2), 0_ n,L
set t1 =
HT g1,
T;
set t2 =
HT g2,
T;
set a1 =
HC g1,
T;
set a2 =
HC g2,
T;
set b1 =
coefficient m1;
set b2 =
coefficient m2;
set u1 =
term m1;
set u2 =
term m2;
A5:
(
HC g1,
T <> 0. L &
HC g2,
T <> 0. L )
by A1, A3, TERMORD:17;
then reconsider a1 =
HC g1,
T,
a2 =
HC g2,
T as non
zero Element of
L by STRUCT_0:def 15;
reconsider g1 =
g1,
g2 =
g2 as
non-zero Polynomial of
n,
L by A1, A3, POLYNOM7:def 2;
A6:
HC (m1 *' g1),
T =
coefficient (HM (m1 *' g1),T)
by TERMORD:22
.=
HC (m2 *' g2),
T
by A4, TERMORD:22
;
now per cases
( coefficient m1 = 0. L or coefficient m2 = 0. L or ( coefficient m1 <> 0. L & coefficient m2 <> 0. L ) )
;
case A7:
(
coefficient m1 = 0. L or
coefficient m2 = 0. L )
;
:: thesis: PolyRedRel G,T reduces (m1 *' g1) - (m2 *' g2), 0_ n,Lnow per cases
( coefficient m1 = 0. L or coefficient m2 = 0. L )
by A7;
case
coefficient m1 = 0. L
;
:: thesis: PolyRedRel G,T reduces (m1 *' g1) - (m2 *' g2), 0_ n,Lthen
HC m1,
T = 0. L
by TERMORD:23;
then
m1 = 0_ n,
L
by TERMORD:17;
then A8:
m1 *' g1 = 0_ n,
L
by POLYRED:5;
then
HC (m2 *' g2),
T = 0. L
by A6, TERMORD:17;
then
m2 *' g2 = 0_ n,
L
by TERMORD:17;
then
(m1 *' g1) - (m2 *' g2) = 0_ n,
L
by A8, POLYRED:4;
hence
PolyRedRel G,
T reduces (m1 *' g1) - (m2 *' g2),
0_ n,
L
by REWRITE1:13;
:: thesis: verum end; case
coefficient m2 = 0. L
;
:: thesis: PolyRedRel G,T reduces (m1 *' g1) - (m2 *' g2), 0_ n,Lthen
HC m2,
T = 0. L
by TERMORD:23;
then
m2 = 0_ n,
L
by TERMORD:17;
then A9:
m2 *' g2 = 0_ n,
L
by POLYRED:5;
then
HC (m1 *' g1),
T = 0. L
by A6, TERMORD:17;
then
m1 *' g1 = 0_ n,
L
by TERMORD:17;
then
(m1 *' g1) - (m2 *' g2) = 0_ n,
L
by A9, POLYRED:4;
hence
PolyRedRel G,
T reduces (m1 *' g1) - (m2 *' g2),
0_ n,
L
by REWRITE1:13;
:: thesis: verum end; hence
PolyRedRel G,
T reduces (m1 *' g1) - (m2 *' g2),
0_ n,
L
;
:: thesis: verum case A10:
(
coefficient m1 <> 0. L &
coefficient m2 <> 0. L )
;
:: thesis: PolyRedRel G,T reduces (m1 *' g1) - (m2 *' g2), 0_ n,Lthen reconsider b1 =
coefficient m1,
b2 =
coefficient m2 as non
zero Element of
L by STRUCT_0:def 15;
(
HC m1,
T <> 0. L &
HC m2,
T <> 0. L )
by A10, TERMORD:23;
then
(
m1 <> 0_ n,
L &
m2 <> 0_ n,
L )
by TERMORD:17;
then reconsider m1 =
m1,
m2 =
m2 as
non-zero Monomial of
n,
L by POLYNOM7:def 2;
A11:
Monom (b1 * a1),
((term m1) + (HT g1,T)) =
(Monom b1,(term m1)) *' (Monom a1,(HT g1,T))
by TERMORD:3
.=
m1 *' (Monom a1,(HT g1,T))
by POLYNOM7:11
.=
(HM m1,T) *' (Monom a1,(HT g1,T))
by TERMORD:23
.=
(HM m1,T) *' (HM g1,T)
by TERMORD:def 8
.=
HM (m2 *' g2),
T
by A4, TERMORD:33
.=
(HM m2,T) *' (HM g2,T)
by TERMORD:33
.=
(HM m2,T) *' (Monom a2,(HT g2,T))
by TERMORD:def 8
.=
m2 *' (Monom a2,(HT g2,T))
by TERMORD:23
.=
(Monom b2,(term m2)) *' (Monom a2,(HT g2,T))
by POLYNOM7:11
.=
Monom (b2 * a2),
((term m2) + (HT g2,T))
by TERMORD:3
;
(
b1 * a1 <> 0. L &
b2 * a2 <> 0. L )
by A5, A10, VECTSP_2:def 5;
then A12:
( not
b1 * a1 is
zero & not
b2 * a2 is
zero )
by STRUCT_0:def 15;
then A13:
(term m1) + (HT g1,T) =
term (Monom (b2 * a2),((term m2) + (HT g2,T)))
by A11, POLYNOM7:10
.=
(term m2) + (HT g2,T)
by A12, POLYNOM7:10
;
HT g1,
T divides lcm (HT g1,T),
(HT g2,T)
by Th7;
then consider s1 being
bag of
such that A14:
(HT g1,T) + s1 = lcm (HT g1,T),
(HT g2,T)
by TERMORD:1;
HT g2,
T divides lcm (HT g1,T),
(HT g2,T)
by Th7;
then consider s2 being
bag of
such that A15:
(HT g2,T) + s2 = lcm (HT g1,T),
(HT g2,T)
by TERMORD:1;
(
HT g1,
T divides (term m1) + (HT g1,T) &
HT g2,
T divides (term m1) + (HT g1,T) )
by A13, TERMORD:1;
then
lcm (HT g1,T),
(HT g2,T) divides (term m1) + (HT g1,T)
by Th8;
then consider v being
bag of
such that A16:
(term m1) + (HT g1,T) = (lcm (HT g1,T),(HT g2,T)) + v
by TERMORD:1;
(term m1) + (HT g1,T) = (v + s1) + (HT g1,T)
by A14, A16, POLYNOM1:39;
then A17:
term m1 =
((v + s1) + (HT g1,T)) -' (HT g1,T)
by POLYNOM1:52
.=
v + s1
by POLYNOM1:52
;
(term m2) + (HT g2,T) = (v + s2) + (HT g2,T)
by A13, A15, A16, POLYNOM1:39;
then A18:
term m2 =
((v + s2) + (HT g2,T)) -' (HT g2,T)
by POLYNOM1:52
.=
v + s2
by POLYNOM1:52
;
b1 * a1 =
coefficient (Monom (b2 * a2),((term m2) + (HT g2,T)))
by A11, POLYNOM7:9
.=
b2 * a2
by POLYNOM7:9
;
then (b1 * a1) / a2 =
(b2 * a2) * (a2 " )
by VECTSP_1:def 23
.=
b2 * (a2 * (a2 " ))
by GROUP_1:def 4
.=
b2 * (1. L)
by A5, VECTSP_1:def 22
;
then A19:
b2 / a1 =
((b1 * a1) / a2) / a1
by VECTSP_1:def 13
.=
((b1 * a1) * (a2 " )) / a1
by VECTSP_1:def 23
.=
((b1 * a1) * (a2 " )) * (a1 " )
by VECTSP_1:def 23
.=
((b1 * (a2 " )) * a1) * (a1 " )
by GROUP_1:def 4
.=
(b1 * (a2 " )) * (a1 * (a1 " ))
by GROUP_1:def 4
.=
(b1 * (a2 " )) * (1. L)
by A5, VECTSP_1:def 22
.=
b1 * (a2 " )
by VECTSP_1:def 13
.=
b1 / a2
by VECTSP_1:def 23
;
HT g1,
T divides lcm (HT g1,T),
(HT g2,T)
by Th7;
then A20:
s1 = (lcm (HT g1,T),(HT g2,T)) / (HT g1,T)
by A14, Def1;
HT g2,
T divides lcm (HT g1,T),
(HT g2,T)
by Th7;
then A21:
s2 = (lcm (HT g1,T),(HT g2,T)) / (HT g2,T)
by A15, Def1;
A22:
(b1 / a2) * a2 =
(b1 * (a2 " )) * a2
by VECTSP_1:def 23
.=
b1 * ((a2 " ) * a2)
by GROUP_1:def 4
.=
b1 * (1. L)
by A5, VECTSP_1:def 22
;
A23:
(b2 / a1) * a1 =
(b2 * (a1 " )) * a1
by VECTSP_1:def 23
.=
b2 * ((a1 " ) * a1)
by GROUP_1:def 4
.=
b2 * (1. L)
by A5, VECTSP_1:def 22
.=
b2
by VECTSP_1:def 13
;
(m1 *' g1) - (m2 *' g2) =
((Monom b1,(term m1)) *' g1) - (m2 *' g2)
by POLYNOM7:11
.=
((Monom b1,(term m1)) *' g1) - ((Monom b2,(term m2)) *' g2)
by POLYNOM7:11
.=
(b1 * ((v + s1) *' g1)) - ((Monom b2,(v + s2)) *' g2)
by A17, A18, POLYRED:22
.=
(b1 * (v *' (s1 *' g1))) - ((Monom b2,(v + s2)) *' g2)
by POLYRED:18
.=
(b1 * (v *' (s1 *' g1))) - (b2 * ((v + s2) *' g2))
by POLYRED:22
.=
(b1 * (v *' (s1 *' g1))) - (b2 * (v *' (s2 *' g2)))
by POLYRED:18
.=
(b1 * (v *' (s1 *' g1))) + (- (b2 * (v *' (s2 *' g2))))
by POLYNOM1:def 23
.=
(b1 * (v *' (s1 *' g1))) + (b2 * (- (v *' (s2 *' g2))))
by POLYRED:9
.=
(((b1 / a2) * a2) * (v *' (s1 *' g1))) + (((b2 / a1) * a1) * (- (v *' (s2 *' g2))))
by A22, A23, VECTSP_1:def 13
.=
(((b1 / a2) * a2) * (v *' (s1 *' g1))) + (((b2 / a1) * a1) * (v *' (- (s2 *' g2))))
by Th17
.=
(((b1 / a2) * a2) * (v *' (s1 *' g1))) + ((b1 / a2) * (a1 * (v *' (- (s2 *' g2)))))
by A19, POLYRED:11
.=
((b1 / a2) * (a2 * (v *' (s1 *' g1)))) + ((b1 / a2) * (a1 * (v *' (- (s2 *' g2)))))
by POLYRED:11
.=
(b1 / a2) * ((a2 * (v *' (s1 *' g1))) + (a1 * (v *' (- (s2 *' g2)))))
by Th19
.=
(b1 / a2) * ((a2 * (v *' (s1 *' g1))) + (v *' (a1 * (- (s2 *' g2)))))
by Th18
.=
(b1 / a2) * ((a2 * (v *' (s1 *' g1))) + (v *' (- (a1 * (s2 *' g2)))))
by POLYRED:9
.=
(b1 / a2) * ((v *' (a2 * (s1 *' g1))) + (v *' (- (a1 * (s2 *' g2)))))
by Th18
.=
(b1 / a2) * (v *' ((a2 * (s1 *' g1)) + (- (a1 * (s2 *' g2)))))
by Th16
.=
(b1 / a2) * (v *' (S-Poly g1,g2,T))
by A20, A21, POLYNOM1:def 23
.=
(Monom (b1 / a2),v) *' (S-Poly g1,g2,T)
by POLYRED:22
;
hence
PolyRedRel G,
T reduces (m1 *' g1) - (m2 *' g2),
0_ n,
L
by A2, A3, POLYRED:48;
:: thesis: verum end;
hence
PolyRedRel G,
T reduces (m1 *' g1) - (m2 *' g2),
0_ n,
L
;
:: thesis: verum
end; end;
hence
G is_Groebner_basis_wrt T
by A1, Th21; :: thesis: verum