let V be non trivial torsion-free Z_Module; :: thesis: for Z being Submodule of V
for v being non zero Vector of V
for f being Function of [: the carrier of Z, the carrier of Z:], the carrier of F_Real st Z = Lin {v} & ( for v1, v2 being Vector of Z
for a, b being Element of INT.Ring st v1 = a * v & v2 = b * v holds
f . (v1,v2) = a * b ) holds
GenLat (Z,f) is Z_Lattice-like
let Z be Submodule of V; :: thesis: for v being non zero Vector of V
for f being Function of [: the carrier of Z, the carrier of Z:], the carrier of F_Real st Z = Lin {v} & ( for v1, v2 being Vector of Z
for a, b being Element of INT.Ring st v1 = a * v & v2 = b * v holds
f . (v1,v2) = a * b ) holds
GenLat (Z,f) is Z_Lattice-like
let v be non zero Vector of V; :: thesis: for f being Function of [: the carrier of Z, the carrier of Z:], the carrier of F_Real st Z = Lin {v} & ( for v1, v2 being Vector of Z
for a, b being Element of INT.Ring st v1 = a * v & v2 = b * v holds
f . (v1,v2) = a * b ) holds
GenLat (Z,f) is Z_Lattice-like
let f be Function of [: the carrier of Z, the carrier of Z:], the carrier of F_Real; :: thesis: ( Z = Lin {v} & ( for v1, v2 being Vector of Z
for a, b being Element of INT.Ring st v1 = a * v & v2 = b * v holds
f . (v1,v2) = a * b ) implies GenLat (Z,f) is Z_Lattice-like )
assume that
A1: Z = Lin {v} and
A2: for v1, v2 being Vector of Z
for a, b being Element of INT.Ring st v1 = a * v & v2 = b * v holds
f . (v1,v2) = a * b ; :: thesis: GenLat (Z,f) is Z_Lattice-like
set L = GenLat (Z,f);
reconsider L = GenLat (Z,f) as non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed free finite-rank LatticeStr over INT.Ring by A1;
L is Z_Lattice-like

proof

thus for x being Vector of L st ( for y being Vector of L holds <;x,y;> = 0 ) holds
x = 0. L :: according to ZMODLAT1:def 3 :: thesis: ( ( for x, y being Vector of L holds <;x,y;> = <;y,x;> ) & ( for x, y, z being Vector of L
for a being Element of INT.Ring holds
( <;(x + y),z;> = <;x,z;> + <;y,z;> & <;(a * x),y;> = a * <;x,y;> ) ) )

proof

let x be Vector of L; :: thesis: ( ( for y being Vector of L holds <;x,y;> = 0 ) implies x = 0. L )
assume C1: for y being Vector of L holds <;x,y;> = 0 ; :: thesis: x = 0. L
assume x <> 0. L ; :: thesis: contradiction
then C2: x <> 0. V by ZMODUL01:26;
x in Lin {v} by A1;
then consider ix being Element of INT.Ring such that
C3: x = ix * v by ZMODUL06:19;
reconsider xx = x as Vector of Z ;
C4: ix <> 0 by C2, C3, ZMODUL01:1;
<;x,x;> = f . (x,x)
.= ix * ix by A2, C3 ;
hence contradiction by C1, C4; :: thesis: verum

end;

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

proof

let x, y be Vector of L; :: thesis: <;x,y;> = <;y,x;>
C1: ( x in Lin {v} & y in Lin {v} ) by A1;
then consider ix being Element of INT.Ring such that
C2: x = ix * v by ZMODUL06:19;
consider iy being Element of INT.Ring such that
C3: y = iy * v by C1, ZMODUL06:19;
thus <;x,y;> = f . (x,y)
.= ix * iy by A2, C2, C3
.= f . (y,x) by A2, C2, C3
.= <;y,x;> ; :: thesis: verum

end;

thus for x, y, z being Vector of L
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 L; :: 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;> )
C1: ( x in Lin {v} & y in Lin {v} & z in Lin {v} ) by A1;
then consider ix being Element of INT.Ring such that
C2: x = ix * v by ZMODUL06:19;
consider iy being Element of INT.Ring such that
C3: y = iy * v by C1, ZMODUL06:19;
consider iz being Element of INT.Ring such that
C4: z = iz * v by C1, ZMODUL06:19;
ix * v in Lin {v} by ZMODUL06:21;
then reconsider iixv = ix * v as Vector of Z by A1;
reconsider ixv = ix * v as Vector of V ;
iy * v in Lin {v} by ZMODUL06:21;
then reconsider iiyv = iy * v as Vector of Z by A1;
reconsider iyv = iy * v as Vector of V ;
C5: x + y = iixv + iiyv by C2, C3
.= ixv + iyv by ZMODUL01:28
.= (ix + iy) * v by VECTSP_1:def 15 ;
C6: a * x = a * iixv by C2
.= a * ixv by ZMODUL01:29
.= (a * ix) * v by VECTSP_1:def 16 ;
thus <;(x + y),z;> = f . ((x + y),z)
.= (ix + iy) * iz by A2, C4, C5
.= (ix * iz) + (iy * iz)
.= (f . (x,z)) + (iy * iz) by A2, C2, C4
.= (f . [x,z]) + (f . (y,z)) by A2, C3, C4
.= <;x,z;> + <;y,z;> ; :: thesis: <;(a * x),y;> = a * <;x,y;>
thus <;(a * x),y;> = f . ((a * x),y)
.= (a * ix) * iy by A2, C3, C6
.= a * (ix * iy)
.= a * (f . (x,y)) by A2, C2, C3
.= a * <;x,y;> ; :: thesis: verum

end;

end;

hence GenLat (Z,f) is Z_Lattice-like ; :: thesis: verum