:: The Rank+Nullity Theorem
:: by Jesse Alama
::
:: Received July 31, 2007
:: Copyright (c) 2007-2011 Association of Mizar Users


begin

theorem Th1: :: RANKNULL:1
for f, g being Function st g is one-to-one & f | (rng g) is one-to-one & rng g c= dom f holds
f * g is one-to-one
proof end;

theorem Th2: :: RANKNULL:2
for f being Function
for X, Y being set st X c= Y & f | Y is one-to-one holds
f | X is one-to-one
proof end;

theorem Th3: :: RANKNULL:3
for V being 1-sorted
for X, Y being Subset of V holds
( X meets Y iff ex v being Element of V st
( v in X & v in Y ) )
proof end;

registration
let F be Field;
let V be finite-dimensional VectSp of F;
cluster finite Basis of V;
existence
ex b1 being Basis of V st b1 is finite
proof end;
end;

registration
let F be Field;
let V, W be VectSp of F;
cluster Relation-like Function-like quasi_total homogeneous additive Element of K6(K7( the carrier of V, the carrier of W));
existence
ex b1 being Function of V,W st
( b1 is additive & b1 is homogeneous )
proof end;
end;

theorem Th4: :: RANKNULL:4
for F being Field
for V being VectSp of F st [#] V is finite holds
V is finite-dimensional
proof end;

theorem :: RANKNULL:5
for F being Field
for V being finite-dimensional VectSp of F st card ([#] V) = 1 holds
dim V = 0
proof end;

theorem :: RANKNULL:6
for F being Field
for V being VectSp of F st card ([#] V) = 2 holds
dim V = 1
proof end;

begin

definition
let F be Field;
let V, W be VectSp of F;
mode linear-transformation of V,W is homogeneous additive Function of V,W;
end;

theorem Th7: :: RANKNULL:7
for V, W being non empty 1-sorted
for T being Function of V,W holds
( dom T = [#] V & rng T c= [#] W )
proof end;

theorem Th8: :: RANKNULL:8
for F being Field
for W, V 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)
proof end;

theorem Th9: :: RANKNULL:9
for F being Field
for V, W being VectSp of F
for T being linear-transformation of V,W holds T . (0. V) = 0. W
proof end;

definition
let F be Field;
let V, W be VectSp of F;
let T be linear-transformation of V,W;
func ker T -> strict Subspace of V means :Def1: :: RANKNULL:def 1
 [#] it = { u where u is Element of V : T . u = 0. W } ;
existence
ex b1 being strict Subspace of V st [#] b1 = { u where u is Element of V : T . u = 0. W }
proof end;
uniqueness
for b1, b2 being strict Subspace of V st [#] b1 = { u where u is Element of V : T . u = 0. W } & [#] b2 = { u where u is Element of V : T . u = 0. W } holds
b1 = b2 by VECTSP_4:37;
end;

:: deftheorem Def1 defines ker RANKNULL:def 1 :
for F being Field
for V, W being VectSp of F
for T being linear-transformation of V,W
for b5 being strict Subspace of V holds
( b5 = ker T iff [#] b5 = { u where u is Element of V : T . u = 0. W } );

theorem Th10: :: RANKNULL:10
for F being Field
for V, W being VectSp of F
for T being linear-transformation of V,W
for x being Element of V holds
( x in ker T iff T . x = 0. W )
proof end;

definition
let V, W be non empty 1-sorted ;
let T be Function of V,W;
let X be Subset of V;
:: original: .:
redefine func T .: X -> Subset of W;
coherence
T .: X is Subset of W
proof end;
end;

definition
let F be Field;
let V, W be VectSp of F;
let T be linear-transformation of V,W;
func im T -> strict Subspace of W means :Def2: :: RANKNULL:def 2
 [#] it = T .: ([#] V);
existence
ex b1 being strict Subspace of W st [#] b1 = T .: ([#] V)
proof end;
uniqueness
for b1, b2 being strict Subspace of W st [#] b1 = T .: ([#] V) & [#] b2 = T .: ([#] V) holds
b1 = b2 by VECTSP_4:37;
end;

:: deftheorem Def2 defines im RANKNULL:def 2 :
for F being Field
for V, W being VectSp of F
for T being linear-transformation of V,W
for b5 being strict Subspace of W holds
( b5 = im T iff [#] b5 = T .: ([#] V) );

theorem :: RANKNULL:11
for F being Field
for W, V being VectSp of F
for T being linear-transformation of V,W holds 0. V in ker T
proof end;

theorem Th12: :: RANKNULL:12
for F being Field
for W, V being VectSp of F
for T being linear-transformation of V,W
for X being Subset of V holds T .: X is Subset of (im T)
proof end;

theorem Th13: :: RANKNULL:13
for F being Field
for W, V being VectSp of F
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 )
proof end;

theorem :: RANKNULL:14
for F being Field
for V, W being VectSp of F
for T being linear-transformation of V,W
for x being Element of (ker T) holds T . x = 0. W
proof end;

theorem Th15: :: RANKNULL:15
for F being Field
for W, V being VectSp of F
for T being linear-transformation of V,W st T is one-to-one holds
ker T = (0). V
proof end;

theorem Th16: :: RANKNULL:16
for F being Field
for V being finite-dimensional VectSp of F holds dim ((0). V) = 0
proof end;

theorem Th17: :: RANKNULL:17
for F being Field
for W, V being VectSp of F
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
proof end;

theorem Th18: :: RANKNULL:18
for F being Field
for V being VectSp of F
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})
proof end;

begin

theorem Th19: :: RANKNULL:19
for F being Field
for V, W being VectSp of F
for X being Subset of V st V is Subspace of W holds
X is Subset of W
proof end;

theorem Th20: :: RANKNULL:20
for F being Field
for V being VectSp of F
for A being Subset of V st A is linearly-independent holds
A is Basis of Lin A
proof end;

theorem Th21: :: RANKNULL:21
for F being Field
for V being VectSp of F
for A being Subset of V
for x being Element of V st x in Lin A & not x in A holds
not A \/ {x} is linearly-independent
proof end;

theorem Th22: :: RANKNULL:22
for F being Field
for W, V being VectSp of F
for T being linear-transformation of V,W
for A being Subset of V
for B being Basis of V st A is Basis of ker T & A c= B holds
T | (B \ A) is one-to-one
proof end;

theorem :: RANKNULL:23
for F being Field
for V being VectSp of F
for A being Subset of V
for l being Linear_Combination of A
for x being Element of V
for a being Element of F holds l +* (x,a) is Linear_Combination of A \/ {x}
proof end;

definition
let V be 1-sorted ;
let X be Subset of V;
func V \ X -> Subset of V equals :: RANKNULL:def 3
([#] V) \ X;
coherence
([#] V) \ X is Subset of V ;
end;

:: deftheorem defines \ RANKNULL:def 3 :
for V being 1-sorted
for X being Subset of V holds V \ X = ([#] V) \ X;

definition
let F be Field;
let V be VectSp of F;
let l be Linear_Combination of V;
let X be Subset of V;
:: original: .:
redefine func l .: X -> Subset of F;
coherence
l .: X is Subset of F
proof end;
end;

registration
let F be Field;
let V be VectSp of F;
cluster linearly-dependent Element of K6( the carrier of V);
existence
not for b1 being Subset of V holds b1 is linearly-independent
proof end;
end;

definition
let F be Field;
let V be VectSp of F;
let l be Linear_Combination of V;
let A be Subset of V;
func l ! A -> Linear_Combination of A equals :: RANKNULL:def 4
(l | A) +* ((V \ A) --> (0. F));
coherence
(l | A) +* ((V \ A) --> (0. F)) is Linear_Combination of A
proof end;
end;

:: deftheorem defines ! RANKNULL:def 4 :
for F being Field
for V being VectSp of F
for l being Linear_Combination of V
for A being Subset of V holds l ! A = (l | A) +* ((V \ A) --> (0. F));

theorem Th24: :: RANKNULL:24
for F being Field
for V being VectSp of F
for l being Linear_Combination of V holds l = l ! (Carrier l)
proof end;

Lm1: for F being Field
for V being VectSp of F
for l being Linear_Combination of V
for X being Subset of V holds l .: X is finite
proof end;

theorem Th25: :: RANKNULL:25
for F being Field
for V being VectSp of F
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: :: RANKNULL:26
for F being Field
for V being VectSp of F
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. F
proof end;

theorem Th27: :: RANKNULL:27
for F being Field
for V being VectSp of F
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 F be Field;
let V be VectSp of F;
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;

definition
let V, W be non empty 1-sorted ;
let T be Function of V,W;
let X be Subset of W;
:: original: "
redefine func T " X -> Subset of V;
coherence
T " X is Subset of V
proof end;
end;

theorem Th28: :: RANKNULL:28
for F being Field
for V being VectSp of F
for l being Linear_Combination of V
for X being Subset of V st X misses Carrier l holds
l .: X c= {(0. F)}
proof end;

definition
let F be Field;
let V, W be VectSp of F;
let l be Linear_Combination of V;
let T be linear-transformation of V,W;
func T @ l -> Linear_Combination of W means :Def5: :: RANKNULL:def 5
 for w being Element of W holds it . w = Sum (l .: (T " {w}));
existence
ex b1 being Linear_Combination of W st
for w being Element of W holds b1 . w = Sum (l .: (T " {w}))
proof end;
uniqueness
for b1, b2 being Linear_Combination of W st ( for w being Element of W holds b1 . w = Sum (l .: (T " {w})) ) & ( for w being Element of W holds b2 . w = Sum (l .: (T " {w})) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def5 defines @ RANKNULL:def 5 :
for F being Field
for V, W being VectSp of F
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 for w being Element of W holds b6 . w = Sum (l .: (T " {w})) );

theorem Th29: :: RANKNULL:29
for F being Field
for W, V being VectSp of F
for T being linear-transformation of V,W
for l being Linear_Combination of V holds T @ l is Linear_Combination of T .: (Carrier l)
proof end;

theorem Th30: :: RANKNULL:30
for F being Field
for W, V being VectSp of F
for T being linear-transformation of V,W
for l being Linear_Combination of V holds Carrier (T @ l) c= T .: (Carrier l)
proof end;

theorem Th31: :: RANKNULL:31
for F being Field
for V being VectSp of F
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: :: RANKNULL:32
for F being Field
for V being VectSp of F
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 Th33: :: RANKNULL:33
for F being Field
for V being VectSp of F
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 Th34: :: RANKNULL:34
for F being Field
for W, V being VectSp of F
for T being linear-transformation of V,W
for A being Subset of V
for l being Linear_Combination of A
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 Th35: :: RANKNULL:35
for F being Field
for V being VectSp of F
for l being Linear_Combination of V
for X being Subset of V st X misses Carrier l & X <> {} holds
l .: X = {(0. F)}
proof end;

theorem Th36: :: RANKNULL:36
for F being Field
for V, W being VectSp of F
for T being linear-transformation of V,W
for l being Linear_Combination of V
for w being Element of W st w in Carrier (T @ l) holds
T " {w} meets Carrier l
proof end;

theorem Th37: :: RANKNULL:37
for F being Field
for W, V being VectSp of F
for T being linear-transformation of V,W
for l being Linear_Combination of V
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: :: RANKNULL:38
for F being Field
for W, V being VectSp of F
for T being linear-transformation of V,W
for l being Linear_Combination of V
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: :: RANKNULL:39
for F being Field
for W, V being VectSp of F
for T being linear-transformation of V,W
for l being Linear_Combination of V st T | (Carrier l) is one-to-one holds
T .: (Carrier l) = Carrier (T @ l)
proof end;

theorem Th40: :: RANKNULL:40
for F being Field
for W, V being VectSp of F
for T being linear-transformation of V,W
for A being Subset of V
for B being Basis of V
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 Th41: :: RANKNULL:41
for F being Field
for V being VectSp of F
for X being Subset of V st not X is linearly-independent holds
ex l being Linear_Combination of X st
( Carrier l <> {} & Sum l = 0. V )
proof end;

definition
let F be Field;
let V, W be VectSp of F;
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: :: RANKNULL:def 6
(l * T) +* ((V \ X) --> (0. F));
coherence
(l * T) +* ((V \ X) --> (0. F)) is Linear_Combination of X
proof end;
end;

:: deftheorem Def6 defines # RANKNULL:def 6 :
for F being Field
for V, W being VectSp of F
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) +* ((V \ X) --> (0. F));

theorem Th42: :: RANKNULL:42
for F being Field
for W, V being VectSp of F
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;

theorem Th43: :: RANKNULL:43
for F being Field
for W, V being VectSp of F
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;

begin

definition
let F be Field;
let V, W be finite-dimensional VectSp of F;
let T be linear-transformation of V,W;
func rank T -> Nat equals :: RANKNULL:def 7
 dim (im T);
coherence
dim (im T) is Nat ;
func nullity T -> Nat equals :: RANKNULL:def 8
 dim (ker T);
coherence
dim (ker T) is Nat ;
end;

:: deftheorem defines rank RANKNULL:def 7 :
for F being Field
for V, W being finite-dimensional VectSp of F
for T being linear-transformation of V,W holds rank T = dim (im T);

:: deftheorem defines nullity RANKNULL:def 8 :
for F being Field
for V, W being finite-dimensional VectSp of F
for T being linear-transformation of V,W holds nullity T = dim (ker T);

theorem Th44: :: RANKNULL:44
for F being 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)
proof end;

theorem :: RANKNULL:45
for F being Field
for V, W being finite-dimensional VectSp of F
for T being linear-transformation of V,W st T is one-to-one holds
dim V = rank T
proof end;