:: by Yuichi Futa , Hiroyuki Okazaki and Yasunari Shidama

::

:: Received August 14, 2015

:: Copyright (c) 2015-2019 Association of Mizar Users

registration

ex b_{1} being Element of INT.Ring st

( b_{1} is prime & not b_{1} is zero )
end;

cluster V31() integer non zero complex ext-real rational prime g_integer g_rational for Element of the carrier of INT.Ring;

existence ex b

( b

proof end;

registration
end;

LmDOMRNG: for V, W being non empty 1-sorted

for T being Function of V,W holds

( dom T = [#] V & rng T c= [#] W )

proof end;

theorem LmTF1: :: ZMODUL07:2

for V being Z_Module

for A being Subset of V st A is linearly-independent holds

ex B being Subset of V st

( A c= B & B is linearly-independent & ( for v being VECTOR of V ex a being Element of INT.Ring st

( a <> 0 & a * v in Lin B ) ) )

for A being Subset of V st A is linearly-independent holds

ex B being Subset of V st

( A c= B & B is linearly-independent & ( for v being VECTOR of V ex a being Element of INT.Ring st

( a <> 0 & a * v in Lin B ) ) )

proof end;

theorem LmTF1C: :: ZMODUL07:3

for V being Z_Module

for I being finite Subset of V

for W being Submodule of V st ( for v being VECTOR of V st v in I holds

ex a being Element of INT.Ring st

( a <> 0. INT.Ring & a * v in W ) ) holds

ex 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 ) )

for I being finite Subset of V

for W being Submodule of V st ( for v being VECTOR of V st v in I holds

ex a being Element of INT.Ring st

( a <> 0. INT.Ring & a * v in W ) ) holds

ex 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 ) )

proof end;

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

proof end;

theorem LmTF1D: :: ZMODUL07:4

for V being free finite-rank Z_Module

for I being linearly-independent Subset of V holds I is finite

for I being linearly-independent Subset of V holds I is finite

proof end;

registration

let V be free finite-rank Z_Module;

coherence

for b_{1} being Subset of V st b_{1} is linearly-independent holds

b_{1} is finite
by LmTF1D;

end;
coherence

for b

b

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 ) )

proof end;

theorem LmRankSX11: :: ZMODUL07:5

for V being free finite-rank Z_Module

for A being linearly-independent Subset of V ex I being finite linearly-independent Subset of V ex a being Element of INT.Ring st

( a <> 0. INT.Ring & A c= I & a (*) V is Submodule of Lin I )

for A being linearly-independent Subset of V ex I being finite linearly-independent Subset of V ex a being Element of INT.Ring st

( a <> 0. INT.Ring & A c= I & a (*) V is Submodule of Lin I )

proof end;

theorem LmRankSX1: :: ZMODUL07:6

for V being free finite-rank Z_Module

for A being linearly-independent Subset of V ex I being finite linearly-independent Subset of V st

( A c= I & rank V = card I )

for A being linearly-independent Subset of V ex I being finite linearly-independent Subset of V st

( A c= I & rank V = card I )

proof end;

theorem LmRankSX2: :: ZMODUL07:7

for V being torsion-free Z_Module

for W1, W2 being free finite-rank Submodule of V

for I1 being Basis of W1 ex I being finite linearly-independent Subset of V st

( I is Subset of (W1 + W2) & I1 c= I & rank (W1 + W2) = rank (Lin I) )

for W1, W2 being free finite-rank Submodule of V

for I1 being Basis of W1 ex I being finite linearly-independent Subset of V st

( I is Subset of (W1 + W2) & I1 c= I & rank (W1 + W2) = rank (Lin I) )

proof end;

theorem :: ZMODUL07:8

for V being torsion-free Z_Module

for W1, W2 being free finite-rank Submodule of V st W2 is Submodule of W1 holds

ex W3 being free finite-rank Submodule of V st

( rank W1 = (rank W2) + (rank W3) & W2 /\ W3 = (0). V & W3 is Submodule of W1 )

for W1, W2 being free finite-rank Submodule of V st W2 is Submodule of W1 holds

ex W3 being free finite-rank Submodule of V st

( rank W1 = (rank W2) + (rank W3) & W2 /\ W3 = (0). V & W3 is Submodule of W1 )

proof end;

theorem :: ZMODUL07:9

for V being torsion-free Z_Module

for W1, W2 being free finite-rank Submodule of V ex W3 being free finite-rank Submodule of V st

( rank (W1 + W2) = (rank W1) + (rank W3) & W1 /\ W3 = (0). V & W3 is Submodule of W1 + W2 )

for W1, W2 being free finite-rank Submodule of V ex W3 being free finite-rank Submodule of V st

( rank (W1 + W2) = (rank W1) + (rank W3) & W1 /\ W3 = (0). V & W3 is Submodule of W1 + W2 )

proof end;

theorem :: ZMODUL07:10

for V being free finite-rank Z_Module

for W1, W2 being Submodule of V holds rank (W1 /\ W2) >= ((rank W1) + (rank W2)) - (rank V)

for W1, W2 being Submodule of V holds rank (W1 /\ W2) >= ((rank W1) + (rank W2)) - (rank V)

proof end;

definition

let V be LeftMod of INT.Ring ;

ex b_{1} being strict Subspace of V st the carrier of b_{1} = { v where v is Vector of V : v is torsion }

for b_{1}, b_{2} being strict Subspace of V st the carrier of b_{1} = { v where v is Vector of V : v is torsion } & the carrier of b_{2} = { v where v is Vector of V : v is torsion } holds

b_{1} = b_{2}
by ZMODUL01:45;

end;
func torsion_part V -> strict Subspace of V means :defTorsionPart: :: ZMODUL07:def 1

the carrier of it = { v where v is Vector of V : v is torsion } ;

existence the carrier of it = { v where v is Vector of V : v is torsion } ;

ex b

proof end;

uniqueness for b

b

:: deftheorem defTorsionPart defines torsion_part ZMODUL07:def 1 :

for V being LeftMod of INT.Ring

for b_{2} being strict Subspace of V holds

( b_{2} = torsion_part V iff the carrier of b_{2} = { v where v is Vector of V : v is torsion } );

for V being LeftMod of INT.Ring

for b

( b

ThTF1: for V being Z_Module holds VectQuot (V,(torsion_part V)) is torsion-free

proof end;

registration
end;

definition

let R be Ring;

let V be LeftMod of R;

let W be Subspace of V;

ex b_{1} being linear-transformation of V,(VectQuot (V,W)) st

for v being Element of V holds b_{1} . v = v + W

for b_{1}, b_{2} being linear-transformation of V,(VectQuot (V,W)) st ( for v being Element of V holds b_{1} . v = v + W ) & ( for v being Element of V holds b_{2} . v = v + W ) holds

b_{1} = b_{2}

end;
let V be LeftMod of R;

let W be Subspace of V;

func ZQMorph (V,W) -> linear-transformation of V,(VectQuot (V,W)) means :defMophVW: :: ZMODUL07:def 2

for v being Element of V holds it . v = v + W;

existence for v being Element of V holds it . v = v + W;

ex b

for v being Element of V holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem defMophVW defines ZQMorph ZMODUL07:def 2 :

for R being Ring

for V being LeftMod of R

for W being Subspace of V

for b_{4} being linear-transformation of V,(VectQuot (V,W)) holds

( b_{4} = ZQMorph (V,W) iff for v being Element of V holds b_{4} . v = v + W );

for R being Ring

for V being LeftMod of R

for W being Subspace of V

for b

( b

registration

let R be Ring;

let V be LeftMod of R;

let W be Subspace of V;

coherence

ZQMorph (V,W) is onto

end;
let V be LeftMod of R;

let W be Subspace of V;

coherence

ZQMorph (V,W) is onto

proof end;

theorem :: ZMODUL07:13

for V, W being Z_Module

for T being linear-transformation of V,W

for s being FinSequence of V

for t being FinSequence of W st len s = len t & ( for i being Element of NAT st i in dom s holds

ex si being VECTOR of V st

( si = s . i & t . i = T . si ) ) holds

Sum t = T . (Sum s)

for T being linear-transformation of V,W

for s being FinSequence of V

for t being FinSequence of W st len s = len t & ( for i being Element of NAT st i in dom s holds

ex si being VECTOR of V st

( si = s . i & t . i = T . si ) ) holds

Sum t = T . (Sum s)

proof end;

registration

let V be finitely-generated Z_Module;

let W be Submodule of V;

coherence

VectQuot (V,W) is finitely-generated

end;
let W be Submodule of V;

coherence

VectQuot (V,W) is finitely-generated

proof end;

registration

let V be finitely-generated Z_Module;

correctness

coherence

VectQuot (V,(torsion_part V)) is free ;

;

end;
correctness

coherence

VectQuot (V,(torsion_part V)) is free ;

;

definition

ModuleStr(# the carrier of F_Rat, the addF of F_Rat, the ZeroF of F_Rat,(Int-mult-left F_Rat) #) is ModuleStr over INT.Ring ;

end;

func Rat-Module -> ModuleStr over INT.Ring equals :: ZMODUL07:def 3

ModuleStr(# the carrier of F_Rat, the addF of F_Rat, the ZeroF of F_Rat,(Int-mult-left F_Rat) #);

coherence ModuleStr(# the carrier of F_Rat, the addF of F_Rat, the ZeroF of F_Rat,(Int-mult-left F_Rat) #);

ModuleStr(# the carrier of F_Rat, the addF of F_Rat, the ZeroF of F_Rat,(Int-mult-left F_Rat) #) is ModuleStr over INT.Ring ;

:: deftheorem defines Rat-Module ZMODUL07:def 3 :

Rat-Module = ModuleStr(# the carrier of F_Rat, the addF of F_Rat, the ZeroF of F_Rat,(Int-mult-left F_Rat) #);

Rat-Module = ModuleStr(# the carrier of F_Rat, the addF of F_Rat, the ZeroF of F_Rat,(Int-mult-left F_Rat) #);

registration

coherence

( Rat-Module is Abelian & Rat-Module is add-associative & Rat-Module is right_zeroed & Rat-Module is right_complementable & Rat-Module is scalar-distributive & Rat-Module is vector-distributive & Rat-Module is scalar-associative & Rat-Module is scalar-unital );

end;

cluster Rat-Module -> right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ;

correctness coherence

( Rat-Module is Abelian & Rat-Module is add-associative & Rat-Module is right_zeroed & Rat-Module is right_complementable & Rat-Module is scalar-distributive & Rat-Module is vector-distributive & Rat-Module is scalar-associative & Rat-Module is scalar-unital );

proof end;

theorem LMTFRat1: :: ZMODUL07:14

for v being Element of F_Rat

for v1 being Rational st v = v1 holds

for n being Nat holds (Nat-mult-left F_Rat) . (n,v) = n * v1

for v1 being Rational st v = v1 holds

for n being Nat holds (Nat-mult-left F_Rat) . (n,v) = n * v1

proof end;

theorem LMTFRat2: :: ZMODUL07:15

for x being Integer

for v being Element of F_Rat

for v1 being Rational st v = v1 holds

(Int-mult-left F_Rat) . (x,v) = x * v1

for v being Element of F_Rat

for v1 being Rational st v = v1 holds

(Int-mult-left F_Rat) . (x,v) = x * v1

proof end;

registration
end;

registration
end;

registration
end;

theorem :: ZMODUL07:18

for A being finite Subset of Rat-Module ex n being Integer st

( n <> 0 & ( for s being Element of Rat-Module st s in Lin A holds

ex m being Integer st s = m / n ) )

( n <> 0 & ( for s being Element of Rat-Module st s in Lin A holds

ex m being Integer st s = m / n ) )

proof end;

registration

let W be free finite-rank Z_Module;

let V be Z_Module;

let T be linear-transformation of V,W;

correctness

coherence

( im T is finite-rank & im T is free );

;

end;
let V be Z_Module;

let T be linear-transformation of V,W;

correctness

coherence

( im T is finite-rank & im T is free );

;

definition

let W be free finite-rank Z_Module;

let V be Z_Module;

let T be linear-transformation of V,W;

coherence

rank (im T) is Nat ;

end;
let V be Z_Module;

let T be linear-transformation of V,W;

coherence

rank (im T) is Nat ;

:: deftheorem defines rank ZMODUL07:def 4 :

for W being free finite-rank Z_Module

for V being Z_Module

for T being linear-transformation of V,W holds rank T = rank (im T);

for W being free finite-rank Z_Module

for V being Z_Module

for T being linear-transformation of V,W holds rank T = rank (im T);

definition

let V be free finite-rank Z_Module;

let W be Z_Module;

let T be linear-transformation of V,W;

coherence

rank (ker T) is Nat ;

end;
let W be Z_Module;

let T be linear-transformation of V,W;

coherence

rank (ker T) is Nat ;

:: deftheorem defines nullity ZMODUL07:def 5 :

for V being free finite-rank Z_Module

for W being Z_Module

for T being linear-transformation of V,W holds nullity T = rank (ker T);

for V being free finite-rank Z_Module

for W being Z_Module

for T being linear-transformation of V,W holds nullity T = rank (ker T);

theorem ZM05Th35: :: ZMODUL07:20

for W, V being free finite-rank Z_Module

for A being Subset of V

for B being linearly-independent Subset of V

for T being linear-transformation of V,W st rank V = card B & A is Basis of (ker T) & A c= B holds

T | (B \ A) is one-to-one

for A being Subset of V

for B being linearly-independent Subset of V

for T being linear-transformation of V,W st rank V = card B & A is Basis of (ker T) & A c= B holds

T | (B \ A) is one-to-one

proof end;

theorem ZM05Th59: :: ZMODUL07:21

for W, V being free finite-rank Z_Module

for A being Subset of V

for B being linearly-independent Subset of V

for T being linear-transformation of V,W

for l being Linear_Combination of B \ A st rank V = card B & A is Basis of (ker T) & A c= B holds

T . (Sum l) = Sum (T @* l)

for A being Subset of V

for B being linearly-independent Subset of V

for T being linear-transformation of V,W

for l being Linear_Combination of B \ A st rank V = card B & A is Basis of (ker T) & A c= B holds

T . (Sum l) = Sum (T @* l)

proof end;

theorem LMTh441: :: ZMODUL07:22

for R being Ring

for V, W being LeftMod of R

for T being linear-transformation of V,W

for A being Subset of V st A c= the carrier of (ker T) holds

Lin (T .: A) = (0). W

for V, W being LeftMod of R

for T being linear-transformation of V,W

for A being Subset of V st A c= the carrier of (ker T) holds

Lin (T .: A) = (0). W

proof end;

theorem LMTh44: :: ZMODUL07:23

for R being Ring

for V, W being LeftMod of R

for T being linear-transformation of V,W

for A, B, X being Subset of V st A c= the carrier of (ker T) & X = B \/ A holds

Lin (T .: X) = Lin (T .: B)

for V, W being LeftMod of R

for T being linear-transformation of V,W

for A, B, X being Subset of V st A c= the carrier of (ker T) & X = B \/ A holds

Lin (T .: X) = Lin (T .: B)

proof end;

:: Rank-nullity theorem

theorem Th44: :: ZMODUL07:24

for V, W being free finite-rank Z_Module

for T being linear-transformation of V,W holds rank V = (rank T) + (nullity T)

for T being linear-transformation of V,W holds rank V = (rank T) + (nullity T)

proof end;

theorem :: ZMODUL07:25

for V, W being free finite-rank Z_Module

for T being linear-transformation of V,W st T is one-to-one holds

rank V = rank T

for T being linear-transformation of V,W st T is one-to-one holds

rank V = rank T

proof end;

::: canonical decomposition

definition

let R be Ring;

let V, W be LeftMod of R;

let T be linear-transformation of V,W;

ex b_{1} being linear-transformation of (VectQuot (V,(ker T))),(im T) st

( b_{1} is bijective & ( for v being Element of V holds b_{1} . ((ZQMorph (V,(ker T))) . v) = T . v ) )

for b_{1}, b_{2} being linear-transformation of (VectQuot (V,(ker T))),(im T) st b_{1} is bijective & ( for v being Element of V holds b_{1} . ((ZQMorph (V,(ker T))) . v) = T . v ) & b_{2} is bijective & ( for v being Element of V holds b_{2} . ((ZQMorph (V,(ker T))) . v) = T . v ) holds

b_{1} = b_{2}

end;
let V, W be LeftMod of R;

let T be linear-transformation of V,W;

func Zdecom T -> linear-transformation of (VectQuot (V,(ker T))),(im T) means :defdecom: :: ZMODUL07:def 6

( it is bijective & ( for v being Element of V holds it . ((ZQMorph (V,(ker T))) . v) = T . v ) );

existence ( it is bijective & ( for v being Element of V holds it . ((ZQMorph (V,(ker T))) . v) = T . v ) );

ex b

( b

proof end;

uniqueness for b

b

proof end;

:: deftheorem defdecom defines Zdecom ZMODUL07:def 6 :

for R being Ring

for V, W being LeftMod of R

for T being linear-transformation of V,W

for b_{5} being linear-transformation of (VectQuot (V,(ker T))),(im T) holds

( b_{5} = Zdecom T iff ( b_{5} is bijective & ( for v being Element of V holds b_{5} . ((ZQMorph (V,(ker T))) . v) = T . v ) ) );

for R being Ring

for V, W being LeftMod of R

for T being linear-transformation of V,W

for b

( b

theorem :: ZMODUL07:26

for R being Ring

for V, W being LeftMod of R

for T being linear-transformation of V,W holds T = (Zdecom T) * (ZQMorph (V,(ker T)))

for V, W being LeftMod of R

for T being linear-transformation of V,W holds T = (Zdecom T) * (ZQMorph (V,(ker T)))

proof end;

theorem LMFirst1: :: ZMODUL07:27

for R being Ring

for V, U, W being LeftMod of R

for f being linear-transformation of V,U

for g being linear-transformation of U,W holds g * f is linear-transformation of V,W

for V, U, W being LeftMod of R

for f being linear-transformation of V,U

for g being linear-transformation of U,W holds g * f is linear-transformation of V,W

proof end;

definition

let R be Ring;

let V, U, W be LeftMod of R;

let f be linear-transformation of V,U;

let g be linear-transformation of U,W;

:: original: (#)

redefine func g * f -> linear-transformation of V,W;

correctness

coherence

f (#) g is linear-transformation of V,W;

by LMFirst1;

end;
let V, U, W be LeftMod of R;

let f be linear-transformation of V,U;

let g be linear-transformation of U,W;

:: original: (#)

redefine func g * f -> linear-transformation of V,W;

correctness

coherence

f (#) g is linear-transformation of V,W;

by LMFirst1;

theorem LMFirst2: :: ZMODUL07:28

for R being Ring

for V, W being LeftMod of R

for f being linear-transformation of V,W holds the carrier of (ker f) = f " {(0. W)}

for V, W being LeftMod of R

for f being linear-transformation of V,W holds the carrier of (ker f) = f " {(0. W)}

proof end;

theorem LMFirst3: :: ZMODUL07:29

for R being Ring

for V, U, W being LeftMod of R

for f being linear-transformation of V,U

for g being linear-transformation of U,W holds the carrier of (ker (g * f)) = f " the carrier of (ker g)

for V, U, W being LeftMod of R

for f being linear-transformation of V,U

for g being linear-transformation of U,W holds the carrier of (ker (g * f)) = f " the carrier of (ker g)

proof end;

theorem LMFirst4: :: ZMODUL07:30

for R being Ring

for V, W being LeftMod of R

for f being linear-transformation of V,W st f is onto holds

im f = (Omega). W

for V, W being LeftMod of R

for f being linear-transformation of V,W st f is onto holds

im f = (Omega). W

proof end;

theorem LMFirst5: :: ZMODUL07:31

for R being Ring

for V being LeftMod of R

for W being Subspace of V holds ker (ZQMorph (V,W)) = (Omega). W

for V being LeftMod of R

for W being Subspace of V holds ker (ZQMorph (V,W)) = (Omega). W

proof end;

theorem LmStrict11a: :: ZMODUL07:32

for R being Ring

for V being LeftMod of R

for W being Subspace of V

for Ws being strict Subspace of V

for v being Vector of V st Ws = (Omega). W holds

v + W = v + Ws

for V being LeftMod of R

for W being Subspace of V

for Ws being strict Subspace of V

for v being Vector of V st Ws = (Omega). W holds

v + W = v + Ws

proof end;

theorem LmStrict11: :: ZMODUL07:33

for R being Ring

for V being LeftMod of R

for W being Subspace of V

for Ws being strict Subspace of V

for A being object st Ws = (Omega). W holds

( A is Coset of W iff A is Coset of Ws )

for V being LeftMod of R

for W being Subspace of V

for Ws being strict Subspace of V

for A being object st Ws = (Omega). W holds

( A is Coset of W iff A is Coset of Ws )

proof end;

theorem LmStrict1: :: ZMODUL07:34

for R being Ring

for V being LeftMod of R

for W being Subspace of V

for Ws being strict Subspace of V st Ws = (Omega). W holds

CosetSet (V,W) = CosetSet (V,Ws)

for V being LeftMod of R

for W being Subspace of V

for Ws being strict Subspace of V st Ws = (Omega). W holds

CosetSet (V,W) = CosetSet (V,Ws)

proof end;

theorem LmStrict2: :: ZMODUL07:35

for R being Ring

for V being LeftMod of R

for W being Subspace of V

for Ws being strict Subspace of V st Ws = (Omega). W holds

addCoset (V,W) = addCoset (V,Ws)

for V being LeftMod of R

for W being Subspace of V

for Ws being strict Subspace of V st Ws = (Omega). W holds

addCoset (V,W) = addCoset (V,Ws)

proof end;

theorem LmStrict3: :: ZMODUL07:36

for R being Ring

for V being LeftMod of R

for W being Subspace of V

for Ws being strict Subspace of V st Ws = (Omega). W holds

lmultCoset (V,W) = lmultCoset (V,Ws)

for V being LeftMod of R

for W being Subspace of V

for Ws being strict Subspace of V st Ws = (Omega). W holds

lmultCoset (V,W) = lmultCoset (V,Ws)

proof end;

theorem ThStrict1: :: ZMODUL07:37

for R being Ring

for V being LeftMod of R

for W being Subspace of V

for Ws being strict Subspace of V st Ws = (Omega). W holds

VectQuot (V,W) = VectQuot (V,Ws)

for V being LeftMod of R

for W being Subspace of V

for Ws being strict Subspace of V st Ws = (Omega). W holds

VectQuot (V,W) = VectQuot (V,Ws)

proof end;

theorem :: ZMODUL07:38

for R being Ring

for V, U being LeftMod of R

for V1 being Submodule of V

for U1 being Submodule of U

for f being linear-transformation of V,U st f is onto & the carrier of V1 = f " the carrier of U1 holds

ex F being linear-transformation of (VectQuot (V,V1)),(VectQuot (U,U1)) st F is bijective

for V, U being LeftMod of R

for V1 being Submodule of V

for U1 being Submodule of U

for f being linear-transformation of V,U st f is onto & the carrier of V1 = f " the carrier of U1 holds

ex F being linear-transformation of (VectQuot (V,V1)),(VectQuot (U,U1)) st F is bijective

proof end;

theorem :: ZMODUL07:39

for R being Ring

for V being LeftMod of R

for W1, W2 being Submodule of V

for U1 being Submodule of W1 + W2

for U2 being strict Submodule of W1 st U1 = W2 & U2 = W1 /\ W2 holds

ex F being linear-transformation of (VectQuot ((W1 + W2),U1)),(VectQuot (W1,U2)) st F is bijective

for V being LeftMod of R

for W1, W2 being Submodule of V

for U1 being Submodule of W1 + W2

for U2 being strict Submodule of W1 st U1 = W2 & U2 = W1 /\ W2 holds

ex F being linear-transformation of (VectQuot ((W1 + W2),U1)),(VectQuot (W1,U2)) st F is bijective

proof end;

theorem :: ZMODUL07:40

for R being Ring

for V being LeftMod of R

for W1 being Submodule of V

for W2 being Submodule of W1

for U1 being Submodule of V

for U2 being Submodule of VectQuot (V,U1) st U1 = W2 & U2 = VectQuot (W1,W2) holds

ex F being linear-transformation of (VectQuot ((VectQuot (V,U1)),U2)),(VectQuot (V,W1)) st F is bijective

for V being LeftMod of R

for W1 being Submodule of V

for W2 being Submodule of W1

for U1 being Submodule of V

for U2 being Submodule of VectQuot (V,U1) st U1 = W2 & U2 = VectQuot (W1,W2) holds

ex F being linear-transformation of (VectQuot ((VectQuot (V,U1)),U2)),(VectQuot (V,W1)) st F is bijective

proof end;

registration

let V be Z_Module;

let a be non zero Element of INT.Ring;

correctness

coherence

VectQuot (V,(a (*) V)) is torsion ;

end;
let a be non zero Element of INT.Ring;

correctness

coherence

VectQuot (V,(a (*) V)) is torsion ;

proof end;

theorem ThTrivial2: :: ZMODUL07:42

for R being Ring

for V being LeftMod of R

for v being Vector of V st v <> 0. V holds

not Lin {v} is trivial

for V being LeftMod of R

for v being Vector of V st v <> 0. V holds

not Lin {v} is trivial

proof end;

theorem LMCLUS1: :: ZMODUL07:43

ex V being Z_Module ex p being Element of INT.Ring st

( p <> 0. INT.Ring & not VectQuot (V,(p (*) V)) is trivial )

( p <> 0. INT.Ring & not VectQuot (V,(p (*) V)) is trivial )

proof end;

registration

existence

not for b_{1} being torsion Z_Module holds b_{1} is trivial ;

end;

cluster non empty non trivial left_complementable right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed V170() torsion for ModuleStr over INT.Ring ;

correctness existence

not for b

proof end;

registration

existence

not for b_{1} being Z_Module holds b_{1} is torsion-free ;

end;

cluster non empty left_complementable right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed V170() non torsion-free for ModuleStr over INT.Ring ;

correctness existence

not for b

proof end;

registration

let V be non torsion-free Z_Module;

correctness

existence

ex b_{1} being Vector of V st

( not b_{1} is zero & b_{1} is torsion );

end;
correctness

existence

ex b

( not b

proof end;

registration

existence

not for b_{1} being finitely-generated Z_Module holds b_{1} is trivial ;

end;

cluster non empty non trivial left_complementable right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed V170() finitely-generated for ModuleStr over INT.Ring ;

correctness existence

not for b

proof end;

registration

coherence

for b_{1} being non torsion-free Z_Module holds not b_{1} is trivial ;

end;

cluster non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed non torsion-free -> non trivial non torsion-free for ModuleStr over INT.Ring ;

correctness coherence

for b

proof end;

registration

existence

not for b_{1} being finitely-generated torsion-free Z_Module holds b_{1} is trivial ;

end;

cluster non empty non trivial left_complementable right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed V170() Mult-cancelable free finite-rank finitely-generated torsion-free for ModuleStr over INT.Ring ;

correctness existence

not for b

proof end;

registration

let V be non trivial finitely-generated torsion-free Z_Module;

let p be prime Element of INT.Ring;

coherence

not VectQuot (V,(p (*) V)) is trivial

end;
let p be prime Element of INT.Ring;

coherence

not VectQuot (V,(p (*) V)) is trivial

proof end;

registration

existence

ex b_{1} being torsion Z_Module st b_{1} is finitely-generated ;

end;

cluster non empty left_complementable right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed V170() finitely-generated torsion for ModuleStr over INT.Ring ;

correctness existence

ex b

proof end;

registration

existence

not for b_{1} being finitely-generated torsion Z_Module holds b_{1} is trivial ;

end;

cluster non empty non trivial left_complementable right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed V170() finitely-generated torsion for ModuleStr over INT.Ring ;

correctness existence

not for b

proof end;

registration

let V be non trivial finitely-generated torsion-free Z_Module;

let p be prime Element of INT.Ring;

correctness

coherence

( VectQuot (V,(p (*) V)) is finitely-generated & VectQuot (V,(p (*) V)) is torsion );

;

end;
let p be prime Element of INT.Ring;

correctness

coherence

( VectQuot (V,(p (*) V)) is finitely-generated & VectQuot (V,(p (*) V)) is torsion );

;

registration

let V be non torsion Z_Module;

correctness

coherence

not VectQuot (V,(torsion_part V)) is trivial ;

end;
correctness

coherence

not VectQuot (V,(torsion_part V)) is trivial ;

proof end;