let S, T be Semilattice; :: thesis: for f being Function of S,T holds

( f is meet-preserving iff for x, y being Element of S holds f . (x "/\" y) = (f . x) "/\" (f . y) )

let f be Function of S,T; :: thesis: ( f is meet-preserving iff for x, y being Element of S holds f . (x "/\" y) = (f . x) "/\" (f . y) )

A1: dom f = the carrier of S by FUNCT_2:def 1;

thus ( f is meet-preserving implies for x, y being Element of S holds f . (x "/\" y) = (f . x) "/\" (f . y) ) :: thesis: ( ( for x, y being Element of S holds f . (x "/\" y) = (f . x) "/\" (f . y) ) implies f is meet-preserving )

for z, y being Element of S holds f preserves_inf_of {z,y}

( f is meet-preserving iff for x, y being Element of S holds f . (x "/\" y) = (f . x) "/\" (f . y) )

let f be Function of S,T; :: thesis: ( f is meet-preserving iff for x, y being Element of S holds f . (x "/\" y) = (f . x) "/\" (f . y) )

A1: dom f = the carrier of S by FUNCT_2:def 1;

thus ( f is meet-preserving implies for x, y being Element of S holds f . (x "/\" y) = (f . x) "/\" (f . y) ) :: thesis: ( ( for x, y being Element of S holds f . (x "/\" y) = (f . x) "/\" (f . y) ) implies f is meet-preserving )

proof

assume A5:
for x, y being Element of S holds f . (x "/\" y) = (f . x) "/\" (f . y)
; :: thesis: f is meet-preserving
assume A2:
f is meet-preserving
; :: thesis: for x, y being Element of S holds f . (x "/\" y) = (f . x) "/\" (f . y)

let z, y be Element of S; :: thesis: f . (z "/\" y) = (f . z) "/\" (f . y)

A3: f preserves_inf_of {z,y} by A2;

A4: ( f .: {z,y} = {(f . z),(f . y)} & ex_inf_of {z,y},S ) by A1, FUNCT_1:60, YELLOW_0:21;

thus f . (z "/\" y) = f . (inf {z,y}) by YELLOW_0:40

.= inf {(f . z),(f . y)} by A4, A3

.= (f . z) "/\" (f . y) by YELLOW_0:40 ; :: thesis: verum

end;let z, y be Element of S; :: thesis: f . (z "/\" y) = (f . z) "/\" (f . y)

A3: f preserves_inf_of {z,y} by A2;

A4: ( f .: {z,y} = {(f . z),(f . y)} & ex_inf_of {z,y},S ) by A1, FUNCT_1:60, YELLOW_0:21;

thus f . (z "/\" y) = f . (inf {z,y}) by YELLOW_0:40

.= inf {(f . z),(f . y)} by A4, A3

.= (f . z) "/\" (f . y) by YELLOW_0:40 ; :: thesis: verum

for z, y being Element of S holds f preserves_inf_of {z,y}

proof

hence
f is meet-preserving
; :: thesis: verum
let z, y be Element of S; :: thesis: f preserves_inf_of {z,y}

A6: f .: {z,y} = {(f . z),(f . y)} by A1, FUNCT_1:60;

then A7: ( ex_inf_of {z,y},S implies ex_inf_of f .: {z,y},T ) by YELLOW_0:21;

inf (f .: {z,y}) = (f . z) "/\" (f . y) by A6, YELLOW_0:40

.= f . (z "/\" y) by A5

.= f . (inf {z,y}) by YELLOW_0:40 ;

hence f preserves_inf_of {z,y} by A7; :: thesis: verum

end;A6: f .: {z,y} = {(f . z),(f . y)} by A1, FUNCT_1:60;

then A7: ( ex_inf_of {z,y},S implies ex_inf_of f .: {z,y},T ) by YELLOW_0:21;

inf (f .: {z,y}) = (f . z) "/\" (f . y) by A6, YELLOW_0:40

.= f . (z "/\" y) by A5

.= f . (inf {z,y}) by YELLOW_0:40 ;

hence f preserves_inf_of {z,y} by A7; :: thesis: verum