:: $\mathbb Z$-modules
:: by Yuichi Futa , Hiroyuki Okazaki and Yasunari Shidama
::
:: Received September 5, 2011
:: Copyright (c) 2011-2014 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, ALGSTR_0, STRUCT_0, SUBSET_1, BINOP_1, FUNCT_1,
ZFMISC_1, XBOOLE_0, RELAT_1, ARYTM_3, PARTFUN1, SUPINF_2, FUNCT_5,
MCART_1, ARYTM_1, CARD_1, FINSEQ_1, CARD_3, TARSKI, XXREAL_0, RLVECT_1,
REALSET1, RLSUB_1, ZMODUL01, INT_1, FINSEQ_4, LATTICES, EQREL_1, PBOOLE,
RLSUB_2, RMOD_2, RMOD_3, BINOM, NAT_1, INT_3, VECTSP_1, MESFUNC1,
BINOP_2, MOD_2, VECTSP_2;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1,
PARTFUN1, MCART_1, FUNCT_2, BINOP_1, DOMAIN_1, FUNCT_3, FUNCT_5, NUMBERS,
XCMPLX_0, XXREAL_0, INT_1, NAT_1, REALSET1, FINSEQ_1, BINOP_2, XREAL_0,
FINSEQ_4, STRUCT_0, ALGSTR_0, LATTICES, RLVECT_1, VECTSP_1, BINOM,
GROUP_1, VECTSP_2, INT_3, VECTSP_4, VECTSP_5, MOD_2;
constructors BINOP_1, NAT_1, FUNCT_3, FUNCT_5, REALSET1, RELSET_1, GROUP_1,
LATTICES, RLSUB_1, ALGSTR_1, BINOM, FINSEQ_4, VECTSP_1, INT_3, VECTSP_2,
VECTSP_4, BINOP_2, MOD_2, VECTSP_5;
registrations ORDINAL1, NUMBERS, XREAL_0, NAT_1, STRUCT_0, ALGSTR_0, FINSEQ_1,
CARD_1, SUBSET_1, INT_1, REALSET1, LATTICES, RELAT_1, ALGSTR_1, XTUPLE_0,
INT_3, XCMPLX_0, VECTSP_1, VECTSP_2, VECTSP_4, VECTSP_5;
requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
begin :: 1. Definition of Z-module
registration
cluster -> integer for Element of INT.Ring;
end;
registration
let a,b be Element of INT.Ring, c,d be Integer;
identify a * b with c * d when a = c, b = d;
identify a + b with c + d when a = c, b = d;
end;
registration
let a be Element of INT.Ring, b be Integer;
identify - a with - b when a = b;
end;
definition
::$CD 6
end;
definition
mode Z_Module is LeftMod of INT.Ring;
end;
registration
cluster TrivialLMod INT.Ring -> trivial non empty strict;
end;
registration
cluster strict for Z_Module;
end;
definition
let V be Z_Module;
mode VECTOR of V is Element of V;
end;
reserve x, y, y1 for set;
reserve a, b for Element of INT.Ring;
reserve V for Z_Module;
reserve v, w for Vector of V;
definition
let IT be Z_Module;
attr IT is Mult-cancelable means
:: ZMODUL01:def 7
for a being Element of INT.Ring
for v being Vector of IT st a * v = 0.IT holds
a = 0.INT.Ring or v = 0.IT;
end;
theorem :: ZMODUL01:1
a = 0.INT.Ring or v = 0.V implies a * v = 0.V;
theorem :: ZMODUL01:2
- v = (- 1.(INT.Ring)) * v;
theorem :: ZMODUL01:3
V is Mult-cancelable & v = - v implies v = 0.V;
theorem :: ZMODUL01:4
V is Mult-cancelable & v + v = 0.V implies v = 0.V;
theorem :: ZMODUL01:5
a * (- v) = (- a) * v;
theorem :: ZMODUL01:6
a * (- v) = - (a * v);
theorem :: ZMODUL01:7
(- a) * (- v) = a * v;
theorem :: ZMODUL01:8
a * (v - w) = a * v - a * w;
theorem :: ZMODUL01:9
(a - b) * v = a * v - b * v;
theorem :: ZMODUL01:10
V is Mult-cancelable & a <> 0.INT.Ring & a * v = a * w implies v = w;
theorem :: ZMODUL01:11
V is Mult-cancelable & v <> 0.V & a * v = b * v implies a = b;
reserve V for Z_Module;
reserve u,v,w for Vector of V;
reserve F,G,H,I for FinSequence of V;
reserve j,k,n for Nat;
reserve f,f9,g for sequence of V;
theorem :: ZMODUL01:12
len F = len G & (for k,v st k in dom F & v = G.k holds F.k = a * v)
implies Sum(F) = a * Sum(G);
theorem :: ZMODUL01:13
for V being Z_Module, a being Element of INT.Ring holds
a * Sum(<*>(the carrier of V)) = 0.V;
theorem :: ZMODUL01:14
for V being Z_Module, a being Element of INT.Ring,
v, u being Vector of V holds
a * Sum<* v,u *> = a * v + a * u;
theorem :: ZMODUL01:15
for V being Z_Module, a being Element of INT.Ring, v, u, w being Vector of V
holds a * Sum<* v,u,w *> = a * v + a * u + a * w;
theorem :: ZMODUL01:16
(- a) * v = - a * v;
theorem :: ZMODUL01:17
len F = len G & (for k st k in dom F holds G.k = a * F/.k )
implies Sum(G) = a * Sum(F);
begin :: 2. Submodules and cosets of submodules in Z-module
reserve V, X, Y for Z_Module;
reserve u, u1, u2, v, v1, v2 for Vector of V;
reserve a for Element of INT.Ring;
reserve V1, V2, V3 for Subset of V;
reserve x for set;
theorem :: ZMODUL01:18
V1 <> {} & V1 is linearly-closed implies 0.V in V1;
theorem :: ZMODUL01:19
V1 is linearly-closed implies for v st v in V1 holds - v in V1;
theorem :: ZMODUL01:20
V1 is linearly-closed implies for v, u st v in V1 & u in V1 holds v - u in V1
;
theorem :: ZMODUL01:21
the carrier of V = V1 implies V1 is linearly-closed;
theorem :: ZMODUL01:22
V1 is linearly-closed & V2 is linearly-closed &
V3 = {v + u : v in V1 & u in V2} implies
V3 is linearly-closed;
registration let V;
cluster {0.V} -> linearly-closed for Subset of V;
end;
registration let V;
cluster linearly-closed for Subset of V;
end;
registration let V;
let V1,V2 be linearly-closed Subset of V;
cluster V1 /\ V2 -> linearly-closed for Subset of V;
end;
definition
::$CD 2
end;
definition let V be Z_Module;
mode Submodule of V is Subspace of V;
end;
reserve W, W1, W2 for Submodule of V;
reserve w, w1, w2 for Vector of W;
theorem :: ZMODUL01:23
x in W1 & W1 is Submodule of W2 implies x in W2;
theorem :: ZMODUL01:24
for x being object holds x in W implies x in V;
theorem :: ZMODUL01:25
w is Vector of V;
theorem :: ZMODUL01:26
0.W = 0.V;
theorem :: ZMODUL01:27
0.W1 = 0.W2;
theorem :: ZMODUL01:28
w1 = v & w2 = u implies w1 + w2 = v + u;
theorem :: ZMODUL01:29
w = v implies a * w = a * v;
theorem :: ZMODUL01:30
w = v implies - v = - w;
theorem :: ZMODUL01:31
w1 = v & w2 = u implies w1 - w2 = v - u;
theorem :: ZMODUL01:32
V is Submodule of V;
theorem :: ZMODUL01:33
0.V in W;
theorem :: ZMODUL01:34
0.W1 in W2;
theorem :: ZMODUL01:35
0.W in V;
theorem :: ZMODUL01:36
u in W & v in W implies u + v in W;
theorem :: ZMODUL01:37
v in W implies a * v in W;
theorem :: ZMODUL01:38
v in W implies - v in W;
theorem :: ZMODUL01:39
u in W & v in W implies u - v in W;
reserve D for non empty set;
reserve d1 for Element of D;
reserve A for BinOp of D;
reserve M for Function of [:the carrier of INT.Ring,D:],D;
theorem :: ZMODUL01:40
V1 = D & d1 = 0.V & A = (the addF of V) || V1 &
M = (the lmult of V) | [:the carrier of INT.Ring,V1:] implies
ModuleStr (# D,A,d1,M #) is Submodule of V;
theorem :: ZMODUL01:41
for V,X being strict Z_Module st V is Submodule of X &
X is Submodule of V holds V = X;
theorem :: ZMODUL01:42
V is Submodule of X & X is Submodule of Y implies V is Submodule of Y;
theorem :: ZMODUL01:43
the carrier of W1 c= the carrier of W2 implies W1 is Submodule of W2;
theorem :: ZMODUL01:44
(for v st v in W1 holds v in W2) implies W1 is Submodule of W2;
registration let V;
cluster strict for Submodule of V;
end;
theorem :: ZMODUL01:45
for W1, W2 being strict Submodule of V holds
the carrier of W1 = the carrier of W2 implies W1 = W2;
theorem :: ZMODUL01:46
for W1, W2 being strict Submodule of V holds
(for v holds v in W1 iff v in W2) implies W1 = W2;
theorem :: ZMODUL01:47
for V being strict Z_Module, W being strict Submodule of V holds
the carrier of W = the carrier of V implies W = V;
theorem :: ZMODUL01:48
for V being strict Z_Module, W being strict Submodule of V holds
(for v being Vector of V holds v in W iff v in V) implies W = V;
theorem :: ZMODUL01:49
the carrier of W = V1 implies V1 is linearly-closed;
theorem :: ZMODUL01:50
V1 <> {} & V1 is linearly-closed implies
ex W being strict Submodule of V st V1 = the carrier of W;
theorem :: ZMODUL01:51
(0).W = (0).V;
theorem :: ZMODUL01:52
(0).W1 = (0).W2;
theorem :: ZMODUL01:53
(0).W is Submodule of V;
theorem :: ZMODUL01:54
(0).V is Submodule of W;
theorem :: ZMODUL01:55
(0).W1 is Submodule of W2;
theorem :: ZMODUL01:56
for V being Z_Module holds V is Submodule of (Omega).V;
definition
::$CD 4
end;
reserve B,C for Coset of W;
theorem :: ZMODUL01:57
0.V in v + W iff v in W;
theorem :: ZMODUL01:58
v in v + W;
theorem :: ZMODUL01:59
0.V + W = the carrier of W;
theorem :: ZMODUL01:60
v + (0).V = {v};
theorem :: ZMODUL01:61
v + (Omega).V = the carrier of V;
theorem :: ZMODUL01:62
0.V in v + W iff v + W = the carrier of W;
theorem :: ZMODUL01:63
v in W iff v + W = the carrier of W;
theorem :: ZMODUL01:64
v in W implies (a * v) + W = the carrier of W;
theorem :: ZMODUL01:65
u in W iff v + W = (v + u) + W;
theorem :: ZMODUL01:66
u in W iff v + W = (v - u) + W;
theorem :: ZMODUL01:67
v in u + W iff u + W = v + W;
theorem :: ZMODUL01:68
u in v1 + W & u in v2 + W implies v1 + W = v2 + W;
theorem :: ZMODUL01:69
v in W implies a * v in v + W;
theorem :: ZMODUL01:70
u + v in v + W iff u in W;
theorem :: ZMODUL01:71
v - u in v + W iff u in W;
theorem :: ZMODUL01:72
u in v + W iff ex v1 st v1 in W & u = v + v1;
theorem :: ZMODUL01:73
u in v + W iff ex v1 st v1 in W & u = v - v1;
theorem :: ZMODUL01:74
(ex v st v1 in v + W & v2 in v + W) iff v1 - v2 in W;
theorem :: ZMODUL01:75
v + W = u + W implies ex v1 st v1 in W & v + v1 = u;
theorem :: ZMODUL01:76
v + W = u + W implies ex v1 st v1 in W & v - v1 = u;
theorem :: ZMODUL01:77
for W1, W2 being strict Submodule of V st v + W1 = v + W2 holds W1 = W2;
theorem :: ZMODUL01:78
for W1, W2 being strict Submodule of V st v + W1 = u + W2 holds W1 = W2;
theorem :: ZMODUL01:79
C is linearly-closed iff C = the carrier of W;
theorem :: ZMODUL01:80
for W1, W2 being strict Submodule of V, C1 being Coset of W1,
C2 being Coset of W2 st C1 = C2 holds W1 = W2;
theorem :: ZMODUL01:81
{v} is Coset of (0).V;
theorem :: ZMODUL01:82
V1 is Coset of (0).V implies ex v st V1 = {v};
theorem :: ZMODUL01:83
the carrier of W is Coset of W;
theorem :: ZMODUL01:84
the carrier of V is Coset of (Omega).V;
theorem :: ZMODUL01:85
V1 is Coset of (Omega).V implies V1 = the carrier of V;
theorem :: ZMODUL01:86
0.V in C iff C = the carrier of W;
theorem :: ZMODUL01:87
u in C iff C = u + W;
theorem :: ZMODUL01:88
u in C & v in C implies ex v1 st v1 in W & u + v1 = v;
theorem :: ZMODUL01:89
u in C & v in C implies ex v1 st v1 in W & u - v1 = v;
theorem :: ZMODUL01:90
(ex C st v1 in C & v2 in C) iff v1 - v2 in W;
theorem :: ZMODUL01:91
u in B & u in C implies B = C;
begin :: 3. Operations on submodules in Z-module
reserve V for Z_Module;
reserve W, W1, W2, W3 for Submodule of V;
reserve u, u1, u2, v, v1, v2 for Vector of V;
reserve a, a1, a2 for Element of INT.Ring;
reserve X, Y, y, y1, y2 for set;
definition let GF be add-associative right_zeroed right_complementable
Abelian associative well-unital distributive non empty doubleLoopStr;
let M be Abelian add-associative right_zeroed right_complementable
vector-distributive scalar-distributive scalar-associative scalar-unital
non empty ModuleStr over GF;
let W1, W2 be Subspace of M;
redefine func W1 + W2;
commutativity;
end;
theorem :: ZMODUL01:92
x in W1 + W2 iff ex v1, v2 st v1 in W1 & v2 in W2 & x = v1 + v2;
theorem :: ZMODUL01:93
v in W1 or v in W2 implies v in W1 + W2;
theorem :: ZMODUL01:94
for x being object holds x in W1 /\ W2 iff x in W1 & x in W2;
theorem :: ZMODUL01:95
for W being strict Submodule of V holds W + W = W;
theorem :: ZMODUL01:96
W1 + (W2 + W3) = (W1 + W2) + W3;
theorem :: ZMODUL01:97
W1 is Submodule of W1 + W2;
theorem :: ZMODUL01:98
for W2 being strict Submodule of V holds
W1 is Submodule of W2 iff W1 + W2 = W2;
theorem :: ZMODUL01:99
for W being strict Submodule of V holds (0).V + W = W;
theorem :: ZMODUL01:100
(0).V + (Omega).V = the ModuleStr of V;
theorem :: ZMODUL01:101
(Omega).V + W = the ModuleStr of V;
theorem :: ZMODUL01:102
for V being strict Z_Module holds (Omega).V + (Omega).V = V;
theorem :: ZMODUL01:103
for W being strict Submodule of V holds W /\ W = W;
theorem :: ZMODUL01:104
W1 /\ (W2 /\ W3) = (W1 /\ W2) /\ W3;
theorem :: ZMODUL01:105
W1 /\ W2 is Submodule of W1;
theorem :: ZMODUL01:106
for W1 being strict Submodule of V holds W1 is Submodule of W2 iff
W1 /\ W2 = W1;
theorem :: ZMODUL01:107
(0).V /\ W = (0).V;
theorem :: ZMODUL01:108
(0).V /\ (Omega).V = (0).V;
theorem :: ZMODUL01:109
for W being strict Submodule of V holds (Omega).V /\ W = W;
theorem :: ZMODUL01:110
for V being strict Z_Module holds (Omega).V /\ (Omega).V = V;
theorem :: ZMODUL01:111
W1 /\ W2 is Submodule of W1 + W2;
theorem :: ZMODUL01:112
for W2 being strict Submodule of V
holds (W1 /\ W2) + W2 = W2;
theorem :: ZMODUL01:113
for W1 being strict Submodule of V holds
W1 /\ (W1 + W2) = W1;
theorem :: ZMODUL01:114
(W1 /\ W2) + (W2 /\ W3) is Submodule of W2 /\ (W1 + W3);
theorem :: ZMODUL01:115
W1 is Submodule of W2 implies W2 /\ (W1 + W3) = (W1 /\ W2) + (W2 /\ W3);
theorem :: ZMODUL01:116
W2 + (W1 /\ W3) is Submodule of (W1 + W2) /\ (W2 + W3);
theorem :: ZMODUL01:117
W1 is Submodule of W2 implies W2 + (W1 /\ W3) = (W1 + W2) /\ (W2 + W3);
theorem :: ZMODUL01:118
W1 is strict Submodule of W3 implies W1 + (W2 /\ W3) = (W1 + W2) /\ W3;
theorem :: ZMODUL01:119
for W1,W2 being strict Submodule of V holds W1 + W2 = W2 iff W1 /\ W2 = W1;
theorem :: ZMODUL01:120
for W2,W3 being strict Submodule of V holds W1 is Submodule of W2
implies W1 + W3 is Submodule of W2 + W3;
theorem :: ZMODUL01:121
(ex W st the carrier of W = (the carrier of W1) \/ (the carrier of W2))
iff W1 is Submodule of W2 or W2 is Submodule of W1;
notation let GF be add-associative right_zeroed right_complementable Abelian
associative well-unital distributive non empty doubleLoopStr;
let V be Abelian add-associative right_zeroed right_complementable
vector-distributive scalar-distributive scalar-associative
scalar-unital non empty ModuleStr over GF;
synonym Submodules V for Subspaces(V);
end;
registration let V;
cluster Submodules(V) -> non empty;
end;
theorem :: ZMODUL01:122
for V being strict Z_Module holds V in Submodules(V);
definition
::$CD 3
let V be Z_Module;
let W be Submodule of V;
attr W is with_Linear_Compl means
:: ZMODUL01:def 17
ex C being Submodule of V st V is_the_direct_sum_of C,W;
end;
registration
let V be Z_Module;
cluster with_Linear_Compl for Submodule of V;
end;
definition
let V be Z_Module;
let W be Submodule of V;
assume W is with_Linear_Compl;
mode Linear_Compl of W -> Submodule of V means
:: ZMODUL01:def 18
V is_the_direct_sum_of it,W;
end;
theorem :: ZMODUL01:123
for V being Z_Module, W1, W2 being Submodule of V holds V
is_the_direct_sum_of W1,W2 implies W2 is Linear_Compl of W1;
theorem :: ZMODUL01:124
for V being Z_Module, W being with_Linear_Compl Submodule of V,
L being Linear_Compl of W holds
V is_the_direct_sum_of L,W & V is_the_direct_sum_of W,L;
theorem :: ZMODUL01:125
for V being Z_Module, W being with_Linear_Compl Submodule of V, L being
Linear_Compl of W holds W + L = the ModuleStr of V;
theorem :: ZMODUL01:126
for V being Z_Module, W being with_Linear_Compl Submodule of V,
L being Linear_Compl of W holds W /\ L = (0).V;
theorem :: ZMODUL01:127
V is_the_direct_sum_of W1,W2
implies V is_the_direct_sum_of W2,W1;
theorem :: ZMODUL01:128
for V being Z_Module, W being with_Linear_Compl Submodule of V,
L being Linear_Compl of W holds W is Linear_Compl of L;
theorem :: ZMODUL01:129
for V being Z_Module holds V is_the_direct_sum_of (0).V, (Omega).V &
V is_the_direct_sum_of (Omega).V,(0).V;
theorem :: ZMODUL01:130
for V being Z_Module holds (0).V is Linear_Compl of (Omega).V &
(Omega).V is Linear_Compl of (0).V;
reserve C for Coset of W;
reserve C1 for Coset of W1;
reserve C2 for Coset of W2;
theorem :: ZMODUL01:131
C1 meets C2 implies C1 /\ C2 is Coset of W1 /\ W2;
theorem :: ZMODUL01:132
for V being Z_Module, W1, W2 being Submodule of V holds V
is_the_direct_sum_of W1,W2 iff for C1 being Coset of W1, C2 being Coset of W2
ex v being Vector of V st C1 /\ C2 = {v};
theorem :: ZMODUL01:133
for V being Z_Module, W1,W2 being Submodule of V holds
W1 + W2 = the ModuleStr of V
iff for v being Vector of V ex v1, v2 being Vector of V
st v1 in W1 & v2 in W2 & v = v1 + v2;
theorem :: ZMODUL01:134
V is_the_direct_sum_of W1,W2 & v1 + v2 = u1 + u2 & v1 in
W1 & u1 in W1 & v2 in W2 & u2 in W2 implies v1 = u1 & v2 = u2;
theorem :: ZMODUL01:135
V = W1 + W2 & (ex v st for v1,v2,u1,u2 st v1 + v2 = u1 + u2 &
v1 in W1 & u1 in W1 & v2 in W2 & u2 in W2 holds v1 = u1 & v2 = u2) implies
V is_the_direct_sum_of W1,W2;
definition
::$CD
end;
theorem :: ZMODUL01:136
V is_the_direct_sum_of W1,W2 implies (v |-- (W1,W2))`1 = (v |-- (W2,W1))`2;
theorem :: ZMODUL01:137
V is_the_direct_sum_of W1,W2 implies (v |-- (W1,W2))`2 = (v |-- (W2,W1))`1;
theorem :: ZMODUL01:138
for V being Z_Module, W being with_Linear_Compl Submodule of V,
L being Linear_Compl of W, v being Vector of V,
t being Element of [:the carrier of V, the carrier of V:]
holds t`1 + t`2 = v & t`1 in W & t`2 in L implies t = v |-- (W,L);
theorem :: ZMODUL01:139
for V being Z_Module, W being with_Linear_Compl Submodule of V,
L being Linear_Compl of W, v being Vector of V holds
(v |-- (W,L))`1 + (v |-- (W,L))`2 = v;
theorem :: ZMODUL01:140
for V being Z_Module, W being with_Linear_Compl Submodule of V,
L being Linear_Compl of W, v being Vector of V holds
(v |-- (W,L))`1 in W & (v |-- (W,L))`2 in L;
theorem :: ZMODUL01:141
for V being Z_Module, W being with_Linear_Compl Submodule of V,
L being Linear_Compl of W, v being Vector of V holds
(v |-- (W,L))`1 = (v |-- (L,W))`2;
theorem :: ZMODUL01:142
for V being Z_Module, W being with_Linear_Compl Submodule of V,
L being Linear_Compl of W, v being Vector of V holds
(v |-- (W,L))`2 = (v |-- (L,W))`1;
reserve A1,A2,B for Element of Submodules(V);
theorem :: ZMODUL01:143
LattStr (# Submodules(V), SubJoin(V), SubMeet(V) #) is Lattice;
registration let V;
cluster LattStr (# Submodules(V), SubJoin(V), SubMeet(V) #)
-> Lattice-like;
end;
theorem :: ZMODUL01:144
for V being Z_Module holds LattStr (# Submodules(V),
SubJoin(V), SubMeet(V) #) is lower-bounded;
theorem :: ZMODUL01:145
for V being Z_Module holds LattStr (# Submodules(V),
SubJoin(V), SubMeet(V) #) is upper-bounded;
theorem :: ZMODUL01:146
for V being Z_Module holds LattStr (# Submodules(V),
SubJoin(V), SubMeet(V) #) is 01_Lattice;
theorem :: ZMODUL01:147
for V being Z_Module holds LattStr (# Submodules(V),
SubJoin(V), SubMeet(V) #) is modular;
theorem :: ZMODUL01:148
for V being Z_Module, W1,W2,W3 being strict Submodule of V holds
W1 is Submodule of W2 implies W1 /\ W3 is Submodule of W2 /\ W3;
theorem :: ZMODUL01:149
for V being Z_Module, W being strict Submodule of V holds
(for v being Vector of V holds v in W) implies
W = the ModuleStr of V;
theorem :: ZMODUL01:150
ex C st v in C;
begin :: 4.Transformation of Abelian group to Z-module
definition
let AG be non empty addLoopStr;
func Int-mult-left(AG) -> Function of
[:the carrier of INT.Ring,
the carrier of AG:], the carrier of AG means
:: ZMODUL01:def 20
for i being Element of INT.Ring, a being Element of AG holds
(i >= 0 implies it.(i,a) = (Nat-mult-left(AG)).(i,a)) &
(i < 0 implies it.(i,a) = (Nat-mult-left(AG)).(-i,-a));
end;
theorem :: ZMODUL01:151
for R being non empty addLoopStr, a being Element of R,
i be Element of INT.Ring, i1 be Element of NAT st i=i1 holds
(Int-mult-left(R)).(i,a) = i1 * a;
theorem :: ZMODUL01:152
for R being non empty addLoopStr, a being Element of R,
i be Integer st i=0 holds
(Int-mult-left(R)).(i,a) = 0.R;
theorem :: ZMODUL01:153
for R being add-associative right_zeroed right_complementable
non empty addLoopStr,
i be Element of NAT holds
(Nat-mult-left(R)).(i,0.R) = 0.R;
theorem :: ZMODUL01:154
for R being add-associative right_zeroed right_complementable
non empty addLoopStr,
i be Element of INT.Ring holds
(Int-mult-left(R)).(i,0.R) = 0.R;
theorem :: ZMODUL01:155
for R being right_zeroed non empty addLoopStr, a being Element of R,
i be Integer st i = 1
holds (Int-mult-left(R)).(i,a) = a;
theorem :: ZMODUL01:156
for R being Abelian right_zeroed add-associative right_complementable
non empty addLoopStr,
a being Element of R, i, j, k being Element of NAT
st i <= j & k = j-i holds
(Nat-mult-left(R)).(k,a)
= (Nat-mult-left(R)).(j,a) - (Nat-mult-left(R)).(i,a);
theorem :: ZMODUL01:157
for R being Abelian right_zeroed add-associative right_complementable
non empty addLoopStr,
a being Element of R, i being Element of NAT
holds -(Nat-mult-left(R)).(i,a) = (Nat-mult-left(R)).(i,-a);
theorem :: ZMODUL01:158
for R being Abelian right_zeroed add-associative right_complementable
non empty addLoopStr,
a being Element of R, i, j being Element of INT.Ring
st i in NAT & not j in NAT
holds (Int-mult-left(R)).(i+j,a)
= (Int-mult-left(R)).(i,a) + (Int-mult-left(R)).(j,a);
theorem :: ZMODUL01:159
for R being Abelian right_zeroed add-associative
right_complementable non empty addLoopStr,
a being Element of R, i, j being Element of INT.Ring
holds (Int-mult-left(R)).(i+j,a)
= (Int-mult-left(R)).(i,a) + (Int-mult-left(R)).(j,a);
theorem :: ZMODUL01:160
for R being Abelian right_zeroed add-associative
right_complementable non empty addLoopStr,
a, b being Element of R, i being Element of NAT
holds (Nat-mult-left(R)).(i,a+b)
= (Nat-mult-left(R)).(i,a) + (Nat-mult-left(R)).(i,b);
theorem :: ZMODUL01:161
for R being Abelian right_zeroed add-associative
right_complementable non empty addLoopStr,
a, b being Element of R, i being Element of INT.Ring
holds (Int-mult-left(R)).(i,a+b)
= (Int-mult-left(R)).(i,a) + (Int-mult-left(R)).(i,b);
theorem :: ZMODUL01:162
for R being Abelian right_zeroed add-associative
right_complementable non empty addLoopStr,
a being Element of R, i, j being Element of NAT holds
(Nat-mult-left(R)).(i*j,a) = (Nat-mult-left(R)).(i,(Nat-mult-left(R)).(j,a));
theorem :: ZMODUL01:163
for R being Abelian right_zeroed add-associative right_complementable
non empty addLoopStr,
a being Element of R, i, j being Element of INT.Ring holds
(Int-mult-left(R)).(i*j,a) = (Int-mult-left(R)).(i,(Int-mult-left(R)).(j,a));
theorem :: ZMODUL01:164
for AG be non empty Abelian add-associative right_zeroed
right_complementable addLoopStr holds
ModuleStr (# the carrier of AG, the addF of AG, the ZeroF of AG,
Int-mult-left(AG) #) is Z_Module;