let V be non trivial torsion-free Z_Module; 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; 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; 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; ( 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
; 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
ZMODLAT1:def 3 ( ( 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;> ) ) )
thus
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,
y be
Vector of
L;
<;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;>
;
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;> )
verumproof
let x,
y,
z be
Vector of
L;
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;> )
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;>
;
<;(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;>
;
verum
end;
end;
hence
GenLat (Z,f) is Z_Lattice-like
; verum