:: Artin's Theorem towards the Existence of Algebraic Closures
:: by Christoph Schwarzweller
::
:: Received September 30, 2022
:: Copyright (c) 2022-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies ARYTM_3, VECTSP_1, ALGSTR_0, TARSKI, EQREL_1, STRUCT_0, MOD_4,
SUBSET_1, SUPINF_2, POLYNOM8, FUNCT_2, NAT_1, MESFUNC1, C0SP1, CARD_1,
PRE_POLY, GROUP_6, POLYNOM1, POLYNOM3, FUNCSDOM, RLVECT_1, GROUP_2,
EC_PF_1, HURWITZ, FINSEQ_1, FINSET_1, ORDINAL4, FUNCT_1, RELAT_1,
BINOP_1, FUNCT_7, FINSEQ_5, RFINSEQ, XBOOLE_0, NUMBERS, POLYNOM5,
GROUP_1, ORDINAL1, ZFMISC_1, AFINSQ_1, VECTSP_2, CARD_3, RATFUNC1,
RING_1, RING_2, WELLORD2, RING_3, MSSUBFAM, LATTICES, IDEAL_1, CARD_FIL,
GROUP_4, GROEB_2, FDIFF_1, UPROOTS, ALGNUM_1, ARYTM_1, FIELD_4, FIELD_2,
FOMODEL1, REALSET1, CAT_3, WELLORD1, XXREAL_0, QUOFIELD, XCMPLX_0,
NEWTON, FUNCOP_1, FUNCT_4, FIELD_1, PARTFUN1, POLYNOM2, POLYNOM4,
POLYNOM7, WAYBEL20, ORDERS_1, FIELD_11;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, DOMAIN_1, BINOP_1, RELAT_1,
RELSET_1, ORDINAL1, FUNCT_1, FUNCT_2, ORDERS_1, RECDEF_1, FINSEQ_5,
RFINSEQ, NUMBERS, CARD_1, CARD_3, PARTFUN1, REALSET1, WELLORD1, WELLORD2,
XCMPLX_0, XXREAL_0, NAT_1, NAT_D, FUNCOP_1, INT_1, VFUNCT_1, FUNCT_4,
FUNCT_7, FINSET_1, ALGSEQ_1, FINSEQ_1, PRE_POLY, UPROOTS, POLYNOM3,
POLYNOM1, POLYNOM2, POLYNOM5, POLYNOM4, POLYNOM7, STRUCT_0, GROUP_1,
GROUP_4, GROUP_6, MOD_4, BINOM, ALGSTR_0, QUOFIELD, IDEAL_1, RLVECT_1,
VECTSP_2, HURWITZ, VECTSP_1, C0SP1, EC_PF_1, RATFUNC1, RINGCAT1, EQREL_1,
RING_1, RING_2, RING_3, RING_4, ALGNUM_1, FIELD_1, FIELD_2, FIELD_3,
FIELD_4;
constructors BINOP_1, REAL_1, FINSOP_1, BINARITH, VECTSP_2, POLYNOM3, C0SP1,
ALGSTR_1, MCART_1, NUMBERS, RING_1, ZFMISC_1, RELAT_1, HURWITZ, VALUED_0,
VECTSP_1, STRUCT_0, POLYNOM4, XBOOLE_0, RELSET_1, ARYTM_3, QUOFIELD,
PARTFUN1, RLVECT_1, FUNCT_7, NAT_D, FINSEQ_1, VFUNCT_1, CARD_1, FINSET_1,
TSEP_1, RATFUNC1, FINSEQ_3, GCD_1, GROUP_6, FUNCT_5, REALSET1, ALGSTR_2,
BINOM, RINGCAT1, MEMBERED, IDEAL_1, RING_3, EC_PF_1, FINSEQ_5, ALGSEQ_1,
RING_2, PRE_POLY, EQREL_1, POLYDIFF, RLVECT_5, RING_4, FUNCOP_1, GROUP_4,
ALGNUM_1, GROUP_1, RECDEF_1, POLYNOM1, POLYNOM2, FVSUM_1, CARD_3, MOD_4,
ORDINAL2, WELLORD2, POLYNOM7, ORDERS_1, UPROOTS, INT_1, POLYNOM5,
FIELD_4, FIELD_1, FIELD_2, FIELD_5, FIELD_6, RFINSEQ, FIELD_7;
registrations XBOOLE_0, ORDINAL1, RELSET_1, FUNCOP_1, XXREAL_0, XREAL_0,
NAT_1, INT_1, STRUCT_0, VECTSP_1, ALGSTR_1, GCD_1, EC_PF_1, VALUED_0,
FUNCT_2, ALGSTR_0, ALGSEQ_1, SUBSET_1, RLVECT_1, QUOFIELD, PRE_POLY,
MOD_4, POLYDIFF, FUNCT_1, PARTFUN1, VFUNCT_1, CARD_1, FINSET_1, RATFUNC1,
EQREL_1, RELAT_1, RINGCAT1, FINSEQ_1, RING_1, RING_2, RING_3, RING_4,
RING_5, GROUP_1, GROUP_4, GROUP_6, IDEAL_1, WELLORD2, REALSET1, POLYNOM1,
POLYNOM2, POLYNOM3, POLYNOM4, POLYNOM5, POLYNOM7, ALGNUM_1, FIELD_1,
FIELD_2, FIELD_4, FIELD_7;
requirements NUMERALS, SUBSET, BOOLE, REAL, ARITHM;
definitions STRUCT_0, ALGSTR_0, ALGSTR_1, VECTSP_1, VECTSP_2, REALSET1,
GROUP_1, RLVECT_1, TARSKI, BINOP_1, ORDERS_1, IDEAL_1, XBOOLE_0, FUNCT_1,
GCD_1, QUOFIELD, POLYNOM3, FINSEQ_1, GROUP_6;
equalities BINOP_1, REALSET1, XCMPLX_0, STRUCT_0, ALGSTR_0, POLYNOM3, GCD_1,
FUNCOP_1, VECTSP_1, QUOFIELD, ALGNUM_1, RING_4, ORDERS_1, FINSEQ_1,
WELLORD1;
expansions STRUCT_0, GROUP_1, ALGSTR_0, ALGSTR_1, RLVECT_1, VECTSP_1, GCD_1,
TARSKI, GROUP_6, QUOFIELD, BINOP_1, ORDERS_1, IDEAL_1, FINSEQ_1, FUNCT_1,
FUNCT_2, RING_4;
theorems GROUP_1, VECTSP_1, RLVECT_1, IDEAL_1, SUBSET_1, C0SP1, PARTFUN1,
FUNCT_2, TARSKI, ALGNUM_1, FUNCT_1, RELAT_1, POLYNOM1, POLYNOM4, FIELD_7,
RATFUNC1, POLYNOM5, UPROOTS, RING_4, RING_5, NAT_2, PBOOLE, HURWITZ,
NAT_1, XREAL_1, INT_1, BINOM, XBOOLE_0, FUNCT_7, FIELD_2, FIELD_4,
ALGSEQ_1, RING_2, FUNCOP_1, POLYNOM3, RING_3, CARD_1, ZFMISC_1, XXREAL_0,
PRE_POLY, XBOOLE_1, FINSEQ_1, NORMSP_1, ORDINAL1, FIELD_1, WELLORD2,
RELAT_2, BHSP_1, RFINSEQ, FUNCT_4, XREAL_0, RING_1, RINGCAT1, CARD_2,
POLYNOM2, FIELD_5, ORDERS_1, POLYNOM7, FINSEQ_2, FINSEQ_3, FINSEQ_5,
POLYDIFF, FIELD_8;
schemes FINSEQ_1, FINSEQ_2, FUNCT_2, NAT_1;
begin
:: Preliminaries about bags and multivariate polynomials
theorem Th13e:
for n,m being Ordinal
for b1,b2 being bag of n
st support b1 = {m} & support b2 = {m} holds b1 <=' b2 iff b1.m <= b2.m
proof
let n,m be Ordinal, b1,b2 be bag of n;
assume H0: support b1 = {m} & support b2 = {m};
H1: now let l be Ordinal;
assume l <> m;
then H2: not l in support b1 & not l in support b2 by H0,TARSKI:def 1;
hence b1.l = 0 by PRE_POLY:def 7;
thus b2.l = 0 by H2,PRE_POLY:def 7;
end;
A: now assume A1: b1 <=' b2;
per cases;
suppose b1 = b2;
hence b1.m <= b2.m;
end;
suppose b1 <> b2; then
consider k being Ordinal such that
A3: b1.k < b2.k & for l being Ordinal st l in k holds b1.l = b2.l
by A1,PRE_POLY:def 10,PRE_POLY:def 9;
k = m by H1,A3;
hence b1.m <= b2.m by A3;
end;
end;
now assume A1: b1.m <= b2.m;
per cases;
suppose b1 = b2;
hence b1 <=' b2;
end;
suppose A4: b1 <> b2;
A2: now assume A5: b1.m = b2.m;
now let o be object;
assume A6: o in n;
per cases;
suppose o = m;
hence b1.o = b2.o by A5;
end;
suppose A7: o <> m;
hence b1.o = 0 by H1,A6 .= b2.o by A6,A7,H1;
end;
end;
hence contradiction by A4,PBOOLE:def 10;
end;
ex k being Ordinal st b1.k < b2.k &
for l being Ordinal st l in k holds b1.l = b2.l
proof
take k = m;
thus b1.k < b2.k by A2,A1,XXREAL_0:1;
now let l be Ordinal;
assume l in k;
then A3: l <> m;
hence b1.l = 0 by H1 .= b2.l by A3,H1;
end;
hence thesis;
end;
hence b1 <=' b2 by PRE_POLY:def 9,PRE_POLY:def 10;
end;
end;
hence thesis by A;
end;
theorem Th13h:
for n,m being Ordinal
for b1,b2 being bag of n st support b1 = {m}
holds b2 divides b1 iff (b2 = EmptyBag n or (support b2 = {m} & b2.m <= b1.m))
proof
let n,m be Ordinal; let b1,b2 be bag of n;
assume AS: support b1 = {m};
A: now assume b2 = EmptyBag n or (support b2 = {m} & b2.m <= b1.m); then
per cases;
suppose b2 = EmptyBag n;
hence b2 divides b1 by PRE_POLY:59;
end;
suppose A2: support b2 = {m} & b2.m <= b1.m;
now let k be object;
assume k in n;
per cases;
suppose k = m;
hence b2.k <= b1.k by A2;
end;
suppose k <> m; then
A3: not k in {m} by TARSKI:def 1;
then b2.k = 0 by A2,PRE_POLY:def 7
.= b1.k by A3,AS,PRE_POLY:def 7;
hence b2.k <= b1.k;
end;
end;
hence b2 divides b1 by PRE_POLY:46;
end;
end;
H: now let l be object;
assume l <> m;
then not l in support b1 by AS,TARSKI:def 1;
hence b1.l = 0 by PRE_POLY:def 7;
end;
now assume A4: b2 divides b1;
then A5: b2 <=' b1 by PRE_POLY:49;
assume A6: b2 <> EmptyBag n;
support b2 = {m}
proof
B: now let o be object;
assume B1: o in support b2;
now assume o <> m;
then b1.o = 0 by H;
then b2.o = 0 by A4,PRE_POLY:def 11;
hence contradiction by B1,PRE_POLY:def 7;
end;
hence o in {m} by TARSKI:def 1;
end;
now let o be object;
assume o in {m};
then B2: o = m by TARSKI:def 1;
now assume B3: b2.m = 0;
now let u be object;
assume u in n;
per cases;
suppose u = m;
hence b2.u = {} by B3;
end;
suppose u <> m;
then b1.u = 0 by H;
hence b2.u = {} by A4,PRE_POLY:def 11;
end;
end;
hence contradiction by A6,PBOOLE:6;
end;
hence o in support b2 by B2,PRE_POLY:def 7;
end;
hence thesis by B,TARSKI:2;
end;
hence support b2 = {m} & b2.m <= b1.m by A5,AS,Th13e;
end;
hence thesis by A;
end;
theorem Th13f:
for F being Field,
m,n being Ordinal
for b being bag of n st support b = {m} holds
len(divisors b) = b.m + 1 &
for k being Nat, S being finite Subset of n st S = {m} &
k in dom(divisors b) holds (divisors b).k = (S,k-'1)-bag
proof
let F being Field, m,n be Ordinal; let b be bag of n;
assume AS: support b = {m};
per cases;
suppose A: not(m in n);
now let o be object;
assume o in n;
then not o in support b by A,AS,TARSKI:def 1;
hence b.o = {} by PRE_POLY:def 7 .= (EmptyBag n).o by PBOOLE:5;
end; then
B: b = EmptyBag n by PBOOLE:def 10; then
C: b.m = 0 by PBOOLE:5;
D: divisors b = <* EmptyBag n *> by B,PRE_POLY:67; then
E: dom(divisors b) = { 1 } by FINSEQ_1:2,FINSEQ_1:38;
thus len(divisors b) = b.m + 1 by C,D,FINSEQ_1:40;
now let k be Nat, S be finite Subset of n;
assume H: S = {m} & k in dom(divisors b);
then I: k = 1 by E,TARSKI:def 1; then
F: (divisors b).k = EmptyBag n by D;
k -' 1 = k - 1 by H,E,XREAL_0:def 2;
hence (divisors b).k = (S,k-'1)-bag by F,I,UPROOTS:9;
end;
hence thesis;
end;
suppose m in n; then
for o being object st o in {m} holds o in n by TARSKI:def 1; then
reconsider S = {m} as finite Subset of n by TARSKI:def 3;
deffunc g(Nat) = (S,$1-'1)-bag;
consider F being FinSequence such that
A: len F = b.m + 1 &
for k being Nat st k in dom F holds F.k = g(k) from FINSEQ_1:sch 2;
set B = { (S,i)-bag where i is Element of NAT : i <= b.m };
F: B is finite
proof
defpred P[set] means 1 = 1;
set G = { g(i) where i is Nat: i <= b.m+1 & P[i] };
H: G is finite from FINSEQ_1:sch 6;
B c= G
proof
now let o be object;
assume o in B; then
consider i being Element of NAT such that
H1: o = (S,i)-bag & i <= b.m;
H2: i + 1 <= b.m + 1 by H1,XREAL_1:6;
i + 1 -' 1 = i + 1 - 1 by XREAL_0:def 2;
hence o in G by H1,H2;
end;
hence thesis;
end;
hence thesis by H;
end;
G: B c= Bags n
proof
now let o be object;
assume o in B; then
consider i being Element of NAT such that
H1: o = (S,i)-bag & i <= b.m;
thus o in Bags n by H1;
end;
hence thesis;
end;
(S,0)-bag in B; then
reconsider B as non empty finite Subset of Bags n by F,G;
D: rng F = B
proof
D0: now let o be object;
assume o in rng F; then
consider i being Nat such that
D1: i in dom F & F.i = o by FINSEQ_2:10;
D2: o = (S,i-'1)-bag by D1,A;
dom F = Seg(len F) by FINSEQ_1:def 3; then
D3: 1 <= i & i <= b.m + 1 by D1,A,FINSEQ_1:1; then
D4: i - 1 <= b.m + 1 - 1 by XREAL_1:9;
i - 1 = i -' 1 by D3,XREAL_0:def 2;
hence o in B by D2,D4;
end;
now let o be object;
assume o in B; then
consider i being Element of NAT such that
D1: o = (S,i)-bag & i <= b.m;
D2: i + 1 -' 1 = i + 1 - 1 by XREAL_0:def 2;
1 <= i + 1 & i + 1 <= b.m + 1 by D1,XREAL_1:6,NAT_1:11; then
i + 1 in Seg(len F) by A; then
D3: i + 1 in dom F by FINSEQ_1:def 3; then
F.(i+1) = o by A,D2,D1;
hence o in rng F by D3,FUNCT_1:def 3;
end;
hence thesis by D0,TARSKI:2;
end; then
reconsider F as FinSequence of Bags n by FINSEQ_1:def 4;
field(BagOrder n) = Bags n by ORDERS_1:12; then
C: BagOrder n linearly_orders B by ORDERS_1:37,ORDERS_1:38;
for x,y being Nat st x in dom F & y in dom F & x < y
holds F/.x <> F/.y & [F/.x,F/.y] in BagOrder n
proof
let x,y being Nat;
assume C1: x in dom F & y in dom F & x < y; then
C2: F/.x = F.x & F/.y = F.y by PARTFUN1:def 6;
dom F = Seg(len F) by FINSEQ_1:def 3; then
1 <= x & 1 <= y by C1,FINSEQ_1:1; then
C4: x -' 1 = x - 1 & y -' 1 = y - 1 by XREAL_0:def 2; then
C7: x -' 1 < y -' 1 by C1,XREAL_1:9;
C5: F.x = (S,x-'1)-bag & F.y = (S,y-'1)-bag by C1,A;
C6: m in {m} by TARSKI:def 1;
thus F/.x <> F/.y
proof
(F.x).m = x -' 1 & (F.y).m = y -' 1 by C5,C6,UPROOTS:7;
hence thesis by C4,C2,C1;
end;
thus [F/.x,F/.y] in BagOrder n
proof
(S,x-'1)-bag <=' (S,y-'1)-bag
proof
per cases;
suppose x -' 1 = 0; then
(S,x-'1)-bag = EmptyBag n by UPROOTS:9;
hence thesis by PRE_POLY:60;
end;
suppose x -' 1 <> 0; then
D2: support (S,x-'1)-bag = {m} by UPROOTS:8;
D3: (S,x-'1)-bag.m = x -' 1 by C6,UPROOTS:7;
D4: support (S,y-'1)-bag = {m} by C7,UPROOTS:8;
(S,y-'1)-bag.m = y -' 1 by C6,UPROOTS:7;
hence thesis by C7,D2,D3,D4,Th13e;
end;
end;
hence thesis by C2,C5,PRE_POLY:def 14;
end;
end; then
B: F = SgmX(BagOrder n, B) by C,D,PRE_POLY:def 2;
H: for p being bag of n holds p in B iff p divides b
proof
let p be bag of n;
B1: now assume p in B; then
consider i being Element of NAT such that
B2: p = (S,i)-bag & i <= b.m;
per cases;
suppose i = 0; then
(S,i)-bag = EmptyBag n by UPROOTS:9;
hence p divides b by B2,PRE_POLY:59;
end;
suppose i <> 0; then
B3: support (S,i)-bag = {m} by UPROOTS:8;
now let k be object;
per cases;
suppose B4: k = m;
m in {m} by TARSKI:def 1;
hence p.k <= b.k by B2,B4,UPROOTS:7;
end;
suppose k <> m;
then not k in support p by B2,B3,TARSKI:def 1;
hence p.k <= b.k by PRE_POLY:def 7;
end;
end;
hence p divides b by PRE_POLY:def 11;
end;
end;
now assume p divides b; then
per cases by AS,Th13h;
suppose p = EmptyBag n;
then p = (S,0)-bag by UPROOTS:9;
hence p in B;
end;
suppose B2: support p = {m} & p.m <= b.m;
p = (S,p.m)-bag
proof
now let o be object;
assume o in n;
per cases;
suppose o in support p;
then B3: o = m by B2,TARSKI:def 1;
m in {m} by TARSKI:def 1;
hence p.o = (S,p.m)-bag.o by B3,UPROOTS:7;
end;
suppose B3: not o in support p;
hence p.o = 0 by PRE_POLY:def 7
.= (S,p.m)-bag.o by B3,B2,UPROOTS:6;
end;
end;
hence thesis by PBOOLE:3;
end;
hence p in B by B2;
end;
end;
hence thesis by B1;
end; then
E: F = divisors b by B,PRE_POLY:def 16;
thus len(divisors b) = b.m + 1 by A,B,H,PRE_POLY:def 16;
thus for k being Nat, S being finite Subset of n st S = {m} &
k in dom(divisors b) holds (divisors b).k = (S,k-'1)-bag by A,E;
end;
end;
registration
let n be Ordinal;
let L be right_zeroed add-associative right_complementable
right_unital distributive non degenerated doubleLoopStr;
cluster Polynom-Ring(n,L) -> non degenerated;
coherence
proof
set P = Polynom-Ring(n,L);
now assume 1.P = 0.P; then
1_(n,L) = 0.P by POLYNOM1:def 11 .= 0_(n,L) by POLYNOM1:def 11; then
1.L = (0_(n,L)).EmptyBag n by POLYNOM1:25 .= 0.L by POLYNOM1:22;
hence contradiction;
end;
hence thesis;
end;
end;
theorem ringext:
for R being non degenerated comRing
for S being comRingExtension of R
for n being Ordinal
holds Polynom-Ring(n,S) is comRingExtension of Polynom-Ring(n,R)
proof
let R be non degenerated comRing, S be comRingExtension of R, n be Ordinal;
A1: R is Subring of S by FIELD_4:def 1; then
A2: the carrier of R c= the carrier of S by C0SP1:def 3;
A3: 0.S = 0.R by A1,C0SP1:def 3;
X1: for p being Polynomial of n,R holds p is Polynomial of n,S
proof
let p be Polynomial of n,R;
rng p c= the carrier of R by RELAT_1:def 19; then
rng p c= the carrier of S by A2; then
reconsider p1 = p as Series of n,S by FUNCT_2:6;
now let o be object;
assume
A5: o in Support p1; then
reconsider b = o as Element of Bags n;
A6: 0.R <> p.b by A3,A5,POLYNOM1:def 3;
dom p = Bags n by FUNCT_2:def 1;
hence o in Support p by A6,POLYNOM1:def 3;
end; then
Support p1 c= Support p;
hence thesis by POLYNOM1:def 5;
end;
X2: the carrier of Polynom-Ring(n,R) c= the carrier of Polynom-Ring(n,S)
proof
now let o be object;
assume o in the carrier of Polynom-Ring(n,R); then
o is Polynomial of n,R by POLYNOM1:def 11; then
o is Polynomial of n,S by X1;
hence o in the carrier of Polynom-Ring(n,S) by POLYNOM1:def 11;
end;
hence thesis;
end;
X3: 0.(Polynom-Ring(n,R)) = 0_(n,R) by POLYNOM1:def 11
.= (Bags n) --> 0.R by POLYNOM1:def 8
.= (Bags n) --> 0.S by A1,C0SP1:def 3
.= 0_(n,S) by POLYNOM1:def 8
.= 0.(Polynom-Ring(n,S)) by POLYNOM1:def 11;
H: 0_(n,R) = (Bags n) --> 0.R by POLYNOM1:def 8
.= (Bags n) --> 0.S by A1,C0SP1:def 3
.= 0_(n,S) by POLYNOM1:def 8;
X4: 1.(Polynom-Ring(n,R)) = 1_(n,R) by POLYNOM1:def 11
.= 0_(n,R)+*(EmptyBag n,1.R) by POLYNOM1:def 9
.= 0_(n,S)+*(EmptyBag n,1.S) by H,A1,C0SP1:def 3
.= 1_(n,S) by POLYNOM1:def 9
.= 1.(Polynom-Ring(n,S)) by POLYNOM1:def 11;
X5: for p,q being Polynomial of n,R
for p1,q1 being Polynomial of n,S st p = p1 & q = q1 holds p + q = p1 + q1
proof
let p,q be Polynomial of n,R; let p1,q2 be Polynomial of n,S;
assume
A1: p = p1 & q = q2;
A2: R is Subring of S by FIELD_4:def 1;
now let b be Element of Bags n;
p.b = p1.b & q.b = q2.b by A1; then
A3: [p1.b,q2.b] in [:the carrier of R,the carrier of R:] by ZFMISC_1:def 2;
thus (p+q).b = p.b + q.b by POLYNOM1:15
.= ((the addF of S)||the carrier of R).(p1.b,q2.b) by A1,A2,C0SP1:def 3
.= p1.b + q2.b by A3,FUNCT_1:49
.= (p1+q2).b by POLYNOM1:15;
end;
hence thesis;
end;
X6: the addF of Polynom-Ring(n,R)
= (the addF of Polynom-Ring(n,S))||the carrier of Polynom-Ring(n,R)
proof
set aR = the addF of Polynom-Ring(n,R),
aS = (the addF of Polynom-Ring(n,S))||the carrier of Polynom-Ring(n,R);
set cR = the carrier of Polynom-Ring(n,R),
cS = the carrier of Polynom-Ring(n,S);
A2: dom aS = dom(the addF of Polynom-Ring(n,S)) /\ [:cR,cR:] by RELAT_1:61
.= [:cS,cS:] /\ [:cR,cR:] by FUNCT_2:def 1
.= [:cR,cR:] by X2,ZFMISC_1:96,XBOOLE_1:28
.= dom aR by FUNCT_2:def 1;
now let o be object;
assume
A3: o in dom aR; then
consider p,q being object such that
A4: p in the carrier of Polynom-Ring(n,R) &
q in the carrier of Polynom-Ring(n,R) & o = [p,q] by ZFMISC_1:def 2;
reconsider p,q as Element of cR by A4;
reconsider p1 = p, q1 = q as Element of cS by X2;
reconsider p2 = p, q2 = q as Polynomial of n,R by POLYNOM1:def 11;
reconsider p3 = p1, q3 = q1 as Polynomial of n,S by POLYNOM1:def 11;
thus
aR.o = p + q by A4
.= p2 + q2 by POLYNOM1:def 11
.= p3 + q3 by X5
.= p1 + q1 by POLYNOM1:def 11
.= aS.o by A2,A3,A4,FUNCT_1:47;
end;
hence thesis by A2;
end;
X7: for p,q being Polynomial of n,R
for p1,q1 being Polynomial of n,S st p = p1 & q = q1 holds p*'q = p1*'q1
proof
let p,q be Polynomial of n,R; let p1,qq be Polynomial of n,S;
assume
A1: p = p1 & q = qq;
A2: R is Subring of S by FIELD_4:def 1;
now let b be bag of n;
consider r being FinSequence of the carrier of R such that
A3: (p*'q).b = Sum r & len r = len decomp b &
for k being Element of NAT st k in dom r ex b1, b2 being bag of n st
(decomp b)/.k = <*b1,b2*> & r/.k = p.b1*q.b2 by POLYNOM1:def 10;
consider r1 being FinSequence of the carrier of S such that
A4: (p1*'qq).b = Sum r1 & len r1 = len decomp b &
for k being Element of NAT st k in dom r1 ex b1, b2 being bag of n st
(decomp b)/.k = <*b1,b2*> & r1/.k = (p1.b1)*(qq.b2) by POLYNOM1:def 10;
A5: dom r1 = Seg(len r) by A3,A4,FINSEQ_1:def 3
.= dom r by FINSEQ_1:def 3;
now let m be Nat;
assume
A6: m in dom r; then
consider b1, b2 being bag of n such that
B1: (decomp b)/.m = <*b1,b2*> & r/.m = p.b1*q.b2 by A3;
consider b11, b22 being bag of n such that
B2: (decomp b)/.m = <*b11,b22*> & r1/.m = p1.b11*qq.b22 by A5,A6,A4;
B3: b11 = <*b1,b2*>.1 by B1,B2,FINSEQ_1:44 .= b1;
B4: b22 = <*b1,b2*>.2 by B1,B2,FINSEQ_1:44 .= b2;
p.b1 = p1.b1 & q.b2 = qq.b2 by A1; then
A7: [p1.b1,qq.b2] in [:the carrier of R,the carrier of R:]
by ZFMISC_1:def 2;
thus
r.m = p.b1 * q.b2 by B1,A6,PARTFUN1:def 6
.= ((the multF of S)||the carrier of R).(p1.b1,qq.b2)
by A1,A2,C0SP1:def 3
.= p1.b11 * qq.b22 by B3,B4,A7,FUNCT_1:49
.= r1.m by B2,A6,A5,PARTFUN1:def 6;
end; then
r = r1 by A5;
hence (p*'q).b = (p1*'qq).b by A4,A3,A2,FIELD_4:2;
end;
hence thesis;
end;
X8: the multF of Polynom-Ring(n,R)
= (the multF of Polynom-Ring(n,S))||the carrier of Polynom-Ring(n,R)
proof
set mR = the multF of Polynom-Ring(n,R),
mS = (the multF of Polynom-Ring(n,S))||the carrier of Polynom-Ring(n,R);
set cR = the carrier of Polynom-Ring(n,R),
cS = the carrier of Polynom-Ring(n,S);
A2: dom mS = dom(the multF of Polynom-Ring(n,S)) /\ [:cR,cR:] by RELAT_1:61
.= [:cS,cS:] /\ [:cR,cR:] by FUNCT_2:def 1
.= [:cR,cR:] by X2,ZFMISC_1:96,XBOOLE_1:28
.= dom mR by FUNCT_2:def 1;
now let o be object;
assume
A3: o in dom mR; then
consider p,q being object such that
A4: p in cR & q in cR & o = [p,q] by ZFMISC_1:def 2;
reconsider p,q as Element of cR by A4;
reconsider p1 = p, q1 = q as Element of cS by X2;
reconsider p2 = p, q2 = q as Polynomial of n,R by POLYNOM1:def 11;
reconsider p3 = p1, q3 = q1 as Polynomial of n,S by POLYNOM1:def 11;
thus
mR.o = p * q by A4
.= p2 *' q2 by POLYNOM1:def 11
.= p3 *' q3 by X7
.= p1 * q1 by POLYNOM1:def 11
.= mS.o by A2,A3,A4,FUNCT_1:47;
end;
hence thesis by A2;
end;
(Polynom-Ring(n,R)) is Subring of (Polynom-Ring(n,S))
by X2,X3,X4,X6,X8,C0SP1:def 3;
hence thesis by FIELD_4:def 1;
end;
definition
let R be non degenerated Ring;
let n be Ordinal;
let p be Polynomial of n,R;
func Leading-Term p -> bag of n equals :defLT:
SgmX(BagOrder n,Support p).(len SgmX(BagOrder n,Support p)) if p <> 0_(n,R)
otherwise EmptyBag n;
consistency;
coherence
proof
set S = SgmX(BagOrder n,Support p);
per cases;
suppose p = 0_(n,R);
hence thesis;
end;
suppose I: p <> 0_(n,R);
field(BagOrder n) = Bags n by ORDERS_1:12; then
BagOrder n linearly_orders Support p by ORDERS_1:37,ORDERS_1:38; then
B: rng S = Support p by PRE_POLY:def 2;
Support p <> {} by I,POLYNOM2:17; then
len S >= 1 by FINSEQ_1:20; then
len S in Seg(len S); then
len S in dom S by FINSEQ_1:def 3; then
S.(len S) in rng S by FUNCT_1:3;
hence thesis by B;
end;
end;
end;
definition
let R be non degenerated Ring;
let n be Ordinal;
let p be Polynomial of n,R;
func Leading-Coefficient p -> Element of R equals
p.(Leading-Term p);
coherence;
end;
definition
let R be non degenerated Ring;
let n be Ordinal;
let p be Polynomial of n,R;
func Leading-Monomial p -> Monomial of n,R equals
Monom(Leading-Coefficient p,Leading-Term p);
coherence;
end;
notation
let R be non degenerated Ring;
let n be Ordinal;
let p be Polynomial of n,R;
synonym LC p for Leading-Coefficient p;
synonym Lt p for Leading-Term p;
synonym LM p for Leading-Monomial p;
end;
theorem YY:
for R being non degenerated Ring
for n being Ordinal
for p being Polynomial of n,R holds p = 0_(n,R) iff Support p = {}
proof
let R be non degenerated Ring, n be Ordinal, p be Polynomial of n,R;
A: now assume B: p = 0_(n,R);
now let o be object;
assume C: o in Support p;
then reconsider b1 = o as Element of Bags n;
p.b1 <> 0.R by C,POLYNOM1:def 4;
hence contradiction by B,POLYNOM1:22;
end;
hence Support p = {} by XBOOLE_0:def 1;
end;
now assume Support p = {};
then p = (Bags n) --> 0.R by POLYNOM1:def 4;
hence p = 0_(n,R) by POLYNOM1:def 8;
end;
hence thesis by A;
end;
theorem Y0:
for R being non degenerated Ring
for n being Ordinal
for p being Polynomial of n,R holds LC p = 0.R iff p = 0_(n,R)
proof
let R be non degenerated Ring, n be Ordinal, p be Polynomial of n,R;
H: Lt p is Element of Bags n by PRE_POLY:def 12;
A: now assume p = 0_(n,R);
then Support p = {} by YY;
hence LC p = 0.R by H,POLYNOM1:def 4;
end;
now assume LC p = 0.R;
then B: not Lt p in Support p by POLYNOM1:def 4;
field(BagOrder n) = Bags n by ORDERS_1:12; then
K: BagOrder n linearly_orders Support p by ORDERS_1:37,ORDERS_1:38;
now assume I: p <> 0_(n,R); then
G: Lt p = SgmX(BagOrder n,Support p).(len SgmX(BagOrder n,Support p))
by defLT;
L: rng SgmX(BagOrder n,Support p) = Support p by K,PRE_POLY:def 2;
Support p <> {} by I,YY;
then M: 1 <= len SgmX(BagOrder n,Support p) by FINSEQ_1:20;
dom SgmX(BagOrder n,Support p) = Seg(len SgmX(BagOrder n,Support p))
by FINSEQ_1:def 3; then
len SgmX(BagOrder n,Support p) in dom SgmX(BagOrder n,Support p)
by M;
hence contradiction by B,L,G,FUNCT_1:def 3;
end;
hence p = 0_(n,R);
end;
hence thesis by A;
end;
theorem LT1:
for R being non degenerated Ring
for n being Ordinal
for p being Polynomial of n,R
for b being bag of n st b in Support p
holds b = Lt p iff for b1 being bag of n st b1 in Support p holds b1 <=' b
proof
let R be non degenerated Ring, n be Ordinal, p be Polynomial of n,R;
let b be bag of n;
set F = SgmX(BagOrder n,Support p);
assume AS1: b in Support p; then
AS2: p <> 0_(n,R) by YY;
field(BagOrder n) = Bags n by ORDERS_1:12; then
AS3: BagOrder n linearly_orders Support p by ORDERS_1:37,ORDERS_1:38;
card(Support p) >= 0 + 1 by AS1,INT_1:7; then
1 <= len F by AS3,PRE_POLY:11; then
len F in Seg(len F); then
AS4: len F in dom F by FINSEQ_1:def 3; then
AS5: F.(len F) = F/.(len F) by PARTFUN1:def 6;
A: now assume AS6: b = Lt p; then
A0: b = F.(len F) by AS2,defLT;
thus for b1 being bag of n st b1 in Support p holds b1 <=' b
proof
let b1 be bag of n;
assume b1 in Support p; then
b1 in rng F by AS3,PRE_POLY:def 2; then
consider o being object such that
A1: o in dom F & b1 = F.o by FUNCT_1:def 3;
reconsider i = o as Element of NAT by A1;
A2: F.i = F/.i by A1,PARTFUN1:def 6;
i in Seg(len F) by A1,FINSEQ_1:def 3; then
i <= len F by FINSEQ_1:1; then
per cases by XXREAL_0:1;
suppose i = len F;
hence thesis by AS6,A1,AS2,defLT;
end;
suppose i < len F;
then [b1,b] in BagOrder n by A0,A1,A2,AS4,AS5,AS3,PRE_POLY:def 2;
hence b1 <=' b by PRE_POLY:def 14;
end;
end;
end;
now assume B: for b1 being bag of n st b1 in Support p holds b1 <=' b;
now let y being Element of Bags n;
assume y in Support p;
then y <=' b by B;
hence [y,b] in BagOrder n by PRE_POLY:def 14;
end;
then b = F/.(len F) by AS1,AS3,PRE_POLY:21
.= F.(len F) by AS4,PARTFUN1:def 6;
hence b = Lt p by AS2,defLT;
end;
hence thesis by A;
end;
theorem YZ:
for R being non degenerated Ring
for n being Ordinal
for p being Polynomial of n,R holds Support(LM p) c= Support p
proof
let R be non degenerated Ring, n be Ordinal, p be Polynomial of n,R;
now let o be object;
assume A: o in Support(LM p);
then reconsider b = o as Element of Bags n;
B: (LM p).b <> 0.R by A,POLYNOM1:def 4;
D: Lt p is Element of Bags n by PRE_POLY:def 12;
C: dom 0_(n,R) = Bags n by FUNCT_2:def 1;
E: LM p = 0_(n,R) +* (Lt p,LC p) by POLYNOM7:def 4
.= 0_(n,R) +* (Lt p .--> LC p) by C,D,FUNCT_7:def 3;
per cases;
suppose H: b in dom(Lt p .--> LC p); then
I: b = Lt p by TARSKI:def 1;
(LM p).b = (Lt p .--> LC p).b by H,E,FUNCT_4:13
.= LC p by I,FUNCOP_1:72;
hence o in Support p by B,I,POLYNOM1:def 4;
end;
suppose not b in dom(Lt p .--> LC p); then
(LM p).b = (0_(n,R)).b by E,FUNCT_4:11 .= 0.R by POLYNOM1:22;
hence o in Support p by A,POLYNOM1:def 4;
end;
end;
hence thesis;
end;
theorem Th14x:
for F being Field
for n being Ordinal
for p being Monomial of n,F holds LC p = coefficient p & Lt p = term p
proof
let F be Field, n be Ordinal, p be Monomial of n,F;
H: Lt p is Element of Bags n &
term(p) is Element of Bags n by PRE_POLY:def 12;
field(BagOrder n) = Bags n by ORDERS_1:12; then
A: BagOrder n linearly_orders Support(p) by ORDERS_1:37,ORDERS_1:38;
per cases by POLYNOM7:def 5;
suppose p.term(p) <> 0.F;
then AS: term(p) in Support p by H,POLYNOM1:def 4;
then B: Support p = {term(p)} by POLYNOM7:7; then
C: rng SgmX(BagOrder n,Support p) = {term(p)} by A,PRE_POLY:def 2;
F: card Support p = 1 by B,CARD_1:30; then
D: len SgmX(BagOrder n,Support p) = 1 by A,PRE_POLY:11;
E: SgmX(BagOrder n,Support p) = <*term(p)*> by F,C,A,PRE_POLY:11,FINSEQ_1:39;
p <> 0_(n,F) by AS,YY; then
Lt p = SgmX(BagOrder n,Support p).1 by D,defLT
.= term(p) by E;
hence thesis by POLYNOM7:def 6;
end;
suppose J: Support p = {} & term(p) = EmptyBag n; then
K: LC p = 0.F by H,POLYNOM1:def 4; then
L: LC p = p.(term(p)) by J,POLYNOM1:def 4
.= coefficient(p) by POLYNOM7:def 6; then
p = Monom(0.F,term(p)) by K,POLYNOM7:11; then
M: term(p) = EmptyBag n by POLYNOM7:8;
p = 0_(n,F) by J,YY;
hence thesis by M,L,defLT;
end;
end;
theorem Z2:
for R being non degenerated Ring
for n being Ordinal
for p being Polynomial of n,R
holds Support(LM p) = {} or Support(LM p) = {Lt p}
proof
let R be non degenerated Ring, n be Ordinal, p be Polynomial of n,R;
set m = LM p;
per cases by POLYNOM7:6;
suppose Support(LM p) = {};
hence thesis;
end;
suppose ex b being bag of n st Support(LM p) = {b};
then consider b being bag of n such that H: Support(LM p) = {b};
per cases;
suppose Support p = {};
then p = 0_(n,R) by YY;
then Lt p = EmptyBag n & 0.R = p.b by defLT,POLYNOM1:22;
then not b in Support p by POLYNOM1:def 4;
then not b in Support(LM p) by YZ,TARSKI:def 3;
hence thesis by H,TARSKI:def 1;
end;
suppose Support p <> {};
then p <> 0_(n,R) by YY;
then I: LC p is non zero by Y0;
{b} = {term(m)} by H,POLYNOM7:7;
then b in {term(m)} by TARSKI:def 1;
then b = term(m) by TARSKI:def 1 .= Lt p by I,POLYNOM7:10;
hence thesis by H;
end;
end;
end;
lemY:
for R being non degenerated Ring
for n being Ordinal
for p being Polynomial of n,R holds (LM p).(Lt p) = LC p
proof
let R be non degenerated Ring, n be Ordinal, p be Polynomial of n,R;
D: Lt p is Element of Bags n by PRE_POLY:def 12;
C: dom 0_(n,R) = Bags n by FUNCT_2:def 1;
B: Lt p in dom(Lt p .--> LC p) by TARSKI:def 1;
LM p = 0_(n,R) +* (Lt p,LC p) by POLYNOM7:def 4
.= 0_(n,R) +* (Lt p .--> LC p) by C,D,FUNCT_7:def 3;
hence (LM p).(Lt p)
= (Lt p .--> LC p).(Lt p) by B,FUNCT_4:13
.= LC p by FUNCOP_1:72;
end;
theorem Z2a:
for R being non degenerated Ring
for n being Ordinal
for p being Polynomial of n,R holds LM p = 0_(n,R) iff p = 0_(n,R)
proof
let R be non degenerated Ring, n be Ordinal, p be Polynomial of n,R;
H: Lt p is Element of Bags n by PRE_POLY:def 12;
A: now assume p = 0_(n,R);
then B: Support p = {} by YY;
Support(LM p) c= Support p by YZ;
then Support(LM p) = {} by B;
hence LM p = 0_(n,R) by YY;
end;
now assume LM p = 0_(n,R);
then Support(LM p) = {} by YY;
then 0.R = (LM p).(Lt p) by H,POLYNOM1:def 4 .= LC p by lemY;
hence p = 0_(n,R) by Y0;
end;
hence thesis by A;
end;
W2: for R being non degenerated Ring
for n being Ordinal
for p being Polynomial of n,R
holds for b being bag of n st b <> Lt p holds (LM p).b = 0.R
proof
let R be non degenerated Ring, n be Ordinal;
let p be Polynomial of n,R, b be bag of n;
now assume AS: (LM p).b <> 0.R;
b is Element of Bags n by PRE_POLY:def 12; then
A: b in Support(LM p) by AS,POLYNOM1:def 4;
now assume b <> Lt p;
then not b in {Lt p} by TARSKI:def 1;
hence contradiction by Z2,A;
end;
hence b = Lt p;
end;
hence thesis;
end;
theorem
for R being non degenerated Ring
for n being Ordinal
for p being Polynomial of n,R
holds (LM p).(Lt p) = LC p &
for b being bag of n st b <> Lt p holds (LM p).b = 0.R by lemY,W2;
lemZ:
for R being non degenerated Ring
for n being Ordinal
for p being Polynomial of n,R holds Lt (LM p) = Lt p
proof
let R be non degenerated Ring, n be Ordinal, p be Polynomial of n,R;
H: Lt p is Element of Bags n by PRE_POLY:def 12;
field(BagOrder n) = Bags n by ORDERS_1:12; then
I: BagOrder n linearly_orders Support(LM p) by ORDERS_1:37,ORDERS_1:38;
per cases;
suppose AS: p = 0_(n,R); then
B: Support p = {} by YY;
Support(LM p) c= Support p by YZ; then
Support(LM p) = {} by B;
hence thesis by AS,YY;
end;
suppose p <> 0_(n,R); then
LC p <> 0.R by Y0; then
(LM p).(Lt p) <> 0.R by lemY; then
A: Lt p in Support(LM p) by H,POLYNOM1:def 4; then
B: Support(LM p) = {Lt p} by Z2; then
E: card Support(LM p) = 1 by CARD_1:30; then
C: len SgmX(BagOrder n,Support LM p) = 1 by I,PRE_POLY:11;
rng SgmX(BagOrder n,Support LM p) = {Lt p} by I,B,PRE_POLY:def 2; then
D: SgmX(BagOrder n,Support LM p) = <*Lt p*> by E,I,PRE_POLY:11,FINSEQ_1:39;
E: LM p <> 0_(n,R) by A,YY;
thus Lt (LM p) = <* Lt p *>.1 by C,D,E,defLT .= Lt p;
end;
end;
theorem
for R being non degenerated Ring
for n being Ordinal
for p being Polynomial of n,R holds Lt (LM p) = Lt p & LC (LM p) = LC p
proof
let R be non degenerated Ring, n be Ordinal, p be Polynomial of n,R;
thus Lt (LM p) = Lt p by lemZ;
thus LC (LM p) = (LM p).(Lt p) by lemZ .= LC p by lemY;
end;
theorem T4a:
for n being Ordinal
for R being non degenerated Ring
for a,b being Element of R holds a|(n,R) + b|(n,R) = (a + b)|(n,R)
proof
let n be Ordinal, L be non degenerated Ring; let a,b be Element of L;
set p = (a+b)|(n,L);
A2: now let x be object;
assume x in dom p;
then reconsider i = x as Element of Bags n;
per cases;
suppose H: i = EmptyBag n;
thus (a|(n,L) + b|(n,L)).x
= ((a|(n,L)).i) + ((b|(n,L)).i) by POLYNOM1:15
.= a + ((b|(n,L)).i) by H,POLYNOM7:18
.= a + b by H,POLYNOM7:18
.= p.x by H,POLYNOM7:18;
end;
suppose H: i <> EmptyBag n;
thus (a|(n,L) + b|(n,L)).x
= ((a|(n,L)).i) + ((b|(n,L)).i) by POLYNOM1:15
.= 0.L + ((b|(n,L)).i) by H,POLYNOM7:18
.= 0.L by H,POLYNOM7:18
.= p.x by H,POLYNOM7:18;
end;
end;
dom p = Bags n by FUNCT_2:def 1;
hence thesis by A2;
end;
theorem T4:
for n being Ordinal
for R being non degenerated Ring
for a,b being Element of R holds a|(n,R) *' (b|(n,R)) = (a * b)|(n,R)
proof
let n be Ordinal, L be non degenerated Ring; let a,b be Element of L;
set p = (a*b)|(n,L), q = (a|(n,L) *' (b|(n,L)));
set ap = a|(n,L), bp = b|(n,L);
A2: now let x be object;
assume x in dom p;
then reconsider i = x as Element of Bags n;
consider s being FinSequence of the carrier of L such that
A3: q.i = Sum s & len s = len decomp i &
for k being Element of NAT st k in dom s
ex b1,b2 being bag of n
st (decomp i)/.k = <*b1,b2*> & s/.k = ap.b1*bp.b2 by POLYNOM1:def 10;
per cases;
suppose H0: i <> EmptyBag n;
H1: for b1,b2 being bag of n
st b1 <> EmptyBag n or b2 <> EmptyBag n holds ap.b1*bp.b2 = 0.L
proof
let b1,b2 be bag of n;
assume b1 <> EmptyBag n or b2 <> EmptyBag n; then
per cases;
suppose b1 <> EmptyBag n;
then ap.b1 = 0.L by POLYNOM7:18;
hence thesis;
end;
suppose b2 <> EmptyBag n;
then bp.b2 = 0.L by POLYNOM7:18;
hence thesis;
end;
end;
1 <= len(decomp i) by NAT_1:14;
then 1 in Seg(len s) by A3;
then H2: 1 in dom s by FINSEQ_1:def 3;
H3: for k being Element of NAT st k in dom s holds s/.k = 0.L
proof
let k be Element of NAT;
assume H4: k in dom s;
then consider b1,b2 being bag of n such that
H5: (decomp i)/.k = <*b1,b2*> & s/.k = ap.b1 * bp.b2 by A3;
H8: dom s = Seg(len decomp i) by A3,FINSEQ_1:def 3
.= dom(decomp i) by FINSEQ_1:def 3;
then H6: b1 = (divisors i)/.k by H4,H5,PRE_POLY:70;
then (decomp i)/.k = <*b1,i-'b1*> by H4,H8,PRE_POLY:def 17;
then H10: b2 = i -' b1 by H5,FINSEQ_1:77;
dom divisors i = dom decomp i by PRE_POLY:def 17;
then H7: k in Seg(len divisors i) by H4,H8,FINSEQ_1:def 3;
then H11: 1 <= k & k <= len divisors i by FINSEQ_1:1;
per cases;
suppose k = 1;
then b1 = EmptyBag n by H6,PRE_POLY:65;
then b2 = i by H10,PRE_POLY:54;
hence thesis by H0,H1,H5;
end;
suppose k <> 1; then
H8: 1 < k by H11,XXREAL_0:1;
per cases by XXREAL_0:1;
suppose k = len divisors i;
then b1 = i by H6,PRE_POLY:65;
hence thesis by H0,H1,H5;
end;
suppose k < len divisors i;
then b1 <> EmptyBag n by H8,H6,PRE_POLY:66;
hence thesis by H5,H1;
end;
suppose k > len divisors i;
hence thesis by H7,FINSEQ_1:1;
end;
end;
end;
then for k being Element of NAT st k in dom s & k <> 1 holds s/.k = 0.L;
then Sum s = s/.1 by H2,POLYNOM2:3 .= ap.i * 0.L by H3,H2;
hence q.x = p.x by H0,A3,POLYNOM7:18;
end;
suppose AS: i = EmptyBag n;
then F: decomp i = <* <*EmptyBag n,EmptyBag n*> *> by PRE_POLY:73;
then F1: len(decomp i) = 1 & (decomp i).1 = <*EmptyBag n,EmptyBag n*>
by FINSEQ_1:40;
dom(decomp i) = Seg 1 by F,FINSEQ_1:38;
then F2: (decomp i)/.1 = <*EmptyBag n,EmptyBag n*>
by F1,FINSEQ_1:3,PARTFUN1:def 6;
H4: 1 = len s by F,A3,FINSEQ_1:40;
then 1 in Seg(len s);
then H3: 1 in dom s by FINSEQ_1:def 3;
then consider b1,b2 being bag of n such that
H2: (decomp i)/.1 = <*b1,b2*> & s/.1 = ap.b1 * bp.b2 by A3;
s = <*s.1*> by H4,FINSEQ_1:40 .= <*s/.1*> by H3,PARTFUN1:def 6;
then Sum s = ap.b1 * bp.b2 by H2,RLVECT_1:44
.= ap.(EmptyBag n) * bp.b2 by F2,H2,FINSEQ_1:77
.= ap.(EmptyBag n) * bp.(EmptyBag n) by F2,H2,FINSEQ_1:77
.= a * bp.(EmptyBag n) by POLYNOM7:18
.= a * b by POLYNOM7:18;
hence q.x = p.x by AS,A3,POLYNOM7:18;
end;
end;
dom p = Bags n by FUNCT_2:def 1;
hence thesis by A2;
end;
:: Extended evaluation of multivariate polynomials
definition
let R,S be non degenerated comRing;
let n be Ordinal;
let p be Polynomial of n,R;
let x be Function of n,S;
func Ext_eval(p,x) -> Element of S means :defeval:
ex y being FinSequence of S
st it = Sum y & len y = len SgmX(BagOrder n, Support p) &
for i being Element of NAT st 1 <= i & i <= len y
holds y.i = In( (p * SgmX(BagOrder n, Support p)).i, S) *
eval(SgmX(BagOrder n, Support p)/.i,x);
existence
proof
deffunc G(Nat) = In( (p * SgmX(BagOrder n, Support p)).$1, S) *
eval(((SgmX(BagOrder n, Support p))/.$1),x);
consider F be FinSequence of S such that
A1: len F = len SgmX(BagOrder n, Support p) and
A2: for n be Nat st n in dom F holds F.n = G(n) from FINSEQ_2:sch 1;
take a = Sum F;
take F;
thus a = Sum F & len F = len SgmX(BagOrder n, Support p) by A1;
now let i be Element of NAT;
assume 1 <= i & i <= len F;
then i in Seg(len F);
then i in dom F by FINSEQ_1:def 3;
hence F.i = In( (p * SgmX(BagOrder n, Support p)).i, S) *
eval(((SgmX(BagOrder n, Support p))/.i),x) by A2;
end;
hence thesis;
end;
uniqueness
proof
let y1,y2 be Element of S such that
A1: ex F1 being FinSequence of S
st y1 = Sum F1 & len F1 = len SgmX(BagOrder n, Support p) &
for i being Element of NAT st 1 <= i & i <= len F1
holds F1.i = In( (p * SgmX(BagOrder n, Support p)).i, S) *
eval(((SgmX(BagOrder n, Support p))/.i),x) and
A2: ex F2 being FinSequence of S
st y2 = Sum F2 & len F2 = len SgmX(BagOrder n, Support p) &
for i being Element of NAT st 1 <= i & i <= len F2
holds F2.i = In( (p * SgmX(BagOrder n, Support p)).i, S) *
eval(((SgmX(BagOrder n, Support p))/.i),x);
consider F1 being FinSequence of S such that
A3: y1 = Sum F1 and
A4: len F1 = len SgmX(BagOrder n, Support p) and
A5: for i being Element of NAT st 1 <= i & i <= len F1
holds F1.i = In( (p * SgmX(BagOrder n, Support p)).i, S) *
eval(((SgmX(BagOrder n, Support p))/.i),x) by A1;
consider F2 being FinSequence of S such that
A6: y2 = Sum F2 and
A7: len F2 = len SgmX(BagOrder n, Support p) and
A8: for i being Element of NAT st 1 <= i & i <= len F2
holds F2.i = In( (p * SgmX(BagOrder n, Support p)).i, S) *
eval(((SgmX(BagOrder n, Support p))/.i),x) by A2;
A9: dom F1 = Seg(len F2) by A4,A7,FINSEQ_1:def 3;
now
let i be Nat;
A13: i is Element of NAT by ORDINAL1:def 12;
assume
A10: i in dom F1; then
i in Seg(len F1) by FINSEQ_1:def 3; then
A14: 1 <= i & i <= len F1 by FINSEQ_1:1;
A15: 1 <= i & i <= len F2 by A10,A9,FINSEQ_1:1;
thus F1.i = In( (p * SgmX(BagOrder n, Support p)).i, S) *
eval(((SgmX(BagOrder n, Support p))/.i),x) by A5,A14,A13
.= F2.i by A8,A15,A13;
end;
hence thesis by A3,A4,A6,A7,FINSEQ_2:9;
end;
end;
theorem ev0:
for R,S being non degenerated comRing
for n being Ordinal
for x being Function of n,S holds Ext_eval(0_(n,R),x) = 0.S
proof
let A,B be non degenerated comRing, n be Ordinal, x be Function of n,B;
set p = 0_(n,A);
consider y being FinSequence of the carrier of B such that
A: Ext_eval(p,x) = Sum y & len y = len SgmX(BagOrder n, Support p) &
for i being Element of NAT st 1 <= i & i <= len y
holds y.i = In( (p * SgmX(BagOrder n, Support p)).i, B) *
eval(((SgmX(BagOrder n, Support p))/.i),x) by defeval;
field(BagOrder n) = Bags n by ORDERS_1:12; then
B: BagOrder n linearly_orders (Support p) by ORDERS_1:37,ORDERS_1:38;
Support p = {} by YY;
then card(Support p) = 0;
then y = <*>the carrier of B by A,B,PRE_POLY:11;
hence thesis by A,RLVECT_1:43;
end;
theorem eval1:
for R,S being non degenerated comRing
for n being Ordinal
for x being Function of n,S
st R is Subring of S holds Ext_eval(1_(n,R),x) = 1.S
proof
let A,B be non degenerated comRing; let n be Ordinal;
let x be Function of n,B;
set p = 1_(n,A);
assume
A0: A is Subring of B;
field(BagOrder n) = Bags n by ORDERS_1:12; then
B0: BagOrder n linearly_orders (Support p) by ORDERS_1:37,ORDERS_1:38;
C: p = 1.Polynom-Ring(n,A) &
0_(n,A) = 0.Polynom-Ring(n,A) by POLYNOM1:def 11;
consider y being FinSequence of B such that
A1: Ext_eval(p,x) = Sum y & len y = len SgmX(BagOrder n, Support p) &
for i being Element of NAT st 1 <= i & i <= len y
holds y.i = In( (p * SgmX(BagOrder n, Support p)).i, B) *
eval(((SgmX(BagOrder n, Support p))/.i),x) by defeval;
B1: Support p = { EmptyBag n } by C,POLYNOM7:14; then
A2: card(Support p) = 1 by CARD_1:30; then
A3: len y = 1 by A1,B0,PRE_POLY:11;
rng SgmX(BagOrder n, Support p) = {EmptyBag n} by B0,B1,PRE_POLY:def 2;
then
A5: SgmX(BagOrder n, Support p) = <* EmptyBag n *>
by A2,B0,PRE_POLY:11,FINSEQ_1:39; then
J: dom SgmX(BagOrder n, Support p) = Seg 1 by FINSEQ_1:38;
B2: SgmX(BagOrder n, Support p)/.1
= SgmX(BagOrder n, Support p).1 by J,PARTFUN1:def 6,FINSEQ_1:3
.= EmptyBag n by A5;
I: 1.B = 1.A by A0,C0SP1:def 3;
B3: (p * SgmX(BagOrder n, Support p)).1
= p.(SgmX(BagOrder n, Support p).1) by J,FUNCT_1:13,FINSEQ_1:3
.= p.(EmptyBag n) by B2,J,PARTFUN1:def 6,FINSEQ_1:3
.= 1.A by POLYNOM1:25;
A4: y.1 = In( (p * SgmX(BagOrder n, Support p)).1, B) *
eval(((SgmX(BagOrder n, Support p))/.1),x) by A1,A3
.= 1.B by I,B3,B2,POLYNOM2:14;
Sum y = Sum <*1.B*> by A2,A4,A1,B0,PRE_POLY:11,FINSEQ_1:40
.= 1.B by RLVECT_1:44;
hence thesis by A1;
end;
Lm6: for n being Ordinal, R,S being non degenerated comRing
for p,q being Polynomial of n,R, x being Function of n, S,
b being bag of n st not(b in Support p) & Support q = Support p \/ {b} &
for b1 being bag of n st b1 <> b holds q.b1 = p.b1
holds Ext_eval(q,x) = Ext_eval(p,x) + In(q.b,S) * eval(b,x)
proof
let n be Ordinal, R,S be non degenerated comRing;
let p,q be Polynomial of n,R, x be Function of n, S, b be bag of n;
assume that
A1: not b in Support p and
A2: Support q = Support p \/ {b} and
A3: for b9 being bag of n st b9 <> b holds q.b9 = p.b9;
set sq = SgmX(BagOrder n, Support q), sp = SgmX(BagOrder n, Support p);
A4: BagOrder n linearly_orders Support q by POLYNOM2:18;
b in {b} by TARSKI:def 1;
then b in Support q by A2,XBOOLE_0:def 3;
then b in rng sq by A4,PRE_POLY:def 2;
then consider k being Nat such that
A5: k in dom sq and
A6: sq.k = b by FINSEQ_2:10;
A7: sq/.k = b by A5,A6,PARTFUN1:def 6;
reconsider b as Element of Bags n by PRE_POLY:def 12;
A8: dom sq = Seg(len sq) by FINSEQ_1:def 3;
then
A9: k <= len sq by A5,FINSEQ_1:1;
1 <= k by A5,A8,FINSEQ_1:1;
then reconsider k9 = k - 1 as Element of NAT by INT_1:3;
A10: k9 + 1 = k + 0;
then
A11: sq = Ins(sp,k9,b) by A1,A2,A5,A7,POLYNOM2:18,PRE_POLY:80;
consider yp being FinSequence of S such that
A13: Ext_eval(p,x) = Sum yp and
A12: len yp = len sp and
A14: for i being Element of NAT st 1 <= i & i <= len yp
holds yp.i = In((p * sp).i,S) * eval((sp/.i),x) by defeval;
consider yq being FinSequence of S such that
A16: Ext_eval(q,x) = Sum yq and
A15: len yq = len sq and
A17: for i being Element of NAT st 1 <= i & i <= len yq
holds yq.i = In((q * sq).i,S) * eval((sq/.i),x) by defeval;
VA: dom yq = dom sq by A15,FINSEQ_3:29;
reconsider b as Element of Bags n;
set ytmp = Ins(yp,k9,In(q.b,S) * eval(b,x));
A18: len sp + 1 = (card(Support p) + 1) by POLYNOM2:18,PRE_POLY:11
.= card(Support q) by A1,A2,CARD_2:41
.= len sq by POLYNOM2:18,PRE_POLY:11;
then
A19: len yq = len ytmp by A15,A12,FINSEQ_5:69;
A20: BagOrder n linearly_orders Support p by POLYNOM2:18;
A21: for i being Nat st 1 <= i & i <= len yq holds yq.i = ytmp.i
proof
let i be Nat;
assume that
A22: 1 <= i and
A23: i <= len yq;
i in Seg len ytmp by A19,A22,A23;
then
A25: i in dom ytmp by FINSEQ_1:def 3;
per cases;
suppose
A26: i = k;
dom q = Bags n by FUNCT_2:def 1;
then sq.k in dom q by A6,PRE_POLY:def 12;
then
k in dom(q * sq) by A5,FUNCT_1:11;
then
A28: (q * sq).k = q.b by A6,FUNCT_1:12;
A29: yq.i = In((q * sq).k,S) * eval((sq/.k),x) by A5,A17,A22,A23,A26
.= In(q.b,S) * eval(b,x) by A5,A6,A28,PARTFUN1:def 6;
A30: k9 <= len yp by A8,A10,A12,A18,A5,FINSEQ_1:1,XREAL_1:6;
thus ytmp.i = yq.i by A29,A10,A26,A30,FINSEQ_5:73;
end;
suppose
A31: i <> k;
len(Ins(sp,k9,b)) = len sp + 1 by FINSEQ_5:69;
then
A32: dom(Ins(sp,k9,b)) = Seg(len(sp)+1) by FINSEQ_1:def 3;
now
per cases by A31,XXREAL_0:1;
case
A33: i < k;
k9 < k by A10,NAT_1:19;
then k9 < len yq by A9,A15,XXREAL_0:2;
then
A34: k9 <= len yp by A15,A12,A18,NAT_1:13;
A36: i <= k9 by A10,A33,NAT_1:13;
then i in Seg k9 by A22;
then
A37: i in dom(yp|k9) by A34,FINSEQ_1:17;
A38: k - 1 <= (len sp + 1) - 1 by A9,A18,XREAL_1:9;
then
A39: i <= len sp by A36,XXREAL_0:2;
then
A40: i in dom sp by A22,FINSEQ_3:25;
A41: now
assume sp/.i = b;
then sp.i = b by A40,PARTFUN1:def 6;
then b in rng sp by A40,FUNCT_1:def 3;
hence contradiction by A1,A20,PRE_POLY:def 2;
end;
i < len yq by A9,A15,A33,XXREAL_0:2;
then
A42: i <= len yp by A15,A12,A18,NAT_1:13;
A44: rng Ins(sp,k9,b) c= Bags n by FINSEQ_1:def 4;
A45: dom q = Bags n by FUNCT_2:def 1;
A46: rng sp c= Bags n by FINSEQ_1:def 4;
i in Seg k9 by A22,A36;
then
A47: i in dom(sp|k9) by A38,FINSEQ_1:17;
sp.i in rng sp by A40,FUNCT_1:def 3;
then sp.i in Bags n by A46;
then sp.i in dom p by FUNCT_2:def 1;
then
A48: i in dom(p * sp) by A40,FUNCT_1:11;
len sp <= len sp + 1 by XREAL_1:29;
then i <= len sp + 1 by A39,XXREAL_0:2;
then
A49: i in dom(Ins(sp,k9,b)) by A22,A32;
then Ins(sp,k9,b).i in rng Ins(sp,k9,b) by FUNCT_1:def 3;
then
i in dom(q * Ins(sp,k9,b)) by A49,A44,A45,FUNCT_1:11;
then
A51: (q * Ins(sp,k9,b)).i = q.(Ins(sp,k9,b).i) by FUNCT_1:12
.= q.(sp.i) by A47,FINSEQ_5:72
.= q.(sp/.i) by A40,PARTFUN1:def 6
.= p.(sp/.i) by A3,A41
.= p.(sp.i) by A40,PARTFUN1:def 6
.= (p * sp).i by A48,FUNCT_1:12;
Z1: sq/.i = sq.i & sp/.i = sp.i
by VA,A22,A23,FINSEQ_3:25,A40,PARTFUN1:def 6;
A52: yq.i = In((q * sq).i,S) * eval((sq/.i),x) by A17,A22,A23,A49
.= In((p * sp).i,S)*eval((sp/.i),x) by A11,A47,A51,FINSEQ_5:72,Z1
.= yp.i by A14,A22,A49,A42
.= ytmp.i by A37,FINSEQ_5:72
.= ytmp/.i by A25,PARTFUN1:def 6;
thus yq.i = ytmp.i by A25,A52,PARTFUN1:def 6;
end;
case
A53: i > k;
then reconsider i1 = i - 1 as Element of NAT by INT_1:3;
A54: (i - 1) + 1 = i + 0; then
A55: k9 + 1 <= i1 by A53,NAT_1:13;
A56: dom q = Bags n by FUNCT_2:def 1;
A57: rng Ins(sp,k9,b) c= Bags n by FINSEQ_1:def 4;
A58: dom p = Bags n by FUNCT_2:def 1;
A59: rng sp c= Bags n by FINSEQ_1:def 4;
A60: i - 1 <= (len yp + 1) - 1 by A15,A12,A18,A23,XREAL_1:9;
0 + 1 <= k9 + 1 by XREAL_1:6;
then 1 < i by A53,XXREAL_0:2; then
A61: 1 <= i1 by A54,NAT_1:13;
then i1 in Seg len sp by A12,A60;
then
A62: i1 in dom sp by FINSEQ_1:def 3;
A63: now
assume sp/.i1 = b;
then sp.i1 = b by A62,PARTFUN1:def 6;
then b in rng sp by A62,FUNCT_1:def 3;
hence contradiction by A1,A20,PRE_POLY:def 2;
end;
sp.i1 in rng sp by A62,FUNCT_1:def 3;
then
A64: i1 in dom(p * sp) by A62,A59,A58,FUNCT_1:11;
A65: i = i1 + 1;
A66: i in dom(Ins(sp,k9,b)) by A15,A18,A22,A23,A32;
then Ins(sp,k9,b).i in rng Ins(sp,k9,b) by FUNCT_1:def 3;
then
i in dom(q * Ins(sp,k9,b)) by A66,A57,A56,FUNCT_1:11;
then
A68: (q * Ins(sp,k9,b)).i
= q.(Ins(sp,k9,b).i) by FUNCT_1:12
.= q.(sp.i1) by A12,A60,A65,A55,FINSEQ_5:74
.= q.(sp/.i1) by A62,PARTFUN1:def 6
.= p.(sp/.i1) by A3,A63
.= p.(sp.i1) by A62,PARTFUN1:def 6
.= (p * sp).i1 by A64,FUNCT_1:12;
dom yq = dom sq by FINSEQ_3:29,A15; then
BB: sq/.i = sq.i by A22,A23,FINSEQ_3:25,PARTFUN1:def 6
.= sp.i1 by A12,A60,A65,A55,A11,FINSEQ_5:74
.= sp/.i1 by PARTFUN1:def 6,A62;
A69: yq.i
= In((p*sp).i1,S) * eval((sq/.i),x) by A68,A11,A17,A22,A23,A66
.= yp.i1 by A14,A60,A61,BB
.= ytmp.i by A60,A65,A55,FINSEQ_5:74
.= ytmp/.i by PARTFUN1:def 6,A25;
thus yq.i = ytmp.i by A25,A69,PARTFUN1:def 6;
end;
end;
hence thesis;
end;
end;
Sum((yp|k9)^<*In(q.b,S) * eval(b,x)*>^(yp/^k9))
= Sum((yp|k9)^<*In(q.b,S) * eval(b,x)*>) + Sum(yp/^k9)
by RLVECT_1:41
.= (Sum(yp|k9) + Sum(<*In(q.b,S) * eval(b,x)*>)) + Sum(yp/^k9)
by RLVECT_1:41
.= (Sum(yp|k9) + Sum(yp/^k9)) + Sum(<*In(q.b,S) * eval(b,x)*>)
by RLVECT_1:def 3
.= Sum((yp|k9)^(yp/^k9)) + Sum(<*In(q.b,S) * eval(b,x)*>)
by RLVECT_1:41
.= Sum yp + Sum(<*In(q.b,S) * eval(b,x)*>) by RFINSEQ:8
.= Ext_eval(p,x) + In(q.b,S) * eval(b,x) by A13,RLVECT_1:44;
then Sum ytmp = Ext_eval(p,x) + In(q.b,S) * eval(b,x) by FINSEQ_5:def 4;
hence thesis by A16,A19,A21,FINSEQ_1:14;
end;
theorem Th11:
for R,S being non degenerated comRing
for n being Ordinal
for p being Polynomial of n,R
for b being bag of n st Support p = {b}
for x being Function of n,S holds Ext_eval(p,x) = In(p.b,S) * eval(b,x)
proof
let R,S be non degenerated comRing;
let n be Ordinal, p be Polynomial of n,R;
let b be bag of n;
assume A0: Support p = {b};
let x be Function of n,S;
reconsider sp = Support p as finite Subset of Bags n;
set sg = SgmX(BagOrder n, sp);
A3: BagOrder n linearly_orders sp by POLYNOM2:18;
A4: rng sg = {b} by A0,A3,PRE_POLY:def 2;
then
A5: b in rng sg by TARSKI:def 1;
then
A6: 1 in dom sg by FINSEQ_3:31;
then
A7: sg/.1 = sg.1 by PARTFUN1:def 6;
A8: for u being object holds u in dom sg implies u in {1}
proof
let u be object;
assume
A9: u in dom sg;
assume
A10: not u in {1};
reconsider u as Element of NAT by A9;
sg/.u = sg.u by A9,PARTFUN1:def 6;
then
A11: sg/.u in rng sg by A9,FUNCT_1:def 3;
A12: u <> 1 by A10,TARSKI:def 1;
A13: 1 < u
proof
consider k being Nat such that
A14: dom sg = Seg k by FINSEQ_1:def 2;
ex m9 being Nat st m9 = u & 1 <= m9 & m9 <= k by A9,A14;
hence thesis by A12,XXREAL_0:1;
end;
sg/.1 = sg.1 by A5,A9,FINSEQ_3:31,PARTFUN1:def 6;
then sg/.1 in rng sg by A6,FUNCT_1:def 3;
then sg/.1 = b by A4,TARSKI:def 1
.= sg/.u by A4,A11,TARSKI:def 1;
hence thesis by A3,A6,A9,A13,PRE_POLY:def 2;
end;
Z:for u being object holds u in {1} implies u in dom sg by A6,TARSKI:def 1;
then
A15: dom sg = Seg 1 by A8,FINSEQ_1:2,TARSKI:2;
A16: len sg = 1 by Z,A8,FINSEQ_1:2,TARSKI:2,FINSEQ_1:def 3;
A17: sg.1 in rng sg by A6,FUNCT_1:def 3;
A18: (p * sg).1 = p.(sg.1) by A6,FUNCT_1:13
.= p.b by A4,A17,TARSKI:def 1;
1 in dom sg by A15;
then
A19: sg/.1 in rng sg by A7,FUNCT_1:def 3;
consider y being FinSequence of the carrier of S such that
A21: Ext_eval(p,x) = Sum y and
A20: len y = len SgmX(BagOrder n, Support p) and
A22: for i being Element of NAT st 1 <= i & i <= len y
holds y.i = In( (p * SgmX(BagOrder n, sp)).i ,S) *
eval(((SgmX(BagOrder n, sp))/.i),x)
by defeval;
y.1 = In((p * sg).1,S) * eval((sg/.1),x) by A20,A22,A16
.= In((p * sg).1,S) * eval(b,x) by A4,A19,TARSKI:def 1;
then y = <* In(p.b,S) * eval(b,x) *> by A20,A16,A18,FINSEQ_1:40;
hence thesis by A21,RLVECT_1:44;
end;
Lm5: for A,B being Ring holds
A is Subring of B implies In(0.A, B) = 0.B & In(1.A,B) = 1.B
proof
let A,B be Ring;
assume
A1: A is Subring of B; then
A2: In(0.A,B) = In(0.B,B) by C0SP1:def 3 .= 0.B;
In(1.A,B) = In(1.B,B) by A1,C0SP1:def 3 .= 1.B;
hence thesis by A2;
end;
Th12: for A,B being Ring
for x1 be Element of A st A is Subring of B holds
In(-x1,B) = - In(x1,B)
proof
let A,B be Ring;
let x1 be Element of A;
assume
A0: A is Subring of B;
In(-x1,B) + In(x1,B) = In(-x1+x1,B) by A0,ALGNUM_1:8
.= In(0.A,B) by RLVECT_1:5 .= 0.B by A0,Lm5;
hence thesis by RLVECT_1:6;
end;
Lm7: for n being Ordinal, R,S being non degenerated comRing
st R is Subring of S
for p being Polynomial of n,R
st (ex b being bag of n st Support p = {b})
for q being Polynomial of n,R, x being Function of n, S
holds Ext_eval(p+q,x) = Ext_eval(p,x) + Ext_eval(q,x)
proof
let n be Ordinal, R,S be non degenerated comRing;
assume
A0: R is Subring of S;
let p be Polynomial of n,R;
assume
ex b being bag of n st Support p = {b};
then consider b being bag of n such that
A1: Support p = {b};
b in Support p by A1,TARSKI:def 1;
then
A2: p.b <> 0.R by POLYNOM1:def 4;
let q be Polynomial of n,R, x be Function of n, S;
A3: for b1 being bag of n st b1 <> b holds (p+q).b1 = q.b1
proof
let b1 be bag of n;
A4: b1 is Element of Bags n by PRE_POLY:def 12;
assume b1 <> b;
then
A5: not b1 in Support p by A1,TARSKI:def 1;
thus (p+q).b1 = p.b1 + q.b1 by POLYNOM1:15
.= 0.R + q.b1 by A5,A4,POLYNOM1:def 4
.= q.b1;
end;
set sq = SgmX(BagOrder n, Support q), spq = SgmX(BagOrder n, Support (p+q));
A6: b is Element of Bags n by PRE_POLY:def 12;
A7: Support(p+q) c= Support p \/ Support q by POLYNOM1:20;
consider yq being FinSequence of the carrier of S such that
A9: Ext_eval(q,x) = Sum yq and
A8: len yq = len sq and
A10: for i being Element of NAT st 1 <= i & i <= len yq
holds yq.i = In((q * sq).i,S) * eval((sq/.i),x) by defeval;
consider ypq being FinSequence of the carrier of S such that
A12: Ext_eval(p+q,x) = Sum ypq and
A11: len ypq = len spq and
A13: for i being Element of NAT st 1 <= i & i <= len ypq
holds ypq.i = In(((p+q) * spq).i,S) * eval((spq/.i),x) by defeval;
A14: BagOrder n linearly_orders Support q by POLYNOM2:18;
now
per cases;
case
A15: b in Support q;
now
per cases;
case
A16: p.b = - q.b;
A17: for u being object
holds u in Support q implies u in Support(p+q) \/ {b }
proof
let u be object;
assume
A18: u in Support q;
then reconsider u as bag of n;
per cases;
suppose
u = b;
then u in {b} by TARSKI:def 1;
hence thesis by XBOOLE_0:def 3;
end;
suppose
u <> b;
then (p+q).u = q.u by A3;
then
A19: (p+q).u <> 0.R by A18,POLYNOM1:def 4;
u is Element of Bags n by PRE_POLY:def 12;
then u in Support(p+q) by A19,POLYNOM1:def 4;
hence thesis by XBOOLE_0:def 3;
end;
end;
(p+q).b = p.b + q.b by POLYNOM1:15
.= 0.R by A16,RLVECT_1:5;
then
A20: not b in Support(p+q) by POLYNOM1:def 4;
A23: for u being object
holds u in Support(p+q) \/ {b} implies u in Support q
proof
let u be object;
assume
A21: u in Support(p+q) \/ {b};
per cases by A21,XBOOLE_0:def 3;
suppose
A22: u in Support(p+q);
then not u in {b} by A20,TARSKI:def 1;
hence thesis by A1,A7,A22,XBOOLE_0:def 3;
end;
suppose
u in {b};
hence thesis by A15,TARSKI:def 1;
end;
end;
thus Ext_eval(p+q,x) = Ext_eval(p+q,x) + 0.S
.= Ext_eval(p+q,x) +
(In(q.b,S) * eval(b,x) + -(In(q.b,S) * eval(b,x))) by RLVECT_1:5
.= Ext_eval(p+q,x) +
(In(q.b,S) * eval(b,x) + (-In(q.b,S)) * eval(b,x)) by VECTSP_1:9
.= Ext_eval(p+q,x) +
(In(q.b,S) * eval(b,x) + In(-q.b,S) * eval(b,x)) by A0,Th12
.= (Ext_eval(p+q,x) + In(q.b,S) * eval(b,x)) +
In(-q.b,S) * eval(b,x) by RLVECT_1:def 3
.= Ext_eval(q,x) + In(p.b,S) * eval(b,x)
by A16,A3,A20,A23,A17,TARSKI:2,Lm6
.= Ext_eval(q,x) + Ext_eval(p,x) by A1,Th11;
end;
case
A24: p.b <> -q.b;
p.b + q.b <> (-q.b) + q.b
proof
assume
A25: p.b + q.b = (-q.b) + q.b;
p.b = p.b + 0.R
.= p.b + (q.b + -q.b) by RLVECT_1:5
.= ((-q.b) + q.b) + -q.b by A25,RLVECT_1:def 3
.= 0.R + -q.b by RLVECT_1:5
.= - q.b;
hence thesis by A24;
end;
then p.b + q.b <> 0.R by RLVECT_1:5;
then
A26: (p+q).b <> 0.R by POLYNOM1:15;
A27: for u being object holds u in Support q implies u in Support(p+q)
proof
let u be object;
assume
A28: u in Support q;
then reconsider u as bag of n;
per cases;
suppose
u = b;
hence thesis by A6,A26,POLYNOM1:def 4;
end;
suppose
u <> b;
then (p+q).u = q.u by A3;
then
A29: (p+q).u <> 0.R by A28,POLYNOM1:def 4;
u is Element of Bags n by PRE_POLY:def 12;
hence thesis by A29,POLYNOM1:def 4;
end;
end;
A30: for u being object holds u in Support(p+q) implies u in Support q
proof
let u be object;
assume
A31: u in Support(p+q);
then reconsider u as bag of n;
per cases by A7,A31,XBOOLE_0:def 3;
suppose
u in Support p;
hence thesis by A1,A15,TARSKI:def 1;
end;
suppose
u in Support q;
hence thesis;
end;
end;
then
A32: Support(p+q) = Support q by A27,TARSKI:2;
A33: len ypq = len yq by A11,A8,A30,A27,TARSKI:2;
consider spqk being Nat such that
A34: dom spq = Seg spqk by FINSEQ_1:def 2;
b in rng sq by A14,A15,PRE_POLY:def 2;
then consider k being Nat such that
A35: k in dom sq and
A36: sq.k = b by FINSEQ_2:10;
consider sqk being Nat such that
A37: dom sq = Seg sqk by FINSEQ_1:def 2;
reconsider k as Element of NAT by ORDINAL1:def 12;
reconsider k,sqk,spqk as Element of NAT by ORDINAL1:def 12;
A38: 1 <= k by A35,A37,FINSEQ_1:1;
A39: dom(p+q) = Bags n by FUNCT_2:def 1;
then sq.k in dom(p+q) by A36,PRE_POLY:def 12;
then
A40: k in dom((p+q) * sq) by A35,FUNCT_1:11;
A41: ((p+q) * sq).k = (p+q).b by A36,A40,FUNCT_1:12;
A42: k <= sqk by A35,A37,FINSEQ_1:1;
A43: dom q = Bags n by FUNCT_2:def 1;
then sq.k in dom q by A36,PRE_POLY:def 12;
then
A44: k in dom(q * sq) by A35,FUNCT_1:11;
A45: (q * sq).k = q.b by A36,A44,FUNCT_1:12;
consider i being Nat such that
A46: dom yq = Seg i by FINSEQ_1:def 2;
A47: sqk = len sq by A37,FINSEQ_1:def 3
.= len spq by A30,A27,TARSKI:2
.= spqk by A34,FINSEQ_1:def 3;
A48: i in NAT by ORDINAL1:def 12;
then
A49: len yq = i by A46,FINSEQ_1:def 3;
A50: for i9 being Element of NAT st i9 in dom yq & i9 <> k holds ypq
/.i9 = yq/.i9
proof
let i9 be Element of NAT;
assume that
A51: i9 in dom yq and
A52: i9 <> k;
A53: 1 <= i9 by A46,A51,FINSEQ_1:1;
i9 in Seg(len spq) by A11,A33,A51,FINSEQ_1:def 3;
then
A54: i9 in dom spq by FINSEQ_1:def 3;
then
spq/.i9 = spq.i9 by PARTFUN1:def 6;
then
A55: i9 in dom((p+q) * spq) by A39,A54,FUNCT_1:11;
A56: ((p+q) * spq).i9 = (p+q).(spq.i9) by A55,FUNCT_1:12;
A57: spq/.i9 <> b
proof
assume spq/.i9 = b;
then
A58: spq.i9 = b by A54,PARTFUN1:def 6;
A59: spq is one-to-one by POLYNOM2:18,PRE_POLY:10;
spq.k = b by A30,A27,A36,TARSKI:2;
hence thesis by A35,A37,A34,A47,A52,A54,A58,A59;
end;
A60: i9 in dom sq by A8,A46,A49,A51,FINSEQ_1:def 3;
sq/.i9 = sq.i9 by A37,A34,A47,A54,PARTFUN1:def 6;
then
A61: i9 in dom(q * sq) by A43,A60,FUNCT_1:11;
A62: (q * sq).i9 = q.(sq.i9) by A61,FUNCT_1:12;
A63: i9 <= len yq by A46,A49,A51,FINSEQ_1:1;
A64: i9 in dom ypq by A33,A46,A49,A51,FINSEQ_1:def 3;
A65: spq/.i9 = sq/.i9 by A30,A27,TARSKI:2;
not spq/.i9 in Support p by A1,A57,TARSKI:def 1; then
A67: p.(spq/.i9) = 0.R by POLYNOM1:def 4;
A66: ((p+q) * spq).i9 = (p+q).(spq/.i9) by A56,A54,PARTFUN1:def 6
.= 0.R + q.(sq/.i9) by A67,A32,POLYNOM1:15
.= q.(sq.i9) by A37,A34,A47,A54,PARTFUN1:def 6;
thus ypq/.i9 = ypq.i9 by A64,PARTFUN1:def 6
.= In(((p+q) * spq).i9,S) * eval((spq/.i9),x) by A13,A33,A53,A63
.= yq.i9 by A10,A53,A63,A62,A66,A65
.= yq/.i9 by A51,PARTFUN1:def 6;
end;
A64: sq/.k = b by A35,A36,PARTFUN1:def 6;
A65: sqk = len yq by A8,A37,FINSEQ_1:def 3;
then k <= i by A42,A46,A48,FINSEQ_1:def 3;
then
A66: k in dom yq by A38,A46;
then
A66a: yq/.k = yq.k by PARTFUN1:def 6;
A66b: len ypq = sqk by A11,A34,A47,FINSEQ_1:def 3;
then k in dom ypq by A35,A37,FINSEQ_1:def 3;
then ypq/.k
= ypq.k by PARTFUN1:def 6
.= In(((p+q) * spq).k,S) * eval((spq/.k),x) by A13,A38,A42,A66b
.= In((p.b + q.b),S) * eval(b,x) by A32,A64,A41,POLYNOM1:15
.= (In(p.b,S) + In(q.b,S)) * eval(b,x) by A0,ALGNUM_1:8
.= In(p.b,S) * eval(b,x) + In((q * sq).k,S) * eval((sq/.k),x)
by A64,A45,VECTSP_1:def 7
.= In(p.b,S) * eval(b,x) + yq/.k by A10,A38,A42,A65,A66a;
hence Ext_eval(p+q,x)
= In(p.b,S) * eval(b,x) + Sum yq by A12,A33,A66,A50,POLYNOM2:5
.= Ext_eval(p,x) + Ext_eval(q,x) by A1,A9,Th11;
end;
end;
hence thesis;
end;
case
A67: not b in Support q;
A68: (p+q).b = p.b + q.b by POLYNOM1:15
.= p.b + 0.R by A6,A67,POLYNOM1:def 4
.= p.b;
A69: for u being object holds u in Support p \/ Support q implies u in
Support(p+q)
proof
let u be object;
assume
A70: u in Support p \/ Support q;
per cases by A70,XBOOLE_0:def 3;
suppose
u in Support p;
then u = b by A1,TARSKI:def 1;
hence thesis by A6,A2,A68,POLYNOM1:def 4;
end;
suppose
A71: u in Support q;
then reconsider u as bag of n;
A72: q.u <> 0.R by A71,POLYNOM1:def 4;
(p+q).u = q.u by A3,A67,A71;
hence thesis by A71,A72,POLYNOM1:def 4;
end;
end;
thus Ext_eval(p+q,x)
= Ext_eval(q,x) + In((p+q).b,S) * eval(b,x)
by A3,A67,A7,A1,A69,TARSKI:2,Lm6
.= Ext_eval(q,x) + Ext_eval(p,x) by A1,A68,Th11;
end;
end;
hence thesis;
end;
theorem evalpl:
for R,S being non degenerated comRing
for n being Ordinal
for p,q being Polynomial of n,R
for x being Function of n,S
st R is Subring of S holds Ext_eval(p+q,x) = Ext_eval(p,x) + Ext_eval(q,x)
proof
let R,S be non degenerated comRing;
let n be Ordinal, p,q be Polynomial of n,R, x be Function of n,S;
assume
A0: R is Subring of S;
defpred P[Nat] means
for p being Polynomial of n,R st card(Support p) = $1
holds Ext_eval(p+q,x) = Ext_eval(p,x) + Ext_eval(q,x);
A1: ex k being Element of NAT st card(Support p) = k;
A2: for k being Nat st P[k] holds P[k + 1]
proof
let k be Nat;
assume
A3: P[k];
let p be Polynomial of n,R;
assume
A4: card(Support p) = k + 1;
set sgp = SgmX(BagOrder n, Support p);
set bg = sgp/.(len sgp);
A5: BagOrder n linearly_orders Support p by POLYNOM2:18;
then sgp <> {} by A4,PRE_POLY:def 2,RELAT_1:38;
then 1 <= len sgp by NAT_1:14;
then len sgp in Seg(len sgp);
then
A6: len sgp in dom sgp by FINSEQ_1:def 3;
then sgp/.(len sgp) = sgp.(len sgp) by PARTFUN1:def 6;
then bg in rng sgp by A6,FUNCT_1:def 3;
then
A7: bg in Support p by A5,PRE_POLY:def 2;
then
A8: p.bg <> 0.R by POLYNOM1:def 4;
set m = 0_(n,R)+*(bg,p.bg);
set p9 = p+*(bg,0.R);
reconsider bg as bag of n;
dom p = Bags n by FUNCT_2:def 1;
then
A9: p9 = p+*(bg.-->0.R) by FUNCT_7:def 3;
reconsider p9 as Function of Bags n,the carrier of R;
reconsider p9 as Function of Bags n,R;
for u being object holds u in Support p9 implies u in Support p
proof
let u be object;
assume
A10: u in Support p9;
then reconsider u as Element of Bags n;
reconsider u as bag of n;
now
assume
A11: u = bg;
then u in dom(bg.-->0.R) by TARSKI:def 1;
then p9.u = (bg.-->0.R).bg by A9,A11,FUNCT_4:13;
then p9.u = 0.R by FUNCOP_1:72;
hence contradiction by A10,POLYNOM1:def 4;
end;
then not u in dom(bg.-->0.R) by TARSKI:def 1;
then p.u = p9.u by A9,FUNCT_4:11;
then p.u <> 0.R by A10,POLYNOM1:def 4;
hence thesis by POLYNOM1:def 4;
end;
then Support p9 c= Support p;
then reconsider p9 as Polynomial of n,R by POLYNOM1:def 5;
A12: dom p = Bags n by FUNCT_2:def 1;
A13: for u being object holds u in Support p implies u in Support p9 \/ {bg}
proof
let u be object;
assume
A14: u in Support p;
then reconsider u as Element of Bags n;
A15: p.u <> 0.R by A14,POLYNOM1:def 4;
per cases;
suppose
u = bg;
then u in {bg} by TARSKI:def 1;
hence thesis by XBOOLE_0:def 3;
end;
suppose
u <> bg;
then not u in dom(bg.-->0.R) by TARSKI:def 1;
then p9.u = p.u by A9,FUNCT_4:11;
then u in Support p9 by A15,POLYNOM1:def 4;
hence thesis by XBOOLE_0:def 3;
end;
end;
bg in dom(bg.-->0.R) by TARSKI:def 1;
then p9.bg = (bg.-->0.R).bg by A9,FUNCT_4:13;
then
A16: p9.bg = 0.R by FUNCOP_1:72;
then
A17: not bg in Support p9 by POLYNOM1:def 4;
for u being object holds u in Support p9 \/ {bg} implies u in Support p
proof
let u be object;
assume
A18: u in Support p9 \/ {bg};
per cases by A18,XBOOLE_0:def 3;
suppose
A19: u in Support p9;
then reconsider u as Element of Bags n;
u <> bg by A16,A19,POLYNOM1:def 4;
then not u in dom(bg.-->0.R) by TARSKI:def 1;
then
A20: p9.u = p.u by A9,FUNCT_4:11;
p9.u <> 0.R by A19,POLYNOM1:def 4;
hence thesis by A20,POLYNOM1:def 4;
end;
suppose
u in {bg};
hence thesis by A7,TARSKI:def 1;
end;
end;
then Support p = Support p9 \/ {bg} by A13,TARSKI:2;
then
A21: k + 1 = card(Support p9) + 1 by A4,A17,CARD_2:41;
dom 0_(n,R) = Bags n by FUNCT_2:def 1;
then
A22: m = 0_(n,R)+*(bg.-->p.bg) by FUNCT_7:def 3;
reconsider m as Function of Bags n,the carrier of R;
reconsider m as Function of Bags n,R;
A23: for u being object holds u in Support m implies u in {bg}
proof
let u be object;
assume
A24: u in Support m;
then reconsider u as Element of Bags n;
A25: m.u <> 0.R by A24,POLYNOM1:def 4;
now
assume u <> bg;
then not u in dom(bg.-->p.bg) by TARSKI:def 1;
then m.u = 0_(n,R).u by A22,FUNCT_4:11;
hence contradiction by A25,POLYNOM1:22;
end;
hence thesis by TARSKI:def 1;
end;
A27: for u being object holds u in {bg} implies u in Support m
proof
let u be object;
bg in dom(bg.-->p.bg) by TARSKI:def 1;
then m.bg = (bg.-->p.bg).bg by A22,FUNCT_4:13;
then
A26: m.bg = p.bg by FUNCOP_1:72;
assume u in {bg};
then u = bg by TARSKI:def 1;
hence thesis by A8,A26,POLYNOM1:def 4;
end;
then
Support m = {bg} by A23,TARSKI:2;
then reconsider m as Polynomial of n,R by POLYNOM1:def 5;
reconsider m as Polynomial of n,R;
A28: for u being object st u in Bags n holds (p9+m).u = p.u
proof
let u be object;
assume u in Bags n;
then reconsider u as bag of n;
per cases;
suppose
A29: u = bg;
bg in dom(bg.-->p.bg) by TARSKI:def 1;
then m.bg = (bg.-->p.bg).bg by A22,FUNCT_4:13;
then
A30: m.bg = p.bg by FUNCOP_1:72;
u in dom(bg.-->0.R) by A29,TARSKI:def 1;
then
A31: p9.u = (bg.-->0.R).bg by A9,A29,FUNCT_4:13;
(p9+m).u = p9.u + m.u by POLYNOM1:15
.= 0.R + p.bg by A29,A31,A30,FUNCOP_1:72
.= p.bg;
hence thesis by A29;
end;
suppose
A32: u <> bg;
then
A33: not u in dom(bg.-->0.R) by TARSKI:def 1;
not u in dom(bg.-->p.bg) by A32,TARSKI:def 1;
then m.u = 0_(n,R).u by A22,FUNCT_4:11;
then
A34: m.u = 0.R by POLYNOM1:22;
(p9+m).u = p9.u + m.u by POLYNOM1:15
.= p.u by A9,A33,A34,FUNCT_4:11;
hence thesis;
end;
end;
A35: dom(p9 + m) = Bags n by FUNCT_2:def 1;
then Ext_eval(p,x) = Ext_eval(m+p9,x) by A12,A28,FUNCT_1:2
.= Ext_eval(p9,x) + Ext_eval(m,x) by A0,A23,A27,TARSKI:2,Lm7;
hence Ext_eval(p,x) + Ext_eval(q,x)
= (Ext_eval(p9,x) + Ext_eval(q,x)) + Ext_eval(m,x) by RLVECT_1:def 3
.= Ext_eval(p9+q,x) + Ext_eval(m,x) by A3,A21
.= Ext_eval(m+(p9+q),x) by A0,A27,A23,TARSKI:2,Lm7
.= Ext_eval((p9+m)+q,x) by POLYNOM1:21
.= Ext_eval(p+q,x) by A35,A12,A28,FUNCT_1:2;
end;
A36: P[0]
proof
let p be Polynomial of n,R;
assume card(Support p) = 0;
then Support p = {};
then
A37: p = 0_(n,R) by YY;
hence Ext_eval(p+q,x) = 0.S + Ext_eval(q,x) by POLYNOM1:23
.= Ext_eval(p,x) + Ext_eval(q,x) by A37,ev0;
end;
for k being Nat holds P[k] from NAT_1:sch 2(A36,A2);
hence thesis by A1;
end;
Lm3: for X being set, S being Subset of X, R being Order of X st R is
being_linear-order holds R linearly_orders S
proof
let X be set, S be Subset of X, R be Order of X;
A1: field R = X by ORDERS_1:12;
A3: for x,y,z being object holds x in S & y in S & z in S & [x,y] in R & [y,z]
in R implies [x,z] in R by A1,RELAT_2:def 8,RELAT_2:def 16;
A4: for x,y being object holds x in S & y in S & [x,y] in R & [y,x] in R
implies x = y by A1,RELAT_2:def 4,RELAT_2:def 12;
assume R is being_linear-order; then
A2: for x,y being object holds x in S & y in S & x <> y implies
[x,y] in R or [y,x] in R by A1,RELAT_2:def 14,def 6;
for x being object holds x in S implies [x,x] in R
by A1,RELAT_2:def 1,RELAT_2:def 9;
hence thesis by A4,A3,A2,RELAT_2:def 6,def 1,def 4,def 8;
end;
Lm8: for R,S being non degenerated comRing st R is Subring of S
for n being Ordinal, p,q being Polynomial of n,R, b1,b2 being bag of n
st Support p = {b1} & Support q = {b2} for x being Function of n,S
holds Ext_eval(p*'q,x) = Ext_eval(p,x) * Ext_eval(q,x)
proof
let R,S1 be non degenerated comRing;
assume
A0: R is Subring of S1;
let n be Ordinal;
let p,q be Polynomial of n,R, b1,b2 be bag of n;
assume that
A1: Support p = {b1} and
A2: Support q = {b2};
consider s being FinSequence of the carrier of R such that
A3: (p*'q).(b1+b2) = Sum s and
A4: len s = len decomp(b1+b2) and
A5: for k being Element of NAT st k in dom s ex u1,u2 being bag of n st
(decomp(b1+b2))/.k = <*u1,u2*> & s/.k = p.u1 * q.u2 by POLYNOM1:def 10;
A6: b1+b2 is Element of Bags n by PRE_POLY:def 12;
let x be Function of n,S1;
A7: In(p.b1 * q.b2,S1) * (eval(b1,x) * eval(b2,x))
= (In(p.b1 * q.b2,S1) * eval(b1,x)) * eval(b2,x)
by GROUP_1:def 3
.= ((In(p.b1,S1) * In(q.b2,S1)) * eval(b1,x)) * eval(b2,x)
by A0,ALGNUM_1:9
.= (In(q.b2,S1) * (In(p.b1,S1)) * eval(b1,x)) * eval(b2,x)
by GROUP_1:def 12
.= (In(q.b2,S1) * (In(p.b1,S1) * eval(b1,x))) * eval(b2,x)
by GROUP_1:def 3
.= ((In(p.b1,S1) * eval(b1,x)) * In(q.b2,S1)) * eval(b2,x)
by GROUP_1:def 12
.= (In(p.b1,S1) * eval(b1,x)) * (In(q.b2,S1) * eval(b2,x))
by GROUP_1:def 3
.= Ext_eval(p,x) * (In(q.b2,S1) * eval(b2,x)) by A1,Th11
.= Ext_eval(p,x) * Ext_eval(q,x) by A2,Th11;
A8: for b being bag of n st b <> b2 holds q.b = 0.R
proof
let b be bag of n;
assume b <> b2;
then
A9: not b in Support q by A2,TARSKI:def 1;
b is Element of Bags n by PRE_POLY:def 12;
hence thesis by A9,POLYNOM1:def 4;
end;
A10: for b being bag of n st b <> b1 holds p.b = 0.R
proof
let b be bag of n;
assume b <> b1;
then
A11: not b in Support p by A1,TARSKI:def 1;
b is Element of Bags n by PRE_POLY:def 12;
hence thesis by A11,POLYNOM1:def 4;
end;
A12: for u being object holds u in Support(p*'q) implies u in {b1+b2}
proof
let u be object;
assume
A13: u in Support(p*'q);
assume
A14: not u in {b1+b2};
reconsider u as bag of n by A13;
consider t being FinSequence of the carrier of R such that
A15: (p*'q).u = Sum t and
A16: len t = len decomp u and
A17: for k being Element of NAT st k in dom t ex b19,b29 being bag of
n st (decomp u)/.k = <*b19,b29*> & t/.k = p.b19 * q.b29 by POLYNOM1:def 10;
A18: 1 <= len t by A16,NAT_1:14;
A19: dom t = Seg len t by FINSEQ_1:def 3
.= dom decomp u by A16,FINSEQ_1:def 3;
A20: for i being Element of NAT st i in dom t holds t/.i = 0.R
proof
let i be Element of NAT;
consider S being non empty finite Subset of Bags n such that
A21: divisors u = SgmX(BagOrder n, S) and
A22: for b being bag of n holds b in S iff b divides u by PRE_POLY:def 16;
BagOrder n linearly_orders S by Lm3;
then
A23: S = rng(divisors u) by A21,PRE_POLY:def 2;
assume
A24: i in dom t;
then consider b19,b29 being bag of n such that
A25: (decomp u)/.i = <*b19,b29*> and
A26: t/.i = p.b19 * q.b29 by A17;
A27: b19 = (divisors u)/.i by A19,A24,A25,PRE_POLY:70;
A28: i in dom(divisors u) by A19,A24,PRE_POLY:def 17;
then b19 = (divisors u).i by A27,PARTFUN1:def 6;
then
A29: b19 in rng(divisors u) by A28,FUNCT_1:def 3;
per cases;
suppose
A30: b19 = b1 & b29 = b2;
b2 = <*b1,b2*>.2
.= <*b1,u-'b1*>.2 by A19,A24,A25,A27,A30,PRE_POLY:def 17
.= u-'b1;
then b1 + b2 = u by A29,A22,A23,A30,PRE_POLY:47;
hence thesis by A14,TARSKI:def 1;
end;
suppose
b19 <> b1;
then p.b19 = 0.R by A10;
hence thesis by A26;
end;
suppose
b29 <> b2;
then q.b29 = 0.R by A8;
hence thesis by A26;
end;
end;
then for i being Element of NAT st i in dom t & i <> 1 holds t/.i = 0.R;
then Sum t = t/.1 by A18,FINSEQ_3:25,POLYNOM2:3
.= 0.R by A18,FINSEQ_3:25,A20;
hence thesis by A13,A15,POLYNOM1:def 4;
end;
consider k being Element of NAT such that
A31: k in dom decomp(b1+b2) and
A32: (decomp(b1+b2))/.k = <*b1,b2*> by PRE_POLY:69;
A33: dom s = Seg(len s) by FINSEQ_1:def 3
.= dom decomp(b1+b2) by A4,FINSEQ_1:def 3;
then consider b19,b29 being bag of n such that
A34: (decomp(b1+b2))/.k = <*b19,b29*> and
A35: s/.k = p.b19 * q.b29 by A5,A31;
A36: b2 = <*b1,b2*>.2
.= b29 by A32,A34,FINSEQ_1:44;
A37: for k9 being Element of NAT st k9 in dom s & k9 <> k holds s/.k9 = 0.R
proof
let k9 be Element of NAT;
assume that
A38: k9 in dom s and
A39: k9 <> k;
consider b19,b29 being bag of n such that
A40: (decomp(b1+b2))/.k9 = <*b19,b29*> and
A41: s/.k9 = p.b19 * q.b29 by A5,A38;
per cases;
suppose
A42: b19 = b1 & b29 = b2;
(decomp(b1+b2)).k9 = (decomp(b1+b2))/.k9 by A33,A38,PARTFUN1:def 6
.= (decomp(b1+b2)).k by A31,A32,A40,A42,PARTFUN1:def 6;
hence thesis by A33,A31,A38,A39,FUNCT_1:def 4;
end;
suppose
b19 <> b1;
then p.b19 = 0.R by A10;
hence thesis by A41;
end;
suppose
b29 <> b2;
then q.b29 = 0.R by A8;
hence thesis by A41;
end;
end;
b1 = <*b19,b29*>.1 by A32,A34
.= b19;
then
A43: (p*'q).(b1+b2) = p.b1 * q.b2 by A3,A33,A31,A35,A36,A37,POLYNOM2:3;
per cases;
suppose
A44: p.b1 * q.b2 = 0.R;
then
A45: not b1+b2 in Support(p*'q) by A43,POLYNOM1:def 4;
A48: In(p.b1 * q.b2,S1) = 0.S1 by A0,A44,Lm5;
Support(p*'q) = {}
proof
set u = the Element of Support(p*'q);
assume
A46: Support(p*'q) <> {};
then
A47: u in Support(p*'q);
u in {b1+b2} by A12,A46;
hence thesis by A45,A47,TARSKI:def 1;
end;
then p*'q = 0_(n,R) by POLYNOM2:17;
hence Ext_eval(p*'q,x) = Ext_eval(p,x) * Ext_eval(q,x) by A7,A48,ev0;
end;
suppose
p.b1 * q.b2 <> 0.R;
then b1+b2 in Support(p*'q) by A43,A6,POLYNOM1:def 4;
then for u being object holds u in {b1+b2} implies u in Support(p*'q)
by TARSKI:def 1;
hence Ext_eval(p*'q,x) = In((p*'q).(b1+b2),S1) * eval(b1+b2,x)
by A12,TARSKI:2,Th11
.= Ext_eval(p,x) * Ext_eval(q,x) by A43,A7,POLYNOM2:16;
end;
end;
Lm9: for R,S being non degenerated comRing st R is Subring of S
for n being Ordinal, q being Polynomial of n,R st ex b being
bag of n st Support q = {b} for p being Polynomial of n,R, x being Function of
n, S holds Ext_eval(p*'q,x) = Ext_eval(p,x) * Ext_eval(q,x)
proof
let R,S be non degenerated comRing;
assume
A0: R is Subring of S;
let n be Ordinal, q be Polynomial of n,R;
given b being bag of n such that
A1: Support q = {b};
let p be Polynomial of n,R;
let x be Function of n,S;
defpred P[Nat] means for p being Polynomial of n,R st
card(Support p) = $1 holds Ext_eval(p*'q,x) = Ext_eval(p,x) * Ext_eval(q,x);
A2: for k being Nat st P[k] holds P[k + 1]
proof
let k be Nat;
assume
A3: P[k];
let p be Polynomial of n,R;
assume
A4: card(Support p) = k + 1;
set sgp = SgmX(BagOrder n, Support p);
set bg = sgp/.(len sgp);
A5: BagOrder n linearly_orders Support p by POLYNOM2:18;
then sgp <> {} by A4,PRE_POLY:def 2,RELAT_1:38;
then 1 <= len sgp by NAT_1:14;
then len sgp in Seg(len sgp);
then
A6: len sgp in dom sgp by FINSEQ_1:def 3;
then sgp/.(len sgp) = sgp.(len sgp) by PARTFUN1:def 6;
then bg in rng sgp by A6,FUNCT_1:def 3;
then
A7: bg in Support p by A5,PRE_POLY:def 2;
then
A8: p.bg <> 0.R by POLYNOM1:def 4;
set m = 0_(n,R)+*(bg,p.bg);
set p9 = p+*(bg,0.R);
reconsider bg as bag of n;
dom p = Bags n by FUNCT_2:def 1;
then
A9: p9 = p+*(bg.-->0.R) by FUNCT_7:def 3;
reconsider p9 as Function of Bags n,the carrier of R;
reconsider p9 as Function of Bags n,R;
for u being object holds u in Support p9 implies u in Support p
proof
let u be object;
assume
A10: u in Support p9;
then reconsider u as Element of Bags n;
reconsider u as bag of n;
now
assume
A11: u = bg;
then u in dom(bg.-->0.R) by TARSKI:def 1;
then p9.u = (bg.-->0.R).bg by A9,A11,FUNCT_4:13;
then p9.u = 0.R by FUNCOP_1:72;
hence contradiction by A10,POLYNOM1:def 4;
end;
then not u in dom(bg.-->0.R) by TARSKI:def 1;
then p.u = p9.u by A9,FUNCT_4:11;
then p.u <> 0.R by A10,POLYNOM1:def 4;
hence thesis by POLYNOM1:def 4;
end;
then Support p9 c= Support p;
then reconsider p9 as Polynomial of n,R by POLYNOM1:def 5;
A12: dom p = Bags n by FUNCT_2:def 1;
A13: for u being object holds u in Support p implies u in Support p9 \/ {bg}
proof
let u be object;
assume
A14: u in Support p;
then reconsider u as Element of Bags n;
A15: p.u <> 0.R by A14,POLYNOM1:def 4;
per cases;
suppose
u = bg;
then u in {bg} by TARSKI:def 1;
hence thesis by XBOOLE_0:def 3;
end;
suppose
u <> bg;
then not u in dom(bg.-->0.R) by TARSKI:def 1;
then p9.u = p.u by A9,FUNCT_4:11;
then u in Support p9 by A15,POLYNOM1:def 4;
hence thesis by XBOOLE_0:def 3;
end;
end;
bg in dom(bg.-->0.R) by TARSKI:def 1;
then p9.bg = (bg.-->0.R).bg by A9,FUNCT_4:13;
then
A16: p9.bg = 0.R by FUNCOP_1:72;
then
A17: not bg in Support p9 by POLYNOM1:def 4;
for u being object holds u in Support p9 \/ {bg} implies u in Support p
proof
let u be object;
assume
A18: u in Support p9 \/ {bg};
per cases by A18,XBOOLE_0:def 3;
suppose
A19: u in Support p9;
then reconsider u as Element of Bags n;
u <> bg by A16,A19,POLYNOM1:def 4;
then not u in dom(bg.-->0.R) by TARSKI:def 1;
then
A20: p9.u = p.u by A9,FUNCT_4:11;
p9.u <> 0.R by A19,POLYNOM1:def 4;
hence thesis by A20,POLYNOM1:def 4;
end;
suppose
u in {bg};
hence thesis by A7,TARSKI:def 1;
end;
end;
then Support p = Support p9 \/ {bg} by A13,TARSKI:2;
then
A21: k + 1 = card(Support p9) + 1 by A4,A17,CARD_2:41;
dom 0_(n,R) = Bags n by FUNCT_2:def 1;
then
A22: m = 0_(n,R)+*(bg.-->p.bg) by FUNCT_7:def 3;
reconsider m as Function of Bags n,the carrier of R;
reconsider m as Function of Bags n,R;
A23: for u being object holds u in Support m implies u in {bg}
proof
let u be object;
assume
A24: u in Support m;
then reconsider u as Element of Bags n;
A25: m.u <> 0.R by A24,POLYNOM1:def 4;
now
assume u <> bg;
then not u in dom(bg.-->p.bg) by TARSKI:def 1;
then m.u = 0_(n,R).u by A22,FUNCT_4:11;
hence contradiction by A25,POLYNOM1:22;
end;
hence thesis by TARSKI:def 1;
end;
A27: for u being object holds u in {bg} implies u in Support m
proof
let u be object;
bg in dom(bg.-->p.bg) by TARSKI:def 1;
then m.bg = (bg.-->p.bg).bg by A22,FUNCT_4:13;
then
A26: m.bg = p.bg by FUNCOP_1:72;
assume u in {bg};
then u = bg by TARSKI:def 1;
hence thesis by A8,A26,POLYNOM1:def 4;
end;
then
A40: Support m = {bg} by A23,TARSKI:2;
then reconsider m as Polynomial of n,R by POLYNOM1:def 5;
reconsider m as Polynomial of n,R;
A28: for u being object st u in Bags n holds (p9+m).u = p.u
proof
let u be object;
assume u in Bags n;
then reconsider u as bag of n;
per cases;
suppose
A29: u = bg;
bg in dom(bg.-->p.bg) by TARSKI:def 1;
then m.bg = (bg.-->p.bg).bg by A22,FUNCT_4:13;
then
A30: m.bg = p.bg by FUNCOP_1:72;
u in dom(bg.-->0.R) by A29,TARSKI:def 1;
then
A31: p9.u = (bg.-->0.R).bg by A9,A29,FUNCT_4:13;
(p9+m).u = p9.u + m.u by POLYNOM1:15
.= 0.R + p.bg by A29,A31,A30,FUNCOP_1:72
.= p.bg;
hence thesis by A29;
end;
suppose
A32: u <> bg;
then
A33: not u in dom(bg.-->0.R) by TARSKI:def 1;
not u in dom(bg.-->p.bg) by A32,TARSKI:def 1;
then m.u = 0_(n,R).u by A22,FUNCT_4:11;
then
A34: m.u = 0.R by POLYNOM1:22;
(p9+m).u = p9.u + m.u by POLYNOM1:15
.= p.u by A9,A33,A34,FUNCT_4:11;
hence thesis;
end;
end;
A35: dom(p9 + m) = Bags n by FUNCT_2:def 1;
then Ext_eval(p,x) = Ext_eval(m+p9,x) by A12,A28,FUNCT_1:2
.= Ext_eval(p9,x) + Ext_eval(m,x) by A27,A23,TARSKI:2,A0,Lm7;
hence
Ext_eval(p,x) * Ext_eval(q,x)
= Ext_eval(p9,x)*Ext_eval(q,x) + Ext_eval(m,x)*Ext_eval(q,x)
by VECTSP_1:def 7
.= Ext_eval(p9*'q,x) + Ext_eval(m,x)*Ext_eval(q,x) by A3,A21
.= Ext_eval(p9*'q,x)+Ext_eval(m*'q,x) by A0,A1,A40,Lm8
.= Ext_eval(p9*'q+m*'q,x) by A0,evalpl
.= Ext_eval(q*'(p9+m),x) by POLYNOM1:26
.= Ext_eval(p*'q,x) by A35,A12,A28,FUNCT_1:2;
end;
A36: ex k being Element of NAT st card(Support p) = k;
A37: P[0]
proof
let p be Polynomial of n,R;
assume card(Support p) = 0;
then Support p ={};
then
A38: p = 0_(n,R) by POLYNOM2:17;
hence Ext_eval(p*'q,x) = Ext_eval(p,x) by POLYNOM1:28
.= 0.S * Ext_eval(q,x) by A38,ev0
.= Ext_eval(p,x) * Ext_eval(q,x) by A38,ev0;
end;
for k being Nat holds P[k] from NAT_1:sch 2(A37,A2);
hence thesis by A36;
end;
theorem evalti:
for R,S being non degenerated comRing
for n being Ordinal
for p,q being Polynomial of n,R
for x being Function of n,S
st R is Subring of S holds Ext_eval(p*'q,x) = Ext_eval(p,x) * Ext_eval(q,x)
proof
let R,S be non degenerated comRing;
let n be Ordinal, p,q be Polynomial of n,R, x be Function of n,S;
assume
A0: R is Subring of S;
defpred P[Nat] means for p being Polynomial of n,R st
card(Support p) = $1 holds Ext_eval(p*'q,x) = Ext_eval(p,x) * Ext_eval(q,x);
A1: ex k being Element of NAT st card(Support p) = k;
A2: for k being Nat st P[k] holds P[k + 1]
proof
let k be Nat;
assume
A3: P[k];
let p be Polynomial of n,R;
assume
A4: card(Support p) = k + 1;
set sgp = SgmX(BagOrder n, Support p);
set bg = sgp/.(len sgp);
A5: BagOrder n linearly_orders Support p by POLYNOM2:18;
then sgp <> {} by A4,PRE_POLY:def 2,RELAT_1:38;
then 1 <= len sgp by NAT_1:14;
then len sgp in Seg(len sgp);
then
A6: len sgp in dom sgp by FINSEQ_1:def 3;
then sgp/.(len sgp) = sgp.(len sgp) by PARTFUN1:def 6;
then bg in rng sgp by A6,FUNCT_1:def 3;
then
A7: bg in Support p by A5,PRE_POLY:def 2;
then
A8: p.bg <> 0.R by POLYNOM1:def 4;
set m = 0_(n,R)+*(bg,p.bg);
set p9 = p+*(bg,0.R);
reconsider bg as bag of n;
dom p = Bags n by FUNCT_2:def 1;
then
A9: p9 = p+*(bg.-->0.R) by FUNCT_7:def 3;
reconsider p9 as Function of Bags n,R;
for u being object holds u in Support p9 implies u in Support p
proof
let u be object;
assume
A10: u in Support p9;
then reconsider u as Element of Bags n;
reconsider u as bag of n;
now
assume
A11: u = bg;
then u in dom(bg.-->0.R) by TARSKI:def 1;
then p9.u = (bg.-->0.R).bg by A9,A11,FUNCT_4:13;
then p9.u = 0.R by FUNCOP_1:72;
hence contradiction by A10,POLYNOM1:def 4;
end;
then not u in dom(bg.-->0.R) by TARSKI:def 1;
then p.u = p9.u by A9,FUNCT_4:11;
then p.u <> 0.R by A10,POLYNOM1:def 4;
hence thesis by POLYNOM1:def 4;
end;
then Support p9 c= Support p;
then reconsider p9 as Polynomial of n,R by POLYNOM1:def 5;
A12: dom p = Bags n by FUNCT_2:def 1;
A13: for u being object holds u in Support p implies u in Support p9 \/ {bg}
proof
let u be object;
assume
A14: u in Support p;
then reconsider u as Element of Bags n;
A15: p.u <> 0.R by A14,POLYNOM1:def 4;
per cases;
suppose
u = bg;
then u in {bg} by TARSKI:def 1;
hence thesis by XBOOLE_0:def 3;
end;
suppose
u <> bg;
then not u in dom(bg.-->0.R) by TARSKI:def 1;
then p9.u = p.u by A9,FUNCT_4:11;
then u in Support p9 by A15,POLYNOM1:def 4;
hence thesis by XBOOLE_0:def 3;
end;
end;
bg in dom(bg.-->0.R) by TARSKI:def 1;
then p9.bg = (bg.-->0.R).bg by A9,FUNCT_4:13;
then
A16: p9.bg = 0.R by FUNCOP_1:72;
then
A17: not bg in Support p9 by POLYNOM1:def 4;
for u being object holds u in Support p9 \/ {bg} implies u in Support p
proof
let u be object;
assume
A18: u in Support p9 \/ {bg};
per cases by A18,XBOOLE_0:def 3;
suppose
A19: u in Support p9;
then reconsider u as Element of Bags n;
u <> bg by A16,A19,POLYNOM1:def 4;
then not u in dom(bg.-->0.R) by TARSKI:def 1;
then
A20: p9.u = p.u by A9,FUNCT_4:11;
p9.u <> 0.R by A19,POLYNOM1:def 4;
hence thesis by A20,POLYNOM1:def 4;
end;
suppose
u in {bg};
hence thesis by A7,TARSKI:def 1;
end;
end;
then Support p = Support p9 \/ {bg} by A13,TARSKI:2;
then
A21: k + 1 = card(Support p9) + 1 by A4,A17,CARD_2:41;
dom 0_(n,R) = Bags n by FUNCT_2:def 1;
then
A22: m = 0_(n,R)+*(bg.-->p.bg) by FUNCT_7:def 3;
reconsider m as Function of Bags n,the carrier of R;
reconsider m as Function of Bags n,R;
A23: for u being object holds u in Support m implies u in {bg}
proof
let u be object;
assume
A24: u in Support m;
then reconsider u as Element of Bags n;
A25: m.u <> 0.R by A24,POLYNOM1:def 4;
now
assume u <> bg;
then not u in dom(bg.-->p.bg) by TARSKI:def 1;
then m.u = 0_(n,R).u by A22,FUNCT_4:11;
hence contradiction by A25,POLYNOM1:22;
end;
hence thesis by TARSKI:def 1;
end;
A27: for u being object holds u in {bg} implies u in Support m
proof
let u be object;
bg in dom(bg.-->p.bg) by TARSKI:def 1;
then m.bg = (bg.-->p.bg).bg by A22,FUNCT_4:13;
then
A26: m.bg = p.bg by FUNCOP_1:72;
assume u in {bg};
then u = bg by TARSKI:def 1;
hence thesis by A8,A26,POLYNOM1:def 4;
end;
then
Support m = {bg} by A23,TARSKI:2;
then reconsider m as Polynomial of n,R by POLYNOM1:def 5;
reconsider m as Polynomial of n,R;
A28: for u being object st u in Bags n holds (p9+m).u = p.u
proof
let u be object;
assume u in Bags n;
then reconsider u as bag of n;
per cases;
suppose
A29: u = bg;
bg in dom(bg.-->p.bg) by TARSKI:def 1;
then m.bg = (bg.-->p.bg).bg by A22,FUNCT_4:13;
then
A30: m.bg = p.bg by FUNCOP_1:72;
u in dom(bg.-->0.R) by A29,TARSKI:def 1;
then
A31: p9.u = (bg.-->0.R).bg by A9,A29,FUNCT_4:13;
(p9+m).u = p9.u + m.u by POLYNOM1:15
.= 0.R + p.bg by A29,A31,A30,FUNCOP_1:72
.= p.bg;
hence thesis by A29;
end;
suppose
A32: u <> bg;
then
A33: not u in dom(bg.-->0.R) by TARSKI:def 1;
not u in dom(bg.-->p.bg) by A32,TARSKI:def 1;
then m.u = 0_(n,R).u by A22,FUNCT_4:11;
then
A34: m.u = 0.R by POLYNOM1:22;
(p9+m).u = p9.u + m.u by POLYNOM1:15
.= p.u by A9,A33,A34,FUNCT_4:11;
hence thesis;
end;
end;
A35: dom(p9 + m) = Bags n by FUNCT_2:def 1;
then Ext_eval(p,x) = Ext_eval(m+p9,x) by A12,A28,FUNCT_1:2
.= Ext_eval(p9,x) + Ext_eval(m,x) by A27,A23,TARSKI:2,A0,Lm7;
hence
Ext_eval(p,x) * Ext_eval(q,x)
= Ext_eval(p9,x)*Ext_eval(q,x) + Ext_eval(m,x)*Ext_eval(q,x)
by VECTSP_1:def 7
.= Ext_eval(p9*'q,x) + Ext_eval(m,x)*Ext_eval(q,x) by A3,A21
.= Ext_eval(p9*'q,x) + Ext_eval(q,x)*Ext_eval(m,x) by GROUP_1:def 12
.= Ext_eval(p9*'q,x) + Ext_eval(m*'q,x) by A27,A23,TARSKI:2,A0,Lm9
.= Ext_eval(p9*'q+m*'q,x) by A0,evalpl
.= Ext_eval(q*'(p9+m),x) by POLYNOM1:26
.= Ext_eval(p*'q,x) by A35,A12,A28,FUNCT_1:2;
end;
A36: P[0]
proof
let p be Polynomial of n,R;
assume card(Support p) = 0;
then Support p = {};
then
A37: p = 0_(n,R) by POLYNOM2:17;
hence Ext_eval(p*'q,x) = Ext_eval(p,x) by POLYNOM1:28
.= 0.S * Ext_eval(q,x) by A37,ev0
.= Ext_eval(p,x) * Ext_eval(q,x) by A37,ev0;
end;
for k being Nat holds P[k] from NAT_1:sch 2(A36,A2);
hence thesis by A1;
end;
ideal2:
for R being non degenerated comRing
for S being comRingExtension of R
for n being Ordinal
for P being non empty Subset of Polynom-Ring(n,R)
for F being LeftLinearCombination of P
for p being Polynomial of n,R st p = Sum F
for x being Function of n,S
ex G being FinSequence of S st len G = len F &
Ext_eval(p,x) = Sum G &
for i being set st i in dom G
for q being Polynomial of n,R st q = F.i holds G.i = Ext_eval(q,x)
proof
let R be non degenerated comRing, S be comRingExtension of R, n be Ordinal;
let P be non empty Subset of Polynom-Ring(n,R);
let F be LeftLinearCombination of P, p be Polynomial of n,R;
assume AS: p = Sum F;
let x be Function of n,S;
defpred P[Nat] means
for P being non empty Subset of Polynom-Ring(n,R)
for F being LeftLinearCombination of P st len F = $1
for p being Polynomial of n,R st p = Sum F
for x being Function of n,S
ex G being FinSequence of S st len G = len F &
Ext_eval(p,x) = Sum G &
for i being set st i in dom G
for q being Polynomial of n,R st q = F.i holds G.i = Ext_eval(q,x);
H: R is Subring of S by FIELD_4:def 1;
IA: P[0]
proof
now let P be non empty Subset of Polynom-Ring(n,R);
let F be LeftLinearCombination of P;
assume A1: len F = 0;
let p be Polynomial of n,R;
assume A2: p = Sum F;
let x be Function of n,S;
thus ex G being FinSequence of S st len G = len F &
Ext_eval(p,x) = Sum G &
for i being set st i in dom G
for q being Polynomial of n,R st q = F.i holds G.i = Ext_eval(q,x)
proof
take G = <*>(the carrier of S);
thus len G = len F by A1;
F = <*>(the carrier of Polynom-Ring(n,R)) by A1; then
Sum F = 0.(Polynom-Ring(n,R)) by RLVECT_1:43;
then p = 0_(n,R) by A2,POLYNOM1:def 11;
hence Ext_eval(p,x) = 0.S by ev0 .= Sum G by RLVECT_1:43;
thus for i being set st i in dom G
for q being Polynomial of n,R st q = F.i holds G.i = Ext_eval(q,x);
end;
end;
hence thesis;
end;
IS: now let k be Nat;
assume IV: P[k];
now let P be non empty Subset of Polynom-Ring(n,R);
let F be LeftLinearCombination of P;
assume I1: len F = k+1;
let p be Polynomial of n,R;
assume I2: p = Sum F;
let x be Function of n,S;
set PR = Polynom-Ring(n,R), PS = Polynom-Ring(n,S);
F <> {} by I1; then
consider K being LeftLinearCombination of P,
a being Element of PR such that
I3: F = K^<* a *> & <*a*> is LeftLinearCombination of P by IDEAL_1:33;
I4: len F = len K + len <*a*> by I3,FINSEQ_1:22
.= len K + 1 by FINSEQ_1:39;
reconsider r = Sum K as Polynomial of n,R by POLYNOM1:def 11;
consider GK being FinSequence of S such that
I5: len GK = len K &
Ext_eval(r,x) = Sum GK &
for i being set st i in dom GK
for q being Polynomial of n,R st q = K.i holds GK.i = Ext_eval(q,x)
by IV,I1,I4;
I9: Sum <*a*> = a by RLVECT_1:44;
reconsider pa = a as Polynomial of n,R by POLYNOM1:def 11;
set G = GK ^ <*Ext_eval(pa,x)*>;
len <*Ext_eval(pa,x)*> = 1 by FINSEQ_1:39; then
I6: len G = len F by I4,I5,FINSEQ_1:22;
p = Sum K + Sum <*a*> by I2,I3,RLVECT_1:41; then
I8: r + pa = p by I9,POLYNOM1:def 11;
I7: Sum G = Sum GK + Sum <*Ext_eval(pa,x)*> by RLVECT_1:41
.= Ext_eval(r,x) + Ext_eval(pa,x) by I5,RLVECT_1:44
.= Ext_eval(p,x) by I8,H,evalpl;
now let i be set;
assume J1: i in dom G;
let q being Polynomial of n,R;
assume J2: q = F.i;
per cases by J1,FINSEQ_1:25;
suppose J3: i in dom GK; then
J4: GK.i = G.i by FINSEQ_1:def 7;
dom K = Seg(len GK) by I5,FINSEQ_1:def 3
.= dom GK by FINSEQ_1:def 3; then
K.i = F.i by J3,I3,FINSEQ_1:def 7;
hence G.i = Ext_eval(q,x) by J2,J3,J4,I5;
end;
suppose ex k being Nat st
k in dom <*Ext_eval(pa,x)*> & i = len GK + k; then
consider k being Nat such that
J3: k in dom <*Ext_eval(pa,x)*> & i = len GK + k;
J6: dom <*Ext_eval(pa,x)*> = {1} by FINSEQ_1:38,FINSEQ_1:2; then
J4: k = 1 by J3,TARSKI:def 1;
k in dom <*a*> by J6,J3,FINSEQ_1:2,FINSEQ_1:38; then
J5: F.i = <*a*>.1 by J4,J3,I5,I3,FINSEQ_1:def 7
.= a;
thus G.i = <*Ext_eval(pa,x)*>.1 by J4,J3,FINSEQ_1:def 7
.= Ext_eval(q,x) by J5,J2;
end;
end;
hence ex G being FinSequence of S st len G = len F &
Ext_eval(p,x) = Sum G &
for i being set st i in dom G
for q being Polynomial of n,R st q = F.i holds G.i = Ext_eval(q,x)
by I6,I7;
end;
hence P[k+1];
end;
I: for k being Nat holds P[k] from NAT_1:sch 2(IA,IS);
thus thesis by AS,I;
end;
:: "... To each polynomial f in K[X] we associate a letter X_f and we let
:: S be the set of all such letters X_f (so that S is in bijection with the
:: set of all polynomials in K[X] of degree >= 1). We form the polynomial
:: ring K[S], ..."
:: First a bijection between the set of all polynomials in K[X] of degree >= 1
:: and S = n, where n = card {p in K[X] | deg p > = 1}, is shown to exist.
definition
let F be Field;
func nonConstantPolys F ->
non empty Subset of the carrier of Polynom-Ring F equals
the set of all p where p is
non constant Element of the carrier of Polynom-Ring F;
coherence
proof
A: now let o be object;
assume o in the set of all p where p is
non constant Element of the carrier of Polynom-Ring F;
then consider p being non constant Element of the carrier of Polynom-Ring F
such that A: o = p;
thus o in the carrier of Polynom-Ring F by A;
end;
set p = the non constant Element of the carrier of Polynom-Ring F;
p in the set of all p where p is
non constant Element of the carrier of Polynom-Ring F;
hence thesis by A,TARSKI:def 3;
end;
end;
registration
let F be Field;
cluster card(nonConstantPolys F) -> non empty;
coherence;
end;
registration
let F be Field;
cluster bijective for
Function of (nonConstantPolys F),card(nonConstantPolys F);
existence
proof
set X = nonConstantPolys F, Y = card(nonConstantPolys F);
consider f being Function such that
H: f is one-to-one & dom f = X & rng f = Y by CARD_1:def 2,WELLORD2:def 4;
reconsider f as Function of X,Y by H,FUNCT_2:2;
f is onto by H;
hence thesis by H;
end;
end;
definition
let F be Field;
let g be Function of (nonConstantPolys F),card(nonConstantPolys F);
let p be non constant Element of the carrier of Polynom-Ring F;
redefine func g.p -> Ordinal; :: redefines . (FUNCT_1, definition)
coherence
proof
p in nonConstantPolys F;
then p in dom g by FUNCT_2:def 1;
then A: g.p in rng g by FUNCT_1:3;
rng g c= card(nonConstantPolys F) by RELAT_1:def 19;
hence thesis by A;
end;
end;
:: Translation of polynomials from K[X] into K[X1,X2,...] = K[n]:
:: For p in K[X] we have Poly(m,p) = p(Xm) where m is the m-th variable of
:: n = card { p in K[X] | deg p >= 1 }
:: --- if not m in n, then Poly(m,p) is the constant polynomial given by p(0)
definition
let F be Field;
let m be Ordinal;
let p be Polynomial of F;
func Poly(m,p) -> Polynomial of card(nonConstantPolys F),F means :defPg:
it.(EmptyBag card(nonConstantPolys F)) = p.0 &
(for b being bag of card(nonConstantPolys F)
st support b = {m} holds it.b = p.(b.m)) &
(for b being bag of card(nonConstantPolys F)
st support b <> {} & support b <> {m} holds it.b = 0.F);
existence
proof
set n = card(nonConstantPolys F);
defpred P[Element of Bags n,Element of the carrier of F] means
(support($1) = {} & $2 = p.0) or
(support($1) = {m} & $2 = p.($1.m)) or
(support($1) <> {} & support($1) <> {m} & $2 = 0.F);
A: for x being Element of Bags n
ex y being Element of the carrier of F st P[x,y]
proof
let x be Element of Bags n;
per cases;
suppose support x = {};
hence thesis;
end;
suppose support x = {m};
hence thesis;
end;
suppose support x <> {} & support x <> {m};
hence thesis;
end;
end;
consider f being Function of Bags n, the carrier of F such that
B: for x being Element of Bags n holds P[x,f.x] from FUNCT_2:sch 3(A);
set M = {b where b is bag of n :
support b = {m} & b.m is Element of NAT & b.m in Support p};
C: M is finite
proof
per cases;
suppose M = {};
hence thesis;
end;
suppose M <> {};
then reconsider M1 = M as non empty set;
defpred Q[Element of M1,Element of NAT] means
ex b being bag of n st $1 = b & support b = {m} & $2 = b.m;
C0: for x being Element of M1 ex y being Element of NAT st Q[x,y]
proof
let x be Element of M1;
x in M; then
consider b being bag of n such that
C1: x = b & support b = {m} &
b.m is Element of NAT & b.m in Support p;
take b.m;
thus thesis by C1;
end;
consider f being Function of M1,NAT such that
C1: for x being Element of M1 holds Q[x,f.x] from FUNCT_2:sch 3(C0);
f is one-to-one
proof
now let x1,x2 be object;
assume C2: x1 in dom f & x2 in dom f & f.x1 = f.x2;
C3: dom f = M1 by FUNCT_2:def 1;
reconsider x1b = x1, x2b = x2 as Element of M1 by C2;
consider b1 being bag of n such that
C4: x1 = b1 & support b1 = {m} &
b1.m is Element of NAT & b1.m in Support p by C2,C3;
consider b2 being bag of n such that
C5: x2 = b2 & support b2 = {m} &
b2.m is Element of NAT & b2.m in Support p by C2,C3;
C6: Q[x1b,f.x1b] & Q[x2b,f.x2b] by C1;
C8: dom b1 = n by PARTFUN1:def 2 .= dom b2 by PARTFUN1:def 2;
now let x be object;
assume x in dom b1;
per cases;
suppose x in support b1;
then x = m by C4,TARSKI:def 1;
hence b1.x = b2.x by C4,C2,C5,C6;
end;
suppose C9: not x in support b1;
hence b2.x = 0 by C5,C4,PRE_POLY:def 7 .= b1.x by C9,PRE_POLY:def 7;
end;
end;
then b1 = b2 by C8;
hence x1 = x2 by C4,C5;
end;
hence thesis;
end;
then C2: card dom f = card rng f by CARD_1:70;
C3: Support p is finite by POLYNOM1:def 5;
rng f c= Support p
proof
now let o be object;
assume o in rng f;
then consider u being object such that
C4: u in dom f & f.u = o by FUNCT_1:def 3;
u in M1 by C4;
then consider b being bag of n such that
C5: u = b & support b = {m} &
b.m is Element of NAT & b.m in Support p;
reconsider u as Element of M1 by C4;
Q[u,f.u] by C1;
hence o in Support p by C4,C5;
end;
hence thesis;
end;
then dom f is finite by C3,C2;
hence M is finite by FUNCT_2:def 1;
end;
end;
Support f c= M \/ {n --> 0}
proof
now let x be object;
assume C0: x in Support f;
then C1: x in dom f & f.x <> 0.F by POLYNOM1:def 3;
reconsider b = x as Element of Bags n by C0;
C2: dom b = n by PARTFUN1:def 2;
per cases;
suppose support b = {};
then for z being object st z in dom b holds b.z = 0 by PRE_POLY:def 7;
then b = n --> 0 by C2,FUNCOP_1:11;
then x in {n --> 0} by TARSKI:def 1;
hence x in M \/ {n --> 0} by XBOOLE_0:def 3;
end;
suppose H: support b = {m};
reconsider i = b.m as Element of NAT;
K: dom p = NAT by FUNCT_2:def 1;
f.b = p.(b.m) by B,H;
then b.m in Support p by K,C1,POLYNOM1:def 3;
then b in M by H;
hence x in M \/ {n --> 0} by XBOOLE_0:def 3;
end;
suppose support b <> {} & support b <> {m};
hence x in M \/ {n --> 0} by B,C1;
end;
end;
hence thesis;
end;
then reconsider f as Polynomial of n,F by C,POLYNOM1:def 5;
take f;
support(EmptyBag n) = {};
hence f.(EmptyBag n) = p.0 by B;
thus for b being bag of n st support b = {m} holds f.b = p.(b.m)
proof
let b be bag of n;
assume H: support b = {m};
reconsider b1 = b as Element of Bags n by PRE_POLY:def 12;
P[b1,f.b1] by B;
hence f.b = p.(b.m) by H;
end;
thus for b being bag of n
st support b <> {} & support b <> {m} holds f.b = 0.F
proof
let b be bag of n;
assume H: support b <> {} & support b <> {m};
reconsider b1 = b as Element of Bags n by PRE_POLY:def 12;
P[b1,f.b1] by B;
hence f.b = 0.F by H;
end;
end;
uniqueness
proof
set n = card(nonConstantPolys F);
let r1,r2 be Polynomial of card(nonConstantPolys F),F such that
A3: r1.(EmptyBag n) = p.0 &
(for b being bag of n st support b = {m} holds r1.b = p.(b.m)) &
(for b being bag of n st
support b <> {} & support b <> {m} holds r1.b = 0.F) and
A4: r2.(EmptyBag n) = p.0 &
(for b being bag of n st support b = {m} holds r2.b = p.(b.m)) &
(for b being bag of n st
support b <> {} & support b <> {m} holds r2.b = 0.F);
A5: dom r1 = Bags n by FUNCT_2:def 1 .= dom r2 by FUNCT_2:def 1;
now let o be object;
assume o in dom r1;
then reconsider b = o as bag of n;
per cases;
suppose support b = {};
then for i being object st i in n holds b.i = {} by PRE_POLY:def 7;
then b = EmptyBag n by PBOOLE:6;
hence r1.o = r2.o by A4,A3;
end;
suppose H: support b = {m};
then r1.b = p.(b.m) by A3 .= r2.b by H,A4;
hence r1.o = r2.o;
end;
suppose H: support b <> {} & support b <> {m};
then r1.b = 0.F by A3 .= r2.b by H,A4;
hence r1.o = r2.o;
end;
end;
hence thesis by A5;
end;
end;
definition
let F be Field;
let g be bijective Function of (nonConstantPolys F),card(nonConstantPolys F);
func nonConstantPolys(g,F) ->
non empty Subset of Polynom-Ring(card(nonConstantPolys F),F) equals
the set of all Poly(g.p,p)
where p is non constant Element of the carrier of Polynom-Ring F;
coherence
proof
A: now let o be object;
assume o in the set of all Poly(g.p,p)
where p is non constant Element of the carrier of Polynom-Ring F;
then consider p being non constant Element of the carrier of Polynom-Ring F
such that A: o = Poly(g.p,p);
thus o in the carrier of Polynom-Ring(card(nonConstantPolys F),F)
by A,POLYNOM1:def 11;
end;
set p = the non constant Element of the carrier of Polynom-Ring F;
Poly(g.p,p) in the set of all Poly(g.p,p)
where p is non constant Element of the carrier of Polynom-Ring F;
hence thesis by A,TARSKI:def 3;
end;
end;
registration
let F be Field;
let m be Ordinal;
let p be Polynomial of F;
cluster Poly(m,LM p) -> monomial-like;
coherence
proof
set n = card(nonConstantPolys F), q = Poly(m,LM p);
per cases;
suppose m in n; then
for o being object st o in {m} holds o in n by TARSKI:def 1;
then reconsider S = {m} as finite Subset of n by TARSKI:def 3;
per cases;
suppose p is non constant; then
deg p > 0 by RATFUNC1:def 2; then
Z2: len p - 1 > 0 by HURWITZ:def 2; then
Z3: len p - 1 = len p -' 1 by XREAL_0:def 2;
set c = (S,len p -' 1)-bag;
E: {m} = support c by Z2,Z3,UPROOTS:8;
X: now let b be bag of n;
assume AS: q.b <> 0.F;
A: now assume support b = {}; then
b = EmptyBag n by PRE_POLY:81; then
q.b = (LM p).0 by defPg .= 0.F by Z2,Z3,POLYNOM4:def 1;
hence contradiction by AS;
end;
B: support b = {} or support b = {m} by AS,defPg;
then q.b = (LM p).(b.m) by A,defPg;
then C: b.m = len p -' 1 by AS,POLYNOM4:def 1;
thus b = c
proof
now let o be object;
assume o in n;
per cases;
suppose D: o in support b;
then o = m by B,TARSKI:def 1;
hence b.o = c.o by B,C,D,UPROOTS:7;
end;
suppose D: not o in support b;
hence b.o = 0 by PRE_POLY:def 7 .= c.o by A,B,D,E,PRE_POLY:def 7;
end;
end;
hence thesis by PBOOLE:3;
end;
end;
ex b being bag of n st
for b1 being bag of n st b1 <> b holds q.b1 = 0.F
proof
take c;
thus thesis by X;
end;
hence thesis by POLYNOM7:def 3;
end;
suppose Z: p is constant;
reconsider p1 = p as Element of the carrier of Polynom-Ring F
by POLYNOM3:def 10;
Z2: deg p <= 0 by Z,RATFUNC1:def 2;
Z1: len p -' 1 = 0
proof
per cases by Z2,HURWITZ:def 2;
suppose len p - 1 = 0;
hence thesis by XREAL_0:def 2;
end;
suppose len p - 1 < 0;
hence thesis by XREAL_0:def 2;
end;
end;
X: now let b be bag of n;
assume AS: q.b <> 0.F;
A: now assume B: support b = {m};
m in {m} by TARSKI:def 1; then
C: b.m <> 0 by B,PRE_POLY:def 7;
q.b = (LM p).(b.m) by B,defPg .= 0.F by C,Z1,POLYNOM4:def 1;
hence contradiction by AS;
end;
support b = {} or support b = {m} by AS,defPg;
then for i being object st i in n holds b.i = {} by A,PRE_POLY:def 7;
hence b = EmptyBag n by PBOOLE:6;
end;
ex b being bag of n st
for b1 being bag of n st b1 <> b holds q.b1 = 0.F
proof
take EmptyBag n;
thus thesis by X;
end;
hence thesis by POLYNOM7:def 3;
end;
end;
suppose Y: not m in n;
X: now let b be bag of n;
A: not m in support b by Y;
assume q.b <> 0.F; then
support b = {} or support b = {m} by defPg;
then for i being object st i in n holds b.i = {}
by A,PRE_POLY:def 7,TARSKI:def 1;
hence b = EmptyBag n by PBOOLE:6;
end;
ex b being bag of n st
for b1 being bag of n st b1 <> b holds q.b1 = 0.F
proof
take EmptyBag n;
thus thesis by X;
end;
hence thesis by POLYNOM7:def 3;
end;
end;
end;
Th14c:
for F being Field
for m being Ordinal
for p being Polynomial of F holds
Support Poly(m,p) c= {EmptyBag card(nonConstantPolys F)} \/
{b where b is bag of card(nonConstantPolys F) : support b = {m}}
proof
let F be Field;
let m be Ordinal;
let p be Polynomial of F;
set n = card(nonConstantPolys F), q = Poly(m,p);
now let o be object;
assume A: o in Support Poly(m,p); then
reconsider b = o as bag of n;
B: q.b <> 0.F by A,POLYNOM1:def 3;
per cases;
suppose support b = {};
then for i being object st i in n holds b.i = {} by PRE_POLY:def 7;
then b = EmptyBag n by PBOOLE:6;
then b in {EmptyBag n} by TARSKI:def 1;
hence o in {EmptyBag n} \/
{b where b is bag of card(nonConstantPolys F) : support b = {m}}
by XBOOLE_0:def 3;
end;
suppose support b = {m} & b.m is Element of NAT;
then b in {b where b is bag of card(nonConstantPolys F) : support b = {m}};
hence o in {EmptyBag card(nonConstantPolys F)} \/
{b where b is bag of card(nonConstantPolys F) : support b = {m}}
by XBOOLE_0:def 3;
end;
suppose support b = {m} & not b.m is Element of NAT;
hence o in {EmptyBag card(nonConstantPolys F)} \/
{b where b is bag of card(nonConstantPolys F) : support b = {m}};
end;
suppose support b <> {} & support b <> {m};
hence o in {EmptyBag card(nonConstantPolys F)} \/
{b where b is bag of card(nonConstantPolys F) : support b = {m}}
by defPg,B;
end;
end;
hence thesis;
end;
Th28:
for L be non empty ZeroStr, a be Element of L
holds (a|L).0 = a & for n be Nat st n <> 0 holds (a|L).n = 0.L
proof
let L be non empty ZeroStr, a be Element of L;
0 in dom 0_.(L);
hence (a|L).0 = a by FUNCT_7:31;
let n be Nat;
assume n <> 0;
hence (a|L).n = (0_.(L)).n by FUNCT_7:32
.= 0.L by ORDINAL1:def 12,FUNCOP_1:7;
end;
theorem pZero:
for F being Field
for m being Ordinal st m in card(nonConstantPolys F)
for p being Polynomial of F
holds Poly(m,p) = 0_(card(nonConstantPolys F),F) iff p = 0_.(F)
proof
let F be Field, m be Ordinal;
assume K: m in card(nonConstantPolys F);
let p be Polynomial of F;
set n = card(nonConstantPolys F);
H: Support Poly(m,p) c= {EmptyBag n} \/
{b where b is bag of n : support b = {m}} by Th14c;
A: now assume AS: p = 0_.(F);
now let o be object;
assume B: o in Support Poly(m,p);
per cases by H,B,XBOOLE_0:def 3;
suppose o in {EmptyBag n};
then o = EmptyBag n by TARSKI:def 1;
then Poly(m,p).o = p.0 by defPg;
hence contradiction by B,AS,POLYNOM1:def 4;
end;
suppose o in {b where b is bag of n : support b = {m}};
then consider b being bag of n such that
D: o = b & support b = {m};
Poly(m,p).b = p.(b.m) by D,defPg;
hence contradiction by D,B,AS,POLYNOM1:def 4;
end;
end;
then Support Poly(m,p) = {} by XBOOLE_0:def 1;
hence Poly(m,p) = 0_(n,F) by YY;
end;
now assume AS: Poly(m,p) = 0_(n,F);
now let i be Element of NAT;
per cases;
suppose i = 0;
hence p.i = Poly(m,p).(EmptyBag n) by defPg .= 0.F by AS,POLYNOM1:22;
end;
suppose A: i <> 0;
for o being object st o in {m} holds o in n by K,TARSKI:def 1;
then reconsider S = {m} as finite Subset of n by TARSKI:def 3;
set b = (S,i)-bag;
B: support b = S by A,UPROOTS:8;
m in {m} by TARSKI:def 1;
hence p.i = p.(b.m) by UPROOTS:7
.= Poly(m,p).b by B,defPg .= 0.F by AS,POLYNOM1:22;
end;
end;
hence p = 0_.(F);
end;
hence thesis by A;
end;
theorem XYZbb:
for F being Field
for m being Ordinal st m in card(nonConstantPolys F)
for p being Polynomial of F
for a being Element of F
holds Poly(m,p) = a|(card(nonConstantPolys F),F) iff p = a|F
proof
let F be Field, m be Ordinal;
assume K: m in card(nonConstantPolys F);
let p be Polynomial of F; let a be Element of F;
set n = card(nonConstantPolys F);
A: now assume AS: p = a|F;
set q = a|(n,F);
now let o be object;
assume o in Bags n;
then reconsider b = o as bag of n;
per cases;
suppose support b = {};
then for i being object st i in n holds b.i = {} by PRE_POLY:def 7;
then D: b = EmptyBag n by PBOOLE:6;
hence Poly(m,p).o = p.0 by defPg
.= a by AS,Th28
.= q.o by D,POLYNOM7:18;
end;
suppose D: support b = {m};
m in {m} by TARSKI:def 1; then
E: b.m <> 0 by D,PRE_POLY:def 7;
F: b <> EmptyBag n by D;
thus Poly(m,p).o = p.(b.m) by D,defPg
.= 0.F by AS,E,Th28
.= q.o by F,POLYNOM7:18;
end;
suppose E: support b <> {} & support b <> {m};
then D: b <> EmptyBag n;
thus Poly(m,p).o = 0.F by E,defPg
.= q.o by D,POLYNOM7:18;
end;
end;
hence Poly(m,p) = a|(n,F);
end;
now assume AS: Poly(m,p) = a|(n,F);
now let o be object;
assume o in NAT;
then reconsider i = o as Element of NAT;
per cases;
suppose B: i = 0;
then p.i = Poly(m,p).(EmptyBag n) by defPg
.= a by AS,POLYNOM7:18
.= (a|F).i by B,Th28;
hence p.o = (a|F).o;
end;
suppose C: i <> 0;
for o being object st o in {m} holds o in n by K,TARSKI:def 1;
then reconsider S = {m} as finite Subset of n by TARSKI:def 3;
set b = (S,i)-bag;
B: support b = S by C,UPROOTS:8; then
D: b <> EmptyBag n;
m in {m} by TARSKI:def 1;
then p.i = p.(b.m) by UPROOTS:7
.= Poly(m,p).b by B,defPg
.= 0.F by D,AS,POLYNOM7:18
.= (a|F).i by C,Th28;
hence p.o = (a|F).o;
end;
end;
hence p = a|F;
end;
hence thesis by A;
end;
theorem bij3a:
for F being Field
for m being Ordinal st m in card(nonConstantPolys F)
for p being non zero Element of the carrier of Polynom-Ring F
holds Support Poly(m,p) = {EmptyBag card(nonConstantPolys F)} iff p is constant
proof
let F be Field, m be Ordinal;
assume A: m in card(nonConstantPolys F);
let p be non zero Element of the carrier of Polynom-Ring F;
set n = card(nonConstantPolys F);
B: now assume B1: Support Poly(m,p) = {EmptyBag n};
now let b be bag of n;
assume b <> EmptyBag n;
then B2: not b in Support Poly(m,p) by B1,TARSKI:def 1;
b is Element of Bags n by PRE_POLY:def 12;
hence Poly(m,p).b = 0.F by B2,POLYNOM1:def 4;
end;
then Poly(m,p) is Constant by POLYNOM7:def 7;
then consider a being Element of F such that
C: Poly(m,p) = a|(card(nonConstantPolys F),F) by POLYNOM7:17;
p = a|F by C,A,XYZbb;
hence p is constant by RING_4:20;
end;
now assume p is constant; then
consider a being Element of F such that
C: p = a|F by RING_4:20;
D: Poly(m,p) = a|(n,F) by C,A,XYZbb;
p <> 0_.(F); then
a|(n,F) <> 0_(n,F) by A,D,pZero;
hence Support Poly(m,p) = {EmptyBag n} by D,POLYNOM7:14;
end;
hence thesis by B;
end;
lemSet:
for o being object, S being set st S c= {o} holds S = {} or S = {o}
proof
let o be object, S be set;
assume AS1: S c= {o};
assume AS2: S <> {};
set u = the Element of S;
A: u in S by AS2;
now let x be object;
assume x in {o};
then x = o by TARSKI:def 1;
hence x in S by A,AS1,TARSKI:def 1;
end;
hence thesis by AS1,TARSKI:2;
end;
theorem bij3:
for F being Field
for m1,m2 being Ordinal
st m1 in card(nonConstantPolys F) & m2 in card(nonConstantPolys F)
for p1,p2 being non constant Polynomial of F
st Poly(m1,p1) = Poly(m2,p2) holds m1 = m2 & p1 = p2
proof
let F be Field, m1,m2 be Ordinal;
assume A: m1 in card(nonConstantPolys F) & m2 in card(nonConstantPolys F);
let p1,p2 be non constant Polynomial of F;
set n = card(nonConstantPolys F);
assume B: Poly(m1,p1) = Poly(m2,p2);
H: Support Poly(m1,p1)
c= {EmptyBag n} \/ {b where b is bag of n : support b = {m1}} &
Support Poly(m2,p2)
c= {EmptyBag n} \/ {b where b is bag of n : support b = {m2}}by Th14c;
ex b being bag of n st
b in Support Poly(m1,p1) & b in Support Poly(m2,p2) & b <> EmptyBag n
proof
p1 <> 0_.(F); then
B0: Poly(m1,p1) <> 0_(n,F) by A,pZero;
deg p1 > 0 by RATFUNC1:def 2; then
p1 is non constant Element of the carrier of Polynom-Ring F
by RING_4:def 4,POLYNOM3:def 10; then
B2: Support Poly(m1,p1) <> {EmptyBag n} by A,bij3a;
now assume C0: not ex b being object st
b in Support Poly(m1,p1) & b <> EmptyBag n;
now let o be object;
assume o in Support Poly(m1,p1);
then o = EmptyBag n by C0;
hence o in {EmptyBag n} by TARSKI:def 1;
end; then
Support Poly(m1,p1) c= {EmptyBag n};
hence contradiction by B0,YY,B2,lemSet;
end; then
consider b being object such that
B3: b in Support Poly(m1,p1) & b <> EmptyBag n;
reconsider b as bag of n by B3;
thus thesis by B3,B;
end;
then consider b being bag of n such that
D0: b in Support Poly(m1,p1) & b in Support Poly(m2,p2) & b <> EmptyBag n;
b in {EmptyBag n} \/ {b where b is bag of n : support b = {m1}} &
not b in {EmptyBag n} by D0,H,TARSKI:def 1;
then b in {b where b is bag of n : support b = {m1}} by XBOOLE_0:def 3;
then consider b1 being bag of n such that
D1: b = b1 & support b1 = {m1};
b in {EmptyBag n} \/ {b where b is bag of n : support b = {m2}} &
not b in {EmptyBag n} by D0,H,TARSKI:def 1;
then b in {b where b is bag of n : support b = {m2}} by XBOOLE_0:def 3;
then consider b2 being bag of n such that
D2: b = b2 & support b2 = {m2};
m1 in {m2} by D1,D2,TARSKI:def 1;
hence X: m1 = m2 by TARSKI:def 1;
now let i be Element of NAT;
per cases;
suppose E: i = 0;
hence p1.i = Poly(m2,p2).(EmptyBag n) by B,defPg
.= p2.i by E,defPg;
end;
suppose C: i <> 0;
for o being object st o in {m1} holds o in n by A,TARSKI:def 1;
then reconsider S = {m1} as finite Subset of n by TARSKI:def 3;
set b = (S,i)-bag;
E: support b = S by C,UPROOTS:8;
F: m1 in {m1} by TARSKI:def 1;
hence p1.i = p1.(b.m1) by UPROOTS:7
.= Poly(m2,p2).b by E,B,defPg
.= p2.(b.m2) by E,X,defPg
.= p2.i by F,UPROOTS:7,X;
end;
end;
hence thesis;
end;
theorem ZZZ:
for F being Field
for m being Ordinal st m in card(nonConstantPolys F)
for p being constant Polynomial of F
holds Lt Poly(m,p) = EmptyBag card(nonConstantPolys F) & LC Poly(m,p) = p.0
proof
let F be Field, m be Ordinal;
assume AS: m in card(nonConstantPolys F);
let p be constant Polynomial of F;
set q = Poly(m,p), n = card(nonConstantPolys F);
reconsider p1 = p as Element of the carrier of Polynom-Ring F
by POLYNOM3:def 10;
I: p1 is constant by RATFUNC1:def 2;
field(BagOrder n) = Bags n by ORDERS_1:12; then
J: BagOrder n linearly_orders Support q by ORDERS_1:37,ORDERS_1:38; then
B: rng SgmX(BagOrder n,Support q) = Support q by PRE_POLY:def 2;
per cases;
suppose A: q <> 0_(n,F);
consider a being Element of F such that H: p1 = a|F by I,RING_4:20;
C: q = a|(n,F) by H,AS,XYZbb;
D: Support q = {EmptyBag n}
proof
E: now let o be object;
assume D2: o in Support q;
then reconsider b = o as bag of n;
now assume o <> EmptyBag n; then
D3: support b <> {} by PRE_POLY:81;
per cases;
suppose D4: support b = {m};
m in {m} by TARSKI:def 1;
then D5: b.m <> 0 by D4,PRE_POLY:def 7;
q.b = p.(b.m) by D4,defPg .= 0.F by D5,H,Th28;
hence contradiction by D2,POLYNOM1:def 4;
end;
suppose support b <> {m};
then q.b = 0.F by D3,defPg;
hence contradiction by D2,POLYNOM1:def 4;
end;
end;
hence o in {EmptyBag n} by TARSKI:def 1;
end;
now let o be object;
assume o in {EmptyBag n}; then
D1: o = EmptyBag n by TARSKI:def 1;
D2: q.(EmptyBag n) = p.0 by defPg .= a by H,Th28;
a <> 0.F by A,C,POLYNOM7:19;
hence o in Support q by D1,D2,POLYNOM1:def 4;
end;
hence thesis by E,TARSKI:2;
end; then
E: card Support q = 1 by CARD_1:30; then
C: len SgmX(BagOrder n,Support q) = 1 by J,PRE_POLY:11;
SgmX(BagOrder n,Support q)
= <* EmptyBag n *> by D,B,E,J,PRE_POLY:11,FINSEQ_1:39;
hence Lt Poly(m,p) = <* EmptyBag n *>.1 by C,A,defLT
.= EmptyBag n;
hence LC Poly(m,p) = p.0 by defPg;
end;
suppose q = 0_(n,F);
hence Lt Poly(m,p) = EmptyBag n by defLT;
hence LC Poly(m,p) = p.0 by defPg;
end;
end;
theorem XYZaa:
for F being Field
for m being Ordinal st m in card(nonConstantPolys F)
for p being non constant Polynomial of F
holds (Lt Poly(m,p)).m = deg p &
for o being Ordinal st o <> m holds (Lt Poly(m,p)).o = 0
proof
let F be Field, m be Ordinal;
assume AS: m in card(nonConstantPolys F);
let p be non constant Polynomial of F;
set n = card(nonConstantPolys F), q = Poly(m,p);
for o being object st o in {m} holds o in n by AS,TARSKI:def 1;
then reconsider S = {m} as finite Subset of n by TARSKI:def 3;
reconsider degp = deg p as non zero Element of NAT by RATFUNC1:def 2;
H: m in {m} by TARSKI:def 1;
K: deg p = len p - 1 by HURWITZ:def 2; then
I: deg p = len p -' 1 by XREAL_0:def 2;
set b = (S,degp)-bag;
D: support b = S by UPROOTS:8;
E: b in Support q
proof
F: q.b = p.(b.m) by D,defPg .= p.degp by H,UPROOTS:7;
p.degp = LC p by I,RATFUNC1:def 6; then
p.degp <> 0.F;
hence thesis by F,POLYNOM1:def 4;
end;
for b1 being bag of n st b1 in Support q holds b1 <=' b
proof
let b1 be bag of n;
assume b1 in Support q;
then E1: q.b1 <> 0.F by POLYNOM1:def 4;
per cases;
suppose support b1 = {}; then
b1 = EmptyBag n by PRE_POLY:81;
hence thesis by PRE_POLY:60;
end;
suppose E0: support b1 = {m};
per cases;
suppose b1 = b;
hence thesis;
end;
suppose EE: b1 <> b;
E4: q.b1 = p.(b1.m) by E0,defPg;
E3: b.m = len p - 1 by K,H,UPROOTS:7;
E7: now assume b1.m >= b.m; then
per cases by XXREAL_0:1;
suppose E5: b1.m = b.m;
now let i be object;
assume i in n;
per cases;
suppose i = m;
hence b1.i = b.i by E5;
end;
suppose i <> m;
then E6: not i in {m} by TARSKI:def 1;
hence b.i = 0 by UPROOTS:6 .= b1.i by E6,E0,PRE_POLY:def 7;
end;
end;
hence contradiction by EE,PBOOLE:def 10;
end;
suppose b1.m > b.m;
then b1.m >= (len p - 1) + 1 by E3,INT_1:7;
hence contradiction by E4,E1,ALGSEQ_1:8;
end;
end;
ex k being Ordinal st b1.k < b.k &
for l being Ordinal st l in k holds b1.l = b.l
proof
take k = m;
thus b1.k < b.k by E7;
now let l be Ordinal;
assume l in k;
then l <> k;
then E8: not l in {m} by TARSKI:def 1;
hence b.l = 0 by UPROOTS:6 .= b1.l by E8,E0,PRE_POLY:def 7;
end;
hence thesis;
end;
hence thesis by PRE_POLY:def 9,PRE_POLY:def 10;
end;
end;
suppose support b1 <> {} & support b1 <> {m};
hence thesis by E1,defPg;
end;
end; then
F: b = Lt q by E,LT1;
hence (Lt Poly(m,p)).m = deg p by H,UPROOTS:7;
now let o be Ordinal;
assume o <> m;
then not o in {m} by TARSKI:def 1;
hence (Lt Poly(m,p)).o = 0 by F,UPROOTS:6;
end;
hence thesis;
end;
XYZa:
for F being Field
for m being Ordinal st m in card(nonConstantPolys F)
for p being non constant Polynomial of F
holds support(Lt Poly(m,p)) = {m} & (Lt Poly(m,p)).m = deg p
proof
let F be Field, m be Ordinal;
assume AS: m in card(nonConstantPolys F);
let p be non constant Polynomial of F;
set n = card(nonConstantPolys F), q = Poly(m,p);
A: now let o be object;
assume A1: o in support(Lt Poly(m,p)); then
reconsider i = o as Element of n;
(Lt Poly(m,p)).o <> 0 by A1,PRE_POLY:def 7;
then i = m by AS,XYZaa;
hence o in {m} by TARSKI:def 1;
end;
now let o be object;
assume o in {m}; then
o = m by TARSKI:def 1; then
B1: (Lt Poly(m,p)).o = deg p by AS,XYZaa;
deg p > 0 by RATFUNC1:def 2;
hence o in support(Lt Poly(m,p)) by B1,PRE_POLY:def 7;
end;
hence support(Lt Poly(m,p)) = {m} by A,TARSKI:2;
thus thesis by AS,XYZaa;
end;
Th14b: for F being Field
for m being Ordinal st m in card(nonConstantPolys F)
for p being Polynomial of F holds LC Poly(m,p) = LC p
proof
let F be Field, m be Ordinal;
assume K: m in card(nonConstantPolys F);
let p be Polynomial of F;
H: LC p = p.(len p-'1) by RATFUNC1:def 6;
per cases;
suppose I0: p is constant;
reconsider p1 = p as Element of the carrier of Polynom-Ring F
by POLYNOM3:def 10;
p1 is constant by I0,RATFUNC1:def 2; then
consider a being Element of F such that I1: p = a|F by RING_4:20;
thus LC Poly(m,p) = p.0 by K,I0,ZZZ
.= a by I1,Th28
.= LC p by I1,RING_5:6;
end;
suppose I: p is non constant;
then A: p <> 0_.(F);
B: support(Lt Poly(m,p)) = {m} by I,K,XYZa;
E: len p <> 0 by A,POLYNOM4:5;
D: deg p = len p - 1 by HURWITZ:def 2 .= len p -' 1 by E,XREAL_0:def 2;
thus LC Poly(m,p) = p.((Lt Poly(m,p)).m) by B,defPg
.= LC p by I,K,D,H,XYZa;
end;
end;
theorem Th14z:
for F being Field
for m being Ordinal st m in card(nonConstantPolys F)
for p being Polynomial of F
holds LC Poly(m,LM p) = LC Poly(m,p) & Lt Poly(m,LM p) = Lt Poly(m,p)
proof
let F be Field, m be Ordinal;
assume AS: m in card(nonConstantPolys F);
let p be Polynomial of F;
set n = card(nonConstantPolys F);
thus LC Poly(m,LM p) = LC(LM p) by AS,Th14b
.= (LM p).(len(LM p) -' 1) by RATFUNC1:def 6
.= (LM p).(len p -' 1) by POLYNOM4:15
.= p.(len p -' 1) by POLYNOM4:def 1
.= LC p by RATFUNC1:def 6
.= LC Poly(m,p) by Th14b,AS;
per cases;
suppose I0: p is constant;
hence Lt Poly(m,p) = EmptyBag n by AS,ZZZ
.= Lt Poly(m,LM p) by AS,I0,ZZZ;
end;
suppose I0: p is non constant;
len(LM p) = len p by POLYNOM4:15; then
H: deg(LM p) = len p - 1 by HURWITZ:def 2 .= deg p by HURWITZ:def 2;
deg p > 0 by I0,RATFUNC1:def 2; then
I1: LM p is non constant by H,RATFUNC1:def 2;
set b1 = Lt Poly(m,p), b2 = Lt Poly(m,LM p);
now let o be object;
assume o in n;
then reconsider i = o as Ordinal;
per cases;
suppose I4: i = m;
then b1.i = deg p by I0,AS,XYZaa .= b2.i by H,I4,I1,AS,XYZaa;
hence b1.o = b2.o;
end;
suppose I4: i <> m;
then b1.i = 0 by I0,AS,XYZaa .= b2.i by I4,I1,AS,XYZaa;
hence b1.o = b2.o;
end;
end;
hence thesis by PBOOLE:def 10;
end;
end;
theorem Th14y:
for F being Field
for m being Ordinal st m in card(nonConstantPolys F)
for p being Polynomial of F holds
Poly(m,LM p) = Monom(LC Poly(m,p),Lt Poly(m,p))
proof
let F be Field, m be Ordinal;
assume AS: m in card(nonConstantPolys F);
let p be Polynomial of F;
set n = card(nonConstantPolys F), q = Poly(m,LM p);
thus Poly(m,LM p) = Monom(coefficient(q),term(q)) by POLYNOM7:11
.= Monom(LC q,term(q)) by Th14x
.= Monom(LC q,Lt q) by Th14x
.= Monom(LC Poly(m,p),Lt q) by AS,Th14z
.= Monom(LC Poly(m,p),Lt Poly(m,p)) by AS,Th14z;
end;
theorem
for F being Field
for m being Ordinal st m in card(nonConstantPolys F)
for p being Polynomial of F holds LM Poly(m,p) = Poly(m,LM p)
by Th14y;
lemKr3:
for F being Field
for m being Ordinal
for a being Element of F holds Poly(m,a|F) = a|(card(nonConstantPolys F),F)
proof
let F be Field, m be Ordinal, a be Element of F;
set n = card(nonConstantPolys F), pa = Poly(m,a|F);
now let o be object;
assume o in Bags n;
then reconsider b = o as bag of n;
per cases;
suppose support b = {};
then for i being object st i in n holds b.i = {} by PRE_POLY:def 7;
then H: b = EmptyBag n by PBOOLE:6;
then pa.b = (a|F).0 by defPg
.= a by Th28
.= (a|(n,F)).b by H,POLYNOM7:18;
hence pa.o = (a|(n,F)).o;
end;
suppose H: support b = {m};
m in {m} by TARSKI:def 1;
then I: b.m <> 0 & b <> EmptyBag n by H,PRE_POLY:def 7;
pa.b = (a|F).(b.m) by H,defPg
.= 0.F by I,Th28
.= (a|(n,F)).b by I,POLYNOM7:18;
hence pa.o = (a|(n,F)).o;
end;
suppose H: support b <> {} & support b <> {m}; then
I: b <> EmptyBag n;
pa.b = 0.F by H,defPg
.= (a|(n,F)).b by I,POLYNOM7:18;
hence pa.o = (a|(n,F)).o;
end;
end;
hence thesis;
end;
theorem Th14:
for F being Field
for m being Ordinal
for p,q being Polynomial of F holds Poly(m,p+q) = Poly(m,p) + Poly(m,q)
proof
let F be Field, m be Ordinal, p,q be Polynomial of F;
set r1 = Poly(m,p), r2 = Poly(m,q), r = Poly(m,p+q),
n = card(nonConstantPolys F);
I: dom r = Bags n by FUNCT_2:def 1 .= dom(r1+r2) by FUNCT_2:def 1;
now let o be object;
assume o in dom r;
then reconsider b = o as bag of n;
per cases;
suppose support b = {};
then for i being object st i in n holds b.i = {} by PRE_POLY:def 7;
then H: b = EmptyBag n by PBOOLE:6;
then r.b = (p+q).0 by defPg
.= p.0 + q.0 by NORMSP_1:def 2
.= r1.b + q.0 by H,defPg
.= r1.b + r2.b by H,defPg
.= (r1+r2).b by POLYNOM1:15;
hence r.o = (r1 + r2).o;
end;
suppose H: support b = {m};
then r.b = (p+q).(b.m) by defPg
.= p.(b.m) + q.(b.m) by NORMSP_1:def 2
.= r1.b + q.(b.m) by H,defPg
.= r1.b + r2.b by H,defPg
.= (r1+r2).b by POLYNOM1:15;
hence r.o = (r1 + r2).o;
end;
suppose H: support b <> {} & support b <> {m};
then r.b = 0.F + 0.F by defPg
.= r1.b + 0.F by H,defPg
.= r1.b + r2.b by H,defPg
.= (r1+r2).b by POLYNOM1:15;
hence r.o = (r1 + r2).o;
end;
end;
hence thesis by I;
end;
theorem Th14xy:
for F being Field
for m being Ordinal
for p being Polynomial of F holds Poly(m,-p) = - Poly(m,p)
proof
let F be Field, m be Ordinal, p be Polynomial of F;
set r1 = Poly(m,p), r2 = Poly(m,-p), n = card(nonConstantPolys F);
I: dom r2 = Bags n by FUNCT_2:def 1 .= dom(-r1) by FUNCT_2:def 1;
now let o be object;
assume o in dom r2;
then reconsider b = o as bag of n;
per cases;
suppose support b = {};
then for i being object st i in n holds b.i = {} by PRE_POLY:def 7;
then H: b = EmptyBag n by PBOOLE:6;
r2.b = (-p).0 by H,defPg
.= -(p.0) by BHSP_1:44
.= -(r1.b) by H,defPg
.= (-r1).b by POLYNOM1:17;
hence r2.o = (-r1).o;
end;
suppose H: support b = {m};
then r2.b = (-p).(b.m) by defPg
.= - (p.(b.m)) by BHSP_1:44
.= -(r1.b) by H,defPg
.= (-r1).b by POLYNOM1:17;
hence r2.o = (-r1).o;
end;
suppose H: support b <> {} & support b <> {m};
then r2.b = - 0.F by defPg
.= -(r1.b) by H,defPg
.= (-r1).b by POLYNOM1:17;
hence r2.o = (-r1).o;
end;
end;
hence thesis by I;
end;
theorem Th11:
for F being Field,
a being non zero Element of F,
i being Nat, m being Ordinal st m in card(nonConstantPolys F)
holds Poly(m,anpoly(a,0)) *' Poly(m,anpoly(1.F,i)) = Poly(m,anpoly(a,i))
proof
let F be Field, a be non zero Element of F, i be Nat, m being Ordinal;
set n = card(nonConstantPolys F);
assume AS: m in n;
anpoly(a,0) = a|F by FIELD_1:7; then
C: Poly(m,anpoly(a,0)) = a|(n,F) by AS,XYZbb; then
A: Poly(m,anpoly(a,0)) *' Poly(m,anpoly(1.F,i))
= a * Poly(m,anpoly(1.F,i)) by POLYNOM7:27;
set q = a * Poly(m,anpoly(1.F,i));
per cases;
suppose I: i = 0; then
anpoly(1.F,i) = (1.F)|F by FIELD_1:7; then
Poly(m,anpoly(1.F,i)) = (1.F)|(n,F) by AS,XYZbb;
hence Poly(m,anpoly(a,0)) *' Poly(m,anpoly(1.F,i))
= a|(n,F) *' 1_(n,F) by C,POLYNOM7:20
.= Poly(m,anpoly(a,i)) by I,C,POLYNOM1:29;
end;
suppose I: i <> 0;
now let o be Element of Bags n;
per cases;
suppose support o = {};
then B: o = EmptyBag n by PRE_POLY:81;
hence Poly(m,anpoly(a,i)).o
= anpoly(a,i).0 by defPg
.= a * 0.F by I,POLYDIFF:25
.= a * (anpoly(1.F,i).0) by I,POLYDIFF:25
.= a * (Poly(m,anpoly(1.F,i))).o by B,defPg
.= q.o by POLYNOM7:def 9;
end;
suppose I1: support o = {m};
per cases;
suppose I2: o.m = i;
thus Poly(m,anpoly(a,i)).o
= anpoly(a,i).(o.m) by I1,defPg
.= a * 1.F by I2,POLYDIFF:24
.= a * anpoly(1.F,i).(o.m) by I2,POLYDIFF:24
.= a * Poly(m,anpoly(1.F,i)).o by I1,defPg
.= q.o by POLYNOM7:def 9;
end;
suppose I2: o.m <> i;
thus Poly(m,anpoly(a,i)).o
= anpoly(a,i).(o.m) by I1,defPg
.= a * 0.F by I2,POLYDIFF:25
.= a * anpoly(1.F,i).(o.m) by I2,POLYDIFF:25
.= a * Poly(m,anpoly(1.F,i)).o by I1,defPg
.= q.o by POLYNOM7:def 9;
end;
end;
suppose I2: support o <> {} & support o <> {m};
hence Poly(m,anpoly(a,i)).o
= a * 0.F by defPg
.= a * Poly(m,anpoly(1.F,i)).o by I2,defPg
.= q.o by POLYNOM7:def 9;
end;
end;
hence thesis by A;
end;
end;
theorem Th13a:
for F being Field,
i being Element of NAT,
m being Ordinal st m in card(nonConstantPolys F)
holds Poly(m,anpoly(1.F,1)) *' Poly(m,anpoly(1.F,i)) = Poly(m,anpoly(1.F,i+1))
proof
let F be Field, i be Element of NAT, m be Ordinal;
set n = card(nonConstantPolys F);
set f = power Polynom-Ring(card(nonConstantPolys F),F);
assume AS: m in n;
for o being object st o in {m} holds o in n by AS,TARSKI:def 1; then
reconsider S = {m} as finite Subset of n by TARSKI:def 3;
set p1 = Poly(m,anpoly(1.F,1)), p2 = Poly(m,anpoly(1.F,i));
set q = Poly(m,anpoly(1.F,i+1));
per cases;
suppose U: i = 0;
then anpoly(1.F,i) = (1.F)|F by FIELD_1:7;
then p2 = (1.F)|(n,F) by AS,XYZbb .= 1_(n,F) by POLYNOM7:20;
hence p1 *' p2 = q by U,POLYNOM1:29;
end;
suppose U: i <> 0;
now let b be Element of Bags n;
consider s being FinSequence of the carrier of F such that
A: (p1*'p2).b = Sum s & len s = len decomp b &
for k being Element of NAT st k in dom s
ex b1,b2 being bag of n
st (decomp b)/.k = <*b1,b2*> & s/.k = p1.b1*p2.b2 by POLYNOM1:def 10;
A1: dom s = Seg(len decomp b) by A,FINSEQ_1:def 3
.= dom(decomp b) by FINSEQ_1:def 3;
A2: m in {m} by TARSKI:def 1;
per cases;
suppose support b = {}; then
B: b = EmptyBag n by PRE_POLY:81;
C: Sum s = 0.F
proof
divisors b = <* EmptyBag n *> by B,PRE_POLY:67; then
C1: dom(decomp b) = dom <* EmptyBag n *> by PRE_POLY:def 17;
dom <* EmptyBag n *> = Seg 1 by FINSEQ_1:38; then
C2: 1 in dom(decomp b) by C1;
C3: dom s = Seg(len decomp b) by A,FINSEQ_1:def 3
.= dom(decomp b) by FINSEQ_1:def 3; then
consider b1,b2 being bag of n such that
C5: (decomp b)/.1 = <*b1,b2*> & s/.1 = p1.b1*p2.b2 by A,C2;
b1 = (divisors b)/.1 by C5,C2,PRE_POLY:70
.= EmptyBag n by PRE_POLY:65; then
p1.b1 = anpoly(1.F,1).0 by defPg .= 0.F by POLYDIFF:25; then
C6: 0.F = s.1 by C3,C2,C5,PARTFUN1:def 6;
dom(decomp b) = Seg 1 by C1,FINSEQ_1:38; then
1 = len s by A,FINSEQ_1:def 3; then
s = <* s.1 *> by FINSEQ_1:40;
hence Sum s = 0.F by C6,RLVECT_1:44;
end;
thus q.b = anpoly(1.F,i+1).0 by B,defPg
.= (p1 *' p2).b by A,C,POLYDIFF:25;
end;
suppose B: support b = {m}; then
C: q.b = anpoly(1.F,i+1).(b.m) by defPg;
per cases;
suppose C1: b.m = i + 1; then
W: q.b = 1.F by C,POLYDIFF:24;
C2: len(divisors b) = i + 1 + 1 by B,C1,Th13f;
2 <= i + 2 by NAT_1:11; then
2 in Seg(len(divisors b)) by C2; then
C3: 2 in dom(divisors b) by FINSEQ_1:def 3;
2 - 1 > 0; then
2 -' 1 = 1 by XREAL_0:def 2; then
C4: (S,1)-bag = (divisors b).2 by C3,B,Th13f
.= (divisors b)/.2 by C3,PARTFUN1:def 6;
set b3 = (S,1)-bag;
2 in dom(decomp b) by C3,PRE_POLY:def 17; then
C6: (decomp b)/.2 = <*b3, b-'b3*> by C4,PRE_POLY:def 17;
C20: 2 in dom s by A1,C3,PRE_POLY:def 17;
V:s/.2 = 1.F
proof
consider b1,b2 being bag of n such that
C7: (decomp b)/.2 = <*b1,b2*> & s/.2 = p1.b1*p2.b2 by A,C20;
C8: b3 = <*b1,b2*>.1 by C7,C6,FINSEQ_1:44 .= b1;
C9: b-'b3 = <*b1,b2*>.2 by C7,C6,FINSEQ_1:44 .= b2;
C12: b -' b3 = (S,i)-bag
proof
now let o be object;
assume o in n;
per cases;
suppose D2: o = m;
hence (b-'b3).o
= b.m -' b3.m by PRE_POLY:def 6
.= b.m -' 1 by A2,UPROOTS:7
.= b.m - 1 by C1,XREAL_0:def 2
.= (S,i)-bag.o by A2,C1,D2,UPROOTS:7;
end;
suppose o <> m;
then D3: not o in {m} by TARSKI:def 1;
thus (b-'b3).o
= b.o -' b3.o by PRE_POLY:def 6
.= 0 -' b3.o by D3,B,PRE_POLY:def 7
.= 0 by NAT_2:8
.= (S,i)-bag.o by D3,UPROOTS:6;
end;
end;
hence thesis by PBOOLE:def 10;
end; then
support(b-'b3) = {m} by U,UPROOTS:8; then
C10: Poly(m,anpoly(1.F,i)).(b-'b3)
= anpoly(1.F,i).(((S,i)-bag).m) by C12,defPg
.= anpoly(1.F,i).i by A2,UPROOTS:7
.= 1.F by POLYDIFF:24;
support b3 = {m} by UPROOTS:8; then
p1.b3 = anpoly(1.F,1).(b3.m) by defPg
.= anpoly(1.F,1).1 by A2,UPROOTS:7
.= 1.F by POLYDIFF:24;
hence s/.2 = 1.F by C10,C9,C8,C7;
end;
now let k be Element of NAT;
assume C11: k in dom s & k <> 2; then
consider b1,b2 being bag of n such that
C7: (decomp b)/.k = <*b1,b2*> & s/.k = p1.b1*p2.b2 by A;
C10: k in dom(divisors b) by C11,A1,PRE_POLY:def 17; then
k in Seg(len(divisors b)) by FINSEQ_1:def 3; then
1 <= k by FINSEQ_1:1; then
C17: k -' 1 = k - 1 by XREAL_0:def 2;
C9: b1 = (divisors b)/.k by C11,A1,C7,PRE_POLY:70; then
C16: b1 = (divisors b).k by C10,PARTFUN1:def 6;
per cases;
suppose k -' 1 = 0; then
b1 = EmptyBag n by C17,C9,PRE_POLY:65; then
p1.b1 = anpoly(1.F,1).0 by defPg
.= 0.F by POLYDIFF:25;
hence s/.k = 0.F by C7;
end;
suppose C13: k-'1 <> 0;
C15: b1 = (S,k-'1)-bag by B,C16,C10,Th13f; then
C12: support b1 = {m} by C13,UPROOTS:8;
C14: now assume b1.m = 1;
then k -' 1 = 1 by C15,A2,UPROOTS:7;
hence contradiction by C17,C11;
end;
p1.b1 = anpoly(1.F,1).(b1.m) by C12,defPg
.= 0.F by C14,POLYDIFF:25;
hence s/.k = 0.F by C7;
end;
end;
hence (p1 *' p2).b = q.b by V,W,C20,A,POLYNOM2:3;
end;
suppose U: b.m <> i + 1; then
W: q.b = 0.F by C,POLYDIFF:25;
C3: 1 in dom s
proof
1 <= len(decomp b) by NAT_1:14;
then 1 in Seg(len decomp b);
hence thesis by A1,FINSEQ_1:def 3;
end;
C2: now let k be Element of NAT;
assume C11: k in dom s; then
consider b1,b2 being bag of n such that
C3: (decomp b)/.k = <*b1,b2*> & s/.k = p1.b1*p2.b2 by A;
C10: k in dom(divisors b) by C11,A1,PRE_POLY:def 17; then
k in Seg(len(divisors b)) by FINSEQ_1:def 3; then
1 <= k by FINSEQ_1:1; then
C17: k -' 1 = k - 1 by XREAL_0:def 2;
C9: b1 = (divisors b)/.k by C11,A1,C3,PRE_POLY:70; then
C16: b1 = (divisors b).k by C10,PARTFUN1:def 6;
per cases;
suppose k -' 1 = 0; then
b1 = EmptyBag n by C17,C9,PRE_POLY:65; then
p1.b1 = anpoly(1.F,1).0 by defPg
.= 0.F by POLYDIFF:25;
hence s/.k = 0.F by C3;
end;
suppose C13: k-'1 <> 0;
C15: b1 = (S,k-'1)-bag by B,C16,C10,Th13f; then
C12: support b1 = {m} by C13,UPROOTS:8;
C13: b1.m = k -' 1 by C15,A2,UPROOTS:7;
per cases;
suppose C14: b1.m <> 1;
p1.b1 = anpoly(1.F,1).(b1.m) by C12,defPg
.= 0.F by C14,POLYDIFF:25;
hence s/.k = 0.F by C3;
end;
suppose C14: b1.m = 1; then
CC: b1 = (S,1)-bag by C15,A2,UPROOTS:7;
C2: len(divisors b) = b.m + 1 by B,Th13f;
C32: b.m <> 0 by A2,B,PRE_POLY:def 7;
b.m + 1 >= 1 + 1 by C32,NAT_1:14,XREAL_1:6; then
2 in Seg(len(divisors b)) by C2; then
C30: 2 in dom(divisors b) by FINSEQ_1:def 3;
2 - 1 > 0; then
2 -' 1 = 1 by XREAL_0:def 2; then
C4: (S,1)-bag = (divisors b).2 by C30,B,Th13f
.= (divisors b)/.2 by C30,PARTFUN1:def 6;
2 in dom(decomp b) by C30,PRE_POLY:def 17; then
C6: (decomp b)/.2 = <*b1, b-'b1*>
by C13,C14,B,C16,C10,Th13f,C4,PRE_POLY:def 17;
C90: b-'b1 = <*b1,b2*>.2 by C13,C17,C14,C3,C6,FINSEQ_1:44
.= b2;
reconsider j = b.m - 1 as Element of NAT by C32,INT_1:3;
per cases;
suppose C34: b.m - 1 = 0;
now let o be object;
assume o in n;
per cases;
suppose o = m;
hence b.o = b1.o by C14,C34;
end;
suppose H: o <> m;
support b1 = {m} by CC,UPROOTS:8; then
I: not o in support b1 by H,TARSKI:def 1;
not o in support b by H,B,TARSKI:def 1;
hence b.o = 0 by PRE_POLY:def 7
.= b1.o by I,PRE_POLY:def 7;
end;
end;
then b1 = b by PBOOLE:def 10;
then C35: EmptyBag n = b2 by C90,PRE_POLY:56;
C36: i <> 0 by U,C34;
p2.b2 = anpoly(1.F,i).0 by C35,defPg .= 0.F by C36,POLYDIFF:25;
hence s/.k = 0.F by C3;
end;
suppose C34: b.m - 1 <> 0;
C12: b -' b1 = (S,j)-bag
proof
now let o be object;
assume o in n;
per cases;
suppose D2: o = m;
hence (b-'b1).o
= b.m -' 1 by C14,PRE_POLY:def 6
.= b.m - 1 by C32,XREAL_0:def 2
.= (S,j)-bag.o by A2,D2,UPROOTS:7;
end;
suppose o <> m;
then D3: not o in {m} by TARSKI:def 1;
thus (b-'b1).o
= b.o -' b1.o by PRE_POLY:def 6
.= 0 -' b1.o by D3,B,PRE_POLY:def 7
.= 0 by NAT_2:8
.= (S,j)-bag.o by D3,UPROOTS:6;
end;
end;
hence thesis by PBOOLE:def 10;
end; then
C36: support(b-'b1) = {m} by C34,UPROOTS:8;
b2.m = b.m - 1 by C12,C90,A2,UPROOTS:7; then
C35: b2.m <> i by U;
p2.b2 = anpoly(1.F,i).(b2.m) by C36,C90,defPg
.= 0.F by C35,POLYDIFF:25;
hence s/.k = 0.F by C3;
end;
end;
end;
end;
then for k being Element of NAT st k in dom s & k <> 1 holds s/.k = 0.F;
hence (p1 *' p2).b = s/.1 by A,C3,POLYNOM2:3 .= q.b by C2,C3,W;
end;
end;
suppose U1: support b <> {} & support b <> {m}; then
W: q.b = 0.F by defPg;
C3: 1 in dom s
proof
1 <= len(decomp b) by NAT_1:14;
then 1 in Seg(len decomp b);
hence thesis by A1,FINSEQ_1:def 3;
end;
C2: now let k be Element of NAT;
assume C11: k in dom s; then
consider b1,b2 being bag of n such that
C3: (decomp b)/.k = <*b1,b2*> & s/.k = p1.b1*p2.b2 by A;
consider a1,a2 being bag of n such that
C4: (decomp b)/.k = <*a1, a2*> & b = a1 + a2 by C11,A1,PRE_POLY:68;
C5: a1 = <*b1,b2*>.1 by C3,C4,FINSEQ_1:44 .= b1;
C6: a2 = <*b1,b2*>.2 by C3,C4,FINSEQ_1:44 .= b2;
per cases;
suppose support b1 = {};
then b1 = EmptyBag n by PRE_POLY:81;
then p1.b1 = anpoly(1.F,1).0 by defPg
.= 0.F by POLYDIFF:25;
hence s/.k = 0.F by C3;
end;
suppose D1: support b1 <> {};
per cases;
suppose support b2 = {};
then b2 = EmptyBag n by PRE_POLY:81;
then p2.b2 = anpoly(1.F,i).0 by defPg
.= 0.F by U,POLYDIFF:25;
hence s/.k = 0.F by C3;
end;
suppose D2: support b2 <> {};
now assume support b1 = {m} & support b2 = {m};
then support b = {m} \/ {m} by C4,C5,C6,PRE_POLY:38;
hence contradiction by U1;
end; then
per cases;
suppose support b1 <> {m};
then p1.b1 = 0.F by D1,defPg;
hence s/.k = 0.F by C3;
end;
suppose support b2 <> {m};
then p2.b2 = 0.F by D2,defPg;
hence s/.k = 0.F by C3;
end;
end;
end;
end;
then for k being Element of NAT st k in dom s & k <> 1 holds s/.k = 0.F;
hence (p1 *' p2).b = s/.1 by A,C3,POLYNOM2:3 .= q.b by C2,C3,W;
end;
end;
hence thesis;
end;
end;
theorem Th13:
for F being Field,
i being Nat
for m being Ordinal st m in card(nonConstantPolys F) holds
(power Polynom-Ring(card(nonConstantPolys F),F)).(Poly(m,anpoly(1.F,1)),i)
= Poly(m,anpoly(1.F,i))
proof
let F be Field, i be Nat, m be Ordinal;
set n = card(nonConstantPolys F);
set f = power Polynom-Ring(card(nonConstantPolys F),F);
assume AS: m in n;
defpred P[Nat] means
f.(Poly(m,anpoly(1.F,1)),$1) = Poly(m,anpoly(1.F,$1));
reconsider p = Poly(m,anpoly(1.F,1)) as Element of Polynom-Ring(n,F)
by POLYNOM1:def 11;
IA: P[0]
proof
anpoly(1.F,0) = (1.F)|F by FIELD_1:7; then
Poly(m,anpoly(1.F,0))
= (1.F)|(n,F) by AS,XYZbb
.= 1_(n,F) by POLYNOM7:20
.= 1_(Polynom-Ring(n,F)) by POLYNOM1:def 11
.= f.(p,0) by GROUP_1:def 7;
hence thesis;
end;
IS: now let k be Nat;
assume IV: P[k];
H: k is Element of NAT by ORDINAL1:def 12;
reconsider q = Poly(m,anpoly(1.F,k)) as Element of Polynom-Ring(n,F)
by POLYNOM1:def 11;
f.(p,k+1)
= f.(p,k) * p by GROUP_1:def 7
.= Poly(m,anpoly(1.F,k)) *' Poly(m,anpoly(1.F,1)) by IV,POLYNOM1:def 11
.= Poly(m,anpoly(1.F,k+1)) by H,AS,Th13a;
hence P[k+1];
end;
for k being Nat holds P[k] from NAT_1:sch 2(IA,IS);
hence thesis;
end;
theorem Th12:
for F being Field
for p being non constant Element of the carrier of Polynom-Ring F
for m being Ordinal st m in card(nonConstantPolys F)
holds Poly(m,anpoly(LC p,deg p)) = LM Poly(m,p)
proof
let F be Field, p be non constant Element of the carrier of Polynom-Ring F;
let m be Ordinal;
set n = card(nonConstantPolys F);
assume AS: m in n;
deg p > 0 by RING_4:def 4; then
len p - 1 > 0 by HURWITZ:def 2; then
len p - 1 = len p -' 1 by XREAL_0:def 2; then
deg p = len p -' 1 by HURWITZ:def 2;
then anpoly(LC p,deg p)
= anpoly(p.(deg p),deg p) by RATFUNC1:def 6
.= LM p by FIELD_1:11;
hence thesis by AS,Th14y;
end;
:: "... and contend that the ideal generated by all the polynomials
:: f(X_f) in K[S] is not the unit ideal. ..."
theorem KrSet:
for F being Field
for P being finite Subset of the carrier of Polynom-Ring F
ex E being FieldExtension of F
st for p being non constant Element of the carrier of Polynom-Ring F
st p in P holds p is_with_roots_in E
proof
let F be Field;
let P be finite Subset of the carrier of Polynom-Ring F;
defpred P[Nat] means
for F being Field
for P being finite Subset of the carrier of Polynom-Ring F
st card P = $1
ex E being FieldExtension of F
st for p being non constant Element of the carrier of Polynom-Ring F
st p in P holds p is_with_roots_in E;
IA: P[0]
proof
now let F be Field,
P be finite Subset of the carrier of Polynom-Ring F;
assume A: card P = 0;
reconsider E = F as FieldExtension of F by FIELD_4:6;
for p being non constant Element of the carrier of Polynom-Ring F
st p in P holds p is_with_roots_in E by A;
hence ex E being FieldExtension of F
st for p being non constant Element of the carrier of Polynom-Ring F
st p in P holds p is_with_roots_in E;
end;
hence P[0];
end;
IS: now let k be Nat;
assume A: P[k];
now let F be Field,
P be finite Subset of the carrier of Polynom-Ring F;
assume AS: card P = k+1;
set p = the Element of P;
set B = P \ { p };
P <> {} by AS; then
B3: p in P & p in {p} by TARSKI:def 1; then
B1: not(p in B) by XBOOLE_0:def 5;
{ p } c= P by TARSKI:def 1,B3; then
B2: P = B \/ { p } by FIELD_5:1; then
card P = card B + 1 by B1,CARD_2:41; then
consider K being FieldExtension of F such that
C: for p being non constant Element of the carrier of Polynom-Ring F
st p in B holds p is_with_roots_in K by A,AS;
reconsider p as Element of the carrier of Polynom-Ring F by B3;
the carrier of Polynom-Ring F c= the carrier of Polynom-Ring K
by FIELD_4:10; then
reconsider p1 = p as Element of the carrier of Polynom-Ring K;
per cases;
suppose E0: p1 is constant;
now let q be non constant Element of the carrier of Polynom-Ring F;
H: deg q > 0 by RING_4:def 4;
assume E1: q in P;
q <> p by H,E0,FIELD_4:20;
then not q in { p } by TARSKI:def 1;
then q in B by B2,E1,XBOOLE_0:def 3;
hence q is_with_roots_in K by C;
end;
hence ex E being FieldExtension of F
st for p being non constant Element of the carrier of Polynom-Ring F
st p in P holds p is_with_roots_in E;
end;
suppose p1 is non constant; then
reconsider p1 as non constant Element of the carrier of Polynom-Ring K;
consider E being FieldExtension of K such that
D: p1 is_with_roots_in E by FIELD_5:30;
E: K is Subring of E by FIELD_4:def 1;
reconsider E as K-extending FieldExtension of F;
now let q be non constant Element of the carrier of Polynom-Ring F;
assume E1: q in P;
per cases;
suppose E2: q = p1;
consider a being Element of E such that
E3: a is_a_root_of p1,E by D,FIELD_4:def 3;
E4: Ext_eval(p1,a) = 0.E by E3,FIELD_4:def 2;
Ext_eval(p1,a) = Ext_eval(p,a) by FIELD_7:15;
hence q is_with_roots_in E by E2,E4,FIELD_4:def 2,FIELD_4:def 3;
end;
suppose q <> p1;
then not q in { p } by TARSKI:def 1;
then q in B by E1,B2,XBOOLE_0:def 3;
then consider a being Element of K such that
E3: a is_a_root_of q,K by C,FIELD_4:def 3;
the carrier of K c= the carrier of E by E,C0SP1:def 3; then
reconsider a1 = a as Element of E;
Ext_eval(q,a1) = Ext_eval(q,a) by FIELD_7:14
.= 0.K by E3,FIELD_4:def 2
.= 0.E by E,C0SP1:def 3;
hence q is_with_roots_in E by FIELD_4:def 2,FIELD_4:def 3;
end;
end;
hence ex E being FieldExtension of F
st for p being non constant Element of the carrier of Polynom-Ring F
st p in P holds p is_with_roots_in E;
end;
end;
hence P[k+1];
end;
I: for k being Nat holds P[k] from NAT_1:sch 2(IA,IS);
consider n being Nat such that H: card P = n;
thus thesis by I,H;
end;
eval0LM:
for F being Field, E being FieldExtension of F
for m being Ordinal st m in card(nonConstantPolys F)
for p being Polynomial of F
for x being Function of card(nonConstantPolys F),E
st card(Support Poly(m,p)) = 1 holds Ext_eval(Poly(m,p),x) = Ext_eval(p,x/.m)
proof
let F be Field, E be FieldExtension of F;
let m be Ordinal;
assume AS0: m in card(nonConstantPolys F);
let p be Polynomial of F;
let x be Function of card(nonConstantPolys F),E;
set q = Poly(m,p), n = card(nonConstantPolys F);
assume card(Support Poly(m,p)) = 1;
then consider b being object such that
AS: Support Poly(m,p) = {b} by CARD_2:42;
b in Support Poly(m,p) by AS,TARSKI:def 1; then
reconsider b as bag of n;
AS1: q.b = p.(b.m)
proof
A0: b in Support q by AS,TARSKI:def 1;
Support q c= {EmptyBag n} \/
{b where b is bag of n : support b = {m}} by Th14c; then
per cases by A0,XBOOLE_0:def 3;
suppose b in {EmptyBag n};
then A1: b = EmptyBag n by TARSKI:def 1;
hence q.b = p.0 by defPg .= p.(b.m) by A1,PBOOLE:5;
end;
suppose b in {b where b is bag of n : support b = {m}};
then consider b1 being bag of n such that
A1: b1 = b & support b1 = {m};
thus thesis by A1,defPg;
end;
end;
consider y being FinSequence of E such that
A: Ext_eval(q,x) = Sum y & len y = len SgmX(BagOrder n, Support q) &
for i being Element of NAT st 1 <= i & i <= len y
holds y.i = In( (q * SgmX(BagOrder n, Support q)).i, E) *
eval(((SgmX(BagOrder n, Support q))/.i),x) by defeval;
field(BagOrder n) = Bags n by ORDERS_1:12; then
B: BagOrder n linearly_orders Support q by ORDERS_1:37,ORDERS_1:38; then
C: rng SgmX(BagOrder n,Support q) = {b} by AS,PRE_POLY:def 2;
D: len y = card {b} by AS,A,B,PRE_POLY:11 .= 1 by CARD_1:30; then
F: y = <*y.1*> by FINSEQ_1:40;
len SgmX(BagOrder n, Support q) = card {b} by AS,B,PRE_POLY:11
.= 1 by CARD_1:30; then
H: SgmX(BagOrder n, Support q) = <*b*> by C,FINSEQ_1:39; then
dom SgmX(BagOrder n, Support q) = Seg 1 by FINSEQ_1:38; then
I: 1 in dom SgmX(BagOrder n, Support q);
J: SgmX(BagOrder n, Support q).1 = b by H; then
G: eval(((SgmX(BagOrder n, Support q))/.1),x) = eval(b,x) by I,PARTFUN1:def 6;
(q*SgmX(BagOrder n, Support q)).1 = p.(b.m) by J,AS1,I,FUNCT_1:13; then
y.1 = In(p.(b.m),E) * eval(b,x) by G,D,A; then
Z: Ext_eval(Poly(m,p),x) = In(p.(b.m),E) * eval(b,x) by A,F,RLVECT_1:44;
Y: m in dom x by AS0,FUNCT_2:def 1; then
x.m in rng x & rng x c= the carrier of E by RELAT_1:def 19,FUNCT_1:3; then
reconsider a = x.m as Element of E;
per cases;
suppose A1: p = 0_.F;
now let o be object;
assume B: o in Support Poly(m,p);
Support q c= {EmptyBag n} \/
{b where b is bag of n : support b = {m}} by Th14c; then
per cases by B,XBOOLE_0:def 3;
suppose o in {EmptyBag n};
then o = EmptyBag n by TARSKI:def 1;
then Poly(m,p).o = p.0 by defPg;
hence contradiction by B,A1,POLYNOM1:def 4;
end;
suppose o in {b where b is bag of n : support b = {m}};
then consider b being bag of n such that
D: o = b & support b = {m};
Poly(m,p).b = p.(b.m) by D,defPg;
hence contradiction by D,B,A1,POLYNOM1:def 4;
end;
end;
then Support Poly(m,p) = {} by XBOOLE_0:def 1;
then Poly(m,p) = 0_(n,F) by YY;
hence Ext_eval(Poly(m,p),x) = 0.E by ev0
.= Ext_eval(p,x/.m) by A1,ALGNUM_1:13;
end;
suppose p <> 0_.F;
b in Support q by AS,TARSKI:def 1; then
H3: p.(b.m) <> 0.F by POLYNOM1:def 3,AS1;
reconsider i = b.m as Element of NAT;
AA: now let o be object;
assume H0: o in Support p; then
reconsider u = o as Element of NAT;
H4: p.u <> 0.F by H0,POLYNOM1:def 3;
H5: now assume H6: u <> i;
for o being object st o in {m} holds o in n by AS0,TARSKI:def 1;
then reconsider S = {m} as finite Subset of n by TARSKI:def 3;
set b1 = (S,u)-bag, b2 = (S,i)-bag;
J: m in S by TARSKI:def 1;
per cases;
suppose H7: u = 0; then
H12: b1 = EmptyBag n by UPROOTS:9; then
H8: q.b1 = p.u by H7,defPg;
support b2 = S by H7,H6,UPROOTS:8; then
H9: q.b2 = p.(b2.m) by defPg .= p.i by J,UPROOTS:7;
b2.m = i by J,UPROOTS:7; then
b2 <> EmptyBag n by H7,H6,PBOOLE:5; then
H10: card {b1,b2} = 2 by H12,CARD_2:57;
{b1,b2} c= Support q
proof
now let o be object;
assume o in {b1,b2}; then
per cases by TARSKI:def 2;
suppose o = b1;
hence o in Support q by H8,H4,POLYNOM1:def 4;
end;
suppose o = b2;
hence o in Support q by H9,H3,POLYNOM1:def 4;
end;
end;
hence thesis;
end;
hence card(Support q) >= 2 by H10,NAT_1:43;
end;
suppose H7a: u <> 0; then
support b1 = S by UPROOTS:8; then
H9: q.b1 = p.(b1.m) by defPg .= p.u by J,UPROOTS:7;
per cases;
suppose H11: i = 0; then
H12: b2 = EmptyBag n by UPROOTS:9; then
H8: q.b2 = p.i by H11,defPg;
b1.m = u by J,UPROOTS:7; then
b1 <> EmptyBag n by H7a,PBOOLE:5; then
H10: card {b1,b2} = 2 by H12,CARD_2:57;
{b1,b2} c= Support q
proof
now let o be object;
assume o in {b1,b2}; then
per cases by TARSKI:def 2;
suppose o = b1;
hence o in Support q by H9,H4,POLYNOM1:def 4;
end;
suppose o = b2;
hence o in Support q by H8,H3,POLYNOM1:def 4;
end;
end;
hence thesis;
end;
hence card(Support q) >= 2 by H10,NAT_1:43;
end;
suppose i <> 0; then
support b2 = S by UPROOTS:8; then
H9a: q.b2 = p.(b2.m) by defPg .= p.i by J,UPROOTS:7;
b1.m = u & b2.m = i by J,UPROOTS:7; then
H10: card {b1,b2} = 2 by H6,CARD_2:57;
{b1,b2} c= Support q
proof
now let o be object;
assume o in {b1,b2}; then
per cases by TARSKI:def 2;
suppose o = b1;
hence o in Support q by H9,H4,POLYNOM1:def 4;
end;
suppose o = b2;
hence o in Support q by H9a,H3,POLYNOM1:def 4;
end;
end;
hence thesis;
end;
hence card(Support q) >= 2 by H10,NAT_1:43;
end;
end;
end;
card(Support q) = 1 by AS,CARD_1:30;
hence o = b.m by H5;
end;
consider G being FinSequence of E such that
A1: Ext_eval(p,a) = Sum G & len G = len p &
for n being Element of NAT st n in dom G
holds G.n = In(p.(n-'1),E) * (power E).(a,n-'1) by ALGNUM_1:def 1;
A2: now let j be Element of NAT;
assume A3: j in dom G & j <> i+1;
H: F is Subring of E by FIELD_4:def 1;
now assume A4: j -' 1 = i;
j in Seg(len G) by A3,FINSEQ_1:def 3; then
1 <= j & j <= len G by FINSEQ_1:1; then
j -' 1 = j - 1 by XREAL_0:def 2;
hence contradiction by A3,A4;
end;
then not(j -' 1 in Support p) by AA;
then p.(j -' 1) = 0.F by POLYNOM1:def 4
.= 0.E by H,C0SP1:def 3;
then In(p.(j-'1),E) * (power E).(a,j-'1) = 0.E;
hence 0.E = G.j by A1,A3 .= G/.j by A3,PARTFUN1:def 6;
end;
1 <= i + 1 & i + 1 <= len p by H3,NAT_1:11,NAT_1:13,ALGSEQ_1:8; then
i + 1 in Seg(len G) by A1; then
A3: i + 1 in dom G by FINSEQ_1:def 3;
A5: (i + 1) -' 1 = (i + 1) - 1 by NAT_1:11,XREAL_1:233;
A4: Ext_eval(p,a) = G/.(i+1) by A3,A2,A1,POLYNOM2:3
.= G.(i+1) by A3,PARTFUN1:def 6
.= In(p.i,E) * (power E).(a,i) by A5,A3,A1;
per cases;
suppose support b = {};
then A6: b = EmptyBag n by PRE_POLY:81;
then A5: b.m = 0 & eval(b,x) = 1.E by PBOOLE:5,POLYNOM2:14;
thus Ext_eval(Poly(m,p),x)
= In(p.i,E) * 1_E by Z,A6,POLYNOM2:14
.= In(p.i,E) * (power E).(a,i) by A5,GROUP_1:def 7
.= Ext_eval(p,x/.m) by A4,Y,PARTFUN1:def 6;
end;
suppose support b <> {};
then b <> EmptyBag n;
then A6: not b in {EmptyBag n} & b in Support q by AS,TARSKI:def 1;
Support q c= {EmptyBag n} \/
{b where b is bag of n : support b = {m}} by Th14c; then
b in {b where b is bag of n : support b = {m}} by A6,XBOOLE_0:def 3;
then consider b1 being bag of n such that
A5: b1 = b & support b1 = {m};
thus Ext_eval(Poly(m,p),x)
= In(p.i,E) * power(E).(a,i) by A5,Z,POLYNOM2:15
.= Ext_eval(p,x/.m) by A4,Y,PARTFUN1:def 6;
end;
end;
end;
theorem eval0:
for F being Field, E being FieldExtension of F
for m being Ordinal st m in card(nonConstantPolys F)
for p being Polynomial of F
for x being Function of card(nonConstantPolys F),E
holds Ext_eval(Poly(m,p),x) = Ext_eval(p,x/.m)
proof
let F be Field, E be FieldExtension of F; let m be Ordinal;
assume AS: m in card(nonConstantPolys F);
let p be Polynomial of F;
let x be Function of card(nonConstantPolys F),E;
set q = Poly(m,p), n = card(nonConstantPolys F);
defpred P[Nat] means
for p being Polynomial of F for x being Function of n,E
st card(Support Poly(m,p)) = $1
holds Ext_eval(Poly(m,p),x) = Ext_eval(p,x/.m);
IS: now let k be Nat;
assume IV: for n being Nat st n < k holds P[n];
per cases;
suppose A: k = 0;
now let p be Polynomial of F; let x be Function of n,E;
assume card(Support Poly(m,p)) = k;
then Support Poly(m,p) = {} by A;
then B: Poly(m,p) = 0_(n,F) by YY;
then C: p = 0_.(F) by AS,pZero;
thus Ext_eval(Poly(m,p),x) = 0.E by B,ev0
.= Ext_eval(p,x/.m) by C,ALGNUM_1:13;
end;
hence P[k];
end;
suppose A: k <> 0;
then reconsider k1 = k - 1 as Element of NAT by INT_1:3;
H: F is Subring of E by FIELD_4:def 1;
now let p be Polynomial of F; let x be Function of n,E;
assume Z: card(Support Poly(m,p)) = k;
set q = p - LM p;
B: (LM p) + q
= ((LM p) + -LM p) + p by POLYNOM3:26
.= ((LM p) - LM p) + p
.= 0_.(F) + p by POLYNOM3:29;
C: (LM Poly(m,p)) + Poly(m,p-LM p)
= (LM Poly(m,p)) + (Poly(m,p) + Poly(m,-LM p)) by Th14
.= (LM Poly(m,p)) + (Poly(m,p) + - Poly(m,LM p)) by Th14xy
.= (LM Poly(m,p)) + (Poly(m,p) + - LM Poly(m,p)) by AS,Th14y
.= ((LM Poly(m,p)) + -LM Poly(m,p)) + Poly(m,p) by POLYNOM1:21
.= ((LM Poly(m,p)) - LM Poly(m,p)) + Poly(m,p) by POLYNOM1:def 7
.= 0_(n,F) + Poly(m,p) by POLYNOM1:24
.= Poly(m,p) by POLYNOM1:23;
Support Poly(m,q) c< Support Poly(m,p)
proof
Support Poly(m,p) <> {} by A,Z; then
LM Poly(m,p) <> 0_(n,F) by YY,Z2a; then
C5: Support(LM Poly(m,p)) = {Lt Poly(m,p)} by YY,Z2; then
C8: Lt Poly(m,p) in Support(LM Poly(m,p)) by TARSKI:def 1;
Support(LM Poly(m,p)) c= Support Poly(m,p) by YZ; then
C4: Lt Poly(m,p) in Support Poly(m,p) by C8;
set b = Lt Poly(m,p);
C7: Poly(m,q).(Lt Poly(m,p))
= (Poly(m,p) + Poly(m,-LM p)).b by Th14
.= Poly(m,p).b + Poly(m,-LM p).b by POLYNOM1:15
.= Poly(m,p).b + (-Poly(m,LM p)).b by Th14xy
.= Poly(m,p).b + -(Poly(m,LM p).b) by POLYNOM1:17
.= LC Poly(m,p) + -((LM Poly(m,p)).b) by AS,Th14y
.= LC Poly(m,p) + -LC Poly(m,p) by lemY
.= 0.F by RLVECT_1:5; then
C6: not Lt Poly(m,p) in Support Poly(m,q) by POLYNOM1:def 4;
now let o be object;
assume C0: o in Support Poly(m,q); then
reconsider b = o as bag of n;
C3: b is Element of Bags n by PRE_POLY:def 12;
C1: Poly(m,q).b <> 0.F by C0,POLYNOM1:def 4; then
not b in Support(LM Poly(m,p)) by C7,C5,TARSKI:def 1; then
not b in Support Poly(m,LM p) by AS,Th14y; then
C2: Poly(m,LM p).b = 0.F by C3,POLYNOM1:def 4;
Poly(m,q).b = (Poly(m,p) + Poly(m,-LM p)).b by Th14
.= Poly(m,p).b + Poly(m,-LM p).b by POLYNOM1:15
.= Poly(m,p).b + (-Poly(m,LM p)).b by Th14xy
.= Poly(m,p).b + -(Poly(m,LM p).b) by POLYNOM1:17
.= Poly(m,p).b by C2;
hence o in Support Poly(m,p) by C1,C3,POLYNOM1:def 4;
end;
then Support Poly(m,q) c= Support Poly(m,p);
hence thesis by C6,C4,XBOOLE_0:def 8;
end; then
D: card(Support Poly(m,q)) < k by Z,CARD_2:48;
Support Poly(m,p) <> {} by A,Z; then
LM Poly(m,p) <> 0_(n,F) by YY,Z2a; then
Support LM Poly(m,p) <> {} by YY; then
Support(Poly(m,LM p)) <> {} by AS,Th14y; then
ex b being bag of n st Support Poly(m,LM p) = {b} by POLYNOM7:6;
then
E: card(Support Poly(m,LM p)) = 1 by CARD_2:42;
thus Ext_eval(Poly(m,p),x)
= Ext_eval(LM Poly(m,p),x) + Ext_eval(Poly(m,q),x) by H,C,evalpl
.= Ext_eval(LM Poly(m,p),x) + Ext_eval(q,x/.m) by D,IV
.= Ext_eval(Poly(m,LM p),x) + Ext_eval(q,x/.m) by AS,Th14y
.= Ext_eval(LM p,x/.m) + Ext_eval(q,x/.m) by AS,E,eval0LM
.= Ext_eval(p,x/.m) by B,H,ALGNUM_1:15;
end;
hence P[k];
end;
end;
I: for k being Nat holds P[k] from NAT_1:sch 4(IS);
consider n being Nat such that H: card(Support q) = n;
thus thesis by I,H;
end;
ideal1:
for R being non degenerated comRing
for M being non empty Subset of R
for o being object
holds o in M-Ideal iff
ex P being non empty finite Subset of R,
L being LeftLinearCombination of P st P c= M & o = Sum L
proof
let R be non degenerated comRing, M be non empty Subset of R, o be object;
A: now assume
ex P being non empty finite Subset of R,
L being LeftLinearCombination of P st P c= M & o = Sum L;
then consider P being non empty finite Subset of R,
L being LeftLinearCombination of P such that
A1: P c= M & o = Sum L;
now let i be set;
assume i in dom L; then
consider u being Element of R, a being Element of P such that
A2: L/.i = u * a by IDEAL_1:def 9;
a is Element of M by A1;
hence
ex u being Element of R, a being Element of M st L/.i = u*a by A2;
end; then
L is LeftLinearCombination of M by IDEAL_1:def 9;
then o in M-LeftIdeal by A1,IDEAL_1:61;
hence o in M-Ideal by IDEAL_1:63;
end;
defpred P[Nat] means
for L being LinearCombination of M st len L = $1
ex P being non empty finite Subset of R,
L1 being LeftLinearCombination of P st P c= M & Sum L1 = Sum L;
IA: P[0]
proof
now let L be LinearCombination of M;
assume len L = 0;
then L = <*>(the carrier of R);
then I3: Sum L = 0.R by RLVECT_1:43;
set a = the Element of M;
set P = {a};
set K = <*0.R*a*>;
now let u be object;
assume u in P;
then u = a by TARSKI:def 1;
hence u in M;
end; then
I4: P c= M;
I5: Sum K = Sum L by I3,RLVECT_1:44;
now let i be set;
assume I6: i in dom K; then
i in Seg 1 by FINSEQ_1:38; then
I8: i = 1 by TARSKI:def 1,FINSEQ_1:2;
I7: 0.R * a = K.1 .= K/.1 by I6,I8,PARTFUN1:def 6;
a in P by TARSKI:def 1;
hence ex u being Element of R,
a being Element of P st K/.i = u*a by I7,I8;
end; then
K is LeftLinearCombination of P by IDEAL_1:def 9;
hence ex P being non empty finite Subset of R,
L1 being LeftLinearCombination of P st P c= M & Sum L1 = Sum L
by I4,I5;
end;
hence thesis;
end;
IS: now let k be Nat;
assume IV: P[k];
now let L be LinearCombination of M;
assume I2: len L = k + 1; then
L <> {}; then
consider K being LinearCombination of M,
a being Element of R such that
I3: L = K^<* a *> & <*a*> is LinearCombination of M by IDEAL_1:32;
I4: len L = len K + len <*a*> by I3,FINSEQ_1:22
.= len K + 1 by FINSEQ_1:39; then
consider Pk being non empty finite Subset of R,
U being LeftLinearCombination of Pk such that
I6: Pk c= M & Sum U = Sum K by I2,IV;
1 <= len L by I2,NAT_1:11; then
len L in Seg(len L); then
I11: len L in dom L by FINSEQ_1:def 3; then
consider u,v being Element of R, b being Element of M such that
I7: L/.(len L) = u*b*v by IDEAL_1:def 8;
set P = Pk \/ { b };
set V = <* (u*v)*b *>;
now let i be set;
assume E1: i in dom V; then
i in Seg 1 by FINSEQ_1:38; then
E2: i = 1 by TARSKI:def 1,FINSEQ_1:2;
E3: (u*v)*b = V.1 .= V/.1 by E1,E2,PARTFUN1:def 6;
b in {b} by TARSKI:def 1; then
b in P by XBOOLE_0:def 3;
hence ex u being Element of R,
a being Element of P st V/.i = u*a by E3,E2;
end; then
reconsider V as LeftLinearCombination of P by IDEAL_1:def 9;
I8: U^V is LeftLinearCombination of P by XBOOLE_1:7,XBOOLE_1:12;
now let o be object;
assume o in P; then
per cases by XBOOLE_0:def 3;
suppose o in Pk;
hence o in M by I6;
end;
suppose o in { b };
then o = b by TARSKI:def 1;
hence o in M;
end;
end; then
I9: P c= M;
I10: a = L.(len L) by I3,I4,FINSEQ_1:42
.= L/.(len L) by I11,PARTFUN1:def 6
.= u*(b*v) by I7,GROUP_1:def 3
.= u*(v*b) by GROUP_1:def 12
.= (u*v)*b by GROUP_1:def 3;
Sum L = Sum K + Sum <*a*> by I3,RLVECT_1:41
.= Sum(U^V) by I10,I6,RLVECT_1:41;
hence ex P being non empty finite Subset of R,
L1 being LeftLinearCombination of P st P c= M & Sum L1 = Sum L
by I8,I9;
end;
hence P[k+1];
end;
I: for k being Nat holds P[k] from NAT_1:sch 2(IA,IS);
now let o be object;
assume o in M-Ideal; then
consider L being LinearCombination of M such that
C: o = Sum L by IDEAL_1:60;
consider n being Nat such that H: n = len L;
thus ex P being non empty finite Subset of R,
L being LeftLinearCombination of P st P c= M & o = Sum L by H,C,I;
end;
hence thesis by A;
end;
theorem
for R being non degenerated comRing
for M being non empty Subset of R
for o being object
holds o in M-Ideal iff
ex P being non empty finite Subset of R,
L being LinearCombination of P st P c= M & o = Sum L
proof
let R be non degenerated comRing, M be non empty Subset of R, o be object;
A: now assume o in M-Ideal; then
consider P being non empty finite Subset of R,
L being LeftLinearCombination of P such that
A1: P c= M & o = Sum L by ideal1;
L is LinearCombination of P by IDEAL_1:25;
hence ex P being non empty finite Subset of R,
L being LinearCombination of P st P c= M & o = Sum L by A1;
end;
now assume ex P being non empty finite Subset of R,
L being LinearCombination of P st P c= M & o = Sum L; then
consider P being non empty finite Subset of R,
L being LinearCombination of P such that
A2: P c= M & o = Sum L;
L is LeftLinearCombination of P by IDEAL_1:31;
hence o in M-Ideal by A2,ideal1;
end;
hence thesis by A;
end;
:: "... If it is, then there is a finite combination of elements in our ideal
:: which is equal to 1: g1 * f1(X_f1) + ... + gn * fn(X_fn) = 1 with gi in K[S].
:: For simplicity, write Xi instead of X_fi. ...
:: Let F be a finite extension in which each polynomial f1, ..., fn has a root,
:: say ai is a root of fi in F, for i = 1,..., n. Let ai = 0 for i > n.
:: Substitute ai for Xi in our relation. We get 0 = 1, contradiction. ... "
registration
let F be Field;
let g be bijective Function of (nonConstantPolys F),card(nonConstantPolys F);
cluster nonConstantPolys(g,F)-Ideal -> proper;
coherence
proof
set n = card(nonConstantPolys F);
set M = nonConstantPolys(g,F), I = M-Ideal;
set R = Polynom-Ring(n,F);
now assume I is non proper; then I = the carrier of R by SUBSET_1:def 6; then
consider Ps being non empty finite Subset of R,
L being LeftLinearCombination of Ps such that
A: Ps c= M & 1.R = Sum L by ideal1;
now assume L = <*>(the carrier of R);
then Sum L = 0.R by RLVECT_1:43;
hence contradiction by A;
end; then
reconsider L as non empty LeftLinearCombination of Ps;
set PsF =
{p where p is non constant Element of the carrier of Polynom-Ring F :
Poly(g.p,p) in Ps};
H: PsF is finite
proof
defpred P[object,object] means
ex p being non constant Element of the carrier of Polynom-Ring F
st p in PsF & $1 = p & $2 = Poly(g.p,p);
H0: for x being object st x in PsF
ex y being object st y in Ps & P[x,y]
proof
let x be object;
assume H1: x in PsF; then
consider p being non constant
Element of the carrier of Polynom-Ring F such that
H2: x = p & Poly(g.p,p) in Ps;
thus thesis by H1,H2;
end;
consider f being Function of PsF,Ps such that
H1: for x being object st x in PsF holds P[x,f.x] from FUNCT_2:sch 1(H0);
H3: rng f c= Ps by RELAT_1:def 19;
f is one-to-one
proof
now let x1,x2 be object;
assume H4: x1 in dom f & x2 in dom f & f.x1 = f.x2; then
consider p1 being non constant
Element of the carrier of Polynom-Ring F such that
H5: p1 in PsF & x1 = p1 & f.x1 = Poly(g.p1,p1) by H1;
consider p2 being non constant
Element of the carrier of Polynom-Ring F such that
H6: p2 in PsF & x2 = p2 & f.x2 = Poly(g.p2,p2) by H1,H4;
H7: p1 is non constant Polynomial of F &
p2 is non constant Polynomial of F
proof
reconsider q1 = p1, q2 = p2 as Polynomial of F;
deg p1 > 0 & deg p2 > 0 by RING_4:def 4;
hence thesis by RATFUNC1:def 2;
end;
rng g c= card(nonConstantPolys F) &
dom g = nonConstantPolys F &
p1 in nonConstantPolys F &
p2 in nonConstantPolys F by FUNCT_2:def 1,RELAT_1:def 19; then
g.p1 in n & g.p2 in n by FUNCT_1:3;
hence x1 = x2 by H4,H5,H6,H7,bij3;
end;
hence thesis;
end; then
dom f is finite by H3,CARD_1:59;
hence thesis by FUNCT_2:def 1;
end;
PsF is Subset of the carrier of Polynom-Ring F
proof
now let o be object;
assume o in PsF; then
consider p being non constant Element of the carrier of Polynom-Ring F
such that H: o = p & Poly(g.p,p) in Ps;
thus o in the carrier of Polynom-Ring F by H;
end;
then PsF c= the carrier of Polynom-Ring F;
hence thesis;
end; then
reconsider PsF as finite Subset of the carrier of Polynom-Ring F by H;
consider E being FieldExtension of F such that
B: for p being non constant Element of the carrier of Polynom-Ring F
st p in PsF holds p is_with_roots_in E by KrSet;
reconsider S = Polynom-Ring(n,E) as comRingExtension of R by ringext;
D: F is Subring of E by FIELD_4:def 1;
ex x being Function of n,E
st for pF being non constant Element of the carrier of Polynom-Ring F
st pF in PsF
ex a being Element of E st x.(g.pF) = a & Ext_eval(pF,a) = 0.E
proof
defpred P[object,object] means
(ex pF being non constant Element of the carrier of Polynom-Ring F
st pF in PsF & g.pF = $1 &
ex a being Element of E st $2 = a & Ext_eval(pF,a) = 0.E) or
((not ex pF being non constant Element of the carrier of Polynom-Ring F
st pF in PsF & g.pF = $1) & $2 = 0.E);
C0: for x being object st x in n
ex y being object st y in the carrier of E & P[x,y]
proof
let x be object;
assume x in n;
per cases;
suppose
ex pF being non constant Element of the carrier of Polynom-Ring F
st pF in PsF & g.pF = x; then
consider pF being non constant
Element of the carrier of Polynom-Ring F such that
I: pF in PsF & g.pF = x;
consider a being Element of E such that
J: a is_a_root_of pF,E by I,B,FIELD_4:def 3;
Ext_eval(pF,a) = 0.E by J,FIELD_4:def 2;
hence thesis by I;
end;
suppose not
ex pF being non constant Element of the carrier of Polynom-Ring F
st pF in PsF & g.pF = x;
hence thesis;
end;
end;
consider f being Function of n,the carrier of E such that
C1: for x being object st x in n holds P[x,f.x] from FUNCT_2:sch 1(C0);
take f;
now let pF be non constant Element of the carrier of Polynom-Ring F;
assume C2: pF in PsF;
set m = g.pF;
dom g = nonConstantPolys F by FUNCT_2:def 1; then
pF in dom g; then
m in rng g & rng g c= n by FUNCT_1:3,RELAT_1:def 19; then
consider q being non constant Element of the carrier of Polynom-Ring F
such that
C3: q in PsF & g.q = m & ex a being Element of E
st f.m = a & Ext_eval(q,a) = 0.E by C1,C2;
dom g = nonConstantPolys F by FUNCT_2:def 1; then
C4: q in dom g & pF in dom g; then
q = (g").(g.q) by FUNCT_2:26 .= pF by C4,C3,FUNCT_2:26;
hence ex a being Element of E
st f.(g.pF) = a & Ext_eval(pF,a) = 0.E by C3;
end;
hence thesis;
end; then
consider x being Function of n,E such that
C: for pF being non constant Element of the carrier of Polynom-Ring F
st pF in PsF
ex a being Element of E st x.(g.pF) = a & Ext_eval(pF,a) = 0.E;
reconsider p = Sum L as Polynomial of n,F by POLYNOM1:def 11;
consider G being FinSequence of the carrier of E such that
U: len G = len L &
Ext_eval(p,x) = Sum G &
for i being set st i in dom G
for q being Polynomial of n,F st q = L.i holds G.i = Ext_eval(q,x)
by ideal2;
E: for i being Nat st i in dom L
for q being Polynomial of n,F st q = L.i holds Ext_eval(q,x) = 0.E
proof
let i be Nat;
assume E1: i in dom L;
let q be Polynomial of n,F;
assume q = L.i; then
q = L/.i by E1,PARTFUN1:def 6; then
consider u being Element of R, p being Element of Ps such that
E2: q = u * p by E1,IDEAL_1:def 9;
reconsider p as Polynomial of n,F by POLYNOM1:def 11;
p in nonConstantPolys(g,F) by A; then
consider pF being
non constant Element of the carrier of Polynom-Ring F such that
E3: Poly(g.pF,pF) = p;
E7: dom x = n by FUNCT_2:def 1;
E8: rng g c= card(nonConstantPolys F) &
dom g = nonConstantPolys F &
pF in nonConstantPolys F by FUNCT_2:def 1,RELAT_1:def 19;
E9: g.pF in rng g by E8,FUNCT_1:3; then
E6: x.(g.pF) = x/.(g.pF) by E8,E7,PARTFUN1:def 6;
pF in PsF by E3; then
consider a being Element of E such that
E4: x.(g.pF) = a & Ext_eval(pF,a) = 0.E by C;
E5: Ext_eval(Poly(g.pF,pF),x) = 0.E by E9,E8,E6,E4,eval0;
reconsider u as Polynomial of n,F by POLYNOM1:def 11;
thus Ext_eval(q,x)
= Ext_eval(u *' Poly(g.pF,pF),x) by E2,E3,POLYNOM1:def 11
.= Ext_eval(u,x) * 0.E by D,E5,evalti
.= 0.E;
end;
F: for i being Element of NAT st i in dom G holds G/.i = 0.E
proof
let i be Element of NAT;
assume F1: i in dom G;
dom G = Seg(len G) by FINSEQ_1:def 3; then
F2: i in dom L by U,F1,FINSEQ_1:def 3; then
L.i = L/.i by PARTFUN1:def 6; then
reconsider q = L.i as Polynomial of n,F by POLYNOM1:def 11;
thus G/.i = G.i by F1,PARTFUN1:def 6
.= Ext_eval(q,x) by F1,U
.= 0.E by F2,E;
end; then
H: for i being Element of NAT st i in dom G & i <> 1 holds G/.i = 0.E;
G: 1 in dom G
proof
len L >= 1 by FINSEQ_1:20;
then 1 in Seg(len L);
hence 1 in dom G by U,FINSEQ_1:def 3;
end; then
0.E = G/.1 by F
.= Ext_eval(p,x) by U,G,H,POLYNOM2:3
.= Ext_eval(1_(n,F),x) by A,POLYNOM1:def 11
.= 1.E by D,eval1;
hence contradiction;
end;
hence thesis;
end;
end;
:: "... Let m be a maximal ideal generated by all polynomials f(X_f) in K[S].
:: Then K[S]/m is a field, ..."
definition
let R be non degenerated commutative Ring;
let I be proper Ideal of R;
mode maxIdeal of I -> Ideal of R means :defideal:
I c= it & it is maximal;
existence
proof
set S = {A where A is Ideal of R: I c= A & A is proper};
set P = RelIncl S;
A2: field P = S by WELLORD2:def 1;
A3: S has_upper_Zorn_property_wrt P
proof
let Y be set such that
A4: Y c= S and
A5: P |_2 Y is being_linear-order;
per cases;
suppose
A6: Y is empty;
take x = I;
thus x in S;
thus thesis by A6;
end;
suppose
H: Y is non empty;
set e = the Element of Y;
take x = union Y;
x c= the carrier of R
proof
let a be object;
assume a in x;
then consider Z being set such that
A9: a in Z and
A10: Z in Y by TARSKI:def 4;
Z in S by A4,A10;
then ex A being Ideal of R st Z = A & I c= A & A is proper;
hence thesis by A9;
end;
then reconsider B = x as Subset of R;
A11: B is right-ideal
proof
let p, a be Element of R;
assume a in B;
then consider Aa being set such that
A12: a in Aa and
A13: Aa in Y by TARSKI:def 4;
Aa in S by A4,A13;
then consider Ia being Ideal of R such that
A14: Aa = Ia and
I c= Ia & Ia is proper;
a*p in Ia & Ia c= B by A12,A13,A14,IDEAL_1:def 3,ZFMISC_1:74;
hence thesis;
end;
A15: B is left-ideal
proof
let p, a be Element of R;
assume a in B;
then consider Aa being set such that
A16: a in Aa and
A17: Aa in Y by TARSKI:def 4;
Aa in S by A4,A17;
then consider Ia being Ideal of R such that
A18: Aa = Ia and
I c= Ia & Ia is proper;
p*a in Ia & Ia c= B by A16,A17,A18,IDEAL_1:def 2,ZFMISC_1:74;
hence thesis;
end;
A19: now
assume B is non proper;
then 1.R in B by A15,IDEAL_1:19;
then consider Aa being set such that
A20: 1.R in Aa and
A21: Aa in Y by TARSKI:def 4;
Aa in S by A4,A21;
then ex Ia being Ideal of R st Aa = Ia & I c= Ia & Ia is proper;
hence contradiction by A20,IDEAL_1:19;
end;
A22: B is add-closed
proof
A23: field (P |_2 Y) = Y by A2,A4,ORDERS_1:71;
let a, b be Element of R;
A24: now
let A be Ideal of R;
assume a in A & b in A;
then
A25: a+b in A by IDEAL_1:def 1;
assume A in Y;
hence a+b in B by A25,TARSKI:def 4;
end;
assume a in B;
then consider Aa being set such that
A26: a in Aa and
A27: Aa in Y by TARSKI:def 4;
Aa in S by A4,A27;
then
A28: ex Ia being Ideal of R st Aa = Ia & I c= Ia & Ia is proper;
assume b in B;
then consider Ab being set such that
A29: b in Ab and
A30: Ab in Y by TARSKI:def 4;
[Aa,Ab] in P |_2 Y or [Ab,Aa] in P |_2 Y or Aa = Ab
by A27,A30,A23,A5,RELAT_2:def 14,RELAT_2:def 6;
then [Aa,Ab] in P or [Ab,Aa] in P or Aa = Ab by XBOOLE_0:def 4;
then
A31: Aa c= Ab or Ab c= Aa by A4,A27,A30,WELLORD2:def 1;
Ab in S by A4,A30;
then ex Ib being Ideal of R st Ab = Ib & I c= Ib & Ib is proper;
hence a+b in B by A26,A27,A29,A30,A24,A28,A31;
end;
A40: I c= x
proof
now let o be object;
assume H1: o in I;
e in S by A4,H; then
consider A being Ideal of R such that
K: e = A & I c= A & A is proper;
thus o in x by K,H1,H,TARSKI:def 4;
end;
hence thesis;
end;
e in S by A4,H;
then consider A being Ideal of R such that
A32: e = A and
I c= A & A is proper;
ex q being object st q in A by XBOOLE_0:def 1;
then B is non empty by H,A32,TARSKI:def 4;
hence
A33: x in S by A22,A11,A19,A40;
let y be set;
assume
A34: y in Y;
then y c= x by ZFMISC_1:74;
hence thesis by A4,A33,A34,WELLORD2:def 1;
end;
end;
P partially_orders S by WELLORD2:21,WELLORD2:19,20;
then consider x being set such that
A4: x is_maximal_in P by A2,A3,ORDERS_1:63;
consider H being Ideal of R such that
A6: x = H and
A7: I c= H & H is proper by A2,A4;
take H;
thus I c= H by A7;
now let J be Ideal of R;
assume A10: H c= J; then
A8: I c= J by A7;
now
assume J is proper;
then
A9: J in S by A8;
then [H,J] in P by A10,A2,A4,A6,WELLORD2:def 1;
hence H = J by A2,A4,A6,A9;
end;
hence J = H or J is non proper;
end;
then H is quasi-maximal by RING_1:def 3;
hence H is maximal by A7;
end;
end;
registration
let R be non degenerated commutative Ring;
let I be proper Ideal of R;
cluster -> maximal for maxIdeal of I;
coherence by defideal;
end;
definition
let F be Field;
let g be bijective Function of (nonConstantPolys F),card(nonConstantPolys F);
let I be maxIdeal of nonConstantPolys(g,F)-Ideal;
func KroneckerField(F,g,I) -> Field equals
Polynom-Ring(card(nonConstantPolys F),F) / I;
coherence by RING_1:21;
end;
:: " ... and we have a canonical map sigma: K[S] -> K[S]/m.
:: For any polynomial f in K[X] of degree >= 1, the polynomial sigma(f) has
:: a root in K[S]/m, which is an extension of sigma(K). ..."
:: Embedding F in KroneckerField(F,b,I)
definition
let n be Ordinal;
let R be non degenerated Ring;
func canHom(n,R) -> Function of R,Polynom-Ring(n,R) means :defcanhom:
for a being Element of R holds it.a = a|(n,R);
existence
proof
set B = Polynom-Ring(n,R);
defpred P[object,object] means
ex a being Element of R st $1 = a & $2 = a|(n,R);
X: for x being object st x in the carrier of R
ex y being object st y in the carrier of B & P[x,y]
proof
let x be object;
assume x in the carrier of R;
then reconsider a = x as Element of R;
reconsider y = a|(n,R) as Element of B by POLYNOM1:def 11;
take y;
thus thesis;
end;
consider g being Function of the carrier of R,the carrier of B
such that
Z: for x being object st x in the carrier of R holds P[x,g.x]
from FUNCT_2:sch 1(X);
now let x be Element of R;
consider a being Element of R such that
H: x = a & g.x = a|(n,R) by Z;
thus g.x = x|(n,R) by H;
end;
then consider f being Function of R,B such that
Y: for x being Element of R holds f.x = x|(n,R);
take f;
thus thesis by Y;
end;
uniqueness
proof
set B = Polynom-Ring(n,R);
let g1,g2 be Function of R,B such that
A1: for a being Element of R holds g1.a = a|(n,R) and
A2: for a being Element of R holds g2.a = a|(n,R);
A: dom g1 = the carrier of R by FUNCT_2:def 1
.= dom g2 by FUNCT_2:def 1;
now let x be object;
assume x in dom g1;
then reconsider a = x as Element of R;
thus g1.x = a|(n,R) by A1 .= g2.x by A2;
end;
hence thesis by A;
end;
end;
registration
let n be Ordinal;
let R be non degenerated comRing;
cluster canHom(n,R) -> additive multiplicative unity-preserving;
coherence
proof
set f = canHom(n,R);
hereby
let x,y be Element of R;
f.x = x|(n,R) & f.y = y|(n,R) by defcanhom;
hence f.x + f.y = x|(n,R) + y|(n,R) by POLYNOM1:def 11
.= (x + y)|(n,R) by T4a
.= f.(x+y) by defcanhom;
end;
hereby
let x,y be Element of R;
f.x = x|(n,R) & f.y = y|(n,R) by defcanhom;
hence f.x * f.y = x|(n,R) *' (y|(n,R)) by POLYNOM1:def 11
.= (x * y)|(n,R) by T4
.= f.(x*y) by defcanhom;
end;
thus f.1_R = (1.R)|(n,R) by defcanhom
.= 1_(n,R) by POLYNOM7:20
.= 1_(Polynom-Ring(n,R)) by POLYNOM1:def 11;
end;
end;
registration
let n be Ordinal;
let R be non degenerated comRing;
cluster canHom(n,R) -> monomorphism;
coherence
proof
set f = canHom(n,R);
now let x1,x2 be object;
assume AS: x1 in the carrier of R & x2 in the carrier of R & f.x1 = f.x2;
then reconsider a = x1, b = x2 as Element of R;
a|(n,R) = f.x2 by AS,defcanhom .= b|(n,R) by defcanhom;
hence x1 = x2 by POLYNOM7:21;
end;
then f is one-to-one by FUNCT_2:19;
hence thesis;
end;
end;
definition
let F be Field;
let g be bijective Function of (nonConstantPolys F),card(nonConstantPolys F);
let I be maxIdeal of nonConstantPolys(g,F)-Ideal;
func emb(F,I,g) -> Function of F,KroneckerField(F,g,I) equals
(canHom I) * (canHom(card(nonConstantPolys F),F));
coherence;
end;
registration
let F be Field;
let g be bijective Function of (nonConstantPolys F),card(nonConstantPolys F);
let I be maxIdeal of nonConstantPolys(g,F)-Ideal;
cluster emb(F,I,g) -> additive multiplicative unity-preserving;
coherence
proof
set f = emb(F,I,g), n = card(nonConstantPolys F),
R = Polynom-Ring(n,F);
J: dom(canHom(card(nonConstantPolys F),F)) = the carrier of F by FUNCT_2:def 1;
hereby
let x,y be Element of F;
A1: x|(n,F) is Element of R & y|(n,F) is Element of R by POLYNOM1:def 11;
reconsider xF = x|(n,F),yF = y|(n,F) as Element of R by POLYNOM1:def 11;
reconsider a = Class(EqRel(R,I),x|(n,F)),
b = Class(EqRel(R,I),y|(n,F)) as Element of KroneckerField(F,g,I)
by A1,RING_1:12;
A: f.x = (canHom I).(canHom(card(nonConstantPolys F),F).x) by J,FUNCT_1:13
.= (canHom I).(x|(n,F)) by defcanhom
.= Class(EqRel(R,I),x|(n,F)) by A1,RING_2:def 5;
B: f.y = (canHom I).(canHom(card(nonConstantPolys F),F).y) by J,FUNCT_1:13
.= (canHom I).(y|(n,F)) by defcanhom
.= Class(EqRel(R,I),y|(n,F)) by A1,RING_2:def 5;
E: canHom(card(nonConstantPolys F),F).(x+y)
= canHom(card(nonConstantPolys F),F).x +
canHom(card(nonConstantPolys F),F).y by VECTSP_1:def 20
.= xF + canHom(card(nonConstantPolys F),F).y by defcanhom
.= xF + yF by defcanhom;
thus f.x + f.y
= Class(EqRel(R,I),xF+yF) by A,B,RING_1:13
.= (canHom I).(canHom(card(nonConstantPolys F),F).(x+y)) by E,RING_2:def 5
.= f.(x+y) by J,FUNCT_1:13;
end;
thus f is multiplicative;
thus f is unity-preserving;
end;
end;
registration
let F be Field;
let g be bijective Function of (nonConstantPolys F),card(nonConstantPolys F);
let I be maxIdeal of nonConstantPolys(g,F)-Ideal;
cluster emb(F,I,g) -> monomorphism;
coherence;
end;
registration
let F be Field;
let g be bijective Function of (nonConstantPolys F),card(nonConstantPolys F);
let I be maxIdeal of nonConstantPolys(g,F)-Ideal;
cluster KroneckerField(F,g,I) -> F-monomorphic F-homomorphic;
coherence
proof
set f = emb(F,I,g);
f is monomorphism;
hence KroneckerField(F,g,I) is F-monomorphic by RING_3:def 3;
hence KroneckerField(F,g,I) is F-homomorphic;
end;
end;
:: the roots are - analogous to Kronecker's construction - the classes [Xm]
definition
let F be Field;
let m be Ordinal;
let g be bijective Function of (nonConstantPolys F),card(nonConstantPolys F);
let I be maxIdeal of nonConstantPolys(g,F)-Ideal;
func KrRoot(I,m) -> Element of KroneckerField(F,g,I) equals
Class(EqRel(Polynom-Ring(card(nonConstantPolys F),F),I),Poly(m,<%0.F,1.F%>));
coherence
proof
Poly(m,<%0.F,1.F%>) is Element of Polynom-Ring(card(nonConstantPolys F),F)
by POLYNOM1:def 11;
hence thesis by RING_1:12;
end;
end;
theorem TH39:
for F being Field
for g being bijective Function of (nonConstantPolys F),card(nonConstantPolys F)
for I being maxIdeal of nonConstantPolys(g,F)-Ideal
for a being Element of F holds
emb(F,I,g).a = Class(EqRel(Polynom-Ring(card(nonConstantPolys F),F),I),
a|(card(nonConstantPolys F),F))
proof
let F be Field;
let g be bijective Function of (nonConstantPolys F),card(nonConstantPolys F);
let I be maxIdeal of nonConstantPolys(g,F)-Ideal;
let a be Element of F;
set n = card(nonConstantPolys F), R = Polynom-Ring(n,F);
reconsider pa = a|(n,F) as Element of Polynom-Ring(n,F) by POLYNOM1:def 11;
dom(canHom(n,F)) = the carrier of F by FUNCT_2:def 1; then
emb(F,I,g).a
= (canHom I).(canHom(card(nonConstantPolys F),F).a) by FUNCT_1:13
.= (canHom I).(pa) by defcanhom
.= Class(EqRel(R,I),pa) by RING_2:def 5;
hence thesis;
end;
theorem TH40:
for F being Field
for g being bijective Function of (nonConstantPolys F),card(nonConstantPolys F)
for I being maxIdeal of nonConstantPolys(g,F)-Ideal
for p being Element of the carrier of Polynom-Ring F
for n being Element of NAT holds
((PolyHom emb(F,I,g)).p).n =
Class(EqRel(Polynom-Ring(card(nonConstantPolys F),F),I),
(p.n)|(card(nonConstantPolys F),F))
proof
let F be Field;
let g be bijective Function of (nonConstantPolys F),card(nonConstantPolys F);
let I be maxIdeal of nonConstantPolys(g,F)-Ideal;
let p be Element of the carrier of Polynom-Ring F;
let m be Nat;
set n = card(nonConstantPolys F), R = Polynom-Ring(n,F);
((PolyHom emb(F,I,g)).p).m
= emb(F,I,g).(p.m) by FIELD_1:def 2
.= Class(EqRel(R,I),(p.m)|(n,F)) by TH39;
hence thesis;
end;
Kr2a:
for F being Field
for g being bijective Function of (nonConstantPolys F),card(nonConstantPolys F)
for I being maxIdeal of nonConstantPolys(g,F)-Ideal
for p being constant Element of the carrier of Polynom-Ring F
for n being Ordinal
holds eval((PolyHom emb(F,I,g)).p,KrRoot(I,n)) =
Class(EqRel(Polynom-Ring(card(nonConstantPolys F),F),I), Poly(n,p))
proof
let F be Field;
let g be bijective Function of (nonConstantPolys F),card(nonConstantPolys F);
let I be maxIdeal of nonConstantPolys(g,F)-Ideal;
let p be constant Element of the carrier of Polynom-Ring F;
let n be Ordinal;
set E = KroneckerField(F,g,I), u = KrRoot(I,n), m = card(nonConstantPolys F);
reconsider q = (PolyHom emb(F,I,g)).p as
Element of the carrier of Polynom-Ring E;
deg q = deg p & deg p <= 0 by FIELD_1:31,RING_4:def 4; then
reconsider q as constant Element of the carrier of Polynom-Ring E
by RING_4:def 4;
consider c being Element of F such that H0: p = c|F by RING_4:20;
reconsider r = Poly(n,c|F) as Element of Polynom-Ring(m,F) by POLYNOM1:def 11;
set h = emb(F,I,g);
q = (h.c)|E by H0,FIELD_8:13;
hence eval((PolyHom emb(F,I,g)).p,u)
= h.c by RING_5:8
.= Class(EqRel(Polynom-Ring(m,F),I), c|(m,F)) by TH39
.= Class(EqRel(Polynom-Ring(m,F),I), Poly(n,p)) by H0,lemKr3;
end;
lemKr2:
for F being Field
for g being bijective Function of (nonConstantPolys F),card(nonConstantPolys F)
for I being maxIdeal of nonConstantPolys(g,F)-Ideal
for p being non constant Element of the carrier of Polynom-Ring F
for m being Ordinal st m in card(nonConstantPolys F)
holds eval(LM((PolyHom emb(F,I,g)).p),KrRoot(I,m)) =
Class(EqRel(Polynom-Ring(card(nonConstantPolys F),F),I), LM Poly(m,p))
proof
let F be Field;
let g be bijective Function of (nonConstantPolys F),card(nonConstantPolys F);
let I be maxIdeal of nonConstantPolys(g,F)-Ideal;
let p be non constant Element of the carrier of Polynom-Ring F;
let o be Ordinal;
assume A0: o in card(nonConstantPolys F);
set m = card(nonConstantPolys F);
set LMf = Leading-Monomial(p), LMfe = Leading-Monomial((PolyHom emb(F,I,g)).p);
set z = KrRoot(I,o), E = KroneckerField(F,g,I);
set efp = (PolyHom emb(F,I,g)).p; set n = len efp -' 1;
reconsider f1 = p as non zero Polynomial of F;
reconsider fnF = (p.n)|(m,F) as Element of the carrier of Polynom-Ring(m,F)
by POLYNOM1:def 11;
reconsider x = Poly(o,<%0.F,1.F%>) as
Element of the carrier of Polynom-Ring(m,F)
by POLYNOM1:def 11;
A3: efp.n = Class(EqRel(Polynom-Ring(m,F),I), (p.n)|(m,F)) by TH40;
A4: (power E).(z,n) = z|^n by BINOM:def 2
.= Class(EqRel(Polynom-Ring(m,F),I),x|^n) by FIELD_1:2;
set a = p.n;
I: deg p = deg efp by FIELD_1:31;
H: deg p = len p - 1 & deg efp = len efp - 1 by HURWITZ:def 2;
deg p > 0 & deg efp > 0 by I,RING_4:def 4; then
len efp - 1 > 0 & len p - 1 > 0 by HURWITZ:def 2; then
J: len p - 1 = len p -' 1 & len efp - 1 = len efp -' 1 by XREAL_0:def 2;
A1: n = deg p by H,J,FIELD_1:31;
A2: a = LC p by H,I,RATFUNC1:def 6;
A8: fnF = Poly(o,a|F) by A0,XYZbb .= Poly(o,anpoly(a,0)) by FIELD_1:7;
x|^n = (power Polynom-Ring (m,F)).(Poly(o,<%-0.F,1.F%>),n) by BINOM:def 2
.= (power Polynom-Ring (m,F)).(Poly(o,rpoly(1,0.F)),n) by RING_5:10
.= (power Polynom-Ring (m,F)).(Poly(o,anpoly(1.F,1)),n) by FIELD_1:8
.= Poly(o,anpoly(1.F,n)) by A0,Th13; then
A9: fnF * (x|^n)
= Poly(o,anpoly(a,0)) *' Poly(o,anpoly(1.F,n)) by A8,POLYNOM1:def 11
.= Poly(o,anpoly(a * 1.F,0 + n)) by A0,A2,Th11
.= LM Poly(o,p) by A0,A2,A1,Th12;
eval(LMfe,z) = efp.n * (power E).(z,n) by POLYNOM4:22;
hence eval(LMfe,z) = Class(EqRel(Polynom-Ring(m,F),I), LM Poly(o,p))
by A9,A4,A3,RING_1:14;
end;
Kr3:
for F being Field
for g being bijective Function of (nonConstantPolys F),card(nonConstantPolys F)
for I being maxIdeal of nonConstantPolys(g,F)-Ideal
for p being non constant Element of the carrier of Polynom-Ring F
for m being Ordinal st m in card(nonConstantPolys F)
holds eval((PolyHom emb(F,I,g)).p,KrRoot(I,m)) =
Class(EqRel(Polynom-Ring(card(nonConstantPolys F),F),I), Poly(m,p))
proof
let F be Field;
let g be bijective Function of (nonConstantPolys F),card(nonConstantPolys F);
let I be maxIdeal of nonConstantPolys(g,F)-Ideal;
let p be non constant Element of the carrier of Polynom-Ring F;
let n be Ordinal;
assume A0: n in card(nonConstantPolys F);
set m = card(nonConstantPolys F), E = KroneckerField(F,g,I);
set h = canHom emb(F,I,g);
defpred P[Nat] means
for f being non constant Element of the carrier of Polynom-Ring F
st len f = $1 holds eval((PolyHom emb(F,I,g)).f,KrRoot(I,n))
= Class(EqRel(Polynom-Ring(m,F),I), Poly(n,f));
A1: now let f be non constant Element of the carrier of Polynom-Ring F;
assume B: len f = 0;
deg f = len f - 1 by HURWITZ:def 2;
hence eval((PolyHom emb(F,I,g)).f,KrRoot(I,n))
= Class(EqRel(Polynom-Ring(m,F),I), Poly(n,f)) by B;
end;
A3: now let k be Nat;
assume IV: for m being Nat st m < k holds P[m];
now let f be non constant Element of the carrier of Polynom-Ring F;
assume A5: len f = k;
per cases;
suppose k = 0;
hence eval((PolyHom emb(F,I,g)).f,KrRoot(I,n))
= Class(EqRel(Polynom-Ring(m,F),I), Poly(n,f)) by A5,A1;
end;
suppose k > 0; then
consider q being Polynomial of F such that
A6: len q < len f & f = q + Leading-Monomial(f) &
for n being Element of NAT st n < len f-1 holds q.n = f.n
by A5,POLYNOM4:16;
reconsider q as Element of the carrier of Polynom-Ring F
by POLYNOM3:def 10;
reconsider LMf = LM f as Element of the carrier of Polynom-Ring F
by POLYNOM3:def 10;
reconsider r1 = (PolyHom emb(F,I,g)).LMf,
r2 = (PolyHom emb(F,I,g)).q,
f1 = (PolyHom emb(F,I,g)).f as Polynomial of E;
A7: (PolyHom emb(F,I,g)).f
= (PolyHom emb(F,I,g)).(LMf+q) by A6,POLYNOM3:def 10
.= (PolyHom emb(F,I,g)).LMf + (PolyHom emb(F,I,g)).q
by VECTSP_1:def 20
.= r1 + r2 by POLYNOM3:def 10;
A14: LM((PolyHom emb(F,I,g)).f) = (PolyHom emb(F,I,g)).LMf
by FIELD_1:32;
A8: eval(LM((PolyHom emb(F,I,g)).f),KrRoot(I,n))
= Class(EqRel(Polynom-Ring(m,F),I), LM Poly(n,f)) by A0,lemKr2;
A11: Poly(n,f) = Poly(n,LM f) + Poly(n,q) by A6,Th14
.= LM Poly(n,f) + Poly(n,q) by A0,Th14y;
LM Poly(n,f) is Element of Polynom-Ring(m,F) &
Poly(n,q) is Element of Polynom-Ring(m,F) by POLYNOM1:def 11; then
reconsider a1 = Class(EqRel(Polynom-Ring(m,F),I), LM Poly(n,f)),
a2 = Class(EqRel(Polynom-Ring(m,F),I), Poly(n,q))
as Element of E by RING_1:12;
reconsider u = Poly(n,f),
u1 = LM Poly(n,f),
u2 = Poly(n,q)
as Element of the carrier of Polynom-Ring(m,F) by POLYNOM1:def 11;
A16: a1 + a2 = Class(EqRel(Polynom-Ring(m,F),I),u1+u2)
by RING_1:13;
A18: u1 + u2 = Poly(n,f) by A11,POLYNOM1:def 11;
per cases;
suppose q is non constant; then
eval((PolyHom emb(F,I,g)).q,KrRoot(I,n))
= Class(EqRel(Polynom-Ring(m,F),I), Poly(n,q)) by A5,A6,IV;
hence eval((PolyHom emb(F,I,g)).f,KrRoot(I,n))
= Class(EqRel(Polynom-Ring(m,F),I), Poly(n,f))
by A8,A16,A18,A14,A7,POLYNOM4:19;
end;
suppose q is constant; then
eval((PolyHom emb(F,I,g)).q,KrRoot(I,n))
= Class(EqRel(Polynom-Ring(m,F),I), Poly(n,q)) by Kr2a;
hence eval((PolyHom emb(F,I,g)).f,KrRoot(I,n))
= Class(EqRel(Polynom-Ring(m,F),I), Poly(n,f))
by A8,A16,A18,A14,A7,POLYNOM4:19;
end;
end;
end;
hence P[k];
end;
A11: for k being Nat holds P[k] from NAT_1:sch 4(A3);
ex n being Nat st len p = n;
hence thesis by A11;
end;
theorem Kr2:
for F being Field
for g being bijective Function of (nonConstantPolys F),card(nonConstantPolys F)
for I being maxIdeal of nonConstantPolys(g,F)-Ideal
for p being Element of the carrier of Polynom-Ring F
for m being Ordinal st m in card(nonConstantPolys F)
holds eval((PolyHom emb(F,I,g)).p,KrRoot(I,m)) =
Class(EqRel(Polynom-Ring(card(nonConstantPolys F),F),I), Poly(m,p))
proof
let F be Field;
let g be bijective Function of (nonConstantPolys F),card(nonConstantPolys F);
let I be maxIdeal of nonConstantPolys(g,F)-Ideal;
let p be Element of the carrier of Polynom-Ring F;
let m be Ordinal;
assume A0: m in card(nonConstantPolys F);
per cases;
suppose p is constant;
hence thesis by Kr2a;
end;
suppose p is non constant;
hence thesis by A0,Kr3;
end;
end;
theorem Kr1:
for F being Field
for g being bijective Function of (nonConstantPolys F),card(nonConstantPolys F)
for I being maxIdeal of nonConstantPolys(g,F)-Ideal
for p being non constant Element of the carrier of Polynom-Ring F
holds KrRoot(I,g.p) is_a_root_of (PolyHom emb(F,I,g)).p
proof
let F be Field;
let g be bijective Function of (nonConstantPolys F),card(nonConstantPolys F);
let I be maxIdeal of nonConstantPolys(g,F)-Ideal;
let p be non constant Element of the carrier of Polynom-Ring F;
set n = card(nonConstantPolys F),
R = Polynom-Ring(card(nonConstantPolys F),F);
rng g c= card(nonConstantPolys F) &
dom g = nonConstantPolys F &
p in nonConstantPolys F by FUNCT_2:def 1,RELAT_1:def 19; then
A0: g.p in n by FUNCT_1:3;
reconsider q = Poly(g.p,p) as
Element of the carrier of Polynom-Ring(n,F) by POLYNOM1:def 11;
A1: q in nonConstantPolys(g,F);
A3: nonConstantPolys(g,F) c= nonConstantPolys(g,F)-Ideal by IDEAL_1:def 14;
nonConstantPolys(g,F)-Ideal c= I by defideal; then
A2: q - 0.(Polynom-Ring(n,F)) in I by A1,A3;
eval((PolyHom emb(F,I,g)).p,KrRoot(I,g.p))
= Class(EqRel(Polynom-Ring(n,F),I), q) by A0,Kr2
.= Class(EqRel(Polynom-Ring(n,F),I), 0.Polynom-Ring(n,F)) by A2,RING_1:6
.= 0.KroneckerField(F,g,I) by RING_1:def 6;
hence thesis by POLYNOM5:def 7;
end;
:: "... Using the same set-theoretic argument as in Proposition 2.3, we conclude
:: that there exists an extension E1 of K in which every polynomial f in K[X] of
:: degree >= 1 has a root in E1."
theorem :: Artin
for F being Field
ex E1 being FieldExtension of F
st for p being non constant Element of the carrier of Polynom-Ring F
holds p is_with_roots_in E1
proof
let F be Field;
set b = the bijective
Function of (nonConstantPolys F),card(nonConstantPolys F);
set I = the maxIdeal of nonConstantPolys(b,F)-Ideal;
set KF = KroneckerField(F,b,I);
consider FP being Field such that
X1: KF,FP are_isomorphic &
(the carrier of FP) /\ ((the carrier of KF) \/ (the carrier of F)) = {}
by FIELD_5:29;
X: [#] F = the carrier of F & [#] FP = the carrier of FP;
X2: F,FP are_disjoint
proof
now assume A: (the carrier of F) /\ (the carrier of FP) <> {};
set x = the Element of (the carrier of F) /\ (the carrier of FP);
B: x in the carrier of F & x in the carrier of FP by A,XBOOLE_0:def 4;
then x in (the carrier of KF) \/ (the carrier of F) by XBOOLE_0:def 3;
hence contradiction by B,X1,XBOOLE_0:def 4;
end;
hence thesis by X,FIELD_2:def 1;
end;
consider phi being Function of KF,FP such that
X3: phi is isomorphism by X1;
set h = phi * emb(F,I,b);
reconsider h as Function of F,FP;
X4: h is linear one-to-one by X3,RINGCAT1:1; then
reconsider FP as F-monomorphic Field by RING_3:def 3;
reconsider h as Monomorphism of F,FP by X4;
reconsider E = embField h as Field by X2,FIELD_2:12;
emb_iso h is onto by X2,FIELD_2:15; then
reconsider embisoh = (emb_iso h)" as Function of FP,E by FUNCT_2:25;
emb_iso h is additive multiplicative by X2,FIELD_2:13,FIELD_2:14; then
Y: emb_iso h is linear one-to-one onto by X2,FIELD_2:15; then
reconsider FP as E-isomorphic Field by RING_3:def 4;
reconsider embisoh as Isomorphism of FP,E by Y,RING_3:73;
set iso = embisoh * phi;
reconsider iso as Function of KF,E;
X5: iso is RingHomomorphism by X3,RINGCAT1:1;
then reconsider E as KF-homomorphic Field by RING_2:def 4;
reconsider iso as Homomorphism of KF,E by X5;
F is Subfield of E by FIELD_2:17;
then reconsider E as FieldExtension of F by FIELD_4:7;
take E;
now let p be non constant Element of the carrier of Polynom-Ring F;
set u = KrRoot(I,b.p), n = card(nonConstantPolys F);
u is_a_root_of (PolyHom emb(F,I,b)).p by Kr1; then
B: eval((PolyHom iso).((PolyHom emb(F,I,b)).p),iso.u) = 0.E
by FIELD_1:33,POLYNOM5:def 7;
reconsider a = iso.KrRoot(I,b.p) as Element of E;
(PolyHom iso).((PolyHom emb(F,I,b)).p) = p
proof
set g = (PolyHom iso).((PolyHom emb(F,I,b)).p);
A: for a being Element of F holds iso.(emb(F,I,b).a) = a
proof
let a be Element of F;
a|(n,F) is Element of Polynom-Ring(n,F) by POLYNOM1:def 11; then
reconsider v =
Class(EqRel(Polynom-Ring(n,F),I), a|(n,F))
as Element of KroneckerField(F,b,I) by RING_1:12;
dom(emb(F,I,b)) = the carrier of F by FUNCT_2:def 1; then
C: h.a = phi.(emb(F,I,b).a) by FUNCT_1:13 .= phi.v by TH39;
the carrier of (embField h) = carr h by FIELD_2:def 7
.= ([#]FP \ rng h) \/ [#]F by FIELD_2:def 2
.= ((the carrier of FP)\(rng h))\/(the carrier of F);
then reconsider a1 = a as Element of embField h by XBOOLE_0:def 3;
a in F; then
D: (emb_iso h).a1 = phi.v by C,FIELD_2:def 8;
A1: dom phi = the carrier of KF by FUNCT_2:def 1;
A3: dom(emb_iso h) = the carrier of E by FUNCT_2:def 1;
thus iso.(emb(F,I,b).a) = (embisoh * phi).v by TH39
.= ((emb_iso h)").(phi.v) by A1,FUNCT_1:13
.= a by D,A3,FUNCT_1:34;
end;
now let x be object;
assume x in NAT;
then reconsider i = x as Element of NAT;
g.i = iso.(((PolyHom emb(F,I,b)).p).i) by FIELD_1:def 2
.= iso.(Class(EqRel(Polynom-Ring(n,F),I),(p.i)|(n,F))) by TH40
.= iso.(emb(F,I,b).(p.i)) by TH39;
hence g.x = p.x by A;
end;
hence thesis;
end;
then Ext_eval(p,a) = 0.E by B,FIELD_4:26;
hence p is_with_roots_in E by FIELD_4:def 3,def 2;
end;
hence thesis;
end;