:: CAYLEY semantic presentation begin registration let X be set ; cluster {} (X,{}) -> onto ; coherence {} (X,{}) is onto proof thus rng ({} (X,{})) = {} ; :: according to FUNCT_2:def_3 ::_thesis: verum end; end; registration cluster permutational -> functional for set ; coherence for b1 being set st b1 is permutational holds b1 is functional proof let X be set ; ::_thesis: ( X is permutational implies X is functional ) assume X is permutational ; ::_thesis: X is functional then A1: ex n being Nat st for x being set st x in X holds x is Permutation of (Seg n) by MATRIX_2:def_7; let x be set ; :: according to FUNCT_1:def_13 ::_thesis: ( not x in X or x is set ) thus ( not x in X or x is set ) by A1; ::_thesis: verum end; 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 proof let X, f be set ; ::_thesis: ( f in permutations X implies f is Permutation of X ) assume f in permutations X ; ::_thesis: f is Permutation of X then ex g being Permutation of X st g = f ; hence f is Permutation of X ; ::_thesis: verum end; theorem Th2: :: CAYLEY:2 for X being set holds permutations X c= Funcs (X,X) proof let X be set ; ::_thesis: permutations X c= Funcs (X,X) let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in permutations X or x in Funcs (X,X) ) assume x in permutations X ; ::_thesis: x in Funcs (X,X) then x is Permutation of X by Th1; hence x in Funcs (X,X) by FUNCT_2:9; ::_thesis: verum end; theorem Th3: :: CAYLEY:3 for n being Nat holds permutations (Seg n) = Permutations n proof let n be Nat; ::_thesis: permutations (Seg n) = Permutations n thus permutations (Seg n) c= Permutations n :: according to XBOOLE_0:def_10 ::_thesis: Permutations n c= permutations (Seg n) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in permutations (Seg n) or x in Permutations n ) assume x in permutations (Seg n) ; ::_thesis: x in Permutations n then x is Permutation of (Seg n) by Th1; hence x in Permutations n by MATRIX_2:def_9; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Permutations n or x in permutations (Seg n) ) assume x in Permutations n ; ::_thesis: x in permutations (Seg n) then x is Permutation of (Seg n) by MATRIX_2:def_9; hence x in permutations (Seg n) ; ::_thesis: verum end; registration let X be set ; cluster permutations X -> non empty functional ; coherence ( not permutations X is empty & permutations X is functional ) proof the Permutation of X in permutations X ; hence not permutations X is empty ; ::_thesis: permutations X is functional let x be set ; :: according to FUNCT_1:def_13 ::_thesis: ( not x in permutations X or x is set ) thus ( not x in permutations X or x is set ) by Th1; ::_thesis: verum end; end; registration let X be finite set ; cluster permutations X -> finite ; coherence permutations X is finite proof permutations X c= Funcs (X,X) by Th2; hence permutations X is finite ; ::_thesis: verum end; end; theorem Th4: :: CAYLEY:4 permutations {} = 1 proof set P = permutations {}; thus permutations {} c= 1 :: according to XBOOLE_0:def_10 ::_thesis: 1 c= permutations {} proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in permutations {} or x in 1 ) assume x in permutations {} ; ::_thesis: x in 1 then x is Permutation of {} by Th1; hence x in 1 by CARD_1:49, TARSKI:def_1; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in 1 or x in permutations {} ) assume x in 1 ; ::_thesis: x in permutations {} then x = {} ({},{}) by CARD_1:49, TARSKI:def_1; hence x in permutations {} ; ::_thesis: verum end; 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 ) ) proof defpred S1[ Element of permutations X, Element of permutations X, set ] means \$3 = \$2 * \$1; A1: for x, y being Element of permutations X ex z being Element of permutations X st S1[x,y,z] proof let x, y be Element of permutations X; ::_thesis: ex z being Element of permutations X st S1[x,y,z] reconsider f = x, g = y as Permutation of X by Th1; g * f in permutations X ; hence ex z being Element of permutations X st S1[x,y,z] ; ::_thesis: verum end; consider F being BinOp of (permutations X) such that A2: for x, y being Element of permutations X holds S1[x,y,F . (x,y)] from BINOP_1:sch_3(A1); set S = multMagma(# (permutations X),F #); multMagma(# (permutations X),F #) is constituted-Functions proof let x be Element of multMagma(# (permutations X),F #); :: according to MONOID_0:def_1 ::_thesis: x is set thus x is set ; ::_thesis: verum end; then reconsider S = multMagma(# (permutations X),F #) as strict constituted-Functions multMagma ; take S ; ::_thesis: ( the carrier of S = permutations X & ( for x, y being Element of S holds x * y = y * x ) ) thus the carrier of S = permutations X ; ::_thesis: for x, y being Element of S holds x * y = y * x let x, y be Element of S; ::_thesis: x * y = y * x thus x * y = y * x by A2; ::_thesis: verum end; 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 proof let A, B be strict constituted-Functions multMagma ; ::_thesis: ( the carrier of A = permutations X & ( for x, y being Element of A holds x * y = y * x ) & the carrier of B = permutations X & ( for x, y being Element of B holds x * y = y * x ) implies A = B ) assume that A3: the carrier of A = permutations X and A4: for x, y being Element of A holds x * y = y * x and A5: the carrier of B = permutations X and A6: for x, y being Element of B holds x * y = y * x ; ::_thesis: A = B now__::_thesis:_for_x,_y_being_Element_of_A_holds_the_multF_of_A_._(x,y)_=_the_multF_of_B_._(x,y) let x, y be Element of A; ::_thesis: the multF of A . (x,y) = the multF of B . (x,y) reconsider f = x, g = y as Element of B by A3, A5; thus the multF of A . (x,y) = x * y .= y * x by A4 .= f * g by A6 .= the multF of B . (x,y) ; ::_thesis: verum end; hence A = B by A3, A5, BINOP_1:2; ::_thesis: verum end; 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 proof let X be set ; ::_thesis: for f being Element of (SymGroup X) holds f is Permutation of X let f be Element of (SymGroup X); ::_thesis: f is Permutation of X the carrier of (SymGroup X) = permutations X by Def2; hence f is Permutation of X by Th1; ::_thesis: verum end; 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 ) proof the carrier of (SymGroup X) = permutations X by Def2; hence not the carrier of (SymGroup X) is empty ; :: according to STRUCT_0:def_1 ::_thesis: ( SymGroup X is associative & SymGroup X is Group-like ) thus SymGroup X is associative ::_thesis: SymGroup X is Group-like proof let x, y, z be Element of (SymGroup X); :: according to GROUP_1:def_3 ::_thesis: (x * y) * z = x * (y * z) thus (x * y) * z = z * (x * y) by Def2 .= z * (y * x) by Def2 .= (z * y) * x by RELAT_1:36 .= (y * z) * x by Def2 .= x * (y * z) by Def2 ; ::_thesis: verum end; set e = id X; id X in permutations X ; then reconsider e = id X as Element of (SymGroup X) by Def2; take e ; :: according to GROUP_1:def_2 ::_thesis: for b1 being Element of the carrier of (SymGroup X) holds ( b1 * e = b1 & e * b1 = b1 & ex b2 being Element of the carrier of (SymGroup X) st ( b1 * b2 = e & b2 * b1 = e ) ) let h be Element of (SymGroup X); ::_thesis: ( h * e = h & e * h = h & ex b1 being Element of the carrier of (SymGroup X) st ( h * b1 = e & b1 * h = e ) ) reconsider h1 = h as Permutation of X by Th5; thus h * e = e * h1 by Def2 .= h by FUNCT_2:17 ; ::_thesis: ( e * h = h & ex b1 being Element of the carrier of (SymGroup X) st ( h * b1 = e & b1 * h = e ) ) thus e * h = h1 * e by Def2 .= h by FUNCT_2:17 ; ::_thesis: ex b1 being Element of the carrier of (SymGroup X) st ( h * b1 = e & b1 * h = e ) h1 " in permutations X ; then reconsider g = h1 " as Element of (SymGroup X) by Def2; take g ; ::_thesis: ( h * g = e & g * h = e ) thus h * g = g * h by Def2 .= e by FUNCT_2:61 ; ::_thesis: g * h = e thus g * h = h * g by Def2 .= e by FUNCT_2:61 ; ::_thesis: verum end; end; theorem Th6: :: CAYLEY:6 for X being set holds 1_ (SymGroup X) = id X proof let X be set ; ::_thesis: 1_ (SymGroup X) = id X set e = id X; id X in permutations X ; then reconsider e = id X as Element of (SymGroup X) by Def2; now__::_thesis:_for_h_being_Element_of_(SymGroup_X)_holds_ (_h_*_e_=_h_&_e_*_h_=_h_) let h be Element of (SymGroup X); ::_thesis: ( h * e = h & e * h = h ) reconsider h1 = h as Permutation of X by Th5; thus h * e = e * h1 by Def2 .= h by FUNCT_2:17 ; ::_thesis: e * h = h thus e * h = h1 * e by Def2 .= h by FUNCT_2:17 ; ::_thesis: verum end; hence 1_ (SymGroup X) = id X by GROUP_1:4; ::_thesis: verum end; theorem :: CAYLEY:7 for X being set for x being Element of (SymGroup X) holds x " = x " proof let X be set ; ::_thesis: for x being Element of (SymGroup X) holds x " = x " let x be Element of (SymGroup X); ::_thesis: x " = x " reconsider f = x as Permutation of X by Th5; f " in permutations X ; then reconsider g = f " as Element of (SymGroup X) by Def2; A1: 1_ (SymGroup X) = id X by Th6; x * g = g * x by Def2; then A2: x * g = id X by FUNCT_2:61; g * x = x * g by Def2; then g * x = id X by FUNCT_2:61; hence x " = x " by A2, A1, GROUP_1:def_5; ::_thesis: verum end; registration let n be Nat; cluster Group_of_Perm n -> constituted-Functions ; coherence Group_of_Perm n is constituted-Functions proof let x be set ; :: according to MONOID_0:def_1 ::_thesis: ( x is Element of the carrier of (Group_of_Perm n) implies x is set ) the carrier of (Group_of_Perm n) = Permutations n by MATRIX_2:def_10; hence ( x is Element of the carrier of (Group_of_Perm n) implies x is set ) ; ::_thesis: verum end; end; theorem :: CAYLEY:8 for n being Nat holds SymGroup (Seg n) = Group_of_Perm n proof let n be Nat; ::_thesis: SymGroup (Seg n) = Group_of_Perm n A1: the carrier of (SymGroup (Seg n)) = permutations (Seg n) by Def2; A2: permutations (Seg n) = Permutations n by Th3 .= the carrier of (Group_of_Perm n) by MATRIX_2:def_10 ; now__::_thesis:_for_a,_b_being_Element_of_(SymGroup_(Seg_n))_holds_the_multF_of_(SymGroup_(Seg_n))_._(a,b)_=_the_multF_of_(Group_of_Perm_n)_._(a,b) let a, b be Element of (SymGroup (Seg n)); ::_thesis: the multF of (SymGroup (Seg n)) . (a,b) = the multF of (Group_of_Perm n) . (a,b) A3: a * b = b * a by Def2; ( a is Permutation of (Seg n) & b is Permutation of (Seg n) ) by Th5; then ( a in Permutations n & b in Permutations n ) by MATRIX_2:def_9; hence the multF of (SymGroup (Seg n)) . (a,b) = the multF of (Group_of_Perm n) . (a,b) by A3, MATRIX_2:def_10; ::_thesis: verum end; hence SymGroup (Seg n) = Group_of_Perm n by A1, A2, BINOP_1:2; ::_thesis: verum end; registration let X be finite set ; cluster SymGroup X -> finite strict constituted-Functions ; coherence SymGroup X is finite proof the carrier of (SymGroup X) = permutations X by Def2; hence the carrier of (SymGroup X) is finite ; :: according to STRUCT_0:def_11 ::_thesis: verum end; end; theorem Th9: :: CAYLEY:9 SymGroup {} = Trivial-multMagma proof set G = SymGroup {}; A1: the carrier of (SymGroup {}) = permutations {} by Def2; now__::_thesis:_for_x,_y_being_Element_of_1_holds_the_multF_of_(SymGroup_{})_._(x,y)_=_op2_._(x,y) let x, y be Element of 1; ::_thesis: the multF of (SymGroup {}) . (x,y) = op2 . (x,y) reconsider f = x, g = y as Element of (SymGroup {}) by Th4, Def2; thus the multF of (SymGroup {}) . (x,y) = f * g .= {} by A1, Th4, CARD_1:49, TARSKI:def_1 .= op2 . (x,y) by CARD_1:49, FUNCOP_1:77 ; ::_thesis: verum end; hence SymGroup {} = Trivial-multMagma by A1, Th4, BINOP_1:2; ::_thesis: verum end; 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 <> {} & 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 ") proof A1: dom p = X by B1, FUNCT_2:def_1; A2: rng p = Y by B2, FUNCT_2:def_3; reconsider p1 = p " as Function of Y,X by B2, A2, FUNCT_2:25; A3: rng p1 = X by B2, A1, FUNCT_1:33; defpred S1[ Function, set ] means \$2 = (p * \$1) * p1; A4: for x being Element of (SymGroup X) ex y being Element of (SymGroup Y) st S1[x,y] proof let x be Element of (SymGroup X); ::_thesis: ex y being Element of (SymGroup Y) st S1[x,y] reconsider f = x as Permutation of X by Th5; set y = (p * f) * p1; rng f = X by FUNCT_2:def_3; then rng (p * f) = Y by A2, B1, FUNCT_2:14; then rng ((p * f) * p1) = Y by B1, A3, FUNCT_2:14; then (p * f) * p1 is Permutation of Y by B2, B1, FUNCT_2:57; then (p * f) * p1 in permutations Y ; then reconsider y = (p * f) * p1 as Element of (SymGroup Y) by Def2; take y ; ::_thesis: S1[x,y] thus S1[x,y] ; ::_thesis: verum end; ex h being Function of (SymGroup X),(SymGroup Y) st for x being Element of (SymGroup X) holds S1[x,h . x] from FUNCT_2:sch_3(A4); hence ex b1 being Function of (SymGroup X),(SymGroup Y) st for x being Element of (SymGroup X) holds b1 . x = (p * x) * (p ") ; ::_thesis: verum end; 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 ") ) & ( for x being Element of (SymGroup X) holds b2 . x = (p * x) * (p ") ) holds b1 = b2 proof let f, g be Function of (SymGroup X),(SymGroup Y); ::_thesis: ( ( for x being Element of (SymGroup X) holds f . x = (p * x) * (p ") ) & ( for x being Element of (SymGroup X) holds g . x = (p * x) * (p ") ) implies f = g ) assume that A5: for x being Element of (SymGroup X) holds f . x = (p * x) * (p ") and A6: for x being Element of (SymGroup X) holds g . x = (p * x) * (p ") ; ::_thesis: f = g let x be Element of (SymGroup X); :: according to FUNCT_2:def_8 ::_thesis: f . x = g . x thus f . x = (p * x) * (p ") by A5 .= g . x by A6 ; ::_thesis: verum end; end; :: deftheorem Def3 defines SymGroupsIso CAYLEY:def_3_:_ for X, Y being set for p being Function of X,Y st X <> {} & Y <> {} & 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 proof let X, Y be non empty set ; ::_thesis: for p being Function of X,Y st p is bijective holds SymGroupsIso p is multiplicative let p be Function of X,Y; ::_thesis: ( p is bijective implies SymGroupsIso p is multiplicative ) assume A1: p is bijective ; ::_thesis: SymGroupsIso p is multiplicative set h = SymGroupsIso p; A2: rng p = Y by A1, FUNCT_2:def_3; let x, y be Element of (SymGroup X); :: according to GROUP_6:def_6 ::_thesis: (SymGroupsIso p) . (x * y) = ((SymGroupsIso p) . x) * ((SymGroupsIso p) . y) reconsider p1 = p " as Function of Y,X by A1, A2, FUNCT_2:25; A3: id X = p1 * p by A2, A1, FUNCT_2:29; A4: ( (SymGroupsIso p) . x = (p * x) * p1 & (SymGroupsIso p) . y = (p * y) * p1 ) by A1, Def3; reconsider f = x, g = y as Permutation of X by Th5; thus (SymGroupsIso p) . (x * y) = (p * (x * y)) * p1 by A1, Def3 .= (p * (g * f)) * p1 by Def2 .= (p * ((g * (id X)) * f)) * p1 by FUNCT_2:17 .= (p * (((g * p1) * p) * f)) * p1 by A3, RELAT_1:36 .= (p * ((g * p1) * (p * f))) * p1 by RELAT_1:36 .= ((p * (g * p1)) * (p * f)) * p1 by RELAT_1:36 .= (p * (g * p1)) * ((p * f) * p1) by RELAT_1:36 .= ((p * g) * p1) * ((p * f) * p1) by RELAT_1:36 .= ((SymGroupsIso p) . x) * ((SymGroupsIso p) . y) by A4, Def2 ; ::_thesis: verum end; 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 proof let X, Y be non empty set ; ::_thesis: for p being Function of X,Y st p is bijective holds SymGroupsIso p is one-to-one let p be Function of X,Y; ::_thesis: ( p is bijective implies SymGroupsIso p is one-to-one ) assume A1: p is bijective ; ::_thesis: SymGroupsIso p is one-to-one set h = SymGroupsIso p; A2: rng p = Y by A1, FUNCT_2:def_3; reconsider p1 = p " as Function of Y,X by A1, A2, FUNCT_2:25; A3: id X = p1 * p by A1, A2, FUNCT_2:29; let x, y be set ; :: according to FUNCT_1:def_4 ::_thesis: ( not x in dom (SymGroupsIso p) or not y in dom (SymGroupsIso p) or not (SymGroupsIso p) . x = (SymGroupsIso p) . y or x = y ) assume that A4: ( x in dom (SymGroupsIso p) & y in dom (SymGroupsIso p) ) and A5: (SymGroupsIso p) . x = (SymGroupsIso p) . y ; ::_thesis: x = y reconsider x = x, y = y as Element of (SymGroup X) by A4; reconsider f = x, g = y as Permutation of X by Th5; ( (SymGroupsIso p) . x = (p * f) * p1 & (SymGroupsIso p) . y = (p * g) * p1 ) by A1, Def3; then (p * f) * (p1 * p) = ((p * g) * p1) * p by A5, RELAT_1:36; then (p * f) * (p1 * p) = (p * g) * (p1 * p) by RELAT_1:36; then p * f = (p * g) * (id X) by A3, FUNCT_2:17; then p1 * (p * f) = p1 * (p * g) by FUNCT_2:17; then (p1 * p) * f = p1 * (p * g) by RELAT_1:36; then (p1 * p) * f = (p1 * p) * g by RELAT_1:36; then f = (id X) * g by A3, FUNCT_2:17; hence x = y by FUNCT_2:17; ::_thesis: verum end; 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 proof let X, Y be non empty set ; ::_thesis: for p being Function of X,Y st p is bijective holds SymGroupsIso p is onto let p be Function of X,Y; ::_thesis: ( p is bijective implies SymGroupsIso p is onto ) assume A1: p is bijective ; ::_thesis: SymGroupsIso p is onto set G = SymGroup X; set H = SymGroup Y; set h = SymGroupsIso p; A2: dom p = X by FUNCT_2:def_1; thus rng (SymGroupsIso p) c= the carrier of (SymGroup Y) ; :: according to XBOOLE_0:def_10,FUNCT_2:def_3 ::_thesis: the carrier of (SymGroup Y) c= rng (SymGroupsIso p) let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in the carrier of (SymGroup Y) or y in rng (SymGroupsIso p) ) assume y in the carrier of (SymGroup Y) ; ::_thesis: y in rng (SymGroupsIso p) then reconsider y = y as Element of (SymGroup Y) ; reconsider g = y as Permutation of Y by Th5; A3: rng p = Y by A1, FUNCT_2:def_3; then reconsider p1 = p " as Function of Y,X by A1, FUNCT_2:25; A4: id Y = p * p1 by A1, A3, FUNCT_2:29; A5: dom (SymGroupsIso p) = the carrier of (SymGroup X) by FUNCT_2:def_1; set x = (p1 * g) * p; A6: rng p1 = X by A1, A2, FUNCT_1:33; rng g = Y by FUNCT_2:def_3; then rng (p1 * g) = X by A6, FUNCT_2:14; then rng ((p1 * g) * p) = X by A3, FUNCT_2:14; then (p1 * g) * p is Permutation of X by A1, FUNCT_2:57; then (p1 * g) * p in permutations X ; then reconsider x = (p1 * g) * p as Element of (SymGroup X) by Def2; (SymGroupsIso p) . x = (p * x) * p1 by A1, Def3 .= ((p * (p1 * g)) * p) * p1 by RELAT_1:36 .= (p * (p1 * g)) * (p * p1) by RELAT_1:36 .= ((id Y) * g) * (id Y) by A4, RELAT_1:36 .= g * (id Y) by FUNCT_2:17 .= y by FUNCT_2:17 ; hence y in rng (SymGroupsIso p) by A5, FUNCT_1:def_3; ::_thesis: verum end; theorem :: CAYLEY:13 for X, Y being set st X,Y are_equipotent holds SymGroup X, SymGroup Y are_isomorphic proof let X, Y be set ; ::_thesis: ( X,Y are_equipotent implies SymGroup X, SymGroup Y are_isomorphic ) assume A1: X,Y are_equipotent ; ::_thesis: SymGroup X, SymGroup Y are_isomorphic then consider p being Function such that A2: p is one-to-one and A3: dom p = X and A4: rng p = Y by WELLORD2:def_4; percases ( X = {} or X <> {} ) ; suppose X = {} ; ::_thesis: SymGroup X, SymGroup Y are_isomorphic hence SymGroup X, SymGroup Y are_isomorphic by A1, CARD_1:26; ::_thesis: verum end; supposeA5: X <> {} ; ::_thesis: SymGroup X, SymGroup Y are_isomorphic then A6: Y <> {} by A1, CARD_1:26; reconsider p = p as Function of X,Y by A3, A4, FUNCT_2:2; A7: p is onto by A4, FUNCT_2:def_3; then reconsider h = SymGroupsIso p as Homomorphism of (SymGroup X),(SymGroup Y) by A2, A5, A6, Th10; take h ; :: according to GROUP_6:def_11 ::_thesis: h is bijective thus ( h is one-to-one & h is onto ) by A2, A5, A6, A7, Th11, Th12; :: according to FUNCT_2:def_4 ::_thesis: verum end; end; end; 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 proof set c = the carrier of G; defpred S1[ Element of G, set ] means \$2 = * \$1; A1: for x being Element of G ex y being Element of (SymGroup the carrier of G) st S1[x,y] proof let x be Element of G; ::_thesis: ex y being Element of (SymGroup the carrier of G) st S1[x,y] set y = * x; * x in permutations the carrier of G ; then reconsider y = * x as Element of (SymGroup the carrier of G) by Def2; take y ; ::_thesis: S1[x,y] thus S1[x,y] ; ::_thesis: verum end; ex f being Function of G,(SymGroup the carrier of G) st for x being Element of G holds S1[x,f . x] from FUNCT_2:sch_3(A1); hence ex b1 being Function of G,(SymGroup the carrier of G) st for g being Element of G holds b1 . g = * g ; ::_thesis: verum end; uniqueness for b1, b2 being Function of G,(SymGroup the carrier of G) st ( for g being Element of G holds b1 . g = * g ) & ( for g being Element of G holds b2 . g = * g ) holds b1 = b2 proof let a, b be Function of G,(SymGroup the carrier of G); ::_thesis: ( ( for g being Element of G holds a . g = * g ) & ( for g being Element of G holds b . g = * g ) implies a = b ) assume that A2: for g being Element of G holds a . g = * g and A3: for g being Element of G holds b . g = * g ; ::_thesis: a = b let x be Element of G; :: according to FUNCT_2:def_8 ::_thesis: a . x = b . x thus a . x = * x by A2 .= b . x by A3 ; ::_thesis: verum end; 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 proof set c = the carrier of G; set f = CayleyIso G; let g1, g2 be Element of G; :: according to GROUP_6:def_6 ::_thesis: (CayleyIso G) . (g1 * g2) = ((CayleyIso G) . g1) * ((CayleyIso G) . g2) A1: (CayleyIso G) . (g1 * g2) is Permutation of the carrier of G by Th5; then A2: dom ((CayleyIso G) . (g1 * g2)) = the carrier of G by FUNCT_2:def_1; ((CayleyIso G) . g1) * ((CayleyIso G) . g2) is Permutation of the carrier of G by Th5; then A3: dom (((CayleyIso G) . g1) * ((CayleyIso G) . g2)) = the carrier of G by FUNCT_2:def_1; now__::_thesis:_for_y_being_set_st_y_in_dom_((CayleyIso_G)_._(g1_*_g2))_holds_ ((CayleyIso_G)_._(g1_*_g2))_._y_=_(((CayleyIso_G)_._g1)_*_((CayleyIso_G)_._g2))_._y let y be set ; ::_thesis: ( y in dom ((CayleyIso G) . (g1 * g2)) implies ((CayleyIso G) . (g1 * g2)) . y = (((CayleyIso G) . g1) * ((CayleyIso G) . g2)) . y ) assume y in dom ((CayleyIso G) . (g1 * g2)) ; ::_thesis: ((CayleyIso G) . (g1 * g2)) . y = (((CayleyIso G) . g1) * ((CayleyIso G) . g2)) . y then reconsider x = y as Element of G by A1, FUNCT_2:def_1; thus ((CayleyIso G) . (g1 * g2)) . y = (* (g1 * g2)) . x by Def4 .= x * (g1 * g2) by TOPGRP_1:def_2 .= (x * g1) * g2 by GROUP_1:def_3 .= (* g2) . (x * g1) by TOPGRP_1:def_2 .= (* g2) . ((* g1) . x) by TOPGRP_1:def_2 .= ((* g2) * (* g1)) . x by FUNCT_2:15 .= (((CayleyIso G) . g2) * (* g1)) . x by Def4 .= (((CayleyIso G) . g2) * ((CayleyIso G) . g1)) . y by Def4 .= (((CayleyIso G) . g1) * ((CayleyIso G) . g2)) . y by Def2 ; ::_thesis: verum end; hence (CayleyIso G) . (g1 * g2) = ((CayleyIso G) . g1) * ((CayleyIso G) . g2) by A2, A3, FUNCT_1:2; ::_thesis: verum end; end; registration let G be Group; cluster CayleyIso G -> one-to-one ; coherence CayleyIso G is one-to-one proof set f = CayleyIso G; let g1, g2 be set ; :: according to FUNCT_1:def_4 ::_thesis: ( not g1 in dom (CayleyIso G) or not g2 in dom (CayleyIso G) or not (CayleyIso G) . g1 = (CayleyIso G) . g2 or g1 = g2 ) assume that A1: ( g1 in dom (CayleyIso G) & g2 in dom (CayleyIso G) ) and A2: (CayleyIso G) . g1 = (CayleyIso G) . g2 and A3: g1 <> g2 ; ::_thesis: contradiction reconsider g1 = g1, g2 = g2 as Element of G by A1; A4: ( (CayleyIso G) . g1 = * g1 & (CayleyIso G) . g2 = * g2 ) by Def4; A5: dom (* g1) = the carrier of G by FUNCT_2:def_1; A6: g1 " <> g2 " by A3, GROUP_1:9; A7: (* g1) . (g1 ") = (g1 ") * g1 by TOPGRP_1:def_2 .= 1_ G by GROUP_1:def_5 ; (* g2) . (g2 ") = (g2 ") * g2 by TOPGRP_1:def_2 .= 1_ G by GROUP_1:def_5 ; hence contradiction by A2, A4, A5, A6, A7, FUNCT_1:def_4; ::_thesis: verum end; end; theorem :: CAYLEY:14 for G being Group holds G, Image (CayleyIso G) are_isomorphic by GROUP_6:68;