:: The Rank+Nullity Theorem
::  by Jesse Alama
::
:: Received July 31, 2007
:: Copyright (c) 2007-2021 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, RLVECT_1,
      ALGSTR_0, FUNCSDOM;
 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, RELSET_1, VECTSP_4;
 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 K for Ring,
  V1,W1 for VectSp of K;
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 Ring;
  let 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 Ring, 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 F being Ring,
      V, W being VectSp of F,
      T being linear-transformation of V,W
  for x,y being Element of V holds T.x - T.y = T.(x - y);

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

definition
  let F be Ring, 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 F being Ring,
      V, W being VectSp of F,
      T being linear-transformation of V,W
  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 Ring, 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
  for F being Ring,
      V, W being VectSp of F,
      T being linear-transformation of V,W holds
  0.V in ker T;

theorem :: RANKNULL:12
  for F being Ring, V, W being VectSp of F,
      T being linear-transformation of V,W holds
  for X being Subset of V holds T .: X is Subset of im T;

theorem :: RANKNULL:13
  for F being Ring, V, W being VectSp of F,
      T being linear-transformation of V,W holds
  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 F being Ring, V, W being VectSp of F,
      T being linear-transformation of V,W
  for x being Element of ker T holds T.x = 0.W;

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

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

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

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