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

f * g 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 ) )

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;

existence

ex b_{1} being Basis of V st b_{1} is finite

end;
let V be finite-dimensional VectSp of F;

existence

ex b

proof end;

registration

let F be Field;

let V, W be VectSp of F;

ex b_{1} being Function of V,W st

( b_{1} is additive & b_{1} is homogeneous )

end;
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 b

( b

proof end;

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;
let V, W be VectSp of F;

mode linear-transformation of V,W is additive homogeneous Function of V,W;

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 )

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)

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

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;

ex b_{1} being strict Subspace of V st [#] b_{1} = { u where u is Element of V : T . u = 0. W }

for b_{1}, b_{2} being strict Subspace of V st [#] b_{1} = { u where u is Element of V : T . u = 0. W } & [#] b_{2} = { u where u is Element of V : T . u = 0. W } holds

b_{1} = b_{2}
by VECTSP_4:29;

end;
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 [#] it = { u where u is Element of V : T . u = 0. W } ;

ex b

proof end;

uniqueness for b

b

:: 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 b_{5} being strict Subspace of V holds

( b_{5} = ker T iff [#] b_{5} = { u where u is Element of V : T . u = 0. W } );

for F being Field

for V, W being VectSp of F

for T being linear-transformation of V,W

for b

( b

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 )

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

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

definition

let F be Field;

let V, W be VectSp of F;

let T be linear-transformation of V,W;

existence

ex b_{1} being strict Subspace of W st [#] b_{1} = T .: ([#] V)

for b_{1}, b_{2} being strict Subspace of W st [#] b_{1} = T .: ([#] V) & [#] b_{2} = T .: ([#] V) holds

b_{1} = b_{2}
by VECTSP_4:29;

end;
let V, W be VectSp of F;

let T be linear-transformation of V,W;

existence

ex b

proof end;

uniqueness for b

b

:: 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 b_{5} being strict Subspace of W holds

( b_{5} = im T iff [#] b_{5} = T .: ([#] V) );

for F being Field

for V, W being VectSp of F

for T being linear-transformation of V,W

for b

( b

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

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)

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 )

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

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

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

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

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

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

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

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.

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

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

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}

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;

:: deftheorem defines \ RANKNULL:def 3 :

for V being 1-sorted

for X being Subset of V holds V \ X = ([#] V) \ X;

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

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

registration

let F be Field;

let V be VectSp of F;

existence

ex b_{1} being Subset of V st b_{1} is linearly-dependent

end;
let V be VectSp of F;

existence

ex b

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

coherence

(l | A) +* ((V \ A) --> (0. F)) is Linear_Combination of A

end;
let V be VectSp of F;

let l be Linear_Combination of V;

let A be Subset of V;

coherence

(l | A) +* ((V \ A) --> (0. F)) is Linear_Combination of A

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

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)

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

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

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

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;

coherence

l .: X is finite by Lm1;

end;
let V be VectSp of F;

let l be Linear_Combination of V;

let X be Subset of V;

coherence

l .: X is finite by Lm1;

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

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

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

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

::

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

ex b_{1} being Linear_Combination of W st

for w being Element of W holds b_{1} . w = Sum (l .: (T " {w}))

for b_{1}, b_{2} being Linear_Combination of W st ( for w being Element of W holds b_{1} . w = Sum (l .: (T " {w})) ) & ( for w being Element of W holds b_{2} . w = Sum (l .: (T " {w})) ) holds

b_{1} = b_{2}

end;
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 for w being Element of W holds it . w = Sum (l .: (T " {w}));

ex b

for w being Element of W holds b

proof end;

uniqueness for b

b

proof 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_{6} being Linear_Combination of W holds

( b_{6} = T @ l iff for w being Element of W holds b_{6} . w = Sum (l .: (T " {w})) );

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

( b

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)

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)

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)

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)

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)

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 )

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

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

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

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)

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)

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)

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 X is linearly-dependent holds

ex l being Linear_Combination of X st

( Carrier l <> {} & Sum l = 0. V )

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.

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

(l * T) +* ((V \ X) --> (0. F)) is Linear_Combination of X

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

(l * T) +* ((V \ X) --> (0. F)) is Linear_Combination of X

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

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)

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;

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

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;

coherence

dim (im T) is Nat ;

coherence

dim (ker T) is Nat ;

end;
let V, W be finite-dimensional VectSp of F;

let T be linear-transformation of V,W;

coherence

dim (im T) is Nat ;

coherence

dim (ker T) is Nat ;

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

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

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)

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

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;

:: any subset of X.