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

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;

:: 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

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 V143(F,V) for Element of K16( the carrier of V);

existence
ex b₁ being Basis of V st b₁ is finite

proof end;

end;

registration

let F be Ring;
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 K16(K17( the carrier of V, the carrier of W));

existence
ex b₁ being Function of V,W st
( b₁ is additive & b₁ 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;

definition

let F be Ring;
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 )

proof end;

theorem Th8: :: RANKNULL:8

for F being Ring
for V, W 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 Ring
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 Ring;
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 b₁ being strict Subspace of V st [#] b₁ = { u where u is Element of V : T . u = 0. W }

proof end;

uniqueness
for b₁, b₂ being strict Subspace of V st [#] b₁ = { u where u is Element of V : T . u = 0. W } & [#] b₂ = { u where u is Element of V : T . u = 0. W } holds
b₁ = b₂ by VECTSP_4:29;

end;

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

theorem Th10: :: RANKNULL:10

for F being Ring
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 Ring;
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 b₁ being strict Subspace of W st [#] b₁ = T .: ([#] V)

proof end;

uniqueness
for b₁, b₂ being strict Subspace of W st [#] b₁ = T .: ([#] V) & [#] b₂ = T .: ([#] V) holds
b₁ = b₂ by VECTSP_4:29;

end;

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

theorem :: RANKNULL:11

for F being Ring
for V, W 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 Ring
for V, W 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 Ring
for V, W 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 Ring
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 Ring
for V, W 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 Ring
for V, W 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 Ring
for V, W 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;

:: combinations

theorem Th19: :: RANKNULL:19

for F being Ring
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;

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

proof end;

:: 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

proof end;

theorem Th22: :: RANKNULL:22

for F being Field
for V, W 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 for Element of K16( the carrier of V);

existence
ex b₁ being Subset of V st b₁ is linearly-dependent

proof end;

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;

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;

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

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 b₁ being Linear_Combination of W st
for w being Element of W holds b₁ . w = Sum (l .: (T " {w}))

proof end;

uniqueness
for b₁, b₂ being Linear_Combination of W st ( for w being Element of W holds b₁ . w = Sum (l .: (T " {w})) ) & ( for w being Element of W holds b₂ . w = Sum (l .: (T " {w})) ) holds
b₁ = b₂

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 b₆ being Linear_Combination of W holds
( b₆ = T @ l iff for w being Element of W holds b₆ . w = Sum (l .: (T " {w})) );

theorem Th29: :: RANKNULL:29

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 holds T @ l is Linear_Combination of T .: (Carrier l)

proof end;

theorem Th30: :: RANKNULL:30

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 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 V, W 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 V, W 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 V, W 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 V, W 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 V, W 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 X is linearly-dependent holds
ex l being Linear_Combination of X st
( Carrier l <> {} & Sum l = 0. V )

proof end;

:: "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 ;

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 V, W 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;

:: # is a right inverse of @

theorem Th43: :: RANKNULL:43

for F being Field
for V, W 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;

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

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

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;