Copyright (c) 2003 Association of Mizar Users
environ
vocabulary ARYTM_1, SQUARE_1, ARYTM_3, FINSEQ_1, RELAT_1, FUNCT_1, RLVECT_1,
BOOLE, FINSEQ_2, FINSEQ_4, BINOP_1, VECTSP_1, LATTICES, NORMSP_1,
COMPLFLD, GROUP_1, REALSET1, POLYNOM1, TARSKI, CARD_1, CARD_3, SETWISEO,
ALGSEQ_1, POLYNOM3, POLYNOM2, ALGSTR_2, FUNCT_4, VECTSP_2, FUNCOP_1,
FUNCT_2, SEQM_3, RFINSEQ, POLYNOM5, FVSUM_1, FINSET_1, NEWTON, MCART_1,
SGRAPH1, CAT_1, DTCONSTR, PBOOLE, MEMBERED, ANPROJ_1, UPROOTS;
notation TARSKI, XBOOLE_0, SUBSET_1, STRUCT_0, NUMBERS, XREAL_0, ZFMISC_1,
REAL_1, NAT_1, SETWISEO, RLVECT_1, VECTSP_1, VECTSP_2, BINOP_1, RELAT_1,
FUNCT_1, FUNCT_2, SETWOP_2, FINSEQ_1, FINSEQ_2, FINSEQ_4, FINSOP_1,
TOPREAL1, NORMSP_1, BINARITH, RVSUM_1, ALGSEQ_1, COMPLFLD, POLYNOM3,
POLYNOM4, POLYNOM5, CARD_1, FINSET_1, GROUP_1, MCART_1, PRE_CIRC,
FUNCT_4, RLVECT_2, CQC_LANG, DTCONSTR, RFINSEQ, POLYNOM1, FVSUM_1,
WSIERP_1, PBOOLE, SEQM_3, MEMBERED, REALSET1;
constructors REAL_1, FINSOP_1, MONOID_0, WELLORD2, TOPREAL1, BINARITH,
POLYNOM4, FVSUM_1, POLYNOM5, PREPOWER, SETWOP_2, WELLFND1, PRE_CIRC,
FINSEQOP, ALGSTR_1, RLVECT_2, CQC_LANG, POLYNOM2, WSIERP_1, SETWISEO,
GOBOARD1;
clusters XREAL_0, STRUCT_0, RELSET_1, SEQ_1, VECTSP_1, VECTSP_2, FINSEQ_2,
POLYNOM1, POLYNOM3, MONOID_0, NAT_1, INT_1, POLYNOM5, FINSEQ_1, FINSET_1,
CARD_1, MEMBERED, FUNCT_1, ALGSTR_1, SUBSET_1, ORDINAL2, RFINSEQ,
GOBRD13, PRE_CIRC, PRELAMB, CHAIN_1, POLYNOM7;
requirements NUMERALS, BOOLE, SUBSET, ARITHM, REAL;
definitions TARSKI, VECTSP_2, FUNCT_1, POLYNOM5;
theorems GROUP_1, CARD_1, FINSEQ_1, ZFMISC_1, NAT_1, FUNCT_1, FUNCT_2,
RELAT_1, TARSKI, XBOOLE_0, XBOOLE_1, VECTSP_1, REAL_1, XCMPLX_1,
POLYNOM5, BINARITH, INT_1, XCMPLX_0, SCMFSA_7, AXIOMS, RVSUM_1, FVSUM_1,
FINSEQ_3, FINSEQ_2, FINSEQ_4, POLYNOM4, POLYNOM3, NORMSP_1, FUNCT_7,
ALGSEQ_1, RLVECT_1, FINSET_1, PBOOLE, FUNCOP_1, POLYNOM1, MATRIX_3,
PRE_CIRC, VECTSP_2, CARD_2, FINSEQ_5, GRAPH_5, QC_LANG4, CQC_LANG,
DTCONSTR, BAGORDER, RFINSEQ, GOBOARD9, WELLORD2, CARD_3, ORDINAL2, FSM_1,
JORDAN3, FINSOP_1, MONOID_0, INTEGRA1, SEQM_3, TRIANG_1, FUNCT_4,
MCART_1, REALSET1;
schemes NAT_1, FUNCT_1, FUNCT_2, FINSEQ_1, FRAENKEL, POLYNOM2, INT_2,
ALGSEQ_1, RECDEF_1;
begin :: Preliminaries
theorem neNat1: :: neNat1:
for n being Nat holds n is non empty iff n = 1 or n > 1
proof let n be Nat;
hereby assume n is non empty; then n <> 0; then 0 < n by NAT_1:19; then
0+1 <= n by NAT_1:38;
hence n = 1 or n > 1 by REAL_1:def 5;
end;
assume n = 1 or n > 1; then n <> 0;
hence thesis;
end;
theorem SumFS: :: SumFS:
for f being FinSequence of NAT
st for i being Nat st i in dom f holds f.i <> 0
holds Sum f = len f iff f = (len f) |-> 1
proof let f be FinSequence of NAT;
defpred P[Nat] means
for f being FinSequence of NAT
st len f = $1 &
for i being Nat st i in dom f holds f.i <> 0
holds Sum f = len f iff f = (len f) |-> 1;
BA: P[0] proof let f be FinSequence of NAT such that
A: len f = 0 and for i being Nat st i in dom f holds f.i <> 0;
f = {} by A, FINSEQ_1:25; then
B: f = <*>REAL;
hereby assume Sum f = len f;
thus f = {} by A, FINSEQ_1:25 .= (len f) |-> 1 by A, FINSEQ_2:72;
end;
assume f = (len f) |-> 1;
thus Sum f = len f by A, B, RVSUM_1:102;
end;
IS: for n being Nat st P[n] holds P[n+1] proof let n be Nat; assume
A: P[n];
let f be FinSequence of NAT such that
B: len f = n+1 and
D: for i being Nat st i in dom f holds f.i <> 0;
len f <> 0 by B;
then consider g being FinSequence of NAT, a being Nat such that
E: f = g^<*a*> by FINSEQ_2:22;
Ea: g is FinSequence of REAL by FINSEQ_2:27;
n+1 = len g + len <*a*> by B, E, FINSEQ_1:35; then
n+1 = len g + 1 by FINSEQ_1:57; then
F: len g = n by XCMPLX_1:2;
G: now let i be Nat; assume
A1: i in dom g;
dom g c= dom f by E, FINSEQ_1:39; then
B1: i in dom f by A1;
f.i = g.i by A1, E, FINSEQ_1:def 7;
hence g.i <> 0 by B1, D;
end;
I: Sum f = Sum g + a by E, Ea, RVSUM_1:104;
J: len f in Seg len f by B, FINSEQ_1:6;
K: dom f = Seg len f by FINSEQ_1:def 3;
f.len f = a by E, F, B, FINSEQ_1:59; then
a <> 0 by J, K, D; then 0 < a by NAT_1:19; then
L: 0+1 <= a by NAT_1:38;
hereby assume A1: Sum f = len f;
reconsider h = (len g) |-> (1 qua Real) as FinSequence of REAL;
X1: len h = len g by FINSEQ_2:69;
Z1: h is Element of (len h)-tuples_on REAL by FINSEQ_2:110;
Y1: g is Element of (len g)-tuples_on REAL by Ea, FINSEQ_2:110;
now let j be Nat; assume
A2: j in Seg len g; then
j in dom g by FINSEQ_1:def 3; then
g.j <> 0 by G; then 0 < g.j by NAT_1:19;
then 0+1 <= g.j by NAT_1:38;
hence h.j <= g.j by A2, FINSEQ_2:70;
end; then
E1: Sum h <= Sum g by Z1, Y1, X1, RVSUM_1:112;
F1: Sum h = n*1 by F, RVSUM_1:110 .= n;
G1: Sum g = Sum g +a -a by XCMPLX_1:26 .= n+1 -a by B, I, A1; then
n <= n+1-a by E1, F1; then
n+a <= n+1-a+a by AXIOMS:24; then
n+a <= n+1 by XCMPLX_1:27; then
a <= 1 by REAL_1:53; then
D1: a = 1 by L, AXIOMS:21; then
Sum g = len g by F, G1, XCMPLX_1:26; then
g = (len g) |-> 1 by F, G, A;
hence f = (len f) |-> 1 by D1, B, E, F, FINSEQ_2:74;
end;
assume f = (len f) |-> 1; then
f = (n |-> 1)^(1 |-> 1) by B, FINSEQ_2:143
.= (n |-> 1)^<*1*> by FINSEQ_2:73; then
A1: g = (len g) |-> 1 & a = 1 by E, F, FINSEQ_2:20;
B1: Sum g = len g by F, G, A1, A;
thus Sum f = len f by A1, I, B, B1, F;
end;
for n being Nat holds P[n] from Ind(BA, IS);
hence thesis;
end;
:: Stolen from POLYNOM2
scheme IndFinSeq0 { F() -> FinSequence, P[set, set]} :
for i being Nat st 1 <= i & i <= len F() holds P[i, F().i]
provided
A1: P[1, F().1] and
A2: for i being Nat st 1 <= i & i < len F()
holds P[i, F().i] implies P[i+1, F().(i+1)]
proof
defpred Q[Nat] means 1 <= $1 & $1 <= len F() & not(P[$1, F().($1)]);
assume not(for i being Nat st 1 <= i & i <= len F() holds P[i, F().i]);
then A3: ex k being Nat st Q[k];
consider k being Nat such that
A4: Q[k] & for k' being Nat st Q[k'] holds k <= k' from Min(A3);
per cases;
suppose k = 1;
hence thesis by A1,A4;
suppose A5: k <> 1;
1 - 1 <= k - 1 by A4,REAL_1:49;
then reconsider k' = k - 1 as Nat by INT_1:16;
A6: (k - 1) + 1 = (k + (-1)) + 1 by XCMPLX_0:def 8
.= k + ((-1) + 1) by XCMPLX_1:1
.= k + 0;
A7: k' <= k' + 1 by NAT_1:29;
k' <> k' + 1
proof
assume A8: k' = k' + 1;
(k' + 1) - k' = (k' + 1) + (-k') by XCMPLX_0:def 8
.= 1 + (k' + (-k')) by XCMPLX_1:1
.= 1 + 0 by XCMPLX_0:def 6;
hence thesis by A8,XCMPLX_1:14;
end;
then A9: k' < k by A6,A7,REAL_1:def 5;
then A10: not(Q[k']) by A4;
1 < k by A4,A5,REAL_1:def 5;
then A11: 1 <= k' by A6,NAT_1:38;
k' < len F() by A4,A9,AXIOMS:22;
hence thesis by A2,A4,A6,A10,A11;
end;
theorem thsum2: :: thsum2:
for L be add-associative right_zeroed right_complementable (non empty LoopStr),
r be FinSequence of L
st len r >= 2 & for k being 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 LoopStr), r being FinSequence of L such that
A: len r >= 2 and
B: for k being Nat st 2 < k & k in dom r holds r.k = 0.L;
now assume r is empty; then r = <*>(the carrier of L);
then len r = 0 by FINSEQ_1:32;
hence contradiction by A;
end; then
consider a being Element of L, r1 being FinSequence of L such that
D: a = r.1 and
E: r = <*a*>^r1 by FSM_1:5;
Eb: len <*a*> = 1 by FINSEQ_1:57; then
Ea: len r = 1 + len r1 by E, FINSEQ_1:35;
now assume r1 is empty; then r1 = <*>(the carrier of L);
then len r1 = 0 by FINSEQ_1:32;
hence contradiction by A, Ea;
end; then
consider b being Element of L, r2 being FinSequence of L such that
F: b = r1.1 and
G: r1 = <*b*>^r2 by FSM_1:5;
Ga: len <*b*> = 1 by FINSEQ_1:57;
H: now let i be Nat such that
A1: i in dom r2;
B1: 1+i in dom r1 by A1, G, Ga, FINSEQ_1:41;
1 <= i by A1, FINSEQ_3:27; then 1 < 1+i by NAT_1:38; then
C1: 1+1 < 1+(1+i) by REAL_1:67;
D1: 1+(1+i) in dom r by B1, Eb, E, FINSEQ_1:41;
thus r2.i = r1.(1+i) by A1, Ga, G, FINSEQ_1:def 7
.= r.(1+(1+i)) by B1, Eb, E, FINSEQ_1:def 7 .= 0.L by C1, D1, B;
end; 1 <= len r by A, AXIOMS:22; then
I: 1 in dom r by FINSEQ_3:27;
J: 2 in dom r by A, FINSEQ_3:27;
K: r.2 = r1.(2-1) by E, Eb, A, FINSEQ_1:37 .= r1.1;
thus Sum r = a + Sum r1 by E, FVSUM_1:89
.= a + (b + Sum r2) by G, FVSUM_1:89 .= a + (b + 0.L) by H, POLYNOM3:1
.= a+b by RLVECT_1:def 7 .= r/.1 + b by I, D, FINSEQ_4:def 4
.= r/.1 + r/.2 by J, K, F, FINSEQ_4:def 4;
end;
begin :: Canonical ordering of a finite set into a finite sequence
definition
let A be finite set;
func canFS(A) -> FinSequence of A means :LCFS:
len it = card A &
ex f being FinSequence st len f = card A &
(f.1 = [choose A, A \ {choose A}] or card A = 0) &
(for i being Nat st 1 <= i & i < card A
for x being set
st f.i = x holds f.(i+1) = [choose x`2, x`2 \ {choose x`2}]) &
for i being Nat st i in dom it holds it.i = (f.i)`1;
existence proof set cA = card A;
defpred P[Nat,Function,Function] means
for x being set
st $2 = x holds $3 = [choose x`2, x`2 \ {choose x`2}];
P1: for n being Nat st 1 <= n & n < cA
for x being set ex y being set st P[n,x,y] proof
let n be Nat such that 1 <= n and n < cA;
let x be set; take y = [choose x`2, x`2 \ {choose x`2}]; thus thesis;
end;
P2: for n being Nat st 1 <= n & n < cA
for x,y1,y2 being set st P[n,x,y1] & P[n,x,y2] holds y1 = y2 proof
let n be Nat such that 1 <= n and n < cA; let x,y1,y2 be set such that
C1: P[n,x,y1] and D1: P[n,x,y2];
thus y1 = [choose x`2, x`2 \ {choose x`2}] by C1 .= y2 by D1;
end;
consider f being FinSequence such that
A: len f = cA and
B: f.1 = [choose A, A \ {choose A}] or cA = 0 and
C: for n being Nat st 1<=n&n<cA holds P[n,f.n,f.(n+1)] from FinRecEx(P1, P2);
defpred R[Nat,set] means
$1 in dom f implies $2 in [: A, bool A :] &
ex X being finite set st X = ($2)`2 & card X +$1 = cA;
R1: R[1,f.1] proof assume 1 in dom f; then 0+1 <= len f by FINSEQ_3:27; then
0 < len f by NAT_1:38; then
C1: cA <> 0 by A; then A <> {} by CARD_1:78; then
B1: choose A in A;
A \ {choose A} c= A by XBOOLE_1:36; then A \ {choose A} in bool A;
hence f.1 in [: A, bool A :] by C1, B, B1, ZFMISC_1:def 2;
reconsider X = A \ {choose A} as finite set;
take X; thus X = (f.1)`2 by C1, B, MCART_1:7;
E1: now assume choose A in A \ {choose A};
then not choose A in {choose A} by XBOOLE_0:def 4;
hence contradiction by TARSKI:def 1;
end;
{choose A} c= A by B1, ZFMISC_1:37; then
A = {choose A} \/ (A \ {choose A}) by XBOOLE_1:45;
hence card X + 1 = cA by E1, CARD_2:54;
end;
R2: for i being Nat st 1 <= i & i < len f & R[i, f.i] holds R[i+1,f.(i+1)]
proof let i be Nat such that
A1: 1 <= i and
B1: i < len f and
C1: R[i, f.i] and i+1 in dom f; i <= len f by B1; then
E1: i in dom f by A1,FINSEQ_3:27; then
F1: f.i in [: A, bool A :] by C1;
consider X being finite set such that
G1: X = (f.i)`2 and
H1: card X +i = cA by E1, C1;
H1a: X <> {} by H1, B1, A, CARD_1:78;
consider a, ba being set such that a in A and
J1: ba in bool A and
K1: f.i = [a, ba] by F1, ZFMISC_1:def 2;
L1: f.(i+1) = [choose (f.i)`2, (f.i)`2 \ {choose (f.i)`2}] by A,A1,B1,C;
M1: (f.i)`1 = a & (f.i)`2 = ba by K1, MCART_1:7;
M1a: (f.i)`2 c= A by M1, J1;
P1: choose (f.i)`2 in (f.i)`2 by H1a, G1; then
N1: choose (f.i)`2 in A by M1a;
(f.i)`2 \ {choose (f.i)`2} c= (f.i)`2 by XBOOLE_1:36; then
(f.i)`2 \ {choose (f.i)`2} c= A by M1a, XBOOLE_1:1; then
(f.i)`2 \ {choose (f.i)`2} in bool A;
hence f.(i+1) in [: A, bool A :] by N1, L1, ZFMISC_1:def 2;
reconsider XX = (f.i)`2 \{choose(f.i)`2} as finite set by G1, FINSET_1:16;
take XX; thus XX = (f.(i+1))`2 by L1, MCART_1:7;
R1: now assume choose (f.i)`2 in (f.i)`2 \ {choose (f.i)`2};
then not choose (f.i)`2 in {choose (f.i)`2} by XBOOLE_0:def 4;
hence contradiction by TARSKI:def 1;
end;
{choose (f.i)`2} c= (f.i)`2 by P1, ZFMISC_1:37; then
(f.i)`2 = {choose (f.i)`2} \/ ((f.i)`2 \ {choose (f.i)`2})
by XBOOLE_1:45;
then card X = card XX + 1 by R1, G1, CARD_2:54;
then card X +i = card XX + 1 + i;
hence card XX + (i+1) = cA by H1, XCMPLX_1:1;
end;
R3: for i being Nat st 1<=i & i <= len f holds R[i,f.i]from IndFinSeq0(R1, R2);
rng f c= [: A, bool A :] proof let y be set; assume y in rng f; then
consider i being Nat such that
A1: i in dom f and
B1: y = f.i by FINSEQ_2:11; 1 <= i & i <= len f by A1, FINSEQ_3:27;
hence thesis by B1, A1, R3;
end; then reconsider f as FinSequence of [: A, bool A :] by FINSEQ_1:def 4;
deffunc F(Nat) = (f.$1)`1;
consider p being FinSequence such that
D: len p = card A and
E: for k being Nat st k in Seg card A holds p.k = F(k) from SeqLambda;
F: dom p = Seg card A by D, FINSEQ_1:def 3;
G: dom p = dom f by D, A, FINSEQ_3:31;
rng p c= A proof let y be set; assume y in rng p; then
consider i being Nat such that
A1: i in dom p and
B1: p.i = y by FINSEQ_2:11;
E1: p.i = (f.i)`1 by A1, F, E;
f.i in [:A, bool A:] by A1,G,FINSEQ_2:13; then(f.i)`1 in A by MCART_1:10;
hence y in A by B1, E1;
end; then reconsider p as FinSequence of A by FINSEQ_1:def 4;
take p; thus len p = card A by D;
take f; thus thesis by A, B, C, E, F;
end;
uniqueness proof let it1, it2 be FinSequence of A such that
A1: len it1 = card A; given f being FinSequence such that
B1a: len f = card A and
B1: f.1 = [choose A, A \ {choose A}] or card A = 0 and
C1: for i being Nat st 1 <= i & i < card A
holds for x being set
st f.i = x holds f.(i+1) = [choose x`2, x`2 \ {choose x`2}] and
D1: for i being Nat st i in dom it1 holds it1.i = (f.i)`1;
assume
A2: len it2 = card A; given g being FinSequence such that
B2a: len g = card A and
B2: g.1 = [choose A, A \ {choose A}] or card A = 0 and
C2: for i being Nat st 1 <= i & i < card A
holds for x being set
st g.i = x holds g.(i+1) = [choose x`2, x`2 \ {choose x`2}] and
D2: for i being Nat st i in dom it2 holds it2.i = (g.i)`1;
defpred Q[Nat,set] means card A <> 0 implies $2 = g.$1;
Q1: Q[1, f.1] by B1, B2;
Q2: for i being Nat st 1 <= i & i < len f & Q[i, f.i] holds Q[i+1, f.(i+1)]
proof let i be Nat such that
A3: 1 <= i and
B3: i < len f and
D3: Q[i, f.i] and
E3: card A <> 0; set x = f.i;
thus f.(i+1) = [choose x`2, x`2 \ {choose x`2}] by B1a, A3, B3, C1
.= g.(i+1) by E3, D3, A3, B3, B1a, C2;
end;
Q3: for i being Nat st 1<=i & i<=len f holds Q[i, f.i] from IndFinSeq0(Q1,Q2);
E2: f = g proof
per cases;
suppose S1: card A = 0;
thus f = {} by S1, B1a, FINSEQ_1:25 .= g by S1, B2a, FINSEQ_1:25;
suppose S1: card A <> 0;
now let j be Nat; assume j in Seg len f;
then j in dom f by FINSEQ_1:def 3; then
1 <= j & j <= len f by FINSEQ_3:27;
hence f.j = g.j by S1, Q3;
end;
hence f = g by B1a, B2a, FINSEQ_2:10;
end;
now let j be Nat such that
A3: j in Seg card A;
B3: dom it1 = dom it2 by A1, A2, FINSEQ_3:31;
C3: dom it1 = Seg card A by A1, FINSEQ_1:def 3;
thus it1.j = (f.j)`1 by D1, C3, A3 .= it2.j by E2, D2, A3, B3, C3;
end;
hence it1 = it2 by A1, A2, FINSEQ_2:10;
end;
end;
theorem CFS0: :: CFS0:
for A being finite set holds canFS(A) is one-to-one
proof let A be finite set;
set F = canFS(A), cA = card A;
A: len F = card A by LCFS;
consider f being FinSequence such that
B: len f = cA and
C: f.1 = [choose A, A \ {choose A}] or card A = 0 and
D: for i being Nat st 1 <= i & i < cA
for x being set
st f.i = x holds f.(i+1) = [choose x`2, x`2 \ {choose x`2}] and
E: for i being Nat st i in dom F holds F.i = (f.i)`1 by LCFS;
per cases;
suppose A = {}; then card A = 0 by CARD_1:78; then F = {} by A, FINSEQ_1:25;
hence canFS(A) is one-to-one;
suppose S1: A <> {}; then
Z: card A <> 0 by GRAPH_5:5; then card A > 0 by NAT_1:19; then
Y: 0+1 <= len F by A, NAT_1:38;
X: 1 in dom F by Y, FINSEQ_3:27;
defpred P[Nat, set] means
rng (F| Seg $1) /\ ($2)`2 = {} &
(ex X being finite set st X = ($2)`2 & card X +$1 = cA) &
($1 < len F implies not F.($1+1) in rng (F| Seg $1));
P1: P[1, f.1] proof
B1: choose A in A by S1;
reconsider F1 = (F | Seg 1) as FinSequence of A by FINSEQ_1:23;
1 <= len F by X, FINSEQ_3:27; then
consider a being Element of A such that
C1b: F1 = <* a *> by S1, QC_LANG4:7;
C1a: len F1 = 1 by C1b, FINSEQ_1:56;
1 in Seg (0+1) by FINSEQ_1:6; then
F1.1 = F.1 by FUNCT_1:72 .= (f.1)`1 by X, E
.= choose A by Z, C, MCART_1:7; then
F | Seg 1 = <* choose A *> by C1a, FINSEQ_1:57; then
D1: rng (F| Seg 1) = {choose A} by FINSEQ_1:56;
E1: (f.1)`2 = A \ {choose A} by Z, C, MCART_1:7;
thus rng (F| Seg 1) /\ (f.1)`2 = {} proof assume not thesis; then
consider x being set such that
A2: x in rng (F| Seg 1) /\ (f.1)`2 by XBOOLE_0:def 1;
x in {choose A} & x in (f.1)`2 by A2, D1, XBOOLE_0:def 3;
hence contradiction by E1, XBOOLE_0:def 4;
end;
now reconsider X = A \ {choose A} as finite set;
take X; thus X = (f.1)`2 by C, Z, MCART_1:7;
E1: now assume choose A in A \ {choose A};
then not choose A in {choose A} by XBOOLE_0:def 4;
hence contradiction by TARSKI:def 1;
end;
{choose A} c= A by B1, ZFMISC_1:37; then
A = {choose A} \/ (A \ {choose A}) by XBOOLE_1:45;
hence card X + 1 = cA by E1, CARD_2:54;
end;
hence ex X being finite set st X = (f.1)`2 & card X +1 = cA; then
consider X being finite set such that
H1: X = (f.1)`2 and
I1: card X +1 = cA;
J1: 1 < len F implies (f.1)`2 <> {} by H1, CARD_1:78, I1, A;
assume
Aa: 1 < len F; then 1+1 <= len F by NAT_1:38; then
1+1 in dom F by FINSEQ_3:27; then
A2: F.2 = (f.2)`1 by E;
f.(1+1) = [choose (f.1)`2, (f.1)`2 \ {choose (f.1)`2}]
by Aa, A, D; then
C2: (f.(1+1))`1 = choose (A \ {choose A}) by E1, MCART_1:7;
thus not F.(1+1) in rng (F| Seg 1)
by A2,C2,D1,Aa,J1,E1,XBOOLE_0:def 4;
end;
P2: for i being Nat st 1 <= i & i < len f & P[i, f.i] holds P[i+1, f.(i+1)]
proof let i be Nat such that
A1: 1 <= i and
B1: i < len f and
C1: P[i, f.i];
D1: rng (F| Seg i) /\ (f.i)`2 = {} by C1;
consider X being finite set such that
G1: X = (f.i)`2 and
H1: card X +i = cA by C1;
L1: f.(i+1) = [choose (f.i)`2, (f.i)`2 \ {choose (f.i)`2}] by A1,B1,B,D;
M1: (f.i)`2 is non empty by H1, G1, B1, B, CARD_1:78;
{choose (f.i)`2} c= (f.i)`2 by M1, ZFMISC_1:37; then
M1a: (f.i)`2={choose (f.i)`2}\/((f.i)`2 \ {choose (f.i)`2}) by XBOOLE_1:45;
N1: i+1 <= len F by B1, A, B, NAT_1:38;
1 <= i+1 by NAT_1:37; then
N1a: i+1 in dom F by N1, FINSEQ_3:27;
reconsider Fi = F| Seg i, Fi1 = F| Seg (i+1) as FinSequence of A
by FINSEQ_1:23;
consider a being Element of A such that
O1: Fi1 = Fi^<*a*> by N1, S1, QC_LANG4:6;
P1: rng Fi1 = rng Fi \/ rng <*a*> by O1, FINSEQ_1:44
.= rng Fi \/ {a} by FINSEQ_1:56;
i+1 in Seg (i+1) by FINSEQ_1:6; then
P1a: F.(i+1) = Fi1.(i+1) by FUNCT_1:72;
i = len Fi by B1, A, B, FINSEQ_1:21; then
Fi1.(i+1) = a by O1, FINSEQ_1:59; then
R1: a = F.(i+1) by P1a .= (f.(i+1))`1 by N1a, E
.= choose (f.i)`2 by L1, MCART_1:7;
T1: (f.(i+1))`2 = (f.i)`2 \ {a} by L1, R1, MCART_1:7;
thus
Z1: rng (F| Seg (i+1)) /\ (f.(i+1))`2 = {} proof assume not thesis;
then consider x being set such that
A2: x in (rng Fi \/ {a}) /\ ((f.i)`2 \ {a}) by P1, T1, XBOOLE_0:def 1;
x in (rng Fi \/ {a}) & x in ((f.i)`2 \ {a}) by A2, XBOOLE_0:def 3; then
(x in rng Fi or x in {a}) & (x in (f.i)`2 & not x in {a})
by XBOOLE_0:def 2, XBOOLE_0:def 4; then
(x in rng Fi) & x in (f.i)`2; then
x in rng (F| Seg i) /\ (f.i)`2 by XBOOLE_0:def 3;
hence contradiction by D1;
end;
now reconsider XX = (f.i)`2 \{choose(f.i)`2} as finite set
by G1,FINSET_1:16;
take XX; thus XX = (f.(i+1))`2 by L1, MCART_1:7;
now assume choose (f.i)`2 in (f.i)`2 \ {choose (f.i)`2};
then not choose (f.i)`2 in {choose (f.i)`2} by XBOOLE_0:def 4;
hence contradiction by TARSKI:def 1;
end;
then card X = card XX + 1 by M1a, G1, CARD_2:54;
then card X +i = card XX + 1 + i;
hence card XX + (i+1) = cA by H1, XCMPLX_1:1;
end;
hence
V1: ex X being finite set st X = (f.(i+1))`2 & card X +(i+1) = cA;
assume
A2: i+1 < len F; consider X being finite set such that
V2: X = (f.(i+1))`2 and
W2: card X +(i+1) = cA by V1;
U1: (f.(i+1))`2 <> {} by V2, CARD_1:78, W2, A2, A;
B2: 1 <= i+1 by NAT_1:37; set i1 = i+1;
D2: 1 <= i1+1 by NAT_1:37; i1+1 <= len F by A2, NAT_1:38; then
i1+1 in dom F by D2, FINSEQ_3:27; then
G2: F.(i1+1) = (f.(i1+1))`1 by E;
f.(i1+1) = [choose (f.i1)`2, (f.i1)`2 \ {choose (f.i1)`2}]
by A2,B2,A,D; then
I2: (f.(i1+1))`1 = choose (f.i1)`2 by MCART_1:7;
assume
K2: F.((i+1)+1) in rng (F| Seg (i+1));
choose (f.i1)`2 in (f.i1)`2 by U1; then
choose (f.i1)`2 in (rng Fi1 /\ (f.i1)`2) by K2, G2, I2, XBOOLE_0:def 3;
hence contradiction by Z1;
end;
P3: for i being Nat st 1<=i & i<=len f holds P[i, f.i] from IndFinSeq0(P1,P2);
thus canFS(A) is one-to-one proof let i, j be set such that
H: i in dom F and
I: j in dom F and
J: F.i = F.j;
Fd: dom F = Seg len F by FINSEQ_1:def 3;
per cases;
suppose i = j;
hence thesis;
suppose S1: i <> j; reconsider i, j as Nat by H, I, FINSEQ_3:25;
K: 1 <= i & i <= len F by H, FINSEQ_3:27;
L: 1 <= j & j <= len F by I, FINSEQ_3:27;
now
per cases by S1, REAL_1:def 5;
suppose S2: i < j; j <> 0 by L; then consider j1 being Nat such that
A2: j = j1+1 by NAT_1:22;
B2: j1 < len F by L, A2, NAT_1:38;
C2: j1 <= len F by B2; i+1 <= j by S2, NAT_1:38; then
C2b: i <= j1 by A2, REAL_1:53; then 1 <= j1 by K, AXIOMS:22; then
D2: not F.(j1+1) in rng (F|Seg j1) by B2, P3, A, B;
E2: i in Seg j1 by K, C2b, FINSEQ_1:3;
F2: (F|Seg j1).i = F.i by E2, FUNCT_1:72;
Seg j1 c= dom F by C2, Fd, FINSEQ_1:7; then
dom (F|Seg j1) = Seg j1 by RELAT_1:91; then
i in dom (F|Seg j1) by E2; then F.i in rng (F|Seg j1) by F2, FUNCT_1:12;
hence contradiction by D2, A2, J;
suppose S2: i > j;
i <> 0 by K; then
consider i1 being Nat such that
A2: i = i1+1 by NAT_1:22;
B2: i1 < len F by K, A2, NAT_1:38;
C2: i1 <= len F by B2; j+1 <= i by S2, NAT_1:38; then
C2b: j <= i1 by A2, REAL_1:53; then 1 <= i1 by L, AXIOMS:22; then
D2: not F.(i1+1) in rng (F|Seg i1) by B2, P3, A, B;
E2: j in Seg i1 by L, C2b, FINSEQ_1:3;
F2: (F|Seg i1).j = F.j by E2, FUNCT_1:72;
Seg i1 c= dom F by C2, Fd, FINSEQ_1:7; then
dom (F|Seg i1)=Seg i1 by RELAT_1:91; then j in dom (F|Seg i1) by E2;then
F.j in rng (F|Seg i1) by F2, FUNCT_1:12;
hence contradiction by D2, A2, J;
end;
hence thesis;
end;
end;
theorem CFS1: :: CFS1:
for A being finite set holds rng canFS(A) = A
proof let A be finite set; set F = canFS(A), cA = card A;
A: len F = card A by LCFS;
consider f being FinSequence such that
B: len f = cA and
C: f.1 = [choose A, A \ {choose A}] or card A = 0 and
D: for i being Nat st 1 <= i & i < cA
for x being set
st f.i = x holds f.(i+1) = [choose x`2, x`2 \ {choose x`2}] and
E: for i being Nat st i in dom F holds F.i = (f.i)`1 by LCFS;
per cases;
suppose S1: A = {}; then card A = 0 by CARD_1:78; then
F = {} by A, FINSEQ_1:25;
hence thesis by S1, FINSEQ_1:27;
suppose S1: A <> {}; then
Z: card A <> 0 by GRAPH_5:5; then card A > 0 by NAT_1:19; then
Y: 0+1 <= len F by A, NAT_1:38;
X: 1 in dom F by Y, FINSEQ_3:27;
defpred P[Nat, set] means
rng (F| Seg $1) \/ ($2)`2 = A &
ex X being finite set st X = ($2)`2 & card X +$1 = cA;
P1: P[1, f.1] proof
B1: choose A in A by S1;
reconsider F1 = (F | Seg 1) as FinSequence of A by FINSEQ_1:23;
1 <= len F by X, FINSEQ_3:27; then
consider a being Element of A such that
C1b: F1 = <* a *> by S1, QC_LANG4:7;
C1a: len F1 = 1 by C1b, FINSEQ_1:56; 1 in Seg (0+1) by FINSEQ_1:6; then
F1.1 = F.1 by FUNCT_1:72
.= (f.1)`1 by X, E .= choose A by Z, C, MCART_1:7; then
F | Seg 1 = <* choose A *> by C1a, FINSEQ_1:57; then
D1: rng (F| Seg 1) = {choose A} by FINSEQ_1:56;
E1: (f.1)`2 = A \ {choose A} by Z, C, MCART_1:7;
{choose A} c= A by B1, ZFMISC_1:37;
hence rng (F| Seg 1) \/ (f.1)`2 = A by D1, E1, XBOOLE_1:45;
reconsider X = A \ {choose A} as finite set;
take X; thus X = (f.1)`2 by C, Z, MCART_1:7;
E1: now assume choose A in A \ {choose A};
then not choose A in {choose A} by XBOOLE_0:def 4;
hence contradiction by TARSKI:def 1;
end;
{choose A} c= A by B1, ZFMISC_1:37; then
A = {choose A} \/ (A \ {choose A}) by XBOOLE_1:45;
hence card X + 1 = cA by E1, CARD_2:54;
end;
P2: for i being Nat st 1 <= i & i < len f & P[i, f.i] holds P[i+1, f.(i+1)]
proof let i be Nat such that
A1: 1 <= i and
B1: i < len f and
C1: P[i, f.i];
D1: rng (F| Seg i) \/ (f.i)`2 = A by C1;
consider X being finite set such that
G1: X = (f.i)`2 and
H1: card X +i = cA by C1;
L1: f.(i+1) = [choose (f.i)`2, (f.i)`2 \ {choose (f.i)`2}] by A1,B1,B,D;
M1: (f.i)`2 is non empty by H1, G1, B1, B, CARD_1:78;
{choose (f.i)`2} c= (f.i)`2 by M1, ZFMISC_1:37; then
M1a: (f.i)`2 = {choose (f.i)`2} \/ ((f.i)`2 \ {choose (f.i)`2})
by XBOOLE_1:45;
N1: i+1 <= len F by B1, A, B, NAT_1:38;
1 <= i+1 by NAT_1:37; then
N1a: i+1 in dom F by N1, FINSEQ_3:27;
reconsider Fi = F| Seg i, Fi1 = F| Seg (i+1) as FinSequence of A
by FINSEQ_1:23;
consider a being Element of A such that
O1: Fi1 = Fi^<*a*> by N1, S1, QC_LANG4:6;
P1: rng Fi1 = rng Fi \/ rng <*a*> by O1, FINSEQ_1:44
.= rng Fi \/ {a} by FINSEQ_1:56;
i+1 in Seg (i+1) by FINSEQ_1:6; then
P1a: F.(i+1) = Fi1.(i+1) by FUNCT_1:72;
i = len Fi by B1, A, B, FINSEQ_1:21; then
Fi1.(i+1) = a by O1, FINSEQ_1:59; then
R1: a = F.(i+1) by P1a .= (f.(i+1))`1 by N1a, E
.= choose (f.i)`2 by L1, MCART_1:7;
T1: (f.(i+1))`2 = (f.i)`2 \ {a} by L1, R1, MCART_1:7;
rng Fi1 \/ (f.(i+1))`2
= rng Fi \/ ({a} \/ ((f.i)`2 \ {a})) by T1, P1, XBOOLE_1:4;
hence rng (F| Seg (i+1)) \/ (f.(i+1))`2 = A by M1a, D1, R1;
reconsider XX = (f.i)`2 \{choose(f.i)`2} as finite set by G1, FINSET_1:16;
take XX;
thus XX = (f.(i+1))`2 by L1, MCART_1:7;
now assume choose (f.i)`2 in (f.i)`2 \ {choose (f.i)`2};
then not choose (f.i)`2 in {choose (f.i)`2} by XBOOLE_0:def 4;
hence contradiction by TARSKI:def 1;
end;
then card X = card XX + 1 by M1a, G1, CARD_2:54;
then card X +i = card XX + 1 + i;
hence card XX + (i+1) = cA by H1, XCMPLX_1:1;
end;
P3: for i being Nat st 1<=i & i<=len f holds P[i, f.i] from IndFinSeq0(P1,P2);
now assume len F < 1; then len F = 0 by RLVECT_1:98;
hence contradiction by S1, A, GRAPH_5:5;
end; then
F: 1 <= len F;
G: F = F | (Seg len F) by FINSEQ_3:55;
H: rng F \/ (f.len F)`2 = A by F, G, A, B, P3;
consider X being finite set such that
I: X = (f.len F)`2 and
J: card X + len f = cA by F, A, B, P3;
card X = 0 by J, B, XCMPLX_1:3; then
X = {} by GRAPH_5:5; then
X c= rng F by XBOOLE_1:2;
hence rng canFS(A) = A by H, I, XBOOLE_1:12;
end;
theorem CFS2: :: CFS2:
for a being set holds canFS({a}) = <* a *>
proof let a be set;
A: len canFS({a}) = card {a} by LCFS .= 1 by CARD_1:79;
rng canFS({a}) = {a} by CFS1;
hence canFS({a}) = <* a *> by A, FINSEQ_1:56;
end;
theorem CFS3: :: CFS3:
for A being finite set holds (canFS A)" is Function of A, Seg card A
proof let A be finite set;
A: canFS A is one-to-one by CFS0;
len canFS A = card A by LCFS; then
C: dom canFS A = Seg card A by FINSEQ_1:def 3;
rng canFS A = A by CFS1; then
D: dom ((canFS A)") = A by A, FUNCT_1:55;
rng ((canFS A)") = Seg card A by A, C, FUNCT_1:55;
hence (canFS A)" is Function of A, Seg card A by D, FUNCT_2:3;
end;
begin :: More about bags
definition
let X be set, S be finite Subset of X, n be Nat;
func (S, n)-bag -> Element of Bags X equals :BAG2:
(EmptyBag X) +* (S --> n);
correctness proof
set b = (EmptyBag X) +* (S --> n);
E: dom (S --> n) = S by FUNCOP_1:19;
D: EmptyBag X = (X --> 0) by POLYNOM1:def 15;
C: dom b = dom (EmptyBag X) \/ dom (S --> n) by FUNCT_4:def 1
.= X \/ dom (S --> n) by D, FUNCOP_1:19 .= X \/ S by FUNCOP_1:19
.= X by XBOOLE_1:12;
rng (EmptyBag X) c= {0} & rng (S-->n) c= {n} by D, FUNCOP_1:19; then
F: rng (EmptyBag X) \/ rng (S --> n) c= {0} \/ {n} by XBOOLE_1:13;
G: {0} c= NAT by ZFMISC_1:37;
H: {n} c= NAT by ZFMISC_1:37;
I: {0} \/ {n} c= NAT by G, H, XBOOLE_1:8;
rng b c= rng (EmptyBag X) \/ rng (S --> n) by FUNCT_4:18; then
rng b c= {0} \/ {n} by F, XBOOLE_1:1; then
rng b c= NAT by I, XBOOLE_1:1 ; then
A: b is natural-yielding by SEQM_3:def 8;
J: now let i be set such that
A: not i in S;
thus b.i = (EmptyBag X).i by A, E, FUNCT_4:12 .= 0 by POLYNOM1:56;
end;
K: now let i be set such that A: i in S;
thus b.i = (S --> n).i by A, E, FUNCT_4:14 .= n by A, FUNCOP_1:13;
end;
support b is finite proof
per cases;
suppose S1: S is empty;
now assume support b is non empty; then consider x being set such that
A1: x in support b by XBOOLE_0:def 1;
b.x <> 0 by A1, POLYNOM1:def 7; then x in S by J;
hence contradiction by S1;
end;
hence support b is finite;
suppose S1: S is non empty & n = 0;
now assume support b is non empty; then consider x being set such that
A1: x in support b by XBOOLE_0:def 1;
C1: b.x <> 0 by A1, POLYNOM1:def 7; then
B1: x in S by J; then
b.x = (S-->n).x by E, FUNCT_4:14 .= 0 by S1, B1, FUNCOP_1:13;
hence contradiction by C1;
end;
hence support b is finite;
suppose A: S is non empty & n <> 0;
for x being set holds x in S iff b.x <> 0 by A, J, K;
then support b = S by POLYNOM1:def 7;
hence support b is finite;
end; then
b is finite-support by POLYNOM1:def 8;
then (EmptyBag X) +* (S --> n) is bag of X by A, C, PBOOLE:def 3;
hence (EmptyBag X) +* (S --> n) is Element of Bags X by POLYNOM1:def 14;
end;
end;
Snbagdom:
for X being set, S being finite Subset of X, n being Nat
holds dom (S, n)-bag = X by PBOOLE:def 3;
theorem Snbag0: :: Snbag0:
for X being set, S being finite Subset of X, n being Nat, i being set
st not i in S holds (S, n)-bag.i = 0
proof let X be set, S be finite Subset of X, n be Nat, i be set such that
A: not i in S;
B: dom (S --> n) = S by FUNCOP_1:19;
(S, n)-bag = (EmptyBag X) +* (S --> n) by BAG2;
hence (S, n)-bag.i = (EmptyBag X).i by A, B, FUNCT_4:12 .= 0 by POLYNOM1:56;
end;
theorem Snbag1: :: Snbag1:
for X being set, S being finite Subset of X, n being 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 Nat, i be set such that
A: i in S;
B: dom (S --> n) = S by FUNCOP_1:19;
(S, n)-bag = (EmptyBag X) +* (S --> n) by BAG2;
hence (S, n)-bag.i = (S --> n).i by A, B, FUNCT_4:14 .= n by A, FUNCOP_1:13;
end;
theorem Snbagsup: :: Snbagsup:
for X being set, S being finite Subset of X, n being Nat
st n <> 0 holds support (S, n)-bag = S
proof let X be set, S be finite Subset of X, n be Nat; assume n <> 0; then
for x being set holds x in S iff (S, n)-bag.x <> 0 by Snbag0, Snbag1;
hence support (S, n)-bag = S by POLYNOM1:def 7;
end;
theorem :: Snbage: :: :: Snbage:
for X being set, S being finite Subset of X, n being 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 Nat such that
A: S is empty or n = 0;
now let i be set; assume i in X;
per cases;
suppose S1: i in S; then n = 0 by A;
hence (S, n)-bag.i = 0 by S1, Snbag1 .= (EmptyBag X).i by POLYNOM1:56;
suppose not i in S;
hence (S, n)-bag.i = 0 by Snbag0 .= (EmptyBag X).i by POLYNOM1:56;
end;
hence (S, n)-bag = EmptyBag X by PBOOLE:3;
end;
theorem Snbagsum: :: Snbagsum:
for X being set, S, T being finite Subset of X, n being 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 Nat; assume
S misses T; then
AA: S /\ T = {} by XBOOLE_0:def 7;
now let i be set such that i in X;
per cases by XBOOLE_0:def 2;
suppose
B: not i in S \/ T; then
C: not i in S & not i in T by XBOOLE_0:def 2;
thus (S \/ T, n)-bag.i = 0 by B, Snbag0 .= (S,n)-bag.i + 0 by C, Snbag0
.= (S,n)-bag.i + (T,n)-bag.i by C, Snbag0
.= ((S,n)-bag + (T,n)-bag).i by POLYNOM1:def 5;
suppose
B: i in S; then
C: i in S \/ T by XBOOLE_0:def 2;
D: not i in T by B, AA, XBOOLE_0:def 3;
thus (S \/ T, n)-bag.i = n by C, Snbag1
.= (S,n)-bag.i + 0 by B, Snbag1 .= (S,n)-bag.i +(T,n)-bag.i by D, Snbag0
.= ((S,n)-bag + (T,n)-bag).i by POLYNOM1:def 5;
suppose
B: i in T; then
C: i in S \/ T by XBOOLE_0:def 2;
D: not i in S by B, AA, XBOOLE_0:def 3;
thus (S \/ T, n)-bag.i = n by C, Snbag1 .= (T,n)-bag.i + 0 by B, Snbag1
.= (S,n)-bag.i + (T,n)-bag.i by D, Snbag0
.= ((S,n)-bag + (T,n)-bag).i by POLYNOM1:def 5;
end;
hence (S \/ T, n)-bag = (S,n)-bag + (T,n)-bag by PBOOLE:3;
end;
definition
let A be set, b be bag of A;
func degree b -> Nat means :LBAGDEG:
ex f being FinSequence of NAT st it = Sum f & f = b*canFS(support b);
existence proof set cS = canFS(support b);
set f = b*cS;
A: rng b c= NAT by SEQM_3:def 8;
Aa: support b c= dom b by POLYNOM1:41; rng cS = support b by CFS1;
then rng cS c= dom b by Aa; then dom f = dom cS by RELAT_1:46;
then dom f = Seg len cS by FINSEQ_1:def 3; then
B: f is FinSequence by FINSEQ_1:def 2;
rng f c= rng b by RELAT_1:45; then rng f c= NAT by A, XBOOLE_1:1; then
reconsider f as FinSequence of NAT by B, FINSEQ_1:def 4;
take S = Sum f; thus thesis;
end;
uniqueness;
end;
theorem BAGDEG0: :: BAGDEG0:
for A being set, b being bag of A holds b = EmptyBag A iff degree b = 0
proof let A be set, b be bag of A;
set cS = canFS(support b);
hereby assume b = EmptyBag A; then support b = {} by BAGORDER:19; then
len cS = 0 by LCFS, CARD_1:78; then cS = <*>NAT by FINSEQ_1:32; then
D1: b*cS = <*>NAT by RELAT_1:62; set f = <*>NAT; Sum f = 0 by RVSUM_1:102;
hence degree b = 0 by D1, LBAGDEG;
end;
assume A: degree b = 0;
consider f being FinSequence of NAT such that
B: degree b = Sum f and
C: f = b*canFS(support b) by LBAGDEG;
now assume
A1: support b <> {}; f is FinSequence of REAL by FINSEQ_2:27; then
B1: f is Element of (len f)-tuples_on REAL by FINSEQ_2:110;
C1: for i be Nat st i in dom f holds 0 <= f.i by NAT_1:18;
now consider x being set such that
A2: x in support b by A1, XBOOLE_0:def 1;
x in rng cS by A2, CFS1; then consider i being Nat such that
B2: i in dom cS and
C2: cS.i = x by FINSEQ_2:11;
support b c= dom b by POLYNOM1:41; then x in dom b by A2; then
E2: i in dom f by B2, C2, C, FUNCT_1:21;
f.i = b.(cS.i) by B2, C, FUNCT_1:23; then
f.i <> 0 by A2, C2, POLYNOM1:def 7; then 0 < f.i by NAT_1:19;
hence ex i being Nat st i in dom f & 0 < f.i by E2;
end; then
0 < Sum f by C1, B1, RVSUM_1:115;
hence contradiction by A, B;
end;
hence b = EmptyBag A by BAGORDER:20;
end;
theorem BAGDEG1: :: BAGDEG1:
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;
A: rng cS = S by CFS1;
B: dom b = A by PBOOLE:def 3; then rng cS c= dom b by A; then
C: dom f = dom cS by RELAT_1:46; then
D: dom f = Seg len cS by FINSEQ_1:def 3; then
reconsider f as FinSequence by FINSEQ_1:def 2;
Da: len cS = card S by LCFS;
E: rng cS = S by CFS1;
F: len cS = len f by C, FINSEQ_3:31;
rng f c= NAT proof let y be set; assume y in rng f; then
consider x being set such that
A1: x in dom f and
B1: y = f.x by FUNCT_1:def 5;
C1: cS.x in dom b by A1, FUNCT_1:21;
D1: rng b c= NAT by SEQM_3:def 8;
f.x = b.(cS.x) by A1, FUNCT_1:22; then f.x in rng b by C1, FUNCT_1:12;
hence y in NAT by B1, D1;
end; then reconsider f as FinSequence of NAT by FINSEQ_1:def 4;
hereby assume that
C1: S = support b and
D1: degree b = card S;
consider F being FinSequence of NAT such that
E1: degree b = Sum F and
F1: F = b*cS by C1, LBAGDEG;
G1: len F = card S by F1, Da, F;
now let i be Nat; assume
A2: i in dom F; then
B2: F.i = b.(cS.i) by F1, FUNCT_1:22;
i in dom cS by A2, F1, C; then cS.i in rng cS by FUNCT_1:12;
hence F.i <> 0 by A, C1, B2, POLYNOM1:def 7;
end; then
H1: F = len F |-> 1 by G1, E1, D1, SumFS;
set sb = (S, 1)-bag;
G1: support b = support sb by C1, Snbagsup;
now
thus dom b = dom sb by B, Snbagdom;
let x be set; assume x in dom b;
per cases;
suppose S1: x in support b;
F2: cS is one-to-one by CFS0;
E2: rng cS = support b by A, C1; then
D2: cS".x in dom cS by S1, F2, FUNCT_1:54;
B2: cS".x in Seg len F by C, F1, D2, FINSEQ_1:def 3;
C2: cS.(cS".x) = x by S1, E2, F2, FUNCT_1:57;
thus b.x = b.(cS.(cS".x)) by C2 .= F.(cS".x) by F1, D2, FUNCT_1:23
.= 1 by B2, H1, FINSEQ_2:70 .= sb.x by S1, C1, Snbag1;
suppose S1: not x in support b;
hence b.x = 0 by POLYNOM1:def 7 .= sb.x by S1, G1, POLYNOM1:def 7;
end;
hence b = (S, 1)-bag by FUNCT_1:9;
end;
assume
A1: b = (S, 1)-bag;
hence
C1: S = support b by Snbagsup;
D1: degree b = Sum f by C1, LBAGDEG; set g = (card S) |-> 1;
now
thus len f = card S by C, Da, FINSEQ_3:31;
thus len g = card S by FINSEQ_2:69;
let i be Nat; assume
D1: i in Seg card S;
E1: cS.i in S by D1, C, D, Da, E, FUNCT_1:12;
thus f.i = b.(cS.i) by D, Da, D1, FUNCT_1:22
.= 1 by A1, E1, Snbag1 .= g.i by D1, FINSEQ_2:70;
end; then f = g by FINSEQ_2:10;
hence degree b = (card S)*1 by D1, RVSUM_1:110 .= card S;
end;
theorem BAGDEG2c: :: BAGDEG2c:
for A being set, S being finite Subset of A, b being bag of A
st support b c= S
ex f being FinSequence of NAT st f = b*canFS(S) & degree b = Sum f
proof let A be set, S be finite Subset of A, b be bag of A such that
A: support b c= S; set cS = canFS(S); set f = b*cS;
len cS = card S by LCFS; then
B: dom cS = Seg card S by FINSEQ_1:def 3;
C: rng cS = S by CFS1;
Ca: cS is one-to-one by CFS0;
D: dom b = A by PBOOLE:def 3; then
E: dom f = Seg card S by B, C, RELAT_1:46; then
reconsider f as FinSequence by FINSEQ_1:def 2;
F: rng b c= NAT by SEQM_3:def 8;
rng f c= rng b by RELAT_1:45; then rng f c= NAT by F, XBOOLE_1:1; then
reconsider f as FinSequence of NAT by FINSEQ_1:def 4;
take f; thus f = b*canFS(S);
set cs = canFS(support b);
Ga: cs is one-to-one by CFS0;
consider g being FinSequence of NAT such that
G: degree b = Sum g and
H: g = b*cs by LBAGDEG; len cs = card support b by LCFS; then
Hb: dom cs = Seg card support b by FINSEQ_1:def 3;
Hc: rng cs = support b by CFS1; support b c= A by A, XBOOLE_1:1; then
Hd: dom g = Seg card support b by H, Hb, Hc, D, RELAT_1:46; then
Ha: len g = card support b by FINSEQ_1:def 3;
I: card support b <= card S by A, CARD_1:80;
per cases by I, REAL_1:def 5;
suppose
SU: card support b < card S; then consider d being Nat such that
J: card S = (card support b) + d and 1 <= d by FSM_1:1;
set h = d |-> (0 qua Real);
Kb: len h = d by FINSEQ_2:69; then
Kc: dom h = Seg d by FINSEQ_1:def 3;
reconsider gr = g, fr = f as FinSequence of REAL by FINSEQ_2:27;
set F = gr^h;
len F = len g + len h by FINSEQ_1:35 .= card S by J, Kb, Ha; then
Ka: dom F = Seg card S by FINSEQ_1:def 3;
set dd = {j where j is Nat : j in dom f & f.j = 0};
M: now support b <> S by SU; then consider x being set such that
B1: not (x in support b iff x in S) by TARSKI:2;
x in support b implies x in S by A; then
C1: not x in support b & x in S by B1; then consider j being set such that
D1: j in dom cS and
E1: cS.j = x by C, FUNCT_1:def 5;
reconsider j as Nat by D1, FINSEQ_3:25; f.j =b.x by D1, E1, FUNCT_1:23;
then f.j = 0 by C1, POLYNOM1:def 7; then j in dd by D1, B, E;
hence dd is non empty;
end;
L: dd c= dom f proof let x be set; assume x in dd; then
ex j being Nat st x = j & j in dom f & f.j = 0;
hence thesis;
end; then
reconsider dd as finite non empty set by M, FINSET_1:13;
rng canFS(dd) = dd & dd c= NAT by CFS1, L, E, XBOOLE_1:1; then
reconsider cdd = canFS(dd) as FinSequence of NAT by FINSEQ_1:def 4;
set cdi = cdd";
reconsider cdi as Function of dd, Seg card dd by CFS3;
reconsider cadd = card dd as non empty Nat by GRAPH_5:5;
V: Seg cadd <> {} & Seg card dd c= NAT; then
reconsider cdi as Function of dd, NAT by FUNCT_2:9;
set cSr = cS | (dom f \ dd);
Ub: cSr is one-to-one by Ca, FUNCT_1:84;
dom f \ dd c= dom f by XBOOLE_1:36; then
(dom f \ dd) /\ dom f = dom f \ dd by XBOOLE_1:28; then
Uc: dom cSr = (dom f \ dd) by B, E, FUNCT_1:68;
now let y be set;
hereby assume y in rng cSr; then consider x being set such that
A1: x in dom cSr and
B1: y = cSr.x by FUNCT_1:def 5;
C1: x in dom cS & x in dom f \ dd by A1, RELAT_1:86; then
reconsider j = x as Nat by FINSEQ_3:25;
D1: cSr.x = cS.x by A1, FUNCT_1:70;
not j in dd by C1, XBOOLE_0:def 4; then
f.j <> 0 by C1, B, E; then
b.(cS.j) <> 0 by C1, FUNCT_1:23;
hence y in support b by B1, D1, POLYNOM1:def 7;
end;
assume A1: y in support b; then y in S by A; then
consider x being set such that
B1: x in dom cS and
C1: y = cS.x by C, FUNCT_1:def 5;
now assume x in dd; then consider j being Nat such that
A2: j = x and
B2: j in dom f and
C2: f.j = 0;
0 = b.(cS.j) by C2, B2, B, E, FUNCT_1:23;
hence contradiction by A1, A2, C1, POLYNOM1:def 7;
end; then x in dom f \ dd by B1, B, E, XBOOLE_0:def 4;
hence y in rng cSr by B1, C1, FUNCT_1:73;
end; then
rng cSr = support b by TARSKI:2; then
support b, dom f \dd are_equipotent by Ub, Uc, WELLORD2:def 4; then
Ua: card support b = card (dom f \ dd) by CARD_1:81;
card (dom f \ dd) = card dom f - card dd by L, CARD_2:63; then
card (dom f \ dd) = card S - card dd by E, FINSEQ_1:78; then
card support b + card dd = card S - card dd + card dd by Ua; then
card support b + card dd = card S by XCMPLX_1:27; then
U: card dd = d by J, XCMPLX_1:2;
len cdd = card dd by LCFS; then
Va: dom cdd = Seg d by U, FINSEQ_1:def 3;
Vb: rng cdd = dd by CFS1;
Vc: dom cdi = dd by FUNCT_2:def 1;
Vd: cdd is one-to-one by CFS0; then
Ve: cdi is one-to-one by FUNCT_1:62;
Vf: rng cdi = Seg d by Vd, Va, FUNCT_1:55;
deffunc Z(set) = cdi /. $1 + card support b;
consider z being Function such that
R: dom z = dd and
S: for x being set st x in dd holds z.x = Z(x) from Lambda;
Sa: rng z c= Seg card S proof let y be set; assume y in rng z; then
consider x being set such that
A1: x in dom z and
B1: y = z.x by FUNCT_1:def 5;
C1: y = cdi/.x + card support b by A1, R, S, B1;
E1: cdi/.x = cdi.x by A1, R, Vc, FINSEQ_4:def 4;
cdi.x in Seg d by Vf, A1, R, Vc, FUNCT_1:12; then
1 <= cdi/.x & cdi/.x <= d by E1, FINSEQ_1:3; then
1 <= cdi/.x + card support b &
cdi/.x + card support b <= d + card support b by NAT_1:37, AXIOMS:24;
then cdi/.x + card support b in Seg card S by J, FINSEQ_1:3;
hence thesis by C1;
end;
set p = cs"*cS +* z;
Tc: dom p = dom (cs"*cS) \/ dom z by FUNCT_4:def 1;
Tb: now assume dom (cs"*cS) /\ dom z <> {}; then
consider x being set such that
A1: x in dom (cs"*cS) /\ dom z by XBOOLE_0:def 1;
B1: x in dom (cs"*cS) & x in dom z by A1, XBOOLE_0:def 3;
then consider j being Nat such that
C1: j = x and j in dom f and
E1: f.j = 0 by R;
H1: dom (cs") = support b by Hc, Ga, FUNCT_1:55;
j in dom cS by B1, C1, FUNCT_1:21; then
f.j = b.(cS.j) by FUNCT_1:23; then
not cS.j in support b by E1, POLYNOM1:def 7;
hence contradiction by C1, B1, H1, FUNCT_1:21;
end;
now let x be set;
hereby assume S1: x in dom (cs"*cS) \/ dom z;
per cases by S1, XBOOLE_0:def 2;
suppose x in dom (cs"*cS); then x in dom cS by FUNCT_1:21;
hence x in dom F by Ka, B;
suppose x in dom z;
hence x in dom F by L, Ka, E, R;
end;
assume
A1: x in dom F; then reconsider i = x as Nat by FINSEQ_3:25;
per cases;
suppose f.x = 0; then i in dom z by R, A1, Ka, E;
hence x in dom (cs"*cS) \/ dom z by XBOOLE_0:def 2;
suppose S1: f.x <> 0;
B1: i in dom cS by A1, Ka, B; then
C1: f.i = b.(cS.i) by FUNCT_1:23;
cS.i in support b by S1, C1, POLYNOM1:def 7; then
cS.i in rng cs by Hc; then cS.i in dom (cs") by Ga, FUNCT_1:55;
then i in dom (cs"*cS) by B1, FUNCT_1:21;
hence x in dom (cs"*cS) \/ dom z by XBOOLE_0:def 2;
end; then
Ta: dom (cs"*cS) \/ dom z = dom F by TARSKI:2; then
T: dom p = dom F by FUNCT_4:def 1;
now let x be set such that
A1: x in dom F;
per cases by A1, Ta, XBOOLE_0:def 2;
suppose S1: x in dom (cs"*cS);
not x in dom z by S1, Tb, XBOOLE_0:def 3; then
K1: p.x = (cs"*cS).x by FUNCT_4:12;
(cs"*cS).x in rng (cs"*cS) by S1, FUNCT_1:12; then
(cs"*cS).x in rng (cs") by FUNCT_1:25; then
(cs"*cS).x in dom cs by Ga, FUNCT_1:55; then
L1: (cs"*cS).x in Seg card support b by Hb;
Seg card support b c= Seg card S by I, FINSEQ_1:7;
hence p.x in dom F by K1, L1, Ka;
suppose S1: x in dom z; then
B1: p.x = z.x by FUNCT_4:14; z.x in rng z by S1, FUNCT_1:12;
hence p.x in dom F by B1, Ka, Sa;
end; then
reconsider p as Function of dom F, dom F by T, FUNCT_2:5;
Na: p is one-to-one proof let a, c be set such that
A1: a in dom p and
B1: c in dom p and
C1: p.a = p.c;
D1: (a in dom (cs"*cS) or a in dom z) by A1, Tc, XBOOLE_0:def 2;
E1: (c in dom (cs"*cS) or c in dom z) by B1, Tc, XBOOLE_0:def 2;
per cases by D1, E1;
suppose S1: a in dom (cs"*cS) & c in dom (cs"*cS);
not a in dom z by S1, Tb, XBOOLE_0:def 3; then
K1: p.a = (cs"*cS).a by FUNCT_4:12 .= cs".(cS.a) by S1, FUNCT_1:22;
not c in dom z by S1, Tb, XBOOLE_0:def 3; then
L1: p.c = (cs"*cS).c by FUNCT_4:12 .= cs".(cS.c) by S1, FUNCT_1:22;
M1: cs.(cs".(cS.a)) = cs.(cs".(cS.c)) by C1, K1, L1;
cS.a in dom (cs") by S1, FUNCT_1:21; then
cS.a in rng cs by Ga, FUNCT_1:55; then
N1: cs.(cs".(cS.a)) = cS.a by Ga, FUNCT_1:57;
cS.c in dom (cs") by S1, FUNCT_1:21; then
cS.c in rng cs by Ga, FUNCT_1:55; then
cs.(cs".(cS.c)) = cS.c by Ga, FUNCT_1:57; then
O1: cS".(cS.a) = cS".(cS.c) by N1, M1;
a in dom cS by S1, FUNCT_1:21; then
P1: cS".(cS.a) = a by Ca, FUNCT_1:56;
c in dom cS by S1, FUNCT_1:21; then
cS".(cS.c) = c by Ca, FUNCT_1:56;
hence a = c by O1, P1;
suppose S1: a in dom (cs"*cS) & c in dom z;
K1: p.c = z.c by S1, FUNCT_4:14 .= cdi /. c + card support b by S1, R, S;
not a in dom z by S1, Tb, XBOOLE_0:def 3; then
L1: p.a = (cs"*cS).a by FUNCT_4:12 .= cs".(cS.a) by S1, FUNCT_1:22;
cS.a in dom (cs") by S1, FUNCT_1:21; then
cs".(cS.a) in rng (cs") by FUNCT_1:12; then
M1: cs".(cS.a) in dom cs by Ga, FUNCT_1:55; then
reconsider ccc = cs".(cS.a) as Nat by FINSEQ_3:25;
cdi /. c + card support b <= 0+card support b
by C1, K1, L1, M1, Hb, FINSEQ_1:3; then
N1: cdi /. c <= 0 by REAL_1:53; cdi /. c >= 0 by NAT_1:18; then
P1: cdi /. c = 0 by N1; then
O1: cdi.c = 0 by S1, R, Vc, FINSEQ_4:def 4;
cdi.c in rng cdi by S1, R, Vc, FUNCT_1:12; then
1 <= cdi/.c by O1, Vf, FINSEQ_1:3;
hence a = c by P1;
suppose S1: a in dom z & c in dom (cs"*cS);
K1: p.a = z.a by S1, FUNCT_4:14 .= cdi /. a + card support b by S1, R, S;
not c in dom z by S1, Tb, XBOOLE_0:def 3; then
L1: p.c = (cs"*cS).c by FUNCT_4:12 .= cs".(cS.c) by S1, FUNCT_1:22;
cS.c in dom (cs") by S1, FUNCT_1:21; then
cs".(cS.c) in rng (cs") by FUNCT_1:12; then
M1: cs".(cS.c) in dom cs by Ga, FUNCT_1:55; then
reconsider ccc = cs".(cS.c) as Nat by FINSEQ_3:25;
cdi /. a + card support b <= 0+card support b
by C1, K1, L1, M1, Hb, FINSEQ_1:3; then
N1: cdi /. a <= 0 by REAL_1:53; cdi /. a >= 0 by NAT_1:18; then
P1: cdi /. a = 0 by N1; then
O1: cdi.a = 0 by S1, R, Vc, FINSEQ_4:def 4;
cdi.a in rng cdi by S1, R, Vc, FUNCT_1:12; then
1 <= cdi/.a by O1, Vf, FINSEQ_1:3;
hence a = c by P1;
suppose S1: a in dom z & c in dom z;
K1: p.a = z.a by S1, FUNCT_4:14 .= cdi /. a + card support b by S1, R, S;
L1: p.c = z.c by S1, FUNCT_4:14 .= cdi /. c + card support b by S1, R, S;
O1: cdi /. a = cdi /. c by K1, L1, C1, XCMPLX_1:2;
cdi /. a = cdi . a & cdi /. c = cdi . c by S1,Vc,R,FINSEQ_4:def 4;
hence a = c by Ve, S1, Vc, R, O1, FUNCT_1:def 8;
end;
now let x be set;
hereby assume x in rng p; then consider a being set such that
A1: a in dom p and
B1: x = p.a by FUNCT_1:def 5;
per cases by A1, FUNCT_4:13;
suppose S1: a in dom (cs"*cS);
not a in dom z by S1, Tb, XBOOLE_0:def 3; then
C1: p.a = (cs"*cS).a by FUNCT_4:12 .= cs".(cS.a) by S1, FUNCT_1:22;
cS.a in dom (cs") by S1, FUNCT_1:21; then
cs".(cS.a) in rng (cs") by FUNCT_1:12; then
D1: cs".(cS.a) in dom cs by Ga, FUNCT_1:55;
dom cs c= dom F by I, Ka, Hb, FINSEQ_1:7;
hence x in dom F by D1, C1, B1;
suppose S1: a in dom z; then
C1: z.a in rng z by FUNCT_1:12; p.a = z.a by S1, FUNCT_4:14;
hence x in dom F by B1, Ka, Sa, C1;
end;
assume A1: x in dom F; then reconsider j = x as Nat by FINSEQ_3:25;
per cases by A1, FINSEQ_1:38;
suppose j in dom gr; then
B1: j in dom cs by Hb, Hd; then
H1: cs.j in support b by Hc, FUNCT_1:12; then
F1: cs.j in S by A; then
E1: cS".(cs.j) in Seg card S by B, Ca, C, FUNCT_1:54; then
C1: cS".(cs.j) in dom p by T, Ka;
G1: cs.j in dom (cS*cS") by Ca, C, F1, FUNCT_1:59;
now assume
A2: cS".(cs.j) in dom z;
(b*cS).(cS".(cs.j)) = b.(cS.(cS".(cs.j))) by E1, B, FUNCT_1:23
.= b.(cs.j) by F1, C, Ca, FUNCT_1:57; then
B2: f.(cS".(cs.j)) <> 0 by H1, POLYNOM1:def 7;
ex k being Nat st k = cS".(cs.j) & k in dom f & f.k = 0 by A2, R;
hence contradiction by B2;
end; then p.(cS".(cs.j)) = (cs"*cS).(cS".(cs.j)) by FUNCT_4:12
.= cs".(cS.(cS".(cs.j))) by E1, B, FUNCT_1:23
.= cs".((cS*cS").(cs.j)) by G1, FUNCT_1:22
.= cs".(cs.j) by F1, C, Ca, FUNCT_1:57 .= (cs"*cs).j by B1, FUNCT_1:23
.= j by B1, Ga, FUNCT_1:56;
hence x in rng p by C1, FUNCT_1:12;
suppose ex n being Nat st n in dom h & j=len gr + n; then
consider n being Nat such that
A1: n in dom h and
B1: j = len gr + n;
D1: cdd.n in dd by A1, Va, Vb, Kc, FUNCT_1:12; then
cdd.n in dom f by L; then
C1: cdd.n in dom p by Ka, E, T;
p.(cdd.n) = z.(cdd.n) by D1, R, FUNCT_4:14
.= cdi /. (cdd.n) + card support b by D1, S
.= cdi.(cdd.n) + card support b by D1, Vc, FINSEQ_4:def 4
.= n + card support b by A1, Va, Kc, Vd, FUNCT_1:56 .= j by B1, Ha;
hence x in rng p by C1, FUNCT_1:12;
end; then
Nc: rng p = dom F by TARSKI:2; then p is onto by FUNCT_2:def 3; then
N: p is Permutation of dom F by Na, FUNCT_2:def 4;
Pc: dom (F*p) = dom F by T, Nc, RELAT_1:46; then
Pa: dom f = dom (F*p) by Ka, E;
now let x be set; assume
A1: x in dom f;
per cases;
suppose S1: f.x = 0;
reconsider j = x as Nat by A1, FINSEQ_3:25;
B1: j in dom z by A1, S1, R; then
C1: p.x = z.x by FUNCT_4:14 .= cdi /. x + card support b by B1, S, R;
p.x in dom F by T, A1, Pc, Pa, Nc, FUNCT_1:12; then
reconsider px = p.x as Nat by FINSEQ_3:25;
dom cdi = dd by FUNCT_2:def 1; then
E1: cdi /. x = cdi.x by B1, R, FINSEQ_4:def 4;
cdi.x in Seg card dd by V, B1, R, FUNCT_2:7; then
D1: cdi /. x in dom h by E1, Kc, U;
reconsider cdix = cdi /. x as Nat;
thus f.x = h.(cdix) by Kc, S1, D1, FINSEQ_2:70
.= F.px by C1, Ha, D1, FINSEQ_1:def 7 .= (F*p).x by A1, Pa, FUNCT_1:22;
suppose S1: f.x <> 0;
B1: now assume x in dd; then ex j being Nat st j=x & j in dom f & f.j = 0;
hence contradiction by S1;
end; f.x = b.(cS.x) by A1, FUNCT_1:22; then
cS.x in support b by S1, POLYNOM1:def 7; then
C1: cS.x in rng cs by CFS1; then
D1: cs".(cS.x) in dom cs by Ga, FUNCT_1:54;
E1: cS.x = cs.(cs".(cS.x)) by C1, Ga, FUNCT_1:54;
F1: p.x = (cs"*cS).x by R, B1, FUNCT_4:12
.= cs".(cS.x) by A1, B, E, FUNCT_1:23; then
G1: p.x in dom g by D1, Hd, Hb; then
reconsider px = p.x as Nat by FINSEQ_3:25;
thus f.x = b.(cS.x) by A1, FUNCT_1:22
.= b.(cs.px) by E1, F1 .= g.(px) by H, D1, F1, FUNCT_1:23
.= F.(px) by G1, FINSEQ_1:def 7 .= (F*p).x by A1, Pa, FUNCT_1:22;
end; then
P: f = F*p by Pa, FUNCT_1:9;
R: addreal is commutative associative & addreal has_a_unity by RVSUM_1:5,6,7;
O: Sum F = addreal $$ F by RVSUM_1:def 10
.= addreal $$ fr by P, R, N, FINSOP_1:8 .= Sum f by RVSUM_1:def 10;
Sum h = 0 by RVSUM_1:111;
then Sum gr = Sum gr + Sum h .= Sum F by RVSUM_1:105;
hence degree b = Sum f by O, G;
suppose card support b = card S; then support b = S by A, TRIANG_1:3;
hence degree b = Sum f by G, H;
end;
theorem BAGDEG2: :: BAGDEG2:
for A being set, b, b1, b2 being bag of A
st b = b1 + b2 holds degree b = degree b1 + degree b2
proof let A be set, b, b1, b2 be bag of A; assume
A: b = b1 + b2;
consider f being FinSequence of NAT such that
B: degree b = Sum f and
C: f = b*canFS(support b) by LBAGDEG; set S = support b;
Z: dom b = A & dom b1 = A & dom b2 = A by PBOOLE:def 3;
S c= dom b by POLYNOM1:41; then reconsider S as finite Subset of A by Z;
D: S = support b1 \/ support b2 by A, POLYNOM1:42;
then support b1 c= S by XBOOLE_1:7; then
consider f1r being FinSequence of NAT such that
I: f1r = b1*canFS(S) and
J: degree b1 = Sum f1r by BAGDEG2c; support b2 c= S by D, XBOOLE_1:7; then
consider f2r being FinSequence of NAT such that
K: f2r = b2*canFS(S) and
L: degree b2 = Sum f2r by BAGDEG2c;
rng f c= NAT & rng f1r c= NAT & rng f2r c= NAT by FINSEQ_1:def 4; then
rng f c= REAL & rng f1r c= REAL & rng f2r c= REAL by XBOOLE_1:1; then
reconsider f,f1r,f2r as FinSequence of REAL by FINSEQ_1:def 4;
set cS = canFS S; rng cS = S by CFS1; then
O: dom f = dom cS & dom f1r = dom cS & dom f2r = dom cS
by Z, C, I, K, RELAT_1:46; then
N: len f1r = len f2r & len f1r = len f by FINSEQ_3:31;
now let k be Nat such that
A1: k in dom f1r;
B1: f1r/.k = f1r.k by A1, FINSEQ_4:def 4 .= b1.(cS.k) by A1, I, FUNCT_1:22;
C1: f2r/.k = f2r.k by A1, O, FINSEQ_4:def 4
.= b2.(cS.k) by A1, K, O, FUNCT_1:22;
f.k = b.(cS.k) by A1, C, O, FUNCT_1:22;
hence f.k = f1r/.k + f2r/.k by B1, C1, A, POLYNOM1:def 5;
end; then
Sum f = (Sum f1r) + Sum f2r by N, INTEGRA1:23;
hence degree b = degree b1 + degree b2 by B, J, L;
end;
theorem Permprod: :: GROUP_4:18 but about a different Product
for L being associative commutative unital (non empty HGrStr),
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 HGrStr),
f, g be FinSequence of L, p be Permutation of dom f such that
A: g = f * p; set mL = (the mult of L);
B: mL is commutative by MONOID_0:def 11;
C: mL is associative by GROUP_1:31;
D: mL has_a_unity by GROUP_1:34;
thus Product(g) = (the mult of L) $$ g by FVSUM_1:def 9
.= (the mult of L) $$ f by A, B, C, D, FINSOP_1:8
.= Product(f) by FVSUM_1:def 9;
end;
begin :: More on polynomials
definition
let L be non empty ZeroStr, p be Polynomial of L;
attr p is non-zero means :LNZ:
p <> 0_. L;
end;
theorem lenNZ: :: lenNZ
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 by LNZ;
then len p <> 0 by POLYNOM4:8;
hence len p > 0 by NAT_1:19;
end;
assume len p > 0; then p <> 0_. L by POLYNOM4:6;
hence p is non-zero by LNZ;
end;
definition
let L be non trivial (non empty ZeroStr);
cluster non-zero Polynomial of L;
existence proof
consider a being Element of (the carrier of L)\{0.L};
the carrier of L is non trivial by REALSET1:def 13;
then (the carrier of L)\{0.L} is non empty by REALSET1:32;
then A1: a in the carrier of L & not(a in {0.L}) by XBOOLE_0:def 4;
then reconsider a as Element of L;
take p = <%a%>;
p.0 = a & (0_. L).0 = 0.L by POLYNOM3:28, POLYNOM5:33; then
p <> 0_. L by A1, TARSKI:def 1;
hence thesis by LNZ;
end;
end;
definition
let L be non degenerated non empty multLoopStr_0, x be Element of L;
cluster <%x, 1_ L%> -> non-zero;
correctness proof 0.L <> 1_ L by VECTSP_1:def 21;
then len <%x, 1_ L%> = 2 by POLYNOM5:41;
hence thesis by lenNZ;
end;
end;
theorem LC1:
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 consider k being Nat such that
B: len p = k+1 by NAT_1:22;
len p = (len p -'1)+1 by B, BINARITH:39;
hence p.(len p -'1) <> 0.L by ALGSEQ_1:25;
end;
theorem plen1: :: plen1:
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
A: len p = 1;
thus B: p=<%p.0%> by A, ALGSEQ_1:def 6; p <> <%0.L%> by A, ALGSEQ_1:31;
hence p.0 <> 0.L by B;
end;
theorem P4Th5: :: P4Th5: 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 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 Nat st k in dom r holds r.k = p.(k-'1) * (0_. L).(i+1-'k)
by POLYNOM3:def 11;
now let k be 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 POLYNOM3:28 .= 0.L by VECTSP_1:36;
end;
hence (p*'(0_.(L))).i = 0.L by A1,POLYNOM3:1 .= (0_.(L)).i by POLYNOM3:28;
end;
hence thesis by FUNCT_2:113;
end;
definition
cluster algebraic-closed add-associative right_zeroed right_complementable
Abelian commutative associative distributive domRing-like
non degenerated (well-unital (non empty doubleLoopStr));
existence proof take F_Complex; thus thesis; end;
end;
theorem pintdom: :: pintdom:
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
A: p*'q = 0_. L and
B: p <> 0_. L and
C: q <> 0_. L;
Ba: len p <> 0 by B, POLYNOM4:8; then consider lp1 being Nat such that
D: len p = lp1+1 by NAT_1:22; len q <> 0 by C, POLYNOM4:8;
then consider lq1 being Nat such that
E: len q = lq1+1 by NAT_1:22;
F: p.lp1 <> 0.L & q.lq1 <> 0.L by D, E, ALGSEQ_1:25;
set lpq = lp1 + lq1;
consider r being FinSequence of L such that
G: len r = lpq+1 and
H: (p*'q).lpq = Sum r and
I: for k be Nat st k in dom r holds r.k=p.(k-'1)*q.(lpq+1-'k)
by POLYNOM3:def 11; len p <= lp1+1+lq1 by D, NAT_1:37; then
len p <= lp1+(1+lq1) by XCMPLX_1:1; then
N: len p <= lp1+lq1+1 by XCMPLX_1:1; 0 < len p by Ba, NAT_1:19; then
M: 0+1 <= len p by NAT_1:38;
J: len p in dom r by M, N, G, FINSEQ_3:27;
K: lpq+1-'len p = lq1+(lp1+1)-'len p by XCMPLX_1:1 .= lq1 by D, BINARITH:39;
now let k be Nat such that
A1: k in dom r and
B1: k <> len p;
C1: r.k = p.(k-'1) * q.(lpq+1-'k) by A1, I;
per cases by B1, REAL_1:def 5;
suppose k < len p; then consider d being Nat such that
D1: len p = k+d & 1 <= d by FSM_1:1;
lpq+1 = lq1 +len p by D, XCMPLX_1:1; then
E1: lpq+1-'k = lq1+d+k-'k by D1, XCMPLX_1:1 .= lq1+d by BINARITH:39;
len q <= lq1+d by D1, E, AXIOMS:24;
hence r.k = p.(k-'1)*0.L by C1, E1, ALGSEQ_1:22 .= 0.L by VECTSP_1:36;
suppose k > len p; then k >= len p + 1 by NAT_1:38; then
k-'1 >= len p + 1-'1 by JORDAN3:5; then k-'1 >= len p by BINARITH:39;
hence r.k = 0.L * q.(lpq+1-'k) by C1, ALGSEQ_1:22 .= 0.L by VECTSP_1:39;
end;
then Sum r = r.(len p) by J, MATRIX_3:14
.= p.(len p -'1)*q.(lpq+1-'len p) by J,I.= p.lp1 * q.lq1 by K,D,BINARITH:39;
then Sum r <> 0.L by F, VECTSP_2:def 5;
hence contradiction by A, H, POLYNOM3:28;
end;
definition
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 12;
Z: 0_. L = 0.PRL by POLYNOM3:def 12;
assume x*y = 0.PRL; then xp*'yp = 0_. L by Z, POLYNOM3:def 12;
hence x = 0.PRL or y = 0.PRL by Z, pintdom;
end;
end;
definition
let L be domRing, p, q be non-zero Polynomial of L;
cluster p*'q -> non-zero;
correctness proof p <> 0_. L & q <> 0_. L by LNZ;
then p*'q <> 0_. L by pintdom;
hence thesis by LNZ;
end;
end;
theorem :: pcomring0:
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 set;
assume A: x in Roots p \/ Roots q;
per cases by A, XBOOLE_0:def 2;
suppose B: x in Roots p; then reconsider a = x as Element of L;
a is_a_root_of p by B, POLYNOM5:def 9; then
eval(p,a) = 0.L by POLYNOM5:def 6; then
eval(p,a) * eval(q,a) = 0.L by VECTSP_1:39; then
eval(p*'q,a) = 0.L by POLYNOM4:27; then
a is_a_root_of p*'q by POLYNOM5:def 6;
hence x in Roots (p*'q) by POLYNOM5:def 9;
suppose B: x in Roots q; then reconsider a = x as Element of L;
a is_a_root_of q by B, POLYNOM5:def 9; then
eval(q,a) = 0.L by POLYNOM5:def 6; then
eval(p,a) * eval(q,a) = 0.L by VECTSP_1:36; then
eval(p*'q,a) = 0.L by POLYNOM4:27; then
a is_a_root_of p*'q by POLYNOM5:def 6;
hence x in Roots (p*'q) by POLYNOM5:def 9;
end;
theorem pdomring0: :: pdomring0:
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 set;
hereby assume
A: x in Roots (p*'q); then reconsider a = x as Element of L;
a is_a_root_of p*'q by A, POLYNOM5:def 9; then
eval(p*'q,a) = 0.L by POLYNOM5:def 6; then
eval(p,a) * eval(q,a) = 0.L by POLYNOM4:27; then
B: eval(p,a) = 0.L or eval(q,a) = 0.L by VECTSP_2:def 5;
per cases by B;
suppose eval(p,a) = 0.L; then a is_a_root_of p by POLYNOM5:def 6; then
a in Roots p by POLYNOM5:def 9;
hence x in Roots p \/ Roots q by XBOOLE_0:def 2;
suppose eval(q,a) = 0.L; then a is_a_root_of q by POLYNOM5:def 6; then
a in Roots q by POLYNOM5:def 9;
hence x in Roots p \/ Roots q by XBOOLE_0:def 2;
end;
assume A: x in Roots p \/ Roots q;
per cases by A, XBOOLE_0:def 2;
suppose B: x in Roots p; then reconsider a = x as Element of L;
a is_a_root_of p by B, POLYNOM5:def 9; then
eval(p,a) = 0.L by POLYNOM5:def 6; then
eval(p,a) * eval(q,a) = 0.L by VECTSP_1:39; then
eval(p*'q,a) = 0.L by POLYNOM4:27; then
a is_a_root_of p*'q by POLYNOM5:def 6;
hence x in Roots (p*'q) by POLYNOM5:def 9;
suppose B: x in Roots q; then reconsider a = x as Element of L;
a is_a_root_of q by B, POLYNOM5:def 9; then
eval(q,a) = 0.L by POLYNOM5:def 6; then
eval(p,a) * eval(q,a) = 0.L by VECTSP_1:36; then
eval(p*'q,a) = 0.L by POLYNOM4:27; then
a is_a_root_of p*'q by POLYNOM5:def 6;
hence x in Roots (p*'q) by POLYNOM5:def 9;
end;
hence Roots (p*'q) = Roots p \/ Roots q by TARSKI:2;
end;
theorem puminus: :: puminus:
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
A: p = pc;
set PRL = Polynom-Ring L;
reconsider mpc = -p as Element of PRL by POLYNOM3:def 12;
p+-p = p-p by POLYNOM3:def 8 .= 0_. L by POLYNOM3:30; then
pc + mpc = 0_. L by A, POLYNOM3:def 12 .= 0.PRL by POLYNOM3:def 12;
hence -p = -pc by RLVECT_1:def 10;
end;
theorem pminus: :: pminus:
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
A: p = pc and
B: q = qc;
C: -q = -qc by B, puminus;
thus p-q = p+-q by POLYNOM3:def 8 .= pc+-qc by A, C,POLYNOM3:def 12
.= pc-qc by RLVECT_1:def 11;
end;
theorem distrminus: :: distrminus:
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 12;
A: p*'q = pc*qc by POLYNOM3:def 12;
B: p*'r = pc*rc by POLYNOM3:def 12;
C: qc-rc = q-r by pminus;
thus p*'q-p*'r = pc*qc - pc*rc by A, B, pminus
.= pc*(qc-rc) by VECTSP_1:43 .= p*'(q-r) by C, POLYNOM3:def 12;
end;
theorem minus0: :: minus0:
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 12;
Z: 0_. L = 0.PRL by POLYNOM3:def 12;
assume q-r = 0_. L; then qc-rc = 0.PRL by Z,pminus; then
qc=rc by VECTSP_1:84;
hence q = r;
end;
theorem pcanc0: :: pcanc0:
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
A: p <> 0_. L;
set PRL = Polynom-Ring L;
reconsider pc = p, qc = q, rc = r as Element of PRL by POLYNOM3:def 12;
assume p*'q = p*'r; then p*'q-p*'r = p*'r-p*'r; then
p*'q-p*'r = 0_. L by POLYNOM3:30; then p*'(q-r) = 0_. L by distrminus; then
q-r = 0_. L by A, pintdom;
hence q = r by minus0;
end;
theorem pexp0: :: pexp0:
for L being domRing, n being Nat, p being Polynomial of L
st p <> 0_. L holds p`^n <> 0_. L
proof let L be domRing, n be Nat, p be Polynomial of L; assume
A: p <> 0_. L;
(1_. L).0 = 1_ L & (0_. L).0 = 0.L by POLYNOM3:28,31; then
B: 1_. L <> 0_. L by VECTSP_1:def 21;
defpred P[Nat] means p`^$1 <> 0_. L;
p`^0 = 1_. L by POLYNOM5:16; then
BA: P[0] by B;
IS: for n being Nat st P[n] holds P[n+1] proof
let n be Nat such that
A1: P[n]; p`^(n+1) = (p`^n) *' p by POLYNOM5:20;
hence P[n+1] by A1, A, pintdom;
end; for n being Nat holds P[n] from Ind(BA,IS);
hence p`^n <> 0_. L;
end;
theorem pexp1: :: pexp1:
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);
(p`^i) *' (p`^0) = (p`^i) *' 1_. L by POLYNOM5:16
.= (p`^(i+0)) by POLYNOM3:36; then
BA: P[0];
IS: for j being Nat st P[j] holds P[j+1] proof
let j be Nat such that
A: P[j];
(p`^i) *' (p`^(j+1)) = (p`^i) *' ((p`^j) *' p) by POLYNOM5:20
.= (p`^i) *' (p`^j) *' p by POLYNOM3:34 .= (p`^(i+j)) *' p by A
.= p`^(i+j+1) by POLYNOM5:20 .= p`^(i+(j+1)) by XCMPLX_1:1;
hence P[j+1];
end; for j being Nat holds P[j] from Ind(BA,IS);
hence (p`^i) *' (p`^j) = p `^(i+j);
end;
theorem poly1b: :: poly1b:
for L being non empty multLoopStr_0 holds 1_.(L) = <%1_ L%>
proof let L be non empty multLoopStr_0;
A: 1_.(L) = 0_.(L)+*(0,1_(L)) by POLYNOM3:def 10;
B: dom 0_.(L) = NAT by FUNCT_2:def 1;
now let x be set; assume x in NAT; then reconsider n = x as Nat;
per cases;
suppose S1: x = 0;
thus (1_.(L)).x = 1_(L) by S1, A, B, FUNCT_7:33
.= <%1_ L%>.x by S1, ALGSEQ_1:def 6;
suppose S1: n <> 0; then n = 1 or n > 1 by neNat1; then
A1: n >= 1;
thus (1_.(L)).x = (0_.(L)).n by S1, A, FUNCT_7:34
.= 0.L by POLYNOM3:28 .= <%1_ L%>.x by A1, POLYNOM5:33;
end;
hence 1_.(L) = <%1_ L%> by FUNCT_2:18;
end;
theorem :: poly1a
for L being add-associative right_zeroed right_complementable right_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 right_unital
right-distributive (non empty doubleLoopStr),
p being Polynomial of L;
thus p*'<%1_ L%> = p*'1_.(L) by poly1b .= p by POLYNOM3:36;
end;
theorem LM0:
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
A: len p = 0 or len q = 0;
per cases by A;
suppose len p = 0; then p = 0_. L by POLYNOM4:8;
then p*'q = 0_. L by POLYNOM4:5;
hence len (p*'q) = 0 by POLYNOM4:6;
suppose len q = 0; then q = 0_. L by POLYNOM4:8; then p*'q = 0_. L by P4Th5;
hence len (p*'q) = 0 by POLYNOM4:6;
end;
theorem LM1: :: LM1
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
A: p*'q is non-zero and
B: p is non non-zero or q is non non-zero;
B1: len p <= 0 or len q <= 0 by B, lenNZ;
0 <= len p & 0 <= len q by NAT_1:18; then
len p = 0 or len q = 0 by B1; then
len (p*'q) = 0 by LM0;
hence thesis by A, lenNZ;
end;
theorem :: LM1a
for L being add-associative right_zeroed right_complementable distributive
commutative associative left_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 left_unital (non empty doubleLoopStr),
p, q being Polynomial of L; assume
Aa: p.(len p -'1) * q.(len q -'1) <> 0.L;
C: len (p*'q) = len p + len q -1 by Aa, POLYNOM4:13;
A1: now assume A2: len p <= 0; len p >= 0 by NAT_1:18;
then len p = 0 by A2; then p = 0_. L by POLYNOM4:8;
then p.(len p -'1) = 0.L by POLYNOM3:28;
hence contradiction by Aa, VECTSP_1:39;
end;
A2: now assume A2: len q <= 0; len q >= 0 by NAT_1:18;
then len q = 0 by A2; then q = 0_. L by POLYNOM4:8;
then q.(len q -'1) = 0.L by POLYNOM3:28;
hence contradiction by Aa,VECTSP_1:36;
end;
0+1 <= len p & 0+1 <= len q by A1, A2, NAT_1:38; then
len p + len q >= 1+1 by REAL_1:55;
then len p + len q -1 >= 1+1-1 by REAL_1:49;
then len p + len q -1 >= 1 & 1 > 0;
hence thesis by C;
end;
theorem LM2: :: LM2
for L being add-associative right_zeroed right_complementable distributive
commutative associative left_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 left_unital domRing-like (non empty doubleLoopStr),
p, q be Polynomial of L such that
B: 1 < len p and
C: 1 < len q;
0 < len p & 0 < len q by B, C, AXIOMS:22; then
p.(len p -'1) <> 0.L & q.(len q -'1)<>0.L by LC1; then
p.(len p -'1) * q.(len q -'1)<>0.L by VECTSP_2:def 5; then
E: len (p*'q) = len p + len q - 1 by POLYNOM4:13;
len q - 1 > 1-1 by C, REAL_1:92; then len q - 1 > 0; then
len p + (len q - 1) > 0+len p by REAL_1:67; then
len p + (len q +- 1) > len p by XCMPLX_0:def 8; then
len p + len q +- 1 > len p by XCMPLX_1:1;
hence len p < len (p*'q) by E, XCMPLX_0:def 8;
end;
theorem f2mpoly: :: f2mpoly:
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
A: len r = 0+1 and
B: p*'q.0 = Sum r and
C: for k be Nat st k in dom r holds r.k = p.(k-'1) * q.(0+1-'k)
by POLYNOM3:def 11;
D: 1 in dom r by A, FINSEQ_3:27; then
reconsider r1 = r.1 as Element of L by FINSEQ_2:13;
r = <*r1*> by A, FINSEQ_1:57; then
Sum r = r1 by RLVECT_1:61 .= p.(1-'1) * q.(0+1-'1) by C, D
.= p.0 * q.(0+1-'1) by GOBOARD9:1 .= p.0 * q.0 by BINARITH:39;
hence (<%a, b%>*'q).0 = a*q.0 by B, POLYNOM5:39;
let i be Nat;
consider r being FinSequence of L such that
A: len r = (i+1)+1 and
B: p*'q.(i+1) = Sum r and
C: for k be Nat st k in dom r holds r.k = p.(k-'1) * q.((i+1)+1-'k)
by POLYNOM3:def 11;
Aa: len r = i+(1+1) by A, XCMPLX_1:1 .= i+2; 0 <= i by NAT_1:18; then
D: 0+2 <= len r by Aa, AXIOMS:24; 1 <= len r by D, AXIOMS:22; then
E: 1 in dom r by FINSEQ_3:27;
F: 2 in dom r by D, FINSEQ_3:27;
G: r/.1 = r.1 by E, FINSEQ_4:def 4
.= p.(1-'1) * q.((i+1)+1-'1) by E, C .= p.0 * q.((i+1)+1-'1) by GOBOARD9:1
.= p.0 * q.(i+1) by BINARITH:39 .= a*q.(i+1) by POLYNOM5:39;
H: r/.2 = r.2 by F, FINSEQ_4:def 4
.= p.(2-'1) * q.((i+1)+1-'2) by F, C .= p.(1+1-'1) * q.((i+1)+1-'2)
.= p.1 * q.((i+1)+1-'2) by BINARITH:39 .= b * q.((i+1)+1-'2) by POLYNOM5:39
.= b * q.(i+(1+1)-'2) by XCMPLX_1:1 .= b * q.(i+2-'2)
.= b * q.i by BINARITH:39;
now let k be Nat such that
A1: 2 < k and
B1: k in dom r; k <> 0 by A1; then consider k1 being Nat such that
C1: k = k1+1 by NAT_1:22; 2+1 <= k by A1, NAT_1:38; then
D1: 2 <= k1 by C1, REAL_1:53;
thus r.k = p.(k-'1) * q.((i+1)+1-'k) by B1, C
.= p.k1 * q.((i+1)+1-'k) by C1, BINARITH:39
.= (0.L) * q.((i+1)+1-'k) by D1, POLYNOM5:39 .= 0.L by VECTSP_1:39;
end; then Sum r = r/.1 + r/.2 by D, thsum2;
hence (<%a, b%>*'q).(i+1) = a*q.(i+1)+b*q.i by B, G, H;
end;
theorem LM3a: :: LM3a
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;
1_ L <> 0.L by VECTSP_1:def 21; then
B: len <%r, 1_ L%> = 2 by POLYNOM5:41;
set p = <%r, 1_ L%>;
len q > 0 by lenNZ; then
C: q.(len q -'1)<>0.L by LC1;
p.(len p -'1) * q.(len q -'1) = p.(1+1-'1) * q.(len q -'1) by B
.= p.(1) * q.(len q -'1) by BINARITH:39
.= 1_ L * q.(len q -'1) by POLYNOM5:39
.= q.(len q -'1) by VECTSP_1:def 19;
hence len (<%r, 1_ L%>*'q) = 2 + len q - 1 by B,C,POLYNOM4:13
.= len q +(1+1)-1 .= len q +1+1-1 by XCMPLX_1:1 .= len q +1 by XCMPLX_1:26;
end;
theorem pexp2: :: pexp2
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%>;
r`^0 = 1_. L by POLYNOM5:16; then
BA: P[0] by POLYNOM4:7;
IS: for i being Nat st P[i] holds P[i+1] proof let i be Nat such that
A1: P[i];
i >= 0 by NAT_1:18; then i+1 > 0 by NAT_1:38; then
reconsider ri = r`^i as non-zero Polynomial of L by A1, lenNZ;
thus len (r`^(i+1)) = len ((r`^1)*'ri) by pexp1
.= len (r*'ri) by POLYNOM5:17 .= i+1+1 by A1, LM3a;
end;
thus for i being Nat holds P[i] from Ind(BA,IS);
end;
definition
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 pexp2; then
len (<%x, 1_ L%>`^n) <> 0; then
len (<%x, 1_ L%>`^n) > 0 by NAT_1:19;
hence thesis by lenNZ;
end;
end;
theorem pexp3: :: pexp3
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;
len ((r`^0)*'q) = len ((1_. L)*'q) by POLYNOM5:16
.= 0 + len q by POLYNOM3:36; then
BA: P[0];
IS: for i being Nat st P[i] holds P[i+1] proof let i be Nat such that
A1: P[i];
0 <= i & len q > 0 by NAT_1:18, lenNZ; then i+len q > 0+0 by REAL_1:67;
then
B1: (r`^i)*'q is non-zero by A1, lenNZ;
thus len ((r`^(i+1))*'q) = len ((r`^1)*'(r`^i)*'q) by pexp1
.= len (r*'(r`^i)*'q) by POLYNOM5:17
.= len (r*'((r`^i)*'q)) by POLYNOM3:34
.= (i+len q)+1 by A1, B1, LM3a
.= (i+1)+len q by XCMPLX_1:1;
end;
thus for i being Nat holds P[i] from Ind(BA,IS);
end;
theorem LM3: :: LM3:
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
A: p = <%x, 1_ L%>*'q and
B: p.(len p -'1) = 1_ L;
set lp1 = (len p -'1), lq1 = (len q -'1), d = <%x, 1_ L%>;
G: now assume q = 0_. L; then p = 0_. L by A, POLYNOM3:35; then
p.(len p -'1) = 0.L by POLYNOM3:28;
hence contradiction by B, VECTSP_1:def 21;
end; then q is non-zero by LNZ; then
I: len p = len q + 1 by A, LM3a;
J: lp1 = len q by I, BINARITH:39; len q <> 0 by G, POLYNOM4:8; then
consider lp2 being Nat such that
C: lp1 = lp2+1 by J, NAT_1:22;
D: lq1 = lp2 by C, J, BINARITH:39;
E: q.lp1 = 0.L by J, ALGSEQ_1:22;
(<%x, 1_ L%>*'q).lp1 = x*q.(lp1)+(1_ L)*q.lp2 by C, f2mpoly
.= 0.L +(1_ L)*q.lp2 by E, VECTSP_1:36
.= (1_ L)*q.lp2 by RLVECT_1:10 .= q.lp2 by VECTSP_2:def 2;
hence q.(len q -'1) = 1_ L by A, D, B;
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 :LPS:
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
A: len ps <= len p and
B: for k being Nat st k < len p holds ps.k = F(k) from AlgSeqLambdaF;
take ps; let i be Nat;
per cases;
suppose i < len p; hence ps.i = p.(n + i) by B;
suppose A1: i >= len p; then
B1: i >= len ps by A, AXIOMS:22;
C1: n+i >= len p by A1, NAT_1:37;
thus ps.i = 0.L by B1, ALGSEQ_1:22 .= p.(n + i) by C1, ALGSEQ_1:22;
end;
uniqueness proof let it1, it2 be Polynomial of L such that
A: for i being Nat holds it1.i = p.(n + i) and
B: for i being Nat holds it2.i = p.(n + i);
now let x be set; assume x in NAT; then
reconsider i = x as Nat;
thus it1.x = it1.i .= p.(n+i) by A .= it2.i by B .= it2.x;
end;
hence it1 = it2 by FUNCT_2:18;
end;
end;
theorem PS0: :: PS0:
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 set; assume x in NAT; then reconsider i = x as Nat;
thus ps.x = ps.i .= p.(0+i) by LPS .= p.x;
end;
hence poly_shift(p,0) = p by FUNCT_2:18;
end;
theorem PS1: :: PS1:
for L being non empty ZeroStr, n being 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 Nat, p be Polynomial of L; assume
A: n >= len p; set ps = poly_shift(p,n);
B: dom ps = NAT by FUNCT_2:def 1;
now let z be set; assume z in dom ps; then reconsider i = z as Nat by B;
B1: n+i >= len p by A, NAT_1:37;
thus ps.z = ps.i .= p.(n+i) by LPS .= 0.L by B1, ALGSEQ_1:22;
end; then ps = NAT --> 0.L by B, FUNCOP_1:17;
hence poly_shift(p,n) = 0_. L by POLYNOM3:def 9;
end;
theorem PS2: :: PS2:
for L being non degenerated non empty multLoopStr_0,
n being 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 Nat, p be Polynomial of L such that
A: n <= len p;
set ps = poly_shift(p,n), lpn = len p - n;
n-n <= lpn by A, REAL_1:49; then 0 <= lpn by XCMPLX_1:14; then
reconsider lpn as Nat by INT_1:16;
now let i be Nat; assume i >= lpn; then
A1: i+n >= len p by REAL_1:86;
thus ps.i = p.(n+i) by LPS .= 0.L by A1, ALGSEQ_1:22;
end; then
B: lpn is_at_least_length_of ps by ALGSEQ_1:def 3;
now let m be Nat such that
A1: m is_at_least_length_of ps and
B1: lpn > m; lpn >= m+1 by B1, NAT_1:38; then
lpn -1 >= m +1-1 by REAL_1:49; then
C1: lpn -1 >= m by XCMPLX_1:26; 0 <= m by NAT_1:18; then
0 <= lpn -1 by C1; then reconsider lpn1 = lpn -1 as Nat by INT_1:16;
D1: (n+lpn1)+1 = n +(lpn1+1) by XCMPLX_1:1
.= n+lpn by XCMPLX_1:27 .= len p by XCMPLX_1:27;
F1: ps.lpn1 = p.(n+lpn1) by LPS;
E1: p.(n+lpn1) <> 0.L by D1, ALGSEQ_1:25;
ps.lpn1 = 0.L by C1, A1, ALGSEQ_1:def 3;
hence contradiction by E1, F1;
end;
hence len poly_shift(p,n) + n = lpn + n by B, ALGSEQ_1:def 4
.= len p by XCMPLX_1:27;
end;
theorem evps: :: evps:
for L being non degenerated comRing,
x being Element of L, n being 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 Nat, p being Polynomial of L such that
AA: n < len p;
AAb: n <= len p by AA;
set ps = poly_shift(p,n), ps1 = poly_shift(p,n+1);
consider f be FinSequence of L such that
A: eval(ps,x) = Sum f and
B: len f = len ps and
C: for k be 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
D: eval(ps1,x) = Sum f1 and
E: len f1 = len ps1 and
F: for k be Nat st k in dom f1 holds f1.k = ps1.(k-'1) * (power L).(x,k-'1)
by POLYNOM4:def 2;
G: x*(Sum f1) = Sum (x*f1) by FVSUM_1:92;
H: x*f1 = (x multfield)*f1 by FVSUM_1:def 6;
rng f1 c= the carrier of L &
dom (x multfield) = the carrier of L by FINSEQ_1:def 4, FUNCT_2:def 1; then
I: dom ((x multfield)*f1) = dom f1 by RELAT_1:46;
now thus len f = len f;
A1a: n+1 <= len p by AA, NAT_1:38;
len ps1 +1+n = len ps1 +(n+1) by XCMPLX_1:1
.= len ps1 + (n+1) .= len p by A1a, PS2 .= len ps + n by AAb, PS2; then
A1: len ps1 + 1 = len ps by XCMPLX_1:2;
B1: len <*p.n*> = 1 by FINSEQ_1:57;
C1: len ((x*f1)) = len f1 by I, H, FINSEQ_3:31;
C1a: len (<*p.n*>^(x*f1)) = len (x*f1) + 1 by B1, FINSEQ_1:35;
hence
C1b: len (<*p.n*>^(x*f1)) = len f by A1, B, E, C1;
let j be Nat such that
D1: j in Seg len f;
E1: j in dom f by D1, FINSEQ_1:def 3; then
F1: 1 <= j & j <= len f by FINSEQ_3:27;
per cases by F1, REAL_1:def 5;
suppose S1: j = 1;
G1: 1 in dom <*p.n*> by B1, FINSEQ_3:27;
thus f.j = ps.(1-'1) * (power L).(x,1-'1) by E1, S1, C
.= ps.0 * (power L).(x,1-'1) by GOBOARD9:1
.= ps.0 * (power L).(x,0) by GOBOARD9:1 .= ps.0 * 1.L by GROUP_1:def 7
.= ps.0 by GROUP_1:def 4 .= p.(n+0) by LPS .= <*p.n*>.1 by FINSEQ_1:57
.= (<*p.n*>^(x*f1)).j by S1, G1, FINSEQ_1:def 7;
suppose 1 < j; then
G1: 1+1 <= j by NAT_1:38; 1-1 <= j-1 by F1, REAL_1:49; then 0 <= j-1; then
reconsider j1 = j-1 as Nat by INT_1:16;
I1a: 1+1-1 <= j-1 by G1, REAL_1:49;
j-1 <= len f1 + 1-1 by F1, C1a, C1, C1b, REAL_1:49; then
J1: 1 <= j1 & j1 <= len f1 by I1a, XCMPLX_1:26; then
J1a: j1 in dom f1 by FINSEQ_3:27; then
reconsider f1j = f1.j1 as Element of L by FINSEQ_2:13;
j = j1+1 by XCMPLX_1:27; then
K1a: j1 = j-'1 by BINARITH:39;
0 < j1 by J1, AXIOMS:22; then
consider j2 being Nat such that
Ma: j1 = j2+1 by NAT_1:22;
M: j1-'1+1 = j2+1 by Ma, BINARITH:39 .= j1 by Ma;
L: (n+1)+(j1-'1) = n+(1+(j1-'1)) by XCMPLX_1:1 .= n+j1 by M;
thus f.j = ps.(j-'1) * (power L).(x,j-'1) by E1, C
.= p.(n+j1) * (power L).(x,j1) by K1a, LPS
.= p.((n+1)+(j1-'1)) * (((power L).(x,j1-'1)) * x) by L,M,GROUP_1:def 7
.= (p.((n+1)+(j1-'1))*(power L).(x,j1-'1)) * x by VECTSP_1:def 16
.= x*(p.((n+1)+(j1-'1)) * (power L).(x,j1-'1))
.= x*(ps1.(j1-'1) * (power L).(x,j1-'1)) by LPS .= x*f1j by J1a, F
.= (x*f1).j1 by J1a, I, H, FVSUM_1:62
.= (<*p.n*>^(x*f1)).j by G1, B1, C1a, F1, C1b, FINSEQ_1:36;
end; then f = <*p.n*>^(x*f1)by FINSEQ_2:10;
hence eval(poly_shift(p,n),x) = p.n + x*eval(poly_shift(p,n+1),x)
by A, D, G, FVSUM_1:89
.= x*eval(poly_shift(p,n+1),x) + p.n;
end;
theorem Roots0: :: Roots0:
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
A: len p = 1; assume Roots p <> {}; then consider x being set such that
B: x in Roots p by XBOOLE_0:def 1;
C: p =<%p.0%> & p.0 <> 0.L by A, plen1; reconsider x as Element of L by B;
x is_a_root_of p by B,POLYNOM5:def 9;then eval(p,x) = 0.L by POLYNOM5:def 6;
hence contradiction by C, POLYNOM5:38;
end;
definition
let L be non degenerated comRing, r be Element of L, p be Polynomial of L
such that A: r is_a_root_of p;
func poly_quotient(p,r) -> Polynomial of L means :LPQUO:
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 assume B: len p > 0; consider p1 being Nat such that
F: len p = p1+1 by B, NAT_1:22; set lq = len p -'1;
Fa: lq = p1 by F, BINARITH:39;
Aa: len p >= 0+1 by B, NAT_1:38; r in Roots p by A, POLYNOM5:def 9; then
Roots p <> {}; then len p <> 1 by Roots0; then
len p > 0+1 by Aa, REAL_1:def 5; then lq > 0 by F, Fa, AXIOMS:24;
then consider lq1 being Nat such that
Ab: lq = lq1 + 1 by NAT_1:22;
Ac: lq1 = lq -'1 by Ab, BINARITH:39;
Ad: lq < len p by Fa, F, NAT_1:38;
deffunc F(Nat) = eval(poly_shift(p, $1+1),r);
consider q being Function of NAT, the carrier of L such that
Ba: for k being Nat holds q.k = F(k) from LambdaD;
reconsider q as sequence of L by NORMSP_1:def 3;
q.lq1 = eval(poly_shift(p, lq1+1),r) by Ba
.= r*eval(poly_shift(p, len p),r) + p.lq by Ab,Ad,Fa,F,evps
.= r*eval(0_. L,r) + p.lq by PS1 .= r*0.L + p.lq by POLYNOM4:20
.= 0.L + p.lq by VECTSP_1:36 .= p.lq by RLVECT_1:10; then
Bd: q.lq1 <> 0.L by F, Fa, ALGSEQ_1:25;
Bc: now let i be Nat such that
A1: i >= lq; i >= p1+1 -' 1 by A1, F; then
i >= p1 by BINARITH:39; then
B1: i+1 >= len p by F, AXIOMS:24;
thus q.i = eval(poly_shift(p, i+1),r) by Ba
.= eval(0_.L,r) by B1, PS1 .= 0.L by POLYNOM4:20;
end; then reconsider q as AlgSequence of L by ALGSEQ_1:def 2;
take q;
C: lq is_at_least_length_of q by Bc, ALGSEQ_1:def 3;
now let m be Nat; assume m is_at_least_length_of q; then
B1: for i being Nat st i >= m holds q.i = 0.L by ALGSEQ_1:def 3;
assume
C1: lq > m; 0 <= m by NAT_1:18; then
lq > 0 by C1; then consider lq1 being Nat such that
D1: lq = lq1 + 1 by NAT_1:22; lq >= m+1 by C1, NAT_1:38; then
E1: lq1 >= m by D1, REAL_1:53; lq1 = lq-'1 by D1, BINARITH:39; then
lq -'1 >= m by E1; then q.(lq-'1) = 0.L by B1;
hence contradiction by Ac, Bd;
end; then
E: len q = lq by C, ALGSEQ_1:def 4;
thus len q + 1 = len p -'1+1 by E .=p1+1-'1+1 by F .=len p by F,BINARITH:39;
thus for k being Nat holds q.k = F(k) by Ba;
end;
thus thesis;
end;
uniqueness proof let it1, it2 be Polynomial of L;
hereby assume len p > 0; assume that
A: len it1 + 1 = len p &
for i being Nat holds it1.i = eval(poly_shift(p, i+1),r) and
B: len it2 + 1 = len p &
for i being Nat holds it2.i = eval(poly_shift(p, i+1),r);
C: len it1 = len it1 +1-1 by XCMPLX_1:26 .= len it2 by A, B, XCMPLX_1:26;
now let k be Nat such that k < len it1;
thus it1.k = eval(poly_shift(p, k+1),r) by A .= it2.k by B;
end;
hence it1 = it2 by C, ALGSEQ_1:28;
end;
thus thesis;
end;
consistency;
end;
theorem pqlen: :: pqlen:
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
B: r is_a_root_of p;
A: len p > 0 by lenNZ;
Ca: len poly_quotient(p,r) + 1 = len p by A, B, LPQUO;
C: len poly_quotient(p,r) >= 0 by NAT_1:18;
assume len poly_quotient(p,r) <= 0; then
len poly_quotient(p,r) = 0 by C; then
D: Roots p = {} by Ca, Roots0;
r in Roots p by B, POLYNOM5:def 9;
hence contradiction by D;
end;
theorem Roots1: :: Roots1:
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 set;
hereby assume
A: a in Roots <%-x, 1_ L%>; then
reconsider b = a as Element of L;
b is_a_root_of <%-x, 1_ L%> by A, POLYNOM5:def 9; then
0.L = eval(<%-x, 1_ L%>,b) by POLYNOM5:def 6
.= -x + b by POLYNOM5:48; then -x = -b by RLVECT_1:19;
hence x = a by RLVECT_1:31;
end;
assume A: a = x;
eval(<%-x, 1_ L%>,x) = -x + x by POLYNOM5:48 .= 0.L by RLVECT_1:16; then
x is_a_root_of <%-x, 1_ L%> by POLYNOM5:def 6;
hence a in Roots <%-x, 1_ L%> by A, POLYNOM5:def 9;
end;
hence Roots <%-x, 1_ L%> = {x} by TARSKI:def 1;
end;
theorem BZA: :: BZA:
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
A: p = <%-x,1_ L%>*'q;
B: eval(<%-x,1_ L%>,x) = (-x)+x by POLYNOM5:48 .= 0.L by RLVECT_1:16;
thus eval(p,x) = eval(<%-x,1_ L%>,x) * eval(q,x) by A, POLYNOM4:27
.= 0.L by B, VECTSP_1:39;
end;
theorem BEZOUT: :: Factor theorem (Bezout)
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 that
B: x is_a_root_of p;
set r = <%-x,1_ L%>, pq = poly_quotient(p,x);
Aa: len p >= 0 by NAT_1:18;
per cases by Aa;
suppose A: len p > 0;
0.L <> 1_ L by VECTSP_1:def 21; then
C: len r = 2 by POLYNOM5:41;
p is non-zero by A, lenNZ; then
len pq > 0 by B, pqlen; then
Da: pq.(len pq -'1) <> 0.L by LC1;
r.(len r -'1) = r.(1+1-'1) by C .= r.1 by BINARITH:39
.= 1_ L by POLYNOM5:39; then
Db: r.(len r -'1) * pq.(len pq -'1) = pq.(len pq -'1) by VECTSP_1:def 19;
now len (r *' pq) = len r + len pq - 1 by Db, Da, POLYNOM4:13
.= len pq +(1+1)-1 by C .= len pq +1+1- 1 by XCMPLX_1:1
.= len pq +1 by XCMPLX_1:26 .= len p by A, B, LPQUO;
hence len p = len (r *' pq);
let k be Nat; assume k < len p;
defpred P[Nat] means p.$1 = (r*'pq).$1;
E: (r*'pq).0 = (-x)*pq.0 by f2mpoly
.= (-x)*eval(poly_shift(p, 0+1),x) by A, B, LPQUO;
F: 0.L = eval(p,x) by B, POLYNOM5:def 6 .= eval(poly_shift(p,0),x) by PS0
.= x*eval(poly_shift(p,0+1),x) + p.0 by A, evps;
(-x)*eval(poly_shift(p, 0+1),x)
= (-x)*eval(poly_shift(p, 0+1),x) + 0.L by RLVECT_1:def 7
.= (-x)*eval(poly_shift(p, 0+1),x) + x*eval(poly_shift(p,1),x) + p.0
by F, RLVECT_1:def 6
.= -x*eval(poly_shift(p, 0+1),x) + x*eval(poly_shift(p,1),x) + p.0
by VECTSP_1:41 .= 0.L +p.0 by RLVECT_1:16 .= p.0 by RLVECT_1:10; then
BA: P[0] by E;
IS: for k being Nat st P[k] holds P[k+1] proof
let k be Nat; assume P[k];
C1: pq.(k+1) = eval(poly_shift(p, k+1+1),x) by A, B, LPQUO;
B1: pq.k = eval(poly_shift(p, k+1),x) by A, B, LPQUO;
per cases;
suppose A1a: k+1 >= len p; then
D1: pq.k = eval(0_.L,x) by B1, PS1 .= 0.L by POLYNOM4:20;
k+1 <= k+1+1 by NAT_1:37; then k+1+1 >= len p by A1a, AXIOMS:22; then
E1: pq.(k+1) = eval(0_.L,x) by C1, PS1 .= 0.L by POLYNOM4:20;
(r*'pq).(k+1) = (-x)*pq.(k+1)+(1_ L)*pq.k by f2mpoly
.= 0.L + (1_ L)*pq.k by E1, VECTSP_1:36
.= 0.L + 0.L by D1, VECTSP_1:36 .= 0.L by RLVECT_1:10;
hence P[k+1] by A1a, ALGSEQ_1:22;
suppose A1a: k+1 < len p;
pq.k = x*eval(poly_shift(p, k+1+1),x) + p.(k+1) by B1,A1a, evps; then
D1: -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 6
.= 0.L + p.(k+1) by C1, RLVECT_1:16;
(r*'pq).(k+1) = (-x)*pq.(k+1)+(1_ L)*pq.k by f2mpoly
.= (-x)*pq.(k+1)+pq.k by VECTSP_1:def 19
.= -x*pq.(k+1)+pq.k by VECTSP_1:41;
hence P[k+1] by D1, RLVECT_1:10;
end; for k being Nat holds P[k] from Ind(BA,IS);
hence p.k = (r*'pq).k;
end;
hence p = r*'pq by ALGSEQ_1:28;
suppose len p = 0; then pq = 0_. L & p = 0_. L by POLYNOM4:8, B, LPQUO;
hence thesis by POLYNOM3:35;
end;
theorem BEZOUTa: :: 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:27
.= (-r+r) * eval(q,r) by POLYNOM5:48
.= 0.L * eval(q,r) by RLVECT_1:def 10
.= 0.L by VECTSP_1:39;
hence thesis by POLYNOM5:def 6;
end;
BZBL: now let L be domRing, p be non-zero Polynomial of L;
p <> 0_. L by LNZ; then len p <> 0 by POLYNOM4:8; then
len p > 0 by NAT_1:19; then
A: len p >= 0+1 by NAT_1:38;
defpred P[Nat] means
for p being Polynomial of L st len p = $1 holds
Roots p is finite &
ex n being Nat st n = Card Roots p & n < len p;
BA: P[1] proof let p be Polynomial of L; assume
B1: len p = 1; then
A1: Roots p = {} by Roots0;
thus Roots p is finite by A1;
take 0; thus 0 = Card Roots p by A1, CARD_1:78; thus 0 < len p by B1;
end;
IS: for n being Nat st n>=1 & P[n] holds P[n+1] proof
let n be Nat such that
A1: n >= 1 and
B1: P[n]; let p be Polynomial of L; assume
C1a: len p = n+1; then
C1: len p > 1 by A1, NAT_1:38;
per cases;
suppose p is with_roots; then
consider x being Element of L such that
D1: x is_a_root_of p by POLYNOM5:def 7;
D1a: len p > 0 by C1, AXIOMS:22;
E1: p = <%-x,1_ L%>*'poly_quotient(p,x) by D1, BEZOUT;
set r = <%-x,1_ L%>, pq = poly_quotient(p,x);
len pq + 1 = len p by D1, D1a, LPQUO; then
H1: len pq = n by C1a, XCMPLX_1:2; then
F1: Roots pq is finite by B1;
G1: Roots r = {x} by Roots1;
K1: Roots p = (Roots r)\/Roots pq by E1,pdomring0;
hence Roots p is finite by F1, G1, FINSET_1:14;
consider k being Nat such that
I1: k = Card Roots pq and
J1: k < len pq by B1, H1;
reconsider Rpq = Roots pq as finite set by B1, H1;
reconsider Rr = Roots r as finite set by G1;
reconsider Rp = Rpq \/ Rr as finite set;
take m = card Rp; thus m = Card Roots p by K1;
card Rr = 1 by G1, CARD_1:79; then
L1: card Rp <= k + 1 by I1, CARD_2:62;
k+1 < n+1 by J1, H1, REAL_1:67;
hence m < len p by C1a, L1, AXIOMS:22;
suppose S1: not p is with_roots;
A1: now assume Roots p <> {}; then consider x being set 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 9;
hence contradiction by S1, POLYNOM5:def 7;
end;
thus Roots p is finite by A1;
take 0; thus 0 = Card Roots p by A1, CARD_1:78;
thus 0 < len p by C1, AXIOMS:22;
end;
for n being Nat st n >= 1 holds P[n] from Ind1(BA,IS);
hence Roots p is finite &
ex n being Nat st n = Card Roots p & n < len p by A;
end;
begin :: Polynomials defined by roots
definition :: It is not true for a comRing. Who knows an example?
let L be domRing, p be non-zero Polynomial of L;
cluster Roots p -> finite;
correctness by BZBL;
end;
definition
let L be non degenerated comRing, x be Element of L,
p be non-zero (Polynomial of L);
func multiplicity(p,x) -> Nat means :MultiDef:
ex F being finite non empty Subset of NAT
st F = {k where k is Nat : ex q being Polynomial of L
st p = (<%-x, 1_ L%>`^k) *' q} &
it = max F;
existence proof
A: len p > 0 by lenNZ;
set r = <%-x, 1_ L%>;
defpred P[Nat] means ex q being Polynomial of L st p = (r`^$1) *' q;
set F = {k where k is Nat : P[k]};
p = (1_. L) *' p by POLYNOM3:36 .= (r`^0) *' p by POLYNOM5:16; then
A1: 0 in F;
B1: F c= len p proof let a be set; assume a in F; then
consider k being Nat such that
A2: a = k and
B2: P[k]; consider q being Polynomial of L such that
C2: p = (r`^k) *' q by B2;
now assume len q = 0; then q = 0_. L by POLYNOM4:8; then
p = 0_. L by C2, POLYNOM4:5; then len p = 0 by POLYNOM4:6;
hence contradiction by A;
end; then
D2: len q > 0 by NAT_1:19;
then reconsider q as non-zero Polynomial of L by lenNZ;
now assume k >= len p; then
k+len q > len p + 0 by D2, REAL_1:67;
hence contradiction by C2, pexp3;
end; then k in {i where i is Nat : i < len p};
hence a in len p by A2, AXIOMS:30;
end; F c= NAT from Fr_Set0; then
reconsider F as finite non empty Subset of NAT by A1, B1, FINSET_1:13;
reconsider FF = F as finite non empty natural-membered set;
max FF in NAT by ORDINAL2:def 21; then
reconsider m = max FF as Nat;
take m; thus thesis;
end;
uniqueness;
end;
theorem MULTI1: :: MULTI1:
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
B: F = {k where k is Nat : ex q being Polynomial of L st p = (r`^k) *' q} and
C: m = max F by MultiDef;
hereby assume x is_a_root_of p; then
A1: p = r*'poly_quotient(p,x) by BEZOUT;
r`^1 = r by POLYNOM5:17; then 1 in F by B, A1;
hence multiplicity(p,x) >= 1 by C, PRE_CIRC:def 1;
end;
assume
A1: multiplicity(p,x) >= 1;
m in F by C, PRE_CIRC:def 1; then consider k being Nat such that
B1: m = k and
C1: ex q being Polynomial of L st p = (r`^k) *' q by B;
consider q being Polynomial of L such that
D1: p = (r`^k) *' q by C1; m <> 0 by A1; then
consider k1 being Nat such that
E1: k = k1+1 by B1, NAT_1:22;
p = r *' (r`^k1) *' q by D1, E1, POLYNOM5:20
.= r *' ((r`^k1) *' q) by POLYNOM3:34;
hence x is_a_root_of p by BZA;
end;
theorem MULTI2: :: MULTI2:
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%>; 0.L <> 1_ L by VECTSP_1:def 21; then
A: len r = 2 by POLYNOM5:41;
consider F being finite non empty Subset of NAT such that
B: F = {k where k is Nat : ex q being Polynomial of L st r = (r`^k) *' q} and
C: multiplicity(r,x) = max F by MultiDef;
r = (r`^1) by POLYNOM5:17; then r = (r`^1) *' 1_. L by POLYNOM3:36; then
1 in F by B; then
D: multiplicity(r,x) >= 1 by C, PRE_CIRC:def 1;
set j = multiplicity(r,x); j in F by C, PRE_CIRC:def 1; then
consider k being Nat such that
E: k = j and
F: ex q being Polynomial of L st r = (r`^k) *' q by B;
consider q being Polynomial of L such that
G: r = (r`^k) *' q by F;
now assume len q = 0; then q = 0_. L by POLYNOM4:8; then
r = 0_. L by G, POLYNOM4:5; then len r = 0 by POLYNOM4:6;
hence contradiction by A;
end; then
H: len q > 0 by NAT_1:19; then
Ha: q is non-zero by lenNZ;
J: 2 = k+len q by Ha, G, A, pexp3;
now assume k > 1; then k >= 1+1 by NAT_1:38; then
k+len q > 2+0 by H, REAL_1:67;
hence contradiction by J;
end;
hence multiplicity(<%-x, 1_ L%>,x) = 1 by D, E, REAL_1:def 5;
end;
definition
let L be domRing, p be non-zero Polynomial of L;
func BRoots(p) -> bag of the carrier of L means :LBRoots:
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
A: for x being Element of L holds b.x = F(x) from LambdaD;
Ba: dom b = the carrier of L by FUNCT_2:def 1; then
B: b is ManySortedSet of the carrier of L by PBOOLE:def 3;
C: support b c= the carrier of L by Ba, POLYNOM1:41;
now let x be set;
hereby assume
A1: x in support b; then
B1: b.x <> 0 by POLYNOM1:def 7; reconsider xx = x as Element of L by A1, C;
C1: b.x = F(xx) by A; 0 < b.xx by B1, NAT_1:19;
then b.xx >= 0+1 by NAT_1:38; then xx is_a_root_of p by C1, MULTI1;
hence x in Roots p by POLYNOM5:def 9;
end;
assume A1: x in Roots p; then
reconsider xx = x as Element of L; xx is_a_root_of p by A1,POLYNOM5:def 9;
then multiplicity(p,xx) >= 1 by MULTI1; then b.xx >= 1 by A; then
b.xx <> 0;
hence x in support b by POLYNOM1:def 7;
end; then
Z: support b = Roots p by TARSKI:2; then support b is finite; then
C: b is finite-support by POLYNOM1:def 8;
reconsider b as bag of the carrier of L by B, C;
take b; thus thesis by Z, A;
end;
uniqueness proof let it1, it2 be bag of the carrier of L such that
support it1 = Roots p and
A1: for x being Element of L holds it1.x = multiplicity(p,x) and
support it2 = Roots p and
B1: for x being Element of L holds it2.x = multiplicity(p,x);
now let x be set; assume x in the carrier of L; then
reconsider xx = x as Element of L;
thus it1.x = multiplicity(p,xx) by A1 .= it2.x by B1;
end;
hence it1 = it2 by PBOOLE:3;
end;
end;
theorem BR1e: :: BR1e:
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%>; 0.L <> 1_ L by VECTSP_1:def 21; then
Roots r = {x} by Roots1; then
B: support BRoots r = {x} by LBRoots;
C: x in {x} by TARSKI:def 1;
now let i be set; assume i in the carrier of L; then
reconsider i1 = i as Element of L;
per cases;
suppose B1: i = x;
thus (BRoots r).i = multiplicity(r,i1) by LBRoots
.= 1 by B1, MULTI2 .= (({x}, 1)-bag).i by B1, C, Snbag1;
suppose i <> x; then
C1: not i in {x} by TARSKI:def 1;
hence (BRoots r).i = 0 by B, POLYNOM1:def 7
.= (({x}, 1)-bag).i by C1, Snbag0;
end;
hence BRoots <%-x, 1_ L%> = ({x}, 1)-bag by PBOOLE:3;
end;
theorem BR1da: :: BR1da:
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
D: F = {k where k is Nat : ex pqq being Polynomial of L
st p*'q = (r`^k) *' pqq} and
E: multiplicity(p*'q,x) = max F by MultiDef;
consider f being finite non empty Subset of NAT such that
F: f = {k where k is Nat : ex pq being Polynomial of L
st p = (r`^k) *' pq} and
G: multiplicity(p,x) = max f by MultiDef;
consider g being finite non empty Subset of NAT such that
H: g = {k where k is Nat : ex qq being Polynomial of L
st q = (r`^k) *' qq} and
I: multiplicity(q,x) = max g by MultiDef;
max F in F by PRE_CIRC:def 1; then
consider k being Nat such that
Da: k = max F and
Db: ex pqq being Polynomial of L st p*'q = (r`^k) *' pqq by D;
consider pqq being Polynomial of L such that
Dc: p*'q = (r`^k) *' pqq by Db;
max f in f by PRE_CIRC:def 1; then
consider i being Nat such that
Fa: i = max f and
Fb: ex pq being Polynomial of L st p = (r`^i) *' pq by F;
consider pq being Polynomial of L such that
Fc: p = (r`^i) *' pq by Fb;
max g in g by PRE_CIRC:def 1; then
consider j being Nat such that
Ga: j = max g and
Gb: ex qq being Polynomial of L st q = (r`^j) *' qq by H;
consider qq being Polynomial of L such that
Gc: q = (r`^j) *' qq by Gb;
K: p*'q = (r`^i) *' pq *' ((r`^j) *' qq) by Fc, Gc
.= (r`^i) *' pq *' (r`^j) *' qq by POLYNOM3:34
.= (r`^i) *' (pq *' (r`^j)) *' qq by POLYNOM3:34
.= (r`^i) *' (r`^j) *' pq *' qq by POLYNOM3:34
.= (r`^(i+j)) *' pq *' qq by pexp1
.= (r`^(i+j)) *' (pq *' qq) by POLYNOM3:34;
then i+j in F by D; then
J: i+j <= k by Da, PRE_CIRC:def 1;
now assume i+j < k; then 0+(i+j) < k; then
B1: 0 < k-(i+j) by REAL_1:86; then 0 <= k-(i+j); then
reconsider kij = k-(i+j) as Nat by INT_1:16;
consider kk being Nat such that
D1: kij = kk+1 by B1, NAT_1:22;
(0_. L).1 = 0.L & r.1 = 1_ L by POLYNOM3:28, POLYNOM5:39; then
r <> 0_. L by VECTSP_1:def 21; then
C1: r`^(i+j) <> 0_. L by pexp0;
k = kij + (i+j) by XCMPLX_1:27; then
p*'q = ((r`^(i+j)) *' (r`^kij)) *' pqq by Dc, pexp1
.= (r`^(i+j)) *' ((r`^kij) *' pqq) by POLYNOM3:34; then
E1: (r`^kij) *' pqq = pq *' qq by C1, K, pcanc0;
(r`^kij) = (r`^1) *' (r`^kk) by D1, pexp1
.= r *' (r`^kk) by POLYNOM5:17; then
(r`^kij) *' pqq = r *' ((r`^kk) *' pqq) by POLYNOM3:34; then
x is_a_root_of (pq *' qq) by E1, BZA; then
x in Roots (pq *' qq) by POLYNOM5:def 9; then
x in (Roots pq \/ Roots qq) by pdomring0; then
F1: x in Roots(pq) or x in Roots(qq) by XBOOLE_0:def 2;
per cases by F1;
suppose x in Roots(pq); then x is_a_root_of pq by POLYNOM5:def 9; then
pq = r *' poly_quotient(pq,x) by BEZOUT; then
p = (r`^i) *' r *' poly_quotient(pq,x) by Fc, POLYNOM3:34
.= (r`^i) *' (r`^1) *' poly_quotient(pq,x) by POLYNOM5:17
.= (r`^(i+1)) *' poly_quotient(pq,x) by pexp1; then
i+1 in f by F; then i+1 <= i by Fa, PRE_CIRC:def 1;
hence contradiction by NAT_1:38;
suppose x in Roots(qq); then x is_a_root_of qq by POLYNOM5:def 9; then
qq = r *' poly_quotient(qq,x) by BEZOUT; then
q = (r`^j) *' r *' poly_quotient(qq,x) by Gc, POLYNOM3:34
.= (r`^j) *' (r`^1) *' poly_quotient(qq,x) by POLYNOM5:17
.= (r`^(j+1)) *' poly_quotient(qq,x) by pexp1; then
j+1 in g by H; then j+1 <= j by Ga, PRE_CIRC:def 1;
hence contradiction by NAT_1:38;
end;
hence multiplicity(p*'q,x) = multiplicity(p,x) + multiplicity(q,x)
by J, Da, Fa, Ga, E, G, I, REAL_1:def 5;
end;
theorem BR1d: :: BR1d:
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 set; assume
A1: i in the carrier of L;
reconsider x = i as Element of L by A1;
thus (BRoots(p*'q)).i = multiplicity(p*'q, x) by LBRoots
.= multiplicity(p,x) + multiplicity(q,x) by BR1da
.= (BRoots p).i + multiplicity(q,x) by LBRoots
.= (BRoots p).i + (BRoots q).i by LBRoots
.= (BRoots(p) + BRoots(q)).i by POLYNOM1:def 5;
end;
hence BRoots(p*'q) = BRoots(p) + BRoots(q) by PBOOLE:3;
end;
BR1a:
now let L be domRing, p, q be non-zero Polynomial of L;
BRoots(p*'q) = BRoots(p) + BRoots(q) by BR1d;
hence degree BRoots (p*'q) = degree (BRoots p) + degree BRoots q by BAGDEG2;
end;
theorem BR1b: :: BR1b:
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 Roots0; then
support BRoots p = {} by LBRoots; then
BRoots p = EmptyBag the carrier of L by BAGORDER:20;
hence degree BRoots p = 0 by BAGDEG0;
end;
theorem BR1c: :: BR1c:
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;
A: len 1_. L = 1 by POLYNOM4:7;
B: r`^0 = 1_. L by POLYNOM5:16;
BA: P[0] by BR1b, A, B;
IS: for n being Nat st P[n] holds P[n+1] proof let n be Nat such that
A: P[n]; 0.L <> 1_ L by VECTSP_1:def 21; then
card {x} = 1 & support ({x},1)-bag = {x} by Snbagsup, CARD_1:79; then
D: degree ({x},1)-bag = 1 by BAGDEG1;
r`^(n+1) = (r`^n)*'r by POLYNOM5:20; then
degree BRoots(r`^(n+1))
= degree BRoots (r`^n) + degree BRoots r by BR1a
.= n + degree ({x},1)-bag by A, BR1e;
hence P[n+1] by D;
end;
thus for n being Nat holds P[n] from Ind(BA,IS);
end;
theorem :: BR2
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;
A: len p > 0 by lenNZ;
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;
P: for k being Nat st for n being Nat st n < k holds P[n] holds P[k]
proof let k be Nat; assume
A1: for n being Nat st n < k holds P[n];
let p be non-zero Polynomial of L; assume that
B1: len p = k and
C1b: k > 0;
C1a: k >= 0+1 by C1b, NAT_1:38;
thus thesis proof per cases by C1a, REAL_1:def 5;
suppose S1: k = 1;
hence degree BRoots p = 0 by B1, BR1b .= 1-1
.= len p -' 1 by B1, S1, SCMFSA_7:3;
suppose C1: k > 1;
p is with_roots by B1, C1, POLYNOM5:def 8; then
consider x being Element of L such that
D1: x is_a_root_of p by POLYNOM5:def 7;
E1: multiplicity(p,x) >= 1 by D1, MULTI1;
consider F being finite non empty Subset of NAT such that
F1: F = {l where l is Nat : ex q being Polynomial of L
st p = (<%-x, 1_ L%>`^l) *' q} and
G1: multiplicity(p,x) = max F by MultiDef;
max F in F by PRE_CIRC:def 1; then
consider l being Nat such that
J1: l = max F and
K1: ex q being Polynomial of L st p = (<%-x, 1_ L%>`^l) *' q by F1;
consider q being Polynomial of L such that
L1: p = (<%-x, 1_ L%>`^l) *' q by K1;
set r = <%-x, 1_ L%>; set rr = <%-x, 1_ L%>`^l;
len p > 0 by B1, C1, AXIOMS:22; then p is non-zero by lenNZ;
then reconsider q as non-zero Polynomial of L by L1, LM1;
len q > 0 by lenNZ; then
M1: len q >= 0+1 by NAT_1:38;
thus thesis proof 0.L <> 1_ L by VECTSP_1:def 21; then
len r = 2 by POLYNOM5:41; then
A2: len rr = l*2 -l+1 by POLYNOM5:24;
B2: l*2 -l+1 = l+l-l+1 by XCMPLX_1:11 .= l+1 by XCMPLX_1:26;
C2: len rr > 1 by A2, J1, G1, E1, B2, NAT_1:38;
F2: len rr > 0 & len q > 0 by C2, M1, AXIOMS:22; then
rr.(len rr -'1) <> 0.L & q.(len q -'1) <> 0.L by LC1; then
F2a: rr.(len rr -'1) * q.(len q -'1) <> 0.L by VECTSP_2:def 5;
per cases by M1, REAL_1:def 5;
suppose S1: len q = 1;
A3: len p = len rr + len q -1 by F2a, L1, POLYNOM4:13
.= len rr by S1, XCMPLX_1:26;
thus degree BRoots p
= degree (BRoots rr) + degree BRoots q by L1, BR1a
.= degree (BRoots rr) + 0 by S1, BR1b
.= l by BR1c .= l+l-l by XCMPLX_1:26 .= 2*l - l by XCMPLX_1:11
.= 2*l-l+1-1 by XCMPLX_1:26
.= len p -' 1 by A3, A2, B1, C1a, SCMFSA_7:3;
suppose S1: len q > 1;
E2: len rr < k & len q < k by B1, C2, L1, S1, LM2;
D2: degree BRoots rr = l+1 -' 1 &
degree BRoots q = len q -' 1 by A2, B2, E2, A1, F2;
thus degree BRoots p
= degree (BRoots rr) + degree BRoots q by L1, BR1a
.= len rr-'1 + (len q -'1) by A2, B2, D2
.= len rr-1 + (len q -'1) by C2, SCMFSA_7:3
.= len rr-1 + (len q -1) by S1, SCMFSA_7:3
.= len rr + (len q -1) -1 by XCMPLX_1:29
.= len rr + (len q + -1) -1 by XCMPLX_0:def 8
.= len rr + len q + -1 -1 by XCMPLX_1:1
.= len rr + len q -1 -1 by XCMPLX_0:def 8
.= len p -1 by F2a,L1, POLYNOM4:13 .= len p -' 1 by B1, C1, SCMFSA_7:3;
end; end; end;
for n being Nat holds P[n] from Comp_Ind(P);
hence degree BRoots p = len p -' 1 by A;
end;
definition
let L be add-associative right_zeroed right_complementable distributive
(non empty doubleLoopStr),
c be Element of L, n be Nat;
func fpoly_mult_root(c,n) -> FinSequence of Polynom-Ring L means :LFPMR:
len it = n &
for i being 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 12;
then reconsider f = n |-> <% -c, 1_ L%>
as FinSequence of Polynom-Ring L by FINSEQ_2:77;
take f;
thus
A: len f = n by FINSEQ_2:69;
let i be Nat;
assume i in dom f; then i in Seg n by A, FINSEQ_1:def 3;
hence f.i = <% -c, 1_ L%> by FINSEQ_2:70;
end;
uniqueness proof let it1, it2 be FinSequence of Polynom-Ring L such that
A1: len it1 = n and
B1: for i being Nat st i in dom it1 holds it1.i = <% -c, 1_ L%> and
A2: len it2 = n and
B2: for i being Nat st i in dom it2 holds it2.i = <% -c, 1_ L%>;
C: dom it1 = dom it2 by A1, A2, FINSEQ_3:31;
now let x be Nat; assume
D: x in dom it1;
thus it1.x = <% -c, 1_ L%> by D, B1 .= it2.x by D, C, B2;
end;
hence it1 = it2 by C, FINSEQ_1:17;
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 :LPWR:
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 Nat st i in dom f holds f.i = fpoly_mult_root(s/.i,b.(s/.i)))
& it = Product FlattenSeq f;
existence proof
AA: support b c= dom b & dom b = the carrier of L by POLYNOM1:41, PBOOLE:def 3;
rng canFS(support b) c= support b by FINSEQ_1:def 4; then
rng canFS(support b) c= the carrier of L by AA, 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
A: len f = card support b and
B: for k being Nat st k in Seg card support b holds f.k = F(k) from SeqLambda;
rng f c= (the carrier of Polynom-Ring L)* proof let x be set;
assume x in rng f; then consider i being Nat such that
A1: i in dom f and
B1: f.i = x by FINSEQ_2:11;
i in Seg card support b by A1, A, FINSEQ_1:def 3; then
x = F(i) by B1, B;
hence x in (the carrier of Polynom-Ring L)* 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 12;
take it1, f, s;
thus len f = card support b by A;
thus s = canFS(support b);
hereby let i be Nat; assume i in dom f; then
i in Seg card support b by A, FINSEQ_1:def 3;
hence f.i = fpoly_mult_root(s/.i,b.(s/.i)) by B;
end;
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
A: len f1 = card support b & s1 = canFS(support b) &
(for i being Nat st i in dom f1
holds f1.i = fpoly_mult_root(s1/.i,b.(s1/.i)))
& it1 = Product FlattenSeq f1;
given f2 being FinSequence of (the carrier of Polynom-Ring L)*,
s2 being FinSequence of L such that
B: len f2 = card support b & s2 = canFS(support b) &
(for i being Nat st i in dom f2
holds f2.i = fpoly_mult_root(s2/.i,b.(s2/.i)))
& it2 = Product FlattenSeq f2;
C: dom f1 = dom f2 by A, B, FINSEQ_3:31;
D: dom f1 = Seg len f1 by FINSEQ_1:def 3;
now let i be Nat; assume
A1: i in Seg len f1;
hence f1.i = fpoly_mult_root(s1/.i,b.(s1/.i)) by D, A
.= f2.i by A, C, A1, D, B;
end; then f1 = f2 by A, B, FINSEQ_2:10;
hence thesis by A, B;
end;
end;
theorem poly1: :: poly1:
for L being Abelian add-associative right_zeroed right_complementable
commutative distributive right_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 right_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
A: len f = card support b and s = canFS(support b) and
for i being Nat st i in dom f holds f.i = fpoly_mult_root(s/.i,b.(s/.i))and
D: poly_with_roots(b) = Product FlattenSeq f by LPWR;
card support b = 0 by CARD_1:78, BAGORDER:19; then
f = <*>((the carrier of Polynom-Ring L)*) by A, FINSEQ_1:32; then
FlattenSeq f = <*>(the carrier of Polynom-Ring L) by SCMFSA_7:13; then
Product FlattenSeq f = 1_ Polynom-Ring L by FVSUM_1:98
.= 1_.(L) by POLYNOM3:def 12;
hence thesis by D, poly1b;
end;
theorem poly1_1: :: poly1_1:
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
A: len f = card support b and
B: s = canFS(support b) and
C: for i being Nat st i in dom f holds f.i = fpoly_mult_root(s/.i,b.(s/.i))and
D: poly_with_roots(b) = Product FlattenSeq f by LPWR;
Da: support b = {c} by Snbagsup; then
E: card support b = 1 by CARD_1:79; then
F: f = <*f/.1*> by A, FINSEQ_5:15;
G: 1 in dom f by A, E, FINSEQ_3:27; then f.1 = f/.1 by FINSEQ_4:def 4; then
Ia: FlattenSeq f = f.1 by F, DTCONSTR:13;
I: f.1 = fpoly_mult_root(s/.1,b.(s/.1)) by G, C;
set f1 = fpoly_mult_root(s/.1,b.(s/.1));
Ic: s = <* c *> by Da, B, CFS2; len s = 1 by B, E, LCFS; then
1 in dom s by FINSEQ_3:27; then
Ib: s/.1 = s.1 by FINSEQ_4:def 4 .= c by Ic, FINSEQ_1:57;
c in {c} by TARSKI:def 1; then b.(s/.1) = 1 by Ib, Snbag1; then
J: len f1 = 1 by LFPMR;
K: for i being Nat st i in dom f1 holds f1.i = <% -c, 1_ L%> by Ib, LFPMR;
L: f1 = <*f1/.1*> by J, FINSEQ_5:15;
M: 1 in dom f1 by J, FINSEQ_3:27;
thus poly_with_roots(({c},1)-bag) = Product FlattenSeq f by D
.= f1/.1 by Ia, I, L, FVSUM_1:99 .= f1.1 by M, FINSEQ_4:def 4
.= <% -c, 1_ L %> by K, M;
end;
theorem PWRBBa: :: PWRBBa:
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 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
A: len f = card support b and
B: s = canFS(support b) and
C: for i being Nat st i in dom f holds f.i = fpoly_mult_root(s/.i,b.(s/.i));
len s = card support b by B, LCFS; then
Aa: dom f = dom s by A, FINSEQ_3:31;
reconsider Cf = Card f as FinSequence of NAT;
D: len FlattenSeq f = Sum Cf by POLYNOM1:30;
consider g being FinSequence of NAT such that
E: degree b = Sum g and
F: g = b*canFS(support b) by LBAGDEG;
now
A1: rng s c= dom b proof let x be set; assume x in rng s; then
A2: x in support b by B, CFS1; support b c= dom b by POLYNOM1:41;
hence x in dom b by A2;
end;
thus dom Card f = dom f by CARD_3:def 2
.= dom g by B, F, Aa, A1, RELAT_1:46;
let i be Nat such that
C1: i in dom Card f;
D1: i in dom f by C1, CARD_3:def 2; then
f.i = fpoly_mult_root(s/.i,b.(s/.i)) by C; then
E1: len (f.i) = b.(s/.i) by LFPMR;
F1: g.i = b.(s.i) by D1, Aa, F, B, FUNCT_1:23;
thus Cf.i = Card (f.i) by D1, CARD_3:def 2
.= g.i by F1, E1, D1, Aa, FINSEQ_4:def 4;
end; then
Card f = b*canFS(support b) by F, FINSEQ_1:17;
hence len FlattenSeq f = degree b by D, E, F;
end;
theorem PWRBBb: :: PWRBBb:
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 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
A: len f = card support b and
B: s = canFS(support b) and
C: for i being Nat st i in dom f holds f.i = fpoly_mult_root(s/.i,b.(s/.i));
len f = len s by A, B, LCFS; then
Ab: dom f = dom s by FINSEQ_3:31;
Ac: s is one-to-one by B, CFS0;
hereby assume c in support b; then c in rng s by B, CFS1; then
consider i being Nat such that
A1: i in dom s and
B1: s.i = c by FINSEQ_2:11;
B1a: s/.i = c by A1, B1, FINSEQ_4:def 4;
C1: card (b.c) = b.c by CARD_1:66;
D1: b.c = { k where k is Nat : k < b.c } by AXIOMS:30;
set ff = FlattenSeq f; set Y = ff"{<% -c, 1_ L%>};
set X = { k where k is Nat : k < b.c };
defpred P[set,Nat] means ex n being Nat st n = $1 &
$2 = (Sum Card(f|(i-'1)))+(1+n);
UN: for x,y1,y2 being set st x in X & P[x,y1] & P[x,y2] holds y1 = y2;
EX: for x being set st x in X ex y being set st P[x,y] proof
let x be set; assume x in X; then consider k being Nat such that
A2: x = k and k < b.c;
take y = (Sum Card(f|(i-'1)))+(1+k); thus P[x,y] by A2;
end;
consider g being Function such that
E1: dom g = X and
F1: for x being set st x in X holds P[x,g.x] from FuncEx(UN,EX);
Z1: g is one-to-one proof let x1,x2 be set such that
A2: x1 in dom g and
B2: x2 in dom g and
C2: g.x1 = g.x2; consider n1 being Nat such that
D2: n1 = x1 and
E2: g.x1 = (Sum Card(f|(i-'1)))+(1+n1) by E1, A2, F1;
consider n2 being Nat such that
F2: n2 = x2 and
G2: g.x2 = (Sum Card(f|(i-'1)))+(1+n2) by E1, B2, F1;
1+n1 = 1+n2 by C2, E2, G2, XCMPLX_1:2;
hence x1 = x2 by D2, F2, XCMPLX_1:2;
end;
now let y be set;
hereby assume y in rng g; then consider x being set such that
A2: x in dom g and
B2: y = g.x by FUNCT_1:def 5;
consider k being Nat such that
C2: x = k and
D2: k < b.c by A2, E1;
consider n being Nat such that
E2: n = x and
F2: g.x = (Sum Card(f|(i-'1)))+(1+n) by A2, E1, F1;
G2: f.i = fpoly_mult_root(s/.i,b.(s/.i)) by A1, Ab, C;
G2b: 1 <= 1+n & 1+n <= b.c by E2, C2, D2, NAT_1:38,37;
len (f.i) = b.c by B1a, G2, LFPMR; then
G2a: 1+n in dom (f.i) by G2b, FINSEQ_3:27; then
H2:(Sum Card (f|(i-'1))) + (1+n) in dom ff &
(f.i).(1+n) = ff.((Sum Card (f|(i-'1))) + (1+n))
by A1, Ab, POLYNOM1:33;
(f.i).(1+n) = <% -c, 1_ L%> by G2, G2a, B1a, LFPMR; then
(f.i).(1+n) in {<% -c, 1_ L%>} by TARSKI:def 1;
hence y in Y by H2, B2, F2, FUNCT_1:def 13;
end;
assume y in Y; then
A2: y in dom ff & ff.y in {<% -c, 1_ L%>} by FUNCT_1:def 13;
reconsider yn = y as Nat by A2, FINSEQ_3:25;
consider i1, j being Nat such that
B2: i1 in dom f and
C2: j in dom (f.i1) and
D2: yn = (Sum Card (f|(i1-'1))) + j and
E2: (f.i1).j = ff.yn by A2, POLYNOM1:32;
j <> 0 by C2, FINSEQ_3:26; then consider j1 being Nat such that
G2: j = j1 + 1 by NAT_1:22;
C3: f.i1 = fpoly_mult_root(s/.i1,b.(s/.i1)) by B2, C;
(f.i1).j = <%-s/.i1, 1_ L%> by C3, C2, LFPMR; then
D3: <% -c, 1_ L%> = <%-s/.i1, 1_ L%> by E2, A2, TARSKI:def 1;
<% -c, 1_ L%>.0 = -c & <% -s/.i1,1_ L%>.0 = -s/.i1 by POLYNOM5:39;
then -c = -s/.i1 by D3; then
E3: c = s/.i1 by RLVECT_1:31;
F3: i1 in dom s by B2, Ab; then s/.i1 = s.i1 by FINSEQ_4:def 4; then
s.i = s.i1 by E3, B1; then
J2: i1 = i by F3, A1, Ac, FUNCT_1:def 8;
len (f.i1) = b.c by C3, E3, LFPMR; then
j <= b.c by C2, FINSEQ_3:27; then j1 < b.c by G2, NAT_1:38; then
G2a: j1 in X; then consider n being Nat such that
H2: n = j1 and
I2: g.j1 = (Sum Card(f|(i-'1)))+(1+n) by F1;
g.j1 = y by J2, I2, H2, G2, D2;
hence y in rng g by G2a, E1, FUNCT_1:12;
end; then
rng g = Y by TARSKI:2; then X,Y are_equipotent by Z1, E1, WELLORD2:def 4;
hence card ((FlattenSeq f)"{<% -c, 1_ L%>}) = b.c by C1, D1, CARD_1:21;
end;
assume that
D: not c in support b and
E: card ((FlattenSeq f)"{<% -c, 1_ L%>}) <> 0;
(FlattenSeq f)"{<% -c, 1_ L%>} <> {} by E, CARD_1:78; then
consider x being set such that
F: x in (FlattenSeq f)"{<% -c, 1_ L%>} by XBOOLE_0:def 1;
G: x in dom FlattenSeq f by F, FUNCT_1:def 13; then
reconsider x as Nat by FINSEQ_3:25;
consider i, j being Nat such that
I: i in dom f and
J: j in dom (f.i) and x = (Sum Card (f|(i-'1))) + j and
K: (f.i).j = (FlattenSeq f).x by G, POLYNOM1:32;
(FlattenSeq f).x in {<% -c, 1_ L%>} by F, FUNCT_1:def 13; then
H: (FlattenSeq f).x = <% -c, 1_ L%> by TARSKI:def 1;
f.i = fpoly_mult_root(s/.i,b.(s/.i)) by C, I; then
L: (f.i).j = <% -s/.i, 1_ L%> by J, LFPMR;
<% -c, 1_ L%>.0 = -c & <% -s/.i, 1_ L%>.0 = -s/.i by POLYNOM5:39; then
-c = -s/.i by L, H, K; then
M: c = s/.i by RLVECT_1:31; i in dom s by Ab, I; then
s/.i = s.i & s.i in rng s by FINSEQ_4:def 4, FUNCT_1:12; then
c in support b by B, CFS1, M;
hence contradiction by D;
end;
theorem PWRBB: :: PWRBB:
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;
consider f being FinSequence of (the carrier of Polynom-Ring L)*,
s being FinSequence of L such that
A: len f = card support b and
B: s = canFS(support b) and
C: for i being Nat st i in dom f holds f.i = fpoly_mult_root(s/.i,b.(s/.i)) and
D: poly_with_roots(b1+b2) = Product FlattenSeq f by LPWR;
consider f1 being FinSequence of (the carrier of Polynom-Ring L)*,
s1 being FinSequence of L such that
Aa: len f1 = card support b1 and
Ba: s1 = canFS(support b1) and
Ca: for i being Nat st i in dom f1
holds f1.i = fpoly_mult_root(s1/.i,b1.(s1/.i)) and
Da: poly_with_roots(b1) = Product FlattenSeq f1 by LPWR;
consider f2 being FinSequence of (the carrier of Polynom-Ring L)*,
s2 being FinSequence of L such that
Ab: len f2 = card support b2 and
Bb: s2 = canFS(support b2) and
Cb: for i being Nat st i in dom f2
holds f2.i = fpoly_mult_root(s2/.i,b2.(s2/.i)) and
Db: poly_with_roots(b2) = Product FlattenSeq f2 by LPWR;
set ff = FlattenSeq f, ff1 = FlattenSeq f1, ff2 = FlattenSeq f2;
set g = (FlattenSeq f1) ^ (FlattenSeq f2);
E: support b = support b1 \/ support b2 by POLYNOM1:42;
F: len ff = degree b by A, B, C, PWRBBa;
G: len ff1 = degree b1 by Aa, Ba, Ca, PWRBBa;
H: len ff2 = degree b2 by Ab, Bb, Cb, PWRBBa;
len g = len ff1 + len ff2 by FINSEQ_1:35
.= degree b1 + degree b2 by G, H .= degree b by BAGDEG2; then
I: dom ff = dom g by F, FINSEQ_3:31;
J: len s = card support b by B, LCFS;
now let x be set;
set ffx = ff"{x}, gx = g"{x};
per cases;
suppose x in rng ff; then consider k being Nat such that
A1: k in dom ff and
B1: ff.k = x by FINSEQ_2:11;
consider i, j being Nat such that
C1: i in dom f and
D1: j in dom (f.i) and k = (Sum Card (f|(i-'1))) + j and
F1: (f.i).j = ff.k by A1, POLYNOM1:32;
G1: f.i = fpoly_mult_root(s/.i,b.(s/.i)) by C1, C;
H1: (f.i).j = <% -s/.i, 1_ L %> by D1, G1, LFPMR;
i in dom s by J, A, C1, FINSEQ_3:31; then
s.i = s/.i & s.i in rng s by FINSEQ_4:def 4, FUNCT_1:12; then
K1: s/.i in support b by B, CFS1; then
L1: card (ff"{x}) = b.(s/.i) by H1, F1, B1, A, B, C, PWRBBb;
M1: card (g"{x}) = card (ff1"{x}) + card (ff2"{x}) by FINSEQ_3:63;
thus card (ff"{x}) = card (g"{x}) proof
per cases by K1, E, XBOOLE_0:def 2;
suppose A2: s/.i in support b1 & not s/.i in support b2; then
B2: card(ff1"{x}) = b1.(s/.i) by H1, F1, B1, Aa, Ba, Ca, PWRBBb;
C2: card(ff2"{x}) = 0 by A2, H1, F1, B1, Ab, Bb, Cb, PWRBBb;
thus card (ff"{x}) = b.(s/.i) by L1
.= b1.(s/.i) + b2.(s/.i) by POLYNOM1:def 5
.= b1.(s/.i) + 0 by A2, POLYNOM1:def 7
.= card(g"{x}) by B2, C2, M1;
suppose A2: not s/.i in support b1 & s/.i in support b2; then
B2: card(ff1"{x}) = 0 by H1, F1, B1, Aa, Ba, Ca, PWRBBb;
C2: card(ff2"{x}) = b2.(s/.i) by A2, H1, F1, B1, Ab, Bb, Cb, PWRBBb;
thus card (ff"{x}) = b.(s/.i) by L1
.= b1.(s/.i) + b2.(s/.i) by POLYNOM1:def 5
.= 0+b2.(s/.i) by A2, POLYNOM1:def 7
.= card(g"{x}) by B2, C2, M1;
suppose A2: s/.i in support b1 & s/.i in support b2;then
B2: card(ff1"{x}) = b1.(s/.i) by H1, F1, B1, Aa, Ba, Ca, PWRBBb;
C2: card(ff2"{x}) = b2.(s/.i) by A2, H1, F1, B1, Ab, Bb, Cb, PWRBBb;
thus card (ff"{x}) = b.(s/.i) by L1
.= b1.(s/.i) + b2.(s/.i) by POLYNOM1:def 5
.= card(g"{x}) by B2, C2, M1;
end;
suppose A1: not x in rng ff; then
B1: ff"{x} = {} by FUNCT_1:142;
now assume x in rng g; then
AA: x in (rng ff1 \/ rng ff2) by FINSEQ_1:44;
per cases by AA, XBOOLE_0:def 2;
suppose x in rng ff1; then consider k being Nat such that
A2: k in dom ff1 and
B2: ff1.k = x by FINSEQ_2:11; consider i, j being Nat such that
C2: i in dom f1 and
D2: j in dom (f1.i) and k = (Sum Card (f1|(i-'1))) + j and
F2: (f1.i).j = ff1.k by A2, POLYNOM1:32;
G2: f1.i = fpoly_mult_root(s1/.i,b1.(s1/.i)) by C2, Ca;
H2: (f1.i).j = <% -s1/.i, 1_ L %> by D2, G2, LFPMR;
len s1 = card support b1 by Ba, LCFS;
then i in dom s1 by Aa, C2, FINSEQ_3:31; then
s1.i = s1/.i & s1.i in rng s1 by FINSEQ_4:def 4, FUNCT_1:12; then
s1/.i in support b1 by Ba, CFS1; then
K2a: s1/.i in support b by E, XBOOLE_0:def 2; then
s1/.i in rng s by B, CFS1; then consider l being Nat such that
L2: l in dom s and
M2: s.l = s1/.i by FINSEQ_2:11;
N2: l in dom f by A, L2, J, FINSEQ_3:31; then
O2: f.l = fpoly_mult_root(s/.l,b.(s/.l)) by C;
O2a: s.l = s/.l by L2, FINSEQ_4:def 4;
b.(s1/.i) <> 0 by K2a, POLYNOM1:def 7; then
0 < b.(s1/.i) by NAT_1:19; then
O2b: 0+1 <= b.(s1/.i) by NAT_1:38;
len (f.l) = b.(s/.l) by O2, LFPMR; then
P2: 1 in dom (f.l) by O2a, O2b, M2, FINSEQ_3:27; then
(Sum Card (f|(l-'1))) + 1 in dom ff &
(f.l).1 = ff.((Sum Card (f|(l-'1))) + 1) by N2, POLYNOM1:33; then
Q2: (f.l).1 in rng ff by FUNCT_1:12;
(f.l).1 = <% -s/.l, 1_ L %> by P2, O2, LFPMR;
hence contradiction by Q2, A1, M2, H2, F2, B2, O2a;
suppose x in rng ff2; then consider k being Nat such that
A2: k in dom ff2 and
B2: ff2.k = x by FINSEQ_2:11;
consider i, j being Nat such that
C2: i in dom f2 and
D2: j in dom (f2.i) and k = (Sum Card (f2|(i-'1))) + j and
F2: (f2.i).j = ff2.k by A2, POLYNOM1:32;
G2: f2.i = fpoly_mult_root(s2/.i,b2.(s2/.i)) by C2, Cb;
H2: (f2.i).j = <% -s2/.i, 1_ L %> by D2, G2, LFPMR;
len s2 = card support b2 by Bb, LCFS;
then i in dom s2 by Ab, C2, FINSEQ_3:31; then
s2.i = s2/.i & s2.i in rng s2 by FINSEQ_4:def 4, FUNCT_1:12; then
s2/.i in support b2 by Bb, CFS1; then
K2a: s2/.i in support b by E, XBOOLE_0:def 2; then
s2/.i in rng s by B, CFS1; then
consider l being Nat such that
L2: l in dom s and
M2: s.l = s2/.i by FINSEQ_2:11;
N2: l in dom f by A, L2, J, FINSEQ_3:31; then
O2: f.l = fpoly_mult_root(s/.l,b.(s/.l)) by C;
O2a: s.l = s/.l by L2, FINSEQ_4:def 4;
b.(s2/.i) <> 0 by K2a, POLYNOM1:def 7; then
0 < b.(s2/.i) by NAT_1:19; then
O2b: 0+1 <= b.(s2/.i) by NAT_1:38;
len (f.l) = b.(s/.l) by O2, LFPMR; then
P2: 1 in dom (f.l) by O2a, O2b, M2, FINSEQ_3:27; then
(Sum Card (f|(l-'1))) + 1 in dom ff &
(f.l).1 = ff.((Sum Card (f|(l-'1))) + 1) by N2, POLYNOM1:33; then
Q2: (f.l).1 in rng ff by FUNCT_1:12;
(f.l).1 = <% -s/.l, 1_ L %> by P2, O2, LFPMR;
hence contradiction by Q2, A1, M2, H2, F2, B2, O2a;
end; then
C1: g"{x} = {} by FUNCT_1:142;
thus card (ff"{x}) = card (g"{x}) by B1, C1;
end; then
ff, g are_fiberwise_equipotent by RFINSEQ:def 1; then
consider p being Permutation of dom FlattenSeq f such that
Z: FlattenSeq f = ((FlattenSeq f1) ^ (FlattenSeq f2)) * p by I, RFINSEQ:17;
thus poly_with_roots(b1+b2)
= Product ((FlattenSeq f1) ^ (FlattenSeq f2)) by I, Z, D, Permprod
.= (Product FlattenSeq f1) * (Product FlattenSeq f2) by FVSUM_1:101
.= (poly_with_roots b1)*'(poly_with_roots b2) by Da, Db, POLYNOM3:def 12;
end;
theorem :: PWRBR1
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
B: p.(len p-'1) = 1_ L;
len p > 0 by lenNZ; then
A: len p >= 0+1 by NAT_1:38;
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));
P1: P[1] proof let p be non-zero Polynomial of L such that
A1: len p = 1 and 1 >= 1 and
C1: p.(len p -'1) = 1_ L;
degree BRoots p = 0 by A1, BR1b; then
D1: BRoots p = EmptyBag the carrier of L by BAGDEG0;
len p -'1 = 0 by A1, GOBOARD9:1;
hence p = <%1_ L%> by A1, C1, ALGSEQ_1:def 6
.= poly_with_roots(BRoots(p)) by D1, poly1;
end;
PS: for n being Nat st n >= 1 & P[n] holds P[n+1] proof
let n be Nat such that
A1: n >= 1 and
B1: P[n];
let p being non-zero Polynomial of L such that
C1: len p = n+1 and n+1 >= 1 and
E1: p.(len p -'1) = 1_ L;
C1a: n+1 > 1 by A1, NAT_1:38; then
p is with_roots by C1, POLYNOM5:def 8; then
consider x being Element of L such that
F1: x is_a_root_of p by POLYNOM5:def 7;
set q = poly_quotient(p,x); set r = <%-x,1_ L%>;
x in Roots p by F1,POLYNOM5:def 9; then
x is_a_root_of p by POLYNOM5:def 9; then
G1: p = r*'q by BEZOUT;
len p > 0 by C1a, C1, AXIOMS:22; then p is non-zero by lenNZ; then
reconsider q as non-zero Polynomial of L by G1, LM1;
BRoots r = ({x},1)-bag by BR1e; then
H1: BRoots(p) = ({x},1)-bag + BRoots(q) by G1, BR1d;
1_ L <> 0.L by VECTSP_1:def 21; then
H1b: len r = 2 by POLYNOM5:41;
n+1 > 0 by C1a, AXIOMS:22; then
len q > 0 by lenNZ; then
r.(len r -'1) <> 0.L & q.(len q -'1) <> 0.L by H1b, LC1; then
r.(len r -'1) * q.(len q -'1) <> 0.L by VECTSP_2:def 5; then
len p = 2 + len q - 1 by H1b, G1, POLYNOM4:13; then
len p = len q + 2 - 1; then len p = len q + (1+1)- 1; then
len p = len q + 1+1- 1 by XCMPLX_1:1; then
len p = len q +1 by XCMPLX_1:26; then
I1a: len q = n by C1, XCMPLX_1:2;
q.(len q -'1) = 1_ L by G1, E1, LM3; then
I1: q = poly_with_roots(BRoots(q)) by I1a, A1, B1;
poly_with_roots(({x},1)-bag) = <%-x,1_ L%> by poly1_1;
hence p = poly_with_roots(BRoots(p)) by H1, I1, G1, PWRBB;
end;
for n being Nat st n >= 1 holds P[n] from Ind1(P1,PS);
hence p = poly_with_roots(BRoots(p)) by A, B;
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 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
A: len f = card s and
B: for i being 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);
C: len cs = card s by LCFS; card s <> 0 by GRAPH_5:5; then
0 < card s by NAT_1:19; then
D: 0+1 <= len f by A, NAT_1:38;
cs | Seg len f is FinSequence by FINSEQ_1:23; then
X: cs | Seg len f = cs by A, C, FINSEQ_2:23;
f | Seg len f is FinSequence by FINSEQ_1:23; then
Y: f | Seg len f = f by FINSEQ_2:23;
U: rng cs = s by CFS1;
W: dom f = dom cs by A, C, FINSEQ_3:31;
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);
P1: P[1] proof reconsider cs_1 = cs | Seg 1 as FinSequence of s by FINSEQ_1:23;
reconsider g = f | Seg 1 as FinSequence of cPRL by FINSEQ_1:23;
set t = rng cs_1;
consider s1 being Element of s such that
A1: cs_1 = <* s1 *> by A, C, D, QC_LANG4:7;
B1: 1 in Seg 1 by FINSEQ_1:3; 1 in dom cs by D, A, C, FINSEQ_3:27; then
reconsider cs1 = cs.1 as Element of s by FINSEQ_2:13;
C1: cs_1.1 = cs1 by B1, FUNCT_1:72;
cs1 in cL; then reconsider cs1 = cs.1 as Element of cL;
cs_1.1 = s1 by A1, FINSEQ_1:57; then
T1: t = {cs1} by A1, C1, FINSEQ_1:56;
reconsider t = {cs1} as finite Subset of cL;
consider p1 being Element of cPRL such that
D1: g = <* p1 *> by D, QC_LANG4:7;
D1a: 1 in dom f by D, FINSEQ_3:27; then
reconsider f1 = f.1 as Element of cPRL by FINSEQ_2:13;
E1: g.1 = f1 by B1, FUNCT_1:72;
F1: g.1 = p1 by D1, FINSEQ_1:57;
take t, g; thus t = rng (cs | Seg 1) & g = f | Seg 1 by T1;
G1: Product(g) = p1 by D1, FVSUM_1:99;
f1 = <% -cs1, 1_ L %> by D1a, B;
hence poly_with_roots((t,1)-bag) = Product(g) by poly1_1, G1, E1, F1;
end;
PIH: for j being Nat st 1 <= j & j < len f holds P[j] implies P[j+1]
proof let j be Nat such that
A1: 1 <= j and
B1: j < len f;
reconsider cs_j = cs | Seg j as FinSequence of s by FINSEQ_1:23;
reconsider cs_j1 = cs | Seg (j+1) as FinSequence of s by FINSEQ_1:23;
given t being finite Subset of cL, g being FinSequence of cPRL
such that
D1: t = rng (cs | Seg j) and
E1: g = f | Seg j and
F1: poly_with_roots((t,1)-bag) = Product(g);
reconsider g1 = f | Seg (j+1) as FinSequence of cPRL by FINSEQ_1:23;
set t1 = rng cs_j1;
F1a: 1 <= j+1 & j+1 <= len f by A1, B1, NAT_1:38; then
G1: j+1 in dom cs by A,C,FINSEQ_3:27; then cs.(j+1) in s by FINSEQ_2:13; then
cs.(j+1) in cL; then reconsider csj1 = cs.(j+1) as Element of cL;
Seg (j+1) = Seg j \/ {j+1} by FINSEQ_1:11; then
H1: cs_j1 = cs_j \/ cs|{j+1} by RELAT_1:107;
cs|{j+1} = (j+1) .--> csj1 by G1, FUNCT_7:6;
then rng (cs|{j+1}) = {csj1} by CQC_LANG:5; then
M1: t1 = t \/ {csj1} by H1, D1, RELAT_1:26; then
reconsider t1 as finite Subset of cL;
take t1, g1; thus t1 = rng (cs | Seg (j+1)) & g1 = f | Seg (j+1);
reconsider pt = poly_with_roots((t,1)-bag) as Polynomial of L;
reconsider ept = pt as Element of cPRL by POLYNOM3:def 12;
reconsider pj1 = poly_with_roots(({csj1},1)-bag) as Polynomial of L;
reconsider epj1 =<% -csj1, 1_ L %> as Element of cPRL by POLYNOM3:def 12;
consider l being Nat such that
I1a: len f = j+1+l by F1a, NAT_1:28;
I1: len g1 = j+1 by I1a, FINSEQ_3:59; j <= j+1 by NAT_1:37; then
Seg j c= Seg (j+1) by FINSEQ_1:7; then
J1: g = g1 | Seg j by E1, RELAT_1:103; j+1 in Seg (j+1) by FINSEQ_1:6; then
g1.(j+1) = f.(j+1) by FUNCT_1:72 .= <% -csj1, 1_ L %> by G1, W, B; then
K1: g1 = g ^ <* <% -csj1, 1_ L %> *> by I1, J1, FINSEQ_3:61;
L1: pj1 = epj1 by poly1_1;
t misses {csj1} proof assume not thesis; then
t /\ {csj1} <> {} by XBOOLE_0:def 7; then
consider x being set such that
A2: x in t /\ {csj1} by XBOOLE_0:def 1;
B2: x in t & x in {csj1} by A2, XBOOLE_0:def 3; then
C2: x = csj1 by TARSKI:def 1;
consider i being set such that
D2: i in dom (cs | Seg j) and
E2: x = (cs | Seg j).i by B2, D1, FUNCT_1:def 5;
F2: i in Seg j by D2, RELAT_1:86; then
reconsider i as Nat;
G2: 1 <= i & i <= j by F2, FINSEQ_1:3;
H2: i < j+1 by G2, NAT_1:38; x = cs.i by D2, E2, FUNCT_1:70;
hence contradiction by A, C2,G2,H2,F1a,C,U,GRAPH_5:10;
end; then
(t1,1)-bag = (t,1)-bag + ({csj1},1)-bag by M1, Snbagsum;
hence poly_with_roots((t1,1)-bag) = pt *' pj1 by PWRBB
.= ept * epj1 by L1, POLYNOM3:def 12 .= Product(g) * epj1 by F1
.= Product(g1) by K1, FVSUM_1:100;
end;
Z: for i being Nat st 1 <= i & i <= len f holds P[i] from FinInd(P1,PIH);
consider t being finite Subset of cL, g being FinSequence of cPRL such that
Z1: t = rng (cs | Seg len f) and
Z2: g = f | Seg len f and
Z4: poly_with_roots((t,1)-bag) = Product(g) by D, Z;
thus poly_with_roots((s,1)-bag) = Product(f) by Z1, Z2, Z4, X, Y, U;
end;
theorem :: PolyEval1:
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 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;
set cPRL = the carrier of Polynom-Ring L;
let s be non empty finite Subset of cL, x be Element of cL,
f be FinSequence of L such that
A: len f = card s and
B: for i being 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);
C: len cs = card s by LCFS;
card s <> 0 by GRAPH_5:5; then 0 < card s by NAT_1:19; then
D: 0+1 <= len f by A, NAT_1:38;
cs | Seg len f is FinSequence by FINSEQ_1:23; then
X: cs | Seg len f = cs by A, C, FINSEQ_2:23;
f | Seg len f is FinSequence by FINSEQ_1:23; then
Y: f | Seg len f = f by FINSEQ_2:23;
U: rng cs = s by CFS1;
W: dom f = dom cs by A, C, FINSEQ_3:31;
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);
P1: P[1] proof
reconsider cs_1 = cs | Seg 1 as FinSequence of s by FINSEQ_1:23;
reconsider g = f | Seg 1 as FinSequence of cL by FINSEQ_1:23;
set t = rng cs_1;
consider s1 being Element of s such that
A1: cs_1 = <* s1 *> by A, C, D, QC_LANG4:7;
B1: 1 in Seg 1 by FINSEQ_1:3;
1 in dom cs by D, A, C, FINSEQ_3:27; then
reconsider cs1 = cs.1 as Element of s by FINSEQ_2:13;
C1: cs_1.1 = cs1 by B1, FUNCT_1:72;
cs1 in cL; then reconsider cs1 = cs.1 as Element of cL;
cs_1.1 = s1 by A1, FINSEQ_1:57; then
T1: t = {cs1} by A1, C1, FINSEQ_1:56;
reconsider t = {cs1} as finite Subset of cL;
consider p1 being Element of cL such that
D1: g = <* p1 *> by D, QC_LANG4:7;
D1a: 1 in dom f by D, FINSEQ_3:27; then
reconsider f1 = f.1 as Element of cL by FINSEQ_2:13;
E1: g.1 = f1 by B1, FUNCT_1:72;
F1: g.1 = p1 by D1, FINSEQ_1:57;
take t, g; thus t = rng (cs | Seg 1) & g = f | Seg 1 by T1;
G1: Product(g) = p1 by D1, FVSUM_1:99;
f1 = eval(<% -cs1, 1_ L %>,x) by D1a, B;
hence eval(poly_with_roots((t,1)-bag),x) = Product(g) by poly1_1,G1,E1,F1;
end;
PIH: for j being Nat st 1 <= j & j < len f holds P[j] implies P[j+1]
proof let j be Nat such that
A1: 1 <= j and
B1: j < len f;
reconsider cs_j = cs | Seg j as FinSequence of s by FINSEQ_1:23;
reconsider cs_j1 = cs | Seg (j+1) as FinSequence of s by FINSEQ_1:23;
given t being finite Subset of cL, g being FinSequence of cL
such that
D1: t = rng (cs | Seg j) and
E1: g = f | Seg j and
F1: eval(poly_with_roots((t,1)-bag),x) = Product(g);
reconsider g1 = f | Seg (j+1) as FinSequence of cL by FINSEQ_1:23;
set t1 = rng cs_j1;
F1a: 1 <= j+1 & j+1 <= len f by A1, B1, NAT_1:38; then
G1: j+1 in dom cs by A,C,FINSEQ_3:27; then cs.(j+1) in s by FINSEQ_2:13; then
cs.(j+1) in cL; then reconsider csj1 = cs.(j+1) as Element of cL;
Seg (j+1) = Seg j \/ {j+1} by FINSEQ_1:11; then
H1: cs_j1 = cs_j \/ cs|{j+1} by RELAT_1:107;
cs|{j+1} = (j+1) .--> csj1 by G1, FUNCT_7:6;
then rng (cs|{j+1}) = {csj1} by CQC_LANG:5; then
M1: t1 = t \/ {csj1} by H1, D1, RELAT_1:26; then
reconsider t1 as finite Subset of cL;
take t1, g1; thus t1 = rng (cs | Seg (j+1)) & g1 = f | Seg (j+1);
reconsider pt = poly_with_roots((t,1)-bag) as Polynomial of L;
reconsider pj1 = poly_with_roots(({csj1},1)-bag) as Polynomial of L;
reconsider epj1 = <% -csj1, 1_ L %> as Element of cPRL
by POLYNOM3:def 12;
consider l being Nat such that
I1a: len f = j+1+l by F1a, NAT_1:28;
I1: len g1 = j+1 by I1a, FINSEQ_3:59;
j <= j+1 by NAT_1:37; then
Seg j c= Seg (j+1) by FINSEQ_1:7; then
J1: g = g1 | Seg j by E1, RELAT_1:103;
j+1 in Seg (j+1) by FINSEQ_1:6; then
g1.(j+1) = f.(j+1) by FUNCT_1:72
.= eval(<% -csj1, 1_ L %>,x) by G1, W, B; then
K1: g1 = g ^ <* eval(<% -csj1, 1_ L %>,x) *> by I1, J1, FINSEQ_3:61;
L1: pj1 = <% -csj1, 1_ L %> by poly1_1;
t misses {csj1} proof assume not thesis; then
t /\ {csj1} <> {} by XBOOLE_0:def 7; then
consider x being set such that
A2: x in t /\ {csj1} by XBOOLE_0:def 1;
B2: x in t & x in {csj1} by A2, XBOOLE_0:def 3; then
C2: x = csj1 by TARSKI:def 1;
consider i being set such that
D2: i in dom (cs | Seg j) and
E2: x = (cs | Seg j).i by B2, D1, FUNCT_1:def 5;
F2: i in Seg j by D2, RELAT_1:86; then reconsider i as Nat;
G2: 1 <= i & i <= j by F2, FINSEQ_1:3;
H2: i < j+1 by G2, NAT_1:38; x = cs.i by D2, E2, FUNCT_1:70;
hence contradiction by A, C2,G2,H2,F1a,C,U,GRAPH_5:10;
end; then
(t1,1)-bag = (t,1)-bag + ({csj1},1)-bag by M1, Snbagsum; then
poly_with_roots((t1,1)-bag) = pt *' pj1 by PWRBB;
hence eval(poly_with_roots((t1,1)-bag),x)
= eval(pt,x) * eval(pj1,x) by POLYNOM4:27
.= Product(g) * eval(pj1,x) by F1
.= Product(g1) by K1, L1, FVSUM_1:100;
end;
Z: for i being Nat st 1 <= i & i <= len f holds P[i] from FinInd(P1,PIH);
consider t being finite Subset of cL, g being FinSequence of cL such that
Z1: t = rng (cs | Seg len f) and
Z2: g = f | Seg len f and
Z4: eval(poly_with_roots((t,1)-bag),x) = Product(g) by D, Z;
thus eval(poly_with_roots((s,1)-bag),x) = Product(f) by Z1, Z2, Z4, X, Y, U;
end;