:: On the Group of Inner Automorphisms
::  by Artur Korni{\l}owicz
::
:: Received April 22, 1994
:: Copyright (c) 1994-2012 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 STRUCT_0, GROUP_1, GROUP_2, SUBSET_1, GROUP_6, NEWTON, PRE_TOPC,
      RELAT_1, TARSKI, FUNCT_2, FUNCT_1, XBOOLE_0, BINOP_1, ALGSTR_0, ZFMISC_1,
      REALSET1, GROUP_5, WELLORD1, AUTGROUP;
 notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, REALSET1, RELAT_1, FUNCT_1,
      RELSET_1, PARTFUN1, FUNCT_2, STRUCT_0, ALGSTR_0, BINOP_1, GROUP_1,
      GROUP_2, GROUP_3, GROUP_5, GROUP_6;
 constructors BINOP_1, REALSET1, GROUP_5, GROUP_6, RELSET_1;
 registrations XBOOLE_0, FUNCT_1, RELSET_1, FUNCT_2, STRUCT_0, GROUP_1,
      GROUP_2, GROUP_3, GROUP_6, GR_CY_2;
 requirements SUBSET, BOOLE;
 definitions FUNCT_1, TARSKI, BINOP_1, REALSET1, GROUP_2, GROUP_3, ALGSTR_0,
      FUNCT_2;
 theorems BINOP_1, FUNCT_1, FUNCT_2, GROUP_1, GROUP_2, GROUP_3, GROUP_5,
      GROUP_6, REALSET1, RELAT_1, ZFMISC_1, TARSKI, XBOOLE_0, STRUCT_0;
 schemes BINOP_1, FUNCT_2;

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;

Lm1: (for a,b st b is Element of H holds b |^ a in H) implies H is normal
proof
  assume
A1: for a, b st b is Element of H holds b |^ a in H;
  now
    let a;
    thus H * a c= a * H
    proof
      set A = carr H;
      let q;
      assume q in H * a;
      then consider b such that
A2:   q = b * a and
A3:   b in H by GROUP_2:104;
      b is Element of H by A3,STRUCT_0:def 5;
      then b |^ a in H by A1;
      then b |^ a in A by STRUCT_0:def 5;
      then a * (a" * b * a) in a * A by GROUP_2:27;
      then a * (a" * (b * a)) in a * A by GROUP_1:def 3;
      then (a * a") * (b * a) in a * A by GROUP_1:def 3;
      then a * a" * b * a in a * A by GROUP_1:def 3;
      then 1_G * b * a in a * A by GROUP_1:def 5;
      hence thesis by A2,GROUP_1:def 4;
    end;
  end;
  hence thesis by GROUP_3:119;
end;

Lm2: H is normal implies for a,b st b is Element of H holds b |^ a in H
proof

  assume
A1: H is normal;
  set A = carr H;
  let a, b;
  H * a = a * H by A1,GROUP_3:117;
  then a" * H * a = a" * (a * H) by GROUP_2:106;
  then a" * H * a = a" * a * H by GROUP_2:105;
  then a" * H * a = 1_G * H by GROUP_1:def 5;
  then a" * H * a = A by GROUP_2:109;
  then the carrier of H |^ a = A by GROUP_3:59;
  then
A2: A |^ a = A by GROUP_3:def 6;
  assume b is Element of H;
  then a" * b in a" * A by GROUP_2:27;
  then a" * b * a in a" * A * a by GROUP_2:28;
  then b |^ a in A by A2,GROUP_3:50;
  hence thesis by STRUCT_0:def 5;
end;

theorem
  (for a, b st b is Element of H holds b |^ a in H) iff H is normal by Lm1,Lm2;

definition
  let G;
  func Aut G -> FUNCTION_DOMAIN of the carrier of G, the carrier of G means
  :
  Def1: ( 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 onto;
  existence
  proof
    set X = { x where x is Element of Funcs (the carrier of G,the carrier of G
    ) : ex h st x = h & h is one-to-one & h is onto };
A1: id the carrier of G in X
    proof
      set I = id the carrier of G;
A2:   I in Funcs (the carrier of G, the carrier of G) by FUNCT_2:8;
      reconsider I as Homomorphism of G, G by GROUP_6:38;
      rng I = the carrier of G by RELAT_1:45;
      then I is onto by FUNCT_2:def 3;
      hence thesis by A2;
    end;
    reconsider X as set;
    X is functional
    proof
      let q;
      assume q in X;
      then
      ex x be Element of Funcs (the carrier of G, the carrier of G) st q =
      x & ex h st h = x & h is one-to-one & h is onto;
      hence thesis;
    end;
    then reconsider X as functional non empty set by A1;
    X is FUNCTION_DOMAIN of the carrier of G, the carrier of G
    proof
      let a be Element of X;
      a in X;
      then ex x be Element of Funcs (the carrier of G, the carrier of G ) st a
      = x & ex h st h = x & h is one-to-one & h is onto;
      hence thesis;
    end;
    then reconsider
    X as FUNCTION_DOMAIN of the carrier of G, the carrier of G;
    take X;
    hereby
      let f be Element of X;
      f in X;
      then
      ex x being Element of Funcs (the carrier of G, the carrier of G) st
      f = x & ex h st h = x & h is one-to-one & h is onto;
      hence f is Homomorphism of G, G;
    end;
    let x be Homomorphism of G, G;
    hereby
      assume x in X;
      then
      ex f being Element of Funcs (the carrier of G, the carrier of G) st
      f = x & ex h st h = f & h is one-to-one & h is onto;
      hence x is one-to-one & x is onto;
    end;
A3: x is Element of Funcs (the carrier of G, the carrier of G) by FUNCT_2:8;
    assume x is one-to-one & x is onto;
    hence thesis by A3;
  end;
  uniqueness
  proof
    let F1, F2 be FUNCTION_DOMAIN of the carrier of G, the carrier of G such
    that
A4: for f being Element of F1 holds f is Homomorphism of G, G and
A5: for h holds h in F1 iff h is one-to-one & h is onto and
A6: for f being Element of F2 holds f is Homomorphism of G, G and
A7: for h holds h in F2 iff h is one-to-one & h is onto;
A8: F2 c= F1
    proof
      let q;
      assume
A9:   q in F2;
      then reconsider h1 = q as Homomorphism of G, G by A6;
      h1 is one-to-one & h1 is onto by A7,A9;
      hence thesis by A5;
    end;
    F1 c= F2
    proof
      let q;
      assume
A10:  q in F1;
      then reconsider h1 = q as Homomorphism of G, G by A4;
      h1 is one-to-one & h1 is onto by A5,A10;
      hence thesis by A7;
    end;
    hence thesis by A8,XBOOLE_0:def 10;
  end;
end;

theorem
  Aut G c= Funcs (the carrier of G, the carrier of G)
proof
  let q;
  assume q in Aut G;
  then ex f be Element of Aut G st f = q;
  hence thesis by FUNCT_2:9;
end;

theorem Th3:
  id the carrier of G is Element of Aut G
proof
  id the carrier of G is Homomorphism of G, G by GROUP_6:38;
  then consider h such that
A1: h = id the carrier of G;
  rng h = the carrier of G by A1,RELAT_1:45;
  then h is onto by FUNCT_2:def 3;
  hence thesis by A1,Def1;
end;

theorem Th4:
  for h holds h in Aut G iff h is bijective
proof
  let h;
  hereby
    assume h in Aut G;
    then h is onto & h is one-to-one by Def1;
    hence h is bijective;
  end;
  thus thesis by Def1;
end;

Lm3: for f being Element of Aut G holds dom f = rng f & dom f = the carrier of
G
proof
  let f be Element of Aut G;
  reconsider f as Homomorphism of G, G by Def1;
A1: f is bijective by Th4;
  then dom f = the carrier of G by GROUP_6:61;
  hence thesis by A1,GROUP_6:61;
end;

theorem Th5:
  for f being Element of Aut G holds f" is Homomorphism of G, G
proof
  let f be Element of Aut G;
  reconsider f as Homomorphism of G, G by Def1;
  f is bijective by Th4;
  hence thesis by GROUP_6:62;
end;

theorem Th6:
  for f being Element of Aut G holds f" is Element of Aut G
proof
  let f be Element of Aut G;
  reconsider f as Homomorphism of G, G by Def1;
  reconsider A = f" as Homomorphism of G, G by Th5;
  f is bijective by Th4;
  then A is bijective by GROUP_6:63;
  hence thesis by Def1;
end;

theorem Th7:
  for f1, f2 being Element of Aut G holds f1 * f2 is Element of Aut G
proof
  let f1, f2 be Element of Aut G;
  reconsider f1, f2 as Homomorphism of G, G by Def1;
  f1 is bijective & f2 is bijective by Th4;
  then f1 * f2 is bijective;
  hence thesis by Th4;
end;

definition
  let G;
  func AutComp G -> BinOp of Aut G means
  :Def2:
  for x, y being Element of Aut G holds it.(x,y) = x * y;
  existence
  proof
    defpred P[Element of Aut G,Element of Aut G,set] means $3 = $1 * $2;
A1: for x, y being Element of Aut G ex m being Element of Aut G st P[x,y,m ]
    proof
      let x, y be Element of Aut G;
      reconsider xx = x, yy = y as Homomorphism of G, G by Def1;
      reconsider m = xx * yy as Element of Aut G by Th7;
      take m;
      thus thesis;
    end;
    thus ex M being BinOp of Aut G st for x, y being Element of Aut G holds P[
    x,y,M.(x,y)] from BINOP_1:sch 3 (A1);
  end;
  uniqueness
  proof
    let b1, b2 be BinOp of Aut G such that
A2: for x, y be Element of Aut G holds b1.(x,y) = x * y and
A3: for x, y be Element of Aut G holds b2.(x,y) = x * y;
    for x, y be Element of Aut G holds b1.(x,y) = b2.(x,y)
    proof
      let x, y be Element of Aut G;
      thus b1.(x,y) = x * y by A2
        .= b2.(x,y) by A3;
    end;
    hence thesis by BINOP_1:2;
  end;
end;

definition
  let G;
  func AutGroup G -> strict Group equals
  multMagma (# Aut G, AutComp G #);
  coherence
  proof
    set H = multMagma (# Aut G, AutComp G #);
A1: ex e being Element of H st for h being Element of H holds h * e = h &
    e * h = h & ex g being Element of H st h * g = e & g * h = e
    proof
      reconsider e = id the carrier of G as Element of H by Th3;
      take e;
      let h be Element of H;
      consider A be Element of Aut G such that
A2:   A = h;
      h * e = A * id the carrier of G by A2,Def2
        .= A by FUNCT_2:17;
      hence h * e = h by A2;
      e * h = (id the carrier of G) * A by A2,Def2
        .= A by FUNCT_2:17;
      hence e * h = h by A2;
      reconsider g = A" as Element of H by Th6;
      take g;
      reconsider A as Homomorphism of G, G by Def1;
A3:   A is one-to-one by Def1;
      A is onto by Def1;
      then
A4:   rng A = the carrier of G by FUNCT_2:def 3;
      thus h * g = A * A" by A2,Def2
        .= e by A3,A4,FUNCT_2:29;
      thus g * h = A" * A by A2,Def2
        .= e by A3,A4,FUNCT_2:29;
    end;
    for f, g, h being Element of H holds (f * g) * h = f * (g * h)
    proof
      let f,g,h be Element of H;
      reconsider A = f, B = g, C = h as Element of Aut G;
A5:   g * h = B * C by Def2;
      f * g = A * B by Def2;
      hence (f * g) * h = A * B * C by Def2
        .= A * (B * C) by RELAT_1:36
        .= f * (g * h) by A5,Def2;
    end;
    hence thesis by A1,GROUP_1:def 2,def 3;
  end;
end;

theorem
  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 by Def2;

theorem Th9:
  id the carrier of G = 1_AutGroup G
proof
  set f = the Element of AutGroup G;
  reconsider g = id the carrier of G as Element of AutGroup G by Th3;
  consider g1 be Function of the carrier of G, the carrier of G such that
A1: g1 = g;
  f is Homomorphism of G, G by Def1;
  then consider f1 be Function of the carrier of G, the carrier of G such that
A2: f1 = f;
  f1 = f & g1 = g implies f1 * g1 = f * g by Def2;
  hence thesis by A1,A2,FUNCT_2:17,GROUP_1:7;
end;

theorem Th10:
  for f being Element of Aut G for g being Element of AutGroup G
  st f = g holds f" = g"
proof
  let f be Element of Aut G;
  let g be Element of AutGroup G;
  consider g1 be Element of Aut G such that
A1: g1 = g";
  assume f = g;
  then g1 * f = g" * g by A1,Def2;
  then g1 * f = 1_AutGroup G by GROUP_1:def 5;
  then
A2: g1 * f = id the carrier of G by Th9;
  f is Homomorphism of G, G by Def1;
  then
A3: f is one-to-one by Def1;
  rng f = dom f by Lm3
    .= the carrier of G by Lm3;
  hence thesis by A1,A3,A2,FUNCT_2:30;
end;

definition
  let G;
  func InnAut G -> FUNCTION_DOMAIN of the carrier of G,the carrier of G means
  :Def4:
  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;
  existence
  proof
    set I = id the carrier of G;
    set X = { f where f is Element of Funcs (the carrier of G,the carrier of G
    ) : ex a st for x holds f.x = x |^ a };
A1: ex a st for x holds I.x = x |^ a
    proof
      take a = 1_G;
      let x;
A2:   a" = 1_G by GROUP_1:8;
      thus I.x = x by FUNCT_1:18
        .= x * a by GROUP_1:def 4
        .= x |^ a by A2,GROUP_1:def 4;
    end;
    I is Element of Funcs (the carrier of G, the carrier of G) by FUNCT_2:8;
    then
A3: I in X by A1;
    X is functional
    proof
      let h be set;
      assume h in X;
      then
      ex f being Element of Funcs (the carrier of G,the carrier of G) st f
      = h & ex a st for x holds f.x = x |^ a;
      hence thesis;
    end;
    then reconsider X as functional non empty set by A3;
    X is FUNCTION_DOMAIN of the carrier of G, the carrier of G
    proof
      let h be Element of X;
      h in X;
      then ex f being Element of Funcs (the carrier of G,the carrier of G) st
      f = h & ex a st for x holds f.x = x |^ a;
      hence thesis;
    end;
    then reconsider
    X as FUNCTION_DOMAIN of the carrier of G, the carrier of G;
    take X;
    let f be Element of Funcs (the carrier of G, the carrier of G);
    hereby
      assume f in X;
      then
      ex f1 being Element of Funcs (the carrier of G,the carrier of G) st
      f1 = f & ex a st for x holds f1.x = x |^ a;
      hence ex a st for x holds f.x = x |^ a;
    end;
    thus thesis;
  end;
  uniqueness
  proof
    let F1, F2 be FUNCTION_DOMAIN of the carrier of G, the carrier of G such
    that
A4: for f being Element of Funcs (the carrier of G, the carrier of G)
    holds f in F1 iff ex a st for x holds f.x = x |^ a and
A5: for f being Element of Funcs (the carrier of G, the carrier of G)
    holds f in F2 iff ex a st for x holds f.x = x |^ a;
A6: F2 c= F1
    proof
      let q;
      assume
A7:   q in F2;
      then q is Function of the carrier of G, the carrier of G by
FUNCT_2:def 12;
      then reconsider
      b1 = q as Element of Funcs (the carrier of G,the carrier of G
      ) by FUNCT_2:9;
      ex a st for x holds b1.x = x |^ a by A5,A7;
      hence thesis by A4;
    end;
    F1 c= F2
    proof
      let q;
      assume
A8:   q in F1;
      then q is Function of the carrier of G, the carrier of G by
FUNCT_2:def 12;
      then reconsider
      b1 = q as Element of Funcs (the carrier of G,the carrier of G
      ) by FUNCT_2:9;
      ex a st for x holds b1.x = x |^ a by A4,A8;
      hence thesis by A5;
    end;
    hence thesis by A6,XBOOLE_0:def 10;
  end;
end;

theorem
  InnAut G c= Funcs (the carrier of G, the carrier of G)
proof
  let q;
  assume q in InnAut G;
  then ex f be Element of InnAut G st f = q;
  hence thesis by FUNCT_2:9;
end;

theorem Th12:
  for f being Element of InnAut G holds f is Element of Aut G
proof
  let f be Element of InnAut G;
A1: f is Element of Funcs (the carrier of G, the carrier of G) by FUNCT_2:9;
  now
    let x,y;
    consider a such that
A2: for x holds f.x = x |^ a by A1,Def4;
    thus f.(x * y) = (x * y) |^ a by A2
      .= a" * x * y * a by GROUP_1:def 3
      .= (a" * x) * (y * a) by GROUP_1:def 3
      .= (a" * x) * 1_G * (y * a) by GROUP_1:def 4
      .= a" * x * (a * a") * (y * a) by GROUP_1:def 5
      .= a" * x * a * a" * (y * a) by GROUP_1:def 3
      .= (a" * x * a) * a" * y * a by GROUP_1:def 3
      .= (a" * x * a) * (a" * y) * a by GROUP_1:def 3
      .= (x |^ a) * (y |^ a) by GROUP_1:def 3
      .= f.x * (y |^ a) by A2
      .= f.x * f.y by A2;
  end;
  then reconsider f as Homomorphism of G, G by GROUP_6:def 6;
A3: f is one-to-one
  proof
    let q,q1;
    assume that
A4: q in dom f & q1 in dom f and
A5: f.q = f.q1;
    consider x, y such that
A6: x = q & y = q1 by A4;
    consider a such that
A7: for x holds f.x = x |^ a by A1,Def4;
    f.x = y |^ a by A7,A5,A6;
    then x |^ a = y |^ a by A7;
    then a * (a" * (x * a)) = a * (a" * y * a) by GROUP_1:def 3;
    then (a * a") * (x * a) = a * (a" * y * a) by GROUP_1:def 3;
    then (a * a") * (x * a) = a * (a" * (y * a)) by GROUP_1:def 3;
    then (a * a") * (x * a) = (a * a") * (y * a) by GROUP_1:def 3;
    then 1_G * (x * a) = (a * a") * (y * a) by GROUP_1:def 5;
    then 1_G * (x * a) = 1_G * (y * a) by GROUP_1:def 5;
    then x * a = 1_G * (y * a) by GROUP_1:def 4;
    then x * a * a" = y * a * a" by GROUP_1:def 4;
    then x * (a * a") = y * a * a" by GROUP_1:def 3;
    then x * (a * a") = y * (a * a") by GROUP_1:def 3;
    then x * 1_G = y * (a * a") by GROUP_1:def 5;
    then x * 1_G = y * 1_G by GROUP_1:def 5;
    then x = y * 1_G by GROUP_1:def 4;
    hence thesis by A6,GROUP_1:def 4;
  end;
  for q st q in the carrier of G ex q1 st q1 in dom f & q=f.q1
  proof
    let q;
    assume q in the carrier of G;
    then consider y such that
A8: y = q;
    consider a such that
A9: for x holds f.x = x |^ a by A1,Def4;
    take q1 = a * y * a";
    ex f1 being Function st f = f1 & dom f1 = the carrier of G & rng f1
    c= the carrier of G by A1,FUNCT_2:def 2;
    hence q1 in dom f;
    y = 1_G * y by GROUP_1:def 4
      .= 1_G * y * 1_G by GROUP_1:def 4
      .= a" * a * y * 1_G by GROUP_1:def 5
      .= a" * a * y * (a" * a) by GROUP_1:def 5
      .= (a" * a * y) * a" * a by GROUP_1:def 3
      .= (a" * a * (y * a")) * a by GROUP_1:def 3
      .= a" * (a * (y * a")) * a by GROUP_1:def 3
      .= q1 |^ a by GROUP_1:def 3
      .= f.q1 by A9;
    hence thesis by A8;
  end;
  then the carrier of G c= rng f by FUNCT_1:9;
  then rng f = the carrier of G by XBOOLE_0:def 10;
  then f is onto by FUNCT_2:def 3;
  hence thesis by A3,Def1;
end;

theorem Th13:
  InnAut G c= Aut G
proof
  now
    let q;
    assume q in InnAut G;
    then consider f be Element of InnAut G such that
A1: f = q;
    f is Element of Aut G by Th12;
    hence q in Aut G by A1;
  end;
  hence thesis by TARSKI:def 3;
end;

theorem Th14:
  for f, g being Element of InnAut G holds (AutComp G).(f, g) = f * g
proof
  let f, g be Element of InnAut G;
  f is Element of Aut G & g is Element of Aut G by Th12;
  hence thesis by Def2;
end;

theorem Th15:
  id the carrier of G is Element of InnAut G
proof
  set I = id the carrier of G;
A1: ex a st for x holds I.x = x |^ a
  proof
    take a = 1_G;
    let x;
A2: a" = 1_G by GROUP_1:8;
    thus I.x = x by FUNCT_1:18
      .= x * a by GROUP_1:def 4
      .= x |^ a by A2,GROUP_1:def 4;
  end;
  I is Element of Funcs (the carrier of G, the carrier of G) by FUNCT_2:8;
  hence thesis by A1,Def4;
end;

theorem Th16:
  for f being Element of InnAut G holds f" is Element of InnAut G
proof
  let f be Element of InnAut G;
  reconsider f1 = f as Element of Funcs (the carrier of G, the carrier of G)
  by FUNCT_2:9;
  f1 = f;
  then consider
  f1 be Element of Funcs (the carrier of G, the carrier of G) such
  that
A1: f1 = f;
A2: ex a st for x holds f".x = x |^ a
  proof
    consider b such that
A3: for y holds f1.y = y |^ b by A1,Def4;
    take a = b";
    let x;
A4: f1 is Element of Aut G by A1,Th12;
    then reconsider f1 as Homomorphism of G, G by Def1;
A5: f1 is bijective by A4,Th4;
    then consider y1 be Element of G such that
A6: x = f1.y1 by GROUP_6:58;
    f1".x = y1 by A5,A6,FUNCT_2:26
      .= 1_G * y1 by GROUP_1:def 4
      .= 1_G * y1 * 1_G by GROUP_1:def 4
      .= b * b" * y1 * 1_G by GROUP_1:def 5
      .= b * b" * y1 * (b * b") by GROUP_1:def 5
      .= (b * b" * y1) * b * b" by GROUP_1:def 3
      .= (b * b" * (y1 * b)) * b" by GROUP_1:def 3
      .= b * (b" * (y1 * b)) * b" by GROUP_1:def 3
      .= b * (y1 |^ b) * b" by GROUP_1:def 3
      .= b * x * b" by A3,A6
      .= a" * x * a;
    hence thesis by A1;
  end;
A7: f is Element of Aut G by Th12;
  then reconsider f2 = f as Homomorphism of G, G by Def1;
  f2 = f;
  then consider f2 be Homomorphism of G, G such that
A8: f2 = f;
  f2 is onto by A7,A8,Def1;
  then
A9: rng f2 = the carrier of G by FUNCT_2:def 3;
  f2 is one-to-one by A7,A8,Def1;
  then f" is Function of the carrier of G, the carrier of G by A8,A9,FUNCT_2:25
;
  then f" is Element of Funcs(the carrier of G, the carrier of G) by FUNCT_2:9
;
  hence thesis by A2,Def4;
end;

theorem Th17:
  for f, g being Element of InnAut G holds f * g is Element of InnAut G
proof
  let f, g be Element of InnAut G;
A1: g is Element of Funcs (the carrier of G, the carrier of G) by FUNCT_2:9;
A2: f is Element of Funcs (the carrier of G, the carrier of G) by FUNCT_2:9;
A3: ex a st for x holds (f * g).x = x |^ a
  proof
    consider c such that
A4: for x2 being Element of G holds g.x2 = x2 |^ c by A1,Def4;
    consider b such that
A5: for x1 being Element of G holds f.x1 = x1 |^ b by A2,Def4;
    take a = c * b;
    let x;
    (f * g).x = f.(g.x) by FUNCT_2:15
      .= f.(x |^ c) by A4
      .= (c" * x * c) |^ b by A5
      .= b" * (c" * x * c * b) by GROUP_1:def 3
      .= b" * (c" * (x * c) * b) by GROUP_1:def 3
      .= b" * (c" * (x * c * b)) by GROUP_1:def 3
      .= (b" * c") * (x * c * b) by GROUP_1:def 3
      .= (b" * c") * (x * (c * b)) by GROUP_1:def 3
      .= (b" * c") * x * (c * b) by GROUP_1:def 3
      .= x |^ a by GROUP_1:17;
    hence thesis;
  end;
  f * g is Element of Funcs (the carrier of G, the carrier of G) by FUNCT_2:9;
  hence thesis by A3,Def4;
end;

definition
  let G;
  func InnAutGroup G -> normal strict Subgroup of AutGroup G means
  :Def5:
  the carrier of it = InnAut G;
  existence
  proof
    reconsider K1 = Aut G as set;
    reconsider K2 = InnAut G as Subset of K1 by Th13;
    for q holds q in [:K2,K2:] implies (AutComp G).q in K2
    proof
      let q;
      assume q in [:K2,K2:];
      then consider x, y be set such that
A1:   x in K2 & y in K2 and
A2:   q = [x, y] by ZFMISC_1:def 2;
      reconsider x, y as Element of InnAut G by A1;
A3:   x * y is Element of InnAut G by Th17;
      (AutComp G).q = (AutComp G).(x, y) by A2
        .= x * y by Th14;
      hence thesis by A3;
    end;
    then AutComp G is Presv of K1, K2 by REALSET1:def 4;
    then reconsider op = (AutComp G)||InnAut G as BinOp of InnAut G by
REALSET1:6;
    set IG = multMagma (# InnAut G, op #);
A4: now
      let x,y be Element of IG, f,g be Element of InnAut G;
A5:   [f, g] in [:InnAut G, InnAut G:] by ZFMISC_1:def 2;
      assume x = f & y = g;
      hence x * y = (AutComp G).(f,g) by A5,FUNCT_1:49
        .= f * g by Th14;
    end;
A6: for f,g,h being Element of IG holds (f * g) * h = f * (g * h)
    proof
      let f,g,h be Element of IG;
      reconsider A = f, B = g, C = h as Element of InnAut G;
A7:   g * h = B * C by A4;
      f * g = A * B by A4;
      hence (f * g) * h = A * B * C by A4
        .= A * (B * C) by RELAT_1:36
        .= f * (g * h) by A4,A7;
    end;
    ex e being Element of IG st for h being Element of IG holds h * e = h
    & e * h = h & ex g being Element of IG st h * g = e & g * h = e
    proof
      reconsider e = id the carrier of G as Element of IG by Th15;
      take e;
      let h be Element of IG;
      consider A be Element of InnAut G such that
A8:   A = h;
      h * e = A * id the carrier of G by A4,A8
        .= A by FUNCT_2:17;
      hence h * e = h by A8;
      e * h = (id the carrier of G) * A by A4,A8
        .= A by FUNCT_2:17;
      hence e * h = h by A8;
      reconsider g = A" as Element of IG by Th16;
      take g;
      reconsider A as Element of Aut G by Th12;
      reconsider A as Homomorphism of G, G by Def1;
A9:   A is one-to-one by Def1;
      A is onto by Def1;
      then
A10:  rng A = the carrier of G by FUNCT_2:def 3;
      thus h * g = A * A" by A4,A8
        .= e by A9,A10,FUNCT_2:29;
      thus g * h = A" * A by A4,A8
        .= e by A9,A10,FUNCT_2:29;
    end;
    then reconsider IG as Group by A6,GROUP_1:def 2,def 3;
    the carrier of IG c= the carrier of AutGroup G by Th13;
    then reconsider IG as strict Subgroup of AutGroup G by GROUP_2:def 5;
    for f, k being Element of AutGroup G st k is Element of IG holds k |^
    f in IG
    proof
      let f, k be Element of AutGroup G;
      consider f1 be Element of Aut G such that
A11:  f1 = f;
      assume k is Element of IG;
      then consider g be Element of InnAut G such that
A12:  g = k;
      reconsider D = g as Element of Aut G by Th12;
      g is Element of Aut G by Th12;
      then consider g1 be Element of Aut G such that
A13:  g1 = g;
      g1 is Element of Funcs (the carrier of G, the carrier of G) by FUNCT_2:8
;
      then consider a such that
A14:  for x holds g1.x = x |^ a by A13,Def4;
      f1" * g1 * f1 is Element of InnAut G
      proof
        f1 is Homomorphism of G, G by Def1;
        then
A15:    f1 is one-to-one by Def1;
A16:    rng f1 = dom f1 by Lm3
          .= the carrier of G by Lm3;
        then f1" is Function of the carrier of G, the carrier of G by A15,
FUNCT_2:25;
        then
f1" * g1 is Function of the carrier of G, the carrier of G by FUNCT_2:13;
        then f1" * g1 * f1 is Function of the carrier of G, the carrier of G
        by FUNCT_2:13;
        then
A17:    f1" * g1 * f1 is Element of Funcs (the carrier of G, the carrier
        of G) by FUNCT_2:8;
        f1" is Element of Aut G by Th6;
        then f1" is Homomorphism of G, G by Def1;
        then consider A be Homomorphism of G, G such that
A18:    A = f1";
A19:    A * f1 = id the carrier of G by A15,A16,A18,FUNCT_2:29;
        now
          let y;
          thus (f1" * g1 * f1).y = (f1" * (g1 * f1)).y by RELAT_1:36
            .= f1".((g1 * f1).y) by FUNCT_2:15
            .= f1".(g1.(f1.y)) by FUNCT_2:15
            .= f1".(f1.y |^ a) by A14
            .= A.(a" * f1.y) * A.a by A18,GROUP_6:def 6
            .= A.a" * A.(f1.y) * A.a by GROUP_6:def 6
            .= A.a" * (A * f1).y * A.a by FUNCT_2:15
            .= A.a" * y * A.a by A19,FUNCT_1:18
            .= y |^ A.a by GROUP_6:32;
        end;
        hence thesis by A17,Def4;
      end;
      then
A20:  f1" * g * f1 in InnAut G by A13;
      reconsider C = f1" as Element of Aut G by Th6;
      consider q such that
A21:  q = f" * k * f;
      f1" = f" by A11,Th10;
      then C * D = f" * k by A12,Def2;
      then q in carr IG by A11,A20,A21,Def2;
      hence thesis by A21,STRUCT_0:def 5;
    end;
    then reconsider IG as normal strict Subgroup of AutGroup G by Lm1;
    take IG;
    thus thesis;
  end;
  uniqueness by GROUP_2:59;
end;

theorem Th18:
  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
proof
  let x,y be Element of InnAutGroup G;
  let f,g be Element of InnAut G;
  x is Element of AutGroup G & y is Element of AutGroup G by GROUP_2:42;
  then consider x1, y1 be Element of AutGroup G such that
A1: x1 = x & y1 = y;
  f is Element of Aut G & g is Element of Aut G by Th12;
  then consider f1, g1 be Element of Aut G such that
A2: f1 = f & g1 = g;
  assume x = f & y = g;
  then x1 * y1 = f1 * g1 by A2,A1,Def2;
  hence thesis by A2,A1,GROUP_2:43;
end;

theorem Th19:
  id the carrier of G = 1_InnAutGroup G
proof
  id the carrier of G = 1_AutGroup G by Th9;
  hence thesis by GROUP_2:44;
end;

theorem
  for f being Element of InnAut G for g being Element of InnAutGroup G
  st f = g holds f" = g"
proof
  let f be Element of InnAut G;
  let g be Element of InnAutGroup G;
  g is Element of AutGroup G by GROUP_2:42;
  then consider g1 be Element of AutGroup G such that
A1: g1 = g;
  f is Element of Aut G by Th12;
  then consider f1 be Element of Aut G such that
A2: f1 = f;
  assume f = g;
  then f1" = g1" by A2,A1,Th10;
  hence thesis by A2,A1,GROUP_2:48;
end;

definition
  let G, b;
  func Conjugate b -> Element of InnAut G means
  :Def6:
  for a holds it.a = a |^ b;
  existence
  proof
    deffunc F(Element of G) = ($1) |^ b;
    consider g be Function of the carrier of G, the carrier of G such that
A1: for a holds g.a = F(a) from FUNCT_2:sch 4;
    g is Element of Funcs (the carrier of G, the carrier of G) by FUNCT_2:8;
    then reconsider g as Element of InnAut G by A1,Def4;
    take g;
    let a;
    thus thesis by A1;
  end;
  uniqueness
  proof
    let f1, f2 be Element of InnAut G such that
A2: for a holds f1.a = a |^ b and
A3: for a holds f2.a = a |^ b;
    for a holds f1.a = f2.a
    proof
      let a;
      thus f1.a = a |^ b by A2
        .= f2.a by A3;
    end;
    hence f1 = f2 by FUNCT_2:63;
  end;
end;

theorem Th21:
  for a, b holds Conjugate (a * b) = (Conjugate b) * (Conjugate a)
proof
  let a, b;
  set f1 = Conjugate (a * b);
  set f2 = ((Conjugate b) * (Conjugate a));
A1: for c holds f1.c = c |^ a |^ b
  proof
    let c;
    c |^ (a * b) = c |^ a |^ b by GROUP_3:24;
    hence thesis by Def6;
  end;
A2: for c holds f1.c = (Conjugate b).(c |^ a)
  proof
    let c;
    c |^ a |^ b = (Conjugate b).(c |^ a) by Def6;
    hence thesis by A1;
  end;
A3: for c holds f1.c = (Conjugate b).((Conjugate a).c)
  proof
    let c;
    (Conjugate b).(c |^ a) = (Conjugate b).((Conjugate a).c) by Def6;
    hence thesis by A2;
  end;
  for c holds f1.c = f2.c
  proof
    let c;
    (Conjugate b).((Conjugate a).c) = f2.c by FUNCT_2:15;
    hence thesis by A3;
  end;
  hence thesis by FUNCT_2:63;
end;

theorem Th22:
  Conjugate 1_G = id the carrier of G
proof
  for a holds (Conjugate 1_G).a = a
  proof
    let a;
    a |^ 1_G = a by GROUP_3:19;
    hence thesis by Def6;
  end;
  then
A1: for q st q in the carrier of G holds (Conjugate 1_G).q = q;
  Conjugate 1_G is Element of Aut G by Th12;
  then dom (Conjugate 1_G) = the carrier of G by Lm3;
  hence thesis by A1,FUNCT_1:17;
end;

theorem Th23:
  for a holds (Conjugate 1_G).a = a
proof
  let a;
  thus (Conjugate 1_G).a = a |^ 1_G by Def6
    .= a by GROUP_3:19;
end;

theorem
  for a holds (Conjugate a) * (Conjugate a") = Conjugate 1_G
proof
  let a;
  set f1 = (Conjugate a) * (Conjugate a");
  set f2 = Conjugate 1_G;
A1: for b holds f1.b = b
  proof
    let b;
    (Conjugate a).((Conjugate a").b) = (Conjugate a).(b |^ a") by Def6
      .= b |^ a" |^ a by Def6
      .= b by GROUP_3:25;
    hence thesis by FUNCT_2:15;
  end;
  for b holds f1.b = f2.b
  proof
    let b;
    thus f1.b = b by A1
      .= f2.b by Th23;
  end;
  hence thesis by FUNCT_2:63;
end;

theorem Th25:
  for a holds (Conjugate a") * (Conjugate a) = Conjugate 1_G
proof
  let a;
  set f1 = (Conjugate a") * (Conjugate a);
  set f2 = Conjugate 1_G;
A1: for b holds f1.b = b
  proof
    let b;
    (Conjugate a").((Conjugate a).b) = (Conjugate a").(b |^ a) by Def6
      .= b |^ a |^ a" by Def6
      .= b by GROUP_3:25;
    hence thesis by FUNCT_2:15;
  end;
  for b holds f1.b = f2.b
  proof
    let b;
    thus f1.b = b by A1
      .= f2.b by Th23;
  end;
  hence thesis by FUNCT_2:63;
end;

theorem
  for a holds Conjugate a" = (Conjugate a)"
proof
  let a;
  set f = Conjugate a;
  set g = Conjugate a";
A1: g * f = Conjugate 1_G by Th25
    .= id the carrier of G by Th22;
A2: f is Element of Aut G by Th12;
  then f is Homomorphism of G, G by Def1;
  then
A3: f is one-to-one by A2,Def1;
  rng f = dom f by A2,Lm3
    .= the carrier of G by A2,Lm3;
  hence thesis by A1,A3,FUNCT_2:30;
end;

theorem
  for a holds (Conjugate a) * (Conjugate 1_G) = Conjugate a & (Conjugate
  1_G) * (Conjugate a) = Conjugate a
proof
  let a;
  Conjugate 1_G = id the carrier of G by Th22;
  hence thesis by FUNCT_2:17;
end;

theorem
  for f being Element of InnAut G holds f * Conjugate 1_G = f & (
  Conjugate 1_G) * f = f
proof
  let f be Element of InnAut G;
  Conjugate 1_G = id the carrier of G by Th22;
  hence thesis by FUNCT_2:17;
end;

theorem
  for G holds InnAutGroup G, G./.center G are_isomorphic
proof
  let G;
  deffunc F(Element of G) = Conjugate ($1)";
  consider f be Function of the carrier of G, InnAut G such that
A1: for a holds f.a = F(a) from FUNCT_2:sch 4;
  reconsider f as Function of the carrier of G, the carrier of InnAutGroup G
  by Def5;
  now
    let a,b;
A2: f.(a * b) = Conjugate (a * b)" by A1
      .= Conjugate (b" * a") by GROUP_1:17
      .= (Conjugate a") * (Conjugate b") by Th21;
    now
      let A, B be Element of InnAutGroup G;
      assume
A3:   A = f.a & B = f.b;
      then A = Conjugate a" & B = Conjugate b" by A1;
      hence f.(a * b) = f.a * f.b by A2,A3,Th18;
    end;
    hence f.(a * b) = f.a * f.b;
  end;
  then reconsider f1 = f as Homomorphism of G, InnAutGroup G by GROUP_6:def 6;
A4: Ker f1 = center G
  proof
    set C = { a : for b holds a * b = b * a };
    set KER = the carrier of Ker f1;
A5: KER = { a : f1.a = 1_InnAutGroup G } by GROUP_6:def 9;
A6: KER c= C
    proof
      let q;
      assume
A7:   q in KER;
      1_InnAutGroup G = id the carrier of G by Th19;
      then consider x such that
A8:   q = x and
A9:   f1.x = id the carrier of G by A5,A7;
A10:  for b holds (Conjugate x").b = b
      proof
        let b;
        (id the carrier of G).b = b by FUNCT_1:18;
        hence thesis by A1,A9;
      end;
A11:  for b holds b |^ x" = b
      proof
        let b;
        (Conjugate x").b = b |^ x" by Def6;
        hence thesis by A10;
      end;
      for b holds x * b = b * x
      proof
        let b;
        b |^ x" = x * b * x";
        then x * b * x" * x = b * x by A11;
        then x * b * (x" * x) = b * x by GROUP_1:def 3;
        then x * b * 1_G = b * x by GROUP_1:def 5;
        hence thesis by GROUP_1:def 4;
      end;
      hence thesis by A8;
    end;
    C c= KER
    proof
      let q;
      assume q in C;
      then consider x such that
A12:  x = q and
A13:  for b holds x * b = b * x;
      consider g be Function of the carrier of G, the carrier of G such that
A14:  g = Conjugate x";
A15:  for b holds b = (Conjugate x").b
      proof
        let b;
        x * b * x" = b * x * x" by A13;
        then x * b * x" = b * (x * x") by GROUP_1:def 3;
        then x * b * x" = b * 1_G by GROUP_1:def 5;
        then b = b |^ x" by GROUP_1:def 4;
        hence thesis by Def6;
      end;
      for b holds (id the carrier of G).b = g.b
      proof
        let b;
        b = g.b by A15,A14;
        hence thesis by FUNCT_1:18;
      end;
      then g = id the carrier of G by FUNCT_2:63;
      then Conjugate x" = 1_InnAutGroup G by A14,Th19;
      then f1.x = 1_InnAutGroup G by A1;
      hence thesis by A5,A12;
    end;
    then KER = C by A6,XBOOLE_0:def 10;
    hence thesis by GROUP_5:def 10;
  end;
A16: the carrier of InnAutGroup G = InnAut G by Def5;
  for q st q in the carrier of InnAutGroup G ex q1 st q1 in the carrier
  of G & q = f1.q1
  proof
    let q;
    assume
A17: q in the carrier of InnAutGroup G;
    then
A18: q is Element of InnAut G by Def5;
    then consider
    y1 be Function of the carrier of G, the carrier of G such that
A19: y1 = q;
    y1 is Element of Funcs (the carrier of G, the carrier of G) by FUNCT_2:9;
    then consider b such that
A20: for a holds y1.a = a |^ b by A16,A17,A19,Def4;
    take q1 = b";
    thus q1 in the carrier of G;
    f1.q1 = Conjugate b"" by A1
      .= Conjugate b;
    hence thesis by A18,A19,A20,Def6;
  end;
  then rng f1 = the carrier of InnAutGroup G by FUNCT_2:10;
  then f1 is onto by FUNCT_2:def 3;
  then InnAutGroup G = Image f1 by GROUP_6:57;
  hence thesis by A4,GROUP_6:78;
end;

theorem
  for G holds ( G is commutative Group implies for f being Element of
  InnAutGroup G holds f = 1_InnAutGroup G )
proof
  let G;
  assume
A1: G is commutative Group;
  let f be Element of InnAutGroup G;
  the carrier of InnAutGroup G = InnAut G by Def5;
  then consider f1 be Element of InnAut G such that
A2: f1 = f;
  f1 is Element of Funcs (the carrier of G, the carrier of G) by FUNCT_2:8;
  then consider a such that
A3: for x holds f1.x = x |^ a by Def4;
A4: for x holds f1.x = x
  proof
    let x;
    thus f1.x = x |^ a by A3
      .= x by A1,GROUP_3:29;
  end;
  for x holds f1.x = (id the carrier of G).x
  proof
    let x;
    thus f1.x = x by A4
      .= (id the carrier of G).x by FUNCT_1:18;
  end;
  then f1 = id the carrier of G by FUNCT_2:63;
  hence thesis by A2,Th19;
end;