zmodlat3.miz



    begin

    theorem :: ZMODLAT3:1

    

     ThSLGM1: for L be RATional Z_Lattice, LX be Z_Lattice st LX is Submodule of ( DivisibleMod L) & the scalar of LX = (( ScProductDM L) || the carrier of LX) holds LX is RATional

    proof

      let L be RATional Z_Lattice, LX be Z_Lattice such that

       A1: LX is Submodule of ( DivisibleMod L) & the scalar of LX = (( ScProductDM L) || the carrier of LX);

      for v,u be Vector of LX holds <;v, u;> in RAT

      proof

        let v,u be Vector of LX;

        reconsider vv = v, uu = u as Vector of ( DivisibleMod L) by A1, ZMODUL01: 25;

         <;v, u;> = (( ScProductDM L) . (vv,uu)) by A1, FUNCT_1: 49;

        hence thesis by RAT_1:def 2;

      end;

      hence thesis by ZMODLAT2:def 1;

    end;

    registration

      let L be RATional Z_Lattice;

      cluster ( EMLat L) -> RATional;

      correctness

      proof

        

         A1: the scalar of ( EMLat L) = ( ScProductEM L) by ZMODLAT2:def 4

        .= (( ScProductDM L) || ( rng ( MorphsZQ L))) by ZMODLAT2: 7

        .= (( ScProductDM L) || the carrier of ( EMLat L)) by ZMODLAT2:def 4;

        ( EMLat L) is Submodule of ( DivisibleMod L) by ZMODLAT2: 20;

        hence thesis by A1, ThSLGM1;

      end;

    end

    registration

      let L be RATional Z_Lattice;

      let r be Element of F_Rat ;

      cluster ( EMLat (r,L)) -> RATional;

      correctness

      proof

        

         A1: the scalar of ( EMLat (r,L)) = (( ScProductDM L) || (r * ( rng ( MorphsZQ L)))) by ZMODLAT2:def 5

        .= (( ScProductDM L) || the carrier of ( EMLat (r,L))) by ZMODLAT2:def 5;

        ( EMLat (r,L)) is Submodule of ( DivisibleMod L) by ZMODLAT2: 21;

        hence thesis by A1, ThSLGM1;

      end;

    end

    definition

      let L be Z_Lattice;

      let F be FinSequence of L;

      let f be Function of L, INT.Ring ;

      let v be Vector of L;

      :: ZMODLAT3:def1

      func ScFS (v,f,F) -> FinSequence of F_Real means

      : defScFS: ( len it ) = ( len F) & for i be Nat st i in ( dom it ) holds (it . i) = <;v, ((f . (F /. i)) * (F /. i));>;

      existence

      proof

        deffunc X( object) = <;v, ((f . (F /. $1)) * (F /. $1));>;

        consider G be FinSequence such that

         A1: ( len G) = ( len F) & for i be Nat st i in ( dom G) holds (G . i) = X(i) from FINSEQ_1:sch 2;

        ( rng G) c= the carrier of F_Real

        proof

          let x be object such that

           B1: x in ( rng G);

          consider z be object such that

           B2: z in ( dom G) & x = (G . z) by B1, FUNCT_1:def 3;

          x = <;v, ((f . (F /. z)) * (F /. z));> by A1, B2;

          hence thesis;

        end;

        then

        reconsider G as FinSequence of F_Real by FINSEQ_1:def 4;

        take G;

        thus thesis by A1;

      end;

      uniqueness

      proof

        let f1,f2 be FinSequence of F_Real ;

        assume

         AS1: ( len f1) = ( len F) & for i be Nat st i in ( dom f1) holds (f1 . i) = <;v, ((f . (F /. i)) * (F /. i));>;

        assume

         AS2: ( len f2) = ( len F) & for i be Nat st i in ( dom f2) holds (f2 . i) = <;v, ((f . (F /. i)) * (F /. i));>;

        

         A2: ( dom f1) = ( dom f2) by AS1, AS2, FINSEQ_3: 29;

        for k be Nat st k in ( dom f1) holds (f1 . k) = (f2 . k)

        proof

          let k be Nat;

          assume

           B1: k in ( dom f1);

          

          hence (f1 . k) = <;v, ((f . (F /. k)) * (F /. k));> by AS1

          .= (f2 . k) by AS2, A2, B1;

        end;

        hence thesis by AS1, AS2, FINSEQ_3: 29;

      end;

    end

    theorem :: ZMODLAT3:2

    

     ThScFS1: for L be Z_Lattice, f be Function of L, INT.Ring , F be FinSequence of L, v,u be Vector of L, i be Nat st i in ( dom F) & u = (F . i) holds (( ScFS (v,f,F)) . i) = <;v, ((f . u) * u);>

    proof

      let L be Z_Lattice, f be Function of L, INT.Ring , F be FinSequence of L, v,u be Vector of L, i be Nat such that

       A1: i in ( dom F) & u = (F . i);

      

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

      ( len ( ScFS (v,f,F))) = ( len F) by defScFS;

      then i in ( dom ( ScFS (v,f,F))) by A1, FINSEQ_3: 29;

      hence thesis by A1, A2, defScFS;

    end;

    theorem :: ZMODLAT3:3

    

     ThScFS3: for L be Z_Lattice, f be Function of L, INT.Ring , v,u be Vector of L holds ( ScFS (v,f, <*u*>)) = <* <;v, ((f . u) * u);>*>

    proof

      let L be Z_Lattice, f be Function of L, INT.Ring ;

      let v,u be Vector of L;

      

       A1: 1 in {1} by TARSKI:def 1;

      

       A2: ( len ( ScFS (v,f, <*u*>))) = ( len <*u*>) by defScFS

      .= 1 by FINSEQ_1: 40;

      then ( dom ( ScFS (v,f, <*u*>))) = {1} by FINSEQ_1: 2, FINSEQ_1:def 3;

      

      then (( ScFS (v,f, <*u*>)) . 1) = <;v, ((f . ( <*u*> /. 1)) * ( <*u*> /. 1));> by A1, defScFS

      .= <;v, ((f . ( <*u*> /. 1)) * u);> by FINSEQ_4: 16

      .= <;v, ((f . u) * u);> by FINSEQ_4: 16;

      hence thesis by A2, FINSEQ_1: 40;

    end;

    theorem :: ZMODLAT3:4

    

     ThScFS6: for L be Z_Lattice, f be Function of L, INT.Ring , F,G be FinSequence of L, v be Vector of L holds ( ScFS (v,f,(F ^ G))) = (( ScFS (v,f,F)) ^ ( ScFS (v,f,G)))

    proof

      let L be Z_Lattice, f be Function of L, INT.Ring , F,G be FinSequence of L, v be Vector of L;

      set H = (( ScFS (v,f,F)) ^ ( ScFS (v,f,G)));

      set I = (F ^ G);

      

       A1: ( len F) = ( len ( ScFS (v,f,F))) by defScFS;

      

       A2: ( len H) = (( len ( ScFS (v,f,F))) + ( len ( ScFS (v,f,G)))) by FINSEQ_1: 22

      .= (( len F) + ( len ( ScFS (v,f,G)))) by defScFS

      .= (( len F) + ( len G)) by defScFS

      .= ( len I) by FINSEQ_1: 22;

      

       A3: ( len G) = ( len ( ScFS (v,f,G))) by defScFS;

      now

        let k be Nat;

        assume

         A4: k in ( dom H);

        per cases by A4, FINSEQ_1: 25;

          suppose

           A5: k in ( dom ( ScFS (v,f,F)));

          then

           A6: k in ( dom F) by A1, FINSEQ_3: 29;

          then

           A7: k in ( dom (F ^ G)) by FINSEQ_3: 22;

          

           A8: (F /. k) = (F . k) by A6, PARTFUN1:def 6

          .= ((F ^ G) . k) by A6, FINSEQ_1:def 7

          .= ((F ^ G) /. k) by A7, PARTFUN1:def 6;

          

          thus (H . k) = (( ScFS (v,f,F)) . k) by A5, FINSEQ_1:def 7

          .= <;v, ((f . (I /. k)) * (I /. k));> by A5, A8, defScFS;

        end;

          suppose

           A9: ex n be Nat st n in ( dom ( ScFS (v,f,G))) & k = (( len ( ScFS (v,f,F))) + n);

          

           A10: k in ( dom I) by A2, A4, FINSEQ_3: 29;

          consider n be Nat such that

           A11: n in ( dom ( ScFS (v,f,G))) and

           A12: k = (( len ( ScFS (v,f,F))) + n) by A9;

          

           A13: n in ( dom G) by A3, A11, FINSEQ_3: 29;

          

          then

           A14: (G /. n) = (G . n) by PARTFUN1:def 6

          .= ((F ^ G) . k) by A1, A12, A13, FINSEQ_1:def 7

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

          

          thus (H . k) = (( ScFS (v,f,G)) . n) by A11, A12, FINSEQ_1:def 7

          .= <;v, ((f . (I /. k)) * (I /. k));> by A11, A14, defScFS;

        end;

      end;

      hence thesis by A2, defScFS;

    end;

    definition

      let L be Z_Lattice;

      let l be Linear_Combination of L;

      let v be Vector of L;

      :: ZMODLAT3:def2

      func SumSc (v,l) -> Element of F_Real means

      : defSumSc: ex F be FinSequence of L st F is one-to-one & ( rng F) = ( Carrier l) & it = ( Sum ( ScFS (v,l,F)));

      existence

      proof

        consider F be FinSequence such that

         A1: ( rng F) = ( Carrier l) & F is one-to-one by FINSEQ_4: 58;

        reconsider F as FinSequence of L by A1, FINSEQ_1:def 4;

        take ( Sum ( ScFS (v,l,F))), F;

        thus thesis by A1;

      end;

      uniqueness

      proof

        let r1,r2 be Element of F_Real ;

        given F1 be FinSequence of L such that

         A1: F1 is one-to-one and

         A2: ( rng F1) = ( Carrier l) and

         A3: r1 = ( Sum ( ScFS (v,l,F1)));

        given F2 be FinSequence of L such that

         A4: F2 is one-to-one and

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

         A6: r2 = ( Sum ( ScFS (v,l,F2)));

        deffunc F( object) = ((F1 " ) . (F2 . $1));

        

         A7: ( len F1) = ( len F2) by A1, A2, A4, A5, FINSEQ_1: 48;

        then

         A8: ( dom F1) = ( dom F2) by FINSEQ_3: 29;

        

         A9: for x be object st x in ( dom F1) holds F(x) in ( dom F1)

        proof

          let x be object;

          assume x in ( dom F1);

          then (F2 . x) in ( rng F1) by A2, A5, A8, FUNCT_1: 3;

          then (F2 . x) in ( dom (F1 " )) by A1, FUNCT_1: 33;

          then ((F1 " ) . (F2 . x)) in ( rng (F1 " )) by FUNCT_1: 3;

          hence thesis by A1, FUNCT_1: 33;

        end;

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

         A10: for x be object st x in ( dom F1) holds (f . x) = F(x) from FUNCT_2:sch 2( A9);

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

        proof

          let x1,x2 be object;

          assume

           B1: x1 in ( dom f) & x2 in ( dom f) & (f . x1) = (f . x2);

          then (F2 . x1) in ( rng F1) by A2, A5, A8, FUNCT_1: 3;

          then

           B4: (F2 . x1) in ( dom (F1 " )) by A1, FUNCT_1: 33;

          (F2 . x2) in ( rng F1) by A2, A5, A8, B1, FUNCT_1: 3;

          then

           B7: (F2 . x2) in ( dom (F1 " )) by A1, FUNCT_1: 33;

          ((F1 " ) . (F2 . x1)) = (f . x1) by A10, B1

          .= ((F1 " ) . (F2 . x2)) by A10, B1;

          then (F2 . x1) = (F2 . x2) by A1, B4, B7, FUNCT_1:def 4;

          hence thesis by A4, A8, B1;

        end;

        then

         A11: f is one-to-one;

        ( dom F1) c= ( rng f)

        proof

          let y be object;

          assume

           B1: y in ( dom F1);

          then (F1 . y) in ( rng F2) by A2, A5, FUNCT_1: 3;

          then

          consider x be object such that

           B2: x in ( dom F2) & (F2 . x) = (F1 . y) by FUNCT_1:def 3;

          

           B3: (f . x) = ((F1 " ) . (F2 . x)) by A8, A10, B2

          .= y by A1, B1, B2, FUNCT_1: 34;

          x in ( dom f) by A8, B2, FUNCT_2:def 1;

          hence thesis by B3, FUNCT_1: 3;

        end;

        then

         A12: ( rng f) = ( dom F1);

        then

        reconsider f as Permutation of ( dom F1) by A11, FUNCT_2: 57;

        reconsider G1 = ( ScFS (v,l,F1)) as FinSequence of F_Real ;

        set G2 = ( ScFS (v,l,F2));

        

         A14: ( len G2) = ( len F2) by defScFS;

        ( len F1) = ( len G1) by defScFS;

        then

         A15: ( dom F1) = ( dom G1) by FINSEQ_3: 29;

        then

        reconsider f as Permutation of ( dom G1);

        

         A16: ( len G1) = ( len F2) by A7, defScFS

        .= ( len G2) by defScFS;

        for i be Nat st i in ( dom G2) holds (G2 . i) = (G1 . (f . i))

        proof

          let i be Nat such that

           B1: i in ( dom G2);

          

           B2: (G2 . i) = <;v, ((l . (F2 /. i)) * (F2 /. i));> by B1, defScFS;

          

           B3: i in ( dom F2) by A14, B1, FINSEQ_3: 29;

          then

          reconsider u = (F2 . i) as Element of L by FINSEQ_2: 11;

          

           B4: i in ( dom f) by A8, B3, FUNCT_2:def 1;

          then (f . i) in ( dom F1) by A12, FUNCT_1: 3;

          then

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

          reconsider w = (F1 . m) as Element of L by A12, B4, FINSEQ_2: 11, FUNCT_1: 3;

          

           B5: (F2 . i) in ( rng F1) by A2, A5, B3, FUNCT_1: 3;

          

           B6: (F1 . (f . i)) = (F1 . ((F1 " ) . (F2 . i))) by A8, A10, B3

          .= (F2 . i) by A1, B5, FUNCT_1: 35;

          (F1 . m) = (F1 /. m) & (F2 . i) = (F2 /. i) by A12, B3, B4, FUNCT_1: 3, PARTFUN1:def 6;

          hence (G2 . i) = (G1 . (f . i)) by A12, A15, B2, B4, B6, defScFS, FUNCT_1: 3;

        end;

        hence thesis by A3, A6, A16, RLVECT_2: 6;

      end;

    end

    theorem :: ZMODLAT3:5

    

     LmSumSc11: for L be Z_Lattice, v be Vector of L holds ( SumSc (v,( ZeroLC L))) = ( 0. F_Real )

    proof

      let L be Z_Lattice, v be Vector of L;

      consider F be FinSequence of L such that

       A1: F is one-to-one & ( rng F) = ( Carrier ( ZeroLC L)) & ( SumSc (v,( ZeroLC L))) = ( Sum ( ScFS (v,( ZeroLC L),F))) by defSumSc;

      F = {} by A1, VECTSP_6:def 3;

      then ( len ( ScFS (v,( ZeroLC L),F))) = 0 by defScFS;

      hence thesis by A1, RLVECT_1: 75;

    end;

    theorem :: ZMODLAT3:6

    for L be Z_Lattice, v be Vector of L, l be Linear_Combination of ( {} the carrier of L) holds ( SumSc (v,l)) = ( 0. F_Real )

    proof

      let L be Z_Lattice, v be Vector of L, l be Linear_Combination of ( {} the carrier of L);

      l = ( ZeroLC L) by VECTSP_6: 6;

      hence thesis by LmSumSc11;

    end;

    theorem :: ZMODLAT3:7

    

     LmSumSc13: for L be Z_Lattice, v be Vector of L, l be Linear_Combination of L st ( Carrier l) = {} holds ( SumSc (v,l)) = ( 0. F_Real )

    proof

      let L be Z_Lattice, v be Vector of L, l be Linear_Combination of L;

      assume ( Carrier l) = {} ;

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

      hence thesis by LmSumSc11;

    end;

    theorem :: ZMODLAT3:8

    

     LmSumSc14: for L be Z_Lattice, v,u be Vector of L, l be Linear_Combination of {u} holds ( SumSc (v,l)) = <;v, ((l . u) * u);>

    proof

      let L be Z_Lattice, v,u be Vector of L, l be Linear_Combination of {u};

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

        suppose ( Carrier l) = {} ;

        then

         A2: l = ( ZeroLC L) by VECTSP_6:def 3;

        

        hence ( SumSc (v,l)) = ( 0. F_Real ) by LmSumSc11

        .= <;v, ( 0. L);> by ZMODLAT1: 12

        .= <;v, (( 0. INT.Ring ) * u);> by VECTSP_1: 14

        .= <;v, ((l . u) * u);> by A2, VECTSP_6: 3;

      end;

        suppose ( Carrier l) = {u};

        then

        consider F be FinSequence of L such that

         A3: F is one-to-one & ( rng F) = {u} & ( SumSc (v,l)) = ( Sum ( ScFS (v,l,F))) by defSumSc;

        F = <*u*> by A3, FINSEQ_3: 97;

        then ( ScFS (v,l,F)) = <* <;v, ((l . u) * u);>*> by ThScFS3;

        hence thesis by A3, RLVECT_1: 44;

      end;

    end;

    theorem :: ZMODLAT3:9

    

     LmSumSc1X: for L be Z_Lattice, v be Vector of L, l1,l2 be Linear_Combination of L holds ( SumSc (v,(l1 + l2))) = (( SumSc (v,l1)) + ( SumSc (v,l2)))

    proof

      let L be Z_Lattice, w be Vector of L, l1,l2 be Linear_Combination of L;

      set A = ((( Carrier (l1 + l2)) \/ ( Carrier l1)) \/ ( Carrier l2));

      set C1 = (A \ ( Carrier l1));

      consider p be FinSequence such that

       A1: ( rng p) = C1 and

       A2: p is one-to-one by FINSEQ_4: 58;

      reconsider p as FinSequence of L by A1, FINSEQ_1:def 4;

      

       A3: A = (( Carrier l1) \/ (( Carrier (l1 + l2)) \/ ( Carrier l2))) by XBOOLE_1: 4;

      set C3 = (A \ ( Carrier (l1 + l2)));

      consider r be FinSequence such that

       A4: ( rng r) = C3 and

       A5: r is one-to-one by FINSEQ_4: 58;

      reconsider r as FinSequence of L by A4, FINSEQ_1:def 4;

      

       A6: A = (( Carrier (l1 + l2)) \/ (( Carrier l1) \/ ( Carrier l2))) by XBOOLE_1: 4;

      set C2 = (A \ ( Carrier l2));

      consider q be FinSequence such that

       A7: ( rng q) = C2 and

       A8: q is one-to-one by FINSEQ_4: 58;

      reconsider q as FinSequence of L by A7, FINSEQ_1:def 4;

      consider F be FinSequence of L such that

       A9: F is one-to-one and

       A10: ( rng F) = ( Carrier (l1 + l2)) and

       A11: ( SumSc (w,(l1 + l2))) = ( Sum ( ScFS (w,(l1 + l2),F))) by defSumSc;

      set FF = (F ^ r);

      consider G be FinSequence of L such that

       A12: G is one-to-one and

       A13: ( rng G) = ( Carrier l1) and

       A14: ( SumSc (w,l1)) = ( Sum ( ScFS (w,l1,G))) by defSumSc;

      ( rng FF) = (( rng F) \/ ( rng r)) by FINSEQ_1: 31;

      then ( rng FF) = (( Carrier (l1 + l2)) \/ A) by A10, A4, XBOOLE_1: 39;

      then

       A15: ( rng FF) = A by A6, XBOOLE_1: 7, XBOOLE_1: 12;

      set GG = (G ^ p);

      ( rng GG) = (( rng G) \/ ( rng p)) by FINSEQ_1: 31;

      then ( rng GG) = (( Carrier l1) \/ A) by A13, A1, XBOOLE_1: 39;

      then

       A16: ( rng GG) = A by A3, XBOOLE_1: 7, XBOOLE_1: 12;

      ( rng F) misses ( rng r)

      proof

        set x = the Element of (( rng F) /\ ( rng r));

        assume not thesis;

        then x in ( Carrier (l1 + l2)) & x in C3 by A10, A4, XBOOLE_0:def 4;

        hence thesis by XBOOLE_0:def 5;

      end;

      then

       A17: FF is one-to-one by A9, A5, FINSEQ_3: 91;

      ( rng G) misses ( rng p)

      proof

        set x = the Element of (( rng G) /\ ( rng p));

        assume not thesis;

        then x in ( Carrier l1) & x in C1 by A13, A1, XBOOLE_0:def 4;

        hence thesis by XBOOLE_0:def 5;

      end;

      then

       A18: GG is one-to-one by A12, A2, FINSEQ_3: 91;

      then

       A19: ( len GG) = ( len FF) by A17, A16, A15, FINSEQ_1: 48;

      deffunc F( Nat) = (FF <- (GG . $1));

      consider P be FinSequence such that

       A20: ( len P) = ( len FF) and

       A21: for k be Nat st k in ( dom P) holds (P . k) = F(k) from FINSEQ_1:sch 2;

      

       A22: ( dom P) = ( dom FF) by A20, FINSEQ_3: 29;

      

       a22: ( dom FF) = ( dom GG) by A19, FINSEQ_3: 29;

       A23:

      now

        let x be object;

        assume

         A24: x in ( dom GG);

        then

        reconsider n = x as Element of NAT ;

        (GG . n) in ( rng FF) by A16, A15, A24, FUNCT_1:def 3;

        then

         A25: FF just_once_values (GG . n) by A17, FINSEQ_4: 8;

        (FF . (P . n)) = (FF . (FF <- (GG . n))) by A21, A22, a22, A24

        .= (GG . n) by A25, FINSEQ_4:def 3;

        hence (GG . x) = (FF . (P . x));

      end;

      

       A26: ( rng P) c= ( dom FF)

      proof

        let x be object;

        assume x in ( rng P);

        then

        consider y be object such that

         A27: y in ( dom P) and

         A28: (P . y) = x by FUNCT_1:def 3;

        reconsider y as Element of NAT by A27;

        y in ( dom GG) by A19, A20, A27, FINSEQ_3: 29;

        then (GG . y) in ( rng FF) by A16, A15, FUNCT_1:def 3;

        then

         A29: FF just_once_values (GG . y) by A17, FINSEQ_4: 8;

        (P . y) = (FF <- (GG . y)) by A21, A27;

        hence thesis by A28, A29, FINSEQ_4:def 3;

      end;

      now

        let x be object;

        thus x in ( dom GG) implies x in ( dom P) & (P . x) in ( dom FF)

        proof

          assume x in ( dom GG);

          hence x in ( dom P) by A20, FINSEQ_3: 29, A19;

          then (P . x) in ( rng P) by FUNCT_1:def 3;

          hence thesis by A26;

        end;

        assume x in ( dom P) & (P . x) in ( dom FF);

        hence x in ( dom GG) by A20, FINSEQ_3: 29, A19;

      end;

      then

       A31: GG = (FF * P) by A23, FUNCT_1: 10;

      ( dom FF) c= ( rng P)

      proof

        set f = ((FF " ) * GG);

        let x be object;

        assume

         A32: x in ( dom FF);

        ( dom (FF " )) = ( rng GG) by A17, A16, A15, FUNCT_1: 33;

        

        then

         A33: ( rng f) = ( rng (FF " )) by RELAT_1: 28

        .= ( dom FF) by A17, FUNCT_1: 33;

        f = (((FF " ) * FF) * P) by A31, RELAT_1: 36

        .= (( id ( dom FF)) * P) by A17, FUNCT_1: 39

        .= P by A26, RELAT_1: 53;

        hence thesis by A32, A33;

      end;

      then

       A34: ( dom FF) = ( rng P) by A26;

      

       A35: ( len r) = ( len ( ScFS (w,(l1 + l2),r))) by defScFS;

      then

       B1: ( dom r) = ( dom ( ScFS (w,(l1 + l2),r))) by FINSEQ_3: 29;

      now

        let k be Nat;

        assume

         A36: k in ( dom ( ScFS (w,(l1 + l2),r)));

        then (r /. k) = (r . k) by B1, PARTFUN1:def 6;

        then (r /. k) in C3 by A4, A36, B1, FUNCT_1:def 3;

        then

         A37: not (r /. k) in ( Carrier (l1 + l2)) by XBOOLE_0:def 5;

        (( ScFS (w,(l1 + l2),r)) . k) = <;w, (((l1 + l2) . (r /. k)) * (r /. k));> by A36, defScFS;

        

        then (( ScFS (w,(l1 + l2),r)) . k) = <;w, (( 0. INT.Ring ) * (r /. k));> by A37

        .= <;w, ( 0. L);> by VECTSP_1: 14

        .= ( 0. F_Real ) by ZMODLAT1: 12;

        

        hence (( ScFS (w,(l1 + l2),r)) . k) = ( - (( ScFS (w,(l1 + l2),r)) . k))

        .= ( - (( ScFS (w,(l1 + l2),r)) /. k)) by A36, PARTFUN1:def 6;

      end;

      then

       A38: ( Sum ( ScFS (w,(l1 + l2),r))) = ( - ( Sum ( ScFS (w,(l1 + l2),r)))) by A35, RLVECT_2: 4;

      

       A39: ( len p) = ( len ( ScFS (w,l1,p))) by defScFS;

      then

       B1: ( dom p) = ( dom ( ScFS (w,l1,p))) by FINSEQ_3: 29;

      now

        let k be Nat;

        assume

         A40: k in ( dom ( ScFS (w,l1,p)));

        then (p /. k) = (p . k) by B1, PARTFUN1:def 6;

        then (p /. k) in C1 by A1, A40, B1, FUNCT_1:def 3;

        then

         A41: not (p /. k) in ( Carrier l1) by XBOOLE_0:def 5;

        (( ScFS (w,l1,p)) . k) = <;w, ((l1 . (p /. k)) * (p /. k));> by A40, defScFS;

        

        then (( ScFS (w,l1,p)) . k) = <;w, (( 0. INT.Ring ) * (p /. k));> by A41

        .= <;w, ( 0. L);> by VECTSP_1: 14

        .= ( 0. F_Real ) by ZMODLAT1: 12;

        

        hence (( ScFS (w,l1,p)) . k) = ( - (( ScFS (w,l1,p)) . k))

        .= ( - (( ScFS (w,l1,p)) /. k)) by A40, PARTFUN1:def 6;

      end;

      then

       A42: ( Sum ( ScFS (w,l1,p))) = ( - ( Sum ( ScFS (w,l1,p)))) by A39, RLVECT_2: 4;

      

       A43: ( len q) = ( len ( ScFS (w,l2,q))) by defScFS;

      then

       B1: ( dom q) = ( dom ( ScFS (w,l2,q))) by FINSEQ_3: 29;

      now

        let k be Nat;

        assume

         A44: k in ( dom ( ScFS (w,l2,q)));

        then (q /. k) = (q . k) by B1, PARTFUN1:def 6;

        then (q /. k) in C2 by A7, A44, B1, FUNCT_1:def 3;

        then

         A45: not (q /. k) in ( Carrier l2) by XBOOLE_0:def 5;

        (( ScFS (w,l2,q)) . k) = <;w, ((l2 . (q /. k)) * (q /. k));> by A44, defScFS;

        

        then (( ScFS (w,l2,q)) . k) = <;w, (( 0. INT.Ring ) * (q /. k));> by A45

        .= <;w, ( 0. L);> by VECTSP_1: 14

        .= ( 0. F_Real ) by ZMODLAT1: 12;

        

        hence (( ScFS (w,l2,q)) . k) = ( - (( ScFS (w,l2,q)) . k))

        .= ( - (( ScFS (w,l2,q)) /. k)) by A44, PARTFUN1:def 6;

      end;

      then

       A46: ( Sum ( ScFS (w,l2,q))) = ( - ( Sum ( ScFS (w,l2,q)))) by A43, RLVECT_2: 4;

      set g = ( ScFS (w,l1,GG));

      

       A47: ( len g) = ( len GG) by defScFS;

      then

       A48: ( dom GG) = ( dom g) by FINSEQ_3: 29;

      set f = ( ScFS (w,(l1 + l2),FF));

      consider H be FinSequence of L such that

       A49: H is one-to-one and

       A50: ( rng H) = ( Carrier l2) and

       A51: ( Sum ( ScFS (w,l2,H))) = ( SumSc (w,l2)) by defSumSc;

      set HH = (H ^ q);

      ( rng H) misses ( rng q)

      proof

        set x = the Element of (( rng H) /\ ( rng q));

        assume not thesis;

        then x in ( Carrier l2) & x in C2 by A50, A7, XBOOLE_0:def 4;

        hence thesis by XBOOLE_0:def 5;

      end;

      then

       A52: HH is one-to-one by A49, A8, FINSEQ_3: 91;

      ( rng HH) = (( rng H) \/ ( rng q)) by FINSEQ_1: 31;

      then ( rng HH) = (( Carrier l2) \/ A) by A50, A7, XBOOLE_1: 39;

      then

       A53: ( rng HH) = A by XBOOLE_1: 7, XBOOLE_1: 12;

      then

       A54: ( len GG) = ( len HH) by A52, A18, A16, FINSEQ_1: 48;

      then

       a54: ( dom GG) = ( dom HH) by FINSEQ_3: 29;

      deffunc F( Nat) = (HH <- (GG . $1));

      consider R be FinSequence such that

       A55: ( len R) = ( len HH) and

       A56: for k be Nat st k in ( dom R) holds (R . k) = F(k) from FINSEQ_1:sch 2;

      

       A57: ( dom R) = ( dom HH) by A55, FINSEQ_3: 29;

       A58:

      now

        let x be object;

        assume

         A59: x in ( dom GG);

        then

        reconsider n = x as Element of NAT ;

        (GG . n) in ( rng HH) by A16, A53, A59, FUNCT_1:def 3;

        then

         A60: HH just_once_values (GG . n) by A52, FINSEQ_4: 8;

        (HH . (R . n)) = (HH . (HH <- (GG . n))) by A56, A57, A59, a54

        .= (GG . n) by A60, FINSEQ_4:def 3;

        hence (GG . x) = (HH . (R . x));

      end;

      

       A61: ( rng R) c= ( dom HH)

      proof

        let x be object;

        assume x in ( rng R);

        then

        consider y be object such that

         A62: y in ( dom R) and

         A63: (R . y) = x by FUNCT_1:def 3;

        reconsider y as Element of NAT by A62;

        y in ( dom GG) by A54, A55, A62, FINSEQ_3: 29;

        then (GG . y) in ( rng HH) by A16, A53, FUNCT_1:def 3;

        then

         A64: HH just_once_values (GG . y) by A52, FINSEQ_4: 8;

        (R . y) = (HH <- (GG . y)) by A56, A62;

        hence thesis by A63, A64, FINSEQ_4:def 3;

      end;

      now

        let x be object;

        thus x in ( dom GG) implies x in ( dom R) & (R . x) in ( dom HH)

        proof

          assume x in ( dom GG);

          hence x in ( dom R) by A55, FINSEQ_3: 29, A54;

          then (R . x) in ( rng R) by FUNCT_1:def 3;

          hence thesis by A61;

        end;

        assume x in ( dom R) & (R . x) in ( dom HH);

        hence x in ( dom GG) by A54, A55, FINSEQ_3: 29;

      end;

      then

       A66: GG = (HH * R) by A58, FUNCT_1: 10;

      ( dom HH) c= ( rng R)

      proof

        set f = ((HH " ) * GG);

        let x be object;

        assume

         A67: x in ( dom HH);

        ( dom (HH " )) = ( rng GG) by A52, A16, A53, FUNCT_1: 33;

        

        then

         A68: ( rng f) = ( rng (HH " )) by RELAT_1: 28

        .= ( dom HH) by A52, FUNCT_1: 33;

        f = (((HH " ) * HH) * R) by A66, RELAT_1: 36

        .= (( id ( dom HH)) * R) by A52, FUNCT_1: 39

        .= R by A61, RELAT_1: 53;

        hence thesis by A67, A68;

      end;

      then

       A69: ( dom HH) = ( rng R) by A61;

      set h = ( ScFS (w,l2,HH));

      

       A70: ( Sum h) = ( Sum (( ScFS (w,l2,H)) ^ ( ScFS (w,l2,q)))) by ThScFS6

      .= (( Sum ( ScFS (w,l2,H))) + ( 0. F_Real )) by A46, RLVECT_1: 41

      .= ( Sum ( ScFS (w,l2,H)));

      

       A71: ( Sum g) = ( Sum (( ScFS (w,l1,G)) ^ ( ScFS (w,l1,p)))) by ThScFS6

      .= (( Sum ( ScFS (w,l1,G))) + ( 0. F_Real )) by A42, RLVECT_1: 41

      .= ( Sum ( ScFS (w,l1,G)));

      

       A72: ( dom P) = ( dom FF) by A20, FINSEQ_3: 29;

      

       A73: P is one-to-one by A20, A34, FINSEQ_3: 29, FINSEQ_4: 60;

      

       A74: ( dom R) = ( dom HH) by A55, FINSEQ_3: 29;

      

       A75: R is one-to-one by A55, A69, FINSEQ_3: 29, FINSEQ_4: 60;

      R is Function of ( dom HH), ( dom HH) by A61, A74, FUNCT_2: 2;

      then

      reconsider R as Permutation of ( dom HH) by A69, A75, FUNCT_2: 57;

      

       A76: ( len h) = ( len HH) by defScFS;

      then ( dom h) = ( dom HH) by FINSEQ_3: 29;

      then

      reconsider R as Permutation of ( dom h);

      reconsider Hp = (h * R) as FinSequence of F_Real by FINSEQ_2: 47;

      

       A77: ( len Hp) = ( len GG) by A54, A76, FINSEQ_2: 44;

      P is Function of ( dom FF), ( dom FF) by A26, A72, FUNCT_2: 2;

      then

      reconsider P as Permutation of ( dom FF) by A34, A73, FUNCT_2: 57;

      

       A78: ( len f) = ( len FF) by defScFS;

      then ( dom f) = ( dom FF) by FINSEQ_3: 29;

      then

      reconsider P as Permutation of ( dom f);

      reconsider Fp = (f * P) as FinSequence of F_Real by FINSEQ_2: 47;

      

       A79: ( Sum f) = ( Sum (( ScFS (w,(l1 + l2),F)) ^ ( ScFS (w,(l1 + l2),r)))) by ThScFS6

      .= (( Sum ( ScFS (w,(l1 + l2),F))) + ( 0. F_Real )) by A38, RLVECT_1: 41

      .= ( Sum ( ScFS (w,(l1 + l2),F)));

      deffunc F( Nat) = ((g /. $1) + (Hp /. $1));

      consider I be FinSequence such that

       A80: ( len I) = ( len GG) and

       A81: for k be Nat st k in ( dom I) holds (I . k) = F(k) from FINSEQ_1:sch 2;

      

       A83: ( dom I) = ( dom GG) by A80, FINSEQ_3: 29;

      ( rng I) c= the carrier of F_Real

      proof

        let x be object;

        assume x in ( rng I);

        then

        consider y be object such that

         A84: y in ( dom I) and

         A85: (I . y) = x by FUNCT_1:def 3;

        reconsider y as Element of NAT by A84;

        (I . y) = ((g /. y) + (Hp /. y)) by A81, A84;

        hence thesis by A85;

      end;

      then

      reconsider I as FinSequence of F_Real by FINSEQ_1:def 4;

      

       A86: ( len Fp) = ( len I) by A19, A78, A80, FINSEQ_2: 44;

      then

       X1: ( dom I) = ( Seg ( len I)) & ( dom Fp) = ( Seg ( len I)) by FINSEQ_1:def 3;

      

       X2: ( dom Hp) = ( Seg ( len Hp)) by FINSEQ_1:def 3

      .= ( dom I) by A54, A76, A80, FINSEQ_1:def 3, FINSEQ_2: 44;

      

       X3: ( dom HH) = ( Seg ( len HH)) by FINSEQ_1:def 3

      .= ( dom I) by A18, A16, A52, A53, A80, FINSEQ_1: 48, FINSEQ_1:def 3;

      

       X5: ( dom g) = ( Seg ( len g)) by FINSEQ_1:def 3

      .= ( dom I) by A80, defScFS, FINSEQ_1:def 3;

       A87:

      now

        let k be Nat;

        assume

         A88: k in ( dom I);

        

        then

         A90: (Hp /. k) = ((h * R) . k) by X2, PARTFUN1:def 6

        .= (h . (R . k)) by A88, X2, FUNCT_1: 12;

        set v = (GG /. k);

        

         A91: (Fp . k) = (f . (P . k)) by A88, X1, FUNCT_1: 12;

        (R . k) in ( dom R) by A69, A74, A88, X3, FUNCT_1:def 3;

        then

        reconsider j = (R . k) as Element of NAT by FINSEQ_3: 23;

        

         A94: (HH . j) = (GG . k) by A58, A88, X3, a54

        .= (GG /. k) by A88, X3, PARTFUN1:def 6, a54;

        

         A95: ( dom FF) = ( dom GG) by A19, FINSEQ_3: 29;

        then (P . k) in ( dom P) by A34, A72, A88, X3, FUNCT_1:def 3, a54;

        then

        reconsider l = (P . k) as Element of NAT by FINSEQ_3: 23;

        

         A96: (FF . l) = (GG . k) by A23, A88, X3, a54

        .= (GG /. k) by A88, X3, a54, PARTFUN1:def 6;

        (R . k) in ( dom HH) by A69, A74, A88, X3, FUNCT_1:def 3;

        then

         A97: (h . j) = <;w, ((l2 . v) * v);> by A94, ThScFS1;

        (P . k) in ( dom FF) by A34, A72, A88, A95, X3, a54, FUNCT_1:def 3;

        

        then

         A98: (f . l) = <;w, (((l1 + l2) . v) * v);> by A96, ThScFS1

        .= <;w, (((l1 . v) + (l2 . v)) * v);> by VECTSP_6: 22

        .= <;w, (((l1 . v) * v) + ((l2 . v) * v));> by VECTSP_1:def 15

        .= ( <;w, ((l1 . v) * v);> + <;w, ((l2 . v) * v);>) by ZMODLAT1: 8;

        (g /. k) = (g . k) by A88, X5, PARTFUN1:def 6

        .= <;w, ((l1 . v) * v);> by A88, X5, defScFS;

        hence (I . k) = (Fp . k) by A81, A88, A90, A97, A91, A98;

      end;

      ( dom I) = ( Seg ( len I)) & ( dom Fp) = ( Seg ( len I)) by A86, FINSEQ_1:def 3;

      then

       A100: I = Fp by A87;

      ( Sum Fp) = ( Sum f) & ( Sum Hp) = ( Sum h) by RLVECT_2: 7;

      hence thesis by A11, A14, A51, A71, A70, A79, A80, A81, A83, A77, A47, A100, A48, RLVECT_2: 2;

    end;

    theorem :: ZMODLAT3:10

    

     ThSumSc1: for L be Z_Lattice, l be Linear_Combination of L, v be Vector of L holds <;v, ( Sum l);> = ( SumSc (v,l))

    proof

      defpred P[ Nat] means for L be Z_Lattice, l be Linear_Combination of L, v be Vector of L st ( card ( Carrier l)) = $1 holds <;v, ( Sum l);> = ( SumSc (v,l));

      

       A1: P[ 0 ]

      proof

        let L be Z_Lattice, l be Linear_Combination of L, v be Vector of L such that

         B1: ( card ( Carrier l)) = 0 ;

        

         B2: ( Carrier l) = {} by B1;

        then ( Sum l) = ( 0. L) by VECTSP_6: 19;

        then <;v, ( Sum l);> = ( 0. F_Real ) by ZMODLAT1: 12;

        hence thesis by B2, LmSumSc13;

      end;

      

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

      proof

        let n be Nat such that

         B1: P[n];

        let L be Z_Lattice, l be Linear_Combination of L, v be Vector of L such that

         B2: ( card ( Carrier l)) = (n + 1);

        ( Carrier l) <> {} by B2;

        then

        consider u be object such that

         B3: u in ( Carrier l) by XBOOLE_0:def 1;

        reconsider u as Element of L by B3;

        

         B4: ( card (( Carrier l) \ {u})) = (( card ( Carrier l)) - ( card {u})) by B3, CARD_2: 44, ZFMISC_1: 31

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

        .= n;

        

         B5: ( Carrier l) = ((( Carrier l) \ {u}) \/ {u}) by B3, XBOOLE_1: 45, ZFMISC_1: 31;

        

         B6: ((( Carrier l) \ {u}) /\ {u}) = {} by XBOOLE_0:def 7, XBOOLE_1: 79;

        l is Linear_Combination of ( Carrier l) by VECTSP_6: 7;

        then

        consider l1 be Linear_Combination of (( Carrier l) \ {u}), l2 be Linear_Combination of {u} such that

         B7: l = (l1 + l2) by B5, B6, ZMODUL04: 26;

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

        then

         B8: <;v, ( Sum l);> = ( <;v, ( Sum l1);> + <;v, ( Sum l2);>) by ZMODLAT1: 8;

        

         B9: ( SumSc (v,l)) = (( SumSc (v,l1)) + ( SumSc (v,l2))) by B7, LmSumSc1X;

        for x be Vector of L st x in (( Carrier l) \ {u}) holds x in ( Carrier l1)

        proof

          let x be Vector of L such that

           C1: x in (( Carrier l) \ {u});

          x in ( Carrier l) by C1, XBOOLE_0:def 5;

          then

           C2: (l . x) <> ( 0. INT.Ring ) by VECTSP_6: 2;

          

           C3: ( Carrier l2) c= {u} by VECTSP_6:def 4;

          

           C4: (l . x) = ((l1 . x) + (l2 . x)) by B7, VECTSP_6: 22;

           not x in ( Carrier l2) by C1, C3, XBOOLE_0:def 5;

          then (l1 . x) <> ( 0. INT.Ring ) by C2, C4;

          hence thesis;

        end;

        then (( Carrier l) \ {u}) c= ( Carrier l1);

        then

         B10: ( Carrier l1) = (( Carrier l) \ {u}) by VECTSP_6:def 4;

        ( SumSc (v,l2)) = <;v, ((l2 . u) * u);> by LmSumSc14

        .= <;v, ( Sum l2);> by VECTSP_6: 17;

        hence thesis by B1, B4, B8, B9, B10;

      end;

      

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

      let L be Z_Lattice, l be Linear_Combination of L, v be Vector of L;

      reconsider n = ( card ( Carrier l)) as Nat;

       P[n] by A3;

      hence thesis;

    end;

    definition

      let L be Z_Lattice;

      let F be FinSequence of ( DivisibleMod L);

      let f be Function of ( DivisibleMod L), INT.Ring ;

      let v be Vector of ( DivisibleMod L);

      :: ZMODLAT3:def3

      func ScFS (v,f,F) -> FinSequence of F_Real means

      : defScFSDM: ( len it ) = ( len F) & for i be Nat st i in ( dom it ) holds (it . i) = (( ScProductDM L) . (v,((f . (F /. i)) * (F /. i))));

      existence

      proof

        deffunc X( object) = (( ScProductDM L) . (v,((f . (F /. $1)) * (F /. $1))));

        consider G be FinSequence such that

         A1: ( len G) = ( len F) & for i be Nat st i in ( dom G) holds (G . i) = X(i) from FINSEQ_1:sch 2;

        ( rng G) c= the carrier of F_Real

        proof

          let x be object such that

           B1: x in ( rng G);

          consider z be object such that

           B2: z in ( dom G) & x = (G . z) by B1, FUNCT_1:def 3;

          x = (( ScProductDM L) . (v,((f . (F /. z)) * (F /. z)))) by A1, B2;

          hence thesis;

        end;

        then

        reconsider G as FinSequence of F_Real by FINSEQ_1:def 4;

        take G;

        thus thesis by A1;

      end;

      uniqueness

      proof

        let f1,f2 be FinSequence of F_Real ;

        assume

         AS1: ( len f1) = ( len F) & for i be Nat st i in ( dom f1) holds (f1 . i) = (( ScProductDM L) . (v,((f . (F /. i)) * (F /. i))));

        assume

         AS2: ( len f2) = ( len F) & for i be Nat st i in ( dom f2) holds (f2 . i) = (( ScProductDM L) . (v,((f . (F /. i)) * (F /. i))));

        

         A2: ( dom f1) = ( dom f2) by AS1, AS2, FINSEQ_3: 29;

        for k be Nat st k in ( dom f1) holds (f1 . k) = (f2 . k)

        proof

          let k be Nat;

          assume

           B1: k in ( dom f1);

          

          hence (f1 . k) = (( ScProductDM L) . (v,((f . (F /. k)) * (F /. k)))) by AS1

          .= (f2 . k) by AS2, A2, B1;

        end;

        hence thesis by AS1, AS2, FINSEQ_3: 29;

      end;

    end

    theorem :: ZMODLAT3:11

    

     ThScFSDM1: for L be Z_Lattice, f be Function of ( DivisibleMod L), INT.Ring , F be FinSequence of ( DivisibleMod L), v,u be Vector of ( DivisibleMod L), i be Nat st i in ( dom F) & u = (F . i) holds (( ScFS (v,f,F)) . i) = (( ScProductDM L) . (v,((f . u) * u)))

    proof

      let L be Z_Lattice, f be Function of ( DivisibleMod L), INT.Ring , F be FinSequence of ( DivisibleMod L), v,u be Vector of ( DivisibleMod L), i be Nat such that

       A1: i in ( dom F) & u = (F . i);

      

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

      ( len ( ScFS (v,f,F))) = ( len F) by defScFSDM;

      then i in ( dom ( ScFS (v,f,F))) by A1, FINSEQ_3: 29;

      hence thesis by A1, A2, defScFSDM;

    end;

    theorem :: ZMODLAT3:12

    

     ThScFSDM3: for L be Z_Lattice, f be Function of ( DivisibleMod L), INT.Ring , v,u be Vector of ( DivisibleMod L) holds ( ScFS (v,f, <*u*>)) = <*(( ScProductDM L) . (v,((f . u) * u)))*>

    proof

      let L be Z_Lattice, f be Function of ( DivisibleMod L), INT.Ring ;

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

      

       A1: 1 in {1} by TARSKI:def 1;

      

       A2: ( len ( ScFS (v,f, <*u*>))) = ( len <*u*>) by defScFSDM

      .= 1 by FINSEQ_1: 40;

      then ( dom ( ScFS (v,f, <*u*>))) = {1} by FINSEQ_1: 2, FINSEQ_1:def 3;

      

      then (( ScFS (v,f, <*u*>)) . 1) = (( ScProductDM L) . (v,((f . ( <*u*> /. 1)) * ( <*u*> /. 1)))) by A1, defScFSDM

      .= (( ScProductDM L) . (v,((f . ( <*u*> /. 1)) * u))) by FINSEQ_4: 16

      .= (( ScProductDM L) . (v,((f . u) * u))) by FINSEQ_4: 16;

      hence thesis by A2, FINSEQ_1: 40;

    end;

    theorem :: ZMODLAT3:13

    

     ThScFSDM6: for L be Z_Lattice, f be Function of ( DivisibleMod L), INT.Ring , F,G be FinSequence of ( DivisibleMod L), v be Vector of ( DivisibleMod L) holds ( ScFS (v,f,(F ^ G))) = (( ScFS (v,f,F)) ^ ( ScFS (v,f,G)))

    proof

      let L be Z_Lattice, f be Function of ( DivisibleMod L), INT.Ring , F,G be FinSequence of ( DivisibleMod L), v be Vector of ( DivisibleMod L);

      set H = (( ScFS (v,f,F)) ^ ( ScFS (v,f,G)));

      set I = (F ^ G);

      

       A1: ( len F) = ( len ( ScFS (v,f,F))) by defScFSDM;

      

       A2: ( len H) = (( len ( ScFS (v,f,F))) + ( len ( ScFS (v,f,G)))) by FINSEQ_1: 22

      .= (( len F) + ( len ( ScFS (v,f,G)))) by defScFSDM

      .= (( len F) + ( len G)) by defScFSDM

      .= ( len I) by FINSEQ_1: 22;

      

       A3: ( len G) = ( len ( ScFS (v,f,G))) by defScFSDM;

      now

        let k be Nat;

        assume

         A4: k in ( dom H);

        per cases by FINSEQ_1: 25;

          suppose

           A5: k in ( dom ( ScFS (v,f,F)));

          then

           A6: k in ( dom F) by A1, FINSEQ_3: 29;

          then

           A7: k in ( dom (F ^ G)) by FINSEQ_3: 22;

          

           A8: (F /. k) = (F . k) by A6, PARTFUN1:def 6

          .= ((F ^ G) . k) by A6, FINSEQ_1:def 7

          .= ((F ^ G) /. k) by A7, PARTFUN1:def 6;

          

          thus (H . k) = (( ScFS (v,f,F)) . k) by A5, FINSEQ_1:def 7

          .= (( ScProductDM L) . (v,((f . (I /. k)) * (I /. k)))) by A5, A8, defScFSDM;

        end;

          suppose

           A9: ex n be Nat st n in ( dom ( ScFS (v,f,G))) & k = (( len ( ScFS (v,f,F))) + n);

          

           A10: k in ( dom I) by A2, A4, FINSEQ_3: 29;

          consider n be Nat such that

           A11: n in ( dom ( ScFS (v,f,G))) and

           A12: k = (( len ( ScFS (v,f,F))) + n) by A9;

          

           A13: n in ( dom G) by A3, A11, FINSEQ_3: 29;

          

          then

           A14: (G /. n) = (G . n) by PARTFUN1:def 6

          .= ((F ^ G) . k) by A1, A12, A13, FINSEQ_1:def 7

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

          

          thus (H . k) = (( ScFS (v,f,G)) . n) by A11, A12, FINSEQ_1:def 7

          .= (( ScProductDM L) . (v,((f . (I /. k)) * (I /. k)))) by A11, A14, defScFSDM;

        end;

      end;

      hence thesis by A2, defScFSDM;

    end;

    definition

      let L be Z_Lattice;

      let l be Linear_Combination of ( DivisibleMod L);

      let v be Vector of ( DivisibleMod L);

      :: ZMODLAT3:def4

      func SumSc (v,l) -> Element of F_Real means

      : defSumScDM: ex F be FinSequence of ( DivisibleMod L) st F is one-to-one & ( rng F) = ( Carrier l) & it = ( Sum ( ScFS (v,l,F)));

      existence

      proof

        consider F be FinSequence such that

         A1: ( rng F) = ( Carrier l) & F is one-to-one by FINSEQ_4: 58;

        reconsider F as FinSequence of ( DivisibleMod L) by A1, FINSEQ_1:def 4;

        take ( Sum ( ScFS (v,l,F))), F;

        thus thesis by A1;

      end;

      uniqueness

      proof

        let r1,r2 be Element of F_Real ;

        given F1 be FinSequence of ( DivisibleMod L) such that

         A1: F1 is one-to-one and

         A2: ( rng F1) = ( Carrier l) and

         A3: r1 = ( Sum ( ScFS (v,l,F1)));

        given F2 be FinSequence of ( DivisibleMod L) such that

         A4: F2 is one-to-one and

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

         A6: r2 = ( Sum ( ScFS (v,l,F2)));

        deffunc F( object) = ((F1 " ) . (F2 . $1));

        

         A7: ( len F1) = ( len F2) by A1, A2, A4, A5, FINSEQ_1: 48;

        then

         A8: ( dom F1) = ( dom F2) by FINSEQ_3: 29;

        

         A9: for x be object st x in ( dom F1) holds F(x) in ( dom F1)

        proof

          let x be object;

          assume x in ( dom F1);

          then (F2 . x) in ( rng F1) by A2, A5, A8, FUNCT_1: 3;

          then (F2 . x) in ( dom (F1 " )) by A1, FUNCT_1: 33;

          then ((F1 " ) . (F2 . x)) in ( rng (F1 " )) by FUNCT_1: 3;

          hence thesis by A1, FUNCT_1: 33;

        end;

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

         A10: for x be object st x in ( dom F1) holds (f . x) = F(x) from FUNCT_2:sch 2( A9);

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

        proof

          let x1,x2 be object such that

           B1: x1 in ( dom f) & x2 in ( dom f) & (f . x1) = (f . x2);

          (F2 . x1) in ( rng F1) by A2, A5, A8, B1, FUNCT_1: 3;

          then

           B4: (F2 . x1) in ( dom (F1 " )) by A1, FUNCT_1: 33;

          (F2 . x2) in ( rng F1) by A2, A5, A8, B1, FUNCT_1: 3;

          then

           B7: (F2 . x2) in ( dom (F1 " )) by A1, FUNCT_1: 33;

          ((F1 " ) . (F2 . x1)) = (f . x1) by A10, B1

          .= ((F1 " ) . (F2 . x2)) by A10, B1;

          then (F2 . x1) = (F2 . x2) by A1, B4, B7, FUNCT_1:def 4;

          hence thesis by A4, A8, B1;

        end;

        then

         A11: f is one-to-one;

        ( dom F1) c= ( rng f)

        proof

          let y be object such that

           B1: y in ( dom F1);

          (F1 . y) in ( rng F2) by A2, A5, B1, FUNCT_1: 3;

          then

          consider x be object such that

           B2: x in ( dom F2) & (F2 . x) = (F1 . y) by FUNCT_1:def 3;

          

           B3: (f . x) = ((F1 " ) . (F2 . x)) by A8, A10, B2

          .= y by A1, B1, B2, FUNCT_1: 34;

          x in ( dom f) by A8, B2, FUNCT_2:def 1;

          hence thesis by B3, FUNCT_1: 3;

        end;

        then

         A12: ( rng f) = ( dom F1);

        then

        reconsider f as Permutation of ( dom F1) by A11, FUNCT_2: 57;

        reconsider G1 = ( ScFS (v,l,F1)) as FinSequence of F_Real ;

        set G2 = ( ScFS (v,l,F2));

        

         A14: ( len G2) = ( len F2) by defScFSDM;

        

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

        .= ( Seg ( len G1)) by defScFSDM

        .= ( dom G1) by FINSEQ_1:def 3;

        then

        reconsider f as Permutation of ( dom G1);

        

         A16: ( len G1) = ( len F2) by A7, defScFSDM

        .= ( len G2) by defScFSDM;

        for i be Nat st i in ( dom G2) holds (G2 . i) = (G1 . (f . i))

        proof

          let i be Nat such that

           B1: i in ( dom G2);

          

           B2: (G2 . i) = (( ScProductDM L) . (v,((l . (F2 /. i)) * (F2 /. i)))) by B1, defScFSDM;

          

           B3: i in ( dom F2) by A14, B1, FINSEQ_3: 29;

          then

          reconsider u = (F2 . i) as Element of ( DivisibleMod L) by FINSEQ_2: 11;

          

           B4: i in ( dom f) by A8, B3, FUNCT_2:def 1;

          then (f . i) in ( dom F1) by A12, FUNCT_1: 3;

          then

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

          reconsider w = (F1 . m) as Element of ( DivisibleMod L) by A12, B4, FINSEQ_2: 11, FUNCT_1: 3;

          

           B5: (F2 . i) in ( rng F1) by A2, A5, B3, FUNCT_1: 3;

          

           B6: (F1 . (f . i)) = (F1 . ((F1 " ) . (F2 . i))) by A8, A10, B3

          .= (F2 . i) by A1, B5, FUNCT_1: 35;

          (F1 . m) = (F1 /. m) & (F2 . i) = (F2 /. i) by A12, B3, B4, FUNCT_1: 3, PARTFUN1:def 6;

          hence (G2 . i) = (G1 . (f . i)) by A12, A15, B2, B4, B6, defScFSDM, FUNCT_1: 3;

        end;

        hence thesis by A3, A6, A16, RLVECT_2: 6;

      end;

    end

    theorem :: ZMODLAT3:14

    

     LmSumScDM11: for L be Z_Lattice, v be Vector of ( DivisibleMod L) holds ( SumSc (v,( ZeroLC ( DivisibleMod L)))) = ( 0. F_Real )

    proof

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

      consider F be FinSequence of ( DivisibleMod L) such that

       A1: F is one-to-one & ( rng F) = ( Carrier ( ZeroLC ( DivisibleMod L))) & ( SumSc (v,( ZeroLC ( DivisibleMod L)))) = ( Sum ( ScFS (v,( ZeroLC ( DivisibleMod L)),F))) by defSumScDM;

      F = {} by A1, VECTSP_6:def 3;

      then ( len ( ScFS (v,( ZeroLC ( DivisibleMod L)),F))) = 0 by defScFSDM;

      hence thesis by A1, RLVECT_1: 75;

    end;

    theorem :: ZMODLAT3:15

    for L be Z_Lattice, v be Vector of ( DivisibleMod L), l be Linear_Combination of ( {} the carrier of ( DivisibleMod L)) holds ( SumSc (v,l)) = ( 0. F_Real )

    proof

      let L be Z_Lattice, v be Vector of ( DivisibleMod L), l be Linear_Combination of ( {} the carrier of ( DivisibleMod L));

      l = ( ZeroLC ( DivisibleMod L)) by VECTSP_6: 6;

      hence thesis by LmSumScDM11;

    end;

    theorem :: ZMODLAT3:16

    

     LmSumScDM13: for L be Z_Lattice, v be Vector of ( DivisibleMod L), l be Linear_Combination of ( DivisibleMod L) st ( Carrier l) = {} holds ( SumSc (v,l)) = ( 0. F_Real )

    proof

      let L be Z_Lattice, v be Vector of ( DivisibleMod L), l be Linear_Combination of ( DivisibleMod L) such that

       A1: ( Carrier l) = {} ;

      l = ( ZeroLC ( DivisibleMod L)) by A1, VECTSP_6:def 3;

      hence thesis by LmSumScDM11;

    end;

    theorem :: ZMODLAT3:17

    

     LmSumScDM14: for L be Z_Lattice, v,u be Vector of ( DivisibleMod L), l be Linear_Combination of {u} holds ( SumSc (v,l)) = (( ScProductDM L) . (v,((l . u) * u)))

    proof

      let L be Z_Lattice, v,u be Vector of ( DivisibleMod L), l be Linear_Combination of {u};

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

        suppose ( Carrier l) = {} ;

        then

         A2: l = ( ZeroLC ( DivisibleMod L)) by VECTSP_6:def 3;

        

        hence ( SumSc (v,l)) = ( 0. F_Real ) by LmSumScDM11

        .= (( ScProductDM L) . (v,( 0. ( DivisibleMod L)))) by ZMODLAT2: 14

        .= (( ScProductDM L) . (v,(( 0. INT.Ring ) * u))) by VECTSP_1: 14

        .= (( ScProductDM L) . (v,((l . u) * u))) by A2, VECTSP_6: 3;

      end;

        suppose ( Carrier l) = {u};

        then

        consider F be FinSequence of ( DivisibleMod L) such that

         A3: F is one-to-one & ( rng F) = {u} & ( SumSc (v,l)) = ( Sum ( ScFS (v,l,F))) by defSumScDM;

        F = <*u*> by A3, FINSEQ_3: 97;

        then ( ScFS (v,l,F)) = <*(( ScProductDM L) . (v,((l . u) * u)))*> by ThScFSDM3;

        hence thesis by A3, RLVECT_1: 44;

      end;

    end;

    theorem :: ZMODLAT3:18

    

     LmSumScDM1X: for L be Z_Lattice, v be Vector of ( DivisibleMod L), l1,l2 be Linear_Combination of ( DivisibleMod L) holds ( SumSc (v,(l1 + l2))) = (( SumSc (v,l1)) + ( SumSc (v,l2)))

    proof

      let L be Z_Lattice, w be Vector of ( DivisibleMod L), l1,l2 be Linear_Combination of ( DivisibleMod L);

      set A = ((( Carrier (l1 + l2)) \/ ( Carrier l1)) \/ ( Carrier l2));

      set C1 = (A \ ( Carrier l1));

      consider p be FinSequence such that

       A1: ( rng p) = C1 and

       A2: p is one-to-one by FINSEQ_4: 58;

      reconsider p as FinSequence of ( DivisibleMod L) by A1, FINSEQ_1:def 4;

      

       A3: A = (( Carrier l1) \/ (( Carrier (l1 + l2)) \/ ( Carrier l2))) by XBOOLE_1: 4;

      set C3 = (A \ ( Carrier (l1 + l2)));

      consider r be FinSequence such that

       A4: ( rng r) = C3 and

       A5: r is one-to-one by FINSEQ_4: 58;

      reconsider r as FinSequence of ( DivisibleMod L) by A4, FINSEQ_1:def 4;

      

       A6: A = (( Carrier (l1 + l2)) \/ (( Carrier l1) \/ ( Carrier l2))) by XBOOLE_1: 4;

      set C2 = (A \ ( Carrier l2));

      consider q be FinSequence such that

       A7: ( rng q) = C2 and

       A8: q is one-to-one by FINSEQ_4: 58;

      reconsider q as FinSequence of ( DivisibleMod L) by A7, FINSEQ_1:def 4;

      consider F be FinSequence of ( DivisibleMod L) such that

       A9: F is one-to-one and

       A10: ( rng F) = ( Carrier (l1 + l2)) and

       A11: ( SumSc (w,(l1 + l2))) = ( Sum ( ScFS (w,(l1 + l2),F))) by defSumScDM;

      set FF = (F ^ r);

      consider G be FinSequence of ( DivisibleMod L) such that

       A12: G is one-to-one and

       A13: ( rng G) = ( Carrier l1) and

       A14: ( SumSc (w,l1)) = ( Sum ( ScFS (w,l1,G))) by defSumScDM;

      ( rng FF) = (( rng F) \/ ( rng r)) by FINSEQ_1: 31;

      then ( rng FF) = (( Carrier (l1 + l2)) \/ A) by A10, A4, XBOOLE_1: 39;

      then

       A15: ( rng FF) = A by A6, XBOOLE_1: 7, XBOOLE_1: 12;

      set GG = (G ^ p);

      ( rng GG) = (( rng G) \/ ( rng p)) by FINSEQ_1: 31;

      then ( rng GG) = (( Carrier l1) \/ A) by A13, A1, XBOOLE_1: 39;

      then

       A16: ( rng GG) = A by A3, XBOOLE_1: 7, XBOOLE_1: 12;

      ( rng F) misses ( rng r)

      proof

        set x = the Element of (( rng F) /\ ( rng r));

        assume not thesis;

        then x in ( Carrier (l1 + l2)) & x in C3 by A10, A4, XBOOLE_0:def 4;

        hence thesis by XBOOLE_0:def 5;

      end;

      then

       A17: FF is one-to-one by A9, A5, FINSEQ_3: 91;

      ( rng G) misses ( rng p)

      proof

        set x = the Element of (( rng G) /\ ( rng p));

        assume not thesis;

        then x in ( Carrier l1) & x in C1 by A13, A1, XBOOLE_0:def 4;

        hence thesis by XBOOLE_0:def 5;

      end;

      then

       A18: GG is one-to-one by A12, A2, FINSEQ_3: 91;

      then

       A19: ( len GG) = ( len FF) by A17, A16, A15, FINSEQ_1: 48;

      deffunc F( Nat) = (FF <- (GG . $1));

      consider P be FinSequence such that

       A20: ( len P) = ( len FF) and

       A21: for k be Nat st k in ( dom P) holds (P . k) = F(k) from FINSEQ_1:sch 2;

      

       A22: ( dom P) = ( Seg ( len FF)) by A20, FINSEQ_1:def 3;

       A23:

      now

        let x be object;

        assume

         A24: x in ( dom GG);

        then

        reconsider n = x as Element of NAT ;

        (GG . n) in ( rng FF) by A16, A15, A24, FUNCT_1:def 3;

        then

         A25: FF just_once_values (GG . n) by A17, FINSEQ_4: 8;

        n in ( Seg ( len FF)) by A19, A24, FINSEQ_1:def 3;

        

        then (FF . (P . n)) = (FF . (FF <- (GG . n))) by A21, A22

        .= (GG . n) by A25, FINSEQ_4:def 3;

        hence (GG . x) = (FF . (P . x));

      end;

      

       A26: ( rng P) c= ( dom FF)

      proof

        let x be object;

        assume x in ( rng P);

        then

        consider y be object such that

         A27: y in ( dom P) and

         A28: (P . y) = x by FUNCT_1:def 3;

        reconsider y as Element of NAT by A27;

        y in ( dom GG) by A19, A20, A27, FINSEQ_3: 29;

        then (GG . y) in ( rng FF) by A16, A15, FUNCT_1:def 3;

        then

         A29: FF just_once_values (GG . y) by A17, FINSEQ_4: 8;

        (P . y) = (FF <- (GG . y)) by A21, A27;

        hence thesis by A28, A29, FINSEQ_4:def 3;

      end;

      now

        let x be object;

        thus x in ( dom GG) implies x in ( dom P) & (P . x) in ( dom FF)

        proof

          assume x in ( dom GG);

          then x in ( Seg ( len P)) by A19, A20, FINSEQ_1:def 3;

          hence x in ( dom P) by FINSEQ_1:def 3;

          then (P . x) in ( rng P) by FUNCT_1:def 3;

          hence thesis by A26;

        end;

        assume that

         A30: x in ( dom P) and (P . x) in ( dom FF);

        x in ( Seg ( len P)) by A30, FINSEQ_1:def 3;

        hence x in ( dom GG) by A19, A20, FINSEQ_1:def 3;

      end;

      then

       A31: GG = (FF * P) by A23, FUNCT_1: 10;

      ( dom FF) c= ( rng P)

      proof

        set f = ((FF " ) * GG);

        let x be object;

        assume

         A32: x in ( dom FF);

        ( dom (FF " )) = ( rng GG) by A17, A16, A15, FUNCT_1: 33;

        

        then

         A33: ( rng f) = ( rng (FF " )) by RELAT_1: 28

        .= ( dom FF) by A17, FUNCT_1: 33;

        f = (((FF " ) * FF) * P) by A31, RELAT_1: 36

        .= (( id ( dom FF)) * P) by A17, FUNCT_1: 39

        .= P by A26, RELAT_1: 53;

        hence thesis by A32, A33;

      end;

      then

       A34: ( dom FF) = ( rng P) by A26;

      

       A35: ( len r) = ( len ( ScFS (w,(l1 + l2),r))) by defScFSDM;

      

       B1: ( dom r) = ( Seg ( len r)) by FINSEQ_1:def 3

      .= ( Seg ( len ( ScFS (w,(l1 + l2),r)))) by defScFSDM

      .= ( dom ( ScFS (w,(l1 + l2),r))) by FINSEQ_1:def 3;

      now

        let k be Nat;

        assume

         A36: k in ( dom ( ScFS (w,(l1 + l2),r)));

        then (r /. k) = (r . k) by B1, PARTFUN1:def 6;

        then (r /. k) in C3 by A4, A36, B1, FUNCT_1:def 3;

        then

         A37: not (r /. k) in ( Carrier (l1 + l2)) by XBOOLE_0:def 5;

        (( ScFS (w,(l1 + l2),r)) . k) = (( ScProductDM L) . (w,(((l1 + l2) . (r /. k)) * (r /. k)))) by A36, defScFSDM;

        

        then (( ScFS (w,(l1 + l2),r)) . k) = (( ScProductDM L) . (w,(( 0. INT.Ring ) * (r /. k)))) by A37

        .= (( ScProductDM L) . (w,( 0. ( DivisibleMod L)))) by VECTSP_1: 14

        .= ( 0. F_Real ) by ZMODLAT2: 14;

        

        hence (( ScFS (w,(l1 + l2),r)) . k) = ( - (( ScFS (w,(l1 + l2),r)) . k))

        .= ( - (( ScFS (w,(l1 + l2),r)) /. k)) by A36, PARTFUN1:def 6;

      end;

      then

       A38: ( Sum ( ScFS (w,(l1 + l2),r))) = ( - ( Sum ( ScFS (w,(l1 + l2),r)))) by A35, RLVECT_2: 4;

      

       A39: ( len p) = ( len ( ScFS (w,l1,p))) by defScFSDM;

      

       B1: ( dom p) = ( Seg ( len p)) by FINSEQ_1:def 3

      .= ( Seg ( len ( ScFS (w,l1,p)))) by defScFSDM

      .= ( dom ( ScFS (w,l1,p))) by FINSEQ_1:def 3;

      now

        let k be Nat;

        assume

         A40: k in ( dom ( ScFS (w,l1,p)));

        then (p /. k) = (p . k) by B1, PARTFUN1:def 6;

        then (p /. k) in C1 by A1, A40, B1, FUNCT_1:def 3;

        then

         A41: not (p /. k) in ( Carrier l1) by XBOOLE_0:def 5;

        (( ScFS (w,l1,p)) . k) = (( ScProductDM L) . (w,((l1 . (p /. k)) * (p /. k)))) by A40, defScFSDM;

        

        then (( ScFS (w,l1,p)) . k) = (( ScProductDM L) . (w,(( 0. INT.Ring ) * (p /. k)))) by A41

        .= (( ScProductDM L) . (w,( 0. ( DivisibleMod L)))) by VECTSP_1: 14

        .= ( 0. F_Real ) by ZMODLAT2: 14;

        

        hence (( ScFS (w,l1,p)) . k) = ( - (( ScFS (w,l1,p)) . k))

        .= ( - (( ScFS (w,l1,p)) /. k)) by A40, PARTFUN1:def 6;

      end;

      then

       A42: ( Sum ( ScFS (w,l1,p))) = ( - ( Sum ( ScFS (w,l1,p)))) by A39, RLVECT_2: 4;

      

       A43: ( len q) = ( len ( ScFS (w,l2,q))) by defScFSDM;

      then

       B1: ( dom q) = ( dom ( ScFS (w,l2,q))) by FINSEQ_3: 29;

      now

        let k be Nat;

        assume

         A44: k in ( dom ( ScFS (w,l2,q)));

        then (q /. k) = (q . k) by B1, PARTFUN1:def 6;

        then (q /. k) in C2 by A7, A44, B1, FUNCT_1:def 3;

        then

         A45: not (q /. k) in ( Carrier l2) by XBOOLE_0:def 5;

        (( ScFS (w,l2,q)) . k) = (( ScProductDM L) . (w,((l2 . (q /. k)) * (q /. k)))) by A44, defScFSDM;

        

        then (( ScFS (w,l2,q)) . k) = (( ScProductDM L) . (w,(( 0. INT.Ring ) * (q /. k)))) by A45

        .= (( ScProductDM L) . (w,( 0. ( DivisibleMod L)))) by VECTSP_1: 14

        .= ( 0. F_Real ) by ZMODLAT2: 14;

        

        hence (( ScFS (w,l2,q)) . k) = ( - (( ScFS (w,l2,q)) . k))

        .= ( - (( ScFS (w,l2,q)) /. k)) by A44, PARTFUN1:def 6;

      end;

      then

       A46: ( Sum ( ScFS (w,l2,q))) = ( - ( Sum ( ScFS (w,l2,q)))) by A43, RLVECT_2: 4;

      set g = ( ScFS (w,l1,GG));

      

       A47: ( len g) = ( len GG) by defScFSDM;

      then

       A48: ( Seg ( len GG)) = ( dom g) by FINSEQ_1:def 3;

      set f = ( ScFS (w,(l1 + l2),FF));

      consider H be FinSequence of ( DivisibleMod L) such that

       A49: H is one-to-one and

       A50: ( rng H) = ( Carrier l2) and

       A51: ( Sum ( ScFS (w,l2,H))) = ( SumSc (w,l2)) by defSumScDM;

      set HH = (H ^ q);

      ( rng H) misses ( rng q)

      proof

        set x = the Element of (( rng H) /\ ( rng q));

        assume not thesis;

        then x in ( Carrier l2) & x in C2 by A50, A7, XBOOLE_0:def 4;

        hence thesis by XBOOLE_0:def 5;

      end;

      then

       A52: HH is one-to-one by A49, A8, FINSEQ_3: 91;

      ( rng HH) = (( rng H) \/ ( rng q)) by FINSEQ_1: 31;

      then ( rng HH) = (( Carrier l2) \/ A) by A50, A7, XBOOLE_1: 39;

      then

       A53: ( rng HH) = A by XBOOLE_1: 7, XBOOLE_1: 12;

      then

       A54: ( len GG) = ( len HH) by A52, A18, A16, FINSEQ_1: 48;

      then

       B1: ( dom GG) = ( dom HH) by FINSEQ_3: 29;

      deffunc F( Nat) = (HH <- (GG . $1));

      consider R be FinSequence such that

       A55: ( len R) = ( len HH) and

       A56: for k be Nat st k in ( dom R) holds (R . k) = F(k) from FINSEQ_1:sch 2;

      

       A57: ( dom R) = ( dom HH) by A55, FINSEQ_3: 29;

       A58:

      now

        let x be object;

        assume

         A59: x in ( dom GG);

        then

        reconsider n = x as Element of NAT ;

        (GG . n) in ( rng HH) by A16, A53, A59, FUNCT_1:def 3;

        then

         A60: HH just_once_values (GG . n) by A52, FINSEQ_4: 8;

        (HH . (R . n)) = (HH . (HH <- (GG . n))) by A56, A57, B1, A59

        .= (GG . n) by A60, FINSEQ_4:def 3;

        hence (GG . x) = (HH . (R . x));

      end;

      

       A61: ( rng R) c= ( dom HH)

      proof

        let x be object;

        assume x in ( rng R);

        then

        consider y be object such that

         A62: y in ( dom R) and

         A63: (R . y) = x by FUNCT_1:def 3;

        reconsider y as Element of NAT by A62;

        y in ( dom GG) by A54, A55, A62, FINSEQ_3: 29;

        then (GG . y) in ( rng HH) by A16, A53, FUNCT_1:def 3;

        then

         A64: HH just_once_values (GG . y) by A52, FINSEQ_4: 8;

        (R . y) = (HH <- (GG . y)) by A56, A62;

        hence thesis by A63, A64, FINSEQ_4:def 3;

      end;

      now

        let x be object;

        thus x in ( dom GG) implies x in ( dom R) & (R . x) in ( dom HH)

        proof

          assume x in ( dom GG);

          hence x in ( dom R) by A55, FINSEQ_3: 29, A54;

          then (R . x) in ( rng R) by FUNCT_1:def 3;

          hence thesis by A61;

        end;

        assume x in ( dom R) & (R . x) in ( dom HH);

        hence x in ( dom GG) by A54, A55, FINSEQ_3: 29;

      end;

      then

       A66: GG = (HH * R) by A58, FUNCT_1: 10;

      ( dom HH) c= ( rng R)

      proof

        set f = ((HH " ) * GG);

        let x be object;

        assume

         A67: x in ( dom HH);

        ( dom (HH " )) = ( rng GG) by A52, A16, A53, FUNCT_1: 33;

        

        then

         A68: ( rng f) = ( rng (HH " )) by RELAT_1: 28

        .= ( dom HH) by A52, FUNCT_1: 33;

        f = (((HH " ) * HH) * R) by A66, RELAT_1: 36

        .= (( id ( dom HH)) * R) by A52, FUNCT_1: 39

        .= R by A61, RELAT_1: 53;

        hence thesis by A67, A68;

      end;

      then

       A69: ( dom HH) = ( rng R) by A61;

      set h = ( ScFS (w,l2,HH));

      

       A70: ( Sum h) = ( Sum (( ScFS (w,l2,H)) ^ ( ScFS (w,l2,q)))) by ThScFSDM6

      .= (( Sum ( ScFS (w,l2,H))) + ( 0. F_Real )) by A46, RLVECT_1: 41

      .= ( Sum ( ScFS (w,l2,H)));

      

       A71: ( Sum g) = ( Sum (( ScFS (w,l1,G)) ^ ( ScFS (w,l1,p)))) by ThScFSDM6

      .= (( Sum ( ScFS (w,l1,G))) + ( 0. F_Real )) by A42, RLVECT_1: 41

      .= ( Sum ( ScFS (w,l1,G)));

      

       A72: ( dom P) = ( dom FF) by A20, FINSEQ_3: 29;

      

       A73: P is one-to-one by A20, A34, FINSEQ_3: 29, FINSEQ_4: 60;

      

       A74: ( dom R) = ( dom HH) by A55, FINSEQ_3: 29;

      

       A75: R is one-to-one by A55, A69, FINSEQ_3: 29, FINSEQ_4: 60;

      R is Function of ( dom HH), ( dom HH) by A61, A74, FUNCT_2: 2;

      then

      reconsider R as Permutation of ( dom HH) by A69, A75, FUNCT_2: 57;

      

       A76: ( len h) = ( len HH) by defScFSDM;

      then ( dom h) = ( dom HH) by FINSEQ_3: 29;

      then

      reconsider R as Permutation of ( dom h);

      reconsider Hp = (h * R) as FinSequence of F_Real by FINSEQ_2: 47;

      

       A77: ( len Hp) = ( len GG) by A54, A76, FINSEQ_2: 44;

      reconsider P as Function of ( dom FF), ( dom FF) by A26, A72, FUNCT_2: 2;

      reconsider P as Permutation of ( dom FF) by A34, A73, FUNCT_2: 57;

      

       A78: ( len f) = ( len FF) by defScFSDM;

      then ( dom f) = ( dom FF) by FINSEQ_3: 29;

      then

      reconsider P as Permutation of ( dom f);

      reconsider Fp = (f * P) as FinSequence of F_Real by FINSEQ_2: 47;

      

       A79: ( Sum f) = ( Sum (( ScFS (w,(l1 + l2),F)) ^ ( ScFS (w,(l1 + l2),r)))) by ThScFSDM6

      .= (( Sum ( ScFS (w,(l1 + l2),F))) + ( 0. F_Real )) by A38, RLVECT_1: 41

      .= ( Sum ( ScFS (w,(l1 + l2),F)));

      deffunc F( Nat) = ((g /. $1) + (Hp /. $1));

      consider I be FinSequence such that

       A80: ( len I) = ( len GG) and

       A81: for k be Nat st k in ( dom I) holds (I . k) = F(k) from FINSEQ_1:sch 2;

      

       A83: ( dom I) = ( Seg ( len GG)) by A80, FINSEQ_1:def 3;

      ( rng I) c= the carrier of F_Real

      proof

        let x be object;

        assume x in ( rng I);

        then

        consider y be object such that

         A84: y in ( dom I) and

         A85: (I . y) = x by FUNCT_1:def 3;

        reconsider y as Element of NAT by A84;

        (I . y) = ((g /. y) + (Hp /. y)) by A81, A84;

        hence thesis by A85;

      end;

      then

      reconsider I as FinSequence of F_Real by FINSEQ_1:def 4;

      

       A86: ( len Fp) = ( len I) by A19, A78, A80, FINSEQ_2: 44;

      then

       X1: ( dom I) = ( Seg ( len I)) & ( dom Fp) = ( Seg ( len I)) by FINSEQ_1:def 3;

      

       X2: ( dom Hp) = ( Seg ( len Hp)) by FINSEQ_1:def 3

      .= ( dom I) by A54, A76, A80, FINSEQ_1:def 3, FINSEQ_2: 44;

      

       X3: ( dom HH) = ( Seg ( len HH)) by FINSEQ_1:def 3

      .= ( dom I) by A18, A16, A52, A53, A80, FINSEQ_1: 48, FINSEQ_1:def 3;

      then

       X4: ( dom GG) = ( dom I) by A54, FINSEQ_3: 29;

      

       X5: ( dom g) = ( Seg ( len g)) by FINSEQ_1:def 3

      .= ( dom I) by A80, defScFSDM, FINSEQ_1:def 3;

       A87:

      now

        let k be Nat;

        assume

         A88: k in ( dom I);

        

        then

         A90: (Hp /. k) = ((h * R) . k) by X2, PARTFUN1:def 6

        .= (h . (R . k)) by A88, X2, FUNCT_1: 12;

        set v = (GG /. k);

        

         A91: (Fp . k) = (f . (P . k)) by A88, X1, FUNCT_1: 12;

        (R . k) in ( dom R) by A69, A74, A88, X3, FUNCT_1:def 3;

        then

        reconsider j = (R . k) as Element of NAT by FINSEQ_3: 23;

        

         A94: (HH . j) = (GG . k) by A58, A88, X3, B1

        .= (GG /. k) by A88, X3, B1, PARTFUN1:def 6;

        

         A95: ( dom FF) = ( dom GG) by A19, FINSEQ_3: 29;

        then (P . k) in ( dom P) by A34, A72, A88, X3, FUNCT_1:def 3, B1;

        then

        reconsider l = (P . k) as Element of NAT by FINSEQ_3: 23;

        

         A96: (FF . l) = (GG . k) by A23, A88, X3, B1

        .= (GG /. k) by A88, X3, B1, PARTFUN1:def 6;

        (R . k) in ( dom HH) by A69, A74, A88, X3, FUNCT_1:def 3;

        then

         A97: (h . j) = (( ScProductDM L) . (w,((l2 . v) * v))) by A94, ThScFSDM1;

        (P . k) in ( dom FF) by A34, A72, A88, A95, X4, FUNCT_1:def 3;

        

        then

         A98: (f . l) = (( ScProductDM L) . (w,(((l1 + l2) . v) * v))) by A96, ThScFSDM1

        .= (( ScProductDM L) . (w,(((l1 . v) + (l2 . v)) * v))) by VECTSP_6: 22

        .= (( ScProductDM L) . (w,(((l1 . v) * v) + ((l2 . v) * v)))) by VECTSP_1:def 15

        .= ((( ScProductDM L) . (w,((l1 . v) * v))) + (( ScProductDM L) . (w,((l2 . v) * v)))) by ZMODLAT2: 12;

        (g /. k) = (g . k) by A88, X5, PARTFUN1:def 6

        .= (( ScProductDM L) . (w,((l1 . v) * v))) by A88, X5, defScFSDM;

        hence (I . k) = (Fp . k) by A81, A88, A90, A97, A91, A98;

      end;

      ( dom I) = ( Seg ( len I)) & ( dom Fp) = ( Seg ( len I)) by A86, FINSEQ_1:def 3;

      then

       A100: I = Fp by A87;

      ( Sum Fp) = ( Sum f) & ( Sum Hp) = ( Sum h) by RLVECT_2: 7;

      hence thesis by A11, A14, A47, A48, A51, A71, A70, A77, A79, A80, A81, A83, A100, RLVECT_2: 2;

    end;

    theorem :: ZMODLAT3:19

    

     ThSumScDM1: for L be Z_Lattice, l be Linear_Combination of ( DivisibleMod L), v be Vector of ( DivisibleMod L) holds (( ScProductDM L) . (v,( Sum l))) = ( SumSc (v,l))

    proof

      defpred P[ Nat] means for L be Z_Lattice, l be Linear_Combination of ( DivisibleMod L), v be Vector of ( DivisibleMod L) st ( card ( Carrier l)) = $1 holds (( ScProductDM L) . (v,( Sum l))) = ( SumSc (v,l));

      

       A1: P[ 0 ]

      proof

        let L be Z_Lattice, l be Linear_Combination of ( DivisibleMod L), v be Vector of ( DivisibleMod L) such that

         B1: ( card ( Carrier l)) = 0 ;

        

         B2: ( Carrier l) = {} by B1;

        then ( Sum l) = ( 0. ( DivisibleMod L)) by VECTSP_6: 19;

        then (( ScProductDM L) . (v,( Sum l))) = ( 0. F_Real ) by ZMODLAT2: 14;

        hence thesis by B2, LmSumScDM13;

      end;

      

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

      proof

        let n be Nat such that

         B1: P[n];

        let L be Z_Lattice, l be Linear_Combination of ( DivisibleMod L), v be Vector of ( DivisibleMod L) such that

         B2: ( card ( Carrier l)) = (n + 1);

        ( Carrier l) <> {} by B2;

        then

        consider u be object such that

         B3: u in ( Carrier l) by XBOOLE_0:def 1;

        reconsider u as Element of ( DivisibleMod L) by B3;

        

         B4: ( card (( Carrier l) \ {u})) = (( card ( Carrier l)) - ( card {u})) by B3, CARD_2: 44, ZFMISC_1: 31

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

        .= n;

        

         B5: ( Carrier l) = ((( Carrier l) \ {u}) \/ {u}) by B3, XBOOLE_1: 45, ZFMISC_1: 31;

        

         B6: ((( Carrier l) \ {u}) /\ {u}) = {} by XBOOLE_0:def 7, XBOOLE_1: 79;

        l is Linear_Combination of ( Carrier l) by VECTSP_6: 7;

        then

        consider l1 be Linear_Combination of (( Carrier l) \ {u}), l2 be Linear_Combination of {u} such that

         B7: l = (l1 + l2) by B5, B6, ZMODUL04: 26;

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

        then

         B8: (( ScProductDM L) . (v,( Sum l))) = ((( ScProductDM L) . (v,( Sum l1))) + (( ScProductDM L) . (v,( Sum l2)))) by ZMODLAT2: 12;

        for x be Vector of ( DivisibleMod L) st x in (( Carrier l) \ {u}) holds x in ( Carrier l1)

        proof

          let x be Vector of ( DivisibleMod L) such that

           C1: x in (( Carrier l) \ {u});

          x in ( Carrier l) by C1, XBOOLE_0:def 5;

          then

           C2: (l . x) <> ( 0. INT.Ring ) by VECTSP_6: 2;

          

           C3: ( Carrier l2) c= {u} by VECTSP_6:def 4;

          

           C4: (l . x) = ((l1 . x) + (l2 . x)) by B7, VECTSP_6: 22;

           not x in ( Carrier l2) by C1, C3, XBOOLE_0:def 5;

          then (l1 . x) <> ( 0. INT.Ring ) by C2, C4;

          hence thesis;

        end;

        then (( Carrier l) \ {u}) c= ( Carrier l1);

        then ( Carrier l1) = (( Carrier l) \ {u}) by VECTSP_6:def 4;

        then

         B10: (( ScProductDM L) . (v,( Sum l1))) = ( SumSc (v,l1)) by B1, B4;

        ( SumSc (v,l2)) = (( ScProductDM L) . (v,((l2 . u) * u))) by LmSumScDM14

        .= (( ScProductDM L) . (v,( Sum l2))) by VECTSP_6: 17;

        hence thesis by B7, B8, B10, LmSumScDM1X;

      end;

      

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

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

      reconsider n = ( card ( Carrier l)) as Nat;

       P[n] by A3;

      hence thesis;

    end;

    theorem :: ZMODLAT3:20

    

     INVMN1: for n be Nat, M be Matrix of n, F_Real holds for H be Matrix of n, F_Rat st M = H & M is invertible holds H is invertible & (M ~ ) = (H ~ )

    proof

      let n be Nat;

      let M be Matrix of n, F_Real ;

      let H be Matrix of n, F_Rat ;

      assume

       AS: M = H & M is invertible;

      then

       N1: ( 0. F_Real ) <> ( Det M) by LAPLACE: 34;

      then

       P0: ( 0. F_Rat ) <> ( Det H) by AS, ZMODLAT2: 54;

      hence H is invertible by LAPLACE: 34;

      

       Q0: ( Indices M) = [:( Seg n), ( Seg n):] by MATRIX_0: 24;

      

       P1: ( len (M ~ )) = n by MATRIX_0: 24

      .= ( len (H ~ )) by MATRIX_0: 24;

      

       P2: ( width (M ~ )) = n by MATRIX_0: 24

      .= ( width (H ~ )) by MATRIX_0: 24;

      

       P3A: ( Indices (M ~ )) = [:( Seg n), ( Seg n):] by MATRIX_0: 24;

      

       P3B: ( Indices (H ~ )) = [:( Seg n), ( Seg n):] by MATRIX_0: 24;

      for i,j be Nat st [i, j] in ( Indices (M ~ )) holds ((M ~ ) * (i,j)) = ((H ~ ) * (i,j))

      proof

        let i,j be Nat;

        assume

         P01: [i, j] in ( Indices (M ~ ));

        then [i, j] in [:( Seg n), ( Seg n):] by MATRIX_0: 24;

        then i in ( Seg n) & j in ( Seg n) by ZFMISC_1: 87;

        then

         P02: [j, i] in ( Indices M) by Q0, ZFMISC_1: 87;

        set MM = ( Delete (M,j,i));

        set HH = ( Delete (H,j,i));

        MM = HH

        proof

          per cases ;

            suppose n <= 1;

            then (n - 1) <= (1 - 1) by XREAL_1: 9;

            then (n -' 1) = 0 by XREAL_0:def 2;

            hence MM = HH by MATRIX_0: 22;

          end;

            suppose

             NN21: n > 1;

            then

             NN2: (n - 1) > (1 - 1) by XREAL_1: 14;

            reconsider k = (n - 1) as Nat by NN21;

            n = (k + 1) & 0 < k by NN2;

            hence ( Delete (M,j,i)) = ( Delete (H,j,i)) by AS, P02, ZMODLAT2: 52;

          end;

        end;

        then

         S1: ((( power F_Real ) . (( - ( 1_ F_Real )),(i + j))) * ( Minor (M,j,i))) = ((( power F_Rat ) . (( - ( 1_ F_Rat )),(i + j))) * ( Minor (H,j,i))) by ZMODLAT2: 54, ZMODLAT2: 47;

        

        thus ((M ~ ) * (i,j)) = (((( Det M) " ) * (( power F_Real ) . (( - ( 1_ F_Real )),(i + j)))) * ( Minor (M,j,i))) by P01, LAPLACE: 36, AS

        .= ((( Det M) " ) * ((( power F_Real ) . (( - ( 1_ F_Real )),(i + j))) * ( Minor (M,j,i))))

        .= ((( Det H) " ) * ((( power F_Rat ) . (( - ( 1_ F_Rat )),(i + j))) * ( Minor (H,j,i)))) by AS, N1, S1, GAUSSINT: 14, GAUSSINT: 21, ZMODLAT2: 54

        .= (((( Det H) " ) * (( power F_Rat ) . (( - ( 1_ F_Rat )),(i + j)))) * ( Minor (H,j,i)))

        .= ((H ~ ) * (i,j)) by P01, P0, P3A, P3B, LAPLACE: 34, LAPLACE: 36;

      end;

      hence (M ~ ) = (H ~ ) by P1, P2, ZMATRLIN: 4;

    end;

    theorem :: ZMODLAT3:21

    

     INVMN2: for n be Nat, M be Matrix of n, F_Real st M is Matrix of n, F_Rat & M is invertible holds (M ~ ) is Matrix of n, F_Rat

    proof

      let n be Nat, M be Matrix of n, F_Real ;

      assume that

       A1: M is Matrix of n, F_Rat and

       A2: M is invertible;

      reconsider H = M as Matrix of n, F_Rat by A1;

      (M ~ ) = (H ~ ) by A2, INVMN1;

      hence (M ~ ) is Matrix of n, F_Rat ;

    end;

    theorem :: ZMODLAT3:22

    

     ThGM3: for L be non trivial RATional positive-definite Z_Lattice, b be OrdBasis of L holds (( GramMatrix b) ~ ) is Matrix of ( dim L), F_Rat

    proof

      let L be non trivial RATional positive-definite Z_Lattice, b be OrdBasis of L;

      ( GramMatrix b) is Matrix of ( dim L), F_Rat by ZMODLAT2: 45;

      hence thesis by INVMN2;

    end;

    theorem :: ZMODLAT3:23

    

     LmDE311A: for X be finite Subset of RAT holds ex a be Element of INT st a <> 0 & for r be Element of RAT st r in X holds (a * r) in INT

    proof

      defpred P[ Nat] means for X be finite Subset of RAT st ( card X) = $1 holds ex a be Element of INT st a <> 0 & for r be Element of RAT st r in X holds (a * r) in INT ;

      

       P1: P[ 0 ]

      proof

        let X be finite Subset of RAT ;

        assume

         AS: ( card X) = 0 ;

        reconsider a = 1 as Element of INT by NUMBERS: 17;

        take a;

        thus a <> 0 ;

        thus for r be Element of RAT st r in X holds (a * r) in INT by AS;

      end;

      

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

      proof

        let n be Nat;

        assume

         AS1: P[n];

        let X be finite Subset of RAT ;

        assume

         AS2: ( card X) = (n + 1);

        then X <> {} ;

        then

        consider x be object such that

         A1: x in X by XBOOLE_0:def 1;

        

         B6: {x} is Subset of X by A1, SUBSET_1: 41;

        set Y = (X \ {x});

        reconsider Y as finite Subset of RAT ;

        

         D1: X = (Y \/ {x}) by B6, XBOOLE_1: 45;

        ( card Y) = (( card X) - ( card {x})) by B6, CARD_2: 44

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

        .= n;

        then

        consider a0 be Element of INT such that

         A4: a0 <> 0 and

         A5: for r be Element of RAT st r in Y holds (a0 * r) in INT by AS1;

        reconsider x as Element of RAT by A1;

        consider x0,ib0 be Integer such that

         A6: ib0 <> 0 & x = (x0 / ib0) by RAT_1: 1;

        reconsider ia0 = a0 as Integer;

        set ia = (ia0 * ib0);

        reconsider a = ia as Element of INT by INT_1:def 2;

        for r be Element of RAT st r in X holds (a * r) in INT

        proof

          let r be Element of RAT ;

          assume r in X;

          per cases by D1, XBOOLE_0:def 3;

            suppose r in Y;

            then

            reconsider iar = (ia0 * r) as Integer by A5, INT_1:def 2;

            (a * r) = (ib0 * iar);

            hence (a * r) in INT by INT_1:def 2;

          end;

            suppose

             A72: r in {x};

            (a * r) = (ia0 * (ib0 * r))

            .= (ia0 * (ib0 * (x0 / ib0))) by A6, A72, TARSKI:def 1

            .= (ia0 * x0) by A6, XCMPLX_1: 87;

            hence (a * r) in INT by INT_1:def 2;

          end;

        end;

        hence thesis by A4, A6;

      end;

      

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

      let X be finite Subset of RAT ;

      ( card X) is Nat;

      hence ex a be Element of INT st a <> 0 & for r be Element of RAT st r in X holds (a * r) in INT by P3;

    end;

    theorem :: ZMODLAT3:24

    

     LmDE311: for L be non trivial RATional positive-definite Z_Lattice, b be OrdBasis of L holds ex a be Element of F_Real st a is Element of INT.Ring & a <> 0 & (a * (( GramMatrix b) ~ )) is Matrix of ( dim L), INT.Ring

    proof

      let L be non trivial RATional positive-definite Z_Lattice, b be OrdBasis of L;

      set G = (( GramMatrix b) ~ );

      reconsider M = G as Matrix of ( dim L), F_Rat by ThGM3;

      

       A2: ( rng M) c= (the carrier of F_Rat * );

      

       A5: ( len M) = ( dim L) & ( width M) = ( dim L) by MATRIX_0: 24;

      

       B1: for i,j be Nat st [i, j] in ( Indices G) holds (G * (i,j)) in the carrier of F_Rat

      proof

        let i,j be Nat;

        assume

         B10: [i, j] in ( Indices G);

        then

        consider p be FinSequence of F_Real such that

         B11: p = (G . i) & (G * (i,j)) = (p . j) by MATRIX_0:def 5;

        

         B12: i in ( dom G) & j in ( Seg ( width G)) by ZFMISC_1: 87, B10;

        then p in ( rng G) by B11, FUNCT_1: 3;

        then

         B14: ( len p) = ( width G) by A5, MATRIX_0:def 3;

        p in (the carrier of F_Rat * ) by A2, B11, B12, FUNCT_1: 3;

        then p is FinSequence of F_Rat by FINSEQ_1:def 11;

        then

         B15: ( rng p) c= the carrier of F_Rat by FINSEQ_1:def 4;

        j in ( dom p) by B12, B14, FINSEQ_1:def 3;

        hence (G * (i,j)) in the carrier of F_Rat by B11, B15, FUNCT_1: 3;

      end;

      deffunc F( Nat, Nat) = (G * ($1,$2));

      set Dn = { F(u,v) where u be Element of NAT , v be Element of NAT : u in ( Seg ( len G)) & v in ( Seg ( width G)) };

      

       F1: ( Seg ( len G)) is finite;

      

       F2: ( Seg ( width G)) is finite;

      

       F3: Dn is finite from FRAENKEL:sch 22( F1, F2);

      

       D2: { (G * (i,j)) where i,j be Nat : [i, j] in ( Indices G) } c= Dn

      proof

        let x be object;

        assume x in { (G * (i,j)) where i,j be Nat : [i, j] in ( Indices G) };

        then

        consider i,j be Nat such that

         F40: x = (G * (i,j)) & [i, j] in ( Indices G);

        i in ( dom G) & j in ( Seg ( width G)) by ZFMISC_1: 87, F40;

        then i in ( Seg ( len G)) & j in ( Seg ( width G)) by FINSEQ_1:def 3;

        hence x in Dn by F40;

      end;

      { (G * (i,j)) where i,j be Nat : [i, j] in ( Indices G) } c= the carrier of F_Rat

      proof

        let x be object;

        assume x in { (G * (i,j)) where i,j be Nat : [i, j] in ( Indices G) };

        then

        consider i,j be Nat such that

         D1: x = (G * (i,j)) & [i, j] in ( Indices G);

        thus x in the carrier of F_Rat by B1, D1;

      end;

      then

      reconsider X = { (G * (i,j)) where i,j be Nat : [i, j] in ( Indices G) } as finite Subset of F_Rat by D2, F3;

      consider a be Element of INT such that

       A10: a <> 0 & for r be Element of RAT st r in X holds (a * r) in INT by LmDE311A;

      reconsider a as Element of F_Real by NUMBERS: 15;

      

       A6: ( len (a * G)) = ( dim L) & ( width (a * G)) = ( dim L) by MATRIX_0: 24;

      take a;

      thus a is Element of INT.Ring & a <> 0 by A10;

      for i,j be Nat st [i, j] in ( Indices (a * G)) holds ((a * G) * (i,j)) in the carrier of INT.Ring

      proof

        let i,j be Nat;

        assume

         B1: [i, j] in ( Indices (a * G));

        

         B2: ( Indices G) = [:( Seg ( dim L)), ( Seg ( dim L)):] by MATRIX_0: 24

        .= ( Indices (a * G)) by MATRIX_0: 24;

        then

         B3: ((a * G) * (i,j)) = (a * (G * (i,j))) by B1, MATRIX_3:def 5;

        (G * (i,j)) in X by B1, B2;

        hence ((a * G) * (i,j)) in the carrier of INT.Ring by A10, B3;

      end;

      hence thesis by A6, MATRIX_0: 20, ZMATRLIN: 5;

    end;

    

     LM0: for n be Nat, F be FinSequence of F_Real st F = (( Seg n) --> ( 0. F_Real )) holds ( Sum F) = ( 0. F_Real )

    proof

      let n be Nat, F be FinSequence of F_Real ;

      assume

       AS: F = (( Seg n) --> ( 0. F_Real ));

      

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

      for k be Nat holds for v be Element of F_Real st k in ( dom F) & v = (F . k) holds (F . k) = ( - v)

      proof

        let k be Nat;

        let v be Element of F_Real ;

        assume that

         X3: k in ( dom F) and

         X30: v = (F . k);

        

         X2: k in ( Seg n) by AS, X3, FUNCT_2:def 1;

        then v = ( 0. F_Real ) by AS, X30, FUNCOP_1: 7;

        hence (F . k) = ( - v) by AS, X2, FUNCOP_1: 7;

      end;

      then ( Sum F) = ( - ( Sum F)) by X2, RLVECT_1: 40;

      hence ( Sum F) = ( 0. F_Real );

    end;

    

     LM1: for L be Z_Lattice, F,F0 be FinSequence of L, l be Linear_Combination of L, v be Vector of L st F is one-to-one & F0 is one-to-one & ( Carrier l) c= ( rng F) & ( canFS ( Carrier l)) = F0 holds ( Sum ( ScFS (v,l,F))) = ( Sum ( ScFS (v,l,F0)))

    proof

      let L be Z_Lattice, F,F0 be FinSequence of L, l be Linear_Combination of L, v be Vector of L;

      assume that

       A1: F is one-to-one and

       A2: F0 is one-to-one and

       A3: ( Carrier l) c= ( rng F) and

       A4: ( canFS ( Carrier l)) = F0;

      

       A51: ( card ( dom F)) = ( card ( rng F)) by A1, CARD_1: 5, WELLORD2:def 4;

      then

       A5: ( len F) = ( card ( rng F)) by CARD_1: 62;

      

       Q1: F0 is one-to-one & ( rng F0) = ( Carrier l) by A4, FUNCT_2:def 3;

      

       FA5: ( card ( dom F0)) = ( card ( rng F0)) by A2, CARD_1: 5, WELLORD2:def 4;

      

       R1: ( len F0) = ( card ( Carrier l)) by A4, FINSEQ_1: 93;

      set CLN = (( rng F) \ ( Carrier l));

      reconsider CLN as finite Subset of L;

      set g = ( canFS CLN);

      

       Q2: g is one-to-one & ( rng g) = CLN by FUNCT_2:def 3;

      

       R2: ( len g) = ( card CLN) by FINSEQ_1: 93;

      reconsider g as FinSequence of L by Q2, FINSEQ_1:def 4;

      set H = (F0 ^ g);

      reconsider H as FinSequence of L;

      (( rng F0) /\ ( rng g)) = (( Carrier l) /\ CLN) by Q1, FUNCT_2:def 3

      .= ((( Carrier l) /\ ( rng F)) \ ( Carrier l)) by XBOOLE_1: 49

      .= (( Carrier l) \ ( Carrier l)) by A3, XBOOLE_1: 28

      .= {} by XBOOLE_1: 37;

      then ( rng F0) misses ( rng g);

      then

       Q31: H is one-to-one by A4, FINSEQ_3: 91;

      

       Q32: ( rng H) = (( rng F0) \/ ( rng g)) by FINSEQ_1: 31

      .= (( Carrier l) \/ (( rng F) \ ( Carrier l))) by Q1, FUNCT_2:def 3

      .= ( rng F) by A3, XBOOLE_1: 45;

      

       C12: (( card CLN) + ( card ( Carrier l))) = ((( card ( rng F)) - ( card ( Carrier l))) + ( card ( Carrier l))) by A3, CARD_2: 44

      .= ( card ( rng F));

      

       R3: ( len H) = (( len F0) + ( len g)) by FINSEQ_1: 22

      .= ( card ( rng F)) by C12, R1, FINSEQ_1: 93;

      then

       R4: ( dom H) = ( Seg ( card ( rng F))) by FINSEQ_1:def 3;

      set P = ((F " ) * H);

      

       T3: ( dom (F " )) = ( rng H) by A1, Q32, FUNCT_1: 33;

      

      then

       T4: ( dom P) = ( dom H) by RELAT_1: 27

      .= ( Seg ( card ( rng F))) by R3, FINSEQ_1:def 3;

      

       T5: ( rng P) = ( rng (F " )) by RELAT_1: 28, T3

      .= ( dom F) by FUNCT_1: 33, A1

      .= ( Seg ( card ( rng F))) by A5, FINSEQ_1:def 3;

      then

      reconsider P as Function of ( Seg ( card ( rng F))), ( Seg ( card ( rng F))) by T4, FUNCT_2: 1;

      P is onto by T5;

      then

      reconsider P as Permutation of ( Seg ( card ( rng F))) by A1, Q31;

      

       R5: ( len ( ScFS (v,l,F))) = ( len F) by defScFS

      .= ( card ( rng F)) by A51, CARD_1: 62;

      then

       R6: ( dom ( ScFS (v,l,F))) = ( Seg ( card ( rng F))) by FINSEQ_1:def 3;

      ( len ( ScFS (v,l,F0))) = ( len F0) by defScFS

      .= ( card ( rng F0)) by FA5, CARD_1: 62;

      then

       XR6: ( dom ( ScFS (v,l,F0))) = ( Seg ( card ( rng F0))) by FINSEQ_1:def 3;

      

       R7: ( len ( ScFS (v,l,H))) = ( card ( rng F)) by R3, defScFS;

      then

       R8: ( dom ( ScFS (v,l,H))) = ( Seg ( card ( rng F))) by FINSEQ_1:def 3;

      

       R9: for i be Nat st i in ( dom ( ScFS (v,l,F))) holds (( ScFS (v,l,H)) . i) = (( ScFS (v,l,F)) . (P . i))

      proof

        let i be Nat;

        assume

         R90: i in ( dom ( ScFS (v,l,F)));

        then i in ( dom ( ScFS (v,l,H))) by R6, R7, FINSEQ_1:def 3;

        then

         R92: (( ScFS (v,l,H)) . i) = <;v, ((l . (H /. i)) * (H /. i));> by defScFS;

        

         S3: (H . i) in ( dom (F " )) by R4, R6, R90, T3, FUNCT_1: 3;

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

        then

         S4: ((F " ) . (H . i)) in ( dom F) by FUNCT_1: 33, A1;

        

         S5: (H . i) in ( rng F) by A1, FUNCT_1: 33, S3;

        (F /. (P . i)) = (F /. ((F " ) . (H . i))) by R6, R90, T4, FUNCT_1: 12

        .= (F . ((F " ) . (H . i))) by S4, PARTFUN1:def 6

        .= (H . i) by FUNCT_1: 35, A1, S5

        .= (H /. i) by R4, R6, R90, PARTFUN1:def 6;

        hence thesis by R6, R90, R92, defScFS, FUNCT_2: 5;

      end;

      set K = (( Seg ( card CLN)) --> ( 0. F_Real ));

      ( rng K) c= the carrier of F_Real ;

      then

      reconsider K as FinSequence of F_Real by FINSEQ_1:def 4;

      

       K100: ( dom K) = ( Seg ( card CLN)) by FUNCT_2:def 1;

      

       K2: ( dom (( ScFS (v,l,F0)) ^ K)) = ( Seg (( len ( ScFS (v,l,F0))) + ( len K))) by FINSEQ_1:def 7

      .= ( Seg (( len F0) + ( len K))) by defScFS

      .= ( Seg (( card ( Carrier l)) + ( card CLN))) by R1, K100, FINSEQ_1:def 3

      .= ( dom ( ScFS (v,l,H))) by C12, R7, FINSEQ_1:def 3;

      for k be Nat st k in ( dom ( ScFS (v,l,H))) holds (( ScFS (v,l,H)) . k) = ((( ScFS (v,l,F0)) ^ K) . k)

      proof

        let k be Nat;

        assume

         K3: k in ( dom ( ScFS (v,l,H)));

        then

         L4: 1 <= k & k <= ( card ( rng F)) by R8, FINSEQ_1: 1;

        

         L5: ( card ( rng F)) = (( len F0) + ( len g)) by C12, R1, FINSEQ_1: 93;

        

         K4: (( ScFS (v,l,H)) . k) = <;v, ((l . (H /. k)) * (H /. k));> by defScFS, K3;

        per cases ;

          suppose

           CAS2: k <= ( len F0);

          then

           CAS21: k in ( dom F0) by FINSEQ_3: 25, L4;

          then (H . k) = (F0 . k) by FINSEQ_1:def 7;

          then (H . k) = (F0 /. k) by CAS21, PARTFUN1:def 6;

          then

           CAS3: (H /. k) = (F0 /. k) by K3, R4, R8, PARTFUN1:def 6;

          

           CAS4: k in ( dom ( ScFS (v,l,F0))) by CAS2, L4, XR6, R1, Q1;

          

          then ((( ScFS (v,l,F0)) ^ K) . k) = (( ScFS (v,l,F0)) . k) by FINSEQ_1:def 7

          .= <;v, ((l . (F0 /. k)) * (F0 /. k));> by CAS4, defScFS;

          hence (( ScFS (v,l,H)) . k) = ((( ScFS (v,l,F0)) ^ K) . k) by K3, CAS3, defScFS;

        end;

          suppose ( len F0) < k;

          then

           CAS7: (k - ( len F0)) > 0 by XREAL_1: 50;

          then (k - ( len F0)) in NAT by INT_1: 3;

          then

          reconsider k1 = (k - ( len F0)) as Nat;

          

           CAS8: 1 <= k1 by NAT_1: 14, CAS7;

          k1 <= ((( len F0) + ( len g)) - ( len F0)) by L4, L5, XREAL_1: 9;

          then

           CAS100: k1 in ( Seg ( len g)) by CAS8;

          then

           CAS10: k1 in ( dom g) by FINSEQ_1:def 3;

          then (H . (( len F0) + k1)) = (g . k1) by FINSEQ_1:def 7;

          then (H . k) in CLN by CAS10, Q2, FUNCT_1: 3;

          then (H /. k) in CLN by K3, R4, R8, PARTFUN1:def 6;

          then

           CAS11: not (H /. k) in ( Carrier l) by XBOOLE_0:def 5;

          

           X1: ((( ScFS (v,l,F0)) ^ K) . (( len ( ScFS (v,l,F0))) + k1)) = (K . k1) by CAS100, K100, R2, FINSEQ_1:def 7

          .= ( 0. F_Real ) by R2, CAS100, FUNCOP_1: 7;

          

           CAS5: (( len ( ScFS (v,l,F0))) + k1) = (( len F0) + k1) by defScFS;

          (( ScFS (v,l,H)) . k) = <;v, (( 0. INT.Ring ) * (H /. k));> by K4, CAS11

          .= <;(( 0. INT.Ring ) * (H /. k)), v;> by ZMODLAT1:def 3

          .= (( 0. INT.Ring ) * <;(H /. k), v;>) by ZMODLAT1:def 3

          .= ( 0. INT.Ring );

          hence (( ScFS (v,l,H)) . k) = ((( ScFS (v,l,F0)) ^ K) . k) by CAS5, X1;

        end;

      end;

      then

       R11: ( ScFS (v,l,H)) = (( ScFS (v,l,F0)) ^ K) by K2;

      ( Sum ( ScFS (v,l,H))) = (( Sum ( ScFS (v,l,F0))) + ( Sum K)) by R11, RLVECT_1: 41

      .= (( Sum ( ScFS (v,l,F0))) + ( 0. F_Real )) by LM0

      .= ( Sum ( ScFS (v,l,F0)));

      hence thesis by R6, R8, R9, R7, R5, RLVECT_2: 6;

    end;

    theorem :: ZMODLAT3:25

    

     LmDE31: for L be non trivial RATional positive-definite Z_Lattice, b be OrdBasis of ( EMLat L), i be Nat st i in ( dom b) holds ex v be Vector of ( DivisibleMod L) st (( ScProductDM L) . ((b /. i),v)) = 1 & (for j be Nat st i <> j & j in ( dom b) holds (( ScProductDM L) . ((b /. j),v)) = 0 )

    proof

      let L be non trivial RATional positive-definite Z_Lattice, b be OrdBasis of ( EMLat L), i be Nat such that

       A1: i in ( dom b);

      

       A2: ( dim L) = ( dim ( EMLat L)) by ZMODLAT2: 42;

      consider a be Element of F_Real such that

       A3: a is Element of INT.Ring & a <> 0 & (a * (( GramMatrix b) ~ )) is Matrix of ( dim L), INT.Ring by A2, LmDE311;

      (( GramMatrix b) ~ ) is_reverse_of ( GramMatrix b) by MATRIX_6:def 4;

      

      then

       A5: ((( GramMatrix b) ~ ) * ( GramMatrix b)) = ( 1. ( F_Real ,( dim ( EMLat L)))) by MATRIX_6:def 2

      .= ( 1. ( F_Real ,( dim L))) by ZMODLAT2: 42;

      ( len (( GramMatrix b) ~ )) = ( dim ( EMLat L)) by MATRIX_0:def 2;

      

      then ( width (( GramMatrix b) ~ )) = ( dim ( EMLat L)) by MATRIX_0: 20

      .= ( len ( GramMatrix b)) by MATRIX_0:def 2;

      then

       A8: ((a * (( GramMatrix b) ~ )) * ( GramMatrix b)) = (a * ( 1. ( F_Real ,( dim L)))) by A5, MATRIX15: 1;

      

       AX1: ( len b) = ( dim ( EMLat L)) by ZMATRLIN: 49;

      then

       A9: i in ( Seg ( dim L)) by A1, A2, FINSEQ_1:def 3;

      

       A10: ( Indices ( 1. ( F_Real ,( dim L)))) = [:( Seg ( dim L)), ( Seg ( dim L)):] by MATRIX_0: 24;

      then

       A11: [i, i] in ( Indices ( 1. ( F_Real ,( dim L)))) by A9, ZFMISC_1: 87;

      

       A12: ( Indices (a * ( 1. ( F_Real ,( dim L))))) = [:( Seg ( dim L)), ( Seg ( dim L)):] by MATRIX_0: 24;

      then

       A14: [i, i] in ( Indices ((a * (( GramMatrix b) ~ )) * ( GramMatrix b))) by A8, A9, ZFMISC_1: 87;

      

       AX3: ( width (a * (( GramMatrix b) ~ ))) = ( dim ( EMLat L)) by MATRIX_0: 23

      .= ( len ( GramMatrix b)) by MATRIX_0:def 2;

      

       A15: (( Line ((a * (( GramMatrix b) ~ )),i)) "*" ( Col (( GramMatrix b),i))) = (((a * (( GramMatrix b) ~ )) * ( GramMatrix b)) * (i,i)) by A14, AX3, MATRIX_3:def 4

      .= (a * (( 1. ( F_Real ,( dim L))) * (i,i))) by A8, A11, MATRIX_3:def 5

      .= (a * ( 1. F_Real )) by A11, MATRIX_1:def 3

      .= a;

      

       A16: for j be Nat st i <> j & j in ( dom b) holds (( Line ((a * (( GramMatrix b) ~ )),i)) "*" ( Col (( GramMatrix b),j))) = 0

      proof

        let j be Nat such that

         B1: i <> j & j in ( dom b);

        

         B2: j in ( Seg ( dim L)) by A2, AX1, B1, FINSEQ_1:def 3;

        then

         B3: [i, j] in ( Indices ( 1. ( F_Real ,( dim L)))) by A9, A10, ZFMISC_1: 87;

         [i, j] in ( Indices ((a * (( GramMatrix b) ~ )) * ( GramMatrix b))) by A8, A9, A12, B2, ZFMISC_1: 87;

        

        hence (( Line ((a * (( GramMatrix b) ~ )),i)) "*" ( Col (( GramMatrix b),j))) = (((a * (( GramMatrix b) ~ )) * ( GramMatrix b)) * (i,j)) by AX3, MATRIX_3:def 4

        .= (a * (( 1. ( F_Real ,( dim L))) * (i,j))) by A8, B3, MATRIX_3:def 5

        .= (a * ( 0. F_Real )) by B1, B3, MATRIX_1:def 3

        .= 0 ;

      end;

      reconsider I = ( rng b) as Basis of ( EMLat L) by ZMATRLIN:def 5;

      defpred P[ object, object] means ($1 in I implies for n be Nat st n = ((b " ) . $1) & n in ( dom b) holds $2 = ((a * (( GramMatrix b) ~ )) * (i,n))) & ( not $1 in I implies $2 = ( 0. INT.Ring ));

      

       A17: for x be Element of ( EMLat L) holds ex y be Element of INT.Ring st P[x, y]

      proof

        let x be Element of ( EMLat L);

        per cases ;

          suppose

           B1: x in I;

          b is one-to-one by ZMATRLIN:def 5;

          then

           B3: ((b " ) . x) in ( dom b) by B1, FUNCT_1: 32;

          then

          reconsider n = ((b " ) . x) as Nat;

          reconsider aG = (a * (( GramMatrix b) ~ )) as Matrix of ( dim L), INT.Ring by A3;

          

           B4: ( Indices aG) = [:( Seg ( dim L)), ( Seg ( dim L)):] by MATRIX_0: 24;

          n in ( Seg ( dim L)) by A2, AX1, B3, FINSEQ_1:def 3;

          then

           B5: [i, n] in ( Indices aG) by A9, B4, ZFMISC_1: 87;

          (aG * (i,n)) is Element of INT.Ring ;

          then

          reconsider y = ((a * (( GramMatrix b) ~ )) * (i,n)) as Element of INT.Ring by B5, ZMATRLIN: 1;

          take y;

          thus thesis by B1;

        end;

          suppose

           B1: not x in I;

          take ( 0. INT.Ring );

          thus thesis by B1;

        end;

      end;

      consider l be Function of ( EMLat L), INT.Ring such that

       A18: for x be Element of ( EMLat L) holds P[x, (l . x)] from FUNCT_2:sch 3( A17);

      l is Element of ( Funcs (the carrier of ( EMLat L),the carrier of INT.Ring )) by FUNCT_2: 8;

      then

      reconsider l as Linear_Combination of ( EMLat L) by A18, VECTSP_6:def 1;

      reconsider ai = a as Element of INT.Ring by A3;

      

       L1: ( len ( GramMatrix b)) = ( len b) by MATRIX_0: 24;

      

       L2: ( width (a * (( GramMatrix b) ~ ))) = ( dim ( EMLat L)) by MATRIX_0: 23

      .= ( len b) by ZMATRLIN: 49;

      

       Q7: ( len ( Line ((a * (( GramMatrix b) ~ )),i))) = ( len b) by L2, MATRIX_0:def 7;

      

       Q8: ( len ( Col (( GramMatrix b),i))) = ( len b) by L1, MATRIX_0:def 8;

      

       A31: ( len ( ScFS ((b /. i),l,b))) = ( len b) by defScFS

      .= ( len ( mlt (( Line ((a * (( GramMatrix b) ~ )),i)),( Col (( GramMatrix b),i))))) by Q7, Q8, FINSEQ_2: 72;

      for k be Nat st 1 <= k & k <= ( len ( ScFS ((b /. i),l,b))) holds (( mlt (( Line ((a * (( GramMatrix b) ~ )),i)),( Col (( GramMatrix b),i)))) . k) = (( ScFS ((b /. i),l,b)) . k)

      proof

        let k be Nat;

        assume

         AS1: 1 <= k <= ( len ( ScFS ((b /. i),l,b)));

        then

         Q0: k in ( dom ( ScFS ((b /. i),l,b))) by FINSEQ_3: 25;

        

         D0: 1 <= k <= ( len b) by AS1, defScFS;

        then

         D1: k in ( dom b) by FINSEQ_3: 25;

        then (b . k) in ( rng b) by FUNCT_1: 3;

        then

         Q1: (b /. k) in I by PARTFUN1:def 6, D1;

        b is one-to-one by ZMATRLIN:def 5;

        

        then

         Q2: k = ((b " ) . (b . k)) by FUNCT_1: 34, D1

        .= ((b " ) . (b /. k)) by PARTFUN1:def 6, D1;

        

         Q3: (l . (b /. k)) = ((a * (( GramMatrix b) ~ )) * (i,k)) by Q1, Q2, D0, A18, FINSEQ_3: 25;

        k in ( Seg ( width (a * (( GramMatrix b) ~ )))) by D0, L2;

        then

         Q4: (( Line ((a * (( GramMatrix b) ~ )),i)) . k) = ((a * (( GramMatrix b) ~ )) * (i,k)) by MATRIX_0:def 7;

        k in ( Seg ( len ( GramMatrix b))) by D0, L1;

        then k in ( dom ( GramMatrix b)) by FINSEQ_1:def 3;

        

        then

         Q5: (( Col (( GramMatrix b),i)) . k) = (( GramMatrix b) * (k,i)) by MATRIX_0:def 8

        .= (( InnerProduct ( EMLat L)) . ((b /. k),(b /. i))) by D1, A1, ZMODLAT1:def 32

        .= <;(b /. k), (b /. i);>

        .= <;(b /. i), (b /. k);> by ZMODLAT1:def 3

        .= (( InnerProduct ( EMLat L)) . ((b /. i),(b /. k)))

        .= (( GramMatrix b) * (i,k)) by D1, A1, ZMODLAT1:def 32;

        ( Seg ( len ( mlt (( Line ((a * (( GramMatrix b) ~ )),i)),( Col (( GramMatrix b),i)))))) = ( Seg ( len b)) by Q7, Q8, FINSEQ_2: 72

        .= ( dom b) by FINSEQ_1:def 3;

        then

         Q6: k in ( dom ( mlt (( Line ((a * (( GramMatrix b) ~ )),i)),( Col (( GramMatrix b),i))))) by D1, FINSEQ_1:def 3;

         <;(b /. i), ((l . (b /. k)) * (b /. k));> = (((a * (( GramMatrix b) ~ )) * (i,k)) * <;(b /. i), (b /. k);>) by Q3, ZMODLAT1: 9

        .= (((a * (( GramMatrix b) ~ )) * (i,k)) * (( InnerProduct ( EMLat L)) . ((b /. i),(b /. k))))

        .= (((a * (( GramMatrix b) ~ )) * (i,k)) * (( GramMatrix b) * (i,k))) by D1, A1, ZMODLAT1:def 32

        .= (( mlt (( Line ((a * (( GramMatrix b) ~ )),i)),( Col (( GramMatrix b),i)))) . k) by Q4, Q5, Q6, FVSUM_1: 60;

        hence thesis by Q0, defScFS;

      end;

      then

       A32: ( mlt (( Line ((a * (( GramMatrix b) ~ )),i)),( Col (( GramMatrix b),i)))) = ( ScFS ((b /. i),l,b)) by A31;

      set F = ( canFS ( Carrier l));

      

       A303: F is one-to-one & ( rng F) = ( Carrier l) by FUNCT_2:def 3;

      then

      reconsider F as FinSequence of ( EMLat L) by FINSEQ_1:def 4;

      

       A30: ( SumSc ((b /. i),l)) = ( Sum ( ScFS ((b /. i),l,F))) by A303, defSumSc;

      

       A302: ( Carrier l) c= ( rng b)

      proof

        let x be object;

        assume x in ( Carrier l);

        then

        consider v be Element of ( EMLat L) such that

         B30: x = v & (l . v) <> ( 0. INT.Ring );

        assume not x in ( rng b);

        hence contradiction by A18, B30;

      end;

      b is one-to-one by ZMATRLIN:def 5;

      then

       A20: ( SumSc ((b /. i),l)) = a by A15, A30, A32, A302, LM1;

      

       A21: for j be Nat st i <> j & j in ( dom b) holds <;(b /. j), ( Sum l);> = 0

      proof

        let j be Nat such that

         BJ1: i <> j & j in ( dom b);

        

         Q7: ( len ( Line ((a * (( GramMatrix b) ~ )),i))) = ( len b) by L2, MATRIX_0:def 7;

        

         Q8: ( len ( Col (( GramMatrix b),j))) = ( len b) by L1, MATRIX_0:def 8;

        

         A31: ( len ( ScFS ((b /. j),l,b))) = ( len b) by defScFS

        .= ( len ( mlt (( Line ((a * (( GramMatrix b) ~ )),i)),( Col (( GramMatrix b),j))))) by Q7, Q8, FINSEQ_2: 72;

        for k be Nat st 1 <= k & k <= ( len ( ScFS ((b /. j),l,b))) holds (( mlt (( Line ((a * (( GramMatrix b) ~ )),i)),( Col (( GramMatrix b),j)))) . k) = (( ScFS ((b /. j),l,b)) . k)

        proof

          let k be Nat;

          assume

           AS1: 1 <= k <= ( len ( ScFS ((b /. j),l,b)));

          then

           Q0: k in ( dom ( ScFS ((b /. j),l,b))) by FINSEQ_3: 25;

          

           D0: 1 <= k <= ( len b) by AS1, defScFS;

          then

           D1: k in ( dom b) by FINSEQ_3: 25;

          then (b . k) in ( rng b) by FUNCT_1: 3;

          then

           Q1: (b /. k) in I by PARTFUN1:def 6, D1;

          b is one-to-one by ZMATRLIN:def 5;

          

          then k = ((b " ) . (b . k)) by FUNCT_1: 34, D1

          .= ((b " ) . (b /. k)) by PARTFUN1:def 6, D1;

          then

           Q3: (l . (b /. k)) = ((a * (( GramMatrix b) ~ )) * (i,k)) by Q1, D0, A18, FINSEQ_3: 25;

          k in ( Seg ( width (a * (( GramMatrix b) ~ )))) by D0, L2;

          then

           Q4: (( Line ((a * (( GramMatrix b) ~ )),i)) . k) = ((a * (( GramMatrix b) ~ )) * (i,k)) by MATRIX_0:def 7;

          k in ( Seg ( len ( GramMatrix b))) by D0, L1;

          then k in ( dom ( GramMatrix b)) by FINSEQ_1:def 3;

          

          then

           Q5: (( Col (( GramMatrix b),j)) . k) = (( GramMatrix b) * (k,j)) by MATRIX_0:def 8

          .= (( InnerProduct ( EMLat L)) . ((b /. k),(b /. j))) by D1, BJ1, ZMODLAT1:def 32

          .= <;(b /. k), (b /. j);>

          .= <;(b /. j), (b /. k);> by ZMODLAT1:def 3

          .= (( InnerProduct ( EMLat L)) . ((b /. j),(b /. k)))

          .= (( GramMatrix b) * (j,k)) by D1, BJ1, ZMODLAT1:def 32;

          ( Seg ( len ( mlt (( Line ((a * (( GramMatrix b) ~ )),i)),( Col (( GramMatrix b),j)))))) = ( Seg ( len b)) by Q7, Q8, FINSEQ_2: 72

          .= ( dom b) by FINSEQ_1:def 3;

          then

           Q6: k in ( dom ( mlt (( Line ((a * (( GramMatrix b) ~ )),i)),( Col (( GramMatrix b),j))))) by D1, FINSEQ_1:def 3;

           <;(b /. j), ((l . (b /. k)) * (b /. k));> = (((a * (( GramMatrix b) ~ )) * (i,k)) * <;(b /. j), (b /. k);>) by Q3, ZMODLAT1: 9

          .= (((a * (( GramMatrix b) ~ )) * (i,k)) * (( InnerProduct ( EMLat L)) . ((b /. j),(b /. k))))

          .= (((a * (( GramMatrix b) ~ )) * (i,k)) * (( GramMatrix b) * (j,k))) by D1, BJ1, ZMODLAT1:def 32

          .= (( mlt (( Line ((a * (( GramMatrix b) ~ )),i)),( Col (( GramMatrix b),j)))) . k) by Q4, Q5, Q6, FVSUM_1: 60;

          hence thesis by Q0, defScFS;

        end;

        then ( mlt (( Line ((a * (( GramMatrix b) ~ )),i)),( Col (( GramMatrix b),j)))) = ( ScFS ((b /. j),l,b)) by A31;

        

        then

         A32: ( Sum ( ScFS ((b /. j),l,b))) = (( Line ((a * (( GramMatrix b) ~ )),i)) "*" ( Col (( GramMatrix b),j)))

        .= 0 by A16, BJ1;

        

         A30: ( SumSc ((b /. j),l)) = ( Sum ( ScFS ((b /. j),l,F))) by A303, defSumSc;

        b is one-to-one by ZMATRLIN:def 5;

        then ( Sum ( ScFS ((b /. j),l,F))) = ( Sum ( ScFS ((b /. j),l,b))) by LM1, A302;

        hence thesis by A30, A32, ThSumSc1;

      end;

      reconsider EL = ( EMLat L) as Submodule of ( DivisibleMod L) by ZMODLAT2: 20;

      ( Sum l) in EL;

      then ( Sum l) in ( DivisibleMod L) by ZMODUL01: 24;

      then

      consider u be Vector of ( DivisibleMod L) such that

       A22: (ai * u) = ( Sum l) by A3, ZMODUL08: 23;

      take u;

      (b /. i) in ( EMLat L);

      then (b /. i) in ( rng ( MorphsZQ L)) by ZMODLAT2:def 4;

      then

       A24: (b /. i) in ( EMbedding L) by ZMODUL08:def 3;

      ( Sum l) in ( EMLat L);

      then ( Sum l) in ( rng ( MorphsZQ L)) by ZMODLAT2:def 4;

      then

       A25: ( Sum l) in ( EMbedding L) by ZMODUL08:def 3;

      (b /. i) in EL;

      then (b /. i) in ( DivisibleMod L) by ZMODUL01: 24;

      then

      reconsider bi = (b /. i) as Element of ( DivisibleMod L);

      

       A28: a <> ( 0. F_Real ) by A3;

      

       A29: (a * (( ScProductDM L) . (bi,u))) = (( ScProductDM L) . (bi,(ai * u))) by ZMODLAT2: 13

      .= (( ScProductEM L) . ((b /. i),( Sum l))) by A22, A24, A25, ZMODLAT2: 8

      .= <;(b /. i), ( Sum l);> by ZMODLAT2:def 4

      .= (a * ( 1. F_Real )) by A20, ThSumSc1;

      for j be Nat st i <> j & j in ( dom b) holds (( ScProductDM L) . ((b /. j),u)) = 0

      proof

        let j be Nat such that

         B1: i <> j & j in ( dom b);

        (b /. j) in ( EMLat L);

        then (b /. j) in ( rng ( MorphsZQ L)) by ZMODLAT2:def 4;

        then

         B2: (b /. j) in ( EMbedding L) by ZMODUL08:def 3;

        (b /. j) in EL;

        then (b /. j) in ( DivisibleMod L) by ZMODUL01: 24;

        then

        reconsider bj = (b /. j) as Element of ( DivisibleMod L);

        (a * (( ScProductDM L) . (bj,u))) = (( ScProductDM L) . (bj,(ai * u))) by ZMODLAT2: 13

        .= (( ScProductEM L) . ((b /. j),( Sum l))) by A22, A25, B2, ZMODLAT2: 8

        .= <;(b /. j), ( Sum l);> by ZMODLAT2:def 4

        .= (a * ( 0. F_Real )) by A21, B1;

        hence thesis by A3;

      end;

      hence thesis by A28, A29, VECTSP_1: 5;

    end;

    begin

    

     LmDE00: for L be Z_Lattice, v be Vector of ( DivisibleMod L) holds (( ScProductDM L) . (( 0. ( DivisibleMod L)),v)) in INT.Ring

    proof

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

      reconsider m1 = ( - 1) as Element of INT.Ring by INT_1:def 2;

      

       A1: ( - ( 1. INT.Ring )) = ( - 1);

      (( ScProductDM L) . (( 0. ( DivisibleMod L)),v)) = (( ScProductDM L) . ((v + ( - v)),v)) by RLVECT_1: 5

      .= ((( ScProductDM L) . (v,v)) + (( ScProductDM L) . (( - v),v))) by ZMODLAT2: 6

      .= ((( ScProductDM L) . (v,v)) + (( ScProductDM L) . ((m1 * v),v))) by A1, ZMODUL01: 2

      .= ((( ScProductDM L) . (v,v)) + (( - 1) * (( ScProductDM L) . (v,v)))) by ZMODLAT2: 6

      .= ( 0. INT.Ring );

      hence thesis;

    end;

    definition

      let L be Z_Lattice;

      :: ZMODLAT3:def5

      mode Dual of L -> Vector of ( DivisibleMod L) means

      : defDualElement: for v be Vector of ( DivisibleMod L) st v in ( EMbedding L) holds (( ScProductDM L) . (it ,v)) in INT.Ring ;

      existence

      proof

        take ( 0. ( DivisibleMod L));

        thus thesis by LmDE00;

      end;

    end

    theorem :: ZMODLAT3:26

    

     LmDE0: for L be Z_Lattice holds ( 0. ( DivisibleMod L)) is Dual of L

    proof

      let L be Z_Lattice;

      for v be Vector of ( DivisibleMod L) st v in ( EMbedding L) holds (( ScProductDM L) . (( 0. ( DivisibleMod L)),v)) in INT.Ring by LmDE00;

      hence thesis by defDualElement;

    end;

    theorem :: ZMODLAT3:27

    

     LmDE1: for L be Z_Lattice, v,u be Dual of L holds (v + u) is Dual of L

    proof

      let L be Z_Lattice, v,u be Dual of L;

      for x be Vector of ( DivisibleMod L) st x in ( EMbedding L) holds (( ScProductDM L) . ((v + u),x)) in INT.Ring

      proof

        let x be Vector of ( DivisibleMod L) such that

         B1: x in ( EMbedding L);

        (( ScProductDM L) . (v,x)) in INT.Ring by B1, defDualElement;

        then

        reconsider iv = (( ScProductDM L) . (v,x)) as Element of INT.Ring ;

        (( ScProductDM L) . (u,x)) in INT.Ring by B1, defDualElement;

        then

        reconsider iu = (( ScProductDM L) . (u,x)) as Element of INT.Ring ;

        set iiv = iv;

        set iiu = iu;

        (( ScProductDM L) . ((v + u),x)) = ((( ScProductDM L) . (v,x)) + (( ScProductDM L) . (u,x))) by ZMODLAT2: 6

        .= (iv + iu);

        hence thesis;

      end;

      hence thesis by defDualElement;

    end;

    theorem :: ZMODLAT3:28

    

     LmDE2: for L be Z_Lattice, v be Dual of L, a be Element of INT.Ring holds (a * v) is Dual of L

    proof

      let L be Z_Lattice, v be Dual of L, a be Element of INT.Ring ;

      for x be Vector of ( DivisibleMod L) st x in ( EMbedding L) holds (( ScProductDM L) . ((a * v),x)) in INT.Ring

      proof

        let x be Vector of ( DivisibleMod L) such that

         B1: x in ( EMbedding L);

        (( ScProductDM L) . (v,x)) in INT.Ring by B1, defDualElement;

        then

        reconsider iv = (( ScProductDM L) . (v,x)) as Element of INT.Ring ;

        (( ScProductDM L) . ((a * v),x)) = (a * iv) by ZMODLAT2: 6;

        hence thesis;

      end;

      hence thesis by defDualElement;

    end;

    definition

      let L be Z_Lattice;

      :: ZMODLAT3:def6

      func DualSet (L) -> non empty Subset of ( DivisibleMod L) equals the set of all v where v be Dual of L;

      correctness

      proof

        set A = the set of all v where v be Dual of L;

        ( 0. ( DivisibleMod L)) is Dual of L by LmDE0;

        then

         A1: ( 0. ( DivisibleMod L)) in A;

        A c= the carrier of ( DivisibleMod L)

        proof

          let v be object;

          assume v in A;

          then

          consider v1 be Dual of L such that

           B1: v1 = v;

          thus thesis by B1;

        end;

        hence thesis by A1;

      end;

    end

    registration

      let L be Z_Lattice;

      cluster ( DualSet L) -> linearly-closed;

      coherence

      proof

        set A = ( DualSet L);

        

         A2: for v,u be Vector of ( DivisibleMod L) st v in A & u in A holds (v + u) in A

        proof

          let v,u be Vector of ( DivisibleMod L) such that

           B1: v in A & u in A;

          consider v1 be Dual of L such that

           B2: v1 = v by B1;

          consider u1 be Dual of L such that

           B3: u1 = u by B1;

          (v + u) is Dual of L by B2, B3, LmDE1;

          hence thesis;

        end;

        for a be Element of INT.Ring , v be Vector of ( DivisibleMod L) st v in A holds (a * v) in A

        proof

          let a be Element of INT.Ring , v be Vector of ( DivisibleMod L) such that

           B1: v in A;

          consider v1 be Dual of L such that

           B2: v1 = v by B1;

          (a * v) is Dual of L by B2, LmDE2;

          hence thesis;

        end;

        hence thesis by A2, VECTSP_4:def 1;

      end;

    end

    definition

      let L be Z_Lattice;

      :: ZMODLAT3:def7

      func DualLatMod (L) -> strict non empty LatticeStr over INT.Ring means

      : defDualMod: the carrier of it = ( DualSet L) & the addF of it = (the addF of ( DivisibleMod L) || ( DualSet L)) & the ZeroF of it = ( 0. ( DivisibleMod L)) & the lmult of it = (the lmult of ( DivisibleMod L) | [:the carrier of INT.Ring , ( DualSet L):]) & the scalar of it = (( ScProductDM L) | [:( DualSet L), ( DualSet L):]);

      existence

      proof

        reconsider ad = (the addF of ( DivisibleMod L) || ( DualSet L)) as Function of [:( DualSet L), ( DualSet L):], the carrier of ( DivisibleMod L) by FUNCT_2: 32;

        for z be Element of [:( DualSet L), ( DualSet L):] holds (ad . z) in ( DualSet L)

        proof

          let z be Element of [:( DualSet L), ( DualSet L):];

          consider x,y be object such that

           G1: x in ( DualSet L) & y in ( DualSet L) & z = [x, y] by ZFMISC_1:def 2;

          reconsider x, y as Element of ( DivisibleMod L) by G1;

          (ad . z) = (x + y) by FUNCT_1: 49, G1;

          hence (ad . z) in ( DualSet L) by G1, VECTSP_4:def 1;

        end;

        then ( rng ad) c= ( DualSet L) by FUNCT_2: 114;

        then

        reconsider ad as BinOp of ( DualSet L) by FUNCT_2: 6;

        ( 0. ( DivisibleMod L)) is Dual of L by LmDE0;

        then ( 0. ( DivisibleMod L)) in ( DualSet L);

        then

        reconsider ze = ( 0. ( DivisibleMod L)) as Element of ( DualSet L);

         [:the carrier of INT.Ring , ( DualSet L):] c= [:the carrier of INT.Ring , the carrier of ( DivisibleMod L):] by ZFMISC_1: 95;

        then

        reconsider mu = (the lmult of ( DivisibleMod L) | [:the carrier of INT.Ring , ( DualSet L):]) as Function of [:the carrier of INT.Ring , ( DualSet L):], the carrier of ( DivisibleMod L) by FUNCT_2: 32;

        for z be Element of [:the carrier of INT.Ring , ( DualSet L):] holds (mu . z) in ( DualSet L)

        proof

          let z be Element of [:the carrier of INT.Ring , ( DualSet L):];

          consider x,y be object such that

           G1: x in the carrier of INT.Ring & y in ( DualSet L) & z = [x, y] by ZFMISC_1:def 2;

          reconsider x as Element of INT.Ring by G1;

          reconsider y as Element of ( DivisibleMod L) by G1;

          (mu . z) = (x * y) by FUNCT_1: 49, G1;

          hence (mu . z) in ( DualSet L) by G1, VECTSP_4:def 1;

        end;

        then ( rng mu) c= ( DualSet L) by FUNCT_2: 114;

        then

        reconsider mu as Function of [:the carrier of INT.Ring , ( DualSet L):], ( DualSet L) by FUNCT_2: 6;

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

        take IT = LatticeStr (# ( DualSet L), ad, ze, mu, sc #);

        thus thesis;

      end;

      uniqueness ;

    end

    theorem :: ZMODLAT3:29

    for L be Z_Lattice holds ( DualLatMod L) is Submodule of ( DivisibleMod L)

    proof

      let L be Z_Lattice;

      the carrier of ( DualLatMod L) = ( DualSet L) & the addF of ( DualLatMod L) = (the addF of ( DivisibleMod L) || ( DualSet L)) & the ZeroF of ( DualLatMod L) = ( 0. ( DivisibleMod L)) & the lmult of ( DualLatMod L) = (the lmult of ( DivisibleMod L) | [:the carrier of INT.Ring , ( DualSet L):]) & the scalar of ( DualLatMod L) = (( ScProductDM L) | [:( DualSet L), ( DualSet L):]) by defDualMod;

      hence thesis by ZMODLAT2: 10;

    end;

    theorem :: ZMODLAT3:30

    

     LmDE21: 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)) in INT.Ring holds v is Dual of 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)) in INT.Ring ;

      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)) in INT.Ring holds for w be Vector of ( DivisibleMod L) st w in ( Lin I) holds (( ScProductDM L) . (v,w)) in INT.Ring ;

      

       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)) in INT.Ring ;

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

        then

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

        for w be Vector of ( DivisibleMod L) st w in ( Lin I) holds (( ScProductDM L) . (v,w)) in INT.Ring

        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;

          then (( ScProductDM L) . (w,v)) in INT.Ring by LmDE00;

          hence thesis by ZMODLAT2: 6;

        end;

        hence thesis;

      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)) in INT.Ring ;

        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)) in INT.Ring by B2, B7;

        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;

        

         C3: (( ScProductDM L) . (v,w1)) in INT.Ring by B1, B4, B6, B8, C2, C9;

        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)) in INT.Ring 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;

        

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

        .= (( ScProductDM L) . ((i * uu),v)) by ZMODLAT2: 6

        .= (i * (( ScProductDM L) . (uu,v))) by ZMODLAT2: 6

        .= (i * (( ScProductDM L) . (v,u))) by ZMODLAT2: 6;

        

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

        (( ScProductDM L) . (v,w)) = (( ScProductDM L) . (w,v)) by ZMODLAT2: 6

        .= ((( ScProductDM L) . (ww1,v)) + (( ScProductDM L) . (ww2,v))) by C10, ZMODLAT2: 6

        .= ((( ScProductDM L) . (v,w1)) + (( ScProductDM L) . (ww2,v))) by ZMODLAT2: 6

        .= ((( ScProductDM L) . (v,w1)) + (( ScProductDM L) . (v,w2))) by ZMODLAT2: 6;

        hence thesis by C3, C4, C6, C11, INT_1:def 2;

      end;

      

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

      

       P4: ( card I) is Nat;

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

      then for w be Vector of ( DivisibleMod L) st w in ( EMbedding L) holds (( ScProductDM L) . (v,w)) in INT.Ring by A1, P3, P4;

      hence thesis by defDualElement;

    end;

    definition

      let L be RATional positive-definite Z_Lattice;

      let I be Basis of ( EMLat L);

      :: ZMODLAT3:def8

      func DualBasis (I) -> Subset of ( DivisibleMod L) means

      : defDualBasis: for v be Vector of ( DivisibleMod L) holds v in it iff ex u be Vector of ( EMLat L) st u in I & (( ScProductDM L) . (u,v)) = 1 & (for w be Vector of ( EMLat L) st w in I & u <> w holds (( ScProductDM L) . (w,v)) = 0 );

      existence

      proof

        defpred P[ object] means ex u be Vector of ( EMLat L) st u in I & (( ScProductDM L) . (u,$1)) = 1 & (for w be Vector of ( EMLat L) st w in I & u <> w holds (( ScProductDM L) . (w,$1)) = 0 );

        consider C be Subset of ( DivisibleMod L) such that

         A1: for v be Element of ( DivisibleMod L) holds v in C iff P[v] from SUBSET_1:sch 3;

        take C;

        thus thesis by A1;

      end;

      uniqueness

      proof

        let C1,C2 be Subset of ( DivisibleMod L) such that

         A1: (for v be Vector of ( DivisibleMod L) holds v in C1 iff ex u be Vector of ( EMLat L) st u in I & (( ScProductDM L) . (u,v)) = 1 & (for w be Vector of ( EMLat L) st w in I & u <> w holds (( ScProductDM L) . (w,v)) = 0 )) and

         A2: (for v be Vector of ( DivisibleMod L) holds v in C2 iff ex u be Vector of ( EMLat L) st u in I & (( ScProductDM L) . (u,v)) = 1 & (for w be Vector of ( EMLat L) st w in I & u <> w holds (( ScProductDM L) . (w,v)) = 0 ));

        for v be Vector of ( DivisibleMod L) st v in C1 holds v in C2

        proof

          let v be Vector of ( DivisibleMod L) such that

           B1: v in C1;

          ex u be Vector of ( EMLat L) st u in I & (( ScProductDM L) . (u,v)) = 1 & (for w be Vector of ( EMLat L) st w in I & u <> w holds (( ScProductDM L) . (w,v)) = 0 ) by A1, B1;

          hence thesis by A2;

        end;

        then

         A3: C1 c= C2;

        for v be Vector of ( DivisibleMod L) st v in C2 holds v in C1

        proof

          let v be Vector of ( DivisibleMod L) such that

           B1: v in C2;

          ex u be Vector of ( EMLat L) st u in I & (( ScProductDM L) . (u,v)) = 1 & (for w be Vector of ( EMLat L) st w in I & u <> w holds (( ScProductDM L) . (w,v)) = 0 ) by A2, B1;

          hence thesis by A1;

        end;

        then C2 c= C1;

        hence thesis by A3;

      end;

    end

    definition

      let L be RATional positive-definite Z_Lattice;

      let I be Basis of ( EMLat L);

      :: ZMODLAT3:def9

      func B2DB (I) -> Function of I, ( DualBasis I) means

      : defB2DB: ( dom it ) = I & ( rng it ) = ( DualBasis I) & for v be Vector of ( EMLat L) st v in I holds (( ScProductDM L) . (v,(it . v))) = 1 & (for w be Vector of ( EMLat L) st w in I & v <> w holds (( ScProductDM L) . (w,(it . v))) = 0 );

      existence

      proof

        per cases ;

          suppose L is trivial;

          then ( (Omega). L) = ( (0). L) by ZMODUL07: 41;

          then ( rank L) = 0 by ZMODUL05: 1;

          then ( rank ( EMLat L)) = 0 by ZMODLAT2: 42;

          then

           A1: ( card I) = 0 by ZMODUL03:def 5;

          for v be Vector of ( DivisibleMod L) holds v in {} iff ex u be Vector of ( EMLat L) st u in I & (( ScProductDM L) . (u,v)) = 1 & (for w be Vector of ( EMLat L) st w in I & u <> w holds (( ScProductDM L) . (w,v)) = 0 ) by A1;

          then

           A2: ( DualBasis I) = ( {} the carrier of ( DivisibleMod L)) by defDualBasis;

          set F = the Function of I, ( DualBasis I);

          take F;

          I = {} by A1;

          hence thesis by A2;

        end;

          suppose

           X1: L is non trivial;

          defpred P[ object, object] means (( ScProductDM L) . ($1,$2)) = 1 & (for w be Vector of ( EMLat L) st w in I & $1 <> w holds (( ScProductDM L) . (w,$2)) = 0 );

          consider b be FinSequence such that

           A0: ( rng b) = I & b is one-to-one by FINSEQ_4: 58;

          b is FinSequence of ( EMLat L) by A0, FINSEQ_1:def 4;

          then

          reconsider b as OrdBasis of ( EMLat L) by A0, ZMATRLIN:def 5;

          

           A1: for x be object st x in I holds ex y be object st y in ( DualBasis I) & P[x, y]

          proof

            let x be object such that

             B1: x in I;

            consider i be Nat such that

             B3: i in ( dom b) & (b . i) = x by A0, B1, FINSEQ_2: 10;

            (b /. i) = x by B3, PARTFUN1:def 6;

            then

            consider y be Vector of ( DivisibleMod L) such that

             B4: (( ScProductDM L) . (x,y)) = 1 & (for j be Nat st i <> j & j in ( dom b) holds (( ScProductDM L) . ((b /. j),y)) = 0 ) by X1, B3, LmDE31;

            

             B5: for w be Vector of ( EMLat L) st w in I & x <> w holds (( ScProductDM L) . (w,y)) = 0

            proof

              let w be Vector of ( EMLat L) such that

               C1: w in I & x <> w;

              consider j be Nat such that

               C2: j in ( dom b) & (b . j) = w by A0, C1, FINSEQ_2: 10;

              (b /. j) = w by C2, PARTFUN1:def 6;

              hence thesis by B3, B4, C1, C2;

            end;

            take y;

            thus thesis by B1, B4, B5, defDualBasis;

          end;

          consider f be Function such that

           A2: ( dom f) = I & ( rng f) c= ( DualBasis I) & for x be object st x in I holds P[x, (f . x)] from FUNCT_1:sch 6( A1);

          

           A3: ( DualBasis I) c= ( rng f)

          proof

            for y be object st y in ( DualBasis I) holds ex x be object st x in ( dom f) & y = (f . x)

            proof

              let y be object such that

               B1: y in ( DualBasis I);

              consider u be Vector of ( EMLat L) such that

               B2: u in I & (( ScProductDM L) . (u,y)) = 1 & (for w be Vector of ( EMLat L) st w in I & u <> w holds (( ScProductDM L) . (w,y)) = 0 ) by B1, defDualBasis;

              take u;

              consider i be Nat such that

               B6: i in ( dom b) & (b . i) = u by A0, B2, FINSEQ_2: 10;

              

               B8: for n be Nat st n in ( dom b) holds (( ScProductDM L) . ((b /. n),y)) = (( ScProductDM L) . ((b /. n),(f . u)))

              proof

                let n be Nat such that

                 C1: n in ( dom b);

                per cases ;

                  suppose

                   C2: n = i;

                  

                  hence (( ScProductDM L) . ((b /. n),y)) = (( ScProductDM L) . (u,y)) by B6, PARTFUN1:def 6

                  .= (( ScProductDM L) . (u,(f . u))) by A2, B2

                  .= (( ScProductDM L) . ((b /. n),(f . u))) by B6, C2, PARTFUN1:def 6;

                end;

                  suppose n <> i;

                  then (b . n) <> (b . i) by A0, B6, C1;

                  then

                   C2: (b /. n) <> u by B6, C1, PARTFUN1:def 6;

                  (b . n) in ( rng b) by C1, FUNCT_1: 3;

                  then

                   C3: (b /. n) in I by A0, C1, PARTFUN1:def 6;

                  

                  hence (( ScProductDM L) . ((b /. n),y)) = 0 by B2, C2

                  .= (( ScProductDM L) . ((b /. n),(f . u))) by A2, B2, C2, C3;

                end;

              end;

              (f . u) in ( DualBasis I) by A2, B2, FUNCT_1: 3;

              hence thesis by A2, B1, B2, B8, ZMODLAT2: 63;

            end;

            hence thesis by FUNCT_1: 9;

          end;

          then ( rng f) = ( DualBasis I) by A2;

          then

          reconsider f as Function of I, ( DualBasis I) by A2, FUNCT_2: 1;

          take f;

          thus thesis by A2, A3;

        end;

      end;

      uniqueness

      proof

        let f1,f2 be Function of I, ( DualBasis I);

        assume

         AS1: ( dom f1) = I & ( rng f1) = ( DualBasis I) & for v be Vector of ( EMLat L) st v in I holds (( ScProductDM L) . (v,(f1 . v))) = 1 & (for w be Vector of ( EMLat L) st w in I & v <> w holds (( ScProductDM L) . (w,(f1 . v))) = 0 );

        assume

         AS2: ( dom f2) = I & ( rng f2) = ( DualBasis I) & for v be Vector of ( EMLat L) st v in I holds (( ScProductDM L) . (v,(f2 . v))) = 1 & (for w be Vector of ( EMLat L) st w in I & v <> w holds (( ScProductDM L) . (w,(f2 . v))) = 0 );

        consider b be FinSequence such that

         A0: ( rng b) = I & b is one-to-one by FINSEQ_4: 58;

        b is FinSequence of ( EMLat L) by A0, FINSEQ_1:def 4;

        then

        reconsider b as OrdBasis of ( EMLat L) by A0, ZMATRLIN:def 5;

        for x be Element of I holds (f1 . x) = (f2 . x)

        proof

          let x be Element of I;

          per cases ;

            suppose I is empty;

            hence thesis;

          end;

            suppose

             XX1: I is non empty;

            then

             X1: x in I;

            

             A1: for n be Nat st n in ( dom b) holds (( ScProductDM L) . ((b /. n),(f1 . x))) = (( ScProductDM L) . ((b /. n),(f2 . x)))

            proof

              let n be Nat such that

               B1: n in ( dom b);

              

               B2: (b . n) in I by A0, B1, FUNCT_1: 3;

              then

               B2X: (b /. n) in I by B1, PARTFUN1:def 6;

              per cases ;

                suppose

                 B3: (b /. n) = x;

                

                hence (( ScProductDM L) . ((b /. n),(f1 . x))) = 1 by AS1, B2

                .= (( ScProductDM L) . ((b /. n),(f2 . x))) by AS2, B2, B3;

              end;

                suppose

                 B4: (b /. n) <> x;

                

                hence (( ScProductDM L) . ((b /. n),(f1 . x))) = 0 by AS1, X1, B2X

                .= (( ScProductDM L) . ((b /. n),(f2 . x))) by AS2, X1, B2X, B4;

              end;

            end;

            

             A2: (f1 . x) in ( DualBasis I) by AS1, XX1, FUNCT_1: 3;

            (f2 . x) in ( DualBasis I) by AS2, XX1, FUNCT_1: 3;

            hence thesis by A1, A2, ZMODLAT2: 63;

          end;

        end;

        hence f1 = f2;

      end;

    end

    registration

      let L be RATional positive-definite Z_Lattice;

      let I be Basis of ( EMLat L);

      cluster ( B2DB I) -> onto one-to-one;

      correctness

      proof

        set f = ( B2DB I);

        thus f is onto by defB2DB;

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

        proof

          let x1,x2 be object such that

           B1: x1 in ( dom f) & x2 in ( dom f) & (f . x1) = (f . x2);

          

           B2: x1 in I by B1;

          

           B5: x2 in I by B1;

          

           B6: (( ScProductDM L) . (x1,(f . x2))) = 1 by B1, B2, defB2DB;

          assume x1 <> x2;

          hence contradiction by B2, B5, B6, defB2DB;

        end;

        hence ( B2DB I) is one-to-one;

      end;

    end

    theorem :: ZMODLAT3:31

    

     ThDB1: for L be RATional positive-definite Z_Lattice, I be Basis of ( EMLat L) holds ( card I) = ( card ( DualBasis I))

    proof

      let L be RATional positive-definite Z_Lattice, I be Basis of ( EMLat L);

      ( B2DB I) is one-to-one & ( dom ( B2DB I)) = I & ( rng ( B2DB I)) = ( DualBasis I) by defB2DB;

      hence thesis by CARD_1: 5, WELLORD2:def 4;

    end;

    registration

      let L be RATional positive-definite Z_Lattice;

      let I be Basis of ( EMLat L);

      cluster ( DualBasis I) -> finite;

      correctness

      proof

        ( card ( DualBasis I)) c= ( card I) by ThDB1;

        hence thesis;

      end;

    end

    registration

      let L be non trivial RATional positive-definite Z_Lattice;

      let I be Basis of ( EMLat L);

      cluster ( DualBasis I) -> non empty;

      correctness

      proof

        ( card I) <> 0 ;

        hence thesis by ThDB1, CARD_1: 27;

      end;

    end

    theorem :: ZMODLAT3:32

    

     LmDE32: for L be RATional positive-definite Z_Lattice, I be Basis of ( EMLat L), v be Vector of ( DivisibleMod L), l be Linear_Combination of ( DualBasis I) st v in I holds (( ScProductDM L) . (v,( Sum l))) = (l . (( B2DB I) . v))

    proof

      let L be RATional positive-definite Z_Lattice, I be Basis of ( EMLat L), v be Vector of ( DivisibleMod L), l be Linear_Combination of ( DualBasis I) such that

       A1: v in I;

      v in ( dom ( B2DB I)) by A1, defB2DB;

      then (( B2DB I) . v) in ( rng ( B2DB I)) by FUNCT_1: 3;

      then

       A2: (( B2DB I) . v) in ( DualBasis I);

      then

      reconsider bv = (( B2DB I) . v) as Vector of ( DivisibleMod L);

      per cases ;

        suppose

         B1: not (( B2DB I) . v) in ( Carrier l);

        consider F be FinSequence of ( DivisibleMod L) such that

         B2: F is one-to-one & ( rng F) = ( Carrier l) & ( SumSc (v,l)) = ( Sum ( ScFS (v,l,F))) by defSumScDM;

        

         B3: ( len F) = ( len ( ScFS (v,l,F))) by defScFSDM;

        then

         B4: ( dom ( ScFS (v,l,F))) = ( dom F) by FINSEQ_3: 29;

        for k be Nat st k in ( dom ( ScFS (v,l,F))) holds (( ScFS (v,l,F)) . k) = ( - (( ScFS (v,l,F)) /. k))

        proof

          let k be Nat such that

           C1: k in ( dom ( ScFS (v,l,F)));

          

           CX2: (( ScFS (v,l,F)) . k) = (( ScProductDM L) . (v,((l . (F /. k)) * (F /. k)))) by C1, defScFSDM;

          (F . k) in ( Carrier l) by B2, B4, C1, FUNCT_1: 3;

          then

           C2: (F /. k) in ( Carrier l) by B4, C1, PARTFUN1:def 6;

          then (F /. k) in ( DualBasis I) by TARSKI:def 3, VECTSP_6:def 4;

          then

           C4: (F /. k) in ( rng ( B2DB I)) by defB2DB;

          then

           C5: (( B2DB I) . ((( B2DB I) " ) . (F /. k))) = (F /. k) by FUNCT_1: 35;

          (F /. k) in ( dom (( B2DB I) " )) by C4, FUNCT_1: 33;

          then ((( B2DB I) " ) . (F /. k)) in ( rng (( B2DB I) " )) by FUNCT_1: 3;

          then ((( B2DB I) " ) . (F /. k)) in ( dom ( B2DB I)) by FUNCT_1: 33;

          then ((( B2DB I) " ) . (F /. k)) in I;

          then (( ScProductDM L) . (v,(F /. k))) = ( 0. F_Real ) by A1, B1, C2, C5, defB2DB;

          then ((l . (F /. k)) * (( ScProductDM L) . (v,(F /. k)))) = ( 0. F_Real );

          then (( ScProductDM L) . (v,((l . (F /. k)) * (F /. k)))) = ( 0. F_Real ) by ZMODLAT2: 13;

          

          hence (( ScFS (v,l,F)) . k) = ( - (( ScFS (v,l,F)) . k)) by CX2

          .= ( - (( ScFS (v,l,F)) /. k)) by C1, PARTFUN1:def 6;

        end;

        then

         B5: ( Sum ( ScFS (v,l,F))) = ( - ( Sum ( ScFS (v,l,F)))) by B3, RLVECT_2: 4;

        

        thus (l . (( B2DB I) . v)) = ( 0. INT.Ring ) by A2, B1

        .= (( ScProductDM L) . (v,( Sum l))) by B2, B5, ThSumScDM1;

      end;

        suppose (( B2DB I) . v) in ( Carrier l);

        then

         C2: ( Carrier l) = ((( Carrier l) \ {(( B2DB I) . v)}) \/ {(( B2DB I) . v)}) by XBOOLE_1: 45, ZFMISC_1: 31;

        

         C3: ((( Carrier l) \ {(( B2DB I) . v)}) /\ {(( B2DB I) . v)}) = {} by XBOOLE_0:def 7, XBOOLE_1: 79;

        l is Linear_Combination of ( Carrier l) by VECTSP_6: 7;

        then

        consider l1 be Linear_Combination of (( Carrier l) \ {bv}), l2 be Linear_Combination of {bv} such that

         C4: l = (l1 + l2) by C2, C3, ZMODUL04: 26;

        for x be Vector of ( DivisibleMod L) st x in (( Carrier l) \ {bv}) holds x in ( Carrier l1)

        proof

          let x be Vector of ( DivisibleMod L) such that

           D1: x in (( Carrier l) \ {bv});

          x in ( Carrier l) by D1, XBOOLE_0:def 5;

          then

           D2: (l . x) <> ( 0. INT.Ring ) by VECTSP_6: 2;

          

           D3: ( Carrier l2) c= {bv} by VECTSP_6:def 4;

          

           D4: (l . x) = ((l1 . x) + (l2 . x)) by C4, VECTSP_6: 22;

           not x in ( Carrier l2) by D1, D3, XBOOLE_0:def 5;

          then (l1 . x) <> ( 0. INT.Ring ) by D2, D4;

          hence thesis;

        end;

        then (( Carrier l) \ {bv}) c= ( Carrier l1);

        then

         C6: ( Carrier l1) = (( Carrier l) \ {bv}) by VECTSP_6:def 4;

        then

         C7: not bv in ( Carrier l1) by ZFMISC_1: 56;

        consider F1 be FinSequence of ( DivisibleMod L) such that

         C8: F1 is one-to-one & ( rng F1) = ( Carrier l1) & ( SumSc (v,l1)) = ( Sum ( ScFS (v,l1,F1))) by defSumScDM;

        

         C9: ( len F1) = ( len ( ScFS (v,l1,F1))) by defScFSDM;

        then

         C10: ( dom ( ScFS (v,l1,F1))) = ( dom F1) by FINSEQ_3: 29;

        for k be Nat st k in ( dom ( ScFS (v,l1,F1))) holds (( ScFS (v,l1,F1)) . k) = ( - (( ScFS (v,l1,F1)) /. k))

        proof

          let k be Nat such that

           D1: k in ( dom ( ScFS (v,l1,F1)));

          

           D2: (( ScFS (v,l1,F1)) . k) = (( ScProductDM L) . (v,((l1 . (F1 /. k)) * (F1 /. k)))) by D1, defScFSDM;

          per cases ;

            suppose

             E1: (F1 /. k) <> (( B2DB I) . v);

            (F1 . k) in ( Carrier l1) by C8, C10, D1, FUNCT_1: 3;

            then (F1 /. k) in ( Carrier l1) by C10, D1, PARTFUN1:def 6;

            then (F1 /. k) in ( Carrier l) by C6, XBOOLE_0:def 5;

            then (F1 /. k) in ( DualBasis I) by TARSKI:def 3, VECTSP_6:def 4;

            then

             E5: (F1 /. k) in ( rng ( B2DB I)) by defB2DB;

            then (F1 /. k) in ( dom (( B2DB I) " )) by FUNCT_1: 33;

            then ((( B2DB I) " ) . (F1 /. k)) in ( rng (( B2DB I) " )) by FUNCT_1: 3;

            then ((( B2DB I) " ) . (F1 /. k)) in ( dom ( B2DB I)) by FUNCT_1: 33;

            then

             E7: ((( B2DB I) " ) . (F1 /. k)) in I;

            

             E9: (( B2DB I) . ((( B2DB I) " ) . (F1 /. k))) = (F1 /. k) by E5, FUNCT_1: 35;

            (( ScProductDM L) . (v,(F1 /. k))) = ( 0. F_Real ) by A1, E1, E7, E9, defB2DB;

            then ((l1 . (F1 /. k)) * (( ScProductDM L) . (v,(F1 /. k)))) = ( 0. F_Real );

            then (( ScProductDM L) . (v,((l1 . (F1 /. k)) * (F1 /. k)))) = ( 0. F_Real ) by ZMODLAT2: 13;

            

            hence (( ScFS (v,l1,F1)) . k) = ( - (( ScFS (v,l1,F1)) . k)) by D2

            .= ( - (( ScFS (v,l1,F1)) /. k)) by D1, PARTFUN1:def 6;

          end;

            suppose (F1 /. k) = (( B2DB I) . v);

            

            then (( ScFS (v,l1,F1)) . k) = (( ScProductDM L) . (v,(( 0. INT.Ring ) * (F1 /. k)))) by C7, D2

            .= (( ScProductDM L) . (v,( 0. ( DivisibleMod L)))) by VECTSP_1: 14

            .= ( 0. F_Real ) by ZMODLAT2: 14;

            

            hence (( ScFS (v,l1,F1)) . k) = ( - (( ScFS (v,l1,F1)) . k))

            .= ( - (( ScFS (v,l1,F1)) /. k)) by D1, PARTFUN1:def 6;

          end;

        end;

        then

         C11: ( Sum ( ScFS (v,l1,F1))) = ( - ( Sum ( ScFS (v,l1,F1)))) by C9, RLVECT_2: 4;

        

         C12: ( SumSc (v,l2)) = (( ScProductDM L) . (v,((l2 . bv) * bv))) by LmSumScDM14

        .= ((l2 . bv) * (( ScProductDM L) . (v,bv))) by ZMODLAT2: 13

        .= ((l2 . bv) * 1) by A1, defB2DB

        .= (l2 . bv);

        

         C13: (l . bv) = ((l1 . bv) + (l2 . bv)) by C4, VECTSP_6: 22

        .= (( 0. INT.Ring ) + (l2 . bv)) by C7

        .= (l2 . bv);

        

        thus (( ScProductDM L) . (v,( Sum l))) = ( SumSc (v,l)) by ThSumScDM1

        .= (( SumSc (v,l1)) + ( SumSc (v,l2))) by C4, LmSumScDM1X

        .= (l . (( B2DB I) . v)) by C8, C11, C12, C13;

      end;

    end;

    theorem :: ZMODLAT3:33

    

     ThDE3: for L be RATional positive-definite Z_Lattice, I be Basis of ( EMLat L), v be Vector of ( DivisibleMod L) st v is Dual of L holds v in ( Lin ( DualBasis I))

    proof

      let L be RATional positive-definite Z_Lattice, I be Basis of ( EMLat L), v be Vector of ( DivisibleMod L) such that

       A1: v is Dual of L;

      set f = (( B2DB I) " );

      defpred P[ object, object] means ($1 in ( DualBasis I) implies $2 = (( ScProductDM L) . ((f . $1),v))) & ( not $1 in ( DualBasis I) implies $2 = ( 0. INT.Ring ));

      

       A2: for x be object st x in the carrier of ( DivisibleMod L) holds ex y be object st y in the carrier of INT.Ring & P[x, y]

      proof

        let x be object such that x in the carrier of ( DivisibleMod L);

        per cases ;

          suppose

           B2: x in ( DualBasis I);

          then x in ( rng ( B2DB I)) by defB2DB;

          then x in ( dom f) by FUNCT_1: 33;

          then (f . x) in ( rng f) by FUNCT_1: 3;

          then (f . x) in ( dom ( B2DB I)) by FUNCT_1: 33;

          then (f . x) in I;

          then (f . x) in ( EMLat L);

          then (f . x) in ( rng ( MorphsZQ L)) by ZMODLAT2:def 4;

          then

           B3: (f . x) in ( EMbedding L) by ZMODUL08:def 3;

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

          then

           B4: (f . x) is Vector of ( DivisibleMod L) by B3, ZMODUL01: 25;

          then

           B5: (( ScProductDM L) . (v,(f . x))) in INT.Ring by A1, B3, defDualElement;

          take (( ScProductDM L) . ((f . x),v));

          thus thesis by B2, B4, B5, ZMODLAT2: 6;

        end;

          suppose not x in ( DualBasis I);

          hence thesis;

        end;

      end;

      consider l be Function of ( DivisibleMod L), the carrier of INT.Ring such that

       A3: for x be object st x in the carrier of ( DivisibleMod L) holds P[x, (l . x)] from FUNCT_2:sch 1( A2);

      reconsider l as Element of ( Funcs (the carrier of ( DivisibleMod L),the carrier of INT.Ring )) by FUNCT_2: 8;

      for v be Vector of ( DivisibleMod L) st not v in ( DualBasis I) holds (l . v) = ( 0. INT.Ring ) by A3;

      then

      reconsider l as Linear_Combination of ( DivisibleMod L) by VECTSP_6:def 1;

      ( Carrier l) c= ( DualBasis I)

      proof

        for x be Vector of ( DivisibleMod L) st not x in ( DualBasis I) holds not x in ( Carrier l)

        proof

          let x be Vector of ( DivisibleMod L) such that

           B1: not x in ( DualBasis I);

          (l . x) = ( 0. INT.Ring ) by A3, B1;

          hence thesis by VECTSP_6: 2;

        end;

        hence thesis;

      end;

      then

       A5: l is Linear_Combination of ( DualBasis I) by VECTSP_6:def 4;

      consider b be FinSequence such that

       A6: ( rng b) = I & b is one-to-one by FINSEQ_4: 58;

      b is FinSequence of ( EMLat L) by A6, FINSEQ_1:def 4;

      then

      reconsider b as OrdBasis of ( EMLat L) by A6, ZMATRLIN:def 5;

      for n be Nat st n in ( dom b) holds (( ScProductDM L) . ((b /. n),v)) = (( ScProductDM L) . ((b /. n),( Sum l)))

      proof

        let n be Nat such that

         B1: n in ( dom b);

        ( EMLat L) is Submodule of ( DivisibleMod L) by ZMODLAT2: 20;

        then

        reconsider bn = (b /. n) as Vector of ( DivisibleMod L) by ZMODUL01: 25;

        (( ScProductDM L) . (bn,v)) = ( SumSc (bn,l))

        proof

          (b . n) in ( rng b) by B1, FUNCT_1: 3;

          then

           B2: bn in I by A6, B1, PARTFUN1:def 6;

          then

           B5: bn in ( dom ( B2DB I)) by defB2DB;

          then

           B3: (( B2DB I) . bn) in ( rng ( B2DB I)) by FUNCT_1: 3;

          then

           B31: (( B2DB I) . bn) in ( DualBasis I);

          

           B4: for v be Vector of ( DivisibleMod L) st v <> (( B2DB I) . bn) holds (( ScProductDM L) . (bn,((l . v) * v))) = ( 0. F_Real )

          proof

            let v be Vector of ( DivisibleMod L) such that

             C1: v <> (( B2DB I) . bn);

            per cases ;

              suppose not v in ( DualBasis I);

              then (l . v) = ( 0. INT.Ring ) by A3;

              then ((l . v) * v) = ( 0. ( DivisibleMod L)) by VECTSP_1: 14;

              hence thesis by ZMODLAT2: 14;

            end;

              suppose v in ( DualBasis I);

              then

               C21: v in ( rng ( B2DB I)) by defB2DB;

              then

               C0: (( B2DB I) . (f . v)) = v by FUNCT_1: 35;

              v in ( dom f) by C21, FUNCT_1: 33;

              then (f . v) in ( rng f) by FUNCT_1: 3;

              then (f . v) in ( dom ( B2DB I)) by FUNCT_1: 33;

              then (f . v) in I;

              then (( ScProductDM L) . (bn,v)) = ( 0. F_Real ) by B2, C0, C1, defB2DB;

              then ((l . v) * (( ScProductDM L) . (bn,v))) = ( 0. F_Real );

              hence (( ScProductDM L) . (bn,((l . v) * v))) = ( 0. F_Real ) by ZMODLAT2: 13;

            end;

          end;

          reconsider bbn = (( B2DB I) . bn) as Vector of ( DivisibleMod L) by B31;

          per cases ;

            suppose

             C1: not (( B2DB I) . bn) in ( Carrier l);

            consider F be FinSequence of ( DivisibleMod L) such that

             C2: F is one-to-one & ( rng F) = ( Carrier l) & ( SumSc (bn,l)) = ( Sum ( ScFS (bn,l,F))) by defSumScDM;

            

             C3: ( len F) = ( len ( ScFS (bn,l,F))) by defScFSDM;

            for k be Nat st k in ( dom ( ScFS (bn,l,F))) holds (( ScFS (bn,l,F)) . k) = ( - (( ScFS (bn,l,F)) /. k))

            proof

              let k be Nat such that

               D1: k in ( dom ( ScFS (bn,l,F)));

              

               D2: (( ScFS (bn,l,F)) . k) = (( ScProductDM L) . (bn,((l . (F /. k)) * (F /. k)))) by D1, defScFSDM;

              per cases ;

                suppose (F /. k) <> (( B2DB I) . bn);

                then (( ScFS (bn,l,F)) . k) = ( 0. F_Real ) by B4, D2;

                

                hence (( ScFS (bn,l,F)) . k) = ( - (( ScFS (bn,l,F)) . k))

                .= ( - (( ScFS (bn,l,F)) /. k)) by D1, PARTFUN1:def 6;

              end;

                suppose (F /. k) = (( B2DB I) . bn);

                

                then (( ScFS (bn,l,F)) . k) = (( ScProductDM L) . (bn,(( 0. INT.Ring ) * (F /. k)))) by C1, D2

                .= (( ScProductDM L) . (bn,( 0. ( DivisibleMod L)))) by VECTSP_1: 14

                .= ( 0. F_Real ) by ZMODLAT2: 14;

                

                hence (( ScFS (bn,l,F)) . k) = ( - (( ScFS (bn,l,F)) . k))

                .= ( - (( ScFS (bn,l,F)) /. k)) by D1, PARTFUN1:def 6;

              end;

            end;

            then

             C4: ( Sum ( ScFS (bn,l,F))) = ( - ( Sum ( ScFS (bn,l,F)))) by C3, RLVECT_2: 4;

            (l . (( B2DB I) . bn)) = (( ScProductDM L) . ((f . (( B2DB I) . bn)),v)) by A3, B31;

            then (( ScProductDM L) . ((f . bbn),v)) = ( 0. INT.Ring ) by C1;

            hence thesis by B5, C2, C4, FUNCT_1: 34;

          end;

            suppose (( B2DB I) . bn) in ( Carrier l);

            then

             C2: ( Carrier l) = ((( Carrier l) \ {(( B2DB I) . bn)}) \/ {(( B2DB I) . bn)}) by XBOOLE_1: 45, ZFMISC_1: 31;

            

             C3: ((( Carrier l) \ {(( B2DB I) . bn)}) /\ {(( B2DB I) . bn)}) = {} by XBOOLE_0:def 7, XBOOLE_1: 79;

            l is Linear_Combination of ( Carrier l) by VECTSP_6: 7;

            then

            consider l1 be Linear_Combination of (( Carrier l) \ {bbn}), l2 be Linear_Combination of {bbn} such that

             C4: l = (l1 + l2) by C2, C3, ZMODUL04: 26;

            for x be Vector of ( DivisibleMod L) st x in (( Carrier l) \ {bbn}) holds x in ( Carrier l1)

            proof

              let x be Vector of ( DivisibleMod L) such that

               D1: x in (( Carrier l) \ {bbn});

              x in ( Carrier l) by D1, XBOOLE_0:def 5;

              then

               D2: (l . x) <> ( 0. INT.Ring ) by VECTSP_6: 2;

              

               D3: ( Carrier l2) c= {bbn} by VECTSP_6:def 4;

              

               D4: (l . x) = ((l1 . x) + (l2 . x)) by C4, VECTSP_6: 22;

               not x in ( Carrier l2) by D1, D3, XBOOLE_0:def 5;

              then (l1 . x) <> ( 0. INT.Ring ) by D2, D4;

              hence thesis;

            end;

            then (( Carrier l) \ {bbn}) c= ( Carrier l1);

            then ( Carrier l1) = (( Carrier l) \ {bbn}) by VECTSP_6:def 4;

            then

             C12: not bbn in ( Carrier l1) by ZFMISC_1: 56;

            consider F1 be FinSequence of ( DivisibleMod L) such that

             C7: F1 is one-to-one & ( rng F1) = ( Carrier l1) & ( SumSc (bn,l1)) = ( Sum ( ScFS (bn,l1,F1))) by defSumScDM;

            

             C8: ( len F1) = ( len ( ScFS (bn,l1,F1))) by defScFSDM;

            for k be Nat st k in ( dom ( ScFS (bn,l1,F1))) holds (( ScFS (bn,l1,F1)) . k) = ( - (( ScFS (bn,l1,F1)) /. k))

            proof

              let k be Nat such that

               D1: k in ( dom ( ScFS (bn,l1,F1)));

              per cases ;

                suppose

                 E1: (F1 /. k) <> (( B2DB I) . bn);

                then not (F1 /. k) in {bbn} by TARSKI:def 1;

                then

                 E2: not (F1 /. k) in ( Carrier l2) by TARSKI:def 3, VECTSP_6:def 4;

                (l . (F1 /. k)) = ((l1 . (F1 /. k)) + (l2 . (F1 /. k))) by C4, VECTSP_6: 22

                .= ((l1 . (F1 /. k)) + ( 0. INT.Ring )) by E2

                .= (l1 . (F1 /. k));

                

                then (( ScFS (bn,l1,F1)) . k) = (( ScProductDM L) . (bn,((l . (F1 /. k)) * (F1 /. k)))) by D1, defScFSDM

                .= ( 0. F_Real ) by B4, E1;

                

                hence (( ScFS (bn,l1,F1)) . k) = ( - (( ScFS (bn,l1,F1)) . k))

                .= ( - (( ScFS (bn,l1,F1)) /. k)) by D1, PARTFUN1:def 6;

              end;

                suppose (F1 /. k) = (( B2DB I) . bn);

                then (l1 . (F1 /. k)) = ( 0. INT.Ring ) by C12;

                

                then (( ScFS (bn,l1,F1)) . k) = (( ScProductDM L) . (bn,(( 0. INT.Ring ) * (F1 /. k)))) by D1, defScFSDM

                .= (( ScProductDM L) . (bn,( 0. ( DivisibleMod L)))) by VECTSP_1: 14

                .= ( 0. F_Real ) by ZMODLAT2: 14;

                

                hence (( ScFS (bn,l1,F1)) . k) = ( - (( ScFS (bn,l1,F1)) . k))

                .= ( - (( ScFS (bn,l1,F1)) /. k)) by D1, PARTFUN1:def 6;

              end;

            end;

            then

             C9: ( Sum ( ScFS (bn,l1,F1))) = ( - ( Sum ( ScFS (bn,l1,F1)))) by C8, RLVECT_2: 4;

            

             C10: ( SumSc (bn,l2)) = (( ScProductDM L) . (bn,((l2 . bbn) * bbn))) by LmSumScDM14

            .= ((l2 . bbn) * (( ScProductDM L) . (bn,bbn))) by ZMODLAT2: 13

            .= ((l2 . bbn) * 1) by B2, defB2DB

            .= (l2 . bbn);

            (l . bbn) = ((l1 . bbn) + (l2 . bbn)) by C4, VECTSP_6: 22

            .= (( 0. INT.Ring ) + (l2 . bbn)) by C12

            .= (l2 . bbn);

            

            then

             C11: ( SumSc (bn,l2)) = (( ScProductDM L) . ((f . bbn),v)) by A3, B3, C10

            .= (( ScProductDM L) . (bn,v)) by B5, FUNCT_1: 34;

            

            thus ( SumSc (bn,l)) = (( SumSc (bn,l1)) + ( SumSc (bn,l2))) by C4, LmSumScDM1X

            .= (( ScProductDM L) . (bn,v)) by C7, C9, C11;

          end;

        end;

        hence thesis by ThSumScDM1;

      end;

      hence thesis by A5, ZMODLAT2: 63, ZMODUL02: 64;

    end;

    registration

      let L be RATional positive-definite Z_Lattice;

      let I be Basis of ( EMLat L);

      cluster ( DualBasis I) -> linearly-independent;

      correctness

      proof

        assume ( DualBasis I) is linearly-dependent;

        then

        consider l be Linear_Combination of ( DualBasis I) such that

         B1: ( Sum l) = ( 0. ( DivisibleMod L)) & ( Carrier l) <> {} by VECTSP_7:def 1;

        consider u be object such that

         B2: u in ( Carrier l) by B1, XBOOLE_0:def 1;

        reconsider u as Element of ( DivisibleMod L) by B2;

        

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

        then u in ( DualBasis I) by B2;

        then

         B31: u in ( rng ( B2DB I)) by defB2DB;

        then u in ( dom (( B2DB I) " )) by FUNCT_1: 33;

        then ((( B2DB I) " ) . u) in ( rng (( B2DB I) " )) by FUNCT_1: 3;

        then

         B4: ((( B2DB I) " ) . u) in ( dom ( B2DB I)) by FUNCT_1: 33;

        then ((( B2DB I) " ) . u) in I;

        then

        reconsider bu = ((( B2DB I) " ) . u) as Vector of ( EMLat L);

        ( EMLat L) is Submodule of ( DivisibleMod L) by ZMODLAT2: 20;

        then

        reconsider bu as Vector of ( DivisibleMod L) by ZMODUL01: 25;

        

         B5: (( ScProductDM L) . (bu,( Sum l))) = ( SumSc (bu,l)) by ThSumScDM1;

        

         B6: ( Carrier l) = ((( Carrier l) \ {u}) \/ {u}) by B2, XBOOLE_1: 45, ZFMISC_1: 31;

        

         B7: ((( Carrier l) \ {u}) /\ {u}) = {} by XBOOLE_0:def 7, XBOOLE_1: 79;

        l is Linear_Combination of ( Carrier l) by VECTSP_6: 7;

        then

        consider l1 be Linear_Combination of (( Carrier l) \ {u}), l2 be Linear_Combination of {u} such that

         B8: l = (l1 + l2) by B6, B7, ZMODUL04: 26;

        for x be Vector of ( DivisibleMod L) st x in (( Carrier l) \ {u}) holds x in ( Carrier l1)

        proof

          let x be Vector of ( DivisibleMod L) such that

           C1: x in (( Carrier l) \ {u});

          x in ( Carrier l) by C1, XBOOLE_0:def 5;

          then

           C2: (l . x) <> ( 0. INT.Ring ) by VECTSP_6: 2;

          

           C3: ( Carrier l2) c= {u} by VECTSP_6:def 4;

          

           C4: (l . x) = ((l1 . x) + (l2 . x)) by B8, VECTSP_6: 22;

           not x in ( Carrier l2) by C1, C3, XBOOLE_0:def 5;

          then (l1 . x) <> ( 0. INT.Ring ) by C2, C4;

          hence thesis;

        end;

        then (( Carrier l) \ {u}) c= ( Carrier l1);

        then

         B10: ( Carrier l1) = (( Carrier l) \ {u}) by VECTSP_6:def 4;

        then

         B11: not u in ( Carrier l1) by ZFMISC_1: 56;

        

         B12: (( B2DB I) . bu) = u by B31, FUNCT_1: 35;

        consider F1 be FinSequence of ( DivisibleMod L) such that

         B13: F1 is one-to-one & ( rng F1) = ( Carrier l1) & ( SumSc (bu,l1)) = ( Sum ( ScFS (bu,l1,F1))) by defSumScDM;

        

         B14: ( len F1) = ( len ( ScFS (bu,l1,F1))) by defScFSDM;

        for k be Nat st k in ( dom ( ScFS (bu,l1,F1))) holds (( ScFS (bu,l1,F1)) . k) = ( - (( ScFS (bu,l1,F1)) /. k))

        proof

          let k be Nat such that

           C1: k in ( dom ( ScFS (bu,l1,F1)));

          

           C2: (( ScFS (bu,l1,F1)) . k) = (( ScProductDM L) . (bu,((l1 . (F1 /. k)) * (F1 /. k)))) by C1, defScFSDM;

          

           C3: ( dom ( ScFS (bu,l1,F1))) = ( dom F1) by B14, FINSEQ_3: 29;

          per cases ;

            suppose

             D1: (F1 /. k) <> (( B2DB I) . bu);

            then (F1 /. k) <> u by B31, FUNCT_1: 35;

            then not (F1 /. k) in {u} by TARSKI:def 1;

            then

             D2: not (F1 /. k) in ( Carrier l2) by TARSKI:def 3, VECTSP_6:def 4;

            (l . (F1 /. k)) = ((l1 . (F1 /. k)) + (l2 . (F1 /. k))) by B8, VECTSP_6: 22

            .= ((l1 . (F1 /. k)) + ( 0. INT.Ring )) by D2

            .= (l1 . (F1 /. k));

            

            then

             D3: (( ScFS (bu,l1,F1)) . k) = (( ScProductDM L) . (bu,((l . (F1 /. k)) * (F1 /. k)))) by C1, defScFSDM

            .= (( ScProductDM L) . (((l . (F1 /. k)) * (F1 /. k)),bu)) by ZMODLAT2: 6

            .= ((l . (F1 /. k)) * (( ScProductDM L) . ((F1 /. k),bu))) by ZMODLAT2: 6

            .= ((l . (F1 /. k)) * (( ScProductDM L) . (bu,(F1 /. k)))) by ZMODLAT2: 6;

            (F1 . k) in ( Carrier l1) by B13, C1, C3, FUNCT_1: 3;

            then (F1 . k) in ( Carrier l) by B10, XBOOLE_0:def 5;

            then (F1 . k) in ( DualBasis I) by B21;

            then (F1 /. k) in ( DualBasis I) by C1, C3, PARTFUN1:def 6;

            then

             D7: (F1 /. k) in ( rng ( B2DB I)) by defB2DB;

            then (F1 /. k) in ( dom (( B2DB I) " )) by FUNCT_1: 33;

            then ((( B2DB I) " ) . (F1 /. k)) in ( rng (( B2DB I) " )) by FUNCT_1: 3;

            then ((( B2DB I) " ) . (F1 /. k)) in ( dom ( B2DB I)) by FUNCT_1: 33;

            then

             D6: ((( B2DB I) " ) . (F1 /. k)) in I;

            ( EMLat L) is Submodule of ( DivisibleMod L) by ZMODLAT2: 20;

            then

            reconsider bf = ((( B2DB I) " ) . (F1 /. k)) as Vector of ( DivisibleMod L) by D6, ZMODUL01: 25;

            (( B2DB I) . bf) = (F1 /. k) by D7, FUNCT_1: 35;

            

            then (( ScFS (bu,l1,F1)) . k) = ((l . (F1 /. k)) * ( 0. F_Real )) by B4, D1, D3, D6, defB2DB

            .= ( 0. F_Real );

            

            hence (( ScFS (bu,l1,F1)) . k) = ( - (( ScFS (bu,l1,F1)) . k))

            .= ( - (( ScFS (bu,l1,F1)) /. k)) by C1, PARTFUN1:def 6;

          end;

            suppose (F1 /. k) = (( B2DB I) . bu);

            then (F1 /. k) = u by B31, FUNCT_1: 35;

            

            then (( ScFS (bu,l1,F1)) . k) = (( ScProductDM L) . (bu,(( 0. INT.Ring ) * (F1 /. k)))) by B11, C2

            .= (( ScProductDM L) . (bu,( 0. ( DivisibleMod L)))) by VECTSP_1: 14

            .= ( 0. F_Real ) by ZMODLAT2: 14;

            

            hence (( ScFS (bu,l1,F1)) . k) = ( - (( ScFS (bu,l1,F1)) . k))

            .= ( - (( ScFS (bu,l1,F1)) /. k)) by C1, PARTFUN1:def 6;

          end;

        end;

        then

         B15: ( Sum ( ScFS (bu,l1,F1))) = ( - ( Sum ( ScFS (bu,l1,F1)))) by B14, RLVECT_2: 4;

        

         B16: ( SumSc (bu,l2)) = (( ScProductDM L) . (bu,((l2 . u) * u))) by LmSumScDM14

        .= (( ScProductDM L) . (((l2 . u) * u),bu)) by ZMODLAT2: 6

        .= ((l2 . u) * (( ScProductDM L) . (u,bu))) by ZMODLAT2: 6

        .= ((l2 . u) * (( ScProductDM L) . (bu,u))) by ZMODLAT2: 6

        .= ((l2 . u) * 1) by B4, B12, defB2DB

        .= (l2 . u);

        

         B17: (l . u) = ((l1 . u) + (l2 . u)) by B8, VECTSP_6: 22

        .= (( 0. INT.Ring ) + (l2 . u)) by B11

        .= (l2 . u);

        ( SumSc (bu,l)) = (( SumSc (bu,l1)) + ( SumSc (bu,l2))) by B8, LmSumScDM1X

        .= (l . u) by B13, B15, B16, B17;

        hence contradiction by B1, B2, B5, VECTSP_6: 2, ZMODLAT2: 14;

      end;

    end

    definition

      let L be RATional positive-definite Z_Lattice;

      :: ZMODLAT3:def10

      func DualLat (L) -> strict Z_Lattice means

      : defDualLat: the carrier of it = ( DualSet L) & ( 0. it ) = ( 0. ( DivisibleMod L)) & the addF of it = (the addF of ( DivisibleMod L) || the carrier of it ) & the lmult of it = (the lmult of ( DivisibleMod L) | [:the carrier of INT.Ring , the carrier of it :]) & the scalar of it = (( ScProductDM L) || the carrier of it );

      existence

      proof

        set A = ( DualSet L);

        reconsider A as non empty Subset of ( DivisibleMod L);

        set ad = (the addF of ( DivisibleMod L) || A);

        ( dom the addF of ( DivisibleMod L)) = [:the carrier of ( DivisibleMod L), the carrier of ( DivisibleMod L):] by FUNCT_2:def 1;

        

        then

         A3: ( dom ad) = ( [:the carrier of ( DivisibleMod L), the carrier of ( DivisibleMod L):] /\ [:A, A:]) by RELAT_1: 61

        .= [:A, A:] by XBOOLE_1: 28;

        for x be object st x in [:A, A:] holds (ad . x) in A

        proof

          let x be object;

          assume

           B1: x in [:A, A:];

          then

          consider x1,x2 be object such that

           B2: x1 in A & x2 in A & x = [x1, x2] by ZFMISC_1:def 2;

          reconsider v1 = x1, v2 = x2 as Vector of ( DivisibleMod L) by B2;

          (ad . (x1,x2)) = (v1 + v2) by B1, B2, FUNCT_1: 49;

          hence thesis by B2, VECTSP_4:def 1;

        end;

        then

        reconsider ad as Function of [:A, A:], A by A3, FUNCT_2: 3;

        

         A6: [:the carrier of INT.Ring , A:] c= [:the carrier of INT.Ring , the carrier of ( DivisibleMod L):] by ZFMISC_1: 95;

        set mu = (the lmult of ( DivisibleMod L) | [:the carrier of INT.Ring , A:]);

        ( dom the lmult of ( DivisibleMod L)) = [:the carrier of INT.Ring , the carrier of ( DivisibleMod L):] by FUNCT_2:def 1;

        

        then

         A4: ( dom mu) = ( [:the carrier of INT.Ring , the carrier of ( DivisibleMod L):] /\ [:the carrier of INT.Ring , A:]) by RELAT_1: 61

        .= [:the carrier of INT.Ring , A:] by A6, XBOOLE_1: 28;

        for x be object st x in [:the carrier of INT.Ring , A:] holds (mu . x) in A

        proof

          let x be object;

          assume

           B1: x in [:the carrier of INT.Ring , A:];

          then

          consider x1,x2 be object such that

           B2: x1 in INT & x2 in A & x = [x1, x2] by ZFMISC_1:def 2;

          reconsider i1 = x1 as Element of INT.Ring by B2;

          reconsider v2 = x2 as Vector of ( DivisibleMod L) by B2;

          (mu . (x1,x2)) = (i1 * v2) by B1, B2, FUNCT_1: 49;

          hence thesis by B2, VECTSP_4:def 1;

        end;

        then

        reconsider mu as Function of [:the carrier of INT.Ring , A:], A by A4, FUNCT_2: 3;

        set sc = (( ScProductDM L) || A);

        ( dom ( ScProductDM L)) = [:the carrier of ( DivisibleMod L), the carrier of ( DivisibleMod L):] by FUNCT_2:def 1;

        

        then

         A5: ( dom sc) = ( [:the carrier of ( DivisibleMod L), the carrier of ( DivisibleMod L):] /\ [:A, A:]) by RELAT_1: 61

        .= [:A, A:] by XBOOLE_1: 28;

        for x be object st x in [:A, A:] holds (sc . x) in the carrier of F_Real

        proof

          let x be object;

          assume

           B1: x in [:A, A:];

          then

          consider x1,x2 be object such that

           B2: x1 in A & x2 in A & x = [x1, x2] by ZFMISC_1:def 2;

          reconsider v1 = x1, v2 = x2 as Vector of ( DivisibleMod L) by B2;

          (sc . (x1,x2)) = (( ScProductDM L) . (v1,v2)) by B1, B2, FUNCT_1: 49;

          hence thesis by B2;

        end;

        then

        reconsider sc as Function of [:A, A:], the carrier of F_Real by A5, FUNCT_2: 3;

        reconsider ze = ( 0. ( DivisibleMod L)) as Element of A by ZMODUL01: 18;

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

        reconsider L1 as non empty LatticeStr over INT.Ring ;

        

         A7: L1 is Submodule of ( DivisibleMod L) by ZMODLAT2: 10;

        reconsider L1 as Abelian add-associative right_zeroed right_complementable scalar-distributive vector-distributive scalar-associative scalar-unital non empty LatticeStr over INT.Ring by ZMODLAT2: 10;

        set I = the Basis of ( EMLat L);

        for v be Vector of ( DivisibleMod L) st v in L1 holds v in ( Lin ( DualBasis I))

        proof

          let v be Vector of ( DivisibleMod L) such that

           B1: v in L1;

          consider x be Dual of L such that

           B2: x = v by B1;

          thus thesis by B2, ThDE3;

        end;

        then L1 is Submodule of ( Lin ( DualBasis I)) by A7, ZMODUL01: 44;

        then

        reconsider L1 as strict Z_Lattice by A7, ZMODLAT2: 27;

        take L1;

        thus thesis;

      end;

      uniqueness ;

    end

    theorem :: ZMODLAT3:34

    

     ThDL1: for L be RATional positive-definite Z_Lattice, v be Vector of ( DivisibleMod L) holds v in ( DualLat L) iff v is Dual of L

    proof

      let L be RATional positive-definite Z_Lattice, v be Vector of ( DivisibleMod L);

      hereby

        assume v in ( DualLat L);

        then v in ( DualSet L) by defDualLat;

        then

        consider x be Dual of L such that

         A1: x = v;

        thus v is Dual of L by A1;

      end;

      assume v is Dual of L;

      then v in ( DualSet L);

      hence v in ( DualLat L) by defDualLat;

    end;

    theorem :: ZMODLAT3:35

    

     ThDL2: for L be RATional positive-definite Z_Lattice holds ( DualLat L) is Submodule of ( DivisibleMod L)

    proof

      let L be RATional positive-definite Z_Lattice;

      

       A1: the carrier of ( DualLat L) c= the carrier of ( DivisibleMod L)

      proof

        let x be object such that

         B1: x in the carrier of ( DualLat L);

        x in ( DualSet L) by B1, defDualLat;

        then

        consider v be Dual of L such that

         B2: x = v;

        thus thesis by B2;

      end;

      ( 0. ( DualLat L)) = ( 0. ( DivisibleMod L)) & the addF of ( DualLat L) = (the addF of ( DivisibleMod L) || the carrier of ( DualLat L)) & the lmult of ( DualLat L) = (the lmult of ( DivisibleMod L) | [:the carrier of INT.Ring , the carrier of ( DualLat L):]) by defDualLat;

      hence thesis by A1, VECTSP_4:def 2;

    end;

    theorem :: ZMODLAT3:36

    

     ThELEM1: for L be Z_Lattice, I be Basis of ( EMLat L) holds I is Basis of ( EMbedding L)

    proof

      let L be Z_Lattice, I be Basis of ( EMLat L);

       the ModuleStr of ( EMLat L) = the ModuleStr of ( EMbedding L) by ZMODLAT2: 28;

      hence thesis by ZMODLAT2: 35;

    end;

    theorem :: ZMODLAT3:37

    for L be Z_Lattice, I be Basis of ( EMbedding L) holds I is Basis of ( EMLat L)

    proof

      let L be Z_Lattice, I be Basis of ( EMbedding L);

       the ModuleStr of ( EMLat L) = the ModuleStr of ( EMbedding L) by ZMODLAT2: 28;

      hence thesis by ZMODLAT2: 35;

    end;

    theorem :: ZMODLAT3:38

    

     ThDB2: for L be RATional positive-definite Z_Lattice, I be Basis of ( EMLat L), v be Vector of ( DivisibleMod L) st v in ( DualBasis I) holds v is Dual of L

    proof

      let L be RATional positive-definite Z_Lattice, I be Basis of ( EMLat L), v be Vector of ( DivisibleMod L) such that

       A1: v in ( DualBasis I);

      consider u be Vector of ( EMLat L) such that

       A2: u in I & (( ScProductDM L) . (u,v)) = 1 & (for w be Vector of ( EMLat L) st w in I & u <> w holds (( ScProductDM L) . (w,v)) = 0 ) by A1, defDualBasis;

      reconsider J = I as Basis of ( EMbedding L) by ThELEM1;

      for w be Vector of ( DivisibleMod L) st w in J holds (( ScProductDM L) . (v,w)) in INT.Ring

      proof

        let w be Vector of ( DivisibleMod L) such that

         B1: w in J;

        per cases ;

          suppose u <> w;

          then (( ScProductDM L) . (w,v)) = 0 by A2, B1;

          then (( ScProductDM L) . (v,w)) = 0 by ZMODLAT2: 6;

          hence thesis;

        end;

          suppose u = w;

          then (( ScProductDM L) . (v,w)) = 1 by A2, ZMODLAT2: 6;

          hence thesis;

        end;

      end;

      hence thesis by LmDE21;

    end;

    theorem :: ZMODLAT3:39

    

     ThDLDB: for L be RATional positive-definite Z_Lattice, I be Basis of ( EMLat L) holds ( DualBasis I) is Basis of ( DualLat L)

    proof

      let L be RATional positive-definite Z_Lattice, I be Basis of ( EMLat L);

      reconsider DL = ( DualLat L) as Submodule of ( DivisibleMod L) by ThDL2;

      for v be Vector of ( DivisibleMod L) st v in ( DualBasis I) holds v in the carrier of ( DualLat L)

      proof

        let v be Vector of ( DivisibleMod L) such that

         B1: v in ( DualBasis I);

        v in ( DualLat L) by B1, ThDB2, ThDL1;

        hence thesis;

      end;

      then ( DualBasis I) c= the carrier of ( DualLat L);

      then

      reconsider DB = ( DualBasis I) as linearly-independent Subset of DL by ZMODUL03: 16;

      

       A2: for v be Vector of ( DivisibleMod L) st v in the ModuleStr of DL holds v in ( Lin ( DualBasis I))

      proof

        let v be Vector of ( DivisibleMod L) such that

         B1: v in the ModuleStr of DL;

        v in ( DualLat L) by B1;

        hence thesis by ThDE3, ThDL1;

      end;

      

       A3: for v be Vector of ( DivisibleMod L) st v in ( Lin ( DualBasis I)) holds v in the ModuleStr of DL

      proof

        let v be Vector of ( DivisibleMod L) such that

         B1: v in ( Lin ( DualBasis I));

        consider l be Linear_Combination of ( DualBasis I) such that

         B2: v = ( Sum l) by B1, VECTSP_7: 7;

        reconsider J = I as Basis of ( EMbedding L) by ThELEM1;

        for u be Vector of ( DivisibleMod L) st u in J holds (( ScProductDM L) . (v,u)) in INT.Ring

        proof

          let u be Vector of ( DivisibleMod L) such that

           C1: u in J;

          

           C2: (( ScProductDM L) . (u,v)) = (l . (( B2DB I) . u)) by B2, C1, LmDE32;

          u in ( dom ( B2DB I)) by C1, defB2DB;

          then (( B2DB I) . u) in ( rng ( B2DB I)) by FUNCT_1: 3;

          then (( B2DB I) . u) in ( DualBasis I);

          then (l . (( B2DB I) . u)) in the carrier of INT.Ring by FUNCT_2: 5;

          hence thesis by C2, ZMODLAT2: 6;

        end;

        then v in DL by LmDE21, ThDL1;

        hence thesis;

      end;

      ( (Omega). DL) is Submodule of DL;

      then the ModuleStr of DL is Submodule of ( DivisibleMod L) by ZMODUL01: 42;

      

      then the ModuleStr of ( DualLat L) = ( Lin ( DualBasis I)) by A2, A3, ZMODUL01: 46

      .= ( Lin DB) by ZMODUL03: 20;

      hence thesis by VECTSP_7:def 3;

    end;

    theorem :: ZMODLAT3:40

    for L be RATional positive-definite Z_Lattice, b be OrdBasis of ( EMLat L), I be Basis of ( EMLat L) st I = ( rng b) holds (( B2DB I) * b) is OrdBasis of ( DualLat L)

    proof

      let L be RATional positive-definite Z_Lattice, b be OrdBasis of ( EMLat L), I be Basis of ( EMLat L) such that

       A1: I = ( rng b);

      

       A2: b is one-to-one by ZMATRLIN:def 5;

      b is FinSequence of I by A1, FINSEQ_1:def 4;

      then

       A3: (( B2DB I) * b) is FinSequence of ( DualBasis I) by FINSEQ_2: 32;

      

       A4: ( dom ( B2DB I)) = I by defB2DB;

      

       A5: ( rng (( B2DB I) * b)) = (( B2DB I) .: ( rng b)) by RELAT_1: 127

      .= ( rng ( B2DB I)) by A1, A4, RELAT_1: 113

      .= ( DualBasis I) by defB2DB;

      ( DualBasis I) is Subset of ( DualLat L) by ThDLDB;

      then

       A6: (( B2DB I) * b) is FinSequence of ( DualLat L) by A3, A5, FINSEQ_1:def 4;

      ( rng (( B2DB I) * b)) is Basis of ( DualLat L) by A5, ThDLDB;

      hence thesis by A2, A6, ZMATRLIN:def 5;

    end;

    theorem :: ZMODLAT3:41

    

     LmEMDetX3: for L be positive-definite finite-rank free Z_Lattice, b be OrdBasis of L, e be OrdBasis of ( EMLat L) st e = (( MorphsZQ L) * b) holds ( GramMatrix (( InnerProduct L),b)) = ( GramMatrix (( InnerProduct ( EMLat L)),e))

    proof

      let L be positive-definite finite-rank free Z_Lattice, b be OrdBasis of L, e be OrdBasis of ( EMLat L);

      assume

       AS: e = (( MorphsZQ L) * b);

      

       R1: ( rank L) = ( rank ( EMLat L)) by ZMODLAT2: 42;

      

       R2: ( len ( GramMatrix (( InnerProduct L),b))) = ( rank L) & ( width ( GramMatrix (( InnerProduct L),b))) = ( rank L) & ( Indices ( GramMatrix (( InnerProduct L),b))) = [:( Seg ( rank L)), ( Seg ( rank L)):] by MATRIX_0: 24;

      

       S2: ( len ( GramMatrix (( InnerProduct ( EMLat L)),e))) = ( rank ( EMLat L)) & ( width ( GramMatrix (( InnerProduct ( EMLat L)),e))) = ( rank ( EMLat L)) & ( Indices ( GramMatrix (( InnerProduct ( EMLat L)),e))) = [:( Seg ( rank ( EMLat L))), ( Seg ( rank ( EMLat L))):] by MATRIX_0: 24;

      for i,j be Nat st [i, j] in ( Indices ( GramMatrix (( InnerProduct L),b))) holds (( GramMatrix (( InnerProduct L),b)) * (i,j)) = (( GramMatrix (( InnerProduct ( EMLat L)),e)) * (i,j))

      proof

        let i,j be Nat;

        assume [i, j] in ( Indices ( GramMatrix (( InnerProduct L),b)));

        then

         X1: i in ( Seg ( rank L)) & j in ( Seg ( rank L)) by R2, ZFMISC_1: 87;

        then

         A2: i in ( dom b) & j in ( dom b) by R2, FINSEQ_1:def 3, MATRIX_0: 24;

        then

         A3: (( GramMatrix (( InnerProduct L),b)) * (i,j)) = (( InnerProduct L) . ((b /. i),(b /. j))) by ZMODLAT1:def 32;

        

         A4: i in ( dom e) & j in ( dom e) by R1, S2, X1, FINSEQ_1:def 3, MATRIX_0: 24;

        

         Y0: the carrier of ( EMLat L) = ( rng ( MorphsZQ L)) by ZMODLAT2:def 4

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

        

         Y1: (e /. i) = (e . i) by A4, PARTFUN1:def 6

        .= (( MorphsZQ L) . (b . i)) by A2, AS, FUNCT_1: 13

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

        

         Y2: (e /. j) = (e . j) by A4, PARTFUN1:def 6

        .= (( MorphsZQ L) . (b . j)) by A2, AS, FUNCT_1: 13

        .= (( MorphsZQ L) . (b /. j)) by A2, PARTFUN1:def 6;

        reconsider ei = (e /. i), ej = (e /. j) as Vector of ( EMbedding L) by Y0;

        (( InnerProduct ( EMLat L)) . ((e /. i),(e /. j))) = (( ScProductEM L) . (ei,ej)) by ZMODLAT2:def 4

        .= <;(b /. i), (b /. j);> by Y1, Y2, ZMODLAT2:def 2

        .= (( InnerProduct L) . ((b /. i),(b /. j)));

        hence thesis by A3, A4, ZMODLAT1:def 32;

      end;

      hence thesis by MATRIX_0: 27, R1;

    end;

    theorem :: ZMODLAT3:42

    for L be positive-definite finite-rank free Z_Lattice holds ( GramDet ( InnerProduct L)) = ( GramDet ( InnerProduct ( EMLat L)))

    proof

      let L be positive-definite finite-rank free Z_Lattice;

      set b = the OrdBasis of L;

      reconsider e = (( MorphsZQ L) * b) as OrdBasis of ( EMLat L) by ZMODLAT2: 41;

      

       P1: ( GramMatrix (( InnerProduct L),b)) = ( GramMatrix (( InnerProduct ( EMLat L)),e)) by LmEMDetX3;

      ( GramDet ( InnerProduct L)) = ( Det ( GramMatrix (( InnerProduct L),b))) by ZMODLAT1:def 35

      .= ( Det ( GramMatrix (( InnerProduct ( EMLat L)),e))) by P1, ZMODLAT2: 42

      .= ( GramDet ( InnerProduct ( EMLat L))) by ZMODLAT1:def 35;

      hence thesis;

    end;

    theorem :: ZMODLAT3:43

    

     ThRankDL: for L be RATional positive-definite Z_Lattice holds ( rank L) = ( rank ( DualLat L))

    proof

      let L be RATional positive-definite Z_Lattice;

      set I = the Basis of ( EMLat L);

      ( DualBasis I) is Basis of ( DualLat L) by ThDLDB;

      

      then ( rank ( DualLat L)) = ( card ( DualBasis I)) by ZMODUL03:def 5

      .= ( card I) by ThDB1

      .= ( rank ( EMLat L)) by ZMODUL03:def 5;

      hence thesis by ZMODLAT2: 42;

    end;

    theorem :: ZMODLAT3:44

    for L be INTegral positive-definite Z_Lattice holds ( EMLat L) is Z_Sublattice of ( DualLat L)

    proof

      let L be INTegral positive-definite Z_Lattice;

      

       A1: ( EMLat L) is Submodule of ( DivisibleMod L) by ZMODLAT2: 20;

      

       A2: ( DualLat L) is Submodule of ( DivisibleMod L) by ThDL2;

      for v be Vector of ( DivisibleMod L) st v in ( EMLat L) holds v in ( DualLat L)

      proof

        let v be Vector of ( DivisibleMod L) such that

         B1: v in ( EMLat L);

        set I = the Basis of ( EMLat L);

        reconsider J = I as Basis of ( EMbedding L) by ThELEM1;

        for u be Vector of ( DivisibleMod L) st u in J holds (( ScProductDM L) . (v,u)) in INT.Ring

        proof

          let u be Vector of ( DivisibleMod L) such that

           C1: u in J;

          reconsider vv = v as Vector of ( EMLat L) by B1;

          reconsider uu = u as Vector of ( EMLat L) by C1;

           the ModuleStr of ( EMLat L) = ( EMbedding L) by ZMODLAT2: 28;

          

          then (( ScProductDM L) . (v,u)) = (( ScProductEM L) . (vv,uu)) by ZMODLAT2: 8

          .= <;vv, uu;> by ZMODLAT2:def 4;

          hence thesis by ZMODLAT1:def 5;

        end;

        hence thesis by LmDE21, ThDL1;

      end;

      then ( EMLat L) is Submodule of ( DualLat L) by A1, A2, ZMODUL01: 44;

      then

       A3: the carrier of ( EMLat L) c= the carrier of ( DualLat L) & ( 0. ( EMLat L)) = ( 0. ( DualLat L)) & the addF of ( EMLat L) = (the addF of ( DualLat L) || the carrier of ( EMLat L)) & the lmult of ( EMLat L) = (the lmult of ( DualLat L) | [:the carrier of INT.Ring , the carrier of ( EMLat L):]) by VECTSP_4:def 2;

      

       A4: [:the carrier of ( EMLat L), the carrier of ( EMLat L):] c= [:the carrier of ( DualLat L), the carrier of ( DualLat L):] by A3, ZFMISC_1: 96;

      (the scalar of ( DualLat L) || the carrier of ( EMLat L)) = ((( ScProductDM L) || the carrier of ( DualLat L)) || the carrier of ( EMLat L)) by defDualLat

      .= (( ScProductDM L) || the carrier of ( EMLat L)) by A4, FUNCT_1: 51

      .= (( ScProductDM L) || ( rng ( MorphsZQ L))) by ZMODLAT2:def 4

      .= ( ScProductEM L) by ZMODLAT2: 7

      .= the scalar of ( EMLat L) by ZMODLAT2:def 4;

      hence thesis by A3, ZMODLAT1:def 9;

    end;

    theorem :: ZMODLAT3:45

    for L be Z_Lattice, b be OrdBasis of L st ( GramMatrix (( InnerProduct L),b)) is Matrix of ( dim L), INT.Ring holds L is INTegral

    proof

      let L be Z_Lattice, b be OrdBasis of L such that

       A1: ( GramMatrix (( InnerProduct L),b)) is Matrix of ( dim L), INT.Ring ;

      set I = ( rng b);

      reconsider I as Basis of L by ZMATRLIN:def 5;

      set GM = ( GramMatrix (( InnerProduct L),b));

      reconsider GMI = GM as Matrix of ( dim L), INT.Ring by A1;

      for v,u be Vector of L st v in I & u in I holds <;v, u;> in INT

      proof

        let v,u be Vector of L such that

         B1: v in I & u in I;

        consider i be Nat such that

         B2: i in ( dom b) & (b . i) = v by B1, FINSEQ_2: 10;

        consider j be Nat such that

         B3: j in ( dom b) & (b . j) = u by B1, FINSEQ_2: 10;

        

         B4: (b /. i) = v by B2, PARTFUN1:def 6;

        

         B6: (GM * (i,j)) = (( InnerProduct L) . ((b /. i),(b /. j))) by B2, B3, ZMODLAT1:def 32

        .= <;v, u;> by B3, B4, PARTFUN1:def 6;

        

         B7: ( dom b) = ( Seg ( len b)) by FINSEQ_1:def 3

        .= ( Seg ( dim L)) by ZMATRLIN: 49;

        ( Indices GM) = [:( Seg ( dim L)), ( Seg ( dim L)):] by MATRIX_0: 24;

        then [i, j] in ( Indices GM) by B2, B3, B7, ZFMISC_1: 87;

        then (GM * (i,j)) = (GMI * (i,j)) by ZMATRLIN: 1;

        hence thesis by B6;

      end;

      hence thesis by ZMODLAT1: 15;

    end;

    theorem :: ZMODLAT3:46

    

     ThRatLat1B: for L be Z_Lattice, I be finite Subset of L, u be Vector of L st for v be Vector of L st v in I holds <;v, u;> in RAT holds for v be Vector of L st v in ( Lin I) holds <;v, u;> in RAT

    proof

      let L be Z_Lattice, I be finite Subset of L, u be Vector of L;

      assume

       AS: for v be Vector of L st v in I holds <;v, u;> in RAT ;

      defpred P[ Nat] means for I be finite Subset of L st ( card I) = $1 & for v be Vector of L st v in I holds <;v, u;> in RAT holds for v be Vector of L st v in ( Lin I) holds <;v, u;> in RAT ;

      

       P1: P[ 0 ]

      proof

        let I be finite Subset of L;

        assume ( card I) = 0 & for v be Vector of L st v in I holds <;v, u;> in RAT ;

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

        then

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

        let v be Vector of L;

        assume v in ( Lin I);

        then v in {( 0. L)} by A2, VECTSP_4:def 3;

        then v = ( 0. L) by TARSKI:def 1;

        then <;v, u;> = 0 by ZMODLAT1: 12;

        hence <;v, u;> in RAT by RAT_1:def 2;

      end;

      

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

      proof

        let n be Nat;

        assume

         A0: P[n];

        let I be finite Subset of L;

        assume

         A1: ( card I) = (n + 1) & for v be Vector of L st v in I holds <;v, u;> in RAT ;

        then I <> {} ;

        then

        consider v be object such that

         A3: v in I by XBOOLE_0:def 1;

        reconsider v as Vector of L by A3;

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

        .= I by A3, ZFMISC_1: 40;

        then

         A4: ( Lin I) = (( Lin (I \ {v})) + ( Lin {v})) by ZMODUL02: 72;

        

         A5: ( card (I \ {v})) = (( card I) - ( card {v})) by A3, CARD_2: 44, ZFMISC_1: 31

        .= (( card I) - 1) by CARD_1: 30

        .= n by A1;

        reconsider J = (I \ {v}) as finite Subset of L;

        

         B8: for x be Vector of L st x in J holds <;x, u;> in RAT

        proof

          let x be Vector of L;

          assume x in J;

          then x in I by XBOOLE_1: 36, TARSKI:def 3;

          hence <;x, u;> in RAT by A1;

        end;

        thus for x be Vector of L st x in ( Lin I) holds <;x, u;> in RAT

        proof

          let x be Vector of L;

          assume x in ( Lin I);

          then

          consider xu1,xu2 be Vector of L such that

           A10: xu1 in ( Lin (I \ {v})) & xu2 in ( Lin {v}) & x = (xu1 + xu2) by A4, ZMODUL01: 92;

          consider ixu2 be Element of INT.Ring such that

           A12: xu2 = (ixu2 * v) by A10, ZMODUL06: 19;

          

           B11: x = ((( 1. INT.Ring ) * xu1) + (ixu2 * v)) by A10, A12, VECTSP_1:def 17;

          set i1 = ( 1. INT.Ring );

          

           B13: <;x, u;> = ((i1 * <;xu1, u;>) + (ixu2 * <;v, u;>)) by B11, ZMODLAT1: 10;

          

           B14: <;xu1, u;> in RAT by A0, A5, B8, A10;

           <;v, u;> in RAT by A1, A3;

          hence <;x, u;> in RAT by B13, B14, RAT_1:def 2;

        end;

      end;

      

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

      ( card I) is Nat;

      hence thesis by X1, AS;

    end;

    theorem :: ZMODLAT3:47

    

     ThRatLat1A: for L be Z_Lattice, I be Basis of L st for v,u be Vector of L st v in I & u in I holds <;v, u;> in RAT holds for v,u be Vector of L holds <;v, u;> in RAT

    proof

      let L be Z_Lattice;

      defpred P[ Nat] means for I be finite Subset of L st ( card I) = $1 & for v,u be Vector of L st v in I & u in I holds <;v, u;> in RAT holds for v,u be Vector of L st v in ( Lin I) & u in ( Lin I) holds <;v, u;> in RAT ;

      

       P1: P[ 0 ]

      proof

        let I be finite Subset of L;

        assume ( card I) = 0 & for v,u be Vector of L st v in I & u in I holds <;v, u;> in RAT ;

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

        then

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

        let v,u be Vector of L;

        assume v in ( Lin I) & u in ( Lin I);

        then v in {( 0. L)} & u in {( 0. L)} by A2, VECTSP_4:def 3;

        then v = ( 0. L) & u = ( 0. L) by TARSKI:def 1;

        then <;v, u;> = 0 by ZMODLAT1: 12;

        hence <;v, u;> in RAT by RAT_1:def 2;

      end;

      

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

      proof

        let n be Nat;

        assume

         A0: P[n];

        let I be finite Subset of L;

        assume

         A1: ( card I) = (n + 1) & for v,u be Vector of L st v in I & u in I holds <;v, u;> in RAT ;

        then I <> {} ;

        then

        consider v be object such that

         A3: v in I by XBOOLE_0:def 1;

        reconsider v as Vector of L by A3;

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

        .= I by A3, ZFMISC_1: 40;

        then

         A4: ( Lin I) = (( Lin (I \ {v})) + ( Lin {v})) by ZMODUL02: 72;

        

         A5: ( card (I \ {v})) = (( card I) - ( card {v})) by A3, CARD_2: 44, ZFMISC_1: 31

        .= (( card I) - 1) by CARD_1: 30

        .= n by A1;

        reconsider J = (I \ {v}) as finite Subset of L;

        

         B8: for x,y be Vector of L st x in J & y in J holds <;x, y;> in RAT

        proof

          let x,y be Vector of L;

          assume x in J & y in J;

          then x in I & y in I by XBOOLE_1: 36, TARSKI:def 3;

          hence <;x, y;> in RAT by A1;

        end;

        

         A6X: for x be Vector of L st x in J holds <;x, v;> in RAT

        proof

          let x be Vector of L;

          assume x in J;

          then x in I & v in I by A3, XBOOLE_1: 36, TARSKI:def 3;

          hence <;x, v;> in RAT by A1;

        end;

        thus for x,y be Vector of L st x in ( Lin I) & y in ( Lin I) holds <;x, y;> in RAT

        proof

          let x,y be Vector of L;

          assume

           A9: x in ( Lin I) & y in ( Lin I);

          then

          consider xu1,xu2 be Vector of L such that

           A10: xu1 in ( Lin (I \ {v})) & xu2 in ( Lin {v}) & x = (xu1 + xu2) by A4, ZMODUL01: 92;

          consider yu1,yu2 be Vector of L such that

           A11: yu1 in ( Lin (I \ {v})) & yu2 in ( Lin {v}) & y = (yu1 + yu2) by A9, A4, ZMODUL01: 92;

          consider ixu2 be Element of INT.Ring such that

           A12: xu2 = (ixu2 * v) by A10, ZMODUL06: 19;

          consider iyu2 be Element of INT.Ring such that

           A13: yu2 = (iyu2 * v) by A11, ZMODUL06: 19;

          

           B11: x = ((( 1. INT.Ring ) * xu1) + (ixu2 * v)) by A10, A12, VECTSP_1:def 17;

          set i1 = ( 1. INT.Ring );

          

           B13: <;x, y;> = ( <;((i1 * xu1) + (ixu2 * v)), yu1;> + <;((i1 * xu1) + (ixu2 * v)), (iyu2 * v);>) by A11, A13, B11, ZMODLAT1: 8

          .= (((i1 * <;xu1, yu1;>) + (ixu2 * <;v, yu1;>)) + <;((i1 * xu1) + (ixu2 * v)), (iyu2 * v);>) by ZMODLAT1: 10

          .= (((i1 * <;xu1, yu1;>) + (ixu2 * <;v, yu1;>)) + ((i1 * <;xu1, (iyu2 * v);>) + (ixu2 * <;v, (iyu2 * v);>))) by ZMODLAT1: 10

          .= ((( <;xu1, yu1;> + (ixu2 * <;v, yu1;>)) + <;xu1, (iyu2 * v);>) + (ixu2 * <;v, (iyu2 * v);>))

          .= ((( <;xu1, yu1;> + (ixu2 * <;v, yu1;>)) + <;xu1, (iyu2 * v);>) + (ixu2 * (iyu2 * <;v, v;>))) by ZMODLAT1: 9

          .= ((( <;xu1, yu1;> + (ixu2 * <;v, yu1;>)) + (iyu2 * <;xu1, v;>)) + ((ixu2 * iyu2) * <;v, v;>)) by ZMODLAT1: 9;

          

           B14: <;xu1, yu1;> in RAT by A0, A5, B8, A10, A11;

           <;yu1, v;> in RAT by A11, A6X, ThRatLat1B;

          then

           B15: <;v, yu1;> in RAT by ZMODLAT1:def 3;

          

           B16: <;xu1, v;> in RAT by A10, A6X, ThRatLat1B;

           <;v, v;> in RAT by A3, A1;

          hence <;x, y;> in RAT by B13, B14, B15, B16, RAT_1:def 2;

        end;

      end;

      

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

      let I be Basis of L;

      assume

       X2: for v,u be Vector of L st v in I & u in I holds <;v, u;> in RAT ;

      

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

      

       X4: ( card I) is Nat;

      let v,u be Vector of L;

      v in ( Lin I) & u in ( Lin I) by X3;

      hence <;v, u;> in RAT by X1, X2, X4;

    end;

    theorem :: ZMODLAT3:48

    

     ThRatLat1: for L be Z_Lattice, I be Basis of L st for v,u be Vector of L st v in I & u in I holds <;v, u;> in RAT holds L is RATional

    proof

      let L be Z_Lattice, I be Basis of L such that

       A1: for v,u be Vector of L st v in I & u in I holds <;v, u;> in RAT ;

      for v,u be Vector of L holds <;v, u;> in RAT by A1, ThRatLat1A;

      hence thesis by ZMODLAT2:def 1;

    end;

    theorem :: ZMODLAT3:49

    for L be Z_Lattice, b be OrdBasis of L st ( GramMatrix (( InnerProduct L),b)) is Matrix of ( dim L), F_Rat holds L is RATional

    proof

      let L be Z_Lattice, b be OrdBasis of L such that

       A1: ( GramMatrix (( InnerProduct L),b)) is Matrix of ( dim L), F_Rat ;

      set I = ( rng b);

      reconsider I as Basis of L by ZMATRLIN:def 5;

      set GM = ( GramMatrix (( InnerProduct L),b));

      reconsider GMR = GM as Matrix of ( dim L), F_Rat by A1;

      for v,u be Vector of L st v in I & u in I holds <;v, u;> in RAT

      proof

        let v,u be Vector of L such that

         B1: v in I & u in I;

        consider i be Nat such that

         B2: i in ( dom b) & (b . i) = v by B1, FINSEQ_2: 10;

        consider j be Nat such that

         B3: j in ( dom b) & (b . j) = u by B1, FINSEQ_2: 10;

        

         B4: (b /. i) = v by B2, PARTFUN1:def 6;

        

         B6: (GM * (i,j)) = (( InnerProduct L) . ((b /. i),(b /. j))) by B2, B3, ZMODLAT1:def 32

        .= <;v, u;> by B3, B4, PARTFUN1:def 6;

        

         B7: ( dom b) = ( Seg ( len b)) by FINSEQ_1:def 3

        .= ( Seg ( dim L)) by ZMATRLIN: 49;

        ( Indices GM) = [:( Seg ( dim L)), ( Seg ( dim L)):] by MATRIX_0: 24;

        then [i, j] in ( Indices GM) by B2, B3, B7, ZFMISC_1: 87;

        then (GM * (i,j)) = (GMR * (i,j)) by ZMATRLIN: 1;

        hence thesis by B6;

      end;

      hence thesis by ThRatLat1;

    end;

    registration

      let L be RATional positive-definite Z_Lattice;

      cluster ( DualLat L) -> RATional;

      correctness

      proof

        

         A1: the scalar of ( DualLat L) = (( ScProductDM L) || the carrier of ( DualLat L)) by defDualLat;

        ( DualLat L) is Submodule of ( DivisibleMod L) by ThDL2;

        hence thesis by A1, ThSLGM1;

      end;

    end

    theorem :: ZMODLAT3:50

    

     ThSLGM2: for L be RATional Z_Lattice, LX be Z_Lattice, b be OrdBasis of LX st LX is Submodule of ( DivisibleMod L) & the scalar of LX = (( ScProductDM L) || the carrier of LX) holds ( GramMatrix (( InnerProduct LX),b)) is Matrix of ( dim LX), F_Rat

    proof

      let L be RATional Z_Lattice, LX be Z_Lattice, b be OrdBasis of LX such that

       A1: LX is Submodule of ( DivisibleMod L) & the scalar of LX = (( ScProductDM L) || the carrier of LX);

      LX is RATional by A1, ThSLGM1;

      then ( GramMatrix b) is Matrix of ( dim LX), F_Rat by ZMODLAT2: 45;

      hence thesis;

    end;

    theorem :: ZMODLAT3:51

    for L be RATional positive-definite Z_Lattice, b be OrdBasis of ( DualLat L) holds ( GramMatrix (( InnerProduct ( DualLat L)),b)) is Matrix of ( dim L), F_Rat

    proof

      let L be RATional positive-definite Z_Lattice, b be OrdBasis of ( DualLat L);

      

       A1: the scalar of ( DualLat L) = (( ScProductDM L) || the carrier of ( DualLat L)) by defDualLat;

      

       A2: ( DualLat L) is Submodule of ( DivisibleMod L) by ThDL2;

      ( dim L) = ( dim ( DualLat L)) by ThRankDL;

      hence thesis by A1, A2, ThSLGM2;

    end;

    theorem :: ZMODLAT3:52

    

     ThSLGM3: for L be positive-definite Z_Lattice, LX be Z_Lattice st LX is Submodule of ( DivisibleMod L) & the scalar of LX = (( ScProductDM L) || the carrier of LX) holds LX is positive-definite

    proof

      let L be positive-definite Z_Lattice, LX be Z_Lattice such that

       A1: LX is Submodule of ( DivisibleMod L) & the scalar of LX = (( ScProductDM L) || the carrier of LX);

      for v be Vector of LX st v <> ( 0. LX) holds ||.v.|| > 0

      proof

        let v be Vector of LX such that

         B1: v <> ( 0. LX);

        reconsider vv = v as Vector of ( DivisibleMod L) by A1, ZMODUL01: 25;

        

         B3: ||.v.|| = (( ScProductDM L) . (vv,vv)) by A1, FUNCT_1: 49;

        consider i be Element of INT.Ring such that

         B4: i <> 0 & (i * vv) in ( EMbedding L) by ZMODUL08: 29;

        (i * vv) in ( rng ( MorphsZQ L)) by B4, ZMODUL08:def 3;

        then

        reconsider iv = (i * vv) as Vector of ( EMLat L) by ZMODLAT2:def 4;

        

         B5: ((i * i) * ||.v.||) = (i * (i * (( ScProductDM L) . (vv,vv)))) by B3

        .= (i * (( ScProductDM L) . (vv,(i * vv)))) by ZMODLAT2: 13

        .= (( ScProductDM L) . ((i * vv),(i * vv))) by ZMODLAT2: 6

        .= (( ScProductEM L) . (iv,iv)) by B4, ZMODLAT2: 8

        .= ||.iv.|| by ZMODLAT2:def 4;

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

        then (i * v) <> ( 0. LX) by B1, ZMODUL01:def 7;

        then (i * vv) <> ( 0. LX) by A1, ZMODUL01: 29;

        then iv <> ( 0. ( DivisibleMod L)) by A1, VECTSP_4:def 2;

        then iv <> ( zeroCoset L) by ZMODUL08:def 4;

        then iv <> ( 0. ( EMLat L)) by ZMODLAT2:def 4;

        then ||.iv.|| > 0 by ZMODLAT1:def 6;

        hence ||.v.|| > 0 by B5, XREAL_1: 63, XREAL_1: 131;

      end;

      hence thesis;

    end;

    registration

      let L be RATional positive-definite Z_Lattice;

      cluster ( DualLat L) -> positive-definite;

      correctness

      proof

        

         A1: ( DualLat L) is Submodule of ( DivisibleMod L) by ThDL2;

        the scalar of ( DualLat L) = (( ScProductDM L) || the carrier of ( DualLat L)) by defDualLat;

        hence thesis by A1, ThSLGM3;

      end;

    end

    registration

      let L be non trivial RATional positive-definite Z_Lattice;

      cluster ( DualLat L) -> non trivial;

      correctness

      proof

        ( rank L) > 0 ;

        then ( rank ( DualLat L)) <> 0 by ThRankDL;

        then ( (Omega). ( DualLat L)) <> ( (0). ( DualLat L)) by ZMODUL05: 1;

        hence thesis by ZMODUL07: 41;

      end;

    end