:: by Hiroshi Yamazaki , Hiroyuki Okazaki , Kazuhisa Nakasho and Yasunari Shidama

::

:: Received October 7, 2013

:: Copyright (c) 2013-2018 Association of Mizar Users

definition

let G be finite Group;

{ (ord a) where a is Element of G : verum } is Subset of NAT

end;
func Ordset G -> Subset of NAT equals :: GROUP_18:def 1

{ (ord a) where a is Element of G : verum } ;

coherence { (ord a) where a is Element of G : verum } ;

{ (ord a) where a is Element of G : verum } is Subset of NAT

proof end;

:: deftheorem defines Ordset GROUP_18:def 1 :

for G being finite Group holds Ordset G = { (ord a) where a is Element of G : verum } ;

for G being finite Group holds Ordset G = { (ord a) where a is Element of G : verum } ;

registration
end;

theorem GROUP630: :: GROUP_18:2

for G being strict Group

for N being strict normal Subgroup of G st G is commutative holds

G ./. N is commutative

for N being strict normal Subgroup of G st G is commutative holds

G ./. N is commutative

proof end;

theorem GRCY26: :: GROUP_18:3

for G being finite Group

for a, b being Element of G holds

( b in gr {a} iff ex p being Element of NAT st b = a |^ p )

for a, b being Element of G holds

( b in gr {a} iff ex p being Element of NAT st b = a |^ p )

proof end;

theorem GRCY28: :: GROUP_18:4

for G being finite Group

for a being Element of G

for n, p, s being Element of NAT st card (gr {a}) = n & n = p * s holds

ord (a |^ p) = s

for a being Element of G

for n, p, s being Element of NAT st card (gr {a}) = n & n = p * s holds

ord (a |^ p) = s

proof end;

theorem GRCY212: :: GROUP_18:5

for k being Element of NAT

for G being finite Group

for a being Element of G holds

( gr {a} = gr {(a |^ k)} iff k gcd (ord a) = 1 )

for G being finite Group

for a being Element of G holds

( gr {a} = gr {(a |^ k)} iff k gcd (ord a) = 1 )

proof end;

theorem GRCY212A: :: GROUP_18:6

for k being Element of NAT

for G being finite Group

for a being Element of G st k gcd (ord a) = 1 holds

ord a = ord (a |^ k)

for G being finite Group

for a being Element of G st k gcd (ord a) = 1 holds

ord a = ord (a |^ k)

proof end;

theorem GRCY211: :: GROUP_18:7

for k being Element of NAT

for G being finite Group

for a being Element of G holds ord a divides k * (ord (a |^ k))

for G being finite Group

for a being Element of G holds ord a divides k * (ord (a |^ k))

proof end;

theorem GRCY212: :: GROUP_18:8

for G being Group

for a, b being Element of G st b in gr {a} holds

gr {b} is strict Subgroup of gr {a}

for a, b being Element of G st b in gr {a} holds

gr {b} is strict Subgroup of gr {a}

proof end;

definition

let G be strict commutative Group;

let x be Element of Subgroups G;

correctness

coherence

x is strict normal Subgroup of G;

end;
let x be Element of Subgroups G;

correctness

coherence

x is strict normal Subgroup of G;

proof end;

:: deftheorem defines modetrans GROUP_18:def 2 :

for G being strict commutative Group

for x being Element of Subgroups G holds modetrans x = x;

for G being strict commutative Group

for x being Element of Subgroups G holds modetrans x = x;

theorem GROUP252INV: :: GROUP_18:9

for G, H being Group

for K being Subgroup of H

for f being Homomorphism of G,H ex J being strict Subgroup of G st the carrier of J = f " the carrier of K

for K being Subgroup of H

for f being Homomorphism of G,H ex J being strict Subgroup of G st the carrier of J = f " the carrier of K

proof end;

theorem GRCY112: :: GROUP_18:10

for p being Nat

for G being finite Group

for x, d being Element of G st ord d = p & p is prime & x in gr {d} & not x = 1_ G holds

gr {x} = gr {d}

for G being finite Group

for x, d being Element of G st ord d = p & p is prime & x in gr {d} & not x = 1_ G holds

gr {x} = gr {d}

proof end;

theorem LM204D: :: GROUP_18:11

for G being Group

for H, K being normal Subgroup of G st the carrier of H /\ the carrier of K = {(1_ G)} holds

(nat_hom H) | the carrier of K is one-to-one

for H, K being normal Subgroup of G st the carrier of H /\ the carrier of K = {(1_ G)} holds

(nat_hom H) | the carrier of K is one-to-one

proof end;

theorem LM204L: :: GROUP_18:12

for G, F being finite commutative Group

for a being Element of G

for f being Homomorphism of G,F holds the carrier of (gr {(f . a)}) = f .: the carrier of (gr {a})

for a being Element of G

for f being Homomorphism of G,F holds the carrier of (gr {(f . a)}) = f .: the carrier of (gr {a})

proof end;

theorem LM204E: :: GROUP_18:13

for G, F being finite commutative Group

for a being Element of G

for f being Homomorphism of G,F holds ord (f . a) <= ord a

for a being Element of G

for f being Homomorphism of G,F holds ord (f . a) <= ord a

proof end;

theorem LM204F: :: GROUP_18:14

for G, F being finite commutative Group

for a being Element of G

for f being Homomorphism of G,F st f is one-to-one holds

ord (f . a) = ord a

for a being Element of G

for f being Homomorphism of G,F st f is one-to-one holds

ord (f . a) = ord a

proof end;

theorem LM204G: :: GROUP_18:15

for G, F being Group

for H being Subgroup of G

for f being Homomorphism of G,F holds f | the carrier of H is Homomorphism of H,F

for H being Subgroup of G

for f being Homomorphism of G,F holds f | the carrier of H is Homomorphism of H,F

proof end;

theorem LM204H: :: GROUP_18:16

for G, F being finite commutative Group

for a being Element of G

for f being Homomorphism of G,F st f | the carrier of (gr {a}) is one-to-one holds

ord (f . a) = ord a

for a being Element of G

for f being Homomorphism of G,F st f | the carrier of (gr {a}) is one-to-one holds

ord (f . a) = ord a

proof end;

theorem LM204I: :: GROUP_18:17

for G being finite commutative Group

for p being Prime

for m being Nat

for a being Element of G st card G = p |^ m & a <> 1_ G holds

ex n being Nat st ord a = p |^ (n + 1)

for p being Prime

for m being Nat

for a being Element of G st card G = p |^ m & a <> 1_ G holds

ex n being Nat st ord a = p |^ (n + 1)

proof end;

LM204K1: for p being Prime

for m, k being Nat st m divides p |^ k & m <> 1 holds

ex j being Nat st m = p |^ (j + 1)

proof end;

LM204A: for G being finite strict commutative Group

for p being Prime

for m being Nat

for g being Element of G st card G = p |^ m & ord g = upper_bound (Ordset G) holds

ex K being strict normal Subgroup of G st

( the carrier of K /\ the carrier of (gr {g}) = {(1_ G)} & ( for x being Element of G ex b1, a1 being Element of G st

( b1 in K & a1 in gr {g} & x = b1 * a1 ) ) )

proof end;

theorem LM204: :: GROUP_18:19

for G being finite strict commutative Group

for p being Prime

for m being Nat st card G = p |^ m holds

ex K being strict normal Subgroup of G ex n, k being Nat ex g being Element of G st

( ord g = upper_bound (Ordset G) & K is finite & K is commutative & the carrier of K /\ the carrier of (gr {g}) = {(1_ G)} & ( for x being Element of G ex b1, a1 being Element of G st

( b1 in K & a1 in gr {g} & x = b1 * a1 ) ) & ord g = p |^ n & k = m - n & n <= m & card K = p |^ k & ex F being Homomorphism of (product <*K,(gr {g})*>),G st

( F is bijective & ( for a, b being Element of G st a in K & b in gr {g} holds

F . <*a,b*> = a * b ) ) )

for p being Prime

for m being Nat st card G = p |^ m holds

ex K being strict normal Subgroup of G ex n, k being Nat ex g being Element of G st

( ord g = upper_bound (Ordset G) & K is finite & K is commutative & the carrier of K /\ the carrier of (gr {g}) = {(1_ G)} & ( for x being Element of G ex b1, a1 being Element of G st

( b1 in K & a1 in gr {g} & x = b1 * a1 ) ) & ord g = p |^ n & k = m - n & n <= m & card K = p |^ k & ex F being Homomorphism of (product <*K,(gr {g})*>),G st

( F is bijective & ( for a, b being Element of G st a in K & b in gr {g} holds

F . <*a,b*> = a * b ) ) )

proof end;

theorem LM205A: :: GROUP_18:20

for G being finite strict commutative Group

for p being Prime

for m being Nat st card G = p |^ m holds

ex k being non zero Nat ex a being b_{4} -element FinSequence of G ex Inda being b_{4} -element FinSequence of NAT ex F being Group-like associative commutative multMagma-Family of Seg k ex HFG being Homomorphism of (product F),G st

( ( for i being Nat st i in Seg k holds

ex ai being Element of G st

( ai = a . i & F . i = gr {ai} & ord ai = p |^ (Inda . i) ) ) & ( for i being Nat st 1 <= i & i <= k - 1 holds

Inda . i <= Inda . (i + 1) ) & ( for p, q being Element of Seg k st p <> q holds

the carrier of (F . p) /\ the carrier of (F . q) = {(1_ G)} ) & HFG is bijective & ( for x being Seg b_{4} -defined the carrier of b_{1} -valued total Function st ( for p being Element of Seg k holds x . p in F . p ) holds

( x in product F & HFG . x = Product x ) ) )

for p being Prime

for m being Nat st card G = p |^ m holds

ex k being non zero Nat ex a being b

( ( for i being Nat st i in Seg k holds

ex ai being Element of G st

( ai = a . i & F . i = gr {ai} & ord ai = p |^ (Inda . i) ) ) & ( for i being Nat st 1 <= i & i <= k - 1 holds

Inda . i <= Inda . (i + 1) ) & ( for p, q being Element of Seg k st p <> q holds

the carrier of (F . p) /\ the carrier of (F . q) = {(1_ G)} ) & HFG is bijective & ( for x being Seg b

( x in product F & HFG . x = Product x ) ) )

proof end;

XLM18Th401: for I being non empty finite set

for F being Group-like associative multMagma-Family of I

for x being set st x in the carrier of (product F) holds

x is b

proof end;

XLM18Th402: for I being non empty finite set

for F being Group-like associative multMagma-Family of I

for f being Function st f in the carrier of (product F) holds

for x being set st x in I holds

ex R being non empty multMagma st

( R = F . x & f . x in the carrier of R )

proof end;

theorem :: GROUP_18:21

for G being finite strict commutative Group

for p being Prime

for m being Nat st card G = p |^ m holds

ex k being non zero Nat ex a being b_{4} -element FinSequence of G ex Inda being b_{4} -element FinSequence of NAT ex F being Group-like associative commutative multMagma-Family of Seg k st

( ( for i being Nat st i in Seg k holds

ex ai being Element of G st

( ai = a . i & F . i = gr {ai} & ord ai = p |^ (Inda . i) ) ) & ( for i being Nat st 1 <= i & i <= k - 1 holds

Inda . i <= Inda . (i + 1) ) & ( for p, q being Element of Seg k st p <> q holds

the carrier of (F . p) /\ the carrier of (F . q) = {(1_ G)} ) & ( for y being Element of G ex x being Seg b_{4} -defined the carrier of b_{1} -valued total Function st

( ( for p being Element of Seg k holds x . p in F . p ) & y = Product x ) ) & ( for x1, x2 being Seg b_{4} -defined the carrier of b_{1} -valued total Function st ( for p being Element of Seg k holds x1 . p in F . p ) & ( for p being Element of Seg k holds x2 . p in F . p ) & Product x1 = Product x2 holds

x1 = x2 ) )

for p being Prime

for m being Nat st card G = p |^ m holds

ex k being non zero Nat ex a being b

( ( for i being Nat st i in Seg k holds

ex ai being Element of G st

( ai = a . i & F . i = gr {ai} & ord ai = p |^ (Inda . i) ) ) & ( for i being Nat st 1 <= i & i <= k - 1 holds

Inda . i <= Inda . (i + 1) ) & ( for p, q being Element of Seg k st p <> q holds

the carrier of (F . p) /\ the carrier of (F . q) = {(1_ G)} ) & ( for y being Element of G ex x being Seg b

( ( for p being Element of Seg k holds x . p in F . p ) & y = Product x ) ) & ( for x1, x2 being Seg b

x1 = x2 ) )

proof end;