ranknull.miz



    begin

    theorem :: RANKNULL:1

    

     Th1: for f,g be 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

      let f,g be Function such that

       A1: g is one-to-one and

       A2: (f | ( rng g)) is one-to-one and

       A3: ( rng g) c= ( dom f);

      set h = (f * g);

      

       A4: ( dom h) c= ( dom g) by FUNCT_1: 11;

      ( dom g) c= ( dom h)

      proof

        let x be object such that

         A5: x in ( dom g);

        (g . x) in ( rng g) by A5, FUNCT_1: 3;

        hence thesis by A3, A5, FUNCT_1: 11;

      end;

      then

       A6: ( dom h) = ( dom g) by A4;

      for x1,x2 be object st x1 in ( dom h) & x2 in ( dom h) & (h . x1) = (h . x2) holds x1 = x2

      proof

        let x1,x2 be object such that

         A7: x1 in ( dom h) and

         A8: x2 in ( dom h) and

         A9: (h . x1) = (h . x2);

        

         A10: (h . x1) = (f . (g . x1)) & (h . x2) = (f . (g . x2)) by A7, A8, FUNCT_1: 12;

        ( dom (f | ( rng g))) = ( rng g) by A3, RELAT_1: 62;

        then

         A11: (g . x1) in ( dom (f | ( rng g))) by A4, A7, FUNCT_1: 3;

        (g . x2) in ( rng g) by A4, A8, FUNCT_1: 3;

        then

         A12: (g . x2) in ( dom (f | ( rng g))) by A3, RELAT_1: 62;

        (f . (g . x1)) = ((f | ( rng g)) . (g . x1)) & (f . (g . x2)) = ((f | ( rng g)) . (g . x2)) by A6, A7, A8, FUNCT_1: 3, FUNCT_1: 49;

        then (g . x1) = (g . x2) by A2, A9, A10, A11, A12;

        hence thesis by A1, A4, A7, A8;

      end;

      hence thesis;

    end;

    theorem :: RANKNULL:2

    

     Th2: for f be Function, X,Y be set st X c= Y & (f | Y) is one-to-one holds (f | X) is one-to-one

    proof

      let f be Function, X,Y be set such that

       A1: X c= Y and

       A2: (f | Y) is one-to-one;

      (f | X) = ((f | Y) | X) by A1, RELAT_1: 74;

      hence thesis by A2, FUNCT_1: 52;

    end;

    theorem :: RANKNULL:3

    

     Th3: for V be 1-sorted, X,Y be Subset of V holds X meets Y iff ex v be Element of V st v in X & v in Y

    proof

      let V be 1-sorted, X,Y be Subset of V;

      X meets Y implies ex v be Element of V st v in X & v in Y

      proof

        assume X meets Y;

        then

        consider z be object such that

         A1: z in X and

         A2: z in Y by XBOOLE_0: 3;

        reconsider v = z as Element of V by A1;

        take v;

        thus thesis by A1, A2;

      end;

      hence thesis by XBOOLE_0: 3;

    end;

    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;

      existence

      proof

        consider A be finite Subset of V such that

         A1: A is Basis of V by MATRLIN:def 1;

        reconsider A as Basis of V by A1;

        take A;

        thus thesis;

      end;

    end

    registration

      let F be Ring;

      let V,W be VectSp of F;

      cluster additive homogeneous for Function of V, W;

      existence

      proof

        set f = ( FuncZero (( [#] V),W));

        reconsider f as Function of V, W;

        

         A1: for x,y be Vector of V holds (f . (x + y)) = ((f . x) + (f . y)) by RLVECT_1:def 4;

        take f;

        for a be Element of F, x be Element of V holds (f . (a * x)) = (a * (f . x)) by VECTSP_1: 14;

        hence f is additive homogeneous by A1, MOD_2:def 2, VECTSP_1:def 20;

      end;

    end

    theorem :: RANKNULL:4

    

     Th4: ( [#] V) is finite implies V is finite-dimensional

    proof

      set B = the Basis of V;

      assume ( [#] V) is finite;

      then

      reconsider B as finite Subset of V;

      take B;

      thus thesis;

    end;

    theorem :: RANKNULL:5

    for V be finite-dimensional VectSp of F st ( card ( [#] V)) = 1 holds ( dim V) = 0

    proof

      let V be finite-dimensional VectSp of F such that

       A1: ( card ( [#] V)) = 1;

      ( [#] V) = {( 0. V)}

      proof

        ex y be object st ( [#] V) = {y} by A1, CARD_2: 42;

        hence thesis by TARSKI:def 1;

      end;

      then ( (Omega). V) = ( (0). V) by VECTSP_4:def 3;

      hence thesis by VECTSP_9: 29;

    end;

    theorem :: RANKNULL:6

    ( card ( [#] V)) = 2 implies ( dim V) = 1

    proof

      assume

       A1: ( card ( [#] V)) = 2;

      then

       A2: ( [#] V) is finite;

      reconsider C = ( [#] V) as finite set by A1;

      reconsider V as finite-dimensional VectSp of F by A2, Th4;

      ex v be Vector of V st v <> ( 0. V) & ( (Omega). V) = ( Lin {v})

      proof

        consider x,y be object such that

         A3: x <> y and

         A4: ( [#] V) = {x, y} by A1, CARD_2: 60;

        per cases by A4, TARSKI:def 2;

          suppose

           A5: x = ( 0. V);

          then

          reconsider x as Element of V;

          reconsider y as Element of V by A4, TARSKI:def 2;

          set L = ( Lin {y});

          take y;

          for v be Element of V holds v in ( (Omega). V) iff v in L

          proof

            let v be Element of V;

            v in ( (Omega). V) implies v in L

            proof

              assume v in ( (Omega). V);

              

               A6: y in {y} by TARSKI:def 1;

              

               A7: ( 0. L) in L;

              per cases by A4, TARSKI:def 2;

                suppose v = x;

                hence thesis by A5, A7, VECTSP_4:def 2;

              end;

                suppose v = y;

                hence thesis by A6, VECTSP_7: 8;

              end;

            end;

            hence thesis;

          end;

          hence thesis by A3, A5, VECTSP_4: 30;

        end;

          suppose

           A8: y = ( 0. V);

          reconsider x as Element of V by A4, TARSKI:def 2;

          reconsider y as Element of V by A8;

          set L = ( Lin {x});

          take x;

          for v be Element of V holds v in ( (Omega). V) iff v in L

          proof

            let v be Element of V;

            v in ( (Omega). V) implies v in L

            proof

              assume v in ( (Omega). V);

              

               A9: x in {x} by TARSKI:def 1;

              

               A10: ( 0. L) in L;

              per cases by A4, TARSKI:def 2;

                suppose v = y;

                hence thesis by A8, A10, VECTSP_4:def 2;

              end;

                suppose v = x;

                hence thesis by A9, VECTSP_7: 8;

              end;

            end;

            hence thesis;

          end;

          hence thesis by A3, A8, VECTSP_4: 30;

        end;

      end;

      hence thesis by VECTSP_9: 30;

    end;

    begin

    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

    

     Th7: for V,W be non empty 1-sorted, T be Function of V, W holds ( dom T) = ( [#] V) & ( rng T) c= ( [#] W)

    proof

      let V,W be non empty 1-sorted, T be Function of V, W;

      T is Element of ( Funcs (( [#] V),( [#] W))) by FUNCT_2: 8;

      hence thesis by FUNCT_2: 92;

    end;

    theorem :: RANKNULL:8

    

     Th8: for F be Ring, V,W be VectSp of F, T be linear-transformation of V, W holds for x,y be Element of V holds ((T . x) - (T . y)) = (T . (x - y))

    proof

      let F be Ring, V,W be VectSp of F, T be linear-transformation of V, W;

      let x,y be Element of V;

      

       A1: (T . (( - ( 1. F)) * y)) = (( - ( 1. F)) * (T . y)) by MOD_2:def 2;

      (T . (x - y)) = ((T . x) + (T . ( - y))) & ( - y) = (( - ( 1. F)) * y) by VECTSP_1: 14, VECTSP_1:def 20;

      hence thesis by A1, VECTSP_1: 14;

    end;

    theorem :: RANKNULL:9

    

     Th9: for F be Ring, V,W be VectSp of F, T be linear-transformation of V, W holds (T . ( 0. V)) = ( 0. W)

    proof

      let F be Ring, V,W be VectSp of F, T be linear-transformation of V, W;

      ( 0. V) = (( 0. F) * ( 0. V)) by VECTSP_1: 14;

      

      then (T . ( 0. V)) = (( 0. F) * (T . ( 0. V))) by MOD_2:def 2

      .= ( 0. W) by VECTSP_1: 14;

      hence thesis;

    end;

    definition

      let F be Ring, V,W be VectSp of F, T be linear-transformation of V, W;

      :: RANKNULL:def1

      func ker T -> strict Subspace of V means

      : Def1: ( [#] it ) = { u where u be Element of V : (T . u) = ( 0. W) };

      existence

      proof

        set K = { u where u be Element of V : (T . u) = ( 0. W) };

        K c= ( [#] V)

        proof

          let x be object;

          assume x in K;

          then ex u be Element of V st u = x & (T . u) = ( 0. W);

          hence thesis;

        end;

        then

        reconsider K as Subset of V;

        

         A1: for v be Element of V st v in K holds (T . v) = ( 0. W)

        proof

          let v be Element of V;

          assume v in K;

          then ex u be Element of V st u = v & (T . u) = ( 0. W);

          hence thesis;

        end;

        now

          let u be Element of V, a be Element of F;

          assume u in K;

          then (T . u) = ( 0. W) by A1;

          

          then (T . (a * u)) = (a * ( 0. W)) by MOD_2:def 2

          .= ( 0. W) by VECTSP_1: 14;

          hence (a * u) in K;

        end;

        then

         A2: for a be Element of F, u be Element of V st u in K holds (a * u) in K;

        (T . ( 0. V)) = ( 0. W) by Th9;

        then

         A3: ( 0. V) in K;

        now

          let u,v be Element of V;

          assume u in K & v in K;

          then (T . u) = ( 0. W) & (T . v) = ( 0. W) by A1;

          

          then (T . (u + v)) = (( 0. W) + ( 0. W)) by VECTSP_1:def 20

          .= ( 0. W) by RLVECT_1:def 4;

          hence (u + v) in K;

        end;

        then K is linearly-closed by A2;

        then

        consider W be strict Subspace of V such that

         A4: K = the carrier of W by A3, VECTSP_4: 34;

        take W;

        thus thesis by A4;

      end;

      uniqueness by VECTSP_4: 29;

    end

    theorem :: RANKNULL:10

    

     Th10: for F be Ring, V,W be VectSp of F, T be linear-transformation of V, W holds for x be Element of V holds x in ( ker T) iff (T . x) = ( 0. W)

    proof

      let F be Ring, V,W be VectSp of F, T be linear-transformation of V, W;

      let x be Element of V;

      thus x in ( ker T) implies (T . x) = ( 0. W)

      proof

        assume x in ( ker T);

        then

         A1: x in ( [#] ( ker T));

        ( [#] ( ker T)) = { u where u be Element of V : (T . u) = ( 0. W) } by Def1;

        then ex u be Element of V st u = x & (T . u) = ( 0. W) by A1;

        hence thesis;

      end;

      assume (T . x) = ( 0. W);

      then x in { u where u be Element of V : (T . u) = ( 0. W) };

      then x in ( [#] ( ker T)) by Def1;

      hence thesis;

    end;

    definition

      let V,W be non empty 1-sorted, T be Function of V, W, X be Subset of V;

      :: original: .:

      redefine

      func T .: X -> Subset of W ;

      coherence

      proof

        ( rng T) c= ( [#] W) & (T .: X) c= ( rng T) by Th7, RELAT_1: 111;

        hence thesis by XBOOLE_1: 1;

      end;

    end

    definition

      let F be Ring, V,W be VectSp of F, T be linear-transformation of V, W;

      :: RANKNULL:def2

      func im T -> strict Subspace of W means

      : Def2: ( [#] it ) = (T .: ( [#] V));

      existence

      proof

        reconsider U = (T .: ( [#] V)) as Subset of W;

        

         A1: for u be Element of W holds u in U iff ex v be Element of V st (T . v) = u

        proof

          let u be Element of W;

          thus u in U implies ex v be Element of V st (T . v) = u

          proof

            assume u in U;

            then

            consider x be object such that x in ( dom T) and

             A2: x in ( [#] V) and

             A3: u = (T . x) by FUNCT_1:def 6;

            reconsider x as Element of V by A2;

            take x;

            thus thesis by A3;

          end;

          thus (ex v be Element of V st (T . v) = u) implies u in U

          proof

            given v be Element of V such that

             A4: (T . v) = u;

            v in ( [#] V);

            then v in ( dom T) by Th7;

            hence thesis by A4, FUNCT_1:def 6;

          end;

        end;

         A5:

        now

          let u,v be Element of W such that

           A6: u in U and

           A7: v in U;

          consider x be Element of V such that

           A8: (T . x) = u by A1, A6;

          consider y be Element of V such that

           A9: (T . y) = v by A1, A7;

          (u + v) = (T . (x + y)) by A8, A9, VECTSP_1:def 20;

          hence (u + v) in U by A1;

        end;

        now

          let a be Element of F, w be Element of W;

          assume w in U;

          then

          consider v be Element of V such that

           A10: (T . v) = w by A1;

          (T . (a * v)) = (a * w) by A10, MOD_2:def 2;

          hence (a * w) in U by A1;

        end;

        then

         A11: U is linearly-closed by A5;

        (T . ( 0. V)) = ( 0. W) by Th9;

        then U <> {} by A1;

        then

        consider A be strict Subspace of W such that

         A12: U = the carrier of A by A11, VECTSP_4: 34;

        take A;

        thus thesis by A12;

      end;

      uniqueness by VECTSP_4: 29;

    end

    theorem :: RANKNULL:11

    for F be Ring, V,W be VectSp of F, T be linear-transformation of V, W holds ( 0. V) in ( ker T)

    proof

      let F be Ring, V,W be VectSp of F, T be linear-transformation of V, W;

      ( 0. V) = (( 0. F) * ( 0. V)) by VECTSP_1: 14;

      

      then (T . ( 0. V)) = (( 0. F) * (T . ( 0. V))) by MOD_2:def 2

      .= ( 0. W) by VECTSP_1: 14;

      hence thesis by Th10;

    end;

    theorem :: RANKNULL:12

    

     Th12: for F be Ring, V,W be VectSp of F, T be linear-transformation of V, W holds for X be Subset of V holds (T .: X) is Subset of ( im T)

    proof

      let F be Ring, V,W be VectSp of F, T be linear-transformation of V, W;

      let X be Subset of V;

      ( [#] ( im T)) = (T .: ( [#] V)) by Def2;

      hence thesis by RELAT_1: 123;

    end;

    theorem :: RANKNULL:13

    

     Th13: for F be Ring, V,W be VectSp of F, T be linear-transformation of V, W holds for y be Element of W holds y in ( im T) iff ex x be Element of V st y = (T . x)

    proof

      let F be Ring, V,W be VectSp of F, T be linear-transformation of V, W;

      let y be Element of W;

      

       A1: y in ( im T) implies ex x be Element of V st y = (T . x)

      proof

        assume y in ( im T);

        then

        reconsider y as Element of ( im T);

        ( [#] ( im T)) = (T .: ( [#] V)) by Def2;

        then

        consider x be object such that x in ( dom T) and

         A2: x in ( [#] V) and

         A3: y = (T . x) by FUNCT_1:def 6;

        reconsider x as Element of V by A2;

        take x;

        thus thesis by A3;

      end;

      (ex x be Element of V st y = (T . x)) implies y in ( im T)

      proof

        assume

         A4: ex x be Element of V st y = (T . x);

        ( dom T) = ( [#] V) by Th7;

        then y in (T .: ( [#] V)) by A4, FUNCT_1:def 6;

        then y in ( [#] ( im T)) by Def2;

        hence thesis;

      end;

      hence thesis by A1;

    end;

    theorem :: RANKNULL:14

    for F be Ring, V,W be VectSp of F, T be linear-transformation of V, W holds for x be Element of ( ker T) holds (T . x) = ( 0. W)

    proof

      let F be Ring, V,W be VectSp of F, T be linear-transformation of V, W;

      let x be Element of ( ker T);

      reconsider y = x as Element of V by VECTSP_4: 10;

      y in ( ker T);

      hence thesis by Th10;

    end;

    theorem :: RANKNULL:15

    

     Th15: for F be Ring, V,W be VectSp of F, T be linear-transformation of V, W st T is one-to-one holds ( ker T) = ( (0). V)

    proof

      let F be Ring, V,W be VectSp of F, T be linear-transformation of V, W;

      reconsider Z = ( (0). V) as Subspace of ( ker T) by VECTSP_4: 39;

      assume

       A1: T is one-to-one;

      for v be Element of ( ker T) holds v in Z

      proof

        let v be Element of ( ker T);

        

         A2: v in ( ker T);

        assume not v in Z;

        then

         A3: not v = ( 0. V) by VECTSP_4: 35;

        

         A4: (T . ( 0. V)) = ( 0. W) & ( dom T) = ( [#] V) by Th7, Th9;

        reconsider v as Element of V by VECTSP_4: 10;

        (T . v) = ( 0. W) by A2, Th10;

        hence thesis by A1, A3, A4;

      end;

      hence thesis by VECTSP_4: 32;

    end;

    theorem :: RANKNULL:16

    

     Th16: for V be finite-dimensional VectSp of F holds ( dim ( (0). V)) = 0

    proof

      let V be finite-dimensional VectSp of F;

      ( (Omega). ( (0). V)) = ( (0). ( (0). V)) by VECTSP_4: 36;

      hence thesis by VECTSP_9: 29;

    end;

    theorem :: RANKNULL:17

    

     Th17: for F be Ring, V,W be VectSp of F, T be linear-transformation of V, W holds for x,y be Element of V st (T . x) = (T . y) holds (x - y) in ( ker T)

    proof

      let F be Ring, V,W be VectSp of F, T be linear-transformation of V, W;

      let x,y be Element of V such that

       A1: (T . x) = (T . y);

      (T . (x - y)) = ((T . x) - (T . y)) by Th8

      .= ( 0. W) by A1, VECTSP_1: 19;

      hence thesis by Th10;

    end;

    theorem :: RANKNULL:18

    

     Th18: for F be Ring, V,W be VectSp of F holds for A be Subset of V, x,y be Element of V st (x - y) in ( Lin A) holds x in ( Lin (A \/ {y}))

    proof

      let F be Ring, V,W be VectSp of F;

      let A be Subset of V, x,y be Element of V such that

       A1: (x - y) in ( Lin A);

      

       A2: ( Lin (A \/ {y})) = (( Lin A) + ( Lin {y})) by VECTSP_7: 15;

      y in {y} by TARSKI:def 1;

      then

       A3: y in ( Lin {y}) by VECTSP_7: 8;

      ((x - y) + y) = (x - (y - y)) by RLVECT_1: 29

      .= (x - ( 0. V)) by VECTSP_1: 19

      .= x by RLVECT_1: 13;

      hence thesis by A1, A3, A2, VECTSP_5: 1;

    end;

    begin

    theorem :: RANKNULL:19

    

     Th19: for F be Ring, V,W be VectSp of F holds for X be Subset of V st V is Subspace of W holds X is Subset of W

    proof

      let F be Ring, V,W be VectSp of F;

      let X be Subset of V;

      assume V is Subspace of W;

      then

       A1: ( [#] V) c= ( [#] W) by VECTSP_4:def 2;

      X c= ( [#] W) by A1;

      hence thesis;

    end;

    theorem :: RANKNULL:20

    

     Th20: for A be Subset of V st A is linearly-independent holds A is Basis of ( Lin A)

    proof

      let A be Subset of V such that

       A1: A is linearly-independent;

      A c= ( [#] ( Lin A))

      proof

        let x be object such that

         A2: x in A;

        reconsider x as Element of V by A2;

        x in ( Lin A) by A2, VECTSP_7: 8;

        hence thesis;

      end;

      then

      reconsider B = A as Subset of ( Lin A);

      

       A3: ( Lin B) = ( Lin A) by VECTSP_9: 17;

      B is linearly-independent by A1, VECTSP_9: 12;

      hence thesis by A3, VECTSP_7:def 3;

    end;

    theorem :: RANKNULL:21

    

     Th21: for A be Subset of V, x be Element of V st x in ( Lin A) & not x in A holds (A \/ {x}) is linearly-dependent

    proof

      let A be Subset of V, x be Element of V such that

       A1: x in ( Lin A) and

       A2: not x in A;

      per cases ;

        suppose

         A3: A is linearly-independent;

        x in ( [#] ( Lin A)) by A1;

        then

        reconsider X = {x} as Subset of ( Lin A) by SUBSET_1: 41;

        reconsider A9 = A as Basis of ( Lin A) by A3, Th20;

        reconsider B = (A9 \/ X) as Subset of ( Lin A);

        X misses A9

        proof

          assume X meets A9;

          then ex y be object st y in X & y in A9 by XBOOLE_0: 3;

          hence contradiction by A2, TARSKI:def 1;

        end;

        then B is linearly-dependent by VECTSP_9: 15;

        hence thesis by VECTSP_9: 12;

      end;

        suppose A is linearly-dependent;

        hence thesis by VECTSP_7: 1, XBOOLE_1: 7;

      end;

    end;

    theorem :: RANKNULL:22

    

     Th22: for A be Subset of V, B be Basis of V st A is Basis of ( ker T) & A c= B holds (T | (B \ A)) is one-to-one

    proof

      let A be Subset of V, B be Basis of V such that

       A1: A is Basis of ( ker T) and

       A2: A c= B;

      reconsider A9 = A as Subset of V;

      set f = (T | (B \ A));

      let x1,x2 be object such that

       A3: x1 in ( dom f) and

       A4: x2 in ( dom f) and

       A5: (f . x1) = (f . x2) and

       A6: x1 <> x2;

      x2 in ( dom T) by A4, RELAT_1: 57;

      then

      reconsider x2 as Element of V;

      x1 in ( dom T) by A3, RELAT_1: 57;

      then

      reconsider x1 as Element of V;

      

       A7: x1 in (B \ A) by A3;

      

       A8: not x1 in (A9 \/ {x2})

      proof

        assume

         A9: x1 in (A9 \/ {x2});

        per cases by A9, XBOOLE_0:def 3;

          suppose x1 in A9;

          hence contradiction by A7, XBOOLE_0:def 5;

        end;

          suppose x1 in {x2};

          hence contradiction by A6, TARSKI:def 1;

        end;

      end;

      

       A10: x2 in (B \ A) by A4;

      then

       A11: (f . x2) = (T . x2) by FUNCT_1: 49;

      reconsider A as Basis of ( ker T) by A1;

      

       A12: ( ker T) = ( Lin A) by VECTSP_7:def 3;

      (f . x1) = (T . x1) by A7, FUNCT_1: 49;

      then (x1 - x2) in ( ker T) by A5, A11, Th17;

      then (x1 - x2) in ( Lin A9) by A12, VECTSP_9: 17;

      then

       A13: x1 in ( Lin (A9 \/ {x2})) by Th18;

      ( {x2} \/ {x1}) = {x1, x2} by ENUMSET1: 1;

      then

       A14: ((A9 \/ {x2}) \/ {x1}) = (A9 \/ {x1, x2}) by XBOOLE_1: 4;

       {x1, x2} c= B

      proof

        let z be object such that

         A15: z in {x1, x2};

        per cases by A15, TARSKI:def 2;

          suppose z = x1;

          hence thesis by A7, XBOOLE_0:def 5;

        end;

          suppose z = x2;

          hence thesis by A10, XBOOLE_0:def 5;

        end;

      end;

      then

       A16: (A9 \/ {x1, x2}) c= B by A2, XBOOLE_1: 8;

      B is linearly-independent by VECTSP_7:def 3;

      hence thesis by A13, A14, A8, A16, Th21, VECTSP_7: 1;

    end;

    theorem :: RANKNULL:23

    for A be Subset of V, l be Linear_Combination of A, x be Element of V, a be Element of F holds (l +* (x,a)) is Linear_Combination of (A \/ {x})

    proof

      let A be Subset of V, l be Linear_Combination of A, x be Element of V, a be Element of F;

      set m = (l +* (x,a));

      

       A1: ( dom m) = ( [#] V) by FUNCT_2:def 1;

      ( rng m) c= ( [#] F)

      proof

        let y be object;

        assume y in ( rng m);

        then

        consider x9 be object such that

         A2: x9 in ( dom m) and

         A3: (m . x9) = y by FUNCT_1:def 3;

        

         A4: x9 in ( dom l) by A1, A2, FUNCT_2: 92;

        per cases ;

          suppose x9 = x;

          then (m . x9) = a by A4, FUNCT_7: 31;

          hence thesis by A3;

        end;

          suppose

           A5: x9 <> x;

          

           A6: (l . x9) in ( rng l) & ( rng l) c= ( [#] F) by A4, FUNCT_1: 3, FUNCT_2: 92;

          (m . x9) = (l . x9) by A5, FUNCT_7: 32;

          hence thesis by A3, A6;

        end;

      end;

      then

      reconsider m as Element of ( Funcs (( [#] V),( [#] F))) by A1, FUNCT_2:def 2;

      set T = (( Carrier l) \/ {x});

      for v be Element of V st not v in T holds (m . v) = ( 0. F)

      proof

        let v be Element of V such that

         A7: not v in T;

         not v in {x} by A7, XBOOLE_0:def 3;

        then v <> x by TARSKI:def 1;

        then

         A8: (m . v) = (l . v) by FUNCT_7: 32;

         not v in ( Carrier l) by A7, XBOOLE_0:def 3;

        hence thesis by A8;

      end;

      then

      reconsider m as Linear_Combination of V by VECTSP_6:def 1;

      

       A9: ( Carrier m) c= T

      proof

        let y be object;

        assume y in ( Carrier m);

        then

        consider z be Element of V such that

         A10: y = z and

         A11: (m . z) <> ( 0. F);

        per cases ;

          suppose

           A12: z = x;

          x in {x} & {x} c= T by TARSKI:def 1, XBOOLE_1: 7;

          hence thesis by A10, A12;

        end;

          suppose z <> x;

          then (m . z) = (l . z) by FUNCT_7: 32;

          then

           A13: z in ( Carrier l) by A11;

          ( Carrier l) c= T by XBOOLE_1: 7;

          hence thesis by A10, A13;

        end;

      end;

      ( Carrier l) c= A by VECTSP_6:def 4;

      then T c= (A \/ {x}) by XBOOLE_1: 9;

      then ( Carrier m) c= (A \/ {x}) by A9;

      hence thesis by VECTSP_6:def 4;

    end;

    definition

      let V be 1-sorted, X be Subset of V;

      :: RANKNULL:def3

      func V \ X -> Subset of V equals (( [#] V) \ X);

      coherence ;

    end

    definition

      let F be Field, V be VectSp of F, l be Linear_Combination of V, X be Subset of V;

      :: original: .:

      redefine

      func l .: X -> Subset of F ;

      coherence

      proof

        (l .: X) c= ( [#] F);

        hence thesis;

      end;

    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;

      existence

      proof

        reconsider S = {( 0. V)} as Subset of V;

        take S;

        ( 0. V) in S by TARSKI:def 1;

        hence thesis by VECTSP_7: 2;

      end;

    end

    definition

      let F be Field, V be VectSp of F, l be Linear_Combination of V, A be Subset of V;

      :: RANKNULL:def4

      func l ! A -> Linear_Combination of A equals ((l | A) +* ((V \ A) --> ( 0. F)));

      coherence

      proof

        set f = ((l | A) +* ((V \ A) --> ( 0. F)));

        

         A1: ( dom f) = (( dom (l | A)) \/ ( dom ((V \ A) --> ( 0. F)))) by FUNCT_4:def 1;

        ( dom l) = ( [#] V) by FUNCT_2: 92;

        then

         A3: ( dom (l | A)) = A by RELAT_1: 62;

        then

         A4: ( dom f) = ( [#] V) by A1, XBOOLE_1: 45;

        

         A5: (A \/ (( [#] V) \ A)) = ( [#] V) by XBOOLE_1: 45;

        ( rng f) c= ( [#] F)

        proof

          let y be object;

          assume y in ( rng f);

          then

          consider x be object such that

           A6: x in ( dom f) and

           A7: y = (f . x) by FUNCT_1:def 3;

          reconsider x as Element of V by A1, A3, A6, XBOOLE_1: 45;

          per cases by A5, XBOOLE_0:def 3;

            suppose

             A8: x in A;

            then not x in ( dom ((V \ A) --> ( 0. F))) by XBOOLE_0:def 5;

            then

             A9: (f . x) = ((l | A) . x) by FUNCT_4: 11;

            ((l | A) . x) = (l . x) by A8, FUNCT_1: 49;

            hence thesis by A7, A9;

          end;

            suppose

             A10: x in (V \ A);

            then x in ( dom ((V \ A) --> ( 0. F)));

            

            then (f . x) = (((V \ A) --> ( 0. F)) . x) by FUNCT_4: 13

            .= ( 0. F) by A10, FUNCOP_1: 7;

            hence thesis by A7;

          end;

        end;

        then

        reconsider f as Element of ( Funcs (( [#] V),( [#] F))) by A4, FUNCT_2:def 2;

        ex T be finite Subset of V st for v be Element of V st not v in T holds (f . v) = ( 0. F)

        proof

          set D = { v where v be Element of V : (f . v) <> ( 0. F) };

          D c= ( [#] V)

          proof

            let x be object;

            assume x in D;

            then ex v be Element of V st x = v & (f . v) <> ( 0. F);

            hence thesis;

          end;

          then

          reconsider D as Subset of V;

          set C = ( Carrier l);

          D c= C

          proof

            let x be object;

            assume x in D;

            then

            consider v be Element of V such that

             A11: x = v and

             A12: (f . v) <> ( 0. F);

             A14:

            now

              assume

               A15: v in (V \ A);

              

              then (f . v) = (((V \ A) --> ( 0. F)) . v) by A1, A4, FUNCT_4:def 1

              .= ( 0. F) by A15, FUNCOP_1: 7;

              hence contradiction by A12;

            end;

            then v in A by XBOOLE_0:def 5;

            then

             A16: ((l | A) . v) = (l . v) by FUNCT_1: 49;

             not v in ( dom ((V \ A) --> ( 0. F))) by A14;

            then (f . v) = ((l | A) . v) by FUNCT_4: 11;

            hence thesis by A11, A12, A16;

          end;

          then

          reconsider D as finite Subset of V;

          take D;

          thus thesis;

        end;

        then

        reconsider f as Linear_Combination of V by VECTSP_6:def 1;

        ( Carrier f) c= A

        proof

          let x be object such that

           A17: x in ( Carrier f);

          reconsider x as Element of V by A17;

          

           A18: (f . x) <> ( 0. F) by A17, VECTSP_6: 2;

          now

            assume not x in A;

            then

             A19: x in (V \ A) by XBOOLE_0:def 5;

            then x in (( dom (l | A)) \/ ( dom ((V \ A) --> ( 0. F)))) by XBOOLE_0:def 3;

            then (f . x) = (((V \ A) --> ( 0. F)) . x) by A19, FUNCT_4:def 1;

            hence contradiction by A18, A19, FUNCOP_1: 7;

          end;

          hence thesis;

        end;

        hence thesis by VECTSP_6:def 4;

      end;

    end

    theorem :: RANKNULL:24

    

     Th24: l = (l ! ( Carrier l))

    proof

      set f = (l | ( Carrier l));

      set g = ((V \ ( Carrier l)) --> ( 0. F));

      set m = (f +* g);

      

       A2: ( dom l) = ( [#] V) by FUNCT_2: 92;

      then ( dom f) = ( Carrier l) by RELAT_1: 62;

      then

       A3: (( dom f) \/ ( dom g)) = ( [#] V) by XBOOLE_1: 45;

      

       A4: for x be object st x in ( dom l) holds (l . x) = (m . x)

      proof

        let x be object;

        assume x in ( dom l);

        then

        reconsider x as Element of V;

        per cases ;

          suppose

           A5: x in ( Carrier l);

          then not x in ( dom g) by XBOOLE_0:def 5;

          then (m . x) = (f . x) by A3, FUNCT_4:def 1;

          hence thesis by A5, FUNCT_1: 49;

        end;

          suppose

           A6: not x in ( Carrier l);

          then x in (V \ ( Carrier l)) by XBOOLE_0:def 5;

          then (m . x) = (g . x) & (g . x) = ( 0. F) by A3, FUNCOP_1: 7, FUNCT_4:def 1;

          hence thesis by A6;

        end;

      end;

      ( dom l) = ( dom m) by A2, A3, FUNCT_4:def 1;

      hence thesis by A4;

    end;

    

     Lm1: for X be Subset of V holds (l .: X) is finite

    proof

      let X be Subset of V;

      

       A1: l = (l ! ( Carrier l)) by Th24;

      (( rng (l | ( Carrier l))) \/ ( rng ((V \ ( Carrier l)) --> ( 0. F)))) is finite;

      then ( rng l) is finite by A1, FINSET_1: 1, FUNCT_4: 17;

      hence thesis by FINSET_1: 1, RELAT_1: 111;

    end;

    theorem :: RANKNULL:25

    

     Th25: for A be Subset of V, v be Element of V st v in A holds ((l ! A) . v) = (l . v)

    proof

      let A be Subset of V, v be Element of V such that

       A1: v in A;

      ( dom (l ! A)) = ( [#] V) by FUNCT_2: 92;

      then

       A2: (( dom (l | A)) \/ ( dom ((V \ A) --> ( 0. F)))) = ( [#] V) by FUNCT_4:def 1;

       not v in ( dom ((V \ A) --> ( 0. F))) by A1, XBOOLE_0:def 5;

      

      then ((l ! A) . v) = ((l | A) . v) by A2, FUNCT_4:def 1

      .= (l . v) by A1, FUNCT_1: 49;

      hence thesis;

    end;

    theorem :: RANKNULL:26

    

     Th26: for A be Subset of V, v be Element of V st not v in A holds ((l ! A) . v) = ( 0. F)

    proof

      let A be Subset of V, v be Element of V;

      assume not v in A;

      then

       A1: v in (V \ A) by XBOOLE_0:def 5;

      

       A2: ( dom (l ! A)) = ( [#] V) by FUNCT_2: 92;

      ( dom ((V \ A) --> ( 0. F))) = (V \ A) & ( dom (l ! A)) = (( dom (l | A)) \/ ( dom ((V \ A) --> ( 0. F)))) by FUNCT_4:def 1;

      

      then ((l ! A) . v) = (((V \ A) --> ( 0. F)) . v) by A2, A1, FUNCT_4:def 1

      .= ( 0. F) by A1, FUNCOP_1: 7;

      hence thesis;

    end;

    theorem :: RANKNULL:27

    

     Th27: for A,B be Subset of V, l be Linear_Combination of B st A c= B holds l = ((l ! A) + (l ! (B \ A)))

    proof

      let A,B be Subset of V, l be Linear_Combination of B such that

       A1: A c= B;

      set r = ((l ! A) + (l ! (B \ A)));

      let v be Element of V;

      

       A2: v in B implies (v in A or v in (B \ A))

      proof

        assume

         A3: v in B;

        B = (A \/ (B \ A)) by A1, XBOOLE_1: 45;

        hence thesis by A3, XBOOLE_0:def 3;

      end;

      per cases by A2;

        suppose

         A4: v in A;

        then not v in (B \ A) by XBOOLE_0:def 5;

        then

         A5: ((l ! (B \ A)) . v) = ( 0. F) by Th26;

        ((l ! A) . v) = (l . v) by A4, Th25;

        

        then (r . v) = ((l . v) + ( 0. F)) by A5, VECTSP_6: 22

        .= (l . v) by RLVECT_1: 4;

        hence (l . v) = (r . v);

      end;

        suppose

         A6: v in (B \ A);

        then not v in A by XBOOLE_0:def 5;

        then

         A7: ((l ! A) . v) = ( 0. F) by Th26;

        ((l ! (B \ A)) . v) = (l . v) by A6, Th25;

        

        then (r . v) = (( 0. F) + (l . v)) by A7, VECTSP_6: 22

        .= (l . v) by RLVECT_1: 4;

        hence (l . v) = (r . v);

      end;

        suppose

         A8: not v in B;

        ( Carrier l) c= B by VECTSP_6:def 4;

        then

         A9: not v in ( Carrier l) by A8;

         not v in (B \ A) by A8, XBOOLE_0:def 5;

        then

         A10: ((l ! (B \ A)) . v) = ( 0. F) by Th26;

         not v in A by A1, A8;

        then ((l ! A) . v) = ( 0. F) by Th26;

        

        then (r . v) = (( 0. F) + ( 0. F)) by A10, VECTSP_6: 22

        .= ( 0. F) by RLVECT_1: 4;

        hence (l . v) = (r . v) by A9;

      end;

    end;

    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;

      coherence by Lm1;

    end

    definition

      let V,W be non empty 1-sorted, T be Function of V, W, X be Subset of W;

      :: original: "

      redefine

      func T " X -> Subset of V ;

      coherence

      proof

        ( dom T) = ( [#] V) by Th7;

        hence thesis by RELAT_1: 132;

      end;

    end

    theorem :: RANKNULL:28

    

     Th28: for X be Subset of V st X misses ( Carrier l) holds (l .: X) c= {( 0. F)}

    proof

      let X be Subset of V such that

       A1: X misses ( Carrier l);

      set M = (l .: X);

      let y be object;

      assume y in M;

      then

      consider x be object such that

       A2: x in ( dom l) and

       A3: x in X and

       A4: y = (l . x) by FUNCT_1:def 6;

      reconsider x as Element of V by A2;

      now

        assume (l . x) <> ( 0. F);

        then x in ( Carrier l);

        then x in (( Carrier l) /\ X) by A3, XBOOLE_0:def 4;

        hence contradiction by A1;

      end;

      hence thesis by A4, TARSKI:def 1;

    end;

    definition

      let F be Field, V,W be VectSp of F, l be Linear_Combination of V, T be linear-transformation of V, W;

      :: RANKNULL:def5

      func T @ l -> Linear_Combination of W means

      : Def5: for w be Element of W holds (it . w) = ( Sum (l .: (T " {w})));

      existence

      proof

        defpred P[ object, object] means ex w be Element of W st $1 = w & $2 = ( Sum (l .: (T " {w})));

        

         A1: for x be object st x in ( [#] W) holds ex y be object st P[x, y]

        proof

          let x be object;

          assume x in ( [#] W);

          then

          reconsider x as Element of W;

          take ( Sum (l .: (T " {x})));

          thus thesis;

        end;

        consider f be Function such that

         A2: ( dom f) = ( [#] W) and

         A3: for x be object st x in ( [#] W) holds P[x, (f . x)] from CLASSES1:sch 1( A1);

        

         A4: ( rng f) c= ( [#] F)

        proof

          let y be object;

          assume y in ( rng f);

          then

          consider x be object such that

           A5: x in ( dom f) and

           A6: (f . x) = y by FUNCT_1:def 3;

          ex w be Element of W st x = w & (f . x) = ( Sum (l .: (T " {w}))) by A2, A3, A5;

          hence thesis by A6;

        end;

        

         A7: for w be Element of W holds (f . w) = ( Sum (l .: (T " {w})))

        proof

          let w be Element of W;

          ex w9 be Element of W st w = w9 & (f . w) = ( Sum (l .: (T " {w9}))) by A3;

          hence thesis;

        end;

        reconsider f as Element of ( Funcs (( [#] W),( [#] F))) by A2, A4, FUNCT_2:def 2;

        ex T be finite Subset of W st for w be Element of W st not w in T holds (f . w) = ( 0. F)

        proof

          set X = { w where w be Element of W : (f . w) <> ( 0. F) };

          X c= ( [#] W)

          proof

            let x be object;

            assume x in X;

            then ex w be Element of W st x = w & (f . w) <> ( 0. F);

            hence thesis;

          end;

          then

          reconsider X as Subset of W;

          set C = ( Carrier l);

          reconsider TC = (T .: C) as Subset of W;

          X c= TC

          proof

            let x be object;

            assume x in X;

            then

            consider w be Element of W such that

             A8: x = w and

             A9: (f . w) <> ( 0. F);

            (T " {w}) meets ( Carrier l)

            proof

              assume

               A10: (T " {w}) misses ( Carrier l);

              then

               A11: (l .: (T " {w})) c= {( 0. F)} by Th28;

              ( Sum (l .: (T " {w}))) = ( 0. F)

              proof

                per cases ;

                  suppose (l .: (T " {w})) = ( {} F);

                  hence thesis by RLVECT_2: 8;

                end;

                  suppose

                   A12: (l .: (T " {w})) <> ( {} F);

                  

                   A13: {( 0. F)} c= (l .: (T " {w}))

                  proof

                    let y be object;

                    assume y in {( 0. F)};

                    then

                     A14: y = ( 0. F) by TARSKI:def 1;

                    ex z be object st z in (l .: (T " {w})) by A12, XBOOLE_0:def 1;

                    hence thesis by A11, A14, TARSKI:def 1;

                  end;

                  (l .: (T " {w})) c= {( 0. F)} by A10, Th28;

                  then (l .: (T " {w})) = {( 0. F)} by A13;

                  hence thesis by RLVECT_2: 9;

                end;

              end;

              hence contradiction by A7, A9;

            end;

            then

            consider y be object such that

             A15: y in (T " {w}) and

             A16: y in ( Carrier l) by XBOOLE_0: 3;

            

             A17: ( dom T) = ( [#] V) by Th7;

            reconsider y as Element of V by A16;

            (T . y) in {w} by A15, FUNCT_1:def 7;

            then (T . y) = w by TARSKI:def 1;

            hence thesis by A8, A16, A17, FUNCT_1:def 6;

          end;

          then

          reconsider X as finite Subset of W;

          take X;

          thus thesis;

        end;

        then

        reconsider f as Linear_Combination of W by VECTSP_6:def 1;

        take f;

        for w be Element of W holds (f . w) = ( Sum (l .: (T " {w})))

        proof

          let w be Element of W;

          ex w9 be Element of W st w = w9 & (f . w) = ( Sum (l .: (T " {w9}))) by A3;

          hence thesis;

        end;

        hence thesis;

      end;

      uniqueness

      proof

        let f,g be Linear_Combination of W such that

         A18: for w be Element of W holds (f . w) = ( Sum (l .: (T " {w}))) and

         A19: for w be Element of W holds (g . w) = ( Sum (l .: (T " {w})));

        

         A20: for x be object st x in ( dom f) holds (f . x) = (g . x)

        proof

          let x be object;

          assume x in ( dom f);

          then

          reconsider x as Element of W;

          (f . x) = ( Sum (l .: (T " {x}))) by A18;

          hence thesis by A19;

        end;

        ( dom f) = ( [#] W) & ( dom g) = ( [#] W) by FUNCT_2: 92;

        hence thesis by A20;

      end;

    end

    theorem :: RANKNULL:29

    

     Th29: (T @ l) is Linear_Combination of (T .: ( Carrier l))

    proof

      ( Carrier (T @ l)) c= (T .: ( Carrier l))

      proof

        let w be object such that

         A1: w in ( Carrier (T @ l));

        reconsider w as Element of W by A1;

        

         A2: ((T @ l) . w) <> ( 0. F) by A1, VECTSP_6: 2;

        now

          assume

           A3: (T " {w}) misses ( Carrier l);

          then

           A4: (l .: (T " {w})) c= {( 0. F)} by Th28;

          ( Sum (l .: (T " {w}))) = ( 0. F)

          proof

            per cases ;

              suppose (l .: (T " {w})) = ( {} F);

              hence thesis by RLVECT_2: 8;

            end;

              suppose

               A5: (l .: (T " {w})) <> ( {} F);

              

               A6: {( 0. F)} c= (l .: (T " {w}))

              proof

                let y be object;

                assume y in {( 0. F)};

                then

                 A7: y = ( 0. F) by TARSKI:def 1;

                ex z be object st z in (l .: (T " {w})) by A5, XBOOLE_0:def 1;

                hence thesis by A4, A7, TARSKI:def 1;

              end;

              (l .: (T " {w})) c= {( 0. F)} by A3, Th28;

              then (l .: (T " {w})) = {( 0. F)} by A6;

              hence thesis by RLVECT_2: 9;

            end;

          end;

          hence contradiction by A2, Def5;

        end;

        then

        consider x be object such that

         A8: x in (T " {w}) and

         A9: x in ( Carrier l) by XBOOLE_0: 3;

        

         A10: x in ( dom T) by A8, FUNCT_1:def 7;

        

         A11: (T . x) in {w} by A8, FUNCT_1:def 7;

        reconsider x as Element of V by A8;

        (T . x) = w by A11, TARSKI:def 1;

        hence thesis by A9, A10, FUNCT_1:def 6;

      end;

      hence thesis by VECTSP_6:def 4;

    end;

    theorem :: RANKNULL:30

    

     Th30: ( Carrier (T @ l)) c= (T .: ( Carrier l))

    proof

      (T @ l) is Linear_Combination of (T .: ( Carrier l)) by Th29;

      hence thesis by VECTSP_6:def 4;

    end;

    theorem :: RANKNULL:31

    

     Th31: for l,m be Linear_Combination of V st ( Carrier l) misses ( Carrier m) holds ( Carrier (l + m)) = (( Carrier l) \/ ( Carrier m))

    proof

      let l,m be Linear_Combination of V such that

       A1: ( Carrier l) misses ( Carrier m);

      thus ( Carrier (l + m)) c= (( Carrier l) \/ ( Carrier m)) by VECTSP_6: 23;

      thus (( Carrier l) \/ ( Carrier m)) c= ( Carrier (l + m))

      proof

        let v be object such that

         A2: v in (( Carrier l) \/ ( Carrier m));

        per cases by A2, XBOOLE_0:def 3;

          suppose

           A3: v in ( Carrier l);

          then

          reconsider v as Element of V;

           not v in ( Carrier m) by A1, A2, A3, XBOOLE_0: 5;

          then ((l + m) . v) = ((l . v) + (m . v)) & (m . v) = ( 0. F) by VECTSP_6: 22;

          then

           A4: ((l + m) . v) = (l . v) by RLVECT_1: 4;

          (l . v) <> ( 0. F) by A3, VECTSP_6: 2;

          hence thesis by A4;

        end;

          suppose

           A5: v in ( Carrier m);

          then

          reconsider v as Element of V;

           not v in ( Carrier l) by A1, A2, A5, XBOOLE_0: 5;

          then ((l + m) . v) = ((l . v) + (m . v)) & (l . v) = ( 0. F) by VECTSP_6: 22;

          then

           A6: ((l + m) . v) = (m . v) by RLVECT_1: 4;

          (m . v) <> ( 0. F) by A5, VECTSP_6: 2;

          hence thesis by A6;

        end;

      end;

    end;

    theorem :: RANKNULL:32

    

     Th32: for l,m be Linear_Combination of V st ( Carrier l) misses ( Carrier m) holds ( Carrier (l - m)) = (( Carrier l) \/ ( Carrier m))

    proof

      let l,m be Linear_Combination of V such that

       A1: ( Carrier l) misses ( Carrier m);

      ( Carrier ( - m)) = ( Carrier m) by VECTSP_6: 38;

      hence thesis by A1, Th31;

    end;

    theorem :: RANKNULL:33

    

     Th33: for A,B be 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

      let A,B be Subset of V such that

       A1: A c= B and

       A2: B is Basis of V;

      

       A3: (( Lin A) /\ ( Lin (B \ A))) = ( (0). V)

      proof

        set U = (( Lin A) /\ ( Lin (B \ A)));

        reconsider W = ( (0). V) as strict Subspace of U by VECTSP_4: 39;

        for v be Element of U holds v in W

        proof

          let v be Element of U;

          

           A4: B is linearly-independent by A2, VECTSP_7:def 3;

          

           A5: v in U;

          then v in ( Lin A) by VECTSP_5: 3;

          then

          consider l be Linear_Combination of A such that

           A6: v = ( Sum l) by VECTSP_7: 7;

          v in ( Lin (B \ A)) by A5, VECTSP_5: 3;

          then

          consider m be Linear_Combination of (B \ A) such that

           A7: v = ( Sum m) by VECTSP_7: 7;

          

           A8: ( 0. V) = (( Sum l) - ( Sum m)) by A6, A7, VECTSP_1: 19

          .= ( Sum (l - m)) by VECTSP_6: 47;

          

           A9: ( Carrier (l - m)) c= (( Carrier l) \/ ( Carrier m)) & (A \/ (B \ A)) = B by A1, VECTSP_6: 41, XBOOLE_1: 45;

          

           A10: ( Carrier l) c= A & ( Carrier m) c= (B \ A) by VECTSP_6:def 4;

          then (( Carrier l) \/ ( Carrier m)) c= (A \/ (B \ A)) by XBOOLE_1: 13;

          then ( Carrier (l - m)) c= B by A9;

          then

          reconsider n = (l - m) as Linear_Combination of B by VECTSP_6:def 4;

          A misses (B \ A) by XBOOLE_1: 79;

          then ( Carrier n) = (( Carrier l) \/ ( Carrier m)) by A10, Th32, XBOOLE_1: 64;

          then ( Carrier l) = {} by A8, A4, VECTSP_7:def 1;

          then l = ( ZeroLC V) by VECTSP_6:def 3;

          then ( Sum l) = ( 0. V) by VECTSP_6: 15;

          hence thesis by A6, VECTSP_4: 35;

        end;

        hence thesis by VECTSP_4: 32;

      end;

      ( (Omega). V) = (( Lin A) + ( Lin (B \ A)))

      proof

        set U = (( Lin A) + ( Lin (B \ A)));

        

         A11: ( [#] V) c= ( [#] U)

        proof

          let v be object;

          assume v in ( [#] V);

          then

          reconsider v as Element of V;

          v in ( Lin B) by A2, VECTSP_9: 10;

          then

          consider l be Linear_Combination of B such that

           A12: v = ( Sum l) by VECTSP_7: 7;

          set n = (l ! (B \ A));

          set m = (l ! A);

          

           A13: l = (m + n) by A1, Th27;

          ex v1,v2 be Element of V st v1 in ( Lin A) & v2 in ( Lin (B \ A)) & v = (v1 + v2)

          proof

            take ( Sum m), ( Sum n);

            thus thesis by A12, A13, VECTSP_6: 44, VECTSP_7: 7;

          end;

          then v in (( Lin A) + ( Lin (B \ A))) by VECTSP_5: 1;

          hence thesis;

        end;

        ( [#] U) c= ( [#] V) by VECTSP_4:def 2;

        then ( [#] U) = ( [#] V) by A11;

        hence thesis by VECTSP_4: 29;

      end;

      hence thesis by A3, VECTSP_5:def 4;

    end;

    theorem :: RANKNULL:34

    

     Th34: for A be Subset of V, l be Linear_Combination of A, v be Element of V st (T | A) is one-to-one & v in A holds ex X be Subset of V st X misses A & (T " {(T . v)}) = ( {v} \/ X)

    proof

      let A be Subset of V, l be Linear_Combination of A, v be Element of V such that

       A1: (T | A) is one-to-one and

       A2: v in A;

      set X = ((T " {(T . v)}) \ {v});

      

       A3: X misses A

      proof

        ( dom T) = ( [#] V) by Th7;

        then

         A4: ( dom (T | A)) = A by RELAT_1: 62;

        assume X meets A;

        then

        consider x be object such that

         A5: x in X and

         A6: x in A by XBOOLE_0: 3;

         not x in {v} by A5, XBOOLE_0:def 5;

        then

         A7: x <> v by TARSKI:def 1;

        x in (T " {(T . v)}) by A5, XBOOLE_0:def 5;

        then (T . x) in {(T . v)} by FUNCT_1:def 7;

        then

         A8: (T . x) = (T . v) by TARSKI:def 1;

        (T . x) = ((T | A) . x) by A6, FUNCT_1: 49;

        then ((T | A) . v) = ((T | A) . x) by A2, A8, FUNCT_1: 49;

        hence thesis by A1, A2, A6, A7, A4;

      end;

      take X;

       {v} c= (T " {(T . v)})

      proof

        let x be object;

        assume x in {v};

        then

         A9: x = v by TARSKI:def 1;

        ( dom T) = ( [#] V) & (T . v) in {(T . v)} by Th7, TARSKI:def 1;

        hence thesis by A9, FUNCT_1:def 7;

      end;

      hence thesis by A3, XBOOLE_1: 45;

    end;

    theorem :: RANKNULL:35

    

     Th35: for X be Subset of V st X misses ( Carrier l) & X <> {} holds (l .: X) = {( 0. F)}

    proof

      let X be Subset of V such that

       A1: X misses ( Carrier l) and

       A2: X <> {} ;

      ( dom l) = ( [#] V) by FUNCT_2: 92;

      then

       A3: (l .: X) <> {} by A2, RELAT_1: 119;

      (l .: X) c= {( 0. F)} by A1, Th28;

      hence thesis by A3, ZFMISC_1: 33;

    end;

    theorem :: RANKNULL:36

    

     Th36: for w be Element of W st w in ( Carrier (T @ l)) holds (T " {w}) meets ( Carrier l)

    proof

      let w be Element of W;

      assume w in ( Carrier (T @ l));

      then

       A1: ((T @ l) . w) <> ( 0. F) by VECTSP_6: 2;

      assume

       A2: (T " {w}) misses ( Carrier l);

      per cases ;

        suppose (T " {w}) = {} ;

        

        then ( Sum (l .: (T " {w}))) = ( Sum ( {} F))

        .= ( 0. F) by RLVECT_2: 8;

        hence thesis by A1, Def5;

      end;

        suppose (T " {w}) <> {} ;

        then (l .: (T " {w})) = {( 0. F)} by A2, Th35;

        then ( Sum (l .: (T " {w}))) = ( 0. F) by RLVECT_2: 9;

        hence thesis by A1, Def5;

      end;

    end;

    theorem :: RANKNULL:37

    

     Th37: for v be Element of V st (T | ( Carrier l)) is one-to-one & v in ( Carrier l) holds ((T @ l) . (T . v)) = (l . v)

    proof

      let v be Element of V such that

       A1: (T | ( Carrier l)) is one-to-one and

       A2: v in ( Carrier l);

      consider X be Subset of V such that

       A3: X misses ( Carrier l) and

       A4: (T " {(T . v)}) = ( {v} \/ X) by A1, A2, Th34;

      per cases ;

        suppose

         A5: X = {} ;

        

         A6: ( dom l) = ( [#] V) by FUNCT_2: 92;

        (l .: {v}) = ( Im (l,v))

        .= {(l . v)} by A6, FUNCT_1: 59;

        then ( Sum (l .: (T " {(T . v)}))) = (l . v) by A4, A5, RLVECT_2: 9;

        hence thesis by Def5;

      end;

        suppose

         A7: X <> {} ;

        

         A8: (l .: X) c= {( 0. F)}

        proof

          let y be object;

          assume y in (l .: X);

          then

          consider x be object such that

           A9: x in ( dom l) and

           A10: x in X and

           A11: y = (l . x) by FUNCT_1:def 6;

          

           A12: not x in ( Carrier l) by A3, A10, XBOOLE_0:def 4;

          reconsider x as Element of V by A9;

          (l . x) = ( 0. F) by A12;

          hence thesis by A11, TARSKI:def 1;

        end;

        

         A13: (l .: X) misses (l .: {v})

        proof

          assume (l .: X) meets (l .: {v});

          then

          consider x be object such that

           A14: x in (l .: X) and

           A15: x in (l .: {v}) by XBOOLE_0: 3;

          

           A16: ( dom l) = ( [#] V) by FUNCT_2: 92;

          (l .: {v}) = ( Im (l,v))

          .= {(l . v)} by A16, FUNCT_1: 59;

          then

           A17: x = (l . v) by A15, TARSKI:def 1;

          x = ( 0. F) by A8, A14, TARSKI:def 1;

          hence thesis by A2, A17, VECTSP_6: 2;

        end;

        

         A18: ( dom l) = ( [#] V) by FUNCT_2: 92;

         {( 0. F)} c= (l .: X)

        proof

          consider y be object such that

           A19: y in X by A7, XBOOLE_0:def 1;

          

           A20: not y in ( Carrier l) by A3, A19, XBOOLE_0:def 4;

          reconsider y as Element of V by A19;

          let x be object;

          assume x in {( 0. F)};

          then x = ( 0. F) by TARSKI:def 1;

          then (l . y) = x by A20;

          hence thesis by A18, A19, FUNCT_1:def 6;

        end;

        then

         A21: (l .: X) = {( 0. F)} by A8;

        

         A22: (l .: {v}) = ( Im (l,v))

        .= {(l . v)} by A18, FUNCT_1: 59;

        (l .: (T " {(T . v)})) = ((l .: {v}) \/ (l .: X)) by A4, RELAT_1: 120;

        

        then ( Sum (l .: (T " {(T . v)}))) = (( Sum (l .: {v})) + ( Sum (l .: X))) by A13, RLVECT_2: 12

        .= ((l . v) + ( Sum {( 0. F)})) by A22, A21, RLVECT_2: 9

        .= ((l . v) + ( 0. F)) by RLVECT_2: 9

        .= (l . v) by RLVECT_1: 4;

        hence thesis by Def5;

      end;

    end;

    theorem :: RANKNULL:38

    

     Th38: for G be FinSequence of V st ( rng G) = ( Carrier l) & (T | ( Carrier l)) is one-to-one holds (T * (l (#) G)) = ((T @ l) (#) (T * G))

    proof

      let G be FinSequence of V such that

       A1: ( rng G) = ( Carrier l) and

       A2: (T | ( Carrier l)) is one-to-one;

      reconsider R = ((T @ l) (#) (T * G)) as FinSequence of W;

      reconsider L = (T * (l (#) G)) as FinSequence of W;

      

       A3: ( len R) = ( len (T * G)) by VECTSP_6:def 5

      .= ( len G) by FINSEQ_2: 33;

      

       A4: ( len L) = ( len (l (#) G)) by FINSEQ_2: 33

      .= ( len G) by VECTSP_6:def 5;

      for k be Nat st 1 <= k & k <= ( len L) holds (L . k) = (R . k)

      proof

        

         A5: ( dom R) = ( Seg ( len G)) by A3, FINSEQ_1:def 3;

        let k be Nat such that

         A6: 1 <= k & k <= ( len L);

        reconsider gk = (G /. k) as Element of V;

        ( len (l (#) G)) = ( len G) by VECTSP_6:def 5;

        then

         A7: ( dom (l (#) G)) = ( Seg ( len G)) by FINSEQ_1:def 3;

        

         A8: k in ( dom (l (#) G)) by A4, A6, A7;

        then

         A9: k in ( dom G) by A7, FINSEQ_1:def 3;

        then

         A10: (G . k) = (G /. k) by PARTFUN1:def 6;

        then

        reconsider Gk = (G . k) as Element of V;

        ((T * G) . k) = (T . Gk) by A9, FUNCT_1: 13;

        then

        reconsider TGk = ((T * G) . k) as Element of W;

        ((l (#) G) . k) = ((l . gk) * gk) by A8, VECTSP_6:def 5;

        

        then

         A11: (L . k) = (T . ((l . gk) * gk)) by A8, FUNCT_1: 13

        .= ((l . gk) * (T . gk)) by MOD_2:def 2

        .= ((l . Gk) * TGk) by A9, A10, FUNCT_1: 13;

        (G . k) in ( rng G) & ((T * G) . k) = (T . (G . k)) by A9, FUNCT_1: 3, FUNCT_1: 13;

        then

         A12: ((T @ l) . ((T * G) . k)) = (l . (G . k)) by A1, A2, Th37;

        ( dom T) = ( [#] V) by Th7;

        then ( dom (T * G)) = ( dom G) by A1, RELAT_1: 27;

        then ((T * G) /. k) = ((T * G) . k) by A9, PARTFUN1:def 6;

        hence thesis by A7, A8, A11, A5, A12, VECTSP_6:def 5;

      end;

      hence thesis by A4, A3;

    end;

    theorem :: RANKNULL:39

    

     Th39: (T | ( Carrier l)) is one-to-one implies (T .: ( Carrier l)) = ( Carrier (T @ l))

    proof

      assume

       A1: (T | ( Carrier l)) is one-to-one;

      

       A2: (T .: ( Carrier l)) c= ( Carrier (T @ l))

      proof

        let w be object;

        assume w in (T .: ( Carrier l));

        then

        consider v be object such that

         A3: v in ( dom T) and

         A4: v in ( Carrier l) and

         A5: (T . v) = w by FUNCT_1:def 6;

        reconsider v as Element of V by A3;

        ((T @ l) . (T . v)) = (l . v) & (l . v) <> ( 0. F) by A1, A4, Th37, VECTSP_6: 2;

        hence thesis by A5;

      end;

      ( Carrier (T @ l)) c= (T .: ( Carrier l)) by Th30;

      hence thesis by A2;

    end;

    theorem :: RANKNULL:40

    

     Th40: for A be Subset of V, B be Basis of V, l be Linear_Combination of (B \ A) st A is Basis of ( ker T) & A c= B holds (T . ( Sum l)) = ( Sum (T @ l))

    proof

      let A be Subset of V, B be Basis of V, l be Linear_Combination of (B \ A);

      assume A is Basis of ( ker T) & A c= B;

      then

       A1: (T | (B \ A)) is one-to-one by Th22;

      ( Carrier l) c= (B \ A) by VECTSP_6:def 4;

      then

       A2: ((T | (B \ A)) | ( Carrier l)) = (T | ( Carrier l)) by RELAT_1: 74;

      then

       A3: (T | ( Carrier l)) is one-to-one by A1, FUNCT_1: 52;

      consider G be FinSequence of V such that

       A4: G is one-to-one and

       A5: ( rng G) = ( Carrier l) and

       A6: ( Sum l) = ( Sum (l (#) G)) by VECTSP_6:def 6;

      set H = (T * G);

      reconsider H as FinSequence of W;

      

       A7: ( rng H) = (T .: ( Carrier l)) by A5, RELAT_1: 127

      .= ( Carrier (T @ l)) by A3, Th39;

      ( dom T) = ( [#] V) by Th7;

      then H is one-to-one by A4, A5, A1, A2, Th1, FUNCT_1: 52;

      then

       A8: ( Sum (T @ l)) = ( Sum ((T @ l) (#) H)) by A7, VECTSP_6:def 6;

      (T * (l (#) G)) = ((T @ l) (#) H) by A5, A3, Th38;

      hence thesis by A6, A8, MATRLIN: 16;

    end;

    theorem :: RANKNULL:41

    

     Th41: for X be Subset of V st X is linearly-dependent holds ex l be Linear_Combination of X st ( Carrier l) <> {} & ( Sum l) = ( 0. V)

    proof

      let X be Subset of V;

      assume X is linearly-dependent;

      then not (for l be Linear_Combination of X st ( Sum l) = ( 0. V) holds ( Carrier l) = {} ) by VECTSP_7:def 1;

      hence thesis;

    end;

    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

       A1: (T | X) is one-to-one;

      :: RANKNULL:def6

      func T # l -> Linear_Combination of X equals

      : Def6: ((l * T) +* ((V \ X) --> ( 0. F)));

      coherence

      proof

        ( rng (l * T)) c= ( rng l) & ( rng l) c= ( [#] F) by FUNCT_2: 92, RELAT_1: 26;

        then

         A2: ( rng (l * T)) c= ( [#] F);

        ( dom l) = ( [#] W) by FUNCT_2: 92;

        then ( rng T) c= ( dom l) by Th7;

        then

         A3: ( dom (l * T)) = ( dom T) by RELAT_1: 27;

        set f = ((l * T) +* ((V \ X) --> ( 0. F)));

        

         A4: ( dom ((V \ X) --> ( 0. F))) = (( [#] V) \ X);

        ( rng ((V \ X) --> ( 0. F))) c= {( 0. F)} by FUNCOP_1: 13;

        then ( rng ((V \ X) --> ( 0. F))) c= ( [#] F) by XBOOLE_1: 1;

        then ( rng f) c= (( rng (l * T)) \/ ( rng ((V \ X) --> ( 0. F)))) & (( rng (l * T)) \/ ( rng ((V \ X) --> ( 0. F)))) c= ( [#] F) by A2, FUNCT_4: 17, XBOOLE_1: 8;

        then

         A5: ( rng f) c= ( [#] F);

        ( dom T) = ( [#] V) & (( [#] V) \/ (( [#] V) \ X)) = ( [#] V) by Th7, XBOOLE_1: 12;

        then ( dom f) = ( [#] V) by A3, A4, FUNCT_4:def 1;

        then

        reconsider f as Element of ( Funcs (( [#] V),( [#] F))) by A5, FUNCT_2:def 2;

        ex T be finite Subset of V st for v be Element of V st not v in T holds (f . v) = ( 0. F)

        proof

          set C = { v where v be Element of V : (f . v) <> ( 0. F) };

          C c= ( [#] V)

          proof

            let x be object;

            assume x in C;

            then ex v be Element of V st v = x & (f . v) <> ( 0. F);

            hence thesis;

          end;

          then

          reconsider C as Subset of V;

          ex g be Function st g is one-to-one & ( dom g) = C & ( rng g) c= ( Carrier l)

          proof

            set S = ((T " ( Carrier l)) /\ X);

            set g = (T | S);

            take g;

            

             A6: C c= S

            proof

              let x be object such that

               A7: x in C;

              

               A8: ex v be Element of V st v = x & (f . v) <> ( 0. F) by A7;

              reconsider x as Element of V by A7;

               A9:

              now

                assume not x in X;

                then

                 A10: x in (V \ X) by XBOOLE_0:def 5;

                then x in ( dom ((V \ X) --> ( 0. F)));

                then (f . x) = (((V \ X) --> ( 0. F)) . x) by FUNCT_4: 13;

                hence contradiction by A8, A10, FUNCOP_1: 7;

              end;

              then not x in (V \ X) by XBOOLE_0:def 5;

              then

               A11: (f . x) = ((l * T) . x) by A4, FUNCT_4: 11;

              

               A12: ( dom T) = ( [#] V) by Th7;

              then ((l * T) . x) = (l . (T . x)) by FUNCT_1: 13;

              then (T . x) in ( Carrier l) by A8, A11;

              then x in (T " ( Carrier l)) by A12, FUNCT_1:def 7;

              hence thesis by A9, XBOOLE_0:def 4;

            end;

            

             A13: ( dom T) = ( [#] V) by Th7;

            

             A14: ( rng g) c= ( Carrier l)

            proof

              let y be object;

              assume y in ( rng g);

              then

              consider x be object such that

               A15: x in ( dom g) and

               A16: y = (g . x) by FUNCT_1:def 3;

              x in (T " ( Carrier l)) by A15, XBOOLE_0:def 4;

              then (T . x) in ( Carrier l) by FUNCT_1:def 7;

              hence thesis by A15, A16, FUNCT_1: 49;

            end;

            S c= C

            proof

              let x be object such that

               A17: x in S;

              

               A18: x in X by A17, XBOOLE_0:def 4;

              

               A19: x in (T " ( Carrier l)) by A17, XBOOLE_0:def 4;

              then

               A20: x in ( dom T) by FUNCT_1:def 7;

              

               A21: (T . x) in ( Carrier l) by A19, FUNCT_1:def 7;

              reconsider x as Element of V by A17;

              

               A22: (l . (T . x)) <> ( 0. F) by A21, VECTSP_6: 2;

               not x in ( dom ((V \ X) --> ( 0. F))) by A18, XBOOLE_0:def 5;

              then

               A23: (f . x) = ((l * T) . x) by FUNCT_4: 11;

              ((l * T) . x) = (l . (T . x)) by A20, FUNCT_1: 13;

              hence thesis by A23, A22;

            end;

            then S = C by A6;

            hence thesis by A1, A13, A14, Th2, RELAT_1: 62, XBOOLE_1: 17;

          end;

          then ( card C) c= ( card ( Carrier l)) by CARD_1: 10;

          then

          reconsider C as finite Subset of V;

          take C;

          thus thesis;

        end;

        then

        reconsider f as Linear_Combination of V by VECTSP_6:def 1;

        ( Carrier f) c= X

        proof

          let x be object such that

           A24: x in ( Carrier f);

          reconsider x as Element of V by A24;

          now

            assume not x in X;

            then

             A25: x in (V \ X) by XBOOLE_0:def 5;

            

            then (f . x) = (((V \ X) --> ( 0. F)) . x) by A4, FUNCT_4: 13

            .= ( 0. F) by A25, FUNCOP_1: 7;

            hence contradiction by A24, VECTSP_6: 2;

          end;

          hence thesis;

        end;

        hence thesis by VECTSP_6:def 4;

      end;

    end

    theorem :: RANKNULL:42

    

     Th42: for X be Subset of V, l be Linear_Combination of (T .: X), v be Element of V st v in X & (T | X) is one-to-one holds ((T # l) . v) = (l . (T . v))

    proof

      let X be Subset of V, l be Linear_Combination of (T .: X), v be Element of V;

      assume v in X & (T | X) is one-to-one;

      then ( not v in ( dom ((V \ X) --> ( 0. F)))) & (T # l) = ((l * T) +* ((V \ X) --> ( 0. F))) by Def6, XBOOLE_0:def 5;

      then

       A1: ((T # l) . v) = ((l * T) . v) by FUNCT_4: 11;

      ( dom T) = ( [#] V) by Th7;

      hence thesis by A1, FUNCT_1: 13;

    end;

    theorem :: RANKNULL:43

    

     Th43: for X be Subset of V, l be Linear_Combination of (T .: X) st (T | X) is one-to-one holds (T @ (T # l)) = l

    proof

      let X be Subset of V, l be Linear_Combination of (T .: X) such that

       A1: (T | X) is one-to-one;

      let w be Element of W;

      set m = (T @ (T # l));

      per cases ;

        suppose

         A2: w in ( Carrier l);

        then

         A3: (l . w) <> ( 0. F) by VECTSP_6: 2;

        

         A4: ( dom (T # l)) = ( [#] V) by FUNCT_2: 92;

        ( Carrier l) c= (T .: X) by VECTSP_6:def 4;

        then

        consider v be object such that

         A5: v in ( dom T) and

         A6: v in X and

         A7: w = (T . v) by A2, FUNCT_1:def 6;

        reconsider v as Element of V by A5;

        consider B be Subset of V such that

         A8: B misses X and

         A9: (T " {(T . v)}) = ( {v} \/ B) by A1, A6, Th34;

        

         A10: ((T # l) . v) = (l . (T . v)) by A1, A6, Th42;

        

         A11: ((T # l) .: {v}) = ( Im ((T # l),v))

        .= {((T # l) . v)} by A4, FUNCT_1: 59;

        

         A12: (m . w) = ( Sum ((T # l) .: (T " {(T . v)}))) by A7, Def5

        .= ( Sum ( {(l . (T . v))} \/ ((T # l) .: B))) by A9, A10, A11, RELAT_1: 120;

        per cases ;

          suppose B = {} ;

          

          then (m . w) = ( Sum ( {(l . (T . v))} \/ ( {} F))) by A12

          .= (l . w) by A7, RLVECT_2: 9;

          hence thesis;

        end;

          suppose

           A13: B <> {} ;

          ( Carrier (T # l)) c= X by VECTSP_6:def 4;

          then B misses ( Carrier (T # l)) by A8, XBOOLE_1: 63;

          

          then (m . w) = ( Sum ( {(l . (T . v))} \/ {( 0. F)})) by A12, A13, Th35

          .= (( Sum {(l . (T . v))}) + ( Sum {( 0. F)})) by A3, A7, RLVECT_2: 12, ZFMISC_1: 11

          .= ((l . (T . v)) + ( Sum {( 0. F)})) by RLVECT_2: 9

          .= ((l . (T . v)) + ( 0. F)) by RLVECT_2: 9

          .= (l . w) by A7, RLVECT_1: 4;

          hence thesis;

        end;

      end;

        suppose

         A14: not w in ( Carrier l);

        then

         A15: (l . w) = ( 0. F);

        now

          assume

           A16: (m . w) <> ( 0. F);

          then w in ( Carrier m);

          then (T " {w}) meets ( Carrier (T # l)) by Th36;

          then

          consider v be Element of V such that

           A17: v in (T " {w}) and

           A18: v in ( Carrier (T # l)) by Th3;

          (T . v) in {w} by A17, FUNCT_1:def 7;

          then

           A19: (T . v) = w by TARSKI:def 1;

          

           A20: ( Carrier (T # l)) c= X by VECTSP_6:def 4;

          then (T | ( Carrier (T # l))) is one-to-one by A1, Th2;

          

          then (m . w) = ((T # l) . v) by A18, A19, Th37

          .= ( 0. F) by A1, A15, A18, A19, A20, Th42;

          hence contradiction by A16;

        end;

        hence thesis by A14;

      end;

    end;

    begin

    definition

      let F be Field, V,W be finite-dimensional VectSp of F, T be linear-transformation of V, W;

      :: RANKNULL:def7

      func rank (T) -> Nat equals ( dim ( im T));

      coherence ;

      :: RANKNULL:def8

      func nullity (T) -> Nat equals ( dim ( ker T));

      coherence ;

    end

    ::$Notion-Name

    theorem :: RANKNULL:44

    

     Th44: for V,W be finite-dimensional VectSp of F, T be linear-transformation of V, W holds ( dim V) = (( rank T) + ( nullity T))

    proof

      let V,W be finite-dimensional VectSp of F, T be linear-transformation of V, W;

      set A = the finite Basis of ( ker T);

      reconsider A9 = A as Subset of V by Th19;

      consider B be Basis of V such that

       A1: A c= B by VECTSP_9: 13;

      reconsider B as finite Subset of V by VECTSP_9: 20;

      reconsider X = (B \ A9) as finite Subset of B by XBOOLE_1: 36;

      reconsider X as finite Subset of V;

      

       A2: B = (A \/ X) by A1, XBOOLE_1: 45;

      reconsider B as finite Basis of V;

      reconsider A as finite Basis of ( ker T);

      reconsider C = (T .: X) as finite Subset of W;

      

       A3: (T | X) is one-to-one by A1, Th22;

      

       A4: C is linearly-independent

      proof

        assume C is linearly-dependent;

        then

        consider l be Linear_Combination of C such that

         A5: ( Carrier l) <> {} and

         A6: ( Sum l) = ( 0. W) by Th41;

        ex m be Linear_Combination of X st l = (T @ m)

        proof

          reconsider l9 = l as Linear_Combination of (T .: X);

          set m = (T # l9);

          take m;

          thus thesis by A3, Th43;

        end;

        then

        consider m be Linear_Combination of (B \ A9) such that

         A7: l = (T @ m);

        (T . ( Sum m)) = ( 0. W) by A1, A6, A7, Th40;

        then ( Sum m) in ( ker T) by Th10;

        then ( Sum m) in ( Lin A) by VECTSP_7:def 3;

        then ( Sum m) in ( Lin A9) by VECTSP_9: 17;

        then

        consider n be Linear_Combination of A9 such that

         A8: ( Sum m) = ( Sum n) by VECTSP_7: 7;

        

         A9: ( Carrier (m - n)) c= (( Carrier m) \/ ( Carrier n)) & ((B \ A9) \/ A9) = B by A1, VECTSP_6: 41, XBOOLE_1: 45;

        

         A10: ( Carrier m) c= (B \ A9) & ( Carrier n) c= A by VECTSP_6:def 4;

        then (( Carrier m) \/ ( Carrier n)) c= ((B \ A9) \/ A) by XBOOLE_1: 13;

        then ( Carrier (m - n)) c= B by A9;

        then

        reconsider o = (m - n) as Linear_Combination of B by VECTSP_6:def 4;

        

         A11: B is linearly-independent by VECTSP_7:def 3;

        (( Sum m) - ( Sum n)) = ( 0. V) by A8, VECTSP_1: 19;

        then ( Sum (m - n)) = ( 0. V) by VECTSP_6: 47;

        then

         A12: ( Carrier o) = {} by A11, VECTSP_7:def 1;

        A9 misses (B \ A9) by XBOOLE_1: 79;

        then ( Carrier (m - n)) = (( Carrier m) \/ ( Carrier n)) by A10, Th32, XBOOLE_1: 64;

        then ( Carrier m) = {} by A12;

        then (T .: ( Carrier m)) = {} ;

        hence thesis by A5, A7, Th30, XBOOLE_1: 3;

      end;

      ( dom T) = ( [#] V) by Th7;

      then X c= ( dom (T | X)) by RELAT_1: 62;

      then (X,((T | X) .: X)) are_equipotent by A3, CARD_1: 33;

      then (X,C) are_equipotent by RELAT_1: 129;

      then

       A13: ( card C) = ( card X) by CARD_1: 5;

      reconsider C as finite Subset of ( im T) by Th12;

      reconsider L = ( Lin C) as strict Subspace of ( im T);

      for v be Element of ( im T) holds v in L

      proof

        reconsider A9 = A as Subset of V by Th19;

        let v be Element of ( im T);

        reconsider v9 = v as Element of W by VECTSP_4: 10;

        reconsider C9 = C as Subset of W;

        v in ( im T);

        then

        consider u be Element of V such that

         A14: (T . u) = v9 by Th13;

        V is_the_direct_sum_of (( Lin A9),( Lin (B \ A9))) by A1, Th33;

        then

         A15: ( (Omega). V) = (( Lin A9) + ( Lin (B \ A9))) by VECTSP_5:def 4;

        u in ( (Omega). V);

        then

        consider u1,u2 be Element of V such that

         A16: u1 in ( Lin A9) and

         A17: u2 in ( Lin (B \ A9)) and

         A18: u = (u1 + u2) by A15, VECTSP_5: 1;

        consider l be Linear_Combination of (B \ A9) such that

         A19: u2 = ( Sum l) by A17, VECTSP_7: 7;

        ( Lin A) = ( ker T) by VECTSP_7:def 3;

        then u1 in ( ker T) by A16, VECTSP_9: 17;

        then

         A20: (T . u1) = ( 0. W) by Th10;

        (T @ l) is Linear_Combination of (T .: ( Carrier l)) & ( Carrier l) c= (B \ A9) by Th29, VECTSP_6:def 4;

        then

        reconsider m = (T @ l) as Linear_Combination of C9 by RELAT_1: 123, VECTSP_6: 4;

        (T . u) = ((T . u1) + (T . u2)) by A18, VECTSP_1:def 20;

        then

         A21: (T . u) = (T . u2) by A20, RLVECT_1: 4;

        ex m be Linear_Combination of C9 st v = ( Sum m)

        proof

          take m;

          thus thesis by A1, A14, A21, A19, Th40;

        end;

        then v in ( Lin C9) by VECTSP_7: 7;

        hence thesis by VECTSP_9: 17;

      end;

      then

       A22: ( Lin C) = ( im T) by VECTSP_4: 32;

      reconsider C as linearly-independent Subset of ( im T) by A4, VECTSP_9: 12;

      reconsider C as finite Basis of ( im T) by A22, VECTSP_7:def 3;

      

       A23: ( nullity T) = ( card A) & ( rank T) = ( card C) by VECTSP_9:def 1;

      ( dim V) = ( card B) by VECTSP_9:def 1

      .= (( rank T) + ( nullity T)) by A2, A13, A23, CARD_2: 40, XBOOLE_1: 79;

      hence thesis;

    end;

    theorem :: RANKNULL:45

    for V,W be finite-dimensional VectSp of F, T be linear-transformation of V, W st T is one-to-one holds ( dim V) = ( rank T)

    proof

      let V,W be finite-dimensional VectSp of F, T be linear-transformation of V, W;

      assume T is one-to-one;

      then ( ker T) = ( (0). V) by Th15;

      then

       A1: ( nullity T) = 0 by Th16;

      ( dim V) = (( rank T) + ( nullity T)) by Th44

      .= ( rank T) by A1;

      hence thesis;

    end;