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
ZMODLAT1:def 3 ( ( for b1, b2 being Element of the carrier of Z holds <;b1,b2;> = <;b2,b1;> ) & ( for b1, b2, b3 being Element of the carrier of Z
for b4 being Element of the carrier of INT.Ring holds
( <;(b1 + b2),b3;> = <;b1,b3;> + <;b2,b3;> & <;(b4 * b1),b2;> = b4 * <;b1,b2;> ) ) )proof
let x be
Vector of
Z;
( ( 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
;
x = 0. Z
per cases
( r is zero or not r is zero )
;
suppose AS:
not
r is
zero
;
x = 0. Zthen 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);
(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;
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;
verum end;
end;
thus
for
x,
y being
Vector of
Z holds
<;x,y;> = <;y,x;>
for b1, b2, b3 being Element of the carrier of Z
for b4 being Element of the carrier of INT.Ring holds
( <;(b1 + b2),b3;> = <;b1,b3;> + <;b2,b3;> & <;(b4 * b1),b2;> = b4 * <;b1,b2;> )proof
let x,
y be
Vector of
Z;
<;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;>
;
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;> )
verumproof
let x,
y,
z be
Vector of
Z;
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;
( <;(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;>
;
<;(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;>
;
verum
end;
end;
then reconsider Z = Z as strict Z_Lattice by AZ;
take
Z
; ( 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; verum