let L be Z_Lattice; :: thesis: 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

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

hence
ScProductEM L = (ScProductDM L) || (rng (MorphsZQ L))
by P1, FUNCT_2:12; :: thesis: verum
let x be object ; :: thesis: ( x in [:(rng (MorphsZQ L)),(rng (MorphsZQ L)):] implies (ScProductEM L) . x = scd . x )

assume B1: x in [:(rng (MorphsZQ L)),(rng (MorphsZQ L)):] ; :: thesis: (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 ; :: thesis: verum

end;assume B1: x in [:(rng (MorphsZQ L)),(rng (MorphsZQ L)):] ; :: thesis: (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 ; :: thesis: verum