:: On polynomials with coefficients in a ring of polynomials
:: by Barbara Dzienis
::
:: Received August 10, 2001
:: Copyright (c) 2001-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, ORDINAL1, XBOOLE_0, ALGSTR_0, WELLORD1, QUOFIELD,
RELAT_1, FUNCT_1, SUBSET_1, STRUCT_0, ORDINAL2, TARSKI, ORDINAL3,
PRE_POLY, ARYTM_3, CARD_1, PBOOLE, FINSET_1, VALUED_0, FUNCOP_1,
RLVECT_1, LATTICES, BINOP_1, POLYNOM1, FINSEQ_1, CARD_3, PARTFUN1,
FINSEQ_2, NAT_1, VECTSP_1, ZFMISC_1, GROUP_1, SUPINF_2, XXREAL_0,
FINSEQ_3, ORDINAL4, ARYTM_1, ORDERS_1, MSSUBFAM, POLYNOM6;
notations TARSKI, XBOOLE_0, SUBSET_1, CARD_1, ORDINAL1, NUMBERS, XCMPLX_0,
VALUED_0, VECTSP_1, RELAT_1, FUNCT_1, PARTFUN1, FUNCT_2, FUNCOP_1,
POLYNOM1, STRUCT_0, ALGSTR_0, NAT_1, NAT_D, ORDERS_1, PBOOLE, RLVECT_1,
FINSET_1, FINSEQ_1, FINSEQ_2, ORDINAL2, ORDINAL3, GROUP_1, QUOFIELD,
GRCAT_1, WSIERP_1, PRE_POLY, FVSUM_1, POLYNOM3, GROUP_6, XXREAL_0,
MATRLIN;
constructors ORDINAL3, BINARITH, WSIERP_1, GRCAT_1, GROUP_6, TRIANG_1,
QUOFIELD, POLYNOM1, POLYNOM3, NAT_D, RELSET_1, MATRLIN, FVSUM_1,
RINGCAT1, MOD_4;
registrations FUNCT_1, ORDINAL1, RELSET_1, FUNCOP_1, FINSET_1, XREAL_0,
FINSEQ_1, FINSEQ_2, STRUCT_0, VECTSP_1, QUOFIELD, PRE_POLY, POLYNOM1,
POLYNOM2, VALUED_0, CARD_1;
requirements BOOLE, SUBSET, NUMERALS, REAL;
definitions VECTSP_1, QUOFIELD, FUNCT_1, TARSKI, XBOOLE_0, FUNCT_2, STRUCT_0,
VALUED_0, RINGCAT1, MOD_4;
equalities XBOOLE_0, STRUCT_0, ORDINAL1;
expansions FUNCT_1, XBOOLE_0;
theorems POLYNOM1, TOPGRP_1, FUNCT_2, PBOOLE, FUNCT_1, ORDINAL3, ORDINAL1,
ORDINAL2, FINSEQ_3, FINSEQ_2, FVSUM_1, FINSEQ_1, RELAT_1, FUNCOP_1,
POLYALG1, FINSEQ_5, VECTSP_1, FINSEQ_4, FINSET_1, TARSKI, POLYNOM2,
MATRLIN, RLVECT_1, NAT_1, SUBSET_1, CARD_3, POLYNOM3, ORDERS_1, RVSUM_1,
XBOOLE_0, XBOOLE_1, XREAL_1, GROUP_6, XXREAL_0, GROUP_1, PARTFUN1, NAT_D,
PRE_POLY;
schemes PBOOLE, FUNCT_2, FRAENKEL, FUNCT_1, RECDEF_1;
begin :: Preliminaries
reserve o1,o2 for Ordinal;
notation
let L1,L2 be non empty doubleLoopStr;
synonym L1,L2 are_isomorphic for L1 is_ringisomorph_to L2;
end;
definition
let L1,L2 be non empty doubleLoopStr;
redefine pred L1 is_ringisomorph_to L2; :: redefines is_ringisomorph_to (QUOFIELD, definition)
reflexivity
proof
let L1 be non empty doubleLoopStr;
take id L1;
thus id L1 is RingHomomorphism;
thus id L1 is one-to-one;
thus rng id L1 = [#]L1 by TOPGRP_1:1
.= the carrier of L1;
end;
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 object holds x in o1+^o2 iff x in o1 \/ B
proof
let x be object;
A2: x in o1 \/ B implies x in o1+^o2
proof
assume
A3: x in o1 \/ B;
per cases by A3,XBOOLE_0:def 3;
suppose
A4: x in o1;
o1 c= o1+^o2 by ORDINAL3:24;
hence thesis by A4;
end;
suppose
x in B;
then ex o be Ordinal st x=o1+^o & o in o2 by A1;
hence thesis by ORDINAL2:32;
end;
end;
per cases;
suppose
x in o1;
hence x in o1+^o2 implies x in o1 \/ B by XBOOLE_0:def 3;
thus thesis by A2;
end;
suppose
A5: not x in o1;
thus x in o1+^o2 implies x in o1 \/ B
proof
assume
A6: x in o1+^o2;
per cases;
suppose
o2 = {};
hence thesis by A5,A6,ORDINAL2:27;
end;
suppose
A7: o2 <> {};
reconsider o = x as Ordinal by A6;
o1 c= o by A5,ORDINAL1:16;
then
A8: o = o1 +^ (o -^ o1) by ORDINAL3:def 5;
o -^ o1 in o2 by A6,A7,ORDINAL3:60;
then x in B by A1,A8;
hence thesis by XBOOLE_0:def 3;
end;
end;
thus thesis by A2;
end;
end;
hence thesis by TARSKI:2;
end;
registration
let o1 be Ordinal, o2 be non empty Ordinal;
cluster o1 +^ o2 -> non empty;
coherence by ORDINAL3:26;
cluster o2 +^ o1 -> non empty;
coherence by ORDINAL3:26;
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 PRE_POLY:def 9;
take o;
now
assume
A3: not o in n;
then
A4: not o in dom b by PARTFUN1:def 2;
n = dom a by PARTFUN1:def 2;
then a.o = 0 by A3,FUNCT_1:def 2;
hence contradiction by A1,A4,FUNCT_1:def 2;
end;
hence o in n;
thus a.o < b.o by A1;
thus thesis 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 reconsider a9=a as Element of Bags (o1+^o2) by ORDINAL2:27;
take a9;
let o be Ordinal;
thus o in o1 implies a9.o = a.o;
o1+^o2 = o1 by A1,ORDINAL2:27;
hence thesis by XBOOLE_1:37;
end;
suppose
o2 <> {};
then reconsider o29 = o2 as non empty Ordinal;
defpred P[object,object] 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));
deffunc F(Element of o29) = o1 +^ $1;
set B = {F(o) where o is Element of o29: o in support b}, C = the set of
all o1 +^ o
where o is Element of o29;
A2: for i be object st i in o1+^o2 ex j be object st P[i,j]
proof
let i be object such that
A3: i in o1+^o2;
reconsider o = i as Ordinal by A3;
A4: o in o1 iff not o in (o1+^ o2)\o1 by A3,XBOOLE_0:def 5;
per cases by A3,XBOOLE_0:def 5;
suppose
A5: o in o1;
take a.o,o;
thus thesis by A5,XBOOLE_0:def 5;
end;
suppose
A6: o in (o1 +^o2)\o1;
take b.(o -^o1);
thus thesis by A4,A6;
end;
end;
consider f being ManySortedSet of o1+^o2 such that
A7: for i be object st i in o1+^o2 holds P[i,f.i] from PBOOLE:sch 3(A2);
A8: support f c= support a \/ B
proof
let x be object;
assume x in support f;
then
A9: f.x <> 0 by PRE_POLY:def 7;
then x in dom f by FUNCT_1:def 2;
then
A10: x in o1+^o2 by PARTFUN1:def 2;
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 o9 be Element of o29 st x = o1 +^ o9;
hence thesis;
end;
thus thesis;
end;
then
A11: x in o1 \/ C by A10,Th1;
per cases by A11,XBOOLE_0:def 3;
suppose
A12: x in o1;
P[x,f.x] by A7,A10;
then x in support a by A9,A12,PRE_POLY:def 7;
hence thesis by XBOOLE_0:def 3;
end;
suppose
x in C;
then ex o9 be Element of o29 st x = o1 +^ o9;
then consider o99 be Ordinal such that
A13: x=o1+^o99 and
A14: o99 in o2;
reconsider o=x as Ordinal by A13;
A15: o1 c= o by A13,ORDINAL3:24;
A16: now
per cases;
suppose
o = o1;
hence not o in o1;
end;
suppose
o <> o1;
then o1 c< o by A15;
hence not o in o1 by ORDINAL1:11;
end;
end;
A17: P[x,f.x] by A7,A10;
x in o1+^o2 & o99 = o-^o1 by A13,A14,ORDINAL2:32,ORDINAL3:52;
then o99 in support b by A9,A16,A17,PRE_POLY:def 7,XBOOLE_0:def 5;
then x in B by A13;
hence thesis by XBOOLE_0:def 3;
end;
end;
A18: support b is finite;
B is finite from FRAENKEL:sch 21(A18);
then
A19: f is finite-support by A8,PRE_POLY:def 8;
f is natural-valued
proof
let x be object;
assume x in dom f;
then
A20: x in o1+^o2 by PARTFUN1:def 2;
then reconsider o = x as Ordinal;
A21: ex o9 be Ordinal st o9=x &( o9 in o1 implies f.x = a.o9)&( o9 in (
o1+^o2) \ o1 implies f.x=b.(o9-^o1)) by A7,A20;
per cases by A20,XBOOLE_0:def 5;
suppose
o in o1;
hence thesis by A21;
end;
suppose
o in (o1 +^o2)\o1;
hence thesis by A21;
end;
end;
then reconsider f as Element of Bags (o1+^o2) by A19,PRE_POLY:def 12;
take f;
let o be Ordinal;
thus o in o1 implies f.o = a.o
proof
assume
A22: o in o1;
o1 c= o1 +^ o2 by ORDINAL3:24;
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 A7,A22;
hence thesis by A22;
end;
assume
A23: o in (o1+^o2) \ o1;
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 A7;
hence thesis by A23;
end;
end;
uniqueness
proof
let a1,a2 be Element of Bags (o1+^o2) such that
A24: 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
A25: for o be Ordinal holds (o in o1 implies a2.o = a.o) & (o in (o1+^
o2) \ o1 implies a2.o=b.(o-^o1));
A26: dom a1 = o1+^o2 by PARTFUN1:def 2;
A27: for c be object st c in dom a1 holds a1.c = a2.c
proof
let c be object such that
A28: c in dom a1;
reconsider o=c as Ordinal by A26,A28;
A29: o1 c= o1+^o2 by ORDINAL3:24;
A30: (o1+^o2)\o1 \/ o1 = (o1+^o2) \/ o1 by XBOOLE_1:39
.=o1+^o2 by A29,XBOOLE_1:12;
per cases by A26,A28,A30,XBOOLE_0:def 3;
suppose
A31: o in o1;
hence a1.c =a.o by A24
.=a2.c by A25,A31;
end;
suppose
A32: o in (o1+^o2) \o1;
hence a1.c =b.(o-^o1) by A24
.=a2.c by A25,A32;
end;
end;
dom a1 = dom a2 by A26,PARTFUN1:def 2;
hence a1 = a2 by A27;
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:27;
for i being object st i in o1 holds ab.i = a.i by Def1;
hence thesis 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:30;
now
let i be object;
assume
A2: i in o2;
then reconsider i9=i as Ordinal;
A3: i9-^o1 = i9 by A1,ORDINAL3:56;
i in (o1+^o2) \ o1 by A1,A2,ORDINAL2:30;
hence ab.i = b.i by A3,Def1;
end;
hence thesis 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 object st z in dom b1 holds b1.z = 0
proof
let z be object;
A3: dom b1 = o1 by PARTFUN1:def 2;
assume
A4: z in dom b1;
then reconsider o=z as Ordinal by A3;
b1.o = (b1+^b2).o by A4,A3,Def1
.= 0 by A1,PBOOLE:5;
hence thesis;
end;
dom b1 = o1 by PARTFUN1:def 2;
then b1 = o1 --> 0 by A2,FUNCOP_1:11;
hence b1=EmptyBag o1 by PBOOLE:def 3;
A5: for z be object st z in dom b2 holds b2.z = 0
proof
let z be object;
A6: dom b2 = o2 by PARTFUN1:def 2;
assume
A7: z in dom b2;
then reconsider o=z as Ordinal by A6;
o1 c= o1+^o by ORDINAL3:24;
then
A8: not o1+^o in o1 by ORDINAL1:5;
o1+^o in o1+^o2 by A7,A6,ORDINAL2:32;
then o1+^o in (o1+^o2) \ o1 by A8,XBOOLE_0:def 5;
then (b1+^b2).(o1+^o) = b2.(o1+^o-^o1) by Def1;
then b2.(o1+^o-^o1) = 0 by A1,PBOOLE:5;
hence thesis by ORDINAL3:52;
end;
dom b2 = o2 by PARTFUN1:def 2;
then b2 = o2 --> 0 by A5,FUNCOP_1:11;
hence b2=EmptyBag o2 by PBOOLE:def 3;
end;
thus b1 = EmptyBag o1 & b2 = EmptyBag o2 implies b1+^b2 = EmptyBag(o1+^o2)
proof
assume that
A9: b1 = EmptyBag o1 and
A10: b2 = EmptyBag o2;
A11: for z be object st z in dom (b1+^b2) holds (b1+^b2).z = 0
proof
let z be object;
A12: dom (b1+^b2) = o1+^o2 by PARTFUN1:def 2;
assume
A13: z in dom (b1+^b2);
then reconsider o=z as Ordinal by A12;
A14: o in (o1+^o2) \ o1 implies b2.(o-^o1) = 0 & (b1+^b2).o=b2.(o-^o1)
by A10,Def1,PBOOLE:5;
o in o1 implies b1.o = 0 & (b1+^b2).o=b1.o by A9,Def1,PBOOLE:5;
hence thesis by A13,A12,A14,XBOOLE_0:def 5;
end;
dom (b1+^b2) = o1+^o2 by PARTFUN1:def 2;
then b1+^b2 = (o1+^o2) --> 0 by A11,FUNCOP_1:11;
hence thesis by PBOOLE:def 3;
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 c2={} as Element of Bags o2 by PRE_POLY:51,TARSKI:def 1;
reconsider c1=c as Element of Bags o1 by A1,ORDINAL2:27;
take c1;
take c2;
thus thesis by A1,Th3;
end;
suppose
A2: o2 is non empty;
then reconsider o29 = o2 as non empty Ordinal;
A3: support c|o1 c= support c
proof
let x be object;
assume x in support c|o1;
then
A4: (c|o1).x <> 0 by PRE_POLY:def 7;
then x in dom (c|o1) by FUNCT_1:def 2;
then [x,(c|o1.x)] in c|o1 by FUNCT_1:1;
then [x,(c|o1).x] in c by RELAT_1:def 11;
then c|o1.x = c.x by FUNCT_1:1;
hence thesis by A4,PRE_POLY:def 7;
end;
dom c = o1+^o2 by PARTFUN1:def 2;
then o1 c= dom c by ORDINAL3:24;
then dom (c|o1) = o1 by RELAT_1:62;
then c|o1 is bag of o1 by A3,PARTFUN1:def 2,PRE_POLY:def 8,RELAT_1:def 18;
then reconsider c1=c|o1 as Element of Bags o1 by PRE_POLY:def 12;
deffunc F(Element of o1+^o29) = $1-^ o1;
defpred P[object,object] means
for x1 be Element of o2 st x1=$1 holds $2=c.(o1+^
x1);
take c1;
set B = { o9-^ o1 where o9 is Element of o1+^o29:o1 c= o9& o9 in support c
}, C = {F(o9) where o9 is Element of o1+^o29:o9 in support c};
A5: B c= C
proof
let x be object;
assume x in B;
then ex o9 being Element of o1+^o29 st x = o9 -^ o1 & o1 c= o9& o9 in
support c;
hence thesis;
end;
A6: for i be object st i in o2 ex j be object st P[i,j]
proof
let i be object;
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
A7: for i be object st i in o2 holds P[i,f.i] from PBOOLE:sch 3(A6);
A8: support f c= B
proof
let x be object;
assume x in support f;
then
A9: f.x <> 0 by PRE_POLY:def 7;
then x in dom f by FUNCT_1:def 2;
then reconsider o9 = x as Element of o29 by PARTFUN1:def 2;
c.(o1+^o9)<>0 by A7,A9;
then
A10: o1+^o9 in support c by PRE_POLY:def 7;
reconsider o99 = o1+^o9 as Element of o1+^o29 by ORDINAL2:32;
o9 = o99-^o1 & o1 c= o99 by ORDINAL3:24,52;
hence thesis by A10;
end;
A11: f is natural-valued
proof
let x be object;
assume
A12: x in dom f;
then reconsider o = x as Element of o2 by PARTFUN1:def 2;
x in o2 by A12,PARTFUN1:def 2;
then f.x = c.(o1+^o) by A7;
hence thesis;
end;
A13: support c is finite;
C is finite from FRAENKEL:sch 21(A13);
then f is finite-support by A5,A8,PRE_POLY:def 8;
then reconsider c2 = f as Element of Bags o2 by A11,PRE_POLY:def 12;
take c2;
now
let i be object;
assume
A14: i in o1+^o2;
per cases by A14,XBOOLE_0:def 5;
suppose
A15: i in o1;
then reconsider i9=i as Ordinal;
dom c1 = o1 by PARTFUN1:def 2;
then c.i9 = c1.i9 by A15,FUNCT_1:47
.= (c1+^c2).i9 by A15,Def1;
hence c.i = (c1+^c2).i;
end;
suppose
A16: i in (o1+^o2)\o1;
then reconsider i9=i as Ordinal;
A17: i9-^o1 in o2 by A2,A16,ORDINAL3:60;
not i9 in o1 by A16,XBOOLE_0:def 5;
then o1 c= i9 by ORDINAL1:16;
then c.i9 = c.(o1+^(i9-^o1)) by ORDINAL3:def 5
.= c2.(i9-^o1) by A7,A17
.= (c1+^c2).i9 by A16,Def1;
hence c.i = (c1+^c2).i;
end;
end;
hence thesis by PBOOLE:3;
end;
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 object;
assume
A2: i in o1;
then reconsider i9 = i as Ordinal;
(b1+^b2).i9 = b1.i9 by A2,Def1;
hence b1.i=c1.i by A1,A2,Def1;
end;
hence b1 = c1 by PBOOLE:3;
now
let i be object;
assume
A3: i in o2;
then reconsider i9 = i as Ordinal;
A4: i9= o1+^i9-^o1 by ORDINAL3:52;
o1 c= o1+^i9 by ORDINAL3:24;
then
A5: not o1+^i9 in o1 by ORDINAL1:5;
o1+^i9 in o1+^o2 by A3,ORDINAL2:32;
then
A6: o1+^i9 in (o1+^o2) \ o1 by A5,XBOOLE_0:def 5;
then (b1+^b2).(o1+^i9) = b2.(o1+^i9-^o1) by Def1;
hence b2.i = c2.i by A1,A6,A4,Def1;
end;
hence thesis 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 Element of 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 10;
consider u being FinSequence of cL such that
A4: (q*'r).b = Sum u and
A5: len u = len decomp b and
A6: for k being Element of 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 10;
consider t being FinSequence of cL such that
A7: (p*'r).b = Sum t and
A8: len t = len decomp b and
A9: for k being Element of 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 10;
reconsider t, u as Element of (len s)-tuples_on cL by A2,A8,A5,FINSEQ_2:92;
A10: dom u = dom s by A2,A5,FINSEQ_3:29;
A11: dom t = dom s by A2,A8,FINSEQ_3:29;
then
A12: dom (t+u) = dom s by A10,POLYNOM1:1;
A13: now
let i be Nat;
assume
A14: i in dom s;
then consider sb1, sb2 being bag of n such that
A15: (decomp b)/.i = <*sb1, sb2*> and
A16: s/.i = (p+q).sb1*r.sb2 by A3;
A17: t/.i = t.i & u/.i = u.i by A11,A10,A14,PARTFUN1:def 6;
consider ub1, ub2 being bag of n such that
A18: (decomp b)/.i = <*ub1, ub2*> and
A19: u/.i = q.ub1*r.ub2 by A6,A10,A14;
A20: sb1 = ub1 & sb2 = ub2 by A15,A18,FINSEQ_1:77;
consider tb1, tb2 being bag of n such that
A21: (decomp b)/.i = <*tb1, tb2*> and
A22: t/.i = p.tb1*r.tb2 by A9,A11,A14;
A23: sb1 = tb1 & sb2 = tb2 by A15,A21,FINSEQ_1:77;
s/.i = s.i by A14,PARTFUN1:def 6;
hence s.i = (p.sb1+q.sb1)*r.sb2 by A16,POLYNOM1:15
.= p.sb1*r.sb2+q.sb1*r.sb2 by VECTSP_1:def 7
.= (t + u).i by A12,A14,A22,A19,A23,A20,A17,FVSUM_1:17;
end;
len (t+u) = len s by A12,FINSEQ_3:29;
then s = t + u by A13,FINSEQ_2:9;
hence ((p+q)*'r).b = Sum t + Sum u by A1,FVSUM_1:76
.= (p*'r+q*'r).b by A7,A4,POLYNOM1:15;
end;
hence thesis by FUNCT_2:63;
end;
begin :: Main results
registration
let n be Ordinal, L be right_zeroed Abelian add-associative
right_complementable well-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 1_Polynom-Ring (n,L);
A1: 1_(Polynom-Ring (n,L)) = 1_(n,L) & 0_(n,L).EmptyBag n = 0.L by
POLYNOM1:22,31;
0.L <> 1_L & 0.Polynom-Ring (n,L) = 0_(n,L) by POLYNOM1:def 11;
hence thesis by A1,POLYNOM1:25;
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 11;
reconsider x9=x,y9=y,z9=z as Element of Polynom-Ring (n,L);
A2: u*'v=x9*y9 & u*'w=x9*z9 by POLYNOM1:def 11;
y9+z9 = v+w by POLYNOM1:def 11;
hence x*(y+z) = u*'(v+w) by POLYNOM1:def 11
.=u*'v+u*'w by POLYNOM1:26
.= x*y+x*z by A2,POLYNOM1:def 11;
A3: v*'u=y9*x9 & w*'u=z9*x9 by POLYNOM1:def 11;
y9+z9 = v+w by POLYNOM1:def 11;
hence (y+z)*x = (v+w)*'u by POLYNOM1:def 11
.= v*'u+w*'u by Th8
.= y*x+z*x by A3,POLYNOM1:def 11;
end;
end;
end;
definition
let o1,o2 be non empty Ordinal, L be right_zeroed add-associative
right_complementable well-unital distributive non trivial
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
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};
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;
set A={ F(b1) where b1 is Element of Bags o1: b1 in Support P };
A1: 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
A2: 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;
deffunc F(Element of Bags o2) = b1+^$1;
reconsider Q0 = P.b1 as Polynomial of o2,L by POLYNOM1:def 11;
set B0 = { F(b2) where b2 is Element of Bags o2: b2 in Support Q0};
A3: B c= B0
proof
let x be object;
assume x in B;
then ex b2 be Element of Bags o2 st x = b1+^b2 & ex Q be Polynomial of
o2,L st Q=P.b1 & b2 in Support Q by A2;
hence thesis;
end;
A4: Support Q0 is finite;
B0 is finite from FRAENKEL:sch 21(A4);
hence thesis by A3;
end;
A5: 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
A6: b = b1+^b2 by Th6;
reconsider Q1=P.b1 as Polynomial of o2,L by POLYNOM1:def 11;
take Q1.b2,b1,b2,Q1;
thus thesis by A6;
end;
consider f being Function of Bags (o1+^o2),the carrier of L such that
A7: for b being Element of Bags (o1+^o2) holds P[b,f.b] from FUNCT_2:
sch 3 (A5);
reconsider f as Series of o1+^o2, L;
A8: Support f = union A
proof
thus Support f c= union A
proof
let x be object;
assume
A9: x in Support f;
then
A10: f.x <> 0.L by POLYNOM1:def 4;
consider b1 be Element of Bags o1,b2 be Element of Bags o2 such that
A11: x = b1+^b2 by A9,Th6;
consider Y be set such that
A12: Y = {b1+^b29 where b29 is Element of Bags o2: ex Q be
Polynomial of o2,L st Q=P.b1 & b29 in Support Q};
consider b19 be Element of Bags o1, b29 be Element of Bags o2, Q1 be
Polynomial of o2,L such that
A13: Q1=P.b19 and
A14: b1+^b2 = b19+^b29 and
A15: f.(b1+^b2)=Q1.b29 by A7;
A16: b1=b19 by A14,Th7;
now
assume P.b1 = 0.Polynom-Ring(o2,L);
then Q1=0_(o2,L) by A13,A16,POLYNOM1:def 11;
hence contradiction by A10,A11,A15,POLYNOM1:22;
end;
then b1 in Support P by POLYNOM1:def 4;
then
A17: Y in A by A12;
b2=b29 by A14,Th7;
then b2 in Support Q1 by A10,A11,A15,POLYNOM1:def 4;
then x in Y by A11,A12,A13,A16;
hence thesis by A17,TARSKI:def 4;
end;
let x be object;
assume x in union A;
then consider Y be set such that
A18: x in Y and
A19: Y in A by TARSKI:def 4;
consider b1 be Element of Bags o1 such that
A20: 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 A19;
consider b2 be Element of Bags o2 such that
A21: x = b1+^b2 and
A22: ex Q be Polynomial of o2,L st Q=P.b1 & b2 in Support Q by A18,A20;
consider Q be Polynomial of o2,L such that
A23: Q=P.b1 and
A24: b2 in Support Q by A22;
A25: Q .b2 <> 0.L by A24,POLYNOM1:def 4;
consider b19 be Element of Bags o1, b29 be Element of Bags o2, Q1 be
Polynomial of o2,L such that
A26: Q1 =P.b19 and
A27: b1+^b2 = b19+^b29 and
A28: f.(b1+^b2)=Q1.b29 by A7;
A29: f.(b1+^b2) = Q1.b2 by A27,A28,Th7;
Q1=Q by A23,A26,A27,Th7;
hence thesis by A21,A25,A29,POLYNOM1:def 4;
end;
A30: Support P is finite by POLYNOM1:def 5;
A is finite from FRAENKEL:sch 21(A30);
then union A is finite by A1,FINSET_1:7;
then reconsider f as Polynomial of o1+^o2,L by A8,POLYNOM1:def 5;
take f;
let b be Element of Bags (o1+^o2);
consider b19 be Element of Bags o1, b29 be Element of Bags o2, Q19 be
Polynomial of o2,L such that
A31: Q19=P.b19 and
A32: b = b19+^b29 and
A33: f.b=Q19.b29 by A7;
consider b1 be Element of Bags o1, b2 be Element of Bags o2 such that
A34: b = b1+^b2 by Th6;
reconsider Q1=P.b1 as Polynomial of o2,L by POLYNOM1:def 11;
take b1,b2;
take Q1;
thus Q1=P.b1;
thus b = b1+^b2 by A34;
b1 = b19 by A34,A32,Th7;
hence thesis by A34,A31,A32,A33,Th7;
end;
uniqueness
proof
let w1,w2 be Polynomial of o1+^o2,L such that
A35: 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
A36: 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
A37: Q1= P.c1 and
A38: c = c1+^c2 and
A39: w1.c = Q1.c2 by A35;
consider d1 be Element of Bags o1,d2 be Element of Bags o2, S1 be
Polynomial of o2,L such that
A40: S1= P.d1 and
A41: c = d1+^d2 and
A42: w2.c = S1.d2 by A36;
c2 = d2 by A38,A41,Th7;
hence thesis by A37,A38,A39,A40,A41,A42,Th7;
end;
hence w1=w2 by FUNCT_2:63;
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 that
A1: b1 divides c1 and
A2: b2 divides c2;
now
reconsider b19 = b1,c19 = c1 as bag of o1;
let k be object;
A3: b19.k <= c19.k by A1,PRE_POLY:def 11;
assume
A4: k in o1+^o2;
per cases by A4,XBOOLE_0:def 5;
suppose
A5: k in o1;
then reconsider k9=k as Ordinal;
(b1 +^ b2).k9 = b1.k9 by A5,Def1;
hence (b1 +^ b2).k <= (c1 +^ c2).k by A3,A5,Def1;
end;
suppose
A6: k in (o1+^ o2)\o1;
then reconsider k9=k as Ordinal;
(b1 +^ b2).k9 = b2.(k9-^o1) & (c1 +^ c2).k9 = c2.(k9-^o1) by A6,Def1;
hence (b1 +^ b2).k <= (c1 +^ c2).k by A2,PRE_POLY:def 11;
end;
end;
hence thesis by PRE_POLY:46;
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;
reconsider b9=b as Element of Bags (o1+^o2) by PRE_POLY:def 12;
consider c1 be Element of Bags o1, c2 be Element of Bags o2 such that
A1: b9 = c1+^c2 by Th6;
reconsider c19=c1,b19=b1 as bag of o1;
reconsider c29=c2,b29=b2 as bag of o2;
assume
A2: b divides b1 +^ b2;
A3: for k being object st k in o2 holds c29.k <= b29.k
proof
let k be object;
assume
A4: k in o2;
then reconsider k9=k as Ordinal;
set x = o1+^k9;
o1 c= o1+^k9 by ORDINAL3:24;
then
A5: not o1+^k9 in o1 by ORDINAL1:5;
A6: (c1+^c2).x <= (b1 +^ b2).x & k9= o1+^k9-^o1 by A2,A1,ORDINAL3:52
,PRE_POLY:def 11;
o1+^k9 in o1+^o2 by A4,ORDINAL2:32;
then
A7: o1+^k9 in (o1+^o2) \ o1 by A5,XBOOLE_0:def 5;
then (b1+^b2).(o1+^k9) = b2.(o1+^k9-^o1) by Def1;
hence thesis by A7,A6,Def1;
end;
take c1,c2;
for k being object st k in o1 holds c19.k <= b19.k
proof
let k be object;
assume
A8: k in o1;
then reconsider k9=k as Ordinal;
A9: (c1+^c2).k <= (b1 +^ b2).k by A2,A1,PRE_POLY:def 11;
(c1+^c2).k9 = c1.k9 by A8,Def1;
hence thesis by A8,A9,Def1;
end;
hence thesis by A1,A3,PRE_POLY:46;
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
PRE_POLY:def 9;
now
assume not k in dom(b1+^b2);
then (b1+^b2).k = 0 by FUNCT_1:def 2;
hence contradiction by A1,NAT_1:2;
end;
then
A3: k in o1+^o2 by PARTFUN1:def 2;
now
per cases by A3,XBOOLE_0:def 5;
case
A4: k in o1;
reconsider a19=a1,b19=b1 as bag of o1;
A5: for l being Ordinal st l in k holds a19.l = b19.l
proof
let l be Ordinal;
assume
A6: l in k;
then
A7: (a1 +^ a2).l = (b1 +^ b2).l by A2;
A8: l in o1 by A4,A6,ORDINAL1:10;
then (a1 +^ a2).l = a1.l by Def1;
hence thesis by A7,A8,Def1;
end;
(a1 +^ a2).k = a1.k by A4,Def1;
then a1.k < b1.k by A1,A4,Def1;
hence a1 < b1 by A5,PRE_POLY:def 9;
end;
case
A9: k in (o1+^ o2)\o1;
set k1 = k -^ o1;
not k in o1 by A9,XBOOLE_0:def 5;
then o1 c= k by ORDINAL1:16;
then
A10: k = o1+^(k-^o1) by ORDINAL3:def 5;
A11: for l being Ordinal st l in k1 holds a2.l = b2.l
proof
let l be Ordinal;
o1 c= o1 +^l by ORDINAL3:24;
then
A12: not o1 +^l in o1 by ORDINAL1:5;
assume
A13: l in k1;
then o1 +^ l in o1 +^ k1 by ORDINAL2:32;
then o1 +^ l in o1 +^o2 by A9,A10,ORDINAL1:10;
then
A14: o1 +^ l in (o1+^ o2)\o1 by A12,XBOOLE_0:def 5;
then
A15: (b1 +^ b2).(o1 +^ l) = b2.(o1+^l-^o1) by Def1
.= b2.l by ORDINAL3:52;
(a1 +^ a2).(o1 +^ l) = a2.(o1+^l-^o1) by A14,Def1
.= a2.l by ORDINAL3:52;
hence thesis by A2,A10,A13,A15,ORDINAL2:32;
end;
for i be object st i in o1 holds a1.i = b1.i
proof
not k in o1 by A9,XBOOLE_0:def 5;
then
A16: o1 c= k by ORDINAL1:16;
let i be object;
assume
A17: i in o1;
then reconsider i9=i as Ordinal;
(a1 +^ a2).i9 = a1.i9 & (b1 +^ b2).i9 = b1.i9 by A17,Def1;
hence thesis by A2,A17,A16;
end;
hence a1 = b1 by PBOOLE:3;
(a1+^a2).k = a2.(k-^o1) by A9,Def1;
then a2.k1 < b2.k1 by A1,A9,Def1;
hence a2 < b2 by A11,PRE_POLY:def 9;
end;
end;
hence thesis;
end;
thus a1 < b1 or a1 = b1 & a2 < b2 implies a1 +^ a2 < b1 +^ b2
proof
assume
A18: a1 < b1 or a1 = b1 & a2 < b2;
now
per cases;
case
a1 < b1;
then consider k be Ordinal such that
A19: k in o1 and
A20: a1.k < b1.k and
A21: for l being Ordinal st l in k holds a1.l = b1.l by Th2;
A22: for l being Ordinal st l in k holds (a1 +^ a2).l = (b1 +^ b2).l
proof
let l be Ordinal;
assume
A23: l in k;
then l in o1 by A19,ORDINAL1:10;
then (a1 +^ a2).l = a1.l & (b1 +^ b2).l = b1.l by Def1;
hence thesis by A21,A23;
end;
(a1 +^ a2).k = a1.k & (b1 +^ b2).k = b1.k by A19,Def1;
hence thesis by A20,A22,PRE_POLY:def 9;
end;
case
A24: not a1 < b1;
then consider k be Ordinal such that
A25: k in o2 and
A26: a2.k < b2.k and
A27: for l being Ordinal st l in k holds a2.l = b2.l by A18,Th2;
set x = o1+^k;
A28: for l being Ordinal st l in x holds (a1 +^ a2).l = (b1 +^ b2).l
proof
let l be Ordinal;
assume
A29: l in x;
per cases;
suppose
A30: l in o1;
hence (a1 +^ a2).l = b1.l by A18,A24,Def1
.= (b1 +^ b2).l by A30,Def1;
end;
suppose
A31: not l in o1;
then o1 c= l by ORDINAL1:16;
then l-^o1 in o1+^k-^o1 by A29,ORDINAL3:53;
then
A32: l-^o1 in k by ORDINAL3:52;
o1 +^ k in o1+^o2 by A25,ORDINAL2:32;
then l in o1+^o2 by A29,ORDINAL1:10;
then
A33: l in (o1+^o2) \ o1 by A31,XBOOLE_0:def 5;
hence (a1 +^ a2).l = a2.(l -^ o1) by Def1
.= b2.(l -^ o1) by A27,A32
.= (b1 +^ b2).l by A33,Def1;
end;
end;
o1 c= o1+^k by ORDINAL3:24;
then
A34: not o1+^k in o1 by ORDINAL1:5;
A35: k= o1+^k-^o1 by ORDINAL3:52;
o1+^k in o1+^o2 by A25,ORDINAL2:32;
then
A36: o1+^k in (o1+^o2) \ o1 by A34,XBOOLE_0:def 5;
then (b1+^b2).(o1+^k) = b2.(o1+^k-^o1) by Def1;
then (a1 +^ a2).x < (b1 +^ b2).x by A26,A36,A35,Def1;
hence thesis by A28,PRE_POLY:def 9;
end;
end;
hence thesis;
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 a19 being Element of Bags o1, Fk being
FinSequence of Bags(o1+^o2) st Fk = G/.i & (divisors b1)/.i = a19 & len Fk =
len divisors b2 & for m being Nat st m in dom Fk ex a199 being Element of Bags
o2 st (divisors b2)/.m = a199 & Fk/.m = a19+^a199 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 a19 being Element
of Bags o1, Fk being FinSequence of Bags(o1+^o2) st Fk = G/.i & (divisors b1)/.
i = a19 & len Fk = len divisors b2 & for m being Nat st m in dom Fk ex a199
being Element of Bags o2 st (divisors b2)/.m = a199 & Fk/.m = a19+^a199;
reconsider D = Del(G,1) as FinSequence of (Bags(o1+^o2))*;
consider a19 being Element of Bags o1, Fk being FinSequence of Bags(o1+^o2)
such that
A3: Fk = G/.1 and
(divisors b1)/.1 = a19 and
A4: len Fk = len divisors b2 and
for m being Nat st m in dom Fk ex a199 being Element of Bags o2 st (
divisors b2)/.m = a199 & Fk/.m = a19+^a199 by A2,FINSEQ_5:6;
len divisors b1 <> 0;
then len G <> 0 by A1,FINSEQ_3:29;
then
A5: G is non empty;
then
A6: 1 in dom G by FINSEQ_5:6;
then reconsider G1 = G.1 as Element of (Bags(o1+^o2))* by A3,PARTFUN1:def 6;
G = <*G.1*>^Del(G,1) by A5,FINSEQ_5:86;
then
A7: FlattenSeq G = (FlattenSeq <*G1*>)^FlattenSeq D by PRE_POLY:3
.= G1^FlattenSeq D by PRE_POLY:1;
set F = FlattenSeq G;
A8: 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
A9: n in dom F and
A10: m in dom F and
A11: n < m;
A12: F/.n = F.n by A9,PARTFUN1:def 6;
consider i1, j1 being Nat such that
A13: i1 in dom G and
A14: j1 in dom (G.i1) and
A15: n = (Sum Card (G|(i1-'1))) + j1 and
A16: (G.i1).j1 = (FlattenSeq G).n by A9,PRE_POLY:29;
consider a19 being Element of Bags o1, Fk being FinSequence of Bags(o1+^o2
) such that
A17: Fk = G/.i1 and
A18: (divisors b1)/.i1 = a19 and
A19: len Fk = len divisors b2 and
A20: for r being Nat st r in dom Fk ex a199 being Element of Bags o2
st (divisors b2)/.r = a199 & Fk/.r = a19+^a199 by A1,A2,A13;
A21: j1 in dom Fk by A13,A14,A17,PARTFUN1:def 6;
then consider a199 being Element of Bags o2 such that
A22: (divisors b2)/.j1 = a199 and
A23: Fk/.j1 = a19+^a199 by A20;
Seg len Fk = dom Fk by FINSEQ_1:def 3;
then
A24: j1 in dom divisors b2 by A19,A21,FINSEQ_1:def 3;
now
consider i2, j2 being Nat such that
A25: i2 in dom G and
A26: j2 in dom (G.i2) and
A27: m = (Sum Card (G|(i2-'1))) + j2 and
A28: (G.i2).j2 = (FlattenSeq G).m by A10,PRE_POLY:29;
consider a29 being Element of Bags o1, Fk9 being FinSequence of Bags(o1
+^o2) such that
A29: Fk9 = G/.i2 and
A30: (divisors b1)/.i2 = a29 and
A31: len Fk9 = len divisors b2 and
A32: for r being Nat st r in dom Fk9 ex a299 being Element of Bags
o2 st (divisors b2)/.r = a299 & Fk9/.r = a29+^a299 by A1,A2,A25;
A33: (divisors b1).i2 = a29 by A1,A25,A30,PARTFUN1:def 6;
Fk9 = G.i2 by A25,A29,PARTFUN1:def 6;
then
A34: (FlattenSeq G).m = Fk9/.j2 by A26,A28,PARTFUN1:def 6;
A35: j2 in dom Fk9 by A25,A26,A29,PARTFUN1:def 6;
then consider a299 being Element of Bags o2 such that
A36: (divisors b2)/.j2 = a299 and
A37: Fk9/.j2 = a29+^a299 by A32;
Seg len Fk9 = dom Fk9 by FINSEQ_1:def 3;
then
A38: j2 in dom divisors b2 by A31,A35,FINSEQ_1:def 3;
then
A39: (divisors b2).j2 = a299 by A36,PARTFUN1:def 6;
consider i1, j1 being Nat such that
A40: i1 in dom G and
A41: j1 in dom (G.i1) and
A42: n = (Sum Card (G|(i1-'1))) + j1 and
A43: (G.i1).j1 = (FlattenSeq G).n by A9,PRE_POLY:29;
consider a19 being Element of Bags o1, Fk being FinSequence of Bags(o1+^
o2) such that
A44: Fk = G/.i1 and
A45: (divisors b1)/.i1 = a19 and
A46: len Fk = len divisors b2 and
A47: for r being Nat st r in dom Fk ex a199 being Element of Bags o2
st (divisors b2)/.r = a199 & Fk/.r = a19+^a199 by A1,A2,A40;
A48: (divisors b1).i1 = a19 by A1,A40,A45,PARTFUN1:def 6;
Fk = G.i1 by A40,A44,PARTFUN1:def 6;
then
A49: (FlattenSeq G).n = Fk/.j1 by A41,A43,PARTFUN1:def 6;
A50: j1 in dom Fk by A40,A41,A44,PARTFUN1:def 6;
then consider a199 being Element of Bags o2 such that
A51: (divisors b2)/.j1 = a199 and
A52: Fk/.j1 = a19+^a199 by A47;
Seg len Fk = dom Fk by FINSEQ_1:def 3;
then
A53: j1 in dom divisors b2 by A46,A50,FINSEQ_1:def 3;
then
A54: (divisors b2).j1 = a199 by A51,PARTFUN1:def 6;
assume
A55: F/.n = F/.m;
A56: F/.n=F.n & F/.m=F.m by A9,A10,PARTFUN1:def 6;
then a19=a29 by A55,A52,A37,A49,A34,Th7;
then
A57: i1=i2 by A1,A40,A25,A48,A33,FUNCT_1:def 4;
a199=a299 by A55,A56,A52,A37,A49,A34,Th7;
hence contradiction by A11,A42,A27,A57,A53,A54,A38,A39,FUNCT_1:def 4;
end;
hence F/.n <> F/.m;
reconsider Fn=F/.n, Fm=F/.m as bag of (o1+^o2);
reconsider Fn9=Fn,Fm9=Fm as Element of Bags (o1+^o2);
consider a1 be Element of Bags o1, a2 be Element of Bags o2 such that
A58: Fn9 = a1+^a2 by Th6;
Fk = G.i1 by A13,A17,PARTFUN1:def 6;
then
A59: Fn9 = Fk/.j1 by A12,A14,A16,PARTFUN1:def 6;
then
A60: a19=a1 by A58,A23,Th7;
then
A61: (divisors b1).i1 = a1 by A1,A13,A18,PARTFUN1:def 6;
A62: a199= a2 by A58,A23,A59,Th7;
then
A63: (divisors b2).j1 = a2 by A22,A24,PARTFUN1:def 6;
A64: F/.m = F.m by A10,PARTFUN1:def 6;
consider c1 be Element of Bags o1, c2 be Element of Bags o2 such that
A65: Fm9 = c1+^c2 by Th6;
consider i2, j2 being Nat such that
A66: i2 in dom G and
A67: j2 in dom (G.i2) and
A68: m = (Sum Card (G|(i2-'1))) + j2 and
A69: (G.i2).j2 = (FlattenSeq G).m by A10,PRE_POLY:29;
consider a29 being Element of Bags o1, Fk9 being FinSequence of Bags(o1+^
o2) such that
A70: Fk9 = G/.i2 and
A71: (divisors b1)/.i2 = a29 and
A72: len Fk9 = len divisors b2 and
A73: for r being Nat st r in dom Fk9 ex a299 being Element of Bags o2
st (divisors b2)/.r = a299 & Fk9/.r = a29+^a299 by A1,A2,A66;
A74: j2 in dom Fk9 by A66,A67,A70,PARTFUN1:def 6;
then consider a299 being Element of Bags o2 such that
A75: (divisors b2)/.j2 = a299 and
A76: Fk9/.j2 = a29+^a299 by A73;
Seg len Fk9 = dom Fk9 by FINSEQ_1:def 3;
then
A77: j2 in dom divisors b2 by A72,A74,FINSEQ_1:def 3;
Fk9 = G.i2 by A66,A70,PARTFUN1:def 6;
then
A78: Fm9 = Fk9/.j2 by A64,A67,A69,PARTFUN1:def 6;
then
A79: a29= c1 by A65,A76,Th7;
then
A80: (divisors b1).i2 = c1 by A1,A66,A71,PARTFUN1:def 6;
A81: a299= c2 by A65,A76,A78,Th7;
then
A82: (divisors b2).j2 = c2 by A75,A77,PARTFUN1:def 6;
now
A83: now
assume that
A84: not i1 < i2 and
A85: not (i1 = i2 & j1 < j2);
per cases by A84,XXREAL_0:1;
suppose
i1=i2;
hence contradiction by A11,A15,A68,A85,XREAL_1:6;
end;
suppose
A86: i1>i2;
i2>=1 by A66,FINSEQ_3:25;
then
A87: i2 -' 1 = i2 - 1 by XREAL_1:233;
reconsider G1 = G.i2 as Element of (Bags(o1+^o2))* by A66,A70,
PARTFUN1:def 6;
A88: Card(G|i2) = (Card G)|i2 & Card (G|(i1-'1)) = (Card G)|(i1-'1)
by POLYNOM3:16;
reconsider GG1 = <*G1*> as FinSequence of (Bags(o1+^o2))*;
i2 < i2 + 1 by XREAL_1:29;
then
A89: i2 - 1 < i2 by XREAL_1:19;
i2>=1 by A66,FINSEQ_3:25;
then
A90: i2-'1+1 = i2 by XREAL_1:235;
i2 <= len G by A66,FINSEQ_3:25;
then i2-'1 < len G by A87,A89,XXREAL_0:2;
then G|i2 = G|(i2-'1) ^ GG1 by A90,FINSEQ_5:83;
then Card (G|i2) = Card (G|(i2-'1))^Card(GG1) by PRE_POLY:25;
then Card (G|i2) = (Card (G|(i2-'1)))^<*card G1*> by PRE_POLY:24;
then
A91: Sum Card (G|i2) = (Sum Card (G|(i2-'1))) + card(G.i2) by RVSUM_1:74;
j2<= card (G.i2) by A67,FINSEQ_3:25;
then
A92: (Sum Card (G|(i2-'1))) + j2 <= Sum Card (G|i2) by A91,XREAL_1:6;
i2 <= i1 -' 1 by A86,NAT_D:49;
then (Sum Card (G|i2)) <= (Sum Card (G|(i1-'1))) by A88,POLYNOM3:18;
then
A93: (Sum Card (G|(i2-'1))) + j2 <= (Sum Card (G|(i1-'1))) by A92,
XXREAL_0:2;
(Sum Card (G|(i1-'1))) <= (Sum Card (G|(i1-'1))) +j1 by NAT_1:11;
hence contradiction by A11,A15,A68,A93,XXREAL_0:2;
end;
end;
consider S being non empty finite Subset of Bags o1 such that
A94: divisors b1 = SgmX(BagOrder o1, S) and
for p being bag of o1 holds p in S iff p divides b1 by PRE_POLY:def 16;
field BagOrder o1 = Bags o1 by ORDERS_1:15;
then
A95: BagOrder o1 linearly_orders S by ORDERS_1:37,38;
consider T being non empty finite Subset of Bags o2 such that
A96: divisors b2 = SgmX(BagOrder o2, T) and
for p being bag of o2 holds p in T iff p divides b2 by PRE_POLY:def 16;
field BagOrder o2= Bags o2 by ORDERS_1:15;
then
A97: BagOrder o2 linearly_orders T by ORDERS_1:37,38;
per cases by A83;
case
A98: i1 < i2;
then [(divisors b1)/.i1, (divisors b1)/.i2] in BagOrder o1 by A1,A13
,A66,A94,A95,PRE_POLY:def 2;
then
A99: a1 <=' c1 by A18,A71,A60,A79,PRE_POLY:def 14;
a1<>c1 by A1,A13,A66,A61,A80,A98,FUNCT_1:def 4;
hence a1<c1 by A99,PRE_POLY:def 10;
end;
case that
A100: i1 = i2 and
A101: j1 < j2;
[(divisors b2)/.j1, (divisors b2)/.j2] in BagOrder o2 by A24,A77,A96
,A97,A101,PRE_POLY:def 2;
then
A102: a2 <=' c2 by A22,A75,A62,A81,PRE_POLY:def 14;
thus a1=c1 by A65,A18,A71,A76,A78,A60,A100,Th7;
a2<>c2 by A24,A63,A77,A82,A101,FUNCT_1:def 4;
hence a2<c2 by A102,PRE_POLY:def 10;
end;
end;
then Fn < Fm or Fn = Fm by A58,A65,Th11;
then Fn <=' Fm by PRE_POLY:def 10;
hence thesis by PRE_POLY:def 14;
end;
Fk = G.1 by A6,A3,PARTFUN1:def 6;
then G.1 <> {} by A4;
then reconsider
S = rng FlattenSeq G as non empty finite Subset of Bags(o1+^o2)
by A7,FINSEQ_1:def 4,RELAT_1:41;
A103: for p being bag of o1+^o2 holds p in S iff p divides b1+^b2
proof
consider W being non empty finite Subset of Bags o2 such that
A104: divisors b2 = SgmX(BagOrder o2, W) and
A105: for q being bag of o2 holds q in W iff q divides b2 by PRE_POLY:def 16;
field BagOrder o2 = Bags o2 by ORDERS_1:15;
then BagOrder o2 linearly_orders W by ORDERS_1:37,38;
then
A106: rng SgmX(BagOrder o2, W) = W by PRE_POLY:def 2;
let p be bag of o1+^o2;
consider T being non empty finite Subset of Bags o1 such that
A107: divisors b1 = SgmX(BagOrder o1, T) and
A108: for q being bag of o1 holds q in T iff q divides b1 by PRE_POLY:def 16;
field BagOrder o1 = Bags o1 by ORDERS_1:15;
then BagOrder o1 linearly_orders T by ORDERS_1:37,38;
then
A109: rng SgmX(BagOrder o1, T) = T by PRE_POLY:def 2;
thus p in S implies p divides b1+^b2
proof
assume p in S;
then consider x be object such that
A110: x in dom FlattenSeq G and
A111: p = (FlattenSeq G).x by FUNCT_1:def 3;
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,PRE_POLY:29;
consider a19 being Element of Bags o1, Fk being FinSequence of Bags(o1+^
o2) such that
A115: Fk = G/.i and
A116: (divisors b1)/.i = a19 and
A117: len Fk = len divisors b2 and
A118: for m being Nat st m in dom Fk ex a199 being Element of Bags
o2 st (divisors b2)/.m = a199 & Fk/.m = a19+^a199 by A1,A2,A112;
reconsider a119= a19 as bag of o1;
(divisors b1).i = a19 by A1,A112,A116,PARTFUN1:def 6;
then a19 in T by A1,A107,A109,A112,FUNCT_1:3;
then
A119: a119 divides b1 by A108;
A120: Fk=G.i by A112,A115,PARTFUN1:def 6;
then consider a199 being Element of Bags o2 such that
A121: (divisors b2)/.j = a199 and
A122: Fk/.j = a19+^a199 by A113,A118;
reconsider a1199= a199 as bag of o2;
j in Seg len Fk by A113,A120,FINSEQ_1:def 3;
then
A123: j in dom divisors b2 by A117,FINSEQ_1:def 3;
then (divisors b2).j = a199 by A121,PARTFUN1:def 6;
then a199 in W by A104,A106,A123,FUNCT_1:3;
then
A124: a1199 divides b2 by A105;
p = a19 +^ a199 by A111,A113,A114,A120,A122,PARTFUN1:def 6;
hence thesis by A119,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
A125: p1 divides b1 and
A126: p2 divides b2 and
A127: p = p1 +^ p2 by Th10;
p1 in T by A108,A125;
then consider i be object such that
A128: i in dom divisors b1 and
A129: p1 = (divisors b1).i by A107,A109,FUNCT_1:def 3;
reconsider i as Element of NAT by A128;
consider a19 being Element of Bags o1, Fk being FinSequence of Bags(o1+^
o2) such that
A130: Fk = G/.i and
A131: (divisors b1)/.i = a19 and
A132: len Fk = len divisors b2 and
A133: for m being Nat st m in dom Fk ex a199 being Element of Bags
o2 st (divisors b2)/.m = a199 & Fk/.m = a19+^a199 by A2,A128;
A134: a19 = p1 by A128,A129,A131,PARTFUN1:def 6;
p2 in rng divisors b2 by A104,A105,A106,A126;
then consider j be object such that
A135: j in dom divisors b2 and
A136: p2 = (divisors b2).j by FUNCT_1:def 3;
A137: j in Seg len divisors b2 by A135,FINSEQ_1:def 3;
Seg len (G.i) = Seg len divisors b2 by A1,A128,A130,A132,PARTFUN1:def 6;
then
A138: j in dom (G.i) by A137,FINSEQ_1:def 3;
reconsider j as Element of NAT by A135;
A139: G/.i = G.i by A1,A128,PARTFUN1:def 6;
then consider a199 being Element of Bags o2 such that
A140: (divisors b2)/.j = a199 and
A141: Fk/.j = a19+^a199 by A130,A133,A138;
A142: a199 = p2 by A135,A136,A140,PARTFUN1:def 6;
A143: (Sum Card (G|(i-'1))) + j in dom FlattenSeq G & (G.i).j = (
FlattenSeq G).(( Sum Card (G|(i-'1))) + j) by A1,A128,A138,PRE_POLY:30;
(G.i).j = a19+^a199 by A130,A138,A139,A141,PARTFUN1:def 6;
hence thesis by A127,A143,A134,A142,FUNCT_1:def 3;
end;
end;
field BagOrder(o1+^o2) = Bags(o1+^o2) by ORDERS_1:15;
then BagOrder(o1+^o2) linearly_orders S by ORDERS_1:37,38;
then FlattenSeq G = SgmX(BagOrder(o1+^o2), S) by A8,PRE_POLY:def 2;
hence thesis by A103,PRE_POLY:def 16;
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 that
A1: c1 = b1 -' a1 and
A2: c2 = b2 -' a2;
reconsider w = (b1 +^ b2) -' (a1 +^ a2) as Element of Bags(o1+^o2) by
PRE_POLY:def 12;
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
A3: o in o1;
thus w.o = (b1 +^ b2).o -' (a1 +^ a2).o by PRE_POLY:def 6
.= b1.o -' (a1 +^ a2).o by A3,Def1
.= b1.o -' a1.o by A3,Def1
.= c1.o by A1,PRE_POLY:def 6;
end;
assume
A4: o in (o1+^o2) \ o1;
thus w.o = (b1 +^ b2).o -' (a1 +^ a2).o by PRE_POLY:def 6
.= b2.(o-^o1) -' (a1 +^ a2).o by A4,Def1
.= b2.(o-^o1) -' a2.(o-^o1) by A4,Def1
.= c2.(o-^o1) by A2,PRE_POLY:def 6;
end;
hence thesis 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 a19, b19 being Element of Bags
o1, Fk being FinSequence of 2-tuples_on Bags(o1+^o2) st Fk = G/.i & (decomp b1)
/.i = <*a19, b19*> & len Fk = len decomp b2 & for m being Nat st m in dom Fk ex
a199,b199 being Element of Bags o2 st (decomp b2)/.m = <*a199, b199*> & Fk/.m =
<*a19+^a199,b19+^b199*> 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 a19, b19 being
Element of Bags o1, Fk being FinSequence of 2-tuples_on Bags(o1+^o2) st Fk = G
/.i & (decomp b1)/.i = <*a19, b19*> & len Fk = len decomp b2 & for m being Nat
st m in dom Fk ex a199,b199 being Element of Bags o2 st (decomp b2)/.m = <*a199
, b199*> & Fk/.m =<*a19+^a199,b19+^b199*>;
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
k in dom G by A4,FINSEQ_1:def 3;
then
A6: G.k in rng G by FUNCT_1:3;
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 A6;
then reconsider Gk = G.k as FinSequence of 2-tuples_on (Bags(o1+^o2));
let j be Nat;
assume j in Seg len(G.k);
then j in dom(G.k) by FINSEQ_1:def 3;
then G.k.j = (Gk)/.j by PARTFUN1:def 6;
then reconsider q = G.k.j as Element of 2-tuples_on (Bags(o1+^o2));
ex q1,q2 being Element of(Bags(o1+^o2)) st q = <*q1,q2*> by FINSEQ_2:100;
then reconsider x = q.1 as Element of (Bags(o1+^o2));
take x;
thus thesis;
end;
consider p being FinSequence of (Bags(o1+^o2)) such that
A7: dom p = Seg len(G.k) and
A8: for j being Nat st j in Seg len(G.k) holds Q[j,p/.j]
from RECDEF_1:sch 17(A5);
reconsider p as Element of (Bags(o1+^o2))* by FINSEQ_1:def 11;
take p;
thus dom p = dom(G.k) by A7,FINSEQ_1:def 3;
let j be Nat;
assume
A9: j in dom p;
then consider q being Element of 2-tuples_on (Bags(o1+^o2)) such that
A10: q = G.k.j and
A11: p/.j = q.1 by A7,A8;
take q;
thus q = G.k.j by A10;
thus thesis by A9,A11,PARTFUN1:def 6;
end;
consider F being FinSequence of (Bags(o1+^o2))* such that
A12: dom F = Seg len G and
A13: for i being Nat st i in Seg len G holds P[i,F/.i] from
RECDEF_1:sch 17(A3);
A14: dom Card F = dom F by CARD_3:def 2
.= dom G by A12,FINSEQ_1:def 3
.= dom Card G by CARD_3:def 2;
A15: dom divisors b1 = dom decomp b1 by PRE_POLY:def 17;
A16: for i being Nat st i in dom divisors b1 holds ex a19 being Element of
Bags o1, Fk being FinSequence of Bags(o1+^o2) st Fk = F/.i & (divisors b1)/.i =
a19 & len Fk = len divisors b2 & for m being Nat st m in dom Fk ex a199 being
Element of Bags o2 st (divisors b2)/.m = a199 & Fk/.m = a19+^a199
proof
let i be Nat;
reconsider Fk = F/.i as FinSequence of Bags(o1+^o2);
A17: dom decomp b2 = dom divisors b2 by PRE_POLY:def 17;
assume
A18: i in dom divisors b1;
then consider a19, b19 being Element of Bags o1, Gi being FinSequence of 2
-tuples_on Bags(o1+^o2) such that
A19: Gi = G/.i and
A20: (decomp b1)/.i = <*a19, b19*> and
A21: len Gi = len decomp b2 and
A22: for m being Nat st m in dom Gi ex a199,b199 being Element of Bags
o2 st (decomp b2)/.m = <*a199, b199*> & Gi/.m =<*a19+^a199,b19+^b199*> by A2
,A15;
take a19,Fk;
thus Fk = F/.i;
thus (divisors b1)/.i = a19 by A15,A18,A20,PRE_POLY:70;
A23: i in Seg len G by A1,A15,A18,FINSEQ_1:def 3;
then
A24: dom(F/.i) = dom(G.i) by A13;
hence len Fk = len(G.i) by FINSEQ_3:29
.= len decomp b2 by A1,A15,A18,A19,A21,PARTFUN1:def 6
.= len divisors b2 by A17,FINSEQ_3:29;
let m be Nat;
assume
A25: m in dom Fk;
then consider p being Element of (2-tuples_on (Bags(o1+^o2))) such that
A26: p = G.i.m and
A27: (F/.i).m = p.1 by A13,A23;
A28: G.i = G/.i by A1,A15,A18,PARTFUN1:def 6;
then consider a199,b199 being Element of Bags o2 such that
A29: (decomp b2)/.m = <*a199, b199*> and
A30: Gi/.m =<*a19+^a199,b19+^b199*> by A19,A22,A24,A25;
A31: p = <*a19+^a199,b19+^b199*> by A19,A24,A28,A25,A30,A26,PARTFUN1:def 6;
take a199;
m in dom decomp b2 by A19,A21,A24,A28,A25,FINSEQ_3:29;
hence (divisors b2)/.m = a199 by A29,PRE_POLY:70;
thus Fk/.m = Fk.m by A25,PARTFUN1:def 6
.= a19+^a199 by A27,A31;
end;
dom decomp b2 = dom divisors b2 by PRE_POLY:def 17;
then
A32: len decomp b2 = len divisors b2 by FINSEQ_3:29;
A33: for j be Nat st j in dom Card F holds (Card F).j = (Card G).j
proof
let j be Nat;
assume
A34: j in dom Card F;
then
A35: j in dom G by A14,CARD_3:def 2;
A36: dom Card F = dom F by CARD_3:def 2;
then
A37: (Card F).j = card(F.j) by A34,CARD_3:def 2;
j in dom decomp b1 by A1,A12,A34,A36,FINSEQ_1:def 3;
then
A38: (ex a19 being Element of Bags o1, Fk being FinSequence of Bags(o1+^o2
) st Fk = F/.j & (divisors b1)/.j = a19 & len Fk = len divisors b2 & for m
being Nat st m in dom Fk ex a199 being Element of Bags o2 st ( divisors b2)/.m
= a199 & Fk/.m = a19+^a199 )& ex a29, b29 being Element of Bags o1, Gk being
FinSequence of 2-tuples_on Bags(o1+^o2) st Gk = G/.j & (decomp b1)/.j = <*a29,
b29*> & len Gk = len decomp b2 & for m being Nat st m in dom Gk ex a299,b299
being Element of Bags o2 st (decomp b2)/.m = <*a299, b299*> & Gk/.m =<*a29+^
a299,b29 +^b299*> by A2,A15,A16;
card(F.j) = card(F/.j) by A34,A36,PARTFUN1:def 6
.= card(G.j) by A32,A35,A38,PARTFUN1:def 6;
hence thesis by A35,A37,CARD_3:def 2;
end;
reconsider bb = b1+^b2 as bag of o1+^o2;
reconsider FG = FlattenSeq G as FinSequence of 2-tuples_on Bags(o1+^o2);
len Card F = len Card G by A14,FINSEQ_3:29;
then
A39: Card F = Card G by A33,FINSEQ_2:9;
then
A40: len FG = len FlattenSeq F by PRE_POLY:28;
dom decomp b1 = dom divisors b1 by PRE_POLY:def 17;
then dom F = dom divisors b1 by A1,A12,FINSEQ_1:def 3;
then
A41: divisors(b1+^b2) = FlattenSeq F by A16,Th12;
A42: dom decomp b1 = dom divisors b1 by PRE_POLY:def 17;
A43: for i being Element of 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 Element of NAT, p be bag of o1+^o2 such that
A44: k in dom FG and
A45: p = (divisors bb)/.k;
consider i, j being Nat such that
A46: i in dom G and
A47: j in dom (G.i) and
A48: k = (Sum Card (G|(i-'1))) + j and
A49: (G.i).j = FG.k by A44,PRE_POLY:29;
consider fa1 being Element of Bags o1, Fk being FinSequence of Bags(o1+^o2
) such that
A50: Fk = F/.i and
A51: (divisors b1)/.i = fa1 and
len Fk = len divisors b2 and
A52: for m being Nat st m in dom Fk ex fa19 being Element of Bags o2
st (divisors b2)/.m = fa19 & Fk/.m = fa1+^fa19 by A1,A16,A42,A46;
consider a19, b19 being Element of Bags o1, Gi being FinSequence of 2
-tuples_on Bags(o1+^o2) such that
A53: Gi = G/.i and
A54: (decomp b1)/.i = <*a19, b19*> and
A55: len Gi = len decomp b2 and
A56: for m being Nat st m in dom Gi ex a199,b199 being Element of Bags
o2 st (decomp b2)/.m = <*a199, b199*> & Gi/.m =<*a19+^a199,b19+^b199*> by A1,A2
,A46;
A57: a19 = fa1 by A1,A46,A54,A51,PRE_POLY:70;
then
A58: <*a19, b19*> = <*a19, b1-'a19*> by A1,A46,A54,A51,PRE_POLY:def 17;
A59: j in dom Gi by A46,A47,A53,PARTFUN1:def 6;
then consider a199,b199 being Element of Bags o2 such that
A60: (decomp b2)/.j = <*a199, b199*> and
A61: Gi/.j =<*a19+^a199,b19+^b199*> by A56;
reconsider b2a1 = b2-'a199 as Element of Bags o2 by PRE_POLY:def 12;
reconsider b1a1 = b1-'a19 as Element of Bags o1 by PRE_POLY:def 12;
k in dom FlattenSeq F by A40,A44,FINSEQ_3:29;
then consider i9, j9 being Nat such that
A62: i9 in dom F and
A63: j9 in dom (F.i9) and
A64: k = (Sum Card (F|(i9-'1))) + j9 and
A65: (F.i9).j9 = (FlattenSeq F).k by PRE_POLY:29;
A66: Card (G|(i-'1)) = (Card G)|(i-'1) & Card (F|(i9-'1)) = (Card F)|(i9-'
1) by POLYNOM3:16;
then
A67: i = i9 by A39,A46,A47,A48,A62,A63,A64,POLYNOM3:22;
A68: j = j9 by A39,A46,A47,A48,A62,A63,A64,A66,POLYNOM3:22;
then
A69: j in dom Fk by A62,A63,A67,A50,PARTFUN1:def 6;
then consider fa19 being Element of Bags o2 such that
A70: (divisors b2)/.j = fa19 and
A71: Fk/.j = fa1+^fa19 by A52;
A72: j in dom decomp b2 by A55,A59,FINSEQ_3:29;
then
A73: a199 = fa19 by A60,A70,PRE_POLY:70;
then
A74: <*a199, b199*> = <*a199, b2-'a199*> by A60,A70,A72,PRE_POLY:def 17;
k in dom FlattenSeq F by A40,A44,FINSEQ_3:29;
then
A75: p = F.i.j by A41,A45,A65,A67,A68,PARTFUN1:def 6
.= Fk.j by A62,A67,A50,PARTFUN1:def 6
.= a19+^a199 by A69,A71,A57,A73,PARTFUN1:def 6;
then
A76: bb-'p = b1a1 +^ b2a1 by Th13
.= b19+^ b2a1 by A58,FINSEQ_1:77
.= b19+^ b199 by A74,FINSEQ_1:77;
thus FG/.k = (G.i).j by A44,A49,PARTFUN1:def 6
.= Gi.j by A46,A53,PARTFUN1:def 6
.= <*p, bb-'p*> by A59,A61,A75,A76,PARTFUN1:def 6;
end;
dom FG = dom divisors bb by A41,A40,FINSEQ_3:29;
hence thesis by A43,PRE_POLY:def 17;
end;
theorem
for o1,o2 be non empty Ordinal, L be Abelian right_zeroed
add-associative right_complementable well-unital distributive associative
well-unital non trivial 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 well-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;
reconsider 1P1 = 1_P1 as Polynomial of o1,Polynom-Ring(o2,L) by
POLYNOM1:def 11;
reconsider 1P2 = 1_P2 as Polynomial of o1+^o2,L by POLYNOM1:def 11;
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 11;
reconsider u = Compress Q as Element of P2 by POLYNOM1:def 11;
take u;
let P be Polynomial of o1,Polynom-Ring(o2,L);
assume x=P;
hence thesis;
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 FUNCT_2:sch 3(A1);
reconsider f as Function of P1,P2;
take f;
thus f is additive
proof
let x,y be Element of P1;
reconsider x9 =x, y9= y as Element of P1;
reconsider p =x9, q= y9 as Polynomial of o1,Polynom-Ring(o2,L) by
POLYNOM1:def 11;
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 11;
for x being bag of o1+^o2 holds fpq.x = fp.x+fq.x
proof
let b be bag of o1+^o2;
reconsider b9= b as Element of Bags (o1+^o2) by PRE_POLY:def 12;
consider b1 be Element of Bags o1, b2 be Element of Bags o2, Q1 be
Polynomial of o2,L such that
A3: Q1=p.b1 and
A4: b9 = b1+^b2 and
A5: (Compress p).b9=Q1.b2 by Def2;
consider b19 be Element of Bags o1, b29 be Element of Bags o2, Q19 be
Polynomial of o2,L such that
A6: Q19=q.b19 and
A7: b9 = b19+^b29 and
A8: (Compress q).b9=Q19.b29 by Def2;
consider b199 be Element of Bags o1, b299 be Element of Bags o2, Q199 be
Polynomial of o2,L such that
A9: Q199=(p+q).b199 and
A10: b9 = b199+^b299 and
A11: (Compress (p + q)).b9=Q199.b299 by Def2;
A12: b19=b199 by A7,A10,Th7;
reconsider b1 as bag of o1;
A13: (p+q).b1 = p.b1+q.b1 by POLYNOM1:15;
b1=b19 by A4,A7,Th7;
then Q199= Q1+ Q19 by A3,A6,A9,A12,A13,POLYNOM1:def 11;
then
A14: Q199.b2 = Q1.b2 + Q19.b2 by POLYNOM1:15;
A15: b29=b299 by A7,A10,Th7;
A16: b2=b29 by A4,A7,Th7;
x + y = p + q by POLYNOM1:def 11;
hence fpq.b = (Compress (p + q)).b9 by A2
.= (Compress p).b9+fq.b by A2,A5,A8,A11,A16,A15,A14
.= fp.b+fq.b by A2;
end;
hence f.(x+y) = fp+fq by POLYNOM1:16
.=(f.x)+(f.y) by POLYNOM1:def 11;
end;
now
let x,y be Element of P1;
reconsider x9 =x, y9= y as Element of P1;
reconsider p =x9, q= y9 as Polynomial of o1,Polynom-Ring(o2,L) by
POLYNOM1:def 11;
reconsider fp =f.x, fq= f.y as Element of P2;
reconsider fp, fq as Polynomial of o1+^o2,L by POLYNOM1:def 11;
f.(x*y)=f.(p*'q) by POLYNOM1:def 11;
then reconsider fpq9 = f.(p*'q) as Polynomial of o1+^o2, L by
POLYNOM1:def 11;
A17: for b being bag of o1+^o2 ex s being FinSequence of the carrier of L
st fpq9.b = Sum s & len s = len decomp b & for k being Element of 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
reconsider x = p*'q as Element of P1 by POLYNOM1:def 11;
let c be bag of (o1+^o2);
reconsider b=c as Element of Bags (o1+^o2) by PRE_POLY:def 12;
consider b1 be Element of Bags o1, b2 be Element of Bags o2 such that
A18: 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
A19: (p*'q).b1 = Sum r and
A20: len r = len decomp b1 and
A21: for k being Element of NAT st k in dom r ex a19, b19 being bag
of o1 st (decomp b1)/.k = <*a19, b19*> & r/.k = (p.a19)*(q.b19) by
POLYNOM1:def 10;
for x be object st x in dom r holds r.x is Function
proof
let x be object;
assume x in dom r;
then
A22: r.x in rng r by FUNCT_1:3;
rng r c= the carrier of Polynom-Ring(o2,L) by FINSEQ_1:def 4;
hence thesis by A22,POLYNOM1:def 11;
end;
then reconsider rFF = r as Function-yielding Function by FUNCOP_1:def 6;
deffunc F(object) = (rFF.$1).b2;
consider rFFb2 being Function such that
A23: dom rFFb2 = dom r and
A24: for i being object st i in dom r holds rFFb2.i = F(i) from FUNCT_1
:sch 3;
ex i be Nat st dom r = Seg i by FINSEQ_1:def 2;
then reconsider rFFb2 as FinSequence by A23,FINSEQ_1:def 2;
A25: rng rFFb2 c= the carrier of L
proof
let u be object;
A26: rng rFF c= the carrier of Polynom-Ring(o2,L) by FINSEQ_1:def 4;
assume u in rng rFFb2;
then consider x be object such that
A27: x in dom rFFb2 and
A28: u = rFFb2.x by FUNCT_1:def 3;
rFF.x in rng rFF by A23,A27,FUNCT_1:3;
then
A29: rFF.x is Function of Bags o2, the carrier of L by A26,POLYNOM1:def 11;
then
A30: rng (rFF.x) c= the carrier of L by RELAT_1:def 19;
dom (rFF.x) = Bags o2 by A29,FUNCT_2:def 1;
then
A31: (rFF.x).b2 in rng (rFF.x) by FUNCT_1:3;
rFFb2.x = (rFF.x).b2 by A23,A24,A27;
hence thesis by A28,A30,A31;
end;
defpred P[set,set] means ex a19, b19 being bag of o1, Fk being
FinSequence of the carrier of L, pa19, qb19 being Polynomial of o2,L st pa19 =
p.a19 & qb19 = q.b19 & Fk = $2 & (decomp b1)/.$1 = <*a19, b19*> & len Fk = len
decomp b2 & for m being Nat st m in dom Fk ex a199,b199 being bag of o2 st (
decomp b2)/.m = <*a199, b199*> & Fk/.m =pa19.a199*qb19.b199;
A32: 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 A20,FINSEQ_1:def 3;
then consider a19,b19 being bag of o1 such that
A33: (decomp b1)/.k = <*a19, b19*> and
b1 = a19 + b19 by PRE_POLY:68;
reconsider pa199=p.a19,qb199=q.b19 as Element of Polynom-Ring(o2,L);
reconsider pa19=pa199,qb19 = qb199 as Polynomial of o2,L by
POLYNOM1:def 11;
defpred Q[set,set] means ex a199,b199 being bag of o2 st (decomp b2)/.
$1 = <*a199, b199*> & $2 =pa19.a199*qb19.b199;
A34: 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 a199,b199 being bag of o2 such that
A35: (decomp b2)/.k = <*a199, b199*> and
b2 = a199 + b199 by PRE_POLY:68;
reconsider x=pa19.a199*qb19.b199 as Element of L;
take x,a199,b199;
thus thesis by A35;
end;
consider Fk being FinSequence of the carrier of L such that
A36: dom Fk = Seg len decomp b2 and
A37: for k being Nat st k in Seg len decomp b2 holds Q[
k,Fk/.k] from RECDEF_1:sch 17(A34);
reconsider x=Fk as Element of (the carrier of L)* by FINSEQ_1:def 11;
take x,a19,b19,Fk,pa19,qb19;
thus pa19 = p.a19 & qb19 = q.b19 & Fk = x;
thus (decomp b1)/.k = <*a19, b19*> by A33;
thus len Fk = len decomp b2 by A36,FINSEQ_1:def 3;
let m be Nat;
assume m in dom Fk;
hence thesis by A36,A37;
end;
consider F being FinSequence of (the carrier of L)* such that
A38: dom F = Seg len r and
A39: for k being Nat st k in Seg len r holds P[k,F/.k]
from RECDEF_1:sch 17(A32);
take s = FlattenSeq F;
A40: len(Sum F) = len F by MATRLIN:def 6;
reconsider rFFb2 as FinSequence of the carrier of L by A25,FINSEQ_1:def 4
;
A41: f.x = Compress(p*'q) by A2;
A42: dom rFFb2 = dom F by A38,A23,FINSEQ_1:def 3
.= dom(Sum F) by A40,FINSEQ_3:29;
for k being Nat st k in dom rFFb2 holds rFFb2.k = (Sum F).k
proof
let k be Nat such that
A43: k in dom rFFb2;
consider c1, d1 being bag of o1 such that
A44: (decomp b1)/.k = <*c1, d1*> and
A45: r/.k = (p.c1)*(q.d1) by A21,A23,A43;
k in Seg len r by A23,A43,FINSEQ_1:def 3;
then consider
a19, b19 being bag of o1, Fk being FinSequence of the carrier
of L, pa19, qb19 being Polynomial of o2,L such that
A46: pa19 = p.a19 & qb19 = q.b19 and
A47: Fk = F/.k and
A48: (decomp b1)/.k = <*a19, b19*> and
A49: len Fk = len decomp b2 and
A50: for ki being Nat st ki in dom Fk ex a199,b199 being bag of o2
st (decomp b2)/.ki = <*a199, b199*> & Fk/.ki =pa19.a199*qb19.b199 by A39;
A51: c1=a19 & d1=b19 by A44,A48,FINSEQ_1:77;
consider s1 being FinSequence of the carrier of L such that
A52: (pa19)*'(qb19).b2 = Sum s1 and
A53: len s1 = len decomp b2 and
A54: for ki being Element of NAT st ki in dom s1 ex x1, y2 being
bag of o2 st (decomp b2)/.ki = <*x1, y2*> & s1/.ki = (pa19.x1)*(qb19.y2) by
POLYNOM1:def 10;
A55: dom s1 = Seg len s1 by FINSEQ_1:def 3;
now
let ki be Nat;
assume
A56: ki in dom s1;
then
A57: s1/.ki = s1.ki by PARTFUN1:def 6;
A58: ki in dom Fk by A49,A53,A55,A56,FINSEQ_1:def 3;
then consider a199,b199 being bag of o2 such that
A59: (decomp b2)/.ki = <*a199, b199*> and
A60: Fk/.ki =pa19.a199*qb19.b199 by A50;
consider x1, y2 being bag of o2 such that
A61: (decomp b2)/.ki = <*x1, y2*> and
A62: s1/.ki = (pa19.x1)*(qb19.y2) by A54,A56;
x1=a199 & y2=b199 by A61,A59,FINSEQ_1:77;
hence s1.ki = Fk.ki by A62,A58,A60,A57,PARTFUN1:def 6;
end;
then
A63: s1=Fk by A49,A53,FINSEQ_2:9;
A64: rFF.k = r/.k by A23,A43,PARTFUN1:def 6
.= (pa19)*'(qb19) by A45,A46,A51,POLYNOM1:def 11;
thus rFFb2.k = (rFF.k).b2 by A23,A24,A43
.= (Sum F)/.k by A42,A43,A47,A64,A52,A63,MATRLIN:def 6
.= (Sum F).k by A42,A43,PARTFUN1:def 6;
end;
then
A65: rFFb2 = Sum F by A42;
reconsider Sr = Sum r as Polynomial of o2,L by POLYNOM1:def 11;
consider gg being sequence of the carrier of Polynom-Ring(o2,L)
such that
A66: Sum r = gg.(len r) and
A67: gg.0 = 0.Polynom-Ring(o2,L) and
A68: 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;
A69: for x being Element of NAT ex y being Element of L st R[x,y]
proof
let x be Element of NAT;
reconsider pp9 = gg.x as Polynomial of o2,L by POLYNOM1:def 11;
take y = pp9.b2;
let pp be Polynomial of o2,L;
assume that
x <= len r and
A70: pp=gg.x;
thus thesis by A70;
end;
consider ff being sequence of the carrier of L such that
A71: for j being Element of NAT holds R[j,ff.j] from FUNCT_2:sch 3(A69);
A72: for j being Nat holds R[j,ff.j]
proof let n be Nat;
n in NAT by ORDINAL1:def 12;
hence thesis by A71;
end;
defpred VV[set,set] means ex a19, b19 being Element of Bags o1, Fk being
FinSequence of 2-tuples_on Bags(o1+^o2) st Fk = $2 & (decomp b1)/.$1 = <*a19,
b19*> & len Fk = len decomp b2 & for m being Nat st m in dom Fk ex a199,b199
being Element of Bags o2 st (decomp b2)/.m = <*a199, b199*> & Fk/.m =<*a19+^
a199,b19+^b199*>;
A73: 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 A20,FINSEQ_1:def 3;
then consider a19,b19 being bag of o1 such that
A74: (decomp b1)/.k = <*a19, b19*> and
b1 = a19 + b19 by PRE_POLY:68;
reconsider a19,b19 as Element of Bags o1 by PRE_POLY:def 12;
defpred Q[set,set] means ex a199,b199 being Element of Bags o2 st (
decomp b2)/.$1 = <*a199, b199*> & $2 =<*a19+^a199,b19+^b199*>;
A75: 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 a199,b199 being bag of o2 such that
A76: (decomp b2)/.k = <*a199, b199*> and
b2 = a199 + b199 by PRE_POLY:68;
reconsider a199,b199 as Element of Bags o2 by PRE_POLY:def 12;
reconsider x = <*a19+^a199,b19+^b199*> as Element of 2-tuples_on
Bags(o1+^o2);
take x;
take a199,b199;
thus thesis by A76;
end;
consider Fk being FinSequence of 2-tuples_on Bags(o1+^o2) such that
A77: dom Fk = Seg len decomp b2 and
A78: for k being Nat st k in Seg len decomp b2 holds Q
[k,Fk/.k] from RECDEF_1:sch 17(A75);
reconsider x=Fk as Element of (2-tuples_on Bags(o1+^o2))* by
FINSEQ_1:def 11;
take x, a19, b19;
take Fk;
thus Fk = x;
thus (decomp b1)/.k = <*a19, b19*> by A74;
thus len Fk = len decomp b2 by A77,FINSEQ_1:def 3;
let m be Nat;
assume m in dom Fk;
hence thesis by A77,A78;
end;
consider G being FinSequence of (2-tuples_on Bags(o1+^o2))* such that
A79: dom G = Seg len r and
A80: for i being Nat st i in Seg len r holds VV[i,G/.i]
from RECDEF_1:sch 17(A73);
A81: for i being Nat st i in Seg len r holds VV[i,G/.i] by A80;
A82: dom Card F = dom F by CARD_3:def 2;
A83: for j be Nat st j in dom Card F holds (Card F).j = (Card G).j
proof
let j be Nat;
assume
A84: j in dom Card F;
then
A85: j in dom F by CARD_3:def 2;
then
A86: (Card F).j = card(F.j) by CARD_3:def 2;
A87: (ex a19, b19 being bag of o1, Fk being FinSequence of the
carrier of L, pa19, qb19 being Polynomial of o2,L st pa19 = p.a19 & qb19 = q .
b19 & Fk = F/.j & (decomp b1)/.j = <*a19, b19*> & len Fk = len decomp b2 & for
m being Nat st m in dom Fk ex a199,b199 being bag of o2 st (decomp b2)/.m = <*
a199, b199*> & Fk /.m =pa19.a199*qb19.b199 )& ex a29, b29 being Element of Bags
o1, Gk being FinSequence of 2-tuples_on Bags(o1+^o2) st Gk = G/.j & (decomp b1)
/.j = <* a29, b29*> & len Gk = len decomp b2 & for m being Nat st m in dom Gk
ex a299, b299 being Element of Bags o2 st (decomp b2)/.m = <*a299, b299*> & Gk
/.m =<*a29 +^a299,b29 +^b299*> by A38,A39,A80,A85;
card(F.j) = card(F/.j) by A85,PARTFUN1:def 6
.= card(G.j) by A38,A79,A82,A84,A87,PARTFUN1:def 6;
hence thesis by A38,A79,A82,A84,A86,CARD_3:def 2;
end;
consider c1 be Element of Bags o1, c2 be Element of Bags o2, Q1 be
Polynomial of o2,L such that
A88: Q1=(p*'q).c1 and
A89: b = c1+^c2 and
A90: (Compress(p*'q)).b = Q1.c2 by Def2;
A91: c1 = b1 by A18,A89,Th7;
then dom G = dom decomp c1 by A20,A79,FINSEQ_1:def 3;
then
A92: decomp c = FlattenSeq G by A18,A79,A81,A91,Th14;
A93: 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 that
A94: j < len rFFb2 and
A95: v = rFFb2.(j + 1);
reconsider w = r/.(j+1),pp = gg.j, pp9 = gg.(j+1) as Polynomial of o2,
L by POLYNOM1:def 11;
reconsider w1 = w, pp1 = pp, pp19 = pp9 as Element of Polynom-Ring(o2,
L);
reconsider w1, pp1, pp19 as Element of Polynom-Ring(o2,L);
A96: j < len r by A23,A94,FINSEQ_3:29;
then
A97: j+1 <= len r by NAT_1:13;
then
A98: w = r.(j+1) by FINSEQ_4:15,NAT_1:11;
then
A99: pp19 = pp1 + w1 by A68,A96;
1 <= j+1 by NAT_1:11;
then j + 1 in dom r by A97,FINSEQ_3:25;
then
A100: w.b2 = v by A24,A95,A98;
j+1 <= len r by A96,NAT_1:13;
hence ff.(j + 1) = pp9.b2 by A72
.= (pp + w).b2 by A99,POLYNOM1:def 11
.= pp.b2 + w.b2 by POLYNOM1:15
.= ff.j + v by A72,A96,A100;
end;
gg.0 = 0_(o2,L) by A67,POLYNOM1:def 11;
then
A101: ff.0 = (0_(o2,L)).b2 by A72,NAT_1:2
.= 0.L by POLYNOM1:22;
len rFFb2 = len r by A23,FINSEQ_3:29;
then Sr.b2 = ff.(len rFFb2) by A66,A72;
then
A102: Sr.b2 = Sum rFFb2 by A101,A93,RLVECT_1:def 12;
b1=c1 & b2=c2 by A18,A89,Th7;
hence fpq9.c = Sum s by A19,A88,A90,A65,A102,A41,POLYNOM1:14;
dom Card G = dom G by CARD_3:def 2;
then len Card F = len Card G by A38,A79,A82,FINSEQ_3:29;
then
A103: Card F = Card G by A83,FINSEQ_2:9;
hence
A104: len s = len decomp c by A92,PRE_POLY:28;
let k be Element of NAT;
assume
A105: k in dom s;
then consider i, j being Nat such that
A106: i in dom F and
A107: j in dom (F.i) and
A108: k = Sum (Card (F|(i-'1))) + j and
A109: (F.i).j = (FlattenSeq F).k by PRE_POLY:29;
A110: k in dom decomp c by A104,A105,FINSEQ_3:29;
then consider i9, j9 being Nat such that
A111: i9 in dom G and
A112: j9 in dom (G.i9) and
A113: k = Sum (Card (G|(i9-'1))) + j9 and
A114: (G.i9).j9 = (decomp c).k by A92,PRE_POLY:29;
(Sum ((Card F)|(i-'1))) + j = Sum (Card(F|(i-'1))) + j by POLYNOM3:16
.= (Sum ((Card G)|(i9-'1))) + j9 by A108,A113,POLYNOM3:16;
then
A115: i = i9 & j = j9 by A103,A106,A107,A111,A112,POLYNOM3:22;
consider c1, c2 being bag of o1+^o2 such that
A116: (decomp c)/.k = <*c1, c2*> and
c = c1+c2 by A110,PRE_POLY:68;
reconsider cc1=c1, cc2=c2 as Element of Bags(o1+^o2) by PRE_POLY:def 12;
consider cb1 be Element of Bags o1, cb2 be Element of Bags o2, Q1 be
Polynomial of o2,L such that
A117: Q1=p.cb1 and
A118: cc1 = cb1+^cb2 and
A119: (Compress p).cc1=Q1.cb2 by Def2;
consider a19, b19 being bag of o1, Fk being FinSequence of the carrier
of L, pa19, qb19 being Polynomial of o2,L such that
A120: pa19 = p.a19 and
A121: qb19 = q.b19 and
A122: Fk = F/.i and
A123: (decomp b1)/.i = <*a19, b19*> and
len Fk = len decomp b2 and
A124: for m being Nat st m in dom Fk ex a199,b199 being bag of o2 st
(decomp b2)/.m = <*a199, b199*> & Fk/.m =pa19.a199*qb19.b199 by A38,A39,A106;
consider ga19, gb19 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 = <*ga19, gb19*> and
len Gk = len decomp b2 and
A127: for m being Nat st m in dom Gk ex ga199,gb199 being Element of
Bags o2 st (decomp b2)/.m = <*ga199, gb199*> & Gk/.m =<*ga19+^ga199,gb19+^gb199
*> by A38,A80,A106;
A128: b19 = gb19 by A123,A126,FINSEQ_1:77;
A129: Gk = G.i by A38,A79,A106,A125,PARTFUN1:def 6;
then consider ga199,gb199 be Element of Bags o2 such that
A130: (decomp b2)/.j = <*ga199, gb199*> and
A131: Gk/.j =<*ga19+^ga199,gb19+^gb199*> by A112,A115,A127;
A132: <*c1,c2*> = G.i.j by A110,A116,A114,A115,PARTFUN1:def 6
.= <*ga19+^ga199,gb19+^gb199*> by A112,A115,A129,A131,PARTFUN1:def 6;
then c1 = ga19 +^ ga199 by FINSEQ_1:77;
then
A133: cb1 = ga19 & cb2 = ga199 by A118,Th7;
A134: a19 = ga19 by A123,A126,FINSEQ_1:77;
j in dom Fk by A106,A107,A122,PARTFUN1:def 6;
then consider a199,b199 be bag of o2 such that
A135: (decomp b2)/.j = <*a199, b199*> and
A136: Fk/.j =pa19.a199*qb19.b199 by A124;
a199 = ga199 by A130,A135,FINSEQ_1:77;
then
A137: pa19.a199 = fp.c1 by A2,A120,A117,A119,A133,A134;
take c1,c2;
thus (decomp c)/.k = <*c1, c2*> by A116;
consider cb1 be Element of Bags o1, cb2 be Element of Bags o2, Q1 be
Polynomial of o2,L such that
A138: Q1=q.cb1 and
A139: cc2 = cb1+^cb2 and
A140: (Compress q).cc2=Q1.cb2 by Def2;
c2 = gb19 +^ gb199 by A132,FINSEQ_1:77;
then
A141: cb1 = gb19 & cb2 = gb199 by A139,Th7;
A142: Fk = F.i by A106,A122,PARTFUN1:def 6;
b199 = gb199 by A130,A135,FINSEQ_1:77;
then
A143: qb19.b199 = fq.c2 by A2,A121,A128,A138,A140,A141;
thus s/.k = s.k by A105,PARTFUN1:def 6
.= fp.c1*fq.c2 by A107,A109,A142,A136,A137,A143,PARTFUN1:def 6;
end;
thus f.(x*y) = f.(p*'q) by POLYNOM1:def 11
.= (fp)*'(fq) by A17,POLYNOM1:def 10
.=(f.x)*(f.y) by POLYNOM1:def 11;
end;
hence f is multiplicative by GROUP_6:def 6;
A144: for b being Element of Bags(o1+^o2) holds (Compress 1P1).b = (1P2).b
proof
let b be Element of Bags(o1+^o2);
A145: 1P2.b = (1_(o1+^o2,L)).b by POLYNOM1:31;
consider b1 be Element of Bags o1, b2 be Element of Bags o2, Q1 be
Polynomial of o2,L such that
A146: Q1=1P1.b1 and
A147: b = b1+^b2 and
A148: (Compress 1P1).b = Q1.b2 by Def2;
per cases;
suppose
A149: b = EmptyBag(o1+^o2);
then
A150: b1 = EmptyBag o1 by A147,Th5;
A151: b2 = EmptyBag o2 by A147,A149,Th5;
Q1 = 1_(o1,Polynom-Ring(o2,L)).b1 by A146,POLYNOM1:31
.=1_Polynom-Ring(o2,L) by A150,POLYNOM1:25;
then Q1.b2 = (1_(o2,L)).b2 by POLYNOM1:31
.= 1_L by A151,POLYNOM1:25
.=1P2.b by A145,A149,POLYNOM1:25;
hence thesis by A148;
end;
suppose
A152: b <> EmptyBag(o1+^o2);
then
A153: b1 <> EmptyBag o1 or b2 <> EmptyBag o2 by A147,Th5;
now
per cases;
suppose
A154: b1 = EmptyBag o1;
Q1 = 1_(o1,Polynom-Ring(o2,L)).b1 by A146,POLYNOM1:31
.=1_Polynom-Ring(o2,L) by A154,POLYNOM1:25
.=1_(o2,L) by POLYNOM1:31;
then Q1.b2 = 0.L by A153,A154,POLYNOM1:25
.=1P2.b by A145,A152,POLYNOM1:25;
hence thesis by A148;
end;
suppose
A155: b1 <> EmptyBag o1;
Q1 = 1_(o1,Polynom-Ring(o2,L)).b1 by A146,POLYNOM1:31
.=0.Polynom-Ring(o2,L) by A155,POLYNOM1:25
.=0_(o2,L) by POLYNOM1:def 11;
then Q1.b2 = 0.L by POLYNOM1:22
.=1P2.b by A145,A152,POLYNOM1:25;
hence thesis by A148;
end;
end;
hence thesis;
end;
end;
f.1_P1 = Compress 1P1 by A2
.= 1_P2 by A144,FUNCT_2:63;
hence f is unity-preserving by GROUP_1:def 13;
thus f is one-to-one
proof
let x1,x2 be object;
assume x1 in dom f;
then reconsider x19=x1 as Element of P1 by FUNCT_2:def 1;
assume x2 in dom f;
then reconsider x29=x2 as Element of P1 by FUNCT_2:def 1;
reconsider x299=x29 as Polynomial of o1,Polynom-Ring(o2,L) by
POLYNOM1:def 11;
reconsider x199=x19 as Polynomial of o1,Polynom-Ring(o2,L) by
POLYNOM1:def 11;
A156: f.x29=Compress x299 by A2;
then reconsider w2=f.x29 as Polynomial of o1+^o2,L;
A157: f.x19=Compress x199 by A2;
then reconsider w1=f.x19 as Polynomial of o1+^o2,L;
assume
A158: f.x1 = f.x2;
now
let b1 be Element of Bags o1;
reconsider x199b1 = x199.b1, x299b1 = x299.b1 as Polynomial of o2,L by
POLYNOM1:def 11;
now
let b2 be Element of Bags o2;
set b = b1 +^b2;
consider b19 be Element of Bags o1, b29 be Element of Bags o2, Q1 be
Polynomial of o2,L such that
A159: Q1=x199.b19 and
A160: b = b19+^b29 and
A161: w1.b=Q1.b29 by A157,Def2;
A162: b1=b19 & b2=b29 by A160,Th7;
consider c1 be Element of Bags o1, c2 be Element of Bags o2, Q19 be
Polynomial of o2,L such that
A163: Q19=x299.c1 and
A164: b = c1+^c2 and
A165: w2.b=Q19.c2 by A156,Def2;
b1=c1 by A164,Th7;
hence x199b1.b2 = x299b1.b2 by A158,A159,A161,A163,A164,A165,A162,Th7;
end;
hence x199.b1 = x299.b1 by FUNCT_2:63;
end;
hence thesis by FUNCT_2:63;
end;
thus rng f c= the carrier of P2 by RELAT_1:def 19;
thus the carrier of P2 c= rng f
proof
defpred KK[set,set] means ex b1 being Element of Bags o1, b2 being Element
of Bags o2 st $1 = b1 +^b2 & $2 = b1;
let y be object;
assume y in the carrier of P2;
then reconsider s = y as Polynomial of o1+^o2,L by POLYNOM1:def 11;
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;
A166: 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
A167: x = b1+^b2 by Th6;
reconsider y = b1 as Element of Bags o1;
take y,b1,b2;
thus x = b1 +^b2 by A167;
thus y = b1;
end;
consider kk being Function of Bags(o1+^o2), Bags o1 such that
A168: for b being Element of Bags(o1+^o2) holds KK[b,kk.b] from
FUNCT_2:sch 3(A166);
A169: for x being Element of Bags o1 ex y being Element of Polynom-Ring(o2
,L) st K[x,y]
proof
defpred KK[set,set] means ex b1 being Element of Bags o1, b2 being
Element of Bags o2 st $1 = b1 +^b2 & $2 = b2;
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;
A170: 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 s.(b1+^p);
let b being Element of Bags (o1+^o2);
assume b = b1 +^p;
hence thesis;
end;
consider t being Function of Bags o2, the carrier of L such that
A171: for b2 be Element of Bags o2 holds L[b2,t.b2] from FUNCT_2:sch
3(A170);
reconsider t as Function of Bags o2, L;
A172: 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
A173: x = b1+^b2 by Th6;
reconsider y = b2 as Element of Bags o2;
take y,b1,b2;
thus x = b1 +^b2 by A173;
thus y = b2;
end;
consider kk being Function of Bags(o1+^o2), Bags o2 such that
A174: for b being Element of Bags(o1+^o2) holds KK[b,kk.b] from
FUNCT_2:sch 3(A172);
Support t c= kk.:Support s
proof
let x be object;
assume
A175: x in Support t;
then reconsider b2 = x as Element of Bags o2;
set b = b1+^b2;
t.x<>0.L by A175,POLYNOM1:def 4;
then s.b<>0.L by A171;
then
A176: dom kk = Bags (o1+^o2) & b in Support s by FUNCT_2:def 1,POLYNOM1:def 4
;
ex b19 being Element of Bags o1, b29 being Element of Bags o2 st
b = b19+^b29 & kk.b = b29 by A174;
then x = kk.b by Th7;
hence thesis by A176,FUNCT_1:def 6;
end;
then t is Polynomial of o2,L by POLYNOM1:def 5;
then reconsider t99=t as Element of Polynom-Ring(o2,L) by POLYNOM1:def 11
;
reconsider t9 = t as Function;
take t99,t9;
thus t99 =t9;
let b2 be Element of Bags o2, b be Element of Bags (o1+^o2);
assume b = x +^b2;
hence thesis by A171;
end;
consider g be Function of Bags o1,the carrier of Polynom-Ring(o2,L) such
that
A177: for x being Element of Bags o1 holds K[x,g.x] from FUNCT_2:sch 3
(A169);
reconsider g as Function of Bags o1,Polynom-Ring(o2,L);
A178: Support g c= kk.:Support s
proof
let x be object;
assume
A179: x in Support g;
then reconsider b1 = x as Element of Bags o1;
consider h be Function such that
A180: h = g.b1 and
A181: for b2 be Element of Bags o2, b be Element of Bags (o1+^o2) st
b = b1 +^b2 holds h.b2 = s.b by A177;
reconsider h as Polynomial of o2,L by A180,POLYNOM1:def 11;
g.b1<>0.Polynom-Ring(o2,L) by A179,POLYNOM1:def 4;
then g.b1<>0_(o2,L) by POLYNOM1:def 11;
then consider b2 be Element of Bags o2 such that
A182: b2 in Support h by A180,POLYNOM2:17,SUBSET_1:4;
set b = b1+^b2;
h.b2 <> 0.L by A182,POLYNOM1:def 4;
then s.b <> 0.L by A181;
then
A183: dom kk = Bags (o1+^o2) & b in Support s by FUNCT_2:def 1,POLYNOM1:def 4;
ex b19 being Element of Bags o1, b29 being Element of Bags o2 st b
= b19+^b29 & kk.b = b19 by A168;
then x = kk.b by Th7;
hence thesis by A183,FUNCT_1:def 6;
end;
then g is Polynomial of o1,Polynom-Ring(o2,L) by POLYNOM1:def 5;
then reconsider g as Element of P1 by POLYNOM1:def 11;
reconsider g9 = g as Polynomial of o1,Polynom-Ring(o2,L) by A178,
POLYNOM1:def 5;
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
A184: Q1=g9.b1 & b = b1+^b2 & (Compress g9).b=Q1.b2 by Def2;
ex h be Function st h = g9.b1 & for b2 be Element of Bags o2, b be
Element of Bags (o1+^o2) st b = b1 +^b2 holds h.b2 = s.b by A177;
hence s.b = (Compress g9).b by A184;
end;
then
A185: y = Compress g9 by FUNCT_2:63
.= f.g by A2;
dom f = the carrier of P1 by FUNCT_2:def 1;
hence thesis by A185,FUNCT_1:3;
end;
end;