environ
vocabularies HIDDEN, GAUSSINT, NUMBERS, FINSEQ_1, SUBSET_1, RLVECT_1, STRUCT_0, PBOOLE, FUNCT_1, RAT_1, XBOOLE_0, ALGSTR_0, RELAT_1, ARYTM_3, CARD_3, BINOM, RLSUB_2, PRELAMB, XXREAL_0, TARSKI, CARD_1, SUPINF_2, MSSUBFAM, ARYTM_1, NAT_1, FUNCT_2, FINSET_1, VALUED_1, RLSUB_1, ZFMISC_1, INT_1, ORDINAL1, RLVECT_2, ZMODUL01, ZMODUL03, ORDERS_1, RLVECT_3, RMOD_2, RANKNULL, UNIALG_1, MSAFREE2, INT_3, VECTSP_1, XCMPLX_0, MESFUNC1, MOD_3, MONOID_0, VECTSP10, ZMODUL02, ZMODUL05, ZMODUL06, ZMODUL07, INT_2;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1, RELSET_1, PARTFUN1, FUNCT_2, BINOP_1, DOMAIN_1, FINSET_1, ORDERS_1, INT_2, CARD_1, NUMBERS, XCMPLX_0, XXREAL_0, NAT_1, INT_1, RAT_1, FINSEQ_1, FINSEQOP, STRUCT_0, ALGSTR_0, RLVECT_1, VECTSP_1, INT_3, VECTSP_4, VECTSP_5, VECTSP_6, VECTSP_7, MOD_2, BINOM, ZMODUL01, ZMODUL02, ZMODUL03, GAUSSINT, ZMODUL05, ZMODUL06;
definitions FUNCT_1, TARSKI, FUNCT_2, ALGSTR_0, VECTSP_7;
theorems BINOP_1, CARD_1, CARD_2, ENUMSET1, SUBSET_1, FINSEQ_1, FUNCT_1, FUNCT_2, INT_1, NAT_1, RLSUB_2, RLVECT_1, TARSKI, RANKNULL, ZMODUL01, BINOP_2, ZFMISC_1, RELAT_1, GAUSSINT, ZMODUL03, XBOOLE_0, XBOOLE_1, XCMPLX_1, XREAL_1, XXREAL_0, ORDINAL1, FINSET_1, ORDERS_1, VECTSP_1, INT_2, ZMODUL02, NAT_D, BINOM, RAT_1, ZMODUL04, RLVECT_3, ZMODUL05, ZMODUL06, VECTSP_6, VECTSP_4, VECTSP_7, MOD_2, STRUCT_0;
schemes FUNCT_2, NAT_1, FUNCT_1, XFAMILY;
registrations SUBSET_1, RELSET_1, FUNCT_2, FINSET_1, XREAL_0, STRUCT_0, RLVECT_1, MEMBERED, FINSEQ_1, CARD_1, INT_1, XBOOLE_0, ORDINAL1, XXREAL_0, NAT_1, INT_3, RELAT_1, VECTSP_1, GAUSSINT, RAT_1, XCMPLX_0, ZMODUL02, ZMODUL03, ZMODUL04, ZMODUL05, ZMODUL06;
constructors HIDDEN, BINOP_2, BINOM, UPROOTS, ORDERS_1, REALSET1, FINSEQOP, ALGSTR_1, ZMODUL01, ZMODUL02, EC_PF_1, ZMODUL04, ZMODUL05, ZMODUL06;
requirements HIDDEN, REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
equalities XCMPLX_0, STRUCT_0, ALGSTR_0, INT_3, GAUSSINT, VECTSP_4, VECTSP_6, ZMODUL02, VECTSP_1;
expansions TARSKI, STRUCT_0, ALGSTR_0, VECTSP_1, MOD_2, ZMODUL06, VECTSP_4, VECTSP_7;
LmDOMRNG:
for V, W being non empty 1-sorted
for T being Function of V,W holds
( dom T = [#] V & rng T c= [#] W )
LmTF1B:
for V being Z_Module
for I being finite Subset of V
for W being Submodule of V
for a being Element of INT.Ring st a <> 0. INT.Ring & ( for v being VECTOR of V st v in I holds
a * v in W ) holds
for v being VECTOR of V st v in Lin I holds
a * v in W
LmTF1A:
for V being free finite-rank Z_Module
for A being Subset of V st A is linearly-independent holds
ex B being finite Subset of V ex a being Element of INT.Ring st
( a <> 0. INT.Ring & A c= B & B is linearly-independent & ( for v being VECTOR of V holds a * v in Lin B ) )
ThTF1:
for V being Z_Module holds Z_ModuleQuot (V,(torsion_part V)) is torsion-free
definition
let V,
W be
Z_Module;
let T be
linear-transformation of
V,
W;
existence
ex b1 being linear-transformation of (Z_ModuleQuot (V,(ker T))),(im T) st
( b1 is bijective & ( for v being Element of V holds b1 . ((ZQMorph (V,(ker T))) . v) = T . v ) )
uniqueness
for b1, b2 being linear-transformation of (Z_ModuleQuot (V,(ker T))),(im T) st b1 is bijective & ( for v being Element of V holds b1 . ((ZQMorph (V,(ker T))) . v) = T . v ) & b2 is bijective & ( for v being Element of V holds b2 . ((ZQMorph (V,(ker T))) . v) = T . v ) holds
b1 = b2
end;