let G be addGroup; :: thesis: for H being Subgroup of G holds
( H is normal Subgroup of G iff for A being Subset of G holds A + H = H + A )
let H be Subgroup of G; :: thesis: ( H is normal Subgroup of G iff for A being Subset of G holds A + H = H + A )
thus ( H is normal Subgroup of G implies for A being Subset of G holds A + H = H + A ) :: thesis: ( ( for A being Subset of G holds A + H = H + A ) implies H is normal Subgroup of G )
proof
assume A1: H is normal Subgroup of G ; :: thesis: for A being Subset of G holds A + H = H + A
let A be Subset of G; :: thesis: A + H = H + A
thus A + H c= H + A :: according to XBOOLE_0:def 10 :: thesis: H + A c= A + H
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in A + H or x in H + A )
assume x in A + H ; :: thesis: x in H + A
then consider a, h being Element of G such that
A2: x = a + h and
A3: a in A and
A4: h in H by Th94;
x in a + H by A2, A4, Th103;
then x in H + a by A1, Th117;
then ex g being Element of G st
( x = g + a & g in H ) by Th104;
hence x in H + A by A3; :: thesis: verum
end;
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 h, a being Element of G such that
A5: ( x = h + a & h in H ) and
A6: a in A by ThB95;
x in H + a by A5, Th104;
then x in a + H by A1, Th117;
then ex g being Element of G st
( x = a + g & g in H ) by Th103;
hence x in A + H by A6; :: thesis: verum
end;
assume A7: for A being Subset of G holds A + H = H + A ; :: thesis: H is normal Subgroup of G
now :: thesis: for a being Element of G holds a + H = H + a
let a be Element of G; :: thesis: a + H = H + a
thus a + H = {a} + H
.= H + {a} by A7
.= H + a ; :: thesis: verum
end;
hence H is normal Subgroup of G by Th117; :: thesis: verum