:: Little {B}ezout Theorem (Factor Theorem)
:: by Piotr Rudnicki
::
:: Received December 30, 2003
:: Copyright (c) 2003-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, FINSEQ_1, SUBSET_1, RELAT_1, FUNCT_1, CARD_1, CARD_3,
FINSEQ_2, ARYTM_3, ORDINAL4, TARSKI, NAT_1, XXREAL_0, REAL_1, ARYTM_1,
XBOOLE_0, RLVECT_1, ALGSTR_0, SUPINF_2, PARTFUN1, FINSET_1, FUNCT_2,
ZFMISC_1, PRE_POLY, FUNCT_4, FUNCOP_1, VALUED_0, PBOOLE, SGRAPH1,
FINSOP_1, BINOP_1, GROUP_1, STRUCT_0, POLYNOM1, POLYNOM3, AFINSQ_1,
MESFUNC1, ALGSEQ_1, VECTSP_1, POLYNOM5, LATTICES, VECTSP_2, COMPLFLD,
POLYNOM2, FVSUM_1, MEMBERED, CLASSES1, UPROOTS, FUNCT_7;
notations TARSKI, XBOOLE_0, XTUPLE_0, XCMPLX_0, XXREAL_0, SUBSET_1, ORDINAL1,
CARD_1, NUMBERS, XREAL_0, ZFMISC_1, REAL_1, VECTSP_2, BINOP_1, RELAT_1,
FUNCT_1, PBOOLE, RELSET_1, PARTFUN1, FINSEQ_1, FINSEQ_2, DOMAIN_1,
FUNCT_2, XXREAL_2, VALUED_0, NAT_1, NAT_D, STRUCT_0, ALGSTR_0, RLVECT_1,
VFUNCT_1, VECTSP_1, FINSOP_1, NORMSP_1, GROUP_4, RVSUM_1, ALGSEQ_1,
COMPLFLD, POLYNOM3, POLYNOM4, POLYNOM5, FINSET_1, MCART_1, FUNCT_4,
FUNCOP_1, CLASSES1, FVSUM_1, WSIERP_1, MEMBERED, GROUP_1, RECDEF_1,
PRE_POLY;
constructors WELLORD2, SETWISEO, REAL_1, FINSEQOP, FINSOP_1, NAT_D, WSIERP_1,
VECTSP_2, REALSET2, ALGSTR_1, GROUP_4, MATRIX_1, GOBOARD1, POLYNOM2,
POLYNOM4, POLYNOM5, RECDEF_1, BINOP_2, CLASSES1, XXREAL_2, RELSET_1,
FUNCT_7, FVSUM_1, VFUNCT_1, XTUPLE_0, ALGSEQ_1, BINOP_1, NUMBERS,
COMPLFLD;
registrations XBOOLE_0, RELAT_1, FUNCT_1, ORDINAL1, FINSET_1, NUMBERS,
XXREAL_0, XREAL_0, NAT_1, INT_1, BINOP_2, CARD_1, MEMBERED, FINSEQ_1,
STRUCT_0, VECTSP_1, COMPLFLD, ALGSTR_1, PRE_POLY, POLYNOM3, POLYNOM4,
POLYNOM5, FINSEQ_2, VALUED_0, XXREAL_2, FUNCT_2, RELSET_1, GROUP_1,
VFUNCT_1;
requirements NUMERALS, BOOLE, SUBSET, ARITHM, REAL;
definitions TARSKI, VECTSP_2, FUNCT_1, POLYNOM5;
equalities POLYNOM3, POLYNOM5, FINSEQ_2, RVSUM_1, GROUP_4, RLVECT_1, FUNCOP_1,
RELAT_1, STRUCT_0;
expansions FUNCT_1, POLYNOM5, RELAT_1;
theorems GROUP_1, CARD_1, FINSEQ_1, NAT_1, FUNCT_1, FUNCT_2, RELAT_1, TARSKI,
XBOOLE_0, XBOOLE_1, VECTSP_1, POLYNOM5, INT_1, AXIOMS, RVSUM_1, FVSUM_1,
FINSEQ_3, FINSEQ_2, POLYNOM4, POLYNOM3, FUNCT_7, ALGSEQ_1, RLVECT_1,
PBOOLE, FUNCOP_1, MATRIX_3, VECTSP_2, CARD_2, FINSEQ_5, GRAPH_5, RFINSEQ,
WELLORD2, CARD_3, ORDINAL1, FINSOP_1, MONOID_0, INTEGRA1, FUNCT_4,
XREAL_1, GROUP_4, XXREAL_0, PARTFUN1, XXREAL_2, NAT_D, FINSEQ_4,
CLASSES1, PRE_POLY, TREES_9, XREAL_0, NUMBERS;
schemes NAT_1, FUNCT_1, FUNCT_2, FRAENKEL, ALGSEQ_1, FINSEQ_1, CLASSES1,
INT_1;
begin :: Preliminaries
reconsider jj=1 as Element of REAL by XREAL_0:def 1;
theorem Th1:
for f being FinSequence of NAT st for i being Element of NAT st i
in dom f holds f.i <> 0 holds Sum f = len f iff f = (len f) |-> 1
proof
defpred P[Nat] means
for f being FinSequence of NAT st len f = $1
& for i being Element of NAT st i in dom f holds f.i <> 0 holds Sum f = len f
iff f = (len f) |-> 1;
let f be FinSequence of NAT;
A1: for n being Nat st P[n] holds P[n+1]
proof
let n be Nat;
assume
A2: P[n];
let f be FinSequence of NAT such that
A3: len f = n+1 and
A4: for i being Element of NAT st i in dom f holds f.i <> 0;
consider g being FinSequence of NAT, a being Element of NAT such that
A5: f = g^<*a*> by A3,FINSEQ_2:19;
A6: now
let i be Element of NAT;
A7: dom g c= dom f by A5,FINSEQ_1:26;
assume
A8: i in dom g;
then f.i = g.i by A5,FINSEQ_1:def 7;
hence g.i <> 0 by A4,A8,A7;
end;
n+1 = len g + len <*a*> by A3,A5,FINSEQ_1:22;
then
A9: n+1 = len g + 1 by FINSEQ_1:40;
then dom f = Seg len f & f.len f = a by A3,A5,FINSEQ_1:42,def 3;
then a <> 0 by A3,A4,FINSEQ_1:4;
then
A10: 0 qua Nat+1 <= a by NAT_1:13;
A11: g is FinSequence of REAL by FINSEQ_2:24,NUMBERS:19;
hereby
reconsider h = (len g) |-> jj as FinSequence of REAL;
reconsider h1=h as Element of (len h)-tuples_on REAL by FINSEQ_2:92;
reconsider g1=g as Element of (len g)-tuples_on REAL by A11,FINSEQ_2:92;
assume
A12: Sum f = len f;
A13: Sum g = Sum g +a -a .= n+1 -a by A3,A5,A12,RVSUM_1:74;
A14: now
let j be Nat;
reconsider a = j as Element of NAT by ORDINAL1:def 12;
assume
A15: j in Seg len g;
then j in dom g by FINSEQ_1:def 3;
then g.j <> 0 by A6;
then 0 qua Nat+1 <= g.a by NAT_1:13;
hence h1.j <= g1.j by A15,FUNCOP_1:7;
end;
A16: Sum h1 <= Sum g1 by A14,RVSUM_1:82;
Sum h = n*1 by A9,RVSUM_1:80
.= n;
then n+a <= n+1-a+a by A16,A13,XREAL_1:6;
then a <= 1 by XREAL_1:6;
then
A17: a = 1 by A10,XXREAL_0:1;
then g = (len g) |-> 1 by A2,A9,A6,A13;
hence f = (len f) |-> 1 by A3,A5,A9,A17,FINSEQ_2:60;
end;
assume f = (len f) |-> 1;
then
A18: f = (n |-> 1)^(1 |-> 1) by A3,FINSEQ_2:123
.= (n |-> 1)^<*1*> by FINSEQ_2:59;
then
A19: a = 1 by A5,FINSEQ_2:17;
A20: Sum f = Sum g + a by A5,RVSUM_1:74;
g = (len g) |-> 1 by A5,A9,A18,FINSEQ_2:17;
hence thesis by A2,A3,A9,A6,A20,A19;
end;
A21: P[ 0 ]
proof
let f be FinSequence of NAT such that
A22: len f = 0 and
for i being Element of NAT st i in dom f holds f.i <> 0;
thus Sum f = len f implies f = (len f) |-> 1 by A22;
assume f = (len f) |-> 1;
f = {} by A22;
hence thesis by RVSUM_1:72;
end;
for n being Nat holds P[n] from NAT_1:sch 2(A21, A1);
hence thesis;
end;
:: Stolen from POLYNOM2
scheme
IndFinSeq0 { k() -> Nat, P[set]} : for i being Element of NAT st
1 <= i & i <= k() holds P[i]
provided
A1: P[1] and
A2: for i being Element of NAT st 1 <= i & i < k() holds P[i] implies P[ i+1]
proof
defpred Q[Nat] means 1 <= $1 & $1 <= k() & not P[$1];
assume not for i being Element of NAT st 1 <= i & i <= k() holds P[i];
then
A3: ex k being Nat st Q[k];
consider k being Nat such that
A4: Q[k] & for k9 being Nat st Q[k9] holds k <= k9 from NAT_1:sch 5(A3);
per cases;
suppose
k = 1;
hence thesis by A1,A4;
end;
suppose
A5: k <> 1;
1 - 1 <= k - 1 by A4,XREAL_1:9;
then reconsider k9 = k - 1 as Element of NAT by INT_1:3;
A6: (k - 1) + 1 = k + (0 qua Nat);
1 < k by A4,A5,XXREAL_0:1;
then
A7: 1 <= k9 by A6,NAT_1:13;
k9 <= k9 + 1 & k9 <> k9 + 1 by NAT_1:11;
then
A8: k9 < k by XXREAL_0:1;
then k9 < k() by A4,XXREAL_0:2;
hence thesis by A2,A4,A6,A8,A7;
end;
end;
theorem Th2:
for L be add-associative right_zeroed right_complementable non
empty addLoopStr, r be FinSequence of L st len r >= 2 & for k being Element of
NAT st 2 < k & k in dom r holds r.k = 0.L holds Sum r = r/.1 + r/.2
proof
let L be add-associative right_zeroed right_complementable non empty
addLoopStr, r being FinSequence of L such that
A1: len r >= 2 and
A2: for k being Element of NAT st 2 < k & k in dom r holds r.k = 0.L;
A3: 2 in dom r by A1,FINSEQ_3:25;
1 <= len r by A1,XXREAL_0:2;
then
A4: 1 in dom r by FINSEQ_3:25;
r is not empty by A1;
then consider a being Element of L, r1 being FinSequence of L such that
A5: a = r.1 and
A6: r = <*a*>^r1 by FINSEQ_3:102;
A7: len <*a*> = 1 by FINSEQ_1:40;
then
A8: r.2 = r1.(2-1) by A1,A6,FINSEQ_1:24
.= r1.1;
len r = 1 + len r1 by A6,A7,FINSEQ_1:22;
then r1 is non empty by A1;
then consider b being Element of L, r2 being FinSequence of L such that
A9: b = r1.1 and
A10: r1 = <*b*>^r2 by FINSEQ_3:102;
A11: len <*b*> = 1 by FINSEQ_1:40;
A12: now
let i be Element of NAT such that
A13: i in dom r2;
A14: 1+i in dom r1 by A10,A11,A13,FINSEQ_1:28;
1 <= i by A13,FINSEQ_3:25;
then 1 < 1+i by NAT_1:13;
then
A15: 1+1 < 1+(1+i) by XREAL_1:8;
thus r2.i = r1.(1+i) by A10,A11,A13,FINSEQ_1:def 7
.= r.(1+(1+i)) by A6,A7,A14,FINSEQ_1:def 7
.= 0.L by A2,A6,A7,A14,A15,FINSEQ_1:28;
end;
thus Sum r = a + Sum r1 by A6,FVSUM_1:72
.= a + (b + Sum r2) by A10,FVSUM_1:72
.= a + (b + 0.L) by A12,POLYNOM3:1
.= a+b by RLVECT_1:def 4
.= r/.1 + b by A5,A4,PARTFUN1:def 6
.= r/.1 + r/.2 by A9,A3,A8,PARTFUN1:def 6;
end;
begin :: More about bags
definition
::$CD
let X be set, S be finite Subset of X, n be Element of NAT;
func (S, n)-bag -> Element of Bags X equals
(EmptyBag X) +* (S --> n);
correctness
proof
set b = (EmptyBag X) +* (S --> n);
A1: EmptyBag X = (X --> 0) by PBOOLE:def 3;
A2: dom (S --> n) = S by FUNCOP_1:13;
A3: now
let i be object;
assume not i in S;
hence b.i = (EmptyBag X).i by A2,FUNCT_4:11
.= 0 by PBOOLE:5;
end;
A4: now
let i be set such that
A5: i in S;
thus b.i = (S --> n).i by A2,A5,FUNCT_4:13
.= n by A5,FUNCOP_1:7;
end;
A6: support b is finite
proof
per cases;
suppose
A7: S is empty;
now
assume support b is non empty;
then consider x being object such that
A8: x in support b by XBOOLE_0:def 1;
b.x <> 0 by A8,PRE_POLY:def 7;
hence contradiction by A3,A7;
end;
hence thesis;
end;
suppose
A9: S is non empty & n = 0;
now
assume support b is non empty;
then consider x being object such that
A10: x in support b by XBOOLE_0:def 1;
A11: b.x <> 0 by A10,PRE_POLY:def 7;
then b.x = (S-->n).x by A2,A3,FUNCT_4:13
.= 0 by A3,A9,A11,FUNCOP_1:7;
hence contradiction by A10,PRE_POLY:def 7;
end;
hence thesis;
end;
suppose
S is non empty & n <> 0;
then for x being object holds x in S iff b.x <> 0 by A3,A4;
hence thesis by PRE_POLY:def 7;
end;
end;
dom b = dom (EmptyBag X) \/ dom (S --> n) by FUNCT_4:def 1
.= X \/ dom (S --> n) by A1,FUNCOP_1:13
.= X \/ S by FUNCOP_1:13
.= X by XBOOLE_1:12;
then (EmptyBag X) +* (S --> n) is bag of X by A6,PARTFUN1:def 2
,PRE_POLY:def 8,RELAT_1:def 18;
hence thesis by PRE_POLY:def 12;
end;
end;
::$CT 3
theorem Th3:
for X being set, S being finite Subset of X, n being Element of
NAT, i being object st not i in S holds (S, n)-bag.i = 0
proof
let X be set, S be finite Subset of X, n be Element of NAT,
i be object such that
A1: not i in S;
dom (S --> n) = S by FUNCOP_1:13;
hence (S, n)-bag.i = (EmptyBag X).i by A1,FUNCT_4:11
.= 0 by PBOOLE:5;
end;
theorem Th4:
for X being set, S being finite Subset of X, n being Element of
NAT, i being set st i in S holds (S, n)-bag.i = n
proof
let X be set, S be finite Subset of X, n be Element of NAT, i be set such
that
A1: i in S;
dom (S --> n) = S by FUNCOP_1:13;
hence (S, n)-bag.i = (S --> n).i by A1,FUNCT_4:13
.= n by A1,FUNCOP_1:7;
end;
theorem Th5:
for X being set, S being finite Subset of X, n being Element of
NAT st n <> 0 holds support (S, n)-bag = S
proof
let X be set, S be finite Subset of X, n be Element of NAT;
assume n <> 0;
then for x being object holds x in S iff (S, n)-bag.x <> 0 by Th3,Th4;
hence thesis by PRE_POLY:def 7;
end;
theorem
for X being set, S being finite Subset of X, n being Element of NAT st
S is empty or n = 0 holds (S, n)-bag = EmptyBag X
proof
let X be set, S be finite Subset of X, n be Element of NAT such that
A1: S is empty or n = 0;
now
let i be object;
assume i in X;
per cases;
suppose
i in S;
hence (S, n)-bag.i = 0 by A1,Th4
.= (EmptyBag X).i by PBOOLE:5;
end;
suppose
not i in S;
hence (S, n)-bag.i = 0 by Th3
.= (EmptyBag X).i by PBOOLE:5;
end;
end;
hence thesis by PBOOLE:3;
end;
theorem Th7:
for X being set, S, T being finite Subset of X, n being Element
of NAT st S misses T holds (S \/ T, n)-bag = (S,n)-bag + (T,n)-bag
proof
let X be set, S, T be finite Subset of X, n be Element of NAT;
assume S misses T;
then
A1: S /\ T = {} by XBOOLE_0:def 7;
now
let i be object such that
i in X;
per cases by XBOOLE_0:def 3;
suppose
A2: not i in S \/ T;
then
A3: not i in T by XBOOLE_0:def 3;
A4: not i in S by A2,XBOOLE_0:def 3;
thus (S \/ T, n)-bag.i = 0 by A2,Th3
.= (S,n)-bag.i + (0 qua Nat) by A4,Th3
.= (S,n)-bag.i + (T,n)-bag.i by A3,Th3
.= ((S,n)-bag + (T,n)-bag).i by PRE_POLY:def 5;
end;
suppose
A5: i in S;
then
A6: not i in T by A1,XBOOLE_0:def 4;
i in S \/ T by A5,XBOOLE_0:def 3;
hence (S \/ T, n)-bag.i = n by Th4
.= (S,n)-bag.i + (0 qua Nat) by A5,Th4
.= (S,n)-bag.i +(T,n)-bag.i by A6,Th3
.= ((S,n)-bag + (T,n)-bag).i by PRE_POLY:def 5;
end;
suppose
A7: i in T;
then
A8: not i in S by A1,XBOOLE_0:def 4;
i in S \/ T by A7,XBOOLE_0:def 3;
hence (S \/ T, n)-bag.i = n by Th4
.= (T,n)-bag.i + (0 qua Nat) by A7,Th4
.= (S,n)-bag.i + (T,n)-bag.i by A8,Th3
.= ((S,n)-bag + (T,n)-bag).i by PRE_POLY:def 5;
end;
end;
hence thesis by PBOOLE:3;
end;
definition
let X be set;
mode Rbag of X is real-valued finite-support ManySortedSet of X;
end;
definition
let A be set, b be Rbag of A;
func Sum b -> Real means
:Def2:
ex f being FinSequence of REAL st it = Sum f & f = b*canFS(support b);
existence
proof
set cS = canFS(support b);
set f = b*cS;
A1: rng f c= REAL;
support b c= dom b & rng cS = support b by FUNCT_2:def 3,PRE_POLY:37;
then dom f = dom cS by RELAT_1:27;
then dom f = Seg len cS by FINSEQ_1:def 3;
then f is FinSequence by FINSEQ_1:def 2;
then reconsider f as FinSequence of REAL by A1,FINSEQ_1:def 4;
take Sum f;
thus thesis;
end;
uniqueness;
end;
notation
let A be set, b be bag of A;
synonym degree b for Sum b;
end;
definition
let A be set, b be bag of A;
redefine func degree b -> Element of NAT means :: redefines degree (UPROOTS, synonym) → Sum (UPROOTS, definition)
:Def3:
ex f being FinSequence of NAT st it = Sum f & f = b*canFS(support b);
coherence
proof
consider f being FinSequence of REAL such that
A1: degree b = Sum f and
A2: f = b*canFS(support b) by Def2;
rng f c= NAT
proof
let y be object;
assume y in rng f;
then consider x being object such that
A3: x in dom f and
A4: y = f.x by FUNCT_1:def 3;
f.x = b.((canFS(support b)).x) by A2,A3,FUNCT_1:12;
hence thesis by A4;
end;
then reconsider f as FinSequence of NAT by FINSEQ_1:def 4;
Sum f is Element of NAT;
hence thesis by A1;
end;
compatibility
proof
set cS = canFS(support b);
let n be Element of NAT;
hereby
consider f being FinSequence of REAL such that
A5: degree b = Sum f and
A6: f = b*canFS(support b) by Def2;
A7: rng f c= NAT
proof
let y be object;
assume y in rng f;
then consider x being object such that
A8: x in dom f and
A9: y = f.x by FUNCT_1:def 3;
f.x = b.((canFS(support b)).x) by A6,A8,FUNCT_1:12;
hence thesis by A9;
end;
assume
A10: n = degree b;
reconsider f as FinSequence of NAT by A7,FINSEQ_1:def 4;
take f;
thus n = Sum f & f = b*cS by A10,A5,A6;
end;
given f being FinSequence of NAT such that
A11: n = Sum f & f = b*cS;
rng f c= REAL;
then reconsider f as FinSequence of REAL by FINSEQ_1:def 4;
f = f;
hence thesis by A11,Def2;
end;
end;
theorem Th8:
for A being set, b being Rbag of A st b = EmptyBag A holds Sum b = 0
proof
let A be set, b be Rbag of A;
set cS = canFS(support b);
assume b = EmptyBag A;
then b*cS = <*>NAT;
hence thesis by Def2,RVSUM_1:72;
end;
theorem Th9:
for A being set, b being bag of A st Sum b = 0 holds b = EmptyBag A
proof
let A be set, b be bag of A;
set cS = canFS(support b);
consider f being FinSequence of NAT such that
A1: degree b = Sum f and
A2: f = b*canFS(support b) by Def3;
assume
A3: degree b = 0;
now
assume
A4: support b <> {};
consider x being object such that
A5: x in support b by A4,XBOOLE_0:def 1;
x in rng cS by A5,FUNCT_2:def 3;
then consider i being Nat such that
A6: i in dom cS and
A7: cS.i = x by FINSEQ_2:10;
reconsider i as Element of NAT by ORDINAL1:def 12;
f.i = b.(cS.i) by A2,A6,FUNCT_1:13;
then
A8: f.i <> 0 by A5,A7,PRE_POLY:def 7;
support b c= dom b by PRE_POLY:37;
then
A9: i in dom f & 0 < f.i
by A8,A2,A5,A6,A7,FUNCT_1:11;
for i be Nat st i in dom f holds 0 <= f.i;
hence contradiction by A3,A1,A9,RVSUM_1:85;
end;
hence thesis by PRE_POLY:81;
end;
theorem Th10:
for A being set, S being finite Subset of A, b being bag of A
holds S = support b & degree b = card S iff b = (S, 1)-bag
proof
let A be set, S be finite Subset of A, b be bag of A;
set cS = canFS(S);
set f = b*cS;
A1: dom b = A by PARTFUN1:def 2;
set g = (card S) |-> 1;
A2: len cS = card S by FINSEQ_1:93;
A3: rng cS = S by FUNCT_2:def 3;
then
A4: dom f = dom cS by A1,RELAT_1:27;
then dom f = Seg len cS by FINSEQ_1:def 3;
then reconsider f as FinSequence by FINSEQ_1:def 2;
A5: len cS = len f by A4,FINSEQ_3:29;
hereby
set sb = (S, 1)-bag;
assume that
A6: S = support b and
A7: degree b = card S;
consider F being FinSequence of NAT such that
A8: degree b = Sum F and
A9: F = b*cS by A6,Def3;
now
let i be Element of NAT;
assume i in dom F;
then F.i = b.(cS.i) & cS.i in rng cS by A4,A9,FUNCT_1:3,12;
hence F.i <> 0 by A6,PRE_POLY:def 7;
end;
then
A10: F = len F |-> 1 by A2,A5,A7,A8,A9,Th1;
A11: support b = support sb by A6,Th5;
now
thus dom b = dom sb by A1,PARTFUN1:def 2;
let x be object;
assume x in dom b;
per cases;
suppose
A12: x in support b;
then
A13: cS".x in dom cS by A3,A6,FUNCT_1:32;
then
A14: cS".x in Seg len F by A4,A9,FINSEQ_1:def 3;
rng cS = support b by A6,FUNCT_2:def 3;
hence b.x = b.(cS.(cS".x)) by A12,FUNCT_1:35
.= F.(cS".x) by A9,A13,FUNCT_1:13
.= 1 by A10,A14,FUNCOP_1:7
.= sb.x by A6,A12,Th4;
end;
suppose
A15: not x in support b;
hence b.x = 0 by PRE_POLY:def 7
.= sb.x by A11,A15,PRE_POLY:def 7;
end;
end;
hence b = (S, 1)-bag;
end;
rng f c= NAT
proof
let y be object;
assume y in rng f;
then consider x being object such that
A16: x in dom f and
A17: y = f.x by FUNCT_1:def 3;
f.x = b.(cS.x) by A16,FUNCT_1:12;
hence thesis by A17;
end;
then reconsider f as FinSequence of NAT by FINSEQ_1:def 4;
assume
A18: b = (S, 1)-bag;
A19: rng cS = S by FUNCT_2:def 3;
now
thus len f = card S by A4,A2,FINSEQ_3:29;
thus len g = card S by CARD_1:def 7;
let i be Nat;
A20: dom f = Seg card S by A4,A2,FINSEQ_1:def 3;
assume
A21: i in dom f;
hence f.i = b.(cS.i) by FUNCT_1:12
.= 1 by A4,A19,A18,A21,Th4,FUNCT_1:3
.= g.i by A20,A21,FUNCOP_1:7;
end;
then
A22: f = g by FINSEQ_2:9;
thus S = support b by A18,Th5;
then degree b = Sum f by Def3;
hence degree b = (card S)*1 by A22,RVSUM_1:80
.= card S;
end;
theorem Th11:
for A being set, S being finite Subset of A, b being Rbag of A
st support b c= S ex f being FinSequence of REAL st f = b*canFS(S) & Sum b =
Sum f
proof
let A be set, S be finite Subset of A, b be Rbag of A such that
A1: support b c= S;
A2: card support b <= card S by A1,NAT_1:43;
set cs = canFS(support b);
A3: rng cs = support b by FUNCT_2:def 3;
set cS = canFS(S);
set f = b*cS;
len cS = card S by FINSEQ_1:93;
then
A4: dom cS = Seg card S by FINSEQ_1:def 3;
len cs = card support b by FINSEQ_1:93;
then
A5: dom cs = Seg card support b by FINSEQ_1:def 3;
consider g being FinSequence of REAL such that
A6: Sum b = Sum g and
A7: g = b*cs by Def2;
A8: dom b = A by PARTFUN1:def 2;
then
A9: dom g = Seg card support b by A1,A7,A5,A3,RELAT_1:27,XBOOLE_1:1;
then
A10: len g = card support b by FINSEQ_1:def 3;
A11: rng cS = S by FUNCT_2:def 3;
then
A12: dom f = Seg card S by A4,A8,RELAT_1:27;
then reconsider f as FinSequence by FINSEQ_1:def 2;
rng f c= rng b by RELAT_1:26;
then rng f c= REAL by XBOOLE_1:1;
then reconsider f as FinSequence of REAL by FINSEQ_1:def 4;
take f;
thus f = b*canFS(S);
per cases by A2,XXREAL_0:1;
suppose
A13: card support b < card S;
set dd = {j where j is Element of NAT : j in dom f & f.j = 0};
A14: now
consider x being object such that
A15: not (x in support b iff x in S) by A13,TARSKI:2;
consider j being object such that
A16: j in dom cS and
A17: cS.j = x by A1,A11,A15,FUNCT_1:def 3;
reconsider j as Element of NAT by A16;
f.j =b.x by A16,A17,FUNCT_1:13;
then f.j = 0 by A1,A15,PRE_POLY:def 7;
then j in dd by A4,A12,A16;
hence dd is non empty;
end;
reconsider gr = g as FinSequence of REAL;
A18: dd c= dom f
proof
let x be object;
assume x in dd;
then ex j being Element of NAT st x = j & j in dom f & f.j = 0;
hence thesis;
end;
then reconsider dd as finite non empty set by A14;
consider d being Element of NAT such that
A19: card S = (card support b) + d and
1 <= d by A13,FINSEQ_4:84;
set h = d |-> (In(0,REAL));
set F = gr^h;
rng canFS(dd) = dd & dd c= NAT by A18,FUNCT_2:def 3,XBOOLE_1:1;
then reconsider cdd = canFS(dd) as FinSequence of NAT by FINSEQ_1:def 4;
set cdi = cdd qua Function";
reconsider cdi as Function of dd, Seg card dd by FINSEQ_1:95;
reconsider cdi as Function of dd, NAT by FUNCT_2:7;
deffunc Z(object) = cdi /. $1 + card support b;
consider z being Function such that
A20: dom z = dd and
A21: for x being object st x in dd holds z.x = Z(x) from FUNCT_1:sch 3;
set p = cs"*cS +* z;
A22: dom cdi = dd by FUNCT_2:def 1;
set cSr = cS | (dom f \ dd);
now
let y be object;
hereby
assume y in rng cSr;
then consider x being object such that
A23: x in dom cSr and
A24: y = cSr.x by FUNCT_1:def 3;
A25: cSr.x = cS.x by A23,FUNCT_1:47;
x in dom cS by A23,RELAT_1:57;
then reconsider j = x as Element of NAT;
dom cSr c= dom f \ dd by RELAT_1:58;
then
A26: x in findom f \ dd by A23;
then not j in dd by XBOOLE_0:def 5;
then
A27: f.j <> 0 by A26;
x in dom cS by A23,RELAT_1:57;
then b.(cS.j) <> 0 by A27,FUNCT_1:13;
hence y in support b by A24,A25,PRE_POLY:def 7;
end;
assume
A28: y in support b;
then consider x being object such that
A29: x in dom cS and
A30: y = cS.x by A1,A11,FUNCT_1:def 3;
now
assume x in dd;
then consider j being Element of NAT such that
A31: j = x and
A32: j in dom f & f.j = 0;
0 = b.(cS.j) by A4,A12,A32,FUNCT_1:13;
hence contradiction by A28,A30,A31,PRE_POLY:def 7;
end;
then x in dom f \ dd by A4,A12,A29,XBOOLE_0:def 5;
hence y in rng cSr by A29,A30,FUNCT_1:50;
end;
then
A33: rng cSr = support b by TARSKI:2;
(findom f \ dd) /\ dom f = dom f \ dd by XBOOLE_1:28;
then cSr is one-to-one & dom cSr = (dom f \ dd) by A4,A12,FUNCT_1:52
,RELAT_1:61;
then support b, dom f \dd are_equipotent by A33,WELLORD2:def 4;
then
A34: card support b = card (dom f \ dd) by CARD_1:5;
card (dom f \ dd) = card dom f - card dd by A18,CARD_2:44;
then
A35: card support b + card dd = card S by A12,A34,FINSEQ_1:57;
A36: now
A37: dom (cs") = support b by A3,FUNCT_1:33;
assume dom (cs"*cS) /\ dom z <> {};
then consider x being object such that
A38: x in dom (cs"*cS) /\ dom z by XBOOLE_0:def 1;
x in dom z by A38,XBOOLE_0:def 4;
then consider j being Element of NAT such that
A39: j = x and
j in dom f and
A40: f.j = 0 by A20;
A41: x in dom (cs"*cS) by A38,XBOOLE_0:def 4;
then j in dom cS by A39,FUNCT_1:11;
then f.j = b.(cS.j) by FUNCT_1:13;
then not cS.j in support b by A40,PRE_POLY:def 7;
hence contradiction by A41,A39,A37,FUNCT_1:11;
end;
len F = len g + len h by FINSEQ_1:22
.= card S by A10,A19,CARD_1:def 7;
then
A42: dom F = Seg card S by FINSEQ_1:def 3;
now
let x be object;
hereby
assume
A43: x in dom (cs"*cS) \/ dom z;
per cases by A43,XBOOLE_0:def 3;
suppose
x in dom (cs"*cS);
hence x in dom F by A4,A42,FUNCT_1:11;
end;
suppose
x in dom z;
hence x in dom F by A12,A42,A18,A20;
end;
end;
assume
A44: x in dom F;
then reconsider i = x as Element of NAT;
per cases;
suppose
f.x = 0;
then i in dom z by A12,A42,A20,A44;
hence x in dom (cs"*cS) \/ dom z by XBOOLE_0:def 3;
end;
suppose
A45: f.x <> 0;
f.i = b.(cS.i) by A4,A42,A44,FUNCT_1:13;
then cS.i in support b by A45,PRE_POLY:def 7;
then cS. i in dom (cs") by A3,FUNCT_1:33;
then i in dom (cs"*cS) by A4,A42,A44,FUNCT_1:11;
hence x in dom (cs"*cS) \/ dom z by XBOOLE_0:def 3;
end;
end;
then
A46: dom (cs"*cS) \/ dom z = dom F by TARSKI:2;
then
A47: dom p = dom F by FUNCT_4:def 1;
len cdd = card dd by FINSEQ_1:93;
then
A48: dom cdd = Seg d by A19,A35,FINSEQ_1:def 3;
then
A49: rng cdi = Seg d by FUNCT_1:33;
A50: rng z c= Seg card S
proof
let y be object;
assume y in rng z;
then consider x being object such that
A51: x in dom z and
A52: y = z.x by FUNCT_1:def 3;
A53: cdi/.x = cdi.x & cdi.x in Seg d by A22,A49,A20,A51,FUNCT_1:3
,PARTFUN1:def 6;
then 1 <= cdi/.x by FINSEQ_1:1;
then
A54: 1 <= cdi/.x + card support b by NAT_1:12;
cdi/.x <= d by A53,FINSEQ_1:1;
then
A55: cdi/.x + card support b <= d + card support b by XREAL_1:6;
y = cdi/.x + card support b by A20,A21,A51,A52;
hence thesis by A19,A54,A55,FINSEQ_1:1;
end;
A56: now
let x be object such that
A57: x in dom F;
per cases by A46,A57,XBOOLE_0:def 3;
suppose
A58: x in dom (cs"*cS);
then (cs"*cS).x in rng (cs"*cS) by FUNCT_1:3;
then (cs"*cS).x in rng (cs") by FUNCT_1:14;
then
A59: (cs"*cS).x in dom cs by FUNCT_1:33;
not x in dom z by A36,A58,XBOOLE_0:def 4;
then
A60: p.x = (cs"*cS).x by FUNCT_4:11;
Seg card support b c= Seg card S by A2,FINSEQ_1:5;
hence p.x in dom F by A5,A42,A60,A59;
end;
suppose
x in dom z;
then p.x = z.x & z.x in rng z by FUNCT_1:3,FUNCT_4:13;
hence p.x in dom F by A42,A50;
end;
end;
A61: dom p = dom (cs"*cS) \/ dom z by FUNCT_4:def 1;
reconsider p as Function of dom F, dom F by A47,A56,FUNCT_2:3;
len h = d by CARD_1:def 7;
then
A62: dom h = Seg d by FINSEQ_1:def 3;
A63: rng cdd = dd by FUNCT_2:def 3;
now
let x be object;
hereby
assume x in rng p;
then consider a being object such that
A64: a in dom p and
A65: x = p.a by FUNCT_1:def 3;
per cases by A64,FUNCT_4:12;
suppose
A66: a in dom (cs"*cS);
then cS.a in dom (cs") by FUNCT_1:11;
then cs".(cS.a) in rng (cs") by FUNCT_1:3;
then
A67: cs".(cS.a) in dom cs by FUNCT_1:33;
not a in dom z by A36,A66,XBOOLE_0:def 4;
then
A68: p.a = (cs"*cS).a by FUNCT_4:11
.= cs".(cS.a) by A66,FUNCT_1:12;
dom cs c= dom F by A5,A2,A42,FINSEQ_1:5;
hence x in dom F by A65,A68,A67;
end;
suppose
a in dom z;
then z.a in rng z & p.a = z.a by FUNCT_1:3,FUNCT_4:13;
hence x in dom F by A42,A50,A65;
end;
end;
assume
A69: x in dom F;
then reconsider j = x as Element of NAT;
per cases by A69,FINSEQ_1:25;
suppose
A70: j in dom gr;
then
A71: cs.j in support b by A5,A3,A9,FUNCT_1:3;
then
A72: cS".(cs.j) in Seg card S by A1,A4,A11,FUNCT_1:32;
now
assume cS".(cs.j) in dom z;
then
A73: ex k being Element of NAT st k = cS".(cs.j) & k in dom f & f.k
= 0 by A20;
(b*cS).(cS".(cs.j)) = b.(cS.(cS".(cs.j))) by A4,A72,FUNCT_1:13
.= b.(cs.j) by A1,A11,A71,FUNCT_1:35;
hence contradiction by A71,A73,PRE_POLY:def 7;
end;
then p.(cS".(cs.j)) = (cs"*cS).(cS".(cs.j)) by FUNCT_4:11
.= cs".(cS.(cS".(cs.j))) by A4,A72,FUNCT_1:13
.= cs".(cs.j) by A1,A11,A71,FUNCT_1:35
.= j by A5,A9,A70,FUNCT_1:34;
hence x in rng p by A42,A47,A72,FUNCT_1:3;
end;
suppose
ex n being Nat st n in dom h & j=len gr + n;
then consider n being Nat such that
A74: n in dom h and
A75: j = len gr + n;
A76: cdd.n in dd by A62,A48,A63,A74,FUNCT_1:3;
p.(cdd.n) = z.(cdd.n) by A62,A48,A63,A20,A74,FUNCT_1:3,FUNCT_4:13
.= cdi /. (cdd.n) + card support b by A62,A48,A63,A21,A74,FUNCT_1:3
.= cdi.(cdd.n) + card support b by A62,A48,A63,A22,A74,FUNCT_1:3
,PARTFUN1:def 6
.= n + card support b by A62,A48,A74,FUNCT_1:34
.= j by A9,A75,FINSEQ_1:def 3;
hence x in rng p by A12,A42,A18,A47,A76,FUNCT_1:3;
end;
end;
then
A77: rng p = dom F by TARSKI:2;
then
A78: dom (F*p) = dom F by A47,RELAT_1:27;
now
let x be object;
assume
A79: x in dom f;
per cases;
suppose
A80: f.x = 0;
reconsider cdix = cdi /. x as Element of NAT;
reconsider px = p.x as Element of NAT by ORDINAL1:def 12;
reconsider j = x as Element of NAT by A79;
A81: j in dom z by A20,A79,A80;
then
A82: p.x = z.x by FUNCT_4:13
.= cdi /. x + card support b by A20,A21,A81;
A83: cdi.x in Seg card dd by A20,A81,FUNCT_2:5;
dom cdi = dd by FUNCT_2:def 1;
then
A84: cdi /. x = cdi.x by A20,A81,PARTFUN1:def 6;
thus f.x = h.(cdix) by A80
.= F.px by A10,A19,A62,A35,A82,A84,A83,FINSEQ_1:def 7
.= (F*p).x by A12,A42,A78,A79,FUNCT_1:12;
end;
suppose
A85: f.x <> 0;
reconsider px = p.x as Element of NAT by ORDINAL1:def 12;
f.x = b.(cS.x) by A79,FUNCT_1:12;
then cS.x in support b by A85,PRE_POLY:def 7;
then
A86: cS.x in rng cs by FUNCT_2:def 3;
then
A87: cs".(cS.x) in dom cs by FUNCT_1:32;
now
assume x in dd;
then ex j being Element of NAT st j=x & j in dom f & f.j = 0;
hence contradiction by A85;
end;
then
A88: p.x = (cs"*cS).x by A20,FUNCT_4:11
.= cs".(cS.x) by A4,A12,A79,FUNCT_1:13;
thus f.x = b.(cS.x) by A79,FUNCT_1:12
.= b.(cs.px) by A86,A88,FUNCT_1:32
.= g.(px) by A7,A87,A88,FUNCT_1:13
.= F.(px) by A5,A9,A87,A88,FINSEQ_1:def 7
.= (F*p).x by A12,A42,A78,A79,FUNCT_1:12;
end;
end;
then
A89: f = F*p by A4,A11,A8,A42,A78,RELAT_1:27;
A90: p is one-to-one
proof
let a, c be object such that
A91: a in dom p & c in dom p and
A92: p.a = p.c;
per cases by A61,A91,XBOOLE_0:def 3;
suppose
A93: a in dom (cs"*cS) & c in dom (cs"*cS);
then cS.a in dom (cs") by FUNCT_1:11;
then cS.a in rng cs by FUNCT_1:33;
then
A94: cs.(cs".(cS.a)) = cS.a by FUNCT_1:35;
a in dom cS by A93,FUNCT_1:11;
then
A95: cS".(cS.a) = a by FUNCT_1:34;
cS.c in dom (cs") by A93,FUNCT_1:11;
then
A96: cS.c in rng cs by FUNCT_1:33;
not c in dom z by A36,A93,XBOOLE_0:def 4;
then
A97: p.c = (cs"*cS).c by FUNCT_4:11
.= cs".(cS.c) by A93,FUNCT_1:12;
A98: c in dom cS by A93,FUNCT_1:11;
not a in dom z by A36,A93,XBOOLE_0:def 4;
then p.a = (cs"*cS).a by FUNCT_4:11
.= cs".(cS.a) by A93,FUNCT_1:12;
then cS".(cS.a) = cS".(cS.c) by A92,A97,A94,A96,FUNCT_1:35;
hence thesis by A95,A98,FUNCT_1:34;
end;
suppose
A99: a in dom (cs"*cS) & c in dom z;
then cS.a in dom (cs") by FUNCT_1:11;
then cs".(cS.a) in rng (cs") by FUNCT_1:3;
then
A100: cs".(cS.a) in dom cs by FUNCT_1:33;
not a in dom z by A36,A99,XBOOLE_0:def 4;
then
A101: p.a = (cs"*cS).a by FUNCT_4:11
.= cs".(cS.a) by A99,FUNCT_1:12;
p.c = z.c by A99,FUNCT_4:13
.= cdi /. c + card support b by A20,A21,A99;
then cdi /. c + card support b <= (0 qua Nat)+card support b by A5,A92
,A101,A100,FINSEQ_1:1;
then cdi /. c = 0 by XREAL_1:6;
then
A102: cdi.c = 0 by A22,A20,A99,PARTFUN1:def 6;
cdi.c in rng cdi by A22,A20,A99,FUNCT_1:3;
hence thesis by A49,A102,FINSEQ_1:1;
end;
suppose
A103: a in dom z & c in dom (cs"*cS);
then cS.c in dom (cs") by FUNCT_1:11;
then cs".(cS.c) in rng (cs") by FUNCT_1:3;
then
A104: cs".(cS.c) in dom cs by FUNCT_1:33;
not c in dom z by A36,A103,XBOOLE_0:def 4;
then
A105: p.c = (cs"*cS).c by FUNCT_4:11
.= cs".(cS.c) by A103,FUNCT_1:12;
p.a = z.a by A103,FUNCT_4:13
.= cdi /. a + card support b by A20,A21,A103;
then cdi /. a + card support b <= (0 qua Nat)+card support b by A5,A92
,A105,A104,FINSEQ_1:1;
then cdi /. a = 0 by XREAL_1:6;
then
A106: cdi.a = 0 by A22,A20,A103,PARTFUN1:def 6;
cdi.a in rng cdi by A22,A20,A103,FUNCT_1:3;
hence thesis by A49,A106,FINSEQ_1:1;
end;
suppose
A107: a in dom z & c in dom z;
then
A108: cdi /. a = cdi . a & cdi /. c = cdi . c by A22,A20,PARTFUN1:def 6;
A109: p.c = z.c by A107,FUNCT_4:13
.= cdi /. c + card support b by A20,A21,A107;
p.a = z.a by A107,FUNCT_4:13
.= cdi /. a + card support b by A20,A21,A107;
hence thesis by A22,A20,A92,A107,A109,A108,FUNCT_1:def 4;
end;
end;
Sum h = 0 by RVSUM_1:81;
then
A110: Sum gr = Sum gr + Sum h .= Sum F by RVSUM_1:75;
p is onto by A77,FUNCT_2:def 3;
hence thesis by A6,A90,A89,A110,FINSOP_1:7;
end;
suppose
card support b = card S;
hence thesis by A1,A6,A7,CARD_2:102;
end;
end;
theorem Th12:
for A being set, b, b1, b2 being Rbag of A st b = b1 + b2 holds
Sum b = Sum b1 + Sum b2
proof
let A be set, b, b1, b2 be Rbag of A;
set S = support b;
set SS = support b1 \/ support b2;
A1: dom b2 = A by PARTFUN1:def 2;
then
A2: support b2 c= A by PRE_POLY:37;
A3: dom b1 = A by PARTFUN1:def 2;
then support b1 c= A by PRE_POLY:37;
then reconsider SS as finite Subset of A by A2,XBOOLE_1:8;
set cS = canFS SS;
consider f1r being FinSequence of REAL such that
A4: f1r = b1*canFS(SS) and
A5: Sum b1 = Sum f1r by Th11,XBOOLE_1:7;
A6: rng cS = SS by FUNCT_2:def 3;
then
A7: dom f1r = dom cS by A3,A4,RELAT_1:27;
assume
A8: b = b1 + b2;
then S c= SS by PRE_POLY:75;
then consider f being FinSequence of REAL such that
A9: f = b*canFS(SS) and
A10: Sum b = Sum f by Th11;
dom b = A by PARTFUN1:def 2;
then
A11: dom f = dom cS by A9,A6,RELAT_1:27;
then
A12: len f1r = len f by A7,FINSEQ_3:29;
consider f2r being FinSequence of REAL such that
A13: f2r = b2*canFS(SS) and
A14: Sum b2 = Sum f2r by Th11,XBOOLE_1:7;
A15: dom f2r = dom cS by A1,A13,A6,RELAT_1:27;
A16: now
let k be Element of NAT such that
A17: k in dom f1r;
A18: f1r/.k = f1r.k by A17,PARTFUN1:def 6
.= b1.(cS.k) by A4,A17,FUNCT_1:12;
A19: f.k = b.(cS.k) by A9,A11,A7,A17,FUNCT_1:12;
f2r/.k = f2r.k by A7,A15,A17,PARTFUN1:def 6
.= b2.(cS.k) by A13,A7,A15,A17,FUNCT_1:12;
hence f.k = f1r/.k + f2r/.k by A8,A18,A19,PRE_POLY:def 5;
end;
len f1r = len f2r by A7,A15,FINSEQ_3:29;
hence thesis by A10,A5,A14,A12,A16,INTEGRA1:21;
end;
theorem Th13: :: GROUP_4:18 but about a different Product
for L being associative commutative unital non empty multMagma
, f, g being FinSequence of L, p being Permutation of dom f st g = f * p holds
Product(g) = Product(f)
proof
let L be associative commutative unital non empty multMagma, f, g be
FinSequence of L, p be Permutation of dom f such that
A1: g = f * p;
set mL = (the multF of L);
mL is commutative & mL is associative by MONOID_0:def 11;
hence thesis by A1,FINSOP_1:7;
end;
begin :: More on polynomials
definition
let L be non empty ZeroStr, p be Polynomial of L;
attr p is non-zero means
:Def4:
p <> 0_. L;
end;
theorem Th14:
for L being non empty ZeroStr, p being Polynomial of L holds p
is non-zero iff len p > 0
proof
let L be non empty ZeroStr, p be Polynomial of L;
hereby
assume p is non-zero;
then p <> 0_. L;
then len p <> 0 by POLYNOM4:5;
hence len p > 0;
end;
assume len p > 0;
then p <> 0_. L by POLYNOM4:3;
hence thesis;
end;
registration
let L be non trivial ZeroStr;
cluster non-zero for Polynomial of L;
existence
proof
set a = the Element of NonZero L;
reconsider a as Element of L;
take p = <%a%>;
A1: ( not a in {0.L})& (0_. L).0 = 0.L by FUNCOP_1:7,XBOOLE_0:def 5;
p.0 = a by POLYNOM5:32;
then p <> 0_. L by A1,TARSKI:def 1;
hence thesis;
end;
end;
registration
let L be non degenerated non empty multLoopStr_0, x be Element of L;
cluster <%x, 1.L%> -> non-zero;
correctness
proof
len <%x, 1.L%> = 2 by POLYNOM5:40;
hence thesis by Th14;
end;
end;
theorem Th15:
for L being non empty ZeroStr, p being Polynomial of L st len p
> 0 holds p.(len p -'1) <> 0.L
proof
let L be non empty ZeroStr, p be Polynomial of L;
assume len p > 0;
then ex k being Nat st len p = k+1 by NAT_1:6;
then len p = (len p -'1)+1 by NAT_D:34;
hence thesis by ALGSEQ_1:10;
end;
theorem Th16:
for L being non empty ZeroStr, p being AlgSequence of L st len p
= 1 holds p = <%p.0%> & p.0 <> 0.L
proof
let L be non empty ZeroStr, p being AlgSequence of L such that
A1: len p = 1;
thus p=<%p.0%> by A1,ALGSEQ_1:def 5;
hence thesis by A1,ALGSEQ_1:14;
end;
theorem Th17: :: from POLYNOM4:5 right-distributive
for L be add-associative right_zeroed right_complementable
right-distributive non empty doubleLoopStr, p be Polynomial of L holds p*'(
0_.(L)) = 0_.(L)
proof
let L be add-associative right_zeroed right_complementable
right-distributive non empty doubleLoopStr, p be Polynomial of L;
now
let i be Element of NAT;
consider r be FinSequence of L such that
len r = i+1 and
A1: (p*'(0_.(L))).i = Sum r and
A2: for k be Element of NAT st k in dom r holds r.k = p.(k-'1) * (0_.
L).(i+1-'k) by POLYNOM3:def 9;
now
let k be Element of NAT;
assume k in dom r;
hence r.k = p.(k-'1) * (0_. L).(i+1-'k) by A2
.= p.(k-'1) * 0.L by FUNCOP_1:7
.= 0.L;
end;
hence (p*'(0_.(L))).i = 0.L by A1,POLYNOM3:1
.= (0_.(L)).i by FUNCOP_1:7;
end;
hence thesis by FUNCT_2:63;
end;
registration
cluster algebraic-closed add-associative right_zeroed right_complementable
Abelian commutative associative distributive domRing-like non degenerated
for
unital non empty doubleLoopStr;
existence
proof
take F_Complex;
thus thesis;
end;
end;
theorem Th18:
for L being add-associative right_zeroed right_complementable
distributive domRing-like non empty doubleLoopStr, p, q being Polynomial of L
st p*'q = 0_. L holds p = 0_. L or q = 0_. L
proof
let L be add-associative right_zeroed right_complementable distributive
domRing-like non empty doubleLoopStr, p, q being Polynomial of L such that
A1: p*'q = 0_. L and
A2: p <> 0_. L and
A3: q <> 0_. L;
consider lp1 being Nat such that
A4: len p = lp1+1 by A2,NAT_1:6,POLYNOM4:5;
len p <> 0 by A2,POLYNOM4:5;
then
A5: 0 qua Nat+1 <= len p by NAT_1:13;
consider lq1 being Nat such that
A6: len q = lq1+1 by A3,NAT_1:6,POLYNOM4:5;
reconsider lp1, lq1 as Element of NAT by ORDINAL1:def 12;
A7: p.lp1 <> 0.L by A4,ALGSEQ_1:10;
A8: q.lq1 <> 0.L by A6,ALGSEQ_1:10;
set lpq = lp1 + lq1;
consider r being FinSequence of L such that
A9: len r = lpq+1 and
A10: (p*'q).lpq = Sum r and
A11: for k be Element of NAT st k in dom r holds r.k=p.(k-'1)*q.(lpq+1-'
k) by POLYNOM3:def 9;
A12: lpq+1-'len p = lq1+(lp1+1)-'len p .= lq1 by A4,NAT_D:34;
len p <= lp1+1+lq1 by A4,NAT_1:12;
then
A13: len p in dom r by A9,A5,FINSEQ_3:25;
now
let k be Nat such that
A14: k in dom r and
A15: k <> len p;
reconsider k1=k as Element of NAT by ORDINAL1:def 12;
A16: r.k1 = p.(k1-'1) * q.(lpq+1-'k1) by A11,A14;
per cases by A15,XXREAL_0:1;
suppose
k < len p;
then consider d being Element of NAT such that
A17: len p = k1+d and
A18: 1 <= d by FINSEQ_4:84;
A19: len q <= lq1+d by A6,A18,XREAL_1:6;
lpq+1-'k = lq1+d+k-'k by A4,A17
.= lq1+d by NAT_D:34;
hence r.k = p.(k-'1)*0.L by A16,A19,ALGSEQ_1:8
.= 0.L;
end;
suppose
k > len p;
then k >= len p + 1 by NAT_1:13;
then k-'1 >= len p + 1-'1 by NAT_D:42;
then k-'1 >= len p by NAT_D:34;
hence r.k = 0.L * q.(lpq+1-'k) by A16,ALGSEQ_1:8
.= 0.L;
end;
end;
then Sum r = r.(len p) by A13,MATRIX_3:12
.= p.(len p -'1)*q.(lpq+1-'len p) by A11,A13
.= p.lp1 * q.lq1 by A4,A12,NAT_D:34;
then Sum r <> 0.L by A7,A8,VECTSP_2:def 1;
hence contradiction by A1,A10,FUNCOP_1:7;
end;
registration
let L be add-associative right_zeroed right_complementable distributive
domRing-like non empty doubleLoopStr;
cluster Polynom-Ring L -> domRing-like;
correctness
proof
set PRL = Polynom-Ring L;
let x, y be Element of PRL;
reconsider xp = x, yp = y as Polynomial of L by POLYNOM3:def 10;
A1: 0_. L = 0.PRL by POLYNOM3:def 10;
assume x*y = 0.PRL;
then xp*'yp = 0_. L by A1,POLYNOM3:def 10;
hence thesis by A1,Th18;
end;
end;
registration
let L be domRing, p, q be non-zero Polynomial of L;
cluster p*'q -> non-zero;
correctness
by Th18;
end;
theorem
for L being non degenerated comRing, p, q being Polynomial of L holds
Roots p \/ Roots q c= Roots (p*'q)
proof
let L be non degenerated comRing, p, q being Polynomial of L;
let x be object;
assume
A1: x in Roots p \/ Roots q;
per cases by A1,XBOOLE_0:def 3;
suppose
A2: x in Roots p;
then reconsider a = x as Element of L;
a is_a_root_of p by A2,POLYNOM5:def 10;
then eval(p,a) = 0.L;
then eval(p,a) * eval(q,a) = 0.L;
then eval(p*'q,a) = 0.L by POLYNOM4:24;
then a is_a_root_of p*'q;
hence thesis by POLYNOM5:def 10;
end;
suppose
A3: x in Roots q;
then reconsider a = x as Element of L;
a is_a_root_of q by A3,POLYNOM5:def 10;
then eval(q,a) = 0.L;
then eval(p,a) * eval(q,a) = 0.L;
then eval(p*'q,a) = 0.L by POLYNOM4:24;
then a is_a_root_of p*'q;
hence thesis by POLYNOM5:def 10;
end;
end;
theorem Th20:
for L being domRing, p, q being Polynomial of L holds Roots (p*'
q) = Roots p \/ Roots q
proof
let L be domRing, p, q being Polynomial of L;
now
let x be object;
hereby
assume
A1: x in Roots (p*'q);
then reconsider a = x as Element of L;
a is_a_root_of p*'q by A1,POLYNOM5:def 10;
then eval(p*'q,a) = 0.L;
then
A2: eval(p,a) * eval(q,a) = 0.L by POLYNOM4:24;
per cases by A2,VECTSP_2:def 1;
suppose
eval(p,a) = 0.L;
then a is_a_root_of p;
then a in Roots p by POLYNOM5:def 10;
hence x in Roots p \/ Roots q by XBOOLE_0:def 3;
end;
suppose
eval(q,a) = 0.L;
then a is_a_root_of q;
then a in Roots q by POLYNOM5:def 10;
hence x in Roots p \/ Roots q by XBOOLE_0:def 3;
end;
end;
assume
A3: x in Roots p \/ Roots q;
per cases by A3,XBOOLE_0:def 3;
suppose
A4: x in Roots p;
then reconsider a = x as Element of L;
a is_a_root_of p by A4,POLYNOM5:def 10;
then eval(p,a) = 0.L;
then eval(p,a) * eval(q,a) = 0.L;
then eval(p*'q,a) = 0.L by POLYNOM4:24;
then a is_a_root_of p*'q;
hence x in Roots (p*'q) by POLYNOM5:def 10;
end;
suppose
A5: x in Roots q;
then reconsider a = x as Element of L;
a is_a_root_of q by A5,POLYNOM5:def 10;
then eval(q,a) = 0.L;
then eval(p,a) * eval(q,a) = 0.L;
then eval(p*'q,a) = 0.L by POLYNOM4:24;
then a is_a_root_of p*'q;
hence x in Roots (p*'q) by POLYNOM5:def 10;
end;
end;
hence thesis by TARSKI:2;
end;
theorem Th21:
for L being add-associative right_zeroed right_complementable
distributive non empty doubleLoopStr, p being (Polynomial of L), pc being (
Element of Polynom-Ring L) st p = pc holds -p = -pc
proof
let L be add-associative right_zeroed right_complementable distributive non
empty doubleLoopStr, p be (Polynomial of L), pc be (Element of Polynom-Ring L)
such that
A1: p = pc;
set PRL = Polynom-Ring L;
reconsider mpc = -p as Element of PRL by POLYNOM3:def 10;
p+-p = p-p .= 0_. L by POLYNOM3:29;
then pc + mpc = 0_. L by A1,POLYNOM3:def 10
.= 0.PRL by POLYNOM3:def 10;
hence thesis by RLVECT_1:def 10;
end;
theorem Th22:
for L being add-associative right_zeroed right_complementable
distributive non empty doubleLoopStr, p, q being (Polynomial of L), pc, qc
being (Element of Polynom-Ring L) st p= pc & q = qc holds p-q = pc-qc
proof
let L be add-associative right_zeroed right_complementable distributive non
empty doubleLoopStr, p,q be (Polynomial of L), pc,qc be (Element of
Polynom-Ring L) such that
A1: p = pc and
A2: q = qc;
-q = -qc by A2,Th21;
hence thesis by A1,POLYNOM3:def 10;
end;
theorem Th23:
for L being Abelian add-associative right_zeroed
right_complementable distributive non empty doubleLoopStr, p, q, r being (
Polynomial of L) holds p*'q-p*'r = p*'(q-r)
proof
let L be Abelian add-associative right_zeroed right_complementable
distributive non empty doubleLoopStr, p, q, r be (Polynomial of L);
set PRL = Polynom-Ring L;
reconsider pc = p, qc = q, rc = r as Element of PRL by POLYNOM3:def 10;
A1: qc-rc = q-r by Th22;
p*'q = pc*qc & p*'r = pc*rc by POLYNOM3:def 10;
hence p*'q-p*'r = pc*qc - pc*rc by Th22
.= pc*(qc-rc) by VECTSP_1:11
.= p*'(q-r) by A1,POLYNOM3:def 10;
end;
theorem Th24:
for L being add-associative right_zeroed right_complementable
distributive non empty doubleLoopStr, p, q being (Polynomial of L) st p-q =
0_. L holds p = q
proof
let L be add-associative right_zeroed right_complementable distributive non
empty doubleLoopStr, q, r be (Polynomial of L);
set PRL = Polynom-Ring L;
reconsider qc = q, rc = r as Element of PRL by POLYNOM3:def 10;
assume
A1: q-r = 0_. L;
0_. L = 0.PRL by POLYNOM3:def 10;
then qc-rc = 0.PRL by A1,Th22;
hence thesis by VECTSP_1:27;
end;
theorem Th25:
for L being Abelian add-associative right_zeroed
right_complementable distributive domRing-like non empty doubleLoopStr, p, q,
r being Polynomial of L st p <> 0_. L & p*'q = p*'r holds q = r
proof
let L be Abelian add-associative right_zeroed right_complementable
distributive domRing-like non empty doubleLoopStr, p, q, r be Polynomial of L;
assume
A1: p <> 0_. L;
assume p*'q = p*'r;
then p*'q-p*'r = 0_. L by POLYNOM3:29;
then p*'(q-r) = 0_. L by Th23;
then q-r = 0_. L by A1,Th18;
hence thesis by Th24;
end;
theorem Th26:
for L being domRing, n being Element of NAT, p being Polynomial
of L st p <> 0_. L holds p`^n <> 0_. L
proof
let L be domRing, n be Element of NAT, p be Polynomial of L;
defpred P[Nat] means p`^$1 <> 0_. L;
assume
A1: p <> 0_. L;
A2: for n being Nat st P[n] holds P[n+1]
proof
let n be Nat such that
A3: P[n];
p`^(n+1) = (p`^n) *' p by POLYNOM5:19;
hence thesis by A1,A3,Th18;
end;
(1_. L).0 = 1.L & (0_. L).0 = 0.L by FUNCOP_1:7,POLYNOM3:30;
then
A4: P[ 0 ] by POLYNOM5:15;
for n being Nat holds P[n] from NAT_1:sch 2(A4,A2);
hence thesis;
end;
theorem Th27:
for L being comRing, i, j being Nat, p being
Polynomial of L holds (p`^i) *' (p`^j) = p `^(i+j)
proof
let L be comRing, i, j being Nat, p be Polynomial of L;
defpred P[Nat] means (p`^i) *' (p`^$1) = p `^(i+$1);
A1: for j being Nat st P[j] holds P[j+1]
proof
let j be Nat such that
A2: P[j];
(p`^i) *' (p`^(j+1)) = (p`^i) *' ((p`^j) *' p) by POLYNOM5:19
.= (p`^(i+j)) *' p by A2,POLYNOM3:33
.= p`^(i+j+1) by POLYNOM5:19
.= p`^(i+(j+1));
hence thesis;
end;
(p`^i) *' (p`^0) = (p`^i) *' 1_. L by POLYNOM5:15
.= (p`^(i+(0 qua Nat))) by POLYNOM3:35;
then
A3: P[ 0 ];
for j being Nat holds P[j] from NAT_1:sch 2(A3,A1);
hence thesis;
end;
theorem Th28:
for L being non empty multLoopStr_0 holds 1_.(L) = <%1.L%>
proof
let L be non empty multLoopStr_0;
A1: dom 0_.(L) = NAT by FUNCT_2:def 1;
now
let x be object;
assume x in NAT;
then reconsider n = x as Element of NAT;
per cases;
suppose
A2: x = 0;
hence (1_.(L)).x = 1.L by A1,FUNCT_7:31
.= <%1.L%>.x by A2,ALGSEQ_1:def 5;
end;
suppose
A3: n <> 0;
then
A4: n = 1 or n > 1 by NAT_1:53;
thus (1_.(L)).x = (0_.(L)).n by A3,FUNCT_7:32
.= 0.L by FUNCOP_1:7
.= <%1.L%>.x by A4,POLYNOM5:32;
end;
end;
hence thesis by FUNCT_2:12;
end;
theorem
for L being add-associative right_zeroed right_complementable
well-unital right-distributive non empty doubleLoopStr, p being Polynomial of
L holds p*'<%1.L%> = p
proof
let L be add-associative right_zeroed right_complementable well-unital
right-distributive non empty doubleLoopStr, p being Polynomial of L;
thus p*'<%1.L%> = p*'1_.(L) by Th28
.= p by POLYNOM3:35;
end;
theorem Th30:
for L being add-associative right_zeroed right_complementable
distributive non empty doubleLoopStr, p, q being Polynomial of L st len p = 0
or len q = 0 holds len (p*'q) = 0
proof
let L be add-associative right_zeroed right_complementable distributive non
empty doubleLoopStr, p, q being Polynomial of L;
assume
A1: len p = 0 or len q = 0;
per cases by A1;
suppose
len p = 0;
then p = 0_. L by POLYNOM4:5;
then p*'q = 0_. L by POLYNOM4:2;
hence thesis by POLYNOM4:3;
end;
suppose
len q = 0;
then q = 0_. L by POLYNOM4:5;
then p*'q = 0_. L by Th17;
hence thesis by POLYNOM4:3;
end;
end;
theorem Th31:
for L being add-associative right_zeroed right_complementable
distributive non empty doubleLoopStr, p, q being Polynomial of L st p*'q is
non-zero holds p is non-zero & q is non-zero
proof
let L be add-associative right_zeroed right_complementable distributive non
empty doubleLoopStr, p, q being Polynomial of L;
assume that
A1: p*'q is non-zero and
A2: p is non non-zero or q is non non-zero;
len p = 0 or len q = 0 by A2,Th14;
then len (p*'q) = 0 by Th30;
hence thesis by A1,Th14;
end;
theorem
for L being add-associative right_zeroed right_complementable
distributive commutative associative well-unital non empty doubleLoopStr, p,
q being Polynomial of L st p.(len p -'1) * q.(len q -'1) <> 0.L holds 0 < len (
p*'q)
proof
let L be add-associative right_zeroed right_complementable distributive
commutative associative well-unital non empty doubleLoopStr, p, q being
Polynomial of L;
assume
A1: p.(len p -'1) * q.(len q -'1) <> 0.L;
now
assume len q <= 0;
then len q = 0;
then q = 0_. L by POLYNOM4:5;
then q.(len q -'1) = 0.L by FUNCOP_1:7;
hence contradiction by A1;
end;
then
A2: 0 qua Nat+1 <= len q by NAT_1:13;
now
assume len p <= 0;
then len p = 0;
then p = 0_. L by POLYNOM4:5;
then p.(len p -'1) = 0.L by FUNCOP_1:7;
hence contradiction by A1;
end;
then 0 qua Nat+1 <= len p by NAT_1:13;
then len p + len q >= 1+1 by A2,XREAL_1:7;
then len p + len q -1 >= 1+1-1 by XREAL_1:9;
hence thesis by A1,POLYNOM4:10;
end;
theorem Th33:
for L being add-associative right_zeroed right_complementable
distributive commutative associative well-unital domRing-like non empty
doubleLoopStr, p, q being Polynomial of L st 1 < len p & 1 < len q holds len p
< len (p*'q)
proof
let L be add-associative right_zeroed right_complementable distributive
commutative associative well-unital domRing-like non empty doubleLoopStr, p,
q be Polynomial of L such that
A1: 1 < len p and
A2: 1 < len q;
p.(len p -'1) <> 0.L & q.(len q -'1)<>0.L by A1,A2,Th15;
then p.(len p -'1) * q.(len q -'1)<>0.L by VECTSP_2:def 1;
then
A3: len (p*'q) = len p + len q - 1 by POLYNOM4:10;
len q - 1 > 1-1 by A2,XREAL_1:14;
then len p + (len q - 1) > 0 qua Nat+len p by XREAL_1:8;
hence thesis by A3;
end;
theorem Th34:
for L being add-associative right_zeroed right_complementable
left-distributive non empty doubleLoopStr, a, b being Element of L, p being
Polynomial of L holds (<%a, b%>*'p).0 = a*p.0 & for i being Nat holds (<%a, b%>
*'p).(i+1) = a*p.(i+1)+b*p.i
proof
let L be add-associative right_zeroed right_complementable left-distributive
non empty doubleLoopStr, a, b be Element of L, q be Polynomial of L;
set p = <%a, b%>;
consider r being FinSequence of L such that
A1: len r = 0 qua Nat+1 and
A2: p*'q.0 = Sum r and
A3: for k be Element of NAT st k in dom r holds r.k = p.(k-'1) * q.(0
qua Nat+1-'k) by POLYNOM3:def 9;
A4: 1 in dom r by A1,FINSEQ_3:25;
then reconsider r1 = r.1 as Element of L by FINSEQ_2:11;
r = <*r1*> by A1,FINSEQ_1:40;
then Sum r = r1 by RLVECT_1:44
.= p.(1-'1) * q.(0 qua Nat+1-'1) by A3,A4
.= p.0 * q.(0 qua Nat+1-'1) by XREAL_1:232
.= p.0 * q.0 by NAT_D:34;
hence (<%a, b%>*'q).0 = a*q.0 by A2,POLYNOM5:38;
let i be Nat;
consider r being FinSequence of L such that
A5: len r = (i+1)+1 and
A6: p*'q.(i+1) = Sum r and
A7: for k be Element of NAT st k in dom r holds r.k = p.(k-'1) * q.((i+1
)+1-'k) by POLYNOM3:def 9;
len r = i+2 by A5;
then
A8: 0 qua Nat+2 <= len r by XREAL_1:6;
then
A9: 2 in dom r by FINSEQ_3:25;
then
A10: r/.2 = r.2 by PARTFUN1:def 6
.= p.(1+1-'1) * q.((i+1)+1-'2) by A7,A9
.= p.1 * q.((i+1)+1-'2) by NAT_D:34
.= b * q.(i+(1+1)-'2) by POLYNOM5:38
.= b * q.i by NAT_D:34;
A11: now
let k be Element of NAT such that
A12: 2 < k and
A13: k in dom r;
consider k1 being Nat such that
A14: k = k1+1 by A12,NAT_1:6;
A15: 2 <= k1 by A12,A14,NAT_1:13;
reconsider k1 as Element of NAT by ORDINAL1:def 12;
thus r.k = p.(k-'1) * q.((i+1)+1-'k) by A7,A13
.= p.k1 * q.((i+1)+1-'k) by A14,NAT_D:34
.= (0.L) * q.((i+1)+1-'k) by A15,POLYNOM5:38
.= 0.L;
end;
1 <= len r by A8,XXREAL_0:2;
then
A16: 1 in dom r by FINSEQ_3:25;
then r/.1 = r.1 by PARTFUN1:def 6
.= p.(1-'1) * q.((i+1)+1-'1) by A7,A16
.= p.0 * q.((i+1)+1-'1) by XREAL_1:232
.= p.0 * q.(i+1) by NAT_D:34
.= a*q.(i+1) by POLYNOM5:38;
hence thesis by A6,A8,A10,A11,Th2;
end;
theorem Th35:
for L being add-associative right_zeroed right_complementable
distributive well-unital commutative associative non degenerated non empty
doubleLoopStr, r being Element of L, q being non-zero Polynomial of L holds
len (<%r, 1.L%>*'q) = len q + 1
proof
let L be add-associative right_zeroed right_complementable distributive
well-unital commutative associative non degenerated non empty doubleLoopStr,
r be Element of L, q being non-zero Polynomial of L;
set p = <%r, 1.L%>;
A1: p.(len p -'1) * q.(len q -'1) = p.(1+1-'1) * q.(len q -'1) by POLYNOM5:40
.= p.(1) * q.(len q -'1) by NAT_D:34
.= 1.L * q.(len q -'1) by POLYNOM5:38
.= q.(len q -'1);
len <%r, 1.L%> = 2 & len q > 0 by Th14,POLYNOM5:40;
hence len (<%r, 1.L%>*'q) = len q +(1+1)-1 by A1,Th15,POLYNOM4:10
.= len q +1;
end;
theorem Th36:
for L being non degenerated comRing, x being Element of L, i
being Nat holds len (<%x, 1.L%>`^i) = i+1
proof
let L be non degenerated comRing, x be Element of L;
defpred P[Nat] means len (<%x, 1.L%>`^$1) = $1+1;
set r = <%x, 1.L%>;
A1: for i being Nat st P[i] holds P[i+1]
proof
let i be Nat such that
A2: P[i];
reconsider ri = r`^i as non-zero Polynomial of L by A2,Th14;
thus len (r`^(i+1)) = len ((r`^1)*'ri) by Th27
.= len (r*'ri) by POLYNOM5:16
.= i+1+1 by A2,Th35;
end;
r`^0 = 1_. L by POLYNOM5:15;
then
A3: P[ 0 ] by POLYNOM4:4;
thus for i being Nat holds P[i] from NAT_1:sch 2(A3,A1);
end;
registration
let L be non degenerated comRing, x be Element of L, n be Nat;
cluster <%x, 1.L%>`^n -> non-zero;
correctness
proof
len (<%x, 1.L%>`^n) = n+1 by Th36;
hence thesis by Th14;
end;
end;
theorem Th37:
for L being non degenerated comRing, x being Element of L, q
being non-zero (Polynomial of L), i being Nat holds len ((<%x, 1.L%>
`^i)*'q) = i + len q
proof
let L being non degenerated comRing, x being Element of L, q being non-zero
Polynomial of L;
set r = <%x, 1.L%>;
defpred P[Nat] means len ((r`^$1)*'q) = $1 + len q;
A1: for i being Nat st P[i] holds P[i+1]
proof
let i be Nat such that
A2: P[i];
len q > 0 by Th14;
then
A3: (r`^i)*'q is non-zero by A2,Th14;
thus len ((r`^(i+1))*'q) = len ((r`^1)*'(r`^i)*'q) by Th27
.= len (r*'(r`^i)*'q) by POLYNOM5:16
.= len (r*'((r`^i)*'q)) by POLYNOM3:33
.= (i+len q)+1 by A2,A3,Th35
.= (i+1)+len q;
end;
len ((r`^0)*'q) = len ((1_. L)*'q) by POLYNOM5:15
.= 0 qua Nat+ len q by POLYNOM3:35;
then
A4: P[ 0 ];
thus for i being Nat holds P[i] from NAT_1:sch 2(A4,A1);
end;
theorem Th38:
for L being add-associative right_zeroed right_complementable
distributive well-unital commutative associative non degenerated non empty
doubleLoopStr, r being Element of L, p, q being Polynomial of L st p = <%r, 1.
L%>*'q & p.(len p -'1) = 1.L holds q.(len q -'1) = 1.L
proof
let L be add-associative right_zeroed right_complementable distributive
well-unital commutative associative non degenerated non empty doubleLoopStr,
x be Element of L, p, q be Polynomial of L such that
A1: p = <%x, 1.L%>*'q and
A2: p.(len p -'1) = 1.L;
set lp1 = len p -'1;
A3: now
assume q = 0_. L;
then p = 0_. L by A1,POLYNOM3:34;
hence contradiction by A2,FUNCOP_1:7;
end;
then q is non-zero;
then len p = len q + 1 by A1,Th35;
then
A4: lp1 = len q by NAT_D:34;
then consider lp2 being Nat such that
A5: lp1 = lp2+1 by A3,NAT_1:6,POLYNOM4:5;
reconsider lp2 as Element of NAT by ORDINAL1:def 12;
A6: q.lp1 = 0.L by A4,ALGSEQ_1:8;
(<%x, 1.L%>*'q).lp1 = x*q.(lp1)+(1.L)*q.lp2 by A5,Th34
.= 0.L +(1.L)*q.lp2 by A6
.= (1.L)*q.lp2 by RLVECT_1:4
.= q.lp2;
hence thesis by A1,A2,A4,A5,NAT_D:34;
end;
begin :: Little Bezout theorem
definition
let L be non empty ZeroStr, p be Polynomial of L;
let n be Nat;
func poly_shift(p,n) -> Polynomial of L means
:Def5:
for i being Nat holds it.i = p.(n + i);
existence
proof
deffunc F(Nat) = p.(n+$1);
consider ps being AlgSequence of L such that
A1: len ps <= len p and
A2: for k being Nat st k < len p holds ps.k = F(k) from ALGSEQ_1:sch 1;
take ps;
let i be Nat;
per cases;
suppose
i < len p;
hence thesis by A2;
end;
suppose
A3: i >= len p;
hence ps.i = 0.L by A1,ALGSEQ_1:8,XXREAL_0:2
.= p.(n + i) by A3,ALGSEQ_1:8,NAT_1:12;
end;
end;
uniqueness
proof
let it1, it2 be Polynomial of L such that
A4: for i being Nat holds it1.i = p.(n + i) and
A5: for i being Nat holds it2.i = p.(n + i);
now
let x be object;
assume x in NAT;
then reconsider i = x as Element of NAT;
thus it1.x = p.(n+i) by A4
.= it2.x by A5;
end;
hence it1 = it2 by FUNCT_2:12;
end;
end;
theorem Th39:
for L being non empty ZeroStr,p being Polynomial of L holds
poly_shift(p,0) = p
proof
let L be non empty ZeroStr, p be Polynomial of L;
set ps = poly_shift(p,0);
now
let x be object;
assume x in NAT;
then reconsider i = x as Element of NAT;
thus ps.x = p.(0 qua Nat+i) by Def5
.= p.x;
end;
hence thesis by FUNCT_2:12;
end;
theorem Th40:
for L being non empty ZeroStr, n being Element of NAT, p being
Polynomial of L st n >= len p holds poly_shift(p,n) = 0_. L
proof
let L be non empty ZeroStr, n be Element of NAT, p be Polynomial of L;
set ps = poly_shift(p,n);
assume
A1: n >= len p;
A2: now
let z be object;
assume z in dom ps;
then reconsider i = z as Element of NAT;
thus ps.z = p.(n+i) by Def5
.= 0.L by A1,ALGSEQ_1:8,NAT_1:12;
end;
dom ps = NAT by FUNCT_2:def 1;
hence thesis by A2,FUNCOP_1:11;
end;
theorem Th41:
for L being non degenerated non empty multLoopStr_0, n being
Element of NAT, p being Polynomial of L st n <= len p holds len poly_shift(p,n)
+ n = len p
proof
let L be non degenerated non empty multLoopStr_0, n be Element of NAT, p
be Polynomial of L such that
A1: n <= len p;
set ps = poly_shift(p,n), lpn = len p - n;
n-n <= lpn by A1,XREAL_1:9;
then reconsider lpn as Element of NAT by INT_1:3;
A2: now
let m be Nat such that
A3: m is_at_least_length_of ps and
A4: lpn > m;
lpn >= m+1 by A4,NAT_1:13;
then
A5: lpn -1 >= m +1-1 by XREAL_1:9;
then reconsider lpn1 = lpn -1 as Element of NAT by INT_1:3;
(n+lpn1)+1 = len p;
then
A6: p.(n+lpn1) <> 0.L by ALGSEQ_1:10;
ps.lpn1 = p.(n+lpn1) by Def5;
hence contradiction by A3,A5,A6,ALGSEQ_1:def 2;
end;
now
let i be Nat;
assume i >= lpn;
then
A7: i+n >= len p by XREAL_1:20;
thus ps.i = p.(n+i) by Def5
.= 0.L by A7,ALGSEQ_1:8;
end;
then lpn is_at_least_length_of ps by ALGSEQ_1:def 2;
hence len poly_shift(p,n) + n = lpn + n by A2,ALGSEQ_1:def 3
.= len p;
end;
theorem Th42:
for L being non degenerated comRing, x being Element of L, n
being Element of NAT, p being Polynomial of L st n < len p holds eval(
poly_shift(p,n),x) = x*eval(poly_shift(p,n+1),x) + p.n
proof
let L be non degenerated comRing, x being Element of L, n be Element of NAT,
p being Polynomial of L such that
A1: n < len p;
set ps = poly_shift(p,n), ps1 = poly_shift(p,n+1);
consider f be FinSequence of L such that
A2: eval(ps,x) = Sum f and
A3: len f = len ps and
A4: for k be Element of NAT st k in dom f holds f.k = ps.(k-'1) * (power
L).(x,k-'1) by POLYNOM4:def 2;
consider f1 be FinSequence of L such that
A5: eval(ps1,x) = Sum f1 and
A6: len f1 = len ps1 and
A7: for k be Element of NAT st k in dom f1 holds f1.k = ps1.(k-'1) * (
power L).(x,k-'1) by POLYNOM4:def 2;
rng f1 c= the carrier of L & dom (x multfield) = the carrier of L by
FUNCT_2:def 1;
then
A8: x*f1 = (x multfield)*f1 & dom ((x multfield)*f1) = dom f1 by FVSUM_1:def 6
,RELAT_1:27;
A9: 1_L = 1.L;
now
A10: n+1 <= len p by A1,NAT_1:13;
A11: len ps1 +1+n = len ps1 + (n+1) .= len p by A10,Th41
.= len ps + n by A1,Th41;
thus len f = len f;
A12: len <*p.n*> = 1 by FINSEQ_1:40;
A13: len ((x*f1)) = len f1 by A8,FINSEQ_3:29;
hence len (<*p.n*>^(x*f1)) = len f by A3,A6,A11,A12,FINSEQ_1:22;
let j be Nat such that
A14: j in dom f;
A15: 1 <= j by A14,FINSEQ_3:25;
A16: j <= len f by A14,FINSEQ_3:25;
per cases by A15,XXREAL_0:1;
suppose
A17: j = 1;
A18: 1 in dom <*p.n*> by A12,FINSEQ_3:25;
thus f.j = ps.(1-'1) * (power L).(x,1-'1) by A4,A14,A17
.= ps.0 * (power L).(x,1-'1) by XREAL_1:232
.= ps.0 * (power L).(x,0) by XREAL_1:232
.= ps.0 * 1.L by A9,GROUP_1:def 7
.= ps.0
.= p.(n+(0 qua Nat)) by Def5
.= <*p.n*>.1
.= (<*p.n*>^(x*f1)).j by A17,A18,FINSEQ_1:def 7;
end;
suppose
A19: 1 < j;
1-1 <= j-1 by A15,XREAL_1:9;
then reconsider j1 = j-1 as Element of NAT by INT_1:3;
A20: 1+1 <= j by A19,NAT_1:13;
then
A21: 1+1-1 <= j-1 by XREAL_1:9;
then ex j2 being Nat st j1 = j2+1 by NAT_1:6;
then
A22: j1-'1+1 = j1 by NAT_D:34;
j = j1+1;
then
A23: j1 = j-'1 by NAT_D:34;
j-1 <= len f1 + 1-1 by A3,A6,A11,A16,XREAL_1:9;
then
A24: j1 in dom f1 by A21,FINSEQ_3:25;
then reconsider f1j = f1.j1 as Element of L by FINSEQ_2:11;
thus f.j = ps.(j-'1) * (power L).(x,j-'1) by A4,A14
.= p.(n+j1) * (power L).(x,j1) by A23,Def5
.= p.((n+1)+(j1-'1)) * (((power L).(x,j1-'1)) * x) by A22,GROUP_1:def 7
.= x*(p.((n+1)+(j1-'1)) * (power L).(x,j1-'1)) by GROUP_1:def 3
.= x*(ps1.(j1-'1) * (power L).(x,j1-'1)) by Def5
.= x*f1j by A7,A24
.= (x*f1).j1 by A8,A24,FVSUM_1:50
.= (<*p.n*>^(x*f1)).j by A3,A6,A11,A12,A13,A16,A20,FINSEQ_1:23;
end;
end;
then x*(Sum f1) = Sum (x*f1) & f = <*p.n*>^(x*f1) by FINSEQ_2:9,FVSUM_1:73;
hence thesis by A2,A5,FVSUM_1:72;
end;
theorem Th43:
for L being non degenerated comRing, p being Polynomial of L st
len p = 1 holds Roots p = {}
proof
let L be non degenerated comRing, p be Polynomial of L;
assume len p = 1;
then
A1: p =<%p.0%> & p.0 <> 0.L by Th16;
assume Roots p <> {};
then consider x being object such that
A2: x in Roots p by XBOOLE_0:def 1;
reconsider x as Element of L by A2;
x is_a_root_of p by A2,POLYNOM5:def 10;
then eval(p,x) = 0.L;
hence contradiction by A1,POLYNOM5:37;
end;
definition
let L be non degenerated comRing, r be Element of L, p be Polynomial of L
such that
A1: r is_a_root_of p;
func poly_quotient(p,r) -> Polynomial of L means
:Def6:
len it + 1 = len p &
for i being Nat holds it.i = eval(poly_shift(p, i+1),r) if len p > 0 otherwise
it = 0_. L;
existence
proof
hereby
r in Roots p by A1,POLYNOM5:def 10;
then
A2: len p <> 1 by Th43;
deffunc F(Nat) = eval(poly_shift(p, $1+1),r);
set lq = len p -'1;
consider q being sequence of L such that
A3: for k being Element of NAT holds q.k = F(k) from FUNCT_2:sch 4;
reconsider q as sequence of L;
assume
A4: len p > 0;
then consider p1 being Nat such that
A5: len p = p1+1 by NAT_1:6;
A6: lq = p1 by A5,NAT_D:34;
then
A7: lq < len p by A5,NAT_1:13;
len p >= 0 qua Nat+1 by A4,NAT_1:13;
then consider lq1 being Nat such that
A8: lq = lq1 + 1 by A5,A6,A2,NAT_1:6;
A9: now
let i be Nat;
assume i >= lq;
then i >= p1 by A5,NAT_D:34;
then
A10: i+1 >= len p by A5,XREAL_1:6;
i in NAT by ORDINAL1:def 12;
hence q.i = eval(poly_shift(p, i+1),r) by A3
.= eval(0_.L,r) by A10,Th40
.= 0.L by POLYNOM4:17;
end;
reconsider lq1 as Element of NAT by ORDINAL1:def 12;
q.lq1 = eval(poly_shift(p, lq1+1),r) by A3
.= r*eval(poly_shift(p, len p),r) + p.lq by A5,A6,A8,A7,Th42
.= r*eval(0_. L,r) + p.lq by Th40
.= r*0.L + p.lq by POLYNOM4:17
.= 0.L + p.lq
.= p.lq by RLVECT_1:4;
then
A11: q.lq1 <> 0.L by A5,A6,ALGSEQ_1:10;
reconsider q as AlgSequence of L by A9,ALGSEQ_1:def 1;
A12: lq1 = lq -'1 by A8,NAT_D:34;
A13: now
let m be Nat;
assume
A14: m is_at_least_length_of q;
assume
A15: lq > m;
then consider lq1 being Nat such that
A16: lq = lq1 + 1 by NAT_1:6;
lq1 >= m by A15,A16,NAT_1:13;
then lq -'1 >= m by A16,NAT_D:34;
hence contradiction by A12,A11,A14,ALGSEQ_1:def 2;
end;
take q;
lq is_at_least_length_of q by A9,ALGSEQ_1:def 2;
hence len q + 1 =p1+1-'1+1 by A5,A13,ALGSEQ_1:def 3
.=len p by A5,NAT_D:34;
let k be Nat;
k in NAT by ORDINAL1:def 12;
hence q.k = F(k) by A3;
end;
thus thesis;
end;
uniqueness
proof
let it1, it2 be Polynomial of L;
hereby
assume len p > 0;
assume that
A17: len it1 + 1 = len p and
A18: for i being Nat holds it1.i = eval(poly_shift(p, i+1),r) and
A19: len it2 + 1 = len p and
A20: for i being Nat holds it2.i = eval(poly_shift(p, i+1),r);
now
let k be Nat such that
k < len it1;
thus it1.k = eval(poly_shift(p, k+1),r) by A18
.= it2.k by A20;
end;
hence it1 = it2 by A17,A19,ALGSEQ_1:12;
end;
thus thesis;
end;
consistency;
end;
theorem Th44:
for L being non degenerated comRing, r being Element of L, p
being non-zero Polynomial of L st r is_a_root_of p holds len poly_quotient(p,r)
> 0
proof
let L be non degenerated comRing, r be Element of L, p be non-zero
Polynomial of L such that
A1: r is_a_root_of p;
assume len poly_quotient(p,r) <= 0;
then
A2: len poly_quotient(p,r) = 0;
len p > 0 by Th14;
then len poly_quotient(p,r) + 1 = len p by A1,Def6;
then Roots p = {} by A2,Th43;
hence contradiction by A1,POLYNOM5:def 10;
end;
theorem Th45:
for L being add-associative right_zeroed right_complementable
left-distributive well-unital non empty doubleLoopStr, x being Element of L
holds Roots <%-x, 1.L%> = {x}
proof
let L be add-associative right_zeroed right_complementable left-distributive
well-unital non empty doubleLoopStr, x be Element of L;
now
let a be object;
hereby
assume
A1: a in Roots <%-x, 1.L%>;
then reconsider b = a as Element of L;
b is_a_root_of <%-x, 1.L%> by A1,POLYNOM5:def 10;
then 0.L = eval(<%-x, 1.L%>,b)
.= -x + b by POLYNOM5:47;
then -x = -b by RLVECT_1:6;
hence x = a by RLVECT_1:18;
end;
eval(<%-x, 1.L%>,x) = -x + x by POLYNOM5:47
.= 0.L by RLVECT_1:5;
then
A2: x is_a_root_of <%-x, 1.L%>;
assume a = x;
hence a in Roots <%-x, 1.L%> by A2,POLYNOM5:def 10;
end;
hence thesis by TARSKI:def 1;
end;
theorem Th46:
for L being non trivial comRing, x being Element of L, p, q
being Polynomial of L st p = <%-x,1.L%>*'q holds x is_a_root_of p
proof
let L be non trivial comRing, x be Element of L, p, q be Polynomial of L
such that
A1: p = <%-x,1.L%>*'q;
A2: eval(<%-x,1.L%>,x) = (-x)+x by POLYNOM5:47
.= 0.L by RLVECT_1:5;
thus eval(p,x) = eval(<%-x,1.L%>,x) * eval(q,x) by A1,POLYNOM4:24
.= 0.L by A2;
end;
::$N Little Bezout Theorem (Factor Theorem)
::$L https://en.wikipedia.org/wiki/Polynomial_remainder_theorem Polynomial remainder theorem
theorem Th47:
for L being non degenerated comRing, r being Element of L,
p being Polynomial of L st r is_a_root_of p holds
p = <%-r,1.L%>*'poly_quotient(p,r)
proof
let L be non degenerated comRing, x be Element of L, p be Polynomial of L;
assume
A1: x is_a_root_of p;
set r = <%-x,1.L%>, pq = poly_quotient(p,x);
per cases;
suppose
A2: len p > 0;
r.(len r -'1) = r.(1+1-'1) by POLYNOM5:40
.= r.1 by NAT_D:34
.= 1.L by POLYNOM5:38;
then
A3: r.(len r -'1) * pq.(len pq -'1) = pq.(len pq -'1);
p is non-zero by A2,Th14;
then
A4: len pq > 0 by A1,Th44;
now
len (r *' pq) = len r + len pq - 1 by A4,A3,Th15,POLYNOM4:10
.= len pq +(1+1)-1 by POLYNOM5:40
.= len pq +1
.= len p by A1,A2,Def6;
hence len p = len (r *' pq);
defpred P[Nat] means p.$1 = (r*'pq).$1;
let k be Nat;
assume k < len p;
A5: 0.L = eval(p,x) by A1
.= eval(poly_shift(p,0),x) by Th39
.= x*eval(poly_shift(p,0 qua Nat+1),x) + p.0 by A2,Th42;
A6: (-x)*eval(poly_shift(p, 0 qua Nat+1),x) = (-x)*eval(poly_shift(p, 0
qua Nat+1),x) + 0.L by RLVECT_1:def 4
.= (-x)*eval(poly_shift(p, 0 qua Nat+1),x) + x*eval(poly_shift(p,1),
x) + p.0 by A5,RLVECT_1:def 3
.= -x*eval(poly_shift(p, 0 qua Nat+1),x) + x*eval(poly_shift(p,1),x)
+ p.0 by VECTSP_1:9
.= 0.L +p.0 by RLVECT_1:5
.= p.0 by RLVECT_1:4;
A7: for k being Nat st P[k] holds P[k+1]
proof
let k be Nat;
assume P[k];
A8: pq.(k+1) = eval(poly_shift(p, k+1+1),x) by A1,A2,Def6;
A9: pq.k = eval(poly_shift(p, k+1),x) by A1,A2,Def6;
per cases;
suppose
A10: k+1 >= len p;
then
A11: pq.(k+1) = eval(0_.L,x) by A8,Th40,NAT_1:12
.= 0.L by POLYNOM4:17;
A12: pq.k = eval(0_.L,x) by A9,A10,Th40
.= 0.L by POLYNOM4:17;
(r*'pq).(k+1) = (-x)*pq.(k+1)+(1.L)*pq.k by Th34
.= 0.L + (1.L)*pq.k by A11
.= 0.L + 0.L by A12
.= 0.L by RLVECT_1:4;
hence thesis by A10,ALGSEQ_1:8;
end;
suppose
k+1 < len p;
then pq.k = x*eval(poly_shift(p, k+1+1),x) + p.(k+1) by A9,Th42;
then
A13: -x*pq.(k+1)+pq.k = -x*pq.(k+1)+x*eval(poly_shift(p, k+1+1),x)+p
.(k+1) by RLVECT_1:def 3
.= 0.L + p.(k+1) by A8,RLVECT_1:5;
(r*'pq).(k+1) = (-x)*pq.(k+1)+(1.L)*pq.k by Th34
.= (-x)*pq.(k+1)+pq.k
.= -x*pq.(k+1)+pq.k by VECTSP_1:9;
hence thesis by A13,RLVECT_1:4;
end;
end;
(r*'pq).0 = (-x)*pq.0 by Th34
.= (-x)*eval(poly_shift(p, 0 qua Nat+1),x) by A1,A2,Def6;
then
A14: P[ 0 ] by A6;
for k being Nat holds P[k] from NAT_1:sch 2(A14,A7);
hence p.k = (r*'pq).k;
end;
hence thesis by ALGSEQ_1:12;
end;
suppose
len p = 0;
then pq = 0_. L & p = 0_. L by A1,Def6,POLYNOM4:5;
hence thesis by POLYNOM3:34;
end;
end;
theorem :: Factor theorem (Bezout)
for L being non degenerated comRing, r being Element of L, p, q being
Polynomial of L st p = <%-r,1.L%>*'q holds r is_a_root_of p
proof
let L be non degenerated comRing, r be Element of L, p, q be Polynomial of L;
assume p = <%-r,1.L%>*'q;
then eval(p,r) = eval(<%-r,1.L%>,r) * eval(q,r) by POLYNOM4:24
.= (-r+r) * eval(q,r) by POLYNOM5:47
.= 0.L * eval(q,r) by RLVECT_1:def 10
.= 0.L;
hence thesis;
end;
Lm1: now
let L be domRing, p be non-zero Polynomial of L;
defpred P[Nat] means for p being Polynomial of L st len p = $1 holds Roots p
is finite & ex n being Element of NAT st n = card Roots p & n < len p;
p <> 0_. L by Def4;
then len p <> 0 by POLYNOM4:5;
then
A1: len p >= 0 qua Nat+1 by NAT_1:13;
A2: for n being Nat st n>=1 & P[n] holds P[n+1]
proof
let n be Nat such that
n >= 1 and
A3: P[n];
let p be Polynomial of L;
assume
A4: len p = n+1;
per cases;
suppose
p is with_roots;
then consider x being Element of L such that
A5: x is_a_root_of p;
set r = <%-x,1.L%>, pq = poly_quotient(p,x);
A6: p = <%-x,1.L%>*'poly_quotient(p,x) by A5,Th47;
then
A7: Roots p = (Roots r)\/Roots pq by Th20;
A8: Roots r = {x} by Th45;
then reconsider Rr = Roots r as finite set;
A9: len pq + 1 = len p by A4,A5,Def6;
then consider k being Element of NAT such that
A10: k = card Roots pq and
A11: k < len pq by A3,A4;
reconsider Rpq = Roots pq as finite set by A3,A4,A9;
reconsider Rp = Rpq \/ Rr as finite set;
card Rr = 1 by A8,CARD_1:30;
then
A12: card Rp <= k + 1 by A10,CARD_2:43;
Roots pq is finite by A3,A4,A9;
hence Roots p is finite by A8,A7;
take m = card Rp;
thus m = card Roots p by A6,Th20;
k+1 < n+1 by A4,A9,A11,XREAL_1:8;
hence thesis by A4,A12,XXREAL_0:2;
end;
suppose
A13: not p is with_roots;
A14: now
assume Roots p <> {};
then consider x being object such that
A15: x in Roots p by XBOOLE_0:def 1;
reconsider x as Element of L by A15;
x is_a_root_of p by A15,POLYNOM5:def 10;
hence contradiction by A13;
end;
hence Roots p is finite;
take 0;
thus 0 = card Roots p by A14;
thus thesis by A4;
end;
end;
A16: P[1]
proof
let p be Polynomial of L;
assume
A17: len p = 1;
hence Roots p is finite by Th43;
take 0;
thus 0 = card Roots p by A17,Th43,CARD_1:27;
thus thesis by A17;
end;
for n being Nat st n >= 1 holds P[n] from NAT_1:sch 8(A16,A2);
hence
Roots p is finite & ex n being Element of NAT st n = card Roots p & n <
len p by A1;
end;
begin :: Polynomials defined by roots
registration
let L be domRing, p be non-zero Polynomial of L;
cluster Roots p -> finite;
correctness by Lm1;
end;
definition
let L be non degenerated comRing, x be Element of L, p be non-zero (
Polynomial of L);
func multiplicity(p,x) -> Element of NAT means
:Def7:
ex F being finite non
empty Subset of NAT st F = {k where k is Element of NAT : ex q being Polynomial
of L st p = (<%-x, 1.L%>`^k) *' q} & it = max F;
existence
proof
set r = <%-x, 1.L%>;
defpred P[Element of NAT] means ex q being Polynomial of L st p = (r`^$1)
*' q;
set F = {k where k is Element of NAT : P[k]};
A1: F c= NAT from FRAENKEL:sch 10;
p = (1_. L) *' p by POLYNOM3:35
.= (r`^0) *' p by POLYNOM5:15;
then
A2: 0 in F;
A3: len p > 0 by Th14;
F c= len p
proof
let a be object;
assume a in F;
then consider k being Element of NAT such that
A4: a = k and
A5: P[k];
consider q being Polynomial of L such that
A6: p = (r`^k) *' q by A5;
A7: now
assume len q = 0;
then q = 0_. L by POLYNOM4:5;
then p = 0_. L by A6,POLYNOM4:2;
hence contradiction by A3,POLYNOM4:3;
end;
then reconsider q as non-zero Polynomial of L by Th14;
now
assume k >= len p;
then k+len q > len p + (0 qua Nat) by A7,XREAL_1:8;
hence contradiction by A6,Th37;
end;
then k in {i where i is Nat : i < len p};
hence thesis by A4,AXIOMS:4;
end;
then reconsider F as finite non empty Subset of NAT by A2,A1;
reconsider FF = F as finite non empty natural-membered set;
reconsider m = max FF as Element of NAT by ORDINAL1:def 12;
take m;
thus thesis;
end;
uniqueness;
end;
theorem Th49:
for L being non degenerated comRing, p being non-zero (
Polynomial of L), x being Element of L holds x is_a_root_of p iff multiplicity(
p,x) >= 1
proof
let L be non degenerated comRing, p being non-zero (Polynomial of L), x
being Element of L;
set r = <%-x, 1.L%>;
set m = multiplicity(p,x);
consider F being finite non empty Subset of NAT such that
A1: F = {k where k is Element of NAT : ex q being Polynomial of L st p =
(r`^k) *' q} and
A2: m = max F by Def7;
m in F by A2,XXREAL_2:def 8;
then consider k being Element of NAT such that
A3: m = k and
A4: ex q being Polynomial of L st p = (r`^k) *' q by A1;
hereby
assume x is_a_root_of p;
then
A5: p = r*'poly_quotient(p,x) by Th47;
r`^1 = r by POLYNOM5:16;
then 1 in F by A1,A5;
hence multiplicity(p,x) >= 1 by A2,XXREAL_2:def 8;
end;
consider q being Polynomial of L such that
A6: p = (r`^k) *' q by A4;
assume multiplicity(p,x) >= 1;
then consider k1 being Nat such that
A7: k = k1+1 by A3,NAT_1:6;
reconsider k1 as Element of NAT by ORDINAL1:def 12;
p = r *' (r`^k1) *' q by A6,A7,POLYNOM5:19
.= r *' ((r`^k1) *' q) by POLYNOM3:33;
hence thesis by Th46;
end;
theorem Th50:
for L being non degenerated comRing, x being Element of L holds
multiplicity(<%-x, 1.L%>,x) = 1
proof
let L be non degenerated comRing, x be Element of L;
set r = <%-x, 1.L%>;
set j = multiplicity(r,x);
consider F being finite non empty Subset of NAT such that
A1: F = {k where k is Element of NAT : ex q being Polynomial of L st r =
(r`^k) *' q} and
A2: multiplicity(r,x) = max F by Def7;
j in F by A2,XXREAL_2:def 8;
then consider k being Element of NAT such that
A3: k = j and
A4: ex q being Polynomial of L st r = (r`^k) *' q by A1;
consider q being Polynomial of L such that
A5: r = (r`^k) *' q by A4;
A6: len r = 2 by POLYNOM5:40;
A7: now
assume len q = 0;
then q = 0_. L by POLYNOM4:5;
then r = 0_. L by A5,POLYNOM4:2;
hence contradiction by A6,POLYNOM4:3;
end;
then
A8: q is non-zero by Th14;
A9: now
assume k > 1;
then k >= 1+1 by NAT_1:13;
then k+len q > 2+(0 qua Nat) by A7,XREAL_1:8;
hence contradiction by A6,A5,A8,Th37;
end;
r = (r`^1) by POLYNOM5:16;
then r = (r`^1) *' 1_. L by POLYNOM3:35;
then 1 in F by A1;
then multiplicity(r,x) >= 1 by A2,XXREAL_2:def 8;
hence thesis by A3,A9,XXREAL_0:1;
end;
definition
let L be domRing, p be non-zero Polynomial of L;
func BRoots(p) -> bag of the carrier of L means
:Def8:
support it = Roots p
& for x being Element of L holds it.x = multiplicity(p,x);
existence
proof
deffunc F(Element of L) = multiplicity(p,$1);
consider b being Function of the carrier of L, NAT such that
A1: for x being Element of L holds b.x = F(x) from FUNCT_2:sch 4;
dom b = the carrier of L by FUNCT_2:def 1;
then
A2: support b c= the carrier of L by PRE_POLY:37;
A3: now
let x be object;
hereby
assume
A4: x in support b;
then reconsider xx = x as Element of L by A2;
b.x <> 0 by A4,PRE_POLY:def 7;
then
A5: b.xx >= 0 qua Nat+1 by NAT_1:13;
b.x = F(xx) by A1;
then xx is_a_root_of p by A5,Th49;
hence x in Roots p by POLYNOM5:def 10;
end;
assume
A6: x in Roots p;
then reconsider xx = x as Element of L;
xx is_a_root_of p by A6,POLYNOM5:def 10;
then multiplicity(p,xx) >= 1 by Th49;
then b.xx >= 1 by A1;
hence x in support b by PRE_POLY:def 7;
end;
then support b = Roots p by TARSKI:2;
then reconsider b as bag of the carrier of L by PRE_POLY:def 8;
take b;
thus thesis by A1,A3,TARSKI:2;
end;
uniqueness
proof
let it1, it2 be bag of the carrier of L such that
support it1 = Roots p and
A7: for x being Element of L holds it1.x = multiplicity(p,x) and
support it2 = Roots p and
A8: for x being Element of L holds it2.x = multiplicity(p,x);
now
let x be object;
assume x in the carrier of L;
then reconsider xx = x as Element of L;
thus it1.x = multiplicity(p,xx) by A7
.= it2.x by A8;
end;
hence it1 = it2 by PBOOLE:3;
end;
end;
theorem Th51:
for L being domRing, x being Element of L holds BRoots <%-x, 1.L
%> = ({x}, 1)-bag
proof
let L be domRing, x be Element of L;
set r = <%-x, 1.L%>;
Roots r = {x} by Th45;
then
A1: support BRoots r = {x} by Def8;
A2: x in {x} by TARSKI:def 1;
now
let i be object;
assume i in the carrier of L;
then reconsider i1 = i as Element of L;
per cases;
suppose
A3: i = x;
thus (BRoots r).i = multiplicity(r,i1) by Def8
.= 1 by A3,Th50
.= (({x}, 1)-bag).i by A2,A3,Th4;
end;
suppose
i <> x;
then
A4: not i in {x} by TARSKI:def 1;
hence (BRoots r).i = 0 by A1,PRE_POLY:def 7
.= (({x}, 1)-bag).i by A4,Th3;
end;
end;
hence thesis by PBOOLE:3;
end;
theorem Th52:
for L being domRing, x be Element of L, p, q being non-zero
Polynomial of L holds multiplicity(p*'q,x) = multiplicity(p,x) + multiplicity(q
,x)
proof
let L be domRing,x be Element of L, p, q being non-zero Polynomial of L;
set r = <%-x, 1.L%>;
consider F being finite non empty Subset of NAT such that
A1: F = {k where k is Element of NAT : ex pqq being Polynomial of L st p
*'q = (r`^k) *' pqq} and
A2: multiplicity(p*'q,x) = max F by Def7;
consider f being finite non empty Subset of NAT such that
A3: f = {k where k is Element of NAT : ex pq being Polynomial of L st p
= (r`^k) *' pq} and
A4: multiplicity(p,x) = max f by Def7;
max f in f by XXREAL_2:def 8;
then consider i being Element of NAT such that
A5: i = max f and
A6: ex pq being Polynomial of L st p = (r`^i) *' pq by A3;
consider pq being Polynomial of L such that
A7: p = (r`^i) *' pq by A6;
consider g being finite non empty Subset of NAT such that
A8: g = {k where k is Element of NAT : ex qq being Polynomial of L st q
= (r`^k) *' qq} and
A9: multiplicity(q,x) = max g by Def7;
max F in F by XXREAL_2:def 8;
then consider k being Element of NAT such that
A10: k = max F and
A11: ex pqq being Polynomial of L st p*'q = (r`^k) *' pqq by A1;
consider pqq being Polynomial of L such that
A12: p*'q = (r`^k) *' pqq by A11;
max g in g by XXREAL_2:def 8;
then consider j being Element of NAT such that
A13: j = max g and
A14: ex qq being Polynomial of L st q = (r`^j) *' qq by A8;
consider qq being Polynomial of L such that
A15: q = (r`^j) *' qq by A14;
A16: p*'q = (r`^i) *' pq *' (r`^j) *' qq by A7,A15,POLYNOM3:33
.= (r`^i) *' (r`^j) *' pq *' qq by POLYNOM3:33
.= (r`^(i+j)) *' pq *' qq by Th27
.= (r`^(i+j)) *' (pq *' qq) by POLYNOM3:33;
A17: now
assume i+j < k;
then 0 qua Nat+(i+j) < k;
then
A18: 0 < k-(i+j) by XREAL_1:20;
then reconsider kij = k-(i+j) as Element of NAT by INT_1:3;
consider kk being Nat such that
A19: kij = kk+1 by A18,NAT_1:6;
reconsider kk as Element of NAT by ORDINAL1:def 12;
(r`^kij) = (r`^1) *' (r`^kk) by A19,Th27
.= r *' (r`^kk) by POLYNOM5:16;
then
A20: (r`^kij) *' pqq = r *' ((r`^kk) *' pqq) by POLYNOM3:33;
(0_. L).1 = 0.L & r.1 = 1.L by FUNCOP_1:7,POLYNOM5:38;
then
A21: r`^(i+j) <> 0_. L by Th26;
k = kij + (i+j);
then p*'q = ((r`^(i+j)) *' (r`^kij)) *' pqq by A12,Th27
.= (r`^(i+j)) *' ((r`^kij) *' pqq) by POLYNOM3:33;
then x is_a_root_of (pq *' qq) by A16,A21,A20,Th25,Th46;
then x in Roots (pq *' qq) by POLYNOM5:def 10;
then
A22: x in (Roots pq \/ Roots qq) by Th20;
per cases by A22,XBOOLE_0:def 3;
suppose
x in Roots(pq);
then x is_a_root_of pq by POLYNOM5:def 10;
then pq = r *' poly_quotient(pq,x) by Th47;
then p = (r`^i) *' r *' poly_quotient(pq,x) by A7,POLYNOM3:33
.= (r`^i) *' (r`^1) *' poly_quotient(pq,x) by POLYNOM5:16
.= (r`^(i+1)) *' poly_quotient(pq,x) by Th27;
then i+1 in f by A3;
then i+1 <= i by A5,XXREAL_2:def 8;
hence contradiction by NAT_1:13;
end;
suppose
x in Roots(qq);
then x is_a_root_of qq by POLYNOM5:def 10;
then qq = r *' poly_quotient(qq,x) by Th47;
then q = (r`^j) *' r *' poly_quotient(qq,x) by A15,POLYNOM3:33
.= (r`^j) *' (r`^1) *' poly_quotient(qq,x) by POLYNOM5:16
.= (r`^(j+1)) *' poly_quotient(qq,x) by Th27;
then j+1 in g by A8;
then j+1 <= j by A13,XXREAL_2:def 8;
hence contradiction by NAT_1:13;
end;
end;
i+j in F by A1,A16;
then i+j <= k by A10,XXREAL_2:def 8;
hence thesis by A2,A4,A9,A10,A5,A13,A17,XXREAL_0:1;
end;
theorem Th53:
for L being domRing, p, q being non-zero Polynomial of L holds
BRoots(p*'q) = BRoots(p) + BRoots(q)
proof
let L be domRing, p, q being non-zero Polynomial of L;
now
let i be object;
assume i in the carrier of L;
then reconsider x = i as Element of L;
thus (BRoots(p*'q)).i = multiplicity(p*'q, x) by Def8
.= multiplicity(p,x) + multiplicity(q,x) by Th52
.= (BRoots p).i + multiplicity(q,x) by Def8
.= (BRoots p).i + (BRoots q).i by Def8
.= (BRoots(p) + BRoots(q)).i by PRE_POLY:def 5;
end;
hence thesis by PBOOLE:3;
end;
Lm2: now
let L be domRing, p, q be non-zero Polynomial of L;
BRoots(p*'q) = BRoots(p) + BRoots(q) by Th53;
hence degree BRoots (p*'q) = degree (BRoots p) + degree BRoots q by Th12;
end;
theorem Th54:
for L being domRing, p being non-zero Polynomial of L st len p =
1 holds degree BRoots p = 0
proof
let L be domRing, p being non-zero Polynomial of L;
assume len p = 1;
then Roots p = {} by Th43;
then support BRoots p = {} by Def8;
then BRoots p = EmptyBag the carrier of L by PRE_POLY:81;
hence thesis by Th8;
end;
theorem Th55:
for L being domRing, x be Element of L, n being Nat
holds degree BRoots (<%-x, 1.L%>`^n) = n
proof
let L be domRing, x be Element of L;
set r = <%-x, 1.L%>;
defpred P[Nat] means degree BRoots (r`^$1) = $1;
A1: for n being Nat st P[n] holds P[n+1]
proof
let n be Nat such that
A2: P[n];
r`^(n+1) = (r`^n)*'r by POLYNOM5:19;
then
A3: degree BRoots(r`^(n+1)) = degree BRoots (r`^n) + degree BRoots r by Lm2
.= n + degree ({x},1)-bag by A2,Th51;
card {x} = 1 by CARD_1:30;
hence thesis by A3,Th10;
end;
len 1_. L = 1 & r`^0 = 1_. L by POLYNOM4:4,POLYNOM5:15;
then
A4: P[ 0 ] by Th54;
thus for n being Nat holds P[n] from NAT_1:sch 2(A4, A1);
end;
theorem
for L being algebraic-closed domRing, p being non-zero Polynomial of L
holds degree BRoots p = len p -' 1
proof
let L be algebraic-closed domRing, p be non-zero Polynomial of L;
defpred P[Nat] means for p being non-zero Polynomial of L st len p = $1 & $1
> 0 holds degree BRoots p = len p -' 1;
A1: for k being Nat st for n being Nat st n < k holds P[n] holds P[k]
proof
let k be Nat;
assume
A2: for n being Nat st n < k holds P[n];
let p be non-zero Polynomial of L;
assume that
A3: len p = k and
A4: k > 0;
A5: k >= 0 qua Nat+1 by A4,NAT_1:13;
thus thesis
proof
per cases by A5,XXREAL_0:1;
suppose
A6: k = 1;
hence degree BRoots p = 1-1 by A3,Th54
.= len p -' 1 by A3,A6,XREAL_1:233;
end;
suppose
A7: k > 1;
then p is with_roots by A3,POLYNOM5:def 9;
then consider x being Element of L such that
A8: x is_a_root_of p;
A9: multiplicity(p,x) >= 1 by A8,Th49;
set r = <%-x, 1.L%>;
consider F being finite non empty Subset of NAT such that
A10: F = {l where l is Element of NAT : ex q being Polynomial of L
st p = (<%-x, 1.L%>`^l) *' q} and
A11: multiplicity(p,x) = max F by Def7;
max F in F by XXREAL_2:def 8;
then consider l being Element of NAT such that
A12: l = max F and
A13: ex q being Polynomial of L st p = (<%-x, 1.L%>`^l) *' q by A10;
set rr = <%-x, 1.L%>`^l;
consider q being Polynomial of L such that
A14: p = (<%-x, 1.L%>`^l) *' q by A13;
reconsider q as non-zero Polynomial of L by A14,Th31;
len q > 0 by Th14;
then
A15: len q >= 0 qua Nat+1 by NAT_1:13;
thus thesis
proof
len q > 0 by Th14;
then
A16: q.(len q -'1) <> 0.L by Th15;
len rr > 0 by Th14;
then rr.(len rr -'1) <> 0.L by Th15;
then
A17: rr.(len rr -'1) * q.(len q -'1) <> 0.L by A16,VECTSP_2:def 1;
A18: l*2 -l+1 = l+1;
A19: len r = 2 by POLYNOM5:40;
then
A20: len rr = l*2 -l+1 by POLYNOM5:23;
then
A21: len rr > 1 by A9,A11,A12,NAT_1:13;
per cases by A15,XXREAL_0:1;
suppose
A22: len q = 1;
A23: len p = len rr + len q -1 by A14,A17,POLYNOM4:10
.= len rr by A22;
thus degree BRoots p = degree (BRoots rr) + degree BRoots q by A14
,Lm2
.= degree (BRoots rr) + (0 qua Nat) by A22,Th54
.= 2*l-l+1-1 by Th55
.= len p -' 1 by A3,A5,A20,A23,XREAL_1:233;
end;
suppose
A24: len q > 1;
then
A25: degree BRoots rr = l+1 -' 1 & degree BRoots q = len q -' 1 by A2,A3
,A14,A20,A21,Th33;
thus degree BRoots p = degree (BRoots rr) + degree BRoots q by A14
,Lm2
.= len rr-'1 + (len q -'1) by A19,A18,A25,POLYNOM5:23
.= len rr-1 + (len q -'1) by A21,XREAL_1:233
.= len rr-1 + (len q -1) by A24,XREAL_1:233
.= len rr + len q -1 -1
.= len p -1 by A14,A17,POLYNOM4:10
.= len p -' 1 by A3,A7,XREAL_1:233;
end;
end;
end;
end;
end;
A26: for n being Nat holds P[n] from NAT_1:sch 4(A1);
len p > 0 by Th14;
hence thesis by A26;
end;
definition
let L be add-associative right_zeroed right_complementable distributive non
empty doubleLoopStr, c be Element of L, n be Element of NAT;
func fpoly_mult_root(c,n) -> FinSequence of Polynom-Ring L means
:Def9:
len
it = n & for i being Element of NAT st i in dom it holds it.i = <% -c, 1.L%>;
existence
proof
<% -c, 1.L%> is Element of Polynom-Ring L by POLYNOM3:def 10;
then reconsider
f = n |-> <% -c, 1.L%> as FinSequence of Polynom-Ring L by FINSEQ_2:63;
take f;
thus
A1: len f = n by CARD_1:def 7;
let i be Element of NAT;
assume i in dom f;
then i in Seg n by A1,FINSEQ_1:def 3;
hence thesis by FUNCOP_1:7;
end;
uniqueness
proof
let it1, it2 be FinSequence of Polynom-Ring L such that
A2: len it1 = n and
A3: for i being Element of NAT st i in dom it1 holds it1.i = <% -c, 1. L%> and
A4: len it2 = n and
A5: for i being Element of NAT st i in dom it2 holds it2.i = <% -c, 1. L%>;
A6: dom it1 = dom it2 by A2,A4,FINSEQ_3:29;
now
let x be Nat;
assume
A7: x in dom it1;
hence it1.x = <% -c, 1.L%> by A3
.= it2.x by A5,A6,A7;
end;
hence thesis by A6;
end;
end;
definition
let L be add-associative right_zeroed right_complementable distributive non
empty doubleLoopStr, b be bag of the carrier of L;
func poly_with_roots(b) -> Polynomial of L means
:Def10:
ex f being
FinSequence of (the carrier of Polynom-Ring L)*, s being FinSequence of L st
len f = card support b & s = canFS(support b) & (for i being Element of NAT st
i in dom f holds f.i = fpoly_mult_root(s/.i,b.(s/.i))) & it = Product
FlattenSeq f;
existence
proof
rng canFS(support b) c= the carrier of L by XBOOLE_1:1;
then reconsider s = canFS(support b) as FinSequence of L by FINSEQ_1:def 4;
deffunc F(set) = fpoly_mult_root(s/.$1,b.(s/.$1));
consider f being FinSequence such that
A1: len f = card support b and
A2: for k being Nat st k in dom f holds f.k = F(k) from FINSEQ_1:sch 2;
rng f c= (the carrier of Polynom-Ring L)*
proof
let x be object;
assume x in rng f;
then consider i being Nat such that
A3: i in dom f & f.i = x by FINSEQ_2:10;
x = F(i) by A2,A3;
hence thesis by FINSEQ_1:def 11;
end;
then reconsider f as FinSequence of (the carrier of Polynom-Ring L)* by
FINSEQ_1:def 4;
reconsider it1 = Product FlattenSeq f as Polynomial of L by POLYNOM3:def 10
;
take it1, f, s;
thus len f = card support b by A1;
thus s = canFS(support b);
thus for i be Element of NAT st i in dom f holds f.i = fpoly_mult_root(s/.
i,b.(s/.i)) by A2;
thus thesis;
end;
uniqueness
proof
let it1, it2 be Polynomial of L;
given f1 being FinSequence of (the carrier of Polynom-Ring L)*, s1 being
FinSequence of L such that
A4: len f1 = card support b and
A5: s1 = canFS(support b) and
A6: for i being Element of NAT st i in dom f1 holds f1.i =
fpoly_mult_root(s1/.i,b.(s1/.i)) and
A7: it1 = Product FlattenSeq f1;
given f2 being FinSequence of (the carrier of Polynom-Ring L)*, s2 being
FinSequence of L such that
A8: len f2 = card support b and
A9: s2 = canFS(support b) & for i being Element of NAT st i in dom f2
holds f2.i = fpoly_mult_root(s2/.i,b.(s2/.i)) and
A10: it2 = Product FlattenSeq f2;
A11: dom f1 = dom f2 by A4,A8,FINSEQ_3:29;
now
let i be Nat;
assume
A12: i in dom f1;
hence f1.i = fpoly_mult_root(s1/.i,b.(s1/.i)) by A6
.= f2.i by A5,A9,A11,A12;
end;
hence thesis by A4,A7,A8,A10,FINSEQ_2:9;
end;
end;
theorem Th57:
for L being Abelian add-associative right_zeroed
right_complementable commutative distributive well-unital non empty
doubleLoopStr holds poly_with_roots(EmptyBag the carrier of L) = <%1.L%>
proof
let L be Abelian add-associative right_zeroed right_complementable
commutative distributive well-unital non empty doubleLoopStr;
set b = EmptyBag the carrier of L;
consider f being FinSequence of (the carrier of Polynom-Ring L)*, s being
FinSequence of L such that
A1: len f = card support b and
s = canFS(support b) and
for i being Element of NAT st i in dom f holds f.i = fpoly_mult_root(s/.
i,b.(s/.i)) and
A2: poly_with_roots(b) = Product FlattenSeq f by Def10;
f = <*>((the carrier of Polynom-Ring L)*) by A1;
then
1_Polynom-Ring L = 1.Polynom-Ring L & FlattenSeq f = <*>(the carrier of
Polynom-Ring L);
then Product FlattenSeq f = 1.Polynom-Ring L by GROUP_4:8
.= 1_.(L) by POLYNOM3:37;
hence thesis by A2,Th28;
end;
theorem Th58:
for L being add-associative right_zeroed right_complementable
distributive non empty doubleLoopStr, c being Element of L holds
poly_with_roots(({c},1)-bag) = <% -c, 1.L %>
proof
let L be add-associative right_zeroed right_complementable distributive non
empty doubleLoopStr, c being Element of L;
set b = ({c},1)-bag;
consider f being FinSequence of (the carrier of Polynom-Ring L)*, s being
FinSequence of L such that
A1: len f = card support b and
A2: s = canFS(support b) and
A3: for i being Element of NAT st i in dom f holds f.i = fpoly_mult_root
(s/.i,b.(s/.i)) and
A4: poly_with_roots(b) = Product FlattenSeq f by Def10;
A5: support b = {c} by Th5;
then
A6: s = <* c *> by A2,FINSEQ_1:94;
A7: card support b = 1 by A5,CARD_1:30;
then
A8: 1 in dom f by A1,FINSEQ_3:25;
then
A9: f.1 = f/.1 by PARTFUN1:def 6;
len s = 1 by A2,A7,FINSEQ_1:93;
then 1 in dom s by FINSEQ_3:25;
then
A10: s/.1 = s.1 by PARTFUN1:def 6
.= c by A6;
set f1 = fpoly_mult_root(s/.1,b.(s/.1));
c in {c} by TARSKI:def 1;
then b.(s/.1) = 1 by A10,Th4;
then
A11: len f1 = 1 by Def9;
then
A12: 1 in dom f1 by FINSEQ_3:25;
f = <*f.1*> by A1,A5,CARD_1:30,FINSEQ_5:14;
then
A13: FlattenSeq f = f.1 by A9,PRE_POLY:1;
A14: f.1 = fpoly_mult_root(s/.1,b.(s/.1)) by A3,A8;
A: f1.1 = f1/.1 by PARTFUN1:def 6,A12;
f1 = <*f1.1*> by A11,FINSEQ_5:14;
hence poly_with_roots(({c},1)-bag) = f1.1 by A,A4,A13,A14,FINSOP_1:11
.= <% -c, 1.L %> by A10,A12,Def9;
end;
theorem Th59:
for L being add-associative right_zeroed right_complementable
distributive non empty doubleLoopStr, b being bag of the carrier of L, f
being FinSequence of (the carrier of Polynom-Ring L)*, s being FinSequence of L
st len f = card support b & s = canFS(support b) & (for i being Element of NAT
st i in dom f holds f.i = fpoly_mult_root(s/.i,b.(s/.i))) holds len FlattenSeq
f = degree b
proof
let L be add-associative right_zeroed right_complementable distributive non
empty doubleLoopStr, b being bag of the carrier of L, f being FinSequence of (
the carrier of Polynom-Ring L)*, s being FinSequence of L such that
A1: len f = card support b and
A2: s = canFS(support b) and
A3: for i being Element of NAT st i in dom f holds f.i = fpoly_mult_root
(s/.i,b.(s/.i));
reconsider Cf = Card f as FinSequence of NAT;
consider g being FinSequence of NAT such that
A4: degree b = Sum g and
A5: g = b*canFS(support b) by Def3;
len s = card support b by A2,FINSEQ_1:93;
then
A6: dom f = dom s by A1,FINSEQ_3:29;
A7: now
A8: rng s c= dom b
proof
let x be object;
assume x in rng s;
then
A9: x in support b by A2,FUNCT_2:def 3;
support b c= dom b by PRE_POLY:37;
hence thesis by A9;
end;
thus dom Card f = dom f by CARD_3:def 2
.= dom g by A2,A6,A5,A8,RELAT_1:27;
let i be Nat;
assume i in dom Card f;
then
A10: i in dom f by CARD_3:def 2;
then
A11: g.i = b.(s.i) by A2,A6,A5,FUNCT_1:13;
f.i = fpoly_mult_root(s/.i,b.(s/.i)) by A3,A10;
then
A12: len (f.i) = b.(s/.i) by Def9;
thus Cf.i = card (f.i) by A10,CARD_3:def 2
.= g.i by A6,A10,A12,A11,PARTFUN1:def 6;
end;
len FlattenSeq f = Sum Cf by PRE_POLY:27;
hence thesis by A4,A7,FINSEQ_1:13;
end;
theorem Th60:
for L being add-associative right_zeroed right_complementable
distributive non empty doubleLoopStr, b being bag of the carrier of L, f
being FinSequence of (the carrier of Polynom-Ring L)*, s being FinSequence of L
, c being Element of L st len f = card support b & s = canFS(support b) & (for
i being Element of NAT st i in dom f holds f.i = fpoly_mult_root(s/.i,b.(s/.i))
) holds (c in support b implies card ((FlattenSeq f)"{<% -c, 1.L%>}) = b.c) & (
not c in support b implies card ((FlattenSeq f)"{<% -c, 1.L%>}) = 0)
proof
let L be add-associative right_zeroed right_complementable distributive non
empty doubleLoopStr, b be bag of the carrier of L, f be FinSequence of (the
carrier of Polynom-Ring L)*, s be FinSequence of L, c be Element of L such that
A1: len f = card support b and
A2: s = canFS(support b) and
A3: for i being Element of NAT st i in dom f holds f.i = fpoly_mult_root
(s/.i,b.(s/.i));
len f = len s by A1,A2,FINSEQ_1:93;
then
A4: dom f = dom s by FINSEQ_3:29;
hereby
set X = { k where k is Nat : k < b.c };
set ff = FlattenSeq f;
set Y = ff"{<% -c, 1.L%>};
assume c in support b;
then c in rng s by A2,FUNCT_2:def 3;
then consider i being Nat such that
A5: i in dom s and
A6: s.i = c by FINSEQ_2:10;
defpred P[object,object] means
ex n being Nat st n = $1 & $2 = (Sum
Card(f|(i-'1)))+(1+n);
A7: for x being object st x in X ex y being object st P[x,y]
proof
let x be object;
assume x in X;
then consider k being Nat such that
A8: x = k and
k < b.c;
take (Sum Card(f|(i-'1)))+(1+k);
thus thesis by A8;
end;
consider g being Function such that
A9: dom g = X and
A10: for x being object st x in X holds P[x,g.x] from CLASSES1:sch 1(A7);
A11: s/.i = c by A5,A6,PARTFUN1:def 6;
now
let y be object;
A12: <% -c, 1.L%>.0 = -c by POLYNOM5:38;
hereby
assume y in rng g;
then consider x being object such that
A13: x in dom g and
A14: y = g.x by FUNCT_1:def 3;
consider n being Nat such that
A15: n = x and
A16: g.x = (Sum Card(f|(i-'1)))+(1+n) by A9,A10,A13;
ex k being Nat st x = k & k < b.c by A9,A13;
then
A17: 1 <= 1+n & 1+n <= b.c by A15,NAT_1:12,13;
A18: f.i = fpoly_mult_root(s/.i,b.(s/.i)) by A3,A4,A5;
then len (f.i) = b.c by A11,Def9;
then
A19: 1+n in dom (f.i) by A17,FINSEQ_3:25;
then (f.i).(1+n) = <% -c, 1.L%> by A11,A18,Def9;
then
A20: (f.i).(1+n) in {<% -c, 1.L%>} by TARSKI:def 1;
(Sum Card (f|(i-'1))) + (1+n) in dom ff & (f.i).(1+n) = ff.((Sum
Card (f|(i -'1))) + (1+n)) by A4,A5,A19,PRE_POLY:30;
hence y in Y by A14,A16,A20,FUNCT_1:def 7;
end;
assume
A21: y in Y;
then reconsider yn = y as Element of NAT;
A22: ff.y in {<% -c, 1.L%>} by A21,FUNCT_1:def 7;
y in dom ff by A21,FUNCT_1:def 7;
then consider i1, j being Nat such that
A23: i1 in dom f and
A24: j in dom (f.i1) and
A25: yn = (Sum Card (f|(i1-'1))) + j and
A26: (f.i1).j = ff.yn by PRE_POLY:29;
A27: f.i1 = fpoly_mult_root(s/.i1,b.(s/.i1)) by A3,A23;
then (f.i1).j = <%-s/.i1, 1.L%> by A24,Def9;
then <% -c, 1.L%> = <%-s/.i1, 1.L%> by A22,A26,TARSKI:def 1;
then
A28: c = s/.i1 by A12,POLYNOM5:38,RLVECT_1:18;
i1 in dom s & s/.i1 = s.i1 by A4,A23,PARTFUN1:def 6;
then
A29: i1 = i by A2,A5,A6,A28,FUNCT_1:def 4;
consider j1 being Nat such that
A30: j = j1 + 1 by A24,FINSEQ_3:24,NAT_1:6;
reconsider j1 as Element of NAT by ORDINAL1:def 12;
len (f.i1) = b.c by A27,A28,Def9;
then j <= b.c by A24,FINSEQ_3:25;
then j1 < b.c by A30,NAT_1:13;
then
A31: j1 in X;
then
ex n being Nat st n = j1 & g.j1 = (Sum Card(f |(i-'1)))+(
1+n) by A10;
hence y in rng g by A9,A25,A30,A29,A31,FUNCT_1:3;
end;
then
A32: rng g = Y by TARSKI:2;
g is one-to-one
proof
let x1,x2 be object such that
A33: x1 in dom g & x2 in dom g and
A34: g.x1 = g.x2;
(ex n1 being Nat st n1 = x1 & g.x1 = (Sum Card (f|(i-'1)
))+(1+n1) )& ex n2 being Nat st n2 = x2 & g.x2 = (Sum Card (f|(i-'1)
))+(1+ n2) by A9,A10,A33;
hence thesis by A34;
end;
then b.c = { k where k is Nat : k < b.c } & X,Y are_equipotent
by A9,A32,AXIOMS:4,WELLORD2:def 4;
hence card ((FlattenSeq f)"{<% -c, 1.L%>}) = b.c by CARD_1:def 2;
end;
assume that
A35: not c in support b and
A36: card ((FlattenSeq f)"{<% -c, 1.L%>}) <> 0;
consider x being object such that
A37: x in (FlattenSeq f)"{<% -c, 1.L%>} by A36,CARD_1:27,XBOOLE_0:def 1;
A38: x in dom FlattenSeq f by A37,FUNCT_1:def 7;
reconsider x as Element of NAT by A37;
consider i, j being Nat such that
A39: i in dom f and
A40: j in dom (f.i) and
x = (Sum Card (f|(i-'1))) + j and
A41: (f.i).j = (FlattenSeq f).x by A38,PRE_POLY:29;
A42: s/.i = s.i & s.i in rng s by A4,A39,FUNCT_1:3,PARTFUN1:def 6;
(FlattenSeq f).x in {<% -c, 1.L%>} by A37,FUNCT_1:def 7;
then
A43: (FlattenSeq f).x = <% -c, 1.L%> by TARSKI:def 1;
f.i = fpoly_mult_root(s/.i,b.(s/.i)) by A3,A39;
then
A44: (f.i).j = <% -s/.i, 1.L%> by A40,Def9;
<% -c, 1.L%>.0 = -c by POLYNOM5:38;
then c = s/.i by A41,A43,A44,POLYNOM5:38,RLVECT_1:18;
hence contradiction by A2,A35,A42,FUNCT_2:def 3;
end;
theorem Th61:
for L being comRing for b1,b2 being bag of the carrier of L
holds poly_with_roots(b1+b2) = (poly_with_roots b1)*'(poly_with_roots b2)
proof
let L be comRing, b1,b2 be bag of the carrier of L;
set b = b1+b2;
A1: support b = support b1 \/ support b2 by PRE_POLY:38;
consider f2 being FinSequence of (the carrier of Polynom-Ring L)*, s2 being
FinSequence of L such that
A2: len f2 = card support b2 and
A3: s2 = canFS(support b2) and
A4: for i being Element of NAT st i in dom f2 holds f2.i =
fpoly_mult_root(s2/.i,b2.(s2/.i)) and
A5: poly_with_roots(b2) = Product FlattenSeq f2 by Def10;
consider f1 being FinSequence of (the carrier of Polynom-Ring L)*, s1 being
FinSequence of L such that
A6: len f1 = card support b1 and
A7: s1 = canFS(support b1) and
A8: for i being Element of NAT st i in dom f1 holds f1.i =
fpoly_mult_root(s1/.i,b1.(s1/.i)) and
A9: poly_with_roots(b1) = Product FlattenSeq f1 by Def10;
consider f being FinSequence of (the carrier of Polynom-Ring L)*, s being
FinSequence of L such that
A10: len f = card support b and
A11: s = canFS(support b) and
A12: for i being Element of NAT st i in dom f holds f.i = fpoly_mult_root
(s/.i,b.(s/.i)) and
A13: poly_with_roots(b1+b2) = Product FlattenSeq f by Def10;
set ff = FlattenSeq f, ff1 = FlattenSeq f1, ff2 = FlattenSeq f2;
A14: len ff = degree b by A10,A11,A12,Th59;
A15: len ff2 = degree b2 by A2,A3,A4,Th59;
set g = (FlattenSeq f1) ^ (FlattenSeq f2);
len g = len ff1 + len ff2 by FINSEQ_1:22
.= degree b1 + degree b2 by A6,A7,A8,A15,Th59
.= degree b by Th12;
then
A16: dom ff = dom g by A14,FINSEQ_3:29;
A17: len s = card support b by A11,FINSEQ_1:93;
now
let x be object;
per cases;
suppose
x in rng ff;
then consider k being Nat such that
A18: k in dom ff and
A19: ff.k = x by FINSEQ_2:10;
consider i, j being Nat such that
A20: i in dom f and
A21: j in dom (f.i) and
k = (Sum Card (f|(i-'1))) + j and
A22: (f.i).j = ff.k by A18,PRE_POLY:29;
f.i = fpoly_mult_root(s/.i,b.(s/.i)) by A12,A20;
then
A23: (f.i).j = <% -s/.i, 1.L %> by A21,Def9;
i in dom s by A10,A17,A20,FINSEQ_3:29;
then s.i = s/.i & s.i in rng s by FUNCT_1:3,PARTFUN1:def 6;
then
A24: s/.i in support b by A11,FUNCT_2:def 3;
A25: card (g"{x}) = card (ff1"{x}) + card (ff2"{x}) by FINSEQ_3:57;
per cases by A1,A24,XBOOLE_0:def 3;
suppose
A26: s/.i in support b1 & not s/.i in support b2;
then
A27: card(ff2"{x}) = 0 by A2,A3,A4,A19,A22,A23,Th60;
thus card Coim(ff,x) = b.(s/.i) by A10,A11,A12,A19,A22,A23,A24,Th60
.= b1.(s/.i) + b2.(s/.i) by PRE_POLY:def 5
.= b1.(s/.i) + (0 qua Nat) by A26,PRE_POLY:def 7
.= card Coim(g,x) by A6,A7,A8,A19,A22,A23,A25,A26,A27,Th60;
end;
suppose
A28: not s/.i in support b1 & s/.i in support b2;
then
A29: card(ff2"{x}) = b2.(s/.i) by A2,A3,A4,A19,A22,A23,Th60;
thus card Coim(ff,x) = b.(s/.i) by A10,A11,A12,A19,A22,A23,A24,Th60
.= b1.(s/.i) + b2.(s/.i) by PRE_POLY:def 5
.= 0 qua Nat+b2.(s/.i) by A28,PRE_POLY:def 7
.= card Coim(g,x) by A6,A7,A8,A19,A22,A23,A25,A28,A29,Th60;
end;
suppose
A30: s/.i in support b1 & s/.i in support b2;
then
A31: card(ff2"{x}) = b2.(s/.i) by A2,A3,A4,A19,A22,A23,Th60;
thus card Coim(ff,x) = b.(s/.i) by A10,A11,A12,A19,A22,A23,A24,Th60
.= b1.(s/.i) + b2.(s/.i) by PRE_POLY:def 5
.= card Coim(g,x) by A6,A7,A8,A19,A22,A23,A25,A30,A31,Th60;
end;
end;
suppose
A32: not x in rng ff;
now
assume x in rng g;
then
A33: x in (rng ff1 \/ rng ff2) by FINSEQ_1:31;
per cases by A33,XBOOLE_0:def 3;
suppose
x in rng ff1;
then consider k being Nat such that
A34: k in dom ff1 and
A35: ff1.k = x by FINSEQ_2:10;
consider i, j being Nat such that
A36: i in dom f1 and
A37: j in dom (f1.i) and
k = (Sum Card (f1|(i-'1))) + j and
A38: (f1.i).j = ff1.k by A34,PRE_POLY:29;
f1.i = fpoly_mult_root(s1/.i,b1.(s1/.i)) by A8,A36;
then
A39: (f1.i).j = <% -s1/.i, 1.L %> by A37,Def9;
len s1 = card support b1 by A7,FINSEQ_1:93;
then i in dom s1 by A6,A36,FINSEQ_3:29;
then s1.i = s1/.i & s1.i in rng s1 by FUNCT_1:3,PARTFUN1:def 6;
then s1/.i in support b1 by A7,FUNCT_2:def 3;
then
A40: s1/.i in support b by A1,XBOOLE_0:def 3;
then b.(s1/.i) <> 0 by PRE_POLY:def 7;
then
A41: 0 qua Nat+1 <= b.(s1/.i) by NAT_1:13;
s1/.i in rng s by A11,A40,FUNCT_2:def 3;
then consider l being Nat such that
A42: l in dom s and
A43: s.l = s1/.i by FINSEQ_2:10;
A44: s.l = s/.l by A42,PARTFUN1:def 6;
A45: l in dom f by A10,A17,A42,FINSEQ_3:29;
then
A46: f.l = fpoly_mult_root(s/.l,b.(s/.l)) by A12;
then len (f.l) = b.(s/.l) by Def9;
then
A47: 1 in dom (f.l) by A43,A44,A41,FINSEQ_3:25;
then
(Sum Card (f|(l-'1))) + 1 in dom ff & (f.l).1 = ff.((Sum Card (
f|(l-'1))) + 1) by A45,PRE_POLY:30;
then (f.l).1 in rng ff by FUNCT_1:3;
hence contradiction by A32,A35,A38,A39,A43,A46,A44,A47,Def9;
end;
suppose
x in rng ff2;
then consider k being Nat such that
A48: k in dom ff2 and
A49: ff2.k = x by FINSEQ_2:10;
consider i, j being Nat such that
A50: i in dom f2 and
A51: j in dom (f2.i) and
k = (Sum Card (f2|(i-'1))) + j and
A52: (f2.i).j = ff2.k by A48,PRE_POLY:29;
f2.i = fpoly_mult_root(s2/.i,b2.(s2/.i)) by A4,A50;
then
A53: (f2.i).j = <% -s2/.i, 1.L %> by A51,Def9;
len s2 = card support b2 by A3,FINSEQ_1:93;
then i in dom s2 by A2,A50,FINSEQ_3:29;
then s2.i = s2/.i & s2.i in rng s2 by FUNCT_1:3,PARTFUN1:def 6;
then s2/.i in support b2 by A3,FUNCT_2:def 3;
then
A54: s2/.i in support b by A1,XBOOLE_0:def 3;
then b.(s2/.i) <> 0 by PRE_POLY:def 7;
then
A55: 0 qua Nat+1 <= b.(s2/.i) by NAT_1:13;
s2/.i in rng s by A11,A54,FUNCT_2:def 3;
then consider l being Nat such that
A56: l in dom s and
A57: s.l = s2/.i by FINSEQ_2:10;
A58: s.l = s/.l by A56,PARTFUN1:def 6;
A59: l in dom f by A10,A17,A56,FINSEQ_3:29;
then
A60: f.l = fpoly_mult_root(s/.l,b.(s/.l)) by A12;
then len (f.l) = b.(s/.l) by Def9;
then
A61: 1 in dom (f.l) by A57,A58,A55,FINSEQ_3:25;
then
(Sum Card (f|(l-'1))) + 1 in dom ff & (f.l).1 = ff.((Sum Card (
f|(l-'1))) + 1) by A59,PRE_POLY:30;
then (f.l).1 in rng ff by FUNCT_1:3;
hence contradiction by A32,A49,A52,A53,A57,A60,A58,A61,Def9;
end;
end;
then g"{x} = {} by FUNCT_1:72;
hence card Coim(ff,x) = card Coim(g,x) by A32,FUNCT_1:72;
end;
end;
then ff, g are_fiberwise_equipotent by CLASSES1:def 10;
then ex p being Permutation of dom FlattenSeq f st FlattenSeq f = ((
FlattenSeq f1) ^ (FlattenSeq f2)) * p by A16,RFINSEQ:4;
hence
poly_with_roots(b1+b2) = Product ((FlattenSeq f1) ^ (FlattenSeq f2)) by A13
,A16,Th13
.= (Product FlattenSeq f1) * (Product FlattenSeq f2) by GROUP_4:5
.= (poly_with_roots b1)*'(poly_with_roots b2) by A9,A5,POLYNOM3:def 10;
end;
theorem
for L being algebraic-closed domRing, p being non-zero (Polynomial of
L) st p.(len p-'1) = 1.L holds p = poly_with_roots(BRoots(p))
proof
let L be algebraic-closed domRing, p be non-zero (Polynomial of L);
assume
A1: p.(len p-'1) = 1.L;
defpred P[Nat] means for p being non-zero Polynomial of L st len p = $1 & $1
>= 1 & p.(len p -'1) = 1.L holds p = poly_with_roots(BRoots(p));
len p > 0 by Th14;
then
A2: len p >= 0 qua Nat+1 by NAT_1:13;
A3: for n being Nat st n >= 1 & P[n] holds P[n+1]
proof
let n be Nat such that
A4: n >= 1 and
A5: P[n];
let p being non-zero Polynomial of L such that
A6: len p = n+1 and
n+1 >= 1 and
A7: p.(len p -'1) = 1.L;
n+1 > 1 by A4,NAT_1:13;
then p is with_roots by A6,POLYNOM5:def 9;
then consider x being Element of L such that
A8: x is_a_root_of p;
set r = <%-x,1.L%>;
set q = poly_quotient(p,x);
A9: p = r*'q by A8,Th47;
then reconsider q as non-zero Polynomial of L by Th31;
A10: len r = 2 by POLYNOM5:40;
then
A11: r.(len r -'1) <> 0.L by Th15;
len q > 0 by Th14;
then q.(len q -'1) <> 0.L by Th15;
then r.(len r -'1) * q.(len q -'1) <> 0.L by A11,VECTSP_2:def 1;
then
A12: len p = len q + (1+1)- 1 by A9,A10,POLYNOM4:10;
q.(len q -'1) = 1.L by A7,A9,Th38;
then
A13: q = poly_with_roots(BRoots(q)) by A4,A5,A6,A12;
A14: poly_with_roots(({x},1)-bag) = <%-x,1.L%> by Th58;
BRoots r = ({x},1)-bag by Th51;
then BRoots(p) = ({x},1)-bag + BRoots(q) by A9,Th53;
hence thesis by A9,A13,A14,Th61;
end;
A15: P[1]
proof
let p be non-zero Polynomial of L such that
A16: len p = 1 and
1 >= 1 and
A17: p.(len p -'1) = 1.L;
degree BRoots p = 0 by A16,Th54;
then
A18: BRoots p = EmptyBag the carrier of L by Th9;
len p -'1 = 0 by A16,XREAL_1:232;
hence p = <%1.L%> by A16,A17,ALGSEQ_1:def 5
.= poly_with_roots(BRoots(p)) by A18,Th57;
end;
for n being Nat st n >= 1 holds P[n] from NAT_1:sch 8(A15,A3);
hence thesis by A1,A2;
end;
theorem
for L being comRing, s being non empty finite Subset of L, f being
FinSequence of Polynom-Ring L st len f = card s & for i being Element of NAT, c
being Element of L st i in dom f & c = (canFS(s)).i holds f.i = <% -c, 1.L %>
holds poly_with_roots((s,1)-bag) = Product(f)
proof
let L be comRing;
set cL = the carrier of L;
set cPRL = the carrier of Polynom-Ring L;
let s be non empty finite Subset of cL, f be FinSequence of cPRL such that
A1: len f = card s and
A2: for i being Element of NAT, c being Element of cL st i in dom f & c
= (canFS(s)).i holds f.i = <% -c, 1.L %>;
set cs = canFS(s);
A3: rng cs = s by FUNCT_2:def 3;
defpred P[Nat] means ex t being finite Subset of cL, g being
FinSequence of cPRL st t = rng (cs | Seg $1) & g = f | Seg $1 & poly_with_roots
((t,1)-bag) = Product(g);
A4: len cs = card s by FINSEQ_1:93;
then
A5: dom f = dom cs by A1,FINSEQ_3:29;
A6: for j being Element of NAT st 1 <= j & j < len f holds P[j] implies P[j +1]
proof
let j be Element of NAT such that
A7: 1 <= j and
A8: j < len f;
reconsider g1 = f | Seg (j+1) as FinSequence of cPRL by FINSEQ_1:18;
A9: j+1 <= len f by A8,NAT_1:13;
then ex l being Nat st len f = j+1+l by NAT_1:10;
then
A10: len g1 = j+1 by FINSEQ_3:53;
1 <= j+1 by A7,NAT_1:13;
then
A11: j+1 in dom cs by A1,A4,A9,FINSEQ_3:25;
then cs.(j+1) in s by FINSEQ_2:11;
then reconsider csj1 = cs.(j+1) as Element of cL;
A12: g1.(j+1) = f.(j+1) by FINSEQ_1:4,FUNCT_1:49
.= <% -csj1, 1.L %> by A2,A5,A11;
reconsider csja1 = cs | Seg (j+1) as FinSequence of s by FINSEQ_1:18;
reconsider csja = cs | Seg j as FinSequence of s by FINSEQ_1:18;
given t being finite Subset of cL, g being FinSequence of cPRL such that
A13: t = rng (cs | Seg j) and
A14: g = f | Seg j and
A15: poly_with_roots((t,1)-bag) = Product(g);
j <= j+1 by NAT_1:12;
then Seg j c= Seg (j+1) by FINSEQ_1:5;
then g = g1 | Seg j by A14,RELAT_1:74;
then
A16: g1 = g ^ <* <% -csj1, 1.L %> *> by A10,A12,FINSEQ_3:55;
reconsider pt = poly_with_roots((t,1)-bag) as Polynomial of L;
set t1 = rng csja1;
Seg (j+1) = Seg j \/ {j+1} by FINSEQ_1:9;
then
A17: csja1 = csja \/ cs|{j+1} by RELAT_1:78;
cs|{j+1} = (j+1) .--> csj1 by A11,FUNCT_7:6;
then rng (cs|{j+1}) = {csj1} by FUNCOP_1:8;
then
A18: t1 = t \/ {csj1} by A13,A17,RELAT_1:12;
reconsider epj1 =<% -csj1, 1.L %> as Element of cPRL by POLYNOM3:def 10;
reconsider pj1 = poly_with_roots(({csj1},1)-bag) as Polynomial of L;
A19: pj1 = epj1 by Th58;
reconsider t1 as finite Subset of cL by A18;
take t1, g1;
thus t1 = rng (cs | Seg (j+1)) & g1 = f | Seg (j+1);
t misses {csj1}
proof
assume not thesis;
then t /\ {csj1} <> {} by XBOOLE_0:def 7;
then consider x being object such that
A20: x in t /\ {csj1} by XBOOLE_0:def 1;
x in {csj1} by A20,XBOOLE_0:def 4;
then
A21: x = csj1 by TARSKI:def 1;
x in t by A20,XBOOLE_0:def 4;
then consider i being object such that
A22: i in dom (cs | Seg j) and
A23: x = (cs | Seg j).i by A13,FUNCT_1:def 3;
A24: i in Seg j by A22,RELAT_1:57;
reconsider i as Element of NAT by A22;
A25: 1 <= i by A24,FINSEQ_1:1;
i <= j by A24,FINSEQ_1:1;
then
A26: i < j+1 by NAT_1:13;
x = cs.i by A22,A23,FUNCT_1:47;
hence contradiction by A1,A4,A3,A9,A21,A25,A26,GRAPH_5:7;
end;
then (t1,1)-bag = (t,1)-bag + ({csj1},1)-bag by A18,Th7;
hence poly_with_roots((t1,1)-bag) = pt *' pj1 by Th61
.= Product(g) * epj1 by A15,A19,POLYNOM3:def 10
.= Product(g1) by A16,GROUP_4:6;
end;
f | Seg len f is FinSequence by FINSEQ_1:18;
then
A27: cs | Seg len f is FinSequence & f | Seg len f = f by FINSEQ_1:18
,FINSEQ_2:20;
A28: 0 qua Nat+1 <= len f by A1,NAT_1:13;
A29: P[1]
proof
1 in dom cs by A1,A4,A28,FINSEQ_3:25;
then reconsider cs1 = cs.1 as Element of s by FINSEQ_2:11;
reconsider g = f | Seg 1 as FinSequence of cPRL by FINSEQ_1:18;
reconsider cs1a = cs | Seg 1 as FinSequence of s by FINSEQ_1:18;
A30: cs1 in cL;
A31: 1 in Seg 1 by FINSEQ_1:1;
then
A32: cs1a.1 = cs1 by FUNCT_1:49;
reconsider cs1 = cs.1 as Element of cL by A30;
reconsider t = {cs1} as finite Subset of cL;
take t, g;
consider s1 being Element of s such that
A33: cs1a = <* s1 *> by A1,A4,A28,TREES_9:34;
thus t = rng (cs | Seg 1) & g = f | Seg 1 by A33,A32,FINSEQ_1:39;
consider p1 being Element of cPRL such that
A34: g = <* p1 *> by A28,TREES_9:34;
A35: g.1 = p1 & Product(g) = p1 by A34,FINSOP_1:11;
A36: 1 in dom f by A28,FINSEQ_3:25;
then reconsider f1 = f.1 as Element of cPRL by FINSEQ_2:11;
A37: g.1 = f1 by A31,FUNCT_1:49;
f1 = <% -cs1, 1.L %> by A2,A36;
hence thesis by A37,A35,Th58;
end;
for i being Element of NAT st 1 <= i & i <= len f holds P[i] from
INT_1:sch 7 (A29,A6);
then
ex t being finite Subset of cL, g being FinSequence of cPRL st t = rng (
cs | Seg len f) & g = f | Seg len f & poly_with_roots((t,1)-bag ) = Product(g)
by A28;
hence thesis by A1,A4,A27,A3,FINSEQ_2:20;
end;
theorem
for L being non trivial comRing, s being non empty finite Subset of L,
x being Element of L, f being FinSequence of L st len f = card s & for i being
Element of NAT, c being Element of L st i in dom f & c = (canFS(s)).i holds f.i
= eval(<% -c, 1.L %>,x) holds eval(poly_with_roots((s,1)-bag),x) = Product(f)
proof
let L be non trivial comRing;
set cL = the carrier of L;
let s be non empty finite Subset of cL, x be Element of cL, f be FinSequence
of L such that
A1: len f = card s and
A2: for i being Element of NAT, c being Element of cL st i in dom f & c
= (canFS(s)).i holds f.i = eval(<% -c, 1.L %>,x);
set cs = canFS(s);
A3: rng cs = s by FUNCT_2:def 3;
defpred P[Nat] means ex t being finite Subset of cL, g being
FinSequence of cL st t = rng (cs | Seg $1) & g = f | Seg $1 & eval(
poly_with_roots((t,1)-bag),x) = Product(g);
A4: len cs = card s by FINSEQ_1:93;
then
A5: dom f = dom cs by A1,FINSEQ_3:29;
A6: for j being Element of NAT st 1 <= j & j < len f holds P[j] implies P[j +1]
proof
let j be Element of NAT such that
A7: 1 <= j and
A8: j < len f;
reconsider g1 = f | Seg (j+1) as FinSequence of cL by FINSEQ_1:18;
A9: j+1 <= len f by A8,NAT_1:13;
then ex l being Nat st len f = j+1+l by NAT_1:10;
then
A10: len g1 = j+1 by FINSEQ_3:53;
1 <= j+1 by A7,NAT_1:13;
then
A11: j+1 in dom cs by A1,A4,A9,FINSEQ_3:25;
then cs.(j+1) in s by FINSEQ_2:11;
then reconsider csj1 = cs.(j+1) as Element of cL;
A12: g1.(j+1) = f.(j+1) by FINSEQ_1:4,FUNCT_1:49
.= eval(<% -csj1, 1.L %>,x) by A2,A5,A11;
reconsider csja1 = cs | Seg (j+1) as FinSequence of s by FINSEQ_1:18;
reconsider csja = cs | Seg j as FinSequence of s by FINSEQ_1:18;
given t being finite Subset of cL, g being FinSequence of cL such that
A13: t = rng (cs | Seg j) and
A14: g = f | Seg j and
A15: eval(poly_with_roots((t,1)-bag),x) = Product(g);
j <= j+1 by NAT_1:12;
then Seg j c= Seg (j+1) by FINSEQ_1:5;
then g = g1 | Seg j by A14,RELAT_1:74;
then
A16: g1 = g ^ <* eval(<% -csj1, 1.L %>,x) *> by A10,A12,FINSEQ_3:55;
reconsider pt = poly_with_roots((t,1)-bag) as Polynomial of L;
set t1 = rng csja1;
Seg (j+1) = Seg j \/ {j+1} by FINSEQ_1:9;
then
A17: csja1 = csja \/ cs|{j+1} by RELAT_1:78;
cs|{j+1} = (j+1) .--> csj1 by A11,FUNCT_7:6;
then rng (cs|{j+1}) = {csj1} by FUNCOP_1:8;
then
A18: t1 = t \/ {csj1} by A13,A17,RELAT_1:12;
then reconsider t1 as finite Subset of cL;
take t1, g1;
thus t1 = rng (cs | Seg (j+1)) & g1 = f | Seg (j+1);
reconsider pj1 = poly_with_roots(({csj1},1)-bag) as Polynomial of L;
A19: pj1 = <% -csj1, 1.L %> by Th58;
t misses {csj1}
proof
assume not thesis;
then t /\ {csj1} <> {} by XBOOLE_0:def 7;
then consider x being object such that
A20: x in t /\ {csj1} by XBOOLE_0:def 1;
x in {csj1} by A20,XBOOLE_0:def 4;
then
A21: x = csj1 by TARSKI:def 1;
x in t by A20,XBOOLE_0:def 4;
then consider i being object such that
A22: i in dom (cs | Seg j) and
A23: x = (cs | Seg j).i by A13,FUNCT_1:def 3;
A24: i in Seg j by A22,RELAT_1:57;
reconsider i as Element of NAT by A22;
A25: 1 <= i by A24,FINSEQ_1:1;
i <= j by A24,FINSEQ_1:1;
then
A26: i < j+1 by NAT_1:13;
x = cs.i by A22,A23,FUNCT_1:47;
hence contradiction by A1,A4,A3,A9,A21,A25,A26,GRAPH_5:7;
end;
then (t1,1)-bag = (t,1)-bag + ({csj1},1)-bag by A18,Th7;
then poly_with_roots((t1,1)-bag) = pt *' pj1 by Th61;
hence
eval(poly_with_roots((t1,1)-bag),x) = Product(g) * eval(pj1,x) by A15,
POLYNOM4:24
.= Product(g1) by A16,A19,GROUP_4:6;
end;
f | Seg len f is FinSequence by FINSEQ_1:18;
then
A27: cs | Seg len f is FinSequence & f | Seg len f = f by FINSEQ_1:18
,FINSEQ_2:20;
A28: 0 qua Nat+1 <= len f by A1,NAT_1:13;
A29: P[1]
proof
1 in dom cs by A1,A4,A28,FINSEQ_3:25;
then reconsider cs1 = cs.1 as Element of s by FINSEQ_2:11;
reconsider g = f | Seg 1 as FinSequence of cL by FINSEQ_1:18;
reconsider cs1a = cs | Seg 1 as FinSequence of s by FINSEQ_1:18;
A30: cs1 in cL;
A31: 1 in Seg 1 by FINSEQ_1:1;
then
A32: cs1a.1 = cs1 by FUNCT_1:49;
reconsider cs1 = cs.1 as Element of cL by A30;
reconsider t = {cs1} as finite Subset of cL;
take t, g;
consider s1 being Element of s such that
A33: cs1a = <* s1 *> by A1,A4,A28,TREES_9:34;
thus t = rng (cs | Seg 1) & g = f | Seg 1 by A33,A32,FINSEQ_1:39;
consider p1 being Element of cL such that
A34: g = <* p1 *> by A28,TREES_9:34;
A35: g.1 = p1 & Product(g) = p1 by A34,FINSOP_1:11;
A36: 1 in dom f by A28,FINSEQ_3:25;
then reconsider f1 = f.1 as Element of cL by FINSEQ_2:11;
A37: g.1 = f1 by A31,FUNCT_1:49;
f1 = eval(<% -cs1, 1.L %>,x) by A2,A36;
hence thesis by A37,A35,Th58;
end;
for i being Element of NAT st 1 <= i & i <= len f holds P[i] from
INT_1:sch 7 (A29,A6);
then
ex t being finite Subset of cL, g being FinSequence of cL st t = rng (cs
| Seg len f) & g = f | Seg len f & eval(poly_with_roots((t,1 )-bag),x) =
Product(g) by A28;
hence thesis by A1,A4,A27,A3,FINSEQ_2:20;
end;