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

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

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

then reconsider Z = Z as strict Z_Lattice by AZ;
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_{1}, b_{2} being Element of the carrier of Z holds <;b_{1},b_{2};> = <;b_{2},b_{1};> ) & ( for b_{1}, b_{2}, b_{3} being Element of the carrier of Z

for b_{4} being Element of the carrier of INT.Ring holds

( <;(b_{1} + b_{2}),b_{3};> = <;b_{1},b_{3};> + <;b_{2},b_{3};> & <;(b_{4} * b_{1}),b_{2};> = b_{4} * <;b_{1},b_{2};> ) ) )_{1}, b_{2}, b_{3} being Element of the carrier of Z

for b_{4} being Element of the carrier of INT.Ring holds

( <;(b_{1} + b_{2}),b_{3};> = <;b_{1},b_{3};> + <;b_{2},b_{3};> & <;(b_{4} * b_{1}),b_{2};> = b_{4} * <;b_{1},b_{2};> )

for a being Element of INT.Ring holds

( <;(x + y),z;> = <;x,z;> + <;y,z;> & <;(a * x),y;> = a * <;x,y;> ) :: thesis: verum

end;x = 0. Z :: according to ZMODLAT1:def 3 :: thesis: ( ( for b

for b

( <;(b

proof

thus
for x, y being Vector of Z holds <;x,y;> = <;y,x;>
:: thesis: for b
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

end;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 )
;

end;

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;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

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

.= 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;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

then B6: xz =
0. (EMbedding L)
by ThSPEM1
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;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

.= 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

for b

( <;(b

proof

thus
for x, y, z being Vector of Z
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;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

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;( <;(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

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