set Z = EMLat L;
for v being Vector of (EMLat L) st v <> 0. (EMLat L) holds
||.v.|| > 0
proof
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
proof
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;
||.v.|| = (ScProductEM L) . (v,v) by defEMLat
.= ||.vv.|| by B1, B2, defScProductEM ;
hence ||.v.|| > 0 by B3, ZMODLAT1:def 6; :: thesis: verum
end;
hence EMLat L is positive-definite ; :: thesis: verum