:: The Rank+Nullity Theorem
:: by Jesse Alama
::
:: Received July 31, 2007
:: Copyright (c) 2007-2016 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies FUNCT_1, RELAT_1, TARSKI, STRUCT_0, SUBSET_1, XBOOLE_0, VECTSP_1,
RLVECT_5, FINSET_1, RLVECT_3, LOPBAN_1, ARYTM_3, SUPINF_2, CARD_1,
RLSUB_1, FUNCT_2, ARYTM_1, MESFUNC1, VECTSP10, RLVECT_2, FUNCT_4,
REALSET1, FUNCOP_1, QC_LANG1, CARD_3, RLSUB_2, FINSEQ_1, VALUED_1, NAT_1,
XXREAL_0, PARTFUN1, PBOOLE, RANKNULL, MSSUBFAM, UNIALG_1;
notations TARSKI, XBOOLE_0, SUBSET_1, DOMAIN_1, RELAT_1, RELSET_1, FUNCT_1,
ORDINAL1, NAT_1, NUMBERS, FUNCOP_1, PARTFUN1, FUNCT_2, FUNCT_4, XCMPLX_0,
XXREAL_0, CARD_1, FINSET_1, FINSEQ_1, FINSEQOP, STRUCT_0, RLVECT_1,
RLVECT_2, VECTSP_1, FUNCT_7, VECTSP_4, VECTSP_5, VECTSP_6, VECTSP_7,
MOD_2, MATRLIN, VECTSP_9, LOPBAN_1;
constructors NAT_1, FINSEQOP, HAHNBAN, VECTSP_6, VECTSP_7, MOD_2, VECTSP_9,
REALSET1, RLVECT_2, WELLORD2, LOPBAN_1, VECTSP_5, FUNCT_7, FUNCT_4,
XXREAL_0, MATRLIN, RELSET_1;
registrations RELAT_1, FUNCT_1, STRUCT_0, CARD_1, FINSET_1, VECTSP_9,
XBOOLE_0, MATRLIN, FUNCOP_1, ORDINAL1, XREAL_0, SUBSET_1, RELSET_1;
requirements BOOLE, SUBSET, NUMERALS, ARITHM;
begin
theorem :: 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;
:: If a function is one-to-one on a set X, then it is one-to-one on
:: any subset of X.
theorem :: RANKNULL:2
for f being Function, X,Y being set st X c= Y & f|Y is one-to-one
holds f|X is one-to-one;
theorem :: RANKNULL:3
for V being 1-sorted, X,Y being Subset of V holds X meets Y iff
ex v being Element of V st v in X & v in Y;
reserve F for Field,
V,W for VectSp of F;
registration
let F be Field, V be finite-dimensional VectSp of F;
cluster finite for Basis of V;
end;
registration
let F be Field, V,W be VectSp of F;
cluster additive homogeneous for Function of V,W;
end;
theorem :: RANKNULL:4
[#]V is finite implies V is finite-dimensional;
theorem :: RANKNULL:5
for V being finite-dimensional VectSp of F st card ([#]V) = 1 holds dim V = 0
;
theorem :: RANKNULL:6
card ([#]V) = 2 implies dim V = 1;
begin :: Basic facts of linear transformations
definition
let F be Field, V,W be VectSp of F;
mode linear-transformation of V,W is additive homogeneous Function of V,W;
end;
reserve T for linear-transformation of V,W;
theorem :: RANKNULL:7
for V, W being non empty 1-sorted, T being Function of V,W holds
dom T = [#]V & rng T c= [#]W;
theorem :: RANKNULL:8
for x,y being Element of V holds T.x - T.y = T.(x - y);
theorem :: RANKNULL:9
T.(0.V) = 0.W;
definition
let F be Field, V,W be VectSp of F, T be linear-transformation of V,W;
func ker T -> strict Subspace of V means
:: RANKNULL:def 1
[#]it = { u where u is Element of V : T.u = 0.W };
end;
theorem :: RANKNULL:10
for x being Element of V holds x in ker T iff T.x = 0.W;
definition
let V,W be non empty 1-sorted, T be Function of V,W, X be Subset of V;
redefine func T .: X -> Subset of W;
end;
definition
let F be Field, V,W be VectSp of F, T be linear-transformation of V,W;
func im T -> strict Subspace of W means
:: RANKNULL:def 2
[#]it = T .: [#]V;
end;
theorem :: RANKNULL:11
0.V in ker T;
theorem :: RANKNULL:12
for X being Subset of V holds T .: X is Subset of im T;
theorem :: RANKNULL:13
for y being Element of W holds y in im T iff ex x being Element
of V st y = T.x;
theorem :: RANKNULL:14
for x being Element of ker T holds T.x = 0.W;
theorem :: RANKNULL:15
T is one-to-one implies ker T = (0).V;
theorem :: RANKNULL:16
for V being finite-dimensional VectSp of F holds dim ((0).V) = 0;
theorem :: RANKNULL:17
for x,y being Element of V st T.x = T.y holds x - y in ker T;
theorem :: RANKNULL:18
for A being Subset of V, x,y being Element of V st x - y in Lin
A holds x in Lin (A \/ {y});
begin :: Some basic facts about linearly independent subsets and linear
:: combinations
theorem :: RANKNULL:19
for X being Subset of V st V is Subspace of W holds X is Subset of W;
:: A linearly independent set is a basis of its linear span.
theorem :: RANKNULL:20
for A being Subset of V st A is linearly-independent holds A is
Basis of Lin A;
:: Adjoining an element x to A that is already in its linear span
:: results in a linearly dependent set.
theorem :: RANKNULL:21
for A being Subset of V, x being Element of V st x in Lin A &
not x in A holds A \/ {x} is linearly-dependent;
theorem :: RANKNULL:22
for A being Subset of V, B being Basis of V st A is Basis of ker
T & A c= B holds T|(B \ A) is one-to-one;
theorem :: RANKNULL:23
for A being Subset of V, l being Linear_Combination of A, x being
Element of V, a being Element of F holds l +* (x,a) is Linear_Combination of A
\/ {x};
definition
let V be 1-sorted, X be Subset of V;
func V \ X -> Subset of V equals
:: RANKNULL:def 3
[#]V \ X;
end;
definition
let F be Field, V be VectSp of F, l be Linear_Combination of V, X be Subset
of V;
redefine func l .: X -> Subset of F;
end;
reserve l for Linear_Combination of V;
registration
let F be Field, V be VectSp of F;
cluster linearly-dependent for Subset of V;
end;
:: Restricting a linear combination to a given set
definition
let F be Field, V be VectSp of F, l be Linear_Combination of V, A be Subset
of V;
func l!A -> Linear_Combination of A equals
:: RANKNULL:def 4
(l|A) +* ((V \ A) --> 0.F);
end;
theorem :: RANKNULL:24
l = l!Carrier l;
theorem :: RANKNULL:25
for A being Subset of V, v being Element of V st v in A holds (l !A).v = l.v;
theorem :: RANKNULL:26
for A being Subset of V, v being Element of V st not v in A
holds (l!A).v = 0.F;
theorem :: RANKNULL:27
for A,B being Subset of V, l being Linear_Combination of B st A
c= B holds l = (l!A) + (l!(B\A));
registration
let F be Field, V be VectSp of F, l be Linear_Combination of V, X be Subset
of V;
cluster l .: X -> finite;
end;
definition
let V,W be non empty 1-sorted, T be Function of V,W, X be Subset of W;
redefine func T"X -> Subset of V;
end;
theorem :: RANKNULL:28
for X being Subset of V st X misses Carrier l holds l .: X c= { 0.F};
:: 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, V,W be VectSp of F, l be Linear_Combination of V, T be
linear-transformation of V,W;
func T@l -> Linear_Combination of W means
:: RANKNULL:def 5
for w being Element of W holds it.w = Sum (l .: (T"{w}));
end;
theorem :: RANKNULL:29
T@l is Linear_Combination of T .: (Carrier l);
theorem :: RANKNULL:30
Carrier (T@l) c= T .: (Carrier l);
theorem :: RANKNULL:31
for l,m being Linear_Combination of V st (Carrier l) misses (
Carrier m) holds Carrier (l + m) = (Carrier l) \/ (Carrier m);
theorem :: RANKNULL:32
for l,m being Linear_Combination of V st (Carrier l) misses (
Carrier m) holds Carrier (l - m) = (Carrier l) \/ (Carrier m);
theorem :: RANKNULL:33
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);
theorem :: RANKNULL:34
for A being Subset of V, l being Linear_Combination of A, 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;
theorem :: RANKNULL:35
for X being Subset of V st X misses Carrier l & X <> {} holds l .: X = {0.F};
theorem :: RANKNULL:36
for w being Element of W st w in Carrier (T@l) holds T"{w} meets Carrier l;
theorem :: RANKNULL:37
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;
theorem :: RANKNULL:38
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);
theorem :: RANKNULL:39
T|(Carrier l) is one-to-one implies T .: (Carrier l) = Carrier ( T@l);
theorem :: RANKNULL:40
for A being Subset of V, B being Basis of V, l being
Linear_Combination of B \ A st A is Basis of ker T & A c= B holds T.(Sum l) =
Sum (T@l);
theorem :: RANKNULL:41
for X being Subset of V st X is linearly-dependent holds ex l
being Linear_Combination of X st Carrier l <> {} & Sum l = 0.V;
:: "Pulling back" a linear combination from the image space of a
:: linear transformation to the base space.
definition
let F be Field, V,W be VectSp of F, X be Subset of V, T be
linear-transformation of V,W, l be Linear_Combination of T .: X;
assume
T|X is one-to-one;
func T#l -> Linear_Combination of X equals
:: RANKNULL:def 6
(l*T) +* ((V \ X) --> 0.F);
end;
theorem :: RANKNULL:42
for X being Subset of V, l being Linear_Combination of T .: X, v
being Element of V st v in X & T|X is one-to-one holds (T#l).v = l.(T.v);
:: # is a right inverse of @
theorem :: RANKNULL:43
for X being Subset of V, l being Linear_Combination of T .: X st
T|X is one-to-one holds T@(T#l) = l;
begin :: The rank+nullity theorem
definition
let F be Field, V,W be finite-dimensional VectSp of F, T be
linear-transformation of V,W;
func rank(T) -> Nat equals
:: RANKNULL:def 7
dim (im T);
func nullity(T) -> Nat equals
:: RANKNULL:def 8
dim (ker T);
end;
::$N Rank-nullity theorem
theorem :: RANKNULL:44
for V,W being finite-dimensional VectSp of F, T being
linear-transformation of V,W holds dim V = rank(T) + nullity(T);
theorem :: RANKNULL:45
for V,W being finite-dimensional VectSp of F, T being
linear-transformation of V,W st T is one-to-one holds dim V = rank T;