:: On the Lattice of Subgroups of a Group
:: by Janusz Ganczarski
::
:: Received May 23, 1995
:: Copyright (c) 1995-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies GROUP_1, GROUP_2, STRUCT_0, XBOOLE_0, GROUP_3, SUBSET_1, GROUP_4,
EQREL_1, TARSKI, GROUP_6, RELAT_1, FUNCT_1, ZFMISC_1, SETFAM_1, RLSUB_2,
LATTICES, PBOOLE, REWRITE1, LATTICE3, VECTSP_8;
notations TARSKI, XBOOLE_0, SUBSET_1, FUNCT_1, SETFAM_1, RELAT_1, RELSET_1,
PARTFUN1, FUNCT_2, BINOP_1, STRUCT_0, ALGSTR_0, LATTICES, GROUP_1,
GROUP_2, GROUP_3, GROUP_4, GROUP_6, LATTICE3, LATTICE4, VECTSP_8;
constructors BINOP_1, REALSET1, GROUP_4, GROUP_6, LATTICE3, LATTICE4,
VECTSP_8, RELSET_1;
registrations SUBSET_1, FUNCT_1, FUNCT_2, STRUCT_0, LATTICES, GROUP_3,
GROUP_4, RELSET_1;
requirements BOOLE, SUBSET;
definitions TARSKI, LATTICE3, VECTSP_8, XBOOLE_0;
equalities XBOOLE_0, RELAT_1, GROUP_4;
expansions TARSKI, LATTICE3, XBOOLE_0;
theorems TARSKI, FUNCT_1, SUBSET_1, SETFAM_1, FUNCT_2, LATTICES, GROUP_2,
GROUP_3, GROUP_4, GROUP_6, VECTSP_8, RELAT_1, XBOOLE_0, XBOOLE_1,
STRUCT_0, LATTICE4;
schemes FUNCT_2;
begin
theorem Th1:
for G being Group for H1, H2 being Subgroup of G holds the
carrier of H1 /\ H2 = (the carrier of H1) /\ the carrier of H2
proof
let G be Group;
let H1, H2 be Subgroup of G;
the carrier of H2 = carr H2 by GROUP_2:def 9;
then (the carrier of H1) /\ the carrier of H2 = carr H1 /\ carr H2 by
GROUP_2:def 9;
hence thesis by GROUP_2:def 10;
end;
theorem Th2:
for G being Group for h being set holds h in Subgroups G iff ex H
being strict Subgroup of G st h = H
proof
let G be Group;
let h be set;
thus h in Subgroups G implies ex H being strict Subgroup of G st h = H
proof
assume h in Subgroups G;
then h is strict Subgroup of G by GROUP_3:def 1;
hence thesis;
end;
thus thesis by GROUP_3:def 1;
end;
theorem Th3:
for G being Group for A being Subset of G for H being strict
Subgroup of G st A = the carrier of H holds gr A = H
proof
let G be Group;
let A be Subset of G;
let H be strict Subgroup of G such that
A1: A = the carrier of H;
gr carr H = H by GROUP_4:31;
hence thesis by A1,GROUP_2:def 9;
end;
theorem Th4:
for G being Group for H1, H2 being Subgroup of G for A being
Subset of G st A = (the carrier of H1) \/ the carrier of H2 holds H1 "\/" H2 =
gr A
proof
let G be Group;
let H1, H2 be Subgroup of G;
A1: the carrier of H2 = carr H2 by GROUP_2:def 9;
let A be Subset of G;
assume A = (the carrier of H1) \/ the carrier of H2;
hence thesis by A1,GROUP_2:def 9;
end;
theorem Th5:
for G being Group for H1, H2 being Subgroup of G for g being
Element of G holds g in H1 or g in H2 implies g in H1 "\/" H2
proof
let G be Group;
let H1, H2 be Subgroup of G;
let g be Element of G;
assume
A1: g in H1 or g in H2;
now
per cases by A1;
suppose
A2: g in H1;
the carrier of H1 c= the carrier of G & the carrier of H2 c= the
carrier of G by GROUP_2:def 5;
then reconsider
A = (the carrier of H1) \/ the carrier of H2 as Subset of G
by XBOOLE_1:8;
g in the carrier of H1 by A2,STRUCT_0:def 5;
then g in A by XBOOLE_0:def 3;
then g in gr A by GROUP_4:29;
hence thesis by Th4;
end;
suppose
A3: g in H2;
the carrier of H1 c= the carrier of G & the carrier of H2 c= the
carrier of G by GROUP_2:def 5;
then reconsider
A = (the carrier of H1) \/ the carrier of H2 as Subset of G
by XBOOLE_1:8;
g in the carrier of H2 by A3,STRUCT_0:def 5;
then g in A by XBOOLE_0:def 3;
then g in gr A by GROUP_4:29;
hence thesis by Th4;
end;
end;
hence thesis;
end;
theorem
for G1, G2 being Group for f being Homomorphism of G1, G2 for H1 being
Subgroup of G1 holds ex H2 being strict Subgroup of G2 st the carrier of H2 = f
.:the carrier of H1
proof
let G1, G2 be Group;
let f be Homomorphism of G1, G2;
let H1 be Subgroup of G1;
reconsider y = f.1_G1 as Element of G2;
A1: for g being Element of G2 st g in f.:the carrier of H1 holds g" in f.:
the carrier of H1
proof
let g be Element of G2;
assume g in f.:the carrier of H1;
then consider x being Element of G1 such that
A2: x in the carrier of H1 and
A3: g = f.x by FUNCT_2:65;
x in H1 by A2,STRUCT_0:def 5;
then x" in H1 by GROUP_2:51;
then
A4: x" in the carrier of H1 by STRUCT_0:def 5;
f.x" = (f.x)" by GROUP_6:32;
hence thesis by A3,A4,FUNCT_2:35;
end;
A5: for g1, g2 being Element of G2 st g1 in f.:the carrier of H1 & g2 in f
.:the carrier of H1 holds g1 * g2 in f.:the carrier of H1
proof
let g1, g2 be Element of G2;
assume that
A6: g1 in f.:the carrier of H1 and
A7: g2 in f.:the carrier of H1;
consider x being Element of G1 such that
A8: x in the carrier of H1 and
A9: g1 = f.x by A6,FUNCT_2:65;
consider y being Element of G1 such that
A10: y in the carrier of H1 and
A11: g2 = f.y by A7,FUNCT_2:65;
A12: y in H1 by A10,STRUCT_0:def 5;
x in H1 by A8,STRUCT_0:def 5;
then x * y in H1 by A12,GROUP_2:50;
then
A13: x * y in the carrier of H1 by STRUCT_0:def 5;
f.(x * y) = f.x * f.y by GROUP_6:def 6;
hence thesis by A9,A11,A13,FUNCT_2:35;
end;
1_G1 in H1 by GROUP_2:46;
then dom f = the carrier of G1 & 1_G1 in the carrier of H1 by FUNCT_2:def 1
,STRUCT_0:def 5;
then y in f.:the carrier of H1 by FUNCT_1:def 6;
then consider H2 being strict Subgroup of G2 such that
A14: the carrier of H2 = f.:the carrier of H1 by A1,A5,GROUP_2:52;
take H2;
thus thesis by A14;
end;
theorem
for G1, G2 being Group for f being Homomorphism of G1, G2 for H2 being
Subgroup of G2 ex H1 being strict Subgroup of G1 st the carrier of H1 = f"the
carrier of H2
proof
let G1, G2 be Group;
let f be Homomorphism of G1, G2;
let H2 be Subgroup of G2;
A1: for g being Element of G1 st g in f"the carrier of H2 holds g" in f"the
carrier of H2
proof
let g be Element of G1;
assume g in f"the carrier of H2;
then f.g in the carrier of H2 by FUNCT_2:38;
then f.g in H2 by STRUCT_0:def 5;
then (f.g)" in H2 by GROUP_2:51;
then f.g" in H2 by GROUP_6:32;
then f.g" in the carrier of H2 by STRUCT_0:def 5;
hence thesis by FUNCT_2:38;
end;
A2: for g1, g2 being Element of G1 st g1 in f"the carrier of H2 & g2 in f"
the carrier of H2 holds g1 * g2 in f"the carrier of H2
proof
let g1, g2 be Element of G1;
assume that
A3: g1 in f"the carrier of H2 and
A4: g2 in f"the carrier of H2;
f.g2 in the carrier of H2 by A4,FUNCT_2:38;
then
A5: f.g2 in H2 by STRUCT_0:def 5;
f.g1 in the carrier of H2 by A3,FUNCT_2:38;
then f.g1 in H2 by STRUCT_0:def 5;
then f.g1 * f.g2 in H2 by A5,GROUP_2:50;
then f.(g1 * g2) in H2 by GROUP_6:def 6;
then f.(g1 * g2) in the carrier of H2 by STRUCT_0:def 5;
hence thesis by FUNCT_2:38;
end;
1_G2 in H2 by GROUP_2:46;
then 1_G2 in the carrier of H2 by STRUCT_0:def 5;
then f.1_G1 in the carrier of H2 by GROUP_6:31;
then f"the carrier of H2 <> {} by FUNCT_2:38;
then consider H1 being strict Subgroup of G1 such that
A6: the carrier of H1 = f"the carrier of H2 by A1,A2,GROUP_2:52;
take H1;
thus thesis by A6;
end;
theorem
for G1, G2 being Group for f being Homomorphism of G1, G2 for H1, H2
being Subgroup of G1 for H3, H4 being Subgroup of G2 st the carrier of H3 = f.:
the carrier of H1 & the carrier of H4 = f.:the carrier of H2 holds H1 is
Subgroup of H2 implies H3 is Subgroup of H4
proof
let G1, G2 be Group;
let f be Homomorphism of G1, G2;
let H1, H2 be Subgroup of G1;
let H3, H4 be Subgroup of G2 such that
A1: the carrier of H3 = f.:the carrier of H1 & the carrier of H4 = f.:
the carrier of H2;
assume H1 is Subgroup of H2;
then the carrier of H1 c= the carrier of H2 by GROUP_2:def 5;
hence thesis by A1,GROUP_2:57,RELAT_1:123;
end;
theorem
for G1, G2 being Group for f being Homomorphism of G1, G2 for H1, H2
being Subgroup of G2 for H3, H4 being Subgroup of G1 st the carrier of H3 = f"
the carrier of H1 & the carrier of H4 = f"the carrier of H2 holds H1 is
Subgroup of H2 implies H3 is Subgroup of H4
proof
let G1, G2 be Group;
let f be Homomorphism of G1, G2;
let H1, H2 be Subgroup of G2;
let H3, H4 be Subgroup of G1 such that
A1: the carrier of H3 = f"the carrier of H1 & the carrier of H4 = f"the
carrier of H2;
assume H1 is Subgroup of H2;
then the carrier of H1 c= the carrier of H2 by GROUP_2:def 5;
hence thesis by A1,GROUP_2:57,RELAT_1:143;
end;
theorem
for G1, G2 being Group for f being Function of the carrier of G1, the
carrier of G2 for A being Subset of G1 holds f.:A c= f.:the carrier of gr A
proof
let G1, G2 be Group;
let f be Function of the carrier of G1, the carrier of G2;
let A be Subset of G1;
A c= the carrier of gr A by GROUP_4:def 4;
hence thesis by RELAT_1:123;
end;
theorem
for G1, G2 being Group for H1, H2 being Subgroup of G1 for f being
Function of the carrier of G1, the carrier of G2 for A being Subset of G1 st A
= (the carrier of H1) \/ the carrier of H2 holds f.:the carrier of H1 "\/" H2 =
f.:the carrier of gr A by Th4;
theorem Th12:
for G being Group for A being Subset of G st A = {1_G} holds gr A = (1).G
proof
let G be Group;
let A be Subset of G;
assume A = {1_G};
then A = the carrier of (1).G by GROUP_2:def 7;
hence thesis by Th3;
end;
definition
let G be Group;
func carr G -> Function of Subgroups G, bool the carrier of G means
:Def1:
for H being strict Subgroup of G holds it.H = the carrier of H;
existence
proof
defpred P [object, object] means
for h being strict Subgroup of G st h = $1
holds $2 = the carrier of h;
A1: for e being object st e in Subgroups G
ex u being object st u in bool the carrier of G & P [e,u]
proof
let e be object;
assume e in Subgroups G;
then reconsider E = e as strict Subgroup of G by GROUP_3:def 1;
reconsider u = carr E as Subset of G;
take u;
thus thesis by GROUP_2:def 9;
end;
consider f being Function of Subgroups G, bool the carrier of G such that
A2: for e being object st e in Subgroups G holds P [e,f.e] from FUNCT_2:
sch 1 (A1);
take f;
let H be strict Subgroup of G;
H in Subgroups G by GROUP_3:def 1;
hence thesis by A2;
end;
uniqueness
proof
let F1, F2 be Function of Subgroups G, bool the carrier of G such that
A3: for H1 being strict Subgroup of G holds F1.H1 = the carrier of H1 and
A4: for H2 being strict Subgroup of G holds F2.H2 = the carrier of H2;
for h being object st h in Subgroups G holds F1.h = F2.h
proof
let h be object;
assume h in Subgroups G;
then reconsider H = h as strict Subgroup of G by GROUP_3:def 1;
thus F1.h = the carrier of H by A3
.= F2.h by A4;
end;
hence thesis by FUNCT_2:12;
end;
end;
theorem Th13:
for G being Group for H being strict Subgroup of G for x being
Element of G holds x in carr G.H iff x in H
proof
let G be Group;
let H be strict Subgroup of G;
let x be Element of G;
thus x in carr G.H implies x in H
proof
assume x in carr G.H;
then x in the carrier of H by Def1;
hence thesis by STRUCT_0:def 5;
end;
assume
A1: x in H;
carr G.H = the carrier of H by Def1;
hence thesis by A1,STRUCT_0:def 5;
end;
theorem
for G being Group for H being strict Subgroup of G holds 1_G in carr G .H
proof
let G be Group;
let H be strict Subgroup of G;
carr G.H = the carrier of H & 1_H = 1_G by Def1,GROUP_2:44;
hence thesis;
end;
theorem
for G being Group for H being strict Subgroup of G holds carr G.H <>
{} by Def1;
theorem
for G being Group for H being strict Subgroup of G for g1, g2 being
Element of G holds g1 in carr G.H & g2 in carr G.H implies g1 * g2 in carr G.H
proof
let G be Group;
let H be strict Subgroup of G;
let g1, g2 be Element of G;
assume g1 in carr G.H & g2 in carr G.H;
then g1 in H & g2 in H by Th13;
then g1 * g2 in H by GROUP_2:50;
hence thesis by Th13;
end;
theorem
for G being Group for H being strict Subgroup of G for g being Element
of G holds g in carr G.H implies g" in carr G.H
proof
let G be Group;
let H be strict Subgroup of G;
let g be Element of G;
assume g in carr G.H;
then g in H by Th13;
then g" in H by GROUP_2:51;
hence thesis by Th13;
end;
theorem Th18:
for G being Group for H1, H2 being strict Subgroup of G holds
the carrier of H1 /\ H2 = carr G.H1 /\ carr G.H2
proof
let G be Group;
let H1, H2 be strict Subgroup of G;
carr G.H1 = the carrier of H1 & carr G.H2 = the carrier of H2 by Def1;
hence thesis by Th1;
end;
theorem
for G being Group for H1, H2 being strict Subgroup of G holds carr G.(
H1 /\ H2) = carr G.H1 /\ carr G.H2
proof
let G be Group;
let H1, H2 be strict Subgroup of G;
carr G.H1 /\ carr G.H2 = the carrier of H1 /\ H2 by Th18;
hence thesis by Def1;
end;
definition
let G be Group;
let F be non empty Subset of Subgroups G;
func meet F -> strict Subgroup of G means
:Def2:
the carrier of it = meet ( carr G.:F);
existence
proof
reconsider CG = carr G.:F as Subset-Family of G;
A1: carr G.:F <> {}
proof
consider x being Element of Subgroups G such that
A2: x in F by SUBSET_1:4;
carr G.x in carr G.:F by A2,FUNCT_2:35;
hence thesis;
end;
A3: for g being Element of G st g in meet CG holds g" in meet CG
proof
let g be Element of G such that
A4: g in meet CG;
for X being set st X in carr G.:F holds g" in X
proof
reconsider h = g as Element of G;
let X be set;
assume
A5: X in carr G.:F;
then
A6: g in X by A4,SETFAM_1:def 1;
reconsider X as Subset of G by A5;
consider X1 being Element of Subgroups G such that
X1 in F and
A7: X = carr G.X1 by A5,FUNCT_2:65;
reconsider X1 as strict Subgroup of G by GROUP_3:def 1;
A8: X = the carrier of X1 by A7,Def1;
then h in X1 by A6,STRUCT_0:def 5;
then h" in X1 by GROUP_2:51;
hence thesis by A8,STRUCT_0:def 5;
end;
hence thesis by A1,SETFAM_1:def 1;
end;
A9: for g1, g2 being Element of G st g1 in meet (carr G.:F) & g2 in meet
(carr G.:F) holds g1 * g2 in meet (carr G.:F)
proof
let g1, g2 be Element of G such that
A10: g1 in meet (carr G.:F) and
A11: g2 in meet (carr G.:F);
for X being set st X in carr G.:F holds g1 * g2 in X
proof
reconsider h1 = g1, h2 = g2 as Element of G;
let X be set;
assume
A12: X in carr G.:F;
then
A13: g1 in X by A10,SETFAM_1:def 1;
A14: g2 in X by A11,A12,SETFAM_1:def 1;
reconsider X as Subset of G by A12;
consider X1 being Element of Subgroups G such that
X1 in F and
A15: X = carr G.X1 by A12,FUNCT_2:65;
reconsider X1 as strict Subgroup of G by GROUP_3:def 1;
A16: X = the carrier of X1 by A15,Def1;
then
A17: h2 in X1 by A14,STRUCT_0:def 5;
h1 in X1 by A13,A16,STRUCT_0:def 5;
then h1 * h2 in X1 by A17,GROUP_2:50;
hence thesis by A16,STRUCT_0:def 5;
end;
hence thesis by A1,SETFAM_1:def 1;
end;
for X being set st X in carr G.:F holds 1_G in X
proof
let X be set;
assume
A18: X in carr G.:F;
then reconsider X as Subset of G;
consider X1 being Element of Subgroups G such that
X1 in F and
A19: X = carr G.X1 by A18,FUNCT_2:65;
reconsider X1 as strict Subgroup of G by GROUP_3:def 1;
A20: 1_G in X1 by GROUP_2:46;
X = the carrier of X1 by A19,Def1;
hence thesis by A20,STRUCT_0:def 5;
end;
then meet (carr G.:F) <> {} by A1,SETFAM_1:def 1;
hence thesis by A9,A3,GROUP_2:52;
end;
uniqueness by GROUP_2:59;
end;
theorem
for G being Group for F being non empty Subset of Subgroups G holds
(1).G in F implies meet F = (1).G
proof
let G be Group;
let F be non empty Subset of Subgroups G;
assume
A1: (1).G in F;
reconsider 1G = (1).G as Element of Subgroups G by GROUP_3:def 1;
carr G.1G = the carrier of (1).G by Def1;
then the carrier of (1).G in carr G.:F by A1,FUNCT_2:35;
then {1_G} in carr G.:F by GROUP_2:def 7;
then meet (carr G.:F) c= {1_G} by SETFAM_1:3;
then
A2: the carrier of meet F c= {1_G} by Def2;
(1).G is Subgroup of meet F by GROUP_2:65;
then the carrier of (1).G c= the carrier of meet F by GROUP_2:def 5;
then {1_G} c= the carrier of meet F by GROUP_2:def 7;
then the carrier of meet F = {1_G} by A2;
hence thesis by GROUP_2:def 7;
end;
theorem
for G being Group for h being Element of Subgroups G for F being non
empty Subset of Subgroups G st F = { h } holds meet F = h
proof
let G be Group;
let h be Element of Subgroups G;
let F be non empty Subset of Subgroups G such that
A1: F = { h };
reconsider H = h as strict Subgroup of G by GROUP_3:def 1;
h in Subgroups G;
then h in dom carr G by FUNCT_2:def 1;
then meet Im(carr G,h) = meet {carr G.h} by FUNCT_1:59;
then
A2: meet Im(carr G,h) = carr G.h by SETFAM_1:10;
the carrier of meet F = meet (carr G.:F) by Def2;
then the carrier of meet F = the carrier of H by A1,A2,Def1;
hence thesis by GROUP_2:59;
end;
theorem Th22:
for G being Group for H1, H2 being Subgroup of G for h1, h2
being Element of lattice G st h1 = H1 & h2 = H2 holds h1 "\/" h2 = H1 "\/" H2
proof
let G be Group;
let H1, H2 be Subgroup of G;
let h1, h2 be Element of lattice G;
A1: h1 "\/" h2 = SubJoin G.(h1,h2) by LATTICES:def 1;
assume
A2: h1 = H1 & h2 = H2;
then H1 is strict & H2 is strict by GROUP_3:def 1;
hence thesis by A2,A1,GROUP_4:def 10;
end;
theorem Th23:
for G being Group for H1, H2 being Subgroup of G for h1, h2
being Element of lattice G st h1 = H1 & h2 = H2 holds h1 "/\" h2 = H1 /\ H2
proof
let G be Group;
let H1, H2 be Subgroup of G;
let h1, h2 be Element of lattice G;
A1: h1 "/\" h2 = SubMeet G.(h1,h2) by LATTICES:def 2;
assume
A2: h1 = H1 & h2 = H2;
then H1 is strict & H2 is strict by GROUP_3:def 1;
hence thesis by A2,A1,GROUP_4:def 11;
end;
theorem
for G being Group for p being Element of lattice G for H being
Subgroup of G st p = H holds H is strict Subgroup of G by GROUP_3:def 1;
theorem Th25:
for G being Group for H1, H2 being Subgroup of G for p, q being
Element of lattice G st p = H1 & q = H2 holds p [= q iff the carrier of H1 c=
the carrier of H2
proof
let G be Group;
let H1, H2 be Subgroup of G;
let p, q be Element of lattice G such that
A1: p = H1 and
A2: q = H2;
A3: H1 is strict Subgroup of G by A1,GROUP_3:def 1;
A4: H2 is strict Subgroup of G by A2,GROUP_3:def 1;
thus p [= q implies the carrier of H1 c= the carrier of H2
proof
assume p [= q;
then
A5: p "/\" q = p by LATTICES:4;
p "/\" q = (the L_meet of lattice G).(p,q) by LATTICES:def 2
.= H1 /\ H2 by A1,A2,A3,A4,GROUP_4:def 11;
then
(the carrier of H1) /\ the carrier of H2 = the carrier of H1 by A1,A5,Th1;
hence thesis by XBOOLE_1:17;
end;
thus the carrier of H1 c= the carrier of H2 implies p [= q
proof
assume the carrier of H1 c= the carrier of H2;
then H1 is Subgroup of H2 by GROUP_2:57;
then
A6: H1 /\ H2 = H1 by A3,GROUP_2:89;
H1 /\ H2 = (the L_meet of lattice G).(p,q) by A1,A2,A3,A4,GROUP_4:def 11
.= p "/\" q by LATTICES:def 2;
hence thesis by A1,A6,LATTICES:4;
end;
end;
theorem
for G being Group for H1, H2 being Subgroup of G for p, q being
Element of lattice G st p = H1 & q = H2 holds p [= q iff H1 is Subgroup of H2
proof
let G be Group;
let H1, H2 be Subgroup of G;
let p, q be Element of lattice G;
assume that
A1: p = H1 and
A2: q = H2;
thus p [= q implies H1 is Subgroup of H2
proof
assume p [= q;
then the carrier of H1 c= the carrier of H2 by A1,A2,Th25;
hence thesis by GROUP_2:57;
end;
A3: H1 is strict Subgroup of G by A1,GROUP_3:def 1;
A4: H2 is strict Subgroup of G by A2,GROUP_3:def 1;
thus H1 is Subgroup of H2 implies p [= q
proof
assume H1 is Subgroup of H2;
then
A5: H1 /\ H2 = H1 by A3,GROUP_2:89;
H1 /\ H2 = (the L_meet of lattice G).(p,q) by A1,A2,A3,A4,GROUP_4:def 11
.= p "/\" q by LATTICES:def 2;
hence thesis by A1,A5,LATTICES:4;
end;
end;
theorem
for G being Group holds lattice G is complete
proof
let G be Group;
let Y be Subset of lattice G;
per cases;
suppose
A1: Y = {};
take Top lattice G;
thus Top lattice G is_less_than Y
by A1;
let b be Element of lattice G;
assume b is_less_than Y;
thus thesis by LATTICES:19;
end;
suppose
Y <> {};
then reconsider X = Y as non empty Subset of Subgroups G;
reconsider p = meet X as Element of lattice G by GROUP_3:def 1;
take p;
set x = the Element of X;
thus p is_less_than Y
proof
let q be Element of lattice G;
reconsider H = q as strict Subgroup of G by GROUP_3:def 1;
reconsider h = q as Element of Subgroups G;
assume
A2: q in Y;
carr G.h = the carrier of H by Def1;
then meet (carr G.:X) c= the carrier of H by A2,FUNCT_2:35,SETFAM_1:3;
then the carrier of meet X c= the carrier of H by Def2;
hence thesis by Th25;
end;
let r be Element of lattice G;
reconsider H = r as Subgroup of G by GROUP_3:def 1;
assume
A3: r is_less_than Y;
A4: for Z1 being set st Z1 in carr G.:X holds the carrier of H c= Z1
proof
let Z1 be set;
assume
A5: Z1 in carr G.:X;
then reconsider Z2 = Z1 as Subset of G;
consider z1 being Element of Subgroups G such that
A6: z1 in X & Z2 = carr G.z1 by A5,FUNCT_2:65;
reconsider z1 as Element of lattice G;
reconsider z3 = z1 as strict Subgroup of G by GROUP_3:def 1;
Z1 = the carrier of z3 & r [= z1 by A3,A6,Def1;
hence thesis by Th25;
end;
carr G.x in carr G.:X by FUNCT_2:35;
then the carrier of H c= meet (carr G.:X) by A4,SETFAM_1:5;
then the carrier of H c= the carrier of meet X by Def2;
hence thesis by Th25;
end;
end;
definition
let G1, G2 be Group;
let f be Function of the carrier of G1, the carrier of G2;
func FuncLatt f -> Function of the carrier of lattice G1, the carrier of
lattice G2 means
:Def3:
for H being strict Subgroup of G1, A being Subset of G2
st A = f.:the carrier of H holds it.H = gr A;
existence
proof
defpred P [object, object] means
for H being strict Subgroup of G1 st H = $1 for
A being Subset of G2 st A = f.:the carrier of H holds $2 = gr (f.:the carrier
of H);
A1: for e being object st e in the carrier of lattice G1
ex u being object st u in the carrier of lattice G2 & P [e,u]
proof
let e be object;
assume e in the carrier of lattice G1;
then reconsider E = e as strict Subgroup of G1 by GROUP_3:def 1;
reconsider u = gr (f.:the carrier of E) as strict Subgroup of G2;
reconsider u as Element of lattice G2 by GROUP_3:def 1;
take u;
thus thesis;
end;
consider f1 being Function of the carrier of lattice G1, the carrier of
lattice G2 such that
A2: for e being object st e in the carrier of lattice G1 holds P [e,f1.e]
from FUNCT_2:sch 1 (A1);
take f1;
let H be strict Subgroup of G1;
let A be Subset of G2;
A3: H in the carrier of lattice G1 by GROUP_3:def 1;
assume A = f.:the carrier of H;
hence thesis by A2,A3;
end;
uniqueness
proof
let f1, f2 be Function of the carrier of lattice G1, the carrier of
lattice G2 such that
A4: for H being strict Subgroup of G1, A being Subset of G2 st A = f.:
the carrier of H holds f1.H = gr A and
A5: for H being strict Subgroup of G1, A being Subset of G2 st A = f.:
the carrier of H holds f2.H = gr A;
for h being object st h in the carrier of lattice G1 holds f1.h = f2.h
proof
let h be object;
assume h in the carrier of lattice G1;
then reconsider H = h as strict Subgroup of G1 by GROUP_3:def 1;
thus f1.h = gr (f.:the carrier of H) by A4
.= f2.h by A5;
end;
hence thesis by FUNCT_2:12;
end;
end;
theorem
for G being Group holds FuncLatt id the carrier of G = id the carrier
of lattice G
proof
let G be Group;
set f = id the carrier of G;
A1: for x being object st x in the carrier of lattice G
holds (FuncLatt f).x = x
proof
let x be object;
assume x in the carrier of lattice G;
then reconsider x as strict Subgroup of G by GROUP_3:def 1;
A2: the carrier of x c= f.:the carrier of x
proof
let z be object;
assume
A3: z in the carrier of x;
the carrier of x c= the carrier of G by GROUP_2:def 5;
then reconsider z as Element of G by A3;
f.z = z;
hence thesis by A3,FUNCT_2:35;
end;
A4: f.:the carrier of x c= the carrier of x
proof
let z be object;
assume
A5: z in f.:the carrier of x;
then reconsider z as Element of G;
ex Z being Element of G st Z in the carrier of x & z = f. Z by A5,
FUNCT_2:65;
hence thesis;
end;
then reconsider X = the carrier of x as Subset of G by A2,XBOOLE_0:def 10;
f.:the carrier of x = the carrier of x by A4,A2;
then (FuncLatt f).x = gr X by Def3;
hence thesis by Th3;
end;
dom FuncLatt f = the carrier of lattice G by FUNCT_2:def 1;
hence thesis by A1,FUNCT_1:17;
end;
theorem
for G1, G2 being Group for f being Homomorphism of G1, G2 st f is
one-to-one holds FuncLatt f is one-to-one
proof
let G1, G2 be Group;
let f be Homomorphism of G1, G2 such that
A1: f is one-to-one;
for x1, x2 being object st x1 in dom FuncLatt f & x2 in dom FuncLatt f & (
FuncLatt f).x1 = (FuncLatt f).x2 holds x1 = x2
proof
reconsider y = f.(1_G1) as Element of G2;
let x1, x2 be object;
assume that
A2: x1 in dom FuncLatt f & x2 in dom FuncLatt f and
A3: (FuncLatt f).x1 = (FuncLatt f).x2;
reconsider x1, x2 as strict Subgroup of G1 by A2,GROUP_3:def 1;
reconsider A1 = f.:the carrier of x1, A2 = f.:the carrier of x2 as Subset
of G2;
A4: for g being Element of G2 st g in f.:the carrier of x1 holds g" in f
.:the carrier of x1
proof
let g be Element of G2;
assume g in f.:the carrier of x1;
then consider x being Element of G1 such that
A5: x in the carrier of x1 and
A6: g = f.x by FUNCT_2:65;
x in x1 by A5,STRUCT_0:def 5;
then x" in x1 by GROUP_2:51;
then
A7: x" in the carrier of x1 by STRUCT_0:def 5;
f.x" = (f.x)" by GROUP_6:32;
hence thesis by A6,A7,FUNCT_2:35;
end;
A8: for g1, g2 being Element of G2 st g1 in f.:the carrier of x1 & g2 in
f.:the carrier of x1 holds g1 * g2 in f.:the carrier of x1
proof
let g1, g2 be Element of G2;
assume that
A9: g1 in f.:the carrier of x1 and
A10: g2 in f.:the carrier of x1;
consider x being Element of G1 such that
A11: x in the carrier of x1 and
A12: g1 = f.x by A9,FUNCT_2:65;
consider y being Element of G1 such that
A13: y in the carrier of x1 and
A14: g2 = f.y by A10,FUNCT_2:65;
A15: y in x1 by A13,STRUCT_0:def 5;
x in x1 by A11,STRUCT_0:def 5;
then x * y in x1 by A15,GROUP_2:50;
then
A16: x * y in the carrier of x1 by STRUCT_0:def 5;
f.(x * y) = f.x * f.y by GROUP_6:def 6;
hence thesis by A12,A14,A16,FUNCT_2:35;
end;
A17: for g being Element of G2 st g in f.:the carrier of x2 holds g" in f
.:the carrier of x2
proof
let g be Element of G2;
assume g in f.:the carrier of x2;
then consider x being Element of G1 such that
A18: x in the carrier of x2 and
A19: g = f.x by FUNCT_2:65;
x in x2 by A18,STRUCT_0:def 5;
then x" in x2 by GROUP_2:51;
then
A20: x" in the carrier of x2 by STRUCT_0:def 5;
f.x" = (f.x)" by GROUP_6:32;
hence thesis by A19,A20,FUNCT_2:35;
end;
A21: dom f = the carrier of G1 by FUNCT_2:def 1;
A22: for g1, g2 being Element of G2 st g1 in f.:the carrier of x2 & g2 in
f.:the carrier of x2 holds g1 * g2 in f.:the carrier of x2
proof
let g1, g2 be Element of G2;
assume that
A23: g1 in f.:the carrier of x2 and
A24: g2 in f.:the carrier of x2;
consider x being Element of G1 such that
A25: x in the carrier of x2 and
A26: g1 = f.x by A23,FUNCT_2:65;
consider y being Element of G1 such that
A27: y in the carrier of x2 and
A28: g2 = f.y by A24,FUNCT_2:65;
A29: y in x2 by A27,STRUCT_0:def 5;
x in x2 by A25,STRUCT_0:def 5;
then x * y in x2 by A29,GROUP_2:50;
then
A30: x * y in the carrier of x2 by STRUCT_0:def 5;
f.(x * y) = f.x * f.y by GROUP_6:def 6;
hence thesis by A26,A28,A30,FUNCT_2:35;
end;
1_G1 in x2 by GROUP_2:46;
then
A31: 1_G1 in the carrier of x2 by STRUCT_0:def 5;
A32: (FuncLatt f).x1 = gr A1 & (FuncLatt f).x2 = gr A2 by Def3;
ex y being Element of G2 st y = f.(1_G1);
then f.:the carrier of x2 <> {} by A21,A31,FUNCT_1:def 6;
then consider B2 being strict Subgroup of G2 such that
A33: the carrier of B2 = f.:the carrier of x2 by A17,A22,GROUP_2:52;
1_G1 in x1 by GROUP_2:46;
then 1_G1 in the carrier of x1 by STRUCT_0:def 5;
then y in f.:the carrier of x1 by A21,FUNCT_1:def 6;
then
A34: ex B1 being strict Subgroup of G2 st the carrier of B1 = f .:the
carrier of x1 by A4,A8,GROUP_2:52;
gr (f.:the carrier of x2) = B2 by A33,Th3;
then
A35: f.:the carrier of x1 = f.:the carrier of x2 by A3,A32,A34,A33,Th3;
the carrier of x2 c= dom f by A21,GROUP_2:def 5;
then
A36: the carrier of x2 c= the carrier of x1 by A1,A35,FUNCT_1:87;
the carrier of x1 c= dom f by A21,GROUP_2:def 5;
then the carrier of x1 c= the carrier of x2 by A1,A35,FUNCT_1:87;
then the carrier of x1 = the carrier of x2 by A36;
hence thesis by GROUP_2:59;
end;
hence thesis by FUNCT_1:def 4;
end;
theorem
for G1, G2 being Group for f being Homomorphism of G1, G2 holds (
FuncLatt f).(1).G1 = (1).G2
proof
let G1, G2 be Group;
let f be Homomorphism of G1, G2;
consider A being Subset of G2 such that
A1: A = f.:the carrier of (1).G1;
A2: A = f.:{1_G1} by A1,GROUP_2:def 7;
A3: 1_G1 in {1_G1} & 1_G2 = f.1_G1 by GROUP_6:31,TARSKI:def 1;
for x being object holds x in A iff x = 1_G2
proof
let x be object;
thus x in A implies x = 1_G2
proof
assume
A4: x in A;
then reconsider x as Element of G2;
consider y being Element of G1 such that
A5: y in {1_G1} and
A6: x = f.y by A2,A4,FUNCT_2:65;
y = 1_G1 by A5,TARSKI:def 1;
hence thesis by A6,GROUP_6:31;
end;
thus thesis by A2,A3,FUNCT_2:35;
end;
then A = {1_G2} by TARSKI:def 1;
then gr A = (1).G2 by Th12;
hence thesis by A1,Def3;
end;
theorem Th31:
for G1, G2 being 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
proof
let G1, G2 be Group;
let f be Homomorphism of G1, G2 such that
A1: f is one-to-one;
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;
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 thesis
proof
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
proof
let g1, g2 be Element of G2;
assume that
A5: g1 in f.:the carrier of B1 and
A6: g2 in f.:the carrier of B1;
consider x being Element of G1 such that
A7: x in the carrier of B1 and
A8: g1 = f.x by A5,FUNCT_2:65;
consider y being Element of G1 such that
A9: y in the carrier of B1 and
A10: g2 = f.y by A6,FUNCT_2:65;
A11: y in B1 by A9,STRUCT_0:def 5;
x in B1 by A7,STRUCT_0:def 5;
then x * y in B1 by A11,GROUP_2:50;
then
A12: x * y in the carrier of B1 by STRUCT_0:def 5;
f.(x * y) = f.x * f.y by GROUP_6:def 6;
hence thesis by A8,A10,A12,FUNCT_2:35;
end;
A13: for g being Element of G2 st g in f.:the carrier of B1 holds g" in
f.:the carrier of B1
proof
let g be Element of G2;
assume g in f.:the carrier of B1;
then consider x being Element of G1 such that
A14: x in the carrier of B1 and
A15: g = f.x by FUNCT_2:65;
x in B1 by A14,STRUCT_0:def 5;
then x" in B1 by GROUP_2:51;
then
A16: x" in the carrier of B1 by STRUCT_0:def 5;
f.x" = (f.x)" by GROUP_6:32;
hence thesis by A15,A16,FUNCT_2:35;
end;
A17: for g being Element of G2 st g in f.:the carrier of A1 holds g" in
f.:the carrier of A1
proof
let g be Element of G2;
assume g in f.:the carrier of A1;
then consider x being Element of G1 such that
A18: x in the carrier of A1 and
A19: g = f.x by FUNCT_2:65;
x in A1 by A18,STRUCT_0:def 5;
then x" in A1 by GROUP_2:51;
then
A20: x" in the carrier of A1 by STRUCT_0:def 5;
f.x" = (f.x)" by GROUP_6:32;
hence thesis by A19,A20,FUNCT_2:35;
end;
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
proof
let g1, g2 be Element of G2;
assume that
A25: g1 in f.:the carrier of A1 and
A26: g2 in f.:the carrier of A1;
consider x being Element of G1 such that
A27: x in the carrier of A1 and
A28: g1 = f.x by A25,FUNCT_2:65;
consider y being Element of G1 such that
A29: y in the carrier of A1 and
A30: g2 = f.y by A26,FUNCT_2:65;
A31: y in A1 by A29,STRUCT_0:def 5;
x in A1 by A27,STRUCT_0:def 5;
then x * y in A1 by A31,GROUP_2:50;
then
A32: x * y in the carrier of A1 by STRUCT_0:def 5;
f.(x * y) = f.x * f.y by GROUP_6:def 6;
hence thesis by A28,A30,A32,FUNCT_2:35;
end;
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
proof
let g1, g2 be Element of G2;
assume that
A37: g1 in f.:the carrier of C1 and
A38: g2 in f.:the carrier of C1;
consider x being Element of G1 such that
A39: x in the carrier of C1 and
A40: g1 = f.x by A37,FUNCT_2:65;
consider y being Element of G1 such that
A41: y in the carrier of C1 and
A42: g2 = f.y by A38,FUNCT_2:65;
A43: y in C1 by A41,STRUCT_0:def 5;
x in C1 by A39,STRUCT_0:def 5;
then x * y in C1 by A43,GROUP_2:50;
then
A44: x * y in the carrier of C1 by STRUCT_0:def 5;
f.(x * y) = f.x * f.y by GROUP_6:def 6;
hence thesis by A40,A42,A44,FUNCT_2:35;
end;
A45: for g being Element of G2 st g in f.:the carrier of C1 holds g" in
f.:the carrier of C1
proof
let g be Element of G2;
assume g in f.:the carrier of C1;
then consider x being Element of G1 such that
A46: x in the carrier of C1 and
A47: g = f.x by FUNCT_2:65;
x in C1 by A46,STRUCT_0:def 5;
then x" in C1 by GROUP_2:51;
then
A48: x" in the carrier of C1 by STRUCT_0:def 5;
f.x" = (f.x)" by GROUP_6:32;
hence thesis by A47,A48,FUNCT_2:35;
end;
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
proof
A54: f.:the carrier of A1 /\ B1 c= f.:the carrier of B1
proof
let x be object;
assume
A55: x in f.:the carrier of A1 /\ B1;
then reconsider x as Element of G2;
consider y being Element of G1 such that
A56: y in the carrier of A1 /\ B1 and
A57: x = f.y by A55,FUNCT_2:65;
y in (the carrier of A1) /\ the carrier of B1 by A56,Th1;
then y in the carrier of B1 by XBOOLE_0:def 4;
hence thesis by A57,FUNCT_2:35;
end;
A58: f.:the carrier of A1 /\ B1 c= f.:the carrier of A1
proof
let x be object;
assume
A59: x in f.:the carrier of A1 /\ B1;
then reconsider x as Element of G2;
consider y being Element of G1 such that
A60: y in the carrier of A1 /\ B1 and
A61: x = f.y by A59,FUNCT_2:65;
y in (the carrier of A1) /\ the carrier of B1 by A60,Th1;
then y in the carrier of A1 by XBOOLE_0:def 4;
hence thesis by A61,FUNCT_2:35;
end;
let x be object;
assume
A62: x in the carrier of C3;
the carrier of C3 c= the carrier of G2 by GROUP_2:def 5;
then reconsider x as Element of G2 by A62;
consider y being Element of G1 such that
A63: y in the carrier of A1 /\ B1 and
A64: x = f.y by A23,A50,A62,FUNCT_2:65;
f.y in f.:the carrier of A1 /\ B1 by A63,FUNCT_2:35;
then f.y in (the carrier of A3) /\ the carrier of B3 by A52,A51,A58,A54
,XBOOLE_0:def 4;
hence thesis by A64,Th1;
end;
A65: gr (f.:the carrier of B1) = B3 by A51,Th3;
the carrier of A3 /\ B3 c= the carrier of C3
proof
let x be object;
assume x in the carrier of A3 /\ B3;
then x in (the carrier of A3) /\ the carrier of B3 by Th1;
then
x in f.:((the carrier of A1) /\ the carrier of B1) by A1,A52,A51,
FUNCT_1:62;
hence thesis by A23,A50,Th1;
end;
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 thesis by A2,A3,A22,Th23;
end;
end;
hence thesis by LATTICE4:def 2;
end;
theorem Th32:
for G1, G2 being Group for f being Homomorphism of G1, G2 holds
FuncLatt f is sup-Semilattice-Homomorphism of lattice G1, lattice G2
proof
let G1, G2 be Group;
let f be Homomorphism of G1, 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;
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 thesis
proof
A3: for g being Element of G2 st g in f.:the carrier of B1 holds g" in
f.:the carrier of B1
proof
let g be Element of G2;
assume g in f.:the carrier of B1;
then consider x being Element of G1 such that
A4: x in the carrier of B1 and
A5: g = f.x by FUNCT_2:65;
x in B1 by A4,STRUCT_0:def 5;
then x" in B1 by GROUP_2:51;
then
A6: x" in the carrier of B1 by STRUCT_0:def 5;
f.x" = (f.x)" by GROUP_6:32;
hence thesis by A5,A6,FUNCT_2:35;
end;
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
proof
let g be Element of G2;
assume g in f.:the carrier of A1;
then consider x being Element of G1 such that
A10: x in the carrier of A1 and
A11: g = f.x by FUNCT_2:65;
x in A1 by A10,STRUCT_0:def 5;
then x" in A1 by GROUP_2:51;
then
A12: x" in the carrier of A1 by STRUCT_0:def 5;
f.x" = (f.x)" by GROUP_6:32;
hence thesis by A11,A12,FUNCT_2:35;
end;
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
proof
let g1, g2 be Element of G2;
assume that
A15: g1 in f.:the carrier of B1 and
A16: g2 in f.:the carrier of B1;
consider x being Element of G1 such that
A17: x in the carrier of B1 and
A18: g1 = f.x by A15,FUNCT_2:65;
consider y being Element of G1 such that
A19: y in the carrier of B1 and
A20: g2 = f.y by A16,FUNCT_2:65;
A21: y in B1 by A19,STRUCT_0:def 5;
x in B1 by A17,STRUCT_0:def 5;
then x * y in B1 by A21,GROUP_2:50;
then
A22: x * y in the carrier of B1 by STRUCT_0:def 5;
f.(x * y) = f.x * f.y by GROUP_6:def 6;
hence thesis by A18,A20,A22,FUNCT_2:35;
end;
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
proof
let g1, g2 be Element of G2;
assume that
A27: g1 in f.:the carrier of A1 and
A28: g2 in f.:the carrier of A1;
consider x being Element of G1 such that
A29: x in the carrier of A1 and
A30: g1 = f.x by A27,FUNCT_2:65;
consider y being Element of G1 such that
A31: y in the carrier of A1 and
A32: g2 = f.y by A28,FUNCT_2:65;
A33: y in A1 by A31,STRUCT_0:def 5;
x in A1 by A29,STRUCT_0:def 5;
then x * y in A1 by A33,GROUP_2:50;
then
A34: x * y in the carrier of A1 by STRUCT_0:def 5;
f.(x * y) = f.x * f.y by GROUP_6:def 6;
hence thesis by A30,A32,A34,FUNCT_2:35;
end;
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
proof
let g1, g2 be Element of G2;
assume that
A38: g1 in f.:the carrier of C1 and
A39: g2 in f.:the carrier of C1;
consider x being Element of G1 such that
A40: x in the carrier of C1 and
A41: g1 = f.x by A38,FUNCT_2:65;
consider y being Element of G1 such that
A42: y in the carrier of C1 and
A43: g2 = f.y by A39,FUNCT_2:65;
A44: y in C1 by A42,STRUCT_0:def 5;
x in C1 by A40,STRUCT_0:def 5;
then x * y in C1 by A44,GROUP_2:50;
then
A45: x * y in the carrier of C1 by STRUCT_0:def 5;
f.(x * y) = f.x * f.y by GROUP_6:def 6;
hence thesis by A41,A43,A45,FUNCT_2:35;
end;
A46: for g being Element of G2 st g in f.:the carrier of C1 holds g" in
f.:the carrier of C1
proof
let g be Element of G2;
assume g in f.:the carrier of C1;
then consider x being Element of G1 such that
A47: x in the carrier of C1 and
A48: g = f.x by FUNCT_2:65;
x in C1 by A47,STRUCT_0:def 5;
then x" in C1 by GROUP_2:51;
then
A49: x" in the carrier of C1 by STRUCT_0:def 5;
f.x" = (f.x)" by GROUP_6:32;
hence thesis by A48,A49,FUNCT_2:35;
end;
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
proof
let x be object;
assume
A54: x in f.:the carrier of B1;
then reconsider x as Element of G2;
consider y being Element of G1 such that
A55: y in the carrier of B1 and
A56: x = f.y by A54,FUNCT_2:65;
y in A by A55,XBOOLE_0:def 3;
then y in gr A by GROUP_4:29;
then y in the carrier of gr A by STRUCT_0:def 5;
then y in the carrier of A1 "\/" B1 by Th4;
hence thesis by A36,A50,A56,FUNCT_2:35;
end;
f.:the carrier of A1 c= the carrier of C3
proof
let x be object;
assume
A57: x in f.:the carrier of A1;
then reconsider x as Element of G2;
consider y being Element of G1 such that
A58: y in the carrier of A1 and
A59: x = f.y by A57,FUNCT_2:65;
y in A by A58,XBOOLE_0:def 3;
then y in gr A by GROUP_4:29;
then y in the carrier of gr A by STRUCT_0:def 5;
then y in the carrier of A1 "\/" B1 by Th4;
hence thesis by A36,A50,A59,FUNCT_2:35;
end;
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;
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
proof
let g be Element of G1;
assume g in f"the carrier of A3 "\/" B3;
then f.g in the carrier of A3 "\/" B3 by FUNCT_2:38;
then f.g in A3 "\/" B3 by STRUCT_0:def 5;
then (f.g)" in A3 "\/" B3 by GROUP_2:51;
then f.g" in A3 "\/" B3 by GROUP_6:32;
then f.g" in the carrier of A3 "\/" B3 by STRUCT_0:def 5;
hence thesis by FUNCT_2:38;
end;
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
proof
let g1, g2 be Element of G1;
assume that
A64: g1 in f"the carrier of A3 "\/" B3 and
A65: g2 in f"the carrier of A3 "\/" B3;
f.g2 in the carrier of A3 "\/" B3 by A65,FUNCT_2:38;
then
A66: f.g2 in A3 "\/" B3 by STRUCT_0:def 5;
f.g1 in the carrier of A3 "\/" B3 by A64,FUNCT_2:38;
then f.g1 in A3 "\/" B3 by STRUCT_0:def 5;
then f.g1 * f.g2 in A3 "\/" B3 by A66,GROUP_2:50;
then f.(g1 * g2) in A3 "\/" B3 by GROUP_6:def 6;
then f.(g1 * g2) in the carrier of A3 "\/" B3 by STRUCT_0:def 5;
hence thesis by FUNCT_2:38;
end;
A67: f"the carrier of B3 c= f"the carrier of A3 "\/" B3
proof
let x be object;
assume
A68: x in f"the carrier of B3;
then f.x in the carrier of B3 by FUNCT_2:38;
then
A69: f.x in B3 by STRUCT_0:def 5;
f.x in the carrier of G2 by A68,FUNCT_2:5;
then f.x in A3 "\/" B3 by A69,Th5;
then f.x in the carrier of A3 "\/" B3 by STRUCT_0:def 5;
hence thesis by A68,FUNCT_2:38;
end;
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
proof
let x be object;
assume
A71: x in f"the carrier of A3;
then f.x in the carrier of A3 by FUNCT_2:38;
then
A72: f.x in A3 by STRUCT_0:def 5;
f.x in the carrier of G2 by A71,FUNCT_2:5;
then f.x in A3 "\/" B3 by A72,Th5;
then f.x in the carrier of A3 "\/" B3 by STRUCT_0:def 5;
hence thesis by A71,FUNCT_2:38;
end;
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)
proof
let x be object;
assume
A75: x in f.:the carrier of C1;
then reconsider x as Element of G2;
ex y being Element of G1 st y in the carrier of C1 & x = f.y by A75,
FUNCT_2:65;
hence thesis by A73,FUNCT_2:35;
end;
f.:f"the carrier of A3 "\/" B3 c= the carrier of A3 "\/" B3 by
FUNCT_1:75;
hence thesis by A50,A74;
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 thesis by A1,A2,A24,Th22;
end;
end;
hence thesis by LATTICE4:def 1;
end;
theorem
for G1, G2 being Group for f being Homomorphism of G1, G2 st f is
one-to-one holds FuncLatt f is Homomorphism of lattice G1, lattice G2
by Th31,Th32;