set Z = EMLat L;
for v, u being Vector of (EMLat L) holds <;v,u;> in INT
proof
let v,
u be
Vector of
(EMLat L);
<;v,u;> in INT
v in the
carrier of
(EMLat L)
;
then
v in rng (MorphsZQ L)
by defEMLat;
then B3:
v is
Vector of
(EMbedding L)
by ZMODUL08:def 3;
then consider vv being
Vector of
L such that B1:
(MorphsZQ L) . vv = v
by ZMODUL08:22;
u in the
carrier of
(EMLat L)
;
then
u in rng (MorphsZQ L)
by defEMLat;
then B4:
u is
Vector of
(EMbedding L)
by ZMODUL08:def 3;
then consider uu being
Vector of
L such that B2:
(MorphsZQ L) . uu = u
by ZMODUL08:22;
<;v,u;> =
(ScProductEM L) . (
v,
u)
by defEMLat
.=
<;vv,uu;>
by B1, B2, B3, B4, defScProductEM
;
hence
<;v,u;> in INT
by ZMODLAT1:def 5;
verum
end;
hence
EMLat L is INTegral
; verum