The abstract of the Mizar article:

On the Lattice of Subgroups of a Group

by

Janusz Ganczarski

Received May 23, 1995

MML identifier: LATSUBGR

[ Mizar article, MML identifier index ]

environ

 vocabulary REALSET1, GROUP_2, BOOLE, GROUP_3, GROUP_4, LATTICES, GROUP_6,
      RELAT_1, FUNCT_1, GROUP_1, SETFAM_1, RLSUB_2, BHSP_3, LATTICE3, VECTSP_8;
 notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, FUNCT_1, RELAT_1, SETFAM_1,
      PARTFUN1, FUNCT_2, BINOP_1, STRUCT_0, LATTICES, RLVECT_1, VECTSP_1,
      GROUP_1, GROUP_2, GROUP_3, GROUP_4, GROUP_6, LATTICE3, LATTICE4,
      VECTSP_8;
 constructors DOMAIN_1, BINOP_1, GROUP_4, GROUP_6, LATTICE3, LATTICE4,
      VECTSP_8;
 clusters STRUCT_0, GROUP_1, GROUP_3, RELSET_1, SUBSET_1, GROUP_4, FUNCT_2,
      PARTFUN1, XBOOLE_0;
 requirements BOOLE, SUBSET;


begin

theorem :: LATSUBGR:1
 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;

theorem :: LATSUBGR:2
 for G being Group
 for h being set holds
  h in Subgroups G iff ex H being strict Subgroup of G st h = H;

theorem :: LATSUBGR:3
 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;

theorem :: LATSUBGR:4
 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;

theorem :: LATSUBGR:5
 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;

theorem :: LATSUBGR:6
   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;

theorem :: LATSUBGR:7
   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;

canceled 2;

theorem :: LATSUBGR:10
   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;

theorem :: LATSUBGR:11
   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;

theorem :: LATSUBGR:12
   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;

theorem :: LATSUBGR:13
   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;

theorem :: LATSUBGR:14
 for G being Group
 for A being Subset of G st
  A = {1.G} holds gr A = (1).G;

definition
 let G be Group;
 func carr G -> Function of Subgroups G, bool the carrier of G means
:: LATSUBGR:def 1
  for H being strict Subgroup of G holds it.H = the carrier of H;
end;

canceled 3;

theorem :: LATSUBGR:18
 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;

theorem :: LATSUBGR:19
   for G being Group
 for H being strict Subgroup of G holds
  1.G in carr G.H;

theorem :: LATSUBGR:20
   for G being Group
 for H being strict Subgroup of G holds
  carr G.H <> {};

theorem :: LATSUBGR:21
   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;

theorem :: LATSUBGR:22
   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;

theorem :: LATSUBGR:23
 for G being Group
 for H1, H2 being strict Subgroup of G holds
  the carrier of H1 /\ H2 = carr G.H1 /\ carr G.H2;

theorem :: LATSUBGR:24
   for G being Group
 for H1, H2 being strict Subgroup of G holds
  carr G.(H1 /\ H2) = carr G.H1 /\ carr G.H2;

definition
 let G be Group;
 let F be non empty Subset of Subgroups G;
  func meet F -> strict Subgroup of G means
:: LATSUBGR:def 2
    the carrier of it = meet (carr G.:F);
end;

theorem :: LATSUBGR:25
   for G being Group
 for F being non empty Subset of Subgroups G holds
  (1).G in F implies meet F = (1).G;

theorem :: LATSUBGR:26
   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;

theorem :: LATSUBGR:27
 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;

theorem :: LATSUBGR:28
 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;

theorem :: LATSUBGR:29
 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;

theorem :: LATSUBGR:30
 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;

theorem :: LATSUBGR:31
   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;

theorem :: LATSUBGR:32
   for G being Group holds lattice G is complete;

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
:: LATSUBGR:def 3
   for H being strict Subgroup of G1, A being Subset of G2
    st A = f.:the carrier of H holds it.H = gr A;
end;

theorem :: LATSUBGR:33
   for G being Group holds
   FuncLatt id the carrier of G = id the carrier of lattice G;

theorem :: LATSUBGR:34
   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;

theorem :: LATSUBGR:35
   for G1, G2 being Group
  for f being Homomorphism of G1, G2 holds
   (FuncLatt f).(1).G1 = (1).G2;

theorem :: LATSUBGR:36
 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;

theorem :: LATSUBGR:37
 for G1, G2 being Group
  for f being Homomorphism of G1, G2 holds
   FuncLatt f is sup-Semilattice-Homomorphism of lattice G1, lattice G2;

theorem :: LATSUBGR:38
   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;