let V be free finite-rank Z_Module; :: thesis: 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; :: thesis: ( 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) ; :: thesis: 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
proof
let x be Vector of X; :: thesis: ( ( for y being Vector of X holds <;x,y;> = 0 ) implies x = 0. X )
assume for y being Vector of X holds <;x,y;> = 0 ; :: thesis: x = 0. X
x in the carrier of ((0). V) ;
then x in {(0. V)} by VECTSP_4:def 3;
hence x = 0. V by TARSKI:def 1
.= 0. X by ZMODUL01:26 ;
:: thesis: verum
end;
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; :: thesis: 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; :: thesis: ( <;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;> :: thesis: ( <;(x + y),z;> = <;x,z;> + <;y,z;> & <;(a * x),y;> = a * <;x,y;> )
proof
( x = 0. V & y = 0. V ) by A1, TARSKI:def 1;
hence <;x,y;> = <;y,x;> ; :: thesis: verum
end;
A4: f . [(0. V),(0. V)] = 0 by A3, P1, FUNCOP_1:7, ZFMISC_1:87;
thus <;(x + y),z;> = <;x,z;> + <;y,z;> :: thesis: <;(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; :: thesis: verum
end;
thus <;(a * x),y;> = a * <;x,y;> :: thesis: verum
proof
reconsider u = x, v = y as Vector of ((0). V) ;
( u = 0. V & v = 0. V ) by A1, TARSKI:def 1;
hence <;(a * x),y;> = a * <;x,y;> by A1, A4, TARSKI:def 1; :: thesis: verum
end;
end;
hence GenLat (((0). V),f) is Z_Lattice-like by P2; :: thesis: verum