let G be finite Group; for N being normal Subgroup of G st N is Subgroup of center G & G ./. N is cyclic holds
G is commutative
let N be normal Subgroup of G; ( N is Subgroup of center G & G ./. N is cyclic implies G is commutative )
assume that
A1:
N is Subgroup of center G
and
A2:
G ./. N is cyclic
; G is commutative
reconsider I = G ./. N as finite Group ;
consider S being Element of I such that
A3:
for T being Element of I ex n being Nat st T = S |^ n
by A2, GR_CY_1:18;
consider a1 being Element of G such that
A4:
( S = a1 * N & S = N * a1 )
by GROUP_6:21;
for a, b being Element of G holds a * b = b * a
proof
let a,
b be
Element of
G;
a * b = b * a
A5:
(
a * N is
Element of
I &
b * N is
Element of
I )
by GROUP_6:22;
then consider r1 being
Nat such that A6:
a * N = S |^ r1
by A3;
a * N = (a1 |^ r1) * N
by A4, Th8, A6;
then consider c1 being
Element of
G such that A7:
(
a = (a1 |^ r1) * c1 &
c1 in N )
by Th9;
A8:
c1 in center G
by A1, A7, GROUP_2:40;
consider r2 being
Nat such that A9:
b * N = S |^ r2
by A3, A5;
b * N = (a1 |^ r2) * N
by A4, Th8, A9;
then consider c2 being
Element of
G such that A10:
(
b = (a1 |^ r2) * c2 &
c2 in N )
by Th9;
A11:
c2 in center G
by A1, A10, GROUP_2:40;
a * b =
(a1 |^ r1) * (c1 * ((a1 |^ r2) * c2))
by A7, A10, GROUP_1:def 3
.=
(a1 |^ r1) * (((a1 |^ r2) * c2) * c1)
by A8, GROUP_5:77
.=
(a1 |^ r1) * ((a1 |^ r2) * (c2 * c1))
by GROUP_1:def 3
.=
((a1 |^ r1) * (a1 |^ r2)) * (c2 * c1)
by GROUP_1:def 3
.=
(a1 |^ (r1 + r2)) * (c2 * c1)
by GROUP_1:33
.=
((a1 |^ r2) * (a1 |^ r1)) * (c2 * c1)
by GROUP_1:33
.=
(a1 |^ r2) * ((a1 |^ r1) * (c2 * c1))
by GROUP_1:def 3
.=
(a1 |^ r2) * (((a1 |^ r1) * c2) * c1)
by GROUP_1:def 3
.=
(a1 |^ r2) * ((c2 * (a1 |^ r1)) * c1)
by A11, GROUP_5:77
.=
(a1 |^ r2) * (c2 * ((a1 |^ r1) * c1))
by GROUP_1:def 3
.=
b * a
by A7, A10, GROUP_1:def 3
;
hence
a * b = b * a
;
verum
end;
hence
G is commutative
by GROUP_1:def 12; verum