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 holds H is Subgroup of H |^ a )
let H be strict Subgroup of G; :: thesis: ( H is normal Subgroup of G iff for a being Element of G holds H is Subgroup of H |^ a )
thus ( H is normal Subgroup of G implies for a being Element of G holds H is Subgroup of H |^ a ) :: thesis: ( ( for a being Element of G holds H is Subgroup of H |^ a ) implies H is normal Subgroup of G )
proof
assume A1: H is normal Subgroup of G ; :: thesis: for a being Element of G holds H is Subgroup of H |^ a
let a be Element of G; :: thesis: H is Subgroup of H |^ a
H |^ a = multMagma(# the carrier of H, the multF of H #) by A1, Def13;
hence H is Subgroup of H |^ a by GROUP_2:54; :: thesis: verum
end;
assume A2: for a being Element of G holds H is Subgroup of H |^ a ; :: thesis: H is normal Subgroup of G
now :: thesis: for a being Element of G holds H * a c= a * H
let a be Element of G; :: thesis: H * a c= a * H
A3: (H |^ (a ")) * a = ((((a ") ") * H) * (a ")) * a by Th59
.= (((a ") ") * H) * ((a ") * a) by GROUP_2:34
.= (((a ") ") * H) * (1_ G) by GROUP_1:def 5
.= ((a ") ") * H by GROUP_2:37
.= a * H ;
H is Subgroup of H |^ (a ") by A2;
hence H * a c= a * H by A3, Th6; :: thesis: verum
end;
hence H is normal Subgroup of G by Th119; :: thesis: verum