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

take Z ; :: thesis: ( 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; :: thesis: verum

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

then reconsider Z = Z as strict Z_Lattice by AX;
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

for y being Vector of Z holds (ScProductEM L) . (x,y) = 0

end;assume B1: for y being Vector of Z holds <;x,y;> = 0 ; :: thesis: x = 0. Z

for y being Vector of Z holds (ScProductEM L) . (x,y) = 0

proof

hence
x = 0. Z
by ThSPEM1; :: thesis: verum
let y be Vector of Z; :: thesis: (ScProductEM L) . (x,y) = 0

thus (ScProductEM L) . (x,y) = <;x,y;>

.= 0 by B1 ; :: thesis: verum

end;thus (ScProductEM L) . (x,y) = <;x,y;>

.= 0 by B1 ; :: 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;>

thus <;x,y;> = (ScProductEM L) . (x,y)

.= (ScProductEM L) . (y,x) by ThSPEM1

.= <;y,x;> ; :: thesis: verum

end;thus <;x,y;> = (ScProductEM L) . (x,y)

.= (ScProductEM L) . (y,x) by ThSPEM1

.= <;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 (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;> ; :: thesis: <;(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;> ; :: 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 (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;> ; :: thesis: <;(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;> ; :: thesis: verum

take Z ; :: thesis: ( 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; :: thesis: verum