:: by Yuichi Futa , Hiroyuki Okazaki and Yasunari Shidama

::

:: Received August 6, 2012

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

registration

existence

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

end;

cluster non empty non trivial left_add-cancelable right_add-cancelable right_complementable V156( INT.Ring ) V157( INT.Ring ) V158( INT.Ring ) V159( INT.Ring ) V163() V164() V165() V259() V260() V261() V262() for ModuleStr over INT.Ring ;

correctness existence

not for b

proof end;

registration

let V be Z_Module;

correctness

existence

ex b_{1} being finite Subset of V st b_{1} is linearly-independent ;

end;
correctness

existence

ex b

proof end;

theorem Th1: :: ZMODUL03:1

for V being Z_Module

for u being Vector of V ex l being Linear_Combination of V st

( l . u = 1 & ( for v being Vector of V st v <> u holds

l . v = 0 ) )

for u being Vector of V ex l being Linear_Combination of V st

( l . u = 1 & ( for v being Vector of V st v <> u holds

l . v = 0 ) )

proof end;

Lm1: for r being Element of INT.Ring

for n being Element of NAT

for i being Integer st i = n holds

i * r = n * r

proof end;

theorem Th2: :: ZMODUL03:2

for G being Z_Module

for i being Element of INT.Ring

for w being Element of INT

for v being Element of G st G = ModuleStr(# the carrier of INT.Ring, the addF of INT.Ring, the ZeroF of INT.Ring,(Int-mult-left INT.Ring) #) & v = w holds

i * v = i * w

for i being Element of INT.Ring

for w being Element of INT

for v being Element of G st G = ModuleStr(# the carrier of INT.Ring, the addF of INT.Ring, the ZeroF of INT.Ring,(Int-mult-left INT.Ring) #) & v = w holds

i * v = i * w

proof end;

definition
end;

registration

ex b_{1} being Z_Module st

( b_{1} is strict & b_{1} is free )
end;

cluster non empty left_add-cancelable right_add-cancelable right_complementable strict V156( INT.Ring ) V157( INT.Ring ) V158( INT.Ring ) V159( INT.Ring ) V163() V164() V165() free V259() V260() V261() V262() for ModuleStr over INT.Ring ;

existence ex b

( b

proof end;

registration

let V be Z_Module;

ex b_{1} being Submodule of V st

( b_{1} is strict & b_{1} is free )

end;
cluster non empty left_add-cancelable right_add-cancelable right_complementable strict V156( INT.Ring ) V157( INT.Ring ) V158( INT.Ring ) V159( INT.Ring ) V163() V164() V165() free V259() V260() V261() V262() for Subspace of V;

existence ex b

( b

proof end;

registration
end;

registration

for b_{1} being free Z_Module holds b_{1} is Mult-cancelable
end;

cluster non empty right_complementable V156( INT.Ring ) V157( INT.Ring ) V158( INT.Ring ) V159( INT.Ring ) V163() V164() V165() free -> free Mult-cancelable for ModuleStr over INT.Ring ;

coherence for b

proof end;

registration

existence

ex b_{1} being non trivial Z_Module st b_{1} is free ;

end;

cluster non empty non trivial left_add-cancelable right_add-cancelable right_complementable V156( INT.Ring ) V157( INT.Ring ) V158( INT.Ring ) V159( INT.Ring ) V163() V164() V165() free V259() V260() V261() V262() for ModuleStr over INT.Ring ;

correctness existence

ex b

proof end;

theorem Th3: :: ZMODUL03:3

for V being Z_Module

for KL1, KL2 being Linear_Combination of V

for X being Subset of V st X is linearly-independent & Carrier KL1 c= X & Carrier KL2 c= X & Sum KL1 = Sum KL2 holds

KL1 = KL2

for KL1, KL2 being Linear_Combination of V

for X being Subset of V st X is linearly-independent & Carrier KL1 c= X & Carrier KL2 c= X & Sum KL1 = Sum KL2 holds

KL1 = KL2

proof end;

theorem :: ZMODUL03:4

for V being free 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 * 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 * v in Lin B ) )

proof end;

theorem Th5: :: ZMODUL03:5

for V being Z_Module

for L being Linear_Combination of V

for F, G being FinSequence of V

for P being Permutation of (dom F) st G = F * P holds

Sum (L (#) F) = Sum (L (#) G)

for L being Linear_Combination of V

for F, G being FinSequence of V

for P being Permutation of (dom F) st G = F * P holds

Sum (L (#) F) = Sum (L (#) G)

proof end;

theorem Th6: :: ZMODUL03:6

for V being Z_Module

for L being Linear_Combination of V

for F being FinSequence of V st Carrier L misses rng F holds

Sum (L (#) F) = 0. V

for L being Linear_Combination of V

for F being FinSequence of V st Carrier L misses rng F holds

Sum (L (#) F) = 0. V

proof end;

theorem :: ZMODUL03:7

for V being Z_Module

for F being FinSequence of V st F is one-to-one holds

for L being Linear_Combination of V st Carrier L c= rng F holds

Sum (L (#) F) = Sum L

for F being FinSequence of V st F is one-to-one holds

for L being Linear_Combination of V st Carrier L c= rng F holds

Sum (L (#) F) = Sum L

proof end;

theorem :: ZMODUL03:8

for V being Z_Module

for L being Linear_Combination of V

for F being FinSequence of V ex K being Linear_Combination of V st

( Carrier K = (rng F) /\ (Carrier L) & L (#) F = K (#) F )

for L being Linear_Combination of V

for F being FinSequence of V ex K being Linear_Combination of V st

( Carrier K = (rng F) /\ (Carrier L) & L (#) F = K (#) F )

proof end;

theorem Th9: :: ZMODUL03:9

for V being Z_Module

for L being Linear_Combination of V

for A being Subset of V

for F being FinSequence of V st rng F c= the carrier of (Lin A) holds

ex K being Linear_Combination of A st Sum (L (#) F) = Sum K

for L being Linear_Combination of V

for A being Subset of V

for F being FinSequence of V st rng F c= the carrier of (Lin A) holds

ex K being Linear_Combination of A st Sum (L (#) F) = Sum K

proof end;

theorem Th10: :: ZMODUL03:10

for V being Z_Module

for L being Linear_Combination of V

for A being Subset of V st Carrier L c= the carrier of (Lin A) holds

ex K being Linear_Combination of A st Sum L = Sum K

for L being Linear_Combination of V

for A being Subset of V st Carrier L c= the carrier of (Lin A) holds

ex K being Linear_Combination of A st Sum L = Sum K

proof end;

theorem Th11: :: ZMODUL03:11

for V being Z_Module

for W being Submodule of V

for L being Linear_Combination of V st Carrier L c= the carrier of W holds

for K being Linear_Combination of W st K = L | the carrier of W holds

( Carrier L = Carrier K & Sum L = Sum K )

for W being Submodule of V

for L being Linear_Combination of V st Carrier L c= the carrier of W holds

for K being Linear_Combination of W st K = L | the carrier of W holds

( Carrier L = Carrier K & Sum L = Sum K )

proof end;

theorem Th12: :: ZMODUL03:12

for V being Z_Module

for W being Submodule of V

for K being Linear_Combination of W ex L being Linear_Combination of V st

( Carrier K = Carrier L & Sum K = Sum L )

for W being Submodule of V

for K being Linear_Combination of W ex L being Linear_Combination of V st

( Carrier K = Carrier L & Sum K = Sum L )

proof end;

theorem Th13: :: ZMODUL03:13

for V being Z_Module

for W being Submodule of V

for L being Linear_Combination of V st Carrier L c= the carrier of W holds

ex K being Linear_Combination of W st

( Carrier K = Carrier L & Sum K = Sum L )

for W being Submodule of V

for L being Linear_Combination of V st Carrier L c= the carrier of W holds

ex K being Linear_Combination of W st

( Carrier K = Carrier L & Sum K = Sum L )

proof end;

theorem :: ZMODUL03:15

for V being Z_Module

for W being Submodule of V

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

A is linearly-independent Subset of V

for W being Submodule of V

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

A is linearly-independent Subset of V

proof end;

theorem Th16: :: ZMODUL03:16

for V being Z_Module

for W being Submodule of V

for A being Subset of V st A is linearly-independent & A c= the carrier of W holds

A is linearly-independent Subset of W

for W being Submodule of V

for A being Subset of V st A is linearly-independent & A c= the carrier of W holds

A is linearly-independent Subset of W

proof end;

theorem Th17: :: ZMODUL03:17

for V being Z_Module

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

for v being Vector of V st v in A holds

for B being Subset of V st B = A \ {v} holds

not v in Lin B

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

for v being Vector of V st v in A holds

for B being Subset of V st B = A \ {v} holds

not v in Lin B

proof end;

theorem Th18: :: ZMODUL03:18

for V being free Z_Module

for I being Basis of V

for A being non empty Subset of V st A misses I holds

for B being Subset of V st B = I \/ A holds

B is linearly-dependent

for I being Basis of V

for A being non empty Subset of V st A misses I holds

for B being Subset of V st B = I \/ A holds

B is linearly-dependent

proof end;

theorem :: ZMODUL03:19

for V being Z_Module

for W being Submodule of V

for A being Subset of V st A c= the carrier of W holds

Lin A is Submodule of W

for W being Submodule of V

for A being Subset of V st A c= the carrier of W holds

Lin A is Submodule of W

proof end;

theorem Th20: :: ZMODUL03:20

for V being Z_Module

for W being Submodule of V

for A being Subset of V

for B being Subset of W st A = B holds

Lin A = Lin B

for W being Submodule of V

for A being Subset of V

for B being Subset of W st A = B holds

Lin A = Lin B

proof end;

registration

let V be Z_Module;

let A be linearly-independent Subset of V;

correctness

coherence

Lin A is free ;

end;
let A be linearly-independent Subset of V;

correctness

coherence

Lin A is free ;

proof end;

registration
end;

definition

let IT be free Z_Module;

end;
attr IT is finite-rank means :Def3: :: ZMODUL03:def 3

ex A being finite Subset of IT st A is Basis of IT;

ex A being finite Subset of IT st A is Basis of IT;

:: deftheorem Def3 defines finite-rank ZMODUL03:def 3 :

for IT being free Z_Module holds

( IT is finite-rank iff ex A being finite Subset of IT st A is Basis of IT );

for IT being free Z_Module holds

( IT is finite-rank iff ex A being finite Subset of IT st A is Basis of IT );

registration
end;

registration

ex b_{1} being free Z_Module st

( b_{1} is strict & b_{1} is finite-rank )
end;

cluster non empty left_add-cancelable right_add-cancelable right_complementable strict V156( INT.Ring ) V157( INT.Ring ) V158( INT.Ring ) V159( INT.Ring ) V163() V164() V165() free V259() V260() V261() V262() Mult-cancelable finite-rank for ModuleStr over INT.Ring ;

existence ex b

( b

proof end;

registration

let V be Z_Module;

ex b_{1} being free Submodule of V st

( b_{1} is strict & b_{1} is finite-rank )

end;
cluster non empty left_add-cancelable right_add-cancelable right_complementable strict V156( INT.Ring ) V157( INT.Ring ) V158( INT.Ring ) V159( INT.Ring ) V163() V164() V165() free V259() V260() V261() V262() Mult-cancelable finite-rank for Subspace of V;

existence ex b

( b

proof end;

registration

let V be Z_Module;

let A be finite linearly-independent Subset of V;

coherence

Lin A is finite-rank

end;
let A be finite linearly-independent Subset of V;

coherence

Lin A is finite-rank

proof end;

:: deftheorem defines finitely-generated ZMODUL03:def 4 :

for V being Z_Module holds

( V is finitely-generated iff ex A being finite Subset of V st Lin A = ModuleStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #) );

for V being Z_Module holds

( V is finitely-generated iff ex A being finite Subset of V st Lin A = ModuleStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #) );

registration

ex b_{1} being Z_Module st

( b_{1} is strict & b_{1} is finitely-generated & b_{1} is free )
end;

cluster non empty left_add-cancelable right_add-cancelable right_complementable strict V156( INT.Ring ) V157( INT.Ring ) V158( INT.Ring ) V159( INT.Ring ) V163() V164() V165() free V259() V260() V261() V262() finitely-generated for ModuleStr over INT.Ring ;

existence ex b

( b

proof end;

registration

let V be free finite-rank Z_Module;

coherence

for b_{1} being Basis of V holds b_{1} is finite

end;
coherence

for b

proof end;

theorem Th21: :: ZMODUL03:21

for p being prime Element of INT.Ring

for V being free Z_Module

for I being Basis of V

for u1, u2 being Vector of V st u1 <> u2 & u1 in I & u2 in I holds

ZMtoMQV (V,p,u1) <> ZMtoMQV (V,p,u2)

for V being free Z_Module

for I being Basis of V

for u1, u2 being Vector of V st u1 <> u2 & u1 in I & u2 in I holds

ZMtoMQV (V,p,u1) <> ZMtoMQV (V,p,u2)

proof end;

theorem Th22: :: ZMODUL03:22

for p being prime Element of INT.Ring

for V being Z_Module

for ZQ being VectSp of GF p

for vq being Vector of ZQ st ZQ = Z_MQ_VectSp (V,p) holds

ex v being Vector of V st vq = ZMtoMQV (V,p,v)

for V being Z_Module

for ZQ being VectSp of GF p

for vq being Vector of ZQ st ZQ = Z_MQ_VectSp (V,p) holds

ex v being Vector of V st vq = ZMtoMQV (V,p,v)

proof end;

Lm2: for p being prime Element of INT.Ring

for V being Z_Module

for v, w being Vector of V st (ZMtoMQV (V,p,w)) /\ (ZMtoMQV (V,p,v)) <> {} holds

ZMtoMQV (V,p,w) = ZMtoMQV (V,p,v)

proof end;

theorem Th23: :: ZMODUL03:23

for p being prime Element of INT.Ring

for V being Z_Module

for I being Subset of V

for lq being Linear_Combination of Z_MQ_VectSp (V,p) ex l being Linear_Combination of I st

for v being Vector of V st v in I holds

ex w being Vector of V st

( w in I & w in ZMtoMQV (V,p,v) & l . w = lq . (ZMtoMQV (V,p,v)) )

for V being Z_Module

for I being Subset of V

for lq being Linear_Combination of Z_MQ_VectSp (V,p) ex l being Linear_Combination of I st

for v being Vector of V st v in I holds

ex w being Vector of V st

( w in I & w in ZMtoMQV (V,p,v) & l . w = lq . (ZMtoMQV (V,p,v)) )

proof end;

theorem Th24: :: ZMODUL03:24

for p being prime Element of INT.Ring

for V being free Z_Module

for I being Basis of V

for lq being Linear_Combination of Z_MQ_VectSp (V,p) ex l being Linear_Combination of I st

for v being Vector of V st v in I holds

l . v = lq . (ZMtoMQV (V,p,v))

for V being free Z_Module

for I being Basis of V

for lq being Linear_Combination of Z_MQ_VectSp (V,p) ex l being Linear_Combination of I st

for v being Vector of V st v in I holds

l . v = lq . (ZMtoMQV (V,p,v))

proof end;

theorem Th25: :: ZMODUL03:25

for p being prime Element of INT.Ring

for V being free Z_Module

for I being Basis of V

for X being non empty Subset of (Z_MQ_VectSp (V,p)) st X = { (ZMtoMQV (V,p,u)) where u is Vector of V : u in I } holds

ex F being Function of X, the carrier of V st

( ( for u being Vector of V st u in I holds

F . (ZMtoMQV (V,p,u)) = u ) & F is one-to-one & dom F = X & rng F = I )

for V being free Z_Module

for I being Basis of V

for X being non empty Subset of (Z_MQ_VectSp (V,p)) st X = { (ZMtoMQV (V,p,u)) where u is Vector of V : u in I } holds

ex F being Function of X, the carrier of V st

( ( for u being Vector of V st u in I holds

F . (ZMtoMQV (V,p,u)) = u ) & F is one-to-one & dom F = X & rng F = I )

proof end;

theorem Th26: :: ZMODUL03:26

for p being prime Element of INT.Ring

for V being free Z_Module

for I being Basis of V holds card { (ZMtoMQV (V,p,u)) where u is Vector of V : u in I } = card I

for V being free Z_Module

for I being Basis of V holds card { (ZMtoMQV (V,p,u)) where u is Vector of V : u in I } = card I

proof end;

theorem Th27: :: ZMODUL03:27

for p being prime Element of INT.Ring

for V being free Z_Module holds ZMtoMQV (V,p,(0. V)) = 0. (Z_MQ_VectSp (V,p))

for V being free Z_Module holds ZMtoMQV (V,p,(0. V)) = 0. (Z_MQ_VectSp (V,p))

proof end;

theorem Th28: :: ZMODUL03:28

for p being prime Element of INT.Ring

for V being free Z_Module

for s, t being Element of V holds (ZMtoMQV (V,p,s)) + (ZMtoMQV (V,p,t)) = ZMtoMQV (V,p,(s + t))

for V being free Z_Module

for s, t being Element of V holds (ZMtoMQV (V,p,s)) + (ZMtoMQV (V,p,t)) = ZMtoMQV (V,p,(s + t))

proof end;

theorem Th29: :: ZMODUL03:29

for p being prime Element of INT.Ring

for V being free Z_Module

for s being FinSequence of V

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

Sum t = ZMtoMQV (V,p,(Sum s))

for V being free Z_Module

for s being FinSequence of V

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

Sum t = ZMtoMQV (V,p,(Sum s))

proof end;

theorem Th30: :: ZMODUL03:30

for p being prime Element of INT.Ring

for V being free Z_Module

for s being Element of V

for a being Element of INT.Ring

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

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

for V being free Z_Module

for s being Element of V

for a being Element of INT.Ring

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

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

proof end;

theorem Th31: :: ZMODUL03:31

for p being prime Element of INT.Ring

for V being free Z_Module

for I being Basis of V

for l being Linear_Combination of I

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

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

l . v = lq . (ZMtoMQV (V,p,v)) ) holds

Sum lq = ZMtoMQV (V,p,(Sum l))

for V being free Z_Module

for I being Basis of V

for l being Linear_Combination of I

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

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

l . v = lq . (ZMtoMQV (V,p,v)) ) holds

Sum lq = ZMtoMQV (V,p,(Sum l))

proof end;

theorem Th32: :: ZMODUL03:32

for p being prime Element of INT.Ring

for V being free Z_Module

for I being Basis of V

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

IQ is linearly-independent

for V being free Z_Module

for I being Basis of V

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

IQ is linearly-independent

proof end;

Lm3: for p being Prime

for i being Element of INT holds i mod p is Element of (GF p)

proof end;

Lm4: 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 Th33: :: ZMODUL03:33

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 IQ = { (ZMtoMQV (V,p,u)) where u is Vector of V : u in I } holds

for s being FinSequence of V st ( for i being Element of NAT st i in dom s holds

ex si being Vector of V st

( si = s . i & ZMtoMQV (V,p,si) in Lin IQ ) ) holds

ZMtoMQV (V,p,(Sum s)) 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)) st IQ = { (ZMtoMQV (V,p,u)) where u is Vector of V : u in I } holds

for s being FinSequence of V st ( for i being Element of NAT st i in dom s holds

ex si being Vector of V st

( si = s . i & ZMtoMQV (V,p,si) in Lin IQ ) ) holds

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

proof end;

theorem Th34: :: ZMODUL03:34

for p being prime Element of INT.Ring

for V being free Z_Module

for I being Basis 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 Basis 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 Th35: :: ZMODUL03:35

for p being prime Element of INT.Ring

for V being free Z_Module

for I being Basis of V

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

IQ is Basis of (Z_MQ_VectSp (V,p))

for V being free Z_Module

for I being Basis of V

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

IQ is Basis of (Z_MQ_VectSp (V,p))

proof end;

registration

let p be prime Element of INT.Ring;

let V be free finite-rank Z_Module;

coherence

Z_MQ_VectSp (V,p) is finite-dimensional

end;
let V be free finite-rank Z_Module;

coherence

Z_MQ_VectSp (V,p) is finite-dimensional

proof end;

definition

let V be free finite-rank Z_Module;

existence

ex b_{1} being Nat st

for I being Basis of V holds b_{1} = card I

for b_{1}, b_{2} being Nat st ( for I being Basis of V holds b_{1} = card I ) & ( for I being Basis of V holds b_{2} = card I ) holds

b_{1} = b_{2}

end;
existence

ex b

for I being Basis of V holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def5 defines rank ZMODUL03:def 5 :

for V being free finite-rank Z_Module

for b_{2} being Nat holds

( b_{2} = rank V iff for I being Basis of V holds b_{2} = card I );

for V being free finite-rank Z_Module

for b

( b

theorem :: ZMODUL03:37

for p being prime Element of INT.Ring

for V being free finite-rank Z_Module holds rank V = dim (Z_MQ_VectSp (V,p))

for V being free finite-rank Z_Module holds rank V = dim (Z_MQ_VectSp (V,p))

proof end;