let L be positive-definite Z_Lattice; :: thesis: for Z being non empty LatticeStr over INT.Ring st Z is Submodule of DivisibleMod L & the scalar of Z = (ScProductDM L) || the carrier of Z holds
Z is Z_Lattice-like
let Z be non empty LatticeStr over INT.Ring ; :: thesis: ( Z is Submodule of DivisibleMod L & the scalar of Z = (ScProductDM L) || the carrier of Z implies Z is Z_Lattice-like )
assume A1: ( Z is Submodule of DivisibleMod L & the scalar of Z = (ScProductDM L) || the carrier of Z ) ; :: thesis: Z is Z_Lattice-like
set A = the carrier of Z;
A2: for x, y being Vector of Z holds the scalar of Z . (x,y) = (ScProductDM L) . (x,y)

proof

let x, y be Vector of Z; :: thesis: the scalar of Z . (x,y) = (ScProductDM L) . (x,y)
[x,y] in [: the carrier of Z, the carrier of Z:] ;
hence the scalar of Z . (x,y) = (ScProductDM L) . (x,y) by A1, FUNCT_1:49; :: thesis: verum

end;

Z is Z_Lattice-like

proof

thus for x being Vector of Z st ( for y being Vector of Z holds <;x,y;> = 0 ) holds
x = 0. Z :: according to ZMODLAT1:def 3 :: thesis: ( ( for b₁, b₂ being Element of the carrier of Z holds <;b₁,b₂;> = <;b₂,b₁;> ) & ( for b₁, b₂, b₃ being Element of the carrier of Z
for b₄ being Element of the carrier of INT.Ring holds
( <;(b₁ + b₂),b₃;> = <;b₁,b₃;> + <;b₂,b₃;> & <;(b₄ * b₁),b₂;> = b₄ * <;b₁,b₂;> ) ) )

proof

let x be Vector of Z; :: thesis: ( ( for y being Vector of Z holds <;x,y;> = 0 ) implies x = 0. Z )
assume B1: for y being Vector of Z holds <;x,y;> = 0 ; :: thesis: x = 0. Z
B2: x is Vector of (DivisibleMod L) by A1, ZMODUL01:25;
assume x <> 0. Z ; :: thesis: contradiction
then x <> 0. (DivisibleMod L) by A1, ZMODUL01:26;
then (ScProductDM L) . (x,x) <> 0 by B2, ThSPDM2;
then the scalar of Z . (x,x) <> 0 by A2;
then <;x,x;> <> 0 ;
hence contradiction by B1; :: thesis: verum

end;

thus for x, y being Vector of Z holds <;x,y;> = <;y,x;> :: thesis: for b₁, b₂, b₃ being Element of the carrier of Z
for b₄ being Element of the carrier of INT.Ring holds
( <;(b₁ + b₂),b₃;> = <;b₁,b₃;> + <;b₂,b₃;> & <;(b₄ * b₁),b₂;> = b₄ * <;b₁,b₂;> )

proof

let x, y be Vector of Z; :: thesis: <;x,y;> = <;y,x;>
reconsider xx = x, yy = y as Vector of (DivisibleMod L) by A1, ZMODUL01:25;
thus <;x,y;> = the scalar of Z . (x,y)
.= (ScProductDM L) . (x,y) by A2
.= (ScProductDM L) . (yy,xx) by ThSPDM1
.= the scalar of Z . (y,x) by A2
.= <;y,x;> ; :: thesis: verum

end;

thus for x, y, z being Vector of Z
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 Z; :: 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 (DivisibleMod L) by A1, ZMODUL01:25;
B1: xx + yy = x + y by A1, ZMODUL01:28;
thus <;(x + y),z;> = the scalar of Z . ((x + y),z)
.= (ScProductDM L) . ((xx + yy),zz) by A2, B1
.= ((ScProductDM L) . (xx,zz)) + ((ScProductDM L) . (yy,zz)) by ThSPDM1
.= ( the scalar of Z . (x,z)) + ((ScProductDM L) . (y,z)) by A2
.= ( the scalar of Z . (x,z)) + ( the scalar of Z . (y,z)) by A2
.= <;x,z;> + <;y,z;> ; :: thesis: <;(a * x),y;> = a * <;x,y;>
B2: a * xx = a * x by A1, ZMODUL01:29;
thus <;(a * x),y;> = the scalar of Z . ((a * x),y)
.= (ScProductDM L) . ((a * xx),yy) by A2, B2
.= a * ((ScProductDM L) . (xx,yy)) by ThSPDM1
.= a * ( the scalar of Z . (x,y)) by A2
.= a * <;x,y;> ; :: thesis: verum

end;

end;

hence Z is Z_Lattice-like ; :: thesis: verum