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
proof
let v be
Vector of
(EMLat (r,L));
( v <> 0. (EMLat (r,L)) implies ||.v.|| > 0 )
assume B1:
v <> 0. (EMLat (r,L))
;
||.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
assume
rm0 = 0
;
contradiction
then
r = 0. F_Rat
by A1;
hence
contradiction
;
verum
end;
then
(
rmf <> 0 &
rnf " <> 0 )
by BY, VECTSP_1:25;
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
vd <> zeroCoset L
by ZMODUL08:def 3;
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;
verum
end;
hence
EMLat (r,L) is positive-definite
; verum