let G be Group; :: thesis: ( G is commutative Group iff for A, B being Subset of G st A <> {} & B <> {} holds

commutators (A,B) = {(1_ G)} )

thus ( G is commutative Group implies for A, B being Subset of G st A <> {} & B <> {} holds

commutators (A,B) = {(1_ G)} ) :: thesis: ( ( for A, B being Subset of G st A <> {} & B <> {} holds

commutators (A,B) = {(1_ G)} ) implies G is commutative Group )

commutators (A,B) = {(1_ G)} ; :: thesis: G is commutative Group

G is commutative

commutators (A,B) = {(1_ G)} )

thus ( G is commutative Group implies for A, B being Subset of G st A <> {} & B <> {} holds

commutators (A,B) = {(1_ G)} ) :: thesis: ( ( for A, B being Subset of G st A <> {} & B <> {} holds

commutators (A,B) = {(1_ G)} ) implies G is commutative Group )

proof

assume A5:
for A, B being Subset of G st A <> {} & B <> {} holds
assume A1:
G is commutative Group
; :: thesis: for A, B being Subset of G st A <> {} & B <> {} holds

commutators (A,B) = {(1_ G)}

let A, B be Subset of G; :: thesis: ( A <> {} & B <> {} implies commutators (A,B) = {(1_ G)} )

assume A2: ( A <> {} & B <> {} ) ; :: thesis: commutators (A,B) = {(1_ G)}

thus commutators (A,B) c= {(1_ G)} :: according to XBOOLE_0:def 10 :: thesis: {(1_ G)} c= commutators (A,B)

set a = the Element of A;

reconsider a = the Element of A, b = the Element of B as Element of G by A2, TARSKI:def 3;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in {(1_ G)} or x in commutators (A,B) )

assume x in {(1_ G)} ; :: thesis: x in commutators (A,B)

then A4: x = 1_ G by TARSKI:def 1;

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

.= ((a ") * (a * (b "))) * b by A1, Lm1

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

.= x by A4, GROUP_1:def 5 ;

hence x in commutators (A,B) by A2; :: thesis: verum

end;commutators (A,B) = {(1_ G)}

let A, B be Subset of G; :: thesis: ( A <> {} & B <> {} implies commutators (A,B) = {(1_ G)} )

assume A2: ( A <> {} & B <> {} ) ; :: thesis: commutators (A,B) = {(1_ G)}

thus commutators (A,B) c= {(1_ G)} :: according to XBOOLE_0:def 10 :: thesis: {(1_ G)} c= commutators (A,B)

proof

set b = the Element of B;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in commutators (A,B) or x in {(1_ G)} )

assume x in commutators (A,B) ; :: thesis: x in {(1_ G)}

then consider a, b being Element of G such that

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

a in A and

b in B ;

x = ((a ") * ((b ") * a)) * b by A3, Th16

.= ((a ") * (a * (b "))) * b by A1, Lm1

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

.= 1_ G by GROUP_1:def 5 ;

hence x in {(1_ G)} by TARSKI:def 1; :: thesis: verum

end;assume x in commutators (A,B) ; :: thesis: x in {(1_ G)}

then consider a, b being Element of G such that

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

a in A and

b in B ;

x = ((a ") * ((b ") * a)) * b by A3, Th16

.= ((a ") * (a * (b "))) * b by A1, Lm1

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

.= 1_ G by GROUP_1:def 5 ;

hence x in {(1_ G)} by TARSKI:def 1; :: thesis: verum

set a = the Element of A;

reconsider a = the Element of A, b = the Element of B as Element of G by A2, TARSKI:def 3;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in {(1_ G)} or x in commutators (A,B) )

assume x in {(1_ G)} ; :: thesis: x in commutators (A,B)

then A4: x = 1_ G by TARSKI:def 1;

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

.= ((a ") * (a * (b "))) * b by A1, Lm1

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

.= x by A4, GROUP_1:def 5 ;

hence x in commutators (A,B) by A2; :: thesis: verum

commutators (A,B) = {(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

( a in {a} & b in {b} ) by TARSKI:def 1;

then A6: [.a,b.] in commutators ({a},{b}) ;

commutators ({a},{b}) = {(1_ G)} by A5;

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

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

then ((b * a) ") * (a * b) = 1_ G by GROUP_1:17;

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

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

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

( a in {a} & b in {b} ) by TARSKI:def 1;

then A6: [.a,b.] in commutators ({a},{b}) ;

commutators ({a},{b}) = {(1_ G)} by A5;

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

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

then ((b * a) ") * (a * b) = 1_ G by GROUP_1:17;

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

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