reconsider ad = the addF of (DivisibleMod L) || (DualSet L) as Function of [:(DualSet L),(DualSet L):], the carrier of (DivisibleMod L) by FUNCT_2:32;

for z being Element of [:(DualSet L),(DualSet L):] holds ad . z in DualSet L

then reconsider ad = ad as BinOp of (DualSet L) by FUNCT_2:6;

0. (DivisibleMod L) is Dual of L by LmDE0;

then 0. (DivisibleMod L) in DualSet L ;

then reconsider ze = 0. (DivisibleMod L) as Element of DualSet L ;

[: the carrier of INT.Ring,(DualSet L):] c= [: the carrier of INT.Ring, the carrier of (DivisibleMod L):] by ZFMISC_1:95;

then reconsider mu = the lmult of (DivisibleMod L) | [: the carrier of INT.Ring,(DualSet L):] as Function of [: the carrier of INT.Ring,(DualSet L):], the carrier of (DivisibleMod L) by FUNCT_2:32;

for z being Element of [: the carrier of INT.Ring,(DualSet L):] holds mu . z in DualSet L

then reconsider mu = mu as Function of [: the carrier of INT.Ring,(DualSet L):],(DualSet L) by FUNCT_2:6;

reconsider sc = (ScProductDM L) | [:(DualSet L),(DualSet L):] as Function of [:(DualSet L),(DualSet L):], the carrier of F_Real by FUNCT_2:32;

take IT = LatticeStr(# (DualSet L),ad,ze,mu,sc #); :: thesis: ( the carrier of IT = DualSet L & the addF of IT = the addF of (DivisibleMod L) || (DualSet L) & the ZeroF of IT = 0. (DivisibleMod L) & the lmult of IT = the lmult of (DivisibleMod L) | [: the carrier of INT.Ring,(DualSet L):] & the scalar of IT = (ScProductDM L) | [:(DualSet L),(DualSet L):] )

thus ( the carrier of IT = DualSet L & the addF of IT = the addF of (DivisibleMod L) || (DualSet L) & the ZeroF of IT = 0. (DivisibleMod L) & the lmult of IT = the lmult of (DivisibleMod L) | [: the carrier of INT.Ring,(DualSet L):] & the scalar of IT = (ScProductDM L) | [:(DualSet L),(DualSet L):] ) ; :: thesis: verum

for z being Element of [:(DualSet L),(DualSet L):] holds ad . z in DualSet L

proof

then
rng ad c= DualSet L
by FUNCT_2:114;
let z be Element of [:(DualSet L),(DualSet L):]; :: thesis: ad . z in DualSet L

consider x, y being object such that

G1: ( x in DualSet L & y in DualSet L & z = [x,y] ) by ZFMISC_1:def 2;

reconsider x = x, y = y as Element of (DivisibleMod L) by G1;

ad . z = x + y by FUNCT_1:49, G1;

hence ad . z in DualSet L by G1, VECTSP_4:def 1; :: thesis: verum

end;consider x, y being object such that

G1: ( x in DualSet L & y in DualSet L & z = [x,y] ) by ZFMISC_1:def 2;

reconsider x = x, y = y as Element of (DivisibleMod L) by G1;

ad . z = x + y by FUNCT_1:49, G1;

hence ad . z in DualSet L by G1, VECTSP_4:def 1; :: thesis: verum

then reconsider ad = ad as BinOp of (DualSet L) by FUNCT_2:6;

0. (DivisibleMod L) is Dual of L by LmDE0;

then 0. (DivisibleMod L) in DualSet L ;

then reconsider ze = 0. (DivisibleMod L) as Element of DualSet L ;

[: the carrier of INT.Ring,(DualSet L):] c= [: the carrier of INT.Ring, the carrier of (DivisibleMod L):] by ZFMISC_1:95;

then reconsider mu = the lmult of (DivisibleMod L) | [: the carrier of INT.Ring,(DualSet L):] as Function of [: the carrier of INT.Ring,(DualSet L):], the carrier of (DivisibleMod L) by FUNCT_2:32;

for z being Element of [: the carrier of INT.Ring,(DualSet L):] holds mu . z in DualSet L

proof

then
rng mu c= DualSet L
by FUNCT_2:114;
let z be Element of [: the carrier of INT.Ring,(DualSet L):]; :: thesis: mu . z in DualSet L

consider x, y being object such that

G1: ( x in the carrier of INT.Ring & y in DualSet L & z = [x,y] ) by ZFMISC_1:def 2;

reconsider x = x as Element of INT.Ring by G1;

reconsider y = y as Element of (DivisibleMod L) by G1;

mu . z = x * y by FUNCT_1:49, G1;

hence mu . z in DualSet L by G1, VECTSP_4:def 1; :: thesis: verum

end;consider x, y being object such that

G1: ( x in the carrier of INT.Ring & y in DualSet L & z = [x,y] ) by ZFMISC_1:def 2;

reconsider x = x as Element of INT.Ring by G1;

reconsider y = y as Element of (DivisibleMod L) by G1;

mu . z = x * y by FUNCT_1:49, G1;

hence mu . z in DualSet L by G1, VECTSP_4:def 1; :: thesis: verum

then reconsider mu = mu as Function of [: the carrier of INT.Ring,(DualSet L):],(DualSet L) by FUNCT_2:6;

reconsider sc = (ScProductDM L) | [:(DualSet L),(DualSet L):] as Function of [:(DualSet L),(DualSet L):], the carrier of F_Real by FUNCT_2:32;

take IT = LatticeStr(# (DualSet L),ad,ze,mu,sc #); :: thesis: ( the carrier of IT = DualSet L & the addF of IT = the addF of (DivisibleMod L) || (DualSet L) & the ZeroF of IT = 0. (DivisibleMod L) & the lmult of IT = the lmult of (DivisibleMod L) | [: the carrier of INT.Ring,(DualSet L):] & the scalar of IT = (ScProductDM L) | [:(DualSet L),(DualSet L):] )

thus ( the carrier of IT = DualSet L & the addF of IT = the addF of (DivisibleMod L) || (DualSet L) & the ZeroF of IT = 0. (DivisibleMod L) & the lmult of IT = the lmult of (DivisibleMod L) | [: the carrier of INT.Ring,(DualSet L):] & the scalar of IT = (ScProductDM L) | [:(DualSet L),(DualSet L):] ) ; :: thesis: verum