autgroup.miz



    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 be object;

          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 :: AUTGROUP:1

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

    definition

      let G;

      :: AUTGROUP:def1

      func Aut G -> FUNCTION_DOMAIN of the carrier of G, the carrier of G means

      : Def1: (for f be 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 be 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;

          hence thesis by A2;

        end;

        reconsider X as set;

        X is functional

        proof

          let q be object;

          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 be 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 be 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 be 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 be 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 be object;

          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 be object;

          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 :: AUTGROUP:2

    ( Aut G) c= ( Funcs (the carrier of G,the carrier of G))

    proof

      let q be object;

      assume q in ( Aut G);

      then ex f be Element of ( Aut G) st f = q;

      hence thesis by FUNCT_2: 9;

    end;

    theorem :: AUTGROUP:3

    

     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;

      hence thesis by A1, Def1;

    end;

    theorem :: AUTGROUP:4

    

     Th4: for h holds h in ( Aut G) iff h is bijective by Def1;

    

     Lm3: for f be 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 :: AUTGROUP:5

    

     Th5: for f be 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 :: AUTGROUP:6

    

     Th6: for f be 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 :: AUTGROUP:7

    

     Th7: for f1,f2 be 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;

      :: AUTGROUP:def2

      func AutComp G -> BinOp of ( Aut G) means

      : Def2: for x,y be 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 be Element of ( Aut G) holds ex m be 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 be BinOp of ( Aut G) st for x,y be 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;

      end;

    end

    definition

      let G;

      :: AUTGROUP:def3

      func AutGroup G -> strict Group equals multMagma (# ( Aut G), ( AutComp G) #);

      coherence

      proof

        set H = multMagma (# ( Aut G), ( AutComp G) #);

        

         A1: ex e be Element of H st for h be Element of H holds (h * e) = h & (e * h) = h & ex g be 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;

          

          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 be 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, GROUP_1:def 3;

      end;

    end

    theorem :: AUTGROUP:8

    for x,y be Element of ( AutGroup G) holds for f,g be Element of ( Aut G) st x = f & y = g holds (x * y) = (f * g) by Def2;

    theorem :: AUTGROUP:9

    

     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 :: AUTGROUP:10

    

     Th10: for f be Element of ( Aut G) holds for g be 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;

      :: AUTGROUP:def4

      func InnAut G -> FUNCTION_DOMAIN of the carrier of G, the carrier of G means

      : Def4: for f be 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 be 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

          .= (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 object;

          assume h in X;

          then ex f be 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 be 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 be 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 be 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 be 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 be object;

          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 be object;

          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 :: AUTGROUP:11

    ( InnAut G) c= ( Funcs (the carrier of G,the carrier of G))

    proof

      let q be object;

      assume q in ( InnAut G);

      then ex f be Element of ( InnAut G) st f = q;

      hence thesis by FUNCT_2: 9;

    end;

    theorem :: AUTGROUP:12

    

     Th12: for f be 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 be object;

        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 be object st q in the carrier of G holds ex q1 be object st q1 in ( dom f) & q = (f . q1)

      proof

        let q be object;

        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 be 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;

      hence thesis by A3, Def1;

    end;

    theorem :: AUTGROUP:13

    

     Th13: ( InnAut G) c= ( Aut G)

    proof

      let q be object;

      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;

    theorem :: AUTGROUP:14

    

     Th14: for f,g be 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 :: AUTGROUP:15

    

     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

        .= (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 :: AUTGROUP:16

    

     Th16: for f be 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;

      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 :: AUTGROUP:17

    

     Th17: for f,g be 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 be Element of G holds (g . x2) = (x2 |^ c) by A1, Def4;

        consider b such that

         A5: for x1 be 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;

      :: AUTGROUP:def5

      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 object 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 be 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 be Element of IG st for h be Element of IG holds (h * e) = h & (e * h) = h & ex g be 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;

          

          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, GROUP_1: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 be 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

              .= (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 :: AUTGROUP:18

    

     Th18: for x,y be Element of ( InnAutGroup G) holds for f,g be 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 :: AUTGROUP:19

    

     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 :: AUTGROUP:20

    for f be Element of ( InnAut G) holds for g be 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;

      :: AUTGROUP:def6

      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;

      end;

    end

    theorem :: AUTGROUP:21

    

     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;

    end;

    theorem :: AUTGROUP:22

    

     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 be object st q in the carrier of G holds (( Conjugate ( 1_ G)) . q) = q;

      thus thesis by A1;

    end;

    theorem :: AUTGROUP:23

    

     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 :: AUTGROUP:24

    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;

    end;

    theorem :: AUTGROUP:25

    

     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;

    end;

    theorem :: AUTGROUP:26

    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 :: AUTGROUP:27

    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 :: AUTGROUP:28

    for f be 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 :: AUTGROUP:29

    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 be object;

          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;

            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 be object;

          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) by A15, A14;

          then g = ( id the carrier of G);

          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 be object st q in the carrier of ( InnAutGroup G) holds ex q1 be object st q1 in the carrier of G & q = (f1 . q1)

      proof

        let q be object;

        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;

      then ( InnAutGroup G) = ( Image f1) by GROUP_6: 57;

      hence thesis by A4, GROUP_6: 78;

    end;

    theorem :: AUTGROUP:30

    for G holds (G is commutative Group implies for f be 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) by A4;

      then f1 = ( id the carrier of G);

      hence thesis by A2, Th19;

    end;