zmodul04.miz



    begin

    reserve V for Z_Module;

    reserve W,W1,W2 for Submodule of V;

    

     Lem1: for i be Integer holds i in the carrier of INT.Ring by INT_1:def 2;

    theorem :: ZMODUL04:1

    for R be Ring holds for V be LeftMod of R, W1,W2 be Subspace of V, WW1,WW2 be Subspace of (W1 + W2) st WW1 = W1 & WW2 = W2 holds (W1 + W2) = (WW1 + WW2)

    proof

      let R be Ring;

      let V be LeftMod of R, W1,W2 be Subspace of V, WW1,WW2 be Subspace of (W1 + W2) such that

       A1: WW1 = W1 & WW2 = W2;

      

       A2: (WW1 + WW2) is Subspace of V by VECTSP_4: 26;

      for x be object holds x in (W1 + W2) iff x in (WW1 + WW2)

      proof

        let x be object;

        hereby

          assume x in (W1 + W2);

          then

          consider v1,v2 be Vector of V such that

           B2: v1 in W1 & v2 in W2 & x = (v1 + v2) by VECTSP_5: 1;

          v1 in (W1 + W2) & v2 in (W1 + W2) by B2, VECTSP_5: 2;

          then

          reconsider vv1 = v1, vv2 = v2 as Vector of (W1 + W2);

          v1 in WW1 & v2 in WW2 & x = (vv1 + vv2) by A1, B2, VECTSP_4: 13;

          hence x in (WW1 + WW2) by VECTSP_5: 1;

        end;

        assume x in (WW1 + WW2);

        then

        consider vv1,vv2 be Vector of (W1 + W2) such that

         B1: vv1 in WW1 & vv2 in WW2 & x = (vv1 + vv2) by VECTSP_5: 1;

        thus x in (W1 + W2) by B1;

      end;

      then for x be Vector of V holds x in (W1 + W2) iff x in (WW1 + WW2);

      hence thesis by A2, VECTSP_4: 30;

    end;

    theorem :: ZMODUL04:2

    for R be Ring holds for V be LeftMod of R, W1,W2 be Subspace of V, WW1,WW2 be Subspace of (W1 + W2) st WW1 = W1 & WW2 = W2 holds (W1 /\ W2) = (WW1 /\ WW2)

    proof

      let R be Ring;

      let V be LeftMod of R, W1,W2 be Subspace of V, WW1,WW2 be Subspace of (W1 + W2) such that

       A1: WW1 = W1 & WW2 = W2;

      

       A2: (WW1 /\ WW2) is Subspace of V by VECTSP_4: 26;

      for x be object holds x in (W1 /\ W2) iff x in (WW1 /\ WW2)

      proof

        let x be object;

        hereby

          assume x in (W1 /\ W2);

          then x in WW1 & x in WW2 by A1, VECTSP_5: 3;

          hence x in (WW1 /\ WW2) by VECTSP_5: 3;

        end;

        assume x in (WW1 /\ WW2);

        then x in W1 & x in W2 by A1, VECTSP_5: 3;

        hence x in (W1 /\ W2) by VECTSP_5: 3;

      end;

      then for x be Vector of V holds x in (W1 /\ W2) iff x in (WW1 /\ WW2);

      hence thesis by A2, VECTSP_4: 30;

    end;

    

     Lm19: for A,B be set st (for z be object st z in A holds ex x,y be object st z = [x, y]) & (for z be object st z in B holds ex x,y be object st z = [x, y]) & (for x,y be object holds ( [x, y] in A iff [x, y] in B)) holds A = B

    proof

      let A,B be set;

      assume that

       A1: for z be object st z in A holds ex x,y be object st z = [x, y] and

       A2: for z be object st z in B holds ex x,y be object st z = [x, y] and

       A3: for x,y be object holds [x, y] in A iff [x, y] in B;

      now

        let z be object;

        

         A4: z in B implies ex x,y be object st z = [x, y] by A2;

        z in A implies ex x,y be object st z = [x, y] by A1;

        hence z in A iff z in B by A3, A4;

      end;

      hence A = B by TARSKI: 2;

    end;

    registration

      let V be Z_Module;

      cluster [:the carrier of V, ( INT \ { 0 }):] -> non empty;

      coherence

      proof

        

         X1: 1 in INT by INT_1:def 2;

         not 1 in { 0 } by TARSKI:def 1;

        then ( INT \ { 0 }) <> {} by X1, XBOOLE_0:def 5;

        hence thesis;

      end;

    end

    definition

      let V be Z_Module;

      assume

       AS: V is Mult-cancelable;

      :: ZMODUL04:def1

      func EQRZM (V) -> Equivalence_Relation of [:the carrier of V, ( INT \ { 0 }):] means

      : defEQRZM: for S,T be object holds [S, T] in it iff (S in [:the carrier of V, ( INT \ { 0 }):] & T in [:the carrier of V, ( INT \ { 0 }):] & ex z1,z2 be Element of V, i1,i2 be Element of INT.Ring st S = [z1, i1] & T = [z2, i2] & i1 <> 0 & i2 <> 0 & (i2 * z1) = (i1 * z2));

      existence

      proof

        defpred P1[ object, object] means ex z1,z2 be Element of V, i1,i2 be Element of INT.Ring st $1 = [z1, i1] & $2 = [z2, i2] & i1 <> 0 & i2 <> 0 & (i2 * z1) = (i1 * z2);

        

         A1: for x be object st x in [:the carrier of V, ( INT \ { 0 }):] holds P1[x, x]

        proof

          let x be object;

          assume x in [:the carrier of V, ( INT \ { 0 }):];

          then

          consider z1,i1 be object such that

           A11: z1 in the carrier of V & i1 in ( INT \ { 0 }) & x = [z1, i1] by ZFMISC_1:def 2;

          reconsider z1 as Element of V by A11;

          

           A12: i1 in INT & not i1 in { 0 } by XBOOLE_0:def 5, A11;

          reconsider i1 as Integer by A11;

          reconsider i1 as Element of INT.Ring by A11;

          i1 <> 0 & i1 <> 0 & (i1 * z1) = (i1 * z1) by A12, TARSKI:def 1;

          hence P1[x, x] by A11;

        end;

        

         A2: for x,y be object st P1[x, y] holds P1[y, x];

        

         A3: for x,y,z be object st P1[x, y] & P1[y, z] holds P1[x, z]

        proof

          let x,y,z be object;

          assume

           A31: P1[x, y] & P1[y, z];

          then

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

           A32: x = [z1, i1] & y = [z2, i2] & i1 <> 0 & i2 <> 0 & (i2 * z1) = (i1 * z2);

          consider z3,z4 be Element of V, i3,i4 be Element of INT.Ring such that

           A33: y = [z3, i3] & z = [z4, i4] & i3 <> 0 & i4 <> 0 & (i4 * z3) = (i3 * z4) by A31;

          

           A34: z2 = z3 & i2 = i3 by A32, A33, XTUPLE_0: 1;

          (i2 * (i4 * z1)) = ((i2 * i4) * z1) by VECTSP_1:def 16

          .= ((i4 * i2) * z1)

          .= (i4 * (i2 * z1)) by VECTSP_1:def 16

          .= (i4 * (i1 * z2)) by A32

          .= ((i4 * i1) * z2) by VECTSP_1:def 16

          .= ((i1 * i4) * z2)

          .= (i1 * (i4 * z2)) by VECTSP_1:def 16

          .= ((i1 * i2) * z4) by A33, A34, VECTSP_1:def 16

          .= ((i2 * i1) * z4)

          .= (i2 * (i1 * z4)) by VECTSP_1:def 16;

          hence P1[x, z] by AS, A32, A33, ZMODUL01: 10;

        end;

        consider EqR be Equivalence_Relation of [:the carrier of V, ( INT \ { 0 }):] such that

         A4: for x,y be object holds [x, y] in EqR iff (x in [:the carrier of V, ( INT \ { 0 }):] & y in [:the carrier of V, ( INT \ { 0 }):] & P1[x, y]) from EQREL_1:sch 1( A1, A2, A3);

        take EqR;

        thus thesis by A4;

      end;

      uniqueness

      proof

        let EqR1,EqR2 be Equivalence_Relation of [:the carrier of V, ( INT \ { 0 }):];

        assume

         A1: for S,T be object holds ( [S, T] in EqR1 iff (S in [:the carrier of V, ( INT \ { 0 }):] & T in [:the carrier of V, ( INT \ { 0 }):] & ex z1,z2 be Element of V, i1,i2 be Element of INT.Ring st S = [z1, i1] & T = [z2, i2] & i1 <> 0 & i2 <> 0 & (i2 * z1) = (i1 * z2)));

        assume

         A2: for S,T be object holds [S, T] in EqR2 iff (S in [:the carrier of V, ( INT \ { 0 }):] & T in [:the carrier of V, ( INT \ { 0 }):] & ex z1,z2 be Element of V, i1,i2 be Element of INT.Ring st S = [z1, i1] & T = [z2, i2] & i1 <> 0 & i2 <> 0 & (i2 * z1) = (i1 * z2));

        

         A3: for z be object st z in EqR1 holds ex x,y be object st z = [x, y] by RELAT_1:def 1;

        

         A4: for z be object st z in EqR2 holds ex x,y be object st z = [x, y] by RELAT_1:def 1;

        for x,y be object holds [x, y] in EqR1 iff [x, y] in EqR2

        proof

          let S,T be object;

           [S, T] in EqR2 iff (S in [:the carrier of V, ( INT \ { 0 }):] & T in [:the carrier of V, ( INT \ { 0 }):] & ex z1,z2 be Element of V, i1,i2 be Element of INT.Ring st S = [z1, i1] & T = [z2, i2] & i1 <> 0 & i2 <> 0 & (i2 * z1) = (i1 * z2)) by A2;

          hence thesis by A1;

        end;

        hence EqR1 = EqR2 by Lm19, A3, A4;

      end;

    end

    theorem :: ZMODUL04:3

    

     LMEQR001: for V be Z_Module, z1,z2 be Element of V, i1,i2 be Element of INT.Ring st V is Mult-cancelable holds [ [z1, i1], [z2, i2]] in ( EQRZM V) iff i1 <> 0 & i2 <> 0 & (i2 * z1) = (i1 * z2)

    proof

      let V be Z_Module, z1,z2 be Element of V, i1,i2 be Element of INT.Ring ;

      assume

       AS: V is Mult-cancelable;

      hereby

        assume [ [z1, i1], [z2, i2]] in ( EQRZM V);

        then

        consider zz1,zz2 be Element of V, ii1,ii2 be Element of INT.Ring such that

         P2: [z1, i1] = [zz1, ii1] & [z2, i2] = [zz2, ii2] & ii1 <> 0 & ii2 <> 0 & (ii2 * zz1) = (ii1 * zz2) by AS, defEQRZM;

        z1 = zz1 & i1 = ii1 & z2 = zz2 & i2 = ii2 by P2, XTUPLE_0: 1;

        hence i1 <> 0 & i2 <> 0 & (i2 * z1) = (i1 * z2) by P2;

      end;

      assume

       A2: i1 <> 0 & i2 <> 0 & (i2 * z1) = (i1 * z2);

      then

       A21: not i1 in { 0 } & not i2 in { 0 } by TARSKI:def 1;

      i1 in ( INT \ { 0 }) & i2 in ( INT \ { 0 }) by XBOOLE_0:def 5, A21;

      then [z1, i1] in [:the carrier of V, ( INT \ { 0 }):] & [z2, i2] in [:the carrier of V, ( INT \ { 0 }):] by ZFMISC_1: 87;

      hence [ [z1, i1], [z2, i2]] in ( EQRZM V) by A2, AS, defEQRZM;

    end;

    definition

      let V be Z_Module;

      assume

       AS: V is Mult-cancelable;

      :: ZMODUL04:def2

      func addCoset (V) -> BinOp of ( Class ( EQRZM V)) means

      : DefaddCoset: for A,B be object st A in ( Class ( EQRZM V)) & B in ( Class ( EQRZM V)) holds for z1,z2 be Element of V, i1,i2 be Element of INT.Ring st i1 <> ( 0. INT.Ring ) & i2 <> ( 0. INT.Ring ) & A = ( Class (( EQRZM V), [z1, i1])) & B = ( Class (( EQRZM V), [z2, i2])) holds (it . (A,B)) = ( Class (( EQRZM V), [((i2 * z1) + (i1 * z2)), (i1 * i2)]));

      existence

      proof

        defpred P[ object, object, object] means for z1,z2 be Element of V, i1,i2 be Element of INT.Ring st i1 <> 0 & i2 <> 0 & $1 = ( Class (( EQRZM V), [z1, i1])) & $2 = ( Class (( EQRZM V), [z2, i2])) holds $3 = ( Class (( EQRZM V), [((i2 * z1) + (i1 * z2)), (i1 * i2)]));

        set C = ( Class ( EQRZM V));

         A1:

        now

          let A,B be object;

          assume

           A10: A in C & B in C;

          then

          consider A1 be object such that

           A2: A1 in [:the carrier of V, ( INT \ { 0 }):] & A = ( Class (( EQRZM V),A1)) by EQREL_1:def 3;

          consider z1,i1 be object such that

           A3: z1 in the carrier of V & i1 in ( INT \ { 0 }) & A1 = [z1, i1] by A2, ZFMISC_1:def 2;

          reconsider z1 as Element of V by A3;

          i1 in INT & not i1 in { 0 } by XBOOLE_0:def 5, A3;

          then

           A31: i1 in INT & i1 <> 0 by TARSKI:def 1;

          reconsider i1 as Integer by A3;

          reconsider i1 as Element of INT.Ring by A3;

          consider B1 be object such that

           A4: B1 in [:the carrier of V, ( INT \ { 0 }):] & B = ( Class (( EQRZM V),B1)) by A10, EQREL_1:def 3;

          consider z2,i2 be object such that

           A5: z2 in the carrier of V & i2 in ( INT \ { 0 }) & B1 = [z2, i2] by A4, ZFMISC_1:def 2;

          reconsider z2 as Element of V by A5;

          i2 in INT & not i2 in { 0 } by XBOOLE_0:def 5, A5;

          then

           A51: i2 in INT & i2 <> 0 by TARSKI:def 1;

          reconsider i2 as Integer by A5;

          reconsider i2 as Element of INT.Ring by A5;

          

           A61: not (i1 * i2) in { 0 } by A31, A51, TARSKI:def 1;

          (i1 * i2) in ( INT \ { 0 }) by XBOOLE_0:def 5, A61;

          then

           X1: [((i2 * z1) + (i1 * z2)), (i1 * i2)] in [:the carrier of V, ( INT \ { 0 }):] by ZFMISC_1: 87;

          set z = ( Class (( EQRZM V), [((i2 * z1) + (i1 * z2)), (i1 * i2)]));

          

           A7: z in C by X1, EQREL_1:def 3;

           P[A, B, z]

          proof

            let zz1,zz2 be Element of V, ii1,ii2 be Element of INT.Ring ;

            assume

             A71: ii1 <> 0 & ii2 <> 0 & A = ( Class (( EQRZM V), [zz1, ii1])) & B = ( Class (( EQRZM V), [zz2, ii2]));

            then

             A72: not ii1 in { 0 } by TARSKI:def 1;

            ii1 in ( INT \ { 0 }) by XBOOLE_0:def 5, A72;

            then

             X2: [zz1, ii1] in [:the carrier of V, ( INT \ { 0 }):] by ZFMISC_1: 87;

            

             X21: not ii2 in { 0 } by TARSKI:def 1, A71;

            ii2 in ( INT \ { 0 }) by XBOOLE_0:def 5, X21;

            then

             X3: [zz2, ii2] in [:the carrier of V, ( INT \ { 0 }):] by ZFMISC_1: 87;

            

             X5: [ [zz1, ii1], [z1, i1]] in ( EQRZM V) by X2, A2, A3, A71, EQREL_1: 35;

            then

             XX5: ii1 <> 0 & i1 <> 0 & (i1 * zz1) = (ii1 * z1) by LMEQR001, AS;

            

             X7: [ [zz2, ii2], [z2, i2]] in ( EQRZM V) by X3, A4, A5, A71, EQREL_1: 35;

            then

             XX7: ii2 <> 0 & i2 <> 0 & (i2 * zz2) = (ii2 * z2) by LMEQR001, AS;

            ((ii1 * ii2) * ((i2 * z1) + (i1 * z2))) = (((ii1 * ii2) * (i2 * z1)) + ((ii1 * ii2) * (i1 * z2))) by VECTSP_1:def 14

            .= ((((ii1 * ii2) * i2) * z1) + ((ii1 * ii2) * (i1 * z2))) by VECTSP_1:def 16

            .= ((((ii2 * i2) * ii1) * z1) + (((ii1 * ii2) * i1) * z2)) by VECTSP_1:def 16

            .= (((ii2 * i2) * (ii1 * z1)) + (((ii1 * i1) * ii2) * z2)) by VECTSP_1:def 16

            .= (((ii2 * i2) * (ii1 * z1)) + ((ii1 * i1) * (ii2 * z2))) by VECTSP_1:def 16

            .= (((ii2 * i2) * (i1 * zz1)) + ((ii1 * i1) * (ii2 * z2))) by AS, X5, LMEQR001

            .= (((ii2 * i2) * (i1 * zz1)) + ((ii1 * i1) * (i2 * zz2))) by AS, X7, LMEQR001

            .= ((((ii2 * i2) * i1) * zz1) + ((ii1 * i1) * (i2 * zz2))) by VECTSP_1:def 16

            .= ((((i2 * i1) * ii2) * zz1) + (((ii1 * i1) * i2) * zz2)) by VECTSP_1:def 16

            .= (((i1 * i2) * (ii2 * zz1)) + (((i1 * i2) * ii1) * zz2)) by VECTSP_1:def 16

            .= (((i1 * i2) * (ii2 * zz1)) + ((i1 * i2) * (ii1 * zz2))) by VECTSP_1:def 16

            .= ((i1 * i2) * ((ii2 * zz1) + (ii1 * zz2))) by VECTSP_1:def 14;

            then [ [((i2 * z1) + (i1 * z2)), (i1 * i2)], [((ii2 * zz1) + (ii1 * zz2)), (ii1 * ii2)]] in ( EQRZM V) by XX5, XX7, LMEQR001, AS;

            hence thesis by X1, EQREL_1: 35;

          end;

          hence ex z be object st z in C & P[A, B, z] by A7;

        end;

        consider f be Function of [:C, C:], C such that

         A14: for A,B be object st A in C & B in C holds P[A, B, (f . (A,B))] from BINOP_1:sch 1( A1);

        reconsider f as BinOp of C;

        take f;

        thus thesis by A14;

      end;

      uniqueness

      proof

        defpred P[ object, object, object] means for z1,z2 be Element of V, i1,i2 be Element of INT.Ring st i1 <> ( 0. INT.Ring ) & i2 <> ( 0. INT.Ring ) & $1 = ( Class (( EQRZM V), [z1, i1])) & $2 = ( Class (( EQRZM V), [z2, i2])) holds $3 = ( Class (( EQRZM V), [((i2 * z1) + (i1 * z2)), (i1 * i2)]));

        set C = ( Class ( EQRZM V));

        let f1,f2 be BinOp of C such that

         A15: for A,B be object st A in C & B in C holds P[A, B, (f1 . (A,B))] and

         A16: for A,B be object st A in C & B in C holds P[A, B, (f2 . (A,B))];

        now

          let A,B be set;

          assume

           X0: A in C & B in C;

          then

          consider A1 be object such that

           A2: A1 in [:the carrier of V, ( INT \ { 0 }):] & A = ( Class (( EQRZM V),A1)) by EQREL_1:def 3;

          consider z1,i1 be object such that

           A3: z1 in the carrier of V & i1 in ( INT \ { 0 }) & A1 = [z1, i1] by A2, ZFMISC_1:def 2;

          reconsider z1 as Element of V by A3;

          i1 in INT & not i1 in { 0 } by XBOOLE_0:def 5, A3;

          then

           A31: i1 in INT & i1 <> 0 by TARSKI:def 1;

          reconsider i1 as Integer by A3;

          consider B1 be object such that

           A4: B1 in [:the carrier of V, ( INT \ { 0 }):] & B = ( Class (( EQRZM V),B1)) by X0, EQREL_1:def 3;

          consider z2,i2 be object such that

           A5: z2 in the carrier of V & i2 in ( INT \ { 0 }) & B1 = [z2, i2] by A4, ZFMISC_1:def 2;

          reconsider z2 as Element of V by A5;

          i2 in INT & not i2 in { 0 } by XBOOLE_0:def 5, A5;

          then

           A51: i2 in INT & i2 <> 0 by TARSKI:def 1;

          reconsider i2 as Integer by A5;

          reconsider i1, i2 as Element of INT.Ring by Lem1;

          

          thus (f1 . (A,B)) = ( Class (( EQRZM V), [((i2 * z1) + (i1 * z2)), (i1 * i2)])) by A2, A3, A4, A5, A15, A31, A51, X0

          .= (f2 . (A,B)) by A2, A3, A4, A5, A16, A31, A51, X0;

        end;

        hence thesis by BINOP_1: 1;

      end;

    end

    definition

      let V be Z_Module;

      assume

       AS: V is Mult-cancelable;

      :: ZMODUL04:def3

      func zeroCoset (V) -> Element of ( Class ( EQRZM V)) means

      : defZero: for i be Integer st i <> 0 holds it = ( Class (( EQRZM V), [( 0. V), i]));

      existence

      proof

        

         X1: 1 in INT by INT_1:def 2;

         not 1 in { 0 } by TARSKI:def 1;

        then 1 in ( INT \ { 0 }) by XBOOLE_0:def 5, X1;

        then [( 0. V), 1] in [:the carrier of V, ( INT \ { 0 }):] by ZFMISC_1: 87;

        then

        reconsider z = ( Class (( EQRZM V), [( 0. V), 1])) as Element of ( Class ( EQRZM V)) by EQREL_1:def 3;

        take z;

        for i be Integer st i <> 0 holds z = ( Class (( EQRZM V), [( 0. V), i]))

        proof

          let i be Integer;

          assume

           X2: i <> 0 ;

          then

           X21: not i in { 0 } by TARSKI:def 1;

          

           Z1: i in INT by INT_1:def 2;

          then i in ( INT \ { 0 }) by XBOOLE_0:def 5, X21;

          then

           X3: [( 0. V), i] in [:the carrier of V, ( INT \ { 0 }):] by ZFMISC_1: 87;

          reconsider i as Element of INT.Ring by Z1;

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

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

          then [ [( 0. V), i], [( 0. V), 1]] in ( EQRZM V) by AS, X2, LMEQR001;

          hence thesis by X3, EQREL_1: 35;

        end;

        hence thesis;

      end;

      uniqueness

      proof

        let z1,z2 be Element of ( Class ( EQRZM V));

        assume

         AS1: for i be Integer st i <> 0 holds z1 = ( Class (( EQRZM V), [( 0. V), i]));

        assume

         AS2: for i be Integer st i <> 0 holds z2 = ( Class (( EQRZM V), [( 0. V), i]));

        

        thus z1 = ( Class (( EQRZM V), [( 0. V), 1])) by AS1

        .= z2 by AS2;

      end;

    end

    definition

      let V be Z_Module;

      assume

       AS: V is Mult-cancelable;

      :: ZMODUL04:def4

      func lmultCoset (V) -> Function of [:the carrier of F_Rat , ( Class ( EQRZM V)):], ( Class ( EQRZM V)) means

      : DeflmultCoset: for q be object, A be object st q in RAT & A in ( Class ( EQRZM V)) holds for m,n,i be Integer, mm be Element of INT.Ring , z be Element of V st m = mm & n <> 0 & q = (m / n) & i <> 0 & A = ( Class (( EQRZM V), [z, i])) holds (it . (q,A)) = ( Class (( EQRZM V), [(mm * z), (n * i)]));

      existence

      proof

        defpred P[ object, object, object] means for m,n,i be Integer, mm be Element of INT.Ring , z be Element of V st mm = m & n <> 0 & $1 = (m / n) & i <> 0 & $2 = ( Class (( EQRZM V), [z, i])) holds $3 = ( Class (( EQRZM V), [(mm * z), (n * i)]));

        set cF = RAT ;

        set C = ( Class ( EQRZM V));

         A1:

        now

          let q,A be object;

          assume

           AS0: q in RAT & A in C;

          then

          consider A1 be object such that

           A2: A1 in [:the carrier of V, ( INT \ { 0 }):] & A = ( Class (( EQRZM V),A1)) by EQREL_1:def 3;

          consider z,i be object such that

           A3: z in the carrier of V & i in ( INT \ { 0 }) & A1 = [z, i] by A2, ZFMISC_1:def 2;

          reconsider z as Element of V by A3;

          i in INT & not i in { 0 } by XBOOLE_0:def 5, A3;

          then

           A31: i in INT & i <> 0 by TARSKI:def 1;

          reconsider i as Integer by A3;

          consider m,n be Integer such that

           A4: n <> 0 & q = (m / n) by AS0, RAT_1: 1;

          reconsider I = i, mn = m, no = n as Element of INT.Ring by Lem1;

          

           A61: not (no * i) in { 0 } by A31, A4, TARSKI:def 1;

          (no * i) in INT by INT_1:def 2;

          then (no * i) in ( INT \ { 0 }) by XBOOLE_0:def 5, A61;

          then

           X1: [(mn * z), (no * i)] in [:the carrier of V, ( INT \ { 0 }):] by ZFMISC_1: 87;

          set w = ( Class (( EQRZM V), [(mn * z), (no * i)]));

          

           A7: w in C by X1, EQREL_1:def 3;

           P[q, A, w]

          proof

            let mm,nn,ii be Integer, m1 be Element of INT.Ring , zz be Element of V;

            assume

             A71: m1 = mm & nn <> 0 & q = (mm / nn) & ii <> 0 & A = ( Class (( EQRZM V), [zz, ii]));

            then

             A72: not ii in { 0 } by TARSKI:def 1;

            ii in INT by INT_1:def 2;

            then ii in ( INT \ { 0 }) by XBOOLE_0:def 5, A72;

            then

             X2: [zz, ii] in [:the carrier of V, ( INT \ { 0 }):] by ZFMISC_1: 87;

            reconsider i2 = ii, n1 = nn as Element of INT.Ring by INT_1:def 2;

            

             X51: [ [zz, i2], [z, I]] in ( EQRZM V) by X2, A2, A3, A71, EQREL_1: 35;

            ((n1 * i2) * (mn * z)) = (((n1 * i2) * mn) * z) by VECTSP_1:def 16

            .= (((n1 * mn) * i2) * z)

            .= ((n1 * mn) * (i2 * z)) by VECTSP_1:def 16

            .= ((n1 * mn) * (I * zz)) by AS, X51, LMEQR001

            .= ((no * m1) * (I * zz)) by A4, A71, XCMPLX_1: 95

            .= (((no * m1) * I) * zz) by VECTSP_1:def 16

            .= (((no * I) * m1) * zz)

            .= ((no * I) * (m1 * zz)) by VECTSP_1:def 16;

            then [ [(mn * z), (no * I)], [(m1 * zz), (n1 * i2)]] in ( EQRZM V) by A31, A4, A71, LMEQR001, AS;

            hence thesis by X1, EQREL_1: 35;

          end;

          hence ex w be object st w in C & P[q, A, w] by A7;

        end;

        consider f be Function of [: RAT , C:], C such that

         A14: for q,A be object st q in RAT & A in C holds P[q, A, (f . (q,A))] from BINOP_1:sch 1( A1);

        reconsider f as Function of [:the carrier of F_Rat , C:], C;

        take f;

        thus thesis by A14;

      end;

      uniqueness

      proof

        set cF = the carrier of F_Rat ;

        set C = ( Class ( EQRZM V));

        let f1,f2 be Function of [:cF, C:], C;

        assume

         A7: for q,A be object st q in RAT & A in ( Class ( EQRZM V)) holds for m,n,i be Integer, mm be Element of INT.Ring , z be Element of V st mm = m & n <> 0 & q = (m / n) & i <> 0 & A = ( Class (( EQRZM V), [z, i])) holds (f1 . (q,A)) = ( Class (( EQRZM V), [(mm * z), (n * i)]));

        assume

         A8: for q be object, A be object st q in RAT & A in ( Class ( EQRZM V)) holds for m,n,i be Integer, mm be Element of INT.Ring , z be Element of V st mm = m & n <> 0 & q = (m / n) & i <> 0 & A = ( Class (( EQRZM V), [z, i])) holds (f2 . (q,A)) = ( Class (( EQRZM V), [(mm * z), (n * i)]));

        now

          let q,A be object;

          assume

           AS0: q in RAT & A in C;

          then

          consider A1 be object such that

           A2: A1 in [:the carrier of V, ( INT \ { 0 }):] & A = ( Class (( EQRZM V),A1)) by EQREL_1:def 3;

          consider z,i be object such that

           A3: z in the carrier of V & i in ( INT \ { 0 }) & A1 = [z, i] by A2, ZFMISC_1:def 2;

          reconsider z as Element of V by A3;

          i in INT & not i in { 0 } by XBOOLE_0:def 5, A3;

          then

           A31: i in INT & i <> 0 by TARSKI:def 1;

          reconsider i as Integer by A3;

          consider m,n be Integer such that

           A4: n <> 0 & q = (m / n) by AS0, RAT_1: 1;

          reconsider m, i, n as Element of INT.Ring by Lem1;

          i <> ( 0. INT.Ring ) by A31;

          

          hence (f1 . (q,A)) = ( Class (( EQRZM V), [(m * z), (n * i)])) by AS0, A2, A3, A4, A7

          .= (f2 . (q,A)) by AS0, A2, A3, A4, A8, A31;

        end;

        then for q be Element of F_Rat , A be Element of C holds (f1 . (q,A)) = (f2 . (q,A));

        hence thesis by BINOP_1: 2;

      end;

    end

    theorem :: ZMODUL04:4

    

     LMEQR003: for V be Z_Module, z be Element of V, i,n be Element of INT.Ring st i <> ( 0. INT.Ring ) & n <> ( 0. INT.Ring ) & V is Mult-cancelable holds ( Class (( EQRZM V), [z, i])) = ( Class (( EQRZM V), [(n * z), (n * i)]))

    proof

      let V be Z_Module, z be Element of V, i,n be Element of INT.Ring ;

      assume

       AS: i <> ( 0. INT.Ring ) & n <> ( 0. INT.Ring ) & V is Mult-cancelable;

      then

       B61: not i in { 0 } by TARSKI:def 1;

      i in ( INT \ { 0 }) by XBOOLE_0:def 5, B61;

      then

       X1: [z, i] in [:the carrier of V, ( INT \ { 0 }):] by ZFMISC_1: 87;

      ((n * i) * z) = ((i * n) * z)

      .= (i * (n * z)) by VECTSP_1:def 16;

      then [ [z, i], [(n * z), (n * i)]] in ( EQRZM V) by AS, LMEQR001;

      hence ( Class (( EQRZM V), [z, i])) = ( Class (( EQRZM V), [(n * z), (n * i)])) by X1, EQREL_1: 35;

    end;

    theorem :: ZMODUL04:5

    

     LMEQRZM1: for V be Z_Module, v be Element of ModuleStr (# ( Class ( EQRZM V)), ( addCoset V), ( zeroCoset V), ( lmultCoset V) #) st V is Mult-cancelable holds ex i be Element of INT.Ring , z be Element of V st i <> ( 0. INT.Ring ) & v = ( Class (( EQRZM V), [z, i]))

    proof

      let V be Z_Module, v be Element of ModuleStr (# ( Class ( EQRZM V)), ( addCoset V), ( zeroCoset V), ( lmultCoset V) #);

      assume V is Mult-cancelable;

      v in ( Class ( EQRZM V));

      then

      consider A1 be object such that

       A1: A1 in [:the carrier of V, ( INT \ { 0 }):] & v = ( Class (( EQRZM V),A1)) by EQREL_1:def 3;

      consider z,i be object such that

       A2: z in the carrier of V & i in ( INT \ { 0 }) & A1 = [z, i] by A1, ZFMISC_1:def 2;

      reconsider z as Element of V by A2;

      

       A31: i in INT & not i in { 0 } by XBOOLE_0:def 5, A2;

      reconsider i as Integer by A2;

      reconsider i as Element of INT.Ring by A2;

      take i, z;

      thus i <> ( 0. INT.Ring ) & v = ( Class (( EQRZM V), [z, i])) by A1, A2, A31, TARSKI:def 1;

    end;

    

     ThEQRZMV1: for V be Z_Module st V is Mult-cancelable holds ModuleStr (# ( Class ( EQRZM V)), ( addCoset V), ( zeroCoset V), ( lmultCoset V) #) is VectSp of F_Rat

    proof

      let V be Z_Module;

      assume

       AS: V is Mult-cancelable;

      reconsider IT = ModuleStr (# ( Class ( EQRZM V)), ( addCoset V), ( zeroCoset V), ( lmultCoset V) #) as non empty ModuleStr over F_Rat ;

      set F = F_Rat ;

      set AD = ( addCoset V);

      set ML = ( lmultCoset V);

      

       P1: for x be Element of F holds for v,w be Element of IT holds (x * (v + w)) = ((x * v) + (x * w))

      proof

        let x be Element of F, v,w be Element of IT;

        consider i be Element of INT.Ring , z be Element of V such that

         X1: i <> 0 & v = ( Class (( EQRZM V), [z, i])) by AS, LMEQRZM1;

        consider j be Element of INT.Ring , y be Element of V such that

         X2: j <> 0 & w = ( Class (( EQRZM V), [y, j])) by AS, LMEQRZM1;

        consider m,n be Integer such that

         X3: n <> 0 & x = (m / n) by RAT_1: 1;

        reconsider m, n as Element of INT.Ring by Lem1;

        

         X5: (v + w) = ( Class (( EQRZM V), [((j * z) + (i * y)), (i * j)])) by X1, X2, DefaddCoset, AS;

        

         X7: (x * v) = ( Class (( EQRZM V), [(m * z), (n * i)])) by DeflmultCoset, AS, X1, X3;

        

         X8: (x * w) = ( Class (( EQRZM V), [(m * y), (n * j)])) by DeflmultCoset, AS, X2, X3;

        

         X11: (((n * j) * (m * z)) + ((n * i) * (m * y))) = ((((n * j) * m) * z) + ((n * i) * (m * y))) by VECTSP_1:def 16

        .= ((((n * m) * j) * z) + (((n * i) * m) * y)) by VECTSP_1:def 16

        .= (((n * m) * (j * z)) + (((n * m) * i) * y)) by VECTSP_1:def 16

        .= (((n * m) * (j * z)) + ((n * m) * (i * y))) by VECTSP_1:def 16

        .= ((n * (m * (j * z))) + ((n * m) * (i * y))) by VECTSP_1:def 16

        .= ((n * (m * (j * z))) + (n * (m * (i * y)))) by VECTSP_1:def 16

        .= (n * ((m * (j * z)) + (m * (i * y)))) by VECTSP_1:def 14

        .= (n * (m * ((j * z) + (i * y)))) by VECTSP_1:def 14;

        ((x * v) + (x * w)) = ( Class (( EQRZM V), [(((n * j) * (m * z)) + ((n * i) * (m * y))), ((n * i) * (n * j))])) by X1, X2, X3, X7, X8, DefaddCoset, AS

        .= ( Class (( EQRZM V), [(n * (m * ((j * z) + (i * y)))), (n * (n * (i * j)))])) by X11

        .= ( Class (( EQRZM V), [(m * ((j * z) + (i * y))), (n * (i * j))])) by AS, X1, X2, X3, LMEQR003;

        hence (x * (v + w)) = ((x * v) + (x * w)) by DeflmultCoset, AS, X1, X2, X3, X5;

      end;

      

       P2: for x,y be Element of F holds for v be Element of IT holds ((x + y) * v) = ((x * v) + (y * v))

      proof

        let x,y be Element of F, v be Element of IT;

        consider i be Element of INT.Ring , z be Element of V such that

         X1: i <> 0 & v = ( Class (( EQRZM V), [z, i])) by AS, LMEQRZM1;

        consider m,n be Integer such that

         X3: n <> 0 & x = (m / n) by RAT_1: 1;

        consider l,k be Integer such that

         Y3: k <> 0 & y = (l / k) by RAT_1: 1;

        

         Y4: (x + y) = ((m / n) + (l / k)) by X3, Y3

        .= (((k * m) + (n * l)) / (n * k)) by XCMPLX_1: 116, X3, Y3;

        reconsider l, k, m, n as Element of INT.Ring by Lem1;

        

         X7: (x * v) = ( Class (( EQRZM V), [(m * z), (n * i)])) by DeflmultCoset, AS, X1, X3;

        

         X8: (y * v) = ( Class (( EQRZM V), [(l * z), (k * i)])) by DeflmultCoset, AS, X1, Y3;

        

         X11: (((k * i) * (m * z)) + ((n * i) * (l * z))) = ((((k * i) * m) * z) + ((n * i) * (l * z))) by VECTSP_1:def 16

        .= (((i * (k * m)) * z) + (((i * n) * l) * z)) by VECTSP_1:def 16

        .= ((i * ((k * m) * z)) + ((i * (n * l)) * z)) by VECTSP_1:def 16

        .= ((i * ((k * m) * z)) + (i * ((n * l) * z))) by VECTSP_1:def 16

        .= (i * (((k * m) * z) + ((n * l) * z))) by VECTSP_1:def 14

        .= (i * (((k * m) + (n * l)) * z)) by VECTSP_1:def 15;

        ((x * v) + (y * v)) = ( Class (( EQRZM V), [(((k * i) * (m * z)) + ((n * i) * (l * z))), ((n * i) * (k * i))])) by X1, X3, X7, X8, Y3, DefaddCoset, AS

        .= ( Class (( EQRZM V), [(i * (((k * m) + (n * l)) * z)), (i * ((n * k) * i))])) by X11

        .= ( Class (( EQRZM V), [(((k * m) + (n * l)) * z), ((n * k) * i)])) by AS, X1, X3, Y3, LMEQR003;

        hence ((x + y) * v) = ((x * v) + (y * v)) by DeflmultCoset, AS, X1, X3, Y3, Y4;

      end;

      

       P3: for x,y be Element of F holds for v be Element of IT holds ((x * y) * v) = (x * (y * v))

      proof

        let x,y be Element of F, v be Element of IT;

        consider i be Element of INT.Ring , z be Element of V such that

         X1: i <> 0 & v = ( Class (( EQRZM V), [z, i])) by AS, LMEQRZM1;

        consider m,n be Integer such that

         X3: n <> 0 & x = (m / n) by RAT_1: 1;

        consider l,k be Integer such that

         Y3: k <> 0 & y = (l / k) by RAT_1: 1;

        reconsider mm = m, nn = n, ll = l, kk = k as Element of INT.Ring by Lem1;

        

         Y4: (x * y) = ((m / n) * (l / k)) by X3, Y3

        .= ((m * l) / (n * k)) by XCMPLX_1: 76;

        

         X8: (y * v) = ( Class (( EQRZM V), [(ll * z), (kk * i)])) by DeflmultCoset, AS, X1, Y3;

        (x * (y * v)) = ( Class (( EQRZM V), [(mm * (ll * z)), (nn * (kk * i))])) by DeflmultCoset, AS, X1, X3, X8, Y3

        .= ( Class (( EQRZM V), [((mm * ll) * z), ((nn * kk) * i)])) by VECTSP_1:def 16;

        hence ((x * y) * v) = (x * (y * v)) by DeflmultCoset, AS, X1, X3, Y3, Y4;

      end;

      

       P4: for v be Element of IT holds (( 1. F) * v) = v

      proof

        let v be Element of IT;

        set i1 = ( 1. INT.Ring );

        reconsider ii1 = i1 as Integer;

        consider i be Element of INT.Ring , z be Element of V such that

         X1: i <> 0 & v = ( Class (( EQRZM V), [z, i])) by AS, LMEQRZM1;

        

         X2: ( 1. F) = 1

        .= (ii1 / ii1);

        

        thus (( 1. F) * v) = ( Class (( EQRZM V), [(i1 * z), (i1 * i)])) by DeflmultCoset, AS, X1, X2

        .= v by X1, VECTSP_1:def 17;

      end;

      

       P5: for v be Element of IT holds v is right_complementable

      proof

        let v be Element of IT;

        consider i be Element of INT.Ring , z be Element of V such that

         X1: i <> 0 & v = ( Class (( EQRZM V), [z, i])) by AS, LMEQRZM1;

        

         X21: not ( - i) in { 0 } by X1, TARSKI:def 1;

        ( - i) in ( INT \ { 0 }) by XBOOLE_0:def 5, X21;

        then [z, ( - i)] in [:the carrier of V, ( INT \ { 0 }):] by ZFMISC_1: 87;

        then

        reconsider w = ( Class (( EQRZM V), [z, ( - i)])) as Element of IT by EQREL_1:def 3;

        

         X3: ((( - i) * z) + (i * z)) = ((( - i) + i) * z) by VECTSP_1:def 15

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

        (v + w) = ( Class (( EQRZM V), [((( - i) * z) + (i * z)), (i * ( - i))])) by X1, DefaddCoset, AS

        .= ( 0. IT) by AS, X1, X3, defZero;

        hence v is right_complementable by ALGSTR_0:def 11;

      end;

      

       P6: for v,w be Element of IT holds (v + w) = (w + v)

      proof

        let v,w be Element of IT;

        consider i be Element of INT.Ring , z be Element of V such that

         X1: i <> 0 & v = ( Class (( EQRZM V), [z, i])) by AS, LMEQRZM1;

        consider j be Element of INT.Ring , y be Element of V such that

         X2: j <> 0 & w = ( Class (( EQRZM V), [y, j])) by AS, LMEQRZM1;

        (v + w) = ( Class (( EQRZM V), [((j * z) + (i * y)), (i * j)])) by X1, X2, DefaddCoset, AS;

        hence (v + w) = (w + v) by AS, X1, X2, DefaddCoset;

      end;

      

       P7: for u,v,w be Element of IT holds ((u + v) + w) = (u + (v + w))

      proof

        let u,v,w be Element of IT;

        consider k be Element of INT.Ring , s be Element of V such that

         X0: k <> 0 & u = ( Class (( EQRZM V), [s, k])) by AS, LMEQRZM1;

        consider i be Element of INT.Ring , z be Element of V such that

         X1: i <> 0 & v = ( Class (( EQRZM V), [z, i])) by AS, LMEQRZM1;

        consider j be Element of INT.Ring , y be Element of V such that

         X2: j <> 0 & w = ( Class (( EQRZM V), [y, j])) by AS, LMEQRZM1;

        

         X3: (u + v) = ( Class (( EQRZM V), [((i * s) + (k * z)), (k * i)])) by X0, X1, DefaddCoset, AS;

        

         X4: ((u + v) + w) = ( Class (( EQRZM V), [((j * ((i * s) + (k * z))) + ((k * i) * y)), ((k * i) * j)])) by X0, X1, X2, X3, DefaddCoset, AS;

        

         X5: (v + w) = ( Class (( EQRZM V), [((j * z) + (i * y)), (i * j)])) by X1, X2, DefaddCoset, AS;

        

         X6: (u + (v + w)) = ( Class (( EQRZM V), [(((i * j) * s) + (k * ((j * z) + (i * y)))), (k * (i * j))])) by X0, X1, X2, X5, DefaddCoset, AS;

        ((j * ((i * s) + (k * z))) + ((k * i) * y)) = (((j * (i * s)) + (j * (k * z))) + ((k * i) * y)) by VECTSP_1:def 14

        .= ((((j * i) * s) + (j * (k * z))) + ((k * i) * y)) by VECTSP_1:def 16

        .= ((((i * j) * s) + (j * (k * z))) + ((k * i) * y))

        .= ((((i * j) * s) + (j * (k * z))) + (k * (i * y))) by VECTSP_1:def 16

        .= ((((i * j) * s) + ((j * k) * z)) + (k * (i * y))) by VECTSP_1:def 16

        .= ((((i * j) * s) + ((k * j) * z)) + (k * (i * y)))

        .= ((((i * j) * s) + (k * (j * z))) + (k * (i * y))) by VECTSP_1:def 16

        .= (((i * j) * s) + ((k * (j * z)) + (k * (i * y)))) by RLVECT_1:def 3

        .= (((i * j) * s) + (k * ((j * z) + (i * y)))) by VECTSP_1:def 14;

        hence ((u + v) + w) = (u + (v + w)) by X4, X6;

      end;

      for v be Element of IT holds (v + ( 0. IT)) = v

      proof

        let u be Element of IT;

        consider i be Element of INT.Ring , z be Element of V such that

         X1: i <> 0 & u = ( Class (( EQRZM V), [z, i])) by AS, LMEQRZM1;

        reconsider i1 = ( 1. INT.Ring ) as Element of INT.Ring ;

        

         X3: ( 0. IT) = ( Class (( EQRZM V), [( 0. V), i1])) by AS, defZero;

        

         X5: (u + ( 0. IT)) = ( Class (( EQRZM V), [((i1 * z) + (i * ( 0. V))), (i1 * i)])) by AS, X1, X3, DefaddCoset;

        ((i1 * z) + (i * ( 0. V))) = (z + (i * ( 0. V))) by VECTSP_1:def 17

        .= (z + ( 0. V)) by ZMODUL01: 1

        .= z;

        hence (u + ( 0. IT)) = u by X5, X1;

      end;

      hence thesis by P1, P2, P3, P4, P5, P6, P7, ALGSTR_0:def 16, RLVECT_1:def 2, RLVECT_1:def 3, RLVECT_1:def 4, VECTSP_1:def 14, VECTSP_1:def 15, VECTSP_1:def 16, VECTSP_1:def 17;

    end;

    definition

      let V be Z_Module;

      assume

       AS: V is Mult-cancelable;

      :: ZMODUL04:def5

      func Z_MQ_VectSp (V) -> VectSp of F_Rat equals

      : defZMQVSp: ModuleStr (# ( Class ( EQRZM V)), ( addCoset V), ( zeroCoset V), ( lmultCoset V) #);

      correctness by ThEQRZMV1, AS;

    end

    

     ThEQRZMV2: for V be Z_Module st V is Mult-cancelable holds ex I be Function of V, ( Z_MQ_VectSp V) st I is one-to-one & (for v be Element of V holds (I . v) = ( Class (( EQRZM V), [v, 1]))) & (for v,w be Element of V holds (I . (v + w)) = ((I . v) + (I . w))) & (for v be Element of V, i be Element of INT.Ring , q be Element of F_Rat st i = q holds (I . (i * v)) = (q * (I . v))) & (I . ( 0. V)) = ( 0. ( Z_MQ_VectSp V))

    proof

      let V be Z_Module;

      assume

       AS: V is Mult-cancelable;

      then

       Z0: ( Z_MQ_VectSp V) = ModuleStr (# ( Class ( EQRZM V)), ( addCoset V), ( zeroCoset V), ( lmultCoset V) #) by defZMQVSp;

      

       X1: 1 in INT by INT_1:def 2;

       not 1 in { 0 } by TARSKI:def 1;

      then

       X2: 1 in ( INT \ { 0 }) by XBOOLE_0:def 5, X1;

      set i1 = ( 1. INT.Ring );

      defpred F0[ Element of V, Element of ( Z_MQ_VectSp V)] means $2 = ( Class (( EQRZM V), [$1, 1]));

      

       A2: for x be Element of V holds ex v be Element of ( Z_MQ_VectSp V) st F0[x, v]

      proof

        let x be Element of V;

        

         X1: 1 in INT by INT_1:def 2;

         not 1 in { 0 } by TARSKI:def 1;

        then 1 in ( INT \ { 0 }) by XBOOLE_0:def 5, X1;

        then [x, 1] in [:the carrier of V, ( INT \ { 0 }):] by ZFMISC_1: 87;

        then

        reconsider z = ( Class (( EQRZM V), [x, 1])) as Element of ( Z_MQ_VectSp V) by Z0, EQREL_1:def 3;

        z = ( Class (( EQRZM V), [x, 1]));

        hence ex z be Element of ( Z_MQ_VectSp V) st F0[x, z];

      end;

      consider F be Function of V, ( Z_MQ_VectSp V) such that

       X3: for x be Element of V holds F0[x, (F . x)] from FUNCT_2:sch 3( A2);

      take F;

       S2:

      now

        let x1,x2 be object;

        assume

         A1: x1 in the carrier of V & x2 in the carrier of V & (F . x1) = (F . x2);

        then

        reconsider x10 = x1, x20 = x2 as Element of V;

        

         P1: (F . x1) = ( Class (( EQRZM V), [x10, 1])) by X3;

        

         P2: [x10, 1] in [:the carrier of V, ( INT \ { 0 }):] by X2, ZFMISC_1: 87;

        ( Class (( EQRZM V), [x10, i1])) = ( Class (( EQRZM V), [x20, i1])) by A1, P1, X3;

        then

         P3: [ [x10, i1], [x20, i1]] in ( EQRZM V) by P2, EQREL_1: 35;

        

        thus x1 = (i1 * x10) by VECTSP_1:def 17

        .= (i1 * x20) by AS, P3, LMEQR001

        .= x2 by VECTSP_1:def 17;

      end;

      

       S3: for v,w be Element of V holds (F . (v + w)) = ((F . v) + (F . w))

      proof

        let v,w be Element of V;

        

         P1: (F . v) = ( Class (( EQRZM V), [v, 1])) by X3;

        

         P2: (F . w) = ( Class (( EQRZM V), [w, 1])) by X3;

        

         P8: ((i1 * v) + (i1 * w)) = (i1 * (v + w)) by VECTSP_1:def 14

        .= (v + w) by VECTSP_1:def 17;

        ((F . v) + (F . w)) = ( Class (( EQRZM V), [((i1 * v) + (i1 * w)), (i1 * i1)])) by AS, P1, P2, Z0, DefaddCoset

        .= (F . (v + w)) by P8, X3;

        hence thesis;

      end;

      

       S4: for v be Element of V, i be Element of INT.Ring , q be Element of F_Rat st i = q holds (F . (i * v)) = (q * (F . v))

      proof

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

        assume

         AS0: i = x;

        

         P1: (F . v) = ( Class (( EQRZM V), [v, i1])) by X3;

        reconsider ii = i, ii1 = i1 as Integer;

        i1 <> ( 0. INT.Ring ) & x = (ii / ii1) by AS0;

        

        then (x * (F . v)) = ( Class (( EQRZM V), [(i * v), (i1 * i1)])) by AS, P1, Z0, DeflmultCoset

        .= (F . (i * v)) by X3;

        hence thesis;

      end;

      (F . ( 0. V)) = ( Class (( EQRZM V), [( 0. V), 1])) by X3

      .= ( 0. ( Z_MQ_VectSp V)) by AS, Z0, defZero;

      hence thesis by S2, S3, S4, X3, FUNCT_2: 19;

    end;

    definition

      let V be Z_Module;

      assume

       AS: V is Mult-cancelable;

      :: ZMODUL04:def6

      func MorphsZQ (V) -> Function of V, ( Z_MQ_VectSp V) means

      : defMorph: it is one-to-one & (for v be Element of V holds (it . v) = ( Class (( EQRZM V), [v, 1]))) & (for v,w be Element of V holds (it . (v + w)) = ((it . v) + (it . w))) & (for v be Element of V, i be Element of INT.Ring , q be Element of F_Rat st i = q holds (it . (i * v)) = (q * (it . v))) & (it . ( 0. V)) = ( 0. ( Z_MQ_VectSp V));

      existence by ThEQRZMV2, AS;

      uniqueness

      proof

        let F1,F2 be Function of V, ( Z_MQ_VectSp V);

        assume

         A1: F1 is one-to-one & (for v be Element of V holds (F1 . v) = ( Class (( EQRZM V), [v, 1]))) & (for v,w be Element of V holds (F1 . (v + w)) = ((F1 . v) + (F1 . w))) & (for v be Element of V, i be Element of INT.Ring , q be Element of F_Rat st i = q holds (F1 . (i * v)) = (q * (F1 . v))) & (F1 . ( 0. V)) = ( 0. ( Z_MQ_VectSp V));

        assume

         A2: F2 is one-to-one & (for v be Element of V holds (F2 . v) = ( Class (( EQRZM V), [v, 1]))) & (for v,w be Element of V holds (F2 . (v + w)) = ((F2 . v) + (F2 . w))) & (for v be Element of V, i be Element of INT.Ring , q be Element of F_Rat st i = q holds (F2 . (i * v)) = (q * (F2 . v))) & (F2 . ( 0. V)) = ( 0. ( Z_MQ_VectSp V));

        now

          let v be Element of V;

          

          thus (F1 . v) = ( Class (( EQRZM V), [v, 1])) by A1

          .= (F2 . v) by A2;

        end;

        hence F1 = F2 by FUNCT_2:def 8;

      end;

    end

    theorem :: ZMODUL04:6

    

     XThSum: for V be Z_Module st V is Mult-cancelable holds for s be FinSequence of V, t be FinSequence of ( Z_MQ_VectSp V) st ( len s) = ( len t) & for i be Element of NAT st i in ( dom s) holds ex si be Vector of V st si = (s . i) & (t . i) = (( MorphsZQ V) . si) holds ( Sum t) = (( MorphsZQ V) . ( Sum s))

    proof

      let V be Z_Module;

      assume

       AS: V is Mult-cancelable;

      defpred P[ Nat] means for s be FinSequence of V, t be FinSequence of ( Z_MQ_VectSp V) st ( len s) = $1 & ( len s) = ( len t) & for i be Element of NAT st i in ( dom s) holds ex si be Vector of V st si = (s . i) & (t . i) = (( MorphsZQ V) . si) holds ( Sum t) = (( MorphsZQ V) . ( Sum s));

      

       A1: P[ 0 ]

      proof

        let s be FinSequence of V, t be FinSequence of ( Z_MQ_VectSp V);

        assume that

         A2: ( len s) = 0 & ( len s) = ( len t) and for i be Element of NAT st i in ( dom s) holds ex si be Vector of V st si = (s . i) & (t . i) = (( MorphsZQ V) . si);

        s = ( <*> the carrier of V) by A2;

        then ( Sum s) = ( 0. V) by RLVECT_1: 43;

        then

         A3: (( MorphsZQ V) . ( Sum s)) = ( 0. ( Z_MQ_VectSp V)) by defMorph, AS;

        t = ( <*> the carrier of ( Z_MQ_VectSp V)) by A2;

        hence thesis by A3, RLVECT_1: 43;

      end;

      

       A4: for k be Nat st P[k] holds P[(k + 1)]

      proof

        let k be Nat;

        assume

         A5: P[k];

        now

          let s be FinSequence of V, t be FinSequence of ( Z_MQ_VectSp V);

          assume that

           A6: ( len s) = (k + 1) & ( len s) = ( len t) and

           A7: for i be Element of NAT st i in ( dom s) holds ex si be Vector of V st si = (s . i) & (t . i) = (( MorphsZQ V) . si);

          reconsider s1 = (s | k) as FinSequence of V;

          

           A8: ( dom s) = ( Seg (k + 1)) by A6, FINSEQ_1:def 3;

          

           A9: ( dom t) = ( Seg (k + 1)) by A6, FINSEQ_1:def 3;

          

           A10: ( len s1) = k by A6, FINSEQ_1: 59, NAT_1: 11;

          

           A11: ( dom s1) = ( Seg ( len s1)) by FINSEQ_1:def 3

          .= ( Seg k) by A6, FINSEQ_1: 59, NAT_1: 11;

          then

           A12: s1 = (s | ( dom s1)) by FINSEQ_1:def 15;

          reconsider t1 = (t | k) as FinSequence of ( Z_MQ_VectSp V);

          

           A13: ( dom t1) = ( Seg ( len t1)) by FINSEQ_1:def 3

          .= ( Seg k) by A6, FINSEQ_1: 59, NAT_1: 11;

          then

           A14: t1 = (t | ( dom t1)) by FINSEQ_1:def 15;

          k in NAT by ORDINAL1:def 12;

          then

           A15: ( len t1) = k by A13, FINSEQ_1:def 3;

          (s . ( len s)) in ( rng s) by A6, A8, FINSEQ_1: 4, FUNCT_1: 3;

          then

          reconsider vs = (s . ( len s)) as Element of V;

          (t . ( len t)) in ( rng t) by A6, A9, FINSEQ_1: 4, FUNCT_1: 3;

          then

          reconsider vt = (t . ( len t)) as Element of ( Z_MQ_VectSp V);

          

           A16: ( len s1) = k & ( len s1) = ( len t1) by A10, A13, FINSEQ_1:def 3;

          

           A17: for i be Element of NAT st i in ( dom s1) holds ex si be Vector of V st si = (s1 . i) & (t1 . i) = (( MorphsZQ V) . si)

          proof

            let i be Element of NAT ;

            assume

             A18: i in ( dom s1);

            ( Seg k) c= ( Seg (k + 1)) by FINSEQ_1: 5, NAT_1: 11;

            then

            consider si be Vector of V such that

             A19: si = (s . i) & (t . i) = (( MorphsZQ V) . si) by A7, A11, A8, A18;

            take si;

            thus si = (s1 . i) by A12, A18, A19, FUNCT_1: 49;

            thus (t1 . i) = (( MorphsZQ V) . si) by A14, A11, A13, A18, A19, FUNCT_1: 49;

          end;

          

           A20: ( Sum t1) = (( MorphsZQ V) . ( Sum s1)) by A5, A16, A17;

          

           A21: ( len s) = (( len s1) + 1) by A6, FINSEQ_1: 59, NAT_1: 11;

          consider ssi be Vector of V such that

           A22: ssi = (s . ( len s)) & (t . ( len s)) = (( MorphsZQ V) . ssi) by A6, A7, A8, FINSEQ_1: 4;

          

          thus ( Sum t) = (( Sum t1) + vt) by A6, A14, A15, RLVECT_1: 38

          .= (( MorphsZQ V) . (( Sum s1) + vs)) by AS, A6, A20, A22, defMorph

          .= (( MorphsZQ V) . ( Sum s)) by A12, A21, RLVECT_1: 38;

        end;

        hence P[(k + 1)];

      end;

      for k be Nat holds P[k] from NAT_1:sch 2( A1, A4);

      hence thesis;

    end;

    theorem :: ZMODUL04:7

    

     XThSum1: for V be Z_Module, I be Subset of V, IQ be Subset of ( Z_MQ_VectSp V), l be Linear_Combination of I, lq be Linear_Combination of IQ st V is Mult-cancelable & IQ = (( MorphsZQ V) .: I) & l = (lq * ( MorphsZQ V)) holds ( Sum lq) = (( MorphsZQ V) . ( Sum l))

    proof

      let V be Z_Module, I be Subset of V, IQ be Subset of ( Z_MQ_VectSp V), l be Linear_Combination of I, lq be Linear_Combination of IQ;

      assume

       AS0: V is Mult-cancelable & IQ = (( MorphsZQ V) .: I) & l = (lq * ( MorphsZQ V));

      per cases ;

        suppose

         A3: I is empty;

        then IQ = ( {} the carrier of ( Z_MQ_VectSp V)) by AS0;

        then lq = ( ZeroLC ( Z_MQ_VectSp V)) by VECTSP_6: 6;

        then

         A6: ( Sum lq) = ( 0. ( Z_MQ_VectSp V)) by VECTSP_6: 15;

        I = ( {} the carrier of V) by A3;

        then l = ( ZeroLC V) by ZMODUL02: 12;

        then ( Sum l) = ( 0. V) by ZMODUL02: 19;

        hence ( Sum lq) = (( MorphsZQ V) . ( Sum l)) by A6, defMorph, AS0;

      end;

        suppose

         E1: I is non empty;

        then

        consider v0 be object such that

         A7: v0 in I;

        reconsider v0 as Vector of V by A7;

        (( MorphsZQ V) . v0) in IQ by A7, AS0, FUNCT_2: 35;

        then

        reconsider X = IQ as non empty Subset of ( Z_MQ_VectSp V);

        reconsider g = (( MorphsZQ V) | I) as Function of I, IQ by FUNCT_2: 101, AS0;

        ( MorphsZQ V) is one-to-one by defMorph, AS0;

        then

         AX1: g is one-to-one by FUNCT_1: 52;

        

         AX2: ( rng g) = IQ by RELAT_1: 115, AS0;

        then

        reconsider F = (g " ) as Function of IQ, I by FUNCT_2: 25, AX1;

        reconsider F as Function of X, the carrier of V by E1, FUNCT_2: 7;

        X = IQ;

        then

         AX2A: ( dom g) = I by FUNCT_2:def 1;

        then

         AX3: ( dom F) = X & ( rng F) = I by AX1, AX2, FUNCT_1: 33;

        

         A8: for u be Vector of V st u in I holds (F . (( MorphsZQ V) . u)) = u

        proof

          let u be Vector of V;

          assume

           AS8: u in I;

          

          hence (F . (( MorphsZQ V) . u)) = (F . (g . u)) by FUNCT_1: 49

          .= u by FUNCT_1: 34, AS8, AX2A, AX1;

        end;

        consider Gq be FinSequence of ( Z_MQ_VectSp V) such that

         A9: Gq is one-to-one & ( rng Gq) = ( Carrier lq) & ( Sum lq) = ( Sum (lq (#) Gq)) by VECTSP_6:def 6;

        set n = ( len Gq);

        

         A10: ( dom Gq) = ( Seg n) by FINSEQ_1:def 3;

        

         A11: ( Carrier lq) c= X by VECTSP_6:def 4;

        

         A12: ( dom (F * Gq)) = ( Seg n) by A10, A9, AX3, RELAT_1: 27, VECTSP_6:def 4;

        

         A13: ( rng (F * Gq)) c= the carrier of V;

        (F * Gq) is FinSequence by AX3, A9, FINSEQ_1: 16, VECTSP_6:def 4;

        then

        reconsider FGq = (F * Gq) as FinSequence of V by A13, FINSEQ_1:def 4;

        for x be object holds x in ( rng FGq) iff x in ( Carrier l)

        proof

          let x be object;

          hereby

            assume x in ( rng FGq);

            then

            consider z be object such that

             A14: z in ( dom FGq) & x = (FGq . z) by FUNCT_1:def 3;

            

             A15: x = (F . (Gq . z)) by A14, FUNCT_1: 12;

            

             A16: z in ( dom Gq) & (Gq . z) in ( dom F) by A14, FUNCT_1: 11;

            then

            consider u be Vector of V such that

             A17: u in I & (Gq . z) = (( MorphsZQ V) . u) by AS0, FUNCT_2: 65;

            

             A18: (F . (Gq . z)) = u by A8, A17;

            consider w be Element of ( Z_MQ_VectSp V) such that

             A19: (Gq . z) = w & (lq . w) <> ( 0. F_Rat ) by A9, A16, FUNCT_1: 3, VECTSP_6: 1;

            (l . u) <> ( 0. F_Rat ) by AS0, A17, A19, FUNCT_2: 15;

            hence x in ( Carrier l) by A15, A18;

          end;

          assume

           A20: x in ( Carrier l);

          then

          reconsider u = x as Vector of V;

          

           A21: (l . u) <> 0 by A20, ZMODUL02: 8;

          

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

          (lq . (( MorphsZQ V) . u)) <> 0 by AS0, A21, FUNCT_2: 15;

          then

           A23: (( MorphsZQ V) . u) in ( rng Gq) by A9;

          then

          consider z be object such that

           A24: z in ( dom Gq) & (( MorphsZQ V) . u) = (Gq . z) by FUNCT_1:def 3;

          

           A25: (F . (Gq . z)) = u by A20, A22, A24, A8;

          

           A26: z in ( dom FGq) by A11, A9, A24, AX3, A23, FUNCT_1: 11;

          then (FGq . z) = u by A25, FUNCT_1: 12;

          hence x in ( rng FGq) by A26, FUNCT_1:def 3;

        end;

        then ( rng FGq) = ( Carrier l) by TARSKI: 2;

        then

         A27: ( Sum l) = ( Sum (l (#) FGq)) by A9, AX1, VECTSP_6:def 6;

        

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

        then

         A29: ( len (l (#) FGq)) = n by A12, FINSEQ_1:def 3;

        

         A30: ( len (lq (#) Gq)) = n by VECTSP_6:def 5;

        now

          let i be Element of NAT ;

          assume

           A31: i in ( dom (l (#) FGq));

          then i in ( Seg ( len FGq)) by A28, FINSEQ_1:def 3;

          then

           A32: i in ( dom FGq) by FINSEQ_1:def 3;

          then (FGq . i) in ( rng FGq) by FUNCT_1: 3;

          then

          reconsider v = (FGq . i) as Element of V;

          

           A33: ((l (#) FGq) . i) = ((l . v) * v) by A32, ZMODUL02: 13;

          i in ( Seg n) by A29, A31, FINSEQ_1:def 3;

          then

           A34: i in ( dom Gq) by FINSEQ_1:def 3;

          then

           A35: (Gq . i) in ( rng Gq) by FUNCT_1: 3;

          reconsider w = (Gq . i) as Element of ( Z_MQ_VectSp V) by A35;

          consider u be Vector of V such that

           A37: u in I & (Gq . i) = (( MorphsZQ V) . u) by AS0, A9, A11, A35, FUNCT_2: 65;

          

           A381: (F . (Gq . i)) = u by A8, A37;

          then

           A38: v = u by A32, FUNCT_1: 12;

          

           A39: w = (( MorphsZQ V) . v) by A32, A37, A381, FUNCT_1: 12;

          

           A40: (lq . w) = (l . v) by AS0, A37, A38, FUNCT_2: 15;

          

           T1: ((lq . w) * w) = (( MorphsZQ V) . ((l . v) * v)) by defMorph, A39, A40, AS0;

          thus ex si be VECTOR of V st si = ((l (#) FGq) . i) & ((lq (#) Gq) . i) = (( MorphsZQ V) . si)

          proof

            take si = ((l (#) FGq) . i);

            thus thesis by A33, A34, VECTSP_6: 8, T1;

          end;

        end;

        hence ( Sum lq) = (( MorphsZQ V) . ( Sum l)) by A9, A27, A29, A30, AS0, XThSum;

      end;

    end;

    theorem :: ZMODUL04:8

    

     ThEQRZMV3A: for V be Z_Module, IQ be Subset of ( Z_MQ_VectSp V) holds for lq be Linear_Combination of IQ holds ex m be Integer, a be Element of F_Rat st m <> 0 & m = a & ( rng (a * lq)) c= INT

    proof

      let V be Z_Module, IQ be Subset of ( Z_MQ_VectSp V);

      defpred P[ Nat] means for lq be Linear_Combination of IQ st ( card ( Carrier lq)) = $1 holds ex m be Integer, a be Element of F_Rat st m <> 0 & m = a & ( rng (a * lq)) c= INT ;

      

       P1: P[ 0 ]

      proof

        let lq be Linear_Combination of IQ such that

         P2: ( card ( Carrier lq)) = 0 ;

        

         P3: ( Carrier lq) = {} by P2;

        reconsider m = 1 as Integer;

        reconsider a = m as Element of F_Rat ;

        ( Carrier (a * lq)) c= ( Carrier lq) by VECTSP_6: 28;

        then ( Carrier (a * lq)) = {} by P3;

        then

         X1: (a * lq) = ( ZeroLC ( Z_MQ_VectSp V)) by VECTSP_6:def 3;

        now

          let y be object;

          assume y in ( rng (a * lq));

          then

          consider x be Element of ( Z_MQ_VectSp V) such that

           X2: y = ((a * lq) . x) by FUNCT_2: 113;

          ((a * lq) . x) = ( 0. F_Rat ) by X1, VECTSP_6: 3

          .= 0 ;

          hence y in INT by X2;

        end;

        hence thesis by TARSKI:def 3;

      end;

      

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

      proof

        let n be Nat;

        assume

         P21: P[n];

        now

          let lq be Linear_Combination of IQ;

          assume

           P22: ( card ( Carrier lq)) = (n + 1);

          then ( Carrier lq) <> {} ;

          then

          consider x be object such that

           P24: x in ( Carrier lq) by XBOOLE_0:def 1;

          reconsider x as Element of ( Z_MQ_VectSp V) by P24;

          

           P25: ( card (( Carrier lq) \ {x})) = (( card ( Carrier lq)) - ( card {x})) by P24, CARD_2: 44, ZFMISC_1: 31

          .= ((n + 1) - 1) by P22, CARD_2: 42

          .= n;

          defpred PN[ Element of ( Z_MQ_VectSp V), Element of F_Rat ] means ($1 in {x} implies $2 = 0 ) & ( not $1 in {x} implies $2 = (lq . $1));

          

           A2: for v be Element of ( Z_MQ_VectSp V) holds ex y be Element of F_Rat st PN[v, y]

          proof

            let v be Element of ( Z_MQ_VectSp V);

            v in {x} or not v in {x};

            hence thesis;

          end;

          consider lq0 be Function of the carrier of ( Z_MQ_VectSp V), the carrier of F_Rat such that

           A4: for v be Element of ( Z_MQ_VectSp V) holds PN[v, (lq0 . v)] from FUNCT_2:sch 3( A2);

          reconsider lq0 as Element of ( Funcs (the carrier of ( Z_MQ_VectSp V),the carrier of F_Rat )) by FUNCT_2: 8;

          set T = { v where v be Element of ( Z_MQ_VectSp V) : (lq0 . v) <> ( 0. F_Rat ) };

          

           A400: T c= (( Carrier lq) \ {x})

          proof

            let v0 be object;

            assume v0 in T;

            then

             XX2: ex v1 be Element of ( Z_MQ_VectSp V) st v1 = v0 & (lq0 . v1) <> ( 0. F_Rat );

            then

            reconsider v = v0 as Element of ( Z_MQ_VectSp V);

            

             XX4: not v in {x} by A4, XX2;

            (lq . v) <> ( 0. F_Rat ) by A4, XX2;

            then v0 in ( Carrier lq);

            hence v0 in (( Carrier lq) \ {x}) by XBOOLE_0:def 5, XX4;

          end;

          (( Carrier lq) \ {x}) c= ( Carrier lq) by XBOOLE_1: 36;

          then

           A40: T c= ( Carrier lq) by XBOOLE_1: 1, A400;

          reconsider T as finite Subset of ( Z_MQ_VectSp V) by A400, XBOOLE_1: 1;

          for v be Element of ( Z_MQ_VectSp V) st not v in T holds (lq0 . v) = ( 0. F_Rat );

          then

          reconsider lq0 as Linear_Combination of ( Z_MQ_VectSp V) by VECTSP_6:def 1;

          

           X5: T = ( Carrier lq0);

          ( Carrier lq) c= IQ by VECTSP_6:def 4;

          then

          reconsider lq0 as Linear_Combination of IQ by A40, X5, VECTSP_6:def 4, XBOOLE_1: 1;

          (( Carrier lq) \ {x}) c= T

          proof

            let v0 be object;

            assume

             YY11: v0 in (( Carrier lq) \ {x});

            then

             YY1: v0 in ( Carrier lq) & not v0 in {x} by XBOOLE_0:def 5;

            reconsider v = v0 as Element of ( Z_MQ_VectSp V) by YY11;

            (lq . v) <> ( 0. F_Rat ) by YY1, VECTSP_6: 2;

            then (lq0 . v) <> ( 0. F_Rat ) by A4, YY1;

            hence v0 in T;

          end;

          then ( card ( Carrier lq0)) = n by A400, P25, XBOOLE_0:def 10;

          then

          consider m0 be Integer, a0 be Element of F_Rat such that

           X8: m0 <> 0 & m0 = a0 & ( rng (a0 * lq0)) c= INT by P21;

          consider k0,n0 be Integer such that

           X9: n0 <> 0 & (lq . x) = (k0 / n0) by RAT_1: 1;

          reconsider m = (n0 * m0) as Integer;

          reconsider a = m as Element of F_Rat by RAT_1:def 2;

          reconsider b = n0 as Element of F_Rat by RAT_1:def 2;

          for y be object st y in ( rng (a * lq)) holds y in INT

          proof

            let y be object;

            assume y in ( rng (a * lq));

            then

            consider z be Element of ( Z_MQ_VectSp V) such that

             X2: y = ((a * lq) . z) by FUNCT_2: 113;

            per cases ;

              suppose

               B2: z in {x};

              

               BB2: y = ((a * lq) . x) by B2, X2, TARSKI:def 1

              .= (a * (lq . x)) by VECTSP_6:def 9;

              (a * (lq . x)) = ((m0 * n0) * (k0 / n0)) by X9

              .= (m0 * (n0 * (k0 / n0)))

              .= (m0 * k0) by XCMPLX_1: 87, X9;

              hence y in INT by BB2, INT_1:def 2;

            end;

              suppose not z in {x};

              then

               B31: (lq0 . z) = (lq . z) by A4;

              

               BBB: a = (b * a0) by X8;

              

               B32: ((a * lq) . z) = (a * (lq . z)) by VECTSP_6:def 9

              .= (b * (a0 * (lq0 . z))) by B31, BBB

              .= (b * ((a0 * lq0) . z)) by VECTSP_6:def 9;

              ((a0 * lq0) . z) in ( rng (a0 * lq0)) by FUNCT_2: 4;

              then

              reconsider aqz = ((a0 * lq0) . z) as Integer by X8;

              (b * ((a0 * lq0) . z)) = (n0 * aqz);

              hence y in INT by B32, X2, INT_1:def 2;

            end;

          end;

          hence ex m be Integer, a be Element of F_Rat st m <> 0 & m = a & ( rng (a * lq)) c= INT by X8, X9, TARSKI:def 3;

        end;

        hence P[(n + 1)];

      end;

      

       P3: for n be Nat holds P[n] from NAT_1:sch 2( P1, P2);

      now

        let lq be Linear_Combination of IQ;

        ( card ( Carrier lq)) is Element of NAT ;

        hence ex m be Integer, a be Element of F_Rat st m <> 0 & m = a & ( rng (a * lq)) c= INT by P3;

      end;

      hence thesis;

    end;

    theorem :: ZMODUL04:9

    

     ThEQRZMV3: for V be Z_Module, I be Subset of V, IQ be Subset of ( Z_MQ_VectSp V), lq be Linear_Combination of IQ st V is Mult-cancelable & IQ = (( MorphsZQ V) .: I) holds ex m be Element of INT.Ring , a be Element of F_Rat , l be Linear_Combination of I st m <> ( 0. INT.Ring ) & m = a & l = ((a * lq) * ( MorphsZQ V)) & (( MorphsZQ V) " ( Carrier lq)) = ( Carrier l)

    proof

      let V be Z_Module, I be Subset of V, IQ be Subset of ( Z_MQ_VectSp V), lq be Linear_Combination of IQ;

      assume

       AS: V is Mult-cancelable & IQ = (( MorphsZQ V) .: I);

      consider m be Integer, a be Element of F_Rat such that

       X3: m <> 0 & m = a & ( rng (a * lq)) c= INT by ThEQRZMV3A;

      reconsider mm = m as Element of INT.Ring by INT_1:def 2;

      

       P81: ( rng ((a * lq) * ( MorphsZQ V))) c= ( rng (a * lq)) by RELAT_1: 26;

      ( dom ((a * lq) * ( MorphsZQ V))) = the carrier of V by FUNCT_2:def 1;

      then ((a * lq) * ( MorphsZQ V)) is Function of the carrier of V, INT by P81, X3, FUNCT_2: 2, XBOOLE_1: 1;

      then

      reconsider l = ((a * lq) * ( MorphsZQ V)) as Element of ( Funcs (the carrier of V, INT )) by FUNCT_2: 8;

      set T = { v where v be Element of V : (l . v) <> 0 };

      set F = ( MorphsZQ V);

       B2:

      now

        let v be object;

        assume v in T;

        then ex v1 be Element of V st v1 = v & (l . v1) <> 0 ;

        hence v in the carrier of V;

      end;

      

       R1: T c= (F " ( Carrier lq))

      proof

        let x be object;

        assume x in T;

        then

        consider v be Element of V such that

         R11: x = v & (l . v) <> 0 ;

        

         RRR: ( dom F) = the carrier of V by FUNCT_2:def 1;

        

         V1: (l . v) = ((a * lq) . (F . v)) by FUNCT_1: 13, RRR

        .= (a * (lq . (F . v))) by VECTSP_6:def 9;

        (lq . (F . v)) <> ( 0. F_Rat ) by V1, R11;

        then (F . v) in ( Carrier lq);

        hence x in (F " ( Carrier lq)) by R11, FUNCT_2: 38;

      end;

      F is one-to-one by AS, defMorph;

      then (F " ( Carrier lq)) = ((F " ) .: ( Carrier lq)) by FUNCT_1: 85;

      then

      reconsider T as finite Subset of V by B2, R1, TARSKI:def 3;

      for v be Element of V st not v in T holds (l . v) = ( 0. INT.Ring );

      then

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

      (F " ( Carrier lq)) c= T

      proof

        let x be object;

        assume

         S21: x in (F " ( Carrier lq));

        then x in the carrier of V & (F . x) in ( Carrier lq) by FUNCT_2: 38;

        then

        consider w be Element of ( Z_MQ_VectSp V) such that

         R11: (F . x) = w & (lq . w) <> ( 0. F_Rat );

        reconsider v = x as Element of V by S21;

        

         RRR: ( dom F) = the carrier of V by FUNCT_2:def 1;

        

         RR1: (l . v) = ((a * lq) . (F . v)) by FUNCT_1: 13, RRR

        .= (a * (lq . w)) by R11, VECTSP_6:def 9;

        reconsider a1 = a, d1 = (lq . w) as Rational;

        (l . v) <> 0 by RR1, R11, X3;

        hence x in T;

      end;

      then

       A9: (F " ( Carrier lq)) = T by R1;

      

       A7: T = ( Carrier l);

      

       AA1: (F " ( Carrier lq)) c= (F " (F .: I)) by AS, RELAT_1: 143, VECTSP_6:def 4;

      ( dom F) = the carrier of V by FUNCT_2:def 1;

      then F is one-to-one & I c= ( dom F) by AS, defMorph;

      then T c= I by A9, AA1, FUNCT_1: 94;

      then

      reconsider l1 = l as Linear_Combination of I by A7, VECTSP_6:def 4;

      take mm;

      take a;

      take l1;

      thus mm <> ( 0. INT.Ring ) & mm = a & l1 = ((a * lq) * ( MorphsZQ V)) & (( MorphsZQ V) " ( Carrier lq)) = ( Carrier l1) by A9, X3;

    end;

    theorem :: ZMODUL04:10

    

     ThEQRZMV3B: for V be Z_Module, I be Subset of V, IQ be Subset of ( Z_MQ_VectSp V), lq be Linear_Combination of IQ, m be Integer, a be Element of F_Rat , l be Linear_Combination of I st V is Mult-cancelable & IQ = (( MorphsZQ V) .: I) & m <> 0 & m = a & l = ((a * lq) * ( MorphsZQ V)) holds (a * ( Sum lq)) = (( MorphsZQ V) . ( Sum l))

    proof

      let V be Z_Module, I be Subset of V, IQ be Subset of ( Z_MQ_VectSp V), lq be Linear_Combination of IQ, m be Integer, a be Element of F_Rat , l be Linear_Combination of I;

      assume

       AS: V is Mult-cancelable & IQ = (( MorphsZQ V) .: I) & m <> 0 & m = a & l = ((a * lq) * ( MorphsZQ V));

      reconsider lqa = (a * lq) as Linear_Combination of IQ by VECTSP_6: 31;

      

      thus (a * ( Sum lq)) = ( Sum lqa) by VECTSP_6: 45

      .= (( MorphsZQ V) . ( Sum l)) by AS, XThSum1;

    end;

    theorem :: ZMODUL04:11

    

     ThEQRZMV3C: for V be Z_Module, I be Subset of V, IQ be Subset of ( Z_MQ_VectSp V) st V is Mult-cancelable & IQ = (( MorphsZQ V) .: I) & I is linearly-independent holds IQ is linearly-independent

    proof

      let V be Z_Module, I be Subset of V, IQ be Subset of ( Z_MQ_VectSp V);

      assume

       AS: V is Mult-cancelable & IQ = (( MorphsZQ V) .: I) & I is linearly-independent;

      assume not IQ is linearly-independent;

      then

      consider lq be Linear_Combination of IQ such that

       P1: ( Sum lq) = ( 0. ( Z_MQ_VectSp V)) & ( Carrier lq) <> {} by VECTSP_7:def 1;

      consider m be Element of INT.Ring , a be Element of F_Rat , l be Linear_Combination of I such that

       P2: m <> ( 0. INT.Ring ) & m = a & l = ((a * lq) * ( MorphsZQ V)) & (( MorphsZQ V) " ( Carrier lq)) = ( Carrier l) by ThEQRZMV3, AS;

      (a * ( Sum lq)) = ( 0. ( Z_MQ_VectSp V)) by P1, VECTSP_1: 15;

      then

       X2: (( MorphsZQ V) . ( Sum l)) = ( 0. ( Z_MQ_VectSp V)) by AS, P2, ThEQRZMV3B;

      

       X3: (( MorphsZQ V) . ( 0. V)) = ( 0. ( Z_MQ_VectSp V)) by AS, defMorph;

      ( MorphsZQ V) is one-to-one by AS, defMorph;

      then

       P3: ( Sum l) = ( 0. V) by X2, X3, FUNCT_2: 19;

      

       H6: ( Carrier lq) c= IQ by VECTSP_6:def 4;

      IQ c= ( rng ( MorphsZQ V)) by AS, RELAT_1: 111;

      then

       H2: ( Carrier lq) = (( MorphsZQ V) .: ( Carrier l)) by H6, P2, FUNCT_1: 77, XBOOLE_1: 1;

      ( Carrier l) <> {} by H2, P1;

      hence contradiction by AS, P3, VECTSP_7:def 1;

    end;

    theorem :: ZMODUL04:12

    

     ThEQRZMV4: for V be Z_Module, I be Subset of V, l be Linear_Combination of I, IQ be Subset of ( Z_MQ_VectSp V) st V is Mult-cancelable & IQ = (( MorphsZQ V) .: I) holds ex lq be Linear_Combination of IQ st l = (lq * ( MorphsZQ V)) & ( Carrier lq) = (( MorphsZQ V) .: ( Carrier l))

    proof

      let V be Z_Module, I be Subset of V, l be Linear_Combination of I, IQ be Subset of ( Z_MQ_VectSp V);

      assume

       AS0: V is Mult-cancelable & IQ = (( MorphsZQ V) .: I);

      reconsider I0 = ( Carrier l) as finite Subset of V;

      

       K2: (( MorphsZQ V) .: I0) c= IQ & (( MorphsZQ V) .: I0) is finite by AS0, RELAT_1: 123, VECTSP_6:def 4;

      reconsider IQ0 = (( MorphsZQ V) .: I0) as finite Subset of ( Z_MQ_VectSp V);

      defpred P[ object, object] means ($1 in IQ0 & ex v be Element of V st v in I0 & $1 = (( MorphsZQ V) . v) & $2 = (l . v)) or ( not $1 in IQ0 & $2 = ( 0. F_Rat ));

      

       A2: for x be object st x in the carrier of ( Z_MQ_VectSp V) holds ex y be object st y in RAT & P[x, y]

      proof

        let x be object;

        assume x in the carrier of ( Z_MQ_VectSp V);

        then

        reconsider x as Element of ( Z_MQ_VectSp V);

        per cases ;

          suppose

           A3: x in IQ0;

          then

          consider v be object such that

           A4: v in the carrier of V & v in I0 & x = (( MorphsZQ V) . v) by FUNCT_2: 64;

          reconsider v as Element of V by A4;

          (l . v) in RAT by NUMBERS: 14, TARSKI:def 3;

          hence thesis by A3, A4;

        end;

          suppose not x in IQ0;

          hence thesis;

        end;

      end;

      consider lq be Function of the carrier of ( Z_MQ_VectSp V), RAT such that

       A5: for x be object st x in the carrier of ( Z_MQ_VectSp V) holds P[x, (lq . x)] from FUNCT_2:sch 1( A2);

      

       A6: for x be Element of ( Z_MQ_VectSp V) st not x in IQ0 holds (lq . x) = ( 0. F_Rat ) by A5;

      lq is Element of ( Funcs (the carrier of ( Z_MQ_VectSp V), RAT )) by FUNCT_2: 8;

      then

      reconsider lq as Linear_Combination of ( Z_MQ_VectSp V) by A6, VECTSP_6:def 1;

      

       A11: ( Carrier lq) c= IQ0

      proof

        let x be object;

        assume that

         A7: x in ( Carrier lq) and

         A8: not x in IQ0;

        consider z be Element of ( Z_MQ_VectSp V) such that

         A9: x = z and

         A10: (lq . z) <> ( 0. F_Rat ) by A7;

        thus contradiction by A5, A8, A9, A10;

      end;

      then

      reconsider lq as Linear_Combination of IQ by K2, VECTSP_6:def 4, XBOOLE_1: 1;

      

       A12: ( dom l) = the carrier of V by FUNCT_2:def 1;

      

       A13: ( dom (lq * ( MorphsZQ V))) = the carrier of V by FUNCT_2:def 1;

      take lq;

      

       F1: ( MorphsZQ V) is one-to-one by defMorph, AS0;

      for x be object st x in ( dom l) holds (l . x) = ((lq * ( MorphsZQ V)) . x)

      proof

        let x be object;

        assume x in ( dom l);

        then

        reconsider v = x as Element of V;

        reconsider w = (( MorphsZQ V) . v) as Element of ( Z_MQ_VectSp V);

        per cases ;

          suppose v in I0;

          then w in IQ0 by FUNCT_2: 35;

          then

          consider v0 be Element of V such that

           A16: v0 in I0 & w = (( MorphsZQ V) . v0) & (lq . w) = (l . v0) by A5;

          v0 = v by A16, FUNCT_2: 19, F1;

          hence (l . x) = ((lq * ( MorphsZQ V)) . x) by A13, A16, FUNCT_1: 12;

        end;

          suppose

           A18: not v in I0;

          then

           A19: (l . v) = ( 0. F_Rat );

           not w in IQ0

          proof

            assume w in IQ0;

            then

            consider v0 be Element of V such that

             A16: v0 in I0 & w = (( MorphsZQ V) . v0) & (lq . w) = (l . v0) by A5;

            thus contradiction by A16, A18, F1, FUNCT_2: 19;

          end;

          then (lq . w) = ( 0. F_Rat ) by A5;

          hence (l . x) = ((lq * ( MorphsZQ V)) . x) by A13, A19, FUNCT_1: 12;

        end;

      end;

      hence

       U1: l = (lq * ( MorphsZQ V)) by FUNCT_1: 2, A12, A13;

      IQ0 c= ( Carrier lq)

      proof

        let x be object;

        assume x in IQ0;

        then

        consider v be object such that

         A4: v in the carrier of V & v in I0 & x = (( MorphsZQ V) . v) by FUNCT_2: 64;

        reconsider v as Element of V by A4;

        x = (( MorphsZQ V) . v) by A4;

        then

        reconsider y = x as Element of ( Z_MQ_VectSp V);

        

         X1: (lq . y) = (l . v) by A4, A13, U1, FUNCT_1: 12;

        (l . v) <> 0 by ZMODUL02: 8, A4;

        hence x in ( Carrier lq) by X1;

      end;

      hence ( Carrier lq) = (( MorphsZQ V) .: ( Carrier l)) by A11;

    end;

    theorem :: ZMODUL04:13

    

     ThQuotAX: for V be free Z_Module, I be Subset of V, IQ be Subset of ( Z_MQ_VectSp V), l be Linear_Combination of I, i be Element of INT.Ring st i <> ( 0. INT.Ring ) & IQ = (( MorphsZQ V) .: I) holds ( Class (( EQRZM V), [( Sum l), i])) in ( Lin IQ)

    proof

      let V be free Z_Module, I be Subset of V, IQ be Subset of ( Z_MQ_VectSp V), l be Linear_Combination of I, i be Element of INT.Ring ;

      assume

       AS: i <> ( 0. INT.Ring ) & IQ = (( MorphsZQ V) .: I);

      

       Z0: ( Z_MQ_VectSp V) = ModuleStr (# ( Class ( EQRZM V)), ( addCoset V), ( zeroCoset V), ( lmultCoset V) #) by defZMQVSp;

      consider lq be Linear_Combination of IQ such that

       P1: l = (lq * ( MorphsZQ V)) & ( Carrier lq) = (( MorphsZQ V) .: ( Carrier l)) by ThEQRZMV4, AS;

      

       P2: ( Sum lq) = (( MorphsZQ V) . ( Sum l)) by AS, P1, XThSum1;

      reconsider a = (1 / i) as Element of F_Rat by RAT_1:def 2;

      

       P3: (( MorphsZQ V) . ( Sum l)) = ( Class (( EQRZM V), [( Sum l), ( 1. INT.Ring )])) by defMorph;

      (a * (( MorphsZQ V) . ( Sum l))) = ( Class (( EQRZM V), [(( 1. INT.Ring ) * ( Sum l)), (i * ( 1. INT.Ring ))])) by AS, P3, Z0, DeflmultCoset

      .= ( Class (( EQRZM V), [( Sum l), i])) by VECTSP_1:def 17;

      hence thesis by P2, VECTSP_4: 21, VECTSP_7: 7;

    end;

    theorem :: ZMODUL04:14

    

     ThEQRZMV3E: for V be free Z_Module, I be Subset of V, IQ be Subset of ( Z_MQ_VectSp V) st IQ = (( MorphsZQ V) .: I) holds ( card I) = ( card IQ)

    proof

      let V be free Z_Module, I be Subset of V, IQ be Subset of ( Z_MQ_VectSp V);

      assume

       AS1: IQ = (( MorphsZQ V) .: I);

      

       P1: ( MorphsZQ V) is one-to-one by defMorph;

      the carrier of V = ( dom ( MorphsZQ V)) by FUNCT_2:def 1;

      hence ( card I) = ( card IQ) by AS1, P1, CARD_1: 5, CARD_1: 33;

    end;

    theorem :: ZMODUL04:15

    

     ThEQRZMV3D: for V be free Z_Module, I be Subset of V, IQ be Subset of ( Z_MQ_VectSp V) st IQ = (( MorphsZQ V) .: I) & I is Basis of V holds IQ is Basis of ( Z_MQ_VectSp V)

    proof

      let V be free Z_Module, I be Subset of V, IQ be Subset of ( Z_MQ_VectSp V);

      assume

       AS: IQ = (( MorphsZQ V) .: I) & I is Basis of V;

      then I is base;

      then

       X0: I is linearly-independent & ( Lin I) = the ModuleStr of V by VECTSP_7:def 3;

      

       X1: IQ is linearly-independent by AS, ThEQRZMV3C, VECTSP_7:def 3;

      

       AS0: ( Z_MQ_VectSp V) = ModuleStr (# ( Class ( EQRZM V)), ( addCoset V), ( zeroCoset V), ( lmultCoset V) #) by defZMQVSp;

      for vq be Element of ( Z_MQ_VectSp V) holds vq in ( Lin IQ)

      proof

        let vq be Element of ( Z_MQ_VectSp V);

        consider i be Element of INT.Ring , v be Element of V such that

         P3: i <> 0 & vq = ( Class (( EQRZM V), [v, i])) by AS0, LMEQRZM1;

        v in ( Lin I) by X0;

        then

        consider l be Linear_Combination of I such that

         P4: v = ( Sum l) by ZMODUL02: 64;

        thus vq in ( Lin IQ) by AS, P4, P3, ThQuotAX;

      end;

      hence thesis by AS0, X1, VECTSP_4: 32, VECTSP_7:def 3;

    end;

    registration

      let V be finite-rank free Z_Module;

      cluster ( Z_MQ_VectSp V) -> finite-dimensional;

      coherence

      proof

        consider I be finite Subset of V such that

         P1: I is Basis of V by ZMODUL03:def 3;

        reconsider IQ = (( MorphsZQ V) .: I) as Subset of ( Z_MQ_VectSp V);

        IQ is Basis of ( Z_MQ_VectSp V) by P1, ThEQRZMV3D;

        hence thesis by MATRLIN:def 1;

      end;

    end

    theorem :: ZMODUL04:16

    for V be finite-rank free Z_Module holds ( rank V) = ( dim ( Z_MQ_VectSp V))

    proof

      let V be finite-rank free Z_Module;

      reconsider I = the Basis of V as Subset of V;

      reconsider IQ = (( MorphsZQ V) .: I) as Subset of ( Z_MQ_VectSp V);

      

       A1: IQ is Basis of ( Z_MQ_VectSp V) by ThEQRZMV3D;

      

      thus ( rank V) = ( card I) by ZMODUL03:def 5

      .= ( card IQ) by ThEQRZMV3E

      .= ( dim ( Z_MQ_VectSp V)) by A1, VECTSP_9:def 1;

    end;

    theorem :: ZMODUL04:17

    

     XXTh1: for V be free Z_Module, I,A be finite Subset of V st I is Basis of V & (( card I) + 1) = ( card A) holds A is linearly-dependent

    proof

      let V be free Z_Module, I,A be finite Subset of V;

      assume

       AS: I is Basis of V & (( card I) + 1) = ( card A);

      reconsider IQ = (( MorphsZQ V) .: I) as Subset of ( Z_MQ_VectSp V);

      reconsider IQ as finite Subset of ( Z_MQ_VectSp V);

      

       P2: IQ is Basis of ( Z_MQ_VectSp V) by AS, ThEQRZMV3D;

      assume

       P31: not A is linearly-dependent;

      reconsider B = (( MorphsZQ V) .: A) as Subset of ( Z_MQ_VectSp V);

      reconsider B as finite Subset of ( Z_MQ_VectSp V);

      

       PP: IQ is linearly-independent & ( Lin IQ) = the ModuleStr of ( Z_MQ_VectSp V) by VECTSP_7:def 3, P2;

      B is linearly-independent by P31, ThEQRZMV3C;

      then

       P5: ( card B) <= ( card IQ) by VECTSP_9: 19, PP;

      ( card IQ) = ( card I) by ThEQRZMV3E;

      then ( card A) <= ( card I) by P5, ThEQRZMV3E;

      hence contradiction by AS, NAT_1: 13;

    end;

    theorem :: ZMODUL04:18

    

     XXTh2: for V be free Z_Module, A,B be Subset of V st A is linearly-dependent & A c= B holds B is linearly-dependent by VECTSP_7: 1;

    theorem :: ZMODUL04:19

    

     XXTh3: for V be free Z_Module, D,A be Subset of V st D is Basis of V & D is finite & ( card D) c< ( card A) holds A is linearly-dependent

    proof

      let V be free Z_Module, D,A be Subset of V;

      assume

       AS: D is Basis of V & D is finite & ( card D) c< ( card A);

      reconsider D0 = D as finite Subset of V by AS;

      (A \ D0) <> {} by AS, CARD_1: 68, ORDINAL1: 11;

      then

      consider x be object such that

       P3: x in (A \ D0) by XBOOLE_0:def 1;

      x in A & not x in D0 by P3, XBOOLE_0:def 5;

      then

       P5: ( card (D0 \/ {x})) = (( card D0) + 1) by CARD_2: 41;

      ( succ ( card D0)) = (( card D0) +^ 1) by ORDINAL2: 31

      .= (( card D0) + 1) by CARD_2: 36;

      then

       P6: (( card D0) + 1) c= ( card A) by AS, ORDINAL1: 11, ORDINAL1: 21;

      consider f be Function such that

       P7: f is one-to-one & ( dom f) = (D0 \/ {x}) & ( rng f) c= A by CARD_1: 10, P5, P6;

      set B = ( rng f);

      

       P8: ( card B) = (( card D0) + 1) by P5, P7, CARD_1: 5, WELLORD2:def 4;

      then

      reconsider B as finite set;

      reconsider B as finite Subset of V by P7, XBOOLE_1: 1;

      B is linearly-dependent by XXTh1, P8, AS;

      hence A is linearly-dependent by XXTh2, P7;

    end;

    theorem :: ZMODUL04:20

    for V be free Z_Module, I,A be Subset of V st I is Basis of V & I is finite & A is linearly-independent holds ( card A) c= ( card I) by XXTh3, XBOOLE_0:def 8;

    begin

    theorem :: ZMODUL04:21

    for V be Z_Module st ( (Omega). V) is free holds V is free

    proof

      let V be Z_Module such that

       A1: ( (Omega). V) is free;

      consider I be Subset of ( (Omega). V) such that

       a2: I is base by VECTSP_7:def 4, A1;

      

       A2: I is linearly-independent & ( (Omega). V) = ( Lin I) by a2, VECTSP_7:def 3;

      reconsider II = I as linearly-independent Subset of V by A2, ZMODUL03: 15;

      ( (Omega). V) = ( Lin II) by A2, ZMODUL03: 20;

      then II is base by VECTSP_7:def 3;

      hence thesis by VECTSP_7:def 4;

    end;

    theorem :: ZMODUL04:22

    for R be Ring holds for V be LeftMod of R, W1,W2 be Subspace of V, W1s,W2s be strict Subspace of V st W1s = ( (Omega). W1) & W2s = ( (Omega). W2) holds (W1s + W2s) = (W1 + W2)

    proof

      let R be Ring;

      let V be LeftMod of R, W1,W2 be Subspace of V, W1s,W2s be strict Subspace of V such that

       A1: W1s = ( (Omega). W1) & W2s = ( (Omega). W2);

      for x be Vector of V holds x in (W1 + W2) iff x in (W1s + W2s)

      proof

        let x be Vector of V;

        hereby

          assume x in (W1 + W2);

          then

          consider x1,x2 be Vector of V such that

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

          

           B2: x1 in W1s by A1, B1;

          x2 in W2s by A1, B1;

          hence x in (W1s + W2s) by B1, B2, VECTSP_5: 1;

        end;

        assume x in (W1s + W2s);

        then

        consider x1,x2 be Vector of V such that

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

        

         B2: x1 in W1 by A1, B1;

        x2 in W2 by A1, B1;

        hence x in (W1 + W2) by B1, B2, VECTSP_5: 1;

      end;

      hence (W1 + W2) = (W1s + W2s) by VECTSP_4: 30;

    end;

    theorem :: ZMODUL04:23

    for R be Ring holds for V be LeftMod of R, W1,W2 be Subspace of V, W1s,W2s be strict Subspace of V st W1s = ( (Omega). W1) & W2s = ( (Omega). W2) holds (W1s /\ W2s) = (W1 /\ W2)

    proof

      let R be Ring;

      let V be LeftMod of R, W1,W2 be Subspace of V, W1s,W2s be strict Subspace of V such that

       A1: W1s = ( (Omega). W1) & W2s = ( (Omega). W2);

      for x be Vector of V holds x in (W1 /\ W2) iff x in (W1s /\ W2s)

      proof

        let x be Vector of V;

        hereby

          assume x in (W1 /\ W2);

          then

           B1: x in W1 & x in W2 by VECTSP_5: 3;

          

           B2: x in W1s by A1, B1;

          x in W2s by A1, B1;

          hence x in (W1s /\ W2s) by B2, VECTSP_5: 3;

        end;

        assume

         B1: x in (W1s /\ W2s);

        x in the ModuleStr of W1 by A1, B1, VECTSP_5: 3;

        then

         B2: x in W1;

        x in the ModuleStr of W2 by A1, B1, VECTSP_5: 3;

        then x in W2;

        hence x in (W1 /\ W2) by B2, VECTSP_5: 3;

      end;

      hence (W1 /\ W2) = (W1s /\ W2s) by VECTSP_4: 30;

    end;

    theorem :: ZMODUL04:24

    

     Thn0V: for R be Ring holds for V be LeftMod of R, W be strict Subspace of V st W <> ( (0). V) holds ex v be Vector of V st v in W & v <> ( 0. V)

    proof

      let R be Ring;

      let V be LeftMod of R, W be strict Subspace of V such that

       A1: W <> ( (0). V);

      

       A2: ( 0. V) in W by VECTSP_4: 17;

      the carrier of W <> {( 0. V)} by A1, VECTSP_4:def 3;

      then {( 0. V)} c< the carrier of W by A2, ZFMISC_1: 31;

      then

      consider v be object such that

       A3: v in the carrier of W and

       A4: not v in {( 0. V)} by XBOOLE_0: 6;

      reconsider v as Vector of V by A3, VECTSP_4: 10;

      take v;

      thus thesis by A3, A4, TARSKI:def 1;

    end;

    theorem :: ZMODUL04:25

    

     ThCarrier1: for K be Ring holds for V be VectSp of K holds for A be Subset of V, l1,l2 be Linear_Combination of A st (( Carrier l1) /\ ( Carrier l2)) = {} holds ( Carrier (l1 + l2)) = (( Carrier l1) \/ ( Carrier l2))

    proof

      let K be Ring;

      let V be VectSp of K;

      let A be Subset of V, l1,l2 be Linear_Combination of A such that

       A0: (( Carrier l1) /\ ( Carrier l2)) = {} ;

      

       A1: ( Carrier l1) misses ( Carrier l2) by A0;

      (( Carrier l1) \/ ( Carrier l2)) c= ( Carrier (l1 + l2))

      proof

        let x be object;

        assume

         B1: x in (( Carrier l1) \/ ( Carrier l2));

        then

        reconsider x as Vector of V;

        per cases by B1, XBOOLE_0:def 3;

          suppose

           C1: x in ( Carrier l1);

          then not x in ( Carrier l2) by A1, B1, XBOOLE_0: 5;

          then

           C2: (l2 . x) = ( 0. K);

          ((l1 + l2) . x) = ((l1 . x) + (l2 . x)) by VECTSP_6: 22

          .= (l1 . x) by C2;

          then ((l1 + l2) . x) <> ( 0. K) by C1, VECTSP_6: 2;

          hence thesis;

        end;

          suppose

           C1: x in ( Carrier l2);

          then not x in ( Carrier l1) by A1, B1, XBOOLE_0: 5;

          then

           C2: (l1 . x) = ( 0. K);

          ((l1 + l2) . x) = ((l1 . x) + (l2 . x)) by VECTSP_6: 22

          .= (l2 . x) by C2;

          then ((l1 + l2) . x) <> ( 0. K) by C1, VECTSP_6: 2;

          hence thesis;

        end;

      end;

      hence thesis by VECTSP_6: 23;

    end;

    theorem :: ZMODUL04:26

    

     ThCarrier2: for R be Ring holds for V be VectSp of R holds for A1,A2 be Subset of V, l be Linear_Combination of (A1 \/ A2) st (A1 /\ A2) = {} holds ex l1 be Linear_Combination of A1, l2 be Linear_Combination of A2 st l = (l1 + l2)

    proof

      let K be Ring;

      let V be VectSp of K;

      let A1,A2 be Subset of V, l be Linear_Combination of (A1 \/ A2) such that

       A1: (A1 /\ A2) = {} ;

      

       A2: A1 misses A2 by A1;

      defpred P[ object, object] means $1 is Vector of V implies ($1 in A1 & $2 = (l . $1)) or ( not $1 in A1 & $2 = ( 0. K));

      

       A3: for x be object st x in the carrier of V holds ex y be object st y in the carrier of K & P[x, y]

      proof

        let x be object;

        assume x in the carrier of V;

        then

        reconsider x9 = x as Vector of V;

        per cases ;

          suppose

           B1: x in A1;

          (l . x9) in the carrier of K;

          hence thesis by B1;

        end;

          suppose not x in A1;

          hence thesis;

        end;

      end;

      ex l1 be Function of the carrier of V, the carrier of K st for x be object st x in the carrier of V holds P[x, (l1 . x)] from FUNCT_2:sch 1( A3);

      then

      consider l1 be Function of the carrier of V, the carrier of K such that

       A4: for x be object st x in the carrier of V holds P[x, (l1 . x)];

       A5:

      now

        let v be Vector of V;

        assume

         A6: not v in (A1 /\ ( Carrier l));

        per cases by A6, XBOOLE_0:def 4;

          suppose not v in A1;

          hence (l1 . v) = ( 0. K) by A4;

        end;

          suppose not v in ( Carrier l);

          then (l . v) = ( 0. K);

          hence (l1 . v) = ( 0. K) by A4;

        end;

      end;

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

      reconsider l1 as Linear_Combination of V by A5, VECTSP_6:def 1;

      for x be object holds x in ( Carrier l1) implies x in A1

      proof

        let x be object;

        assume

         B1: x in ( Carrier l1);

        then

        reconsider x as Vector of V;

        (l1 . x) <> ( 0. K) by B1, VECTSP_6: 2;

        hence thesis by A4;

      end;

      then

       AX1: l1 is Linear_Combination of A1 by TARSKI:def 3, VECTSP_6:def 4;

      defpred Q[ object, object] means $1 is Vector of V implies ($1 in A2 & $2 = (l . $1)) or ( not $1 in A2 & $2 = ( 0. K));

      

       A7: for x be object st x in the carrier of V holds ex y be object st y in the carrier of K & Q[x, y]

      proof

        let x be object;

        assume x in the carrier of V;

        then

        reconsider x9 = x as Vector of V;

        per cases ;

          suppose

           B1: x in A2;

          (l . x9) in the carrier of K;

          hence thesis by B1;

        end;

          suppose not x in A2;

          hence thesis;

        end;

      end;

      ex l2 be Function of the carrier of V, the carrier of K st for x be object st x in the carrier of V holds Q[x, (l2 . x)] from FUNCT_2:sch 1( A7);

      then

      consider l2 be Function of the carrier of V, the carrier of K such that

       A8: for x be object st x in the carrier of V holds Q[x, (l2 . x)];

       A9:

      now

        let v be Vector of V;

        assume

         A10: not v in (A2 /\ ( Carrier l));

        per cases by A10, XBOOLE_0:def 4;

          suppose not v in A2;

          hence (l2 . v) = ( 0. K) by A8;

        end;

          suppose not v in ( Carrier l);

          then (l . v) = ( 0. K);

          hence (l2 . v) = ( 0. K) by A8;

        end;

      end;

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

      reconsider l2 as Linear_Combination of V by A9, VECTSP_6:def 1;

      for x be object holds x in ( Carrier l2) implies x in A2

      proof

        let x be object;

        assume

         B1: x in ( Carrier l2);

        then

        reconsider x as Vector of V;

        (l2 . x) <> ( 0. K) by B1, VECTSP_6: 2;

        hence thesis by A8;

      end;

      then

       AX2: l2 is Linear_Combination of A2 by TARSKI:def 3, VECTSP_6:def 4;

      for v be Vector of V holds (l . v) = ((l1 + l2) . v)

      proof

        let v be Vector of V;

        per cases ;

          suppose

           B1: v in A1;

          then v in (A1 \/ A2) by XBOOLE_0:def 3;

          then

           B2: not v in A2 by A2, B1, XBOOLE_0: 5;

          

          thus (l . v) = ((l1 . v) + ( 0. K)) by A4, B1

          .= ((l1 . v) + (l2 . v)) by A8, B2

          .= ((l1 + l2) . v) by VECTSP_6: 22;

        end;

          suppose

           B1: v in A2;

          then v in (A1 \/ A2) by XBOOLE_0:def 3;

          then

           B2: not v in A1 by A2, B1, XBOOLE_0: 5;

          

          thus (l . v) = (( 0. K) + (l2 . v)) by A8, B1

          .= ((l1 . v) + (l2 . v)) by A4, B2

          .= ((l1 + l2) . v) by VECTSP_6: 22;

        end;

          suppose

           B1: not v in A1 & not v in A2;

          then not v in (A1 \/ A2) by XBOOLE_0:def 3;

          then not v in ( Carrier l) by TARSKI:def 3, VECTSP_6:def 4;

          

          hence (l . v) = ( 0. K)

          .= ((l1 . v) + ( 0. K)) by A4, B1

          .= ((l1 . v) + (l2 . v)) by A8, B1

          .= ((l1 + l2) . v) by VECTSP_6: 22;

        end;

      end;

      hence thesis by AX1, AX2, VECTSP_6:def 7;

    end;

    theorem :: ZMODUL04:27

    

     FRds1: for V be Z_Module, W1,W2 be free Subspace of V, I1 be Basis of W1, I2 be Basis of W2 st V is_the_direct_sum_of (W1,W2) holds (I1 /\ I2) = {}

    proof

      let V be Z_Module, W1,W2 be free Subspace of V, I1 be Basis of W1, I2 be Basis of W2 such that

       A1: V is_the_direct_sum_of (W1,W2);

      assume (I1 /\ I2) <> {} ;

      then

      consider v be object such that

       A2: v in (I1 /\ I2) by XBOOLE_0: 7;

      

       A3: v in I1 by A2, XBOOLE_0:def 4;

       not ( 0. W1) in I1 by ZMODUL02: 57, VECTSP_7:def 3;

      then

       A4: v <> ( 0. V) by A3, ZMODUL01: 26;

      

       A5: v in W1 by A3;

      v in W2 by A2;

      then

       W1: v in (W1 /\ W2) by A5, VECTSP_5: 3;

      (W1 /\ W2) = ( (0). V) by A1, VECTSP_5:def 4;

      then v in ( (0). V) by W1;

      hence contradiction by A4, ZMODUL02: 66;

    end;

    theorem :: ZMODUL04:28

    

     FRds2: for V be Z_Module, W1,W2 be free Subspace of V, I1 be Basis of W1, I2 be Basis of W2, I be Subset of V st V is_the_direct_sum_of (W1,W2) & I = (I1 \/ I2) holds ( Lin I) = the ModuleStr of V

    proof

      let V be Z_Module, W1,W2 be free Subspace of V, I1 be Basis of W1, I2 be Basis of W2, I be Subset of V such that

       A1: V is_the_direct_sum_of (W1,W2) and

       A2: I = (I1 \/ I2);

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

      then

      reconsider II1 = I1 as Subset of V by XBOOLE_1: 1;

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

      then

      reconsider II2 = I2 as Subset of V by XBOOLE_1: 1;

      

       A5: the ModuleStr of W1 = ( Lin I1) by VECTSP_7:def 3

      .= ( Lin II1) by ZMODUL03: 20;

      

       A6: the ModuleStr of W2 = ( Lin I2) by VECTSP_7:def 3

      .= ( Lin II2) by ZMODUL03: 20;

      for x be Vector of V holds x in (W1 + W2) iff x in (( Lin II1) + ( Lin II2))

      proof

        let x be Vector of V;

        hereby

          assume x in (W1 + W2);

          then

          consider x1,x2 be Vector of V such that

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

          

           B2: x1 in ( Lin II1) by A5, B1;

          x2 in ( Lin II2) by A6, B1;

          hence x in (( Lin II1) + ( Lin II2)) by B1, B2, VECTSP_5: 1;

        end;

        assume x in (( Lin II1) + ( Lin II2));

        then

        consider x1,x2 be Vector of V such that

         B1: x1 in ( Lin II1) & x2 in ( Lin II2) & x = (x1 + x2) by VECTSP_5: 1;

        

         B2: x1 in W1 by A5, B1;

        x2 in W2 by A6, B1;

        hence x in (W1 + W2) by B1, B2, VECTSP_5: 1;

      end;

      then

       A7: (W1 + W2) = (( Lin II1) + ( Lin II2)) by VECTSP_4: 30;

      

      thus the ModuleStr of V = (W1 + W2) by A1, VECTSP_5:def 4

      .= ( Lin I) by A2, A7, ZMODUL02: 72;

    end;

    theorem :: ZMODUL04:29

    

     FRds3: for V be LeftMod of INT.Ring , W1,W2 be free Subspace of V, I1 be Basis of W1, I2 be Basis of W2, I be Subset of V st V is_the_direct_sum_of (W1,W2) & I = (I1 \/ I2) holds I is linearly-independent

    proof

      let V be LeftMod of INT.Ring , W1,W2 be free Subspace of V, I1 be Basis of W1, I2 be Basis of W2, I be Subset of V such that

       A1: V is_the_direct_sum_of (W1,W2) and

       A2: I = (I1 \/ I2);

      assume I is linearly-dependent;

      then

      consider l be Linear_Combination of I such that

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

       A4: ( Carrier l) <> {} by VECTSP_7:def 1;

      

       A5A: (I1 /\ I2) = {} by A1, FRds1;

      then

       A5B: I1 misses I2;

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

      then

      reconsider II1 = I1, II2 = I2 as Subset of V by XBOOLE_1: 1;

      consider l1 be Linear_Combination of II1, l2 be Linear_Combination of II2 such that

       A6: l = (l1 + l2) by A2, A5A, ThCarrier2;

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

      reconsider ll2 = l2 as Linear_Combination of I by A2, XBOOLE_1: 7, ZMODUL02: 10;

      

       A7: ( Sum l) = (( Sum ll1) + ( Sum ll2)) by A6, ZMODUL02: 52;

      set v1 = ( Sum ll1);

      set v2 = ( Sum ll2);

      ( Carrier ll1) c= I1 & ( Carrier ll2) c= I2 by VECTSP_6:def 4;

      then

       A8: (( Carrier ll1) /\ ( Carrier ll2)) = {} by A5B, XBOOLE_0:def 7, XBOOLE_1: 64;

      

       A10: v1 <> ( 0. V)

      proof

        assume

         B1: v1 = ( 0. V);

        II1 is linearly-independent by VECTSP_7:def 3, ZMODUL03: 15;

        then

         B3: ( Carrier l1) = {} by B1, VECTSP_7:def 1;

        II2 is linearly-independent by VECTSP_7:def 3, ZMODUL03: 15;

        then (( Carrier ll1) \/ ( Carrier ll2)) = {} by A3, A7, B1, B3, VECTSP_7:def 1;

        hence contradiction by A4, A6, A8, ThCarrier1;

      end;

      

       A13: v1 = ( - v2) by A3, A7, RLVECT_1: 6;

      v1 in ( Lin II1) by ZMODUL02: 64;

      then v1 in ( Lin I1) by ZMODUL03: 20;

      then v1 in the ModuleStr of W1 by VECTSP_7:def 3;

      then

       A14: v1 in W1;

      v2 in ( Lin II2) by ZMODUL02: 64;

      then v2 in ( Lin I2) by ZMODUL03: 20;

      then v2 in the ModuleStr of W2 by VECTSP_7:def 3;

      then v2 in W2;

      then

       A15: v1 in W2 by A13, ZMODUL01: 38;

      (W1 /\ W2) = ( (0). V) by A1, VECTSP_5:def 4;

      hence contradiction by A10, A14, A15, VECTSP_5: 3, ZMODUL02: 66;

    end;

    theorem :: ZMODUL04:30

    

     FRdsX: for V be Z_Module, W1,W2 be free Subspace of V st V is_the_direct_sum_of (W1,W2) holds V is free

    proof

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

       A1: V is_the_direct_sum_of (W1,W2);

      set I1 = the Basis of W1;

      set I2 = the Basis of W2;

      set I = (I1 \/ I2);

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

      then

       A3: I1 is Subset of V by XBOOLE_1: 1;

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

      then I2 is Subset of V by XBOOLE_1: 1;

      then

      reconsider I as Subset of V by A3, XBOOLE_1: 8;

       the ModuleStr of V = ( Lin I) by A1, FRds2;

      then I is base by VECTSP_7:def 3, FRds3, A1;

      hence thesis by VECTSP_7:def 4;

    end;

    theorem :: ZMODUL04:31

    

     ThDirectSum: for V be Z_Module, W1,W2 be free Subspace of V st (W1 /\ W2) = ( (0). V) holds (W1 + W2) is free

    proof

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

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

      reconsider W = (W1 + W2) as strict Subspace of V;

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

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

      

       A2: (WW1 /\ WW2) is Subspace of V by ZMODUL01: 42;

      

       A3: (WW1 + WW2) is Subspace of V by ZMODUL01: 42;

      for x be object holds x in (WW1 /\ WW2) iff x in ( (0). V)

      proof

        let x be object;

        hereby

          assume x in (WW1 /\ WW2);

          then x in WW1 & x in WW2 by VECTSP_5: 3;

          hence x in ( (0). V) by P1, VECTSP_5: 3;

        end;

        assume x in ( (0). V);

        then x in W1 & x in W2 by P1, VECTSP_5: 3;

        hence x in (WW1 /\ WW2) by VECTSP_5: 3;

      end;

      then for x be Vector of V holds x in (WW1 /\ WW2) iff x in ( (0). V);

      

      then

       A4: (WW1 /\ WW2) = ( (0). V) by A2, VECTSP_4: 30

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

      for x be object holds x in W iff x in (WW1 + WW2)

      proof

        let x be object;

        hereby

          assume x in W;

          then

          consider x1,x2 be Vector of V such that

           B2: x1 in W1 & x2 in W2 & x = (x1 + x2) by VECTSP_5: 1;

          x1 in (W1 + W2) by B2, VECTSP_5: 2;

          then

          reconsider xx1 = x1 as Vector of W;

          x2 in (W1 + W2) by B2, VECTSP_5: 2;

          then

          reconsider xx2 = x2 as Vector of W;

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

          hence x in (WW1 + WW2) by B2, VECTSP_5: 1;

        end;

        assume x in (WW1 + WW2);

        then

        consider x1,x2 be Vector of W such that

         B2: x1 in WW1 & x2 in WW2 & x = (x1 + x2) by VECTSP_5: 1;

        thus x in W by B2;

      end;

      then for x be Vector of V holds x in W iff x in (WW1 + WW2);

      then W = (WW1 + WW2) by A3, VECTSP_4: 30;

      hence (W1 + W2) is free by A4, FRdsX, VECTSP_5:def 4;

    end;

    theorem :: ZMODUL04:32

    for V be free Z_Module, I be Basis of V, v be Vector of V st v in I holds ( Lin (I \ {v})) is free & ( Lin {v}) is free

    proof

      let V be free Z_Module, I be Basis of V, v be Vector of V such that

       A1: v in I;

      

       A2: I is linearly-independent by VECTSP_7:def 3;

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

      hence ( Lin (I \ {v})) is free;

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

      hence ( Lin {v}) is free;

    end;

    theorem :: ZMODUL04:33

    

     FRdsY: for V be free Z_Module, I be Basis of V, v be Vector of V st v in I holds V is_the_direct_sum_of (( Lin (I \ {v})),( Lin {v}))

    proof

      let V be free Z_Module, I be Basis of V, v be Vector of V such that

       A1: v in I;

      I = ((I \ {v}) \/ {v}) by A1, XBOOLE_1: 45, ZFMISC_1: 31;

      then ( Lin I) = (( Lin (I \ {v})) + ( Lin {v})) by ZMODUL02: 72;

      then

       A3: the ModuleStr of V = (( Lin (I \ {v})) + ( Lin {v})) by VECTSP_7:def 3;

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

      proof

        assume

         B1: (the carrier of ( Lin (I \ {v})) /\ the carrier of ( Lin {v})) <> {( 0. V)};

        ( 0. V) in (( Lin (I \ {v})) /\ ( Lin {v})) by ZMODUL01: 33;

        then ( 0. V) in (the carrier of ( Lin (I \ {v})) /\ the carrier of ( Lin {v})) by VECTSP_5:def 2;

        then {( 0. V)} c< (the carrier of ( Lin (I \ {v})) /\ the carrier of ( Lin {v})) by B1, ZFMISC_1: 31;

        then

        consider x be object such that

         B2: x in (the carrier of ( Lin (I \ {v})) /\ the carrier of ( Lin {v})) and

         B3: not x in {( 0. V)} by XBOOLE_0: 6;

        

         B4: x <> ( 0. V) by B3, TARSKI:def 1;

        

         B5: x in (( Lin (I \ {v})) /\ ( Lin {v})) by B2, VECTSP_5:def 2;

        then x in V by ZMODUL01: 24;

        then

        reconsider x as Vector of V;

        x in ( Lin (I \ {v})) by B5, VECTSP_5: 3;

        then

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

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

        

         B7: ( Carrier lx1) <> {} by B4, B6, ZMODUL02: 23;

        

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

        x in ( Lin {v}) by B5, VECTSP_5: 3;

        then

        consider lx2 be Linear_Combination of {v} such that

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

        

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

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

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

        ( Carrier lx1) misses ( Carrier lx2) by B8, B11, XBOOLE_1: 64, XBOOLE_1: 79;

        then (( Carrier lx1) /\ ( Carrier lx2)) = {} ;

        then

         B12: ( Carrier (llx1 + llx2)) = (( Carrier llx1) \/ ( Carrier llx2)) by ThCarrier1;

        

         B13: (( Sum llx1) + ( Sum llx2)) = ( 0. V) by B6, B9, RLVECT_1: 5;

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

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

        hence contradiction by B7, B12, VECTSP_7:def 1, VECTSP_7:def 3;

      end;

      then (( Lin (I \ {v})) /\ ( Lin {v})) = ( (0). V) by VECTSP_4:def 3, VECTSP_5:def 2;

      hence thesis by A3, VECTSP_5:def 4;

    end;

    

     FRX: for V be finite-rank free Z_Module, W be Subspace of V holds W is free

    proof

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

      

       A1: P[ 0 ]

      proof

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

         B1: ( rank V) = 0 ;

        set I = the Basis of V;

        set sW = the ModuleStr of W;

        

         B2: sW = ( (Omega). W);

        

         B3: ( card I) = 0 by B1, ZMODUL03:def 5;

        then

         B31: I = ( {} the carrier of V);

         the ModuleStr of V = ( Lin I) by VECTSP_7:def 3

        .= ( (0). V) by B31, ZMODUL02: 67;

        then the carrier of V = {( 0. V)} by VECTSP_4:def 3;

        then the carrier of W c= {( 0. V)} by VECTSP_4:def 2;

        then

         B5: the carrier of W c= {( 0. W)} by ZMODUL01: 26;

        

         B6: I = ( {} the carrier of W) by B3;

        then

        reconsider II = I as Subset of W;

        II = ( {} the carrier of W) by B6;

        then

         AA: II is linearly-independent;

        sW = ( (0). W) by B2, B5, XBOOLE_0:def 10, VECTSP_4:def 3

        .= ( Lin II) by B6, ZMODUL02: 67;

        then ( Lin II) = the ModuleStr of W;

        then II is base by VECTSP_7:def 3, AA;

        then W is free by VECTSP_7:def 4;

        hence thesis;

      end;

      

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

      proof

        let n be Nat such that

         B1: P[n];

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

         B2: ( rank V) = (n + 1);

        set I = the Basis of V;

        

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

        ( card I) > 0 by B2, ZMODUL03:def 5;

        then I <> {} ;

        then

        consider v be object such that

         B4: v in I by XBOOLE_0: 7;

        reconsider v as Vector of V by B4;

        set Iv = (I \ {v});

        

         B22: {v} is Subset of I by B4, SUBSET_1: 41;

        

        then

         B5: ( card Iv) = ((n + 1) - ( card {v})) by B3, CARD_2: 44

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

        .= n;

        I is linearly-independent by VECTSP_7:def 3;

        then

         B6: Iv is linearly-independent by XBOOLE_1: 36, ZMODUL02: 56;

        set Vv = ( Lin Iv);

        reconsider VVv = Vv as finite-rank free Z_Module by B6;

        for x be object holds x in Iv implies x in the carrier of VVv by STRUCT_0:def 5, ZMODUL02: 65;

        then

        reconsider IIv = Iv as linearly-independent Subset of VVv by B6, TARSKI:def 3, ZMODUL03: 16;

        ( Lin Iv) = ( Lin IIv) by ZMODUL03: 20;

        then IIv is Basis of VVv by VECTSP_7:def 3;

        then

         B8: ( rank VVv) = n by B5, ZMODUL03:def 5;

        set Wv = (W /\ Vv);

        reconsider WWv = (W /\ Vv) as Subspace of Vv by ZMODUL01: 105;

        reconsider WWv as free Subspace of Vv by B1, B8;

        set IIwv = the Basis of WWv;

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

        then

        reconsider Iwv = IIwv as Subset of V by XBOOLE_1: 1;

        

         B13: V is_the_direct_sum_of (Vv,( Lin {v})) by B4, FRdsY;

        set B = { (l . v) where l be Linear_Combination of I : ( Sum l) in W };

        

         B15: B c= INT

        proof

          let b be object such that

           CX1: b in B;

          consider l be Linear_Combination of I such that

           CX2: (l . v) = b & ( Sum l) in W by CX1;

          thus b in INT by CX2;

        end;

        

         B16: for b1,b2 be Element of INT st b1 in B & b2 in B holds (b1 + b2) in B

        proof

          let b1,b2 be Element of INT such that

           C1: b1 in B & b2 in B;

          set bb1 = b1, bb2 = b2;

          consider l1 be Linear_Combination of I such that

           C3: (l1 . v) = bb1 & ( Sum l1) in W by C1;

          consider l2 be Linear_Combination of I such that

           C4: (l2 . v) = bb2 & ( Sum l2) in W by C1;

          (( Sum l1) + ( Sum l2)) = ( Sum (l1 + l2)) by ZMODUL02: 52;

          then

           C5: ( Sum (l1 + l2)) in W by C3, C4, ZMODUL01: 36;

          (l1 + l2) is Linear_Combination of I by ZMODUL02: 27;

          then ((l1 + l2) . v) in B by C5;

          then ((l1 . v) + (l2 . v)) in B by VECTSP_6: 22;

          then (b1 + b2) in B by C3, C4;

          hence thesis;

        end;

        

         B17: 0 in B

        proof

          set wv = the Element of Wv;

          wv in WWv;

          then

          consider lwv be Linear_Combination of Iv such that

           C2: wv = ( Sum lwv) by ZMODUL01: 23, ZMODUL02: 64;

          ( Carrier lwv) c= Iv by VECTSP_6:def 4;

          then not v in ( Carrier lwv) by ZFMISC_1: 56;

          then

           C4: (lwv . v) = 0 ;

          wv in (Vv /\ W);

          then

           C5: wv in W by VECTSP_5: 3;

          lwv is Linear_Combination of I by XBOOLE_1: 36, ZMODUL02: 10;

          hence 0 in B by C2, C4, C5;

        end;

        

         B18: for b be Element of INT st b in B holds ( - b) in B

        proof

          let b be Element of INT such that

           C1: b in B;

          consider l be Linear_Combination of I such that

           C2: (l . v) = b & ( Sum l) in W by C1;

          ( - ( Sum l)) in W by C2, ZMODUL01: 38;

          then

           C3: ( Sum ( - l)) in W by ZMODUL02: 54;

          consider bm be Element of INT.Ring such that

           C4: bm = (( - l) . v);

          reconsider bb = b as Element of INT.Ring ;

          bm = ( - bb) by C2, C4, VECTSP_6: 36;

          then

           C5: bm = ( - b);

          ( - l) is Linear_Combination of I by ZMODUL02: 38;

          hence thesis by C3, C4, C5;

        end;

        

         B19: for b be Element of INT st b in B holds for i be Element of INT holds (i * b) in B

        proof

          let b be Element of INT such that

           C1: b in B;

          defpred Q[ Integer] means ($1 * b) in B;

          

           C2: Q[ 0 ] by B17;

          

           C3: for i be Integer st Q[i] holds Q[(i - 1)] & Q[(i + 1)]

          proof

            let i be Integer such that

             D1: Q[i];

            

             D3: ( - b) in B by B18, C1;

            (i * b) is Element of INT & ( - b) is Element of INT by INT_1:def 2;

            then ((i * b) + ( - b)) in B by B16, D1, D3;

            hence Q[(i - 1)];

            (i * b) is Element of INT by INT_1:def 2;

            then ((i * b) + b) in B by B16, C1, D1;

            hence Q[(i + 1)];

          end;

          for i be Integer holds Q[i] from INT_1:sch 4( C2, C3);

          hence thesis;

        end;

        set BP = (B /\ NAT );

        ex p be Element of INT st p in B & for b be Element of INT st b in B holds p divides b

        proof

          

           C2: BP is non empty by B17, XBOOLE_0:def 4;

          

           C5: BP c= NAT by XBOOLE_1: 17;

          set BPN = (BP \ { 0 });

          per cases ;

            suppose BPN = {} ;

            then

             D1: BP = { 0 } by C2, ZFMISC_1: 58;

            

             D2: for b be object st b in B holds b = 0

            proof

              let b be object such that

               E1: b in B;

              reconsider bb = b as Element of INT by B15, E1;

              assume

               E2: b <> 0 ;

              per cases ;

                suppose bb > 0 ;

                then bb in NAT by INT_1: 3;

                then bb in BP by E1, XBOOLE_0:def 4;

                hence contradiction by D1, E2, TARSKI:def 1;

              end;

                suppose bb < 0 ;

                then

                 F1: ( - bb) in NAT by INT_1: 3;

                ( - bb) in B by B18, E1;

                then ( - bb) in BP by F1, XBOOLE_0:def 4;

                hence contradiction by D1, E2, TARSKI:def 1;

              end;

            end;

            set p = 0 ;

            reconsider p as Element of INT by INT_1:def 2;

            take p;

            thus thesis by B17, D2;

          end;

            suppose BPN <> {} ;

            then

            reconsider BPN as non empty Subset of NAT by C5, XBOOLE_1: 1;

            set p = ( min* BPN);

            

             D1: p in BPN by NAT_1:def 1;

            then

             D2: p in B by XBOOLE_0:def 4;

            

             D4: p <> 0 & p is Element of NAT by D1, ZFMISC_1: 56;

            

             D5: for b be Element of INT st b in BP holds p divides b

            proof

              let b be Element of INT such that

               E1: b in BP;

              assume

               E2: not p divides b;

              set r = (b mod p);

              reconsider r as Element of NAT by INT_1: 3, INT_1: 57;

              

               E3: r <> 0 by D4, E2, INT_1: 62;

              

               E4: r in BPN

              proof

                set q = (b div p);

                reconsider q as Element of INT by INT_1:def 2;

                

                 F1: b = ((q * p) + r) by D4, INT_1: 59;

                

                 F2: b in B by E1, XBOOLE_0:def 4;

                

                 F3: (q * p) is Element of INT by INT_1:def 2;

                p is Element of INT by INT_1:def 2;

                then

                 F5: ( - (q * p)) in B by B18, B19, D2, F3;

                ( - (q * p)) is Element of INT by INT_1:def 2;

                then (b + ( - (q * p))) in B by B16, F2, F5;

                then r in BP by F1, XBOOLE_0:def 4;

                hence thesis by E3, ZFMISC_1: 56;

              end;

              r < p by D4, INT_1: 58;

              hence contradiction by E4, NAT_1:def 1;

            end;

            

             D6: for b be Element of INT st b in B holds p divides b

            proof

              let b be Element of INT such that

               E1: b in B;

              assume

               E2: not p divides b;

              per cases ;

                suppose b >= 0 ;

                then b in NAT by INT_1: 3;

                then b in BP by E1, XBOOLE_0:def 4;

                hence contradiction by D5, E2;

              end;

                suppose b < 0 ;

                then

                 F1: ( - b) in NAT by INT_1: 3;

                ( - b) in B by B18, E1;

                then

                 F2: ( - b) in BP by F1, XBOOLE_0:def 4;

                ( - b) is Element of INT by INT_1:def 2;

                hence contradiction by D5, E2, F2, INT_2: 10;

              end;

            end;

            reconsider p as Element of INT by INT_1:def 1;

            take p;

            thus thesis by D1, D6, XBOOLE_0:def 4;

          end;

        end;

        then

        consider p be Element of INT such that

         B20: p in B and

         B21: for b be Element of INT st b in B holds p divides b;

        reconsider pp = p as Element of INT.Ring ;

        set Ws = ModuleStr (# the carrier of W, the addF of W, the ZeroF of W, the lmult of W #);

        Ws is Subspace of V

        proof

          

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

          

           C3: ( 0. Ws) = ( 0. W)

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

          

           C4: the addF of Ws = (the addF of V || the carrier of Ws) by VECTSP_4:def 2;

          the lmult of Ws = (the lmult of V | [: INT , the carrier of Ws:]) by VECTSP_4:def 2;

          hence thesis by C2, C3, C4, ZMODUL01: 40;

        end;

        then

        reconsider Ws as strict Subspace of V;

        

         B24: for w be Vector of V holds w in Ws iff w in W;

        per cases ;

          suppose p = ( 0. INT.Ring );

          then

           C2: for b be Element of INT holds b in B implies b = 0 by B21, INT_2: 3;

          for w be Vector of V st w in W holds w in Vv

          proof

            let w be Vector of V such that

             D1: w in W;

             the ModuleStr of V = ( Lin I) by VECTSP_7:def 3;

            then w in ( Lin I);

            then

            consider lw be Linear_Combination of I such that

             D2: w = ( Sum lw) by ZMODUL02: 64;

            (lw . v) in B by D1, D2;

            then not v in ( Carrier lw) by C2, ZMODUL02: 8;

            then ( Carrier lw) c= (I \ {v}) by ZFMISC_1: 34, VECTSP_6:def 4;

            then lw is Linear_Combination of Iv by VECTSP_6:def 4;

            hence thesis by D2, ZMODUL02: 64;

          end;

          then for w be Vector of V st w in Ws holds w in Vv by B24;

          then

           C4: Ws is Subspace of Vv by ZMODUL01: 44;

          Ws is free by B1, B8, C4;

          then

          consider Iws be Subset of Ws such that

           c5: Iws is base by VECTSP_7:def 4;

          

           C5: Iws is linearly-independent & ( Lin Iws) = the ModuleStr of Ws by c5, VECTSP_7:def 3;

          reconsider IwsV = Iws as linearly-independent Subset of V by C5, ZMODUL03: 15;

          reconsider IwsW = IwsV as linearly-independent Subset of W by ZMODUL03: 16;

          ( Lin IwsW) = ( Lin IwsV) by ZMODUL03: 20

          .= the ModuleStr of W by C5, ZMODUL03: 20;

          then IwsW is base by VECTSP_7:def 3;

          hence thesis by VECTSP_7:def 4;

        end;

          suppose

           C1: p <> ( 0. INT.Ring );

          consider lwpv be Linear_Combination of I such that

           C2: (lwpv . v) = p & ( Sum lwpv) in W by B20;

          set wpv = ( Sum lwpv);

          set vpv = (wpv - (pp * v));

          consider lv be Linear_Combination of V such that

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

          

           C4: ( Carrier lv) = {v}

          proof

            for u be object holds u in ( Carrier lv) implies u in {v}

            proof

              assume ex u be object st u in ( Carrier lv) & not u in {v};

              then

              consider u be Vector of V such that

               D1: u in ( Carrier lv) & not u in {v};

              u <> v by D1, TARSKI:def 1;

              then (lv . u) = 0 by C3;

              hence contradiction by D1, ZMODUL02: 8;

            end;

            then

             D2: ( Carrier lv) c= {v} by TARSKI:def 3;

            v in ( Carrier lv) by C3;

            then {v} c= ( Carrier lv) by ZFMISC_1: 31;

            hence thesis by D2;

          end;

          then

           C18: ( Sum lv) = ((lv . v) * v) by ZMODUL02: 24;

          

          then

           C5: ( Sum (pp * lv)) = (pp * ((lv . v) * v)) by ZMODUL02: 53

          .= (pp * v) by C3, VECTSP_1:def 17;

          lv is Linear_Combination of {v} by C4, VECTSP_6:def 4;

          then (pp * lv) is Linear_Combination of {v} by ZMODUL02: 31;

          then

           C6: (pp * v) in ( Lin {v}) by C5, ZMODUL02: 64;

          

           C17: v <> ( 0. V) by B22, ZMODUL02: 56, VECTSP_7:def 3;

          

           C8: not (pp * v) in Vv

          proof

            assume (pp * v) in Vv;

            then (pp * v) in (Vv /\ ( Lin {v})) by C6, VECTSP_5: 3;

            then (pp * v) in ( (0). V) by B13, VECTSP_5:def 4;

            hence contradiction by C1, C17, ZMODUL01:def 7, ZMODUL02: 66;

          end;

          

           C9: vpv in Vv

          proof

             the ModuleStr of V = ( Lin I) by VECTSP_7:def 3;

            then vpv in ( Lin I);

            then

            consider lvpv be Linear_Combination of I such that

             D2: vpv = ( Sum lvpv) by ZMODUL02: 64;

            ( Carrier (pp * lv)) = {v} by C1, C4, ZMODUL02: 29;

            then

            reconsider lpv = (pp * lv) as Linear_Combination of I by B4, ZFMISC_1: 31, VECTSP_6:def 4;

            

             D3: ( Sum lvpv) = ( Sum (lwpv - lpv)) by C5, D2, ZMODUL02: 55;

            (lwpv - lpv) is Linear_Combination of I by ZMODUL02: 41;

            then ( Carrier lvpv) c= I & ( Carrier (lwpv - lpv)) c= I by VECTSP_6:def 4;

            then lvpv = (lwpv - lpv) by D3, VECTSP_7:def 3, ZMODUL03: 3;

            

            then (lvpv . v) = ((lwpv . v) - (lpv . v)) by ZMODUL02: 39

            .= ((lwpv . v) - (pp * (lv . v))) by VECTSP_6:def 9

            .= 0 by C2, C3;

            then not v in ( Carrier lvpv) by ZMODUL02: 8;

            then ( Carrier lvpv) c= Iv by ZFMISC_1: 34, VECTSP_6:def 4;

            then

            reconsider lvvpv = lvpv as Linear_Combination of Iv by VECTSP_6:def 4;

            vpv = ( Sum lvvpv) by D2;

            hence thesis by ZMODUL02: 64;

          end;

          reconsider wpv as Vector of V;

          set Iw = (Iwv \/ {wpv});

          

           C10: wpv <> ( 0. V)

          proof

            assume wpv = ( 0. V);

            then ( - ( - (pp * v))) in Vv by C9, ZMODUL01: 38;

            hence contradiction by C8;

          end;

          set WX = (Wv + ( Lin {wpv}));

          reconsider WXv = WWv as Subspace of WX by ZMODUL01: 97;

          reconsider Xwpv = ( Lin {wpv}) as Subspace of WX by ZMODUL01: 97;

          

           C11: not wpv in Iwv

          proof

            assume wpv in Iwv;

            then wpv in WWv;

            then

             D2: wpv in Vv by ZMODUL01: 23;

            (wpv - vpv) = ((wpv - wpv) + (pp * v)) by RLVECT_1: 29

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

            .= (pp * v);

            hence contradiction by C8, C9, D2, ZMODUL01: 39;

          end;

          

           C12: WX = (WXv + Xwpv)

          proof

            

             D1: (Iwv /\ {wpv}) = {} by C11, XBOOLE_0:def 7, ZFMISC_1: 50;

            for x be Vector of WX holds ex x1,x2 be Vector of WX st x1 in WXv & x2 in Xwpv & x = (x1 + x2)

            proof

              let x be Vector of WX;

              

               E1: Wv = ( Lin IIwv) by VECTSP_7:def 3

              .= ( Lin Iwv) by ZMODUL03: 20;

              WX = ( Lin (Iwv \/ {wpv})) by E1, ZMODUL02: 72;

              then x in ( Lin (Iwv \/ {wpv}));

              then

              consider lx be Linear_Combination of (Iwv \/ {wpv}) such that

               E3: x = ( Sum lx) by ZMODUL02: 64;

              consider lx1 be Linear_Combination of Iwv, lx2 be Linear_Combination of {wpv} such that

               E4: lx = (lx1 + lx2) by D1, ThCarrier2;

              set x1 = ( Sum lx1);

              set x2 = ( Sum lx2);

              x1 in WXv by E1, ZMODUL02: 64;

              then x1 in WX by ZMODUL01: 24;

              then

              reconsider xx1 = x1 as Vector of WX;

              x2 in Xwpv by ZMODUL02: 64;

              then x2 in WX by ZMODUL01: 24;

              then

              reconsider xx2 = x2 as Vector of WX;

              

               E5: (x1 + x2) = x by E3, E4, ZMODUL02: 52;

              take xx1, xx2;

              thus thesis by E1, E5, ZMODUL01: 28, ZMODUL02: 64;

            end;

            hence thesis by ZMODUL01: 133;

          end;

          

           C15: {wpv} is linearly-independent by C10, ZMODUL02: 59;

          (WXv /\ Xwpv) = ( (0). WX)

          proof

            assume (WXv /\ Xwpv) <> ( (0). WX);

            then

            consider x be Vector of WX such that

             D2: x in (WXv /\ Xwpv) & x <> ( 0. WX) by Thn0V;

            

             D3: x in WXv by D2, VECTSP_5: 3;

            x in ( Lin {wpv}) by D2, VECTSP_5: 3;

            then

            consider lx be Linear_Combination of {wpv} such that

             D5: x = ( Sum lx) by ZMODUL02: 64;

            x in V by D3, ZMODUL01: 24;

            then

            reconsider xx = x as Vector of V;

            x in WWv by D2, VECTSP_5: 3;

            then

             D9: x in Vv by ZMODUL01: 23;

            

             D6: x = ((lx . wpv) * wpv) by D5, ZMODUL02: 21;

            

             D7: (lx . wpv) <> 0

            proof

              assume (lx . wpv) = 0 ;

              

              then x = ( 0. V) by D6, ZMODUL01: 1

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

              hence contradiction by D2;

            end;

            (vpv + (pp * v)) = (wpv - ((pp * v) - (pp * v))) by RLVECT_1: 29

            .= (wpv - ( 0. V)) by RLVECT_1: 15

            .= wpv;

            

            then x = (((lx . wpv) * vpv) + ((lx . wpv) * (pp * v))) by D6, VECTSP_1:def 14

            .= (((lx . wpv) * vpv) + (((lx . wpv) * pp) * v)) by VECTSP_1:def 16;

            

            then

             D8: (xx - ((lx . wpv) * vpv)) = ((((lx . wpv) * pp) * v) + (((lx . wpv) * vpv) - ((lx . wpv) * vpv))) by RLVECT_1: 28

            .= ((((lx . wpv) * pp) * v) + ( 0. V)) by RLVECT_1: 15

            .= (((lx . wpv) * pp) * v);

            ((lx . wpv) * vpv) in Vv by C9, ZMODUL01: 37;

            then

             D10: (((lx . wpv) * pp) * v) in Vv by D8, D9, ZMODUL01: 39;

            

             D11: ( Sum (((lx . wpv) * pp) * lv)) = (((lx . wpv) * pp) * ((lv . v) * v)) by C18, ZMODUL02: 53

            .= (((lx . wpv) * pp) * v) by C3, VECTSP_1:def 17;

            lv is Linear_Combination of {v} by C4, VECTSP_6:def 4;

            then (((lx . wpv) * pp) * lv) is Linear_Combination of {v} by ZMODUL02: 31;

            then (((lx . wpv) * pp) * v) in ( Lin {v}) by D11, ZMODUL02: 64;

            then (((lx . wpv) * pp) * v) in (Vv /\ ( Lin {v})) by D10, VECTSP_5: 3;

            then (((lx . wpv) * pp) * v) in ( (0). V) by B13, VECTSP_5:def 4;

            hence contradiction by C1, C17, D7, ZMODUL01:def 7, ZMODUL02: 66;

          end;

          then

           C17: WX is free by C12, C15, FRdsX, VECTSP_5:def 4;

          for x be Vector of V holds x in W iff x in WX

          proof

            let x be Vector of V;

            hereby

              assume

               D1: x in W;

               the ModuleStr of V = ( Lin I) by VECTSP_7:def 3;

              then x in ( Lin I);

              then

              consider lx be Linear_Combination of I such that

               D2: x = ( Sum lx) by ZMODUL02: 64;

              (lx . v) in B by D1, D2;

              then

              consider y be Integer such that

               D4: (lx . v) = (p * y) by B21, INT_1:def 3;

              reconsider y as Element of INT.Ring by Lem1;

              (y * wpv) in W by C2, ZMODUL01: 37;

              then

               E3: (x - (y * wpv)) in W by D1, ZMODUL01: 39;

              (x - (y * wpv)) in Vv

              proof

                

                 F2: (y * wpv) = ( Sum (y * lwpv)) by ZMODUL02: 53;

                ((lx - (y * lwpv)) . v) = ((lx . v) - ((y * lwpv) . v)) by ZMODUL02: 39

                .= ((pp * y) - (y * (lwpv . v))) by D4, VECTSP_6:def 9

                .= 0 by C2;

                then

                 F3: not v in ( Carrier (lx - (y * lwpv))) by ZMODUL02: 8;

                (y * lwpv) is Linear_Combination of I by ZMODUL02: 31;

                then (lx - (y * lwpv)) is Linear_Combination of I by ZMODUL02: 41;

                then ( Carrier (lx - (y * lwpv))) c= Iv by F3, ZFMISC_1: 34, VECTSP_6:def 4;

                then

                reconsider lxy = (lx - (y * lwpv)) as Linear_Combination of Iv by VECTSP_6:def 4;

                (x - (y * wpv)) = ( Sum lxy) by D2, F2, ZMODUL02: 55;

                hence thesis by ZMODUL02: 64;

              end;

              then

               E4: (x - (y * wpv)) in Wv by E3, VECTSP_5: 3;

              wpv in {wpv} by TARSKI:def 1;

              then

               E5: (y * wpv) in ( Lin {wpv}) by ZMODUL01: 37, ZMODUL02: 65;

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

              .= (x - ( 0. V)) by RLVECT_1: 5

              .= x;

              hence x in WX by E4, E5, VECTSP_5: 1;

            end;

            assume

             D1: x in WX;

            

             D2: Wv is Subspace of W by ZMODUL01: 105;

            ( Lin {wpv}) is Subspace of W by C2, ZFMISC_1: 31, ZMODUL03: 19;

            then WX is Subspace of W by D2, ZMODUL02: 76;

            hence x in W by D1, ZMODUL01: 23;

          end;

          then for x be Vector of V holds x in Ws iff x in WX by B24;

          then Ws is free by C17, VECTSP_4: 30;

          then

          consider Iws be Subset of Ws such that

           c18: Iws is base by VECTSP_7:def 4;

          

           C18: Iws is linearly-independent & ( Lin Iws) = the ModuleStr of Ws by VECTSP_7:def 3, c18;

          reconsider IwsV = Iws as linearly-independent Subset of V by C18, ZMODUL03: 15;

          reconsider IwsW = IwsV as linearly-independent Subset of W by ZMODUL03: 16;

          ( Lin IwsW) = ( Lin IwsV) by ZMODUL03: 20

          .= the ModuleStr of W by C18, ZMODUL03: 20;

          then IwsW is base by VECTSP_7:def 3;

          hence thesis by VECTSP_7:def 4;

        end;

      end;

      

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

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

      set n = ( rank V);

       P[n] by A3;

      hence thesis;

    end;

    registration

      let V be finite-rank free Z_Module;

      cluster -> free for Subspace of V;

      correctness by FRX;

    end

    theorem :: ZMODUL04:34

    for V be Z_Module, W be Subspace of V, W1,W2 be free Subspace of V st (W1 /\ W2) = ( (0). V) & the ModuleStr of W = (W1 + W2) holds W is free

    proof

      let V be Z_Module, W be Subspace of V, W1,W2 be free Subspace of V such that

       A1: (W1 /\ W2) = ( (0). V) & the ModuleStr of W = (W1 + W2);

      reconsider Ws = (W1 + W2) as free Subspace of V by A1, ThDirectSum;

      consider I be Subset of Ws such that

       a3: I is base by VECTSP_7:def 4;

      

       A3: I is linearly-independent & Ws = ( Lin I) by VECTSP_7:def 3, a3;

      reconsider IV = I as linearly-independent Subset of V by A3, ZMODUL03: 15;

      reconsider IW = IV as linearly-independent Subset of W by A1, ZMODUL03: 16;

       the ModuleStr of W = ( Lin IV) by A1, A3, ZMODUL03: 20

      .= ( Lin IW) by ZMODUL03: 20;

      then IW is base by VECTSP_7:def 3;

      hence thesis by VECTSP_7:def 4;

    end;

    theorem :: ZMODUL04:35

    for p be prime Element of INT.Ring , V be free Z_Module st ( Z_MQ_VectSp (V,p)) is finite-dimensional holds V is finite-rank

    proof

      let p be prime Element of INT.Ring , V be free Z_Module such that

       A1: ( Z_MQ_VectSp (V,p)) is finite-dimensional;

      set I = the Basis of V;

      set IQ = { ( ZMtoMQV (V,p,u)) where u be Vector of V : u in I };

      now

        let x be object;

        assume x in IQ;

        then

        consider v be Vector of V such that

         B1: x = ( ZMtoMQV (V,p,v)) & v in I;

        thus x in the carrier of ( Z_MQ_VectSp (V,p)) by B1;

      end;

      then

      reconsider IQ as Subset of ( Z_MQ_VectSp (V,p)) by TARSKI:def 3;

      

       A3: IQ is Basis of ( Z_MQ_VectSp (V,p)) by ZMODUL03: 35;

      

       A2: ( card IQ) = ( card I) by ZMODUL03: 26;

      IQ is finite by A1, A3, VECTSP_9: 20;

      then I is finite by A2;

      hence thesis by ZMODUL03:def 3;

    end;

    theorem :: ZMODUL04:36

    for p be prime Element of INT.Ring , V be Z_Module, s be Element of V, a be Element of INT.Ring , b be Element of ( GF p) st b = (a mod p) holds (b * ( ZMtoMQV (V,p,s))) = ( ZMtoMQV (V,p,(a * s)))

    proof

      let p be prime Element of INT.Ring , V be Z_Module, s be Element of V, a be Element of INT.Ring , b be Element of ( GF p) such that

       A1: b = (a mod p);

      

       A2: ( ZMtoMQV (V,p,s)) = (s + (p (*) V));

      set t = ( ZMtoMQV (V,p,s));

      reconsider t1 = t as Element of ( VectQuot (V,(p (*) V)));

      

       A3: (s + (p (*) V)) is Element of ( CosetSet (V,(p (*) V))) by A2, VECTSP10:def 6;

      reconsider i = b as Nat;

      

      thus (b * t) = ((a mod p) * t1) by A1, ZMODUL02:def 11

      .= (a * t1) by ZMODUL02: 2

      .= (( lmultCoset (V,(p (*) V))) . (a,(s + (p (*) V)))) by VECTSP10:def 6

      .= ( ZMtoMQV (V,p,(a * s))) by A3, VECTSP10:def 5;

    end;

    

     LMX2: for p be prime Element of INT.Ring , V be free Z_Module, i be Element of INT.Ring , v be Element of V holds ( ZMtoMQV (V,p,((i mod p) * v))) = ( ZMtoMQV (V,p,(i * v)))

    proof

      let p be prime Element of INT.Ring , V be free Z_Module, i be Element of INT.Ring , v be Element of V;

      reconsider a = (i mod p) as Element of ( GF p) by EC_PF_1: 14;

      reconsider t1 = ( ZMtoMQV (V,p,v)) as Element of ( Z_MQ_VectSp (V,p));

      reconsider t1 as Element of ( VectQuot (V,(p (*) V)));

      ( ZMtoMQV (V,p,v)) = (v + (p (*) V));

      then

       Q1: (v + (p (*) V)) is Element of ( CosetSet (V,(p (*) V))) by VECTSP10:def 6;

      

      thus ( ZMtoMQV (V,p,((i mod p) * v))) = (a * ( ZMtoMQV (V,p,v))) by ZMODUL03: 30

      .= ((i mod p) * t1) by ZMODUL02:def 11

      .= (i * t1) by ZMODUL02: 2

      .= (( lmultCoset (V,(p (*) V))) . (i,t1)) by VECTSP10:def 6

      .= ( ZMtoMQV (V,p,(i * v))) by Q1, VECTSP10:def 5;

    end;

    theorem :: ZMODUL04:37

    

     ThQuotBasis5A: for p be prime Element of INT.Ring , V be free Z_Module, I be Subset of V, IQ be Subset of ( Z_MQ_VectSp (V,p)), l be Linear_Combination of I st IQ = { ( ZMtoMQV (V,p,u)) where u be Vector of V : u in I } holds ( ZMtoMQV (V,p,( Sum l))) in ( Lin IQ)

    proof

      let p be prime Element of INT.Ring , V be free Z_Module, I be Subset of V, IQ be Subset of ( Z_MQ_VectSp (V,p)), l be Linear_Combination of I;

      assume

       AS: IQ = { ( ZMtoMQV (V,p,u)) where u be Vector of V : u in I };

      consider G be FinSequence of V such that

       P1: G is one-to-one & ( rng G) = ( Carrier l) & ( Sum l) = ( Sum (l (#) G)) by VECTSP_6:def 6;

      now

        let i be Element of NAT ;

        assume i in ( dom (l (#) G));

        then i in ( Seg ( len (l (#) G))) by FINSEQ_1:def 3;

        then i in ( Seg ( len G)) by VECTSP_6:def 5;

        then

         Y3: i in ( dom G) by FINSEQ_1:def 3;

        then (G . i) in ( rng G) by FUNCT_1: 3;

        then

        reconsider v = (G . i) as Element of V;

        

         Y5: ((l (#) G) . i) = ((l . v) * v) by Y3, ZMODUL02: 13;

        reconsider b = ((l . v) mod p) as Element of ( GF p) by EC_PF_1: 14;

        reconsider a = ((l . v) mod p) as Element of INT.Ring ;

        reconsider k = (l . v) as Element of INT.Ring ;

        reconsider si = ((l . v) * v) as Element of V;

        reconsider t = ( ZMtoMQV (V,p,v)) as Element of ( Z_MQ_VectSp (V,p));

        

         Y7: (b * t) = ( ZMtoMQV (V,p,(a * v))) by ZMODUL03: 30

        .= ( ZMtoMQV (V,p,(k * v))) by LMX2;

        

         H1: v in ( Carrier l) by Y3, P1, FUNCT_1: 3;

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

        then t in IQ by AS, H1;

        then (b * t) in ( Lin IQ) by VECTSP_4: 21, VECTSP_7: 8;

        hence ex si be Vector of V st si = ((l (#) G) . i) & ( ZMtoMQV (V,p,si)) in ( Lin IQ) by Y7, Y5;

      end;

      hence ( ZMtoMQV (V,p,( Sum l))) in ( Lin IQ) by AS, P1, ZMODUL03: 33;

    end;

    theorem :: ZMODUL04:38

    

     ThQuotBasis5: for p be prime Element of INT.Ring , V be free Z_Module, I be Subset of V, IQ be Subset of ( Z_MQ_VectSp (V,p)) st ( Lin I) = the ModuleStr of V & IQ = { ( ZMtoMQV (V,p,u)) where u be Vector of V : u in I } holds ( Lin IQ) = the ModuleStr of ( Z_MQ_VectSp (V,p))

    proof

      let p be prime Element of INT.Ring , V be free Z_Module, I be Subset of V, IQ be Subset of ( Z_MQ_VectSp (V,p)) such that

       P0: ( Lin I) = the ModuleStr of V and

       AS: IQ = { ( ZMtoMQV (V,p,u)) where u be Vector of V : u in I };

      for vq be Element of ( Z_MQ_VectSp (V,p)) holds vq in ( Lin IQ)

      proof

        let vq be Element of ( Z_MQ_VectSp (V,p));

        consider v be Vector of V such that

         P3: vq = ( ZMtoMQV (V,p,v)) by ZMODUL03: 22;

        consider l be Linear_Combination of I such that

         P4: v = ( Sum l) by P0, STRUCT_0:def 5, ZMODUL02: 64;

        thus vq in ( Lin IQ) by AS, P4, P3, ThQuotBasis5A;

      end;

      hence thesis by VECTSP_4: 32;

    end;

    theorem :: ZMODUL04:39

    

     FG02: for V be finitely-generated free Z_Module holds ex A be finite Subset of V st A is Basis of V

    proof

      let V be finitely-generated free Z_Module;

      set p = the prime Element of INT.Ring ;

      set A = the Basis of V;

      set AQ = { ( ZMtoMQV (V,p,u)) where u be Vector of V : u in A };

      now

        let x be object;

        assume x in AQ;

        then

        consider v be Vector of V such that

         B1: x = ( ZMtoMQV (V,p,v)) & v in A;

        thus x in the carrier of ( Z_MQ_VectSp (V,p)) by B1;

      end;

      then

      reconsider AQ as Subset of ( Z_MQ_VectSp (V,p)) by TARSKI:def 3;

      reconsider AQ as Basis of ( Z_MQ_VectSp (V,p)) by ZMODUL03: 35;

      consider B be finite Subset of V such that

       P1: ( Lin B) = the ModuleStr of V by ZMODUL03:def 4;

      set BQ = { ( ZMtoMQV (V,p,u)) where u be Vector of V : u in B };

      now

        let x be object;

        assume x in BQ;

        then

        consider v be Vector of V such that

         B1: x = ( ZMtoMQV (V,p,v)) & v in B;

        thus x in the carrier of ( Z_MQ_VectSp (V,p)) by B1;

      end;

      then

      reconsider BQ as Subset of ( Z_MQ_VectSp (V,p)) by TARSKI:def 3;

      deffunc F( Element of V) = ( ZMtoMQV (V,p,$1));

      consider f be Function of the carrier of V, ( Z_MQ_VectSp (V,p)) such that

       P6: for x be Element of V holds (f . x) = F(x) from FUNCT_2:sch 4;

      B c= the carrier of V;

      then

       P8: B c= ( dom f) by FUNCT_2:def 1;

      for y be object st y in BQ holds ex x be object st x in ( dom (f | B)) & y = ((f | B) . x)

      proof

        let y be object such that

         Q1: y in BQ;

        consider x be Vector of V such that

         Q2: y = ( ZMtoMQV (V,p,x)) & x in B by Q1;

        

         Q3: x in ( dom (f | B)) by P8, Q2, RELAT_1: 62;

        

         Q4: y = (f . x) by P6, Q2

        .= ((f | B) . x) by Q3, FUNCT_1: 47;

        take x;

        thus thesis by P8, Q2, Q4, RELAT_1: 62;

      end;

      then

       P2: BQ c= ( rng (f | B)) by FUNCT_1: 9;

      ( Lin BQ) = the ModuleStr of ( Z_MQ_VectSp (V,p)) by P1, ThQuotBasis5;

      then

      consider IQ be Basis of ( Z_MQ_VectSp (V,p)) such that

       P4: IQ c= BQ by VECTSP_7: 20;

      

       P5: AQ is finite by P2, P4, MATRLIN:def 1, VECTSP_9: 20;

      ( card A) = ( card AQ) by ZMODUL03: 26;

      then A is finite by P5;

      hence thesis;

    end;

    registration

      cluster -> finite-rank for finitely-generated free Z_Module;

      coherence

      proof

        let V be finitely-generated free Z_Module;

        ex A be finite Subset of V st A is Basis of V by FG02;

        hence thesis by ZMODUL03:def 3;

      end;

    end

    registration

      cluster -> finitely-generated for finite-rank free Z_Module;

      coherence

      proof

        let V be finite-rank free Z_Module;

        consider A be finite Subset of V such that

         A1: A is Basis of V by ZMODUL03:def 3;

        take A;

        thus thesis by A1, VECTSP_7:def 3;

      end;

    end

    theorem :: ZMODUL04:40

    

     RL5Th25: for V be finite-rank free Z_Module holds for A be Subset of V st A is linearly-independent holds A is finite

    proof

      let V be finite-rank free Z_Module;

      let A be Subset of V;

      consider I be finite Subset of V such that

       A1: I is Basis of V by ZMODUL03:def 3;

      assume A is linearly-independent;

      then ( card A) c= ( card I) by A1, XXTh3, XBOOLE_0:def 8;

      hence thesis;

    end;

    

     RL5Th28: for V be finite-rank free Z_Module, W be Subspace of V holds W is finite-rank

    proof

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

      set A = the Basis of W;

      reconsider A0 = A as linearly-independent Subset of V by VECTSP_7:def 3, ZMODUL03: 15;

      A0 is finite by RL5Th25;

      hence thesis by ZMODUL03:def 3;

    end;

    registration

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

      cluster (W1 /\ W2) -> free;

      correctness

      proof

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

        hence thesis;

      end;

    end

    registration

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

      cluster (W1 /\ W2) -> finite-rank;

      correctness

      proof

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

        hence thesis by RL5Th28;

      end;

    end

    registration

      let V be finite-rank free Z_Module;

      cluster -> finite-rank for Subspace of V;

      correctness by RL5Th28;

    end