let n be Ordinal; :: thesis: for T being connected admissible TermOrder of n
for L being non trivial right_complementable well-unital distributive add-associative right_zeroed domRing-like doubleLoopStr
for p being Polynomial of n,L
for m being non-zero Monomial of n,L
for i being Element of NAT st i <= card (Support p) holds
for b being bag of n holds
( (term m) + b in Support (Low ((m *' p),T,i)) iff b in Support (Low (p,T,i)) )
let T be connected admissible TermOrder of n; :: thesis: for L being non trivial right_complementable well-unital distributive add-associative right_zeroed domRing-like doubleLoopStr
for p being Polynomial of n,L
for m being non-zero Monomial of n,L
for i being Element of NAT st i <= card (Support p) holds
for b being bag of n holds
( (term m) + b in Support (Low ((m *' p),T,i)) iff b in Support (Low (p,T,i)) )
let L be non trivial right_complementable well-unital distributive add-associative right_zeroed domRing-like doubleLoopStr ; :: thesis: for p being Polynomial of n,L
for m being non-zero Monomial of n,L
for i being Element of NAT st i <= card (Support p) holds
for b being bag of n holds
( (term m) + b in Support (Low ((m *' p),T,i)) iff b in Support (Low (p,T,i)) )
let p be Polynomial of n,L; :: thesis: for m being non-zero Monomial of n,L
for i being Element of NAT st i <= card (Support p) holds
for b being bag of n holds
( (term m) + b in Support (Low ((m *' p),T,i)) iff b in Support (Low (p,T,i)) )
let m be non-zero Monomial of n,L; :: thesis: for i being Element of NAT st i <= card (Support p) holds
for b being bag of n holds
( (term m) + b in Support (Low ((m *' p),T,i)) iff b in Support (Low (p,T,i)) )
let i be Element of NAT ; :: thesis: ( i <= card (Support p) implies for b being bag of n holds
( (term m) + b in Support (Low ((m *' p),T,i)) iff b in Support (Low (p,T,i)) ) )
set l = Low (p,T,i);
assume A1: i <= card (Support p) ; :: thesis: for b being bag of n holds
( (term m) + b in Support (Low ((m *' p),T,i)) iff b in Support (Low (p,T,i)) )
then A2: Support (Low (p,T,i)) c= Support p by Th26;
A3: Support (Up (p,T,i)) = Upper_Support (p,T,i) by A1, Lm3;
then A4: card (Support (Up (p,T,i))) = i by A1, Def2;
A5: Support (Up (p,T,i)) c= Support p by A1, Th26;
A6: Support (Low (p,T,i)) = Lower_Support (p,T,i) by A1, Lm3;
let b be bag of n; :: thesis: ( (term m) + b in Support (Low ((m *' p),T,i)) iff b in Support (Low (p,T,i)) )
A7: i <= card (Support (m *' p)) by A1, Th10;
then A8: Support (Low ((m *' p),T,i)) = Lower_Support ((m *' p),T,i) by Lm3;
A9: Support (Low ((m *' p),T,i)) c= Support (m *' p) by A7, Th26;
A10: Support (Up ((m *' p),T,i)) c= Support (m *' p) by A7, Th26;
A11: Support (Up ((m *' p),T,i)) = Upper_Support ((m *' p),T,i) by A7, Lm3;
then A12: card (Support (Up ((m *' p),T,i))) = i by A7, Def2;
then A13: ( Support (Up (p,T,i)) = {} implies Support (Up ((m *' p),T,i)) = {} ) by A4;
A14: now :: thesis: ( (term m) + b in Support (Low ((m *' p),T,i)) implies b in Support (Low (p,T,i)) )
assume A15: (term m) + b in Support (Low ((m *' p),T,i)) ; :: thesis: b in Support (Low (p,T,i))
A16: now :: thesis: not (term m) + b in Support (Up ((m *' p),T,i))
assume (term m) + b in Support (Up ((m *' p),T,i)) ; :: thesis: contradiction
then (term m) + b in (Support (Up ((m *' p),T,i))) /\ (Support (Low ((m *' p),T,i))) by A15, XBOOLE_0:def 4;
hence contradiction by A7, A9, A15, Th28; :: thesis: verum
end;
A17: Support (m *' p) = { ((term m) + u) where u is Element of Bags n : u in Support p } by Th9;
A18: now :: thesis: not b in Support (Up (p,T,i))
defpred S1[ object , object ] means $1 = (term m) + (In ($2,(Bags n)));
assume A19: b in Support (Up (p,T,i)) ; :: thesis: contradiction
A20: now :: thesis: for b9 being bag of n st (term m) + b9 in Support (Up ((m *' p),T,i)) holds
b9 in Support (Up (p,T,i))
let b9 be bag of n; :: thesis: ( (term m) + b9 in Support (Up ((m *' p),T,i)) implies b9 in Support (Up (p,T,i)) )
assume A21: (term m) + b9 in Support (Up ((m *' p),T,i)) ; :: thesis: b9 in Support (Up (p,T,i))
then A22: (term m) + b < (term m) + b9,T by A7, A11, A8, A15, Th20;
not b9 <= b,T by A22, TERMORD:5, Th2;
then b < b9,T by TERMORD:5;
then A23: b <= b9,T by TERMORD:def 3;
b9 in Support p by A10, A21, Th8;
hence b9 in Support (Up (p,T,i)) by A1, A3, A19, A23, Def2; :: thesis: verum
end;
A24: for x being object st x in Support (Up ((m *' p),T,i)) holds
ex y being object st
( y in Support (Up (p,T,i)) & S1[x,y] )
proof
let x be object ; :: thesis: ( x in Support (Up ((m *' p),T,i)) implies ex y being object st
( y in Support (Up (p,T,i)) & S1[x,y] ) )
assume A25: x in Support (Up ((m *' p),T,i)) ; :: thesis: ex y being object st
( y in Support (Up (p,T,i)) & S1[x,y] )
then x in Support (m *' p) by A10;
then consider x9 being Element of Bags n such that
A26: x = (term m) + x9 and
x9 in Support p by A17;
take x9 ; :: thesis: ( x9 in Support (Up (p,T,i)) & S1[x,x9] )
thus ( x9 in Support (Up (p,T,i)) & S1[x,x9] ) by A20, A25, A26; :: thesis: verum
end;
consider f being Function of (Support (Up ((m *' p),T,i))),(Support (Up (p,T,i))) such that
A27: for x being object st x in Support (Up ((m *' p),T,i)) holds
S1[x,f . x] from FUNCT_2:sch 1(A24);
now :: thesis: for x1, x2 being object st x1 in dom f & x2 in dom f & f . x1 = f . x2 holds
x1 = x2
let x1, x2 be object ; :: thesis: ( x1 in dom f & x2 in dom f & f . x1 = f . x2 implies x1 = x2 )
assume that
A28: x1 in dom f and
A29: x2 in dom f and
A30: f . x1 = f . x2 ; :: thesis: x1 = x2
f . x2 in rng f by A29, FUNCT_1:3;
then A31: f . x2 in Support (Up (p,T,i)) ;
f . x1 in rng f by A28, FUNCT_1:3;
then f . x1 in Support (Up (p,T,i)) ;
then reconsider x19 = f . x1, x29 = f . x2 as Element of Bags n by A31;
A32: x19 = In (x19,(Bags n)) ;
x29 = In (x29,(Bags n)) ;
hence x1 = (term m) + x19 by A27, A28, A30
.= x2 by A27, A29, A30, A32 ;
:: thesis: verum
end;
then A33: f is one-to-one by FUNCT_1:def 4;
Support (Up ((m *' p),T,i)) c= dom f by A13, FUNCT_2:def 1;
then Support (Up ((m *' p),T,i)),f .: (Support (Up ((m *' p),T,i))) are_equipotent by A33, CARD_1:33;
then card (f .: (Support (Up ((m *' p),T,i)))) = card (Support (Up ((m *' p),T,i))) by CARD_1:5
.= i by A7, A11, Def2 ;
then b in f .: (Support (Up ((m *' p),T,i))) by A4, A19, CARD_2:102;
then consider bb being object such that
A34: bb in dom f and
A35: ( bb in Support (Up ((m *' p),T,i)) & f . bb = b ) by FUNCT_1:def 6;
f . bb in rng f by A34, FUNCT_1:3;
then f . bb in Support (Up (p,T,i)) ;
then reconsider bb9 = f . bb as Element of Bags n ;
bb9 = In (bb9,(Bags n)) ;
hence contradiction by A16, A27, A35; :: thesis: verum
end;
(term m) + b in Support (m *' p) by A9, A15;
then (term m) + b in { ((term m) + u) where u is Element of Bags n : u in Support p } by Th9;
then consider u being Element of Bags n such that
A36: (term m) + b = (term m) + u and
A37: u in Support p ;
b = ((term m) + b) -' (term m) by PRE_POLY:48
.= u by A36, PRE_POLY:48 ;
hence b in Support (Low (p,T,i)) by A1, A37, A18, Th28; :: thesis: verum
end;
A38: ( Support (Up ((m *' p),T,i)) = {} implies Support (Up (p,T,i)) = {} ) by A12, A4;
now :: thesis: ( b in Support (Low (p,T,i)) implies (term m) + b in Support (Low ((m *' p),T,i)) )
assume A39: b in Support (Low (p,T,i)) ; :: thesis: (term m) + b in Support (Low ((m *' p),T,i))
A40: now :: thesis: not b in Support (Up (p,T,i))
assume b in Support (Up (p,T,i)) ; :: thesis: contradiction
then b in (Support (Up (p,T,i))) /\ (Support (Low (p,T,i))) by A39, XBOOLE_0:def 4;
hence contradiction by A1, A2, A39, Th28; :: thesis: verum
end;
A41: now :: thesis: not (term m) + b in Support (Up ((m *' p),T,i))
defpred S1[ object , object ] means $2 = (term m) + (In ($1,(Bags n)));
assume A42: (term m) + b in Support (Up ((m *' p),T,i)) ; :: thesis: contradiction
A43: now :: thesis: for b9 being bag of n st b9 in Support (Up (p,T,i)) holds
(term m) + b9 in Support (Up ((m *' p),T,i))
let b9 be bag of n; :: thesis: ( b9 in Support (Up (p,T,i)) implies (term m) + b9 in Support (Up ((m *' p),T,i)) )
assume A44: b9 in Support (Up (p,T,i)) ; :: thesis: (term m) + b9 in Support (Up ((m *' p),T,i))
then (term m) + b < (term m) + b9,T by A1, A3, A6, A39, Th4, Th20;
then A45: (term m) + b <= (term m) + b9,T by TERMORD:def 3;
(term m) + b9 in Support (m *' p) by A5, A44, Th8;
hence (term m) + b9 in Support (Up ((m *' p),T,i)) by A7, A11, A42, A45, Def2; :: thesis: verum
end;
A46: for x being object st x in Support (Up (p,T,i)) holds
ex y being object st
( y in Support (Up ((m *' p),T,i)) & S1[x,y] )
proof
let x be object ; :: thesis: ( x in Support (Up (p,T,i)) implies ex y being object st
( y in Support (Up ((m *' p),T,i)) & S1[x,y] ) )
assume A47: x in Support (Up (p,T,i)) ; :: thesis: ex y being object st
( y in Support (Up ((m *' p),T,i)) & S1[x,y] )
then reconsider x9 = x as Element of Bags n ;
take (term m) + x9 ; :: thesis: ( (term m) + x9 in Support (Up ((m *' p),T,i)) & S1[x,(term m) + x9] )
thus ( (term m) + x9 in Support (Up ((m *' p),T,i)) & S1[x,(term m) + x9] ) by A43, A47; :: thesis: verum
end;
consider f being Function of (Support (Up (p,T,i))),(Support (Up ((m *' p),T,i))) such that
A48: for x being object st x in Support (Up (p,T,i)) holds
S1[x,f . x] from FUNCT_2:sch 1(A46);
now :: thesis: for x1, x2 being object st x1 in dom f & x2 in dom f & f . x1 = f . x2 holds
x1 = x2
let x1, x2 be object ; :: thesis: ( x1 in dom f & x2 in dom f & f . x1 = f . x2 implies x1 = x2 )
assume that
A49: x1 in dom f and
A50: x2 in dom f and
A51: f . x1 = f . x2 ; :: thesis: x1 = x2
( x1 in Support (Up (p,T,i)) & x2 in Support (Up (p,T,i)) ) by A49, A50;
then reconsider x = x1, y = x2 as Element of Bags n ;
y = In (y,(Bags n)) ;
then A52: f . y = (term m) + y by A48, A50;
x = In (x,(Bags n)) ;
then A53: f . x = (term m) + x by A48, A49;
thus x1 = ((term m) + x) -' (term m) by PRE_POLY:48
.= x2 by A51, A53, A52, PRE_POLY:48 ; :: thesis: verum
end;
then A54: f is one-to-one by FUNCT_1:def 4;
Support (Up (p,T,i)) c= dom f by A38, FUNCT_2:def 1;
then Support (Up (p,T,i)),f .: (Support (Up (p,T,i))) are_equipotent by A54, CARD_1:33;
then card (f .: (Support (Up (p,T,i)))) = card (Support (Up (p,T,i))) by CARD_1:5
.= i by A1, A3, Def2 ;
then (term m) + b in f .: (Support (Up (p,T,i))) by A12, A42, CARD_2:102;
then consider bb being object such that
A55: bb in dom f and
A56: bb in Support (Up (p,T,i)) and
A57: f . bb = (term m) + b by FUNCT_1:def 6;
reconsider bb = bb as Element of Bags n by A56;
bb = In (bb,(Bags n)) ;
then A58: (term m) + bb = (term m) + b by A48, A55, A57;
bb = ((term m) + bb) -' (term m) by PRE_POLY:48
.= b by A58, PRE_POLY:48 ;
hence contradiction by A40, A55; :: thesis: verum
end;
(term m) + b in Support (m *' p) by A2, A39, Th8;
hence (term m) + b in Support (Low ((m *' p),T,i)) by A7, A41, Th28; :: thesis: verum
end;
hence ( (term m) + b in Support (Low ((m *' p),T,i)) iff b in Support (Low (p,T,i)) ) by A14; :: thesis: verum