:: Embedding Principle for Rings and Abelian Groups
:: by Yasushige Watase
::
:: Received November 21, 2023
:: Copyright (c) 2023-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, SUBSET_1, RELAT_1, XBOOLE_0, BINOP_1, FUNCT_1, TARSKI,
NAT_1, ARYTM_3, ZFMISC_1, CARD_1, ARYTM_1, FUNCOP_1, FUNCT_2, PRE_POLY,
GROUP_1, ALGSTR_0, RLVECT_1, VECTSP_1, LATTICES, SUPINF_2, MESFUNC1,
MOD_4, POLYNOM1, ALGSEQ_1, POLYNOM2, HILBASIS, POLYNOM3, FUNCT_4,
VECTSP_2, QUOFIELD, MSSUBFAM, FUNCSDOM, FDIFF_1, C0SP1, FIELD_2,
STRUCT_0, RING_3, REALSET1, WELLORD1, POLYNOM7, FINSEQ_1, POLYNOM4,
GROUP_6, RING_EMB;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, RELSET_1,
PARTFUN1, FUNCT_2, BINOP_1, DOMAIN_1, FUNCOP_1, REALSET1, PBOOLE,
NUMBERS, XCMPLX_0, NAT_D, FUNCT_7, PRE_POLY, STRUCT_0, ALGSTR_0,
RLVECT_1, GROUP_1, VECTSP_1, VECTSP_2, POLYNOM1, ALGSEQ_1, GROUP_6,
RINGCAT1, MOD_4, QUOFIELD, POLYNOM3, POLYNOM4, POLYNOM7, C0SP1, RING_3,
RING_4;
constructors RELSET_1, WELLORD2, REALSET1, NAT_D, FUNCT_7, ALGSEQ_1, RINGCAT1,
POLYNOM4, RING_3, FIELD_11;
registrations RELAT_1, FUNCT_1, ORDINAL1, XREAL_0, NAT_1, CARD_1, VALUED_0,
RELSET_1, FUNCT_2, STRUCT_0, VECTSP_1, RING_4, POLYNOM1, PRE_POLY, MOD_4,
POLYNOM3, FUNCOP_1, SUBSET_1, RINGCAT1, REALSET1, RVSUM_4, XBOOLE_0,
RING_3, POLYNOM6, POLYNOM4, RLVECT_1, POLYDIFF;
requirements NUMERALS, SUBSET, BOOLE, ARITHM;
definitions TARSKI;
equalities STRUCT_0, ORDINAL1, REALSET1, POLYNOM3, ALGSTR_0, BINOP_1;
expansions TARSKI, FUNCT_2, VECTSP_1, GROUP_6, ALGSTR_0, FUNCT_1, BINOP_1,
RLVECT_1, GROUP_1, XBOOLE_0;
theorems TARSKI, ZFMISC_1, RLVECT_1, FUNCT_1, FUNCT_2, POLYNOM1, RELAT_1,
CARD_1, GROUP_1, XBOOLE_0, XBOOLE_1, PRE_POLY, HILBASIS, WELLORD2,
POLYNOM3, XTUPLE_0, POLYNOM7, FUNCT_7, RING_4, VECTSP_1, RING_2, C0SP1,
QUOFIELD, STRUCT_0, MOD_4, REALSET1, GROUP_14, NIVEN, POLYNOM4;
schemes FUNCT_2, BINOP_1;
begin :: Preliminaries from Set Theory
reserve a for non empty set;
reserve b, x, o for object;
theorem Th1:
for a holds
ex b be object st (for x be set holds not [x,b] in a)
proof
let a;
reconsider b={u where u is Element of a:ex y,z be set st [y,z]=u & not u in z}
as set;
A1: for x be set holds [x,b] in b implies [x,b] in a & not [x,b] in b
proof
let x be set;
assume [x,b] in b; then
consider u1 be Element of a such that
A3: u1 = [x,b] & ex y,z be set st
[y,z] = u1 & not u1 in z;
thus thesis by A3,XTUPLE_0:1;
end;
A4: for x be set holds not [x,b] in a
proof
let x be set;
assume
A5: [x,b] in a;
per cases;
suppose [x,b] in b;
hence contradiction by A1;
end;
suppose
not [x,b] in b;
hence thesis by A5;
end;
end;
take b;
thus thesis by A4;
end;
theorem Th2:
for a,b be non empty set holds ex c be non empty set st a /\ c = {} &
(ex f be Function st f is one-to-one & dom f = b & rng f = c )
proof
let a,b be non empty set;
consider d be object such that
A1: for x be set holds not [x,d] in a by Th1;
set C = [:b,{d}:];
consider f be Function such that
A2: f is one-to-one & dom f = b & rng f = C
by WELLORD2:def 4,CARD_1:69;
A3: a /\ C = {}
proof
assume a /\ C <> {}; then
consider x be object such that
A5: x in a /\ C by XBOOLE_0:def 1;
x in C by A5,XBOOLE_0:def 4; then
consider y,z be object such that
A6: y in b & z in {d} & x = [y,z] by ZFMISC_1:84;
A7: x = [y,d] by A6,TARSKI:def 1;
reconsider y as set by A6;
not [y,d] in a by A1;
hence contradiction by A7, A5,XBOOLE_0:def 4;
end;
take C;
thus thesis by A3,A2;
end;
::$N Apply Embedding Principle to Rings.
theorem Th3:
for A be Ring, X be non empty set, f be Function of A,X,
a,b be Element of X st f is bijective holds
f.((the addF of A).(f".a,f".b)) is Element of X
proof
let A be Ring, X be non empty set, f be Function of A,X;
let a,b be Element of X;
assume
A1: f is bijective; then
A2: rng f = X by FUNCT_2:def 3;
A3: dom f = [#]A by FUNCT_2:def 1;
reconsider x = f".a, y = f".b as Element of [#]A by A3,A2,A1,FUNCT_1:32;
reconsider z = (the addF of A).(x,y) as Element of [#]A;
f.z in X;
hence thesis;
end;
definition
let A be Ring, X be non empty set;
let f be Function of A,X;
let a,b be Element of X;
assume
A1: f is bijective;
func addemb(f,a,b) -> Element of X equals :Def1:
f.((the addF of A).(f".a,f".b));
coherence by A1,Th3;
end;
theorem Th4:
for A be Ring, X be non empty set, f be Function of A,X,
a,b,c be Element of X st f is bijective holds
addemb(f,a,addemb(f,b,c)) = addemb(f,addemb(f,a,b),c)
proof
let A be Ring, X be non empty set, f be Function of A,X;
let a,b,c be Element of X;
assume
A1: f is bijective; then
A2: rng f = X by FUNCT_2:def 3;
A3: dom f = [#]A by FUNCT_2:def 1; then
reconsider x=f".a, y=f".b, z=f".c as Element of [#]A by A2,A1,FUNCT_1:32;
A4: addemb(f,a,b) = f.((the addF of A).(f".a,f".b)) by A1,Def1;
A5: addemb(f,b,c) = f.((the addF of A).(f".b,f".c)) by A1,Def1;
reconsider ab1 = f.((the addF of A).(f".a,f".b)),
bc1 = f.((the addF of A).(f".b,f".c)) as Element of X by A4,A5;
addemb(f,a,addemb(f,b,c)) = addemb(f,a,bc1) by A1,Def1
.= f.((the addF of A).(f".a,f".bc1)) by A1,Def1
.= f.(x+(y+z)) by A1,A3,FUNCT_1:34
.= f.((x+y)+z) by RLVECT_1:def 3
.= f.((the addF of A).(f".ab1,f".c)) by A1,A3,FUNCT_1:34
.= addemb(f,ab1,c) by A1,Def1
.= addemb(f,addemb(f,a,b),c) by A1,Def1;
hence thesis;
end;
definition
let A be Ring, X be non empty set;
let f be Function of A,X;
func addemb f -> BinOp of X means
:Def2:
for a,b being Element of X holds it.(a,b) = addemb(f,a,b);
existence
proof
deffunc O(Element of X,Element of X) = addemb(f,$1,$2);
consider F being BinOp of X such that
A1: for a,b being Element of X holds F.(a,b)=O(a,b) from BINOP_1:sch 4;
take F;
thus thesis by A1;
end;
uniqueness
proof
let F1,F2 be BinOp of X such that
A2: for a,b being Element of X holds F1.(a,b) = addemb(f,a,b) and
A3: for a,b being Element of X holds F2.(a,b) = addemb(f,a,b);
now let a,b be Element of X;
thus F1.(a,b) = addemb(f,a,b) by A2 .= F2.(a,b) by A3;
end;
hence thesis;
end;
end;
theorem Th5:
for A be Ring, X be non empty set, f be Function of A,X,
a,b be Element of X st f is bijective holds
f.((the multF of A).(f".a,f".b)) is Element of X
proof
let A be Ring, X be non empty set, f be Function of A,X;
let a,b be Element of X;
assume
A1: f is bijective; then
A2: rng f = X by FUNCT_2:def 3;
A3: dom f = [#]A by FUNCT_2:def 1;
reconsider x = f".a, y = f".b as Element of [#]A by A3,A2,A1,FUNCT_1:32;
reconsider z = (the multF of A).(x,y) as Element of [#]A;
f.z in X;
hence thesis;
end;
definition
let A be Ring, X be non empty set;
let f be Function of A,X;
let a,b be Element of X;
assume
A1: f is bijective;
func multemb(f,a,b) -> Element of X equals :Def3:
f.((the multF of A).(f".a,f".b));
coherence by Th5,A1;
end;
definition
let A be Ring, X be non empty set;
let f be Function of A,X;
func multemb f -> BinOp of X means :Def4:
for a,b being Element of X holds it.(a,b) = multemb(f,a,b);
existence
proof
deffunc O(Element of X,Element of X) = multemb(f,$1,$2);
consider F being BinOp of X such that
A1: for a,b being Element of X holds F.(a,b)=O(a,b) from BINOP_1:sch 4;
take F;
thus thesis by A1;
end;
uniqueness
proof
let F1,F2 be BinOp of X such that
A2: for a,b being Element of X holds F1.(a,b) = multemb(f,a,b) and
A3: for a,b being Element of X holds F2.(a,b) = multemb(f,a,b);
now let a,b be Element of X;
thus F1.(a,b) = multemb(f,a,b) by A2 .= F2.(a,b) by A3;
end;
hence thesis;
end;
end;
definition
let A be Ring, X be non empty set;
let f be Function of A,X;
func emb_Ring(f) -> strict non empty doubleLoopStr equals
doubleLoopStr(# X, addemb f, multemb f, f.1.A, f.0.A #);
coherence;
end;
theorem Th6:
for A be Ring, X be non empty set, f be Function of A,X
st f is bijective holds emb_Ring(f) is Ring
proof
let A be Ring, X be non empty set, f be Function of A,X;
assume
A1: f is bijective; then
A2: rng f = X by FUNCT_2:def 3;
A3: dom f = [#]A by FUNCT_2:def 1;
reconsider ZS = doubleLoopStr(# X, addemb f, multemb f, f.1.A, f.0.A #)
as non empty doubleLoopStr;
A5: for v, w being Element of ZS holds v + w = w + v
proof
let v, w be Element of ZS;
reconsider v1 = v, w1 = w as Element of X;
reconsider x = f".v1, y = f".w1 as Element of [#]A by A2,A3,A1,FUNCT_1:32;
v + w = addemb(f,v1,w1) by Def2
.= f.(x+y) by A1,Def1
.= f.(y+x)
.= addemb(f,w1,v1) by A1,Def1
.= w + v by Def2;
hence thesis;
end;
A6: emb_Ring(f) is Abelian by A5;
for u, v, w being Element of ZS holds u+(v+w) = (u+v)+w
proof
let u, v, w be Element of ZS;
reconsider u1 = u, v1 = v, w1 = w as Element of X;
u+(v+w) = addemb(f,u1, (addemb f).(v1,w1)) by Def2
.= addemb(f,u1, addemb(f,v1,w1)) by Def2
.= addemb(f,addemb(f,u1,v1),w1) by A1,Th4
.= addemb(f,(addemb f).(u1,v1),w1) by Def2
.= (u+v)+w by Def2;
hence thesis;
end; then
A8: emb_Ring(f) is add-associative;
for v being Element of ZS holds v + 0.ZS = v
proof
let v be Element of ZS;
reconsider v1 = v as Element of X;
reconsider x = f".v1 as Element of [#]A by A2,A3,A1,FUNCT_1:32;
v + 0.ZS = addemb(f,v1,f.0.A) by Def2
.= f.((the addF of A).(f".v1,f".(f.0.A))) by A1,Def1
.= f.(x+0.A) by A1,A3, FUNCT_1:34
.= v1 by A1,A2,FUNCT_1:35;
hence thesis;
end; then
A9: emb_Ring(f) is right_zeroed;
A10: for v being Element of ZS holds v is right_complementable
proof
let v be Element of ZS;
reconsider v1 = v as Element of X;
reconsider x = f".v1 as Element of A by A2,A3,A1,FUNCT_1:32;
consider u be Element of ZS such that
A11: u = f.(-x);
reconsider u1 = u as Element of X;
v+u = addemb(f,v1,u1) by Def2
.= f.((the addF of A).(f".v1,f".u1)) by A1,Def1
.= f.(x + (-x)) by A11,A3,A1,FUNCT_1:34
.= 0.ZS by RLVECT_1:5;
hence thesis;
end;
A12: emb_Ring(f) is right_complementable by A10;
A13: for a, b, v being Element of ZS holds (a + b) * v = a * v + b * v
proof
let a, b, v be Element of ZS;
reconsider a1 = a, b1 = b, v1 = v as Element of X;
reconsider ab = a+b as Element of ZS;
reconsider ab1 = a+b as Element of X;
reconsider x = f".a1, y = f".b1, z = f".v1 as Element of [#]A
by A2,A3,A1,FUNCT_1:32;
A14: a+b = addemb(f,a1,b1) by Def2 .= f.(x+y) by A1,Def1;
A15: f".ab1 = x+y by A14,A1,A3,FUNCT_1:34;
A16: (a + b) * v = multemb(f,ab1,v1) by Def4
.= f.((x+y)*z) by A15,A1,Def3
.= f.(x*z+y*z) by VECTSP_1:def 7;
reconsider av1 = a*v, bv1 = b*v as Element of X;
A17: a*v = multemb(f,a1,v1) by Def4
.= f.((the multF of A).(f".a1,f".v1)) by A1,Def3;
A18: b*v = multemb(f,b1,v1) by Def4
.= f.((the multF of A).(f".b1,f".v1)) by A1,Def3;
reconsider za = f".av1,
zb = f".bv1 as Element of [#]A by A2,A3,A1,FUNCT_1:32;
A19: za = x*z by A3,A1,A17,FUNCT_1:34;
A20: zb = y*z by A3,A1,A18,FUNCT_1:34;
a*v + b*v = addemb(f,av1,bv1) by Def2
.= (a + b) * v by A16,A19,A20,A1,Def1;
hence thesis;
end;
for a, b, v being Element of ZS
holds v * (a+b) = v * a + v * b & (a + b)*v = a*v + b*v
proof
let a, b, v be Element of ZS;
reconsider a1 = a, v1 = v, b1 = b as Element of X;
reconsider ab = a+b as Element of ZS;
reconsider ab1 = a+b as Element of X;
reconsider x = f".a1, y = f".b1, z = f".v1 as Element of [#]A
by A2,A3,A1,FUNCT_1:32;
A21: a+b = addemb(f,a1,b1) by Def2 .= f.(x+y) by A1,Def1;
A22: f".ab1 = x+y by A21,A1,A3,FUNCT_1:34;
A23: v*(a + b) = multemb(f,v1,ab1) by Def4
.= f.(z*(x+y)) by A22,A1,Def3
.= f.(z*x+z*y) by VECTSP_1:def 7;
reconsider va1 = v*a,
vb1 = v*b as Element of X;
A24: v*a = multemb(f,v1,a1) by Def4
.= f.((the multF of A).(f".v1,f".a1)) by A1,Def3;
A25: v*b = multemb(f,v1,b1) by Def4
.= f.((the multF of A).(f".v1,f".b1)) by A1,Def3;
reconsider za = f".va1,
zb = f".vb1 as Element of [#]A by A2,A3,A1,FUNCT_1:32;
A26: za = z*x by A3,A1,A24,FUNCT_1:34;
A27: zb = z*y by A3,A1,A25,FUNCT_1:34;
v*a + v*b = addemb(f,va1,vb1) by Def2
.= v*(a + b) by A23,A26,A27,A1,Def1;
hence thesis by A13;
end; then
A28: emb_Ring(f) is distributive;
for a, b, v being Element of ZS holds (a * b) * v = a * (b * v)
proof
let a, b, v be Element of ZS;
reconsider a1 = a, b1 = b, v1 = v as Element of X;
reconsider x = f".a1, y = f".b1,z = f".v1 as Element of [#]A
by A2,A3,A1,FUNCT_1:32;
reconsider ab1 = (a*b), bv1 = (b*v) as Element of X;
A29: a*b = multemb(f,a1,b1) by Def4
.= f.(x*y) by A1,Def3;
A30: b*v = multemb(f,b1,v1) by Def4
.= f.(y*z) by A1,Def3;
(a * b) * v = multemb(f,ab1,v1) by Def4
.= f.((the multF of A).(f".ab1,f".v1)) by A1,Def3
.= f.((x*y)*z) by A1,A3,A29,FUNCT_1:34
.= f.(x*(y*z)) by GROUP_1:def 3
.= f.((the multF of A).(f".a1,f".bv1)) by A1,A3,A30,FUNCT_1:34
.= multemb(f,a1,bv1) by A1,Def3
.= a*(b*v) by Def4;
hence thesis;
end; then
A31: emb_Ring(f) is associative;
for v being Element of ZS holds v *1.ZS = v & 1.ZS * v = v
proof
let v be Element of ZS;
reconsider v1 = v, 1zs = 1.ZS as Element of X;
reconsider y = f".v1, z = f".1zs as Element of [#]A by A2,A3,A1,FUNCT_1:32;
A32: v * 1.ZS = multemb(f,v1,1zs) by Def4
.= f.(y*z) by A1,Def3
.= f.(y*1.A) by A1,A3,FUNCT_1:34
.= v1 by A1,A2,FUNCT_1:35;
1.ZS*v = multemb(f,1zs,v1) by Def4
.= f.(z*y) by A1,Def3
.= f.(1.A*y) by A1,A3,FUNCT_1:34
.= v1 by A1,A2,FUNCT_1:35;
hence thesis by A32;
end; then
emb_Ring(f) is well-unital;
hence thesis by A31,A6,A8,A9,A12,A28;
end;
theorem
for A be comRing, X be non empty set, f be Function of A,X
st f is bijective holds emb_Ring(f) is comRing
proof
let A be comRing, X be non empty set, f be Function of A,X;
assume
A1: f is bijective; then
A2: rng f = X by FUNCT_2:def 3;
A3: dom f = [#]A by FUNCT_2:def 1;
reconsider ZS = doubleLoopStr(# X, addemb f, multemb f, f.1.A, f.0.A #)
as non empty doubleLoopStr;
emb_Ring(f) is commutative
proof
for a, b, v being Element of ZS holds a * b = b * a
proof
let a, b be Element of ZS;
reconsider a1 = a, b1 = b as Element of X;
reconsider x = f".a1, y = f".b1 as Element of [#]A by A2,A3,A1,FUNCT_1:32;
reconsider ab1 = (a*b) as Element of X;
a*b = multemb(f,a1,b1) by Def4
.= f.(x*y) by A1,Def3
.= f.(y*x)
.= multemb(f,b1,a1) by A1,Def3
.= b*a by Def4;
hence thesis;
end;
hence thesis;
end;
hence thesis by A1,Th6;
end;
theorem Th8:
for A, B be Ring, i be Function of A,B st i is RingHomomorphism
& i = id A holds A is Subring of B
proof
let A, B be Ring, i be Function of A,B;
assume
A1: i is RingHomomorphism & i = id A; then
A2: i is unity-preserving;
A3: for o be object holds
o in the carrier of A implies o in the carrier of B
proof
let o be object;
assume
A4: o in the carrier of A; then
i.o = o by A1,FUNCT_1:18;
hence thesis by FUNCT_2:5,A4;
end; then
A6: the carrier of A c= the carrier of B;
A7: the addF of A = (the addF of B)||the carrier of A
proof
set aA = the addF of A,
aB = (the addF of B) || the carrier of A;
A8: dom aB = dom(the addF of B) /\ [:the carrier of A,the carrier of A:]
by RELAT_1:61
.= [:the carrier of B,the carrier of B:] /\
[:the carrier of A,the carrier of A:] by FUNCT_2:def 1
.= [:the carrier of A,the carrier of A:] by A6,ZFMISC_1:96,XBOOLE_1:28;
for x be object st x in dom aA holds aA.x = aB.x
proof
let x be object;
assume
A9: x in dom aA; then
consider a,b being object such that
A10: a in the carrier of A & b in the carrier of A & x = [a,b]
by ZFMISC_1:def 2;
reconsider a,b as Element of A by A10;
reconsider a1 = a, b1 = b as Element of B by A3;
A11: i.a = a by A1;
A12: i.b = b by A1;
aA.x = i.(a+b) by A1,A10
.= a1 + b1 by A11,A12,A1,VECTSP_1:def 20
.= aB.x by A9,A10,FUNCT_1:49;
hence thesis;
end;
hence thesis by A8,FUNCT_2:def 1;
end;
A13: the multF of A = (the multF of B)||the carrier of A
proof
set aA = the multF of A,
aB = (the multF of B) || the carrier of A;
A14: dom aB = dom(the multF of B) /\ [:the carrier of A,the carrier of A:]
by RELAT_1:61
.= [:the carrier of B,the carrier of B:] /\
[:the carrier of A,the carrier of A:] by FUNCT_2:def 1
.= [:the carrier of A,the carrier of A:] by A6,ZFMISC_1:96,XBOOLE_1:28;
for x be object st x in dom aA holds aA.x = aB.x
proof
let x be object;
assume
A15: x in dom aA; then
consider a,b being object such that
A16: a in the carrier of A & b in the carrier of A & x = [a,b]
by ZFMISC_1:def 2;
reconsider a,b as Element of A by A16;
reconsider a1 = a, b1 = b as Element of B by A3;
A17: i.a = a by A1;
A18: i.b = b by A1;
A19: i is multiplicative by A1;
aA.x = i.(a*b) by A1,A16
.= a1 * b1 by A19,A17,A18
.= aB.x by A15,A16,FUNCT_1:49;
hence thesis;
end;
hence thesis by A14,FUNCT_2:def 1;
end;
0.B = i.0.A by A1,RING_2:6 .= 0.A by A1;
hence thesis by A1,A2,A6,A7,A13,C0SP1:def 3;
end;
theorem Th9:
for A,B be Ring
for f being Function of A,B st f is monomorphism & ([#]B \ rng f) <> {}
holds
ex C be Ring, X be set, h be Function, G be Function of B,C
st X /\ [#]A = {} & h is one-to-one & dom h = [#]B \ rng f & rng h = X &
[#]C = X \/ [#]A &
A is Subring of C &
G is RingIsomorphism & id A = G*f
proof
let A, B be Ring;
let f be Function of A,B;
assume
A1: f is monomorphism & ([#]B \ rng f) <> {};
A2: dom f = [#]A by FUNCT_2:def 1;
consider X be non empty set such that
A3: [#]A /\ X = {} &
ex h be Function st h is one-to-one & dom h = [#]B \ rng f &
rng h = X by A1,Th2;
consider h be Function such that
A4: h is one-to-one & dom h = [#]B \ rng f & rng h = X
& [#]A /\ X= {} by A3;
defpred P[Element of B,Element of [#]A \/ X] means
($1 in rng f & f".$1 = $2 ) or (not $1 in rng f & $2 = h.$1);
set C1 = [#]A \/ X;
A5: now let y be Element of B;
per cases;
suppose
A6: y in rng f; then
consider x be object such that
A7: x in dom f & y = f.x by FUNCT_1:def 3;
f".y = x by A7,A1,FUNCT_1:34; then
f".y in C1 by A7, XBOOLE_0:def 3;
hence ex x being Element of C1 st P[y,x] by A6;
end;
suppose
A8: not y in rng f; then
y in dom h by A4,XBOOLE_0:def 5; then
h.y in X by A4,FUNCT_1:def 3; then
h.y in C1 by XBOOLE_0:def 3;
hence ex x being Element of C1 st P[y,x] by A8;
end;
end;
consider g being Function of the carrier of B,C1 such that
A10: for x being Element of B holds P[x,g.x] from FUNCT_2:sch 3(A5);
A11: dom g = the carrier of B & rng g c= C1 by FUNCT_2:def 1;
A12: g is bijective
proof
C1 c= rng g
proof
let o;
assume
A13: o in C1; then
per cases by XBOOLE_0:def 3;
suppose
A14: o in [#]A; then
A15: o in dom f by FUNCT_2:def 1;
f.o in [#]B by A14,FUNCT_2:5; then
consider b be Element of B such that
A16: b = f.o;
reconsider x = o as Element of C1 by A13;
P[b,x] by A16, A1,A15,FUNCT_1:3,34; then
g.b = x by A10;
hence thesis by A11, FUNCT_1:3;
end;
suppose o in X; then
consider x be object such that
A18: x in dom h & o = h.x by A4,FUNCT_1:def 3;
reconsider c = o as Element of C1 by A13;
reconsider b = x as Element of B by A4,A18;
P[b,c] by A18, A4,XBOOLE_0:def 5; then
g.b = c by A10;
hence thesis by A11, FUNCT_1:3;
end;
end; then
C1 c= rng g; then
A19: C1 = rng g;
reconsider g as C1-valued Function;
A20: g is onto by A19;
for o1,o2 being object st o1 in dom g & o2 in dom g holds
g.o1 = g.o2 implies o1 = o2
proof
let o1,o2 be object;
assume
A21: o1 in dom g & o2 in dom g;
assume
A22: g.o1 = g.o2;
assume
A23: o1 <> o2;
per cases;
suppose
A24: o1 in rng f & o2 in rng f; then
consider x1 be object such that
A25: x1 in dom f & o1 = f.x1 by FUNCT_1:def 3;
reconsider c1 = x1 as Element of C1 by A25,XBOOLE_0:def 3;
reconsider b1 = o1 as Element of B by A25,FUNCT_2:5;
A26: f".b1 = c1 by A1,A25,FUNCT_1:34;
P[b1,c1] by A24,A1,A25,FUNCT_1:34; then
A27: g.b1 = c1 by A10;
consider x2 be object such that
A28: x2 in dom f & o2 = f.x2 by A24, FUNCT_1:def 3;
reconsider c2 = x2 as Element of C1 by A28, XBOOLE_0:def 3;
reconsider b2 = o2 as Element of B by A28,FUNCT_2:5;
A29: f".b2 = c2 by A1,A28,FUNCT_1:34;
P[b2,c2] by A24,A1,A28,FUNCT_1:34; then
A30: g.b2 = c2 by A10;
A31: b1 in dom (f") & b2 in dom (f") by A24,A1,FUNCT_1:33;
f" is one-to-one by A1;
hence contradiction by A22,A27,A30, A26,A29, A23,A31;
end;
suppose
A33: o1 in rng f & not o2 in rng f; then
consider x1 be object such that
A34: x1 in dom f & o1 = f.x1 by FUNCT_1:def 3;
reconsider c1 = x1 as Element of C1 by A34,XBOOLE_0:def 3;
reconsider b1 = o1 as Element of B by A34,FUNCT_2:5;
A35: P[b1,c1] by A33,A1,A34,FUNCT_1:34;
A36: o2 in [#]B by FUNCT_2:def 1, A21;
o2 in dom h by A36,A4,A33,XBOOLE_0:def 5; then
h.o2 in X by A4,FUNCT_1:def 3; then
consider x2 be Element of X such that
A37: x2 = h.o2;
reconsider c2 = x2 as Element of C1 by XBOOLE_0:def 3;
reconsider b2 = o2 as Element of B by FUNCT_2:def 1, A21;
g.b2 = c2 by A10, A37, A33; then
c1 = c2 by A10,A35,A22;
hence contradiction by A4,A34,XBOOLE_0:def 4;
end;
suppose
A40: not o1 in rng f & o2 in rng f; then
consider x2 be object such that
A41: x2 in dom f & o2 = f.x2 by FUNCT_1:def 3;
reconsider c2 = x2 as Element of C1 by A41, XBOOLE_0:def 3;
reconsider b2 = o2 as Element of B by A41,FUNCT_2:5;
A42: P[b2,c2] by A40,A1,A41,FUNCT_1:34;
A43: o1 in [#]B by FUNCT_2:def 1, A21;
o1 in dom h by A4,A40,XBOOLE_0:def 5, A43; then
h.o1 in X by A4,FUNCT_1:def 3; then
consider x1 be Element of X such that
A44: x1 = h.o1;
reconsider c1 = x1 as Element of C1 by XBOOLE_0:def 3;
reconsider b1 = o1 as Element of B by FUNCT_2:def 1, A21;
g.b1 = c1 by A44, A40, A10; then
c1 = c2 by A10, A42,A22;
hence contradiction by A4,A41,XBOOLE_0:def 4;
end;
suppose
A47: not o1 in rng f & not o2 in rng f;
o1 in [#]B by FUNCT_2:def 1, A21; then
A48: o1 in dom h by A4, A47, XBOOLE_0:def 5;
reconsider b1 = o1 as Element of B by FUNCT_2:def 1, A21;
o2 in [#]B by A21, FUNCT_2:def 1; then
A50: o2 in dom h by A4,A47,XBOOLE_0:def 5;
reconsider b2 = o2 as Element of B by A21, FUNCT_2:def 1;
h.o1 = g.b1 by A10, A47
.= g.b2 by A22
.= h.o2 by A10, A47;
hence contradiction by A48,A50,A23,A4;
end;
end; then
g is one-to-one;
hence thesis by A20;
end;
reconsider C = emb_Ring(g) as non empty Ring by A12,Th6;
A52: [#]C = [#]A \/ X;
reconsider G = g as Function of B,C;
A53: G is linear
proof
for o1, o2 being Element of B holds G.(o1 + o2) = (G.o1) + (G.o2)
& G.(o1 * o2) = (G.o1) * (G.o2)
proof
let o1, o2 be Element of B;
::goal G.o1 + G.o2 = G.(o1+o2) & & G.(o1 * o2) = (G.o1) * (G.o2);
per cases;
suppose
A54: o1 in rng f & o2 in rng f; then
consider x1 be object such that
A55: x1 in dom f & o1 = f.x1 by FUNCT_1:def 3;
reconsider c1 = x1 as Element of C1 by A55, XBOOLE_0:def 3;
reconsider b1 = o1 as Element of B;
A56: P[b1,c1] by A54,A1, A55,FUNCT_1:34;
consider x2 be object such that
A57: x2 in dom f & o2 = f.x2 by A54, FUNCT_1:def 3;
reconsider c2 = x2 as Element of C1 by A57, XBOOLE_0:def 3;
reconsider b2 = o2 as Element of B;
A58: P[b2,c2] by A54, A1, A57, FUNCT_1:34;
reconsider x1,x2 as Element of C1 by A57,A55,XBOOLE_0:def 3;
A59: o1 = g".(g.o1) by A11, A12,FUNCT_1:34 .= g".x1 by A10, A56;
A60: o2 = g".(g.o2) by A11,A12,FUNCT_1:34 .= g".x2 by A10, A58;
A61: G.o1 = x1 by A10, A56;
A62: G.o2 = x2 by A10, A58; then
A63: G.o1 + G.o2 = addemb(g,x1,x2) by Def2,A61
.= g.(o1+o2) by A59,A60,A12,Def1;
G.o1 * G.o2 = multemb(g,x1,x2) by Def4,A61,A62
.= g.(o1 * o2) by A59,A60,A12,Def3;
hence thesis by A63;
end;
suppose
A64: o1 in rng f & not o2 in rng f; then
consider x1 be object such that
A65: x1 in dom f & o1 = f.x1 by FUNCT_1:def 3;
reconsider c1 = x1 as Element of C1 by XBOOLE_0:def 3, A65;
reconsider b1 = o1 as Element of B;
A66: P[b1,c1] by A64, A1,A65,FUNCT_1:34;
o2 in dom h by A4,A64,XBOOLE_0:def 5; then
h.o2 in X by A4,FUNCT_1:def 3; then
consider x2 be Element of X such that
A67: x2 = h.o2;
reconsider c2 = x2 as Element of C1 by XBOOLE_0:def 3;
reconsider b2 = o2 as Element of B;
reconsider x1,x2 as Element of C1 by A65,XBOOLE_0:def 3;
A68: o1 = g".(g.o1) by A11, A12,FUNCT_1:34 .= g".x1 by A10, A66;
A69: o2 = g".(g.o2) by A11, A12,FUNCT_1:34 .= g".x2 by A10,A67,A64;
A70: G.o1 = x1 by A10, A66;
A71: G.o2 = x2 by A10, A67, A64; then
A72: G.o1 + G.o2 = addemb(g,x1,x2) by Def2,A70
.= g.(o1+o2) by A68,A69,A12,Def1;
G.o1 * G.o2 = multemb(g,x1,x2) by Def4,A70,A71
.= g.(o1 * o2) by A68,A69,A12,Def3;
hence thesis by A72;
end;
suppose
A73: not o1 in rng f & o2 in rng f; then
o1 in dom h by A4,XBOOLE_0:def 5; then
h.o1 in X by A4,FUNCT_1:def 3; then
consider x1 be Element of X such that
A74: x1 = h.o1;
reconsider c1 = x1 as Element of C1 by XBOOLE_0:def 3;
reconsider b1 = o1 as Element of B;
consider x2 be object such that
A75: x2 in dom f & o2 = f.x2 by A73, FUNCT_1:def 3;
reconsider c2 = x2 as Element of C1 by A75, XBOOLE_0:def 3;
reconsider b2 = o2 as Element of B;
A76: P[b2,c2] by A73,A1, A75, FUNCT_1:34;
reconsider x1,x2 as Element of C1 by A75,XBOOLE_0:def 3;
A77: o1 = g".(g.o1) by A11, A12,FUNCT_1:34
.= g".x1 by A10,A74,A73;
A78: o2 = g".(g.o2) by A11, A12,FUNCT_1:34 .= g".x2 by A10,A76;
A79: G.o2 = x2 by A10,A76;
A80: G.o1 = x1 by A10,A74,A73; then
A81: G.o1 + G.o2 = addemb(g,x1,x2) by Def2,A79
.= g.(o1+o2) by A78,A77,A12,Def1;
G.o1 * G.o2 = multemb(g,x1,x2) by Def4,A79,A80
.= g.(o1 * o2) by A78,A77,A12,Def3;
hence thesis by A81;
end;
suppose
A82: not o1 in rng f & not o2 in rng f; then
o1 in dom h by A4,XBOOLE_0:def 5; then
h.o1 in X by A4,FUNCT_1:def 3; then
consider x1 be Element of X such that
A83: x1 = h.o1;
reconsider c1 = x1 as Element of C1 by XBOOLE_0:def 3;
reconsider b1 = o1 as Element of B;
o2 in dom h by A4,A82,XBOOLE_0:def 5; then
h.o2 in X by A4,FUNCT_1:def 3; then
consider x2 be Element of X such that
A84: x2 = h.o2;
reconsider c2 = x2 as Element of C1 by XBOOLE_0:def 3;
reconsider b2 = o2 as Element of B;
reconsider x1,x2 as Element of C1 by XBOOLE_0:def 3;
A85: o1 = g".(g.o1) by A11, A12,FUNCT_1:34
.= g".x1 by A10, A83, A82;
A86: o2 = g".(g.o2) by A11,A12,FUNCT_1:34
.= g".x2 by A10, A84, A82;
A87: G.o1 = x1 by A10, A83, A82;
A88: G.o2 = x2 by A10, A84, A82; then
A89: G.o1 + G.o2 = addemb(g,x1,x2) by Def2,A87
.= g.(o1+o2) by A86,A85,A12,Def1;
G.o1 * G.o2 = multemb(g,x1,x2) by Def4,A87,A88
.= g.(o1 * o2) by A86,A85,A12,Def3;
hence thesis by A89;
end;
end; then
A90: G is additive & G is multiplicative;
G is unity-preserving;
hence thesis by A90;
end;
A91: for o st o in [#]A holds (G*f).o = o
proof
let o;
assume
A92: o in [#]A; then
A93: f.o in rng f by A2,FUNCT_1:3;
reconsider c1 = o as Element of C1 by A92,XBOOLE_0:def 3;
reconsider b1 = f.o as Element of B by A93;
A94: P[b1,c1] by A92,A2,FUNCT_1:3,A1,FUNCT_1:34;
(G*f).o = G.b1 by A2,A92,FUNCT_1:13
.= c1 by A10,A94;
hence thesis;
end;
rng(id [#]A) c= [#]A \/ X by XBOOLE_1:7; then
reconsider i = id A as Function of dom(id A), C by FUNCT_2:2;
i is Function of A, C;then
reconsider i = id A as Function of A, C;
A96: G*f = i by A91;
G*f is RingHomomorphism by A1,A53,QUOFIELD:54; then
A is Subring of C by Th8, A96;
hence thesis by A4, A52, A96, A12, A53;
end;
::$N Embedding Principle Applied to AbGroups.
definition
let G be AbGroup;
mode SubAbGr of G -> AbGroup means
:Def6:
the carrier of it c= the carrier of G &
the addF of it = (the addF of G)||the carrier of it & 0.it = 0.G;
existence
proof
take G;
thus thesis;
end;
end;
Lm1: for R,S being AbGroup,
f be Homomorphism of R,S holds 0.S in rng f
proof
let R,S be AbGroup, f be Homomorphism of R,S;
A1: f.(0.R) = 0.S by MOD_4:40;
dom f = the carrier of R by FUNCT_2:def 1;
hence 0.S in rng f by A1,FUNCT_1:def 3;
end;
Lm2: for R,S being AbGroup,
f being Homomorphism of R,S holds rng f is Preserv of the addF of S
proof
let R,S be AbGroup, f be Homomorphism of R,S;
set F = rng f; set A = the addF of S;
now let x be set;
assume x in [:F,F:]; then
consider a,b being object such that
A1: a in F and
A2: b in F and
A3: x = [a,b] by ZFMISC_1:def 2;
consider a1 being Element of S such that
A4: a1 = a & a1 in rng f by A1;
consider x1 being object such that
A5: x1 in dom f & f.x1 = a1 by A4,FUNCT_1:def 3;
reconsider x1 as Element of R by A5;
consider a2 being Element of S such that
A6: a2 = b & a2 in rng f by A2;
consider x2 being object such that
A7: x2 in dom f & f.x2 = a2 by A6,FUNCT_1:def 3;
reconsider x2 as Element of R by A7;
A8: dom f = the carrier of R by FUNCT_2:def 1;
f.(x1+x2) = a1 + a2 by A7,A5,VECTSP_1:def 20 .= A.x by A3,A4,A6;
hence A.x in rng f by A8,FUNCT_1:def 3;
end;
hence thesis by REALSET1:def 1;
end;
definition
let G,H be AbGroup, f be Homomorphism of G,H;
func Image f -> strict addLoopStr means
the carrier of it = rng f &
the addF of it = (the addF of H)||(rng f) &
the ZeroF of it = 0.H;
existence
proof
set A = the addF of H;
reconsider P = rng f as Preserv of A by Lm2;
reconsider Z = 0.H as Element of P by Lm1;
take addLoopStr(#P,A||P,Z#);
thus thesis;
end;
uniqueness;
end;
theorem Th10:
for A be AbGroup, X be non empty set, f be Function of A,X,
a,b be Element of X st f is bijective holds
f.((the addF of A).(f".a,f".b)) is Element of X
proof
let A be AbGroup, X be non empty set, f be Function of A,X;
let a,b be Element of X;
assume
A1: f is bijective; then
A2: rng f = X by FUNCT_2:def 3;
dom f = [#]A by FUNCT_2:def 1; then
reconsider x = f".a, y = f".b as Element of [#]A by A2,A1,FUNCT_1:32;
reconsider z = (the addF of A).(x,y) as Element of [#]A;
f.z in X;
hence thesis;
end;
definition
let A be AbGroup, X be non empty set;
let f be Function of A,X;
let a,b be Element of X;
assume
A1: f is bijective;
func addemb(f,a,b) -> Element of X equals :Def8:
f.((the addF of A).(f".a,f".b));
coherence by A1,Th10;
end;
theorem Th11:
for A be AbGroup, X be non empty set, f be Function of A,X,
a,b,c be Element of X st f is bijective holds
addemb(f,a,addemb(f,b,c)) = addemb(f,addemb(f,a,b),c)
proof
let A be AbGroup, X be non empty set, f be Function of A,X;
let a,b,c be Element of X;
assume
A1: f is bijective; then
A2: rng f = X by FUNCT_2:def 3;
A3: dom f = [#]A by FUNCT_2:def 1;
reconsider x=f".a, y=f".b, z=f".c as Element of [#]A by A3,A2,A1,FUNCT_1:32;
A4: addemb(f,a,b) = f.((the addF of A).(f".a,f".b)) by A1,Def8;
addemb(f,b,c) = f.((the addF of A).(f".b,f".c)) by A1,Def8; then
reconsider ab1 = f.((the addF of A).(f".a,f".b)),
bc1 = f.((the addF of A).(f".b,f".c)) as Element of X by A4;
addemb(f,a,addemb(f,b,c)) = addemb(f,a,bc1) by A1,Def8
.= f.((the addF of A).(f".a,f".bc1)) by A1,Def8
.= f.(x+(y+z)) by A1,A3,FUNCT_1:34
.= f.((x+y)+z) by RLVECT_1:def 3
.= f.((the addF of A).(f".ab1,f".c)) by A1,A3,FUNCT_1:34
.= addemb(f,ab1,c) by A1,Def8
.= addemb(f,addemb(f,a,b),c) by A1,Def8;
hence thesis;
end;
definition
let A be AbGroup, X be non empty set;
let f be Function of A,X;
func addemb f -> BinOp of X means
:Def9:
for a,b being Element of X holds it.(a,b) = addemb(f,a,b);
existence
proof
deffunc O(Element of X,Element of X) = addemb(f,$1,$2);
consider F being BinOp of X such that
A1: for a,b being Element of X holds F.(a,b)=O(a,b) from BINOP_1:sch 4;
take F;
thus thesis by A1;
end;
uniqueness
proof
let F1,F2 be BinOp of X such that
A2: for a,b being Element of X holds F1.(a,b) = addemb(f,a,b) and
A3: for a,b being Element of X holds F2.(a,b) = addemb(f,a,b);
now let a,b be Element of X;
thus F1.(a,b) = addemb(f,a,b) by A2 .= F2.(a,b) by A3;
end;
hence thesis;
end;
end;
definition
let A be AbGroup, X be non empty set;
let f be Function of A,X;
func emb_AbGr(f) -> strict non empty addLoopStr equals
addLoopStr(# X, addemb f, f.0.A #);
coherence;
end;
theorem Th12:
for A be AbGroup, X be non empty set, f be Function of A,X
st f is bijective holds emb_AbGr(f) is AbGroup
proof
let A be AbGroup, X be non empty set, f be Function of A,X;
assume
A1: f is bijective; then
A2: rng f = X by FUNCT_2:def 3;
A3: dom f = [#]A by FUNCT_2:def 1;
reconsider ZS = addLoopStr(# X, addemb f, f.0.A #) as non empty addLoopStr;
A5: for v, w being Element of ZS holds v + w = w + v
proof
let v, w be Element of ZS;
reconsider v1 = v, w1 = w as Element of X;
reconsider x = f".v1, y = f".w1 as Element of [#]A by A2,A3,A1,FUNCT_1:32;
v + w = addemb(f,v1,w1) by Def9
.= f.(x+y) by A1,Def8
.= f.(y+x)
.= addemb(f,w1,v1) by A1,Def8
.= w + v by Def9;
hence thesis;
end;
A6: emb_AbGr(f) is Abelian by A5;
A7: for u, v, w being Element of ZS holds u+(v+w) = (u+v)+w
proof
let u, v, w be Element of ZS;
reconsider u1 = u, v1 = v, w1 = w as Element of X;
u+(v+w) = addemb(f,u1, (addemb f).(v1,w1)) by Def9
.= addemb(f,u1, addemb(f,v1,w1)) by Def9
.= addemb(f,addemb(f,u1,v1),w1) by A1,Th11
.= addemb(f,(addemb f).(u1,v1),w1) by Def9
.= (u+v)+w by Def9;
hence thesis;
end;
A8: emb_AbGr(f) is add-associative by A7;
for v being Element of ZS holds v + 0.ZS = v
proof
let v be Element of ZS;
reconsider v1 = v as Element of X;
reconsider x = f".v1 as Element of [#]A by A2,A3,A1,FUNCT_1:32;
v + 0.ZS = addemb(f,v1,f.0.A) by Def9
.= f.((the addF of A).(f".v1,f".(f.0.A))) by A1,Def8
.= f.(x+0.A) by A1,A3, FUNCT_1:34
.= v1 by A1,A2,FUNCT_1:35;
hence thesis;
end; then
A9: emb_AbGr(f) is right_zeroed;
A10: for v being Element of ZS holds v is right_complementable
proof
let v be Element of ZS;
reconsider v1 = v as Element of X;
reconsider x = f".v1 as Element of A by A2,A3,A1,FUNCT_1:32;
consider u be Element of ZS such that
A11: u = f.(-x);
reconsider u1 = u as Element of X;
v+u = addemb(f,v1,u1) by Def9
.= f.((the addF of A).(f".v1,f".u1)) by A1,Def8
.= f.(x + (-x)) by A11,A3,A1,FUNCT_1:34
.= 0.ZS by RLVECT_1:5;
hence thesis;
end;
emb_AbGr(f) is right_complementable by A10;
hence thesis by A6,A8,A9;
end;
theorem Th13:
for A, B be AbGroup, i be Homomorphism of A,B st
i = id A holds A is SubAbGr of B
proof
let A, B be AbGroup, i be Homomorphism of A,B;
assume
A1: i = id A;
A2: for o be object holds
o in the carrier of A implies o in the carrier of B
proof
let o be object;
assume
A3: o in the carrier of A; then
i.o = o by A1,FUNCT_1:18;
hence thesis by FUNCT_2:5,A3;
end;
A5: the carrier of A c= the carrier of B by A2;
A6: the addF of A = (the addF of B)||the carrier of A
proof
set aA = the addF of A,
aB = (the addF of B) || the carrier of A;
A7: dom aB = dom(the addF of B) /\ [:the carrier of A,the carrier of A:]
by RELAT_1:61
.= [:the carrier of B,the carrier of B:] /\
[:the carrier of A,the carrier of A:] by FUNCT_2:def 1
.= [:the carrier of A,the carrier of A:] by A5,ZFMISC_1:96,XBOOLE_1:28;
for x be object st x in dom aA holds aA.x = aB.x
proof
let x be object;
assume
A8: x in dom aA; then
consider a,b being object such that
A9: a in the carrier of A & b in the carrier of A & x = [a,b]
by ZFMISC_1:def 2;
reconsider a,b as Element of A by A9;
reconsider a1 = a, b1 = b as Element of B by A2;
A10: i.a = a by A1;
A11: i.b = b by A1;
aA.x = i.(a+b) by A1,A9
.= a1 + b1 by A10,A11,VECTSP_1:def 20
.= aB.x by A8,A9,FUNCT_1:49;
hence thesis;
end;
hence thesis by A7,FUNCT_2:def 1;
end;
0.B = i.0.A by MOD_4:40 .= 0.A by A1;
hence thesis by A5,A6,Def6;
end;
theorem
for A,B be AbGroup
for f being Homomorphism of A,B st f is one-to-one & ([#]B \ rng f) <> {}
holds
ex C be AbGroup, X be set, h be Function, G be Function of B,C
st X /\ [#]A = {} & h is one-to-one & dom h = [#]B \ rng f & rng h = X &
[#]C = X \/ [#]A &
A is SubAbGr of C &
G is Homomorphism of B,C & id A = G*f
proof
let A, B be AbGroup;
let f be Homomorphism of A,B;
assume
A1: f is one-to-one & ([#]B \ rng f) <> {};
A2: dom f = [#]A by FUNCT_2:def 1;
consider X be non empty set such that
A3: [#]A /\ X = {} &
ex h be Function st h is one-to-one & dom h = [#]B \ rng f &
rng h = X by A1,Th2;
consider h be Function such that
A4: h is one-to-one & dom h = [#]B \ rng f & rng h = X
& [#]A /\ X= {} by A3;
defpred P[Element of B,Element of [#]A \/ X] means
($1 in rng f & f".$1 = $2 ) or (not $1 in rng f & $2 = h.$1);
set C1 = [#]A \/ X;
A5: now let y be Element of B;
per cases;
suppose
A6: y in rng f; then
consider x be object such that
A7: x in dom f & y = f.x by FUNCT_1:def 3;
f".y = x by A7,A1,FUNCT_1:34; then
f".y in C1 by A7, XBOOLE_0:def 3;
hence ex x being Element of C1 st P[y,x] by A6;
end;
suppose
A8: not y in rng f; then
y in dom h by A4,XBOOLE_0:def 5; then
h.y in X by A4,FUNCT_1:def 3; then
h.y in C1 by XBOOLE_0:def 3;
hence ex x being Element of C1 st P[y,x] by A8;
end;
end;
consider g being Function of the carrier of B,C1 such that
A10: for x being Element of B holds P[x,g.x] from FUNCT_2:sch 3(A5);
A11: dom g = the carrier of B & rng g c= C1 by FUNCT_2:def 1;
A12: g is bijective
proof
for o holds o in C1 implies o in rng g
proof
let o;
assume
A13: o in C1; then
per cases by XBOOLE_0:def 3;
suppose
A14: o in [#]A; then
A15: o in dom f by FUNCT_2:def 1;
f.o in [#]B by A14,FUNCT_2:5; then
consider b be Element of B such that
A16: b = f.o;
reconsider x = o as Element of C1 by A13;
P[b,x] by A16, A1,A15,FUNCT_1:3,34; then
g.b = x by A10;
hence thesis by A11, FUNCT_1:3;
end;
suppose o in X; then
consider x be object such that
A18: x in dom h & o = h.x by A4,FUNCT_1:def 3;
reconsider c = o as Element of C1 by A13;
reconsider b = x as Element of B by A4,A18;
P[b,c] by A18, A4,XBOOLE_0:def 5; then
g.b = c by A10;
hence thesis by A11, FUNCT_1:3;
end;
end; then
C1 c= rng g; then
A19: C1 = rng g;
reconsider g as C1-valued Function;
A20: g is onto by A19;
for o1,o2 being object st o1 in dom g & o2 in dom g holds
g.o1 = g.o2 implies o1= o2
proof
let o1,o2 be object;
assume
A21: o1 in dom g & o2 in dom g;
assume
A22: g.o1 = g.o2;
assume
A23: o1 <> o2;
per cases;
suppose
A24: o1 in rng f & o2 in rng f; then
consider x1 be object such that
A25: x1 in dom f & o1 = f.x1 by FUNCT_1:def 3;
reconsider c1 = x1 as Element of C1 by A25,XBOOLE_0:def 3;
reconsider b1 = o1 as Element of B by A25,FUNCT_2:5;
A26: f".b1 = c1 by A1,A25,FUNCT_1:34;
P[b1,c1] by A24,A1,A25,FUNCT_1:34; then
A27: g.b1 = c1 by A10;
consider x2 be object such that
A28: x2 in dom f & o2 = f.x2 by A24, FUNCT_1:def 3;
reconsider c2 = x2 as Element of C1 by A28, XBOOLE_0:def 3;
reconsider b2 = o2 as Element of B by A28,FUNCT_2:5;
A29: f".b2 = c2 by A1,A28,FUNCT_1:34;
P[b2,c2] by A24,A1,A28,FUNCT_1:34; then
A30: g.b2 = c2 by A10;
A31: b1 in dom (f") & b2 in dom (f") by A24,A1,FUNCT_1:33;
f" is one-to-one by A1;
hence contradiction by A22,A27,A30, A26,A29, A23,A31;
end;
suppose
A33: o1 in rng f & not o2 in rng f; then
consider x1 be object such that
A34: x1 in dom f & o1 = f.x1 by FUNCT_1:def 3;
reconsider c1 = x1 as Element of C1 by A34,XBOOLE_0:def 3;
reconsider b1 = o1 as Element of B by A34,FUNCT_2:5;
A35: P[b1,c1] by A33,A1,A34,FUNCT_1:34;
o2 in [#]B by FUNCT_2:def 1, A21; then
o2 in dom h by A4,A33,XBOOLE_0:def 5; then
h.o2 in X by A4,FUNCT_1:def 3; then
consider x2 be Element of X such that
A37: x2 = h.o2;
reconsider c2 = x2 as Element of C1 by XBOOLE_0:def 3;
reconsider b2 = o2 as Element of B by FUNCT_2:def 1, A21;
g.b2 = c2 by A10, A37, A33; then
c1 = c2 by A10,A35,A22;
hence contradiction by A4,A34,XBOOLE_0:def 4;
end;
suppose
A40: not o1 in rng f & o2 in rng f; then
consider x2 be object such that
A41: x2 in dom f & o2 = f.x2 by FUNCT_1:def 3;
reconsider c2 = x2 as Element of C1 by A41, XBOOLE_0:def 3;
reconsider b2 = o2 as Element of B by A41,FUNCT_2:5;
A42: P[b2,c2] by A40,A1,A41,FUNCT_1:34;
A43: o1 in [#]B by FUNCT_2:def 1, A21;
o1 in dom h by A4,A40,XBOOLE_0:def 5, A43; then
h.o1 in X by A4,FUNCT_1:def 3; then
consider x1 be Element of X such that
A44: x1 = h.o1;
reconsider c1 = x1 as Element of C1 by XBOOLE_0:def 3;
reconsider b1 = o1 as Element of B by FUNCT_2:def 1, A21;
A45: g.b1 = c1 by A44, A40, A10;
c1 = c2 by A45,A10, A42,A22;
hence contradiction by A4, A41,XBOOLE_0:def 4;
end;
suppose
A47: not o1 in rng f & not o2 in rng f;
o1 in [#]B by FUNCT_2:def 1, A21; then
A48: o1 in dom h by A4, A47, XBOOLE_0:def 5;
reconsider b1 = o1 as Element of B by FUNCT_2:def 1, A21;
o2 in [#]B by A21, FUNCT_2:def 1; then
A50: o2 in dom h by A4,A47,XBOOLE_0:def 5;
reconsider b2 = o2 as Element of B by A21, FUNCT_2:def 1;
h.o1 = g.b1 by A10, A47
.= g.b2 by A22
.= h.o2 by A10, A47;
hence contradiction by A48,A50,A23,A4;
end;
end; then
g is one-to-one;
hence thesis by A20;
end;
reconsider C = emb_AbGr(g) as non empty AbGroup by A12,Th12;
A52: [#]C = [#]A \/ X;
reconsider G = g as Function of B,C;
G is additive
proof
for o1, o2 being Element of B holds G.(o1 + o2) = (G.o1) + (G.o2)
proof
let o1, o2 be Element of B;
per cases;
suppose
A53: o1 in rng f & o2 in rng f; then
consider x1 be object such that
A54: x1 in dom f & o1 = f.x1 by FUNCT_1:def 3;
reconsider c1 = x1 as Element of C1 by A54, XBOOLE_0:def 3;
reconsider b1 = o1 as Element of B;
A55: P[b1,c1] by A53,A1, A54,FUNCT_1:34;
consider x2 be object such that
A56: x2 in dom f & o2 = f.x2 by A53, FUNCT_1:def 3;
reconsider c2 = x2 as Element of C1 by A56, XBOOLE_0:def 3;
reconsider b2 = o2 as Element of B;
A57: P[b2,c2] by A53, A1, A56, FUNCT_1:34;
reconsider x1,x2 as Element of C1 by A56,A54,XBOOLE_0:def 3;
A58: o1 = g".(g.o1) by A11, A12,FUNCT_1:34 .= g".x1 by A10, A55;
A59: o2 = g".(g.o2) by A11,A12,FUNCT_1:34 .= g".x2 by A10, A57;
A60: G.o1 = x1 by A10, A55;
G.o2 = x2 by A10, A57; then
G.o1 + G.o2 = addemb(g,x1,x2) by Def9,A60
.= g.(o1+o2) by A58,A59,A12,Def8;
hence thesis;
end;
suppose
A62: o1 in rng f & not o2 in rng f; then
consider x1 be object such that
A63: x1 in dom f & o1 = f.x1 by FUNCT_1:def 3;
reconsider c1 = x1 as Element of C1 by XBOOLE_0:def 3, A63;
reconsider b1 = o1 as Element of B;
A64: P[b1,c1] by A62, A1,A63,FUNCT_1:34;
o2 in dom h by A4,A62,XBOOLE_0:def 5; then
h.o2 in X by A4,FUNCT_1:def 3; then
consider x2 be Element of X such that
A65: x2 = h.o2;
reconsider c2 = x2 as Element of C1 by XBOOLE_0:def 3;
reconsider b2 = o2 as Element of B;
reconsider x1,x2 as Element of C1 by A63,XBOOLE_0:def 3;
A66: o1 = g".(g.o1) by A11, A12,FUNCT_1:34 .= g".x1 by A10, A64;
A67: o2 = g".(g.o2) by A11, A12,FUNCT_1:34 .= g".x2 by A10,A65,A62;
A68: G.o1 = x1 by A10, A64;
G.o2 = x2 by A10, A65, A62; then
G.o1 + G.o2 = addemb(g,x1,x2) by Def9,A68
.= g.(o1+o2) by A66,A67,A12,Def8;
hence thesis;
end;
suppose
A70: not o1 in rng f & o2 in rng f; then
o1 in dom h by A4,XBOOLE_0:def 5; then
h.o1 in X by A4,FUNCT_1:def 3; then
consider x1 be Element of X such that
A71: x1 = h.o1;
reconsider c1 = x1 as Element of C1 by XBOOLE_0:def 3;
reconsider b1 = o1 as Element of B;
consider x2 be object such that
A72: x2 in dom f & o2 = f.x2 by A70, FUNCT_1:def 3;
reconsider c2 = x2 as Element of C1 by A72, XBOOLE_0:def 3;
reconsider b2 = o2 as Element of B;
A73: P[b2,c2] by A70,A1, A72, FUNCT_1:34;
reconsider x1,x2 as Element of C1 by A72,XBOOLE_0:def 3;
A74: o1 = g".(g.o1) by A11, A12,FUNCT_1:34
.= g".x1 by A10,A71,A70;
A75: o2 = g".(g.o2) by A11, A12,FUNCT_1:34 .= g".x2 by A10,A73;
A76: G.o2 = x2 by A10,A73;
G.o1 = x1 by A10,A71,A70; then
G.o1 + G.o2 = addemb(g,x1,x2) by Def9,A76
.= g.(o1+o2) by A75,A74,A12,Def8;
hence thesis;
end;
suppose
A78: not o1 in rng f & not o2 in rng f; then
o1 in dom h by A4,XBOOLE_0:def 5; then
h.o1 in X by A4,FUNCT_1:def 3; then
consider x1 be Element of X such that
A79: x1 = h.o1;
reconsider c1 = x1 as Element of C1 by XBOOLE_0:def 3;
reconsider b1 = o1 as Element of B;
o2 in dom h by A4,A78,XBOOLE_0:def 5; then
h.o2 in X by A4,FUNCT_1:def 3; then
consider x2 be Element of X such that
A80: x2 = h.o2;
reconsider c2 = x2 as Element of C1 by XBOOLE_0:def 3;
reconsider b2 = o2 as Element of B;
reconsider x1,x2 as Element of C1 by XBOOLE_0:def 3;
A81: o1 = g".(g.o1) by A11, A12,FUNCT_1:34
.= g".x1 by A10, A79, A78;
A82: o2 = g".(g.o2) by A11,A12,FUNCT_1:34
.= g".x2 by A10, A80, A78;
A83: G.o1 = x1 by A10, A79, A78;
A84: G.o2 = x2 by A10, A80, A78;
G.o1 + G.o2 = addemb(g,x1,x2) by Def9,A83,A84
.= g.(o1+o2) by A82,A81,A12,Def8;
hence thesis;
end;
end;
hence thesis;
end; then
reconsider G as Homomorphism of B,C;
A85: for o st o in [#]A holds (G*f).o = o
proof
let o;
assume
A86: o in [#]A; then
A87: f.o in rng f by A2,FUNCT_1:3;
reconsider c1 = o as Element of C1 by A86,XBOOLE_0:def 3;
reconsider b1 = f.o as Element of B by A87;
A88: P[b1,c1] by A86,A2,FUNCT_1:3,A1,FUNCT_1:34;
(G*f).o = G.b1 by A2,A86,FUNCT_1:13
.= c1 by A10,A88;
hence thesis;
end;
A89: rng(id [#]A) c= [#]A \/ X by XBOOLE_1:7;
reconsider i = id A as Function of dom(id A), C by A89,FUNCT_2:2;
i is Function of A, C;then
reconsider i = id A as Function of A, C;
A90: G*f = i by A85;
A91: G*f is Homomorphism of A,C by GROUP_14:6;
A is SubAbGr of C by Th13, A90, A91;
hence thesis by A4, A52, A90;
end;
::$N Relation with Polynomial Rings
theorem Th15:
for b be bag of 0 holds dom b = {} & b = EmptyBag {} & rng b = 0 &
EmptyBag {} = {} --> 0 & Bags {} = {EmptyBag {}}
proof
let b be bag of 0;
Bags {} = {EmptyBag {}}
proof
for o st o in Bags {} holds o in {EmptyBag {}}
proof
let o;
assume o in Bags {}; then
o = EmptyBag {};
hence thesis by TARSKI:def 1;
end; then
Bags {} c= {EmptyBag {}};
hence thesis;
end;
hence thesis;
end;
reserve R for right_zeroed add-associative right_complementable Abelian
well-unital distributive associative non trivial non trivial doubleLoopStr;
theorem
for f be Polynomial of 0,R holds dom f = Bags 0 & Bags 0 = {{}}
& rng f = {f.(EmptyBag 0)}
proof
let f be Polynomial of 0,R;
dom f = Bags 0 by FUNCT_2:def 1;
hence thesis by Th15,FUNCT_1:4;
end;
theorem Th17:
for f be Polynomial of 0,R holds f is Constant
proof
let f be Polynomial of 0,R;
assume not f is Constant; then
consider b being bag of 0 such that
A2: b <> EmptyBag 0 & f.b <> 0.R by POLYNOM7:def 7;
b = EmptyBag 0;
hence contradiction by A2;
end;
theorem
for f be Polynomial of 0,R holds ex a being Element of R st f = a |(0,R)
proof
let f be Polynomial of 0,R;
f is Constant by Th17;
hence thesis by POLYNOM7:17;
end;
definition
let R;
func 1_1(R) -> sequence of R equals
(0_.R) +* (1,1.R);
coherence;
end;
theorem
for R be non degenerated comRing holds Support(1_1(R)) = {1}
proof
let R be non degenerated comRing;
A1: for o holds o in Support(1_1(R)) implies o in {1}
proof
let o;
assume
A2: o in Support(1_1(R)); then
reconsider x = o as Element of NAT;
x = 1
proof
assume x <> 1; then
((0_.R) +* (1,1.R)).x = (0_.R).x by FUNCT_7:32
.= 0.R;
hence contradiction by A2,POLYNOM1:def 4;
end;
hence thesis by TARSKI:def 1;
end;
for o holds o in {1} implies o in Support(1_1(R))
proof
let o;
assume
A4: o in {1}; then
A5: o = 1 by TARSKI:def 1;
A6: o in dom (0_.R) by A4; then
A7: o in dom((0_.R) +* (1,1.R)) by FUNCT_7:30;
((0_.R) +* (1,1.R)).o = 1.R by A5,A6,FUNCT_7:31;
hence thesis by A7,POLYNOM1:def 3;
end;
hence thesis by A1,TARSKI:2;
end;
registration
let R;
cluster 1_1(R) -> finite-Support;
coherence;
end;
theorem Th20:
Leading-Monomial(1_1(R)) = 1_1(R)
proof
A1: 1 in dom(0_.(R));
A2: len 1_1(R) = 1+1 by NIVEN:20;
Leading-Monomial(1_1(R))
= 0_.(R)+*(len(1_1(R))-'1,(1_1(R)).(len(1_1(R))-'1)) by POLYNOM4:11
.= 1_1(R) by A2,A1,FUNCT_7:31;
hence thesis;
end;
theorem
for m be Element of R holds eval(1_1(R),m) = m
proof
let m be Element of R;
A1: len 1_1(R) = 1+1 by NIVEN:20;
A2: 1 in dom(0_.(R));
eval(1_1(R),m) = eval (Leading-Monomial(1_1(R)),m) by Th20
.= (1_1(R)).(len(1_1(R))-'1)*(power R).(m,len(1_1(R))-'1) by POLYNOM4:22
.= 1.R * (power R).(m,1) by A1,A2,FUNCT_7:31
.= (power R).(m,0+1)
.= power(R).(m,0) * m by GROUP_1:def 7
.= 1_R * m by GROUP_1:def 7
.= m;
hence thesis;
end;
reserve R for non degenerated comRing;
theorem Th22:
for p0 be Element of Polynom-Ring(0,R) holds
not p0 is Polynomial of Polynom-Ring(0,R)
proof
let p0 be Element of Polynom-Ring(0,R);
reconsider P0 = p0 as Series of 0,R by POLYNOM1:def 11;
not p0 in [#]Polynom-Ring(Polynom-Ring(0,R))
proof
assume
p0 in [#]Polynom-Ring(Polynom-Ring(0,R)); then
reconsider P1 = p0 as sequence of Polynom-Ring(0,R) by POLYNOM3:def 10;
A2: dom P1 = NAT by FUNCT_2:def 1;
1 --> 0 in Bags 1 by PRE_POLY:def 12; then
dom P0 <> dom P1 by A2;
hence contradiction;
end;
hence thesis by POLYNOM3:def 10;
end;
theorem
for R being non degenerated comRing holds
Polynom-Ring (Polynom-Ring(0,R)),Polynom-Ring(1,R) are_isomorphic
proof
let R be non degenerated comRing;
ex P being Function
of Polynom-Ring (Polynom-Ring(0,R)),Polynom-Ring(0+1,R) st
P is RingIsomorphism by HILBASIS:31;
hence thesis by QUOFIELD:def 23;
end;
::ThQ3:
:: for R being non degenerated comRing holds
:: Polynom-Ring(1,R),Polynom-Ring R are_isomorphic
:: proof
:: let R being non degenerated comRing;
:: BSPoly(R) is RingIsomorphism;
:: hence thesis by QUOFIELD:def 23;
:: end;
::ThQ4:
:: for R being non degenerated comRing holds
:: Polynom-Ring(Polynom-Ring(0,R)),Polynom-Ring R are_isomorphic
:: proof
:: let R being non degenerated comRing;
::A1: Polynom-Ring (Polynom-Ring(0,R)),Polynom-Ring(1,R) are_isomorphic by ThQ1;
:: Polynom-Ring(1,R),Polynom-Ring R are_isomorphic by ThQ3;
:: hence thesis by A1,RING_3:44;
:: end;
theorem Th24:
for R be non degenerated Ring holds
[#]Polynom-Ring R \ rng (canHom R) <> {}
proof
let R be non degenerated Ring;
reconsider p = 0_.(R) +*(1,1.R) as Polynomial of R;
assume [#]Polynom-Ring R \ rng (canHom R) = {}; then
A2: [#]Polynom-Ring R c= rng (canHom R) by XBOOLE_1:37;
p in [#]Polynom-Ring R by POLYNOM3:def 10; then
consider x be object such that
A4: x in dom canHom R & (canHom R).x = p by A2,FUNCT_1:def 3;
reconsider x0 = x as Element of R by A4;
A5: p = x0|R by A4,RING_4:def 6
.= 0_.(R) +*(0,x) by RING_4:def 5;
1 in dom(0_.(R)); then
1.R = (0_.(R) +*(0,x)).1 by A5,FUNCT_7:31
.= (0_.(R)).1 by FUNCT_7:32 .= 0.R;
hence contradiction;
end;
theorem Th25:
for R be non degenerated Ring holds
ex PR be non degenerated Ring, X be set, h be Function,
G be Function of Polynom-Ring R,PR
st R is Subring of PR & G is RingIsomorphism & id R = G*(canHom R) &
X /\ [#]R = {} & h is one-to-one &
dom h = [#]Polynom-Ring R \ rng (canHom R) & rng h = X &
[#]PR = X \/ [#]R
proof
let R be non degenerated Ring;
consider PR be Ring, X be set, h be Function,
G be Function of Polynom-Ring R,PR such that
A1: X /\ [#]R = {} & h is one-to-one &
dom h = [#]Polynom-Ring R \ rng (canHom R) & rng h = X &
[#]PR = X \/ [#]R & R is Subring of PR &
G is RingIsomorphism & id R = G*(canHom R) by Th24, Th9;
A2: 1.PR = 1.R & 0.PR = 0.R by A1,C0SP1:def 3;
PR is non degenerated Ring by A2,STRUCT_0:def 8;
hence thesis by A1;
end;
theorem
[#]Polynom-Ring(0,R) /\ [#]Polynom-Ring (Polynom-Ring(0,R)) = {}
proof
set P0 = Polynom-Ring(0,R);
assume [#]P0 /\ [#]Polynom-Ring P0 <> {}; then
consider o be object such that
A2: o in [#]P0 /\ [#]Polynom-Ring P0 by XBOOLE_0:def 1;
o is Element of [#]P0 by A2,XBOOLE_0:def 4; then
not o is Polynomial of P0 by Th22;
hence contradiction by A2,POLYNOM3:def 10;
end;
theorem
for R be non degenerated Ring holds
ex PR be non degenerated Ring, X be set, h be Function,
G be Function of Polynom-Ring(Polynom-Ring(0,R)),PR
st Polynom-Ring(0,R) is Subring of PR & G is RingIsomorphism &
id Polynom-Ring(0,R) = G*(canHom Polynom-Ring(0,R)) &
X /\ [#]Polynom-Ring(0,R) = {} & h is one-to-one &
dom h =
[#]Polynom-Ring(Polynom-Ring(0,R)) \ rng (canHom (Polynom-Ring(0,R))) &
rng h = X &
[#]PR = X \/ [#]Polynom-Ring(0,R) by Th25;
definition
let R;
let A be R-monomorphic comRing;
let x be Element of A;
attr x is indeterminate means
ex g being Function of Polynom-Ring R,A st g is isomorphism &
x = g.1_1(R);
end;
theorem
for R be non degenerated comRing holds
ex X be Element of Polynom-Ring R st X is indeterminate & X = 1_1(R)
proof
let R be non degenerated comRing;
reconsider X = 1_1(R) as Element of Polynom-Ring R
by POLYNOM3:def 10;
A1: (id Polynom-Ring R).1_1(R) = X;
take X;
thus thesis by A1;
end;