let G be Group; :: thesis: ( G is commutative Group iff for H1, H2 being Subgroup of G holds commutators (H1,H2) = {(1_ G)} )

thus ( G is commutative Group implies for H1, H2 being Subgroup of G holds commutators (H1,H2) = {(1_ G)} ) by Th51; :: thesis: ( ( for H1, H2 being Subgroup of G holds commutators (H1,H2) = {(1_ G)} ) implies G is commutative Group )

assume A1: for H1, H2 being Subgroup of G holds commutators (H1,H2) = {(1_ G)} ; :: thesis: G is commutative Group

G is commutative

thus ( G is commutative Group implies for H1, H2 being Subgroup of G holds commutators (H1,H2) = {(1_ G)} ) by Th51; :: thesis: ( ( for H1, H2 being Subgroup of G holds commutators (H1,H2) = {(1_ G)} ) implies G is commutative Group )

assume A1: for H1, H2 being Subgroup of G holds commutators (H1,H2) = {(1_ G)} ; :: thesis: G is commutative Group

G is commutative

proof

hence
G is commutative Group
; :: thesis: verum
let a be Element of G; :: according to GROUP_1:def 12 :: thesis: for b_{1} being Element of the carrier of G holds a * b_{1} = b_{1} * a

let b be Element of G; :: thesis: a * b = b * a

b in {b} by TARSKI:def 1;

then A2: b in gr {b} by GROUP_4:29;

a in {a} by TARSKI:def 1;

then a in gr {a} by GROUP_4:29;

then [.a,b.] in commutators ((gr {a}),(gr {b})) by A2, Th52;

then [.a,b.] in {(1_ G)} by A1;

then [.a,b.] = 1_ G by TARSKI:def 1;

hence a * b = b * a by Th36; :: thesis: verum

end;let b be Element of G; :: thesis: a * b = b * a

b in {b} by TARSKI:def 1;

then A2: b in gr {b} by GROUP_4:29;

a in {a} by TARSKI:def 1;

then a in gr {a} by GROUP_4:29;

then [.a,b.] in commutators ((gr {a}),(gr {b})) by A2, Th52;

then [.a,b.] in {(1_ G)} by A1;

then [.a,b.] = 1_ G by TARSKI:def 1;

hence a * b = b * a by Th36; :: thesis: verum