:: AUTALG_1 semantic presentation begin theorem Th1: :: AUTALG_1:1 for UA being Universal_Algebra holds id the carrier of UA is_isomorphism UA,UA proof let UA be Universal_Algebra; ::_thesis: id the carrier of UA is_isomorphism UA,UA set I = id the carrier of UA; id the carrier of UA is_homomorphism UA,UA by ALG_1:5; hence id the carrier of UA is_monomorphism UA,UA by ALG_1:def_2; :: according to ALG_1:def_4 ::_thesis: id the carrier of UA is_epimorphism UA,UA ( id the carrier of UA is_homomorphism UA,UA & rng (id the carrier of UA) = the carrier of UA ) by ALG_1:5, RELAT_1:45; hence id the carrier of UA is_epimorphism UA,UA by ALG_1:def_3; ::_thesis: verum end; definition let UA be Universal_Algebra; func UAAut UA -> FUNCTION_DOMAIN of the carrier of UA, the carrier of UA means :Def1: :: AUTALG_1:def 1 for h being Function of UA,UA holds ( h in it iff h is_isomorphism UA,UA ); existence ex b1 being FUNCTION_DOMAIN of the carrier of UA, the carrier of UA st for h being Function of UA,UA holds ( h in b1 iff h is_isomorphism UA,UA ) proof set F = { x where x is Element of Funcs ( the carrier of UA, the carrier of UA) : x is_isomorphism UA,UA } ; A1: id the carrier of UA in { x where x is Element of Funcs ( the carrier of UA, the carrier of UA) : x is_isomorphism UA,UA } proof set I = id the carrier of UA; ( id the carrier of UA in Funcs ( the carrier of UA, the carrier of UA) & id the carrier of UA is_isomorphism UA,UA ) by Th1, FUNCT_2:8; hence id the carrier of UA in { x where x is Element of Funcs ( the carrier of UA, the carrier of UA) : x is_isomorphism UA,UA } ; ::_thesis: verum end; reconsider F = { x where x is Element of Funcs ( the carrier of UA, the carrier of UA) : x is_isomorphism UA,UA } as set ; F is functional proof let q be set ; :: according to FUNCT_1:def_13 ::_thesis: ( not q in F or q is set ) assume q in F ; ::_thesis: q is set then ex x being Element of Funcs ( the carrier of UA, the carrier of UA) st ( q = x & x is_isomorphism UA,UA ) ; hence q is set ; ::_thesis: verum end; then reconsider F = F as functional non empty set by A1; F is FUNCTION_DOMAIN of the carrier of UA, the carrier of UA proof let a be Element of F; :: according to FUNCT_2:def_12 ::_thesis: a is Element of bool [: the carrier of UA, the carrier of UA:] a in F ; then ex x being Element of Funcs ( the carrier of UA, the carrier of UA) st ( a = x & x is_isomorphism UA,UA ) ; hence a is Element of bool [: the carrier of UA, the carrier of UA:] ; ::_thesis: verum end; then reconsider F = F as FUNCTION_DOMAIN of the carrier of UA, the carrier of UA ; take F ; ::_thesis: for h being Function of UA,UA holds ( h in F iff h is_isomorphism UA,UA ) let h be Function of UA,UA; ::_thesis: ( h in F iff h is_isomorphism UA,UA ) thus ( h in F implies h is_isomorphism UA,UA ) ::_thesis: ( h is_isomorphism UA,UA implies h in F ) proof assume h in F ; ::_thesis: h is_isomorphism UA,UA then ex f being Element of Funcs ( the carrier of UA, the carrier of UA) st ( f = h & f is_isomorphism UA,UA ) ; hence h is_isomorphism UA,UA ; ::_thesis: verum end; A2: h is Element of Funcs ( the carrier of UA, the carrier of UA) by FUNCT_2:8; assume h is_isomorphism UA,UA ; ::_thesis: h in F hence h in F by A2; ::_thesis: verum end; uniqueness for b1, b2 being FUNCTION_DOMAIN of the carrier of UA, the carrier of UA st ( for h being Function of UA,UA holds ( h in b1 iff h is_isomorphism UA,UA ) ) & ( for h being Function of UA,UA holds ( h in b2 iff h is_isomorphism UA,UA ) ) holds b1 = b2 proof let F1, F2 be FUNCTION_DOMAIN of the carrier of UA, the carrier of UA; ::_thesis: ( ( for h being Function of UA,UA holds ( h in F1 iff h is_isomorphism UA,UA ) ) & ( for h being Function of UA,UA holds ( h in F2 iff h is_isomorphism UA,UA ) ) implies F1 = F2 ) assume that A3: for h being Function of UA,UA holds ( h in F1 iff h is_isomorphism UA,UA ) and A4: for h being Function of UA,UA holds ( h in F2 iff h is_isomorphism UA,UA ) ; ::_thesis: F1 = F2 A5: F2 c= F1 proof let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in F2 or q in F1 ) assume A6: q in F2 ; ::_thesis: q in F1 then reconsider h1 = q as Function of UA,UA by FUNCT_2:def_12; h1 is_isomorphism UA,UA by A4, A6; hence q in F1 by A3; ::_thesis: verum end; F1 c= F2 proof let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in F1 or q in F2 ) assume A7: q in F1 ; ::_thesis: q in F2 then reconsider h1 = q as Function of UA,UA by FUNCT_2:def_12; h1 is_isomorphism UA,UA by A3, A7; hence q in F2 by A4; ::_thesis: verum end; hence F1 = F2 by A5, XBOOLE_0:def_10; ::_thesis: verum end; end; :: deftheorem Def1 defines UAAut AUTALG_1:def_1_:_ for UA being Universal_Algebra for b2 being FUNCTION_DOMAIN of the carrier of UA, the carrier of UA holds ( b2 = UAAut UA iff for h being Function of UA,UA holds ( h in b2 iff h is_isomorphism UA,UA ) ); theorem :: AUTALG_1:2 for UA being Universal_Algebra holds UAAut UA c= Funcs ( the carrier of UA, the carrier of UA) proof let UA be Universal_Algebra; ::_thesis: UAAut UA c= Funcs ( the carrier of UA, the carrier of UA) let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in UAAut UA or q in Funcs ( the carrier of UA, the carrier of UA) ) assume q in UAAut UA ; ::_thesis: q in Funcs ( the carrier of UA, the carrier of UA) then ex f being Element of UAAut UA st f = q ; hence q in Funcs ( the carrier of UA, the carrier of UA) by FUNCT_2:9; ::_thesis: verum end; theorem Th3: :: AUTALG_1:3 for UA being Universal_Algebra holds id the carrier of UA in UAAut UA proof let UA be Universal_Algebra; ::_thesis: id the carrier of UA in UAAut UA id the carrier of UA is_isomorphism UA,UA by Th1; hence id the carrier of UA in UAAut UA by Def1; ::_thesis: verum end; theorem :: AUTALG_1:4 for UA being Universal_Algebra for f, g being Function of UA,UA st f is Element of UAAut UA & g = f " holds g is_isomorphism UA,UA proof let UA be Universal_Algebra; ::_thesis: for f, g being Function of UA,UA st f is Element of UAAut UA & g = f " holds g is_isomorphism UA,UA let f, g be Function of UA,UA; ::_thesis: ( f is Element of UAAut UA & g = f " implies g is_isomorphism UA,UA ) assume that A1: f is Element of UAAut UA and A2: g = f " ; ::_thesis: g is_isomorphism UA,UA f is_isomorphism UA,UA by A1, Def1; hence g is_isomorphism UA,UA by A2, ALG_1:10; ::_thesis: verum end; Lm1: for UA being Universal_Algebra for f being Function of UA,UA st f is_isomorphism UA,UA holds f " is Function of UA,UA proof let UA be Universal_Algebra; ::_thesis: for f being Function of UA,UA st f is_isomorphism UA,UA holds f " is Function of UA,UA let f be Function of UA,UA; ::_thesis: ( f is_isomorphism UA,UA implies f " is Function of UA,UA ) assume A1: f is_isomorphism UA,UA ; ::_thesis: f " is Function of UA,UA then f is_epimorphism UA,UA by ALG_1:def_4; then A2: rng f = the carrier of UA by ALG_1:def_3; f is one-to-one by A1, ALG_1:7; hence f " is Function of UA,UA by A2, FUNCT_2:25; ::_thesis: verum end; theorem Th5: :: AUTALG_1:5 for UA being Universal_Algebra for f being Element of UAAut UA holds f " in UAAut UA proof let UA be Universal_Algebra; ::_thesis: for f being Element of UAAut UA holds f " in UAAut UA let f be Element of UAAut UA; ::_thesis: f " in UAAut UA A1: f is_isomorphism UA,UA by Def1; then f " is Function of UA,UA by Lm1; then consider ff being Function of UA,UA such that A2: ff = f " ; ff is_isomorphism UA,UA by A1, A2, ALG_1:10; hence f " in UAAut UA by A2, Def1; ::_thesis: verum end; theorem Th6: :: AUTALG_1:6 for UA being Universal_Algebra for f1, f2 being Element of UAAut UA holds f1 * f2 in UAAut UA proof let UA be Universal_Algebra; ::_thesis: for f1, f2 being Element of UAAut UA holds f1 * f2 in UAAut UA let f1, f2 be Element of UAAut UA; ::_thesis: f1 * f2 in UAAut UA ( f1 is_isomorphism UA,UA & f2 is_isomorphism UA,UA ) by Def1; then f1 * f2 is_isomorphism UA,UA by ALG_1:11; hence f1 * f2 in UAAut UA by Def1; ::_thesis: verum end; definition let UA be Universal_Algebra; func UAAutComp UA -> BinOp of (UAAut UA) means :Def2: :: AUTALG_1:def 2 for x, y being Element of UAAut UA holds it . (x,y) = y * x; existence ex b1 being BinOp of (UAAut UA) st for x, y being Element of UAAut UA holds b1 . (x,y) = y * x proof defpred S1[ Element of UAAut UA, Element of UAAut UA, set ] means \$3 = \$2 * \$1; A1: for x, y being Element of UAAut UA ex m being Element of UAAut UA st S1[x,y,m] proof let x, y be Element of UAAut UA; ::_thesis: ex m being Element of UAAut UA st S1[x,y,m] reconsider xx = x, yy = y as Function of UA,UA ; reconsider m = yy * xx as Element of UAAut UA by Th6; take m ; ::_thesis: S1[x,y,m] thus S1[x,y,m] ; ::_thesis: verum end; thus ex IT being BinOp of (UAAut UA) st for x, y being Element of UAAut UA holds S1[x,y,IT . (x,y)] from BINOP_1:sch_3(A1); ::_thesis: verum end; uniqueness for b1, b2 being BinOp of (UAAut UA) st ( for x, y being Element of UAAut UA holds b1 . (x,y) = y * x ) & ( for x, y being Element of UAAut UA holds b2 . (x,y) = y * x ) holds b1 = b2 proof let b1, b2 be BinOp of (UAAut UA); ::_thesis: ( ( for x, y being Element of UAAut UA holds b1 . (x,y) = y * x ) & ( for x, y being Element of UAAut UA holds b2 . (x,y) = y * x ) implies b1 = b2 ) assume that A2: for x, y being Element of UAAut UA holds b1 . (x,y) = y * x and A3: for x, y being Element of UAAut UA holds b2 . (x,y) = y * x ; ::_thesis: b1 = b2 for x, y being Element of UAAut UA holds b1 . (x,y) = b2 . (x,y) proof let x, y be Element of UAAut UA; ::_thesis: b1 . (x,y) = b2 . (x,y) thus b1 . (x,y) = y * x by A2 .= b2 . (x,y) by A3 ; ::_thesis: verum end; hence b1 = b2 by BINOP_1:2; ::_thesis: verum end; end; :: deftheorem Def2 defines UAAutComp AUTALG_1:def_2_:_ for UA being Universal_Algebra for b2 being BinOp of (UAAut UA) holds ( b2 = UAAutComp UA iff for x, y being Element of UAAut UA holds b2 . (x,y) = y * x ); definition let UA be Universal_Algebra; func UAAutGroup UA -> Group equals :: AUTALG_1:def 3 multMagma(# (UAAut UA),(UAAutComp UA) #); coherence multMagma(# (UAAut UA),(UAAutComp UA) #) is Group proof set H = multMagma(# (UAAut UA),(UAAutComp UA) #); A1: ex e being Element of multMagma(# (UAAut UA),(UAAutComp UA) #) st for h being Element of multMagma(# (UAAut UA),(UAAutComp UA) #) holds ( h * e = h & e * h = h & ex g being Element of multMagma(# (UAAut UA),(UAAutComp UA) #) st ( h * g = e & g * h = e ) ) proof reconsider e = id the carrier of UA as Element of multMagma(# (UAAut UA),(UAAutComp UA) #) by Th3; take e ; ::_thesis: for h being Element of multMagma(# (UAAut UA),(UAAutComp UA) #) holds ( h * e = h & e * h = h & ex g being Element of multMagma(# (UAAut UA),(UAAutComp UA) #) st ( h * g = e & g * h = e ) ) let h be Element of multMagma(# (UAAut UA),(UAAutComp UA) #); ::_thesis: ( h * e = h & e * h = h & ex g being Element of multMagma(# (UAAut UA),(UAAutComp UA) #) st ( h * g = e & g * h = e ) ) consider A being Element of UAAut UA such that A2: A = h ; h * e = (id the carrier of UA) * A by A2, Def2 .= A by FUNCT_2:17 ; hence h * e = h by A2; ::_thesis: ( e * h = h & ex g being Element of multMagma(# (UAAut UA),(UAAutComp UA) #) st ( h * g = e & g * h = e ) ) e * h = A * (id the carrier of UA) by A2, Def2 .= A by FUNCT_2:17 ; hence e * h = h by A2; ::_thesis: ex g being Element of multMagma(# (UAAut UA),(UAAutComp UA) #) st ( h * g = e & g * h = e ) reconsider g = A " as Element of multMagma(# (UAAut UA),(UAAutComp UA) #) by Th5; take g ; ::_thesis: ( h * g = e & g * h = e ) A3: A is_isomorphism UA,UA by Def1; then A4: A is one-to-one by ALG_1:7; A is_epimorphism UA,UA by A3, ALG_1:def_4; then A5: rng A = the carrier of UA by ALG_1:def_3; thus h * g = (A ") * A by A2, Def2 .= e by A4, A5, FUNCT_2:29 ; ::_thesis: g * h = e thus g * h = A * (A ") by A2, Def2 .= e by A4, A5, FUNCT_2:29 ; ::_thesis: verum end; for f, g, h being Element of multMagma(# (UAAut UA),(UAAutComp UA) #) holds (f * g) * h = f * (g * h) proof let f, g, h be Element of multMagma(# (UAAut UA),(UAAutComp UA) #); ::_thesis: (f * g) * h = f * (g * h) reconsider A = f, B = g, C = h as Element of UAAut UA ; A6: g * h = C * B by Def2; f * g = B * A by Def2; hence (f * g) * h = C * (B * A) by Def2 .= (C * B) * A by RELAT_1:36 .= f * (g * h) by A6, Def2 ; ::_thesis: verum end; hence multMagma(# (UAAut UA),(UAAutComp UA) #) is Group by A1, GROUP_1:def_2, GROUP_1:def_3; ::_thesis: verum end; end; :: deftheorem defines UAAutGroup AUTALG_1:def_3_:_ for UA being Universal_Algebra holds UAAutGroup UA = multMagma(# (UAAut UA),(UAAutComp UA) #); registration let UA be Universal_Algebra; cluster UAAutGroup UA -> strict ; coherence UAAutGroup UA is strict ; end; Lm2: for UA being Universal_Algebra for f being Element of UAAut UA holds ( dom f = rng f & dom f = the carrier of UA ) proof let UA be Universal_Algebra; ::_thesis: for f being Element of UAAut UA holds ( dom f = rng f & dom f = the carrier of UA ) let f be Element of UAAut UA; ::_thesis: ( dom f = rng f & dom f = the carrier of UA ) A1: f is_isomorphism UA,UA by Def1; then dom f = the carrier of UA by ALG_1:8; hence ( dom f = rng f & dom f = the carrier of UA ) by A1, ALG_1:8; ::_thesis: verum end; theorem :: AUTALG_1:7 for UA being Universal_Algebra for x, y being Element of (UAAutGroup UA) for f, g being Element of UAAut UA st x = f & y = g holds x * y = g * f by Def2; theorem Th8: :: AUTALG_1:8 for UA being Universal_Algebra holds id the carrier of UA = 1_ (UAAutGroup UA) proof let UA be Universal_Algebra; ::_thesis: id the carrier of UA = 1_ (UAAutGroup UA) set f = the Element of (UAAutGroup UA); reconsider g = id the carrier of UA as Element of (UAAutGroup UA) by Th3; consider g1 being Function of the carrier of UA, the carrier of UA such that A1: g1 = g ; the Element of (UAAutGroup UA) is Element of UAAut UA ; then consider f1 being Function of the carrier of UA, the carrier of UA such that A2: f1 = the Element of (UAAutGroup UA) ; g * the Element of (UAAutGroup UA) = f1 * g1 by A1, A2, Def2 .= the Element of (UAAutGroup UA) by A1, A2, FUNCT_2:17 ; hence id the carrier of UA = 1_ (UAAutGroup UA) by GROUP_1:7; ::_thesis: verum end; theorem :: AUTALG_1:9 for UA being Universal_Algebra for f being Element of UAAut UA for g being Element of (UAAutGroup UA) st f = g holds f " = g " proof let UA be Universal_Algebra; ::_thesis: for f being Element of UAAut UA for g being Element of (UAAutGroup UA) st f = g holds f " = g " let f be Element of UAAut UA; ::_thesis: for g being Element of (UAAutGroup UA) st f = g holds f " = g " let g be Element of (UAAutGroup UA); ::_thesis: ( f = g implies f " = g " ) consider g1 being Element of UAAut UA such that A1: g1 = g " ; assume f = g ; ::_thesis: f " = g " then g1 * f = g * (g ") by A1, Def2; then g1 * f = 1_ (UAAutGroup UA) by GROUP_1:def_5; then A2: g1 * f = id the carrier of UA by Th8; f is_isomorphism UA,UA by Def1; then f is_monomorphism UA,UA by ALG_1:def_4; then A3: f is one-to-one by ALG_1:def_2; rng f = dom f by Lm2 .= the carrier of UA by Lm2 ; hence f " = g " by A1, A3, A2, FUNCT_2:30; ::_thesis: verum end; begin theorem :: AUTALG_1:10 for I being set for A, B, C being ManySortedSet of I st A is_transformable_to B & B is_transformable_to C holds A is_transformable_to C proof let I be set ; ::_thesis: for A, B, C being ManySortedSet of I st A is_transformable_to B & B is_transformable_to C holds A is_transformable_to C let A, B, C be ManySortedSet of I; ::_thesis: ( A is_transformable_to B & B is_transformable_to C implies A is_transformable_to C ) assume that A1: A is_transformable_to B and A2: B is_transformable_to C ; ::_thesis: A is_transformable_to C let i be set ; :: according to PZFMISC1:def_3 ::_thesis: ( not i in I or not C . i = {} or A . i = {} ) assume A3: i in I ; ::_thesis: ( not C . i = {} or A . i = {} ) then ( B . i = {} implies A . i = {} ) by A1, PZFMISC1:def_3; hence ( not C . i = {} or A . i = {} ) by A2, A3, PZFMISC1:def_3; ::_thesis: verum end; theorem Th11: :: AUTALG_1:11 for x being set for A being ManySortedSet of {x} holds A = x .--> (A . x) proof let x be set ; ::_thesis: for A being ManySortedSet of {x} holds A = x .--> (A . x) let A be ManySortedSet of {x}; ::_thesis: A = x .--> (A . x) A1: dom A = {x} by PARTFUN1:def_2; then rng A = {(A . x)} by FUNCT_1:4; hence A = x .--> (A . x) by A1, FUNCOP_1:9; ::_thesis: verum end; theorem Th12: :: AUTALG_1:12 for I being set for A, B being V2() ManySortedSet of I for F being ManySortedFunction of A,B st F is "1-1" & F is "onto" holds ( F "" is "1-1" & F "" is "onto" ) proof let I be set ; ::_thesis: for A, B being V2() ManySortedSet of I for F being ManySortedFunction of A,B st F is "1-1" & F is "onto" holds ( F "" is "1-1" & F "" is "onto" ) let A, B be V2() ManySortedSet of I; ::_thesis: for F being ManySortedFunction of A,B st F is "1-1" & F is "onto" holds ( F "" is "1-1" & F "" is "onto" ) let F be ManySortedFunction of A,B; ::_thesis: ( F is "1-1" & F is "onto" implies ( F "" is "1-1" & F "" is "onto" ) ) assume A1: ( F is "1-1" & F is "onto" ) ; ::_thesis: ( F "" is "1-1" & F "" is "onto" ) now__::_thesis:_for_i_being_set_st_i_in_I_holds_ (F_"")_._i_is_one-to-one let i be set ; ::_thesis: ( i in I implies (F "") . i is one-to-one ) assume A2: i in I ; ::_thesis: (F "") . i is one-to-one then reconsider g = F . i as Function of (A . i),(B . i) by PBOOLE:def_15; g is one-to-one by A1, A2, MSUALG_3:1; then g " is one-to-one ; hence (F "") . i is one-to-one by A1, A2, MSUALG_3:def_4; ::_thesis: verum end; hence F "" is "1-1" by MSUALG_3:1; ::_thesis: F "" is "onto" thus F "" is "onto" ::_thesis: verum proof let i be set ; :: according to MSUALG_3:def_3 ::_thesis: ( not i in I or rng ((F "") . i) = A . i ) assume A3: i in I ; ::_thesis: rng ((F "") . i) = A . i then reconsider g = F . i as Function of (A . i),(B . i) by PBOOLE:def_15; A4: g is one-to-one by A1, A3, MSUALG_3:1; A . i = dom g by A3, FUNCT_2:def_1 .= rng (g ") by A4, FUNCT_1:33 ; hence rng ((F "") . i) = A . i by A1, A3, MSUALG_3:def_4; ::_thesis: verum end; end; theorem :: AUTALG_1:13 for I being set for A, B being V2() ManySortedSet of I for F being ManySortedFunction of A,B st F is "1-1" & F is "onto" holds (F "") "" = F proof let I be set ; ::_thesis: for A, B being V2() ManySortedSet of I for F being ManySortedFunction of A,B st F is "1-1" & F is "onto" holds (F "") "" = F let A, B be V2() ManySortedSet of I; ::_thesis: for F being ManySortedFunction of A,B st F is "1-1" & F is "onto" holds (F "") "" = F let F be ManySortedFunction of A,B; ::_thesis: ( F is "1-1" & F is "onto" implies (F "") "" = F ) assume A1: ( F is "1-1" & F is "onto" ) ; ::_thesis: (F "") "" = F now__::_thesis:_for_i_being_set_st_i_in_I_holds_ ((F_"")_"")_._i_=_F_._i let i be set ; ::_thesis: ( i in I implies ((F "") "") . i = F . i ) assume A2: i in I ; ::_thesis: ((F "") "") . i = F . i then reconsider f = F . i as Function of (A . i),(B . i) by PBOOLE:def_15; reconsider f9 = (F "") . i as Function of (B . i),(A . i) by A2, PBOOLE:def_15; f is one-to-one by A1, A2, MSUALG_3:1; then A3: (f ") " = f by FUNCT_1:43; ( F "" is "1-1" & F "" is "onto" ) by A1, Th12; then ((F "") "") . i = f9 " by A2, MSUALG_3:def_4; hence ((F "") "") . i = F . i by A1, A2, A3, MSUALG_3:def_4; ::_thesis: verum end; hence (F "") "" = F by PBOOLE:3; ::_thesis: verum end; theorem Th14: :: AUTALG_1:14 for F, G being Function-yielding Function st F is "1-1" & G is "1-1" holds G ** F is "1-1" proof let F, G be Function-yielding Function; ::_thesis: ( F is "1-1" & G is "1-1" implies G ** F is "1-1" ) assume that A1: F is "1-1" and A2: G is "1-1" ; ::_thesis: G ** F is "1-1" let i be set ; :: according to MSUALG_3:def_2 ::_thesis: for b1 being set holds ( not i in dom (G ** F) or not (G ** F) . i = b1 or b1 is one-to-one ) let f be Function; ::_thesis: ( not i in dom (G ** F) or not (G ** F) . i = f or f is one-to-one ) assume that A3: i in dom (G ** F) and A4: (G ** F) . i = f ; ::_thesis: f is one-to-one A5: dom (G ** F) = (dom G) /\ (dom F) by PBOOLE:def_19; then i in dom F by A3, XBOOLE_0:def_4; then A6: F . i is one-to-one by A1, MSUALG_3:def_2; i in dom G by A3, A5, XBOOLE_0:def_4; then G . i is one-to-one by A2, MSUALG_3:def_2; then (G . i) * (F . i) is one-to-one by A6; hence f is one-to-one by A3, A4, PBOOLE:def_19; ::_thesis: verum end; theorem Th15: :: AUTALG_1:15 for I being set for A being ManySortedSet of I for B, C being V2() ManySortedSet of I for F being ManySortedFunction of A,B for G being ManySortedFunction of B,C st F is "onto" & G is "onto" holds G ** F is "onto" proof let I be set ; ::_thesis: for A being ManySortedSet of I for B, C being V2() ManySortedSet of I for F being ManySortedFunction of A,B for G being ManySortedFunction of B,C st F is "onto" & G is "onto" holds G ** F is "onto" let A be ManySortedSet of I; ::_thesis: for B, C being V2() ManySortedSet of I for F being ManySortedFunction of A,B for G being ManySortedFunction of B,C st F is "onto" & G is "onto" holds G ** F is "onto" let B, C be V2() ManySortedSet of I; ::_thesis: for F being ManySortedFunction of A,B for G being ManySortedFunction of B,C st F is "onto" & G is "onto" holds G ** F is "onto" let F be ManySortedFunction of A,B; ::_thesis: for G being ManySortedFunction of B,C st F is "onto" & G is "onto" holds G ** F is "onto" let G be ManySortedFunction of B,C; ::_thesis: ( F is "onto" & G is "onto" implies G ** F is "onto" ) assume A1: ( F is "onto" & G is "onto" ) ; ::_thesis: G ** F is "onto" now__::_thesis:_for_i_being_set_st_i_in_I_holds_ rng_((G_**_F)_._i)_=_C_._i let i be set ; ::_thesis: ( i in I implies rng ((G ** F) . i) = C . i ) assume A2: i in I ; ::_thesis: rng ((G ** F) . i) = C . i then reconsider f = F . i as Function of (A . i),(B . i) by PBOOLE:def_15; reconsider g = G . i as Function of (B . i),(C . i) by A2, PBOOLE:def_15; ( rng f = B . i & rng g = C . i ) by A1, A2, MSUALG_3:def_3; then rng (g * f) = C . i by A2, FUNCT_2:14; hence rng ((G ** F) . i) = C . i by A2, MSUALG_3:2; ::_thesis: verum end; hence G ** F is "onto" by MSUALG_3:def_3; ::_thesis: verum end; theorem :: AUTALG_1:16 for I being set for A, B, C being V2() ManySortedSet of I for F being ManySortedFunction of A,B for G being ManySortedFunction of B,C st F is "1-1" & F is "onto" & G is "1-1" & G is "onto" holds (G ** F) "" = (F "") ** (G "") proof let I be set ; ::_thesis: for A, B, C being V2() ManySortedSet of I for F being ManySortedFunction of A,B for G being ManySortedFunction of B,C st F is "1-1" & F is "onto" & G is "1-1" & G is "onto" holds (G ** F) "" = (F "") ** (G "") let A, B, C be V2() ManySortedSet of I; ::_thesis: for F being ManySortedFunction of A,B for G being ManySortedFunction of B,C st F is "1-1" & F is "onto" & G is "1-1" & G is "onto" holds (G ** F) "" = (F "") ** (G "") let F be ManySortedFunction of A,B; ::_thesis: for G being ManySortedFunction of B,C st F is "1-1" & F is "onto" & G is "1-1" & G is "onto" holds (G ** F) "" = (F "") ** (G "") let G be ManySortedFunction of B,C; ::_thesis: ( F is "1-1" & F is "onto" & G is "1-1" & G is "onto" implies (G ** F) "" = (F "") ** (G "") ) assume that A1: ( F is "1-1" & F is "onto" ) and A2: ( G is "1-1" & G is "onto" ) ; ::_thesis: (G ** F) "" = (F "") ** (G "") now__::_thesis:_for_i_being_set_st_i_in_I_holds_ ((G_**_F)_"")_._i_=_((F_"")_**_(G_""))_._i let i be set ; ::_thesis: ( i in I implies ((G ** F) "") . i = ((F "") ** (G "")) . i ) assume A3: i in I ; ::_thesis: ((G ** F) "") . i = ((F "") ** (G "")) . i then reconsider f = F . i as Function of (A . i),(B . i) by PBOOLE:def_15; A4: f is one-to-one by A1, A3, MSUALG_3:1; reconsider g = G . i as Function of (B . i),(C . i) by A3, PBOOLE:def_15; A5: g is one-to-one by A2, A3, MSUALG_3:1; ( (F "") . i = f " & rng f = B . i ) by A1, A3, MSUALG_3:def_3, MSUALG_3:def_4; then reconsider ff = (F "") . i as Function of (B . i),(A . i) by A4, FUNCT_2:25; A6: ( G ** F is "1-1" & G ** F is "onto" ) by A1, A2, Th14, Th15; (G ** F) . i = g * f by A3, MSUALG_3:2; then A7: ((G ** F) "") . i = (g * f) " by A3, A6, MSUALG_3:def_4; ( (G "") . i = g " & rng g = C . i ) by A2, A3, MSUALG_3:def_3, MSUALG_3:def_4; then reconsider gg = (G "") . i as Function of (C . i),(B . i) by A5, FUNCT_2:25; ((F "") ** (G "")) . i = ff * gg by A3, MSUALG_3:2 .= ff * (g ") by A2, A3, MSUALG_3:def_4 .= (f ") * (g ") by A1, A3, MSUALG_3:def_4 ; hence ((G ** F) "") . i = ((F "") ** (G "")) . i by A4, A5, A7, FUNCT_1:44; ::_thesis: verum end; hence (G ** F) "" = (F "") ** (G "") by PBOOLE:3; ::_thesis: verum end; theorem Th17: :: AUTALG_1:17 for I being set for A, B being V2() ManySortedSet of I for F being ManySortedFunction of A,B for G being ManySortedFunction of B,A st F is "1-1" & F is "onto" & G ** F = id A holds G = F "" proof let I be set ; ::_thesis: for A, B being V2() ManySortedSet of I for F being ManySortedFunction of A,B for G being ManySortedFunction of B,A st F is "1-1" & F is "onto" & G ** F = id A holds G = F "" let A, B be V2() ManySortedSet of I; ::_thesis: for F being ManySortedFunction of A,B for G being ManySortedFunction of B,A st F is "1-1" & F is "onto" & G ** F = id A holds G = F "" let F be ManySortedFunction of A,B; ::_thesis: for G being ManySortedFunction of B,A st F is "1-1" & F is "onto" & G ** F = id A holds G = F "" let G be ManySortedFunction of B,A; ::_thesis: ( F is "1-1" & F is "onto" & G ** F = id A implies G = F "" ) assume that A1: F is "1-1" and A2: F is "onto" and A3: G ** F = id A ; ::_thesis: G = F "" now__::_thesis:_for_i_being_set_st_i_in_I_holds_ G_._i_=_(F_"")_._i let i be set ; ::_thesis: ( i in I implies G . i = (F "") . i ) assume A4: i in I ; ::_thesis: G . i = (F "") . i then reconsider f = F . i as Function of (A . i),(B . i) by PBOOLE:def_15; A5: f is one-to-one by A1, A4, MSUALG_3:1; reconsider g = G . i as Function of (B . i),(A . i) by A4, PBOOLE:def_15; (G ** F) . i = id (A . i) by A3, A4, MSUALG_3:def_1; then A6: g * f = id (A . i) by A4, MSUALG_3:2; ( (F "") . i = f " & rng f = B . i ) by A1, A2, A4, MSUALG_3:def_3, MSUALG_3:def_4; hence G . i = (F "") . i by A4, A6, A5, FUNCT_2:30; ::_thesis: verum end; hence G = F "" by PBOOLE:3; ::_thesis: verum end; theorem Th18: :: AUTALG_1:18 for I being set for A, B being ManySortedSet of I st A is_transformable_to B holds (Funcs) (A,B) is V2() proof let I be set ; ::_thesis: for A, B being ManySortedSet of I st A is_transformable_to B holds (Funcs) (A,B) is V2() let A, B be ManySortedSet of I; ::_thesis: ( A is_transformable_to B implies (Funcs) (A,B) is V2() ) assume A1: A is_transformable_to B ; ::_thesis: (Funcs) (A,B) is V2() A2: for i being set st i in I holds Funcs ((A . i),(B . i)) <> {} proof let i be set ; ::_thesis: ( i in I implies Funcs ((A . i),(B . i)) <> {} ) assume i in I ; ::_thesis: Funcs ((A . i),(B . i)) <> {} then ( B . i = {} implies A . i = {} ) by A1, PZFMISC1:def_3; hence Funcs ((A . i),(B . i)) <> {} by FUNCT_2:8; ::_thesis: verum end; for i being set st i in I holds ((Funcs) (A,B)) . i <> {} proof let i be set ; ::_thesis: ( i in I implies ((Funcs) (A,B)) . i <> {} ) assume A3: i in I ; ::_thesis: ((Funcs) (A,B)) . i <> {} then ((Funcs) (A,B)) . i = Funcs ((A . i),(B . i)) by PBOOLE:def_17; hence ((Funcs) (A,B)) . i <> {} by A2, A3; ::_thesis: verum end; then for i being set st i in I holds not ((Funcs) (A,B)) . i is empty ; hence (Funcs) (A,B) is V2() by PBOOLE:def_13; ::_thesis: verum end; definition let I be set ; let A, B be ManySortedSet of I; assume A1: A is_transformable_to B ; func MSFuncs (A,B) -> non empty set equals :Def4: :: AUTALG_1:def 4 product ((Funcs) (A,B)); coherence product ((Funcs) (A,B)) is non empty set proof (Funcs) (A,B) is V2() by A1, Th18; then not {} in rng ((Funcs) (A,B)) by PBOOLE:137; hence product ((Funcs) (A,B)) is non empty set by CARD_3:26; ::_thesis: verum end; end; :: deftheorem Def4 defines MSFuncs AUTALG_1:def_4_:_ for I being set for A, B being ManySortedSet of I st A is_transformable_to B holds MSFuncs (A,B) = product ((Funcs) (A,B)); theorem Th19: :: AUTALG_1:19 for I being set for A, B being ManySortedSet of I st A is_transformable_to B holds for x being set st x in MSFuncs (A,B) holds x is ManySortedFunction of A,B proof let I be set ; ::_thesis: for A, B being ManySortedSet of I st A is_transformable_to B holds for x being set st x in MSFuncs (A,B) holds x is ManySortedFunction of A,B let A, B be ManySortedSet of I; ::_thesis: ( A is_transformable_to B implies for x being set st x in MSFuncs (A,B) holds x is ManySortedFunction of A,B ) assume A1: A is_transformable_to B ; ::_thesis: for x being set st x in MSFuncs (A,B) holds x is ManySortedFunction of A,B set f = (Funcs) (A,B); let x be set ; ::_thesis: ( x in MSFuncs (A,B) implies x is ManySortedFunction of A,B ) assume x in MSFuncs (A,B) ; ::_thesis: x is ManySortedFunction of A,B then x in product ((Funcs) (A,B)) by A1, Def4; then consider g being Function such that A2: x = g and A3: dom g = dom ((Funcs) (A,B)) and A4: for i being set st i in dom ((Funcs) (A,B)) holds g . i in ((Funcs) (A,B)) . i by CARD_3:def_5; A5: dom ((Funcs) (A,B)) = I by PARTFUN1:def_2; A6: for i being set st i in I holds g . i in Funcs ((A . i),(B . i)) proof let i be set ; ::_thesis: ( i in I implies g . i in Funcs ((A . i),(B . i)) ) assume A7: i in I ; ::_thesis: g . i in Funcs ((A . i),(B . i)) then ((Funcs) (A,B)) . i = Funcs ((A . i),(B . i)) by PBOOLE:def_17; hence g . i in Funcs ((A . i),(B . i)) by A4, A5, A7; ::_thesis: verum end; A8: for i being set st i in I holds ex F being Function st ( F = g . i & dom F = A . i & rng F c= B . i ) proof let i be set ; ::_thesis: ( i in I implies ex F being Function st ( F = g . i & dom F = A . i & rng F c= B . i ) ) assume i in I ; ::_thesis: ex F being Function st ( F = g . i & dom F = A . i & rng F c= B . i ) then g . i in Funcs ((A . i),(B . i)) by A6; hence ex F being Function st ( F = g . i & dom F = A . i & rng F c= B . i ) by FUNCT_2:def_2; ::_thesis: verum end; A9: for i being set st i in I holds g . i is Function of (A . i),(B . i) proof let i be set ; ::_thesis: ( i in I implies g . i is Function of (A . i),(B . i) ) assume A10: i in I ; ::_thesis: g . i is Function of (A . i),(B . i) ex F being Function st ( F = g . i & dom F = A . i & rng F c= B . i ) by A8, A10; hence g . i is Function of (A . i),(B . i) by FUNCT_2:2; ::_thesis: verum end; dom g = I by A3, PARTFUN1:def_2; then g is ManySortedSet of I by PARTFUN1:def_2, RELAT_1:def_18; hence x is ManySortedFunction of A,B by A2, A9, PBOOLE:def_15; ::_thesis: verum end; theorem Th20: :: AUTALG_1:20 for I being set for A, B being ManySortedSet of I st A is_transformable_to B holds for g being ManySortedFunction of A,B holds g in MSFuncs (A,B) proof let I be set ; ::_thesis: for A, B being ManySortedSet of I st A is_transformable_to B holds for g being ManySortedFunction of A,B holds g in MSFuncs (A,B) let A, B be ManySortedSet of I; ::_thesis: ( A is_transformable_to B implies for g being ManySortedFunction of A,B holds g in MSFuncs (A,B) ) assume A1: A is_transformable_to B ; ::_thesis: for g being ManySortedFunction of A,B holds g in MSFuncs (A,B) set f = (Funcs) (A,B); let g be ManySortedFunction of A,B; ::_thesis: g in MSFuncs (A,B) A2: dom ((Funcs) (A,B)) = I by PARTFUN1:def_2; A3: now__::_thesis:_for_x_being_set_st_x_in_dom_((Funcs)_(A,B))_holds_ g_._x_in_((Funcs)_(A,B))_._x let x be set ; ::_thesis: ( x in dom ((Funcs) (A,B)) implies g . x in ((Funcs) (A,B)) . x ) assume A4: x in dom ((Funcs) (A,B)) ; ::_thesis: g . x in ((Funcs) (A,B)) . x then reconsider i = x as Element of I by PARTFUN1:def_2; A5: g . i is Function of (A . i),(B . i) by A2, A4, PBOOLE:def_15; ( B . i = {} implies A . i = {} ) by A1, A2, A4, PZFMISC1:def_3; then g . i in Funcs ((A . i),(B . i)) by A5, FUNCT_2:8; hence g . x in ((Funcs) (A,B)) . x by A2, A4, PBOOLE:def_17; ::_thesis: verum end; dom g = I by PARTFUN1:def_2; then g in product ((Funcs) (A,B)) by A2, A3, CARD_3:9; hence g in MSFuncs (A,B) by A1, Def4; ::_thesis: verum end; registration let I be set ; let A be ManySortedSet of I; cluster (Funcs) (A,A) -> V2() ; coherence (Funcs) (A,A) is non-empty proof for i being set st i in I holds not ((Funcs) (A,A)) . i is empty proof let i be set ; ::_thesis: ( i in I implies not ((Funcs) (A,A)) . i is empty ) assume A1: i in I ; ::_thesis: not ((Funcs) (A,A)) . i is empty then (id A) . i is Function of (A . i),(A . i) by PBOOLE:def_15; then (id A) . i in Funcs ((A . i),(A . i)) by FUNCT_2:9; hence not ((Funcs) (A,A)) . i is empty by A1, PBOOLE:def_17; ::_thesis: verum end; hence (Funcs) (A,A) is non-empty by PBOOLE:def_13; ::_thesis: verum end; end; definition let I be set ; let D be ManySortedSet of I; let A be non empty Subset of (MSFuncs (D,D)); :: original: Element redefine mode Element of A -> ManySortedFunction of D,D; coherence for b1 being Element of A holds b1 is ManySortedFunction of D,D proof let f be Element of A; ::_thesis: f is ManySortedFunction of D,D thus f is ManySortedFunction of D,D by Th19; ::_thesis: verum end; end; registration let I be set ; let A be ManySortedSet of I; cluster id A -> "onto" ; coherence id A is "onto" proof let i be set ; :: according to MSUALG_3:def_3 ::_thesis: ( not i in I or rng ((id A) . i) = A . i ) assume i in I ; ::_thesis: rng ((id A) . i) = A . i then (id A) . i = id (A . i) by MSUALG_3:def_1; hence rng ((id A) . i) = A . i by RELAT_1:45; ::_thesis: verum end; cluster id A -> "1-1" ; coherence id A is "1-1" proof now__::_thesis:_for_i_being_set_st_i_in_I_holds_ (id_A)_._i_is_one-to-one let i be set ; ::_thesis: ( i in I implies (id A) . i is one-to-one ) assume i in I ; ::_thesis: (id A) . i is one-to-one then (id A) . i = id (A . i) by MSUALG_3:def_1; hence (id A) . i is one-to-one ; ::_thesis: verum end; hence id A is "1-1" by MSUALG_3:1; ::_thesis: verum end; end; begin definition let S be non empty non void ManySortedSign ; let U1, U2 be non-empty MSAlgebra over S; mode MSFunctionSet of U1,U2 is non empty Subset of (MSFuncs ( the Sorts of U1, the Sorts of U2)); end; theorem :: AUTALG_1:21 for S being non empty non void ManySortedSign for U1 being non-empty MSAlgebra over S holds id the Sorts of U1 in MSFuncs ( the Sorts of U1, the Sorts of U1) by Th20; definition let S be non empty non void ManySortedSign ; let U1 be non-empty MSAlgebra over S; set T = the Sorts of U1; func MSAAut U1 -> MSFunctionSet of U1,U1 means :Def5: :: AUTALG_1:def 5 for h being ManySortedFunction of U1,U1 holds ( h in it iff h is_isomorphism U1,U1 ); existence ex b1 being MSFunctionSet of U1,U1 st for h being ManySortedFunction of U1,U1 holds ( h in b1 iff h is_isomorphism U1,U1 ) proof defpred S1[ set ] means ex msf being ManySortedFunction of U1,U1 st ( \$1 = msf & msf is_isomorphism U1,U1 ); consider X being set such that A1: for x being set holds ( x in X iff ( x in MSFuncs ( the Sorts of U1, the Sorts of U1) & S1[x] ) ) from XBOOLE_0:sch_1(); A2: X c= MSFuncs ( the Sorts of U1, the Sorts of U1) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X or x in MSFuncs ( the Sorts of U1, the Sorts of U1) ) thus ( not x in X or x in MSFuncs ( the Sorts of U1, the Sorts of U1) ) by A1; ::_thesis: verum end; ( id the Sorts of U1 in MSFuncs ( the Sorts of U1, the Sorts of U1) & ex F being ManySortedFunction of U1,U1 st ( id the Sorts of U1 = F & F is_isomorphism U1,U1 ) ) by Th20, MSUALG_3:16; then reconsider X = X as MSFunctionSet of U1,U1 by A1, A2; take X ; ::_thesis: for h being ManySortedFunction of U1,U1 holds ( h in X iff h is_isomorphism U1,U1 ) let h be ManySortedFunction of U1,U1; ::_thesis: ( h in X iff h is_isomorphism U1,U1 ) hereby ::_thesis: ( h is_isomorphism U1,U1 implies h in X ) assume h in X ; ::_thesis: h is_isomorphism U1,U1 then ex msf being ManySortedFunction of U1,U1 st ( h = msf & msf is_isomorphism U1,U1 ) by A1; hence h is_isomorphism U1,U1 ; ::_thesis: verum end; h in MSFuncs ( the Sorts of U1, the Sorts of U1) by Th20; hence ( h is_isomorphism U1,U1 implies h in X ) by A1; ::_thesis: verum end; uniqueness for b1, b2 being MSFunctionSet of U1,U1 st ( for h being ManySortedFunction of U1,U1 holds ( h in b1 iff h is_isomorphism U1,U1 ) ) & ( for h being ManySortedFunction of U1,U1 holds ( h in b2 iff h is_isomorphism U1,U1 ) ) holds b1 = b2 proof let F1, F2 be MSFunctionSet of U1,U1; ::_thesis: ( ( for h being ManySortedFunction of U1,U1 holds ( h in F1 iff h is_isomorphism U1,U1 ) ) & ( for h being ManySortedFunction of U1,U1 holds ( h in F2 iff h is_isomorphism U1,U1 ) ) implies F1 = F2 ) assume that A3: for h being ManySortedFunction of U1,U1 holds ( h in F1 iff h is_isomorphism U1,U1 ) and A4: for h being ManySortedFunction of U1,U1 holds ( h in F2 iff h is_isomorphism U1,U1 ) ; ::_thesis: F1 = F2 thus F1 c= F2 :: according to XBOOLE_0:def_10 ::_thesis: F2 c= F1 proof let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in F1 or q in F2 ) assume A5: q in F1 ; ::_thesis: q in F2 then reconsider h1 = q as ManySortedFunction of U1,U1 by Th19; h1 is_isomorphism U1,U1 by A3, A5; hence q in F2 by A4; ::_thesis: verum end; let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in F2 or q in F1 ) assume A6: q in F2 ; ::_thesis: q in F1 then reconsider h1 = q as ManySortedFunction of U1,U1 by Th19; h1 is_isomorphism U1,U1 by A4, A6; hence q in F1 by A3; ::_thesis: verum end; end; :: deftheorem Def5 defines MSAAut AUTALG_1:def_5_:_ for S being non empty non void ManySortedSign for U1 being non-empty MSAlgebra over S for b3 being MSFunctionSet of U1,U1 holds ( b3 = MSAAut U1 iff for h being ManySortedFunction of U1,U1 holds ( h in b3 iff h is_isomorphism U1,U1 ) ); theorem :: AUTALG_1:22 for S being non empty non void ManySortedSign for U1 being non-empty MSAlgebra over S for f being Element of MSAAut U1 holds f in MSFuncs ( the Sorts of U1, the Sorts of U1) by Th20; theorem :: AUTALG_1:23 for S being non empty non void ManySortedSign for U1 being non-empty MSAlgebra over S holds MSAAut U1 c= MSFuncs ( the Sorts of U1, the Sorts of U1) ; Lm3: for S being non empty non void ManySortedSign for U1 being non-empty MSAlgebra over S for f being Element of MSAAut U1 holds ( f is "1-1" & f is "onto" ) proof let S be non empty non void ManySortedSign ; ::_thesis: for U1 being non-empty MSAlgebra over S for f being Element of MSAAut U1 holds ( f is "1-1" & f is "onto" ) let U1 be non-empty MSAlgebra over S; ::_thesis: for f being Element of MSAAut U1 holds ( f is "1-1" & f is "onto" ) let f be Element of MSAAut U1; ::_thesis: ( f is "1-1" & f is "onto" ) f is_isomorphism U1,U1 by Def5; hence ( f is "1-1" & f is "onto" ) by MSUALG_3:13; ::_thesis: verum end; theorem Th24: :: AUTALG_1:24 for S being non empty non void ManySortedSign for U1 being non-empty MSAlgebra over S holds id the Sorts of U1 in MSAAut U1 proof let S be non empty non void ManySortedSign ; ::_thesis: for U1 being non-empty MSAlgebra over S holds id the Sorts of U1 in MSAAut U1 let U1 be non-empty MSAlgebra over S; ::_thesis: id the Sorts of U1 in MSAAut U1 id the Sorts of U1 is_isomorphism U1,U1 by MSUALG_3:16; hence id the Sorts of U1 in MSAAut U1 by Def5; ::_thesis: verum end; theorem Th25: :: AUTALG_1:25 for S being non empty non void ManySortedSign for U1 being non-empty MSAlgebra over S for f being Element of MSAAut U1 holds f "" in MSAAut U1 proof let S be non empty non void ManySortedSign ; ::_thesis: for U1 being non-empty MSAlgebra over S for f being Element of MSAAut U1 holds f "" in MSAAut U1 let U1 be non-empty MSAlgebra over S; ::_thesis: for f being Element of MSAAut U1 holds f "" in MSAAut U1 let f be Element of MSAAut U1; ::_thesis: f "" in MSAAut U1 f is_isomorphism U1,U1 by Def5; then f "" is_isomorphism U1,U1 by MSUALG_3:14; hence f "" in MSAAut U1 by Def5; ::_thesis: verum end; theorem Th26: :: AUTALG_1:26 for S being non empty non void ManySortedSign for U1 being non-empty MSAlgebra over S for f1, f2 being Element of MSAAut U1 holds f1 ** f2 in MSAAut U1 proof let S be non empty non void ManySortedSign ; ::_thesis: for U1 being non-empty MSAlgebra over S for f1, f2 being Element of MSAAut U1 holds f1 ** f2 in MSAAut U1 let U1 be non-empty MSAlgebra over S; ::_thesis: for f1, f2 being Element of MSAAut U1 holds f1 ** f2 in MSAAut U1 let f1, f2 be Element of MSAAut U1; ::_thesis: f1 ** f2 in MSAAut U1 ( f1 is_isomorphism U1,U1 & f2 is_isomorphism U1,U1 ) by Def5; then f1 ** f2 is_isomorphism U1,U1 by MSUALG_3:15; hence f1 ** f2 in MSAAut U1 by Def5; ::_thesis: verum end; theorem Th27: :: AUTALG_1:27 for UA being Universal_Algebra for F being ManySortedFunction of (MSAlg UA),(MSAlg UA) for f being Element of UAAut UA st F = 0 .--> f holds F in MSAAut (MSAlg UA) proof let UA be Universal_Algebra; ::_thesis: for F being ManySortedFunction of (MSAlg UA),(MSAlg UA) for f being Element of UAAut UA st F = 0 .--> f holds F in MSAAut (MSAlg UA) let F be ManySortedFunction of (MSAlg UA),(MSAlg UA); ::_thesis: for f being Element of UAAut UA st F = 0 .--> f holds F in MSAAut (MSAlg UA) let f be Element of UAAut UA; ::_thesis: ( F = 0 .--> f implies F in MSAAut (MSAlg UA) ) assume F = 0 .--> f ; ::_thesis: F in MSAAut (MSAlg UA) then A1: F = MSAlg f by MSUHOM_1:def_3; f is_isomorphism UA,UA by Def1; then MSAlg f is_isomorphism MSAlg UA,(MSAlg UA) Over (MSSign UA) by MSUHOM_1:20; then F is_isomorphism MSAlg UA, MSAlg UA by A1, MSUHOM_1:9; hence F in MSAAut (MSAlg UA) by Def5; ::_thesis: verum end; definition let S be non empty non void ManySortedSign ; let U1 be non-empty MSAlgebra over S; func MSAAutComp U1 -> BinOp of (MSAAut U1) means :Def6: :: AUTALG_1:def 6 for x, y being Element of MSAAut U1 holds it . (x,y) = y ** x; existence ex b1 being BinOp of (MSAAut U1) st for x, y being Element of MSAAut U1 holds b1 . (x,y) = y ** x proof defpred S1[ Element of MSAAut U1, Element of MSAAut U1, set ] means \$3 = \$2 ** \$1; A1: for x, y being Element of MSAAut U1 ex m being Element of MSAAut U1 st S1[x,y,m] proof let x, y be Element of MSAAut U1; ::_thesis: ex m being Element of MSAAut U1 st S1[x,y,m] reconsider xx = x, yy = y as ManySortedFunction of U1,U1 ; reconsider m = yy ** xx as Element of MSAAut U1 by Th26; take m ; ::_thesis: S1[x,y,m] thus S1[x,y,m] ; ::_thesis: verum end; thus ex IT being BinOp of (MSAAut U1) st for x, y being Element of MSAAut U1 holds S1[x,y,IT . (x,y)] from BINOP_1:sch_3(A1); ::_thesis: verum end; uniqueness for b1, b2 being BinOp of (MSAAut U1) st ( for x, y being Element of MSAAut U1 holds b1 . (x,y) = y ** x ) & ( for x, y being Element of MSAAut U1 holds b2 . (x,y) = y ** x ) holds b1 = b2 proof let b1, b2 be BinOp of (MSAAut U1); ::_thesis: ( ( for x, y being Element of MSAAut U1 holds b1 . (x,y) = y ** x ) & ( for x, y being Element of MSAAut U1 holds b2 . (x,y) = y ** x ) implies b1 = b2 ) assume that A2: for x, y being Element of MSAAut U1 holds b1 . (x,y) = y ** x and A3: for x, y being Element of MSAAut U1 holds b2 . (x,y) = y ** x ; ::_thesis: b1 = b2 for x, y being Element of MSAAut U1 holds b1 . (x,y) = b2 . (x,y) proof let x, y be Element of MSAAut U1; ::_thesis: b1 . (x,y) = b2 . (x,y) thus b1 . (x,y) = y ** x by A2 .= b2 . (x,y) by A3 ; ::_thesis: verum end; hence b1 = b2 by BINOP_1:2; ::_thesis: verum end; end; :: deftheorem Def6 defines MSAAutComp AUTALG_1:def_6_:_ for S being non empty non void ManySortedSign for U1 being non-empty MSAlgebra over S for b3 being BinOp of (MSAAut U1) holds ( b3 = MSAAutComp U1 iff for x, y being Element of MSAAut U1 holds b3 . (x,y) = y ** x ); definition let S be non empty non void ManySortedSign ; let U1 be non-empty MSAlgebra over S; func MSAAutGroup U1 -> Group equals :: AUTALG_1:def 7 multMagma(# (MSAAut U1),(MSAAutComp U1) #); coherence multMagma(# (MSAAut U1),(MSAAutComp U1) #) is Group proof set SO = the Sorts of U1; set H = multMagma(# (MSAAut U1),(MSAAutComp U1) #); A1: ex e being Element of multMagma(# (MSAAut U1),(MSAAutComp U1) #) st for h being Element of multMagma(# (MSAAut U1),(MSAAutComp U1) #) holds ( h * e = h & e * h = h & ex g being Element of multMagma(# (MSAAut U1),(MSAAutComp U1) #) st ( h * g = e & g * h = e ) ) proof reconsider e = id the Sorts of U1 as Element of multMagma(# (MSAAut U1),(MSAAutComp U1) #) by Th24; take e ; ::_thesis: for h being Element of multMagma(# (MSAAut U1),(MSAAutComp U1) #) holds ( h * e = h & e * h = h & ex g being Element of multMagma(# (MSAAut U1),(MSAAutComp U1) #) st ( h * g = e & g * h = e ) ) let h be Element of multMagma(# (MSAAut U1),(MSAAutComp U1) #); ::_thesis: ( h * e = h & e * h = h & ex g being Element of multMagma(# (MSAAut U1),(MSAAutComp U1) #) st ( h * g = e & g * h = e ) ) consider A being Element of MSAAut U1 such that A2: A = h ; h * e = (id the Sorts of U1) ** A by A2, Def6 .= A by MSUALG_3:4 ; hence h * e = h by A2; ::_thesis: ( e * h = h & ex g being Element of multMagma(# (MSAAut U1),(MSAAutComp U1) #) st ( h * g = e & g * h = e ) ) e * h = A ** (id the Sorts of U1) by A2, Def6 .= A by MSUALG_3:3 ; hence e * h = h by A2; ::_thesis: ex g being Element of multMagma(# (MSAAut U1),(MSAAutComp U1) #) st ( h * g = e & g * h = e ) reconsider g = A "" as Element of multMagma(# (MSAAut U1),(MSAAutComp U1) #) by Th25; take g ; ::_thesis: ( h * g = e & g * h = e ) A3: ( A is "onto" & A is "1-1" ) by Lm3; thus h * g = (A "") ** A by A2, Def6 .= e by A3, MSUALG_3:5 ; ::_thesis: g * h = e thus g * h = A ** (A "") by A2, Def6 .= e by A3, MSUALG_3:5 ; ::_thesis: verum end; for f, g, h being Element of multMagma(# (MSAAut U1),(MSAAutComp U1) #) holds (f * g) * h = f * (g * h) proof let f, g, h be Element of multMagma(# (MSAAut U1),(MSAAutComp U1) #); ::_thesis: (f * g) * h = f * (g * h) reconsider A = f, B = g, C = h as Element of MSAAut U1 ; A4: g * h = C ** B by Def6; f * g = B ** A by Def6; hence (f * g) * h = C ** (B ** A) by Def6 .= (C ** B) ** A by PBOOLE:140 .= f * (g * h) by A4, Def6 ; ::_thesis: verum end; hence multMagma(# (MSAAut U1),(MSAAutComp U1) #) is Group by A1, GROUP_1:def_2, GROUP_1:def_3; ::_thesis: verum end; end; :: deftheorem defines MSAAutGroup AUTALG_1:def_7_:_ for S being non empty non void ManySortedSign for U1 being non-empty MSAlgebra over S holds MSAAutGroup U1 = multMagma(# (MSAAut U1),(MSAAutComp U1) #); registration let S be non empty non void ManySortedSign ; let U1 be non-empty MSAlgebra over S; cluster MSAAutGroup U1 -> strict ; coherence MSAAutGroup U1 is strict ; end; theorem :: AUTALG_1:28 for S being non empty non void ManySortedSign for U1 being non-empty MSAlgebra over S for x, y being Element of (MSAAutGroup U1) for f, g being Element of MSAAut U1 st x = f & y = g holds x * y = g ** f by Def6; theorem Th29: :: AUTALG_1:29 for S being non empty non void ManySortedSign for U1 being non-empty MSAlgebra over S holds id the Sorts of U1 = 1_ (MSAAutGroup U1) proof let S be non empty non void ManySortedSign ; ::_thesis: for U1 being non-empty MSAlgebra over S holds id the Sorts of U1 = 1_ (MSAAutGroup U1) let U1 be non-empty MSAlgebra over S; ::_thesis: id the Sorts of U1 = 1_ (MSAAutGroup U1) set T = the Sorts of U1; set f = the Element of (MSAAutGroup U1); reconsider g = id the Sorts of U1 as Element of (MSAAutGroup U1) by Th24; consider g1 being ManySortedFunction of the Sorts of U1, the Sorts of U1 such that A1: g1 = g ; the Element of (MSAAutGroup U1) is Element of MSAAut U1 ; then consider f1 being ManySortedFunction of the Sorts of U1, the Sorts of U1 such that A2: f1 = the Element of (MSAAutGroup U1) ; g * the Element of (MSAAutGroup U1) = f1 ** g1 by A1, A2, Def6 .= the Element of (MSAAutGroup U1) by A1, A2, MSUALG_3:3 ; hence id the Sorts of U1 = 1_ (MSAAutGroup U1) by GROUP_1:7; ::_thesis: verum end; theorem :: AUTALG_1:30 for S being non empty non void ManySortedSign for U1 being non-empty MSAlgebra over S for f being Element of MSAAut U1 for g being Element of (MSAAutGroup U1) st f = g holds f "" = g " proof let S be non empty non void ManySortedSign ; ::_thesis: for U1 being non-empty MSAlgebra over S for f being Element of MSAAut U1 for g being Element of (MSAAutGroup U1) st f = g holds f "" = g " let U1 be non-empty MSAlgebra over S; ::_thesis: for f being Element of MSAAut U1 for g being Element of (MSAAutGroup U1) st f = g holds f "" = g " let f be Element of MSAAut U1; ::_thesis: for g being Element of (MSAAutGroup U1) st f = g holds f "" = g " let g be Element of (MSAAutGroup U1); ::_thesis: ( f = g implies f "" = g " ) consider g1 being Element of MSAAut U1 such that A1: g1 = g " ; assume f = g ; ::_thesis: f "" = g " then g1 ** f = g * (g ") by A1, Def6; then g1 ** f = 1_ (MSAAutGroup U1) by GROUP_1:def_5; then A2: g1 ** f = id the Sorts of U1 by Th29; ( f is "1-1" & f is "onto" ) by Lm3; hence f "" = g " by A1, A2, Th17; ::_thesis: verum end; begin theorem Th31: :: AUTALG_1:31 for UA1, UA2 being Universal_Algebra st UA1,UA2 are_similar holds for F being ManySortedFunction of (MSAlg UA1),((MSAlg UA2) Over (MSSign UA1)) holds F . 0 is Function of UA1,UA2 proof let UA1, UA2 be Universal_Algebra; ::_thesis: ( UA1,UA2 are_similar implies for F being ManySortedFunction of (MSAlg UA1),((MSAlg UA2) Over (MSSign UA1)) holds F . 0 is Function of UA1,UA2 ) A1: 0 in {0} by TARSKI:def_1; assume UA1,UA2 are_similar ; ::_thesis: for F being ManySortedFunction of (MSAlg UA1),((MSAlg UA2) Over (MSSign UA1)) holds F . 0 is Function of UA1,UA2 then MSSign UA1 = MSSign UA2 by MSUHOM_1:10; then A2: ( MSAlg UA2 = MSAlgebra(# (MSSorts UA2),(MSCharact UA2) #) & (MSAlg UA2) Over (MSSign UA1) = MSAlg UA2 ) by MSUALG_1:def_11, MSUHOM_1:9; let F be ManySortedFunction of (MSAlg UA1),((MSAlg UA2) Over (MSSign UA1)); ::_thesis: F . 0 is Function of UA1,UA2 A3: ( the carrier of (MSSign UA1) = {0} & MSAlg UA1 = MSAlgebra(# (MSSorts UA1),(MSCharact UA1) #) ) by MSUALG_1:def_8, MSUALG_1:def_11; A4: (MSSorts UA2) . 0 = (0 .--> the carrier of UA2) . 0 by MSUALG_1:def_9 .= the carrier of UA2 by A1, FUNCOP_1:7 ; (MSSorts UA1) . 0 = (0 .--> the carrier of UA1) . 0 by MSUALG_1:def_9 .= the carrier of UA1 by A1, FUNCOP_1:7 ; hence F . 0 is Function of UA1,UA2 by A1, A3, A4, A2, PBOOLE:def_15; ::_thesis: verum end; theorem Th32: :: AUTALG_1:32 for UA being Universal_Algebra for f being Element of UAAut UA holds 0 .--> f is ManySortedFunction of (MSAlg UA),(MSAlg UA) proof let UA be Universal_Algebra; ::_thesis: for f being Element of UAAut UA holds 0 .--> f is ManySortedFunction of (MSAlg UA),(MSAlg UA) let f be Element of UAAut UA; ::_thesis: 0 .--> f is ManySortedFunction of (MSAlg UA),(MSAlg UA) MSAlg f is ManySortedFunction of (MSAlg UA),(MSAlg UA) by MSUHOM_1:9; hence 0 .--> f is ManySortedFunction of (MSAlg UA),(MSAlg UA) by MSUHOM_1:def_3; ::_thesis: verum end; Lm4: for UA being Universal_Algebra for h being Function st dom h = UAAut UA & ( for x being set st x in UAAut UA holds h . x = 0 .--> x ) holds rng h = MSAAut (MSAlg UA) proof let UA be Universal_Algebra; ::_thesis: for h being Function st dom h = UAAut UA & ( for x being set st x in UAAut UA holds h . x = 0 .--> x ) holds rng h = MSAAut (MSAlg UA) let h be Function; ::_thesis: ( dom h = UAAut UA & ( for x being set st x in UAAut UA holds h . x = 0 .--> x ) implies rng h = MSAAut (MSAlg UA) ) assume that A1: dom h = UAAut UA and A2: for x being set st x in UAAut UA holds h . x = 0 .--> x ; ::_thesis: rng h = MSAAut (MSAlg UA) thus rng h c= MSAAut (MSAlg UA) :: according to XBOOLE_0:def_10 ::_thesis: MSAAut (MSAlg UA) c= rng h proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng h or x in MSAAut (MSAlg UA) ) assume x in rng h ; ::_thesis: x in MSAAut (MSAlg UA) then consider q being set such that A3: q in dom h and A4: x = h . q by FUNCT_1:def_3; consider q9 being Element of UAAut UA such that A5: q9 = q by A1, A3; ( x = 0 .--> q & 0 .--> q is ManySortedFunction of (MSAlg UA),(MSAlg UA) ) by A1, A2, A3, A4, Th32; then consider d being ManySortedFunction of (MSAlg UA),(MSAlg UA) such that A6: d = x ; q9 is_isomorphism UA,UA by Def1; then A7: MSAlg q9 is_isomorphism MSAlg UA,(MSAlg UA) Over (MSSign UA) by MSUHOM_1:20; MSAlg q9 = 0 .--> q by A5, MSUHOM_1:def_3 .= x by A1, A2, A3, A4 ; then d is_isomorphism MSAlg UA, MSAlg UA by A6, A7, MSUHOM_1:9; hence x in MSAAut (MSAlg UA) by A6, Def5; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in MSAAut (MSAlg UA) or x in rng h ) assume A8: x in MSAAut (MSAlg UA) ; ::_thesis: x in rng h then reconsider f = x as ManySortedFunction of (MSAlg UA),(MSAlg UA) by Th19; the carrier of (MSSign UA) = {0} by MSUALG_1:def_8; then A9: f = 0 .--> (f . 0) by Th11; A10: f is_isomorphism MSAlg UA, MSAlg UA by A8, Def5; ex q being set st ( q in dom h & x = h . q ) proof take q = f . 0; ::_thesis: ( q in dom h & x = h . q ) f is ManySortedFunction of (MSAlg UA),((MSAlg UA) Over (MSSign UA)) by MSUHOM_1:9; then reconsider q9 = q as Function of UA,UA by Th31; MSAlg q9 = f by A9, MSUHOM_1:def_3; then MSAlg q9 is_isomorphism MSAlg UA,(MSAlg UA) Over (MSSign UA) by A10, MSUHOM_1:9; then q9 is_isomorphism UA,UA by MSUHOM_1:24; hence q in dom h by A1, Def1; ::_thesis: x = h . q hence x = h . q by A1, A2, A9; ::_thesis: verum end; hence x in rng h by FUNCT_1:def_3; ::_thesis: verum end; theorem Th33: :: AUTALG_1:33 for UA being Universal_Algebra for h being Function st dom h = UAAut UA & ( for x being set st x in UAAut UA holds h . x = 0 .--> x ) holds h is Homomorphism of (UAAutGroup UA),(MSAAutGroup (MSAlg UA)) proof let UA be Universal_Algebra; ::_thesis: for h being Function st dom h = UAAut UA & ( for x being set st x in UAAut UA holds h . x = 0 .--> x ) holds h is Homomorphism of (UAAutGroup UA),(MSAAutGroup (MSAlg UA)) let h be Function; ::_thesis: ( dom h = UAAut UA & ( for x being set st x in UAAut UA holds h . x = 0 .--> x ) implies h is Homomorphism of (UAAutGroup UA),(MSAAutGroup (MSAlg UA)) ) assume that A1: dom h = UAAut UA and A2: for x being set st x in UAAut UA holds h . x = 0 .--> x ; ::_thesis: h is Homomorphism of (UAAutGroup UA),(MSAAutGroup (MSAlg UA)) set H = MSAAutGroup (MSAlg UA); set G = UAAutGroup UA; rng h c= the carrier of (MSAAutGroup (MSAlg UA)) by A1, A2, Lm4; then reconsider h9 = h as Function of (UAAutGroup UA),(MSAAutGroup (MSAlg UA)) by A1, FUNCT_2:def_1, RELSET_1:4; now__::_thesis:_for_a,_b_being_Element_of_(UAAutGroup_UA)_holds_h9_._(a_*_b)_=_(h9_._a)_*_(h9_._b) let a, b be Element of (UAAutGroup UA); ::_thesis: h9 . (a * b) = (h9 . a) * (h9 . b) thus h9 . (a * b) = (h9 . a) * (h9 . b) ::_thesis: verum proof reconsider a9 = a, b9 = b as Element of UAAut UA ; A3: h9 . (b9 * a9) = 0 .--> (b9 * a9) by A2, Th6; reconsider A = 0 .--> a9, B = 0 .--> b9 as ManySortedFunction of (MSAlg UA),(MSAlg UA) by Th32; reconsider ha = h9 . a, hb = h9 . b as Element of MSAAut (MSAlg UA) ; reconsider A9 = A, B9 = B as Element of (MSAAutGroup (MSAlg UA)) by Th27; A4: ( ha = A9 & hb = B9 ) by A2; thus h9 . (a * b) = h9 . (b9 * a9) by Def2 .= MSAlg (b9 * a9) by A3, MSUHOM_1:def_3 .= (MSAlg b9) ** (MSAlg a9) by MSUHOM_1:26 .= B ** (MSAlg a9) by MSUHOM_1:def_3 .= B ** A by MSUHOM_1:def_3 .= (h9 . a) * (h9 . b) by A4, Def6 ; ::_thesis: verum end; end; hence h is Homomorphism of (UAAutGroup UA),(MSAAutGroup (MSAlg UA)) by GROUP_6:def_6; ::_thesis: verum end; theorem Th34: :: AUTALG_1:34 for UA being Universal_Algebra for h being Homomorphism of (UAAutGroup UA),(MSAAutGroup (MSAlg UA)) st ( for x being set st x in UAAut UA holds h . x = 0 .--> x ) holds h is bijective proof let UA be Universal_Algebra; ::_thesis: for h being Homomorphism of (UAAutGroup UA),(MSAAutGroup (MSAlg UA)) st ( for x being set st x in UAAut UA holds h . x = 0 .--> x ) holds h is bijective let h be Homomorphism of (UAAutGroup UA),(MSAAutGroup (MSAlg UA)); ::_thesis: ( ( for x being set st x in UAAut UA holds h . x = 0 .--> x ) implies h is bijective ) set G = UAAutGroup UA; assume A1: for x being set st x in UAAut UA holds h . x = 0 .--> x ; ::_thesis: h is bijective for a, b being Element of (UAAutGroup UA) st h . a = h . b holds a = b proof let a, b be Element of (UAAutGroup UA); ::_thesis: ( h . a = h . b implies a = b ) assume A2: h . a = h . b ; ::_thesis: a = b A3: h . b = 0 .--> b by A1 .= [:{0},{b}:] ; h . a = 0 .--> a by A1 .= [:{0},{a}:] ; then {a} = {b} by A2, A3, ZFMISC_1:110; hence a = b by ZFMISC_1:3; ::_thesis: verum end; then A4: h is one-to-one by GROUP_6:1; dom h = UAAut UA by FUNCT_2:def_1; then rng h = the carrier of (MSAAutGroup (MSAlg UA)) by A1, Lm4; then h is onto by FUNCT_2:def_3; hence h is bijective by A4; ::_thesis: verum end; theorem :: AUTALG_1:35 for UA being Universal_Algebra holds UAAutGroup UA, MSAAutGroup (MSAlg UA) are_isomorphic proof let UA be Universal_Algebra; ::_thesis: UAAutGroup UA, MSAAutGroup (MSAlg UA) are_isomorphic deffunc H1( set ) -> set = 0 .--> \$1; consider h being Function such that A1: ( dom h = UAAut UA & ( for x being set st x in UAAut UA holds h . x = H1(x) ) ) from FUNCT_1:sch_3(); reconsider h = h as Homomorphism of (UAAutGroup UA),(MSAAutGroup (MSAlg UA)) by A1, Th33; take h ; :: according to GROUP_6:def_11 ::_thesis: h is bijective thus h is bijective by A1, Th34; ::_thesis: verum end;