:: Characteristic of Rings; Prime Fields
:: by Christoph Schwarzweller and Artur Korni{\l}owicz
::
:: Received August 14, 2015
:: Copyright (c) 2015-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, FUNCT_1, RELAT_1, RLVECT_1, VECTSP_1, ALGSTR_0, TARSKI,
INT_1, FUNCT_2, VECTSP_2, VECTSP10, STRUCT_0, SUBSET_1, SUPINF_2, NAT_1,
CARD_1, MESFUNC1, INT_3, GROUP_1, ARYTM_1, ORDINAL1, INT_2, QUOFIELD,
MSSUBFAM, BINOP_1, GROUP_6, MOD_4, LATTICES, NUMBERS, IDEAL_1, C0SP1,
ZFMISC_1, FUNCSDOM, RING_2, FINSET_1, XXREAL_0, WELLORD1, REALSET1,
XBOOLE_0, EC_PF_1, BINOP_2, COMPLFLD, GAUSSINT, XCMPLX_0, REAL_1, RING_3,
RAT_1, NEWTON;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, DOMAIN_1, RELAT_1,
FUNCT_1, RELSET_1, PARTFUN1, ORDINAL1, FUNCT_2, BINOP_1, REALSET1,
XXREAL_0, XREAL_0, CARD_1, BINOP_2, XXREAL_2, NAT_1, INT_1, INT_2,
NAT_D, RAT_1, INT_3, GCD_1, XCMPLX_0, NUMBERS, MATRLIN2, STRUCT_0,
MOD_4, BINOM, ALGSTR_0, GROUP_1, GROUP_6, RLVECT_1, VECTSP_2,
VECTSP_1, GR_CY_1, COMPLFLD, VECTSP10, EC_PF_1, GAUSSINT, IDEAL_1,
QUOFIELD, C0SP1, RING_1, RING_2;
constructors BINOM, QUOFIELD, MOD_4, REALSET1, BINOP_2, GCD_1, RINGCAT1,
XXREAL_2, RING_2, GAUSSINT, GR_CY_1, EC_PF_1, NAT_D, MATRLIN2, TOPALG_7;
registrations ORDINAL1, XXREAL_0, XREAL_0, RELSET_1, VECTSP_1, STRUCT_0,
MEMBERED, NUMBERS, XBOOLE_0, RAT_1, RLVECT_1, INT_1, INT_3, COMPLFLD,
REALSET1, GAUSSINT, NAT_1, ALGSTR_1, SUBSET_1, RELAT_1, FUNCT_2,
ALGSTR_0, QUOFIELD, GROUP_6, MOD_4, RINGCAT1, RING_1, C0SP1, GRCAT_1,
XCMPLX_0, XXREAL_2, FOMODEL0, RING_2, NAT_2, FUNCT_1, CARD_1, EC_PF_1;
requirements NUMERALS, SUBSET, BOOLE, REAL, ARITHM;
definitions TARSKI, FUNCT_2, INT_1, STRUCT_0, ALGSTR_0, VECTSP_1, REALSET1,
GROUP_1, GROUP_6, RLVECT_1, QUOFIELD, RING_2;
equalities BINOP_1, REALSET1, XCMPLX_0, STRUCT_0, ALGSTR_0, VECTSP_1,
QUOFIELD, COMPLEX1, VECTSP10, INT_3, GAUSSINT, INT_1, MATRLIN2;
expansions STRUCT_0, GROUP_1, VECTSP_1, XBOOLE_0, FUNCT_1, RINGCAT1, QUOFIELD,
GROUP_6, TARSKI, RING_2, INT_1;
theorems GROUP_1, GROUP_6, VECTSP_1, VECTSP_2, FUNCT_2, TARSKI, BINOM, INT_1,
INT_2, INT_3, FUNCT_1, RLVECT_1, RING_2, EC_PF_1, XREAL_1, NAT_2,
XXREAL_0, ORDINAL1, XBOOLE_0, IDEAL_1, XCMPLX_1, XXREAL_2, C0SP1, NAT_1,
QUOFIELD, GR_CY_1, GAUSSINT, SUBSET_1, GCD_1, NUMBERS, RELAT_1, ZFMISC_1,
BINOP_2, COMPLFLD, RAT_1, EC_PF_2, XCMPLX_0, PEPIN, PRE_FF, WSIERP_1;
schemes NAT_1, INT_1, FUNCT_2;
begin :: Preliminaries
theorem Th1:
for f being Function, A being set, a,b being object st a in A & b in A
holds (f||A).(a,b) = f.(a,b)
proof
let f be Function;
let A be set;
let a,b be object;
assume a in A & b in A;
then [a,b] in [:A,A:] by ZFMISC_1:def 2;
hence thesis by FUNCT_1:49;
end;
theorem Th2:
addcomplex||REAL = addreal
proof
set ad = addcomplex||REAL;
[:REAL,REAL:] c= [:COMPLEX,COMPLEX:] by NUMBERS:11,ZFMISC_1:96;
then
A1: [:REAL,REAL:] c= dom(addcomplex) by FUNCT_2:def 1;
then
A2: dom ad = [:REAL,REAL:] by RELAT_1:62;
A3: dom(addreal) = [:REAL,REAL:] by FUNCT_2:def 1;
for z be object st z in dom ad holds ad.z = addreal.z
proof
let z be object;
assume
A4: z in dom ad;
then consider x, y be object such that
A5: x in REAL & y in REAL & z = [x,y] by A2,ZFMISC_1:def 2;
reconsider x1 = x, y1 = y as Real by A5;
thus ad.z = addcomplex.(x1,y1) by A4,A5,A2,FUNCT_1:49
.= x1+y1 by BINOP_2:def 3
.= addreal.(x1,y1) by BINOP_2:def 9
.= addreal.z by A5;
end;
hence thesis by A1,A3,RELAT_1:62;
end;
theorem Th3:
multcomplex||REAL = multreal
proof
set mu = multcomplex||REAL;
[:REAL,REAL:] c= [:COMPLEX,COMPLEX:] by NUMBERS:11,ZFMISC_1:96;
then
A1: [:REAL,REAL:] c= dom(multcomplex) by FUNCT_2:def 1;
then
A2: dom mu = [:REAL,REAL:] by RELAT_1:62;
A3: dom(multreal) = [:REAL,REAL:] by FUNCT_2:def 1;
for z be object st z in dom mu holds mu.z = multreal.z
proof
let z be object;
assume
A4: z in dom mu;
then consider x, y be object such that
A5: x in REAL & y in REAL & z = [x,y] by A2,ZFMISC_1:def 2;
reconsider x1 = x, y1 = y as Real by A5;
thus mu.z = multcomplex.(x1,y1) by A4,A5,A2,FUNCT_1:49
.= x1*y1 by BINOP_2:def 5
.= multreal.(x1,y1) by BINOP_2:def 11
.= multreal.z by A5;
end;
hence thesis by A1,A3,RELAT_1:62;
end;
theorem Th4:
addrat||INT = addint
proof
set ad = addrat||INT;
[:INT,INT:] c= [:RAT,RAT:] by NUMBERS:14,ZFMISC_1:96;
then
A1: [:INT,INT:] c= dom(addrat) by FUNCT_2:def 1;
then
A2: dom ad = [:INT,INT:] by RELAT_1:62;
A3: dom(addint) = [:INT,INT:] by FUNCT_2:def 1;
for z be object st z in dom ad holds ad.z = addint.z
proof
let z be object;
assume
A4: z in dom ad;
then consider x, y be object such that
A5: x in INT & y in INT & z = [x,y] by A2,ZFMISC_1:def 2;
reconsider x1 = x, y1 = y as Integer by A5;
thus ad.z = addrat.(x1,y1) by A4,A5,A2,FUNCT_1:49
.= x1+y1 by BINOP_2:def 15
.= addint.(x1,y1) by BINOP_2:def 20
.= addint.z by A5;
end;
hence thesis by A1,A3,RELAT_1:62;
end;
theorem Th5:
multrat||INT = multint
proof
set mu = multrat||INT;
[:INT,INT:] c= [:RAT,RAT:] by NUMBERS:14,ZFMISC_1:96;
then
A1: [:INT,INT:] c= dom(multrat) by FUNCT_2:def 1;
then
A2: dom mu = [:INT,INT:] by RELAT_1:62;
A3: dom(multint) = [:INT,INT:] by FUNCT_2:def 1;
for z be object st z in dom mu holds mu.z = multint.z
proof
let z be object;
assume
A4: z in dom mu;
then consider x, y be object such that
A5: x in INT & y in INT & z = [x,y] by A2,ZFMISC_1:def 2;
reconsider x1 = x, y1 = y as Integer by A5;
thus mu.z = multrat.(x1,y1) by A4,A5,A2,FUNCT_1:49
.= x1*y1 by BINOP_2:def 17
.= multint.(x1,y1) by BINOP_2:def 22
.= multint.z by A5;
end;
hence thesis by A1,A3,RELAT_1:62;
end;
begin :: Properties of Fractions
reserve p,q for Rational;
reserve g,m,m1,m2,n,n1,n2 for Nat;
reserve i,i1,i2,j,j1,j2 for Integer;
theorem Th6:
n divides i implies i div n = i / n
proof
per cases;
suppose n = 0;
hence thesis;
end;
suppose
A1: n <> 0;
assume
A2: n divides i;
i mod n = 0 by A2;
hence thesis by PEPIN:63;
end;
end;
theorem Th7:
i div (i gcd n) = i / (i gcd n)
proof
i gcd n divides i & i gcd n divides n by INT_2:def 2;
hence thesis by Th6;
end;
theorem Th8:
n div (n gcd i) = n / (n gcd i)
proof
i gcd n divides i & i gcd n divides n by INT_2:def 2;
hence thesis by Th6;
end;
theorem Th9:
g divides i & g divides m implies i / m = (i div g) / (m div g)
proof
assume that
A1: g divides i and
A2: g divides m;
per cases;
suppose g = 0;
hence thesis by A1;
end;
suppose
A4: m = 0;
i / 0 = 0 & (i div g) / (0 div g) = 0 by XCMPLX_1:49;
hence thesis by A4;
end;
suppose that
A5: g <> 0 and
A6: m <> 0;
g <= m by A2,A6,INT_2:27;
then
A7: m div g <> 0 by A5,NAT_2:13;
i mod g = 0 & m mod g = 0 by A1,A2;
then m div g = m / g & i div g = i / g by PEPIN:63;
then i * (m div g) = m * (i div g);
hence thesis by A6,A7,XCMPLX_1:94;
end;
end;
theorem Th10:
i / m = (i div (i gcd m)) / (m div (i gcd m))
proof
i gcd m divides i & i gcd m divides m by INT_2:def 2;
hence thesis by Th9;
end;
theorem Th11:
0 < m & m*i divides m implies i = 1 or i = -1
proof
assume that
A1: 0 < m and
A2: m*i divides m;
m divides m*i;
then m = m*i or m = ---m*i by A2,INT_2:11;
hence i = 1 or i = -1 by A1,XCMPLX_1:7,181;
end;
theorem
0 < m & m*n divides m implies n = 1
proof
assume that
A1: 0 < m and
A2: m*n divides m;
m divides m*n;
then m = m*n or m = -m*n by A2,INT_2:11;
hence n = 1 by A1,XCMPLX_1:7;
end;
theorem
m divides i implies i div m divides i
proof
assume
A1: m divides i;
per cases;
suppose
A2: m <> 0;
take m;
i div m = i/m by A1,Th6;
hence thesis by A2,XCMPLX_1:87;
end;
suppose m = 0;
hence thesis by A1;
end;
end;
theorem Th14:
m <> 0 implies (i div (i gcd m)) gcd (m div (i gcd m)) = 1
proof
set g = i gcd m;
set a = i div g, b = m div g;
assume
A1: m <> 0;
then
A2: g <> 0 by INT_2:5;
A3: 1 divides a & 1 divides b by INT_2:12;
now
let w be Integer such that
A4: w divides a and
A5: w divides b;
consider i1 such that
A6: a = i1*w by A4;
consider i2 such that
A7: b = i2*w by A5;
A8: g divides i by INT_2:def 2;
A9: g divides m by INT_2:def 2;
A10: now
assume
A11: w = 0;
g <= m by A1,A9,INT_2:27;
hence contradiction by A2,A5,A11,NAT_2:13;
end;
A12: (i/g/w)*w = i/g by A10,XCMPLX_1:87;
A13: (m/g/w)*w = m/g by A10,XCMPLX_1:87;
i/g/w = i1*w/w by A6,A8,Th6
.= i1 by A10,XCMPLX_1:89;
then (i/g/w)*w*g = i1*w*g;
then i = i1*(g*w) by A12,A2,XCMPLX_1:87;
then
A14: g*w divides i;
m/g/w = i2*w/w by A7,A9,Th6
.= i2 by A10,XCMPLX_1:89;
then (m/g/w)*w*g = i2*w*g;
then m = i2*(g*w) by A13,A2,XCMPLX_1:87;
then g*w divides m;
then g*w divides g by A14,INT_2:def 2;
then w = 1 or w = -1 by A2,Th11;
hence w divides 1 by INT_2:14;
end;
hence a gcd b = 1 by A3,INT_2:def 2;
end;
theorem Th15:
m <> 0 implies
denominator(i/m) = m div ( i gcd m ) &
numerator(i/m) = i div ( i gcd m )
proof
set p = i/m;
set g = i gcd m;
set d = m div g;
assume
A1: 0 <> m;
then
A2: g <> 0 by INT_2:5;
g divides m by INT_2:def 2;
then g <= m by A1,INT_2:27;
then
A3: d <> 0 by A2,PRE_FF:3;
A4: p = (i div g) / d by Th10;
now
given w being Nat such that
A5: 1 < w and
A6: ex i1,m1 st i div g = i1*w & m div g = m1*w;
consider i1,m1 such that
A7: i div g = i1*w and
A8: d = m1*w by A6;
w divides i div g & w divides m div g by A7,A8;
then
A9: w divides (i div g) gcd (m div g) by INT_2:def 2;
(i div g) gcd (m div g) = 1 by A1,Th14;
hence contradiction by A5,A9,WSIERP_1:15;
end;
hence thesis by A3,A4,RAT_1:30;
end;
theorem
m <> 0 implies
denominator(i/m) = m / ( i gcd m ) &
numerator(i/m) = i / ( i gcd m )
proof
assume
A1: m <> 0;
hence denominator(i/m) = m div ( i gcd m ) by Th15
.= m / ( i gcd m ) by Th8;
thus numerator(i/m) = i div ( i gcd m ) by A1,Th15
.= i / ( i gcd m ) by Th7;
end;
theorem Th17:
m <> 0 implies
denominator -(i/m) = m div ( (-i) gcd m ) &
numerator -(i/m) = (-i) div ( (-i) gcd m )
proof
-(i/m) = (-i)/m;
hence thesis by Th15;
end;
theorem
m <> 0 implies
denominator -(i/m) = m / ( (-i) gcd m ) &
numerator -(i/m) = (-i) / ( (-i) gcd m )
proof
assume
A1: m <> 0;
hence denominator -(i/m) = m div ( (-i) gcd m ) by Th17
.= m / ( (-i) gcd m ) by Th8;
thus numerator -(i/m) = (-i) div ( (-i) gcd m ) by A1,Th17
.= (-i) / ( (-i) gcd m ) by Th7;
end;
theorem Th19:
m <> 0 implies
denominator((m/i)") = m div ( m gcd i ) &
numerator((m/i)") = i div ( m gcd i )
proof
(m/i)" = i/m by XCMPLX_1:213;
hence thesis by Th15;
end;
theorem
m <> 0 implies
denominator((m/i)") = m / ( m gcd i ) &
numerator((m/i)") = i / ( m gcd i )
proof
assume
A1: m <> 0;
hence denominator((m/i)") = m div ( m gcd i ) by Th19
.= m / ( m gcd i ) by Th8;
thus numerator((m/i)") = i div ( m gcd i ) by A1,Th19
.= i / ( m gcd i ) by Th7;
end;
theorem Th21:
m <> 0 & n <> 0 implies
denominator(i/m+j/n) = (m*n) div ( (i*n+j*m) gcd (m*n) ) &
numerator(i/m+j/n) = (i*n+j*m) div ( (i*n+j*m) gcd (m*n) )
proof
assume that
A1: m <> 0 and
A2: n <> 0;
(i/m+j/n) = (i*n)/(m*n) + j/n by A2,XCMPLX_1:91
.= (i*n)/(m*n) + (j*m)/(m*n) by A1,XCMPLX_1:91
.= (i*n+j*m)/(m*n);
hence thesis by A1,A2,Th15;
end;
theorem
m <> 0 & n <> 0 implies
denominator(i/m+j/n) = (m*n) / ( (i*n+j*m) gcd (m*n) ) &
numerator(i/m+j/n) = (i*n+j*m) / ( (i*n+j*m) gcd (m*n) )
proof
assume
A1: m <> 0 & n <> 0;
hence denominator(i/m+j/n) = (m*n) div ( (i*n+j*m) gcd (m*n) ) by Th21
.= (m*n) / ( (i*n+j*m) gcd (m*n) ) by Th8;
thus numerator(i/m+j/n) = (i*n+j*m) div ( (i*n+j*m) gcd (m*n) ) by A1,Th21
.= (i*n+j*m) / ( (i*n+j*m) gcd (m*n) ) by Th7;
end;
theorem Th23:
m <> 0 & n <> 0 implies
denominator(i/m-j/n) = (m*n) div ( (i*n-j*m) gcd (m*n) ) &
numerator(i/m-j/n) = (i*n-j*m) div ( (i*n-j*m) gcd (m*n) )
proof
assume that
A1: m <> 0 and
A2: n <> 0;
(i/m-j/n) = (i*n)/(m*n) - j/n by A2,XCMPLX_1:91
.= (i*n)/(m*n) - (j*m)/(m*n) by A1,XCMPLX_1:91
.= (i*n-j*m)/(m*n);
hence thesis by A1,A2,Th15;
end;
theorem
m <> 0 & n <> 0 implies
denominator(i/m-j/n) = (m*n) / ( (i*n-j*m) gcd (m*n) ) &
numerator(i/m-j/n) = (i*n-j*m) / ( (i*n-j*m) gcd (m*n) )
proof
assume
A1: m <> 0 & n <> 0;
hence denominator(i/m-j/n) = (m*n) div ( (i*n-j*m) gcd (m*n) ) by Th23
.= (m*n) / ( (i*n-j*m) gcd (m*n) ) by Th8;
thus numerator(i/m-j/n) = (i*n-j*m) div ( (i*n-j*m) gcd (m*n) ) by A1,Th23
.= (i*n-j*m) / ( (i*n-j*m) gcd (m*n) ) by Th7;
end;
theorem Th25:
m <> 0 & n <> 0 implies
denominator((i/m)*(j/n)) = (m*n) div ( (i*j) gcd (m*n) ) &
numerator((i/m)*(j/n)) = (i*j) div ( (i*j) gcd (m*n) )
proof
(i/m)*(j/n) = (i*j)/(m*n) by XCMPLX_1:76;
hence thesis by Th15;
end;
theorem
m <> 0 & n <> 0 implies
denominator((i/m)*(j/n)) = (m*n) / ( (i*j) gcd (m*n) ) &
numerator((i/m)*(j/n)) = (i*j) / ( (i*j) gcd (m*n) )
proof
assume
A1: m <> 0 & n <> 0;
hence denominator((i/m)*(j/n)) = (m*n) div ( (i*j) gcd (m*n) ) by Th25
.= (m*n) / ( (i*j) gcd (m*n) ) by Th8;
thus numerator((i/m)*(j/n)) = (i*j) div ( (i*j) gcd (m*n) ) by A1,Th25
.= (i*j) / ( (i*j) gcd (m*n) ) by Th7;
end;
theorem Th27:
m <> 0 & n <> 0 implies
denominator((i/m)/(n/j)) = (m*n) div ( (i*j) gcd (m*n) ) &
numerator((i/m)/(n/j)) = (i*j) div ( (i*j) gcd (m*n) )
proof
(i/m)/(n/j) = (i*j)/(m*n) by XCMPLX_1:84;
hence thesis by Th15;
end;
theorem
m <> 0 & n <> 0 implies
denominator((i/m)/(n/j)) = (m*n) / ( (i*j) gcd (m*n) ) &
numerator((i/m)/(n/j)) = (i*j) / ( (i*j) gcd (m*n) )
proof
assume
A1: m <> 0 & n <> 0;
hence denominator((i/m)/(n/j)) = (m*n) div ( (i*j) gcd (m*n) ) by Th27
.= (m*n) / ( (i*j) gcd (m*n) ) by Th8;
thus numerator((i/m)/(n/j)) = (i*j) div ( (i*j) gcd (m*n) ) by A1,Th27
.= (i*j) / ( (i*j) gcd (m*n) ) by Th7;
end;
theorem
denominator(p) = denominator(p) div (numerator(p) gcd denominator(p))
proof
p = numerator(p) / denominator(p);
hence thesis by Th15;
end;
theorem
numerator(p) = numerator(p) div (numerator(p) gcd denominator(p))
proof
p = numerator(p) / denominator(p);
hence thesis by Th15;
end;
theorem Th31:
m = denominator p & i = numerator p implies
denominator(-p) = m div ( (-i) gcd m ) &
numerator(-p) = (-i) div ( (-i) gcd m )
proof
p = numerator p / denominator p;
hence thesis by Th17;
end;
theorem
m = denominator p & i = numerator p implies
denominator(-p) = m / ( (-i) gcd m ) &
numerator(-p) = (-i) / ( (-i) gcd m )
proof
assume
A1: m = denominator p & i = numerator p;
hence denominator(-p) = m div ( (-i) gcd m ) by Th31
.= m / ( (-i) gcd m ) by Th8;
thus numerator(-p) = (-i) div ( (-i) gcd m ) by A1,Th31
.= (-i) / ( (-i) gcd m ) by Th7;
end;
theorem Th33:
m = denominator p & n = numerator p & n <> 0 implies
denominator(p") = n div ( n gcd m ) &
numerator(p") = m div ( n gcd m )
proof
assume m = denominator p & n = numerator p;
then p = n/m;
hence thesis by Th19;
end;
theorem
m = denominator p & n = numerator p & n <> 0 implies
denominator(p") = n / ( n gcd m ) &
numerator(p") = m / ( n gcd m )
proof
assume
A1: m = denominator p & n = numerator p & n <> 0;
hence denominator(p") = n div ( n gcd m ) by Th33
.= n / ( n gcd m ) by Th8;
thus numerator(p") = m div ( n gcd m ) by A1,Th33
.= m / ( n gcd m ) by Th7;
end;
theorem Th35:
m = denominator p & n = denominator q &
i = numerator p & j = numerator q implies
denominator(p+q) = (m*n) div ( (i*n+j*m) gcd (m*n) ) &
numerator(p+q) = (i*n+j*m) div ( (i*n+j*m) gcd (m*n) )
proof
p = numerator p / denominator p & q = numerator q / denominator q;
hence thesis by Th21;
end;
theorem
m = denominator p & n = denominator q &
i = numerator p & j = numerator q implies
denominator(p+q) = (m*n) / ( (i*n+j*m) gcd (m*n) ) &
numerator(p+q) = (i*n+j*m) / ( (i*n+j*m) gcd (m*n) )
proof
assume
A1: m = denominator p & n = denominator q &
i = numerator p & j = numerator q;
hence denominator(p+q) = (m*n) div ( (i*n+j*m) gcd (m*n) ) by Th35
.= (m*n) / ( (i*n+j*m) gcd (m*n) ) by Th8;
thus numerator(p+q) = (i*n+j*m) div ( (i*n+j*m) gcd (m*n) ) by A1,Th35
.= (i*n+j*m) / ( (i*n+j*m) gcd (m*n) ) by Th7;
end;
theorem Th37:
m = denominator p & n = denominator q &
i = numerator p & j = numerator q implies
denominator(p-q) = (m*n) div ( (i*n-j*m) gcd (m*n) ) &
numerator(p-q) = (i*n-j*m) div ( (i*n-j*m) gcd (m*n) )
proof
p = numerator p / denominator p & q = numerator q / denominator q;
hence thesis by Th23;
end;
theorem
m = denominator p & n = denominator q &
i = numerator p & j = numerator q implies
denominator(p-q) = (m*n) / ( (i*n-j*m) gcd (m*n) ) &
numerator(p-q) = (i*n-j*m) / ( (i*n-j*m) gcd (m*n) )
proof
assume
A1: m = denominator p & n = denominator q &
i = numerator p & j = numerator q;
hence denominator(p-q) = (m*n) div ( (i*n-j*m) gcd (m*n) ) by Th37
.= (m*n) / ( (i*n-j*m) gcd (m*n) ) by Th8;
thus numerator(p-q) = (i*n-j*m) div ( (i*n-j*m) gcd (m*n) ) by A1,Th37
.= (i*n-j*m) / ( (i*n-j*m) gcd (m*n) ) by Th7;
end;
theorem Th39:
m = denominator p & n = denominator q &
i = numerator p & j = numerator q implies
denominator(p*q) = (m*n) div ( (i*j) gcd (m*n) ) &
numerator(p*q) = (i*j) div ( (i*j) gcd (m*n) )
proof
p = numerator p / denominator p & q = numerator q / denominator q;
hence thesis by Th25;
end;
theorem
m = denominator p & n = denominator q &
i = numerator p & j = numerator q implies
denominator(p*q) = (m*n) / ( (i*j) gcd (m*n) ) &
numerator(p*q) = (i*j) / ( (i*j) gcd (m*n) )
proof
assume
A1: m = denominator p & n = denominator q &
i = numerator p & j = numerator q;
hence denominator(p*q) = (m*n) div ( (i*j) gcd (m*n) ) by Th39
.= (m*n) / ( (i*j) gcd (m*n) ) by Th8;
thus numerator(p*q) = (i*j) div ( (i*j) gcd (m*n) ) by A1,Th39
.= (i*j) / ( (i*j) gcd (m*n) ) by Th7;
end;
theorem Th41:
m1 = denominator p & m2 = denominator q &
n1 = numerator p & n2 = numerator q & n2 <> 0 implies
denominator(p/q) = (m1*n2) div ( (n1*m2) gcd (m1*n2) ) &
numerator(p/q) = (n1*m2) div ( (n1*m2) gcd (m1*n2) )
proof
assume
A1: m1 = denominator p & m2 = denominator q &
n1 = numerator p & n2 = numerator q & n2 <> 0;
then p = n1/m1 & q = n2/m2;
hence thesis by A1,Th27;
end;
theorem
m1 = denominator p & m2 = denominator q &
n1 = numerator p & n2 = numerator q & n2 <> 0 implies
denominator(p/q) = (m1*n2) / ( (n1*m2) gcd (m1*n2) ) &
numerator(p/q) = (n1*m2) / ( (n1*m2) gcd (m1*n2) )
proof
assume
A1: m1 = denominator p & m2 = denominator q &
n1 = numerator p & n2 = numerator q & n2 <> 0;
hence denominator(p/q) = (m1*n2) div ( (n1*m2) gcd (m1*n2) ) by Th41
.= (m1*n2) / ( (n1*m2) gcd (m1*n2) ) by Th8;
thus numerator(p/q) = (n1*m2) div ( (n1*m2) gcd (m1*n2) ) by A1,Th41
.= (n1*m2) / ( (n1*m2) gcd (m1*n2) ) by Th7;
end;
begin :: Preliminaries about Rings and Fields
reserve R for Ring, F for Field;
set I = INT.Ring;
registration
cluster positive for Element of INT.Ring;
existence;
cluster negative for Element of INT.Ring;
existence
proof
take -(1.INT.Ring);
thus thesis;
end;
end;
registration
let a be non zero Element of F_Rat, x be Rational;
identify a" with x" when a = x;
compatibility
proof
reconsider b = x" as Element of F_Rat by RAT_1:def 2;
assume
A1: x = a;
A2: a <> 0.F_Rat;
then b * a = 1.F_Rat by A1,XCMPLX_0:def 7;
hence thesis by A2,VECTSP_1:def 10;
end;
end;
registration
let a be Element of F_Rat, b be non zero Element of F_Rat;
let x,y be Rational;
identify a/b with x/y when a = x, b = y;
compatibility;
end;
registration
let F be Field;
reduce (1.F)" to 1.F;
reducibility by EC_PF_2:2;
end;
definition
let R,S be Ring;
pred R includes_an_isomorphic_copy_of S means
ex T being strict Subring of R st T,S are_isomorphic;
end;
notation
let R,S be Ring;
synonym R includes S for R includes_an_isomorphic_copy_of S;
end;
definition
let R,S be Ring;
redefine pred R,S are_isomorphic; :: redefines are_isomorphic (RING_2, synonym) → is_ringisomorph_to (QUOFIELD, definition)
reflexivity
proof
let R be Ring;
id R is isomorphism;
hence R,R are_isomorphic;
end;
end;
theorem Lm1:
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 F is Subring of E by C0SP1:def 3;
end;
theorem Th43:
for R,S,T being Ring
st R,S are_isomorphic & S,T are_isomorphic holds R,T are_isomorphic
proof
let R,S,T be Ring;
assume
A1: R,S are_isomorphic & S,T are_isomorphic;
then consider f being Function of R,S such that
A2: f is isomorphism;
consider g being Function of S,T such that
A3: g is isomorphism by A1;
g*f is one-to-one onto by A2,A3,FUNCT_2:27;
hence thesis by A2,A3;
end;
theorem
for F being Field,
R being Subring of F holds R is Subfield of F iff R is Field
proof
let F be Field, R be Subring of F;
the carrier of R c= the carrier of F
& the addF of R = (the addF of F)||the carrier of R
& the multF of R = (the multF of F)||the carrier of R
& 1.R = 1.F & 0.R = 0.F by C0SP1:def 3;
hence thesis by EC_PF_1:def 1;
end;
theorem
for E being Field, F being strict Subfield of E holds E includes F
proof
let E be Field, F be strict 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;
then F is strict Subring of E by C0SP1:def 3;
then ex T being strict Subring of E st T,F are_isomorphic;
hence thesis;
end;
Lm2:
the carrier of F_Real is Subset of the carrier of F_Complex
& the addF of F_Real = (the addF of F_Complex) || (the carrier of F_Real)
& the multF of F_Real = (the multF of F_Complex) || (the carrier of F_Real)
& 1.F_Complex = 1.F_Real & 0.F_Complex = 0.F_Real
by NUMBERS:11,COMPLFLD:def 1,Th2,Th3;
Lm3: for u,v be Integer
for p,q be Element of INT.Ring
st u = p & v = q holds u divides v iff p divides q
proof
let u,v be Integer, p,q be Element of INT.Ring;
assume A1: u = p & v = q;
hereby assume u divides v;
then consider w being Integer such that A2: v = u * w;
reconsider r = w as Element of INT.Ring by INT_1:def 2;
q = p * r by A1,A2;
hence p divides q by GCD_1:def 1;
end;
assume p divides q;
then ex r being Element of INT.Ring st q = p * r by GCD_1:def 1;
hence u divides v by A1;
end;
Lm4: the carrier of INT.Ring c= the carrier of F_Rat
& the addF of INT.Ring = (the addF of F_Rat)||the carrier of INT.Ring
& the multF of INT.Ring = (the multF of F_Rat)||the carrier of INT.Ring
& 1.INT.Ring = 1.F_Rat & 0.INT.Ring = 0.F_Rat by NUMBERS:14,Th4,Th5;
theorem
INT.Ring is Subring of F_Rat by Lm4,C0SP1:def 3;
theorem Th47:
F_Real is Subfield of F_Complex by Lm2,EC_PF_1:2;
registration
let R be domRing;
cluster R-homomorphic for domRing;
existence
proof take R,id R; thus thesis; end;
cluster R-homomorphic for comRing;
existence
proof take R,id R; thus thesis; end;
cluster R-homomorphic for Ring;
existence
proof take R,id R; thus thesis; end;
end;
registration
let R be Field;
cluster R-homomorphic for domRing;
existence
proof take R,id R; thus thesis; end;
end;
registration
let F be Field,
R be F-homomorphic Ring,
f be Homomorphism of F,R;
cluster Image f -> almost_left_invertible;
coherence
proof
set K = Image f;
now let x be Element of K;
assume A1: x <> 0.K;
A2: the carrier of K = rng f by RING_2:def 6;
consider y being object such that
A3: y in dom f & x = f.y by A2,FUNCT_1:def 3;
reconsider y as Element of F by A3;
now assume y = 0.F;
then f.y = 0.R by RING_2:6 .= 0.K by RING_2:def 6;
hence contradiction by A3,A1;
end;
then consider a being Element of F such that
A4: a * y = 1.F by VECTSP_1:def 9;
reconsider b = f.a as Element of K by A2,FUNCT_2:4;
1.K = 1_R by RING_2:def 6
.= f.(1_F) by GROUP_1:def 13
.= f.a * f.y by A4,GROUP_6:def 6
.= ((the multF of R)||(rng f)).(b,x) by Th1,A2,A3
.= b * x by RING_2:def 6;
hence ex z be Element of K st z*x = 1.K;
end;
hence thesis;
end;
end;
registration
let F be domRing,
E be F-homomorphic domRing,
f be Homomorphism of F,E;
cluster Image f -> non degenerated;
coherence
proof
0.(Image f) = 0.E & 1.(Image f) = 1.E by RING_2:def 6;
hence 0.(Image f) <> 1.(Image f);
end;
end;
theorem Th48:
for R being Ring, E being R-homomorphic Ring, K being Subring of R
for f being Function of R,E, g being Function of K,E st
g = f|(the carrier of K) & f is additive
holds g is additive
proof
let R be Ring,
E be R-homomorphic Ring,
K be Subring of R,
f be Function of R,E,
g be Function of K,E such that
A1: g = f|(the carrier of K) and
A2: f is additive;
let x,y be Element of K;
the carrier of K c= the carrier of R by C0SP1:def 3;
then reconsider x1=x, y1=y as Element of R;
A3: x + y = ((the addF of R)||the carrier of K).(x,y) by C0SP1:def 3
.= x1 + y1 by Th1;
thus g.(x+y) = f.(x+y) by A1,FUNCT_1:49
.= f.x1 + f.y1 by A2,A3
.= g.x + f.y1 by A1,FUNCT_1:49
.= g.x + g.y by A1,FUNCT_1:49;
end;
theorem Th49:
for R being Ring, E being R-homomorphic Ring, K being Subring of R
for f being Function of R,E, g being Function of K,E st
g = f|(the carrier of K) & f is multiplicative
holds g is multiplicative
proof
let R be Ring,
E be R-homomorphic Ring,
K be Subring of R,
f be Function of R,E,
g be Function of K,E such that
A1: g = f|(the carrier of K) and
A2: f is multiplicative;
let x,y be Element of K;
the carrier of K c= the carrier of R by C0SP1:def 3;
then reconsider x1=x, y1=y as Element of R;
A3: x * y = ((the multF of R)||the carrier of K).(x,y) by C0SP1:def 3
.= x1 * y1 by Th1;
thus g.(x*y) = f.(x*y) by A1,FUNCT_1:49
.= f.x1 * f.y1 by A2,A3
.= g.x * f.y1 by A1,FUNCT_1:49
.= g.x * g.y by A1,FUNCT_1:49;
end;
theorem Th50:
for R being Ring, E being R-homomorphic Ring, K being Subring of R
for f being Function of R,E, g being Function of K,E st
g = f|(the carrier of K) & f is unity-preserving
holds g is unity-preserving
proof
let R be Ring,
E be R-homomorphic Ring,
K be Subring of R,
f be Function of R,E,
g be Function of K,E such that
A1: g = f|(the carrier of K) and
A2: f is unity-preserving;
thus g.(1_K) = f.(1_K) by A1,FUNCT_1:49
.= 1_E by A2,C0SP1:def 3;
end;
theorem
for R being Ring, E being R-homomorphic Ring, K being Subring of R holds
E is K-homomorphic
proof
let R be Ring,
E be R-homomorphic Ring,
K be Subring of R;
consider f being Function of R,E such that
A1: f is RingHomomorphism by RING_2:def 4;
the carrier of K c= the carrier of R by C0SP1:def 3; then
reconsider g = f|(the carrier of K) as Function of K,E by FUNCT_2:32;
take g;
thus thesis by A1,Th48,Th49,Th50;
end;
theorem
for R being Ring,
E being R-homomorphic Ring,
K being Subring of R,
EK being K-homomorphic Ring
for f being Homomorphism of R,E st E = EK holds f|K is Homomorphism of K,EK
proof
let R be Ring, E be R-homomorphic Ring, K be Subring of R;
let EK be K-homomorphic Ring;
let f be Homomorphism of R,E;
the carrier of K c= the carrier of R by C0SP1:def 3; then
reconsider g = f|(the carrier of K) as Function of K,E by FUNCT_2:32;
g = f|K;
hence thesis by Th48,Th49,Th50;
end;
theorem Th53:
for F being Field, E being F-homomorphic Field, K being Subfield of F
for f being Function of F,E, g being Function of K,E st
g = f|(the carrier of K) & f is additive
holds g is additive
proof
let F be Field,
E be F-homomorphic Field,
K be Subfield of F,
f be Function of F,E,
g be Function of K,E such that
A1: g = f|(the carrier of K) and
A2: f is additive;
let x,y be Element of K;
the carrier of K c= the carrier of F by EC_PF_1:def 1;
then reconsider x1 = x, y1 = y as Element of F;
A3: x + y = ((the addF of F)||the carrier of K).(x,y) by EC_PF_1:def 1
.= x1 + y1 by Th1;
thus g.(x+y) = f.(x+y) by A1,FUNCT_1:49
.= f.x1 + f.y1 by A2,A3
.= g.x + f.y1 by A1,FUNCT_1:49
.= g.x + g.y by A1,FUNCT_1:49;
end;
theorem Th54:
for F being Field, E being F-homomorphic Field, K being Subfield of F
for f being Function of F,E, g being Function of K,E st
g = f|(the carrier of K) & f is multiplicative
holds g is multiplicative
proof
let F be Field,
E be F-homomorphic Field,
K be Subfield of F,
f be Function of F,E,
g be Function of K,E such that
A1: g = f|(the carrier of K) and
A2: f is multiplicative;
let x,y be Element of K;
the carrier of K c= the carrier of F by EC_PF_1:def 1;
then reconsider x1 = x, y1 = y as Element of F;
A3: x * y = ((the multF of F)||the carrier of K).(x,y) by EC_PF_1:def 1
.= x1 * y1 by Th1;
thus g.(x*y) = f.(x*y) by A1,FUNCT_1:49
.= f.x1 * f.y1 by A2,A3
.= g.x * f.y1 by A1,FUNCT_1:49
.= g.x * g.y by A1,FUNCT_1:49;
end;
theorem Th55:
for F being Field, E being F-homomorphic Field, K being Subfield of F
for f being Function of F,E, g being Function of K,E st
g = f|(the carrier of K) & f is unity-preserving
holds g is unity-preserving
proof
let F be Field,
E be F-homomorphic Field,
K be Subfield of F,
f be Function of F,E,
g be Function of K,E such that
A1: g = f|(the carrier of K) and
A2: f is unity-preserving;
thus g.(1_K) = f.(1_K) by A1,FUNCT_1:49
.= 1_E by A2,EC_PF_1:def 1;
end;
theorem Th56:
for F being Field, E being F-homomorphic Field, K being Subfield of F holds
E is K-homomorphic
proof
let F be Field,
E be F-homomorphic Field,
K be Subfield of F;
consider f being Function of F,E such that
A1: f is RingHomomorphism by RING_2:def 4;
the carrier of K c= the carrier of F by EC_PF_1:def 1; then
reconsider g = f|(the carrier of K) as Function of K,E by FUNCT_2:32;
take g;
thus thesis by A1,Th53,Th54,Th55;
end;
theorem Th57:
for F being Field,
E being F-homomorphic Field,
K being Subfield of F,
EK being K-homomorphic Field
for f being Homomorphism of F,E st E = EK holds f|K is Homomorphism of K,EK
proof
let F be Field, E being F-homomorphic Field,K be Subfield of F;
let EK be K-homomorphic Field;
let f be Homomorphism of F,E;
the carrier of K c= the carrier of F by EC_PF_1:def 1; then
reconsider g = f|(the carrier of K) as Function of K,E by FUNCT_2:32;
g = f|K;
hence thesis by Th53,Th54,Th55;
end;
notation
let n be Nat;
synonym Z/n for INT.Ring n;
end;
registration
let n be Nat;
cluster Z/n -> finite;
coherence;
end;
registration
let n be non trivial Nat;
cluster Z/n -> non degenerated;
coherence
proof
n >= 1 + 1 by NAT_2:29;
then n > 1 by NAT_1:13;
hence thesis by INT_3:11;
end;
end;
registration
let n be positive Nat;
cluster Z/n -> Abelian add-associative right_zeroed right_complementable;
coherence
proof
n + 1 > 0 + 1 by XREAL_1:6;
then A1: n >= 1 by NAT_1:13;
per cases by A1,XXREAL_0:1;
suppose n = 1;
hence thesis by INT_3:10;
end;
suppose n > 1;
hence thesis by INT_3:11;
end;
end;
end;
registration
let n be positive Nat;
cluster Z/n -> associative well-unital distributive commutative;
coherence
proof
n + 1 > 0 + 1 by XREAL_1:6;
then A1: n >= 1 by NAT_1:13;
per cases by A1,XXREAL_0:1;
suppose n = 1;
hence thesis by INT_3:10;
end;
suppose n > 1;
hence thesis by INT_3:11;
end;
end;
end;
registration
let p be Prime;
cluster Z/p -> almost_left_invertible;
coherence;
end;
begin :: Embedding the Integers in Rings
definition
let R be add-associative right_zeroed right_complementable
non empty doubleLoopStr,
a be Element of R,
i be Integer;
func i '*' a -> Element of R means :Def2:
ex n being Nat st (i = n & it = n*a) or (i = -n & it = -(n*a));
existence
proof
i in INT by INT_1:def 2; then
consider n being Nat such that A1: i = n or i = -n by INT_1:def 1;
per cases by A1;
suppose A2: i = n;
take n * a;
thus thesis by A2;
end;
suppose A3: i = -n;
take -(n * a);
thus thesis by A3;
end;
end;
uniqueness
proof
let x1,x2 be Element of R such that
A4: ex n being Nat
st (i = n & x1 = n*a) or (i = -n & x1 = -(n*a)) and
A5: ex n being Nat
st (i = n & x2 = n*a) or (i = -n & x2 = -(n*a));
i in INT by INT_1:def 2; then
consider n being Nat such that A6: i = n or i = -n by INT_1:def 1;
per cases;
suppose A7: n = 0;
then A8: x1 = 0.R or x1 = -0.R by A6,A4,BINOM:12;
x2 = 0.R or x2 = -0.R by A6,A5,A7,BINOM:12;
hence x1 = x2 by A8;
end;
suppose A9: n <> 0;
per cases by A6;
suppose i = n;
hence x1 = x2 by A9,A5,A4;
end;
suppose i = -n;
hence x1 = x2 by A5,A9,A4;
end;
end;
end;
end;
theorem Th58:
for R being add-associative right_zeroed right_complementable
non empty doubleLoopStr,
a being Element of R holds 0 '*' a = 0.R
proof
let R be add-associative right_zeroed right_complementable
non empty doubleLoopStr,
a be Element of R;
thus 0 '*' a = 0 * a by Def2 .= 0.R by BINOM:12;
end;
theorem Th59:
for R being add-associative right_zeroed right_complementable
non empty doubleLoopStr,
a being Element of R holds 1 '*' a = a
proof
let R be add-associative right_zeroed right_complementable
non empty doubleLoopStr,
a be Element of R;
thus 1 '*' a = 1 *a by Def2 .= a by BINOM:13;
end;
theorem Th60:
for R being add-associative right_zeroed right_complementable
non empty doubleLoopStr,
a being Element of R holds (-1) '*' a = -a
proof
let R be add-associative right_zeroed right_complementable
non empty doubleLoopStr,
a being Element of R;
(-1) '*' a = - (1*a) by Def2 .= - a by BINOM:13;
hence thesis;
end;
Lm5:
for R being add-associative right_zeroed right_complementable
Abelian non empty doubleLoopStr,
a being Element of R,
i being Integer holds (i + 1) '*' a = i '*' a + a
proof
let R be add-associative right_zeroed right_complementable
Abelian non empty doubleLoopStr,
a be Element of R, i be Integer;
i in INT by INT_1:def 2; then
consider n being Nat such that A1: i = n or i = -n by INT_1:def 1;
per cases;
suppose A2: n = 0;
hence (i + 1) '*' a = 0.R + a by A1,Th59 .= (i'*'a) + a by A1,A2,Th58;
end;
suppose A3: n <> 0;
per cases by A1;
suppose A4: i = n;
then A5: i'*'a = n*a by Def2;
(n+1)*a = n*a+(1*a) by BINOM:15 .= n*a + a by BINOM:13;
hence (i + 1) '*' a = i '*' a + a by A4,A5,Def2;
end;
suppose A6: i = -n;
reconsider n1 = n-1 as Element of NAT by INT_1:3,A3;
(n1+1)*a = n1*a+1*a by BINOM:15 .= n1*a+a by BINOM:13;
then i'*'a = -(n1*a+a) by A6,Def2
.= -(n1*a) + -a by RLVECT_1:31;
then A7: i'*'a + a
= -(n1*a) + (-a + a) by RLVECT_1:def 3
.= -(n1*a) + 0.R by RLVECT_1:5;
i+1 = -(n-1) by A6;
hence (i+1) '*' a = i '*' a + a by Def2,A7;
end;
end;
end;
Lm6:
for R being add-associative right_zeroed right_complementable
Abelian non empty doubleLoopStr,
a being Element of R,
i being Integer holds (i - 1) '*' a = i '*' a - a
proof
let R be add-associative right_zeroed right_complementable
Abelian non empty doubleLoopStr,
a be Element of R, i be Integer;
i in INT by INT_1:def 2; then
consider n being Nat such that A1: i = n or i = -n by INT_1:def 1;
per cases;
suppose A2: n = 0;
hence (i - 1) '*' a = 0.R + -a by Th60,A1
.= (i'*'a) - a by A1,A2,Th58;
end;
suppose A3: n <> 0;
per cases by A1;
suppose A4: i = -n;
then i-1 = -(n+1);
hence (i - 1) '*' a = -((n+1)*a) by Def2
.= -((n*a)+(1*a)) by BINOM:15
.= -((n*a)+a) by BINOM:13
.= -(n*a) + -a by RLVECT_1:31
.= i '*' a - a by A4,Def2;
end;
suppose A5: i = n;
reconsider n1 = n-1 as Element of NAT by A3,INT_1:3;
(n1+1)*a = n1*a+1*a by BINOM:15 .= n1*a+a by BINOM:13;
then i'*'a - a = (n1*a + a) - a by A5,Def2
.= n1*a + (a + -a) by RLVECT_1:def 3
.= n1*a + 0.R by RLVECT_1:5;
hence (i-1) '*'a = i '*' a - a by A5,Def2;
end;
end;
end;
theorem Th61:
for R being add-associative right_zeroed right_complementable
Abelian non empty doubleLoopStr,
a being Element of R,
i,j being Integer holds (i + j) '*' a = i '*' a + j '*' a
proof
let R be add-associative right_zeroed right_complementable
Abelian non empty doubleLoopStr,
a be Element of R,
i,j be Integer;
defpred P[Integer] means
for k being Integer st k = $1 holds (i + k)'*'a = i'*'a + k'*'a;
now let k be Integer;
assume A1: k = 0;
hence (i + k)'*'a = i'*'a + 0.R .= i'*'a + k'*'a by A1,Th58;
end;
then A2: P[0];
A3: for u being Integer holds P[u] implies P[u - 1] & P[u + 1]
proof
let u be Integer;
assume A4: P[u];
now let k be Integer;
assume k = u-1;
then A5: (i + (k+1))'*'a = i'*'a + (k+1)'*'a by A4
.= i'*'a + (k'*'a + a) by Lm5
.= (i'*'a + k'*'a) + a by RLVECT_1:def 3;
(i + (k+1))'*'a = ((i + k)+1)'*'a
.= (i+k)'*'a + a by Lm5;
hence (i + k)'*'a = i'*'a + k'*'a by A5,RLVECT_1:8;
end;
hence P[u-1];
now let k be Integer;
assume k = u+1;
then A6: (i + (k-1))'*'a = i'*'a + (k-1)'*'a by A4
.= i'*'a + (k'*'a - a) by Lm6
.= (i'*'a + k'*'a) - a by RLVECT_1:def 3;
(i + (k-1))'*'a = ((i + k)-1)'*'a
.= (i+k)'*'a - a by Lm6;
hence (i + k)'*'a = i'*'a + k'*'a by A6,RLVECT_1:8;
end;
hence P[u+1];
end;
for i being Integer holds P[i] from INT_1:sch 4(A2,A3);
hence thesis;
end;
theorem Th62:
for R being add-associative right_zeroed right_complementable
Abelian non empty doubleLoopStr,
a being Element of R,
i being Integer holds (-i) '*' a = -(i '*' a)
proof
let R be add-associative right_zeroed right_complementable
Abelian non empty doubleLoopStr,
a be Element of R, i be Integer;
defpred P[Integer] means
for k being Integer st k = $1 holds (-k) '*' a = -(k '*' a);
now let k be Integer;
assume A1: k = 0;
hence (-k)'*'a = -0.R by Th58 .= -(k'*'a) by A1,Th58;
end;
then A2: P[0];
A3: for u being Integer holds P[u] implies P[u - 1] & P[u + 1]
proof
let u be Integer;
assume A4: P[u];
now let k be Integer;
assume A5: k = u-1;
hence (-k) '*' a= ((0-u)+1)'*'a
.= (0-u) '*' a + a by Lm5
.= -(u '*' a) + a by A4
.= -(u '*' a - a) by RLVECT_1:33
.= -(k '*' a) by Lm6,A5;
end;
hence P[u-1];
now let k be Integer;
assume A6: k = u+1;
hence (-k) '*' a= ((0-u)-1)'*'a
.= (0-u) '*' a - a by Lm6
.= -(u '*' a) - a by A4
.= -(u '*' a + a) by RLVECT_1:30
.= -(k '*' a) by Lm5,A6;
end;
hence P[u+1];
end;
for i being Integer holds P[i] from INT_1:sch 4(A2,A3);
hence thesis;
end;
theorem Th63:
for R being add-associative right_zeroed right_complementable
Abelian non empty doubleLoopStr,
a being Element of R,
i,j being Integer holds (i - j) '*' a = i '*' a - j '*' a
proof
let R be add-associative right_zeroed right_complementable
Abelian non empty doubleLoopStr,
a be Element of R, i,j be Integer;
thus (i - j) '*' a
= (i '*' a) + ((0-j) '*' a) by Th61
.= i '*' a - j '*' a by Th62;
end;
theorem Th64:
for R being add-associative right_zeroed right_complementable
Abelian non empty doubleLoopStr,
a being Element of R,
i,j being Integer holds (i * j) '*' a = i '*' (j '*' a)
proof
let R be add-associative right_zeroed right_complementable
Abelian non empty doubleLoopStr,
a be Element of R, i,j be Integer;
defpred P[Integer] means
for k being Integer st k = $1 holds (k*j) '*' a = k'*'(j '*' a);
now let k be Integer;
assume A1: k = 0;
hence (k*j) '*' a = 0.R by Th58 .= k'*'(j '*' a) by A1,Th58;
end;
then A2: P[0];
A3: for u being Integer holds P[u] implies P[u - 1] & P[u + 1]
proof
let u be Integer;
assume A4: P[u];
now let k be Integer;
assume A5: k = u-1;
hence (k*j) '*' a = (u*j-j) '*' a
.= (u * j) '*' a - j '*' a by Th63
.= u '*' (j '*' a) - j '*' a by A4
.= k '*' (j '*' a) by A5,Lm6;
end;
hence P[u-1];
now let k be Integer;
assume A6: k = u+1;
hence (k*j) '*' a = (u*j+j) '*' a
.= (u * j) '*' a + j '*' a by Th61
.= u '*' (j '*' a) + j '*' a by A4
.= k '*' (j '*' a) by A6,Lm5;
end;
hence P[u+1];
end;
for i being Integer holds P[i] from INT_1:sch 4(A2,A3);
hence thesis;
end;
theorem
for R being add-associative right_zeroed right_complementable
Abelian non empty doubleLoopStr,
a being Element of R,
i,j being Integer holds i '*' (j '*' a) = j '*' (i '*' a)
proof
let R be add-associative right_zeroed right_complementable
Abelian non empty doubleLoopStr,
a be Element of R, i,j be Integer;
thus i '*' (j '*' a) = (i * j) '*' a by Th64 .= j '*' (i '*' a) by Th64;
end;
theorem Th66:
for R being add-associative right_zeroed right_complementable
Abelian left_unital distributive non empty doubleLoopStr,
i,j being Integer holds (i * j) '*' 1.R = (i '*' 1.R) * (j '*' 1.R)
proof
let R be add-associative right_zeroed right_complementable
Abelian left_unital distributive non empty doubleLoopStr,
i,j be Integer;
defpred P[Integer] means
for k being Integer st k = $1 holds
(k * j) '*' 1.R = (k '*' 1.R) * (j '*' 1.R);
now let k be Integer;
assume A1: k = 0;
hence (k * j) '*' 1.R = 0.R * (j '*' 1.R) by Th58
.= (k '*' 1.R) * (j '*' 1.R) by A1,Th58;
end;
then A2: P[0];
A3: for u being Integer holds P[u] implies P[u - 1] & P[u + 1]
proof
let u be Integer;
assume A4: P[u];
now let k be Integer;
assume A5: k = u-1;
hence (k * j) '*' 1.R = (u*j-j) '*' 1.R
.= (u*j) '*' 1.R - (j '*' 1.R) by Th63
.= (u '*' 1.R) * (j '*' 1.R) - (j '*' 1.R) by A4
.= ((u '*' 1.R) * (j '*' 1.R)) + -(1.R * (j'*'1.R))
.= ((u '*' 1.R) * (j '*' 1.R)) + (-(1.R)) * (j '*' 1.R) by VECTSP_1:9
.= ((u '*' 1.R) + -1.R) * (j '*' 1.R) by VECTSP_1:def 3
.= ((u '*' 1.R) - (1 '*' 1.R)) * (j '*' 1.R) by Th59
.= (k '*' 1.R) * (j '*' 1.R) by Th63,A5;
end;
hence P[u-1];
now let k be Integer;
assume A6: k = u+1;
hence (k * j) '*' 1.R = (u*j+j) '*' 1.R
.= (u*j) '*' 1.R + (j '*' 1.R) by Th61
.= (u '*' 1.R) * (j '*' 1.R) + (j '*' 1.R) by A4
.= ((u '*' 1.R) * (j '*' 1.R)) + (1.R * (j '*' 1.R))
.= ((u '*' 1.R) + 1.R) * (j '*' 1.R) by VECTSP_1:def 3
.= ((u '*' 1.R) + (1 '*' 1.R)) * (j '*' 1.R) by Th59
.= (k '*' 1.R) * (j '*' 1.R) by Th61,A6;
end;
hence P[u+1];
end;
for i being Integer holds P[i] from INT_1:sch 4(A2,A3);
hence thesis;
end;
theorem
for R being Ring, S being R-homomorphic Ring, f being Homomorphism of R,S
for a being Element of R,
i being Integer holds f.(i '*' a) = i '*' f.a
proof
let R be Ring,
S be R-homomorphic Ring,
f be Homomorphism of R,S;
let a be Element of R, i be Integer;
defpred P[Integer] means
for j being Integer st j = $1 holds f.(j'*'a) = j'*'f.a;
now let j be Integer;
assume A1: j = 0;
hence f.(j'*'a) = f.(0.R) by Th58
.= 0.S by RING_2:6
.= j '*' f.a by A1,Th58;
end;
then A2: P[0];
A3: for i being Integer holds P[i] implies P[i - 1] & P[i + 1]
proof
let i be Integer;
assume A4: P[i];
now let k be Integer;
assume k = i-1;
then A5: f.((k+1)'*'a) = (k+1) '*' f.a by A4
.= (k '*' (f.a)) + (1 '*' f.a) by Th61
.= (k '*' (f.a)) + f.a by Th59;
f.((k+1)'*'a) = f.(k'*'a + 1'*'a) by Th61
.= f.(k'*'a + a) by Th59
.= f.(k'*'a) + f.a by VECTSP_1:def 20;
hence f.(k '*' a) = k '*' f.a by A5,RLVECT_1:8;
end;
hence P[i-1];
now let k be Integer;
assume k = i+1;
then A6: f.((k-1) '*' a) = (k-1) '*' f.a by A4
.= k '*' (f.a) + (-1.(INT.Ring))'*' f.a by Th61
.= k '*' (f.a) - f.a by Th60;
f.((k-1)'*'a) = f.(k'*'a + (-1.(INT.Ring))'*'a) by Th61
.= f.(k'*'a - a) by Th60
.= f.(k'*'a) - f.a by RING_2:8;
hence f.(k '*' a) = k '*' f.a by A6,RLVECT_1:8;
end;
hence P[i+1];
end;
for i being Integer holds P[i] from INT_1:sch 4(A2,A3);
hence thesis;
end;
begin :: Mono- and Isomorphisms of Rings
definition
let R,S be Ring;
attr S is R-monomorphic means :Def3:
ex f being Function of R,S st f is RingHomomorphism monomorphism;
end;
registration
let R be Ring;
cluster R-monomorphic for Ring;
existence
proof take R; take id R; thus thesis; end;
end;
registration
let R be comRing;
cluster R-monomorphic for comRing;
existence
proof take R; take id R; thus thesis; end;
cluster R-monomorphic for Ring;
existence
proof take R; take id R; thus thesis; end;
end;
registration
let R be domRing;
cluster R-monomorphic for domRing;
existence
proof take R; take id R; thus thesis; end;
cluster R-monomorphic for comRing;
existence
proof take R; take id R; thus thesis; end;
cluster R-monomorphic for Ring;
existence
proof take R; take id R; thus thesis; end;
end;
registration
let R be Field;
cluster R-monomorphic for Field;
existence
proof take R; take id R; thus thesis; end;
cluster R-monomorphic for domRing;
existence
proof take R; take id R; thus thesis; end;
cluster R-monomorphic for comRing;
existence
proof take R; take id R; thus thesis; end;
cluster R-monomorphic for Ring;
existence
proof take R; take id R; thus thesis; end;
end;
registration
let R be Ring,
S be R-monomorphic Ring;
cluster additive multiplicative unity-preserving monomorphism
for Function of R,S;
existence
proof
consider f being Function of R,S such that
A1: f is RingHomomorphism monomorphism by Def3;
take f;
thus f is additive by A1;
thus f is multiplicative by A1;
thus f is unity-preserving by A1;
thus f is monomorphism by A1;
end;
end;
definition
let R be Ring,
S be R-monomorphic Ring;
mode Monomorphism of R,S is additive multiplicative unity-preserving
monomorphism Function of R,S;
end;
registration
let R be Ring,
S be R-monomorphic Ring;
cluster -> R-monomorphic for S-monomorphic Ring;
coherence
proof
let T be S-monomorphic Ring;
(the Monomorphism of S,T) * the Monomorphism of R,S is monomorphism;
hence thesis;
end;
end;
registration
let R be Ring;
cluster -> R-homomorphic for R-monomorphic Ring;
coherence
proof
let S be R-monomorphic Ring;
ex f being Function of R,S st f is RingHomomorphism monomorphism by Def3;
hence thesis;
end;
end;
registration
let R be Ring;
let S be R-monomorphic Ring;
let f be Monomorphism of R,S;
reduce (f")" to f;
reducibility by FUNCT_1:43;
end;
theorem Th68:
for R being Ring,
S being R-homomorphic Ring, T being S-homomorphic Ring
for f being Homomorphism of R,S
for g being Homomorphism of S,T holds ker(f) c= ker(g*f)
proof
let R be Ring, S be R-homomorphic Ring, T be S-homomorphic Ring;
let f be Homomorphism of R,S; let g be Homomorphism of S,T;
now let x be object;
assume x in ker f;
then consider r being Element of R such that A1: x = r & f.r = 0.S;
(g*f).r = g.(f.r) by FUNCT_2:15 .= 0.T by A1,RING_2:6;
hence x in ker(g*f) by A1;
end;
hence thesis;
end;
theorem Th69:
for R being Ring,
S being R-homomorphic Ring, T being S-monomorphic Ring
for f being Homomorphism of R,S
for g being Monomorphism of S,T holds ker(f) = ker(g*f)
proof
let R be Ring, S be R-homomorphic Ring, T be S-monomorphic Ring;
let f be Homomorphism of R,S; let g be Monomorphism of S,T;
A1: ker g = {0.S} by RING_2:12;
now let x be object;
assume x in ker(g*f);
then consider r being Element of R such that A2: x = r & (g*f).r = 0.T;
g.(f.r) = 0.T by A2,FUNCT_2:15;
then f.r in {0.S} by A1;
then f.r = 0.S by TARSKI:def 1;
hence x in ker f by A2;
end;
then ker(g*f) c= ker f;
hence thesis by Th68;
end;
theorem Th70:
for R being Ring, S being Subring of R holds R is S-monomorphic
proof
let R be Ring, S be Subring of R;
the carrier of S c= the carrier of R by C0SP1:def 3; then
reconsider f = id S as Function of S,R by FUNCT_2:7;
A1: now let x,y be Element of S;
A2: [x,y] in [:the carrier of S, the carrier of S:];
thus f.(x+y) = ((the addF of R)||the carrier of S).(x,y) by C0SP1:def 3
.= f.x + f.y by A2,FUNCT_1:49;
end;
A3: now let x,y be Element of S;
A4: [x,y] in [:the carrier of S, the carrier of S:];
thus f.(x*y) = ((the multF of R)||the carrier of S).(x,y) by C0SP1:def 3
.= f.x * f.y by A4,FUNCT_1:49;
end;
f.(1_S) = 1_R by C0SP1:def 3; then
f is RingHomomorphism by A1,A3,VECTSP_1:def 20,GROUP_1:def 13,GROUP_6:def 6;
hence thesis;
end;
theorem Th71:
for R,S being Ring holds S is R-monomorphic Ring iff S includes R
proof
let R,S be Ring;
A1: now assume S is R-monomorphic; then
reconsider T = S as R-monomorphic Ring;
set f = the Monomorphism of R,T;
ker f = {0.R} by RING_2:12;
then A2: R/(ker f), R are_isomorphic by RING_2:17;
R/(ker f), (Image f) are_isomorphic by RING_2:15;
hence S includes R by Th43,A2;
end;
now assume S includes R;
then consider T being Subring of S such that A3: T,R are_isomorphic;
consider f being Function of R,T such that A4: f is isomorphism
by A3,QUOFIELD:def 23;
A5: f is additive multiplicative unity-preserving one-to-one by A4;
the carrier of T c= the carrier of S by C0SP1:def 3; then
reconsider g = f as Function of R,S by FUNCT_2:7;
now let x,y be Element of R;
A6: [f.x,f.y] in [:the carrier of T, the carrier of T:];
thus g.(x+y) = f.x + f.y by A5
.= ((the addF of S)||the carrier of T).(f.x,f.y)
by C0SP1:def 3
.= g.x + g.y by A6,FUNCT_1:49;
end;
then A7: g is additive;
now let x,y be Element of R;
A8: [f.x,f.y] in [:the carrier of T, the carrier of T:];
thus g.(x*y) = f.x * f.y by A5
.= ((the multF of S)||the carrier of T).(f.x,f.y)
by C0SP1:def 3
.= g.x * g.y by A8,FUNCT_1:49;
end;
then A9: g is multiplicative;
g is unity-preserving by A5,C0SP1:def 3;
hence S is R-monomorphic by A7,A9,A4;
end;
hence thesis by A1;
end;
definition
let R,S be Ring;
attr S is R-isomorphic means :Def4:
ex f being Function of R,S st f is RingHomomorphism isomorphism;
end;
registration
let R be Ring;
cluster R-isomorphic for Ring;
existence
proof take R; take id R; thus thesis; end;
end;
registration
let R be comRing;
cluster R-isomorphic for comRing;
existence
proof take R; take id R; thus thesis; end;
cluster R-isomorphic for Ring;
existence
proof take R; take id R; thus thesis; end;
end;
registration
let R be domRing;
cluster R-isomorphic for domRing;
existence
proof take R; take id R; thus thesis; end;
cluster R-isomorphic for comRing;
existence
proof take R; take id R; thus thesis; end;
cluster R-isomorphic for Ring;
existence
proof take R; take id R; thus thesis; end;
end;
registration
let R be Field;
cluster R-isomorphic for Field;
existence
proof take R; take id R; thus thesis; end;
cluster R-isomorphic for domRing;
existence
proof take R; take id R; thus thesis; end;
cluster R-isomorphic for comRing;
existence
proof take R; take id R; thus thesis; end;
cluster R-isomorphic for Ring;
existence
proof take R; take id R; thus thesis; end;
end;
registration
let R be Ring,
S be R-isomorphic Ring;
cluster additive multiplicative unity-preserving
isomorphism for Function of R,S;
existence
proof
consider f being Function of R,S such that
A1: f is RingHomomorphism isomorphism by Def4;
take f;
thus f is additive by A1;
thus f is multiplicative by A1;
thus f is unity-preserving by A1;
thus f is isomorphism by A1;
end;
end;
definition
let R be Ring,
S be R-isomorphic Ring;
mode Isomorphism of R,S is additive multiplicative unity-preserving
isomorphism Function of R,S;
end;
definition
let R be Ring;
let S be R-isomorphic Ring;
let f be Isomorphism of R,S;
redefine func f" -> Function of S,R; :: redefines " (FUNCT_1, definition)
coherence
proof
rng f = the carrier of S by FUNCT_2:def 3;
then reconsider g = f" as Function of the carrier of S,the carrier of R
by FUNCT_2:25;
g is Function of S,R;
hence thesis;
end;
end;
Lm7: for R be Ring, S be R-isomorphic Ring, f be Isomorphism of R,S
holds f" is additive multiplicative unity-preserving isomorphism
proof
let R be Ring, S be R-isomorphic Ring,
f be Isomorphism of R,S;
set g = f";
A1: rng f = the carrier of S by FUNCT_2:def 3;
now let a,b be Element of S;
consider x being object such that
A2: x in the carrier of R & a = f.x by A1,FUNCT_2:11;
reconsider x as Element of R by A2;
consider y being object such that
A3: y in the carrier of R & b = f.y by A1,FUNCT_2:11;
reconsider y as Element of R by A3;
thus g.a + g.b = x + g.(f.y) by A2,A3,FUNCT_2:26
.= x + y by FUNCT_2:26
.= g.(f.(x+y)) by FUNCT_2:26
.= g.(a+b) by A2,A3,VECTSP_1:def 20;
end;
hence A4: g is additive;
now let a,b be Element of S;
consider x being object such that
A5: x in the carrier of R & a = f.x by A1,FUNCT_2:11;
reconsider x as Element of R by A5;
consider y being object such that
A6: y in the carrier of R & b = f.y by A1,FUNCT_2:11;
reconsider y as Element of R by A6;
thus g.a * g.b = x * g.(f.y) by A5,A6,FUNCT_2:26
.= x * y by FUNCT_2:26
.= g.(f.(x*y)) by FUNCT_2:26
.= g.(a* b) by A5,A6,GROUP_6:def 6;
end;
hence A7: g is multiplicative;
1.R = g.(f.(1_R)) by FUNCT_2:26
.= g.(1_S) by GROUP_1:def 13
.= g.(1.S);
hence A8: g is unity-preserving;
now let x be object;
now assume x in the carrier of R;
then reconsider x1 = x as Element of R;
f.x1 in the carrier of S;
then A9: f.x1 in dom g by FUNCT_2:def 1;
g.(f.x1) = x1 by FUNCT_2:26;
hence x in rng g by A9,FUNCT_1:def 3;
end;
hence x in rng g iff x in the carrier of R;
end;
then g is onto by FUNCT_2:def 3,TARSKI:2;
hence thesis by A8,A4,A7;
end;
registration
let R be Ring,
S be R-isomorphic Ring;
cluster additive multiplicative unity-preserving
isomorphism for Function of S,R;
existence
proof
take (the Isomorphism of R,S)";
thus thesis by Lm7;
end;
end;
definition
let R be Ring,
S be R-isomorphic Ring;
mode Isomorphism of S,R is additive multiplicative unity-preserving
isomorphism Function of S,R;
end;
registration
let R be Ring,
S be R-isomorphic Ring;
cluster -> R-isomorphic for S-isomorphic Ring;
coherence
proof
let T be S-isomorphic Ring;
(the Isomorphism of S,T) * the Isomorphism of R,S is onto by FUNCT_2:27;
hence thesis;
end;
end;
registration
let R be Ring;
cluster -> R-monomorphic for R-isomorphic Ring;
coherence
proof
let S be R-isomorphic Ring;
the Isomorphism of R,S
is additive multiplicative unity-preserving monomorphism;
hence thesis;
end;
end;
theorem Th72:
for R being Ring, S being R-isomorphic Ring,
f being Isomorphism of R,S holds f" is Isomorphism of S,R by Lm7;
theorem
for R being Ring, S being R-isomorphic Ring holds R is S-isomorphic
proof
let R be Ring,
S be R-isomorphic Ring;
(the Isomorphism of R,S)" is additive multiplicative
unity-preserving monomorphism epimorphism by Th72;
hence thesis;
end;
registration
let R be comRing;
cluster -> commutative for R-isomorphic Ring;
coherence
proof
let S be R-isomorphic Ring;
set f = the Isomorphism of R,S;
reconsider g = f" as Isomorphism of S,R by Lm7;
A1: g" = f;
now let a,b be Element of the carrier of S;
thus a * b = f.(g.(a*b)) by A1,FUNCT_2:26
.= f.((g.a) * (g.b)) by GROUP_6:def 6
.= f.(g.(b*a)) by GROUP_6:def 6
.= b * a by A1,FUNCT_2:26;
end;
hence S is commutative;
end;
end;
registration
let R be domRing;
cluster -> non degenerated domRing-like for R-isomorphic Ring;
coherence
proof
let S be R-isomorphic Ring;
set f = the Isomorphism of R,S;
reconsider g = f" as Isomorphism of S,R by Lm7;
A1: g" = f;
now assume A2: S is degenerated;
1.R = (f").(f.(1_R)) by FUNCT_2:26
.= (f").(1_S) by GROUP_1:def 13
.= (f").(f.(0.R)) by A2,RING_2:6
.= 0.R by FUNCT_2:26;
hence contradiction;
end;
hence S is non degenerated;
now let x,y be Element of S;
assume A3: x*y = 0.S;
A4: 0.R = g.(0.S) by RING_2:6
.= g.x * g.y by A3,GROUP_6:def 6;
per cases by A4,VECTSP_2:def 1;
suppose g.x = 0.R;
then 0.S = f.(g.x) by RING_2:6 .= x by A1,FUNCT_2:26;
hence x = 0.S or y = 0.S;
end;
suppose g.y = 0.R;
then 0.S = f.(g.y) by RING_2:6 .= y by A1,FUNCT_2:26;
hence x = 0.S or y = 0.S;
end;
end;
hence thesis by VECTSP_2:def 1;
end;
end;
registration
let F be Field;
cluster -> almost_left_invertible for F-isomorphic Ring;
coherence
proof
let K be F-isomorphic Ring;
set f = the Isomorphism of F,K;
reconsider g = f" as Isomorphism of K,F by Lm7;
A1: g" = f;
now let x be Element of K;
assume A2: x <> 0.K;
now assume g.x = 0.F;
then g.x = g.(0.K) by RING_2:6;
hence contradiction by A2,FUNCT_2:19;
end;
then consider a being Element of F such that
A3: a * (g.x) = 1.F by VECTSP_1:def 9;
1.K = 1_K .= f.(1_F) by GROUP_1:def 13
.= f.a * f.(g.x) by A3,GROUP_6:def 6
.= f.a * x by A1,FUNCT_2:26;
hence ex y be Element of K st y*x = 1.K;
end;
hence thesis;
end;
end;
theorem
for E,F being Field
holds E includes F iff ex K being strict Subfield of E st K,F are_isomorphic
proof
let E,F be Field;
hereby assume A1: E includes F;
reconsider EE = E as Ring;
consider K being strict Subring of EE such that
A2: K,F are_isomorphic by A1;
ex f being Function of F,K st f is RingIsomorphism by A2,QUOFIELD:def 23;
then reconsider KK = K as F-isomorphic Ring by Def4;
the carrier of KK c= the carrier of E
& the addF of KK = (the addF of E) || the carrier of KK
& the multF of KK = (the multF of E) || the carrier of KK
& 1.E = 1.KK & 0.E = 0.KK by C0SP1:def 3;
then KK is strict Subfield of E by EC_PF_1:def 1;
hence ex K being strict Subfield of E st K,F are_isomorphic by A2;
end;
given K being strict Subfield of E such that A3: K,F are_isomorphic;
the carrier of K c= the carrier of E
& the addF of K = (the addF of E) || the carrier of K
& the multF of K = (the multF of E) || the carrier of K
& 1.E = 1.K & 0.E = 0.K by EC_PF_1:def 1;
then K is strict Subring of E by C0SP1:def 3;
hence E includes F by A3;
end;
begin :: Characteristic of Rings
definition
let R be Ring;
func Char R -> Nat means :Def5:
(it '*' 1.R = 0.R & it <> 0 &
for m being positive Nat st m < it holds m '*' 1.R <> 0.R) or
(it = 0 &
for m being positive Nat holds m '*' 1.R <> 0.R);
existence
proof
per cases;
suppose A1: for m being positive Nat holds m '*' 1.R <> 0.R;
take 0;
thus thesis by A1;
end;
suppose A2: ex m being positive Nat st m '*' 1.R = 0.R;
defpred P[Nat] means $1 <> 0 & $1 '*' 1.R = 0.R;
A3: ex k being Nat st P[k] by A2;
ex k being Nat st P[k] & for n being Nat st P[n] holds k <= n
from NAT_1:sch 5(A3);
then consider k being Nat such that
A4: P[k] & for n being Nat st P[n] holds k <= n;
take k;
thus thesis by A4;
end;
end;
uniqueness
proof
let n1,n2 be Nat such that
A5:
(n1 '*' 1.R = 0.R & n1 <> 0 &
for m being positive Nat st m < n1 holds m '*' 1.R <> 0.R) or
(n1 = 0 &
for m being positive Nat holds m '*' 1.R <> 0.R) and
A6:
(n2 '*' 1.R = 0.R & n2 <> 0 &
for m being positive Nat st m < n2 holds m '*' 1.R <> 0.R) or
(n2 = 0 &
for m being positive Nat holds m '*' 1.R <> 0.R);
per cases;
suppose n1 = 0;
hence thesis by A5,A6;
end;
suppose n1 <> 0;
not(n1 < n2) & not(n2 < n1) by A6,A5;
hence n1 = n2 by XXREAL_0:1;
end;
end;
end;
definition
let n be Nat;
let R be Ring;
attr R is n-characteristic means :Def6:
Char R = n;
end;
Lm8: for i be Integer holds i '*' 1.(INT.Ring) = i
proof
let i be Integer;
set R = INT.Ring;
defpred P[Integer] means
for k being Integer st k = $1 holds k = k '*' 1.R;
0 '*' 1.R = 0.R by Th58;
then A1: P[0];
A2: now let u be Integer;
assume A3: P[u];
(u-1) '*' 1.R = u '*' 1.R - 1.R by Lm6
.= u - 1 by A3;
hence P[u-1];
(u+1) '*' 1.R = u '*' 1.R + 1.R by Lm5
.= u + 1 by A3;
hence P[u+1];
end;
for k being Integer holds P[k] from INT_1:sch 4(A1,A2);
hence i '*' 1.(INT.Ring) = i;
end;
theorem Th75:
Char(INT.Ring) = 0
proof
for n be positive Nat holds n'*'1.INT.Ring<>0.INT.Ring by Lm8;
hence thesis by Def5;
end;
theorem Th76:
for n being positive Nat holds Char(Z/n) = n
proof
let n be positive Nat;
set R = Z/n;
per cases by NAT_1:25;
suppose A1: n = 1;
then A2: 1 '*' 1.R = 0.R by Th59,INT_3:10;
for n being positive Nat st n<1 holds n'*'1.R <>0.R by NAT_1:14;
hence thesis by A2,A1,Def5;
end;
suppose A3: n > 1;
reconsider m = n-1 as Nat;
n-1 < n-0 by XREAL_1:15; then
reconsider mm = m as Element of Segm(n) by NAT_1:44;
reconsider e = 1 as Element of Segm(n) by A3,NAT_1:44;
A4: 1 '*' 1.R = 1.R by Th59 .= 1 by INT_3:14,A3;
A5: for k being Nat st k <= m holds k '*' 1.R = k
proof
let k be Nat;
assume A6: k <= m;
defpred P[Nat] means ($1) '*' 1.R = ($1);
reconsider u = m as Element of NAT by INT_1:3;
0 '*' 1.R = 0.R by Th58
.= 0 by NAT_1:44,SUBSET_1:def 8;
then A7: P[0];
A8: for k being Element of NAT st 0<=k & k<u holds P[k] implies P[k+1]
proof
let k be Element of NAT;
assume A9: 0 <= k & k < u;
assume A10: P[k];
reconsider z = k '*' 1.R as Element of Segm(n);
A11: k+1 < m+1 by A9,XREAL_1:6;
(k+1) '*' 1.R = (k '*' 1.R) + 1.R by Lm5
.= (k '*' 1.R) + (1 '*' 1.R) by Th59
.= k+1 by INT_3:7,A11,A10,A4;
hence P[k+1];
end;
A12: for i being Element of NAT st 0 <= i & i <= u holds P[i]
from INT_1:sch 7(A7,A8);
k is Element of NAT by INT_1:3;
hence thesis by A12,A6;
end;
A13: n '*' 1.R = (m+1) '*' 1.R
.= (m '*' 1.R) + 1.R by Lm5
.= (m '*' 1.R) + (1 '*' 1.R) by Th59
.= (addint(n)).(mm,e) by A4,A5
.= (m+1) mod n by GR_CY_1:def 4
.= 0 by INT_1:50
.= 0.R by NAT_1:44,SUBSET_1:def 8;
now let k be positive Nat;
assume k < n;
then k < m+1;
then A14: k <= m by NAT_1:13;
now assume k '*' 1.R = 0.R;
then k = 0.R by A5,A14
.= 0 by NAT_1:44,SUBSET_1:def 8;
hence contradiction;
end;
hence k '*' 1.R <> 0.R;
end;
hence thesis by A13,Def5;
end;
end;
registration
cluster INT.Ring -> 0-characteristic;
coherence by Th75;
end;
registration
let n be positive Nat;
cluster Z/n -> n-characteristic;
coherence by Th76;
end;
registration
let n be Nat;
cluster n-characteristic for comRing;
existence
proof
per cases;
suppose n = 0;
hence thesis by Th75;
end;
suppose n <> 0;
then reconsider k = n as positive Nat;
Char(Z/k) = k by Th76;
hence thesis;
end;
end;
end;
registration
let n be positive Nat;
let R be n-characteristic Ring;
cluster Char R -> positive;
coherence by Def6;
end;
definition
let R be Ring;
func CharSet R -> Subset of NAT equals
{ n where n is positive Nat : n '*' 1.R = 0.R };
coherence
proof
set M = {n where n is positive Nat : n '*' 1.R = 0.R};
now let x be object;
assume x in M;
then consider k being positive Nat such that
A1: x = k & k '*' 1.R = 0.R;
thus x in NAT by A1,ORDINAL1:def 12;
end;
then M c= NAT;
hence thesis;
end;
end;
registration
let n be positive Nat,
R be n-characteristic Ring;
cluster CharSet R -> non empty;
coherence
proof
Char R = n by Def6;
then n '*' 1.R = 0.R & n <> 0 & for m being positive Nat
st m < n holds m '*' 1.R <> 0.R by Def5;
then n in {k where k is positive Nat : k '*' 1.R = 0.R};
hence thesis;
end;
end;
theorem Th77:
for R being Ring holds Char R = 0 iff CharSet R = {}
proof
let R be Ring;
A1: now assume A2: Char R = 0;
now let x be object;
assume x in CharSet R;
then ex n being positive Nat st x = n & n '*' 1.R = 0.R;
hence contradiction by A2,Def5;
end;
hence CharSet R = {} by XBOOLE_0:def 1;
end;
now assume A3: CharSet R = {};
now assume ex m being positive Nat st m '*' 1.R = 0.R;
then consider m being positive Nat such that
A4: m '*' 1.R = 0.R;
m in {k where k is positive Nat : k '*' 1.R = 0.R} by A4;
hence contradiction by A3;
end;
hence Char R = 0 by Def5;
end;
hence thesis by A1;
end;
theorem Th78:
for n being positive Nat,
R being n-characteristic Ring holds Char R = min(CharSet R)
proof
let n be positive Nat,
R be n-characteristic Ring;
set M = CharSet R;
A1: n = Char R by Def6;
n '*' 1.R = 0.R & n <> 0 & for m being positive Nat
st m < n holds m '*' 1.R <> 0.R by A1,Def5;
then A2: n in M;
now let x be ExtReal;
assume x in M;
then consider m being positive Nat such that
A3: x = m & m '*' 1.R = 0.R;
thus n <= x by A3,A1,Def5;
end;
hence thesis by A2,A1,XXREAL_2:def 7;
end;
theorem Th79:
for R being Ring holds Char R = min*(CharSet R)
proof
let R be Ring;
set n = Char R;
per cases;
suppose A1: Char R = 0;
then CharSet R = {} by Th77;
hence thesis by A1,NAT_1:def 1;
end;
suppose Char R > 0;
then reconsider n1 = n as positive Nat;
reconsider R1 = R as n1-characteristic Ring by Def6;
A2: Char R = Char R1 = min(CharSet R1) by Th78;
then A3: n in CharSet R by XXREAL_2:def 7;
for k being Nat st k in CharSet R holds n <= k by A2,XXREAL_2:def 7;
hence thesis by A3,NAT_1:def 1;
end;
end;
theorem
for p being Prime,
R being p-characteristic Ring,
n being positive Nat
holds n is Element of CharSet R iff p divides n
proof
let p be Prime, R be p-characteristic Ring, j be positive Nat;
A1: Char R = p by Def6; then
A2: p '*' 1.R = 0.R by Def5;
A3: now assume A4: j is Element of CharSet R;
A5: ((j div p) * p) '*' 1.R = ((j div p) '*' 1.R) * (p '*' 1.R) by Th66
.= 0.R by A2;
A6: j '*' 1.R = ((j div p) * p + (j mod p)) '*' 1.R by INT_1:59
.= 0.R + ((j mod p) '*' 1.R) by A5,Th61
.= (j mod p) '*' 1.R;
j in {k where k is positive Nat : k '*' 1.R = 0.R} by A4;
then consider l being positive Nat such that A7: l = j & l '*' 1.R = 0.R;
now assume j mod p > 0;
then reconsider l = j mod p as positive Nat;
A8: l in {k where k is positive Nat : k '*' 1.R = 0.R} by A7,A6;
p = min(CharSet R) by A1,Th78;
then p <= (j mod p) by A8,XXREAL_2:def 7;
hence contradiction by INT_1:58;
end;
then A9: j mod p = 0;
j = (j div p) * p + (j mod p) by INT_1:59;
hence p divides j by A9;
end;
now assume p divides j;
then consider i being Integer such that A10: j = p * i;
j '*' 1.R = (p '*' 1.R) * (i '*' 1.R) by A10,Th66
.= 0.R * (i '*' 1.R) by A1,Def5
.= 0.R;
then j in {k where k is positive Nat : k '*' 1.R = 0.R};
hence j is Element of CharSet R;
end;
hence thesis by A3;
end;
definition
let R be Ring;
func canHom_Int R -> Function of INT.Ring,R means :Def8:
for x being Element of INT.Ring holds it.x = x '*' 1.R;
existence
proof
defpred P[object,object] means
ex a being Element of I st $1 = a & $2 = a '*' 1.R;
A1: for x being object st x in the carrier of I
ex y being object st y in the carrier of R & P[x,y]
proof
let x be object;
assume x in the carrier of I;
then reconsider a = x as Element of I;
take a '*' 1.R;
thus thesis;
end;
consider g being Function of the carrier of I,the carrier of R
such that
A2: for x being object st x in the carrier of I holds P[x,g.x]
from FUNCT_2:sch 1(A1);
now let x be Element of I;
consider a being Element of I such that A3: x = a & g.x = a'*'1.R by A2;
thus g.x = x'*'1.R by A3;
end;
then consider f being Function of I,R such that
A4: for x being Element of I holds f.x = x'*'1.R;
take f;
thus thesis by A4;
end;
uniqueness
proof
let g1,g2 be Function of I,R such that
A5: for a being Element of I holds g1.a = a '*' 1.R and
A6: for a being Element of I holds g2.a = a '*' 1.R;
let a be Element of I;
thus g1.a = a '*' 1.R by A5
.= g2.a by A6;
end;
end;
registration
let R be Ring;
cluster canHom_Int R -> additive multiplicative unity-preserving;
coherence
proof
set g = canHom_Int R;
now let x,y be Element of I;
thus g.(x+y) = (x+y) '*' 1.R by Def8
.= (x'*'1.R) + (y'*'1.R) by Th61
.= g.x + (y'*'1.R) by Def8
.= g.x + g.y by Def8;
end;
hence g is additive;
now let x,y be Element of I;
reconsider x1=x, y1=y as Integer;
thus g.(x*y) = (x*y) '*' 1.R by Def8
.= (x1'*'1.R) * (y1'*'1.R) by Th66
.= g.x * (y'*'1.R) by Def8
.= (g.x) * (g.y) by Def8;
end;
hence g is multiplicative;
g.(1_I) = 1 '*' 1.R by Def8 .= 1_R by Th59;
hence thesis;
end;
end;
registration
cluster -> (INT.Ring)-homomorphic for Ring;
coherence
proof
let R be Ring;
canHom_Int R is additive multiplicative unity-preserving;
hence thesis;
end;
end;
theorem Th81:
for R being Ring,
n being non negative Element of INT.Ring
holds Char R = n iff ker(canHom_Int R) = {n}-Ideal
proof
let R be Ring,
n be non negative Element of INT.Ring;
set f = canHom_Int R;
reconsider k = n as Integer;
A1: now assume A2: Char R = n;
reconsider k as Nat;
per cases;
suppose A3: k = 0;
then A4: {n}-Ideal = {0.I} by IDEAL_1:47;
now let x1,x2 be object;
assume A5: x1 in the carrier of I &
x2 in the carrier of I & f.x1 = f.x2;
then reconsider y1=x1,y2=x2 as Integer;
y1 '*' 1.R = f.y1 by A5,Def8 .= y2 '*' 1.R by A5,Def8;
then A6: 0.R = y1 '*' 1.R - y2 '*' 1.R by RLVECT_1:15
.= (y1 - y2) '*' 1.R by Th63;
now assume y1 - y2 <> 0;
then A7: y1 <> y2;
ex n being positive Nat st n '*' 1.R = 0.R
proof
per cases by A7,XREAL_1:55;
suppose y1 - y2 > 0;
hence thesis by A6;
end;
suppose A8: 0 < y2 - y1;
(y2-y1) '*' 1.R = (0-(y1-y2)) '*' 1.R
.= -((y1 - y2) '*' 1.R) by Th62
.= 0.R by A6;
hence thesis by A8;
end;
end;
hence contradiction by Def5,A2,A3;
end;
hence x1 = x2;
end;
then f is one-to-one by FUNCT_2:19;
hence ker(canHom_Int R) = {n}-Ideal by A4,RING_2:12;
end;
suppose A9: k > 0;
A10: now let x be object;
assume x in {n}-Ideal;
then x in the set of all n*r where r is Element of I by IDEAL_1:64;
then consider r being Element of I such that A11: x = n * r;
f.x = f.n * f.r by A11,GROUP_6:def 6
.= (n'*'1.R) * f.r by Def8
.= 0.R * f.r by A2,Def5,A9
.= 0.R;
hence x in ker(canHom_Int R) by A11;
end;
now let x be object;
assume x in ker(canHom_Int R);
then consider y being Element of I such that
A12: y = x & f.y = 0.R;
reconsider d = y div n, r = y mod n as Element of I;
A13: y mod n < n by A9,INT_1:58;
A14: y = d * n + r by A9,INT_1:59;
(y mod n) in NAT by INT_1:3;
reconsider rr = y mod n as Nat;
0.R = f.(d * n) + f.r by A12,A14,VECTSP_1:def 20
.= f.d * f.n + f.r by GROUP_6:def 6
.= f.d * (n'*'1.R) + f.r by Def8
.= (f.d * 0.R) + f.r by Def5,A9,A2
.= (y mod n) '*' 1.R by Def8;
then rr = 0 by A13,Def5,A2;
then y in the set of all n*a where a is Element of I by A14;
hence x in {n}-Ideal by A12,IDEAL_1:64;
end;
hence ker(canHom_Int R) = {n}-Ideal by A10,TARSKI:2;
end;
end;
now assume A15: ker(canHom_Int R) = {n}-Ideal;
per cases;
suppose A16: n = 0;
then ker(canHom_Int R) = {0.I} by A15,IDEAL_1:47;
then A17: canHom_Int R is monomorphism by RING_2:12;
now assume ex n being positive Nat st n '*' 1.R = 0.R;
then consider k being positive Nat such that
A18: k '*' 1.R = 0.R;
reconsider kk = k as Element of I by INT_1:def 2;
f.kk = 0.R by A18,Def8 .= f.(0.I) by RING_2:6;
hence contradiction by A17,FUNCT_2:19;
end;
hence Char R = n by A16,Def5;
end;
suppose A19: n <> 0;
reconsider l = n as positive Nat by A19;
n in ker(canHom_Int R) by A15,IDEAL_1:66;
then consider y being Element of I such that
A20: y = n & f.y = 0.R;
f.n = n '*' 1.R by Def8;
then A21: n in CharSet R by A19,A20;
now let x be Nat;
assume x in CharSet R;
then consider m being positive Nat such that
A22: x = m & m '*' 1.R = 0.R;
reconsider a = m as Element of I by INT_1:def 2;
f.a = 0.R by A22,Def8;
then a in {n}-Ideal by A15;
then a in the set of all n*r where r is Element of I by IDEAL_1:64;
then consider q being Element of I such that A23: a = n * q;
reconsider qq = q as Integer;
now assume n > a;
then l/l > (l * qq)/l by A23,XREAL_1:74;
then 1 > qq * (l/l) by XCMPLX_1:60;
then 1 > qq * 1 by XCMPLX_1:60;
then qq + 1 <= 1 by INT_1:7;
then (qq + 1) - 1 <= 1 - 1 by XREAL_1:13;
hence contradiction by A23;
end;
hence n <= x by A22;
end;
then n = min*(CharSet R) by A21,NAT_1:def 1;
hence Char R = n by Th79;
end;
end;
hence thesis by A1;
end;
theorem Th82:
for R being Ring holds Char R = 0 iff canHom_Int R is monomorphism
proof
let R be Ring; set f = canHom_Int R;
canHom_Int R is monomorphism iff ker f = {0.INT.Ring} by RING_2:12; then
canHom_Int R is monomorphism iff ker f = {0.INT.Ring}-Ideal by IDEAL_1:47;
hence thesis by Th81;
end;
registration
let R be 0-characteristic Ring;
cluster canHom_Int R -> monomorphism;
coherence
proof
Char R = 0 by Def6;
hence thesis by Th82;
end;
end;
registration
let R be 0-characteristic Ring;
cluster additive multiplicative unity-preserving monomorphism for
Function of INT.Ring,R;
existence
proof
take canHom_Int R;
thus thesis;
end;
end;
theorem Th83:
for R being Ring, f being Homomorphism of INT.Ring,R holds f = canHom_Int R
proof
let R be Ring, f being Homomorphism of INT.Ring,R;
set g = canHom_Int R;
A1: dom f = the carrier of I by FUNCT_2:def 1
.= dom g by FUNCT_2:def 1;
defpred P[Integer] means
for j be Integer st j = $1 holds f.j = j '*' 1.R;
now let j be Integer;
assume A2: j = 0;
hence f.j = f.(0.INT.Ring)
.= 0.R by RING_2:6
.= j '*' 1.R by A2,Th58;
end;
then A3: P[0];
A4: for u being Integer holds P[u] implies P[u - 1] & P[u + 1]
proof
let u be Integer;
assume A5: P[u];
reconsider uu = u as Element of INT.Ring by INT_1:def 2;
now let k be Integer;
assume A6: k = u-1;
then k = uu - 1.I;
hence f.k = f.uu - f.(1.I) by RING_2:8
.= (uu '*' 1.R) - f.(1_I) by A5
.= (uu '*' 1.R) - 1_R by GROUP_1:def 13
.= (uu '*' 1.R) - (1 '*' 1.R) by Th59
.= k '*' 1.R by Th63,A6;
end;
hence P[u-1];
now let k be Integer;
assume A7: k = u+1;
then k = uu + 1.I;
hence f.k = f.uu + f.(1.I) by VECTSP_1:def 20
.= (uu '*' 1.R) + f.(1_I) by A5
.= (uu '*' 1.R) + 1_R by GROUP_1:def 13
.= (uu '*' 1.R) + (1 '*' 1.R) by Th59
.= k '*' 1.R by Th61,A7;
end;
hence P[u+1];
end;
A8: for i be Integer holds P[i] from INT_1:sch 4(A3,A4);
now let x be object;
assume x in dom f;
then reconsider a = x as Element of INT.Ring;
reconsider aa = a as Integer;
f.a = aa '*' 1.R by A8;
hence f.x = g.x by Def8;
end;
hence thesis by A1;
end;
theorem
for f being Homomorphism of INT.Ring,INT.Ring holds f = id INT.Ring
proof
canHom_Int INT.Ring = id INT.Ring by Th83;
hence thesis by Th83;
end;
theorem Th85:
for R being domRing holds Char R = 0 or Char R is prime
proof
let R be domRing;
set n = Char R;
now assume A1: Char R <> 0; then
A2: n '*' 1.R = 0.R & n <> 0 & for m being positive Nat
st m < n holds m '*' 1.R <> 0.R by Def5;
per cases by A1,NAT_1:25;
suppose n = 1;
hence Char R is prime by A2,Th59;
end;
suppose A3: n > 1;
now assume not (n is prime);
then consider m being Nat such that
A4: m divides n & not(m = 1 or m = n) by A3,INT_2:def 4;
consider u being Integer such that A5: m * u = n by A4;
u > 0 by A5,A3;
then u in NAT by INT_1:3;
then reconsider u as positive Nat by A5,A3;
m <> 0 by A5,A3;
then reconsider m as positive Nat;
0.R = (m * u) '*' 1.R by A5,Def5 .= (m '*' 1.R) * (u '*' 1.R) by Th66;
then A6: (m '*' 1.R) = 0.R or (u '*' 1.R) = 0.R by VECTSP_2:def 1;
m <= n by A3,A4,INT_2:27;
then A7: m < n by A4,XXREAL_0:1;
A8: u <= n by A3,INT_2:27,A5,INT_1:def 3;
now assume u = n;
then n/n = (m * n) / n by A5 .= m * (n/n)
.= m*1 by A1,XCMPLX_1:60;
hence contradiction by A4,A3,XCMPLX_1:60;
end;
then u < n by A8,XXREAL_0:1;
hence contradiction by A7,A6,Def5;
end;
hence Char R is prime;
end;
end;
hence thesis;
end;
theorem
for R being Ring, S being R-homomorphic Ring holds Char S divides Char R
proof
let R be Ring, S be R-homomorphic Ring;
set n = Char S, m = Char R;
reconsider n1=n,m1=m as Element of INT.Ring by INT_1:def 2;
(the Homomorphism of R,S) * canHom_Int(R) = canHom_Int(S) by Th83;
then ker(canHom_Int(R)) c= ker(canHom_Int(S)) by Th68;
then {m1}-Ideal c= ker(canHom_Int(S)) by Th81;
then {m1}-Ideal c= {n1}-Ideal by Th81;
then n1 divides m1 by RING_2:19;
hence thesis by Lm3;
end;
theorem Th87:
for R being Ring, S being R-monomorphic Ring holds Char S = Char R
proof
let R be Ring, S be R-monomorphic Ring;
set n = Char S, m = Char R;
reconsider n1 = n, m1 = m as Element of INT.Ring by INT_1:def 2;
(the Monomorphism of R,S) * canHom_Int(R) = canHom_Int(S) by Th83;
then ker(canHom_Int(R)) = ker(canHom_Int(S)) by Th69;
then A1: {m1}-Ideal = ker(canHom_Int(S)) by Th81;
then A2: n divides m & m divides n by Th81;
per cases;
suppose A3: m = 0;
then A4: {0.INT.Ring} = {m1}-Ideal by IDEAL_1:47
.= {n1}-Ideal by A1,Th81;
now assume A5: n <> 0.INT.Ring;
n1 in {n1}-Ideal by IDEAL_1:66;
hence contradiction by A5,A4,TARSKI:def 1;
end;
hence n = m by A3;
end;
suppose A6: m > 0;
consider u being Integer such that A7: m = n * u by A2;
consider v being Integer such that A8: n = m * v by A2;
m = (m * v) * u by A7,A8 .= m * (v * u);
then m/m = (v*u)*(m/m) by XCMPLX_1:74;
then m/m = (u * v) * 1 by A6,XCMPLX_1:60;
then A9: u * v = 1 by A6,XCMPLX_1:60;
u <> -1 by A7,A6;
then u = 1 & v = 1 by A9,INT_1:9;
hence thesis by A7;
end;
end;
theorem Th88:
for R being Ring, S being Subring of R holds Char S = Char R
proof
let R be Ring, S be Subring of R;
R is S-monomorphic by Th70;
hence thesis by Th87;
end;
registration
let n be Nat;
let R be n-characteristic Ring;
cluster R-monomorphic -> n-characteristic for Ring;
coherence
proof
let S be Ring;
assume A1: S is R-monomorphic;
Char R = n by Def6;
hence thesis by A1,Th87;
end;
cluster -> n-characteristic for Subring of R;
coherence
proof
let S be Subring of R;
Char R = n by Def6;
hence thesis by Th88;
end;
end;
Lm9: for n be Nat holds n '*' 1.(F_Complex) = n
proof
let n be Nat;
defpred P[Nat] means $1 '*' 1.(F_Complex) = $1;
0 '*' 1.(F_Complex) = 0.(F_Complex) by Th58; then
A1: P[0] by COMPLFLD:def 1;
A2: now let k be Nat;
assume A3: P[k];
reconsider kk = k as Nat;
(kk+1) '*' 1.(F_Complex)
= kk '*' 1.(F_Complex) + 1.(F_Complex) by Lm5
.= kk + 1 by A3,COMPLFLD:def 1;
hence P[k+1];
end;
for k be Nat holds P[k] from NAT_1:sch 2(A1,A2);
hence thesis;
end;
registration
cluster F_Complex -> 0-characteristic;
coherence
proof
now let n be positive Nat;
n '*' 1.(F_Complex) = n by Lm9;
hence n '*' 1.(F_Complex) <> 0.(F_Complex) by COMPLFLD:def 1;
end;
hence thesis by Def5;
end;
end;
registration
cluster F_Real -> 0-characteristic;
coherence
proof
F_Real is Subring of F_Complex by Th47,Lm1;
hence thesis;
end;
end;
registration
cluster F_Rat -> 0-characteristic;
coherence
proof
F_Rat is Subring of F_Real by Lm1,GAUSSINT:14;
hence thesis;
end;
end;
registration
cluster 0-characteristic for Field;
existence
proof
take F_Real;
thus thesis;
end;
end;
registration
let p be Prime;
cluster p-characteristic for Field;
existence
proof
take Z/p;
thus thesis;
end;
end;
registration
let p be Prime;
let R be p-characteristic domRing;
cluster Char R -> prime;
coherence by Th85;
end;
registration
let F be 0-characteristic Field;
cluster -> 0-characteristic for Subfield of F;
coherence
proof
let S be Subfield of F;
S is Subring of F by Lm1;
hence thesis;
end;
end;
registration
let p be Prime;
let F be p-characteristic Field;
cluster -> p-characteristic for Subfield of F;
coherence
proof
let S be Subfield of F;
S is Subring of F by Lm1;
hence thesis;
end;
end;
begin :: Prime Fields
definition
let F be Field;
func carrier/\ F -> Subset of F equals
{x where x is Element of F : for K being Subfield of F holds x in K};
coherence
proof
now let x be object;
assume x in {x where x is Element of F :
for K being Subfield of F holds x in K};
then consider x1 being Element of F such that
A1: x1 = x & for K being Subfield of F holds x1 in K;
thus x in the carrier of F by A1;
end;
hence thesis by TARSKI:def 3;
end;
end;
definition
let F be Field;
func PrimeField F -> strict doubleLoopStr means :Def10:
the carrier of it = carrier/\ F &
the addF of it = (the addF of F)||(carrier/\ F) &
the multF of it = (the multF of F)||(carrier/\ F) &
the OneF of it = 1.F &
the ZeroF of it = 0.F;
existence
proof
set C = carrier/\ F;
set f = the addF of F;
C is f-binopclosed
proof
let x be set;
assume x in [:C,C:];
then consider x1,x2 being object such that
A1: x1 in C and
A2: x2 in C and
A3: x = [x1,x2] by ZFMISC_1:def 2;
consider y1 being Element of F such that
A4: x1 = y1 and
A5: for K being Subfield of F holds y1 in K by A1;
consider y2 being Element of F such that
A6: x2 = y2 and
A7: for K being Subfield of F holds y2 in K by A2;
now
let K be Subfield of F;
y1 in K & y2 in K by A5,A7;
then reconsider a1 = y1, a2 = y2 as Element of K;
the addF of K = f || the carrier of K by EC_PF_1:def 1;
then (the addF of K).(a1,a2) = f.(a1,a2) by Th1;
hence f.(y1,y2) in K;
end;
hence f.x in C by A3,A4,A6;
end;
then reconsider C as Preserv of the addF of F;
set f = the multF of F;
C is f-binopclosed
proof
let x be set;
assume x in [:C,C:];
then consider x1,x2 being object such that
A8: x1 in C and
A9: x2 in C and
A10: x = [x1,x2] by ZFMISC_1:def 2;
consider y1 being Element of F such that
A11: x1 = y1 and
A12: for K being Subfield of F holds y1 in K by A8;
consider y2 being Element of F such that
A13: x2 = y2 and
A14: for K being Subfield of F holds y2 in K by A9;
now
let K be Subfield of F;
y1 in K & y2 in K by A12,A14;
then reconsider a1 = y1, a2 = y2 as Element of K;
the multF of K = f || the carrier of K by EC_PF_1:def 1;
then (the multF of K).(a1,a2) = f.(a1,a2) by Th1;
hence f.(y1,y2) in K;
end;
hence f.x in C by A10,A11,A13;
end;
then reconsider D = C as Preserv of the multF of F;
reconsider m = (the multF of F)||D as BinOp of C;
set o = 1.F, z = 0.F;
now
let K be Subfield of F;
o = 1.K & z = 0.K by EC_PF_1:def 1;
hence o in K & z in K;
end;
then o in C & z in C;
then reconsider o,z as Element of C;
take doubleLoopStr (# C,(the addF of F)||C,m,o,z #);
thus thesis;
end;
uniqueness;
end;
registration
let F be Field;
cluster PrimeField F -> non degenerated;
coherence
proof
0.PrimeField F = 0.F & 1.PrimeField F = 1.F by Def10;
hence 0.PrimeField F <> 1.PrimeField F;
end;
end;
Lm10:
for x being Element of PrimeField F holds x is Element of F
proof
let x be Element of PrimeField F;
A1: the carrier of PrimeField F = carrier/\ F by Def10;
x in the carrier of PrimeField F;
hence thesis by A1;
end;
Lm11:
for a,b being Element of F
for x,y being Element of PrimeField F st a = x & b = y holds
a+b = x+y
proof
let a,b be Element of F;
let x,y be Element of PrimeField F such that
A1: a = x & b = y;
the carrier of PrimeField F = carrier/\ F by Def10;
hence a+b = (the addF of F)||(carrier/\ F).(x,y) by A1,Th1
.= x+y by Def10;
end;
Lm12:
for a,b being Element of F
for x,y being Element of PrimeField F st a = x & b = y holds
a*b = x*y
proof
let a,b be Element of F;
let x,y be Element of PrimeField F such that
A1: a = x & b = y;
the carrier of PrimeField F = carrier/\ F by Def10;
hence a*b = (the multF of F)||(carrier/\ F).(x,y) by A1,Th1
.= x*y by Def10;
end;
registration
let F be Field;
cluster PrimeField F -> Abelian
add-associative right_zeroed right_complementable;
coherence
proof
set P = PrimeField F;
A1: 0.P = 0.F by Def10;
A2: the carrier of PrimeField F = carrier/\ F by Def10;
hereby
let x,y be Element of P;
reconsider a = x, b = y as Element of F by Lm10;
thus x+y = a+b by Lm11
.= y+x by Lm11;
end;
hereby
let x,y,z be Element of P;
reconsider a = x, b = y, c = z as Element of F by Lm10;
A3: y+z = b+c by Lm11;
x+y = a+b by Lm11;
hence x+y+z = a+b+c by Lm11
.= a+(b+c) by RLVECT_1:def 3
.= x+(y+z) by A3,Lm11;
end;
hereby
let x be Element of P;
reconsider a = x as Element of F by Lm10;
thus x+0.P = a+0.F by A1,Lm11
.= x;
end;
let x be Element of P;
reconsider a = x as Element of F by Lm10;
x in carrier/\ F by A2;
then consider x1 being Element of F such that
A4: x = x1 and
A5: for K being Subfield of F holds x1 in K;
now
let K be Subfield of F;
x1 in K by A5;
then reconsider t = x1 as Element of K;
-t = -x1 by GAUSSINT:19;
hence -x1 in K;
end;
then -x1 in carrier/\ F;
then reconsider y = -x1 as Element of P by Def10;
take y;
thus x+y = a+-x1 by Lm11
.= 0.P by A1,A4,RLVECT_1:5;
end;
end;
registration
let F be Field;
cluster PrimeField F -> commutative;
coherence
proof
let x,y be Element of PrimeField F;
reconsider a = x, b = y as Element of F by Lm10;
thus x*y = a*b by Lm12
.= y*x by Lm12;
end;
end;
registration
let F be Field;
cluster PrimeField F -> associative well-unital
distributive almost_left_invertible;
coherence
proof
set P = PrimeField F;
A1: 1.P = 1.F by Def10;
A2: 0.P = 0.F by Def10;
hereby
let x,y,z be Element of P;
reconsider a = x, b = y, c = z as Element of F by Lm10;
A3: y*z = b*c by Lm12;
x*y = a*b by Lm12;
hence x*y*z = a*b*c by Lm12
.= a*(b*c) by GROUP_1:def 3
.= x*(y*z) by A3,Lm12;
end;
hereby
let x be Element of P;
reconsider a = x as Element of F by Lm10;
thus x * 1.P = a * 1.F by A1,Lm12
.= x;
thus 1.P * x = 1.F * a by A1,Lm12
.= x;
end;
hereby
let x,y,z be Element of P;
reconsider a = x, b = y, c = z as Element of F by Lm10;
A4: a*b = x*y & a*c = x*z by Lm12;
y+z = b+c by Lm11;
hence x*(y+z) = a*(b+c) by Lm12
.= a*b+a*c by VECTSP_1:def 7
.= x*y+x*z by A4,Lm11;
hence (y+z)*x = y*x+z*x;
end;
let x be Element of P such that
A5: x <> 0.P;
reconsider a = x as Element of F by Lm10;
the carrier of PrimeField F = carrier/\ F by Def10;
then x in carrier/\ F;
then consider x1 being Element of F such that
A6: x = x1 and
A7: for K being Subfield of F holds x1 in K;
now
let K be Subfield of F;
x1 in K by A7;
then reconsider t = x1 as Element of K;
t" = x1" by A5,A6,A2,GAUSSINT:21;
hence x1" in K;
end;
then x1" in carrier/\ F;
then reconsider y = x1" as Element of P by Def10;
take y;
thus y*x = x1"*a by Lm12
.= 1.P by A1,A2,A5,A6,VECTSP_1:def 10;
end;
end;
definition
let F be Field;
redefine func PrimeField F -> strict Subfield of F; :: redefines PrimeField (RING_3, definition)
coherence
proof
set P = PrimeField F;
the carrier of P = carrier/\ F by Def10;
then the carrier of P is Subset of the carrier of F
& the addF of P = (the addF of F) || (the carrier of P)
& the multF of P = (the multF of F) || (the carrier of P)
& 1.P = 1.F & 0.P = 0.F by Def10;
hence thesis by EC_PF_1:2;
end;
end;
Lm13:
for F being Field, K being Subfield of F holds carrier/\ F c= the carrier of K
proof
let F be Field, K be Subfield of F;
now let x be object;
assume x in carrier/\ F;
then consider y being Element of F such that
A1: x = y & for E being Subfield of F holds y in E;
y in K by A1;
hence x in the carrier of K by A1;
end;
hence thesis;
end;
theorem Th89:
for F being Field,
E being strict Subfield of PrimeField F holds E = PrimeField F
proof
let F be Field, E be strict Subfield of PrimeField F;
set K = PrimeField F;
A1: the carrier of E c= the carrier of K
& the addF of E = (the addF of K) || the carrier of E
& the multF of E = (the multF of K) || the carrier of E
& 1.E = 1.K & 0.E = 0.K by EC_PF_1:def 1;
E is Subfield of F by EC_PF_1:5;
then carrier/\ F c= the carrier of E by Lm13;
then the carrier of E = the carrier of PrimeField F by EC_PF_1:def 1,Def10;
hence thesis by A1;
end;
theorem Th90:
for F being Field, E being Subfield of F holds PrimeField F is Subfield of E
proof
let F be Field, E be Subfield of F;
the carrier of PrimeField F c= the carrier of E
proof
let x be object;
assume x in the carrier of PrimeField F;
then x in carrier/\ F by Def10;
then ex y being Element of F st
x = y & for K being Subfield of F holds y in K;
then x in E;
hence thesis;
end;
hence thesis by EC_PF_1:6;
end;
theorem Th91:
for F,K being Field holds
K = PrimeField F iff (K is strict Subfield of F &
for E being strict Subfield of K holds E = K)
proof
let F,K be Field;
now assume A1: K is strict Subfield of F &
for E being strict Subfield of K holds E = K;
then PrimeField F is Subfield of K by Th90;
hence K = PrimeField F by A1;
end;
hence thesis by Th89;
end;
theorem Th92:
for F,K being Field holds
K = PrimeField F iff (K is strict Subfield of F &
for E being Subfield of F holds K is Subfield of E)
proof
let F,K be Field;
now assume A1: K is strict Subfield of F &
for E being Subfield of F holds K is Subfield of E;
then A2: the carrier of K c= the carrier of F
& the addF of K = (the addF of F) || the carrier of K
& the multF of K = (the multF of F) || the carrier of K
& 1.F = 1.K & 0.F = 0.K by EC_PF_1:def 1;
A3: now let x be object;
assume x in carrier/\ F;
then consider y being Element of F such that
A4: x = y & for E being Subfield of F holds y in E;
x in K by A4,A1;
hence x in the carrier of K;
end;
now let x be object;
assume A5: x in the carrier of K;
for E being Subfield of F holds x in E
proof
let E be Subfield of F;
K is Subfield of E by A1;
then the carrier of K c= the carrier of E by EC_PF_1:def 1;
hence x in E by A5;
end;
hence x in carrier/\ F by A2,A5;
end;
then the carrier of K = carrier/\ F by A3,TARSKI:2;
hence K = PrimeField F by A1,A2,Def10;
end;
hence thesis by Th90;
end;
theorem
for E being Field, F being Subfield of E holds PrimeField F = PrimeField E
proof
let E be Field, F be Subfield of E;
PrimeField F is Subfield of E by EC_PF_1:5;
then PrimeField E is Subfield of PrimeField F by Th92;
hence thesis by Th91;
end;
theorem
for F being Field holds PrimeField(PrimeField F) = PrimeField F by Th91;
registration
let F be Field;
cluster PrimeField F -> prime;
coherence
proof
for K being Field holds
K is strict Subfield of PrimeField F implies K = PrimeField F by Th91;
hence thesis by EC_PF_1:def 2;
end;
end;
theorem
for F being Field holds F is prime iff F = PrimeField F
by EC_PF_1:def 2;
theorem Th96:
for F being 0-characteristic Field,
i,j being non zero Integer st j divides i
holds (i div j) '*' 1.F = (i '*' 1.F) * (j '*' 1.F)"
proof
let F be 0-characteristic Field, i,j be non zero Integer;
A1: Char F = 0 by Def6;
assume j divides i;
then consider k being Integer such that A2: i = j * k;
A3: (i div j) * j = [\ k * (j / j) /] * j by A2
.= [\ k*1 /] * j by XCMPLX_1:60
.= i by A2;
A4: j '*' 1.F <> 0.F
proof
per cases;
suppose j > 0;
then j is Element of NAT by INT_1:3;
hence thesis by A1,Def5;
end;
suppose j < 0;
then A5: - j is Element of NAT by INT_1:3;
A6: j '*' 1.F = (-(-j)) '*' 1.F .= -((-j) '*' 1.F) by Th62;
now assume j '*' 1.F = 0.F;
then -(-((-j) '*' 1.F)) = 0.F by A6;
hence (-j) '*' 1.F = 0.F;
end;
hence thesis by A5,A1,Def5;
end;
end;
A7: i '*' 1.F <> 0.F
proof
per cases;
suppose i > 0;
then i is Element of NAT by INT_1:3;
hence thesis by A1,Def5;
end;
suppose i < 0;
then A8: - i is Element of NAT by INT_1:3;
A9: i '*' 1.F = (-(-i)) '*' 1.F .= -((-i) '*' 1.F) by Th62;
now assume i '*' 1.F = 0.F;
then -(-((-i) '*' 1.F)) = 0.F by A9;
hence (-i) '*' 1.F = 0.F;
end;
hence thesis by A8,A1,Def5;
end;
end;
(((i div j) '*' 1.F) * (i '*' 1.F)") * (j '*' 1.F)
= (i '*' 1.F)" * (((i div j) '*' 1.F) * (j '*' 1.F)) by GROUP_1:def 3
.= (i '*' 1.F)" * ((i div j)*j '*' 1.F) by Th66
.= 1.F by A3,A7,VECTSP_1:def 10;
then (j '*' 1.F)"
= ((i div j) '*' 1.F) * (i '*' 1.F)" by A4,VECTSP_1:def 10;
hence (i '*' 1.F) * (j '*' 1.F)"
= ((i '*' 1.F) * (i '*' 1.F)") * ((i div j) '*' 1.F) by GROUP_1:def 3
.= 1.F * ((i div j) '*' 1.F) by A7,VECTSP_1:def 10
.= ((i div j) '*' 1.F);
end;
definition
let x be Element of F_Rat;
redefine func denominator(x) -> positive Element of INT.Ring; :: redefines denominator (RAT_1, definition)
coherence by INT_1:def 2;
redefine func numerator(x) -> Element of INT.Ring; :: redefines numerator (RAT_1, definition)
coherence by INT_1:def 2;
end;
definition
let F be Field;
func canHom_Rat F -> Function of F_Rat,F means :Def11:
for x being Element of F_Rat holds
it.x = ((canHom_Int F).numerator x) / ((canHom_Int F).denominator x);
existence
proof
deffunc F(Element of F_Rat) =
((canHom_Int F).numerator $1) / ((canHom_Int F).denominator $1);
ex f being Function of F_Rat,F st
for x being Element of F_Rat holds f.x = F(x) from FUNCT_2:sch 4;
hence thesis;
end;
uniqueness
proof
let f,g be Function of F_Rat,F such that
A1: for x being Element of F_Rat holds
f.x = ((canHom_Int F).numerator x) / ((canHom_Int F).denominator x) and
A2: for x being Element of F_Rat holds
g.x = ((canHom_Int F).numerator x) / ((canHom_Int F).denominator x);
let x be Element of F_Rat;
thus f.x = ((canHom_Int F).numerator x) / ((canHom_Int F).denominator x)
by A1
.= g.x by A2;
end;
end;
registration
let F be Field;
cluster canHom_Rat F -> unity-preserving;
coherence
proof
set f = canHom_Rat F; set c = canHom_Int F;
A1: numerator 1 = 1 & denominator 1 = 1 by RAT_1:17;
c.1_INT.Ring = 1_F by GROUP_1:def 13;
hence f.1_F_Rat = 1.F / (1.F) by A1,Def11 .= 1_F;
end;
end;
registration
let F be 0-characteristic Field;
cluster canHom_Rat F -> additive multiplicative;
coherence
proof
set f = canHom_Rat F;
set c = canHom_Int F;
hereby
let x,y be Element of F_Rat;
reconsider x1 = x, y1 = y as Rational;
set m = denominator x1, n = denominator y1;
set i = numerator x1, j = numerator y1;
A1: c.numerator(x) = numerator(x) '*' 1.F by Def8;
A2: c.numerator(y) = numerator(y) '*' 1.F by Def8;
A3: c.numerator(x+y) = numerator(x+y) '*' 1.F by Def8;
A4: Char F = 0 by Def6;
A5: (i*n+j*m) gcd (m*n) <> 0 by INT_2:5;
A6: ((i*n+j*m) gcd (m*n)) divides (i*n+j*m) by INT_2:def 2;
A7: ((i*n+j*m) gcd (m*n)) divides (m * n) by INT_2:def 2;
A8: ((i*n+j*m) gcd (m*n)) '*' 1.F <> 0.F by A4,A5,Def5; then
A9: (((i*n+j*m) gcd (m*n)) '*' 1.F)" <> 0.F by VECTSP_2:13;
A10: (m*n) '*' 1.F <> 0.F by A4,Def5;
A11: m '*' 1.F <> 0.F by A4,Def5;
A12: n '*' 1.F <> 0.F by A4,Def5;
A13: f.x + f.y
= f.x + ((c.numerator(y)) / (c.denominator(y))) by Def11
.= ((c.numerator(x)) / (c.denominator(x))) +
((c.numerator(y)) / (c.denominator(y))) by Def11
.= (i '*' 1.F) * (m '*' 1.F)" +
((c.numerator(y)) / (c.denominator(y))) by A1,Def8
.= (i '*' 1.F) * (m '*' 1.F)" + ((j '*' 1.F) / (n '*' 1.F)) by A2,Def8
.= ((i '*' 1.F) * (m '*' 1.F)") * 1.F +
(j '*' 1.F) * (n '*' 1.F)"
.= ((i '*' 1.F) * (m '*' 1.F)") * (1 '*' 1.F) +
(j '*' 1.F) * (n '*' 1.F)" by Th59
.= ((i '*' 1.F) * (m '*' 1.F)") * ((n div n) '*' 1.F) +
(j '*' 1.F) * (n '*' 1.F)" by INT_1:49
.= ((i '*' 1.F) * (m '*' 1.F)") * ((n '*' 1.F) * (n '*' 1.F)") +
(j '*' 1.F) * (n '*' 1.F)" by Th96
.= (i '*' 1.F) * ((m '*' 1.F)" * ((n '*' 1.F) * (n '*' 1.F)")) +
(j '*' 1.F) * (n '*' 1.F)" by GROUP_1:def 3
.= (i '*' 1.F) * ((n '*' 1.F) * ((n '*' 1.F)" * (m '*' 1.F)")) +
(j '*' 1.F) * (n '*' 1.F)" by GROUP_1:def 3
.= ((i '*' 1.F) * (n '*' 1.F)) * ((n '*' 1.F)" * (m '*' 1.F)") +
(j '*' 1.F) * (n '*' 1.F)" by GROUP_1:def 3
.= ((i '*' 1.F) * (n '*' 1.F)) * ((n '*' 1.F)" * (m '*' 1.F)") +
(j '*' 1.F) * (n '*' 1.F)" * 1.F
.= ((i '*' 1.F) * (n '*' 1.F)) * ((n '*' 1.F)" * (m '*' 1.F)") +
(j '*' 1.F) * (n '*' 1.F)" * (1 '*' 1.F) by Th59
.= ((i '*' 1.F) * (n '*' 1.F)) * ((n '*' 1.F)" * (m '*' 1.F)") +
(j '*' 1.F) * (n '*' 1.F)" * ((m div m) '*' 1.F) by INT_1:49
.= ((i '*' 1.F) * (n '*' 1.F)) * ((n '*' 1.F)" * (m '*' 1.F)") +
(j '*' 1.F) * (n '*' 1.F)" * ((m '*' 1.F) * (m '*' 1.F)") by Th96
.= ((i '*' 1.F) * (n '*' 1.F)) * ((n '*' 1.F)" * (m '*' 1.F)") +
(j '*' 1.F) * ((n '*' 1.F)" * ((m '*' 1.F) * (m '*' 1.F)"))
by GROUP_1:def 3
.= ((i '*' 1.F) * (n '*' 1.F)) * ((n '*' 1.F)" * (m '*' 1.F)") +
(j '*' 1.F) * ((m '*' 1.F) * ((n '*' 1.F)" * (m '*' 1.F)"))
by GROUP_1:def 3
.= ((i '*' 1.F) * (n '*' 1.F)) * ((n '*' 1.F)" * (m '*' 1.F)") +
((j '*' 1.F) * (m '*' 1.F)) * ((n '*' 1.F)" * (m '*' 1.F)")
by GROUP_1:def 3
.= (((i '*' 1.F) * (n '*' 1.F)) + ((j '*' 1.F) * (m '*' 1.F)))
* ((n '*' 1.F)" * (m '*' 1.F)") by VECTSP_1:def 7
.= ((((i*n) '*' 1.F)) + ((j '*' 1.F) * (m '*' 1.F)))
* ((n '*' 1.F)" * (m '*' 1.F)") by Th66
.= ((((i*n) '*' 1.F)) + (((j*m) '*' 1.F)))
* ((n '*' 1.F)" * (m '*' 1.F)") by Th66
.= ((i*n+j*m) '*' 1.F) * ((n '*' 1.F)" * (m '*' 1.F)") by Th61
.= ((i*n+j*m) '*' 1.F) * ((n '*' 1.F) * (m '*' 1.F))" by A11,A12
,VECTSP_2:11
.= ((i*n+j*m) '*' 1.F) * ((n*m) '*' 1.F)" by Th66
.= ((i*n+j*m) '*' 1.F) * (1.F * ((n*m) '*' 1.F)")
.= ((i*n+j*m) '*' 1.F) * (((((i*n+j*m) gcd (m*n)) '*' 1.F)" *
(((i*n+j*m) gcd (m*n)) '*' 1.F)) * ((m*n) '*' 1.F)")
by A8,VECTSP_2:def 2
.= ((i*n+j*m) '*' 1.F) * ((((i*n+j*m) gcd (m*n)) '*' 1.F)" *
(((m*n) '*' 1.F)" * (((i*n+j*m) gcd (m*n)) '*' 1.F)))
by GROUP_1:def 3
.= (((i*n+j*m) '*' 1.F) * (((i*n+j*m) gcd (m*n)) '*' 1.F)") *
(((m*n) '*' 1.F)" * (((i*n+j*m) gcd (m*n)) '*' 1.F))
by GROUP_1:def 3
.= (((i*n+j*m) '*' 1.F) * (((i*n+j*m) gcd (m*n)) '*' 1.F)") *
(((m*n) '*' 1.F)" * ((((i*n+j*m) gcd (m*n)) '*' 1.F)")")
by A8,VECTSP_1:24
.= (((i*n+j*m) '*' 1.F) * (((i*n+j*m) gcd (m*n)) '*' 1.F)") *
((((m*n) '*' 1.F) * (((i*n+j*m)gcd(m*n)) '*' 1.F)")")
by A9,A10,VECTSP_2:11;
A14: f.(x+y)
= (c.numerator(x+y)) / (c.denominator(x+y)) by Def11
.= numerator(x+y) '*' 1.F * ((denominator(x+y) '*' 1.F)") by A3,Def8
.= ((i*n+j*m) div ( (i*n+j*m) gcd (m*n) )) '*' 1.F *
((denominator(x+y) '*' 1.F)") by Th35
.= ((i*n+j*m) div ( (i*n+j*m) gcd (m*n) )) '*' 1.F *
((((m*n) div ( (i*n+j*m) gcd (m*n) )) '*' 1.F)") by Th35;
per cases;
suppose i*n+j*m <> 0;
hence f.(x+y)
= (((i*n+j*m) '*' 1.F) * (((i*n+j*m) gcd (m*n)) '*' 1.F)") *
((((m*n) div ( (i*n+j*m) gcd (m*n))) '*' 1.F)") by A14,A5,A6,Th96
.= f.x + f.y by A13,A5,A7,Th96;
end;
suppose A15: i*n+j*m = 0;
(m*n)*0 = 0; then
A16: (m*n) divides 0 & (m*n) divides (m*n);
for a being Integer
st a divides 0 & a divides (m*n) holds a divides (m*n);
then (i*n+j*m) gcd (m*n) = m*n by A16,A15,INT_2:def 2;
hence f.(x+y)
= ((i*n+j*m) div (m*n)) '*' 1.F * ((1 '*' 1.F)") by A14,INT_1:49
.= ((i*n+j*m) div (m*n)) '*' 1.F * ((1.F)") by Th59
.= [\ 0 / (m*n) /] '*' 1.F by A15
.= 0 '*' 1.F
.= (0.F * (((i*n+j*m) gcd (m*n)) '*' 1.F)") *
((((m*n) '*' 1.F)*(((i*n+j*m) gcd (m*n)) '*' 1.F)")") by Th58
.= f.x + f.y by A13,A15,Th58;
end;
end;
hereby
let x,y be Element of F_Rat;
reconsider x1 = x, y1 = y as Rational;
set m = denominator x1, n = denominator y1;
set i = numerator x1, j = numerator y1;
A17: c.numerator(x) = numerator(x) '*' 1.F by Def8;
A18: c.numerator(y) = numerator(y) '*' 1.F by Def8;
A19: c.numerator(x*y) = numerator(x*y) '*' 1.F by Def8;
A20: Char F = 0 by Def6;
A21: (i*j) gcd (m*n) <> 0 by INT_2:5;
A22: ((i*j) gcd (m*n)) divides (i * j) by INT_2:def 2;
A23: ((i*j) gcd (m*n)) divides (m * n) by INT_2:def 2;
A24: ((i*j) gcd (m*n)) '*' 1.F <> 0.F by A20,A21,Def5; then
A25: (((i*j) gcd (m*n)) '*' 1.F)" <> 0.F by VECTSP_2:13;
A26: (m*n) '*' 1.F <> 0.F by A20,Def5;
A27: m '*' 1.F <> 0.F by A20,Def5;
A28: n '*' 1.F <> 0.F by A20,Def5;
A29: f.x * f.y
= f.x * ((c.numerator(y)) / (c.denominator(y))) by Def11
.= ((c.numerator(x)) / (c.denominator(x))) *
((c.numerator(y)) / (c.denominator(y))) by Def11
.= (i '*' 1.F) * (m '*' 1.F)" *
((c.numerator(y)) / (c.denominator(y))) by A17,Def8
.= (i '*' 1.F) * (m '*' 1.F)" * ((j '*' 1.F) / (n '*' 1.F)) by A18,Def8
.= (i'*'1.F) * ((m'*'1.F)" * ((j'*'1.F) * (n'*'1.F)")) by GROUP_1:def 3
.= (i'*'1.F) * (((m'*'1.F)" * (n'*'1.F)") * (j'*'1.F)) by GROUP_1:def 3
.= ((i '*' 1.F)*(j '*' 1.F))*((m '*' 1.F)"*(n '*' 1.F)") by GROUP_1:def 3
.= ((i*j) '*' 1.F) * ((m '*' 1.F)" * (n '*' 1.F)") by Th66
.= ((i*j) '*' 1.F) * ((m '*' 1.F) * (n '*' 1.F))" by A27,A28,VECTSP_2:11
.= ((i*j) '*' 1.F) * ((m*n) '*' 1.F)" by Th66
.= ((i*j) '*' 1.F) * (1.F * ((m*n) '*' 1.F)")
.= ((i*j) '*' 1.F) * (((((i*j) gcd (m*n)) '*' 1.F)" *
(((i*j) gcd (m*n)) '*' 1.F)) * ((m*n) '*' 1.F)") by A24,VECTSP_2:def 2
.= ((i*j) '*' 1.F) * ((((i*j) gcd (m*n)) '*' 1.F)" *
(((m*n) '*' 1.F)" * (((i*j) gcd (m*n)) '*' 1.F))) by GROUP_1:def 3
.= (((i*j) '*' 1.F) * (((i*j) gcd (m*n)) '*' 1.F)") *
(((m*n) '*' 1.F)" * (((i*j) gcd (m*n)) '*' 1.F)) by GROUP_1:def 3
.= (((i*j) '*' 1.F) * (((i*j) gcd (m*n)) '*' 1.F)") *
(((m*n) '*' 1.F)" * ((((i*j) gcd (m*n)) '*' 1.F)")") by A24,VECTSP_1:24
.= (((i*j) '*' 1.F) * (((i*j) gcd (m*n)) '*' 1.F)") *
((((m*n) '*' 1.F)*(((i*j) gcd (m*n)) '*' 1.F)")") by A25,A26
,VECTSP_2:11;
A30: f.(x*y)
= (c.numerator(x*y)) / (c.denominator(x*y)) by Def11
.= numerator(x*y) '*' 1.F * ((denominator(x*y) '*' 1.F)") by A19,Def8
.= ((i*j) div ( (i*j) gcd (m*n))) '*' 1.F *
((denominator(x*y) '*' 1.F)") by Th39
.= ((i*j) div ( (i*j) gcd (m*n))) '*' 1.F *
((((m*n) div ( (i*j) gcd (m*n))) '*' 1.F)") by Th39;
per cases;
suppose i * j <> 0;
hence f.(x*y)
= (((i*j) '*' 1.F) * (((i*j) gcd (m*n)) '*' 1.F)") *
((((m*n) div ( (i*j) gcd (m*n))) '*' 1.F)") by A30,A21,A22,Th96
.= f.x * f.y by A29,A21,A23,Th96;
end;
suppose A31: i * j = 0;
(m*n)*0 = 0; then
A32: (m*n) divides 0 & (m*n) divides (m*n);
for a being Integer
st a divides 0 & a divides (m*n) holds a divides (m*n);
then (i*j) gcd (m*n) = m*n by A32,A31,INT_2:def 2;
hence f.(x*y)
= ((i*j) div (m*n)) '*' 1.F * ((1 '*' 1.F)") by A30,INT_1:49
.= ((i*j) div (m*n)) '*' 1.F * ((1.F)") by Th59
.= [\ 0 / (m*n) /] '*' 1.F by A31
.= 0 '*' 1.F
.= (0.F * (((i*j) gcd (m*n)) '*' 1.F)") *
((((m*n) '*' 1.F)*(((i*j) gcd (m*n)) '*' 1.F)")") by Th58
.= f.x * f.y by A29,A31,Th58;
end;
end;
end;
end;
registration
cluster -> (F_Rat)-monomorphic for 0-characteristic Field;
coherence
proof
let F be 0-characteristic Field;
take canHom_Rat F;
thus thesis;
end;
end;
theorem Th97:
for F being Field holds canHom_Int F = (canHom_Rat F) | INT
proof
let F be Field;
set f = canHom_Int F;
set g = canHom_Rat F;
dom g = RAT by FUNCT_2:def 1;
then
A1: dom(g|INT) = INT by RELAT_1:62,NUMBERS:14;
now
let x be object;
assume
A2: x in dom f;
then reconsider y = x as Element of INT.Ring;
reconsider r = y as Element of F_Rat by NUMBERS:14;
A3: f.1_I = 1_F by GROUP_1:def 13;
thus f.x = (f.numerator r) / 1_F
.= (f.numerator r) / (f.denominator r) by A3,RAT_1:17
.= g.x by Def11
.= (g|INT).x by A2,FUNCT_1:49;
end;
hence thesis by FUNCT_2:def 1,A1;
end;
registration
cluster 0-characteristic F_Rat-homomorphic for Field;
existence;
end;
theorem Th98:
for F being 0-characteristic F_Rat-homomorphic Field,
f being Homomorphism of F_Rat,F holds f = canHom_Rat F
proof
let F be 0-characteristic F_Rat-homomorphic Field,
f be Homomorphism of F_Rat,F;
set g = canHom_Rat F;
A1: f is unity-preserving;
A2: f is multiplicative;
A3: g is unity-preserving;
A4: dom f = the carrier of F_Rat by FUNCT_2:def 1
.= dom g by FUNCT_2:def 1;
defpred P[Integer] means for j being Element of F_Rat
st j = $1 holds f.j = g.j;
A5: 0.F_Rat = 0;
then f.0 = 0.F by RING_2:6
.= g.0 by A5,RING_2:6;
then A6: P[0];
A7: now let u be Integer;
assume A8: P[u];
reconsider uu = u as Element of F_Rat by RAT_1:def 2;
now let k be Integer;
assume k = u-1;
then A9: k = uu - 1.F_Rat;
hence f.k = f.uu - f.(1.F_Rat) by RING_2:8
.= g.uu - g.(1_F_Rat) by A8,A1,A3
.= g.k by A9,RING_2:8;
end;
hence P[u-1];
now let k be Integer;
assume k = u+1;
then A10: k = uu + 1.F_Rat;
hence f.k = f.uu + f.(1.F_Rat) by VECTSP_1:def 20
.= g.uu + g.(1_F_Rat) by A8,A1,A3
.= g.k by A10,VECTSP_1:def 20;
end;
hence P[u+1];
end;
A11: for i be Integer holds P[i] from INT_1:sch 4(A6,A7);
A12: for i be Integer, j be Element of F_Rat
st j = i holds f.j = (canHom_Int F).i
proof
let i be Integer, j be Element of F_Rat;
assume A13: j = i;
A14: canHom_Int F = (canHom_Rat F) | INT by Th97;
thus f.j = g.i by A13,A11
.= (canHom_Int F).i by A14,INT_1:def 2,FUNCT_1:49;
end;
now let x be object;
assume x in dom f;
then reconsider a = x as Element of F_Rat;
reconsider a1 = numerator a as Element of F_Rat by RAT_1:def 2;
reconsider a2 = denominator a as Element of F_Rat by RAT_1:def 2;
A15: a2 <> 0.F_Rat;
g.a = ((canHom_Int F).numerator a) / ((canHom_Int F).denominator a)
by Def11
.= f.a1 / ((canHom_Int F).denominator a) by A12
.= f.a1 / f.a2 by A12
.= f.a1 * f.(a2") by A15,QUOFIELD:52
.= f.(a1*a2") by A2
.= f.((numerator a) * (denominator a)" ) by GAUSSINT:15
.= f.a by RAT_1:15;
hence f.x = g.x;
end;
hence thesis by A4;
end;
registration
cluster F_Rat -> F_Rat-homomorphic;
coherence;
end;
registration
let F be 0-characteristic Field;
cluster PrimeField F -> F_Rat-homomorphic;
coherence;
end;
theorem
for f being Homomorphism of F_Rat,F_Rat holds f = id F_Rat
proof
let f be Homomorphism of F_Rat,F_Rat;
id F_Rat = canHom_Rat F_Rat by Th98;
hence thesis by Th98;
end;
definition
let F be Field,
S be F-homomorphic Field,
f be Homomorphism of F,S;
redefine func Image f -> strict Subfield of S; :: redefines Image (RING_2, definition)
coherence
proof
set I = Image f;
the carrier of I = rng f &
the addF of I = (the addF of S)||rng f &
the multF of I = (the multF of S)||rng f &
1.I = 1.S & 0.I = 0.S by RING_2:def 6;
hence thesis by EC_PF_1:def 1;
end;
end;
registration
let F be 0-characteristic Field;
cluster canHom_Rat PrimeField F -> onto;
coherence
proof
set K = PrimeField F;
thus the carrier of K = the carrier of Image canHom_Rat K by EC_PF_1:def 2
.= rng canHom_Rat K by RING_2:def 6;
end;
end;
theorem Th100:
for F being 0-characteristic Field holds F_Rat,PrimeField F are_isomorphic
proof
let F be 0-characteristic Field;
take canHom_Rat PrimeField F;
thus thesis;
end;
theorem
PrimeField F_Rat = F_Rat by GAUSSINT:26;
theorem
for F being 0-characteristic Field holds F includes F_Rat by Th71;
theorem
for F being 0-characteristic Field,
E being Field st F includes E holds E includes F_Rat
proof
let F be 0-characteristic Field, E be Field;
assume F includes E;
then F is E-monomorphic by Th71;
then Char E = Char F by Th87 .= 0 by Def6;
then E is 0-characteristic;
hence thesis by Th71;
end;
theorem Th104:
for p being Prime, R being p-characteristic Ring,
i being Integer
holds i '*' 1.R = (i mod p) '*' 1.R
proof
let p be Prime, R be p-characteristic Ring, i be Integer;
Char R = p by Def6; then A1: p '*' 1.R = 0.R by Def5;
A2: ((i div p) * p) '*' 1.R = ((i div p) '*' 1.R) * (p '*' 1.R) by Th66
.= 0.R by A1;
thus i '*' 1.R
= ((i div p) * p + (i mod p)) '*' 1.R by INT_1:59
.= 0.R + ((i mod p) '*' 1.R) by A2,Th61
.= (i mod p) '*' 1.R;
end;
definition
let p be Prime,
F be Field;
func canHom_Z/(p,F) -> Function of Z/p,F equals
(canHom_Int F) | (the carrier of Z/p);
coherence
proof
set f = (canHom_Int F) | (the carrier of Z/p);
now let x be object;
assume x in the carrier of Z/p;
then reconsider x1 = x as natural Number;
x1 in INT by NUMBERS:17,ORDINAL1:def 12;
hence x in dom(canHom_Int F) by FUNCT_2:def 1;
end;
then the carrier of Z/p c= dom(canHom_Int F);
then A1: dom f = the carrier of Z/p by RELAT_1:62;
now let x be object;
assume A2: x in the carrier of Z/p;
then f.x = (canHom_Int F).x by FUNCT_1:49;
then f.x in rng(canHom_Int F) by A1,A2,FUNCT_2:4;
hence f.x in the carrier of F;
end;
hence thesis by A1,FUNCT_2:3;
end;
end;
Lm14:
for p be Prime, F be Field, x be Element of Z/p, y be Element of INT.Ring
st x = y holds (canHom_Z/(p,F)).x = y '*' 1.F
proof
let p be Prime, F be Field, x be Element of Z/p, y be Element of INT.Ring;
assume x = y;
hence (canHom_Z/(p,F)).x = (canHom_Int F).y by FUNCT_1:49
.= y '*' 1.F by Def8;
end;
registration
let p be Prime,
F be Field;
cluster canHom_Z/(p,F) -> unity-preserving;
coherence
proof
set f = canHom_Z/(p,F); set c = canHom_Int F;
1_Z/p = 1_INT.Ring by INT_3:14,INT_2:def 4;
hence f.1_Z/p = c.1_INT.Ring by FUNCT_1:49 .= 1_F by GROUP_1:def 13;
end;
end;
registration
let p be Prime,
F be p-characteristic Field;
cluster canHom_Z/(p,F) -> additive multiplicative;
coherence
proof
set f = canHom_Z/(p,F);
hereby
let x,y be Element of Z/p;
reconsider x1 = x,
y1 = y as Element of INT.Ring by ORDINAL1:def 12,NUMBERS:17;
A1: x + y = (x1 + y1) mod p by GR_CY_1:def 4;
reconsider z = (x1 + y1) mod p as Element of INT.Ring by INT_1:def 2;
thus f.x + f.y = (x1 '*' 1.F) + f.y by Lm14
.= (x1 '*' 1.F) + (y1 '*' 1.F) by Lm14
.= (x1 + y1) '*' 1.F by Th61
.= z '*' 1.F by Th104
.= f.(x+y) by Lm14,A1;
end;
hereby
let x,y be Element of Z/p;
reconsider x1 = x,
y1 = y as Element of INT.Ring by ORDINAL1:def 12,NUMBERS:17;
A2: x * y = (x1 * y1) mod p by INT_3:def 10;
reconsider z = (x1 * y1) mod p as Element of INT.Ring by INT_1:def 2;
thus f.x * f.y = (x1 '*' 1.F) * f.y by Lm14
.= (x1 '*' 1.F) * (y1 '*' 1.F) by Lm14
.= (x1 * y1) '*' 1.F by Th66
.= z '*' 1.F by Th104
.= f.(x*y) by Lm14,A2;
end;
end;
end;
registration
let p be Prime;
cluster -> (Z/p)-monomorphic for p-characteristic Field;
coherence
proof
let F be p-characteristic Field;
take canHom_Z/(p,F);
thus thesis;
end;
end;
registration
let p be Prime;
cluster p-characteristic (Z/p)-homomorphic for Field;
existence;
cluster Z/p -> (Z/p)-homomorphic;
coherence;
end;
theorem Th105:
for p being Prime,
F being p-characteristic (Z/p)-homomorphic Field,
f being Homomorphism of Z/p,F holds f = canHom_Z/(p,F)
proof
let p be Prime, F be p-characteristic (Z/p)-homomorphic Field,
f be Homomorphism of Z/p,F;
set g = canHom_Z/(p,F);
A1: f is unity-preserving;
A2: g is unity-preserving additive multiplicative;
A3: dom f = the carrier of Z/p by FUNCT_2:def 1
.= dom g by FUNCT_2:def 1;
A4: 1.(Z/p) = 1 by INT_3:14,INT_2:def 4;
reconsider p1 = p-1 as Element of NAT by INT_1:3;
A5: p1 + 1 = p;
defpred P[Nat] means for j being Element of Z/p st j = $1 holds f.j = g.j;
f.0 = f.(0.(Z/p)) by NAT_1:44,SUBSET_1:def 8
.= 0.F by RING_2:6
.= g.(0.(Z/p)) by RING_2:6
.= g.0 by NAT_1:44,SUBSET_1:def 8;
then A6: P[0];
A7: for k being Element of NAT st 0<=k & k<p1 holds P[k] implies P[k+1]
proof
let k be Element of NAT;
assume A8: 0 <= k & k < p1;
assume A9: P[k];
reconsider e = 1 as Element of Segm(p) by A4;
k < p by A5,A8,NAT_1:13; then
reconsider z = k as Element of Z/p by NAT_1:44;
reconsider z0 = z as Element of Segm(p);
A10: k+1 < p1 + 1 by A8,XREAL_1:6; then
reconsider z1 = k+1 as Element of Segm(p) by NAT_1:44;
reconsider z1 as Element of Z/p;
A11: z + 1.Z/p = (addint(p)).(k,1) by INT_3:14,INT_2:def 4
.= z0 + e by A10,INT_3:7
.= k + 1;
f.z1 = f.z + f.(1.Z/p) by A11,VECTSP_1:def 20
.= g.z + g.(1.Z/p) by A9,A1,A2
.= g.z1 by A11,A2;
hence P[k+1];
end;
A12: for k be Element of NAT st 0 <= k & k <= p1 holds P[k]
from INT_1:sch 7(A6,A7);
now let x be object;
assume x in dom f;
then reconsider a = x as Element of Segm(p);
a < p1 + 1 by NAT_1:44;
then a <= p-1 by NAT_1:13;
hence f.x = g.x by A12;
end;
hence thesis by A3;
end;
theorem
for p being Prime,
f being Homomorphism of Z/p,Z/p holds f = id Z/p
proof
let p be Prime;
let f be Homomorphism of Z/p,Z/p;
id Z/p = canHom_Z/(p,Z/p) by Th105;
hence thesis by Th105;
end;
registration
let p be Prime, F be p-characteristic Field;
cluster PrimeField F -> Z/p-homomorphic;
coherence;
end;
registration
let p be Prime, F be p-characteristic Field;
cluster canHom_Z/(p,PrimeField F) -> onto;
coherence
proof
set K = PrimeField F;
thus the carrier of K = the carrier of Image canHom_Z/(p,K) by EC_PF_1:def 2
.= rng canHom_Z/(p,K) by RING_2:def 6;
end;
end;
theorem Th107:
for p being Prime,
F being p-characteristic Field holds Z/p,PrimeField F are_isomorphic
proof
let p be Prime;
let F be p-characteristic Field;
take canHom_Z/(p,PrimeField F);
thus thesis;
end;
theorem
for p being Prime, F being strict Subfield of Z/p holds F = Z/p
by EC_PF_1:def 2;
theorem
for p being Prime holds PrimeField Z/p = Z/p by EC_PF_1:def 2;
theorem
for p being Prime,
F being p-characteristic Field holds F includes Z/p by Th71;
theorem
for p being Prime,
F being p-characteristic Field,
E being Field st F includes E holds E includes Z/p
proof
let p be Prime, F be p-characteristic Field, E be Field;
assume F includes E;
then F is E-monomorphic by Th71;
then Char E = Char F by Th87 .= p by Def6;
then E is p-characteristic;
hence thesis by Th71;
end;
registration
let p be Prime;
cluster Z/p -> prime;
coherence;
end;
theorem
for F being Field
holds Char F = 0 iff PrimeField F, F_Rat are_isomorphic
proof
let F be Field;
A1: now assume Char F = 0;
then F is 0-characteristic;
hence PrimeField F, F_Rat are_isomorphic by Th100;
end;
now assume PrimeField F, F_Rat are_isomorphic;
then ex f being Function of F_Rat,PrimeField F st f is RingIsomorphism
by QUOFIELD:def 23;
then PrimeField F is F_Rat-isomorphic;
then A2: PrimeField F is 0-characteristic;
PrimeField F is Subring of F by Lm1;
hence Char F = 0 by A2,Th88;
end;
hence thesis by A1;
end;
theorem
for p being Prime,
F being Field
holds Char F = p iff PrimeField F, Z/p are_isomorphic
proof
let p be Prime, F be Field;
A1: now assume Char F = p;
then F is p-characteristic;
hence PrimeField F,Z/p are_isomorphic by Th107;
end;
now assume PrimeField F, Z/p are_isomorphic;
then ex f being Function of Z/p,PrimeField F st f is RingIsomorphism
by QUOFIELD:def 23;
then PrimeField F is Z/p-isomorphic;
then A2: PrimeField F is p-characteristic;
PrimeField F is Subring of F by Lm1;
hence Char F = p by A2,Th88;
end;
hence thesis by A1;
end;
theorem
for F being strict Field
holds F is prime iff (F,F_Rat are_isomorphic or
ex p being Prime st F,Z/p are_isomorphic)
proof
let F be strict Field;
thus F is prime implies F, F_Rat are_isomorphic or
ex p being Prime st F, Z/p are_isomorphic
proof
assume A1: F is prime;
per cases by Th85;
suppose Char F = 0;
then F is 0-characteristic;
then PrimeField F, F_Rat are_isomorphic by Th100;
hence thesis by EC_PF_1:def 2,A1;
end;
suppose Char F is prime;
then consider p being Prime such that A2: Char F = p;
F is p-characteristic by A2;
then A3: PrimeField F, Z/p are_isomorphic by Th107;
PrimeField F, F are_isomorphic by EC_PF_1:def 2,A1;
hence thesis by A3,Th43;
end;
end;
assume A4: F, F_Rat are_isomorphic or
ex p being Prime st F, Z/p are_isomorphic;
per cases by A4;
suppose F, F_Rat are_isomorphic;
then consider f being Function of F,F_Rat such that
A5: f is RingIsomorphism;
A6: F_Rat is F-isomorphic by A5;
then reconsider EK1 = F_Rat as F-homomorphic Field;
reconsider f as Homomorphism of F,EK1 by A5;
now let K be Field;
assume A7: K is strict Subfield of F;
then reconsider EK = F_Rat as K-homomorphic Field by A6,Th56;
reconsider g = f|K as Homomorphism of K,EK by A7,Th57;
A8: Image g = F_Rat by EC_PF_1:def 2;
A9: the carrier of K c= the carrier of F by A7,EC_PF_1:def 1;
now let x be object;
assume x in the carrier of F;
then reconsider a = x as Element of the carrier of F;
f.a in Image g by A8;
then f.a in rng g by RING_2:def 6;
then consider y being object such that
A10: y in dom g & g.y = f.a by FUNCT_1:def 3;
reconsider y as Element of the carrier of K by A10;
A11: y in the carrier of F by A9;
(f|the carrier of K).y = f.y by FUNCT_1:49;
then a = y by A10,A11,FUNCT_2:19;
hence x in the carrier of K;
end;
then the carrier of F c= the carrier of K;
then A12: the carrier of F = the carrier of K by A7,EC_PF_1:def 1;
the addF of K = (the addF of F) || the carrier of K
& the multF of K = (the multF of F) || the carrier of K
& 1.F = 1.K & 0.F = 0.K by A7,EC_PF_1:def 1;
hence K = F by A7,A12;
end;
hence thesis by EC_PF_1:def 2;
end;
suppose ex p being Prime st F, Z/p are_isomorphic;
then consider p being Prime such that A13: F, Z/p are_isomorphic;
consider f being Function of F, Z/p such that
A14: f is RingIsomorphism by A13;
A15: Z/p is F-isomorphic by A14;
then reconsider EK1 = Z/p as F-homomorphic Field;
reconsider f as Homomorphism of F,EK1 by A14;
now let K be Field;
assume A16: K is strict Subfield of F;
then reconsider EK = Z/p as K-homomorphic Field by A15,Th56;
reconsider g = f|K as Homomorphism of K,EK by A16,Th57;
A17: Image g = Z/p by EC_PF_1:def 2;
A18: the carrier of K c= the carrier of F by A16,EC_PF_1:def 1;
now let x be object;
assume x in the carrier of F;
then reconsider a = x as Element of the carrier of F;
f.a in Image g by A17;
then f.a in rng g by RING_2:def 6;
then consider y being object such that
A19: y in dom g & g.y = f.a by FUNCT_1:def 3;
reconsider y as Element of the carrier of K by A19;
A20: y in the carrier of F by A18;
(f|the carrier of K).y = f.y by FUNCT_1:49;
then a = y by A19,A20,FUNCT_2:19;
hence x in the carrier of K;
end;
then the carrier of F c= the carrier of K;
then A21: the carrier of F = the carrier of K by A16,EC_PF_1:def 1;
the addF of K = (the addF of F) || the carrier of K
& the multF of K = (the multF of F) || the carrier of K
& 1.F = 1.K & 0.F = 0.K by A16,EC_PF_1:def 1;
hence K = F by A16,A21;
end;
hence thesis by EC_PF_1:def 2;
end;
end;