The abstract of the Mizar article:

On the Group of Inner Automorphisms

by

Artur Kornilowicz

Received April 22, 1994

MML identifier: AUTGROUP

[ Mizar article, MML identifier index ]

environ

 vocabulary REALSET1, GROUP_2, GROUP_6, GROUP_1, GROUP_3, RELAT_1, FRAENKEL,
      FUNCT_1, FUNCT_2, BINOP_1, VECTSP_1, GROUP_5, WELLORD1, AUTGROUP;
 notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, REALSET1, RELAT_1, FUNCT_1,
      PARTFUN1, FUNCT_2, STRUCT_0, BINOP_1, FRAENKEL, RLVECT_1, VECTSP_1,
      GROUP_1, GROUP_2, GROUP_3, GROUP_5, GROUP_6;
 constructors REALSET1, FUNCSDOM, GROUP_5, GROUP_6, PARTFUN1, MEMBERED,
      RELAT_2, XBOOLE_0;
 clusters FUNCT_1, FRAENKEL, GROUP_1, GROUP_2, GROUP_3, GROUP_6, STRUCT_0,
      GR_CY_2, RELSET_1, MEMBERED, ZFMISC_1, PARTFUN1, FUNCT_2, XBOOLE_0;
 requirements SUBSET, BOOLE;


begin

 reserve G for strict Group;
 reserve H for Subgroup of G;
 reserve a, b, c, x, y for Element of G;
 reserve h for Homomorphism of G, G;
 reserve q, q1 for set;

theorem :: AUTGROUP:1
 (for a, b st b is Element of H holds b |^ a in
 H) iff H is normal;

definition
  let G;
  func Aut G -> FUNCTION_DOMAIN of the carrier of G, the carrier of G means
:: AUTGROUP:def 1
  ( for f being Element of it
    holds f is Homomorphism of G, G ) &
     for h holds h in it iff h is one-to-one & h is_epimorphism;
end;

canceled;

theorem :: AUTGROUP:3
  Aut G c= Funcs (the carrier of G, the carrier of G);

theorem :: AUTGROUP:4
id the carrier of G is Element of Aut G;

theorem :: AUTGROUP:5
for h holds h in Aut G iff h is_isomorphism;

theorem :: AUTGROUP:6
for f being Element of Aut G holds f" is Homomorphism of G, G;

theorem :: AUTGROUP:7
for f being Element of Aut G
  holds f" is Element of Aut G;

theorem :: AUTGROUP:8
for f1, f2 being Element of Aut G
holds f1 * f2 is Element of Aut G;

definition
  let G;
  func AutComp G -> BinOp of Aut G means
:: AUTGROUP:def 2
  for x, y being Element of Aut G holds it.(x,y) = x * y;
end;

definition
  let G;
  func AutGroup G -> strict Group equals
:: AUTGROUP:def 3
   HGrStr (# Aut G, AutComp G #);
end;

theorem :: AUTGROUP:9
for x, y being Element of AutGroup G
  for f, g being Element of Aut G st x = f & y = g
  holds x * y = f * g;

theorem :: AUTGROUP:10
id the carrier of G = 1.AutGroup G;

theorem :: AUTGROUP:11
for f being Element of Aut G
  for g being Element of AutGroup G st f = g holds f" = g";

definition
  let G;
  func InnAut G -> FUNCTION_DOMAIN of the carrier of G,the carrier of G means
:: AUTGROUP:def 4
  for f being Element of Funcs (the carrier of G, the carrier of G)
    holds f in it iff ex a st for x holds f.x = x |^ a;
end;

theorem :: AUTGROUP:12
  InnAut G c= Funcs (the carrier of G, the carrier of G);

theorem :: AUTGROUP:13
for f being Element of InnAut G
 holds f is Element of Aut G;

theorem :: AUTGROUP:14
InnAut G c= Aut G;

theorem :: AUTGROUP:15
for f, g being Element of InnAut G
holds (AutComp G).(f, g) = f * g;

theorem :: AUTGROUP:16
id the carrier of G is Element of InnAut G;

theorem :: AUTGROUP:17
for f being Element of InnAut G
holds f" is Element of InnAut G;

theorem :: AUTGROUP:18
for f, g being Element of InnAut G
holds f * g is Element of InnAut G;

definition
  let G;
  func InnAutGroup G -> normal strict Subgroup of AutGroup G means
:: AUTGROUP:def 5
  the carrier of it = InnAut G;
end;

canceled;

theorem :: AUTGROUP:20
for x, y being Element of InnAutGroup G
  for f, g being Element of InnAut G st x = f & y = g
  holds x * y = f * g;

theorem :: AUTGROUP:21
id the carrier of G = 1.InnAutGroup G;

theorem :: AUTGROUP:22
  for f being Element of InnAut G
  for g being Element of InnAutGroup G st f = g holds f" = g";

definition
  let G, b;
  func Conjugate b -> Element of InnAut G means
:: AUTGROUP:def 6
  for a holds it.a = a |^ b;
end;

theorem :: AUTGROUP:23
for a, b holds Conjugate (a * b) = (Conjugate b) * (Conjugate a);

theorem :: AUTGROUP:24
Conjugate 1.G = id the carrier of G;

theorem :: AUTGROUP:25
for a holds (Conjugate 1.G).a = a;

theorem :: AUTGROUP:26
  for a holds (Conjugate a) * (Conjugate a") = Conjugate 1.G;

theorem :: AUTGROUP:27
for a holds (Conjugate a") * (Conjugate a) = Conjugate 1.G;

theorem :: AUTGROUP:28
  for a holds Conjugate a" = (Conjugate a)";

theorem :: AUTGROUP:29
  for a holds ( (Conjugate a) * (Conjugate 1.G) = Conjugate a ) &
       ( (Conjugate 1.G) * (Conjugate a) = Conjugate a );

theorem :: AUTGROUP:30
  for f being Element of InnAut G holds
    f * Conjugate 1.G = f & (Conjugate 1.G) * f = f;

theorem :: AUTGROUP:31
  for G holds InnAutGroup G, G./.center G are_isomorphic;

theorem :: AUTGROUP:32
  for G holds ( G is commutative Group implies
  for f being Element of InnAutGroup G
  holds f = 1.InnAutGroup G );