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)

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

Z is Z_Lattice-like
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;[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

proof

hence
Z is Z_Lattice-like
; :: thesis: verum
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_{1}, b_{2} being Element of the carrier of Z holds <;b_{1},b_{2};> = <;b_{2},b_{1};> ) & ( for b_{1}, b_{2}, b_{3} being Element of the carrier of Z

for b_{4} being Element of the carrier of INT.Ring holds

( <;(b_{1} + b_{2}),b_{3};> = <;b_{1},b_{3};> + <;b_{2},b_{3};> & <;(b_{4} * b_{1}),b_{2};> = b_{4} * <;b_{1},b_{2};> ) ) )_{1}, b_{2}, b_{3} being Element of the carrier of Z

for b_{4} being Element of the carrier of INT.Ring holds

( <;(b_{1} + b_{2}),b_{3};> = <;b_{1},b_{3};> + <;b_{2},b_{3};> & <;(b_{4} * b_{1}),b_{2};> = b_{4} * <;b_{1},b_{2};> )

for a being Element of INT.Ring holds

( <;(x + y),z;> = <;x,z;> + <;y,z;> & <;(a * x),y;> = a * <;x,y;> ) :: thesis: verum

end;x = 0. Z :: according to ZMODLAT1:def 3 :: thesis: ( ( for b

for b

( <;(b

proof

thus
for x, y being Vector of Z holds <;x,y;> = <;y,x;>
:: thesis: for b
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;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

for b

( <;(b

proof

thus
for x, y, z being Vector of Z
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;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

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;( <;(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