:: by Yuichi Futa , Hiroyuki Okazaki and Yasunari Shidama

::

:: Received December 31, 2013

:: Copyright (c) 2013-2016 Association of Mizar Users

Lem1: for i being Integer holds i in the carrier of INT.Ring

proof end;

theorem :: ZMODUL04:1

for V being Z_Module

for W1, W2 being Submodule of V

for WW1, WW2 being Submodule of W1 + W2 st WW1 = W1 & WW2 = W2 holds

W1 + W2 = WW1 + WW2

for W1, W2 being Submodule of V

for WW1, WW2 being Submodule of W1 + W2 st WW1 = W1 & WW2 = W2 holds

W1 + W2 = WW1 + WW2

proof end;

theorem :: ZMODUL04:2

for V being Z_Module

for W1, W2 being Submodule of V

for WW1, WW2 being Submodule of W1 + W2 st WW1 = W1 & WW2 = W2 holds

W1 /\ W2 = WW1 /\ WW2

for W1, W2 being Submodule of V

for WW1, WW2 being Submodule of W1 + W2 st WW1 = W1 & WW2 = W2 holds

W1 /\ W2 = WW1 /\ WW2

proof end;

Lm19: for A, B being set st ( for z being object st z in A holds

ex x, y being object st z = [x,y] ) & ( for z being object st z in B holds

ex x, y being object st z = [x,y] ) & ( for x, y being object holds

( [x,y] in A iff [x,y] in B ) ) holds

A = B

proof end;

registration
end;

definition

let V be Z_Module;

assume AS: V is Mult-cancelable ;

ex b_{1} being Equivalence_Relation of [: the carrier of V,(INT \ {0}):] st

for S, T being object holds

( [S,T] in b_{1} iff ( S in [: the carrier of V,(INT \ {0}):] & T in [: the carrier of V,(INT \ {0}):] & ex z1, z2 being Element of V ex i1, i2 being Element of INT.Ring st

( S = [z1,i1] & T = [z2,i2] & i1 <> 0 & i2 <> 0 & i2 * z1 = i1 * z2 ) ) )

for b_{1}, b_{2} being Equivalence_Relation of [: the carrier of V,(INT \ {0}):] st ( for S, T being object holds

( [S,T] in b_{1} iff ( S in [: the carrier of V,(INT \ {0}):] & T in [: the carrier of V,(INT \ {0}):] & ex z1, z2 being Element of V ex i1, i2 being Element of INT.Ring st

( S = [z1,i1] & T = [z2,i2] & i1 <> 0 & i2 <> 0 & i2 * z1 = i1 * z2 ) ) ) ) & ( for S, T being object holds

( [S,T] in b_{2} iff ( S in [: the carrier of V,(INT \ {0}):] & T in [: the carrier of V,(INT \ {0}):] & ex z1, z2 being Element of V ex i1, i2 being Element of INT.Ring st

( S = [z1,i1] & T = [z2,i2] & i1 <> 0 & i2 <> 0 & i2 * z1 = i1 * z2 ) ) ) ) holds

b_{1} = b_{2}

end;
assume AS: V is Mult-cancelable ;

func EQRZM V -> Equivalence_Relation of [: the carrier of V,(INT \ {0}):] means :defEQRZM: :: ZMODUL04:def 1

for S, T being object holds

( [S,T] in it iff ( S in [: the carrier of V,(INT \ {0}):] & T in [: the carrier of V,(INT \ {0}):] & ex z1, z2 being Element of V ex i1, i2 being Element of INT.Ring st

( S = [z1,i1] & T = [z2,i2] & i1 <> 0 & i2 <> 0 & i2 * z1 = i1 * z2 ) ) );

existence for S, T being object holds

( [S,T] in it iff ( S in [: the carrier of V,(INT \ {0}):] & T in [: the carrier of V,(INT \ {0}):] & ex z1, z2 being Element of V ex i1, i2 being Element of INT.Ring st

( S = [z1,i1] & T = [z2,i2] & i1 <> 0 & i2 <> 0 & i2 * z1 = i1 * z2 ) ) );

ex b

for S, T being object holds

( [S,T] in b

( S = [z1,i1] & T = [z2,i2] & i1 <> 0 & i2 <> 0 & i2 * z1 = i1 * z2 ) ) )

proof end;

uniqueness for b

( [S,T] in b

( S = [z1,i1] & T = [z2,i2] & i1 <> 0 & i2 <> 0 & i2 * z1 = i1 * z2 ) ) ) ) & ( for S, T being object holds

( [S,T] in b

( S = [z1,i1] & T = [z2,i2] & i1 <> 0 & i2 <> 0 & i2 * z1 = i1 * z2 ) ) ) ) holds

b

proof end;

:: deftheorem defEQRZM defines EQRZM ZMODUL04:def 1 :

for V being Z_Module st V is Mult-cancelable holds

for b_{2} being Equivalence_Relation of [: the carrier of V,(INT \ {0}):] holds

( b_{2} = EQRZM V iff for S, T being object holds

( [S,T] in b_{2} iff ( S in [: the carrier of V,(INT \ {0}):] & T in [: the carrier of V,(INT \ {0}):] & ex z1, z2 being Element of V ex i1, i2 being Element of INT.Ring st

( S = [z1,i1] & T = [z2,i2] & i1 <> 0 & i2 <> 0 & i2 * z1 = i1 * z2 ) ) ) );

for V being Z_Module st V is Mult-cancelable holds

for b

( b

( [S,T] in b

( S = [z1,i1] & T = [z2,i2] & i1 <> 0 & i2 <> 0 & i2 * z1 = i1 * z2 ) ) ) );

theorem LMEQR001: :: ZMODUL04:3

for V being Z_Module

for z1, z2 being Element of V

for i1, i2 being Element of INT.Ring st V is Mult-cancelable holds

( [[z1,i1],[z2,i2]] in EQRZM V iff ( i1 <> 0 & i2 <> 0 & i2 * z1 = i1 * z2 ) )

for z1, z2 being Element of V

for i1, i2 being Element of INT.Ring st V is Mult-cancelable holds

( [[z1,i1],[z2,i2]] in EQRZM V iff ( i1 <> 0 & i2 <> 0 & i2 * z1 = i1 * z2 ) )

proof end;

definition

let V be Z_Module;

assume AS: V is Mult-cancelable ;

ex b_{1} being BinOp of (Class (EQRZM V)) st

for A, B being object st A in Class (EQRZM V) & B in Class (EQRZM V) holds

for z1, z2 being Element of V

for i1, i2 being Element of INT.Ring st i1 <> 0. INT.Ring & i2 <> 0. INT.Ring & A = Class ((EQRZM V),[z1,i1]) & B = Class ((EQRZM V),[z2,i2]) holds

b_{1} . (A,B) = Class ((EQRZM V),[((i2 * z1) + (i1 * z2)),(i1 * i2)])

for b_{1}, b_{2} being BinOp of (Class (EQRZM V)) st ( for A, B being object st A in Class (EQRZM V) & B in Class (EQRZM V) holds

for z1, z2 being Element of V

for i1, i2 being Element of INT.Ring st i1 <> 0. INT.Ring & i2 <> 0. INT.Ring & A = Class ((EQRZM V),[z1,i1]) & B = Class ((EQRZM V),[z2,i2]) holds

b_{1} . (A,B) = Class ((EQRZM V),[((i2 * z1) + (i1 * z2)),(i1 * i2)]) ) & ( for A, B being object st A in Class (EQRZM V) & B in Class (EQRZM V) holds

for z1, z2 being Element of V

for i1, i2 being Element of INT.Ring st i1 <> 0. INT.Ring & i2 <> 0. INT.Ring & A = Class ((EQRZM V),[z1,i1]) & B = Class ((EQRZM V),[z2,i2]) holds

b_{2} . (A,B) = Class ((EQRZM V),[((i2 * z1) + (i1 * z2)),(i1 * i2)]) ) holds

b_{1} = b_{2}

end;
assume AS: V is Mult-cancelable ;

func addCoset V -> BinOp of (Class (EQRZM V)) means :DefaddCoset: :: ZMODUL04:def 2

for A, B being object st A in Class (EQRZM V) & B in Class (EQRZM V) holds

for z1, z2 being Element of V

for i1, i2 being Element of INT.Ring st i1 <> 0. INT.Ring & i2 <> 0. INT.Ring & A = Class ((EQRZM V),[z1,i1]) & B = Class ((EQRZM V),[z2,i2]) holds

it . (A,B) = Class ((EQRZM V),[((i2 * z1) + (i1 * z2)),(i1 * i2)]);

existence for A, B being object st A in Class (EQRZM V) & B in Class (EQRZM V) holds

for z1, z2 being Element of V

for i1, i2 being Element of INT.Ring st i1 <> 0. INT.Ring & i2 <> 0. INT.Ring & A = Class ((EQRZM V),[z1,i1]) & B = Class ((EQRZM V),[z2,i2]) holds

it . (A,B) = Class ((EQRZM V),[((i2 * z1) + (i1 * z2)),(i1 * i2)]);

ex b

for A, B being object st A in Class (EQRZM V) & B in Class (EQRZM V) holds

for z1, z2 being Element of V

for i1, i2 being Element of INT.Ring st i1 <> 0. INT.Ring & i2 <> 0. INT.Ring & A = Class ((EQRZM V),[z1,i1]) & B = Class ((EQRZM V),[z2,i2]) holds

b

proof end;

uniqueness for b

for z1, z2 being Element of V

for i1, i2 being Element of INT.Ring st i1 <> 0. INT.Ring & i2 <> 0. INT.Ring & A = Class ((EQRZM V),[z1,i1]) & B = Class ((EQRZM V),[z2,i2]) holds

b

for z1, z2 being Element of V

for i1, i2 being Element of INT.Ring st i1 <> 0. INT.Ring & i2 <> 0. INT.Ring & A = Class ((EQRZM V),[z1,i1]) & B = Class ((EQRZM V),[z2,i2]) holds

b

b

proof end;

:: deftheorem DefaddCoset defines addCoset ZMODUL04:def 2 :

for V being Z_Module st V is Mult-cancelable holds

for b_{2} being BinOp of (Class (EQRZM V)) holds

( b_{2} = addCoset V iff for A, B being object st A in Class (EQRZM V) & B in Class (EQRZM V) holds

for z1, z2 being Element of V

for i1, i2 being Element of INT.Ring st i1 <> 0. INT.Ring & i2 <> 0. INT.Ring & A = Class ((EQRZM V),[z1,i1]) & B = Class ((EQRZM V),[z2,i2]) holds

b_{2} . (A,B) = Class ((EQRZM V),[((i2 * z1) + (i1 * z2)),(i1 * i2)]) );

for V being Z_Module st V is Mult-cancelable holds

for b

( b

for z1, z2 being Element of V

for i1, i2 being Element of INT.Ring st i1 <> 0. INT.Ring & i2 <> 0. INT.Ring & A = Class ((EQRZM V),[z1,i1]) & B = Class ((EQRZM V),[z2,i2]) holds

b

definition

let V be Z_Module;

assume AS: V is Mult-cancelable ;

ex b_{1} being Element of Class (EQRZM V) st

for i being Integer st i <> 0 holds

b_{1} = Class ((EQRZM V),[(0. V),i])

for b_{1}, b_{2} being Element of Class (EQRZM V) st ( for i being Integer st i <> 0 holds

b_{1} = Class ((EQRZM V),[(0. V),i]) ) & ( for i being Integer st i <> 0 holds

b_{2} = Class ((EQRZM V),[(0. V),i]) ) holds

b_{1} = b_{2}

end;
assume AS: V is Mult-cancelable ;

func zeroCoset V -> Element of Class (EQRZM V) means :defZero: :: ZMODUL04:def 3

for i being Integer st i <> 0 holds

it = Class ((EQRZM V),[(0. V),i]);

existence for i being Integer st i <> 0 holds

it = Class ((EQRZM V),[(0. V),i]);

ex b

for i being Integer st i <> 0 holds

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem defZero defines zeroCoset ZMODUL04:def 3 :

for V being Z_Module st V is Mult-cancelable holds

for b_{2} being Element of Class (EQRZM V) holds

( b_{2} = zeroCoset V iff for i being Integer st i <> 0 holds

b_{2} = Class ((EQRZM V),[(0. V),i]) );

for V being Z_Module st V is Mult-cancelable holds

for b

( b

b

definition

let V be Z_Module;

assume AS: V is Mult-cancelable ;

ex b_{1} being Function of [: the carrier of F_Rat,(Class (EQRZM V)):],(Class (EQRZM V)) st

for q, A being object st q in RAT & A in Class (EQRZM V) holds

for m, n, i being Integer

for mm being Element of INT.Ring

for z being Element of V st m = mm & n <> 0 & q = m / n & i <> 0 & A = Class ((EQRZM V),[z,i]) holds

b_{1} . (q,A) = Class ((EQRZM V),[(mm * z),(n * i)])

for b_{1}, b_{2} being Function of [: the carrier of F_Rat,(Class (EQRZM V)):],(Class (EQRZM V)) st ( for q, A being object st q in RAT & A in Class (EQRZM V) holds

for m, n, i being Integer

for mm being Element of INT.Ring

for z being Element of V st m = mm & n <> 0 & q = m / n & i <> 0 & A = Class ((EQRZM V),[z,i]) holds

b_{1} . (q,A) = Class ((EQRZM V),[(mm * z),(n * i)]) ) & ( for q, A being object st q in RAT & A in Class (EQRZM V) holds

for m, n, i being Integer

for mm being Element of INT.Ring

for z being Element of V st m = mm & n <> 0 & q = m / n & i <> 0 & A = Class ((EQRZM V),[z,i]) holds

b_{2} . (q,A) = Class ((EQRZM V),[(mm * z),(n * i)]) ) holds

b_{1} = b_{2}

end;
assume AS: V is Mult-cancelable ;

func lmultCoset V -> Function of [: the carrier of F_Rat,(Class (EQRZM V)):],(Class (EQRZM V)) means :DeflmultCoset: :: ZMODUL04:def 4

for q, A being object st q in RAT & A in Class (EQRZM V) holds

for m, n, i being Integer

for mm being Element of INT.Ring

for z being Element of V st m = mm & n <> 0 & q = m / n & i <> 0 & A = Class ((EQRZM V),[z,i]) holds

it . (q,A) = Class ((EQRZM V),[(mm * z),(n * i)]);

existence for q, A being object st q in RAT & A in Class (EQRZM V) holds

for m, n, i being Integer

for mm being Element of INT.Ring

for z being Element of V st m = mm & n <> 0 & q = m / n & i <> 0 & A = Class ((EQRZM V),[z,i]) holds

it . (q,A) = Class ((EQRZM V),[(mm * z),(n * i)]);

ex b

for q, A being object st q in RAT & A in Class (EQRZM V) holds

for m, n, i being Integer

for mm being Element of INT.Ring

for z being Element of V st m = mm & n <> 0 & q = m / n & i <> 0 & A = Class ((EQRZM V),[z,i]) holds

b

proof end;

uniqueness for b

for m, n, i being Integer

for mm being Element of INT.Ring

for z being Element of V st m = mm & n <> 0 & q = m / n & i <> 0 & A = Class ((EQRZM V),[z,i]) holds

b

for m, n, i being Integer

for mm being Element of INT.Ring

for z being Element of V st m = mm & n <> 0 & q = m / n & i <> 0 & A = Class ((EQRZM V),[z,i]) holds

b

b

proof end;

:: deftheorem DeflmultCoset defines lmultCoset ZMODUL04:def 4 :

for V being Z_Module st V is Mult-cancelable holds

for b_{2} being Function of [: the carrier of F_Rat,(Class (EQRZM V)):],(Class (EQRZM V)) holds

( b_{2} = lmultCoset V iff for q, A being object st q in RAT & A in Class (EQRZM V) holds

for m, n, i being Integer

for mm being Element of INT.Ring

for z being Element of V st m = mm & n <> 0 & q = m / n & i <> 0 & A = Class ((EQRZM V),[z,i]) holds

b_{2} . (q,A) = Class ((EQRZM V),[(mm * z),(n * i)]) );

for V being Z_Module st V is Mult-cancelable holds

for b

( b

for m, n, i being Integer

for mm being Element of INT.Ring

for z being Element of V st m = mm & n <> 0 & q = m / n & i <> 0 & A = Class ((EQRZM V),[z,i]) holds

b

theorem LMEQR003: :: ZMODUL04:4

for V being Z_Module

for z being Element of V

for i, n being Element of INT.Ring st i <> 0. INT.Ring & n <> 0. INT.Ring & V is Mult-cancelable holds

Class ((EQRZM V),[z,i]) = Class ((EQRZM V),[(n * z),(n * i)])

for z being Element of V

for i, n being Element of INT.Ring st i <> 0. INT.Ring & n <> 0. INT.Ring & V is Mult-cancelable holds

Class ((EQRZM V),[z,i]) = Class ((EQRZM V),[(n * z),(n * i)])

proof end;

theorem LMEQRZM1: :: ZMODUL04:5

for V being Z_Module

for v being Element of ModuleStr(# (Class (EQRZM V)),(addCoset V),(zeroCoset V),(lmultCoset V) #) st V is Mult-cancelable holds

ex i being Element of INT.Ring ex z being Element of V st

( i <> 0. INT.Ring & v = Class ((EQRZM V),[z,i]) )

for v being Element of ModuleStr(# (Class (EQRZM V)),(addCoset V),(zeroCoset V),(lmultCoset V) #) st V is Mult-cancelable holds

ex i being Element of INT.Ring ex z being Element of V st

( i <> 0. INT.Ring & v = Class ((EQRZM V),[z,i]) )

proof end;

ThEQRZMV1: for V being Z_Module st V is Mult-cancelable holds

ModuleStr(# (Class (EQRZM V)),(addCoset V),(zeroCoset V),(lmultCoset V) #) is VectSp of F_Rat

proof end;

definition

let V be Z_Module;

assume AS: V is Mult-cancelable ;

coherence

ModuleStr(# (Class (EQRZM V)),(addCoset V),(zeroCoset V),(lmultCoset V) #) is VectSp of F_Rat ;

by ThEQRZMV1, AS;

end;
assume AS: V is Mult-cancelable ;

func Z_MQ_VectSp V -> VectSp of F_Rat equals :defZMQVSp: :: ZMODUL04:def 5

ModuleStr(# (Class (EQRZM V)),(addCoset V),(zeroCoset V),(lmultCoset V) #);

correctness ModuleStr(# (Class (EQRZM V)),(addCoset V),(zeroCoset V),(lmultCoset V) #);

coherence

ModuleStr(# (Class (EQRZM V)),(addCoset V),(zeroCoset V),(lmultCoset V) #) is VectSp of F_Rat ;

by ThEQRZMV1, AS;

:: deftheorem defZMQVSp defines Z_MQ_VectSp ZMODUL04:def 5 :

for V being Z_Module st V is Mult-cancelable holds

Z_MQ_VectSp V = ModuleStr(# (Class (EQRZM V)),(addCoset V),(zeroCoset V),(lmultCoset V) #);

for V being Z_Module st V is Mult-cancelable holds

Z_MQ_VectSp V = ModuleStr(# (Class (EQRZM V)),(addCoset V),(zeroCoset V),(lmultCoset V) #);

ThEQRZMV2: for V being Z_Module st V is Mult-cancelable holds

ex I being Function of V,(Z_MQ_VectSp V) st

( I is one-to-one & ( for v being Element of V holds I . v = Class ((EQRZM V),[v,1]) ) & ( for v, w being Element of V holds I . (v + w) = (I . v) + (I . w) ) & ( for v being Element of V

for i being Element of INT.Ring

for q being Element of F_Rat st i = q holds

I . (i * v) = q * (I . v) ) & I . (0. V) = 0. (Z_MQ_VectSp V) )

proof end;

definition

let V be Z_Module;

assume AS: V is Mult-cancelable ;

ex b_{1} being Function of V,(Z_MQ_VectSp V) st

( b_{1} is one-to-one & ( for v being Element of V holds b_{1} . v = Class ((EQRZM V),[v,1]) ) & ( for v, w being Element of V holds b_{1} . (v + w) = (b_{1} . v) + (b_{1} . w) ) & ( for v being Element of V

for i being Element of INT.Ring

for q being Element of F_Rat st i = q holds

b_{1} . (i * v) = q * (b_{1} . v) ) & b_{1} . (0. V) = 0. (Z_MQ_VectSp V) )
by ThEQRZMV2, AS;

uniqueness

for b_{1}, b_{2} being Function of V,(Z_MQ_VectSp V) st b_{1} is one-to-one & ( for v being Element of V holds b_{1} . v = Class ((EQRZM V),[v,1]) ) & ( for v, w being Element of V holds b_{1} . (v + w) = (b_{1} . v) + (b_{1} . w) ) & ( for v being Element of V

for i being Element of INT.Ring

for q being Element of F_Rat st i = q holds

b_{1} . (i * v) = q * (b_{1} . v) ) & b_{1} . (0. V) = 0. (Z_MQ_VectSp V) & b_{2} is one-to-one & ( for v being Element of V holds b_{2} . v = Class ((EQRZM V),[v,1]) ) & ( for v, w being Element of V holds b_{2} . (v + w) = (b_{2} . v) + (b_{2} . w) ) & ( for v being Element of V

for i being Element of INT.Ring

for q being Element of F_Rat st i = q holds

b_{2} . (i * v) = q * (b_{2} . v) ) & b_{2} . (0. V) = 0. (Z_MQ_VectSp V) holds

b_{1} = b_{2}

end;
assume AS: V is Mult-cancelable ;

func MorphsZQ V -> Function of V,(Z_MQ_VectSp V) means :defMorph: :: ZMODUL04:def 6

( it is one-to-one & ( for v being Element of V holds it . v = Class ((EQRZM V),[v,1]) ) & ( for v, w being Element of V holds it . (v + w) = (it . v) + (it . w) ) & ( for v being Element of V

for i being Element of INT.Ring

for q being Element of F_Rat st i = q holds

it . (i * v) = q * (it . v) ) & it . (0. V) = 0. (Z_MQ_VectSp V) );

existence ( it is one-to-one & ( for v being Element of V holds it . v = Class ((EQRZM V),[v,1]) ) & ( for v, w being Element of V holds it . (v + w) = (it . v) + (it . w) ) & ( for v being Element of V

for i being Element of INT.Ring

for q being Element of F_Rat st i = q holds

it . (i * v) = q * (it . v) ) & it . (0. V) = 0. (Z_MQ_VectSp V) );

ex b

( b

for i being Element of INT.Ring

for q being Element of F_Rat st i = q holds

b

uniqueness

for b

for i being Element of INT.Ring

for q being Element of F_Rat st i = q holds

b

for i being Element of INT.Ring

for q being Element of F_Rat st i = q holds

b

b

proof end;

:: deftheorem defMorph defines MorphsZQ ZMODUL04:def 6 :

for V being Z_Module st V is Mult-cancelable holds

for b_{2} being Function of V,(Z_MQ_VectSp V) holds

( b_{2} = MorphsZQ V iff ( b_{2} is one-to-one & ( for v being Element of V holds b_{2} . v = Class ((EQRZM V),[v,1]) ) & ( for v, w being Element of V holds b_{2} . (v + w) = (b_{2} . v) + (b_{2} . w) ) & ( for v being Element of V

for i being Element of INT.Ring

for q being Element of F_Rat st i = q holds

b_{2} . (i * v) = q * (b_{2} . v) ) & b_{2} . (0. V) = 0. (Z_MQ_VectSp V) ) );

for V being Z_Module st V is Mult-cancelable holds

for b

( b

for i being Element of INT.Ring

for q being Element of F_Rat st i = q holds

b

theorem XThSum: :: ZMODUL04:6

for V being Z_Module st V is Mult-cancelable holds

for s being FinSequence of V

for t being FinSequence of (Z_MQ_VectSp V) 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 = (MorphsZQ V) . si ) ) holds

Sum t = (MorphsZQ V) . (Sum s)

for s being FinSequence of V

for t being FinSequence of (Z_MQ_VectSp V) 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 = (MorphsZQ V) . si ) ) holds

Sum t = (MorphsZQ V) . (Sum s)

proof end;

theorem XThSum1: :: ZMODUL04:7

for V being Z_Module

for I being Subset of V

for IQ being Subset of (Z_MQ_VectSp V)

for l being Linear_Combination of I

for lq being Linear_Combination of IQ st V is Mult-cancelable & IQ = (MorphsZQ V) .: I & l = lq * (MorphsZQ V) holds

Sum lq = (MorphsZQ V) . (Sum l)

for I being Subset of V

for IQ being Subset of (Z_MQ_VectSp V)

for l being Linear_Combination of I

for lq being Linear_Combination of IQ st V is Mult-cancelable & IQ = (MorphsZQ V) .: I & l = lq * (MorphsZQ V) holds

Sum lq = (MorphsZQ V) . (Sum l)

proof end;

theorem ThEQRZMV3A: :: ZMODUL04:8

for V being Z_Module

for IQ being Subset of (Z_MQ_VectSp V)

for lq being Linear_Combination of IQ ex m being Integer ex a being Element of F_Rat st

( m <> 0 & m = a & rng (a * lq) c= INT )

for IQ being Subset of (Z_MQ_VectSp V)

for lq being Linear_Combination of IQ ex m being Integer ex a being Element of F_Rat st

( m <> 0 & m = a & rng (a * lq) c= INT )

proof end;

theorem ThEQRZMV3: :: ZMODUL04:9

for V being Z_Module

for I being Subset of V

for IQ being Subset of (Z_MQ_VectSp V)

for lq being Linear_Combination of IQ st V is Mult-cancelable & IQ = (MorphsZQ V) .: I holds

ex m being Element of INT.Ring ex a being Element of F_Rat ex l being Linear_Combination of I st

( m <> 0. INT.Ring & m = a & l = (a * lq) * (MorphsZQ V) & (MorphsZQ V) " (Carrier lq) = Carrier l )

for I being Subset of V

for IQ being Subset of (Z_MQ_VectSp V)

for lq being Linear_Combination of IQ st V is Mult-cancelable & IQ = (MorphsZQ V) .: I holds

ex m being Element of INT.Ring ex a being Element of F_Rat ex l being Linear_Combination of I st

( m <> 0. INT.Ring & m = a & l = (a * lq) * (MorphsZQ V) & (MorphsZQ V) " (Carrier lq) = Carrier l )

proof end;

theorem ThEQRZMV3B: :: ZMODUL04:10

for V being Z_Module

for I being Subset of V

for IQ being Subset of (Z_MQ_VectSp V)

for lq being Linear_Combination of IQ

for m being Integer

for a being Element of F_Rat

for l being Linear_Combination of I st V is Mult-cancelable & IQ = (MorphsZQ V) .: I & m <> 0 & m = a & l = (a * lq) * (MorphsZQ V) holds

a * (Sum lq) = (MorphsZQ V) . (Sum l)

for I being Subset of V

for IQ being Subset of (Z_MQ_VectSp V)

for lq being Linear_Combination of IQ

for m being Integer

for a being Element of F_Rat

for l being Linear_Combination of I st V is Mult-cancelable & IQ = (MorphsZQ V) .: I & m <> 0 & m = a & l = (a * lq) * (MorphsZQ V) holds

a * (Sum lq) = (MorphsZQ V) . (Sum l)

proof end;

theorem ThEQRZMV3C: :: ZMODUL04:11

for V being Z_Module

for I being Subset of V

for IQ being Subset of (Z_MQ_VectSp V) st V is Mult-cancelable & IQ = (MorphsZQ V) .: I & I is linearly-independent holds

IQ is linearly-independent

for I being Subset of V

for IQ being Subset of (Z_MQ_VectSp V) st V is Mult-cancelable & IQ = (MorphsZQ V) .: I & I is linearly-independent holds

IQ is linearly-independent

proof end;

theorem ThEQRZMV4: :: ZMODUL04:12

for V being Z_Module

for I being Subset of V

for l being Linear_Combination of I

for IQ being Subset of (Z_MQ_VectSp V) st V is Mult-cancelable & IQ = (MorphsZQ V) .: I holds

ex lq being Linear_Combination of IQ st

( l = lq * (MorphsZQ V) & Carrier lq = (MorphsZQ V) .: (Carrier l) )

for I being Subset of V

for l being Linear_Combination of I

for IQ being Subset of (Z_MQ_VectSp V) st V is Mult-cancelable & IQ = (MorphsZQ V) .: I holds

ex lq being Linear_Combination of IQ st

( l = lq * (MorphsZQ V) & Carrier lq = (MorphsZQ V) .: (Carrier l) )

proof end;

theorem ThQuotAX: :: ZMODUL04:13

for V being free Z_Module

for I being Subset of V

for IQ being Subset of (Z_MQ_VectSp V)

for l being Linear_Combination of I

for i being Element of INT.Ring st i <> 0. INT.Ring & IQ = (MorphsZQ V) .: I holds

Class ((EQRZM V),[(Sum l),i]) in Lin IQ

for I being Subset of V

for IQ being Subset of (Z_MQ_VectSp V)

for l being Linear_Combination of I

for i being Element of INT.Ring st i <> 0. INT.Ring & IQ = (MorphsZQ V) .: I holds

Class ((EQRZM V),[(Sum l),i]) in Lin IQ

proof end;

theorem ThEQRZMV3E: :: ZMODUL04:14

for V being free Z_Module

for I being Subset of V

for IQ being Subset of (Z_MQ_VectSp V) st IQ = (MorphsZQ V) .: I holds

card I = card IQ

for I being Subset of V

for IQ being Subset of (Z_MQ_VectSp V) st IQ = (MorphsZQ V) .: I holds

card I = card IQ

proof end;

theorem ThEQRZMV3D: :: ZMODUL04:15

for V being free Z_Module

for I being Subset of V

for IQ being Subset of (Z_MQ_VectSp V) st IQ = (MorphsZQ V) .: I & I is Basis of V holds

IQ is Basis of (Z_MQ_VectSp V)

for I being Subset of V

for IQ being Subset of (Z_MQ_VectSp V) st IQ = (MorphsZQ V) .: I & I is Basis of V holds

IQ is Basis of (Z_MQ_VectSp V)

proof end;

registration
end;

theorem XXTh1: :: ZMODUL04:17

for V being free Z_Module

for I, A being finite Subset of V st I is Basis of V & (card I) + 1 = card A holds

A is linearly-dependent

for I, A being finite Subset of V st I is Basis of V & (card I) + 1 = card A holds

A is linearly-dependent

proof end;

theorem XXTh2: :: ZMODUL04:18

for V being free Z_Module

for A, B being Subset of V st A is linearly-dependent & A c= B holds

B is linearly-dependent by VECTSP_7:1;

for A, B being Subset of V st A is linearly-dependent & A c= B holds

B is linearly-dependent by VECTSP_7:1;

theorem XXTh3: :: ZMODUL04:19

for V being free Z_Module

for D, A being Subset of V st D is Basis of V & D is finite & card D c< card A holds

A is linearly-dependent

for D, A being Subset of V st D is Basis of V & D is finite & card D c< card A holds

A is linearly-dependent

proof end;

theorem :: ZMODUL04:20

theorem :: ZMODUL04:22

for V being Z_Module

for W1, W2 being Submodule of V

for W1s, W2s being strict Submodule of V st W1s = (Omega). W1 & W2s = (Omega). W2 holds

W1s + W2s = W1 + W2

for W1, W2 being Submodule of V

for W1s, W2s being strict Submodule of V st W1s = (Omega). W1 & W2s = (Omega). W2 holds

W1s + W2s = W1 + W2

proof end;

theorem :: ZMODUL04:23

for V being Z_Module

for W1, W2 being Submodule of V

for W1s, W2s being strict Submodule of V st W1s = (Omega). W1 & W2s = (Omega). W2 holds

W1s /\ W2s = W1 /\ W2

for W1, W2 being Submodule of V

for W1s, W2s being strict Submodule of V st W1s = (Omega). W1 & W2s = (Omega). W2 holds

W1s /\ W2s = W1 /\ W2

proof end;

theorem Thn0V: :: ZMODUL04:24

for V being Z_Module

for W being strict Submodule of V st W <> (0). V holds

ex v being Vector of V st

( v in W & v <> 0. V )

for W being strict Submodule of V st W <> (0). V holds

ex v being Vector of V st

( v in W & v <> 0. V )

proof end;

theorem ThCarrier1: :: ZMODUL04:25

for V being Z_Module

for A being Subset of V

for l1, l2 being Linear_Combination of A st (Carrier l1) /\ (Carrier l2) = {} holds

Carrier (l1 + l2) = (Carrier l1) \/ (Carrier l2)

for A being Subset of V

for l1, l2 being Linear_Combination of A st (Carrier l1) /\ (Carrier l2) = {} holds

Carrier (l1 + l2) = (Carrier l1) \/ (Carrier l2)

proof end;

theorem ThCarrier2: :: ZMODUL04:26

for V being Z_Module

for A1, A2 being Subset of V

for l being Linear_Combination of A1 \/ A2 st A1 /\ A2 = {} holds

ex l1 being Linear_Combination of A1 ex l2 being Linear_Combination of A2 st l = l1 + l2

for A1, A2 being Subset of V

for l being Linear_Combination of A1 \/ A2 st A1 /\ A2 = {} holds

ex l1 being Linear_Combination of A1 ex l2 being Linear_Combination of A2 st l = l1 + l2

proof end;

theorem FRds1: :: ZMODUL04:27

for V being Z_Module

for W1, W2 being free Submodule of V

for I1 being Basis of W1

for I2 being Basis of W2 st V is_the_direct_sum_of W1,W2 holds

I1 /\ I2 = {}

for W1, W2 being free Submodule of V

for I1 being Basis of W1

for I2 being Basis of W2 st V is_the_direct_sum_of W1,W2 holds

I1 /\ I2 = {}

proof end;

theorem FRds2: :: ZMODUL04:28

for V being Z_Module

for W1, W2 being free Submodule of V

for I1 being Basis of W1

for I2 being Basis of W2

for I being Subset of V st V is_the_direct_sum_of W1,W2 & I = I1 \/ I2 holds

Lin I = ModuleStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #)

for W1, W2 being free Submodule of V

for I1 being Basis of W1

for I2 being Basis of W2

for I being Subset of V st V is_the_direct_sum_of W1,W2 & I = I1 \/ I2 holds

Lin I = ModuleStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #)

proof end;

theorem FRds3: :: ZMODUL04:29

for V being Z_Module

for W1, W2 being free Submodule of V

for I1 being Basis of W1

for I2 being Basis of W2

for I being Subset of V st V is_the_direct_sum_of W1,W2 & I = I1 \/ I2 holds

I is linearly-independent

for W1, W2 being free Submodule of V

for I1 being Basis of W1

for I2 being Basis of W2

for I being Subset of V st V is_the_direct_sum_of W1,W2 & I = I1 \/ I2 holds

I is linearly-independent

proof end;

theorem FRdsX: :: ZMODUL04:30

for V being Z_Module

for W1, W2 being free Submodule of V st V is_the_direct_sum_of W1,W2 holds

V is free

for W1, W2 being free Submodule of V st V is_the_direct_sum_of W1,W2 holds

V is free

proof end;

theorem ThDirectSum: :: ZMODUL04:31

for V being Z_Module

for W1, W2 being free Submodule of V st W1 /\ W2 = (0). V holds

W1 + W2 is free

for W1, W2 being free Submodule of V st W1 /\ W2 = (0). V holds

W1 + W2 is free

proof end;

theorem :: ZMODUL04:32

for V being free Z_Module

for I being Basis of V

for v being Vector of V st v in I holds

( Lin (I \ {v}) is free & Lin {v} is free )

for I being Basis of V

for v being Vector of V st v in I holds

( Lin (I \ {v}) is free & Lin {v} is free )

proof end;

theorem FRdsY: :: ZMODUL04:33

for V being free Z_Module

for I being Basis of V

for v being Vector of V st v in I holds

V is_the_direct_sum_of Lin (I \ {v}), Lin {v}

for I being Basis of V

for v being Vector of V st v in I holds

V is_the_direct_sum_of Lin (I \ {v}), Lin {v}

proof end;

FRX: for V being free finite-rank Z_Module

for W being Submodule of V holds W is free

proof end;

registration

let V be free finite-rank Z_Module;

correctness

coherence

for b_{1} being Submodule of V holds b_{1} is free ;

by FRX;

end;
correctness

coherence

for b

by FRX;

theorem :: ZMODUL04:34

for V being Z_Module

for W being Submodule of V

for W1, W2 being free Submodule of V st W1 /\ W2 = (0). V & ModuleStr(# the carrier of W, the addF of W, the ZeroF of W, the lmult of W #) = W1 + W2 holds

W is free

for W being Submodule of V

for W1, W2 being free Submodule of V st W1 /\ W2 = (0). V & ModuleStr(# the carrier of W, the addF of W, the ZeroF of W, the lmult of W #) = W1 + W2 holds

W is free

proof end;

theorem :: ZMODUL04:35

for p being prime Element of INT.Ring

for V being free Z_Module st Z_MQ_VectSp (V,p) is finite-dimensional holds

V is finite-rank

for V being free Z_Module st Z_MQ_VectSp (V,p) is finite-dimensional holds

V is finite-rank

proof end;

theorem :: ZMODUL04:36

for p being prime Element of INT.Ring

for V being Z_Module

for s being Element of V

for a being Element of INT.Ring

for b being Element of (GF p) st b = a mod p holds

b * (ZMtoMQV (V,p,s)) = ZMtoMQV (V,p,(a * s))

for V being Z_Module

for s being Element of V

for a being Element of INT.Ring

for b being Element of (GF p) st b = a mod p holds

b * (ZMtoMQV (V,p,s)) = ZMtoMQV (V,p,(a * s))

proof end;

LMX2: for p being prime Element of INT.Ring

for V being free Z_Module

for i being Element of INT.Ring

for v being Element of V holds ZMtoMQV (V,p,((i mod p) * v)) = ZMtoMQV (V,p,(i * v))

proof end;

theorem ThQuotBasis5A: :: ZMODUL04:37

for p being prime Element of INT.Ring

for V being free Z_Module

for I being Subset of V

for IQ being Subset of (Z_MQ_VectSp (V,p))

for l being Linear_Combination of I st IQ = { (ZMtoMQV (V,p,u)) where u is Vector of V : u in I } holds

ZMtoMQV (V,p,(Sum l)) in Lin IQ

for V being free Z_Module

for I being Subset of V

for IQ being Subset of (Z_MQ_VectSp (V,p))

for l being Linear_Combination of I st IQ = { (ZMtoMQV (V,p,u)) where u is Vector of V : u in I } holds

ZMtoMQV (V,p,(Sum l)) in Lin IQ

proof end;

theorem ThQuotBasis5: :: ZMODUL04:38

for p being prime Element of INT.Ring

for V being free Z_Module

for I being Subset of V

for IQ being Subset of (Z_MQ_VectSp (V,p)) st Lin I = ModuleStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #) & IQ = { (ZMtoMQV (V,p,u)) where u is Vector of V : u in I } holds

Lin IQ = ModuleStr(# the carrier of (Z_MQ_VectSp (V,p)), the addF of (Z_MQ_VectSp (V,p)), the ZeroF of (Z_MQ_VectSp (V,p)), the lmult of (Z_MQ_VectSp (V,p)) #)

for V being free Z_Module

for I being Subset of V

for IQ being Subset of (Z_MQ_VectSp (V,p)) st Lin I = ModuleStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #) & IQ = { (ZMtoMQV (V,p,u)) where u is Vector of V : u in I } holds

Lin IQ = ModuleStr(# the carrier of (Z_MQ_VectSp (V,p)), the addF of (Z_MQ_VectSp (V,p)), the ZeroF of (Z_MQ_VectSp (V,p)), the lmult of (Z_MQ_VectSp (V,p)) #)

proof end;

registration

for b_{1} being free finitely-generated Z_Module holds b_{1} is finite-rank
end;

cluster non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed free finitely-generated -> free finite-rank finitely-generated for ModuleStr over INT.Ring ;

coherence for b

proof end;

registration

for b_{1} being free finite-rank Z_Module holds b_{1} is finitely-generated
end;

cluster non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed free finite-rank -> free finite-rank finitely-generated for ModuleStr over INT.Ring ;

coherence for b

proof end;

theorem RL5Th25: :: ZMODUL04:40

for V being free finite-rank Z_Module

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

A is finite

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

A is finite

proof end;

RL5Th28: for V being free finite-rank Z_Module

for W being Submodule of V holds W is finite-rank

proof end;

registration

let V be Z_Module;

let W1, W2 be free finite-rank Submodule of V;

correctness

coherence

W1 /\ W2 is free ;

end;
let W1, W2 be free finite-rank Submodule of V;

correctness

coherence

W1 /\ W2 is free ;

proof end;

registration

let V be Z_Module;

let W1, W2 be free finite-rank Submodule of V;

correctness

coherence

W1 /\ W2 is finite-rank ;

end;
let W1, W2 be free finite-rank Submodule of V;

correctness

coherence

W1 /\ W2 is finite-rank ;

proof end;

registration

let V be free finite-rank Z_Module;

correctness

coherence

for b_{1} being Submodule of V holds b_{1} is finite-rank ;

by RL5Th28;

end;
correctness

coherence

for b

by RL5Th28;