zmodul06.miz



    begin

    theorem :: ZMODUL06:1

    

     Th1V: for R be commutative Ring holds for V be LeftMod of R, W be Subspace of V holds (( 1. R) (*) W) = ( (Omega). W)

    proof

      let R be commutative Ring;

      let V be LeftMod of R, W be Subspace of V;

      for v be Vector of V st v in ( (Omega). W) holds v in (( 1. R) (*) W)

      proof

        let v be Vector of V such that

         B1: v in ( (Omega). W);

        reconsider vv = v as Vector of W by B1;

        (( 1. R) * vv) in (( 1. R) (*) W);

        hence thesis by VECTSP_1:def 17;

      end;

      then

       A2: for v be Vector of V holds v in (( 1. R) (*) W) iff v in ( (Omega). W);

      

       A3: ( (Omega). W) is Subspace of V by ZMODUL01: 42;

      (( 1. R) (*) W) is Subspace of V by ZMODUL01: 42;

      hence thesis by A2, A3, ZMODUL01: 46;

    end;

    theorem :: ZMODUL06:2

    for R be Ring holds for V be LeftMod of R, W1,W2,W3 be Subspace of V holds (W1 /\ W2) is Subspace of ((W1 + W3) /\ W2)

    proof

      let R be Ring;

      let V be LeftMod of R, W1,W2,W3 be Subspace of V;

      for v be Vector of V st v in (W1 /\ W2) holds v in ((W1 + W3) /\ W2)

      proof

        let v be Vector of V such that

         A1: v in (W1 /\ W2);

        v in W1 by A1, VECTSP_5: 3;

        then

         A2: v in (W1 + W3) by VECTSP_5: 2;

        v in W2 by A1, VECTSP_5: 3;

        hence thesis by A2, VECTSP_5: 3;

      end;

      hence thesis by VECTSP_4: 28;

    end;

    theorem :: ZMODUL06:3

    

     ThIS1: for R be Ring holds for V be LeftMod of R, W1,W2,W3 be Subspace of V st (W1 /\ W2) <> ( (0). V) holds ((W1 + W3) /\ W2) <> ( (0). V)

    proof

      let R be Ring;

      let V be LeftMod of R, W1,W2,W3 be Subspace of V such that

       A1: (W1 /\ W2) <> ( (0). V);

      consider v be Vector of V such that

       A2: v in (W1 /\ W2) & v <> ( 0. V) by A1, ZMODUL04: 24;

      

       A3: v in W1 & v in W2 by A2, ZMODUL01: 94;

      then v in (W1 + W3) by ZMODUL01: 93;

      hence thesis by A2, ZMODUL02: 66, A3, ZMODUL01: 94;

    end;

    theorem :: ZMODUL06:4

    for V be Z_Module, I,I1 be linearly-independent Subset of V st I1 c= I holds (( Lin (I \ I1)) /\ ( Lin I1)) = ( (0). V)

    proof

      let V be Z_Module, I,I1 be linearly-independent Subset of V such that

       A1: I1 c= I;

      assume (( Lin (I \ I1)) /\ ( Lin I1)) <> ( (0). V);

      then

      consider v be Vector of V such that

       A2: v in (( Lin (I \ I1)) /\ ( Lin I1)) & v <> ( 0. V) by ZMODUL04: 24;

      v in ( Lin (I \ I1)) by A2, ZMODUL01: 94;

      then

      consider l1 be Linear_Combination of (I \ I1) such that

       A3: v = ( Sum l1) by ZMODUL02: 64;

      

       A4: ( Carrier l1) c= (I \ I1) by VECTSP_6:def 4;

      v in ( Lin I1) by A2, ZMODUL01: 94;

      then

      consider l2 be Linear_Combination of I1 such that

       A5: v = ( Sum l2) by ZMODUL02: 64;

      

       A6: ( Carrier l2) c= I1 by VECTSP_6:def 4;

      reconsider ll1 = l1 as Linear_Combination of I by XBOOLE_1: 36, ZMODUL02: 10;

      reconsider ll2 = l2 as Linear_Combination of I by A1, ZMODUL02: 10;

      ( Carrier l1) misses ( Carrier l2) by A4, A6, XBOOLE_1: 64, XBOOLE_1: 79;

      then (( Carrier ll1) /\ ( Carrier ll2)) = {} by XBOOLE_0:def 7;

      then

       A10: (( Carrier ll1) /\ ( Carrier ( - ll2))) = {} by ZMODUL02: 37;

      reconsider ll2x = ( - ll2) as Linear_Combination of I by ZMODUL02: 38;

      

       A7: ( Carrier (ll1 - ll2)) = (( Carrier ll1) \/ ( Carrier ll2x)) by A10, ZMODUL04: 25;

      

       A8: (( Sum ll1) - ( Sum ll2)) = ( 0. V) by A3, A5, RLVECT_1: 5;

      reconsider l = (ll1 - ll2) as Linear_Combination of I by ZMODUL02: 41;

      

       A9: ( Sum l) = ( 0. V) by A8, ZMODUL02: 55;

      ( Carrier ll1) <> {} by A2, A3, ZMODUL02: 23;

      hence contradiction by A9, A7, VECTSP_7:def 1;

    end;

    reserve V for Z_Module;

    reserve W for Subspace of V;

    reserve v,u for Vector of V;

    reserve i for Element of INT.Ring ;

    definition

      let R be Ring;

      let V be LeftMod of R, v be Vector of V;

      :: ZMODUL06:def1

      attr v is torsion means ex i be Element of R st i <> ( 0. R) & (i * v) = ( 0. V);

    end

    

     ThTV1: ( 0. V) is torsion

    proof

      (( 1. INT.Ring ) * ( 0. V)) = ( 0. V) by ZMODUL01: 1;

      hence thesis;

    end;

    registration

      let V be Z_Module;

      cluster ( 0. V) -> torsion;

      coherence by ThTV1;

    end

    theorem :: ZMODUL06:5

    v is torsion & u is torsion implies (v + u) is torsion

    proof

      assume v is torsion & u is torsion;

      then

      consider i1,i2 be Element of INT.Ring such that

       A1: i1 <> 0 & (i1 * v) = ( 0. V) and

       A2: i2 <> 0 & (i2 * u) = ( 0. V);

      ((i1 * i2) * (v + u)) = (((i1 * i2) * v) + ((i1 * i2) * u)) by VECTSP_1:def 14

      .= (((i2 * i1) * v) + (i1 * (i2 * u))) by VECTSP_1:def 16

      .= ((i2 * (i1 * v)) + (i1 * (i2 * u))) by VECTSP_1:def 16

      .= (( 0. V) + (i1 * ( 0. V))) by ZMODUL01: 1, A1, A2

      .= ( 0. V) by ZMODUL01: 1;

      hence thesis by A1, A2;

    end;

    theorem :: ZMODUL06:6

    v is torsion implies ( - v) is torsion

    proof

      assume v is torsion;

      then

      consider i be Element of INT.Ring such that

       A1: i <> 0 & (i * v) = ( 0. V);

      (i * ( - v)) = ( - (i * v)) by ZMODUL01: 6

      .= ( 0. V) by A1;

      hence thesis by A1;

    end;

    theorem :: ZMODUL06:7

    v is torsion & u is torsion implies (v - u) is torsion

    proof

      assume v is torsion & u is torsion;

      then

      consider i1,i2 be Element of INT.Ring such that

       A1: i1 <> 0 & (i1 * v) = ( 0. V) and

       A2: i2 <> 0 & (i2 * u) = ( 0. V);

      ((i1 * i2) * (v - u)) = (((i1 * i2) * v) - ((i1 * i2) * u)) by ZMODUL01: 8

      .= (((i2 * i1) * v) - (i1 * (i2 * u))) by VECTSP_1:def 16

      .= ((i2 * (i1 * v)) - (i1 * (i2 * u))) by VECTSP_1:def 16

      .= (( 0. V) - (i1 * ( 0. V))) by ZMODUL01: 1, A1, A2

      .= (( 0. V) - ( 0. V)) by ZMODUL01: 1

      .= ( 0. V);

      hence thesis by A1, A2;

    end;

    theorem :: ZMODUL06:8

    v is torsion implies (i * v) is torsion

    proof

      assume v is torsion;

      then

      consider i1 be Element of INT.Ring such that

       A1: i1 <> 0 & (i1 * v) = ( 0. V);

      (i1 * (i * v)) = ((i1 * i) * v) by VECTSP_1:def 16

      .= (i * (i1 * v)) by VECTSP_1:def 16

      .= ( 0. V) by ZMODUL01: 1, A1;

      hence thesis by A1;

    end;

    theorem :: ZMODUL06:9

    

     ThTV6: for v be Vector of V, w be Vector of W st v = w holds v is torsion iff w is torsion

    proof

      let v be Vector of V, w be Vector of W such that

       A1: v = w;

      hereby

        assume v is torsion;

        then

        consider i be Element of INT.Ring such that

         B2: i <> 0 & (i * v) = ( 0. V);

        (i * w) = (i * v) by A1, ZMODUL01: 29

        .= ( 0. W) by ZMODUL01: 26, B2;

        hence w is torsion by B2;

      end;

      assume w is torsion;

      then

      consider i be Element of INT.Ring such that

       B2: i <> 0 & (i * w) = ( 0. W);

      (i * v) = (i * w) by A1, ZMODUL01: 29

      .= ( 0. V) by ZMODUL01: 26, B2;

      hence v is torsion by B2;

    end;

    registration

      let V be Z_Module;

      cluster torsion for Vector of V;

      correctness

      proof

        take ( 0. V);

        thus thesis;

      end;

    end

    theorem :: ZMODUL06:10

    v is non torsion implies ( - v) is non torsion

    proof

      assume

       A1: not v is torsion;

      assume ( - v) is torsion;

      then

      consider i be Element of INT.Ring such that

       A3: i <> 0 & (i * ( - v)) = ( 0. V);

      (( - i) * v) = ( 0. V) by A3, ZMODUL01: 5;

      hence contradiction by A1, A3;

    end;

    theorem :: ZMODUL06:11

    v is non torsion & i <> 0 implies (i * v) is non torsion

    proof

      assume

       A1: not v is torsion & i <> 0 ;

      assume (i * v) is torsion;

      then

      consider i1 be Element of INT.Ring such that

       A3: i1 <> 0 & (i1 * (i * v)) = ( 0. V);

      ((i1 * i) * v) = ( 0. V) by A3, VECTSP_1:def 16;

      hence contradiction by A1, A3;

    end;

    theorem :: ZMODUL06:12

    

     ThnTV3: v is non torsion iff {v} is linearly-independent

    proof

      

       A1: not v is torsion implies {v} is linearly-independent

      proof

        assume

         B1: not v is torsion;

        let l be Linear_Combination of {v};

        assume

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

        now

          per cases by ZFMISC_1: 33, VECTSP_6:def 4;

            suppose ( Carrier l) = {} ;

            hence thesis;

          end;

            suppose

             B5: ( Carrier l) = {v};

            then

             B6: ( 0. V) = ((l . v) * v) by B4, ZMODUL02: 24;

            now

              assume v in ( Carrier l);

              then ex u st v = u & (l . u) <> ( 0. INT.Ring );

              hence contradiction by B1, B6;

            end;

            hence thesis by B5, TARSKI:def 1;

          end;

        end;

        hence thesis;

      end;

       {v} is linearly-independent implies not v is torsion

      proof

        assume

         B1: {v} is linearly-independent;

        assume v is torsion;

        then

        consider i be Element of INT.Ring such that

         C2: i <> 0 & (i * v) = ( 0. V);

        consider l be Linear_Combination of V such that

         C3: (l . v) = 1 & for u be Vector of V st v <> u holds (l . u) = ( 0. INT.Ring ) by ZMODUL03: 1;

        for u be Vector of V st u <> v holds not u in ( Carrier l)

        proof

          let u be Vector of V;

          assume u <> v;

          then (l . u) = 0 by C3;

          hence not u in ( Carrier l) by ZMODUL02: 8;

        end;

        then for u be object holds u = v iff u in ( Carrier l) by C3;

        then

         C5: ( Carrier l) = {v} by TARSKI:def 1;

        then

         C6: ( Carrier (i * l)) = {v} by C2, ZMODUL02: 29;

        

         C7: ( Carrier (i * l)) <> {} by C2, C5, ZMODUL02: 29;

        reconsider li = (i * l) as Linear_Combination of {v} by C6, VECTSP_6:def 4;

        ( Sum (i * l)) = (i * ( Sum l)) by ZMODUL02: 53

        .= (i * (( 1. INT.Ring ) * v)) by C3, C5, ZMODUL02: 24

        .= ( 0. V) by C2, VECTSP_1:def 17;

        then ( Sum li) = ( 0. V);

        hence contradiction by B1, C7;

      end;

      hence thesis by A1;

    end;

    definition

      let V be Z_Module;

      :: ZMODUL06:def2

      attr V is torsion means

      : defTorsionModule: for v be Vector of V holds v is torsion;

    end

    

     ThTZM: ( (0). V) is torsion

    proof

      for x be Vector of ( (0). V) holds x is torsion

      proof

        let x be Vector of ( (0). V);

        x in ( (0). V);

        

        then x = ( 0. V) by ZMODUL02: 66

        .= ( 0. ( (0). V)) by ZMODUL01: 26;

        hence thesis;

      end;

      hence thesis;

    end;

    registration

      let V be Z_Module;

      cluster ( (0). V) -> torsion;

      coherence by ThTZM;

    end

    registration

      cluster torsion for Z_Module;

      existence

      proof

        set V = the Z_Module;

        take ( (0). V);

        thus thesis;

      end;

    end

    theorem :: ZMODUL06:13

    

     LMINTRNG1: for v be Element of INT.Ring , v1 be Integer st v = v1 holds for n be Nat holds (( Nat-mult-left INT.Ring ) . (n,v)) = (n * v1)

    proof

      let v be Element of INT.Ring , v1 be Integer;

      assume

       A1: v = v1;

      defpred P[ Nat] means (( Nat-mult-left INT.Ring ) . ($1,v)) = ($1 * v1);

      (( Nat-mult-left INT.Ring ) . ( 0 ,v)) = ( 0. INT.Ring ) by BINOM:def 3

      .= (( 0. INT.Ring ) * v1);

      then

       X1: P[ 0 ];

      

       X2: for n be Nat st P[n] holds P[(n + 1)]

      proof

        let n be Nat;

        assume

         X22: P[n];

        (( Nat-mult-left INT.Ring ) . ((n + 1),v)) = (v + (( Nat-mult-left INT.Ring ) . (n,v))) by BINOM:def 3

        .= ((n + 1) * v1) by A1, X22;

        hence thesis;

      end;

      for n be Nat holds P[n] from NAT_1:sch 2( X1, X2);

      hence thesis;

    end;

    theorem :: ZMODUL06:14

    

     LMINTRNG2: for x be Element of INT.Ring , v be Element of INT.Ring , v1 be Integer st v = v1 holds (( Int-mult-left INT.Ring ) . (x,v)) = (x * v1)

    proof

      let x be Element of INT.Ring , v be Element of INT.Ring , v1 be Integer;

      assume

       A1: v = v1;

      reconsider xx = x as Element of INT ;

      per cases ;

        suppose

         C1: x >= 0 ;

        then

        reconsider x0 = x as Element of NAT by INT_1: 3;

        

        thus (( Int-mult-left INT.Ring ) . (x,v)) = (( Nat-mult-left INT.Ring ) . (xx,v)) by C1, ZMODUL01:def 20

        .= (( Nat-mult-left INT.Ring ) . (x0,v))

        .= (x0 * v1) by LMINTRNG1, A1

        .= (x * v1);

      end;

        suppose

         C2: x < 0 ;

        then

        reconsider x0 = ( - x) as Element of NAT by INT_1: 3;

        

        thus (( Int-mult-left INT.Ring ) . (x,v)) = (( Nat-mult-left INT.Ring ) . (( - x),( - v))) by C2, ZMODUL01:def 20

        .= (x0 * ( - v1)) by LMINTRNG1, A1

        .= (x * v1);

      end;

    end;

    registration

      cluster non torsion for Z_Module;

      existence

      proof

        set AG = INT.Ring ;

        set G = ModuleStr (# the carrier of AG, the addF of AG, the ZeroF of AG, ( Int-mult-left AG) #);

        reconsider G as Z_Module by ZMODUL01: 164;

        reconsider v = ( 1. INT.Ring ) as Vector of G;

        set One = ( 1. INT.Ring );

        for i be Element of INT.Ring st i <> 0 holds (i * v) <> ( 0. G)

        proof

          assume ex i be Element of INT.Ring st i <> 0 & (i * v) = ( 0. G);

          then

          consider i be Element of INT.Ring such that

           B1: i <> 0 & (i * v) = ( 0. G);

          (i * v) = (the lmult of G . (i,v)) by VECTSP_1:def 12

          .= (( Int-mult-left AG) . (i,v))

          .= (i * One) by LMINTRNG2

          .= i;

          hence contradiction by B1;

        end;

        then v is non torsion;

        hence thesis by defTorsionModule;

      end;

    end

    registration

      let V be non torsion Z_Module;

      cluster non torsion for Vector of V;

      existence by defTorsionModule;

    end

    definition

      let V be Z_Module;

      :: ZMODUL06:def3

      attr V is torsion-free means

      : defTorsionFree: for v be Vector of V st v <> ( 0. V) holds v is non torsion;

    end

    theorem :: ZMODUL06:15

    

     ThMCTF: V is Mult-cancelable iff V is torsion-free

    proof

      hereby

        assume V is Mult-cancelable;

        then for v be Vector of V st v <> ( 0. V) holds v is non torsion;

        hence V is torsion-free;

      end;

      assume

       AS: V is torsion-free;

      for i be Element of INT.Ring , v be Vector of V holds i <> ( 0. INT.Ring ) & v <> ( 0. V) implies (i * v) <> ( 0. V)

      proof

        let i be Element of INT.Ring , v be Vector of V;

        assume

         A1: i <> ( 0. INT.Ring ) & v <> ( 0. V);

        then v is non torsion by AS;

        hence (i * v) <> ( 0. V) by A1;

      end;

      hence V is Mult-cancelable;

    end;

    registration

      cluster -> torsion-free for Mult-cancelable Z_Module;

      coherence by ThMCTF;

    end

    registration

      cluster -> Mult-cancelable for torsion-free Z_Module;

      coherence by ThMCTF;

    end

    registration

      cluster -> torsion-free for free Z_Module;

      coherence ;

    end

    registration

      cluster torsion-free free for Z_Module;

      existence

      proof

        set V = the free Z_Module;

        take V;

        thus thesis;

      end;

    end

    theorem :: ZMODUL06:16

    for V be torsion-free Z_Module, v be Vector of V holds v is torsion iff v = ( 0. V) by defTorsionFree;

    registration

      let V be torsion-free Z_Module;

      cluster -> torsion-free for Subspace of V;

      coherence

      proof

        let W be Subspace of V;

        for w be Vector of W st w <> ( 0. W) holds w is non torsion

        proof

          let w be Vector of W such that

           A1: w <> ( 0. W);

          

           A2: w <> ( 0. V) by A1, ZMODUL01: 26;

          reconsider v = w as Vector of V by ZMODUL01: 25;

          v is non torsion by A2, defTorsionFree;

          hence thesis by ThTV6;

        end;

        hence thesis;

      end;

    end

    registration

      let R be Ring;

      let V be LeftMod of R;

      cluster ( (0). V) -> trivial;

      coherence

      proof

        for x,y be Vector of ( (0). V) holds x = y

        proof

          let x,y be Vector of ( (0). V);

          x in ( (0). V) & y in ( (0). V);

          then x = ( 0. V) & y = ( 0. V) by VECTSP_4: 35;

          hence thesis;

        end;

        hence ( (0). V) is trivial;

      end;

    end

    registration

      cluster -> non torsion for non trivial torsion-free Z_Module;

      coherence

      proof

        let V be non trivial torsion-free Z_Module;

        ( (Omega). V) <> ( (0). V);

        then

        consider v be Vector of V such that

         A2: v in ( (Omega). V) & v <> ( 0. V) by ZMODUL04: 24;

        thus thesis by A2, defTorsionFree;

      end;

    end

    registration

      let R be Ring;

      cluster trivial for LeftMod of R;

      existence

      proof

        set V = the LeftMod of R;

        take ( (0). V);

        thus thesis;

      end;

    end

    registration

      let K be Abelian add-associative right_zeroed right_complementable associative left_unital distributive non degenerated non empty doubleLoopStr;

      cluster Abelian add-associative right_zeroed right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital strict for non trivial ModuleStr over K;

      existence

      proof

        take ( StructVectSp K);

        thus thesis;

      end;

    end

    registration

      let R be non degenerated non empty Ring;

      let V be non trivial LeftMod of R;

      cluster non zero for Vector of V;

      existence

      proof

        ( (Omega). V) <> ( (0). V);

        then

        consider v be Vector of V such that

         A1: v in ( (Omega). V) & v <> ( 0. V) by ZMODUL04: 24;

        take v;

        thus thesis by A1;

      end;

    end

    theorem :: ZMODUL06:17

    

     ThnTV4: v is non torsion iff ( Lin {v}) is free & v <> ( 0. V)

    proof

      hereby

        assume v is non torsion;

        then {v} is linearly-independent Subset of V by ThnTV3;

        hence ( Lin {v}) is free & v <> ( 0. V);

      end;

      assume

       A1: ( Lin {v}) is free & v <> ( 0. V);

      then

       A2: ( Lin {v}) is torsion-free;

      

       A3: v <> ( 0. ( Lin {v})) by A1, ZMODUL01: 26;

      v in {v} by TARSKI:def 1;

      then v in ( Lin {v}) by ZMODUL02: 65;

      then

      reconsider vl = v as Vector of ( Lin {v});

      vl is non torsion by A2, A3;

      hence v is non torsion by ThTV6;

    end;

    registration

      let V be non torsion Z_Module;

      let v be non torsion Vector of V;

      cluster ( Lin {v}) -> free;

      coherence by ThnTV4;

    end

    theorem :: ZMODUL06:18

    

     ThLIV1: for V be Z_Module, A be Subset of V, v be Vector of V st A is linearly-independent & v in A holds v is non torsion

    proof

      let V be Z_Module, A be Subset of V, v be Vector of V such that

       A1: A is linearly-independent & v in A;

       {v} is linearly-independent by A1, ZMODUL02: 56, ZFMISC_1: 31;

      hence v is non torsion by ThnTV3;

    end;

    theorem :: ZMODUL06:19

    

     ThLin1: for u be object holds u in ( Lin {v}) implies ex i be Element of INT.Ring st u = (i * v)

    proof

      let u be object;

      assume u in ( Lin {v});

      then

      consider l be Linear_Combination of {v} such that

       A1: u = ( Sum l) by ZMODUL02: 64;

      take (l . v);

      thus thesis by A1, ZMODUL02: 21;

    end;

    theorem :: ZMODUL06:20

    

     ThLin2: v in ( Lin {v}) by ZMODUL02: 65, ZFMISC_1: 31;

    theorem :: ZMODUL06:21

    (i * v) in ( Lin {v}) by ZMODUL01: 37, ThLin2;

    

     ThLin4: for A be Subset of V holds A is Subset of ( Lin A) by ZMODUL05: 30;

    theorem :: ZMODUL06:22

    

     ThLin5: for R be Ring holds for V be LeftMod of R holds ( Lin {( 0. V)}) = ( (0). V)

    proof

      let R be Ring;

      let V be LeftMod of R;

      for x be object holds x in ( Lin {( 0. V)}) iff x in ( (0). V)

      proof

        let x be object;

        hereby

          assume x in ( Lin {( 0. V)});

          then

          consider l be Linear_Combination of {( 0. V)} such that

           B2: x = ( Sum l) by MOD_3: 4;

          ( Sum l) = ((l . ( 0. V)) * ( 0. V)) by VECTSP_6: 17

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

          hence x in ( (0). V) by B2, VECTSP_4: 17;

        end;

        assume x in ( (0). V);

        then x = ( 0. V) by VECTSP_4: 35;

        hence x in ( Lin {( 0. V)}) by VECTSP_4: 17;

      end;

      then for x be Vector of V holds x in ( Lin {( 0. V)}) iff x in ( (0). V);

      hence thesis by VECTSP_4: 30;

    end;

    registration

      let V be torsion-free Z_Module;

      let v be Vector of V;

      cluster ( Lin {v}) -> free;

      coherence

      proof

        per cases ;

          suppose v = ( 0. V);

          then ( Lin {v}) = ( (0). V) by ThLin5;

          hence thesis;

        end;

          suppose v <> ( 0. V);

          then v is non torsion by defTorsionFree;

          hence thesis by ThnTV4;

        end;

      end;

    end

    theorem :: ZMODUL06:23

    for A1,A2 be Subset of V st A1 is linearly-independent & A2 is linearly-independent & (A1 /\ A2) = {} & (A1 \/ A2) is linearly-dependent holds (( Lin A1) /\ ( Lin A2)) <> ( (0). V)

    proof

      let A1,A2 be Subset of V such that

       A1: A1 is linearly-independent & A2 is linearly-independent and

       A2: (A1 /\ A2) = {} & (A1 \/ A2) is linearly-dependent;

      consider l be Linear_Combination of (A1 \/ A2) such that

       A3: ( Sum l) = ( 0. V) & ( Carrier l) <> {} by A2;

      consider l1 be Linear_Combination of A1, l2 be Linear_Combination of A2 such that

       A4: l = (l1 + l2) by A2, ZMODUL04: 26;

      

       A5: ( Sum l) = (( Sum l1) + ( Sum l2)) by ZMODUL02: 52, A4;

      

       A6: ( Carrier l) c= (( Carrier l1) \/ ( Carrier l2)) by A4, ZMODUL02: 26;

      per cases by A3, A6;

        suppose ( Carrier l1) <> {} ;

        then

         B2: ( Sum l1) <> ( 0. V) by A1;

        

         B3: ( Sum l1) = ( - ( Sum l2)) by A3, A5, RLVECT_1: 6;

        

         B4: ( - ( Sum l2)) in ( Lin A2) by ZMODUL01: 38, ZMODUL02: 64;

        

         B5: ( Sum l1) in ( Lin A1) by ZMODUL02: 64;

        assume (( Lin A1) /\ ( Lin A2)) = ( (0). V);

        hence contradiction by B2, B5, ZMODUL02: 66, B3, B4, ZMODUL01: 94;

      end;

        suppose ( Carrier l2) <> {} ;

        then

         B2: ( Sum l2) <> ( 0. V) by A1;

        

         B3: ( Sum l2) = ( - ( Sum l1)) by A3, A5, RLVECT_1: 6;

        

         B4: ( - ( Sum l1)) in ( Lin A1) by ZMODUL01: 38, ZMODUL02: 64;

        

         B5: ( Sum l2) in ( Lin A2) by ZMODUL02: 64;

        assume (( Lin A1) /\ ( Lin A2)) = ( (0). V);

        hence contradiction by B2, B5, ZMODUL02: 66, B3, B4, ZMODUL01: 94;

      end;

    end;

    

     ThLin7: for V be Z_Module, A be linearly-independent Subset of V holds A is Basis of ( Lin A)

    proof

      let V be Z_Module, A be linearly-independent Subset of V;

      reconsider AA = A as Subset of ( Lin A) by ThLin4;

      ( (Omega). ( Lin A)) = ( Lin AA) by ZMODUL03: 20;

      hence thesis by VECTSP_7:def 3, ZMODUL03: 16;

    end;

    theorem :: ZMODUL06:24

    

     ThLin8: for V be Z_Module, W be free Subspace of V, I be Subset of V, v be Vector of V st I is linearly-independent & ( Lin I) = ( (Omega). W) & v in I holds ( (Omega). W) = (( Lin (I \ {v})) + ( Lin {v})) & (( Lin (I \ {v})) /\ ( Lin {v})) = ( (0). V) & ( Lin (I \ {v})) is free & ( Lin {v}) is free & v <> ( 0. V)

    proof

      let V be Z_Module, W be free Subspace of V, I be Subset of V, v be Vector of V such that

       A1: I is linearly-independent & ( Lin I) = ( (Omega). W) & v in I;

      

       A2: ((I \ {v}) \/ {v}) = (I \/ {v}) by XBOOLE_1: 39

      .= I by A1, ZFMISC_1: 40;

      

       A3: (I \ {v}) is linearly-independent by A1, ZMODUL02: 56, XBOOLE_1: 36;

      

       A4: v is non torsion by A1, ThLIV1;

      (( Lin (I \ {v})) /\ ( Lin {v})) = ( (0). V)

      proof

        assume (( Lin (I \ {v})) /\ ( Lin {v})) <> ( (0). V);

        then

        consider x be Vector of V such that

         B2: x in (( Lin (I \ {v})) /\ ( Lin {v})) & x <> ( 0. V) by ZMODUL04: 24;

        x in ( Lin (I \ {v})) by B2, ZMODUL01: 94;

        then

        consider lx1 be Linear_Combination of (I \ {v}) such that

         B3: x = ( Sum lx1) by ZMODUL02: 64;

        

         B4: ( Carrier lx1) <> {} by B2, B3, ZMODUL02: 23;

        reconsider llx1 = lx1 as Linear_Combination of I by XBOOLE_1: 36, ZMODUL02: 10;

        x in ( Lin {v}) by B2, ZMODUL01: 94;

        then

        consider lx2 be Linear_Combination of {v} such that

         B5: ( - x) = ( Sum lx2) by ZMODUL01: 38, ZMODUL02: 64;

        reconsider llx2 = lx2 as Linear_Combination of I by A1, ZFMISC_1: 31, ZMODUL02: 10;

        

         B6: ( Carrier lx1) c= (I \ {v}) by VECTSP_6:def 4;

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

        then ( Carrier lx1) misses ( Carrier lx2) by B6, XBOOLE_1: 64, XBOOLE_1: 79;

        then (( Carrier lx1) /\ ( Carrier lx2)) = {} by XBOOLE_0:def 7;

        then

         B7: ( Carrier (llx1 + llx2)) = (( Carrier llx1) \/ ( Carrier llx2)) by ZMODUL04: 25;

        

         B8: (( Sum llx1) + ( Sum llx2)) = ( 0. V) by B3, B5, RLVECT_1: 5;

        reconsider llx = (llx1 + llx2) as Linear_Combination of I by ZMODUL02: 27;

        ( Sum llx) = ( 0. V) by B8, ZMODUL02: 52;

        hence contradiction by A1, B4, B7;

      end;

      hence thesis by A2, A3, A4, A1, ZMODUL02: 72, ThnTV4;

    end;

    

     LmGCD1: for i1,i2 be Integer st (i1,i2) are_coprime holds ex j1,j2 be Element of INT.Ring st ((i1 * j1) + (i2 * j2)) = 1

    proof

      let i1,i2 be Integer such that

       A1: (i1,i2) are_coprime ;

      

       A2: ( |.i1.| gcd |.i2.|) = (i1 gcd i2) by INT_2: 34

      .= 1 by A1, INT_2:def 3;

      reconsider n1 = |.i1.|, n2 = |.i2.| as Nat;

      consider jj1,jj2 be Integer such that

       A3: ((jj1 * n1) + (jj2 * n2)) = 1 by A2, EULER_1: 10, INT_2:def 3;

      reconsider jj1, jj2 as Element of INT.Ring by INT_1:def 2;

      per cases ;

        suppose i1 >= 0 & i2 >= 0 ;

        then

         B1: |.i1.| = i1 & |.i2.| = i2 by ABSVALUE:def 1;

        take jj1, jj2;

        thus thesis by B1, A3;

      end;

        suppose i1 >= 0 & i2 < 0 ;

        then

         B1: |.i1.| = i1 & |.i2.| = ( - i2) by ABSVALUE:def 1;

        take jj1, ( - jj2);

        thus thesis by B1, A3;

      end;

        suppose i1 < 0 & i2 >= 0 ;

        then

         B1: |.i1.| = ( - i1) & |.i2.| = i2 by ABSVALUE:def 1;

        take ( - jj1), jj2;

        thus thesis by B1, A3;

      end;

        suppose i1 < 0 & i2 < 0 ;

        then

         B1: |.i1.| = ( - i1) & |.i2.| = ( - i2) by ABSVALUE:def 1;

        take ( - jj1), ( - jj2);

        thus thesis by B1, A3;

      end;

    end;

    

     LmGCD: for i1,i2 be Element of INT.Ring st (i1,i2) are_coprime holds ex j1,j2 be Element of INT.Ring st ((i1 * j1) + (i2 * j2)) = 1

    proof

      let i1,i2 be Element of INT.Ring ;

      assume

       A1: (i1,i2) are_coprime ;

      reconsider ii1 = i1, ii2 = i2 as Integer;

      consider j1,j2 be Element of INT.Ring such that

       T1: ((ii1 * j1) + (ii2 * j2)) = 1 by LmGCD1, A1;

      ((i1 * j1) + (i2 * j2)) = 1 by T1;

      hence thesis;

    end;

    theorem :: ZMODUL06:25

    for V be Z_Module, W be free Subspace of V holds ex A be Subset of V st A is Subset of W & A is linearly-independent & ( Lin A) = ( (Omega). W)

    proof

      let V be Z_Module, W be free Subspace of V;

      consider AW be Subset of W such that

       a1: AW is base by VECTSP_7:def 4;

      AW c= the carrier of W & the carrier of W c= the carrier of V by VECTSP_4:def 2;

      then AW c= the carrier of V;

      then

      reconsider A = AW as Subset of V;

      ( Lin A) = ( (Omega). W) by a1, ZMODUL03: 20;

      hence thesis by a1, ZMODUL03: 15;

    end;

    theorem :: ZMODUL06:26

    

     LmFree2: for V be Z_Module, W be finite-rank free Subspace of V holds ex A be finite Subset of V st A is finite Subset of W & A is linearly-independent & ( Lin A) = ( (Omega). W) & ( card A) = ( rank W)

    proof

      let V be Z_Module, W be finite-rank free Subspace of V;

      consider AW be finite Subset of W such that

       A1: AW is Basis of W by ZMODUL03:def 3;

      

       A2: AW is linearly-independent & ( Lin AW) = ( (Omega). W) by A1, VECTSP_7:def 3;

      AW c= the carrier of W & the carrier of W c= the carrier of V by VECTSP_4:def 2;

      then AW c= the carrier of V;

      then

      reconsider A = AW as finite Subset of V;

      

       A3: A is linearly-independent by ZMODUL03: 15, A1, VECTSP_7:def 3;

      

       A4: ( rank W) = ( card A) by A1, ZMODUL03:def 5;

      ( Lin A) = ( (Omega). W) by A2, ZMODUL03: 20;

      hence thesis by A3, A4;

    end;

    theorem :: ZMODUL06:27

    

     LmSumMod1: for V be torsion-free Z_Module, v1,v2 be Vector of V st v1 <> ( 0. V) & v2 <> ( 0. V) & (( Lin {v1}) /\ ( Lin {v2})) <> ( (0). V) holds ex u be Vector of V st u <> ( 0. V) & (( Lin {v1}) /\ ( Lin {v2})) = ( Lin {u})

    proof

      let V be torsion-free Z_Module, v1,v2 be Vector of V such that

       A1: v1 <> ( 0. V) & v2 <> ( 0. V) & (( Lin {v1}) /\ ( Lin {v2})) <> ( (0). V);

      consider x be Vector of V such that

       A2: x in (( Lin {v1}) /\ ( Lin {v2})) & x <> ( 0. V) by A1, ZMODUL04: 24;

      x in ( Lin {v1}) by A2, ZMODUL01: 94;

      then

      consider ii1 be Element of INT.Ring such that

       A4: x = (ii1 * v1) by ThLin1;

      x in ( Lin {v2}) by A2, ZMODUL01: 94;

      then

      consider ii2 be Element of INT.Ring such that

       A6: x = (ii2 * v2) by ThLin1;

      

       A8: ii1 <> 0 by A2, A4, ZMODUL01: 1;

      consider i1,i2 be Integer such that

       A10: ii1 = ((ii1 gcd ii2) * i1) & ii2 = ((ii1 gcd ii2) * i2) & (i1,i2) are_coprime by A8, INT_2: 23;

      reconsider I1 = i1, I2 = i2 as Element of INT.Ring by INT_1:def 2;

      

       AX1: (ii1 gcd ii2) <> 0 by A8, INT_2: 5;

      reconsider igi = (ii1 gcd ii2) as Element of INT.Ring by INT_1:def 2;

      

       a10: ii1 = (igi * I1) & ii2 = (igi * I2) by A10;

      then

       A11: x = (igi * (I1 * v1)) by VECTSP_1:def 16, A4;

      x = (igi * (I2 * v2)) by VECTSP_1:def 16, A6, a10;

      then

       A12: (I1 * v1) = (I2 * v2) by A11, AX1, ZMODUL01: 10;

      (I1 * v1) in ( Lin {v1}) & (I2 * v2) in ( Lin {v2}) by ZMODUL01: 37, ThLin2;

      then

       A13: (I1 * v1) in (( Lin {v1}) /\ ( Lin {v2})) by A12, ZMODUL01: 94;

      

       A14: for y be Vector of V st y in ( Lin {(I1 * v1)}) holds y in (( Lin {v1}) /\ ( Lin {v2}))

      proof

        let y be Vector of V such that

         B1: y in ( Lin {(I1 * v1)});

        consider iy be Element of INT.Ring such that

         B2: y = (iy * (I1 * v1)) by B1, ThLin1;

        thus y in (( Lin {v1}) /\ ( Lin {v2})) by A13, B2, ZMODUL01: 37;

      end;

      

       A16: ( Lin {(I1 * v1)}) = (( Lin {v1}) /\ ( Lin {v2}))

      proof

        assume ( Lin {(I1 * v1)}) <> (( Lin {v1}) /\ ( Lin {v2}));

        then

        consider y be Vector of V such that

         B2: y in (( Lin {v1}) /\ ( Lin {v2})) & not y in ( Lin {(I1 * v1)}) by A14, ZMODUL01: 46;

        y in ( Lin {v1}) by B2, ZMODUL01: 94;

        then

        consider iy1 be Element of INT.Ring such that

         B4: y = (iy1 * v1) by ThLin1;

        consider J1,Jy1 be Integer such that

         B5: (i1 gcd iy1) = ((J1 * i1) + (Jy1 * iy1)) by NAT_D: 68;

        reconsider j1 = J1, jy1 = Jy1 as Element of INT.Ring by INT_1:def 2;

        reconsider iyi = (i1 gcd iy1) as Element of INT.Ring by INT_1:def 2;

        iyi = ((j1 * I1) + (jy1 * iy1)) by B5;

        

        then

         B6: (iyi * v1) = (((j1 * I1) * v1) + ((jy1 * iy1) * v1)) by VECTSP_1:def 15

        .= ((j1 * (I1 * v1)) + ((jy1 * iy1) * v1)) by VECTSP_1:def 16

        .= ((j1 * (I1 * v1)) + (jy1 * y)) by B4, VECTSP_1:def 16;

        

         B7: (j1 * (I1 * v1)) in (( Lin {v1}) /\ ( Lin {v2})) by A13, ZMODUL01: 37;

        (jy1 * y) in (( Lin {v1}) /\ ( Lin {v2})) by B2, ZMODUL01: 37;

        then

         B8: (iyi * v1) in (( Lin {v1}) /\ ( Lin {v2})) by B6, B7, ZMODUL01: 36;

        (iyi * v1) in ( Lin {v2}) by B8, ZMODUL01: 94;

        then

        consider iiy2 be Element of INT.Ring such that

         B10: (iyi * v1) = (iiy2 * v2) by ThLin1;

        (i1 gcd iy1) divides i1 by INT_2:def 2;

        then

        consider I3 be Integer such that

         B11: i1 = ((i1 gcd iy1) * I3) by INT_1:def 3;

        reconsider i3 = I3 as Element of INT.Ring by INT_1:def 2;

        i1 = (iyi * i3) by B11;

        

        then

         B12: (I1 * v1) = (i3 * (iyi * v1)) by VECTSP_1:def 16

        .= ((i3 * iiy2) * v2) by VECTSP_1:def 16, B10;

        per cases ;

          suppose (i3 * iiy2) = i2;

          then

           C3: i3 divides i2 by INT_1:def 3;

          

           C2: i3 divides i1 by B11, INT_1:def 3;

          per cases ;

            suppose (i1 gcd i2) = 1;

            then i3 = 1 or i3 = ( - 1) by INT_2: 13, C3, C2, INT_2: 22;

            then i1 divides iy1 or ( - i1) divides iy1 by INT_2:def 2, B11;

            then

            consider iy3 be Integer such that

             D2: iy1 = (i1 * iy3) by INT_1:def 3, INT_2: 10;

            reconsider Iy3 = iy3 as Element of INT.Ring by INT_1:def 2;

            iy1 = (I1 * Iy3) by D2;

            then y = (Iy3 * (I1 * v1)) by VECTSP_1:def 16, B4;

            hence contradiction by B2, ZMODUL01: 37, ThLin2;

          end;

            suppose (i1 gcd i2) <> 1;

            hence contradiction by A10, INT_2:def 3;

          end;

        end;

          suppose (i3 * iiy2) <> i2;

          then

           C2: (i2 - (i3 * iiy2)) <> 0 ;

          ( 0. V) = ((I2 * v2) - ((i3 * iiy2) * v2)) by RLVECT_1: 15, A12, B12

          .= ((I2 - (i3 * iiy2)) * v2) by ZMODUL01: 9;

          then v2 is torsion by C2;

          hence contradiction by A1, defTorsionFree;

        end;

      end;

      i1 <> ( 0. INT.Ring ) by A10, A2, A4, ZMODUL01: 1;

      hence thesis by A16, A1, ZMODUL01:def 7;

    end;

    theorem :: ZMODUL06:28

    

     LmSumMod2: for V be torsion-free Z_Module, v1,v2 be Vector of V st v1 <> ( 0. V) & v2 <> ( 0. V) & (( Lin {v1}) /\ ( Lin {v2})) <> ( (0). V) holds ex u be Vector of V st u <> ( 0. V) & (( Lin {v1}) + ( Lin {v2})) = ( Lin {u})

    proof

      let V be torsion-free Z_Module, v1,v2 be Vector of V such that

       A1: v1 <> ( 0. V) & v2 <> ( 0. V) & (( Lin {v1}) /\ ( Lin {v2})) <> ( (0). V);

      consider x be Vector of V such that

       A2: x <> ( 0. V) & (( Lin {v1}) /\ ( Lin {v2})) = ( Lin {x}) by A1, LmSumMod1;

      

       A3: x in ( Lin {x}) by ZMODUL02: 65, ZFMISC_1: 31;

      then x in ( Lin {v1}) by A2, ZMODUL01: 94;

      then

      consider i1 be Element of INT.Ring such that

       A4: x = (i1 * v1) by ThLin1;

      x in ( Lin {v2}) by A2, A3, ZMODUL01: 94;

      then

      consider i2 be Element of INT.Ring such that

       A5: x = (i2 * v2) by ThLin1;

      ( |.i1.| gcd |.i2.|) = 1

      proof

        set n1 = |.i1.|;

        set n2 = |.i2.|;

        assume

         ASB: (n1 gcd n2) <> 1;

        per cases ;

          suppose (n1 gcd n2) = 0 ;

          then n1 = 0 & n2 = 0 by INT_2: 5;

          hence contradiction by ABSVALUE: 2, A2, A4, ZMODUL01: 1;

        end;

          suppose (n1 gcd n2) <> 0 ;

          then (n1 gcd n2) > 1 by ASB, NAT_1: 25;

          then

           C1: (i1 gcd i2) > 1 by INT_2: 34;

          (i1 gcd i2) divides i1 by INT_2:def 2;

          then

          consider k1 be Integer such that

           C2: i1 = ((i1 gcd i2) * k1) by INT_1:def 3;

          (i1 gcd i2) divides i2 by INT_2:def 2;

          then

          consider k2 be Integer such that

           C3: i2 = ((i1 gcd i2) * k2) by INT_1:def 3;

          reconsider K1 = k1, K2 = k2 as Element of INT.Ring by INT_1:def 2;

          reconsider igi = (i1 gcd i2) as Element of INT.Ring by INT_1:def 2;

          

           c2: i1 = (igi * K1) & i2 = (igi * K2) by C2, C3;

          

          then

           C4: (igi * (K1 * v1)) = ((igi * K2) * v2) by VECTSP_1:def 16, A4, A5

          .= (igi * (K2 * v2)) by VECTSP_1:def 16;

          

           C5: (K1 * v1) = (K2 * v2) by ZMODUL01: 10, C1, C4;

          

           C6: (K1 * v1) in ( Lin {v1}) by ZMODUL01: 37, ThLin2;

          (K2 * v2) in ( Lin {v2}) by ZMODUL01: 37, ThLin2;

          then

          consider ikv be Element of INT.Ring such that

           C8: (K1 * v1) = (ikv * x) by ThLin1, A2, C5, C6, ZMODUL01: 94;

          x = (igi * (K1 * v1)) by VECTSP_1:def 16, A4, c2

          .= ((igi * ikv) * x) by VECTSP_1:def 16, C8;

          

          then

           C9: ( 0. V) = (((igi * ikv) * x) - x) by RLVECT_1: 15

          .= (((igi * ikv) * x) - (( 1. INT.Ring ) * x)) by VECTSP_1:def 17

          .= (((igi * ikv) - ( 1. INT.Ring )) * x) by ZMODUL01: 9;

          ((igi * ikv) - ( 1. INT.Ring )) <> ( 0. INT.Ring ) by C1, INT_1: 9;

          hence contradiction by A2, C9, ZMODUL01:def 7;

        end;

      end;

      then (i1 gcd i2) = 1 by INT_2: 34;

      then

      consider j1,j2 be Element of INT.Ring such that

       A7: ((i1 * j1) + (i2 * j2)) = 1 by LmGCD, INT_2:def 3;

      reconsider J1 = j1, J2 = j2 as Element of INT.Ring ;

      

       a7: ((i1 * J1) + (i2 * J2)) = ( 1. INT.Ring ) by A7;

      reconsider u = ((J1 * v2) + (J2 * v1)) as Vector of V;

      

       A8: u in ( Lin {u}) by ZMODUL02: 65, ZFMISC_1: 31;

      

       B1: (i1 * u) = ((i1 * (J1 * v2)) + (i1 * (J2 * v1))) by VECTSP_1:def 14

      .= ((i1 * (J1 * v2)) + ((i1 * J2) * v1)) by VECTSP_1:def 16

      .= ((i1 * (J1 * v2)) + (J2 * (i1 * v1))) by VECTSP_1:def 16

      .= (((i1 * J1) * v2) + (J2 * (i2 * v2))) by VECTSP_1:def 16, A4, A5

      .= (((i1 * J1) * v2) + ((i2 * J2) * v2)) by VECTSP_1:def 16

      .= (((i1 * J1) + (i2 * J2)) * v2) by VECTSP_1:def 15

      .= v2 by VECTSP_1:def 17, a7;

      

       B3: (i2 * u) = ((i2 * (J1 * v2)) + (i2 * (J2 * v1))) by VECTSP_1:def 14

      .= (((i2 * J1) * v2) + (i2 * (J2 * v1))) by VECTSP_1:def 16

      .= ((J1 * (i2 * v2)) + (i2 * (J2 * v1))) by VECTSP_1:def 16

      .= ((J1 * (i2 * v2)) + ((i2 * J2) * v1)) by VECTSP_1:def 16

      .= (((i1 * J1) * v1) + ((i2 * J2) * v1)) by VECTSP_1:def 16, A4, A5

      .= (((i1 * J1) + (i2 * J2)) * v1) by VECTSP_1:def 15

      .= v1 by VECTSP_1:def 17, a7;

      (( Lin {v1}) + ( Lin {v2})) = ( Lin {u})

      proof

        

         B5: for vx be Vector of V st vx in ( Lin {v1}) holds vx in ( Lin {u})

        proof

          let vx be Vector of V such that

           C1: vx in ( Lin {v1});

          consider ivx1 be Element of INT.Ring such that

           C2: vx = (ivx1 * v1) by C1, ThLin1;

          vx = ((ivx1 * i2) * u) by VECTSP_1:def 16, B3, C2;

          hence thesis by A8, ZMODUL01: 37;

        end;

        

         B6: for vx be Vector of V st vx in ( Lin {v2}) holds vx in ( Lin {u})

        proof

          let vx be Vector of V such that

           C1: vx in ( Lin {v2});

          consider ivx2 be Element of INT.Ring such that

           C2: vx = (ivx2 * v2) by C1, ThLin1;

          vx = ((ivx2 * i1) * u) by VECTSP_1:def 16, B1, C2;

          hence thesis by A8, ZMODUL01: 37;

        end;

        for vx be Vector of V holds vx in (( Lin {v1}) + ( Lin {v2})) iff vx in ( Lin {u})

        proof

          let vx be Vector of V;

          hereby

            assume vx in (( Lin {v1}) + ( Lin {v2}));

            then

            consider vx1,vx2 be Vector of V such that

             C2: vx1 in ( Lin {v1}) & vx2 in ( Lin {v2}) & vx = (vx1 + vx2) by ZMODUL01: 92;

            

             C3: vx1 in ( Lin {u}) by B5, C2;

            vx2 in ( Lin {u}) by B6, C2;

            hence vx in ( Lin {u}) by C2, C3, ZMODUL01: 36;

          end;

          assume vx in ( Lin {u});

          then

          consider ivx be Element of INT.Ring such that

           C2: vx = (ivx * u) by ThLin1;

          

           C3: vx = ((ivx * (J1 * v2)) + (ivx * (J2 * v1))) by VECTSP_1:def 14, C2

          .= (((ivx * J1) * v2) + (ivx * (J2 * v1))) by VECTSP_1:def 16

          .= (((ivx * J1) * v2) + ((ivx * J2) * v1)) by VECTSP_1:def 16;

          v1 in ( Lin {v1}) by ZMODUL02: 65, ZFMISC_1: 31;

          then

           C4: ((ivx * J2) * v1) in ( Lin {v1}) by ZMODUL01: 37;

          v2 in ( Lin {v2}) by ZMODUL02: 65, ZFMISC_1: 31;

          then ((ivx * J1) * v2) in ( Lin {v2}) by ZMODUL01: 37;

          hence vx in (( Lin {v1}) + ( Lin {v2})) by C3, C4, ZMODUL01: 92;

        end;

        hence thesis by ZMODUL01: 46;

      end;

      hence thesis by A1, B3, ZMODUL01: 1;

    end;

    theorem :: ZMODUL06:29

    

     LmSumMod3: for V be torsion-free Z_Module, W be finite-rank free Subspace of V, v,u be Vector of V st v <> ( 0. V) & u <> ( 0. V) & (W /\ ( Lin {v})) = ( (0). V) & ((W + ( Lin {u})) /\ ( Lin {v})) <> ( (0). V) & (( Lin {u}) /\ ( Lin {v})) = ( (0). V) holds ex w1,w2 be Vector of V st w1 <> ( 0. V) & w2 <> ( 0. V) & ((W + ( Lin {u})) + ( Lin {v})) = ((W + ( Lin {w1})) + ( Lin {w2})) & (W /\ ( Lin {w1})) <> ( (0). V) & ((W + ( Lin {w1})) /\ ( Lin {w2})) = ( (0). V) & u in (( Lin {w1}) + ( Lin {w2})) & v in (( Lin {w1}) + ( Lin {w2})) & w1 in (( Lin {u}) + ( Lin {v})) & w2 in (( Lin {u}) + ( Lin {v}))

    proof

      let V be torsion-free Z_Module, W be finite-rank free Subspace of V, v,u be Vector of V such that

       A1: v <> ( 0. V) & u <> ( 0. V) and

       A2: (W /\ ( Lin {v})) = ( (0). V) and

       A3: ((W + ( Lin {u})) /\ ( Lin {v})) <> ( (0). V) & (( Lin {u}) /\ ( Lin {v})) = ( (0). V);

      consider x be Vector of V such that

       A4: x in ((W + ( Lin {u})) /\ ( Lin {v})) & x <> ( 0. V) by A3, ZMODUL04: 24;

      x in (W + ( Lin {u})) by A4, ZMODUL01: 94;

      then

      consider x1,x2 be Vector of V such that

       A6: x1 in W & x2 in ( Lin {u}) & x = (x1 + x2) by ZMODUL01: 92;

      

       A7: x in ( Lin {v}) by A4, ZMODUL01: 94;

      consider iv be Element of INT.Ring such that

       A9: x = (iv * v) by A7, ThLin1;

      

       A10: iv <> 0 by A4, A9, ZMODUL01: 1;

      consider iu2 be Element of INT.Ring such that

       A11: x2 = (iu2 * u) by A6, ThLin1;

      consider iiv,iiu2 be Integer such that

       A13: iv = ((iv gcd iu2) * iiv) & iu2 = ((iv gcd iu2) * iiu2) & (iiv,iiu2) are_coprime by A10, INT_2: 23;

      reconsider iiv, iiu2 as Element of INT.Ring by INT_1:def 2;

      consider Jv,Ju2 be Element of INT.Ring such that

       A14: ((iiv * Jv) + (iiu2 * Ju2)) = 1 by A13, LmGCD;

      reconsider jv = Jv, ju2 = Ju2 as Element of INT.Ring ;

      

       a14: ((iiv * jv) + (iiu2 * ju2)) = ( 1. INT.Ring ) by A14;

      

       A15: (x - x2) = (x1 + (x2 - x2)) by RLVECT_1:def 3, A6

      .= (x1 + ( 0. V)) by RLVECT_1: 15

      .= x1;

      set w1 = ((iiv * v) - (iiu2 * u));

      set w2 = ((jv * u) + (ju2 * v));

      

       A16: w1 <> ( 0. V)

      proof

        assume w1 = ( 0. V);

        then

         B1: (iiv * v) = (iiu2 * u) by RLVECT_1: 21;

        

         B2: (iiv * v) in ( Lin {v}) by ZMODUL01: 37, ThLin2;

        (iiv * v) in ( Lin {u}) by B1, ZMODUL01: 37, ThLin2;

        then

         B3: (iiv * v) in (( Lin {u}) /\ ( Lin {v})) by B2, ZMODUL01: 94;

        iiv <> ( 0. INT.Ring ) by A13, A4, A9, ZMODUL01: 1;

        hence contradiction by A3, B3, ZMODUL02: 66, A1, ZMODUL01:def 7;

      end;

      reconsider igu = (iv gcd iu2) as Element of INT.Ring by INT_1:def 2;

      

       a13: iv = (igu * iiv) & iu2 = (igu * iiu2) by A13;

      

       AX1: (igu * w1) in W

      proof

        (igu * w1) = ((igu * (iiv * v)) - (igu * (iiu2 * u))) by ZMODUL01: 8

        .= (((igu * iiv) * v) - (igu * (iiu2 * u))) by VECTSP_1:def 16

        .= ((iv * v) - (iu2 * u)) by a13, VECTSP_1:def 16;

        hence (igu * w1) in W by A15, A6, A9, A11;

      end;

      

       AX2: (iv gcd iu2) <> ( 0. INT.Ring ) by A10, INT_2: 5;

      

       A17: (W /\ ( Lin {w1})) <> ( (0). V)

      proof

        (igu * w1) in ( Lin {w1}) by ZMODUL01: 37, ThLin2;

        then (igu * w1) in (W /\ ( Lin {w1})) by AX1, ZMODUL01: 94;

        hence thesis by ZMODUL02: 66, A16, AX2, ZMODUL01:def 7;

      end;

      

       A18: u = ((iiv * w2) - (ju2 * w1))

      proof

        

        thus ((iiv * w2) - (ju2 * w1)) = (((iiv * (jv * u)) + (iiv * (ju2 * v))) - (ju2 * ((iiv * v) - (iiu2 * u)))) by VECTSP_1:def 14

        .= ((((iiv * jv) * u) + (iiv * (ju2 * v))) - (ju2 * ((iiv * v) - (iiu2 * u)))) by VECTSP_1:def 16

        .= ((((iiv * jv) * u) + ((iiv * ju2) * v)) - (ju2 * ((iiv * v) - (iiu2 * u)))) by VECTSP_1:def 16

        .= ((((iiv * ju2) * v) + ((iiv * jv) * u)) - ((ju2 * (iiv * v)) - (ju2 * (iiu2 * u)))) by ZMODUL01: 8

        .= (((((iiv * ju2) * v) + ((iiv * jv) * u)) - (ju2 * (iiv * v))) + (ju2 * (iiu2 * u))) by RLVECT_1: 29

        .= (((((iiv * jv) * u) + ((iiv * ju2) * v)) - (ju2 * (iiv * v))) + ((ju2 * iiu2) * u)) by VECTSP_1:def 16

        .= ((((iiv * jv) * u) + (((iiv * ju2) * v) - (ju2 * (iiv * v)))) + ((ju2 * iiu2) * u)) by RLVECT_1: 28

        .= ((((iiv * jv) * u) + (((iiv * ju2) * v) - ((ju2 * iiv) * v))) + ((ju2 * iiu2) * u)) by VECTSP_1:def 16

        .= ((((iiv * jv) * u) + ( 0. V)) + ((ju2 * iiu2) * u)) by RLVECT_1: 15

        .= (((iiv * jv) + (iiu2 * ju2)) * u) by VECTSP_1:def 15

        .= u by VECTSP_1:def 17, a14;

      end;

      

       A19: v = ((jv * w1) + (iiu2 * w2))

      proof

        

        thus ((jv * w1) + (iiu2 * w2)) = (((jv * (iiv * v)) - (jv * (iiu2 * u))) + (iiu2 * ((jv * u) + (ju2 * v)))) by ZMODUL01: 8

        .= ((((jv * iiv) * v) - (jv * (iiu2 * u))) + (iiu2 * ((jv * u) + (ju2 * v)))) by VECTSP_1:def 16

        .= ((((jv * iiv) * v) + (iiu2 * ((jv * u) + (ju2 * v)))) - (jv * (iiu2 * u))) by RLVECT_1:def 3

        .= (((jv * iiv) * v) + ((iiu2 * ((jv * u) + (ju2 * v))) - (jv * (iiu2 * u)))) by RLVECT_1:def 3

        .= (((jv * iiv) * v) + ((iiu2 * ((ju2 * v) + (jv * u))) - ((jv * iiu2) * u))) by VECTSP_1:def 16

        .= (((jv * iiv) * v) + (((iiu2 * (ju2 * v)) + (iiu2 * (jv * u))) - ((jv * iiu2) * u))) by VECTSP_1:def 14

        .= (((iiv * jv) * v) + ((iiu2 * (ju2 * v)) + ((iiu2 * (jv * u)) - ((jv * iiu2) * u)))) by RLVECT_1: 28

        .= (((iiv * jv) * v) + ((iiu2 * (ju2 * v)) + (((iiu2 * jv) * u) - ((iiu2 * jv) * u)))) by VECTSP_1:def 16

        .= (((iiv * jv) * v) + ((iiu2 * (ju2 * v)) + ( 0. V))) by RLVECT_1: 15

        .= (((iiv * jv) * v) + ((iiu2 * ju2) * v)) by VECTSP_1:def 16

        .= (((iiv * jv) + (iiu2 * ju2)) * v) by VECTSP_1:def 15

        .= v by VECTSP_1:def 17, a14;

      end;

      

       A20: u in (( Lin {w1}) + ( Lin {w2}))

      proof

        (ju2 * w1) in ( Lin {w1}) by ZMODUL01: 37, ThLin2;

        then

         B1: ( - (ju2 * w1)) in ( Lin {w1}) by ZMODUL01: 38;

        (iiv * w2) in ( Lin {w2}) by ZMODUL01: 37, ThLin2;

        hence thesis by A18, B1, ZMODUL01: 92;

      end;

      

       A21: v in (( Lin {w1}) + ( Lin {w2}))

      proof

        

         B1: (jv * w1) in ( Lin {w1}) by ZMODUL01: 37, ThLin2;

        (iiu2 * w2) in ( Lin {w2}) by ZMODUL01: 37, ThLin2;

        hence thesis by A19, B1, ZMODUL01: 92;

      end;

      

       A22: w1 in (( Lin {u}) + ( Lin {v}))

      proof

        (iiu2 * u) in ( Lin {u}) by ZMODUL01: 37, ThLin2;

        then

         B1: ( - (iiu2 * u)) in ( Lin {u}) by ZMODUL01: 38;

        (iiv * v) in ( Lin {v}) by ZMODUL01: 37, ThLin2;

        hence thesis by B1, ZMODUL01: 92;

      end;

      

       A23: w2 in (( Lin {u}) + ( Lin {v}))

      proof

        

         B1: (jv * u) in ( Lin {u}) by ZMODUL01: 37, ThLin2;

        (ju2 * v) in ( Lin {v}) by ZMODUL01: 37, ThLin2;

        hence thesis by B1, ZMODUL01: 92;

      end;

      

       A24: for x be object holds x in ((W + ( Lin {u})) + ( Lin {v})) implies x in ((W + ( Lin {w1})) + ( Lin {w2}))

      proof

        let x be object;

        assume x in ((W + ( Lin {u})) + ( Lin {v}));

        then

        consider xx,x3 be Vector of V such that

         B1: xx in (W + ( Lin {u})) & x3 in ( Lin {v}) & x = (xx + x3) by ZMODUL01: 92;

        consider x1,x2 be Vector of V such that

         B2: x1 in W & x2 in ( Lin {u}) & xx = (x1 + x2) by B1, ZMODUL01: 92;

        consider ix2 be Element of INT.Ring such that

         B3: x2 = (ix2 * u) by B2, ThLin1;

        consider ix3 be Element of INT.Ring such that

         B4: x3 = (ix3 * v) by B1, ThLin1;

        

         B5: x2 in (( Lin {w1}) + ( Lin {w2})) by A20, B3, ZMODUL01: 37;

        x3 in (( Lin {w1}) + ( Lin {w2})) by A21, B4, ZMODUL01: 37;

        then (x2 + x3) in (( Lin {w1}) + ( Lin {w2})) by B5, ZMODUL01: 36;

        then (x1 + (x2 + x3)) in (W + (( Lin {w1}) + ( Lin {w2}))) by B2, ZMODUL01: 92;

        then (xx + x3) in (W + (( Lin {w1}) + ( Lin {w2}))) by B2, RLVECT_1:def 3;

        hence x in ((W + ( Lin {w1})) + ( Lin {w2})) by B1, ZMODUL01: 96;

      end;

      for x be object holds x in ((W + ( Lin {w1})) + ( Lin {w2})) implies x in ((W + ( Lin {u})) + ( Lin {v}))

      proof

        let x be object;

        assume x in ((W + ( Lin {w1})) + ( Lin {w2}));

        then

        consider xx,x3 be Vector of V such that

         B1: xx in (W + ( Lin {w1})) & x3 in ( Lin {w2}) & x = (xx + x3) by ZMODUL01: 92;

        consider x1,x2 be Vector of V such that

         B2: x1 in W & x2 in ( Lin {w1}) & xx = (x1 + x2) by B1, ZMODUL01: 92;

        consider ix2 be Element of INT.Ring such that

         B3: x2 = (ix2 * w1) by B2, ThLin1;

        consider ix3 be Element of INT.Ring such that

         B4: x3 = (ix3 * w2) by B1, ThLin1;

        

         B5: x2 in (( Lin {u}) + ( Lin {v})) by A22, B3, ZMODUL01: 37;

        x3 in (( Lin {u}) + ( Lin {v})) by A23, B4, ZMODUL01: 37;

        then (x2 + x3) in (( Lin {u}) + ( Lin {v})) by B5, ZMODUL01: 36;

        then (x1 + (x2 + x3)) in (W + (( Lin {u}) + ( Lin {v}))) by B2, ZMODUL01: 92;

        then (xx + x3) in (W + (( Lin {u}) + ( Lin {v}))) by B2, RLVECT_1:def 3;

        hence x in ((W + ( Lin {u})) + ( Lin {v})) by B1, ZMODUL01: 96;

      end;

      then for x be Vector of V holds x in ((W + ( Lin {u})) + ( Lin {v})) iff x in ((W + ( Lin {w1})) + ( Lin {w2})) by A24;

      then

       A25: ((W + ( Lin {u})) + ( Lin {v})) = ((W + ( Lin {w1})) + ( Lin {w2})) by ZMODUL01: 46;

      

       A26: w2 <> ( 0. V)

      proof

        assume

         B0: w2 = ( 0. V);

        then

         B1: (ju2 * v) = ( - (jv * u)) by RLVECT_1: 6;

        

         B2: (ju2 * v) in ( Lin {v}) by ZMODUL01: 37, ThLin2;

        (jv * u) in ( Lin {u}) by ZMODUL01: 37, ThLin2;

        then (ju2 * v) in ( Lin {u}) by B1, ZMODUL01: 38;

        then

         B3: (ju2 * v) in (( Lin {u}) /\ ( Lin {v})) by B2, ZMODUL01: 94;

        ju2 <> ( 0. INT.Ring )

        proof

          assume

           C1: ju2 = ( 0. INT.Ring );

          then ((jv * u) + ( 0. V)) = ( 0. V) by B0, ZMODUL01: 1;

          then jv = ( 0. INT.Ring ) by A1, ZMODUL01:def 7;

          hence contradiction by A14, C1;

        end;

        hence contradiction by A3, B3, ZMODUL02: 66, A1, ZMODUL01:def 7;

      end;

      ((W + ( Lin {w1})) /\ ( Lin {w2})) = ( (0). V)

      proof

        assume ((W + ( Lin {w1})) /\ ( Lin {w2})) <> ( (0). V);

        then

        consider wx be Vector of V such that

         B2: wx in ((W + ( Lin {w1})) /\ ( Lin {w2})) & wx <> ( 0. V) by ZMODUL04: 24;

        wx in (W + ( Lin {w1})) by B2, ZMODUL01: 94;

        then

        consider wx1,wx2 be Vector of V such that

         B3: wx1 in W & wx2 in ( Lin {w1}) & wx = (wx1 + wx2) by ZMODUL01: 92;

        consider iwx1 be Element of INT.Ring such that

         B4: wx2 = (iwx1 * w1) by B3, ThLin1;

        reconsider igu = (iv gcd iu2) as Element of INT.Ring by INT_1:def 2;

        

         B5: (igu * wx) in W

        proof

          

           C1: (igu * wx) = ((igu * wx1) + (igu * wx2)) by VECTSP_1:def 14, B3

          .= ((igu * wx1) + ((igu * iwx1) * w1)) by VECTSP_1:def 16, B4

          .= ((igu * wx1) + (iwx1 * (igu * w1))) by VECTSP_1:def 16;

          

           C2: (igu * wx1) in W by B3, ZMODUL01: 37;

          (iwx1 * (igu * w1)) in W by AX1, ZMODUL01: 37;

          hence thesis by C1, C2, ZMODUL01: 36;

        end;

        wx in ( Lin {w2}) by B2, ZMODUL01: 94;

        then

        consider iwx2 be Element of INT.Ring such that

         B6: wx = (iwx2 * w2) by ThLin1;

        

         B7: iwx2 <> 0 by B2, B6, ZMODUL01: 1;

        ex wiu1,wiu2 be Vector of V st (iu2 * w2) = (wiu1 + wiu2) & wiu1 in W & wiu2 = (igu * v)

        proof

          

           C1: (iu2 * w2) = ((iu2 * (jv * u)) + (iu2 * (ju2 * v))) by VECTSP_1:def 14

          .= (((iu2 * jv) * u) + (iu2 * (ju2 * v))) by VECTSP_1:def 16

          .= (((jv * iu2) * u) + ((iu2 * ju2) * v)) by VECTSP_1:def 16

          .= ((jv * (iu2 * u)) + ((iu2 * ju2) * v)) by VECTSP_1:def 16;

          reconsider wiviu = ((iv * v) - (iu2 * u)) as Vector of W by A15, A6, A9, A11;

          

           C2: wiviu in W;

          reconsider wiviu as Vector of V;

          ((iv * v) - wiviu) = (((iv * v) - (iv * v)) + (iu2 * u)) by RLVECT_1: 29

          .= (( 0. V) + (iu2 * u)) by RLVECT_1: 15

          .= (iu2 * u);

          

          then

           C3: (iu2 * w2) = (((jv * (iv * v)) - (jv * wiviu)) + ((iu2 * ju2) * v)) by ZMODUL01: 8, C1

          .= (((jv * (iv * v)) + ((iu2 * ju2) * v)) - (jv * wiviu)) by RLVECT_1:def 3

          .= ((((jv * iv) * v) + ((iu2 * ju2) * v)) - (jv * wiviu)) by VECTSP_1:def 16

          .= ((((jv * iv) + (iu2 * ju2)) * v) - (jv * wiviu)) by VECTSP_1:def 15

          .= (((igu * ((iiv * jv) + (iiu2 * ju2))) * v) - (jv * wiviu)) by A13

          .= (( - (jv * wiviu)) + (igu * v)) by A14;

          

           C4: (jv * wiviu) in W by C2, ZMODUL01: 37;

          take ( - (jv * wiviu)), (igu * v);

          thus thesis by C3, C4, ZMODUL01: 38;

        end;

        then

        consider wiu1,wiu2 be Vector of V such that

         B8: (iu2 * w2) = (wiu1 + wiu2) & wiu1 in W & wiu2 = (igu * v);

        

         B9: (iu2 * wx) = ((iu2 * iwx2) * w2) by VECTSP_1:def 16, B6

        .= (iwx2 * (iu2 * w2)) by VECTSP_1:def 16

        .= ((iwx2 * wiu1) + (iwx2 * (igu * v))) by VECTSP_1:def 14, B8

        .= ((iwx2 * wiu1) + ((iwx2 * igu) * v)) by VECTSP_1:def 16;

        (iu2 * wx) = (iiu2 * (igu * wx)) by VECTSP_1:def 16, a13;

        then

         B10: (iu2 * wx) in W by B5, ZMODUL01: 37;

        (iwx2 * wiu1) in W by B8, ZMODUL01: 37;

        then

         B11: ((iu2 * wx) - (iwx2 * wiu1)) in W by B10, ZMODUL01: 39;

        

         B12: ((iu2 * wx) - (iwx2 * wiu1)) = (((iwx2 * wiu1) - (iwx2 * wiu1)) + ((iwx2 * igu) * v)) by RLVECT_1:def 3, B9

        .= (( 0. V) + ((iwx2 * igu) * v)) by RLVECT_1: 15

        .= ((iwx2 * igu) * v);

        ((iwx2 * igu) * v) in ( Lin {v}) by ZMODUL01: 37, ThLin2;

        then ((iwx2 * igu) * v) in (W /\ ( Lin {v})) by B12, ZMODUL01: 94, B11;

        hence contradiction by A2, ZMODUL02: 66, A1, ZMODUL01:def 7, AX2, B7;

      end;

      hence thesis by A16, A17, A20, A21, A22, A23, A25, A26;

    end;

    theorem :: ZMODUL06:30

    

     LmSumModX: for V be torsion-free Z_Module, W be finite-rank free Subspace of V, v be Vector of V st v <> ( 0. V) & (W /\ ( Lin {v})) <> ( (0). V) holds (W + ( Lin {v})) is free

    proof

      let V be torsion-free Z_Module;

      defpred P[ Nat] means for W be finite-rank free Subspace of V, v be Vector of V st v <> ( 0. V) & (W /\ ( Lin {v})) <> ( (0). V) & ( rank W) = ($1 + 1) holds (W + ( Lin {v})) is free;

      

       A1: P[ 0 ]

      proof

        let W be finite-rank free Subspace of V, v be Vector of V such that

         B1: v <> ( 0. V) & (W /\ ( Lin {v})) <> ( (0). V) and

         B2: ( rank W) = ( 0 + 1);

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

        proof

          consider w be Vector of W such that

           C1: w <> ( 0. W) & ( (Omega). W) = ( Lin {w}) by ZMODUL05: 5, B2;

          reconsider wv = w as Vector of V by ZMODUL01: 25;

          

           C2: ( (Omega). W) = ( Lin {wv}) by C1, ZMODUL03: 20;

          

           C3: ( (Omega). ( Lin {v})) = ( Lin {v});

          then

           C4: (W + ( Lin {v})) = (( Lin {wv}) + ( Lin {v})) by C2, ZMODUL04: 22;

          

           C5: (( Lin {wv}) /\ ( Lin {v})) <> ( (0). V) by B1, C2, C3, ZMODUL04: 23;

          wv <> ( 0. V) by C1, ZMODUL01: 26;

          hence thesis by B1, C4, C5, LmSumMod2;

        end;

        then

        consider x be Vector of V such that

         B3: x <> ( 0. V) & (W + ( Lin {v})) = ( Lin {x});

        thus thesis by B3;

      end;

      

       A2: for n be Nat st P[n] holds P[(n + 1)]

      proof

        let n be Nat such that

         B1: P[n];

        let W be finite-rank free Subspace of V, v be Vector of V such that

         B2: v <> ( 0. V) & (W /\ ( Lin {v})) <> ( (0). V) & ( rank W) = ((n + 1) + 1);

        set I = the Basis of W;

        

         B3: ( card I) = (n + 2) by B2, ZMODUL03:def 5;

        then I <> ( {} the carrier of W);

        then

        consider w be object such that

         B4: w in I by XBOOLE_0: 7;

        reconsider w as Vector of W by B4;

        

         B5: W is_the_direct_sum_of (( Lin (I \ {w})),( Lin {w})) by B4, ZMODUL04: 33;

        I c= the carrier of W & the carrier of W c= the carrier of V by VECTSP_4:def 2;

        then I c= the carrier of V;

        then

        reconsider IV = I as finite Subset of V;

        reconsider wv = w as Vector of V by ZMODUL01: 25;

        

         B6: ( Lin (I \ {w})) = ( Lin (IV \ {wv})) by ZMODUL03: 20;

        

         B7: ( Lin {w}) = ( Lin {wv}) by ZMODUL03: 20;

        then

        reconsider WLinIw = ( Lin (I \ {w})), WLinw = ( Lin {w}) as Subspace of (( Lin (IV \ {wv})) + ( Lin {wv})) by B6, ZMODUL01: 97;

        

         B8: (( Lin (IV \ {wv})) /\ ( Lin {wv})) = ( (0). V)

        proof

          

           C1: for x be object holds x in (( Lin (IV \ {wv})) /\ ( Lin {wv})) implies x in ( (0). V)

          proof

            let x be object;

            assume

             D1: x in (( Lin (IV \ {wv})) /\ ( Lin {wv}));

            

             D2: (( Lin (I \ {w})) /\ ( Lin {w})) = ( (0). V) by ZMODUL01: 51, B5;

            x in ( Lin (I \ {w})) & x in ( Lin {w}) by B6, B7, D1, ZMODUL01: 94;

            hence thesis by D2, ZMODUL01: 94;

          end;

          for x be object holds x in ( (0). V) implies x in (( Lin (IV \ {wv})) /\ ( Lin {wv}))

          proof

            let x be object;

            assume x in ( (0). V);

            then x = ( 0. V) by ZMODUL02: 66;

            hence thesis by ZMODUL01: 33;

          end;

          then for x be Vector of V holds x in (( Lin (IV \ {wv})) /\ ( Lin {wv})) iff x in ( (0). V) by C1;

          hence thesis by ZMODUL01: 46;

        end;

        I is linearly-independent by VECTSP_7:def 3;

        then (I \ {w}) is linearly-independent by XBOOLE_1: 36, ZMODUL02: 56;

        then

         B9: (IV \ {wv}) is linearly-independent by ZMODUL03: 15;

        reconsider LinIw = ( Lin (IV \ {wv})) as finite-rank free Subspace of V by B9;

        reconsider IVwv = (IV \ {wv}) as Subset of ( Lin (IV \ {wv})) by ThLin4;

        ( (Omega). ( Lin (IV \ {wv}))) = ( Lin IVwv) by ZMODUL03: 20;

        then

         B11: IVwv is Basis of LinIw by VECTSP_7:def 3, B9, ZMODUL03: 16;

        

         B12: ( card (I \ {w})) = (( card I) - ( card {w})) by B4, ZFMISC_1: 31, CARD_2: 44

        .= ((n + 2) - 1) by B3, CARD_1: 30

        .= (n + 1);

        

         B13: ( rank LinIw) = (n + 1) by B12, B11, ZMODUL03:def 5;

        

         B15: (( Lin (IV \ {wv})) + ( Lin {v})) is free

        proof

          per cases ;

            suppose (( Lin (IV \ {wv})) /\ ( Lin {v})) = ( (0). V);

            hence thesis by B9, ZMODUL04: 31;

          end;

            suppose (( Lin (IV \ {wv})) /\ ( Lin {v})) <> ( (0). V);

            hence thesis by B1, B2, B13;

          end;

        end;

        

         B16: ((( Lin (IV \ {wv})) + ( Lin {v})) + ( Lin {wv})) is free

        proof

          per cases ;

            suppose ((( Lin (IV \ {wv})) + ( Lin {v})) /\ ( Lin {wv})) = ( (0). V);

            hence thesis by B15, ZMODUL04: 31;

          end;

            suppose

             C1: ((( Lin (IV \ {wv})) + ( Lin {v})) /\ ( Lin {wv})) <> ( (0). V);

            I is linearly-independent by VECTSP_7:def 3;

            then {w} is linearly-independent by B4, ZFMISC_1: 31, ZMODUL02: 56;

            then {wv} is linearly-independent by ZMODUL03: 15;

            then

             C3: wv <> ( 0. V);

            per cases ;

              suppose (( Lin {v}) /\ ( Lin {wv})) <> ( (0). V);

              then

              consider wx be Vector of V such that

               D1: wx <> ( 0. V) & (( Lin {v}) + ( Lin {wv})) = ( Lin {wx}) by B2, C3, LmSumMod2;

              (( Lin (IV \ {wv})) + ( Lin {wx})) is free

              proof

                per cases ;

                  suppose (( Lin (IV \ {wv})) /\ ( Lin {wx})) = ( (0). V);

                  hence thesis by B9, ZMODUL04: 31;

                end;

                  suppose (( Lin (IV \ {wv})) /\ ( Lin {wx})) <> ( (0). V);

                  hence thesis by B1, B13, D1;

                end;

              end;

              hence thesis by D1, ZMODUL01: 96;

            end;

              suppose (( Lin {v}) /\ ( Lin {wv})) = ( (0). V);

              then

              consider w1,w2 be Vector of V such that

               D2: w1 <> ( 0. V) & w2 <> ( 0. V) & ((LinIw + ( Lin {v})) + ( Lin {wv})) = ((LinIw + ( Lin {w1})) + ( Lin {w2})) & (LinIw /\ ( Lin {w1})) <> ( (0). V) & ((LinIw + ( Lin {w1})) /\ ( Lin {w2})) = ( (0). V) & v in (( Lin {w1}) + ( Lin {w2})) & wv in (( Lin {w1}) + ( Lin {w2})) & w1 in (( Lin {v}) + ( Lin {wv})) & w2 in (( Lin {v}) + ( Lin {wv})) by B2, B8, C1, C3, LmSumMod3;

              (( Lin (IV \ {wv})) + ( Lin {w1})) is free by B1, B13, D2;

              hence thesis by D2, ZMODUL04: 31;

            end;

          end;

        end;

        

         B17: ( (Omega). W) = (( Lin (IV \ {wv})) + ( Lin {wv}))

        proof

          for x be object holds x in ( (Omega). W) iff x in (( Lin (IV \ {wv})) + ( Lin {wv}))

          proof

            let x be object;

            hereby

              assume x in ( (Omega). W);

              then

              consider xx1,xx2 be Vector of W such that

               C2: xx1 in ( Lin (I \ {w})) & xx2 in ( Lin {w}) & x = (xx1 + xx2) by ZMODUL01: 92, B5;

              reconsider x1 = xx1, x2 = xx2 as Vector of V by ZMODUL01: 25;

              

               C3: x1 in ( Lin (IV \ {wv})) & x2 in ( Lin {wv}) by C2, ZMODUL03: 20;

              x = (x1 + x2) by C2, ZMODUL01: 28;

              hence x in (( Lin (IV \ {wv})) + ( Lin {wv})) by C3, ZMODUL01: 92;

            end;

            assume x in (( Lin (IV \ {wv})) + ( Lin {wv}));

            then

            consider x1,x2 be Vector of V such that

             C2: x1 in ( Lin (IV \ {wv})) & x2 in ( Lin {wv}) & x = (x1 + x2) by ZMODUL01: 92;

            

             C3: x1 in ( Lin (I \ {w})) & x2 in ( Lin {w}) by C2, ZMODUL03: 20;

            ( Lin (I \ {w})) is Subspace of (( Lin (I \ {w})) + ( Lin {w})) by ZMODUL01: 97;

            then

             C4: x1 in (( Lin (I \ {w})) + ( Lin {w})) by C3, ZMODUL01: 24;

            ( Lin {w}) is Subspace of (( Lin (I \ {w})) + ( Lin {w})) by ZMODUL01: 97;

            then x2 in (( Lin (I \ {w})) + ( Lin {w})) by C3, ZMODUL01: 24;

            then

            reconsider xx1 = x1, xx2 = x2 as Vector of W by B5, C4;

            x = (xx1 + xx2) by C2, ZMODUL01: 28;

            hence x in ( (Omega). W);

          end;

          then

           CX1: for x be Vector of V holds x in ( (Omega). W) iff x in (( Lin (IV \ {wv})) + ( Lin {wv}));

          reconsider Wo = ( (Omega). W) as Subspace of V by ZMODUL01: 42;

          Wo = (( Lin (IV \ {wv})) + ( Lin {wv})) by CX1, ZMODUL01: 46;

          hence thesis;

        end;

        reconsider Ws = ( (Omega). W) as strict Subspace of V by ZMODUL01: 42;

        reconsider Linvs = ( (Omega). ( Lin {v})) as strict Subspace of V;

        ((( Lin (IV \ {wv})) + ( Lin {v})) + ( Lin {wv})) = (Ws + Linvs) by B17, ZMODUL01: 96

        .= (W + ( Lin {v})) by ZMODUL04: 22;

        hence thesis by B16;

      end;

      

       A3: for n be Nat holds P[n] from NAT_1:sch 2( A1, A2);

      let W be finite-rank free Subspace of V, v be Vector of V such that

       A4: v <> ( 0. V) & (W /\ ( Lin {v})) <> ( (0). V);

      set rk = ( rank W);

      (rk - 1) is Nat

      proof

        assume not (rk - 1) is Nat;

        then rk = 0 ;

        

        then

         B1: ( (Omega). W) = ( (0). W) by ZMODUL05: 1

        .= ( (0). V) by ZMODUL01: 51;

        ( (Omega). ( Lin {v})) = ( Lin {v});

        

        then (W /\ ( Lin {v})) = (( (0). V) /\ ( Lin {v})) by B1, ZMODUL04: 23

        .= ( (0). V) by ZMODUL01: 107;

        hence contradiction by A4;

      end;

      then

      reconsider rk1 = (rk - 1) as Nat;

       P[rk1] by A3;

      hence thesis by A4;

    end;

    registration

      let V be torsion-free Z_Module;

      let v be Vector of V;

      let W be finite-rank free Subspace of V;

      cluster (W + ( Lin {v})) -> free;

      coherence

      proof

        per cases ;

          suppose

           B1: v = ( 0. V);

          reconsider Ws = ( (Omega). W) as strict Subspace of V by ZMODUL01: 42;

          reconsider Lw = ( (Omega). ( Lin {v})) as strict Subspace of V;

          (W + ( Lin {v})) = (Ws + Lw) by ZMODUL04: 22

          .= (Ws + ( (0). V)) by B1, ThLin5

          .= Ws by ZMODUL01: 99;

          hence thesis;

        end;

          suppose

           A1: v <> ( 0. V);

          per cases ;

            suppose (W /\ ( Lin {v})) = ( (0). V);

            hence thesis by ZMODUL04: 31;

          end;

            suppose (W /\ ( Lin {v})) <> ( (0). V);

            hence thesis by A1, LmSumModX;

          end;

        end;

      end;

    end

    registration

      let V be Z_Module;

      let v be Vector of V;

      let W be finitely-generated Subspace of V;

      cluster (W + ( Lin {v})) -> finitely-generated;

      coherence

      proof

        consider A be finite Subset of W such that

         A1: ( (Omega). W) = ( Lin A) by ZMODUL03:def 4;

        A c= the carrier of W & the carrier of W c= the carrier of V by VECTSP_4:def 2;

        then

        reconsider A as finite Subset of V by XBOOLE_1: 1;

        reconsider Ws = ( (Omega). W) as strict Subspace of V by ZMODUL01: 42;

        reconsider Lv = ( (Omega). ( Lin {v})) as strict Subspace of V;

        (Ws + Lv) = (( Lin A) + ( Lin {v})) by A1, ZMODUL03: 20

        .= ( Lin (A \/ {v})) by ZMODUL02: 72;

        hence thesis by ZMODUL04: 22;

      end;

    end

    registration

      let V be Z_Module;

      let W1,W2 be finitely-generated Subspace of V;

      cluster (W1 + W2) -> finitely-generated;

      coherence

      proof

        consider A1 be finite Subset of W1 such that

         A1: ( (Omega). W1) = ( Lin A1) by ZMODUL03:def 4;

        A1 c= the carrier of W1 & the carrier of W1 c= the carrier of V by VECTSP_4:def 2;

        then

        reconsider A1 as finite Subset of V by XBOOLE_1: 1;

        consider A2 be finite Subset of W2 such that

         A2: ( (Omega). W2) = ( Lin A2) by ZMODUL03:def 4;

        A2 c= the carrier of W2 & the carrier of W2 c= the carrier of V by VECTSP_4:def 2;

        then

        reconsider A2 as finite Subset of V by XBOOLE_1: 1;

        reconsider W1s = ( (Omega). W1), W2s = ( (Omega). W2) as strict Subspace of V by ZMODUL01: 42;

        

         A3: W1s = ( Lin A1) by A1, ZMODUL03: 20;

        (W1 + W2) = (W1s + W2s) by ZMODUL04: 22

        .= (( Lin A1) + ( Lin A2)) by A2, ZMODUL03: 20, A3

        .= ( Lin (A1 \/ A2)) by ZMODUL02: 72;

        hence thesis;

      end;

    end

    theorem :: ZMODUL06:31

    

     LMThSumMod2: for R be Ring holds for V be LeftMod of R, W be Subspace of V, W1s,W2s be Subspace of W, W1,W2 be Subspace of V st W1s = W1 & W2s = W2 holds (W1s + W2s) = (W1 + W2)

    proof

      let R be Ring;

      let V be LeftMod of R, W be Subspace of V, W1s,W2s be Subspace of W, W1,W2 be Subspace of V;

      assume

       AS: W1s = W1 & W2s = W2;

      reconsider SWs12 = (W1s + W2s) as strict Subspace of V by VECTSP_4: 26;

      for v be Vector of V holds v in SWs12 iff v in (W1 + W2)

      proof

        let v be Vector of V;

        hereby

          assume v in SWs12;

          then

          consider x1,x2 be Vector of W such that

           B1: x1 in W1s & x2 in W2s & v = (x1 + x2) by VECTSP_5: 1;

          the carrier of W1 c= the carrier of V by VECTSP_4:def 2;

          then

          reconsider xx1 = x1 as Vector of V by AS, B1;

          the carrier of W2 c= the carrier of V by VECTSP_4:def 2;

          then

          reconsider xx2 = x2 as Vector of V by AS, B1;

          v = (xx1 + xx2) by VECTSP_4: 13, B1;

          hence v in (W1 + W2) by VECTSP_5: 1, AS, B1;

        end;

        assume v in (W1 + W2);

        then

        consider x1,x2 be Vector of V such that

         B1: x1 in W1 & x2 in W2 & v = (x1 + x2) by VECTSP_5: 1;

        the carrier of W1s c= the carrier of W by VECTSP_4:def 2;

        then

        reconsider xx1 = x1 as Vector of W by AS, B1;

        the carrier of W2s c= the carrier of W by VECTSP_4:def 2;

        then

        reconsider xx2 = x2 as Vector of W by AS, B1;

        v = (xx1 + xx2) by VECTSP_4: 13, B1;

        hence v in SWs12 by AS, B1, VECTSP_5: 1;

      end;

      hence thesis by VECTSP_4: 30;

    end;

    registration

      let V be torsion-free Z_Module;

      let U1,U2 be finite-rank free Subspace of V;

      cluster (U1 + U2) -> free;

      correctness

      proof

        defpred P[ Nat] means for W1,W2 be finite-rank free Subspace of V st ( rank W1) = $1 holds (W1 + W2) is finite-rank free Subspace of V;

        

         A1: P[ 0 ]

        proof

          let W1,W2 be finite-rank free Subspace of V such that

           C2: ( rank W1) = 0 ;

          reconsider W2s = ( (Omega). W2) as strict Subspace of V by ZMODUL01: 42;

          ( (Omega). W1) = ( (0). W1) by C2, ZMODUL05: 1

          .= ( (0). V) by ZMODUL01: 51;

          

          then (W1 + W2) = (( (0). V) + W2s) by ZMODUL04: 22

          .= ( (Omega). W2) by ZMODUL01: 99;

          hence thesis;

        end;

        

         A2: for n be Nat st P[n] holds P[(n + 1)]

        proof

          let n be Nat;

          assume

           A21: P[n];

          let W1,W2 be finite-rank free Subspace of V;

          assume

           A22: ( rank W1) = (n + 1);

          reconsider W1s = ( (Omega). W1) as strict Subspace of V by ZMODUL01: 42;

          reconsider W2s = ( (Omega). W2) as strict Subspace of V by ZMODUL01: 42;

          consider I be finite Subset of W1 such that

           C30: I is Basis of W1 by ZMODUL03:def 3;

          reconsider I as Basis of W1 by C30;

          

           C31: ( card I) <> 0 & ( card I) = (n + 1) by A22, ZMODUL03:def 5;

          then I <> {} ;

          then

          consider u be object such that

           C32: u in I by XBOOLE_0: 7;

          reconsider u0 = u as Vector of W1 by C32;

          I c= the carrier of W1 & the carrier of W1 c= the carrier of V by VECTSP_4:def 2;

          then

          reconsider u as Vector of V by C32;

          

           D33: (I \ {u}) c= I & I c= the carrier of W1 by XBOOLE_1: 36;

          reconsider J = (I \ {u}) as finite Subset of W1;

          (( card I) - ( card {u})) = ((n + 1) - 1) by C31, CARD_1: 30;

          then

           C34: ( card J) = n by C32, ZFMISC_1: 31, CARD_2: 44;

          

           D34: J is linearly-independent by D33, VECTSP_7:def 3, ZMODUL02: 56;

          reconsider W10 = ( Lin J) as finite-rank free Subspace of V by ZMODUL01: 42;

          reconsider W10s = ( (Omega). W10) as strict Subspace of V;

          for x be object st x in J holds x in the carrier of W10

          proof

            let x be object;

            assume x in J;

            then x in ( Lin J) by ZMODUL02: 65;

            hence x in the carrier of W10;

          end;

          then J c= the carrier of W10;

          then

          reconsider J0 = J as linearly-independent Subset of W10 by D34, ZMODUL03: 16;

          W10s = ( Lin J0) & ( Lin J0) = ( Lin J) by ZMODUL03: 20;

          then J0 is Basis of W10 by VECTSP_7:def 3;

          then ( rank W10) = n by C34, ZMODUL03:def 5;

          then

          reconsider W3 = (W10 + W2) as finite-rank free Subspace of V by A21;

          

           R2: ( Lin {u0}) = ( Lin {u}) by ZMODUL03: 20;

          W1 is_the_direct_sum_of (( Lin J),( Lin {u0})) by C32, ZMODUL04: 33;

          then

           Q2: W1s = (W10s + ( Lin {u})) by LMThSumMod2, R2;

          (W1 + W2) = (W1s + W2s) by ZMODUL04: 22

          .= (( Lin {u}) + (W10s + W2s)) by ZMODUL01: 96, Q2

          .= (( Lin {u}) + W3) by ZMODUL04: 22;

          hence thesis;

        end;

        

         A3: for n be Nat holds P[n] from NAT_1:sch 2( A1, A2);

        set rk = ( rank U1);

         P[rk] by A3;

        hence thesis;

      end;

    end

    registration

      cluster -> free for finitely-generated torsion-free Z_Module;

      correctness

      proof

        let V be finitely-generated torsion-free Z_Module;

        consider A be finite Subset of V such that

         A2: ( Lin A) = ( (Omega). V) by ZMODUL03:def 4;

        

         A3: ( Lin (A \ {( 0. V)})) is free

        proof

          defpred P[ Nat] means for B be finite Subset of V st ( card (B \ {( 0. V)})) = $1 holds ( Lin (B \ {( 0. V)})) is free;

          

           B2: P[ 0 ]

          proof

            let B be finite Subset of V such that

             C1: ( card (B \ {( 0. V)})) = 0 ;

            (B \ {( 0. V)}) = ( {} the carrier of V) by C1;

            hence thesis;

          end;

          

           B3: for n be Nat st P[n] holds P[(n + 1)]

          proof

            let n be Nat such that

             C1: P[n];

            let B be finite Subset of V such that

             C2: ( card (B \ {( 0. V)})) = (n + 1);

            (B \ {( 0. V)}) <> {} by C2;

            then

            consider u be object such that

             C3: u in (B \ {( 0. V)}) by XBOOLE_0: 7;

            reconsider u as Vector of V by C3;

            

             C4: ( card ((B \ {( 0. V)}) \ {u})) = (( card (B \ {( 0. V)})) - ( card {u})) by C3, ZFMISC_1: 31, CARD_2: 44

            .= ((n + 1) - 1) by C2, CARD_1: 30

            .= n;

            ((B \ {( 0. V)}) \ {u}) = (B \ ( {( 0. V)} \/ {u})) by XBOOLE_1: 41

            .= ((B \ {u}) \ {( 0. V)}) by XBOOLE_1: 41;

            then

             C5: ( Lin ((B \ {( 0. V)}) \ {u})) is free by C1, C4;

            (( Lin ((B \ {( 0. V)}) \ {u})) + ( Lin {u})) = ( Lin (((B \ {( 0. V)}) \ {u}) \/ {u})) by ZMODUL02: 72

            .= ( Lin ((B \ {( 0. V)}) \/ {u})) by XBOOLE_1: 39

            .= ( Lin (B \ {( 0. V)})) by C3, ZFMISC_1: 40;

            hence thesis by C5;

          end;

          

           B4: for n be Nat holds P[n] from NAT_1:sch 2( B2, B3);

          set n = ( card (A \ {( 0. V)}));

           P[n] by B4;

          hence thesis;

        end;

        per cases ;

          suppose

           B1: ( 0. V) in A;

          

           B2: ( Lin {( 0. V)}) = ( (0). V) by ThLin5;

          V is_the_direct_sum_of (( Lin (A \ {( 0. V)})),( Lin {( 0. V)}))

          proof

            (( Lin (A \ {( 0. V)})) + ( Lin {( 0. V)})) = ( Lin ((A \ {( 0. V)}) \/ {( 0. V)})) by ZMODUL02: 72

            .= ( Lin (A \/ {( 0. V)})) by XBOOLE_1: 39

            .= ( Lin A) by B1, ZFMISC_1: 40;

            hence thesis by A2, B2, ZMODUL01: 107;

          end;

          hence thesis by A3, ZMODUL04: 30;

        end;

          suppose not ( 0. V) in A;

          then ( Lin A) is free by A3, ZFMISC_1: 57;

          hence thesis by A2, ZMODUL04: 21;

        end;

      end;

    end

    begin

    theorem :: ZMODUL06:32

    

     ThRankDirectSum: for V be torsion-free Z_Module, W1,W2 be finite-rank free Subspace of V st (W1 /\ W2) = ( (0). V) holds ( rank (W1 + W2)) = (( rank W1) + ( rank W2))

    proof

      let V be torsion-free Z_Module, W1,W2 be finite-rank free Subspace of V such that

       A1: (W1 /\ W2) = ( (0). V);

      set W = (W1 + W2);

      reconsider WW1 = W1, WW2 = W2 as Subspace of W by ZMODUL01: 97;

      (WW1 /\ WW2) = ( (0). V) by A1, ZMODUL04: 2

      .= ( (0). W) by ZMODUL01: 51;

      then

       A3: W is_the_direct_sum_of (WW1,WW2) by ZMODUL04: 1;

      reconsider WW1, WW2 as finite-rank free Subspace of W;

      set I1 = the Basis of WW1;

      set I2 = the Basis of WW2;

      

       A4: ( card I1) = ( rank WW1) by ZMODUL03:def 5;

      (I1 /\ I2) = {} by A3, ZMODUL04: 27;

      

      then

       A7: ( card (I1 \/ I2)) = (( card I1) + ( card I2)) by CARD_2: 40, XBOOLE_0:def 7

      .= (( rank WW1) + ( rank WW2)) by ZMODUL03:def 5, A4;

      set I = (I1 \/ I2);

      the carrier of WW1 c= the carrier of W by VECTSP_4:def 2;

      then

       A11: I1 is Subset of W by XBOOLE_1: 1;

      the carrier of WW2 c= the carrier of W by VECTSP_4:def 2;

      then I2 is Subset of W by XBOOLE_1: 1;

      then

      reconsider I as Subset of W by A11, XBOOLE_1: 8;

      ( Lin I) = ( (Omega). W) by A3, ZMODUL04: 28;

      then (I1 \/ I2) is Basis of W by VECTSP_7:def 3, A3, ZMODUL04: 29;

      hence thesis by A7, ZMODUL03:def 5;

    end;

    theorem :: ZMODUL06:33

    for V be finite-rank free Z_Module, W1,W2 be finite-rank free Subspace of V st V is_the_direct_sum_of (W1,W2) holds ( rank V) = (( rank W1) + ( rank W2))

    proof

      let V be finite-rank free Z_Module, W1,W2 be finite-rank free Subspace of V such that

       A1: V is_the_direct_sum_of (W1,W2);

      ( rank ( (Omega). V)) = (( rank W1) + ( rank W2)) by ThRankDirectSum, A1;

      hence thesis by ZMODUL05: 4;

    end;

    theorem :: ZMODUL06:34

    

     ThISRank1: for V be torsion-free Z_Module, W1,W2 be finite-rank free Subspace of V holds ( rank (W1 /\ W2)) <= ( rank W1)

    proof

      let V be torsion-free Z_Module, W1,W2 be finite-rank free Subspace of V;

      (W1 /\ W2) is Subspace of W1 by ZMODUL01: 105;

      hence thesis by ZMODUL05: 2;

    end;

    theorem :: ZMODUL06:35

    

     LmRank0a: for V be torsion-free Z_Module, v be Vector of V st v <> ( 0. V) holds ( rank ( Lin {v})) = 1

    proof

      let V be torsion-free Z_Module, v be Vector of V such that

       A1: v <> ( 0. V);

      v in ( Lin {v}) by ZMODUL02: 65, ZFMISC_1: 31;

      then

      reconsider vv = v as Vector of ( Lin {v});

      

       A2: vv <> ( 0. ( Lin {v})) by A1, ZMODUL01: 26;

      ( (Omega). ( Lin {v})) = ( Lin {vv}) by ZMODUL03: 20;

      hence thesis by A2, ZMODUL05: 5;

    end;

    theorem :: ZMODUL06:36

    for V be Z_Module holds ( rank ( (0). V)) = 0

    proof

      let V be Z_Module;

      reconsider 0Vs = ( (Omega). ( (0). V)) as strict finite-rank free Z_Module;

      ( (Omega). 0Vs) = ( (0). ( (0). V)) by ZMODUL01: 51;

      hence thesis by ZMODUL05: 1;

    end;

    theorem :: ZMODUL06:37

    

     LmRank1: for V be torsion-free Z_Module, v,u be Vector of V st v <> ( 0. V) & u <> ( 0. V) & (( Lin {v}) /\ ( Lin {u})) <> ( (0). V) holds ( rank (( Lin {v}) + ( Lin {u}))) = 1

    proof

      let V be torsion-free Z_Module, v,u be Vector of V such that

       A1: v <> ( 0. V) & u <> ( 0. V) & (( Lin {v}) /\ ( Lin {u})) <> ( (0). V);

      consider w be Vector of V such that

       A2: w <> ( 0. V) & (( Lin {v}) + ( Lin {u})) = ( Lin {w}) by A1, LmSumMod2;

      w in ( Lin {w}) by ZMODUL02: 65, ZFMISC_1: 31;

      then

      reconsider ww = w as Vector of ( Lin {w});

      

       A3: ww <> ( 0. ( Lin {w})) by A2, ZMODUL01: 26;

      ( (Omega). ( Lin {w})) = ( Lin {ww}) by ZMODUL03: 20;

      hence thesis by A2, A3, ZMODUL05: 5;

    end;

    theorem :: ZMODUL06:38

    

     LmRank2: for V be torsion-free Z_Module, W be finite-rank free Subspace of V, v be Vector of V st v <> ( 0. V) & (W /\ ( Lin {v})) <> ( (0). V) holds ( rank (W + ( Lin {v}))) = ( rank W)

    proof

      let V be torsion-free Z_Module;

      defpred P[ Nat] means for W be finite-rank free Subspace of V, v be Vector of V st v <> ( 0. V) & (W /\ ( Lin {v})) <> ( (0). V) & ( rank W) = ($1 + 1) holds ( rank (W + ( Lin {v}))) = ( rank W);

      

       A1: P[ 0 ]

      proof

        let W be finite-rank free Subspace of V, v be Vector of V such that

         B1: v <> ( 0. V) & (W /\ ( Lin {v})) <> ( (0). V) & ( rank W) = ( 0 + 1);

        consider uu be Vector of W such that

         B3: uu <> ( 0. W) & ( (Omega). W) = ( Lin {uu}) by B1, ZMODUL05: 5;

        reconsider u = uu as Vector of V by ZMODUL01: 25;

        

         B4: u <> ( 0. V) by ZMODUL01: 26, B3;

        reconsider Ws = ( (Omega). W) as strict Subspace of V by ZMODUL01: 42;

        reconsider Lv = ( (Omega). ( Lin {v})) as strict Subspace of V;

        

         B6: (( Lin {u}) + ( Lin {v})) = (Ws + Lv) by B3, ZMODUL03: 20

        .= (W + ( Lin {v})) by ZMODUL04: 22;

        (( Lin {u}) /\ ( Lin {v})) = (Ws /\ Lv) by B3, ZMODUL03: 20

        .= (W /\ ( Lin {v})) by ZMODUL04: 23;

        hence ( rank (W + ( Lin {v}))) = ( rank W) by B6, B1, B4, LmRank1;

      end;

      

       A2: for n be Nat st P[n] holds P[(n + 1)]

      proof

        let n be Nat such that

         B1: P[n];

        let W be finite-rank free Subspace of V, v be Vector of V such that

         B2: v <> ( 0. V) & (W /\ ( Lin {v})) <> ( (0). V) & ( rank W) = ((n + 1) + 1);

        consider I be finite Subset of V such that

         B3: I is finite Subset of W & I is linearly-independent & ( Lin I) = ( (Omega). W) & ( card I) = ( rank W) by LmFree2;

        I <> ( {} the carrier of W) by B2, B3;

        then

        consider w be object such that

         B5: w in I by XBOOLE_0: 7;

        reconsider w as Vector of V by B5;

        

         B6: ( (Omega). W) = (( Lin (I \ {w})) + ( Lin {w})) & (( Lin (I \ {w})) /\ ( Lin {w})) = ( (0). V) & ( Lin (I \ {w})) is free & ( Lin {w}) is free & w <> ( 0. V) by B3, B5, ThLin8;

        reconsider LIw = ( Lin (I \ {w})), Lw = ( Lin {w}) as finite-rank free Subspace of V;

        

         B7: ( card (I \ {w})) = (( card I) - ( card {w})) by B5, ZFMISC_1: 31, CARD_2: 44

        .= ((n + 2) - 1) by CARD_1: 30, B2, B3

        .= (n + 1);

        reconsider Lv = ( Lin {v}) as finite-rank free Subspace of V;

        (I \ {w}) is linearly-independent by B3, ZMODUL02: 56, XBOOLE_1: 36;

        then

        reconsider Iw = (I \ {w}) as Basis of ( Lin (I \ {w})) by ThLin7;

        

         B10: ( rank ( Lin (I \ {w}))) = ( card Iw) by ZMODUL03:def 5

        .= (n + 1) by B7;

        per cases ;

          suppose

           C1: ((( Lin (I \ {w})) + ( Lin {v})) /\ ( Lin {w})) = ( (0). V);

          then

           C2: ( rank ((( Lin (I \ {w})) + ( Lin {v})) + ( Lin {w}))) = (( rank (( Lin (I \ {w})) + ( Lin {v}))) + ( rank ( Lin {w}))) by ThRankDirectSum;

          

           C3: (( Lin (I \ {w})) /\ ( Lin {v})) <> ( (0). V)

          proof

            assume

             D1: (( Lin (I \ {w})) /\ ( Lin {v})) = ( (0). V);

            consider x be Vector of V such that

             D2: x in (W /\ ( Lin {v})) & x <> ( 0. V) by B2, ZMODUL04: 24;

            x in W by D2, ZMODUL01: 94;

            then x in ( (Omega). W);

            then

            consider x1,x2 be Vector of V such that

             D3: x1 in ( Lin (I \ {w})) & x2 in ( Lin {w}) & x = (x1 + x2) by B6, ZMODUL01: 92;

            

             D4: x in ( Lin {v}) by D2, ZMODUL01: 94;

            

             D5: (x - x1) = (x2 + (x1 - x1)) by RLVECT_1: 28, D3

            .= (x2 + ( 0. V)) by RLVECT_1: 15

            .= x2;

            ( - x1) in ( Lin (I \ {w})) by D3, ZMODUL01: 38;

            then

             D6: x2 in (( Lin (I \ {w})) + ( Lin {v})) by D4, D5, ZMODUL01: 92;

            x2 <> ( 0. V) by D1, D2, ZMODUL02: 66, D4, ZMODUL01: 94, D3;

            hence contradiction by C1, D6, ZMODUL02: 66, D3, ZMODUL01: 94;

          end;

          

           C4: ( rank (LIw + ( Lin {v}))) = (n + 1) by B10, B1, B2, C3;

          

           C5: ( rank ((LIw + ( Lin {v})) + ( Lin {w}))) = ((n + 1) + 1) by C2, C4, B6, LmRank0a

          .= (n + 2);

          ( (Omega). ( Lin {v})) = ( Lin {v});

          

          then (W + ( Lin {v})) = ((( Lin (I \ {w})) + ( Lin {w})) + ( Lin {v})) by B6, ZMODUL04: 22

          .= ((( Lin (I \ {w})) + ( Lin {v})) + ( Lin {w})) by ZMODUL01: 96;

          hence thesis by B2, C5;

        end;

          suppose

           C1: ((( Lin (I \ {w})) + ( Lin {v})) /\ ( Lin {w})) <> ( (0). V);

          per cases ;

            suppose (( Lin {v}) /\ ( Lin {w})) = ( (0). V);

            then

            consider w1,w2 be Vector of V such that

             D2: w1 <> ( 0. V) & w2 <> ( 0. V) & ((LIw + ( Lin {v})) + ( Lin {w})) = ((LIw + ( Lin {w1})) + ( Lin {w2})) & (LIw /\ ( Lin {w1})) <> ( (0). V) & ((LIw + ( Lin {w1})) /\ ( Lin {w2})) = ( (0). V) & v in (( Lin {w1}) + ( Lin {w2})) & w in (( Lin {w1}) + ( Lin {w2})) & w1 in (( Lin {v}) + ( Lin {w})) & w2 in (( Lin {v}) + ( Lin {w})) by B2, B6, LmSumMod3, C1;

            ( (Omega). ( Lin {v})) = ( Lin {v});

            

            then

             D3: (W + ( Lin {v})) = ((( Lin (I \ {w})) + ( Lin {w})) + ( Lin {v})) by B6, ZMODUL04: 22

            .= ((( Lin (I \ {w})) + ( Lin {w1})) + ( Lin {w2})) by D2, ZMODUL01: 96;

            

             D4: ( rank (LIw + ( Lin {w1}))) = (n + 1) by B10, B1, D2;

            ( rank (W + ( Lin {v}))) = (( rank (( Lin (I \ {w})) + ( Lin {w1}))) + ( rank ( Lin {w2}))) by D3, D2, ThRankDirectSum

            .= ((n + 1) + 1) by D4, D2, LmRank0a

            .= (n + 2);

            hence thesis by B2;

          end;

            suppose

             D1: (( Lin {v}) /\ ( Lin {w})) <> ( (0). V);

            consider u be Vector of V such that

             D2: u <> ( 0. V) & (( Lin {v}) + ( Lin {w})) = ( Lin {u}) by B2, B6, D1, LmSumMod2;

            ( (Omega). ( Lin {v})) = ( Lin {v});

            

            then

             D3: (W + ( Lin {v})) = ((( Lin (I \ {w})) + ( Lin {w})) + ( Lin {v})) by B6, ZMODUL04: 22

            .= (( Lin (I \ {w})) + ( Lin {u})) by D2, ZMODUL01: 96;

            (( Lin (I \ {w})) /\ ( Lin {u})) = ( (0). V)

            proof

              assume (( Lin (I \ {w})) /\ ( Lin {u})) <> ( (0). V);

              then

              consider x be Vector of V such that

               E2: x in (( Lin (I \ {w})) /\ ( Lin {u})) & x <> ( 0. V) by ZMODUL04: 24;

              x in ( Lin {u}) by E2, ZMODUL01: 94;

              then

              consider iux be Element of INT.Ring such that

               E3: x = (iux * u) by ThLin1;

              w in ( Lin {w}) by ZMODUL02: 65, ZFMISC_1: 31;

              then w in ( Lin {u}) by D2, ZMODUL01: 93;

              then

              consider iuw be Element of INT.Ring such that

               E4: w = (iuw * u) by ThLin1;

              

               E5: (iux * w) in ( Lin {w}) by ZMODUL01: 37, ThLin2;

              (iux * w) = ((iux * iuw) * u) by VECTSP_1:def 16, E4

              .= (iuw * x) by E3, VECTSP_1:def 16;

              then (iux * w) in (( Lin (I \ {w})) /\ ( Lin {u})) by E2, ZMODUL01: 37;

              then (iux * w) in ( Lin (I \ {w})) by ZMODUL01: 94;

              then

               E6: (iux * w) in (( Lin (I \ {w})) /\ ( Lin {w})) by E5, ZMODUL01: 94;

              iux <> ( 0. INT.Ring ) by E2, E3, ZMODUL01: 1;

              hence contradiction by E6, ZMODUL02: 66, B6, ZMODUL01:def 7;

            end;

            

            then ( rank (LIw + ( Lin {u}))) = (( rank LIw) + ( rank ( Lin {u}))) by ThRankDirectSum

            .= ((n + 1) + 1) by B10, D2, LmRank0a

            .= (n + 2);

            hence thesis by B2, D3;

          end;

        end;

      end;

      

       A3: for n be Nat holds P[n] from NAT_1:sch 2( A1, A2);

      let W be finite-rank free Subspace of V, v be Vector of V such that

       A4: v <> ( 0. V) & (W /\ ( Lin {v})) <> ( (0). V);

      set rk = ( rank W);

      (rk - 1) is Nat

      proof

        assume not (rk - 1) is Nat;

        then rk = 0 ;

        

        then

         B1: ( (Omega). W) = ( (0). W) by ZMODUL05: 1

        .= ( (0). V) by ZMODUL01: 51;

        ( (Omega). ( Lin {v})) = ( Lin {v});

        

        then (W /\ ( Lin {v})) = (( (0). V) /\ ( Lin {v})) by B1, ZMODUL04: 23

        .= ( (0). V) by ZMODUL01: 107;

        hence contradiction by A4;

      end;

      then

      reconsider rk1 = (rk - 1) as Nat;

       P[rk1] by A3;

      hence thesis by A4;

    end;

    theorem :: ZMODUL06:39

    

     LmISRank21: for V be torsion-free Z_Module, W1,W2 be finite-rank free Subspace of V, v be Vector of V st (W1 /\ ( Lin {v})) <> ( (0). V) & (W2 /\ ( Lin {v})) <> ( (0). V) holds ((W1 /\ W2) /\ ( Lin {v})) <> ( (0). V)

    proof

      let V be torsion-free Z_Module, W1,W2 be finite-rank free Subspace of V, v be Vector of V such that

       A1: (W1 /\ ( Lin {v})) <> ( (0). V) & (W2 /\ ( Lin {v})) <> ( (0). V);

      consider u1 be Vector of V such that

       A2: u1 in (W1 /\ ( Lin {v})) & u1 <> ( 0. V) by A1, ZMODUL04: 24;

      consider u2 be Vector of V such that

       A3: u2 in (W2 /\ ( Lin {v})) & u2 <> ( 0. V) by A1, ZMODUL04: 24;

      

       A6: u1 in ( Lin {v}) by A2, ZMODUL01: 94;

      then

      consider iu1 be Element of INT.Ring such that

       A4: u1 = (iu1 * v) by ThLin1;

      u2 in ( Lin {v}) by A3, ZMODUL01: 94;

      then

      consider iu2 be Element of INT.Ring such that

       A5: u2 = (iu2 * v) by ThLin1;

      

       A7: iu2 <> ( 0. INT.Ring ) by A3, A5, ZMODUL01: 1;

      

       A8: (iu2 * u1) = ((iu2 * iu1) * v) by VECTSP_1:def 16, A4

      .= (iu1 * u2) by A5, VECTSP_1:def 16;

      u1 in W1 by A2, ZMODUL01: 94;

      then

       A9: (iu2 * u1) in W1 by ZMODUL01: 37;

      u2 in W2 by A3, ZMODUL01: 94;

      then (iu2 * u1) in W2 by A8, ZMODUL01: 37;

      then

       A10: (iu2 * u1) in (W1 /\ W2) by A9, ZMODUL01: 94;

      (iu2 * u1) in ( Lin {v}) by A6, ZMODUL01: 37;

      then (iu2 * u1) in ((W1 /\ W2) /\ ( Lin {v})) by A10, ZMODUL01: 94;

      hence thesis by ZMODUL02: 66, A2, A7, ZMODUL01:def 7;

    end;

    theorem :: ZMODUL06:40

    

     ThTF3C: for R be Ring holds for V,W be LeftMod of R, T be linear-transformation of V, W, A be Subset of V holds (T .: the carrier of ( Lin A)) c= the carrier of ( Lin (T .: A))

    proof

      let R be Ring;

      let V,W be LeftMod of R, T be linear-transformation of V, W, A be Subset of V;

      for y be object st y in (T .: the carrier of ( Lin A)) holds y in the carrier of ( Lin (T .: A))

      proof

        let y be object;

        assume y in (T .: the carrier of ( Lin A));

        then

        consider x be Element of V such that

         A2: x in the carrier of ( Lin A) & y = (T . x) by FUNCT_2: 65;

        x in ( Lin A) by A2;

        then

        consider l be Linear_Combination of A such that

         A3: x = ( Sum l) by MOD_3: 4;

        reconsider l as Linear_Combination of V;

        reconsider Tl = (T @* l) as Linear_Combination of (T .: ( Carrier l)) by ZMODUL05: 44;

        ( Sum Tl) = (T . ( Sum l)) by ZMODUL05: 46;

        then

         A5: y in ( Lin (T .: ( Carrier l))) by A2, A3, MOD_3: 4;

        (T .: ( Carrier l)) c= (T .: A) by RELAT_1: 123, VECTSP_6:def 4;

        then ( Lin (T .: ( Carrier l))) is Subspace of ( Lin (T .: A)) by MOD_3: 10;

        then the carrier of ( Lin (T .: ( Carrier l))) c= the carrier of ( Lin (T .: A)) by VECTSP_4:def 2;

        hence y in the carrier of ( Lin (T .: A)) by A5;

      end;

      hence thesis;

    end;

    theorem :: ZMODUL06:41

    

     HM0: for R be Ring holds for X,Y be LeftMod of R, L be linear-transformation of X, Y holds (L . ( 0. X)) = ( 0. Y)

    proof

      let R be Ring;

      let X,Y be LeftMod of R, L be linear-transformation of X, Y;

      

      thus (L . ( 0. X)) = (L . (( 0. R) * ( 0. X))) by VECTSP_1: 14

      .= (( 0. R) * (L . ( 0. X))) by MOD_2:def 2

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

    end;

    theorem :: ZMODUL06:42

    

     HM1: for R be Ring holds for X,Y be LeftMod of R, L be linear-transformation of X, Y st L is bijective holds ex K be linear-transformation of Y, X st K = (L " ) & K is bijective

    proof

      let R be Ring;

      let X,Y be LeftMod of R, L be linear-transformation of X, Y;

      assume

       A1: L is bijective;

      then

       P2: ( rng L) = the carrier of Y by FUNCT_2:def 3;

      then

      reconsider K = (L " ) as Function of Y, X by A1, FUNCT_2: 25;

      

       D0: ( dom L) = the carrier of X by FUNCT_2:def 1;

      

       B0: K is additive

      proof

        let x,y be Element of Y;

        consider a be Element of X such that

         B01: x = (L . a) by P2, FUNCT_2: 113;

        consider b be Element of X such that

         B02: y = (L . b) by P2, FUNCT_2: 113;

        

         B03: (K . x) = a by A1, FUNCT_1: 34, D0, B01;

        

         B04: (K . y) = b by A1, FUNCT_1: 34, D0, B02;

        (x + y) = (L . (a + b)) by VECTSP_1:def 20, B01, B02;

        hence (K . (x + y)) = ((K . x) + (K . y)) by B03, B04, A1, FUNCT_1: 34, D0;

      end;

      for r be Element of R, x be Element of Y holds (K . (r * x)) = (r * (K . x))

      proof

        let r be Element of R, x be Element of Y;

        consider a be Element of X such that

         B01: x = (L . a) by P2, FUNCT_2: 113;

        

         B03: (K . x) = a by A1, FUNCT_1: 34, D0, B01;

        (r * x) = (L . (r * a)) by MOD_2:def 2, B01;

        hence (K . (r * x)) = (r * (K . x)) by B03, A1, FUNCT_1: 34, D0;

      end;

      then

      reconsider K as linear-transformation of Y, X by B0, MOD_2:def 2;

      take K;

      ( rng K) = the carrier of X by D0, FUNCT_1: 33, A1;

      then K is onto by FUNCT_2:def 3;

      hence thesis by A1;

    end;

    theorem :: ZMODUL06:43

    for R be Ring holds for X,Y be LeftMod of R, l be Linear_Combination of X, L be linear-transformation of X, Y st L is bijective holds (L @* l) = (l * (L " ))

    proof

      let R be Ring;

      let X,Y be LeftMod of R, l be Linear_Combination of X, L be linear-transformation of X, Y;

      assume

       A1: L is bijective;

      then

       Q4: ( rng L) = the carrier of Y by FUNCT_2:def 3;

      then

      reconsider K = (L " ) as Function of Y, X by A1, FUNCT_2: 25;

      

       P3: ( dom (l * K)) = the carrier of Y by FUNCT_2:def 1;

      

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

      then

       P4: (L .: ( Carrier l)) = ( Carrier (L @* l)) by ZMODUL05: 56;

      for a be Element of Y holds ((L @* l) . a) = ((l * K) . a)

      proof

        let a be Element of Y;

        per cases ;

          suppose

           X0: not a in ( Carrier (L @* l));

          reconsider v = (K . a) as Element of X;

          

           X4: (L . v) = a by Q4, A1, FUNCT_1: 35;

          

           Y2: not v in ( Carrier l) by X0, X4, FUNCT_2: 35, P4;

          ((l * K) . a) = (l . v) by P3, FUNCT_1: 12

          .= ( 0. R) by Y2;

          hence thesis by X0;

        end;

          suppose a in ( Carrier (L @* l));

          then

          consider v be object such that

           X5: v in ( dom L) & v in ( Carrier l) & a = (L . v) by FUNCT_1:def 6, P4;

          reconsider v as Element of X by X5;

          

           X6: (K . a) = v by A1, FUNCT_1: 34, X5;

          

          thus ((L @* l) . a) = (l . v) by ZMODUL05: 54, X1, X5

          .= ((l * K) . a) by P3, FUNCT_1: 12, X6;

        end;

      end;

      hence thesis by FUNCT_2:def 8;

    end;

    theorem :: ZMODUL06:44

    for R be Ring holds for X,Y be LeftMod of R, X0 be Subset of X, L be linear-transformation of X, Y, l be Linear_Combination of (L .: X0) st X0 = the carrier of X & L is one-to-one holds (L # l) = (l * L)

    proof

      let R be Ring;

      let X,Y be LeftMod of R, X0 be Subset of X, L be linear-transformation of X, Y, l be Linear_Combination of (L .: X0);

      assume that

       A0: X0 = the carrier of X and

       A1: L is one-to-one;

      

       X1: (L | X0) is one-to-one by A1, FUNCT_1: 52;

      

       X3: (X0 ` ) = {} by XBOOLE_1: 37, A0;

      (L # l) = ((l * L) +* ( {} --> ( 0. R))) by X3, X1, ZMODUL05:def 9

      .= (l * L);

      hence thesis;

    end;

    

     HM4: for R be Ring holds for X,Y be LeftMod of R, A be Subset of X, L be linear-transformation of X, Y st L is bijective & A is linearly-independent holds (L .: A) is linearly-independent

    proof

      let R be Ring;

      let X,Y be LeftMod of R, A be Subset of X, L be linear-transformation of X, Y;

      assume that

       AS1: L is bijective and

       AS2: A is linearly-independent;

      consider K be linear-transformation of Y, X such that

       AS3: K = (L " ) & K is bijective by HM1, AS1;

      

       D1: ( dom L) = the carrier of X by FUNCT_2:def 1;

      

       R1: ( rng L) = the carrier of Y by FUNCT_2:def 3, AS1;

      for l be Linear_Combination of (L .: A) st ( Sum l) = ( 0. Y) holds ( Carrier l) = {}

      proof

        let l be Linear_Combination of (L .: A);

        assume

         P0: ( Sum l) = ( 0. Y);

        reconsider m = (K @* l) as Linear_Combination of (K .: ( Carrier l)) by ZMODUL05: 44;

        

         P2: ( Sum m) = (K . ( 0. Y)) by P0, ZMODUL05: 46

        .= ( 0. X) by HM0;

        (K .: ( Carrier l)) c= (K .: (L .: A)) by RELAT_1: 123, VECTSP_6:def 4;

        then

         P4: (K .: ( Carrier l)) c= A by D1, AS1, AS3, FUNCT_1: 107;

        (K | ( Carrier l)) is one-to-one by AS3, FUNCT_1: 52;

        then

         P5: (K .: ( Carrier l)) = ( Carrier (K @* l)) by ZMODUL05: 56;

        then m is Linear_Combination of A by VECTSP_6:def 4, P4;

        

        then

         P6: (L .: (K .: ( Carrier l))) = (L .: {} ) by P5, AS2, P2

        .= {} ;

        (L .: (K .: ( Carrier l))) = (L .: (L " ( Carrier l))) by FUNCT_1: 85, AS1, AS3

        .= ( Carrier l) by R1, FUNCT_1: 77;

        hence ( Carrier l) = {} by P6;

      end;

      hence thesis;

    end;

    theorem :: ZMODUL06:45

    

     HM6: for R be Ring holds for X,Y be LeftMod of R, A be Subset of X, L be linear-transformation of X, Y st L is bijective holds A is linearly-independent iff (L .: A) is linearly-independent

    proof

      let R be Ring;

      let X,Y be LeftMod of R, A be Subset of X, L be linear-transformation of X, Y;

      assume

       AS1: L is bijective;

      

       D1: ( dom L) = the carrier of X by FUNCT_2:def 1;

      consider K be linear-transformation of Y, X such that

       AS3: K = (L " ) & K is bijective by HM1, AS1;

      thus A is linearly-independent implies (L .: A) is linearly-independent by AS1, HM4;

      assume (L .: A) is linearly-independent;

      then (K .: (L .: A)) is linearly-independent by AS3, HM4;

      hence thesis by D1, AS1, AS3, FUNCT_1: 107;

    end;

    theorem :: ZMODUL06:46

    

     HM7: for R be Ring holds for X,Y be LeftMod of R, A be Subset of X, T be linear-transformation of X, Y st T is bijective holds (T .: the carrier of ( Lin A)) = the carrier of ( Lin (T .: A))

    proof

      let R be Ring;

      let X,Y be LeftMod of R, A be Subset of X, T be linear-transformation of X, Y;

      assume

       AS1: T is bijective;

      

       X1: (T .: the carrier of ( Lin A)) c= the carrier of ( Lin (T .: A)) by ThTF3C;

      reconsider B = (T .: A) as Subset of Y;

      

       D1: ( dom T) = the carrier of X by FUNCT_2:def 1;

      

       R1: ( rng T) = the carrier of Y by FUNCT_2:def 3, AS1;

      consider K be linear-transformation of Y, X such that

       AS3: K = (T " ) & K is bijective by HM1, AS1;

      (K .: B) = A by D1, AS1, AS3, FUNCT_1: 107;

      then

       X3: (T .: (K .: the carrier of ( Lin B))) c= (T .: the carrier of ( Lin A)) by RELAT_1: 123, ThTF3C;

      

       X4: the carrier of ( Lin B) c= ( rng T) by R1, VECTSP_4:def 2;

      (T .: (K .: the carrier of ( Lin B))) = (T .: (T " the carrier of ( Lin B))) by FUNCT_1: 85, AS1, AS3

      .= the carrier of ( Lin B) by X4, FUNCT_1: 77;

      hence thesis by X1, XBOOLE_0:def 10, X3;

    end;

    theorem :: ZMODUL06:47

    

     HM8: for R be Ring holds for Y be LeftMod of R, A be Subset of Y holds ( Lin A) is strict Subspace of ( (Omega). Y)

    proof

      let R be Ring;

      let Y be LeftMod of R, A be Subset of Y;

      

       U1: the carrier of ( Lin A) c= the carrier of Y & ( 0. ( Lin A)) = ( 0. Y) & the addF of ( Lin A) = (the addF of Y || the carrier of ( Lin A)) & the lmult of ( Lin A) = (the lmult of Y | [:the carrier of R, the carrier of ( Lin A):]) by VECTSP_4:def 2;

      the carrier of Y = the carrier of ( (Omega). Y) & ( 0. Y) = ( 0. ( (Omega). Y)) & the addF of Y = the addF of ( (Omega). Y) & the lmult of Y = the lmult of ( (Omega). Y);

      hence ( Lin A) is strict Subspace of ( (Omega). Y) by U1, VECTSP_4:def 2;

    end;

    

     HM9: for R be Ring holds for X,Y be LeftMod of R, T be linear-transformation of X, Y st T is bijective holds X is free implies Y is free

    proof

      let R be Ring;

      let X,Y be LeftMod of R, T be linear-transformation of X, Y;

      assume

       AS1: T is bijective;

      

       D1: ( dom T) = the carrier of X by FUNCT_2:def 1;

      

       R1: ( rng T) = the carrier of Y by FUNCT_2:def 3, AS1;

      assume X is free;

      then

      consider A be Subset of X such that

       p1: A is base;

      

       P2: (T .: A) is linearly-independent by HM6, AS1, p1;

      the carrier of ( Lin (T .: A)) = (T .: the carrier of the ModuleStr of X) by p1, AS1, HM7

      .= the carrier of ( (Omega). Y) by D1, R1, RELAT_1: 113;

      

      then ( Lin (T .: A)) = ( (Omega). Y) by VECTSP_4: 29

      .= the ModuleStr of Y;

      then (T .: A) is base by P2;

      hence Y is free;

    end;

    theorem :: ZMODUL06:48

    for R be Ring holds for X,Y be LeftMod of R, T be linear-transformation of X, Y st T is bijective holds X is free iff Y is free

    proof

      let R be Ring;

      let X,Y be LeftMod of R, T be linear-transformation of X, Y;

      assume

       AS1: T is bijective;

      consider K be linear-transformation of Y, X such that

       AS3: K = (T " ) & K is bijective by HM1, AS1;

      thus thesis by HM9, AS1, AS3;

    end;

    

     HM11: for X,Y be free Z_Module, T be linear-transformation of X, Y, A be Subset of X st T is bijective holds A is Basis of X implies (T .: A) is Basis of Y

    proof

      let X,Y be free Z_Module, T be linear-transformation of X, Y, A be Subset of X;

      assume

       AS1: T is bijective;

      assume A is Basis of X;

      then

       P1: A is linearly-independent & ( Lin A) = the ModuleStr of X by VECTSP_7:def 3;

      

       D1: ( dom T) = the carrier of X by FUNCT_2:def 1;

      

       R1: ( rng T) = the carrier of Y by FUNCT_2:def 3, AS1;

      

       P2: (T .: A) is linearly-independent by HM6, AS1, P1;

      

       P6: ( Lin (T .: A)) is strict Subspace of ( (Omega). Y) by HM8;

      the carrier of ( Lin (T .: A)) = (T .: the carrier of the ModuleStr of X) by P1, AS1, HM7

      .= the carrier of ( (Omega). Y) by D1, R1, RELAT_1: 113;

      hence thesis by P2, VECTSP_7:def 3, P6, ZMODUL01: 47;

    end;

    theorem :: ZMODUL06:49

    

     HM12: for X,Y be free Z_Module, T be linear-transformation of X, Y, A be Subset of X st T is bijective holds A is Basis of X iff (T .: A) is Basis of Y

    proof

      let X,Y be free Z_Module, L be linear-transformation of X, Y, A be Subset of X;

      assume

       AS1: L is bijective;

      

       D1: ( dom L) = the carrier of X by FUNCT_2:def 1;

      consider K be linear-transformation of Y, X such that

       AS3: K = (L " ) & K is bijective by HM1, AS1;

      thus A is Basis of X implies (L .: A) is Basis of Y by AS1, HM11;

      assume (L .: A) is Basis of Y;

      then (K .: (L .: A)) is Basis of X by AS3, HM11;

      hence thesis by D1, AS1, AS3, FUNCT_1: 107;

    end;

    

     HM13: for X,Y be free Z_Module, T be linear-transformation of X, Y st T is bijective holds X is finite-rank implies Y is finite-rank

    proof

      let X,Y be free Z_Module, L be linear-transformation of X, Y;

      assume

       AS1: L is bijective;

      assume X is finite-rank;

      then

      consider A be finite Subset of X such that

       P1: A is Basis of X;

      (L .: A) is Basis of Y by P1, HM12, AS1;

      hence thesis;

    end;

    theorem :: ZMODUL06:50

    for X,Y be free Z_Module, T be linear-transformation of X, Y st T is bijective holds X is finite-rank iff Y is finite-rank

    proof

      let X,Y be free Z_Module, T be linear-transformation of X, Y;

      assume

       AS1: T is bijective;

      consider K be linear-transformation of Y, X such that

       AS3: K = (T " ) & K is bijective by HM1, AS1;

      thus thesis by HM13, AS1, AS3;

    end;

    theorem :: ZMODUL06:51

    

     HM15: for X,Y be finite-rank free Z_Module, T be linear-transformation of X, Y st T is bijective holds ( rank X) = ( rank Y)

    proof

      let X,Y be finite-rank free Z_Module, T be linear-transformation of X, Y;

      assume

       AS1: T is bijective;

      for I be Basis of X holds ( rank Y) = ( card I)

      proof

        let I be Basis of X;

        ( dom T) = the carrier of X by FUNCT_2:def 1;

        then

         X12: ( card I) = ( card (T .: I)) by CARD_1: 5, AS1, CARD_1: 33;

        (T .: I) is Basis of Y by AS1, HM12;

        hence ( rank Y) = ( card I) by X12, ZMODUL03:def 5;

      end;

      hence thesis by ZMODUL03:def 5;

    end;

    theorem :: ZMODUL06:52

    

     ThRankS1: for V be Z_Module, W be finite-rank free Subspace of V, a be Element of INT.Ring st a <> ( 0. INT.Ring ) holds ( rank (a (*) W)) = ( rank W)

    proof

      let V be Z_Module, W be finite-rank free Subspace of V, a be Element of INT.Ring such that

       A1: a <> ( 0. INT.Ring );

      defpred P[ Element of W, object] means $2 = (a * $1);

      

       P0: for x be Element of W holds ex y be Element of (a (*) W) st P[x, y]

      proof

        let x be Element of W;

        (a * x) in the carrier of (a (*) W);

        hence thesis;

      end;

      consider F be Function of W, (a (*) W) such that

       A2: for x be Element of W holds P[x, (F . x)] from FUNCT_2:sch 3( P0);

      

       X1X: for x1,x2 be object st x1 in the carrier of W & x2 in the carrier of W & (F . x1) = (F . x2) holds x1 = x2

      proof

        let x1,x2 be object such that

         D1: x1 in the carrier of W & x2 in the carrier of W & (F . x1) = (F . x2);

        reconsider xx1 = x1, xx2 = x2 as Element of W by D1;

        (F . x1) = (a * xx1) & (F . x2) = (a * xx2) by A2;

        hence thesis by A1, ZMODUL01: 10, D1;

      end;

      for y be object st y in the carrier of (a (*) W) holds y in ( rng F)

      proof

        let y be object such that

         D1: y in the carrier of (a (*) W);

        consider v be Element of W such that

         D2: y = (a * v) by D1;

        (F . v) = (a * v) by A2;

        hence y in ( rng F) by D2, FUNCT_2: 4;

      end;

      then

       X2X: the carrier of (a (*) W) c= ( rng F);

      

       B0: F is additive

      proof

        let x,y be Element of W;

        

         B03: (F . x) = (a * x) by A2;

        

         B04: (F . y) = (a * y) by A2;

        

        thus (F . (x + y)) = (a * (x + y)) by A2

        .= ((a * x) + (a * y)) by VECTSP_1:def 14

        .= ((F . x) + (F . y)) by ZMODUL01: 28, B03, B04;

      end;

      for r be Element of INT.Ring , x be Element of W holds (F . (r * x)) = (r * (F . x))

      proof

        let r be Element of INT.Ring , x be Element of W;

        

        thus (F . (r * x)) = (a * (r * x)) by A2

        .= ((a * r) * x) by VECTSP_1:def 16

        .= (r * (a * x)) by VECTSP_1:def 16

        .= (r * (F . x)) by ZMODUL01: 29, A2;

      end;

      then

      reconsider F as linear-transformation of W, (a (*) W) by B0, MOD_2:def 2;

      reconsider aW = (a (*) W) as finite-rank free Z_Module;

      reconsider W0 = W as finite-rank free Z_Module;

      reconsider F as linear-transformation of W0, aW;

      F is one-to-one onto by X1X, FUNCT_2: 19, X2X, FUNCT_2:def 3, XBOOLE_0:def 10;

      hence thesis by HM15;

    end;

    theorem :: ZMODUL06:53

    for V be Z_Module, W1,W2,W3 be finite-rank free Subspace of V, a be Element of INT.Ring st a <> ( 0. INT.Ring ) & W3 = (a (*) W1) holds ( rank (W3 /\ W2)) = ( rank (W1 /\ W2))

    proof

      let V be Z_Module, W1,W2,W3 be finite-rank free Subspace of V, a be Element of INT.Ring such that

       A1: a <> ( 0. INT.Ring ) & W3 = (a (*) W1);

      (W3 /\ W2) is Subspace of (W1 /\ W2)

      proof

        (W3 /\ W2) is Subspace of W3 by ZMODUL01: 105;

        then

         B2: (W3 /\ W2) is Subspace of W1 by A1, ZMODUL01: 42;

        (W3 /\ W2) is Subspace of W2 by ZMODUL01: 105;

        hence thesis by B2, ZMODUL02: 75;

      end;

      then

       A2: ( rank (W3 /\ W2)) <= ( rank (W1 /\ W2)) by ZMODUL05: 2;

      (a (*) (W1 /\ W2)) is Subspace of (W3 /\ W2)

      proof

        reconsider WX = (a (*) (W1 /\ W2)) as Subspace of V by ZMODUL01: 42;

        for v be Vector of V st v in WX holds v in (W3 /\ W2)

        proof

          let v be Vector of V such that

           C1: v in WX;

          consider vx be Vector of (W1 /\ W2) such that

           C2: v = (a * vx) by C1;

          reconsider vvx = vx as Vector of V by ZMODUL01: 25;

          

           CX: vvx in (W1 /\ W2);

          then vvx in W1 by ZMODUL01: 94;

          then

          reconsider vvvx = vvx as Vector of W1;

          (a * vvvx) in (a * W1);

          then (a * vvx) in W3 by A1, ZMODUL01: 29;

          then

           C3: v in W3 by C2, ZMODUL01: 29;

          vvx in W2 by CX, ZMODUL01: 94;

          then (a * vvx) in W2 by ZMODUL01: 37;

          then v in W2 by C2, ZMODUL01: 29;

          hence thesis by C3, ZMODUL01: 94;

        end;

        hence thesis by ZMODUL01: 44;

      end;

      then ( rank (a (*) (W1 /\ W2))) <= ( rank (W3 /\ W2)) by ZMODUL05: 2;

      then ( rank (W1 /\ W2)) <= ( rank (W3 /\ W2)) by A1, ThRankS1;

      hence thesis by A2, XXREAL_0: 1;

    end;

    theorem :: ZMODUL06:54

    for V be torsion-free Z_Module, W1,W2,W3 be finite-rank free Subspace of V, a be Element of INT.Ring st a <> ( 0. INT.Ring ) & W3 = (a (*) W1) holds ( rank (W3 + W2)) = ( rank (W1 + W2))

    proof

      let V be torsion-free Z_Module, W1,W2,W3 be finite-rank free Subspace of V, a be Element of INT.Ring such that

       A1: a <> ( 0. INT.Ring ) & W3 = (a (*) W1);

      for v be Vector of V st v in (W3 + W2) holds v in (W1 + W2)

      proof

        let v be Vector of V such that

         B1: v in (W3 + W2);

        consider v1,v2 be Vector of V such that

         B2: v1 in W3 & v2 in W2 & v = (v1 + v2) by B1, ZMODUL01: 92;

        v1 in W1 by B2, A1;

        hence thesis by B2, ZMODUL01: 92;

      end;

      then (W3 + W2) is Subspace of (W1 + W2) by ZMODUL01: 44;

      then

       A2: ( rank (W3 + W2)) <= ( rank (W1 + W2)) by ZMODUL05: 2;

      reconsider aW = (a (*) (W1 + W2)) as finite-rank free Subspace of V by ZMODUL01: 42;

      for v be Vector of V st v in (a (*) (W1 + W2)) holds v in (W3 + W2)

      proof

        let v be Vector of V such that

         B1: v in (a (*) (W1 + W2));

        consider vx be Vector of (W1 + W2) such that

         B2: v = (a * vx) by B1;

        reconsider vvx = vx as Vector of V by ZMODUL01: 25;

        vvx in (W1 + W2);

        then

        consider v1,v2 be Vector of V such that

         B3: v1 in W1 & v2 in W2 & vvx = (v1 + v2) by ZMODUL01: 92;

        

         B4: v = (a * vvx) by B2, ZMODUL01: 29

        .= ((a * v1) + (a * v2)) by VECTSP_1:def 14, B3;

        reconsider vv1 = v1 as Vector of W1 by B3;

        (a * vv1) in (a * W1);

        then

         B5: (a * v1) in W3 by A1, ZMODUL01: 29;

        (a * v2) in W2 by B3, ZMODUL01: 37;

        hence thesis by B4, B5, ZMODUL01: 92;

      end;

      then aW is Subspace of (W3 + W2) by ZMODUL01: 44;

      then ( rank (a (*) (W1 + W2))) <= ( rank (W3 + W2)) by ZMODUL05: 2;

      then ( rank (W1 + W2)) <= ( rank (W3 + W2)) by A1, ThRankS1;

      hence thesis by A2, XXREAL_0: 1;

    end;

    theorem :: ZMODUL06:55

    

     ThISRank2: for V be torsion-free Z_Module, W1,W2 be finite-rank free Subspace of V, I be Basis of W1 st (for v be Vector of V st v in I holds ((W1 /\ W2) /\ ( Lin {v})) <> ( (0). V)) holds ( rank (W1 /\ W2)) = ( rank W1)

    proof

      let V be torsion-free Z_Module;

      defpred P[ Nat] means for W1,W2 be finite-rank free Subspace of V, I be Basis of W1 st (for v be Vector of V st v in I holds ((W1 /\ W2) /\ ( Lin {v})) <> ( (0). V)) & ( rank W1) = $1 holds ( rank (W1 /\ W2)) = ( rank W1);

      

       A1: P[ 0 ] by ThISRank1;

      

       A2: for n be Nat st P[n] holds P[(n + 1)]

      proof

        let n be Nat such that

         B1: P[n];

        let W1,W2 be finite-rank free Subspace of V, I be Basis of W1 such that

         B2: (for v be Vector of V st v in I holds ((W1 /\ W2) /\ ( Lin {v})) <> ( (0). V)) & ( rank W1) = (n + 1);

        ( card I) > 0 by ZMODUL03:def 5, B2;

        then I <> ( {} the carrier of W1);

        then

        consider u be object such that

         B3: u in I by XBOOLE_0: 7;

        reconsider u as Vector of W1 by B3;

        reconsider uu = u as Vector of V by ZMODUL01: 25;

        

         BX1: I is linearly-independent by VECTSP_7:def 3;

        reconsider II = I as linearly-independent Subset of V by ZMODUL03: 15, VECTSP_7:def 3;

        (I \ {u}) is linearly-independent by BX1, XBOOLE_1: 36, ZMODUL02: 56;

        then

        reconsider Iu = (I \ {u}) as linearly-independent Subset of V by ZMODUL03: 15;

        ( (Omega). W1) = ( Lin I) by VECTSP_7:def 3

        .= ( Lin II) by ZMODUL03: 20;

        then

         BX2: ( (Omega). W1) = (( Lin Iu) + ( Lin {uu})) & (( Lin Iu) /\ ( Lin {uu})) = ( (0). V) & ( Lin Iu) is free & ( Lin {uu}) is free & uu <> ( 0. V) by B3, ThLin8;

        reconsider LIu = ( Lin Iu) as finite-rank free Subspace of V;

        

         B5: Iu is Basis of ( Lin Iu) by ThLin7;

        ( card Iu) = (( card I) - ( card {u})) by B3, ZFMISC_1: 31, CARD_2: 44

        .= (( rank W1) - ( card {u})) by ZMODUL03:def 5

        .= ((n + 1) - 1) by B2, CARD_1: 30

        .= n;

        then

         B6: ( rank LIu) = n by B5, ZMODUL03:def 5;

        

         B7X: for v be Vector of V st v in Iu holds ((( Lin Iu) /\ W2) /\ ( Lin {v})) <> ( (0). V)

        proof

          let v be Vector of V such that

           C1: v in Iu;

          v in I by C1, TARSKI:def 3, XBOOLE_1: 36;

          then ((W1 /\ W2) /\ ( Lin {v})) <> ( (0). V) by B2;

          then (W1 /\ (W2 /\ ( Lin {v}))) <> ( (0). V) by ZMODUL01: 104;

          then

           C2: (W2 /\ ( Lin {v})) <> ( (0). V) by ZMODUL01: 107;

          

           C3: v <> ( 0. V) by C1, ZMODUL02: 57;

          

           C4: v in ( Lin {v}) by ZMODUL02: 65, ZFMISC_1: 31;

          v in LIu by C1, ZMODUL02: 65;

          then (LIu /\ ( Lin {v})) <> ( (0). V) by C3, ZMODUL02: 66, C4, ZMODUL01: 94;

          hence thesis by C2, LmISRank21;

        end;

        

         B8: ((W1 /\ W2) /\ ( Lin {uu})) <> ( (0). V) by B2, B3;

        ((LIu /\ W2) + ( Lin {uu})) is Subspace of ((W1 /\ W2) + ( Lin {uu}))

        proof

          for x be Vector of V st x in ((LIu /\ W2) + ( Lin {uu})) holds x in ((W1 /\ W2) + ( Lin {uu}))

          proof

            let x be Vector of V such that

             D1: x in ((LIu /\ W2) + ( Lin {uu}));

            consider x1,x2 be Vector of V such that

             D2: x1 in (LIu /\ W2) & x2 in ( Lin {uu}) & x = (x1 + x2) by D1, ZMODUL01: 92;

            

             D3: x1 in LIu & x1 in W2 by D2, ZMODUL01: 94;

            then x1 in ( (Omega). W1) by BX2, ZMODUL01: 93;

            then x1 in W1;

            then x1 in (W1 /\ W2) by D3, ZMODUL01: 94;

            hence thesis by D2, ZMODUL01: 92;

          end;

          hence thesis by ZMODUL01: 44;

        end;

        then

         B10X: ( rank ((LIu /\ W2) + ( Lin {uu}))) <= ( rank ((W1 /\ W2) + ( Lin {uu}))) by ZMODUL05: 2;

        ((LIu /\ ( Lin {uu})) /\ W2) = ( (0). V) by ZMODUL01: 107, BX2;

        then ((W2 /\ LIu) /\ ( Lin {uu})) = ( (0). V) by ZMODUL01: 104;

        

        then ( rank ((LIu /\ W2) + ( Lin {uu}))) = (( rank (LIu /\ W2)) + ( rank ( Lin {uu}))) by ThRankDirectSum

        .= (( rank (LIu /\ W2)) + 1) by BX2, LmRank0a

        .= (( rank LIu) + 1) by B7X, B1, B5, B6;

        then

         B11: (( rank LIu) + 1) <= ( rank (W1 /\ W2)) by B10X, B8, BX2, LmRank2;

        

         B12: ( rank W1) = ( rank ( (Omega). W1)) by ZMODUL05: 4

        .= (( rank LIu) + ( rank ( Lin {uu}))) by BX2, ThRankDirectSum

        .= (( rank LIu) + 1) by BX2, LmRank0a;

        (W1 /\ W2) is Subspace of W1 by ZMODUL01: 105;

        then ( rank (W1 /\ W2)) <= ( rank W1) by ZMODUL05: 2;

        hence thesis by B12, B11, XXREAL_0: 1;

      end;

      

       A3: for n be Nat holds P[n] from NAT_1:sch 2( A1, A2);

      let W1,W2 be finite-rank free Subspace of V, I be Basis of W1 such that

       A4: for v be Vector of V st v in I holds ((W1 /\ W2) /\ ( Lin {v})) <> ( (0). V);

      thus thesis by A4, A3;

    end;

    theorem :: ZMODUL06:56

    for V be torsion-free Z_Module, W1,W2 be finite-rank free Subspace of V, I be Basis of W1 st ( rank (W1 /\ W2)) < ( rank W1) holds ex v be Vector of V st v in I & ((W1 /\ W2) /\ ( Lin {v})) = ( (0). V) by ThISRank2;

    theorem :: ZMODUL06:57

    

     LmISRank41: for V be torsion-free Z_Module, W1,W2 be finite-rank free Subspace of V, I be Basis of W1 st ( rank (W1 /\ W2)) = ( rank W1) holds (for v be Vector of V st v in I holds ((W1 /\ W2) /\ ( Lin {v})) <> ( (0). V))

    proof

      let V be torsion-free Z_Module, W1,W2 be finite-rank free Subspace of V, I be Basis of W1 such that

       A1: ( rank (W1 /\ W2)) = ( rank W1);

      assume ex v be Vector of V st v in I & ((W1 /\ W2) /\ ( Lin {v})) = ( (0). V);

      then

      consider v be Vector of V such that

       A2: v in I & ((W1 /\ W2) /\ ( Lin {v})) = ( (0). V);

      reconsider II = I as linearly-independent Subset of V by ZMODUL03: 15, VECTSP_7:def 3;

      

       A4X: ( (Omega). W1) = ( Lin I) by VECTSP_7:def 3

      .= ( Lin II) by ZMODUL03: 20;

      then

       A4: ( (Omega). W1) = (( Lin (II \ {v})) + ( Lin {v})) & (( Lin (II \ {v})) /\ ( Lin {v})) = ( (0). V) & ( Lin (II \ {v})) is free & ( Lin {v}) is free & v <> ( 0. V) by A2, ThLin8;

      reconsider LIv = ( Lin (II \ {v})) as finite-rank free Subspace of V;

      reconsider W1s = ( (Omega). W1), W2s = ( (Omega). W2) as strict finite-rank free Subspace of V by ZMODUL01: 42;

      ( rank W1s) = ( rank ((W1s /\ W2s) + W1s)) by ZMODUL01: 112

      .= ( rank ((W1 /\ W2) + W1s)) by ZMODUL04: 23;

      then

       A6: ( rank W1) = ( rank ((W1 /\ W2) + W1s)) by ZMODUL05: 4;

      ((W1 /\ W2) + W1s) = ((W1 /\ W2) + (LIv + ( Lin {v}))) by A4X, A2, ThLin8

      .= (((W1 /\ W2) + ( Lin {v})) + LIv) by ZMODUL01: 96;

      then ((W1 /\ W2) + ( Lin {v})) is Subspace of ((W1 /\ W2) + W1s) by ZMODUL01: 97;

      then

       A8: ( rank ((W1 /\ W2) + ( Lin {v}))) <= ( rank W1) by A6, ZMODUL05: 2;

      ( rank ((W1 /\ W2) + ( Lin {v}))) = (( rank (W1 /\ W2)) + ( rank ( Lin {v}))) by A2, ThRankDirectSum

      .= (( rank W1) + 1) by A1, A4, LmRank0a;

      hence contradiction by A8, NAT_1: 13;

    end;

    theorem :: ZMODUL06:58

    

     LmISRank42: for V be torsion-free Z_Module, W1,W2 be finite-rank free Subspace of V, I be Basis of W1 st (for v be Vector of V st v in I holds ((W1 /\ W2) /\ ( Lin {v})) <> ( (0). V)) holds ( rank (W1 + W2)) = ( rank W2)

    proof

      let V be torsion-free Z_Module;

      defpred P[ Nat] means for W1,W2 be finite-rank free Subspace of V, I be Basis of W1 st (for v be Vector of V st v in I holds ((W1 /\ W2) /\ ( Lin {v})) <> ( (0). V)) & ( rank W1) = $1 holds ( rank (W1 + W2)) = ( rank W2);

      

       A1: P[ 0 ]

      proof

        let W1,W2 be finite-rank free Subspace of V, I be Basis of W1 such that

         B1: (for v be Vector of V st v in I holds ((W1 /\ W2) /\ ( Lin {v})) <> ( (0). V)) & ( rank W1) = 0 ;

        

         B2: ( (Omega). W1) = ( (0). W1) by B1, ZMODUL05: 1

        .= ( (0). V) by ZMODUL01: 51;

        reconsider W1s = ( (Omega). W1), W2s = ( (Omega). W2) as strict finite-rank free Subspace of V by ZMODUL01: 42;

        

        thus ( rank (W1 + W2)) = ( rank (W1s + W2s)) by ZMODUL04: 22

        .= ( rank W2s) by ZMODUL01: 99, B2

        .= ( rank W2) by ZMODUL05: 4;

      end;

      

       A2: for n be Nat st P[n] holds P[(n + 1)]

      proof

        let n be Nat such that

         B1: P[n];

        let W1,W2 be finite-rank free Subspace of V, I be Basis of W1 such that

         B2: (for v be Vector of V st v in I holds ((W1 /\ W2) /\ ( Lin {v})) <> ( (0). V)) & ( rank W1) = (n + 1);

        ( card I) > 0 by ZMODUL03:def 5, B2;

        then I <> ( {} the carrier of W1);

        then

        consider u be object such that

         B3: u in I by XBOOLE_0: 7;

        reconsider u as Vector of W1 by B3;

        reconsider uu = u as Vector of V by ZMODUL01: 25;

        

         B4: I is linearly-independent by VECTSP_7:def 3;

        reconsider II = I as linearly-independent Subset of V by ZMODUL03: 15, VECTSP_7:def 3;

        (I \ {u}) is linearly-independent by B4, XBOOLE_1: 36, ZMODUL02: 56;

        then

        reconsider Iu = (I \ {u}) as linearly-independent Subset of V by ZMODUL03: 15;

        

         BX2X: ( (Omega). W1) = ( Lin I) by VECTSP_7:def 3

        .= ( Lin II) by ZMODUL03: 20;

        then

         BX2: ( (Omega). W1) = (( Lin Iu) + ( Lin {uu})) & (( Lin Iu) /\ ( Lin {uu})) = ( (0). V) & ( Lin Iu) is free & ( Lin {uu}) is free & uu <> ( 0. V) by B3, ThLin8;

        reconsider LIu = ( Lin Iu) as finite-rank free Subspace of V;

        

         B5: Iu is Basis of ( Lin Iu) by ThLin7;

        ( card Iu) = (( card I) - ( card {u})) by B3, ZFMISC_1: 31, CARD_2: 44

        .= (( rank W1) - ( card {u})) by ZMODUL03:def 5

        .= ((n + 1) - 1) by B2, CARD_1: 30

        .= n;

        then

         B6: ( rank LIu) = n by B5, ZMODUL03:def 5;

        

         B7X: for v be Vector of V st v in Iu holds ((( Lin Iu) /\ W2) /\ ( Lin {v})) <> ( (0). V)

        proof

          let v be Vector of V such that

           C1: v in Iu;

          v in I by C1, TARSKI:def 3, XBOOLE_1: 36;

          then ((W1 /\ W2) /\ ( Lin {v})) <> ( (0). V) by B2;

          then (W1 /\ (W2 /\ ( Lin {v}))) <> ( (0). V) by ZMODUL01: 104;

          then

           C2: (W2 /\ ( Lin {v})) <> ( (0). V) by ZMODUL01: 107;

          

           C3: v <> ( 0. V) by C1, ZMODUL02: 57;

          

           C4: v in ( Lin {v}) by ZMODUL02: 65, ZFMISC_1: 31;

          v in LIu by C1, ZMODUL02: 65;

          then (LIu /\ ( Lin {v})) <> ( (0). V) by C3, ZMODUL02: 66, C4, ZMODUL01: 94;

          hence thesis by C2, LmISRank21;

        end;

        ((W1 /\ W2) /\ ( Lin {uu})) = (W1 /\ (W2 /\ ( Lin {uu}))) by ZMODUL01: 104;

        then (W2 /\ ( Lin {uu})) <> ( (0). V) by ZMODUL01: 107, B2, B3;

        then ((LIu + W2) /\ ( Lin {uu})) <> ( (0). V) by ThIS1;

        

        then

         B8: ( rank ((LIu + W2) + ( Lin {uu}))) = ( rank (LIu + W2)) by BX2, LmRank2

        .= ( rank W2) by B7X, B1, B5, B6;

        reconsider W1s = ( (Omega). W1), W2s = ( (Omega). W2) as strict finite-rank free Subspace of V by ZMODUL01: 42;

        

         B9: ( (Omega). W1s) = W1s;

        ((LIu + W2) + ( Lin {uu})) = ((( Lin {uu}) + LIu) + W2) by ZMODUL01: 96

        .= (W1s + W2) by BX2X, B3, ThLin8

        .= (W1s + W2s) by B9, ZMODUL04: 22

        .= (W1 + W2) by ZMODUL04: 22;

        hence thesis by B8;

      end;

      

       A3: for n be Nat holds P[n] from NAT_1:sch 2( A1, A2);

      let W1,W2 be finite-rank free Subspace of V, I be Basis of W1 such that

       A4: for v be Vector of V st v in I holds ((W1 /\ W2) /\ ( Lin {v})) <> ( (0). V);

      set rk = ( rank W1);

       P[rk] by A3;

      hence thesis by A4;

    end;

    theorem :: ZMODUL06:59

    

     ThISRank4: for V be torsion-free Z_Module, W1,W2 be finite-rank free Subspace of V st ( rank (W1 /\ W2)) = ( rank W1) holds ( rank (W1 + W2)) = ( rank W2)

    proof

      let V be torsion-free Z_Module, W1,W2 be finite-rank free Subspace of V such that

       A1: ( rank (W1 /\ W2)) = ( rank W1);

      set I = the Basis of W1;

      for v be Vector of V st v in I holds ((W1 /\ W2) /\ ( Lin {v})) <> ( (0). V) by A1, LmISRank41;

      hence thesis by LmISRank42;

    end;

    theorem :: ZMODUL06:60

    

     VECT9Th26: for G be Field, V be VectSp of G, A be Subset of V st A is linearly-independent holds A is Basis of ( Lin A)

    proof

      let G be Field, V be VectSp of G;

      let A be Subset of V such that

       A1: A is linearly-independent;

      set W = ( Lin A);

      for x be object st x in A holds x in the carrier of W by STRUCT_0:def 5, VECTSP_7: 8;

      then

      reconsider B = A as linearly-independent Subset of W by A1, VECTSP_9: 12, TARSKI:def 3;

      W = ( Lin B) by VECTSP_9: 17;

      hence thesis by VECTSP_7:def 3;

    end;

    theorem :: ZMODUL06:61

    

     LmISRank501: for V be Mult-cancelable finite-rank free Z_Module, W1,W2 be finite-rank free Subspace of V holds (( rank (W1 + W2)) + ( rank (W1 /\ W2))) = (( rank W1) + ( rank W2))

    proof

      let V be Mult-cancelable finite-rank free Z_Module, W1,W2 be finite-rank free Subspace of V;

      consider I1 be finite Subset of V such that

       P1: I1 is finite Subset of W1 & I1 is linearly-independent & ( Lin I1) = ( (Omega). W1) & ( card I1) = ( rank W1) by LmFree2;

      reconsider I1 as linearly-independent Subset of V by P1;

      reconsider I10 = I1 as Basis of ( Lin I1) by ThLin7;

      consider I2 be finite Subset of V such that

       P2: I2 is finite Subset of W2 & I2 is linearly-independent & ( Lin I2) = ( (Omega). W2) & ( card I2) = ( rank W2) by LmFree2;

      reconsider I2 as linearly-independent Subset of V by P2;

      reconsider I20 = I2 as Basis of ( Lin I2) by ThLin7;

      consider I1I2 be finite Subset of V such that

       P3: I1I2 is finite Subset of (W1 + W2) & I1I2 is linearly-independent & ( Lin I1I2) = ( (Omega). (W1 + W2)) & ( card I1I2) = ( rank (W1 + W2)) by LmFree2;

      reconsider I1I2 as linearly-independent Subset of V by P3;

      reconsider I1I20 = I1I2 as Basis of ( Lin I1I2) by ThLin7;

      consider I12 be finite Subset of V such that

       P4: I12 is finite Subset of (W1 /\ W2) & I12 is linearly-independent & ( Lin I12) = ( (Omega). (W1 /\ W2)) & ( card I12) = ( rank (W1 /\ W2)) by LmFree2;

      set Iq1 = (( MorphsZQ V) .: I1);

      set Iq2 = (( MorphsZQ V) .: I2);

      set IIq12 = (( MorphsZQ V) .: I1I2);

      set Iq12 = (( MorphsZQ V) .: I12);

      reconsider Iq10 = Iq1 as Basis of ( Lin Iq1) by ZMODUL04: 11, VECT9Th26;

      reconsider Iq20 = Iq2 as Basis of ( Lin Iq2) by ZMODUL04: 11, VECT9Th26;

      reconsider IIq120 = IIq12 as Basis of ( Lin IIq12) by ZMODUL04: 11, VECT9Th26;

      reconsider Iq120 = Iq12 as Basis of ( Lin Iq12) by P4, ZMODUL04: 11, VECT9Th26;

      

       R1: ( dim ( Lin Iq1)) = ( card Iq1) by VECTSP_9: 26, ZMODUL04: 11;

      

       R2: ( dim ( Lin Iq2)) = ( card Iq2) by VECTSP_9: 26, ZMODUL04: 11;

      

       R3: ( dim ( Lin IIq12)) = ( card IIq12) by VECTSP_9: 26, ZMODUL04: 11;

      

       R4: ( dim ( Lin Iq12)) = ( card Iq12) by P4, VECTSP_9: 26, ZMODUL04: 11;

      

       Z0: ( MorphsZQ V) is one-to-one by ZMODUL04:def 6;

      

       S2: ( dom ( MorphsZQ V)) = the carrier of V by FUNCT_2:def 1;

      

       D1: ( dim ( Lin Iq1)) = ( rank W1) by P1, S2, CARD_1: 5, Z0, CARD_1: 33, R1;

      

       D2: ( dim ( Lin Iq2)) = ( rank W2) by P2, CARD_1: 5, Z0, CARD_1: 33, S2, R2;

      

       D3: ( dim ( Lin IIq12)) = ( rank (W1 + W2)) by P3, CARD_1: 5, Z0, CARD_1: 33, S2, R3;

      

       D4: ( dim ( Lin Iq12)) = ( rank (W1 /\ W2)) by P4, CARD_1: 5, Z0, CARD_1: 33, S2, R4;

      for v be Vector of ( Z_MQ_VectSp V) holds v in (( Lin Iq1) + ( Lin Iq2)) iff v in ( Lin IIq12)

      proof

        let v be Vector of ( Z_MQ_VectSp V);

        hereby

          assume v in (( Lin Iq1) + ( Lin Iq2));

          then

          consider v1,v2 be Vector of ( Z_MQ_VectSp V) such that

           PP1: v1 in ( Lin Iq1) & v2 in ( Lin Iq2) & v = (v1 + v2) by VECTSP_5: 1;

          consider lq1 be Linear_Combination of Iq1 such that

           PP2: v1 = ( Sum lq1) by VECTSP_7: 7, PP1;

          consider lq2 be Linear_Combination of Iq2 such that

           PP3: v2 = ( Sum lq2) by VECTSP_7: 7, PP1;

          consider m1 be Element of INT.Ring , a1 be Element of F_Rat , l1 be Linear_Combination of I1 such that

           PP4: m1 <> 0 & m1 = a1 & l1 = ((a1 * lq1) * ( MorphsZQ V)) & (( MorphsZQ V) " ( Carrier lq1)) = ( Carrier l1) by ZMODUL04: 9;

          

           PP5: (a1 * v1) = (( MorphsZQ V) . ( Sum l1)) by PP4, ZMODUL04: 10, PP2;

          consider m2 be Element of INT.Ring , a2 be Element of F_Rat , l2 be Linear_Combination of I2 such that

           PP6: m2 <> 0 & m2 = a2 & l2 = ((a2 * lq2) * ( MorphsZQ V)) & (( MorphsZQ V) " ( Carrier lq2)) = ( Carrier l2) by ZMODUL04: 9;

          

           PP7: (a2 * v2) = (( MorphsZQ V) . ( Sum l2)) by PP6, ZMODUL04: 10, PP3;

          

           PP8: ((a1 * a2) * v1) = (a2 * (a1 * v1)) by VECTSP_1:def 16

          .= (( MorphsZQ V) . (m2 * ( Sum l1))) by PP6, ZMODUL04:def 6, PP5;

          

           PP9: ((a1 * a2) * v2) = (a1 * (a2 * v2)) by VECTSP_1:def 16

          .= (( MorphsZQ V) . (m1 * ( Sum l2))) by PP4, ZMODUL04:def 6, PP7;

          

           PP10: ((a1 * a2) * (v1 + v2)) = (((a1 * a2) * v1) + ((a1 * a2) * v2)) by VECTSP_1:def 14

          .= (( MorphsZQ V) . ((m2 * ( Sum l1)) + (m1 * ( Sum l2)))) by ZMODUL04:def 6, PP8, PP9;

          ( Sum l1) in ( (Omega). W1) by P1, ZMODUL02: 64;

          then ( Sum l1) in W1;

          then

           PP11: (m2 * ( Sum l1)) in W1 by ZMODUL01: 37;

          ( Sum l2) in ( Lin I2) by ZMODUL02: 64;

          then ( Sum l2) in W2 by P2;

          then (m1 * ( Sum l2)) in W2 by ZMODUL01: 37;

          then

          consider l12 be Linear_Combination of I1I2 such that

           PP13: ((m2 * ( Sum l1)) + (m1 * ( Sum l2))) = ( Sum l12) by ZMODUL02: 64, P3, PP11, ZMODUL01: 92;

          reconsider r1 = 1 as Element of F_Rat ;

          reconsider i1 = 1 as Element of INT.Ring ;

          consider lq12 be Linear_Combination of IIq12 such that

           PP14: l12 = (lq12 * ( MorphsZQ V)) & ( Carrier lq12) = (( MorphsZQ V) .: ( Carrier l12)) by ZMODUL04: 12;

          r1 = ( 1. F_Rat );

          then l12 = ((r1 * lq12) * ( MorphsZQ V)) & 0 <> i1 & r1 = i1 by PP14;

          then

           Y1: (r1 * ( Sum lq12)) = (( MorphsZQ V) . ( Sum l12)) by ZMODUL04: 10;

          reconsider ra1 = a1, ra2 = a2 as Rational;

          

           Y3: (((ra1 * ra2) " ) * (ra1 * ra2)) = 1 by XCMPLX_0:def 7, PP4, PP6;

          ((a1 * a2) " ) = ((ra1 * ra2) " ) by GAUSSINT: 15, PP4, PP6;

          then

           Y2: (((a1 * a2) " ) * (a1 * a2)) = ( 1. F_Rat ) by Y3;

          

           X1X: (r1 * ( Sum lq12)) = (( 1. F_Rat ) * ( Sum lq12))

          .= ( Sum lq12) by VECTSP_1:def 17;

          (((a1 * a2) " ) * ((a1 * a2) * (v1 + v2))) = ((((a1 * a2) " ) * (a1 * a2)) * (v1 + v2)) by VECTSP_1:def 16

          .= (v1 + v2) by VECTSP_1:def 17, Y2;

          hence v in ( Lin IIq12) by X1X, PP1, VECTSP_4: 21, VECTSP_7: 7, PP13, PP10, Y1;

        end;

        assume v in ( Lin IIq12);

        then

        consider lq12 be Linear_Combination of IIq12 such that

         PP2: v = ( Sum lq12) by VECTSP_7: 7;

        consider m12 be Element of INT.Ring , a12 be Element of F_Rat , l12 be Linear_Combination of I1I2 such that

         PP4: m12 <> 0 & m12 = a12 & l12 = ((a12 * lq12) * ( MorphsZQ V)) & (( MorphsZQ V) " ( Carrier lq12)) = ( Carrier l12) by ZMODUL04: 9;

        

         PP5: (a12 * v) = (( MorphsZQ V) . ( Sum l12)) by PP4, ZMODUL04: 10, PP2;

        consider v1,v2 be Vector of V such that

         PP1: v1 in W1 & v2 in W2 & ( Sum l12) = (v1 + v2) by ZMODUL01: 92, P3, ZMODUL02: 64;

        v1 in ( (Omega). W1) by PP1;

        then

        consider l1 be Linear_Combination of I1 such that

         PP13: v1 = ( Sum l1) by ZMODUL02: 64, P1;

        v2 in ( (Omega). W2) by PP1;

        then

        consider l2 be Linear_Combination of I2 such that

         PP14: v2 = ( Sum l2) by ZMODUL02: 64, P2;

        

         Y1: (a12 * v) = ((( MorphsZQ V) . ( Sum l1)) + (( MorphsZQ V) . ( Sum l2))) by ZMODUL04:def 6, PP1, PP5, PP13, PP14;

        consider lq1 be Linear_Combination of Iq1 such that

         PP15: l1 = (lq1 * ( MorphsZQ V)) & ( Carrier lq1) = (( MorphsZQ V) .: ( Carrier l1)) by ZMODUL04: 12;

        consider lq2 be Linear_Combination of Iq2 such that

         PP16: l2 = (lq2 * ( MorphsZQ V)) & ( Carrier lq2) = (( MorphsZQ V) .: ( Carrier l2)) by ZMODUL04: 12;

        

         Y3: ( Sum lq2) = (( MorphsZQ V) . ( Sum l2)) by PP16, ZMODUL04: 7;

        

         Y4: (a12 * v) = (( Sum lq1) + ( Sum lq2)) by Y1, PP15, ZMODUL04: 7, Y3;

        reconsider w1 = ( Sum lq1) as Vector of ( Z_MQ_VectSp V);

        reconsider w2 = ( Sum lq2) as Vector of ( Z_MQ_VectSp V);

        w1 in ( Lin Iq1) & w2 in ( Lin Iq2) by VECTSP_7: 7;

        then

         Y5: (a12 * v) in (( Lin Iq1) + ( Lin Iq2)) by Y4, VECTSP_5: 1;

        reconsider ra12 = a12 as Rational;

        

         Y7: ((ra12 " ) * ra12) = 1 by XCMPLX_0:def 7, PP4;

        (a12 " ) = (ra12 " ) by PP4, GAUSSINT: 15;

        then

         Y8: ((a12 " ) * a12) = ( 1. F_Rat ) by Y7;

        ((a12 " ) * (a12 * v)) in (( Lin Iq1) + ( Lin Iq2)) by Y5, VECTSP_4: 21;

        then (( 1. F_Rat ) * v) in (( Lin Iq1) + ( Lin Iq2)) by Y8, VECTSP_1:def 16;

        hence v in (( Lin Iq1) + ( Lin Iq2)) by VECTSP_1:def 17;

      end;

      then

       E1: (( Lin Iq1) + ( Lin Iq2)) = ( Lin IIq12) by VECTSP_4: 30;

      for v be Vector of ( Z_MQ_VectSp V) holds v in (( Lin Iq1) /\ ( Lin Iq2)) iff v in ( Lin Iq12)

      proof

        let v be Vector of ( Z_MQ_VectSp V);

        hereby

          assume v in (( Lin Iq1) /\ ( Lin Iq2));

          then

           PP1: v in ( Lin Iq1) & v in ( Lin Iq2) by VECTSP_5: 3;

          consider lq1 be Linear_Combination of Iq1 such that

           PP2: v = ( Sum lq1) by VECTSP_7: 7, PP1;

          consider lq2 be Linear_Combination of Iq2 such that

           PP3: v = ( Sum lq2) by VECTSP_7: 7, PP1;

          consider m1 be Element of INT.Ring , a1 be Element of F_Rat , l1 be Linear_Combination of I1 such that

           PP4: m1 <> 0 & m1 = a1 & l1 = ((a1 * lq1) * ( MorphsZQ V)) & (( MorphsZQ V) " ( Carrier lq1)) = ( Carrier l1) by ZMODUL04: 9;

          

           PP5: (a1 * v) = (( MorphsZQ V) . ( Sum l1)) by PP4, ZMODUL04: 10, PP2;

          consider m2 be Element of INT.Ring , a2 be Element of F_Rat , l2 be Linear_Combination of I2 such that

           PP6: m2 <> 0 & m2 = a2 & l2 = ((a2 * lq2) * ( MorphsZQ V)) & (( MorphsZQ V) " ( Carrier lq2)) = ( Carrier l2) by ZMODUL04: 9;

          

           PP7: (a2 * v) = (( MorphsZQ V) . ( Sum l2)) by PP6, ZMODUL04: 10, PP3;

          

           PP8: ((a1 * a2) * v) = (a2 * (a1 * v)) by VECTSP_1:def 16

          .= (( MorphsZQ V) . (m2 * ( Sum l1))) by PP6, ZMODUL04:def 6, PP5;

          

           PP9: ((a1 * a2) * v) = (a1 * (a2 * v)) by VECTSP_1:def 16

          .= (( MorphsZQ V) . (m1 * ( Sum l2))) by PP4, ZMODUL04:def 6, PP7;

          ( MorphsZQ V) is one-to-one by ZMODUL04:def 6;

          then

           PP10: (m1 * ( Sum l2)) = (m2 * ( Sum l1)) by FUNCT_2: 19, PP8, PP9;

          ( Sum l1) in ( Lin I1) by ZMODUL02: 64;

          then ( Sum l1) in W1 by P1;

          then

           PP11: (m2 * ( Sum l1)) in W1 by ZMODUL01: 37;

          ( Sum l2) in ( (Omega). W2) by P2, ZMODUL02: 64;

          then ( Sum l2) in W2;

          then (m1 * ( Sum l2)) in W2 by ZMODUL01: 37;

          then

          consider l12 be Linear_Combination of I12 such that

           PP13: (m2 * ( Sum l1)) = ( Sum l12) by ZMODUL02: 64, P4, PP10, PP11, ZMODUL01: 94;

          reconsider r1 = 1 as Element of F_Rat ;

          reconsider i1 = 1 as Element of INT.Ring ;

          consider lq12 be Linear_Combination of Iq12 such that

           PP14: l12 = (lq12 * ( MorphsZQ V)) & ( Carrier lq12) = (( MorphsZQ V) .: ( Carrier l12)) by ZMODUL04: 12;

          r1 = ( 1. F_Rat );

          then l12 = ((r1 * lq12) * ( MorphsZQ V)) & 0 <> i1 & r1 = i1 by PP14;

          then

           Y1: (r1 * ( Sum lq12)) = (( MorphsZQ V) . ( Sum l12)) by ZMODUL04: 10;

          reconsider ra1 = a1, ra2 = a2 as Rational;

          

           Y3: (((ra1 * ra2) " ) * (ra1 * ra2)) = 1 by XCMPLX_0:def 7, PP4, PP6;

          ((a1 * a2) " ) = ((ra1 * ra2) " ) by PP4, PP6, GAUSSINT: 15;

          then

           Y2: (((a1 * a2) " ) * (a1 * a2)) = ( 1. F_Rat ) by Y3;

          

           X1X: (r1 * ( Sum lq12)) = (( 1. F_Rat ) * ( Sum lq12))

          .= ( Sum lq12) by VECTSP_1:def 17;

          (((a1 * a2) " ) * ((a1 * a2) * v)) = ((((a1 * a2) " ) * (a1 * a2)) * v) by VECTSP_1:def 16

          .= v by VECTSP_1:def 17, Y2;

          hence v in ( Lin Iq12) by X1X, VECTSP_4: 21, VECTSP_7: 7, PP8, PP13, Y1;

        end;

        assume v in ( Lin Iq12);

        then

        consider lq12 be Linear_Combination of Iq12 such that

         PP2: v = ( Sum lq12) by VECTSP_7: 7;

        consider m12 be Element of INT.Ring , a12 be Element of F_Rat , l12 be Linear_Combination of I12 such that

         PP4: m12 <> 0 & m12 = a12 & l12 = ((a12 * lq12) * ( MorphsZQ V)) & (( MorphsZQ V) " ( Carrier lq12)) = ( Carrier l12) by ZMODUL04: 9;

        

         PP5: (a12 * v) = (( MorphsZQ V) . ( Sum l12)) by PP4, ZMODUL04: 10, PP2;

        ( Sum l12) in ( (Omega). (W1 /\ W2)) by P4, ZMODUL02: 64;

        then

         PP1: ( Sum l12) in W1 & ( Sum l12) in W2 by ZMODUL01: 94;

        ( Sum l12) in ( (Omega). W1) by PP1;

        then

        consider l1 be Linear_Combination of I1 such that

         PP13: ( Sum l12) = ( Sum l1) by ZMODUL02: 64, P1;

        ( Sum l12) in ( (Omega). W2) by PP1;

        then

        consider l2 be Linear_Combination of I2 such that

         PP14: ( Sum l12) = ( Sum l2) by ZMODUL02: 64, P2;

        consider lq1 be Linear_Combination of Iq1 such that

         PP15: l1 = (lq1 * ( MorphsZQ V)) & ( Carrier lq1) = (( MorphsZQ V) .: ( Carrier l1)) by ZMODUL04: 12;

        consider lq2 be Linear_Combination of Iq2 such that

         PP16: l2 = (lq2 * ( MorphsZQ V)) & ( Carrier lq2) = (( MorphsZQ V) .: ( Carrier l2)) by ZMODUL04: 12;

        

         Y4: (a12 * v) = ( Sum lq1) & (a12 * v) = ( Sum lq2) by PP5, PP13, PP14, PP15, PP16, ZMODUL04: 7;

        reconsider w1 = ( Sum lq1) as Vector of ( Z_MQ_VectSp V);

        reconsider w2 = ( Sum lq2) as Vector of ( Z_MQ_VectSp V);

        w1 in ( Lin Iq1) & w2 in ( Lin Iq2) by VECTSP_7: 7;

        then

         Y5: (a12 * v) in (( Lin Iq1) /\ ( Lin Iq2)) by Y4, VECTSP_5: 3;

        reconsider ra12 = a12 as Rational;

        

         Y7: ((ra12 " ) * ra12) = 1 by XCMPLX_0:def 7, PP4;

        (a12 " ) = (ra12 " ) by PP4, GAUSSINT: 15;

        then

         Y8: ((a12 " ) * a12) = ( 1. F_Rat ) by Y7;

        ((a12 " ) * (a12 * v)) in (( Lin Iq1) /\ ( Lin Iq2)) by Y5, VECTSP_4: 21;

        then (((a12 " ) * a12) * v) in (( Lin Iq1) /\ ( Lin Iq2)) by VECTSP_1:def 16;

        hence v in (( Lin Iq1) /\ ( Lin Iq2)) by VECTSP_1:def 17, Y8;

      end;

      then (( Lin Iq1) /\ ( Lin Iq2)) = ( Lin Iq12) by VECTSP_4: 30;

      hence thesis by VECTSP_9: 32, E1, D1, D2, D3, D4;

    end;

    theorem :: ZMODUL06:62

    

     LmISRank51X: for V be torsion-free Z_Module, W1,W2 be finite-rank free Subspace of V holds (( rank (W1 + W2)) + ( rank (W1 /\ W2))) = (( rank W1) + ( rank W2))

    proof

      let V be torsion-free Z_Module, W1,W2 be finite-rank free Subspace of V;

      set W1W2 = (W1 + W2);

      reconsider W10 = W1 as finite-rank free Subspace of W1W2 by ZMODUL01: 97;

      reconsider W20 = W2 as finite-rank free Subspace of W1W2 by ZMODUL01: 97;

      

       R0: (( rank (W10 + W20)) + ( rank (W10 /\ W20))) = (( rank W10) + ( rank W20)) by LmISRank501;

      

       SB1: (W10 + W20) is strict Subspace of V by ZMODUL01: 42;

      for v be Vector of V holds v in (W10 + W20) iff v in (W1 + W2)

      proof

        let v be Vector of V;

        hereby

          assume v in (W10 + W20);

          then

          consider v1,v2 be Vector of W1W2 such that

           S11: v1 in W10 & v2 in W20 & v = (v1 + v2) by ZMODUL01: 92;

          thus v in (W1 + W2) by S11;

        end;

        assume v in (W1 + W2);

        then

        consider v1,v2 be Vector of V such that

         S11: v1 in W1 & v2 in W2 & v = (v1 + v2) by ZMODUL01: 92;

        v1 in the carrier of W10 & v2 in the carrier of W20 by S11;

        then

        reconsider v11 = v1, v22 = v2 as Vector of W1W2 by ZMODUL01: 25;

        (v11 + v22) = (v1 + v2) by ZMODUL01: 28;

        hence v in (W10 + W20) by S11, ZMODUL01: 92;

      end;

      then

       R1: ( rank (W10 + W20)) = ( rank (W1 + W2)) by SB1, ZMODUL01: 46;

      

       SB2: (W10 /\ W20) is strict Subspace of V by ZMODUL01: 42;

      for v be Vector of V holds v in (W10 /\ W20) iff v in (W1 /\ W2)

      proof

        let v be Vector of V;

        hereby

          assume

           X1: v in (W10 /\ W20);

          then

          reconsider v0 = v as Vector of (W10 /\ W20);

          v0 in W10 & v0 in W20 by X1, ZMODUL01: 94;

          hence v in (W1 /\ W2) by ZMODUL01: 94;

        end;

        assume

         X1: v in (W1 /\ W2);

        then

        reconsider v0 = v as Vector of (W1 /\ W2);

        v in W1 & v in W2 by X1, ZMODUL01: 94;

        hence v in (W10 /\ W20) by ZMODUL01: 94;

      end;

      hence thesis by R1, R0, SB2, ZMODUL01: 46;

    end;

    theorem :: ZMODUL06:63

    for V be torsion-free Z_Module, W1,W2 be finite-rank free Subspace of V st ( rank (W1 + W2)) = ( rank W2) holds ( rank (W1 /\ W2)) = ( rank W1)

    proof

      let V be torsion-free Z_Module, W1,W2 be finite-rank free Subspace of V;

      assume ( rank (W1 + W2)) = ( rank W2);

      then (( rank W2) + ( rank (W1 /\ W2))) = (( rank W1) + ( rank W2)) by LmISRank51X;

      hence thesis;

    end;

    theorem :: ZMODUL06:64

    for V be torsion-free Z_Module, W1,W2 be finite-rank free Subspace of V, v be Vector of V st v <> ( 0. V) & (W1 /\ ( Lin {v})) = ( (0). V) & ((W1 + W2) /\ ( Lin {v})) = ( (0). V) holds ( rank ((W1 + ( Lin {v})) /\ W2)) = ( rank (W1 /\ W2))

    proof

      let V be torsion-free Z_Module, W1,W2 be finite-rank free Subspace of V, v be Vector of V such that

       A1: v <> ( 0. V) & (W1 /\ ( Lin {v})) = ( (0). V) & ((W1 + W2) /\ ( Lin {v})) = ( (0). V);

      for u be Vector of V st u in (W1 /\ W2) holds u in ((W1 + ( Lin {v})) /\ W2)

      proof

        let u be Vector of V such that

         B1: u in (W1 /\ W2);

        u in W1 & u in W2 by B1, ZMODUL01: 94;

        then u in (W1 + ( Lin {v})) & u in W2 by ZMODUL01: 93;

        hence thesis by ZMODUL01: 94;

      end;

      then (W1 /\ W2) is Subspace of ((W1 + ( Lin {v})) /\ W2) by ZMODUL01: 44;

      then

       A2: ( rank ((W1 + ( Lin {v})) /\ W2)) >= ( rank (W1 /\ W2)) by ZMODUL05: 2;

      assume

       AS: ( rank ((W1 + ( Lin {v})) /\ W2)) <> ( rank (W1 /\ W2));

      ex u be Vector of V st u in ((W1 + ( Lin {v})) /\ W2) & not u in (W1 /\ W2)

      proof

        assume for u be Vector of V st u in ((W1 + ( Lin {v})) /\ W2) holds u in (W1 /\ W2);

        then ((W1 + ( Lin {v})) /\ W2) is Subspace of (W1 /\ W2) by ZMODUL01: 44;

        then ( rank ((W1 + ( Lin {v})) /\ W2)) <= ( rank (W1 /\ W2)) by ZMODUL05: 2;

        hence contradiction by AS, A2, XXREAL_0: 1;

      end;

      then

      consider u be Vector of V such that

       A4: u in ((W1 + ( Lin {v})) /\ W2) & not u in (W1 /\ W2);

      u in (W1 + ( Lin {v})) by A4, ZMODUL01: 94;

      then

      consider u1,u2 be Vector of V such that

       A5: u1 in W1 & u2 in ( Lin {v}) & u = (u1 + u2) by ZMODUL01: 92;

      

       A6: u in W2 by A4, ZMODUL01: 94;

      

       A7: u2 <> ( 0. V) by A4, A5, A6, ZMODUL01: 94;

      

       A8: ( - u1) in W1 by A5, ZMODUL01: 38;

      (u - u1) = (u2 + (u1 - u1)) by RLVECT_1: 28, A5

      .= (u2 + ( 0. V)) by RLVECT_1: 15

      .= u2;

      then u2 in (W1 + W2) by A6, A8, ZMODUL01: 92;

      hence contradiction by A1, A7, ZMODUL02: 66, A5, ZMODUL01: 94;

    end;

    theorem :: ZMODUL06:65

    

     LmRank41: for V be torsion-free Z_Module, W be finite-rank free Subspace of V, v be Vector of V st v <> ( 0. V) & (W /\ ( Lin {v})) <> ( (0). V) holds ( rank (W /\ ( Lin {v}))) = 1

    proof

      let V be torsion-free Z_Module, W be finite-rank free Subspace of V, v be Vector of V such that

       A1: v <> ( 0. V) & (W /\ ( Lin {v})) <> ( (0). V);

      

       A2: ( rank ( Lin {v})) = 1 by A1, LmRank0a;

      

       A3: (W /\ ( Lin {v})) is Subspace of ( Lin {v}) by ZMODUL01: 105;

      ( rank (W /\ ( Lin {v}))) <> 0

      proof

        assume ( rank (W /\ ( Lin {v}))) = 0 ;

        

        then ( (Omega). (W /\ ( Lin {v}))) = ( (0). (W /\ ( Lin {v}))) by ZMODUL05: 1

        .= ( (0). V) by ZMODUL01: 51;

        hence contradiction by A1;

      end;

      hence ( rank (W /\ ( Lin {v}))) = 1 by A3, NAT_1: 25, ZMODUL05: 2, A2;

    end;

    theorem :: ZMODUL06:66

    

     LmSumMod4: for V be torsion-free Z_Module, W be finite-rank free Subspace of V, v be Vector of V st v <> ( 0. V) & (W /\ ( Lin {v})) <> ( (0). V) holds ex u be Vector of V st u <> ( 0. V) & (W /\ ( Lin {v})) = ( Lin {u})

    proof

      let V be torsion-free Z_Module, W be finite-rank free Subspace of V, v be Vector of V such that

       A1: v <> ( 0. V) & (W /\ ( Lin {v})) <> ( (0). V);

      ( rank (W /\ ( Lin {v}))) = 1 by A1, LmRank41;

      then

      consider uu be Vector of (W /\ ( Lin {v})) such that

       A2: uu <> ( 0. (W /\ ( Lin {v}))) & ( (Omega). (W /\ ( Lin {v}))) = ( Lin {uu}) by ZMODUL05: 5;

      reconsider u = uu as Vector of V by ZMODUL01: 25;

      

       A3: u <> ( 0. V) by A2, ZMODUL01: 26;

      ( (Omega). (W /\ ( Lin {v}))) = ( Lin {u}) by A2, ZMODUL03: 20;

      hence thesis by A3;

    end;

    theorem :: ZMODUL06:67

    

     LmRank421: for V be torsion-free Z_Module, W be finite-rank free Subspace of V, u,v be Vector of V st (W /\ ( Lin {v})) = ( (0). V) & ((W + ( Lin {u})) /\ ( Lin {v})) <> ( (0). V) holds (W /\ ( Lin {u})) = ( (0). V)

    proof

      let V be torsion-free Z_Module, W be finite-rank free Subspace of V, u,v be Vector of V such that

       A1: (W /\ ( Lin {v})) = ( (0). V) & ((W + ( Lin {u})) /\ ( Lin {v})) <> ( (0). V);

      consider x be Vector of V such that

       A2: x in ((W + ( Lin {u})) /\ ( Lin {v})) & x <> ( 0. V) by A1, ZMODUL04: 24;

      x in (W + ( Lin {u})) by A2, ZMODUL01: 94;

      then

      consider x1,x2 be Vector of V such that

       A3: x1 in W & x2 in ( Lin {u}) & x = (x1 + x2) by ZMODUL01: 92;

      consider i be Element of INT.Ring such that

       A5: x2 = (i * u) by A3, ThLin1;

      assume (W /\ ( Lin {u})) <> ( (0). V);

      then

      consider y be Vector of V such that

       A7: y in (W /\ ( Lin {u})) & y <> ( 0. V) by ZMODUL04: 24;

      y in ( Lin {u}) by A7, ZMODUL01: 94;

      then

      consider j be Element of INT.Ring such that

       A8: y = (j * u) by ThLin1;

      

       A9: (j * x1) in W by A3, ZMODUL01: 37;

      

       A10: (j * x2) = ((j * i) * u) by VECTSP_1:def 16, A5

      .= (i * y) by A8, VECTSP_1:def 16;

      y in W by A7, ZMODUL01: 94;

      then (j * x2) in W by A10, ZMODUL01: 37;

      then ((j * x1) + (j * x2)) in W by A9, ZMODUL01: 36;

      then

       A11: (j * x) in W by A3, VECTSP_1:def 14;

      x in ( Lin {v}) by A2, ZMODUL01: 94;

      then (j * x) in ( Lin {v}) by ZMODUL01: 37;

      then

       A12: (j * x) in (W /\ ( Lin {v})) by A11, ZMODUL01: 94;

      j <> ( 0. INT.Ring ) by A7, A8, ZMODUL01: 1;

      hence contradiction by A1, A12, ZMODUL02: 66, A2, ZMODUL01:def 7;

    end;

    theorem :: ZMODUL06:68

    for V be torsion-free Z_Module, W1,W2 be finite-rank free Subspace of V, v be Vector of V st ( rank (W1 /\ W2)) = ( rank W1) & ((W1 + W2) /\ ( Lin {v})) <> ( (0). V) holds (W2 /\ ( Lin {v})) <> ( (0). V)

    proof

      let V be torsion-free Z_Module;

      defpred P[ Nat] means for W1,W2 be finite-rank free Subspace of V, v be Vector of V st ( rank (W1 /\ W2)) = ( rank W1) & ((W1 + W2) /\ ( Lin {v})) <> ( (0). V) & ( rank W1) = $1 holds (W2 /\ ( Lin {v})) <> ( (0). V);

      

       A1: P[ 0 ]

      proof

        let W1,W2 be finite-rank free Subspace of V, v be Vector of V;

        assume

         B1: ( rank (W1 /\ W2)) = ( rank W1) & ((W1 + W2) /\ ( Lin {v})) <> ( (0). V) & ( rank W1) = 0 ;

        

        then

         B2: ( (Omega). W1) = ( (0). W1) by ZMODUL05: 1

        .= ( (0). V) by ZMODUL01: 51;

        reconsider WW2 = ( (Omega). W2) as strict Subspace of V by ZMODUL01: 42;

        

         B3: (W1 + W2) = (( (0). V) + WW2) by B2, ZMODUL04: 22

        .= WW2 by ZMODUL01: 99;

        ( (Omega). ( Lin {v})) = ( Lin {v});

        hence thesis by B3, ZMODUL04: 23, B1;

      end;

      

       A2: for n be Nat st P[n] holds P[(n + 1)]

      proof

        let n be Nat such that

         B1: P[n];

        let W1,W2 be finite-rank free Subspace of V, v be Vector of V;

        assume

         B2: ( rank (W1 /\ W2)) = ( rank W1) & ((W1 + W2) /\ ( Lin {v})) <> ( (0). V) & ( rank W1) = (n + 1);

        then

        consider I be finite Subset of V such that

         B3: I is finite Subset of W1 & I is linearly-independent & ( Lin I) = ( (Omega). W1) & ( card I) = (n + 1) by LmFree2;

        

         BX1: I is Basis of W1

        proof

          reconsider II = I as Subset of W1 by B3;

          ( (Omega). W1) = ( Lin II) by ZMODUL03: 20, B3;

          hence thesis by VECTSP_7:def 3, B3, ZMODUL03: 16;

        end;

        I is non empty by B3;

        then

        consider u be object such that

         B4: u in I by XBOOLE_0:def 1;

        reconsider u as Vector of V by B4;

        

         B5: ( (Omega). W1) = (( Lin (I \ {u})) + ( Lin {u})) & u <> ( 0. V) by B3, B4, ThLin8;

        set Iu = (I \ {u});

         {u} is Subset of I by B4, SUBSET_1: 41;

        

        then

         B7: ( card Iu) = ((n + 1) - ( card {u})) by B3, CARD_2: 44

        .= ((n + 1) - 1) by CARD_1: 30

        .= n;

        reconsider Iu as finite Subset of V;

        

         B8: Iu is linearly-independent by B3, XBOOLE_1: 36, ZMODUL02: 56;

        reconsider LIu = ( Lin Iu) as strict finite-rank free Subspace of V;

        

         BX2: Iu is Basis of LIu by B8, ThLin7;

        

         C1: for v be Vector of V st v in I holds (W2 /\ ( Lin {v})) <> ( (0). V)

        proof

          let v be Vector of V such that

           D1: v in I;

          ((W1 /\ W2) /\ ( Lin {v})) = (W1 /\ (W2 /\ ( Lin {v}))) by ZMODUL01: 104;

          hence (W2 /\ ( Lin {v})) <> ( (0). V) by ZMODUL01: 107, B2, BX1, D1, LmISRank41;

        end;

        

         B10: ( rank (LIu /\ W2)) = ( rank LIu)

        proof

          

           C2: for v be Vector of V st v in Iu holds (W2 /\ ( Lin {v})) <> ( (0). V) by C1, ZFMISC_1: 56;

          for v be Vector of V st v in Iu holds ((LIu /\ W2) /\ ( Lin {v})) <> ( (0). V)

          proof

            let v be Vector of V such that

             D1: v in Iu;

            v in LIu & v in ( Lin {v}) by D1, ZMODUL02: 65, ZFMISC_1: 31;

            then

             D2: v in (LIu /\ ( Lin {v})) by ZMODUL01: 94;

            consider iv be Vector of V such that

             D3: iv in (W2 /\ ( Lin {v})) & iv <> ( 0. V) by ZMODUL04: 24, C2, D1;

            iv in ( Lin {v}) by D3, ZMODUL01: 94;

            then

            consider i be Element of INT.Ring such that

             D4: iv = (i * v) by ThLin1;

            

             D5: iv in (LIu /\ ( Lin {v})) by D2, D4, ZMODUL01: 37;

            iv in W2 by D3, ZMODUL01: 94;

            then (W2 /\ (LIu /\ ( Lin {v}))) <> ( (0). V) by D3, ZMODUL02: 66, D5, ZMODUL01: 94;

            hence thesis by ZMODUL01: 104;

          end;

          hence thesis by BX2, ThISRank2;

        end;

        ((LIu + W2) /\ ( Lin {v})) <> ( (0). V)

        proof

          assume

           C1: ((LIu + W2) /\ ( Lin {v})) = ( (0). V);

          reconsider WW1 = ( (Omega). W1) as strict Subspace of V by ZMODUL01: 42;

          reconsider WW2 = ( (Omega). W2) as strict Subspace of V by ZMODUL01: 42;

          

           C2: ( (Omega). (LIu + ( Lin {u}))) = (LIu + ( Lin {u}));

          

           C3: ((LIu + W2) + ( Lin {u})) = (W2 + (LIu + ( Lin {u}))) by ZMODUL01: 96

          .= (WW2 + (LIu + ( Lin {u}))) by C2, ZMODUL04: 22

          .= (WW2 + WW1) by B3, B4, ThLin8

          .= (W2 + W1) by ZMODUL04: 22;

          then ((LIu + W2) /\ ( Lin {u})) = ( (0). V) by C1, LmRank421, B2;

          

          then

           C4: ( rank ((LIu + W2) + ( Lin {u}))) = (( rank (LIu + W2)) + ( rank ( Lin {u}))) by ThRankDirectSum

          .= (( rank W2) + ( rank ( Lin {u}))) by B10, ThISRank4

          .= (( rank W2) + 1) by B5, LmRank0a;

          ( rank ((LIu + W2) + ( Lin {u}))) = ( rank W2) by B2, ThISRank4, C3;

          hence contradiction by C4;

        end;

        hence thesis by B1, B10, B7, ZMODUL03:def 5, BX2;

      end;

      

       A3: for n be Nat holds P[n] from NAT_1:sch 2( A1, A2);

      let W1,W2 be finite-rank free Subspace of V, v be Vector of V;

      assume ( rank (W1 /\ W2)) = ( rank W1) & ((W1 + W2) /\ ( Lin {v})) <> ( (0). V);

      hence thesis by A3;

    end;

    theorem :: ZMODUL06:69

    

     ThRankS5: for V be torsion-free Z_Module, W1,W2,W3 be finite-rank free Subspace of V st ( rank (W1 + W2)) = ( rank W2) & W3 is Subspace of W1 holds ( rank (W3 + W2)) = ( rank W2)

    proof

      let V be torsion-free Z_Module, W1,W2,W3 be finite-rank free Subspace of V such that

       A1: ( rank (W1 + W2)) = ( rank W2) & W3 is Subspace of W1;

      for v be Vector of V st v in (W3 + W2) holds v in (W1 + W2)

      proof

        let v be Vector of V such that

         B1: v in (W3 + W2);

        consider v1,v2 be Vector of V such that

         B2: v1 in W3 & v2 in W2 & v = (v1 + v2) by B1, ZMODUL01: 92;

        v1 in W1 by A1, B2, ZMODUL01: 23;

        hence thesis by B2, ZMODUL01: 92;

      end;

      then (W3 + W2) is Subspace of (W1 + W2) by ZMODUL01: 44;

      then

       A2: ( rank (W3 + W2)) <= ( rank (W1 + W2)) by ZMODUL05: 2;

      W2 is Subspace of (W3 + W2) by ZMODUL01: 97;

      then ( rank W2) <= ( rank (W3 + W2)) by ZMODUL05: 2;

      hence thesis by A1, A2, XXREAL_0: 1;

    end;

    theorem :: ZMODUL06:70

    for V be torsion-free Z_Module, W1,W2 be finite-rank free Subspace of V, I be Basis of W1 st ( rank (W1 + W2)) = ( rank W2) holds (for v be Vector of V st v in I holds ((W1 /\ W2) /\ ( Lin {v})) <> ( (0). V))

    proof

      let V be torsion-free Z_Module, W1,W2 be finite-rank free Subspace of V, I be Basis of W1 such that

       A1: ( rank (W1 + W2)) = ( rank W2);

      thus for v be Vector of V st v in I holds ((W1 /\ W2) /\ ( Lin {v})) <> ( (0). V)

      proof

        let v be Vector of V such that

         C1: v in I;

        reconsider II = I as linearly-independent Subset of V by ZMODUL03: 15, VECTSP_7:def 3;

        v in II by C1;

        then

         C2: v <> ( 0. V) by ZMODUL02: 57;

        

         C3: (W1 /\ ( Lin {v})) <> ( (0). V)

        proof

          

           D1: v in W1 by C1;

          

           D2: v in ( Lin {v}) by ZMODUL02: 65, ZFMISC_1: 31;

          v in II by C1;

          then v <> ( 0. V) by ZMODUL02: 57;

          hence thesis by D2, ZMODUL02: 66, D1, ZMODUL01: 94;

        end;

        (W2 /\ ( Lin {v})) <> ( (0). V)

        proof

          ( Lin {v}) is Subspace of ( Lin II) by ZMODUL02: 70, C1, ZFMISC_1: 31;

          then ( Lin {v}) is Subspace of ( Lin I) by ZMODUL03: 20;

          then ( Lin {v}) is Subspace of W1 by ZMODUL01: 42;

          then

           D1: ( rank (( Lin {v}) + W2)) = ( rank W2) by A1, ThRankS5;

          assume (W2 /\ ( Lin {v})) = ( (0). V);

          

          then ( rank (( Lin {v}) + W2)) = (( rank ( Lin {v})) + ( rank W2)) by ThRankDirectSum

          .= (( rank W2) + 1) by C2, LmRank0a;

          hence contradiction by D1;

        end;

        hence thesis by C3, LmISRank21;

      end;

    end;

    theorem :: ZMODUL06:71

    for V be torsion-free Z_Module, W1,W2 be finite-rank free Subspace of V st ( rank (W1 /\ W2)) = ( rank W1) holds ex a be Element of INT.Ring st (a (*) W1) is Subspace of W2

    proof

      let V be torsion-free Z_Module;

      defpred P[ Nat] means for W1,W2 be finite-rank free Subspace of V st ( rank (W1 /\ W2)) = ( rank W1) & ( rank W1) = $1 holds ex a be Element of INT.Ring st (a (*) W1) is Subspace of W2;

      

       A1: P[ 0 ]

      proof

        let W1,W2 be finite-rank free Subspace of V such that

         B1: ( rank (W1 /\ W2)) = ( rank W1) & ( rank W1) = 0 ;

        ( (Omega). W1) = ( (0). W1) by B1, ZMODUL05: 1;

        then

         B2: ( (Omega). W1) is Subspace of W2 by ZMODUL01: 55;

        take ( 1. INT.Ring );

        thus thesis by B2, Th1V;

      end;

      

       A2: for n be Nat st P[n] holds P[(n + 1)]

      proof

        let n be Nat such that

         B1: P[n];

        let W1,W2 be finite-rank free Subspace of V such that

         B2: ( rank (W1 /\ W2)) = ( rank W1) & ( rank W1) = (n + 1);

        set I = the Basis of W1;

        ( card I) > 0 by ZMODUL03:def 5, B2;

        then I <> ( {} the carrier of W1);

        then

        consider u be object such that

         B3: u in I by XBOOLE_0: 7;

        reconsider u as Vector of W1 by B3;

        reconsider uu = u as Vector of V by ZMODUL01: 25;

        

         B4: I is linearly-independent by VECTSP_7:def 3;

        reconsider II = I as linearly-independent Subset of V by ZMODUL03: 15, VECTSP_7:def 3;

        (I \ {u}) is linearly-independent by B4, XBOOLE_1: 36, ZMODUL02: 56;

        then

        reconsider Iu = (I \ {u}) as linearly-independent Subset of V by ZMODUL03: 15;

        ( (Omega). W1) = ( Lin I) by VECTSP_7:def 3

        .= ( Lin II) by ZMODUL03: 20;

        then

         B5: ( (Omega). W1) = (( Lin Iu) + ( Lin {uu})) & (( Lin Iu) /\ ( Lin {uu})) = ( (0). V) & ( Lin Iu) is free & ( Lin {uu}) is free & uu <> ( 0. V) by B3, ThLin8;

        reconsider LIu = ( Lin Iu) as finite-rank free Subspace of V;

        

         B6: Iu is Basis of LIu by ThLin7;

        

         B7: ( card Iu) = (( card I) - ( card {u})) by B3, ZFMISC_1: 31, CARD_2: 44

        .= (( rank W1) - ( card {u})) by ZMODUL03:def 5

        .= ((n + 1) - 1) by B2, CARD_1: 30

        .= n;

        for v be Vector of V st v in Iu holds ((( Lin Iu) /\ W2) /\ ( Lin {v})) <> ( (0). V)

        proof

          let v be Vector of V such that

           C1: v in Iu;

          v in I by C1, TARSKI:def 3, XBOOLE_1: 36;

          then ((W1 /\ W2) /\ ( Lin {v})) <> ( (0). V) by B2, LmISRank41;

          then (W1 /\ (W2 /\ ( Lin {v}))) <> ( (0). V) by ZMODUL01: 104;

          then

           C2: (W2 /\ ( Lin {v})) <> ( (0). V) by ZMODUL01: 107;

          

           C3: v <> ( 0. V) by C1, ZMODUL02: 57;

          

           C4: v in ( Lin {v}) by ZMODUL02: 65, ZFMISC_1: 31;

          v in LIu by C1, ZMODUL02: 65;

          then (LIu /\ ( Lin {v})) <> ( (0). V) by C3, ZMODUL02: 66, C4, ZMODUL01: 94;

          hence thesis by C2, LmISRank21;

        end;

        then ( rank (LIu /\ W2)) = ( rank LIu) by B6, ThISRank2;

        then

        consider a be Element of INT.Ring such that

         B9: (a (*) LIu) is Subspace of W2 by B1, B7, B6, ZMODUL03:def 5;

        (W2 /\ ( Lin {uu})) <> ( (0). V)

        proof

          assume (W2 /\ ( Lin {uu})) = ( (0). V);

          

          then ((W1 /\ W2) /\ ( Lin {uu})) = (W1 /\ ( (0). V)) by ZMODUL01: 104

          .= ( (0). V) by ZMODUL01: 107;

          hence contradiction by B3, B2, LmISRank41;

        end;

        then

        consider iu be Vector of V such that

         B10: iu <> ( 0. V) & (W2 /\ ( Lin {uu})) = ( Lin {iu}) by B5, LmSumMod4;

        

         B14: iu in ( Lin {iu}) by ZMODUL02: 65, ZFMISC_1: 31;

        then iu in ( Lin {uu}) by B10, ZMODUL01: 94;

        then

        consider i be Element of INT.Ring such that

         B11: iu = (i * uu) by ThLin1;

        

         B12: ((i * a) (*) W1) is Subspace of W2

        proof

          

           CX: ((i * a) (*) W1) is Subspace of V by ZMODUL01: 42;

          for v be Vector of V st v in ((i * a) (*) W1) holds v in W2

          proof

            let v be Vector of V such that

             C1: v in ((i * a) (*) W1);

            consider vw be Vector of W1 such that

             C2: v = ((i * a) * vw) by C1;

            reconsider vvw = vw as Vector of V by ZMODUL01: 25;

            vvw in ( (Omega). W1);

            then

            consider vw1,vw2 be Vector of V such that

             C3: vw1 in LIu & vw2 in ( Lin {uu}) & vvw = (vw1 + vw2) by B5, ZMODUL01: 92;

            

             C4: v = ((i * a) * vvw) by C2, ZMODUL01: 29

            .= (((i * a) * vw1) + ((i * a) * vw2)) by VECTSP_1:def 14, C3

            .= ((a * (i * vw1)) + ((i * a) * vw2)) by VECTSP_1:def 16

            .= ((a * (i * vw1)) + (a * (i * vw2))) by VECTSP_1:def 16;

            consider i2 be Element of INT.Ring such that

             C5: vw2 = (i2 * uu) by C3, ThLin1;

            

             C6: (i * vw2) = ((i * i2) * uu) by VECTSP_1:def 16, C5

            .= (i2 * iu) by B11, VECTSP_1:def 16;

            iu in W2 by B10, B14, ZMODUL01: 94;

            then (i * vw2) in W2 by C6, ZMODUL01: 37;

            then

             C7: (a * (i * vw2)) in W2 by ZMODUL01: 37;

            

             C8: (a (*) LIu) is Subspace of V by ZMODUL01: 42;

            (i * vw1) in LIu by C3, ZMODUL01: 37;

            then

            reconsider ivw1 = (i * vw1) as Vector of LIu;

            (a * ivw1) in (a * LIu);

            then (a * (i * vw1)) in (a (*) LIu) by ZMODUL01: 29;

            then (a * (i * vw1)) in W2 by B9, C8, ZMODUL01: 23;

            hence thesis by C4, C7, ZMODUL01: 36;

          end;

          hence thesis by CX, ZMODUL01: 44;

        end;

        take (i * a);

        thus thesis by B12;

      end;

      

       A3: for n be Nat holds P[n] from NAT_1:sch 2( A1, A2);

      let W1,W2 be finite-rank free Subspace of V;

      assume ( rank (W1 /\ W2)) = ( rank W1);

      hence thesis by A3;

    end;