let L be positive-definite Z_Lattice; for LX being Z_Lattice st LX is Submodule of DivisibleMod L & the scalar of LX = (ScProductDM L) || the carrier of LX holds
LX is positive-definite
let LX be Z_Lattice; ( LX is Submodule of DivisibleMod L & the scalar of LX = (ScProductDM L) || the carrier of LX implies LX is positive-definite )
assume A1:
( LX is Submodule of DivisibleMod L & the scalar of LX = (ScProductDM L) || the carrier of LX )
; LX is positive-definite
for v being Vector of LX st v <> 0. LX holds
||.v.|| > 0
proof
let v be
Vector of
LX;
( v <> 0. LX implies ||.v.|| > 0 )
assume B1:
v <> 0. LX
;
||.v.|| > 0
reconsider vv =
v as
Vector of
(DivisibleMod L) by A1, ZMODUL01:25;
B3:
||.v.|| = (ScProductDM L) . (
vv,
vv)
by A1, FUNCT_1:49;
consider i being
Element of
INT.Ring such that B4:
(
i <> 0 &
i * vv in EMbedding L )
by ZMODUL08:29;
i * vv in rng (MorphsZQ L)
by B4, ZMODUL08:def 3;
then reconsider iv =
i * vv as
Vector of
(EMLat L) by ZMODLAT2:def 4;
B5:
(i * i) * ||.v.|| =
i * (i * ((ScProductDM L) . (vv,vv)))
by B3
.=
i * ((ScProductDM L) . (vv,(i * vv)))
by ZMODLAT2:13
.=
(ScProductDM L) . (
(i * vv),
(i * vv))
by ZMODLAT2:6
.=
(ScProductEM L) . (
iv,
iv)
by B4, ZMODLAT2:8
.=
||.iv.||
by ZMODLAT2:def 4
;
i <> 0. INT.Ring
by B4;
then
i * v <> 0. LX
by B1, ZMODUL01:def 7;
then
i * vv <> 0. LX
by A1, ZMODUL01:29;
then
iv <> 0. (DivisibleMod L)
by A1, VECTSP_4:def 2;
then
iv <> zeroCoset L
by ZMODUL08:def 4;
then
iv <> 0. (EMLat L)
by ZMODLAT2:def 4;
then
||.iv.|| > 0
by ZMODLAT1:def 6;
hence
||.v.|| > 0
by B5, XREAL_1:63, XREAL_1:131;
verum
end;
hence
LX is positive-definite
; verum