let F be Field; :: thesis: for V, W being finite-dimensional VectSp of F
for T being linear-transformation of V,W holds dim V = (rank T) + (nullity T)
let V, W be finite-dimensional VectSp of F; :: thesis: for T being linear-transformation of V,W holds dim V = (rank T) + (nullity T)
let T be linear-transformation of V,W; :: thesis: dim V = (rank T) + (nullity T)
consider A being finite Basis of ker T;
reconsider A' = A as Subset of V by Th19;
consider B being Basis of V such that
A1:
A c= B
by VECTSP_9:17;
reconsider B = B as finite Subset of V by VECTSP_9:24;
reconsider X = B \ A' as finite Subset of B by XBOOLE_1:36;
reconsider X = X as finite Subset of V ;
A2:
B = A \/ X
by A1, XBOOLE_1:45;
reconsider C = T .: X as finite Subset of W ;
reconsider A = A as finite Basis of ker T ;
reconsider B = B as finite Basis of V ;
A3:
T | X is one-to-one
by A1, Th22;
A4:
X c= dom (T | X)
A5:
card C = card X
A6:
C is linearly-independent
proof
assume
not
C is
linearly-independent
;
:: thesis: contradiction
then consider l being
Linear_Combination of
C such that A7:
Carrier l <> {}
and A8:
Sum l = 0. W
by Th41;
ex
m being
Linear_Combination of
X st
l = T @ m
then consider m being
Linear_Combination of
B \ A' such that A9:
l = T @ m
;
T . (Sum m) = 0. W
by A1, A8, A9, Th40;
then
Sum m in ker T
by Th10;
then
Sum m in Lin A
by VECTSP_7:def 3;
then
Sum m in Lin A'
by VECTSP_9:21;
then consider n being
Linear_Combination of
A' such that A10:
Sum m = Sum n
by VECTSP_7:12;
(Sum m) - (Sum n) = 0. V
by A10, VECTSP_1:66;
then A11:
Sum (m - n) = 0. V
by VECTSP_6:80;
A12:
Carrier (m - n) c= (Carrier m) \/ (Carrier n)
by VECTSP_6:74;
A13:
Carrier m c= B \ A'
by VECTSP_6:def 7;
A14:
Carrier n c= A
by VECTSP_6:def 7;
A15:
(B \ A') \/ A' = B
by A1, XBOOLE_1:45;
(Carrier m) \/ (Carrier n) c= (B \ A') \/ A
by A13, A14, XBOOLE_1:13;
then
Carrier (m - n) c= B
by A12, A15, XBOOLE_1:1;
then reconsider o =
m - n as
Linear_Combination of
B by VECTSP_6:def 7;
B is
linearly-independent
by VECTSP_7:def 3;
then A16:
Carrier o = {}
by A11, VECTSP_7:def 1;
A' misses B \ A'
by XBOOLE_1:79;
then
Carrier (m - n) = (Carrier m) \/ (Carrier n)
by A13, A14, Th32, XBOOLE_1:64;
then
Carrier m = {}
by A16;
then
T .: (Carrier m) = {}
by RELAT_1:149;
hence
contradiction
by A7, A9, Th30, XBOOLE_1:3;
:: thesis: verum
end;
reconsider C = C as finite Subset of (im T) by Th12;
reconsider L = Lin C as strict Subspace of im T ;
for v being Element of (im T) holds v in L
proof
let v be
Element of
(im T);
:: thesis: v in L
A17:
v in im T
by STRUCT_0:def 5;
reconsider v' =
v as
Element of
W by VECTSP_4:18;
consider u being
Element of
V such that A18:
T . u = v'
by A17, Th13;
reconsider A' =
A as
Subset of
V by Th19;
V is_the_direct_sum_of Lin A',
Lin (B \ A')
by A1, Th33;
then A19:
(Omega). V = (Lin A') + (Lin (B \ A'))
by VECTSP_5:def 4;
u in (Omega). V
by STRUCT_0:def 5;
then consider u1,
u2 being
Element of
V such that A20:
u1 in Lin A'
and A21:
u2 in Lin (B \ A')
and A22:
u = u1 + u2
by A19, VECTSP_5:5;
A23:
T . u = (T . u1) + (T . u2)
by A22, MOD_2:def 5;
Lin A = ker T
by VECTSP_7:def 3;
then
u1 in ker T
by A20, VECTSP_9:21;
then
T . u1 = 0. W
by Th10;
then A24:
T . u = T . u2
by A23, RLVECT_1:10;
consider l being
Linear_Combination of
B \ A' such that A25:
u2 = Sum l
by A21, VECTSP_7:12;
A26:
T @ l is
Linear_Combination of
T .: (Carrier l)
by Th29;
A27:
Carrier l c= B \ A'
by VECTSP_6:def 7;
reconsider C' =
C as
Subset of
W ;
reconsider m =
T @ l as
Linear_Combination of
C' by A26, A27, RELAT_1:156, VECTSP_6:25;
ex
m being
Linear_Combination of
C' st
v = Sum m
then
v in Lin C'
by VECTSP_7:12;
hence
v in L
by VECTSP_9:21;
:: thesis: verum
end;
then A28:
Lin C = im T
by VECTSP_4:40;
reconsider C = C as linearly-independent Subset of (im T) by A6, VECTSP_9:16;
reconsider C = C as finite Basis of im T by A28, VECTSP_7:def 3;
A29:
nullity T = card A
by VECTSP_9:def 2;
A30:
rank T = card C
by VECTSP_9:def 2;
dim V =
card B
by VECTSP_9:def 2
.=
(rank T) + (nullity T)
by A2, A5, A29, A30, CARD_2:53, XBOOLE_1:79
;
hence
dim V = (rank T) + (nullity T)
; :: thesis: verum