let G be finite Group; for a being Element of G holds ord a = card (gr {a})
let a be Element of G; 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;
A4:
for y being set st y in rng F holds
ex n being Element of NAT st y = a |^ n
for x being set st x in rng F holds
x in the carrier of (gr {a})
then A7:
rng F c= the carrier of (gr {a})
by TARSKI:def 3;
not a is being_of_order_0
by Th26;
then A8:
ord a <> 0
by GROUP_1:def 12;
A9:
ex x being set st
( x in dom F & F . x = a )
then A11:
a in rng F
by FUNCT_1:def 5;
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 A9, FUNCT_1:def 5;
the
carrier of
(gr {a}) c= the
carrier of
G
by GROUP_2:def 5;
then A12:
car c= the
carrier of
G
by A7, XBOOLE_1:1;
dom the
multF of
G = [:the carrier of G,the carrier of G:]
by FUNCT_2:def 1;
then A13:
dom (the multF of G || car) = [:car,car:]
by A12, RELAT_1:91, ZFMISC_1:119;
for
y being
set st
y in rng (the multF of G || car) holds
y in car
proof
let y be
set ;
( y in rng (the multF of G || car) implies y in car )
set f = the
multF of
G || car;
assume
y in rng (the multF of G || car)
;
y in car
then consider x being
set such that A14:
x in dom (the multF of G || car)
and A15:
(the multF of G || car) . x = y
by FUNCT_1:def 5;
consider xp,
yp being
set such that A16:
[xp,yp] = x
by A13, A14, RELAT_1:def 1;
yp in car
by A13, A14, A16, ZFMISC_1:106;
then consider s being
Element of
NAT such that A17:
yp = a |^ s
by A4;
xp in car
by A13, A14, A16, ZFMISC_1:106;
then consider p being
Element of
NAT such that A18:
xp = a |^ p
by A4;
A19:
ex
x being
set st
(
x in dom F &
F . x = a |^ (p + s) )
y =
(a |^ p) * (a |^ s)
by A14, A15, A16, A18, A17, FUNCT_1:70
.=
a |^ (p + s)
by GROUP_1:63
;
hence
y in car
by A19, FUNCT_1:def 5;
verum
end;
then
rng (the multF of G || car) c= car
by TARSKI:def 3;
then reconsider op = the
multF of
G || car as
BinOp of
car by A13, FUNCT_2:def 1, RELSET_1:11;
set H =
multMagma(#
car,
op #);
A23:
for
f,
g being
Element of
multMagma(#
car,
op #)
for
f9,
g9 being
Element of
G st
f = f9 &
g = g9 holds
f9 * g9 = f * g
A25:
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 ) )
for
f,
g,
h being
Element of
multMagma(#
car,
op #) holds
(f * g) * h = f * (g * h)
then reconsider H1 =
multMagma(#
car,
op #) as
Group by A25, GROUP_1:5;
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 A7, 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
;
verum
end;
then consider H being
strict Subgroup of
G such that A36:
the
carrier of
H = rng F
;
{a} c= the
carrier of
H
by A11, A36, 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 A36, GROUP_2:def 5;
verum
end;
then A37:
rng F = the carrier of (gr {a})
by A7, XBOOLE_0:def 10;
reconsider So = Seg (ord a) as finite set ;
set ca = the carrier of (gr {a});
F is one-to-one
proof
let x be
set ;
FUNCT_1:def 8 for b1 being set holds
( not x in proj1 F or not b1 in proj1 F or not F . x = F . b1 or x = b1 )let y be
set ;
( not x in proj1 F or not y in proj1 F or not F . x = F . y or x = y )
assume that A38:
x in dom F
and A39:
y in dom F
and A40:
F . x = F . y
and A41:
x <> y
;
contradiction
reconsider s =
y as
Element of
NAT by A39;
reconsider p =
x as
Element of
NAT by A38;
A42:
(
F . p = a |^ p &
F . s = a |^ s )
by A2, A38, A39;
reconsider s9 =
s,
p9 =
p,
z =
ord a as
Real ;
per cases
( p <= s or s <= p )
;
suppose
p <= s
;
contradictionthen reconsider r1 =
s - p as
Element of
NAT by INT_1:18;
p > 0
by A3, A38, FINSEQ_1:3;
then A43:
z < z + p9
by XREAL_1:31;
s9 <= z
by A3, A39, FINSEQ_1:3;
then
s9 < z + p9
by A43, XXREAL_0:2;
then A44:
s9 - p9 < (z + p9) - p9
by XREAL_1:11;
1_ G = (a |^ s) * ((a |^ p) " )
by A40, A42, GROUP_1:def 6;
then
a |^ 0 = (a |^ s) * ((a |^ p) " )
by GROUP_1:43;
then
a |^ 0 = (a |^ s) * (a |^ (- p))
by GROUP_1:70;
then
a |^ 0 = a |^ (s + (- p))
by GROUP_1:63;
then A45:
1_ G = a |^ r1
by GROUP_1:43;
(
r1 <> 0 & not
a is
being_of_order_0 )
by A41, Th26;
hence
contradiction
by A45, A44, GROUP_1:def 12;
verum end; suppose
s <= p
;
contradictionthen reconsider r2 =
p - s as
Element of
NAT by INT_1:18;
s > 0
by A3, A39, FINSEQ_1:3;
then A46:
z < z + s9
by XREAL_1:31;
p9 <= z
by A3, A38, FINSEQ_1:3;
then
p9 < z + s9
by A46, XXREAL_0:2;
then A47:
p9 - s9 < (z + s9) - s9
by XREAL_1:11;
1_ G = (a |^ p) * ((a |^ s) " )
by A40, A42, GROUP_1:def 6;
then
a |^ 0 = (a |^ p) * ((a |^ s) " )
by GROUP_1:43;
then
a |^ 0 = (a |^ p) * (a |^ (- s))
by GROUP_1:70;
then
a |^ 0 = a |^ (p + (- s))
by GROUP_1:63;
then A48:
1_ G = a |^ r2
by GROUP_1:43;
(
r2 <> 0 & not
a is
being_of_order_0 )
by A41, Th26;
hence
contradiction
by A48, A47, GROUP_1:def 12;
verum end;
end;
then
Seg (ord a),the carrier of (gr {a}) are_equipotent
by A3, A37, WELLORD2:def 4;
then
card So = card the carrier of (gr {a})
by CARD_1:21;
hence
ord a = card (gr {a})
by FINSEQ_1:78; verum