let n be Ordinal; :: 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 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; :: 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 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 associative commutative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; :: thesis: 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); :: thesis: 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; :: thesis: 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; :: thesis: ( 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 ; :: thesis: ( 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 ) ; :: thesis: 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 f - g = 0_ n,L ; :: thesis: f = g
hence g = (f - g) + g by POLYRED:2
.= (f + (- g)) + g by POLYNOM1:def 23
.= f + ((- g) + g) by POLYNOM1:80
.= f + (0_ n,L) by POLYRED:3
.= f by POLYNOM1:82 ;
:: thesis: verum
end;
suppose A9: f - g <> 0_ n,L ; :: thesis: f = g
now
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 ) ; :: thesis: contradiction
set 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
assume HT (f - g),T = HT f,T ; :: thesis: contradiction
then (f - g) . (HT (f - g),T) = (f + (- g)) . (HT f,T) by POLYNOM1:def 23
.= (f . (HT f,T)) + ((- g) . (HT g,T)) by A5, POLYNOM1:def 21
.= (f . (HT f,T)) + (- (g . (HT g,T))) by POLYNOM1:def 22
.= (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:16 ;
hence contradiction by A14, POLYNOM1:def 9; :: thesis: 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 9;
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 23
.= (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:def 21
.= (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:def 22
.= (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 10
.= (f . (HT f,T)) + (- (0. L)) by VECTSP_1:39
.= (f . (HT f,T)) + (0. L) by RLVECT_1:25
.= f . (HT f,T) by RLVECT_1:def 7 ;
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 9;
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 9;
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 23;
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:79;
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, XBOOLE_1:1;
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:79, POLYNOM1:def 23;
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, XBOOLE_1:1;
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 27;
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 27;
reconsider f9 = f, g9 = g as Element of (Polynom-Ring n,L) by POLYNOM1:def 27;
A29: (f - g) . (HT (f - g),T) = (f + (- g)) . (HT (f - g),T) by POLYNOM1:def 23
.= (f . (HT (f - g),T)) + ((- g) . (HT (f - g),T)) by POLYNOM1:def 21
.= (f . (HT (f - g),T)) + (- (g . (HT (f - g),T))) by POLYNOM1:def 22
.= (f . (HT (f - g),T)) - (g . (HT (f - g),T)) by RLVECT_1:def 14 ;
A30: HT (f - g),T in Support (f - g) by A13, TERMORD:def 6;
A31: now
A32: (f - g) . (HT (f - g),T) <> 0. L by A30, POLYNOM1:def 9;
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 4
.= - ((f . (HT (f - g),T)) * (1. L)) by A29, A32, VECTSP_1:def 22
.= - (f . (HT (f - g),T)) by VECTSP_1:def 19 ;
assume A34: Support (f - (((f . (HT (f - g),T)) * (((f . (HT (f - g),T)) - (g . (HT (f - g),T))) " )) * (f - g))) = Support f ; :: thesis: 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 23
.= (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:def 21
.= (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 10
.= (f . (HT (f - g),T)) + (- (f . (HT (f - g),T))) by A29, A33, VECTSP_1:41
.= 0. L by RLVECT_1:16 ;
hence contradiction by A23, A14, A24, A34, POLYNOM1:def 9; :: thesis: 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 27;
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; :: thesis: verum
end;
end;
end;
hence f = g ; :: thesis: verum
end;
end;