let G be Group; :: thesis: for H being strict Subgroup of G holds
( H is normal Subgroup of G iff con_class H = {H} )
let H be strict Subgroup of G; :: thesis: ( H is normal Subgroup of G iff con_class H = {H} )
thus ( H is normal Subgroup of G implies con_class H = {H} ) :: thesis: ( con_class H = {H} implies H is normal Subgroup of G )
proof
assume A1: H is normal Subgroup of G ; :: thesis: con_class H = {H}
thus con_class H c= {H} :: according to XBOOLE_0:def 10 :: thesis: {H} c= con_class H
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in con_class H or x in {H} )
assume x in con_class H ; :: thesis: x in {H}
then consider H1 being strict Subgroup of G such that
A2: x = H1 and
A3: H,H1 are_conjugated by Def12;
ex g being Element of G st H1 = H |^ g by A3, Th102;
then x = H by A1, A2, Def13;
hence x in {H} by TARSKI:def 1; :: thesis: verum
end;
H in con_class H by Th109;
hence {H} c= con_class H by ZFMISC_1:31; :: thesis: verum
end;
assume A4: con_class H = {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 in con_class H by Th108;
hence H |^ a = multMagma(# the carrier of H, the multF of H #) by A4, TARSKI:def 1; :: thesis: verum
end;
hence H is normal Subgroup of G ; :: thesis: verum