let L be positive-definite Z_Lattice; :: thesis: for A being non empty set
for ze being Element of A
for ad being BinOp of A
for mu being Function of [: the carrier of INT.Ring,A:],A
for sc being Function of [:A,A:], the carrier of F_Real st A is linearly-closed Subset of L & ze = 0. L & ad = the addF of L || A & mu = the lmult of L | [: the carrier of INT.Ring,A:] & sc = the scalar of L || A holds
LatticeStr(# A,ad,ze,mu,sc #) is Z_Sublattice of L
let A be non empty set ; :: thesis: for ze being Element of A
for ad being BinOp of A
for mu being Function of [: the carrier of INT.Ring,A:],A
for sc being Function of [:A,A:], the carrier of F_Real st A is linearly-closed Subset of L & ze = 0. L & ad = the addF of L || A & mu = the lmult of L | [: the carrier of INT.Ring,A:] & sc = the scalar of L || A holds
LatticeStr(# A,ad,ze,mu,sc #) is Z_Sublattice of L
let ze be Element of A; :: thesis: for ad being BinOp of A
for mu being Function of [: the carrier of INT.Ring,A:],A
for sc being Function of [:A,A:], the carrier of F_Real st A is linearly-closed Subset of L & ze = 0. L & ad = the addF of L || A & mu = the lmult of L | [: the carrier of INT.Ring,A:] & sc = the scalar of L || A holds
LatticeStr(# A,ad,ze,mu,sc #) is Z_Sublattice of L
let ad be BinOp of A; :: thesis: for mu being Function of [: the carrier of INT.Ring,A:],A
for sc being Function of [:A,A:], the carrier of F_Real st A is linearly-closed Subset of L & ze = 0. L & ad = the addF of L || A & mu = the lmult of L | [: the carrier of INT.Ring,A:] & sc = the scalar of L || A holds
LatticeStr(# A,ad,ze,mu,sc #) is Z_Sublattice of L
let mu be Function of [: the carrier of INT.Ring,A:],A; :: thesis: for sc being Function of [:A,A:], the carrier of F_Real st A is linearly-closed Subset of L & ze = 0. L & ad = the addF of L || A & mu = the lmult of L | [: the carrier of INT.Ring,A:] & sc = the scalar of L || A holds
LatticeStr(# A,ad,ze,mu,sc #) is Z_Sublattice of L
let sc be Function of [:A,A:], the carrier of F_Real; :: thesis: ( A is linearly-closed Subset of L & ze = 0. L & ad = the addF of L || A & mu = the lmult of L | [: the carrier of INT.Ring,A:] & sc = the scalar of L || A implies LatticeStr(# A,ad,ze,mu,sc #) is Z_Sublattice of L )
assume A1: ( A is linearly-closed Subset of L & ze = 0. L & ad = the addF of L || A & mu = the lmult of L | [: the carrier of INT.Ring,A:] & sc = the scalar of L || A ) ; :: thesis: LatticeStr(# A,ad,ze,mu,sc #) is Z_Sublattice of L
set L1 = LatticeStr(# A,ad,ze,mu,sc #);
set V1 = ModuleStr(# A,ad,ze,mu #);
reconsider V1 = ModuleStr(# A,ad,ze,mu #) as Submodule of L by A1, ZMODUL01:40;
AY3: ( A = the carrier of V1 & ze = 0. V1 & ad = the addF of V1 & mu = the lmult of V1 ) ;
reconsider scc = sc as Function of [: the carrier of V1, the carrier of V1:], the carrier of F_Real ;
AA: LatticeStr(# A,ad,ze,mu,sc #) = GenLat (V1,scc) ;
then A3: LatticeStr(# A,ad,ze,mu,sc #) is Submodule of V1 by LmZMtoZL1;
reconsider L1 = LatticeStr(# A,ad,ze,mu,sc #) as non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed LatticeStr over INT.Ring by AA;
reconsider L1 = L1 as non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed free LatticeStr over INT.Ring by AA;
AX3: L1 is Submodule of L by A3, ZMODUL01:42;
L1 is Z_Lattice-like
proof
thus for x being Vector of L1 st ( for y being Vector of L1 holds <;x,y;> = 0 ) holds
x = 0. L1 :: according to ZMODLAT1:def 3 :: thesis: ( ( for x, y being Vector of L1 holds <;x,y;> = <;y,x;> ) & ( for x, y, z being Vector of L1
for a being Element of INT.Ring holds
( <;(x + y),z;> = <;x,z;> + <;y,z;> & <;(a * x),y;> = a * <;x,y;> ) ) )
proof
let x be Vector of L1; :: thesis: ( ( for y being Vector of L1 holds <;x,y;> = 0 ) implies x = 0. L1 )
assume B1: for y being Vector of L1 holds <;x,y;> = 0 ; :: thesis: x = 0. L1
reconsider xx = x as Vector of L by AY3, ZMODUL01:25;
assume x <> 0. L1 ; :: thesis: contradiction
then ||.xx.|| <> 0 by A1, defPositive;
then <;x,x;> <> 0 by A1, FUNCT_1:49;
hence contradiction by B1; :: thesis: verum
end;
thus for x, y being Vector of L1 holds <;x,y;> = <;y,x;> :: thesis: for x, y, z being Vector of L1
for a being Element of INT.Ring holds
( <;(x + y),z;> = <;x,z;> + <;y,z;> & <;(a * x),y;> = a * <;x,y;> )
proof
let x, y be Vector of L1; :: thesis: <;x,y;> = <;y,x;>
reconsider xx = x, yy = y as Vector of L by AY3, ZMODUL01:25;
thus <;x,y;> = <;xx,yy;> by A1, FUNCT_1:49
.= <;yy,xx;> by defZLattice
.= <;y,x;> by A1, FUNCT_1:49 ; :: thesis: verum
end;
thus for x, y, z being Vector of L1
for a being Element of INT.Ring holds
( <;(x + y),z;> = <;x,z;> + <;y,z;> & <;(a * x),y;> = a * <;x,y;> ) :: thesis: verum
proof
let x, y, z be Vector of L1; :: thesis: for a being Element of INT.Ring holds
( <;(x + y),z;> = <;x,z;> + <;y,z;> & <;(a * x),y;> = a * <;x,y;> )
let a be Element of INT.Ring; :: thesis: ( <;(x + y),z;> = <;x,z;> + <;y,z;> & <;(a * x),y;> = a * <;x,y;> )
reconsider xx = x, yy = y, zz = z as Vector of L by AY3, ZMODUL01:25;
xx + yy = x + y by AX3, ZMODUL01:28;
hence <;(x + y),z;> = <;(xx + yy),zz;> by A1, FUNCT_1:49
.= <;xx,zz;> + <;yy,zz;> by defZLattice
.= <;x,z;> + <;yy,zz;> by A1, FUNCT_1:49
.= <;x,z;> + <;y,z;> by A1, FUNCT_1:49 ;
:: thesis: <;(a * x),y;> = a * <;x,y;>
a * xx = a * x by AX3, ZMODUL01:29;
hence <;(a * x),y;> = <;(a * xx),yy;> by A1, FUNCT_1:49
.= a * <;xx,yy;> by defZLattice
.= a * <;x,y;> by A1, FUNCT_1:49 ;
:: thesis: verum
end;
end;
hence LatticeStr(# A,ad,ze,mu,sc #) is Z_Sublattice of L by A1, defSublattice, AA; :: thesis: verum