let G be Group; :: thesis: for H being Subgroup of G st H is Subgroup of center G holds

H is normal Subgroup of G

let H be Subgroup of G; :: thesis: ( H is Subgroup of center G implies H is normal Subgroup of G )

assume A1: H is Subgroup of center G ; :: thesis: H is normal Subgroup of G

H is normal Subgroup of G

let H be Subgroup of G; :: thesis: ( H is Subgroup of center G implies H is normal Subgroup of G )

assume A1: H is Subgroup of center G ; :: thesis: H is normal Subgroup of G

now :: thesis: for a being Element of G holds H * a c= a * H

hence
H is normal Subgroup of G
by GROUP_3:119; :: thesis: verumlet a be Element of G; :: thesis: H * a c= a * H

thus H * a c= a * H :: thesis: verum

end;thus H * a c= a * H :: thesis: verum

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in H * a or x in a * H )

assume x in H * a ; :: thesis: x in a * H

then consider b being Element of G such that

A2: x = b * a and

A3: b in H by GROUP_2:104;

b in center G by A1, A3, GROUP_2:40;

then x = a * b by A2, Th77;

hence x in a * H by A3, GROUP_2:103; :: thesis: verum

end;assume x in H * a ; :: thesis: x in a * H

then consider b being Element of G such that

A2: x = b * a and

A3: b in H by GROUP_2:104;

b in center G by A1, A3, GROUP_2:40;

then x = a * b by A2, Th77;

hence x in a * H by A3, GROUP_2:103; :: thesis: verum