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 )proof
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 .: {z,y} = {(f . z),(f . y)}
by A1, FUNCT_1:118;
A4:
ex_inf_of {z,y},
S
by YELLOW_0:21;
A5:
f preserves_inf_of {z,y}
by A2, WAYBEL_0:def 34;
thus f . (z "/\" y) =
f . (inf {z,y})
by YELLOW_0:40
.=
inf {(f . z),(f . y)}
by A3, A4, A5, WAYBEL_0:def 30
.=
(f . z) "/\" (f . y)
by YELLOW_0:40
;
:: thesis: verum
end;
assume A6:
for x, y being Element of S holds f . (x "/\" y) = (f . x) "/\" (f . y)
; :: thesis: f is meet-preserving
for z, y being Element of S holds f preserves_inf_of {z,y}
proof
let z,
y be
Element of
S;
:: thesis: f preserves_inf_of {z,y}
A7:
f .: {z,y} = {(f . z),(f . y)}
by A1, FUNCT_1:118;
then A8:
(
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 A7, YELLOW_0:40
.=
f . (z "/\" y)
by A6
.=
f . (inf {z,y})
by YELLOW_0:40
;
hence
f preserves_inf_of {z,y}
by A8, WAYBEL_0:def 30;
:: thesis: verum
end;
hence
f is meet-preserving
by WAYBEL_0:def 34; :: thesis: verum