let G be addGroup; :: 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;
hence x in carr H by A1, Def13; :: 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_1A:def 41 :: thesis: H * a = addMagma(# the carrier of H, the addF of H #)
H * a = H
proof
let b be Element of G; :: according to GROUP_1A:def 16 :: thesis: ( b in H * a iff b in H )
thus ( b in H * a implies b in H ) :: thesis: ( b in H implies 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, Th80, Th74;
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 Th80, Th74;
then b * (- a) in H by A8;
then (b * (- a)) * a in H * a by Th58;
hence b in H * a by ThB25; :: thesis: verum
end;
hence H * a = addMagma(# the carrier of H, the addF of H #) ; :: thesis: verum
end;
hence H is normal Subgroup of G ; :: thesis: verum