let G1, G2 be Group; for f being Homomorphism of G1,G2 st f is one-to-one holds
FuncLatt f is Semilattice-Homomorphism of (lattice G1),(lattice G2)
let f be Homomorphism of G1,G2; ( f is one-to-one implies FuncLatt f is Semilattice-Homomorphism of (lattice G1),(lattice G2) )
assume A1:
f is one-to-one
; FuncLatt f is Semilattice-Homomorphism of (lattice G1),(lattice G2)
for a, b being Element of (lattice G1) holds (FuncLatt f) . (a "/\" b) = ((FuncLatt f) . a) "/\" ((FuncLatt f) . b)
proof
let a,
b be
Element of
(lattice G1);
(FuncLatt f) . (a "/\" b) = ((FuncLatt f) . a) "/\" ((FuncLatt f) . b)
consider A1 being
strict Subgroup of
G1 such that A2:
A1 = a
by Th2;
consider B1 being
strict Subgroup of
G1 such that A3:
B1 = b
by Th2;
thus
(FuncLatt f) . (a "/\" b) = ((FuncLatt f) . a) "/\" ((FuncLatt f) . b)
verumproof
A4:
for
g1,
g2 being
Element of
G2 st
g1 in f .: the
carrier of
B1 &
g2 in f .: the
carrier of
B1 holds
g1 * g2 in f .: the
carrier of
B1
A13:
for
g being
Element of
G2 st
g in f .: the
carrier of
B1 holds
g " in f .: the
carrier of
B1
A17:
for
g being
Element of
G2 st
g in f .: the
carrier of
A1 holds
g " in f .: the
carrier of
A1
1_ G1 in A1
by GROUP_2:46;
then A21:
1_ G1 in the
carrier of
A1
by STRUCT_0:def 5;
A22:
(FuncLatt f) . (A1 /\ B1) = gr (f .: the carrier of (A1 /\ B1))
by Def3;
consider C1 being
strict Subgroup of
G1 such that A23:
C1 = A1 /\ B1
;
A24:
for
g1,
g2 being
Element of
G2 st
g1 in f .: the
carrier of
A1 &
g2 in f .: the
carrier of
A1 holds
g1 * g2 in f .: the
carrier of
A1
1_ G1 in B1
by GROUP_2:46;
then A33:
1_ G1 in the
carrier of
B1
by STRUCT_0:def 5;
A34:
(
(FuncLatt f) . a = gr (f .: the carrier of A1) &
(FuncLatt f) . b = gr (f .: the carrier of B1) )
by A2, A3, Def3;
A35:
dom f = the
carrier of
G1
by FUNCT_2:def 1;
A36:
for
g1,
g2 being
Element of
G2 st
g1 in f .: the
carrier of
C1 &
g2 in f .: the
carrier of
C1 holds
g1 * g2 in f .: the
carrier of
C1
A45:
for
g being
Element of
G2 st
g in f .: the
carrier of
C1 holds
g " in f .: the
carrier of
C1
1_ G1 in C1
by GROUP_2:46;
then A49:
1_ G1 in the
carrier of
C1
by STRUCT_0:def 5;
ex
y2 being
Element of
G2 st
y2 = f . (1_ G1)
;
then
f .: the
carrier of
C1 <> {}
by A35, A49, FUNCT_1:def 6;
then consider C3 being
strict Subgroup of
G2 such that A50:
the
carrier of
C3 = f .: the
carrier of
C1
by A45, A36, GROUP_2:52;
ex
y1 being
Element of
G2 st
y1 = f . (1_ G1)
;
then
f .: the
carrier of
B1 <> {}
by A35, A33, FUNCT_1:def 6;
then consider B3 being
strict Subgroup of
G2 such that A51:
the
carrier of
B3 = f .: the
carrier of
B1
by A13, A4, GROUP_2:52;
ex
y being
Element of
G2 st
y = f . (1_ G1)
;
then
f .: the
carrier of
A1 <> {}
by A35, A21, FUNCT_1:def 6;
then consider A3 being
strict Subgroup of
G2 such that A52:
the
carrier of
A3 = f .: the
carrier of
A1
by A17, A24, GROUP_2:52;
A53:
the
carrier of
C3 c= the
carrier of
(A3 /\ B3)
A65:
gr (f .: the carrier of B1) = B3
by A51, Th3;
the
carrier of
(A3 /\ B3) c= the
carrier of
C3
then
the
carrier of
(A3 /\ B3) = the
carrier of
C3
by A53;
then gr (f .: the carrier of (A1 /\ B1)) =
A3 /\ B3
by A23, A50, Th3
.=
(gr (f .: the carrier of A1)) /\ (gr (f .: the carrier of B1))
by A52, A65, Th3
.=
((FuncLatt f) . a) "/\" ((FuncLatt f) . b)
by A34, Th23
;
hence
(FuncLatt f) . (a "/\" b) = ((FuncLatt f) . a) "/\" ((FuncLatt f) . b)
by A2, A3, A22, Th23;
verum
end;
end;
hence
FuncLatt f is Semilattice-Homomorphism of (lattice G1),(lattice G2)
by LATTICE4:def 2; verum