:: Diophantine sets -- Preliminaries
:: by Karol P\kak
::
:: Received March 27, 2018
:: Copyright (c) 2018-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, SUBSET_1, RELAT_1, ORDINAL4, FINSEQ_1, XBOOLE_0,
BINOP_1, FUNCT_1, FINSOP_1, XXREAL_0, TARSKI, NAT_1, INT_1, ARYTM_3,
ORDERS_1, FINSET_1, ZFMISC_1, CARD_1, PARTFUN1, ORDINAL1, RELAT_2,
ARYTM_1, FUNCOP_1, PBOOLE, CARD_3, VALUED_0, FUNCT_2, PRE_POLY, XCMPLX_0,
WELLORD2, QC_LANG1, GROUP_1, ALGSTR_0, RLVECT_1, VECTSP_1, LATTICES,
STRUCT_0, SUPINF_2, MESFUNC1, RFINSEQ, POLYNOM1, ALGSEQ_1, POLYNOM2,
HILBASIS, GRAPH_2, AFINSQ_1, HILB10_2;
notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, CARD_1, NUMBERS, RELAT_1,
XXREAL_0, XCMPLX_0, RELAT_2, FUNCT_1, PBOOLE, RELSET_1, FINSET_1,
PARTFUN1, FUNCT_2, FINSOP_1, FINSEQ_1, FUNCT_3, BINOP_1, XREAL_0,
ORDERS_1, FUNCOP_1, NAT_1, INT_1, VALUED_0, FINSEQOP, ALGSTR_0, RLVECT_1,
VFUNCT_1, VECTSP_1, GROUP_1, GROUP_4, RECDEF_1, PRE_POLY, POLYNOM1,
POLYNOM2, BAGORDER, HILBASIS, AFINSQ_1, AFINSQ_2, STRUCT_0;
constructors SETWISEO, FINSEQOP, FINSOP_1, RFUNCT_3, RECDEF_1, BINOP_2,
CLASSES1, RELSET_1, DOMAIN_1, GROUP_4, VFUNCT_1, POLYNOM2, BAGORDER,
HILBASIS, AFINSQ_2;
registrations XBOOLE_0, RELAT_1, FUNCT_1, ORDINAL1, FINSET_1, XREAL_0, NAT_1,
CARD_1, FINSEQ_1, VALUED_0, RELSET_1, FUNCT_2, INT_1, RFUNCT_2, STRUCT_0,
VECTSP_1, POLYNOM1, PRE_POLY, VFUNCT_1, MEMBERED, PRE_CIRC, POLYNOM2,
GROUP_1, FVSUM_1, AFINSQ_2, HILBASIS, BAGORDER, AFINSQ_1, NUMBERS,
NIVEN;
requirements NUMERALS, REAL, SUBSET, BOOLE, ARITHM;
definitions TARSKI, VALUED_0, RELAT_1, XBOOLE_0, FUNCT_1;
equalities STRUCT_0, ORDINAL1, FINSEQ_1, VECTSP_1, SUBSET_1;
expansions TARSKI, FUNCT_2, RELAT_2;
theorems TARSKI, ZFMISC_1, RLVECT_1, FUNCT_1, FUNCT_2, POLYNOM1, NAT_1,
FINSEQ_1, FINSEQ_3, FUNCOP_1, INT_1, RELAT_1, CARD_1, ORDINAL1, ORDERS_1,
POLYNOM2, FINSEQ_5, GROUP_1, XBOOLE_0, XBOOLE_1, RLVECT_2, XREAL_1,
XXREAL_0, PARTFUN1, NAT_D, PRE_POLY, AFINSQ_1, HILBASIS, BAGORDER,
WELLORD2, FINSEQ_4, PARTFUN2, RFINSEQ, CLASSES1, GROUP_4, FINSOP_1,
VALUED_0, AFINSQ_2, CARD_FIN, XCMPLX_1;
schemes NAT_1, FUNCT_2, FRAENKEL;
begin :: Preliminaries
reserve i,j,k,n,m for Nat,
b,b1,b2 for bag of n;
registration
let X be non empty set;
let n be Nat;
cluster n-element for XFinSequence of X;
existence
proof
reconsider N0=n --> the Element of X as XFinSequence of X;
len N0=n by FUNCOP_1:13;
then N0 is n-element by CARD_1:def 7;
hence thesis;
end;
end;
registration
let n be Nat;
cluster n-element real-valued for XFinSequence;
existence
proof
take the n-element XFinSequence of REAL;
thus thesis;
end;
end;
registration
let n,m be Nat;
let p be n-element XFinSequence;
let q be m-element XFinSequence;
cluster p^q -> (n+m) -element;
coherence
proof
len (p^q) = len p + len q & len p= n & len q = m
by AFINSQ_1:17,CARD_1:def 7;
hence thesis by CARD_1:def 7;
end;
end;
registration
let p be real-valued XFinSequence;
let q be real-valued XFinSequence;
cluster p^q -> real-valued;
coherence;
end;
definition
let n be Nat;
let p be n-element real-valued XFinSequence;
func @p -> Function of n,F_Real equals
p;
coherence
proof
A1: len p=n by CARD_1:def 7;
rng p c= REAL;
hence thesis by A1,FUNCT_2:2;
end;
end;
definition
let n be Nat;
let X be non empty set;
let p be Function of n,X;
func @p -> n-element XFinSequence of X equals
p;
coherence
proof
dom p = n & rng p c= X by FUNCT_2:def 1;
then reconsider P=p as XFinSequence by AFINSQ_1:5;
reconsider P as XFinSequence of X;
len P = n by FUNCT_2:def 1;
hence thesis by CARD_1:def 7;
end;
end;
registration
let X be set, p be Permutation of X, M be ManySortedSet of X;
cluster M * p -> total;
coherence
proof
dom p = X & rng p = X & dom M = X by FUNCT_2:def 3,PARTFUN1:def 2;
then dom (M*p) = X by RELAT_1:27;
hence thesis by PARTFUN1:def 2;
end;
end;
registration
let F be finite-support Function;
let f be one-to-one Function;
cluster F*f -> finite-support;
coherence
proof
support (F*f) c= f".:support (F)
proof
let y be object;
A1: rng f = dom (f") by FUNCT_1:33;
assume y in support (F*f);
then
A2: (F*f).y <>0 by PRE_POLY:def 7;
then y in dom (F*f) by FUNCT_1:def 2;
then (F*f).y = F.(f.y) & y in dom f & f.y in dom F by FUNCT_1:11,12;
then (f").(f.y)=y & f.y in support F & f.y in rng f
by A2,PRE_POLY:def 7,FUNCT_1:34,def 3;
hence thesis by A1,FUNCT_1:def 6;
end;
hence thesis by PRE_POLY:def 8;
end;
end;
theorem Th1:
for F, G being XFinSequence st F^G is one-to-one holds
rng F misses rng G
proof
let F, G be XFinSequence such that
A1: F^G is one-to-one;
assume rng F meets rng G;
then consider y be object such that
A2: y in rng F & y in rng G by XBOOLE_0:3;
consider n1 be object such that
A3: n1 in dom F & F.n1 = y by A2,FUNCT_1:def 3;
consider n2 be object such that
A4: n2 in dom G & G.n2 = y by A2,FUNCT_1:def 3;
reconsider n1,n2 as Nat by A3,A4;
A5: (F^G).n1 = F.n1 & (F^G).(len F+n2) = G.n2 by A3,A4,AFINSQ_1:def 3;
dom F c= dom (F^G) by AFINSQ_1:21;then
n1 in dom (F^G) & (len F+n2) in dom (F^G) by A3,A4,AFINSQ_1:23;
then n1 = n2+len F & n1 < len F by A5,A1,FUNCT_1:def 4,A3,A4,AFINSQ_1:86;
hence thesis by NAT_1:11;
end;
theorem Th2:
for X being set, f being X-defined Function,
perm being Permutation of X holds
card support (f*perm) = card support (f)
proof
let X be set,
f be X-defined Function,
perm be Permutation of X;
set P=perm";
A1:dom perm=X=rng perm & dom P=X=rng P by FUNCT_2:52,def 3;
support (f) c= dom f c= X = dom P by FUNCT_2:52,PRE_POLY:37;
then
A2: support (f) c= dom P;
A3:P.:support (f) c= support (f*perm)
proof
let y be object;assume y in P.:support (f);
then consider x be object such that
A4:x in dom P & x in support f & P.x=y by FUNCT_1:def 6;
A5:x = perm.y by A1,A4,FUNCT_1:32;
A6:f.x <>0 by A4,PRE_POLY:def 7;
then x in dom f & y in dom perm by A4,A1,FUNCT_1:def 2,def 3;
then perm.y in dom f & f.(perm.y) = (f*perm).y
by A1,A4,FUNCT_1:32,FUNCT_1:13;
hence thesis by A6,A5,PRE_POLY:def 7;
end;
support (f*perm) c= P.:support (f)
proof
let y be object;assume y in support (f*perm);
then A7:(f*perm).y <>0 by PRE_POLY:def 7;
then y in dom (f*perm) by FUNCT_1:def 2;
then f.(perm.y) = (f*perm).y & y in dom perm & perm.y in dom f
by FUNCT_1:11,12;
then perm.y in dom P & perm.y in support (f) & P.(perm.y)=y
by A1,A7,FUNCT_1:32,PRE_POLY:def 7;
hence thesis by FUNCT_1:def 6;
end;
then support (f*perm) = P.:support (f) by A3,XBOOLE_0:def 10;
hence thesis by CARD_1:5,A2,CARD_1:33;
end;
registration
let X be set;
cluster 0_(X, F_Real) -> natural-valued;
coherence
proof
let x be object;
assume x in dom 0_(X, F_Real);
then 0_(X, F_Real).x = 0.F_Real by POLYNOM1:22
.= 0;
hence thesis;
end;
cluster 1_(X, F_Real) -> natural-valued;
coherence
proof
let x be object;
assume
A1: x in dom 1_(X, F_Real);
x=EmptyBag X or x<>EmptyBag X;
then 1_(X, F_Real).x = 1.F_Real or 1_(X, F_Real).x = 0.F_Real
by A1,POLYNOM1:25;
hence thesis;
end;
end;
registration
let X be set;
let x be Element of X;
cluster 1_1(x,F_Real) -> natural-valued;
coherence
proof
let a be object;
assume
A1: a in dom (1_1(x, F_Real));
a=UnitBag x or a<>UnitBag x;
then 1_1(x, F_Real).a = 1_F_Real or 1_1(x, F_Real).a = 0.F_Real
by A1,HILBASIS:12;
hence thesis;
end;
end;
registration
let X be set;
cluster INT -valued for Series of X,F_Real;
existence
proof
set x=the Element of X;
1_1(x,F_Real) is INT -valued;
hence thesis;
end;
end;
registration
let O be Ordinal;
cluster INT -valued for Polynomial of O,F_Real;
existence
proof
set x=the Element of O;
1_1(x,F_Real) is INT -valued;
hence thesis;
end;
end;
registration
let X be set, p be INT -valued Series of X, F_Real;
cluster -p -> INT -valued;
coherence
proof
thus rng (-p) c= INT
proof
let y be object such that
A1: y in rng (-p);
consider x be object such that
A2: x in dom (-p) & (-p).x=y by A1,FUNCT_1:def 3;
reconsider x as bag of X by A2;
(-p).x = -(p.x) by POLYNOM1:17;
hence thesis by A2,INT_1:def 2;
end;
end;
let q be INT -valued Series of X, F_Real;
cluster p+q ->INT -valued;
coherence
proof
thus rng (p+q) c= INT
proof
let y be object such that
A3: y in rng (p+q);
consider x be object such that
A4: x in dom (p+q) & (p+q).x=y by A3,FUNCT_1:def 3;
reconsider x as bag of X by A4;
(p+q).x = (p.x)+(q.x) by POLYNOM1:15;
hence thesis by A4,INT_1:def 2;
end;
end;
cluster p-q ->INT -valued;
coherence
proof
thus rng (p-q) c= INT
proof
let y be object such that
A5: y in rng (p-q);
consider x be object such that
A6: x in dom (p-q) & (p-q).x=y by A5,FUNCT_1:def 3;
reconsider x as bag of X by A6;
p-q = p+-q by POLYNOM1:def 7;
then (p-q).x = (p.x)+((-q).x) by POLYNOM1:15
.= (p.x)+-(q.x) by POLYNOM1:17;
hence thesis by A6,INT_1:def 2;
end;
end;
end;
registration
let X be Ordinal, p,q be INT -valued Series of X, F_Real;
cluster p *' q ->INT -valued;
coherence
proof
thus rng (p*'q) c= INT
proof
let y be object such that
A1: y in rng (p*'q);
consider x be object such that
A2: x in dom (p*'q) & (p*'q).x=y by A1,FUNCT_1:def 3;
reconsider x as bag of X by A2;
consider s be FinSequence of F_Real such that
A3: (p*'q).x = Sum s & len s = len decomp x and
A4: for k be Element of NAT st k in dom s ex b1, b2 be bag of X st
(decomp x)/.k = <*b1, b2*> & s/.k = p.b1*q.b2 by POLYNOM1:def 10;
consider f be sequence of F_Real such that
A5: Sum s = f . (len s) & f . 0 = 0. F_Real and
A6: for j be Nat for v be Element of F_Real st
j < len s & v = s . (j + 1) holds
f . (j + 1) = (f . j) + v by RLVECT_1:def 12;
defpred P[Nat] means $1 <= len s implies f.$1 is integer;
A7: P[0] by A5;
A8: P[n] implies P[n+1]
proof
assume
A9: P[n];set n1=n+1;
assume
A10: n1 <= len s;
A11: n1 in dom s by A10,FINSEQ_3:25,NAT_1:11;
then consider b1, b2 be bag of X such that
A12: (decomp x)/.n1 = <*b1, b2*> &
s/.n1 = p.b1*q.b2 by A4;
A13: s/.n1 = s.n1 by A11,PARTFUN1:def 6;
f.n is integer & f . n1 = (f . n) + s/.n1 by A9,A6,A13,A10,NAT_1:13;
hence thesis by A12;
end;
P[n] from NAT_1:sch 2(A7,A8);
then Sum s is integer by A5;
hence thesis by A3,A2,INT_1:def 2;
end;
end;
end;
registration
let X be set;
cluster natural-valued for Function of X, F_Real;
existence
proof
set A = the Function of X,NAT;
A1: rng A c= REAL & dom A = X by VALUED_0:def 3,FUNCT_2:def 1;
reconsider A as Function of X, F_Real by A1,FUNCT_2:2;
A is natural-valued;
hence thesis;
end;
end;
registration
let O be Ordinal;
cluster INT -valued for Function of O, F_Real;
existence
proof
the natural-valued Function of O, F_Real is INT -valued;
hence thesis;
end;
end;
registration
let O be Ordinal;
let b be bag of O;
let x be INT -valued Function of O, F_Real;
cluster eval(b,x) -> integer;
coherence
proof
reconsider FR=F_Real as well-unital non trivial doubleLoopStr;
reconsider X=x as Function of O, FR;
set S = SgmX(RelIncl O, support b);
consider y be FinSequence of the carrier of FR such that
A1: len y = len S & eval(b,X) = Product y and
A2: for i be Element of NAT st 1 <= i & i <= len y holds
y/.i = power(FR).((X * S)/.i,(b * S)/.i) by POLYNOM2:def 2;
reconsider Y=y as FinSequence of the carrier of F_Real;
A3: dom y = dom S by A1,FINSEQ_3:29;
defpred P[Nat] means $1 <= len y implies Product (Y|$1) is integer;
A4: P[0]
proof
(Y|0) = <*> the carrier of F_Real;
then Product (Y|0) = 1_ F_Real by GROUP_4:8;
hence thesis;
end;
A5: Y|(len y) = Y by FINSEQ_1:58;
A6: P[n] implies P[n+1]
proof
assume
A7: P[n];set n1=n+1;
assume
A8: n1<= len y;
then
A9: n1 in dom y by FINSEQ_3:25,NAT_1:11;
then
A10: Y.n1 = Y/.n1 by PARTFUN1:def 6;
Y|n1 = (Y|n)^<*Y.n1*> by A8,NAT_1:13,FINSEQ_5:83;
then
A11: Product (Y|n1) = Product (Y|n) * (Y/.n1) by A10,GROUP_4:6;
reconsider A = x*S as INT -valued FinSequence of the carrier of F_Real;
set I = A/.n1;
RelIncl O linearly_orders support b by PRE_POLY:82;
then
A12: rng S = support b by PRE_POLY:def 2;
dom X = O by FUNCT_2:def 1;
then dom (X * S) = dom S by A12,RELAT_1:27;
then
A13: (X * S)/.n1 = (X*S).n1 = I by A3,A9,PARTFUN1:def 6;
then
A14: y/.n1 = power(F_Real).(I,(b * S)/.n1) by A8,NAT_1:11,A2;
reconsider I as Element of F_Real by A13;
defpred R[Nat] means power(F_Real).(I,$1) is integer;
(power F_Real).(I,0) = 1_ F_Real by GROUP_1:def 7;
then
A15: R[0];
A16: R[k] implies R[k+1]
proof
(power F_Real).(I,k+1) = power(F_Real).(I,k)*I by GROUP_1:def 7;
hence thesis;
end;
R[k] from NAT_1:sch 2(A15,A16);
then y/.n1 is integer by A14;
hence thesis by A11,A8,NAT_1:13,A7;
end;
P[n] from NAT_1:sch 2(A4,A6);
hence thesis by A5,A1;
end;
end;
registration
let O be Ordinal;
let p be INT -valued Polynomial of O,F_Real;
let x be INT -valued Function of O, F_Real;
cluster eval(p,x) -> integer;
coherence
proof
reconsider FR=F_Real as right_zeroed add-associative right_complementable
well-unital distributive non trivial non empty doubleLoopStr;
reconsider X= x as Function of O, FR;
reconsider P=p as Polynomial of O,FR;
set S=SgmX(BagOrder O, Support P);
consider y be FinSequence of the carrier of F_Real such that
A1: len y = len S & eval(p,x) = Sum y and
A2: for i being Element of NAT st 1 <= i & i <= len y holds
y/.i = (P * S)/.i * eval(S/.i,X) by POLYNOM2:def 4;
consider f be sequence of F_Real such that
A3:Sum y = f . (len y) & f . 0 = 0. F_Real and
A4: for j be Nat for v be Element of F_Real st
j < len y & v = y . (j + 1) holds
f . (j + 1) = (f . j) + v by RLVECT_1:def 12;
defpred P[Nat] means $1 <=len y implies f.$1 is integer;
A5: P[0] by A3;
A6: P[n] implies P[n+1]
proof
assume
A7: P[n];
set n1=n+1;
assume
A8: n1 <= len y;
A9: dom y = dom S by A1,FINSEQ_3:29;
reconsider A = p*S as INT -valued FinSequence of the carrier of F_Real;
set I=A/.n1;
BagOrder O linearly_orders Support P by POLYNOM2:18;
then
A10: rng S = Support P by PRE_POLY:def 2;
dom p = Bags O by FUNCT_2:def 1;
then
A11: dom (P * S) = dom S by A10,RELAT_1:27;
A12: n1 in dom y by A8,NAT_1:11,FINSEQ_3:25;
then
A13: A/.n1 = (p*S).n1 = (P * S)/.n1 by A11,A9,PARTFUN1:def 6;
then reconsider PP = A/.n1 as Element of F_Real;
A14: y/.n1 =PP * (eval(S/.n1,x)) by A13,A2,A8,NAT_1:11;
y.n1 = y/.n1 by A12,PARTFUN1:def 6;
then f . n1 = (f.n) + y/.n1 by A4,A8,NAT_1:13;
hence thesis by A14,A7,A8,NAT_1:13;
end;
P[n] from NAT_1:sch 2(A5,A6);
hence thesis by A1,A3;
end;
end;
begin :: Polynomial extended by 0
theorem Th3:
for b being ManySortedSet of n st k <= n holds (0,k)-cut b = b|k
proof
let b be ManySortedSet of n;
assume k <=n;
then
A1: Segm k c= Segm n by NAT_1:39;
A2: dom (b|k)=k by A1,PARTFUN1:def 2;
A3: dom ((0,k)-cut b) = k-'0 & k-'0 =k by NAT_D:40,PARTFUN1:def 2;
for x be object st x in k holds ((0,k)-cut b).x = (b|k).x
proof
let x be object;
assume
A4: x in k;
then x in Segm k;
then reconsider n=x as Element of NAT;
thus ((0,k)-cut b).x = b.(0+n) by A4,A3,BAGORDER:def 1
.= (b|k).x by A4,FUNCT_1:49;
end;
hence thesis by FUNCT_1:2,A2,A3;
end;
theorem Th4:
for b being bag of (n+1) holds
b = (0,n)-cut b bag_extend (b.n)
proof
let b be bag of (n+1);
set C=(0,n)-cut b, B= C bag_extend (b.n);
A1: n-'0 = n by NAT_D:40;
then
A2: B|n = C & B.n = b.n by HILBASIS:def 1;
A3: C=b|n by Th3,NAT_1:11;
A4:dom b = n+1 = dom B by A1,PARTFUN1:def 2;
for x be object st x in n+1 holds B.x = b.x
proof
let x be object;
assume x in n+1;
then x in Segm (n+1);
then x in (Segm n)\/{n} by AFINSQ_1:2;
then x in n or x=n by ZFMISC_1:136;
then B.x = C.x = b.x or B.x = b.x by FUNCT_1:49,A2,A3;
hence thesis;
end;
hence thesis by FUNCT_1:2,A4;
end;
theorem Th5:
(0,n)-cut (b bag_extend k) = b
proof
thus (0,n)-cut (b bag_extend k) = (b bag_extend k)|n by Th3,NAT_1:11
.= b by HILBASIS:def 1;
end;
definition
let n;
let L be non empty ZeroStr;
let p be Series of n,L;
func p extended_by_0 -> Series of n+1,L means :Def3:
for b being bag of n+1 holds
(b.n <>0 implies it.b = 0.L) &
(b.n = 0 implies it.b = p.(0,n)-cut b);
existence
proof
defpred P[Element of Bags (n+1), Element of L] means
($1.n <>0 implies $2=0.L) &
($1.n = 0 implies $2 = p.(0,n)-cut $1);
A1: for x being Element of Bags (n+1) ex y being Element of L st P[x,y]
proof
let x be Element of Bags (n+1);
n= n-'0 by NAT_D:40;
then (0,n)-cut x in Bags n by PRE_POLY:def 12;
then
A2: (0,n)-cut x in dom p by PARTFUN1:def 2;
per cases;
suppose
A3: x.n<>0;
take 0.L;
thus thesis by A3;
end;
suppose
A4: x.n = 0;
take p/.(0,n)-cut x;
thus thesis by A4,A2,PARTFUN1:def 6;
end;
end;
consider f be Function of Bags (n+1),L such that
A5: for x be Element of Bags (n+1) holds P[x,f.x] from FUNCT_2:sch 3(A1);
take f;
let b be bag of n+1;
b is Element of Bags (n+1) by PRE_POLY:def 12;
hence thesis by A5;
end;
uniqueness
proof
let e1,e2 be Series of n+1,L such that
A6: for b be bag of n+1 holds
(b.n <>0 implies e1.b = 0.L)& (b.n = 0 implies e1.b = p.(0,n)-cut b)and
A7: for b be bag of n+1 holds
(b.n <>0 implies e2.b = 0.L)& (b.n = 0 implies e2.b = p.(0,n)-cut b);
now let b be Element of Bags(n+1);
b.n = 0 or b.n<>0;
then e1.b=0.L=e2.b or e1.b=p.(0,n)-cut b=e2.b by A6,A7;
hence e1.b=e2.b;
end;
hence thesis;
end;
end;
theorem Th6:
for L being non empty ZeroStr, p being Series of n,L holds
(p extended_by_0).(b bag_extend 0) = p.b
proof
let L be non empty ZeroStr;
let p be Series of n,L;
(b bag_extend 0).n = 0 by HILBASIS:def 1;
hence (p extended_by_0).(b bag_extend 0) = p.(0,n)-cut (b bag_extend 0)
by Def3
.= p.b by Th5;
end;
theorem Th7:
for L being non empty ZeroStr, p being Series of n,L,
b being bag of n+1 st b in Support (p extended_by_0)
holds b.n = 0
proof
let L be non empty ZeroStr,p be Series of n,L, b be bag of n+1;
assume b in Support (p extended_by_0);
then (p extended_by_0).b <>0.L by POLYNOM1:def 3;
hence thesis by Def3;
end;
theorem Th8:
for L being non empty ZeroStr, p being Series of n,L holds
b bag_extend 0 in Support (p extended_by_0) iff
b in Support p
proof
let L be non empty ZeroStr,
p be Series of n,L;
set B= b bag_extend 0,P=p extended_by_0;
B.n=0 by HILBASIS:def 1;
then
A1: P.B = p.(0,n)-cut B by Def3
.= p.b by Th5;
thus B in Support P implies b in Support p
proof
assume B in Support P;
then p.b<>0.L & b in Bags n & dom p = Bags n
by POLYNOM1:def 3,A1,FUNCT_2:def 1,PRE_POLY:def 12;
hence thesis by POLYNOM1:def 3;
end;
assume b in Support p;
then
A2: p.b <> 0.L by POLYNOM1:def 3;
B in Bags (n+1) & dom P = Bags (n+1) by FUNCT_2:def 1;
hence thesis by POLYNOM1:def 3,A2,A1;
end;
theorem Th9:
for L being non empty ZeroStr,
p being Series of n,L, b being bag of n+1 st b.n = 0 holds
b in Support (p extended_by_0) iff (0,n)-cut b in Support p
proof
let L be non empty ZeroStr,
p be Series of n,L, b be bag of n+1;
assume
A1: b.n = 0;
A2: n-'0 = n by NAT_D:40;
b = ((0,n)-cut b) bag_extend 0 by A1,Th4;
hence thesis by Th8,A2;
end;
registration
let n;
let L be non empty ZeroStr;
let p be Polynomial of n,L;
cluster p extended_by_0 -> finite-Support;
coherence
proof
deffunc F(bag of n)= $1 bag_extend 0;
A1:(Support p) is finite by POLYNOM1:def 5;
set FS={F(w) where w is Element of Bags(n):w in Support p};
A2: FS is finite from FRAENKEL:sch 21(A1);
set P=p extended_by_0;
Support P c= FS
proof
let x be object;
assume
A3: x in Support P;
then reconsider b=x as bag of (n+1);
A4: n-'0=n by NAT_D:40;
then reconsider B=(0,n)-cut b as bag of n;
A5: b.n =0 by A3,Th7;
then B in Support p by A3,Th9;
then F(B) in FS;
hence thesis by A4,A5,Th4;
end;
hence thesis by A2,POLYNOM1:def 5;
end;
end;
theorem Th10:
for L being non empty ZeroStr,
p being Series of n,L holds
{0.L} \/ rng p = rng (p extended_by_0)
proof
let L be non empty ZeroStr,
p be Series of n,L;
A1:dom p = Bags n & dom (p extended_by_0) = Bags (n+1) by FUNCT_2:def 1;
A2:rng p c= rng (p extended_by_0)
proof
let y be object;
assume y in rng p;
then consider x be object such that
A3: x in dom p & p.x=y by FUNCT_1:def 3;
reconsider x as Element of Bags n by A3;
(p extended_by_0).(x bag_extend 0) = p.x by Th6;
hence thesis by A1,FUNCT_1:def 3,A3;
end;
set b0= (the bag of n) bag_extend 1;
b0.n = 1 by HILBASIS:def 1;
then
A4: (p extended_by_0).b0 =0.L by Def3;
0.L in rng (p extended_by_0) by A1,A4,FUNCT_1:def 3;
hence {0.L} \/rng p c= rng (p extended_by_0) by A2,ZFMISC_1:137;
let y be object;
assume y in rng (p extended_by_0);
then consider x be object such that
A5:x in dom (p extended_by_0) & (p extended_by_0).x=y by FUNCT_1:def 3;
reconsider x as Element of Bags (n+1) by A5;
per cases;
suppose x.n<>0;
then y = 0.L by A5,Def3;
hence thesis by ZFMISC_1:136;
end;
suppose x.n = 0; then
A6: y = p.(0,n)-cut x by Def3,A5;
n-'0=n by NAT_D:40;
then ((0,n)-cut x) in Bags n by PRE_POLY:def 12;
then p.(0,n)-cut x in rng p by A1,FUNCT_1:def 3;
hence thesis by A6,ZFMISC_1:136;
end;
end;
theorem Th11:
support b = support (b bag_extend 0)
proof
set E = b bag_extend 0;
A1: b = E|n by HILBASIS:def 1;
thus support b c= support E
proof
let x be object;
assume x in support b;
then
A2: b.x <>0 by PRE_POLY:def 7;
then x in dom b by FUNCT_1:def 2;
then E.x = b.x by A1,FUNCT_1:49;
hence thesis by A2,PRE_POLY:def 7;
end;
let x be object;
assume x in support E;
then
A3:E.x <>0 by PRE_POLY:def 7;
then
A4:x <> n & x in dom E by HILBASIS:def 1,FUNCT_1:def 2;
dom E=Segm(n+1) by PARTFUN1:def 2;
then x in (Segm n)\/{n} by A4,AFINSQ_1:2;
then E.x = b.x by A1,FUNCT_1:49,A4,ZFMISC_1:136;
hence thesis by A3,PRE_POLY:def 7;
end;
theorem Th12:
SgmX(RelIncl n, support b) =
SgmX(RelIncl (n+1), support (b bag_extend 0))
proof
set S1=SgmX(RelIncl n, support b);
set B=b bag_extend 0;
set S2 = SgmX(RelIncl (n+1), support B);
A1:RelIncl n linearly_orders support b by PRE_POLY:82;
A2:RelIncl (n+1) linearly_orders support B by PRE_POLY:82;
A3:rng S1 = support b & rng S2 = support B by A1,A2,PRE_POLY:def 2;
A4: support b = support B by Th11;
then reconsider s2=S2 as FinSequence of n by A3,FINSEQ_1:def 4;
reconsider R1=RelIncl (n+1) as Order of (n+1);
for n1,m1 be Nat
st n1 in dom s2 & m1 in dom s2 & n1 < m1 holds
s2/.n1 <> s2/.m1 & [s2/.n1,s2/.m1] in RelIncl n
proof
let n1,m1 be Nat such that
A5: n1 in dom s2 & m1 in dom s2 & n1 < m1;
[S2/.n1,S2/.m1] in RelIncl (n+1) by A5,A2,PRE_POLY:def 2;
then
A6: S2/.n1 c= S2/.m1 by WELLORD2:def 1;
A7: S2/.n1 = S2.n1 = s2/.n1 by A5,PARTFUN1:def 6;
A8: S2/.m1 = S2.m1 = s2/.m1 by A5,PARTFUN1:def 6;
s2.n1 in rng S2 & s2.m1 in rng S2 by A5,FUNCT_1:def 3;
hence thesis by A5,A2,PRE_POLY:def 2,A6,A7,A8,A3,A4, WELLORD2:def 1;
end;
hence thesis by A3,A4,A1,PRE_POLY:def 2;
end;
theorem Th13:
for L being well-unital non trivial doubleLoopStr
for x being Function of n, L, y be Function of n+1,L st y|n = x
holds
eval(b,x) = eval(b bag_extend 0,y)
proof
let L be well-unital non trivial doubleLoopStr;
let x be Function of n, L, y be Function of n+1,L such that
A1: y|n = x;
set S=SgmX(RelIncl n, support b);
set B=b bag_extend 0;
set S1=SgmX(RelIncl (n+1), support B);
consider P be FinSequence of L such that
A2: len P = len S & eval(b,x) = Product P and
A3: for i be Element of NAT st
1 <= i & i <= len P holds
P/.i = power(L).((x * S)/.i,(b * S)/.i) by POLYNOM2:def 2;
consider P1 be FinSequence of L such that
A4: len P1 = len S1 & eval(B,y) = Product P1 and
A5: for i be Element of NAT st
1 <= i & i <= len P1 holds
P1/.i = power(L).((y * S1)/.i,(B * S1)/.i) by POLYNOM2:def 2;
A6:S=S1 by Th12;
A7: rng S c= n;
A8:y*S = y*((id n)*S) by A7,RELAT_1:53
.= y*(id n)*S by RELAT_1:36
.= x*S by RELAT_1:65,A1;
A9:b=(0,n)-cut B by Th5
.= B|n by NAT_1:11,Th3;
A10:B*S = B*((id n)*S) by A7,RELAT_1:53
.= B*(id n)*S by RELAT_1:36
.=b*S by A9,RELAT_1:65;
for i be Nat st 1<= i <= len P holds P.i=P1.i
proof
let i be Nat such that
A11: 1<=i <= len P;
reconsider I=i as Element of NAT by ORDINAL1:def 12;
A12:i in dom P & i in dom P1 by A2,A4,A6,A11,FINSEQ_3:25;
then P/.I = P.i by PARTFUN1:def 6;
hence P.i = power(L).((y * S1)/.i,(B * S1)/.i) by A3,A11,A6,A8,A10
.= P1/.I by A5,A11,A2,A4,A6
.= P1.i by A12,PARTFUN1:def 6;
end;
hence thesis by A2,A4,A6,FINSEQ_1:14;
end;
theorem Th14:
b1 < b2 iff b1 bag_extend k < b2 bag_extend k
proof
set B1=b1 bag_extend k,B2=b2 bag_extend k;
A1:B1|n=b1 & B2|n=b2 & B1.n=k=B2.n by HILBASIS:def 1;
A2:dom b2 = n =dom b1 by PARTFUN1:def 2;
thus b1 < b2 implies b1 bag_extend k < b2 bag_extend k
proof
assume b1<b2;
then consider o be Ordinal such that
A3: b1.o < b2.o and
A4: for l be Ordinal st l in o holds b1.l = b2.l by PRE_POLY:def 9;
A5: o in dom b2 by A3,FUNCT_1:def 2;
then
A6: B2.o = b2.o & B1.o = b1.o by A1,FUNCT_1:47,A2;
for l be Ordinal st l in o holds B1.l = B2.l
proof
let l be Ordinal;assume
A7: l in o;
then B2.l = b2.l & B1.l = b1.l by A1,FUNCT_1:47,A2,A5,ORDINAL1:10;
hence thesis by A7,A4;
end;
hence thesis by A3,A6,PRE_POLY:def 9;
end;
assume B1 < B2;
then consider o be Ordinal such that
A8:B1.o < B2.o and
A9:for l be Ordinal st l in o holds B1.l = B2.l by PRE_POLY:def 9;
o in dom B2 by A8,FUNCT_1:def 2;
then o in Segm (n+1);
then o in (Segm n)\/{n} by AFINSQ_1:2;
then
A10: o in n or o=n by ZFMISC_1:136;
then
A11:B2.o = b2.o & B1.o = b1.o by A1,A8,FUNCT_1:47,A2;
for l be Ordinal st l in o holds b1.l = b2.l
proof
let l be Ordinal;
assume
A12: l in o;
then B2.l = b2.l & B1.l = b1.l by A2,A10,A1,FUNCT_1:47,ORDINAL1:10;
hence thesis by A12,A9;
end;
hence thesis by A8,A11,PRE_POLY:def 9;
end;
theorem
for X being non empty set,
A being finite Subset of X,
R being Order of X st R linearly_orders A
for i,k st 1 <= i <= k <= card A holds
SgmX(R, rng (SgmX(R,A)|k))/.i = SgmX(R,A)/.i
proof
let X be non empty set,
A be finite Subset of X,
R be Order of X;
assume
A1:R linearly_orders A;
set Sp = SgmX(R,A);
A2: card A = len Sp by A1,PRE_POLY:11;
A3: rng Sp =A by A1,PRE_POLY:def 2;
defpred P[Nat] means
for i st 1 <= i <= $1 <= card A holds
SgmX(R, rng (Sp|$1))/.i = Sp/.i;
A4: P[0];
A5: for k st P[k] holds P[k+1]
proof
let k be Nat;set k1=k+1;
assume
A6: P[k];
let i be Nat such that
A7: 1<= i <= k1 <= card A;
A8: Sp is one-to-one by A1,PRE_POLY:10;
set Spk1=Sp|k1;
A9: k < card A by A7,NAT_1:13;then
A10: len Spk1= k1 & len (Sp|k)= k by A7,A2,FINSEQ_1:59;
A11: k < len Sp by A7,A2,NAT_1:13;
A12: Spk1 = (Sp|k) ^ <*Sp.k1*> by A7,A2,NAT_1:13,FINSEQ_5:83;
A13: R linearly_orders rng (Sp|k1) by A3,RELAT_1:70,A1,ORDERS_1:38;
A14: 1<= k1 by NAT_1:11;
A15: k1 in dom Sp by NAT_1:11,A7,A2,FINSEQ_3:25; then
A16: Sp.k1 in rng Sp by FUNCT_1:def 3;
A17: Sp.k1 = Sp/.k1 by A15,PARTFUN1:def 6;
A18: k1 in Seg k1 by A14;
A19: Sp/.k1 in rng Spk1 by A15,A18,PARTFUN2:18;
A20: for y be Element of X st y in rng (Sp|k1) holds [y,Sp/.k1] in R
proof
let y be Element of X such that
A21: y in rng Spk1;
consider w be object such that
A22: w in dom Spk1 & Spk1.w = y by A21,FUNCT_1:def 3;
reconsider w as Nat by A22;
A23: 1<= w <= k1 by A22,A10,FINSEQ_3:25;
then
A24: Spk1.w = Sp.w by FINSEQ_3:112;
w <= len Sp by A7,A2,A23,XXREAL_0:2;
then
A25: w in dom Sp by A23,FINSEQ_3:25;
then
A26: Sp/.w = Sp.w by PARTFUN1:def 6;
per cases by A23,XXREAL_0:1;
suppose
A27: w=k1;
R is_reflexive_in A by A1,ORDERS_1:def 9;
hence [y,Sp/.k1] in R by A27,A17,A24,A22,A3,A16;
end;
suppose w <k1;
hence [y,Sp/.k1] in R by A22,A24,A26,A25,A15,A1,PRE_POLY:def 2;
end;
end;
A28:len SgmX(R, rng (Sp|k1)) = card rng (Sp|k1) by A13,PRE_POLY:11
.= k1 by A10,A8,FINSEQ_4:62;
A29:not Sp/.k1 in rng (Sp|k)
proof
assume Sp/.k1 in rng (Sp|k);
then consider w be object such that
A30: w in dom (Sp|k) & (Sp|k).w = Sp/.k1 by FUNCT_1:def 3;
reconsider w as Nat by A30;
A31: 1<= w <= k by A30,A10,FINSEQ_3:25;
w <= len Sp by A9,A2,A31,XXREAL_0:2;
then
A32: w in dom Sp by A31,FINSEQ_3:25;
Sp.w = Sp.k1 by A30,A31,FINSEQ_3:112,A17;
then w=k1 by A8,A15,A32,FUNCT_1:def 4;
hence thesis by A31,NAT_1:13;
end;
rng Spk1 = rng (Sp|k) \/ rng <*Sp.k1*> by A12,FINSEQ_1:31
.= rng (Sp|k) \/ {Sp.k1} by FINSEQ_1:38;
then
A33: rng (Sp|k1) = {Sp/.k1} \/ rng (Sp|k) by A15,PARTFUN1:def 6;
A34: k1 in dom SgmX(R, rng (Sp|k1)) by A14,A28,FINSEQ_3:25;
SgmX(R, rng (Sp|k1))/.k1 = Sp/.k1 by A28,A20,A19,A13,PRE_POLY:21;
then
A35:for i being Element of NAT st 1 <= i & i <= k1-1
holds SgmX(R,rng (Sp|k))/.i = SgmX(R,rng (Sp|k1))/.i
by A13,A29,A33,A34,PRE_POLY:78;
A36: i in NAT by ORDINAL1:def 12;
per cases by A7,XXREAL_0:1;
suppose i <k1;
then
A37: i <=k by NAT_1:13;
hence SgmX(R,rng (Sp|k1))/.i = SgmX(R,rng (Sp|k))/.i by A36,A7,A35
.= Sp/.i by A11,A6,A37,A7,A2;
end;
suppose i=k1;
hence thesis by A20,A28,A19,A13,PRE_POLY:21;
end;
end;
for k holds P[k] from NAT_1:sch 2(A4,A5);
hence thesis;
end;
theorem Th16:
for O being Ordinal,
A being finite Subset of Bags O st
n in dom SgmX(BagOrder O, A) & m in dom SgmX(BagOrder O, A) & n < m
holds SgmX(BagOrder O, A)/.n < SgmX(BagOrder O, A)/.m
proof
let O be Ordinal,A be finite Subset of Bags O;
set S=SgmX(BagOrder O, A);
assume
A1: n in dom S & m in dom S & n < m;
BagOrder O linearly_orders field BagOrder O by ORDERS_1:37;
then BagOrder O linearly_orders Bags O by ORDERS_1:12;
then BagOrder O linearly_orders A by ORDERS_1:38;
then A2: S/.n <> S/.m & [S/.n,S/.m] in BagOrder O by PRE_POLY:def 2,A1;
then S/.n <=' S/.m by PRE_POLY:def 14;
hence thesis by A2,PRE_POLY:def 10;
end;
theorem Th17:
for L being right_zeroed add-associative right_complementable
well-unital distributive non trivial doubleLoopStr
for p being Polynomial of n,L
holds
len SgmX(BagOrder n, Support p) =
len SgmX(BagOrder (n+1), Support (p extended_by_0)) &
for i be Nat st 1<=i<= len SgmX(BagOrder n, Support p) holds
SgmX(BagOrder (n+1), Support (p extended_by_0))/.i =
SgmX(BagOrder n, Support p)/.i bag_extend 0
proof
let L be right_zeroed add-associative right_complementable
well-unital distributive non trivial doubleLoopStr;
let p be Polynomial of n,L;
set B=BagOrder n,B1=BagOrder (n+1);
set P=p extended_by_0;
A1:n-'0=n by NAT_D:40;
A2:B linearly_orders Support p & B1 linearly_orders Support P by POLYNOM2:18;
deffunc F(bag of n) = $1 bag_extend 0;
A3: for x being Element of Bags n holds F(x) in Bags(n+1);
consider f be Function of Bags n,Bags (n+1) such that
A4: for x being Element of Bags n holds f.x = F(x) from FUNCT_2:sch 8(A3);
set F=f|(Support p);
A5:dom F = Support p by FUNCT_2:def 1;
set Sp=SgmX(B, Support p),SP=SgmX(B1, Support P);
A6: rng F c= Support P
proof
let y be object;
assume y in rng F;
then consider x be object such that
A7: x in dom F & F.x=y by FUNCT_1:def 3;
reconsider x as Element of Bags n by A7,A5;
A8: f.x =F.x by A7,FUNCT_1:47;
f.x = F(x) by A4;
hence thesis by A7,A8,Th8;
end;
Support P c= rng F
proof
let y be object;
assume
A9:y in Support P;
then reconsider b=y as bag of n+1;
set C=(0,n)-cut b;
A10: b.n=0 by A9,Th7;
then
A11: C in Support p by A9,Th9;
then reconsider C as Element of Bags n;
F(C)=f.C = F.C by A11,A4,FUNCT_1:49;
then
A12: F(C) in rng F by A11,A5,FUNCT_1:def 3;
n-'0=n by NAT_D:40;
hence thesis by A12,A10,Th4;
end;
then
A13: Support P = rng F by A6,XBOOLE_0:def 10;
F is one-to-one
proof
let x1,x2 be object;
assume
A14: x1 in dom F & x2 in dom F & F.x1=F.x2;
reconsider x1,x2 as Element of Bags n by A14,A5;
A15: f.x1 =F.x1 & f.x2 = F.x2 by A14,FUNCT_1:47;
f.x1 = F(x1) & f.x2 = F(x2) by A4;
then F(x1)=F(x2) & x1=F(x1) |n by HILBASIS:def 1, A15,A14;
hence thesis by HILBASIS:def 1;
end;
then
A16: len Sp = card Support p = card Support P = len SP
by CARD_1:5,POLYNOM2:18,PRE_POLY:11,A5,A13,WELLORD2:def 4;
hence len Sp= len SP;
defpred P[Nat] means 1<=$1 <= len Sp implies
for i st 1<= i <= $1 holds SP/.i = Sp/.i bag_extend 0;
A17: rng Sp =Support p & rng SP =Support P by A2,PRE_POLY:def 2;
A18:P[0];
A19:for k be Nat st P[k] holds P[k+1]
proof
let k be Nat;set k1=k+1;
assume that
A20:P[k] and A21:1<= k1<=len Sp;
let i be Nat such that
A22: 1<= i <=k1;
A23: k < len Sp by A21,NAT_1:13;
A24: k = len (SP|k) by A23,A16,FINSEQ_1:59;
A25: rng (Sp|k1) c= Support p &
rng (SP|k1) c= Support P by A17,RELAT_1:70;
A26:Sp|k1 = (Sp|k) ^ <*Sp.k1*> &
SP|k1 = (SP|k) ^ <*SP.k1*> by A16,A21,NAT_1:13,FINSEQ_5:83;
A27:k1 in dom Sp & k1 in dom SP by A21,A16,FINSEQ_3:25;
then
A28: Sp.k1 in rng Sp & SP.k1 in rng SP by FUNCT_1:def 3;
A29: Sp.k1 = Sp/.k1 & SP.k1 = SP/.k1 by A27,PARTFUN1:def 6;
per cases by NAT_1:14;
suppose
A30: k=0;
A31: i=1 by A30,A22,XXREAL_0:1;
A32: Sp/.1 bag_extend 0 in Support P by Th8,A30,A29,A28,A17;
for y be Element of Bags (n+1) st y in Support P
holds [Sp/.1 bag_extend 0 ,y] in B1
proof
let y be Element of Bags (n+1);
set Y=(0,n)-cut y;
assume
A33: y in Support P;
then y.n =0 by Th7;
then Y in Support p by A33,Th9;
then consider w be object such that
A34: w in dom Sp & Sp.w = Y by FUNCT_1:def 3,A17;
y.n = 0 by Th7,A33;
then
A35: y = Y bag_extend 0 by Th4;
reconsider w as Nat by A34;
A36: Sp.w = Sp/.w by A34,PARTFUN1:def 6;
A37: 1<=w by A34,FINSEQ_3:25;
per cases by A37,XXREAL_0:1;
suppose w =1;
hence thesis by PRE_POLY:def 14,A35,A1,A34,A36;
end;
suppose w>1; then
A38: Sp/.1 <> Sp/.w & [Sp/.1,Sp/.w] in B
by A2,PRE_POLY:def 2,A27,A34,A30;
then Sp/.1 <=' Sp/.w by PRE_POLY:def 14;
then Sp/.1 bag_extend 0 < Sp/.w bag_extend 0
by Th14,A38,PRE_POLY:def 10;
then Sp/.1 bag_extend 0 <=' y by A1,A34,A36,A35,PRE_POLY:def 10;
hence thesis by PRE_POLY:def 14;
end;
end;
hence SP/.i = Sp/.i bag_extend 0 by A31,A32,POLYNOM2:18,PRE_POLY:20;
end;
suppose
A39: k >=1;
A40: k1 in Seg k1 by A21;
set Ck = (0,n)-cut SP/.k1;
reconsider Ck as bag of n by A1;
A41: SP/.k1 in rng (SP|k1) by PARTFUN2:18,A40,A27;
then
A42: (SP/.k1).n=0 by Th7,A25;
then Ck in Support p by Th9,A41,A25;
then consider f be object such that
A43: f in dom Sp & Sp.f = Ck by FUNCT_1:def 3,A17;
reconsider f as Nat by A43;
A44: Sp/.f=Sp.f by A43,PARTFUN1:def 6;
A45: SP/.k1 = Ck bag_extend 0 by A1,A42,Th4;
set SpEk=Sp/.k1 bag_extend 0;
SpEk in Support P by A29,A28,A17,Th8;
then consider e be object such that
A46: e in dom SP & SP.e = SpEk by FUNCT_1:def 3,A17;
reconsider e as Nat by A46;
A47: 1<= e<= len SP by FINSEQ_3:25,A46;
A48: SP/.e=SP.e by A46,PARTFUN1:def 6;
A49: SP/.k = Sp/.k bag_extend 0 by A20,A39,A21,NAT_1:13;
A50: SpEk in rng (SP|k1)
proof
assume
A51: not SpEk in rng (SP|k1);
e > k1
proof
assume e <=k1;
then e in Seg k1 by A47;
hence thesis by A51,A48,A46,PARTFUN2:18;
end;
then
A52: Sp/.f < Sp/.k1 by A43,A44,Th14,A46,A27,A45,A48,Th16;
A53: k in dom SP & k in dom Sp by A23,A39,A16,FINSEQ_3:25;
A54: k< k1 by NAT_1:13;
A55: Sp/.k < Sp/.f by A43,A44,Th14,A49,A45,Th16,A27,A53,A54;
then
A56: k<>f;
per cases;
suppose k <=f;
then k < f by A56,XXREAL_0:1;
then k1<=f & k1<>f by A52,NAT_1:13;
then k1 < f by XXREAL_0:1;
hence thesis by A52,A43,A27,Th16;
end;
suppose k > f;
hence thesis by A55,A43,A53,Th16;
end;
end;
A57: rng (SP|k1) = rng (SP|k) \/ rng <*SP.k1*> by A26,FINSEQ_1:31
.= rng (SP|k) \/ {SP.k1} by FINSEQ_1:38;
A58: SpEk = SP.k1
proof
assume SpEk <> SP.k1;
then SpEk in rng (SP|k) by A50,A57,ZFMISC_1:136;
then consider w be object such that
A59: w in dom (SP|k) & (SP|k).w = SpEk by FUNCT_1:def 3;
reconsider w as Nat by A59;
A60: 1<= w<= k by A24,FINSEQ_3:25,A59;
then w < len Sp by A23,XXREAL_0:2;
then
A61: w in dom Sp & w in dom SP by A16,A60,FINSEQ_3:25;
A62: SP/.w = Sp/.w bag_extend 0 by A39,A20,A21,NAT_1:13,A60;
A63: SP/.w = SP.w = (SP|k).w = SpEk by A59,A60,A61,PARTFUN1:def 6,
FINSEQ_3:112;
w<k1 by A60,NAT_1:13;
then Sp/.w bag_extend 0 < Sp/.k1 bag_extend 0 by A27,A61,Th14,Th16;
hence thesis by A62,A63;
end;
per cases by A22,XXREAL_0:1;
suppose i <k1;
then i<=k by NAT_1:13;
hence thesis by A22,A20,A21,NAT_1:13,A39;
end;
suppose i = k1;
hence SP/.i = Sp/.i bag_extend 0 by A58,A27,PARTFUN1:def 6;
end;
end;
end;
for k holds P[k] from NAT_1:sch 2(A18,A19);
hence thesis;
end;
theorem Th18:
for L being right_zeroed add-associative right_complementable
well-unital distributive non trivial doubleLoopStr,
p being Polynomial of n,L,
x being Function of n, L,
y being Function of (n+1), L st y|n=x
holds eval(p,x) = eval(p extended_by_0,y)
proof
let L be right_zeroed add-associative right_complementable
well-unital distributive non trivial doubleLoopStr,
p be Polynomial of n,L,
x be Function of n, L,
y be Function of (n+1), L;
set n1=n+1;
assume
A1:y|n=x;
set S=SgmX(BagOrder n, Support p);
set P=p extended_by_0;
set S1=SgmX(BagOrder n1, Support P);
consider T be FinSequence of L such that
A2: len T = len S & eval(p,x) = Sum T and
A3: for i be Element of NAT st 1 <= i & i <= len T
holds T/.i = (p * S)/.i * eval(S/.i,x) by POLYNOM2:def 4;
consider T1 be FinSequence of L such that
A4: len T1 = len S1 & eval(P,y) = Sum T1 and
A5: for i be Element of NAT st 1 <= i & i <= len T1
holds T1/.i = (P * S1)/.i * eval(S1/.i,y) by POLYNOM2:def 4;
A6:len S = len S1 &
for i be Nat st 1<=i<= len S holds S1/.i = S/.i bag_extend 0 by Th17;
BagOrder n linearly_orders Support p & BagOrder n1 linearly_orders Support P
by POLYNOM2:18;
then
A7:rng S = Support p & rng S1 = Support P by PRE_POLY:def 2;
dom p = Bags n & dom P = Bags n1 by FUNCT_2:def 1;
then
A8:dom (p*S) = dom S & dom (P*S1)=dom S1 by A7,RELAT_1:27;
for i be Nat st 1<=i<=len S holds T.i = T1.i
proof
let i such that
A9: 1<= i<= len S;
A10: i in NAT by ORDINAL1:def 12;
A11:i in dom T & i in dom T1 by A9,A6,A2,A4,FINSEQ_3:25;
A12:i in dom S & i in dom S1 by A9,A6,FINSEQ_3:25;
then
A13:S/.i = S.i & S1/.i = S1.i by PARTFUN1:def 6;
A14: S1/.i = S/.i bag_extend 0 by Th17,A9;
A15: (P * S1)/.i = (P * S1).i by A9,A6,FINSEQ_3:25,A8,PARTFUN1:def 6
.= P.(S1/.i) by A12,A13,FUNCT_1:13
.= P.(S/.i bag_extend 0) by Th17,A9
.= p.(S/.i) by Th6
.= p.(S.i) by A12,PARTFUN1:def 6
.= (p*S).i by A12,FUNCT_1:13
.= (p*S)/.i by A9,FINSEQ_3:25,A8,PARTFUN1:def 6;
thus T1.i = T1/.i by A11,PARTFUN1:def 6
.= (P * S1)/.i * eval(S1/.i,y) by A10,A5,A9,A4,A6
.= (p*S)/.i * eval(S/.i,x) by A14,Th13,A1,A15
.= T/.i by A10,A3,A9,A2
.=T.i by A11,PARTFUN1:def 6;
end;
hence thesis by FINSEQ_1:14,A2,A4,Th17;
end;
begin :: Polynomial permuted by perm
theorem Th19:
for O being Ordinal, L being well-unital commutative associative non trivial
doubleLoopStr, x being Function of O, L, b being bag of O
for S being one-to-one FinSequence of O st
rng S = support b
ex y being FinSequence of L st
len y = card support b &
eval(b,x) = Product y &
for i st 1 <= i & i <= len y holds
y/.i = power(L).((x*S)/.i, (b*S)/.i)
proof
let n be Ordinal, L be well-unital commutative associative non trivial
doubleLoopStr, x be Function of n,L, b be bag of n;
let S be one-to-one FinSequence of n such that
A1:rng S = support b;
set SG=SgmX(RelIncl n, support b);
consider y be FinSequence of L such that
A2: len y = len SG & eval(b,x) = Product y and
A3: for i being Element of NAT st 1 <= i & i <= len y holds
y/.i = power(L).((x * SG)/.i,(b * SG)/.i) by POLYNOM2:def 2;
A4:RelIncl n linearly_orders support b by PRE_POLY:82;
A5:SG is one-to-one & len SG = card support b by PRE_POLY:10,11,82;
A6:rng SG = support b by A4,PRE_POLY:def 2;
then consider H be Function such that
A7: dom H=dom S & rng H = dom SG & H is one-to-one & SG*H = S
by A1,A5,RFINSEQ:26,CLASSES1:77;
A8:len S=len SG by A1,A5,A6,FINSEQ_1:48;
A9: dom y = dom SG = dom S by A2,A8,FINSEQ_3:29;
then
A10: dom (y*H) = dom H & dom S = Seg len S
by A7,RELAT_1:27,FINSEQ_1:def 3;
then reconsider yH=y*H as FinSequence by A7,FINSEQ_1:def 2;
reconsider H as Function of dom y,dom y by A7,A9,FUNCT_2:1;
H is onto by A7,A2,FINSEQ_3:29;
then reconsider H as Permutation of dom y by A7;
A11:rng y c= the carrier of L;
rng yH c= rng y by RELAT_1:26;
then rng yH c= the carrier of L by A11;
then reconsider yH as FinSequence of L by FINSEQ_1:def 4;
take yH;
thus len yH = card support b by A7,A10,FINSEQ_3:29,A8,A5;
A12: H is Permutation of dom y;
thus eval(b,x) = (the multF of L)"**" y by GROUP_4:def 2,A2
.=(the multF of L)"**" yH by FINSOP_1:7,A12
.= Product yH by GROUP_4:def 2;
let i be Nat such that
A13:1<=i & i <= len yH;set Hi=H/.i;
i in dom yH by A13,FINSEQ_3:25;
then
A14: yH/.i = yH.i & H.i = Hi & yH.i = y.(H.i) & H.i in rng H
by A10,PARTFUN1:def 6,FUNCT_1:12,def 3;
then
A15:1<= Hi <= len y & Hi in NAT & y.Hi = y/.Hi
by FINSEQ_3:25,PARTFUN1:def 6;
dom x = n by FUNCT_2:def 1;
then rng SG c= dom x & rng S c= dom x;
then
A16: dom (x * SG) = dom SG & dom (x * S) = dom S by RELAT_1:27;
then
A17:(x * SG)/.Hi = (x * SG).Hi by A14,A7,PARTFUN1:def 6
.= x.(SG.Hi) by A16,A14,A7,FUNCT_1:12
.= x.((SG*H).i) by A14,A13,FINSEQ_3:25,A7,A10,FUNCT_1:12
.= (x*S).i by A7,A16,A13,FINSEQ_3:25,A10,FUNCT_1:12
.= (x*S)/.i by A7,A16,A13,FINSEQ_3:25,A10,PARTFUN1:def 6;
dom b = n by PARTFUN1:def 2;
then rng SG c= dom b & rng S c= dom b;
then
A18: dom (b * SG) = dom SG & dom (b * S) = dom S by RELAT_1:27;
then (b * SG)/.Hi = (b * SG).Hi by A14,A7,PARTFUN1:def 6
.= b.(SG.Hi) by A18,A14,A7,FUNCT_1:12
.= b.((SG*H).i) by A14,A13,FINSEQ_3:25,A7,A10,FUNCT_1:12
.= (b*S).i by A7,A18,A13,FINSEQ_3:25,A10,FUNCT_1:12
.= (b*S)/.i by A7,A18,A13,FINSEQ_3:25,A10,PARTFUN1:def 6;
hence yH/.i = power(L).((x * S)/.i,(b * S)/.i) by A3,A17,A14,A15;
end;
theorem Th20:
for O being Ordinal,
L being well-unital commutative associative non trivial
doubleLoopStr, x being Function of O, L, b being bag of O
for perm being Permutation of O holds
eval(b,x) = eval(b*perm,x*perm)
proof
let n be Ordinal, L be well-unital commutative associative non trivial
doubleLoopStr, x be Function of n, L, b be bag of n;
let perm be Permutation of n;
set SG=SgmX(RelIncl n, support b);
consider y be FinSequence of L such that
A1: len y = len SG & eval(b,x) = Product y and
A2: for i being Element of NAT st 1 <= i & i <= len y holds
y/.i = power(L).((x * SG)/.i,(b * SG)/.i) by POLYNOM2:def 2;
A3:RelIncl n linearly_orders support b by PRE_POLY:82;
A4:SG is one-to-one & len SG = card support b by PRE_POLY:10,11,82;
A5:rng SG = support b by A3,PRE_POLY:def 2;
set P=perm";
A6:dom perm=n=rng perm & dom P=n=rng P by FUNCT_2:52,def 3;
A7: rng (P*SG) c= support (b*perm)
proof
let y be object such that
A8: y in rng (P*SG);
consider w be object such that
A9: w in dom (P*SG) & (P*SG).w=y by A8,FUNCT_1:def 3;
A10: w in dom SG & y = P.(SG.w) & SG.w in dom P by A9,FUNCT_1:11,12;
then
A11: y in rng P by FUNCT_1:def 3;
A12: SG.w = perm.y by A10,FUNCT_1:35,A6;
SG.w in support b by A5,A10,FUNCT_1:def 3;
then
A13: b.(perm.y)<>0 by A12,PRE_POLY:def 7;
b.(perm.y)= (b*perm).y by A11,A6,FUNCT_1:13;
hence thesis by A13,PRE_POLY:def 7;
end;
A14:support (b*perm) c= rng (P*SG)
proof
let x be object such that
A15:x in support (b*perm);
A16:(b*perm).x <>0 by A15,PRE_POLY:def 7;
then x in dom (b*perm) by FUNCT_1:def 2;
then
A17:x in dom perm & perm.x in dom b & (b*perm).x = b.(perm.x)
by FUNCT_1:11,12;
then A18: x= P.(perm.x) & perm.x in support b
by A16,FUNCT_1:34,PRE_POLY:def 7;
then consider w be object such that
A19: w in dom SG & SG.w = perm.x by A5,FUNCT_1:def 3;
w in dom (P*SG) & (P*SG).w = P.(SG.w) by A6,A17,A19,FUNCT_1:11,13;
hence thesis by A18,A19,FUNCT_1:def 3;
end;
reconsider S=P*SG as one-to-one FinSequence of n by A4;
consider Y be FinSequence of L such that
A20:len Y = card support (b*perm) &
eval(b*perm,x*perm) = Product Y and
A21: for i being Nat st 1 <= i & i <= len Y holds
Y/.i = power(L).(((x*perm)*S)/.i, ((b*perm)*S)/.i)
by Th19,A7,XBOOLE_0:def 10,A14;
A22: len Y = len y by A20,A1,A4,Th2;
for i being Nat st 1 <= i & i <= len Y holds Y.i = y.i
proof
let i be Nat such that A23:1<=i <= len Y;
A24: rng perm = n by FUNCT_2:def 3;
A25:n c= dom x & n = dom b by PARTFUN1:def 2;
A26:(x*perm)*S = (x*perm)*P*SG by RELAT_1:36
.= x*(perm*P)*SG by RELAT_1:36
.= x*(id n)*SG by A24, FUNCT_1:39
.= x*SG by A25,RELAT_1:51;
A27:(b*perm)*S = (b*perm)*P*SG by RELAT_1:36
.= b*(perm*P)*SG by RELAT_1:36
.= b*(id n)*SG by A24, FUNCT_1:39
.= b*SG by A25,RELAT_1:51;
A28: i in dom y & i in dom Y by A22,A23,FINSEQ_3:25;
hence Y.i = Y/.i by PARTFUN1:def 6
.= power(L).(((x*perm)*S)/.i, ((b*perm)*S)/.i) by A21,A23
.= y/.i by A2,A23,A28,A22,A27,A26
.= y.i by A28,PARTFUN1:def 6;
end;
hence thesis by A20,A1,A4,Th2,FINSEQ_1:14;
end;
definition
let O be Ordinal;
let L be non empty ZeroStr;
let s be Series of O,L;
let perm be Permutation of O;
func s permuted_by perm -> Series of O,L means :Def4:
for b being bag of O holds it.b = s.(b*perm);
existence
proof
defpred P[Element of Bags O, Element of L] means $2=s. ($1*perm);
A1:for x being Element of Bags O ex y being Element of L st P[x,y];
consider f be Function of Bags O,L such that
A2: for x be Element of Bags O holds P[x,f.x] from FUNCT_2:sch 3(A1);
take f;
let b be bag of O;
b is Element of Bags O by PRE_POLY:def 12;
hence thesis by A2;
end;
uniqueness
proof
let e1,e2 be Series of O,L such that
A3: for b be bag of O holds e1.b = s.(b*perm) and
A4: for b be bag of O holds e2.b = s.(b*perm);
now let b be Element of Bags O;
e1.b=s.(b*perm)=e2.b by A3,A4;
hence e1.b=e2.b;
end;
hence thesis;
end;
end;
theorem Th21:
for O being Ordinal,
L being non empty ZeroStr,
perm being Permutation of O,
s being Series of O,L, b being bag of O holds
b in Support (s permuted_by perm) iff b*perm in Support s
proof
let O be Ordinal, L be non empty ZeroStr,
perm be Permutation of O,s be Series of O,L, b be bag of O;
set P = s permuted_by perm;
A1: dom P= Bags O = dom s by FUNCT_2:def 1;
A2:P.b = s.(b*perm) by Def4;
thus b in Support P implies b*perm in Support s
proof
assume b in Support P;
then
A3: P.b <>0.L by POLYNOM1:def 3;
b*perm in Bags O by PRE_POLY:def 12;
hence thesis by A3,A1,A2,POLYNOM1:def 3;
end;
assume b*perm in Support s;
then
A4: s.(b*perm)<>0.L by POLYNOM1:def 3;
b in Bags O by PRE_POLY:def 12;
hence thesis by A4,A1,A2,POLYNOM1:def 3;
end;
theorem Th22:
for O being Ordinal,
L being non empty ZeroStr,
perm being Permutation of O,
s being Series of O,L, b being bag of O holds
b*perm" in Support (s permuted_by perm) iff b in Support s
proof
let O be Ordinal,
L be non empty ZeroStr,
perm be Permutation of O,
s be Series of O,L, b be bag of O;
set P = s permuted_by perm;
A1: dom P= Bags O = dom s by FUNCT_2:def 1;
A2: dom b = O by PARTFUN1:def 2;
dom perm = O by FUNCT_2:52;
then perm"*perm = id O by FUNCT_1:39;
then (b*perm")*perm = b*(id O) by RELAT_1:36 .= b by A2,RELAT_1:51;
then
A3:P.(b*perm") = s.b by Def4;
thus b*perm" in Support P implies b in Support s
proof
assume b*perm" in Support P;
then
A4: P.(b*perm") <>0.L by POLYNOM1:def 3;
b in Bags O by PRE_POLY:def 12;
hence thesis by A4,A1,A3,POLYNOM1:def 3;
end;
assume b in Support s;
then
A5: s.b<>0.L by POLYNOM1:def 3;
b*perm" in Bags O by PRE_POLY:def 12;
hence thesis by A5,A1,A3,POLYNOM1:def 3;
end;
theorem Th23:
for O being Ordinal,
L being non empty ZeroStr,
perm being Permutation of O,
s being Series of O,L holds
card Support s = card Support (s permuted_by perm)
proof
let O be Ordinal, L be non empty ZeroStr,
perm be Permutation of O,s be Series of O,L;
set P = s permuted_by perm;
defpred R[bag of O,bag of O] means $2 = $1*perm;
A1:for x be Element of Bags O ex y be Element of Bags O st R[x,y]
proof
let x be Element of Bags O;
x*perm in Bags O by PRE_POLY:def 12;
hence thesis;
end;
consider f be Function of Bags O,Bags O such that
A2:for x be Element of Bags O holds R[x,f.x] from FUNCT_2:sch 3(A1);
A3:dom f= Bags O by FUNCT_2:52;
rng perm = O =dom perm by FUNCT_2:52,def 3;
then
A4: perm*perm" = id O = perm"*perm by FUNCT_1:39;
A5:f is one-to-one
proof
let x1,x2 be object such that
A6:x1 in dom f & x2 in dom f & f.x1=f.x2;
reconsider x1,x2 as Element of Bags O by A6;
A7: f.x1 = x1*perm & f.x2 = x2*perm by A2;
A8:dom x1=O =dom x2 by PARTFUN1:def 2;
A9:(x1*perm)*perm" = x1*(id O) by A4,RELAT_1:36
.= x1 by A8,RELAT_1:51;
(x2*perm)*perm" = x2*(id O) by A4,RELAT_1:36
.= x2 by A8,RELAT_1:51;
hence thesis by A6,A7,A9;
end;
A10:f.:(Support P) c= Support s
proof
let y be object such that
A11:y in f.:(Support P);
consider x be object such that
A12:x in dom f & x in Support P & f.x=y by A11,FUNCT_1:def 6;
reconsider x as Element of Bags O by A12;
f.x = x*perm in Support s by A2,Th21,A12;
hence thesis by A12;
end;
Support s c= f.:(Support P)
proof
let y be object such that
A13:y in Support s;
reconsider y as Element of Bags O by A13;
A14:y*perm" in Support P by A13,Th22;
A15:dom y=O by PARTFUN1:def 2;
y*perm" in Bags O by PRE_POLY:def 12;
then
f.(y*perm") = (y*perm")*perm by A2
.= y*(id O) by A4,RELAT_1:36
.= y by A15,RELAT_1:51;
hence thesis by A3,FUNCT_1:def 6,A14;
end;
then f.:(Support P) = Support s by A10,XBOOLE_0:def 10;
hence thesis by CARD_1:5,A5,A3,CARD_1:33;
end;
theorem Th24:
for O being Ordinal,
L being Abelian right_zeroed add-associative right_complementable
well-unital distributive non trivial doubleLoopStr,
p being Polynomial of O,L,
x being Function of O, L
for S being one-to-one FinSequence of Bags O st
rng S = Support p
ex y being FinSequence of L st
len y = card Support p &
eval(p,x) = Sum y &
for i being Nat st 1 <= i & i <= len y holds
y/.i = (p * S)/.i * eval(S/.i,x)
proof
let n be Ordinal, L be Abelian right_zeroed add-associative
right_complementable well-unital distributive non trivial doubleLoopStr,
p be Polynomial of n,L,x be Function of n, L;
let S be one-to-one FinSequence of Bags n such that
A1:rng S = Support p;
set SG=SgmX(BagOrder n, Support p);
consider y be FinSequence of L such that
A2: len y = len SG & eval(p,x) = Sum y and
A3: for i be Element of NAT st 1 <= i & i <= len y
holds y/.i = (p * SG)/.i * eval((SG/.i),x) by POLYNOM2:def 4;
A4:BagOrder n linearly_orders Support p by POLYNOM2:18;
A5:SG is one-to-one & len SG = card Support p
by POLYNOM2:18,PRE_POLY:10,11;
A6:rng SG = Support p by A4,PRE_POLY:def 2;
then consider H be Function such that
A7: dom H=dom S & rng H = dom SG & H is one-to-one & SG*H = S
by A1,A5, RFINSEQ:26,CLASSES1:77;
A8:len S=len SG by A1,A5,A6,FINSEQ_1:48;
A9: dom y = dom SG = dom S by A2,A8,FINSEQ_3:29;
then
A10: dom (y*H) = dom H & dom S = Seg len S by A7,RELAT_1:27,FINSEQ_1:def 3;
then reconsider yH=y*H as FinSequence by A7,FINSEQ_1:def 2;
reconsider H as Function of dom y,dom y by A7,A9,FUNCT_2:1;
H is onto by A7,A2,FINSEQ_3:29;then
reconsider H as Permutation of dom y by A7;
A11:rng y c= the carrier of L;
rng yH c= rng y by RELAT_1:26;
then rng yH c= the carrier of L by A11;
then reconsider yH as FinSequence of L by FINSEQ_1:def 4;
reconsider yH as FinSequence of L;
take yH;
thus len yH = card Support p by A7,A10,FINSEQ_3:29,A8,A5;
A12: len y = len yH by A2,A8,A7,A10,FINSEQ_3:29;
for i be Nat st i in dom yH holds yH.i = y.(H.i) by FUNCT_1:12;
hence eval(p,x) = Sum yH by A2,A12,RLVECT_2:6;
let i be Nat such that
A13:1<=i<= len yH;
set Hi=H/.i;
i in dom yH by A13,FINSEQ_3:25;
then
A14: yH/.i = yH.i & H.i = Hi & yH.i = y.(H.i) & H.i in rng H
by A10,PARTFUN1:def 6,FUNCT_1:12,def 3;
then
A15:1<= Hi <= len y & Hi in NAT & y.Hi = y/.Hi
by FINSEQ_3:25,PARTFUN1:def 6;
dom p = Bags n by FUNCT_2:def 1;
then rng SG c= dom p & rng S c= dom p;
then
A16: dom (p * SG) = dom SG & dom (p * S) = dom S by RELAT_1:27;
then
A17:(p * SG)/.Hi = (p * SG).Hi by A14,A7,PARTFUN1:def 6
.= p.(SG.Hi) by A16,A14,A7,FUNCT_1:12
.= p.((SG*H).i) by A14,A13,FINSEQ_3:25,A7,A10,FUNCT_1:12
.= (p*S).i by A7,A16,A13,FINSEQ_3:25,A10,FUNCT_1:12
.= (p*S)/.i by A7,A16,A13,FINSEQ_3:25,A10,PARTFUN1:def 6;
SG/.Hi = SG.(H.i) by A14,A7,PARTFUN1:def 6
.= (SG*H).i by A13,FINSEQ_3:25,A7,A10,FUNCT_1:12
.= S/.i by A13,FINSEQ_3:25,A7,A10,PARTFUN1:def 6;
hence yH/.i = (p * S)/.i * eval(S/.i,x) by A3,A17,A14,A15;
end;
registration
let O be Ordinal;
let L be non empty ZeroStr;
let perm be Permutation of O;
let p be Polynomial of O,L;
cluster p permuted_by perm -> finite-Support;
coherence
proof
A1: Support p is finite by POLYNOM1:def 5;
card Support p = card Support (p permuted_by perm) by Th23;
then Support (p permuted_by perm) is finite by A1;
hence thesis by POLYNOM1:def 5;
end;
end;
theorem Th25:
for O being Ordinal,
L being Abelian right_zeroed add-associative right_complementable
well-unital distributive commutative associative non trivial
doubleLoopStr,
p being Polynomial of O,L,
x being Function of O, L
for perm being Permutation of O holds
eval(p,x) = eval(p permuted_by perm,x*perm")
proof
let O be Ordinal, L be Abelian right_zeroed add-associative
right_complementable
well-unital distributive commutative associative non trivial doubleLoopStr,
p be Polynomial of O,L,
x be Function of O, L;
let perm be Permutation of O;
set SB=SgmX(BagOrder O, Support p);
consider y be FinSequence of L such that
A1: len y = len SB & eval(p,x) = Sum y and
A2: for i be Element of NAT st 1 <= i & i <= len y holds
y/.i = (p * SB)/.i * eval((SB/.i),x) by POLYNOM2:def 4;
A3:BagOrder O linearly_orders Support p by POLYNOM2:18;
A4:SB is one-to-one & len SB = card Support p
by PRE_POLY:10,11,POLYNOM2:18;
A5:rng SB = Support p by A3,PRE_POLY:def 2;
set P=p permuted_by perm;
defpred R[bag of O,bag of O] means $2 = $1*perm";
A6:for x be Element of Bags O ex y be Element of Bags O st R[x,y]
proof
let x be Element of Bags O;
x*perm" in Bags O by PRE_POLY:def 12;
hence thesis;
end;
consider f be Function of Bags O,Bags O such that
A7:for x be Element of Bags O holds R[x,f.x] from FUNCT_2:sch 3(A6);
A8:dom f= Bags O by FUNCT_2:52;
rng perm = O =dom perm by FUNCT_2:52,def 3;
then
A9: perm*perm" = id O = perm"*perm by FUNCT_1:39;
A10:f is one-to-one
proof
let x1,x2 be object such that
A11:x1 in dom f & x2 in dom f & f.x1=f.x2;
reconsider x1,x2 as Element of Bags O by A11;
A12: f.x1 = x1*perm" & f.x2 = x2*perm" by A7;
A13:dom x1=O =dom x2 by PARTFUN1:def 2;
A14:(x1*perm")*perm = x1*(id O) by A9,RELAT_1:36
.= x1 by A13,RELAT_1:51;
(x2*perm")*perm = x2*(id O) by A9,RELAT_1:36
.= x2 by A13,RELAT_1:51;
hence thesis by A11,A12,A14;
end;
reconsider fSB = f*SB as one-to-one FinSequence of Bags O by A4,A10;
rng SB c= dom f by A8;
then
A15: dom fSB = dom SB by RELAT_1:27;
A16:rng fSB c= Support P
proof
let y be object such that
A17: y in rng fSB;
consider x be object such that
A18: x in dom fSB & fSB.x=y by FUNCT_1:def 3,A17;
A19:y = f.(SB.x) & x in dom SB & SB.x in dom f by A18,FUNCT_1:11,12;
then reconsider SBx =SB.x as Element of Bags O;
SBx in Support p by A19,A5,FUNCT_1:def 3;
then SBx*perm" in Support P by Th22;
hence thesis by A7,A19;
end;
Support P c= rng fSB
proof
let y be object such that
A20:y in Support P;
reconsider y as Element of Bags O by A20;
A21:dom y=O by PARTFUN1:def 2;
A22:y*perm in Support p by A20,Th21;
then
A23: f.(y*perm) = y*perm*perm" by A7
.= y*(id O) by A9,RELAT_1:36
.= y by A21,RELAT_1:51;
consider w be object such that
A24: w in dom SB & SB.w=y*perm by A5,A22,FUNCT_1:def 3;
w in dom fSB & fSB.w =y by A8,A22,A23,A24,FUNCT_1:11,13;
hence thesis by FUNCT_1:def 3;
end;
then consider z be FinSequence of L such that
A25: len z = card Support P & eval(P,x*perm") = Sum z and
A26: for i be Nat st 1 <= i & i <= len z holds
z/.i = (P * fSB)/.i * eval(fSB/.i,x*perm") by A16,XBOOLE_0:def 10,Th24;
A27: len y = len z by A1,A4,A25,Th23;
for i be Nat st 1<=i<=len y holds y.i=z.i
proof
let i be Nat such that
A28:1<=i<=len y;
A29:i in NAT by ORDINAL1:def 12;
A30:i in dom y & i in dom z & i in dom SB by A28,A1,FINSEQ_3:25,A27;
then
A31: SB.i = SB/.i by PARTFUN1:def 6;
then reconsider SBi=SB.i as Element of Bags O;
A32:dom SBi=O by PARTFUN1:def 2;
A33:SBi*perm"*perm = SBi*(id O) by A9,RELAT_1:36
.= SBi by A32,RELAT_1:51;
dom p = Bags O =dom P by FUNCT_2:def 1;
then rng SB c= dom p & rng fSB c= dom P;
then
A34: dom (p * SB) = dom SB & dom (P * fSB) = dom fSB by RELAT_1:27;
then
A35:(P * fSB)/.i = (P * fSB).i by A15,A28,FINSEQ_3:25,A1,PARTFUN1:def 6
.= P.(fSB.i) by A1,A15,A28,FINSEQ_3:25,A34,FUNCT_1:12
.= P.(f.SBi) by A15,A28,FINSEQ_3:25,A1,FUNCT_1:12
.= P.(SBi*perm") by A7
.= p.(SBi*perm"*perm) by Def4
.= (p*SB).i by A28,A1,A33,FINSEQ_3:25,A34,FUNCT_1:12
.= (p*SB)/.i by A34,A28,A1,FINSEQ_3:25,PARTFUN1:def 6;
A36: (SB/.i)*perm" = f.SBi by A7,A31
.=fSB.i by A15,A28,A1,FINSEQ_3:25,FUNCT_1:12
.=fSB/.i by A15,A28,A1,FINSEQ_3:25,PARTFUN1:def 6;
thus y.i = y/.i by A30,PARTFUN1:def 6
.= (p * SB)/.i * eval(SB/.i,x) by A29,A2,A28
.= (P * fSB)/.i * eval(fSB/.i,x*perm") by A35,A36,Th20
.= z/.i by A26,A28,A27
.= z.i by A30,PARTFUN1:def 6;
end;
hence thesis by FINSEQ_1:14,A1,A4,A25,Th23;
end;
theorem Th26:
for O being Ordinal,
L being non empty ZeroStr,
s being Series of O,L,
perm being Permutation of O holds
rng (s permuted_by perm) = rng s
proof
let O be Ordinal,L be non empty ZeroStr,
s be Series of O,L,perm be Permutation of O;
set P=s permuted_by perm;
A1:dom P = Bags O & dom s= Bags O by FUNCT_2:def 1;
thus rng P c= rng s
proof
let y be object;
assume y in rng P;
then consider x be object such that
A2: x in dom P & P.x=y by FUNCT_1:def 3;
reconsider x as Element of Bags O by A2;
A3: x*perm in dom s by A1,PRE_POLY:def 12;
s.(x*perm) = P.x by Def4;
hence thesis by A3,FUNCT_1:def 3,A2;
end;
let y be object;
assume y in rng s;
then consider x be object such that
A4: x in dom s & s.x=y by FUNCT_1:def 3;
reconsider x as Element of Bags O by A4;
A5: dom x = O by PARTFUN1:def 2;
dom perm = O by FUNCT_2:52;
then perm"*perm = id O by FUNCT_1:39;
then (x*perm")*perm = x*(id O) by RELAT_1:36
.= x by A5,RELAT_1:51;
then
A6:P.(x*perm") = s.x by Def4;
x*perm" in dom P by A1,PRE_POLY:def 12;
hence thesis by A4,A6,FUNCT_1:def 3;
end;
begin :: Main Lemmas
theorem Th27:
for L being right_zeroed add-associative right_complementable
well-unital distributive non trivial doubleLoopStr,
p being Polynomial of n,L
ex q being Polynomial of n+m,L st
rng q c= rng p \/ {0.L}&
for x being Function of n, L,
y being Function of (n+m), L st y|n=x
holds eval(p,x) = eval(q,y)
proof
let L be right_zeroed add-associative right_complementable
well-unital distributive non trivial doubleLoopStr,
p be Polynomial of n,L;
defpred P[Nat] means ex q be Polynomial of n+$1,L st
rng q c= rng p \/ {0.L}&
for x be Function of n, L,
y be Function of (n+$1), L st y|n=x
holds eval(p,x) = eval(q,y);
A1:P[0]
proof
reconsider q=p as Polynomial of n+0,L;
take q;
thus rng q c= rng p \/ {0.L} by XBOOLE_1:7;
:: let x be Function of n, L,y be Function of (n+0), L;
thus thesis;
end;
A2:P[k] implies P[k+1]
proof set k1=k+1;
assume P[k];then
consider q be Polynomial of n+k,L such that
A3: rng q c= rng p \/{0.L} and
A4: for x be Function of n, L,y be Function of (n+k), L st y|n=x
holds eval(p,x) = eval(q,y);
reconsider P = q extended_by_0 as Polynomial of n+k1,L;
take P;
rng P = rng q \/ {0.L} by Th10;
then rng P c= rng p \/{0.L}\/{0.L} by A3,XBOOLE_1:13;
hence rng P c= rng p \/ {0.L} by XBOOLE_1:7,12;
let x be Function of n, L,
y be Function of n+k1, L such that
A5: y|n=x;
A6: rng (y|(n+k)) c= rng y & rng y c= the carrier of L by RELAT_1:70;
len (@y) = n+k1 & n+k < n+k+1 by CARD_1:def 7,NAT_1:13;
then len (@y|(n+k)) = n+k by AFINSQ_1:54;
then reconsider Y= @y|(n+k) as Function of n+k,L by A6,FUNCT_2:2;
Segm n c= Segm (n+k) by NAT_1:39,11;
then
A7: Y |n = x by A5,RELAT_1:74;
thus eval(P,y) = eval(q,Y) by Th18
.= eval(p,x) by A4,A7;
end;
P[k] from NAT_1:sch 2(A1,A2);
hence thesis;
end;
theorem Th28:
for L being Abelian right_zeroed add-associative
right_complementable well-unital distributive commutative
associative non trivial doubleLoopStr,
p being Polynomial of n+m,L
ex q being Polynomial of n+k+m,L st
rng q c= rng p \/{0.L}&
for XY being Function of n+m,L,
XanyY being Function of n+k+m,L st
XY|n = XanyY|n&@XY/^n = @XanyY/^(n+k)
holds eval(p,XY) = eval(q,XanyY)
proof
let L be Abelian right_zeroed add-associative
right_complementable well-unital distributive commutative associative
non trivial doubleLoopStr,
p be Polynomial of n+m,L;
consider P be Polynomial of n+m+k,L such that
A1: rng P c= rng p \/ {0.L} and
A2: for x be Function of n+m, L,
y be Function of (n+m)+k, L st y|(n+m)=x
holds eval(p,x) = eval(P,y) by Th27;
reconsider P1=P as Polynomial of n+k+m,L;
set I=id (n+k+m);
dom I = n+k+m;
then reconsider I as XFinSequence by AFINSQ_1:5;
set nm=n+m,Inm = I|nm;
A3:I = Inm ^ (I/^nm);
A4:Inm = (Inm|n)^(Inm/^n);
A5:rng I = rng Inm \/ rng (I/^nm) by A3,AFINSQ_1:26;
A6:rng Inm misses rng (I/^nm) by A3,Th1;
A7:rng Inm = rng(Inm|n)\/rng(Inm/^n) by A4,AFINSQ_1:26;
A8:rng (Inm|n) misses rng (Inm/^n) by A4,Th1;
rng (Inm|n) misses rng (I/^nm) by A6,XBOOLE_1:63,A7, XBOOLE_1:7;
then
A9: (Inm|n) ^ (I/^nm) is one-to-one by CARD_FIN:52;
A10: rng ((Inm|n) ^ (I/^nm)) = rng (Inm|n) \/ rng (I/^nm) by AFINSQ_1:26;
rng (I/^nm) misses rng (Inm/^n) by A6,XBOOLE_1:63,A7,XBOOLE_1:7;
then rng ((Inm|n) ^ (I/^nm)) misses rng (Inm/^n) by A10,A8,XBOOLE_1:70;
then
A11: (Inm|n) ^ (I/^nm)^ (Inm/^n) is one-to-one by A9,CARD_FIN:52;
A12: rng ((Inm|n) ^ (I/^nm)^ (Inm/^n)) =
rng ((Inm|n) ^ (I/^nm)) \/ rng (Inm/^n) by AFINSQ_1:26
.= rng (Inm|n) \/ rng(I/^nm) \/ rng (Inm/^n) by AFINSQ_1:26
.= n+k+m by A5,A7,XBOOLE_1:4;
len ((Inm|n) ^ (I/^nm)^ (Inm/^n))
= len ((Inm|n) ^ (I/^nm)) + len (Inm/^n) by AFINSQ_1:17
.= len (Inm|n) + len (I/^nm) +len (Inm/^n) by AFINSQ_1:17
.= len (Inm|n) + len (Inm/^n)+ len (I/^nm)
.= len Inm+ len (I/^nm) by A4,AFINSQ_1:17
.= len I by A3,AFINSQ_1:17;
then reconsider III=(Inm|n) ^ (I/^nm)^ (Inm/^n) as Function of n+k+m,n+k+m
by A12,FUNCT_2:1;
III is onto by A12;
then reconsider III as Permutation of n+k+m by A11;
take T = P1 permuted_by III";
thus rng T c= rng p \/ {0.L} by A1,Th26;
let XY be Function of n+m,L,
XanyY be Function of n+k+m,L such that
A13: XY|n = XanyY|n & @XY/^n = @XanyY/^(n+k);
A14: len @XY = n+m & len @XanyY = n+k+m by FUNCT_2:def 1; then
A15:len(@XY/^n) = n+m-'n by AFINSQ_2:def 2
.= m by NAT_D:34;
A16:len(@XanyY/^(n+k)) = n+k+m-'(n+k) by A14,AFINSQ_2:def 2
.= m by NAT_D:34;
len (@XanyY|(n+k)) = n+k by A14,AFINSQ_1:54,NAT_1:11; then
A17: len (@XanyY|(n+k) /^ n) = n+k-'n by AFINSQ_2:def 2
.= k by NAT_D:34;
then A18: len (@XY ^ (@XanyY|(n+k) /^ n)) = n+m+k by A14,AFINSQ_1:17;
rng (@XY ^ (@XanyY|(n+k) /^ n)) c= the carrier of L by RELAT_1:def 19;
then reconsider R = @XY ^ (@XanyY|(n+k) /^ n) as Function of (n+m)+k,L
by A18,FUNCT_2:2;
reconsider r = R as Function of (n+k)+m,L;
R|(n+m) = @XY|(n+m) by AFINSQ_1:58,A14 .= @XY;
then A19: eval(p,XY) = eval(P,R) by A2;
(III")"=III by FUNCT_1:43;then A20: eval(P1,r) = eval(T,r*III) by Th25;
A21: dom @(r*III)=n+k+m = dom @XanyY by FUNCT_2:def 1;
n+m <= n+m+k by NAT_1:11;
then nm <= len I;
then
A22:len Inm = nm & len (I/^nm)= nm+k-'nm by AFINSQ_1:54,AFINSQ_2:def 2;
then
A23:len (I/^nm) = k by NAT_D:34;
A24: n<=nm by NAT_1:11;
A25:len (Inm|n) = n & len (Inm/^n) = nm-'n
by A22,NAT_1:11,AFINSQ_1:54,AFINSQ_2:def 2;
then
A26: len (Inm/^n) = m by NAT_D:34;
A27: len ((Inm|n) ^ (I/^nm)) = n+k by A23,A25,AFINSQ_1:17;
for k st k in dom @XanyY holds @(r*III).k = @XanyY.k
proof
let w be Nat;
assume
A28: w in dom @XanyY;
per cases;
suppose
A29: w < n;
then
A30: w in dom (Inm|n) c= dom ((Inm|n) ^ (I/^nm))
by A25,AFINSQ_1:66,21;
w < nm by A29,A24,XXREAL_0:2;
then
A31: w in Segm nm by NAT_1:44;
A32: III.w = ((Inm|n) ^ (I/^nm)).w by AFINSQ_1:def 3,A30
.= (Inm|n).w by A30,AFINSQ_1:def 3
.= Inm.w by A29,A25,AFINSQ_1:66,FUNCT_1:47
.= I.w by A31,FUNCT_1:49
.= w by A21,A28,FUNCT_1:17;
w+0 < n+m by A29,XREAL_1:8;
then w in dom @XY by A14,AFINSQ_1:66;
then r.w = @XY.w by AFINSQ_1:def 3
.= (@XY|n).w by A29,A25,AFINSQ_1:66,FUNCT_1:49
.= XanyY.w by A13,A29,A25,AFINSQ_1:66,FUNCT_1:49;
hence thesis by A32,A28,FUNCT_1:12,A21;
end;
suppose
A33: n+k > w >= n;
then reconsider wn=w-n as Nat by NAT_1:21;
n+k>n+wn by A33;
then
A34: wn in Segm k by NAT_1:44,XREAL_1:6;
A35: w in Segm (n+k) by A33,NAT_1:44;
nm+wn = m+w;
then nm+wn < m+(n+k) by A33,XREAL_1:6;
then
A36: nm+wn in Segm (n+m+k) by NAT_1:44;
w in dom ((Inm|n) ^ (I/^nm)) by A33,A27,AFINSQ_1:66;
then
A37: III.w = ((Inm|n) ^ (I/^nm)).w by AFINSQ_1:def 3
.= (I/^nm).wn by A33,AFINSQ_1:18,A23,A25
.= I.(nm+wn) by A23,A34,AFINSQ_2:def 2
.= nm+wn by A36,FUNCT_1:17;
r.(nm+wn) = (@XanyY|(n+k) /^ n).wn by A14,A17,A34,AFINSQ_1:def 3
.= (@XanyY|(n+k)). (wn+n) by A17,A34,AFINSQ_2:def 2
.=@XanyY.w by A35,FUNCT_1:49;
hence thesis by A37,A28,FUNCT_1:12,A21;
end;
suppose w >= n+k;
then reconsider wnk=w-(n+k) as Nat by NAT_1:21;
A38: n+k+m >n+k+wnk by A28,A14,AFINSQ_1:66;
then
A39: m > wnk by XREAL_1:6;
A40: wnk in Segm m by NAT_1:44,A38,XREAL_1:6;
then
A41: wnk in dom (Inm/^n) by A25,NAT_D:34;
wnk +n < m+n by A39,XREAL_1:6;
then wnk +n+0 < m+n+k by XREAL_1:8;
then
A42: wnk +n in Segm (n+k+m) & wnk +n in Segm (m+n) by A39,XREAL_1:6,NAT_1:44;
A43: III.(n+k+wnk) = (Inm/^n).wnk by A40,A26,A27,AFINSQ_1:def 3
.=Inm.(n+wnk) by A41,AFINSQ_2:def 2
.=I.(n+wnk) by A42,FUNCT_1:49
.=n+wnk by A42,FUNCT_1:17;
r.(n+wnk) = @XY.(n+wnk) by A14,A42,AFINSQ_1:def 3
.= (@XY/^n).wnk by A40,A15,AFINSQ_2:def 2
.=@XanyY.(n+k+wnk) by A13,A16,A40,AFINSQ_2:def 2;
hence thesis by A43,A28,FUNCT_1:12,A21;
end;
end;
hence thesis by A20,A19,A21,AFINSQ_1:8;
end;
begin :: Diophantine Sets
reserve x,s for object;
definition
let D be non empty set;
let n be Nat;
func n -xtuples_of D -> Subset of D^omega means :Def5:
x in it iff x is n-element XFinSequence of D;
existence
proof
take X = the set of all x where x is n-element XFinSequence of D;
X c= D^omega
proof
let y be object;
assume y in X;
then ex x be n-element XFinSequence of D st y=x;
hence thesis by AFINSQ_1:def 7;
end;
hence X is Subset of D^omega;
let x;
thus x in X implies x is n-element XFinSequence of D
proof
assume x in X;
then ex y be n-element XFinSequence of D st x=y;
hence thesis;
end;
assume x is n-element XFinSequence of D;
hence thesis;
end;
uniqueness
proof
let X1,X2 be Subset of D^omega such that
A1: x in X1 iff x is n-element XFinSequence of D and
A2: x in X2 iff x is n-element XFinSequence of D;
now let x;
x in X1 iff x is n-element XFinSequence of D by A1;
hence x in X1 iff x in X2 by A2;
end;
hence thesis by TARSKI:2;
end;
end;
registration
let D be non empty set;
let n be Nat;
cluster n -xtuples_of D -> non empty;
coherence
proof
the n-element XFinSequence of D in n -xtuples_of D by Def5;
hence thesis;
end;
cluster -> n-element D-valued for Element of n -xtuples_of D;
coherence by Def5;
end;
definition
let n be Nat;
let A be Subset of n -xtuples_of NAT;
attr A is diophantine means :Def6:
ex m being Nat, p being INT -valued Polynomial of n+m,F_Real st
for s holds
s in A iff ex x being n-element XFinSequence of NAT,
y being m-element XFinSequence of NAT st
s = x & eval(p,@(x^y)) = 0;
end;
registration
let n be Nat;
cluster empty -> diophantine for Subset of n-xtuples_of NAT;
coherence
proof
let A be Subset of n-xtuples_of NAT;
assume A1: A is empty;
reconsider p=1_(n+0, F_Real) as INT -valued Polynomial of n+0,F_Real;
take 0,p;
let s;
thus s in A implies ex x be n-element XFinSequence of NAT,
y be 0-element XFinSequence of NAT st s=x & eval(p,@(x^y)) = 0 by A1;
given x be n-element XFinSequence of NAT,
y be 0-element XFinSequence of NAT such that
A2: s=x & eval(p,@(x^y)) = 0;
eval(p,@(x^y)) = 1. F_Real by POLYNOM2:21
.= 1;
hence thesis by A2;
end;
cluster [#](n-xtuples_of NAT) -> diophantine;
coherence
proof
reconsider p=0_(n+0, F_Real) as INT -valued Polynomial of n+0,F_Real;
set ALL= [#](n-xtuples_of NAT);
take 0,p;
let s;
thus s in ALL implies ex x be n-element XFinSequence of NAT,
y be 0-element XFinSequence of NAT st
s=x & eval(p,@(x^y)) = 0
proof
assume s in ALL;
then reconsider x=s as n-element NAT-valued XFinSequence;
set y = the 0-element XFinSequence of NAT;
eval(p,@(x^y)) = 0.F_Real by POLYNOM2:20
.= 0;
hence thesis;
end;
given x be n-element XFinSequence of NAT,
y be 0-element XFinSequence of NAT such that
A3: s=x & eval(p,@(x^y)) = 0;
thus thesis by A3,Def5;
end;
end;
registration
let n be zero Nat;
cluster -> diophantine for Subset of n -xtuples_of NAT;
coherence
proof
let S be Subset of n -xtuples_of NAT;
per cases;
suppose S={};
hence thesis;
end;
suppose S<>0;
then consider x such that
A1: x in S by XBOOLE_0:def 1;
reconsider x as n-element XFinSequence of NAT by A1;
n -xtuples_of NAT c= S by A1;
then [#](n-xtuples_of NAT) = S by XBOOLE_0:def 10;
hence thesis;
end;
end;
end;
registration
let n be Nat;
cluster non empty diophantine for Subset of n-xtuples_of NAT;
existence
proof
take [#](n-xtuples_of NAT);
thus thesis;
end;
cluster empty diophantine for Subset of n-xtuples_of NAT;
existence
proof
take {}(n-xtuples_of NAT);
thus thesis;
end;
end;
registration
let n be Nat;
let A,B be diophantine Subset of n -xtuples_of NAT;
cluster A /\ B -> diophantine for Subset of n -xtuples_of NAT;
coherence
proof
consider nA be Nat, pA be INT -valued Polynomial of n+nA,F_Real such that
A1: for s holds
s in A iff ex x be n-element XFinSequence of NAT,
y be nA-element XFinSequence of NAT st
s=x & eval(pA,@(x^y)) = 0 by Def6;
consider nB be Nat, pB be INT -valued Polynomial of n+nB,F_Real such that
A2: for s holds
s in B iff ex x be n-element XFinSequence of NAT,
y be nB-element XFinSequence of NAT st
s=x & eval(pB,@(x^y)) = 0 by Def6;
A /\ B is diophantine
proof
take N=nA+nB;
consider qA be Polynomial of n+nA+nB,F_Real such that
A3: rng qA c= rng pA \/{0.F_Real} and
A4: for x be Function of n+nA, F_Real,
y be Function of n+nA+nB, F_Real st y|(n+nA)=x
holds eval(pA,x) = eval(qA,y) by Th27;
rng qA c= INT by A3,INT_1:def 2;
then reconsider qA as INT -valued Polynomial of n+N,F_Real
by RELAT_1:def 19;
consider qB be Polynomial of n+nA+nB,F_Real such that
A5: rng qB c= rng pB \/ {0.F_Real}and
A6: for XY be Function of n+nB,F_Real,
XanyY be Function of n+nA+nB,F_Real st XY|n = XanyY|n &
@XY/^n = @XanyY/^(n+nA)
holds eval(pB,XY) = eval(qB,XanyY) by Th28;
rng qB c= INT by A5,INT_1:def 2;
then reconsider qB as INT -valued Polynomial of n+N,F_Real
by RELAT_1:def 19;
take Q =qA *' qA + qB *' qB;
let y be object;
thus y in A/\B implies ex x be n-element XFinSequence of NAT,
y1 be N-element XFinSequence of NAT st y=x & eval(Q,@(x^y1)) = 0
proof
assume
A7: y in A/\B;
then y in A by XBOOLE_0:def 4;
then consider xA be n-element XFinSequence of NAT,
yA be nA-element XFinSequence of NAT such that
A8: y=xA & eval(pA,@(xA^yA)) = 0 by A1;
y in B by A7,XBOOLE_0:def 4;
then consider xB be n-element XFinSequence of NAT,
yB be nB-element XFinSequence of NAT such that
A9: y=xB & eval(pB,@(xB^yB)) = 0 by A2;
reconsider X=@(xA^yA^yB) as Function of n+N,F_Real;
A10: len (xA^yA) = n+nA by CARD_1:def 7;
then (xA^yA^yB)|(n+nA) = xA^yA by AFINSQ_1:57;
then
A11: eval(qA,X) = 0 by A8,A4;
A12: X = xA^(yA^yB) by AFINSQ_1:27;
A13: len xA = n by CARD_1:def 7;
then
A14: @@(xA^yB)|n = xA & X|n = xA by A12,AFINSQ_1:57;
@X /^ (n+nA) = yB & @@(xA^yB)/^n = yB by A10,A13,AFINSQ_2:12;
then
A15: eval(qB,X) = 0 by A8,A9,A14,A6;
reconsider Y = @@(yA^yB) as N-element XFinSequence of NAT;
A16: eval(qA *' qA,@(xA^Y))=eval(qA,@(xA^Y))*eval(qA,@(xA^Y))
by POLYNOM2:25
.= 0*0 by A11,A12;
A17: eval(qB *' qB,@(xA^Y))=eval(qB,@(xA^Y))*eval(qB,@(xA^Y))
by POLYNOM2:25
.= 0*0 by A15,A12;
eval(Q,@(xA^Y)) = eval(qA *' qA,@(xA^Y))+eval(qB *' qB,@(xA^Y))
by POLYNOM2:23
.= 0 by A16,A17;
hence thesis by A8;
end;
given xA be n-element XFinSequence of NAT,
y1 be N-element XFinSequence of NAT such that
A18: xA=y& eval(Q,@(xA^y1)) = 0;
reconsider yA = y1|nA,yB=y1/^nA as XFinSequence of NAT;
A19: nA<= nA+nB & len y1 = nA+nB by NAT_1:11,CARD_1:def 7;
then len yA = nA by AFINSQ_1:54;
then reconsider yA as nA-element XFinSequence of NAT by CARD_1:def 7;
len yB = nA+nB-'nA by A19,AFINSQ_2:def 2
.= nB by NAT_D:34;
then reconsider yB as nB-element XFinSequence of NAT by CARD_1:def 7;
reconsider X=@(xA^yA^yB) as Function of n+N,F_Real;
A21: len (xA^yA) = n+nA by CARD_1:def 7;
then (xA^yA^yB)|(n+nA) = xA^yA by AFINSQ_1:57;
then
A22: eval(pA,@(xA^yA)) = eval(qA,X) by A4;
A23: X = xA^(yA^yB) by AFINSQ_1:27;
A24: len xA = n by CARD_1:def 7;
then
A25: @@(xA^yB)|n = xA & X|n = xA by A23,AFINSQ_1:57;
@X /^ (n+nA) = yB & @@(xA^yB)/^n = yB by A21,A24,AFINSQ_2:12;
then
A26: eval(pB,@(xA^yB)) = eval(qB,X) by A25,A6;
reconsider eA=eval(qA,@(xA^y1)) as Integer by INT_1:def 2;
reconsider eB=eval(qB,@(xA^y1)) as Integer by INT_1:def 2;
reconsider eAA=eA*eA,eBB=eB*eB as Element of NAT by INT_1:3,XREAL_1:63;
A27: eval(qA *' qA,@(xA^y1))=eval(qA,@(xA^y1))*eval(qA,@(xA^y1))
by POLYNOM2:25
.= eAA;
A28: eval(qB *' qB,@(xA^y1))=eval(qB,@(xA^y1))*eval(qB,@(xA^y1))
by POLYNOM2:25
.= eBB;
eval(Q,@(xA^y1)) = eval(qA *' qA,@(xA^y1))+eval(qB *' qB,@(xA^y1))
by POLYNOM2:23
.= eAA+eBB by A27,A28;
then eAA = 0 & eBB = 0 by A18;
then
A29: eA= 0 & eB = 0 by XCMPLX_1:6;
then
A30: xA in A by A1,A22,A23;
xA in B by A2,A29,A26,A23;
hence thesis by A18,A30,XBOOLE_0:def 4;
end;
hence thesis;
end;
cluster A \/ B -> diophantine for Subset of n -xtuples_of NAT;
coherence
proof
consider nA be Nat, pA be INT -valued Polynomial of n+nA,F_Real such that
A31: for s holds s in A iff ex x be n-element XFinSequence of NAT,
y be nA-element XFinSequence of NAT st
s=x & eval(pA,@(x^y)) = 0 by Def6;
consider nB be Nat, pB be INT -valued Polynomial of n+nB,F_Real such that
A32: for s holds
s in B iff ex x be n-element XFinSequence of NAT,
y be nB-element XFinSequence of NAT st s=x & eval(pB,@(x^y)) = 0 by Def6;
A\/B is diophantine
proof
take N=nA+nB;
consider qA be Polynomial of n+nA+nB,F_Real such that
A33: rng qA c= rng pA \/{0.F_Real} and
A34: for x be Function of n+nA, F_Real,
y be Function of n+nA+nB, F_Real st y|(n+nA)=x
holds eval(pA,x) = eval(qA,y) by Th27;
rng qA c= INT by A33,INT_1:def 2;
then reconsider qA as INT -valued Polynomial of n+N,F_Real
by RELAT_1:def 19;
consider qB be Polynomial of n+nA+nB,F_Real such that
A35: rng qB c= rng pB \/ {0.F_Real}and
A36: for XY be Function of n+nB,F_Real,
XanyY be Function of n+nA+nB,F_Real st XY|n = XanyY|n &
@XY/^n = @XanyY/^(n+nA)
holds eval(pB,XY) = eval(qB,XanyY) by Th28;
rng qB c= INT by A35,INT_1:def 2;
then reconsider qB as INT -valued Polynomial of n+N,F_Real
by RELAT_1:def 19;
take Q =qA *' qB;
let y be object;
thus y in A\/B implies ex x be n-element XFinSequence of NAT,
y1 be N-element XFinSequence of NAT st y=x & eval(Q,@(x^y1)) = 0
proof
assume y in A \/ B; then
per cases by XBOOLE_0:def 3;
suppose y in A;
then consider xA be n-element XFinSequence of NAT,
yA be nA-element XFinSequence of NAT such that
A38: y=xA & eval(pA,@(xA^yA)) = 0 by A31;
set yB= the nB-element XFinSequence of NAT;
reconsider X=@(xA^yA^yB) as Function of n+N,F_Real;
len (xA^yA) = n+nA by CARD_1:def 7;
then (xA^yA^yB)|(n+nA) = xA^yA by AFINSQ_1:57;
then
A39: eval(qA,X) = 0 by A38,A34;
reconsider Y = @@(yA^yB) as N-element XFinSequence of NAT;
eval(Q,@(xA^Y)) = eval(qA,@(xA^Y))*eval(qB,@(xA^Y)) by POLYNOM2:25
.= 0*eval(qB,@(xA^Y)) by A39,AFINSQ_1:27;
hence thesis by A38;
end;
suppose y in B;
then consider xA be n-element XFinSequence of NAT,
yB be nB-element XFinSequence of NAT such that
A40: y=xA & eval(pB,@(xA^yB)) = 0 by A32;
set yA= the nA-element XFinSequence of NAT;
reconsider X=@(xA^yA^yB) as Function of n+N,F_Real;
A41: len (xA^yA) = n+nA by CARD_1:def 7;
A42: X = xA^(yA^yB) by AFINSQ_1:27;
A43: len xA = n by CARD_1:def 7;
then
A44: @@(xA^yB)|n = xA & X|n = xA by A42,AFINSQ_1:57;
A45: @X /^ (n+nA) = yB & @@(xA^yB)/^n = yB by A41,A43,AFINSQ_2:12;
reconsider Y = @@(yA^yB) as N-element XFinSequence of NAT;
eval(Q,@(xA^Y)) = eval(qA,@(xA^Y))*eval(qB,@(xA^Y)) by POLYNOM2:25
.= eval(qA,@(xA^Y))*0 by A45,A40,A44,A36,A42;
hence thesis by A40;
end;
end;
given xA be n-element XFinSequence of NAT,
y1 be N-element XFinSequence of NAT such that
A46: xA=y & eval(Q,@(xA^y1)) = 0;
reconsider yA = y1|nA,yB=y1/^nA as XFinSequence of NAT;
A47: nA<= nA+nB & len y1 = nA+nB by NAT_1:11,CARD_1:def 7;
then len yA = nA by AFINSQ_1:54;
then reconsider yA as nA-element
XFinSequence of NAT by CARD_1:def 7;
len yB = nA+nB-'nA by A47,AFINSQ_2:def 2
.= nB by NAT_D:34;
then reconsider yB as nB-element XFinSequence of NAT by CARD_1:def 7;
reconsider X=@(xA^yA^yB) as Function of n+N,F_Real;
A49: len (xA^yA) = n+nA by CARD_1:def 7;
then (xA^yA^yB)|(n+nA) = xA^yA by AFINSQ_1:57;
then
A50: eval(pA,@(xA^yA)) = eval(qA,X) by A34;
A51: X = xA^(yA^yB) by AFINSQ_1:27;
A52: len xA = n by CARD_1:def 7;
then
A53: @@(xA^yB)|n = xA & X|n = xA by A51,AFINSQ_1:57;
@X /^ (n+nA) = yB & @@(xA^yB)/^n = yB by A49,A52,AFINSQ_2:12;
then
A54: eval(pB,@(xA^yB)) = eval(qB,X) by A53,A36;
reconsider eA=eval(qA,@(xA^y1)) as Integer by INT_1:def 2;
reconsider eB=eval(qB,@(xA^y1)) as Integer by INT_1:def 2;
eval(Q,@(xA^y1)) = eval(qA,@(xA^y1))*eval(qB,@(xA^y1)) by POLYNOM2:25
.= eA*eB;
then eA= 0 or eB = 0 by A46,XCMPLX_1:6;
then xA in A or xA in B by A31,A32,A54,A50,A51;
hence thesis by A46,XBOOLE_0:def 3;
end;
hence thesis;
end;
end;