:: AUTALG_1 semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

theorem Th1: :: AUTALG_1:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for UA being Universal_Algebra holds id the carrier of UA is_isomorphism UA,UA
proof 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 f being Element of it holds f is Function of UA,UA ) & ( 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 f being Element of b1 holds f is Function of UA,UA ) & ( for h being Function of UA,UA holds
( h in b1 iff h is_isomorphism UA,UA ) ) )
proof end;
uniqueness
for b1, b2 being FUNCTION_DOMAIN of the carrier of UA,the carrier of UA st ( for f being Element of b1 holds f is Function of UA,UA ) & ( for h being Function of UA,UA holds
( h in b1 iff h is_isomorphism UA,UA ) ) & ( for f being Element of b2 holds f is Function of UA,UA ) & ( for h being Function of UA,UA holds
( h in b2 iff h is_isomorphism UA,UA ) ) holds
b1 = b2
proof 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 f being Element of b2 holds f is Function of UA,UA ) & ( for h being Function of UA,UA holds
( h in b2 iff h is_isomorphism UA,UA ) ) ) );

theorem :: AUTALG_1:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for UA being Universal_Algebra holds UAAut UA c= Funcs the carrier of UA,the carrier of UA
proof end;

theorem :: AUTALG_1:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th4: :: AUTALG_1:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for UA being Universal_Algebra holds id the carrier of UA in UAAut UA
proof end;

theorem :: AUTALG_1:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 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 end;

theorem Th6: :: AUTALG_1:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for UA being Universal_Algebra
for f being Element of UAAut UA holds f " in UAAut UA
proof end;

theorem Th7: :: AUTALG_1:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for UA being Universal_Algebra
for f1, f2 being Element of UAAut UA holds f1 * f2 in UAAut UA
proof 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 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 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
HGrStr(# (UAAut UA),(UAAutComp UA) #);
coherence
HGrStr(# (UAAut UA),(UAAutComp UA) #) is Group
proof end;
end;

:: deftheorem defines UAAutGroup AUTALG_1:def 3 :
for UA being Universal_Algebra holds UAAutGroup UA = HGrStr(# (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 end;

theorem Th8: :: AUTALG_1:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 Th9: :: AUTALG_1:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for UA being Universal_Algebra holds id the carrier of UA = 1. (UAAutGroup UA)
proof end;

theorem :: AUTALG_1:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem :: AUTALG_1:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem Th12: :: AUTALG_1:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x being set
for A being ManySortedSet of {x} holds A = x .--> (A . x)
proof end;

theorem Th13: :: AUTALG_1:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for F, G, H being Function-yielding Function holds (H ** G) ** F = H ** (G ** F)
proof end;

theorem Th14: :: AUTALG_1:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem :: AUTALG_1:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem Th16: :: AUTALG_1:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for F, G being Function-yielding Function st F is "1-1" & G is "1-1" holds
G ** F is "1-1"
proof end;

theorem Th17: :: AUTALG_1:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem :: AUTALG_1:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem Th19: :: AUTALG_1:19  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem :: AUTALG_1:20  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th21: :: AUTALG_1:21  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 product (MSFuncs A,B) holds
x is ManySortedFunction of A,B
proof end;

theorem Th22: :: AUTALG_1:22  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 product (MSFuncs A,B)
proof end;

theorem Th23: :: AUTALG_1:23  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for A, B being ManySortedSet of I st A is_transformable_to B holds
MSFuncs A,B is non-empty
proof end;

definition
let I be set ;
let A, B be ManySortedSet of I;
assume A1: A is_transformable_to B ;
canceled;
canceled;
mode MSFunctionSet of A,B -> non empty set means :Def6: :: AUTALG_1:def 6
for x being set st x in it holds
x is ManySortedFunction of A,B;
existence
ex b1 being non empty set st
for x being set st x in b1 holds
x is ManySortedFunction of A,B
proof end;
end;

:: deftheorem AUTALG_1:def 4 :
canceled;

:: deftheorem AUTALG_1:def 5 :
canceled;

:: deftheorem Def6 defines MSFunctionSet AUTALG_1:def 6 :
for I being set
for A, B being ManySortedSet of I st A is_transformable_to B holds
for b4 being non empty set holds
( b4 is MSFunctionSet of A,B iff for x being set st x in b4 holds
x is ManySortedFunction of A,B );

registration
let I be set ;
let A be ManySortedSet of I;
cluster MSFuncs A,A -> V2 ;
coherence
MSFuncs A,A is non-empty
proof end;
end;

definition
let S be non empty non void ManySortedSign ;
let U1, U2 be non-empty MSAlgebra of S;
mode MSFunctionSet of U1,U2 is MSFunctionSet of the Sorts of U1,the Sorts of U2;
end;

registration
let I be set ;
let D be ManySortedSet of I;
cluster non empty MSFunctionSet of D,D;
existence
not for b1 being MSFunctionSet of D,D holds b1 is empty
proof end;
end;

definition
let I be set ;
let D be ManySortedSet of I;
let A be non empty MSFunctionSet of 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
by Def6;
end;

theorem :: AUTALG_1:24  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for A being ManySortedSet of I holds id A is "onto"
proof end;

theorem :: AUTALG_1:25  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for A being ManySortedSet of I holds id A is "1-1"
proof end;

theorem :: AUTALG_1:26  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: AUTALG_1:27  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being non empty non void ManySortedSign
for U1 being non-empty MSAlgebra of S holds id the Sorts of U1 in product (MSFuncs the Sorts of U1,the Sorts of U1) by Th22;

definition
let S be non empty non void ManySortedSign ;
let U1 be non-empty MSAlgebra of S;
func MSAAut U1 -> MSFunctionSet of the Sorts of U1,the Sorts of U1 means :Def7: :: AUTALG_1:def 7
( ( for f being Element of it holds f is ManySortedFunction of U1,U1 ) & ( for h being ManySortedFunction of U1,U1 holds
( h in it iff h is_isomorphism U1,U1 ) ) );
existence
ex b1 being MSFunctionSet of the Sorts of U1,the Sorts of U1 st
( ( for f being Element of b1 holds f is ManySortedFunction of U1,U1 ) & ( for h being ManySortedFunction of U1,U1 holds
( h in b1 iff h is_isomorphism U1,U1 ) ) )
proof end;
uniqueness
for b1, b2 being MSFunctionSet of the Sorts of U1,the Sorts of U1 st ( for f being Element of b1 holds f is ManySortedFunction of U1,U1 ) & ( for h being ManySortedFunction of U1,U1 holds
( h in b1 iff h is_isomorphism U1,U1 ) ) & ( for f being Element of b2 holds f is ManySortedFunction of U1,U1 ) & ( for h being ManySortedFunction of U1,U1 holds
( h in b2 iff h is_isomorphism U1,U1 ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def7 defines MSAAut AUTALG_1:def 7 :
for S being non empty non void ManySortedSign
for U1 being non-empty MSAlgebra of S
for b3 being MSFunctionSet of the Sorts of U1,the Sorts of U1 holds
( b3 = MSAAut U1 iff ( ( for f being Element of b3 holds f is ManySortedFunction of U1,U1 ) & ( for h being ManySortedFunction of U1,U1 holds
( h in b3 iff h is_isomorphism U1,U1 ) ) ) );

theorem :: AUTALG_1:28  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: AUTALG_1:29  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being non empty non void ManySortedSign
for U1 being non-empty MSAlgebra of S
for f being Element of MSAAut U1 holds f in product (MSFuncs the Sorts of U1,the Sorts of U1) by Th22;

theorem :: AUTALG_1:30  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being non empty non void ManySortedSign
for U1 being non-empty MSAlgebra of S holds MSAAut U1 c= product (MSFuncs the Sorts of U1,the Sorts of U1)
proof end;

Lm3: for S being non empty non void ManySortedSign
for U1 being non-empty MSAlgebra of S
for f being Element of MSAAut U1 holds
( f is "1-1" & f is "onto" )
proof end;

theorem Th31: :: AUTALG_1:31  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being non empty non void ManySortedSign
for U1 being non-empty MSAlgebra of S holds id the Sorts of U1 in MSAAut U1
proof end;

theorem Th32: :: AUTALG_1:32  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being non empty non void ManySortedSign
for U1 being non-empty MSAlgebra of S
for f being Element of MSAAut U1 holds f "" in MSAAut U1
proof end;

theorem Th33: :: AUTALG_1:33  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being non empty non void ManySortedSign
for U1 being non-empty MSAlgebra of S
for f1, f2 being Element of MSAAut U1 holds f1 ** f2 in MSAAut U1
proof end;

theorem Th34: :: AUTALG_1:34  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

definition
let S be non empty non void ManySortedSign ;
let U1 be non-empty MSAlgebra of S;
func MSAAutComp U1 -> BinOp of MSAAut U1 means :Def8: :: AUTALG_1:def 8
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 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 end;
end;

:: deftheorem Def8 defines MSAAutComp AUTALG_1:def 8 :
for S being non empty non void ManySortedSign
for U1 being non-empty MSAlgebra of 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 of S;
func MSAAutGroup U1 -> Group equals :: AUTALG_1:def 9
HGrStr(# (MSAAut U1),(MSAAutComp U1) #);
coherence
HGrStr(# (MSAAut U1),(MSAAutComp U1) #) is Group
proof end;
end;

:: deftheorem defines MSAAutGroup AUTALG_1:def 9 :
for S being non empty non void ManySortedSign
for U1 being non-empty MSAlgebra of S holds MSAAutGroup U1 = HGrStr(# (MSAAut U1),(MSAAutComp U1) #);

registration
let S be non empty non void ManySortedSign ;
let U1 be non-empty MSAlgebra of S;
cluster MSAAutGroup U1 -> strict ;
coherence
MSAAutGroup U1 is strict
;
end;

theorem Th35: :: AUTALG_1:35  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being non empty non void ManySortedSign
for U1 being non-empty MSAlgebra of 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 Def8;

theorem Th36: :: AUTALG_1:36  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being non empty non void ManySortedSign
for U1 being non-empty MSAlgebra of S holds id the Sorts of U1 = 1. (MSAAutGroup U1)
proof end;

theorem :: AUTALG_1:37  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being non empty non void ManySortedSign
for U1 being non-empty MSAlgebra of S
for f being Element of MSAAut U1
for g being Element of (MSAAutGroup U1) st f = g holds
f "" = g "
proof end;

theorem Th38: :: AUTALG_1:38  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem Th39: :: AUTALG_1:39  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for UA being Universal_Algebra
for f being Element of UAAut UA holds 0 .--> f is ManySortedFunction of (MSAlg UA),(MSAlg UA)
proof 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 end;

theorem Th40: :: AUTALG_1:40  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem Th41: :: AUTALG_1:41  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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_isomorphism
proof end;

theorem :: AUTALG_1:42  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for UA being Universal_Algebra holds UAAutGroup UA, MSAAutGroup (MSAlg UA) are_isomorphic
proof end;