set Z = EMLat L;

for v being Vector of (EMLat L) st v <> 0. (EMLat L) holds

||.v.|| > 0

for v being Vector of (EMLat L) st v <> 0. (EMLat L) holds

||.v.|| > 0

proof

hence
EMLat L is positive-definite
; :: thesis: verum
let v be Vector of (EMLat L); :: thesis: ( v <> 0. (EMLat L) implies ||.v.|| > 0 )

assume AS: v <> 0. (EMLat L) ; :: thesis: ||.v.|| > 0

v in the carrier of (EMLat L) ;

then v in rng (MorphsZQ L) by defEMLat;

then B1: v is Vector of (EMbedding L) by ZMODUL08:def 3;

then consider vv being Vector of L such that

B2: (MorphsZQ L) . vv = v by ZMODUL08:22;

B3: vv <> 0. L

.= ||.vv.|| by B1, B2, defScProductEM ;

hence ||.v.|| > 0 by B3, ZMODLAT1:def 6; :: thesis: verum

end;assume AS: v <> 0. (EMLat L) ; :: thesis: ||.v.|| > 0

v in the carrier of (EMLat L) ;

then v in rng (MorphsZQ L) by defEMLat;

then B1: v is Vector of (EMbedding L) by ZMODUL08:def 3;

then consider vv being Vector of L such that

B2: (MorphsZQ L) . vv = v by ZMODUL08:22;

B3: vv <> 0. L

proof

||.v.|| =
(ScProductEM L) . (v,v)
by defEMLat
assume
vv = 0. L
; :: thesis: contradiction

then v = 0. (Z_MQ_VectSp L) by B2, ZMODUL04:def 6

.= 0. (EMbedding L) by ZMODUL08:19

.= zeroCoset L by ZMODUL08:def 3

.= 0. (EMLat L) by defEMLat ;

hence contradiction by AS; :: thesis: verum

end;then v = 0. (Z_MQ_VectSp L) by B2, ZMODUL04:def 6

.= 0. (EMbedding L) by ZMODUL08:19

.= zeroCoset L by ZMODUL08:def 3

.= 0. (EMLat L) by defEMLat ;

hence contradiction by AS; :: thesis: verum

.= ||.vv.|| by B1, B2, defScProductEM ;

hence ||.v.|| > 0 by B3, ZMODLAT1:def 6; :: thesis: verum