:: Rank of Submodule, Linear Transformations and Linearly Independent Subsets of $\mathbb Z$-module
:: by Kazuhisa Nakasho , Yuichi Futa , Hiroyuki Okazaki and Yasunari Shidama
::
:: Received July 10, 2014
:: Copyright (c) 2014-2021 Association of Mizar Users


registration
let V be LeftMod of INT.Ring ;
let A be finite Subset of V;
cluster Lin A -> finitely-generated ;
correctness
coherence
Lin A is finitely-generated ;
proof end;
end;

theorem RL5Th33: :: ZMODUL05:1
for V being free finite-rank Z_Module holds
( rank V = 0 iff (Omega). V = (0). V )
proof end;

registration
let V be free finite-rank Z_Module;
cluster finite base for Element of K10( the carrier of V);
existence
ex b1 being Basis of V st b1 is finite
proof end;
end;

registration
let V be free finite-rank Z_Module;
cluster base -> finite for Element of K10( the carrier of V);
correctness
coherence
for b1 being Basis of V holds b1 is finite ;
;
end;

theorem RL5Th29: :: ZMODUL05:2
for V being free finite-rank Z_Module
for W being Submodule of V holds rank W <= rank V
proof end;

theorem RL5Th30: :: ZMODUL05:3
for V being Z_Module
for A being finite linearly-independent Subset of V holds card A = rank (Lin A)
proof end;

theorem :: ZMODUL05:4
for V being free finite-rank Z_Module holds rank V = rank ((Omega). V)
proof end;

theorem :: ZMODUL05:5
for V being free finite-rank Z_Module holds
( rank V = 1 iff ex v being VECTOR of V st
( v <> 0. V & (Omega). V = Lin {v} ) )
proof end;

theorem :: ZMODUL05:6
for V being free finite-rank Z_Module holds
( rank V = 2 iff ex u, v being VECTOR of V st
( u <> v & {u,v} is linearly-independent & (Omega). V = Lin {u,v} ) )
proof end;

RL5Lm2: for V being free finite-rank Z_Module
for W being Submodule of V
for n being Nat st n <= rank V holds
ex W being strict free Submodule of V st rank W = n
proof end;

theorem :: ZMODUL05:7
for V being free finite-rank Z_Module
for W being Submodule of V
for n being Nat holds
( n <= rank V iff ex W being strict free Submodule of V st rank W = n ) by RL5Lm2, RL5Th29;

definition
let V be free finite-rank Z_Module;
let n be Nat;
func n Submodules_of V -> set means :RL5Def4: :: ZMODUL05:def 1
 for x being object holds
( x in it iff ex W being strict free Submodule of V st
( W = x & rank W = n ) );
existence
ex b1 being set st
for x being object holds
( x in b1 iff ex W being strict free Submodule of V st
( W = x & rank W = n ) )
proof end;
uniqueness
for b1, b2 being set st ( for x being object holds
( x in b1 iff ex W being strict free Submodule of V st
( W = x & rank W = n ) ) ) & ( for x being object holds
( x in b2 iff ex W being strict free Submodule of V st
( W = x & rank W = n ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem RL5Def4 defines Submodules_of ZMODUL05:def 1 :
for V being free finite-rank Z_Module
for n being Nat
for b3 being set holds
( b3 = n Submodules_of V iff for x being object holds
( x in b3 iff ex W being strict free Submodule of V st
( W = x & rank W = n ) ) );

theorem :: ZMODUL05:8
for V being free finite-rank Z_Module
for n being Nat st n <= rank V holds
not n Submodules_of V is empty
proof end;

theorem :: ZMODUL05:9
for V being free finite-rank Z_Module
for n being Nat st rank V < n holds
n Submodules_of V = {}
proof end;

theorem :: ZMODUL05:10
for V being free finite-rank Z_Module
for W being Submodule of V
for n being Nat holds n Submodules_of W c= n Submodules_of V
proof end;

theorem :: ZMODUL05:11
for F, G being FinSequence of INT
for v being Integer st len F = (len G) + 1 & G = F | (dom G) & v = F . (len F) holds
Sum F = (Sum G) + v
proof end;

theorem RLVECT142: :: ZMODUL05:12
for F, G being FinSequence of INT st rng F = rng G & F is one-to-one & G is one-to-one holds
Sum F = Sum G
proof end;

definition
let T be finite Subset of the carrier of INT.Ring;
::: what for? defined for reals, then redefine
func Sum T -> Element of INT.Ring means :: ZMODUL05:def 2
 ex F being FinSequence of INT st
( rng F = T & F is one-to-one & it = Sum F );
existence
ex b1 being Element of INT.Ring ex F being FinSequence of INT st
( rng F = T & F is one-to-one & b1 = Sum F )
proof end;
uniqueness
for b1, b2 being Element of INT.Ring st ex F being FinSequence of INT st
( rng F = T & F is one-to-one & b1 = Sum F ) & ex F being FinSequence of INT st
( rng F = T & F is one-to-one & b2 = Sum F ) holds
b1 = b2 by RLVECT142;
end;

:: deftheorem defines Sum ZMODUL05:def 2 :
for T being finite Subset of the carrier of INT.Ring
for b2 being Element of INT.Ring holds
( b2 = Sum T iff ex F being FinSequence of INT st
( rng F = T & F is one-to-one & b2 = Sum F ) );

theorem RF9: :: ZMODUL05:13
for K being Ring
for R1, R2 being FinSequence of K st R1,R2 are_fiberwise_equipotent holds
Sum R1 = Sum R2
proof end;

theorem :: ZMODUL05:14
canceled;

theorem :: ZMODUL05:15
canceled;

::$CT 2
::theorem
::: for X be finite Subset of INT st X = {}
::: holds Sum X = 0 by Def2,GR_CY_1:3,RELAT_1:38;
::theorem
:: for v be Element of INT holds Sum {v} = v
:: proof
:: let v be Element of INT;
:: A1: Sum <*v*> = v by RVSUM_1:73;
:: rng <*v*> = {v} & <*v*> is one-to-one by FINSEQ_1:39;
:: hence Sum {v} = v by A1,Def2;
:: end;
::theorem
:: for S, T being finite Subset of INT
:: st T misses S holds
:: Sum (T \/ S) = (Sum T) + (Sum S)
:: proof
:: let S, T be finite Subset of INT;
:: consider F being FinSequence of INT such that
:: A1: rng F = T \/ S and
:: A2: F is one-to-one & Sum (T \/ S) = Sum F by Def2;
:: consider G being FinSequence of INT such that
:: A3: rng G = T and
:: A4: G is one-to-one and
:: A5: Sum T = Sum G by Def2;
:: consider H being FinSequence of INT such that
:: A6: rng H = S and
:: A7: H is one-to-one and
:: A8: Sum S = Sum H by Def2;
:: set I = G ^ H;
:: reconsider G0 = G, H0 = H as real-valued FinSequence;
::: A9: Sum (G0 ^ H0) = Sum (G) + Sum (H) by RVSUM_1:75;
:: assume T misses S; then
:: A10: G ^ H is one-to-one by A3,A4,A6,A7,FINSEQ_3:91;
:: rng (G ^ H) = rng F by A1,A3,A6,FINSEQ_1:31;
:: hence Sum (T \/ S) = (Sum T) + (Sum S) by A2,A5,A8,A9,A10,RLVECT142;
:: end;
definition
end;

:: deftheorem ZMODUL05:def 3 :
canceled;

:: deftheorem ZMODUL05:def 4 :
canceled;

:: deftheorem ZMODUL05:def 5 :
canceled;

theorem MATRLIN16: :: ZMODUL05:16
for R being Ring
for V1, V2 being LeftMod of R
for f being Function of V1,V2
for p being FinSequence of V1 st f is additive & f is homogeneous holds
f . (Sum p) = Sum (f * p)
proof end;

theorem :: ZMODUL05:17
for V being free Z_Module st [#] V is finite holds
(Omega). V = (0). V
proof end;

theorem :: ZMODUL05:18
for F being Ring
for V, W being VectSp of F
for T being linear-transformation of V,W
for x, y being Element of V holds (T . x) - (T . y) = T . (x - y) by RANKNULL:8;

theorem :: ZMODUL05:19
for V, W being Z_Module
for T being linear-transformation of V,W holds T . (0. V) = 0. W by RANKNULL:9;

theorem :: ZMODUL05:20
for V, W being Z_Module
for T being linear-transformation of V,W
for x being Element of V holds
( x in ker T iff T . x = 0. W ) by RANKNULL:10;

theorem :: ZMODUL05:21
for V, W being Z_Module
for T being linear-transformation of V,W holds 0. V in ker T by RANKNULL:11;

theorem :: ZMODUL05:22
for V, W being Z_Module
for T being linear-transformation of V,W
for X being Subset of V holds T .: X is Subset of (im T) by RANKNULL:12;

theorem :: ZMODUL05:23
for V, W being Z_Module
for T being linear-transformation of V,W
for y being Element of W holds
( y in im T iff ex x being Element of V st y = T . x ) by RANKNULL:13;

theorem :: ZMODUL05:24
for V, W being Z_Module
for T being linear-transformation of V,W
for x being Element of (ker T) holds T . x = 0. W by RANKNULL:14;

theorem :: ZMODUL05:25
for V, W being Z_Module
for T being linear-transformation of V,W st T is one-to-one holds
ker T = (0). V by RANKNULL:15;

theorem :: ZMODUL05:26
for V being free finite-rank Z_Module holds rank ((0). V) = 0
proof end;

theorem Th17: :: ZMODUL05:27
for V, W being Z_Module
for T being linear-transformation of V,W
for x, y being Element of V st T . x = T . y holds
x - y in ker T by RANKNULL:17;

theorem Th18: :: ZMODUL05:28
for V being Z_Module
for A being Subset of V
for x, y being Element of V st x - y in Lin A holds
x in Lin (A \/ {y}) by RANKNULL:18;

:: combinations
theorem :: ZMODUL05:29
for V, W being Z_Module
for X being Subset of V st V is Submodule of W holds
X is Subset of W
proof end;

theorem ThLin4: :: ZMODUL05:30
for R being Ring
for V being LeftMod of R
for A being Subset of V holds A is Subset of (Lin A)
proof end;

theorem ThLin7: :: ZMODUL05:31
for V being LeftMod of INT.Ring
for A being linearly-independent Subset of V holds A is Basis of (Lin A)
proof end;

:: Adjoining an element x to A that is already in its linear span
:: results in a linearly dependent set.
theorem Th21: :: ZMODUL05:32
for V being free finite-rank Z_Module
for A being Subset of V
for x being Element of V st x in Lin A & not x in A holds
A \/ {x} is linearly-dependent
proof end;

registration
let V be free finite-rank Z_Module;
let W be Z_Module;
let T be linear-transformation of V,W;
cluster ker T -> free finite-rank ;
correctness
coherence
( ker T is finite-rank & ker T is free );
;
end;

theorem Th22: :: ZMODUL05:33
for W being Z_Module
for V being free finite-rank Z_Module
for A being Subset of V
for B being Basis of V
for T being linear-transformation of V,W st A is Basis of (ker T) & A c= B holds
T | (B \ A) is one-to-one
proof end;

theorem :: ZMODUL05:34
for R being Ring
for V being LeftMod of R
for A being Subset of V
for l being Linear_Combination of A
for x being Element of V
for a being Element of R holds l +* (x,a) is Linear_Combination of A \/ {x}
proof end;

registration
let R be non degenerated Ring;
let V be LeftMod of R;
cluster linearly-dependent for Element of K10( the carrier of V);
existence
ex b1 being Subset of V st b1 is linearly-dependent
proof end;
end;

:: Restricting a linear combination to a given set
definition
let R be Ring;
let V be LeftMod of R;
let l be Linear_Combination of V;
let A be Subset of V;
func l ! A -> Linear_Combination of A equals :: ZMODUL05:def 6
(l | A) +* ((A `) --> (0. R));
coherence
(l | A) +* ((A `) --> (0. R)) is Linear_Combination of A
proof end;
end;

:: deftheorem defines ! ZMODUL05:def 6 :
for R being Ring
for V being LeftMod of R
for l being Linear_Combination of V
for A being Subset of V holds l ! A = (l | A) +* ((A `) --> (0. R));

theorem Th24: :: ZMODUL05:35
for R being Ring
for V being LeftMod of R
for l being Linear_Combination of V holds l = l ! (Carrier l)
proof end;

Lm1: for R being Ring
for V being LeftMod of R
for l being Linear_Combination of V
for X being Subset of V holds l .: X is finite
proof end;

theorem Th25: :: ZMODUL05:36
for R being Ring
for V being LeftMod of R
for l being Linear_Combination of V
for A being Subset of V
for v being Element of V st v in A holds
(l ! A) . v = l . v
proof end;

theorem Th26: :: ZMODUL05:37
for R being Ring
for V being LeftMod of R
for l being Linear_Combination of V
for A being Subset of V
for v being Element of V st not v in A holds
(l ! A) . v = 0. R
proof end;

theorem Th27: :: ZMODUL05:38
for R being Ring
for V being LeftMod of R
for A, B being Subset of V
for l being Linear_Combination of B st A c= B holds
l = (l ! A) + (l ! (B \ A))
proof end;

registration
let R be Ring;
let V be LeftMod of R;
let l be Linear_Combination of V;
let X be Subset of V;
cluster l .: X -> finite ;
coherence
l .: X is finite by Lm1;
end;

theorem Th28: :: ZMODUL05:39
for R being Ring
for V being LeftMod of R
for l being Linear_Combination of V
for X being Subset of V st X misses Carrier l holds
l .: X c= {(0. R)}
proof end;

definition
let K be Ring;
let V, W be VectSp of K;
let l be Linear_Combination of V;
let T be linear-transformation of V,W;
let w be Element of W;
func lCFST (l,T,w) -> the carrier of K -valued FinSequence equals :: ZMODUL05:def 7
l * (canFS ((T " {w}) /\ (Carrier l)));
correctness
coherence
l * (canFS ((T " {w}) /\ (Carrier l))) is the carrier of K -valued FinSequence;
proof end;
end;

:: deftheorem defines lCFST ZMODUL05:def 7 :
for K being Ring
for V, W being VectSp of K
for l being Linear_Combination of V
for T being linear-transformation of V,W
for w being Element of W holds lCFST (l,T,w) = l * (canFS ((T " {w}) /\ (Carrier l)));

theorem ThTF3C0: :: ZMODUL05:40
for V, W being non empty set
for f being FinSequence
for l being Function of V,W st rng f c= V holds
( l * f is W -valued & l * f is FinSequence-like )
proof end;

registration
let V, W be non empty set ;
let f be V -valued FinSequence;
let l be Function of V,W;
cluster f (#) l -> W -valued FinSequence-like ;
coherence
( l * f is W -valued & l * f is FinSequence-like )
proof end;
end;

ThTF3C1: for V, W being non empty set
for A being finite Subset of V
for l being Function of V,W holds
( l * (canFS A) is W -valued & l * (canFS A) is FinSequence-like )
proof end;

registration
let V, W be non empty set ;
let A be finite Subset of V;
let l be Function of V,W;
cluster (canFS A) (#) l -> W -valued FinSequence-like ;
coherence
( l * (canFS A) is W -valued & l * (canFS A) is FinSequence-like ) by ThTF3C1;
end;

registration
let R be Ring;
let V be LeftMod of R;
let A be finite Subset of V;
let l be Linear_Combination of V;
cluster (canFS A) (#) l -> the carrier of R -valued FinSequence-like ;
coherence
( l * (canFS A) is the carrier of R -valued & l * (canFS A) is FinSequence-like ) ;
end;

theorem ThTF3C3: :: ZMODUL05:41
for V, W being non empty set
for f, g being b1 -valued FinSequence
for l being Function of V,W holds l * (f ^ g) = (l * f) ^ (l * g)
proof end;

theorem ThTF3C2: :: ZMODUL05:42
for R being Ring
for V being LeftMod of R
for A, B being finite Subset of V
for l being Linear_Combination of V
for l0, l1, l2 being FinSequence of R st A /\ B = {} & l0 = l * (canFS (A \/ B)) & l1 = l * (canFS A) & l2 = l * (canFS B) holds
Sum l0 = (Sum l1) + (Sum l2)
proof end;

theorem ThTF3C3: :: ZMODUL05:43
for R being Ring
for V being LeftMod of R
for A being finite Subset of V
for l, l0 being Linear_Combination of V st l | (Carrier l0) = l0 | (Carrier l0) & Carrier l0 c= Carrier l & A c= Carrier l0 holds
Sum (l * (canFS A)) = Sum (l0 * (canFS A))
proof end;

definition
let R be Ring;
let V, W be LeftMod of R;
let l be Linear_Combination of V;
let T be linear-transformation of V,W;
func T @* l -> Linear_Combination of W means :LDef5: :: ZMODUL05:def 8
( Carrier it c= T .: (Carrier l) & ( for w being Element of W holds it . w = Sum (lCFST (l,T,w)) ) );
existence
ex b1 being Linear_Combination of W st
( Carrier b1 c= T .: (Carrier l) & ( for w being Element of W holds b1 . w = Sum (lCFST (l,T,w)) ) )
proof end;
uniqueness
for b1, b2 being Linear_Combination of W st Carrier b1 c= T .: (Carrier l) & ( for w being Element of W holds b1 . w = Sum (lCFST (l,T,w)) ) & Carrier b2 c= T .: (Carrier l) & ( for w being Element of W holds b2 . w = Sum (lCFST (l,T,w)) ) holds
b1 = b2
proof end;
end;

:: deftheorem LDef5 defines @* ZMODUL05:def 8 :
for R being Ring
for V, W being LeftMod of R
for l being Linear_Combination of V
for T being linear-transformation of V,W
for b6 being Linear_Combination of W holds
( b6 = T @* l iff ( Carrier b6 c= T .: (Carrier l) & ( for w being Element of W holds b6 . w = Sum (lCFST (l,T,w)) ) ) );

theorem LTh29: :: ZMODUL05:44
for R being Ring
for V, W being LeftMod of R
for l being Linear_Combination of V
for T being linear-transformation of V,W holds T @* l is Linear_Combination of T .: (Carrier l)
proof end;

theorem ThTF3B2: :: ZMODUL05:45
for K being Ring
for V, W being LeftMod of K
for T being linear-transformation of V,W
for s being Vector of W
for A being Subset of V
for l being Linear_Combination of A st ( for v being Vector of V st v in Carrier l holds
T . v = s ) holds
T . (Sum l) = (Sum (lCFST (l,T,s))) * s
proof end;

theorem :: ZMODUL05:46
for K being Ring
for V, W being LeftMod of K
for T being linear-transformation of V,W
for A being Subset of V
for l being Linear_Combination of A
for Tl being Linear_Combination of T .: (Carrier l) st Tl = T @* l holds
T . (Sum l) = Sum Tl
proof end;

::: same as ZMODUL04:25
theorem Th31: :: ZMODUL05:47
for R being Ring
for V being LeftMod of R
for l, m being Linear_Combination of V st Carrier l misses Carrier m holds
Carrier (l + m) = (Carrier l) \/ (Carrier m)
proof end;

theorem Th32: :: ZMODUL05:48
for R being Ring
for V being LeftMod of R
for l, m being Linear_Combination of V st Carrier l misses Carrier m holds
Carrier (l - m) = (Carrier l) \/ (Carrier m)
proof end;

theorem :: ZMODUL05:49
for R being Ring
for V being LeftMod of R
for A being Subset of V
for l1, l2 being Linear_Combination of A st Carrier l1 misses Carrier l2 holds
Carrier (l1 - l2) = (Carrier l1) \/ (Carrier l2)
proof end;

theorem :: ZMODUL05:50
for V being free Z_Module
for A, B being Subset of V st A c= B & B is Basis of V holds
V is_the_direct_sum_of Lin A, Lin (B \ A)
proof end;

theorem :: ZMODUL05:51
for R being Ring
for V, W being LeftMod of R
for A being Subset of V
for l being Linear_Combination of A
for T being linear-transformation of V,W
for v being Element of V st T | A is one-to-one & v in A holds
ex X being Subset of V st
( X misses A & T " {(T . v)} = {v} \/ X )
proof end;

theorem :: ZMODUL05:52
for R being Ring
for V being LeftMod of R
for A being Subset of V
for l being Linear_Combination of A
for X being Subset of V st X misses Carrier l & X <> {} holds
l .: X = {(0. R)}
proof end;

theorem Th36: :: ZMODUL05:53
for R being Ring
for V, W being LeftMod of R
for l being Linear_Combination of V
for T being linear-transformation of V,W
for w being Element of W st w in Carrier (T @* l) holds
T " {w} meets Carrier l
proof end;

theorem Th37: :: ZMODUL05:54
for R being Ring
for V, W being LeftMod of R
for l being Linear_Combination of V
for T being linear-transformation of V,W
for v being Element of V st T | (Carrier l) is one-to-one & v in Carrier l holds
(T @* l) . (T . v) = l . v
proof end;

theorem Th38: :: ZMODUL05:55
for R being Ring
for V, W being LeftMod of R
for l being Linear_Combination of V
for T being linear-transformation of V,W
for G being FinSequence of V st rng G = Carrier l & T | (Carrier l) is one-to-one holds
T * (l (#) G) = (T @* l) (#) (T * G)
proof end;

theorem Th39: :: ZMODUL05:56
for R being Ring
for V, W being LeftMod of R
for l being Linear_Combination of V
for T being linear-transformation of V,W st T | (Carrier l) is one-to-one holds
T .: (Carrier l) = Carrier (T @* l)
proof end;

theorem :: ZMODUL05:57
for W being Z_Module
for V being free finite-rank Z_Module
for A being Subset of V
for B being Basis of V
for T being linear-transformation of V,W
for l being Linear_Combination of B \ A st A is Basis of (ker T) & A c= B holds
T . (Sum l) = Sum (T @* l)
proof end;

theorem :: ZMODUL05:58
for V being Z_Module
for X being Subset of V st X is linearly-dependent holds
ex l being Linear_Combination of X st
( Carrier l <> {} & Sum l = 0. V ) ;

:: "Pulling back" a linear combination from the image space of a
:: linear transformation to the base space.
definition
let R be Ring;
let V, W be LeftMod of R;
let X be Subset of V;
let T be linear-transformation of V,W;
let l be Linear_Combination of T .: X;
assume A1: T | X is one-to-one ;
func T # l -> Linear_Combination of X equals :Def6: :: ZMODUL05:def 9
(l * T) +* ((X `) --> (0. R));
coherence
(l * T) +* ((X `) --> (0. R)) is Linear_Combination of X
proof end;
end;

:: deftheorem Def6 defines # ZMODUL05:def 9 :
for R being Ring
for V, W being LeftMod of R
for X being Subset of V
for T being linear-transformation of V,W
for l being Linear_Combination of T .: X st T | X is one-to-one holds
T # l = (l * T) +* ((X `) --> (0. R));

theorem Th42: :: ZMODUL05:59
for R being Ring
for V, W being LeftMod of R
for X being Subset of V
for T being linear-transformation of V,W
for X being Subset of V
for l being Linear_Combination of T .: X
for v being Element of V st v in X & T | X is one-to-one holds
(T # l) . v = l . (T . v)
proof end;

:: # is a right inverse of @*
theorem :: ZMODUL05:60
for R being Ring
for V, W being LeftMod of R
for X being Subset of V
for T being linear-transformation of V,W
for X being Subset of V
for l being Linear_Combination of T .: X st T | X is one-to-one holds
T @* (T # l) = l
proof end;