set A = DualSet L;
reconsider A = DualSet L as non empty Subset of () ;
set ad = the addF of () || A;
dom the addF of () = [: the carrier of (), the carrier of ():] by FUNCT_2:def 1;
then A3: dom ( the addF of () || A) = [: the carrier of (), the carrier of ():] /\ [:A,A:] by RELAT_1:61
.= [:A,A:] by XBOOLE_1:28 ;
for x being object st x in [:A,A:] holds
( the addF of () || A) . x in A
proof
let x be object ; :: thesis: ( x in [:A,A:] implies ( the addF of () || A) . x in A )
assume B1: x in [:A,A:] ; :: thesis: ( the addF of () || A) . x in A
then consider x1, x2 being object such that
B2: ( x1 in A & x2 in A & x = [x1,x2] ) by ZFMISC_1:def 2;
reconsider v1 = x1, v2 = x2 as Vector of () by B2;
( the addF of () || A) . (x1,x2) = v1 + v2 by ;
hence ( the addF of () || A) . x in A by ; :: thesis: verum
end;
then reconsider ad = the addF of () || A as Function of [:A,A:],A by ;
A6: [: the carrier of INT.Ring,A:] c= [: the carrier of INT.Ring, the carrier of ():] by ZFMISC_1:95;
set mu = the lmult of () | [: the carrier of INT.Ring,A:];
dom the lmult of () = [: the carrier of INT.Ring, the carrier of ():] by FUNCT_2:def 1;
then A4: dom ( the lmult of () | [: the carrier of INT.Ring,A:]) = [: the carrier of INT.Ring, the carrier of ():] /\ [: the carrier of INT.Ring,A:] by RELAT_1:61
.= [: the carrier of INT.Ring,A:] by ;
for x being object st x in [: the carrier of INT.Ring,A:] holds
( the lmult of () | [: the carrier of INT.Ring,A:]) . x in A
proof
let x be object ; :: thesis: ( x in [: the carrier of INT.Ring,A:] implies ( the lmult of () | [: the carrier of INT.Ring,A:]) . x in A )
assume B1: x in [: the carrier of INT.Ring,A:] ; :: thesis: ( the lmult of () | [: the carrier of INT.Ring,A:]) . x in A
then consider x1, x2 being object such that
B2: ( x1 in INT & x2 in A & x = [x1,x2] ) by ZFMISC_1:def 2;
reconsider i1 = x1 as Element of INT.Ring by B2;
reconsider v2 = x2 as Vector of () by B2;
( the lmult of () | [: the carrier of INT.Ring,A:]) . (x1,x2) = i1 * v2 by ;
hence ( the lmult of () | [: the carrier of INT.Ring,A:]) . x in A by ; :: thesis: verum
end;
then reconsider mu = the lmult of () | [: the carrier of INT.Ring,A:] as Function of [: the carrier of INT.Ring,A:],A by ;
set sc = () || A;
dom () = [: the carrier of (), the carrier of ():] by FUNCT_2:def 1;
then A5: dom (() || A) = [: the carrier of (), the carrier of ():] /\ [:A,A:] by RELAT_1:61
.= [:A,A:] by XBOOLE_1:28 ;
for x being object st x in [:A,A:] holds
(() || A) . x in the carrier of F_Real
proof
let x be object ; :: thesis: ( x in [:A,A:] implies (() || A) . x in the carrier of F_Real )
assume B1: x in [:A,A:] ; :: thesis: (() || A) . x in the carrier of F_Real
then consider x1, x2 being object such that
B2: ( x1 in A & x2 in A & x = [x1,x2] ) by ZFMISC_1:def 2;
reconsider v1 = x1, v2 = x2 as Vector of () by B2;
((ScProductDM L) || A) . (x1,x2) = () . (v1,v2) by ;
hence ((ScProductDM L) || A) . x in the carrier of F_Real by B2; :: thesis: verum
end;
then reconsider sc = () || A as Function of [:A,A:], the carrier of F_Real by ;
reconsider ze = 0. () as Element of A by ZMODUL01:18;
set L1 = LatticeStr(# A,ad,ze,mu,sc #);
reconsider L1 = LatticeStr(# A,ad,ze,mu,sc #) as non empty LatticeStr over INT.Ring ;
A7: L1 is Submodule of DivisibleMod L by ZMODLAT2:10;
reconsider L1 = L1 as non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed LatticeStr over INT.Ring by ZMODLAT2:10;
set I = the Basis of ();
for v being Vector of () st v in L1 holds
v in Lin (DualBasis the Basis of ())
proof
let v be Vector of (); :: thesis: ( v in L1 implies v in Lin (DualBasis the Basis of ()) )
assume B1: v in L1 ; :: thesis: v in Lin (DualBasis the Basis of ())
consider x being Dual of L such that
B2: x = v by B1;
thus v in Lin (DualBasis the Basis of ()) by ; :: thesis: verum
end;
then L1 is Submodule of Lin (DualBasis the Basis of ()) by ;
then reconsider L1 = L1 as strict Z_Lattice by ;
take L1 ; :: thesis: ( the carrier of L1 = DualSet L & 0. L1 = 0. () & the addF of L1 = the addF of () || the carrier of L1 & the lmult of L1 = the lmult of () | [: the carrier of INT.Ring, the carrier of L1:] & the scalar of L1 = () || the carrier of L1 )
thus ( the carrier of L1 = DualSet L & 0. L1 = 0. () & the addF of L1 = the addF of () || the carrier of L1 & the lmult of L1 = the lmult of () | [: the carrier of INT.Ring, the carrier of L1:] & the scalar of L1 = () || the carrier of L1 ) ; :: thesis: verum