let n be Ordinal; for T being connected admissible TermOrder of n
for L being non empty non degenerated right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative doubleLoopStr
for I being add-closed left-ideal Subset of (Polynom-Ring (n,L))
for m being Monomial of n,L
for f, g being Polynomial of n,L st f in I & g in I & HM (f,T) = m & HM (g,T) = m & ( for p being Polynomial of n,L holds
( not p in I or not p < f,T or not HM (p,T) = m ) ) & ( for p being Polynomial of n,L holds
( not p in I or not p < g,T or not HM (p,T) = m ) ) holds
f = g
let T be connected admissible TermOrder of n; for L being non empty non degenerated right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative doubleLoopStr
for I being add-closed left-ideal Subset of (Polynom-Ring (n,L))
for m being Monomial of n,L
for f, g being Polynomial of n,L st f in I & g in I & HM (f,T) = m & HM (g,T) = m & ( for p being Polynomial of n,L holds
( not p in I or not p < f,T or not HM (p,T) = m ) ) & ( for p being Polynomial of n,L holds
( not p in I or not p < g,T or not HM (p,T) = m ) ) holds
f = g
let L be non empty non degenerated right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative doubleLoopStr ; for I being add-closed left-ideal Subset of (Polynom-Ring (n,L))
for m being Monomial of n,L
for f, g being Polynomial of n,L st f in I & g in I & HM (f,T) = m & HM (g,T) = m & ( for p being Polynomial of n,L holds
( not p in I or not p < f,T or not HM (p,T) = m ) ) & ( for p being Polynomial of n,L holds
( not p in I or not p < g,T or not HM (p,T) = m ) ) holds
f = g
let I be add-closed left-ideal Subset of (Polynom-Ring (n,L)); for m being Monomial of n,L
for f, g being Polynomial of n,L st f in I & g in I & HM (f,T) = m & HM (g,T) = m & ( for p being Polynomial of n,L holds
( not p in I or not p < f,T or not HM (p,T) = m ) ) & ( for p being Polynomial of n,L holds
( not p in I or not p < g,T or not HM (p,T) = m ) ) holds
f = g
let m be Monomial of n,L; for f, g being Polynomial of n,L st f in I & g in I & HM (f,T) = m & HM (g,T) = m & ( for p being Polynomial of n,L holds
( not p in I or not p < f,T or not HM (p,T) = m ) ) & ( for p being Polynomial of n,L holds
( not p in I or not p < g,T or not HM (p,T) = m ) ) holds
f = g
let f, g be Polynomial of n,L; ( f in I & g in I & HM (f,T) = m & HM (g,T) = m & ( for p being Polynomial of n,L holds
( not p in I or not p < f,T or not HM (p,T) = m ) ) & ( for p being Polynomial of n,L holds
( not p in I or not p < g,T or not HM (p,T) = m ) ) implies f = g )
assume that
A1:
f in I
and
A2:
g in I
and
A3:
HM (f,T) = m
and
A4:
HM (g,T) = m
; ( ex p being Polynomial of n,L st
( p in I & p < f,T & HM (p,T) = m ) or ex p being Polynomial of n,L st
( p in I & p < g,T & HM (p,T) = m ) or f = g )
A5: HT (f,T) =
term (HM (f,T))
by TERMORD:22
.=
HT (g,T)
by A3, A4, TERMORD:22
;
A6: HC (f,T) =
f . (HT (f,T))
by TERMORD:def 7
.=
(HM (f,T)) . (HT (f,T))
by TERMORD:18
.=
g . (HT (g,T))
by A3, A4, A5, TERMORD:18
.=
HC (g,T)
by TERMORD:def 7
;
assume that
A7:
for p being Polynomial of n,L holds
( not p in I or not p < f,T or not HM (p,T) = m )
and
A8:
for p being Polynomial of n,L holds
( not p in I or not p < g,T or not HM (p,T) = m )
; f = g
reconsider I = I as LeftIdeal of (Polynom-Ring (n,L)) by A1;
per cases
( f - g = 0_ (n,L) or f - g <> 0_ (n,L) )
;
suppose A9:
f - g <> 0_ (
n,
L)
;
f = gnow ( ( f = 0_ (n,L) & f = g ) or ( g = 0_ (n,L) & f = g ) or ( f <> 0_ (n,L) & g <> 0_ (n,L) & contradiction ) )per cases
( f = 0_ (n,L) or g = 0_ (n,L) or ( f <> 0_ (n,L) & g <> 0_ (n,L) ) )
;
case A12:
(
f <> 0_ (
n,
L) &
g <> 0_ (
n,
L) )
;
contradictionset s =
HT (
(f - g),
T);
set d =
(f . (HT ((f - g),T))) - (g . (HT ((f - g),T)));
set c =
(f . (HT ((f - g),T))) * (((f . (HT ((f - g),T))) - (g . (HT ((f - g),T)))) ");
set h =
f - (((f . (HT ((f - g),T))) * (((f . (HT ((f - g),T))) - (g . (HT ((f - g),T)))) ")) * (f - g));
A13:
Support (f - g) <> {}
by A9, POLYNOM7:1;
then A14:
HT (
(f - g),
T)
in Support (f - g)
by TERMORD:def 6;
A15:
now not HT ((f - g),T) = HT (f,T)assume
HT (
(f - g),
T)
= HT (
f,
T)
;
contradictionthen (f - g) . (HT ((f - g),T)) =
(f + (- g)) . (HT (f,T))
by POLYNOM1:def 7
.=
(f . (HT (f,T))) + ((- g) . (HT (g,T)))
by A5, POLYNOM1:15
.=
(f . (HT (f,T))) + (- (g . (HT (g,T))))
by POLYNOM1:17
.=
(HC (f,T)) + (- (g . (HT (g,T))))
by TERMORD:def 7
.=
(HC (f,T)) + (- (HC (g,T)))
by TERMORD:def 7
.=
0. L
by A6, RLVECT_1:5
;
hence
contradiction
by A14, POLYNOM1:def 4;
verum end;
HT (
(f - g),
T)
<= max (
(HT (f,T)),
(HT (f,T)),
T),
T
by A5, Th7;
then
HT (
(f - g),
T)
<= HT (
f,
T),
T
by TERMORD:12;
then
HT (
(f - g),
T)
< HT (
f,
T),
T
by A15, TERMORD:def 3;
then
not
HT (
f,
T)
<= HT (
(f - g),
T),
T
by TERMORD:5;
then
not
HT (
f,
T)
in Support (f - g)
by TERMORD:def 6;
then A16:
(f - g) . (HT (f,T)) = 0. L
by POLYNOM1:def 4;
A17:
(f - (((f . (HT ((f - g),T))) * (((f . (HT ((f - g),T))) - (g . (HT ((f - g),T)))) ")) * (f - g))) . (HT (f,T)) =
(f + (- (((f . (HT ((f - g),T))) * (((f . (HT ((f - g),T))) - (g . (HT ((f - g),T)))) ")) * (f - g)))) . (HT (f,T))
by POLYNOM1:def 7
.=
(f . (HT (f,T))) + ((- (((f . (HT ((f - g),T))) * (((f . (HT ((f - g),T))) - (g . (HT ((f - g),T)))) ")) * (f - g))) . (HT (f,T)))
by POLYNOM1:15
.=
(f . (HT (f,T))) + (- ((((f . (HT ((f - g),T))) * (((f . (HT ((f - g),T))) - (g . (HT ((f - g),T)))) ")) * (f - g)) . (HT (f,T))))
by POLYNOM1:17
.=
(f . (HT (f,T))) + (- (((f . (HT ((f - g),T))) * (((f . (HT ((f - g),T))) - (g . (HT ((f - g),T)))) ")) * (0. L)))
by A16, POLYNOM7:def 9
.=
(f . (HT (f,T))) + (- (0. L))
.=
(f . (HT (f,T))) + (0. L)
by RLVECT_1:12
.=
f . (HT (f,T))
by RLVECT_1:def 4
;
Support f <> {}
by A12, POLYNOM7:1;
then
HT (
f,
T)
in Support f
by TERMORD:def 6;
then
(f - (((f . (HT ((f - g),T))) * (((f . (HT ((f - g),T))) - (g . (HT ((f - g),T)))) ")) * (f - g))) . (HT (f,T)) <> 0. L
by A17, POLYNOM1:def 4;
then A18:
HT (
f,
T)
in Support (f - (((f . (HT ((f - g),T))) * (((f . (HT ((f - g),T))) - (g . (HT ((f - g),T)))) ")) * (f - g)))
by POLYNOM1:def 4;
then A19:
HT (
f,
T)
<= HT (
(f - (((f . (HT ((f - g),T))) * (((f . (HT ((f - g),T))) - (g . (HT ((f - g),T)))) ")) * (f - g))),
T),
T
by TERMORD:def 6;
Support (f - (((f . (HT ((f - g),T))) * (((f . (HT ((f - g),T))) - (g . (HT ((f - g),T)))) ")) * (f - g))) = Support (f + (- (((f . (HT ((f - g),T))) * (((f . (HT ((f - g),T))) - (g . (HT ((f - g),T)))) ")) * (f - g))))
by POLYNOM1:def 7;
then
Support (f - (((f . (HT ((f - g),T))) * (((f . (HT ((f - g),T))) - (g . (HT ((f - g),T)))) ")) * (f - g))) c= (Support f) \/ (Support (- (((f . (HT ((f - g),T))) * (((f . (HT ((f - g),T))) - (g . (HT ((f - g),T)))) ")) * (f - g))))
by POLYNOM1:20;
then A20:
Support (f - (((f . (HT ((f - g),T))) * (((f . (HT ((f - g),T))) - (g . (HT ((f - g),T)))) ")) * (f - g))) c= (Support f) \/ (Support (((f . (HT ((f - g),T))) * (((f . (HT ((f - g),T))) - (g . (HT ((f - g),T)))) ")) * (f - g)))
by Th5;
(Support f) \/ (Support (((f . (HT ((f - g),T))) * (((f . (HT ((f - g),T))) - (g . (HT ((f - g),T)))) ")) * (f - g))) c= (Support f) \/ (Support (f - g))
by POLYRED:19, XBOOLE_1:9;
then A21:
Support (f - (((f . (HT ((f - g),T))) * (((f . (HT ((f - g),T))) - (g . (HT ((f - g),T)))) ")) * (f - g))) c= (Support f) \/ (Support (f - g))
by A20;
not
g < f,
T
by A2, A4, A7;
then A22:
f <= g,
T
by POLYRED:29;
not
f < g,
T
by A1, A3, A8;
then
g <= f,
T
by POLYRED:29;
then A23:
Support f = Support g
by A22, POLYRED:26;
(
Support (f - g) = Support (f + (- g)) &
Support (f + (- g)) c= (Support f) \/ (Support (- g)) )
by POLYNOM1:20, POLYNOM1:def 7;
then A24:
Support (f - g) c= (Support f) \/ (Support g)
by Th5;
then A25:
(Support f) \/ (Support (f - g)) c= (Support f) \/ (Support f)
by A23, XBOOLE_1:9;
then A26:
Support (f - (((f . (HT ((f - g),T))) * (((f . (HT ((f - g),T))) - (g . (HT ((f - g),T)))) ")) * (f - g))) c= Support f
by A21;
HT (
(f - (((f . (HT ((f - g),T))) * (((f . (HT ((f - g),T))) - (g . (HT ((f - g),T)))) ")) * (f - g))),
T)
in Support (f - (((f . (HT ((f - g),T))) * (((f . (HT ((f - g),T))) - (g . (HT ((f - g),T)))) ")) * (f - g)))
by A18, TERMORD:def 6;
then
HT (
(f - (((f . (HT ((f - g),T))) * (((f . (HT ((f - g),T))) - (g . (HT ((f - g),T)))) ")) * (f - g))),
T)
<= HT (
f,
T),
T
by A26, TERMORD:def 6;
then A27:
HT (
(f - (((f . (HT ((f - g),T))) * (((f . (HT ((f - g),T))) - (g . (HT ((f - g),T)))) ")) * (f - g))),
T)
= HT (
f,
T)
by A19, TERMORD:7;
then HC (
(f - (((f . (HT ((f - g),T))) * (((f . (HT ((f - g),T))) - (g . (HT ((f - g),T)))) ")) * (f - g))),
T) =
f . (HT (f,T))
by A17, TERMORD:def 7
.=
HC (
f,
T)
by TERMORD:def 7
;
then A28:
HM (
(f - (((f . (HT ((f - g),T))) * (((f . (HT ((f - g),T))) - (g . (HT ((f - g),T)))) ")) * (f - g))),
T) =
Monom (
(HC (f,T)),
(HT (f,T)))
by A27, TERMORD:def 8
.=
m
by A3, TERMORD:def 8
;
reconsider cp =
(((f . (HT ((f - g),T))) * (((f . (HT ((f - g),T))) - (g . (HT ((f - g),T)))) ")) | (n,L)) *' (f - g) as
Element of
(Polynom-Ring (n,L)) by POLYNOM1:def 11;
reconsider cc =
((f . (HT ((f - g),T))) * (((f . (HT ((f - g),T))) - (g . (HT ((f - g),T)))) ")) | (
n,
L) as
Element of
(Polynom-Ring (n,L)) by POLYNOM1:def 11;
reconsider f9 =
f,
g9 =
g as
Element of
(Polynom-Ring (n,L)) by POLYNOM1:def 11;
A29:
(f - g) . (HT ((f - g),T)) =
(f + (- g)) . (HT ((f - g),T))
by POLYNOM1:def 7
.=
(f . (HT ((f - g),T))) + ((- g) . (HT ((f - g),T)))
by POLYNOM1:15
.=
(f . (HT ((f - g),T))) + (- (g . (HT ((f - g),T))))
by POLYNOM1:17
.=
(f . (HT ((f - g),T))) - (g . (HT ((f - g),T)))
;
A30:
HT (
(f - g),
T)
in Support (f - g)
by A13, TERMORD:def 6;
A31:
now not Support (f - (((f . (HT ((f - g),T))) * (((f . (HT ((f - g),T))) - (g . (HT ((f - g),T)))) ")) * (f - g))) = Support fA32:
(f - g) . (HT ((f - g),T)) <> 0. L
by A30, POLYNOM1:def 4;
A33:
- (((f . (HT ((f - g),T))) * (((f . (HT ((f - g),T))) - (g . (HT ((f - g),T)))) ")) * ((f . (HT ((f - g),T))) - (g . (HT ((f - g),T))))) =
- ((f . (HT ((f - g),T))) * ((((f . (HT ((f - g),T))) - (g . (HT ((f - g),T)))) ") * ((f . (HT ((f - g),T))) - (g . (HT ((f - g),T))))))
by GROUP_1:def 3
.=
- ((f . (HT ((f - g),T))) * (1. L))
by A29, A32, VECTSP_1:def 10
.=
- (f . (HT ((f - g),T)))
;
assume A34:
Support (f - (((f . (HT ((f - g),T))) * (((f . (HT ((f - g),T))) - (g . (HT ((f - g),T)))) ")) * (f - g))) = Support f
;
contradiction(f - (((f . (HT ((f - g),T))) * (((f . (HT ((f - g),T))) - (g . (HT ((f - g),T)))) ")) * (f - g))) . (HT ((f - g),T)) =
(f + (- (((f . (HT ((f - g),T))) * (((f . (HT ((f - g),T))) - (g . (HT ((f - g),T)))) ")) * (f - g)))) . (HT ((f - g),T))
by POLYNOM1:def 7
.=
(f . (HT ((f - g),T))) + ((- (((f . (HT ((f - g),T))) * (((f . (HT ((f - g),T))) - (g . (HT ((f - g),T)))) ")) * (f - g))) . (HT ((f - g),T)))
by POLYNOM1:15
.=
(f . (HT ((f - g),T))) + (((- ((f . (HT ((f - g),T))) * (((f . (HT ((f - g),T))) - (g . (HT ((f - g),T)))) "))) * (f - g)) . (HT ((f - g),T)))
by POLYRED:9
.=
(f . (HT ((f - g),T))) + ((- ((f . (HT ((f - g),T))) * (((f . (HT ((f - g),T))) - (g . (HT ((f - g),T)))) "))) * ((f - g) . (HT ((f - g),T))))
by POLYNOM7:def 9
.=
(f . (HT ((f - g),T))) + (- (f . (HT ((f - g),T))))
by A29, A33, VECTSP_1:9
.=
0. L
by RLVECT_1:5
;
hence
contradiction
by A23, A14, A24, A34, POLYNOM1:def 4;
verum end;
f - (((f . (HT ((f - g),T))) * (((f . (HT ((f - g),T))) - (g . (HT ((f - g),T)))) ")) * (f - g)) <= f,
T
by A21, A25, Th8, XBOOLE_1:1;
then A35:
f - (((f . (HT ((f - g),T))) * (((f . (HT ((f - g),T))) - (g . (HT ((f - g),T)))) ")) * (f - g)) < f,
T
by A31, POLYRED:def 3;
reconsider cp =
cp as
Element of
(Polynom-Ring (n,L)) ;
reconsider cc =
cc as
Element of
(Polynom-Ring (n,L)) ;
reconsider f9 =
f9,
g9 =
g9 as
Element of
(Polynom-Ring (n,L)) ;
f - g = f9 - g9
by Lm2;
then A36:
cp = cc * (f9 - g9)
by POLYNOM1:def 11;
f9 - g9 in I
by A1, A2, IDEAL_1:15;
then A37:
cc * (f9 - g9) in I
by IDEAL_1:def 2;
f9 - cp =
f - ((((f . (HT ((f - g),T))) * (((f . (HT ((f - g),T))) - (g . (HT ((f - g),T)))) ")) | (n,L)) *' (f - g))
by Lm2
.=
f - (((f . (HT ((f - g),T))) * (((f . (HT ((f - g),T))) - (g . (HT ((f - g),T)))) ")) * (f - g))
by POLYNOM7:27
;
hence
contradiction
by A1, A7, A28, A35, A37, A36, IDEAL_1:15;
verum end; end; end; hence
f = g
;
verum end; end;