let L be RATional Z_Lattice; :: thesis: for LX being Z_Lattice st LX is Submodule of DivisibleMod L & the scalar of LX = (ScProductDM L) || the carrier of LX holds
LX is RATional
let LX be Z_Lattice; :: thesis: ( LX is Submodule of DivisibleMod L & the scalar of LX = (ScProductDM L) || the carrier of LX implies LX is RATional )
assume A1: ( LX is Submodule of DivisibleMod L & the scalar of LX = (ScProductDM L) || the carrier of LX ) ; :: thesis: LX is RATional
for v, u being Vector of LX holds <;v,u;> in RAT
proof
let v, u be Vector of LX; :: thesis: <;v,u;> in RAT
reconsider vv = v, uu = u as Vector of (DivisibleMod L) by A1, ZMODUL01:25;
<;v,u;> = (ScProductDM L) . (vv,uu) by A1, FUNCT_1:49;
hence <;v,u;> in RAT by RAT_1:def 2; :: thesis: verum
end;
hence LX is RATional by ZMODLAT2:def 1; :: thesis: verum