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 )
proof
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)
proof
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;
set b = the Element of 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;
assume A5: for A, B being Subset of G st A <> {} & B <> {} holds
commutators (A,B) = {(1_ G)} ; :: thesis: G is commutative Group
G is commutative
proof
let a be Element of G; :: according to GROUP_1:def 12 :: thesis: for b1 being Element of the carrier of G holds a * b1 = b1 * 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;
hence G is commutative Group ; :: thesis: verum