set V = the non trivial torsion-free Z_Module;
set v = the non zero Vector of the non trivial torsion-free Z_Module;
set Z = Lin { the non zero Vector of the non trivial torsion-free Z_Module};
defpred S1[ object , object ] means ex a, b being Element of INT.Ring st
( c1 = [(a * the non zero Vector of the non trivial torsion-free Z_Module),(b * the non zero Vector of the non trivial torsion-free Z_Module)] & c2 = a * b );
A1: for x being Element of [: the carrier of (Lin { the non zero Vector of the non trivial torsion-free Z_Module}), the carrier of (Lin { the non zero Vector of the non trivial torsion-free Z_Module}):] ex y being Element of the carrier of F_Real st S1[x,y]
proof
let x be Element of [: the carrier of (Lin { the non zero Vector of the non trivial torsion-free Z_Module}), the carrier of (Lin { the non zero Vector of the non trivial torsion-free Z_Module}):]; :: thesis: ex y being Element of the carrier of F_Real st S1[x,y]
consider x1, x2 being object such that
B1: ( x1 in the carrier of (Lin { the non zero Vector of the non trivial torsion-free Z_Module}) & x2 in the carrier of (Lin { the non zero Vector of the non trivial torsion-free Z_Module}) & x = [x1,x2] ) by ZFMISC_1:def 2;
reconsider x1 = x1, x2 = x2 as Vector of (Lin { the non zero Vector of the non trivial torsion-free Z_Module}) by B1;
x1 in Lin { the non zero Vector of the non trivial torsion-free Z_Module} ;
then consider i1 being Element of INT.Ring such that
B2: x1 = i1 * the non zero Vector of the non trivial torsion-free Z_Module by ZMODUL06:19;
x2 in Lin { the non zero Vector of the non trivial torsion-free Z_Module} ;
then consider i2 being Element of INT.Ring such that
B3: x2 = i2 * the non zero Vector of the non trivial torsion-free Z_Module by ZMODUL06:19;
reconsider i12 = i1 * i2 as Element of INT ;
INT c= the carrier of F_Real by NUMBERS:5, XBOOLE_0:def 8;
then reconsider i12 = i12 as Element of F_Real ;
take i12 ; :: thesis: S1[x,i12]
thus S1[x,i12] by B1, B2, B3; :: thesis: verum
end;
consider f being Function of [: the carrier of (Lin { the non zero Vector of the non trivial torsion-free Z_Module}), the carrier of (Lin { the non zero Vector of the non trivial torsion-free Z_Module}):], the carrier of F_Real such that
A2: for x being Element of [: the carrier of (Lin { the non zero Vector of the non trivial torsion-free Z_Module}), the carrier of (Lin { the non zero Vector of the non trivial torsion-free Z_Module}):] holds S1[x,f . x] from FUNCT_2:sch 3(A1);
 A3: for a, b being Element of INT.Ring holds f . [(a * the non zero Vector of the non trivial torsion-free Z_Module),(b * the non zero Vector of the non trivial torsion-free Z_Module)] = a * b
proof
let a, b be Element of INT.Ring; :: thesis: f . [(a * the non zero Vector of the non trivial torsion-free Z_Module),(b * the non zero Vector of the non trivial torsion-free Z_Module)] = a * b
( a * the non zero Vector of the non trivial torsion-free Z_Module in Lin { the non zero Vector of the non trivial torsion-free Z_Module} & b * the non zero Vector of the non trivial torsion-free Z_Module in Lin { the non zero Vector of the non trivial torsion-free Z_Module} ) by ZMODUL06:21;
then [(a * the non zero Vector of the non trivial torsion-free Z_Module),(b * the non zero Vector of the non trivial torsion-free Z_Module)] in [: the carrier of (Lin { the non zero Vector of the non trivial torsion-free Z_Module}), the carrier of (Lin { the non zero Vector of the non trivial torsion-free Z_Module}):] by ZFMISC_1:87;
then consider a0, b0 being Element of INT.Ring such that
B1: ( [(a * the non zero Vector of the non trivial torsion-free Z_Module),(b * the non zero Vector of the non trivial torsion-free Z_Module)] = [(a0 * the non zero Vector of the non trivial torsion-free Z_Module),(b0 * the non zero Vector of the non trivial torsion-free Z_Module)] & f . [(a * the non zero Vector of the non trivial torsion-free Z_Module),(b * the non zero Vector of the non trivial torsion-free Z_Module)] = a0 * b0 ) by A2;
B2: the non zero Vector of the non trivial torsion-free Z_Module <> 0. the non trivial torsion-free Z_Module ;
a * the non zero Vector of the non trivial torsion-free Z_Module = a0 * the non zero Vector of the non trivial torsion-free Z_Module by B1, XTUPLE_0:1;
then B3: a = a0 by B2, ZMODUL01:11;
b * the non zero Vector of the non trivial torsion-free Z_Module = b0 * the non zero Vector of the non trivial torsion-free Z_Module by B1, XTUPLE_0:1;
hence f . [(a * the non zero Vector of the non trivial torsion-free Z_Module),(b * the non zero Vector of the non trivial torsion-free Z_Module)] = a * b by B1, B2, B3, ZMODUL01:11; :: thesis: verum
end;
set L = GenLat ((Lin { the non zero Vector of the non trivial torsion-free Z_Module}),f);
reconsider L = GenLat ((Lin { the non zero Vector of the non trivial torsion-free Z_Module}),f) as non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed free finite-rank LatticeStr over INT.Ring ;
L is Z_Lattice-like
proof
thus for x being Vector of L st ( for y being Vector of L holds <;x,y;> = 0 ) holds
x = 0. L :: according to ZMODLAT1:def 3 :: thesis: ( ( for x, y being Vector of L holds <;x,y;> = <;y,x;> ) & ( for x, y, z being Vector of L
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 L; :: thesis: ( ( for y being Vector of L holds <;x,y;> = 0 ) implies x = 0. L )
assume C1: for y being Vector of L holds <;x,y;> = 0 ; :: thesis: x = 0. L
assume x <> 0. L ; :: thesis: contradiction
then C2: x <> 0. the non trivial torsion-free Z_Module by ZMODUL01:26;
x in Lin { the non zero Vector of the non trivial torsion-free Z_Module} ;
then consider ix being Element of INT.Ring such that
C3: x = ix * the non zero Vector of the non trivial torsion-free Z_Module by ZMODUL06:19;
C4: ix <> 0 by C2, C3, ZMODUL01:1;
<;x,x;> = ix * ix by A3, C3;
hence contradiction by C1, C4; :: thesis: verum
end;
thus for x, y being Vector of L holds <;x,y;> = <;y,x;> :: thesis: for x, y, z being Vector of L
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 L; :: thesis: <;x,y;> = <;y,x;>
C1: ( x in Lin { the non zero Vector of the non trivial torsion-free Z_Module} & y in Lin { the non zero Vector of the non trivial torsion-free Z_Module} ) ;
then consider ix being Element of INT.Ring such that
C2: x = ix * the non zero Vector of the non trivial torsion-free Z_Module by ZMODUL06:19;
consider iy being Element of INT.Ring such that
C3: y = iy * the non zero Vector of the non trivial torsion-free Z_Module by C1, ZMODUL06:19;
thus <;x,y;> = ix * iy by A3, C2, C3
.= <;y,x;> by A3, C2, C3 ; :: thesis: verum
end;
thus for x, y, z being Vector of L
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 L; :: 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;> )
C1: ( x in Lin { the non zero Vector of the non trivial torsion-free Z_Module} & y in Lin { the non zero Vector of the non trivial torsion-free Z_Module} & z in Lin { the non zero Vector of the non trivial torsion-free Z_Module} ) ;
then consider ix being Element of INT.Ring such that
C2: x = ix * the non zero Vector of the non trivial torsion-free Z_Module by ZMODUL06:19;
consider iy being Element of INT.Ring such that
C3: y = iy * the non zero Vector of the non trivial torsion-free Z_Module by C1, ZMODUL06:19;
consider iz being Element of INT.Ring such that
C4: z = iz * the non zero Vector of the non trivial torsion-free Z_Module by C1, ZMODUL06:19;
ix * the non zero Vector of the non trivial torsion-free Z_Module in Lin { the non zero Vector of the non trivial torsion-free Z_Module} by ZMODUL06:21;
then reconsider iixv = ix * the non zero Vector of the non trivial torsion-free Z_Module as Vector of (Lin { the non zero Vector of the non trivial torsion-free Z_Module}) ;
reconsider ixv = ix * the non zero Vector of the non trivial torsion-free Z_Module as Vector of the non trivial torsion-free Z_Module ;
iy * the non zero Vector of the non trivial torsion-free Z_Module in Lin { the non zero Vector of the non trivial torsion-free Z_Module} by ZMODUL06:21;
then reconsider iiyv = iy * the non zero Vector of the non trivial torsion-free Z_Module as Vector of (Lin { the non zero Vector of the non trivial torsion-free Z_Module}) ;
reconsider iyv = iy * the non zero Vector of the non trivial torsion-free Z_Module as Vector of the non trivial torsion-free Z_Module ;
C5: x + y = iixv + iiyv by C2, C3
.= ixv + iyv by ZMODUL01:28
.= (ix + iy) * the non zero Vector of the non trivial torsion-free Z_Module by VECTSP_1:def 15 ;
C6: a * x = a * iixv by C2
.= a * ixv by ZMODUL01:29
.= (a * ix) * the non zero Vector of the non trivial torsion-free Z_Module by VECTSP_1:def 16 ;
thus <;(x + y),z;> = (ix + iy) * iz by A3, C4, C5
.= (ix * iz) + (iy * iz)
.= (f . [x,z]) + (iy * iz) by A3, C2, C4
.= <;x,z;> + <;y,z;> by A3, C3, C4 ; :: thesis: <;(a * x),y;> = a * <;x,y;>
thus <;(a * x),y;> = (a * ix) * iy by A3, C3, C6
.= a * (ix * iy)
.= a * <;x,y;> by A3, C2, C3 ; :: thesis: verum
end;
end;
then reconsider L = L as Z_Lattice ;
A4: for u being Vector of L st u <> 0. L holds
||.u.|| > 0
proof
let u be Vector of L; :: thesis: ( u <> 0. L implies ||.u.|| > 0 )
assume B1: u <> 0. L ; :: thesis: ||.u.|| > 0
B2: u <> 0. the non trivial torsion-free Z_Module by B1, ZMODUL01:26;
u in Lin { the non zero Vector of the non trivial torsion-free Z_Module} ;
then consider iu being Element of INT.Ring such that
B4: u = iu * the non zero Vector of the non trivial torsion-free Z_Module by ZMODUL06:19;
B5: iu <> 0 by B2, B4, ZMODUL01:1;
||.u.|| = iu * iu by A3, B4;
hence ||.u.|| > 0 by B5, XREAL_1:63; :: thesis: verum
end;
take L ; :: thesis: ( not L is trivial & L is INTegral & L is positive-definite )
A5: not L is trivial
proof
assume B1: L is trivial ; :: thesis: contradiction
the non zero Vector of the non trivial torsion-free Z_Module in Lin { the non zero Vector of the non trivial torsion-free Z_Module} by ZMODUL06:20;
then B2: the non zero Vector of the non trivial torsion-free Z_Module = 0. L by B1;
the non zero Vector of the non trivial torsion-free Z_Module <> 0. the non trivial torsion-free Z_Module ;
hence contradiction by B2, ZMODUL01:26; :: thesis: verum
end;
for w, u being Vector of L holds <;w,u;> in INT
proof
let w, u be Vector of L; :: thesis: <;w,u;> in INT
w in Lin { the non zero Vector of the non trivial torsion-free Z_Module} ;
then consider iw being Element of INT.Ring such that
B1: w = iw * the non zero Vector of the non trivial torsion-free Z_Module by ZMODUL06:19;
u in Lin { the non zero Vector of the non trivial torsion-free Z_Module} ;
then consider iu being Element of INT.Ring such that
B2: u = iu * the non zero Vector of the non trivial torsion-free Z_Module by ZMODUL06:19;
<;w,u;> = iw * iu by A3, B1, B2;
hence <;w,u;> in INT ; :: thesis: verum
end;
hence ( not L is trivial & L is INTegral & L is positive-definite ) by A4, A5; :: thesis: verum