let G be Group; :: thesis: for a, b being Element of G holds

( [.a,b.] = 1_ G iff a * b = b * a )

let a, b be Element of G; :: thesis: ( [.a,b.] = 1_ G iff a * b = b * a )

thus ( [.a,b.] = 1_ G implies a * b = b * a ) :: thesis: ( a * b = b * a implies [.a,b.] = 1_ G )

then A1: (b * a) " = (b ") * (a ") by GROUP_1:18;

[.a,b.] = ((b * a) ") * (a * b) by Th17;

hence [.a,b.] = (((b ") * (a ")) * a) * b by A1, GROUP_1:def 3

.= (b ") * b by GROUP_3:1

.= 1_ G by GROUP_1:def 5 ;

:: thesis: verum

( [.a,b.] = 1_ G iff a * b = b * a )

let a, b be Element of G; :: thesis: ( [.a,b.] = 1_ G iff a * b = b * a )

thus ( [.a,b.] = 1_ G implies a * b = b * a ) :: thesis: ( a * b = b * a implies [.a,b.] = 1_ G )

proof

assume
a * b = b * a
; :: thesis: [.a,b.] = 1_ G
assume
[.a,b.] = 1_ G
; :: thesis: a * b = b * a

then ((b * a) ") * (a * b) = 1_ G by Th17;

then a * b = ((b * a) ") " by GROUP_1:12;

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

end;then ((b * a) ") * (a * b) = 1_ G by Th17;

then a * b = ((b * a) ") " by GROUP_1:12;

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

then A1: (b * a) " = (b ") * (a ") by GROUP_1:18;

[.a,b.] = ((b * a) ") * (a * b) by Th17;

hence [.a,b.] = (((b ") * (a ")) * a) * b by A1, GROUP_1:def 3

.= (b ") * b by GROUP_3:1

.= 1_ G by GROUP_1:def 5 ;

:: thesis: verum