:: Rings and Modules - Part II
:: by Michal Muzalewski
::
:: Received October 18, 1991
:: Copyright (c) 1991-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 XBOOLE_0, FUNCSDOM, VECTSP_1, CLASSES2, FUNCT_5, MCART_1,
STRUCT_0, VECTSP_2, SUPINF_2, ALGSTR_0, SUBSET_1, ARYTM_3, RLVECT_1,
RELAT_1, MESFUNC1, FUNCT_1, MSSUBFAM, GRCAT_1, GRAPH_1, CAT_1, MIDSP_1,
ORDINAL1, CARD_1, ARYTM_1, BINOP_1, LATTICES, FUNCT_2, ZFMISC_1, MOD_2,
UNIALG_1;
notations TARSKI, XBOOLE_0, ENUMSET1, ZFMISC_1, SUBSET_1, BINOP_1, PARTFUN1,
ORDINAL1, NUMBERS, FUNCT_2, FUNCT_5, STRUCT_0, ALGSTR_0, RLVECT_1,
GROUP_1, VECTSP_1, VECTSP_2, CLASSES2, GRCAT_1, FUNCT_3;
constructors ENUMSET1, PARTFUN1, VECTSP_2, GRCAT_1, FUNCOP_1, ALGSTR_1,
RELSET_1, CLASSES1, FUNCT_5;
registrations XBOOLE_0, SUBSET_1, RELSET_1, FUNCT_2, STRUCT_0, VECTSP_1,
ALGSTR_1, ALGSTR_0, CLASSES2, GRCAT_1;
requirements SUBSET, BOOLE, NUMERALS;
definitions RLVECT_1, ALGSTR_0;
equalities STRUCT_0, GRCAT_1, ALGSTR_0, ORDINAL1;
expansions VECTSP_1;
theorems BINOP_1, CLASSES2, ENUMSET1, GRCAT_1, FUNCT_2, ORDINAL1, VECTSP_1,
RLVECT_1, RELAT_1, GROUP_1, FUNCOP_1, FUNCT_1, STRUCT_0, ALGSTR_0;
schemes FUNCT_2, BINOP_1;
begin
reserve D,D9 for non empty set;
reserve R for Ring;
reserve G,H,S for non empty ModuleStr over R;
reserve UN for Universe;
::
:: Trivial Left Module
::
Lm1: ModuleStr (#{0},op2,op0,pr2(the carrier of R,{0})#)
is strict LeftMod of R
proof
set a = 0.Trivial-addLoopStr;
set G = ModuleStr (#{0},op2,op0,pr2(the carrier of R,{0})#);
A1: for a,b being Element of G for x,y being Element of Trivial-addLoopStr
st x = a & b = y holds a + b = x + y;
A2: G is Abelian add-associative right_zeroed right_complementable
proof
thus G is Abelian
proof
let a,b be Element of G;
reconsider x = a, y = b as Element of Trivial-addLoopStr;
thus a + b = y + x by A1
.= b + a;
end;
hereby
let a,b,c be Element of G;
reconsider x = a, y = b, z = c as Element of Trivial-addLoopStr;
thus a + b + c = x + y + z .= x + (y + z) by RLVECT_1:def 3
.= a + (b + c);
end;
hereby
let a be Element of G;
reconsider x = a as Element of Trivial-addLoopStr;
thus a + 0.G = x + 0.Trivial-addLoopStr .= a by RLVECT_1:4;
end;
let a be Element of G;
reconsider x = a as Element of Trivial-addLoopStr;
consider b being Element of Trivial-addLoopStr such that
A3: x + b = 0.Trivial-addLoopStr by ALGSTR_0:def 11;
reconsider b9 = b as Element of G;
take b9;
thus thesis by A3;
end;
now
let x,y be Scalar of R, v,w be Vector of G;
A4: (x*y)*v = a & (1.R)*v = a by GRCAT_1:4;
x*(v+w) = a & (x+y)*v = a by GRCAT_1:4;
hence
x*(v+w) = x*v+x*w & (x+y)*v = x*v+y*v & (x*y)*v = x*(y*v) & (1.R)*v =
v by A4,GRCAT_1:4;
end;
hence thesis by A2,VECTSP_1:def 14,def 15,def 16,def 17;
end;
definition
let R;
func TrivialLMod(R) -> strict LeftMod of R equals
ModuleStr (#{0},op2,op0,pr2(the carrier of R,{0})#);
coherence by Lm1;
end;
theorem
for x being Vector of TrivialLMod R holds x = 0.TrivialLMod R by GRCAT_1:4;
definition
let R be non empty multMagma;
let G,H be non empty ModuleStr over R;
let f be Function of G,H;
attr f is homogeneous means
for a being Scalar of R, x being Vector of G holds f.(a*x) = a*f.x;
end;
theorem Th2:
for f being Function of G,H, g being Function of H,S st
f is homogeneous & g is homogeneous holds g*f is homogeneous
proof
let f be Function of G,H, g be Function of H,S;
assume that
A1: f is homogeneous and
A2: g is homogeneous;
set h = g*f;
let a be Scalar of R, x be Vector of G;
thus h.(a*x) = g.(f.(a*x)) by FUNCT_2:15
.= g.(a*f.x) by A1
.= a*g.(f.x) by A2
.= a*h.x by FUNCT_2:15;
end;
reserve R for Ring;
reserve G, H for LeftMod of R;
registration let R,G,H;
cluster ZeroMap(G,H) -> homogeneous;
coherence
proof
let a be Scalar of R, x be Vector of G;
set f = ZeroMap(G,H);
f.(a*x) = 0.H & f.x = 0.H by FUNCOP_1:7;
hence thesis by VECTSP_1:14;
end;
end;
::
:: Morphisms of Left Modules
::
reserve G1, G2, G3 for LeftMod of R;
definition
let R;
struct LModMorphismStr over R (#
DomL, CodL -> LeftMod of R,
Fun -> Function of the DomL, the CodL #);
end;
reserve f for LModMorphismStr over R;
definition
let R,f;
func dom(f) -> LeftMod of R equals
the DomL of f;
correctness;
func cod(f) -> LeftMod of R equals
the CodL of f;
correctness;
end;
definition
let R,f;
func fun(f) -> Function of dom(f),cod(f) equals
the Fun of f;
coherence;
end;
theorem
for f0 being Function of G1,G2 st f = LModMorphismStr(#G1,G2,f0#)
holds dom f = G1 & cod f = G2 & fun f = f0;
definition
let R,G,H;
func ZERO(G,H) -> strict LModMorphismStr over R equals
LModMorphismStr(# G,H,ZeroMap(G,H)#);
coherence;
end;
definition
let R;
let IT be LModMorphismStr over R;
attr IT is LModMorphism-like means
:Def7:
fun(IT) is additive homogeneous;
end;
registration
let R;
cluster strict LModMorphism-like for LModMorphismStr over R;
existence
proof
set G = the LeftMod of R;
set z = ZERO(G,G);
z is LModMorphism-like;
hence thesis;
end;
end;
definition
let R;
mode LModMorphism of R is LModMorphism-like LModMorphismStr over R;
end;
theorem Th4:
for F being LModMorphism of R holds the Fun of F is additive homogeneous
proof
let F be LModMorphism of R;
the Fun of F = fun(F);
hence thesis by Def7;
end;
registration
let R,G,H;
cluster ZERO(G,H) -> LModMorphism-like;
coherence;
end;
definition
let R,G,H;
mode Morphism of G,H -> LModMorphism of R means
:Def8:
dom(it) = G & cod(it) = H;
existence
proof
take ZERO(G,H);
thus thesis;
end;
end;
registration
let R,G,H;
cluster strict for Morphism of G,H;
existence
proof
dom(ZERO(G,H)) = G & cod(ZERO(G,H)) = H;
then reconsider z = ZERO(G,H) as Morphism of G,H by Def8;
take z;
thus thesis;
end;
end;
theorem Th5:
for f being LModMorphismStr over R holds dom(f) = G & cod(f) = H
& fun(f) is additive homogeneous implies f is Morphism of G,H
proof
let f be LModMorphismStr over R;
assume that
A1: dom(f) = G & cod(f) = H and
A2: fun(f) is additive homogeneous;
reconsider f9 = f as LModMorphism of R by A2,Def7;
f9 is Morphism of G,H by A1,Def8;
hence thesis;
end;
theorem Th6:
for f being Function of G,H st f is additive homogeneous
holds LModMorphismStr(#G,H,f#) is strict Morphism of G,H
proof
let f be Function of G,H such that
A1: f is additive homogeneous;
set F = LModMorphismStr (#G,H,f#);
fun(F) = f;
hence thesis by A1,Th5;
end;
registration let R,G;
cluster id G -> homogeneous;
coherence
proof
set f = id G;
let a be Scalar of R, x be Vector of G;
thus f.(a*x) = a*x by FUNCT_1:18
.= a*f.x by FUNCT_1:18;
end;
end;
definition
let R,G;
func ID G -> strict Morphism of G,G equals
LModMorphismStr(# G,G,id G#);
coherence
proof
set i = LModMorphismStr(# G,G,id G#);
fun(i) = id G;
hence thesis by Th5;
end;
end;
definition
let R,G,H;
redefine func ZERO(G,H) -> strict Morphism of G,H; :: redefines ZERO (MOD_2, definition)
coherence
proof
set i = ZERO(G,H);
fun(i) = ZeroMap(G,H);
hence thesis by Th5;
end;
end;
theorem Th7:
for F being Morphism of G,H ex f being Function of G,H st the
LModMorphismStr of F = LModMorphismStr(#G,H,f#) & f is additive homogeneous
proof
let F be Morphism of G,H;
A1: the CodL of F = cod(F) .= H by Def8;
A2: the DomL of F = dom(F) .= G by Def8;
then reconsider f = the Fun of F as Function of G,H by A1;
take f;
thus thesis by A2,A1,Th4;
end;
theorem Th8:
for F being strict Morphism of G,H ex f being Function of G,H st
F = LModMorphismStr(#G,H,f#)
proof
let F be strict Morphism of G,H;
consider f being Function of G,H such that
A1: the LModMorphismStr of F = LModMorphismStr(#G,H,f#) and
f is additive homogeneous by Th7;
take f;
thus thesis by A1;
end;
theorem Th9:
for F being LModMorphism of R ex G,H st F is Morphism of G,H
proof
let F be LModMorphism of R;
take G = the DomL of F,H = the CodL of F;
dom(F) = G & cod(F) = H;
hence thesis by Def8;
end;
theorem
for F being strict LModMorphism of R ex G,H being LeftMod of R, f
being Function of G,H st F is strict Morphism of G,H & F = LModMorphismStr(#G,H
,f#) & f is additive homogeneous
proof
let F be strict LModMorphism of R;
consider G,H such that
A1: F is Morphism of G,H by Th9;
reconsider F9 = F as Morphism of G,H by A1;
consider f being Function of G,H such that
A2: the LModMorphismStr of F9 = LModMorphismStr(#G,H,f#) &
f is additive homogeneous
by Th7;
take G,H,f;
thus thesis by A2;
end;
theorem Th11:
for g,f being LModMorphism of R st dom(g) = cod(f) ex G1,G2,G3
st g is Morphism of G2,G3 & f is Morphism of G1,G2
proof
defpred P[LModMorphism of R,LModMorphism of R] means dom($1) = cod($2);
let g,f be LModMorphism of R such that
A1: P[g,f];
consider G2,G3 such that
A2: g is Morphism of G2,G3 by Th9;
A3: G2 = dom(g) by A2,Def8;
consider G1,G2 being LeftMod of R such that
A4: f is Morphism of G1,G2 by Th9;
G2 = cod(f) by A4,Def8;
hence thesis by A1,A2,A3,A4;
end;
definition
let R;
let G,F be LModMorphism of R;
assume
A1: dom(G) = cod(F);
func G*F -> strict LModMorphism of R means
:Def10:
for G1,G2,G3 being
LeftMod of R, g being Function of G2,G3, f being Function of G1,G2 st the
LModMorphismStr of G = LModMorphismStr(#G2,G3,g#) & the LModMorphismStr of F =
LModMorphismStr(#G1,G2,f#) holds it = LModMorphismStr(#G1,G3,g*f#);
existence
proof
consider G19,G2,G39 being LeftMod of R such that
A2: G is Morphism of G2,G39 and
A3: F is Morphism of G19,G2 by A1,Th11;
consider f9 being Function of G19,G2 such that
A4: the LModMorphismStr of F = LModMorphismStr(#G19,G2,f9#) and
A5: f9 is additive homogeneous by A3,Th7;
consider g9 being Function of G2,G39 such that
A6: the LModMorphismStr of G = LModMorphismStr(#G2,G39,g9#) and
A7: g9 is additive homogeneous by A2,Th7;
g9*f9 is additive homogeneous by A7,A5,Th2;
then reconsider
T9 = (LModMorphismStr(#G19,G39,g9*f9#)) as strict LModMorphism
of R by Th6;
take T9;
thus thesis by A6,A4;
end;
uniqueness
proof
consider G19,G29 being LeftMod of R such that
A8: F is Morphism of G19,G29 by Th9;
reconsider F9 = F as Morphism of G19,G29 by A8;
consider G2,G39 being LeftMod of R such that
A9: G is Morphism of G2,G39 by Th9;
G2 = dom(G) by A9,Def8;
then reconsider F9 as Morphism of G19,G2 by A1,Def8;
consider f9 being Function of G19,G2 such that
A10: the LModMorphismStr of F9 = LModMorphismStr(#G19,G2,f9#) and
f9 is additive homogeneous by Th7;
reconsider G9 = G as Morphism of G2,G39 by A9;
let S1,S2 be strict LModMorphism of R such that
A11: for G1,G2,G3 being LeftMod of R, g being Function of G2,G3, f
being Function of G1,G2 st the LModMorphismStr of G = LModMorphismStr(#G2,G3,g
#) & the LModMorphismStr of F = LModMorphismStr(#G1,G2,f#) holds S1 =
LModMorphismStr(#G1,G3,g*f#) and
A12: for G1,G2,G3 being LeftMod of R, g being Function of G2,G3, f
being Function of G1,G2 st the LModMorphismStr of G = LModMorphismStr(#G2,G3,g
#) & the LModMorphismStr of F = LModMorphismStr(#G1,G2,f#) holds S2 =
LModMorphismStr(#G1,G3,g*f#);
consider g9 being Function of G2,G39 such that
A13: the LModMorphismStr of G9 = LModMorphismStr(#G2,G39,g9#) and
g9 is additive homogeneous by Th7;
thus S1 = (LModMorphismStr(#G19,G39,g9*f9#)) by A11,A13,A10
.= S2 by A12,A13,A10;
end;
end;
theorem Th12:
for G being Morphism of G2,G3, F being Morphism of G1,G2 holds G
*F is strict Morphism of G1,G3
proof
let G be Morphism of G2,G3, F be Morphism of G1,G2;
consider g being Function of G2,G3 such that
A1: the LModMorphismStr of G = LModMorphismStr(#G2,G3,g#) and
g is additive homogeneous by Th7;
consider f being Function of G1,G2 such that
A2: the LModMorphismStr of F = LModMorphismStr(#G1,G2,f#) and
f is additive homogeneous by Th7;
dom(G) = G2 by Def8
.= cod(F) by Def8;
then G*F = LModMorphismStr(#G1,G3,g*f#) by A1,A2,Def10;
then dom(G*F) = G1 & cod(G*F) = G3;
hence thesis by Def8;
end;
definition
let R,G1,G2,G3;
let G be Morphism of G2,G3;
let F be Morphism of G1,G2;
func G*'F -> strict Morphism of G1,G3 equals
G*F;
coherence by Th12;
end;
theorem Th13:
for G being Morphism of G2,G3, F being Morphism of G1,G2, g
being Function of G2,G3, f being Function of G1,G2 st G = LModMorphismStr(#G2,
G3,g#) & F = LModMorphismStr(#G1,G2,f#) holds G*'F = LModMorphismStr(#G1,G3,g*f
#) & G*F = LModMorphismStr(# G1,G3,g*f#)
proof
let G be Morphism of G2,G3, F be Morphism of G1,G2, g be Function of G2,G3,
f be Function of G1,G2 such that
A1: G = LModMorphismStr(#G2,G3,g#) & F = LModMorphismStr(#G1,G2,f#);
dom(G) = G2 by Def8
.= cod(F) by Def8;
hence thesis by A1,Def10;
end;
theorem Th14:
for f,g being strict LModMorphism of R st dom g = cod f holds ex
G1,G2,G3 being LeftMod of R, f0 being Function of G1,G2, g0 being Function of
G2,G3 st f = LModMorphismStr(#G1,G2,f0#) & g = LModMorphismStr(#G2,G3,g0#) & g*
f = LModMorphismStr(#G1,G3,g0*f0#)
proof
let f,g be strict LModMorphism of R such that
A1: dom g = cod f;
set G1 = dom f,G2 = cod f, G3 = cod g;
reconsider f9 = f as strict Morphism of G1,G2 by Def8;
reconsider g9 = g as strict Morphism of G2,G3 by A1,Def8;
consider f0 being Function of G1,G2 such that
A2: f9 = LModMorphismStr(#G1,G2,f0#);
consider g0 being Function of G2,G3 such that
A3: g9 = LModMorphismStr(#G2,G3,g0#) by Th8;
take G1,G2,G3,f0,g0;
thus thesis by A2,A3,Th13;
end;
theorem
for f,g being strict LModMorphism of R st dom g = cod f holds dom(g*f)
= dom f & cod (g*f) = cod g
proof
let f,g be strict LModMorphism of R;
assume dom g = cod f;
then
A1: ex G1,G2,G3 being LeftMod of R, f0 being Function of G1,G2, g0 being
Function of G2,G3 st f = LModMorphismStr(#G1,G2,f0#) & g = LModMorphismStr(#G2,
G3,g0#) & g*f = LModMorphismStr(#G1,G3,g0*f0#) by Th14;
hence dom(g*f) = dom f;
thus thesis by A1;
end;
theorem Th16:
for G1,G2,G3,G4 being LeftMod of R, f being strict Morphism of
G1,G2, g being strict Morphism of G2,G3, h being strict Morphism of G3,G4 holds
h*(g*f) = (h*g)*f
proof
let G1,G2,G3,G4 be LeftMod of R, f be strict Morphism of G1,G2, g be strict
Morphism of G2,G3, h be strict Morphism of G3,G4;
consider f0 being Function of G1,G2 such that
A1: f = LModMorphismStr(#G1,G2,f0#) by Th8;
consider g0 being Function of G2,G3 such that
A2: g = LModMorphismStr(#G2,G3,g0#) by Th8;
consider h0 being Function of G3,G4 such that
A3: h = LModMorphismStr(#G3,G4,h0#) by Th8;
A4: h*'g = LModMorphismStr(#G2,G4,h0*g0#) by A2,A3,Th13;
g*'f = LModMorphismStr(#G1,G3,g0*f0#) by A1,A2,Th13;
then h*(g*f) = LModMorphismStr(#G1,G4,h0*(g0*f0)#) by A3,Th13
.= LModMorphismStr(#G1,G4,(h0*g0)*f0#) by RELAT_1:36
.= (h*g)*f by A1,A4,Th13;
hence thesis;
end;
theorem
for f,g,h being strict LModMorphism of R st dom h = cod g & dom g =
cod f holds h*(g*f) = (h*g)*f
proof
let f,g,h be strict LModMorphism of R such that
A1: dom h = cod g and
A2: dom g = cod f;
set G2 = cod f, G3 = cod g;
reconsider h9 = h as strict Morphism of G3,(cod h) by A1,Def8;
reconsider g9 = g as strict Morphism of G2,G3 by A2,Def8;
reconsider f9 = f as strict Morphism of (dom f),G2 by Def8;
h9*(g9*f9) = (h9*g9)*f9 by Th16;
hence thesis;
end;
theorem
dom ID(G) = G & cod ID(G) = G & (for f being strict LModMorphism of R
st cod f = G holds (ID G)*f = f) & for g being strict LModMorphism of R st dom
g = G holds g*(ID G) = g
proof
set i = ID G;
thus dom i = G;
thus cod i = G;
thus for f being strict LModMorphism of R st cod f = G holds i*f = f
proof
let f be strict LModMorphism of R such that
A1: cod f = G;
set H = dom(f);
reconsider f9 = f as Morphism of H,G by A1,Def8;
consider m being Function of H,G such that
A2: f9 = LModMorphismStr(#H,G,m#) by Th8;
dom(i) = G & (id G)*m = m by FUNCT_2:17;
hence thesis by A1,A2,Def10;
end;
thus for g being strict LModMorphism of R st dom g = G holds g*(ID G) = g
proof
let f be strict LModMorphism of R such that
A3: dom f = G;
set H = cod(f);
reconsider f9 = f as Morphism of G,H by A3,Def8;
consider m being Function of G,H such that
A4: f9 = LModMorphismStr(#G,H,m#) by Th8;
cod(i) = G & m*(id G) = m by FUNCT_2:17;
hence thesis by A3,A4,Def10;
end;
end;
theorem Th19:
for u,v,w being Element of UN holds {u,v,w} is Element of UN
proof
let u,v,w be Element of UN;
{u,v,w} = {u,v} \/ {w} by ENUMSET1:3;
hence thesis;
end;
theorem Th20:
for u being Element of UN holds succ u is Element of UN
proof
let u be Element of UN;
succ u = u \/ {u};
hence thesis;
end;
theorem Th21:
0 is Element of UN & 1 is Element of UN & 2 is Element of UN
proof
thus 0 is Element of UN by CLASSES2:56;
{} is Element of UN & 1 = succ 0 by CLASSES2:56;
hence
A1: 1 is Element of UN by Th20;
2 = succ 1;
hence thesis by A1,Th20;
end;
reserve a,b,c for Element of {0,1,2};
Lm2: ex c st c = 0
proof
reconsider c = 0 as Element of {0,1,2} by ENUMSET1:def 1;
take c;
thus thesis;
end;
Lm3: ex c st c = 1
proof
reconsider c = 1 as Element of {0,1,2} by ENUMSET1:def 1;
take c;
thus thesis;
end;
Lm4: ex c st c = 2
proof
reconsider c = 2 as Element of {0,1,2} by ENUMSET1:def 1;
take c;
thus thesis;
end;
definition
let a;
func -a -> Element of {0,1,2} equals
:Def12:
0 if a = 0, 2 if a = 1, 1 if a = 2;
coherence by Lm3,Lm4;
consistency;
let b;
func a+b -> Element of {0,1,2} equals
:Def13:
b if a = 0, a if b = 0, 2 if a
= 1 & b = 1, 0 if a = 1 & b = 2, 0 if a = 2 & b = 1, 1 if a = 2 & b = 2;
coherence by Lm2,Lm3,Lm4;
consistency;
func a*b -> Element of {0,1,2} equals
:Def14:
0 if b = 0, 0 if a = 0, a if b
= 1, b if a = 1, 1 if a = 2 & b = 2;
coherence by Lm3;
consistency;
end;
definition
func add3 -> BinOp of {0,1,2} means
:Def15:
it.(a,b) = a+b;
existence
proof
deffunc O(Element of {0,1,2},Element of {0,1,2})=$1+$2;
ex o being BinOp of {0,1,2} st for a,b being Element of {0,1,2} holds
o.(a,b) = O(a,b) from BINOP_1:sch 4;
hence thesis;
end;
uniqueness
proof
let o1,o2 be BinOp of ({0,1,2}) such that
A1: for a,b holds o1.(a,b) = a+b and
A2: for a,b holds o2.(a,b) = a+b;
now
let a,b;
thus o1.(a,b) = a+b by A1
.= o2.(a,b) by A2;
end;
hence thesis by BINOP_1:2;
end;
func mult3 -> BinOp of {0,1,2} means
:Def16:
it.(a,b) = a*b;
existence
proof
deffunc O(Element of {0,1,2},Element of {0,1,2})=$1*$2;
ex o being BinOp of {0,1,2} st for a,b being Element of {0,1,2} holds
o.(a,b) = O(a,b) from BINOP_1:sch 4;
hence thesis;
end;
uniqueness
proof
let o1,o2 be BinOp of ({0,1,2}) such that
A3: for a,b holds o1.(a,b) = a*b and
A4: for a,b holds o2.(a,b) = a*b;
now
let a,b;
thus o1.(a,b) = a*b by A3
.= o2.(a,b) by A4;
end;
hence thesis by BINOP_1:2;
end;
func compl3 -> UnOp of {0,1,2} means
:Def17:
it.a = -a;
existence
proof
deffunc F( Element of {0,1,2})= -$1;
ex f being UnOp of {0,1,2} st for x being Element of {0,1,2} holds f.x
= F(x) from FUNCT_2:sch 4;
hence thesis;
end;
uniqueness
proof
let o1,o2 be UnOp of ({0,1,2}) such that
A5: for a holds o1.a = -a and
A6: for a holds o2.a = -a;
now
let a;
thus o1.a = -a by A5
.= o2.a by A6;
end;
hence thesis by FUNCT_2:63;
end;
func unit3 -> Element of {0,1,2} equals
1;
coherence by ENUMSET1:def 1;
func zero3 -> Element of {0,1,2} equals
0;
coherence by ENUMSET1:def 1;
end;
definition
func Z_3 -> strict doubleLoopStr equals
:Def20:
doubleLoopStr (#{0,1,2},add3,mult3,unit3,zero3#);
coherence;
end;
registration
cluster Z_3 -> non empty;
coherence;
end;
Lm5: now
let h, e be Element of Z_3;
assume
A1: e = 1;
reconsider a=e, b=h as Element of {0,1,2};
thus h * e = b*a by Def16
.= h by A1,Def14;
thus e * h = a*b by Def16
.= h by A1,Def14;
end;
registration
cluster Z_3 -> well-unital;
coherence by Lm5;
end;
theorem Th22:
0.Z_3 = 0 & 1.Z_3 = 1 & 0.Z_3 is Element of {0,1,2} & 1.Z_3 is
Element of {0,1,2} & the addF of Z_3 = add3 & the multF of Z_3 = mult3;
Lm6: for x,y,z being Scalar of Z_3, X,Y,Z being Element of {0,1,2} st X=x
& Y=y
& Z=z holds (x+y)+z = (X+Y)+Z & x+(y+z) = X+(Y+Z) & (x*y)*z = (X*Y)*Z & x*(y*z)
= X*(Y*Z)
proof
let x,y,z be Scalar of Z_3, X,Y,Z be Element of {0,1,2};
assume that
A1: X=x and
A2: Y=y and
A3: Z=z;
A4: x*y = X*Y & y*z = Y*Z by A1,A2,A3,Def16;
x+y = X+Y & y+z = Y+Z by A1,A2,A3,Def15;
hence thesis by A1,A3,A4,Def15,Def16;
end;
Lm7: for x,y,z,a being Element of {0,1,2} st a = 0 holds x+(-x) = a & x+a = x
& (x+y)+z = x+(y+z)
proof
let x,y,z,a be Element of {0,1,2} such that
A1: a = 0;
thus x+(-x) = a
proof
now
per cases by ENUMSET1:def 1;
suppose
A2: x = 0;
then -x = 0 by Def12;
hence thesis by A1,A2,Def13;
end;
suppose
A3: x = 1;
then -x = 2 by Def12;
hence thesis by A1,A3,Def13;
end;
suppose
A4: x = 2;
then -x = 1 by Def12;
hence thesis by A1,A4,Def13;
end;
end;
hence thesis;
end;
thus x+a = x by A1,Def13;
thus (x+y)+z = x+(y+z)
proof
now
per cases by ENUMSET1:def 1;
suppose
A5: x = 0;
hence (x+y)+z = y+z by Def13
.= x+(y+z) by A5,Def13;
end;
suppose
A6: y = 0;
then x+y = x by Def13;
hence thesis by A6,Def13;
end;
suppose
A7: z = 0;
then y+z = y by Def13;
hence thesis by A7,Def13;
end;
suppose
A8: x = 1 & y = 1 & z = 1;
thus (x+y)+z = 0 by A8,Def13
.= x+(y+z) by A8,Def13;
end;
suppose
A9: x = 1 & y = 1 & z = 2;
then
A10: y+z = 0 by Def13;
x+y = 2 by A9,Def13;
hence (x+y)+z = 1 by A9,Def13
.= x+(y+z) by A9,A10,Def13;
end;
suppose
A11: x = 1 & y = 2 & z = 1;
then
A12: y+z = 0 by Def13;
x+y = 0 by A11,Def13;
hence (x+y)+z = 1 by A11,Def13
.= x+(y+z) by A11,A12,Def13;
end;
suppose
A13: x = 1 & y = 2 & z = 2;
then
A14: y+z = 1 by Def13;
x+y = 0 by A13,Def13;
hence (x+y)+z = 2 by A13,Def13
.= x+(y+z) by A13,A14,Def13;
end;
suppose
A15: x = 2 & y = 1 & z = 1;
then
A16: y+z = 2 by Def13;
x+y = 0 by A15,Def13;
hence (x+y)+z = 1 by A15,Def13
.= x+(y+z) by A15,A16,Def13;
end;
suppose
A17: x = 2 & y = 1 & z = 2;
then
A18: y+z = 0 by Def13;
x+y = 0 by A17,Def13;
hence (x+y)+z = 2 by A17,Def13
.= x+(y+z) by A17,A18,Def13;
end;
suppose
A19: x = 2 & y = 2 & z = 1;
then
A20: y+z = 0 by Def13;
x+y = 1 by A19,Def13;
hence (x+y)+z = 2 by A19,Def13
.= x+(y+z) by A19,A20,Def13;
end;
suppose
A21: x = 2 & y = 2 & z = 2;
thus (x+y)+z = 0 by A21,Def13
.= x+(y+z) by A21,Def13;
end;
end;
hence thesis;
end;
end;
registration
cluster Z_3 -> add-associative right_zeroed right_complementable;
coherence
proof
thus Z_3 is add-associative
proof
let x,y,z be Element of Z_3;
reconsider X=x,Y=y,Z=z as Element of {0,1,2};
thus (x+y)+z = (X+Y)+Z by Lm6
.= X+(Y+Z) by Lm7
.= x+(y+z) by Lm6;
end;
thus Z_3 is right_zeroed
proof
let x be Element of Z_3;
reconsider X=x,a=0 as Element of {0,1,2} by Def20;
thus x+0.Z_3 = X+a by Def15
.= x by Lm7;
end;
let x be Element of Z_3;
reconsider x9 = x as Element of {0,1,2};
reconsider y = compl3.x9 as Element of Z_3;
reconsider y9 = y as Element of {0,1,2};
take y;
A1: y9 = -x9 by Def17;
thus x + y = 0.Z_3
proof
per cases by ENUMSET1:def 1;
suppose
A2: x = 0;
then
A3: y9 = 0 by A1,Def12;
thus x+y = x9+y9 by Def15
.= 0.Z_3 by A2,A3,Def13;
end;
suppose
A4: x = 1;
then
A5: y9 = 2 by A1,Def12;
thus x+y = x9+y9 by Def15
.= 0.Z_3 by A4,A5,Def13;
end;
suppose
A6: x = 2;
then
A7: y9 = 1 by A1,Def12;
thus x+y = x9+y9 by Def15
.= 0.Z_3 by A6,A7,Def13;
end;
end;
end;
end;
theorem Th23:
for x,y being Scalar of Z_3, X,Y being Element of {0,1,2} st
X=x & Y=y holds x+y = X+Y & x*y = X*Y & -x = -X
proof
let x,y be Scalar of Z_3, X,Y be Element of {0,1,2};
assume that
A1: X=x and
A2: Y=y;
thus x+y = X+Y by A1,A2,Def15;
thus x*y = X*Y by A1,A2,Def16;
reconsider a = -X as Element of Z_3;
x + a = X + -X by A1,Def15
.= 0.Z_3 by Lm7;
hence thesis by RLVECT_1:def 10;
end;
theorem Th24:
for x,y,z being Scalar of Z_3, X,Y,Z being Element of {0,1,2} st
X=x & Y=y & Z=z holds (x+y)+z = (X+Y)+Z &
x+(y+z) = X+(Y+Z) & (x*y)*z = (X*Y)*Z
& x*(y*z) = X*(Y*Z)
proof
let x,y,z be Scalar of Z_3, X,Y,Z be Element of {0,1,2};
assume that
A1: X=x and
A2: Y=y and
A3: Z=z;
A4: x*y = X*Y & y*z = Y*Z by A1,A2,A3,Th23;
x+y = X+Y & y+z = Y+Z by A1,A2,A3,Th23;
hence thesis by A1,A3,A4,Th23;
end;
theorem Th25:
for x,y,z,a,b being Element of {0,1,2} st a = 0 & b = 1 holds
x+y = y+x & (x+y)+z = x+(y+z) & x+a = x &
x+(-x) = a & x*y = y*x & (x*y)*z = x*(y*z) & b*x = x &
(x<>a implies ex y be Element of {0,1,2} st x*y = b) &
a <> b & x*(y+z) = x*y+x*z
proof
let x,y,z,a,b be Element of {0,1,2} such that
A1: a = 0 and
A2: b = 1;
thus x+y = y+x
proof
now
per cases by ENUMSET1:def 1;
suppose
A3: x = 0;
hence x+y = y by Def13
.= y+x by A3,Def13;
end;
suppose
A4: y = 0;
hence x+y = x by Def13
.= y+x by A4,Def13;
end;
suppose
x = 1 & y = 1;
hence thesis;
end;
suppose
A5: x = 1 & y = 2;
hence x+y = 0 by Def13
.= y+x by A5,Def13;
end;
suppose
A6: x = 2 & y = 1;
hence x+y = 0 by Def13
.= y+x by A6,Def13;
end;
suppose
x = 2 & y = 2;
hence thesis;
end;
end;
hence thesis;
end;
thus (x+y)+z = x+(y+z) by A1,Lm7;
thus x+a = x by A1,Def13;
thus x+(-x) = a by A1,Lm7;
thus x*y = y*x
proof
now
per cases by ENUMSET1:def 1;
suppose
A7: y = 0;
hence x*y = 0 by Def14
.= y*x by A7,Def14;
end;
suppose
A8: x = 0;
hence x*y = 0 by Def14
.= y*x by A8,Def14;
end;
suppose
A9: y = 1;
hence x*y = x by Def14
.= y*x by A9,Def14;
end;
suppose
A10: x = 1;
hence x*y = y by Def14
.= y*x by A10,Def14;
end;
suppose
x = 2 & y = 2;
hence thesis;
end;
end;
hence thesis;
end;
thus (x*y)*z = x*(y*z)
proof
now
per cases by ENUMSET1:def 1;
suppose
A11: z = 0;
then
A12: y*z = 0 by Def14;
thus (x*y)*z = 0 by A11,Def14
.= x*(y*z) by A12,Def14;
end;
suppose
A13: y = 0;
then
A14: y*z = 0 by Def14;
x*y = 0 by A13,Def14;
hence (x*y)*z = 0 by Def14
.= x*(y*z) by A14,Def14;
end;
suppose
A15: x = 0;
then x*y = 0 by Def14;
hence (x*y)*z = 0 by Def14
.= x*(y*z) by A15,Def14;
end;
suppose
A16: z = 1;
then y*z = y by Def14;
hence thesis by A16,Def14;
end;
suppose
A17: y = 1;
then x*y = x by Def14;
hence thesis by A17,Def14;
end;
suppose
A18: x = 1;
hence (x*y)*z = y*z by Def14
.= x*(y*z) by A18,Def14;
end;
suppose
A19: x = 2 & y = 2 & z = 2;
then
A20: y*z = 1 by Def14;
x*y = 1 by A19,Def14;
hence (x*y)*z = x by A19,Def14
.= x*(y*z) by A20,Def14;
end;
end;
hence thesis;
end;
thus b*x = x by A2,Def14;
thus x<>a implies ex y be Element of {0,1,2} st x*y = b
proof
now
per cases by ENUMSET1:def 1;
case
x = 0;
hence thesis by A1;
end;
case
A21: x = 1;
reconsider y = 1 as Element of {0,1,2} by ENUMSET1:def 1;
take y;
x*y = 1 by A21,Def14;
hence thesis by A2;
end;
case
A22: x = 2;
reconsider y = 2 as Element of {0,1,2} by ENUMSET1:def 1;
take y;
x*y = 1 by A22,Def14;
hence thesis by A2;
end;
end;
hence thesis;
end;
thus a <> b by A1,A2;
thus x*(y+z) = x*y+x*z
proof
now
per cases by ENUMSET1:def 1;
suppose
A23: x = 0;
then
A24: x*y = 0 & x*z = 0 by Def14;
thus x*(y+z) = 0 by A23,Def14
.= x*y+x*z by A24,Def13;
end;
suppose
y = 0;
then y+z = z & x*y = 0 by Def13,Def14;
hence thesis by Def13;
end;
suppose
z = 0;
then y+z = y & x*z = 0 by Def13,Def14;
hence thesis by Def13;
end;
suppose
A25: x = 1 & y = 1 & z = 1;
then x*y = 1 by Def14;
hence thesis by A25,Def14;
end;
suppose
A26: x = 1 & y = 1 & z = 2;
then
A27: x*y = 1 & x*z = 2 by Def14;
y+z = 0 by A26,Def13;
hence x*(y+z) = 0 by Def14
.= x*y+x*z by A27,Def13;
end;
suppose
A28: x = 1 & y = 2 & z = 1;
then
A29: x*y = 2 & x*z = 1 by Def14;
y+z = 0 by A28,Def13;
hence x*(y+z) = 0 by Def14
.= x*y+x*z by A29,Def13;
end;
suppose
A30: x = 1 & y = 2 & z = 2;
then x*y = 2 by Def14;
hence thesis by A30,Def14;
end;
suppose
A31: x = 2 & y = 1 & z = 1;
then
A32: x*y = 2 by Def14;
y+z = 2 by A31,Def13;
hence x*(y+z) = 1 by A31,Def14
.= x*y+x*z by A31,A32,Def13;
end;
suppose
A33: x = 2 & y = 1 & z = 2;
then
A34: x*y = 2 & x*z = 1 by Def14;
y+z = 0 by A33,Def13;
hence x*(y+z) = 0 by Def14
.= x*y+x*z by A34,Def13;
end;
suppose
A35: x = 2 & y = 2 & z = 1;
then
A36: x*y = 1 & x*z = 2 by Def14;
y+z = 0 by A35,Def13;
hence x*(y+z) = 0 by Def14
.= x*y+x*z by A36,Def13;
end;
suppose
A37: x = 2 & y = 2 & z = 2;
then
A38: x*y = 1 by Def14;
y+z = 1 by A37,Def13;
hence x*(y+z) = 2 by A37,Def14
.= x*y+x*z by A37,A38,Def13;
end;
end;
hence thesis;
end;
end;
theorem Th26:
for F being non empty doubleLoopStr st
for x,y,z being Scalar of F holds x+y = y+x &
(x+y)+z = x+(y+z) & x+(0.F) = x & x+(-x) = (0.F) &
x*y = y*x & (x*y)*z = x*(y*z) & 1.F*x = x & x*(1.F) = x &
(x<>(0.F) implies ex y be Scalar of F st
x*y = 1.F) & 0.F <> 1.F & x*(y+z) = x*y+x*z holds
F is Field
proof
let F be non empty doubleLoopStr such that
A1: for x,y,z being Scalar of F holds x+y = y+x & (x+y)+z = x+(y+z) & x+
(0.F) = x & x+(-x) = (0.F) & x*y = y*x & (x*y)*z = x*(y*z) & (1.F)*x = x & x*(
1.F) = x & (x<>(0.F) implies ex y be Scalar of F st x*y = 1.F) & 0.F <> 1.F & x
*(y+z) = x*y+x*z;
A2: for x being Scalar of F st x<>0.F ex y be Scalar of F st y*x = 1.F
proof
let x being Scalar of F;
assume x<>0.F;
then consider y be Scalar of F such that
A3: x*y = 1.F by A1;
take y;
thus thesis by A1,A3;
end;
A4: now
let x,y,z be Scalar of F;
thus x+y = y+x & (x+y)+z = x+(y+z) & x+(0.F) = x & x+(-x) = (0.F) & x*y =
y*x & (x*y)*z = x*(y*z) & (1.F)*x = x & x*(1.F) = x & (x<>(0.F) implies ex y be
Scalar of F st x*y = 1.F) & 0.F <> 1.F & x*(y+z) = x*y+x*z by A1;
thus (y+z)*x = x*(y+z) by A1
.= x*y + x*z by A1
.= y*x + x*z by A1
.= y*x + z*x by A1;
end;
F is right_complementable
proof
let v be Element of F;
take -v;
thus thesis by A4;
end;
hence thesis by A2,A4,GROUP_1:def 3,def 12,RLVECT_1:def 2,def 3,def 4
,STRUCT_0:def 8,VECTSP_1:def 6,def 7,def 9;
end;
theorem Th27:
Z_3 is Fanoian Field
proof
set F = Z_3;
reconsider a = 0.F, b = 1.F as Element of {0,1,2};
now
let x,y,z be Scalar of Z_3;
thus x+y = y+x & (x+y)+z = x+(y+z) & x+(0.Z_3) = x &
x+(-x) = (0.Z_3) & x*y
= y*x & (x*y)*z = x*(y*z) & (1.Z_3)*x = x & x*(1.Z_3) = x &
(x<>0.Z_3 implies ex y
be Scalar of Z_3 st x*y = 1.Z_3) & 0.Z_3 <> 1.Z_3 & x*(y+z) = x*y+x*z
proof
reconsider X=x, Y=y, Z=z as Element of {0,1,2};
A1: x*y = X*Y & x*z = X*Z by Th23;
thus x+y = X+Y by Th23
.= Y+X by Th25
.= y+x by Th23;
thus (x+y)+z = (X+Y)+Z by Th24
.= X+(Y+Z) by Th25
.= x+(y+z) by Th24;
thus x+(0.Z_3) = X+a by Th23
.= x by Th25;
-x = -X by Th23;
hence x+(-x) = X+(-X) by Th23
.= (0.Z_3) by Th25;
thus x*y = X*Y by Th23
.= Y*X by Th25
.= y*x by Th23;
thus (x*y)*z = (X*Y)*Z by Th24
.= X*(Y*Z) by Th25
.= x*(y*z) by Th24;
thus (1.Z_3)*x = b*X by Th23
.= x by Th25;
thus x*(1.Z_3) = X*b by Th23
.= b*X by Th25
.= x by Th25;
thus x <> 0.Z_3 implies ex y being Scalar of Z_3 st x*y = 1.Z_3
proof
assume x <> 0.Z_3;
then consider Y being Element of {0,1,2} such that
A2: X*Y = b by Th25;
reconsider y=Y as Scalar of Z_3;
take y;
thus thesis by A2,Th23;
end;
thus 0.Z_3 <> 1.Z_3;
y+z = Y+Z by Th23;
hence x*(y+z) = X*(Y+Z) by Th23
.= X*Y + X*Z by Th25
.= x*y+x*z by A1,Th23;
end;
end;
then reconsider F as Field by Th26;
1.F + 1.F = b + b by Def15
.= 2 by Def13;
hence thesis by Th22,VECTSP_1:def 19;
end;
registration
cluster Z_3 -> Fanoian add-associative right_zeroed right_complementable
Abelian commutative associative well-unital distributive
almost_left_invertible;
coherence by Th27;
end;
Lm8: the carrier of Z_3 in UN
proof
reconsider a = 0, b = 1, c = 2 as Element of UN by Th21;
{a,b,c} is Element of UN by Th19;
hence thesis;
end;
theorem Th28:
for f being Function of D,D9 st D in UN & D9 in UN holds f in UN
proof
let f be Function of D,D9;
assume D in UN & D9 in UN;
then
A1: Funcs(D,D9) in UN by CLASSES2:61;
f in Funcs(D,D9) by FUNCT_2:8;
hence thesis by A1,ORDINAL1:10;
end;
Lm9: (for f being BinOp of D st D in UN holds f in UN) & for f being UnOp of D
st D in UN holds f in UN
proof
now
let f be BinOp of D;
assume
A1: D in UN;
then [:D,D:] in UN by CLASSES2:61;
then
A2: Funcs([:D,D:],D) in UN by A1,CLASSES2:61;
f in Funcs([:D,D:],D) by FUNCT_2:8;
hence f in UN by A2,ORDINAL1:10;
end;
hence thesis by Th28;
end;
theorem
the carrier of Z_3 in UN & the addF of Z_3 in UN &
comp Z_3 in UN & 0.Z_3 in UN & the multF of Z_3 in UN &
1.Z_3 in UN
proof
thus the carrier of Z_3 in UN by Lm8;
hence thesis by Lm9,ORDINAL1:10;
end;