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
> 0
proof
let v be Vector of (EMLat (r,L)); :: thesis: ( v <> 0. (EMLat (r,L)) implies > 0 )
assume B1: v <> 0. (EMLat (r,L)) ; :: thesis:
consider T being linear-transformation of (),(EMbedding (r,L)) such that
B2: ( ( for v being Vector of () 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 ()) by defrEMLat;
then v in the carrier of (EMbedding (r,L)) by ZMODUL08:def 6;
then v in rng T by ;
then consider ve being object such that
B3: ( ve in the carrier of () & v = T . ve ) by FUNCT_2:11;
reconsider vz = ve as Vector of () by ;
reconsider vd = vz as Vector of () by ZMODUL08:30;
consider zvd being Vector of () such that
B4: ( vd = rn * zvd & r * vz = rm * zvd ) by ;
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 ;
reconsider vd = vd as Vector of () by B3;
B8: = (() || (r * (rng ()))) . (v,v) by defrEMLat
.= (() || the carrier of (EMbedding (r,L))) . (v,v) by ZMODUL08:def 6
.= () . (v,v) by
.= rm0 * (() . (zvd,(rm * zvd))) by
.= rm0 * (() . ((rm * zvd),zvd)) by ThSPDM1
.= rm0 * (rm0 * (() . (zvd,zvd))) by ThSPDM1
.= (rm0 * rm0) * (() . (zvd,zvd))
.= (rmf * rmf) * (((rnf ") * (rnf ")) * (() . (vd,vd))) by
.= ((rmf * rmf) * ((rnf ") * (rnf "))) * (() . (vd,vd)) ;
BY: rnf <> 0. F_Real by A1;
rm0 <> 0
proof
assume rm0 = 0 ; :: thesis: contradiction
then r = 0. F_Rat by A1;
hence contradiction ; :: thesis: verum
end;
then ( rmf <> 0 & rnf " <> 0 ) by ;
then B9: ( rmf * rmf > 0 & (rnf ") * (rnf ") > 0 ) by XREAL_1:63;
vd in the carrier of () ;
then vd in rng () by ZMODUL08:def 3;
then reconsider vl = vd as Vector of () by defEMLat;
vd <> 0. ()
proof
assume C1: vd = 0. () ; :: thesis: contradiction
rn * zvd = zeroCoset L by
.= 0. () by ZMODUL08:def 4 ;
then zvd = 0. () by ;
then v = 0. () by
.= zeroCoset L by ZMODUL08:def 4
.= 0. (EMLat (r,L)) by defrEMLat ;
hence contradiction by B1; :: thesis: verum
end;
then vd <> zeroCoset L by ZMODUL08:def 3;
then B10: vd <> 0. () by defEMLat;
(ScProductEM L) . (vd,vd) = ||.vl.|| by defEMLat;
then (ScProductEM L) . (vd,vd) > 0 by ;
hence ||.v.|| > 0 by B8, B9; :: thesis: verum
end;
hence EMLat (r,L) is positive-definite ; :: thesis: verum