:: Cayley's Theorem
:: by Artur Korni{\l}owicz
::
:: Received December 29, 2010
:: Copyright (c) 2010-2012 Association of Mizar Users


begin

registration
let X be set ;
cluster {} (X,{}) ->  onto ;
coherence
 {} (X,{}) is onto
proofend;
end;

registration
cluster permutational  ->  functional for set ;
coherence
 for b1 being set st b1 is permutational holds
b1 is functional
proofend;
end;

definition
let X be set ;
func permutations X ->  set  equals :: CAYLEY:def 1
 {  f where f is Permutation of X : verum  }  ;
coherence
  {  f where f is Permutation of X : verum  }  is set ;
end;

:: deftheorem  defines permutations CAYLEY:def_1_:_
 for X being set holds permutations X =  {  f where f is Permutation of X : verum  }  ;

theorem Th1: :: CAYLEY:1
for X, f being set st f in permutations X holds
f is Permutation of X
proofend;

theorem Th2: :: CAYLEY:2
for X being set holds permutations X c= Funcs (X,X)
proofend;

theorem Th3: :: CAYLEY:3
for n being Nat holds permutations (Seg n) = Permutations n
proofend;

registration
let X be set ;
cluster permutations X ->  non empty functional ;
coherence
 ( not permutations X is empty & permutations X is functional )
proofend;
end;

registration
let X be finite set ;
cluster permutations X ->  finite ;
coherence
 permutations X is finite
proofend;
end;

theorem Th4: :: CAYLEY:4
permutations {} = 1
proofend;

definition
let X be set ;
set c = permutations X;
func SymGroup X ->  strict constituted-Functions multMagma  means :Def2: :: CAYLEY:def 2
( the carrier of it = permutations X & ( for x, y being Element of it holds x * y = y * x ) );
existence
 ex b1 being strict constituted-Functions multMagma st
( the carrier of b1 = permutations X & ( for x, y being Element of b1 holds x * y = y * x ) )
proofend;
uniqueness
 for b1, b2 being strict constituted-Functions multMagma st the carrier of b1 = permutations X & ( for x, y being Element of b1 holds x * y = y * x ) & the carrier of b2 = permutations X & ( for x, y being Element of b2 holds x * y = y * x ) holds
b1 = b2
proofend;
end;

:: deftheorem Def2 defines SymGroup CAYLEY:def_2_:_
 for X being set
for b2 being strict constituted-Functions multMagma holds
( b2 = SymGroup X iff ( the carrier of b2 = permutations X & ( for x, y being Element of b2 holds x * y = y * x ) ) );

theorem Th5: :: CAYLEY:5
for X being set
for f being Element of (SymGroup X) holds f is Permutation of X
proofend;

registration
let X be set ;
cluster SymGroup X ->  non empty strict Group-like associative constituted-Functions ;
coherence
 ( not SymGroup X is empty & SymGroup X is associative & SymGroup X is Group-like )
proofend;
end;

theorem Th6: :: CAYLEY:6
for X being set holds 1_ (SymGroup X) = id X
proofend;

theorem :: CAYLEY:7
for X being set
for x being Element of (SymGroup X) holds x " = x "
proofend;

registration
let n be Nat;
cluster Group_of_Perm n ->  constituted-Functions ;
coherence
 Group_of_Perm n is constituted-Functions
proofend;
end;

theorem :: CAYLEY:8
for n being Nat holds SymGroup (Seg n) = Group_of_Perm n
proofend;

registration
let X be finite set ;
cluster SymGroup X ->  finite strict constituted-Functions ;
coherence
 SymGroup X is finite
proofend;
end;

theorem Th9: :: CAYLEY:9
SymGroup {} = Trivial-multMagma
proofend;

registration
cluster SymGroup {} ->  trivial strict constituted-Functions ;
coherence
 SymGroup {} is trivial by Th9, CARD_1:49;
end;

definition
let X, Y be set ;
let p be Function of X,Y;
assume that
B1: ( X <> {} &amp; Y <> {} ) and
B2: p is bijective ;
set G = SymGroup X;
set H = SymGroup Y;
func SymGroupsIso p ->  Function of (SymGroup X),(SymGroup Y) means :Def3: :: CAYLEY:def 3
 for x being Element of (SymGroup X) holds it . x = (p * x) * (p ");
existence
 ex b1 being Function of (SymGroup X),(SymGroup Y) st
for x being Element of (SymGroup X) holds b1 . x = (p * x) * (p ")
proofend;
uniqueness
 for b1, b2 being Function of (SymGroup X),(SymGroup Y) st ( for x being Element of (SymGroup X) holds b1 . x = (p * x) * (p ") ) &amp; ( for x being Element of (SymGroup X) holds b2 . x = (p * x) * (p ") ) holds
b1 = b2
proofend;
end;

:: deftheorem Def3 defines SymGroupsIso CAYLEY:def_3_:_
 for X, Y being set
for p being Function of X,Y st X <> {} &amp; Y <> {} &amp; p is bijective holds
for b4 being Function of (SymGroup X),(SymGroup Y) holds
( b4 = SymGroupsIso p iff for x being Element of (SymGroup X) holds b4 . x = (p * x) * (p ") );

theorem Th10: :: CAYLEY:10
for X, Y being non empty set
for p being Function of X,Y st p is bijective holds
SymGroupsIso p is multiplicative
proofend;

theorem Th11: :: CAYLEY:11
for X, Y being non empty set
for p being Function of X,Y st p is bijective holds
SymGroupsIso p is one-to-one
proofend;

theorem Th12: :: CAYLEY:12
for X, Y being non empty set
for p being Function of X,Y st p is bijective holds
SymGroupsIso p is onto
proofend;

theorem :: CAYLEY:13
for X, Y being set st X,Y are_equipotent holds
SymGroup X, SymGroup Y are_isomorphic
proofend;

definition
let G be Group;
func CayleyIso G ->  Function of G,(SymGroup the carrier of G) means :Def4: :: CAYLEY:def 4
 for g being Element of G holds it . g = * g;
existence
 ex b1 being Function of G,(SymGroup the carrier of G) st
for g being Element of G holds b1 . g = * g
proofend;
uniqueness
 for b1, b2 being Function of G,(SymGroup the carrier of G) st ( for g being Element of G holds b1 . g = * g ) &amp; ( for g being Element of G holds b2 . g = * g ) holds
b1 = b2
proofend;
end;

:: deftheorem Def4 defines CayleyIso CAYLEY:def_4_:_
 for G being Group
for b2 being Function of G,(SymGroup the carrier of G) holds
( b2 = CayleyIso G iff for g being Element of G holds b2 . g = * g );

registration
let G be Group;
cluster CayleyIso G ->  multiplicative ;
coherence
 CayleyIso G is multiplicative
proofend;
end;

registration
let G be Group;
cluster CayleyIso G ->  one-to-one ;
coherence
 CayleyIso G is one-to-one
proofend;
end;

:: [WP: ] Cayley_Theorem
theorem :: CAYLEY:14
for G being Group holds G, Image (CayleyIso G) are_isomorphic by GROUP_6:68;