let V be free finite-rank Z_Module; for f being Function of [: the carrier of ((0). V), the carrier of ((0). V):], the carrier of F_Real st f = [: the carrier of ((0). V), the carrier of ((0). V):] --> (0. F_Real) holds
GenLat (((0). V),f) is Z_Lattice-like
let f be Function of [: the carrier of ((0). V), the carrier of ((0). V):], the carrier of F_Real; ( f = [: the carrier of ((0). V), the carrier of ((0). V):] --> (0. F_Real) implies GenLat (((0). V),f) is Z_Lattice-like )
assume P1:
f = [: the carrier of ((0). V), the carrier of ((0). V):] --> (0. F_Real)
; GenLat (((0). V),f) is Z_Lattice-like
set X = GenLat (((0). V),f);
reconsider X = GenLat (((0). V),f) as non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed LatticeStr over INT.Ring ;
reconsider X = X as non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed free LatticeStr over INT.Ring ;
reconsider X = X 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 ;
P2:
for x being Vector of X st ( for y being Vector of X holds <;x,y;> = 0 ) holds
x = 0. X
for x, y, z being Vector of X
for a being Element of INT.Ring holds
( <;x,y;> = <;y,x;> & <;(x + y),z;> = <;x,z;> + <;y,z;> & <;(a * x),y;> = a * <;x,y;> )
proof
let x,
y,
z be
Vector of
X;
for a being Element of INT.Ring holds
( <;x,y;> = <;y,x;> & <;(x + y),z;> = <;x,z;> + <;y,z;> & <;(a * x),y;> = a * <;x,y;> )let a be
Element of
INT.Ring;
( <;x,y;> = <;y,x;> & <;(x + y),z;> = <;x,z;> + <;y,z;> & <;(a * x),y;> = a * <;x,y;> )
A1:
the
carrier of
((0). V) = {(0. V)}
by VECTSP_4:def 3;
then A3:
0. V in the
carrier of
((0). V)
by TARSKI:def 1;
thus
<;x,y;> = <;y,x;>
( <;(x + y),z;> = <;x,z;> + <;y,z;> & <;(a * x),y;> = a * <;x,y;> )
A4:
f . [(0. V),(0. V)] = 0
by A3, P1, FUNCOP_1:7, ZFMISC_1:87;
thus
<;(x + y),z;> = <;x,z;> + <;y,z;>
<;(a * x),y;> = a * <;x,y;>proof
reconsider u =
x,
v =
y,
w =
z as
Vector of
((0). V) ;
B2:
w = 0. V
by A1, TARSKI:def 1;
(
u = 0. V &
v = 0. V )
by A1, TARSKI:def 1;
hence
<;(x + y),z;> = <;x,z;> + <;y,z;>
by A1, A4, B2, TARSKI:def 1;
verum
end;
thus
<;(a * x),y;> = a * <;x,y;>
verum
end;
hence
GenLat (((0). V),f) is Z_Lattice-like
by P2; verum