Volume 3, 1991

University of Bialystok

Copyright (c) 1991 Association of Mizar Users

### The abstract of the Mizar article:

### Rings and Modules --- Part II

**by****Michal Muzalewski**- Received October 18, 1991
- MML identifier: MOD_2

- [ Mizar article, MML identifier index ]

environ vocabulary FUNCSDOM, VECTSP_1, CLASSES2, GRCAT_1, RLVECT_1, BOOLE, MIDSP_1, VECTSP_2, FUNCT_3, FUNCT_1, PRE_TOPC, INCSP_1, ORDINAL4, CAT_1, RELAT_1, ARYTM_3, ORDINAL1, ARYTM_1, BINOP_1, LATTICES, FUNCT_2, MOD_2, ALGSTR_1; notation TARSKI, XBOOLE_0, ENUMSET1, ZFMISC_1, SUBSET_1, BINOP_1, FUNCT_2, STRUCT_0, ORDINAL1, RLVECT_1, VECTSP_1, FUNCSDOM, VECTSP_2, CLASSES2, PRE_TOPC, ALGSTR_1, MIDSP_1, GRCAT_1, FUNCT_3; constructors ENUMSET1, BINOP_1, VECTSP_2, GRCAT_1, TOPS_2, ALGSTR_1, MIDSP_1, MEMBERED, PARTFUN1, XBOOLE_0; clusters VECTSP_1, STRUCT_0, RELSET_1, SUBSET_1, ALGSTR_1, MEMBERED, ZFMISC_1, XBOOLE_0; requirements SUBSET, BOOLE; begin reserve x,y,z for set; reserve D,D' for non empty set; reserve R for Ring; reserve G,H,S for non empty VectSpStr over R; reserve UN for Universe; definition let R; canceled; func TrivialLMod(R) -> strict LeftMod of R equals :: MOD_2:def 2 VectSpStr (#{{}},op2,op0,pr2(the carrier of R,{{}})#); end; theorem :: MOD_2:1 for x being Vector of TrivialLMod(R) holds x = 0.TrivialLMod(R); definition let R be non empty doubleLoopStr; let G,H be non empty VectSpStr over R; let f be map of G,H; canceled 2; attr f is linear means :: MOD_2:def 5 (for x,y being Vector of G holds f.(x+y) = f.x+f.y) & for a being Scalar of R, x being Vector of G holds f.(a*x) = a*f.x; end; canceled 2; theorem :: MOD_2:4 for f being map of G,H st f is linear holds f is additive; canceled; theorem :: MOD_2:6 for f being map of G,H, g being map of H,S st f is linear & g is linear holds g*f is linear; reserve R for Ring; reserve G, H for LeftMod of R; canceled; theorem :: MOD_2:8 ZeroMap(G,H) is linear; :: :: Morphisms of Left Modules :: reserve G1, G2, G3 for LeftMod of R; definition let R; struct LModMorphismStr over R (# Dom,Cod -> LeftMod of R, Fun -> map of the Dom, the Cod #); end; reserve f for LModMorphismStr over R; definition let R,f; func dom(f) -> LeftMod of R equals :: MOD_2:def 6 the Dom of f; func cod(f) -> LeftMod of R equals :: MOD_2:def 7 the Cod of f; end; definition let R,f; func fun(f) -> map of dom(f),cod(f) equals :: MOD_2:def 8 the Fun of f; end; theorem :: MOD_2:9 for f0 being map 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 :: MOD_2:def 9 LModMorphismStr(# G,H,ZeroMap(G,H)#); end; definition let R; let IT be LModMorphismStr over R; attr IT is LModMorphism-like means :: MOD_2:def 10 fun(IT) is linear; end; definition let R; cluster strict LModMorphism-like LModMorphismStr over R; end; definition let R; mode LModMorphism of R is LModMorphism-like LModMorphismStr over R; end; theorem :: MOD_2:10 for F being LModMorphism of R holds the Fun of F is linear; definition let R,G,H; cluster ZERO(G,H) -> LModMorphism-like; end; definition let R,G,H; mode Morphism of G,H -> LModMorphism of R means :: MOD_2:def 11 dom(it) = G & cod(it) = H; end; definition let R,G,H; cluster strict Morphism of G,H; end; theorem :: MOD_2:11 for f being LModMorphismStr over R holds dom(f) = G & cod(f) = H & fun(f) is linear implies f is Morphism of G,H; theorem :: MOD_2:12 for f being map of G,H st f is linear holds LModMorphismStr (#G,H,f#) is strict Morphism of G,H; theorem :: MOD_2:13 id G is linear; definition let R,G; func ID G -> strict Morphism of G,G equals :: MOD_2:def 12 LModMorphismStr(# G,G,id G#); end; definition let R,G,H; redefine func ZERO(G,H) -> strict Morphism of G,H; end; theorem :: MOD_2:14 for F being Morphism of G,H ex f being map of G,H st the LModMorphismStr of F = LModMorphismStr(#G,H,f#) & f is linear; theorem :: MOD_2:15 for F being strict Morphism of G,H ex f being map of G,H st F = LModMorphismStr(#G,H,f#); theorem :: MOD_2:16 for F being LModMorphism of R ex G,H st F is Morphism of G,H; theorem :: MOD_2:17 for F being strict LModMorphism of R ex G,H being LeftMod of R, f being map of G,H st F is strict Morphism of G,H & F = LModMorphismStr(#G,H,f#) & f is linear; theorem :: MOD_2:18 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; definition let R; let G,F be LModMorphism of R; assume dom(G) = cod(F); func G*F -> strict LModMorphism of R means :: MOD_2:def 13 for G1,G2,G3 being LeftMod of R, g being map of G2,G3, f being map 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#); end; canceled; theorem :: MOD_2:20 for G being Morphism of G2,G3, F being Morphism of G1,G2 holds G*F is strict Morphism of G1,G3; 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 :: MOD_2:def 14 G*F; end; theorem :: MOD_2:21 for G being Morphism of G2,G3, F being Morphism of G1,G2, g being map of G2,G3, f being map 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#); theorem :: MOD_2:22 for f,g being strict LModMorphism of R st dom g = cod f holds ex G1,G2,G3 being LeftMod of R, f0 being map of G1,G2, g0 being map of G2,G3 st f = LModMorphismStr(#G1,G2,f0#) & g = LModMorphismStr(#G2,G3,g0#) & g*f = LModMorphismStr(#G1,G3,g0*f0#); theorem :: MOD_2:23 for f,g being strict LModMorphism of R st dom g = cod f holds dom(g*f) = dom f & cod (g*f) = cod g; theorem :: MOD_2:24 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; theorem :: MOD_2:25 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; theorem :: MOD_2:26 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); definition let x,y,z; cluster {x,y,z} -> non empty; end; canceled; theorem :: MOD_2:28 for u,v,w being Element of UN holds {u,v,w} is Element of UN; theorem :: MOD_2:29 for u being Element of UN holds succ u is Element of UN; theorem :: MOD_2:30 0 is Element of UN & 1 is Element of UN & 2 is Element of UN; reserve a,b,c for Element of {0,1,2}; definition let a; func -a -> Element of {0,1,2} equals :: MOD_2:def 15 0 if a = 0, 2 if a = 1, 1 if a = 2; let b; func a+b -> Element of {0,1,2} equals :: MOD_2:def 16 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; func a*b -> Element of {0,1,2} equals :: MOD_2:def 17 0 if b = 0, 0 if a = 0, a if b = 1, b if a = 1, 1 if a = 2 & b = 2; end; definition func add3 -> BinOp of {0,1,2} means :: MOD_2:def 18 it.(a,b) = a+b; func mult3 -> BinOp of {0,1,2} means :: MOD_2:def 19 it.(a,b) = a*b; func compl3 -> UnOp of {0,1,2} means :: MOD_2:def 20 it.a = -a; func unit3 -> Element of {0,1,2} equals :: MOD_2:def 21 1; func zero3 -> Element of {0,1,2} equals :: MOD_2:def 22 0; end; definition func Z3 -> strict doubleLoopStr equals :: MOD_2:def 23 doubleLoopStr (#{0,1,2},add3,mult3,unit3,zero3#); end; definition cluster Z3 -> non empty; end; canceled; theorem :: MOD_2:32 0.Z3 = 0 & 1_ Z3 = 1 & 0.Z3 is Element of {0,1,2} & 1_ Z3 is Element of {0,1,2} & the add of Z3 = add3 & the mult of Z3 = mult3; definition cluster Z3 -> add-associative right_zeroed right_complementable; end; theorem :: MOD_2:33 for x,y being Scalar of Z3, X,Y being Element of {0,1,2} st X=x & Y=y holds x+y = X+Y & x*y = X*Y & -x = -X; theorem :: MOD_2:34 for x,y,z being Scalar of Z3, 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); theorem :: MOD_2:35 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; theorem :: MOD_2:36 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<>(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; theorem :: MOD_2:37 Z3 is Fanoian Field; definition cluster Z3 -> Fanoian add-associative right_zeroed right_complementable Abelian commutative associative left_unital distributive Field-like; end; theorem :: MOD_2:38 for f being Function of D,D' st D in UN & D' in UN holds f in UN; canceled; theorem :: MOD_2:40 the carrier of Z3 in UN & the add of Z3 is Element of UN & comp Z3 is Element of UN & the Zero of Z3 is Element of UN & the mult of Z3 is Element of UN & the unity of Z3 is Element of UN;

Back to top