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}):];
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 the
carrier of
F_Real ;
take
i12
;
S1[x,i12]
thus
S1[
x,
i12]
by B1, B2, B3;
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 v1, v2 being Vector of (Lin { the non zero Vector of the non trivial torsion-free Z_Module})
for a, b being Element of INT.Ring st v1 = a * the non zero Vector of the non trivial torsion-free Z_Module & v2 = b * the non zero Vector of the non trivial torsion-free Z_Module holds
f . (v1,v2) = a * b
proof
let v1,
v2 be
Vector of
(Lin { the non zero Vector of the non trivial torsion-free Z_Module});
for a, b being Element of INT.Ring st v1 = a * the non zero Vector of the non trivial torsion-free Z_Module & v2 = b * the non zero Vector of the non trivial torsion-free Z_Module holds
f . (v1,v2) = a * blet a,
b be
Element of
INT.Ring;
( v1 = a * the non zero Vector of the non trivial torsion-free Z_Module & v2 = b * the non zero Vector of the non trivial torsion-free Z_Module implies f . (v1,v2) = a * b )
assume B0:
(
v1 = a * the non
zero Vector of the non
trivial torsion-free Z_Module &
v2 = b * the non
zero Vector of the non
trivial torsion-free Z_Module )
;
f . (v1,v2) = a * b
consider a0,
b0 being
Element of
INT.Ring such that B1:
(
[v1,v2] = [(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 . [v1,v2] = 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
;
v1 = a0 * the non
zero Vector of the non
trivial torsion-free Z_Module
by B1, XTUPLE_0:1;
then B3:
a = a0
by B0, B2, ZMODUL01:11;
v2 = b0 * the non
zero Vector of the non
trivial torsion-free Z_Module
by B1, XTUPLE_0:1;
hence
f . (
v1,
v2)
= a * b
by B0, B1, B2, B3, ZMODUL01:11;
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 ;
reconsider L = L as strict Z_Lattice by A3, ThNonTrivialLat1;
take
L
; not L is trivial
not L is trivial
hence
not L is trivial
; verum