let L be positive-definite Z_Lattice; :: thesis: 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; :: thesis: ( 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 ) ; :: thesis: LX is positive-definite
for v being Vector of LX st v <> 0. LX holds
||.v.|| > 0

proof

let v be Vector of LX; :: thesis: ( v <> 0. LX implies ||.v.|| > 0 )
assume B1: v <> 0. LX ; :: thesis: ||.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; :: thesis: verum

end;

hence LX is positive-definite ; :: thesis: verum