let V, W be free finite-rank Z_Module; for T being linear-transformation of V,W holds rank V = (rank T) + (nullity T)
let T be linear-transformation of V,W; rank V = (rank T) + (nullity T)
set A = the finite Basis of (ker T);
reconsider A9 = the finite Basis of (ker T) as Subset of V by ZMODUL05:29;
reconsider A9 = A9 as finite linearly-independent Subset of V by VECTSP_7:def 3, ZMODUL03:15;
consider B9 being finite linearly-independent Subset of V, a being Element of INT.Ring such that
A1:
( a <> 0. INT.Ring & A9 c= B9 & a (*) V is Submodule of Lin B9 )
by LmRankSX11;
X1:
V is free finite-rank Submodule of V
by ZMODUL01:32;
rank (a (*) V) <= rank (Lin B9)
by A1, ZMODUL05:2;
then X2:
rank V <= rank (Lin B9)
by A1, X1, ZMODUL06:52;
rank (Lin B9) <= rank V
by ZMODUL05:2;
then
rank (Lin B9) = rank V
by X2, XXREAL_0:1;
then X0:
rank V = card B9
by ZMODUL05:3;
reconsider X = B9 \ A9 as finite Subset of B9 by XBOOLE_1:36;
reconsider X = X as finite Subset of V ;
A2:
B9 = A9 \/ X
by A1, XBOOLE_1:45;
reconsider C = T .: X as finite Subset of W ;
A3:
T | X is one-to-one
by A1, X0, ZM05Th35;
C is linearly-independent
proof
assume
C is
linearly-dependent
;
contradiction
then consider l being
Linear_Combination of
C such that A5:
Carrier l <> {}
and A6:
Sum l = 0. W
;
ex
m being
Linear_Combination of
X st
l = T @* m
then consider m being
Linear_Combination of
B9 \ A9 such that A7:
l = T @* m
;
T . (Sum m) = 0. W
by A1, A6, A7, X0, ZM05Th59;
then
Sum m in ker T
by ZMODUL05:20;
then
Sum m in Lin the
finite Basis of
(ker T)
by VECTSP_7:def 3;
then
Sum m in Lin A9
by ZMODUL03:20;
then consider n being
Linear_Combination of
A9 such that A8:
Sum m = Sum n
by ZMODUL02:64;
A9:
(
Carrier (m - n) c= (Carrier m) \/ (Carrier n) &
(B9 \ A9) \/ A9 = B9 )
by A1, ZMODUL02:40, XBOOLE_1:45;
A10:
(
Carrier m c= B9 \ A9 &
Carrier n c= the
finite Basis of
(ker T) )
by VECTSP_6:def 4;
then
(Carrier m) \/ (Carrier n) c= (B9 \ A9) \/ the
finite Basis of
(ker T)
by XBOOLE_1:13;
then
Carrier (m - n) c= B9
by A9;
then reconsider o =
m - n as
Linear_Combination of
B9 by VECTSP_6:def 4;
(Sum m) - (Sum n) = 0. V
by A8, VECTSP_1:19;
then
Sum (m - n) = 0. V
by ZMODUL02:55;
then A12:
Carrier o = {}
by VECTSP_7:def 1;
A9 misses B9 \ A9
by XBOOLE_1:79;
then
Carrier (m - n) = (Carrier m) \/ (Carrier n)
by A10, XBOOLE_1:64, ZMODUL05:48;
then
Carrier m = {}
by A12;
then
T .: (Carrier m) = {}
;
hence
contradiction
by A5, A7, XBOOLE_1:3, ZMODUL05:def 8;
verum
end;
then reconsider C = C as finite linearly-independent Subset of W ;
dom T = [#] V
by LmDOMRNG;
then
X c= dom (T | X)
by RELAT_1:62;
then
X,(T | X) .: X are_equipotent
by A3, CARD_1:33;
then
X,C are_equipotent
by RELAT_1:129;
then A13:
card C = card X
by CARD_1:5;
reconsider aT = a (*) (im T) as Submodule of W by ZMODUL01:42;
L1:
Lin (T .: B9) = Lin (T .: X)
by A2, LMTh44;
for v being VECTOR of W st v in aT holds
v in Lin C
then
a (*) (im T) is Submodule of Lin C
by ZMODUL01:44;
then
rank (a (*) (im T)) <= rank (Lin C)
by ZMODUL05:2;
then X4:
rank (im T) <= rank (Lin C)
by A1, ZMODUL06:52;
reconsider CC = C as Subset of (im T) by ZMODUL05:22;
Lin CC is Submodule of im T
;
then
Lin C is Submodule of im T
by ZMODUL03:20;
then
rank (Lin C) <= rank (im T)
by ZMODUL05:2;
then X5: rank T =
rank (Lin C)
by X4, XXREAL_0:1
.=
card C
by ZMODUL05:3
;
nullity T = card the finite Basis of (ker T)
by ZMODUL03:def 5;
hence
rank V = (rank T) + (nullity T)
by A2, A13, X0, X5, CARD_2:40, XBOOLE_1:79; verum