let G be Group; :: thesis: for H being Subgroup of G holds H is Subgroup of Normalizer H
let H be Subgroup of G; :: thesis: H is Subgroup of Normalizer H
A1: for g being Element of G st g in H holds
for x being Element of G st x in (carr H) |^ g holds
x in carr H

proof

let g be Element of G; :: thesis: ( g in H implies for x being Element of G st x in (carr H) |^ g holds
x in carr H )
assume B1: g in H ; :: thesis: for x being Element of G st x in (carr H) |^ g holds
x in carr H
let x be Element of G; :: thesis: ( x in (carr H) |^ g implies x in carr H )
assume x in (carr H) |^ g ; :: thesis: x in carr H
then consider h being Element of G such that
B2: ( x = h |^ g & h in carr H ) by GROUP_3:41;
B3: h in H by B2;
g " in H by B1, GROUP_2:51;
then (g ") * h in H by B3, GROUP_2:50;
then x in H by B1, B2, GROUP_2:50;
hence x in carr H ; :: thesis: verum

end;

for g being Element of G st g in H holds
g in Normalizer H

proof

let g be Element of G; :: thesis: ( g in H implies g in Normalizer H )
assume B1: g in H ; :: thesis: g in Normalizer H
for x being Element of G st x in carr H holds
x in (carr H) |^ g

proof

let x be Element of G; :: thesis: ( x in carr H implies x in (carr H) |^ g )
thus ( x in carr H implies x in (carr H) |^ g ) :: thesis: verum

proof

assume x in carr H ; :: thesis: x in (carr H) |^ g
then C1: x in H ;
set h = x |^ (g ");
g " in H by B1, GROUP_2:51;
then x * (g ") in H by C1, GROUP_2:50;
then g * (x * (g ")) in H by B1, GROUP_2:50;
then C2: x |^ (g ") in carr H by GROUP_1:def 3;
(x |^ (g ")) |^ g = x by GROUP_3:25;
hence x in (carr H) |^ g by C2, GROUP_3:41; :: thesis: verum

end;

end;

then ( (carr H) |^ g c= carr H & carr H c= (carr H) |^ g ) by A1, B1;
then (carr H) |^ g = carr H by XBOOLE_0:def 10;
hence g in Normalizer H by GROUP_3:129; :: thesis: verum

end;

hence H is Subgroup of Normalizer H by GROUP_2:58; :: thesis: verum