let G be Group; ( 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)} )
( ( 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
;
for A, B being Subset of G st A <> {} & B <> {} holds
commutators (A,B) = {(1_ G)}
let A,
B be
Subset of
G;
( A <> {} & B <> {} implies commutators (A,B) = {(1_ G)} )
assume A2:
(
A <> {} &
B <> {} )
;
commutators (A,B) = {(1_ G)}
thus
commutators (
A,
B)
c= {(1_ G)}
XBOOLE_0:def 10 {(1_ G)} c= commutators (A,B)
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 ;
TARSKI:def 3 ( not x in {(1_ G)} or x in commutators (A,B) )
assume
x in {(1_ G)}
;
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;
verum
end;
assume A5:
for A, B being Subset of G st A <> {} & B <> {} holds
commutators (A,B) = {(1_ G)}
; G is commutative Group
G is commutative
hence
G is commutative Group
; verum