let G1, G2 be Group; for f being Homomorphism of G1,G2 holds FuncLatt f is sup-Semilattice-Homomorphism of (lattice G1),(lattice G2)
let f be Homomorphism of G1,G2; FuncLatt f is sup-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 A1:
A1 = a
by Th2;
consider B1 being
strict Subgroup of
G1 such that A2:
B1 = b
by Th2;
thus
(FuncLatt f) . (a "\/" b) = ((FuncLatt f) . a) "\/" ((FuncLatt f) . b)
verumproof
A3:
for
g being
Element of
G2 st
g in f .: the
carrier of
B1 holds
g " in f .: the
carrier of
B1
1_ G1 in A1
by GROUP_2:46;
then A7:
1_ G1 in the
carrier of
A1
by STRUCT_0:def 5;
A8:
ex
y being
Element of
G2 st
y = f . (1_ G1)
;
( the
carrier of
A1 c= the
carrier of
G1 & the
carrier of
B1 c= the
carrier of
G1 )
by GROUP_2:def 5;
then reconsider A = the
carrier of
A1 \/ the
carrier of
B1 as
Subset of
G1 by XBOOLE_1:8;
A9:
for
g being
Element of
G2 st
g in f .: the
carrier of
A1 holds
g " in f .: the
carrier of
A1
reconsider B =
(f .: the carrier of A1) \/ (f .: the carrier of B1) as
Subset of
G2 ;
A13:
dom f = the
carrier of
G1
by FUNCT_2:def 1;
A14:
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
1_ G1 in B1
by GROUP_2:46;
then A23:
1_ G1 in the
carrier of
B1
by STRUCT_0:def 5;
A24:
(FuncLatt f) . (A1 "\/" B1) = gr (f .: the carrier of (A1 "\/" B1))
by Def3;
ex
y1 being
Element of
G2 st
y1 = f . (1_ G1)
;
then
f .: the
carrier of
B1 <> {}
by A13, A23, FUNCT_1:def 6;
then consider B3 being
strict Subgroup of
G2 such that A25:
the
carrier of
B3 = f .: the
carrier of
B1
by A3, A14, GROUP_2:52;
A26:
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
A35:
(
(FuncLatt f) . a = gr (f .: the carrier of A1) &
(FuncLatt f) . b = gr (f .: the carrier of B1) )
by A1, A2, Def3;
consider C1 being
strict Subgroup of
G1 such that A36:
C1 = A1 "\/" B1
;
A37:
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
A46:
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
1_ G1 in the
carrier of
C1
by STRUCT_0:def 5;
then
f .: the
carrier of
C1 <> {}
by A13, A8, 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 A46, A37, GROUP_2:52;
ex
y being
Element of
G2 st
y = f . (1_ G1)
;
then
f .: the
carrier of
A1 <> {}
by A13, A7, FUNCT_1:def 6;
then consider A3 being
strict Subgroup of
G2 such that A51:
the
carrier of
A3 = f .: the
carrier of
A1
by A9, A26, GROUP_2:52;
A52:
gr (f .: the carrier of B1) = B3
by A25, Th3;
the
carrier of
(A3 "\/" B3) = the
carrier of
C3
proof
A53:
f .: the
carrier of
B1 c= the
carrier of
C3
f .: the
carrier of
A1 c= the
carrier of
C3
then
B c= the
carrier of
C3
by A53, XBOOLE_1:8;
then
gr B is
Subgroup of
C3
by GROUP_4:def 4;
then
the
carrier of
(gr B) c= the
carrier of
C3
by GROUP_2:def 5;
hence
the
carrier of
(A3 "\/" B3) c= the
carrier of
C3
by A51, A25, Th4;
XBOOLE_0:def 10 the carrier of C3 c= the carrier of (A3 "\/" B3)
reconsider AA =
(f " the carrier of A3) \/ (f " the carrier of B3) as
Subset of
G1 ;
A60:
for
g being
Element of
G1 st
g in f " the
carrier of
(A3 "\/" B3) holds
g " in f " the
carrier of
(A3 "\/" B3)
the
carrier of
B1 c= the
carrier of
G1
by GROUP_2:def 5;
then A61:
the
carrier of
B1 c= f " the
carrier of
B3
by A25, FUNCT_2:42;
the
carrier of
A1 c= the
carrier of
G1
by GROUP_2:def 5;
then
the
carrier of
A1 c= f " the
carrier of
A3
by A51, FUNCT_2:42;
then A62:
A c= AA
by A61, XBOOLE_1:13;
A63:
for
g1,
g2 being
Element of
G1 st
g1 in f " the
carrier of
(A3 "\/" B3) &
g2 in f " the
carrier of
(A3 "\/" B3) holds
g1 * g2 in f " the
carrier of
(A3 "\/" B3)
A67:
f " the
carrier of
B3 c= f " the
carrier of
(A3 "\/" B3)
1_ G2 in A3 "\/" B3
by GROUP_2:46;
then
1_ G2 in the
carrier of
(A3 "\/" B3)
by STRUCT_0:def 5;
then
f . (1_ G1) in the
carrier of
(A3 "\/" B3)
by GROUP_6:31;
then
f " the
carrier of
(A3 "\/" B3) <> {}
by FUNCT_2:38;
then consider H being
strict Subgroup of
G1 such that A70:
the
carrier of
H = f " the
carrier of
(A3 "\/" B3)
by A60, A63, GROUP_2:52;
f " the
carrier of
A3 c= f " the
carrier of
(A3 "\/" B3)
then
(f " the carrier of A3) \/ (f " the carrier of B3) c= f " the
carrier of
(A3 "\/" B3)
by A67, XBOOLE_1:8;
then
A c= the
carrier of
H
by A62, A70;
then
gr A is
Subgroup of
H
by GROUP_4:def 4;
then
the
carrier of
(gr A) c= the
carrier of
H
by GROUP_2:def 5;
then A73:
the
carrier of
C1 c= f " the
carrier of
(A3 "\/" B3)
by A36, A70, Th4;
A74:
f .: the
carrier of
C1 c= f .: (f " the carrier of (A3 "\/" B3))
f .: (f " the carrier of (A3 "\/" B3)) c= the
carrier of
(A3 "\/" B3)
by FUNCT_1:75;
hence
the
carrier of
C3 c= the
carrier of
(A3 "\/" B3)
by A50, A74;
verum
end;
then gr (f .: the carrier of (A1 "\/" B1)) =
A3 "\/" B3
by A36, A50, Th3
.=
(gr (f .: the carrier of A1)) "\/" (gr (f .: the carrier of B1))
by A51, A52, Th3
.=
((FuncLatt f) . a) "\/" ((FuncLatt f) . b)
by A35, Th22
;
hence
(FuncLatt f) . (a "\/" b) = ((FuncLatt f) . a) "\/" ((FuncLatt f) . b)
by A1, A2, A24, Th22;
verum
end;
end;
hence
FuncLatt f is sup-Semilattice-Homomorphism of (lattice G1),(lattice G2)
by LATTICE4:def 1; verum