let G1, G2 be Group; :: thesis: 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; :: thesis: ( f is one-to-one implies FuncLatt f is Semilattice-Homomorphism of lattice G1, lattice G2 )
assume A1:
f is one-to-one
; :: thesis: 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);
:: thesis: (FuncLatt f) . (a "/\" b) = ((FuncLatt f) . a) "/\" ((FuncLatt f) . b)
consider A1 being
strict Subgroup of
G1 such that A3:
A1 = a
by Th2;
consider B1 being
strict Subgroup of
G1 such that A4:
B1 = b
by Th2;
thus
(FuncLatt f) . (a "/\" b) = ((FuncLatt f) . a) "/\" ((FuncLatt f) . b)
:: thesis: verumproof
A5:
(FuncLatt f) . a = gr (f .: the carrier of A1)
by A3, Def3;
A6:
(FuncLatt f) . b = gr (f .: the carrier of B1)
by A4, Def3;
A7:
(FuncLatt f) . (A1 /\ B1) = gr (f .: the carrier of (A1 /\ B1))
by Def3;
A8:
dom f = the
carrier of
G1
by FUNCT_2:def 1;
1_ G1 in A1
by GROUP_2:55;
then A9:
1_ G1 in the
carrier of
A1
by STRUCT_0:def 5;
consider y being
Element of
G2 such that A10:
y = f . (1_ G1)
;
A11:
f .: the
carrier of
A1 <> {}
by A8, A9, A10, FUNCT_1:def 12;
A12:
for
g being
Element of
G2 st
g in f .: the
carrier of
A1 holds
g " in f .: the
carrier of
A1
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
then consider A3 being
strict Subgroup of
G2 such that A20:
the
carrier of
A3 = f .: the
carrier of
A1
by A11, A12, GROUP_2:61;
1_ G1 in B1
by GROUP_2:55;
then A21:
1_ G1 in the
carrier of
B1
by STRUCT_0:def 5;
consider y1 being
Element of
G2 such that A22:
y1 = f . (1_ G1)
;
A23:
f .: the
carrier of
B1 <> {}
by A8, A21, A22, FUNCT_1:def 12;
A24:
for
g being
Element of
G2 st
g in f .: the
carrier of
B1 holds
g " in f .: the
carrier of
B1
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
then consider B3 being
strict Subgroup of
G2 such that A32:
the
carrier of
B3 = f .: the
carrier of
B1
by A23, A24, GROUP_2:61;
A33:
gr (f .: the carrier of B1) = B3
by A32, Th3;
consider C1 being
strict Subgroup of
G1 such that A34:
C1 = A1 /\ B1
;
1_ G1 in C1
by GROUP_2:55;
then A35:
1_ G1 in the
carrier of
C1
by STRUCT_0:def 5;
consider y2 being
Element of
G2 such that A36:
y2 = f . (1_ G1)
;
A37:
f .: the
carrier of
C1 <> {}
by A8, A35, A36, FUNCT_1:def 12;
A38:
for
g being
Element of
G2 st
g in f .: the
carrier of
C1 holds
g " in f .: the
carrier of
C1
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
then consider C3 being
strict Subgroup of
G2 such that A46:
the
carrier of
C3 = f .: the
carrier of
C1
by A37, A38, GROUP_2:61;
the
carrier of
(A3 /\ B3) = the
carrier of
C3
then gr (f .: the carrier of (A1 /\ B1)) =
A3 /\ B3
by A34, A46, Th3
.=
(gr (f .: the carrier of A1)) /\ (gr (f .: the carrier of B1))
by A20, A33, Th3
.=
((FuncLatt f) . a) "/\" ((FuncLatt f) . b)
by A5, A6, Th28
;
hence
(FuncLatt f) . (a "/\" b) = ((FuncLatt f) . a) "/\" ((FuncLatt f) . b)
by A3, A4, A7, Th28;
:: thesis: verum
end;
end;
hence
FuncLatt f is Semilattice-Homomorphism of lattice G1, lattice G2
by VECTSP_8:def 8; :: thesis: verum