let L be positive-definite Z_Lattice; :: thesis: for LX being Z_Lattice st LX is Submodule of DivisibleMod L & the scalar of LX = () || 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 = () || the carrier of LX implies LX is positive-definite )
assume A1: ( LX is Submodule of DivisibleMod L & the scalar of LX = () || the carrier of LX ) ; :: thesis:
for v being Vector of LX st v <> 0. LX holds
> 0
proof
let v be Vector of LX; :: thesis: ( v <> 0. LX implies > 0 )
assume B1: v <> 0. LX ; :: thesis:
reconsider vv = v as Vector of () by ;
B3: ||.v.|| = () . (vv,vv) by ;
consider i being Element of INT.Ring such that
B4: ( i <> 0 & i * vv in EMbedding L ) by ZMODUL08:29;
i * vv in rng () by ;
then reconsider iv = i * vv as Vector of () by ZMODLAT2:def 4;
B5: (i * i) * = i * (i * (() . (vv,vv))) by B3
.= i * (() . (vv,(i * vv))) by ZMODLAT2:13
.= () . ((i * vv),(i * vv)) by ZMODLAT2:6
.= () . (iv,iv) by
.= ||.iv.|| by ZMODLAT2:def 4 ;
i <> 0. INT.Ring by B4;
then i * v <> 0. LX by ;
then i * vv <> 0. LX by ;
then iv <> 0. () by ;
then iv <> zeroCoset L by ZMODUL08:def 4;
then iv <> 0. () by ZMODLAT2:def 4;
then ||.iv.|| > 0 by ZMODLAT1:def 6;
hence ||.v.|| > 0 by ; :: thesis: verum
end;
hence LX is positive-definite ; :: thesis: verum