:: Characteristic Subgroups
:: by Alexander M. Nelson
::
:: Received July 23, 2022
:: Copyright (c) 2022-2025 Association of Mizar Users


theorem Th67a: :: GROUP_22:1
for a, b, c being Nat st c <> 0 & c * a divides c * b holds
a divides b by INT_4:7;

theorem Th68: :: GROUP_22:2
for a, b, c being Nat st b <> 0 & b divides c & a * b,c are_coprime holds
b = 1
proof end;

theorem Th1: :: GROUP_22:3
for G1, G2 being Group
for H being Subgroup of G1
for f being Homomorphism of G1,G2
for h being Element of G1 st h in H holds
(f | H) . h = f . h
proof end;

theorem Th4: :: GROUP_22:4
for X, Y being non empty set
for f being Function of X,Y st f is bijective holds
for y being Element of Y holds f . ((f ") . y) = y
proof end;

theorem Th5: :: GROUP_22:5
for X, Y being non empty set
for A being non empty Subset of X
for x being Element of X st not x in A holds
for f being Function of X,Y st f is one-to-one holds
not f . x in f .: A
proof end;

registration
cluster non empty non trivial strict unital Group-like associative for multMagma ;
existence
ex b1 being Group st
( b1 is strict & not b1 is trivial )
proof end;
end;

registration
let G be Group;
cluster non empty trivial unital Group-like associative for Subgroup of G;
existence
ex b1 being Subgroup of G st b1 is trivial
proof end;
let H be Subgroup of G;
cluster non empty trivial unital Group-like associative for Subgroup of H;
existence
ex b1 being Subgroup of H st b1 is trivial
proof end;
end;

registration
let G be non trivial Group;
cluster non empty non trivial unital Group-like associative for Subgroup of G;
existence
not for b1 being Subgroup of G holds b1 is trivial
proof end;
cluster non empty non trivial strict unital Group-like associative for Subgroup of G;
existence
ex b1 being Subgroup of G st
( b1 is strict & not b1 is trivial )
proof end;
end;

theorem Th6: :: GROUP_22:6
for G being Group holds
( G is trivial iff multMagma(# the carrier of G, the multF of G #) = (1). G )
proof end;

LmFiniteNontrivial: not INT.Group 2 is trivial
proof end;

registration
cluster non empty non trivial finite unital Group-like associative for multMagma ;
existence
not for b1 being finite Group holds b1 is trivial by LmFiniteNontrivial;
end;

theorem Th7: :: GROUP_22:7
for G being Group
for H being Subgroup of G st H is trivial holds
multMagma(# the carrier of H, the multF of H #) = (1). G
proof end;

theorem Th8: :: GROUP_22:8
for G being Group
for H, K being trivial Subgroup of G holds multMagma(# the carrier of H, the multF of H #) = multMagma(# the carrier of K, the multF of K #)
proof end;

theorem Th9: :: GROUP_22:9
for G being Group
for K being trivial Subgroup of G
for H being Subgroup of G st H is Subgroup of K holds
H is trivial Subgroup of G
proof end;

definition
let G be Group;
let IT be Subgroup of G;
attr IT is proper means :Def1: :: GROUP_22:def 1
 multMagma(# the carrier of IT, the multF of IT #) <> multMagma(# the carrier of G, the multF of G #);
end;

:: deftheorem Def1 defines proper GROUP_22:def 1 :
for G being Group
for IT being Subgroup of G holds
( IT is proper iff multMagma(# the carrier of IT, the multF of IT #) <> multMagma(# the carrier of G, the multF of G #) );

theorem Th10: :: GROUP_22:10
for G being Group
for H being Subgroup of G holds
( H is proper iff the carrier of H <> the carrier of G )
proof end;

theorem Th11: :: GROUP_22:11
for G being Group
for H being Subgroup of G holds
( H is proper iff the carrier of G \ the carrier of H is non empty set )
proof end;

registration
let G be non trivial Group;
cluster non empty strict unital Group-like associative proper for Subgroup of G;
existence
ex b1 being Subgroup of G st
( b1 is strict & b1 is proper )
proof end;
end;

registration
let G be non trivial Group;
cluster maximal -> proper for Subgroup of G;
coherence
for b1 being Subgroup of G st b1 is maximal holds
b1 is proper by GROUP_4:def 6;
end;

theorem Th12: :: GROUP_22:12
for G being non trivial Group
for H being proper Subgroup of G
for K being Subgroup of G st H is Subgroup of K & multMagma(# the carrier of H, the multF of H #) <> multMagma(# the carrier of K, the multF of K #) holds
K is non trivial Subgroup of G
proof end;

definition
let G be Group;
mode Endomorphism of G is Homomorphism of G,G;
end;

registration
let G be Group;
cluster non empty Relation-like -defined -valued Function-like total quasi_total bijective unity-preserving multiplicative for Element of K10(K11( the carrier of G, the carrier of G));
existence
ex b1 being Endomorphism of G st b1 is bijective
proof end;
end;

definition
let G be Group;
mode Automorphism of G is bijective Endomorphism of G;
end;

theorem Th13: :: GROUP_22:13
for G being Group
for f being Endomorphism of G holds Image (f | ((1). G)) = (1). G
proof end;

:: In particular, the trivial proper subgroup (1).G of G is invariant
:: under inner automorphisms, and thus is a characteristic subgroup.
theorem Th14: :: GROUP_22:14
for G being Group
for phi being Automorphism of G holds Image (phi | ((1). G)) is Subgroup of (1). G
proof end;

theorem Th15: :: GROUP_22:15
for G1, G2 being Group
for f being Homomorphism of G1,G2
for H being Subgroup of G1 holds Ker (f | H) is Subgroup of Ker f
proof end;

Lm2: for G being Group
for H being Subgroup of G st H is Subgroup of (1). G holds
multMagma(# the carrier of H, the multF of H #) = multMagma(# the carrier of ((1). G), the multF of ((1). G) #)
proof end;

Lm3: for G being Group
for H being Subgroup of G
for phi being Automorphism of G holds
( phi | H is Homomorphism of H,(Image (phi | H)) & phi | H is one-to-one )
proof end;

theorem Th16: :: GROUP_22:16
for G being Group
for H being Subgroup of G
for phi being Automorphism of G st ( for f being Automorphism of G holds Image (f | H) is Subgroup of H ) holds
ex psi being Automorphism of G st
( psi = phi " & Image (phi | (Image (psi | H))) is Subgroup of Image (phi | H) )
proof end;

theorem Th17: :: GROUP_22:17
for G being Group
for H being Subgroup of G
for phi being Automorphism of G ex psi being Automorphism of G st
( psi = phi " & Image (phi | (Image (psi | H))) = multMagma(# the carrier of H, the multF of H #) )
proof end;

theorem Th18: :: GROUP_22:18
for G being Group
for phi being Automorphism of G
for H being strict Subgroup of G
for K being Subgroup of G st Image (phi | H) is Subgroup of K holds
ex psi being Automorphism of G st
( psi = phi " & H is Subgroup of Image (psi | K) )
proof end;

theorem Th19: :: GROUP_22:19
for G being Group
for H being Subgroup of G
for phi being Automorphism of G holds H,phi .: H are_isomorphic
proof end;

theorem Th20: :: GROUP_22:20
for G being finite Group
for H1, H2 being strict Subgroup of G st H1,H2 are_isomorphic holds
index H1 = index H2
proof end;

theorem :: GROUP_22:21
for G being Group
for phi being Automorphism of G st G is finite holds
for p being prime Nat
for P being strict Subgroup of G st P is_Sylow_p-subgroup_of_prime p holds
Image (phi | P) is_Sylow_p-subgroup_of_prime p
proof end;

theorem Th22: :: GROUP_22:22
for G being Group
for H being Subgroup of G
for f being Automorphism of G st Image (f | H) = multMagma(# the carrier of H, the multF of H #) holds
f | H is Automorphism of H
proof end;

theorem Th23: :: GROUP_22:23
for G being non trivial Group
for H being Subgroup of G
for phi being Automorphism of G st H is proper Subgroup of G holds
Image (phi | H) is proper Subgroup of G
proof end;

theorem Th24: :: GROUP_22:24
for G being non trivial Group
for H being strict Subgroup of G
for phi being Automorphism of G st H is maximal holds
Image (phi | H) is maximal
proof end;

definition
let G be Group;
let a be Element of G;
let f be Function;
pred a is_inner_wrt f means :Def2a: :: GROUP_22:def 2
 for x being Element of G holds f . x = x |^ a;
end;

:: deftheorem Def2a defines is_inner_wrt GROUP_22:def 2 :
for G being Group
for a being Element of G
for f being Function holds
( a is_inner_wrt f iff for x being Element of G holds f . x = x |^ a );

definition
let G be Group;
let IT be Automorphism of G;
attr IT is inner means :Def2: :: GROUP_22:def 3
 ex a being Element of G st a is_inner_wrt IT;
end;

:: deftheorem Def2 defines inner GROUP_22:def 3 :
for G being Group
for IT being Automorphism of G holds
( IT is inner iff ex a being Element of G st a is_inner_wrt IT );

notation
let G be Group;
let f be Automorphism of G;
antonym outer f for inner ;
end;

registration
let G be Group;
cluster non empty Relation-like -defined -valued Function-like one-to-one total quasi_total onto bijective unity-preserving multiplicative inner for Element of K10(K11( the carrier of G, the carrier of G));
existence
ex b1 being Automorphism of G st b1 is inner
proof end;
end;

theorem Th26: :: GROUP_22:25
for G being strict Group
for f being object holds
( f in Aut G iff f is Automorphism of G )
proof end;

Lm6: for G being strict Group
for f being Element of InnAut G holds f is Automorphism of G
proof end;

theorem :: GROUP_22:26
for G being strict Group
for f being object holds
( f in InnAut G iff f is inner Automorphism of G )
proof end;

theorem Th28: :: GROUP_22:27
for G being Group
for H being Subgroup of G
for a being Element of G
for f being inner Automorphism of G st a is_inner_wrt f holds
Image (f | H) = H |^ a
proof end;

theorem Th29: :: GROUP_22:28
for G being Group
for a being Element of G
for f being Endomorphism of G st a is_inner_wrt f holds
Ker f = (1). G
proof end;

theorem Th30: :: GROUP_22:29
for G being Group
for a being Element of G
for f being Endomorphism of G st a is_inner_wrt f holds
f is Automorphism of G
proof end;

theorem :: GROUP_22:30
for G being Group
for a being Element of G
for f being Endomorphism of G st a is_inner_wrt f holds
f is inner Automorphism of G by Th30, Def2;

theorem Th32: :: GROUP_22:31
for G being Group
for a being Element of G ex f being inner Automorphism of G st a is_inner_wrt f
proof end;

theorem Th33: :: GROUP_22:32
for G being Group
for H being strict Subgroup of G holds
( H is normal iff for f being inner Automorphism of G holds Image (f | H) = H )
proof end;

:: Dummit and Foote, Abstract Algebra, ch.4 section 4
definition
let G be Group;
let IT be Subgroup of G;
attr IT is characteristic means :Def3: :: GROUP_22:def 4
 for f being Automorphism of G holds Image (f | IT) = multMagma(# the carrier of IT, the multF of IT #);
end;

:: deftheorem Def3 defines characteristic GROUP_22:def 4 :
for G being Group
for IT being Subgroup of G holds
( IT is characteristic iff for f being Automorphism of G holds Image (f | IT) = multMagma(# the carrier of IT, the multF of IT #) );

Lm8: for G being Group
for H being Subgroup of G st H is Subgroup of (1). G holds
multMagma(# the carrier of H, the multF of H #) = multMagma(# the carrier of ((1). G), the multF of ((1). G) #)
proof end;

registration
let G be Group;
cluster (1). G -> characteristic ;
coherence
(1). G is characteristic
proof end;
end;

registration
let G be Group;
cluster non empty unital Group-like associative characteristic for Subgroup of G;
existence
ex b1 being Subgroup of G st b1 is characteristic
proof end;
end;

registration
let G be Group;
cluster non empty strict unital Group-like associative characteristic for Subgroup of G;
existence
ex b1 being Subgroup of G st
( b1 is strict & b1 is characteristic )
proof end;
end;

theorem Th35: :: GROUP_22:33
for G being Group
for K being characteristic Subgroup of G holds K is normal Subgroup of G
proof end;

registration
let G be Group;
cluster characteristic -> normal for Subgroup of G;
coherence
for b1 being Subgroup of G st b1 is characteristic holds
b1 is normal by Th35;
end;

theorem Th36: :: GROUP_22:34
for G1, G2 being Group
for H1 being Subgroup of G1
for K being Subgroup of H1
for H2 being Subgroup of G2
for f being Homomorphism of G1,G2
for g being Homomorphism of H1,H2 st ( for k being Element of G1 st k in K holds
f . k = g . k ) holds
Image (f | K) = Image (g | K)
proof end;

theorem :: GROUP_22:35
for G being Group
for H being strict Subgroup of G st ( for K being strict Subgroup of G st card K = card H holds
H = K ) holds
H is characteristic
proof end;

theorem :: GROUP_22:36
for G being Group
for N being strict normal Subgroup of G
for K being characteristic Subgroup of N holds K is normal Subgroup of G
proof end;

theorem :: GROUP_22:37
for G being Group
for N being characteristic Subgroup of G
for K being characteristic Subgroup of N holds K is characteristic Subgroup of G
proof end;

theorem Th40: :: GROUP_22:38
for G being Group
for H being strict Subgroup of G holds
( H is characteristic Subgroup of G iff for phi being Automorphism of G holds Image (phi | H) is Subgroup of H )
proof end;

theorem :: GROUP_22:39
for G being Group holds center G is characteristic Subgroup of G
proof end;

scheme :: GROUP_22:sch 1
CharMeet{ F1() -> Group, P1[ set ] } :
for phi being Automorphism of F1() holds phi .: (meet { A where A is Subset of F1() : ex K being strict Subgroup of F1() st
( A = the carrier of K & P1[K] ) } ) = meet { A where A is Subset of F1() : ex K being strict Subgroup of F1() st
( A = the carrier of K & P1[K] ) }
provided
A1: for phi being Automorphism of F1()
for H being strict Subgroup of F1() st P1[H] holds
P1[ Image (phi | H)] and
A2: ex H being strict Subgroup of F1() st P1[H]
proof end;

scheme :: GROUP_22:sch 2
MeetIsChar{ F1() -> Group, P1[ set ] } :
ex K being strict Subgroup of F1() st
( the carrier of K = meet { A where A is Subset of F1() : ex H being strict Subgroup of F1() st
( A = the carrier of H & P1[H] ) } & K is characteristic )
provided
A1: for phi being Automorphism of F1()
for H being strict Subgroup of F1() st P1[H] holds
P1[ Image (phi | H)] and
A2: ex H being strict Subgroup of F1() st P1[H]
proof end;

theorem :: GROUP_22:40
for G being non trivial Group st ex H being strict Subgroup of G st H is maximal holds
Phi G is characteristic Subgroup of G
proof end;

theorem Th43: :: GROUP_22:41
for G being Group
for phi being Automorphism of G holds phi .: (commutators G) = commutators G
proof end;

theorem Th44: :: GROUP_22:42
for G being Group
for phi being Automorphism of G
for H being Subgroup of G st ( for h being Element of H holds phi . h in H ) holds
Image (phi | H) is Subgroup of H
proof end;

theorem Th45: :: GROUP_22:43
for G being Group
for A being non empty Subset of G st ( for phi being Automorphism of G holds phi .: A = A ) holds
gr A is characteristic
proof end;

theorem :: GROUP_22:44
for G being Group holds G ` is characteristic
proof end;

theorem Th47: :: GROUP_22:45
for G1, G2 being Group
for H being Subgroup of G1
for a being Element of G1
for f being Homomorphism of G1,G2 holds f .: (a * H) = (f . a) * (f .: H)
proof end;

theorem Th48: :: GROUP_22:46
for G1, G2 being Group
for H being Subgroup of G1
for a being Element of G1
for f being Homomorphism of G1,G2 holds f .: (H * a) = (f .: H) * (f . a)
proof end;

theorem Th49: :: GROUP_22:47
for G being Group
for N being strict normal Subgroup of G
for phi being Automorphism of G holds Image (phi | N) is normal Subgroup of G
proof end;

theorem Th50: :: GROUP_22:48
for G being Group
for H being strict Subgroup of G holds
( H is characteristic iff for phi being Automorphism of G
for x being Element of G st x in H holds
phi . x in H )
proof end;

theorem :: GROUP_22:49
for G being Group
for H, K being strict characteristic Subgroup of G holds H /\ K is characteristic Subgroup of G
proof end;

theorem :: GROUP_22:50
for G being Group
for H, K being strict characteristic Subgroup of G holds H "\/" K is characteristic Subgroup of G
proof end;

theorem Th53: :: GROUP_22:51
for G being Group
for H, K being strict characteristic Subgroup of G
for phi being Automorphism of G holds phi .: (commutators (H,K)) = commutators (H,K)
proof end;

theorem :: GROUP_22:52
for G being Group
for H, K being strict characteristic Subgroup of G holds [.H,K.] is characteristic Subgroup of G
proof end;

scheme :: GROUP_22:sch 3
MeetIsMinimal{ F1() -> Group, P1[ set ] } :
ex H being strict Subgroup of F1() st
( the carrier of H = meet { A where A is Subset of F1() : ex K being strict Subgroup of F1() st
( A = the carrier of K & P1[K] ) } & ( for K being strict Subgroup of F1() st P1[K] holds
H is Subgroup of K ) )
provided
A1: ex H being strict Subgroup of F1() st P1[H]
proof end;

theorem Th55: :: GROUP_22:53
for G being Group
for H1, H2 being Subgroup of G st H1 is Subgroup of H2 holds
for a being Element of G holds H1 |^ a is Subgroup of H2 |^ a
proof end;

scheme :: GROUP_22:sch 4
MeetOfNormsIsNormal{ F1() -> Group, P1[ set ] } :
for H being strict Subgroup of F1() st the carrier of H = meet { A where A is Subset of F1() : ex N being strict Subgroup of F1() st
( A = the carrier of N & N is normal & P1[N] ) } holds
H is strict normal Subgroup of F1()
provided
A1: ex H being strict normal Subgroup of F1() st P1[H]
proof end;

theorem :: GROUP_22:54
for G being Group
for X being finite set st X <> {} & ( for A being Element of X ex N being strict normal Subgroup of G st A = the carrier of N ) holds
ex N being strict normal Subgroup of G st the carrier of N = meet X
proof end;

definition
let G be Group;
let A be Subset of G;
func Centralizer A -> strict Subgroup of G means :Def4: :: GROUP_22:def 5
 the carrier of it = { b where b is Element of G : for a being Element of G st a in A holds
a * b = b * a } ;
existence
ex b1 being strict Subgroup of G st the carrier of b1 = { b where b is Element of G : for a being Element of G st a in A holds
a * b = b * a }
proof end;
uniqueness
for b1, b2 being strict Subgroup of G st the carrier of b1 = { b where b is Element of G : for a being Element of G st a in A holds
a * b = b * a } & the carrier of b2 = { b where b is Element of G : for a being Element of G st a in A holds
a * b = b * a } holds
b1 = b2
proof end;
end;

:: deftheorem Def4 defines Centralizer GROUP_22:def 5 :
for G being Group
for A being Subset of G
for b3 being strict Subgroup of G holds
( b3 = Centralizer A iff the carrier of b3 = { b where b is Element of G : for a being Element of G st a in A holds
a * b = b * a } );

theorem Th57: :: GROUP_22:55
for G being Group
for A being Subset of G
for g being Element of G holds
( ( for a being Element of G st a in A holds
g * a = a * g ) iff g is Element of (Centralizer A) )
proof end;

theorem :: GROUP_22:56
for G being Group
for A, B being Subset of G st A c= B holds
Centralizer B is Subgroup of Centralizer A
proof end;

definition
let G be Group;
let H be Subgroup of G;
func Centralizer H -> strict Subgroup of G means :Def5: :: GROUP_22:def 6
it = Centralizer (carr H);
correctness
existence
ex b1 being strict Subgroup of G st b1 = Centralizer (carr H);
uniqueness
for b1, b2 being strict Subgroup of G st b1 = Centralizer (carr H) & b2 = Centralizer (carr H) holds
b1 = b2;
;
end;

:: deftheorem Def5 defines Centralizer GROUP_22:def 6 :
for G being Group
for H being Subgroup of G
for b3 being strict Subgroup of G holds
( b3 = Centralizer H iff b3 = Centralizer (carr H) );

theorem Th59: :: GROUP_22:57
for G being Group
for H being Subgroup of G holds the carrier of (Centralizer H) = { b where b is Element of G : for a being Element of G st a in H holds
b * a = a * b }
proof end;

theorem Th60: :: GROUP_22:58
for G being Group
for H being Subgroup of G
for g being Element of G holds
( ( for a being Element of G st a in H holds
g * a = a * g ) iff g is Element of (Centralizer H) )
proof end;

theorem :: GROUP_22:59
for G being Group
for A being Subset of G holds A is Subset of (Centralizer (Centralizer A))
proof end;

theorem :: GROUP_22:60
for G being Group
for K being strict characteristic Subgroup of G holds Centralizer K is characteristic Subgroup of G
proof end;

definition
let G be Group;
let a be Element of G;
:: original: {
redefine func {a} -> Subset of G;
coherence
{a} is Subset of G
proof end;
end;

definition
let G be Group;
let a be Element of G;
func Normalizer a -> strict Subgroup of G equals :: GROUP_22:def 7
 Normalizer {a};
correctness
coherence
Normalizer {a} is strict Subgroup of G;
;
end;

:: deftheorem defines Normalizer GROUP_22:def 7 :
for G being Group
for a being Element of G holds Normalizer a = Normalizer {a};

theorem Th64: :: GROUP_22:61
for G being Group
for a, x being Element of G holds
( x in Normalizer a iff ex h being Element of G st
( x = h & a |^ h = a ) )
proof end;

theorem :: GROUP_22:62
for G being Group
for A being non empty Subset of G holds the carrier of (Centralizer A) = meet { B where B is Subset of G : ex H being strict Subgroup of G st
( B = the carrier of H & ex a being Element of G st
( a in A & H = Normalizer a ) ) }
proof end;

theorem Th66: :: GROUP_22:63
for G being finite Group
for H1, H2 being strict Subgroup of G st card (H1 /\ H2) = card H1 & card (H1 /\ H2) = card H2 holds
H1 = H2
proof end;

theorem Th69: :: GROUP_22:64
for G1, G2 being finite Group
for N1 being normal Subgroup of G1
for N2 being normal Subgroup of G2 st G1 ./. N1,G2 ./. N2 are_isomorphic holds
(card N2) * (card G1) = (card N1) * (card G2)
proof end;

theorem Th70: :: GROUP_22:65
for G being finite Group
for K, N being strict normal Subgroup of G
for m, d being Nat st m = card N & m = card K & d = card (K /\ N) holds
d * (card (N "\/" K)) = m * m
proof end;

theorem :: GROUP_22:66
for G being finite Group
for N being strict normal Subgroup of G st card N, index N are_coprime holds
N is characteristic Subgroup of G
proof end;

theorem Th72: :: GROUP_22:67
for G1, G2, G3 being Group
for f1 being Homomorphism of G1,G2
for f2 being Homomorphism of G2,G3
for A being Subgroup of G1 holds multMagma(# the carrier of (f2 .: (f1 .: A)), the multF of (f2 .: (f1 .: A)) #) = multMagma(# the carrier of ((f2 * f1) .: A), the multF of ((f2 * f1) .: A) #)
proof end;

theorem Th73: :: GROUP_22:68
for G being Group
for N being strict normal Subgroup of G
for phi being Automorphism of G st Image (phi | N) = N holds
ex sigma being Automorphism of (G ./. N) st
for x being Element of G holds sigma . (x * N) = (phi . x) * N
proof end;

theorem :: GROUP_22:69
for G being finite Group
for H being strict characteristic Subgroup of G
for K being strict Subgroup of G st H is Subgroup of K holds
H is normal Subgroup of K
proof end;

:: Gorenstein, Finite Groups, Theorem 2.1.2 (iv)
theorem :: GROUP_22:70
for G being finite Group
for H being strict characteristic Subgroup of G
for K being strict Subgroup of G st H is Subgroup of K & K ./. ((K,H) `*`) is characteristic Subgroup of G ./. H holds
K is characteristic Subgroup of G
proof end;

theorem :: GROUP_22:71
for G being Group
for H being Subgroup of G holds
( H is Subgroup of Centralizer H iff H is commutative Group )
proof end;

theorem :: GROUP_22:72
for G being Group holds Centralizer ((Omega). G) = center G
proof end;

theorem :: GROUP_22:73
for G being Group
for N being normal Subgroup of G holds Centralizer N is normal Subgroup of G
proof end;

theorem Th79: :: GROUP_22:74
for G being Group
for H being Subgroup of G
for h, n being Element of G st h in H & n in Normalizer H holds
h |^ n in H
proof end;

theorem Th80: :: GROUP_22:75
for G being Group
for H being Subgroup of G holds H is Subgroup of Normalizer H
proof end;

Lm8: for G being Group
for H being Subgroup of G holds Centralizer H is strict Subgroup of Normalizer H
proof end;

theorem :: GROUP_22:76
for G being Group
for H being Subgroup of G holds Centralizer H is strict normal Subgroup of Normalizer H
proof end;