let G be finite Group; :: thesis: for a being Element of G holds ord a = card (gr {a})
let a be Element of G; :: thesis: ord a = card (gr {a})
deffunc H1( Nat) -> Element of the carrier of G = a |^ $1;
consider F being FinSequence such that
A1:
len F = ord a
and
A2:
for p being Nat st p in dom F holds
F . p = H1(p)
from FINSEQ_1:sch 2();
A3:
dom F = Seg (ord a)
by A1, FINSEQ_1:def 3;
not a is being_of_order_0
by Th26;
then A4:
ord a <> 0
by GROUP_1:def 12;
then A5:
ord a > 0
;
A6:
a in rng F
A8:
rng F = the carrier of (gr {a})
proof
A9:
for
y being
set st
y in rng F holds
ex
n being
Element of
NAT st
y = a |^ n
A12:
rng F c= the
carrier of
(gr {a})
the
carrier of
(gr {a}) c= rng F
proof
ex
H being
strict Subgroup of
G st the
carrier of
H = rng F
proof
reconsider car =
rng F as non
empty set by A6;
A14:
dom the
multF of
G = [:the carrier of G,the carrier of G:]
by FUNCT_2:def 1;
the
carrier of
(gr {a}) c= the
carrier of
G
by GROUP_2:def 5;
then A15:
car c= the
carrier of
G
by A12, XBOOLE_1:1;
then A16:
dom (the multF of G || car) = [:car,car:]
by A14, RELAT_1:91, ZFMISC_1:119;
rng (the multF of G || car) c= car
proof
for
y being
set st
y in rng (the multF of G || car) holds
y in car
proof
set f = the
multF of
G || car;
let y be
set ;
:: thesis: ( y in rng (the multF of G || car) implies y in car )
assume
y in rng (the multF of G || car)
;
:: thesis: y in car
then consider x being
set such that A17:
x in dom (the multF of G || car)
and A18:
(the multF of G || car) . x = y
by FUNCT_1:def 5;
consider xp,
yp being
set such that A19:
[xp,yp] = x
by A16, A17, RELAT_1:def 1;
xp in car
by A16, A17, A19, ZFMISC_1:106;
then consider p being
Element of
NAT such that A20:
xp = a |^ p
by A9;
yp in car
by A16, A17, A19, ZFMISC_1:106;
then consider s being
Element of
NAT such that A21:
yp = a |^ s
by A9;
A22:
y =
(a |^ p) * (a |^ s)
by A17, A18, A19, A20, A21, FUNCT_1:70
.=
a |^ (p + s)
by GROUP_1:63
;
a |^ (p + s) in car
hence
y in car
by A22;
:: thesis: verum
end;
hence
rng (the multF of G || car) c= car
by TARSKI:def 3;
:: thesis: verum
end;
then reconsider op = the
multF of
G || car as
BinOp of
car by A16, FUNCT_2:def 1, RELSET_1:11;
set H =
multMagma(#
car,
op #);
multMagma(#
car,
op #) is
Group
proof
A28:
for
f,
g being
Element of
multMagma(#
car,
op #)
for
f',
g' being
Element of
G st
f = f' &
g = g' holds
f' * g' = f * g
A30:
for
f,
g,
h being
Element of
multMagma(#
car,
op #) holds
(f * g) * h = f * (g * h)
ex
e being
Element of
multMagma(#
car,
op #) st
for
h being
Element of
multMagma(#
car,
op #) holds
(
h * e = h &
e * h = h & ex
g being
Element of
multMagma(#
car,
op #) st
(
h * g = e &
g * h = e ) )
hence
multMagma(#
car,
op #) is
Group
by A30, GROUP_1:5;
:: thesis: verum
end;
then reconsider H1 =
multMagma(#
car,
op #) as
Group ;
the
carrier of
(gr {a}) c= the
carrier of
G
by GROUP_2:def 5;
then
the
carrier of
H1 c= the
carrier of
G
by A12, XBOOLE_1:1;
then
H1 is
Subgroup of
G
by GROUP_2:def 5;
hence
ex
H being
strict Subgroup of
G st the
carrier of
H = rng F
;
:: thesis: verum
end;
then consider H being
strict Subgroup of
G such that A42:
the
carrier of
H = rng F
;
{a} c= the
carrier of
H
by A6, A42, ZFMISC_1:37;
then
gr {a} is
Subgroup of
H
by GROUP_4:def 5;
hence
the
carrier of
(gr {a}) c= rng F
by A42, GROUP_2:def 5;
:: thesis: verum
end;
hence
rng F = the
carrier of
(gr {a})
by A12, XBOOLE_0:def 10;
:: thesis: verum
end;
F is one-to-one
then A59:
Seg (ord a),the carrier of (gr {a}) are_equipotent
by A3, A8, WELLORD2:def 4;
set ca = the carrier of (gr {a});
reconsider So = Seg (ord a) as finite set ;
card So = card the carrier of (gr {a})
by A59, CARD_1:21;
hence
ord a = card (gr {a})
by FINSEQ_1:78; :: thesis: verum