let F be commutative Skew-Field; for G being finite Subgroup of MultGroup F holds G is cyclic Group
let G be finite Subgroup of MultGroup F; G is cyclic Group
consider a being Element of G;
defpred S1[ Nat, Element of G, Element of G] means ord $2 < ord $3;
assume
G is not cyclic Group
; contradiction
then A1:
for x being Element of G holds not ord x = card G
by GR_CY_1:43;
A2:
for x being Element of G holds ord x < card G
A3:
for n being Element of NAT
for x being Element of G ex y being Element of G st S1[n,x,y]
proof
let n be
Element of
NAT ;
for x being Element of G ex y being Element of G st S1[n,x,y]let x be
Element of
G;
ex y being Element of G st S1[n,x,y]
set n =
ord x;
ord x < card G
by A2;
then A4:
card (gr {x}) <> card G
by GR_CY_1:27;
the
carrier of
(gr {x}) c= the
carrier of
G
by GROUP_2:def 5;
then
the
carrier of
(gr {x}) c< the
carrier of
G
by A4, XBOOLE_0:def 8;
then
the
carrier of
G \ the
carrier of
(gr {x}) <> {}
by XBOOLE_1:105;
then consider z being
set such that A5:
z in the
carrier of
G \ the
carrier of
(gr {x})
by XBOOLE_0:def 1;
reconsider z =
z as
Element of
G by A5;
set m =
ord z;
set l =
(ord z) lcm (ord x);
ord x divides (ord z) lcm (ord x)
by INT_2:def 2;
then consider j being
Integer such that A6:
(ord z) lcm (ord x) = (ord x) * j
by INT_1:def 9;
A7:
1
<= card (gr {x})
by GROUP_1:90;
then A8:
1
<= ord x
by GR_CY_1:27;
then
((ord z) lcm (ord x)) / (ord x) = j
by A6, XCMPLX_1:90;
then A9:
j is
Element of
NAT
by INT_1:16;
not
ord z divides ord x
then A12:
ord x <> (ord z) lcm (ord x)
by INT_2:def 2;
A13:
1
<= card (gr {z})
by GROUP_1:90;
then A14:
ord z <> 0
by GR_CY_1:27;
1
<= ord z
by A13, GR_CY_1:27;
then consider m0,
n0 being
Element of
NAT such that A15:
(ord z) lcm (ord x) = n0 * m0
and A16:
n0 gcd m0 = 1
and A17:
n0 divides ord x
and A18:
m0 divides ord z
and A19:
n0 <> 0
and A20:
m0 <> 0
by A8, INT_7:17;
ex
u being
Integer st
ord z = m0 * u
by A18, INT_1:def 9;
then
(ord z) / m0 is
Integer
by A20, XCMPLX_1:90;
then reconsider d2 =
(ord z) / m0 as
Element of
NAT by INT_1:16;
ex
j being
Integer st
ord x = n0 * j
by A17, INT_1:def 9;
then
(ord x) / n0 is
Integer
by A19, XCMPLX_1:90;
then reconsider d1 =
(ord x) / n0 as
Element of
NAT by INT_1:16;
set y =
(x |^ d1) * (z |^ d2);
ord z = d2 * m0
by A20, XCMPLX_1:88;
then A21:
ord (z |^ d2) = m0
by INT_7:30;
ord x <> 0
by A7, GR_CY_1:27;
then
j <> 0
by A14, A6, INT_2:4;
then
(ord x) * 1
<= (ord x) * j
by A9, NAT_1:14, XREAL_1:66;
then A22:
ord x < (ord z) lcm (ord x)
by A12, A6, XXREAL_0:1;
ord x = d1 * n0
by A19, XCMPLX_1:88;
then
ord (x |^ d1) = n0
by INT_7:30;
then
ord ((x |^ d1) * (z |^ d2)) = m0 * n0
by A16, A21, INT_7:25;
hence
ex
y being
Element of
G st
ord x < ord y
by A15, A22;
verum
reconsider H =
gr {z} as
strict Subgroup of
G ;
reconsider d =
(ord z) gcd (ord x) as
Nat ;
end;
consider f being Function of NAT ,the carrier of G such that
A23:
( f . 0 = a & ( for n being Element of NAT holds S1[n,f . n,f . (n + 1)] ) )
from RECDEF_1:sch 2(A3);
deffunc H1( Element of NAT ) -> Element of NAT = ord (f . $1);
consider g being Function of NAT ,NAT such that
A24:
for k being Element of NAT holds g . k = H1(k)
from FUNCT_2:sch 4();
A27:
for k, m being Element of NAT holds g . k < g . ((k + 1) + m)
A31:
for k, m being Element of NAT st k < m holds
g . k < g . m
then
g is one-to-one
by FUNCT_2:25;
then
dom g, rng g are_equipotent
by WELLORD2:def 4;
then
card (dom g) = card (rng g)
by CARD_1:21;
then A38:
card (rng g) = card NAT
by FUNCT_2:def 1;
rng g c= Segm (card G)
hence
contradiction
by A38; verum