let G be strict Group; :: thesis: ( G is commutative Group iff G ` = (1). G )

thus ( G is commutative Group implies G ` = (1). G ) :: thesis: ( G ` = (1). G implies G is commutative Group )

G is commutative

thus ( G is commutative Group implies G ` = (1). G ) :: thesis: ( G ` = (1). G implies G is commutative Group )

proof

assume A3:
G ` = (1). G
; :: thesis: G is commutative Group
assume A1:
G is commutative Group
; :: thesis: G ` = (1). G

(1). G is Subgroup of G ` by GROUP_2:65;

hence G ` = (1). G by A2, GROUP_2:55; :: thesis: verum

end;now :: thesis: for a being Element of G st a in G ` holds

a in (1). G

then A2:
G ` is Subgroup of (1). G
by GROUP_2:58;a in (1). G

let a be Element of G; :: thesis: ( a in G ` implies a in (1). G )

assume a in G ` ; :: thesis: a in (1). G

then a in gr {(1_ G)} by A1, Th51;

then a in gr ({(1_ G)} \ {(1_ G)}) by GROUP_4:35;

then a in gr ({} the carrier of G) by XBOOLE_1:37;

hence a in (1). G by GROUP_4:30; :: thesis: verum

end;assume a in G ` ; :: thesis: a in (1). G

then a in gr {(1_ G)} by A1, Th51;

then a in gr ({(1_ G)} \ {(1_ G)}) by GROUP_4:35;

then a in gr ({} the carrier of G) by XBOOLE_1:37;

hence a in (1). G by GROUP_4:30; :: thesis: verum

(1). G is Subgroup of G ` by GROUP_2:65;

hence G ` = (1). G by A2, GROUP_2:55; :: thesis: verum

G is commutative

proof

hence
G is commutative Group
; :: thesis: verum
let a, b be Element of G; :: according to GROUP_1:def 12 :: thesis: a * b = b * a

[.a,b.] in G ` by Th74;

then [.a,b.] = 1_ G by A3, Th1;

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

end;[.a,b.] in G ` by Th74;

then [.a,b.] = 1_ G by A3, Th1;

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