:: Evaluation of Polynomials
:: by Robert Milewski
::
:: Received June 7, 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, FINSEQ_1, SUBSET_1, XXREAL_0, RELAT_1,
ARYTM_1, ORDINAL4, FUNCT_1, RFINSEQ, ALGSTR_1, ALGSTR_0, VECTSP_1,
SUPINF_2, ARYTM_3, VECTSP_2, BINOP_1, MESFUNC1, STRUCT_0, RLVECT_1,
LATTICES, GROUP_1, ZFMISC_1, NAT_1, POLYNOM3, CARD_3, CARD_1, ALGSEQ_1,
POLYNOM1, TARSKI, PARTFUN1, FUNCT_4, POLYNOM2, FINSEQ_2, MSSUBFAM,
QUOFIELD, POLYNOM4;
notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, RELAT_1,
FUNCT_1, PARTFUN1, FUNCT_2, BINOP_1, FINSEQ_1, NAT_1, STRUCT_0, ALGSTR_0,
FINSEQ_2, FUNCT_7, RFINSEQ, NAT_D, RLVECT_1, VFUNCT_1, GROUP_1, VECTSP_1,
VECTSP_2, NORMSP_1, FVSUM_1, ALGSTR_1, GRCAT_1, QUOFIELD, ALGSEQ_1,
POLYNOM3, GROUP_6, XXREAL_0;
constructors FINSEQOP, RFINSEQ, NAT_D, ALGSEQ_1, GRCAT_1, GROUP_6, QUOFIELD,
POLYNOM3, REAL_1, ALGSTR_1, RELSET_1, FUNCT_7, FVSUM_1, VFUNCT_1,
RINGCAT1;
registrations ORDINAL1, RELSET_1, XXREAL_0, XREAL_0, NAT_1, INT_1, FINSEQ_1,
FINSEQ_2, STRUCT_0, VECTSP_1, ALGSTR_1, POLYNOM3, ALGSTR_0, CARD_1,
VFUNCT_1, FUNCT_2, RINGCAT1;
requirements NUMERALS, SUBSET, REAL, BOOLE, ARITHM;
definitions ALGSEQ_1, GROUP_1, VECTSP_1, GROUP_6;
equalities POLYNOM3, FINSEQ_2;
expansions ALGSEQ_1, VECTSP_1;
theorems NAT_1, FUNCT_2, FUNCT_7, FUNCOP_1, FINSEQ_1, FINSEQ_2, FINSEQ_3,
FINSEQ_4, FINSEQ_5, RFINSEQ, RLVECT_1, VECTSP_1, VECTSP_2, FVSUM_1,
NORMSP_1, ALGSEQ_1, GROUP_1, POLYNOM2, POLYNOM3, INT_1, NAT_2, MATRIX_3,
ALGSTR_1, XREAL_1, XXREAL_0, BHSP_1, PARTFUN1, ORDINAL1, ALGSTR_0,
XREAL_0, CARD_1;
schemes NAT_1, FINSEQ_2, POLYNOM3, FUNCT_2;
begin
theorem
for D be non empty set for p be FinSequence of D for n be Element of
NAT st 1 <= n & n <= len p holds p = (p|(n-'1))^<*p.n*>^(p/^n) by FINSEQ_5:84;
Lm1: for R being left_zeroed right_add-cancelable right-distributive non
empty doubleLoopStr, a being Element of R holds a * 0.R = 0.R
proof
let R be left_zeroed right_add-cancelable right-distributive non empty
doubleLoopStr, a be Element of R;
a * 0.R = a * (0.R + 0.R) by ALGSTR_1:def 2
.= a * 0.R + a * 0.R by VECTSP_1:def 2;
then a * 0.R + a * 0.R = 0.R + a * 0.R by ALGSTR_1:def 2;
hence thesis by ALGSTR_0:def 4;
end;
registration
cluster almost_left_invertible -> domRing-like for left_zeroed
right_add-cancelable right-distributive well-unital associative
non empty doubleLoopStr;
coherence
proof
let L be left_zeroed right_add-cancelable right-distributive well-unital
associative non empty doubleLoopStr;
assume
A1: L is almost_left_invertible;
now
let x,y be Element of L;
assume
A2: x * y = 0.L;
thus x = 0.L or y = 0.L
proof
assume x <> 0.L;
then consider z being Element of L such that
A3: z * x = 1.L by A1;
z * 0.L = 1.L * y by A2,A3,GROUP_1:def 3
.= y;
hence thesis by Lm1;
end;
end;
hence thesis by VECTSP_2:def 1;
end;
end;
registration
cluster strict Abelian add-associative right_zeroed right_complementable
associative commutative distributive unital domRing-like almost_left_invertible
non degenerated for non empty doubleLoopStr;
existence
proof
set F = the non degenerated strict Field;
take F;
thus thesis;
end;
end;
begin :: About Polynomials
theorem Th2:
for L be add-associative right_zeroed right_complementable
left-distributive non empty doubleLoopStr for p be sequence of L holds (0_.(L
))*'p = 0_.(L)
proof
let L be add-associative right_zeroed right_complementable left-distributive
non empty doubleLoopStr;
let p be sequence of L;
now
let i be Element of NAT;
consider r be FinSequence of the carrier of L such that
len r = i+1 and
A1: ((0_.(L))*'p).i = Sum r and
A2: for k be Element of NAT st k in dom r holds r.k = (0_.(L)).(k-'1)
* p.(i+1-'k) by POLYNOM3:def 9;
now
let k be Element of NAT;
assume k in dom r;
hence r.k = (0_.(L)).(k-'1) * p.(i+1-'k) by A2
.= 0.L * p.(i+1-'k) by FUNCOP_1:7
.= 0.L;
end;
hence ((0_.(L))*'p).i = 0.L by A1,POLYNOM3:1
.= (0_.(L)).i by FUNCOP_1:7;
end;
hence thesis by FUNCT_2:63;
end;
theorem Th3:
for L be non empty ZeroStr holds len 0_.(L) = 0
proof
let L be non empty ZeroStr;
for i being Nat holds i >= 0 implies (0_.(L)).i = 0.L
by FUNCOP_1:7,ORDINAL1:def 12;
then 0 is_at_least_length_of 0_.(L);
hence thesis by ALGSEQ_1:def 3;
end;
theorem Th4:
for L be non degenerated non empty multLoopStr_0 holds len 1_.( L) = 1
proof
let L be non degenerated non empty multLoopStr_0;
A1: now
let i be Nat;
assume that
A2: i is_at_least_length_of 1_.(L) and
A3: 0+1 > i;
0 >= i by A3,NAT_1:13;
then (1_.(L)).0 = 0.L by A2;
hence contradiction by POLYNOM3:30;
end;
for i be Nat st i >= 1 holds (1_.(L)).i = 0.L by POLYNOM3:30;
then 1 is_at_least_length_of 1_.(L);
hence thesis by A1,ALGSEQ_1:def 3;
end;
theorem Th5:
for L be non empty ZeroStr for p be Polynomial of L st len p = 0
holds p = 0_.(L)
proof
let L be non empty ZeroStr;
let p be Polynomial of L;
assume len p = 0;
then
A1: 0 is_at_least_length_of p by ALGSEQ_1:def 3;
A2: now
let x be object;
assume x in dom p;
then reconsider i=x as Element of NAT by NORMSP_1:12;
i >= 0;
hence p.x = 0.L by A1;
end;
dom p = NAT by NORMSP_1:12;
hence thesis by A2,FUNCOP_1:11;
end;
theorem Th6:
for L be right_zeroed non empty addLoopStr for p,q be
Polynomial of L for n be Element of NAT st n >= len p & n >= len q holds n >=
len (p+q)
proof
let L be right_zeroed non empty addLoopStr;
let p,q be Polynomial of L;
let n be Element of NAT;
assume n >= len p & n >= len q;
then n is_at_least_length_of p & n is_at_least_length_of q by POLYNOM3:23;
then n is_at_least_length_of p+q by POLYNOM3:24;
hence thesis by POLYNOM3:23;
end;
theorem Th7:
for L be add-associative right_zeroed right_complementable non
empty addLoopStr for p,q be Polynomial of L st len p <> len q holds len (p+q)
= max(len p,len q)
proof
let L be add-associative right_zeroed right_complementable non empty
addLoopStr;
let p,q be Polynomial of L;
assume
A1: len p <> len q;
per cases by A1,XXREAL_0:1;
suppose
A2: len p < len q;
then len q >= len p+1 by NAT_1:13;
then len q-1 >= len p by XREAL_1:19;
then
A3: len q-'1 >= len p by XREAL_0:def 2;
len q >= 0+1 by A2,NAT_1:13;
then
A4: len q = len q-'1+1 by XREAL_1:235;
A5: (p+q).(len q-'1) = p.(len q-'1) + q.(len q-'1) by NORMSP_1:def 2
.= 0.L + q.(len q-'1) by A3,ALGSEQ_1:8
.= q.(len q-'1) by RLVECT_1:4;
A6: len (p+q) >= len q
proof
assume len (p+q) < len q;
then len (p+q) + 1 <= len q by NAT_1:13;
then len (p+q) <= len q - 1 by XREAL_1:19;
then len (p+q) <= len q-'1 by XREAL_0:def 2;
then (p+q).(len q-'1) = 0.L by ALGSEQ_1:8;
hence contradiction by A5,A4,ALGSEQ_1:10;
end;
max(len p,len q) = len q & len (p+q) <= len q by A2,Th6,XXREAL_0:def 10;
hence thesis by A6,XXREAL_0:1;
end;
suppose
A7: len p > len q;
then len p >= len q+1 by NAT_1:13;
then len p-1 >= len q by XREAL_1:19;
then
A8: len p-'1 >= len q by XREAL_0:def 2;
len p >= 0+1 by A7,NAT_1:13;
then
A9: len p = len p-'1+1 by XREAL_1:235;
A10: (p+q).(len p-'1) = p.(len p-'1) + q.(len p-'1) by NORMSP_1:def 2
.= p.(len p-'1) + 0.L by A8,ALGSEQ_1:8
.= p.(len p-'1) by RLVECT_1:4;
A11: len (p+q) >= len p
proof
assume len (p+q) < len p;
then len (p+q) + 1 <= len p by NAT_1:13;
then len (p+q) <= len p - 1 by XREAL_1:19;
then len (p+q) <= len p-'1 by XREAL_0:def 2;
then (p+q).(len p-'1) = 0.L by ALGSEQ_1:8;
hence contradiction by A10,A9,ALGSEQ_1:10;
end;
max(len p,len q) = len p & len (p+q) <= len p by A7,Th6,XXREAL_0:def 10;
hence thesis by A11,XXREAL_0:1;
end;
end;
theorem Th8:
for L be add-associative right_zeroed right_complementable non
empty addLoopStr for p be Polynomial of L holds len (-p) = len p
proof
let L be add-associative right_zeroed right_complementable non empty
addLoopStr;
let p be Polynomial of L;
A1: now
let n be Nat;
assume
A2: n is_at_least_length_of -p;
n is_at_least_length_of p
proof
let i be Nat;
assume i >= n;
then i in NAT & (-p).i = 0.L by A2,ORDINAL1:def 12;
then -p.i = 0.L by BHSP_1:44;
hence p.i = 0.L by VECTSP_2:3;
end;
hence len p <= n by ALGSEQ_1:def 3;
end;
len p is_at_least_length_of -p
proof
let i be Nat;
assume
A3: i >= len p;
thus (-p).i = -(p.i) by BHSP_1:44
.= -0.L by A3,ALGSEQ_1:8
.= 0.L by RLVECT_1:12;
end;
hence thesis by A1,ALGSEQ_1:def 3;
end;
theorem
for L be add-associative right_zeroed right_complementable non empty
addLoopStr for p,q be Polynomial of L for n be Element of NAT st n >= len p &
n >= len q holds n >= len (p-q)
proof
let L be add-associative right_zeroed right_complementable non empty
addLoopStr;
let p,q be Polynomial of L;
len q = len (-q) by Th8;
hence thesis by Th6;
end;
theorem
for L be add-associative right_zeroed right_complementable
distributive associative left_unital non empty doubleLoopStr, p,q
be Polynomial of L st p.(len p -'1) * q.(len q -'1) <> 0.L holds len (p*'q) =
len p + len q - 1
proof
let L be add-associative right_zeroed right_complementable distributive
associative left_unital non empty doubleLoopStr;
let p,q be Polynomial of L;
A1: len p + len q -' 1 is_at_least_length_of p*'q
proof
let i be Nat;
i in NAT by ORDINAL1:def 12;
then consider r be FinSequence of the carrier of L such that
A2: len r = i+1 and
A3: (p*'q).i = Sum r and
A4: for k be Element of NAT st k in dom r holds r.k = p.(k-'1) * q.(i
+1-'k) by POLYNOM3:def 9;
assume i >= len p + len q -' 1;
then i >= len p + len q - 1 by XREAL_0:def 2;
then i+1 >= len p + len q by XREAL_1:20;
then len p <= i+1 - len q by XREAL_1:19;
then
A5: -len p >= -(i+1 - len q) by XREAL_1:24;
now
let k be Element of NAT;
assume
A6: k in dom r;
then
A7: r.k = p.(k-'1) * q.(i+1-'k) by A4;
k in Seg len r by A6,FINSEQ_1:def 3;
then k <= i+1 by A2,FINSEQ_1:1;
then
A8: i+1-k >= 0 by XREAL_1:48;
per cases;
suppose
k-'1 < len p;
then k-1 < len p by XREAL_0:def 2;
then -(k-1) > -len p by XREAL_1:24;
then 1-k > len q - (i+1) by A5,XXREAL_0:2;
then i+1+(1-k) > len q by XREAL_1:19;
then i+1-k+1 > len q;
then i+1-'k+1 > len q by A8,XREAL_0:def 2;
then i+1-'k >= len q by NAT_1:13;
then q.(i+1-'k) = 0.L by ALGSEQ_1:8;
hence r.k = 0.L by A7;
end;
suppose
k-'1 >= len p;
then p.(k-'1) = 0.L by ALGSEQ_1:8;
hence r.k = 0.L by A7;
end;
end;
hence (p*'q).i = 0.L by A3,POLYNOM3:1;
end;
assume
A9: p.(len p -'1) * q.(len q -'1) <> 0.L;
A10: now
assume len p <= 0;
then len p = 0;
then p = 0_. L by Th5;
then p.(len p -'1) = 0.L by FUNCOP_1:7;
hence contradiction by A9;
end;
A11: now
assume len q <= 0;
then len q = 0;
then q = 0_. L by Th5;
then q.(len q -'1) = 0.L by FUNCOP_1:7;
hence contradiction by A9;
end;
then len p + len q >= 0+1 by NAT_1:13;
then
A12: len p + len q - 1 >= 1-1 by XREAL_1:9;
now
let n be Nat;
assume that
A13: n is_at_least_length_of p*'q and
A14: len p + len q -' 1 > n;
len p + len q -' 1 >= n+1 by A14,NAT_1:13;
then
A15: len p + len q -' 1 - 1 >= n by XREAL_1:19;
A16: len p + len q -' 1 - 1 = len p + len q - 1 - 1 by A12,XREAL_0:def 2;
A17: len q >= 0+1 by A11,NAT_1:13;
then
A18: len q - 1 >= 0 by XREAL_1:19;
len p + len q > 0+1 by A10,A17,XREAL_1:8;
then len p + len q >= 1+1 by NAT_1:13;
then
A19: len p + len q - 2 >= 2-2 by XREAL_1:9;
then
A20: len p + len q -' 2 = len p + len q - (1+1) by XREAL_0:def 2;
consider r be FinSequence of the carrier of L such that
A21: len r = len p + len q-'2+1 and
A22: (p*'q).(len p + len q-'2) = Sum r and
A23: for k be Element of NAT st k in dom r holds r.k = p.(k-'1) * q.(
len p + len q-'2+1-'k) by POLYNOM3:def 9;
A24: len r = len p + len q - 1 +- 1 + 1 by A21,A19,XREAL_0:def 2
.= len p + (len q - 1);
then
A25: len p+len q-'2+1-'(len p) = len p+len q-'2+1-(len p) by A21,A18,
XREAL_0:def 2
.= len q-'1 by A21,A18,A24,XREAL_0:def 2;
len r - (len p) = len q - 1 by A24;
then
A26: len p + 0 <= len r by A18,XREAL_1:19;
now
let i be Element of NAT;
assume
A27: i in dom (r/^len p);
then
A28: i in Seg len (r/^len p) by FINSEQ_1:def 3;
then
A29: 1 <= i by FINSEQ_1:1;
i+len p >= i by NAT_1:11;
then i+len p >= 0+1 by A29,XXREAL_0:2;
then i+len p-1 >= 0 by XREAL_1:19;
then
A30: i+len p-'1 = len p+(i-1) by XREAL_0:def 2;
0+1 <= i by A28,FINSEQ_1:1;
then i-1 >= 0 by XREAL_1:19;
then
A31: i+len p-'1 >= len p+0 by A30,XREAL_1:6;
i <= len (r/^len p) by A28,FINSEQ_1:1;
then i <= len r-len p by A26,RFINSEQ:def 1;
then
A32: i+len p <= len r by XREAL_1:19;
i+len p >= i by NAT_1:11;
then i+len p >= 1 by A29,XXREAL_0:2;
then i+len p in Seg len r by A32,FINSEQ_1:1;
then
A33: i+len p in dom r by FINSEQ_1:def 3;
thus (r/^len p).i = r.(i+len p) by A26,A27,RFINSEQ:def 1
.= p.(i+len p-'1) * q.(len p + len q-'2+1-'(i+len p)) by A23,A33
.= 0.L * q.(len p + len q-'2+1-'(i+len p)) by A31,ALGSEQ_1:8
.= 0.L;
end;
then
A34: Sum (r/^len p) = 0.L by POLYNOM3:1;
A35: len p >= 0+1 by A10,NAT_1:13;
then len p in Seg len r by A26,FINSEQ_1:1;
then
A36: len p in dom r by FINSEQ_1:def 3;
now
A37: len p - 1 >= 1-1 by A35,XREAL_1:9;
A38: len p + len q-'2+1 = len p - 1 + len q by A21,A24
.= len p -' 1 + len q by A37,XREAL_0:def 2;
A39: dom (r|((len p)-'1)) c= dom r by FINSEQ_5:18;
let i be Element of NAT;
assume
A40: i in dom (r|((len p)-'1));
len p < len r + 1 by A26,NAT_1:13;
then len p - 1 < len r + 1 - 1 by XREAL_1:9;
then (len p)-'1 < len r by A37,XREAL_0:def 2;
then len (r|((len p)-'1)) = (len p)-'1 by FINSEQ_1:59;
then i in Seg ((len p)-'1) by A40,FINSEQ_1:def 3;
then i <= (len p)-'1 by FINSEQ_1:1;
then i + len q <= (len p)-'1 + len q by XREAL_1:6;
then len q <= len p + len q-'2+1-i by A38,XREAL_1:19;
then
A41: len q <= len p + len q-'2+1-'i by XREAL_0:def 2;
thus (r|((len p)-'1)).i = (r|((len p)-'1))/.i by A40,PARTFUN1:def 6
.= r/.i by A40,FINSEQ_4:70
.= r.i by A40,A39,PARTFUN1:def 6
.= p.(i-'1) * q.(len p + len q-'2+1-'i) by A23,A40,A39
.= p.(i-'1) * 0.L by A41,ALGSEQ_1:8
.= 0.L;
end;
then
A42: Sum(r|((len p)-'1)) = 0.L by POLYNOM3:1;
r = (r|((len p)-'1))^<*r.(len p)*>^(r/^len p) by A26,A35,FINSEQ_5:84;
then r = (r|((len p)-'1))^<*r/.(len p)*>^(r/^len p) by A26,A35,FINSEQ_4:15;
then Sum r = Sum((r|((len p)-'1))^<*r/.(len p)*>) + Sum (r/^len p) by
RLVECT_1:41
.= Sum(r|((len p)-'1)) + Sum<*r/.(len p)*> + Sum (r/^len p) by
RLVECT_1:41;
then Sum r = Sum<*r/.(len p)*> + 0.L by A42,A34,RLVECT_1:4
.= Sum<*r/.(len p)*> by RLVECT_1:4
.= r/.(len p) by RLVECT_1:44
.= r.(len p) by A36,PARTFUN1:def 6
.= p.(len p-'1) * q.(len q-'1) by A23,A36,A25;
hence contradiction by A9,A13,A22,A16,A20,A15;
end;
then len (p*'q) = len p + len q -' 1 by A1,ALGSEQ_1:def 3;
hence thesis by A12,XREAL_0:def 2;
end;
begin :: Leading Monomials
definition
let L be non empty ZeroStr;
let p be Polynomial of L;
func Leading-Monomial(p) -> sequence of L means
:Def1:
it.(len p-'1) = p.(
len p-'1) & for n be Element of NAT st n <> len p-'1 holds it.n = 0.L;
existence
proof
reconsider P=0_.(L)+*(len p-'1,p.(len p-'1)) as sequence of L;
take P;
len p-'1 in NAT;
then len p-'1 in dom 0_.(L) by NORMSP_1:12;
hence P.(len p-'1) = p.(len p-'1) by FUNCT_7:31;
let n be Element of NAT;
assume n <> len p-'1;
hence P.n = (0_.(L)).n by FUNCT_7:32
.= 0.L by FUNCOP_1:7;
end;
uniqueness
proof
let P1,P2 be sequence of L such that
A1: P1.(len p-'1) = p.(len p-'1) and
A2: for n be Element of NAT st n <> len p-'1 holds P1.n = 0.L and
A3: P2.(len p-'1) = p.(len p-'1) and
A4: for n be Element of NAT st n <> len p-'1 holds P2.n = 0.L;
now
let i be Element of NAT;
per cases;
suppose
i = len p-'1;
hence P1.i = P2.i by A1,A3;
end;
suppose
A5: i <> len p-'1;
hence P1.i = 0.L by A2
.= P2.i by A4,A5;
end;
end;
hence P1 = P2 by FUNCT_2:63;
end;
end;
theorem Th11:
for L be non empty ZeroStr for p be Polynomial of L holds
Leading-Monomial(p) = 0_.(L)+*(len p-'1,p.(len p-'1))
proof
let L be non empty ZeroStr;
let p be Polynomial of L;
reconsider P=0_.(L)+*(len p-'1,p.(len p-'1)) as sequence of L;
A1: now
let n be Element of NAT;
assume n <> len p-'1;
hence P.n = (0_.(L)).n by FUNCT_7:32
.= 0.L by FUNCOP_1:7;
end;
len p-'1 in NAT;
then len p-'1 in dom 0_.(L) by NORMSP_1:12;
then P.(len p-'1) = p.(len p-'1) by FUNCT_7:31;
hence thesis by A1,Def1;
end;
registration
let L be non empty ZeroStr;
let p be Polynomial of L;
cluster Leading-Monomial(p) -> finite-Support;
coherence
proof
take len p;
let i be Nat;
A1: i in NAT by ORDINAL1:def 12;
assume i >= len p;
then i+1 > len p by NAT_1:13;
then
A2: i+1-1 > len p-1 by XREAL_1:9;
A3: Leading-Monomial(p) = 0_.(L)+*(len p-'1,p.(len p-'1)) by Th11;
per cases;
suppose
len p > 0;
then len p >= 0+1 by NAT_1:13;
then len p-1 >= 0+1-1 by XREAL_1:9;
then i <> len p-'1 by A2,XREAL_0:def 2;
hence (Leading-Monomial(p)).i = (0_.(L)).i by A3,FUNCT_7:32
.= 0.L by A1,FUNCOP_1:7;
end;
suppose
A4: len p = 0;
then
A5: len p-'1 = 0 by NAT_2:8;
0 in NAT;
then
A6: 0 in dom 0_.(L) by NORMSP_1:12;
now
per cases;
suppose
i > 0;
hence (Leading-Monomial(p)).i = (0_.(L)).i by A3,A5,FUNCT_7:32
.= 0.L by A1,FUNCOP_1:7;
end;
suppose
i = 0;
hence (Leading-Monomial(p)).i = p.0 by A3,A5,A6,FUNCT_7:31
.= (0_.(L)).0 by A4,Th5
.= 0.L by FUNCOP_1:7;
end;
end;
hence thesis;
end;
end;
end;
theorem Th12:
for L be non empty ZeroStr for p be Polynomial of L st len p = 0
holds Leading-Monomial(p) = 0_.(L)
proof
let L be non empty ZeroStr;
let p be Polynomial of L;
assume len p = 0;
then
A1: (0_.(L)).(len p-'1) = p.(len p-'1) by Th5;
for n be Element of NAT st n <> len p-'1 holds (0_.(L)).n = 0.L by FUNCOP_1:7
;
hence thesis by A1,Def1;
end;
theorem
for L be non empty ZeroStr holds Leading-Monomial(0_.(L)) = 0_.(L)
proof
let L be non empty ZeroStr;
len (0_.(L)) = 0 by Th3;
hence thesis by Th12;
end;
theorem
for L be non degenerated non empty multLoopStr_0 holds
Leading-Monomial(1_.(L)) = 1_.(L)
proof
let L be non degenerated non empty multLoopStr_0;
A1: now
let n be Element of NAT;
assume n <> len (1_.(L))-'1;
then n <> 1-'1 by Th4;
then n <> 0 by XREAL_1:232;
hence (1_.(L)).n = 0.L by POLYNOM3:30;
end;
(1_.(L)).(len (1_.(L))-'1) = (1_.(L)).(len (1_.(L))-'1);
hence thesis by A1,Def1;
end;
theorem Th15:
for L be non empty ZeroStr for p be Polynomial of L holds len
Leading-Monomial(p) = len p
proof
let L be non empty ZeroStr;
let p be Polynomial of L;
set r = Leading-Monomial(p);
A1: Leading-Monomial(p) = 0_.(L)+*(len p-'1,p.(len p-'1)) by Th11;
per cases;
suppose
len p > 0;
then
A2: len p >= 0+1 by NAT_1:13;
len p-'1 in NAT;
then
A3: len p-'1 in dom 0_.(L) by NORMSP_1:12;
A4: now
let m be Nat;
assume
A5: m is_at_least_length_of r;
assume len p > m;
then len p >= m+1 by NAT_1:13;
then len p-1 >= m+1-1 by XREAL_1:9;
then len p-'1 >= m by XREAL_0:def 2;
then r.(len p-'1) = 0.L by A5;
then
A6: p.(len p-'1) = 0.L by A1,A3,FUNCT_7:31;
len p = len p-'1+1 by A2,XREAL_1:235;
hence contradiction by A6,ALGSEQ_1:10;
end;
A7: len p-1 >= 0 by A2,XREAL_1:19;
len p is_at_least_length_of r
proof
let i be Nat;
A8: i in NAT by ORDINAL1:def 12;
assume i >= len p;
then i+1 > len p by NAT_1:13;
then i+1-1 > len p-1 by XREAL_1:9;
then i <> len p-'1 by A7,XREAL_0:def 2;
hence r.i = (0_.(L)).i by A1,FUNCT_7:32
.= 0.L by A8,FUNCOP_1:7;
end;
hence thesis by A4,ALGSEQ_1:def 3;
end;
suppose
A9: len p = 0;
hence len Leading-Monomial(p) = len (0_.(L)) by Th12
.= len p by A9,Th5;
end;
end;
theorem Th16:
for L be add-associative right_zeroed right_complementable non
empty addLoopStr for p be Polynomial of L st len p <> 0 ex q be Polynomial of
L st len q < len p & p = q+Leading-Monomial(p) & for n be Element of NAT st n <
len p-1 holds q.n = p.n
proof
let L be add-associative right_zeroed right_complementable non empty
addLoopStr;
let p be Polynomial of L;
deffunc F(Element of NAT) = p.$1;
consider q be Polynomial of L such that
A1: len q <= len p-'1 and
A2: for n be Element of NAT st n < len p-'1 holds q.n=F(n) from POLYNOM3
:sch 2;
assume len p <> 0;
then
A3: len p >= 0+1 by NAT_1:13;
take q;
len q < len p-'1+1 by A1,NAT_1:13;
hence
A4: len q < len p by A3,XREAL_1:235;
A5: now
let k be Nat;
A6: k in NAT by ORDINAL1:def 12;
assume k < len p;
then k+1 <= len p by NAT_1:13;
then
A7: k+1-1 <= len p-1 by XREAL_1:9;
per cases by A7,XXREAL_0:1;
suppose
k < len p-1;
then
A8: k < len p-'1 by XREAL_0:def 2;
thus (q+Leading-Monomial(p)).k = q.k + (Leading-Monomial(p)).k by
NORMSP_1:def 2
.= p.k + (Leading-Monomial(p)).k by A2,A6,A8
.= p.k + 0.L by A6,A8,Def1
.= p.k by RLVECT_1:def 4;
end;
suppose
k = len p-1;
then
A9: k = len p-'1 by XREAL_0:def 2;
thus (q+Leading-Monomial(p)).k = q.k + (Leading-Monomial(p)).k by
NORMSP_1:def 2
.= 0.L + (Leading-Monomial(p)).k by A1,A9,ALGSEQ_1:8
.= (Leading-Monomial(p)).k by RLVECT_1:4
.= p.k by A9,Def1;
end;
end;
A10: len Leading-Monomial(p) = len p by Th15;
then
len (q+Leading-Monomial(p)) = max(len q,len Leading-Monomial(p)) by A4,Th7
.= len p by A4,A10,XXREAL_0:def 10;
hence p = q+Leading-Monomial(p) by A5,ALGSEQ_1:12;
let n be Element of NAT;
assume n < len p-1;
then n < len p-'1 by XREAL_0:def 2;
hence thesis by A2;
end;
begin :: Evaluation of Polynomials
definition
let L be unital non empty doubleLoopStr;
let p be Polynomial of L;
let x be Element of L;
func eval(p,x) -> Element of L means
:Def2:
ex F be FinSequence of the
carrier of L st it = Sum F & len F = len p & for n be Element of NAT st n in
dom F holds F.n = p.(n-'1) * (power L).(x,n-'1);
existence
proof
deffunc G(Nat) = p.($1-'1)*(power L).(x,$1-'1);
consider F be FinSequence of the carrier of L such that
A1: len F = len p and
A2: for n be Nat st n in dom F holds F.n = G(n) from FINSEQ_2:sch 1;
take y = Sum F;
take F;
thus y = Sum F & len F = len p by A1;
let n be Element of NAT;
assume n in dom F;
hence thesis by A2;
end;
uniqueness
proof
let y1,y2 be Element of L;
given F1 be FinSequence of the carrier of L such that
A3: y1 = Sum F1 and
A4: len F1 = len p and
A5: for n be Element of NAT st n in dom F1 holds F1.n = p.(n-'1)*(
power L).(x,n-'1);
given F2 be FinSequence of the carrier of L such that
A6: y2 = Sum F2 and
A7: len F2 = len p and
A8: for n be Element of NAT st n in dom F2 holds F2.n = p.(n-'1)*(
power L).(x,n-'1);
A9: dom F1 = Seg len p by A4,FINSEQ_1:def 3;
now
let n be Nat;
assume
A10: n in dom F1;
then
A11: n in dom F2 by A7,A9,FINSEQ_1:def 3;
thus F1.n = p.(n-'1)*(power L).(x,n-'1) by A5,A10
.= F2.n by A8,A11;
end;
hence thesis by A3,A4,A6,A7,FINSEQ_2:9;
end;
end;
theorem Th17:
for L be unital non empty doubleLoopStr for x be Element of L
holds eval(0_.(L),x) = 0.L
proof
let L be unital non empty doubleLoopStr;
let x be Element of L;
consider F be FinSequence of the carrier of L such that
A1: eval(0_.(L),x) = Sum F and
A2: len F = len 0_.(L) and
for n be Element of NAT st n in dom F holds F.n = (0_.(L)).(n-'1) * (
power L).(x,n-'1) by Def2;
len F = 0 by A2,Th3;
then F = <*>the carrier of L;
hence thesis by A1,RLVECT_1:43;
end;
theorem Th18:
for L be well-unital add-associative right_zeroed
right_complementable associative non degenerated non empty doubleLoopStr for
x be Element of L holds eval(1_.(L),x) = 1.L
proof
let L be well-unital add-associative right_zeroed right_complementable
associative non degenerated non empty doubleLoopStr;
let x be Element of L;
consider F be FinSequence of the carrier of L such that
A1: eval(1_.(L),x) = Sum F and
A2: len F = len 1_.(L) and
A3: for n be Element of NAT st n in dom F holds F.n = (1_.(L)).(n-'1) *
(power L).(x,n-'1) by Def2;
A4: len F = 1 by A2,Th4;
then 1 in Seg len F by FINSEQ_1:1;
then 1 in dom F by FINSEQ_1:def 3;
then F.1 = (1_.(L)).(1-'1) * (power L).(x,1-'1) by A3
.= (1_.(L)).(0) * (power L).(x,1-'1) by XREAL_1:232
.= 1.L * (power L).(x,1-'1) by POLYNOM3:30
.= (power L).(x,1-'1)
.= (power L).(x,0) by XREAL_1:232
.= 1_L by GROUP_1:def 7
.= 1.L;
then F = <*1.L*> by A4,FINSEQ_1:40;
hence thesis by A1,RLVECT_1:44;
end;
theorem Th19:
for L be Abelian add-associative right_zeroed
right_complementable unital left-distributive non empty doubleLoopStr for p,q
be Polynomial of L for x be Element of L holds eval(p+q,x) = eval(p,x) + eval(q
,x)
proof
let L be Abelian add-associative right_zeroed right_complementable unital
left-distributive non empty doubleLoopStr;
let p,q be Polynomial of L;
let x be Element of L;
reconsider k = max(len p,len q) as Element of NAT by ORDINAL1:def 12;
A1: k - len p >= 0 by XREAL_1:48,XXREAL_0:25;
consider F1 be FinSequence of the carrier of L such that
A2: eval(p,x) = Sum F1 and
A3: len F1 = len p and
A4: for n be Element of NAT st n in dom F1 holds F1.n = p.(n-'1) * (
power L).(x,n-'1) by Def2;
A5: len (F1 ^ ((k-'(len F1)) |-> 0.L)) = len p + len ((k-'(len p)) |-> 0.L)
by A3,FINSEQ_1:22
.= len p + (k-'(len p)) by CARD_1:def 7
.= len p + (k-(len p)) by A1,XREAL_0:def 2
.= k;
A6: k - len q >= 0 by XREAL_1:48,XXREAL_0:25;
k >= len p & k >= len q by XXREAL_0:25;
then
A7: k - len (p+q) >= 0 by Th6,XREAL_1:48;
consider F3 be FinSequence of the carrier of L such that
A8: eval(p+q,x) = Sum F3 and
A9: len F3 = len (p+q) and
A10: for n be Element of NAT st n in dom F3 holds F3.n = (p+q).(n-'1) * (
power L).(x,n-'1) by Def2;
A11: len (F3 ^ ((k-'(len F3)) |-> 0.L)) = len (p+q) + len ((k-'(len (p+q)))
|-> 0.L) by A9,FINSEQ_1:22
.= len (p+q) + (k-'(len (p+q))) by CARD_1:def 7
.= len (p+q) + (k-(len (p+q))) by A7,XREAL_0:def 2
.= k;
consider F2 be FinSequence of the carrier of L such that
A12: eval(q,x) = Sum F2 and
A13: len F2 = len q and
A14: for n be Element of NAT st n in dom F2 holds F2.n = q.(n-'1) * (
power L).(x,n-'1) by Def2;
len (F2 ^ ((k-'(len F2)) |-> 0.L)) = len q + len ((k-'(len q)) |-> 0.L)
by A13,FINSEQ_1:22
.= len q + (k-'(len q)) by CARD_1:def 7
.= len q + (k-(len q)) by A6,XREAL_0:def 2
.= k;
then reconsider
G1 = F1 ^ ((k-'(len F1)) |-> 0.L), G2 = F2 ^ ((k-'(len F2)) |->
0.L), G3 = F3 ^ ((k-'(len F3)) |-> 0.L) as Element of k-tuples_on the carrier
of L by A5,A11,FINSEQ_2:92;
now
let n be Nat;
assume
A15: n in Seg k;
then
A16: 0+1 <= n by FINSEQ_1:1;
A17: n <= k by A15,FINSEQ_1:1;
per cases by XXREAL_0:1;
suppose
A18: len p > len q;
then
A19: k = len p by XXREAL_0:def 10;
then len(p+q) = len p by A18,Th7;
then
A20: n in dom F3 by A9,A15,A19,FINSEQ_1:def 3;
A21: len G2 = k by CARD_1:def 7;
then
A22: n in dom G2 by A15,FINSEQ_1:def 3;
then
A23: G2/.n = G2.n by PARTFUN1:def 6;
len G1 = k by CARD_1:def 7;
then
A24: n in dom G1 by A15,FINSEQ_1:def 3;
then
A25: G1/.n = G1.n by PARTFUN1:def 6;
A26: n in dom F1 by A3,A15,A19,FINSEQ_1:def 3;
A27: G1/.n = G1.n by A24,PARTFUN1:def 6
.= F1.n by A26,FINSEQ_1:def 7
.= F1/.n by A26,PARTFUN1:def 6;
A28: F1.n = p.(n-'1)*(power L).(x,n-'1) by A4,A26;
now
per cases;
suppose
n <= len q;
then n in Seg len q by A16,FINSEQ_1:1;
then
A29: n in dom F2 by A13,FINSEQ_1:def 3;
then
A30: F2.n = q.(n-'1)*(power L).(x,n-'1) by A14;
A31: G2/.n = G2.n by A22,PARTFUN1:def 6
.= F2.n by A29,FINSEQ_1:def 7
.= F2/.n by A29,PARTFUN1:def 6;
thus G3.n = F3.n by A20,FINSEQ_1:def 7
.= (p+q).(n-'1) * (power L).(x,n-'1) by A10,A20
.= (p.(n-'1) + q.(n-'1)) * (power L).(x,n-'1) by NORMSP_1:def 2
.= p.(n-'1)*(power L).(x,n-'1) + q.(n-'1)*(power L).(x,n-'1) by
VECTSP_1:def 3
.= p.(n-'1)*(power L).(x,n-'1) + F2/.n by A29,A30,PARTFUN1:def 6
.= F1/.n + F2/.n by A26,A28,PARTFUN1:def 6
.= (G1 + G2).n by A15,A25,A23,A27,A31,FVSUM_1:18;
end;
suppose
A32: n > len q;
then
A33: n >= len q+1 by NAT_1:13;
then n-1 >= len q by XREAL_1:19;
then
A34: n-'1 >= len q by XREAL_0:def 2;
n-len F2 <= k-len F2 by A17,XREAL_1:9;
then
A35: n-len F2 <= k-'len F2 by XREAL_0:def 2;
A36: n-len F2 >= 1 by A13,A33,XREAL_1:19;
then n-len F2 = n-'len F2 by XREAL_0:def 2;
then
A37: n-len F2 in Seg (k-'len F2) by A36,A35,FINSEQ_1:1;
n <= len G2 by A15,A21,FINSEQ_1:1;
then
A38: G2/.n = ((k-'(len F2))|->0.L).(n-len F2) by A13,A23,A32,FINSEQ_1:24
.= 0.L by A37,FUNCOP_1:7;
thus G3.n = F3.n by A20,FINSEQ_1:def 7
.= (p+q).(n-'1) * (power L).(x,n-'1) by A10,A20
.= (p.(n-'1) + q.(n-'1)) * (power L).(x,n-'1) by NORMSP_1:def 2
.= (p.(n-'1) + 0.L) * (power L).(x,n-'1) by A34,ALGSEQ_1:8
.= (p.(n-'1)) * (power L).(x,n-'1) by RLVECT_1:4
.= F1.n by A4,A26
.= G1/.n by A26,A27,PARTFUN1:def 6
.= G1/.n + 0.L by RLVECT_1:4
.= (G1 + G2).n by A15,A25,A23,A38,FVSUM_1:18;
end;
end;
hence G3.n = (G1 + G2).n;
end;
suppose
A39: len p < len q;
then
A40: k = len q by XXREAL_0:def 10;
then len(p+q) = len q by A39,Th7;
then
A41: n in dom F3 by A9,A15,A40,FINSEQ_1:def 3;
A42: len G1 = k by CARD_1:def 7;
then
A43: n in dom G1 by A15,FINSEQ_1:def 3;
then
A44: G1/.n = G1.n by PARTFUN1:def 6;
len G2 = k by CARD_1:def 7;
then
A45: n in dom G2 by A15,FINSEQ_1:def 3;
then
A46: G2/.n = G2.n by PARTFUN1:def 6;
A47: n in dom F2 by A13,A15,A40,FINSEQ_1:def 3;
A48: G2/.n = G2.n by A45,PARTFUN1:def 6
.= F2.n by A47,FINSEQ_1:def 7
.= F2/.n by A47,PARTFUN1:def 6;
A49: F2.n = q.(n-'1)*(power L).(x,n-'1) by A14,A47;
now
per cases;
suppose
n <= len p;
then n in Seg len p by A16,FINSEQ_1:1;
then
A50: n in dom F1 by A3,FINSEQ_1:def 3;
then
A51: F1.n = p.(n-'1)*(power L).(x,n-'1) by A4;
A52: G1/.n = G1.n by A43,PARTFUN1:def 6
.= F1.n by A50,FINSEQ_1:def 7
.= F1/.n by A50,PARTFUN1:def 6;
thus G3.n = F3.n by A41,FINSEQ_1:def 7
.= (p+q).(n-'1) * (power L).(x,n-'1) by A10,A41
.= (p.(n-'1) + q.(n-'1)) * (power L).(x,n-'1) by NORMSP_1:def 2
.= p.(n-'1)*(power L).(x,n-'1) + q.(n-'1)*(power L).(x,n-'1) by
VECTSP_1:def 3
.= F1/.n + q.(n-'1)*(power L).(x,n-'1) by A50,A51,PARTFUN1:def 6
.= F1/.n + F2/.n by A47,A49,PARTFUN1:def 6
.= (G1 + G2).n by A15,A44,A46,A48,A52,FVSUM_1:18;
end;
suppose
A53: n > len p;
then
A54: n >= len p+1 by NAT_1:13;
then n-1 >= len p by XREAL_1:19;
then
A55: n-'1 >= len p by XREAL_0:def 2;
n-len F1 <= k-len F1 by A17,XREAL_1:9;
then
A56: n-len F1 <= k-'len F1 by XREAL_0:def 2;
A57: n-len F1 >= 1 by A3,A54,XREAL_1:19;
then n-len F1 = n-'len F1 by XREAL_0:def 2;
then
A58: n-len F1 in Seg (k-'len F1) by A57,A56,FINSEQ_1:1;
n <= len G1 by A15,A42,FINSEQ_1:1;
then
A59: G1/.n = ((k-'(len F1))|->0.L).(n-len F1) by A3,A44,A53,FINSEQ_1:24
.= 0.L by A58,FUNCOP_1:7;
thus G3.n = F3.n by A41,FINSEQ_1:def 7
.= (p+q).(n-'1) * (power L).(x,n-'1) by A10,A41
.= (p.(n-'1) + q.(n-'1)) * (power L).(x,n-'1) by NORMSP_1:def 2
.= (0.L + q.(n-'1)) * (power L).(x,n-'1) by A55,ALGSEQ_1:8
.= (q.(n-'1)) * (power L).(x,n-'1) by RLVECT_1:4
.= F2.n by A14,A47
.= G2/.n by A47,A48,PARTFUN1:def 6
.= 0.L + G2/.n by RLVECT_1:4
.= (G1 + G2).n by A15,A44,A46,A59,FVSUM_1:18;
end;
end;
hence G3.n = (G1 + G2).n;
end;
suppose
A60: len p = len q;
len G2 = k by CARD_1:def 7;
then
A61: n in dom G2 by A15,FINSEQ_1:def 3;
then
A62: G2/.n = G2.n by PARTFUN1:def 6;
len G1 = k by CARD_1:def 7;
then
A63: n in dom G1 by A15,FINSEQ_1:def 3;
then
A64: G1/.n = G1.n by PARTFUN1:def 6;
A65: len G3 = k by CARD_1:def 7;
A66: n in dom F2 by A13,A15,A60,FINSEQ_1:def 3;
A67: n in dom F1 by A3,A15,A60,FINSEQ_1:def 3;
then
A68: F1.n = p.(n-'1)*(power L).(x,n-'1) by A4;
A69: G1/.n = G1.n by A63,PARTFUN1:def 6
.= F1.n by A67,FINSEQ_1:def 7
.= F1/.n by A67,PARTFUN1:def 6;
now
per cases;
suppose
A70: n <= len (p+q);
A71: n in dom F2 by A13,A15,A60,FINSEQ_1:def 3;
then
A72: F2.n = q.(n-'1)*(power L).(x,n-'1) by A14;
A73: G2/.n = G2.n by A61,PARTFUN1:def 6
.= F2.n by A71,FINSEQ_1:def 7
.= F2/.n by A71,PARTFUN1:def 6;
n in Seg len (p+q) by A16,A70,FINSEQ_1:1;
then
A74: n in dom F3 by A9,FINSEQ_1:def 3;
hence G3.n = F3.n by FINSEQ_1:def 7
.= (p+q).(n-'1) * (power L).(x,n-'1) by A10,A74
.= (p.(n-'1) + q.(n-'1)) * (power L).(x,n-'1) by NORMSP_1:def 2
.= p.(n-'1)*(power L).(x,n-'1) + q.(n-'1)*(power L).(x,n-'1) by
VECTSP_1:def 3
.= p.(n-'1)*(power L).(x,n-'1) + F2/.n by A71,A72,PARTFUN1:def 6
.= F1/.n + F2/.n by A67,A68,PARTFUN1:def 6
.= (G1 + G2).n by A15,A64,A62,A69,A73,FVSUM_1:18;
end;
suppose
A75: n > len (p+q);
then
A76: n >= len (p+q)+1 by NAT_1:13;
then n-1 >= len (p+q)+1-1 by XREAL_1:9;
then
A77: n-'1 >= len (p+q) by XREAL_0:def 2;
n-len F3 <= k-len F3 by A17,XREAL_1:9;
then
A78: n-len F3 <= k-'len F3 by XREAL_0:def 2;
A79: G2.n = F2.n by A66,FINSEQ_1:def 7
.= (q.(n-'1))*(power L).(x,n-'1) by A14,A66;
A80: G1.n = F1.n by A67,FINSEQ_1:def 7
.= (p.(n-'1))*(power L).(x,n-'1) by A4,A67;
A81: n-len F3 >= 1 by A9,A76,XREAL_1:19;
then n-len F3 = n-'len F3 by XREAL_0:def 2;
then
A82: n-len F3 in Seg (k-'len F3) by A81,A78,FINSEQ_1:1;
n <= len G3 by A15,A65,FINSEQ_1:1;
hence G3.n = ((k-'(len F3))|->0.L).(n-len F3) by A9,A75,FINSEQ_1:24
.= 0.L by A82,FUNCOP_1:7
.= 0.L * (power L).(x,n-'1)
.= (p+q).(n-'1) * (power L).(x,n-'1) by A77,ALGSEQ_1:8
.= (p.(n-'1) + q.(n-'1)) * (power L).(x,n-'1) by NORMSP_1:def 2
.= (p.(n-'1))*(power L).(x,n-'1) + (q.(n-'1))*(power L).(x,n-'1)
by VECTSP_1:def 3
.= (G1 + G2).n by A15,A80,A79,FVSUM_1:18;
end;
end;
hence G3.n = (G1 + G2).n;
end;
end;
then
A83: G3 = G1 + G2 by FINSEQ_2:119;
A84: Sum G3 = Sum F3 + Sum ((k-'(len F3)) |-> 0.L) by RLVECT_1:41
.= Sum F3 + 0.L by MATRIX_3:11
.= Sum F3 by RLVECT_1:def 4;
A85: Sum G2 = Sum F2 + Sum ((k-'(len F2)) |-> 0.L) by RLVECT_1:41
.= Sum F2 + 0.L by MATRIX_3:11
.= Sum F2 by RLVECT_1:def 4;
Sum G1 = Sum F1 + Sum ((k-'(len F1)) |-> 0.L) by RLVECT_1:41
.= Sum F1 + 0.L by MATRIX_3:11
.= Sum F1 by RLVECT_1:def 4;
hence thesis by A2,A12,A8,A85,A84,A83,FVSUM_1:76;
end;
theorem Th20:
for L be Abelian add-associative right_zeroed
right_complementable unital distributive non empty doubleLoopStr for p be
Polynomial of L for x be Element of L holds eval(-p,x) = -eval(p,x)
proof
let L be Abelian add-associative right_zeroed right_complementable unital
distributive non empty doubleLoopStr;
let p be Polynomial of L;
let x be Element of L;
consider F1 be FinSequence of the carrier of L such that
A1: eval(p,x) = Sum F1 and
A2: len F1 = len p and
A3: for n be Element of NAT st n in dom F1 holds F1.n = p.(n-'1) * (
power L).(x,n-'1) by Def2;
consider F2 be FinSequence of the carrier of L such that
A4: eval(-p,x) = Sum F2 and
A5: len F2 = len (-p) and
A6: for n be Element of NAT st n in dom F2 holds F2.n=(-p).(n-'1)*(power
L).(x,n-'1) by Def2;
len F2 = len F1 by A2,A5,Th8;
then
A7: dom F2 = dom F1 by FINSEQ_3:29;
now
let n be Nat;
let v be Element of L;
assume that
A8: n in dom F2 and
A9: v = F1.n;
thus F2.n = (-p).(n-'1)*(power L).(x,n-'1) by A6,A8
.= (-p.(n-'1))*(power L).(x,n-'1) by BHSP_1:44
.= -p.(n-'1)*(power L).(x,n-'1) by VECTSP_1:9
.= -v by A3,A7,A8,A9;
end;
hence thesis by A1,A2,A4,A5,Th8,RLVECT_1:40;
end;
theorem
for L be Abelian add-associative right_zeroed right_complementable
unital distributive non empty doubleLoopStr for p,q be Polynomial of L for x
be Element of L holds eval(p-q,x) = eval(p,x) - eval(q,x)
proof
let L be Abelian add-associative right_zeroed right_complementable unital
distributive non empty doubleLoopStr;
let p,q be Polynomial of L;
let x be Element of L;
thus eval(p-q,x) = eval(p,x) + eval(-q,x) by Th19
.= eval(p,x) +- eval(q,x) by Th20
.= eval(p,x) - eval(q,x) by RLVECT_1:def 11;
end;
theorem Th22:
for L be add-associative right_zeroed right_complementable
right_zeroed distributive unital non empty doubleLoopStr for p be Polynomial
of L for x be Element of L holds eval(Leading-Monomial(p),x) = p.(len p-'1) * (
power L).(x,len p-'1)
proof
let L be add-associative right_zeroed right_complementable right_zeroed
distributive unital non empty doubleLoopStr;
let p be Polynomial of L;
let x be Element of L;
set LMp=Leading-Monomial(p);
consider F be FinSequence of the carrier of L such that
A1: eval(LMp,x) = Sum F and
A2: len F = len LMp and
A3: for n be Element of NAT st n in dom F holds F.n = LMp.(n-'1)*(power
L).(x,n-'1) by Def2;
A4: len F = len p by A2,Th15;
per cases;
suppose
len p > 0;
then
A5: len p >= 0+1 by NAT_1:13;
then len p in Seg len F by A4,FINSEQ_1:1;
then
A6: len p in dom F by FINSEQ_1:def 3;
A7: len p-1 >=0 by A5,XREAL_1:19;
now
A8: len p-'1 = len p-1 by A7,XREAL_0:def 2;
let i be Element of NAT;
assume that
A9: i in dom F and
A10: i <> len p;
i in Seg len F by A9,FINSEQ_1:def 3;
then i >= 0+1 by FINSEQ_1:1;
then i-1 >= 0 by XREAL_1:19;
then i-'1 = i-1 by XREAL_0:def 2;
then
A11: i-'1 <> len p-'1 by A10,A8;
thus F/.i = F.i by A9,PARTFUN1:def 6
.= LMp.(i-'1)*(power L).(x,i-'1) by A3,A9
.= 0.L*(power L).(x,i-'1) by A11,Def1
.= 0.L;
end;
then Sum F = F/.(len p) by A6,POLYNOM2:3
.= F.(len p) by A6,PARTFUN1:def 6
.= LMp.(len p-'1)*(power L).(x,len p-'1) by A3,A6;
hence thesis by A1,Def1;
end;
suppose
A12: len p = 0;
then
A13: p = 0_.(L) by Th5;
LMp = 0_.(L) by A12,Th12;
hence eval(Leading-Monomial(p),x) = 0.L by Th17
.= 0.L*(power L).(x,len p-'1)
.= p.(len p-'1)*(power L).(x,len p-'1) by A13,FUNCOP_1:7;
end;
end;
Lm2: for L be add-associative right_zeroed right_complementable unital
distributive associative non empty doubleLoopStr for p,q be Polynomial of L
st len p > 0 & len q > 0 for x be Element of L holds eval((Leading-Monomial(p))
*'(Leading-Monomial(q)),x) = p.(len p-'1)*q.(len q-'1)*(power L).(x,len p+len q
-'2)
proof
let L be add-associative right_zeroed right_complementable unital
distributive associative non empty doubleLoopStr;
let p,q be Polynomial of L;
assume that
A1: len p > 0 and
A2: len q > 0;
A3: len q >= 0+1 by A2,NAT_1:13;
then
A4: len q-1 >= 0 by XREAL_1:19;
A5: len p >= 0+1 by A1,NAT_1:13;
then len p-1 >= 0 by XREAL_1:19;
then
A6: len p-1 = len p-'1 by XREAL_0:def 2;
A7: len p + len q >= 0+(1+1) by A5,A3,XREAL_1:7;
then
A8: len p + len q - 1 >= 1 by XREAL_1:19;
then reconsider i1=len p + len q - 1 as Element of NAT by INT_1:3;
A9: i1-'1+1 = i1 by A8,XREAL_1:235;
set LMp=Leading-Monomial(p), LMq=Leading-Monomial(q);
let x be Element of L;
consider F be FinSequence of the carrier of L such that
A10: eval(LMp*'LMq,x) = Sum F and
A11: len F = len (LMp*'LMq) and
A12: for n be Element of NAT st n in dom F holds F.n = (LMp*'LMq).(n-'1)
* (power L).(x,n-'1) by Def2;
consider r be FinSequence of the carrier of L such that
A13: len r = i1-'1+1 and
A14: (LMp*'LMq).(i1-'1) = Sum r and
A15: for k be Element of NAT st k in dom r holds r.k = LMp.(k-'1)*LMq.(
i1-'1+1-'k) by POLYNOM3:def 9;
len p+0 <= len p+(len q-1) by A4,XREAL_1:7;
then len p in Seg len r by A5,A9,A13,FINSEQ_1:1;
then
A16: len p in dom r by FINSEQ_1:def 3;
len p+(len q-1)-len p >= 0 by A3,XREAL_1:19;
then i1-'len p = len p+(len q-1)-len p by XREAL_0:def 2
.= len q-'1 by A4,XREAL_0:def 2;
then
A17: r.(len p) = LMp.(len p-'1) * LMq.(len q-'1) by A9,A15,A16;
now
let i be Element of NAT;
assume that
A18: i in dom r and
A19: i <> len p;
i in Seg len r by A18,FINSEQ_1:def 3;
then i >= 0+1 by FINSEQ_1:1;
then i-1 >= 0 by XREAL_1:19;
then i-'1 = i-1 by XREAL_0:def 2;
then
A20: i-'1 <> len p-'1 by A6,A19;
thus r/.i = r.i by A18,PARTFUN1:def 6
.= LMp.(i-'1) * LMq.(i1-'1+1-'i) by A15,A18
.= 0.L*LMq.(i1-'1+1-'i) by A20,Def1
.= 0.L;
end;
then
A21: Sum r = r/.(len p) by A16,POLYNOM2:3
.= LMp.(len p-'1) * LMq.(len q-'1) by A16,A17,PARTFUN1:def 6
.= p.(len p-'1) * LMq.(len q-'1) by Def1
.= p.(len p-'1) * q.(len q-'1) by Def1;
A22: len q-1 = len q-'1 by A4,XREAL_0:def 2;
A23: now
let i be Element of NAT;
assume that
A24: i in dom F and
A25: i <> i1;
consider r1 be FinSequence of the carrier of L such that
A26: len r1 = i-'1+1 and
A27: (LMp*'LMq).(i-'1) = Sum r1 and
A28: for k be Element of NAT st k in dom r1 holds r1.k=LMp.(k-'1)*LMq.
(i-'1+1-'k) by POLYNOM3:def 9;
i in Seg len F by A24,FINSEQ_1:def 3;
then i >= 1 by FINSEQ_1:1;
then
A29: i-'1+1 = i by XREAL_1:235;
A30: now
let j be Element of NAT;
assume
A31: j in dom r1;
then j in Seg len r1 by FINSEQ_1:def 3;
then j >= 0+1 by FINSEQ_1:1;
then j-1 >= 0 by XREAL_1:19;
then
A32: j-'1 = j-1 by XREAL_0:def 2;
per cases;
suppose
j<>len p;
then
A33: j-'1 <> len p-'1 by A6,A32;
thus r1.j = LMp.(j-'1)*LMq.(i-'1+1-'j) by A28,A31
.= 0.L*LMq.(i-'1+1-'j) by A33,Def1
.= 0.L;
end;
suppose
A34: j=len p;
j in Seg len r1 by A31,FINSEQ_1:def 3;
then i >= 0+j by A26,A29,FINSEQ_1:1;
then i-j >= 0 by XREAL_1:19;
then i-'len p = i-len p by A34,XREAL_0:def 2;
then
A35: i-'len p <> len q-'1 by A22,A25;
thus r1.j = LMp.(j-'1)*LMq.(i-'len p) by A28,A29,A31,A34
.= LMp.(j-'1)*0.L by A35,Def1
.= 0.L;
end;
end;
thus F/.i = F.i by A24,PARTFUN1:def 6
.= (Sum r1)*(power L).(x,i-'1) by A12,A24,A27
.= 0.L*(power L).(x,i-'1) by A30,POLYNOM3:1
.= 0.L;
end;
A36: len p+len q-2 >= 0 by A7,XREAL_1:19;
len p+len q-(1+1) >= 0 by A7,XREAL_1:19;
then
A37: i1-'1 = len p+len q-1-1 by XREAL_0:def 2
.= len p+len q-'2 by A36,XREAL_0:def 2;
per cases;
suppose
(LMp*'LMq).(i1-'1) <> 0.L;
then len F > i1-'1 by A11,ALGSEQ_1:8;
then len F >= i1 by A9,NAT_1:13;
then i1 in Seg len F by A8,FINSEQ_1:1;
then
A38: i1 in dom F by FINSEQ_1:def 3;
hence eval((Leading-Monomial(p))*'(Leading-Monomial(q)),x) = F/.i1 by A10
,A23,POLYNOM2:3
.= F.i1 by A38,PARTFUN1:def 6
.= p.(len p-'1)*q.(len q-'1)*(power L).(x,len p+len q-'2) by A12,A14,A37
,A21,A38;
end;
suppose
A39: (LMp*'LMq).(i1-'1) = 0.L;
now
let j be Nat;
assume j >= 0;
j in NAT by ORDINAL1:def 12;
then consider r1 be FinSequence of the carrier of L such that
A40: len r1 = j+1 and
A41: (LMp*'LMq).j = Sum r1 and
A42: for k be Element of NAT st k in dom r1 holds r1.k = LMp.(k-'1)*
LMq.(j+1-'k) by POLYNOM3:def 9;
now
per cases;
suppose
j = i1-'1;
hence (LMp*'LMq).j = 0.L by A39;
end;
suppose
A43: j <> i1-'1;
now
let k be Element of NAT;
assume
A44: k in dom r1;
per cases;
suppose
A45: k-'1 <> len p-'1;
thus r1.k = LMp.(k-'1)*LMq.(j+1-'k) by A42,A44
.= 0.L*LMq.(j+1-'k) by A45,Def1
.= 0.L;
end;
suppose
A46: k-'1 = len p-'1;
A47: k in Seg len r1 by A44,FINSEQ_1:def 3;
then 0+1 <= k by FINSEQ_1:1;
then k-1 >= 0 by XREAL_1:19;
then
A48: k-'1 = k-1 by XREAL_0:def 2;
0+k <= j+1 by A40,A47,FINSEQ_1:1;
then j+1-k >= 0 by XREAL_1:19;
then
A49: j+1-'k = j-len p+1 by A6,A46,A48,XREAL_0:def 2;
A50: j-len p+1 <> i1-'1-len p+1 by A43;
thus r1.k = LMp.(k-'1)*LMq.(j+1-'k) by A42,A44
.= LMp.(k-'1)*0.L by A22,A9,A49,A50,Def1
.= 0.L;
end;
end;
hence (LMp*'LMq).j = 0.L by A41,POLYNOM3:1;
end;
end;
hence (LMp*'LMq).j = 0.L;
end;
then 0 is_at_least_length_of (LMp*'LMq);
then len (LMp*'LMq) = 0 by ALGSEQ_1:def 3;
then LMp*'LMq = 0_.(L) by Th5;
then eval(LMp*'LMq,x) = 0.L by Th17;
hence thesis by A14,A21,A39;
end;
end;
Lm3: for L be add-associative right_zeroed right_complementable left_unital
distributive commutative associative non trivial doubleLoopStr for
p,q be Polynomial of L for x be Element of L holds eval((Leading-Monomial(p))*'
(Leading-Monomial(q)),x) = eval(Leading-Monomial(p),x)*eval(Leading-Monomial(q)
,x)
proof
let L be add-associative right_zeroed right_complementable left_unital
distributive commutative associative non trivial doubleLoopStr;
let p,q be Polynomial of L;
let x be Element of L;
set p1 = len p-'1;
set q1 = len q-'1;
per cases;
suppose
A1: len p <> 0 & len q <> 0;
then
A2: len q >= 0+1 by NAT_1:13;
then len q-1 >= 0 by XREAL_1:19;
then
A3: len q-1 = len q-'1 by XREAL_0:def 2;
A4: len p >= 0+1 by A1,NAT_1:13;
then len p-1 >= 0 by XREAL_1:19;
then
A5: len p-1 = len p-'1 by XREAL_0:def 2;
len p+len q >= 0+(1+1) by A4,A2,XREAL_1:7;
then len p+len q-2 >= 0 by XREAL_1:19;
then
A6: len p+len q-'2 = len p+len q-2 by XREAL_0:def 2;
A7: len p+len q-(1+1) = len p-1+(len q-1);
set P1 = (power L).(x,p1);
set Q1 = (power L).(x,q1);
thus eval((Leading-Monomial(p))*'(Leading-Monomial(q)),x)
= p.p1*q.q1*(power L).(x,len p+len q-'2) by A1,Lm2
.= p.p1*q.q1*(P1*Q1) by A5,A3,A6,A7,POLYNOM2:1
.= p.p1*(q.q1*(P1*Q1)) by GROUP_1:def 3
.= p.p1*(P1*(q.q1*Q1)) by GROUP_1:def 3
.= p.p1*P1*(q.q1*Q1) by GROUP_1:def 3
.= p.p1*P1*eval(Leading-Monomial(q),x) by Th22
.= eval(Leading-Monomial(p),x)*eval(Leading-Monomial(q),x) by Th22;
end;
suppose
len p = 0;
then
A8: Leading-Monomial(p) = 0_.(L) by Th12;
hence
eval((Leading-Monomial(p))*'(Leading-Monomial(q)),x) = eval(0_.(L),x)
by Th2
.= 0.L by Th17
.= 0.L*eval(Leading-Monomial(q),x)
.= eval(Leading-Monomial(p),x)*eval(Leading-Monomial(q),x) by A8,Th17;
end;
suppose
len q = 0;
then len Leading-Monomial(q) = 0 by Th15;
then
A9: Leading-Monomial(q) = 0_.(L) by Th5;
hence
eval((Leading-Monomial(p))*'(Leading-Monomial(q)),x) = eval(0_.(L),x)
by POLYNOM3:34
.= 0.L by Th17
.= eval(Leading-Monomial(p),x)*0.L
.= eval(Leading-Monomial(p),x)*eval(Leading-Monomial(q),x) by A9,Th17;
end;
end;
theorem Th23:
for L be add-associative right_zeroed right_complementable
Abelian left_unital distributive commutative associative non trivial
doubleLoopStr for p,q be Polynomial of L for x be Element of L holds eval((
Leading-Monomial(p))*'q,x) = eval(Leading-Monomial(p),x) * eval(q,x)
proof
let L be add-associative right_zeroed right_complementable Abelian
left_unital distributive commutative associative non trivial
doubleLoopStr;
let p1,q be Polynomial of L;
let x be Element of L;
set p=Leading-Monomial(p1);
defpred P[Nat] means for q be Polynomial of L holds len q = $1 implies eval(
p*'q,x) = eval(p,x)*eval(q,x);
A1: for k be Nat st for n be Nat st n < k holds P[n] holds P[k]
proof
let k be Nat;
assume
A2: for n be Nat st n < k holds for q be Polynomial of L holds len q =
n implies eval(p*'q,x) = eval(p,x) * eval(q,x);
let q be Polynomial of L;
assume
A3: len q = k;
per cases;
suppose
A4: len q <> 0;
set LMq = Leading-Monomial(q);
consider r be Polynomial of L such that
A5: len r < len q and
A6: q = r+Leading-Monomial(q) and
for n be Element of NAT st n < len q-1 holds r.n = q.n by A4,Th16;
thus eval(p*'q,x) = eval(p*'r+p*'LMq,x) by A6,POLYNOM3:31
.= eval(p*'r,x) + eval(p*'LMq,x) by Th19
.= eval(p,x)*eval(r,x) + eval(p*'LMq,x) by A2,A3,A5
.= eval(p,x)*eval(r,x) + eval(p,x)*eval(LMq,x) by Lm3
.= eval(p,x)*(eval(r,x) + eval(LMq,x)) by VECTSP_1:def 7
.= eval(p,x) * eval(q,x) by A6,Th19;
end;
suppose
len q = 0;
then
A7: q = 0_.(L) by Th5;
hence eval(p*'q,x) = eval(0_.(L),x) by POLYNOM3:34
.= 0.L by Th17
.= eval(p,x) * 0.L
.= eval(p,x) * eval(q,x) by A7,Th17;
end;
end;
A8: for n be Nat holds P[n] from NAT_1:sch 4(A1);
len q = len q;
hence thesis by A8;
end;
theorem Th24:
for L be add-associative right_zeroed right_complementable
Abelian left_unital distributive commutative associative non trivial
doubleLoopStr for p,q be Polynomial of L for x be Element of L holds eval(p*'q
,x) = eval(p,x) * eval(q,x)
proof
let L be add-associative right_zeroed right_complementable Abelian
left_unital distributive commutative associative non trivial
doubleLoopStr;
let p,q be Polynomial of L;
let x be Element of L;
defpred P[Nat] means for p be Polynomial of L holds len p = $1 implies eval(
p*'q,x) = eval(p,x)*eval(q,x);
A1: for k be Nat st for n be Nat st n < k holds P[n] holds P[k]
proof
let k be Nat;
assume
A2: for n be Nat st n < k holds for p be Polynomial of L holds len p =
n implies eval(p*'q,x) = eval(p,x) * eval(q,x);
let p be Polynomial of L;
assume
A3: len p = k;
per cases;
suppose
A4: len p <> 0;
set LMp = Leading-Monomial(p);
consider r be Polynomial of L such that
A5: len r < len p and
A6: p = r+Leading-Monomial(p) and
for n be Element of NAT st n < len p-1 holds r.n = p.n by A4,Th16;
thus eval(p*'q,x) = eval(r*'q+LMp*'q,x) by A6,POLYNOM3:32
.= eval(r*'q,x) + eval(LMp*'q,x) by Th19
.= eval(r,x)*eval(q,x) + eval(LMp*'q,x) by A2,A3,A5
.= eval(r,x)*eval(q,x) + eval(LMp,x)*eval(q,x) by Th23
.= (eval(r,x) + eval(LMp,x))*eval(q,x) by VECTSP_1:def 7
.= eval(p,x) * eval(q,x) by A6,Th19;
end;
suppose
len p = 0;
then
A7: p = 0_.(L) by Th5;
hence eval(p*'q,x) = eval(0_.(L),x) by Th2
.= 0.L by Th17
.= 0.L * eval(q,x)
.= eval(p,x) * eval(q,x) by A7,Th17;
end;
end;
A8: for n be Nat holds P[n] from NAT_1:sch 4(A1);
len p = len p;
hence thesis by A8;
end;
begin :: Evaluation Homomorphism
definition
let L be add-associative right_zeroed right_complementable distributive
unital non empty doubleLoopStr;
let x be Element of L;
func Polynom-Evaluation(L,x) -> Function of Polynom-Ring L,L means
:Def3:
for p be Polynomial of L holds it.p = eval(p,x);
existence
proof
defpred P[set,set] means ex p be Polynomial of L st p = $1 & $2 = eval(p,x
);
A1: for y be Element of Polynom-Ring L ex z be Element of L st P[y,z]
proof
let y be Element of Polynom-Ring L;
reconsider p=y as Polynomial of L by POLYNOM3:def 10;
take eval(p,x);
take p;
thus thesis;
end;
consider f be Function of the carrier of Polynom-Ring L,the carrier of L
such that
A2: for y be Element of Polynom-Ring L holds P[y,f.y] from FUNCT_2:sch
3 ( A1);
reconsider f as Function of Polynom-Ring L,L;
take f;
let p be Polynomial of L;
p in the carrier of Polynom-Ring L by POLYNOM3:def 10;
then ex q be Polynomial of L st q = p & f.p = eval(q,x) by A2;
hence thesis;
end;
uniqueness
proof
let f1,f2 be Function of Polynom-Ring L,L such that
A3: for p be Polynomial of L holds f1.p = eval(p,x) and
A4: for p be Polynomial of L holds f2.p = eval(p,x);
now
let y be Element of Polynom-Ring L;
reconsider p=y as Polynomial of L by POLYNOM3:def 10;
thus f1.y = eval(p,x) by A3
.= f2.y by A4;
end;
hence f1 = f2 by FUNCT_2:63;
end;
end;
registration
let L be add-associative right_zeroed right_complementable distributive
associative well-unital non degenerated Abelian non empty doubleLoopStr;
let x be Element of L;
cluster Polynom-Evaluation(L,x) -> unity-preserving;
coherence
proof
thus (Polynom-Evaluation(L,x)).(1_Polynom-Ring L) = (Polynom-Evaluation(L,
x)).(1_.(L)) by POLYNOM3:37
.= eval(1_.(L),x) by Def3
.= 1_L by Th18;
end;
end;
registration
let L be Abelian add-associative right_zeroed right_complementable
distributive unital non empty doubleLoopStr;
let x be Element of L;
cluster Polynom-Evaluation(L,x) -> additive;
coherence
proof
let a,b be Element of Polynom-Ring L;
reconsider p=a,q=b as Polynomial of L by POLYNOM3:def 10;
thus (Polynom-Evaluation(L,x)).(a+b) = (Polynom-Evaluation(L,x)).(p+q) by
POLYNOM3:def 10
.= eval(p+q,x) by Def3
.= eval(p,x) + eval(q,x) by Th19
.= (Polynom-Evaluation(L,x)).a + eval(q,x) by Def3
.= (Polynom-Evaluation(L,x)).a+(Polynom-Evaluation(L,x)).b by Def3;
end;
end;
registration
let L be add-associative right_zeroed right_complementable Abelian
left_unital distributive commutative associative non trivial
doubleLoopStr;
let x be Element of L;
cluster Polynom-Evaluation(L,x) -> multiplicative;
coherence
proof
let a,b be Element of Polynom-Ring L;
reconsider p=a,q=b as Polynomial of L by POLYNOM3:def 10;
thus (Polynom-Evaluation(L,x)).(a*b) = (Polynom-Evaluation(L,x)).(p*'q) by
POLYNOM3:def 10
.= eval(p*'q,x) by Def3
.= eval(p,x)*eval(q,x) by Th24
.= (Polynom-Evaluation(L,x)).a*eval(q,x) by Def3
.= (Polynom-Evaluation(L,x)).a*(Polynom-Evaluation(L,x)).b by Def3;
end;
end;
registration
let L be add-associative right_zeroed right_complementable Abelian
well-unital distributive commutative associative non degenerated
doubleLoopStr;
let x be Element of L;
cluster Polynom-Evaluation(L,x) -> RingHomomorphism;
coherence;
end;