:: The Ring of Polynomials
:: by Robert Milewski
::
:: Received April 17, 2000
:: Copyright (c) 2000-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, RLVECT_1, ALGSTR_0, XBOOLE_0, FINSEQ_1, STRUCT_0,
SUBSET_1, RELAT_1, FUNCT_1, SUPINF_2, CARD_3, NAT_1, PARTFUN1, FINSEQ_5,
ORDINAL4, ARYTM_3, XXREAL_0, FINSEQ_3, FINSEQ_2, PRE_POLY, TARSKI,
CARD_1, ORDERS_1, RELAT_2, FINSET_1, ARYTM_1, FUNCT_2, POLYNOM1,
ALGSEQ_1, FUNCOP_1, FUNCT_4, MESFUNC1, LATTICES, VECTSP_1, BINOP_1,
CLASSES1, GROUP_1, ZFMISC_1, POLYNOM3, XCMPLX_0, VALUED_0;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, CARD_1, ORDINAL1, NUMBERS,
XCMPLX_0, RELAT_1, RELAT_2, FUNCT_1, ORDERS_1, XXREAL_0, XREAL_0, NAT_1,
NAT_D, CLASSES1, RELSET_1, PARTFUN1, FINSET_1, FUNCT_2, FUNCOP_1,
FINSEQ_1, PRE_POLY, FINSEQ_2, FINSEQ_5, BINOP_1, RVSUM_1, FUNCT_7,
TREES_4, VALUED_0, WSIERP_1, MATRIX_0, STRUCT_0, ALGSTR_0, MATRLIN,
GROUP_1, RLVECT_1, VFUNCT_1, FVSUM_1, VECTSP_1, NORMSP_1, POLYNOM1,
ALGSEQ_1, RECDEF_1;
constructors BINOP_1, FINSEQOP, REALSET1, NAT_D, FINSEQ_5, WSIERP_1, ALGSEQ_1,
TRIANG_1, POLYNOM1, RECDEF_1, BINARITH, CLASSES1, RELSET_1, FUNCT_7,
MATRLIN, FVSUM_1, VFUNCT_1, NUMBERS;
registrations ORDINAL1, FUNCT_2, NUMBERS, XXREAL_0, XREAL_0, NAT_1, INT_1,
MEMBERED, FINSEQ_1, FINSEQ_2, FINSEQ_5, STRUCT_0, VECTSP_1, VALUED_0,
FINSET_1, RELSET_1, PRE_POLY, VFUNCT_1, CARD_1, FUNCT_1, FINSEQ_3,
WSIERP_1;
requirements NUMERALS, BOOLE, SUBSET, REAL, ARITHM;
definitions TARSKI, XBOOLE_0, RELAT_1, RELAT_2, RLVECT_1, GROUP_1, VECTSP_1,
ALGSEQ_1, FUNCT_2, ALGSTR_0;
equalities XBOOLE_0, FINSEQ_2, STRUCT_0, ALGSTR_0;
expansions RELAT_2, VECTSP_1, ALGSEQ_1, FUNCT_2;
theorems AXIOMS, TARSKI, ENUMSET1, RELSET_1, INT_1, NAT_1, CARD_1, RLVECT_1,
VECTSP_1, ALGSEQ_1, RELAT_2, ORDERS_1, FUNCT_1, FUNCT_2, FUNCT_7,
FUNCOP_1, FINSEQ_1, FINSEQ_2, FINSEQ_3, FINSEQ_4, FINSEQ_5, RFINSEQ,
BINOP_1, CARD_3, RVSUM_1, FVSUM_1, MATRLIN, POLYNOM1, RELAT_1, XBOOLE_0,
RLVECT_2, XCMPLX_1, PARTFUN1, GROUP_1, XREAL_1, XXREAL_0, ORDINAL1,
BHSP_1, NORMSP_1, XREAL_0, NAT_D, PRE_POLY, NUMBERS, VALUED_0, RVSUM_2;
schemes FUNCT_2, FINSEQ_1, FINSEQ_2, NAT_1, RELSET_1, SUBSET_1, BINOP_1,
RECDEF_1;
begin :: Preliminaries
theorem Th1:
for L be add-associative right_zeroed right_complementable non
empty addLoopStr for p be FinSequence of the carrier of L st for i be Element
of NAT st i in dom p holds p.i = 0.L holds Sum p = 0.L
proof
let L be add-associative right_zeroed right_complementable non empty
addLoopStr;
let p be FinSequence of the carrier of L;
assume
A1: for k be Element of NAT st k in dom p holds p.k = 0.L;
now
let k be Nat;
assume
A2: k in dom p;
hence p/.k = p.k by PARTFUN1:def 6
.= 0.L by A1,A2;
end;
hence thesis by MATRLIN:11;
end;
theorem Th2:
for V be Abelian add-associative right_zeroed non empty
addLoopStr for p be FinSequence of the carrier of V holds Sum p = Sum Rev p
proof
let V be Abelian add-associative right_zeroed non empty addLoopStr;
defpred P[FinSequence of the carrier of V] means Sum $1 = Sum Rev $1;
A1: for p be FinSequence of the carrier of V for x be Element of V st P[p]
holds P[p^<*x*>]
proof
let p be FinSequence of the carrier of V;
let x be Element of V;
assume
A2: Sum p = Sum Rev p;
thus Sum (p^<*x*>) = Sum p + Sum <*x*> by RLVECT_1:41
.= Sum (<*x*>^Rev p) by A2,RLVECT_1:41
.= Sum Rev (p^<*x*>) by FINSEQ_5:63;
end;
A3: P[<*>(the carrier of V)];
thus for p be FinSequence of the carrier of V holds P[p] from FINSEQ_2:sch 2
(A3,A1);
end;
theorem Th3:
for p be REAL-valued FinSequence holds Sum p = Sum Rev p
proof
let p be REAL-valued FinSequence;
A0: p is FinSequence of REAL by RVSUM_1:145;
defpred P[FinSequence of REAL] means Sum $1 = Sum Rev $1;
A1: for p be FinSequence of REAL for x be Element of REAL st P[p] holds P[p^
<*x*>]
proof
let p be FinSequence of REAL;
let x be Element of REAL;
assume
A2: Sum p = Sum Rev p;
thus Sum (p^<*x*>) = Sum p + Sum <*x*> by RVSUM_1:75
.= Sum (<*x*>^Rev p) by A2,RVSUM_1:75
.= Sum Rev (p^<*x*>) by FINSEQ_5:63;
end;
A3: P[<*>(REAL)];
for p be FinSequence of REAL holds P[p] from FINSEQ_2:sch 2(A3,A1);
hence thesis by A0;
end;
theorem Th4:
for p being natural-valued FinSequence, i being Nat st i in dom p
holds Sum p >= p.i
proof
let p be natural-valued FinSequence;
let i be Nat;
A0: p is FinSequence of NAT by FINSEQ_1:103;
defpred P[FinSequence of NAT] means for i be Element of NAT st i in dom $1
holds Sum $1 >= $1.i;
A1: for p be FinSequence of NAT for x being Element of NAT st P[p] holds P[p
^<*x*>]
proof
let p be FinSequence of NAT qua set;
let x be Element of NAT;
assume
A2: for i be Element of NAT st i in dom p holds Sum p >= p.i;
let i be Element of NAT;
A3: p.i + x >= p.i by NAT_1:11;
len (p^<*x*>) = len p + 1 by FINSEQ_2:16;
then
A4: dom (p^<*x*>) = Seg (len p + 1) by FINSEQ_1:def 3
.= Seg len p \/ {len p + 1} by FINSEQ_1:9
.= dom p \/ {len p + 1} by FINSEQ_1:def 3;
assume
A5: i in dom (p^<*x*>);
per cases by A5,A4,XBOOLE_0:def 3;
suppose
A6: i in dom p;
then Sum p + x >= p.i + x by A2,XREAL_1:6;
then Sum (p^<*x*>) >= p.i + x by RVSUM_1:74;
then Sum (p^<*x*>) >= p.i by A3,XXREAL_0:2;
hence thesis by A6,FINSEQ_1:def 7;
end;
suppose
i in {len p + 1};
then i = len p + 1 by TARSKI:def 1;
then (p^<*x*>).i = x by FINSEQ_1:42;
then Sum p + x >= (p^<*x*>).i by NAT_1:11;
hence thesis by RVSUM_1:74;
end;
end;
A7: P[<*> NAT qua FinSequence of NAT];
for p be FinSequence of NAT holds P[p] from FINSEQ_2:sch 2(A7,A1);
hence thesis by A0;
end;
definition
let D be non empty set;
let a,b be Element of D;
redefine func <*a,b*> -> Element of 2-tuples_on D; :: redefines <* (FINSEQ_1, definition)
coherence by FINSEQ_2:101;
end;
definition
let D be non empty set;
let k,n be Nat;
let p be Element of k-tuples_on D;
let q be Element of n-tuples_on D;
redefine func p^q -> Element of (k+n)-tuples_on D; :: redefines ^ (FINSEQ_1, definition)
coherence
proof
p^q is Tuple of k+n,D;
hence thesis by FINSEQ_2:131;
end;
end;
definition
let D be non empty set;
let k,n be Nat;
let p be FinSequence of k-tuples_on D;
let q be FinSequence of n-tuples_on D;
redefine func p ^^ q -> Element of ((k+n)-tuples_on D)*; :: redefines ^^ (PRE_POLY, definition)
coherence
proof
rng (p^^q) c= (k+n)-tuples_on D
proof
let y be object;
assume y in rng (p^^q);
then consider x be object such that
A1: x in dom (p^^q) and
A2: y = (p^^q).x by FUNCT_1:def 3;
reconsider x as set by TARSKI:1;
A3: x in (dom p) /\ (dom q) by A1,PRE_POLY:def 4;
then
A4: x in dom p by XBOOLE_0:def 4;
A5: x in dom q by A3,XBOOLE_0:def 4;
y = p.x ^ q.x by A1,A2,PRE_POLY:def 4
.= (p/.x) ^ q.x by A4,PARTFUN1:def 6
.= (p/.x) ^ (q/.x) by A5,PARTFUN1:def 6;
then y is Tuple of k+n,D;
hence thesis by FINSEQ_2:131;
end;
then p^^q is FinSequence of (k+n)-tuples_on D by FINSEQ_1:def 4;
hence thesis by FINSEQ_1:def 11;
end;
end;
scheme
SeqOfSeqLambdaD{D()->non empty set,A()->Element of NAT, T(Nat)->
Element of NAT, F(set,set)->Element of D()}:
ex p be FinSequence of D()* st len
p = A() & for k be Element of NAT st k in Seg A() holds len (p/.k) = T(k) & for
n be Element of NAT st n in dom (p/.k) holds (p/.k).n = F(k,n) proof
defpred P[Nat,FinSequence] means len $2 = T($1) & for n be
Element of NAT st n in dom $2 holds $2.n = F($1,n);
A1: for k be Nat st k in Seg A() ex d be Element of D()* st P[k,d ]
proof
let k be Nat;
assume k in Seg A();
deffunc G(Nat) = F(k,$1);
consider d be FinSequence of D() such that
A2: len d = T(k) and
A3: for n be Nat st n in dom d holds d.n = G(n) from FINSEQ_2:sch 1;
reconsider d as Element of D()* by FINSEQ_1:def 11;
take d;
thus len d = T(k) by A2;
let n be Element of NAT;
assume n in dom d;
hence thesis by A3;
end;
consider p be FinSequence of D()* such that
A4: dom p = Seg A() and
A5: for k be Nat st k in Seg A() holds P[k,p/.k] from
RECDEF_1:sch 17(A1);
take p;
thus len p = A() by A4,FINSEQ_1:def 3;
let k be Element of NAT;
assume k in Seg A();
hence thesis by A5;
end;
begin :: The Lexicographic Order of Finite Sequences
definition
let n be Nat;
let p,q be Element of n-tuples_on NAT;
pred p < q means
ex i be Element of NAT st i in Seg n & p.i < q.i &
for k be Nat st 1 <= k & k < i holds p.k = q.k;
asymmetry
proof
let p,q be Element of n-tuples_on NAT;
given i be Element of NAT such that
A1: i in Seg n and
A2: p.i < q.i and
A3: for k be Nat st 1 <= k & k < i holds p.k = q.k;
A4: 1 <= i by A1,FINSEQ_1:1;
given j be Element of NAT such that
A5: j in Seg n and
A6: q.j < p.j and
A7: for k be Nat st 1 <= k & k < j holds q.k = p.k;
A8: 1 <= j by A5,FINSEQ_1:1;
per cases by XXREAL_0:1;
suppose
i < j;
hence contradiction by A2,A7,A4;
end;
suppose
j < i;
hence contradiction by A3,A6,A8;
end;
suppose
i = j;
hence contradiction by A2,A6;
end;
end;
end;
notation
let n be Element of NAT;
let p,q be Element of n-tuples_on NAT;
synonym q > p for p < q;
end;
definition
let n be Element of NAT;
let p,q be Element of n-tuples_on NAT;
pred p <= q means
p < q or p = q;
reflexivity;
end;
notation
let n be Element of NAT;
let p,q be Element of n-tuples_on NAT;
synonym q >= p for p <= q;
end;
theorem Th5:
for n be Element of NAT for p,q,r be Element of n-tuples_on NAT
holds (p < q & q < r implies p < r) & ( p < q & q <= r or p <= q & q < r or p
<= q & q <= r implies p <= r)
proof
let n be Element of NAT;
let p,q,r be Element of n-tuples_on NAT;
thus
A1: p < q & q < r implies p < r
proof
assume that
A2: p < q and
A3: q < r;
consider i be Element of NAT such that
A4: i in Seg n and
A5: p.i < q.i and
A6: for k be Nat st 1 <= k & k < i holds p.k = q.k by A2;
consider j be Element of NAT such that
A7: j in Seg n and
A8: q.j < r.j and
A9: for k be Nat st 1 <= k & k < j holds q.k = r.k by A3;
reconsider t = min(i,j) as Element of NAT;
take t;
thus t in Seg n by A4,A7,XXREAL_0:15;
now
per cases by XXREAL_0:1;
suppose
A10: i < j;
A11: i >= 1 by A4,FINSEQ_1:1;
t = i by A10,XXREAL_0:def 9;
hence p.t < r.t by A5,A9,A10,A11;
end;
suppose
A12: i > j;
A13: j >= 1 by A7,FINSEQ_1:1;
t = j by A12,XXREAL_0:def 9;
hence p.t < r.t by A6,A8,A12,A13;
end;
suppose
i = j;
hence p.t < r.t by A5,A8,XXREAL_0:2;
end;
end;
hence p.t < r.t;
let k be Nat;
assume that
A14: 1 <= k and
A15: k < t;
t <= j by XXREAL_0:17;
then
A16: k < j by A15,XXREAL_0:2;
t <= i by XXREAL_0:17;
then k < i by A15,XXREAL_0:2;
hence p.k = q.k by A6,A14
.= r.k by A9,A14,A16;
end;
assume
A17: p < q & q <= r or p <= q & q < r or p <= q & q <= r;
per cases by A17;
suppose
A18: p < q & q <= r;
thus thesis by A1,A18;
end;
suppose
A19: p <= q & q < r;
thus thesis by A1,A19;
end;
suppose
p <= q & q <= r;
hence thesis by A1;
end;
end;
theorem Th6:
for n be Nat for p,q be Element of n-tuples_on NAT
holds p <> q implies ex i be Element of NAT st i in Seg n & p.i <> q.i &
for k be Nat st 1 <= k & k < i holds p.k = q.k
proof
defpred P[Nat] means for p,q be Element of $1-tuples_on NAT holds p <> q
implies ex i be Element of NAT st i in Seg $1 & p.i <> q.i &
for k be Nat st 1 <= k & k < i holds p.k = q.k;
A1: for n be Nat st P[n] holds P[n+1]
proof
let n be Nat;
assume
A2: for p,q be Element of n-tuples_on NAT holds p <> q implies ex i be
Element of NAT st i in Seg n & p.i <> q.i & for k be Nat st 1 <= k &
k < i holds p.k = q.k;
let p,q be Element of (n+1)-tuples_on NAT;
consider t1 be Element of n-tuples_on NAT, d1 be Element of NAT such that
A3: p = t1^<*d1*> by FINSEQ_2:117;
assume
A4: p <> q;
consider t2 be Element of n-tuples_on NAT, d2 be Element of NAT such that
A5: q = t2^<*d2*> by FINSEQ_2:117;
A6: len t1 = n by CARD_1:def 7;
A7: len t2 = n by CARD_1:def 7;
per cases;
suppose
t1 <> t2;
then consider i be Element of NAT such that
A8: i in Seg n and
A9: t1.i <> t2.i and
A10: for k be Nat st 1 <= k & k < i holds t1.k = t2.k by A2;
take i;
thus i in Seg (n+1) by A8,FINSEQ_2:8;
i in dom t1 by A6,A8,FINSEQ_1:def 3;
then
A11: p.i = t1.i by A3,FINSEQ_1:def 7;
i in dom t2 by A7,A8,FINSEQ_1:def 3;
hence p.i <> q.i by A5,A9,A11,FINSEQ_1:def 7;
let k be Nat;
assume that
A12: 1 <= k and
A13: k < i;
i <= n by A8,FINSEQ_1:1;
then
A14: k <= n by A13,XXREAL_0:2;
then
A15: k in dom t1 by A6,A12,FINSEQ_3:25;
A16: k in dom t2 by A7,A12,A14,FINSEQ_3:25;
t1.k = t2.k by A10,A12,A13;
hence p.k = t2.k by A3,A15,FINSEQ_1:def 7
.= q.k by A5,A16,FINSEQ_1:def 7;
end;
suppose
A17: t1 = t2;
take i = n+1;
thus i in Seg (n+1) by FINSEQ_1:4;
p.i = d1 by A3,FINSEQ_2:116;
hence p.i <> q.i by A3,A5,A4,A17,FINSEQ_2:116;
let k be Nat;
assume that
A18: 1 <= k and
A19: k < i;
A20: k <= n by A19,NAT_1:13;
then
A21: k in dom t2 by A7,A18,FINSEQ_3:25;
k in dom t1 by A6,A18,A20,FINSEQ_3:25;
hence p.k = t2.k by A3,A17,FINSEQ_1:def 7
.= q.k by A5,A21,FINSEQ_1:def 7;
end;
end;
A22: P[0];
thus for n be Nat holds P[n] from NAT_1:sch 2(A22,A1);
end;
theorem Th7:
for n be Element of NAT for p,q be Element of n-tuples_on NAT
holds p <= q or p > q
proof
let n be Element of NAT;
let p,q be Element of n-tuples_on NAT;
assume
A1: not p <= q;
then consider i be Element of NAT such that
A2: i in Seg n and
A3: p.i <> q.i and
A4: for k be Nat st 1 <= k & k < i holds p.k = q.k by Th6;
take i;
thus i in Seg n by A2;
not p < q by A1;
then p.i >= q.i by A2,A4;
hence q.i < p.i by A3,XXREAL_0:1;
thus thesis by A4;
end;
definition
let n be Element of NAT;
func TuplesOrder n -> Order of n-tuples_on NAT means
:Def3:
for p,q be Element of n-tuples_on NAT holds [p,q] in it iff p <= q;
existence
proof
defpred P[Element of n-tuples_on NAT,Element of n-tuples_on NAT] means $1
<= $2;
consider R be Relation of n-tuples_on NAT,n-tuples_on NAT such that
A1: for x,y be Element of n-tuples_on NAT holds [x,y] in R iff P[x,y]
from RELSET_1:sch 2;
A2: R is_transitive_in n-tuples_on NAT
proof
let x,y,z be object;
assume that
A3: x in n-tuples_on NAT & y in n-tuples_on NAT & z in n-tuples_on NAT and
A4: [x,y] in R & [y,z] in R;
reconsider x1=x, y1=y, z1=z as Element of n-tuples_on NAT by A3;
x1 <= y1 & y1 <= z1 by A1,A4;
then x1 <= z1 by Th5;
hence thesis by A1;
end;
A5: R is_reflexive_in n-tuples_on NAT
by A1;
then
A6: dom R = n-tuples_on NAT & field R =n-tuples_on NAT by ORDERS_1:13;
R is_antisymmetric_in n-tuples_on NAT
proof
let x,y be object;
assume that
A7: x in n-tuples_on NAT & y in n-tuples_on NAT and
A8: [x,y] in R and
A9: [y,x] in R;
reconsider x1=x, y1=y as Element of n-tuples_on NAT by A7;
x1 <= y1 by A1,A8;
then
A10: x1 < y1 or x1 = y1;
y1 <= x1 by A1,A9;
hence thesis by A10;
end;
then reconsider R as Order of n-tuples_on NAT by A5,A2,A6,PARTFUN1:def 2
,RELAT_2:def 9,def 12,def 16;
take R;
thus thesis by A1;
end;
uniqueness
proof
let T1,T2 be Order of n-tuples_on NAT such that
A11: for p,q be Element of n-tuples_on NAT holds [p,q] in T1 iff p <= q and
A12: for p,q be Element of n-tuples_on NAT holds [p,q] in T2 iff p <= q;
let x,y be object;
thus [x,y] in T1 implies [x,y] in T2
proof
assume
A13: [x,y] in T1;
then consider p,q be object such that
A14: [x,y] = [p,q] and
A15: p in n-tuples_on NAT & q in n-tuples_on NAT by RELSET_1:2;
reconsider p,q as Element of n-tuples_on NAT by A15;
p <= q by A11,A13,A14;
hence thesis by A12,A14;
end;
assume
A16: [x,y] in T2;
then consider p,q be object such that
A17: [x,y] = [p,q] and
A18: p in n-tuples_on NAT & q in n-tuples_on NAT by RELSET_1:2;
reconsider p,q as Element of n-tuples_on NAT by A18;
p <= q by A12,A16,A17;
hence thesis by A11,A17;
end;
end;
registration
let n be Element of NAT;
cluster TuplesOrder n -> being_linear-order;
coherence
proof
now
let x,y be object;
assume that
A1: x in n-tuples_on NAT & y in n-tuples_on NAT and
x <> y and
A2: not [x,y] in TuplesOrder n;
reconsider p=x, q=y as Element of n-tuples_on NAT by A1;
not p <= q by A2,Def3;
then p > q by Th7;
then q <= p;
hence [y,x] in TuplesOrder n by Def3;
end;
then
field TuplesOrder n = n-tuples_on NAT & TuplesOrder n is_connected_in
n -tuples_on NAT by ORDERS_1:15;
then TuplesOrder n is connected;
hence thesis by ORDERS_1:def 6;
end;
end;
begin :: Decomposition of Natural Numbers
definition
let i be non zero Element of NAT;
let n be Element of NAT;
func Decomp(n,i) -> FinSequence of i-tuples_on NAT means
:Def4:
ex A be
finite Subset of i-tuples_on NAT st it = SgmX (TuplesOrder i,A) & for p be
Element of i-tuples_on NAT holds p in A iff Sum p = n;
existence
proof
reconsider n1 = n+1 as non empty set;
defpred P[Element of i-tuples_on NAT] means Sum $1 = n;
consider A be Subset of i-tuples_on NAT such that
A1: for p be Element of i-tuples_on NAT holds p in A iff P[p] from
SUBSET_1:sch 3;
A2: A c= i-tuples_on (n+1)
proof
let x be object;
assume
A3: x in A;
then reconsider p=x as Element of i-tuples_on NAT;
A4: Sum p = n by A1,A3;
rng p c= n+1
proof
let y be object;
assume that
A5: y in rng p and
A6: not y in n+1;
rng p c= NAT by FINSEQ_1:def 4;
then reconsider k=y as Element of NAT by A5;
not y in { t where t is Nat : t < n+1 } by A6,AXIOMS:4;
then
A7: k >= n+1;
ex j be Nat st j in dom p & p.j = k by A5,FINSEQ_2:10;
then Sum p >= k by Th4;
hence contradiction by A4,A7,NAT_1:13;
end;
then len p = i & p is FinSequence of (n+1)
by CARD_1:def 7,FINSEQ_1:def 4;
then p is Element of i-tuples_on n1 by FINSEQ_2:92;
hence thesis;
end;
reconsider A as finite Subset of i-tuples_on NAT by A2;
take SgmX (TuplesOrder i,A);
thus thesis by A1;
end;
uniqueness
proof
let p1,p2 be FinSequence of i-tuples_on NAT;
given A1 be finite Subset of i-tuples_on NAT such that
A8: p1 = SgmX (TuplesOrder i,A1) and
A9: for p be Element of i-tuples_on NAT holds p in A1 iff Sum p = n;
given A2 be finite Subset of i-tuples_on NAT such that
A10: p2 = SgmX (TuplesOrder i,A2) and
A11: for p be Element of i-tuples_on NAT holds p in A2 iff Sum p = n;
now
let x be object;
thus x in A1 implies x in A2
proof
assume
A12: x in A1;
then reconsider p = x as Element of i-tuples_on NAT;
Sum p = n by A9,A12;
hence thesis by A11;
end;
assume
A13: x in A2;
then reconsider p = x as Element of i-tuples_on NAT;
Sum p = n by A11,A13;
hence x in A1 by A9;
end;
hence thesis by A8,A10,TARSKI:2;
end;
end;
registration
let i be non zero Element of NAT;
let n be Element of NAT;
cluster Decomp(n,i) -> non empty one-to-one FinSequence-yielding;
coherence
proof
reconsider p2 = (i-'1)|->0 as FinSequence of NAT;
i >= 1 by NAT_1:14;
then i-'1+1 = i by XREAL_1:235;
then ((i-'1)|->0)^<*n*> is Tuple of i, NAT;
then reconsider p1 = ((i-'1)|->0)^<*n*> as Element of i-tuples_on NAT
by FINSEQ_2:131;
consider A be finite Subset of i-tuples_on NAT such that
A1: Decomp(n,i) = SgmX (TuplesOrder i,A) and
A2: for p be Element of i-tuples_on NAT holds p in A iff Sum p = n by Def4;
Sum p1 = Sum p2 + n by RVSUM_1:74
.= 0 +n by RVSUM_1:81;
then reconsider A as non empty finite Subset of i-tuples_on NAT by A2;
SgmX (TuplesOrder i,A) is non empty finite;
hence thesis by A1;
end;
end;
theorem Th8:
for n be Element of NAT holds len Decomp(n,1) = 1
proof
let n be Element of NAT;
consider A be finite Subset of 1-tuples_on NAT such that
A1: Decomp(n,1) = SgmX (TuplesOrder 1,A) and
A2: for p be Element of 1-tuples_on NAT holds p in A iff Sum p = n by Def4;
A3: A = {<*n*>}
proof
thus A c= {<*n*>}
proof
let y be object;
assume
A4: y in A;
then reconsider p=y as Element of 1-tuples_on NAT;
A5: Sum p = n by A2,A4;
consider k be Element of NAT such that
A6: p = <*k*> by FINSEQ_2:97;
Sum p = k by A6,RVSUM_1:73;
hence thesis by A5,A6,TARSKI:def 1;
end;
let y be object;
assume y in {<*n*>};
then
A7: y = <*n*> by TARSKI:def 1;
Sum <*n*> = n by RVSUM_1:73;
hence y in A by A2,A7;
end;
field TuplesOrder 1 = 1-tuples_on NAT by ORDERS_1:15;
then TuplesOrder 1 linearly_orders 1-tuples_on NAT by ORDERS_1:37;
hence len Decomp(n,1) = card A by A1,ORDERS_1:38,PRE_POLY:11
.= 1 by A3,CARD_1:30;
end;
theorem Th9:
for n be Element of NAT holds len Decomp(n,2) = n+1
proof
let n be Element of NAT;
deffunc F(Nat) = <*$1,n-'$1*>;
consider q be FinSequence such that
A1: len q = n and
A2: for k be Nat st k in dom q holds q.k = F(k) from FINSEQ_1:sch 2;
A3: dom q = Seg n by A1,FINSEQ_1:def 3;
set q1 = q^<*<*0,n*>*>;
A4: dom q = Seg n by A1,FINSEQ_1:def 3;
A5: len q1 = n+1 by A1,FINSEQ_2:16;
then
A6: dom q1 = Seg (n+1) by FINSEQ_1:def 3;
now
let x1,x2 be object;
assume that
A7: x1 in dom q1 and
A8: x2 in dom q1 and
A9: q1.x1 = q1.x2;
reconsider k1=x1, k2=x2 as Element of NAT by A7,A8;
x2 in Seg n \/ {n+1} by A6,A8,FINSEQ_1:9;
then
A10: x2 in Seg n or x2 in {n+1} by XBOOLE_0:def 3;
x1 in Seg n \/ {n+1} by A6,A7,FINSEQ_1:9;
then
A11: x1 in Seg n or x1 in {n+1} by XBOOLE_0:def 3;
now
per cases by A11,A10,TARSKI:def 1;
suppose
A12: x1 in Seg n & x2 in Seg n;
then
A13: q1.k1 = q.k1 & q1.k2 = q.k2 by A3,FINSEQ_1:def 7;
q.k1 = <*k1,n-'k1*> & q.k2 = <*k2,n-'k2*> by A2,A4,A12;
hence x1 = x2 by A9,A13,FINSEQ_1:77;
end;
suppose
A14: x1 in Seg n & x2 = n+1;
then
A15: q1.k2 = <*0,n*> by A1,FINSEQ_1:42;
q1.k1 = q.k1 by A3,A14,FINSEQ_1:def 7
.= <*k1,n-'k1*> by A2,A4,A14;
then k1 = 0 by A9,A15,FINSEQ_1:77;
hence x1 = x2 by A14,FINSEQ_1:1;
end;
suppose
A16: x1 = n+1 & x2 in Seg n;
then
A17: q1.k1 = <*0,n*> by A1,FINSEQ_1:42;
q1.k2 = q.k2 by A3,A16,FINSEQ_1:def 7
.= <*k2,n-'k2*> by A2,A4,A16;
then k2 = 0 by A9,A17,FINSEQ_1:77;
hence x1 = x2 by A16,FINSEQ_1:1;
end;
suppose
x1 = n+1 & x2 = n+1;
hence x1 = x2;
end;
end;
hence x1 = x2;
end;
then q1 is one-to-one by FUNCT_1:def 4;
then
A18: card(rng q1) = n+1 by A5,FINSEQ_4:62;
A19: rng q c= rng q1 by FINSEQ_1:29;
A20: rng q1 = {<*i,n-'i*> where i is Element of NAT : i <= n}
proof
thus rng q1 c= {<*i,n-'i*> where i is Element of NAT : i <= n}
proof
let x be object;
assume x in rng q1;
then consider j be Nat such that
A21: j in dom q1 and
A22: q1.j = x by FINSEQ_2:10;
reconsider j as Element of NAT by ORDINAL1:def 12;
j in Seg n \/ {n+1} by A6,A21,FINSEQ_1:9;
then
A23: j in Seg n or j in {n+1} by XBOOLE_0:def 3;
now
per cases by A23,TARSKI:def 1;
suppose
A24: j in Seg n;
then
A25: q1.j = q.j by A3,FINSEQ_1:def 7;
q.j = <*j,n-'j*> & j <= n by A2,A4,A24,FINSEQ_1:1;
hence thesis by A22,A25;
end;
suppose
j = n+1;
then q1.j = <*0,n*> by A1,FINSEQ_1:42
.= <*0,n-'0*> by NAT_D:40;
hence thesis by A22;
end;
end;
hence thesis;
end;
let x be object;
assume x in {<*i,n-'i*> where i is Element of NAT : i <= n};
then consider i be Element of NAT such that
A26: x = <*i,n-'i*> and
A27: i <= n;
A28: i = 0 or i >= 0 qua Nat+1 by NAT_1:13;
now
per cases by A27,A28,FINSEQ_1:1;
suppose
A29: i = 0;
A30: n+1 in dom q1 by A6,FINSEQ_1:4;
q1.(n+1) = <*0,n*> by A1,FINSEQ_1:42
.= x by A26,A29,NAT_D:40;
hence thesis by A30,FUNCT_1:def 3;
end;
suppose
A31: i in Seg n;
then q.i = x by A2,A4,A26;
then x in rng q by A3,A31,FUNCT_1:def 3;
hence thesis by A19;
end;
end;
hence thesis;
end;
consider A be finite Subset of 2-tuples_on NAT such that
A32: Decomp(n,2) = SgmX (TuplesOrder 2,A) and
A33: for p be Element of 2-tuples_on NAT holds p in A iff Sum p = n by Def4;
A34: A = {<*i,n-'i*> where i is Element of NAT : i <= n}
proof
thus A c= {<*i,n-'i*> where i is Element of NAT : i <= n}
proof
let x be object;
assume
A35: x in A;
then reconsider p=x as Element of 2-tuples_on NAT;
consider d1,d2 be Element of NAT such that
A36: p = <*d1,d2*> by FINSEQ_2:100;
A37: d1+d2 = Sum p by A36,RVSUM_1:77
.= n by A33,A35;
then n-d1 >= 0;
then
A38: d2 = n-'d1 by A37,XREAL_0:def 2;
d1 <= n by A37,NAT_1:11;
hence thesis by A36,A38;
end;
let x be object;
assume x in { <*i,n-'i*> where i is Element of NAT : i <= n };
then consider i be Element of NAT such that
A39: x = <*i,n-'i*> and
A40: i <= n;
A41: n-i >= 0 by A40,XREAL_1:48;
Sum <*i,n-'i*> = i+(n-'i) by RVSUM_1:77
.= i+(n-i) by A41,XREAL_0:def 2
.= n;
hence thesis by A33,A39;
end;
field TuplesOrder 2 = 2-tuples_on NAT by ORDERS_1:15;
then TuplesOrder 2 linearly_orders 2-tuples_on NAT by ORDERS_1:37;
hence thesis by A32,A34,A20,A18,ORDERS_1:38,PRE_POLY:11;
end;
theorem
for n be Element of NAT holds Decomp(n,1) = <*<*n*>*>
proof
let n be Element of NAT;
consider A be finite Subset of 1-tuples_on NAT such that
A1: Decomp(n,1) = SgmX (TuplesOrder 1,A) and
A2: for p be Element of 1-tuples_on NAT holds p in A iff Sum p = n by Def4;
A3: A = {<*n*>}
proof
thus A c= {<*n*>}
proof
let y be object;
assume
A4: y in A;
then reconsider p=y as Element of 1-tuples_on NAT;
A5: Sum p = n by A2,A4;
consider k be Element of NAT such that
A6: p = <*k*> by FINSEQ_2:97;
Sum p = k by A6,RVSUM_1:73;
hence thesis by A5,A6,TARSKI:def 1;
end;
let y be object;
assume y in {<*n*>};
then
A7: y = <*n*> by TARSKI:def 1;
Sum <*n*> = n by RVSUM_1:73;
hence thesis by A2,A7;
end;
len Decomp(n,1) = 1 by Th8;
then
A8: dom Decomp(n,1) = Seg 1 by FINSEQ_1:def 3
.= dom <*<*n*>*> by FINSEQ_1:38;
field TuplesOrder 1 = 1-tuples_on NAT by ORDERS_1:15;
then TuplesOrder 1 linearly_orders A by ORDERS_1:37,38;
then rng <*<*n*>*> = {<*n*>} & rng Decomp(n,1) = {<*n*>} by A1,A3,FINSEQ_1:39
,PRE_POLY:def 2;
hence thesis by A8,FUNCT_1:7;
end;
theorem Th11:
for i,j,n,k1,k2 be Element of NAT st
Decomp(n,2).i = <*k1,n-'k1*> & Decomp(n,2).j = <*k2,n-'k2*>
holds i<j iff k1<k2
proof
let i,j,n,k1,k2 be Element of NAT;
assume that
A1: Decomp(n,2).i = <*k1,n-'k1*> and
A2: Decomp(n,2).j = <*k2,n-'k2*>;
A3: j in dom Decomp(n,2) by A2,FUNCT_1:def 2;
then
A4: Decomp(n,2).j = (Decomp(n,2))/.j by PARTFUN1:def 6;
consider A be finite Subset of 2-tuples_on NAT such that
A5: Decomp(n,2) = SgmX (TuplesOrder 2,A) and
for p be Element of 2-tuples_on NAT holds p in A iff Sum p = n by Def4;
field TuplesOrder 2 = 2-tuples_on NAT by ORDERS_1:15;
then
A6: TuplesOrder 2 linearly_orders A by ORDERS_1:37,38;
A7: i in dom Decomp(n,2) by A1,FUNCT_1:def 2;
then
A8: Decomp(n,2).i = (Decomp(n,2))/.i by PARTFUN1:def 6;
thus i<j implies k1<k2
proof
assume
A9: i<j;
then
[<*k1,n-'k1*>,<*k2,n-'k2*>] in TuplesOrder 2 by A5,A6,A1,A2,A7,A3,A8,A4,
PRE_POLY:def 2;
then
A10: <*k1,n-'k1*> <= <*k2,n-'k2*> by Def3;
<*k1,n-'k1*> <> <*k2,n-'k2*> by A5,A6,A1,A2,A7,A3,A8,A4,A9,PRE_POLY:def 2;
then <*k1,n-'k1*> < <*k2,n-'k2*> by A10;
then consider t be Element of NAT such that
A11: t in Seg 2 and
A12: <*k1,n-'k1*>.t < <*k2,n-'k2*>.t and
A13: for k be Nat st 1 <= k & k < t holds <*k1,n-'k1*>.k =
<*k2,n-'k2*>.k;
per cases by A11,FINSEQ_1:2,TARSKI:def 2;
suppose
A14: t = 1;
thus thesis by A12,A14;
end;
suppose
t = 2;
then <*k1,n-'k1*>.1 = <*k2,n-'k2*>.1 by A13;
then <*k1,n-'k1*>.1 = k2;
then k1 = k2;
hence thesis by A12;
end;
end;
assume
A15: k1<k2;
A16: for k be Nat st 1 <= k & k < 1 holds <*k1,n-'k1*>.k = <*k2,n
-'k2*>.k;
A17: <*k1,n-'k1*>.1 = k1;
1 in Seg 2 & <*k2,n-'k2*>.1 = k2 by FINSEQ_1:1;
then
A18: <*k1,n-'k1*> < <*k2,n-'k2*> by A15,A17,A16;
assume
A19: i>=j;
per cases by A19,XXREAL_0:1;
suppose
i = j;
hence contradiction by A1,A2,A15,A17,FINSEQ_1:44;
end;
suppose
j<i;
then
[<*k2,n-'k2*>,<*k1,n-'k1*>] in TuplesOrder 2 by A5,A6,A1,A2,A7,A3,A8,A4,
PRE_POLY:def 2;
then
A20: <*k2,n-'k2*> <= <*k1,n-'k1*> by Def3;
thus contradiction by A18,A20;
end;
end;
theorem Th12:
for i,n,k1,k2 be Element of NAT st Decomp(n,2).i = <*k1,n-'k1*>
& Decomp(n,2).(i+1) = <*k2,n-'k2*> holds k2=k1+1
proof
let i,n,k1,k2 be Element of NAT;
assume that
A1: Decomp(n,2).i = <*k1,n-'k1*> and
A2: Decomp(n,2).(i+1) = <*k2,n-'k2*>;
assume
A3: k2 <> k1+1;
i+(0 qua Nat) < i+1 by XREAL_1:6;
then
A4: k1 < k2 by A1,A2,Th11;
then k1+1 <= k2 by NAT_1:13;
then
A5: k1+1 < k2 by A3,XXREAL_0:1;
consider A be finite Subset of 2-tuples_on NAT such that
A6: Decomp(n,2) = SgmX (TuplesOrder 2,A) and
A7: for p be Element of 2-tuples_on NAT holds p in A iff Sum p = n by Def4;
field TuplesOrder 2 = 2-tuples_on NAT by ORDERS_1:15;
then TuplesOrder 2 linearly_orders A by ORDERS_1:37,38;
then
A8: rng Decomp(n,2) = A by A6,PRE_POLY:def 2;
k1 < n
proof
Sum <*k2,n-'k2*> = k2 + (n-'k2) by RVSUM_1:77;
then
A9: Sum <*k2,n-'k2*> >= k2 by NAT_1:11;
assume k1 >= n;
then k2 > n by A4,XXREAL_0:2;
then not Decomp(n,2).(i+1) in rng Decomp(n,2) by A7,A8,A2,A9;
then not i+1 in dom Decomp(n,2) by FUNCT_1:def 3;
hence contradiction by A2,FUNCT_1:def 2;
end;
then
A10: k1+1 <= n by NAT_1:13;
Sum <*k1+1,n-'(k1+1)*> = k1+1+(n-'(k1+1)) by RVSUM_1:77
.= n by A10,XREAL_1:235;
then <*k1+1,n-'(k1+1)*> in rng Decomp(n,2) by A7,A8;
then consider k be Nat such that
k in dom Decomp(n,2) and
A11: Decomp(n,2).k = <*k1+1,n-'(k1+1)*> by FINSEQ_2:10;
reconsider k as Element of NAT by ORDINAL1:def 12;
k1+(0 qua Nat) < k1+1 by XREAL_1:6;
then i < k by A1,A11,Th11;
then i+1 <= k by NAT_1:13;
hence contradiction by A2,A5,A11,Th11;
end;
theorem Th13:
for n be Element of NAT holds Decomp(n,2).1 = <*0,n*>
proof
let n be Element of NAT;
consider A be finite Subset of 2-tuples_on NAT such that
A1: Decomp(n,2) = SgmX (TuplesOrder 2,A) and
A2: for p be Element of 2-tuples_on NAT holds p in A iff Sum p = n by Def4;
A3: now
let y be Element of 2-tuples_on NAT;
consider d1,d2 be Element of NAT such that
A4: y = <*d1,d2*> by FINSEQ_2:100;
assume y in A;
then Sum <*d1,d2*> = n by A2,A4;
then
A5: d1 + d2 = n by RVSUM_1:77;
now
per cases;
suppose
d1 = 0;
hence <*0,n*> <= <*d1,d2*> by A5;
end;
suppose
d1 > 0;
then <*0,n*>.1 < d1;
then
A6: <*0,n*>.1 < <*d1,d2*>.1;
1 in Seg 2 & for k be Nat st 1 <= k & k < 1 holds <*0,
n*>.k = <* d1,d2*>.k by FINSEQ_1:1;
then <*0,n*> < <*d1,d2*> by A6;
hence <*0,n*> <= <*d1,d2*>;
end;
end;
hence [<*0,n*>,y] in TuplesOrder 2 by A4,Def3;
end;
1 <= n+1 by NAT_1:11;
then 1 in Seg (n+1) by FINSEQ_1:1;
then 1 in Seg len Decomp(n,2) by Th9;
then
A7: 1 in dom Decomp(n,2) by FINSEQ_1:def 3;
field TuplesOrder 2 = 2-tuples_on NAT by ORDERS_1:15;
then
A8: TuplesOrder 2 linearly_orders A by ORDERS_1:37,38;
Sum <*0,n*> = 0 qua Nat+n by RVSUM_1:77;
then <*0,n*> in A by A2;
then (SgmX (TuplesOrder 2,A))/.1 = <*0,n*> by A8,A3,PRE_POLY:20;
hence thesis by A1,A7,PARTFUN1:def 6;
end;
theorem Th14:
for n,i be Element of NAT st i in Seg (n+1) holds Decomp(n,2).i
= <*i-'1,n+1-'i*>
proof
let n,i be Element of NAT;
defpred P[Nat] means $1 <= n+1 implies Decomp(n,2).$1 = <*$1-'1,n+1-'$1*>;
assume i in Seg (n+1);
then
A1: 1 <= i & i <= n+1 by FINSEQ_1:1;
consider A be finite Subset of 2-tuples_on NAT such that
A2: Decomp(n,2) = SgmX (TuplesOrder 2,A) and
A3: for p be Element of 2-tuples_on NAT holds p in A iff Sum p = n by Def4;
A4: for j be non zero Nat st P[j] holds P[j+1]
proof
field TuplesOrder 2 = 2-tuples_on NAT by ORDERS_1:15;
then
A5: TuplesOrder 2 linearly_orders A by ORDERS_1:37,38;
let j be non zero Nat;
assume that
A6: j <= n+1 implies Decomp(n,2).j = <*j-'1,n+1-'j*> and
A7: j+1 <= n+1;
n >= j by A7,XREAL_1:6;
then
A8: n-j >= 0 by XREAL_1:48;
n+1-(j+1) >= 0 by A7,XREAL_1:48;
then
A9: n+1-'(j+1) = n-j by XREAL_0:def 2
.= n-'j by A8,XREAL_0:def 2;
reconsider jj=j as non zero Element of NAT by ORDINAL1:def 12;
j >= 1 by NAT_1:14;
then
A10: j-1 >= 1-1 by XREAL_1:9;
j+1 >= 1 by NAT_1:11;
then j+1 in Seg (n+1) by A7,FINSEQ_1:1;
then j+1 in Seg len Decomp(n,2) by Th9;
then
A11: j+1 in dom Decomp(n,2) by FINSEQ_1:def 3;
then Decomp(n,2).(j+1) = (Decomp(n,2))/.(j+1) by PARTFUN1:def 6;
then consider d1,d2 be Element of NAT such that
A12: Decomp(n,2).(j+1) = <*d1,d2*> by FINSEQ_2:100;
Decomp(n,2).(j+1) in rng Decomp(n,2) by A11,FUNCT_1:def 3;
then Decomp(n,2).(j+1) in A by A2,A5,PRE_POLY:def 2;
then Sum <*d1,d2*> = n by A3,A12;
then
A13: d1+d2 = n by RVSUM_1:77;
then n-d1 >= 0;
then
A14: d2 = n-'d1 by A13,XREAL_0:def 2;
j < n+1 by A7,NAT_1:13;
then
A15: n+1-j >= 0 by XREAL_1:48;
then n-(j-1) >= 0;
then
A16: n-(j-'1) >= 0 by A10,XREAL_0:def 2;
n+1-'j = n-(j-1) by A15,XREAL_0:def 2
.= n-(j-'1) by A10,XREAL_0:def 2
.= n-'(j-'1) by A16,XREAL_0:def 2;
then d1 = jj-'1+1 by A6,A7,A12,A14,Th12,NAT_1:13
.= j by NAT_1:14,XREAL_1:235;
hence thesis by A12,A14,A9,NAT_D:34;
end;
A17: P[1]
proof
assume 1 <= n+1;
thus Decomp(n,2).1 = <*0,n*> by Th13
.= <*1-'1,n*> by XREAL_1:232
.= <*1-'1,n+1-'1*> by NAT_D:34;
end;
for j be non zero Nat holds P[j] from NAT_1:sch 10(A17,A4);
hence thesis by A1;
end;
definition
let L be non empty multMagma;
let p,q,r be sequence of L;
let t be FinSequence of 3-tuples_on NAT;
func prodTuples(p,q,r,t) -> Element of (the carrier of L)* means
:Def5:
len
it = len t & for k be Element of NAT st k in dom t holds it.k = (p.((t/.k)/.1))
*(q.((t/.k)/.2))*(r.((t/.k)/.3));
existence
proof
deffunc F(Nat) = (p.((t/.$1)/.1))*(q.((t/.$1)/.2))*(r.((t/.$1)/.3));
consider p1 be FinSequence of the carrier of L such that
A1: len p1 = len t and
A2: for k be Nat st k in dom p1 holds p1.k = F(k) from FINSEQ_2:sch 1;
A3: dom p1 = Seg len t by A1,FINSEQ_1:def 3;
reconsider p1 as Element of (the carrier of L)* by FINSEQ_1:def 11;
take p1;
thus len p1 = len t by A1;
let k be Element of NAT;
assume k in dom t;
then k in Seg len t by FINSEQ_1:def 3;
hence thesis by A2,A3;
end;
uniqueness
proof
let p1,p2 be Element of (the carrier of L)* such that
A4: len p1 = len t and
A5: for k be Element of NAT st k in dom t holds p1.k = (p.((t/.k)/.1))
*(q.((t/.k)/.2))*(r.((t/.k)/.3)) and
A6: len p2 = len t and
A7: for k be Element of NAT st k in dom t holds p2.k = (p.((t/.k)/.1))
*(q.((t/.k)/.2))*(r.((t/.k)/.3));
A8: dom p1 = Seg len t by A4,FINSEQ_1:def 3;
now
let i be Nat;
assume i in dom p1;
then
A9: i in dom t by A8,FINSEQ_1:def 3;
hence p1.i = (p.((t/.i)/.1))*(q.((t/.i)/.2))*(r.((t/.i)/.3)) by A5
.= p2.i by A7,A9;
end;
hence thesis by A4,A6,FINSEQ_2:9;
end;
end;
theorem Th15:
for L be non empty multMagma for p,q,r be sequence of L for t be
FinSequence of 3-tuples_on NAT for P be Permutation of dom t for t1 be
FinSequence of 3-tuples_on NAT st t1 = t*P holds prodTuples(p,q,r,t1) =
prodTuples(p,q,r,t)*P
proof
let L be non empty multMagma;
let p,q,r be sequence of L;
let t be FinSequence of 3-tuples_on NAT;
let P be Permutation of dom t;
let t1 be FinSequence of 3-tuples_on NAT;
A1: rng P = dom t by FUNCT_2:def 3;
assume
A2: t1 = t*P;
then
A3: dom P = dom t1 by A1,RELAT_1:27;
A4: now
let x be object;
assume
A5: x in dom t1;
then reconsider i=x as Element of NAT;
A6: prodTuples(p,q,r,t1).i = (p.((t1/.i)/.1))*(q.((t1/.i)/.2))*(r.((t1/.i
)/.3)) & (prodTuples(p,q,r,t)*P).x = prodTuples(p,q,r,t).(P.x) by A3,A5,Def5,
FUNCT_1:13;
reconsider j=P.i as Element of NAT;
A7: P.i in rng P by A3,A5,FUNCT_1:def 3;
t1/.i = t1.i by A5,PARTFUN1:def 6
.= t.(P.i) by A2,A5,FUNCT_1:12
.= t/.j by A1,A7,PARTFUN1:def 6;
hence prodTuples(p,q,r,t1).x = (prodTuples(p,q,r,t)*P).x by A1,A7,A6,Def5;
end;
len prodTuples(p,q,r,t1) = len t1 by Def5;
then
A8: dom prodTuples(p,q,r,t1) = Seg len t1 by FINSEQ_1:def 3;
len prodTuples(p,q,r,t) = len t by Def5;
then rng P = dom prodTuples(p,q,r,t) by A1,FINSEQ_3:29;
then
A9: dom (prodTuples(p,q,r,t)*P) = dom t1 by A3,RELAT_1:27;
dom t1 = Seg len t1 by FINSEQ_1:def 3;
hence thesis by A8,A9,A4,FUNCT_1:2;
end;
theorem Th16:
for D be set, f be FinSequence of D*, i be Nat holds Card (f|i) = (Card f)|i
proof
let D be set;
let f be FinSequence of D*;
let i be Nat;
A1: f|i = f|Seg i by FINSEQ_1:def 16;
reconsider k = min(i,len f) as Nat by TARSKI:1;
dom Card (f|i) = dom (f|i) by CARD_3:def 2;
then
A2: len Card (f|i) = len (f|i) by FINSEQ_3:29
.= min(i,len f) by A1,FINSEQ_2:21;
then
A3: dom Card (f|i) = Seg k by FINSEQ_1:def 3;
A4: dom Card f = dom f by CARD_3:def 2;
A5: (Card f)|i = (Card f)|Seg i by FINSEQ_1:def 16;
A6: now
A7: len f = len Card f by A4,FINSEQ_3:29;
let j be Nat;
assume
A8: j in dom Card (f|i);
per cases;
suppose
A9: i <= len f;
A10: 1 <= j by A3,A8,FINSEQ_1:1;
A11: k = i by A9,XXREAL_0:def 9;
then j <= i by A3,A8,FINSEQ_1:1;
then j <= len f by A9,XXREAL_0:2;
then
A12: j in dom f by A10,FINSEQ_3:25;
len ((Card f)|i) = i by A7,A9,FINSEQ_1:59;
then
A13: dom ((Card f)|i) = Seg i by FINSEQ_1:def 3;
reconsider Cf = Card f as FinSequence of NAT qua set;
A14: Seg len (f|i) = dom (f|i) by FINSEQ_1:def 3;
A15: len(f|i) = i by A9,FINSEQ_1:59;
hence Card (f|i).j = card ((f|i).j) by A3,A8,A11,A14,CARD_3:def 2
.= card ((f|i)/.j) by A3,A8,A11,A15,A14,PARTFUN1:def 6
.= card (f/.j) by A3,A8,A11,A15,A14,FINSEQ_4:70
.= card (f.j) by A12,PARTFUN1:def 6
.= (Card f).j by A12,CARD_3:def 2
.= Cf/.j by A4,A12,PARTFUN1:def 6
.= (Cf|i)/.j by A3,A8,A11,A13,FINSEQ_4:70
.= (Card f)|i.j by A3,A8,A11,A13,PARTFUN1:def 6;
end;
suppose
A16: i > len f;
then f|i = f by A1,FINSEQ_2:20;
hence Card (f|i).j = (Card f)|i.j by A5,A7,A16,FINSEQ_2:20;
end;
end;
len ((Card f)|i) = min(i,len Card f) by A5,FINSEQ_2:21
.= min(i,len f) by A4,FINSEQ_3:29;
hence thesis by A2,A6,FINSEQ_2:9;
end;
::$CT
theorem Th17:
for p be natural-valued FinSequence for i,j be Nat st i <= j
holds Sum (p|i) <= Sum (p|j)
proof
let p be natural-valued FinSequence;
let i,j be Nat;
assume
A1: i <= j;
then consider k be Nat such that
A2: j = i + k by NAT_1:10;
reconsider k as Element of NAT by ORDINAL1:def 12;
reconsider p as FinSequence of NAT by FINSEQ_1:103;
per cases;
suppose
A3: j <= len p;
then
A4: len (p|j) = i + k by A2,FINSEQ_1:59;
then consider q,r be FinSequence of NAT such that
A5: len q = i and
len r = k and
A6: (p|j) = q^r by FINSEQ_2:23;
A7: len (p|i) = i by A1,A3,FINSEQ_1:59,XXREAL_0:2;
then
A8: dom (p|i) = Seg i by FINSEQ_1:def 3;
A9: now
let n be Nat;
assume
A10: n in dom (p|i);
then
A11: (p|i)/.n = p/.n by FINSEQ_4:70;
A12: Seg i = dom q by A5,FINSEQ_1:def 3;
A13: Seg i c= Seg j & Seg j = dom (p|j) by A1,A2,A4,FINSEQ_1:5,def 3;
Seg i = dom (p|i) by A7,FINSEQ_1:def 3;
then
A14: (p|j)/.n = p/.n by A10,A13,FINSEQ_4:70;
thus (p|i).n = (p|i)/.n by A10,PARTFUN1:def 6
.= (p|j).n by A8,A10,A13,A11,A14,PARTFUN1:def 6
.= q.n by A6,A8,A10,A12,FINSEQ_1:def 7;
end;
A15: Sum q + Sum r >= Sum q + (0 qua Nat) by XREAL_1:6;
Sum (p|j) = Sum q + Sum r by A6,RVSUM_1:75;
hence thesis by A7,A5,A9,A15,FINSEQ_2:9;
end;
suppose
j > len p;
then
A16: p|j = p by FINSEQ_1:58;
now
per cases;
suppose
i >= len p;
hence thesis by A16,FINSEQ_1:58;
end;
suppose
A17: i < len p;
then consider t be Nat such that
A18: len p = i + t by NAT_1:10;
consider q,r be FinSequence of NAT such that
A19: len q = i and
len r = t and
A20: p = q^r by A18,FINSEQ_2:23;
A21: len (p|i) = i by A17,FINSEQ_1:59;
then
A22: dom(p|i) = Seg i by FINSEQ_1:def 3;
A23: now
A24: Seg i = dom q by A19,FINSEQ_1:def 3;
let n be Nat;
A25: dom (p|i) c= dom p by FINSEQ_5:18;
assume
A26: n in dom(p|i);
then
A27: (p|i)/.n = p/.n by FINSEQ_4:70;
thus (p|i).n = (p|i)/.n by A26,PARTFUN1:def 6
.= p.n by A26,A27,A25,PARTFUN1:def 6
.= q.n by A20,A22,A26,A24,FINSEQ_1:def 7;
end;
A28: Sum q + Sum r >= Sum q + (0 qua Nat) by XREAL_1:6;
Sum p = Sum q + Sum r by A20,RVSUM_1:75;
hence thesis by A16,A19,A21,A23,A28,FINSEQ_2:9;
end;
end;
hence thesis;
end;
end;
::$CT
theorem Th19:
for p be complex-valued FinSequence for i be Nat st i < len p
holds Sum (p|(i+1)) = Sum (p|i) + p.(i+1)
proof
let p be complex-valued FinSequence;
let i be Nat;
assume i < len p;
then p|(i+1) = p|i ^ <*p.(i+1)*> by FINSEQ_5:83;
hence thesis by RVSUM_2:31;
end;
theorem Th20:
for p be natural-valued FinSequence
for i,j,k1,k2 be Nat st
i < len p & j < len p & 1 <= k1 & 1 <= k2 & k1 <= p.(i+1) & k2 <= p.(j+1) &
(Sum(p|i)) + k1 = (Sum (p|j)) + k2 holds i = j & k1 = k2
proof
let p be natural-valued FinSequence;
let i,j,k1,k2 be Nat;
assume that
A1: i < len p and
A2: j < len p and
A3: 1 <= k1 and
A4: 1 <= k2 and
A5: k1 <= p.(i+1) and
A6: k2 <= p.(j+1) and
A7: (Sum (p|i)) + k1 = (Sum (p|j)) + k2 and
A8: i <> j or k1 <> k2;
A9: i <> j by A7,A8,XCMPLX_1:2;
reconsider p1 = p as FinSequence of NAT by FINSEQ_1:103;
A10: Sum (p|i) + p.(i+1) >= Sum (p|i) + k1 by A5,XREAL_1:6;
A11: Sum (p|j) + p.(j+1) >= Sum (p|j) + k2 by A6,XREAL_1:6;
per cases;
suppose
i < j;
then i+1 <= j by NAT_1:13;
then Sum (p|j) >= Sum (p|(i+1)) by Th17;
then Sum (p|j) >= Sum (p1|i) + p.(i+1) by A1,Th19;
then
A12: Sum (p|j) >= Sum (p|j) + k2 by A7,A10,XXREAL_0:2;
Sum (p|j) + k2 >= Sum (p|j) by NAT_1:11;
then Sum (p|j) = Sum (p|j) + k2 by A12,XXREAL_0:1;
then k2 = 0;
hence contradiction by A4;
end;
suppose
i >= j;
then j < i by A9,XXREAL_0:1;
then j+1 <= i by NAT_1:13;
then Sum (p|i) >= Sum (p|(j+1)) by Th17;
then Sum (p|i) >= Sum (p1|j) + p.(j+1) by A2,Th19;
then
A13: Sum (p|i) >= Sum (p|i) + k1 by A7,A11,XXREAL_0:2;
Sum (p|i) + k1 >= Sum (p|i) by NAT_1:11;
then Sum (p|i) = Sum (p|i) + k1 by A13,XXREAL_0:1;
then k1 = 0;
hence contradiction by A3;
end;
end;
theorem Th21:
for D1,D2 be set for f1 be FinSequence of D1* for f2 be
FinSequence of D2* for i1,i2,j1,j2 be Element of NAT st i1 in dom f1 & i2 in
dom f2 & j1 in dom (f1.i1) & j2 in dom (f2.i2) & Card f1 = Card f2 & (Sum ((
Card f1)|(i1-'1))) + j1 = (Sum ((Card f2)|(i2-'1))) + j2
holds i1 = i2 & j1 = j2
proof
let D1,D2 be set;
let f1 be FinSequence of D1*;
let f2 be FinSequence of D2*;
let i1,i2,j1,j2 be Element of NAT;
assume that
A1: i1 in dom f1 and
A2: i2 in dom f2 and
A3: j1 in dom (f1.i1) and
A4: j2 in dom (f2.i2) and
A5: Card f1 = Card f2 & (Sum ((Card f1)|(i1-'1))) + j1 = (Sum ((Card f2)
|(i2-'1) )) + j2;
A6: j1 >= 1 & j2 >= 1 by A3,A4,FINSEQ_3:25;
A7: 1 <= i1 by A1,FINSEQ_3:25;
then
A8: i1-1 >= 0 by XREAL_1:48;
j1 <= len (f1.i1) by A3,FINSEQ_3:25;
then j1 <= (Card f1).i1 by A1,CARD_3:def 2;
then
A9: j1 <= (Card f1).(i1-'1+1) by A7,XREAL_1:235;
A10: 1 <= i2 by A2,FINSEQ_3:25;
then
A11: i2-1 >= 0 by XREAL_1:48;
dom Card f2 = dom f2 by CARD_3:def 2;
then
A12: len Card f2 = len f2 by FINSEQ_3:29;
dom Card f1 = dom f1 by CARD_3:def 2;
then
A13: len Card f1 = len f1 by FINSEQ_3:29;
i1 <= len f1 by A1,FINSEQ_3:25;
then i1 < len f1 + 1 by NAT_1:13;
then i1 - 1 < len f1 + 1 - 1 by XREAL_1:9;
then
A14: i1-'1 < len Card f1 by A13,A8,XREAL_0:def 2;
j2 <= len (f2.i2) by A4,FINSEQ_3:25;
then j2 <= (Card f2).i2 by A2,CARD_3:def 2;
then
A15: j2 <= (Card f2).(i2-'1+1) by A10,XREAL_1:235;
i2 <= len f2 by A2,FINSEQ_3:25;
then i2 < len f2 + 1 by NAT_1:13;
then i2 - 1 < len f2 + 1 - 1 by XREAL_1:9;
then i2-'1 < len Card f2 by A12,A11,XREAL_0:def 2;
then i1-'1 = i2-'1 by A5,A14,A6,A9,A15,Th20;
then i1-1 = i2-'1 by A8,XREAL_0:def 2;
then i1-1 = i2-1 by A11,XREAL_0:def 2;
hence thesis by A5,A14,A6,A9,A15,Th20;
end;
begin :: Polynomials
definition
let L be non empty ZeroStr;
mode Polynomial of L is AlgSequence of L;
end;
theorem
for L be non empty ZeroStr for p be Polynomial of L
for n be Nat holds n >= len p iff n is_at_least_length_of p
by ALGSEQ_1:8,XXREAL_0:2,ALGSEQ_1:def 3;
scheme
PolynomialLambdaF{R()->non empty addLoopStr, A()->Element of NAT, F(Element
of NAT)->Element of R()}: ex p be Polynomial of R() st len p <= A() & for n be
Element of NAT st n < A() holds p.n=F(n) proof
defpred P[Element of NAT,Element of R()] means $1<A() & $2=F($1) or $1>=A()
& $2=0.R();
A1: for x be Element of NAT ex y be Element of R() st P[x,y]
proof
let x be Element of NAT;
x<A() implies x<A() & F(x) = F(x);
hence thesis;
end;
ex f be sequence of the carrier of R() st for x be Element of NAT
holds P[x,f.x] from FUNCT_2:sch 3(A1);
then consider f be sequence of the carrier of R() such that
A2: for x be Element of NAT holds x<A() & f.x=F(x) or x>=A() & f.x=0.R();
ex n be Nat st for i be Nat st i >= n holds f.i = 0.R()
proof
take A();
let i be Nat;
i in NAT by ORDINAL1:def 12;
hence thesis by A2;
end;
then reconsider f as AlgSequence of R() by ALGSEQ_1:def 1;
take f;
now
let i be Nat;
i in NAT by ORDINAL1:def 12;
hence i>=A() implies f.i=0.R() by A2;
end;
then A() is_at_least_length_of f;
hence thesis by A2,ALGSEQ_1:def 3;
end;
registration
let L be right_zeroed non empty addLoopStr;
let p,q be Polynomial of L;
cluster p+q -> finite-Support;
coherence
proof
take s=len p + len q;
let i be Nat;
assume
A1: i >= s;
len p + len q >= len p by NAT_1:11;
then
A2: p.i = 0.L by A1,ALGSEQ_1:8,XXREAL_0:2;
A3: len p + len q >= len q by NAT_1:11;
thus (p+q).i = p.i + q.i by NORMSP_1:def 2
.= 0.L + 0.L by A1,A2,A3,ALGSEQ_1:8,XXREAL_0:2
.= 0.L by RLVECT_1:def 4;
end;
end;
theorem
for L be right_zeroed non empty addLoopStr for p,q be
Polynomial of L for n be Element of NAT holds (n is_at_least_length_of p & n
is_at_least_length_of q) implies n is_at_least_length_of p+q
proof
let L be right_zeroed non empty addLoopStr;
let p,q be Polynomial of L;
let n be Element of NAT;
assume
A1: n is_at_least_length_of p & n is_at_least_length_of q;
let i be Nat;
assume i>=n;
then
A2: p.i = 0.L & q.i = 0.L by A1;
thus (p+q).i = 0.L + 0.L by A2,NORMSP_1:def 2
.= 0.L by RLVECT_1:def 4;
end;
definition
let L be Abelian non empty addLoopStr;
let p,q be sequence of L;
redefine func p+q; :: redefines + (NORMSP_1, definition)
commutativity
proof
let p,q be sequence of L;
let n be Element of NAT;
thus (p+q).n = p.n + q.n by NORMSP_1:def 2
.= (q+p).n by NORMSP_1:def 2;
end;
end;
::$CT
theorem Th24:
for L be add-associative non empty addLoopStr for p,q,r be
sequence of L holds p+q+r = p+(q+r)
proof
let L be add-associative non empty addLoopStr;
let p,q,r be sequence of L;
now
let n be Element of NAT;
thus (p+q+r).n = (p+q).n + r.n by NORMSP_1:def 2
.= p.n + q.n + r.n by NORMSP_1:def 2
.= p.n + (q.n + r.n) by RLVECT_1:def 3
.= p.n + (q+r).n by NORMSP_1:def 2
.= (p+(q+r)).n by NORMSP_1:def 2;
end;
hence thesis;
end;
registration
let L be add-associative right_zeroed right_complementable non empty
addLoopStr;
let p be Polynomial of L;
cluster -p -> finite-Support;
coherence
proof
take s=len p;
let i be Nat;
assume
A1: i >= s;
thus (-p).i = -p.i by BHSP_1:44
.= - 0.L by A1,ALGSEQ_1:8
.= 0.L by RLVECT_1:12;
end;
end;
Lm1: for L be non empty addLoopStr for p,q be sequence of L holds p-q = p+-q
proof
let L be non empty addLoopStr;
let p,q be sequence of L;
let n be Element of NAT;
thus (p-q).n = p.n-q.n by NORMSP_1:def 3
.= p.n + (-q).n by BHSP_1:44
.= (p+-q).n by NORMSP_1:def 2;
end;
definition
let L be non empty addLoopStr;
let p,q be sequence of L;
redefine func p-q equals :: redefines - (NORMSP_1, definition)
p+-q;
compatibility by Lm1;
end;
registration
let L be add-associative right_zeroed right_complementable non empty
addLoopStr;
let p,q be Polynomial of L;
cluster p-q -> finite-Support;
coherence;
end;
theorem
for L be non empty addLoopStr for p,q be sequence of L for n be
Element of NAT holds (p-q).n = p.n - q.n by NORMSP_1:def 3;
definition
let L be non empty ZeroStr;
func 0_.(L) -> sequence of L equals
NAT --> 0.L;
coherence;
end;
registration
let L be non empty ZeroStr;
cluster 0_.(L) -> finite-Support;
coherence
proof
take 0;
let i be Nat;
assume i >= 0;
i in NAT by ORDINAL1:def 12;
hence thesis by FUNCOP_1:7;
end;
end;
theorem Th26:
for L be right_zeroed non empty addLoopStr for p be sequence
of L holds p+0_.(L) = p
proof
let L be right_zeroed non empty addLoopStr;
let p be sequence of L;
now
let n be Element of NAT;
thus (p+0_.(L)).n = p.n + (0_.(L)).n by NORMSP_1:def 2
.= p.n + 0.L by FUNCOP_1:7
.= p.n by RLVECT_1:def 4;
end;
hence thesis;
end;
theorem Th27:
for L be add-associative right_zeroed right_complementable non
empty addLoopStr for p be sequence of L holds p-p = 0_.(L)
proof
let L be add-associative right_zeroed right_complementable non empty
addLoopStr;
let p be sequence of L;
now
let n be Element of NAT;
thus (p-p).n = p.n - p.n by NORMSP_1:def 3
.= 0.L by RLVECT_1:15
.= (0_.(L)).n by FUNCOP_1:7;
end;
hence thesis;
end;
definition
let L be non empty multLoopStr_0;
func 1_.(L) -> sequence of L equals
0_.(L)+*(0,1.L);
coherence;
end;
registration
let L be non empty multLoopStr_0;
cluster 1_.(L) -> finite-Support;
coherence
proof
take 1;
let i be Nat;
A1: i in NAT by ORDINAL1:def 12;
assume i >= 1;
hence (1_.(L)).i = (0_.(L)).i by FUNCT_7:32
.= 0.L by A1,FUNCOP_1:7;
end;
end;
theorem Th28:
for L be non empty multLoopStr_0 holds (1_.(L)).0 = 1.L & for n
be Nat st n <> 0 holds (1_.(L)).n = 0.L
proof
let L be non empty multLoopStr_0;
0 in NAT;
then 0 in dom 0_.(L) by FUNCT_2:def 1;
hence (1_.(L)).0 = 1.L by FUNCT_7:31;
let n be Nat;
A1: n in NAT by ORDINAL1:def 12;
assume n <> 0;
hence (1_.(L)).n = (0_.(L)).n by FUNCT_7:32
.= 0.L by A1,FUNCOP_1:7;
end;
definition
let L be non empty doubleLoopStr;
let p,q be sequence of L;
func p*'q -> sequence of L means
:Def9:
for i be Element of NAT ex r be
FinSequence of the carrier of L st len r = i+1 & it.i = Sum r & for k be
Element of NAT st k in dom r holds r.k = p.(k-'1) * q.(i+1-'k);
existence
proof
defpred P[Element of NAT,Element of L] means ex r be FinSequence of the
carrier of L st len r = $1+1 & $2 = Sum r & for k be Element of NAT st k in dom
r holds r.k = p.(k-'1) * q.($1+1-'k);
A1: for i be Element of NAT ex v be Element of L st P[i,v]
proof
let i be Element of NAT;
deffunc F(Nat) = p.($1-'1) * q.(i+1-'$1);
consider r be FinSequence of the carrier of L such that
A2: len r = i+1 and
A3: for k be Nat st k in dom r holds r.k = F(k) from FINSEQ_2:sch 1;
take v = Sum r;
take r;
thus len r = i+1 by A2;
thus v = Sum r;
let k be Element of NAT;
assume k in dom r;
hence thesis by A3;
end;
consider f be sequence of the carrier of L such that
A4: for i be Element of NAT holds P[i,f.i] from FUNCT_2:sch 3(A1);
take f;
thus thesis by A4;
end;
uniqueness
proof
let p1,p2 be sequence of L such that
A5: for i be Element of NAT ex r be FinSequence of the carrier of L st
len r = i+1 & p1.i = Sum r & for k be Element of NAT st k in dom r holds r.k =
p.(k-'1) * q.(i+1-'k) and
A6: for i be Element of NAT ex r be FinSequence of the carrier of L st
len r = i+1 & p2.i = Sum r & for k be Element of NAT st k in dom r holds r.k =
p.(k-'1) * q.(i+1-'k);
now
let i be Element of NAT;
consider r1 be FinSequence of the carrier of L such that
A7: len r1 = i+1 and
A8: p1.i = Sum r1 and
A9: for k be Element of NAT st k in dom r1 holds r1.k = p.(k-'1) *
q.(i+1-'k) by A5;
consider r2 be FinSequence of the carrier of L such that
A10: len r2 = i+1 and
A11: p2.i = Sum r2 and
A12: for k be Element of NAT st k in dom r2 holds r2.k = p.(k-'1) *
q.(i+1-'k) by A6;
A13: dom r1 = Seg len r2 by A7,A10,FINSEQ_1:def 3
.= dom r2 by FINSEQ_1:def 3;
now
let k be Nat;
assume
A14: k in dom r1;
hence r1.k = p.(k-'1) * q.(i+1-'k) by A9
.= r2.k by A12,A13,A14;
end;
hence p1.i = p2.i by A8,A11,A13,FINSEQ_1:13;
end;
hence p1 = p2;
end;
end;
registration
let L be add-associative right_zeroed right_complementable distributive non
empty doubleLoopStr;
let p,q be Polynomial of L;
cluster p*'q -> finite-Support;
coherence
proof
take s = len p + len q;
let i be Nat;
i in NAT by ORDINAL1:def 12;
then consider r be FinSequence of the carrier of L such that
A1: len r = i+1 and
A2: (p*'q).i = Sum r and
A3: for k be Element of NAT st k in dom r holds r.k = p.(k-'1) * q.(i+
1-'k) by Def9;
assume i >= s;
then len p <= i - len q by XREAL_1:19;
then
A4: -len p >= -(i - len q) by XREAL_1:24;
now
let k be Element of NAT;
assume
A5: k in dom r;
then
A6: r.k = p.(k-'1) * q.(i+1-'k) by A3;
k <= i+1 by A1,A5,FINSEQ_3:25;
then
A7: i+1-k >= 0 by XREAL_1:48;
per cases;
suppose
k-'1 < len p;
then k-1 < len p by XREAL_0:def 2;
then -(k-1) > -len p by XREAL_1:24;
then 1-k > len q - i by A4,XXREAL_0:2;
then i+(1-k) > len q by XREAL_1:19;
then i+1-'k >= len q by A7,XREAL_0:def 2;
then q.(i+1-'k) = 0.L by ALGSEQ_1:8;
hence r.k = 0.L by A6;
end;
suppose
k-'1 >= len p;
then p.(k-'1) = 0.L by ALGSEQ_1:8;
hence r.k = 0.L by A6;
end;
end;
hence thesis by A2,Th1;
end;
end;
theorem Th29:
for L be Abelian add-associative right_zeroed
right_complementable right-distributive non empty doubleLoopStr for p,q,r be
sequence of L holds p*'(q+r) = p*'q+p*'r
proof
let L be Abelian add-associative right_zeroed right_complementable
right-distributive non empty doubleLoopStr;
let p,q,r be sequence of L;
now
let i be Element of NAT;
consider r1 be FinSequence of the carrier of L such that
A1: len r1 = i+1 and
A2: (p*'(q+r)).i = Sum r1 and
A3: for k be Element of NAT st k in dom r1 holds r1.k = p.(k-'1) * (q+
r).(i+1-'k) by Def9;
A4: dom r1 = Seg (i+1) by A1,FINSEQ_1:def 3;
consider r3 be FinSequence of the carrier of L such that
A5: len r3 = i+1 and
A6: (p*'r).i = Sum r3 and
A7: for k be Element of NAT st k in dom r3 holds r3.k = p.(k-'1) * r.
(i+1-'k) by Def9;
consider r2 be FinSequence of the carrier of L such that
A8: len r2 = i+1 and
A9: (p*'q).i = Sum r2 and
A10: for k be Element of NAT st k in dom r2 holds r2.k = p.(k-'1) * q.(
i+1-'k) by Def9;
reconsider r29=r2, r39=r3 as Element of (i+1)-tuples_on (the carrier of L)
by A8,A5,FINSEQ_2:92;
A11: len (r29 + r39) = i+1 by CARD_1:def 7;
now
let k be Nat;
assume
A12: k in dom r1;
then
A13: k in dom (r2 + r3) by A11,A4,FINSEQ_1:def 3;
k in dom r3 by A5,A4,A12,FINSEQ_1:def 3;
then
A14: r3.k = p.(k-'1) * r.(i+1-'k) by A7;
k in dom r2 by A8,A4,A12,FINSEQ_1:def 3;
then
A15: r2.k = p.(k-'1) * q.(i+1-'k) by A10;
thus r1.k = p.(k-'1) * (q+r).(i+1-'k) by A3,A12
.= p.(k-'1) * (q.(i+1-'k) +r.(i+1-'k)) by NORMSP_1:def 2
.= p.(k-'1) * q.(i+1-'k) + p.(k-'1) * r.(i+1-'k) by VECTSP_1:def 2
.= (r2 + r3).k by A13,A15,A14,FVSUM_1:17;
end;
then Sum r1 = Sum(r29 + r39) by A1,A11,FINSEQ_2:9
.= Sum r2 + Sum r3 by FVSUM_1:76;
hence (p*'(q+r)).i = (p*'q+p*'r).i by A2,A9,A6,NORMSP_1:def 2;
end;
hence thesis;
end;
theorem Th30:
for L be Abelian add-associative right_zeroed
right_complementable left-distributive non empty doubleLoopStr for p,q,r be
sequence of L holds (p+q)*'r = p*'r+q*'r
proof
let L be Abelian add-associative right_zeroed right_complementable
left-distributive non empty doubleLoopStr;
let p,q,r be sequence of L;
now
let i be Element of NAT;
consider r1 be FinSequence of the carrier of L such that
A1: len r1 = i+1 and
A2: ((p+q)*'r).i = Sum r1 and
A3: for k be Element of NAT st k in dom r1 holds r1.k = (p+q).(k-'1) *
r.(i+1-'k) by Def9;
A4: dom r1 = Seg(i+1) by A1,FINSEQ_1:def 3;
consider r3 be FinSequence of the carrier of L such that
A5: len r3 = i+1 and
A6: (q*'r).i = Sum r3 and
A7: for k be Element of NAT st k in dom r3 holds r3.k = q.(k-'1) * r.
(i+1-'k) by Def9;
consider r2 be FinSequence of the carrier of L such that
A8: len r2 = i+1 and
A9: (p*'r).i = Sum r2 and
A10: for k be Element of NAT st k in dom r2 holds r2.k = p.(k-'1) * r.(
i+1-'k) by Def9;
reconsider r29=r2, r39=r3 as Element of (i+1)-tuples_on (the carrier of L)
by A8,A5,FINSEQ_2:92;
A11: len (r29 + r39) = i+1 by CARD_1:def 7;
now
let k be Nat;
assume
A12: k in dom r1;
then
A13: k in dom (r2 + r3) by A11,A4,FINSEQ_1:def 3;
k in dom r3 by A5,A4,A12,FINSEQ_1:def 3;
then
A14: r3.k = q.(k-'1) * r.(i+1-'k) by A7;
k in dom r2 by A8,A4,A12,FINSEQ_1:def 3;
then
A15: r2.k = p.(k-'1) * r.(i+1-'k) by A10;
thus r1.k = (p+q).(k-'1) * r.(i+1-'k) by A3,A12
.= (p.(k-'1) + q.(k-'1)) * r.(i+1-'k) by NORMSP_1:def 2
.= p.(k-'1) * r.(i+1-'k) + q.(k-'1) * r.(i+1-'k) by VECTSP_1:def 3
.= (r2 + r3).k by A13,A15,A14,FVSUM_1:17;
end;
then Sum r1 = Sum(r29 + r39) by A1,A11,FINSEQ_2:9
.= Sum r2 + Sum r3 by FVSUM_1:76;
hence ((p+q)*'r).i = (p*'r+q*'r).i by A2,A9,A6,NORMSP_1:def 2;
end;
hence thesis;
end;
theorem Th31:
for L be Abelian add-associative right_zeroed
right_complementable well-unital associative distributive non empty
doubleLoopStr for p,q,r be sequence of L holds p*'q*'r = p*'(q*'r)
proof
let L be Abelian add-associative right_zeroed right_complementable
well-unital associative distributive non empty doubleLoopStr;
let p,q,r be sequence of L;
now
let i be Element of NAT;
deffunc F(Nat) = (Decomp($1-'1,2)) ^^
($1 |-> <*i+1-'$1*> qua FinSequence of 1-tuples_on NAT);
consider f2 be FinSequence of ((2+1)-tuples_on NAT)* such that
A1: len f2 = i+1 and
A2: for k be Nat st k in dom f2 holds f2.k = F(k) from FINSEQ_2:sch 1;
A3: dom f2 = Seg(i+1) by A1,FINSEQ_1:def 3;
reconsider f2 as FinSequence of (3-tuples_on NAT)*;
deffunc F(Nat) = ((i+2-'$1) |-> <*$1-'1*>) ^^ (Decomp(i+1-'$1,2));
consider g2 be FinSequence of ((1+2)-tuples_on NAT)* such that
A4: len g2 = i+1 and
A5: for k be Nat st k in dom g2 holds g2.k = F(k) from FINSEQ_2:sch 1;
A6: dom g2 = Seg(i+1) by A4,FINSEQ_1:def 3;
reconsider g2 as FinSequence of (3-tuples_on NAT)*;
consider r2 be FinSequence of the carrier of L such that
A7: len r2 = i+1 and
A8: (p*'(q*'r)).i = Sum r2 and
A9: for k be Element of NAT st k in dom r2 holds r2.k = p.(k-'1) * (q
*'r).(i+1-'k) by Def9;
A10: dom r2 = Seg(i+1) by A7,FINSEQ_1:def 3;
A11: dom Card f2 = dom f2 by CARD_3:def 2
.= Seg len g2 by A1,A4,FINSEQ_1:def 3
.= dom g2 by FINSEQ_1:def 3
.= dom Card g2 by CARD_3:def 2
.= dom Rev Card g2 by FINSEQ_5:57;
A12: now
let j be Nat;
A13: dom (j |-> <*i+1-'j*>) = Seg j by FUNCOP_1:13;
assume
A14: j in dom Card f2;
then
A15: j in Seg len Rev Card g2 by A11,FINSEQ_1:def 3;
then
A16: j >= 1 by FINSEQ_1:1;
then j-1 >= 0 by XREAL_1:48;
then
A17: i+1-(j-1) <= i+1 by XREAL_1:43;
A18: dom Card g2 = dom g2 by CARD_3:def 2;
then
A19: len Card g2 = len g2 by FINSEQ_3:29;
then
A20: j in Seg len g2 by A15,FINSEQ_5:def 3;
then
A21: f2.j = (Decomp(j-'1,2)) ^^ (j |-> <*i+1-'j*>) by A2,A3,A4;
i+1 >= j by A4,A20,FINSEQ_1:1;
then
A22: i+1-j >= 0 by XREAL_1:48;
then i+1-j+1 = i+1-'j+1 by XREAL_0:def 2;
then reconsider lj = len Card g2 - j + 1 as Element of NAT by A4,A18,
FINSEQ_3:29;
i+1-(i+1-j+1) = 0 qua Nat+(j-1);
then
A23: i+1-(i+1-j+1) >= 0 by A16,XREAL_1:48;
then
A24: i+1-'lj+1 = 0 qua Nat+(j-1)+1 by A4,A19,XREAL_0:def 2
.= j;
i+1-j+1 >= 0 qua Nat+1 by A22,XREAL_1:6;
then lj in Seg (i+1) by A4,A19,A17,FINSEQ_1:1;
then
A25: g2.lj = ((i+2-'lj) |-> <*lj-'1*>)^^(Decomp(i+1-'lj,2)) by A5,A6;
A26: i+1-'lj+1 = i+1-lj+1 by A4,A19,A23,XREAL_0:def 2
.= i+(1+1)-lj;
A27: dom ((i+2-'lj) |-> <*lj-'1*>) = Seg (i+2-'lj) by FUNCOP_1:13
.= Seg j by A24,A26,XREAL_0:def 2;
A28: dom Decomp(i+1-'lj,2) = Seg len Decomp(i+1-'lj,2) by FINSEQ_1:def 3
.= Seg j by A24,Th9;
Seg len (g2.lj) = dom (g2.lj) by FINSEQ_1:def 3
.= (Seg j) /\ (Seg j) by A25,A28,A27,PRE_POLY:def 4
.= Seg j;
then
A29: len (g2.lj) = j by FINSEQ_1:6;
A30: dom Decomp(j-'1,2) = Seg len Decomp(j-'1,2) by FINSEQ_1:def 3
.= Seg (j-'1+1) by Th9
.= Seg j by A16,XREAL_1:235;
Seg len (f2.j) = dom (f2.j) by FINSEQ_1:def 3
.= (Seg j) /\ (Seg j) by A21,A30,A13,PRE_POLY:def 4
.= Seg j;
then
A31: len (f2.j) = j by FINSEQ_1:6;
len Card g2 - j + 1 in Seg len g2 by A19,A20,FINSEQ_5:2;
then
A32: len Card g2 - j + 1 in dom g2 by FINSEQ_1:def 3;
j in dom f2 by A14,CARD_3:def 2;
hence (Card f2).j = j by A31,CARD_3:def 2
.= (Card g2).(len Card g2 - j + 1) by A32,A29,CARD_3:def 2
.= (Rev Card g2).j by A11,A14,FINSEQ_5:def 3;
end;
len Card f2 = len Rev Card g2 by A11,FINSEQ_3:29;
then
A33: Card f2 = Rev Card g2 by A12,FINSEQ_2:9;
reconsider w = Card g2 as FinSequence of NAT;
A34: Seg len FlattenSeq f2 = dom FlattenSeq f2 by FINSEQ_1:def 3;
now
let y be object;
thus y in rng FlattenSeq f2 implies y in rng FlattenSeq g2
proof
assume y in rng FlattenSeq f2;
then consider x be Nat such that
A35: x in dom FlattenSeq f2 and
A36: (FlattenSeq f2).x = y by FINSEQ_2:10;
consider i1,j1 be Nat such that
A37: i1 in dom f2 and
A38: j1 in dom (f2.i1) and
x = (Sum Card (f2|(i1-'1))) + j1 and
A39: (f2.i1).j1 = (FlattenSeq f2).x by A35,PRE_POLY:29;
A40: f2.i1 = (Decomp(i1-'1,2)) ^^ (i1 |-> <*i+1-'i1*>) by A2,A37;
then j1 in dom (Decomp(i1-'1,2)) /\ dom (i1 |-> <*i+1-'i1*>) by A38,
PRE_POLY:def 4;
then j1 in dom (i1 |-> <*i+1-'i1*>) by XBOOLE_0:def 4;
then
A41: j1 in Seg i1 by FUNCOP_1:13;
then
A42: j1 <= i1 by FINSEQ_1:1;
then
A43: i1-j1 >= 0 by XREAL_1:48;
set j2 = i1-'j1+1;
set i2 = j1;
A44: dom ((i+2-'i2) |-> <*i2-'1*>) = Seg (i+2-'i2) by FUNCOP_1:13;
A45: i1 in Seg (i+1) by A1,A37,FINSEQ_1:def 3;
then
A46: 1 <= i1 by FINSEQ_1:1;
then
A47: j1 in Seg (i1-'1+1) by A41,XREAL_1:235;
A48: i1 <= i+1 by A45,FINSEQ_1:1;
then
A49: i+1-i1 >= 0 by XREAL_1:48;
A50: i+1 >= j1 by A48,A42,XXREAL_0:2;
then
A51: i+1-j1 >=0 by XREAL_1:48;
then
A52: i+1-'i2+1 = i+1-i2+1 by XREAL_0:def 2
.= i+(1+1)-i2;
i+1-'j1 >= i1-'j1 by A48,NAT_D:42;
then i+1-'j1+1 >= i1-'j1+1 by XREAL_1:6;
then i+1-'j1+1-(i1-'j1+1) >= 0 by XREAL_1:48;
then
A53: i+1-'j1+1-'(i1-'j1+1)=i+1-'j1+1-(i1-'j1+1) by XREAL_0:def 2
.= i+1-'j1+1-(i1-j1+1) by A43,XREAL_0:def 2
.= i+1-j1+1-(1-j1+i1) by A51,XREAL_0:def 2
.= i+1-'i1 by A49,XREAL_0:def 2;
1 <= j1 by A41,FINSEQ_1:1;
then
A54: i2 in Seg (i+1) by A50,FINSEQ_1:1;
then
A55: g2.i2 = ((i+2-'i2) |-> <*i2-'1*>)^^(Decomp(i+1-'i2,2)) by A5,A6;
i1-'j1 <= i+1-'i2 by A48,NAT_D:42;
then 1 <= i1-'j1+1 & i1-'j1+1 <= i+1-'i2+1 by NAT_1:11,XREAL_1:6;
then
A56: j2 in Seg (i+1-'i2+1) by FINSEQ_1:1;
then
A57: j2 in Seg (i+2-'i2) by A52,XREAL_0:def 2;
dom Decomp(i+1-'i2,2) = Seg len Decomp(i+1-'i2,2) by FINSEQ_1:def 3
.= Seg (i+1-'i2+1) by Th9
.= Seg (i+2-'i2) by A52,XREAL_0:def 2;
then dom (g2.i2) = (Seg (i+2-'i2)) /\ (Seg (i+2-'i2)) by A55,A44,
PRE_POLY:def 4;
then
A58: j2 in dom (g2.i2) by A56,A52,XREAL_0:def 2;
then
A59: (g2.i2).j2=(((i+2-'i2) |-> <*i2-'1*>).j2)^((Decomp(i+1-'i2,2)).
j2) by A55,PRE_POLY:def 4
.= <*i2-'1*> ^ ((Decomp(i+1-'i2,2)).j2) by A57,FUNCOP_1:7
.= <*i2-'1*> ^ <*j2-'1,i+1-'i2+1-'j2*> by A56,Th14
.= <*j1-'1,i1-'j1+1-'1,i+1-'j1+1-'(i1-'j1+1)*> by FINSEQ_1:43
.= <*j1-'1,i1-'j1,i+1-'i1*> by A53,NAT_D:34;
i2 in dom g2 by A4,A54,FINSEQ_1:def 3;
then
A60: (Sum Card (g2|(i2-'1))) + j2 in dom FlattenSeq g2 & (g2.i2).j2 =
(FlattenSeq g2).((Sum Card (g2|(i2-'1))) + j2) by A58,PRE_POLY:30;
y = ((Decomp(i1-'1,2)).j1) ^ ((i1 |-> <*i+1-'i1*>).j1) by A36,A38,A39
,A40,PRE_POLY:def 4
.= ((Decomp(i1-'1,2)).j1) ^ <*i+1-'i1*> by A41,FUNCOP_1:7
.= <*j1-'1,i1-'1+1-'j1*> ^ <*i+1-'i1*> by A47,Th14
.= <*j1-'1,i1-'j1*> ^ <*i+1-'i1*> by A46,XREAL_1:235
.= <*j1-'1,i1-'j1,i+1-'i1*> by FINSEQ_1:43;
hence thesis by A59,A60,FUNCT_1:def 3;
end;
assume y in rng FlattenSeq g2;
then consider x be Nat such that
A61: x in dom FlattenSeq g2 and
A62: (FlattenSeq g2).x = y by FINSEQ_2:10;
consider i1,j1 be Nat such that
A63: i1 in dom g2 and
A64: j1 in dom (g2.i1) and
x = (Sum Card (g2|(i1-'1))) + j1 and
A65: (g2.i1).j1 = (FlattenSeq g2).x by A61,PRE_POLY:29;
A66: g2.i1 = ((i+2-'i1) |-> <*i1-'1*>)^^(Decomp(i+1-'i1,2)) by A5,A63;
then j1 in dom ((i+2-'i1) |-> <*i1-'1*>) /\ dom (Decomp(i+1-'i1,2)) by
A64,PRE_POLY:def 4;
then j1 in dom ((i+2-'i1) |-> <*i1-'1*>) by XBOOLE_0:def 4;
then
A67: j1 in Seg (i+2-'i1) by FUNCOP_1:13;
then j1 >= 1 by FINSEQ_1:1;
then
A68: j1-1 >= 0 by XREAL_1:48;
A69: i1 in Seg (i+1) by A4,A63,FINSEQ_1:def 3;
then i1 <= i+1 by FINSEQ_1:1;
then
A70: i+1-i1 >= 0 by XREAL_1:48;
then i+1-'i1+1 = i+1-i1+1 by XREAL_0:def 2
.= i+(1+1)-i1;
then
A71: j1 in Seg (i+1-'i1+1) by A67,XREAL_0:def 2;
then
A72: j1 <= i+1-'i1+1 by FINSEQ_1:1;
then
A73: i+1-'i1+1-j1 >= 0 by XREAL_1:48;
j1 <= i+1-i1+1 by A70,A72,XREAL_0:def 2;
then j1-1 <= i+1-i1 by XREAL_1:20;
then
A74: j1-1+i1 <= i+1 by XREAL_1:19;
then
A75: j1-'1+i1 <= i+1 by A68,XREAL_0:def 2;
i+1-(j1-1+i1) >= 0 by A74,XREAL_1:48;
then i+1-(j1-'1+i1) >= 0 by A68,XREAL_0:def 2;
then
A76: i+1-'(j1-'1+i1) = i+1-(j1-'1+i1) by XREAL_0:def 2
.= i+1-(j1-1+i1) by A68,XREAL_0:def 2
.= i+1-i1+1-j1
.= i+1-'i1+1-j1 by A70,XREAL_0:def 2
.= i+1-'i1+1-'j1 by A73,XREAL_0:def 2;
A77: y = (((i+2-'i1) |-> <*i1-'1*>).j1) ^ (Decomp(i+1-'i1,2).j1) by A62,A64
,A65,A66,PRE_POLY:def 4
.= <*i1-'1*> ^ (Decomp(i+1-'i1,2).j1) by A67,FUNCOP_1:7
.= <*i1-'1*> ^ <*j1-'1,i+1-'i1+1-'j1*> by A71,Th14
.= <*i1-'1,j1-'1,i+1-'i1+1-'j1*> by FINSEQ_1:43;
set j2 = i1;
set i2 = j1-'1+i1;
A78: j1-'1+i1 >= i1 by NAT_1:11;
A79: dom (i2 |-> <*i+1-'i2*>) = Seg i2 by FUNCOP_1:13;
A80: 1 <= i1 by A69,FINSEQ_1:1;
then
A81: j2 in Seg i2 by A78,FINSEQ_1:1;
then
A82: j2 in Seg (i2-'1+1) by A80,A78,XREAL_1:235,XXREAL_0:2;
j1-'1+i1 >= 1 by A80,A78,XXREAL_0:2;
then
A83: i2 in Seg (i+1) by A75,FINSEQ_1:1;
then
A84: f2.i2 = (Decomp(i2-'1,2)) ^^ (i2 |-> <*i+1-'i2*>) by A2,A3;
dom Decomp(i2-'1,2) = Seg len Decomp(i2-'1,2) by FINSEQ_1:def 3
.= Seg (i2-'1+1) by Th9
.= Seg i2 by A80,A78,XREAL_1:235,XXREAL_0:2;
then dom (f2.i2) = (Seg i2) /\ (Seg i2) by A84,A79,PRE_POLY:def 4;
then
A85: j2 in dom (f2.i2) by A80,A78,FINSEQ_1:1;
i2 in dom f2 by A1,A83,FINSEQ_1:def 3;
then
A86: (Sum Card (f2|(i2-'1))) + j2 in dom FlattenSeq f2 & (f2.i2).j2 = (
FlattenSeq f2).((Sum Card (f2|(i2-'1))) + j2) by A85,PRE_POLY:30;
(f2.i2).j2 = (Decomp(i2-'1,2).j2) ^ ((i2 |-> <*i+1-'i2*>).j2) by A84,A85,
PRE_POLY:def 4
.= (Decomp(i2-'1,2).j2) ^ <*i+1-'i2*> by A81,FUNCOP_1:7
.= <*j2-'1,i2-'1+1-'j2*> ^ <*i+1-'i2*> by A82,Th14
.= <*j2-'1,i2-'1+1-'j2,i+1-'i2*> by FINSEQ_1:43
.= <*i1-'1,j1-'1+i1-'i1,i+1-'(j1-'1+i1)*> by A80,A78,XREAL_1:235
,XXREAL_0:2
.= <*i1-'1,j1-'1,i+1-'i1+1-'j1*> by A76,NAT_D:34;
hence y in rng FlattenSeq f2 by A77,A86,FUNCT_1:def 3;
end;
then
A87: rng FlattenSeq f2 = rng FlattenSeq g2 by TARSKI:2;
now
A88: i+1+1 >= i+1 by NAT_1:11;
let x,y be object;
assume that
A89: x in dom FlattenSeq g2 and
A90: y in dom FlattenSeq g2 and
A91: (FlattenSeq g2).x = (FlattenSeq g2).y;
consider i1,j1 be Nat such that
A92: i1 in dom g2 and
A93: j1 in dom (g2.i1) and
A94: x = (Sum Card (g2|(i1-'1))) + j1 and
A95: (g2.i1).j1 = (FlattenSeq g2).x by A89,PRE_POLY:29;
A96: g2.i1 = ((i+2-'i1) |-> <*i1-'1*>)^^(Decomp(i+1-'i1,2)) by A5,A92;
i1 in Seg (i+1) by A4,A92,FINSEQ_1:def 3;
then
A97: i1 <= i+1 by FINSEQ_1:1;
then i+1+1 >= i1 by A88,XXREAL_0:2;
then
A98: i+2-i1 >= 0 by XREAL_1:48;
i+1-i1 >= 0 by A97,XREAL_1:48;
then
A99: i+1-'i1+1 = i+1-i1+1 by XREAL_0:def 2
.= i+2-'i1 by A98,XREAL_0:def 2;
A100: dom ((i+2-'i1) |-> <*i1-'1*>) = Seg (i+2-'i1) by FUNCOP_1:13;
dom Decomp(i+1-'i1,2) = Seg len Decomp(i+1-'i1,2) by FINSEQ_1:def 3
.= Seg (i+2-'i1) by A99,Th9;
then
A101: dom
(g2.i1) = (Seg (i+2-'i1)) /\ (Seg (i+2-'i1)) by A96,A100,PRE_POLY:def 4
.= Seg (i+2-'i1);
j1 in Seg len(g2.i1) by A93,FINSEQ_1:def 3;
then
A102: j1 >= 1 by FINSEQ_1:1;
consider i2,j2 be Nat such that
A103: i2 in dom g2 and
A104: j2 in dom (g2.i2) and
A105: y = (Sum Card (g2|(i2-'1))) + j2 and
A106: (g2.i2).j2 = (FlattenSeq g2).y by A90,PRE_POLY:29;
A107: g2.i2 = ((i+2-'i2) |-> <*i2-'1*>)^^(Decomp(i+1-'i2,2)) by A5,A103;
i2 in Seg (i+1) by A4,A103,FINSEQ_1:def 3;
then
A108: i2 <= i+1 by FINSEQ_1:1;
then i+1+1 >= i2 by A88,XXREAL_0:2;
then
A109: i+2-i2 >= 0 by XREAL_1:48;
i+1-i2 >= 0 by A108,XREAL_1:48;
then
A110: i+1-'i2+1 = i+1-i2+1 by XREAL_0:def 2
.= i+2-'i2 by A109,XREAL_0:def 2;
A111: dom ((i+2-'i2) |-> <*i2-'1*>) = Seg (i+2-'i2) by FUNCOP_1:13;
dom Decomp(i+1-'i2,2) = Seg len Decomp(i+1-'i2,2) by FINSEQ_1:def 3
.= Seg (i+2-'i2) by A110,Th9;
then
A112: dom
(g2.i2) = (Seg (i+2-'i2)) /\ (Seg (i+2-'i2)) by A107,A111,PRE_POLY:def 4
.= Seg (i+2-'i2);
A113: (g2.i2).j2=(((i+2-'i2) |-> <*i2-'1*>).j2)^((Decomp(i+1-'i2,2)).j2)
by A104,A107,PRE_POLY:def 4
.= <*i2-'1*> ^ ((Decomp(i+1-'i2,2)).j2) by A104,A112,FUNCOP_1:7
.= <*i2-'1*> ^ <*j2-'1,i+1-'i2+1-'j2*> by A104,A110,A112,Th14
.= <*i2-'1,j2-'1,i+1-'i2+1-'j2*> by FINSEQ_1:43;
j2 in Seg len(g2.i2) by A104,FINSEQ_1:def 3;
then
A114: j2 >= 1 by FINSEQ_1:1;
(g2.i1).j1=(((i+2-'i1) |-> <*i1-'1*>).j1)^((Decomp(i+1-'i1,2)).j1)
by A93,A96,PRE_POLY:def 4
.= <*i1-'1*> ^ ((Decomp(i+1-'i1,2)).j1) by A93,A101,FUNCOP_1:7
.= <*i1-'1*> ^ <*j1-'1,i+1-'i1+1-'j1*> by A93,A99,A101,Th14
.= <*i1-'1,j1-'1,i+1-'i1+1-'j1*> by FINSEQ_1:43;
then i1-'1 = i2-'1 & j1-'1 = j2-'1 by A91,A95,A106,A113,FINSEQ_1:78;
hence x = y by A94,A105,A102,A114,XREAL_1:234;
end;
then
A115: FlattenSeq g2 is one-to-one by FUNCT_1:def 4;
len FlattenSeq f2 = Sum Card f2 by PRE_POLY:27
.= Sum w by A33,Th3
.= len FlattenSeq g2 by PRE_POLY:27;
then FlattenSeq f2 is one-to-one by A87,A115,FINSEQ_4:61;
then FlattenSeq f2,FlattenSeq g2 are_fiberwise_equipotent by A87,A115,
RFINSEQ:26;
then consider P be Permutation of dom (FlattenSeq g2) such that
A117: FlattenSeq f2 = (FlattenSeq g2)*P by RFINSEQ:4;
A118: dom Card g2 = dom g2 by CARD_3:def 2;
then
A119: len Card g2 = len g2 by FINSEQ_3:29;
consider r1 be FinSequence of the carrier of L such that
A120: len r1 = i+1 and
A121: (p*'q*'r).i = Sum r1 and
A122: for k be Element of NAT st k in dom r1 holds r1.k = (p*'q).(k-'1)
* r.(i+1-'k) by Def9;
A123: dom r1 = Seg(i+1) by A120,FINSEQ_1:def 3;
deffunc F(Nat) = prodTuples(p,q,r,f2/.$1
qua Element of (3-tuples_on NAT)*);
consider f1 be FinSequence of (the carrier of L)* such that
A124: len f1 = len f2 and
A125: for k be Nat st k in dom f1 holds f1.k = F(k) from FINSEQ_2:sch 1;
A126: dom f1 = Seg len f2 by A124,FINSEQ_1:def 3;
A127: now
let j be Nat;
A128: dom (j |-> <*i+1-'j*>) = Seg j by FUNCOP_1:13;
consider r3 be FinSequence of the carrier of L such that
A129: len r3 = j-'1+1 and
A130: (p*'q).(j-'1) = Sum r3 and
A131: for k be Element of NAT st k in dom r3 holds r3.k = p.(k-'1) *
q.(j-'1+1-'k) by Def9;
assume
A132: j in dom r1;
then
A133: 1 <= j by A123,FINSEQ_1:1;
then
A134: len r3 = j by A129,XREAL_1:235;
len Decomp(j-'1,2) = j-'1+1 by Th9
.= j by A133,XREAL_1:235;
then
A135: dom Decomp(j-'1,2) = Seg j by FINSEQ_1:def 3;
A136: dom r1 = dom f1 by A120,A1,A124,FINSEQ_3:29;
then
A137: f1/.j = f1.j by A132,PARTFUN1:def 6
.= prodTuples(p,q,r,f2/.j qua Element of (3-tuples_on NAT)*)
by A1,A125,A126,A123,A132;
dom f1 = dom f2 by A124,FINSEQ_3:29;
then
A138: f2/.j = f2.j by A132,A136,PARTFUN1:def 6
.= (Decomp(j-'1,2)) ^^ (j |-> <*i+1-'j*>) by A2,A3,A123,A132;
then
A139: dom (f2/.j) = (dom (Decomp(j-'1,2))) /\ dom (j |-> <*i+1-'j*>) by
PRE_POLY:def 4
.= Seg j by A135,A128;
A140: len prodTuples(p,q,r,f2/.j qua Element of (3-tuples_on NAT)*)
= len (f2/.j qua Element of (3-tuples_on NAT)*) by Def5
.= j by A132,A139,FINSEQ_1:def 3;
then
A141: dom prodTuples(p,q,r,f2/.j qua Element of (3-tuples_on NAT)*)
= Seg j by FINSEQ_1:def 3;
A142: dom (r3 * (r.(i+1-'j))) = dom r3 by POLYNOM1:def 2;
A143: now
let k be Nat;
assume
A144: k in dom prodTuples(p,q,r,f2/.j qua Element of (3-tuples_on NAT)*);
then
A145: (f2/.j qua Element of (3-tuples_on NAT)*)/.k
= (f2/.j).k by A139,A141,PARTFUN1:def 6
.= (Decomp(j-'1,2)).k ^ (j |-> <*i+1-'j*>).k by A138,A139,A141,A144,
PRE_POLY:def 4
.= <*k-'1,j-'1+1-'k*> ^ (j |-> <*i+1-'j*>).k by A129,A134,A141,A144
,Th14
.= <*k-'1,j-'1+1-'k*> ^ <*i+1-'j*> by A141,A144,FUNCOP_1:7
.= <*k-'1,j-'1+1-'k,i+1-'j*> by FINSEQ_1:43;
1 in Seg 3 by ENUMSET1:def 1,FINSEQ_3:1;
then 1 in Seg len
((f2/.j qua Element of (3-tuples_on NAT)*)/.k
qua Element of 3-tuples_on NAT)
by A145,FINSEQ_1:45;
then 1 in dom ((f2/.j qua Element of (3-tuples_on NAT)*)/.k)
by FINSEQ_1:def 3;
then
A146: ((f2/.j qua Element of (3-tuples_on NAT)*)/.k
qua Element of 3-tuples_on NAT)/.1
= ((f2/.j qua Element of (3-tuples_on NAT)*)/.k).1 by PARTFUN1:def 6
.= k-'1 by A145;
A147: k in dom r3 by A134,A141,A144,FINSEQ_1:def 3;
then
A148: r3/.k = r3.k by PARTFUN1:def 6
.= p.(k-'1) * q.(j-'1+1-'k) by A131,A147;
3 in Seg 3 by ENUMSET1:def 1,FINSEQ_3:1;
then 3 in Seg len ((f2/.j qua Element of (3-tuples_on NAT)*)/.k
qua Element of 3-tuples_on NAT)
by A145,FINSEQ_1:45;
then 3 in dom ((f2/.j qua Element of (3-tuples_on NAT)*)/.k)
by FINSEQ_1:def 3;
then
A149: ((f2/.j qua Element of (3-tuples_on NAT)*)/.k
qua Element of 3-tuples_on NAT)/.3
= ((f2/.j qua Element of (3-tuples_on NAT)*)/.k).3 by PARTFUN1:def 6
.= i+1-'j by A145;
2 in Seg 3 by ENUMSET1:def 1,FINSEQ_3:1;
then 2 in Seg len (((f2/.j qua Element of (3-tuples_on NAT)*)/.k)
qua Element of 3-tuples_on NAT)
by A145,FINSEQ_1:45;
then 2 in dom ((f2/.j qua Element of (3-tuples_on NAT)*)/.k)
by FINSEQ_1:def 3;
then
A150: ((f2/.j qua Element of (3-tuples_on NAT)*)/.k
qua Element of 3-tuples_on NAT)/.2
= ((f2/.j qua Element of (3-tuples_on NAT)*)/.k
qua Element of 3-tuples_on NAT).2 by PARTFUN1:def 6
.= j-'1+1-'k by A145;
thus prodTuples(p,q,r,f2/.j qua Element of (3-tuples_on NAT)*).k
= (p.(((f2/.j qua Element of (3-tuples_on NAT)*)/.k
qua Element of 3-tuples_on NAT)/.1))*
(q.(((f2/.j qua Element of (3-tuples_on NAT)*)/.
k qua Element of 3-tuples_on NAT)/.2))*
(r.(((f2/.j qua Element of (3-tuples_on NAT)*)/.k
qua Element of 3-tuples_on NAT)/.3))
by A139,A141,A144,Def5
.= (r3*(r.(i+1-'j)))/.k by A147,A148,A146,A150,A149,POLYNOM1:def 2
.= (r3 * (r.(i+1-'j))).k by A142,A147,PARTFUN1:def 6;
end;
len f1 = len (Sum f1) by MATRLIN:def 6;
then
A151: dom f1 = dom (Sum f1) by FINSEQ_3:29;
len (r3 * (r.(i+1-'j))) = len r3 by A142,FINSEQ_3:29;
then
A152: prodTuples(p,q,r,f2/.j qua Element of (3-tuples_on NAT)*)
= r3 * (r.(i+1-'j)) by A140,A134,A143,FINSEQ_2:9;
(p*'q).(j-'1) * r.(i+1-'j) = Sum (r3 * (r.(i+1-'j))) by A130,POLYNOM1:13;
hence r1.j = Sum (r3 * (r.(i+1-'j))) by A122,A132
.= (Sum f1)/.j by A132,A151,A136,A137,A152,MATRLIN:def 6
.= (Sum f1).j by A132,A151,A136,PARTFUN1:def 6;
end;
deffunc F(Nat)
= prodTuples(p,q,r,g2/.$1 qua Element of (3-tuples_on NAT)*);
consider g1 be FinSequence of (the carrier of L)* such that
A153: len g1 = len g2 and
A154: for k be Nat st k in dom g1 holds g1.k = F(k) from FINSEQ_2:sch 1;
A155: dom g1 = Seg len g2 by A153,FINSEQ_1:def 3;
A156: now
let j be Nat;
A157: dom ((i+2-'j) |-> <*j-'1*>) = Seg (i+2-'j) by FUNCOP_1:13;
consider r3 be FinSequence of the carrier of L such that
A158: len r3 = i+1-'j+1 and
A159: (q*'r).(i+1-'j) = Sum r3 and
A160: for k be Element of NAT st k in dom r3 holds r3.k = q.(k-'1) *
r.(i+1-'j+1-'k) by Def9;
assume
A161: j in dom r2;
then
A162: j <= i+1 by A10,FINSEQ_1:1;
i+1+1 >= i+1 by NAT_1:11;
then i+1+1 >= j by A162,XXREAL_0:2;
then
A163: i+2-j >= 0 by XREAL_1:48;
i+1-j >= 0 by A162,XREAL_1:48;
then
A164: i+1-'j+1 =i+1-j+1 by XREAL_0:def 2
.= i+2-'j by A163,XREAL_0:def 2;
then len Decomp(i+1-'j,2) = i+2-'j by Th9;
then
A165: dom Decomp(i+1-'j,2) = Seg (i+2-'j) by FINSEQ_1:def 3;
A166: dom r2 = dom g1 by A7,A4,A153,FINSEQ_3:29;
then
A167: g1/.j = g1.j by A161,PARTFUN1:def 6
.= prodTuples(p,q,r,g2/.j qua Element of (3-tuples_on NAT)*)
by A4,A154,A155,A10,A161;
dom g1 = dom g2 by A153,FINSEQ_3:29;
then
A168: g2/.j = g2.j by A161,A166,PARTFUN1:def 6
.= ((i+2-'j) |-> <*j-'1*>) ^^ (Decomp(i+1-'j,2)) by A5,A6,A10,A161;
then
A169: dom (g2/.j) = dom ((i+2-'j) |-> <*j-'1*>) /\ dom (Decomp(i+1-'j,2))
by PRE_POLY:def 4
.= Seg (i+2-'j) by A165,A157;
A170: len prodTuples(p,q,r,g2/.j qua Element of (3-tuples_on NAT)*)
= len (g2/.j qua Element of (3-tuples_on NAT)*) by Def5
.= i+2-'j by A169,FINSEQ_1:def 3;
then
A171: dom prodTuples(p,q,r,g2/.j qua Element of (3-tuples_on NAT)*)
= Seg (i+2-'j) by FINSEQ_1:def 3;
A172: dom ((p.(j-'1)) * r3) = dom r3 by POLYNOM1:def 1;
A173: now
let k be Nat;
assume
A174: k in dom prodTuples(p,q,r,g2/.j qua Element of (3-tuples_on NAT)*);
then
A175: (g2/.j qua Element of (3-tuples_on NAT)*)/.k = (g2/.j).k
by A169,A171,PARTFUN1:def 6
.= ((i+2-'j) |-> <*j-'1*>).k ^ (Decomp(i+1-'j,2)).k by A168,A169,A171
,A174,PRE_POLY:def 4
.= ((i+2-'j) |-> <*j-'1*>).k^<*k-'1,i+1-'j+1-'k*> by A164,A171,A174
,Th14
.= <*j-'1*> ^ <*k-'1,i+1-'j+1-'k*> by A171,A174,FUNCOP_1:7
.= <*j-'1,k-'1,i+1-'j+1-'k*> by FINSEQ_1:43;
1 in Seg 3 by ENUMSET1:def 1,FINSEQ_3:1;
then 1 in Seg len ((g2/.j qua Element of (3-tuples_on NAT)*)/.k
qua Element of 3-tuples_on NAT)
by A175,FINSEQ_1:45;
then 1 in dom ((g2/.j qua Element of (3-tuples_on NAT)*)/.k)
by FINSEQ_1:def 3;
then
A176: ((g2/.j qua Element of (3-tuples_on NAT)*)/.k
qua Element of 3-tuples_on NAT)/.1
= ((g2/.j qua Element of (3-tuples_on NAT)*)/.k).1
by PARTFUN1:def 6
.= j-'1 by A175;
A177: k in dom r3 by A158,A164,A171,A174,FINSEQ_1:def 3;
then
A178: r3/.k = r3.k by PARTFUN1:def 6
.= q.(k-'1) * r.(i+1-'j+1-'k) by A160,A177;
3 in Seg 3 by ENUMSET1:def 1,FINSEQ_3:1;
then 3 in Seg len ( (g2/.j qua Element of (3-tuples_on NAT)*)/.k
qua Element of 3-tuples_on NAT)
by A175,FINSEQ_1:45;
then 3 in dom ((g2/.j qua Element of (3-tuples_on NAT)*)/.k)
by FINSEQ_1:def 3;
then
A179: ((g2/.j qua Element of (3-tuples_on NAT)*)/.k
qua Element of 3-tuples_on NAT)/.3
= ((g2/.j qua Element of (3-tuples_on NAT)*)/.k).3 by PARTFUN1:def 6
.= i+1-'j+1-'k by A175;
2 in Seg 3 by ENUMSET1:def 1,FINSEQ_3:1;
then 2 in Seg len ((g2/.j qua Element of (3-tuples_on NAT)*)/.k
qua Element of 3-tuples_on NAT)
by A175,FINSEQ_1:45;
then 2 in dom ((g2/.j qua Element of (3-tuples_on NAT)*)/.k)
by FINSEQ_1:def 3;
then
A180: ((g2/.j qua Element of (3-tuples_on NAT)*)/.k
qua Element of 3-tuples_on NAT)/.2
= ((g2/.j qua Element of (3-tuples_on NAT)*)/.k).2 by PARTFUN1:def 6
.= k-'1 by A175;
thus prodTuples(p,q,r,g2/.j qua Element of (3-tuples_on NAT)*).k
= (p.(((g2/.j qua Element of (3-tuples_on NAT)*)/.k
qua Element of 3-tuples_on NAT)/.1))*
(q.(((g2/.j qua Element of (3-tuples_on NAT)*)/.
k qua Element of 3-tuples_on NAT)/.2))
*(r.(((g2/.j qua Element of (3-tuples_on NAT)*)/.k
qua Element of 3-tuples_on NAT)/.3))
by A169,A171,A174,Def5
.= (p.(((g2/.j qua Element of (3-tuples_on NAT)*)/.k
qua Element of 3-tuples_on NAT)/.1))*
((q.(((g2/.j qua Element of (3-tuples_on NAT)*)/.k
qua Element of 3-tuples_on NAT)/.2))*
(r.(((g2/.j qua Element of (3-tuples_on NAT)*)/.k
qua Element of 3-tuples_on NAT)
/.3))) by GROUP_1:def 3
.= ((p.(j-'1)) * r3)/.k by A177,A178,A176,A180,A179,POLYNOM1:def 1
.= ((p.(j-'1)) * r3).k by A172,A177,PARTFUN1:def 6;
end;
len g1 = len (Sum g1) by MATRLIN:def 6;
then
A181: dom g1 = dom (Sum g1) by FINSEQ_3:29;
len ((p.(j-'1)) * r3) = len r3 by A172,FINSEQ_3:29;
then
A182: prodTuples(p,q,r,g2/.j qua Element of (3-tuples_on NAT)*)
= (p.(j-'1)) * r3 by A158,A164,A170,A173,FINSEQ_2:9;
p.(j-'1) * (q*'r).(i+1-'j) = Sum (p.(j-'1) * r3) by A159,POLYNOM1:12;
hence r2.j = Sum (p.(j-'1) * r3) by A9,A161
.= (Sum g1)/.j by A161,A181,A166,A167,A182,MATRLIN:def 6
.= (Sum g1).j by A161,A181,A166,PARTFUN1:def 6;
end;
A183: dom Card g2 = Seg(i+1) by A4,A118,FINSEQ_1:def 3;
A184: now
let j be Nat;
assume
A185: j in dom Card g2;
then
A186: j in dom g1 by A4,A153,A183,FINSEQ_1:def 3;
g1.j = prodTuples(p,q,r,g2/.j qua Element of (3-tuples_on NAT)*)
by A4,A154,A155,A183,A185;
then
A187: len (g1.j) = len (g2/.j) by Def5
.= len (g2.j) by A118,A185,PARTFUN1:def 6;
thus (Card g2).j = len (g2.j) by A118,A185,CARD_3:def 2
.= (Card g1).j by A186,A187,CARD_3:def 2;
end;
A188: dom Card g1 = dom g1 by CARD_3:def 2;
then len Card g1 = len g1 by FINSEQ_3:29;
then
A189: Card g2 = Card g1 by A153,A119,A184,FINSEQ_2:9;
then
A190: len (FlattenSeq g2) = len (FlattenSeq g1) by PRE_POLY:28;
then
A191: dom (FlattenSeq g2) = dom (FlattenSeq g1) by FINSEQ_3:29;
then reconsider P as Permutation of dom (FlattenSeq g1);
A192: dom FlattenSeq g1 = Seg len FlattenSeq g1 by FINSEQ_1:def 3;
A193: now
let j be Nat;
assume
A194: j in dom FlattenSeq g1;
then consider i1,j1 be Nat such that
A195: i1 in dom g1 and
A196: j1 in dom (g1.i1) and
A197: j = (Sum Card (g1|(i1-'1))) + j1 and
A198: (g1.i1).j1 = (FlattenSeq g1).j by PRE_POLY:29;
A199: j in dom FlattenSeq g2 by A190,A192,A194,FINSEQ_1:def 3;
then consider i2,j2 be Nat such that
A200: i2 in dom g2 & j2 in dom (g2.i2) and
A201: j = (Sum Card (g2|(i2-'1))) + j2 and
A202: (g2.i2).j2 = (FlattenSeq g2).j by PRE_POLY:29;
(Sum ((Card g1)|(i1-'1))) + j1 = (Sum Card (g1|(i1-'1))) + j1 by Th16
.= (Sum ((Card g2)|(i2-'1))) + j2 by A197,A201,Th16;
then
A203: i1 = i2 & j1 = j2 by A189,A195,A196,A200,Th21;
i1 in Seg len g2 by A153,A195,FINSEQ_1:def 3;
then
A204: i1 in dom g2 by FINSEQ_1:def 3;
A205: g1.i1 = prodTuples(p,q,r,g2/.i1 qua Element of (3-tuples_on NAT)*)
by A154,A195;
then len (g1.i1) = len (g2/.i1) by Def5
.= len (g2.i1) by A188,A118,A189,A195,PARTFUN1:def 6;
then j1 in Seg len (g2.i1) by A196,FINSEQ_1:def 3;
then
A206: j1 in Seg len (g2/.i1) by A204,PARTFUN1:def 6;
then j1 in dom (g2/.i1) by FINSEQ_1:def 3;
then
A207: ((g2/.i1 qua Element of (3-tuples_on NAT)*)/.j1)
= (g2/.i1 qua Element of (3-tuples_on NAT)*).j1 by PARTFUN1:def 6
.= (g2.i1).j1 by A204,PARTFUN1:def 6
.= (FlattenSeq g2)/.j by A199,A202,A203,PARTFUN1:def 6;
Seg len (g2/.i1) = dom (g2/.i1) by FINSEQ_1:def 3;
hence
(FlattenSeq g1).j
= (p.(((g2/.i1 qua Element of (3-tuples_on NAT)*)/.j1
qua Element of 3-tuples_on NAT)/.1))*
(q.(((g2/.i1 qua Element of (3-tuples_on NAT)*)/.j1
qua Element of 3-tuples_on NAT)/.2)
)*(r.(( (g2/.i1 qua Element of (3-tuples_on NAT)*)/.j1
qua Element of 3-tuples_on NAT)/.3))
by A198,A205,A206,Def5
.= (prodTuples(p,q,r,FlattenSeq g2)).j by A191,A194,A207,Def5;
end;
A208: dom Card f2 = dom f2 by CARD_3:def 2;
then
A209: len Card f2 = len f2 by FINSEQ_3:29;
A210: dom Card f2 = Seg(i+1) by A1,A208,FINSEQ_1:def 3;
A211: now
let j be Nat;
assume
A212: j in dom Card f2;
then
A213: j in dom f1 by A1,A124,A210,FINSEQ_1:def 3;
f1.j = prodTuples(p,q,r,f2/.j qua Element of (3-tuples_on NAT)*)
by A1,A125,A126,A210,A212;
then
A214: len (f1.j) = len (f2/.j) by Def5
.= len (f2.j) by A208,A212,PARTFUN1:def 6;
thus (Card f2).j = len (f2.j) by A208,A212,CARD_3:def 2
.= (Card f1).j by A213,A214,CARD_3:def 2;
end;
A215: dom Card f1 = dom f1 by CARD_3:def 2;
then len Card f1 = len f1 by FINSEQ_3:29;
then
A216: Card f2 = Card f1 by A124,A209,A211,FINSEQ_2:9;
then
A217: len FlattenSeq f1 = len FlattenSeq f2 by PRE_POLY:28;
A218: Seg len FlattenSeq f1 = dom FlattenSeq f1 by FINSEQ_1:def 3;
A219: now
let j be Nat;
assume
A220: j in dom FlattenSeq f1;
then consider i1,j1 be Nat such that
A221: i1 in dom f1 and
A222: j1 in dom (f1.i1) and
A223: j = (Sum Card (f1|(i1-'1))) + j1 and
A224: (f1.i1).j1 = (FlattenSeq f1).j by PRE_POLY:29;
A225: j in dom FlattenSeq f2 by A217,A34,A220,FINSEQ_1:def 3;
then consider i2,j2 be Nat such that
A226: i2 in dom f2 & j2 in dom (f2.i2) and
A227: j = (Sum Card (f2|(i2-'1))) + j2 and
A228: (f2.i2).j2 = (FlattenSeq f2).j by PRE_POLY:29;
(Sum ((Card f1)|(i1-'1))) + j1 = (Sum Card (f1|(i1-'1))) + j1 by Th16
.= (Sum ((Card f2)|(i2-'1))) + j2 by A223,A227,Th16;
then
A229: i1 = i2 & j1 = j2 by A216,A221,A222,A226,Th21;
i1 in Seg len f2 by A124,A221,FINSEQ_1:def 3;
then
A230: i1 in dom f2 by FINSEQ_1:def 3;
A231: f1.i1 = prodTuples(p,q,r,f2/.i1 qua Element of (3-tuples_on NAT)*)
by A125,A221;
then len (f1.i1) = len (f2/.i1) by Def5
.= len (f2.i1) by A215,A208,A216,A221,PARTFUN1:def 6;
then j1 in Seg len (f2.i1) by A222,FINSEQ_1:def 3;
then
A232: j1 in Seg len (f2/.i1) by A230,PARTFUN1:def 6;
then j1 in dom (f2/.i1) by FINSEQ_1:def 3;
then
A233: (f2/.i1 qua Element of (3-tuples_on NAT)*)/.j1
= (f2/.i1 qua Element of (3-tuples_on NAT)*).j1 by PARTFUN1:def 6
.= (f2.i1).j1 by A230,PARTFUN1:def 6
.= (FlattenSeq f2)/.j by A225,A228,A229,PARTFUN1:def 6;
Seg len (f2/.i1) = dom (f2/.i1) by FINSEQ_1:def 3;
hence
(FlattenSeq f1).j =
(p.(((f2/.i1 qua Element of (3-tuples_on NAT)*)/.j1
qua Element of 3-tuples_on NAT)/.1))*
(q.(((f2/.i1 qua Element of (3-tuples_on NAT)*)/.j1
qua Element of 3-tuples_on NAT)/.2)
)*(r.(((f2/.i1 qua Element of (3-tuples_on NAT)*)/.j1
qua Element of 3-tuples_on NAT)/.3))
by A224,A231,A232,Def5
.= (p.(((FlattenSeq f2)/.j)/.1))* (q.(((FlattenSeq f2)/.j)/.2))*(r.(
((FlattenSeq f2)/.j)/.3)) by A233
.= (prodTuples(p,q,r,FlattenSeq f2)).j by A217,A34,A218,A220,Def5;
end;
len Sum g1 = i+1 by A4,A153,MATRLIN:def 6;
then r2 = Sum g1 by A7,A156,FINSEQ_2:9;
then
A234: Sum r2 = Sum FlattenSeq g1 by POLYNOM1:14;
len FlattenSeq g1=len prodTuples(p,q,r,FlattenSeq g2) by A190,Def5;
then
A235: FlattenSeq g1=prodTuples(p,q,r,FlattenSeq g2) by A193,FINSEQ_2:9;
len FlattenSeq f1=len prodTuples(p,q,r,FlattenSeq f2) by A217,Def5;
then FlattenSeq f1=prodTuples(p,q,r,FlattenSeq f2) by A219,FINSEQ_2:9;
then
A236: FlattenSeq f1 = (FlattenSeq g1)*P by A235,A117,Th15;
len Sum f1 = i+1 by A1,A124,MATRLIN:def 6;
then r1 = Sum f1 by A120,A127,FINSEQ_2:9;
then Sum r1 = Sum FlattenSeq f1 by POLYNOM1:14;
hence (p*'q*'r).i = (p*'(q*'r)).i by A121,A8,A234,A236,RLVECT_2:7;
end;
hence thesis;
end;
definition
let L be Abelian add-associative right_zeroed commutative non empty
doubleLoopStr;
let p,q be sequence of L;
redefine func p*'q; :: redefines *' (POLYNOM3, definition)
commutativity
proof
let p,q be sequence of L;
now
let i be Element of NAT;
consider r1 be FinSequence of the carrier of L such that
A1: len r1 = i+1 and
A2: (p*'q).i = Sum r1 and
A3: for k be Element of NAT st k in dom r1 holds r1.k = p.(k-'1) * q
.(i+1-'k) by Def9;
consider r2 be FinSequence of the carrier of L such that
A4: len r2 = i+1 and
A5: (q*'p).i = Sum r2 and
A6: for k be Element of NAT st k in dom r2 holds r2.k = q.(k-'1) * p
.(i+1-'k) by Def9;
now
let k be Nat;
assume
A7: k in dom r1;
then
A8: 1 <= k by FINSEQ_3:25;
then
A9: k-1 >= 0 by XREAL_1:48;
k <= i+1 by A1,A7,FINSEQ_3:25;
then
A10: i+1-k >= 0 by XREAL_1:48;
then reconsider k1 = len r2 - k + 1 as Element of NAT by A4,INT_1:3;
A11: i+1-'k = i+1-k+1-1 by A10,XREAL_0:def 2
.= k1-'1 by A4,A10,XREAL_0:def 2;
1-k <= 0 by A8,XREAL_1:47;
then i+(1-k) <= i+(0 qua Nat) by XREAL_1:6;
then
A12: k1 <= i+1 by A4,XREAL_1:6;
then i+1-k1 >= 0 by XREAL_1:48;
then
A13: i+1-'k1 = i+1-(i+1-(k-1)) by A4,XREAL_0:def 2
.= k-'1 by A9,XREAL_0:def 2;
i+1-k+1 >= 0 qua Nat+1 by A10,XREAL_1:6;
then
A14: k1 in dom r2 by A4,A12,FINSEQ_3:25;
thus r1.k = p.(k-'1) * q.(i+1-'k) by A3,A7
.= r2.(len r2 - k + 1) by A6,A14,A13,A11;
end;
then r1 = Rev r2 by A1,A4,FINSEQ_5:def 3;
hence (p*'q).i = (q*'p).i by A2,A5,Th2;
end;
hence p*'q = q*'p;
end;
end;
theorem
for L be add-associative right_zeroed right_complementable
right-distributive non empty doubleLoopStr for p be sequence of L holds
p*'0_.(L) = 0_.(L)
proof
let L be add-associative right_zeroed right_complementable
right-distributive non empty doubleLoopStr;
let p be sequence of L;
now
let i be Element of NAT;
consider r be FinSequence of the carrier of L such that
len r = i+1 and
A1: (p*'0_.(L)).i = Sum r and
A2: for k be Element of NAT st k in dom r holds r.k = p.(k-'1) * (0_.(
L)).(i+1-'k) by Def9;
now
let k be Element of NAT;
assume k in dom r;
hence r.k = p.(k-'1) * (0_.(L)).(i+1-'k) by A2
.= p.(k-'1) * 0.L by FUNCOP_1:7
.= 0.L;
end;
hence (p*'0_.(L)).i = 0.L by A1,Th1
.= (0_.(L)).i by FUNCOP_1:7;
end;
hence thesis;
end;
theorem Th33:
for L be add-associative right_zeroed well-unital
right_complementable right-distributive non empty doubleLoopStr
for p be sequence of L holds p*'1_.(L) = p
proof
let L be add-associative right_zeroed well-unital right_complementable
right-distributive non empty doubleLoopStr;
let p be sequence of L;
now
let i be Element of NAT;
consider r be FinSequence of the carrier of L such that
A1: len r = i+1 and
A2: (p*'1_.(L)).i = Sum r and
A3: for k be Element of NAT st k in dom r holds r.k = p.(k-'1) * (1_.(
L)).(i+1-'k) by Def9;
a1: r <> {} by A1;
i+1 in Seg len r by A1,FINSEQ_1:4;
then
A4: i+1 in dom r by FINSEQ_1:def 3;
now
let k be Element of NAT;
assume k in dom Del(r,i+1);
then
A5: k in Seg len Del(r,i+1) by FINSEQ_1:def 3;
then k in Seg i by A1,PRE_POLY:12;
then
A6: k <= i by FINSEQ_1:1;
then
A7: k < i+1 by NAT_1:13;
A8: i+1-k <> 0 by A6,NAT_1:13;
i+1-k >= 0 by A7,XREAL_1:48;
then
A9: i+1-'k <> 0 by A8,XREAL_0:def 2;
1 <= k by A5,FINSEQ_1:1;
then k in Seg (i+1) by A7,FINSEQ_1:1;
then
A10: k in dom r by A1,FINSEQ_1:def 3;
thus Del(r,i+1).k = r.k by A7,FINSEQ_3:110
.= p.(k-'1) * (1_.(L)).(i+1-'k) by A3,A10
.= p.(k-'1) * 0.L by A9,Th28
.= 0.L;
end;
then
A11: Sum Del(r,i+1) = 0.L by Th1;
r = Del(r,i+1) ^ <*r.(i+1)*> by A1,a1,PRE_POLY:13
.= Del(r,i+1) ^ <*r/.(i+1)*> by A4,PARTFUN1:def 6;
then
A12: Sum r = Sum Del(r,i+1) + Sum <*r/.(i+1)*> by RLVECT_1:41
.= Sum Del(r,i+1) + (r/.(i+1)) by RLVECT_1:44;
r/.(i+1) = r.(i+1) by A4,PARTFUN1:def 6
.= p.(i+1-'1) * (1_.(L)).(i+1-'(i+1)) by A3,A4
.= p.i * (1_.(L)).(i+1-'(i+1)) by NAT_D:34
.= p.i * (1_.(L)).0 by XREAL_1:232
.= (p.i) * 1_L by Th28
.= p.i;
hence (p*'1_.(L)).i = p.i by A2,A12,A11,RLVECT_1:4;
end;
hence thesis;
end;
begin :: The Ring of Polynomials
definition
let L be add-associative right_zeroed right_complementable distributive
non empty doubleLoopStr;
func Polynom-Ring L -> strict non empty doubleLoopStr means
:Def10:
(for x be set holds x in the carrier of it iff x is Polynomial of L) &
(for x,y be Element of it, p,q be sequence of L st x = p & y = q
holds x+y = p+q) &
(for x,y be Element of it, p,q be sequence of L st x = p & y = q
holds x*y = p*'q) &
0.it = 0_.(L) & 1.it = 1_.(L);
existence
proof
A1: 0_.(L) in the set of all x where x is Polynomial of L ;
then reconsider
Ca = the set of all x where x is Polynomial of L as non
empty set;
reconsider Ze = 0_.(L) as Element of Ca by A1;
defpred P[set,set,set] means ex p,q be Polynomial of L st p=$1 & q=$2 & $3
=p+q;
A2: for x,y be Element of Ca ex u be Element of Ca st P[x,y,u]
proof
let x,y be Element of Ca;
x in Ca;
then consider p be Polynomial of L such that
A3: x=p;
y in Ca;
then consider q be Polynomial of L such that
A4: y=q;
p+q in Ca;
then reconsider u=p+q as Element of Ca;
take u,p,q;
thus thesis by A3,A4;
end;
consider Ad be Function of [:Ca,Ca:],Ca such that
A5: for x,y be Element of Ca holds P[x,y,Ad.(x,y)] from BINOP_1:sch 3(
A2 );
1_.(L) in the set of all x where x is Polynomial of L ;
then reconsider Un = 1_.(L) as Element of Ca;
defpred P[set,set,set] means ex p,q be Polynomial of L st p=$1 & q=$2 & $3
=p*'q;
A6: for x,y be Element of Ca ex u be Element of Ca st P[x,y,u]
proof
let x,y be Element of Ca;
x in Ca;
then consider p be Polynomial of L such that
A7: x=p;
y in Ca;
then consider q be Polynomial of L such that
A8: y=q;
p*'q in Ca;
then reconsider u=p*'q as Element of Ca;
take u,p,q;
thus thesis by A7,A8;
end;
consider Mu be Function of [:Ca,Ca:],Ca such that
A9: for x,y be Element of Ca holds P[x,y,Mu.(x,y)] from BINOP_1:sch 3
(A6 );
reconsider P = doubleLoopStr(# Ca, Ad, Mu, Un, Ze #) as strict non empty
doubleLoopStr;
take P;
thus for x be set holds x in the carrier of P iff x is Polynomial of L
proof
let x be set;
thus x in the carrier of P implies x is Polynomial of L
proof
assume x in the carrier of P;
then ex p be Polynomial of L st x=p;
hence thesis;
end;
thus thesis;
end;
thus for x,y be Element of P, p,q be sequence of L st x = p & y = q holds
x+y = p+q
proof
let x,y be Element of P;
let p,q be sequence of L;
assume
A10: x = p & y = q;
ex p1,q1 be Polynomial of L st p1 = x & q1 = y & Ad.(x, y) = p1+q1 by A5;
hence thesis by A10;
end;
thus for x,y be Element of P, p,q be sequence of L st x = p & y = q holds
x*y = p*'q
proof
let x,y be Element of P;
let p,q be sequence of L;
assume
A11: x = p & y = q;
ex p1,q1 be Polynomial of L st p1 = x & q1 = y & Mu.(x,y) = p1*'q1 by A9;
hence thesis by A11;
end;
thus 0.P = 0_.(L);
thus thesis;
end;
uniqueness
proof
let P1,P2 be strict non empty doubleLoopStr such that
A12: for x be set holds x in the carrier of P1 iff x is Polynomial of L and
A13: for x,y be Element of P1, p,q be sequence of L st x = p & y = q
holds x+y = p+q and
A14: for x,y be Element of P1, p,q be sequence of L st x = p & y = q
holds x*y = p*'q and
A15: 0.P1 = 0_.(L) & 1.P1 = 1_.(L) and
A16: for x be set holds x in the carrier of P2 iff x is Polynomial of L and
A17: for x,y be Element of P2, p,q be sequence of L st x = p & y = q
holds x+y = p+q and
A18: for x,y be Element of P2, p,q be sequence of L st x = p & y = q
holds x*y = p*'q and
A19: 0.P2 = 0_.(L) & 1.P2 = 1_.(L);
A20: now
let x be object;
x in the carrier of P1 iff x is Polynomial of L by A12;
hence x in the carrier of P1 iff x in the carrier of P2 by A16;
end;
then
A21: the carrier of P1 = the carrier of P2 by TARSKI:2;
A22: now
let x be Element of P1, y be Element of P2;
reconsider y1=y as Element of P1 by A20;
reconsider x1=x as Element of P2 by A20;
reconsider p=x as sequence of L by A12;
reconsider q=y as sequence of L by A16;
thus (the multF of P1).(x,y) = x*y1 .= p*'q by A14
.= x1*y by A18
.= (the multF of P2).(x,y);
end;
now
let x be Element of P1, y be Element of P2;
reconsider y1=y as Element of P1 by A20;
reconsider x1=x as Element of P2 by A20;
reconsider p=x as sequence of L by A12;
reconsider q=y as sequence of L by A16;
thus (the addF of P1).(x,y) = x+y1 .= p+q by A13
.= x1+y by A17
.= (the addF of P2).(x,y);
end;
then the addF of P1 = the addF of P2 by A21,BINOP_1:2;
hence thesis by A15,A19,A21,A22,BINOP_1:2;
end;
end;
registration
let L be Abelian add-associative right_zeroed right_complementable
distributive non empty doubleLoopStr;
cluster Polynom-Ring L -> Abelian;
coherence
proof
let p,q be Element of Polynom-Ring L;
reconsider p1=p, q1=q as sequence of L by Def10;
thus p + q = p1 + q1 by Def10
.= q + p by Def10;
end;
end;
registration
let L be add-associative right_zeroed right_complementable distributive
non empty doubleLoopStr;
cluster Polynom-Ring L -> add-associative;
coherence
proof
let p,q,r be Element of Polynom-Ring L;
reconsider p1=p, q1=q, r1=r as sequence of L by Def10;
A1: q + r = q1 + r1 by Def10;
p + q = p1 + q1 by Def10;
hence (p + q) + r = (p1 + q1) + r1 by Def10
.= p1 + (q1 + r1) by Th24
.= p + (q + r) by A1,Def10;
end;
cluster Polynom-Ring L -> right_zeroed;
coherence
proof
let p be Element of Polynom-Ring L;
reconsider p1=p as sequence of L by Def10;
0.(Polynom-Ring L) = 0_.(L) by Def10;
hence p + 0.(Polynom-Ring L) = p1 + 0_.(L) by Def10
.= p by Th26;
end;
cluster Polynom-Ring L -> right_complementable;
coherence
proof
let p be Element of Polynom-Ring L;
reconsider p1=p as Polynomial of L by Def10;
reconsider q = -p1 as Element of Polynom-Ring L by Def10;
take q;
thus p + q = p1 - p1 by Def10
.= 0_.(L) by Th27
.= 0.(Polynom-Ring L) by Def10;
end;
end;
registration
let L be Abelian add-associative right_zeroed right_complementable
commutative distributive non empty doubleLoopStr;
cluster Polynom-Ring L -> commutative;
coherence
proof
let p,q be Element of Polynom-Ring L;
reconsider p1=p, q1=q as sequence of L by Def10;
thus p * q = p1 *' q1 by Def10
.= q * p by Def10;
end;
end;
registration
let L be Abelian add-associative right_zeroed right_complementable
well-unital associative distributive non empty doubleLoopStr;
cluster Polynom-Ring L -> associative;
coherence
proof
let p,q,r be Element of Polynom-Ring L;
reconsider p1=p, q1=q, r1=r as sequence of L by Def10;
A1: q * r = q1 *' r1 by Def10;
p * q = p1 *' q1 by Def10;
hence (p * q) * r = (p1 *' q1) *' r1 by Def10
.= p1 *' (q1 *' r1) by Th31
.= p * (q * r) by A1,Def10;
end;
end;
theorem Th33a:
for L be add-associative right_zeroed well-unital
right_complementable left-distributive non empty doubleLoopStr
for p be sequence of L holds (1_.(L))*'p = p
proof
let L be add-associative right_zeroed well-unital right_complementable
left-distributive non empty doubleLoopStr;
let p be sequence of L;
now
let i be Element of NAT;
consider r be FinSequence of the carrier of L such that
A1: len r = i+1 and
A2: ((1_.(L))*'p).i = Sum r and
A3: for k be Element of NAT st k in dom r holds r.k = (1_.(L)).(k-'1)*
p.(i+1-'k) by Def9;
A4: 1 in dom r by A1,CARD_1:27,FINSEQ_5:6;
now
let k be Element of NAT;
A5: k+1 >= 1 by NAT_1:11;
assume
A6: k in dom Del(r,1);
then
A7: k<>0 by FINSEQ_3:25;
len Del(r,1) = i by A1,A4,FINSEQ_3:109;
then
A8: k <= i by A6,FINSEQ_3:25;
then k+1 <= i+ 1 by XREAL_1:6;
then
A9: k+1 in dom r by A1,A5,FINSEQ_3:25;
0+1 <= k by A6,FINSEQ_3:25;
hence Del(r,1).k = r.(k+1) by A1,A4,A8,FINSEQ_3:111
.= (1_.(L)).(k+1-'1)*p.(i+1-'(k+1)) by A3,A9
.= (1_.(L)).(k)*p.(i+1-'(k+1)) by NAT_D:34
.= 0.(L)*p.(i+1-'(k+1)) by A7,Th28
.= 0.(L);
end;
then
A10: Sum Del(r,1) = 0.(L) by Th1;
r = <*r.1*>^Del(r,1) by A1,FINSEQ_5:86,CARD_1:27
.= <*r/.1*>^Del(r,1) by A4,PARTFUN1:def 6;
then
A11: Sum r = Sum <*r/.1*> + Sum Del(r,1) by RLVECT_1:41
.= r/.1 + Sum Del(r,1)by RLVECT_1:44;
r/.1 = r.1 by A4,PARTFUN1:def 6
.= (1_.(L)).(1-'1)*p.(i+1-'1) by A3,A4
.= (1_.(L)).(1-'1)*p.i by NAT_D:34
.= (1_.(L)).(0)*p.i by XREAL_1:232
.= 1_(L)*p.i by Th28
.= p.i;
hence ((1_.(L))*'p).i = p.i by A2,A11,A10,RLVECT_1:4;
end;
hence thesis;
end;
Lm2: now
let L be add-associative right_zeroed right_complementable well-unital
Abelian distributive non empty doubleLoopStr;
set Pm = Polynom-Ring L;
let x, e be Element of Pm;
reconsider p = x as Polynomial of L by Def10;
assume
A1: e = 1.Pm;
A2: 1.Pm = 1_.L by Def10;
hence x*e = p*'1_.L by A1,Def10
.= x by Th33;
thus e*x = (1_.L)*'p by A1,A2,Def10
.= x by Th33a;
end;
registration
let L be add-associative right_zeroed right_complementable well-unital
Abelian distributive non empty doubleLoopStr;
cluster Polynom-Ring L -> well-unital;
coherence by Lm2;
end;
registration
let L be Abelian add-associative right_zeroed right_complementable
distributive non empty doubleLoopStr;
cluster Polynom-Ring L -> distributive;
coherence
proof
let p,q,r be Element of Polynom-Ring L;
reconsider p1=p, q1=q, r1=r as sequence of L by Def10;
A1: p*q = p1*'q1 & p*r = p1*'r1 by Def10;
q+r = q1+r1 by Def10;
hence p*(q+r) = p1*'(q1+r1) by Def10
.= p1*'q1+p1*'r1 by Th29
.= p*q+p*r by A1,Def10;
A2: q*p = q1*'p1 & r*p = r1*'p1 by Def10;
q+r = q1+r1 by Def10;
hence (q+r)*p = (q1+r1)*'p1 by Def10
.= q1*'p1+r1*'p1 by Th30
.= q*p+r*p by A2,Def10;
end;
end;
theorem
for L being add-associative right_zeroed right_complementable
well-unital Abelian distributive non empty doubleLoopStr
holds 1.Polynom-Ring L = 1_.L by Def10;