mod_3.miz



    begin

    

     Lm1: for R be Ring, a be Scalar of R holds ( - a) = ( 0. R) implies a = ( 0. R)

    proof

      let R be Ring, a be Scalar of R;

      assume ( - a) = ( 0. R);

      then ( - ( - a)) = ( 0. R) by RLVECT_1: 12;

      hence thesis by RLVECT_1: 17;

    end;

    theorem :: MOD_3:1

    

     Th1: for R be non degenerated add-associative right_zeroed right_complementable non empty doubleLoopStr holds ( 0. R) <> ( - ( 1. R))

    proof

      let R be non degenerated add-associative right_zeroed right_complementable non empty doubleLoopStr;

      assume ( 0. R) = ( - ( 1. R));

      

      then ( 0. R) = ( - ( - ( 1. R))) by RLVECT_1: 12

      .= ( 1. R) by RLVECT_1: 17;

      hence contradiction;

    end;

    reserve x,y for object,

R for Ring,

V for LeftMod of R,

L for Linear_Combination of V,

a for Scalar of R,

v,u for Vector of V,

F,G for FinSequence of the carrier of V,

C for finite Subset of V;

    reserve X,Y,Z for set,

A,B for Subset of V,

T for finite Subset of V,

l for Linear_Combination of A,

f,g for Function of the carrier of V, the carrier of R;

    theorem :: MOD_3:2

    ( Carrier L) c= C implies ex F st F is one-to-one & ( rng F) = C & ( Sum L) = ( Sum (L (#) F)) by VECTSP_7: 21;

    theorem :: MOD_3:3

    ( Sum (a * L)) = (a * ( Sum L)) by VECTSP_7: 22;

    theorem :: MOD_3:4

    

     Th4: x in ( Lin A) iff ex l st x = ( Sum l) by VECTSP_7: 7;

    theorem :: MOD_3:5

    

     Th5: x in A implies x in ( Lin A) by VECTSP_7: 8;

    theorem :: MOD_3:6

    

     Th6: ( Lin ( {} the carrier of V)) = ( (0). V) by VECTSP_7: 9;

    theorem :: MOD_3:7

    ( Lin A) = ( (0). V) implies A = {} or A = {( 0. V)} by VECTSP_7: 10;

    theorem :: MOD_3:8

    

     Th8: for R be non degenerated Ring, V be LeftMod of R, A be Subset of V holds for W be strict Subspace of V st A = the carrier of W holds ( Lin A) = W

    proof

      let R be non degenerated Ring, V be LeftMod of R, A be Subset of V;

      let W be strict Subspace of V;

      assume that

       A2: A = the carrier of W;

      now

        let v be Vector of V;

        thus v in ( Lin A) implies v in W

        proof

          assume v in ( Lin A);

          then

           A3: ex l be Linear_Combination of A st v = ( Sum l) by Th4;

          

           A1: ( 0. R) <> ( 1. R);

          A is linearly-closed by A2, VECTSP_4: 33;

          then v in the carrier of W by A1, A2, A3, VECTSP_6: 14;

          hence thesis by STRUCT_0:def 5;

        end;

        v in W iff v in the carrier of W by STRUCT_0:def 5;

        hence v in W implies v in ( Lin A) by A2, Th5;

      end;

      hence thesis by VECTSP_4: 30;

    end;

    theorem :: MOD_3:9

    for R be non degenerated Ring holds for V be strict LeftMod of R holds for A be Subset of V st A = the carrier of V holds ( Lin A) = V

    proof

      let R be non degenerated Ring;

      let V be strict LeftMod of R;

      let A be Subset of V;

      assume A = the carrier of V;

      then A = the carrier of ( (Omega). V);

      hence thesis by Th8;

    end;

    theorem :: MOD_3:10

    

     Th10: A c= B implies ( Lin A) is Subspace of ( Lin B) by VECTSP_7: 13;

    theorem :: MOD_3:11

    ( Lin A) = V & A c= B implies ( Lin B) = V

    proof

      assume that

       A1: ( Lin A) = V and

       A2: A c= B;

      V is Subspace of ( Lin B) by A1, A2, Th10;

      hence thesis by A1, VECTSP_4: 25;

    end;

    theorem :: MOD_3:12

    ( Lin (A \/ B)) = (( Lin A) + ( Lin B)) by VECTSP_7: 15;

    theorem :: MOD_3:13

    ( Lin (A /\ B)) is Subspace of (( Lin A) /\ ( Lin B)) by VECTSP_7: 16;

    theorem :: MOD_3:14

    

     Th14: ( (0). V) is free

    proof

      set W = ( (0). V);

      reconsider B9 = ( {} the carrier of V) as Subset of W by SUBSET_1: 1;

      reconsider V9 = V as Subspace of V by VECTSP_4: 24;

      

       A1: B9 = ( {} the carrier of W);

      then

       A2: B9 is linearly-independent;

      ( (0). V9) = ( (0). W) by VECTSP_4: 37;

      then ( Lin B9) = W by A1, Th6;

      then B9 is base by A2;

      hence thesis;

    end;

    registration

      let R;

      cluster strict free for LeftMod of R;

      existence

      proof

        set V = the LeftMod of R;

        take ( (0). V);

        thus thesis by Th14;

      end;

    end

    reserve R for Skew-Field;

    reserve a,b for Scalar of R;

    reserve V for LeftMod of R;

    reserve v,v1,v2,u for Vector of V;

    reserve f for Function of the carrier of V, the carrier of R;

    

     Lm2: a <> ( 0. R) implies ((a " ) * (a * v)) = (( 1. R) * v) & (((a " ) * a) * v) = (( 1. R) * v)

    proof

      assume

       A1: a <> ( 0. R);

      

      hence ((a " ) * (a * v)) = v by VECTSP_2: 31

      .= (( 1. R) * v) by VECTSP_1:def 17;

      thus thesis by A1, VECTSP_2: 9;

    end;

    theorem :: MOD_3:15

     {v} is linearly-independent iff v <> ( 0. V)

    proof

      thus {v} is linearly-independent implies v <> ( 0. V)

      proof

        assume {v} is linearly-independent;

        then not ( 0. V) in {v} by VECTSP_7: 2;

        hence thesis by TARSKI:def 1;

      end;

      assume

       A2: v <> ( 0. V);

      let l be Linear_Combination of {v};

      

       A3: ( Carrier l) c= {v} by VECTSP_6:def 4;

      assume

       A4: ( Sum l) = ( 0. V);

      now

        per cases by A3, ZFMISC_1: 33;

          suppose ( Carrier l) = {} ;

          hence thesis;

        end;

          suppose

           A5: ( Carrier l) = {v};

          

           A6: ( 0. V) = ((l . v) * v) by A4, VECTSP_6: 17;

           not v in ( Carrier l) by A2, A6, VECTSP_2: 30, VECTSP_6: 2;

          hence thesis by A5, TARSKI:def 1;

        end;

      end;

      hence thesis;

    end;

    theorem :: MOD_3:16

    

     Th16: v1 <> v2 & {v1, v2} is linearly-independent iff v2 <> ( 0. V) & for a holds v1 <> (a * v2)

    proof

      thus v1 <> v2 & {v1, v2} is linearly-independent implies v2 <> ( 0. V) & for a holds v1 <> (a * v2)

      proof

        deffunc F( Element of V) = ( 0. R);

        assume that

         A2: v1 <> v2 and

         A3: {v1, v2} is linearly-independent;

        thus v2 <> ( 0. V) by A3, VECTSP_7: 28;

        let a;

        consider f such that

         A4: (f . v1) = ( - ( 1. R)) & (f . v2) = a and

         A5: for v be Element of V st v <> v1 & v <> v2 holds (f . v) = F(v) from FUNCT_2:sch 7( A2);

        reconsider f as Element of ( Funcs (the carrier of V,the carrier of R)) by FUNCT_2: 8;

        now

          let v;

          assume not v in {v1, v2};

          then v <> v1 & v <> v2 by TARSKI:def 2;

          hence (f . v) = ( 0. R) by A5;

        end;

        then

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

        ( Carrier f) c= {v1, v2}

        proof

          let x be object;

          assume x in ( Carrier f);

          then

           A6: ex u st x = u & (f . u) <> ( 0. R);

          assume not x in {v1, v2};

          then x <> v1 & x <> v2 by TARSKI:def 2;

          hence thesis by A5, A6;

        end;

        then

        reconsider f as Linear_Combination of {v1, v2} by VECTSP_6:def 4;

         A7:

        now

          assume not v1 in ( Carrier f);

          then ( 0. R) = ( - ( 1. R)) by A4;

          hence contradiction by Th1;

        end;

        set w = (a * v2);

        assume v1 = (a * v2);

        

        then ( Sum f) = ((( - ( 1. R)) * w) + w) by A2, A4, VECTSP_6: 18

        .= (( - w) + w) by VECTSP_1: 14

        .= ( 0. V) by RLVECT_1: 5;

        hence thesis by A3, A7;

      end;

      assume

       A8: v2 <> ( 0. V);

      assume

       A9: for a holds v1 <> (a * v2);

      

       A10: (( 1. R) * v2) = v2 by VECTSP_1:def 17;

      hence v1 <> v2 by A9;

      let l be Linear_Combination of {v1, v2};

      assume that

       A11: ( Sum l) = ( 0. V) and

       A12: ( Carrier l) <> {} ;

      

       A13: ( 0. V) = (((l . v1) * v1) + ((l . v2) * v2)) by A9, A10, A11, VECTSP_6: 18;

      set x = the Element of ( Carrier l);

      ( Carrier l) c= {v1, v2} by VECTSP_6:def 4;

      then

       A14: x in {v1, v2} by A12;

      x in ( Carrier l) by A12;

      then

       A15: ex u st x = u & (l . u) <> ( 0. R);

      now

        per cases by A15, A14, TARSKI:def 2;

          suppose

           A16: (l . v1) <> ( 0. R);

          ( 0. V) = (((l . v1) " ) * (((l . v1) * v1) + ((l . v2) * v2))) by A13, VECTSP_2: 30

          .= ((((l . v1) " ) * ((l . v1) * v1)) + (((l . v1) " ) * ((l . v2) * v2))) by VECTSP_1:def 14

          .= (((((l . v1) " ) * (l . v1)) * v1) + (((l . v1) " ) * ((l . v2) * v2))) by VECTSP_1:def 16

          .= (((((l . v1) " ) * (l . v1)) * v1) + ((((l . v1) " ) * (l . v2)) * v2)) by VECTSP_1:def 16

          .= ((( 1. R) * v1) + ((((l . v1) " ) * (l . v2)) * v2)) by A16, Lm2

          .= (v1 + ((((l . v1) " ) * (l . v2)) * v2)) by VECTSP_1:def 17;

          

          then v1 = ( - ((((l . v1) " ) * (l . v2)) * v2)) by VECTSP_1: 16

          .= (( - ( 1. R)) * ((((l . v1) " ) * (l . v2)) * v2)) by VECTSP_1: 14

          .= ((( - ( 1. R)) * (((l . v1) " ) * (l . v2))) * v2) by VECTSP_1:def 16;

          hence thesis by A9;

        end;

          suppose

           A17: (l . v2) <> ( 0. R) & (l . v1) = ( 0. R);

          ( 0. V) = (((l . v2) " ) * (((l . v1) * v1) + ((l . v2) * v2))) by A13, VECTSP_2: 30

          .= ((((l . v2) " ) * ((l . v1) * v1)) + (((l . v2) " ) * ((l . v2) * v2))) by VECTSP_1:def 14

          .= (((((l . v2) " ) * (l . v1)) * v1) + (((l . v2) " ) * ((l . v2) * v2))) by VECTSP_1:def 16

          .= (((((l . v2) " ) * (l . v1)) * v1) + (( 1. R) * v2)) by A17, Lm2

          .= (((((l . v2) " ) * (l . v1)) * v1) + v2) by VECTSP_1:def 17

          .= ((( 0. R) * v1) + v2) by A17

          .= (( 0. V) + v2) by VECTSP_2: 30

          .= v2 by RLVECT_1:def 4;

          hence thesis by A8;

        end;

      end;

      hence thesis;

    end;

    theorem :: MOD_3:17

    v1 <> v2 & {v1, v2} is linearly-independent iff for a, b st ((a * v1) + (b * v2)) = ( 0. V) holds a = ( 0. R) & b = ( 0. R)

    proof

      thus v1 <> v2 & {v1, v2} is linearly-independent implies for a, b st ((a * v1) + (b * v2)) = ( 0. V) holds a = ( 0. R) & b = ( 0. R)

      proof

        assume

         A1: v1 <> v2 & {v1, v2} is linearly-independent;

        let a, b;

        assume that

         A2: ((a * v1) + (b * v2)) = ( 0. V) and

         A3: a <> ( 0. R) or b <> ( 0. R);

        now

          per cases by A3;

            suppose

             A4: a <> ( 0. R);

            ( 0. V) = ((a " ) * ((a * v1) + (b * v2))) by A2, VECTSP_2: 30

            .= (((a " ) * (a * v1)) + ((a " ) * (b * v2))) by VECTSP_1:def 14

            .= ((((a " ) * a) * v1) + ((a " ) * (b * v2))) by VECTSP_1:def 16

            .= ((((a " ) * a) * v1) + (((a " ) * b) * v2)) by VECTSP_1:def 16

            .= ((( 1. R) * v1) + (((a " ) * b) * v2)) by A4, Lm2

            .= (v1 + (((a " ) * b) * v2)) by VECTSP_1:def 17;

            

            then v1 = ( - (((a " ) * b) * v2)) by VECTSP_1: 16

            .= (( - ( 1. R)) * (((a " ) * b) * v2)) by VECTSP_1: 14

            .= ((( - ( 1. R)) * ((a " ) * b)) * v2) by VECTSP_1:def 16;

            hence thesis by A1, Th16;

          end;

            suppose

             A5: b <> ( 0. R);

            ( 0. V) = ((b " ) * ((a * v1) + (b * v2))) by A2, VECTSP_2: 30

            .= (((b " ) * (a * v1)) + ((b " ) * (b * v2))) by VECTSP_1:def 14

            .= ((((b " ) * a) * v1) + ((b " ) * (b * v2))) by VECTSP_1:def 16

            .= ((((b " ) * a) * v1) + (( 1. R) * v2)) by A5, Lm2

            .= ((((b " ) * a) * v1) + v2) by VECTSP_1:def 17;

            

            then v2 = ( - (((b " ) * a) * v1)) by VECTSP_1: 16

            .= (( - ( 1. R)) * (((b " ) * a) * v1)) by VECTSP_1: 14

            .= ((( - ( 1. R)) * ((b " ) * a)) * v1) by VECTSP_1:def 16;

            hence thesis by A1, Th16;

          end;

        end;

        hence thesis;

      end;

      assume

       A6: for a, b st ((a * v1) + (b * v2)) = ( 0. V) holds a = ( 0. R) & b = ( 0. R);

       A7:

      now

        let a;

        assume v1 = (a * v2);

        then v1 = (( 0. V) + (a * v2)) by RLVECT_1:def 4;

        

        then ( 0. V) = (v1 - (a * v2)) by RLSUB_2: 61

        .= (v1 + (( - a) * v2)) by VECTSP_1: 21

        .= ((( 1. R) * v1) + (( - a) * v2)) by VECTSP_1:def 17;

        hence contradiction by A6;

      end;

      now

        assume

         A8: v2 = ( 0. V);

        ( 0. V) = (( 0. V) + ( 0. V)) by RLVECT_1:def 4

        .= ((( 0. R) * v1) + ( 0. V)) by VECTSP_2: 30

        .= ((( 0. R) * v1) + (( 1. R) * v2)) by A8, VECTSP_2: 30;

        hence contradiction by A6;

      end;

      hence thesis by A7, Th16;

    end;

    theorem :: MOD_3:18

    

     Th18: for V be LeftMod of R holds for A be Subset of V st A is linearly-independent holds ex B be Subset of V st A c= B & B is base

    proof

      let V be LeftMod of R;

      let A be Subset of V;

      defpred P[ set] means (ex B be Subset of V st B = $1 & A c= B & B is linearly-independent);

      consider Q be set such that

       A1: for Z holds Z in Q iff Z in ( bool the carrier of V) & P[Z] from XFAMILY:sch 1;

       A2:

      now

        let Z;

        assume that

         A3: Z <> {} and

         A4: Z c= Q and

         A5: Z is c=-linear;

        set W = ( union Z);

        W c= the carrier of V

        proof

          let x be object;

          assume x in W;

          then

          consider X such that

           A6: x in X and

           A7: X in Z by TARSKI:def 4;

          X in ( bool the carrier of V) by A1, A4, A7;

          hence thesis by A6;

        end;

        then

        reconsider W as Subset of V;

        

         A8: W is linearly-independent

        proof

          deffunc F( object) = { C where C be Subset of V : $1 in C & C in Z };

          let l be Linear_Combination of W;

          assume that

           A9: ( Sum l) = ( 0. V) and

           A10: ( Carrier l) <> {} ;

          consider f be Function such that

           A11: ( dom f) = ( Carrier l) and

           A12: for x be object st x in ( Carrier l) holds (f . x) = F(x) from FUNCT_1:sch 3;

          reconsider M = ( rng f) as non empty set by A10, A11, RELAT_1: 42;

          set F = the Choice_Function of M;

          set S = ( rng F);

           A13:

          now

            assume {} in M;

            then

            consider x be object such that

             A14: x in ( dom f) and

             A15: (f . x) = {} by FUNCT_1:def 3;

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

            then

            consider X such that

             A16: x in X and

             A17: X in Z by A11, A14, TARSKI:def 4;

            reconsider X as Subset of V by A1, A4, A17;

            X in { C where C be Subset of V : x in C & C in Z } by A16, A17;

            hence contradiction by A11, A12, A14, A15;

          end;

          then

           A18: ( dom F) = M by RLVECT_3: 28;

          then ( dom F) is finite by A11, FINSET_1: 8;

          then

           A19: S is finite by FINSET_1: 8;

           A20:

          now

            let X;

            assume X in S;

            then

            consider x be object such that

             A21: x in ( dom F) and

             A22: (F . x) = X by FUNCT_1:def 3;

            consider y be object such that

             A23: y in ( dom f) & (f . y) = x by A18, A21, FUNCT_1:def 3;

            

             A24: x = { C where C be Subset of V : y in C & C in Z } by A11, A12, A23;

            reconsider x as set by TARSKI: 1;

            X in x by A13, A18, A21, A22, ORDERS_1: 89;

            then ex C be Subset of V st C = X & y in C & C in Z by A24;

            hence X in Z;

          end;

           A25:

          now

            let X, Y;

            assume X in S & Y in S;

            then X in Z & Y in Z by A20;

            then (X,Y) are_c=-comparable by A5, ORDINAL1:def 8;

            hence X c= Y or Y c= X;

          end;

          S <> {} by A18, RELAT_1: 42;

          then ( union S) in S by A25, A19, CARD_2: 62;

          then ( union S) in Z by A20;

          then

          consider B be Subset of V such that

           A26: B = ( union S) and A c= B and

           A27: B is linearly-independent by A1, A4;

          ( Carrier l) c= ( union S)

          proof

            let x be object;

            set X = (f . x);

            assume

             A28: x in ( Carrier l);

            then

             A29: (f . x) = { C where C be Subset of V : x in C & C in Z } by A12;

            

             A30: (f . x) in M by A11, A28, FUNCT_1:def 3;

            then (F . X) in X by A13, ORDERS_1: 89;

            then

             A31: ex C be Subset of V st (F . X) = C & x in C & C in Z by A29;

            (F . X) in S by A18, A30, FUNCT_1:def 3;

            hence thesis by A31, TARSKI:def 4;

          end;

          then l is Linear_Combination of B by A26, VECTSP_6:def 4;

          hence thesis by A9, A10, A27;

        end;

        set x = the Element of Z;

        x in Q by A3, A4;

        then

         A32: ex B be Subset of V st B = x & A c= B & B is linearly-independent by A1;

        x c= W by A3, ZFMISC_1: 74;

        then A c= W by A32;

        hence ( union Z) in Q by A1, A8;

      end;

      assume A is linearly-independent;

      then Q <> {} by A1;

      then

      consider X such that

       A33: X in Q and

       A34: for Z st Z in Q & Z <> X holds not X c= Z by A2, ORDERS_1: 67;

      consider B be Subset of V such that

       A35: B = X and

       A36: A c= B and

       A37: B is linearly-independent by A1, A33;

      take B;

      thus A c= B & B is linearly-independent by A36, A37;

      assume ( Lin B) <> the ModuleStr of V;

      then

      consider v be Vector of V such that

       A38: not (v in ( Lin B) iff v in ( (Omega). V)) by VECTSP_4: 30;

      

       A39: (B \/ {v}) is linearly-independent

      proof

        let l be Linear_Combination of (B \/ {v});

        assume

         A40: ( Sum l) = ( 0. V);

        now

          per cases ;

            suppose v in ( Carrier l);

            then (l . v) <> ( 0. R) by VECTSP_6: 2;

            then ( - (l . v)) <> ( 0. R) by Lm1;

            

            then

             A41: ((( - (l . v)) " ) * (( - (l . v)) * v)) = (( 1. R) * v) by Lm2

            .= v by VECTSP_1:def 17;

            deffunc F( Vector of V) = (l . $1);

            consider f be Function of the carrier of V, the carrier of R such that

             A42: (f . v) = ( 0. R) and

             A43: for u be Vector of V st u <> v holds (f . u) = F(u) from FUNCT_2:sch 6;

            reconsider f as Element of ( Funcs (the carrier of V,the carrier of R)) by FUNCT_2: 8;

            now

              let u be Vector of V;

              assume not u in (( Carrier l) \ {v});

              then not u in ( Carrier l) or u in {v} by XBOOLE_0:def 5;

              then (l . u) = ( 0. R) & u <> v or u = v by TARSKI:def 1;

              hence (f . u) = ( 0. R) by A42, A43;

            end;

            then

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

            ( Carrier f) c= B

            proof

              let x be object;

              

               A44: ( Carrier l) c= (B \/ {v}) by VECTSP_6:def 4;

              assume x in ( Carrier f);

              then

              consider u be Vector of V such that

               A45: u = x and

               A46: (f . u) <> ( 0. R);

              (f . u) = (l . u) by A42, A43, A46;

              then u in ( Carrier l) by A46;

              then u in B or u in {v} by A44, XBOOLE_0:def 3;

              hence thesis by A42, A45, A46, TARSKI:def 1;

            end;

            then

            reconsider f as Linear_Combination of B by VECTSP_6:def 4;

            deffunc F( Vector of V) = ( 0. R);

            consider g be Function of the carrier of V, the carrier of R such that

             A47: (g . v) = ( - (l . v)) and

             A48: for u be Vector of V st u <> v holds (g . u) = F(u) from FUNCT_2:sch 6;

            reconsider g as Element of ( Funcs (the carrier of V,the carrier of R)) by FUNCT_2: 8;

            now

              let u be Vector of V;

              assume not u in {v};

              then u <> v by TARSKI:def 1;

              hence (g . u) = ( 0. R) by A48;

            end;

            then

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

            ( Carrier g) c= {v}

            proof

              let x be object;

              assume x in ( Carrier g);

              then ex u be Vector of V st x = u & (g . u) <> ( 0. R);

              then x = v by A48;

              hence thesis by TARSKI:def 1;

            end;

            then

            reconsider g as Linear_Combination of {v} by VECTSP_6:def 4;

            (f - g) = l

            proof

              let u be Vector of V;

              now

                per cases ;

                  suppose

                   A49: v = u;

                  

                  thus ((f - g) . u) = ((f . u) - (g . u)) by VECTSP_6: 40

                  .= (( 0. R) + ( - ( - (l . v)))) by A42, A47, A49, RLVECT_1:def 11

                  .= ((l . v) + ( 0. R)) by RLVECT_1: 17

                  .= (l . u) by A49, RLVECT_1: 4;

                end;

                  suppose

                   A50: v <> u;

                  

                  thus ((f - g) . u) = ((f . u) - (g . u)) by VECTSP_6: 40

                  .= ((l . u) - (g . u)) by A43, A50

                  .= ((l . u) - ( 0. R)) by A48, A50

                  .= (l . u) by RLVECT_1: 13;

                end;

              end;

              hence thesis;

            end;

            then

             A51: ( 0. V) = (( Sum f) - ( Sum g)) by A40, VECTSP_6: 47;

            ( Sum g) = (( - (l . v)) * v) by A47, VECTSP_6: 17;

            then ( Sum f) = (( - (l . v)) * v) by A51, VECTSP_1: 19;

            then (( - (l . v)) * v) in ( Lin B) by Th4;

            hence thesis by A38, A41, STRUCT_0:def 5, VECTSP_4: 21;

          end;

            suppose

             A52: not v in ( Carrier l);

            ( Carrier l) c= B

            proof

              let x be object;

              assume

               A53: x in ( Carrier l);

              ( Carrier l) c= (B \/ {v}) by VECTSP_6:def 4;

              then x in B or x in {v} by A53, XBOOLE_0:def 3;

              hence thesis by A52, A53, TARSKI:def 1;

            end;

            then l is Linear_Combination of B by VECTSP_6:def 4;

            hence thesis by A37, A40;

          end;

        end;

        hence thesis;

      end;

      v in {v} by TARSKI:def 1;

      then

       A54: v in (B \/ {v}) by XBOOLE_0:def 3;

      

       A55: not v in B by A38, Th5, STRUCT_0:def 5;

      B c= (B \/ {v}) by XBOOLE_1: 7;

      then A c= (B \/ {v}) by A36;

      then (B \/ {v}) in Q by A1, A39;

      hence contradiction by A34, A35, A54, A55, XBOOLE_1: 7;

    end;

    theorem :: MOD_3:19

    

     Th19: for R be almost_left_invertible non degenerated Ring holds for V be LeftMod of R holds for A be Subset of V st ( Lin A) = V holds ex B be Subset of V st B c= A & B is base

    proof

      let R be almost_left_invertible non degenerated Ring;

      let V be LeftMod of R;

      let A be Subset of V;

      defpred P[ set] means (ex B be Subset of V st B = $1 & B c= A & B is linearly-independent);

      assume

       A2: ( Lin A) = V;

      consider Q be set such that

       A3: for Z holds Z in Q iff Z in ( bool the carrier of V) & P[Z] from XFAMILY:sch 1;

       A4:

      now

        let Z;

        assume that Z <> {} and

         A5: Z c= Q and

         A6: Z is c=-linear;

        set W = ( union Z);

        W c= the carrier of V

        proof

          let x be object;

          assume x in W;

          then

          consider X such that

           A7: x in X and

           A8: X in Z by TARSKI:def 4;

          X in ( bool the carrier of V) by A3, A5, A8;

          hence thesis by A7;

        end;

        then

        reconsider W as Subset of V;

        

         A9: W is linearly-independent

        proof

          deffunc F( object) = { C where C be Subset of V : $1 in C & C in Z };

          let l be Linear_Combination of W;

          assume that

           A10: ( Sum l) = ( 0. V) and

           A11: ( Carrier l) <> {} ;

          consider f be Function such that

           A12: ( dom f) = ( Carrier l) and

           A13: for x be object st x in ( Carrier l) holds (f . x) = F(x) from FUNCT_1:sch 3;

          reconsider M = ( rng f) as non empty set by A11, A12, RELAT_1: 42;

          set F = the Choice_Function of M;

          set S = ( rng F);

           A14:

          now

            assume {} in M;

            then

            consider x be object such that

             A15: x in ( dom f) and

             A16: (f . x) = {} by FUNCT_1:def 3;

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

            then

            consider X such that

             A17: x in X and

             A18: X in Z by A12, A15, TARSKI:def 4;

            reconsider X as Subset of V by A3, A5, A18;

            X in { C where C be Subset of V : x in C & C in Z } by A17, A18;

            hence contradiction by A12, A13, A15, A16;

          end;

          then

           A19: ( dom F) = M by RLVECT_3: 28;

          then ( dom F) is finite by A12, FINSET_1: 8;

          then

           A20: S is finite by FINSET_1: 8;

           A21:

          now

            let X;

            assume X in S;

            then

            consider x be object such that

             A22: x in ( dom F) and

             A23: (F . x) = X by FUNCT_1:def 3;

            consider y be object such that

             A24: y in ( dom f) & (f . y) = x by A19, A22, FUNCT_1:def 3;

            

             A25: x = { C where C be Subset of V : y in C & C in Z } by A12, A13, A24;

            reconsider x as set by TARSKI: 1;

            X in x by A14, A19, A22, A23, ORDERS_1: 89;

            then ex C be Subset of V st C = X & y in C & C in Z by A25;

            hence X in Z;

          end;

           A26:

          now

            let X, Y;

            assume X in S & Y in S;

            then X in Z & Y in Z by A21;

            then (X,Y) are_c=-comparable by A6, ORDINAL1:def 8;

            hence X c= Y or Y c= X;

          end;

          S <> {} by A19, RELAT_1: 42;

          then ( union S) in S by A26, A20, CARD_2: 62;

          then ( union S) in Z by A21;

          then

          consider B be Subset of V such that

           A27: B = ( union S) and B c= A and

           A28: B is linearly-independent by A3, A5;

          ( Carrier l) c= ( union S)

          proof

            let x be object;

            set X = (f . x);

            assume

             A29: x in ( Carrier l);

            then

             A30: (f . x) = { C where C be Subset of V : x in C & C in Z } by A13;

            

             A31: (f . x) in M by A12, A29, FUNCT_1:def 3;

            then (F . X) in X by A14, ORDERS_1: 89;

            then

             A32: ex C be Subset of V st (F . X) = C & x in C & C in Z by A30;

            (F . X) in S by A19, A31, FUNCT_1:def 3;

            hence thesis by A32, TARSKI:def 4;

          end;

          then l is Linear_Combination of B by A27, VECTSP_6:def 4;

          hence thesis by A10, A11, A28;

        end;

        W c= A

        proof

          let x be object;

          assume x in W;

          then

          consider X such that

           A33: x in X and

           A34: X in Z by TARSKI:def 4;

          ex B be Subset of V st B = X & B c= A & B is linearly-independent by A3, A5, A34;

          hence thesis by A33;

        end;

        hence ( union Z) in Q by A3, A9;

      end;

      ( {} the carrier of V) c= A & ( {} the carrier of V) is linearly-independent;

      then Q <> {} by A3;

      then

      consider X such that

       A35: X in Q and

       A36: for Z st Z in Q & Z <> X holds not X c= Z by A4, ORDERS_1: 67;

      consider B be Subset of V such that

       A37: B = X and

       A38: B c= A and

       A39: B is linearly-independent by A3, A35;

      take B;

      thus B c= A & B is linearly-independent by A38, A39;

      assume

       A40: ( Lin B) <> the ModuleStr of V;

      now

        assume

         A41: for v be Vector of V st v in A holds v in ( Lin B);

        now

          reconsider F = the carrier of ( Lin B) as Subset of V by VECTSP_4:def 2;

          let v be Vector of V;

          assume v in ( Lin A);

          then

          consider l be Linear_Combination of A such that

           A42: v = ( Sum l) by Th4;

          ( Carrier l) c= the carrier of ( Lin B)

          proof

            let x be object;

            assume

             A43: x in ( Carrier l);

            then

            reconsider a = x as Vector of V;

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

            then a in ( Lin B) by A41, A43;

            hence thesis by STRUCT_0:def 5;

          end;

          then

          reconsider l as Linear_Combination of F by VECTSP_6:def 4;

          ( Sum l) = v by A42;

          then v in ( Lin F) by Th4;

          hence v in ( Lin B) by Th8;

        end;

        then ( Lin A) is Subspace of ( Lin B) by VECTSP_4: 28;

        hence contradiction by A2, A40, VECTSP_4: 25;

      end;

      then

      consider v be Vector of V such that

       A44: v in A and

       A45: not v in ( Lin B);

      

       A46: (B \/ {v}) is linearly-independent

      proof

        let l be Linear_Combination of (B \/ {v});

        assume

         A47: ( Sum l) = ( 0. V);

        now

          per cases ;

            suppose v in ( Carrier l);

            then (l . v) <> ( 0. R) by VECTSP_6: 2;

            then ( - (l . v)) <> ( 0. R) by Lm1;

            

            then

             A48: ((( - (l . v)) " ) * (( - (l . v)) * v)) = (( 1. R) * v) by Lm2

            .= v by VECTSP_1:def 17;

            deffunc F( Vector of V) = (l . $1);

            consider f be Function of the carrier of V, the carrier of R such that

             A49: (f . v) = ( 0. R) and

             A50: for u be Vector of V st u <> v holds (f . u) = F(u) from FUNCT_2:sch 6;

            reconsider f as Element of ( Funcs (the carrier of V,the carrier of R)) by FUNCT_2: 8;

            now

              let u be Vector of V;

              assume not u in (( Carrier l) \ {v});

              then not u in ( Carrier l) or u in {v} by XBOOLE_0:def 5;

              then (l . u) = ( 0. R) & u <> v or u = v by TARSKI:def 1;

              hence (f . u) = ( 0. R) by A49, A50;

            end;

            then

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

            ( Carrier f) c= B

            proof

              let x be object;

              

               A51: ( Carrier l) c= (B \/ {v}) by VECTSP_6:def 4;

              assume x in ( Carrier f);

              then

              consider u be Vector of V such that

               A52: u = x and

               A53: (f . u) <> ( 0. R);

              (f . u) = (l . u) by A49, A50, A53;

              then u in ( Carrier l) by A53;

              then u in B or u in {v} by A51, XBOOLE_0:def 3;

              hence thesis by A49, A52, A53, TARSKI:def 1;

            end;

            then

            reconsider f as Linear_Combination of B by VECTSP_6:def 4;

            deffunc F( Vector of V) = ( 0. R);

            consider g be Function of the carrier of V, the carrier of R such that

             A54: (g . v) = ( - (l . v)) and

             A55: for u be Vector of V st u <> v holds (g . u) = F(u) from FUNCT_2:sch 6;

            reconsider g as Element of ( Funcs (the carrier of V,the carrier of R)) by FUNCT_2: 8;

            now

              let u be Vector of V;

              assume not u in {v};

              then u <> v by TARSKI:def 1;

              hence (g . u) = ( 0. R) by A55;

            end;

            then

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

            ( Carrier g) c= {v}

            proof

              let x be object;

              assume x in ( Carrier g);

              then ex u be Vector of V st x = u & (g . u) <> ( 0. R);

              then x = v by A55;

              hence thesis by TARSKI:def 1;

            end;

            then

            reconsider g as Linear_Combination of {v} by VECTSP_6:def 4;

            (f - g) = l

            proof

              let u be Vector of V;

              now

                per cases ;

                  suppose

                   A56: v = u;

                  

                  thus ((f - g) . u) = ((f . u) - (g . u)) by VECTSP_6: 40

                  .= (( 0. R) + ( - ( - (l . v)))) by A49, A54, A56, RLVECT_1:def 11

                  .= ((l . v) + ( 0. R)) by RLVECT_1: 17

                  .= (l . u) by A56, RLVECT_1: 4;

                end;

                  suppose

                   A57: v <> u;

                  

                  thus ((f - g) . u) = ((f . u) - (g . u)) by VECTSP_6: 40

                  .= ((l . u) - (g . u)) by A50, A57

                  .= ((l . u) - ( 0. R)) by A55, A57

                  .= (l . u) by RLVECT_1: 13;

                end;

              end;

              hence thesis;

            end;

            then

             A58: ( 0. V) = (( Sum f) - ( Sum g)) by A47, VECTSP_6: 47;

            ( Sum g) = (( - (l . v)) * v) by A54, VECTSP_6: 17;

            then ( Sum f) = (( - (l . v)) * v) by A58, VECTSP_1: 19;

            then (( - (l . v)) * v) in ( Lin B) by Th4;

            hence thesis by A45, A48, VECTSP_4: 21;

          end;

            suppose

             A59: not v in ( Carrier l);

            ( Carrier l) c= B

            proof

              let x be object;

              assume

               A60: x in ( Carrier l);

              ( Carrier l) c= (B \/ {v}) by VECTSP_6:def 4;

              then x in B or x in {v} by A60, XBOOLE_0:def 3;

              hence thesis by A59, A60, TARSKI:def 1;

            end;

            then l is Linear_Combination of B by VECTSP_6:def 4;

            hence thesis by A39, A47;

          end;

        end;

        hence thesis;

      end;

       {v} c= A by A44, ZFMISC_1: 31;

      then (B \/ {v}) c= A by A38, XBOOLE_1: 8;

      then

       A61: (B \/ {v}) in Q by A3, A46;

      v in {v} by TARSKI:def 1;

      then

       A62: v in (B \/ {v}) by XBOOLE_0:def 3;

       not v in B by A45, Th5;

      hence contradiction by A36, A37, A62, A61, XBOOLE_1: 7;

    end;

    

     Lm3: for R be non degenerated almost_left_invertible Ring holds for V be LeftMod of R holds ex B be Subset of V st B is base

    proof

      let R be non degenerated almost_left_invertible Ring;

      let V be LeftMod of R;

      ex B be Subset of V st ( {} the carrier of V) c= B & B is base by VECTSP_7: 17;

      hence thesis;

    end;

    registration

      let R be non degenerated almost_left_invertible Ring;

      let V be LeftMod of R;

      cluster base for Subset of V;

      existence

      proof

        ex B be Subset of V st ( {} the carrier of V) c= B & B is base by VECTSP_7: 17;

        hence thesis;

      end;

    end

    theorem :: MOD_3:20

    for V be LeftMod of R holds V is free by Lm3;

    registration

      let R;

      cluster -> free for LeftMod of R;

      coherence by Lm3;

    end

    theorem :: MOD_3:21

    for R be non degenerated almost_left_invertible Ring holds for V be LeftMod of R holds for A be Subset of V st A is linearly-independent holds ex I be Basis of V st A c= I

    proof

      let R be non degenerated almost_left_invertible Ring;

      let V be LeftMod of R;

      let A be Subset of V;

      assume A is linearly-independent;

      then

      consider B be Subset of V such that

       A1: A c= B and

       A2: B is base by Th18;

      reconsider B as Basis of V by A2;

      take B;

      thus thesis by A1;

    end;

    theorem :: MOD_3:22

    for V be LeftMod of R holds for A be Subset of V st ( Lin A) = V holds ex I be Basis of V st I c= A

    proof

      let V be LeftMod of R;

      let A be Subset of V;

      assume ( Lin A) = V;

      then

      consider B be Subset of V such that

       A1: B c= A and

       A2: B is base by Th19;

      reconsider B as Basis of V by A2;

      take B;

      thus thesis by A1;

    end;