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

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

hence
LX is positive-definite
; :: thesis: verum
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;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