let L be Z_Lattice; ScProductEM L = (ScProductDM L) || (rng (MorphsZQ L))
P1: [: the carrier of (EMbedding L), the carrier of (EMbedding L):] =
[: the carrier of (EMbedding L),(rng (MorphsZQ L)):]
by ZMODUL08:def 3
.=
[:(rng (MorphsZQ L)),(rng (MorphsZQ L)):]
by ZMODUL08:def 3
;
P2: [: the carrier of (DivisibleMod L), the carrier of (DivisibleMod L):] =
[: the carrier of (DivisibleMod L),(Class (EQRZM L)):]
by ZMODUL08:def 4
.=
[:(Class (EQRZM L)),(Class (EQRZM L)):]
by ZMODUL08:def 4
;
A0:
EMbedding L is Submodule of DivisibleMod L
by ZMODUL08:24;
then
the carrier of (EMbedding L) c= the carrier of (DivisibleMod L)
by VECTSP_4:def 2;
then
rng (MorphsZQ L) c= the carrier of (DivisibleMod L)
by ZMODUL08:def 3;
then
rng (MorphsZQ L) c= Class (EQRZM L)
by ZMODUL08:def 4;
then
[:(rng (MorphsZQ L)),(rng (MorphsZQ L)):] c= [:(Class (EQRZM L)),(Class (EQRZM L)):]
by ZFMISC_1:96;
then reconsider scd = (ScProductDM L) || (rng (MorphsZQ L)) as Function of [:(rng (MorphsZQ L)),(rng (MorphsZQ L)):], the carrier of F_Real by P2, FUNCT_2:32;
for x being object st x in [:(rng (MorphsZQ L)),(rng (MorphsZQ L)):] holds
(ScProductEM L) . x = scd . x
proof
let x be
object ;
( x in [:(rng (MorphsZQ L)),(rng (MorphsZQ L)):] implies (ScProductEM L) . x = scd . x )
assume B1:
x in [:(rng (MorphsZQ L)),(rng (MorphsZQ L)):]
;
(ScProductEM L) . x = scd . x
consider x1,
x2 being
object such that B2:
(
x1 in rng (MorphsZQ L) &
x2 in rng (MorphsZQ L) &
x = [x1,x2] )
by B1, ZFMISC_1:def 2;
reconsider x1 =
x1,
x2 =
x2 as
Vector of
(EMbedding L) by B2, ZMODUL08:def 3;
set a =
1. INT.Ring;
x1 in EMbedding L
;
then
x1 in DivisibleMod L
by A0, ZMODUL01:24;
then reconsider xx1 =
x1 as
Vector of
(DivisibleMod L) ;
x2 in EMbedding L
;
then
x2 in DivisibleMod L
by A0, ZMODUL01:24;
then reconsider xx2 =
x2 as
Vector of
(DivisibleMod L) ;
B3:
x1 = (1. INT.Ring) * xx1
by VECTSP_1:def 17;
B4:
x2 = (1. INT.Ring) * xx2
by VECTSP_1:def 17;
thus (ScProductEM L) . x =
((1. F_Real) * ((1. F_Real) ")) * ((ScProductEM L) . (x1,x2))
by B2
.=
(ScProductDM L) . (
xx1,
xx2)
by B3, B4, defScProductDM
.=
scd . x
by B2, FUNCT_1:49, ZFMISC_1:87
;
verum
end;
hence
ScProductEM L = (ScProductDM L) || (rng (MorphsZQ L))
by P1, FUNCT_2:12; verum