let F be Field; 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; for T being linear-transformation of V,W holds dim V = (rank T) + (nullity T)
let T be linear-transformation of V,W; dim 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 Th19;
consider B being Basis of V such that
A1:
the finite Basis of (ker T) c= B
by VECTSP_9:13;
reconsider B = B as finite Subset of V by VECTSP_9:20;
reconsider X = B \ A9 as finite Subset of B by XBOOLE_1:36;
reconsider X = X as finite Subset of V ;
A2:
B = the finite Basis of (ker T) \/ X
by A1, XBOOLE_1:45;
reconsider B = B as finite Basis of V ;
reconsider A = the finite Basis of (ker T) as finite Basis of (ker T) ;
reconsider C = T .: X as finite Subset of W ;
A3:
T | X is one-to-one
by A1, Th22;
A4:
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
by Th41;
ex
m being
Linear_Combination of
X st
l = T @ m
then consider m being
Linear_Combination of
B \ A9 such that A7:
l = T @ m
;
T . (Sum m) = 0. W
by A1, A6, A7, 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 A9
by VECTSP_9:17;
then consider n being
Linear_Combination of
A9 such that A8:
Sum m = Sum n
by VECTSP_7:7;
A9:
(
Carrier (m - n) c= (Carrier m) \/ (Carrier n) &
(B \ A9) \/ A9 = B )
by A1, VECTSP_6:41, XBOOLE_1:45;
A10:
(
Carrier m c= B \ A9 &
Carrier n c= A )
by VECTSP_6:def 4;
then
(Carrier m) \/ (Carrier n) c= (B \ A9) \/ A
by XBOOLE_1:13;
then
Carrier (m - n) c= B
by A9;
then reconsider o =
m - n as
Linear_Combination of
B by VECTSP_6:def 4;
A11:
B is
linearly-independent
by VECTSP_7:def 3;
(Sum m) - (Sum n) = 0. V
by A8, VECTSP_1:19;
then
Sum (m - n) = 0. V
by VECTSP_6:47;
then A12:
Carrier o = {}
by A11, VECTSP_7:def 1;
A9 misses B \ A9
by XBOOLE_1:79;
then
Carrier (m - n) = (Carrier m) \/ (Carrier n)
by A10, Th32, XBOOLE_1:64;
then
Carrier m = {}
by A12;
then
T .: (Carrier m) = {}
;
hence
contradiction
by A5, A7, Th30, XBOOLE_1:3;
verum
end;
dom T = [#] V
by Th7;
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 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
reconsider A9 =
A as
Subset of
V by Th19;
let v be
Element of
(im T);
v in L
reconsider v9 =
v as
Element of
W by VECTSP_4:10;
reconsider C9 =
C as
Subset of
W ;
v in im T
;
then consider u being
Element of
V such that A14:
T . u = v9
by Th13;
V is_the_direct_sum_of Lin A9,
Lin (B \ A9)
by A1, Th33;
then A15:
(Omega). V = (Lin A9) + (Lin (B \ A9))
by VECTSP_5:def 4;
u in (Omega). V
;
then consider u1,
u2 being
Element of
V such that A16:
u1 in Lin A9
and A17:
u2 in Lin (B \ A9)
and A18:
u = u1 + u2
by A15, VECTSP_5:1;
consider l being
Linear_Combination of
B \ A9 such that A19:
u2 = Sum l
by A17, VECTSP_7:7;
Lin A = ker T
by VECTSP_7:def 3;
then
u1 in ker T
by A16, VECTSP_9:17;
then A20:
T . u1 = 0. W
by Th10;
(
T @ l is
Linear_Combination of
T .: (Carrier l) &
Carrier l c= B \ A9 )
by Th29, VECTSP_6:def 4;
then reconsider m =
T @ l as
Linear_Combination of
C9 by RELAT_1:123, VECTSP_6:4;
T . u = (T . u1) + (T . u2)
by A18, VECTSP_1:def 20;
then A21:
T . u = T . u2
by A20, RLVECT_1:4;
ex
m being
Linear_Combination of
C9 st
v = Sum m
then
v in Lin C9
by VECTSP_7:7;
hence
v in L
by VECTSP_9:17;
verum
end;
then A22:
Lin C = im T
by VECTSP_4:32;
reconsider C = C as linearly-independent Subset of (im T) by A4, VECTSP_9:12;
reconsider C = C as finite Basis of (im T) by A22, VECTSP_7:def 3;
A23:
( nullity T = card A & rank T = card C )
by VECTSP_9:def 1;
dim V =
card B
by VECTSP_9:def 1
.=
(rank T) + (nullity T)
by A2, A13, A23, CARD_2:40, XBOOLE_1:79
;
hence
dim V = (rank T) + (nullity T)
; verum