:: AUTGROUP semantic presentation begin 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 let G be strict Group; ::_thesis: 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 let H be Subgroup of G; ::_thesis: ( ( for a, b being Element of G st b is Element of H holds b |^ a in H ) implies H is normal ) assume A1: for a, b being Element of G st b is Element of H holds b |^ a in H ; ::_thesis: H is normal now__::_thesis:_for_a_being_Element_of_G_holds_H_*_a_c=_a_*_H let a be Element of G; ::_thesis: H * a c= a * H thus H * a c= a * H ::_thesis: verum proof set A = carr H; let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in H * a or q in a * H ) assume q in H * a ; ::_thesis: q in a * H then consider b being Element of G 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 carr H by STRUCT_0:def_5; then a * (((a ") * b) * a) in a * (carr H) by GROUP_2:27; then a * ((a ") * (b * a)) in a * (carr H) by GROUP_1:def_3; then (a * (a ")) * (b * a) in a * (carr H) by GROUP_1:def_3; then ((a * (a ")) * b) * a in a * (carr H) by GROUP_1:def_3; then ((1_ G) * b) * a in a * (carr H) by GROUP_1:def_5; hence q in a * H by A2, GROUP_1:def_4; ::_thesis: verum end; end; hence H is normal by GROUP_3:119; ::_thesis: verum 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 let G be strict Group; ::_thesis: 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 let H be Subgroup of G; ::_thesis: ( H is normal implies for a, b being Element of G st b is Element of H holds b |^ a in H ) assume A1: H is normal ; ::_thesis: for a, b being Element of G st b is Element of H holds b |^ a in H set A = carr H; let a, b be Element of G; ::_thesis: ( b is Element of H implies b |^ a in H ) 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 = carr H by GROUP_2:109; then the carrier of (H |^ a) = carr H by GROUP_3:59; then A2: (carr H) |^ a = carr H by GROUP_3:def_6; assume b is Element of H ; ::_thesis: b |^ a in H then (a ") * b in (a ") * (carr H) by GROUP_2:27; then ((a ") * b) * a in ((a ") * (carr H)) * a by GROUP_2:28; then b |^ a in carr H by A2, GROUP_3:50; hence b |^ a in H by STRUCT_0:def_5; ::_thesis: verum end; theorem :: AUTGROUP:1 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 onto ) ) ) ); 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 onto ) ) ) ) proof set X = { x where x is Element of Funcs ( the carrier of G, the carrier of G) : ex h being Homomorphism of G,G st ( x = h & h is one-to-one & h is onto ) } ; A1: id the carrier of G in { x where x is Element of Funcs ( the carrier of G, the carrier of G) : ex h being Homomorphism of G,G st ( x = h & h is one-to-one & h is onto ) } proof set I = id the carrier of G; A2: id the carrier of G in Funcs ( the carrier of G, the carrier of G) by FUNCT_2:8; reconsider I = id the carrier of G 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 id the carrier of G in { x where x is Element of Funcs ( the carrier of G, the carrier of G) : ex h being Homomorphism of G,G st ( x = h & h is one-to-one & h is onto ) } by A2; ::_thesis: verum end; reconsider X = { x where x is Element of Funcs ( the carrier of G, the carrier of G) : ex h being Homomorphism of G,G st ( x = h & h is one-to-one & h is onto ) } as set ; X is functional proof let q be set ; :: according to FUNCT_1:def_13 ::_thesis: ( not q in X or q is set ) assume q in X ; ::_thesis: q is set then ex x being Element of Funcs ( the carrier of G, the carrier of G) st ( q = x & ex h being Homomorphism of G,G st ( h = x & h is one-to-one & h is onto ) ) ; hence q is set ; ::_thesis: verum end; then reconsider X = 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; :: according to FUNCT_2:def_12 ::_thesis: a is Element of bool [: the carrier of G, the carrier of G:] a in X ; then ex x being Element of Funcs ( the carrier of G, the carrier of G) st ( a = x & ex h being Homomorphism of G,G st ( h = x & h is one-to-one & h is onto ) ) ; hence a is Element of bool [: the carrier of G, the carrier of G:] ; ::_thesis: verum end; then reconsider X = X as FUNCTION_DOMAIN of the carrier of G, the carrier of G ; take X ; ::_thesis: ( ( for f being Element of X holds f is Homomorphism of G,G ) & ( for h being Homomorphism of G,G holds ( h in X iff ( h is one-to-one & h is onto ) ) ) ) hereby ::_thesis: for h being Homomorphism of G,G holds ( h in X iff ( h is one-to-one & h is onto ) ) let f be Element of X; ::_thesis: f is Homomorphism of G,G f in X ; then ex x being Element of Funcs ( the carrier of G, the carrier of G) st ( f = x & ex h being Homomorphism of G,G st ( h = x & h is one-to-one & h is onto ) ) ; hence f is Homomorphism of G,G ; ::_thesis: verum end; let x be Homomorphism of G,G; ::_thesis: ( x in X iff ( x is one-to-one & x is onto ) ) hereby ::_thesis: ( x is one-to-one & x is onto implies x in X ) assume x in X ; ::_thesis: ( x is one-to-one & x is onto ) then ex f being Element of Funcs ( the carrier of G, the carrier of G) st ( f = x & ex h being Homomorphism of G,G st ( h = f & h is one-to-one & h is onto ) ) ; hence ( x is one-to-one & x is onto ) ; ::_thesis: verum 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 ) ; ::_thesis: x in X hence x in X by A3; ::_thesis: verum 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 onto ) ) ) & ( 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 onto ) ) ) holds b1 = b2 proof let F1, F2 be FUNCTION_DOMAIN of the carrier of G, the carrier of G; ::_thesis: ( ( for f being Element of F1 holds f is Homomorphism of G,G ) & ( for h being Homomorphism of G,G holds ( h in F1 iff ( h is one-to-one & h is onto ) ) ) & ( for f being Element of F2 holds f is Homomorphism of G,G ) & ( for h being Homomorphism of G,G holds ( h in F2 iff ( h is one-to-one & h is onto ) ) ) implies F1 = F2 ) assume that A4: for f being Element of F1 holds f is Homomorphism of G,G and A5: for h being Homomorphism of G,G 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 being Homomorphism of G,G holds ( h in F2 iff ( h is one-to-one & h is onto ) ) ; ::_thesis: F1 = F2 A8: F2 c= F1 proof let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in F2 or q in F1 ) assume A9: q in F2 ; ::_thesis: q in F1 then reconsider h1 = q as Homomorphism of G,G by A6; ( h1 is one-to-one & h1 is onto ) by A7, A9; hence q in F1 by A5; ::_thesis: verum end; F1 c= F2 proof let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in F1 or q in F2 ) assume A10: q in F1 ; ::_thesis: q in F2 then reconsider h1 = q as Homomorphism of G,G by A4; ( h1 is one-to-one & h1 is onto ) by A5, A10; hence q in F2 by A7; ::_thesis: verum end; hence F1 = F2 by A8, XBOOLE_0:def_10; ::_thesis: verum 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 onto ) ) ) ) ); theorem :: AUTGROUP:2 for G being strict Group holds Aut G c= Funcs ( the carrier of G, the carrier of G) proof let G be strict Group; ::_thesis: Aut G c= Funcs ( the carrier of G, the carrier of G) let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in Aut G or q in Funcs ( the carrier of G, the carrier of G) ) assume q in Aut G ; ::_thesis: q in Funcs ( the carrier of G, the carrier of G) then ex f being Element of Aut G st f = q ; hence q in Funcs ( the carrier of G, the carrier of G) by FUNCT_2:9; ::_thesis: verum end; theorem Th3: :: AUTGROUP:3 for G being strict Group holds id the carrier of G is Element of Aut G proof let G be strict Group; ::_thesis: id the carrier of G is Element of Aut G id the carrier of G is Homomorphism of G,G by GROUP_6:38; then consider h being Homomorphism of G,G 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 id the carrier of G is Element of Aut G by A1, Def1; ::_thesis: verum end; theorem Th4: :: AUTGROUP:4 for G being strict Group for h being Homomorphism of G,G holds ( h in Aut G iff h is bijective ) proof let G be strict Group; ::_thesis: for h being Homomorphism of G,G holds ( h in Aut G iff h is bijective ) let h be Homomorphism of G,G; ::_thesis: ( h in Aut G iff h is bijective ) hereby ::_thesis: ( h is bijective implies h in Aut G ) assume h in Aut G ; ::_thesis: h is bijective then ( h is onto & h is one-to-one ) by Def1; hence h is bijective ; ::_thesis: verum end; thus ( h is bijective implies h in Aut G ) by Def1; ::_thesis: verum 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 let G be strict Group; ::_thesis: for f being Element of Aut G holds ( dom f = rng f & dom f = the carrier of G ) let f be Element of Aut G; ::_thesis: ( dom f = rng f & dom f = the carrier of G ) reconsider f = 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 ( dom f = rng f & dom f = the carrier of G ) by A1, GROUP_6:61; ::_thesis: verum end; theorem Th5: :: AUTGROUP:5 for G being strict Group for f being Element of Aut G holds f " is Homomorphism of G,G proof let G be strict Group; ::_thesis: for f being Element of Aut G holds f " is Homomorphism of G,G let f be Element of Aut G; ::_thesis: f " is Homomorphism of G,G reconsider f = f as Homomorphism of G,G by Def1; f is bijective by Th4; hence f " is Homomorphism of G,G by GROUP_6:62; ::_thesis: verum end; theorem Th6: :: AUTGROUP:6 for G being strict Group for f being Element of Aut G holds f " is Element of Aut G proof let G be strict Group; ::_thesis: for f being Element of Aut G holds f " is Element of Aut G let f be Element of Aut G; ::_thesis: f " is Element of Aut G reconsider f = 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 f " is Element of Aut G by Def1; ::_thesis: verum end; theorem Th7: :: AUTGROUP:7 for G being strict Group for f1, f2 being Element of Aut G holds f1 * f2 is Element of Aut G proof let G be strict Group; ::_thesis: for f1, f2 being Element of Aut G holds f1 * f2 is Element of Aut G let f1, f2 be Element of Aut G; ::_thesis: f1 * f2 is Element of Aut G reconsider f1 = f1, f2 = f2 as Homomorphism of G,G by Def1; ( f1 is bijective & f2 is bijective ) by Th4; then f1 * f2 is bijective ; hence f1 * f2 is Element of Aut G by Th4; ::_thesis: verum 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 defpred S1[ 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 S1[x,y,m] proof let x, y be Element of Aut G; ::_thesis: ex m being Element of Aut G st S1[x,y,m] 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 ; ::_thesis: S1[x,y,m] thus S1[x,y,m] ; ::_thesis: verum end; thus ex M being BinOp of (Aut G) st for x, y being Element of Aut G holds S1[x,y,M . (x,y)] from BINOP_1:sch_3(A1); ::_thesis: verum 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 let b1, b2 be BinOp of (Aut G); ::_thesis: ( ( 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 ) implies b1 = b2 ) assume that A2: for x, y being Element of Aut G holds b1 . (x,y) = x * y and A3: for x, y being Element of Aut G holds b2 . (x,y) = x * y ; ::_thesis: b1 = b2 for x, y being Element of Aut G holds b1 . (x,y) = b2 . (x,y) proof let x, y be Element of Aut G; ::_thesis: b1 . (x,y) = b2 . (x,y) thus b1 . (x,y) = x * y by A2 .= b2 . (x,y) by A3 ; ::_thesis: verum end; hence b1 = b2 by BINOP_1:2; ::_thesis: verum 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 multMagma(# (Aut G),(AutComp G) #); coherence multMagma(# (Aut G),(AutComp G) #) is strict Group proof set H = multMagma(# (Aut G),(AutComp G) #); A1: ex e being Element of multMagma(# (Aut G),(AutComp G) #) st for h being Element of multMagma(# (Aut G),(AutComp G) #) holds ( h * e = h & e * h = h & ex g being Element of multMagma(# (Aut G),(AutComp G) #) st ( h * g = e & g * h = e ) ) proof reconsider e = id the carrier of G as Element of multMagma(# (Aut G),(AutComp G) #) by Th3; take e ; ::_thesis: for h being Element of multMagma(# (Aut G),(AutComp G) #) holds ( h * e = h & e * h = h & ex g being Element of multMagma(# (Aut G),(AutComp G) #) st ( h * g = e & g * h = e ) ) let h be Element of multMagma(# (Aut G),(AutComp G) #); ::_thesis: ( h * e = h & e * h = h & ex g being Element of multMagma(# (Aut G),(AutComp G) #) st ( h * g = e & g * h = e ) ) consider A being 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; ::_thesis: ( e * h = h & ex g being Element of multMagma(# (Aut G),(AutComp G) #) st ( h * g = e & g * h = e ) ) e * h = (id the carrier of G) * A by A2, Def2 .= A by FUNCT_2:17 ; hence e * h = h by A2; ::_thesis: ex g being Element of multMagma(# (Aut G),(AutComp G) #) st ( h * g = e & g * h = e ) reconsider g = A " as Element of multMagma(# (Aut G),(AutComp G) #) by Th6; take g ; ::_thesis: ( h * g = e & g * h = e ) reconsider A = 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 ; ::_thesis: g * h = e thus g * h = (A ") * A by A2, Def2 .= e by A3, A4, FUNCT_2:29 ; ::_thesis: verum end; for f, g, h being Element of multMagma(# (Aut G),(AutComp G) #) holds (f * g) * h = f * (g * h) proof let f, g, h be Element of multMagma(# (Aut G),(AutComp G) #); ::_thesis: (f * g) * h = f * (g * 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 ; ::_thesis: verum end; hence multMagma(# (Aut G),(AutComp G) #) is strict Group by A1, GROUP_1:def_2, GROUP_1:def_3; ::_thesis: verum end; end; :: deftheorem defines AutGroup AUTGROUP:def_3_:_ for G being strict Group holds AutGroup G = multMagma(# (Aut G),(AutComp G) #); theorem :: AUTGROUP:8 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 Th9: :: AUTGROUP:9 for G being strict Group holds id the carrier of G = 1_ (AutGroup G) proof let G be strict Group; ::_thesis: id the carrier of G = 1_ (AutGroup G) set f = the Element of (AutGroup G); reconsider g = id the carrier of G as Element of (AutGroup G) by Th3; consider g1 being Function of the carrier of G, the carrier of G such that A1: g1 = g ; the Element of (AutGroup G) is Homomorphism of G,G by Def1; then consider f1 being Function of the carrier of G, the carrier of G such that A2: f1 = the Element of (AutGroup G) ; ( f1 = the Element of (AutGroup G) & g1 = g implies f1 * g1 = the Element of (AutGroup G) * g ) by Def2; hence id the carrier of G = 1_ (AutGroup G) by A1, A2, FUNCT_2:17, GROUP_1:7; ::_thesis: verum end; theorem Th10: :: AUTGROUP:10 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 let G be strict Group; ::_thesis: for f being Element of Aut G for g being Element of (AutGroup G) st f = g holds f " = g " let f be Element of Aut G; ::_thesis: for g being Element of (AutGroup G) st f = g holds f " = g " let g be Element of (AutGroup G); ::_thesis: ( f = g implies f " = g " ) consider g1 being Element of Aut G such that A1: g1 = g " ; assume f = g ; ::_thesis: 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 f " = g " by A1, A3, A2, FUNCT_2:30; ::_thesis: verum 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 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 being Element of G st for x being Element of G holds f . x = x |^ a } ; A1: ex a being Element of G st for x being Element of G holds (id the carrier of G) . x = x |^ a proof take a = 1_ G; ::_thesis: for x being Element of G holds (id the carrier of G) . x = x |^ a let x be Element of G; ::_thesis: (id the carrier of G) . x = x |^ a A2: a " = 1_ G by GROUP_1:8; thus (id the carrier of G) . x = x by FUNCT_1:18 .= x * a by GROUP_1:def_4 .= x |^ a by A2, GROUP_1:def_4 ; ::_thesis: verum end; id the carrier of G is Element of Funcs ( the carrier of G, the carrier of G) by FUNCT_2:8; then A3: id the carrier of G in { f where f is Element of Funcs ( the carrier of G, the carrier of G) : ex a being Element of G st for x being Element of G holds f . x = x |^ a } by A1; { f where f is Element of Funcs ( the carrier of G, the carrier of G) : ex a being Element of G st for x being Element of G holds f . x = x |^ a } is functional proof let h be set ; :: according to FUNCT_1:def_13 ::_thesis: ( not h in { f where f is Element of Funcs ( the carrier of G, the carrier of G) : ex a being Element of G st for x being Element of G holds f . x = x |^ a } or h is set ) assume h in { f where f is Element of Funcs ( the carrier of G, the carrier of G) : ex a being Element of G st for x being Element of G holds f . x = x |^ a } ; ::_thesis: h is set then ex f being Element of Funcs ( the carrier of G, the carrier of G) st ( f = h & ex a being Element of G st for x being Element of G holds f . x = x |^ a ) ; hence h is set ; ::_thesis: verum end; then reconsider X = { f where f is Element of Funcs ( the carrier of G, the carrier of G) : ex a being Element of G st for x being Element of G holds f . x = x |^ a } 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; :: according to FUNCT_2:def_12 ::_thesis: h is Element of bool [: the carrier of G, the carrier of G:] h in X ; then ex f being Element of Funcs ( the carrier of G, the carrier of G) st ( f = h & ex a being Element of G st for x being Element of G holds f . x = x |^ a ) ; hence h is Element of bool [: the carrier of G, the carrier of G:] ; ::_thesis: verum end; then reconsider X = X as FUNCTION_DOMAIN of the carrier of G, the carrier of G ; take X ; ::_thesis: for f being Element of Funcs ( the carrier of G, the carrier of G) holds ( f in X iff ex a being Element of G st for x being Element of G holds f . x = x |^ a ) let f be Element of Funcs ( the carrier of G, the carrier of G); ::_thesis: ( f in X iff ex a being Element of G st for x being Element of G holds f . x = x |^ a ) hereby ::_thesis: ( ex a being Element of G st for x being Element of G holds f . x = x |^ a implies f in X ) assume f in X ; ::_thesis: ex a being Element of G st for x being Element of G holds f . x = x |^ a then ex f1 being Element of Funcs ( the carrier of G, the carrier of G) st ( f1 = f & ex a being Element of G st for x being Element of G holds f1 . x = x |^ a ) ; hence ex a being Element of G st for x being Element of G holds f . x = x |^ a ; ::_thesis: verum end; thus ( ex a being Element of G st for x being Element of G holds f . x = x |^ a implies f in X ) ; ::_thesis: verum 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 let F1, F2 be FUNCTION_DOMAIN of the carrier of G, the carrier of G; ::_thesis: ( ( for f being Element of Funcs ( the carrier of G, the carrier of G) holds ( f in F1 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 F2 iff ex a being Element of G st for x being Element of G holds f . x = x |^ a ) ) implies F1 = F2 ) assume that A4: for f being Element of Funcs ( the carrier of G, the carrier of G) holds ( f in F1 iff ex a being Element of G st for x being Element of G 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 being Element of G st for x being Element of G holds f . x = x |^ a ) ; ::_thesis: F1 = F2 A6: F2 c= F1 proof let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in F2 or q in F1 ) assume A7: q in F2 ; ::_thesis: 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 being Element of G st for x being Element of G holds b1 . x = x |^ a by A5, A7; hence q in F1 by A4; ::_thesis: verum end; F1 c= F2 proof let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in F1 or q in F2 ) assume A8: q in F1 ; ::_thesis: 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 being Element of G st for x being Element of G holds b1 . x = x |^ a by A4, A8; hence q in F2 by A5; ::_thesis: verum end; hence F1 = F2 by A6, XBOOLE_0:def_10; ::_thesis: verum 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:11 for G being strict Group holds InnAut G c= Funcs ( the carrier of G, the carrier of G) proof let G be strict Group; ::_thesis: InnAut G c= Funcs ( the carrier of G, the carrier of G) let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in InnAut G or q in Funcs ( the carrier of G, the carrier of G) ) assume q in InnAut G ; ::_thesis: q in Funcs ( the carrier of G, the carrier of G) then ex f being Element of InnAut G st f = q ; hence q in Funcs ( the carrier of G, the carrier of G) by FUNCT_2:9; ::_thesis: verum end; theorem Th12: :: AUTGROUP:12 for G being strict Group for f being Element of InnAut G holds f is Element of Aut G proof let G be strict Group; ::_thesis: for f being Element of InnAut G holds f is Element of Aut G let f be Element of InnAut G; ::_thesis: f is Element of Aut G A1: f is Element of Funcs ( the carrier of G, the carrier of G) by FUNCT_2:9; now__::_thesis:_for_x,_y_being_Element_of_G_holds_f_._(x_*_y)_=_(f_._x)_*_(f_._y) let x, y be Element of G; ::_thesis: f . (x * y) = (f . x) * (f . y) consider a being Element of G such that A2: for x being Element of G 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 ; ::_thesis: verum end; then reconsider f = f as Homomorphism of G,G by GROUP_6:def_6; A3: f is one-to-one proof let q be set ; :: according to FUNCT_1:def_4 ::_thesis: for b1 being set holds ( not q in dom f or not b1 in dom f or not f . q = f . b1 or q = b1 ) let q1 be set ; ::_thesis: ( not q in dom f or not q1 in dom f or not f . q = f . q1 or q = q1 ) assume that A4: ( q in dom f & q1 in dom f ) and A5: f . q = f . q1 ; ::_thesis: q = q1 consider x, y being Element of G such that A6: ( x = q & y = q1 ) by A4; consider a being Element of G such that A7: for x being Element of G 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 q = q1 by A6, GROUP_1:def_4; ::_thesis: verum end; for q being set st q in the carrier of G holds ex q1 being set st ( q1 in dom f & q = f . q1 ) proof let q be set ; ::_thesis: ( q in the carrier of G implies ex q1 being set st ( q1 in dom f & q = f . q1 ) ) assume q in the carrier of G ; ::_thesis: ex q1 being set st ( q1 in dom f & q = f . q1 ) then consider y being Element of G such that A8: y = q ; consider a being Element of G such that A9: for x being Element of G holds f . x = x |^ a by A1, Def4; take q1 = (a * y) * (a "); ::_thesis: ( q1 in dom f & q = f . q1 ) 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 ; ::_thesis: q = f . q1 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 q = f . q1 by A8; ::_thesis: verum 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 f is Element of Aut G by A3, Def1; ::_thesis: verum end; theorem Th13: :: AUTGROUP:13 for G being strict Group holds InnAut G c= Aut G proof let G be strict Group; ::_thesis: InnAut G c= Aut G now__::_thesis:_for_q_being_set_st_q_in_InnAut_G_holds_ q_in_Aut_G let q be set ; ::_thesis: ( q in InnAut G implies q in Aut G ) assume q in InnAut G ; ::_thesis: q in Aut G then consider f being Element of InnAut G such that A1: f = q ; f is Element of Aut G by Th12; hence q in Aut G by A1; ::_thesis: verum end; hence InnAut G c= Aut G by TARSKI:def_3; ::_thesis: verum end; theorem Th14: :: AUTGROUP:14 for G being strict Group for f, g being Element of InnAut G holds (AutComp G) . (f,g) = f * g proof let G be strict Group; ::_thesis: for f, g being Element of InnAut G holds (AutComp G) . (f,g) = f * g let f, g be Element of InnAut G; ::_thesis: (AutComp G) . (f,g) = f * g ( f is Element of Aut G & g is Element of Aut G ) by Th12; hence (AutComp G) . (f,g) = f * g by Def2; ::_thesis: verum end; theorem Th15: :: AUTGROUP:15 for G being strict Group holds id the carrier of G is Element of InnAut G proof let G be strict Group; ::_thesis: id the carrier of G is Element of InnAut G set I = id the carrier of G; A1: ex a being Element of G st for x being Element of G holds (id the carrier of G) . x = x |^ a proof take a = 1_ G; ::_thesis: for x being Element of G holds (id the carrier of G) . x = x |^ a let x be Element of G; ::_thesis: (id the carrier of G) . x = x |^ a A2: a " = 1_ G by GROUP_1:8; thus (id the carrier of G) . x = x by FUNCT_1:18 .= x * a by GROUP_1:def_4 .= x |^ a by A2, GROUP_1:def_4 ; ::_thesis: verum end; id the carrier of G is Element of Funcs ( the carrier of G, the carrier of G) by FUNCT_2:8; hence id the carrier of G is Element of InnAut G by A1, Def4; ::_thesis: verum end; theorem Th16: :: AUTGROUP:16 for G being strict Group for f being Element of InnAut G holds f " is Element of InnAut G proof let G be strict Group; ::_thesis: for f being Element of InnAut G holds f " is Element of InnAut G let f be Element of InnAut G; ::_thesis: f " is 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 being Element of Funcs ( the carrier of G, the carrier of G) such that A1: f1 = f ; A2: ex a being Element of G st for x being Element of G holds (f ") . x = x |^ a proof consider b being Element of G such that A3: for y being Element of G holds f1 . y = y |^ b by A1, Def4; take a = b " ; ::_thesis: for x being Element of G holds (f ") . x = x |^ a let x be Element of G; ::_thesis: (f ") . x = x |^ a A4: f1 is Element of Aut G by A1, Th12; then reconsider f1 = f1 as Homomorphism of G,G by Def1; A5: f1 is bijective by A4, Th4; then consider y1 being 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 (f ") . x = x |^ a by A1; ::_thesis: verum 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 being 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 f " is Element of InnAut G by A2, Def4; ::_thesis: verum end; theorem Th17: :: AUTGROUP:17 for G being strict Group for f, g being Element of InnAut G holds f * g is Element of InnAut G proof let G be strict Group; ::_thesis: for f, g being Element of InnAut G holds f * g is Element of InnAut G let f, g be Element of InnAut G; ::_thesis: f * g is 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 being Element of G st for x being Element of G holds (f * g) . x = x |^ a proof consider c being Element of G such that A4: for x2 being Element of G holds g . x2 = x2 |^ c by A1, Def4; consider b being Element of G such that A5: for x1 being Element of G holds f . x1 = x1 |^ b by A2, Def4; take a = c * b; ::_thesis: for x being Element of G holds (f * g) . x = x |^ a let x be Element of G; ::_thesis: (f * g) . x = x |^ a (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 (f * g) . x = x |^ a ; ::_thesis: verum end; f * g is Element of Funcs ( the carrier of G, the carrier of G) by FUNCT_2:9; hence f * g is Element of InnAut G by A3, Def4; ::_thesis: verum 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 reconsider K1 = Aut G as set ; reconsider K2 = InnAut G as Subset of K1 by Th13; for q being set st q in [:K2,K2:] holds (AutComp G) . q in K2 proof let q be set ; ::_thesis: ( q in [:K2,K2:] implies (AutComp G) . q in K2 ) assume q in [:K2,K2:] ; ::_thesis: (AutComp G) . q in K2 then consider x, y being set such that A1: ( x in K2 & y in K2 ) and A2: q = [x,y] by ZFMISC_1:def_2; reconsider x = x, y = 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 (AutComp G) . q in K2 by A3; ::_thesis: verum 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__::_thesis:_for_x,_y_being_Element_of_multMagma(#_(InnAut_G),op_#) for_f,_g_being_Element_of_InnAut_G_st_x_=_f_&_y_=_g_holds_ x_*_y_=_f_*_g let x, y be Element of multMagma(# (InnAut G),op #); ::_thesis: for f, g being Element of InnAut G st x = f & y = g holds x * y = f * g let f, g be Element of InnAut G; ::_thesis: ( x = f & y = g implies x * y = f * g ) A5: [f,g] in [:(InnAut G),(InnAut G):] by ZFMISC_1:def_2; assume ( x = f & y = g ) ; ::_thesis: x * y = f * g hence x * y = (AutComp G) . (f,g) by A5, FUNCT_1:49 .= f * g by Th14 ; ::_thesis: verum end; A6: for f, g, h being Element of multMagma(# (InnAut G),op #) holds (f * g) * h = f * (g * h) proof let f, g, h be Element of multMagma(# (InnAut G),op #); ::_thesis: (f * g) * h = f * (g * h) 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 ; ::_thesis: verum end; ex e being Element of multMagma(# (InnAut G),op #) st for h being Element of multMagma(# (InnAut G),op #) holds ( h * e = h & e * h = h & ex g being Element of multMagma(# (InnAut G),op #) st ( h * g = e & g * h = e ) ) proof reconsider e = id the carrier of G as Element of multMagma(# (InnAut G),op #) by Th15; take e ; ::_thesis: for h being Element of multMagma(# (InnAut G),op #) holds ( h * e = h & e * h = h & ex g being Element of multMagma(# (InnAut G),op #) st ( h * g = e & g * h = e ) ) let h be Element of multMagma(# (InnAut G),op #); ::_thesis: ( h * e = h & e * h = h & ex g being Element of multMagma(# (InnAut G),op #) st ( h * g = e & g * h = e ) ) consider A being 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; ::_thesis: ( e * h = h & ex g being Element of multMagma(# (InnAut G),op #) st ( h * g = e & g * h = e ) ) e * h = (id the carrier of G) * A by A4, A8 .= A by FUNCT_2:17 ; hence e * h = h by A8; ::_thesis: ex g being Element of multMagma(# (InnAut G),op #) st ( h * g = e & g * h = e ) reconsider g = A " as Element of multMagma(# (InnAut G),op #) by Th16; take g ; ::_thesis: ( h * g = e & g * h = e ) reconsider A = A as Element of Aut G by Th12; reconsider A = 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 ; ::_thesis: g * h = e thus g * h = (A ") * A by A4, A8 .= e by A9, A10, FUNCT_2:29 ; ::_thesis: verum end; then reconsider IG = multMagma(# (InnAut G),op #) 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 = 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); ::_thesis: ( k is Element of IG implies k |^ f in IG ) consider f1 being Element of Aut G such that A11: f1 = f ; assume k is Element of IG ; ::_thesis: k |^ f in IG then consider g being 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 being 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 being Element of G such that A14: for x being Element of G 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 being 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__::_thesis:_for_y_being_Element_of_G_holds_(((f1_")_*_g1)_*_f1)_._y_=_y_|^_(A_._a) let y be Element of G; ::_thesis: (((f1 ") * g1) * f1) . y = y |^ (A . a) 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 ; ::_thesis: verum end; hence ((f1 ") * g1) * f1 is Element of InnAut G by A17, Def4; ::_thesis: verum end; then A20: ((f1 ") * g) * f1 in InnAut G by A13; reconsider C = f1 " as Element of Aut G by Th6; consider q being set 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 k |^ f in IG by A21, STRUCT_0:def_5; ::_thesis: verum end; then reconsider IG = IG as strict normal Subgroup of AutGroup G by Lm1; take IG ; ::_thesis: the carrier of IG = InnAut G thus the carrier of IG = InnAut G ; ::_thesis: verum 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:59; 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 Th18: :: AUTGROUP:18 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 let G be strict Group; ::_thesis: 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 let x, y be Element of (InnAutGroup G); ::_thesis: for f, g being Element of InnAut G st x = f & y = g holds x * y = f * g let f, g be Element of InnAut G; ::_thesis: ( x = f & y = g implies x * y = f * g ) ( x is Element of (AutGroup G) & y is Element of (AutGroup G) ) by GROUP_2:42; then consider x1, y1 being 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 being Element of Aut G such that A2: ( f1 = f & g1 = g ) ; assume ( x = f & y = g ) ; ::_thesis: x * y = f * g then x1 * y1 = f1 * g1 by A2, A1, Def2; hence x * y = f * g by A2, A1, GROUP_2:43; ::_thesis: verum end; theorem Th19: :: AUTGROUP:19 for G being strict Group holds id the carrier of G = 1_ (InnAutGroup G) proof let G be strict Group; ::_thesis: id the carrier of G = 1_ (InnAutGroup G) id the carrier of G = 1_ (AutGroup G) by Th9; hence id the carrier of G = 1_ (InnAutGroup G) by GROUP_2:44; ::_thesis: verum end; theorem :: AUTGROUP:20 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 let G be strict Group; ::_thesis: for f being Element of InnAut G for g being Element of (InnAutGroup G) st f = g holds f " = g " let f be Element of InnAut G; ::_thesis: for g being Element of (InnAutGroup G) st f = g holds f " = g " let g be Element of (InnAutGroup G); ::_thesis: ( f = g implies f " = g " ) g is Element of (AutGroup G) by GROUP_2:42; then consider g1 being Element of (AutGroup G) such that A1: g1 = g ; f is Element of Aut G by Th12; then consider f1 being Element of Aut G such that A2: f1 = f ; assume f = g ; ::_thesis: f " = g " then f1 " = g1 " by A2, A1, Th10; hence f " = g " by A2, A1, GROUP_2:48; ::_thesis: verum 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 deffunc H1( Element of G) -> Element of the carrier of G = \$1 |^ b; consider g being Function of the carrier of G, the carrier of G such that A1: for a being Element of G holds g . a = H1(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 = g as Element of InnAut G by A1, Def4; take g ; ::_thesis: for a being Element of G holds g . a = a |^ b let a be Element of G; ::_thesis: g . a = a |^ b thus g . a = a |^ b by A1; ::_thesis: verum 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 let f1, f2 be Element of InnAut G; ::_thesis: ( ( for a being Element of G holds f1 . a = a |^ b ) & ( for a being Element of G holds f2 . a = a |^ b ) implies f1 = f2 ) assume that A2: for a being Element of G holds f1 . a = a |^ b and A3: for a being Element of G holds f2 . a = a |^ b ; ::_thesis: f1 = f2 for a being Element of G holds f1 . a = f2 . a proof let a be Element of G; ::_thesis: f1 . a = f2 . a thus f1 . a = a |^ b by A2 .= f2 . a by A3 ; ::_thesis: verum end; hence f1 = f2 by FUNCT_2:63; ::_thesis: verum 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 Th21: :: AUTGROUP:21 for G being strict Group for a, b being Element of G holds Conjugate (a * b) = (Conjugate b) * (Conjugate a) proof let G be strict Group; ::_thesis: for a, b being Element of G holds Conjugate (a * b) = (Conjugate b) * (Conjugate a) let a, b be Element of G; ::_thesis: Conjugate (a * b) = (Conjugate b) * (Conjugate a) set f1 = Conjugate (a * b); set f2 = (Conjugate b) * (Conjugate a); A1: for c being Element of G holds (Conjugate (a * b)) . c = (c |^ a) |^ b proof let c be Element of G; ::_thesis: (Conjugate (a * b)) . c = (c |^ a) |^ b c |^ (a * b) = (c |^ a) |^ b by GROUP_3:24; hence (Conjugate (a * b)) . c = (c |^ a) |^ b by Def6; ::_thesis: verum end; A2: for c being Element of G holds (Conjugate (a * b)) . c = (Conjugate b) . (c |^ a) proof let c be Element of G; ::_thesis: (Conjugate (a * b)) . c = (Conjugate b) . (c |^ a) (c |^ a) |^ b = (Conjugate b) . (c |^ a) by Def6; hence (Conjugate (a * b)) . c = (Conjugate b) . (c |^ a) by A1; ::_thesis: verum end; A3: for c being Element of G holds (Conjugate (a * b)) . c = (Conjugate b) . ((Conjugate a) . c) proof let c be Element of G; ::_thesis: (Conjugate (a * b)) . c = (Conjugate b) . ((Conjugate a) . c) (Conjugate b) . (c |^ a) = (Conjugate b) . ((Conjugate a) . c) by Def6; hence (Conjugate (a * b)) . c = (Conjugate b) . ((Conjugate a) . c) by A2; ::_thesis: verum end; for c being Element of G holds (Conjugate (a * b)) . c = ((Conjugate b) * (Conjugate a)) . c proof let c be Element of G; ::_thesis: (Conjugate (a * b)) . c = ((Conjugate b) * (Conjugate a)) . c (Conjugate b) . ((Conjugate a) . c) = ((Conjugate b) * (Conjugate a)) . c by FUNCT_2:15; hence (Conjugate (a * b)) . c = ((Conjugate b) * (Conjugate a)) . c by A3; ::_thesis: verum end; hence Conjugate (a * b) = (Conjugate b) * (Conjugate a) by FUNCT_2:63; ::_thesis: verum end; theorem Th22: :: AUTGROUP:22 for G being strict Group holds Conjugate (1_ G) = id the carrier of G proof let G be strict Group; ::_thesis: Conjugate (1_ G) = id the carrier of G for a being Element of G holds (Conjugate (1_ G)) . a = a proof let a be Element of G; ::_thesis: (Conjugate (1_ G)) . a = a a |^ (1_ G) = a by GROUP_3:19; hence (Conjugate (1_ G)) . a = a by Def6; ::_thesis: verum end; then A1: for q being set 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 Conjugate (1_ G) = id the carrier of G by A1, FUNCT_1:17; ::_thesis: verum end; theorem Th23: :: AUTGROUP:23 for G being strict Group for a being Element of G holds (Conjugate (1_ G)) . a = a proof let G be strict Group; ::_thesis: for a being Element of G holds (Conjugate (1_ G)) . a = a let a be Element of G; ::_thesis: (Conjugate (1_ G)) . a = a thus (Conjugate (1_ G)) . a = a |^ (1_ G) by Def6 .= a by GROUP_3:19 ; ::_thesis: verum end; theorem :: AUTGROUP:24 for G being strict Group for a being Element of G holds (Conjugate a) * (Conjugate (a ")) = Conjugate (1_ G) proof let G be strict Group; ::_thesis: for a being Element of G holds (Conjugate a) * (Conjugate (a ")) = Conjugate (1_ G) let a be Element of G; ::_thesis: (Conjugate a) * (Conjugate (a ")) = Conjugate (1_ G) set f1 = (Conjugate a) * (Conjugate (a ")); set f2 = Conjugate (1_ G); A1: for b being Element of G holds ((Conjugate a) * (Conjugate (a "))) . b = b proof let b be Element of G; ::_thesis: ((Conjugate a) * (Conjugate (a "))) . b = b (Conjugate a) . ((Conjugate (a ")) . b) = (Conjugate a) . (b |^ (a ")) by Def6 .= (b |^ (a ")) |^ a by Def6 .= b by GROUP_3:25 ; hence ((Conjugate a) * (Conjugate (a "))) . b = b by FUNCT_2:15; ::_thesis: verum end; for b being Element of G holds ((Conjugate a) * (Conjugate (a "))) . b = (Conjugate (1_ G)) . b proof let b be Element of G; ::_thesis: ((Conjugate a) * (Conjugate (a "))) . b = (Conjugate (1_ G)) . b thus ((Conjugate a) * (Conjugate (a "))) . b = b by A1 .= (Conjugate (1_ G)) . b by Th23 ; ::_thesis: verum end; hence (Conjugate a) * (Conjugate (a ")) = Conjugate (1_ G) by FUNCT_2:63; ::_thesis: verum end; theorem Th25: :: AUTGROUP:25 for G being strict Group for a being Element of G holds (Conjugate (a ")) * (Conjugate a) = Conjugate (1_ G) proof let G be strict Group; ::_thesis: for a being Element of G holds (Conjugate (a ")) * (Conjugate a) = Conjugate (1_ G) let a be Element of G; ::_thesis: (Conjugate (a ")) * (Conjugate a) = Conjugate (1_ G) set f1 = (Conjugate (a ")) * (Conjugate a); set f2 = Conjugate (1_ G); A1: for b being Element of G holds ((Conjugate (a ")) * (Conjugate a)) . b = b proof let b be Element of G; ::_thesis: ((Conjugate (a ")) * (Conjugate a)) . b = b (Conjugate (a ")) . ((Conjugate a) . b) = (Conjugate (a ")) . (b |^ a) by Def6 .= (b |^ a) |^ (a ") by Def6 .= b by GROUP_3:25 ; hence ((Conjugate (a ")) * (Conjugate a)) . b = b by FUNCT_2:15; ::_thesis: verum end; for b being Element of G holds ((Conjugate (a ")) * (Conjugate a)) . b = (Conjugate (1_ G)) . b proof let b be Element of G; ::_thesis: ((Conjugate (a ")) * (Conjugate a)) . b = (Conjugate (1_ G)) . b thus ((Conjugate (a ")) * (Conjugate a)) . b = b by A1 .= (Conjugate (1_ G)) . b by Th23 ; ::_thesis: verum end; hence (Conjugate (a ")) * (Conjugate a) = Conjugate (1_ G) by FUNCT_2:63; ::_thesis: verum end; theorem :: AUTGROUP:26 for G being strict Group for a being Element of G holds Conjugate (a ") = (Conjugate a) " proof let G be strict Group; ::_thesis: for a being Element of G holds Conjugate (a ") = (Conjugate a) " let a be Element of G; ::_thesis: Conjugate (a ") = (Conjugate a) " set f = Conjugate a; set g = Conjugate (a "); A1: (Conjugate (a ")) * (Conjugate a) = Conjugate (1_ G) by Th25 .= id the carrier of G by Th22 ; A2: Conjugate a is Element of Aut G by Th12; then Conjugate a is Homomorphism of G,G by Def1; then A3: Conjugate a is one-to-one by A2, Def1; rng (Conjugate a) = dom (Conjugate a) by A2, Lm3 .= the carrier of G by A2, Lm3 ; hence Conjugate (a ") = (Conjugate a) " by A1, A3, FUNCT_2:30; ::_thesis: verum end; theorem :: AUTGROUP:27 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 let G be strict Group; ::_thesis: for a being Element of G holds ( (Conjugate a) * (Conjugate (1_ G)) = Conjugate a & (Conjugate (1_ G)) * (Conjugate a) = Conjugate a ) let a be Element of G; ::_thesis: ( (Conjugate a) * (Conjugate (1_ G)) = Conjugate a & (Conjugate (1_ G)) * (Conjugate a) = Conjugate a ) Conjugate (1_ G) = id the carrier of G by Th22; hence ( (Conjugate a) * (Conjugate (1_ G)) = Conjugate a & (Conjugate (1_ G)) * (Conjugate a) = Conjugate a ) by FUNCT_2:17; ::_thesis: verum end; theorem :: AUTGROUP:28 for G being strict Group for f being Element of InnAut G holds ( f * (Conjugate (1_ G)) = f & (Conjugate (1_ G)) * f = f ) proof let G be strict Group; ::_thesis: for f being Element of InnAut G holds ( f * (Conjugate (1_ G)) = f & (Conjugate (1_ G)) * f = f ) let f be Element of InnAut G; ::_thesis: ( f * (Conjugate (1_ G)) = f & (Conjugate (1_ G)) * f = f ) Conjugate (1_ G) = id the carrier of G by Th22; hence ( f * (Conjugate (1_ G)) = f & (Conjugate (1_ G)) * f = f ) by FUNCT_2:17; ::_thesis: verum end; theorem :: AUTGROUP:29 for G being strict Group holds InnAutGroup G,G ./. (center G) are_isomorphic proof let G be strict Group; ::_thesis: InnAutGroup G,G ./. (center G) are_isomorphic deffunc H1( Element of G) -> Element of InnAut G = Conjugate (\$1 "); consider f being Function of the carrier of G,(InnAut G) such that A1: for a being Element of G holds f . a = H1(a) from FUNCT_2:sch_4(); reconsider f = f as Function of the carrier of G, the carrier of (InnAutGroup G) by Def5; now__::_thesis:_for_a,_b_being_Element_of_G_holds_f_._(a_*_b)_=_(f_._a)_*_(f_._b) let a, b be Element of G; ::_thesis: f . (a * b) = (f . a) * (f . b) A2: f . (a * b) = Conjugate ((a * b) ") by A1 .= Conjugate ((b ") * (a ")) by GROUP_1:17 .= (Conjugate (a ")) * (Conjugate (b ")) by Th21 ; now__::_thesis:_for_A,_B_being_Element_of_(InnAutGroup_G)_st_A_=_f_._a_&_B_=_f_._b_holds_ f_._(a_*_b)_=_(f_._a)_*_(f_._b) let A, B be Element of (InnAutGroup G); ::_thesis: ( A = f . a & B = f . b implies f . (a * b) = (f . a) * (f . b) ) assume A3: ( A = f . a & B = f . b ) ; ::_thesis: f . (a * b) = (f . a) * (f . b) then ( A = Conjugate (a ") & B = Conjugate (b ") ) by A1; hence f . (a * b) = (f . a) * (f . b) by A2, A3, Th18; ::_thesis: verum end; hence f . (a * b) = (f . a) * (f . b) ; ::_thesis: verum 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 where a is Element of G : for b being Element of G holds a * b = b * a } ; set KER = the carrier of (Ker f1); A5: the carrier of (Ker f1) = { a where a is Element of G : f1 . a = 1_ (InnAutGroup G) } by GROUP_6:def_9; A6: the carrier of (Ker f1) c= { a where a is Element of G : for b being Element of G holds a * b = b * a } proof let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in the carrier of (Ker f1) or q in { a where a is Element of G : for b being Element of G holds a * b = b * a } ) assume A7: q in the carrier of (Ker f1) ; ::_thesis: q in { a where a is Element of G : for b being Element of G holds a * b = b * a } 1_ (InnAutGroup G) = id the carrier of G by Th19; then consider x being Element of G such that A8: q = x and A9: f1 . x = id the carrier of G by A5, A7; A10: for b being Element of G holds (Conjugate (x ")) . b = b proof let b be Element of G; ::_thesis: (Conjugate (x ")) . b = b (id the carrier of G) . b = b by FUNCT_1:18; hence (Conjugate (x ")) . b = b by A1, A9; ::_thesis: verum end; A11: for b being Element of G holds b |^ (x ") = b proof let b be Element of G; ::_thesis: b |^ (x ") = b (Conjugate (x ")) . b = b |^ (x ") by Def6; hence b |^ (x ") = b by A10; ::_thesis: verum end; for b being Element of G holds x * b = b * x proof let b be Element of G; ::_thesis: x * b = b * x 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 x * b = b * x by GROUP_1:def_4; ::_thesis: verum end; hence q in { a where a is Element of G : for b being Element of G holds a * b = b * a } by A8; ::_thesis: verum end; { a where a is Element of G : for b being Element of G holds a * b = b * a } c= the carrier of (Ker f1) proof let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in { a where a is Element of G : for b being Element of G holds a * b = b * a } or q in the carrier of (Ker f1) ) assume q in { a where a is Element of G : for b being Element of G holds a * b = b * a } ; ::_thesis: q in the carrier of (Ker f1) then consider x being Element of G such that A12: x = q and A13: for b being Element of G holds x * b = b * x ; consider g being Function of the carrier of G, the carrier of G such that A14: g = Conjugate (x ") ; A15: for b being Element of G holds b = (Conjugate (x ")) . b proof let b be Element of G; ::_thesis: b = (Conjugate (x ")) . 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 b = (Conjugate (x ")) . b by Def6; ::_thesis: verum end; for b being Element of G holds (id the carrier of G) . b = g . b proof let b be Element of G; ::_thesis: (id the carrier of G) . b = g . b b = g . b by A15, A14; hence (id the carrier of G) . b = g . b by FUNCT_1:18; ::_thesis: verum 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 q in the carrier of (Ker f1) by A5, A12; ::_thesis: verum end; then the carrier of (Ker f1) = { a where a is Element of G : for b being Element of G holds a * b = b * a } by A6, XBOOLE_0:def_10; hence Ker f1 = center G by GROUP_5:def_10; ::_thesis: verum end; A16: the carrier of (InnAutGroup G) = InnAut G by Def5; for q being set st q in the carrier of (InnAutGroup G) holds ex q1 being set st ( q1 in the carrier of G & q = f1 . q1 ) proof let q be set ; ::_thesis: ( q in the carrier of (InnAutGroup G) implies ex q1 being set st ( q1 in the carrier of G & q = f1 . q1 ) ) assume A17: q in the carrier of (InnAutGroup G) ; ::_thesis: ex q1 being set st ( q1 in the carrier of G & q = f1 . q1 ) then A18: q is Element of InnAut G by Def5; then consider y1 being 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 being Element of G such that A20: for a being Element of G holds y1 . a = a |^ b by A16, A17, A19, Def4; take q1 = b " ; ::_thesis: ( q1 in the carrier of G & q = f1 . q1 ) thus q1 in the carrier of G ; ::_thesis: q = f1 . q1 f1 . q1 = Conjugate ((b ") ") by A1 .= Conjugate b ; hence q = f1 . q1 by A18, A19, A20, Def6; ::_thesis: verum 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 InnAutGroup G,G ./. (center G) are_isomorphic by A4, GROUP_6:78; ::_thesis: verum end; theorem :: AUTGROUP:30 for G being strict Group st G is commutative Group holds for f being Element of (InnAutGroup G) holds f = 1_ (InnAutGroup G) proof let G be strict Group; ::_thesis: ( G is commutative Group implies for f being Element of (InnAutGroup G) holds f = 1_ (InnAutGroup G) ) assume A1: G is commutative Group ; ::_thesis: for f being Element of (InnAutGroup G) holds f = 1_ (InnAutGroup G) let f be Element of (InnAutGroup G); ::_thesis: f = 1_ (InnAutGroup G) the carrier of (InnAutGroup G) = InnAut G by Def5; then consider f1 being 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 being Element of G such that A3: for x being Element of G holds f1 . x = x |^ a by Def4; A4: for x being Element of G holds f1 . x = x proof let x be Element of G; ::_thesis: f1 . x = x thus f1 . x = x |^ a by A3 .= x by A1, GROUP_3:29 ; ::_thesis: verum end; for x being Element of G holds f1 . x = (id the carrier of G) . x proof let x be Element of G; ::_thesis: f1 . x = (id the carrier of G) . x thus f1 . x = x by A4 .= (id the carrier of G) . x by FUNCT_1:18 ; ::_thesis: verum end; then f1 = id the carrier of G by FUNCT_2:63; hence f = 1_ (InnAutGroup G) by A2, Th19; ::_thesis: verum end;