EMbedding (r,L) is Submodule of DivisibleMod L by ZMODUL08:32;
then the carrier of (EMbedding (r,L)) c= the carrier of (DivisibleMod L) by VECTSP_4:def 2;
then [: the carrier of (EMbedding (r,L)), the carrier of (EMbedding (r,L)):] c= [: the carrier of (DivisibleMod L), the carrier of (DivisibleMod L):] by ZFMISC_1:96;
then reconsider sc = (ScProductDM L) || the carrier of (EMbedding (r,L)) as Function of [: the carrier of (EMbedding (r,L)), the carrier of (EMbedding (r,L)):], the carrier of F_Real by FUNCT_2:32;
set Z = LatticeStr(# the carrier of (EMbedding (r,L)), the addF of (EMbedding (r,L)),(0. (EMbedding (r,L))), the lmult of (EMbedding (r,L)),sc #);
AZ: LatticeStr(# the carrier of (EMbedding (r,L)), the addF of (EMbedding (r,L)),(0. (EMbedding (r,L))), the lmult of (EMbedding (r,L)),sc #) = GenLat ((EMbedding (r,L)),sc) ;
A0: LatticeStr(# the carrier of (EMbedding (r,L)), the addF of (EMbedding (r,L)),(0. (EMbedding (r,L))), the lmult of (EMbedding (r,L)),sc #) is Submodule of EMbedding (r,L) by AZ, ZMODLAT1:2;
reconsider Z = LatticeStr(# the carrier of (EMbedding (r,L)), the addF of (EMbedding (r,L)),(0. (EMbedding (r,L))), the lmult of (EMbedding (r,L)),sc #) as non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed LatticeStr over INT.Ring by AZ;
AX: EMbedding (r,L) is Submodule of DivisibleMod L by ZMODUL08:32;
then AX2: Z is Submodule of DivisibleMod L by A0, ZMODUL01:42;
reconsider Z = Z as non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed free LatticeStr over INT.Ring by AZ;
Z is Z_Lattice-like

proof

thus for x being Vector of Z st ( for y being Vector of Z holds <;x,y;> = 0 ) holds
x = 0. Z :: according to ZMODLAT1:def 3 :: thesis: ( ( for b₁, b₂ being Element of the carrier of Z holds <;b₁,b₂;> = <;b₂,b₁;> ) & ( for b₁, b₂, b₃ being Element of the carrier of Z
for b₄ being Element of the carrier of INT.Ring holds
( <;(b₁ + b₂),b₃;> = <;b₁,b₃;> + <;b₂,b₃;> & <;(b₄ * b₁),b₂;> = b₄ * <;b₁,b₂;> ) ) )

proof

let x be Vector of Z; :: thesis: ( ( for y being Vector of Z holds <;x,y;> = 0 ) implies x = 0. Z )
assume B1: for y being Vector of Z holds <;x,y;> = 0 ; :: thesis: x = 0. Z

per cases ( r is zero or not r is zero ) ;

suppose C1: r is zero ; :: thesis: x = 0. Z

x in the carrier of (EMbedding (r,L)) ;
then x in r * (rng (MorphsZQ L)) by ZMODUL08:def 6;
then consider y being Vector of (Z_MQ_VectSp L) such that
C2: ( x = (0. F_Rat) * y & y in rng (MorphsZQ L) ) by C1;
thus x = 0. (Z_MQ_VectSp L) by C2, VECTSP_1:14
.= 0. Z by ZMODUL08:25 ; :: thesis: verum

end;

suppose AS: not r is zero ; :: thesis: x = 0. Z

then consider T being linear-transformation of (EMbedding L),(EMbedding (r,L)) such that
B2: ( ( for v being Element of (Z_MQ_VectSp L) st v in EMbedding L holds
T . v = r * v ) & T is bijective ) by ZMODUL08:27;
consider rm0, rn0 being Integer such that
BX: ( rn0 > 0 & r = rm0 / rn0 ) by RAT_1:1;
reconsider rn = rn0, rm = rm0 as Element of INT.Ring by INT_1:def 2;
INT c= the carrier of F_Real by NUMBERS:5;
then reconsider rnf = rn, rmf = rm as Element of F_Real ;
x in the carrier of (EMbedding (r,L)) ;
then x in rng T by B2, FUNCT_2:def 3;
then consider xe being object such that
B3: ( xe in the carrier of (EMbedding L) & x = T . xe ) by FUNCT_2:11;
reconsider xz = xe as Vector of (Z_MQ_VectSp L) by B3, ZMODUL08:19;
reconsider xd = xz as Vector of (DivisibleMod L) by ZMODUL08:30;
consider zxd being Vector of (DivisibleMod L) such that
BY: ( xd = rn * zxd & r * xz = rm * zxd ) by AS, BX, ZMODUL08:31;
reconsider xe = xe as Vector of (EMbedding L) by B3;
for ye being Vector of (EMbedding L) holds (ScProductEM L) . (xe,ye) = 0

proof

let ye be Vector of (EMbedding L); :: thesis: (ScProductEM L) . (xe,ye) = 0
reconsider yz = ye as Vector of (Z_MQ_VectSp L) by ZMODUL08:19;
reconsider yd = yz as Vector of (DivisibleMod L) by ZMODUL08:30;
consider zyd being Vector of (DivisibleMod L) such that
C1: ( yd = rn * zyd & r * yz = rm * zyd ) by AS, BX, ZMODUL08:31;
reconsider y = T . ye as Vector of (EMbedding (r,L)) ;
reconsider y = y as Vector of Z ;
reconsider xd1 = xd as Vector of (EMbedding L) by B3;
reconsider yd1 = yd as Vector of (EMbedding L) ;
C7: xz in EMbedding L by B3;
C8: yz in EMbedding L ;
C5: x = rm * zxd by B2, B3, BY, C7;
C6: y = rm * zyd by B2, C1, C8;
CX: <;x,y;> = sc . (x,y)
.= (ScProductDM L) . ((rm * zxd),y) by C5, ThSPrEM1
.= rm * ((ScProductDM L) . (zxd,(rm * zyd))) by C6, ThSPDM1
.= rm * ((ScProductDM L) . ((rm * zyd),zxd)) by ThSPDM1
.= rm * (rm * ((ScProductDM L) . (zyd,zxd))) by ThSPDM1
.= rm * (rm * ((ScProductDM L) . (zxd,zyd))) by ThSPDM1
.= (rmf * rmf) * ((ScProductDM L) . (zxd,zyd))
.= (rmf * rmf) * (((rnf ") * (rnf ")) * ((ScProductEM L) . (xd1,yd1))) by BX, BY, C1, defScProductDM
.= (((rmf * rmf) * (rnf ")) * (rnf ")) * ((ScProductEM L) . (xd,yd)) ;
rnf <> 0. F_Real by BX;
then ( rmf <> 0 & rnf " <> 0 ) by AS, BX, VECTSP_1:25;
hence (ScProductEM L) . (xe,ye) = 0 by B1, CX; :: thesis: verum

end;

then B6: xz = 0. (EMbedding L) by ThSPEM1
.= 0. (Z_MQ_VectSp L) by ZMODUL08:19 ;
xe in EMbedding L ;
then T . xe = r * xz by B2
.= 0. (Z_MQ_VectSp L) by B6, VECTSP_1:15
.= 0. Z by ZMODUL08:25 ;
hence x = 0. Z by B3; :: thesis: verum

end;

end;

end;

thus for x, y being Vector of Z holds <;x,y;> = <;y,x;> :: thesis: for b₁, b₂, b₃ being Element of the carrier of Z
for b₄ being Element of the carrier of INT.Ring holds
( <;(b₁ + b₂),b₃;> = <;b₁,b₃;> + <;b₂,b₃;> & <;(b₄ * b₁),b₂;> = b₄ * <;b₁,b₂;> )

proof

let x, y be Vector of Z; :: thesis: <;x,y;> = <;y,x;>
reconsider xx = x, yy = y as Vector of (DivisibleMod L) by AX, ZMODUL01:25;
thus <;x,y;> = the scalar of Z . (x,y)
.= (ScProductDM L) . (xx,yy) by ThSPrEM1
.= (ScProductDM L) . (yy,xx) by ThSPDM1
.= the scalar of Z . (y,x) by ThSPrEM1
.= <;y,x;> ; :: thesis: verum

end;

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

proof

let x, y, z be Vector of Z; :: thesis: for a being Element of INT.Ring holds
( <;(x + y),z;> = <;x,z;> + <;y,z;> & <;(a * x),y;> = a * <;x,y;> )
let a be Element of INT.Ring; :: thesis: ( <;(x + y),z;> = <;x,z;> + <;y,z;> & <;(a * x),y;> = a * <;x,y;> )
reconsider xx = x, yy = y, zz = z as Vector of (DivisibleMod L) by AX, ZMODUL01:25;
thus <;(x + y),z;> = the scalar of Z . ((x + y),z)
.= (ScProductDM L) . ((x + y),z) by ThSPrEM1
.= (ScProductDM L) . ((xx + yy),zz) by AX2, ZMODUL01:28
.= ((ScProductDM L) . (xx,zz)) + ((ScProductDM L) . (yy,zz)) by ThSPDM1
.= ( the scalar of Z . (x,z)) + ((ScProductDM L) . (yy,zz)) by ThSPrEM1
.= ( the scalar of Z . (x,z)) + ( the scalar of Z . (y,z)) by ThSPrEM1
.= <;x,z;> + <;y,z;> ; :: thesis: <;(a * x),y;> = a * <;x,y;>
thus <;(a * x),y;> = the scalar of Z . ((a * x),y)
.= (ScProductDM L) . ((a * x),y) by ThSPrEM1
.= (ScProductDM L) . ((a * xx),y) by AX2, ZMODUL01:29
.= a * ((ScProductDM L) . (xx,yy)) by ThSPDM1
.= a * ( the scalar of Z . (x,y)) by ThSPrEM1
.= a * <;x,y;> ; :: thesis: verum

end;

end;

then reconsider Z = Z as strict Z_Lattice by AZ;
take Z ; :: thesis: ( the carrier of Z = r * (rng (MorphsZQ L)) & the ZeroF of Z = zeroCoset L & the addF of Z = (addCoset L) || (r * (rng (MorphsZQ L))) & the lmult of Z = (lmultCoset L) | [: the carrier of INT.Ring,(r * (rng (MorphsZQ L))):] & the scalar of Z = (ScProductDM L) || (r * (rng (MorphsZQ L))) )
thus ( the carrier of Z = r * (rng (MorphsZQ L)) & the ZeroF of Z = zeroCoset L & the addF of Z = (addCoset L) || (r * (rng (MorphsZQ L))) & the lmult of Z = (lmultCoset L) | [: the carrier of INT.Ring,(r * (rng (MorphsZQ L))):] & the scalar of Z = (ScProductDM L) || (r * (rng (MorphsZQ L))) ) by ZMODUL08:def 6; :: thesis: verum