set A = DualSet L;

reconsider A = DualSet L 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 ( the addF of (DivisibleMod L) || A) = [: the carrier of (DivisibleMod L), the carrier of (DivisibleMod L):] /\ [:A,A:] by RELAT_1:61

.= [:A,A:] by XBOOLE_1:28 ;

for x being object st x in [:A,A:] holds

( the addF of (DivisibleMod L) || A) . x in A

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 ( the lmult of (DivisibleMod L) | [: the carrier of INT.Ring,A:]) = [: 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 being object st x in [: the carrier of INT.Ring,A:] holds

( the lmult of (DivisibleMod L) | [: the carrier of INT.Ring,A:]) . x in A

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 ((ScProductDM L) || A) = [: the carrier of (DivisibleMod L), the carrier of (DivisibleMod L):] /\ [:A,A:] by RELAT_1:61

.= [:A,A:] by XBOOLE_1:28 ;

for x being object st x in [:A,A:] holds

((ScProductDM L) || A) . x in the carrier of F_Real

reconsider ze = 0. (DivisibleMod L) as Element of A by ZMODUL01:18;

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

reconsider L1 = LatticeStr(# A,ad,ze,mu,sc #) as non empty LatticeStr over INT.Ring ;

A7: L1 is Submodule of DivisibleMod L by ZMODLAT2:10;

reconsider L1 = L1 as non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed LatticeStr over INT.Ring by ZMODLAT2:10;

set I = the Basis of (EMLat L);

for v being Vector of (DivisibleMod L) st v in L1 holds

v in Lin (DualBasis the Basis of (EMLat L))

then reconsider L1 = L1 as strict Z_Lattice by A7, ZMODLAT2:27;

take L1 ; :: thesis: ( the carrier of L1 = DualSet L & 0. L1 = 0. (DivisibleMod L) & the addF of L1 = the addF of (DivisibleMod L) || the carrier of L1 & the lmult of L1 = the lmult of (DivisibleMod L) | [: the carrier of INT.Ring, the carrier of L1:] & the scalar of L1 = (ScProductDM L) || the carrier of L1 )

thus ( the carrier of L1 = DualSet L & 0. L1 = 0. (DivisibleMod L) & the addF of L1 = the addF of (DivisibleMod L) || the carrier of L1 & the lmult of L1 = the lmult of (DivisibleMod L) | [: the carrier of INT.Ring, the carrier of L1:] & the scalar of L1 = (ScProductDM L) || the carrier of L1 ) ; :: thesis: verum

reconsider A = DualSet L 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 ( the addF of (DivisibleMod L) || A) = [: the carrier of (DivisibleMod L), the carrier of (DivisibleMod L):] /\ [:A,A:] by RELAT_1:61

.= [:A,A:] by XBOOLE_1:28 ;

for x being object st x in [:A,A:] holds

( the addF of (DivisibleMod L) || A) . x in A

proof

then reconsider ad = the addF of (DivisibleMod L) || A as Function of [:A,A:],A by A3, FUNCT_2:3;
let x be object ; :: thesis: ( x in [:A,A:] implies ( the addF of (DivisibleMod L) || A) . x in A )

assume B1: x in [:A,A:] ; :: thesis: ( the addF of (DivisibleMod L) || A) . x in A

then consider x1, x2 being 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;

( the addF of (DivisibleMod L) || A) . (x1,x2) = v1 + v2 by B1, B2, FUNCT_1:49;

hence ( the addF of (DivisibleMod L) || A) . x in A by B2, VECTSP_4:def 1; :: thesis: verum

end;assume B1: x in [:A,A:] ; :: thesis: ( the addF of (DivisibleMod L) || A) . x in A

then consider x1, x2 being 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;

( the addF of (DivisibleMod L) || A) . (x1,x2) = v1 + v2 by B1, B2, FUNCT_1:49;

hence ( the addF of (DivisibleMod L) || A) . x in A by B2, VECTSP_4:def 1; :: thesis: verum

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 ( the lmult of (DivisibleMod L) | [: the carrier of INT.Ring,A:]) = [: 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 being object st x in [: the carrier of INT.Ring,A:] holds

( the lmult of (DivisibleMod L) | [: the carrier of INT.Ring,A:]) . x in A

proof

then reconsider mu = the lmult of (DivisibleMod L) | [: the carrier of INT.Ring,A:] as Function of [: the carrier of INT.Ring,A:],A by A4, FUNCT_2:3;
let x be object ; :: thesis: ( x in [: the carrier of INT.Ring,A:] implies ( the lmult of (DivisibleMod L) | [: the carrier of INT.Ring,A:]) . x in A )

assume B1: x in [: the carrier of INT.Ring,A:] ; :: thesis: ( the lmult of (DivisibleMod L) | [: the carrier of INT.Ring,A:]) . x in A

then consider x1, x2 being 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;

( the lmult of (DivisibleMod L) | [: the carrier of INT.Ring,A:]) . (x1,x2) = i1 * v2 by B1, B2, FUNCT_1:49;

hence ( the lmult of (DivisibleMod L) | [: the carrier of INT.Ring,A:]) . x in A by B2, VECTSP_4:def 1; :: thesis: verum

end;assume B1: x in [: the carrier of INT.Ring,A:] ; :: thesis: ( the lmult of (DivisibleMod L) | [: the carrier of INT.Ring,A:]) . x in A

then consider x1, x2 being 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;

( the lmult of (DivisibleMod L) | [: the carrier of INT.Ring,A:]) . (x1,x2) = i1 * v2 by B1, B2, FUNCT_1:49;

hence ( the lmult of (DivisibleMod L) | [: the carrier of INT.Ring,A:]) . x in A by B2, VECTSP_4:def 1; :: thesis: verum

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 ((ScProductDM L) || A) = [: the carrier of (DivisibleMod L), the carrier of (DivisibleMod L):] /\ [:A,A:] by RELAT_1:61

.= [:A,A:] by XBOOLE_1:28 ;

for x being object st x in [:A,A:] holds

((ScProductDM L) || A) . x in the carrier of F_Real

proof

then reconsider sc = (ScProductDM L) || A as Function of [:A,A:], the carrier of F_Real by A5, FUNCT_2:3;
let x be object ; :: thesis: ( x in [:A,A:] implies ((ScProductDM L) || A) . x in the carrier of F_Real )

assume B1: x in [:A,A:] ; :: thesis: ((ScProductDM L) || A) . x in the carrier of F_Real

then consider x1, x2 being 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;

((ScProductDM L) || A) . (x1,x2) = (ScProductDM L) . (v1,v2) by B1, B2, FUNCT_1:49;

hence ((ScProductDM L) || A) . x in the carrier of F_Real by B2; :: thesis: verum

end;assume B1: x in [:A,A:] ; :: thesis: ((ScProductDM L) || A) . x in the carrier of F_Real

then consider x1, x2 being 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;

((ScProductDM L) || A) . (x1,x2) = (ScProductDM L) . (v1,v2) by B1, B2, FUNCT_1:49;

hence ((ScProductDM L) || A) . x in the carrier of F_Real by B2; :: thesis: verum

reconsider ze = 0. (DivisibleMod L) as Element of A by ZMODUL01:18;

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

reconsider L1 = LatticeStr(# A,ad,ze,mu,sc #) as non empty LatticeStr over INT.Ring ;

A7: L1 is Submodule of DivisibleMod L by ZMODLAT2:10;

reconsider L1 = L1 as non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed LatticeStr over INT.Ring by ZMODLAT2:10;

set I = the Basis of (EMLat L);

for v being Vector of (DivisibleMod L) st v in L1 holds

v in Lin (DualBasis the Basis of (EMLat L))

proof

then
L1 is Submodule of Lin (DualBasis the Basis of (EMLat L))
by A7, ZMODUL01:44;
let v be Vector of (DivisibleMod L); :: thesis: ( v in L1 implies v in Lin (DualBasis the Basis of (EMLat L)) )

assume B1: v in L1 ; :: thesis: v in Lin (DualBasis the Basis of (EMLat L))

consider x being Dual of L such that

B2: x = v by B1;

thus v in Lin (DualBasis the Basis of (EMLat L)) by B2, ThDE3; :: thesis: verum

end;assume B1: v in L1 ; :: thesis: v in Lin (DualBasis the Basis of (EMLat L))

consider x being Dual of L such that

B2: x = v by B1;

thus v in Lin (DualBasis the Basis of (EMLat L)) by B2, ThDE3; :: thesis: verum

then reconsider L1 = L1 as strict Z_Lattice by A7, ZMODLAT2:27;

take L1 ; :: thesis: ( the carrier of L1 = DualSet L & 0. L1 = 0. (DivisibleMod L) & the addF of L1 = the addF of (DivisibleMod L) || the carrier of L1 & the lmult of L1 = the lmult of (DivisibleMod L) | [: the carrier of INT.Ring, the carrier of L1:] & the scalar of L1 = (ScProductDM L) || the carrier of L1 )

thus ( the carrier of L1 = DualSet L & 0. L1 = 0. (DivisibleMod L) & the addF of L1 = the addF of (DivisibleMod L) || the carrier of L1 & the lmult of L1 = the lmult of (DivisibleMod L) | [: the carrier of INT.Ring, the carrier of L1:] & the scalar of L1 = (ScProductDM L) || the carrier of L1 ) ; :: thesis: verum