let L be positive-definite Z_Lattice; 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 ; 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; 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; 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; 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; ( 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 )
; 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
ZMODLAT1:def 3 ( ( 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;> ) ) )
thus
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,
y be
Vector of
L1;
<;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
;
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;> )
verumproof
let x,
y,
z be
Vector of
L1;
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;
( <;(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
;
<;(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
;
verum
end;
end;
hence
LatticeStr(# A,ad,ze,mu,sc #) is Z_Sublattice of L
by A1, defSublattice, AA; verum