:: The Rank+Nullity Theorem
:: by Jesse Alama
::
:: Received July 31, 2007
:: Copyright (c) 2007-2012 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
proofend;

:: If a function is one-to-one on a set X, then it is one-to-one on
:: any subset of X.
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
proofend;

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 ) )
proofend;

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

registration
let F be Field;
let V, W be VectSp of F;
cluster Relation-like the carrier of V -defined the carrier of W -valued Function-like quasi_total additive homogeneous for 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 )
proofend;
end;

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

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

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

begin

definition
let F be Field;
let V, W be VectSp of F;
mode linear-transformation of V,W is additive homogeneous 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 )
proofend;

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)
proofend;

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
proofend;

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  }
proofend;
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:29;
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 )
proofend;

definition
let V, W be non empty 1-sorted ;
let T be Function of V,W;
let X be Subset of V;
:: original:.:
redefine funcT .: X ->  Subset of W;
coherence
 T .: X is Subset of W
proofend;
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)
proofend;
uniqueness
 for b1, b2 being strict Subspace of W st [#] b1 = T .: ([#] V) & [#] b2 = T .: ([#] V) holds
b1 = b2 by VECTSP_4:29;
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
proofend;

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)
proofend;

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 )
proofend;

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
proofend;

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
proofend;

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

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
proofend;

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})
proofend;

begin

:: combinations
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
proofend;

:: A linearly independent set is a basis of its linear span.
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
proofend;

:: Adjoining an element x to A that is already in its linear span
:: results in a linearly dependent set.
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
A \/ {x} is linearly-dependent
proofend;

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
proofend;

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}
proofend;

definition
let V be 1-sorted ;
let X be Subset of V;
funcV \ 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 funcl .: X ->  Subset of F;
coherence
 l .: X is Subset of F
proofend;
end;

registration
let F be Field;
let V be VectSp of F;
cluster linearly-dependent for Element of K6( the carrier of V);
existence
 ex b1 being Subset of V st b1 is linearly-dependent
proofend;
end;

:: Restricting a linear combination to a given set
definition
let F be Field;
let V be VectSp of F;
let l be Linear_Combination of V;
let A be Subset of V;
funcl ! 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
proofend;
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)
proofend;

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
proofend;

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
proofend;

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
proofend;

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))
proofend;

registration
let F be Field;
let V be VectSp of F;
let l be Linear_Combination of V;
let X be Subset of V;
clusterl .: 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 funcT " X ->  Subset of V;
coherence
 T " X is Subset of V
proofend;
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)}
proofend;

:: The image of a linear combination under a linear transformation:
::
:: T(a1*v1 + a2*v2 + ... + an*vn)
:: = a1*T(v1) + a2*T(v2) + ... + an*T(vn).
::
:: Linear combinations are represented as functions from the space to
:: the underlying field having finite support, so to define a new
:: linear combination it is enough to say what its values are for the
:: elements of W and to prove that its support is finite.
::
:: The only difficulty is that some values T(vi) and T(vj) may be
:: equal. In this case, the new linear combination should be the sum
:: of the coefficients ai and aj, i.e., l(vi) and l(vj).
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;
funcT @ 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}))
proofend;
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
proofend;
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)
proofend;

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)
proofend;

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)
proofend;

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)
proofend;

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)
proofend;

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 )
proofend;

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 &amp; X <> {} holds
l .: X = {(0. F)}
proofend;

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
proofend;

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 &amp; v in Carrier l holds
(T @ l) . (T . v) = l . v
proofend;

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 &amp; T | (Carrier l) is one-to-one holds
T * (l (#) G) = (T @ l) (#) (T * G)
proofend;

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)
proofend;

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 &amp; A c= B holds
T . (Sum l) = Sum (T @ l)
proofend;

theorem Th41: :: RANKNULL:41
for F being Field
for V being VectSp of F
for X being Subset of V st X is linearly-dependent holds
ex l being Linear_Combination of X st
( Carrier l <> {} &amp; Sum l = 0. V )
proofend;

:: "Pulling back" a linear combination from the image space of a
:: linear transformation to the base space.
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 ;
funcT # 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
proofend;
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 &amp; T | X is one-to-one holds
(T # l) . v = l . (T . v)
proofend;

:: # is a right inverse of @
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
proofend;

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);

:: [WP: ] Rank-nullity_theorem
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)
proofend;

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
proofend;