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 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 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 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 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 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 holds
( (term m) + b in Support (Low (m *' p),T,i) iff b in Support (Low p,T,i) ) )
assume A1:
i <= card (Support p)
; :: thesis: for b being bag of holds
( (term m) + b in Support (Low (m *' p),T,i) iff b in Support (Low p,T,i) )
then A2:
i <= card (Support (m *' p))
by Th10;
let b be bag of ; :: thesis: ( (term m) + b in Support (Low (m *' p),T,i) iff b in Support (Low p,T,i) )
set l = Low p,T,i;
A3:
Support (Low p,T,i) c= Support p
by A1, Th26;
A4:
( Support (Up p,T,i) = Upper_Support p,T,i & Support (Low p,T,i) = Lower_Support p,T,i )
by A1, Lm3;
A5:
( Support (Up (m *' p),T,i) = Upper_Support (m *' p),T,i & Support (Low (m *' p),T,i) = Lower_Support (m *' p),T,i )
by A2, Lm3;
A6:
Support (Up p,T,i) c= Support p
by A1, Th26;
A7:
card (Support (Up (m *' p),T,i)) = i
by A2, A5, Def2;
A8:
card (Support (Up p,T,i)) = i
by A1, A4, Def2;
A9:
( Support (Low (m *' p),T,i) c= Support (m *' p) & Support (Up (m *' p),T,i) c= Support (m *' p) )
by A2, Th26;
A10:
( Support (Up (m *' p),T,i) = {} implies Support (Up p,T,i) = {} )
by A7, A8;
A11:
( Support (Up p,T,i) = {} implies Support (Up (m *' p),T,i) = {} )
by A7, A8;
A12:
now assume A13:
b in Support (Low p,T,i)
;
:: thesis: (term m) + b in Support (Low (m *' p),T,i)then A14:
(term m) + b in Support (m *' p)
by A3, Th8;
A15:
now assume
b in Support (Up p,T,i)
;
:: thesis: contradictionthen
b in (Support (Up p,T,i)) /\ (Support (Low p,T,i))
by A13, XBOOLE_0:def 4;
hence
contradiction
by A1, A3, A13, Th28;
:: thesis: verum end; now assume A16:
(term m) + b in Support (Up (m *' p),T,i)
;
:: thesis: contradictionA17:
now let b' be
bag of ;
:: thesis: ( b' in Support (Up p,T,i) implies (term m) + b' in Support (Up (m *' p),T,i) )assume A18:
b' in Support (Up p,T,i)
;
:: thesis: (term m) + b' in Support (Up (m *' p),T,i)then A19:
(term m) + b' in Support (m *' p)
by A6, Th8;
(term m) + b < (term m) + b',
T
by A1, A4, A13, A18, Th4, Th20;
then
(term m) + b <= (term m) + b',
T
by TERMORD:def 3;
hence
(term m) + b' in Support (Up (m *' p),T,i)
by A2, A5, A16, A19, Def2;
:: thesis: verum end; defpred S1[
set ,
set ]
means $2
= (term m) + ((In $1,(Bags n)) @ );
A20:
for
x being
set st
x in Support (Up p,T,i) holds
ex
y being
set st
(
y in Support (Up (m *' p),T,i) &
S1[
x,
y] )
proof
let x be
set ;
:: thesis: ( x in Support (Up p,T,i) implies ex y being set st
( y in Support (Up (m *' p),T,i) & S1[x,y] ) )
assume A21:
x in Support (Up p,T,i)
;
:: thesis: ex y being set st
( y in Support (Up (m *' p),T,i) & S1[x,y] )
then reconsider x' =
x as
Element of
Bags n ;
take
(term m) + x'
;
:: thesis: ( (term m) + x' in Support (Up (m *' p),T,i) & S1[x,(term m) + x'] )
x' =
In x',
(Bags n)
by FUNCT_7:def 1
.=
(In x',(Bags n)) @
by POLYNOM2:def 3
;
hence
(
(term m) + x' in Support (Up (m *' p),T,i) &
S1[
x,
(term m) + x'] )
by A17, A21;
:: thesis: verum
end; consider f being
Function of
(Support (Up p,T,i)),
(Support (Up (m *' p),T,i)) such that A22:
for
x being
set st
x in Support (Up p,T,i) holds
S1[
x,
f . x]
from FUNCT_2:sch 1(A20);
now let x1,
x2 be
set ;
:: thesis: ( x1 in dom f & x2 in dom f & f . x1 = f . x2 implies x1 = x2 )assume A23:
(
x1 in dom f &
x2 in dom f &
f . x1 = f . x2 )
;
:: thesis: x1 = x2then
(
x1 in Support (Up p,T,i) &
x2 in Support (Up p,T,i) )
;
then reconsider x =
x1,
y =
x2 as
Element of
Bags n ;
A24:
y =
In y,
(Bags n)
by FUNCT_7:def 1
.=
(In y,(Bags n)) @
by POLYNOM2:def 3
;
x =
In x,
(Bags n)
by FUNCT_7:def 1
.=
(In x,(Bags n)) @
by POLYNOM2:def 3
;
then A25:
(
f . x = (term m) + x &
f . y = (term m) + y )
by A22, A23, A24;
thus x1 =
((term m) + x) -' (term m)
by POLYNOM1:52
.=
x2
by A23, A25, POLYNOM1:52
;
:: thesis: verum end; then A26:
f is
one-to-one
by FUNCT_1:def 8;
Support (Up p,T,i) c= dom f
by A10, FUNCT_2:def 1;
then
Support (Up p,T,i),
f .: (Support (Up p,T,i)) are_equipotent
by A26, CARD_1:60;
then card (f .: (Support (Up p,T,i))) =
card (Support (Up p,T,i))
by CARD_1:21
.=
i
by A1, A4, Def2
;
then
(term m) + b in f .: (Support (Up p,T,i))
by A7, A16, TRIANG_1:3;
then consider bb being
set such that A27:
(
bb in dom f &
bb in Support (Up p,T,i) &
f . bb = (term m) + b )
by FUNCT_1:def 12;
reconsider bb =
bb as
Element of
Bags n by A27;
bb =
In bb,
(Bags n)
by FUNCT_7:def 1
.=
(In bb,(Bags n)) @
by POLYNOM2:def 3
;
then A28:
(term m) + bb = (term m) + b
by A22, A27;
bb =
((term m) + bb) -' (term m)
by POLYNOM1:52
.=
b
by A28, POLYNOM1:52
;
hence
contradiction
by A15, A27;
:: thesis: verum end; hence
(term m) + b in Support (Low (m *' p),T,i)
by A2, A14, Th28;
:: thesis: verum end;
now assume A29:
(term m) + b in Support (Low (m *' p),T,i)
;
:: thesis: b in Support (Low p,T,i)then A30:
(term m) + b in Support (m *' p)
by A9;
A31:
Support (m *' p) = { ((term m) + u) where u is Element of Bags n : u in Support p }
by Th9;
(term m) + b in { ((term m) + u) where u is Element of Bags n : u in Support p }
by A30, Th9;
then consider u being
Element of
Bags n such that A32:
(
(term m) + b = (term m) + u &
u in Support p )
;
A33:
b =
((term m) + b) -' (term m)
by POLYNOM1:52
.=
u
by A32, POLYNOM1:52
;
A34:
now assume
(term m) + b in Support (Up (m *' p),T,i)
;
:: thesis: contradictionthen
(term m) + b in (Support (Up (m *' p),T,i)) /\ (Support (Low (m *' p),T,i))
by A29, XBOOLE_0:def 4;
hence
contradiction
by A2, A9, A29, Th28;
:: thesis: verum end; now assume A35:
b in Support (Up p,T,i)
;
:: thesis: contradictionA36:
now let b' be
bag of ;
:: thesis: ( (term m) + b' in Support (Up (m *' p),T,i) implies b' in Support (Up p,T,i) )assume A37:
(term m) + b' in Support (Up (m *' p),T,i)
;
:: thesis: b' in Support (Up p,T,i)then A38:
b' in Support p
by A9, Th8;
A39:
(term m) + b < (term m) + b',
T
by A2, A5, A29, A37, Th20;
then
b < b',
T
by TERMORD:5;
then
b <= b',
T
by TERMORD:def 3;
hence
b' in Support (Up p,T,i)
by A1, A4, A35, A38, Def2;
:: thesis: verum end; defpred S1[
set ,
set ]
means $1
= (term m) + ((In $2,(Bags n)) @ );
A40:
for
x being
set st
x in Support (Up (m *' p),T,i) holds
ex
y being
set st
(
y in Support (Up p,T,i) &
S1[
x,
y] )
proof
let x be
set ;
:: thesis: ( x in Support (Up (m *' p),T,i) implies ex y being set st
( y in Support (Up p,T,i) & S1[x,y] ) )
assume A41:
x in Support (Up (m *' p),T,i)
;
:: thesis: ex y being set st
( y in Support (Up p,T,i) & S1[x,y] )
then
x in Support (m *' p)
by A9;
then consider x' being
Element of
Bags n such that A42:
(
x = (term m) + x' &
x' in Support p )
by A31;
take
x'
;
:: thesis: ( x' in Support (Up p,T,i) & S1[x,x'] )
x' =
In x',
(Bags n)
by FUNCT_7:def 1
.=
(In x',(Bags n)) @
by POLYNOM2:def 3
;
hence
(
x' in Support (Up p,T,i) &
S1[
x,
x'] )
by A36, A41, A42;
:: thesis: verum
end; consider f being
Function of
(Support (Up (m *' p),T,i)),
(Support (Up p,T,i)) such that A43:
for
x being
set st
x in Support (Up (m *' p),T,i) holds
S1[
x,
f . x]
from FUNCT_2:sch 1(A40);
now let x1,
x2 be
set ;
:: thesis: ( x1 in dom f & x2 in dom f & f . x1 = f . x2 implies x1 = x2 )assume A44:
(
x1 in dom f &
x2 in dom f &
f . x1 = f . x2 )
;
:: thesis: x1 = x2then
(
f . x1 in rng f &
f . x2 in rng f )
by FUNCT_1:12;
then
(
f . x1 in Support (Up p,T,i) &
f . x2 in Support (Up p,T,i) )
;
then reconsider x1' =
f . x1,
x2' =
f . x2 as
Element of
Bags n ;
A45:
x1' =
In x1',
(Bags n)
by FUNCT_7:def 1
.=
(In x1',(Bags n)) @
by POLYNOM2:def 3
;
x2' =
In x2',
(Bags n)
by FUNCT_7:def 1
.=
(In x2',(Bags n)) @
by POLYNOM2:def 3
;
hence x1 =
(term m) + x1'
by A43, A44
.=
x2
by A43, A44, A45
;
:: thesis: verum end; then A46:
f is
one-to-one
by FUNCT_1:def 8;
Support (Up (m *' p),T,i) c= dom f
by A11, FUNCT_2:def 1;
then
Support (Up (m *' p),T,i),
f .: (Support (Up (m *' p),T,i)) are_equipotent
by A46, CARD_1:60;
then card (f .: (Support (Up (m *' p),T,i))) =
card (Support (Up (m *' p),T,i))
by CARD_1:21
.=
i
by A2, A5, Def2
;
then
b in f .: (Support (Up (m *' p),T,i))
by A8, A35, TRIANG_1:3;
then consider bb being
set such that A47:
(
bb in dom f &
bb in Support (Up (m *' p),T,i) &
f . bb = b )
by FUNCT_1:def 12;
f . bb in rng f
by A47, FUNCT_1:12;
then
f . bb in Support (Up p,T,i)
;
then reconsider bb' =
f . bb as
Element of
Bags n ;
bb' =
In bb',
(Bags n)
by FUNCT_7:def 1
.=
(In bb',(Bags n)) @
by POLYNOM2:def 3
;
hence
contradiction
by A34, A43, A47;
:: thesis: verum end; hence
b in Support (Low p,T,i)
by A1, A32, A33, Th28;
:: thesis: verum end;
hence
( (term m) + b in Support (Low (m *' p),T,i) iff b in Support (Low p,T,i) )
by A12; :: thesis: verum