set Z = LatticeStr(# the carrier of (EMbedding L), the addF of (EMbedding L),(0. (EMbedding L)), the lmult of (EMbedding L),(ScProductEM L) #);
AX:
LatticeStr(# the carrier of (EMbedding L), the addF of (EMbedding L),(0. (EMbedding L)), the lmult of (EMbedding L),(ScProductEM L) #) = GenLat ((EMbedding L),(ScProductEM L))
;
then reconsider Z = LatticeStr(# the carrier of (EMbedding L), the addF of (EMbedding L),(0. (EMbedding L)), the lmult of (EMbedding L),(ScProductEM L) #) as non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed LatticeStr over INT.Ring ;
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 AX;
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;> ) ) )
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;> )
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
(EMbedding L) ;
thus <;(x + y),z;> =
(ScProductEM L) . (
(xx + yy),
zz)
.=
( the scalar of Z . (x,z)) + ( the scalar of Z . (y,z))
by ThSPEM1
.=
<;x,z;> + <;y,z;>
;
<;(a * x),y;> = a * <;x,y;>
thus <;(a * x),y;> =
(ScProductEM L) . (
(a * xx),
y)
.=
a * ((ScProductEM L) . (xx,y))
by ThSPEM1
.=
a * <;x,y;>
;
verum
end;
end;
then reconsider Z = Z as strict Z_Lattice by AX;
take
Z
; ( the carrier of Z = rng (MorphsZQ L) & the ZeroF of Z = zeroCoset L & the addF of Z = (addCoset L) || (rng (MorphsZQ L)) & the lmult of Z = (lmultCoset L) | [: the carrier of INT.Ring,(rng (MorphsZQ L)):] & the scalar of Z = ScProductEM L )
thus
( the carrier of Z = rng (MorphsZQ L) & the ZeroF of Z = zeroCoset L & the addF of Z = (addCoset L) || (rng (MorphsZQ L)) & the lmult of Z = (lmultCoset L) | [: the carrier of INT.Ring,(rng (MorphsZQ L)):] & the scalar of Z = ScProductEM L )
by ZMODUL08:def 3; verum