:: Renamings and a Condition-free Formalization of {K}ronecker's Construction
:: by Christoph Schwarzweller
::
:: Received May 19, 2020
:: Copyright (c) 2020-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, VECTSP_2, STRUCT_0,
SUBSET_1, SUPINF_2, BINOP_1, NAT_1, MESFUNC1, REALSET1, C0SP1, FUNCT_2,
POLYNOM1, POLYNOM2, POLYNOM3, WAYBEL20, EC_PF_1, HURWITZ, RLVECT_1,
FUNCT_1, RELAT_1, LATTICES, CARD_1, IDEAL_1, GROUP_6, GROUP_2, ZFMISC_1,
XBOOLE_0, FINSET_1, NUMBERS, MSSUBFAM, POLYNOM5, GROUP_1, GROEB_2, MOD_4,
YELLOW_8, RING_2, RING_3, RING_5, ALGNUM_1, ARYTM_1, FDIFF_1, CARD_2,
NEWTON, WELLORD1, XXREAL_0, XCMPLX_0, EQREL_1, ORDINAL2, POLYNOM8,
FUNCSDOM, FINSEQ_1, ALGSEQ_1, RATFUNC1, AFINSQ_1, GAUSSINT, ORDINAL1,
INT_1, INT_3, BINOP_2, FUNCT_7, QUOFIELD, RING_4, RLSUB_1, RLVECT_5,
FIELD_1, FIELD_2, FIELD_3, FIELD_4, FIELD_5, FOMODEL1;
notations TARSKI, XBOOLE_0, SUBSET_1, BINOP_1, RELAT_1, RELSET_1, ORDINAL1,
INT_2, ARYTM_3, REALSET1, FUNCT_1, FUNCT_2, ZFMISC_1, NUMBERS, FINSET_1,
CARD_1, CARD_2, EQREL_1, XCMPLX_0, XXREAL_0, GR_CY_1, INT_3, ENUMSET1,
NEWTON, POLYNOM3, POLYNOM4, POLYNOM5, RINGCAT1, STRUCT_0, GROUP_1,
RATFUNC1, ALGSEQ_1, GROUP_6, MOD_4, ALGSTR_0, RLVECT_1, MATRLIN, IDEAL_1,
VECTSP_2, VECTSP_9, HURWITZ, VECTSP_1, VECTSP_4, C0SP1, EC_PF_1,
QUOFIELD, GAUSSINT, RING_1, RING_2, RING_3, RING_4, RING_5, ALGNUM_1,
FIELD_1, FIELD_2, FIELD_3, FIELD_4;
constructors ARYTM_3, TSEP_1, VFUNCT_1, RATFUNC1, GCD_1, REALSET1, RINGCAT1,
ALGSEQ_1, GR_CY_1, VECTSP_9, ALGNUM_1, RING_5, POLYNOM4, CARD_2, NEWTON,
FIELD_2, FIELD_3, FIELD_4;
registrations XBOOLE_0, ORDINAL1, RELSET_1, XXREAL_0, XREAL_0, NAT_1, INT_1,
MEMBERED, STRUCT_0, VECTSP_1, ALGSTR_1, POLYNOM4, VFUNCT_1, FUNCT_2,
ALGSTR_0, POLYNOM3, GAUSSINT, SUBSET_1, RLVECT_1, FUNCT_1, CARD_1,
CARD_2, FINSET_1, RATFUNC1, INT_3, RELAT_1, MOD_4, RINGCAT1, RING_1,
RING_2, RING_3, RING_4, RING_5, NEWTON, REALSET1, POLYNOM5, MATRLIN,
VECTSP_9, FIELD_1, FIELD_2, FIELD_3, FIELD_4, NAT_6;
requirements NUMERALS, SUBSET, BOOLE, REAL, ARITHM;
definitions VECTSP_1, GROUP_1, GROUP_6;
equalities BINOP_1, REALSET1, STRUCT_0, ALGSTR_0, ORDINAL1, POLYNOM3, FIELD_1;
expansions STRUCT_0, GROUP_1, ALGSTR_0, RLVECT_1, VECTSP_1, TARSKI, GROUP_6,
QUOFIELD, BINOP_1, FUNCT_2, FUNCT_1, RINGCAT1, FIELD_1;
theorems GROUP_1, VECTSP_1, RLVECT_1, FUNCT_2, GCD_1, C0SP1, TARSKI, CARD_1,
ENUMSET1, FUNCT_1, RELAT_1, RING_3, CARD_2, POLYNOM5, RING_4, RING_5,
NAT_1, HURWITZ, XREAL_1, XBOOLE_0, MOD_4, RING_2, POLYNOM3, ALGNUM_1,
ZFMISC_1, XXREAL_0, XBOOLE_1, RING_1, FIELD_2, NEWTON, RINGCAT1, FIELD_1,
XTUPLE_0, INT_3, ALGSEQ_1, IDEAL_1, NUMBERS, RAT_1, ARYTM_3, INT_1,
VECTSP_9, EC_PF_1, UPROOTS, RATFUNC1, ALGSTR_0, FIELD_3, VECTSP_4,
FIELD_4, AXIOMS, LIOUVIL2;
schemes NAT_1, BINOP_1, FUNCT_2;
begin :: Preliminaries
theorem
for X,Y being set st Y c= X holds (X \ Y) \/ Y = X
proof
let X,Y be set;
assume AS: Y c= X;
A: now let o be object;
assume B: o in X;
per cases;
suppose o in Y;
hence o in (X \ Y) \/ Y by XBOOLE_0:def 3;
end;
suppose not o in Y;
then o in X \ Y by B,XBOOLE_0:def 5;
hence o in (X \ Y) \/ Y by XBOOLE_0:def 3;
end;
end;
now let o be object;
assume B: o in (X \ Y) \/ Y;
now assume C: not o in X;
then not o in (X \ Y);
then o in Y by B,XBOOLE_0:def 3;
hence contradiction by AS,C;
end;
hence o in X;
end;
hence thesis by A,TARSKI:2;
end;
theorem th0a:
for n,m being Nat holds n +` m = n + m & n *` m = n * m
proof
let n,m be Nat;
thus n +` m = card n +` card m
.= card(n + m) by CARD_2:38
.= n + m;
thus n *` m = card [:n,m:] by CARD_2:def 2
.= card n * card m by CARD_2:46
.= n * m;
end;
theorem th0k:
for n,m being Nat holds (n c= m iff n <= m) & (n in m iff n < m)
proof
let n,m be Nat;
H: n = Segm n & m = Segm m;
A: now assume n c= m;
then card Segm n c= card Segm m;
hence n <= m by NAT_1:40;
end;
now assume n <= m;
then card Segm n c= card Segm m by NAT_1:40;
hence n c= m;
end;
hence n c= m iff n <= m by A;
A: now assume n in m;
then card n in card m;
hence n < m by H,NAT_1:41;
end;
now assume n < m;
then card Segm n in card Segm m by NAT_1:41;
hence n in m;
end;
hence n in m iff n < m by A;
end;
theorem th0e:
for n being Nat holds exp(2,n) = 2|^n
proof
let n be Nat;
defpred P[Nat] means exp(2,$1) = 2|^($1);
IA: P[0]
proof
thus exp(2,0) = 1 by CARD_2:25 .= 2|^0 by NEWTON:4;
end;
IS: now let k be Nat;
assume IV: P[k];
exp(2,k+1) = exp(2,k+`1) by th0a
.= exp(2,k) *` exp(2,1) by CARD_2:28
.= (2|^k) *` 2 by IV,CARD_2:27
.= (2|^k) * 2 by th0a
.= 2|^(k+1) by NEWTON:6;
hence P[k+1];
end;
for k being Nat holds P[k] from NAT_1:sch 2(IA,IS);
hence thesis;
end;
theorem th0n:
for n being Nat st n >= 3 holds n + n < 2|^n
proof
let n be Nat;
assume AS: n >= 3;
defpred P[Nat] means $1 + $1 < 2|^($1);
IA: P[3]
proof
2|^(2+1) = 2|^(1+1) * 2 by NEWTON:6
.= (2|^1 * 2|^1) * 2 by NEWTON:6
.= (2 * 2) * 2;
hence 2|^3 > 3 + 3;
end;
IS: now let k be Nat;
assume A: k >= 3;
assume B: P[k];
C: 2|^(k+1) = 2|^k * 2 by NEWTON:6
.= 2|^k + 2|^k;
D: 2|^k + 2|^k > (k + k) + (k + k) by B,XREAL_1:8;
k > 1 by A,XXREAL_0:2; then
k + k > k + 1 by XREAL_1:8; then
(k + k) + (k + k) > (k + 1) + (k + 1) by XREAL_1:8;
hence P[k+1] by C,D,XXREAL_0:2;
end;
for k being Nat st k >= 3 holds P[k] from NAT_1:sch 8(IA,IS);
hence thesis by AS;
end;
theorem th0b:
for n being Nat st n >= 3 holds n +` n in exp(2,n)
proof
let n be Nat;
assume AS: n >= 3;
n +` n = n + n by th0a; then
n +` n < 2|^n by AS,th0n; then
n +` n in 2|^n by th0k;
hence thesis by th0e;
end;
theorem
NAT meets bool NAT
proof
0 in NAT; then
{0} c= NAT by TARSKI:def 1; then
NAT /\ bool NAT <> {} by CARD_1:49,XBOOLE_0:def 4;
hence thesis by XBOOLE_0:def 7;
end;
theorem th1: ::: isn't it just not X in X?
for X being set ex o being object st not o in X
proof
let X be set;
now assume for u being object st u in bool X holds u in X;
then bool X c= X;
then B: card bool X c= card X by CARD_1:11;
card X in card bool X by CARD_1:14;
hence contradiction by B,CARD_1:3;
end;
hence thesis;
end;
theorem thre:
for X being set ex Y being set st card X c= card Y & X /\ Y = {}
proof
let X be set;
set D = bool(X) /\ X;
set Y = bool(X) \ (bool(X) /\ X);
C: now assume H: Y /\ X <> {};
set o = the Element of (Y /\ X);
H1: o in Y & o in X by H,XBOOLE_0:def 4; then
o in bool X & not o in D by XBOOLE_0:def 5;
hence contradiction by H1,XBOOLE_0:def 4;
end;
B: card bool X c= card Y +` card X
proof
now let o be object;
assume B1: o in bool X;
per cases;
suppose o in X;
hence o in Y \/ X by XBOOLE_0:def 3;
end;
suppose not o in X;
then not o in D by XBOOLE_0:def 4;
then o in Y by B1,XBOOLE_0:def 5;
hence o in Y \/ X by XBOOLE_0:def 3;
end;
end;
then B1: bool X c= Y \/ X;
card(Y \/ X) = card Y +` card X by C,CARD_2:35,XBOOLE_0:def 7;
hence thesis by B1,CARD_1:11;
end;
per cases;
suppose AS: card X = 0;
set u = the object;
take Y = {u};
thus card X c= card Y by AS;
now assume A: X /\ Y <> {};
set o = the Element of X /\ Y;
o in X & o in Y by A,XBOOLE_0:def 4;
hence contradiction by AS;
end;
hence thesis;
end;
suppose AS: card X = 1;
then consider o being object such that A: X = {o} by CARD_2:42;
consider u being object such that B: not u in {o} by th1;
take Y = {u};
thus card X c= card Y by AS,CARD_2:42;
now assume C: X /\ Y <> {};
set x = the Element of X /\ Y;
x in X & x in Y by C,XBOOLE_0:def 4;
hence contradiction by A,B,TARSKI:def 1;
end;
hence thesis;
end;
suppose AS: card X = 2;
then consider x,y being object such that
A: x <> y & X = {x,y} by CARD_2:60;
consider u being object such that B: not u in {x,y} by th1;
consider v being object such that C: not v in {x,y,u} by th1;
take Y = {u,v};
u <> v by C,ENUMSET1:def 1;
hence card X c= card Y by AS,CARD_2:57;
now assume H: X /\ Y <> {};
set o = the Element of X /\ Y;
E: o in X & o in Y by H,XBOOLE_0:def 4; then
F: o = x or o = y by A,TARSKI:def 2;
per cases by E,TARSKI:def 2;
suppose o = u;
hence contradiction by A,B,H,XBOOLE_0:def 4;
end;
suppose o = v;
hence contradiction by F,C,ENUMSET1:def 1;
end;
end;
hence thesis;
end;
suppose AS: card X is finite & card X <> 0 & card X <> 1 & card X <> 2;
reconsider n = card X as Nat by AS;
D: now assume n < 2 + 1;
then n <= 2 by NAT_1:13;
then n = 0 or ... or n = 2;
hence contradiction by AS;
end;
B0: card bool X = exp(2,n) by CARD_2:31;
now assume card Y c= card X;
then card Y +` n c= n +` n by CARD_2:83;
then card bool X c= n +` n by B;
hence contradiction by D,B0,th0b,CARD_1:4;
end;
hence thesis by C;
end;
suppose AS: not card X is finite;
now assume card Y c= card X;
then card Y +` card X c= card X +` card X by CARD_2:83; then
card Y +` card X c= card X by AS,CARD_2:75; then
card bool X c= card X by B;
hence contradiction by CARD_1:4,CARD_1:14;
end;
hence thesis by C;
end;
end;
theorem thre1:
for X,Y being set st card X c= card Y
ex Z being set st Z c= Y & card Z = card X
proof
let X,Y be set;
assume card X c= card Y; then
consider f being Function such that
A: f is one-to-one & dom f = X & rng f c= Y by CARD_1:10;
take Z = rng f;
thus thesis by A,CARD_1:70;
end;
theorem
for X being set ex Y being set st card X = card Y & X /\ Y = {}
proof
let X be set;
consider Y being set such that
A: card X c= card Y & X /\ Y = {} by thre;
consider Z being set such that B: Z c= Y & card Z = card X by A,thre1;
take Z;
thus card X = card Z by B;
now assume C: X /\ Z <> {};
set o = the Element of X /\ Z;
o in X & o in Z by C,XBOOLE_0:def 4;
hence contradiction by A,B,XBOOLE_0:def 4;
end;
hence thesis;
end;
theorem pr1:
for E being Field, F being Subfield of E holds F is Subring of E
proof
let E be Field, F be Subfield of E;
the carrier of F c= the carrier of E
& the addF of F = (the addF of E) || the carrier of F
& the multF of F = (the multF of E) || the carrier of F
& 1.E = 1.F & 0.E = 0.F by EC_PF_1:def 1;
hence thesis by C0SP1:def 3;
end;
theorem
for F being Field,
R being Subring of F holds R is Subfield of F iff R is Field
proof
let E be Field, R be Subring of E;
now assume B: R is Field;
the carrier of R c= the carrier of E
& the addF of R = (the addF of E)||the carrier of R
& the multF of R = (the multF of E)||the carrier of R
& 1.R = 1.E & 0.R = 0.E by C0SP1:def 3;
hence R is Subfield of E by EC_PF_1:def 1,B;
end;
hence thesis;
end;
registration
let F be Field;
let E be FieldExtension of F;
cluster E-extending for FieldExtension of F;
existence
proof
take E;
E is Subring of E by LIOUVIL2:18;
hence thesis by FIELD_4:def 1;
end;
end;
notation
let F be Field;
let E be FieldExtension of F;
antonym E is F-infinite for E is F-finite;
end;
theorem sp:
for F being Field,
E being FieldExtension of F
for K being E-extending FieldExtension of F
holds VecSp(E,F) is Subspace of VecSp(K,F)
proof
let F be Field, E be FieldExtension of F;
let K be E-extending FieldExtension of F;
set VK = VecSp(K,F), VE = VecSp(E,F);
H1: E is Subring of K by FIELD_4:def 1; then
H2: the carrier of E c= the carrier of K by C0SP1:def 3;
H3: the carrier of VE = the carrier of E &
the carrier of VK = the carrier of K by FIELD_4:def 6;
F is Subring of E by FIELD_4:def 1; then
H4: the carrier of F c= the carrier of E by C0SP1:def 3;
B1: the carrier of VE c= the carrier of VK by H1,H3,C0SP1:def 3;
B2: 0.VE = 0.E by FIELD_4:def 6
.= 0.K by H1,C0SP1:def 3
.= 0.VK by FIELD_4:def 6;
B3: the addF of VE = the addF of E by FIELD_4:def 6
.= (the addF of K)||the carrier of E by H1,C0SP1:def 3
.= (the addF of VK)||the carrier of E by FIELD_4:def 6
.= (the addF of VK)||the carrier of VE by FIELD_4:def 6;
B4: the lmult of VE
= (the multF of E)|[:the carrier of F,the carrier of VE:]
by H3,FIELD_4:def 6
.= ((the multF of K)||the carrier of E) |
[:the carrier of F,the carrier of VE:] by H1,C0SP1:def 3
.= (the multF of K) | [:the carrier of F,the carrier of VE:]
by H4,H3,ZFMISC_1:96,RELAT_1:74
.= ((the multF of K)|[:the carrier of F,the carrier of K:])
| [:the carrier of F, the carrier of VE:]
by H2,H3,ZFMISC_1:96,RELAT_1:74
.= (the lmult of VK) | [:the carrier of F, the carrier of VE:]
by FIELD_4:def 6;
thus thesis by B1,B2,B3,B4,VECTSP_4:def 2;
end;
theorem
for F being Field,
E being FieldExtension of F
for K being E-extending FieldExtension of F
holds K is F-infinite or (E is F-finite & deg(E,F) <= deg(K,F))
proof
let F be Field, E be FieldExtension of F;
let K be E-extending FieldExtension of F;
set VK = VecSp(K,F), VE = VecSp(E,F);
now assume K is F-finite; then
reconsider VK as finite-dimensional VectSp of F by FIELD_4:def 8;
A: deg(K,F) = dim VK by FIELD_4:def 7;
B: VE is Subspace of VK by sp; then
C: dim VE <= dim VK by VECTSP_9:25;
thus E is F-finite by B,FIELD_4:def 8;
thus deg(E,F) <= deg(K,F) by A,C,FIELD_4:def 7;
end;
hence thesis;
end;
theorem divmod:
for F being Field,
p being Polynomial of F
for q being non zero Polynomial of F holds deg(p mod q) < deg q
proof
let F be Field, p be Polynomial of F; let q be non zero Polynomial of F;
q <> 0_.(F); then
consider t being Polynomial of F such that
C: p = (p div q) *' q + t & deg t < deg q by HURWITZ:def 5;
p mod q = ((p div q) *' q + t) - ((p div q) *' q) by C,HURWITZ:def 6
.= t + ((p div q) *' q - ((p div q) *' q)) by POLYNOM3:26
.= t + 0_.(F) by POLYNOM3:29;
hence thesis by C;
end;
lempk:
for F,K being Field st the carrier of F = the carrier of K & 0.F = 0.K
holds the carrier of Polynom-Ring F = the carrier of Polynom-Ring K
proof
let F,K be Field;
assume AS: the carrier of F = the carrier of K & 0.F = 0.K;
A: now let o be object;
assume o in the carrier of Polynom-Ring F;
then reconsider p = o as Polynomial of F by POLYNOM3:def 10;
reconsider p1 = p as sequence of K by AS;
for i be Nat st i >= len p holds p1.i = 0.K by AS,ALGSEQ_1:8;
then p1 is finite-Support by ALGSEQ_1:def 1;
hence o in the carrier of Polynom-Ring K by POLYNOM3:def 10;
end;
now let o be object;
assume o in the carrier of Polynom-Ring K;
then reconsider p = o as Polynomial of K by POLYNOM3:def 10;
reconsider p1 = p as sequence of F by AS;
for i be Nat st i >= len p holds p1.i = 0.F by AS,ALGSEQ_1:8;
then p1 is finite-Support by ALGSEQ_1:def 1;
hence o in the carrier of Polynom-Ring F by POLYNOM3:def 10;
end;
hence thesis by A,TARSKI:2;
end;
begin :: Linear Polynomials
definition
let R be Ring;
let p be Polynomial of R;
attr p is linear means :defl:
deg p = 1;
end;
registration
let R be non degenerated Ring;
cluster linear for Polynomial of R;
existence
proof
take rpoly(1,0.R);
thus thesis by HURWITZ:27;
end;
cluster non linear for Polynomial of R;
existence
proof
take 0_.(R);
thus thesis by HURWITZ:20;
end;
cluster linear for Element of the carrier of Polynom-Ring R;
existence
proof
reconsider o = rpoly(1,1.R) as Element of the carrier of Polynom-Ring R
by POLYNOM3:def 10;
take o;
thus thesis by HURWITZ:27;
end;
cluster non linear for Element of the carrier of Polynom-Ring R;
existence
proof
reconsider o = 0_.(R) as Element of the carrier of Polynom-Ring R
by POLYNOM3:def 10;
take o;
thus thesis by HURWITZ:20;
end;
end;
registration
let R be non degenerated Ring;
cluster zero -> non linear for Polynomial of R;
coherence
proof
let p be Polynomial of R;
assume p is zero; then
p = 0_.(R) by UPROOTS:def 5;
hence thesis by HURWITZ:20;
end;
cluster constant -> non linear for Polynomial of R;
coherence by RATFUNC1:def 2;
end;
registration
let F be Field;
cluster linear -> with_roots for Polynomial of F;
coherence
proof
let p be Polynomial of F;
assume p is linear;
then consider x,z being Element of F such that
A: x <> 0.F & p = x * rpoly(1,z) by HURWITZ:28;
thus p is with_roots by A;
end;
end;
registration
let F be Field;
cluster linear -> irreducible for Element of the carrier of Polynom-Ring F;
coherence by RING_4:44;
end;
registration
let F be Field;
cluster non linear with_roots -> reducible
for Element of the carrier of Polynom-Ring F;
coherence
proof
let p be Element of the carrier of Polynom-Ring F;
assume AS: p is non linear with_roots; then
consider a being Element of F such that
A: a is_a_root_of p by POLYNOM5:def 8;
consider q1 being Polynomial of F such that
B: p = rpoly(1,a) *' q1 by A,HURWITZ:33;
reconsider q = q1 as Element of the carrier of Polynom-Ring F
by POLYNOM3:def 10;
C: q divides p by B,RING_4:1;
per cases;
suppose p = 0_.(F);
hence thesis;
end;
suppose L: p <> 0_.(F);
then M: q1 <> 0_.(F) by B;
then D: deg p = deg rpoly(1,a) + deg q1 by B,HURWITZ:23
.= 1 + deg q1 by HURWITZ:27;
reconsider degp = deg p, degq = deg q as Element of NAT by M,L,FIELD_1:1;
1 + degq >= 1 + 1 by D,AS,NAT_1:23; then
1 <= degq by XREAL_1:6;
hence thesis by C,D,NAT_1:19,RING_4:40;
end;
end;
end;
registration
let R be domRing;
let p be linear Polynomial of R;
let q be non constant Polynomial of R;
cluster p *' q -> non linear;
coherence
proof
reconsider p1 = p, q1 = q as Polynomial of R;
q <> 0_.(R) & p <> 0_.(R);
then B: deg(p1 *' q1) = deg p + deg q by HURWITZ:23;
deg p = 1 by defl;
hence p *' q is non linear by RATFUNC1:def 2,B;
end;
end;
registration
let F be Field;
let p be linear Polynomial of F;
let q be non constant Polynomial of F;
cluster p *' q -> with_roots;
coherence;
end;
begin :: More on Polynom-Ring(F,p)
lemdis:
for F being polynomial_disjoint Field
for p being non constant Element of the carrier of Polynom-Ring F
holds F,Polynom-Ring p are_disjoint
proof
let F be polynomial_disjoint Field,
p be non constant Element of the carrier of Polynom-Ring F;
now assume not F,Polynom-Ring p are_disjoint;
then A: [#]F /\ [#](Polynom-Ring p) <> {} by FIELD_2:def 1;
let a be Element of
(the carrier of F) /\ (the carrier of Polynom-Ring p);
B: a in the carrier of F & a in the carrier of Polynom-Ring p
by A,XBOOLE_0:def 4;
the carrier of Polynom-Ring p =
{q where q is Polynomial of F : deg q < deg p} by RING_4:def 8;
then consider q being Polynomial of F such that
C: a = q & deg q < deg p by B;
a in the carrier of Polynom-Ring F by C,POLYNOM3:def 10;
then a in [#]F /\ [#]Polynom-Ring F by B,XBOOLE_0:def 4;
hence contradiction by FIELD_3:def 3;
end;
hence thesis;
end;
definition
let F be Field,
p be non constant Element of the carrier of Polynom-Ring F;
func canHomP p -> Function of F,Polynom-Ring(p) means :defch:
for a being Element of F holds it.a = a|F;
existence
proof
set R = F, B = Polynom-Ring p;
defpred P[object,object] means
ex a being Element of R st $1 = a & $2 = a|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;
not deg p <= 0 & deg(a|R) <= 0 by RING_4:def 4,RATFUNC1:def 2;
then a|F in {q where q is Polynomial of F : deg q < deg p};
then reconsider y = a|R as Element of B by RING_4:def 8;
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|R by Z;
thus g.x = x|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|R;
take f;
thus thesis by Y;
end;
uniqueness
proof
set R = F, B = Polynom-Ring p;
let g1,g2 be Function of R,B such that
A1: for a being Element of R holds g1.a = a|R and
A2: for a being Element of R holds g2.a = a|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|R by A1 .= g2.x by A2;
end;
hence thesis by A;
end;
end;
registration
let F be Field,
p be non constant Element of the carrier of Polynom-Ring F;
cluster canHomP p -> additive multiplicative unity-preserving
one-to-one;
coherence
proof
set R = F, RX = Polynom-Ring F, f = canHomP p, B = Polynom-Ring p;
hereby
let x,y be Element of R;
B: f.x = x|R & f.y = y|R by defch;
A: [f.x,f.y] in [:the carrier of B,the carrier of B:] by ZFMISC_1:def 2;
reconsider fx = f.x, fy = f.y as Element of the carrier of RX
by B,POLYNOM3:def 10;
thus f.x + f.y
= (the addF of RX)||(the carrier of B).(f.x,f.y) by RING_4:def 8
.= fx + fy by A,FUNCT_1:49
.= (x|R) + (y|R) by B,POLYNOM3:def 10
.= (x + y)|R by RING_4:17
.= f.(x+y) by defch;
end;
hereby
let x,y be Element of R;
B: f.x = x|R & f.y = y|R by defch;
A: [f.x,f.y] in [:the carrier of B,the carrier of B:] by ZFMISC_1:def 2;
reconsider fx = f.x, fy = f.y as Element of the carrier of RX
by B,POLYNOM3:def 10;
reconsider p1 = p as Polynomial of F;
C: deg((x*y)|R) <= 0 & deg p > 0 by RING_4:def 4,RATFUNC1:def 2;
thus f.x * f.y
= (poly_mult_mod p)||(the carrier of B).(f.x,f.y) by RING_4:def 8
.= (poly_mult_mod p).(fx,fy) by A,FUNCT_1:49
.= ((x|R) *' (y|R)) mod p by B,RING_4:def 7
.= ((x*y)|R) mod p by RING_4:18
.= (x * y)|R by C,RING_4:2
.= f.(x*y) by defch;
end;
thus f.1_R = (1.R)|R by defch
.= 1_.(R) by RING_4:14
.= 1_(Polynom-Ring p) by RING_4:def 8;
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|R = f.x2 by AS,defch .= b|R by defch;
hence x1 = x2 by RING_4:19;
end;
hence f is one-to-one by FUNCT_2:19;
end;
end;
registration
let F be Field;
let p be non constant Element of the carrier of Polynom-Ring F;
cluster Polynom-Ring p -> F-homomorphic F-monomorphic;
coherence
proof
canHomP p is monomorphism;
hence thesis by RING_3:def 3;
end;
end;
registration
let F be polynomial_disjoint Field;
let p be irreducible Element of the carrier of Polynom-Ring F;
cluster embField(canHomP p) ->
add-associative right_complementable associative distributive
almost_left_invertible;
coherence by lemdis,FIELD_2:12;
end;
registration
let F be polynomial_disjoint Field;
let p be irreducible Element of the carrier of Polynom-Ring F;
cluster embField(canHomP p) -> F-extending;
coherence
proof
F is Subfield of embField(canHomP p) by FIELD_2:17; then
F is Subring of embField(canHomP p) by pr1;
hence thesis by FIELD_4:def 1;
end;
end;
definition
let F be polynomial_disjoint Field;
let p be irreducible Element of the carrier of Polynom-Ring F;
func KrRootP p -> Element of embField(canHomP p) equals
((emb_iso (canHomP p))" * (KroneckerIso p)").(KrRoot p);
coherence
proof
set K = KroneckerField(F,p);
E9: emb_iso (canHomP p) is onto by lemdis,FIELD_2:15;
rng(KroneckerIso p) = the carrier of K by FUNCT_2:def 3; then
KrRoot p in rng(KroneckerIso p);
then E3: KrRoot p in dom((KroneckerIso p)") by FUNCT_1:32; then
E6: ((KroneckerIso p)").(KrRoot p) in rng((KroneckerIso p)") by FUNCT_1:def 3;
E10: ((KroneckerIso p)").(KrRoot p) in dom(KroneckerIso p) by E6,FUNCT_1:33;
dom((emb_iso (canHomP p))") = the carrier of Polynom-Ring p by E9,FUNCT_1:33
.= dom(KroneckerIso p) by FUNCT_2:def 1; then
((emb_iso (canHomP p))").(((KroneckerIso p)").(KrRoot p)) in
rng((emb_iso (canHomP p))") by E10,FUNCT_1:3;
then ((emb_iso (canHomP p))").(((KroneckerIso p)").(KrRoot p)) in
dom(emb_iso (canHomP p)) by FUNCT_1:33;
hence thesis by E3,FUNCT_1:13;
end;
end;
theorem
for F being polynomial_disjoint Field
for p being irreducible Element of the carrier of Polynom-Ring F
holds Ext_eval(p,KrRootP p) = 0.F
proof
let F be polynomial_disjoint Field;
let p be irreducible Element of the carrier of Polynom-Ring F;
set K = KroneckerField(F,p), u = KrRoot p, E = embField(canHomP p);
set h = (KroneckerIso p) * (emb_iso (canHomP p));
reconsider h as Function of E,K by FUNCT_2:13;
emb_iso (canHomP p) is onto by lemdis,FIELD_2:15; then
B: h is one-to-one onto by FUNCT_2:27;
emb_iso (canHomP p) is additive multiplicative by lemdis,FIELD_2:13,FIELD_2:14;
then C: h is linear by RINGCAT1:1; then
reconsider P = K as E-isomorphic Field by B,RING_3:def 4;
reconsider iso = h as Isomorphism of E,P by B,C;
reconsider E as P-isomorphic Field by RING_3:74;
reconsider E as P-homomorphic Field;
reconsider isoi = iso" as Homomorphism of P,E by RING_3:73;
reconsider t = emb(p,p) as Element of the carrier of Polynom-Ring P;
reconsider ui = u as Element of P;
u is_a_root_of emb(p,p) by FIELD_1:42; then
X: eval((PolyHom isoi).t,isoi.ui) = 0.E by FIELD_1:34,POLYNOM5:def 7;
Y: (PolyHom isoi).t = p
proof
set g = (PolyHom isoi).t;
A: for a being Element of F holds isoi.((emb p).a) = a
proof
let a be Element of F;
reconsider b = a|F as Element of the carrier of Polynom-Ring F
by POLYNOM3:def 10;
A12: the carrier of Polynom-Ring p =
{q where q is Polynomial of F : deg q < deg p} by RING_4:def 8;
deg(a|F) <= 0 & deg p > 0 by RATFUNC1:def 2,RING_4:def 4; then
A3: a|F in the carrier of Polynom-Ring p by A12; then
reconsider b1 = a|F as Element of Polynom-Ring p;
reconsider v = Class(EqRel(Polynom-Ring F,{p}-Ideal),b)
as Element of KroneckerField(F,p) by RING_1:12;
A5: b1 in dom(KroneckerIso p) by A3,FUNCT_2:def 1;
A7: dom((KroneckerIso p)")
= rng(KroneckerIso p) by FUNCT_1:33
.= the carrier of K by FUNCT_2:def 3;
(KroneckerIso p).b1 = v by FIELD_4:def 9; then
A6: ((KroneckerIso p)").v = b1 by A5,FUNCT_1:34;
F is Subfield of embField(canHomP p) by FIELD_2:17;
then the carrier of F c= the carrier of embField(canHomP p)
by EC_PF_1:def 1; then
reconsider aa = a as Element of embField(canHomP p);
A9: dom(emb_iso (canHomP p)) = the carrier of E by FUNCT_2:def 1;
aa in F; then
(emb_iso (canHomP p)).aa = (canHomP p).aa by FIELD_2:def 8
.= a|F by defch; then
A2: ((emb_iso (canHomP p))").b1 = aa by A9,FUNCT_1:34;
thus isoi.((emb p).a)
= isoi.v by FIELD_1:39
.= ((emb_iso (canHomP p))" * (KroneckerIso p)").v by FUNCT_1:44
.= a by A2,A6,A7,FUNCT_1:13;
end;
now let x be object;
assume x in NAT;
then reconsider i = x as Element of NAT;
g.i = isoi.(emb(p,p).i) by FIELD_1:def 2
.= isoi.(Class(EqRel(Polynom-Ring F,{p}-Ideal),(p.i)|F))
by FIELD_1:40
.= isoi.((emb p).(p.i)) by FIELD_1:39;
hence g.x = p.x by A;
end;
hence thesis;
end;
F0: dom(KroneckerIso p) = the carrier of Polynom-Ring p by FUNCT_2:def 1;
E5: rng(KroneckerIso p) = the carrier of K by FUNCT_2:def 3; then
KrRoot p in rng(KroneckerIso p);
then E3: KrRoot p in dom((KroneckerIso p)") by FUNCT_1:32; then
E6: ((KroneckerIso p)").(KrRoot p) in rng((KroneckerIso p)") by FUNCT_1:def 3;
E9: emb_iso (canHomP p) is onto by lemdis,FIELD_2:15;
then E4: ((KroneckerIso p)").(KrRoot p) in rng(emb_iso (canHomP p))
by E6,F0,FUNCT_1:33;
E10: ((KroneckerIso p)").(KrRoot p) in dom(KroneckerIso p) by E6,FUNCT_1:33;
dom((emb_iso (canHomP p))") = the carrier of Polynom-Ring p by E9,FUNCT_1:33
.= dom(KroneckerIso p) by FUNCT_2:def 1; then
((emb_iso (canHomP p))").(((KroneckerIso p)").(KrRoot p)) in
rng((emb_iso (canHomP p))") by E10,FUNCT_1:3;
then ((emb_iso (canHomP p))").(((KroneckerIso p)").(KrRoot p)) in
dom(emb_iso (canHomP p)) by FUNCT_1:33;
then E2: (((emb_iso (canHomP p))" * (KroneckerIso p)").(KrRoot p)) in
dom(emb_iso (canHomP p)) by E3,FUNCT_1:13;
iso.(KrRootP p)
= (KroneckerIso p).((emb_iso (canHomP p)).
(((emb_iso (canHomP p))" * (KroneckerIso p)").(KrRoot p)))
by E2,FUNCT_1:13
.= (KroneckerIso p).((emb_iso (canHomP p)).
(((emb_iso (canHomP p))").(((KroneckerIso p)").(KrRoot p))))
by E3,FUNCT_1:13
.= (KroneckerIso p).(((KroneckerIso p)").(KrRoot p)) by E4,FUNCT_1:35
.= KrRoot p by E5,FUNCT_1:35;
then isoi.ui = KrRootP p by FUNCT_2:26;
hence Ext_eval(p,KrRootP p) = 0.E by X,Y,FIELD_4:26
.= 0.F by FIELD_2:def 7;
end;
begin :: On Embedding F into F[X]/<p> and Polynom-Ring(F,p)
theorem polyd:
for F being Field
for p being linear Element of the carrier of Polynom-Ring F
holds (Polynom-Ring p), F are_isomorphic &
the carrier of embField(canHomP p) = the carrier of F
proof
let F be Field; let p be linear Element of the carrier of Polynom-Ring F;
set FP = Polynom-Ring p, f = canHomP p;
H: the carrier of FP = {q where q is Polynomial of F : deg q < deg p}
by RING_4:def 8;
A: now let o be object;
assume o in the carrier of FP;
then consider q being Polynomial of F such that
B: q = o & deg q < deg p by H;
reconsider q as Element of the carrier of Polynom-Ring F by POLYNOM3:def 10;
deg q < 1 by B,defl;
then deg q + 1 <= 1 by INT_1:7;
then (deg q + 1) - 1 <= 1 - 1 by XREAL_1:9;
then consider a being Element of F such that
C: q = a|F by RING_4:20,RING_4:def 4;
D: f.a = o by B,C,defch;
dom f = the carrier of F by FUNCT_2:def 1;
hence o in rng f by D,FUNCT_1:def 3;
end;
X: now let o be object;
assume B: o in rng f;
rng f c= the carrier of FP by RELAT_1:def 19;
hence o in the carrier of FP by B;
end;
then B: rng f = the carrier of FP by A,TARSKI:2;
f is monomorphism onto by X,A,TARSKI:2;
then F,(Polynom-Ring p) are_isomorphic;
hence (Polynom-Ring p), F are_isomorphic;
X: [#] FP = the carrier of FP & [#] F = the carrier of F;
thus the carrier of embField(canHomP p)
= carr f by FIELD_2:def 7
.= ((the carrier of FP) \ (rng f)) \/ (the carrier of F) by X,FIELD_2:def 2
.= {} \/ (the carrier of F) by B,XBOOLE_1:37
.= the carrier of F;
end;
theorem
for F being strict Field
for p being linear Element of the carrier of Polynom-Ring F
holds embField(canHomP p) = F
proof
let F be strict Field;
let p be linear Element of the carrier of Polynom-Ring F;
set FP = embField(canHomP p), f = canHomP p;
X: [#] F = the carrier of F &
[#] (Polynom-Ring p) = the carrier of Polynom-Ring p;
H: the carrier of F = the carrier of embField f by polyd;
A: 1.FP = 1.F & 0.FP = 0.F by FIELD_2:def 7;
B: dom(the addF of FP)
= [:the carrier of FP, the carrier of FP:] by FUNCT_2:def 1
.= dom(the addF of F) by H,FUNCT_2:def 1;
now let x be Element of dom(the addF of F);
consider o being Element of [:the carrier of F, the carrier of F:]
such that B1: x = o;
consider a,b being object such that
B2: a in the carrier of F & b in the carrier of F & o = [a,b]
by ZFMISC_1:def 2;
a in ((the carrier of Polynom-Ring p) \ (rng f)) \/ (the carrier of F) &
b in ((the carrier of Polynom-Ring p) \ (rng f)) \/ (the carrier of F)
by B2,XBOOLE_0:def 3;
then reconsider a,b as Element of (carr f) by X,FIELD_2:def 2;
thus (the addF of FP).x
= (addemb f).(a,b) by B1,B2,FIELD_2:def 7
.= addemb(f,a,b) by FIELD_2:def 4
.= (the addF of F).(a,b) by B2,X,FIELD_2:def 3
.= (the addF of F).x by B1,B2;
end;
then C: the addF of FP = the addF of F by B;
B: dom(the multF of FP)
= [:the carrier of FP, the carrier of FP:] by FUNCT_2:def 1
.= dom(the multF of F) by H,FUNCT_2:def 1;
now let x be Element of dom(the multF of F);
consider o being Element of [:the carrier of F, the carrier of F:]
such that B1: x = o;
consider a,b being object such that
B2: a in the carrier of F & b in the carrier of F & o = [a,b]
by ZFMISC_1:def 2;
a in ((the carrier of Polynom-Ring p) \ (rng f)) \/ (the carrier of F) &
b in ((the carrier of Polynom-Ring p) \ (rng f)) \/ (the carrier of F)
by B2,XBOOLE_0:def 3;
then reconsider a,b as Element of (carr f) by X,FIELD_2:def 2;
thus (the multF of FP).x
= (multemb f).(a,b) by B1,B2,FIELD_2:def 7
.= multemb(f,a,b) by FIELD_2:def 6
.= (the multF of F).(a,b) by B2,X,FIELD_2:def 5
.= (the multF of F).x by B1,B2;
end;
then the multF of FP = the multF of F by B;
hence thesis by A,C,polyd;
end;
theorem polyd1:
for F being Field
for p being linear Element of the carrier of Polynom-Ring F
holds (Polynom-Ring F)/({p}-Ideal), F are_isomorphic &
the carrier of embField(emb p) = the carrier of F
proof
let F be Field; let p be linear Element of the carrier of Polynom-Ring F;
set FP = (Polynom-Ring F)/({p}-Ideal), I = {p}-Ideal, f = emb p,
FX = Polynom-Ring F;
A: FP,(Polynom-Ring p) are_isomorphic by RING_4:48;
(Polynom-Ring p), F are_isomorphic by polyd;
hence (Polynom-Ring F)/({p}-Ideal), F are_isomorphic by A,RING_3:44;
B: now let q be Element of the carrier of FX;
B1: q = (q div p) *' p + (q mod p) by RING_4:4;
reconsider r = q mod p, d = q div p as
Element of the carrier of FX by POLYNOM3:def 10;
deg r < deg p by divmod; then
deg r < 1 by defl; then
deg r + 1 <= 1 by INT_1:7; then
(deg r + 1) - 1 <= 1 - 1 by XREAL_1:9; then
reconsider r as constant Element of the carrier of FX by RING_4:def 4;
(q div p) *' p = d * p by POLYNOM3:def 10; then
q = d * p + r by B1,POLYNOM3:def 10; then
B2: q - r = d * p + (r - r) by RLVECT_1:28
.= d * p + 0.FX by RLVECT_1:15;
{p}-Ideal = the set of all p*c where c is Element of FX by IDEAL_1:64;
then p * d in I;
then d * p in I by GROUP_1:def 12;
then Class(EqRel(FX,I),q) = Class(EqRel(FX,I),r) by B2,RING_1:6;
hence ex r being constant Element of the carrier of FX
st Class(EqRel(FX,I),q) = Class(EqRel(FX,I),r);
end;
E: now let o be object;
assume o in the carrier of FP;
then consider q being Element of the carrier of FX such that
E1: o = Class(EqRel(FX,I),q) by RING_1:11;
consider r being constant Element of the carrier of FX such that
E2: Class(EqRel(FX,I),q) = Class(EqRel(FX,I),r) by B;
consider a being Element of F such that
E3: a|F = r by RING_4:20;
E4: f.a = o by E1,E2,E3,FIELD_1:39;
dom f = the carrier of F by FUNCT_2:def 1;
hence o in rng f by E4,FUNCT_1:def 3;
end;
now let o be object;
assume B: o in rng f;
rng f c= the carrier of FP by RELAT_1:def 19;
hence o in the carrier of FP by B;
end;
then C: rng f = the carrier of FP by E,TARSKI:2;
X: [#] F = the carrier of F & [#] FP = the carrier of FP;
thus the carrier of embField(emb p)
= carr f by FIELD_2:def 7
.= ((the carrier of FP)\(rng f))\/(the carrier of F) by X,FIELD_2:def 2
.= {} \/ (the carrier of F) by C,XBOOLE_1:37
.= the carrier of F;
end;
theorem
for F being strict Field
for p being linear Element of the carrier of Polynom-Ring F
holds embField(emb p) = F
proof
let F be strict Field;
let p be linear Element of the carrier of Polynom-Ring F;
set FP = embField(emb p), f = emb p, K = (Polynom-Ring F)/({p}-Ideal);
X: [#] K = the carrier of K & [#] F = the carrier of F;
H: the carrier of F = the carrier of embField f by polyd1;
A: 1.FP = 1.F & 0.FP = 0.F by FIELD_2:def 7;
B: dom(the addF of FP)
= [:the carrier of FP, the carrier of FP:] by FUNCT_2:def 1
.= dom(the addF of F) by H,FUNCT_2:def 1;
now let x be Element of dom(the addF of F);
consider o being Element of [:the carrier of F, the carrier of F:]
such that B1: x = o;
consider a,b being object such that
B2: a in the carrier of F & b in the carrier of F & o = [a,b]
by ZFMISC_1:def 2;
a in ((the carrier of K) \ (rng f)) \/ (the carrier of F) &
b in ((the carrier of K) \ (rng f)) \/ (the carrier of F)
by B2,XBOOLE_0:def 3;
then reconsider a,b as Element of (carr f) by X,FIELD_2:def 2;
thus (the addF of FP).x
= (addemb f).(a,b) by B1,B2,FIELD_2:def 7
.= addemb(f,a,b) by FIELD_2:def 4
.= (the addF of F).(a,b) by B2,X,FIELD_2:def 3
.= (the addF of F).x by B1,B2;
end;
then C: the addF of FP = the addF of F by B;
B: dom(the multF of FP)
= [:the carrier of FP, the carrier of FP:] by FUNCT_2:def 1
.= dom(the multF of F) by H,FUNCT_2:def 1;
now let x be Element of dom(the multF of F);
consider o being Element of [:the carrier of F, the carrier of F:]
such that B1: x = o;
consider a,b being object such that
B2: a in the carrier of F & b in the carrier of F & o = [a,b]
by ZFMISC_1:def 2;
a in ((the carrier of K) \ (rng f)) \/ (the carrier of F) &
b in ((the carrier of K) \ (rng f)) \/ (the carrier of F)
by B2,XBOOLE_0:def 3;
then reconsider a,b as Element of (carr f) by X,FIELD_2:def 2;
thus (the multF of FP).x
= (multemb f).(a,b) by B1,B2,FIELD_2:def 7
.= multemb(f,a,b) by FIELD_2:def 6
.= (the multF of F).(a,b) by B2,X,FIELD_2:def 5
.= (the multF of F).x by B1,B2;
end;
then the multF of FP = the multF of F by B;
hence thesis by A,C,polyd1;
end;
theorem
for F being polynomial_disjoint Field,
p being irreducible Element of the carrier of Polynom-Ring F
holds embField(canHomP p) is polynomial_disjoint iff p is linear
proof
let F be polynomial_disjoint Field,
p be irreducible Element of the carrier of Polynom-Ring F;
set FP = Polynom-Ring p, K = embField(canHomP p), X = <%0.F,1.F%>;
X: [#] F = the carrier of F &
[#] (Polynom-Ring p) = the carrier of Polynom-Ring p;
A: now assume AS: deg p > 1;
H: the carrier of FP = {q where q is Polynomial of F : deg q < deg p}
by RING_4:def 8;
len X = 2 by POLYNOM5:40; then
D: deg X = 2 - 1 by HURWITZ:def 2; then
C: X in the carrier of FP by H,AS;
now assume X in rng(canHomP p);
then consider o being object such that
B1: o in dom(canHomP p) & (canHomP p).o = X by FUNCT_1:def 3;
reconsider a = o as Element of F by B1;
X = a|F by B1,defch;
hence contradiction by D,RATFUNC1:def 2;
end;
then X in (the carrier of FP) \ rng(canHomP p) by C,XBOOLE_0:def 5;
then X in ((the carrier of FP) \ rng(canHomP p)) \/ (the carrier of F)
by XBOOLE_0:def 3;
then X in carr(canHomP p) by X,FIELD_2:def 2; then
A: X in the carrier of K by FIELD_2:def 7;
now let n be Element of NAT;
per cases by NAT_1:23;
suppose B: n = 0;
hence <%0.F,1.F%>.n = 0.F by POLYNOM5:38
.= 0.K by FIELD_2:def 7
.= <%0.K,1.K%>.n by B,POLYNOM5:38;
end;
suppose B: n = 1;
hence <%0.F,1.F%>.n = 1.F by POLYNOM5:38
.= 1.K by FIELD_2:def 7
.= <%0.K,1.K%>.n by B,POLYNOM5:38;
end;
suppose B: n >= 2;
hence <%0.F,1.F%>.n = 0.F by POLYNOM5:38
.= 0.K by FIELD_2:def 7
.= <%0.K,1.K%>.n by B,POLYNOM5:38;
end;
end;
then <%0.F,1.F%> = <%0.K,1.K%>;
then X in the carrier of Polynom-Ring K by POLYNOM3:def 10;
then X in [#]K /\ [#]Polynom-Ring K by A,XBOOLE_0:def 4;
hence K is non polynomial_disjoint by FIELD_3:def 3;
end;
H: 0.K = 0.F by FIELD_2:def 7;
B: now assume C: p is linear;
then D: [#]Polynom-Ring K = [#]Polynom-Ring F by H,lempk,polyd;
[#]K = [#]F by C,polyd;
then [#]K /\ [#]Polynom-Ring K = {} by D,FIELD_3:def 3;
hence K is polynomial_disjoint by FIELD_3:def 3;
end;
now assume C: K is polynomial_disjoint;
deg p >= 0 + 1 by INT_1:7,RING_4:def 4;
hence p is linear by A,C,XXREAL_0:1;
end;
hence thesis by B;
end;
theorem
for F being Field,
p being irreducible Element of the carrier of Polynom-Ring F
for E being polynomial_disjoint Field
st E = embField(emb p) holds F is polynomial_disjoint
proof
let F be Field, p be irreducible Element of the carrier of Polynom-Ring F;
let E be polynomial_disjoint Field;
assume AS1: E = embField(emb p);
assume AS2: F is non polynomial_disjoint;
H: F is Subfield of E by AS1,FIELD_2:17; then
reconsider K = E as FieldExtension of F by FIELD_4:7;
A: the carrier of F c= the carrier of K by H, EC_PF_1:def 1;
set o = the Element of (the carrier of F) /\ (the carrier of Polynom-Ring F);
[#]F /\ [#]Polynom-Ring F <> {} by AS2,FIELD_3:def 3; then
B: o in (the carrier of F) & o in (the carrier of Polynom-Ring F)
by XBOOLE_0:def 4;
the carrier of Polynom-Ring F c= the carrier of Polynom-Ring K by FIELD_4:10;
then o in [#]K /\ [#]Polynom-Ring K by A,B,XBOOLE_0:def 4;
hence thesis by FIELD_3:def 3;
end;
Disj1:
for n being non trivial Nat
for p being Element of the carrier of Polynom-Ring(Z/n)
holds (the carrier of Z/n) /\
(the carrier of (Polynom-Ring(Z/n))/({p}-Ideal)) = {}
proof
let n be non trivial Nat;
let p be Element of the carrier of Polynom-Ring(Z/n);
set F = Z/n;
set FX = Polynom-Ring F, I = {p}-Ideal;
set K = (Polynom-Ring F)/({p}-Ideal);
set x = the Element of (the carrier of F) /\ (the carrier of K);
now assume AS: (the carrier of F) /\ the carrier of K <> {};
reconsider x as Element of F by AS,XBOOLE_0:def 4;
reconsider q = x as Element of K by AS,XBOOLE_0:def 4;
consider a being Element of FX such that
A1: q = Class(EqRel(FX,I),a) by RING_1:11;
reconsider pa = a as Polynomial of F by POLYNOM3:def 10;
a - a = 0.FX by RLVECT_1:15; then
A2: a in q by A1,RING_1:5,IDEAL_1:3;
F = doubleLoopStr(#Segm(n),addint(n),multint(n),
In (1,Segm(n)),In (0,Segm(n))#) by INT_3:def 12; then
x in Segm n; then
reconsider k = x as Element of omega;
k = { m where m is Nat : m < k } by AXIOMS:4; then
consider m being Nat such that B1: a = m & m < k by A2;
dom pa = NAT by FUNCT_2:def 1;
hence contradiction by B1;
end;
hence thesis;
end;
Disj2:
for p being Element of the carrier of Polynom-Ring F_Rat
holds (the carrier of F_Rat) /\
(the carrier of (Polynom-Ring F_Rat)/({p}-Ideal)) = {}
proof
let p be Element of the carrier of Polynom-Ring F_Rat;
set F = F_Rat;
set FX = Polynom-Ring F, I = {p}-Ideal;
set K = (Polynom-Ring F)/({p}-Ideal);
set x = the Element of (the carrier of F) /\ (the carrier of K);
now assume AS: (the carrier of F) /\ the carrier of K <> {};
reconsider x as Element of F by AS,XBOOLE_0:def 4;
reconsider q = x as Element of K by AS,XBOOLE_0:def 4;
consider a being Element of FX such that
A1: q = Class(EqRel(FX,I),a) by RING_1:11;
reconsider pa = a as Polynomial of F by POLYNOM3:def 10;
a - a = 0.FX by RLVECT_1:15; then
A2: a in q by A1,RING_1:5,IDEAL_1:3;
XZ: x in RAT+ \/ [:{0},RAT+:] \ {[0,0]} by NUMBERS:def 3,RAT_1:def 2;
XX: not x in RAT+
proof
assume x in RAT+; then
per cases by XBOOLE_0:def 3,ARYTM_3:def 7;
suppose x in omega;
then reconsider n = x as Element of omega;
n = { m where m is Nat : m < n } by AXIOMS:4; then
consider m being Nat such that B1: a = m & m < n by A2;
dom pa = NAT by FUNCT_2:def 1;
hence contradiction by B1;
end;
suppose x in {[i,j] where i,j is Element of omega
: i,j are_coprime & j <> {}}
\ the set of all [k,1] where k is Element of omega; then
x in {[i,j] where i,j is Element of omega
: i,j are_coprime & j <> {}};
then consider i,j being Element of omega such that
A4: x = [i,j] & i,j are_coprime & j <> {};
A5: dom pa = NAT by FUNCT_2:def 1;
pa in {{i},{i,j}} by A2,A4,TARSKI:def 5; then
per cases by TARSKI:def 2;
suppose pa = {i};
hence contradiction by A5;
end;
suppose pa = {i,j}; then
per cases by A5;
suppose [i,pa.i] = i;
hence contradiction;
end;
suppose [i,pa.i] = j;
hence contradiction;
end;
end;
end;
end;
not x in [:{0},RAT+:]
proof
assume x in [:{0},RAT+:]; then
consider y,z being object such that
A4: y in {0} & z in RAT+ & x = [y,z] by ZFMISC_1:def 2;
reconsider y as Element of NAT by A4,TARSKI:def 1;
A5: dom pa = NAT by FUNCT_2:def 1;
pa in {{y},{y,z}} by A2,A4,TARSKI:def 5; then
per cases by TARSKI:def 2;
suppose pa = {y};
hence contradiction by A5;
end;
suppose pa = {y,z}; then
per cases by A5;
suppose [0,pa.0] = y;
hence contradiction;
end;
suppose A7: [0,pa.0] = z;
per cases by A4,ARYTM_3:def 7,XBOOLE_0:def 3;
suppose A9: z in {[i,j] where i,j is Element of omega
: i,j are_coprime & j <> {}}
\ the set of all [k,1] where k is Element of omega; then
z in {[i,j] where i,j is Element of omega
: i,j are_coprime & j <> {}};
then consider i,j being Element of omega such that
A8: z = [i,j] & i,j are_coprime & j <> {};
i = 0 by A7,A8,XTUPLE_0:1;
then j = 1 by A8,ARYTM_3:3;
then z in the set of all [k,1] where k is Element of omega by A8;
hence contradiction by A9,XBOOLE_0:def 5;
end;
suppose z in omega;
hence contradiction by A7;
end;
end;
end;
end;
hence contradiction by XZ,XX,XBOOLE_0:def 3;
end;
hence thesis;
end;
registration
let n be Prime;
let p be irreducible Element of the carrier of Polynom-Ring(Z/n);
cluster embField(emb p) ->
add-associative right_complementable associative distributive
almost_left_invertible;
coherence
proof
set F = Z/n, KR = KroneckerField(F,p);
X: [#] F = the carrier of F & [#] KR = the carrier of KR;
(the carrier of F) /\ (the carrier of KR) = {} by Disj1;
hence thesis by X,FIELD_2:12,FIELD_2:def 1;
end;
end;
registration
let p be irreducible Element of the carrier of Polynom-Ring F_Rat;
cluster embField(emb p) ->
add-associative right_complementable associative distributive
almost_left_invertible;
coherence
proof
set F = F_Rat, KR = KroneckerField(F,p);
X: [#] F = the carrier of F & [#] KR = the carrier of KR;
(the carrier of F) /\ (the carrier of KroneckerField(F,p)) = {} by Disj2;
hence thesis by X,FIELD_2:12,FIELD_2:def 1;
end;
end;
theorem
for n being Prime,
p being non constant Element of the carrier of Polynom-Ring(Z/n)
holds Z/n, (Polynom-Ring Z/n)/({p}-Ideal) are_disjoint
proof
let n be Prime,
p be non constant Element of the carrier of Polynom-Ring Z/n;
set F = Z/n, KR = (Polynom-Ring Z/n)/({p}-Ideal);
X: [#] F = the carrier of F & [#] KR = the carrier of KR;
(the carrier of Z/n) /\
(the carrier of (Polynom-Ring (Z/n))/({p}-Ideal)) = {} by Disj1;
hence thesis by X,FIELD_2:def 1;
end;
theorem
for p being non constant Element of the carrier of Polynom-Ring F_Rat
holds F_Rat, (Polynom-Ring F_Rat)/({p}-Ideal) are_disjoint
proof
let p be non constant Element of the carrier of Polynom-Ring F_Rat;
set F = F_Rat, KR = (Polynom-Ring F_Rat)/({p}-Ideal);
X: [#] F = the carrier of F & [#] KR = the carrier of KR;
(the carrier of F_Rat) /\
(the carrier of (Polynom-Ring F_Rat)/({p}-Ideal)) = {} by Disj2;
hence thesis by X,FIELD_2:def 1;
end;
registration
let n be Prime;
let p be irreducible Element of the carrier of Polynom-Ring(Z/n);
cluster embField(emb p) -> polynomial_disjoint;
coherence
proof
set F = embField(emb p), FX = Polynom-Ring F, f = emb p,
Kr = KroneckerField(Z/n,p);
set o = the Element of (the carrier of F) /\ the carrier of FX;
X: [#] (Z/n) = the carrier of (Z/n) & [#] Kr = the carrier of Kr;
H: the carrier of F
= carr f by FIELD_2:def 7
.= ((the carrier of Kr)\(rng f))\/(the carrier of (Z/n)) by X,FIELD_2:def 2;
now assume F is non polynomial_disjoint;
then A1: [#]F /\ [#]FX <> {} by FIELD_3:def 3;
then A: o in the carrier of F & o in the carrier of FX by XBOOLE_0:def 4;
reconsider q = o as Element of the carrier of FX by A1,XBOOLE_0:def 4;
Z/n = doubleLoopStr(#Segm(n),addint(n),multint(n),
In (1,Segm(n)),In (0,Segm(n))#) by INT_3:def 12; then
not q in the carrier of (Z/n) by FIELD_3:24; then
o in (the carrier of Kr) \ (rng f) by H,A,XBOOLE_0:def 3; then
reconsider o as Element of (Polynom-Ring Z/n)/({p}-Ideal);
consider a being Element of Polynom-Ring(Z/n) such that
B: o = Class(EqRel(Polynom-Ring(Z/n),{p}-Ideal),a) by RING_1:11;
reconsider q as Polynomial of F;
a - a = 0.(Polynom-Ring(Z/n)) by RLVECT_1:15; then
D0: a in q by B,RING_1:5,IDEAL_1:3; then
consider i,z being object such that
D1: i in NAT & z in the carrier of F & a = [i,z] by ZFMISC_1:def 2;
D2: z = q.i by D0,D1,FUNCT_1:1;
reconsider i as Element of NAT by D1;
reconsider a as Polynomial of (Z/n) by POLYNOM3:def 10;
dom a = NAT by FUNCT_2:def 1; then
[1,a.1] in a & [2,a.2] in a by FUNCT_1:1; then
E: [1,a.1] in {{i},{i,q.i}} & [2,a.2] in {{i},{i,q.i}}
by D1,D2,TARSKI:def 5;
per cases by E,TARSKI:def 2;
suppose [1,a.1] = {i};
then E1: {i} = {{1},{1,a.1}} by TARSKI:def 5;
{1} in {{1},{1,a.1}} & {1,a.1} in {{1},{1,a.1}} by TARSKI:def 2;
hence contradiction by E1;
end;
suppose [1,a.1] = {i,q.i}; then
E1: {i,q.i} = {{1},{1,a.1}} by TARSKI:def 5;
i in {i,q.i} by TARSKI:def 2; then
F0: i = {1,a.1} by E1,TARSKI:def 2;
per cases;
suppose 1 = a.1; then
F3: {2} = {1} by F0,ENUMSET1:29;
2 in {2} by TARSKI:def 1;
hence contradiction by F3,TARSKI:def 1;
end;
suppose 1 <> a.1; then
G1: a.1 = 0 by F0,FIELD_3:2;
per cases by E,TARSKI:def 2;
suppose [2,a.2] = {i};
then F1: {{1,a.1}} = {{2},{2,a.2}} by F0,TARSKI:def 5;
{2} in {{2},{2,a.2}} & {2,a.2} in {{2},{2,a.2}} by TARSKI:def 2;
hence contradiction by G1,F1,CARD_1:50;
end;
suppose [2,a.2] = {i,q.i};
then F1: {2,q.i} = {{2},{2,a.2}} by F0,G1,TARSKI:def 5,CARD_1:50;
2 in {2,q.i} by TARSKI:def 2; then
per cases by F1,TARSKI:def 2;
suppose 2 = {2};
hence contradiction;
end;
suppose F2: 2 = {2,a.2};
2 in {2,a.2} by TARSKI:def 2;
hence contradiction by F2;
end;
end;
end;
end;
end;
hence thesis;
end;
end;
registration
let p be irreducible Element of the carrier of Polynom-Ring F_Rat;
cluster embField(emb p) -> polynomial_disjoint;
coherence
proof
set F = embField(emb p), FX = Polynom-Ring F, f = emb p,
Kr = KroneckerField(F_Rat,p);
set o = the Element of (the carrier of F) /\ the carrier of FX;
X: [#] F_Rat = the carrier of F_Rat & [#] Kr = the carrier of Kr;
H: the carrier of F = carr f by FIELD_2:def 7
.= ((the carrier of Kr)\(rng f))\/(the carrier of F_Rat) by X,FIELD_2:def 2;
now assume F is non polynomial_disjoint;
then A1: [#]F /\ [#]FX <> {} by FIELD_3:def 3;
then A: o in the carrier of F & o in the carrier of FX by XBOOLE_0:def 4;
reconsider q = o as Element of the carrier of FX by A1,XBOOLE_0:def 4;
not q in the carrier of F_Rat by FIELD_3:25; then
o in (the carrier of Kr) \ (rng f) by H,A,XBOOLE_0:def 3; then
reconsider o as Element of (Polynom-Ring F_Rat)/({p}-Ideal);
consider a being Element of Polynom-Ring F_Rat such that
B: o = Class(EqRel(Polynom-Ring F_Rat,{p}-Ideal),a) by RING_1:11;
reconsider q as Polynomial of F;
a - a = 0.(Polynom-Ring F_Rat) by RLVECT_1:15; then
D0: a in q by B,RING_1:5,IDEAL_1:3; then
consider i,z being object such that
D1: i in NAT & z in the carrier of F & a = [i,z] by ZFMISC_1:def 2;
D2: z = q.i by D0,D1,FUNCT_1:1;
reconsider i as Element of NAT by D1;
reconsider a as Polynomial of F_Rat by POLYNOM3:def 10;
dom a = NAT by FUNCT_2:def 1; then
[1,a.1] in a & [2,a.2] in a by FUNCT_1:1; then
E: [1,a.1] in {{i},{i,q.i}} & [2,a.2] in {{i},{i,q.i}}
by D1,D2,TARSKI:def 5;
per cases by E,TARSKI:def 2;
suppose [1,a.1] = {i};
then E1: {i} = {{1},{1,a.1}} by TARSKI:def 5;
{1} in {{1},{1,a.1}} & {1,a.1} in {{1},{1,a.1}} by TARSKI:def 2;
hence contradiction by E1;
end;
suppose [1,a.1] = {i,q.i}; then
E1: {i,q.i} = {{1},{1,a.1}} by TARSKI:def 5;
i in {i,q.i} by TARSKI:def 2; then
F0: i = {1,a.1} by E1,TARSKI:def 2;
per cases;
suppose 1 = a.1; then
F3: {2} = {1} by F0,ENUMSET1:29;
2 in {2} by TARSKI:def 1;
hence contradiction by F3,TARSKI:def 1;
end;
suppose 1 <> a.1; then
G1: a.1 = 0 by F0,FIELD_3:2;
per cases by E,TARSKI:def 2;
suppose [2,a.2] = {i};
then F1: {{1,a.1}} = {{2},{2,a.2}} by F0,TARSKI:def 5;
{2} in {{2},{2,a.2}} & {2,a.2} in {{2},{2,a.2}} by TARSKI:def 2;
hence contradiction by G1,F1,CARD_1:50;
end;
suppose [2,a.2] = {i,q.i};
then F1: {2,q.i} = {{2},{2,a.2}} by CARD_1:50,F0,G1,TARSKI:def 5;
2 in {2,q.i} by TARSKI:def 2; then
per cases by F1,TARSKI:def 2;
suppose 2 = {2};
hence contradiction;
end;
suppose F2: 2 = {2,a.2};
2 in {2,a.2} by TARSKI:def 2;
hence contradiction by F2;
end;
end;
end;
end;
end;
hence thesis;
end;
end;
definition
let R be Ring;
attr R is strong_polynomial_disjoint means :dspd:
for a being Element of R
for S being Ring,
p being Element of the carrier of Polynom-Ring S holds a <> p;
end;
registration
cluster INT.Ring -> strong_polynomial_disjoint;
coherence by FIELD_3:25;
cluster F_Rat -> strong_polynomial_disjoint;
coherence by FIELD_3:25;
cluster F_Real -> strong_polynomial_disjoint;
coherence by FIELD_3:26;
end;
registration
let n be non trivial Nat;
cluster Z/n -> strong_polynomial_disjoint;
coherence
proof
Z/n = doubleLoopStr(#Segm(n),addint(n),multint(n),
In (1,Segm(n)),In (0,Segm(n))#) by INT_3:def 12;
hence thesis by FIELD_3:24;
end;
end;
registration
cluster strong_polynomial_disjoint -> polynomial_disjoint for Ring;
coherence
proof
let R be Ring;
assume A: R is strong_polynomial_disjoint;
set o = the Element of (the carrier of R)/\(the carrier of Polynom-Ring R);
now assume not R is polynomial_disjoint;
then [#]R /\ [#]Polynom-Ring R <> {} by FIELD_3:def 3;
then o in the carrier of R & o in the carrier of Polynom-Ring R
by XBOOLE_0:def 4;
hence contradiction by A;
end;
hence thesis;
end;
end;
registration
cluster strong_polynomial_disjoint for Field;
existence
proof
take F_Rat;
thus thesis;
end;
cluster non strong_polynomial_disjoint for Field;
existence
proof
consider F being Field such that
A: [#]F /\ [#]Polynom-Ring F <> {} by FIELD_3:14;
reconsider K = F as non polynomial_disjoint Field by A,FIELD_3:def 3;
K is non strong_polynomial_disjoint;
hence thesis;
end;
end;
theorem
for F being strong_polynomial_disjoint Field,
p being irreducible Element of the carrier of Polynom-Ring F
for E being Field st E = embField(emb p) holds E is strong_polynomial_disjoint
proof
let F be strong_polynomial_disjoint Field,
p be irreducible Element of the carrier of Polynom-Ring F;
let E be Field;
assume AS: E = embField(emb p);
set FX = Polynom-Ring F, EX = Polynom-Ring E, f = emb p,
Kr = KroneckerField(F,p);
X: [#] F = the carrier of F & [#] Kr = the carrier of Kr;
H: the carrier of E
= carr f by AS,FIELD_2:def 7
.= ((the carrier of Kr)\(rng f))\/(the carrier of F) by X,FIELD_2:def 2;
now assume E is non strong_polynomial_disjoint;
then consider o being Element of E,
S being Ring,
q being Element of the carrier of Polynom-Ring S such that
K: o = q;
set SX = Polynom-Ring S;
per cases by H,XBOOLE_0:def 3;
suppose o in the carrier of F;
hence contradiction by K,dspd;
end;
suppose o in (the carrier of Kr) \ (rng f); then
reconsider o as Element of (Polynom-Ring F)/({p}-Ideal);
consider a being Element of Polynom-Ring F such that
B: o = Class(EqRel(Polynom-Ring F,{p}-Ideal),a) by RING_1:11;
reconsider q as Polynomial of S;
a - a = 0.(Polynom-Ring F) by RLVECT_1:15; then
D0: a in q by K,B,RING_1:5,IDEAL_1:3; then
consider i,z being object such that
D1: i in NAT & z in the carrier of S & a = [i,z] by ZFMISC_1:def 2;
D2: z = q.i by D0,D1,FUNCT_1:1;
reconsider i as Element of NAT by D1;
reconsider a as Polynomial of F by POLYNOM3:def 10;
dom a = NAT by FUNCT_2:def 1; then
[1,a.1] in a & [2,a.2] in a by FUNCT_1:1; then
E: [1,a.1] in {{i},{i,q.i}} & [2,a.2] in {{i},{i,q.i}}
by D1,D2,TARSKI:def 5;
per cases by E,TARSKI:def 2;
suppose [1,a.1] = {i};
then E1: {i} = {{1},{1,a.1}} by TARSKI:def 5;
{1} in {{1},{1,a.1}} & {1,a.1} in {{1},{1,a.1}} by TARSKI:def 2;
hence contradiction by E1;
end;
suppose [1,a.1] = {i,q.i}; then
E1: {i,q.i} = {{1},{1,a.1}} by TARSKI:def 5;
i in {i,q.i} by TARSKI:def 2; then
F0: i = {1,a.1} by E1,TARSKI:def 2;
per cases;
suppose 1 = a.1; then
F3: {2} = {1} by F0,ENUMSET1:29;
2 in {2} by TARSKI:def 1;
hence contradiction by F3,TARSKI:def 1;
end;
suppose 1 <> a.1; then
G1: a.1 = 0 by F0,FIELD_3:2;
per cases by E,TARSKI:def 2;
suppose [2,a.2] = {i};
then F1: {{1,a.1}} = {{2},{2,a.2}} by F0,TARSKI:def 5;
{2} in {{2},{2,a.2}} & {2,a.2} in {{2},{2,a.2}} by TARSKI:def 2;
hence contradiction by G1,F1,CARD_1:50;
end;
suppose [2,a.2] = {i,q.i};
then F1: {2,q.i} = {{2},{2,a.2}} by CARD_1:50,F0,G1,TARSKI:def 5;
2 in {2,q.i} by TARSKI:def 2; then
per cases by F1,TARSKI:def 2;
suppose 2 = {2};
hence contradiction;
end;
suppose F2: 2 = {2,a.2};
2 in {2,a.2} by TARSKI:def 2;
hence contradiction by F2;
end;
end;
end;
end;
end;
end;
hence thesis;
end;
begin :: Renamings
definition
let X be non empty set,
Z be set;
mode Renaming of X,Z -> Function means :defr:
dom it = X & it is one-to-one & (rng it) /\ (X \/ Z) = {};
existence
proof
consider Y being set such that
A: card(Z \/ X) c= card Y & (Z \/ X) /\ Y = {} by thre;
card X c= card(Z \/ X) by XBOOLE_1:7,CARD_1:11; then
card X c= card Y by A; then
consider f being Function such that
B: f is one-to-one & dom f = X & rng f c= Y by CARD_1:10;
take f;
now assume C: (rng f) /\ (X \/ Z) <> {};
set o = the Element of (rng f) /\ (X \/ Z);
o in rng f & o in X \/ Z by C,XBOOLE_0:def 4;
hence contradiction by A,B,XBOOLE_0:def 4;
end;
hence thesis by B;
end;
end;
registration
let X be non empty set,
Z be set;
let r be Renaming of X,Z;
cluster dom r -> non empty;
coherence by defr;
cluster rng r -> non empty;
coherence
proof
set x = the Element of dom r;
r.x in rng r by FUNCT_1:3;
hence thesis;
end;
end;
registration
let X be non empty set,
Z be set;
cluster -> X-defined one-to-one for Renaming of X,Z;
coherence
proof
let r be Renaming of X,Z;
dom r = X by defr;
hence r is X-defined by RELAT_1:def 18;
thus thesis by defr;
end;
end;
definition
let X be non empty set,
Z be set;
let r be Renaming of X,Z;
redefine func r" -> Function of rng r, X; :: redefines " (FUNCT_1, definition)
coherence
proof
dom r = X by defr;
then r is Function of X,(rng r) by FUNCT_2:2;
hence thesis by FUNCT_2:25;
end;
end;
theorem lemonto:
for X being non empty set,
Z being set
for r being Renaming of X,Z holds r" is onto
proof
let X be non empty set, Z be set;
let r be Renaming of X,Z;
A: now let o be object;
assume o in X; then
H: o in dom r by defr; then
r.o in rng r by FUNCT_1:3; then
r.o in dom(r") by FUNCT_2:def 1; then
r".(r.o) in rng(r") by FUNCT_1:3;
hence o in rng(r") by H,FUNCT_1:34;
end;
now let o be object;
assume o in rng(r");
then o in dom r by FUNCT_1:33;
hence o in X;
end;
hence thesis by A,TARSKI:2;
end;
definition
let F be Field,
Z be set;
let r be Renaming of (the carrier of F), Z;
func ren_add r -> BinOp of rng r means :defra:
for a,b being Element of rng r holds it.(a,b) = r.((r").a + (r").b);
existence
proof
defpred P[Element of rng r,Element of rng r,Element of rng r] means
$3 = r.((r").$1 + (r").$2);
A: now let x,y be Element of rng r;
set z = r.((r").x + (r").y);
dom r = the carrier of F by defr;
then z in rng r by FUNCT_1:3;
hence ex z being Element of rng r st P[x,y,z];
end;
consider F being BinOp of (rng r) such that
B: for a,b being Element of (rng r) holds P[a,b,F.(a,b)]
from BINOP_1:sch 3(A);
take F;
let a,b be Element of rng r;
thus thesis by B;
end;
uniqueness
proof
let F1,F2 be BinOp of (rng r) such that
A2: for a,b being Element of (rng r) holds F1.(a,b) = r.((r").a + (r").b)
and
A3: for a,b being Element of (rng r) holds F2.(a,b) = r.((r").a + (r").b);
now let a,b be Element of (rng r);
thus F1.(a,b) = r.((r").a + (r").b) by A2 .= F2.(a,b) by A3;
end;
hence thesis;
end;
end;
definition
let F be Field,
Z be set;
let r be Renaming of (the carrier of F), Z;
func ren_mult r -> BinOp of (rng r) means :defrm:
for a,b being Element of (rng r) holds it.(a,b) = r.((r").a * (r").b);
existence
proof
defpred P[Element of rng r,Element of rng r,Element of rng r] means
$3 = r.((r").$1 * (r").$2);
A: now let x,y be Element of rng r;
set z = r.((r").x * (r").y);
dom r = the carrier of F by defr;
then z in rng r by FUNCT_1:3;
hence ex z being Element of rng r st P[x,y,z];
end;
consider F being BinOp of (rng r) such that
B: for a,b being Element of (rng r) holds P[a,b,F.(a,b)]
from BINOP_1:sch 3(A);
take F;
let a,b be Element of (rng r);
thus thesis by B;
end;
uniqueness
proof
let F1,F2 be BinOp of (rng r) such that
A2: for a,b being Element of (rng r) holds F1.(a,b) = r.((r").a * (r").b)
and
A3: for a,b being Element of (rng r) holds F2.(a,b) = r.((r").a * (r").b);
now let a,b be Element of (rng r);
thus F1.(a,b) = r.((r").a * (r").b) by A2 .= F2.(a,b) by A3;
end;
hence thesis;
end;
end;
definition
let F be Field,
Z be set;
let r be Renaming of (the carrier of F), Z;
func RenField r -> strict doubleLoopStr means :defrf:
the carrier of it = rng r &
the addF of it = ren_add r &
the multF of it = ren_mult r &
the OneF of it = r.(1.F) &
the ZeroF of it = r.(0.F);
existence
proof
H: dom r = the carrier of F by defr; then
reconsider e = r.(1.F) as Element of (rng r) by FUNCT_1:3;
reconsider o = r.(0.F) as Element of (rng r) by H,FUNCT_1:3;
take doubleLoopStr (# rng r,ren_add r, ren_mult r,e,o #);
thus thesis;
end;
uniqueness;
end;
registration
let F be Field,
Z be set;
let r be Renaming of (the carrier of F), Z;
cluster RenField r -> non degenerated;
coherence
proof
dom r = the carrier of F by defr;
then r.(0.F) <> r.(1.F) by FUNCT_1:def 4;
then 0.(RenField r) <> r.(1.F) by defrf;
hence thesis by defrf;
end;
end;
registration
let F be Field,
Z be set;
let r be Renaming of (the carrier of F), Z;
cluster RenField r -> Abelian add-associative right_zeroed
right_complementable;
coherence
proof
set K = RenField r;
thus K is Abelian
proof
now let a,b be Element of K;
reconsider a1 = a, b1 = b as Element of rng r by defrf;
thus a + b = (ren_add r).(a,b) by defrf
.= r.((r").a1 + (r").b1) by defra
.= (ren_add r).(b,a) by defra
.= b + a by defrf;
end;
hence thesis;
end;
thus K is add-associative
proof
now let a,b,c be Element of K;
reconsider a1 = a, b1 = b, c1 = c as Element of rng r by defrf;
H: dom r = the carrier of F by defr; then
reconsider ab = r.((r").a1 + (r").b1),
bc = r.((r").b1 + (r").c1) as Element of rng r by FUNCT_1:3;
thus (a + b) + c = (ren_add r).(a+b,c) by defrf
.= (ren_add r).((ren_add r).(a,b),c) by defrf
.= (ren_add r).(r.((r").a1 + (r").b1),c) by defra
.= r.((r").ab + (r").c1) by defra
.= r.(((r").a1 + (r").b1) + (r").c1) by H,FUNCT_1:34
.= r.((r").a1 + ((r").b1 + (r").c1)) by RLVECT_1:def 3
.= r.((r").a1 + (r").bc) by H,FUNCT_1:34
.= (ren_add r).(a,r.((r").b1 + (r").c1)) by defra
.= (ren_add r).(a,(ren_add r).(b,c)) by defra
.= (ren_add r).(a,b+c) by defrf
.= a + (b + c) by defrf;
end;
hence thesis;
end;
thus K is right_zeroed
proof
now let a be Element of K;
reconsider a1 = a as Element of rng r by defrf;
H0: dom r = the carrier of F by defr; then
reconsider o = r.(0.F) as Element of (rng r) by FUNCT_1:3;
H1: (r").(r.(0.F)) = 0.F by H0,FUNCT_1:34;
thus a + 0.K = (ren_add r).(a,0.K) by defrf
.= (ren_add r).(a,r.(0.F)) by defrf
.= r.((r").a1 + (r").o) by defra
.= a by H1,FUNCT_1:35;
end;
hence thesis;
end;
thus K is right_complementable
proof
now let a be Element of K;
reconsider a1 = a as Element of rng r by defrf;
(r").a1 is right_complementable; then
consider b1 being Element of F such that H0: (r").a1 + b1 = 0.F;
H1: rng r = the carrier of K by defrf;
H2: dom r = the carrier of F by defr; then
reconsider b = r.b1 as Element of K by H1,FUNCT_1:3;
reconsider o = r.b1 as Element of (rng r) by H2,FUNCT_1:3;
a + b = (ren_add r).(a,b) by defrf
.= r.((r").a1 + (r").o) by defra
.= r.(0.F) by H0,H2,FUNCT_1:34
.= 0.K by defrf;
hence a is right_complementable;
end;
hence thesis;
end;
end;
end;
registration
let F be Field,
Z be set;
let r be Renaming of (the carrier of F), Z;
cluster RenField r -> commutative associative well-unital
distributive almost_left_invertible;
coherence
proof
set K = RenField r;
thus C: K is commutative
proof
now let a,b be Element of K;
reconsider a1 = a, b1 = b as Element of rng r by defrf;
thus a * b = (ren_mult r).(a,b) by defrf
.= r.((r").a1 * (r").b1) by defrm
.= r.((r").b1 * (r").a1) by GROUP_1:def 12
.= (ren_mult r).(b,a) by defrm
.= b * a by defrf;
end;
hence thesis;
end;
thus K is associative
proof
now let a,b,c be Element of K;
reconsider a1 = a, b1 = b, c1 = c as Element of rng r by defrf;
H0: dom r = the carrier of F by defr; then
reconsider ab = r.((r").a1 * (r").b1),
bc = r.((r").b1 * (r").c1) as Element of rng r by FUNCT_1:3;
thus (a * b) * c = (ren_mult r).(a*b,c) by defrf
.= (ren_mult r).((ren_mult r).(a,b),c) by defrf
.= (ren_mult r).(r.((r").a1 * (r").b1),c) by defrm
.= r.((r").ab * (r").c1) by defrm
.= r.(((r").a1 * (r").b1) * (r").c1) by H0,FUNCT_1:34
.= r.((r").a1 * ((r").b1 * (r").c1)) by GROUP_1:def 3
.= r.((r").a1 * (r").bc) by H0,FUNCT_1:34
.= (ren_mult r).(a,r.((r").b1 * (r").c1)) by defrm
.= (ren_mult r).(a,(ren_mult r).(b,c)) by defrm
.= (ren_mult r).(a,b*c) by defrf
.= a * (b * c) by defrf;
end;
hence thesis;
end;
thus K is well-unital
proof
now let a be Element of K;
reconsider a1 = a as Element of rng r by defrf;
H0: dom r = the carrier of F by defr; then
reconsider o = r.(1.F) as Element of (rng r) by FUNCT_1:3;
H1: (r").(r.(1.F)) = 1.F by H0,FUNCT_1:34;
thus a * 1.K = (ren_mult r).(a,1.K) by defrf
.= (ren_mult r).(a,r.(1.F)) by defrf
.= r.((r").a1 * (r").o) by defrm
.= a by H1,FUNCT_1:35;
thus 1.K * a = (ren_mult r).(1.K,a) by defrf
.= (ren_mult r).(r.(1.F),a) by defrf
.= r.((r").o * (r").a1) by defrm
.= a by H1,FUNCT_1:35;
end;
hence thesis;
end;
thus K is distributive
proof
D: now let a,b,c be Element of K;
reconsider a1 = a, b1 = b, c1 = c as Element of rng r by defrf;
H: dom r = the carrier of F by defr; then
reconsider ab = r.((r").a1 + (r").b1),
ac = r.((r").a1 * (r").c1),
bc = r.((r").b1 * (r").c1) as Element of (rng r) by FUNCT_1:3;
thus (a + b) * c = (ren_mult r).(a+b,c) by defrf
.= (ren_mult r).((ren_add r).(a,b),c) by defrf
.= (ren_mult r).(r.((r").a1 + (r").b1),c) by defra
.= r.((r").ab * (r").c1) by defrm
.= r.(((r").a1 + (r").b1) * (r").c1) by H,FUNCT_1:34
.= r.((r").a1 * (r").c1 + (r").b1 * (r").c1) by VECTSP_1:def 7
.= r.((r").ac + (r").b1 * (r").c1) by H,FUNCT_1:34
.= r.((r").ac + (r").bc) by H,FUNCT_1:34
.= (ren_add r).(ac,bc) by defra
.= (ren_add r).(r.((r").a1 * (r").c1),(ren_mult r).(b,c)) by defrm
.= (ren_add r).((ren_mult r).(a,c),(ren_mult r).(b,c)) by defrm
.= (ren_add r).(a*c,(ren_mult r).(b,c)) by defrf
.= (ren_add r).(a*c,b*c) by defrf
.= (a * c) + (b * c) by defrf;
end;
now let a,b,c be Element of K;
thus (a + b) * c = a * c + b * c by D;
thus a * (b + c) = (b + c) * a by C
.= b * a + c * a by D
.= a * b + c * a by C
.= a * b + a * c by C;
end;
hence thesis;
end;
thus K is almost_left_invertible
proof
now let a be Element of K;
assume AS: a <> 0.K;
reconsider a1 = a as Element of rng r by defrf;
I0: dom r = the carrier of F by defr;
I1: rng r = the carrier of K by defrf;
I2: dom(r") = rng r by FUNCT_1:33;
0.K = r.(0.F) by defrf; then
(r").a1 <> (r").(r.(0.F)) by I1,I2,AS,FUNCT_1:def 4; then
(r").a1 <> 0.F by I0,FUNCT_1:34; then
(r").a1 is left_invertible by ALGSTR_0:def 39; then
consider b1 being Element of F such that
H0: b1 * (r").a1 = 1.F;
H1: rng r = the carrier of K by defrf;
H2: dom r = the carrier of F by defr; then
reconsider b = r.b1 as Element of K by H1,FUNCT_1:3;
reconsider o = r.b1 as Element of (rng r) by H2,FUNCT_1:3;
b * a = (ren_mult r).(b,a) by defrf
.= r.((r").o * (r").a1) by defrm
.= r.(1.F) by I0,H0,FUNCT_1:34
.= 1.K by defrf;
hence a is left_invertible;
end;
hence thesis;
end;
end;
end;
definition
let F be Field,
Z be set;
let r be Renaming of (the carrier of F), Z;
redefine func r" -> Function of (RenField r), F; :: redefines " (FUNCT_1, definition)
coherence
proof
H0: the carrier of RenField r = rng r by defrf
.= dom(r") by FUNCT_1:33;
rng(r") = dom r by FUNCT_1:33 .= the carrier of F by defr;
hence thesis by H0,FUNCT_2:1;
end;
end;
theorem thiso:
for F being Field,
Z being set
for r being Renaming of (the carrier of F), Z
holds r" is additive multiplicative unity-preserving
one-to-one onto
proof
let F be Field, Z be set;
let r be Renaming of (the carrier of F), Z;
set K = RenField r;
H0: dom r = the carrier of F by defr;
now let a,b be Element of K;
reconsider a1 = a, b1 = b as Element of (rng r) by defrf;
thus (r").(a+b) = (r").((ren_add r).(a1,b1)) by defrf
.= (r").(r.((r").a + (r").b)) by defra
.= (r").a + (r").b by H0,FUNCT_1:34;
end;
hence r" is additive;
now let a,b be Element of K;
reconsider a1 = a, b1 = b as Element of (rng r) by defrf;
thus (r").(a*b) = (r").((ren_mult r).(a1,b1)) by defrf
.= (r").(r.((r").a * (r").b)) by defrm
.= (r").a * (r").b by H0,FUNCT_1:34;
end;
hence r" is multiplicative;
r.(1.F) = 1.K by defrf;
hence r" is unity-preserving by H0,FUNCT_1:34;
thus r" is one-to-one;
thus r" is onto by lemonto;
end;
theorem thisofield:
for F being Field,
Z being set
ex E being Field st E,F are_isomorphic &
(the carrier of E) /\ ((the carrier of F) \/ Z) = {}
proof
let F be Field, Z be set;
set r = the Renaming of (the carrier of F),Z;
take E = RenField r;
r" is linear by thiso; then
r" is isomorphism by thiso,MOD_4:def 12;
hence E,F are_isomorphic;
rng r = the carrier of E by defrf;
hence thesis by defr;
end;
begin :: Kronecker's Construction
kron:
for F being Field
for p being irreducible Element of the carrier of Polynom-Ring F
ex E being FieldExtension of F st p is_with_roots_in E
proof
let F be Field;
let p be irreducible Element of the carrier of Polynom-Ring F;
set KF = KroneckerField(F,p), u = KrRoot p;
consider FP being Field such that
X1: KF,FP are_isomorphic &
(the carrier of FP) /\ ((the carrier of KF) \/ (the carrier of F)) = {}
by thisofield;
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;
reconsider KroneckerIsop = (KroneckerIso p)" as
Isomorphism of KroneckerField(F,p),Polynom-Ring p by RING_3:73;
set h = phi * (emb p);
reconsider h as Function of F,FP by FUNCT_2:13;
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;
Y: emb_iso h is linear one-to-one onto
by X2,FIELD_2:13,FIELD_2:14, 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 by FUNCT_2:13;
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;
u is_a_root_of emb(p,p) by FIELD_1:42; then
Z: eval((PolyHom iso).(emb(p,p)),iso.u) = 0.E by FIELD_1:33,POLYNOM5:def 7;
F is Subfield of E by FIELD_2:17;
then reconsider E as FieldExtension of F by FIELD_4:7;
take E;
reconsider a = iso.u as Element of E;
(PolyHom iso).(emb(p,p)) = p
proof
set g = (PolyHom iso).(emb(p,p));
A: for a being Element of F holds iso.((emb p).a) = a
proof
let a be Element of F;
reconsider b = a|F as Element of the carrier of Polynom-Ring F
by POLYNOM3:def 10;
reconsider v = Class(EqRel(Polynom-Ring F,{p}-Ideal),b)
as Element of KroneckerField(F,p) by RING_1:12;
dom(emb p) = the carrier of F by FUNCT_2:def 1; then
C: h.a = phi.((emb p).a) by FUNCT_1:13 .= phi.v by FIELD_1:39;
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 p).a) = (embisoh * phi).v by FIELD_1:39
.= ((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.(emb(p,p).i) by FIELD_1:def 2
.= iso.(Class(EqRel(Polynom-Ring F,{p}-Ideal),(p.i)|F))
by FIELD_1:40
.= iso.((emb p).(p.i)) by FIELD_1:39;
hence g.x = p.x by A;
end;
hence thesis;
end;
then Ext_eval(p,a) = 0.E by Z,FIELD_4:26;
hence thesis by FIELD_4:def 3,def 2;
end;
theorem main: :: Kronecker
for F being Field
for f being non constant Element of the carrier of Polynom-Ring F
ex E being FieldExtension of F st f is_with_roots_in E
proof
let F be Field;
let f be non constant Element of the carrier of Polynom-Ring F;
consider p being Element of the carrier of Polynom-Ring F such that
A: p is_a_irreducible_factor_of f by FIELD_1:3;
reconsider p as irreducible Element of the carrier of Polynom-Ring F by A;
consider q being Element of the carrier of Polynom-Ring F such that
B: p * q = f by A,GCD_1:def 1;
consider E being FieldExtension of F such that
C: p is_with_roots_in E by kron;
take E;
consider a being Element of E such that
D: a is_a_root_of p,E by C,FIELD_4:def 3;
reconsider p1 = p, q1 = q as Polynomial of F;
F: F is Subring of E by FIELD_4:def 1;
Ext_eval(f,a) = Ext_eval(p1*'q1,a) by B,POLYNOM3:def 10
.= Ext_eval(p1,a) * Ext_eval(q1,a) by F,ALGNUM_1:20
.= 0.E * Ext_eval(q1,a) by D,FIELD_4:def 2;
hence thesis by FIELD_4:def 2,def 3;
end;
theorem
for F being Field
for f being non constant Element of the carrier of Polynom-Ring F
ex E being FieldExtension of F st f splits_in E
proof
let F be Field;
let f be non constant Element of the carrier of Polynom-Ring F;
defpred P[Nat] means
for F being Field
for f being non constant Element of the carrier of Polynom-Ring F
st deg f = $1
ex E being FieldExtension of F st f splits_in E;
IA: P[1]
proof
let F be Field;
let f be non constant Element of the carrier of Polynom-Ring F;
assume A: deg f = 1;
reconsider E = F as FieldExtension of F by FIELD_4:6;
take E;
thus thesis by FIELD_4:29,A;
end;
IS: now let k be non zero Nat;
assume IV: P[k];
now let F be Field;
let f be non constant Element of the carrier of Polynom-Ring F;
assume AS2: deg f = k + 1;
consider E1 being FieldExtension of F such that
A: f is_with_roots_in E1 by main;
reconsider f1 = f as Polynomial of E1 by FIELD_4:8;
reconsider f1 as Element of the carrier of Polynom-Ring E1
by POLYNOM3:def 10;
consider a being Element of E1 such that
B: a is_a_root_of f,E1 by A,FIELD_4:def 3;
reconsider h = rpoly(1,a) as
Element of the carrier of Polynom-Ring E1 by POLYNOM3:def 10;
reconsider q = rpoly(1,a) as Ppoly of E1 by RING_5:51;
Ext_eval(f,a) = 0.E1 by B,FIELD_4:def 2; then
0.E1 = eval(f1,a) by FIELD_4:26; then
consider g2 being Polynomial of E1 such that
C1: f1 = h *' g2 by RING_4:1,RING_5:11;
reconsider g = g2 as Element of the carrier of Polynom-Ring E1
by POLYNOM3:def 10;
C: f1 = h * g by C1,POLYNOM3:def 10;
per cases;
suppose g is constant;
then consider e being Element of E1 such that
D: g = e|E1 by RING_4:20;
now assume e is zero;
then g = 0_.E1 by D,RING_4:13;
then f = 0_.F by C1,FIELD_4:12;
hence contradiction;
end;
then reconsider e as non zero Element of E1;
f = rpoly(1,a) *' (e * 1_.E1) by D,C1,RING_4:16
.= e * (rpoly(1,a) *' 1_.E1) by RING_4:10
.= e * q;
hence ex E being FieldExtension of F st f splits_in E
by FIELD_4:def 5;
end;
suppose I: g is non constant;
deg g = k
proof
reconsider g1 = g as Polynomial of E1;
g1 <> 0_.(E1) by I; then
D: deg f1 = deg(rpoly(1,a)) + deg g1 by C1,HURWITZ:23
.= 1 + deg g1 by HURWITZ:27;
deg f1 = k + 1 by AS2,FIELD_4:20;
hence thesis by D;
end;
then consider E2 being FieldExtension of E1 such that
E: g splits_in E2 by I,IV;
reconsider E2 as FieldExtension of F;
consider e being non zero Element of E2,
r being Ppoly of E2 such that
F: g = e * r by E,FIELD_4:def 5;
E1 is Subring of E2 by FIELD_4:def 1; then
the carrier of E1 c= the carrier of E2 by C0SP1:def 3; then
reconsider a1 = a as Element of E2;
rpoly(1,a1) is Ppoly of E2 by RING_5:51; then
reconsider u = rpoly(1,a1) *' r as Ppoly of E2 by RING_5:52;
reconsider q = rpoly(1,a) as Polynomial of E2 by FIELD_4:8;
reconsider q1 = q as Element of the carrier of Polynom-Ring E2
by POLYNOM3:def 10;
reconsider eg = e * r as Element of the carrier
of Polynom-Ring E2 by POLYNOM3:def 10;
Y: q = rpoly(1,a1) by FIELD_4:21;
Z1: [h,g] in [:the carrier of Polynom-Ring E1,
the carrier of Polynom-Ring E1:] by ZFMISC_1:def 2;
(the multF of (Polynom-Ring E2))||the carrier of (Polynom-Ring E1)
= the multF of (Polynom-Ring E1) by FIELD_4:18; then
f = q1 * eg by F,C,Z1,FUNCT_1:49
.= q *' (e * r) by POLYNOM3:def 10
.= e * u by Y,RING_4:10;
hence ex E being FieldExtension of F st f splits_in E
by FIELD_4:def 5;
end;
end;
hence P[k+1];
end;
I: for k being non zero Nat holds P[k] from NAT_1:sch 10(IA,IS);
consider n being Nat such that H: deg f = n;
n + 1 > 0 + 1 by H,RING_4:def 4,XREAL_1:6;
hence thesis by I,H;
end;