let G be Group; :: thesis: for H being Subgroup of G

for N being strict normal Subgroup of G holds

( commutators (H,N) c= carr N & commutators (N,H) c= carr N )

let H be Subgroup of G; :: thesis: for N being strict normal Subgroup of G holds

( commutators (H,N) c= carr N & commutators (N,H) c= carr N )

let N be strict normal Subgroup of G; :: thesis: ( commutators (H,N) c= carr N & commutators (N,H) c= carr N )

thus commutators (H,N) c= carr N :: thesis: commutators (N,H) c= carr N

assume x in commutators (N,H) ; :: thesis: x in carr N

then consider a, b being Element of G such that

A3: x = [.a,b.] and

A4: a in N and

b in H by Th52;

a |^ b in N |^ b by A4, GROUP_3:58;

then A5: a |^ b in N by GROUP_3:def 13;

( x = (a ") * (a |^ b) & a " in N ) by A3, A4, Th16, GROUP_2:51;

then x in N by A5, GROUP_2:50;

hence x in carr N by STRUCT_0:def 5; :: thesis: verum

for N being strict normal Subgroup of G holds

( commutators (H,N) c= carr N & commutators (N,H) c= carr N )

let H be Subgroup of G; :: thesis: for N being strict normal Subgroup of G holds

( commutators (H,N) c= carr N & commutators (N,H) c= carr N )

let N be strict normal Subgroup of G; :: thesis: ( commutators (H,N) c= carr N & commutators (N,H) c= carr N )

thus commutators (H,N) c= carr N :: thesis: commutators (N,H) c= carr N

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in commutators (N,H) or x in carr N )
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in commutators (H,N) or x in carr N )

assume x in commutators (H,N) ; :: thesis: x in carr N

then consider a, b being Element of G such that

A1: x = [.a,b.] and

a in H and

A2: b in N by Th52;

b " in N by A2, GROUP_2:51;

then (b ") |^ a in N |^ a by GROUP_3:58;

then (b ") |^ a in N by GROUP_3:def 13;

then x in N by A1, A2, GROUP_2:50;

hence x in carr N by STRUCT_0:def 5; :: thesis: verum

end;assume x in commutators (H,N) ; :: thesis: x in carr N

then consider a, b being Element of G such that

A1: x = [.a,b.] and

a in H and

A2: b in N by Th52;

b " in N by A2, GROUP_2:51;

then (b ") |^ a in N |^ a by GROUP_3:58;

then (b ") |^ a in N by GROUP_3:def 13;

then x in N by A1, A2, GROUP_2:50;

hence x in carr N by STRUCT_0:def 5; :: thesis: verum

assume x in commutators (N,H) ; :: thesis: x in carr N

then consider a, b being Element of G such that

A3: x = [.a,b.] and

A4: a in N and

b in H by Th52;

a |^ b in N |^ b by A4, GROUP_3:58;

then A5: a |^ b in N by GROUP_3:def 13;

( x = (a ") * (a |^ b) & a " in N ) by A3, A4, Th16, GROUP_2:51;

then x in N by A5, GROUP_2:50;

hence x in carr N by STRUCT_0:def 5; :: thesis: verum