let L1, L2 be complete Lattice; for f being Function of the carrier of L1, the carrier of L2 st f is one-to-one & rng f = the carrier of L2 & ( for a, b being Element of L1 holds
( a [= b iff f . a [= f . b ) ) holds
f is Homomorphism of L1,L2
let f be Function of the carrier of L1, the carrier of L2; ( f is one-to-one & rng f = the carrier of L2 & ( for a, b being Element of L1 holds
( a [= b iff f . a [= f . b ) ) implies f is Homomorphism of L1,L2 )
assume A1:
( f is one-to-one & rng f = the carrier of L2 )
; ( ex a, b being Element of L1 st
( ( a [= b implies f . a [= f . b ) implies ( f . a [= f . b & not a [= b ) ) or f is Homomorphism of L1,L2 )
assume A2:
for a, b being Element of L1 holds
( a [= b iff f . a [= f . b )
; f is Homomorphism of L1,L2
A3:
for a, b being Element of L1 holds f . (a "/\" b) = (f . a) "/\" (f . b)
proof
let a,
b be
Element of
L1;
f . (a "/\" b) = (f . a) "/\" (f . b)
a "/\" b [= b
by LATTICES:6;
then A4:
f . (a "/\" b) [= f . b
by A2;
A5:
for
r being
Element of
L2 st
r is_less_than {(f . a),(f . b)} holds
r [= f . (a "/\" b)
proof
reconsider g =
f " as
Function of the
carrier of
L2, the
carrier of
L1 by A1, FUNCT_2:25;
let r be
Element of
L2;
( r is_less_than {(f . a),(f . b)} implies r [= f . (a "/\" b) )
assume A6:
r is_less_than {(f . a),(f . b)}
;
r [= f . (a "/\" b)
A7:
f . (g . r) = r
by A1, FUNCT_1:35;
f . b in {(f . a),(f . b)}
by TARSKI:def 2;
then
r [= f . b
by A6;
then A8:
g . r [= b
by A2, A7;
f . a in {(f . a),(f . b)}
by TARSKI:def 2;
then
r [= f . a
by A6;
then
g . r [= a
by A2, A7;
then
for
q being
Element of
L1 st
q in {a,b} holds
g . r [= q
by A8, TARSKI:def 2;
then A9:
g . r is_less_than {a,b}
;
a "/\" b = "/\" {a,b}
by LATTICE3:43;
then
g . r [= a "/\" b
by A9, LATTICE3:34;
hence
r [= f . (a "/\" b)
by A2, A7;
verum
end;
a "/\" b [= a
by LATTICES:6;
then
f . (a "/\" b) [= f . a
by A2;
then
for
q being
Element of
L2 st
q in {(f . a),(f . b)} holds
f . (a "/\" b) [= q
by A4, TARSKI:def 2;
then
f . (a "/\" b) is_less_than {(f . a),(f . b)}
;
then
f . (a "/\" b) = "/\" (
{(f . a),(f . b)},
L2)
by A5, LATTICE3:34;
hence
f . (a "/\" b) = (f . a) "/\" (f . b)
by LATTICE3:43;
verum
end;
for a, b being Element of L1 holds f . (a "\/" b) = (f . a) "\/" (f . b)
proof
let a,
b be
Element of
L1;
f . (a "\/" b) = (f . a) "\/" (f . b)
b [= a "\/" b
by LATTICES:5;
then A10:
f . b [= f . (a "\/" b)
by A2;
A11:
for
r being
Element of
L2 st
{(f . a),(f . b)} is_less_than r holds
f . (a "\/" b) [= r
proof
reconsider g =
f " as
Function of the
carrier of
L2, the
carrier of
L1 by A1, FUNCT_2:25;
let r be
Element of
L2;
( {(f . a),(f . b)} is_less_than r implies f . (a "\/" b) [= r )
assume A12:
{(f . a),(f . b)} is_less_than r
;
f . (a "\/" b) [= r
A13:
f . (g . r) = r
by A1, FUNCT_1:35;
f . b in {(f . a),(f . b)}
by TARSKI:def 2;
then
f . b [= r
by A12;
then A14:
b [= g . r
by A2, A13;
f . a in {(f . a),(f . b)}
by TARSKI:def 2;
then
f . a [= r
by A12;
then
a [= g . r
by A2, A13;
then
for
q being
Element of
L1 st
q in {a,b} holds
q [= g . r
by A14, TARSKI:def 2;
then A15:
{a,b} is_less_than g . r
;
a "\/" b = "\/" {a,b}
by LATTICE3:43;
then
a "\/" b [= g . r
by A15, LATTICE3:def 21;
hence
f . (a "\/" b) [= r
by A2, A13;
verum
end;
a [= a "\/" b
by LATTICES:5;
then
f . a [= f . (a "\/" b)
by A2;
then
for
q being
Element of
L2 st
q in {(f . a),(f . b)} holds
q [= f . (a "\/" b)
by A10, TARSKI:def 2;
then
{(f . a),(f . b)} is_less_than f . (a "\/" b)
;
then
f . (a "\/" b) = "\/" (
{(f . a),(f . b)},
L2)
by A11, LATTICE3:def 21;
hence
f . (a "\/" b) = (f . a) "\/" (f . b)
by LATTICE3:43;
verum
end;
then
( f is "\/"-preserving & f is "/\"-preserving )
by A3, LATTICE4:def 1, LATTICE4:def 2;
hence
f is Homomorphism of L1,L2
; verum