:: AUTGROUP semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

Lm1: for G being strict Group
for H being Subgroup of G st ( for a, b being Element of G st b is Element of H holds
b |^ a in H ) holds
H is normal
proof end;

Lm2: for G being strict Group
for H being Subgroup of G st H is normal holds
for a, b being Element of G st b is Element of H holds
b |^ a in H
proof end;

theorem :: AUTGROUP:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being strict Group
for H being Subgroup of G holds
( ( for a, b being Element of G st b is Element of H holds
b |^ a in H ) iff H is normal ) by Lm1, Lm2;

definition
let G be strict Group;
func Aut G -> FUNCTION_DOMAIN of the carrier of G,the carrier of G means :Def1: :: AUTGROUP:def 1
( ( for f being Element of it holds f is Homomorphism of G,G ) & ( for h being Homomorphism of G,G holds
( h in it iff ( h is one-to-one & h is_epimorphism ) ) ) );
existence
ex b1 being FUNCTION_DOMAIN of the carrier of G,the carrier of G st
( ( for f being Element of b1 holds f is Homomorphism of G,G ) & ( for h being Homomorphism of G,G holds
( h in b1 iff ( h is one-to-one & h is_epimorphism ) ) ) )
proof end;
uniqueness
for b1, b2 being FUNCTION_DOMAIN of the carrier of G,the carrier of G st ( for f being Element of b1 holds f is Homomorphism of G,G ) & ( for h being Homomorphism of G,G holds
( h in b1 iff ( h is one-to-one & h is_epimorphism ) ) ) & ( for f being Element of b2 holds f is Homomorphism of G,G ) & ( for h being Homomorphism of G,G holds
( h in b2 iff ( h is one-to-one & h is_epimorphism ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def1 defines Aut AUTGROUP:def 1 :
for G being strict Group
for b2 being FUNCTION_DOMAIN of the carrier of G,the carrier of G holds
( b2 = Aut G iff ( ( for f being Element of b2 holds f is Homomorphism of G,G ) & ( for h being Homomorphism of G,G holds
( h in b2 iff ( h is one-to-one & h is_epimorphism ) ) ) ) );

theorem :: AUTGROUP:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: AUTGROUP:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being strict Group holds Aut G c= Funcs the carrier of G,the carrier of G
proof end;

theorem Th4: :: AUTGROUP:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being strict Group holds id the carrier of G is Element of Aut G
proof end;

theorem Th5: :: AUTGROUP:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being strict Group
for h being Homomorphism of G,G holds
( h in Aut G iff h is_isomorphism )
proof end;

Lm3: for G being strict Group
for f being Element of Aut G holds
( dom f = rng f & dom f = the carrier of G )
proof end;

theorem Th6: :: AUTGROUP:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being strict Group
for f being Element of Aut G holds f " is Homomorphism of G,G
proof end;

theorem Th7: :: AUTGROUP:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being strict Group
for f being Element of Aut G holds f " is Element of Aut G
proof end;

theorem Th8: :: AUTGROUP:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being strict Group
for f1, f2 being Element of Aut G holds f1 * f2 is Element of Aut G
proof end;

definition
let G be strict Group;
func AutComp G -> BinOp of Aut G means :Def2: :: AUTGROUP:def 2
for x, y being Element of Aut G holds it . x,y = x * y;
existence
ex b1 being BinOp of Aut G st
for x, y being Element of Aut G holds b1 . x,y = x * y
proof end;
uniqueness
for b1, b2 being BinOp of Aut G st ( for x, y being Element of Aut G holds b1 . x,y = x * y ) & ( for x, y being Element of Aut G holds b2 . x,y = x * y ) holds
b1 = b2
proof end;
end;

:: deftheorem Def2 defines AutComp AUTGROUP:def 2 :
for G being strict Group
for b2 being BinOp of Aut G holds
( b2 = AutComp G iff for x, y being Element of Aut G holds b2 . x,y = x * y );

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

:: deftheorem defines AutGroup AUTGROUP:def 3 :
for G being strict Group holds AutGroup G = HGrStr(# (Aut G),(AutComp G) #);

theorem Th9: :: AUTGROUP:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being strict Group
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 Th10: :: AUTGROUP:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being strict Group holds id the carrier of G = 1. (AutGroup G)
proof end;

theorem Th11: :: AUTGROUP:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being strict Group
for f being Element of Aut G
for g being Element of (AutGroup G) st f = g holds
f " = g "
proof end;

definition
let G be strict Group;
func InnAut G -> FUNCTION_DOMAIN of the carrier of G,the carrier of G means :Def4: :: AUTGROUP:def 4
for f being Element of Funcs the carrier of G,the carrier of G holds
( f in it iff ex a being Element of G st
for x being Element of G holds f . x = x |^ a );
existence
ex b1 being FUNCTION_DOMAIN of the carrier of G,the carrier of G st
for f being Element of Funcs the carrier of G,the carrier of G holds
( f in b1 iff ex a being Element of G st
for x being Element of G holds f . x = x |^ a )
proof end;
uniqueness
for b1, b2 being FUNCTION_DOMAIN of the carrier of G,the carrier of G st ( for f being Element of Funcs the carrier of G,the carrier of G holds
( f in b1 iff ex a being Element of G st
for x being Element of G holds f . x = x |^ a ) ) & ( for f being Element of Funcs the carrier of G,the carrier of G holds
( f in b2 iff ex a being Element of G st
for x being Element of G holds f . x = x |^ a ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def4 defines InnAut AUTGROUP:def 4 :
for G being strict Group
for b2 being FUNCTION_DOMAIN of the carrier of G,the carrier of G holds
( b2 = InnAut G iff for f being Element of Funcs the carrier of G,the carrier of G holds
( f in b2 iff ex a being Element of G st
for x being Element of G holds f . x = x |^ a ) );

theorem :: AUTGROUP:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being strict Group holds InnAut G c= Funcs the carrier of G,the carrier of G
proof end;

theorem Th13: :: AUTGROUP:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being strict Group
for f being Element of InnAut G holds f is Element of Aut G
proof end;

theorem Th14: :: AUTGROUP:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being strict Group holds InnAut G c= Aut G
proof end;

theorem Th15: :: AUTGROUP:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being strict Group
for f, g being Element of InnAut G holds (AutComp G) . f,g = f * g
proof end;

theorem Th16: :: AUTGROUP:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being strict Group holds id the carrier of G is Element of InnAut G
proof end;

theorem Th17: :: AUTGROUP:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being strict Group
for f being Element of InnAut G holds f " is Element of InnAut G
proof end;

theorem Th18: :: AUTGROUP:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being strict Group
for f, g being Element of InnAut G holds f * g is Element of InnAut G
proof end;

definition
let G be strict Group;
func InnAutGroup G -> strict normal Subgroup of AutGroup G means :Def5: :: AUTGROUP:def 5
the carrier of it = InnAut G;
existence
ex b1 being strict normal Subgroup of AutGroup G st the carrier of b1 = InnAut G
proof end;
uniqueness
for b1, b2 being strict normal Subgroup of AutGroup G st the carrier of b1 = InnAut G & the carrier of b2 = InnAut G holds
b1 = b2 by GROUP_2:68;
end;

:: deftheorem Def5 defines InnAutGroup AUTGROUP:def 5 :
for G being strict Group
for b2 being strict normal Subgroup of AutGroup G holds
( b2 = InnAutGroup G iff the carrier of b2 = InnAut G );

theorem :: AUTGROUP:19  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th20: :: AUTGROUP:20  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being strict Group
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 end;

theorem Th21: :: AUTGROUP:21  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being strict Group holds id the carrier of G = 1. (InnAutGroup G)
proof end;

theorem :: AUTGROUP:22  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being strict Group
for f being Element of InnAut G
for g being Element of (InnAutGroup G) st f = g holds
f " = g "
proof end;

definition
let G be strict Group;
let b be Element of G;
func Conjugate b -> Element of InnAut G means :Def6: :: AUTGROUP:def 6
for a being Element of G holds it . a = a |^ b;
existence
ex b1 being Element of InnAut G st
for a being Element of G holds b1 . a = a |^ b
proof end;
uniqueness
for b1, b2 being Element of InnAut G st ( for a being Element of G holds b1 . a = a |^ b ) & ( for a being Element of G holds b2 . a = a |^ b ) holds
b1 = b2
proof end;
end;

:: deftheorem Def6 defines Conjugate AUTGROUP:def 6 :
for G being strict Group
for b being Element of G
for b3 being Element of InnAut G holds
( b3 = Conjugate b iff for a being Element of G holds b3 . a = a |^ b );

theorem Th23: :: AUTGROUP:23  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being strict Group
for a, b being Element of G holds Conjugate (a * b) = (Conjugate b) * (Conjugate a)
proof end;

theorem Th24: :: AUTGROUP:24  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being strict Group holds Conjugate (1. G) = id the carrier of G
proof end;

theorem Th25: :: AUTGROUP:25  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being strict Group
for a being Element of G holds (Conjugate (1. G)) . a = a
proof end;

theorem :: AUTGROUP:26  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being strict Group
for a being Element of G holds (Conjugate a) * (Conjugate (a " )) = Conjugate (1. G)
proof end;

theorem Th27: :: AUTGROUP:27  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being strict Group
for a being Element of G holds (Conjugate (a " )) * (Conjugate a) = Conjugate (1. G)
proof end;

theorem :: AUTGROUP:28  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being strict Group
for a being Element of G holds Conjugate (a " ) = (Conjugate a) "
proof end;

theorem :: AUTGROUP:29  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being strict Group
for a being Element of G holds
( (Conjugate a) * (Conjugate (1. G)) = Conjugate a & (Conjugate (1. G)) * (Conjugate a) = Conjugate a )
proof end;

theorem :: AUTGROUP:30  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being strict Group
for f being Element of InnAut G holds
( f * (Conjugate (1. G)) = f & (Conjugate (1. G)) * f = f )
proof end;

theorem :: AUTGROUP:31  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being strict Group holds InnAutGroup G,G ./. (center G) are_isomorphic
proof end;

theorem :: AUTGROUP:32  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being strict Group st G is commutative Group holds
for f being Element of (InnAutGroup G) holds f = 1. (InnAutGroup G)
proof end;