let G1, G2 be Group; :: thesis: 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; :: thesis: 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);
:: thesis: (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)
:: thesis: verumproof
A4:
(FuncLatt f) . a = gr (f .: the carrier of A1)
by A2, Def3;
A5:
(FuncLatt f) . b = gr (f .: the carrier of B1)
by A3, Def3;
A6:
(FuncLatt f) . (A1 "\/" B1) = gr (f .: the carrier of (A1 "\/" B1))
by Def3;
A7:
dom f = the
carrier of
G1
by FUNCT_2:def 1;
1_ G1 in A1
by GROUP_2:55;
then A8:
1_ G1 in the
carrier of
A1
by STRUCT_0:def 5;
consider y being
Element of
G2 such that A9:
y = f . (1_ G1)
;
A10:
f .: the
carrier of
A1 <> {}
by A7, A8, A9, FUNCT_1:def 12;
A11:
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 A19:
the
carrier of
A3 = f .: the
carrier of
A1
by A10, A11, GROUP_2:61;
1_ G1 in B1
by GROUP_2:55;
then A20:
1_ G1 in the
carrier of
B1
by STRUCT_0:def 5;
consider y1 being
Element of
G2 such that A21:
y1 = f . (1_ G1)
;
A22:
f .: the
carrier of
B1 <> {}
by A7, A20, A21, FUNCT_1:def 12;
A23:
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 A31:
the
carrier of
B3 = f .: the
carrier of
B1
by A22, A23, GROUP_2:61;
A32:
gr (f .: the carrier of B1) = B3
by A31, Th3;
consider C1 being
strict Subgroup of
G1 such that A33:
C1 = A1 "\/" B1
;
1_ G1 in C1
by GROUP_2:55;
then A34:
1_ G1 in the
carrier of
C1
by STRUCT_0:def 5;
consider y being
Element of
G2 such that A35:
y = f . (1_ G1)
;
A36:
f .: the
carrier of
C1 <> {}
by A7, A34, A35, FUNCT_1:def 12;
A37:
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 A45:
the
carrier of
C3 = f .: the
carrier of
C1
by A36, A37, GROUP_2:61;
( 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;
reconsider B =
(f .: the carrier of A1) \/ (f .: the carrier of B1) as
Subset of
G2 ;
the
carrier of
(A3 "\/" B3) = the
carrier of
C3
proof
A46:
f .: the
carrier of
A1 c= the
carrier of
C3
f .: the
carrier of
B1 c= the
carrier of
C3
then
B c= the
carrier of
C3
by A46, XBOOLE_1:8;
then
gr B is
Subgroup of
C3
by GROUP_4:def 5;
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 A19, A31, Th4;
:: according to XBOOLE_0:def 10 :: thesis: the carrier of C3 c= the carrier of (A3 "\/" B3)
the
carrier of
A1 c= the
carrier of
G1
by GROUP_2:def 5;
then A51:
the
carrier of
A1 c= f " the
carrier of
A3
by A19, FUNCT_2:50;
the
carrier of
B1 c= the
carrier of
G1
by GROUP_2:def 5;
then A52:
the
carrier of
B1 c= f " the
carrier of
B3
by A31, FUNCT_2:50;
A53:
f " the
carrier of
A3 c= f " the
carrier of
(A3 "\/" B3)
f " the
carrier of
B3 c= f " the
carrier of
(A3 "\/" B3)
then A58:
(f " the carrier of A3) \/ (f " the carrier of B3) c= f " the
carrier of
(A3 "\/" B3)
by A53, XBOOLE_1:8;
reconsider AA =
(f " the carrier of A3) \/ (f " the carrier of B3) as
Subset of
G1 ;
A59:
A c= AA
by A51, A52, XBOOLE_1:13;
1_ G2 in A3 "\/" B3
by GROUP_2:55;
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:40;
then A60:
f " the
carrier of
(A3 "\/" B3) <> {}
by FUNCT_2:46;
A61:
for
g being
Element of
G1 st
g in f " the
carrier of
(A3 "\/" B3) holds
g " in f " the
carrier of
(A3 "\/" B3)
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)
then consider H being
strict Subgroup of
G1 such that A62:
the
carrier of
H = f " the
carrier of
(A3 "\/" B3)
by A60, A61, GROUP_2:61;
A c= the
carrier of
H
by A58, A59, A62, XBOOLE_1:1;
then
gr A is
Subgroup of
H
by GROUP_4:def 5;
then
the
carrier of
(gr A) c= the
carrier of
H
by GROUP_2:def 5;
then A63:
the
carrier of
C1 c= f " the
carrier of
(A3 "\/" B3)
by A33, A62, Th4;
A64:
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:145;
hence
the
carrier of
C3 c= the
carrier of
(A3 "\/" B3)
by A45, A64, XBOOLE_1:1;
:: thesis: verum
end;
then gr (f .: the carrier of (A1 "\/" B1)) =
A3 "\/" B3
by A33, A45, Th3
.=
(gr (f .: the carrier of A1)) "\/" (gr (f .: the carrier of B1))
by A19, A32, Th3
.=
((FuncLatt f) . a) "\/" ((FuncLatt f) . b)
by A4, A5, Th27
;
hence
(FuncLatt f) . (a "\/" b) = ((FuncLatt f) . a) "\/" ((FuncLatt f) . b)
by A2, A3, A6, Th27;
:: thesis: verum
end;
end;
hence
FuncLatt f is sup-Semilattice-Homomorphism of lattice G1, lattice G2
by VECTSP_8:def 9; :: thesis: verum