let L be positive-definite Z_Lattice; for Z being non empty LatticeStr over INT.Ring st Z is Submodule of DivisibleMod L & the scalar of Z = (ScProductDM L) || the carrier of Z holds
Z is Z_Lattice-like
let Z be non empty LatticeStr over INT.Ring ; ( Z is Submodule of DivisibleMod L & the scalar of Z = (ScProductDM L) || the carrier of Z implies Z is Z_Lattice-like )
assume A1:
( Z is Submodule of DivisibleMod L & the scalar of Z = (ScProductDM L) || the carrier of Z )
; Z is Z_Lattice-like
set A = the carrier of Z;
A2:
for x, y being Vector of Z holds the scalar of Z . (x,y) = (ScProductDM L) . (x,y)
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;> )proof
let x,
y be
Vector of
Z;
<;x,y;> = <;y,x;>
reconsider xx =
x,
yy =
y as
Vector of
(DivisibleMod L) by A1, ZMODUL01:25;
thus <;x,y;> =
the
scalar of
Z . (
x,
y)
.=
(ScProductDM L) . (
x,
y)
by A2
.=
(ScProductDM L) . (
yy,
xx)
by ThSPDM1
.=
the
scalar of
Z . (
y,
x)
by A2
.=
<;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 A1, ZMODUL01:25;
B1:
xx + yy = x + y
by A1, ZMODUL01:28;
thus <;(x + y),z;> =
the
scalar of
Z . (
(x + y),
z)
.=
(ScProductDM L) . (
(xx + yy),
zz)
by A2, B1
.=
((ScProductDM L) . (xx,zz)) + ((ScProductDM L) . (yy,zz))
by ThSPDM1
.=
( the scalar of Z . (x,z)) + ((ScProductDM L) . (y,z))
by A2
.=
( the scalar of Z . (x,z)) + ( the scalar of Z . (y,z))
by A2
.=
<;x,z;> + <;y,z;>
;
<;(a * x),y;> = a * <;x,y;>
B2:
a * xx = a * x
by A1, ZMODUL01:29;
thus <;(a * x),y;> =
the
scalar of
Z . (
(a * x),
y)
.=
(ScProductDM L) . (
(a * xx),
yy)
by A2, B2
.=
a * ((ScProductDM L) . (xx,yy))
by ThSPDM1
.=
a * ( the scalar of Z . (x,y))
by A2
.=
a * <;x,y;>
;
verum
end;
end;
hence
Z is Z_Lattice-like
; verum