:: Evaluation of Multivariate Polynomials
:: by Christoph Schwarzweller and Andrzej Trybulec
::
:: Received April 14, 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, XBOOLE_0, SUBSET_1, FINSEQ_1, RELAT_1, PARTFUN1, CARD_1,
FUNCT_1, TARSKI, XXREAL_0, ARYTM_1, ARYTM_3, NAT_1, ORDERS_1, RELAT_2,
GROUP_1, BINOP_1, ALGSTR_0, RLVECT_1, VECTSP_1, LATTICES, ZFMISC_1,
FINSET_1, ALGSTR_1, STRUCT_0, SUPINF_2, CARD_3, FINSOP_1, ORDINAL4,
PRE_POLY, FINSEQ_5, FUNCT_4, FUNCOP_1, ORDINAL1, WELLORD2, MESFUNC1,
RFINSEQ, POLYNOM1, ALGSEQ_1, MSSUBFAM, QUOFIELD, POLYNOM2;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, CARD_1, ORDINAL1, NUMBERS,
RELAT_1, FINSOP_1, RELAT_2, RELSET_1, FUNCT_1, FINSET_1, XCMPLX_0,
PARTFUN1, FUNCT_2, BINOP_1, FUNCT_4, FUNCT_7, REAL_1, NAT_1, ALGSTR_1,
ORDERS_1, FINSEQ_1, STRUCT_0, ALGSTR_0, RLVECT_1, FUNCOP_1, VFUNCT_1,
VECTSP_1, GROUP_1, GROUP_4, QUOFIELD, FINSEQ_5, GRCAT_1, RFINSEQ,
YELLOW_1, GROUP_6, XXREAL_0, RECDEF_1, PRE_POLY, POLYNOM1;
constructors REAL_1, FINSOP_1, RFINSEQ, BINARITH, FINSEQ_5, GROUP_4, GRCAT_1,
GROUP_6, MONOID_0, TRIANG_1, YELLOW_1, QUOFIELD, POLYNOM1, RECDEF_1,
ALGSTR_1, RELSET_1, FUNCT_7, FVSUM_1, VFUNCT_1, DOMAIN_1, RINGCAT1;
registrations XBOOLE_0, ORDINAL1, RELSET_1, FUNCOP_1, FINSET_1, XREAL_0,
NAT_1, INT_1, FINSEQ_1, STRUCT_0, VECTSP_1, ALGSTR_1, MONOID_0, POLYNOM1,
VALUED_0, CARD_1, SUBSET_1, PRE_POLY, RELAT_1, VFUNCT_1, FUNCT_2,
FUNCT_1, PBOOLE, RINGCAT1;
requirements NUMERALS, BOOLE, SUBSET, REAL, ARITHM;
definitions GROUP_1;
equalities BINOP_1, FUNCOP_1, ALGSTR_0;
theorems TARSKI, FINSEQ_1, FUNCT_1, FUNCT_2, ORDINAL1, RELAT_1, ZFMISC_1,
VECTSP_1, POLYNOM1, RELAT_2, FUNCT_7, FUNCT_4, FUNCOP_1, ORDERS_1, NAT_1,
FINSEQ_4, INT_1, FINSEQ_3, RLVECT_1, GROUP_4, PARTFUN2, CARD_1, RFINSEQ,
FINSOP_1, FINSEQ_5, CARD_2, FINSEQ_2, ALGSTR_1, GROUP_1, XBOOLE_0,
XBOOLE_1, PARTFUN1, XREAL_1, GROUP_6, XXREAL_0, PRE_POLY, XTUPLE_0;
schemes FUNCT_2, NAT_1, RECDEF_1, INT_1;
begin :: Preliminaries
Lm1: for X being set, A being Subset of X, O being Order of X holds O
is_reflexive_in A & O is_antisymmetric_in A & O is_transitive_in A
proof
let X be set, A be Subset of X, O be Order of X;
A1: field O = X by ORDERS_1:12;
then O is_antisymmetric_in X by RELAT_2:def 12;
then
A2: for x,y being object holds x in A & y in A & [x,y] in O & [y,x] in O
implies x = y by RELAT_2:def 4;
O is_transitive_in X by A1,RELAT_2:def 16;
then
A3: for x,y,z being object holds x in A & y in A & z in A & [x,y] in O & [y,z]
in O implies [x,z] in O by RELAT_2:def 8;
O is_reflexive_in X by A1,RELAT_2:def 9;
then for x being object holds x in A implies [x,x] in O by RELAT_2:def 1;
hence thesis by A2,A3,RELAT_2:def 1,def 4,def 8;
end;
Lm2: for X being set, A being Subset of X, O being Order of X st O
is_connected_in X holds O is_connected_in A
proof
let X be set, A be Subset of X, O be Order of X;
assume O is_connected_in X;
then
for x,y being object holds x in A & y in A & x <> y implies [x,y] in O or [
y,x] in O by RELAT_2:def 6;
hence thesis by RELAT_2:def 6;
end;
Lm3: for X being set, S being Subset of X, R being Order of X st R is
being_linear-order holds R linearly_orders S
proof
let X be set, S be Subset of X, R be Order of X;
A1: field R = X by ORDERS_1:12;
then
A2: R is_reflexive_in X by RELAT_2:def 9;
R is_transitive_in X by A1,RELAT_2:def 16;
then
for x,y,z being object holds x in S & y in S & z in S & [x,y] in R & [y,z]
in R implies [x,z] in R by RELAT_2:def 8;
then
A3: R is_transitive_in S by RELAT_2:def 8;
R is_antisymmetric_in X by A1,RELAT_2:def 12;
then for x,y being object holds x in S & y in S & [x,y] in R & [y,x] in R
implies x = y by RELAT_2:def 4;
then
A4: R is_antisymmetric_in S by RELAT_2:def 4;
assume R is being_linear-order;
then R is connected by ORDERS_1:def 6;
then
A5: R is_connected_in field R by RELAT_2:def 14;
for x,y being object holds x in S & y in S & x <> y implies [x,y] in R or
[y,x] in R
proof
let x,y be object;
assume that
A6: x in S and
A7: y in S and
A8: x <> y;
A9: field R = dom R \/ rng R by RELAT_1:def 6;
[y,y] in R by A2,A7,RELAT_2:def 1;
then y in dom R by XTUPLE_0:def 12;
then
A10: y in field R by A9,XBOOLE_0:def 3;
[x,x] in R by A2,A6,RELAT_2:def 1;
then x in dom R by XTUPLE_0:def 12;
then x in field R by A9,XBOOLE_0:def 3;
hence thesis by A5,A8,A10,RELAT_2:def 6;
end;
then
A11: R is_connected_in S by RELAT_2:def 6;
for x being object holds x in S implies [x,x] in R by A2,RELAT_2:def 1;
then R is_reflexive_in S by RELAT_2:def 1;
hence thesis by A4,A3,A11,ORDERS_1:def 9;
end;
theorem Th1:
for L being unital associative non empty multMagma, a being Element of L,
n,m being Element of NAT holds
power(L).(a,n+m) = power(L).(a,n) * power(L).(a,m)
proof
let L be unital associative non empty multMagma, a be Element of L, n,m be
Element of NAT;
defpred P[Nat] means power(L).(a,n+$1) = power(L).(a,n) * power(L).(a,$1);
A1: now
let m be Nat;
assume
A2: P[m];
power(L).(a,n+(m+1)) = power(L).(a,(n+m)+1)
.= (power(L).(a,n) * power(L).(a,m)) * a by A2,GROUP_1:def 7
.= power(L).(a,n) * (power(L).(a,m) * a) by GROUP_1:def 3
.= power(L).(a,n) * power(L).(a,(m+1)) by GROUP_1:def 7;
hence P[m+1];
end;
power(L).(a,n + 0) = power(L).(a,n) * 1_L by GROUP_1:def 4
.= power(L).(a,n) * power(L).(a,0) by GROUP_1:def 7;
then
A3: P[0];
for m being Nat holds P[m] from NAT_1:sch 2(A3,A1);
hence thesis;
end;
registration
cluster Abelian right_zeroed add-associative right_complementable
well-unital distributive commutative associative for non trivial
doubleLoopStr;
existence
proof
take F_Real;
thus thesis;
end;
end;
begin
::$CT
theorem Th2:
for L being left_zeroed right_zeroed non empty addLoopStr, p
being FinSequence of the carrier of L, i being Element of NAT st i in dom p &
for i9 being Element of NAT st i9 in dom p & i9 <> i holds p/.i9 = 0.L holds
Sum p = p/.i
proof
let L be left_zeroed right_zeroed non empty addLoopStr, p be FinSequence
of the carrier of L, i be Element of NAT;
assume that
A1: i in dom p and
A2: for i9 being Element of NAT st i9 in dom p & i9 <> i holds p/.i9 = 0.L;
consider fp being sequence of the carrier of L such that
A3: Sum p = fp.(len p) and
A4: fp.0 = 0.L and
A5: for j being Nat, v being Element of L st j < len p & v =
p.(j + 1) holds fp.(j + 1) = fp.j + v by RLVECT_1:def 12;
defpred P[Element of NAT] means ($1 < i & fp.($1) = 0.L) or (i <= $1 & fp.(
$1) = p/.i);
consider l being Nat such that
A6: dom p = Seg l by FINSEQ_1:def 2;
reconsider l as Element of NAT by ORDINAL1:def 12;
A7: len p = l by A6,FINSEQ_1:def 3;
i in {z where z is Nat : 1 <= z & z <= l} by A1,A6,FINSEQ_1:def 1;
then
A8: ex i9 being Nat st i9 = i & 1 <= i9 & i9 <= l;
A9: for j being Element of NAT st 0 <= j & j < len p holds P[j] implies P[j +1]
proof
let j be Element of NAT;
assume that
0 <= j and
A10: j < len p;
assume
A11: P[j];
per cases;
suppose
A12: j < i;
per cases;
suppose
A13: j + 1 = i;
then p.(j+1) = p/.(j+1) by A1,PARTFUN1:def 6;
then fp.(j+1) = 0.L + p/.(j+1) by A5,A10,A11,A12
.= p/.(j+1) by ALGSTR_1:def 2;
hence thesis by A13;
end;
suppose
A14: j + 1 <> i;
A15: j + 1 < i
proof
assume i <= j + 1;
then i < j + 1 by A14,XXREAL_0:1;
hence thesis by A12,NAT_1:13;
end;
j + 1 <= i by A12,NAT_1:13;
then
A16: j + 1 <= l by A8,XXREAL_0:2;
0 + 1 <= j + 1 by XREAL_1:6;
then
A17: j + 1 in Seg l by A16,FINSEQ_1:1;
then p.(j+1) = p/.(j+1) by A6,PARTFUN1:def 6;
then fp.(j+1) = 0.L + p/.(j+1) by A5,A10,A11,A12
.= p/.(j+1) by ALGSTR_1:def 2
.= 0.L by A2,A6,A14,A17;
hence thesis by A15;
end;
end;
suppose
A18: i <= j;
j < l by A6,A10,FINSEQ_1:def 3;
then
A19: j + 1 <= l by NAT_1:13;
A20: i < j + 1 by A18,NAT_1:13;
0 + 1 <= j + 1 by XREAL_1:6;
then
A21: j + 1 in dom p by A6,A19,FINSEQ_1:1;
then p.(j+1) = p/.(j+1) by PARTFUN1:def 6;
then fp.(j+1) = p/.i + p/.(j+1) by A5,A10,A11,A18
.= p/.i + 0.L by A2,A20,A21
.= p/.i by RLVECT_1:def 4;
hence thesis by A18,NAT_1:13;
end;
end;
A22: P[0] by A4,A8;
for j being Element of NAT st 0 <= j & j <= len p holds P[j] from
INT_1:sch 7(A22,A9);
hence thesis by A3,A8,A7;
end;
theorem
for L being add-associative right_zeroed right_complementable
distributive well-unital non empty doubleLoopStr, p being FinSequence of the
carrier of L st ex i being Element of NAT st i in dom p & p/.i = 0.L holds
Product p = 0.L
proof
let L be add-associative right_zeroed right_complementable distributive
well-unital non empty doubleLoopStr, p be FinSequence of the carrier of L;
given i being Element of NAT such that
A1: i in dom p and
A2: p/.i = 0.L;
defpred P[Nat] means for p being FinSequence of the carrier of L
st len p = $1 & ex i being Element of NAT st i in dom p & p/.i = 0.L holds
Product p = 0.L;
A3: for j being Nat holds P[j] implies P[j+1]
proof
let j be Nat;
assume
A4: P[j];
for p being FinSequence of the carrier of L st len p = j+1 & ex i
being Element of NAT st i in dom p & p/.i = 0.L holds Product p = 0.L
proof
let p be FinSequence of the carrier of L;
assume that
A5: len p = j+1 and
A6: ex i being Element of NAT st i in dom p & p/.i = 0.L;
A7: ex fp being sequence of the carrier of L st fp.1 = p.1 &( for
i being Nat st 0 <> i & i < len p holds fp.(i + 1) = (the multF of L
).(fp.i,p.(i+1)))& (the multF of L) "**" p = fp.(len p) by A5,FINSOP_1:1
,NAT_1:14;
A8: len p >= 1 by A5,NAT_1:14;
then
A9: 1 in dom p by FINSEQ_3:25;
A10: dom p = Seg len p by FINSEQ_1:def 3;
then
A11: j+1 in dom p by A5,A8,FINSEQ_1:1;
per cases;
suppose
A12: j = 0;
then
A13: dom p = {1} by A5,FINSEQ_1:2,def 3;
Product p = p.1 by A5,A7,A12,GROUP_4:def 2
.= p/.1 by A9,PARTFUN1:def 6;
hence thesis by A6,A13,TARSKI:def 1;
end;
suppose
j <> 0;
then
A14: 1 <= j by NAT_1:14;
reconsider p9 = p|(Seg j) as FinSequence of the carrier of L by
FINSEQ_1:18;
A15: j <= j+1 by XREAL_1:29;
then
A16: dom p9 = Seg j by A5,FINSEQ_1:17;
p = (p9)^<*p.(len p)*> by A5,FINSEQ_3:55;
then
A17: p = (p9)^<*p/.(len p)*> by A5,A11,PARTFUN1:def 6;
A18: len p9 = j by A5,A15,FINSEQ_1:17;
per cases;
suppose
p/.(len p) = 0.L;
hence Product p = Product(p9) * 0.L by A17,GROUP_4:6
.= 0.L;
end;
suppose
A19: p/.(len p) <> 0.L;
consider i being Element of NAT such that
A20: i in dom p and
A21: p/.i = 0.L by A6;
i <= len p by A10,A20,FINSEQ_1:1;
then i < len p by A19,A21,XXREAL_0:1;
then
A22: i <= j by A5,NAT_1:13;
A23: 1 <= i by A10,A20,FINSEQ_1:1;
then
A24: i in dom p9 by A16,A22,FINSEQ_1:1;
A25: j in dom p by A5,A10,A14,A15,FINSEQ_1:1;
i in Seg j by A23,A22,FINSEQ_1:1;
then (p|j).i = p.i by A25,RFINSEQ:6;
then p9.i = p.i by FINSEQ_1:def 16;
then p9/.i = p.i by A24,PARTFUN1:def 6;
then
A26: p9/.i = 0.L by A20,A21,PARTFUN1:def 6;
thus Product p = Product(p9) * p/.(len p) by A17,GROUP_4:6
.= 0.L * p/.(len p) by A4,A18,A24,A26
.= 0.L;
end;
end;
end;
hence thesis;
end;
A27: ex l being Element of NAT st l = len p;
A28: P[0]
proof
let p be FinSequence of L;
assume len p = 0;
then p = {};
hence thesis;
end;
for j being Nat holds P[j] from NAT_1:sch 2(A28,A3);
hence thesis by A1,A2,A27;
end;
theorem Th4:
for L being Abelian add-associative non empty addLoopStr, a
being Element of L, p,q being FinSequence of the carrier of L st len p = len q
& ex i being Element of NAT st i in dom p & q/.i = a + p/.i & for i9 being
Element of NAT st i9 in dom p & i9 <> i holds q/.i9 = p/.i9 holds Sum q = a +
Sum p
proof
let L be Abelian add-associative non empty addLoopStr, a be Element of L,
p,q be FinSequence of the carrier of L;
assume that
A1: len p = len q and
A2: ex i being Element of NAT st i in dom p & q/.i = a + p/.i & for i9
being Element of NAT st i9 in dom p & i9 <> i holds q/.i9 = p/.i9;
consider i being Element of NAT such that
A3: i in dom p and
A4: q/.i = a + p/.i and
A5: for i9 being Element of NAT st i9 in dom p & i9 <> i holds q/.i9 = p
/.i9 by A2;
consider fq being sequence of the carrier of L such that
A6: Sum q = fq.(len q) and
A7: fq.0 = 0.L and
A8: for j being Nat, v being Element of L st j < len q & v =
q.(j + 1) holds fq.(j + 1) = fq.j + v by RLVECT_1:def 12;
consider l being Nat such that
A9: dom p = Seg l by FINSEQ_1:def 2;
i in {z where z is Nat : 1 <= z & z <= l} by A3,A9,FINSEQ_1:def 1;
then
A10: ex i9 being Nat st i9 = i & 1 <= i9 & i9 <= l;
consider l9 being Nat such that
A11: dom q = Seg l9 by FINSEQ_1:def 2;
reconsider l,l9 as Element of NAT by ORDINAL1:def 12;
consider fp being sequence of the carrier of L such that
A12: Sum p = fp.(len p) and
A13: fp.0 = 0.L and
A14: for j being Nat, v being Element of L st j < len p & v =
p.(j + 1) holds fp.(j + 1) = fp.j + v by RLVECT_1:def 12;
A15: len p = l by A9,FINSEQ_1:def 3;
defpred P[Element of NAT] means ($1 < i & fp.($1) = fq.($1)) or (i <= $1 &
fq.($1) = a + fp.($1));
A16: l = len p by A9,FINSEQ_1:def 3
.= l9 by A1,A11,FINSEQ_1:def 3;
A17: for j being Element of NAT st 0 <= j & j < len p holds P[j] implies P[j
+1]
proof
let j be Element of NAT;
assume that
0 <= j and
A18: j < len p;
assume
A19: P[j];
per cases;
suppose
A20: j < i;
per cases;
suppose
A21: j + 1 = i;
then
A22: p.(j+1) = p/.(j+1) by A3,PARTFUN1:def 6;
q.(j+1) = q/.(j+1) by A3,A9,A11,A16,A21,PARTFUN1:def 6;
then fq.(j+1) = fq.j + (a + p/.(j+1)) by A1,A4,A8,A18,A21
.= a + (fq.j + p/.(j+1)) by RLVECT_1:def 3
.= a + fp.(j+1) by A14,A18,A19,A20,A22;
hence thesis by A21;
end;
suppose
A23: j + 1 <> i;
A24: j + 1 < i
proof
assume i <= j + 1;
then i < j + 1 by A23,XXREAL_0:1;
hence thesis by A20,NAT_1:13;
end;
j + 1 <= i by A20,NAT_1:13;
then
A25: j + 1 <= l by A10,XXREAL_0:2;
0 + 1 <= j + 1 by XREAL_1:6;
then
A26: j + 1 in Seg l by A25,FINSEQ_1:1;
then
A27: p.(j+1) = p/.(j+1) by A9,PARTFUN1:def 6;
q.(j+1) = q/.(j+1) by A11,A16,A26,PARTFUN1:def 6;
then fq.(j+1) = fq.j + q/.(j+1) by A1,A8,A18
.= fp.(j+1) by A5,A14,A9,A18,A19,A20,A23,A26,A27;
hence thesis by A24;
end;
end;
suppose
A28: i <= j;
j < l by A9,A18,FINSEQ_1:def 3;
then
A29: j + 1 <= l by NAT_1:13;
0 + 1 <= j + 1 by XREAL_1:6;
then
A30: j + 1 in dom p by A9,A29,FINSEQ_1:1;
then
A31: p.(j+1) = p/.(j+1) by PARTFUN1:def 6;
A32: i < j + 1 by A28,NAT_1:13;
q.(j+1) = q/.(j+1) by A9,A11,A16,A30,PARTFUN1:def 6;
then fq.(j+1) = fq.j + q/.(j+1) by A1,A8,A18
.= (a + fp.j) + p/.(j+1) by A5,A19,A28,A32,A30
.= a + (fp.j + p/.(j+1)) by RLVECT_1:def 3
.= a + fp.(j+1) by A14,A18,A31;
hence thesis by A28,NAT_1:13;
end;
end;
A33: P[0] by A13,A7,A10;
for j being Element of NAT st 0 <= j & j <= len p holds P[j] from
INT_1:sch 7(A33,A17);
hence thesis by A1,A12,A6,A10,A15;
end;
theorem Th5:
for L being commutative associative non empty doubleLoopStr, a
being Element of L, p,q being FinSequence of the carrier of L st len p = len q
& ex i being Element of NAT st i in dom p & q/.i = a * p/.i & for i9 being
Element of NAT st i9 in dom p & i9 <> i holds q/.i9 = p/.i9 holds Product q = a
* Product p
proof
let L be commutative associative non empty doubleLoopStr, a be Element of
L, p,q be FinSequence of the carrier of L;
assume that
A1: len p = len q and
A2: ex i being Element of NAT st i in dom p & q/.i = a * p/.i & for i9
being Element of NAT st i9 in dom p & i9 <> i holds q/.i9 = p/.i9;
consider i being Element of NAT such that
A3: i in dom p and
A4: q/.i = a * p/.i and
A5: for i9 being Element of NAT st i9 in dom p & i9 <> i holds q/.i9 = p
/.i9 by A2;
A6: Product p = (the multF of L) "**" p by GROUP_4:def 2;
A7: Product q = (the multF of L) "**" q by GROUP_4:def 2;
per cases;
suppose
len p = 0;
then p = {};
hence thesis by A3;
end;
suppose
A8: len p <> 0;
then
A9: len p >= 1 by NAT_1:14;
consider l9 being Nat such that
A10: dom q = Seg l9 by FINSEQ_1:def 2;
consider fp being sequence of the carrier of L such that
A11: fp.1 = p.1 and
A12: for i being Nat st 0 <> i & i < len p holds fp.(i + 1)
= (the multF of L).(fp.i,p.(i+1)) and
A13: Product p = fp.(len p) by A6,A8,FINSOP_1:1,NAT_1:14;
consider fq being sequence of the carrier of L such that
A14: fq.1 = q.1 and
A15: for i being Nat st 0 <> i & i < len q holds fq.(i + 1)
= (the multF of L).(fq.i,q.(i+1)) and
A16: Product q = fq.(len p) by A1,A7,A8,FINSOP_1:1,NAT_1:14;
defpred P[Element of NAT] means ($1 < i & fp.($1) = fq.($1)) or (i <= $1 &
fq.($1) = a * fp.($1));
consider l being Nat such that
A17: dom p = Seg l by FINSEQ_1:def 2;
i in {z where z is Nat : 1 <= z & z <= l} by A3,A17,FINSEQ_1:def 1;
then
A18: ex i9 being Nat st i9 = i & 1 <= i9 & i9 <= l;
reconsider l,l9 as Element of NAT by ORDINAL1:def 12;
A19: len p = l by A17,FINSEQ_1:def 3;
A20: 1 <= l by A18,XXREAL_0:2;
then
A21: 1 in dom p by A17,FINSEQ_1:1;
A22: l = len p by A17,FINSEQ_1:def 3
.= l9 by A1,A10,FINSEQ_1:def 3;
A23: for j being Element of NAT st 1 <= j & j < len p holds P[j] implies P
[j+1]
proof
let j be Element of NAT;
assume that
A24: 1 <= j and
A25: j < len p;
assume
A26: P[j];
per cases;
suppose
A27: j < i;
per cases;
suppose
A28: j + 1 = i;
then
A29: p.(j+1) = p/.(j+1) by A3,PARTFUN1:def 6;
q.(j+1) = q/.(j+1) by A3,A17,A10,A22,A28,PARTFUN1:def 6;
then
fq.(j+1) = fp.j * (a * p/.(j+1)) by A1,A4,A15,A24,A25,A26,A27,A28
.= (fp.j * p/.(j+1)) * a by GROUP_1:def 3
.= fp.(j+1) * a by A12,A24,A25,A29;
hence thesis by A28;
end;
suppose
A30: j + 1 <> i;
A31: j + 1 < i
proof
assume i <= j + 1;
then i < j + 1 by A30,XXREAL_0:1;
hence thesis by A27,NAT_1:13;
end;
j + 1 <= i by A27,NAT_1:13;
then
A32: j + 1 <= l by A18,XXREAL_0:2;
0 + 1 <= j + 1 by XREAL_1:6;
then
A33: j + 1 in Seg l by A32,FINSEQ_1:1;
then
A34: p.(j+1) = p/.(j+1) by A17,PARTFUN1:def 6;
q.(j+1) = q/.(j+1) by A10,A22,A33,PARTFUN1:def 6;
then fq.(j+1) = fq.j * q/.(j+1) by A1,A15,A24,A25
.= (the multF of L).(fq.j,p.(j+1)) by A5,A17,A30,A33,A34
.= fp.(j+1) by A12,A24,A25,A26,A27;
hence thesis by A31;
end;
end;
suppose
A35: i <= j;
j < l by A17,A25,FINSEQ_1:def 3;
then
A36: j + 1 <= l by NAT_1:13;
0 + 1 <= j + 1 by XREAL_1:6;
then
A37: j + 1 in dom p by A17,A36,FINSEQ_1:1;
then
A38: p.(j+1) = p/.(j+1) by PARTFUN1:def 6;
A39: i < j + 1 by A35,NAT_1:13;
q.(j+1) = q/.(j+1) by A17,A10,A22,A37,PARTFUN1:def 6;
then fq.(j+1) = fq.j * q/.(j+1) by A1,A15,A24,A25
.= (a * fp.j) * p/.(j+1) by A5,A26,A35,A39,A37
.= a * (fp.j * p/.(j+1)) by GROUP_1:def 3
.= a * fp.(j+1) by A12,A24,A25,A38;
hence thesis by A35,NAT_1:13;
end;
end;
A40: 1 in dom q by A10,A22,A20,FINSEQ_1:1;
now
per cases;
case
A41: 1 < i;
thus fp.1 = p/.1 by A11,A21,PARTFUN1:def 6
.= q/.1 by A5,A21,A41
.= fq.1 by A14,A40,PARTFUN1:def 6;
end;
case
i <= 1;
then i = 1 by A18,XXREAL_0:1;
hence fq.1 = a * p/.1 by A3,A4,A14,A17,A10,A22,PARTFUN1:def 6
.= a * fp.1 by A11,A21,PARTFUN1:def 6;
end;
end;
then
A42: P[1];
for j being Element of NAT st 1 <= j & j <= len p holds P[j] from
INT_1:sch 7(A42,A23);
hence thesis by A9,A13,A16,A18,A19;
end;
end;
begin :: Evaluation of Bags -------------------------------------------------------
definition
::$CD
let n be Ordinal, b be bag of n, L be well-unital non trivial
doubleLoopStr, x be Function of n, L;
func eval(b,x) -> Element of L means
:Def1:
ex y being FinSequence of the carrier of L st
len y = len SgmX(RelIncl n, support b) & it = Product y &
for i being Element of NAT st 1 <= i & i <= len y holds
y/.i = power(L).((x * SgmX(RelIncl n, support b))/.i,
(b * SgmX(RelIncl n, support b))/.i);
existence
proof
set S = SgmX(RelIncl n, support b);
set l = len S;
defpred P[Nat,Element of L] means
$2 = power(L).((x * S)/.$1,(b * S)/.$1);
A1: for k being Nat st k in Seg l ex x being Element of L st P[k,x];
consider p being FinSequence of the carrier of L such that
A2: dom p = Seg l & for k being Nat st k in Seg l holds P[k,p/.k]
from RECDEF_1:sch 17(A1);
take Product p;
A3: len p = l by A2,FINSEQ_1:def 3;
for m being Element of NAT st 1 <= m & m <= len p
holds p/.m = power(L).((x * S)/.m, (b * S)/.m) by A3,A2,FINSEQ_1:1;
hence thesis by A3;
end;
uniqueness
proof
set S = SgmX(RelIncl n, support b);
let a,c be Element of L;
assume that
A4: ex y1 being FinSequence of the carrier of L st len y1 = (len SgmX(
RelIncl n, support b)) & a = Product y1 & for i being Element of NAT st 1 <= i
& i <= len y1 holds y1/.i = power(L).((x * SgmX(RelIncl n, support b))/.i, (b *
SgmX(RelIncl n, support b))/.i) and
A5: ex y2 being FinSequence of the carrier of L st len y2 = (len SgmX(
RelIncl n, support b)) & c = Product y2 & for i being Element of NAT st 1 <= i
& i <= len y2 holds y2/.i = power(L).((x * SgmX(RelIncl n, support b))/.i, (b *
SgmX(RelIncl n, support b))/.i);
consider y1 being FinSequence of the carrier of L such that
A6: len y1 = (len SgmX(RelIncl n, support b)) and
A7: Product y1 = a and
A8: for i being Element of NAT st 1 <= i & i <= len y1 holds y1/.i =
power(L).((x * SgmX(RelIncl n, support b))/.i, (b * SgmX(RelIncl n, support b))
/.i) by A4;
consider y2 being FinSequence of the carrier of L such that
A9: len y2 = (len SgmX(RelIncl n, support b)) and
A10: Product y2 = c and
A11: for i being Element of NAT st 1 <= i & i <= len y2 holds y2/.i =
power(L).((x * SgmX(RelIncl n, support b))/.i, (b * SgmX(RelIncl n, support b))
/.i) by A5;
now
let i be Nat;
assume that
A12: 1 <= i and
A13: i <= len y1;
i in Seg (len y2) by A6,A9,A12,A13,FINSEQ_1:1;
then
A14: i in dom y2 by FINSEQ_1:def 3;
A15: i in Seg (len y1) by A12,A13,FINSEQ_1:1;
then i in dom y1 by FINSEQ_1:def 3;
hence y1.i = y1/.i by PARTFUN1:def 6
.= power(L).((x * S)/.i,(b * S)/.i) by A8,A12,A13,A15
.= y2/.i by A6,A9,A11,A12,A13,A15
.= y2.i by A14,PARTFUN1:def 6;
end;
hence thesis by A6,A7,A9,A10,FINSEQ_1:14;
end;
end;
::$CT 7
theorem Th6:
for n being Ordinal, L being well-unital non trivial
doubleLoopStr, x being Function of n, L holds eval(EmptyBag n,x) = 1.L
proof
let n be Ordinal, L be well-unital non trivial doubleLoopStr, x
be Function of n, L;
set b = EmptyBag n;
reconsider s = support b as empty Subset of n;
consider y being FinSequence of the carrier of L such that
A1: len y = (len SgmX(RelIncl n, support b)) and
A2: eval(b,x) = Product y and
for i being Element of NAT st 1 <= i & i <= len y holds y/.i = power (L)
.((x * SgmX(RelIncl n, support b))/.i, (b * SgmX(RelIncl n, support b))/.i) by
Def1;
SgmX(RelIncl n, s) = {} by PRE_POLY:76,82;
then y = <*>the carrier of L by A1;
then eval(EmptyBag n,x) = 1_L by A2,GROUP_4:8;
hence thesis;
end;
theorem Th7:
for n being Ordinal, L being well-unital non trivial
doubleLoopStr, u being set, b being bag of n st support b = {u} for x being
Function of n, L holds eval(b,x) = power(L).(x.u,b.u)
proof
let n be Ordinal, L be well-unital non trivial doubleLoopStr, u
be set, b be bag of n;
reconsider sb = support b as finite Subset of n;
set sg = SgmX(RelIncl n, sb);
assume
A1: support b = {u};
then
A2: u in support b by TARSKI:def 1;
let x be Function of n, L;
A3: rng x c= the carrier of L by RELAT_1:def 19;
A4: n = dom x by FUNCT_2:def 1;
then x.u in rng x by A2,FUNCT_1:def 3;
then reconsider xu = x.u as Element of L by A3;
A5: RelIncl n linearly_orders sb by PRE_POLY:82;
then
A6: rng sg = {u} by A1,PRE_POLY:def 2;
then
A7: u in rng sg by TARSKI:def 1;
then
A8: 1 in dom sg by FINSEQ_3:31;
then
A9: sg.1 in rng sg by FUNCT_1:def 3;
then
A10: sg.1 = u by A6,TARSKI:def 1;
then 1 in dom (x * sg) by A4,A8,A2,FUNCT_1:11;
then
A11: (x * sg)/.1 = (x * sg).1 by PARTFUN1:def 6
.= x.(sg.1) by A8,FUNCT_1:13
.= x.u by A6,A9,TARSKI:def 1;
dom b = n by PARTFUN1:def 2;
then 1 in dom (b * sg) by A8,A10,A2,FUNCT_1:11;
then
A12: (b * sg)/.1 = (b * sg).1 by PARTFUN1:def 6
.= b.(sg.1) by A8,FUNCT_1:13
.= b.u by A6,A9,TARSKI:def 1;
A13: power(L).(xu,b.u) = power(L).[xu,b.u];
A14: for v being object holds v in dom sg implies v in {1}
proof
let v be object;
assume
A15: v in dom sg;
assume
A16: not v in {1};
reconsider v as Element of NAT by A15;
sg/.v = sg.v by A15,PARTFUN1:def 6;
then
A17: sg/.v in rng sg by A15,FUNCT_1:def 3;
A18: v <> 1 by A16,TARSKI:def 1;
A19: 1 < v
proof
consider k being Nat such that
A20: dom sg = Seg k by FINSEQ_1:def 2;
Seg k = {l where l is Nat : 1 <= l & l <= k} by FINSEQ_1:def 1;
then
ex m9 being Nat st m9 = v & 1 <= m9 & m9 <= k by A15,A20;
hence thesis by A18,XXREAL_0:1;
end;
sg/.1 = sg.1 by A7,A15,FINSEQ_3:31,PARTFUN1:def 6;
then sg/.1 in rng sg by A8,FUNCT_1:def 3;
then sg/.1 = u by A6,TARSKI:def 1
.= sg/.v by A6,A17,TARSKI:def 1;
hence thesis by A5,A8,A15,A19,PRE_POLY:def 2;
end;
consider y being FinSequence of the carrier of L such that
A21: len y = (len SgmX(RelIncl n, support b)) and
A22: eval(b,x) = Product y and
A23: for i being Element of NAT st 1 <= i & i <= len y holds y/.i = power
(L).((x * SgmX(RelIncl n, support b))/.i, (b * SgmX(RelIncl n, support b))/.i)
by Def1;
for v being object holds v in {1} implies v in dom sg by A8,TARSKI:def 1;
then dom sg = Seg 1 by A14,FINSEQ_1:2,TARSKI:2;
then
A24: len sg = 1 by FINSEQ_1:def 3;
then y.1 = y/.1 by A21,FINSEQ_4:15
.= power(L).((x * sg)/.1,(b * sg)/.1) by A21,A23,A24;
then y = <* power(L).(x.u,b.u) *> by A21,A24,A12,A11,FINSEQ_1:40;
hence thesis by A22,A13,GROUP_4:9;
end;
Lm4: for n being Ordinal, L being right_zeroed add-associative
right_complementable well-unital distributive non trivial commutative
associative non empty doubleLoopStr,
b1,b2 being bag of n, u being object st not
(u in support b1) & support b2 = support b1 \/ {u} &
for u9 being object st u9 <>
u holds b2.u9 = b1.u9 for x being Function of n, L for a being Element of L st
a = (power(L)).(x.u,b2.u) holds eval(b2,x) = a * eval(b1,x)
proof
let n be Ordinal, L be right_zeroed add-associative right_complementable
well-unital distributive commutative associative non trivial
doubleLoopStr, b1,b2 be bag of n, u be object;
assume that
A1: not u in support b1 and
A2: support b2 = support b1 \/ {u} and
A3: for u9 being object st u9 <> u holds b2.u9 = b1.u9;
u in {u} by TARSKI:def 1;
then
A4: u in support b2 by A2,XBOOLE_0:def 3;
set sb2 = SgmX(RelIncl n, support b2), sb1 = SgmX(RelIncl n, support b1);
let x be Function of n, L;
A5: n = dom x by FUNCT_2:def 1;
let a be Element of L;
assume
A6: a = (power(L)).(x.u,b2.u);
RelIncl n linearly_orders support b2 by PRE_POLY:82;
then u in rng sb2 by A4,PRE_POLY:def 2;
then consider k being Nat such that
A7: k in dom sb2 and
A8: sb2.k = u by FINSEQ_2:10;
A9: sb2/.k = u by A7,A8,PARTFUN1:def 6;
reconsider u as Element of n by A4;
A10: dom sb2 = Seg(len sb2) by FINSEQ_1:def 3;
A11: k <= len sb2 by A7,FINSEQ_3:25;
A12: 1 <= k by A7,A10,FINSEQ_1:1;
then 1 - 1 <= k - 1 by XREAL_1:9;
then reconsider k9 = k - 1 as Element of NAT by INT_1:3;
A13: k9 + 1 = k + 0;
A14: RelIncl n linearly_orders support b1 by PRE_POLY:82;
per cases;
suppose
A15: n = {};
A16: b2 in Bags n by PRE_POLY:def 12;
u in {u} by TARSKI:def 1;
then u in support b2 by A2,XBOOLE_0:def 3;
then
A17: b2.u <> 0 by PRE_POLY:def 7;
Bags n = {EmptyBag n} by A15,PRE_POLY:51;
then b2 = EmptyBag n by A16,TARSKI:def 1;
hence thesis by A17;
end;
suppose
n <> {};
then reconsider n9 = n as non empty Ordinal;
reconsider x9 = x as Function of n9, L;
reconsider b1, b2 as bag of n9;
reconsider sb2, sb1 as FinSequence of n9;
reconsider u as Element of n9;
consider yb2 being FinSequence of the carrier of L such that
A18: len yb2 = len sb2 and
A19: eval(b2,x9) = Product yb2 and
A20: for i being Element of NAT st 1 <= i & i <= len yb2 holds yb2/.i
= power(L).((x * sb2)/.i,(b2 * sb2)/.i) by Def1;
consider yb1 being FinSequence of the carrier of L such that
A21: len yb1 = len sb1 and
A22: eval(b1,x9) = Product yb1 and
A23: for i being Element of NAT st 1 <= i & i <= len yb1 holds yb1/.i
= power(L).((x * sb1)/.i,(b1 * sb1)/.i) by Def1;
set ytmp = Ins(yb1,k9,a);
A24: len sb1 + 1 = (card(support b1) + 1) by PRE_POLY:11,82
.= card(support b2) by A1,A2,CARD_2:41
.= len sb2 by PRE_POLY:11,82;
then
A25: len yb2 = len ytmp by A18,A21,FINSEQ_5:69;
A26: sb2 = Ins(sb1,k9,u) by A1,A2,A7,A9,A13,PRE_POLY:80,82;
A27: for i being Nat st 1 <= i & i <= len yb2 holds yb2.i = ytmp.i
proof
let i be Nat;
assume that
A28: 1 <= i and
A29: i <= len yb2;
A30: i in Seg(len yb2) by A28,A29,FINSEQ_1:1; then
A31: yb2/.i = power(L).((x * Ins(sb1,k9,u))/.i, (b2 * Ins(sb1,k9,u))/.i)
by A26,A20,A28,A29;
A32: i in dom yb2 by A30,FINSEQ_1:def 3;
i in Seg(len ytmp) by A25,A28,A29,FINSEQ_1:1; then
A33: i in dom ytmp by FINSEQ_1:def 3;
A34: 1 - 1 <= i - 1 by A28,XREAL_1:9; then
A35: i - 1 is Element of NAT by INT_1:3;
now
per cases;
case
A36: i = k;
A37: sb2.k in {u} by A8,TARSKI:def 1; then
A38: k in dom(x * sb2) by A5,A7,A8,FUNCT_1:11; then
A39: (x * sb2)/.k = (x * sb2).k by PARTFUN1:def 6
.= x.u by A8,A38,FUNCT_1:12;
A40: support b2 c= dom b2 by PRE_POLY:37;
sb2.k in support b2 by A2,A37,XBOOLE_0:def 3; then
A41: k in dom(b2 * sb2) by A7,A40,FUNCT_1:11;
then (b2 * sb2)/.k = (b2 * sb2).k by PARTFUN1:def 6
.= b2.u by A8,A41,FUNCT_1:12;
then
A42: yb2/.i = power(L).(x.u,b2.u) by A20,A28,A29,A30,A36,A39;
A43: k9 <= len yb1 by A13,A18,A21,A24,A29,A36,XREAL_1:6;
yb2.i = yb2/.i by PARTFUN1:def 6,A32;
hence ytmp.i = yb2.i by A6,A13,A36,A43,A42,FINSEQ_5:73;
end;
case
A44: i <> k;
len(Ins(sb1,k9,u)) = len sb1 + 1 by FINSEQ_5:69;
then
A45: dom(Ins(sb1,k9,u)) = Seg(len(sb1)+1) by FINSEQ_1:def 3;
now
per cases by A44,XXREAL_0:1;
case
A46: i < k;
then
A47: i <= k9 by A13,NAT_1:13;
then
A48: i in Seg k9 by A28,FINSEQ_1:1;
A49: yb1|(Seg k9) is FinSequence by FINSEQ_1:15;
k9 <= len yb1 by A11,A13,A21,A24,XREAL_1:6;
then W: i in dom(yb1|(Seg k9)) by A48,A49,FINSEQ_1:17;
then
A50: i in dom(yb1|k9) by FINSEQ_1:def 16;
A51: sb1|(Seg k9) is FinSequence by FINSEQ_1:15;
A52: rng sb1 c= n by FINSEQ_1:def 4;
A53: i < len yb2 by A11,A18,A46,XXREAL_0:2;
then
A54: i <= len yb1 by A18,A21,A24,NAT_1:13;
ST: i in dom yb1 by W,RELAT_1:57;
i <= len sb1 by A18,A24,A53,NAT_1:13;
then
A55: i in dom sb1 by FINSEQ_3:25,A28;
then
A56: sb1.i in rng sb1 by FUNCT_1:def 3;
then
A57: i in dom(x * sb1) by A5,A55,A52,FUNCT_1:11;
A58: now
assume sb1.i = u;
then u in rng sb1 by A55,FUNCT_1:def 3;
hence contradiction by A1,A14,PRE_POLY:def 2;
end;
A59: k - 1 <= (len sb1 + 1) - 1 by A11,A24,XREAL_1:9;
A60: rng Ins(sb1,k9,u) c= n by FINSEQ_1:def 4;
sb1.i in n by A56,A52;
then sb1.i in dom b1 by PARTFUN1:def 2;
then
A61: i in dom(b1 * sb1) by A55,FUNCT_1:11;
i in Seg k9 by A28,A47,FINSEQ_1:1;
then i in dom(sb1|(Seg k9)) by A59,A51,FINSEQ_1:17;
then
A62: i in dom(sb1|k9) by FINSEQ_1:def 16;
i <= len sb1 + 1 by A11,A24,A46,XXREAL_0:2;
then
A63: i in dom(Ins(sb1,k9,u)) by A28,A45,FINSEQ_1:1;
then
A64: Ins(sb1,k9,u).i in rng Ins(sb1,k9,u) by FUNCT_1:def 3;
then
A65: i in dom(x * Ins(sb1,k9,u)) by A5,A63,A60,FUNCT_1:11;
then
A66: (x * Ins(sb1,k9,u))/.i = (x * Ins(sb1,k9,u)).i by PARTFUN1:def 6
.= x.(Ins(sb1,k9,u).i) by A65,FUNCT_1:12
.= x.(sb1.i) by A62,FINSEQ_5:72
.= (x * sb1).i by A57,FUNCT_1:12
.= (x * sb1)/.i by A57,PARTFUN1:def 6;
dom b2 = n by PARTFUN1:def 2;
then
A67: i in dom(b2 * Ins(sb1,k9,u)) by A63,A64,A60,FUNCT_1:11;
then (b2 * Ins(sb1,k9,u))/.i = (b2 * Ins(sb1,k9,u)).i by
PARTFUN1:def 6
.= b2.(Ins(sb1,k9,u).i) by A67,FUNCT_1:12
.= b2.(sb1.i) by A62,FINSEQ_5:72
.= b1.(sb1.i) by A3,A58
.= (b1 * sb1).i by A61,FUNCT_1:12
.= (b1 * sb1)/.i by A61,PARTFUN1:def 6;
then
A68: yb2/.i = yb1/.i by A23,A28,A30,A31,A54,A66
.= yb1.i by PARTFUN1:def 6,ST
.= ytmp.i by A50,FINSEQ_5:72
.= ytmp/.i by A33,PARTFUN1:def 6;
thus yb2.i = yb2/.i by A32,PARTFUN1:def 6
.= ytmp.i by A33,A68,PARTFUN1:def 6;
end;
case
A69: i > k;
reconsider i1 = i - 1 as Element of NAT by A34,INT_1:3;
A70: (i - 1) + 1 = i + 0;
A71: rng sb1 c= n by FINSEQ_1:def 4;
A72: i - 1 <= len sb2 - 1 by A18,A29,XREAL_1:9;
1 < i by A12,A69,XXREAL_0:2;
then
A73: 1 <= i - 1 by A35,A70,NAT_1:13;
then i1 in Seg len sb1 by A24,A72,FINSEQ_1:1;
then
A74: i1 in dom sb1 by FINSEQ_1:def 3;
then
A75: sb1.i1 in rng sb1 by FUNCT_1:def 3;
then
A76: i1 in dom(x * sb1) by A5,A74,A71,FUNCT_1:11;
dom b1 = n by PARTFUN1:def 2;
then
A77: i1 in dom(b1 * sb1) by A74,A75,A71,FUNCT_1:11;
A78: now
assume sb1/.i1 = u;
then sb1.i1 = u by A74,PARTFUN1:def 6;
then u in rng sb1 by A74,FUNCT_1:def 3;
hence contradiction by A1,A14,PRE_POLY:def 2;
end;
A79: i = i1 + 1;
A80: rng Ins(sb1,k9,u) c= n by FINSEQ_1:def 4;
A81: i1 + 1 = i + 0;
then
A82: k9 + 1 <= i1 by A69,NAT_1:13;
A83: i in dom(Ins(sb1,k9,u)) by A18,A24,A28,A29,A45,FINSEQ_1:1;
then
A84: Ins(sb1,k9,u).i in rng Ins(sb1,k9,u) by FUNCT_1:def 3;
then
A85: i in dom(x * Ins(sb1,k9,u)) by A5,A83,A80,FUNCT_1:11;
then
A86: (x * Ins(sb1,k9,u))/.i = (x * Ins(sb1,k9,u)).i by PARTFUN1:def 6
.= x.(Ins(sb1,k9,u).i) by A85,FUNCT_1:12
.= x.(sb1.i1) by A24,A72,A81,A82,FINSEQ_5:74
.= (x * sb1).i1 by A76,FUNCT_1:12
.= (x * sb1)/.i1 by A76,PARTFUN1:def 6;
W1: 1 <= i1 by A73;
i1 <= len sb1 by A74,FINSEQ_3:25; then
i1 <= len yb1 by A21; then
Ze: i1 in dom yb1 by W1,FINSEQ_3:25;
dom b2 = n by PARTFUN1:def 2;
then
A87: i in dom(b2 * Ins(sb1,k9,u)) by A83,A84,A80,FUNCT_1:11;
then (b2 * Ins(sb1,k9,u))/.i = (b2 * Ins(sb1,k9,u)).i by
PARTFUN1:def 6
.= b2.(Ins(sb1,k9,u).i) by A87,FUNCT_1:12
.= b2.(sb1.i1) by A24,A72,A81,A82,FINSEQ_5:74
.= b2.(sb1/.i1) by A74,PARTFUN1:def 6
.= b1.(sb1/.i1) by A3,A78
.= b1.(sb1.i1) by A74,PARTFUN1:def 6
.= (b1 * sb1).i1 by A77,FUNCT_1:12
.= (b1 * sb1)/.i1 by A77,PARTFUN1:def 6;
then
A88: yb2/.i = yb1/.i1 by A21,A23,A24,A31,A73,A72,A86
.= yb1.i1 by Ze,PARTFUN1:def 6
.= ytmp.i by A21,A24,A72,A79,A82,FINSEQ_5:74
.= ytmp/.i by A33,PARTFUN1:def 6;
thus yb2.i = yb2/.i by A32,PARTFUN1:def 6
.= ytmp.i by A33,A88,PARTFUN1:def 6;
end;
end;
hence thesis;
end;
end;
hence thesis;
end;
Product((yb1|k9)^<*a*>^(yb1/^k9)) = Product((yb1|k9)^<*a*>) * Product
(yb1/^k9) by GROUP_4:5
.= (Product(yb1|k9) * Product(<*a*>)) * Product(yb1/^k9) by GROUP_4:5
.= (Product(yb1|k9) * Product(yb1/^k9)) * Product(<*a*>) by GROUP_1:def 3
.= Product((yb1|k9)^(yb1/^k9)) * Product(<*a*>) by GROUP_4:5
.= Product(yb1) * Product(<*a*>) by RFINSEQ:8
.= eval(b1,x9) * a by A22,GROUP_4:9;
then Product ytmp = eval(b1,x9) * a by FINSEQ_5:def 4;
hence thesis by A19,A25,A27,FINSEQ_1:14;
end;
end;
Lm5: for n being Ordinal, L being right_zeroed add-associative
right_complementable Abelian well-unital distributive non trivial commutative
associative non empty doubleLoopStr, b1 being bag of n st (ex u being set st
support b1 = {u}) for b2 being bag of n, x being Function of n, L holds eval(b1
+b2,x) = eval(b1,x) * eval(b2,x)
proof
let n be Ordinal, L be right_zeroed add-associative right_complementable
well-unital distributive Abelian commutative associative non trivial
doubleLoopStr, b1 be bag of n;
assume ex u being set st support b1 = {u};
then consider u being set such that
A1: support b1 = {u};
let b2 be bag of n, x be Function of n, L;
A2: support(b1+b2) = support b2 \/ {u} by A1,PRE_POLY:38;
A3: for u9 being object st u9 <> u holds (b1+b2).u9 = b2.u9
proof
let u9 be object;
assume u9 <> u;
then
A4: not u9 in support b1 by A1,TARSKI:def 1;
thus (b1+b2).u9 = b1.u9 + b2.u9 by PRE_POLY:def 5
.= 0 + b2.u9 by A4,PRE_POLY:def 7
.= b2.u9;
end;
set sb2 = SgmX(RelIncl n, support b2),
sb1b2 = SgmX(RelIncl n, support (b1+b2));
A5: n c= dom x by FUNCT_2:def 1;
A6: RelIncl n linearly_orders support b2 by PRE_POLY:82;
consider yb1b2 being FinSequence of the carrier of L such that
A7: len yb1b2 = len sb1b2 and
A8: eval(b1+b2,x) = Product yb1b2 and
A9: for i being Element of NAT st 1 <= i & i <= len yb1b2 holds yb1b2/.i
= power(L).((x * sb1b2)/.i,((b1+b2) * sb1b2)/.i) by Def1;
consider yb2 being FinSequence of the carrier of L such that
A10: len yb2 = len sb2 and
A11: eval(b2,x) = Product yb2 and
A12: for i being Element of NAT st 1 <= i & i <= len yb2 holds yb2/.i =
power(L).((x * sb2)/.i,(b2 * sb2)/.i) by Def1;
per cases;
suppose
A13: u in support b2;
consider sb2k being Nat such that
A14: dom sb2 = Seg sb2k by FINSEQ_1:def 2;
A15: for v being object holds v in support b2 implies v in support(b1+b2)
proof
let v be object;
assume
A16: v in support b2;
now
per cases;
case
u = v;
then v in {u} by TARSKI:def 1;
hence thesis by A2,XBOOLE_0:def 3;
end;
case
u <> v;
then (b1+b2).v = b2.v by A3;
then (b1+b2).v <> 0 by A16,PRE_POLY:def 7;
hence thesis by PRE_POLY:def 7;
end;
end;
hence thesis;
end;
A17: for v being object holds v in support(b1+b2) implies v in support b2
proof
let v be object;
assume
A18: v in support(b1+b2);
now
per cases by A2,A18,XBOOLE_0:def 3;
case
v in {u};
hence thesis by A13,TARSKI:def 1;
end;
case
v in support b2;
hence thesis;
end;
end;
hence thesis;
end;
then
A19: len yb1b2 = len yb2 by A7,A10,A15,TARSKI:2;
A20: support(b1+b2) = support b2 by A17,A15,TARSKI:2;
u in rng sb2 by A6,A13,PRE_POLY:def 2;
then consider k being Nat such that
A21: k in dom sb2 and
A22: sb2.k = u by FINSEQ_2:10;
reconsider k as Element of NAT by ORDINAL1:def 12;
A23: 1 <= k by A21,A14,FINSEQ_1:1;
A24: support b2 c= dom b2 by PRE_POLY:37;
then
A25: k in dom(b2 * sb2) by A13,A21,A22,FUNCT_1:11;
then
(b2 * sb2)/.k = (b2 * sb2).k by PARTFUN1:def 6;
then
A26: (b2 * sb2)/.k = b2.u by A22,A25,FUNCT_1:12;
A27: rng x c= the carrier of L by RELAT_1:def 19;
consider sb1b2k being Nat such that
A28: dom sb1b2 = Seg sb1b2k by FINSEQ_1:def 2;
support(b1+b2) c= dom(b1+b2) by PRE_POLY:37;
then
A29: k in dom((b1+b2) * sb2) by A13,A20,A21,A22,FUNCT_1:11;
then
A30: ((b1+b2) * sb2)/.k = ((b1+b2) * sb2).k by PARTFUN1:def 6
.= (b1+b2).u by A22,A29,FUNCT_1:12;
consider i being Nat such that
A31: dom yb2 = Seg i by FINSEQ_1:def 2;
reconsider sb2k,sb1b2k as Element of NAT by ORDINAL1:def 12;
A32: k <= sb2k by A21,A14,FINSEQ_1:1;
i in NAT by ORDINAL1:def 12;
then
A33: len yb2 = i by A31,FINSEQ_1:def 3;
A34: sb2k = len yb2 by A10,A14,FINSEQ_1:def 3;
then
A35: k in dom yb2 by A21,A14,FINSEQ_1:def 3;
reconsider bbS = b2*sb2 as PartFunc of NAT,NAT;
A36: sb2k = len sb2 by A14,FINSEQ_1:def 3
.= len sb1b2 by A17,A15,TARSKI:2
.= sb1b2k by A28,FINSEQ_1:def 3;
then len yb1b2 = sb2k by A7,A28,FINSEQ_1:def 3;
then
A37: yb1b2/.k = power(L).((x * sb2)/.k,((b1+b2) * sb2)/.k) by A9,A20,A23,A32
.= power(L).((x * sb2)/.k,b1.u + b2.u) by A30,PRE_POLY:def 5
.= power(L).((x * sb2)/.k,b1.u) * power(L).((x * sb2)/.k,bbS/.k)
by A26,Th1
.= power(L).((x * sb2)/.k,b1.u) * yb2/.k by A12,A23,A32,A34;
A38: dom(b1+b2) = n by PARTFUN1:def 2;
A39: for i9 being Element of NAT st i9 in dom yb2 & i9 <> k holds yb1b2/.
i9 = yb2/.i9
proof
rng(sb1b2) c= dom b2 by A6,A20,A24,PRE_POLY:def 2;
then
A40: rng(sb1b2) c= n by PARTFUN1:def 2;
A41: rng(sb2) c= dom b2 by A6,A24,PRE_POLY:def 2;
let i9 be Element of NAT;
assume that
A42: i9 in dom yb2 and
A43: i9 <> k;
A44: 1 <= i9 by A31,A42,FINSEQ_1:1;
A45: i9 in dom sb2 by A10,A31,A33,A42,FINSEQ_1:def 3;
then sb2.i9 in rng(sb2) by FUNCT_1:def 3;
then
A46: i9 in dom(b2 * sb2) by A45,A41,FUNCT_1:11;
then
A47: (b2 * sb2)/.i9 = (b2 * sb2).i9 by PARTFUN1:def 6
.= b2.(sb2.i9) by A46,FUNCT_1:12
.= b2.(sb2/.i9) by A45,PARTFUN1:def 6;
A48: i9 <= len yb2 by A31,A33,A42,FINSEQ_1:1;
A49: i9 in Seg sb1b2k by A36,A34,A42,FINSEQ_1:def 3;
A50: sb1b2/.i9 <> u
proof
assume sb1b2/.i9 = u;
then
A51: sb1b2.i9 = u by A28,A49,PARTFUN1:def 6;
A52: sb1b2 is one-to-one by PRE_POLY:10,82;
sb1b2.k = u by A17,A15,A22,TARSKI:2;
hence thesis by A21,A14,A28,A36,A43,A49,A51,A52,FUNCT_1:def 4;
end;
sb1b2.i9 in rng(sb1b2) by A28,A49,FUNCT_1:def 3;
then
A53: i9 in dom((b1+b2) * sb1b2) by A28,A38,A49,A40,FUNCT_1:11;
then ((b1+b2) * sb1b2)/.i9 = ((b1+b2) * sb1b2).i9 by PARTFUN1:def 6
.= (b1+b2).(sb1b2.i9) by A53,FUNCT_1:12
.= (b1+b2).(sb1b2/.i9) by A28,A49,PARTFUN1:def 6;
hence yb1b2/.i9 = power(L).((x * sb1b2)/.i9,(b1+b2).(sb1b2/.i9)) by A9
,A19,A44,A48
.= power(L).((x * sb2)/.i9,b2.(sb2/.i9)) by A3,A20,A50
.= yb2/.i9 by A12,A44,A48,A47;
end;
A54: support b1 c= dom b1 by PRE_POLY:37;
u in support b1 by A1,TARSKI:def 1;
then
A55: u in dom b1 by A54;
A56: dom b1 = n by PARTFUN1:def 2;
then x.u in rng x by A5,A55,FUNCT_1:def 3;
then reconsider xu = x.u as Element of L by A27;
consider a being Element of L such that
A57: a = (power(L)).(xu,b1.u);
A58: k in dom (x * sb2) by A5,A21,A22,A55,A56,FUNCT_1:11;
then (x * sb2).k = x.(sb2.k) by FUNCT_1:12;
then yb1b2/.k = a * yb2/.k by A22,A37,A57,A58,PARTFUN1:def 6;
hence eval(b1+b2,x) = a * Product yb2 by A8,A19,A35,A39,Th5
.= eval(b1,x) * eval(b2,x) by A1,A11,A57,Th7;
end;
suppose
A59: not u in support b2;
A60: support b1 c= dom b1 by PRE_POLY:37;
u in support b1 by A1,TARSKI:def 1;
then
A61: u in dom b1 by A60;
A62: rng x c= the carrier of L by RELAT_1:def 19;
dom b1 = n by PARTFUN1:def 2;
then x.u in rng x by A5,A61,FUNCT_1:def 3;
then reconsider xu = x.u as Element of L by A62;
consider a being Element of L such that
A63: a = (power(L)).(xu,(b1+b2).u);
A64: (b1+b2).u = b1.u + b2.u by PRE_POLY:def 5
.= b1.u + 0 by A59,PRE_POLY:def 7;
thus eval(b1+b2,x) = a * eval(b2,x) by A3,A2,A59,A63,Lm4
.= eval(b1,x) * eval(b2,x) by A1,A64,A63,Th7;
end;
end;
theorem Th8:
for n being Ordinal, L being right_zeroed add-associative
right_complementable well-unital distributive Abelian non trivial commutative
associative non empty doubleLoopStr, b1,b2 being bag of n, x being Function
of n, L holds eval(b1+b2,x) = eval(b1,x) * eval(b2,x)
proof
let n be Ordinal, L be right_zeroed add-associative right_complementable
well-unital distributive Abelian commutative associative non trivial
doubleLoopStr, b1,b2 be bag of n, x be Function of n, L;
defpred P[Nat] means for b1 being bag of n st card(support b1) =
$1 holds eval(b1+b2,x) = eval(b1,x) * eval(b2,x);
A1: ex k being Element of NAT st card(support b1) = k;
A2: for k being Nat st P[k] holds P[k + 1]
proof
let k be Nat;
assume
A3: P[k];
let b1 be bag of n;
assume
A4: card(support b1) = k + 1;
set sgb1 = SgmX(RelIncl n, support b1);
set bg = sgb1/.(len sgb1);
A5: RelIncl n linearly_orders support b1 by PRE_POLY:82;
then sgb1 <> {} by A4,CARD_1:27,PRE_POLY:def 2,RELAT_1:38;
then 1 <= len sgb1 by NAT_1:14;
then len sgb1 in Seg(len sgb1) by FINSEQ_1:1;
then
A6: len sgb1 in dom sgb1 by FINSEQ_1:def 3;
then sgb1/.(len sgb1) = sgb1.(len sgb1) by PARTFUN1:def 6;
then bg in rng sgb1 by A6,FUNCT_1:def 3;
then
A7: bg in support b1 by A5,PRE_POLY:def 2;
set b19 = b1+*(bg,0);
support b1 c= dom b1 by PRE_POLY:37;
then
A8: b19 = b1+*(bg.-->0) by A7,FUNCT_7:def 3;
A9: for u being object holds u in support b1 implies u in support b19 \/ {bg }
proof
let u be object;
assume u in support b1;
then
A10: b1.u <> 0 by PRE_POLY:def 7;
per cases;
suppose
u = bg;
then u in {bg} by TARSKI:def 1;
hence thesis by XBOOLE_0:def 3;
end;
suppose
u <> bg;
then not u in {bg} by TARSKI:def 1;
then not u in dom(bg.-->0);
then b19.u = b1.u by A8,FUNCT_4:11;
then u in support b19 by A10,PRE_POLY:def 7;
hence thesis by XBOOLE_0:def 3;
end;
end;
bg in {bg} by TARSKI:def 1;
then bg in dom(bg.-->0);
then b19.bg = (bg.-->0).bg by A8,FUNCT_4:13;
then
A11: b19.bg = 0 by FUNCOP_1:72;
then
A12: not bg in support b19 by PRE_POLY:def 7;
for u being object holds u in support b19 \/ {bg} implies u in support b1
proof
let u be object;
assume
A13: u in support b19 \/ {bg};
per cases by A13,XBOOLE_0:def 3;
suppose
A14: u in support b19;
then u <> bg by A11,PRE_POLY:def 7;
then not u in {bg} by TARSKI:def 1;
then not u in dom(bg.-->0);
then
A15: b19.u = b1.u by A8,FUNCT_4:11;
b19.u <> 0 by A14,PRE_POLY:def 7;
hence thesis by A15,PRE_POLY:def 7;
end;
suppose
u in {bg};
hence thesis by A7,TARSKI:def 1;
end;
end;
then support b1 = support b19 \/ {bg} by A9,TARSKI:2;
then
A16: k + 1 = card(support b19) + 1 by A4,A12,CARD_2:41;
set m = (EmptyBag n)+*(bg,b1.bg);
A17: dom b1 = n by PARTFUN1:def 2;
dom(EmptyBag n) = n by PARTFUN1:def 2;
then
A18: m = (EmptyBag n)+*(bg.-->b1.bg) by A7,FUNCT_7:def 3;
A19: for u being object holds u in support m implies u in {bg}
proof
let u be object;
assume u in support m;
then
A20: m.u <> 0 by PRE_POLY:def 7;
now
assume u <> bg;
then not u in {bg} by TARSKI:def 1;
then not u in dom(bg.-->b1.bg);
then m.u = (EmptyBag n).u by A18,FUNCT_4:11;
hence contradiction by A20;
end;
hence thesis by TARSKI:def 1;
end;
A21: b1.bg <> 0 by A7,PRE_POLY:def 7;
for u being object holds u in {bg} implies u in support m
proof
let u be object;
bg in {bg} by TARSKI:def 1;
then bg in dom(bg.-->b1.bg);
then m.bg = (bg.-->b1.bg).bg by A18,FUNCT_4:13;
then
A22: m.bg = b1.bg by FUNCOP_1:72;
assume u in {bg};
then u = bg by TARSKI:def 1;
hence thesis by A21,A22,PRE_POLY:def 7;
end;
then
A23: support m = {bg} by A19,TARSKI:2;
A24: for u being object st u in n holds (b19+m).u = b1.u
proof
let u be object;
assume u in n;
per cases;
suppose
A25: u = bg;
bg in {bg} by TARSKI:def 1;
then bg in dom(bg.-->b1.bg);
then m.bg = (bg.-->b1.bg).bg by A18,FUNCT_4:13;
then
A26: m.bg = b1.bg by FUNCOP_1:72;
u in {bg} by A25,TARSKI:def 1;
then u in dom(bg.-->0);
then
A27: b19.u = (bg.-->0).bg by A8,A25,FUNCT_4:13;
(b19+m).u = b19.u + m.u by PRE_POLY:def 5
.= 0 + b1.bg by A25,A27,A26,FUNCOP_1:72
.= b1.bg;
hence thesis by A25;
end;
suppose
u <> bg;
then
A28: not u in {bg} by TARSKI:def 1;
then
A29: not u in dom(bg.-->0);
not u in dom(bg.-->b1.bg) by A28;
then m.u = (EmptyBag n).u by A18,FUNCT_4:11;
then
A30: m.u = 0;
(b19+m).u = b19.u + m.u by PRE_POLY:def 5
.= b1.u by A8,A29,A30,FUNCT_4:11;
hence thesis;
end;
end;
A31: dom(b19 + m) = n by PARTFUN1:def 2;
then eval(b1,x) = eval(m+b19,x) by A17,A24,FUNCT_1:2
.= eval(b19,x) * eval(m,x) by A23,Lm5;
hence eval(b1,x) * eval(b2,x) = (eval(b19,x) * eval(b2,x)) * eval(m,x) by
GROUP_1:def 3
.= eval(b19+b2,x) * eval(m,x) by A3,A16
.= eval(m+(b19+b2),x) by A23,Lm5
.= eval((b19+m)+b2,x) by PRE_POLY:35
.= eval(b1+b2,x) by A31,A17,A24,FUNCT_1:2;
end;
A32: P[0]
proof
let b1 be bag of n;
assume card(support b1) = 0;
then support b1 = {};
then
A33: b1 = EmptyBag n by PRE_POLY:81;
hence eval(b1+b2,x) = 1.L * eval(b2,x) by PRE_POLY:53
.= eval(b1,x) * eval(b2,x) by A33,Th6;
end;
for k being Nat holds P[k] from NAT_1:sch 2(A32,A2);
hence thesis by A1;
end;
begin :: Evaluation of Polynomials ------------------------------------------------
registration
let n be Ordinal, L be add-associative right_zeroed right_complementable
non empty addLoopStr, p,q be Polynomial of n, L;
cluster p - q -> finite-Support;
coherence
proof
p - q = p + (-q) by POLYNOM1:def 7;
hence thesis;
end;
end;
theorem Th9:
for L being right_zeroed add-associative right_complementable
well-unital distributive non trivial doubleLoopStr, n being Ordinal
, p being Polynomial of n,L st Support p = {} holds p = 0_(n,L)
proof
let L be right_zeroed add-associative right_complementable well-unital
distributive non trivial doubleLoopStr, n be Ordinal, p be
Polynomial of n,L such that
A1: Support p = {};
A2: for u being object st u in Bags n holds p.u = 0_(n,L).u
proof
let u be object;
assume
A3: u in Bags n;
then reconsider b = u as bag of n;
p.b = 0.L by A1,A3,POLYNOM1:def 4;
hence thesis by POLYNOM1:22;
end;
A4: Bags n = dom 0_(n,L) by FUNCT_2:def 1;
Bags n = dom p by FUNCT_2:def 1;
hence thesis by A4,A2,FUNCT_1:2;
end;
registration
let n be Ordinal, L be right_zeroed add-associative right_complementable
well-unital distributive non trivial doubleLoopStr, p be Polynomial
of n,L;
cluster Support p -> finite;
coherence by POLYNOM1:def 5;
end;
theorem Th10:
for n being Ordinal, L being right_zeroed add-associative
right_complementable well-unital distributive non trivial
doubleLoopStr, p being Polynomial of n,L holds BagOrder n linearly_orders
Support p
proof
let n be Ordinal, L be right_zeroed add-associative right_complementable
well-unital distributive non trivial doubleLoopStr, p be Polynomial
of n,L;
set R = BagOrder n;
R is connected by ORDERS_1:def 6;
then
A1: R is_connected_in field R by RELAT_2:def 14;
for x being object holds x in Bags n implies x in field R
proof
let x be object;
assume x in Bags n;
then reconsider x as bag of n;
EmptyBag n <=' x by PRE_POLY:60;
then [EmptyBag n, x] in R by PRE_POLY:def 14;
then
A2: x in rng R by XTUPLE_0:def 13;
field R = dom R \/ rng R by RELAT_1:def 6;
then rng R c= field R by XBOOLE_1:7;
hence thesis by A2;
end;
then
A3: Bags n c= field R by TARSKI:def 3;
then [:Bags n, Bags n:] c= [:field R, field R:] by ZFMISC_1:96;
then reconsider R9 = R as Relation of field R by XBOOLE_1:1;
R is_reflexive_in field R by RELAT_2:def 9;
then dom R9 = field R by ORDERS_1:13;
then
A4: R9 is total by PARTFUN1:def 2;
Support p c= field R by A3,XBOOLE_1:1;
then
A5: R9 is_connected_in Support p by A1,A4,Lm2;
A6: R is_antisymmetric_in Support p by Lm1;
A7: R is_transitive_in Support p by Lm1;
R is_reflexive_in Support p by Lm1;
hence thesis by A6,A7,A5,ORDERS_1:def 9;
end;
definition
::$CD
let n be Ordinal, L be right_zeroed add-associative right_complementable
well-unital distributive non trivial doubleLoopStr, p be Polynomial
of n,L, x be Function of n, L;
func eval(p,x) -> Element of L means
:Def2:
ex y being FinSequence of the
carrier of L st len y = len SgmX(BagOrder n, Support p) & it = Sum y & for i
being Element of NAT st 1 <= i & i <= len y holds y/.i = (p * SgmX(BagOrder n,
Support p))/.i * eval(((SgmX(BagOrder n, Support p))/.i),x);
existence
proof
set S = SgmX(BagOrder n, Support p);
set l = len S;
defpred P[Nat,Element of L] means $2 = (p * S)/.($1) * eval((S
/.($1)),x);
A1: for k being Nat st k in Seg l ex x being Element of L st P[
k,x];
consider q being FinSequence of the carrier of L such that
A2: dom q = Seg l & for m being Nat st m in Seg l holds P[m
,q/.m] from RECDEF_1:sch 17(A1 );
take Sum q;
A3: len q = l by A2,FINSEQ_1:def 3;
for m being Element of NAT st 1<= m & m <= len q
holds q/.m = (p * SgmX(BagOrder n, Support p))/.m * eval(((SgmX(BagOrder
n, Support p))/.m),x) by A2,A3,FINSEQ_1:1;
hence thesis by A3;
end;
uniqueness
proof
let a,c be Element of L;
assume that
A4: ex y1 being FinSequence of the carrier of L st len y1 = len SgmX(
BagOrder n, Support p) & a = Sum y1 & for i being Element of NAT st 1 <= i & i
<= len y1 holds y1/.i = (p * SgmX(BagOrder n, Support p))/.i * eval(((SgmX(
BagOrder n, Support p))/.i),x) and
A5: ex y2 being FinSequence of the carrier of L st len y2 = len SgmX(
BagOrder n, Support p) & c = Sum y2 & for i being Element of NAT st 1 <= i & i
<= len y2 holds y2/.i = (p * SgmX(BagOrder n, Support p))/.i * eval(((SgmX(
BagOrder n, Support p))/.i),x);
consider y1 being FinSequence of the carrier of L such that
A6: len y1 = len SgmX(BagOrder n, Support p) and
A7: a = Sum y1 and
A8: for i being Element of NAT st 1 <= i & i <= len y1 holds y1/.i =
(p * SgmX(BagOrder n, Support p))/.i * eval(((SgmX(BagOrder n, Support p))/.i)
,x) by A4;
consider y2 being FinSequence of the carrier of L such that
A9: len y2 = len SgmX(BagOrder n, Support p) and
A10: c = Sum y2 and
A11: for i being Element of NAT st 1 <= i & i <= len y2 holds y2/.i =
(p * SgmX(BagOrder n, Support p))/.i * eval(((SgmX(BagOrder n, Support p))/.i)
,x) by A5;
for k being Nat st 1 <= k & k <= len y1 holds y1.k = y2.k
proof
let k be Nat;
assume that
A12: 1 <= k and
A13: k <= len y1;
k in Seg(len y2) by A6,A9,A12,A13,FINSEQ_1:1;
then
A14: k in dom y2 by FINSEQ_1:def 3;
A15: k in Seg(len y1) by A12,A13,FINSEQ_1:1;
then k in dom y1 by FINSEQ_1:def 3;
hence y1.k = y1/.k by PARTFUN1:def 6
.= (p * SgmX(BagOrder n, Support p))/.k * eval(((SgmX(BagOrder n,
Support p))/.k),x) by A8,A12,A13,A15
.= y2/.k by A6,A9,A11,A12,A13,A15
.= y2.k by A14,PARTFUN1:def 6;
end;
hence thesis by A6,A7,A9,A10,FINSEQ_1:14;
end;
end;
theorem Th11:
for n being Ordinal, L being right_zeroed add-associative
right_complementable well-unital distributive non trivial
doubleLoopStr, p being Polynomial of n,L, b being bag of n st Support p = {b}
for x being Function of n, L holds eval(p,x) = p.b * eval(b,x)
proof
let n be Ordinal, L be right_zeroed add-associative right_complementable
well-unital distributive non trivial doubleLoopStr, p be Polynomial
of n,L, b be bag of n;
reconsider sp = Support p as finite Subset of Bags n;
set sg = SgmX(BagOrder n, sp);
A1: b in Bags n by PRE_POLY:def 12;
A2: dom p = Bags n by FUNCT_2:def 1;
A3: BagOrder n linearly_orders sp by Th10;
assume Support p = {b};
then
A4: rng sg = {b} by A3,PRE_POLY:def 2;
then
A5: b in rng sg by TARSKI:def 1;
then
A6: 1 in dom sg by FINSEQ_3:31;
then
A7: sg/.1 = sg.1 by PARTFUN1:def 6;
A8: for u being object holds u in dom sg implies u in {1}
proof
let u be object;
assume
A9: u in dom sg;
assume
A10: not u in {1};
reconsider u as Element of NAT by A9;
sg/.u = sg.u by A9,PARTFUN1:def 6;
then
A11: sg/.u in rng sg by A9,FUNCT_1:def 3;
A12: u <> 1 by A10,TARSKI:def 1;
A13: 1 < u
proof
consider k being Nat such that
A14: dom sg = Seg k by FINSEQ_1:def 2;
Seg k = {l where l is Nat : 1 <= l & l <= k} by FINSEQ_1:def 1;
then
ex m9 being Nat st m9 = u & 1 <= m9 & m9 <= k by A9,A14;
hence thesis by A12,XXREAL_0:1;
end;
sg/.1 = sg.1 by A5,A9,FINSEQ_3:31,PARTFUN1:def 6;
then sg/.1 in rng sg by A6,FUNCT_1:def 3;
then sg/.1 = b by A4,TARSKI:def 1
.= sg/.u by A4,A11,TARSKI:def 1;
hence thesis by A3,A6,A9,A13,PRE_POLY:def 2;
end;
for u being object holds u in {1} implies u in dom sg by A6,TARSKI:def 1;
then
A15: dom sg = Seg 1 by A8,FINSEQ_1:2,TARSKI:2;
then
A16: len sg = 1 by FINSEQ_1:def 3;
A17: sg.1 in rng sg by A6,FUNCT_1:def 3;
then sg.1 = b by A4,TARSKI:def 1;
then 1 in dom (p * sg) by A6,A1,A2,FUNCT_1:11;
then
A18: (p * sg)/.1 = (p * sg).1 by PARTFUN1:def 6
.= p.(sg.1) by A6,FUNCT_1:13
.= p.b by A4,A17,TARSKI:def 1;
1 in dom sg by A15,FINSEQ_1:2,TARSKI:def 1;
then
A19: sg/.1 in rng sg by A7,FUNCT_1:def 3;
let x be Function of n, L;
consider y being FinSequence of the carrier of L such that
A20: len y = len SgmX(BagOrder n, Support p) and
A21: eval(p,x) = Sum y and
A22: for i being Element of NAT st 1 <= i & i <= len y holds y/.i = (p *
SgmX(BagOrder n, Support p))/.i * eval(((SgmX(BagOrder n, Support p))/.i),x)
by Def2;
y.1 = y/.1 by A20,A16,FINSEQ_4:15
.= (p * sg)/.1 * eval((sg/.1),x) by A20,A22,A16
.= (p * sg)/.1 * eval(b,x) by A4,A19,TARSKI:def 1;
then y = <* p.b * eval(b,x) *> by A20,A16,A18,FINSEQ_1:40;
hence thesis by A21,RLVECT_1:44;
end;
theorem Th12:
for n being Ordinal, L being right_zeroed add-associative
right_complementable well-unital distributive non trivial
doubleLoopStr, x being Function of n, L holds eval(0_(n,L),x) = 0.L
proof
let n be Ordinal, L be right_zeroed add-associative right_complementable
well-unital distributive non trivial doubleLoopStr, x be Function
of n, L;
set 0p = 0_(n,L);
consider y being FinSequence of the carrier of L such that
A1: len y = len SgmX(BagOrder n, Support 0p) and
A2: Sum y = eval(0p,x) and
for i being Element of NAT st 1 <= i & i <= len y holds y/.i = (0p *
SgmX(BagOrder n, Support 0p))/.i * eval(((SgmX(BagOrder n, Support 0p))/.i),x)
by Def2;
Support 0p = {}
proof
set u = the Element of Support 0p;
assume Support 0p <> {};
then
A3: u in Support 0p;
then
A4: u is Element of Bags n;
0p.u <> 0.L by A3,POLYNOM1:def 4;
hence thesis by A4,POLYNOM1:22;
end;
then SgmX(BagOrder n, Support 0p) = {} by Th10,PRE_POLY:76;
then y = <*>the carrier of L by A1;
hence thesis by A2,RLVECT_1:43;
end;
theorem Th13:
for n being Ordinal, L being right_zeroed add-associative
right_complementable well-unital distributive non trivial
doubleLoopStr, x being Function of n, L holds eval(1_(n,L),x) = 1.L
proof
let n be Ordinal, L be right_zeroed add-associative right_complementable
well-unital distributive non trivial doubleLoopStr, x be Function
of n, L;
set 1p = 1_(n,L);
A1: for u being object holds u in {EmptyBag n} implies u in Support 1p
proof
let u be object;
assume
A2: u in {EmptyBag n};
then
A3: u = EmptyBag n by TARSKI:def 1;
reconsider u as Element of Bags n by A2,TARSKI:def 1;
1p.u = 1.L by A3,POLYNOM1:25;
then 1p.u <> 0.L;
hence thesis by POLYNOM1:def 4;
end;
reconsider s1p = Support 1p as finite Subset of Bags n;
set sg1p = SgmX(BagOrder n, s1p);
A4: BagOrder n linearly_orders Support 1p by Th10;
for u being object holds u in Support 1p implies u in {EmptyBag n}
proof
let u be object;
assume
A5: u in Support 1p;
then reconsider u as Element of Bags n;
1p.u <> 0.L by A5,POLYNOM1:def 4;
then u = EmptyBag n by POLYNOM1:25;
hence thesis by TARSKI:def 1;
end;
then
A6: Support 1p = {EmptyBag n} by A1,TARSKI:2;
then
A7: rng sg1p = {EmptyBag n} by A4,PRE_POLY:def 2;
then
A8: EmptyBag n in rng sg1p by TARSKI:def 1;
then
A9: 1 in dom sg1p by FINSEQ_3:31;
then sg1p/.1 = sg1p.1 by PARTFUN1:def 6;
then sg1p/.1 in rng sg1p by A9,FUNCT_1:def 3;
then
A10: sg1p/.1 = EmptyBag n by A7,TARSKI:def 1;
A11: for u being object holds u in dom sg1p implies u in {1}
proof
let u be object;
assume
A12: u in dom sg1p;
assume
A13: not u in {1};
reconsider u as Element of NAT by A12;
sg1p/.u = sg1p.u by A12,PARTFUN1:def 6;
then
A14: sg1p/.u in rng sg1p by A12,FUNCT_1:def 3;
A15: u <> 1 by A13,TARSKI:def 1;
A16: 1 < u
proof
consider k being Nat such that
A17: dom sg1p = Seg k by FINSEQ_1:def 2;
Seg k = {m where m is Nat : 1 <= m & m <= k} by FINSEQ_1:def 1;
then
ex m9 being Nat st m9 = u & 1 <= m9 & m9 <= k by A12,A17;
hence thesis by A15,XXREAL_0:1;
end;
sg1p/.1 = sg1p.1 by A8,A12,FINSEQ_3:31,PARTFUN1:def 6;
then sg1p/.1 in rng sg1p by A9,FUNCT_1:def 3;
then sg1p/.1 = EmptyBag n by A7,TARSKI:def 1
.= sg1p/.u by A7,A14,TARSKI:def 1;
hence thesis by A4,A9,A12,A16,PRE_POLY:def 2;
end;
A18: dom 1p = Bags n by FUNCT_2:def 1;
A19: 1 in dom sg1p by A8,FINSEQ_3:31;
A20: sg1p.1 in rng sg1p by A9,FUNCT_1:def 3;
then sg1p.1 in {EmptyBag n} by A6,A4,PRE_POLY:def 2;
then sg1p.1 = EmptyBag n by TARSKI:def 1;
then 1 in dom (1p * sg1p) by A19,A18,FUNCT_1:11;
then
A21: (1p * sg1p)/.1 = (1p * sg1p).1 by PARTFUN1:def 6
.= 1p.(sg1p.1) by A9,FUNCT_1:13
.= 1p.(EmptyBag n) by A7,A20,TARSKI:def 1
.= 1.L by POLYNOM1:25;
consider y being FinSequence of the carrier of L such that
A22: len y = len sg1p and
A23: Sum y = eval(1p,x) and
A24: for i being Element of NAT st 1 <= i & i <= len y holds y/.i = (1p
* sg1p)/.i * eval(((sg1p)/.i),x) by Def2;
for u being object holds u in {1} implies u in dom sg1p by A9,TARSKI:def 1;
then dom sg1p = Seg 1 by A11,FINSEQ_1:2,TARSKI:2;
then
A25: len sg1p = 1 by FINSEQ_1:def 3;
then y.1 = y/.1 by A22,FINSEQ_4:15
.= (1p * sg1p)/.1 * eval(((sg1p)/.1),x) by A25,A22,A24
.= (1p * sg1p)/.1 * 1.L by A10,Th6
.= (1p * sg1p)/.1;
then y = <* 1.L *> by A25,A22,A21,FINSEQ_1:40;
hence thesis by A23,RLVECT_1:44;
end;
theorem Th14:
for n being Ordinal, L being right_zeroed add-associative
right_complementable well-unital distributive non trivial
doubleLoopStr, p being Polynomial of n,L, x being Function of n, L holds eval(
-p,x) = - eval(p,x)
proof
let n be Ordinal, L be right_zeroed add-associative right_complementable
well-unital distributive non trivial doubleLoopStr, p be Polynomial
of n,L, x be Function of n, L;
set mp = -p;
A1: for u being object holds u in Support p implies u in Support mp
proof
let u be object;
assume
A2: u in Support p;
then reconsider u as Element of Bags n;
reconsider u as bag of n;
A3: p.u <> 0.L by A2,POLYNOM1:def 4;
mp.u <> 0.L
proof
assume mp.u = 0.L;
then -(-(p.u)) = - 0.L by POLYNOM1:17;
then p.u = - 0.L by RLVECT_1:17;
hence thesis by A3,RLVECT_1:12;
end;
hence thesis by POLYNOM1:def 4;
end;
consider ymp being FinSequence of the carrier of L such that
A4: len ymp = len SgmX(BagOrder n, Support mp) and
A5: Sum ymp = eval(mp,x) and
A6: for i being Element of NAT st 1 <= i & i <= len ymp holds ymp/.i =
(mp * SgmX(BagOrder n, Support mp))/.i * eval(((SgmX(BagOrder n, Support mp))/.
i),x) by Def2;
consider yp being FinSequence of the carrier of L such that
A7: len yp = len SgmX(BagOrder n, Support p) and
A8: Sum yp = eval(p,x) and
A9: for i being Element of NAT st 1 <= i & i <= len yp holds yp/.i = (p
* SgmX(BagOrder n, Support p))/.i * eval(((SgmX(BagOrder n, Support p))/.i),x)
by Def2;
A10: for u being object holds u in Support mp implies u in Support p
proof
let u be object;
assume
A11: u in Support mp;
then reconsider u as Element of Bags n;
reconsider u as bag of n;
mp.u <> 0.L by A11,POLYNOM1:def 4;
then -(p.u) <> 0.L by POLYNOM1:17;
then p.u <> 0.L by RLVECT_1:12;
hence thesis by POLYNOM1:def 4;
end;
then
A12: len ymp = len yp by A1,A7,A4,TARSKI:2;
A13: dom ((-1.L) * yp) = dom yp by POLYNOM1:def 1;
consider k being Element of NAT such that
A14: k = len ((-1.L) * yp);
consider l being Element of NAT such that
A15: l = len yp;
A16: dom ((-1.L) * yp) = Seg k by A14,FINSEQ_1:def 3;
A17: SgmX(BagOrder n, Support p) = SgmX(BagOrder n, Support mp) by A1,A10,
TARSKI:2;
A18: for k being Nat st 1 <= k & k <= len ymp holds ymp.k = ((-1.L) * yp).k
proof
let k be Nat;
assume that
A19: 1 <= k and
A20: k <= len ymp;
A21: k <= len ((-1.L) * yp) by A12,A13,A14,A16,A20,FINSEQ_1:def 3;
A22: (mp * SgmX(BagOrder n, Support p))/.k = (-1.L) * ((p * SgmX(BagOrder
n, Support p))/.k)
proof
reconsider b = SgmX(BagOrder n, Support p)/.k as bag of n;
k in Seg (len(SgmX(BagOrder n, Support p))) by A7,A12,A19,A20,FINSEQ_1:1;
then
A23: k in dom SgmX(BagOrder n, Support p) by FINSEQ_1:def 3;
A24: dom p = Bags n by FUNCT_2:def 1;
then b in dom p;
then
A25: k in dom (p * SgmX(BagOrder n, Support p)) by A23,PARTFUN2:3;
A26: dom mp = Bags n by FUNCT_2:def 1;
then b in dom mp;
then k in dom (mp * SgmX(BagOrder n, Support p)) by A23,PARTFUN2:3;
hence (mp * SgmX(BagOrder n, Support p))/.k = mp/.b by PARTFUN2:3
.= mp.b by A26,PARTFUN1:def 6
.= -(p.b) by POLYNOM1:17
.= -(1.L * p/.b) by A24,PARTFUN1:def 6
.= (-1.L) * p/.b by VECTSP_1:9
.= (-1.L) * ((p * SgmX(BagOrder n, Support p))/.k) by A25,PARTFUN2:3;
end;
A27: k in Seg l by A12,A15,A19,A20,FINSEQ_1:1;
then
A28: k in dom yp by A15,FINSEQ_1:def 3;
thus ymp.k = ymp/.k by A19,A20,FINSEQ_4:15
.= ((-1.L) * ((p * SgmX(BagOrder n, Support p))/.k)) * eval(((SgmX(
BagOrder n, Support p))/.k),x) by A17,A6,A19,A20,A27,A22
.= (-(1.L * ((p * SgmX(BagOrder n, Support p))/.k))) * eval(((SgmX(
BagOrder n, Support p))/.k),x) by VECTSP_1:9
.= -(((p * SgmX(BagOrder n, Support p))/.k) * eval(((SgmX(BagOrder n,
Support p))/.k),x)) by VECTSP_1:9
.= - (yp/.k) by A9,A12,A19,A20,A27
.= - (1.L * (yp/.k))
.= (-1.L) * (yp/.k) by VECTSP_1:9
.= ((-1.L) * yp)/.k by A28,POLYNOM1:def 1
.= ((-1.L) * yp).k by A19,A21,FINSEQ_4:15;
end;
dom yp = Seg l by A15,FINSEQ_1:def 3;
hence eval(mp,x) = Sum((-1.L) * yp) by A5,A12,A13,A14,A15,A16,A18,FINSEQ_1:6
,14
.= (-1.L) * Sum(yp) by POLYNOM1:12 :: Sum yp = eval(p,x)
.= -(1.L * eval(p,x)) by VECTSP_1:9,A8
.= - eval(p,x);
end;
Lm6: for n being Ordinal, L being right_zeroed add-associative
right_complementable Abelian well-unital distributive non trivial
doubleLoopStr, p,q being Polynomial of n,L, x being Function of n, L, b being
bag of n st not(b in Support p) & Support q = Support p \/ {b} & for b9 being
bag of n st b9 <> b holds q.b9 = p.b9 holds eval(q,x) = eval(p,x) + q.b * eval(
b,x)
proof
let n be Ordinal, L be right_zeroed add-associative right_complementable
Abelian well-unital distributive non trivial doubleLoopStr, p,q be
Polynomial of n,L, x be Function of n, L, b be bag of n;
assume that
A1: not b in Support p and
A2: Support q = Support p \/ {b} and
A3: for b9 being bag of n st b9 <> b holds q.b9 = p.b9;
set sq = SgmX(BagOrder n, Support q), sp = SgmX(BagOrder n, Support p);
A4: BagOrder n linearly_orders Support q by Th10;
b in {b} by TARSKI:def 1;
then b in Support q by A2,XBOOLE_0:def 3;
then b in rng sq by A4,PRE_POLY:def 2;
then consider k being Nat such that
A5: k in dom sq and
A6: sq.k = b by FINSEQ_2:10;
A7: sq/.k = b by A5,A6,PARTFUN1:def 6;
reconsider b as Element of Bags n by PRE_POLY:def 12;
A8: dom sq = Seg(len sq) by FINSEQ_1:def 3;
then
A9: k <= len sq by A5,FINSEQ_1:1;
1 <= k by A5,A8,FINSEQ_1:1;
then 1 - 1 <= k - 1 by XREAL_1:9;
then reconsider k9 = k - 1 as Element of NAT by INT_1:3;
A10: k9 + 1 = k + 0;
then
A11: sq = Ins(sp,k9,b) by A1,A2,A5,A7,Th10,PRE_POLY:80;
consider yp being FinSequence of the carrier of L such that
A12: len yp = len sp and
A13: Sum yp = eval(p,x) and
A14: for i being Element of NAT st 1 <= i & i <= len yp holds yp/.i = (p
* sp)/.i * eval((sp/.i),x) by Def2;
consider yq being FinSequence of the carrier of L such that
A15: len yq = len sq and
A16: Sum yq = eval(q,x) and
A17: for i being Element of NAT st 1 <= i & i <= len yq holds yq/.i = (q
* sq)/.i * eval((sq/.i),x) by Def2;
VA: dom yq = dom sq by A15,FINSEQ_3:29;
reconsider b as Element of Bags n;
set ytmp = Ins(yp,k9,q.b * eval(b,x));
A18: len sp + 1 = (card(Support p) + 1) by Th10,PRE_POLY:11
.= card(Support q) by A1,A2,CARD_2:41
.= len sq by Th10,PRE_POLY:11;
then
A19: len yq = len ytmp by A15,A12,FINSEQ_5:69;
A20: BagOrder n linearly_orders Support p by Th10;
A21: for i being Nat st 1 <= i & i <= len yq holds yq.i = ytmp.i
proof
let i be Nat;
assume that
A22: 1 <= i and
A23: i <= len yq;
A24: i in dom yq by A22,A23,FINSEQ_3:25;
i in Seg len ytmp by A19,A22,A23,FINSEQ_1:1;
then
A25: i in dom ytmp by FINSEQ_1:def 3;
per cases;
suppose
A26: i = k;
dom q = Bags n by FUNCT_2:def 1;
then sq.k in dom q by A6,PRE_POLY:def 12;
then
A27: k in dom(q * sq) by A5,FUNCT_1:11;
then
A28: (q * sq)/.k = (q * sq).k by PARTFUN1:def 6
.= q.b by A6,A27,FUNCT_1:12;
A29: yq/.i = (q * sq)/.k * eval((sq/.k),x) by A5,A17,A22,A23,A26
.= q.b * eval(b,x) by A5,A6,A28,PARTFUN1:def 6;
A30: k9 <= len yp by A9,A10,A12,A18,XREAL_1:6;
thus ytmp.i = q.b * eval(b,x) by A10,A26,A30,FINSEQ_5:73
.= yq.i by A24,A29,PARTFUN1:def 6;
end;
suppose
A31: i <> k;
len(Ins(sp,k9,b)) = len sp + 1 by FINSEQ_5:69;
then
A32: dom(Ins(sp,k9,b)) = Seg(len(sp)+1) by FINSEQ_1:def 3;
now
per cases by A31,XXREAL_0:1;
case
A33: i < k;
k9 < k by A10,NAT_1:19;
then k9 < len yq by A9,A15,XXREAL_0:2;
then
A34: k9 <= len yp by A15,A12,A18,NAT_1:13;
A35: yp|(Seg k9) is FinSequence by FINSEQ_1:15;
A36: i <= k9 by A10,A33,NAT_1:13;
then i in Seg k9 by A22,FINSEQ_1:1;
then i in dom(yp|(Seg k9)) by A34,A35,FINSEQ_1:17;
then
A37: i in dom(yp|k9) by FINSEQ_1:def 16;
A38: k - 1 <= (len sp + 1) - 1 by A9,A18,XREAL_1:9;
then
A39: i <= len sp by A36,XXREAL_0:2;
then
A40: i in dom sp by A22,FINSEQ_3:25;
A41: now
assume sp/.i = b;
then sp.i = b by A40,PARTFUN1:def 6;
then b in rng sp by A40,FUNCT_1:def 3;
hence contradiction by A1,A20,PRE_POLY:def 2;
end;
i < len yq by A9,A15,A33,XXREAL_0:2;
then
A42: i <= len yp by A15,A12,A18,NAT_1:13; then
VV: i in dom yp by FINSEQ_3:25,A22;
A43: sp|(Seg k9) is FinSequence by FINSEQ_1:15;
A44: rng Ins(sp,k9,b) c= Bags n by FINSEQ_1:def 4;
A45: dom q = Bags n by FUNCT_2:def 1;
A46: rng sp c= Bags n by FINSEQ_1:def 4;
i in Seg k9 by A22,A36,FINSEQ_1:1;
then i in dom(sp|(Seg k9)) by A38,A43,FINSEQ_1:17;
then
A47: i in dom(sp|k9) by FINSEQ_1:def 16;
sp.i in rng sp by A40,FUNCT_1:def 3;
then sp.i in Bags n by A46;
then sp.i in dom p by FUNCT_2:def 1;
then
A48: i in dom(p * sp) by A40,FUNCT_1:11;
len sp <= len sp + 1 by XREAL_1:29;
then i <= len sp + 1 by A39,XXREAL_0:2;
then
A49: i in dom(Ins(sp,k9,b)) by A22,A32,FINSEQ_1:1;
then Ins(sp,k9,b).i in rng Ins(sp,k9,b) by FUNCT_1:def 3;
then
A50: i in dom(q * Ins(sp,k9,b)) by A49,A44,A45,FUNCT_1:11;
then
A51: (q * Ins(sp,k9,b)).i = q.(Ins(sp,k9,b).i) by FUNCT_1:12
.= q.(sp.i) by A47,FINSEQ_5:72
.= q.(sp/.i) by A40,PARTFUN1:def 6
.= p.(sp/.i) by A3,A41
.= p.(sp.i) by A40,PARTFUN1:def 6
.= (p * sp).i by A48,FUNCT_1:12;
i in dom (q*sq) by A50,A11; then
Z: (q*sq)/.i = (q*sq).i & (p*sp)/.i = (p*sp).i
by A48,PARTFUN1:def 6;
i in dom sq by A24,VA; then
Z1: sq/.i = sq.i & sp/.i = sp.i by A40,PARTFUN1:def 6;
A52: yq/.i = (q * sq)/.i * eval((sq/.i),x) by A17,A22,A23,A49
.= (p * sp)/.i * eval((sp/.i),x) by A11,A47,A51,FINSEQ_5:72,Z,Z1
.= yp/.i by A14,A22,A49,A42
.= yp.i by PARTFUN1:def 6,VV
.= ytmp.i by A37,FINSEQ_5:72
.= ytmp/.i by A25,PARTFUN1:def 6;
thus yq.i = yq/.i by A24,PARTFUN1:def 6
.= ytmp.i by A25,A52,PARTFUN1:def 6;
end;
case
A53: i > k;
then i - 1 > k9 by XREAL_1:9;
then reconsider i1 = i - 1 as Element of NAT by INT_1:3;
A54: (i - 1) + 1 = i + 0; then
A55: k9 + 1 <= i1 by A53,NAT_1:13;
A56: dom q = Bags n by FUNCT_2:def 1;
A57: rng Ins(sp,k9,b) c= Bags n by FINSEQ_1:def 4;
A58: dom p = Bags n by FUNCT_2:def 1;
A59: rng sp c= Bags n by FINSEQ_1:def 4;
A60: i - 1 <= (len yp + 1) - 1 by A15,A12,A18,A23,XREAL_1:9;
0 + 1 <= k9 + 1 by XREAL_1:6;
then 1 < i by A53,XXREAL_0:2; then
A61: 1 <= i1 by A54,NAT_1:13;
then i1 in Seg len sp by A12,A60,FINSEQ_1:1;
then
A62: i1 in dom sp by FINSEQ_1:def 3;
dom yp = dom sp by A12,FINSEQ_3:29; then
AA: i1 in dom yp by A62;
A63: now
assume sp/.i1 = b;
then sp.i1 = b by A62,PARTFUN1:def 6;
then b in rng sp by A62,FUNCT_1:def 3;
hence contradiction by A1,A20,PRE_POLY:def 2;
end;
sp.i1 in rng sp by A62,FUNCT_1:def 3;
then
A64: i1 in dom(p * sp) by A62,A59,A58,FUNCT_1:11;
A65: i = i1 + 1;
A66: i in dom(Ins(sp,k9,b)) by A15,A18,A22,A23,A32,FINSEQ_1:1;
then Ins(sp,k9,b).i in rng Ins(sp,k9,b) by FUNCT_1:def 3;
then
A67: i in dom(q * Ins(sp,k9,b)) by A66,A57,A56,FUNCT_1:11;
then
A68: (q * Ins(sp,k9,b)).i
= q.(Ins(sp,k9,b).i) by FUNCT_1:12
.= q.(sp.i1) by A12,A60,A65,A55,FINSEQ_5:74
.= q.(sp/.i1) by A62,PARTFUN1:def 6
.= p.(sp/.i1) by A3,A63
.= p.(sp.i1) by A62,PARTFUN1:def 6
.= (p * sp).i1 by A64,FUNCT_1:12;
BB: dom yq = dom sq by FINSEQ_3:29,A15;
SS: (q*sq)/.i = (q*sq).i by A67,PARTFUN1:def 6,A11
.= (p*sp)/.i1 by A64,PARTFUN1:def 6,A68,A11;
SA: sq/.i = sq.i by A24,BB,PARTFUN1:def 6
.= sp.i1 by A12,A60,A65,A55,A11,FINSEQ_5:74
.= sp/.i1 by PARTFUN1:def 6,A62;
A69: yq/.i = (q * sq)/.i * eval((sq/.i),x) by A17,A22,A23,A66
.= yp/.i1 by A14,A60,A61,SS,SA
.= yp.i1 by PARTFUN1:def 6,AA
.= ytmp.i by A60,A65,A55,FINSEQ_5:74
.= ytmp/.i by PARTFUN1:def 6,A25;
thus yq.i = yq/.i by A24,PARTFUN1:def 6
.= ytmp.i by A25,A69,PARTFUN1:def 6;
end;
end;
hence thesis;
end;
end;
Sum((yp|k9)^<*q.b * eval(b,x)*>^(yp/^k9)) = Sum((yp|k9)^<*q.b * eval(b,
x)*>) + Sum(yp/^k9) by RLVECT_1:41
.= (Sum(yp|k9) + Sum(<*q.b * eval(b,x)*>)) + Sum(yp/^k9) by RLVECT_1:41
.= (Sum(yp|k9) + Sum(yp/^k9)) + Sum(<*q.b * eval(b,x)*>) by RLVECT_1:def 3
.= Sum((yp|k9)^(yp/^k9)) + Sum(<*q.b * eval(b,x)*>) by RLVECT_1:41
.= Sum yp + Sum(<*q.b * eval(b,x)*>) by RFINSEQ:8
.= eval(p,x) + q.b * eval(b,x) by A13,RLVECT_1:44;
then Sum ytmp = eval(p,x) + q.b * eval(b,x) by FINSEQ_5:def 4;
hence thesis by A16,A19,A21,FINSEQ_1:14;
end;
Lm7: for n being Ordinal, L being right_zeroed add-associative
right_complementable Abelian well-unital distributive non trivial
doubleLoopStr, p being Polynomial of n,L st (ex b being bag of n st Support p
= {b}) for q being Polynomial of n,L, x being Function of n, L holds eval(p+q,x
) = eval(p,x) + eval(q,x)
proof
let n be Ordinal, L be right_zeroed add-associative right_complementable
well-unital distributive Abelian non trivial doubleLoopStr, p be
Polynomial of n,L;
assume ex b being bag of n st Support p = {b};
then consider b being bag of n such that
A1: Support p = {b};
b in Support p by A1,TARSKI:def 1;
then
A2: p.b <> 0.L by POLYNOM1:def 4;
let q be Polynomial of n,L, x be Function of n, L;
A3: for b9 being bag of n st b9 <> b holds (p+q).b9 = q.b9
proof
let b9 be bag of n;
A4: b9 is Element of Bags n by PRE_POLY:def 12;
assume b9 <> b;
then
A5: not b9 in Support p by A1,TARSKI:def 1;
thus (p+q).b9 = p.b9 + q.b9 by POLYNOM1:15
.= 0.L + q.b9 by A5,A4,POLYNOM1:def 4
.= q.b9 by RLVECT_1:def 4;
end;
set sq = SgmX(BagOrder n, Support q), spq = SgmX(BagOrder n, Support (p+q));
A6: b is Element of Bags n by PRE_POLY:def 12;
A7: Support(p+q) c= Support p \/ Support q by POLYNOM1:20;
consider yq being FinSequence of the carrier of L such that
A8: len yq = len sq and
A9: eval(q,x) = Sum yq and
A10: for i being Element of NAT st 1 <= i & i <= len yq holds yq/.i = (q
* sq)/.i * eval((sq/.i),x) by Def2;
consider ypq being FinSequence of the carrier of L such that
A11: len ypq = len spq and
A12: eval(p+q,x) = Sum ypq and
A13: for i being Element of NAT st 1 <= i & i <= len ypq holds ypq/.i =
((p+q) * spq)/.i * eval((spq/.i),x) by Def2;
A14: BagOrder n linearly_orders Support q by Th10;
now
per cases;
case
A15: b in Support q;
now
per cases;
case
A16: p.b = - q.b;
A17: for u being object
holds u in Support q implies u in Support(p+q) \/ {b }
proof
let u be object;
assume
A18: u in Support q;
then reconsider u as bag of n;
per cases;
suppose
u = b;
then u in {b} by TARSKI:def 1;
hence thesis by XBOOLE_0:def 3;
end;
suppose
u <> b;
then (p+q).u = q.u by A3;
then
A19: (p+q).u <> 0.L by A18,POLYNOM1:def 4;
u is Element of Bags n by PRE_POLY:def 12;
then u in Support(p+q) by A19,POLYNOM1:def 4;
hence thesis by XBOOLE_0:def 3;
end;
end;
(p+q).b = p.b + q.b by POLYNOM1:15
.= 0.L by A16,RLVECT_1:5;
then
A20: not b in Support(p+q) by POLYNOM1:def 4;
for u being object
holds u in Support(p+q) \/ {b} implies u in Support q
proof
let u be object;
assume
A21: u in Support(p+q) \/ {b};
per cases by A21,XBOOLE_0:def 3;
suppose
A22: u in Support(p+q);
then not u in {b} by A20,TARSKI:def 1;
hence thesis by A1,A7,A22,XBOOLE_0:def 3;
end;
suppose
u in {b};
hence thesis by A15,TARSKI:def 1;
end;
end;
then
A23: Support(p+q) \/ {b} = Support q by A17,TARSKI:2;
thus eval(p+q,x) = eval(p+q,x) + 0.L by RLVECT_1:def 4
.= eval(p+q,x) + (q.b * eval(b,x) + -q.b * eval(b,x)) by RLVECT_1:5
.= (eval(p+q,x) + q.b * eval(b,x)) + -q.b * eval(b,x) by
RLVECT_1:def 3
.= eval(q,x) + -q.b * eval(b,x) by A3,A20,A23,Lm6
.= eval(q,x) + p.b * eval(b,x) by A16,VECTSP_1:9
.= eval(q,x) + eval(p,x) by A1,Th11;
end;
case
A24: p.b <> -q.b;
p.b + q.b <> (-q.b) + q.b
proof
assume
A25: p.b + q.b = (-q.b) + q.b;
p.b = p.b + 0.L by RLVECT_1:def 4
.= p.b + (q.b + -q.b) by RLVECT_1:5
.= ((-q.b) + q.b) + -q.b by A25,RLVECT_1:def 3
.= 0.L + -q.b by RLVECT_1:5
.= - q.b by RLVECT_1:def 4;
hence thesis by A24;
end;
then p.b + q.b <> 0.L by RLVECT_1:5;
then
A26: (p+q).b <> 0.L by POLYNOM1:15;
A27: for u being object holds u in Support q implies u in Support(p+q)
proof
let u be object;
assume
A28: u in Support q;
then reconsider u as bag of n;
per cases;
suppose
u = b;
hence thesis by A6,A26,POLYNOM1:def 4;
end;
suppose
u <> b;
then (p+q).u = q.u by A3;
then
A29: (p+q).u <> 0.L by A28,POLYNOM1:def 4;
u is Element of Bags n by PRE_POLY:def 12;
hence thesis by A29,POLYNOM1:def 4;
end;
end;
A30: for u being object holds u in Support(p+q) implies u in Support q
proof
let u be object;
assume
A31: u in Support(p+q);
then reconsider u as bag of n;
per cases by A7,A31,XBOOLE_0:def 3;
suppose
u in Support p;
hence thesis by A1,A15,TARSKI:def 1;
end;
suppose
u in Support q;
hence thesis;
end;
end;
then
A32: Support(p+q) = Support q by A27,TARSKI:2;
A33: len ypq = len yq by A11,A8,A30,A27,TARSKI:2;
consider spqk being Nat such that
A34: dom spq = Seg spqk by FINSEQ_1:def 2;
b in rng sq by A14,A15,PRE_POLY:def 2;
then consider k being Nat such that
A35: k in dom sq and
A36: sq.k = b by FINSEQ_2:10;
consider sqk being Nat such that
A37: dom sq = Seg sqk by FINSEQ_1:def 2;
reconsider k as Element of NAT by ORDINAL1:def 12;
reconsider k,sqk,spqk as Element of NAT by ORDINAL1:def 12;
A38: 1 <= k by A35,A37,FINSEQ_1:1;
A39: dom(p+q) = Bags n by FUNCT_2:def 1;
then sq.k in dom(p+q) by A36,PRE_POLY:def 12;
then
A40: k in dom((p+q) * sq) by A35,FUNCT_1:11;
then
A41: ((p+q) * sq)/.k = ((p+q) * sq).k by PARTFUN1:def 6
.= (p+q).b by A36,A40,FUNCT_1:12;
A42: k <= sqk by A35,A37,FINSEQ_1:1;
A43: dom q = Bags n by FUNCT_2:def 1;
then sq.k in dom q by A36,PRE_POLY:def 12;
then
A44: k in dom(q * sq) by A35,FUNCT_1:11;
then
A45: (q * sq)/.k = (q * sq).k by PARTFUN1:def 6
.= q.b by A36,A44,FUNCT_1:12;
consider i being Nat such that
A46: dom yq = Seg i by FINSEQ_1:def 2;
A47: sqk = len sq by A37,FINSEQ_1:def 3
.= len spq by A30,A27,TARSKI:2
.= spqk by A34,FINSEQ_1:def 3;
A48: i in NAT by ORDINAL1:def 12;
then
A49: len yq = i by A46,FINSEQ_1:def 3;
A50: for i9 being Element of NAT st i9 in dom yq & i9 <> k holds ypq
/.i9 = yq/.i9
proof
let i9 be Element of NAT;
assume that
A51: i9 in dom yq and
A52: i9 <> k;
A53: 1 <= i9 by A46,A51,FINSEQ_1:1;
i9 in Seg(len spq) by A11,A33,A51,FINSEQ_1:def 3;
then
A54: i9 in dom spq by FINSEQ_1:def 3;
then spq/.i9 = spq.i9 by PARTFUN1:def 6;
then
A55: i9 in dom((p+q) * spq) by A39,A54,FUNCT_1:11;
then
A56: ((p+q) * spq)/.i9 = ((p+q) * spq).i9 by PARTFUN1:def 6
.= (p+q).(spq.i9) by A55,FUNCT_1:12
.= (p+q).(spq/.i9) by A54,PARTFUN1:def 6;
A57: spq/.i9 <> b
proof
assume spq/.i9 = b;
then
A58: spq.i9 = b by A54,PARTFUN1:def 6;
A59: spq is one-to-one by Th10,PRE_POLY:10;
spq.k = b by A30,A27,A36,TARSKI:2;
hence thesis by A35,A37,A34,A47,A52,A54,A58,A59,FUNCT_1:def 4;
end;
A60: i9 in dom sq by A8,A46,A49,A51,FINSEQ_1:def 3;
sq/.i9 = sq.i9 by A37,A34,A47,A54,PARTFUN1:def 6;
then
A61: i9 in dom(q * sq) by A43,A60,FUNCT_1:11;
then
A62: (q * sq)/.i9 = (q * sq).i9 by PARTFUN1:def 6
.= q.(sq.i9) by A61,FUNCT_1:12
.= q.(sq/.i9) by A60,PARTFUN1:def 6;
A63: i9 <= len yq by A46,A49,A51,FINSEQ_1:1;
hence ypq/.i9 = ((p+q) * spq)/.i9 * eval((spq/.i9),x) by A13,A33
,A53
.= q.(sq/.i9) * eval((sq/.i9),x) by A3,A32,A57,A56
.= yq/.i9 by A10,A53,A63,A62;
end;
A64: sq/.k = b by A35,A36,PARTFUN1:def 6;
A65: sqk = len yq by A8,A37,FINSEQ_1:def 3;
then k <= i by A42,A46,A48,FINSEQ_1:def 3;
then
A66: k in dom yq by A38,A46,FINSEQ_1:1;
len ypq = sqk by A11,A34,A47,FINSEQ_1:def 3;
then ypq/.k = ((p+q) * spq)/.k * eval((spq/.k),x) by A13,A38,A42
.= (p.b + q.b) * eval(b,x) by A32,A64,A41,POLYNOM1:15
.= p.b * eval(b,x) + (q * sq)/.k * eval((sq/.k),x) by A64,A45,
VECTSP_1:def 7
.= p.b * eval(b,x) + yq/.k by A10,A38,A42,A65;
hence eval(p+q,x) = p.b * eval(b,x) + Sum yq by A12,A33,A66,A50,Th4
.= eval(p,x) + eval(q,x) by A1,A9,Th11;
end;
end;
hence thesis;
end;
case
A67: not b in Support q;
A68: (p+q).b = p.b + q.b by POLYNOM1:15
.= p.b + 0.L by A6,A67,POLYNOM1:def 4
.= p.b by RLVECT_1:def 4;
A69: for u being object holds u in Support p \/ Support q implies u in
Support(p+q)
proof
let u be object;
assume
A70: u in Support p \/ Support q;
per cases by A70,XBOOLE_0:def 3;
suppose
u in Support p;
then u = b by A1,TARSKI:def 1;
hence thesis by A6,A2,A68,POLYNOM1:def 4;
end;
suppose
A71: u in Support q;
then reconsider u as bag of n;
A72: q.u <> 0.L by A71,POLYNOM1:def 4;
(p+q).u = q.u by A3,A67,A71;
hence thesis by A71,A72,POLYNOM1:def 4;
end;
end;
for u being object holds u in Support(p+q) implies u in Support p \/
Support q by A7;
then Support(p+q) = {b} \/ Support q by A1,A69,TARSKI:2;
hence eval(p+q,x) = eval(q,x) + (p+q).b * eval(b,x) by A3,A67,Lm6
.= eval(q,x) + eval(p,x) by A1,A68,Th11;
end;
end;
hence thesis;
end;
theorem Th15:
for n being Ordinal, L being right_zeroed add-associative
right_complementable Abelian well-unital distributive non trivial
doubleLoopStr, p,q being Polynomial of n,L, x being Function of n, L holds
eval(p+q,x) = eval(p,x) + eval(q,x)
proof
let n be Ordinal, L be right_zeroed add-associative right_complementable
Abelian well-unital distributive non trivial doubleLoopStr, p,q be
Polynomial of n,L, x be Function of n, L;
defpred P[Nat] means for p being Polynomial of n,L st card(
Support p) = $1 holds eval(p+q,x) = eval(p,x) + eval(q,x);
A1: ex k being Element of NAT st card(Support p) = k;
A2: for k being Nat st P[k] holds P[k + 1]
proof
let k be Nat;
assume
A3: P[k];
let p be Polynomial of n,L;
assume
A4: card(Support p) = k + 1;
set sgp = SgmX(BagOrder n, Support p);
set bg = sgp/.(len sgp);
A5: BagOrder n linearly_orders Support p by Th10;
then sgp <> {} by A4,CARD_1:27,PRE_POLY:def 2,RELAT_1:38;
then 1 <= len sgp by NAT_1:14;
then len sgp in Seg(len sgp) by FINSEQ_1:1;
then
A6: len sgp in dom sgp by FINSEQ_1:def 3;
then sgp/.(len sgp) = sgp.(len sgp) by PARTFUN1:def 6;
then bg in rng sgp by A6,FUNCT_1:def 3;
then
A7: bg in Support p by A5,PRE_POLY:def 2;
then
A8: p.bg <> 0.L by POLYNOM1:def 4;
set m = 0_(n,L)+*(bg,p.bg);
set p9 = p+*(bg,0.L);
reconsider bg as bag of n;
dom p = Bags n by FUNCT_2:def 1;
then
A9: p9 = p+*(bg.-->0.L) by FUNCT_7:def 3;
reconsider p9 as Function of Bags n,the carrier of L;
reconsider p9 as Function of Bags n,L;
for u being object holds u in Support p9 implies u in Support p
proof
let u be object;
assume
A10: u in Support p9;
then reconsider u as Element of Bags n;
reconsider u as bag of n;
now
assume
A11: u = bg;
then u in {bg} by TARSKI:def 1;
then u in dom(bg.-->0.L);
then p9.u = (bg.-->0.L).bg by A9,A11,FUNCT_4:13;
then p9.u = 0.L by FUNCOP_1:72;
hence contradiction by A10,POLYNOM1:def 4;
end;
then not u in {bg} by TARSKI:def 1;
then not u in dom(bg.-->0.L);
then p.u = p9.u by A9,FUNCT_4:11;
then p.u <> 0.L by A10,POLYNOM1:def 4;
hence thesis by POLYNOM1:def 4;
end;
then Support p9 c= Support p by TARSKI:def 3;
then reconsider p9 as Polynomial of n,L by POLYNOM1:def 5;
A12: dom p = Bags n by FUNCT_2:def 1;
A13: for u being object holds u in Support p implies u in Support p9 \/ {bg}
proof
let u be object;
assume
A14: u in Support p;
then reconsider u as Element of Bags n;
A15: p.u <> 0.L by A14,POLYNOM1:def 4;
per cases;
suppose
u = bg;
then u in {bg} by TARSKI:def 1;
hence thesis by XBOOLE_0:def 3;
end;
suppose
u <> bg;
then not u in {bg} by TARSKI:def 1;
then not u in dom(bg.-->0.L);
then p9.u = p.u by A9,FUNCT_4:11;
then u in Support p9 by A15,POLYNOM1:def 4;
hence thesis by XBOOLE_0:def 3;
end;
end;
bg in {bg} by TARSKI:def 1;
then bg in dom(bg.-->0.L);
then p9.bg = (bg.-->0.L).bg by A9,FUNCT_4:13;
then
A16: p9.bg = 0.L by FUNCOP_1:72;
then
A17: not bg in Support p9 by POLYNOM1:def 4;
for u being object holds u in Support p9 \/ {bg} implies u in Support p
proof
let u be object;
assume
A18: u in Support p9 \/ {bg};
per cases by A18,XBOOLE_0:def 3;
suppose
A19: u in Support p9;
then reconsider u as Element of Bags n;
u <> bg by A16,A19,POLYNOM1:def 4;
then not u in {bg} by TARSKI:def 1;
then not u in dom(bg.-->0.L);
then
A20: p9.u = p.u by A9,FUNCT_4:11;
p9.u <> 0.L by A19,POLYNOM1:def 4;
hence thesis by A20,POLYNOM1:def 4;
end;
suppose
u in {bg};
hence thesis by A7,TARSKI:def 1;
end;
end;
then Support p = Support p9 \/ {bg} by A13,TARSKI:2;
then
A21: k + 1 = card(Support p9) + 1 by A4,A17,CARD_2:41;
dom 0_(n,L) = Bags n by FUNCT_2:def 1;
then
A22: m = 0_(n,L)+*(bg.-->p.bg) by FUNCT_7:def 3;
reconsider m as Function of Bags n,the carrier of L;
reconsider m as Function of Bags n,L;
A23: for u being object holds u in Support m implies u in {bg}
proof
let u be object;
assume
A24: u in Support m;
then reconsider u as Element of Bags n;
A25: m.u <> 0.L by A24,POLYNOM1:def 4;
now
assume u <> bg;
then not u in {bg} by TARSKI:def 1;
then not u in dom(bg.-->p.bg);
then m.u = 0_(n,L).u by A22,FUNCT_4:11;
hence contradiction by A25,POLYNOM1:22;
end;
hence thesis by TARSKI:def 1;
end;
for u being object holds u in {bg} implies u in Support m
proof
let u be object;
bg in {bg} by TARSKI:def 1;
then bg in dom(bg.-->p.bg);
then m.bg = (bg.-->p.bg).bg by A22,FUNCT_4:13;
then
A26: m.bg = p.bg by FUNCOP_1:72;
assume u in {bg};
then u = bg by TARSKI:def 1;
hence thesis by A8,A26,POLYNOM1:def 4;
end;
then
A27: Support m = {bg} by A23,TARSKI:2;
then reconsider m as Polynomial of n,L by POLYNOM1:def 5;
reconsider m as Polynomial of n,L;
A28: for u being object st u in Bags n holds (p9+m).u = p.u
proof
let u be object;
assume u in Bags n;
then reconsider u as bag of n;
per cases;
suppose
A29: u = bg;
bg in {bg} by TARSKI:def 1;
then bg in dom(bg.-->p.bg);
then m.bg = (bg.-->p.bg).bg by A22,FUNCT_4:13;
then
A30: m.bg = p.bg by FUNCOP_1:72;
u in {bg} by A29,TARSKI:def 1;
then u in dom(bg.-->0.L);
then
A31: p9.u = (bg.-->0.L).bg by A9,A29,FUNCT_4:13;
(p9+m).u = p9.u + m.u by POLYNOM1:15
.= 0.L + p.bg by A29,A31,A30,FUNCOP_1:72
.= p.bg by RLVECT_1:def 4;
hence thesis by A29;
end;
suppose
u <> bg;
then
A32: not u in {bg} by TARSKI:def 1;
then
A33: not u in dom(bg.-->0.L);
not u in dom(bg.-->p.bg) by A32;
then m.u = 0_(n,L).u by A22,FUNCT_4:11;
then
A34: m.u = 0.L by POLYNOM1:22;
(p9+m).u = p9.u + m.u by POLYNOM1:15
.= p.u + 0.L by A9,A33,A34,FUNCT_4:11
.= p.u by RLVECT_1:def 4;
hence thesis;
end;
end;
A35: dom(p9 + m) = Bags n by FUNCT_2:def 1;
then eval(p,x) = eval(m+p9,x) by A12,A28,FUNCT_1:2
.= eval(p9,x) + eval(m,x) by A27,Lm7;
hence eval(p,x) + eval(q,x) = (eval(p9,x) + eval(q,x)) + eval(m,x) by
RLVECT_1:def 3
.= eval(p9+q,x) + eval(m,x) by A3,A21
.= eval(m+(p9+q),x) by A27,Lm7
.= eval((p9+m)+q,x) by POLYNOM1:21
.= eval(p+q,x) by A35,A12,A28,FUNCT_1:2;
end;
A36: P[0]
proof
let p be Polynomial of n,L;
assume card(Support p) = 0;
then Support p = {};
then
A37: p = 0_(n,L) by Th9;
hence eval(p+q,x) = eval(q,x) by POLYNOM1:23
.= 0.L + eval(q,x) by RLVECT_1:4
.= eval(p,x) + eval(q,x) by A37,Th12;
end;
for k being Nat holds P[k] from NAT_1:sch 2(A36,A2);
hence thesis by A1;
end;
theorem
for n being Ordinal, L being right_zeroed add-associative
right_complementable Abelian well-unital distributive non trivial
doubleLoopStr, p,q being Polynomial of n,L, x being Function of n, L holds
eval(p-q,x) = eval(p,x) - eval(q,x)
proof
let n be Ordinal, L be right_zeroed add-associative right_complementable
Abelian well-unital distributive non trivial doubleLoopStr, p,q be
Polynomial of n,L, x be Function of n, L;
thus eval(p-q,x) = eval(p + -q,x) by POLYNOM1:def 7
.= eval(p,x) + eval(-q,x) by Th15
.= eval(p,x) - eval(q,x) by Th14;
end;
Lm8: for n being Ordinal, L being right_zeroed add-associative
right_complementable Abelian well-unital distributive non trivial commutative
associative non empty doubleLoopStr, p,q being Polynomial of n,L, b1, b2
being bag of n st Support p = {b1} & Support q = {b2} for x being Function of n
, L holds eval(p*'q,x) = eval(p,x) * eval(q,x)
proof
let n be Ordinal, L be right_zeroed add-associative right_complementable
Abelian well-unital distributive commutative associative non trivial
doubleLoopStr, p,q be Polynomial of n,L, b1, b2 be bag of n;
assume that
A1: Support p = {b1} and
A2: Support q = {b2};
consider s being FinSequence of the carrier of L such that
A3: (p*'q).(b1+b2) = Sum s and
A4: len s = len decomp(b1+b2) and
A5: for k being Element of NAT st k in dom s ex u1,u2 being bag of n st
(decomp(b1+b2))/.k = <*u1,u2*> & s/.k = p.u1 * q.u2 by POLYNOM1:def 10;
A6: b1+b2 is Element of Bags n by PRE_POLY:def 12;
let x be Function of n, L;
A7: (p.b1 * q.b2) * (eval(b1,x) * eval(b2,x)) = ((p.b1 * q.b2) * eval(b1,x)
) * eval(b2,x) by GROUP_1:def 3
.= ((p.b1 * eval(b1,x)) * q.b2) * eval(b2,x) by GROUP_1:def 3
.= (p.b1 * eval(b1,x)) * (q.b2 * eval(b2,x)) by GROUP_1:def 3
.= eval(p,x) * (q.b2 * eval(b2,x)) by A1,Th11
.= eval(p,x) * eval(q,x) by A2,Th11;
A8: for b being bag of n st b <> b2 holds q.b = 0.L
proof
let b be bag of n;
assume b <> b2;
then
A9: not b in Support q by A2,TARSKI:def 1;
b is Element of Bags n by PRE_POLY:def 12;
hence thesis by A9,POLYNOM1:def 4;
end;
A10: for b being bag of n st b <> b1 holds p.b = 0.L
proof
let b be bag of n;
assume b <> b1;
then
A11: not b in Support p by A1,TARSKI:def 1;
b is Element of Bags n by PRE_POLY:def 12;
hence thesis by A11,POLYNOM1:def 4;
end;
A12: for u being object holds u in Support(p*'q) implies u in {b1+b2}
proof
let u be object;
assume
A13: u in Support(p*'q);
assume
A14: not u in {b1+b2};
reconsider u as bag of n by A13;
consider t being FinSequence of the carrier of L such that
A15: (p*'q).u = Sum t and
A16: len t = len decomp u and
A17: for k being Element of NAT st k in dom t ex b19,b29 being bag of
n st (decomp u)/.k = <*b19,b29*> & t/.k = p.b19 * q.b29 by POLYNOM1:def 10;
1 <= len t by A16,NAT_1:14;
then
A18: 1 in dom t by FINSEQ_3:25;
A19: dom t = Seg len t by FINSEQ_1:def 3
.= dom decomp u by A16,FINSEQ_1:def 3;
A20: for i being Element of NAT st i in dom t holds t/.i = 0.L
proof
let i be Element of NAT;
consider S being non empty finite Subset of Bags n such that
A21: divisors u = SgmX(BagOrder n, S) and
A22: for b being bag of n holds b in S iff b divides u by PRE_POLY:def 16;
BagOrder n linearly_orders S by Lm3;
then
A23: S = rng(divisors u) by A21,PRE_POLY:def 2;
assume
A24: i in dom t;
then consider b19,b29 being bag of n such that
A25: (decomp u)/.i = <*b19,b29*> and
A26: t/.i = p.b19 * q.b29 by A17;
A27: b19 = (divisors u)/.i by A19,A24,A25,PRE_POLY:70;
A28: i in dom(divisors u) by A19,A24,PRE_POLY:def 17;
then b19 = (divisors u).i by A27,PARTFUN1:def 6;
then b19 in rng(divisors u) by A28,FUNCT_1:def 3;
then
A29: b19 divides u by A22,A23;
per cases;
suppose
A30: b19 = b1 & b29 = b2;
b2 = <*b1,b2*>.2
.= <*b1,u-'b1*>.2 by A19,A24,A25,A27,A30,PRE_POLY:def 17
.= u-'b1;
then b1 + b2 = u by A29,A30,PRE_POLY:47;
hence thesis by A14,TARSKI:def 1;
end;
suppose
b19 <> b1;
then p.b19 = 0.L by A10;
hence thesis by A26;
end;
suppose
b29 <> b2;
then q.b29 = 0.L by A8;
hence thesis by A26;
end;
end;
then for i being Element of NAT st i in dom t & i <> 1 holds t/.i = 0.L;
then Sum t = t/.1 by A18,Th2
.= 0.L by A18,A20;
hence thesis by A13,A15,POLYNOM1:def 4;
end;
consider k being Element of NAT such that
A31: k in dom decomp(b1+b2) and
A32: (decomp(b1+b2))/.k = <*b1,b2*> by PRE_POLY:69;
A33: dom s = Seg(len s) by FINSEQ_1:def 3
.= dom decomp(b1+b2) by A4,FINSEQ_1:def 3;
then consider b19,b29 being bag of n such that
A34: (decomp(b1+b2))/.k = <*b19,b29*> and
A35: s/.k = p.b19 * q.b29 by A5,A31;
A36: b2 = <*b1,b2*>.2
.= b29 by A32,A34,FINSEQ_1:44;
A37: for k9 being Element of NAT st k9 in dom s & k9 <> k holds s/.k9 = 0.L
proof
let k9 be Element of NAT;
assume that
A38: k9 in dom s and
A39: k9 <> k;
consider b19,b29 being bag of n such that
A40: (decomp(b1+b2))/.k9 = <*b19,b29*> and
A41: s/.k9 = p.b19 * q.b29 by A5,A38;
per cases;
suppose
A42: b19 = b1 & b29 = b2;
(decomp(b1+b2)).k9 = (decomp(b1+b2))/.k9 by A33,A38,PARTFUN1:def 6
.= (decomp(b1+b2)).k by A31,A32,A40,A42,PARTFUN1:def 6;
hence thesis by A33,A31,A38,A39,FUNCT_1:def 4;
end;
suppose
b19 <> b1;
then p.b19 = 0.L by A10;
hence thesis by A41;
end;
suppose
b29 <> b2;
then q.b29 = 0.L by A8;
hence thesis by A41;
end;
end;
b1 = <*b19,b29*>.1 by A32,A34
.= b19;
then
A43: (p*'q).(b1+b2) = p.b1 * q.b2 by A3,A33,A31,A35,A36,A37,Th2;
per cases;
suppose
A44: p.b1 * q.b2 = 0.L;
then
A45: not b1+b2 in Support(p*'q) by A43,POLYNOM1:def 4;
Support(p*'q) = {}
proof
set u = the Element of Support(p*'q);
assume
A46: Support(p*'q) <> {};
then
A47: u in Support(p*'q);
u in {b1+b2} by A12,A46;
hence thesis by A45,A47,TARSKI:def 1;
end;
then p*'q = 0_(n,L) by Th9;
hence eval(p*'q,x) = eval(p,x) * eval(q,x) by A7,A44,Th12;
end;
suppose
p.b1 * q.b2 <> 0.L;
then b1+b2 in Support(p*'q) by A43,A6,POLYNOM1:def 4;
then for u being object holds u in {b1+b2} implies u in Support(p*'q)
by TARSKI:def 1;
then Support(p*'q) = {b1+b2} by A12,TARSKI:2;
hence eval(p*'q,x) = (p*'q).(b1+b2) * eval(b1+b2,x) by Th11
.= eval(p,x) * eval(q,x) by A43,A7,Th8;
end;
end;
Lm9: for n being Ordinal, L being right_zeroed add-associative
right_complementable Abelian well-unital distributive non trivial commutative
associative non empty doubleLoopStr, q being Polynomial of n,L st ex b being
bag of n st Support q = {b} for p being Polynomial of n,L, x being Function of
n, L holds eval(p*'q,x) = eval(p,x) * eval(q,x)
proof
let n be Ordinal, L be right_zeroed add-associative right_complementable
Abelian well-unital distributive commutative associative non trivial
doubleLoopStr, q be Polynomial of n,L;
given b being bag of n such that
A1: Support q = {b};
let p be Polynomial of n,L;
let x be Function of n, L;
defpred P[Nat] means for p being Polynomial of n,L st card(
Support p) = $1 holds eval(p*'q,x) = eval(p,x) * eval(q,x);
A2: for k being Nat st P[k] holds P[k + 1]
proof
let k be Nat;
assume
A3: P[k];
let p be Polynomial of n,L;
assume
A4: card(Support p) = k + 1;
set sgp = SgmX(BagOrder n, Support p);
set bg = sgp/.(len sgp);
A5: BagOrder n linearly_orders Support p by Th10;
then sgp <> {} by A4,CARD_1:27,PRE_POLY:def 2,RELAT_1:38;
then 1 <= len sgp by NAT_1:14;
then len sgp in Seg(len sgp) by FINSEQ_1:1;
then
A6: len sgp in dom sgp by FINSEQ_1:def 3;
then sgp/.(len sgp) = sgp.(len sgp) by PARTFUN1:def 6;
then bg in rng sgp by A6,FUNCT_1:def 3;
then
A7: bg in Support p by A5,PRE_POLY:def 2;
then
A8: p.bg <> 0.L by POLYNOM1:def 4;
set m = 0_(n,L)+*(bg,p.bg);
set p9 = p+*(bg,0.L);
reconsider bg as bag of n;
dom p = Bags n by FUNCT_2:def 1;
then
A9: p9 = p+*(bg.-->0.L) by FUNCT_7:def 3;
reconsider p9 as Function of Bags n,the carrier of L;
reconsider p9 as Function of Bags n,L;
for u being object holds u in Support p9 implies u in Support p
proof
let u be object;
assume
A10: u in Support p9;
then reconsider u as Element of Bags n;
reconsider u as bag of n;
now
assume
A11: u = bg;
then u in {bg} by TARSKI:def 1;
then u in dom(bg.-->0.L);
then p9.u = (bg.-->0.L).bg by A9,A11,FUNCT_4:13;
then p9.u = 0.L by FUNCOP_1:72;
hence contradiction by A10,POLYNOM1:def 4;
end;
then not u in {bg} by TARSKI:def 1;
then not u in dom(bg.-->0.L);
then p.u = p9.u by A9,FUNCT_4:11;
then p.u <> 0.L by A10,POLYNOM1:def 4;
hence thesis by POLYNOM1:def 4;
end;
then Support p9 c= Support p by TARSKI:def 3;
then reconsider p9 as Polynomial of n,L by POLYNOM1:def 5;
A12: dom p = Bags n by FUNCT_2:def 1;
A13: for u being object holds u in Support p implies u in Support p9 \/ {bg}
proof
let u be object;
assume
A14: u in Support p;
then reconsider u as Element of Bags n;
A15: p.u <> 0.L by A14,POLYNOM1:def 4;
per cases;
suppose
u = bg;
then u in {bg} by TARSKI:def 1;
hence thesis by XBOOLE_0:def 3;
end;
suppose
u <> bg;
then not u in {bg} by TARSKI:def 1;
then not u in dom(bg.-->0.L);
then p9.u = p.u by A9,FUNCT_4:11;
then u in Support p9 by A15,POLYNOM1:def 4;
hence thesis by XBOOLE_0:def 3;
end;
end;
bg in {bg} by TARSKI:def 1;
then bg in dom(bg.-->0.L);
then p9.bg = (bg.-->0.L).bg by A9,FUNCT_4:13;
then
A16: p9.bg = 0.L by FUNCOP_1:72;
then
A17: not bg in Support p9 by POLYNOM1:def 4;
for u being object holds u in Support p9 \/ {bg} implies u in Support p
proof
let u be object;
assume
A18: u in Support p9 \/ {bg};
per cases by A18,XBOOLE_0:def 3;
suppose
A19: u in Support p9;
then reconsider u as Element of Bags n;
u <> bg by A16,A19,POLYNOM1:def 4;
then not u in {bg} by TARSKI:def 1;
then not u in dom(bg.-->0.L);
then
A20: p9.u = p.u by A9,FUNCT_4:11;
p9.u <> 0.L by A19,POLYNOM1:def 4;
hence thesis by A20,POLYNOM1:def 4;
end;
suppose
u in {bg};
hence thesis by A7,TARSKI:def 1;
end;
end;
then Support p = Support p9 \/ {bg} by A13,TARSKI:2;
then
A21: k + 1 = card(Support p9) + 1 by A4,A17,CARD_2:41;
dom 0_(n,L) = Bags n by FUNCT_2:def 1;
then
A22: m = 0_(n,L)+*(bg.-->p.bg) by FUNCT_7:def 3;
reconsider m as Function of Bags n,the carrier of L;
reconsider m as Function of Bags n,L;
A23: for u being object holds u in Support m implies u in {bg}
proof
let u be object;
assume
A24: u in Support m;
then reconsider u as Element of Bags n;
A25: m.u <> 0.L by A24,POLYNOM1:def 4;
now
assume u <> bg;
then not u in {bg} by TARSKI:def 1;
then not u in dom(bg.-->p.bg);
then m.u = 0_(n,L).u by A22,FUNCT_4:11;
hence contradiction by A25,POLYNOM1:22;
end;
hence thesis by TARSKI:def 1;
end;
for u being object holds u in {bg} implies u in Support m
proof
let u be object;
bg in {bg} by TARSKI:def 1;
then bg in dom(bg.-->p.bg);
then m.bg = (bg.-->p.bg).bg by A22,FUNCT_4:13;
then
A26: m.bg = p.bg by FUNCOP_1:72;
assume u in {bg};
then u = bg by TARSKI:def 1;
hence thesis by A8,A26,POLYNOM1:def 4;
end;
then
A27: Support m = {bg} by A23,TARSKI:2;
then reconsider m as Polynomial of n,L by POLYNOM1:def 5;
reconsider m as Polynomial of n,L;
A28: for u being object st u in Bags n holds (p9+m).u = p.u
proof
let u be object;
assume u in Bags n;
then reconsider u as bag of n;
per cases;
suppose
A29: u = bg;
bg in {bg} by TARSKI:def 1;
then bg in dom(bg.-->p.bg);
then m.bg = (bg.-->p.bg).bg by A22,FUNCT_4:13;
then
A30: m.bg = p.bg by FUNCOP_1:72;
u in {bg} by A29,TARSKI:def 1;
then u in dom(bg.-->0.L);
then
A31: p9.u = (bg.-->0.L).bg by A9,A29,FUNCT_4:13;
(p9+m).u = p9.u + m.u by POLYNOM1:15
.= 0.L + p.bg by A29,A31,A30,FUNCOP_1:72
.= p.bg by RLVECT_1:def 4;
hence thesis by A29;
end;
suppose
u <> bg;
then
A32: not u in {bg} by TARSKI:def 1;
then
A33: not u in dom(bg.-->0.L);
not u in dom(bg.-->p.bg) by A32;
then m.u = 0_(n,L).u by A22,FUNCT_4:11;
then
A34: m.u = 0.L by POLYNOM1:22;
(p9+m).u = p9.u + m.u by POLYNOM1:15
.= p.u + 0.L by A9,A33,A34,FUNCT_4:11
.= p.u by RLVECT_1:def 4;
hence thesis;
end;
end;
A35: dom(p9 + m) = Bags n by FUNCT_2:def 1;
then eval(p,x) = eval(m+p9,x) by A12,A28,FUNCT_1:2
.= eval(p9,x) + eval(m,x) by A27,Lm7;
hence
eval(p,x) * eval(q,x) = eval(p9,x)*eval(q,x) + eval(m,x)*eval(q,x) by
VECTSP_1:def 7
.= eval(p9*'q,x) + eval(m,x)*eval(q,x) by A3,A21
.= eval(p9*'q,x)+eval(m*'q,x) by A1,A27,Lm8
.= eval(p9*'q+m*'q,x) by Th15
.= eval(q*'(p9+m),x) by POLYNOM1:26
.= eval(p*'q,x) by A35,A12,A28,FUNCT_1:2;
end;
A36: ex k being Element of NAT st card(Support p) = k;
A37: P[0]
proof
let p be Polynomial of n,L;
assume card(Support p) = 0;
then Support p ={};
then
A38: p = 0_(n,L) by Th9;
hence eval(p*'q,x) = eval(p,x) by POLYNOM1:28
.= 0.L * eval(q,x) by A38,Th12
.= eval(p,x) * eval(q,x) by A38,Th12;
end;
for k being Nat holds P[k] from NAT_1:sch 2(A37,A2);
hence thesis by A36;
end;
theorem Th17:
for n being Ordinal, L being right_zeroed add-associative
right_complementable Abelian well-unital distributive non trivial commutative
associative non empty doubleLoopStr, p,q being Polynomial of n,L, x being
Function of n, L holds eval(p*'q,x) = eval(p,x) * eval(q,x)
proof
let n be Ordinal, L be right_zeroed add-associative right_complementable
Abelian well-unital distributive commutative associative non trivial
doubleLoopStr, p,q be Polynomial of n,L, x be Function of n, L;
defpred P[Nat] means for p being Polynomial of n,L st card(
Support p) = $1 holds eval(p*'q,x) = eval(p,x) * eval(q,x);
A1: ex k being Element of NAT st card(Support p) = k;
A2: for k being Nat st P[k] holds P[k + 1]
proof
let k be Nat;
assume
A3: P[k];
let p be Polynomial of n,L;
assume
A4: card(Support p) = k + 1;
set sgp = SgmX(BagOrder n, Support p);
set bg = sgp/.(len sgp);
A5: BagOrder n linearly_orders Support p by Th10;
then sgp <> {} by A4,CARD_1:27,PRE_POLY:def 2,RELAT_1:38;
then 1 <= len sgp by NAT_1:14;
then len sgp in Seg(len sgp) by FINSEQ_1:1;
then
A6: len sgp in dom sgp by FINSEQ_1:def 3;
then sgp/.(len sgp) = sgp.(len sgp) by PARTFUN1:def 6;
then bg in rng sgp by A6,FUNCT_1:def 3;
then
A7: bg in Support p by A5,PRE_POLY:def 2;
then
A8: p.bg <> 0.L by POLYNOM1:def 4;
set m = 0_(n,L)+*(bg,p.bg);
set p9 = p+*(bg,0.L);
reconsider bg as bag of n;
dom p = Bags n by FUNCT_2:def 1;
then
A9: p9 = p+*(bg.-->0.L) by FUNCT_7:def 3;
reconsider p9 as Function of Bags n,L;
for u being object holds u in Support p9 implies u in Support p
proof
let u be object;
assume
A10: u in Support p9;
then reconsider u as Element of Bags n;
reconsider u as bag of n;
now
assume
A11: u = bg;
then u in {bg} by TARSKI:def 1;
then u in dom(bg.-->0.L);
then p9.u = (bg.-->0.L).bg by A9,A11,FUNCT_4:13;
then p9.u = 0.L by FUNCOP_1:72;
hence contradiction by A10,POLYNOM1:def 4;
end;
then not u in {bg} by TARSKI:def 1;
then not u in dom(bg.-->0.L);
then p.u = p9.u by A9,FUNCT_4:11;
then p.u <> 0.L by A10,POLYNOM1:def 4;
hence thesis by POLYNOM1:def 4;
end;
then Support p9 c= Support p by TARSKI:def 3;
then reconsider p9 as Polynomial of n,L by POLYNOM1:def 5;
A12: dom p = Bags n by FUNCT_2:def 1;
A13: for u being object holds u in Support p implies u in Support p9 \/ {bg}
proof
let u be object;
assume
A14: u in Support p;
then reconsider u as Element of Bags n;
A15: p.u <> 0.L by A14,POLYNOM1:def 4;
per cases;
suppose
u = bg;
then u in {bg} by TARSKI:def 1;
hence thesis by XBOOLE_0:def 3;
end;
suppose
u <> bg;
then not u in {bg} by TARSKI:def 1;
then not u in dom(bg.-->0.L);
then p9.u = p.u by A9,FUNCT_4:11;
then u in Support p9 by A15,POLYNOM1:def 4;
hence thesis by XBOOLE_0:def 3;
end;
end;
bg in {bg} by TARSKI:def 1;
then bg in dom(bg.-->0.L);
then p9.bg = (bg.-->0.L).bg by A9,FUNCT_4:13;
then
A16: p9.bg = 0.L by FUNCOP_1:72;
then
A17: not bg in Support p9 by POLYNOM1:def 4;
for u being object holds u in Support p9 \/ {bg} implies u in Support p
proof
let u be object;
assume
A18: u in Support p9 \/ {bg};
per cases by A18,XBOOLE_0:def 3;
suppose
A19: u in Support p9;
then reconsider u as Element of Bags n;
u <> bg by A16,A19,POLYNOM1:def 4;
then not u in {bg} by TARSKI:def 1;
then not u in dom(bg.-->0.L);
then
A20: p9.u = p.u by A9,FUNCT_4:11;
p9.u <> 0.L by A19,POLYNOM1:def 4;
hence thesis by A20,POLYNOM1:def 4;
end;
suppose
u in {bg};
hence thesis by A7,TARSKI:def 1;
end;
end;
then Support p = Support p9 \/ {bg} by A13,TARSKI:2;
then
A21: k + 1 = card(Support p9) + 1 by A4,A17,CARD_2:41;
dom 0_(n,L) = Bags n by FUNCT_2:def 1;
then
A22: m = 0_(n,L)+*(bg.-->p.bg) by FUNCT_7:def 3;
reconsider m as Function of Bags n,the carrier of L;
reconsider m as Function of Bags n,L;
A23: for u being object holds u in Support m implies u in {bg}
proof
let u be object;
assume
A24: u in Support m;
then reconsider u as Element of Bags n;
A25: m.u <> 0.L by A24,POLYNOM1:def 4;
now
assume u <> bg;
then not u in {bg} by TARSKI:def 1;
then not u in dom(bg.-->p.bg);
then m.u = 0_(n,L).u by A22,FUNCT_4:11;
hence contradiction by A25,POLYNOM1:22;
end;
hence thesis by TARSKI:def 1;
end;
for u being object holds u in {bg} implies u in Support m
proof
let u be object;
bg in {bg} by TARSKI:def 1;
then bg in dom(bg.-->p.bg);
then m.bg = (bg.-->p.bg).bg by A22,FUNCT_4:13;
then
A26: m.bg = p.bg by FUNCOP_1:72;
assume u in {bg};
then u = bg by TARSKI:def 1;
hence thesis by A8,A26,POLYNOM1:def 4;
end;
then
A27: Support m = {bg} by A23,TARSKI:2;
then reconsider m as Polynomial of n,L by POLYNOM1:def 5;
reconsider m as Polynomial of n,L;
A28: for u being object st u in Bags n holds (p9+m).u = p.u
proof
let u be object;
assume u in Bags n;
then reconsider u as bag of n;
per cases;
suppose
A29: u = bg;
bg in {bg} by TARSKI:def 1;
then bg in dom(bg.-->p.bg);
then m.bg = (bg.-->p.bg).bg by A22,FUNCT_4:13;
then
A30: m.bg = p.bg by FUNCOP_1:72;
u in {bg} by A29,TARSKI:def 1;
then u in dom(bg.-->0.L);
then
A31: p9.u = (bg.-->0.L).bg by A9,A29,FUNCT_4:13;
(p9+m).u = p9.u + m.u by POLYNOM1:15
.= 0.L + p.bg by A29,A31,A30,FUNCOP_1:72
.= p.bg by RLVECT_1:def 4;
hence thesis by A29;
end;
suppose
u <> bg;
then
A32: not u in {bg} by TARSKI:def 1;
then
A33: not u in dom(bg.-->0.L);
not u in dom(bg.-->p.bg) by A32;
then m.u = 0_(n,L).u by A22,FUNCT_4:11;
then
A34: m.u = 0.L by POLYNOM1:22;
(p9+m).u = p9.u + m.u by POLYNOM1:15
.= p.u + 0.L by A9,A33,A34,FUNCT_4:11
.= p.u by RLVECT_1:def 4;
hence thesis;
end;
end;
A35: dom(p9 + m) = Bags n by FUNCT_2:def 1;
then eval(p,x) = eval(m+p9,x) by A12,A28,FUNCT_1:2
.= eval(p9,x) + eval(m,x) by A27,Lm7;
hence
eval(p,x) * eval(q,x) = eval(p9,x)*eval(q,x) + eval(m,x)*eval(q,x) by
VECTSP_1:def 7
.= eval(p9*'q,x) + eval(m,x)*eval(q,x) by A3,A21
.= eval(p9*'q,x)+eval(m*'q,x) by A27,Lm9
.= eval(p9*'q+m*'q,x) by Th15
.= eval(q*'(p9+m),x) by POLYNOM1:26
.= eval(p*'q,x) by A35,A12,A28,FUNCT_1:2;
end;
A36: P[0]
proof
let p be Polynomial of n,L;
assume card(Support p) = 0;
then Support p = {};
then
A37: p = 0_(n,L) by Th9;
hence eval(p*'q,x) = eval(p,x) by POLYNOM1:28
.= 0.L * eval(q,x) by A37,Th12
.= eval(p,x) * eval(q,x) by A37,Th12;
end;
for k being Nat holds P[k] from NAT_1:sch 2(A36,A2);
hence thesis by A1;
end;
begin :: Evaluation Homomorphism --------------------------------------------------
definition
let n be Ordinal, L be right_zeroed add-associative right_complementable
well-unital distributive non trivial doubleLoopStr, x be Function
of n, L;
func Polynom-Evaluation(n,L,x) -> Function of Polynom-Ring(n,L),L means
:
Def3: for p being Polynomial of n,L holds it.p = eval(p,x);
existence
proof
defpred P[object,object] means
ex p9 being Polynomial of n,L st p9 = $1 & $2 = eval(p9,x);
A1: now
let p be object;
assume p in the carrier of Polynom-Ring(n,L);
then reconsider p9 = p as Polynomial of n,L by POLYNOM1:def 11;
thus ex y being object st y in the carrier of L & P[p,y]
proof
take eval(p9,x);
thus thesis;
end;
end;
consider f being Function of the carrier of Polynom-Ring(n,L), the carrier
of L such that
A2: for x being object st x in the carrier of Polynom-Ring(n,L) holds P[x
,f.x] from FUNCT_2:sch 1(A1);
reconsider f as Function of Polynom-Ring(n,L),L;
take f;
let p be Polynomial of n,L;
p in the carrier of Polynom-Ring(n,L) by POLYNOM1:def 11;
then ex p9 being Polynomial of n,L st p9 = p & f.p = eval(p9,x) by A2;
hence thesis;
end;
uniqueness
proof
let f,g be Function of Polynom-Ring(n,L), L such that
A3: for p being Polynomial of n,L holds f.p = eval(p,x) and
A4: for p being Polynomial of n,L holds g.p = eval(p,x);
reconsider f,g as Function of the carrier of Polynom-Ring(n,L), the
carrier of L;
A5: now
let p be object;
assume p in the carrier of Polynom-Ring(n,L);
then reconsider p9 = p as Polynomial of n,L by POLYNOM1:def 11;
f.p9 = eval(p9,x) by A3
.= g.p9 by A4;
hence f.p = g.p;
end;
A6: dom g = the carrier of Polynom-Ring(n,L) by FUNCT_2:def 1;
dom f = the carrier of Polynom-Ring(n,L) by FUNCT_2:def 1;
hence thesis by A6,A5,FUNCT_1:2;
end;
end;
registration
let n be Ordinal, L be right_zeroed Abelian add-associative
right_complementable well-unital distributive associative non trivial non
empty doubleLoopStr;
cluster Polynom-Ring (n, L) -> well-unital;
coherence;
end;
registration
let n be Ordinal, L be Abelian right_zeroed add-associative
right_complementable well-unital distributive associative non trivial non
empty doubleLoopStr, x be Function of n, L;
cluster Polynom-Evaluation(n,L,x) -> unity-preserving;
coherence
proof
set f = Polynom-Evaluation(n,L,x);
thus f.(1_(Polynom-Ring(n,L))) = f.(1_(n,L)) by POLYNOM1:31
.= eval(1_(n,L),x) by Def3
.= 1_L by Th13;
end;
end;
registration
let n be Ordinal, L be right_zeroed add-associative right_complementable
Abelian well-unital distributive non trivial doubleLoopStr, x be
Function of n, L;
cluster Polynom-Evaluation(n,L,x) -> additive;
coherence
proof
set f = Polynom-Evaluation(n,L,x);
for p,q being Element of Polynom-Ring(n,L) holds f.(p+q) = f.p + f.q
proof
let p,q be Element of Polynom-Ring(n,L);
reconsider p9 = p, q9 = q as Polynomial of n,L by POLYNOM1:def 11;
reconsider p,q as Element of Polynom-Ring(n,L);
A1: f.p = eval(p9,x) by Def3;
f.(p + q) = f.(p9+q9) by POLYNOM1:def 11
.= eval(p9+q9,x) by Def3
.= eval(p9,x) + eval(q9,x) by Th15;
hence thesis by A1,Def3;
end;
hence thesis by VECTSP_1:def 20;
end;
end;
registration
let n be Ordinal, L be right_zeroed add-associative right_complementable
Abelian well-unital distributive commutative associative non trivial
doubleLoopStr, x be Function of n, L;
cluster Polynom-Evaluation(n,L,x) -> multiplicative;
coherence
proof
set f = Polynom-Evaluation(n,L,x);
for p,q being Element of Polynom-Ring(n,L) holds f.(p * q) = f.p * f.q
proof
let p,q be Element of Polynom-Ring(n,L);
reconsider p9 = p, q9 = q as Polynomial of n,L by POLYNOM1:def 11;
reconsider p,q as Element of Polynom-Ring(n,L);
A1: f.p = eval(p9,x) by Def3;
f.(p * q) = f.(p9*'q9) by POLYNOM1:def 11
.= eval(p9*'q9,x) by Def3
.= eval(p9,x) * eval(q9,x) by Th17;
hence thesis by A1,Def3;
end;
hence thesis by GROUP_6:def 6;
end;
end;
registration
let n be Ordinal, L be right_zeroed add-associative right_complementable
Abelian well-unital distributive commutative associative non trivial
doubleLoopStr, x be Function of n, L;
cluster Polynom-Evaluation(n,L,x) -> RingHomomorphism;
coherence;
end;