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

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

hence
LX is RATional
by ZMODLAT2:def 1; :: thesis: verum
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;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