set Z = EMLat (r,L);

consider rm0, rn0 being Integer such that

A1: ( rn0 <> 0 & r = rm0 / rn0 ) by RAT_1:1;

a1: rn0 <> 0. INT.Ring by A1;

reconsider rn = rn0, rm = rm0 as Element of INT.Ring by INT_1:def 2;

INT c= the carrier of F_Real by NUMBERS:5;

then reconsider rnf = rn, rmf = rm as Element of F_Real ;

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

||.v.|| > 0

consider rm0, rn0 being Integer such that

A1: ( rn0 <> 0 & r = rm0 / rn0 ) by RAT_1:1;

a1: rn0 <> 0. INT.Ring by A1;

reconsider rn = rn0, rm = rm0 as Element of INT.Ring by INT_1:def 2;

INT c= the carrier of F_Real by NUMBERS:5;

then reconsider rnf = rn, rmf = rm as Element of F_Real ;

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

||.v.|| > 0

proof

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

assume B1: v <> 0. (EMLat (r,L)) ; :: thesis: ||.v.|| > 0

consider T being linear-transformation of (EMbedding L),(EMbedding (r,L)) such that

B2: ( ( for v being Vector of (Z_MQ_VectSp L) st v in EMbedding L holds

T . v = r * v ) & T is bijective ) by ZMODUL08:27;

v in the carrier of (EMLat (r,L)) ;

then B0: v in r * (rng (MorphsZQ L)) by defrEMLat;

then v in the carrier of (EMbedding (r,L)) by ZMODUL08:def 6;

then v in rng T by B2, FUNCT_2:def 3;

then consider ve being object such that

B3: ( ve in the carrier of (EMbedding L) & v = T . ve ) by FUNCT_2:11;

reconsider vz = ve as Vector of (Z_MQ_VectSp L) by B3, ZMODUL08:19;

reconsider vd = vz as Vector of (DivisibleMod L) by ZMODUL08:30;

consider zvd being Vector of (DivisibleMod L) such that

B4: ( vd = rn * zvd & r * vz = rm * zvd ) by A1, ZMODUL08:31;

BX: vz in EMbedding L by B3;

B5: v = rm * zvd by B2, B3, B4, BX;

B6: v is Vector of (EMbedding (r,L)) by B0, ZMODUL08:def 6;

reconsider vd = vd as Vector of (EMbedding L) by B3;

B8: ||.v.|| = ((ScProductDM L) || (r * (rng (MorphsZQ L)))) . (v,v) by defrEMLat

.= ((ScProductDM L) || the carrier of (EMbedding (r,L))) . (v,v) by ZMODUL08:def 6

.= (ScProductDM L) . (v,v) by B6, ThSPrEM1

.= rm0 * ((ScProductDM L) . (zvd,(rm * zvd))) by B5, ThSPDM1

.= rm0 * ((ScProductDM L) . ((rm * zvd),zvd)) by ThSPDM1

.= rm0 * (rm0 * ((ScProductDM L) . (zvd,zvd))) by ThSPDM1

.= (rm0 * rm0) * ((ScProductDM L) . (zvd,zvd))

.= (rmf * rmf) * (((rnf ") * (rnf ")) * ((ScProductEM L) . (vd,vd))) by A1, B4, defScProductDM

.= ((rmf * rmf) * ((rnf ") * (rnf "))) * ((ScProductEM L) . (vd,vd)) ;

BY: rnf <> 0. F_Real by A1;

rm0 <> 0

then B9: ( rmf * rmf > 0 & (rnf ") * (rnf ") > 0 ) by XREAL_1:63;

vd in the carrier of (EMbedding L) ;

then vd in rng (MorphsZQ L) by ZMODUL08:def 3;

then reconsider vl = vd as Vector of (EMLat L) by defEMLat;

vd <> 0. (EMbedding L)

then B10: vd <> 0. (EMLat L) by defEMLat;

(ScProductEM L) . (vd,vd) = ||.vl.|| by defEMLat;

then (ScProductEM L) . (vd,vd) > 0 by B10, ZMODLAT1:def 6;

hence ||.v.|| > 0 by B8, B9; :: thesis: verum

end;assume B1: v <> 0. (EMLat (r,L)) ; :: thesis: ||.v.|| > 0

consider T being linear-transformation of (EMbedding L),(EMbedding (r,L)) such that

B2: ( ( for v being Vector of (Z_MQ_VectSp L) st v in EMbedding L holds

T . v = r * v ) & T is bijective ) by ZMODUL08:27;

v in the carrier of (EMLat (r,L)) ;

then B0: v in r * (rng (MorphsZQ L)) by defrEMLat;

then v in the carrier of (EMbedding (r,L)) by ZMODUL08:def 6;

then v in rng T by B2, FUNCT_2:def 3;

then consider ve being object such that

B3: ( ve in the carrier of (EMbedding L) & v = T . ve ) by FUNCT_2:11;

reconsider vz = ve as Vector of (Z_MQ_VectSp L) by B3, ZMODUL08:19;

reconsider vd = vz as Vector of (DivisibleMod L) by ZMODUL08:30;

consider zvd being Vector of (DivisibleMod L) such that

B4: ( vd = rn * zvd & r * vz = rm * zvd ) by A1, ZMODUL08:31;

BX: vz in EMbedding L by B3;

B5: v = rm * zvd by B2, B3, B4, BX;

B6: v is Vector of (EMbedding (r,L)) by B0, ZMODUL08:def 6;

reconsider vd = vd as Vector of (EMbedding L) by B3;

B8: ||.v.|| = ((ScProductDM L) || (r * (rng (MorphsZQ L)))) . (v,v) by defrEMLat

.= ((ScProductDM L) || the carrier of (EMbedding (r,L))) . (v,v) by ZMODUL08:def 6

.= (ScProductDM L) . (v,v) by B6, ThSPrEM1

.= rm0 * ((ScProductDM L) . (zvd,(rm * zvd))) by B5, ThSPDM1

.= rm0 * ((ScProductDM L) . ((rm * zvd),zvd)) by ThSPDM1

.= rm0 * (rm0 * ((ScProductDM L) . (zvd,zvd))) by ThSPDM1

.= (rm0 * rm0) * ((ScProductDM L) . (zvd,zvd))

.= (rmf * rmf) * (((rnf ") * (rnf ")) * ((ScProductEM L) . (vd,vd))) by A1, B4, defScProductDM

.= ((rmf * rmf) * ((rnf ") * (rnf "))) * ((ScProductEM L) . (vd,vd)) ;

BY: rnf <> 0. F_Real by A1;

rm0 <> 0

proof

then
( rmf <> 0 & rnf " <> 0 )
by BY, VECTSP_1:25;
assume
rm0 = 0
; :: thesis: contradiction

then r = 0. F_Rat by A1;

hence contradiction ; :: thesis: verum

end;then r = 0. F_Rat by A1;

hence contradiction ; :: thesis: verum

then B9: ( rmf * rmf > 0 & (rnf ") * (rnf ") > 0 ) by XREAL_1:63;

vd in the carrier of (EMbedding L) ;

then vd in rng (MorphsZQ L) by ZMODUL08:def 3;

then reconsider vl = vd as Vector of (EMLat L) by defEMLat;

vd <> 0. (EMbedding L)

proof

then
vd <> zeroCoset L
by ZMODUL08:def 3;
assume C1:
vd = 0. (EMbedding L)
; :: thesis: contradiction

rn * zvd = zeroCoset L by B4, C1, ZMODUL08:def 3

.= 0. (DivisibleMod L) by ZMODUL08:def 4 ;

then zvd = 0. (DivisibleMod L) by ZMODUL01:def 7, a1;

then v = 0. (DivisibleMod L) by B5, ZMODUL01:1

.= zeroCoset L by ZMODUL08:def 4

.= 0. (EMLat (r,L)) by defrEMLat ;

hence contradiction by B1; :: thesis: verum

end;rn * zvd = zeroCoset L by B4, C1, ZMODUL08:def 3

.= 0. (DivisibleMod L) by ZMODUL08:def 4 ;

then zvd = 0. (DivisibleMod L) by ZMODUL01:def 7, a1;

then v = 0. (DivisibleMod L) by B5, ZMODUL01:1

.= zeroCoset L by ZMODUL08:def 4

.= 0. (EMLat (r,L)) by defrEMLat ;

hence contradiction by B1; :: thesis: verum

then B10: vd <> 0. (EMLat L) by defEMLat;

(ScProductEM L) . (vd,vd) = ||.vl.|| by defEMLat;

then (ScProductEM L) . (vd,vd) > 0 by B10, ZMODLAT1:def 6;

hence ||.v.|| > 0 by B8, B9; :: thesis: verum