zmodlat2.miz



    begin

    

     LMBASE2A: for A,B be set, F,G be FinSequence st F is one-to-one & G is one-to-one & (A /\ B) = {} & ( rng F) = A & ( rng G) = B holds (F ^ G) is one-to-one & ( dom (F ^ G)) = ( Seg (( len F) + ( len G))) & ( rng (F ^ G)) = (( rng F) \/ ( rng G))

    proof

      let A,B be set, F,G be FinSequence such that

       A1: F is one-to-one and

       A2: G is one-to-one and

       A3: (A /\ B) = {} and

       A4: ( rng F) = A & ( rng G) = B;

      ( dom (F ^ G)) = ( Seg ( len (F ^ G))) by FINSEQ_1:def 3

      .= ( Seg (( len F) + ( len G))) by FINSEQ_1: 22;

      hence thesis by A1, A2, A3, A4, FINSEQ_1: 31, FINSEQ_3: 91, XBOOLE_0:def 7;

    end;

    

     LMBASE2C: for K be Ring, V be LeftMod of K, L be Linear_Combination of V, F be FinSequence of V st (( rng F) /\ ( Carrier L)) = {} holds (L (#) F) = (( dom F) --> ( 0. V))

    proof

      let K be Ring, V be LeftMod of K, L be Linear_Combination of V, F be FinSequence of V;

      assume

       AS: (( rng F) /\ ( Carrier L)) = {} ;

      

       P1: ( len (L (#) F)) = ( len F) by VECTSP_6:def 5;

      then

       p1: ( dom (L (#) F)) = ( dom F) by FINSEQ_3: 29;

      for z be object st z in ( dom (L (#) F)) holds ((L (#) F) . z) = ( 0. V)

      proof

        let z be object;

        assume

         X1: z in ( dom (L (#) F));

        then

        reconsider i = z as Nat;

        

         X3: i in ( dom F) by X1, P1, FINSEQ_3: 29;

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

        then

         X4: not (F . i) in ( Carrier L) by XBOOLE_0:def 4, AS;

        (F /. i) = (F . i) by X3, PARTFUN1:def 6;

        then (L . (F /. i)) = ( 0. K) by X4;

        

        hence ((L (#) F) . z) = (( 0. K) * (F /. i)) by X1, VECTSP_6:def 5

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

      end;

      hence thesis by FUNCOP_1: 11, p1;

    end;

    

     LMBASE2D: for K be Ring, V be LeftMod of K, F be FinSequence of V st F = (( dom F) --> ( 0. V)) holds ( Sum F) = ( 0. V)

    proof

      let K be Ring, V be LeftMod of K, F be FinSequence of V;

      assume

       AS: F = (( dom F) --> ( 0. V));

      

       X2: ( len F) = ( len F);

      for k be Nat holds for v be Element of V st k in ( dom F) & v = (F . k) holds (F . k) = (( 0. K) * v)

      proof

        let k be Nat;

        let v be Element of V;

        assume k in ( dom F) & v = (F . k);

        

        hence (F . k) = ( 0. V) by FUNCOP_1: 7, AS

        .= (( 0. K) * v) by VECTSP_1: 14;

      end;

      

      hence ( Sum F) = (( 0. K) * ( Sum F)) by X2, RLVECT_2: 66

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

    end;

    theorem :: ZMODLAT2:1

    

     EQSUMLF: for K be Ring, V be LeftMod of K, L be Function of the carrier of V, the carrier of K, A be Subset of V, F,F1 be FinSequence of the carrier of V st F is one-to-one & ( rng F) = A & F1 is one-to-one & ( rng F1) = A holds ( Sum (L (#) F)) = ( Sum (L (#) F1))

    proof

      let K be Ring, V be LeftMod of K, L be Function of the carrier of V, the carrier of K, A be Subset of V, F,F1 be FinSequence of the carrier of V;

      assume that

       A4: F is one-to-one and

       A5: ( rng F) = A and

       A7: F1 is one-to-one and

       A8: ( rng F1) = A;

      set v1 = ( Sum (L (#) F));

      set v2 = ( Sum (L (#) F1));

      defpred S1[ object, object] means {$2} = (F " {(F1 . $1)});

      

       A10: ( len F) = ( len F1) by A4, A5, A7, A8, FINSEQ_1: 48;

      

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

      

       A12: ( dom F1) = ( Seg ( len F1)) by FINSEQ_1:def 3;

      

       A13: for x be object st x in ( dom F) holds ex y be object st y in ( dom F) & S1[x, y]

      proof

        let x be object;

        assume x in ( dom F);

        then (F1 . x) in ( rng F) by A5, A8, A10, A11, A12, FUNCT_1:def 3;

        then

        consider y be object such that

         A14: (F " {(F1 . x)}) = {y} by A4, FUNCT_1: 74;

        take y;

        y in (F " {(F1 . x)}) by A14, TARSKI:def 1;

        hence y in ( dom F) by FUNCT_1:def 7;

        thus S1[x, y] by A14;

      end;

      consider f be Function of ( dom F), ( dom F) such that

       A15: for x be object st x in ( dom F) holds S1[x, (f . x)] from FUNCT_2:sch 1( A13);

      

       A16: ( rng f) = ( dom F)

      proof

        thus ( rng f) c= ( dom F);

        let y be object;

        assume

         A17: y in ( dom F);

        then (F . y) in ( rng F1) by A5, A8, FUNCT_1:def 3;

        then

        consider x be object such that

         A18: x in ( dom F1) and

         A19: (F1 . x) = (F . y) by FUNCT_1:def 3;

        (F " {(F1 . x)}) = (F " ( Im (F,y))) by A17, A19, FUNCT_1: 59;

        then (F " {(F1 . x)}) c= {y} by A4, FUNCT_1: 82;

        then {(f . x)} c= {y} by A10, A11, A12, A15, A18;

        then

         A20: (f . x) = y by ZFMISC_1: 18;

        x in ( dom f) by A10, A11, A12, A18, FUNCT_2:def 1;

        hence y in ( rng f) by A20, FUNCT_1:def 3;

      end;

      reconsider G1 = (L (#) F) as FinSequence of V;

      

       A21: ( len G1) = ( len F) by VECTSP_6:def 5;

      

       A22: f is one-to-one

      proof

        let y1,y2 be object;

        assume that

         A23: y1 in ( dom f) and

         A24: y2 in ( dom f) and

         A25: (f . y1) = (f . y2);

        

         A28: (F " {(F1 . y2)}) = {(f . y2)} by A15, A24;

        (F1 . y1) in ( rng F) by A5, A8, A10, A11, A12, A23, FUNCT_1:def 3;

        then

         A30: {(F1 . y1)} c= ( rng F) by ZFMISC_1: 31;

        (F1 . y2) in ( rng F) by A5, A8, A10, A11, A12, A24, FUNCT_1:def 3;

        then

         A31: {(F1 . y2)} c= ( rng F) by ZFMISC_1: 31;

        (F " {(F1 . y1)}) = {(f . y1)} by A15, A23;

        then {(F1 . y1)} = {(F1 . y2)} by A25, A28, A30, A31, FUNCT_1: 91;

        hence y1 = y2 by A7, A10, A11, A12, A23, A24, ZFMISC_1: 3;

      end;

      set G2 = (L (#) F1);

      

       A33: ( dom (L (#) F1)) = ( Seg ( len (L (#) F1))) by FINSEQ_1:def 3;

      reconsider f as Permutation of ( dom F) by A16, A22, FUNCT_2: 57;

      (( dom F) = ( Seg ( len F)) & ( dom G1) = ( Seg ( len G1))) by FINSEQ_1:def 3;

      then

      reconsider f as Permutation of ( dom G1) by A21;

      

       A34: ( len (L (#) F1)) = ( len F1) by VECTSP_6:def 5;

      

       A35: ( dom G1) = ( Seg ( len G1)) by FINSEQ_1:def 3;

      now

        let i be Nat;

        assume

         A36: i in ( dom (L (#) F1));

        then

         A37: (((L (#) F1) . i) = ((L . (F1 /. i)) * (F1 /. i)) & (F1 . i) = (F1 /. i)) by A34, A12, A33, VECTSP_6:def 5, PARTFUN1:def 6;

        i in ( dom F1) by A34, A36, FINSEQ_3: 29;

        then

        reconsider u = (F1 . i) as Element of V by FINSEQ_2: 11;

        i in ( dom f) by A10, A21, A34, A35, A33, A36, FUNCT_2:def 1;

        then

         A38: (f . i) in ( dom F) by A16, FUNCT_1:def 3;

        then

        reconsider m = (f . i) as Element of NAT ;

        reconsider v = (F . m) as Element of V by A38, FINSEQ_2: 11;

         {(F . (f . i))} = ( Im (F,(f . i))) by A38, FUNCT_1: 59

        .= (F .: (F " {(F1 . i)})) by A10, A34, A11, A33, A15, A36;

        then

         A39: u = v by FUNCT_1: 75, ZFMISC_1: 18;

        (F . m) = (F /. m) by A38, PARTFUN1:def 6;

        hence ((L (#) F1) . i) = (G1 . (f . i)) by A21, A11, A35, A38, A39, A37, VECTSP_6:def 5;

      end;

      hence v1 = v2 by A4, A5, A7, A8, A21, A34, FINSEQ_1: 48, RLVECT_2: 6;

    end;

    theorem :: ZMODLAT2:2

    

     LMBASE2X: for K be Ring, V be LeftMod of K, A be finite Subset of V holds A is linearly-independent iff (for L be Linear_Combination of A st (ex F be FinSequence of the carrier of V st F is one-to-one & ( rng F) = A & ( Sum (L (#) F)) = ( 0. V)) holds ( Carrier L) = {} )

    proof

      let K be Ring, V be LeftMod of K, A be finite Subset of V;

      hereby

        assume

         BS: A is linearly-independent;

        let L be Linear_Combination of A;

        given F be FinSequence of the carrier of V such that

         BS2: F is one-to-one & ( rng F) = A & ( Sum (L (#) F)) = ( 0. V);

        reconsider B = ( Carrier L) as finite Subset of V;

        set F0 = ( canFS B);

        

         BS3: ( rng F0) = B by FUNCT_2:def 3;

        ( rng F0) c= the carrier of V by TARSKI:def 3;

        then

        reconsider F0 as FinSequence of the carrier of V by FINSEQ_1:def 4;

        reconsider C = (A \ B) as finite Subset of V;

        set G0 = ( canFS C);

        

         BS4: ( rng G0) = C by FUNCT_2:def 3;

        ( rng G0) c= the carrier of V by TARSKI:def 3;

        then

        reconsider G0 as FinSequence of the carrier of V by FINSEQ_1:def 4;

        

         BS5: (( rng F0) /\ ( rng G0)) = (B /\ (A \ B)) by BS3, FUNCT_2:def 3

        .= ((B /\ A) \ B) by XBOOLE_1: 49

        .= {} by XBOOLE_1: 37, XBOOLE_1: 17;

        then

         BS6: (F0 ^ G0) is one-to-one by LMBASE2A;

        

         BS7: ( rng (F0 ^ G0)) = (B \/ (A \ B)) by BS3, BS4, BS5, LMBASE2A

        .= (A \/ B) by XBOOLE_1: 39

        .= A by VECTSP_6:def 4, XBOOLE_1: 12;

        (( rng G0) /\ ( Carrier L)) = {} by BS5, FUNCT_2:def 3;

        then

         BS10: (L (#) G0) = (( dom G0) --> ( 0. V)) by LMBASE2C;

        then

         aa: ( dom (L (#) G0)) = ( dom G0) by FUNCOP_1: 13;

        

         BS12: ( Sum (L (#) F)) = ( Sum (L (#) (F0 ^ G0))) by EQSUMLF, BS6, BS7, BS2

        .= ( Sum ((L (#) F0) ^ (L (#) G0))) by VECTSP_6: 13

        .= (( Sum (L (#) F0)) + ( Sum (L (#) G0))) by RLVECT_1: 41

        .= (( Sum (L (#) F0)) + ( 0. V)) by BS10, LMBASE2D, aa

        .= ( Sum (L (#) F0));

        ( Sum L) = ( 0. V) by BS2, BS3, BS12, VECTSP_6:def 6;

        hence ( Carrier L) = {} by VECTSP_7:def 1, BS;

      end;

      assume

       AS: for L be Linear_Combination of A st (ex F be FinSequence of the carrier of V st F is one-to-one & ( rng F) = A & ( Sum (L (#) F)) = ( 0. V)) holds ( Carrier L) = {} ;

      for L be Linear_Combination of A st ( Sum L) = ( 0. V) holds ( Carrier L) = {}

      proof

        let L be Linear_Combination of A;

        assume

         BS: ( Sum L) = ( 0. V);

        consider F0 be FinSequence of the carrier of V such that

         P3: F0 is one-to-one & ( rng F0) = ( Carrier L) & ( Sum L) = ( Sum (L (#) F0)) by VECTSP_6:def 6;

        reconsider B = ( Carrier L) as finite Subset of V;

        reconsider C = (A \ B) as finite Subset of V;

        set G0 = ( canFS C);

        

         BS4: ( rng G0) = C by FUNCT_2:def 3;

        ( rng G0) c= the carrier of V by TARSKI:def 3;

        then

        reconsider G0 as FinSequence of the carrier of V by FINSEQ_1:def 4;

        set F = (F0 ^ G0);

        

         BS5: (( rng F0) /\ ( rng G0)) = (B /\ (A \ B)) by P3, FUNCT_2:def 3

        .= ((B /\ A) \ B) by XBOOLE_1: 49

        .= {} by XBOOLE_1: 37, XBOOLE_1: 17;

        then

         BS6: F is one-to-one by LMBASE2A, P3;

        

         BS7: ( rng F) = (B \/ (A \ B)) by P3, BS4, BS5, LMBASE2A

        .= (A \/ B) by XBOOLE_1: 39

        .= A by VECTSP_6:def 4, XBOOLE_1: 12;

        

         BS10: (L (#) G0) = (( dom G0) --> ( 0. V)) by BS5, P3, LMBASE2C;

        then

         aa: ( dom (L (#) G0)) = ( dom G0) by FUNCOP_1: 13;

        ( Sum (L (#) F)) = ( Sum ((L (#) F0) ^ (L (#) G0))) by VECTSP_6: 13

        .= (( Sum (L (#) F0)) + ( Sum (L (#) G0))) by RLVECT_1: 41

        .= (( Sum (L (#) F0)) + ( 0. V)) by BS10, LMBASE2D, aa

        .= ( Sum (L (#) F0));

        hence ( Carrier L) = {} by AS, BS, BS6, BS7, P3;

      end;

      hence thesis by VECTSP_7:def 1;

    end;

    theorem :: ZMODLAT2:3

    

     LMBASE2: for K be Ring, V be LeftMod of K, b be FinSequence of V st b is one-to-one holds (( rng b) is linearly-independent iff for r be FinSequence of K, rb be FinSequence of V st ( len r) = ( len b) & ( len rb) = ( len b) & (for i be Nat st i in ( dom rb) holds (rb . i) = ((r /. i) * (b /. i))) & ( Sum rb) = ( 0. V) holds r = (( Seg ( len r)) --> ( 0. K)))

    proof

      let K be Ring, V be LeftMod of K, b be FinSequence of V;

      assume

       AS: b is one-to-one;

      hereby

        assume

         AS1: ( rng b) is linearly-independent;

        let r be FinSequence of K, rb be FinSequence of V;

        assume that

         A1: ( len r) = ( len b) & ( len rb) = ( len b) and

         A2: for i be Nat st i in ( dom rb) holds (rb . i) = ((r /. i) * (b /. i)) and

         A3: ( Sum rb) = ( 0. V);

        

         DRB: ( dom r) = ( dom b) by A1, FINSEQ_3: 29;

        defpred P[ object, object] means ($1 in ( rng b) & $2 = ((r * (b " )) . $1)) or ( not $1 in ( rng b) & $2 = ( 0. K));

        

         XA2: 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 x as Vector of V;

          per cases ;

            suppose

             XA3: x in ( rng b);

            then

             XA31: x in ( dom (b " )) by FUNCT_1: 33, AS;

            ((b " ) . x) in ( rng (b " )) by FUNCT_1: 3, XA31;

            then ((b " ) . x) in ( dom r) by AS, DRB, FUNCT_1: 33;

            then (r . ((b " ) . x)) in ( rng r) by FUNCT_1: 3;

            then

            reconsider y = ((r * (b " )) . x) as Element of K by XA31, FUNCT_1: 13;

             P[x, y] by XA3;

            hence thesis;

          end;

            suppose not x in ( rng b);

            hence thesis;

          end;

        end;

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

         XA5: for x be object st x in the carrier of V holds P[x, (L . x)] from FUNCT_2:sch 1( XA2);

        

         XA6: for v be Vector of V st not v in ( rng b) holds (L . v) = ( 0. K) by XA5;

        L is Element of ( Funcs (the carrier of V,the carrier of K)) by FUNCT_2: 8;

        then

        reconsider L as Linear_Combination of V by XA6, VECTSP_6:def 1;

        now

          let x be object;

          assume that

           XA7: x in ( Carrier L) and

           XA8: not x in ( rng b);

          consider v be Vector of V such that

           XA9: x = v and

           XA10: (L . v) <> ( 0. K) by XA7;

          thus contradiction by XA5, XA8, XA9, XA10;

        end;

        then ( Carrier L) c= ( rng b);

        then

        reconsider L as Linear_Combination of ( rng b) by VECTSP_6:def 4;

        

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

        ( rng (b " )) = ( dom r) by AS, DRB, FUNCT_1: 33;

        

        then

         XA43: ( dom (r * (b " ))) = ( dom (b " )) by RELAT_1: 27

        .= ( rng b) by FUNCT_1: 33, AS;

        for i be object st i in ( dom (L | ( rng b))) holds ((L | ( rng b)) . i) = ((r * (b " )) . i)

        proof

          let i be object;

          assume

           ASXA: i in ( dom (L | ( rng b)));

          then

           XA45: i in ( rng b);

          ((L | ( rng b)) . i) = (L . i) by ASXA, FUNCT_1: 49;

          hence thesis by XA5, XA45;

        end;

        then

         A4: (L | ( rng b)) = (r * (b " )) by XA41, XA43, RELAT_1: 62;

        

         ZA2: ( dom rb) = ( Seg ( len b)) by A1, FINSEQ_1:def 3;

        

         ZA3: ( dom (L (#) b)) = ( Seg ( len (L (#) b))) by FINSEQ_1:def 3

        .= ( Seg ( len b)) by VECTSP_6:def 5;

        for i be Nat st i in ( dom (L (#) b)) holds ((L (#) b) . i) = (rb . i)

        proof

          let i be Nat;

          assume

           ZA40: i in ( dom (L (#) b));

          then

           ZA41: ((L (#) b) . i) = ((L . (b /. i)) * (b /. i)) by VECTSP_6:def 5;

          

           ZA42: i in ( dom b) by FINSEQ_1:def 3, ZA40, ZA3;

          then

           ZA45: (b . i) in ( rng b) by FUNCT_1: 3;

          then

           ZA49: (b . i) in ( dom (b " )) by AS, FUNCT_1: 33;

          (L . (b . i)) = ((r * (b " )) . (b . i)) by XA5, ZA45

          .= (r . ((b " ) . (b . i))) by ZA49, FUNCT_1: 13

          .= (r . i) by AS, FUNCT_1: 34, ZA42

          .= (r /. i) by PARTFUN1:def 6, ZA42, DRB;

          then (L . (b /. i)) = (r /. i) by ZA42, PARTFUN1:def 6;

          hence thesis by A2, ZA2, ZA3, ZA40, ZA41;

        end;

        then

         ZA1: rb = (L (#) b) by ZA2, ZA3;

        reconsider B = ( Carrier L) as finite Subset of V;

        set F0 = ( canFS B);

        

         BS3: ( rng F0) = B by FUNCT_2:def 3;

        ( rng F0) c= the carrier of V by TARSKI:def 3;

        then

        reconsider F0 as FinSequence of V by FINSEQ_1:def 4;

        reconsider C = (( rng b) \ B) as finite Subset of V;

        set G0 = ( canFS C);

        

         BS4: ( rng G0) = C by FUNCT_2:def 3;

        ( rng G0) c= the carrier of V by TARSKI:def 3;

        then

        reconsider G0 as FinSequence of V by FINSEQ_1:def 4;

        

         BS5: (( rng F0) /\ ( rng G0)) = (B /\ (( rng b) \ B)) by BS3, FUNCT_2:def 3

        .= ((B /\ ( rng b)) \ B) by XBOOLE_1: 49

        .= {} by XBOOLE_1: 37, XBOOLE_1: 17;

        then

         BS6: (F0 ^ G0) is one-to-one by LMBASE2A;

        

         BS7: ( rng (F0 ^ G0)) = (B \/ (( rng b) \ B)) by BS3, BS4, BS5, LMBASE2A

        .= (( rng b) \/ B) by XBOOLE_1: 39

        .= ( rng b) by VECTSP_6:def 4, XBOOLE_1: 12;

        

         BS10: (L (#) G0) = (( dom G0) --> ( 0. V)) by BS3, BS5, LMBASE2C;

        then

         aa: ( dom (L (#) G0)) = ( dom G0) by FUNCOP_1: 13;

        

         A51: ( Sum (L (#) b)) = ( Sum (L (#) (F0 ^ G0))) by EQSUMLF, BS6, BS7, AS

        .= ( Sum ((L (#) F0) ^ (L (#) G0))) by VECTSP_6: 13

        .= (( Sum (L (#) F0)) + ( Sum (L (#) G0))) by RLVECT_1: 41

        .= (( Sum (L (#) F0)) + ( 0. V)) by BS10, LMBASE2D, aa

        .= ( Sum L) by BS3, VECTSP_6:def 6;

        

         A6: ( Carrier L) = {} by AS1, A3, A51, ZA1, VECTSP_7:def 1;

        set N = { i where i be Nat : i in ( dom r) & (r . i) <> ( 0. K) };

        for z be object st z in (b .: N) holds z in ( Carrier L)

        proof

          let z be object;

          assume z in (b .: N);

          then

          consider x be object such that

           D70: x in ( dom b) & x in N & z = (b . x) by FUNCT_1:def 6;

          reconsider x as Nat by D70;

          consider i be Nat such that

           A80: x = i & i in ( dom r) & (r . i) <> ( 0. K) by D70;

          

           A81: (b . i) in ( rng b) by A80, DRB, FUNCT_1: 3;

          then

           A86: (b . i) in ( dom (b " )) by AS, FUNCT_1: 33;

          

           A83: (L . (b . i)) = ((L | ( rng b)) . (b . i)) by A80, DRB, FUNCT_1: 3, FUNCT_1: 49

          .= (r . ((b " ) . (b . i))) by A4, A86, FUNCT_1: 13

          .= (r . i) by AS, A80, DRB, FUNCT_1: 34;

          reconsider bi = (b . i) as Element of V by A81;

          (L . bi) <> ( 0. K) by A83, A80;

          hence z in ( Carrier L) by D70, A80;

        end;

        then

         A8: (b .: N) c= ( Carrier L);

        for z be object st z in N holds z in ( dom b)

        proof

          let z be object;

          assume z in N;

          then

          consider i be Nat such that

           A80: z = i & i in ( dom r) & (r . i) <> ( 0. K);

          thus thesis by A80, A1, FINSEQ_3: 29;

        end;

        then

         A9: N c= ( dom b);

        

         A7: N = {}

        proof

          per cases ;

            suppose ( rng b) = {} ;

            then ( dom b) = {} by RELAT_1: 42;

            then

             Y2: ( Seg ( len r)) = {} by A1, FINSEQ_1:def 3;

            thus N = {}

            proof

              assume N <> {} ;

              then

              consider z be object such that

               Y3: z in N by XBOOLE_0:def 1;

              ex i be Nat st z = i & i in ( dom r) & (r . i) <> ( 0. K) by Y3;

              hence contradiction by Y2, FINSEQ_1:def 3;

            end;

          end;

            suppose

             Y1: ( rng b) <> {} ;

            b is Function of ( dom b), ( rng b) by FUNCT_2: 1;

            then N c= {} by A6, A8, A9, Y1;

            hence N = {} ;

          end;

        end;

        for z be object st z in ( dom r) holds (r . z) = ( 0. K)

        proof

          let z be object;

          assume

           X1: z in ( dom r);

          assume

           X2: (r . z) <> ( 0. K);

          reconsider i = z as Nat by X1;

          i in N by X1, X2;

          hence contradiction by A7;

        end;

        then r = (( dom r) --> ( 0. K)) by FUNCOP_1: 11;

        hence r = (( Seg ( len r)) --> ( 0. K)) by FINSEQ_1:def 3;

      end;

      assume

       AS2: for r be FinSequence of K, rb be FinSequence of V st ( len r) = ( len b) & ( len rb) = ( len b) & (for i be Nat st i in ( dom rb) holds (rb . i) = ((r /. i) * (b /. i))) & ( Sum rb) = ( 0. V) holds r = (( Seg ( len r)) --> ( 0. K));

      for L be Linear_Combination of ( rng b) st (ex F be FinSequence of the carrier of V st F is one-to-one & ( rng F) = ( rng b) & ( Sum (L (#) F)) = ( 0. V)) holds ( Carrier L) = {}

      proof

        let L be Linear_Combination of ( rng b);

        given F be FinSequence of the carrier of V such that

         A4: F is one-to-one and

         A5: ( rng F) = ( rng b) and

         A6: ( Sum (L (#) F)) = ( 0. V);

        reconsider rb = (L (#) b) as FinSequence of V;

        ( rng (L * b)) c= the carrier of K;

        then

        reconsider r = (L * b) as FinSequence of K by FINSEQ_1:def 4;

        

         B24: ( len rb) = ( len b) by VECTSP_6:def 5;

        ( rng b) c= the carrier of V & ( dom L) = the carrier of V by FUNCT_2:def 1;

        then

         X2: ( dom r) = ( dom b) by RELAT_1: 27;

        then

         B21: ( len r) = ( len b) by FINSEQ_3: 29;

        

         B23: for i be Nat st i in ( dom rb) holds (rb . i) = ((r /. i) * (b /. i))

        proof

          let i be Nat;

          assume

           B231: i in ( dom rb);

          then

           B233: i in ( dom b) by B24, FINSEQ_3: 29;

          i in ( dom r) by B231, B24, X2, FINSEQ_3: 29;

          

          then (r /. i) = (r . i) by PARTFUN1:def 6

          .= (L . (b . i)) by B233, FUNCT_1: 13

          .= (L . (b /. i)) by B233, PARTFUN1:def 6;

          hence thesis by B231, VECTSP_6:def 5;

        end;

        ( Sum rb) = ( Sum (L (#) F)) by AS, A4, A5, EQSUMLF;

        then

         A5: r = (( Seg ( len r)) --> ( 0. K)) by A6, AS2, B21, B23, B24;

        

         A6: ( Carrier L) c= ( rng b) by VECTSP_6:def 4;

        assume ( Carrier L) <> {} ;

        then

        consider x be object such that

         A7: x in ( Carrier L) by XBOOLE_0:def 1;

        consider v be Element of V such that

         A8: x = v & (L . v) <> ( 0. K) by A7;

        consider i be object such that

         A9: i in ( dom b) & v = (b . i) by A6, A7, A8, FUNCT_1:def 3;

        

         A10: (r . i) <> ( 0. K) by A8, A9, FUNCT_1: 13;

        i in ( Seg ( len r)) by A9, X2, FINSEQ_1:def 3;

        hence contradiction by A5, A10, FUNCOP_1: 7;

      end;

      hence ( rng b) is linearly-independent by LMBASE2X;

    end;

    theorem :: ZMODLAT2:4

    for K be Ring, V be LeftMod of K, A be finite Subset of V holds A is linearly-independent iff ex b be FinSequence of V st b is one-to-one & ( rng b) = A & for r be FinSequence of K, rb be FinSequence of V st ( len r) = ( len b) & ( len rb) = ( len b) & (for i be Nat st i in ( dom rb) holds (rb . i) = ((r /. i) * (b /. i))) & ( Sum rb) = ( 0. V) holds r = (( Seg ( len r)) --> ( 0. K))

    proof

      let K be Ring, V be LeftMod of K, A be finite Subset of V;

      hereby

        assume

         AS: A is linearly-independent;

        ( rng ( canFS A)) = A by FUNCT_2:def 3;

        then

        reconsider b = ( canFS A) as FinSequence of the carrier of V by FINSEQ_1:def 4;

        take b;

        thus b is one-to-one;

        thus ( rng b) = A by FUNCT_2:def 3;

        hence for r be FinSequence of K, rb be FinSequence of V st ( len r) = ( len b) & ( len rb) = ( len b) & (for i be Nat st i in ( dom rb) holds (rb . i) = ((r /. i) * (b /. i))) & ( Sum rb) = ( 0. V) holds r = (( Seg ( len r)) --> ( 0. K)) by LMBASE2, AS;

      end;

      given b be FinSequence of V such that

       A1: b is one-to-one & ( rng b) = A & for r be FinSequence of K, rb be FinSequence of V st ( len r) = ( len b) & ( len rb) = ( len b) & (for i be Nat st i in ( dom rb) holds (rb . i) = ((r /. i) * (b /. i))) & ( Sum rb) = ( 0. V) holds r = (( Seg ( len r)) --> ( 0. K));

      thus thesis by A1, LMBASE2;

    end;

    registration

      let V be non trivial free Z_Module;

      cluster -> non empty for Basis of V;

      correctness

      proof

        let I be Basis of V;

        assume I is empty;

        then I = ( {} the carrier of V);

        then ( Lin I) = ( (0). V) by ZMODUL02: 67;

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

        hence contradiction;

      end;

    end

    definition

      let IT be Z_Lattice;

      :: ZMODLAT2:def1

      attr IT is RATional means

      : defRational: for v,u be Vector of IT holds <;v, u;> in RAT ;

    end

    registration

      cluster non trivial RATional positive-definite for Z_Lattice;

      correctness

      proof

        set L = the non trivial INTegral positive-definite Z_Lattice;

        take L;

        thus thesis by RAT_1:def 2;

      end;

    end

    registration

      let L be RATional Z_Lattice;

      let v,u be Vector of L;

      cluster <;v, u;> -> rational;

      correctness by defRational, RAT_1:def 2;

    end

    registration

      cluster -> RATional for INTegral Z_Lattice;

      correctness by RAT_1:def 2;

    end

    

     LMINTFREAL1: for x be Element of INT , y be Element of F_Real st x <> 0 & x = y holds (x " ) = (y " )

    proof

      let x be Element of INT , y be Element of F_Real ;

      assume

       B1: x <> 0 & x = y;

      reconsider xi = (x " ) as Element of F_Real by XREAL_0:def 1;

      

       X2: (xi * y) = ( 1. F_Real ) by B1, XCMPLX_0:def 7;

      y <> ( 0. F_Real ) by B1;

      hence (x " ) = (y " ) by X2, VECTSP_1:def 10;

    end;

    definition

      let L be Z_Lattice;

      :: ZMODLAT2:def2

      func ScProductEM (L) -> Function of [:the carrier of ( EMbedding L), the carrier of ( EMbedding L):], the carrier of F_Real means

      : defScProductEM: for v,u be Vector of L, vv,uu be Vector of ( EMbedding L) st vv = (( MorphsZQ L) . v) & uu = (( MorphsZQ L) . u) holds (it . (vv,uu)) = <;v, u;>;

      existence

      proof

        set Z = ( EMbedding L);

        defpred P[ object, object] means ex vv,uu be Vector of Z, v,u be Vector of L st $1 = [vv, uu] & vv = (( MorphsZQ L) . v) & uu = (( MorphsZQ L) . u) & $2 = <;v, u;>;

        

         A1: for x be Element of [:the carrier of Z, the carrier of Z:] holds ex y be Element of the carrier of F_Real st P[x, y]

        proof

          let x be Element of [:the carrier of Z, the carrier of Z:];

          consider vv,uu be object such that

           B1: vv in the carrier of Z & uu in the carrier of Z & x = [vv, uu] by ZFMISC_1:def 2;

          reconsider vv, uu as Vector of Z by B1;

          consider v be Vector of L such that

           B2: vv = (( MorphsZQ L) . v) by ZMODUL08: 22;

          consider u be Vector of L such that

           B3: uu = (( MorphsZQ L) . u) by ZMODUL08: 22;

          take <;v, u;>;

          thus thesis by B1, B2, B3;

        end;

        consider f be Function of [:the carrier of Z, the carrier of Z:], the carrier of F_Real such that

         A2: for x be Element of [:the carrier of Z, the carrier of Z:] holds P[x, (f . x)] from FUNCT_2:sch 3( A1);

        take f;

        for v,u be Vector of L, vv,uu be Vector of Z st vv = (( MorphsZQ L) . v) & uu = (( MorphsZQ L) . u) holds (f . (vv,uu)) = <;v, u;>

        proof

          let v,u be Vector of L, vv,uu be Vector of Z such that

           B1: vv = (( MorphsZQ L) . v) & uu = (( MorphsZQ L) . u);

          consider vv1,uu1 be Vector of Z, v1,u1 be Vector of L such that

           B2: [vv1, uu1] = [vv, uu] & vv1 = (( MorphsZQ L) . v1) & uu1 = (( MorphsZQ L) . u1) & (f . (vv,uu)) = <;v1, u1;> by A2;

          

           B3: ( MorphsZQ L) is one-to-one by ZMODUL04:def 6;

          vv = (( MorphsZQ L) . v1) by B2, XTUPLE_0: 1;

          then

           B4: v1 = v by B1, B3, FUNCT_2: 19;

          uu = (( MorphsZQ L) . u1) by B2, XTUPLE_0: 1;

          hence thesis by B1, B2, B3, B4, FUNCT_2: 19;

        end;

        hence thesis;

      end;

      uniqueness

      proof

        let f1,f2 be Function of [:the carrier of ( EMbedding L), the carrier of ( EMbedding L):], the carrier of F_Real ;

        assume

         AS1: for v,u be Vector of L, vv,uu be Vector of ( EMbedding L) st vv = (( MorphsZQ L) . v) & uu = (( MorphsZQ L) . u) holds (f1 . (vv,uu)) = <;v, u;>;

        assume

         AS2: for v,u be Vector of L, vv,uu be Vector of ( EMbedding L) st vv = (( MorphsZQ L) . v) & uu = (( MorphsZQ L) . u) holds (f2 . (vv,uu)) = <;v, u;>;

        for x be Element of [:the carrier of ( EMbedding L), the carrier of ( EMbedding L):] holds (f1 . x) = (f2 . x)

        proof

          let x be Element of [:the carrier of ( EMbedding L), the carrier of ( EMbedding L):];

          consider vv,uu be object such that

           B0: vv in the carrier of ( EMbedding L) & uu in the carrier of ( EMbedding L) & x = [vv, uu] by ZFMISC_1:def 2;

          reconsider vv, uu as Vector of ( EMbedding L) by B0;

          consider v be Vector of L such that

           B2: (( MorphsZQ L) . v) = vv by ZMODUL08: 22;

          consider u be Vector of L such that

           B3: (( MorphsZQ L) . u) = uu by ZMODUL08: 22;

          

          thus (f1 . x) = (f1 . (vv,uu)) by B0

          .= <;v, u;> by AS1, B2, B3

          .= (f2 . (vv,uu)) by AS2, B2, B3

          .= (f2 . x) by B0;

        end;

        hence f1 = f2;

      end;

    end

    theorem :: ZMODLAT2:5

    

     ThSPEM1: for L be Z_Lattice holds (for x be Vector of ( EMbedding L) st for y be Vector of ( EMbedding L) holds (( ScProductEM L) . (x,y)) = 0 holds x = ( 0. ( EMbedding L))) & (for x,y be Vector of ( EMbedding L) holds (( ScProductEM L) . (x,y)) = (( ScProductEM L) . (y,x))) & (for x,y,z be Vector of ( EMbedding L), a be Element of INT.Ring holds (( ScProductEM L) . ((x + y),z)) = ((( ScProductEM L) . (x,z)) + (( ScProductEM L) . (y,z))) & (( ScProductEM L) . ((a * x),y)) = (a * (( ScProductEM L) . (x,y))))

    proof

      let L be Z_Lattice;

      set Z = ( EMbedding L);

      set f = ( ScProductEM L);

      set T = ( MorphsZQ L);

      thus for x be Vector of Z st for y be Vector of Z holds (f . (x,y)) = 0 holds x = ( 0. ( EMbedding L))

      proof

        let x be Vector of Z such that

         B1: for y be Vector of Z holds (f . (x,y)) = 0 ;

        consider xx be Vector of L such that

         B2: (T . xx) = x by ZMODUL08: 22;

        for yy be Vector of L holds <;xx, yy;> = 0

        proof

          let yy be Vector of L;

          (T . yy) in ( rng T) by FUNCT_2: 4;

          then

          reconsider y = (T . yy) as Vector of Z by ZMODUL08:def 3;

          (f . (x,y)) = 0 by B1;

          hence thesis by B2, defScProductEM;

        end;

        

        hence x = (T . ( 0. L)) by B2, ZMODLAT1:def 3

        .= ( Class (( EQRZM L), [( 0. L), 1])) by ZMODUL04:def 6

        .= ( zeroCoset L) by ZMODUL04:def 3

        .= ( 0. ( EMbedding L)) by ZMODUL08:def 3;

      end;

      thus for x,y be Vector of Z holds (f . (x,y)) = (f . (y,x))

      proof

        let x,y be Vector of Z;

        consider xx be Vector of L such that

         B1: (T . xx) = x by ZMODUL08: 22;

        consider yy be Vector of L such that

         B2: (T . yy) = y by ZMODUL08: 22;

        

        thus (f . (x,y)) = <;xx, yy;> by B1, B2, defScProductEM

        .= <;yy, xx;> by ZMODLAT1:def 3

        .= (f . (y,x)) by B1, B2, defScProductEM;

      end;

      thus for x,y,z be Vector of Z, a be Element of INT.Ring holds (f . ((x + y),z)) = ((f . (x,z)) + (f . (y,z))) & (f . ((a * x),y)) = (a * (f . (x,y)))

      proof

        let x,y,z be Vector of Z, a be Element of INT.Ring ;

        consider xx be Vector of L such that

         B1: (T . xx) = x by ZMODUL08: 22;

        consider yy be Vector of L such that

         B2: (T . yy) = y by ZMODUL08: 22;

        consider zz be Vector of L such that

         B3: (T . zz) = z by ZMODUL08: 22;

        

         B4: (T . (xx + yy)) = ((T . xx) + (T . yy)) by ZMODUL04:def 6

        .= (x + y) by B1, B2, ZMODUL08: 19;

        reconsider aq = a as Element of F_Rat by NUMBERS: 14;

        

         B5: (T . (a * xx)) = (aq * (T . xx)) by ZMODUL04:def 6

        .= (a * x) by B1, ZMODUL08: 19;

        

        thus (f . ((x + y),z)) = <;(xx + yy), zz;> by B3, B4, defScProductEM

        .= ( <;xx, zz;> + <;yy, zz;>) by ZMODLAT1:def 3

        .= ((f . (x,z)) + <;yy, zz;>) by B1, B3, defScProductEM

        .= ((f . (x,z)) + (f . (y,z))) by B2, B3, defScProductEM;

        

        thus (f . ((a * x),y)) = <;(a * xx), yy;> by B2, B5, defScProductEM

        .= (a * <;xx, yy;>) by ZMODLAT1:def 3

        .= (a * (f . (x,y))) by B1, B2, defScProductEM;

      end;

    end;

    definition

      let L be Z_Lattice;

      :: ZMODLAT2:def3

      func ScProductDM (L) -> Function of [:the carrier of ( DivisibleMod L), the carrier of ( DivisibleMod L):], the carrier of F_Real means

      : defScProductDM: for vv,uu be Vector of ( DivisibleMod L), v,u be Vector of ( EMbedding L), a,b be Element of INT.Ring , ai,bi be Element of F_Real st a = ai & b = bi & ai <> 0 & bi <> 0 & v = (a * vv) & u = (b * uu) holds (it . (vv,uu)) = (((ai " ) * (bi " )) * (( ScProductEM L) . (v,u)));

      existence

      proof

        set Z = ( EMbedding L);

        set D = ( DivisibleMod L);

        defpred P[ object, object] means ex vv,uu be Vector of D, v,u be Vector of Z, a,b be Element of INT.Ring , ai,bi be Element of INT st $1 = [vv, uu] & a = ai & b = bi & ai <> 0 & bi <> 0 & v = (a * vv) & u = (b * uu) & $2 = (((ai " ) * (bi " )) * (( ScProductEM L) . (v,u)));

        

         A1: for x be Element of [:the carrier of D, the carrier of D:] holds ex y be Element of F_Real st P[x, y]

        proof

          let x be Element of [:the carrier of D, the carrier of D:];

          consider vv,uu be object such that

           B1: vv in the carrier of D & uu in the carrier of D & x = [vv, uu] by ZFMISC_1:def 2;

          reconsider vv, uu as Vector of D by B1;

          consider a be Element of INT.Ring such that

           B2: a <> ( 0. INT.Ring ) & (a * vv) in ( EMbedding L) by ZMODUL08: 29;

          reconsider v = (a * vv) as Vector of ( EMbedding L) by B2;

          consider b be Element of INT.Ring such that

           B3: b <> ( 0. INT.Ring ) & (b * uu) in ( EMbedding L) by ZMODUL08: 29;

          reconsider u = (b * uu) as Vector of ( EMbedding L) by B3;

          reconsider ai = a, bi = b as Element of INT ;

          take (((ai " ) * (bi " )) * (( ScProductEM L) . (v,u)));

          thus thesis by B1, B2, B3, XREAL_0:def 1;

        end;

        consider f be Function of [:the carrier of D, the carrier of D:], F_Real such that

         A2: for x be Element of [:the carrier of D, the carrier of D:] holds P[x, (f . x)] from FUNCT_2:sch 3( A1);

        take f;

        for vv,uu be Vector of D, v,u be Vector of Z, a,b be Element of INT.Ring , ai,bi be Element of F_Real st a = ai & b = bi & ai <> 0 & bi <> 0 & v = (a * vv) & u = (b * uu) holds (f . (vv,uu)) = (((ai " ) * (bi " )) * (( ScProductEM L) . (v,u)))

        proof

          let vv,uu be Vector of D, v,u be Vector of Z, a,b be Element of INT.Ring , ai0,bi0 be Element of F_Real such that

           B1: a = ai0 & b = bi0 & ai0 <> 0 & bi0 <> 0 & v = (a * vv) & u = (b * uu);

          reconsider ai = ai0, bi = bi0 as Element of INT by B1;

          consider vv1,uu1 be Vector of D, v1,u1 be Vector of Z, a1,b1 be Element of INT.Ring , a1i,b1i be Element of INT such that

           B2: [vv1, uu1] = [vv, uu] & a1 = a1i & b1 = b1i & a1i <> 0 & b1i <> 0 & v1 = (a1 * vv1) & u1 = (b1 * uu1) & (f . (vv,uu)) = (((a1i " ) * (b1i " )) * (( ScProductEM L) . (v1,u1))) by A2;

          

           B3: v1 = (a1 * vv) by B2, XTUPLE_0: 1;

          

           B4: u1 = (b1 * uu) by B2, XTUPLE_0: 1;

          reconsider a1ga = (a1i gcd ai), b1gb = (b1i gcd bi) as Element of INT.Ring by INT_1:def 2;

          

           BX: Z is Submodule of D by ZMODUL08: 24;

          

           B5: (a1ga * vv) in Z

          proof

            consider c10,c20 be Integer such that

             C10: (a1i gcd ai) = ((c10 * a1i) + (c20 * ai)) by NAT_D: 68;

            reconsider c1 = c10, c2 = c20 as Element of INT.Ring by INT_1:def 2;

            

             C2: ((c1 * a1) * vv) = (c1 * (a1 * vv)) by VECTSP_1:def 16

            .= (c1 * v1) by B3, BX, ZMODUL01: 29;

            

             C3: ((c2 * a) * vv) = (c2 * (a * vv)) by VECTSP_1:def 16

            .= (c2 * v) by B1, BX, ZMODUL01: 29;

            (a1ga * vv) = (((c1 * a1) + (c2 * a)) * vv) by B1, B2, C10

            .= (((c1 * a1) * vv) + ((c2 * a) * vv)) by VECTSP_1:def 15

            .= ((c1 * v1) + (c2 * v)) by C2, C3, BX, ZMODUL01: 28;

            hence (a1ga * vv) in Z;

          end;

          consider c10,c20 be Integer such that

           C10: (b1i gcd bi) = ((c10 * b1i) + (c20 * bi)) by NAT_D: 68;

          reconsider c1 = c10, c2 = c20 as Element of INT.Ring by INT_1:def 2;

          

           C2: ((c1 * b1) * uu) = (c1 * (b1 * uu)) by VECTSP_1:def 16

          .= (c1 * u1) by B4, BX, ZMODUL01: 29;

          

           C3: ((c2 * b) * uu) = (c2 * (b * uu)) by VECTSP_1:def 16

          .= (c2 * u) by B1, BX, ZMODUL01: 29;

          reconsider agv = (a1ga * vv) as Vector of Z by B5;

          (b1gb * uu) = (((c1 * b1) + (c2 * b)) * uu) by B1, B2, C10

          .= (((c1 * b1) * uu) + ((c2 * b) * uu)) by VECTSP_1:def 15

          .= ((c1 * u1) + (c2 * u)) by C2, C3, BX, ZMODUL01: 28;

          then

          reconsider bgu = (b1gb * uu) as Vector of Z;

          consider ci be Integer such that

           B7: ai = ((a1i gcd ai) * ci) by INT_1:def 3, INT_2: 21;

          consider c1i be Integer such that

           B8: a1i = ((a1i gcd ai) * c1i) by INT_1:def 3, INT_2: 21;

          consider di be Integer such that

           B9: bi = ((b1i gcd bi) * di) by INT_1:def 3, INT_2: 21;

          reconsider c = ci, d = di as Element of INT.Ring by INT_1:def 2;

          consider d1i be Integer such that

           B10: b1i = ((b1i gcd bi) * d1i) by INT_1:def 3, INT_2: 21;

          reconsider c = ci, c1 = c1i, d = di, d1 = d1i as Element of INT.Ring by INT_1:def 2;

          

           B11: v = ((c * a1ga) * vv) by B1, B7

          .= (c * (a1ga * vv)) by VECTSP_1:def 16

          .= (c * agv) by BX, ZMODUL01: 29;

          

           B12: v1 = ((c1 * a1ga) * vv) by B2, B8, XTUPLE_0: 1

          .= (c1 * (a1ga * vv)) by VECTSP_1:def 16

          .= (c1 * agv) by BX, ZMODUL01: 29;

          

           B13: u = ((d * b1gb) * uu) by B1, B9

          .= (d * (b1gb * uu)) by VECTSP_1:def 16

          .= (d * bgu) by BX, ZMODUL01: 29;

          

           B14: u1 = ((d1 * b1gb) * uu) by B2, B10, XTUPLE_0: 1

          .= (d1 * (b1gb * uu)) by VECTSP_1:def 16

          .= (d1 * bgu) by BX, ZMODUL01: 29;

          

           B15: ci <> 0 by B1, B7;

          

           B16: c1i <> 0 by B2, B8;

          

           B17: di <> 0 by B1, B9;

          

           B18: d1i <> 0 by B2, B10;

          

           B19: (f . (vv,uu)) = (((a1i " ) * (b1i " )) * (c1i * (( ScProductEM L) . (agv,(d1 * bgu))))) by B2, B12, B14, ThSPEM1

          .= (((a1i " ) * (b1i " )) * (c1i * (( ScProductEM L) . ((d1 * bgu),agv)))) by ThSPEM1

          .= (((a1i " ) * (b1i " )) * (c1i * (d1i * (( ScProductEM L) . (bgu,agv))))) by ThSPEM1

          .= (((a1i " ) * (b1i " )) * (c1i * (d1i * (( ScProductEM L) . (agv,bgu))))) by ThSPEM1

          .= (((((a1i " ) * (b1i " )) * c1i) * d1i) * (( ScProductEM L) . (agv,bgu)))

          .= (((((((a1i gcd ai) " ) * (c1i " )) * (((b1i gcd bi) * d1i) " )) * c1i) * d1i) * (( ScProductEM L) . (agv,bgu))) by B8, B10, XCMPLX_1: 204

          .= (((((((a1i gcd ai) " ) * c1i) * (c1i " )) * (((b1i gcd bi) * d1i) " )) * d1i) * (( ScProductEM L) . (agv,bgu)))

          .= (((((a1i gcd ai) " ) * (((b1i gcd bi) * d1i) " )) * d1i) * (( ScProductEM L) . (agv,bgu))) by B16, XCMPLX_1: 203

          .= ((((((b1i gcd bi) * d1i) " ) * d1i) * ((a1i gcd ai) " )) * (( ScProductEM L) . (agv,bgu)))

          .= ((((((b1i gcd bi) " ) * (d1i " )) * d1i) * ((a1i gcd ai) " )) * (( ScProductEM L) . (agv,bgu))) by XCMPLX_1: 204

          .= ((((((b1i gcd bi) " ) * d1i) * (d1i " )) * ((a1i gcd ai) " )) * (( ScProductEM L) . (agv,bgu)))

          .= ((((b1i gcd bi) " ) * ((a1i gcd ai) " )) * (( ScProductEM L) . (agv,bgu))) by B18, XCMPLX_1: 203;

          

           X1: (((ai " ) * (bi " )) * (( ScProductEM L) . (v,u))) = (((ai " ) * (bi " )) * (ci * (( ScProductEM L) . (agv,(d * bgu))))) by B11, B13, ThSPEM1

          .= (((ai " ) * (bi " )) * (ci * (( ScProductEM L) . ((d * bgu),agv)))) by ThSPEM1

          .= (((ai " ) * (bi " )) * (ci * (di * (( ScProductEM L) . (bgu,agv))))) by ThSPEM1

          .= (((ai " ) * (bi " )) * (ci * (di * (( ScProductEM L) . (agv,bgu))))) by ThSPEM1

          .= (((((((a1i gcd ai) * ci) " ) * (((b1i gcd bi) * di) " )) * ci) * di) * (( ScProductEM L) . (agv,bgu))) by B7, B9

          .= (((((((a1i gcd ai) " ) * (ci " )) * (((b1i gcd bi) * di) " )) * ci) * di) * (( ScProductEM L) . (agv,bgu))) by XCMPLX_1: 204

          .= (((((((a1i gcd ai) " ) * ci) * (ci " )) * (((b1i gcd bi) * di) " )) * di) * (( ScProductEM L) . (agv,bgu)))

          .= (((((a1i gcd ai) " ) * (((b1i gcd bi) * di) " )) * di) * (( ScProductEM L) . (agv,bgu))) by B15, XCMPLX_1: 203

          .= ((((((b1i gcd bi) * di) " ) * di) * ((a1i gcd ai) " )) * (( ScProductEM L) . (agv,bgu)))

          .= ((((((b1i gcd bi) " ) * (di " )) * di) * ((a1i gcd ai) " )) * (( ScProductEM L) . (agv,bgu))) by XCMPLX_1: 204

          .= ((((((b1i gcd bi) " ) * di) * (di " )) * ((a1i gcd ai) " )) * (( ScProductEM L) . (agv,bgu)))

          .= ((((b1i gcd bi) " ) * ((a1i gcd ai) " )) * (( ScProductEM L) . (agv,bgu))) by B17, XCMPLX_1: 203;

          (ai " ) = (ai0 " ) & (bi " ) = (bi0 " ) by LMINTFREAL1, B1;

          hence (f . (vv,uu)) = (((ai0 " ) * (bi0 " )) * (( ScProductEM L) . (v,u))) by X1, B19;

        end;

        hence thesis;

      end;

      uniqueness

      proof

        set Z = ( EMbedding L);

        set D = ( DivisibleMod L);

        let f1,f2 be Function of [:the carrier of D, the carrier of D:], F_Real ;

        assume

         AS1: for vv,uu be Vector of D, v,u be Vector of Z, a,b be Element of INT.Ring , ai,bi be Element of F_Real st a = ai & b = bi & ai <> 0 & bi <> 0 & v = (a * vv) & u = (b * uu) holds (f1 . (vv,uu)) = (((ai " ) * (bi " )) * (( ScProductEM L) . (v,u)));

        assume

         AS2: for vv,uu be Vector of D, v,u be Vector of Z, a,b be Element of INT.Ring , ai,bi be Element of F_Real st a = ai & b = bi & ai <> 0 & bi <> 0 & v = (a * vv) & u = (b * uu) holds (f2 . (vv,uu)) = (((ai " ) * (bi " )) * (( ScProductEM L) . (v,u)));

        for x be Element of [:the carrier of D, the carrier of D:] holds (f1 . x) = (f2 . x)

        proof

          let x be Element of [:the carrier of D, the carrier of D:];

          consider vv,uu be object such that

           B0: vv in the carrier of D & uu in the carrier of D & x = [vv, uu] by ZFMISC_1:def 2;

          reconsider vv, uu as Vector of D by B0;

          consider a be Element of INT.Ring such that

           B1: a <> 0 & (a * vv) in Z by ZMODUL08: 29;

          consider b be Element of INT.Ring such that

           B2: b <> 0 & (b * uu) in Z by ZMODUL08: 29;

          reconsider v = (a * vv) as Vector of Z by B1;

          reconsider u = (b * uu) as Vector of Z by B2;

           INT c= the carrier of F_Real by NUMBERS: 5;

          then

          reconsider ai = a, bi = b as Element of F_Real ;

          

          thus (f1 . x) = (f1 . (vv,uu)) by B0

          .= (((ai " ) * (bi " )) * (( ScProductEM L) . (v,u))) by AS1, B1, B2

          .= (f2 . (vv,uu)) by AS2, B1, B2

          .= (f2 . x) by B0;

        end;

        hence f1 = f2;

      end;

    end

    theorem :: ZMODLAT2:6

    

     ThSPDM1: for L be Z_Lattice holds (for x be Vector of ( DivisibleMod L) st for y be Vector of ( DivisibleMod L) holds (( ScProductDM L) . (x,y)) = 0 holds x = ( 0. ( DivisibleMod L))) & (for x,y be Vector of ( DivisibleMod L) holds (( ScProductDM L) . (x,y)) = (( ScProductDM L) . (y,x))) & (for x,y,z be Vector of ( DivisibleMod L), a be Element of INT.Ring holds (( ScProductDM L) . ((x + y),z)) = ((( ScProductDM L) . (x,z)) + (( ScProductDM L) . (y,z))) & (( ScProductDM L) . ((a * x),y)) = (a * (( ScProductDM L) . (x,y))))

    proof

      let L be Z_Lattice;

      set D = ( DivisibleMod L);

      set Z = ( EMbedding L);

      set f = ( ScProductDM L);

      

       A1: Z is Submodule of D by ZMODUL08: 24;

      thus for x be Vector of D st for y be Vector of D holds (f . (x,y)) = 0 holds x = ( 0. D)

      proof

        let x be Vector of D such that

         B1: for y be Vector of D holds (f . (x,y)) = 0 ;

        consider a be Element of INT.Ring such that

         B2: a <> ( 0. INT.Ring ) & (a * x) in Z by ZMODUL08: 29;

        reconsider xx = (a * x) as Vector of Z by B2;

        for yy be Vector of Z holds (( ScProductEM L) . (xx,yy)) = 0

        proof

          let yy be Vector of Z;

          set b = ( 1. INT.Ring );

          yy in Z;

          then yy in D by A1, ZMODUL01: 24;

          then

          reconsider y = (b * yy) as Vector of D by VECTSP_1:def 17;

          y = yy by VECTSP_1:def 17;

          then

           C1: b <> 0 & yy = (b * y) by VECTSP_1:def 17;

           INT c= the carrier of F_Real by NUMBERS: 5;

          then

          reconsider af = a, bf = b as Element of F_Real ;

          

           C2: (f . (x,y)) = (((af " ) * (bf " )) * (( ScProductEM L) . (xx,yy))) by B2, C1, defScProductDM;

          thus (( ScProductEM L) . (xx,yy)) = 0

          proof

            assume (( ScProductEM L) . (xx,yy)) <> 0 ;

            then

             XX1: (af " ) = 0 or (bf " ) = 0 by B1, C2;

            af <> ( 0. F_Real ) & bf <> ( 0. F_Real ) by B2;

            hence contradiction by XX1, VECTSP_1: 25;

          end;

        end;

        

        then xx = ( 0. Z) by ThSPEM1

        .= ( 0. D) by A1, ZMODUL01: 26;

        hence x = ( 0. D) by B2, ZMODUL01:def 7;

      end;

      thus for x,y be Vector of D holds (f . (x,y)) = (f . (y,x))

      proof

        let x,y be Vector of D;

        consider a be Element of INT.Ring such that

         B1: a <> 0 & (a * x) in Z by ZMODUL08: 29;

        reconsider xx = (a * x) as Vector of Z by B1;

        consider b be Element of INT.Ring such that

         B2: b <> 0 & (b * y) in Z by ZMODUL08: 29;

        reconsider yy = (b * y) as Vector of Z by B2;

         INT c= the carrier of F_Real by NUMBERS: 5;

        then

        reconsider af = a, bf = b as Element of F_Real ;

        

        thus (f . (x,y)) = (((af " ) * (bf " )) * (( ScProductEM L) . (xx,yy))) by B1, B2, defScProductDM

        .= (((bf " ) * (af " )) * (( ScProductEM L) . (yy,xx))) by ThSPEM1

        .= (f . (y,x)) by B1, B2, defScProductDM;

      end;

      thus for x,y,z be Vector of D, i be Element of INT.Ring holds (f . ((x + y),z)) = ((f . (x,z)) + (f . (y,z))) & (f . ((i * x),y)) = (i * (f . (x,y)))

      proof

        let x,y,z be Vector of D, i be Element of INT.Ring ;

        consider a be Element of INT.Ring such that

         B1: a <> 0 & (a * x) in Z by ZMODUL08: 29;

        reconsider xx = (a * x) as Vector of Z by B1;

        consider b be Element of INT.Ring such that

         B2: b <> 0 & (b * y) in Z by ZMODUL08: 29;

        reconsider yy = (b * y) as Vector of Z by B2;

        consider c be Element of INT.Ring such that

         B3: c <> 0 & (c * z) in Z by ZMODUL08: 29;

        reconsider zz = (c * z) as Vector of Z by B3;

        

         B41: (b * (a * x)) = (b * xx) by A1, ZMODUL01: 29;

        

         B42: (a * (b * y)) = (a * yy) by A1, ZMODUL01: 29;

        

         B4: ((a * b) * (x + y)) = (((a * b) * x) + ((a * b) * y)) by VECTSP_1:def 14

        .= (((b * a) * x) + (a * (b * y))) by VECTSP_1:def 16

        .= ((b * (a * x)) + (a * (b * y))) by VECTSP_1:def 16

        .= ((b * xx) + (a * yy)) by A1, B41, B42, ZMODUL01: 28;

        then

        reconsider xy = ((a * b) * (x + y)) as Vector of Z;

         INT c= the carrier of F_Real by NUMBERS: 5;

        then

        reconsider af = a, bf = b, cf = c as Element of F_Real ;

        

         X2: af <> ( 0. F_Real ) & bf <> ( 0. F_Real ) by B1, B2;

        then

         X1: (((af * bf) " ) * (cf " )) = (((af " ) * (bf " )) * (cf " )) by VECTSP_2: 11;

        

        thus (f . ((x + y),z)) = ((((af " ) * (bf " )) * (cf " )) * (( ScProductEM L) . (xy,zz))) by B1, B2, B3, X1, defScProductDM

        .= ((((af " ) * (bf " )) * (cf " )) * ((( ScProductEM L) . ((b * xx),zz)) + (( ScProductEM L) . ((a * yy),zz)))) by B4, ThSPEM1

        .= (((((af " ) * (bf " )) * (cf " )) * (( ScProductEM L) . ((b * xx),zz))) + ((((af " ) * (bf " )) * (cf " )) * (( ScProductEM L) . ((a * yy),zz))))

        .= (((((af " ) * (bf " )) * (cf " )) * (b * (( ScProductEM L) . (xx,zz)))) + ((((af " ) * (bf " )) * (cf " )) * (( ScProductEM L) . ((a * yy),zz)))) by ThSPEM1

        .= (((((af " ) * ((bf " ) * bf)) * (cf " )) * (( ScProductEM L) . (xx,zz))) + ((((af " ) * (bf " )) * (cf " )) * (( ScProductEM L) . ((a * yy),zz))))

        .= (((((af " ) * ( 1. F_Real )) * (cf " )) * (( ScProductEM L) . (xx,zz))) + ((((af " ) * (bf " )) * (cf " )) * (( ScProductEM L) . ((a * yy),zz)))) by VECTSP_1:def 10, X2

        .= ((((af " ) * (cf " )) * (( ScProductEM L) . (xx,zz))) + ((((af " ) * (bf " )) * (cf " )) * (a * (( ScProductEM L) . (yy,zz))))) by ThSPEM1

        .= ((((af " ) * (cf " )) * (( ScProductEM L) . (xx,zz))) + ((((bf " ) * (af * (af " ))) * (cf " )) * (( ScProductEM L) . (yy,zz))))

        .= ((((af " ) * (cf " )) * (( ScProductEM L) . (xx,zz))) + ((((bf " ) * ( 1. F_Real )) * (cf " )) * (( ScProductEM L) . (yy,zz)))) by VECTSP_1:def 10, X2

        .= ((f . (x,z)) + (((bf " ) * (cf " )) * (( ScProductEM L) . (yy,zz)))) by B1, B3, defScProductDM

        .= ((f . (x,z)) + (f . (y,z))) by B2, B3, defScProductDM;

        (a * (i * x)) = ((a * i) * x) by VECTSP_1:def 16

        .= (i * (a * x)) by VECTSP_1:def 16

        .= (i * xx) by A1, ZMODUL01: 29;

        

        hence (f . ((i * x),y)) = (((af " ) * (bf " )) * (( ScProductEM L) . ((i * xx),yy))) by B1, B2, defScProductDM

        .= (((af " ) * (bf " )) * (i * (( ScProductEM L) . (xx,yy)))) by ThSPEM1

        .= (i * (((af " ) * (bf " )) * (( ScProductEM L) . (xx,yy))))

        .= (i * (f . (x,y))) by B1, B2, defScProductDM;

      end;

    end;

    theorem :: ZMODLAT2:7

    

     ThSPEM2: for L be Z_Lattice holds ( ScProductEM L) = (( ScProductDM L) || ( rng ( MorphsZQ L)))

    proof

      let L be Z_Lattice;

      

       P1: [:the carrier of ( EMbedding L), the carrier of ( EMbedding L):] = [:the carrier of ( EMbedding L), ( rng ( MorphsZQ L)):] by ZMODUL08:def 3

      .= [:( rng ( MorphsZQ L)), ( rng ( MorphsZQ L)):] by ZMODUL08:def 3;

      

       P2: [:the carrier of ( DivisibleMod L), the carrier of ( DivisibleMod L):] = [:the carrier of ( DivisibleMod L), ( Class ( EQRZM L)):] by ZMODUL08:def 4

      .= [:( Class ( EQRZM L)), ( Class ( EQRZM L)):] by ZMODUL08:def 4;

      

       A0: ( EMbedding L) is Submodule of ( DivisibleMod L) by ZMODUL08: 24;

      then the carrier of ( EMbedding L) c= the carrier of ( DivisibleMod L) by VECTSP_4:def 2;

      then ( rng ( MorphsZQ L)) c= the carrier of ( DivisibleMod L) by ZMODUL08:def 3;

      then ( rng ( MorphsZQ L)) c= ( Class ( EQRZM L)) by ZMODUL08:def 4;

      then [:( rng ( MorphsZQ L)), ( rng ( MorphsZQ L)):] c= [:( Class ( EQRZM L)), ( Class ( EQRZM L)):] by ZFMISC_1: 96;

      then

      reconsider scd = (( ScProductDM L) || ( rng ( MorphsZQ L))) as Function of [:( rng ( MorphsZQ L)), ( rng ( MorphsZQ L)):], the carrier of F_Real by P2, FUNCT_2: 32;

      for x be object st x in [:( rng ( MorphsZQ L)), ( rng ( MorphsZQ L)):] holds (( ScProductEM L) . x) = (scd . x)

      proof

        let x be object such that

         B1: x in [:( rng ( MorphsZQ L)), ( rng ( MorphsZQ L)):];

        consider x1,x2 be object such that

         B2: x1 in ( rng ( MorphsZQ L)) & x2 in ( rng ( MorphsZQ L)) & x = [x1, x2] by B1, ZFMISC_1:def 2;

        reconsider x1, x2 as Vector of ( EMbedding L) by B2, ZMODUL08:def 3;

        set a = ( 1. INT.Ring );

        x1 in ( EMbedding L);

        then x1 in ( DivisibleMod L) by A0, ZMODUL01: 24;

        then

        reconsider xx1 = x1 as Vector of ( DivisibleMod L);

        x2 in ( EMbedding L);

        then x2 in ( DivisibleMod L) by A0, ZMODUL01: 24;

        then

        reconsider xx2 = x2 as Vector of ( DivisibleMod L);

        

         B3: x1 = (a * xx1) by VECTSP_1:def 17;

        

         B4: x2 = (a * xx2) by VECTSP_1:def 17;

        

        thus (( ScProductEM L) . x) = ((( 1. F_Real ) * (( 1. F_Real ) " )) * (( ScProductEM L) . (x1,x2))) by B2

        .= (( ScProductDM L) . (xx1,xx2)) by B3, B4, defScProductDM

        .= (scd . x) by B2, FUNCT_1: 49, ZFMISC_1: 87;

      end;

      hence thesis by P1, FUNCT_2: 12;

    end;

    theorem :: ZMODLAT2:8

    

     ThSPEM3: for L be Z_Lattice, v1,v2 be Vector of ( DivisibleMod L), u1,u2 be Vector of ( EMbedding L) st v1 = u1 & v2 = u2 holds (( ScProductEM L) . (u1,u2)) = (( ScProductDM L) . (v1,v2))

    proof

      let L be Z_Lattice, v1,v2 be Vector of ( DivisibleMod L), u1,u2 be Vector of ( EMbedding L) such that

       A1: v1 = u1 & v2 = u2;

      

       A2: u1 = (( 1. INT.Ring ) * v1) & u2 = (( 1. INT.Ring ) * v2) by A1, VECTSP_1:def 17;

      

      thus (( ScProductDM L) . (v1,v2)) = (((( 1. F_Real ) " ) * (( 1. F_Real ) " )) * (( ScProductEM L) . (u1,u2))) by A2, defScProductDM

      .= (( ScProductEM L) . (u1,u2));

    end;

    theorem :: ZMODLAT2:9

    

     ThSPrEM1: for L be Z_Lattice, r be Element of F_Rat , v,u be Vector of ( EMbedding (r,L)) holds ((( ScProductDM L) || the carrier of ( EMbedding (r,L))) . (v,u)) = (( ScProductDM L) . (v,u))

    proof

      let L be Z_Lattice, r be Element of F_Rat , v,u be Vector of ( EMbedding (r,L));

      set Z = ( EMbedding (r,L));

      Z is Submodule of ( DivisibleMod L) by ZMODUL08: 32;

      then the carrier of Z c= the carrier of ( DivisibleMod L) by VECTSP_4:def 2;

      then [:the carrier of Z, the carrier of Z:] c= [:the carrier of ( DivisibleMod L), the carrier of ( DivisibleMod L):] by ZFMISC_1: 96;

      then

      reconsider sc = (( ScProductDM L) || the carrier of Z) as Function of [:the carrier of Z, the carrier of Z:], the carrier of F_Real by FUNCT_2: 32;

       [v, u] in [:the carrier of Z, the carrier of Z:];

      hence thesis by FUNCT_1: 49;

    end;

    theorem :: ZMODLAT2:10

    for L be Z_Lattice, A be non empty set, ze be Element of A, ad be BinOp of A, mu be Function of [:the carrier of INT.Ring , A:], A, sc be Function of [:A, A:], the carrier of F_Real st A is linearly-closed Subset of ( DivisibleMod L) & ze = ( 0. ( DivisibleMod L)) & ad = (the addF of ( DivisibleMod L) || A) & mu = (the lmult of ( DivisibleMod L) | [:the carrier of INT.Ring , A:]) holds LatticeStr (# A, ad, ze, mu, sc #) is Submodule of ( DivisibleMod L)

    proof

      let L be Z_Lattice, A be non empty set, ze be Element of A, ad be BinOp of A, mu be Function of [:the carrier of INT.Ring , A:], A, sc be Function of [:A, A:], the carrier of F_Real such that

       A1: A is linearly-closed Subset of ( DivisibleMod L) & ze = ( 0. ( DivisibleMod L)) & ad = (the addF of ( DivisibleMod L) || A) & mu = (the lmult of ( DivisibleMod L) | [:the carrier of INT.Ring , A:]);

      set L1 = LatticeStr (# A, ad, ze, mu, sc #);

      set V1 = ModuleStr (# A, ad, ze, mu #);

      

       A2: V1 is Submodule of ( DivisibleMod L) by A1, ZMODUL01: 40;

      reconsider V1 as Z_Module by A1, ZMODUL01: 40;

      reconsider scc = sc as Function of [:the carrier of V1, the carrier of V1:], the carrier of F_Real ;

      L1 = ( GenLat (V1,scc));

      then L1 is Submodule of V1 by ZMODLAT1: 2;

      hence thesis by A2, ZMODUL01: 42;

    end;

    theorem :: ZMODLAT2:11

    

     ThScDM1: for L be Z_Lattice, v,u be Vector of ( DivisibleMod L) holds (( ScProductDM L) . (( - v),u)) = ( - (( ScProductDM L) . (v,u))) & (( ScProductDM L) . (u,( - v))) = ( - (( ScProductDM L) . (u,v)))

    proof

      let L be Z_Lattice, v,u be Vector of ( DivisibleMod L);

      

      thus

       A1: (( ScProductDM L) . (( - v),u)) = (( ScProductDM L) . ((( - ( 1. INT.Ring )) * v),u)) by ZMODUL01: 2

      .= (( - 1) * (( ScProductDM L) . (v,u))) by ThSPDM1

      .= ( - (( ScProductDM L) . (v,u)));

      

      thus (( ScProductDM L) . (u,( - v))) = (( ScProductDM L) . (( - v),u)) by ThSPDM1

      .= ( - (( ScProductDM L) . (u,v))) by A1, ThSPDM1;

    end;

    theorem :: ZMODLAT2:12

    for L be Z_Lattice, v,u,w be Vector of ( DivisibleMod L) holds (( ScProductDM L) . (v,(u + w))) = ((( ScProductDM L) . (v,u)) + (( ScProductDM L) . (v,w)))

    proof

      let L be Z_Lattice, v,u,w be Vector of ( DivisibleMod L);

      

      thus (( ScProductDM L) . (v,(u + w))) = (( ScProductDM L) . ((u + w),v)) by ThSPDM1

      .= ((( ScProductDM L) . (u,v)) + (( ScProductDM L) . (w,v))) by ThSPDM1

      .= ((( ScProductDM L) . (u,v)) + (( ScProductDM L) . (v,w))) by ThSPDM1

      .= ((( ScProductDM L) . (v,u)) + (( ScProductDM L) . (v,w))) by ThSPDM1;

    end;

    theorem :: ZMODLAT2:13

    for L be Z_Lattice, v,u be Vector of ( DivisibleMod L), a be Element of INT.Ring holds (( ScProductDM L) . (v,(a * u))) = (a * (( ScProductDM L) . (v,u)))

    proof

      let L be Z_Lattice, v,u be Vector of ( DivisibleMod L), a be Element of INT.Ring ;

      

      thus (( ScProductDM L) . (v,(a * u))) = (( ScProductDM L) . ((a * u),v)) by ThSPDM1

      .= (a * (( ScProductDM L) . (u,v))) by ThSPDM1

      .= (a * (( ScProductDM L) . (v,u))) by ThSPDM1;

    end;

    theorem :: ZMODLAT2:14

    

     ThScDM6: for L be Z_Lattice, v be Vector of ( DivisibleMod L) holds (( ScProductDM L) . (( 0. ( DivisibleMod L)),v)) = 0 & (( ScProductDM L) . (v,( 0. ( DivisibleMod L)))) = 0

    proof

      let L be Z_Lattice, v be Vector of ( DivisibleMod L);

      

      thus

       A1: (( ScProductDM L) . (( 0. ( DivisibleMod L)),v)) = (( ScProductDM L) . ((v - v),v)) by RLVECT_1: 15

      .= ((( ScProductDM L) . (v,v)) + (( ScProductDM L) . (( - v),v))) by ThSPDM1

      .= ((( ScProductDM L) . (v,v)) - (( ScProductDM L) . (v,v))) by ThScDM1

      .= 0 ;

      thus (( ScProductDM L) . (v,( 0. ( DivisibleMod L)))) = 0 by A1, ThSPDM1;

    end;

    theorem :: ZMODLAT2:15

    

     LmDE22: for L be Z_Lattice, v be Vector of ( DivisibleMod L), I be Basis of ( EMbedding L) st for u be Vector of ( DivisibleMod L) st u in I holds (( ScProductDM L) . (v,u)) = 0 holds for u be Vector of ( DivisibleMod L) holds (( ScProductDM L) . (v,u)) = 0

    proof

      let L be Z_Lattice, v be Vector of ( DivisibleMod L), I be Basis of ( EMbedding L) such that

       A1: for u be Vector of ( DivisibleMod L) st u in I holds (( ScProductDM L) . (v,u)) = 0 ;

      defpred P[ Nat] means for I be finite Subset of ( EMbedding L) st ( card I) = $1 & I is linearly-independent & for u be Vector of ( DivisibleMod L) st u in I holds (( ScProductDM L) . (v,u)) = 0 holds for w be Vector of ( DivisibleMod L) st w in ( Lin I) holds (( ScProductDM L) . (v,w)) = 0 ;

      

       P1: P[ 0 ]

      proof

        let I be finite Subset of ( EMbedding L) such that

         B1: ( card I) = 0 & I is linearly-independent & for u be Vector of ( DivisibleMod L) st u in I holds (( ScProductDM L) . (v,u)) = 0 ;

        I = ( {} the carrier of ( EMbedding L)) by B1;

        then

         B2: ( Lin I) = ( (0). ( EMbedding L)) by ZMODUL02: 67;

        thus for w be Vector of ( DivisibleMod L) st w in ( Lin I) holds (( ScProductDM L) . (v,w)) = 0

        proof

          let w be Vector of ( DivisibleMod L) such that

           C1: w in ( Lin I);

          w = ( 0. ( EMbedding L)) by B2, C1, ZMODUL02: 66

          .= ( zeroCoset L) by ZMODUL08:def 3

          .= ( 0. ( DivisibleMod L)) by ZMODUL08:def 4;

          hence thesis by ThScDM6;

        end;

      end;

      

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

      proof

        let n be Nat such that

         B1: P[n];

        let I be finite Subset of ( EMbedding L) such that

         B2: ( card I) = (n + 1) & I is linearly-independent & for u be Vector of ( DivisibleMod L) st u in I holds (( ScProductDM L) . (v,u)) = 0 ;

        I is non empty by B2;

        then

        consider u be object such that

         B3: u in I;

        reconsider u as Vector of ( EMbedding L) by B3;

        set Iu = (I \ {u});

         {u} is Subset of I by B3, SUBSET_1: 41;

        

        then

         B4: ( card Iu) = ((n + 1) - ( card {u})) by B2, CARD_2: 44

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

        .= n;

        reconsider Iu as finite Subset of ( EMbedding L);

        I = (Iu \/ {u}) by B3, XBOOLE_1: 45, ZFMISC_1: 31;

        then

         B5: ( Lin I) = (( Lin Iu) + ( Lin {u})) by ZMODUL02: 72;

        

         B7: Iu c= I by XBOOLE_1: 36;

        

         B6: Iu is linearly-independent by B2, XBOOLE_1: 36, ZMODUL02: 56;

        

         B8: for w be Vector of ( DivisibleMod L) st w in Iu holds (( ScProductDM L) . (v,w)) = 0 by B2, B7;

        thus for w be Vector of ( DivisibleMod L) st w in ( Lin I) holds (( ScProductDM L) . (v,w)) = 0

        proof

          let w be Vector of ( DivisibleMod L) such that

           C1: w in ( Lin I);

          consider w1,w2 be Vector of ( EMbedding L) such that

           C2: w1 in ( Lin Iu) & w2 in ( Lin {u}) & w = (w1 + w2) by B5, C1, ZMODUL01: 92;

          

           CX: ( EMbedding L) is Submodule of ( DivisibleMod L) by ZMODUL08: 24;

          then

           C9: w1 is Vector of ( DivisibleMod L) by ZMODUL01: 25;

          reconsider ww1 = w1 as Vector of ( DivisibleMod L) by CX, ZMODUL01: 25;

          consider i be Element of INT.Ring such that

           C4: w2 = (i * u) by C2, ZMODUL06: 19;

          u is Element of ( DivisibleMod L) by CX, ZMODUL01: 25;

          then

           C6: (( ScProductDM L) . (v,u)) = 0 by B2, B3;

          reconsider uu = u as Element of ( DivisibleMod L) by CX, ZMODUL01: 25;

          (i * uu) in ( DivisibleMod L);

          then

          reconsider ww2 = w2 as Vector of ( DivisibleMod L) by C4, CX, ZMODUL01: 29;

          

           C8: (( ScProductDM L) . (v,(i * u))) = (( ScProductDM L) . (v,(i * uu))) by CX, ZMODUL01: 29

          .= (( ScProductDM L) . ((i * uu),v)) by ThSPDM1

          .= (i * (( ScProductDM L) . (uu,v))) by ThSPDM1

          .= (i * (( ScProductDM L) . (v,u))) by ThSPDM1;

          

           C10: w = (ww1 + ww2) by C2, CX, ZMODUL01: 28;

          (( ScProductDM L) . (v,w)) = (( ScProductDM L) . (w,v)) by ThSPDM1

          .= ((( ScProductDM L) . (ww1,v)) + (( ScProductDM L) . (ww2,v))) by C10, ThSPDM1

          .= ((( ScProductDM L) . (v,w1)) + (( ScProductDM L) . (ww2,v))) by ThSPDM1

          .= ((( ScProductDM L) . (v,w1)) + (( ScProductDM L) . (v,w2))) by ThSPDM1;

          hence thesis by B1, B4, B6, B8, C2, C4, C6, C8, C9;

        end;

      end;

      

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

      

       P4: ( card I) is Nat;

      

       P5: I is linearly-independent & ( EMbedding L) = ( Lin I) by VECTSP_7:def 3;

      thus for w be Vector of ( DivisibleMod L) holds (( ScProductDM L) . (v,w)) = 0

      proof

        let w be Vector of ( DivisibleMod L);

        consider a be Element of INT.Ring such that

         B1: a <> ( 0. INT.Ring ) & (a * w) in ( EMbedding L) by ZMODUL08: 29;

        (( ScProductDM L) . (v,(a * w))) = (( ScProductDM L) . ((a * w),v)) by ThSPDM1

        .= (a * (( ScProductDM L) . (w,v))) by ThSPDM1

        .= (a * (( ScProductDM L) . (v,w))) by ThSPDM1;

        hence thesis by A1, B1, P3, P4, P5;

      end;

    end;

    theorem :: ZMODLAT2:16

    for L be Z_Lattice, v be Vector of ( DivisibleMod L), I be Basis of ( EMbedding L) st for u be Vector of ( DivisibleMod L) st u in I holds (( ScProductDM L) . (v,u)) = 0 holds v = ( 0. ( DivisibleMod L))

    proof

      let L be Z_Lattice, v be Vector of ( DivisibleMod L), I be Basis of ( EMbedding L) such that

       A1: for u be Vector of ( DivisibleMod L) st u in I holds (( ScProductDM L) . (v,u)) = 0 ;

      for u be Vector of ( DivisibleMod L) holds (( ScProductDM L) . (v,u)) = 0 by A1, LmDE22;

      hence thesis by ThSPDM1;

    end;

    theorem :: ZMODLAT2:17

    for R be Ring, V be LeftMod of R, v be Vector of V, u be object st u in ( Lin {v}) holds ex i be Element of R st u = (i * v)

    proof

      let R be Ring, V be LeftMod of R, v be Vector of V, u be object such that

       A1: u in ( Lin {v});

      consider l be Linear_Combination of {v} such that

       A2: u = ( Sum l) by A1, VECTSP_7: 7;

      take (l . v);

      thus thesis by A2, VECTSP_6: 17;

    end;

    theorem :: ZMODLAT2:18

    

     ThLin2: for R be Ring, V be LeftMod of R, v be Vector of V holds v in ( Lin {v}) by VECTSP_7: 8, ZFMISC_1: 31;

    theorem :: ZMODLAT2:19

    for R be Ring, V be LeftMod of R, v be Vector of V, i be Element of R holds (i * v) in ( Lin {v}) by ThLin2, VECTSP_4: 21;

    begin

    definition

      let L be Z_Lattice;

      :: ZMODLAT2:def4

      func EMLat (L) -> strict Z_Lattice means

      : defEMLat: the carrier of it = ( rng ( MorphsZQ L)) & the ZeroF of it = ( zeroCoset L) & the addF of it = (( addCoset L) || ( rng ( MorphsZQ L))) & the lmult of it = (( lmultCoset L) | [:the carrier of INT.Ring , ( rng ( MorphsZQ L)):]) & the scalar of it = ( ScProductEM L);

      existence

      proof

        set Z = LatticeStr (# the carrier of ( EMbedding L), the addF of ( EMbedding L), ( 0. ( EMbedding L)), the lmult of ( EMbedding L), ( ScProductEM L) #);

        

         AX: Z = ( GenLat (( EMbedding L),( ScProductEM L)));

        then

        reconsider Z as Abelian add-associative right_zeroed right_complementable scalar-distributive vector-distributive scalar-associative scalar-unital non empty LatticeStr over INT.Ring ;

        reconsider Z as free Abelian add-associative right_zeroed right_complementable scalar-distributive vector-distributive scalar-associative scalar-unital non empty LatticeStr over INT.Ring by AX;

        Z is Z_Lattice-like

        proof

          thus for x be Vector of Z st for y be Vector of Z holds <;x, y;> = 0 holds x = ( 0. Z)

          proof

            let x be Vector of Z such that

             B1: for y be Vector of Z holds <;x, y;> = 0 ;

            for y be Vector of Z holds (( ScProductEM L) . (x,y)) = 0

            proof

              let y be Vector of Z;

              

              thus (( ScProductEM L) . (x,y)) = <;x, y;>

              .= 0 by B1;

            end;

            hence thesis by ThSPEM1;

          end;

          thus for x,y be Vector of Z holds <;x, y;> = <;y, x;>

          proof

            let x,y be Vector of Z;

            

            thus <;x, y;> = (( ScProductEM L) . (x,y))

            .= (( ScProductEM L) . (y,x)) by ThSPEM1

            .= <;y, x;>;

          end;

          thus for x,y,z be Vector of Z, a be Element of INT.Ring holds <;(x + y), z;> = ( <;x, z;> + <;y, z;>) & <;(a * x), y;> = (a * <;x, y;>)

          proof

            let x,y,z be Vector of Z, a be Element of INT.Ring ;

            reconsider xx = x, yy = y, zz = z as Vector of ( EMbedding L);

            

            thus <;(x + y), z;> = (( ScProductEM L) . ((xx + yy),zz))

            .= ((the scalar of Z . (x,z)) + (the scalar of Z . (y,z))) by ThSPEM1

            .= ( <;x, z;> + <;y, z;>);

            

            thus <;(a * x), y;> = (( ScProductEM L) . ((a * xx),y))

            .= (a * (( ScProductEM L) . (xx,y))) by ThSPEM1

            .= (a * <;x, y;>);

          end;

        end;

        then

        reconsider Z as strict Z_Lattice by AX;

        take Z;

        thus thesis by ZMODUL08:def 3;

      end;

      uniqueness ;

    end

    definition

      let L be Z_Lattice;

      let r be Element of F_Rat ;

      :: ZMODLAT2:def5

      func EMLat (r,L) -> strict Z_Lattice means

      : defrEMLat: the carrier of it = (r * ( rng ( MorphsZQ L))) & the ZeroF of it = ( zeroCoset L) & the addF of it = (( addCoset L) || (r * ( rng ( MorphsZQ L)))) & the lmult of it = (( lmultCoset L) | [:the carrier of INT.Ring , (r * ( rng ( MorphsZQ L))):]) & the scalar of it = (( ScProductDM L) || (r * ( rng ( MorphsZQ L))));

      existence

      proof

        ( EMbedding (r,L)) is Submodule of ( DivisibleMod L) by ZMODUL08: 32;

        then the carrier of ( EMbedding (r,L)) c= the carrier of ( DivisibleMod L) by VECTSP_4:def 2;

        then [:the carrier of ( EMbedding (r,L)), the carrier of ( EMbedding (r,L)):] c= [:the carrier of ( DivisibleMod L), the carrier of ( DivisibleMod L):] by ZFMISC_1: 96;

        then

        reconsider sc = (( ScProductDM L) || the carrier of ( EMbedding (r,L))) as Function of [:the carrier of ( EMbedding (r,L)), the carrier of ( EMbedding (r,L)):], the carrier of F_Real by FUNCT_2: 32;

        set Z = LatticeStr (# the carrier of ( EMbedding (r,L)), the addF of ( EMbedding (r,L)), ( 0. ( EMbedding (r,L))), the lmult of ( EMbedding (r,L)), sc #);

        

         AZ: Z = ( GenLat (( EMbedding (r,L)),sc));

        

         A0: Z is Submodule of ( EMbedding (r,L)) by AZ, ZMODLAT1: 2;

        reconsider Z as Abelian add-associative right_zeroed right_complementable scalar-distributive vector-distributive scalar-associative scalar-unital non empty LatticeStr over INT.Ring by AZ;

        

         AX: ( EMbedding (r,L)) is Submodule of ( DivisibleMod L) by ZMODUL08: 32;

        then

         AX2: Z is Submodule of ( DivisibleMod L) by A0, ZMODUL01: 42;

        reconsider Z as free Abelian add-associative right_zeroed right_complementable scalar-distributive vector-distributive scalar-associative scalar-unital non empty LatticeStr over INT.Ring by AZ;

        Z is Z_Lattice-like

        proof

          thus for x be Vector of Z st for y be Vector of Z holds <;x, y;> = 0 holds x = ( 0. Z)

          proof

            let x be Vector of Z such that

             B1: for y be Vector of Z holds <;x, y;> = 0 ;

            per cases ;

              suppose

               C1: r is zero;

              x in the carrier of ( EMbedding (r,L));

              then x in (r * ( rng ( MorphsZQ L))) by ZMODUL08:def 6;

              then

              consider y be Vector of ( Z_MQ_VectSp L) such that

               C2: x = (( 0. F_Rat ) * y) & y in ( rng ( MorphsZQ L)) by C1;

              

              thus x = ( 0. ( Z_MQ_VectSp L)) by C2, VECTSP_1: 14

              .= ( 0. Z) by ZMODUL08: 25;

            end;

              suppose

               AS: r is non zero;

              then

              consider T be linear-transformation of ( EMbedding L), ( EMbedding (r,L)) such that

               B2: (for v be Element of ( Z_MQ_VectSp L) st v in ( EMbedding L) holds (T . v) = (r * v)) & T is bijective by ZMODUL08: 27;

              consider rm0,rn0 be Integer such that

               BX: rn0 <> 0 & r = (rm0 / rn0) by RAT_1: 1;

              reconsider rn = rn0, rm = rm0 as Element of INT.Ring by INT_1:def 2;

               INT c= the carrier of F_Real by NUMBERS: 5;

              then

              reconsider rnf = rn, rmf = rm as Element of F_Real ;

              x in the carrier of ( EMbedding (r,L));

              then x in ( rng T) by B2, FUNCT_2:def 3;

              then

              consider xe be object such that

               B3: xe in the carrier of ( EMbedding L) & x = (T . xe) by FUNCT_2: 11;

              reconsider xz = xe as Vector of ( Z_MQ_VectSp L) by B3, ZMODUL08: 19;

              reconsider xd = xz as Vector of ( DivisibleMod L) by ZMODUL08: 30;

              consider zxd be Vector of ( DivisibleMod L) such that

               BY: xd = (rn * zxd) & (r * xz) = (rm * zxd) by AS, BX, ZMODUL08: 31;

              reconsider xe as Vector of ( EMbedding L) by B3;

              for ye be Vector of ( EMbedding L) holds (( ScProductEM L) . (xe,ye)) = 0

              proof

                let ye be Vector of ( EMbedding L);

                reconsider yz = ye as Vector of ( Z_MQ_VectSp L) by ZMODUL08: 19;

                reconsider yd = yz as Vector of ( DivisibleMod L) by ZMODUL08: 30;

                consider zyd be Vector of ( DivisibleMod L) such that

                 C1: yd = (rn * zyd) & (r * yz) = (rm * zyd) by AS, BX, ZMODUL08: 31;

                reconsider y = (T . ye) as Vector of ( EMbedding (r,L));

                reconsider y as Vector of Z;

                reconsider xd1 = xd as Vector of ( EMbedding L) by B3;

                reconsider yd1 = yd as Vector of ( EMbedding L);

                

                 C7: xz in ( EMbedding L) by B3;

                

                 C8: yz in ( EMbedding L);

                

                 C5: x = (rm * zxd) by B2, B3, BY, C7;

                

                 C6: y = (rm * zyd) by B2, C1, C8;

                

                 CX: <;x, y;> = (sc . (x,y))

                .= (( ScProductDM L) . ((rm * zxd),y)) by C5, ThSPrEM1

                .= (rm * (( ScProductDM L) . (zxd,(rm * zyd)))) by C6, ThSPDM1

                .= (rm * (( ScProductDM L) . ((rm * zyd),zxd))) by ThSPDM1

                .= (rm * (rm * (( ScProductDM L) . (zyd,zxd)))) by ThSPDM1

                .= (rm * (rm * (( ScProductDM L) . (zxd,zyd)))) by ThSPDM1

                .= ((rmf * rmf) * (( ScProductDM L) . (zxd,zyd)))

                .= ((rmf * rmf) * (((rnf " ) * (rnf " )) * (( ScProductEM L) . (xd1,yd1)))) by BX, BY, C1, defScProductDM

                .= ((((rmf * rmf) * (rnf " )) * (rnf " )) * (( ScProductEM L) . (xd,yd)));

                rnf <> ( 0. F_Real ) by BX;

                then rmf <> 0 & (rnf " ) <> 0 by AS, BX, VECTSP_1: 25;

                hence (( ScProductEM L) . (xe,ye)) = 0 by B1, CX;

              end;

              

              then

               B6: xz = ( 0. ( EMbedding L)) by ThSPEM1

              .= ( 0. ( Z_MQ_VectSp L)) by ZMODUL08: 19;

              xe in ( EMbedding L);

              

              then (T . xe) = (r * xz) by B2

              .= ( 0. ( Z_MQ_VectSp L)) by B6, VECTSP_1: 15

              .= ( 0. Z) by ZMODUL08: 25;

              hence thesis by B3;

            end;

          end;

          thus for x,y be Vector of Z holds <;x, y;> = <;y, x;>

          proof

            let x,y be Vector of Z;

            reconsider xx = x, yy = y as Vector of ( DivisibleMod L) by AX, ZMODUL01: 25;

            

            thus <;x, y;> = (the scalar of Z . (x,y))

            .= (( ScProductDM L) . (xx,yy)) by ThSPrEM1

            .= (( ScProductDM L) . (yy,xx)) by ThSPDM1

            .= (the scalar of Z . (y,x)) by ThSPrEM1

            .= <;y, x;>;

          end;

          thus for x,y,z be Vector of Z, a be Element of INT.Ring holds <;(x + y), z;> = ( <;x, z;> + <;y, z;>) & <;(a * x), y;> = (a * <;x, y;>)

          proof

            let x,y,z be Vector of Z, a be Element of INT.Ring ;

            reconsider xx = x, yy = y, zz = z as Vector of ( DivisibleMod L) by AX, ZMODUL01: 25;

            

            thus <;(x + y), z;> = (the scalar of Z . ((x + y),z))

            .= (( ScProductDM L) . ((x + y),z)) by ThSPrEM1

            .= (( ScProductDM L) . ((xx + yy),zz)) by AX2, ZMODUL01: 28

            .= ((( ScProductDM L) . (xx,zz)) + (( ScProductDM L) . (yy,zz))) by ThSPDM1

            .= ((the scalar of Z . (x,z)) + (( ScProductDM L) . (yy,zz))) by ThSPrEM1

            .= ((the scalar of Z . (x,z)) + (the scalar of Z . (y,z))) by ThSPrEM1

            .= ( <;x, z;> + <;y, z;>);

            

            thus <;(a * x), y;> = (the scalar of Z . ((a * x),y))

            .= (( ScProductDM L) . ((a * x),y)) by ThSPrEM1

            .= (( ScProductDM L) . ((a * xx),y)) by AX2, ZMODUL01: 29

            .= (a * (( ScProductDM L) . (xx,yy))) by ThSPDM1

            .= (a * (the scalar of Z . (x,y))) by ThSPrEM1

            .= (a * <;x, y;>);

          end;

        end;

        then

        reconsider Z as strict Z_Lattice by AZ;

        take Z;

        thus thesis by ZMODUL08:def 6;

      end;

      uniqueness ;

    end

    registration

      let L be non trivial Z_Lattice;

      cluster ( EMLat L) -> non trivial;

      correctness

      proof

        consider T be linear-transformation of L, ( EMbedding L) such that

         A1: T is bijective & T = ( MorphsZQ L) & (for v be Vector of L holds (T . v) = ( Class (( EQRZM L), [v, 1]))) by ZMODUL08: 21;

        set v = the non zero Vector of L;

        (T . v) in the carrier of ( EMbedding L);

        then

         A2: (T . v) in ( rng ( MorphsZQ L)) by ZMODUL08:def 3;

        (T . v) <> ( 0. ( EMbedding L))

        proof

          assume (T . v) = ( 0. ( EMbedding L));

          then (T . v) = (T . ( 0. L)) by ZMODUL05: 19;

          hence contradiction by A1, FUNCT_2: 19;

        end;

        then (T . v) <> ( zeroCoset L) by ZMODUL08:def 3;

        then (T . v) <> ( 0. ( EMLat L)) by defEMLat;

        then not (T . v) in ( (0). ( EMLat L)) by ZMODUL02: 66;

        then ( (Omega). ( EMLat L)) <> ( (0). ( EMLat L)) by A2, defEMLat;

        hence thesis by ZMODUL07: 41;

      end;

    end

    registration

      let L be non trivial Z_Lattice, r be non zero Element of F_Rat ;

      cluster ( EMLat (r,L)) -> non trivial;

      correctness

      proof

        consider T be linear-transformation of ( EMbedding L), ( EMbedding (r,L)) such that

         A1: (for v be Element of ( Z_MQ_VectSp L) st v in ( EMbedding L) holds (T . v) = (r * v)) & T is bijective by ZMODUL08: 27;

        set v = the non zero Vector of ( EMbedding L);

        (T . v) in the carrier of ( EMbedding (r,L));

        then

         A2: (T . v) in (r * ( rng ( MorphsZQ L))) by ZMODUL08:def 6;

        (T . v) <> ( 0. ( EMbedding (r,L)))

        proof

          assume (T . v) = ( 0. ( EMbedding (r,L)));

          then (T . v) = (T . ( 0. ( EMbedding L))) by ZMODUL05: 19;

          hence contradiction by A1, FUNCT_2: 19;

        end;

        then (T . v) <> ( zeroCoset L) by ZMODUL08:def 6;

        then (T . v) <> ( 0. ( EMLat (r,L))) by defrEMLat;

        then not (T . v) in ( (0). ( EMLat (r,L))) by ZMODUL02: 66;

        then ( (Omega). ( EMLat (r,L))) <> ( (0). ( EMLat (r,L))) by A2, defrEMLat;

        hence thesis by ZMODUL07: 41;

      end;

    end

    registration

      let L be INTegral Z_Lattice;

      cluster ( EMLat L) -> INTegral;

      correctness

      proof

        set Z = ( EMLat L);

        for v,u be Vector of Z holds <;v, u;> in INT

        proof

          let v,u be Vector of Z;

          v in the carrier of Z;

          then v in ( rng ( MorphsZQ L)) by defEMLat;

          then

           B3: v is Vector of ( EMbedding L) by ZMODUL08:def 3;

          then

          consider vv be Vector of L such that

           B1: (( MorphsZQ L) . vv) = v by ZMODUL08: 22;

          u in the carrier of Z;

          then u in ( rng ( MorphsZQ L)) by defEMLat;

          then

           B4: u is Vector of ( EMbedding L) by ZMODUL08:def 3;

          then

          consider uu be Vector of L such that

           B2: (( MorphsZQ L) . uu) = u by ZMODUL08: 22;

           <;v, u;> = (( ScProductEM L) . (v,u)) by defEMLat

          .= <;vv, uu;> by B1, B2, B3, B4, defScProductEM;

          hence thesis by ZMODLAT1:def 5;

        end;

        hence thesis;

      end;

    end

    theorem :: ZMODLAT2:20

    

     ThDivisibleL1: for L be Z_Lattice holds ( EMLat L) is Submodule of ( DivisibleMod L)

    proof

      let L be Z_Lattice;

      

       A1: the carrier of ( EMbedding L) = ( rng ( MorphsZQ L)) by ZMODUL08:def 3

      .= the carrier of ( EMLat L) by defEMLat;

      

       A2: the addF of ( EMLat L) = (( addCoset L) || ( rng ( MorphsZQ L))) by defEMLat

      .= the addF of ( EMbedding L) by ZMODUL08:def 3;

      then

      reconsider ad = the addF of ( EMbedding L) as BinOp of the carrier of ( EMLat L);

      

       A3: ( 0. ( EMbedding L)) = ( zeroCoset L) by ZMODUL08:def 3

      .= ( 0. ( EMLat L)) by defEMLat;

      then

      reconsider ze = ( 0. ( EMbedding L)) as Vector of ( EMLat L);

      

       A4: the lmult of ( EMLat L) = (( lmultCoset L) | [:the carrier of INT.Ring , ( rng ( MorphsZQ L)):]) by defEMLat

      .= the lmult of ( EMbedding L) by ZMODUL08:def 3;

      then

      reconsider mu = the lmult of ( EMbedding L) as Function of [:the carrier of INT.Ring , the carrier of ( EMLat L):], the carrier of ( EMLat L);

      reconsider sc = the scalar of ( EMLat L) as Function of [:the carrier of ( EMbedding L), the carrier of ( EMbedding L):], the carrier of F_Real by A1;

      ( EMLat L) = ( GenLat (( EMbedding L),sc)) by A1, A2, A3, A4;

      then

       A2: ( EMLat L) is Submodule of ( EMbedding L) by ZMODLAT1: 2;

      ( EMbedding L) is Submodule of ( DivisibleMod L) by ZMODUL08: 24;

      hence thesis by A2, ZMODUL01: 42;

    end;

    theorem :: ZMODLAT2:21

    

     ThDivisibleL2: for L be Z_Lattice, r be Element of F_Rat holds ( EMLat (r,L)) is Submodule of ( DivisibleMod L)

    proof

      let L be Z_Lattice, r be Element of F_Rat ;

      

       A1: the carrier of ( EMbedding (r,L)) = (r * ( rng ( MorphsZQ L))) by ZMODUL08:def 6

      .= the carrier of ( EMLat (r,L)) by defrEMLat;

      

       A2: the addF of ( EMLat (r,L)) = (( addCoset L) || (r * ( rng ( MorphsZQ L)))) by defrEMLat

      .= the addF of ( EMbedding (r,L)) by ZMODUL08:def 6;

      then

      reconsider ad = the addF of ( EMbedding (r,L)) as BinOp of the carrier of ( EMLat (r,L));

      

       A3: ( 0. ( EMbedding (r,L))) = ( zeroCoset L) by ZMODUL08:def 6

      .= ( 0. ( EMLat (r,L))) by defrEMLat;

      then

      reconsider ze = ( 0. ( EMbedding (r,L))) as Vector of ( EMLat (r,L));

      

       A4: the lmult of ( EMLat (r,L)) = (( lmultCoset L) | [:the carrier of INT.Ring , (r * ( rng ( MorphsZQ L))):]) by defrEMLat

      .= the lmult of ( EMbedding (r,L)) by ZMODUL08:def 6;

      then

      reconsider mu = the lmult of ( EMbedding (r,L)) as Function of [:the carrier of INT.Ring , the carrier of ( EMLat (r,L)):], the carrier of ( EMLat (r,L));

      reconsider sc = the scalar of ( EMLat (r,L)) as Function of [:the carrier of ( EMbedding (r,L)), the carrier of ( EMbedding (r,L)):], the carrier of F_Real by A1;

      ( EMLat (r,L)) = ( GenLat (( EMbedding (r,L)),sc)) by A1, A2, A3, A4;

      then

       A2: ( EMLat (r,L)) is Submodule of ( EMbedding (r,L)) by ZMODLAT1: 2;

      ( EMbedding (r,L)) is Submodule of ( DivisibleMod L) by ZMODUL08: 32;

      hence thesis by A2, ZMODUL01: 42;

    end;

    theorem :: ZMODLAT2:22

    

     ThrEMLat1: for L be Z_Lattice, r be non zero Element of F_Rat , m,n be Element of INT.Ring , m1,n1 be Element of INT , v be Vector of ( EMLat (r,L)) st m = m1 & n = n1 & r = (m1 / n1) & n1 <> 0 holds ex x be Vector of ( EMLat L) st (n * v) = (m * x)

    proof

      let L be Z_Lattice, r be non zero Element of F_Rat , m,n be Element of INT.Ring , m1,n1 be Element of INT , v be Vector of ( EMLat (r,L)) such that

       A1: m = m1 & n = n1 & r = (m1 / n1) & n1 <> 0 ;

      consider T be linear-transformation of ( EMbedding L), ( EMbedding (r,L)) such that

       A2: (for u be Element of ( Z_MQ_VectSp L) st u in ( EMbedding L) holds (T . u) = (r * u)) & T is bijective by ZMODUL08: 27;

      v in the carrier of ( EMLat (r,L));

      then v in (r * ( rng ( MorphsZQ L))) by defrEMLat;

      then v in the carrier of ( EMbedding (r,L)) by ZMODUL08:def 6;

      then v in ( rng T) by A2, FUNCT_2:def 3;

      then

      consider ve be object such that

       A3: ve in the carrier of ( EMbedding L) & v = (T . ve) by FUNCT_2: 11;

      reconsider vz = ve as Vector of ( Z_MQ_VectSp L) by A3, ZMODUL08: 19;

      reconsider vd = vz as Vector of ( DivisibleMod L) by ZMODUL08: 30;

      consider zvd be Vector of ( DivisibleMod L) such that

       A4: vd = (n * zvd) & (r * vz) = (m * zvd) by A1, ZMODUL08: 31;

      

       A5: vz in ( EMbedding L) by A3;

      vz in ( rng ( MorphsZQ L)) by A3, ZMODUL08:def 3;

      then

      reconsider x = vz as Vector of ( EMLat L) by defEMLat;

      

       B1: ( EMLat L) is Submodule of ( DivisibleMod L) by ThDivisibleL1;

      

       B2: ( EMLat (r,L)) is Submodule of ( DivisibleMod L) by ThDivisibleL2;

      

       A7: (m * x) = (m * vd) by B1, ZMODUL01: 29

      .= ((m * n) * zvd) by A4, VECTSP_1:def 16

      .= (n * (m * zvd)) by VECTSP_1:def 16

      .= (n * v) by A2, A3, A4, A5, B2, ZMODUL01: 29;

      take x;

      thus thesis by A7;

    end;

    theorem :: ZMODLAT2:23

    

     ThrEMLat2: for L be Z_Lattice, r be Element of F_Rat , v,u be Vector of ( EMLat (r,L)), x,y be Vector of ( EMLat L) st v = x & u = y holds <;v, u;> = <;x, y;>

    proof

      let L be Z_Lattice, r be Element of F_Rat , v,u be Vector of ( EMLat (r,L)), x,y be Vector of ( EMLat L) such that

       A1: v = x & u = y;

      v in the carrier of ( EMLat L) & u in the carrier of ( EMLat L) by A1;

      then

       A2: v in ( rng ( MorphsZQ L)) & u in ( rng ( MorphsZQ L)) by defEMLat;

      v in the carrier of ( EMLat (r,L)) & u in the carrier of ( EMLat (r,L));

      then v in (r * ( rng ( MorphsZQ L))) & u in (r * ( rng ( MorphsZQ L))) by defrEMLat;

      then

       A3: v is Vector of ( EMbedding (r,L)) & u is Vector of ( EMbedding (r,L)) by ZMODUL08:def 6;

      

      thus <;v, u;> = ((( ScProductDM L) || (r * ( rng ( MorphsZQ L)))) . (v,u)) by defrEMLat

      .= ((( ScProductDM L) || the carrier of ( EMbedding (r,L))) . (v,u)) by ZMODUL08:def 6

      .= (( ScProductDM L) . (v,u)) by A3, ThSPrEM1

      .= ((( ScProductDM L) || ( rng ( MorphsZQ L))) . (v,u)) by A2, FUNCT_1: 49, ZFMISC_1: 87

      .= (( ScProductEM L) . (x,y)) by A1, ThSPEM2

      .= <;x, y;> by defEMLat;

    end;

    theorem :: ZMODLAT2:24

    for L be INTegral Z_Lattice, r be non zero Element of F_Rat , a be Rational, v,u be Vector of ( EMLat (r,L)) st r = a holds (((a " ) * (a " )) * <;v, u;>) in INT

    proof

      let L be INTegral Z_Lattice, r be non zero Element of F_Rat , a be Rational, v,u be Vector of ( EMLat (r,L)) such that

       A1: r = a;

      consider m0,n0 be Integer such that

       A2: n0 <> 0 & a = (m0 / n0) by RAT_1: 2;

      reconsider n = n0, m = m0 as Element of INT.Ring by INT_1:def 2;

      consider vv be Vector of ( EMLat L) such that

       A3: (n * v) = (m * vv) by A1, A2, ThrEMLat1;

      consider uu be Vector of ( EMLat L) such that

       A4: (n * u) = (m * uu) by A1, A2, ThrEMLat1;

      r <> ( 0. F_Rat );

      then

       A5: m <> 0 by A1, A2;

      

       A6: ((n * n) * <;v, u;>) = (n * (n * <;v, u;>))

      .= (n * <;v, (n * u);>) by ZMODLAT1: 9

      .= <;(n * v), (n * u);> by ZMODLAT1:def 3

      .= <;(m * vv), (m * uu);> by A3, A4, ThrEMLat2

      .= (m * <;vv, (m * uu);>) by ZMODLAT1:def 3

      .= (m * (m * <;vv, uu;>)) by ZMODLAT1: 9

      .= ((m * m) * <;vv, uu;>);

      

       A7: (((1 / m0) * (1 / m0)) * ((n0 * n0) * <;v, u;>)) = (((n0 / m0) * (n0 / m0)) * <;v, u;>)

      .= (((a " ) * (n0 / m0)) * <;v, u;>) by A2, XCMPLX_1: 213

      .= (((a " ) * (a " )) * <;v, u;>) by A2, XCMPLX_1: 213;

      (((1 / m0) * (1 / m0)) * ((m0 * m0) * <;vv, uu;>)) = ((m0 * (1 / m0)) * ((m0 * (1 / m0)) * <;vv, uu;>))

      .= (1 * ((m0 * (1 / m0)) * <;vv, uu;>)) by A5, XCMPLX_1: 106

      .= (( 1. F_Real ) * <;vv, uu;>) by A5, XCMPLX_1: 106

      .= <;vv, uu;>;

      hence thesis by A6, A7, ZMODLAT1:def 5;

    end;

    registration

      let L be positive-definite Z_Lattice;

      cluster ( EMLat L) -> positive-definite;

      correctness

      proof

        set Z = ( EMLat L);

        for v be Vector of Z st v <> ( 0. Z) holds ||.v.|| > 0

        proof

          let v be Vector of Z such that

           AS: v <> ( 0. Z);

          v in the carrier of Z;

          then v in ( rng ( MorphsZQ L)) by defEMLat;

          then

           B1: v is Vector of ( EMbedding L) by ZMODUL08:def 3;

          then

          consider vv be Vector of L such that

           B2: (( MorphsZQ L) . vv) = v by ZMODUL08: 22;

          

           B3: vv <> ( 0. L)

          proof

            assume vv = ( 0. L);

            

            then v = ( 0. ( Z_MQ_VectSp L)) by B2, ZMODUL04:def 6

            .= ( 0. ( EMbedding L)) by ZMODUL08: 19

            .= ( zeroCoset L) by ZMODUL08:def 3

            .= ( 0. Z) by defEMLat;

            hence contradiction by AS;

          end;

           ||.v.|| = (( ScProductEM L) . (v,v)) by defEMLat

          .= ||.vv.|| by B1, B2, defScProductEM;

          hence thesis by B3, ZMODLAT1:def 6;

        end;

        hence thesis;

      end;

    end

    registration

      let L be positive-definite Z_Lattice;

      let r be non zero Element of F_Rat ;

      cluster ( EMLat (r,L)) -> positive-definite;

      correctness

      proof

        set Z = ( EMLat (r,L));

        consider rm0,rn0 be Integer such that

         A1: rn0 <> 0 & r = (rm0 / rn0) by RAT_1: 1;

        

         a1: rn0 <> ( 0. INT.Ring ) by A1;

        reconsider rn = rn0, rm = rm0 as Element of INT.Ring by INT_1:def 2;

         INT c= the carrier of F_Real by NUMBERS: 5;

        then

        reconsider rnf = rn, rmf = rm as Element of F_Real ;

        for v be Vector of Z st v <> ( 0. Z) holds ||.v.|| > 0

        proof

          let v be Vector of Z such that

           B1: v <> ( 0. Z);

          consider T be linear-transformation of ( EMbedding L), ( EMbedding (r,L)) such that

           B2: (for v be Vector of ( Z_MQ_VectSp L) st v in ( EMbedding L) holds (T . v) = (r * v)) & T is bijective by ZMODUL08: 27;

          v in the carrier of Z;

          then

           B0: v in (r * ( rng ( MorphsZQ L))) by defrEMLat;

          then v in the carrier of ( EMbedding (r,L)) by ZMODUL08:def 6;

          then v in ( rng T) by B2, FUNCT_2:def 3;

          then

          consider ve be object such that

           B3: ve in the carrier of ( EMbedding L) & v = (T . ve) by FUNCT_2: 11;

          reconsider vz = ve as Vector of ( Z_MQ_VectSp L) by B3, ZMODUL08: 19;

          reconsider vd = vz as Vector of ( DivisibleMod L) by ZMODUL08: 30;

          consider zvd be Vector of ( DivisibleMod L) such that

           B4: vd = (rn * zvd) & (r * vz) = (rm * zvd) by A1, ZMODUL08: 31;

          

           BX: vz in ( EMbedding L) by B3;

          

           B5: v = (rm * zvd) by B2, B3, B4, BX;

          

           B6: v is Vector of ( EMbedding (r,L)) by B0, ZMODUL08:def 6;

          reconsider vd as Vector of ( EMbedding L) by B3;

          

           B8: ||.v.|| = ((( ScProductDM L) || (r * ( rng ( MorphsZQ L)))) . (v,v)) by defrEMLat

          .= ((( ScProductDM L) || the carrier of ( EMbedding (r,L))) . (v,v)) by ZMODUL08:def 6

          .= (( ScProductDM L) . (v,v)) by B6, ThSPrEM1

          .= (rm0 * (( ScProductDM L) . (zvd,(rm * zvd)))) by B5, ThSPDM1

          .= (rm0 * (( ScProductDM L) . ((rm * zvd),zvd))) by ThSPDM1

          .= (rm0 * (rm0 * (( ScProductDM L) . (zvd,zvd)))) by ThSPDM1

          .= ((rm0 * rm0) * (( ScProductDM L) . (zvd,zvd)))

          .= ((rmf * rmf) * (((rnf " ) * (rnf " )) * (( ScProductEM L) . (vd,vd)))) by A1, B4, defScProductDM

          .= (((rmf * rmf) * ((rnf " ) * (rnf " ))) * (( ScProductEM L) . (vd,vd)));

          

           BY: rnf <> ( 0. F_Real ) by A1;

          rm0 <> 0

          proof

            assume rm0 = 0 ;

            then r = ( 0. F_Rat ) by A1;

            hence contradiction;

          end;

          then rmf <> 0 & (rnf " ) <> 0 by BY, VECTSP_1: 25;

          then

           B9: (rmf * rmf) > 0 & ((rnf " ) * (rnf " )) > 0 by XREAL_1: 63;

          vd in the carrier of ( EMbedding L);

          then vd in ( rng ( MorphsZQ L)) by ZMODUL08:def 3;

          then

          reconsider vl = vd as Vector of ( EMLat L) by defEMLat;

          vd <> ( 0. ( EMbedding L))

          proof

            assume

             C1: vd = ( 0. ( EMbedding L));

            (rn * zvd) = ( zeroCoset L) by B4, C1, ZMODUL08:def 3

            .= ( 0. ( DivisibleMod L)) by ZMODUL08:def 4;

            then zvd = ( 0. ( DivisibleMod L)) by ZMODUL01:def 7, a1;

            

            then v = ( 0. ( DivisibleMod L)) by B5, ZMODUL01: 1

            .= ( zeroCoset L) by ZMODUL08:def 4

            .= ( 0. Z) by defrEMLat;

            hence contradiction by B1;

          end;

          then vd <> ( zeroCoset L) by ZMODUL08:def 3;

          then

           B10: vd <> ( 0. ( EMLat L)) by defEMLat;

          (( ScProductEM L) . (vd,vd)) = ||.vl.|| by defEMLat;

          then (( ScProductEM L) . (vd,vd)) > 0 by B10, ZMODLAT1:def 6;

          hence thesis by B8, B9;

        end;

        hence thesis;

      end;

    end

    theorem :: ZMODLAT2:25

    

     ThSPDM2: for L be positive-definite Z_Lattice, v be Vector of ( DivisibleMod L) holds (( ScProductDM L) . (v,v)) = 0 iff v = ( 0. ( DivisibleMod L))

    proof

      let L be positive-definite Z_Lattice, v be Vector of ( DivisibleMod L);

      consider a be Element of INT.Ring such that

       A1: a <> 0 & (a * v) in ( EMbedding L) by ZMODUL08: 29;

      

       a1: a <> ( 0. INT.Ring ) by A1;

      reconsider u = (a * v) as Vector of ( EMbedding L) by A1;

      u in the carrier of ( EMbedding L);

      then u in ( rng ( MorphsZQ L)) by ZMODUL08:def 3;

      then

      reconsider ul = u as Vector of ( EMLat L) by defEMLat;

      

       A2: ((a * a) * (( ScProductDM L) . (v,v))) = (a * (a * (( ScProductDM L) . (v,v))))

      .= (a * (( ScProductDM L) . ((a * v),v))) by ThSPDM1

      .= (a * (( ScProductDM L) . (v,(a * v)))) by ThSPDM1

      .= (( ScProductDM L) . ((a * v),(a * v))) by ThSPDM1;

      ( ScProductEM L) = (( ScProductDM L) || ( rng ( MorphsZQ L))) by ThSPEM2

      .= (( ScProductDM L) || the carrier of ( EMbedding L)) by ZMODUL08:def 3;

      

      then

       A4: (( ScProductDM L) . ((a * v),(a * v))) = (( ScProductEM L) . (u,u)) by FUNCT_1: 49, ZFMISC_1: 87

      .= ||.ul.|| by defEMLat;

      hereby

        assume

         B1: (( ScProductDM L) . (v,v)) = 0 ;

        assume v <> ( 0. ( DivisibleMod L));

        then (a * v) <> ( 0. ( DivisibleMod L)) by a1, ZMODUL01:def 7;

        then u <> ( zeroCoset L) by ZMODUL08:def 4;

        then ul <> ( 0. ( EMLat L)) by defEMLat;

        hence contradiction by A2, A4, B1, ZMODLAT1: 16;

      end;

      assume v = ( 0. ( DivisibleMod L));

      

      then u = ( 0. ( DivisibleMod L)) by ZMODUL01: 1

      .= ( zeroCoset L) by ZMODUL08:def 4

      .= ( 0. ( EMLat L)) by defEMLat;

      hence thesis by A1, A2, A4, ZMODLAT1: 16;

    end;

    theorem :: ZMODLAT2:26

    

     ThSLX2: for L be positive-definite Z_Lattice, Z be non empty LatticeStr over INT.Ring st Z is Submodule of ( DivisibleMod L) & the scalar of Z = (( ScProductDM L) || the carrier of Z) holds Z is Z_Lattice-like

    proof

      let L be positive-definite Z_Lattice, Z be non empty LatticeStr over INT.Ring such that

       A1: Z is Submodule of ( DivisibleMod L) & the scalar of Z = (( ScProductDM L) || the carrier of Z);

      set A = the carrier of Z;

      

       A2: for x,y be Vector of Z holds (the scalar of Z . (x,y)) = (( ScProductDM L) . (x,y))

      proof

        let x,y be Vector of Z;

         [x, y] in [:A, A:];

        hence (the scalar of Z . (x,y)) = (( ScProductDM L) . (x,y)) by A1, FUNCT_1: 49;

      end;

      Z is Z_Lattice-like

      proof

        thus for x be Vector of Z st for y be Vector of Z holds <;x, y;> = 0 holds x = ( 0. Z)

        proof

          let x be Vector of Z such that

           B1: for y be Vector of Z holds <;x, y;> = 0 ;

          

           B2: x is Vector of ( DivisibleMod L) by A1, ZMODUL01: 25;

          assume x <> ( 0. Z);

          then x <> ( 0. ( DivisibleMod L)) by A1, ZMODUL01: 26;

          then (( ScProductDM L) . (x,x)) <> 0 by B2, ThSPDM2;

          then (the scalar of Z . (x,x)) <> 0 by A2;

          then <;x, x;> <> 0 ;

          hence contradiction by B1;

        end;

        thus for x,y be Vector of Z holds <;x, y;> = <;y, x;>

        proof

          let x,y be Vector of Z;

          reconsider xx = x, yy = y as Vector of ( DivisibleMod L) by A1, ZMODUL01: 25;

          

          thus <;x, y;> = (the scalar of Z . (x,y))

          .= (( ScProductDM L) . (x,y)) by A2

          .= (( ScProductDM L) . (yy,xx)) by ThSPDM1

          .= (the scalar of Z . (y,x)) by A2

          .= <;y, x;>;

        end;

        thus for x,y,z be Vector of Z, a be Element of INT.Ring holds <;(x + y), z;> = ( <;x, z;> + <;y, z;>) & <;(a * x), y;> = (a * <;x, y;>)

        proof

          let x,y,z be Vector of Z, a be Element of INT.Ring ;

          reconsider xx = x, yy = y, zz = z as Vector of ( DivisibleMod L) by A1, ZMODUL01: 25;

          

           B1: (xx + yy) = (x + y) by A1, ZMODUL01: 28;

          

          thus <;(x + y), z;> = (the scalar of Z . ((x + y),z))

          .= (( ScProductDM L) . ((xx + yy),zz)) by A2, B1

          .= ((( ScProductDM L) . (xx,zz)) + (( ScProductDM L) . (yy,zz))) by ThSPDM1

          .= ((the scalar of Z . (x,z)) + (( ScProductDM L) . (y,z))) by A2

          .= ((the scalar of Z . (x,z)) + (the scalar of Z . (y,z))) by A2

          .= ( <;x, z;> + <;y, z;>);

          

           B2: (a * xx) = (a * x) by A1, ZMODUL01: 29;

          

          thus <;(a * x), y;> = (the scalar of Z . ((a * x),y))

          .= (( ScProductDM L) . ((a * xx),yy)) by A2, B2

          .= (a * (( ScProductDM L) . (xx,yy))) by ThSPDM1

          .= (a * (the scalar of Z . (x,y))) by A2

          .= (a * <;x, y;>);

        end;

      end;

      hence thesis;

    end;

    theorem :: ZMODLAT2:27

    for L be positive-definite Z_Lattice, Z be non empty LatticeStr over INT.Ring st Z is finitely-generated Submodule of ( DivisibleMod L) & the scalar of Z = (( ScProductDM L) || the carrier of Z) holds Z is Z_Lattice by ThSLX2;

    theorem :: ZMODLAT2:28

    

     LmEMDetX0: for L be Z_Lattice holds the ModuleStr of ( EMLat L) = ( EMbedding L)

    proof

      let L be Z_Lattice;

      

       Q1: the carrier of ( EMLat L) = ( rng ( MorphsZQ L)) by defEMLat

      .= the carrier of ( EMbedding L) by ZMODUL08:def 3;

      

       Q2: the ZeroF of ( EMLat L) = ( zeroCoset L) by defEMLat

      .= the ZeroF of ( EMbedding L) by ZMODUL08:def 3;

      

       Q3: the addF of ( EMLat L) = (( addCoset L) || ( rng ( MorphsZQ L))) by defEMLat

      .= the addF of ( EMbedding L) by ZMODUL08:def 3;

      

       Q4: the lmult of ( EMLat L) = (( lmultCoset L) | [:the carrier of INT.Ring , ( rng ( MorphsZQ L)):]) by defEMLat

      .= the lmult of ( EMbedding L) by ZMODUL08:def 3;

      thus the ModuleStr of ( EMLat L) = ( EMbedding L) by Q1, Q2, Q3, Q4;

    end;

    theorem :: ZMODLAT2:29

    

     LmEMDetX53: for L,E be Z_Module st the ModuleStr of L = the ModuleStr of E holds L is Submodule of E

    proof

      let L,E be Z_Module;

      assume

       AS: the ModuleStr of L = the ModuleStr of E;

      

       P2: ( 0. L) = ( 0. E) by AS;

      

       P3: the addF of L = (the addF of E || the carrier of L) by AS;

      the lmult of L = (the lmult of E | [:the carrier of INT.Ring , the carrier of L:] qua set) by AS;

      hence thesis by AS, P2, P3, VECTSP_4:def 2;

    end;

    theorem :: ZMODLAT2:30

    

     LmEMDetX541: for E,L be Z_Module, I be Subset of L, J be Subset of E, K be Linear_Combination of J st I = J & the ModuleStr of L = the ModuleStr of E holds K is Linear_Combination of I

    proof

      let E,L be Z_Module, I be Subset of L, J be Subset of E, K be Linear_Combination of J;

      assume that

       AS1: I = J and

       AS2: the ModuleStr of L = the ModuleStr of E;

      

       P1: K is Linear_Combination of E & ( Carrier K) c= J by VECTSP_6:def 4;

      consider T be finite Subset of E such that

       P4: for v be Element of E st not v in T holds (K . v) = ( 0. INT.Ring ) by VECTSP_6:def 1;

      reconsider S = T as finite Subset of L by AS2;

      reconsider H = K as Linear_Combination of L by AS2, P4, VECTSP_6:def 1;

      ( Carrier H) c= I by P1, AS1, AS2;

      hence thesis by VECTSP_6:def 4;

    end;

    theorem :: ZMODLAT2:31

    for E,L be Z_Module, K be Linear_Combination of E, H be Linear_Combination of L st K = H & the ModuleStr of L = the ModuleStr of E holds ( Carrier K) = ( Carrier H);

    theorem :: ZMODLAT2:32

    

     LmEMDetX543: for E,L be Z_Module, K be Linear_Combination of E, H be Linear_Combination of L st K = H & the ModuleStr of L = the ModuleStr of E holds ( Sum K) = ( Sum H)

    proof

      let E,L be Z_Module, K be Linear_Combination of E, H be Linear_Combination of L;

      assume

       AS: K = H & the ModuleStr of L = the ModuleStr of E;

      

       B3: L is Submodule of E by AS, LmEMDetX53;

      

       B4: ( Carrier K) c= the carrier of L by AS;

      H = (K | the carrier of L) by AS;

      hence ( Sum K) = ( Sum H) by ZMODUL03: 11, B3, B4;

    end;

    theorem :: ZMODLAT2:33

    

     LmEMDetX51: for L,E be Z_Module, I be Subset of L, J be Subset of E st the ModuleStr of L = the ModuleStr of E & I = J holds (I is linearly-independent iff J is linearly-independent)

    proof

      for E,L be Z_Module, I be Subset of L, J be Subset of E st I = J & the ModuleStr of L = the ModuleStr of E & I is linearly-independent holds J is linearly-independent

      proof

        let E,L be Z_Module, I be Subset of L, J be Subset of E;

        assume that

         A1: I = J and

         A3: the ModuleStr of L = the ModuleStr of E and

         A2: I is linearly-independent;

        for K be Linear_Combination of J st ( Sum K) = ( 0. E) holds ( Carrier K) = {}

        proof

          let K be Linear_Combination of J;

          assume

           P0: ( Sum K) = ( 0. E);

          reconsider H = K as Linear_Combination of I by A1, A3, LmEMDetX541;

          

           P1: ( Carrier K) = ( Carrier H) by A3;

          ( Sum H) = ( 0. L) by A3, P0, LmEMDetX543;

          hence thesis by A2, P1, VECTSP_7:def 1;

        end;

        hence thesis by VECTSP_7:def 1;

      end;

      hence thesis;

    end;

    theorem :: ZMODLAT2:34

    

     LmEMDetX52: for L,E be Z_Module, I be Subset of L, J be Subset of E st the ModuleStr of L = the ModuleStr of E & I = J holds ( Lin I) = ( Lin J)

    proof

      let L,E be Z_Module, I be Subset of L, J be Subset of E;

      assume that

       A1: the ModuleStr of L = the ModuleStr of E and

       A2: I = J;

      L is Submodule of E by A1, LmEMDetX53;

      hence ( Lin I) = ( Lin J) by A2, ZMODUL03: 20;

    end;

    theorem :: ZMODLAT2:35

    

     LmEMDetX5: for L,E be free Z_Module, I be Subset of L, J be Subset of E st the ModuleStr of L = the ModuleStr of E & I = J holds (I is Basis of L iff J is Basis of E)

    proof

      let L,E be free Z_Module, I be Subset of L, J be Subset of E;

      assume that

       A1: the ModuleStr of L = the ModuleStr of E and

       A2: I = J;

      hereby

        assume

         P1: I is Basis of L;

        then I is linearly-independent & ( Lin I) = ModuleStr (# the carrier of L, the addF of L, the ZeroF of L, the lmult of L #) by VECTSP_7:def 3;

        then

         P2: J is linearly-independent by A1, A2, LmEMDetX51;

        ( Lin J) = ( Lin I) by A1, A2, LmEMDetX52

        .= ModuleStr (# the carrier of E, the addF of E, the ZeroF of E, the lmult of E #) by A1, P1, VECTSP_7:def 3;

        hence J is Basis of E by P2, VECTSP_7:def 3;

      end;

      assume

       P1: J is Basis of E;

      then J is linearly-independent & ( Lin J) = ModuleStr (# the carrier of E, the addF of E, the ZeroF of E, the lmult of E #) by VECTSP_7:def 3;

      then

       P2: I is linearly-independent by A1, A2, LmEMDetX51;

      ( Lin I) = ( Lin J) by A1, A2, LmEMDetX52

      .= ModuleStr (# the carrier of L, the addF of L, the ZeroF of L, the lmult of L #) by A1, P1, VECTSP_7:def 3;

      hence I is Basis of L by P2, VECTSP_7:def 3;

    end;

    theorem :: ZMODLAT2:36

    

     LmEMDetX4: for L,E be finite-rank free Z_Module st the ModuleStr of L = the ModuleStr of E holds ( rank L) = ( rank E)

    proof

      let L,E be finite-rank free Z_Module;

      assume

       AS: the ModuleStr of L = the ModuleStr of E;

      set I = the Basis of L;

      

       P1: ( rank L) = ( card I) by ZMODUL03:def 5;

      reconsider J = I as Subset of E by AS;

      J is Basis of E by LmEMDetX5, AS;

      hence thesis by P1, ZMODUL03:def 5;

    end;

    theorem :: ZMODLAT2:37

    

     LmEMDetX6: for L be Z_Lattice, I be Subset of L holds I is Basis of L iff (( MorphsZQ L) .: I) is Basis of ( EMbedding L)

    proof

      let L be Z_Lattice, I be Subset of L;

      consider T be linear-transformation of L, ( EMbedding L) such that

       A1: T is bijective and

       A2: T = ( MorphsZQ L) and for v be Vector of L holds (T . v) = ( Class (( EQRZM L), [v, 1])) by ZMODUL08: 21;

      thus thesis by A1, A2, ZMODUL06: 49;

    end;

    theorem :: ZMODLAT2:38

    for L be Z_Lattice, I be Subset of L holds I is Basis of L iff (( MorphsZQ L) .: I) is Basis of ( EMLat L)

    proof

      let L be Z_Lattice, I be Subset of L;

      

       P1: I is Basis of L iff (( MorphsZQ L) .: I) is Basis of ( EMbedding L) by LmEMDetX6;

       the ModuleStr of ( EMLat L) = the ModuleStr of ( EMbedding L) by LmEMDetX0;

      hence thesis by P1, LmEMDetX5;

    end;

    theorem :: ZMODLAT2:39

    

     LmEMDetX8: for L be Z_Lattice, b be FinSequence of L holds b is OrdBasis of L iff (( MorphsZQ L) * b) is OrdBasis of ( EMbedding L)

    proof

      let L be Z_Lattice, b be FinSequence of L;

      

       E1: ex T be linear-transformation of L, ( EMbedding L) st T is bijective & T = ( MorphsZQ L) & (for v be Vector of L holds (T . v) = ( Class (( EQRZM L), [v, 1]))) by ZMODUL08: 21;

      

       E4: (( MorphsZQ L) * b) is FinSequence of ( EMbedding L) by E1, FINSEQ_2: 32;

      

       P3: ( rng (( MorphsZQ L) * b)) = (( MorphsZQ L) .: ( rng b)) by RELAT_1: 127;

      hereby

        assume b is OrdBasis of L;

        then

         P1: b is one-to-one & ( rng b) is Basis of L by ZMATRLIN:def 5;

        then (( MorphsZQ L) .: ( rng b)) is Basis of ( EMbedding L) by LmEMDetX6;

        hence (( MorphsZQ L) * b) is OrdBasis of ( EMbedding L) by E1, E4, P1, P3, ZMATRLIN:def 5;

      end;

      assume (( MorphsZQ L) * b) is OrdBasis of ( EMbedding L);

      then

       P1: (( MorphsZQ L) * b) is one-to-one & ( rng (( MorphsZQ L) * b)) is Basis of ( EMbedding L) by ZMATRLIN:def 5;

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

      then ( rng b) c= ( dom ( MorphsZQ L));

      then

       P2: b is one-to-one by P1, FUNCT_1: 25;

      ( rng b) is Basis of L by LmEMDetX6, P1, P3;

      hence b is OrdBasis of L by ZMATRLIN:def 5, P2;

    end;

    theorem :: ZMODLAT2:40

    

     LmEMDetX9: for L be Z_Lattice, E be finite-rank free Z_Module, I be FinSequence of L, J be FinSequence of E st the ModuleStr of L = the ModuleStr of E & I = J holds (I is OrdBasis of L iff J is OrdBasis of E)

    proof

      let L be Z_Lattice, E be finite-rank free Z_Module, I be FinSequence of L, J be FinSequence of E;

      assume that

       AS1: the ModuleStr of L = the ModuleStr of E and

       AS2: I = J;

      hereby

        assume I is OrdBasis of L;

        then

         P2: I is one-to-one & ( rng I) is Basis of L by ZMATRLIN:def 5;

        then ( rng J) is Basis of E by AS1, AS2, LmEMDetX5;

        hence J is OrdBasis of E by AS2, P2, ZMATRLIN:def 5;

      end;

      assume J is OrdBasis of E;

      then

       P2: J is one-to-one & ( rng J) is Basis of E by ZMATRLIN:def 5;

      then ( rng I) is Basis of L by AS1, AS2, LmEMDetX5;

      hence I is OrdBasis of L by AS2, P2, ZMATRLIN:def 5;

    end;

    theorem :: ZMODLAT2:41

    for L be Z_Lattice, b be FinSequence of L holds b is OrdBasis of L iff (( MorphsZQ L) * b) is OrdBasis of ( EMLat L)

    proof

      let L be Z_Lattice, b be FinSequence of L;

      

       P1: b is OrdBasis of L iff (( MorphsZQ L) * b) is OrdBasis of ( EMbedding L) by LmEMDetX8;

       the ModuleStr of ( EMLat L) = the ModuleStr of ( EMbedding L) by LmEMDetX0;

      hence thesis by P1, LmEMDetX9;

    end;

    theorem :: ZMODLAT2:42

    for L be Z_Lattice holds ( rank L) = ( rank ( EMLat L))

    proof

      let L be Z_Lattice;

      consider T be linear-transformation of L, ( EMbedding L) such that

       A1: T is bijective and T = ( MorphsZQ L) and for v be Vector of L holds (T . v) = ( Class (( EQRZM L), [v, 1])) by ZMODUL08: 21;

      

       P1: ( rank L) = ( rank ( EMbedding L)) by A1, ZMODUL06: 51;

       the ModuleStr of ( EMLat L) = ( EMbedding L) by LmEMDetX0;

      hence thesis by P1, LmEMDetX4;

    end;

    theorem :: ZMODLAT2:43

    

     ThEME1: for L be Z_Lattice, x be object holds x is Vector of ( EMLat L) iff x is Vector of ( EMbedding L)

    proof

      let L be Z_Lattice, x be object;

      hereby

        assume x is Vector of ( EMLat L);

        then x in the ModuleStr of ( EMLat L);

        hence x is Vector of ( EMbedding L) by LmEMDetX0;

      end;

      assume x is Vector of ( EMbedding L);

      then x in ( EMbedding L);

      then x in the ModuleStr of ( EMLat L) by LmEMDetX0;

      hence x is Vector of ( EMLat L);

    end;

    registration

      let L be RATional Z_Lattice;

      let v,u be Vector of ( EMLat L);

      cluster (( ScProductEM L) . (v,u)) -> rational;

      correctness

      proof

        

         A1: v is Vector of ( EMbedding L) by ThEME1;

        then

        consider vv be Vector of L such that

         A2: (( MorphsZQ L) . vv) = v by ZMODUL08: 22;

        

         A3: u is Vector of ( EMbedding L) by ThEME1;

        then

        consider uu be Vector of L such that

         A4: (( MorphsZQ L) . uu) = u by ZMODUL08: 22;

        (( ScProductEM L) . (v,u)) = <;vv, uu;> by A1, A2, A3, A4, defScProductEM;

        hence thesis;

      end;

    end

    registration

      let L be RATional Z_Lattice;

      let v,u be Vector of ( DivisibleMod L);

      cluster (( ScProductDM L) . (v,u)) -> rational;

      correctness

      proof

        consider i be Element of INT.Ring such that

         A1: i <> 0 & (i * v) in ( EMbedding L) by ZMODUL08: 29;

        consider j be Element of INT.Ring such that

         A2: j <> 0 & (j * u) in ( EMbedding L) by ZMODUL08: 29;

        reconsider iv = (i * v), ju = (j * u) as Vector of ( EMbedding L) by A1, A2;

        reconsider a = i, b = j as Element of INT ;

        reconsider a, b as Element of F_Real by XREAL_0:def 1;

        

         A3: (( ScProductDM L) . (v,u)) = (((a " ) * (b " )) * (( ScProductEM L) . (iv,ju))) by A1, A2, defScProductDM;

        

         A4: iv is Vector of ( EMLat L) & ju is Vector of ( EMLat L) by ThEME1;

        reconsider ar = a, br = b as Element of F_Rat by RAT_1:def 2;

        a <> ( 0. F_Real ) & b <> ( 0. F_Real ) by A1, A2;

        then (a " ) = (ar " ) & (b " ) = (br " ) by GAUSSINT: 14, GAUSSINT: 21;

        hence thesis by A3, A4;

      end;

    end

    begin

    definition

      let V be ModuleStr over INT.Ring ;

      let f be FrForm of V, V;

      :: ZMODLAT2:def6

      attr f is symmetric means

      : defSymForm: for v,w be Vector of V holds (f . (v,w)) = (f . (w,v));

    end

    registration

      let V be non empty ModuleStr over INT.Ring ;

      cluster ( NulFrForm (V,V)) -> symmetric;

      correctness

      proof

        set f = ( NulFrForm (V,V));

        for v,w be Vector of V holds (f . (v,w)) = (f . (w,v))

        proof

          let v,w be Vector of V;

          

          thus (f . (v,w)) = ( 0. F_Real ) by FUNCOP_1: 70

          .= (f . (w,v)) by FUNCOP_1: 70;

        end;

        hence thesis;

      end;

    end

    registration

      let V be non empty ModuleStr over INT.Ring ;

      cluster symmetric for FrForm of V, V;

      correctness

      proof

        take ( NulFrForm (V,V));

        thus thesis;

      end;

    end

    registration

      let V be non empty ModuleStr over INT.Ring ;

      cluster symmetric for bilinear-FrForm of V, V;

      correctness

      proof

        take ( NulFrForm (V,V));

        thus thesis;

      end;

    end

    registration

      let L be Z_Lattice;

      cluster ( InnerProduct L) -> symmetric;

      correctness

      proof

        set f = ( InnerProduct L);

        for v,w be Vector of L holds (f . (v,w)) = (f . (w,v))

        proof

          let v,w be Vector of L;

          

          thus (f . (v,w)) = <;v, w;>

          .= <;w, v;> by ZMODLAT1:def 3

          .= (f . (w,v));

        end;

        hence thesis;

      end;

    end

    registration

      let V be finite-rank free Z_Module;

      let f be symmetric bilinear-FrForm of V, V;

      let b be OrdBasis of V;

      cluster ( GramMatrix (f,b)) -> symmetric;

      correctness

      proof

        set M = ( GramMatrix (f,b));

        set MT = (M @ );

        for i,j be Nat st [i, j] in ( Indices M) holds (M * (i,j)) = (MT * (i,j))

        proof

          let i,j be Nat such that

           A1: [i, j] in ( Indices M);

          

           A2: [j, i] in ( Indices M) by A1, MATRIX_0: 28;

          ( Indices M) = [:( Seg ( rank V)), ( Seg ( rank V)):] by MATRIX_0: 24;

          then

           A3: i in ( Seg ( rank V)) & j in ( Seg ( rank V)) by A1, ZFMISC_1: 87;

          ( len b) = ( rank V) by ZMATRLIN: 49;

          then

           A4: i in ( dom b) & j in ( dom b) by A3, FINSEQ_1:def 3;

          

          thus (M * (i,j)) = (f . ((b /. i),(b /. j))) by A4, ZMODLAT1:def 32

          .= (f . ((b /. j),(b /. i))) by defSymForm

          .= (( BilinearM (f,b,b)) * (j,i)) by A4, ZMODLAT1:def 32

          .= (MT * (i,j)) by A2, MATRIX_0:def 6;

        end;

        then M = MT by MATRIX_0: 27;

        hence thesis by MATRIX_6:def 5;

      end;

    end

    theorem :: ZMODLAT2:44

    for L be RATional Z_Lattice, v,u be Vector of ( DivisibleMod L) holds (( ScProductDM L) . (v,u)) in F_Rat by RAT_1:def 2;

    theorem :: ZMODLAT2:45

    

     ThGM1: for L be RATional Z_Lattice, b be OrdBasis of L holds ( GramMatrix b) is Matrix of ( dim L), F_Rat

    proof

      let L be RATional Z_Lattice, b be OrdBasis of L;

      

       X1: ( len ( GramMatrix b)) = ( dim L) & ( width ( GramMatrix b)) = ( dim L) & ( Indices ( GramMatrix b)) = [:( Seg ( dim L)), ( Seg ( dim L)):] by MATRIX_0: 24;

      

       X3: ( len b) = ( dim L) by ZMATRLIN: 49;

      for i,j be Nat st [i, j] in ( Indices ( GramMatrix b)) holds (( GramMatrix b) * (i,j)) in the carrier of F_Rat

      proof

        let i,j be Nat;

        assume [i, j] in ( Indices ( GramMatrix b));

        then i in ( Seg ( dim L)) & j in ( Seg ( dim L)) by X1, ZFMISC_1: 87;

        then

         D1: i in ( dom b) & j in ( dom b) by X3, FINSEQ_1:def 3;

        (( GramMatrix b) * (i,j)) = (( InnerProduct L) . ((b /. i),(b /. j))) by D1, ZMODLAT1:def 32

        .= <;(b /. i), (b /. j);>;

        hence (( GramMatrix b) * (i,j)) in the carrier of F_Rat by defRational;

      end;

      hence ( GramMatrix b) is Matrix of ( dim L), F_Rat by ZMODLAT1: 1;

    end;

    theorem :: ZMODLAT2:46

    

     ZMATRLIN42: for F be FinSequence of F_Real , G be FinSequence of F_Rat st F = G holds ( Sum F) = ( Sum G)

    proof

      defpred P[ Nat] means for F be FinSequence of F_Real , G be FinSequence of F_Rat st ( len F) = $1 & F = G holds ( Sum F) = ( Sum G);

      

       P1: P[ 0 ]

      proof

        let F be FinSequence of F_Real , G be FinSequence of F_Rat ;

        assume

         AS1: ( len F) = 0 & F = G;

        F = ( <*> the carrier of F_Real ) by AS1;

        

        then

         X1: ( Sum F) = ( 0. F_Real ) by RLVECT_1: 43

        .= 0 ;

        G = ( <*> the carrier of F_Rat ) by AS1;

        

        then ( Sum G) = ( 0. F_Rat ) by RLVECT_1: 43

        .= 0 ;

        hence ( Sum F) = ( Sum G) by X1;

      end;

      

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

      proof

        let n be Nat;

        assume

         AS1: P[n];

        let F be FinSequence of F_Real , G be FinSequence of F_Rat ;

        assume

         AS2: ( len F) = (n + 1) & F = G;

        reconsider F0 = (F | n) as FinSequence of F_Real ;

        reconsider G0 = (G | n) as FinSequence of F_Rat ;

        (n + 1) in ( Seg (n + 1)) by FINSEQ_1: 4;

        then

         A70: (n + 1) in ( dom F) by AS2, FINSEQ_1:def 3;

        then (F . (n + 1)) in ( rng F) by FUNCT_1: 3;

        then

        reconsider af = (F . (n + 1)) as Element of F_Real ;

        (G . (n + 1)) in ( rng G) by AS2, A70, FUNCT_1: 3;

        then

        reconsider ag = (G . (n + 1)) as Element of F_Rat ;

        

         P1: ( len F0) = n by FINSEQ_1: 59, AS2, NAT_1: 11;

        ( len G0) = n by FINSEQ_1: 59, AS2, NAT_1: 11;

        then

         BP4: ( dom G0) = ( Seg n) by FINSEQ_1:def 3;

        

         A9: ( len F) = (( len F0) + 1) by AS2, FINSEQ_1: 59, NAT_1: 11;

        

         BP3: ( Sum G) = (( Sum G0) + ag) by AS2, A9, BP4, RLVECT_1: 38;

        (( Sum F0) + af) = (( Sum G0) + ag) by AS1, AS2, P1;

        hence ( Sum F) = ( Sum G) by AS2, A9, BP3, BP4, RLVECT_1: 38;

      end;

      

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

      let F be FinSequence of F_Real , G be FinSequence of F_Rat ;

      assume F = G;

      hence ( Sum F) = ( Sum G) by X1;

    end;

    theorem :: ZMODLAT2:47

    

     ZMATRLIN43: for i be Nat, j be Element of F_Real , k be Element of F_Rat st j = k holds ((( power F_Real ) . (( - ( 1_ F_Real )),i)) * j) = ((( power F_Rat ) . (( - ( 1_ F_Rat )),i)) * k)

    proof

      let i be Nat, j be Element of F_Real , k be Element of F_Rat ;

      assume

       AS: j = k;

      defpred P[ Nat] means ((( power F_Real ) . (( - ( 1_ F_Real )),$1)) * j) = ((( power F_Rat ) . (( - ( 1_ F_Rat )),$1)) * k);

      

       P1: P[ 0 ]

      proof

        ((( power F_Real ) . (( - ( 1_ F_Real )), 0 )) * j) = (( 1_ F_Real ) * j) by GROUP_1:def 7

        .= ((( power F_Rat ) . (( - ( 1_ F_Rat )), 0 )) * k) by AS, GROUP_1:def 7;

        hence thesis;

      end;

      

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

      proof

        let n be Nat;

        assume

         AS1: P[n];

        

         P3: ((( power F_Real ) . (( - ( 1_ F_Real )),(n + 1))) * j) = (((( power F_Real ) . (( - ( 1_ F_Real )),n)) * ( - ( 1_ F_Real ))) * j) by GROUP_1:def 7

        .= (( - ( 1_ F_Real )) * ((( power F_Real ) . (( - ( 1_ F_Real )),n)) * j));

        ((( power F_Rat ) . (( - ( 1_ F_Rat )),(n + 1))) * k) = (((( power F_Rat ) . (( - ( 1_ F_Rat )),n)) * ( - ( 1_ F_Rat ))) * k) by GROUP_1:def 7

        .= (( - ( 1_ F_Rat )) * ((( power F_Rat ) . (( - ( 1_ F_Rat )),n)) * k));

        hence ((( power F_Real ) . (( - ( 1_ F_Real )),(n + 1))) * j) = ((( power F_Rat ) . (( - ( 1_ F_Rat )),(n + 1))) * k) by AS1, P3;

      end;

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

      hence thesis;

    end;

    theorem :: ZMODLAT2:48

    

     LmSign1C: for F be FinSequence of F_Real st for i be Nat st i in ( dom F) holds (F . i) in F_Rat holds ( Sum F) in F_Rat

    proof

      defpred P[ Nat] means for F be FinSequence of F_Real st ( len F) = $1 & for i be Nat st i in ( dom F) holds (F . i) in F_Rat holds ( Sum F) in F_Rat ;

      

       P1: P[ 0 ]

      proof

        let F be FinSequence of F_Real ;

        assume

         AS1: ( len F) = 0 & for i be Nat st i in ( dom F) holds (F . i) in F_Rat ;

        F = ( <*> the carrier of F_Real ) by AS1;

        

        then ( Sum F) = ( 0. F_Real ) by RLVECT_1: 43

        .= 0 ;

        hence ( Sum F) in F_Rat ;

      end;

      

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

      proof

        let n be Nat;

        assume

         AS1: P[n];

        let F be FinSequence of F_Real ;

        assume

         AS2: ( len F) = (n + 1) & for i be Nat st i in ( dom F) holds (F . i) in F_Rat ;

        reconsider F0 = (F | n) as FinSequence of F_Real ;

        (n + 1) in ( Seg (n + 1)) by FINSEQ_1: 4;

        then

         A70: (n + 1) in ( dom F) by AS2, FINSEQ_1:def 3;

        then (F . (n + 1)) in ( rng F) by FUNCT_1: 3;

        then

        reconsider af = (F . (n + 1)) as Element of F_Real ;

        

         P1: ( len F0) = n by FINSEQ_1: 59, AS2, NAT_1: 11;

        then

         P4: ( dom F0) = ( Seg n) by FINSEQ_1:def 3;

        ( len F) = (( len F0) + 1) by AS2, FINSEQ_1: 59, NAT_1: 11;

        then

         P3: ( Sum F) = (( Sum F0) + af) by AS2, P4, RLVECT_1: 38;

        for i be Nat st i in ( dom F0) holds (F0 . i) in F_Rat

        proof

          let i be Nat;

          assume

           P40: i in ( dom F0);

          ( dom F) = ( Seg (n + 1)) by AS2, FINSEQ_1:def 3;

          then ( dom F0) c= ( dom F) by P4, FINSEQ_1: 5, NAT_1: 11;

          then (F . i) in F_Rat by AS2, P40;

          hence thesis by P40, FUNCT_1: 47;

        end;

        then ( Sum F0) in F_Rat by P1, AS1;

        then

        reconsider i1 = ( Sum F0) as Element of F_Rat ;

        (F . (n + 1)) in F_Rat by A70, AS2;

        then

        reconsider i2 = af as Element of F_Rat ;

        ( Sum F) = (i1 + i2) by P3;

        hence ( Sum F) in F_Rat ;

      end;

      

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

      let F be FinSequence of F_Real ;

      assume

       X2: for i be Nat st i in ( dom F) holds (F . i) in F_Rat ;

      ( len F) is Nat;

      hence ( Sum F) in F_Rat by X1, X2;

    end;

    theorem :: ZMODLAT2:49

    

     LmSign1D: for i be Nat holds (( power F_Real ) . (( - ( 1_ F_Real )),i)) in F_Rat

    proof

      let i be Nat;

      ((( power F_Real ) . (( - ( 1_ F_Real )),i)) * ( 1. F_Real )) = ((( power F_Rat ) . (( - ( 1_ F_Rat )),i)) * ( 1. F_Rat )) by ZMATRLIN43;

      hence thesis;

    end;

    theorem :: ZMODLAT2:50

    

     LmSign1F: for n,i,j,k,m be Nat, M be Matrix of (n + 1), F_Real holds for L be Matrix of (n + 1), F_Rat st 0 < n & M = L & [i, j] in ( Indices M) & [k, m] in ( Indices ( Delete (M,i,j))) holds (( Delete (M,i,j)) * (k,m)) = (( Delete (L,i,j)) * (k,m))

    proof

      let n,i,j,k,m be Nat, M be Matrix of (n + 1), F_Real ;

      let L be Matrix of (n + 1), F_Rat ;

      assume that 0 < n and

       A2: M = L and

       A3: [i, j] in ( Indices M) and

       A4: [k, m] in ( Indices ( Delete (M,i,j)));

       [i, j] in [:( Seg (n + 1)), ( Seg (n + 1)):] by A3, MATRIX_0: 24;

      then

       A5: i in ( Seg (n + 1)) & j in ( Seg (n + 1)) by ZFMISC_1: 87;

      set M0 = ( Delete (M,i,j));

      ((n + 1) -' 1) = n by NAT_D: 34;

      then ( len M0) = n & ( width M0) = n & ( Indices M0) = [:( Seg n), ( Seg n):] by MATRIX_0: 24;

      then

       D5: k in ( Seg n) & m in ( Seg n) by A4, ZFMISC_1: 87;

      then

       D3: k in ( Seg ((n + 1) -' 1)) & m in ( Seg ((n + 1) -' 1)) by NAT_D: 34;

      

       FC0: 1 <= k & k <= n & 1 <= m & m <= n by FINSEQ_1: 1, D5;

      then 1 <= k & (k + 0 ) <= (n + 1) & 1 <= m & (m + 0 ) <= (n + 1) by XREAL_1: 7;

      then

       FC1: k in ( Seg (n + 1)) & m in ( Seg (n + 1));

      (1 + 0 ) <= (k + 1) & (k + 1) <= (n + 1) & (1 + 0 ) <= (m + 1) & (m + 1) <= (n + 1) by FC0, XREAL_1: 6;

      then

       FC3: (k + 1) in ( Seg (n + 1)) & (m + 1) in ( Seg (n + 1));

      per cases ;

        suppose

         CS1: k < i & m < j;

        then

         F11: (( Delete (M,i,j)) * (k,m)) = (M * (k,m)) by LAPLACE: 13, A5, D3;

        

         BF11: (( Delete (L,i,j)) * (k,m)) = (L * (k,m)) by LAPLACE: 13, A5, D3, CS1;

         [k, m] in [:( Seg (n + 1)), ( Seg (n + 1)):] by FC1, ZFMISC_1: 87;

        then [k, m] in ( Indices M) by MATRIX_0: 24;

        hence thesis by A2, F11, BF11, ZMATRLIN: 1;

      end;

        suppose

         CS2: k < i & m >= j;

        then

         F21: (( Delete (M,i,j)) * (k,m)) = (M * (k,(m + 1))) by LAPLACE: 13, A5, D3;

        

         BF21: (( Delete (L,i,j)) * (k,m)) = (L * (k,(m + 1))) by LAPLACE: 13, A5, D3, CS2;

         [k, (m + 1)] in [:( Seg (n + 1)), ( Seg (n + 1)):] by FC1, FC3, ZFMISC_1: 87;

        then [k, (m + 1)] in ( Indices M) by MATRIX_0: 24;

        hence thesis by A2, F21, BF21, ZMATRLIN: 1;

      end;

        suppose

         CS3: k >= i & m < j;

        then

         F31: (( Delete (M,i,j)) * (k,m)) = (M * ((k + 1),m)) by LAPLACE: 13, A5, D3;

        

         BF31: (( Delete (L,i,j)) * (k,m)) = (L * ((k + 1),m)) by LAPLACE: 13, A5, CS3, D3;

         [(k + 1), m] in [:( Seg (n + 1)), ( Seg (n + 1)):] by FC1, FC3, ZFMISC_1: 87;

        then [(k + 1), m] in ( Indices M) by MATRIX_0: 24;

        hence thesis by A2, F31, BF31, ZMATRLIN: 1;

      end;

        suppose

         CS4: k >= i & m >= j;

        then

         F41: (( Delete (M,i,j)) * (k,m)) = (M * ((k + 1),(m + 1))) by LAPLACE: 13, A5, D3;

        

         BF41: (( Delete (L,i,j)) * (k,m)) = (L * ((k + 1),(m + 1))) by LAPLACE: 13, A5, D3, CS4;

         [(k + 1), (m + 1)] in [:( Seg (n + 1)), ( Seg (n + 1)):] by FC3, ZFMISC_1: 87;

        then [(k + 1), (m + 1)] in ( Indices M) by MATRIX_0: 24;

        hence thesis by A2, F41, BF41, ZMATRLIN: 1;

      end;

    end;

    theorem :: ZMODLAT2:51

    for n,i,j,k,m be Nat, M be Matrix of (n + 1), F_Real st 0 < n & M is Matrix of (n + 1), F_Rat & [i, j] in ( Indices M) & [k, m] in ( Indices ( Delete (M,i,j))) holds (( Delete (M,i,j)) * (k,m)) is Element of F_Rat

    proof

      let n,i,j,k,m be Nat, M be Matrix of (n + 1), F_Real ;

      assume that

       A1: 0 < n and

       A2: M is Matrix of (n + 1), F_Rat and

       A3: [i, j] in ( Indices M) and

       A4: [k, m] in ( Indices ( Delete (M,i,j)));

      reconsider L = M as Matrix of (n + 1), F_Rat by A2;

      (( Delete (M,i,j)) * (k,m)) = (( Delete (L,i,j)) * (k,m)) by LmSign1F, A1, A3, A4;

      hence thesis;

    end;

    theorem :: ZMODLAT2:52

    

     LmSign1E: for n,i,j be Nat, M be Matrix of (n + 1), F_Real holds for L be Matrix of (n + 1), F_Rat st 0 < n & M = L & [i, j] in ( Indices M) holds ( Delete (M,i,j)) = ( Delete (L,i,j))

    proof

      let n,i,j be Nat, M be Matrix of (n + 1), F_Real ;

      let L be Matrix of (n + 1), F_Rat ;

      assume that

       A1: 0 < n and

       A2: M = L and

       A3: [i, j] in ( Indices M);

      set M0 = ( Delete (M,i,j));

      set L0 = ( Delete (L,i,j));

      

       X39: ((n + 1) -' 1) = n by NAT_D: 34;

      then

       D2: ( len M0) = n & ( width M0) = n & ( Indices M0) = [:( Seg n), ( Seg n):] by MATRIX_0: 24;

      

       BD2: ( len L0) = n & ( width L0) = n & ( Indices L0) = [:( Seg n), ( Seg n):] by MATRIX_0: 24, X39;

      for i1,j1 be Nat st [i1, j1] in ( Indices M0) holds (M0 * (i1,j1)) = (L0 * (i1,j1)) by LmSign1F, A1, A2, A3;

      hence thesis by BD2, D2, ZMATRLIN: 4;

    end;

    theorem :: ZMODLAT2:53

    

     LmSign1EX: for n,i,j be Nat, M be Matrix of (n + 1), F_Real st 0 < n & M is Matrix of (n + 1), F_Rat & [i, j] in ( Indices M) holds ( Delete (M,i,j)) is Matrix of n, F_Rat

    proof

      let n,i,j be Nat, M be Matrix of (n + 1), F_Real ;

      assume that

       A1: 0 < n and

       A2: M is Matrix of (n + 1), F_Rat and

       A3: [i, j] in ( Indices M);

      reconsider L = M as Matrix of (n + 1), F_Rat by A2;

      

       X1: ( Delete (M,i,j)) = ( Delete (L,i,j)) by LmSign1E, A1, A3;

      ((n + 1) -' 1) = n by NAT_D: 34;

      hence thesis by X1;

    end;

    theorem :: ZMODLAT2:54

    

     LmSign1A: for n be Nat, M be Matrix of n, F_Real holds for H be Matrix of n, F_Rat st M = H holds ( Det M) = ( Det H)

    proof

      defpred P[ Nat] means for M be Matrix of $1, F_Real holds for H be Matrix of $1, F_Rat st M = H holds ( Det M) = ( Det H);

      

       P0: P[ 0 ]

      proof

        let M be Matrix of 0 , F_Real ;

        let H be Matrix of 0 , F_Rat ;

        assume M = H;

        ( Det M) = ( 1. F_Real ) by MATRIXR2: 41

        .= ( 1. F_Rat )

        .= ( Det H) by MATRIXR2: 41;

        hence thesis;

      end;

      

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

      proof

        let n be Nat;

        assume

         P10: P[n];

        let M be Matrix of (n + 1), F_Real ;

        let H be Matrix of (n + 1), F_Rat ;

        assume

         AS1: M = H;

        reconsider j = 1 as Nat;

        

         X0: 1 <= 1 & 1 <= (n + 1) by NAT_1: 14;

        then

         JX: j in ( Seg (n + 1));

        then

         X1: ( Det M) = ( Sum ( LaplaceExpC (M,j))) by LAPLACE: 27;

        

         HX1: ( Det H) = ( Sum ( LaplaceExpC (H,j))) by JX, LAPLACE: 27;

        set L = ( LaplaceExpC (M,j));

        set I = ( LaplaceExpC (H,j));

        

         X2: ( len L) = (n + 1) & for i be Nat st i in ( dom L) holds (L . i) = ((M * (i,j)) * ( Cofactor (M,i,j))) by LAPLACE:def 8;

        

         Y3: ( dom L) = ( Seg ( len I)) by X2, FINSEQ_1:def 3, LAPLACE:def 8

        .= ( dom I) by FINSEQ_1:def 3;

        for i be Nat st i in ( dom L) holds (L . i) = (I . i)

        proof

          let i be Nat;

          assume

           X30: i in ( dom L);

          then

           X31: (L . i) = ((M * (i,j)) * ( Cofactor (M,i,j))) by LAPLACE:def 8;

          

           HX31: (I . i) = ((H * (i,j)) * ( Cofactor (H,i,j))) by Y3, X30, LAPLACE:def 8;

          i in ( Seg (n + 1)) & j in ( Seg (n + 1)) by X0, X2, X30, FINSEQ_1:def 3;

          then [i, j] in [:( Seg (n + 1)), ( Seg (n + 1)):] by ZFMISC_1: 87;

          then

           X41: [i, j] in ( Indices M) by MATRIX_0: 24;

          then

           X32: (M * (i,j)) = (H * (i,j)) by AS1, ZMATRLIN: 1;

          

           Y1: ((n + 1) -' 1) = n by NAT_D: 34;

          set DD = ( Delete (M,i,j));

          set EE = ( Delete (H,i,j));

          ( Det DD) = ( Det EE)

          proof

            per cases ;

              suppose 0 < n;

              hence ( Det DD) = ( Det EE) by AS1, P10, X41, Y1, LmSign1E;

            end;

              suppose not 0 < n;

              then

               Y2: n = 0 ;

              

              then ( Det DD) = ( 1. F_Real ) by Y1, MATRIXR2: 41

              .= ( 1. F_Rat )

              .= ( Det EE) by Y2, MATRIXR2: 41, Y1;

              hence thesis;

            end;

          end;

          hence (L . i) = (I . i) by X32, X31, HX31, ZMATRLIN43;

        end;

        then L = I by Y3;

        hence thesis by X1, HX1, ZMATRLIN42;

      end;

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

      hence thesis;

    end;

    theorem :: ZMODLAT2:55

    

     LmGM11: for n be Nat, M be Matrix of n, F_Real st M is Matrix of n, F_Rat holds ( Det M) in F_Rat

    proof

      defpred P[ Nat] means for M be Matrix of $1, F_Real st M is Matrix of $1, F_Rat holds ( Det M) in F_Rat ;

      

       P0: P[ 0 ]

      proof

        let M be Matrix of 0 , F_Real ;

        assume M is Matrix of 0 , F_Rat ;

        ( Det M) = ( 1. F_Real ) by MATRIXR2: 41

        .= 1;

        hence ( Det M) in F_Rat ;

      end;

      

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

      proof

        let n be Nat;

        assume

         P10: P[n];

        let M be Matrix of (n + 1), F_Real ;

        assume

         AS1: M is Matrix of (n + 1), F_Rat ;

        reconsider j = 1 as Nat;

        

         X0: 1 <= 1 & 1 <= (n + 1) by NAT_1: 14;

        then j in ( Seg (n + 1));

        then

         X1: ( Det M) = ( Sum ( LaplaceExpC (M,j))) by LAPLACE: 27;

        set L = ( LaplaceExpC (M,j));

        

         X2: ( len L) = (n + 1) & for i be Nat st i in ( dom L) holds (L . i) = ((M * (i,j)) * ( Cofactor (M,i,j))) by LAPLACE:def 8;

        for i be Nat st i in ( dom L) holds (L . i) in F_Rat

        proof

          let i be Nat;

          assume

           X30: i in ( dom L);

          then

           X31: (L . i) = ((M * (i,j)) * ( Cofactor (M,i,j))) by LAPLACE:def 8;

          i in ( Seg (n + 1)) & j in ( Seg (n + 1)) by X0, X2, X30, FINSEQ_1:def 3;

          then [i, j] in [:( Seg (n + 1)), ( Seg (n + 1)):] by ZFMISC_1: 87;

          then

           X41: [i, j] in ( Indices M) by MATRIX_0: 24;

          then

           X32: (M * (i,j)) is Element of F_Rat by AS1, ZMATRLIN: 41;

          ((n + 1) -' 1) = n by NAT_D: 34;

          then

          reconsider DD = ( Delete (M,i,j)) as Matrix of n, F_Real ;

          ( Det DD) in F_Rat

          proof

            per cases ;

              suppose 0 < n;

              then DD is Matrix of n, F_Rat by LmSign1EX, AS1, X41;

              hence ( Det DD) in F_Rat by P10;

            end;

              suppose not 0 < n;

              then n = 0 ;

              

              then ( Det DD) = ( 1. F_Real ) by MATRIXR2: 41

              .= 1;

              hence ( Det DD) in F_Rat ;

            end;

          end;

          then

           A1: ( Minor (M,i,j)) in F_Rat by NAT_D: 34;

          (( power F_Real ) . (( - ( 1_ F_Real )),(i + j))) in F_Rat by LmSign1D;

          hence (L . i) in F_Rat by A1, X32, X31, RAT_1:def 2;

        end;

        hence thesis by X1, LmSign1C;

      end;

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

      hence thesis;

    end;

    theorem :: ZMODLAT2:56

    for n,i,j be Nat, M be Matrix of (n + 1), F_Real st M is Matrix of (n + 1), F_Rat & [i, j] in ( Indices M) holds ( Cofactor (M,i,j)) in F_Rat

    proof

      let n,i,j be Nat, M be Matrix of (n + 1), F_Real such that

       AS: M is Matrix of (n + 1), F_Rat & [i, j] in ( Indices M);

      ((n + 1) -' 1) = n by NAT_D: 34;

      then

      reconsider DD = ( Delete (M,i,j)) as Matrix of n, F_Real ;

      ( Det DD) in F_Rat

      proof

        per cases ;

          suppose 0 < n;

          then DD is Matrix of n, F_Rat by LmSign1EX, AS;

          hence ( Det DD) in F_Rat by LmGM11;

        end;

          suppose not 0 < n;

          then n = 0 ;

          

          then ( Det DD) = ( 1. F_Real ) by MATRIXR2: 41

          .= 1;

          hence ( Det DD) in F_Rat ;

        end;

      end;

      then

       A1: ( Minor (M,i,j)) in F_Rat by NAT_D: 34;

      (( power F_Real ) . (( - ( 1_ F_Real )),(i + j))) in F_Rat by LmSign1D;

      hence thesis by A1, RAT_1:def 2;

    end;

    theorem :: ZMODLAT2:57

    for L be RATional Z_Lattice, b be OrdBasis of L holds ( Det ( GramMatrix b)) in F_Rat

    proof

      let L be RATional Z_Lattice, b be OrdBasis of L;

      ( GramMatrix b) is Matrix of ( dim L), F_Rat by ThGM1;

      hence thesis by LmGM11;

    end;

    theorem :: ZMODLAT2:58

    

     ZL2LmSc1: for L be positive-definite Z_Lattice, I be Basis of L, v,w be Vector of L holds (for u be Vector of L st u in I holds <;u, v;> = <;u, w;>) implies (for u be Vector of L holds <;u, v;> = <;u, w;>)

    proof

      let L be positive-definite Z_Lattice, I be Basis of L, v,w be Vector of L;

      assume

       AS: for u be Vector of L st u in I holds <;u, v;> = <;u, w;>;

      defpred P[ Nat] means for u be Vector of L, J be finite Subset of L st J c= I & ( card J) = $1 & u in ( Lin J) holds <;u, v;> = <;u, w;>;

      

       A1: P[ 0 ]

      proof

        let u be Vector of L, J be finite Subset of L such that

         B1: J c= I & ( card J) = 0 & u in ( Lin J);

        J = ( {} the carrier of L) by B1;

        then ( Lin J) = ( (0). L) by VECTSP_7: 9;

        then

         B2: u = ( 0. L) by B1, VECTSP_4: 35;

        then <;u, v;> = 0 by ZMODLAT1: 12;

        hence thesis by B2, ZMODLAT1: 12;

      end;

      

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

      proof

        let n be Nat such that

         B1: P[n];

        let u be Vector of L, J be finite Subset of L such that

         B2: J c= I & ( card J) = (n + 1) & u in ( Lin J);

        J is non empty by B2;

        then

        consider s be object such that

         B3: s in J;

        reconsider s as Vector of L by B3;

        set Js = (J \ {s});

         {s} is Subset of J by B3, SUBSET_1: 41;

        

        then

         B4: ( card Js) = ((n + 1) - ( card {s})) by B2, CARD_2: 44

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

        .= n;

        reconsider Js as finite Subset of L;

        reconsider S = {s} as finite Subset of L;

        

         B6: (Js /\ S) = {} by XBOOLE_0:def 7, XBOOLE_1: 79;

        consider l be Linear_Combination of J such that

         B7: u = ( Sum l) by B2, VECTSP_7: 7;

        reconsider lx = l as Linear_Combination of (Js \/ S) by B3, XBOOLE_1: 45, ZFMISC_1: 31;

        consider lx1 be Linear_Combination of Js, lx2 be Linear_Combination of S such that

         B8: lx = (lx1 + lx2) by B6, ZMODUL04: 26;

        

         B9: u = (( Sum lx1) + ( Sum lx2)) by B7, B8, VECTSP_6: 44;

        

         B10: ( Sum lx1) in ( Lin Js) by VECTSP_7: 7;

        Js c= J by XBOOLE_1: 36;

        then

         B11: Js c= I by B2;

        

         B12: ( Sum lx2) = ((lx2 . s) * s) by VECTSP_6: 17;

        

         B14: <;( Sum lx2), v;> = ((lx2 . s) * <;s, v;>) by B12, ZMODLAT1:def 3

        .= ((lx2 . s) * <;s, w;>) by AS, B2, B3

        .= <;( Sum lx2), w;> by B12, ZMODLAT1:def 3;

        

        thus <;u, v;> = ( <;( Sum lx1), v;> + <;( Sum lx2), v;>) by B9, ZMODLAT1:def 3

        .= ( <;( Sum lx1), w;> + <;( Sum lx2), w;>) by B1, B4, B10, B11, B14

        .= <;u, w;> by B9, ZMODLAT1:def 3;

      end;

      

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

      let u be Vector of L;

      

       A4: u in ( Lin I) by ZMODUL03: 14;

      reconsider n = ( card I) as Nat;

       P[n] by A3;

      hence thesis by A4;

    end;

    theorem :: ZMODLAT2:59

    

     ZL2ThSc1: for L be positive-definite Z_Lattice, b be OrdBasis of L, v,w be Vector of L st for n be Nat st n in ( dom b) holds <;(b /. n), v;> = <;(b /. n), w;> holds v = w

    proof

      let L be positive-definite Z_Lattice, b be OrdBasis of L, v,w be Vector of L such that

       A1: for n be Nat st n in ( dom b) holds <;(b /. n), v;> = <;(b /. n), w;>;

      reconsider I = ( rng b) as Basis of L by ZMATRLIN:def 5;

      for u be Vector of L st u in I holds <;u, v;> = <;u, w;>

      proof

        let u be Vector of L such that

         B1: u in I;

        consider i be Nat such that

         B2: i in ( dom b) & (b . i) = u by B1, FINSEQ_2: 10;

        (b /. i) = u by B2, PARTFUN1:def 6;

        hence thesis by A1, B2;

      end;

      then <;(v - w), v;> = <;(v - w), w;> by ZL2LmSc1;

      then ( <;(v - w), v;> - <;(v - w), w;>) = ( 0. INT.Ring );

      then ||.(v - w).|| = ( 0. INT.Ring ) by ZMODLAT1: 11;

      then (v - w) = ( 0. L) by ZMODLAT1: 16;

      hence thesis by RLVECT_1: 21;

    end;

    theorem :: ZMODLAT2:60

    for n be Nat, M be Matrix of n, F_Rat st M is without_repeated_line holds ( Det M) <> ( 0. F_Rat ) iff ( lines M) is linearly-independent

    proof

      let n be Nat, M be Matrix of n, F_Rat ;

      assume

       AS: M is without_repeated_line;

      hereby

        assume ( Det M) <> ( 0. F_Rat );

        then ( the_rank_of M) = n by MATRIX13: 83;

        hence ( lines M) is linearly-independent by MATRIX13: 110;

      end;

      assume ( lines M) is linearly-independent;

      then ( the_rank_of M) = n by AS, MATRIX13: 121;

      hence ( Det M) <> ( 0. F_Rat ) by MATRIX13: 83;

    end;

    theorem :: ZMODLAT2:61

    for L be positive-definite Z_Lattice, I be Basis of L, v,w be Vector of L holds (for u be Vector of L st u in I holds <;v, u;> = <;w, u;>) implies (for u be Vector of L holds <;v, u;> = <;w, u;>)

    proof

      let L be positive-definite Z_Lattice, I be Basis of L, v,w be Vector of L;

      assume

       AS: for u be Vector of L st u in I holds <;v, u;> = <;w, u;>;

      

       P1: for u be Vector of L st u in I holds <;u, v;> = <;u, w;>

      proof

        let u be Vector of L;

        assume

         P0: u in I;

        

        thus <;u, v;> = <;v, u;> by ZMODLAT1:def 3

        .= <;w, u;> by AS, P0

        .= <;u, w;> by ZMODLAT1:def 3;

      end;

      thus for u be Vector of L holds <;v, u;> = <;w, u;>

      proof

        let u be Vector of L;

        

        thus <;v, u;> = <;u, v;> by ZMODLAT1:def 3

        .= <;u, w;> by P1, ZL2LmSc1

        .= <;w, u;> by ZMODLAT1:def 3;

      end;

    end;

    theorem :: ZMODLAT2:62

    

     ZL2ThSc1X: for L be positive-definite Z_Lattice, b be OrdBasis of L, v,w be Vector of L st for n be Nat st n in ( dom b) holds <;v, (b /. n);> = <;w, (b /. n);> holds v = w

    proof

      let L be positive-definite Z_Lattice, b be OrdBasis of L, v,w be Vector of L such that

       A1: for n be Nat st n in ( dom b) holds <;v, (b /. n);> = <;w, (b /. n);>;

      for n be Nat st n in ( dom b) holds <;(b /. n), v;> = <;(b /. n), w;>

      proof

        let n be Nat;

        assume

         A2: n in ( dom b);

        

        thus <;(b /. n), v;> = <;v, (b /. n);> by ZMODLAT1:def 3

        .= <;w, (b /. n);> by A1, A2

        .= <;(b /. n), w;> by ZMODLAT1:def 3;

      end;

      hence thesis by ZL2ThSc1;

    end;

    theorem :: ZMODLAT2:63

    

     ZL2ThSc1D: for L be positive-definite Z_Lattice, b be OrdBasis of ( EMLat L), v,w be Vector of ( DivisibleMod L) st for n be Nat st n in ( dom b) holds (( ScProductDM L) . ((b /. n),v)) = (( ScProductDM L) . ((b /. n),w)) holds v = w

    proof

      let L be positive-definite Z_Lattice, b be OrdBasis of ( EMLat L), v,w be Vector of ( DivisibleMod L) such that

       A1: for n be Nat st n in ( dom b) holds (( ScProductDM L) . ((b /. n),v)) = (( ScProductDM L) . ((b /. n),w));

      consider i be Element of INT.Ring such that

       A2: i <> 0 & (i * v) in ( EMbedding L) by ZMODUL08: 29;

      consider j be Element of INT.Ring such that

       A3: j <> 0 & (j * w) in ( EMbedding L) by ZMODUL08: 29;

      (i * v) in ( rng ( MorphsZQ L)) by A2, ZMODUL08:def 3;

      then

      reconsider iv = (i * v) as Vector of ( EMLat L) by defEMLat;

      (j * w) in ( rng ( MorphsZQ L)) by A3, ZMODUL08:def 3;

      then

      reconsider jw = (j * w) as Vector of ( EMLat L) by defEMLat;

      

       A4: ( EMLat L) is Submodule of ( DivisibleMod L) by ThDivisibleL1;

      for n be Nat st n in ( dom b) holds <;(b /. n), (j * iv);> = <;(b /. n), (i * jw);>

      proof

        let n be Nat such that

         B1: n in ( dom b);

        (b /. n) in ( EMLat L);

        then (b /. n) in ( DivisibleMod L) by A4, ZMODUL01: 24;

        then

        reconsider bn = (b /. n) as Vector of ( DivisibleMod L);

        (b /. n) in ( EMLat L);

        then (b /. n) in ( rng ( MorphsZQ L)) by defEMLat;

        then

         B2: (b /. n) in ( EMbedding L) by ZMODUL08:def 3;

        

         B3: ((i * j) * (( ScProductDM L) . ((b /. n),v))) = (j * (i * (( ScProductDM L) . (bn,v))))

        .= (j * (i * (( ScProductDM L) . (v,bn)))) by ThSPDM1

        .= (j * (( ScProductDM L) . ((i * v),bn))) by ThSPDM1

        .= (j * (( ScProductEM L) . (iv,(b /. n)))) by A2, B2, ThSPEM3

        .= (j * <;iv, (b /. n);>) by defEMLat

        .= <;(j * iv), (b /. n);> by ZMODLAT1:def 3

        .= <;(b /. n), (j * iv);> by ZMODLAT1:def 3;

        ((i * j) * (( ScProductDM L) . ((b /. n),w))) = (i * (j * (( ScProductDM L) . (bn,w))))

        .= (i * (j * (( ScProductDM L) . (w,bn)))) by ThSPDM1

        .= (i * (( ScProductDM L) . ((j * w),bn))) by ThSPDM1

        .= (i * (( ScProductEM L) . (jw,(b /. n)))) by A3, B2, ThSPEM3

        .= (i * <;jw, (b /. n);>) by defEMLat

        .= <;(i * jw), (b /. n);> by ZMODLAT1:def 3

        .= <;(b /. n), (i * jw);> by ZMODLAT1:def 3;

        hence thesis by A1, B1, B3;

      end;

      

      then (j * iv) = (i * jw) by ZL2ThSc1

      .= (i * (j * w)) by A4, ZMODUL01: 29;

      

      then (j * (i * v)) = (i * (j * w)) by A4, ZMODUL01: 29

      .= ((i * j) * w) by VECTSP_1:def 16;

      then ((i * j) * v) = ((i * j) * w) by VECTSP_1:def 16;

      hence thesis by A2, A3, ZMODUL01: 10;

    end;

    theorem :: ZMODLAT2:64

    for L be positive-definite Z_Lattice, b be OrdBasis of ( EMLat L), v,w be Vector of ( DivisibleMod L) st for n be Nat st n in ( dom b) holds (( ScProductDM L) . (v,(b /. n))) = (( ScProductDM L) . (w,(b /. n))) holds v = w

    proof

      let L be positive-definite Z_Lattice, b be OrdBasis of ( EMLat L), v,w be Vector of ( DivisibleMod L) such that

       A1: for n be Nat st n in ( dom b) holds (( ScProductDM L) . (v,(b /. n))) = (( ScProductDM L) . (w,(b /. n)));

      for n be Nat st n in ( dom b) holds (( ScProductDM L) . ((b /. n),v)) = (( ScProductDM L) . ((b /. n),w))

      proof

        let n be Nat such that

         B1: n in ( dom b);

        

         B2: ( EMLat L) is Submodule of ( DivisibleMod L) by ThDivisibleL1;

        (b /. n) in ( EMLat L);

        then (b /. n) in ( DivisibleMod L) by B2, ZMODUL01: 24;

        then

        reconsider bn = (b /. n) as Vector of ( DivisibleMod L);

        

        thus (( ScProductDM L) . ((b /. n),v)) = (( ScProductDM L) . (v,bn)) by ThSPDM1

        .= (( ScProductDM L) . (w,(b /. n))) by A1, B1

        .= (( ScProductDM L) . (bn,w)) by ThSPDM1

        .= (( ScProductDM L) . ((b /. n),w));

      end;

      hence thesis by ZL2ThSc1D;

    end;

    theorem :: ZMODLAT2:65

    

     LMThGM21: for L be non trivial RATional positive-definite Z_Lattice, v be Element of L, b be FinSequence of L, sbv be FinSequence of F_Rat st ( len b) = ( len sbv) & for n be Nat st n in ( dom sbv) holds (sbv . n) = <;(b /. n), v;> holds <;( Sum b), v;> = ( Sum sbv)

    proof

      let L be non trivial RATional positive-definite Z_Lattice;

      let v be Element of L;

      defpred P[ Nat] means for F be FinSequence of L, Fv be FinSequence of F_Rat st ( len F) = $1 & ( len F) = ( len Fv) & for i be Nat st i in ( dom Fv) holds (Fv . i) = <;(F /. i), v;> holds <;( Sum F), v;> = ( Sum Fv);

      

       P1: P[ 0 ]

      proof

        let F be FinSequence of L, Fv be FinSequence of F_Rat ;

        assume

         AS1: ( len F) = 0 & ( len F) = ( len Fv) & for i be Nat st i in ( dom Fv) holds (Fv . i) = <;(F /. i), v;>;

        F = ( <*> the carrier of L) by AS1;

        then ( Sum F) = ( 0. L) by RLVECT_1: 43;

        then

         X1: <;( Sum F), v;> = ( 0. F_Rat ) by ZMODLAT1: 12;

        Fv = ( <*> the carrier of F_Rat ) by AS1;

        hence <;( Sum F), v;> = ( Sum Fv) by X1, RLVECT_1: 43;

      end;

      

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

      proof

        let n be Nat;

        assume

         AS1: P[n];

        let F be FinSequence of L, Fv be FinSequence of F_Rat ;

        assume

         AS2: ( len F) = (n + 1) & ( len F) = ( len Fv) & for i be Nat st i in ( dom Fv) holds (Fv . i) = <;(F /. i), v;>;

        reconsider F0 = (F | n) as FinSequence of L;

        (n + 1) in ( Seg (n + 1)) by FINSEQ_1: 4;

        then

         A70: (n + 1) in ( dom F) by AS2, FINSEQ_1:def 3;

        then (F . (n + 1)) in ( rng F) by FUNCT_1: 3;

        then

        reconsider af = (F . (n + 1)) as Element of L;

        

         P1: ( len F0) = n by FINSEQ_1: 59, AS2, NAT_1: 11;

        then

         P4: ( dom F0) = ( Seg n) by FINSEQ_1:def 3;

        

         A9: ( len F) = (( len F0) + 1) by AS2, FINSEQ_1: 59, NAT_1: 11;

        

         A11: F0 = (F | ( dom F0)) by P1, FINSEQ_1:def 3;

        reconsider Fv0 = (Fv | n) as FinSequence of F_Rat ;

        (n + 1) in ( Seg (n + 1)) by FINSEQ_1: 4;

        then

         A70F: (n + 1) in ( dom Fv) by AS2, FINSEQ_1:def 3;

        then (Fv . (n + 1)) in ( rng Fv) by FUNCT_1: 3;

        then

        reconsider afv = (Fv . (n + 1)) as Element of F_Rat ;

        

         P1F: ( len Fv0) = n by FINSEQ_1: 59, AS2, NAT_1: 11;

        then

         P4F: ( dom Fv0) = ( Seg n) by FINSEQ_1:def 3;

        

         A9F: ( len Fv) = (( len Fv0) + 1) by AS2, FINSEQ_1: 59, NAT_1: 11;

        

         P3F: Fv0 = (Fv | ( dom Fv0)) by P1F, FINSEQ_1:def 3;

        

         X0: for i be Nat st i in ( dom Fv0) holds (Fv0 . i) = <;(F0 /. i), v;>

        proof

          let i be Nat;

          assume

           P40: i in ( dom Fv0);

          ( dom Fv) = ( Seg (n + 1)) by AS2, FINSEQ_1:def 3;

          then ( dom Fv0) c= ( dom Fv) by P4F, FINSEQ_1: 5, NAT_1: 11;

          then

           X1: (Fv . i) = <;(F /. i), v;> by AS2, P40;

          i in ( dom F0) by P40, P4, P1F, FINSEQ_1:def 3;

          then (F /. i) = (F0 /. i) by PARTFUN1: 80;

          hence thesis by X1, P40, FUNCT_1: 47;

        end;

        reconsider i1 = ( Sum F0) as Element of L;

        

         X3: (F /. (n + 1)) = af by A70, PARTFUN1:def 6;

        

        thus <;( Sum F), v;> = <;(i1 + af), v;> by AS2, A9, A11, RLVECT_1: 38

        .= ( <;i1, v;> + <;af, v;>) by ZMODLAT1:def 3

        .= (( Sum Fv0) + <;af, v;>) by P1, P1F, AS1, X0

        .= (( Sum Fv0) + afv) by A70F, AS2, X3

        .= ( Sum Fv) by AS2, P3F, A9F, RLVECT_1: 38;

      end;

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

      hence thesis;

    end;

    

     LMThGM2311: for r be Element of F_Rat holds ex K be Integer st K <> 0 & (K * r) in INT

    proof

      let r be Element of F_Rat ;

      consider m,n be Integer such that

       P1: n <> 0 & r = (m / n) by RAT_1: 1;

      take n;

      thus n <> 0 by P1;

      (n * r) = m by P1, XCMPLX_1: 87;

      hence (n * r) in INT by INT_1:def 2;

    end;

    

     LMThGM231: for n be Nat, r be FinSequence of F_Rat st ( len r) = n holds ex K be Integer st K <> 0 & for i be Nat st i in ( Seg n) holds (K * (r /. i)) in INT

    proof

      defpred P[ Nat] means for r be FinSequence of F_Rat st ( len r) = $1 holds ex K be Integer st K <> 0 & for i be Nat st i in ( Seg $1) holds (K * (r /. i)) in INT ;

      

       P1: P[ 0 ]

      proof

        let r be FinSequence of F_Rat ;

        assume ( len r) = 0 ;

        set K = 1;

        take K;

        thus K <> 0 ;

        thus for i be Nat st i in ( Seg 0 ) holds (K * (r /. i)) in INT ;

      end;

      

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

      proof

        let n be Nat;

        assume

         AS1: P[n];

        let r be FinSequence of F_Rat ;

        assume

         AS2: ( len r) = (n + 1);

        reconsider r0 = (r | n) as FinSequence of F_Rat ;

        consider L0 be Integer such that

         Q0: L0 <> 0 & (L0 * (r /. (n + 1))) in INT by LMThGM2311;

        

         P1: ( len r0) = n by FINSEQ_1: 59, AS2, NAT_1: 11;

        then

        consider K0 be Integer such that

         Q1: K0 <> 0 & for i be Nat st i in ( Seg n) holds (K0 * (r0 /. i)) in INT by AS1;

        

         P4: ( dom r0) = ( Seg n) by P1, FINSEQ_1:def 3;

        set K = (L0 * K0);

        take K;

        thus K <> 0 by Q0, Q1;

        thus for i be Nat st i in ( Seg (n + 1)) holds (K * (r /. i)) in INT

        proof

          let i be Nat;

          assume i in ( Seg (n + 1));

          then

           Q3: 1 <= i & i <= (n + 1) by FINSEQ_1: 1;

          per cases ;

            suppose i <= n;

            then

             Q5: i in ( Seg n) by Q3;

            then (K0 * (r0 /. i)) in INT by Q1;

            then

            reconsider KR = (K0 * (r /. i)) as Integer by P4, Q5, PARTFUN1: 80;

            reconsider iL0 = L0 as Integer;

            (L0 * KR) in INT by INT_1:def 2;

            hence (K * (r /. i)) in INT ;

          end;

            suppose i > n;

            then (n + 1) <= i by NAT_1: 13;

            then

            reconsider LR = (L0 * (r /. i)) as Integer by Q0, Q3, XXREAL_0: 1;

            reconsider iK0 = K0 as Integer;

            (K0 * LR) in INT by INT_1:def 2;

            hence (K * (r /. i)) in INT ;

          end;

        end;

      end;

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

      hence thesis;

    end;

    theorem :: ZMODLAT2:66

    

     LMThGM23: for n be Nat, r be FinSequence of F_Rat st ( len r) = n holds ex K be Integer, Kr be FinSequence of INT.Ring st K <> 0 & ( len Kr) = n & for i be Nat st i in ( dom Kr) holds (Kr . i) = (K * (r /. i))

    proof

      let n be Nat, r be FinSequence of F_Rat ;

      assume ( len r) = n;

      then

      consider K be Integer such that

       P1: K <> 0 & for i be Nat st i in ( Seg n) holds (K * (r /. i)) in INT by LMThGM231;

      defpred Q[ Nat, object] means $2 = (K * (r /. $1));

      

       Z510: for i be Nat st i in ( Seg n) holds ex x be Element of the carrier of INT.Ring st Q[i, x]

      proof

        let i be Nat;

        assume i in ( Seg n);

        then

        reconsider x = (K * (r /. i)) as Element of INT.Ring by P1;

        take x;

        thus thesis;

      end;

      consider Kr be FinSequence of the carrier of INT.Ring such that

       Z511: ( dom Kr) = ( Seg n) & for k be Nat st k in ( Seg n) holds Q[k, (Kr . k)] from FINSEQ_1:sch 5( Z510);

      take K, Kr;

      thus K <> 0 by P1;

      n is Element of NAT by ORDINAL1:def 12;

      hence ( len Kr) = n by Z511, FINSEQ_1:def 3;

      thus for i be Nat st i in ( dom Kr) holds (Kr . i) = (K * (r /. i)) by Z511;

    end;

    theorem :: ZMODLAT2:67

    

     LMThGM24: for i,j be Nat holds for K be Field holds for a,aj be Element of K holds for R be Element of (i -VectSp_over K) st j in ( Seg i) & aj = (R . j) holds ((a * R) . j) = (a * aj)

    proof

      let i,j be Nat;

      let K be Field;

      let a,aj be Element of K;

      let R be Element of (i -VectSp_over K);

      assume

       AS: j in ( Seg i) & aj = (R . j);

      

       P0: the carrier of (i -VectSp_over K) = (i -tuples_on the carrier of K) by MATRIX13: 102;

      reconsider R0 = R as Element of (i -tuples_on the carrier of K) by MATRIX13: 102;

      

       P3: (a * R) = ((i -Mult_over K) . (a,R)) by PRVECT_1:def 5

      .= (the multF of K [;] (a,R0)) by PRVECT_1:def 4;

      (a * R) in (i -tuples_on the carrier of K) by P0;

      then

      consider s be Element of (the carrier of K * ) such that

       P4: (a * R) = s & ( len s) = i;

      ( dom (the multF of K [;] (a,R0))) = ( Seg i) by P3, P4, FINSEQ_1:def 3;

      hence ((a * R) . j) = (a * aj) by P3, AS, FUNCOP_1: 32;

    end;

    theorem :: ZMODLAT2:68

    

     LMThGM25: for i,j be Nat holds for K be Field holds for aj,bj be Element of K holds for A,B be Element of (i -VectSp_over K) st j in ( Seg i) & aj = (A . j) & bj = (B . j) holds ((A + B) . j) = (aj + bj)

    proof

      let i,j be Nat;

      let K be Field;

      let aj,bj be Element of K;

      let A,B be Element of (i -VectSp_over K);

      assume

       AS: j in ( Seg i) & aj = (A . j) & bj = (B . j);

      

       P1: the addLoopStr of (i -VectSp_over K) = (i -Group_over K) by PRVECT_1:def 5;

      

       P2: (i -Group_over K) = addLoopStr (# (i -tuples_on the carrier of K), ( product (the addF of K,i)), (i |-> ( 0. K)) qua Element of (i -tuples_on the carrier of K) #) by PRVECT_1:def 3;

      

       P0: the carrier of (i -VectSp_over K) = (i -tuples_on the carrier of K) by MATRIX13: 102;

      reconsider A0 = A, B0 = B as Element of (i -tuples_on the carrier of K) by MATRIX13: 102;

      

       P3: (A + B) = (the addF of K .: (A0,B0)) by P1, P2, PRVECT_1:def 1;

      (A + B) in (i -tuples_on the carrier of K) by P0;

      then

      consider s be Element of (the carrier of K * ) such that

       P4: (A + B) = s & ( len s) = i;

      ( dom (the addF of K .: (A0,B0))) = ( Seg i) by P3, P4, FINSEQ_1:def 3;

      hence ((A + B) . j) = (aj + bj) by P3, AS, FUNCOP_1: 22;

    end;

    theorem :: ZMODLAT2:69

    

     LMSUM1: for K be Field, n,i be Nat st i in ( Seg n) holds for s be FinSequence of (n -VectSp_over K) holds ex si be FinSequence of K st ( len si) = ( len s) & (( Sum s) . i) = ( Sum si) & for k be Nat st k in ( dom si) holds (si . k) = ((s /. k) . i)

    proof

      let K be Field, n,i be Nat;

      assume

       AS: i in ( Seg n);

      

       XP1: the addLoopStr of (n -VectSp_over K) = (n -Group_over K) by PRVECT_1:def 5;

      

       XP2: (n -Group_over K) = addLoopStr (# (n -tuples_on the carrier of K), ( product (the addF of K,n)), (n |-> ( 0. K)) qua Element of (n -tuples_on the carrier of K) #) by PRVECT_1:def 3;

      defpred P[ Nat] means for s be FinSequence of (n -VectSp_over K) st ( len s) = $1 holds ex si be FinSequence of K st ( len si) = ( len s) & (( Sum s) . i) = ( Sum si) & for k be Nat st k in ( dom si) holds (si . k) = ((s /. k) . i);

      

       P1: P[ 0 ]

      proof

        let s be FinSequence of (n -VectSp_over K);

        assume

         AS1: ( len s) = 0 ;

        

         P1: s = ( <*> the carrier of (n -VectSp_over K)) by AS1;

        set si = ( <*> the carrier of K);

        take si;

        thus ( len si) = ( len s) by AS1;

        (( 0. (n -VectSp_over K)) . i) = ( 0. K) by XP1, XP2, FUNCOP_1: 7, AS;

        

        hence (( Sum s) . i) = ( 0. K) by P1, RLVECT_1: 43

        .= ( Sum si) by RLVECT_1: 43;

        thus for k be Nat st k in ( dom si) holds (si . k) = ((s /. k) . i);

      end;

      

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

      proof

        let k be Nat;

        assume

         AS1: P[k];

        let s be FinSequence of (n -VectSp_over K);

        assume

         AS2: ( len s) = (k + 1);

        reconsider s0 = (s | k) as FinSequence of the carrier of (n -VectSp_over K);

        (k + 1) in ( Seg (k + 1)) by FINSEQ_1: 4;

        then

         A70: (k + 1) in ( dom s) by AS2, FINSEQ_1:def 3;

        then (s . (k + 1)) in ( rng s) by FUNCT_1: 3;

        then

        reconsider sk1 = (s . (k + 1)) as Element of the carrier of (n -VectSp_over K);

        

         P1: ( len s0) = k by FINSEQ_1: 59, AS2, NAT_1: 11;

        then

         P4: ( dom s0) = ( Seg k) by FINSEQ_1:def 3;

        

         A9: ( len s) = (( len s0) + 1) by AS2, FINSEQ_1: 59, NAT_1: 11;

        s0 = (s | ( dom s0)) by P1, FINSEQ_1:def 3;

        then

         P3: ( Sum s) = (( Sum s0) + sk1) by AS2, A9, RLVECT_1: 38;

        consider si0 be FinSequence of K such that

         P1F: ( len si0) = ( len s0) & (( Sum s0) . i) = ( Sum si0) & for k be Nat st k in ( dom si0) holds (si0 . k) = ((s0 /. k) . i) by P1, AS1;

        (s /. (k + 1)) in the carrier of (n -VectSp_over K);

        then (s /. (k + 1)) in (n -tuples_on the carrier of K) by MATRIX13: 102;

        then

        consider ss be Element of (the carrier of K * ) such that

         XP4: (s /. (k + 1)) = ss & ( len ss) = n;

        

         XP5: ( dom ss) = ( Seg n) by XP4, FINSEQ_1:def 3;

        reconsider ss as FinSequence of the carrier of K;

        (ss . i) in ( rng ss) by XP5, AS, FUNCT_1: 3;

        then

        reconsider si0k1 = ((s /. (k + 1)) . i) as Element of K by XP4;

        

         P2F: (sk1 . i) = si0k1 by A70, PARTFUN1:def 6;

        reconsider si = (si0 ^ <*si0k1*>) as FinSequence of K;

        

         Y0: ( Sum si) = (( Sum si0) + ( Sum <*si0k1*>)) by RLVECT_1: 41

        .= (( Sum si0) + si0k1) by RLVECT_1: 44;

        

         Y1: ( len si) = (( len si0) + ( len <*si0k1*>)) by FINSEQ_1: 22

        .= (( len si0) + 1) by FINSEQ_1: 39

        .= ( len s) by AS2, P1F, FINSEQ_1: 59, NAT_1: 11;

        for j be Nat st j in ( dom si) holds (si . j) = ((s /. j) . i)

        proof

          let j be Nat;

          assume j in ( dom si);

          then

           A2: 1 <= j & j <= (k + 1) by Y1, AS2, FINSEQ_3: 25;

          per cases ;

            suppose j <= k;

            then

             Q50: j in ( Seg k) by A2;

            then

             Q5: j in ( dom si0) by P1, P1F, FINSEQ_1:def 3;

            

            hence (si . j) = (si0 . j) by FINSEQ_1:def 7

            .= ((s0 /. j) . i) by P1F, Q5

            .= ((s /. j) . i) by P4, Q50, PARTFUN1: 80;

          end;

            suppose j > k;

            then (k + 1) <= j by NAT_1: 13;

            then j = (k + 1) by A2, XXREAL_0: 1;

            hence (si . j) = ((s /. j) . i) by P1, P1F, FINSEQ_1: 42;

          end;

        end;

        hence thesis by Y1, P3, P1F, P2F, AS, Y0, LMThGM25;

      end;

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

      hence thesis;

    end;

    theorem :: ZMODLAT2:70

    

     ThGM2: for L be non trivial RATional positive-definite Z_Lattice, b be OrdBasis of L holds ( Det ( GramMatrix b)) <> ( 0. F_Real )

    proof

      let L be non trivial RATional positive-definite Z_Lattice, b be OrdBasis of L;

      reconsider M = ( GramMatrix b) as Matrix of ( rank L), F_Rat by ThGM1;

      assume ( Det ( GramMatrix b)) = ( 0. F_Real );

      then

       AS: ( Det M) = ( 0. F_Rat ) by LmSign1A;

      

       A1: ( len M) = ( rank L) by MATRIX_0:def 2;

      

       A2: ( the_rank_of M) <> ( rank L) by AS, MATRIX13: 83;

      

       B3: ( dom M) = ( Seg ( len M)) by FINSEQ_1:def 3

      .= ( Seg ( rank L)) by MATRIX_0:def 2;

      

       B4: ( dom M) = ( Seg ( len b)) by B3, ZMATRLIN: 49

      .= ( dom b) by FINSEQ_1:def 3;

      ( dom b) = ( Seg ( rank L)) & ( rank L) is Element of NAT by B3, B4, ORDINAL1:def 12;

      then ( len b) = ( rank L) by FINSEQ_1:def 3;

      then

       C4: ( Indices ( BilinearM (( InnerProduct L),b,b))) = [:( Seg ( rank L)), ( Seg ( rank L)):] by MATRIX_0: 24;

      

       OTO2: M is one-to-one

      proof

        assume not M is one-to-one;

        then

        consider m1,m2 be object such that

         B1: m1 in ( dom M) & m2 in ( dom M) & (M . m1) = (M . m2) & m1 <> m2;

        

         B3: ( dom M) = ( Seg ( len ( GramMatrix b))) by FINSEQ_1:def 3

        .= ( Seg ( rank L)) by MATRIX_0:def 2;

        

         B4: ( dom M) = ( Seg ( len b)) by B3, ZMATRLIN: 49

        .= ( dom b) by FINSEQ_1:def 3;

        reconsider m1, m2 as Nat by B1;

        

         B5: for n be Nat st n in ( dom b) holds <;(b /. n), (b /. m1);> = <;(b /. n), (b /. m2);>

        proof

          let n be Nat such that

           C1: n in ( dom b);

          

           C3: [m1, n] in ( Indices ( BilinearM (( InnerProduct L),b,b))) by C1, B1, B3, B4, C4, ZFMISC_1: 87;

          

           C6: [m2, n] in ( Indices ( BilinearM (( InnerProduct L),b,b))) by C4, C1, B1, B3, B4, ZFMISC_1: 87;

          

           X1: ex p be FinSequence of F_Real st p = (( BilinearM (( InnerProduct L),b,b)) . m1) & (( BilinearM (( InnerProduct L),b,b)) * (m1,n)) = (p . n) by MATRIX_0:def 5, C3;

          

          thus <;(b /. n), (b /. m1);> = <;(b /. m1), (b /. n);> by ZMODLAT1:def 3

          .= (( InnerProduct L) . ((b /. m1),(b /. n)))

          .= (( BilinearM (( InnerProduct L),b,b)) * (m1,n)) by B1, B4, C1, ZMODLAT1:def 32

          .= (( BilinearM (( InnerProduct L),b,b)) * (m2,n)) by B1, C6, X1, MATRIX_0:def 5

          .= (( InnerProduct L) . ((b /. m2),(b /. n))) by B1, B4, C1, ZMODLAT1:def 32

          .= <;(b /. m2), (b /. n);>

          .= <;(b /. n), (b /. m2);> by ZMODLAT1:def 3;

        end;

        (b . m1) = (b /. m1) by B1, B4, PARTFUN1:def 6

        .= (b /. m2) by B5, ZL2ThSc1

        .= (b . m2) by B1, B4, PARTFUN1:def 6;

        then not b is one-to-one by B1, B4;

        hence contradiction by ZMATRLIN:def 5;

      end;

      then

       AA1: ( lines M) is linearly-dependent by A2, MATRIX13: 121;

      ( lines M) c= the carrier of (( rank L) -VectSp_over F_Rat );

      then

      reconsider M1 = M as FinSequence of (( rank L) -VectSp_over F_Rat ) by FINSEQ_1:def 4;

      consider r be FinSequence of F_Rat , rM1 be FinSequence of (( rank L) -VectSp_over F_Rat ) such that

       Z1: ( len r) = ( rank L) & ( len rM1) = ( rank L) & (for i be Nat st i in ( dom rM1) holds (rM1 . i) = ((r /. i) * (M1 /. i))) & ( Sum rM1) = ( 0. (( rank L) -VectSp_over F_Rat )) & r <> (( Seg ( len r)) --> ( 0. F_Rat )) by A1, AA1, OTO2, LMBASE2;

      consider K be Integer, Kr be FinSequence of INT.Ring such that

       Z2: K <> 0 & ( len Kr) = ( rank L) & for i be Nat st i in ( dom Kr) holds (Kr . i) = (K * (r /. i)) by Z1, LMThGM23;

      reconsider K1 = K as Element of F_Rat by INT_1:def 2, NUMBERS: 14;

      defpred P[ Nat, object] means ex rM1i be Element of (( rank L) -VectSp_over F_Rat ) st rM1i = (rM1 . $1) & $2 = (K1 * rM1i);

      

       KRM10: for k be Nat st k in ( Seg ( rank L)) holds ex x be Element of the carrier of (( rank L) -VectSp_over F_Rat ) st P[k, x]

      proof

        let k be Nat;

        assume

         KRM12: k in ( Seg ( rank L));

        ( dom rM1) = ( Seg ( rank L)) by Z1, FINSEQ_1:def 3;

        then (rM1 . k) = (rM1 /. k) by KRM12, PARTFUN1:def 6;

        then

        reconsider rM1i = (rM1 . k) as Element of (( rank L) -VectSp_over F_Rat );

        (K1 * rM1i) is Element of the carrier of (( rank L) -VectSp_over F_Rat );

        hence thesis;

      end;

      consider KrM1 be FinSequence of the carrier of (( rank L) -VectSp_over F_Rat ) such that

       KRM11: ( dom KrM1) = ( Seg ( rank L)) & for k be Nat st k in ( Seg ( rank L)) holds P[k, (KrM1 . k)] from FINSEQ_1:sch 5( KRM10);

      

       KRM1Z: ( rank L) is Element of NAT by ORDINAL1:def 12;

      then

       KRM1: ( len KrM1) = ( rank L) by FINSEQ_1:def 3, KRM11;

      

       Z3: for i be Nat st i in ( dom KrM1) holds ex M1i be Element of (( rank L) -VectSp_over F_Rat ), Kri be Element of F_Rat st M1i = (M1 . i) & Kri = (Kr . i) & (KrM1 . i) = (Kri * M1i)

      proof

        let i be Nat;

        assume

         Z300: i in ( dom KrM1);

        then

        consider rM1i be Element of (( rank L) -VectSp_over F_Rat ) such that

         Z301: rM1i = (rM1 . i) & (KrM1 . i) = (K1 * rM1i) by KRM11;

        

         Z303: i in ( dom rM1) by Z1, Z300, KRM11, FINSEQ_1:def 3;

        

         Z305: i in ( dom Kr) by Z2, Z300, KRM11, FINSEQ_1:def 3;

        

         Z307: ( dom M1) = ( Seg ( rank L)) by A1, FINSEQ_1:def 3;

        then (M1 /. i) = (M1 . i) by KRM11, Z300, PARTFUN1:def 6;

        then

        reconsider M1i = (M1 . i) as Element of (( rank L) -VectSp_over F_Rat );

        (Kr . i) = (Kr /. i) by PARTFUN1:def 6, Z305;

        then

        reconsider Kri = (Kr . i) as Element of F_Rat by NUMBERS: 14;

        take M1i, Kri;

        thus M1i = (M1 . i) & Kri = (Kr . i);

        

        thus (KrM1 . i) = (K1 * ((r /. i) * (M1 /. i))) by Z1, Z301, Z303

        .= (K1 * ((r /. i) * M1i)) by Z300, Z307, KRM11, PARTFUN1:def 6

        .= ((K1 * (r /. i)) * M1i) by VECTSP_1:def 16

        .= (Kri * M1i) by Z2, Z305;

      end;

      for k be Nat holds for v be Element of (( rank L) -VectSp_over F_Rat ) st k in ( dom KrM1) & v = (rM1 . k) holds (KrM1 . k) = (K1 * v)

      proof

        let k be Nat;

        let v be Element of (( rank L) -VectSp_over F_Rat );

        assume

         Z41: k in ( dom KrM1) & v = (rM1 . k);

        then

        consider rM1i be Element of (( rank L) -VectSp_over F_Rat ) such that

         Z42: rM1i = (rM1 . k) & (KrM1 . k) = (K1 * rM1i) by KRM11;

        thus thesis by Z42, Z41;

      end;

      

      then

       Z4A: ( Sum KrM1) = (K1 * ( Sum rM1)) by KRM1, Z1, RLVECT_2: 66

      .= ( 0. (( rank L) -VectSp_over F_Rat )) by Z1, VECTSP_1: 15;

      

       Z4B: Kr <> (( Seg ( len Kr)) --> ( 0. INT.Ring ))

      proof

        set f = (( Seg ( len Kr)) --> ( 0. INT.Ring ));

        set g = (( Seg ( len r)) --> ( 0. F_Rat ));

        ( dom r) = ( Seg ( len r)) by FINSEQ_1:def 3

        .= ( dom g) by FUNCT_2:def 1;

        then

        consider i be object such that

         R1: i in ( dom r) & (r . i) <> (g . i) by Z1;

        

         R2: i in ( Seg ( len r)) by FINSEQ_1:def 3, R1;

        reconsider i as Nat by R1;

        (r . i) <> ( 0. F_Rat ) by R1, R2, FUNCOP_1: 7;

        then

         R3: (r /. i) <> ( 0. INT.Ring ) by R1, PARTFUN1:def 6;

        

         R9: i in ( Seg ( len Kr)) by R1, Z1, Z2, FINSEQ_1:def 3;

        then i in ( dom Kr) by FINSEQ_1:def 3;

        then (Kr . i) = (K1 * (r /. i)) by Z2;

        hence thesis by R3, R9, Z2, FUNCOP_1: 7;

      end;

      set SKrM1 = ( Sum KrM1);

      

       Z5: for n be Nat st n in ( dom b) holds (SKrM1 . n) = ( 0. INT.Ring )

      proof

        let n be Nat;

        assume

         Z55: n in ( dom b);

        

         Z51: the addLoopStr of (( rank L) -VectSp_over F_Rat ) = (( rank L) -Group_over F_Rat ) by PRVECT_1:def 5;

        (( rank L) -Group_over F_Rat ) = addLoopStr (# (( rank L) -tuples_on the carrier of F_Rat ), ( product (the addF of F_Rat ,( rank L))), (( rank L) |-> ( 0. F_Rat )) qua Element of (( rank L) -tuples_on the carrier of F_Rat ) #) by PRVECT_1:def 3;

        hence (SKrM1 . n) = ( 0. INT.Ring ) by B3, B4, Z4A, Z51, Z55, FUNCOP_1: 7;

      end;

      defpred Q[ Nat, object] means $2 = ((Kr /. $1) * (b /. $1));

      

       Z510: for k be Nat st k in ( Seg ( rank L)) holds ex x be Element of the carrier of L st Q[k, x];

      consider Krb be FinSequence of the carrier of L such that

       Z511: ( dom Krb) = ( Seg ( rank L)) & for k be Nat st k in ( Seg ( rank L)) holds Q[k, (Krb . k)] from FINSEQ_1:sch 5( Z510);

      

       Z51Z: ( rank L) is Element of NAT by ORDINAL1:def 12;

      then

       Z51: ( len Krb) = ( rank L) by FINSEQ_1:def 3, Z511;

      

       Z6: for n be Nat st n in ( dom b) holds (SKrM1 . n) = <;( Sum Krb), (b /. n);>

      proof

        let n be Nat;

        assume

         Z61: n in ( dom b);

        then

        consider SKrM1n be FinSequence of F_Rat such that

         Z62: ( len SKrM1n) = ( len KrM1) & (SKrM1 . n) = ( Sum SKrM1n) & for k be Nat st k in ( dom SKrM1n) holds (SKrM1n . k) = ((KrM1 /. k) . n) by B3, B4, LMSUM1;

        

         Z63: ( len Krb) = ( rank L) by Z511, Z51Z, FINSEQ_1:def 3

        .= ( len SKrM1n) by Z62, KRM11, KRM1Z, FINSEQ_1:def 3;

        for k be Nat st k in ( dom SKrM1n) holds (SKrM1n . k) = <;(Krb /. k), (b /. n);>

        proof

          let k be Nat;

          assume

           X0: k in ( dom SKrM1n);

          then

           XX11: k in ( Seg ( len Krb)) by Z63, FINSEQ_1:def 3;

          then

           XX1: k in ( dom Krb) by FINSEQ_1:def 3;

          

          then

           Z65: (Krb /. k) = (Krb . k) by PARTFUN1:def 6

          .= ((Kr /. k) * (b /. k)) by Z511, XX1;

          (KrM1 /. k) in the carrier of (( rank L) -VectSp_over F_Rat );

          then (KrM1 /. k) in (( rank L) -tuples_on the carrier of F_Rat ) by MATRIX13: 102;

          then

          consider KrM1k be Element of (the carrier of F_Rat * ) such that

           T660: (KrM1 /. k) = KrM1k & ( len KrM1k) = ( rank L);

          

           T66: KrM1k = (KrM1 . k) & (SKrM1n . k) = (KrM1k . n) by KRM11, XX1, Z511, T660, Z62, X0, PARTFUN1:def 6;

          

           Z70: k in ( dom b) by XX11, Z511, B3, B4, FINSEQ_1:def 3;

          k in ( dom KrM1) by KRM1, KRM11, X0, Z62, FINSEQ_1:def 3;

          then

          consider M1k be Element of (( rank L) -VectSp_over F_Rat ), Krk be Element of F_Rat such that

           Z31: M1k = (M1 . k) & Krk = (Kr . k) & (KrM1 . k) = (Krk * M1k) by Z3;

          

           E10: [k, n] in ( Indices M) by Z70, Z61, B3, B4, C4, ZFMISC_1: 87;

          then

          consider p be FinSequence of F_Rat such that

           W34: p = (M . k) & (M * (k,n)) = (p . n) by MATRIX_0:def 5;

          reconsider MMkn = (M * (k,n)) as Element of F_Rat ;

          

           E3: k in ( dom Kr) by Z2, Z70, B3, B4, FINSEQ_1:def 3;

          

           Z90: (KrM1k . n) = (Krk * (M * (k,n))) by T66, W34, Z31, Z61, B3, B4, LMThGM24

          .= ((Kr /. k) * (M * (k,n))) by Z31, E3, PARTFUN1:def 6;

           <;(Krb /. k), (b /. n);> = <;(b /. n), ((Kr /. k) * (b /. k));> by Z65, ZMODLAT1:def 3

          .= ((Kr /. k) * <;(b /. n), (b /. k);>) by ZMODLAT1: 9

          .= ((Kr /. k) * <;(b /. k), (b /. n);>) by ZMODLAT1:def 3

          .= ((Kr /. k) * (( InnerProduct L) . ((b /. k),(b /. n))))

          .= ((Kr /. k) * (( BilinearM (( InnerProduct L),b,b)) * (k,n))) by ZMODLAT1:def 32, Z61, Z70

          .= ((Kr /. k) * (M * (k,n))) by E10, ZMATRLIN: 1

          .= (SKrM1n . k) by T660, Z62, X0, Z90;

          hence thesis;

        end;

        hence thesis by Z62, Z63, LMThGM21;

      end;

      for n be Nat st n in ( dom b) holds <;( 0. L), (b /. n);> = <;( Sum Krb), (b /. n);>

      proof

        let n be Nat;

        assume

         Z71: n in ( dom b);

        

        thus <;( 0. L), (b /. n);> = ( 0. INT.Ring ) by ZMODLAT1: 12

        .= (SKrM1 . n) by Z5, Z71

        .= <;( Sum Krb), (b /. n);> by Z6, Z71;

      end;

      then

       Z8: ( Sum Krb) = ( 0. L) by ZL2ThSc1X;

      

       Z9: b is one-to-one by ZMATRLIN:def 5;

      ( len Kr) = ( len b) by B3, B4, Z2, FINSEQ_1:def 3;

      then ( rng b) is linearly-dependent by Z51, Z511, Z4B, Z2, Z8, Z9, LMBASE2;

      then not ( rng b) is base by VECTSP_7:def 3;

      hence contradiction by ZMATRLIN:def 5;

    end;

    registration

      let L be non trivial RATional positive-definite Z_Lattice;

      let b be OrdBasis of L;

      cluster ( GramMatrix b) -> invertible;

      correctness

      proof

        ( Det ( GramMatrix b)) <> ( 0. F_Real ) by ThGM2;

        hence thesis by LAPLACE: 34;

      end;

    end