let G be Group; :: thesis: for H being strict Subgroup of G holds
( H is normal Subgroup of G iff for a being Element of G st a in H holds
con_class a c= carr H )
let H be strict Subgroup of G; :: thesis: ( H is normal Subgroup of G iff for a being Element of G st a in H holds
con_class a c= carr H )
thus ( H is normal Subgroup of G implies for a being Element of G st a in H holds
con_class a c= carr H ) :: thesis: ( ( for a being Element of G st a in H holds
con_class a c= carr H ) implies H is normal Subgroup of G )

proof

assume A1: H is normal Subgroup of G ; :: thesis: for a being Element of G st a in H holds
con_class a c= carr H
let a be Element of G; :: thesis: ( a in H implies con_class a c= carr H )
assume A2: a in H ; :: thesis: con_class a c= carr H
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in con_class a or x in carr H )
assume x in con_class a ; :: thesis: x in carr H
then consider b being Element of G such that
A3: x = b and
A4: a,b are_conjugated by Th80;
consider c being Element of G such that
A5: b = a |^ c by A4, Th74;
x in H |^ c by A2, A3, A5, Th58;
then x in H by A1, Def13;
hence x in carr H ; :: thesis: verum

end;

assume A6: for a being Element of G st a in H holds
con_class a c= carr H ; :: thesis: H is normal Subgroup of G
H is normal

proof

let a be Element of G; :: according to GROUP_3:def 13 :: thesis: H |^ a = multMagma(# the carrier of H, the multF of H #)
H |^ a = H

proof

let b be Element of G; :: according to GROUP_2:def 6 :: thesis: ( ( not b in H |^ a or b in H ) & ( not b in H or b in H |^ a ) )
thus ( b in H |^ a implies b in H ) :: thesis: ( not b in H or b in H |^ a )

proof

assume b in H |^ a ; :: thesis: b in H
then consider c being Element of G such that
A7: ( b = c |^ a & c in H ) by Th58;
( b in con_class c & con_class c c= carr H ) by A6, A7, Th82;
hence b in H ; :: thesis: verum

end;

assume b in H ; :: thesis: b in H |^ a
then A8: con_class b c= carr H by A6;
b |^ (a ") in con_class b by Th82;
then b |^ (a ") in H by A8;
then (b |^ (a ")) |^ a in H |^ a by Th58;
hence b in H |^ a by Th25; :: thesis: verum

end;

hence H |^ a = multMagma(# the carrier of H, the multF of H #) ; :: thesis: verum

end;

hence H is normal Subgroup of G ; :: thesis: verum