Copyright (c) 2001 Association of Mizar Users
environ
vocabulary ORDINAL1, VECTSP_1, QUOFIELD, FUNCT_1, RELAT_1, SUBSET_1, WELLORD1,
ORDINAL2, BOOLE, ORDINAL3, POLYNOM1, PBOOLE, SEQM_3, ALGSEQ_1, FINSET_1,
FUNCOP_1, RLVECT_1, LATTICES, BINOP_1, ARYTM_3, FINSEQ_1, FINSEQ_4,
FINSEQ_2, GROUP_1, REALSET1, TARSKI, DTCONSTR, MATRIX_2, ORDERS_2,
CARD_1, ARYTM_1, TRIANG_1, VECTSP_2, PRE_TOPC, GRCAT_1, COHSP_1, PRALG_1,
ENDALG, POLYNOM6;
notation TARSKI, XBOOLE_0, SUBSET_1, NUMBERS, XCMPLX_0, XREAL_0, VECTSP_1,
RELAT_1, FUNCT_1, FUNCT_2, FUNCOP_1, STRUCT_0, NAT_1, TRIANG_1, ORDERS_2,
PBOOLE, PRE_TOPC, PRALG_1, RLVECT_1, VECTSP_2, FINSET_1, FINSEQ_1,
FINSEQ_2, FINSEQ_4, SEQM_3, BINARITH, DTCONSTR, ORDINAL1, ORDINAL2,
ORDINAL3, GROUP_1, REALSET1, QUOFIELD, GRCAT_1, ENDALG, WSIERP_1,
MATRLIN, TOPREAL1, FVSUM_1, POLYNOM1, POLYNOM3;
constructors POLYNOM1, ALGSTR_2, QUOFIELD, MONOID_0, GRCAT_1, ORDINAL3,
REAL_1, FVSUM_1, SETWOP_2, ENDALG, BINARITH, WSIERP_1, ORDERS_2,
TOPREAL1, TRIANG_1, FINSOP_1, POLYNOM3, MEMBERED;
clusters XREAL_0, STRUCT_0, FUNCT_1, FINSET_1, RELSET_1, FINSEQ_1, FINSEQ_2,
PRALG_1, ARYTM_3, POLYNOM2, GOBRD13, POLYNOM1, QUOFIELD, WAYBEL10,
VECTSP_1, MEMBERED, NUMBERS, ORDINAL2;
requirements BOOLE, SUBSET, NUMERALS, REAL;
definitions ANPROJ_1, VECTSP_1, QUOFIELD, GRCAT_1, ENDALG, FUNCT_1, SEQM_3,
TARSKI, XBOOLE_0;
theorems POLYNOM1, QUOFIELD, TOPGRP_1, PRE_TOPC, FUNCT_2, PBOOLE, FUNCT_1,
ORDINAL3, ORDINAL1, ORDINAL2, FINSEQ_3, FINSEQ_2, FVSUM_1, GROUP_7,
FINSEQ_1, RELAT_1, FUNCOP_1, POLYALG1, SCMFSA_7, DTCONSTR, FINSEQ_5,
VECTSP_1, FINSEQ_4, SEQM_3, FINSET_1, TARSKI, ENDALG, POLYNOM2, PRALG_1,
RELSET_1, MATRLIN, RLVECT_1, NAT_1, SUBSET_1, CARD_3, POLYNOM3, TRIANG_1,
ORDERS_2, AXIOMS, JORDAN3, REAL_1, RVSUM_1, AMI_5, XBOOLE_0, XBOOLE_1;
schemes MSUALG_1, FUNCT_2, FRAENKEL, POLYNOM2, FUNCT_1;
begin :: Preliminaries
reserve o1,o2 for Ordinal;
definition let L1,L2 be non empty doubleLoopStr;
redefine pred L1 is_ringisomorph_to L2;
reflexivity
proof
let L1 be non empty doubleLoopStr;
take id L1;
thus id L1 is RingHomomorphism;
thus id L1 is one-to-one;
thus id L1 is RingHomomorphism;
thus rng id L1 = [#]L1 by TOPGRP_1:1
.= the carrier of L1 by PRE_TOPC:12;
end;
synonym L1,L2 are_isomorphic;
end;
theorem Th1:
for B be set st
for x be set holds x in B iff
ex o be Ordinal st x=o1+^o & o in o2
holds o1+^o2 = o1 \/ B
proof
let B be set;
assume A1: for x be set holds x in B iff
ex o be Ordinal st x=o1+^o & o in o2;
for x be set holds x in o1+^o2 iff x in o1 \/ B
proof
let x be set;
A2: x in o1 \/ B implies x in o1+^o2
proof
assume A3:x in o1 \/ B;
per cases by A3,XBOOLE_0:def 2;
suppose A4: x in o1;
o1 c= o1+^o2 by ORDINAL3:27;
hence x in o1+^o2 by A4;
suppose x in B;
then consider o be Ordinal such that
A5: x=o1+^o and
A6: o in o2 by A1;
thus x in o1+^o2 by A5,A6,ORDINAL2:49;
end;
per cases;
suppose x in o1;
hence x in o1+^o2 implies x in o1 \/ B by XBOOLE_0:def 2;
thus x in o1 \/ B implies x in o1+^o2 by A2;
suppose A7: not x in o1;
thus x in o1+^o2 implies x in o1 \/ B
proof
assume
A8: x in o1+^o2;
per cases;
suppose o2 = {};
hence thesis by A7,A8,ORDINAL2:44;
suppose A9: o2 <> {};
reconsider o = x as Ordinal by A8,ORDINAL1:23;
o1 c= o by A7,ORDINAL1:26;
then A10: o = o1 +^ (o -^ o1) by ORDINAL3:def 6;
o -^ o1 in o2 by A8,A9,ORDINAL3:73;
then x in B by A1,A10;
hence x in o1 \/ B by XBOOLE_0:def 2;
end;
thus x in o1 \/ B implies x in o1+^o2 by A2;
end;
hence o1+^o2 = o1 \/ B by TARSKI:2;
end;
definition let o1 be Ordinal, o2 be non empty Ordinal;
cluster o1 +^ o2 -> non empty;
coherence by ORDINAL3:29;
cluster o2 +^ o1 -> non empty;
coherence by ORDINAL3:29;
end;
theorem Th2:
for n being Ordinal, a,b being bag of n st a < b
ex o being Ordinal st
o in n & a.o < b.o &
for l being Ordinal st l in o holds a.l = b.l
proof
let n be Ordinal, a,b be bag of n;
assume a < b;
then consider o being Ordinal such that
A1: a.o < b.o and
A2: for l being Ordinal st l in o holds a.l = b.l by POLYNOM1:def 11;
take o;
now assume
A3: not o in n;
n = dom a by PBOOLE:def 3;
then A4: a.o = 0 by A3,FUNCT_1:def 4;
not o in dom b by A3,PBOOLE:def 3;
hence contradiction by A1,A4,FUNCT_1:def 4;
end;
hence o in n;
thus a.o < b.o by A1;
thus for l being Ordinal st l in o holds a.l = b.l by A2;
end;
begin ::About Bags
definition
let o1,o2 be Ordinal;
let a be Element of Bags o1,b be Element of Bags o2;
func a +^ b -> Element of Bags (o1+^o2) means :Def1:
for o be Ordinal holds
(o in o1 implies it.o = a.o) &
(o in (o1+^o2) \ o1 implies it.o=b.(o-^o1));
existence
proof
per cases;
suppose
A1: o2 = {};
then A2: o1+^o2 = o1 by ORDINAL2:44;
reconsider a'=a as Element of Bags (o1+^o2) by A1,ORDINAL2:44;
take a';
let o be Ordinal;
thus o in o1 implies a'.o = a.o;
thus o in (o1+^o2) \ o1 implies a'.o=b.(o-^o1) by A2,XBOOLE_1:37;
suppose o2 <> {};
then reconsider o2' = o2 as non empty Ordinal;
defpred P[set,set] means
ex o be Ordinal st o=$1 &
(o in o1 implies $2 = a.o) &
(o in (o1+^o2) \ o1 implies $2=b.(o-^o1));
A3: for i be set st i in o1+^o2 ex j be set st P[i,j]
proof
let i be set such that A4: i in o1+^o2;
reconsider o = i as Ordinal by A4,ORDINAL1:23;
A5: o in o1 iff not o in (o1+^ o2)\o1 by A4,XBOOLE_0:def 4;
per cases by A4,XBOOLE_0:def 4;
suppose A6: o in o1;
take a.o,o;
thus thesis by A6,XBOOLE_0:def 4;
suppose A7: o in (o1 +^o2)\o1;
take b.(o -^o1);
thus thesis by A5,A7;
end;
consider f being ManySortedSet of o1+^o2 such that
A8: for i be set st i in o1+^o2 holds P[i,f.i] from MSSEx(A3);
A9: f is natural-yielding
proof
let s be set;
assume s in rng f;
then consider x be set such that A10: x in dom f
and A11: s = f.x by FUNCT_1:def 5;
A12: x in o1+^o2 by A10,PBOOLE:def 3;
then reconsider o = x as Ordinal by ORDINAL1:23;
consider o' be Ordinal such that A13: o'=x &
(o' in o1 implies f.x = a.o') &
(o' in (o1+^o2) \ o1 implies f.x=b.(o'-^o1)) by A8,A12;
per cases by A12,XBOOLE_0:def 4;
suppose o in o1;
hence thesis by A11,A13;
suppose o in (o1 +^o2)\o1;
hence thesis by A11,A13;
end;
deffunc F(Element of o2') = o1 +^ $1;
set B = {F(o) where o is Element of o2': o in support b},
C = {o1 +^ o where o is Element of o2': not contradiction};
A14: support f c= support a \/ B
proof
let x be set;
assume x in support f;
then A15: f.x <> 0 by POLYNOM1:def 7;
then x in dom f by FUNCT_1:def 4;
then A16: x in o1+^o2 by PBOOLE:def 3;
for x be set holds x in C iff ex o be Ordinal st x=o1+^o & o in o2
proof
let x be set;
thus x in C implies ex o be Ordinal st x=o1+^o & o in o2
proof
assume x in C;
then ex o' be Element of o2' st x = o1 +^ o';
hence ex o be Ordinal st x=o1+^o & o in o2;
end;
thus thesis;
end;
then A17:x in o1 \/ C by A16,Th1;
per cases by A17,XBOOLE_0:def 2;
suppose A18: x in o1;
P[x,f.x] by A8,A16;
then x in support a by A15,A18,POLYNOM1:def 7;
hence thesis by XBOOLE_0:def 2;
suppose x in C;
then ex o' be Element of o2' st x = o1 +^ o';
then consider o'' be Ordinal such that
A19: x=o1+^o'' & o'' in o2;
A20: x in o1+^o2 by A19,ORDINAL2:49;
reconsider o=x as Ordinal by A19;
A21: o1 c= o by A19,ORDINAL3:27;
A22: o1 is epsilon-transitive set by ORDINAL1:def 4;
A23: now per cases;
suppose o = o1;
hence not o in o1;
suppose o <> o1;
then o1 c< o by A21,XBOOLE_0:def 8;
hence not o in o1 by A22,ORDINAL1:21;
end;
A24: P[x,f.x] by A8,A16;
o'' = o-^o1 by A19,ORDINAL3:65;
then o'' in support b by A15,A20,A23,A24,POLYNOM1:def 7,XBOOLE_0:def 4;
then x in B by A19;
hence thesis by XBOOLE_0:def 2;
end;
A25: support b is finite;
B is finite from FraenkelFin(A25);
then support a \/ B is finite by FINSET_1:14;
then support f is finite by A14,FINSET_1:13;
then f is finite-support by POLYNOM1:def 8;
then reconsider f as Element of Bags (o1+^o2) by A9,POLYNOM1:def 14;
take f;
let o be Ordinal;
thus o in o1 implies f.o = a.o
proof
assume A26: o in o1;
o1 c= o1 +^ o2 by ORDINAL3:27;
then ex p be Ordinal st p=o &
(p in o1 implies f.o = a.p) &
(p in (o1+^o2) \ o1 implies f.o=b.(p-^o1)) by A8,A26;
hence f.o = a.o by A26;
end;
assume A27: o in (o1+^o2) \ o1;
then o in o1 +^ o2 by XBOOLE_0:def 4;
then ex p be Ordinal st p=o &
(p in o1 implies f.o = a.p) &
(p in (o1+^o2) \ o1 implies f.o=b.(p-^o1)) by A8;
hence f.o=b.(o-^o1) by A27;
end;
uniqueness
proof
let a1,a2 be Element of Bags (o1+^o2) such that
A28: for o be Ordinal holds
(o in o1 implies a1.o = a.o) &
(o in (o1+^o2) \ o1 implies a1.o=b.(o-^o1)) and
A29: for o be Ordinal holds
(o in o1 implies a2.o = a.o) &
(o in (o1+^o2) \ o1 implies a2.o=b.(o-^o1));
A30: dom a1 = o1+^o2 by PBOOLE:def 3;
then A31: dom a1 = dom a2 by PBOOLE:def 3;
for c be set st c in dom a1 holds a1.c = a2.c
proof
let c be set such that
A32: c in dom a1;
reconsider o=c as Ordinal by A30,A32,ORDINAL1:23;
A33: o1 c= o1+^o2 by ORDINAL3:27;
A34: (o1+^o2)\o1 \/ o1 = (o1+^o2) \/ o1 by XBOOLE_1:39
.=o1+^o2 by A33,XBOOLE_1:12;
per cases by A30,A32,A34,XBOOLE_0:def 2;
suppose
A35: o in o1;
hence a1.c =a.o by A28
.=a2.c by A29,A35;
suppose
A36: o in (o1+^o2) \o1;
hence a1.c =b.(o-^o1) by A28
.=a2.c by A29,A36;
end;
hence a1 = a2 by A31,FUNCT_1:9;
end;
end;
theorem Th3:
for a be Element of Bags o1,b be Element of Bags o2 st
o2 = {} holds
a +^ b = a
proof
let a be Element of Bags o1,b be Element of Bags o2;
assume o2={};
then reconsider ab = a +^ b as Element of Bags o1 by ORDINAL2:44;
now let i be set;
assume A1:i in o1;
then reconsider i'=i as Ordinal by ORDINAL1:23;
ab.i'=a.i' by A1,Def1;
hence ab.i = a.i;
end;
hence a +^ b = a by PBOOLE:3;
end;
theorem
for a be Element of Bags o1,b be Element of Bags o2 st
o1 = {} holds
a +^ b = b
proof
let a be Element of Bags o1,b be Element of Bags o2;
assume A1:o1={};
then reconsider ab = a +^ b as Element of Bags o2 by ORDINAL2:47;
now let i be set;
assume A2:i in o2;
then A3: i in (o1+^o2) \ o1 by A1,ORDINAL2:47;
reconsider i'=i as Ordinal by A2,ORDINAL1:23;
i'-^o1 = i' by A1,ORDINAL3:69;
hence ab.i = b.i by A3,Def1;
end;
hence a +^ b = b by PBOOLE:3;
end;
theorem Th5:
for b1 be Element of Bags o1 ,b2 be Element of Bags o2 holds
b1+^b2 = EmptyBag(o1+^o2) iff b1 = EmptyBag o1 & b2 = EmptyBag o2
proof
let b1 be Element of Bags o1 ,b2 be Element of Bags o2;
hereby assume A1: b1+^b2 = EmptyBag (o1+^o2);
A2: for z be set st z in dom b1 holds b1.z = 0
proof
let z be set;
assume A3: z in dom b1;
A4: dom b1 = o1 by PBOOLE:def 3;
then reconsider o=z as Ordinal by A3,ORDINAL1:23;
b1.o = (b1+^b2).o by A3,A4,Def1
.= 0 by A1,POLYNOM1:56;
hence b1.z = 0;
end;
dom b1 = o1 by PBOOLE:def 3;
then b1 = o1 --> 0 by A2,FUNCOP_1:17;
hence b1=EmptyBag o1 by POLYNOM1:def 15;
A5:for z be set st z in dom b2 holds b2.z = 0
proof
let z be set;
assume A6: z in dom b2;
A7: dom b2 = o2 by PBOOLE:def 3;
then reconsider o=z as Ordinal by A6,ORDINAL1:23;
A8: o1+^o in o1+^o2 by A6,A7,ORDINAL2:49;
o1 c= o1+^o by ORDINAL3:27;
then not o1+^o in o1 by ORDINAL1:7;
then o1+^o in (o1+^o2) \ o1 by A8,XBOOLE_0:def 4;
then (b1+^b2).(o1+^o) = b2.(o1+^o-^o1) &
(b1+^b2).(o1+^o) = b2.(o1+^o-^o1) by Def1;
then b2.(o1+^o-^o1) = 0 by A1,POLYNOM1:56;
hence b2.z = 0 by ORDINAL3:65;
end;
dom b2 = o2 by PBOOLE:def 3;
then b2 = o2 --> 0 by A5,FUNCOP_1:17;
hence b2=EmptyBag o2 by POLYNOM1:def 15;
end;
thus b1 = EmptyBag o1 & b2 = EmptyBag o2 implies b1+^b2 = EmptyBag(o1+^o2)
proof
assume A9: b1 = EmptyBag o1 & b2 = EmptyBag o2;
A10: for z be set st z in dom (b1+^b2) holds (b1+^b2).z = 0
proof
let z be set;
assume A11:z in dom (b1+^b2);
A12: dom (b1+^b2) = o1+^o2 by PBOOLE:def 3;
then reconsider o=z as Ordinal by A11,ORDINAL1:23;
(o in o1 implies b1.o = 0 & (b1+^b2).o=b1.o) &
(o in (o1+^o2) \ o1 implies b2.(o-^o1) = 0 & (b1+^b2).o=b2.(o-^o1))
by A9,Def1,POLYNOM1:56;
hence (b1+^b2).z = 0 by A11,A12,XBOOLE_0:def 4;
end;
dom (b1+^b2) = o1+^o2 by PBOOLE:def 3;
then b1+^b2 = (o1+^o2) --> 0 by A10,FUNCOP_1:17;
hence b1+^b2 = EmptyBag(o1+^o2) by POLYNOM1:def 15;
end;
end;
theorem Th6:
for c be Element of Bags (o1+^o2)
ex c1 be Element of Bags o1, c2 be Element of Bags o2
st c = c1+^c2
proof
let c be Element of Bags (o1+^o2);
per cases;
suppose
A1: o2 is empty;
then reconsider c1=c as Element of Bags o1 by ORDINAL2:44;
take c1;
reconsider c2={} as Element of Bags o2 by A1,POLYNOM1:55,TARSKI:def 1;
take c2;
thus c = c1+^c2 by A1,Th3;
suppose
A2: o2 is non empty;
then reconsider o2' = o2 as non empty Ordinal;
A3: c|o1 is natural-yielding
proof
let y be set;
assume A4: y in rng (c|o1);
rng(c|o1) c= rng c by RELAT_1:99;
then A5: y in rng c by A4;
rng c c= NAT by SEQM_3:def 8;
hence y in NAT by A5;
end;
support c|o1 c= support c
proof
let x be set;
assume x in support c|o1;
then A6: (c|o1).x <> 0 by POLYNOM1:def 7;
then x in dom (c|o1) by FUNCT_1:def 4;
then [x,(c|o1.x)] in c|o1 by FUNCT_1:8;
then [x,(c|o1).x] in c by RELAT_1:def 11;
then c|o1.x = c.x by FUNCT_1:8;
hence x in support c by A6,POLYNOM1:def 7;
end;
then A7: support c|o1 is finite by FINSET_1:13;
dom c = o1+^o2 by PBOOLE:def 3;
then o1 c= dom c by ORDINAL3:27;
then dom (c|o1) = o1 by RELAT_1:91;
then c|o1 is bag of o1 by A3,A7,PBOOLE:def 3,POLYNOM1:def 8;
then reconsider c1=c|o1 as Element of Bags o1 by POLYNOM1:def 14;
take c1;
defpred P[set,set] means for x1 be Element of o2 st x1=$1 holds $2=c.(o1+^x1);
A8: for i be set st i in o2 ex j be set st P[i,j]
proof
let i be set;
assume i in o2;
then reconsider x1=i as Element of o2;
take c.(o1+^x1);
thus thesis;
end;
consider f being ManySortedSet of o2 such that
A9: for i be set st i in o2 holds P[i,f.i] from MSSEx(A8);
A10: f is natural-yielding
proof
let s be set;
assume s in rng f;
then consider x be set such that A11: x in dom f
and A12: s = f.x by FUNCT_1:def 5;
A13: x in o2 by A11,PBOOLE:def 3;
reconsider o = x as Element of o2 by A11,PBOOLE:def 3;
f.x = c.(o1+^o) by A9,A13;
hence s in NAT by A12;
end;
deffunc F(Element of o1+^o2') = $1-^ o1;
set B = { o'-^ o1 where o' is Element of o1+^o2':o1 c= o'&
o' in support c},
C = {F(o') where o' is Element of o1+^o2':o' in support c};
A14: support c is finite;
A15: B c= C
proof let x be set;
assume x in B;
then ex o' being Element of o1+^o2' st
x = o' -^ o1 & o1 c= o'& o' in support c;
hence x in C;
end;
C is finite from FraenkelFin(A14);
then A16: B is finite by A15,FINSET_1:13;
support f = B
proof
thus support f c= B
proof
let x be set;
assume x in support f;
then A17: f.x <> 0 by POLYNOM1:def 7;
then x in dom f by FUNCT_1:def 4;
then reconsider o' = x as Element of o2' by PBOOLE:def 3;
c.(o1+^o')<>0 by A9,A17;
then A18: o1+^o' in support c by POLYNOM1:def 7;
reconsider o'' = o1+^o' as Element of o1+^o2' by ORDINAL2:49;
A19: o' = o''-^o1 by ORDINAL3:65;
o1 c= o'' by ORDINAL3:27;
hence x in B by A18,A19;
end;
thus B c= support f
proof
let x be set;
assume x in B;
then consider o' be Element of o1+^o2' such that
A20: x = o'-^o1 and
A21: o1 c= o' and
A22: o' in support c;
A23:c.o'<>0 by A22,POLYNOM1:def 7;
o'-^o1 in o1+^o2'-^o1 by A21,ORDINAL3:66;
then A24: o'-^o1 in o2' by ORDINAL3:65;
c.(o1+^(o'-^o1))<>0 by A21,A23,ORDINAL3:def 6;
then f.x <> 0 by A9,A20,A24;
hence x in support f by POLYNOM1:def 7;
end;
end;
then f is finite-support by A16,POLYNOM1:def 8;
then reconsider c2 = f as Element of Bags o2 by A10,POLYNOM1:def 14;
take c2;
now let i be set;
assume A25: i in o1+^o2;
per cases by A25,XBOOLE_0:def 4;
suppose A26:i in o1;
then reconsider i'=i as Ordinal by ORDINAL1:23;
dom c1 = o1 by PBOOLE:def 3;
then c.i' = c1.i' by A26,FUNCT_1:70
.= (c1+^c2).i' by A26,Def1;
hence c.i = (c1+^c2).i;
suppose A27:i in (o1+^o2)\o1;
then A28: i in o1+^o2 by XBOOLE_0:def 4;
then reconsider i'=i as Ordinal by ORDINAL1:23;
A29: i'-^o1 in o2 by A2,A28,ORDINAL3:73;
not i' in o1 by A27,XBOOLE_0:def 4;
then o1 c= i' by ORDINAL1:26;
then c.i' = c.(o1+^(i'-^o1)) by ORDINAL3:def 6
.= c2.(i'-^o1) by A9,A29
.= (c1+^c2).i' by A27,Def1;
hence c.i = (c1+^c2).i;
end;
hence c = c1+^c2 by PBOOLE:3;
end;
theorem Th7:
for b1,c1 be Element of Bags o1
for b2,c2 be Element of Bags o2
st b1+^b2 = c1+^c2 holds b1=c1 & b2=c2
proof
let b1,c1 be Element of Bags o1,
b2,c2 be Element of Bags o2;
assume A1:b1+^b2 = c1+^c2;
now let i be set;
assume
A2: i in o1;
then reconsider i' = i as Ordinal by ORDINAL1:23;
(b1+^b2).i' = b1.i' & (b1+^b2).i'=c1.i' by A1,A2,Def1;
hence b1.i=c1.i;
end;
hence b1 = c1 by PBOOLE:3;
now let i be set;
assume
A3: i in o2;
then reconsider i' = i as Ordinal by ORDINAL1:23;
A4: o1+^i' in o1+^o2 by A3,ORDINAL2:49;
o1 c= o1+^i' by ORDINAL3:27;
then not o1+^i' in o1 by ORDINAL1:7;
then o1+^i' in (o1+^o2) \ o1 by A4,XBOOLE_0:def 4;
then A5: (b1+^b2).(o1+^i') = b2.(o1+^i'-^o1) &
(b1+^b2).(o1+^i') = c2.(o1+^i'-^o1) by A1,Def1;
i'= o1+^i'-^o1 by ORDINAL3:65;
hence b2.i = c2.i by A5;
end;
hence b2 = c2 by PBOOLE:3;
end;
theorem Th8:
for n being Ordinal,
L being Abelian add-associative right_zeroed right_complementable
distributive associative (non empty doubleLoopStr),
p, q, r being Series of n, L
holds (p+q)*'r = p*'r+q*'r
proof let n be Ordinal,
L be Abelian add-associative right_zeroed right_complementable
distributive associative (non empty doubleLoopStr),
p, q, r be Series of n, L;
set cL = the carrier of L;
now let b be Element of Bags n;
consider s being FinSequence of cL such that
A1: ((p+q)*'r).b = Sum s and
A2: len s = len decomp b and
A3: for k being Nat st k in dom s
ex b1, b2 being bag of n st (decomp b)/.k = <*b1, b2*> &
s/.k = (p+q).b1*r.b2 by POLYNOM1:def 26;
consider t being FinSequence of cL such that
A4: (p*'r).b = Sum t and
A5: len t = len decomp b and
A6: for k being Nat st k in dom t
ex b1, b2 being bag of n st (decomp b)/.k = <*b1, b2*> &
t/.k = p.b1*r.b2 by POLYNOM1:def 26;
consider u being FinSequence of cL such that
A7: (q*'r).b = Sum u and
A8: len u = len decomp b and
A9: for k being Nat st k in dom u
ex b1, b2 being bag of n st (decomp b)/.k = <*b1, b2*> &
u/.k = q.b1*r.b2 by POLYNOM1:def 26;
reconsider S = s, t, u as Element of (len s)-tuples_on cL
by A2,A5,A8,FINSEQ_2:110;
A10: dom t = dom s & dom u = dom s by A2,A5,A8,FINSEQ_3:31;
then A11: dom (t+u) = dom s by POLYNOM1:5;
then A12: len (t+u) = len s by FINSEQ_3:31;
now let i be Nat; assume i in Seg len S;
then 1 <= i & i <= len s by FINSEQ_1:3;
then A13: i in dom s by FINSEQ_3:27;
then consider sb1, sb2 being bag of n such that
A14: (decomp b)/.i = <*sb1, sb2*> & s/.i = (p+q).sb1*r.sb2 by A3;
consider tb1, tb2 being bag of n such that
A15: (decomp b)/.i = <*tb1, tb2*> & t/.i = p.tb1*r.tb2
by A6,A10,A13;
consider ub1, ub2 being bag of n such that
A16: (decomp b)/.i = <*ub1, ub2*> & u/.i = q.ub1*r.ub2
by A9,A10,A13;
A17: sb1 = tb1 & sb1 = ub1 & sb2 = tb2 & sb2 = ub2
by A14,A15,A16,GROUP_7:2;
A18: s/.i = s.i & t/.i = t.i & u/.i = u.i
by A10,A13,FINSEQ_4:def 4;
hence s.i = (p.sb1+q.sb1)*r.sb2 by A14,POLYNOM1:def 21
.= p.sb1*r.sb2+q.sb1*r.sb2 by VECTSP_1:def 18
.= (t + u).i by A11,A13,A15,A16,A17,A18,FVSUM_1:21;
end;
then s = t + u by A12,FINSEQ_2:10;
hence ((p+q)*'r).b = Sum t + Sum u by A1,FVSUM_1:95
.= (p*'r+q*'r).b by A4,A7,POLYNOM1:def 21;
end;
hence (p+q)*'r = p*'r+q*'r by FUNCT_2:113;
end;
begin :: Main results
definition
let n be Ordinal,
L be right_zeroed Abelian add-associative right_complementable
unital distributive associative
non trivial (non empty doubleLoopStr);
cluster Polynom-Ring (n, L) -> non trivial distributive;
coherence
proof
thus Polynom-Ring (n, L) is non trivial
proof
take u=1_ Polynom-Ring (n,L);
A1: 0.L <> 1.L by POLYNOM1:27;
A2: 0.Polynom-Ring (n,L) = 0_(n,L) by POLYNOM1:def 27;
A3: 1_ (Polynom-Ring (n,L)) = 1_(n,L) by POLYNOM1:def 27;
0_(n,L).EmptyBag n = 0.L by POLYNOM1:81;
hence u <> 0.Polynom-Ring (n,L) by A1,A2,A3,POLYNOM1:84;
end;
thus Polynom-Ring (n, L) is distributive
proof
let x,y,z be Element of Polynom-Ring (n,L);
reconsider u=x,v=y,w=z as Polynomial of n,L by POLYNOM1:def 27;
reconsider x'=x,y'=y,z'=z as Element of Polynom-Ring (n,L)
;
A4: y'+z' = v+w by POLYNOM1:def 27;
A5: u*'v=x'*y' by POLYNOM1:def 27;
A6: u*'w=x'*z' by POLYNOM1:def 27;
thus x*(y+z) = u*'(v+w) by A4,POLYNOM1:def 27
.=u*'v+u*'w by POLYNOM1:85
.= x*y+x*z by A5,A6,POLYNOM1:def 27;
A7: y'+z' = v+w by POLYNOM1:def 27;
A8: v*'u=y'*x' by POLYNOM1:def 27;
A9: w*'u=z'*x' by POLYNOM1:def 27;
thus (y+z)*x = (v+w)*'u by A7,POLYNOM1:def 27
.= v*'u+w*'u by Th8
.= y*x+z*x by A8,A9,POLYNOM1:def 27;
end;
end;
end;
definition
let o1,o2 be non empty Ordinal, L be right_zeroed add-associative
right_complementable unital distributive
non trivial (non empty doubleLoopStr);
let P be Polynomial of o1,Polynom-Ring(o2,L);
func Compress P -> Polynomial of o1+^o2,L means :Def2:
for b be Element of Bags (o1+^o2)
ex b1 be Element of Bags o1,
b2 be Element of Bags o2,
Q1 be Polynomial of o2,L st
Q1 = P.b1 & b = b1+^b2 & it.b = Q1.b2;
existence
proof
defpred P[Element of Bags (o1+^o2),Element of L]
means
ex b1 be Element of Bags o1,
b2 be Element of Bags o2,
Q1 be Polynomial of o2,L st
Q1=P.b1 &
$1 = b1+^b2 &
$2=Q1.b2;
A1: for b being Element of Bags (o1+^o2)
ex u being Element of L st P[b,u]
proof
let b be Element of Bags (o1+^o2);
consider b1 be Element of Bags o1,
b2 be Element of Bags o2 such that
A2: b = b1+^b2 by Th6;
reconsider Q1=P.b1 as Polynomial of o2,L by POLYNOM1:def 27;
take Q1.b2,b1,b2,Q1;
thus thesis by A2;
end;
consider f being Function of Bags (o1+^o2),the carrier of L such that
A3: for b being Element of Bags (o1+^o2) holds P[b,f.b] from FuncExD(A1);
reconsider f as Series of o1+^o2, L;
deffunc F(Element of Bags o1) = { $1+^b2 where b2 is Element of Bags o2:
ex Q be Polynomial of o2,L st Q=P.$1 & b2 in Support Q};
set A={ F(b1) where b1 is Element of Bags o1: b1 in Support P };
A4: Support P is finite by POLYNOM1:def 10;
A5: A is finite from FraenkelFin(A4);
for B be set st B in A holds B is finite
proof
let B be set;
assume B in A;
then consider b1 being Element of Bags o1 such that
A6: B = {b1+^b2 where b2 is Element of Bags o2:
ex Q be Polynomial of o2,L st
Q=P.b1 & b2 in Support Q} and
b1 in Support P;
reconsider Q0 = P.b1 as Polynomial of o2,L by POLYNOM1:def 27;
deffunc F(Element of Bags o2) = b1+^$1;
set B0 = { F(b2) where b2 is Element of Bags o2: b2 in Support Q0};
A7: B = B0
proof
thus B c= B0
proof
let x be set;
assume x in B;
then consider b2 be Element of Bags o2 such that
A8: x = b1+^b2 and
A9: ex Q be Polynomial of o2,L st
Q=P.b1 & b2 in Support Q by A6;
consider Q be Polynomial of o2,L such that
A10: Q=P.b1 and
A11: b2 in Support Q by A9;
thus x in B0 by A8,A10,A11;
end;
thus B0 c= B
proof
let x be set;
assume x in B0;
then consider b2 be Element of Bags o2 such that
A12: x = b1+^b2 and
A13: b2 in Support Q0;
thus x in B by A6,A12,A13;
end;
end;
A14: Support Q0 is finite;
B0 is finite from FraenkelFin(A14);
hence B is finite by A7;
end;
then A15: union A is finite by A5,FINSET_1:25;
Support f = union A
proof
thus Support f c= union A
proof
let x be set;
assume A16: x in Support f;
then A17: f.x <> 0.L by POLYNOM1:def 9;
consider b1 be Element of Bags o1,b2 be Element of Bags o2
such that
A18: x = b1+^b2 by A16,Th6;
consider Y be set such that
A19: Y = {b1+^b2' where b2' is Element of Bags o2:
ex Q be Polynomial of o2,L st
Q=P.b1 & b2' in Support Q};
consider b1' be Element of Bags o1,
b2' be Element of Bags o2,
Q1 be Polynomial of o2,L such that
A20: Q1=P.b1' and
A21: b1+^b2 = b1'+^b2' and
A22: f.(b1+^b2)=Q1.b2' by A3;
A23: b1=b1' & b2=b2' by A21,Th7;
then b2 in Support Q1 by A17,A18,A22,POLYNOM1:def 9;
then A24: x in Y by A18,A19,A20,A23;
now
assume P.b1 = 0.Polynom-Ring(o2,L);
then Q1=0_(o2,L) by A20,A23,POLYNOM1:def 27;
hence contradiction by A17,A18,A22,POLYNOM1:81;
end;
then b1 in Support P by POLYNOM1:def 9;
then Y in A by A19;
hence x in union A by A24,TARSKI:def 4;
end;
let x be set;
assume x in union A;
then consider Y be set such that
A25: x in Y and
A26: Y in A by TARSKI:def 4;
consider b1 be Element of Bags o1 such that
A27: Y = {b1+^b2 where b2 is Element of Bags o2:
ex Q be Polynomial of o2,L st
Q=P.b1 & b2 in Support Q} and
b1 in Support P by A26;
consider b2 be Element of Bags o2 such that
A28: x = b1+^b2 and
A29: ex Q be Polynomial of o2,L st
Q=P.b1 & b2 in Support Q by A25,A27;
consider Q be Polynomial of o2,L such that
A30: Q=P.b1 and
A31: b2 in Support Q by A29;
A32: Q .b2 <> 0.L by A31,POLYNOM1:def 9;
consider b1' be Element of Bags o1,
b2' be Element of Bags o2,
Q1 be Polynomial of o2,L such that
A33: Q1 =P.b1' and
A34: b1+^b2 = b1'+^b2' and
A35: f.(b1+^b2)=Q1.b2' by A3;
A36: Q1=Q by A30,A33,A34,Th7;
f.(b1+^b2) = Q1.b2 by A34,A35,Th7;
hence x in Support f by A28,A32,A36,POLYNOM1:def 9;
end;
then reconsider f as Polynomial of o1+^o2,L by A15,POLYNOM1:def 10;
take f;
let b be Element of Bags (o1+^o2);
consider b1 be Element of Bags o1,
b2 be Element of Bags o2 such that
A37: b = b1+^b2 by Th6;
take b1,b2;
reconsider Q1=P.b1 as Polynomial of o2,L by POLYNOM1:def 27;
take Q1;
thus Q1=P.b1;
thus b = b1+^b2 by A37;
consider b1' be Element of Bags o1,
b2' be Element of Bags o2,
Q1' be Polynomial of o2,L such that
A38: Q1'=P.b1' and
A39: b = b1'+^b2' and
A40: f.b=Q1'.b2' by A3;
b1 = b1' & b2 = b2' by A37,A39,Th7;
hence f.b=Q1.b2 by A38,A40;
end;
uniqueness
proof
let w1,w2 be Polynomial of o1+^o2,L such that
A41: for b be Element of Bags (o1+^o2)
ex b1 be Element of Bags o1,
b2 be Element of Bags o2,
Q1 be Polynomial of o2,L st
Q1= P.b1 &
b = b1+^b2 &
w1.b=Q1.b2 and
A42: for b be Element of Bags (o1+^o2)
ex b1 be Element of Bags o1,
b2 be Element of Bags o2,
Q1 be Polynomial of o2,L st
Q1=P.b1 & b = b1+^b2 & w2.b=Q1.b2;
for c be Element of Bags(o1+^o2) holds w1.c = w2.c
proof
let c be Element of Bags(o1+^o2);
consider c1 be Element of Bags o1,c2 be Element of Bags o2,
Q1 be Polynomial of o2,L such that
A43: Q1= P.c1 and
A44: c = c1+^c2 and
A45: w1.c = Q1.c2 by A41;
consider d1 be Element of Bags o1,d2 be Element of Bags o2,
S1 be Polynomial of o2,L such that
A46: S1= P.d1 and
A47: c = d1+^d2 and
A48: w2.c = S1.d2 by A42;
c2 = d2 by A44,A47,Th7;
hence w1.c = w2.c by A43,A44,A45,A46,A47,A48,Th7;
end;
hence w1=w2 by FUNCT_2:113;
end;
end;
theorem Th9:
for b1,c1 being Element of Bags o1, b2,c2 being Element of Bags o2
st b1 divides c1 & b2 divides c2
holds b1 +^ b2 divides c1 +^ c2
proof
let b1,c1 be Element of Bags o1, b2,c2 be Element of Bags o2;
assume
A1: b1 divides c1 & b2 divides c2;
now let k be set;
assume
A2: k in o1+^o2;
reconsider b1' = b1,c1' = c1 as bag of o1;
A3: b1'.k <= c1'.k by A1,POLYNOM1:def 13;
per cases by A2,XBOOLE_0:def 4;
suppose A4: k in o1;
then reconsider k'=k as Ordinal by ORDINAL1:23;
(b1 +^ b2).k' = b1.k' by A4,Def1;
hence (b1 +^ b2).k <= (c1 +^ c2).k by A3,A4,Def1;
suppose A5: k in (o1+^ o2)\o1;
then k in (o1+^o2) by XBOOLE_0:def 4;
then reconsider k'=k as Ordinal by ORDINAL1:23;
A6: (b1 +^ b2).k' = b2.(k'-^o1) by A5,Def1;
(c1 +^ c2).k' = c2.(k'-^o1) by A5,Def1;
hence (b1 +^ b2).k <= (c1 +^ c2).k by A1,A6,POLYNOM1:def 13;
end;
hence b1 +^ b2 divides c1 +^ c2 by POLYNOM1:50;
end;
theorem Th10:
for b being bag of (o1+^o2),
b1 being Element of Bags o1, b2 being Element of Bags o2
st b divides b1 +^ b2
ex c1 being Element of Bags o1, c2 being Element of Bags o2
st c1 divides b1 & c2 divides b2 & b = c1 +^ c2
proof
let b be bag of (o1+^o2),
b1 be Element of Bags o1, b2 be Element of Bags o2;
assume
A1: b divides b1 +^ b2;
reconsider b'=b as Element of Bags (o1+^o2) by POLYNOM1:def 14;
consider c1 be Element of Bags o1, c2 be Element of Bags o2
such that
A2: b' = c1+^c2 by Th6;
reconsider c1'=c1,b1'=b1 as bag of o1;
reconsider c2'=c2,b2'=b2 as bag of o2;
A3: for k being set st k in o1 holds c1'.k <= b1'.k
proof
let k be set;
assume A4: k in o1;
A5: (c1+^c2).k <= (b1 +^ b2).k by A1,A2,POLYNOM1:def 13;
reconsider k'=k as Ordinal by A4,ORDINAL1:23;
(c1+^c2).k' = c1.k' by A4,Def1;
hence c1'.k <= b1'.k by A4,A5,Def1;
end;
A6: for k being set st k in o2 holds c2'.k <= b2'.k
proof
let k be set;
assume A7:k in o2;
then reconsider k'=k as Ordinal by ORDINAL1:23;
set x = o1+^k';
A8: (c1+^c2).x <= (b1 +^ b2).x by A1,A2,POLYNOM1:def 13;
A9: o1+^k' in o1+^o2 by A7,ORDINAL2:49;
o1 c= o1+^k' by ORDINAL3:27;
then not o1+^k' in o1 by ORDINAL1:7;
then A10: o1+^k' in (o1+^o2) \ o1 by A9,XBOOLE_0:def 4;
then A11: (b1+^b2).(o1+^k') = b2.(o1+^k'-^o1) by Def1;
k'= o1+^k'-^o1 by ORDINAL3:65;
hence c2'.k <= b2'.k by A8,A10,A11,Def1;
end;
take c1,c2;
thus c1 divides b1 & c2 divides b2 & b = c1 +^ c2
by A2,A3,A6,POLYNOM1:50;
end;
theorem Th11:
for a1,b1 being Element of Bags o1, a2,b2 being Element of Bags o2
holds a1 +^ a2 < b1 +^ b2 iff a1 < b1 or a1 = b1 & a2 < b2
proof
let a1,b1 be Element of Bags o1, a2,b2 be Element of Bags o2;
thus a1 +^ a2 < b1 +^ b2 implies a1 < b1 or a1 = b1 & a2 < b2
proof
assume a1 +^ a2 < b1 +^ b2;
then consider k be Ordinal such that
A1: (a1 +^ a2).k < (b1 +^ b2).k and
A2: for l being Ordinal st l in k holds (a1 +^ a2).l = (b1 +^ b2).l
by POLYNOM1:def 11;
now assume not k in dom(b1+^b2);
then (b1+^b2).k = 0 by FUNCT_1:def 4;
hence contradiction by A1,NAT_1:18;
end;
then A3: k in o1+^o2 by PBOOLE:def 3;
now per cases by A3,XBOOLE_0:def 4;
case A4:k in o1;
then (a1 +^ a2).k = a1.k by Def1;
then A5: a1.k < b1.k by A1,A4,Def1;
reconsider a1'=a1,b1'=b1 as bag of o1;
for l being Ordinal st l in k holds a1'.l = b1'.l
proof
let l be Ordinal;
assume A6: l in k;
then A7: (a1 +^ a2).l = (b1 +^ b2).l by A2;
l is epsilon-transitive by ORDINAL1:def 4;
then A8: l in o1 by A4,A6,ORDINAL1:19;
then (a1 +^ a2).l = a1.l by Def1;
hence a1'.l = b1'.l by A7,A8,Def1;
end;
hence a1 < b1 by A5,POLYNOM1:def 11;
case A9:k in (o1+^ o2)\o1;
for i be set st i in o1 holds a1.i = b1.i
proof
let i be set;
assume A10:i in o1;
then reconsider i'=i as Ordinal by ORDINAL1:23;
not k in o1 by A9,XBOOLE_0:def 4;
then A11: o1 c= k by ORDINAL1:26;
A12: (a1 +^ a2).i' = a1.i' by A10,Def1;
(b1 +^ b2).i' = b1.i' by A10,Def1;
hence a1.i = b1.i by A2,A10,A11,A12;
end;
hence a1 = b1 by PBOOLE:3;
not k in o1 by A9,XBOOLE_0:def 4;
then o1 c= k by ORDINAL1:26;
then A13: k = o1+^(k-^o1) by ORDINAL3:def 6;
set k1 = k -^ o1;
(a1+^a2).k = a2.(k-^o1) by A9,Def1;
then A14: a2.k1 < b2.k1 by A1,A9,Def1;
for l being Ordinal st l in k1 holds a2.l = b2.l
proof
let l be Ordinal;
assume l in k1;
then A15: o1 +^ l in o1 +^ k1 by ORDINAL2:49;
A16: k in o1+^o2 by A9,XBOOLE_0:def 4;
o1+^l is epsilon-transitive by ORDINAL1:def 4;
then A17: o1 +^ l in o1 +^o2 by A13,A15,A16,ORDINAL1:19;
o1 c= o1 +^l by ORDINAL3:27;
then not o1 +^l in o1 by ORDINAL1:7;
then A18: o1 +^ l in (o1+^ o2)\o1 by A17,XBOOLE_0:def 4;
then A19: (a1 +^ a2).(o1 +^ l) = a2.(o1+^l-^o1) by Def1
.= a2.l by ORDINAL3:65;
(b1 +^ b2).(o1 +^ l) = b2.(o1+^l-^o1) by A18,Def1
.= b2.l by ORDINAL3:65;
hence a2.l = b2.l by A2,A13,A15,A19;
end;
hence a2 < b2 by A14,POLYNOM1:def 11;
end;
hence thesis;
end;
thus a1 < b1 or a1 = b1 & a2 < b2 implies a1 +^ a2 < b1 +^ b2
proof
assume A20: a1 < b1 or a1 = b1 & a2 < b2;
now per cases;
case a1 < b1;
then consider k be Ordinal such that
A21: k in o1 and
A22: a1.k < b1.k and
A23: for l being Ordinal st l in k holds a1.l = b1.l by Th2;
A24: (a1 +^ a2).k = a1.k by A21,Def1;
A25: (b1 +^ b2).k = b1.k by A21,Def1;
for l being Ordinal st l in k holds (a1 +^ a2).l = (b1 +^ b2).l
proof
let l be Ordinal;
assume A26:l in k;
l is epsilon-transitive by ORDINAL1:def 4;
then A27: l in o1 by A21,A26,ORDINAL1:19;
then A28: (a1 +^ a2).l = a1.l by Def1;
(b1 +^ b2).l = b1.l by A27,Def1;
hence (a1 +^ a2).l = (b1 +^ b2).l by A23,A26,A28;
end;
hence a1 +^ a2 < b1 +^ b2 by A22,A24,A25,POLYNOM1:def 11;
case A29: not a1 < b1;
then consider k be Ordinal such that
A30: k in o2 and
A31: a2.k < b2.k and
A32: for l being Ordinal st l in k holds a2.l = b2.l by A20,Th2;
set x = o1+^k;
A33: o1+^k in o1+^o2 by A30,ORDINAL2:49;
o1 c= o1+^k by ORDINAL3:27;
then not o1+^k in o1 by ORDINAL1:7;
then A34: o1+^k in (o1+^o2) \ o1 by A33,XBOOLE_0:def 4;
then A35: (b1+^b2).(o1+^k) = b2.(o1+^k-^o1) by Def1;
k= o1+^k-^o1 by ORDINAL3:65;
then A36: (a1 +^ a2).x < (b1 +^ b2).x by A31,A34,A35,Def1;
for l being Ordinal st l in x holds (a1 +^ a2).l = (b1 +^ b2).l
proof
let l be Ordinal;
assume A37:l in x;
per cases;
suppose
A38: l in o1;
hence (a1 +^ a2).l = b1.l by A20,A29,Def1
.= (b1 +^ b2).l by A38,Def1;
suppose
A39: not l in o1;
A40: o1 +^ k in o1+^o2 by A30,ORDINAL2:49;
l is epsilon-transitive by ORDINAL1:def 4;
then A41: l in o1+^o2 by A37,A40,ORDINAL1:19;
o1 c= l by A39,ORDINAL1:26;
then l-^o1 in o1+^k-^o1 by A37,ORDINAL3:66;
then A42: l-^o1 in k by ORDINAL3:65;
A43: l in (o1+^o2) \ o1 by A39,A41,XBOOLE_0:def 4;
hence (a1 +^ a2).l = a2.(l -^ o1) by Def1
.= b2.(l -^ o1) by A32,A42
.= (b1 +^ b2).l by A43,Def1;
end;
hence a1 +^ a2 < b1 +^ b2 by A36,POLYNOM1:def 11;
end;
hence a1 +^ a2 < b1 +^ b2;
end;
end;
theorem Th12:
for b1 being Element of Bags o1, b2 being Element of Bags o2
for G being FinSequence of (Bags(o1+^o2))* st
dom G = dom divisors b1 &
for i being Nat st i in dom divisors b1 holds
ex a1' being Element of Bags o1,
Fk being FinSequence of Bags(o1+^o2)
st Fk = G/.i & (divisors b1)/.i = a1' &
len Fk = len divisors b2 &
for m being Nat st m in dom Fk
ex a1'' being Element of Bags o2 st
(divisors b2)/.m = a1'' &
Fk/.m = a1'+^a1''
holds divisors(b1+^b2) = FlattenSeq G
proof let b1 be Element of Bags o1, b2 be Element of Bags o2;
let G be FinSequence of (Bags(o1+^o2))* such that
A1: dom G = dom divisors b1 and
A2: for i being Nat st i in dom divisors b1 holds
ex a1' being Element of Bags o1,
Fk being FinSequence of Bags(o1+^o2)
st Fk = G/.i & (divisors b1)/.i = a1' &
len Fk = len divisors b2 &
for m being Nat st m in dom Fk
ex a1'' being Element of Bags o2 st
(divisors b2)/.m = a1'' &
Fk/.m = a1'+^a1'';
len divisors b1 <> 0 by FINSEQ_1:25;
then len G <> 0 by A1,FINSEQ_3:31;
then A3:G is non empty by FINSEQ_1:25;
then A4: G = <*G.1*>^Del(G,1) by POLYALG1:4;
reconsider D = Del(G,1) as FinSequence of (Bags(o1+^o2))*;
A5:1 in dom G by A3,FINSEQ_5:6;
then consider a1' being Element of Bags o1,
Fk being FinSequence of Bags(o1+^o2) such that
A6: Fk = G/.1 & (divisors b1)/.1 = a1' and
A7: len Fk = len divisors b2 and
for m being Nat st m in dom Fk
ex a1'' being Element of Bags o2 st
(divisors b2)/.m = a1'' &
Fk/.m = a1'+^a1'' by A1,A2;
reconsider G1 = G.1 as Element of (Bags(o1+^o2))* by A5,A6,FINSEQ_4:def 4;
A8: FlattenSeq G = (FlattenSeq <*G1*>)^FlattenSeq D by A4,SCMFSA_7:14
.= G1^FlattenSeq D by DTCONSTR:13;
A9:Fk = G.1 by A5,A6,FINSEQ_4:def 4;
len divisors b2 <> 0 by FINSEQ_1:25;
then G.1 <> {} by A7,A9,FINSEQ_1:25;
then FlattenSeq G <>{} by A8,FINSEQ_1:48;
then reconsider S = rng FlattenSeq G
as non empty finite Subset of Bags(o1+^o2) by FINSEQ_1:def 4,RELAT_1:64;
set F = FlattenSeq G;
field BagOrder(o1+^o2) = Bags(o1+^o2) by ORDERS_2:2;
then BagOrder(o1+^o2) linearly_orders Bags(o1+^o2) by ORDERS_2:35;
then A10: BagOrder(o1+^o2) linearly_orders S by ORDERS_2:36;
for n,m be Nat st n in dom F & m in dom F & n < m holds
F/.n <> F/.m & [F/.n,F/.m] in BagOrder(o1+^o2)
proof let n,m be Nat such that
A11: n in dom F & m in dom F and
A12: n < m;
now assume A13: F/.n = F/.m;
A14: F/.n=F.n by A11,FINSEQ_4:def 4;
A15: F/.m=F.m by A11,FINSEQ_4:def 4;
consider i1, j1 being Nat such that
A16: i1 in dom G and
A17: j1 in dom (G.i1) and
A18: n = (Sum Card (G|(i1-'1))) + j1 and
A19: (G.i1).j1 = (FlattenSeq G).n by A11,POLYNOM1:32;
consider i2, j2 being Nat such that
A20: i2 in dom G and
A21: j2 in dom (G.i2) and
A22: m = (Sum Card (G|(i2-'1))) + j2 and
A23: (G.i2).j2 = (FlattenSeq G).m by A11,POLYNOM1:32;
consider a1' being Element of Bags o1,
Fk being FinSequence of Bags(o1+^o2) such that
A24: Fk = G/.i1 and
A25: (divisors b1)/.i1 = a1' and
A26: len Fk = len divisors b2 and
A27: for r being Nat st r in dom Fk
ex a1'' being Element of Bags o2 st
(divisors b2)/.r = a1'' & Fk/.r = a1'+^a1'' by A1,A2,A16;
A28: j1 in dom Fk by A16,A17,A24,FINSEQ_4:def 4;
then consider a1'' being Element of Bags o2 such that
A29: (divisors b2)/.j1 = a1'' and
A30: Fk/.j1 = a1'+^a1'' by A27;
consider a2' being Element of Bags o1,
Fk' being FinSequence of Bags(o1+^o2) such that
A31: Fk' = G/.i2 and
A32: (divisors b1)/.i2 = a2' and
A33: len Fk' = len divisors b2 and
A34: for r being Nat st r in dom Fk'
ex a2'' being Element of Bags o2 st
(divisors b2)/.r = a2'' & Fk'/.r = a2'+^a2'' by A1,A2,A20;
A35: j2 in dom Fk' by A20,A21,A31,FINSEQ_4:def 4;
then consider a2'' being Element of Bags o2 such that
A36: (divisors b2)/.j2 = a2'' and
A37: Fk'/.j2 = a2'+^a2'' by A34;
Fk = G.i1 by A16,A24,FINSEQ_4:def 4;
then A38: (FlattenSeq G).n = Fk/.j1 by A17,A19,FINSEQ_4:def 4;
Fk' = G.i2 by A20,A31,FINSEQ_4:def 4;
then (FlattenSeq G).m = Fk'/.j2 by A21,A23,FINSEQ_4:def 4;
then A39: a1'=a2' & a1''=a2'' by A13,A14,A15,A30,A37,A38,Th7;
A40: (divisors b1).i1 = a1' by A1,A16,A25,FINSEQ_4:def 4;
(divisors b1).i2 = a2' by A1,A20,A32,FINSEQ_4:def 4;
then A41: i1=i2 by A1,A16,A20,A39,A40,FUNCT_1:def 8;
Seg len Fk = dom Fk by FINSEQ_1:def 3;
then A42: j1 in dom divisors b2 by A26,A28,FINSEQ_1:def 3;
then A43: (divisors b2).j1 = a1'' by A29,FINSEQ_4:def 4;
Seg len Fk' = dom Fk' by FINSEQ_1:def 3;
then A44: j2 in dom divisors b2 by A33,A35,FINSEQ_1:def 3;
then (divisors b2).j2 = a2'' by A36,FINSEQ_4:def 4;
hence contradiction by A12,A18,A22,A39,A41,A42,A43,A44,FUNCT_1:def 8;
end;
hence F/.n <> F/.m;
A45: F/.n = F.n by A11,FINSEQ_4:def 4;
A46: F/.m = F.m by A11,FINSEQ_4:def 4;
reconsider Fn=F/.n, Fm=F/.m as bag of (o1+^o2) by POLYNOM1:def 14;
reconsider Fn'=Fn,Fm'=Fm as Element of Bags (o1+^o2);
consider a1 be Element of Bags o1, a2 be Element of Bags o2
such that
A47: Fn' = a1+^a2 by Th6;
consider c1 be Element of Bags o1, c2 be Element of Bags o2
such that
A48: Fm' = c1+^c2 by Th6;
consider i1, j1 being Nat such that
A49: i1 in dom G and
A50: j1 in dom (G.i1) and
A51: n = (Sum Card (G|(i1-'1))) + j1 and
A52: (G.i1).j1 = (FlattenSeq G).n by A11,POLYNOM1:32;
consider i2, j2 being Nat such that
A53: i2 in dom G and
A54: j2 in dom (G.i2) and
A55: m = (Sum Card (G|(i2-'1))) + j2 and
A56: (G.i2).j2 = (FlattenSeq G).m by A11,POLYNOM1:32;
consider a1' being Element of Bags o1,
Fk being FinSequence of Bags(o1+^o2) such that
A57: Fk = G/.i1 and
A58: (divisors b1)/.i1 = a1' and
A59: len Fk = len divisors b2 and
A60: for r being Nat st r in dom Fk
ex a1'' being Element of Bags o2 st
(divisors b2)/.r = a1'' & Fk/.r = a1'+^a1'' by A1,A2,A49;
A61: j1 in dom Fk by A49,A50,A57,FINSEQ_4:def 4;
then consider a1'' being Element of Bags o2 such that
A62: (divisors b2)/.j1 = a1'' and
A63: Fk/.j1 = a1'+^a1'' by A60;
consider a2' being Element of Bags o1,
Fk' being FinSequence of Bags(o1+^o2) such that
A64: Fk' = G/.i2 and
A65: (divisors b1)/.i2 = a2' and
A66: len Fk' = len divisors b2 and
A67: for r being Nat st r in dom Fk'
ex a2'' being Element of Bags o2 st
(divisors b2)/.r = a2'' & Fk'/.r = a2'+^a2'' by A1,A2,A53;
A68: j2 in dom Fk' by A53,A54,A64,FINSEQ_4:def 4;
then consider a2'' being Element of Bags o2 such that
A69: (divisors b2)/.j2 = a2'' and
A70: Fk'/.j2 = a2'+^a2'' by A67;
Fk = G.i1 by A49,A57,FINSEQ_4:def 4;
then A71: Fn' = Fk/.j1 by A45,A50,A52,FINSEQ_4:def 4;
Fk' = G.i2 by A53,A64,FINSEQ_4:def 4;
then Fm' = Fk'/.j2 by A46,A54,A56,FINSEQ_4:def 4;
then A72: a1'=a1 & a1''= a2 & a2'= c1 & a2''= c2 by A47,A48,A63,A70,A71,Th7;
then A73: (divisors b1).i1 = a1 by A1,A49,A58,FINSEQ_4:def 4;
A74: (divisors b1).i2 = c1 by A1,A53,A65,A72,FINSEQ_4:def 4;
Seg len Fk = dom Fk by FINSEQ_1:def 3;
then A75: j1 in dom divisors b2 by A59,A61,FINSEQ_1:def 3;
then A76: (divisors b2).j1 = a2 by A62,A72,FINSEQ_4:def 4;
Seg len Fk' = dom Fk' by FINSEQ_1:def 3;
then A77: j2 in dom divisors b2 by A66,A68,FINSEQ_1:def 3;
then A78: (divisors b2).j2 = c2 by A69,A72,FINSEQ_4:def 4;
now consider S being non empty finite Subset of Bags o1 such that
A79: divisors b1 = SgmX(BagOrder o1, S) and
for p being bag of o1 holds p in S iff p divides b1 by POLYNOM1:def 18
;
field BagOrder o1 = Bags o1 by ORDERS_2:2;
then BagOrder o1 linearly_orders Bags o1 by ORDERS_2:35;
then A80: BagOrder o1 linearly_orders S by ORDERS_2:36;
consider T being non empty finite Subset of Bags o2
such that
A81: divisors b2 = SgmX(BagOrder o2, T) and
for p being bag of o2 holds p in T iff p divides b2 by POLYNOM1:def 18
;
field BagOrder o2= Bags o2 by ORDERS_2:2;
then BagOrder o2 linearly_orders Bags o2 by ORDERS_2:35;
then A82: BagOrder o2 linearly_orders T by ORDERS_2:36;
A83: now assume that
A84: not i1 < i2 and
A85: not (i1 = i2 & j1 < j2);
per cases by A84,AXIOMS:21;
suppose i1=i2;
hence contradiction by A12,A51,A55,A85,AXIOMS:24;
suppose
A86: i1>i2;
A87: j2<= Card (G.i2) by A54,FINSEQ_3:27;
A88: Card(G|i2) = (Card G)|i2 by POLYNOM3:16;
A89: Card (G|(i1-'1)) = (Card G)|(i1-'1) by POLYNOM3:16;
i2 <= i1 -' 1 by A86,JORDAN3:12;
then A90: (Sum Card (G|i2)) <= (Sum Card (G|(i1-'1))) by A88,A89,POLYNOM3:
18;
i2>=1 by A53,FINSEQ_3:27;
then A91: i2 -' 1 = i2 - 1 by SCMFSA_7:3;
i2 < i2 + 1 by REAL_1:69;
then A92: i2 - 1 < i2 by REAL_1:84;
i2 <= len G by A53,FINSEQ_3:27;
then A93: i2-'1 < len G by A91,A92,AXIOMS:22;
i2>=1 by A53,FINSEQ_3:27;
then A94: i2-'1+1 = i2 by AMI_5:4;
reconsider G1 = G.i2 as Element of (Bags(o1+^o2))*
by A53,A64,FINSEQ_4:def 4;
reconsider GG1 = <*G1*> as FinSequence of (Bags(o1+^o2))*;
G|i2 = G|(i2-'1) ^ GG1 by A93,A94,POLYNOM3:19;
then Card (G|i2) = Card (G|(i2-'1))^Card(GG1) by POLYNOM1:13;
then Card (G|i2) = (Card (G|(i2-'1)))^<*Card G1*> by POLYNOM1:12;
then Sum Card (G|i2) = (Sum Card (G|(i2-'1))) + Card(G.i2) by RVSUM_1:
104;
then (Sum Card (G|(i2-'1))) + j2 <= Sum Card (G|i2) by A87,AXIOMS:24;
then A95: (Sum Card (G|(i2-'1))) + j2 <= (Sum Card (G|(i1-'1)))
by A90,AXIOMS:22;
(Sum Card (G|(i1-'1))) <= (Sum Card (G|(i1-'1))) +j1 by NAT_1:29;
hence contradiction by A12,A51,A55,A95,AXIOMS:22;
end;
per cases by A83;
case
A96: i1 < i2;
then A97: [(divisors b1)/.i1, (divisors b1)/.i2] in BagOrder o1 by A1,A49,
A53,A79,A80,TRIANG_1:def 2;
A98: a1<>c1 by A1,A49,A53,A73,A74,A96,FUNCT_1:def 8;
a1 <=' c1 by A58,A65,A72,A97,POLYNOM1:def 16;
hence a1<c1 by A98,POLYNOM1:def 12;
case that
A99: i1 = i2 and
A100: j1 < j2;
A101: [(divisors b2)/.j1, (divisors b2)/.j2] in BagOrder o2 by A75,A77,A81,
A82,A100,TRIANG_1:def 2;
thus a1=c1 by A58,A65,A72,A99;
A102: a2<>c2 by A75,A76,A77,A78,A100,FUNCT_1:def 8;
a2 <=' c2 by A62,A69,A72,A101,POLYNOM1:def 16;
hence a2<c2 by A102,POLYNOM1:def 12;
end;
then Fn < Fm or Fn = Fm by A47,A48,Th11;
then Fn <=' Fm by POLYNOM1:def 12;
hence [F/.n,F/.m] in BagOrder(o1+^o2) by POLYNOM1:def 16;
end;
then A103: FlattenSeq G = SgmX(BagOrder(o1+^o2), S) by A10,TRIANG_1:def 2;
for p being bag of o1+^o2 holds p in S iff p divides b1+^b2
proof
consider T being non empty finite Subset of Bags o1 such that
A104: divisors b1 = SgmX(BagOrder o1, T) and
A105: for q being bag of o1 holds q in T iff q divides b1
by POLYNOM1:def 18;
consider W being non empty finite Subset of Bags o2 such that
A106: divisors b2 = SgmX(BagOrder o2, W) and
A107: for q being bag of o2 holds q in W iff q divides b2
by POLYNOM1:def 18;
field BagOrder o1 = Bags o1 by ORDERS_2:2;
then BagOrder o1 linearly_orders Bags o1 by ORDERS_2:35;
then BagOrder o1 linearly_orders T by ORDERS_2:36;
then A108: rng SgmX(BagOrder o1, T) = T by TRIANG_1:def 2;
field BagOrder o2 = Bags o2 by ORDERS_2:2;
then BagOrder o2 linearly_orders Bags o2 by ORDERS_2:35;
then BagOrder o2 linearly_orders W by ORDERS_2:36;
then A109: rng SgmX(BagOrder o2, W) = W by TRIANG_1:def 2;
let p be bag of o1+^o2;
thus p in S implies p divides b1+^b2
proof
assume p in S;
then consider x be set such that
A110: x in dom FlattenSeq G and
A111: p = (FlattenSeq G).x by FUNCT_1:def 5;
consider i, j being Nat such that
A112: i in dom G and
A113: j in dom (G.i) and
x = (Sum Card (G|(i-'1))) + j and
A114: (G.i).j = (FlattenSeq G).x by A110,POLYNOM1:32;
consider a1' being Element of Bags o1,
Fk being FinSequence of Bags(o1+^o2) such that
A115: Fk = G/.i and
A116: (divisors b1)/.i = a1' and
A117: len Fk = len divisors b2 and
A118: for m being Nat st m in dom Fk
ex a1'' being Element of Bags o2 st
(divisors b2)/.m = a1'' & Fk/.m = a1'+^a1'' by A1,A2,A112;
A119: Fk=G.i by A112,A115,FINSEQ_4:def 4;
then consider a1'' being Element of Bags o2 such that
A120: (divisors b2)/.j = a1'' and
A121: Fk/.j = a1'+^a1'' by A113,A118;
A122: p = a1' +^ a1'' by A111,A113,A114,A119,A121,FINSEQ_4:def 4;
(divisors b1).i = a1' by A1,A112,A116,FINSEQ_4:def 4;
then A123:a1' in T by A1,A104,A108,A112,FUNCT_1:12;
reconsider a11'= a1' as bag of o1;
A124:a11' divides b1 by A105,A123;
j in Seg len Fk by A113,A119,FINSEQ_1:def 3;
then A125:j in dom divisors b2 by A117,FINSEQ_1:def 3;
then (divisors b2).j = a1'' by A120,FINSEQ_4:def 4;
then A126:a1'' in W by A106,A109,A125,FUNCT_1:12;
reconsider a11''= a1'' as bag of o2;
a11'' divides b2 by A107,A126;
hence p divides b1+^b2 by A122,A124,Th9;
end;
thus p divides b1+^b2 implies p in S
proof
assume p divides b1+^b2;
then consider p1 being Element of Bags o1, p2 being Element of Bags o2
such that
A127: p1 divides b1 and
A128: p2 divides b2 and
A129: p = p1 +^ p2 by Th10;
p1 in T by A105,A127;
then consider i be set such that
A130: i in dom divisors b1 and
A131: p1 = (divisors b1).i by A104,A108,FUNCT_1:def 5;
p2 in rng divisors b2 by A106,A107,A109,A128;
then consider j be set such that
A132: j in dom divisors b2 and
A133: p2 = (divisors b2).j by FUNCT_1:def 5;
reconsider i as Nat by A130;
consider a1' being Element of Bags o1,
Fk being FinSequence of Bags(o1+^o2)
such that
A134: Fk = G/.i and
A135: (divisors b1)/.i = a1' and
A136: len Fk = len divisors b2 and
A137: for m being Nat st m in dom Fk
ex a1'' being Element of Bags o2 st (divisors b2)/.m = a1'' &
Fk/.m = a1'+^a1'' by A2,A130;
A138: j in Seg len divisors b2 by A132,FINSEQ_1:def 3;
Seg len (G.i) = Seg len divisors b2 by A1,A130,A134,A136,FINSEQ_4:def
4
;
then A139: j in dom (G.i) by A138,FINSEQ_1:def 3;
reconsider j as Nat by A132;
A140: (Sum Card (G|(i-'1))) + j in dom FlattenSeq G &
(G.i).j = (FlattenSeq G).((Sum Card (G|(i-'1))) + j)
by A1,A130,A139,POLYNOM1:33;
A141: G/.i = G.i by A1,A130,FINSEQ_4:def 4;
then consider a1'' being Element of Bags o2 such that
A142: (divisors b2)/.j = a1'' and
A143: Fk/.j = a1'+^a1'' by A134,A137,A139;
A144: (G.i).j = a1'+^a1'' by A134,A139,A141,A143,FINSEQ_4:def 4;
A145: a1' = p1 by A130,A131,A135,FINSEQ_4:def 4;
a1'' = p2 by A132,A133,A142,FINSEQ_4:def 4;
hence p in S by A129,A140,A144,A145,FUNCT_1:def 5;
end;
end;
hence divisors(b1+^b2) = FlattenSeq G by A103,POLYNOM1:def 18;
end;
theorem Th13:
for a1,b1,c1 being Element of Bags o1, a2,b2,c2 being Element of Bags o2
st c1 = b1 -' a1 & c2 = b2 -' a2
holds (b1 +^ b2) -' (a1 +^ a2) = c1 +^ c2
proof let a1,b1,c1 be Element of Bags o1, a2,b2,c2 be Element of Bags o2;
assume
A1: c1 = b1 -' a1 & c2 = b2 -' a2;
reconsider w = (b1 +^ b2) -' (a1 +^ a2) as Element of Bags(o1+^o2)
by POLYNOM1:def 14;
for o be Ordinal holds
(o in o1 implies w.o = c1.o) &
(o in (o1+^o2) \ o1 implies w.o=c2.(o-^o1))
proof let o be Ordinal;
hereby assume
A2: o in o1;
thus w.o = (b1 +^ b2).o -' (a1 +^ a2).o by POLYNOM1:def 6
.= b1.o -' (a1 +^ a2).o by A2,Def1
.= b1.o -' a1.o by A2,Def1
.= c1.o by A1,POLYNOM1:def 6;
end;
assume
A3: o in (o1+^o2) \ o1;
thus w.o = (b1 +^ b2).o -' (a1 +^ a2).o by POLYNOM1:def 6
.= b2.(o-^o1) -' (a1 +^ a2).o by A3,Def1
.= b2.(o-^o1) -' a2.(o-^o1) by A3,Def1
.= c2.(o-^o1) by A1,POLYNOM1:def 6;
end;
hence (b1 +^ b2) -' (a1 +^ a2) = c1 +^ c2 by Def1;
end;
theorem Th14:
for b1 being Element of Bags o1, b2 being Element of Bags o2
for G being FinSequence of (2-tuples_on Bags(o1+^o2))* st
dom G = dom decomp b1 &
for i being Nat st i in dom decomp b1 holds
ex a1', b1' being Element of Bags o1,
Fk being FinSequence of 2-tuples_on Bags(o1+^o2)
st Fk = G/.i & (decomp b1)/.i = <*a1', b1'*> &
len Fk = len decomp b2 &
for m being Nat st m in dom Fk
ex a1'',b1'' being Element of Bags o2 st
(decomp b2)/.m = <*a1'', b1''*> &
Fk/.m =<*a1'+^a1'',b1'+^b1''*>
holds decomp(b1+^b2) = FlattenSeq G
proof let b1 be Element of Bags o1, b2 be Element of Bags o2;
let G be FinSequence of (2-tuples_on Bags(o1+^o2))* such that
A1: dom G = dom decomp b1 and
A2: for i being Nat st i in dom decomp b1 holds
ex a1', b1' being Element of Bags o1,
Fk being FinSequence of 2-tuples_on Bags(o1+^o2)
st Fk = G/.i & (decomp b1)/.i = <*a1', b1'*> &
len Fk = len decomp b2 &
for m being Nat st m in dom Fk
ex a1'',b1'' being Element of Bags o2 st
(decomp b2)/.m = <*a1'', b1''*> &
Fk/.m =<*a1'+^a1'',b1'+^b1''*>;
defpred P[set,Function] means
dom $2 = dom(G.$1) &
for j being Nat st j in dom $2
ex p being Element of (2-tuples_on (Bags(o1+^o2)))
st p = G.$1.j & $2.j = p.1;
A3: for k being Nat st k in Seg len G
ex p being Element of (Bags(o1+^o2))* st P[k,p]
proof let k be Nat such that
A4: k in Seg len G;
defpred Q[set,set] means
ex q being Element of 2-tuples_on (Bags(o1+^o2))
st q = G.k.$1 & $2 = q.1;
A5: for j being Nat st j in Seg len(G.k)
ex x being Element of (Bags(o1+^o2)) st Q[j,x]
proof let j be Nat such that
A6: j in Seg len(G.k);
k in dom G by A4,FINSEQ_1:def 3;
then A7: G.k in rng G by FUNCT_1:12;
rng G c= (2-tuples_on (Bags(o1+^o2)))* by FINSEQ_1:def 4;
then G.k is Element of (2-tuples_on (Bags(o1+^o2)))* by A7;
then reconsider Gk = G.k
as FinSequence of 2-tuples_on (Bags(o1+^o2));
j in dom(G.k) by A6,FINSEQ_1:def 3;
then G.k.j = (Gk)/.j by FINSEQ_4:def 4;
then reconsider q = G.k.j as Element of 2-tuples_on (Bags(o1+^o2));
consider q1,q2 being Element of(Bags(o1+^o2)) such that
A8: q = <*q1,q2*> by FINSEQ_2:120;
reconsider x = q.1 as Element of (Bags(o1+^o2)) by A8,FINSEQ_1:61;
take x;
thus Q[j,x];
end;
consider p being FinSequence of (Bags(o1+^o2)) such that
A9: dom p = Seg len(G.k) and
A10: for j being Nat st j in Seg len(G.k) holds Q[j,p/.j] from SeqExD(A5);
reconsider p as Element of (Bags(o1+^o2))* by FINSEQ_1:def 11;
take p;
thus dom p = dom(G.k) by A9,FINSEQ_1:def 3;
let j be Nat;
assume
A11: j in dom p;
then consider q being Element of 2-tuples_on (Bags(o1+^o2)) such that
A12: q = G.k.j and
A13: p/.j = q.1 by A9,A10;
take q;
thus q = G.k.j by A12;
thus p.j = q.1 by A11,A13,FINSEQ_4:def 4;
end;
consider F being FinSequence of (Bags(o1+^o2))* such that
A14: dom F = Seg len G and
A15: for i being Nat st i in Seg len G holds P[i,F/.i] from SeqExD(A3);
dom decomp b1 = dom divisors b1 by POLYNOM1:def 19;
then A16: dom F = dom divisors b1 by A1,A14,FINSEQ_1:def 3;
A17: dom divisors b1 = dom decomp b1 by POLYNOM1:def 19;
A18: for i being Nat st i in dom divisors b1 holds
ex a1' being Element of Bags o1,
Fk being FinSequence of Bags(o1+^o2)
st Fk = F/.i & (divisors b1)/.i = a1' &
len Fk = len divisors b2 &
for m being Nat st m in dom Fk
ex a1'' being Element of Bags o2 st
(divisors b2)/.m = a1'' & Fk/.m = a1'+^a1''
proof let i be Nat;
assume
A19: i in dom divisors b1;
then consider a1', b1' being Element of Bags o1,
Gi being FinSequence of 2-tuples_on Bags(o1+^o2) such that
A20: Gi = G/.i and
A21: (decomp b1)/.i = <*a1', b1'*> and
A22: len Gi = len decomp b2 and
A23: for m being Nat st m in dom Gi
ex a1'',b1'' being Element of Bags o2 st
(decomp b2)/.m = <*a1'', b1''*> &
Gi/.m =<*a1'+^a1'',b1'+^b1''*> by A2,A17;
A24: i in Seg len G by A1,A17,A19,FINSEQ_1:def 3;
then A25: dom(F/.i) = dom(G.i) &
for j being Nat st j in dom(F/.i)
ex p being Element of (2-tuples_on (Bags(o1+^o2)))
st p = G.i.j & (F/.i).j = p.1 by A15;
reconsider Fk = F/.i as FinSequence of Bags(o1+^o2);
take a1',Fk;
A26: dom decomp b2 = dom divisors b2 by POLYNOM1:def 19;
thus Fk = F/.i;
thus (divisors b1)/.i = a1' by A17,A19,A21,POLYNOM1:74;
thus len Fk = len(G.i) by A25,FINSEQ_3:31
.= len decomp b2 by A1,A17,A19,A20,A22,FINSEQ_4:def 4
.= len divisors b2 by A26,FINSEQ_3:31;
let m be Nat;
A27: G.i = G/.i by A1,A17,A19,FINSEQ_4:def 4;
assume
A28: m in dom Fk;
then consider a1'',b1'' being Element of Bags o2 such that
A29: (decomp b2)/.m = <*a1'', b1''*> and
A30: Gi/.m =<*a1'+^a1'',b1'+^b1''*> by A20,A23,A25,A27;
take a1'';
m in dom decomp b2 by A20,A22,A25,A27,A28,FINSEQ_3:31;
hence (divisors b2)/.m = a1'' by A29,POLYNOM1:74;
consider p being Element of (2-tuples_on (Bags(o1+^o2))) such that
A31: p = G.i.m and
A32: (F/.i).m = p.1 by A15,A24,A28;
A33: p = <*a1'+^a1'',b1'+^b1''*> by A20,A25,A27,A28,A30,A31,FINSEQ_4:def 4;
thus Fk/.m = Fk.m by A28,FINSEQ_4:def 4
.= a1'+^a1'' by A32,A33,FINSEQ_1:61;
end;
then A34: divisors(b1+^b2) = FlattenSeq F by A16,Th12;
reconsider FG = FlattenSeq G as FinSequence of 2-tuples_on Bags(o1+^o2);
reconsider bb = b1+^b2 as bag of o1+^o2;
dom decomp b2 = dom divisors b2 by POLYNOM1:def 19;
then A35: len decomp b2 = len divisors b2 by FINSEQ_3:31;
A36: dom decomp b1 = dom divisors b1 by POLYNOM1:def 19;
A37: dom Card F = dom F by CARD_3:def 2 .= dom G by A14,FINSEQ_1:def 3
.= dom Card G by CARD_3:def 2;
then A38: len Card F = len Card G by FINSEQ_3:31;
for j be Nat st j in Seg len Card F holds (Card F).j = (Card G).j
proof
let j be Nat;
assume A39:j in Seg len Card F;
then A40: j in dom Card F by FINSEQ_1:def 3;
A41: j in dom Card G by A37,A39,FINSEQ_1:def 3;
A42: dom Card F = dom F by CARD_3:def 2;
A43: j in dom G by A41,CARD_3:def 2;
A44: (Card F).j = Card(F.j) by A40,A42,CARD_3:def 2;
A45: j in dom decomp b1 by A1,A14,A40,A42,FINSEQ_1:def 3;
then consider a1' being Element of Bags o1,
Fk being FinSequence of Bags(o1+^o2) such that
A46: Fk = F/.j and (divisors b1)/.j = a1' and
A47: len Fk = len divisors b2 and
for m being Nat st m in dom Fk
ex a1'' being Element of Bags o2 st
(divisors b2)/.m = a1'' &
Fk/.m = a1'+^a1'' by A17,A18;
consider a2', b2' being Element of Bags o1,
Gk being FinSequence of 2-tuples_on Bags(o1+^o2) such that
A48: Gk = G/.j and (decomp b1)/.j = <*a2', b2'*> and
A49: len Gk = len decomp b2 and
for m being Nat st m in dom Gk
ex a2'',b2'' being Element of Bags o2 st
(decomp b2)/.m = <*a2'', b2''*> &
Gk/.m =<*a2'+^a2'',b2'+^b2''*> by A2,A45;
Card(F.j) = Card(F/.j) by A40,A42,FINSEQ_4:def 4
.= Card(G.j) by A35,A43,A46,A47,A48,A49,FINSEQ_4:def 4;
hence (Card F).j = (Card G).j by A43,A44,CARD_3:def 2;
end;
then A50: Card F = Card G by A38,FINSEQ_2:10;
then A51: len FG = len FlattenSeq F by POLYNOM1:31;
then A52: dom FG = dom divisors bb by A34,FINSEQ_3:31;
for i being Nat, p being bag of o1+^o2
st i in dom FG & p = (divisors bb)/.i
holds FG/.i = <*p, bb-'p*>
proof let k be Nat, p be bag of o1+^o2 such that
A53: k in dom FG and
A54: p = (divisors bb)/.k;
consider i, j being Nat such that
A55: i in dom G and
A56: j in dom (G.i) and
A57: k = (Sum Card (G|(i-'1))) + j and
A58: (G.i).j = FG.k by A53,POLYNOM1:32;
k in dom FlattenSeq F by A51,A53,FINSEQ_3:31;
then consider i', j' being Nat such that
A59: i' in dom F and
A60: j' in dom (F.i') and
A61: k = (Sum Card (F|(i'-'1))) + j' and
A62: (F.i').j' = (FlattenSeq F).k by POLYNOM1:32;
Card (G|(i-'1)) = (Card G)|(i-'1) &
Card (F|(i'-'1)) = (Card F)|(i'-'1) by POLYNOM3:16;
then A63: i = i' & j = j' by A50,A55,A56,A57,A59,A60,A61,POLYNOM3:22;
consider a1', b1' being Element of Bags o1,
Gi being FinSequence of 2-tuples_on Bags(o1+^o2) such that
A64: Gi = G/.i and
A65: (decomp b1)/.i = <*a1', b1'*> and
A66: len Gi = len decomp b2 and
A67: for m being Nat st m in dom Gi
ex a1'',b1'' being Element of Bags o2 st
(decomp b2)/.m = <*a1'', b1''*> &
Gi/.m =<*a1'+^a1'',b1'+^b1''*> by A1,A2,A55;
A68: j in dom Gi by A55,A56,A64,FINSEQ_4:def 4;
then consider a1'',b1'' being Element of Bags o2 such that
A69: (decomp b2)/.j = <*a1'', b1''*> and
A70: Gi/.j =<*a1'+^a1'',b1'+^b1''*> by A67;
consider fa1 being Element of Bags o1,
Fk being FinSequence of Bags(o1+^o2) such that
A71: Fk = F/.i and
A72: (divisors b1)/.i = fa1 and len Fk = len divisors b2 and
A73: for m being Nat st m in dom Fk
ex fa1' being Element of Bags o2 st
(divisors b2)/.m = fa1' & Fk/.m = fa1+^fa1' by A1,A18,A36,A55;
A74: j in dom Fk by A59,A60,A63,A71,FINSEQ_4:def 4;
then consider fa1' being Element of Bags o2 such that
A75: (divisors b2)/.j = fa1' and
A76: Fk/.j = fa1+^fa1' by A73;
A77: a1' = fa1 by A1,A55,A65,A72,POLYNOM1:74;
A78: j in dom decomp b2 by A66,A68,FINSEQ_3:31;
then A79: a1'' = fa1' by A69,A75,POLYNOM1:74;
reconsider b1a1 = b1-'a1' as Element of Bags o1 by POLYNOM1:def 14;
reconsider b2a1 = b2-'a1'' as Element of Bags o2 by POLYNOM1:def 14;
k in dom FlattenSeq F by A51,A53,FINSEQ_3:31;
then A80: p = F.i.j by A34,A54,A62,A63,FINSEQ_4:def 4
.= Fk.j by A59,A63,A71,FINSEQ_4:def 4
.= a1'+^a1'' by A74,A76,A77,A79,FINSEQ_4:def 4;
A81: <*a1', b1'*> = <*a1', b1-'a1'*> by A1,A55,A65,A72,A77,POLYNOM1:def 19;
A82: <*a1'', b1''*> = <*a1'', b2-'a1''*> by A69,A75,A78,A79,POLYNOM1:def 19;
A83: bb-'p = b1a1 +^ b2a1 by A80,Th13
.= b1'+^ b2a1 by A81,GROUP_7:2
.= b1'+^ b1'' by A82,GROUP_7:2;
thus FG/.k = (G.i).j by A53,A58,FINSEQ_4:def 4
.= Gi.j by A55,A64,FINSEQ_4:def 4
.= <*p, bb-'p*> by A68,A70,A80,A83,FINSEQ_4:def 4;
end;
hence decomp(b1+^b2) = FlattenSeq G by A52,POLYNOM1:def 19;
end;
theorem
for o1,o2 be non empty Ordinal,
L be Abelian right_zeroed add-associative right_complementable
unital distributive associative well-unital
non trivial (non empty doubleLoopStr)
holds Polynom-Ring (o1,Polynom-Ring(o2,L)),Polynom-Ring (o1+^o2,L)
are_isomorphic
proof
let o1,o2 be non empty Ordinal,
L be Abelian right_zeroed add-associative right_complementable
unital distributive associative well-unital
non trivial (non empty doubleLoopStr);
set P2 = Polynom-Ring (o1+^o2,L),
P1 = Polynom-Ring (o1,Polynom-Ring(o2,L));
defpred R[set,set] means for P be Polynomial of o1,Polynom-Ring(o2,L) st
$1=P holds $2 = Compress P;
A1: for x being Element of P1
ex u being Element of P2 st R[x,u]
proof
let x be Element of P1;
reconsider Q=x as Polynomial of o1,Polynom-Ring(o2,L)
by POLYNOM1:def 27;
reconsider u = Compress Q as Element of P2
by POLYNOM1:def 27;
take u;
let P be Polynomial of o1,Polynom-Ring(o2,L);
assume x=P;
hence u = Compress P;
end;
consider f be Function of the carrier of P1, the carrier of P2
such that
A2: for x be Element of P1 holds R[x,f.x] from FuncExD(A1);
reconsider f as map of P1,P2;
take f;
thus A3: f is additive
proof
let x,y be Element of P1;
reconsider x' =x, y'= y as Element of P1;
reconsider p =x', q= y' as Polynomial of o1,Polynom-Ring(o2,L)
by POLYNOM1:def 27;
reconsider fp =f.x, fq= f.y, fpq = f.(x+y) as Element of P2
;
reconsider fp, fq, fpq as Polynomial of o1+^o2,L by POLYNOM1:def 27;
for x being bag of o1+^o2 holds fpq.x = fp.x+fq.x
proof
let b be bag of o1+^o2;
reconsider b'= b as Element of Bags (o1+^o2) by POLYNOM1:def 14;
consider b1 be Element of Bags o1,
b2 be Element of Bags o2,
Q1 be Polynomial of o2,L such that
A4: Q1=p.b1 and
A5: b' = b1+^b2 and
A6: (Compress p).b'=Q1.b2 by Def2;
consider b1' be Element of Bags o1,
b2' be Element of Bags o2,
Q1' be Polynomial of o2,L such that
A7: Q1'=q.b1' and
A8: b' = b1'+^b2' and
A9: (Compress q).b'=Q1'.b2' by Def2;
consider b1'' be Element of Bags o1,
b2'' be Element of Bags o2,
Q1'' be Polynomial of o2,L such that
A10: Q1''=(p+q).b1'' and
A11: b' = b1''+^b2'' and
A12: (Compress (p + q)).b'=Q1''.b2'' by Def2;
reconsider b1 as bag of o1;
A13: b1=b1' & b1'=b1'' & b1 = b1'' & b2=b2' & b2'=b2'' & b2 = b2''
by A5,A8,A11,Th7;
(p+q).b1 = p.b1+q.b1 by POLYNOM1:def 21;
then Q1''= Q1+ Q1' by A4,A7,A10,A13,POLYNOM1:def 27;
then A14: Q1''.b2 = Q1.b2 + Q1'.b2 by POLYNOM1:def 21;
x + y = p + q by POLYNOM1:def 27;
hence fpq.b = (Compress (p + q)).b' by A2
.= (Compress p).b'+fq.b by A2,A6,A9,A12,A13,A14
.= fp.b+fq.b by A2;
end;
hence f.(x+y) = (fp)+(fq) by POLYNOM1:def 21
.=(f.x)+(f.y) by POLYNOM1:def 27;
end;
thus A15: f is multiplicative
proof
let x,y be Element of P1;
reconsider x' =x, y'= y as Element of P1;
reconsider p =x', q= y' as Polynomial of o1,Polynom-Ring(o2,L)
by POLYNOM1:def 27;
reconsider fp =f.x, fq= f.y as Element of P2;
reconsider fp, fq as Polynomial of o1+^o2,L by POLYNOM1:def 27;
f.(x*y)=f.(p*'q) by POLYNOM1:def 27;
then reconsider fpq' = f.(p*'q) as Polynomial of o1+^o2, L by POLYNOM1:def 27
;
A16: for b being bag of o1+^o2
ex s being FinSequence of the carrier of L st
fpq'.b = Sum s &
len s = len decomp b &
for k being Nat st k in dom s
ex b1, b2 being bag of o1+^o2 st (decomp b)/.k = <*b1, b2*> &
s/.k = fp.b1*fq.b2
proof
let c be bag of (o1+^o2);
reconsider b=c as Element of Bags (o1+^o2) by POLYNOM1:def 14;
consider b1 be Element of Bags o1, b2 be Element of Bags o2
such that
A17: b = b1+^b2 by Th6;
reconsider b1 as bag of o1;
consider r being FinSequence of the carrier of Polynom-Ring(o2,L)
such that
A18: (p*'q).b1 = Sum r and
A19: len r = len decomp b1 and
A20: for k being Nat st k in dom r
ex a1', b1' being bag of o1 st (decomp b1)/.k = <*a1', b1'*> &
r/.k = (p.a1')*(q.b1') by POLYNOM1:def 26;
defpred P[set,set] means
ex a1', b1' being bag of o1, Fk being FinSequence of the carrier of L,
pa1', qb1' being Polynomial of o2,L
st pa1' = p.a1' & qb1' = q.b1' & Fk = $2 &
(decomp b1)/.$1 = <*a1', b1'*> &
len Fk = len decomp b2 &
for m being Nat st m in dom Fk
ex a1'',b1'' being bag of o2 st (decomp b2)/.m = <*a1'', b1''*> &
Fk/.m =pa1'.a1''*qb1'.b1'';
A21: for k being Nat st k in Seg len r
ex x being Element of (the carrier of L)* st P[k,x]
proof
let k be Nat;
assume k in Seg len r;
then k in dom decomp b1 by A19,FINSEQ_1:def 3;
then consider a1',b1' being bag of o1 such that
A22: (decomp b1)/.k = <*a1', b1'*> & b1 = a1' + b1' by POLYNOM1:72;
reconsider pa1''=p.a1',qb1''=q.b1' as Element of
Polynom-Ring(o2,L);
reconsider pa1'=pa1'',qb1' = qb1'' as Polynomial of o2,L
by POLYNOM1:def 27;
defpred Q[set,set] means
ex a1'',b1'' being bag of o2 st (decomp b2)/.$1 = <*a1'', b1''*> &
$2 =pa1'.a1''*qb1'.b1'';
A23: for k being Nat st k in Seg len decomp b2
ex x being Element of L st Q[k,x]
proof
let k be Nat;
assume k in Seg len decomp b2;
then k in dom decomp b2 by FINSEQ_1:def 3;
then consider a1'',b1'' being bag of o2 such that
A24: (decomp b2)/.k = <*a1'', b1''*> & b2 = a1'' + b1''
by POLYNOM1:72;
reconsider x=pa1'.a1''*qb1'.b1'' as Element of L;
take x,a1'',b1'';
thus (decomp b2)/.k = <*a1'', b1''*> &
x =pa1'.a1''*qb1'.b1'' by A24;
end;
consider Fk being FinSequence of the carrier of L such that
A25: dom Fk = Seg len decomp b2 and
A26: for k being Nat st k in Seg len decomp b2 holds Q[k,Fk/.k]
from SeqExD(A23);
reconsider x=Fk as Element of (the carrier of L)* by FINSEQ_1:def 11;
take x,a1',b1',Fk,pa1',qb1';
thus pa1' = p.a1' & qb1' = q.b1' & Fk = x;
thus (decomp b1)/.k = <*a1', b1'*> by A22;
thus len Fk = len decomp b2 by A25,FINSEQ_1:def 3;
let m be Nat;
assume m in dom Fk;
hence thesis by A25,A26;
end;
consider F being FinSequence of (the carrier of L)* such that
A27: dom F = Seg len r and
A28: for k being Nat st k in Seg len r holds
P[k,F/.k] from SeqExD(A21);
take s = FlattenSeq F;
reconsider x = p*'q as Element of P1 by POLYNOM1:def 27;
consider c1 be Element of Bags o1,
c2 be Element of Bags o2,
Q1 be Polynomial of o2,L such that
A29: Q1=(p*'q).c1 and
A30: b = c1+^c2 and
A31: (Compress(p*'q)).b = Q1.c2 by Def2;
A32: b1=c1 & b2=c2 by A17,A30,Th7;
reconsider Sr = Sum r as Polynomial of o2,L by POLYNOM1:def 27;
for x be set st x in dom r holds r.x is Function
proof
let x be set;
assume x in dom r;
then A33: r.x in rng r by FUNCT_1:12;
rng r c= the carrier of Polynom-Ring(o2,L) by FINSEQ_1:def 4;
hence r.x is Function by A33,POLYNOM1:def 27;
end;
then reconsider rFF = r as Function-yielding Function by PRALG_1:def 15;
deffunc F(set) = (rFF.$1).b2;
consider rFFb2 being Function such that
A34: dom rFFb2 = dom r and
A35: for i being set st i in dom r holds rFFb2.i = F(i) from Lambda;
consider i be Nat such that
A36: dom r = Seg i by FINSEQ_1:def 2;
reconsider rFFb2 as FinSequence by A34,A36,FINSEQ_1:def 2;
rng rFFb2 c= the carrier of L
proof let u be set;
assume u in rng rFFb2;
then consider x be set such that
A37: x in dom rFFb2 and
A38: u = rFFb2.x by FUNCT_1:def 5;
A39: rFFb2.x = (rFF.x).b2 by A34,A35,A37;
A40: rFF.x in rng rFF by A34,A37,FUNCT_1:12;
rng rFF c= the carrier of Polynom-Ring(o2,L) by FINSEQ_1:def 4;
then A41: rFF.x is Function of Bags o2, the carrier of L
by A40,POLYNOM1:def 27;
then A42: rng (rFF.x) c= the carrier of L by RELSET_1:12;
dom (rFF.x) = Bags o2 by A41,FUNCT_2:def 1;
then (rFF.x).b2 in rng (rFF.x) by FUNCT_1:12;
hence u in the carrier of L by A38,A39,A42;
end;
then reconsider rFFb2 as FinSequence of the carrier of L by FINSEQ_1:def
4;
A43: len(Sum F) = len F by MATRLIN:def 8;
A44: dom rFFb2 = dom F by A27,A34,FINSEQ_1:def 3
.= dom(Sum F) by A43,FINSEQ_3:31;
for k being Nat st k in dom rFFb2 holds rFFb2.k = (Sum F).k
proof let k be Nat such that
A45: k in dom rFFb2;
consider c1, d1 being bag of o1 such that
A46: (decomp b1)/.k = <*c1, d1*> and
A47: r/.k = (p.c1)*(q.d1) by A20,A34,A45;
k in Seg len r by A34,A45,FINSEQ_1:def 3;
then consider a1', b1' being bag of o1,
Fk being FinSequence of the carrier of L,
pa1', qb1' being Polynomial of o2,L
such that
A48: pa1' = p.a1' & qb1' = q.b1' and
A49: Fk = F/.k and
A50: (decomp b1)/.k = <*a1', b1'*> and
A51: len Fk = len decomp b2 and
A52: for ki being Nat st ki in dom Fk
ex a1'',b1'' being bag of o2 st (decomp b2)/.ki = <*a1'', b1''*> &
Fk/.ki =pa1'.a1''*qb1'.b1'' by A28;
A53: c1=a1' & d1=b1' by A46,A50,GROUP_7:2;
A54: rFF.k = r/.k by A34,A45,FINSEQ_4:def 4
.= (pa1')*'(qb1') by A47,A48,A53,POLYNOM1:def 27;
consider s1 being FinSequence of the carrier of L such that
A55: (pa1')*'(qb1').b2 = Sum s1 and
A56: len s1 = len decomp b2 and
A57: for ki being Nat st ki in dom s1
ex x1, y2 being bag of o2 st (decomp b2)/.ki = <*x1, y2*> &
s1/.ki = (pa1'.x1)*(qb1'.y2) by POLYNOM1:def 26;
now let ki be Nat;
assume A58:ki in Seg len s1;
then A59: ki in dom s1 by FINSEQ_1:def 3;
then consider x1, y2 being bag of o2 such that
A60: (decomp b2)/.ki = <*x1, y2*> and
A61: s1/.ki = (pa1'.x1)*(qb1'.y2) by A57;
A62: ki in dom Fk by A51,A56,A58,FINSEQ_1:def 3;
then consider a1'',b1'' being bag of o2 such that
A63: (decomp b2)/.ki = <*a1'', b1''*> and
A64: Fk/.ki =pa1'.a1''*qb1'.b1'' by A52;
A65: x1=a1'' & y2=b1'' by A60,A63,GROUP_7:2;
s1/.ki = s1.ki by A59,FINSEQ_4:def 4;
hence s1.ki = Fk.ki by A61,A62,A64,A65,FINSEQ_4:def 4;
end;
then A66: s1=Fk by A51,A56,FINSEQ_2:10;
thus rFFb2.k = (rFF.k).b2 by A34,A35,A45
.= (Sum F)/.k by A44,A45,A49,A54,A55,A66,MATRLIN:def 8
.= (Sum F).k by A44,A45,FINSEQ_4:def 4;
end;
then A67: rFFb2 = Sum F by A44,FINSEQ_1:17;
consider gg being Function of NAT, the carrier of Polynom-Ring(o2,L)
such that
A68: Sum r = gg.(len r) and
A69: gg.0 = 0.Polynom-Ring(o2,L) and
A70: for j being Nat, v being Element of Polynom-Ring(o2,L)
st j < len r & v = r.(j + 1) holds gg.(j + 1) = gg.j + v
by RLVECT_1:def 12;
defpred R[Nat,set] means
for pp being Polynomial of o2,L st $1 <= len r & pp=gg.$1
holds $2 = pp.b2;
A71: for x being Nat ex y being Element of L st R[x,y]
proof
let x be Nat;
reconsider pp' = gg.x as Polynomial of o2,L by POLYNOM1:def 27;
take y = pp'.b2;
let pp be Polynomial of o2,L;
assume x <= len r & pp=gg.x;
hence y = pp.b2;
end;
consider ff being Function of NAT,the carrier of L such that
A72: for j being Nat holds R[j,ff.j] from FuncExD(A71);
len rFFb2 = len r by A34,FINSEQ_3:31;
then A73: Sr.b2 = ff.(len rFFb2) by A68,A72;
A74: gg.0 = 0_(o2,L) by A69,POLYNOM1:def 27;
0 <= len r by NAT_1:18;
then A75: ff.0 = (0_(o2,L)).b2 by A72,A74
.= 0.L by POLYNOM1:81;
for j being Nat,v being Element of L
st j < len rFFb2 & v = rFFb2.(j + 1)
holds ff.(j + 1) = ff.j + v
proof
let j being Nat,v being Element of L;
assume A76: j < len rFFb2 & v = rFFb2.(j + 1);
then A77: j < len r by A34,FINSEQ_3:31;
reconsider w = r/.(j+1),pp = gg.j, pp' = gg.(j+1)
as Polynomial of o2,L by POLYNOM1:def 27;
reconsider w1 = w, pp1 = pp, pp1' = pp'
as Element of Polynom-Ring(o2,L);
reconsider w1, pp1, pp1'
as Element of Polynom-Ring(o2,L);
A78: 1 <= j+1 by NAT_1:29;
A79: j+1 <= len r by A77,NAT_1:38;
then A80: w = r.(j+1) by A78,FINSEQ_4:24;
j + 1 in dom r by A78,A79,FINSEQ_3:27;
then A81: w.b2 = v by A35,A76,A80;
A82: j+1 <= len r by A77,NAT_1:38;
A83: pp1' = pp1 + w1 by A70,A77,A80;
thus ff.(j + 1) = pp'.b2 by A72,A82
.= (pp + w).b2 by A83,POLYNOM1:def 27
.= pp.b2 + w.b2 by POLYNOM1:def 21
.= ff.j + v by A72,A77,A81;
end;
then A84: Sr.b2 = Sum rFFb2 by A73,A75,RLVECT_1:def 12;
f.x = Compress(p*'q) by A2;
hence fpq'.c = Sum s by A18,A29,A31,A32,A67,A84,POLYNOM1:34;
defpred VV[set,set] means
ex a1', b1' being Element of Bags o1,
Fk being FinSequence of 2-tuples_on Bags(o1+^o2)
st Fk = $2 & (decomp b1)/.$1 = <*a1', b1'*> &
len Fk = len decomp b2 &
for m being Nat st m in dom Fk
ex a1'',b1'' being Element of Bags o2 st
(decomp b2)/.m = <*a1'', b1''*> &
Fk/.m =<*a1'+^a1'',b1'+^b1''*>;
A85: for i being Nat st i in Seg len r
ex x being Element of (2-tuples_on Bags(o1+^o2))* st VV[i,x]
proof
let k be Nat;
assume k in Seg len r;
then k in dom decomp b1 by A19,FINSEQ_1:def 3;
then consider a1',b1' being bag of o1 such that
A86: (decomp b1)/.k = <*a1', b1'*> & b1 = a1' + b1' by POLYNOM1:72;
reconsider a1',b1' as Element of Bags o1 by POLYNOM1:def 14;
defpred Q[set,set] means
ex a1'',b1'' being Element of Bags o2 st
(decomp b2)/.$1 = <*a1'', b1''*> &
$2 =<*a1'+^a1'',b1'+^b1''*>;
A87: for k being Nat st k in Seg len decomp b2
ex x being Element of 2-tuples_on Bags(o1+^o2) st Q[k,x]
proof
let k be Nat;
assume k in Seg len decomp b2;
then k in dom decomp b2 by FINSEQ_1:def 3;
then consider a1'',b1'' being bag of o2 such that
A88: (decomp b2)/.k = <*a1'', b1''*> & b2 = a1'' + b1'' by POLYNOM1:72;
reconsider a1'',b1'' as Element of Bags o2 by POLYNOM1:def 14;
reconsider x = <*a1'+^a1'',b1'+^b1''*>
as Element of 2-tuples_on Bags(o1+^o2);
take x;
take a1'',b1'';
thus (decomp b2)/.k = <*a1'', b1''*> &
x =<*a1'+^a1'',b1'+^b1''*> by A88;
end;
consider Fk being FinSequence of 2-tuples_on Bags(o1+^o2) such that
A89: dom Fk = Seg len decomp b2 and
A90: for k being Nat st k in Seg len decomp b2 holds Q[k,Fk/.k]
from SeqExD(A87);
reconsider x=Fk as Element of (2-tuples_on Bags(o1+^o2))*
by FINSEQ_1:def 11;
take x, a1', b1';
take Fk;
thus Fk = x;
thus (decomp b1)/.k = <*a1', b1'*> by A86;
thus len Fk = len decomp b2 by A89,FINSEQ_1:def 3;
let m be Nat;
assume m in dom Fk;
hence thesis by A89,A90;
end;
consider G being FinSequence of (2-tuples_on Bags(o1+^o2))* such that
A91: dom G = Seg len r and
A92: for i being Nat st i in Seg len r holds
VV[i,G/.i] from SeqExD(A85);
A93: dom Card G = dom G by CARD_3:def 2;
A94: dom Card F = dom F by CARD_3:def 2;
then A95: len Card F = len Card G by A27,A91,A93,FINSEQ_3:31;
for j be Nat st j in Seg len Card F holds (Card F).j = (Card G).j
proof
let j be Nat;
assume A96:j in Seg len Card F;
then A97: j in dom Card F by FINSEQ_1:def 3;
A98: j in dom Card G by A27,A91,A93,A94,A96,FINSEQ_1:def 3;
A99: j in dom F by A97,CARD_3:def 2;
A100: j in dom G by A27,A91,A94,A96,FINSEQ_1:def 3;
A101: (Card F).j = Card(F.j) by A99,CARD_3:def 2;
consider a1', b1' being bag of o1,
Fk being FinSequence of the carrier of L,
pa1', qb1' being Polynomial of o2,L such that
pa1' = p.a1' & qb1' = q.b1' and
A102: Fk = F/.j and
(decomp b1)/.j = <*a1', b1'*> and
A103: len Fk = len decomp b2 and
for m being Nat st m in dom Fk
ex a1'',b1'' being bag of o2 st (decomp b2)/.m = <*a1'', b1''*> &
Fk/.m =pa1'.a1''*qb1'.b1'' by A27,A28,A99;
consider a2', b2' being Element of Bags o1,
Gk being FinSequence of 2-tuples_on Bags(o1+^o2) such that
A104: Gk = G/.j and (decomp b1)/.j = <*a2', b2'*> and
A105: len Gk = len decomp b2 and
for m being Nat st m in dom Gk
ex a2'',b2'' being Element of Bags o2 st
(decomp b2)/.m = <*a2'', b2''*> &
Gk/.m =<*a2'+^a2'',b2'+^b2''*> by A27,A92,A99;
Card(F.j) = Card(F/.j) by A99,FINSEQ_4:def 4
.= Card(G.j) by A93,A98,A102,A103,A104,A105,FINSEQ_4:def 4;
hence (Card F).j = (Card G).j by A100,A101,CARD_3:def 2;
end;
then A106: Card F = Card G by A95,FINSEQ_2:10;
A107: c1 = b1 & c2 = b2 by A17,A30,Th7;
then dom G = dom decomp c1 by A19,A91,FINSEQ_1:def 3;
then A108: decomp c = FlattenSeq G by A30,A91,A92,A107,Th14;
hence
A109: len s = len decomp c by A106,POLYNOM1:31;
let k be Nat;
assume
A110: k in dom s;
then A111: k in dom decomp c by A109,FINSEQ_3:31;
then consider c1, c2 being bag of o1+^o2 such that
A112: (decomp c)/.k = <*c1, c2*> and c = c1+c2 by POLYNOM1:72;
take c1,c2;
thus (decomp c)/.k = <*c1, c2*> by A112;
consider i, j being Nat such that
A113: i in dom F & j in dom (F.i) and
A114: k = Sum (Card (F|(i-'1))) + j and
A115: (F.i).j = (FlattenSeq F).k by A110,POLYNOM1:32;
consider i', j' being Nat such that
A116: i' in dom G & j' in dom (G.i') and
A117: k = Sum (Card (G|(i'-'1))) + j' and
A118: (G.i').j' = (decomp c).k by A108,A111,POLYNOM1:32;
(Sum ((Card F)|(i-'1))) + j = Sum (Card(F|(i-'1))) + j by POLYNOM3:16
.= (Sum ((Card G)|(i'-'1))) + j' by A114,A117,POLYNOM3:16;
then A119: i = i' & j = j' by A106,A113,A116,POLYNOM3:22;
consider a1', b1' being bag of o1,
Fk being FinSequence of the carrier of L,
pa1', qb1' being Polynomial of o2,L such that
A120: pa1' = p.a1' and
A121: qb1' = q.b1' and
A122: Fk = F/.i and
A123: (decomp b1)/.i = <*a1', b1'*> and
len Fk = len decomp b2 and
A124: for m being Nat st m in dom Fk
ex a1'',b1'' being bag of o2 st (decomp b2)/.m = <*a1'', b1''*> &
Fk/.m =pa1'.a1''*qb1'.b1'' by A27,A28,A113;
consider ga1', gb1' being Element of Bags o1,
Gk being FinSequence of 2-tuples_on Bags(o1+^o2) such that
A125: Gk = G/.i and
A126: (decomp b1)/.i = <*ga1', gb1'*> and
len Gk = len decomp b2 and
A127: for m being Nat st m in dom Gk
ex ga1'',gb1'' being Element of Bags o2 st
(decomp b2)/.m = <*ga1'', gb1''*> &
Gk/.m =<*ga1'+^ga1'',gb1'+^gb1''*> by A27,A92,A113;
A128: Gk = G.i by A27,A91,A113,A125,FINSEQ_4:def 4;
then consider ga1'',gb1'' be Element of Bags o2 such that
A129: (decomp b2)/.j = <*ga1'', gb1''*> and
A130: Gk/.j =<*ga1'+^ga1'',gb1'+^gb1''*> by A116,A119,A127;
A131: Fk = F.i by A113,A122,FINSEQ_4:def 4;
j in dom Fk by A113,A122,FINSEQ_4:def 4;
then consider a1'',b1'' be bag of o2 such that
A132: (decomp b2)/.j = <*a1'', b1''*> and
A133: Fk/.j =pa1'.a1''*qb1'.b1'' by A124;
<*c1,c2*> = G.i.j by A111,A112,A118,A119,FINSEQ_4:def 4
.= <*ga1'+^ga1'',gb1'+^gb1''*> by A116,A119,A128,A130,FINSEQ_4:def
4;
then A134: c1 = ga1' +^ ga1'' & c2 = gb1' +^ gb1'' by GROUP_7:2;
reconsider cc1=c1, cc2=c2 as Element of Bags(o1+^o2) by POLYNOM1:def 14;
consider cb1 be Element of Bags o1,
cb2 be Element of Bags o2,
Q1 be Polynomial of o2,L such that
A135: Q1=p.cb1 and
A136: cc1 = cb1+^cb2 and
A137: (Compress p).cc1=Q1.cb2 by Def2;
A138: cb1 = ga1' & cb2 = ga1'' by A134,A136,Th7;
A139: a1'' = ga1'' & b1'' = gb1'' by A129,A132,GROUP_7:2;
A140: a1' = ga1' & b1' = gb1' by A123,A126,GROUP_7:2;
then A141: pa1'.a1'' = fp.c1 by A2,A120,A135,A137,A138,A139;
consider cb1 be Element of Bags o1,
cb2 be Element of Bags o2,
Q1 be Polynomial of o2,L such that
A142: Q1=q.cb1 and
A143: cc2 = cb1+^cb2 and
A144: (Compress q).cc2=Q1.cb2 by Def2;
cb1 = gb1' & cb2 = gb1'' by A134,A143,Th7;
then A145: qb1'.b1'' = fq.c2 by A2,A121,A139,A140,A142,A144;
thus s/.k = s.k by A110,FINSEQ_4:def 4
.= fp.c1*fq.c2 by A113,A115,A131,A133,A141,A145,FINSEQ_4:def 4;
end;
thus f.(x*y) = f.(p*'q) by POLYNOM1:def 27
.= (fp)*'(fq) by A16,POLYNOM1:def 26
.=(f.x)*(f.y) by POLYNOM1:def 27;
end;
reconsider 1P1 = 1_ P1 as Polynomial of o1,Polynom-Ring(o2,L)
by POLYNOM1:def 27;
reconsider 1P2 = 1_ P2 as Polynomial of o1+^o2,L
by POLYNOM1:def 27;
A146: for b being Element of Bags(o1+^o2) holds
(Compress 1P1).b = (1P2).b
proof
let b be Element of Bags(o1+^o2);
consider b1 be Element of Bags o1,
b2 be Element of Bags o2,
Q1 be Polynomial of o2,L such that
A147: Q1=1P1.b1 and
A148: b = b1+^b2 and
A149: (Compress 1P1).b = Q1.b2 by Def2;
A150: 1P2.b = (1_(o1+^o2,L)).b by POLYNOM1:def 27;
per cases;
suppose
A151: b = EmptyBag(o1+^o2);
then A152: b2 = EmptyBag o2 by A148,Th5;
A153: b1 = EmptyBag o1 by A148,A151,Th5;
Q1 = 1_(o1,Polynom-Ring(o2,L)).b1 by A147,POLYNOM1:def 27
.=1.Polynom-Ring(o2,L) by A153,POLYNOM1:84
.=1_(Polynom-Ring(o2,L)) by POLYNOM2:3;
then Q1.b2 = (1_(o2,L)).b2 by POLYNOM1:def 27
.= 1.L by A152,POLYNOM1:84
.=1P2.b by A150,A151,POLYNOM1:84;
hence (Compress 1P1).b = (1P2).b by A149;
suppose A154:b <> EmptyBag(o1+^o2);
then A155: (b1 <> EmptyBag o1) or (b2 <> EmptyBag o2) by A148,Th5;
now per cases;
suppose A156: b1 = EmptyBag o1;
Q1 = 1_(o1,Polynom-Ring(o2,L)).b1 by A147,POLYNOM1:def 27
.=1.Polynom-Ring(o2,L) by A156,POLYNOM1:84
.=1_(Polynom-Ring(o2,L)) by POLYNOM2:3
.=1_(o2,L) by POLYNOM1:def 27;
then Q1.b2 = 0.L by A155,A156,POLYNOM1:84
.=1P2.b by A150,A154,POLYNOM1:84;
hence (Compress 1P1).b = (1P2).b by A149;
suppose A157:b1 <> EmptyBag o1;
Q1 = 1_(o1,Polynom-Ring(o2,L)).b1 by A147,POLYNOM1:def 27
.=0.Polynom-Ring(o2,L) by A157,POLYNOM1:84
.=0_(o2,L) by POLYNOM1:def 27;
then Q1.b2 = 0.L by POLYNOM1:81
.=1P2.b by A150,A154,POLYNOM1:84;
hence (Compress 1P1).b = (1P2).b by A149;
end;
hence (Compress 1P1).b = (1P2).b;
end;
f.1_ P1 = Compress 1P1 by A2
.= 1_ P2 by A146,FUNCT_2:113;
hence A158: f is unity-preserving by ENDALG:def 8;
thus f is one-to-one
proof
let x1,x2 be set;
assume A159: x1 in dom f;
assume A160: x2 in dom f;
assume A161: f.x1 = f.x2;
reconsider x1'=x1 as Element of P1 by A159,FUNCT_2:def 1;
reconsider x1''=x1' as Polynomial of o1,Polynom-Ring(o2,L)
by POLYNOM1:def 27;
reconsider x2'=x2 as Element of P1 by A160,FUNCT_2:def 1;
reconsider x2''=x2' as Polynomial of o1,Polynom-Ring(o2,L)
by POLYNOM1:def 27;
A162: f.x2'=Compress x2'' by A2;
A163: f.x1'=Compress x1'' by A2;
then reconsider w1=f.x1' as Polynomial of o1+^o2,L;
reconsider w2=f.x2' as Polynomial of o1+^o2,L by A162;
now let b1 be Element of Bags o1;
reconsider x1''b1 = x1''.b1, x2''b1 = x2''.b1 as Polynomial of o2,L
by POLYNOM1:def 27;
now let b2 be Element of Bags o2;
set b = b1 +^b2;
consider b1' be Element of Bags o1,
b2' be Element of Bags o2,
Q1 be Polynomial of o2,L such that
A164: Q1=x1''.b1' and
A165: b = b1'+^b2' and
A166: w1.b=Q1.b2' by A163,Def2;
consider c1 be Element of Bags o1,
c2 be Element of Bags o2,
Q1' be Polynomial of o2,L such that
A167: Q1'=x2''.c1 and
A168: b = c1+^c2 and
A169: w2.b=Q1'.c2 by A162,Def2;
b1=b1'& b1=c1 & b2=b2' & b2=c2 & b1'=c1 & b2'=c2 by A165,A168,Th7;
hence x1''b1.b2 = x2''b1.b2 by A161,A164,A166,A167,A169;
end;
hence x1''.b1 = x2''.b1 by FUNCT_2:113;
end;
hence x1 = x2 by FUNCT_2:113;
end;
thus f is RingHomomorphism by A3,A15,A158,QUOFIELD:def 21;
thus rng f c= the carrier of P2 by RELSET_1:12;
thus the carrier of P2 c= rng f
proof
let y be set;
assume
y in the carrier of P2;
then reconsider s = y as Polynomial of o1+^o2,L by POLYNOM1:def 27;
defpred K[Element of Bags o1,Element of Polynom-Ring(o2,L)]
means
ex h be Function st h = $2 &
for b2 be Element of Bags o2, b be Element of Bags (o1+^o2)
st b = $1 +^b2 holds h.b2 = s.b;
A170:for x being Element of Bags o1
ex y being Element of Polynom-Ring(o2,L) st K[x,y]
proof
let x being Element of Bags o1;
reconsider b1 = x as Element of Bags o1;
defpred L[Element of Bags o2,Element of L] means
for b being Element of Bags (o1+^o2)
st b = b1 +^$1 holds $2 = s.b;
A171: for p being Element of Bags o2 ex q being Element of L
st L[p,q]
proof
let p being Element of Bags o2;
take q = s.(b1+^p);
let b being Element of Bags (o1+^o2);
assume b = b1 +^p;
hence q = s.b;
end;
consider t being Function of Bags o2, the carrier of L such that
A172: for b2 be Element of Bags o2 holds L[b2,t.b2] from FuncExD(A171);
reconsider t as Function of Bags o2, L;
defpred KK[set,set] means
ex b1 being Element of Bags o1, b2 being Element of Bags o2
st $1 = b1 +^b2 & $2 = b2;
A173: for x being Element of Bags(o1+^o2)
ex y being Element of Bags o2 st KK[x,y]
proof
let x being Element of Bags(o1+^o2);
consider b1 be Element of Bags o1, b2 be Element of Bags o2
such that
A174: x = b1+^b2 by Th6;
reconsider y = b2 as Element of Bags o2;
take y,b1,b2;
thus x = b1 +^b2 by A174;
thus y = b2;
end;
consider kk being Function of Bags(o1+^o2), Bags o2 such that
A175: for b being Element of Bags(o1+^o2) holds KK[b,kk.b]
from FuncExD(A173);
Support t c= kk.:Support s
proof
let x be set;
assume A176: x in Support t;
then A177: t.x<>0.L by POLYNOM1:def 9;
reconsider b2 = x as Element of Bags o2 by A176;
set b = b1+^b2;
A178: dom kk = Bags (o1+^o2) by FUNCT_2:def 1;
s.b<>0.L by A172,A177;
then A179: b in Support s by POLYNOM1:def 9;
consider b1' being Element of Bags o1, b2' being Element of Bags o2
such that
A180: b = b1'+^b2' and
A181: kk.b = b2' by A175;
x = kk.b by A180,A181,Th7;
hence x in kk.:Support s by A178,A179,FUNCT_1:def 12;
end;
then Support t is finite by FINSET_1:13;
then t is Polynomial of o2,L by POLYNOM1:def 10;
then reconsider t''=t as Element of Polynom-Ring(o2,L)
by POLYNOM1:def 27;
reconsider t' = t as Function;
take t'',t';
thus t'' =t';
let b2 be Element of Bags o2, b be Element of Bags (o1+^o2);
assume b = x +^b2;
hence t'.b2 = s.b by A172;
end;
consider g be Function of Bags o1,the carrier of Polynom-Ring(o2,L) such that
A182: for x being Element of Bags o1 holds K[x,g.x] from FuncExD(A170);
reconsider g as Function of Bags o1,Polynom-Ring(o2,L);
defpred KK[set,set] means
ex b1 being Element of Bags o1, b2 being Element of Bags o2
st $1 = b1 +^b2 & $2 = b1;
A183: for x being Element of Bags(o1+^o2)
ex y being Element of Bags o1 st KK[x,y]
proof
let x being Element of Bags(o1+^o2);
consider b1 be Element of Bags o1, b2 be Element of Bags o2
such that
A184: x = b1+^b2 by Th6;
reconsider y = b1 as Element of Bags o1;
take y,b1,b2;
thus x = b1 +^b2 by A184;
thus y = b1;
end;
consider kk being Function of Bags(o1+^o2), Bags o1 such that
A185: for b being Element of Bags(o1+^o2) holds KK[b,kk.b]
from FuncExD(A183);
Support g c= kk.:Support s
proof
let x be set;
assume A186:x in Support g;
then reconsider b1 = x as Element of Bags o1;
consider h be Function such that
A187: h = g.b1 and
A188: for b2 be Element of Bags o2, b be Element of Bags (o1+^o2)
st b = b1 +^b2 holds h.b2 = s.b by A182;
g.b1<>0.Polynom-Ring(o2,L) by A186,POLYNOM1:def 9;
then A189: g.b1<>0_(o2,L) by POLYNOM1:def 27;
reconsider h as Polynomial of o2,L by A187,POLYNOM1:def 27;
Support h <> {} by A187,A189,POLYNOM2:19;
then consider b2 be Element of Bags o2 such that
A190: b2 in Support h by SUBSET_1:10;
set b = b1+^b2;
A191: dom kk = Bags (o1+^o2) by FUNCT_2:def 1;
h.b2 <> 0.L by A190,POLYNOM1:def 9;
then s.b <> 0.L by A188;
then A192: b in Support s by POLYNOM1:def 9;
consider b1' being Element of Bags o1, b2' being Element of Bags o2
such that
A193: b = b1'+^b2' and
A194: kk.b = b1' by A185;
x = kk.b by A193,A194,Th7;
hence x in kk.:Support s by A191,A192,FUNCT_1:def 12;
end;
then A195: Support g is finite by FINSET_1:13;
then g is Polynomial of o1,Polynom-Ring(o2,L) by POLYNOM1:def 10;
then reconsider g as Element of P1 by POLYNOM1:def 27;
reconsider g' = g as Polynomial of o1,Polynom-Ring(o2,L) by A195,POLYNOM1:def
10;
A196:dom f = the carrier of P1 by FUNCT_2:def 1;
now let b be Element of Bags (o1+^o2);
consider b1 be Element of Bags o1,
b2 be Element of Bags o2,
Q1 be Polynomial of o2,L such that
A197: Q1=g'.b1 and
A198: b = b1+^b2 and
A199: (Compress g').b=Q1.b2 by Def2;
consider h be Function such that
A200: h = g'.b1 and
A201: for b2 be Element of Bags o2, b be Element of Bags (o1+^o2)
st b = b1 +^b2 holds h.b2 = s.b by A182;
thus s.b = (Compress g').b by A197,A198,A199,A200,A201;
end;
then y = Compress g' by FUNCT_2:113
.= f.g by A2;
hence y in rng f by A196,FUNCT_1:12;
end;
end;